Theorem EQ-3: On Ternary Boolean Algebra

----- OTTER 2.2, July 1991 -----
The job began on altair.mcs.anl.gov, Fri Jun  5 07:39:41 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,x),g(x)]).

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

list(usable).
0 [] (x = x).
end_of_list.

list(sos).
0 [] (f(f(v,w,x),y,f(v,w,z)) = f(v,w,f(x,y,z))).
0 [] (f(y,x,x) = x).
0 [] (f(x,x,y) = x).
0 [] (f(g(y),y,x) = x).
0 [] (f(a,g(a),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).

------------> process sos:
** KEPT: 2 [] (f(f(x,y,z),u,f(x,y,v)) = f(x,y,f(z,u,v))).
** KEPT: 4 [] (f(x,y,y) = y).
** KEPT: 6 [] (f(x,x,y) = x).
** KEPT: 8 [] (f(g(x),x,y) = y).
** KEPT: 10 [] (f(a,g(a),b) != b).

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

----> UNIT CONFLICT at  16.78 sec ----> 1950 [binary,1948,10] .
Level of proof is 11, length is 19.

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

3,2 [] (f(f(x,y,z),u,f(x,y,v)) = f(x,y,f(z,u,v))).
5,4 [] (f(x,y,y) = y).
7,6 [] (f(x,x,y) = x).
9,8 [] (f(g(x),x,y) = y).
10 [] (f(a,g(a),b) != b).
12,11 [para_into,2,6,demod,7,7] (f(x,y,x) = x).
16 [para_into,2,4] (f(f(x,y,z),u,y) = f(x,y,f(z,u,y))).
21,20 [para_into,2,6] (f(x,y,f(z,f(x,y,z),u)) = f(x,y,z)).
24 [para_from,11,2] (f(f(x,y,z),u,x) = f(x,y,f(z,u,x))).
50 [para_into,16,11] (f(x,z,f(x,y,z)) = f(x,y,z)).
53,52 [para_into,16,2] (f(f(x,y,f(z,u,v)),w,u) = f(f(x,y,z),u,f(f(x,y,v),w,u))).
82 [para_into,20,4] (f(x,y,f(x,y,z)) = f(x,y,z)).
90 [para_from,20,50,demod,21] (f(x,f(y,f(x,z,y),u),f(x,z,y)) = f(x,z,y)).
102 [para_from,82,2,demod,3] (f(x,y,f(z,u,f(x,y,v))) = f(x,y,f(z,u,v))).
351,350 [para_from,90,20,demod,5] (f(x,f(y,z,x),y) = f(y,z,x)).
386,385 [para_from,350,24] (f(f(x,y,z),u,z) = f(z,f(x,y,z),f(x,u,z))).
445 [para_into,102,20,demod,5] (f(x,f(y,z,x),f(y,z,u)) = f(y,z,x)).
506,505 [para_into,445,50] (f(x,f(y,z,x),f(y,u,z)) = f(y,z,x)).
524,523 [para_into,445,4] (f(x,f(y,z,x),z) = f(y,z,x)).
781 [para_from,505,350,demod,506] (f(f(x,y,z),f(x,z,u),u) = f(x,z,u)).
1301 [para_into,781,523,demod,53,12,524,524] (f(f(x,y,z),u,f(z,u,x)) = f(z,u,x)).
1734 [para_into,1301,523] (f(f(x,y,z),u,f(y,u,z)) = f(y,u,z)).
1855 [para_into,1734,8,demod,386,9] (f(z,f(x,g(y),z),f(x,y,z)) = z).
1948 [para_into,1855,6,demod,351] (f(y,g(y),x) = x).
1950 [binary,1948,10] .

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

-------------- statistics -------------
clauses input                  6
clauses given                 47
clauses generated           3945
demod & eval rewrites       6838
tautologies deleted            0
clauses forward subsumed    3103
  (subsumed by sos)           19
clauses kept                1030
new demodulators             919
empty clauses                  1
clauses back demodulated     182
clauses back subsumed          3
sos size                     798
Kbytes malloced             1564

----------- times (seconds) -----------
run time            16.81                   (run time  0 hr, 0 min, 16 sec)
system time          1.85
input time           0.01
  clausify time      0.00
  process input      0.02
para_into time       0.50
para_from time       0.43
pre_process time    11.37
  demod time         6.77
  weigh cl time      0.00
  for_sub time       0.92
  renumber time      0.28
  keep cl time       1.41
  print_cl time      0.00
  conflict time      0.17
post_process time    4.32
  back demod time    3.01
  back_sub time      1.30
lex_rpo time         0.40
The job finished        Fri Jun  5 07:40:00 1992