Next: Theorem EQ-5: On Wajsberg
Up: Summary of Otter Outputs
Previous: Theorem EQ-3: On Ternary
----- OTTER 2.2, July 1991 -----
The job began on altair.mcs.anl.gov, Fri Jun 5 07:36:59 1992
The command was "otter22".
set(knuth_bendix).
set(index_for_back_demod).
set(process_input).
assign(max_mem,16000).
set(control_memory).
set(lex_rpo).
clear(print_kept).
clear(print_new_demod).
clear(print_back_demod).
lex([a,b,c,f(x,x),i(x)]).
lrpo_lr_status([f(x,x)]).
list(usable).
0 [] (x = x).
end_of_list.
list(sos).
0 [] (f(x,i(f(f(i(f(i(y),f(i(x),w))),z),i(f(y,z))))) = w).
0 [] (f(a,f(b,c)) != f(f(a,b),c)).
end_of_list.
OTTER sets dynamic_demod_all, because knuth_bendix is set.
OTTER clears para_into_right, because knuth_bendix is set.
OTTER sets back_demod, because knuth_bendix is set.
OTTER sets para_from, because knuth_bendix is set.
OTTER sets para_into, because knuth_bendix is set.
OTTER clears para_from_right, because knuth_bendix is set.
OTTER sets dynamic_demod, because back_demod is set.
OTTER sets order_eq, because dynamic_demod is set.
------------> process usable:
** KEPT: 1 [] (x = x).
++++ cannot make into demodulator: 1 [] (x = x).
------------> process sos:
** KEPT: 2 [] (f(x,i(f(f(i(f(i(y),f(i(x),z))),u),i(f(y,u))))) = z).
** KEPT: 4 [] (f(f(a,b),c) != f(a,f(b,c))).
------------> done processing input.
----> UNIT CONFLICT at 44.12 sec ----> 4092 [binary,4090,4] .
Level of proof is 50, length is 92.
---------------- PROOF ----------------
3,2 [] (f(x,i(f(f(i(f(i(y),f(i(x),z))),u),i(f(y,u))))) = z).
4 [] (f(f(a,b),c) != f(a,f(b,c))).
5 [para_into,2,2] (f(x,i(f(f(i(f(i(y),z)),u),i(f(y,u))))) = i(f(f(i(f(i(v),
f(i(i(x)),z))),w),i(f(v,w))))).
12 [para_into,5,5] (f(x,i(f(i(f(f(i(f(i(y),f(i(i(i(f(i(z),u)))),v))),w),
i(f(y,w)))),i(f(z,i(f(f(i(f(i(v6),v)),v7),i(f(v6,v7))))))))) =
i(f(f(i(f(i(v8),f(i(i(x)),u))),v9),i(f(v8,v9))))).
19,18 [para_into,5,2] (i(f(f(i(f(i(y),f(i(i(z)),f(i(z),x)))),u),i(f(y,u)))) = x).
29 [para_into,18,18,demod,19] (i(f(f(i(f(i(x),f(i(y),f(y,w)))),v6),i(f(x,v6)))) = w).
48 [para_into,29,5] (i(f(i(f(f(i(f(i(x),f(i(i(i(f(i(y),f(i(z),f(z,u)))))),v))),
w),i(f(x,w)))),i(f(y,i(f(f(i(f(i(v6),v)),v7),i(f(v6,v7)))))))) = u).
50 [para_into,29,2] (i(f(x,i(f(y,i(f(f(i(f(i(z),f(i(i(f(i(y),f(i(u),f(u,v))))),
x))),w),i(f(z,w)))))))) = v).
60 [para_from,29,5] (i(f(f(i(f(i(z),f(i(i(x)),f(i(u),f(u,y))))),v),i(f(z,v)))) = f(x,y)).
81 [para_into,60,5] (i(f(i(f(f(i(f(i(x),f(i(i(i(f(i(y),f(i(i(z)),f(i(u),
f(u,v))))))),w))),v6),i(f(x,v6)))),i(f(y,i(f(f(i(f(i(v7),w)),
v8),i(f(v7,v8)))))))) = f(z,v)).
98,97 [para_from,60,5] (i(f(f(i(f(i(u),f(i(i(x)),f(i(i(y)),f(i(v),f(v,z)))))),
w),i(f(u,w)))) = f(x,f(y,z))).
99 [para_from,60,2] (f(i(x),f(x,y)) = f(i(z),f(z,y))).
114 [para_into,99,99] (f(i(i(x)),f(i(y),f(y,z))) = f(i(u),f(u,f(x,z)))).
116,115 [para_into,99,5,demod,3] (f(i(v),f(v,i(f(f(i(f(i(w),z)),v6),i(f(w,v6)))))) = z).
125 [para_from,99,29] (i(f(f(i(f(i(x),f(x,f(y,z)))),u),i(f(i(y),u)))) = z).
136 [para_from,99,2] (f(x,i(f(f(i(f(i(y),f(y,z))),u),i(f(i(x),u))))) = z).
146 [para_from,114,60,demod,98] (f(y,f(i(z),f(z,v))) = f(y,f(i(v6),f(v6,v)))).
158 [para_into,146,99] (f(x,f(i(i(y)),f(i(z),f(z,u)))) = f(x,f(i(v),f(v,f(y,u))))).
160 [para_from,146,99] (f(i(x),f(x,f(i(y),f(y,z)))) = f(i(u),f(u,f(i(v),f(v,z))))).
210 [para_into,115,99] (f(i(x),f(x,i(f(f(i(f(i(y),f(y,z))),u),i(f(v,u)))))) = f(v,z)).
221,220 [para_into,115,99] (f(i(x),f(x,i(f(f(i(y),f(y,z)),i(f(u,f(f(i(u),v),z))))))) = v).
224 [para_into,115,2] (f(i(x),f(x,i(f(y,i(f(z,i(f(f(i(f(i(u),f(i(i(f(i(z),v))),
y))),w),i(f(u,w)))))))))) = v).
300,299 [para_into,125,99] (i(f(f(i(f(i(x),f(x,f(y,z)))),f(y,u)),i(f(i(v),f(v,u))))) = z).
355 [para_into,136,99] (f(x,i(f(f(i(y),f(y,z)),i(f(i(x),f(f(i(u),f(u,v)),z)))))) = v).
1301 [para_into,355,220,demod,221] (f(f(i(x),f(x,y)),i(f(v6,i(v6)))) = y).
1410 [para_from,1301,210] (f(i(f(i(x),f(x,y))),y) = f(i(f(i(z),f(z,u))),u)).
1434 [para_from,1301,220] (f(i(x),f(x,i(f(f(i(f(i(y),f(y,z))),z),i(f(u,
f(f(i(u),v),i(f(w,i(w)))))))))) = v).
1436 [para_from,1301,114] (f(i(i(x)),f(i(f(i(y),f(y,z))),z)) =
f(i(u),f(u,f(x,i(f(v,i(v))))))).
1484 [para_from,1410,355] (f(f(i(x),f(x,f(f(i(y),f(y,z)),u))),i(f(f(i(v),
f(v,u)),i(f(i(f(i(w),f(w,v6))),v6))))) = z).
1489,1488 [para_from,1410,220,demod,221] (f(i(i(v)),f(i(f(i(w),f(w,v6))),v6)) = v).
1493,1492 [para_from,1410,210] (f(i(x),f(x,i(f(f(i(f(i(y),f(y,z))),z),i(f(u,v)))))) = f(u,v)).
1541 [back_demod,1436,demod,1489] (f(i(u),f(u,f(x,i(f(v,i(v)))))) = x).
1545,1544 [back_demod,1434,demod,1493] (f(u,f(f(i(u),v),i(f(w,i(w))))) = v).
1591 [para_from,1541,1301] (f(x,i(f(y,i(y)))) = f(x,i(f(z,i(z))))).
1675 [para_into,1544,5] (f(x,f(i(f(f(i(f(i(y),f(i(i(i(x))),z))),u),i(f(y,u)))),
i(f(v,i(v))))) = i(f(f(i(f(i(w),z)),v6),i(f(w,v6))))).
1802 [para_from,1488,210] (f(i(x),f(x,i(f(f(i(f(i(y),f(y,z))),f(i(f(i(u),
f(u,v))),v)),i(w))))) = f(i(i(w)),z)).
1857 [para_from,1591,1488] (f(i(i(x)),f(i(f(i(y),f(y,i(f(z,i(z)))))),i(f(u,i(u))))) = x).
1884 [para_from,1591,115,demod,116] (i(f(z,i(z))) = i(f(v,i(v)))).
1948 [para_from,1884,1488,demod,1489] (f(x,i(x)) = f(u,i(u))).
1969 [para_from,1884,99] (f(i(f(x,i(x))),f(f(y,i(y)),z)) = f(i(u),f(u,z))).
2010 [para_from,1948,1544] (f(x,f(y,i(y))) = i(i(x))).
2107 [para_into,2010,99] (f(i(x),f(x,i(y))) = i(i(i(y)))).
2116 [para_from,2010,299] (i(f(i(i(i(f(i(x),f(x,f(y,z)))))),i(f(i(u),f(u,i(y)))))) = z).
2131 [para_from,2010,210] (f(i(x),f(x,i(f(i(i(i(f(i(y),f(y,z))))),i(f(u,f(v,i(v)))))))) = f(u,z)).
2368 [para_into,2107,299,demod,300] (f(i(x),f(x,y)) = i(i(y))).
2373 [para_into,2368,1884] (f(i(f(x,i(x))),f(f(y,i(y)),z)) = i(i(z))).
2381,2380 [para_into,2368,2368] (i(i(f(x,y))) = f(i(i(x)),i(i(y)))).
2401 [para_into,2368,158,demod,2381,2381,2381] (f(i(x),f(x,f(i(y),f(y,f(z,u))))) =
f(i(i(i(i(z)))),f(i(i(i(v))),f(i(i(v)),i(i(u)))))).
2438 [back_demod,2131,demod,2381,2381] (f(i(x),f(x,i(f(i(f(i(i(i(y))),f(i(i(y)),
i(i(z))))),i(f(u,f(v,i(v)))))))) = f(u,z)).
2446 [back_demod,2116,demod,2381,2381,2381] (i(f(i(f(i(i(i(x))),f(i(i(x)),f(i(i(y)),
i(i(z)))))),i(f(i(u),f(u,i(y)))))) = z).
2587 [back_demod,224,demod,2381] (f(i(x),f(x,i(f(y,i(f(z,i(f(f(i(f(i(u),f(f(i(i(i(z))),
i(i(v))),y))),w),i(f(u,w)))))))))) = v).
2598 [back_demod,81,demod,2381,2381,2381,2381] (i(f(i(f(f(i(f(i(x),f(i(f(i(i(i(y))),
f(i(i(i(i(z)))),f(i(i(i(u))),f(i(i(u)),i(i(v))))))),w))),v6),i(f(x,v6)))),
i(f(y,i(f(f(i(f(i(v7),w)),v8),i(f(v7,v8)))))))) = f(z,v)).
2604 [back_demod,50,demod,2381,2381,2381] (i(f(x,i(f(y,i(f(f(i(f(i(z),f(f(i(i(i(y))),
f(i(i(i(u))),f(i(i(u)),i(i(v))))),x))),w),i(f(z,w)))))))) = v).
2606 [back_demod,48,demod,2381,2381,2381] (i(f(i(f(f(i(f(i(x),f(i(f(i(i(i(y))),
f(i(i(i(z))),f(i(i(z)),i(i(u)))))),v))),w),i(f(x,w)))),i(f(y,
i(f(f(i(f(i(v6),v)),v7),i(f(v6,v7)))))))) = u).
2617 [back_demod,12,demod,2381] (f(x,i(f(i(f(f(i(f(i(y),f(i(f(i(i(i(z))),i(i(u)))),
v))),w),i(f(y,w)))),i(f(z,i(f(f(i(f(i(v6),v)),v7),i(f(v6,v7))))))))) =
i(f(f(i(f(i(v8),f(i(i(x)),u))),v9),i(f(v8,v9))))).
2621 [para_from,2368,1488] (i(i(x)) = f(i(y),f(y,x))).
2633 [para_from,2368,210] (f(i(x),f(x,i(f(i(i(y)),i(f(z,f(f(i(u),f(u,v)),y))))))) = f(z,v)).
2647 [para_from,2368,1301] (f(i(i(x)),i(f(y,i(y)))) = x).
2706 [para_from,2368,160] (f(i(x),f(x,f(i(i(y)),i(i(z))))) = f(i(u),f(u,f(i(v),f(v,f(y,z)))))).
2709 [para_from,2368,29] (i(f(f(i(f(i(x),i(i(y)))),z),i(f(x,z)))) = y).
2802,2801 [para_from,2621,1488] (f(i(f(i(x),f(x,y))),f(i(f(i(z),f(z,u))),u)) = i(y)).
2866,2865 [back_demod,1802,demod,2802] (f(i(x),f(x,i(f(i(z),i(w))))) = f(i(i(w)),z)).
2873 [back_demod,2633,demod,2866,2381,2381,2381,2381] (f(f(i(i(z)),f(f(i(i(i(u))),
f(i(i(u)),i(i(v)))),i(i(y)))),i(y)) = f(z,v)).
2879 [back_demod,2438,demod,2866,2381,2381] (f(f(i(i(u)),f(i(i(v)),i(i(i(v))))),
f(i(i(i(y))),f(i(i(y)),i(i(z))))) = f(u,z)).
2884,2883 [para_into,2647,2621] (f(i(f(i(x),f(x,y))),i(f(z,i(z)))) = i(y)).
2921,2920 [back_demod,1857,demod,2884,2381] (f(i(i(x)),f(i(i(z)),i(i(i(z))))) = x).
2929,2928 [back_demod,2879,demod,2921] (f(x,f(i(i(i(z))),f(i(i(z)),i(i(u))))) = f(x,u)).
2938,2937 [back_demod,2606,demod,2929] (i(f(i(f(f(i(f(i(x),f(i(f(i(i(i(y))),u)),v))),w),
i(f(x,w)))),i(f(y,i(f(f(i(f(i(v6),v)),v7),i(f(v6,v7)))))))) = u).
2940,2939 [back_demod,2604,demod,2929] (i(f(x,i(f(y,i(f(f(i(f(i(z),f(f(i(i(i(y))),
v),x))),w),i(f(z,w)))))))) = v).
2944,2943 [back_demod,2598,demod,2929,2938] (f(i(i(i(i(z)))),v) = f(z,v)).
2978,2977 [back_demod,2401,demod,2929,2944] (f(i(x),f(x,f(i(y),f(y,f(z,u))))) = f(z,u)).
2985,2984 [back_demod,2617,demod,2938] (i(f(f(i(f(i(v8),f(i(i(x)),u))),v9),i(f(v8,v9)))) =
f(x,i(i(u)))).
2987,2986 [back_demod,2587,demod,2940] (f(i(x),f(x,i(i(v)))) = v).
3017,3016 [back_demod,2706,demod,2978] (f(i(x),f(x,f(i(i(y)),i(i(z))))) = f(y,z)).
3114,3113 [back_demod,1675,demod,2985,1545] (i(f(f(i(f(i(w),z)),v6),i(f(w,v6)))) = i(i(z))).
3204 [back_demod,2873,demod,2987] (f(f(i(i(x)),f(z,i(i(u)))),i(u)) = f(x,z)).
3266 [back_demod,2446,demod,3017] (i(f(i(f(y,z)),i(f(i(u),f(u,i(y)))))) = z).
3344,3343 [back_demod,2709,demod,3114] (i(i(i(i(y)))) = y).
3706,3705 [para_into,3343,2621] (i(f(i(x),f(x,i(y)))) = y).
3711 [back_demod,3266,demod,3706] (i(f(i(f(x,y)),x)) = y).
3752 [para_from,3343,1591] (f(x,i(f(i(i(i(y))),y))) = f(x,i(f(z,i(z))))).
3759 [para_into,3711,1544] (i(f(i(x),y)) = f(f(i(y),x),i(f(z,i(z))))).
3773,3772 [para_into,3711,2010,demod,2381,2381,2381,2381,3344,3344,3344] (f(f(x,i(x)),y) = y).
3814 [back_demod,2373,demod,3773] (f(i(f(x,i(x))),z) = i(i(z))).
3825 [back_demod,1969,demod,3773] (f(i(f(x,i(x))),z) = f(i(u),f(u,z))).
3896,3895 [para_into,3772,1884,demod,3773] (f(i(f(y,i(y))),z) = z).
3900,3899 [para_into,3772,1544,demod,3896] (f(x,i(f(z,i(z)))) = x).
3914,3913 [back_demod,3825,demod,3896] (f(i(z),f(z,y)) = y).
3920,3919 [back_demod,3814,demod,3896] (i(i(y)) = y).
3935,3934 [back_demod,3759,demod,3900] (i(f(i(x),y)) = f(i(y),x)).
3937,3936 [back_demod,3752,demod,3920,3935,3900] (f(x,f(i(y),y)) = x).
4029 [back_demod,3204,demod,3920,3920] (f(f(x,f(y,z)),i(z)) = f(x,y)).
4042 [back_demod,1484,demod,3914,3914,3914,3914,3935,3937] (f(f(z,u),i(u)) = z).
4090 [para_into,4029,4042,demod,3920] (f(f(x,y),z) = f(x,f(y,z))).
4092 [binary,4090,4] .
------------ end of proof -------------
-------------- statistics -------------
clauses input 3
clauses given 57
clauses generated 3417
demod & eval rewrites 9814
tautologies deleted 0
clauses forward subsumed 3327
(subsumed by sos) 503
clauses kept 2507
new demodulators 1584
empty clauses 1
clauses back demodulated 2414
clauses back subsumed 61
sos size 15
Kbytes malloced 4470
----------- times (seconds) -----------
run time 89.93 (run time 0 hr, 1 min, 29 sec)
system time 3.46
input time 0.01
clausify time 0.00
process input 0.01
para_into time 0.69
para_from time 0.83
pre_process time 71.63
demod time 7.86
weigh cl time 0.00
for_sub time 1.73
renumber time 0.84
keep cl time 9.14
print_cl time 0.00
conflict time 0.32
post_process time 16.45
back demod time 14.77
back_sub time 1.43
lex_rpo time 2.54
The job finished Fri Jun 5 07:38:34 1992
Karen D. Toonen
1998-11-18