Started ploop3 Thu Nov 14 16:10:43 CST 2002 on gyro.thornwood. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% op(400, xfx, ^). op(400, xfx, v). lex([X,Y,X,U,0,1,_ ^ _,_ v _, c(_), f(_,_)]). set(knuth_bendix). % set(back_unit_deletion). assign(pick_given_ratio, 3). clear(print_kept). clear(print_new_demod). clear(print_back_demod). clear(sigint_interact). list(usable). x = x. end_of_list. list(sos). % OML 3-basis in terms of join and complement (x v y) v z = x v (y v z). x v c(c(x) v y) = x. x v c(x v c(x v y)) = y v x. % OML JC axiom (right side commuted) c(x) v c(y) = f(x,y). % definition of sheffer stroke c(c(x) v c(y)) = x ^ y. % definition of meet (this helps a lot) % denial of candidate and definitions % f(f(f(f(Y,X),f(X,Z)),U),f(X,f(f(Z,f(f(X,X),Z)),Z))) != X | % X v Y != f(f(X,X),f(Y,Y)) | % c(X) != f(X,X). end_of_list. assign(max_weight, 23). assign(max_seconds, 900). assign(neg_weight, -10). set(sos_arg). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% f(f(f(V0,V2),V2),f(f(f(V2,V1),f(V0,V2)),f(f(V0,V0),V1))) != V2. % Job 1 Search stopped by max_seconds option. clauses kept 132526 user CPU time 900.35 (0 hr, 15 min, 0 sec) f(f(f(V0,V2),V2),f(f(f(V1,V2),f(V0,V2)),f(V1,f(V0,V0)))) != V2. % Job 2 Search stopped by max_seconds option. clauses kept 64507 user CPU time 900.47 (0 hr, 15 min, 0 sec) f(f(f(V0,V2),V2),f(f(V1,f(V0,V0)),f(f(V2,V1),f(V2,V0)))) != V2. % Job 3 Search stopped by max_seconds option. clauses kept 64507 user CPU time 900.46 (0 hr, 15 min, 0 sec) f(f(f(V0,V2),V2),f(f(V1,f(V0,V0)),f(f(V0,V2),f(V2,V1)))) != V2. % Job 4 Search stopped by max_seconds option. clauses kept 64505 user CPU time 900.24 (0 hr, 15 min, 0 sec) f(f(f(V0,f(V0,V2)),V0),f(V2,f(V2,f(f(V1,V0),f(V3,V0))))) != V2. % Job 5 ----> UNIT CONFLICT at 741.56 sec ----> 110031 [binary,110029.1,4729.1] $F. Search stopped by max_proofs option. clauses kept 60741 user CPU time 741.57 (0 hr, 12 min, 21 sec) f(f(f(V0,f(V0,V2)),V0),f(V2,f(V2,f(f(V1,V0),f(V0,V3))))) != V2. % Job 6 ----> UNIT CONFLICT at 746.26 sec ----> 110031 [binary,110029.1,4127.1] $F. Search stopped by max_proofs option. clauses kept 60741 user CPU time 746.26 (0 hr, 12 min, 26 sec) f(f(f(V0,f(V0,V2)),V0),f(V2,f(V2,f(f(V0,V1),f(V3,V0))))) != V2. % Job 7 ----> UNIT CONFLICT at 741.14 sec ----> 110031 [binary,110029.1,4215.1] $F. Search stopped by max_proofs option. clauses kept 60741 user CPU time 741.14 (0 hr, 12 min, 21 sec) f(f(f(V0,f(V0,V2)),V0),f(V2,f(V2,f(f(V0,V1),f(V0,V3))))) != V2. % Job 8 ----> UNIT CONFLICT at 741.71 sec ----> 110031 [binary,110029.1,3924.1] $F. Search stopped by max_proofs option. clauses kept 60741 user CPU time 741.71 (0 hr, 12 min, 21 sec) f(f(V0,f(V0,f(V2,V0))),f(V2,f(V2,f(f(V1,V0),f(V3,V0))))) != V2. % Job 9 ----> UNIT CONFLICT at 740.61 sec ----> 110031 [binary,110029.1,4728.1] $F. Search stopped by max_proofs option. clauses kept 60741 user CPU time 740.61 (0 hr, 12 min, 20 sec) f(f(V0,f(V0,f(V2,V0))),f(V2,f(V2,f(f(V1,V0),f(V0,V3))))) != V2. % Job 10 ----> UNIT CONFLICT at 751.26 sec ----> 110031 [binary,110029.1,4129.1] $F. Search stopped by max_proofs option. clauses kept 60741 user CPU time 751.26 (0 hr, 12 min, 31 sec) f(f(V0,f(V0,f(V2,V0))),f(V2,f(V2,f(f(V0,V1),f(V3,V0))))) != V2. % Job 11 ----> UNIT CONFLICT at 743.01 sec ----> 110031 [binary,110029.1,4217.1] $F. Search stopped by max_proofs option. clauses kept 60741 user CPU time 743.01 (0 hr, 12 min, 23 sec) f(f(V0,f(V0,f(V2,V0))),f(V2,f(V2,f(f(V0,V1),f(V0,V3))))) != V2. % Job 12 ----> UNIT CONFLICT at 741.48 sec ----> 110031 [binary,110029.1,3926.1] $F. Search stopped by max_proofs option. clauses kept 60741 user CPU time 741.48 (0 hr, 12 min, 21 sec) f(f(V0,f(V0,f(V0,V2))),f(V2,f(V2,f(f(V1,V0),f(V3,V0))))) != V2. % Job 13 ----> UNIT CONFLICT at 741.62 sec ----> 110017 [binary,110015.1,4733.1] $F. Search stopped by max_proofs option. clauses kept 60734 user CPU time 741.62 (0 hr, 12 min, 21 sec) f(f(V0,f(V0,f(V0,V2))),f(V2,f(V2,f(f(V1,V0),f(V0,V3))))) != V2. % Job 14 ----> UNIT CONFLICT at 743.19 sec ----> 110017 [binary,110015.1,4131.1] $F. Search stopped by max_proofs option. clauses kept 60734 user CPU time 743.19 (0 hr, 12 min, 23 sec) f(f(V0,f(V0,f(V0,V2))),f(V2,f(V2,f(f(V0,V1),f(V3,V0))))) != V2. % Job 15 ----> UNIT CONFLICT at 740.68 sec ----> 110017 [binary,110015.1,4219.1] $F. Search stopped by max_proofs option. clauses kept 60734 user CPU time 740.69 (0 hr, 12 min, 20 sec) f(f(V0,f(V0,f(V0,V2))),f(V2,f(V2,f(f(V0,V1),f(V0,V3))))) != V2. % Job 16 ----> UNIT CONFLICT at 739.70 sec ----> 110017 [binary,110015.1,3798.1] $F. Search stopped by max_proofs option. clauses kept 60734 user CPU time 739.70 (0 hr, 12 min, 19 sec) f(f(f(V0,V2),V2),f(f(f(f(f(V0,V0),V1),V2),f(V3,V2)),V0)) != V2. % Job 17 ----> UNIT CONFLICT at 9.06 sec ----> 14569 [binary,14568.1,1.1] $F. Search stopped by max_proofs option. clauses kept 8216 user CPU time 9.06 (0 hr, 0 min, 9 sec) f(f(f(V0,V2),V2),f(f(f(f(V1,f(V0,V0)),V2),f(V3,V2)),V0)) != V2. % Job 18 ----> UNIT CONFLICT at 8.97 sec ----> 14569 [binary,14568.1,1.1] $F. Search stopped by max_proofs option. clauses kept 8216 user CPU time 8.97 (0 hr, 0 min, 8 sec) f(f(f(V0,V2),V2),f(f(f(V2,V1),f(f(f(V0,V0),V3),V2)),V0)) != V2. % Job 19 ----> UNIT CONFLICT at 9.17 sec ----> 14569 [binary,14568.1,1.1] $F. Search stopped by max_proofs option. clauses kept 8216 user CPU time 9.17 (0 hr, 0 min, 9 sec) f(f(f(V0,V2),V2),f(f(f(V1,V2),f(f(f(V0,V0),V3),V2)),V0)) != V2. % Job 20 ----> UNIT CONFLICT at 9.01 sec ----> 14569 [binary,14568.1,1.1] $F. Search stopped by max_proofs option. clauses kept 8216 user CPU time 9.02 (0 hr, 0 min, 9 sec) f(f(f(V0,V2),V2),f(f(f(V2,V1),f(f(V3,f(V0,V0)),V2)),V0)) != V2. % Job 21 ----> UNIT CONFLICT at 9.03 sec ----> 14569 [binary,14568.1,1.1] $F. Search stopped by max_proofs option. clauses kept 8216 user CPU time 9.04 (0 hr, 0 min, 9 sec) f(f(f(V0,V2),V2),f(f(f(V1,V2),f(f(V3,f(V0,V0)),V2)),V0)) != V2. % Job 22 ----> UNIT CONFLICT at 9.13 sec ----> 14569 [binary,14568.1,1.1] $F. Search stopped by max_proofs option. clauses kept 8216 user CPU time 9.13 (0 hr, 0 min, 9 sec) f(f(f(V0,V2),V2),f(f(f(V2,V1),f(V0,V2)),f(f(V0,V0),V3))) != V2. % Job 23 Search stopped by max_seconds option. clauses kept 64505 user CPU time 900.36 (0 hr, 15 min, 0 sec) f(f(f(V0,V2),V2),f(f(f(V1,V2),f(V0,V2)),f(f(V0,V0),V3))) != V2. % Job 24 Search stopped by max_seconds option. clauses kept 64500 user CPU time 900.40 (0 hr, 15 min, 0 sec) f(f(f(V0,V2),V2),f(f(f(V0,V2),f(V1,V2)),f(f(V0,V0),V3))) != V2. % Job 25 Search stopped by max_seconds option. clauses kept 64507 user CPU time 900.22 (0 hr, 15 min, 0 sec) f(f(f(V0,V2),V2),f(f(f(V2,V1),f(V0,V2)),f(f(V2,V2),V3))) != V2. % Job 26 ----> UNIT CONFLICT at 2.39 sec ----> 6625 [binary,6624.1,1.1] $F. Search stopped by max_proofs option. clauses kept 3780 user CPU time 2.39 (0 hr, 0 min, 2 sec) f(f(f(V0,V2),V2),f(f(f(V1,V2),f(V0,V2)),f(f(V2,V2),V3))) != V2. % Job 27 ----> UNIT CONFLICT at 2.40 sec ----> 6625 [binary,6624.1,1.1] $F. Search stopped by max_proofs option. clauses kept 3780 user CPU time 2.41 (0 hr, 0 min, 2 sec) f(f(f(V0,V2),V2),f(f(f(V0,V2),f(V1,V2)),f(f(V2,V2),V3))) != V2. % Job 28 ----> UNIT CONFLICT at 2.32 sec ----> 6625 [binary,6624.1,1.1] $F. Search stopped by max_proofs option. clauses kept 3780 user CPU time 2.32 (0 hr, 0 min, 2 sec) f(f(f(V0,V2),V2),f(f(f(V2,V1),f(V0,V2)),f(V3,f(V0,V0)))) != V2. % Job 29 Search stopped by max_seconds option. clauses kept 64505 user CPU time 900.54 (0 hr, 15 min, 0 sec) f(f(f(V0,V2),V2),f(f(f(V1,V2),f(V0,V2)),f(V3,f(V0,V0)))) != V2. % Job 30 Search stopped by max_seconds option. clauses kept 64500 user CPU time 900.26 (0 hr, 15 min, 0 sec) f(f(f(V0,V2),V2),f(f(f(V0,V2),f(V1,V2)),f(V3,f(V0,V0)))) != V2. % Job 31 Search stopped by max_seconds option. clauses kept 64500 user CPU time 900.13 (0 hr, 15 min, 0 sec) f(f(f(V0,V2),V2),f(f(f(V0,V0),V1),f(f(V3,V2),f(V2,V0)))) != V2. % Job 32 Search stopped by max_seconds option. clauses kept 64500 user CPU time 900.25 (0 hr, 15 min, 0 sec) f(f(f(V0,V2),V2),f(f(f(V0,V0),V1),f(f(V2,V3),f(V2,V0)))) != V2. % Job 33 Search stopped by max_seconds option. clauses kept 64507 user CPU time 900.41 (0 hr, 15 min, 0 sec) f(f(f(V0,V2),V2),f(f(f(V0,V0),V1),f(f(V2,V0),f(V2,V3)))) != V2. % Job 34 Search stopped by max_seconds option. clauses kept 64500 user CPU time 900.01 (0 hr, 15 min, 0 sec) f(f(f(V0,V2),V2),f(f(f(V0,V0),V1),f(f(V0,V2),f(V2,V3)))) != V2. % Job 35 Search stopped by max_seconds option. clauses kept 64500 user CPU time 900.08 (0 hr, 15 min, 0 sec) f(f(f(V0,V2),V2),f(f(f(V2,V2),V1),f(f(V3,V2),f(V2,V0)))) != V2. % Job 36 ----> UNIT CONFLICT at 2.21 sec ----> 6623 [binary,6622.1,1.1] $F. Search stopped by max_proofs option. clauses kept 3778 user CPU time 2.21 (0 hr, 0 min, 2 sec) f(f(f(V0,V2),V2),f(f(f(V2,V2),V1),f(f(V0,V2),f(V2,V3)))) != V2. % Job 37 ----> UNIT CONFLICT at 2.18 sec ----> 6623 [binary,6622.1,1.1] $F. Search stopped by max_proofs option. clauses kept 3778 user CPU time 2.18 (0 hr, 0 min, 2 sec) f(f(f(V0,V2),V2),f(f(V1,f(V0,V0)),f(f(V3,V2),f(V2,V0)))) != V2. % Job 38 Search stopped by max_seconds option. clauses kept 64500 user CPU time 900.07 (0 hr, 15 min, 0 sec) f(f(f(V0,V2),V2),f(f(V1,f(V0,V0)),f(f(V2,V3),f(V2,V0)))) != V2. % Job 39 Search stopped by max_seconds option. clauses kept 64512 user CPU time 900.10 (0 hr, 15 min, 0 sec) f(f(f(V0,V2),V2),f(f(V1,f(V0,V0)),f(f(V2,V0),f(V2,V3)))) != V2. % Job 40 Search stopped by max_seconds option. clauses kept 64500 user CPU time 900.16 (0 hr, 15 min, 0 sec) f(f(f(V0,V2),V2),f(f(V1,f(V0,V0)),f(f(V0,V2),f(V2,V3)))) != V2. % Job 41 Search stopped by max_seconds option. clauses kept 64505 user CPU time 900.36 (0 hr, 15 min, 0 sec) f(f(f(V0,V2),V2),f(V0,f(f(f(f(V0,V0),V1),V2),f(V2,V3)))) != V2. % Job 42 ----> UNIT CONFLICT at 9.15 sec ----> 14569 [binary,14568.1,1.1] $F. Search stopped by max_proofs option. clauses kept 8216 user CPU time 9.15 (0 hr, 0 min, 9 sec) f(f(f(V0,V2),V2),f(V0,f(f(f(V1,f(V0,V0)),V2),f(V2,V3)))) != V2. % Job 43 ----> UNIT CONFLICT at 9.06 sec ----> 14569 [binary,14568.1,1.1] $F. Search stopped by max_proofs option. clauses kept 8216 user CPU time 9.06 (0 hr, 0 min, 9 sec) f(f(f(V0,V2),V2),f(V0,f(f(V2,f(f(V0,V0),V1)),f(V2,V3)))) != V2. % Job 44 ----> UNIT CONFLICT at 9.21 sec ----> 14569 [binary,14568.1,1.1] $F. Search stopped by max_proofs option. clauses kept 8216 user CPU time 9.21 (0 hr, 0 min, 9 sec) f(f(f(V0,V2),V2),f(V0,f(f(V2,f(V1,f(V0,V0))),f(V2,V3)))) != V2. % Job 45 ----> UNIT CONFLICT at 9.09 sec ----> 14569 [binary,14568.1,1.1] $F. Search stopped by max_proofs option. clauses kept 8216 user CPU time 9.09 (0 hr, 0 min, 9 sec) f(f(f(V0,V2),V2),f(V0,f(f(V2,V1),f(V2,f(f(V0,V0),V3))))) != V2. % Job 46 ----> UNIT CONFLICT at 8.97 sec ----> 14569 [binary,14568.1,1.1] $F. Search stopped by max_proofs option. clauses kept 8216 user CPU time 8.97 (0 hr, 0 min, 8 sec) f(f(f(V0,V2),V2),f(V0,f(f(V1,V2),f(V2,f(f(V0,V0),V3))))) != V2. % Job 47 ----> UNIT CONFLICT at 9.00 sec ----> 14569 [binary,14568.1,1.1] $F. Search stopped by max_proofs option. clauses kept 8216 user CPU time 9.00 (0 hr, 0 min, 9 sec) f(f(f(V0,V2),V2),f(V0,f(f(V2,V1),f(V2,f(V3,f(V0,V0)))))) != V2. % Job 48 ----> UNIT CONFLICT at 9.00 sec ----> 14569 [binary,14568.1,1.1] $F. Search stopped by max_proofs option. clauses kept 8216 user CPU time 9.00 (0 hr, 0 min, 9 sec) f(f(f(V0,V2),V2),f(V0,f(f(V1,V2),f(V2,f(V3,f(V0,V0)))))) != V2. % Job 49 ----> UNIT CONFLICT at 9.26 sec ----> 14569 [binary,14568.1,1.1] $F. Search stopped by max_proofs option. clauses kept 8216 user CPU time 9.26 (0 hr, 0 min, 9 sec) f(f(V0,V2),f(f(f(f(V2,V0),V2),f(V1,V2)),f(f(V2,V2),V3))) != V2. % Job 50 ----> UNIT CONFLICT at 2.28 sec ----> 6625 [binary,6624.1,1.1] $F. Search stopped by max_proofs option. clauses kept 3780 user CPU time 2.28 (0 hr, 0 min, 2 sec) f(f(V0,V2),f(f(f(f(V0,V2),V2),f(V1,V2)),f(f(V2,V2),V3))) != V2. % Job 51 ----> UNIT CONFLICT at 2.35 sec ----> 6625 [binary,6624.1,1.1] $F. Search stopped by max_proofs option. clauses kept 3780 user CPU time 2.35 (0 hr, 0 min, 2 sec) f(f(V0,V2),f(f(f(V2,f(V2,V0)),f(V1,V2)),f(f(V2,V2),V3))) != V2. % Job 52 ----> UNIT CONFLICT at 2.25 sec ----> 6625 [binary,6624.1,1.1] $F. Search stopped by max_proofs option. clauses kept 3780 user CPU time 2.25 (0 hr, 0 min, 2 sec) f(f(V0,V2),f(f(f(V2,f(V0,V2)),f(V1,V2)),f(f(V2,V2),V3))) != V2. % Job 53 ----> UNIT CONFLICT at 2.27 sec ----> 6625 [binary,6624.1,1.1] $F. Search stopped by max_proofs option. clauses kept 3780 user CPU time 2.27 (0 hr, 0 min, 2 sec) f(f(V0,V2),f(f(f(V2,V2),V1),f(f(f(V2,V0),V2),f(V2,V3)))) != V2. % Job 54 ----> UNIT CONFLICT at 2.37 sec ----> 6625 [binary,6624.1,1.1] $F. Search stopped by max_proofs option. clauses kept 3780 user CPU time 2.37 (0 hr, 0 min, 2 sec) f(f(V0,V2),f(f(f(V2,V2),V1),f(f(f(V0,V2),V2),f(V2,V3)))) != V2. % Job 55 ----> UNIT CONFLICT at 2.39 sec ----> 6625 [binary,6624.1,1.1] $F. Search stopped by max_proofs option. clauses kept 3780 user CPU time 2.39 (0 hr, 0 min, 2 sec) f(f(V0,V2),f(f(f(V2,V2),V1),f(f(V2,f(V2,V0)),f(V2,V3)))) != V2. % Job 56 ----> UNIT CONFLICT at 2.20 sec ----> 6625 [binary,6624.1,1.1] $F. Search stopped by max_proofs option. clauses kept 3780 user CPU time 2.20 (0 hr, 0 min, 2 sec) f(f(V0,V2),f(f(f(V2,V2),V1),f(f(V2,f(V0,V2)),f(V2,V3)))) != V2. % Job 57 ----> UNIT CONFLICT at 2.31 sec ----> 6625 [binary,6624.1,1.1] $F. Search stopped by max_proofs option. clauses kept 3780 user CPU time 2.31 (0 hr, 0 min, 2 sec) f(f(V0,V2),f(f(f(V2,V2),V1),f(f(V2,V3),f(V2,f(V2,V0))))) != V2. % Job 58 ----> UNIT CONFLICT at 2.40 sec ----> 6626 [binary,6625.1,1.1] $F. Search stopped by max_proofs option. clauses kept 3781 user CPU time 2.40 (0 hr, 0 min, 2 sec) Finished ploop3 Fri Nov 15 00:16:11 CST 2002 on gyro.thornwood