Theorem EQ-2: Robbins Algebra, 2#2 Boolean

----- OTTER 2.2, July 1991 -----
The job began on altair.mcs.anl.gov, Fri Jun  5 14:29:55 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,o(x,x),n(x)]).

lrpo_lr_status([o(x,x)]).

list(usable).
0 [] (x = x).
0 [] (o(x,y) = o(y,x)).
0 [] (o(o(x,y),z) = o(x,o(y,z))).
0 [] (n(o(n(o(x,y)),n(o(x,n(y))))) = x).
end_of_list.

list(sos).
0 [] (o(c,c) = c).
0 [] (o(n(o(a,n(b))),n(o(n(a),n(b)))) != b).
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).
** KEPT: 2 [] (o(x,y) = o(y,x)).
++++ cannot make into demodulator: 2 [] (o(x,y) = o(y,x)).
** KEPT: 3 [] (o(o(x,y),z) = o(x,o(y,z))).
** KEPT: 5 [] (n(o(n(o(x,y)),n(o(x,n(y))))) = x).

------------> process sos:
** KEPT: 7 [] (o(c,c) = c).
** KEPT: 9 [] (o(n(o(a,n(b))),n(o(n(a),n(b)))) != b).

------------> done processing input.

Resetting weight limit to 18.
Resetting weight limit to 17.
----> UNIT CONFLICT at  98.19 sec ----> 7578 [binary,7577,1] .
Level of proof is 31, length is 62.

---------------- PROOF ----------------

1 [] (x = x).
2 [] (o(x,y) = o(y,x)).
4,3 [] (o(o(x,y),z) = o(x,o(y,z))).
5 [] (n(o(n(o(x,y)),n(o(x,n(y))))) = x).
8,7 [] (o(c,c) = c).
9 [] (o(n(o(a,n(b))),n(o(n(a),n(b)))) != b).
10 [para_from,7,5] (n(o(n(c),n(o(c,n(c))))) = c).
13,12 [para_from,7,3] (o(c,o(c,x)) = o(c,x)).
15,14 [para_into,12,2] (o(c,o(x,c)) = o(c,x)).
16 [para_from,12,5] (n(o(n(o(c,x)),n(o(c,n(o(c,x)))))) = c).
18 [para_into,14,3] (o(c,o(x,o(y,c))) = o(c,o(x,y))).
20 [para_from,14,5] (n(o(n(o(c,x)),n(o(c,n(o(x,c)))))) = c).
23,22 [para_from,14,3,demod,4,4] (o(c,o(x,o(c,y))) = o(c,o(x,y))).
26 [para_into,10,2] (n(o(n(o(c,n(c))),n(c))) = c).
28 [para_from,10,5] (n(o(n(o(n(c),o(c,n(c)))),c)) = n(c)).
42 [para_from,26,5] (n(o(n(o(n(o(c,n(c))),c)),c)) = n(o(c,n(c)))).
45,44 [para_from,26,5] (n(o(n(o(x,o(n(o(c,n(c))),n(c)))),n(o(x,c)))) = x).
56 [para_into,18,2,demod,4,23] (o(c,o(x,y)) = o(c,o(y,x))).
57 [para_into,18,2,demod,4,4,8] (o(x,o(y,c)) = o(c,o(x,y))).
64 [para_into,56,2,demod,4] (o(x,o(y,c)) = o(c,o(y,x))).
68 [para_from,56,2,demod,4] (o(c,o(x,y)) = o(y,o(x,c))).
70 [para_into,57,2] (o(x,o(c,y)) = o(c,o(x,y))).
71 [para_into,57,2,demod,4] (o(x,o(c,y)) = o(c,o(y,x))).
72 [para_from,57,5] (n(o(n(o(c,o(x,y))),n(o(x,n(o(y,c)))))) = x).
76 [para_from,57,2,demod,4] (o(c,o(x,y)) = o(y,o(c,x))).
82 [para_from,64,5] (n(o(n(o(c,o(x,y))),n(o(y,n(o(x,c)))))) = y).
86 [para_from,64,2,demod,4] (o(c,o(x,y)) = o(x,o(c,y))).
105 [para_into,76,68] (o(x,o(y,c)) = o(x,o(c,y))).
114 [para_into,86,76] (o(x,o(c,y)) = o(y,o(c,x))).
163 [para_into,9,2] (o(n(o(n(b),a)),n(o(n(a),n(b)))) != b).
166 [para_into,28,71] (n(o(n(o(c,o(n(c),n(c)))),c)) = n(c)).
168 [para_into,28,2] (n(o(c,n(o(n(c),o(c,n(c)))))) = n(c)).
180 [para_into,163,2] (o(n(o(n(b),a)),n(o(n(b),n(a)))) != b).
187 [para_from,166,5] (n(o(n(c),n(o(n(o(c,o(n(c),n(c)))),n(c))))) = n(o(c,o(n(c),n(c))))).
190,189 [para_from,168,5,demod,23] (n(o(n(o(c,o(n(c),n(c)))),n(c))) = c).
196,195 [back_demod,187,demod,190] (n(o(c,o(n(c),n(c)))) = n(o(n(c),c))).
201 [back_demod,166,demod,196] (n(o(n(o(n(c),c)),c)) = n(c)).
210,209 [para_into,201,2] (n(o(n(o(c,n(c))),c)) = n(c)).
212,211 [back_demod,42,demod,210] (n(o(n(c),c)) = n(o(c,n(c)))).
219 [back_demod,195,demod,212] (n(o(c,o(n(c),n(c)))) = n(o(c,n(c)))).
230 [para_into,219,68] (n(o(n(c),o(n(c),c))) = n(o(c,n(c)))).
240 [para_into,16,114,demod,8,13] (n(o(n(o(x,c)),n(o(c,n(o(c,x)))))) = c).
276 [para_into,20,2] (n(o(n(o(c,x)),n(o(n(o(x,c)),c)))) = c).
1150 [para_into,240,2] (n(o(n(o(x,c)),n(o(n(o(c,x)),c)))) = c).
2492 [para_into,72,105,demod,13,8] (n(o(n(o(c,x)),n(o(x,n(c))))) = x).
2517,2516 [para_into,72,276] (n(o(n(o(c,o(n(o(c,x)),n(o(x,c))))),c)) = n(o(c,x))).
2590 [para_into,2492,114,demod,8,4] (n(o(n(o(x,c)),n(o(c,o(x,n(c)))))) = o(c,x)).
2636 [para_into,2492,2] (n(o(n(o(c,x)),n(o(n(c),x)))) = x).
2642 [para_into,2492,2] (n(o(n(o(x,n(c))),n(o(c,x)))) = x).
2788 [para_into,2636,230,demod,15] (n(o(n(o(c,n(c))),n(o(c,n(c))))) = o(n(c),c)).
3454 [para_into,82,1150,demod,2517] (n(o(c,x)) = n(o(x,c))).
3508 [para_from,3454,5] (n(o(n(o(c,x)),n(o(n(x),c)))) = c).
3777 [para_into,3508,2] (n(o(n(o(n(x),c)),n(o(c,x)))) = c).
3912,3911 [para_into,3777,26,demod,8] (n(o(n(c),n(o(c,o(n(o(c,n(c))),n(c)))))) = c).
5861 [para_into,2590,209,demod,3912] (o(c,n(o(c,n(c)))) = c).
5928 [para_from,5861,70] (o(c,o(x,n(o(c,n(c))))) = o(x,c)).
5983,5982 [para_from,5928,2642,demod,4,45] (o(x,n(o(c,n(c)))) = x).
6005,6004 [back_demod,2788,demod,5983] (n(n(o(c,n(c)))) = o(n(c),c)).
6015,6014 [para_into,5982,2] (o(n(o(c,n(c))),x) = x).
6039,6038 [para_from,5982,5,demod,6005] (n(o(n(x),n(o(x,o(n(c),c))))) = x).
6040 [para_from,6014,5,demod,6015] (n(o(n(x),n(n(x)))) = n(o(c,n(c)))).
7006 [para_into,6040,6038,demod,6039] (n(o(x,n(x))) = n(o(c,n(c)))).
7023 [para_into,7006,2] (n(o(n(x),x)) = n(o(c,n(c)))).
7066 [para_from,7006,5,demod,6015] (n(n(o(x,n(n(x))))) = x).
7147,7146 [para_into,7066,2] (n(n(o(n(n(x)),x))) = x).
7416,7415 [para_from,7023,5,demod,5983,7147] (n(n(x)) = x).
7576,7575 [para_into,7415,5] (o(n(o(x,y)),n(o(x,n(y)))) = n(x)).
7577 [back_demod,180,demod,7576,7416] (b != b).
7578 [binary,7577,1] .

------------ end of proof -------------

-------------- statistics -------------
clauses input                  6
clauses given                249
clauses generated          50001
demod & eval rewrites     122587
clauses wt,lit,sk delete     901
tautologies deleted            0
clauses forward subsumed   45667
  (subsumed by sos)        10963
clauses kept                4548
new demodulators            3029
empty clauses                  1
clauses back demodulated    1109
clauses back subsumed          3
sos size                    3290
Kbytes malloced             5652

----------- times (seconds) -----------
run time            98.31                   (run time  0 hr, 1 min, 38 sec)
system time         18.22
input time           0.01
  clausify time      0.00
  process input      0.03
para_into time       6.66
para_from time       4.05
pre_process time    63.38
  demod time        24.30
  weigh cl time      0.19
  for_sub time       7.08
  renumber time      3.83
  keep cl time       8.73
  print_cl time      0.00
  conflict time      0.63
post_process time   22.50
  back demod time   16.85
  back_sub time      5.52
lex_rpo time         9.34
The job finished        Fri Jun  5 14:31:54 1992