Started ploop3 Thu Nov 21 16:07:37 CST 2002 on lemma.mcs.anl.gov. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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). % MOL 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) x v c(c(y) v c(x v z)) = c(c(x v y) v c(x v z)). % modularity in JC 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) end_of_list. assign(max_weight, 20). assign(neg_weight, -8). assign(max_seconds, 600). set(sos_arg). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% f(f(f(f(f(V0,V2),V1),V1),V2),f(f(f(V0,V2),f(V1,V2)),V0)) != V2. % Job 1 ----> UNIT CONFLICT at 3.30 sec ----> 8885 [binary,8883.1,3434.1] $F. Search stopped by max_proofs option. clauses kept 5445 user CPU time 3.30 (0 hr, 0 min, 3 sec) f(f(f(f(f(V0,V2),V1),V1),V2),f(V0,f(f(V2,V0),f(V2,V1)))) != V2. % Job 2 ----> UNIT CONFLICT at 2.95 sec ----> 7961 [binary,7959.1,2908.1] $F. Search stopped by max_proofs option. clauses kept 4804 user CPU time 2.95 (0 hr, 0 min, 2 sec) f(f(f(f(f(V0,V2),V1),V1),V2),f(V0,f(f(V1,V2),f(V2,V0)))) != V2. % Job 3 ----> UNIT CONFLICT at 2.96 sec ----> 7998 [binary,7996.1,2960.1] $F. Search stopped by max_proofs option. clauses kept 4827 user CPU time 2.96 (0 hr, 0 min, 2 sec) f(f(f(f(f(V0,V2),V1),V1),V2),f(V0,f(f(V0,V2),f(V2,V1)))) != V2. % Job 4 ----> UNIT CONFLICT at 2.76 sec ----> 7769 [binary,7767.1,2875.1] $F. Search stopped by max_proofs option. clauses kept 4667 user CPU time 2.77 (0 hr, 0 min, 2 sec) f(f(f(f(f(V0,V2),V1),V1),V2),f(V0,f(f(V2,V2),f(V2,V1)))) != V2. % Job 5 ----> UNIT CONFLICT at 2.54 sec ----> 7793 [binary,7791.1,3583.1] $F. Search stopped by max_proofs option. clauses kept 4577 user CPU time 2.54 (0 hr, 0 min, 2 sec) f(f(f(f(f(V0,V2),V1),V1),V2),f(V0,f(f(V2,V2),f(V2,V0)))) != V2. % Job 6 ----> UNIT CONFLICT at 2.51 sec ----> 7793 [binary,7791.1,3583.1] $F. Search stopped by max_proofs option. clauses kept 4577 user CPU time 2.51 (0 hr, 0 min, 2 sec) f(f(f(f(V0,f(V2,V1)),V0),V2),f(f(f(V1,V2),f(V1,V2)),V1)) != V2. % Job 7 ----> UNIT CONFLICT at 2.47 sec ----> 7850 [binary,7848.1,3681.1] $F. Search stopped by max_proofs option. clauses kept 4608 user CPU time 2.47 (0 hr, 0 min, 2 sec) f(f(f(f(V0,f(V1,V2)),V0),V2),f(f(f(V1,V2),f(V1,V2)),V1)) != V2. % Job 8 ----> UNIT CONFLICT at 2.59 sec ----> 7850 [binary,7848.1,3724.1] $F. Search stopped by max_proofs option. clauses kept 4608 user CPU time 2.59 (0 hr, 0 min, 2 sec) f(f(f(f(V0,f(V2,V1)),V0),V2),f(f(f(V1,V2),f(V0,V2)),V1)) != V2. % Job 9 ----> UNIT CONFLICT at 3.29 sec ----> 8885 [binary,8883.1,3906.1] $F. Search stopped by max_proofs option. clauses kept 5445 user CPU time 3.29 (0 hr, 0 min, 3 sec) f(f(f(f(V0,f(V2,V1)),V0),V2),f(f(f(V0,V2),f(V1,V2)),V1)) != V2. % Job 10 ----> UNIT CONFLICT at 4.06 sec ----> 9904 [binary,9902.1,3981.1] $F. Search stopped by max_proofs option. clauses kept 6213 user CPU time 4.06 (0 hr, 0 min, 4 sec) f(f(f(f(V0,f(V1,V2)),V0),V2),f(f(f(V1,V2),f(V0,V2)),V1)) != V2. % Job 11 ----> UNIT CONFLICT at 3.33 sec ----> 8885 [binary,8883.1,3652.1] $F. Search stopped by max_proofs option. clauses kept 5445 user CPU time 3.33 (0 hr, 0 min, 3 sec) f(f(f(f(V0,f(V1,V2)),V0),V2),f(f(f(V0,V2),f(V1,V2)),V1)) != V2. % Job 12 ----> UNIT CONFLICT at 3.97 sec ----> 9904 [binary,9902.1,4236.1] $F. Search stopped by max_proofs option. clauses kept 6213 user CPU time 3.97 (0 hr, 0 min, 3 sec) f(f(f(f(V0,f(V2,V1)),V0),V2),f(V1,f(f(V1,V2),f(V2,V1)))) != V2. % Job 13 ----> UNIT CONFLICT at 2.69 sec ----> 7828 [binary,7826.1,1211.1] $F. Search stopped by max_proofs option. clauses kept 4763 user CPU time 2.69 (0 hr, 0 min, 2 sec) f(f(f(f(V0,f(V2,V1)),V0),V2),f(V1,f(f(V2,V1),f(V2,V0)))) != V2. % Job 14 ----> UNIT CONFLICT at 2.87 sec ----> 7961 [binary,7959.1,2988.1] $F. Search stopped by max_proofs option. clauses kept 4804 user CPU time 2.87 (0 hr, 0 min, 2 sec) f(f(f(f(V0,f(V1,V2)),V0),V2),f(V1,f(f(V2,V1),f(V2,V0)))) != V2. % Job 15 ----> UNIT CONFLICT at 2.89 sec ----> 7961 [binary,7959.1,3086.1] $F. Search stopped by max_proofs option. clauses kept 4804 user CPU time 2.89 (0 hr, 0 min, 2 sec) f(f(f(f(V0,f(V1,V2)),V0),V2),f(V1,f(f(V2,V0),f(V2,V1)))) != V2. % Job 16 ----> UNIT CONFLICT at 2.40 sec ----> 7126 [binary,7124.1,2018.1] $F. Search stopped by max_proofs option. clauses kept 4260 user CPU time 2.40 (0 hr, 0 min, 2 sec) f(f(f(f(V0,f(V1,V2)),V0),V2),f(V1,f(f(V0,V2),f(V2,V1)))) != V2. % Job 17 ----> UNIT CONFLICT at 2.91 sec ----> 7998 [binary,7996.1,3140.1] $F. Search stopped by max_proofs option. clauses kept 4827 user CPU time 2.91 (0 hr, 0 min, 2 sec) f(f(f(f(V0,f(V2,V1)),V0),V2),f(V1,f(f(V2,V2),f(V2,V0)))) != V2. % Job 18 ----> UNIT CONFLICT at 2.58 sec ----> 7793 [binary,7791.1,3673.1] $F. Search stopped by max_proofs option. clauses kept 4577 user CPU time 2.59 (0 hr, 0 min, 2 sec) f(f(f(f(V0,f(V1,V2)),V0),V2),f(V1,f(f(V2,V2),f(V2,V1)))) != V2. % Job 19 ----> UNIT CONFLICT at 2.59 sec ----> 7793 [binary,7791.1,3713.1] $F. Search stopped by max_proofs option. clauses kept 4577 user CPU time 2.60 (0 hr, 0 min, 2 sec) f(f(f(f(V0,f(V1,V2)),V0),V2),f(V1,f(f(V2,V2),f(V2,V0)))) != V2. % Job 20 ----> UNIT CONFLICT at 2.55 sec ----> 7793 [binary,7791.1,3713.1] $F. Search stopped by max_proofs option. clauses kept 4577 user CPU time 2.55 (0 hr, 0 min, 2 sec) f(f(f(f(V0,V2),f(V2,V0)),V0),f(V2,f(f(f(V2,V0),V1),V1))) != V2. % Job 21 ----> UNIT CONFLICT at 2.60 sec ----> 7795 [binary,7793.1,1471.1] $F. Search stopped by max_proofs option. clauses kept 4743 user CPU time 2.60 (0 hr, 0 min, 2 sec) f(f(f(f(V0,V2),f(V2,V1)),V1),f(V2,f(f(f(V2,V1),V0),V0))) != V2. % Job 22 ----> UNIT CONFLICT at 3.42 sec ----> 9255 [binary,9253.1,2979.1] $F. Search stopped by max_proofs option. clauses kept 5692 user CPU time 3.42 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V2,V1)),V1),f(V2,f(f(f(V1,V2),V0),V0))) != V2. % Job 23 ----> UNIT CONFLICT at 3.40 sec ----> 9255 [binary,9253.1,3285.1] $F. Search stopped by max_proofs option. clauses kept 5692 user CPU time 3.40 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V2,V1)),V0),f(V2,f(f(f(V2,V0),V1),V1))) != V2. % Job 24 ----> UNIT CONFLICT at 3.18 sec ----> 8444 [binary,8442.1,2685.1] $F. Search stopped by max_proofs option. clauses kept 5105 user CPU time 3.18 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V2,V1)),V0),f(V2,f(f(f(V0,V2),V1),V1))) != V2. % Job 25 ----> UNIT CONFLICT at 3.10 sec ----> 8444 [binary,8442.1,2810.1] $F. Search stopped by max_proofs option. clauses kept 5105 user CPU time 3.10 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V1,V2)),V1),f(V2,f(f(f(V2,V1),V0),V0))) != V2. % Job 26 ----> UNIT CONFLICT at 3.93 sec ----> 9904 [binary,9902.1,3723.1] $F. Search stopped by max_proofs option. clauses kept 6213 user CPU time 3.93 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V1,V2)),V1),f(V2,f(f(f(V1,V2),V0),V0))) != V2. % Job 27 ----> UNIT CONFLICT at 4.08 sec ----> 9904 [binary,9902.1,3855.1] $F. Search stopped by max_proofs option. clauses kept 6213 user CPU time 4.08 (0 hr, 0 min, 4 sec) f(f(f(f(V0,V2),f(V1,V2)),V0),f(V2,f(f(f(V0,V2),V1),V1))) != V2. % Job 28 ----> UNIT CONFLICT at 3.41 sec ----> 8886 [binary,8884.1,3456.1] $F. Search stopped by max_proofs option. clauses kept 5446 user CPU time 3.41 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V2,V2)),V1),f(V2,f(f(f(V2,V1),V0),V0))) != V2. % Job 29 ----> UNIT CONFLICT at 2.61 sec ----> 7795 [binary,7793.1,1456.1] $F. Search stopped by max_proofs option. clauses kept 4744 user CPU time 2.61 (0 hr, 0 min, 2 sec) f(f(f(f(V0,V2),f(V2,V2)),V1),f(V2,f(f(f(V1,V2),V0),V0))) != V2. % Job 30 ----> UNIT CONFLICT at 2.70 sec ----> 7795 [binary,7793.1,1425.1] $F. Search stopped by max_proofs option. clauses kept 4744 user CPU time 2.70 (0 hr, 0 min, 2 sec) f(f(f(f(V0,V2),f(V2,V0)),V0),f(V2,f(f(V1,f(V2,V0)),V1))) != V2. % Job 31 ----> UNIT CONFLICT at 2.73 sec ----> 7795 [binary,7793.1,1093.1] $F. Search stopped by max_proofs option. clauses kept 4743 user CPU time 2.73 (0 hr, 0 min, 2 sec) f(f(f(f(V0,V2),f(V2,V1)),V1),f(V2,f(f(V0,f(V1,V2)),V0))) != V2. % Job 32 ----> UNIT CONFLICT at 3.53 sec ----> 9255 [binary,9253.1,3462.1] $F. Search stopped by max_proofs option. clauses kept 5692 user CPU time 3.53 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V2,V1)),V0),f(V2,f(f(V1,f(V0,V2)),V1))) != V2. % Job 33 ----> UNIT CONFLICT at 3.15 sec ----> 8444 [binary,8442.1,2657.1] $F. Search stopped by max_proofs option. clauses kept 5105 user CPU time 3.15 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V1,V2)),V1),f(V2,f(f(V0,f(V2,V1)),V0))) != V2. % Job 34 ----> UNIT CONFLICT at 4.16 sec ----> 9904 [binary,9902.1,3803.1] $F. Search stopped by max_proofs option. clauses kept 6213 user CPU time 4.16 (0 hr, 0 min, 4 sec) f(f(f(f(V0,V2),f(V1,V2)),V1),f(V2,f(f(V0,f(V1,V2)),V0))) != V2. % Job 35 ----> UNIT CONFLICT at 3.96 sec ----> 9904 [binary,9902.1,4149.1] $F. Search stopped by max_proofs option. clauses kept 6213 user CPU time 3.96 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V1,V2)),V0),f(V2,f(f(V1,f(V2,V0)),V1))) != V2. % Job 36 ----> UNIT CONFLICT at 3.29 sec ----> 8886 [binary,8884.1,3797.1] $F. Search stopped by max_proofs option. clauses kept 5446 user CPU time 3.29 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V2,V2)),V1),f(V2,f(f(V0,f(V2,V1)),V0))) != V2. % Job 37 ----> UNIT CONFLICT at 2.69 sec ----> 7795 [binary,7793.1,1041.1] $F. Search stopped by max_proofs option. clauses kept 4744 user CPU time 2.70 (0 hr, 0 min, 2 sec) f(f(f(f(V0,V2),f(V2,V2)),V1),f(V2,f(f(V0,f(V1,V2)),V0))) != V2. % Job 38 ----> UNIT CONFLICT at 2.64 sec ----> 7795 [binary,7793.1,1038.1] $F. Search stopped by max_proofs option. clauses kept 4744 user CPU time 2.64 (0 hr, 0 min, 2 sec) f(f(f(f(V0,V2),f(V2,V1)),V0),f(V2,f(V1,f(f(V2,V0),V1)))) != V2. % Job 39 ----> UNIT CONFLICT at 3.11 sec ----> 8444 [binary,8442.1,2248.1] $F. Search stopped by max_proofs option. clauses kept 5105 user CPU time 3.11 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V1,V2)),V1),f(V2,f(V0,f(f(V2,V1),V0)))) != V2. % Job 40 ----> UNIT CONFLICT at 4.09 sec ----> 9904 [binary,9902.1,3725.1] $F. Search stopped by max_proofs option. clauses kept 6213 user CPU time 4.09 (0 hr, 0 min, 4 sec) f(f(f(f(V0,V2),f(V1,V2)),V1),f(V2,f(V0,f(f(V1,V2),V0)))) != V2. % Job 41 ----> UNIT CONFLICT at 3.98 sec ----> 9904 [binary,9902.1,3857.1] $F. Search stopped by max_proofs option. clauses kept 6213 user CPU time 3.98 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V1,V2)),V0),f(V2,f(V1,f(f(V2,V0),V1)))) != V2. % Job 42 ----> UNIT CONFLICT at 3.46 sec ----> 8886 [binary,8884.1,3550.1] $F. Search stopped by max_proofs option. clauses kept 5446 user CPU time 3.46 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V2,V2)),V1),f(V2,f(V0,f(f(V2,V1),V0)))) != V2. % Job 43 ----> UNIT CONFLICT at 2.59 sec ----> 7795 [binary,7793.1,1004.1] $F. Search stopped by max_proofs option. clauses kept 4744 user CPU time 2.59 (0 hr, 0 min, 2 sec) f(f(f(f(V0,V2),f(V2,V2)),V1),f(V2,f(V0,f(f(V1,V2),V0)))) != V2. % Job 44 ----> UNIT CONFLICT at 2.60 sec ----> 7795 [binary,7793.1,1000.1] $F. Search stopped by max_proofs option. clauses kept 4744 user CPU time 2.60 (0 hr, 0 min, 2 sec) f(f(f(f(V0,V2),f(V2,V2)),V0),f(V2,f(V1,f(f(V2,V0),V1)))) != V2. % Job 45 ----> UNIT CONFLICT at 2.56 sec ----> 7795 [binary,7793.1,1004.1] $F. Search stopped by max_proofs option. clauses kept 4744 user CPU time 2.56 (0 hr, 0 min, 2 sec) f(f(f(f(V0,V2),f(V2,V1)),V0),f(V2,f(V1,f(V1,f(V2,V0))))) != V2. % Job 46 ----> UNIT CONFLICT at 3.02 sec ----> 8444 [binary,8442.1,2152.1] $F. Search stopped by max_proofs option. clauses kept 5105 user CPU time 3.02 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V1,V2)),V1),f(V2,f(V0,f(V0,f(V2,V1))))) != V2. % Job 47 ----> UNIT CONFLICT at 4.00 sec ----> 9904 [binary,9902.1,3805.1] $F. Search stopped by max_proofs option. clauses kept 6213 user CPU time 4.00 (0 hr, 0 min, 4 sec) f(f(f(f(V0,V2),f(V2,V2)),V1),f(V2,f(V0,f(V0,f(V2,V1))))) != V2. % Job 48 ----> UNIT CONFLICT at 2.67 sec ----> 7795 [binary,7793.1,906.1] $F. Search stopped by max_proofs option. clauses kept 4744 user CPU time 2.67 (0 hr, 0 min, 2 sec) f(f(f(f(V0,V2),f(V2,V2)),V0),f(V2,f(V1,f(V1,f(V2,V0))))) != V2. % Job 49 ----> UNIT CONFLICT at 2.70 sec ----> 7795 [binary,7793.1,906.1] $F. Search stopped by max_proofs option. clauses kept 4744 user CPU time 2.70 (0 hr, 0 min, 2 sec) f(f(f(V0,f(f(V2,V1),V0)),V2),f(f(f(V1,V2),f(V1,V2)),V1)) != V2. % Job 50 ----> UNIT CONFLICT at 2.49 sec ----> 7850 [binary,7848.1,3706.1] $F. Search stopped by max_proofs option. clauses kept 4608 user CPU time 2.49 (0 hr, 0 min, 2 sec) f(f(f(V0,f(f(V1,V2),V0)),V2),f(f(f(V1,V2),f(V1,V2)),V1)) != V2. % Job 51 ----> UNIT CONFLICT at 2.51 sec ----> 7850 [binary,7848.1,3744.1] $F. Search stopped by max_proofs option. clauses kept 4608 user CPU time 2.51 (0 hr, 0 min, 2 sec) f(f(f(V0,f(f(V2,V1),V0)),V2),f(f(f(V0,V2),f(V1,V2)),V1)) != V2. % Job 52 ----> UNIT CONFLICT at 4.01 sec ----> 9904 [binary,9902.1,3736.1] $F. Search stopped by max_proofs option. clauses kept 6213 user CPU time 4.02 (0 hr, 0 min, 4 sec) f(f(f(V0,f(f(V1,V2),V0)),V2),f(f(f(V1,V2),f(V0,V2)),V1)) != V2. % Job 53 ----> UNIT CONFLICT at 3.43 sec ----> 8885 [binary,8883.1,3436.1] $F. Search stopped by max_proofs option. clauses kept 5445 user CPU time 3.43 (0 hr, 0 min, 3 sec) f(f(f(V0,f(f(V1,V2),V0)),V2),f(f(f(V0,V2),f(V1,V2)),V1)) != V2. % Job 54 ----> UNIT CONFLICT at 4.04 sec ----> 9904 [binary,9902.1,3895.1] $F. Search stopped by max_proofs option. clauses kept 6213 user CPU time 4.04 (0 hr, 0 min, 4 sec) f(f(f(V0,f(f(V1,V2),V0)),V2),f(V1,f(f(V1,V2),f(V2,V1)))) != V2. % Job 55 ----> UNIT CONFLICT at 2.70 sec ----> 7828 [binary,7826.1,1489.1] $F. Search stopped by max_proofs option. clauses kept 4763 user CPU time 2.71 (0 hr, 0 min, 2 sec) f(f(f(V0,f(f(V2,V1),V0)),V2),f(V1,f(f(V2,V1),f(V2,V0)))) != V2. % Job 56 ----> UNIT CONFLICT at 2.88 sec ----> 7961 [binary,7959.1,2707.1] $F. Search stopped by max_proofs option. clauses kept 4804 user CPU time 2.89 (0 hr, 0 min, 2 sec) f(f(f(V0,f(f(V2,V1),V0)),V2),f(V1,f(f(V1,V2),f(V2,V0)))) != V2. % Job 57 ----> UNIT CONFLICT at 2.74 sec ----> 7769 [binary,7767.1,2848.1] $F. Search stopped by max_proofs option. clauses kept 4667 user CPU time 2.74 (0 hr, 0 min, 2 sec) f(f(f(V0,f(f(V2,V1),V0)),V2),f(V1,f(f(V0,V2),f(V2,V1)))) != V2. % Job 58 ----> UNIT CONFLICT at 2.94 sec ----> 7998 [binary,7996.1,2761.1] $F. Search stopped by max_proofs option. clauses kept 4827 user CPU time 2.94 (0 hr, 0 min, 2 sec) f(f(f(V0,f(f(V1,V2),V0)),V2),f(V1,f(f(V2,V1),f(V2,V0)))) != V2. % Job 59 ----> UNIT CONFLICT at 2.83 sec ----> 7961 [binary,7959.1,2761.1] $F. Search stopped by max_proofs option. clauses kept 4804 user CPU time 2.83 (0 hr, 0 min, 2 sec) f(f(f(V0,f(f(V1,V2),V0)),V2),f(V1,f(f(V2,V0),f(V2,V1)))) != V2. % Job 60 ----> UNIT CONFLICT at 2.37 sec ----> 7126 [binary,7124.1,1548.1] $F. Search stopped by max_proofs option. clauses kept 4260 user CPU time 2.38 (0 hr, 0 min, 2 sec) f(f(f(V0,f(f(V2,V1),V0)),V2),f(V1,f(f(V2,V2),f(V2,V0)))) != V2. % Job 61 ----> UNIT CONFLICT at 2.58 sec ----> 7793 [binary,7791.1,3687.1] $F. Search stopped by max_proofs option. clauses kept 4577 user CPU time 2.58 (0 hr, 0 min, 2 sec) f(f(f(V0,f(f(V1,V2),V0)),V2),f(V1,f(f(V2,V2),f(V2,V0)))) != V2. % Job 62 ----> UNIT CONFLICT at 2.48 sec ----> 7793 [binary,7791.1,3707.1] $F. Search stopped by max_proofs option. clauses kept 4577 user CPU time 2.48 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V0,f(V2,V1))),V2),f(f(f(V1,V2),f(V0,V2)),V1)) != V2. % Job 63 ----> UNIT CONFLICT at 3.42 sec ----> 8885 [binary,8883.1,3908.1] $F. Search stopped by max_proofs option. clauses kept 5445 user CPU time 3.42 (0 hr, 0 min, 3 sec) f(f(f(V0,f(V0,f(V1,V2))),V2),f(f(f(V1,V2),f(V0,V2)),V1)) != V2. % Job 64 ----> UNIT CONFLICT at 3.32 sec ----> 8885 [binary,8883.1,3654.1] $F. Search stopped by max_proofs option. clauses kept 5445 user CPU time 3.32 (0 hr, 0 min, 3 sec) f(f(f(V0,f(V0,f(V1,V2))),V2),f(f(f(V0,V2),f(V1,V2)),V1)) != V2. % Job 65 ----> UNIT CONFLICT at 4.07 sec ----> 9904 [binary,9902.1,4238.1] $F. Search stopped by max_proofs option. clauses kept 6213 user CPU time 4.07 (0 hr, 0 min, 4 sec) f(f(f(V0,f(V0,f(V1,V2))),V2),f(V1,f(f(V1,V2),f(V2,V1)))) != V2. % Job 66 ----> UNIT CONFLICT at 2.70 sec ----> 7828 [binary,7826.1,1071.1] $F. Search stopped by max_proofs option. clauses kept 4763 user CPU time 2.71 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V0,f(V2,V1))),V2),f(V1,f(f(V2,V1),f(V2,V0)))) != V2. % Job 67 ----> UNIT CONFLICT at 2.85 sec ----> 7961 [binary,7959.1,2785.1] $F. Search stopped by max_proofs option. clauses kept 4804 user CPU time 2.85 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V0,f(V2,V1))),V2),f(V1,f(f(V2,V0),f(V2,V1)))) != V2. % Job 68 ----> UNIT CONFLICT at 2.40 sec ----> 7126 [binary,7124.1,1912.1] $F. Search stopped by max_proofs option. clauses kept 4260 user CPU time 2.40 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V0,f(V2,V1))),V2),f(V1,f(f(V1,V2),f(V2,V0)))) != V2. % Job 69 ----> UNIT CONFLICT at 2.64 sec ----> 7769 [binary,7767.1,2967.1] $F. Search stopped by max_proofs option. clauses kept 4667 user CPU time 2.64 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V0,f(V2,V1))),V2),f(V1,f(f(V0,V2),f(V2,V1)))) != V2. % Job 70 ----> UNIT CONFLICT at 2.96 sec ----> 7998 [binary,7996.1,2841.1] $F. Search stopped by max_proofs option. clauses kept 4827 user CPU time 2.96 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V0,f(V1,V2))),V2),f(V1,f(f(V2,V1),f(V2,V0)))) != V2. % Job 71 ----> UNIT CONFLICT at 2.92 sec ----> 7961 [binary,7959.1,2883.1] $F. Search stopped by max_proofs option. clauses kept 4804 user CPU time 2.92 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V0,f(V1,V2))),V2),f(V1,f(f(V0,V2),f(V2,V1)))) != V2. % Job 72 ----> UNIT CONFLICT at 2.84 sec ----> 7998 [binary,7996.1,2935.1] $F. Search stopped by max_proofs option. clauses kept 4827 user CPU time 2.84 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V0,f(V2,V1))),V2),f(V1,f(f(V2,V2),f(V2,V0)))) != V2. % Job 73 ----> UNIT CONFLICT at 2.51 sec ----> 7793 [binary,7791.1,3747.1] $F. Search stopped by max_proofs option. clauses kept 4577 user CPU time 2.51 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V0,f(V1,V2))),V2),f(V1,f(f(V2,V2),f(V2,V0)))) != V2. % Job 74 ----> UNIT CONFLICT at 2.62 sec ----> 7793 [binary,7791.1,3767.1] $F. Search stopped by max_proofs option. clauses kept 4577 user CPU time 2.62 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V0),f(V2,V0))),f(V2,f(f(f(V0,V2),V1),V1))) != V2. % Job 75 ----> UNIT CONFLICT at 2.58 sec ----> 7795 [binary,7793.1,1425.1] $F. Search stopped by max_proofs option. clauses kept 4744 user CPU time 2.59 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V1),f(V2,V0))),f(V2,f(f(f(V2,V0),V1),V1))) != V2. % Job 76 ----> UNIT CONFLICT at 2.42 sec ----> 7132 [binary,7130.1,1489.1] $F. Search stopped by max_proofs option. clauses kept 4271 user CPU time 2.42 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V1),f(V2,V0))),f(V2,f(f(f(V0,V2),V1),V1))) != V2. % Job 77 ----> UNIT CONFLICT at 2.42 sec ----> 7132 [binary,7130.1,1257.1] $F. Search stopped by max_proofs option. clauses kept 4271 user CPU time 2.42 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V0),f(V2,V1))),f(V2,f(f(f(V2,V0),V1),V1))) != V2. % Job 78 ----> UNIT CONFLICT at 2.66 sec ----> 7211 [binary,7209.1,1525.1] $F. Search stopped by max_proofs option. clauses kept 4307 user CPU time 2.66 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V0),f(V2,V0))),f(V2,f(f(V1,f(V2,V0)),V1))) != V2. % Job 79 ----> UNIT CONFLICT at 2.66 sec ----> 7795 [binary,7793.1,1041.1] $F. Search stopped by max_proofs option. clauses kept 4744 user CPU time 2.66 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V0),f(V2,V0))),f(V2,f(f(V1,f(V0,V2)),V1))) != V2. % Job 80 ----> UNIT CONFLICT at 2.57 sec ----> 7795 [binary,7793.1,1039.1] $F. Search stopped by max_proofs option. clauses kept 4744 user CPU time 2.57 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V1),f(V2,V0))),f(V2,f(f(V1,f(V2,V0)),V1))) != V2. % Job 81 ----> UNIT CONFLICT at 2.39 sec ----> 7132 [binary,7130.1,2019.1] $F. Search stopped by max_proofs option. clauses kept 4271 user CPU time 2.39 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V0),f(V2,V1))),f(V2,f(f(V1,f(V2,V0)),V1))) != V2. % Job 82 ----> UNIT CONFLICT at 2.54 sec ----> 7211 [binary,7209.1,1845.1] $F. Search stopped by max_proofs option. clauses kept 4307 user CPU time 2.54 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V0),f(V2,V1))),f(V2,f(f(V1,f(V0,V2)),V1))) != V2. % Job 83 ----> UNIT CONFLICT at 2.54 sec ----> 7211 [binary,7209.1,1626.1] $F. Search stopped by max_proofs option. clauses kept 4307 user CPU time 2.55 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V0),f(V2,V0))),f(V2,f(V1,f(f(V2,V0),V1)))) != V2. % Job 84 ----> UNIT CONFLICT at 2.68 sec ----> 7795 [binary,7793.1,1004.1] $F. Search stopped by max_proofs option. clauses kept 4744 user CPU time 2.68 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V0),f(V2,V0))),f(V2,f(V1,f(f(V0,V2),V1)))) != V2. % Job 85 ----> UNIT CONFLICT at 2.71 sec ----> 7795 [binary,7793.1,952.1] $F. Search stopped by max_proofs option. clauses kept 4744 user CPU time 2.72 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V1),f(V2,V0))),f(V2,f(V1,f(f(V2,V0),V1)))) != V2. % Job 86 ----> UNIT CONFLICT at 2.41 sec ----> 7132 [binary,7130.1,1223.1] $F. Search stopped by max_proofs option. clauses kept 4271 user CPU time 2.41 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V1),f(V2,V0))),f(V2,f(V1,f(f(V0,V2),V1)))) != V2. % Job 87 ----> UNIT CONFLICT at 2.40 sec ----> 7132 [binary,7130.1,1039.1] $F. Search stopped by max_proofs option. clauses kept 4271 user CPU time 2.40 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V0),f(V2,V1))),f(V2,f(V1,f(f(V2,V0),V1)))) != V2. % Job 88 ----> UNIT CONFLICT at 2.54 sec ----> 7211 [binary,7209.1,1295.1] $F. Search stopped by max_proofs option. clauses kept 4307 user CPU time 2.54 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V0),f(V2,V1))),f(V2,f(V1,f(f(V0,V2),V1)))) != V2. % Job 89 ----> UNIT CONFLICT at 2.50 sec ----> 7211 [binary,7209.1,1233.1] $F. Search stopped by max_proofs option. clauses kept 4307 user CPU time 2.51 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V1),f(V2,V0))),f(V2,f(V1,f(V1,f(V2,V0))))) != V2. % Job 90 ----> UNIT CONFLICT at 2.41 sec ----> 7132 [binary,7130.1,1539.1] $F. Search stopped by max_proofs option. clauses kept 4271 user CPU time 2.41 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(f(f(f(V1,V0),V0),f(V1,V2)),V1)) != V2. % Job 91 ----> UNIT CONFLICT at 1.73 sec ----> 8263 [binary,8261.1,858.1] $F. Search stopped by max_proofs option. clauses kept 5016 user CPU time 1.73 (0 hr, 0 min, 1 sec) f(f(f(V0,f(V2,V2)),V2),f(f(f(f(V0,V1),V0),f(V1,V2)),V1)) != V2. % Job 92 ----> UNIT CONFLICT at 2.10 sec ----> 8263 [binary,8261.1,822.1] $F. Search stopped by max_proofs option. clauses kept 5016 user CPU time 2.10 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(f(f(V0,f(V1,V0)),f(V1,V2)),V1)) != V2. % Job 93 ----> UNIT CONFLICT at 2.06 sec ----> 8263 [binary,8261.1,783.1] $F. Search stopped by max_proofs option. clauses kept 5016 user CPU time 2.06 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(f(f(V1,V2),f(f(V1,V0),V0)),V1)) != V2. % Job 94 ----> UNIT CONFLICT at 2.10 sec ----> 8263 [binary,8261.1,858.1] $F. Search stopped by max_proofs option. clauses kept 5016 user CPU time 2.10 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(f(f(V1,V2),f(f(V0,V1),V0)),V1)) != V2. % Job 95 ----> UNIT CONFLICT at 2.05 sec ----> 8263 [binary,8261.1,822.1] $F. Search stopped by max_proofs option. clauses kept 5016 user CPU time 2.06 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(f(f(V1,V2),f(V0,f(V1,V0))),V1)) != V2. % Job 96 ----> UNIT CONFLICT at 2.03 sec ----> 8263 [binary,8261.1,783.1] $F. Search stopped by max_proofs option. clauses kept 5016 user CPU time 2.03 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(f(f(V1,V2),f(V0,f(V0,V1))),V1)) != V2. % Job 97 ----> UNIT CONFLICT at 2.04 sec ----> 8263 [binary,8261.1,781.1] $F. Search stopped by max_proofs option. clauses kept 5016 user CPU time 2.04 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(V1,f(f(f(V0,V1),V0),f(V2,V1)))) != V2. % Job 98 ----> UNIT CONFLICT at 2.09 sec ----> 8251 [binary,8249.1,849.1] $F. Search stopped by max_proofs option. clauses kept 5007 user CPU time 2.09 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(V1,f(f(V0,f(V1,V0)),f(V2,V1)))) != V2. % Job 99 ----> UNIT CONFLICT at 2.01 sec ----> 8251 [binary,8249.1,782.1] $F. Search stopped by max_proofs option. clauses kept 5007 user CPU time 2.01 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(V1,f(f(V0,f(V0,V1)),f(V2,V1)))) != V2. % Job 100 ----> UNIT CONFLICT at 2.03 sec ----> 8251 [binary,8249.1,785.1] $F. Search stopped by max_proofs option. clauses kept 5007 user CPU time 2.03 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(V1,f(f(V2,V1),f(f(V1,V0),V0)))) != V2. % Job 101 ----> UNIT CONFLICT at 2.05 sec ----> 8251 [binary,8249.1,812.1] $F. Search stopped by max_proofs option. clauses kept 5007 user CPU time 2.05 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(V1,f(f(V2,V1),f(f(V0,V1),V0)))) != V2. % Job 102 ----> UNIT CONFLICT at 1.97 sec ----> 8251 [binary,8249.1,849.1] $F. Search stopped by max_proofs option. clauses kept 5007 user CPU time 1.97 (0 hr, 0 min, 1 sec) f(f(f(V0,f(V2,V2)),V2),f(V1,f(f(V1,V2),f(f(V1,V0),V0)))) != V2. % Job 103 ----> UNIT CONFLICT at 2.12 sec ----> 8251 [binary,8249.1,875.1] $F. Search stopped by max_proofs option. clauses kept 5007 user CPU time 2.12 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(V1,f(f(V1,V2),f(f(V0,V1),V0)))) != V2. % Job 104 ----> UNIT CONFLICT at 2.07 sec ----> 8251 [binary,8249.1,902.1] $F. Search stopped by max_proofs option. clauses kept 5007 user CPU time 2.07 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(V1,f(f(V2,V1),f(V0,f(V1,V0))))) != V2. % Job 105 ----> UNIT CONFLICT at 2.09 sec ----> 8251 [binary,8249.1,782.1] $F. Search stopped by max_proofs option. clauses kept 5007 user CPU time 2.09 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(V1,f(f(V2,V1),f(V0,f(V0,V1))))) != V2. % Job 106 ----> UNIT CONFLICT at 2.08 sec ----> 8251 [binary,8249.1,785.1] $F. Search stopped by max_proofs option. clauses kept 5007 user CPU time 2.08 (0 hr, 0 min, 2 sec) f(f(f(f(f(V0,V2),V1),V1),V2),f(f(f(V3,V2),f(V0,V2)),V0)) != V2. % Job 107 ----> UNIT CONFLICT at 4.00 sec ----> 9904 [binary,9902.1,3893.1] $F. Search stopped by max_proofs option. clauses kept 6213 user CPU time 4.00 (0 hr, 0 min, 4 sec) f(f(f(f(f(V0,V2),V1),V1),V2),f(f(f(V2,V3),f(V0,V2)),V0)) != V2. % Job 108 ----> UNIT CONFLICT at 3.00 sec ----> 8288 [binary,8286.1,2957.1] $F. Search stopped by max_proofs option. clauses kept 5107 user CPU time 3.01 (0 hr, 0 min, 3 sec) f(f(f(f(f(V0,V2),V1),V1),V2),f(f(f(V0,V2),f(V3,V2)),V0)) != V2. % Job 109 ----> UNIT CONFLICT at 3.35 sec ----> 8885 [binary,8883.1,3434.1] $F. Search stopped by max_proofs option. clauses kept 5445 user CPU time 3.35 (0 hr, 0 min, 3 sec) f(f(f(f(f(V0,V2),V1),V1),V2),f(V0,f(f(V3,V2),f(V2,V0)))) != V2. % Job 110 ----> UNIT CONFLICT at 2.93 sec ----> 7998 [binary,7996.1,2960.1] $F. Search stopped by max_proofs option. clauses kept 4827 user CPU time 2.93 (0 hr, 0 min, 2 sec) f(f(f(f(f(V0,V2),V1),V1),V2),f(V0,f(f(V2,V3),f(V2,V0)))) != V2. % Job 111 ----> UNIT CONFLICT at 2.46 sec ----> 7126 [binary,7124.1,1776.1] $F. Search stopped by max_proofs option. clauses kept 4260 user CPU time 2.46 (0 hr, 0 min, 2 sec) f(f(f(f(f(V0,V2),V1),V1),V2),f(V0,f(f(V2,V0),f(V2,V3)))) != V2. % Job 112 ----> UNIT CONFLICT at 2.84 sec ----> 7961 [binary,7959.1,2908.1] $F. Search stopped by max_proofs option. clauses kept 4804 user CPU time 2.84 (0 hr, 0 min, 2 sec) f(f(f(f(f(V0,V2),V1),V1),V2),f(V0,f(f(V0,V2),f(V2,V3)))) != V2. % Job 113 ----> UNIT CONFLICT at 2.66 sec ----> 7769 [binary,7767.1,2875.1] $F. Search stopped by max_proofs option. clauses kept 4667 user CPU time 2.66 (0 hr, 0 min, 2 sec) f(f(f(f(f(V0,V2),V1),V1),V2),f(V0,f(f(V2,V2),f(V2,V3)))) != V2. % Job 114 ----> UNIT CONFLICT at 2.49 sec ----> 7793 [binary,7791.1,3583.1] $F. Search stopped by max_proofs option. clauses kept 4577 user CPU time 2.50 (0 hr, 0 min, 2 sec) f(f(f(f(V0,f(V2,V1)),V0),V2),f(f(f(V3,V2),f(V1,V2)),V1)) != V2. % Job 115 ----> UNIT CONFLICT at 3.96 sec ----> 9904 [binary,9902.1,3981.1] $F. Search stopped by max_proofs option. clauses kept 6213 user CPU time 3.96 (0 hr, 0 min, 3 sec) f(f(f(f(V0,f(V2,V1)),V0),V2),f(f(f(V2,V3),f(V1,V2)),V1)) != V2. % Job 116 ----> UNIT CONFLICT at 2.95 sec ----> 8288 [binary,8286.1,2701.1] $F. Search stopped by max_proofs option. clauses kept 5107 user CPU time 2.95 (0 hr, 0 min, 2 sec) f(f(f(f(V0,f(V2,V1)),V0),V2),f(f(f(V1,V2),f(V3,V2)),V1)) != V2. % Job 117 ----> UNIT CONFLICT at 3.36 sec ----> 8885 [binary,8883.1,3906.1] $F. Search stopped by max_proofs option. clauses kept 5445 user CPU time 3.36 (0 hr, 0 min, 3 sec) f(f(f(f(V0,f(V1,V2)),V0),V2),f(f(f(V3,V2),f(V1,V2)),V1)) != V2. % Job 118 ----> UNIT CONFLICT at 4.00 sec ----> 9904 [binary,9902.1,4236.1] $F. Search stopped by max_proofs option. clauses kept 6213 user CPU time 4.01 (0 hr, 0 min, 4 sec) f(f(f(f(V0,f(V1,V2)),V0),V2),f(f(f(V2,V3),f(V1,V2)),V1)) != V2. % Job 119 ----> UNIT CONFLICT at 3.01 sec ----> 8288 [binary,8286.1,2788.1] $F. Search stopped by max_proofs option. clauses kept 5107 user CPU time 3.01 (0 hr, 0 min, 3 sec) f(f(f(f(V0,f(V1,V2)),V0),V2),f(f(f(V1,V2),f(V3,V2)),V1)) != V2. % Job 120 ----> UNIT CONFLICT at 3.38 sec ----> 8885 [binary,8883.1,3652.1] $F. Search stopped by max_proofs option. clauses kept 5445 user CPU time 3.38 (0 hr, 0 min, 3 sec) f(f(f(f(V0,f(V2,V1)),V0),V2),f(V1,f(f(V3,V2),f(V2,V1)))) != V2. % Job 121 ----> UNIT CONFLICT at 2.85 sec ----> 7998 [binary,7996.1,3042.1] $F. Search stopped by max_proofs option. clauses kept 4827 user CPU time 2.86 (0 hr, 0 min, 2 sec) f(f(f(f(V0,f(V2,V1)),V0),V2),f(V1,f(f(V2,V3),f(V2,V1)))) != V2. % Job 122 ----> UNIT CONFLICT at 2.45 sec ----> 7126 [binary,7124.1,2277.1] $F. Search stopped by max_proofs option. clauses kept 4260 user CPU time 2.45 (0 hr, 0 min, 2 sec) f(f(f(f(V0,f(V2,V1)),V0),V2),f(V1,f(f(V2,V1),f(V2,V3)))) != V2. % Job 123 ----> UNIT CONFLICT at 2.93 sec ----> 7961 [binary,7959.1,2988.1] $F. Search stopped by max_proofs option. clauses kept 4804 user CPU time 2.93 (0 hr, 0 min, 2 sec) f(f(f(f(V0,f(V2,V1)),V0),V2),f(V1,f(f(V1,V2),f(V2,V3)))) != V2. % Job 124 ----> UNIT CONFLICT at 2.66 sec ----> 7769 [binary,7767.1,3170.1] $F. Search stopped by max_proofs option. clauses kept 4667 user CPU time 2.66 (0 hr, 0 min, 2 sec) f(f(f(f(V0,f(V1,V2)),V0),V2),f(V1,f(f(V3,V2),f(V2,V1)))) != V2. % Job 125 ----> UNIT CONFLICT at 2.89 sec ----> 7998 [binary,7996.1,3140.1] $F. Search stopped by max_proofs option. clauses kept 4827 user CPU time 2.89 (0 hr, 0 min, 2 sec) f(f(f(f(V0,f(V1,V2)),V0),V2),f(V1,f(f(V2,V3),f(V2,V1)))) != V2. % Job 126 ----> UNIT CONFLICT at 2.45 sec ----> 7126 [binary,7124.1,2018.1] $F. Search stopped by max_proofs option. clauses kept 4260 user CPU time 2.45 (0 hr, 0 min, 2 sec) f(f(f(f(V0,f(V1,V2)),V0),V2),f(V1,f(f(V2,V1),f(V2,V3)))) != V2. % Job 127 ----> UNIT CONFLICT at 2.92 sec ----> 7961 [binary,7959.1,3086.1] $F. Search stopped by max_proofs option. clauses kept 4804 user CPU time 2.92 (0 hr, 0 min, 2 sec) f(f(f(f(V0,f(V1,V2)),V0),V2),f(V1,f(f(V1,V2),f(V2,V3)))) != V2. % Job 128 ----> UNIT CONFLICT at 2.78 sec ----> 7769 [binary,7767.1,3074.1] $F. Search stopped by max_proofs option. clauses kept 4667 user CPU time 2.79 (0 hr, 0 min, 2 sec) f(f(f(f(V0,f(V2,V1)),V0),V2),f(V1,f(f(V2,V2),f(V2,V3)))) != V2. % Job 129 ----> UNIT CONFLICT at 2.56 sec ----> 7793 [binary,7791.1,3673.1] $F. Search stopped by max_proofs option. clauses kept 4577 user CPU time 2.56 (0 hr, 0 min, 2 sec) f(f(f(f(V0,f(V1,V2)),V0),V2),f(V1,f(f(V2,V2),f(V2,V3)))) != V2. % Job 130 ----> UNIT CONFLICT at 2.58 sec ----> 7793 [binary,7791.1,3713.1] $F. Search stopped by max_proofs option. clauses kept 4577 user CPU time 2.58 (0 hr, 0 min, 2 sec) f(f(f(f(V0,V2),f(V2,V1)),V1),f(V2,f(f(f(V2,V1),V3),V3))) != V2. % Job 131 ----> UNIT CONFLICT at 3.46 sec ----> 9255 [binary,9253.1,2979.1] $F. Search stopped by max_proofs option. clauses kept 5692 user CPU time 3.46 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V2,V1)),V1),f(V2,f(f(f(V1,V2),V3),V3))) != V2. % Job 132 ----> UNIT CONFLICT at 3.61 sec ----> 9255 [binary,9253.1,3285.1] $F. Search stopped by max_proofs option. clauses kept 5692 user CPU time 3.61 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V2,V1)),V0),f(V2,f(f(f(V2,V0),V3),V3))) != V2. % Job 133 ----> UNIT CONFLICT at 3.10 sec ----> 8444 [binary,8442.1,2685.1] $F. Search stopped by max_proofs option. clauses kept 5105 user CPU time 3.10 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V2,V1)),V0),f(V2,f(f(f(V0,V2),V3),V3))) != V2. % Job 134 ----> UNIT CONFLICT at 3.12 sec ----> 8444 [binary,8442.1,2810.1] $F. Search stopped by max_proofs option. clauses kept 5105 user CPU time 3.13 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V1,V2)),V1),f(V2,f(f(f(V2,V1),V3),V3))) != V2. % Job 135 ----> UNIT CONFLICT at 4.14 sec ----> 9904 [binary,9902.1,3723.1] $F. Search stopped by max_proofs option. clauses kept 6213 user CPU time 4.14 (0 hr, 0 min, 4 sec) f(f(f(f(V0,V2),f(V1,V2)),V1),f(V2,f(f(f(V1,V2),V3),V3))) != V2. % Job 136 ----> UNIT CONFLICT at 3.99 sec ----> 9904 [binary,9902.1,3855.1] $F. Search stopped by max_proofs option. clauses kept 6213 user CPU time 3.99 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V1,V2)),V0),f(V2,f(f(f(V2,V0),V3),V3))) != V2. % Job 137 ----> UNIT CONFLICT at 3.20 sec ----> 8886 [binary,8884.1,3548.1] $F. Search stopped by max_proofs option. clauses kept 5446 user CPU time 3.20 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V1,V2)),V0),f(V2,f(f(f(V0,V2),V3),V3))) != V2. % Job 138 ----> UNIT CONFLICT at 3.42 sec ----> 8886 [binary,8884.1,3456.1] $F. Search stopped by max_proofs option. clauses kept 5446 user CPU time 3.42 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V2,V2)),V1),f(V2,f(f(f(V2,V1),V3),V3))) != V2. % Job 139 ----> UNIT CONFLICT at 2.71 sec ----> 7795 [binary,7793.1,1456.1] $F. Search stopped by max_proofs option. clauses kept 4744 user CPU time 2.71 (0 hr, 0 min, 2 sec) f(f(f(f(V0,V2),f(V2,V2)),V1),f(V2,f(f(f(V1,V2),V3),V3))) != V2. % Job 140 ----> UNIT CONFLICT at 2.53 sec ----> 7795 [binary,7793.1,1425.1] $F. Search stopped by max_proofs option. clauses kept 4744 user CPU time 2.53 (0 hr, 0 min, 2 sec) f(f(f(f(V0,V2),f(V2,V1)),V1),f(V2,f(f(V3,f(V2,V1)),V3))) != V2. % Job 141 ----> UNIT CONFLICT at 3.60 sec ----> 9255 [binary,9253.1,3326.1] $F. Search stopped by max_proofs option. clauses kept 5692 user CPU time 3.60 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V2,V1)),V1),f(V2,f(f(V3,f(V1,V2)),V3))) != V2. % Job 142 ----> UNIT CONFLICT at 3.59 sec ----> 9255 [binary,9253.1,3462.1] $F. Search stopped by max_proofs option. clauses kept 5692 user CPU time 3.59 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V2,V1)),V0),f(V2,f(f(V3,f(V2,V0)),V3))) != V2. % Job 143 ----> UNIT CONFLICT at 3.03 sec ----> 8444 [binary,8442.1,2250.1] $F. Search stopped by max_proofs option. clauses kept 5105 user CPU time 3.04 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V2,V1)),V0),f(V2,f(f(V3,f(V0,V2)),V3))) != V2. % Job 144 ----> UNIT CONFLICT at 3.13 sec ----> 8444 [binary,8442.1,2657.1] $F. Search stopped by max_proofs option. clauses kept 5105 user CPU time 3.14 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V1,V2)),V1),f(V2,f(f(V3,f(V2,V1)),V3))) != V2. % Job 145 ----> UNIT CONFLICT at 4.08 sec ----> 9904 [binary,9902.1,3803.1] $F. Search stopped by max_proofs option. clauses kept 6213 user CPU time 4.08 (0 hr, 0 min, 4 sec) f(f(f(f(V0,V2),f(V1,V2)),V1),f(V2,f(f(V3,f(V1,V2)),V3))) != V2. % Job 146 ----> UNIT CONFLICT at 4.02 sec ----> 9904 [binary,9902.1,4149.1] $F. Search stopped by max_proofs option. clauses kept 6213 user CPU time 4.02 (0 hr, 0 min, 4 sec) f(f(f(f(V0,V2),f(V1,V2)),V0),f(V2,f(f(V3,f(V2,V0)),V3))) != V2. % Job 147 ----> UNIT CONFLICT at 3.32 sec ----> 8886 [binary,8884.1,3797.1] $F. Search stopped by max_proofs option. clauses kept 5446 user CPU time 3.32 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V1,V2)),V0),f(V2,f(f(V3,f(V0,V2)),V3))) != V2. % Job 148 ----> UNIT CONFLICT at 3.45 sec ----> 8886 [binary,8884.1,3531.1] $F. Search stopped by max_proofs option. clauses kept 5446 user CPU time 3.45 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V2,V2)),V1),f(V2,f(f(V3,f(V2,V1)),V3))) != V2. % Job 149 ----> UNIT CONFLICT at 2.63 sec ----> 7795 [binary,7793.1,1041.1] $F. Search stopped by max_proofs option. clauses kept 4744 user CPU time 2.64 (0 hr, 0 min, 2 sec) f(f(f(f(V0,V2),f(V2,V2)),V1),f(V2,f(f(V3,f(V1,V2)),V3))) != V2. % Job 150 ----> UNIT CONFLICT at 2.61 sec ----> 7795 [binary,7793.1,1038.1] $F. Search stopped by max_proofs option. clauses kept 4744 user CPU time 2.61 (0 hr, 0 min, 2 sec) f(f(f(f(V0,V2),f(V2,V1)),V1),f(V2,f(V3,f(f(V2,V1),V3)))) != V2. % Job 151 ----> UNIT CONFLICT at 3.49 sec ----> 9255 [binary,9253.1,2977.1] $F. Search stopped by max_proofs option. clauses kept 5692 user CPU time 3.49 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V2,V1)),V1),f(V2,f(V3,f(f(V1,V2),V3)))) != V2. % Job 152 ----> UNIT CONFLICT at 3.48 sec ----> 9255 [binary,9253.1,3283.1] $F. Search stopped by max_proofs option. clauses kept 5692 user CPU time 3.48 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V2,V1)),V0),f(V2,f(V3,f(f(V2,V0),V3)))) != V2. % Job 153 ----> UNIT CONFLICT at 3.18 sec ----> 8444 [binary,8442.1,2248.1] $F. Search stopped by max_proofs option. clauses kept 5105 user CPU time 3.19 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V2,V1)),V0),f(V2,f(V3,f(f(V0,V2),V3)))) != V2. % Job 154 ----> UNIT CONFLICT at 3.17 sec ----> 8444 [binary,8442.1,2411.1] $F. Search stopped by max_proofs option. clauses kept 5105 user CPU time 3.18 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V1,V2)),V1),f(V2,f(V3,f(f(V2,V1),V3)))) != V2. % Job 155 ----> UNIT CONFLICT at 4.07 sec ----> 9904 [binary,9902.1,3725.1] $F. Search stopped by max_proofs option. clauses kept 6213 user CPU time 4.07 (0 hr, 0 min, 4 sec) f(f(f(f(V0,V2),f(V1,V2)),V1),f(V2,f(V3,f(f(V1,V2),V3)))) != V2. % Job 156 ----> UNIT CONFLICT at 3.94 sec ----> 9904 [binary,9902.1,3857.1] $F. Search stopped by max_proofs option. clauses kept 6213 user CPU time 3.95 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V1,V2)),V0),f(V2,f(V3,f(f(V2,V0),V3)))) != V2. % Job 157 ----> UNIT CONFLICT at 3.35 sec ----> 8886 [binary,8884.1,3550.1] $F. Search stopped by max_proofs option. clauses kept 5446 user CPU time 3.35 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V1,V2)),V0),f(V2,f(V3,f(f(V0,V2),V3)))) != V2. % Job 158 ----> UNIT CONFLICT at 3.36 sec ----> 8886 [binary,8884.1,3458.1] $F. Search stopped by max_proofs option. clauses kept 5446 user CPU time 3.36 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V2,V2)),V1),f(V2,f(V3,f(f(V2,V1),V3)))) != V2. % Job 159 ----> UNIT CONFLICT at 2.73 sec ----> 7795 [binary,7793.1,1004.1] $F. Search stopped by max_proofs option. clauses kept 4744 user CPU time 2.73 (0 hr, 0 min, 2 sec) f(f(f(f(V0,V2),f(V2,V2)),V1),f(V2,f(V3,f(f(V1,V2),V3)))) != V2. % Job 160 ----> UNIT CONFLICT at 2.55 sec ----> 7795 [binary,7793.1,1000.1] $F. Search stopped by max_proofs option. clauses kept 4744 user CPU time 2.55 (0 hr, 0 min, 2 sec) f(f(f(f(V0,V2),f(V2,V1)),V1),f(V2,f(V3,f(V3,f(V2,V1))))) != V2. % Job 161 ----> UNIT CONFLICT at 3.61 sec ----> 9255 [binary,9253.1,3324.1] $F. Search stopped by max_proofs option. clauses kept 5692 user CPU time 3.61 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V2,V1)),V0),f(V2,f(V3,f(V3,f(V2,V0))))) != V2. % Job 162 ----> UNIT CONFLICT at 3.07 sec ----> 8444 [binary,8442.1,2152.1] $F. Search stopped by max_proofs option. clauses kept 5105 user CPU time 3.07 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V1,V2)),V1),f(V2,f(V3,f(V3,f(V2,V1))))) != V2. % Job 163 ----> UNIT CONFLICT at 4.00 sec ----> 9904 [binary,9902.1,3805.1] $F. Search stopped by max_proofs option. clauses kept 6213 user CPU time 4.01 (0 hr, 0 min, 4 sec) f(f(f(f(V0,V2),f(V1,V2)),V0),f(V2,f(V3,f(V3,f(V2,V0))))) != V2. % Job 164 ----> UNIT CONFLICT at 3.34 sec ----> 8886 [binary,8884.1,3799.1] $F. Search stopped by max_proofs option. clauses kept 5446 user CPU time 3.34 (0 hr, 0 min, 3 sec) f(f(f(f(V0,V2),f(V2,V2)),V1),f(V2,f(V3,f(V3,f(V2,V1))))) != V2. % Job 165 ----> UNIT CONFLICT at 2.66 sec ----> 7795 [binary,7793.1,906.1] $F. Search stopped by max_proofs option. clauses kept 4744 user CPU time 2.67 (0 hr, 0 min, 2 sec) f(f(f(V0,f(f(V2,V1),V0)),V2),f(f(f(V3,V2),f(V1,V2)),V1)) != V2. % Job 166 ----> UNIT CONFLICT at 3.92 sec ----> 9904 [binary,9902.1,3736.1] $F. Search stopped by max_proofs option. clauses kept 6213 user CPU time 3.92 (0 hr, 0 min, 3 sec) f(f(f(V0,f(f(V2,V1),V0)),V2),f(f(f(V2,V3),f(V1,V2)),V1)) != V2. % Job 167 ----> UNIT CONFLICT at 2.95 sec ----> 8288 [binary,8286.1,2677.1] $F. Search stopped by max_proofs option. clauses kept 5107 user CPU time 2.95 (0 hr, 0 min, 2 sec) f(f(f(V0,f(f(V2,V1),V0)),V2),f(f(f(V1,V2),f(V3,V2)),V1)) != V2. % Job 168 ----> UNIT CONFLICT at 3.41 sec ----> 8885 [binary,8883.1,3563.1] $F. Search stopped by max_proofs option. clauses kept 5445 user CPU time 3.41 (0 hr, 0 min, 3 sec) f(f(f(V0,f(f(V1,V2),V0)),V2),f(f(f(V3,V2),f(V1,V2)),V1)) != V2. % Job 169 ----> UNIT CONFLICT at 4.20 sec ----> 9904 [binary,9902.1,3895.1] $F. Search stopped by max_proofs option. clauses kept 6213 user CPU time 4.20 (0 hr, 0 min, 4 sec) f(f(f(V0,f(f(V1,V2),V0)),V2),f(f(f(V2,V3),f(V1,V2)),V1)) != V2. % Job 170 ----> UNIT CONFLICT at 3.04 sec ----> 8288 [binary,8286.1,2772.1] $F. Search stopped by max_proofs option. clauses kept 5107 user CPU time 3.04 (0 hr, 0 min, 3 sec) f(f(f(V0,f(f(V1,V2),V0)),V2),f(f(f(V1,V2),f(V3,V2)),V1)) != V2. % Job 171 ----> UNIT CONFLICT at 3.24 sec ----> 8885 [binary,8883.1,3436.1] $F. Search stopped by max_proofs option. clauses kept 5445 user CPU time 3.24 (0 hr, 0 min, 3 sec) f(f(f(V0,f(f(V2,V1),V0)),V2),f(V1,f(f(V3,V2),f(V2,V1)))) != V2. % Job 172 ----> UNIT CONFLICT at 2.89 sec ----> 7998 [binary,7996.1,2761.1] $F. Search stopped by max_proofs option. clauses kept 4827 user CPU time 2.89 (0 hr, 0 min, 2 sec) f(f(f(V0,f(f(V2,V1),V0)),V2),f(V1,f(f(V2,V3),f(V2,V1)))) != V2. % Job 173 ----> UNIT CONFLICT at 2.38 sec ----> 7126 [binary,7124.1,1683.1] $F. Search stopped by max_proofs option. clauses kept 4260 user CPU time 2.38 (0 hr, 0 min, 2 sec) f(f(f(V0,f(f(V2,V1),V0)),V2),f(V1,f(f(V2,V1),f(V2,V3)))) != V2. % Job 174 ----> UNIT CONFLICT at 2.99 sec ----> 7961 [binary,7959.1,2707.1] $F. Search stopped by max_proofs option. clauses kept 4804 user CPU time 2.99 (0 hr, 0 min, 2 sec) f(f(f(V0,f(f(V2,V1),V0)),V2),f(V1,f(f(V1,V2),f(V2,V3)))) != V2. % Job 175 ----> UNIT CONFLICT at 2.69 sec ----> 7769 [binary,7767.1,2848.1] $F. Search stopped by max_proofs option. clauses kept 4667 user CPU time 2.69 (0 hr, 0 min, 2 sec) f(f(f(V0,f(f(V1,V2),V0)),V2),f(V1,f(f(V3,V2),f(V2,V1)))) != V2. % Job 176 ----> UNIT CONFLICT at 2.87 sec ----> 7998 [binary,7996.1,2817.1] $F. Search stopped by max_proofs option. clauses kept 4827 user CPU time 2.87 (0 hr, 0 min, 2 sec) f(f(f(V0,f(f(V1,V2),V0)),V2),f(V1,f(f(V2,V3),f(V2,V1)))) != V2. % Job 177 ----> UNIT CONFLICT at 2.41 sec ----> 7126 [binary,7124.1,1548.1] $F. Search stopped by max_proofs option. clauses kept 4260 user CPU time 2.41 (0 hr, 0 min, 2 sec) f(f(f(V0,f(f(V1,V2),V0)),V2),f(V1,f(f(V2,V1),f(V2,V3)))) != V2. % Job 178 ----> UNIT CONFLICT at 2.91 sec ----> 7961 [binary,7959.1,2761.1] $F. Search stopped by max_proofs option. clauses kept 4804 user CPU time 2.91 (0 hr, 0 min, 2 sec) f(f(f(V0,f(f(V1,V2),V0)),V2),f(V1,f(f(V1,V2),f(V2,V3)))) != V2. % Job 179 ----> UNIT CONFLICT at 2.77 sec ----> 7769 [binary,7767.1,2792.1] $F. Search stopped by max_proofs option. clauses kept 4667 user CPU time 2.78 (0 hr, 0 min, 2 sec) f(f(f(V0,f(f(V2,V1),V0)),V2),f(V1,f(f(V2,V2),f(V2,V3)))) != V2. % Job 180 ----> UNIT CONFLICT at 2.51 sec ----> 7793 [binary,7791.1,3687.1] $F. Search stopped by max_proofs option. clauses kept 4577 user CPU time 2.51 (0 hr, 0 min, 2 sec) f(f(f(V0,f(f(V1,V2),V0)),V2),f(V1,f(f(V2,V2),f(V2,V3)))) != V2. % Job 181 ----> UNIT CONFLICT at 2.45 sec ----> 7793 [binary,7791.1,3707.1] $F. Search stopped by max_proofs option. clauses kept 4577 user CPU time 2.45 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V0,f(V2,V1))),V2),f(f(f(V3,V2),f(V1,V2)),V1)) != V2. % Job 182 ----> UNIT CONFLICT at 4.08 sec ----> 9904 [binary,9902.1,3983.1] $F. Search stopped by max_proofs option. clauses kept 6213 user CPU time 4.08 (0 hr, 0 min, 4 sec) f(f(f(V0,f(V0,f(V2,V1))),V2),f(f(f(V2,V3),f(V1,V2)),V1)) != V2. % Job 183 ----> UNIT CONFLICT at 3.14 sec ----> 8288 [binary,8286.1,2488.1] $F. Search stopped by max_proofs option. clauses kept 5107 user CPU time 3.15 (0 hr, 0 min, 3 sec) f(f(f(V0,f(V0,f(V2,V1))),V2),f(f(f(V1,V2),f(V3,V2)),V1)) != V2. % Job 184 ----> UNIT CONFLICT at 3.34 sec ----> 8885 [binary,8883.1,3908.1] $F. Search stopped by max_proofs option. clauses kept 5445 user CPU time 3.34 (0 hr, 0 min, 3 sec) f(f(f(V0,f(V0,f(V1,V2))),V2),f(f(f(V3,V2),f(V1,V2)),V1)) != V2. % Job 185 ----> UNIT CONFLICT at 4.02 sec ----> 9904 [binary,9902.1,4238.1] $F. Search stopped by max_proofs option. clauses kept 6213 user CPU time 4.03 (0 hr, 0 min, 4 sec) f(f(f(V0,f(V0,f(V1,V2))),V2),f(f(f(V2,V3),f(V1,V2)),V1)) != V2. % Job 186 ----> UNIT CONFLICT at 3.15 sec ----> 8288 [binary,8286.1,2605.1] $F. Search stopped by max_proofs option. clauses kept 5107 user CPU time 3.15 (0 hr, 0 min, 3 sec) f(f(f(V0,f(V0,f(V1,V2))),V2),f(f(f(V1,V2),f(V3,V2)),V1)) != V2. % Job 187 ----> UNIT CONFLICT at 3.34 sec ----> 8885 [binary,8883.1,3654.1] $F. Search stopped by max_proofs option. clauses kept 5445 user CPU time 3.34 (0 hr, 0 min, 3 sec) f(f(f(V0,f(V0,f(V2,V1))),V2),f(V1,f(f(V3,V2),f(V2,V1)))) != V2. % Job 188 ----> UNIT CONFLICT at 2.92 sec ----> 7998 [binary,7996.1,2841.1] $F. Search stopped by max_proofs option. clauses kept 4827 user CPU time 2.92 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V0,f(V2,V1))),V2),f(V1,f(f(V2,V3),f(V2,V1)))) != V2. % Job 189 ----> UNIT CONFLICT at 2.37 sec ----> 7126 [binary,7124.1,1912.1] $F. Search stopped by max_proofs option. clauses kept 4260 user CPU time 2.38 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V0,f(V2,V1))),V2),f(V1,f(f(V2,V1),f(V2,V3)))) != V2. % Job 190 ----> UNIT CONFLICT at 2.88 sec ----> 7961 [binary,7959.1,2785.1] $F. Search stopped by max_proofs option. clauses kept 4804 user CPU time 2.88 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V0,f(V2,V1))),V2),f(V1,f(f(V1,V2),f(V2,V3)))) != V2. % Job 191 ----> UNIT CONFLICT at 2.27 sec ----> 7769 [binary,7767.1,2967.1] $F. Search stopped by max_proofs option. clauses kept 4667 user CPU time 2.28 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V0,f(V1,V2))),V2),f(V1,f(f(V3,V2),f(V2,V1)))) != V2. % Job 192 ----> UNIT CONFLICT at 2.98 sec ----> 7998 [binary,7996.1,2935.1] $F. Search stopped by max_proofs option. clauses kept 4827 user CPU time 2.99 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V0,f(V1,V2))),V2),f(V1,f(f(V2,V3),f(V2,V1)))) != V2. % Job 193 ----> UNIT CONFLICT at 2.45 sec ----> 7126 [binary,7124.1,1773.1] $F. Search stopped by max_proofs option. clauses kept 4260 user CPU time 2.45 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V0,f(V1,V2))),V2),f(V1,f(f(V2,V1),f(V2,V3)))) != V2. % Job 194 ----> UNIT CONFLICT at 2.88 sec ----> 7961 [binary,7959.1,2883.1] $F. Search stopped by max_proofs option. clauses kept 4804 user CPU time 2.88 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V0,f(V1,V2))),V2),f(V1,f(f(V1,V2),f(V2,V3)))) != V2. % Job 195 ----> UNIT CONFLICT at 2.74 sec ----> 7769 [binary,7767.1,2872.1] $F. Search stopped by max_proofs option. clauses kept 4667 user CPU time 2.74 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V0,f(V2,V1))),V2),f(V1,f(f(V2,V2),f(V2,V3)))) != V2. % Job 196 ----> UNIT CONFLICT at 2.48 sec ----> 7793 [binary,7791.1,3747.1] $F. Search stopped by max_proofs option. clauses kept 4577 user CPU time 2.49 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V0,f(V1,V2))),V2),f(V1,f(f(V2,V2),f(V2,V3)))) != V2. % Job 197 ----> UNIT CONFLICT at 2.51 sec ----> 7793 [binary,7791.1,3767.1] $F. Search stopped by max_proofs option. clauses kept 4577 user CPU time 2.51 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V1),f(V2,V0))),f(V2,f(f(f(V2,V0),V3),V3))) != V2. % Job 198 ----> UNIT CONFLICT at 2.48 sec ----> 7132 [binary,7130.1,1489.1] $F. Search stopped by max_proofs option. clauses kept 4271 user CPU time 2.48 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V1),f(V2,V0))),f(V2,f(f(f(V0,V2),V3),V3))) != V2. % Job 199 ----> UNIT CONFLICT at 2.29 sec ----> 7132 [binary,7130.1,1257.1] $F. Search stopped by max_proofs option. clauses kept 4271 user CPU time 2.29 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V0),f(V2,V1))),f(V2,f(f(f(V2,V0),V3),V3))) != V2. % Job 200 ----> UNIT CONFLICT at 2.44 sec ----> 7211 [binary,7209.1,1525.1] $F. Search stopped by max_proofs option. clauses kept 4307 user CPU time 2.44 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V0),f(V2,V1))),f(V2,f(f(f(V0,V2),V3),V3))) != V2. % Job 201 ----> UNIT CONFLICT at 2.50 sec ----> 7211 [binary,7209.1,1374.1] $F. Search stopped by max_proofs option. clauses kept 4307 user CPU time 2.50 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V0),f(V1,V2))),f(V2,f(f(f(V2,V0),V3),V3))) != V2. % Job 202 ----> UNIT CONFLICT at 3.38 sec ----> 9063 [binary,9061.1,3600.1] $F. Search stopped by max_proofs option. clauses kept 5581 user CPU time 3.38 (0 hr, 0 min, 3 sec) f(f(V0,f(f(V2,V0),f(V1,V2))),f(V2,f(f(f(V0,V2),V3),V3))) != V2. % Job 203 ----> UNIT CONFLICT at 3.57 sec ----> 9063 [binary,9061.1,3678.1] $F. Search stopped by max_proofs option. clauses kept 5581 user CPU time 3.57 (0 hr, 0 min, 3 sec) f(f(V0,f(f(V2,V1),f(V2,V0))),f(V2,f(f(V3,f(V2,V0)),V3))) != V2. % Job 204 ----> UNIT CONFLICT at 2.43 sec ----> 7132 [binary,7130.1,2019.1] $F. Search stopped by max_proofs option. clauses kept 4271 user CPU time 2.43 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V1),f(V2,V0))),f(V2,f(f(V3,f(V0,V2)),V3))) != V2. % Job 205 ----> UNIT CONFLICT at 2.45 sec ----> 7132 [binary,7130.1,1590.1] $F. Search stopped by max_proofs option. clauses kept 4271 user CPU time 2.45 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V0),f(V2,V1))),f(V2,f(f(V3,f(V2,V0)),V3))) != V2. % Job 206 ----> UNIT CONFLICT at 2.54 sec ----> 7211 [binary,7209.1,1845.1] $F. Search stopped by max_proofs option. clauses kept 4307 user CPU time 2.54 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V0),f(V2,V1))),f(V2,f(f(V3,f(V0,V2)),V3))) != V2. % Job 207 ----> UNIT CONFLICT at 2.49 sec ----> 7211 [binary,7209.1,1626.1] $F. Search stopped by max_proofs option. clauses kept 4307 user CPU time 2.49 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V0),f(V1,V2))),f(V2,f(f(V3,f(V2,V0)),V3))) != V2. % Job 208 ----> UNIT CONFLICT at 3.62 sec ----> 9063 [binary,9061.1,3649.1] $F. Search stopped by max_proofs option. clauses kept 5581 user CPU time 3.62 (0 hr, 0 min, 3 sec) f(f(V0,f(f(V2,V0),f(V1,V2))),f(V2,f(f(V3,f(V0,V2)),V3))) != V2. % Job 209 ----> UNIT CONFLICT at 3.51 sec ----> 9063 [binary,9061.1,3991.1] $F. Search stopped by max_proofs option. clauses kept 5581 user CPU time 3.51 (0 hr, 0 min, 3 sec) f(f(V0,f(f(V2,V1),f(V2,V0))),f(V2,f(V3,f(f(V2,V0),V3)))) != V2. % Job 210 ----> UNIT CONFLICT at 2.35 sec ----> 7132 [binary,7130.1,1223.1] $F. Search stopped by max_proofs option. clauses kept 4271 user CPU time 2.35 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V1),f(V2,V0))),f(V2,f(V3,f(f(V0,V2),V3)))) != V2. % Job 211 ----> UNIT CONFLICT at 2.36 sec ----> 7132 [binary,7130.1,1039.1] $F. Search stopped by max_proofs option. clauses kept 4271 user CPU time 2.37 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V0),f(V2,V1))),f(V2,f(V3,f(f(V2,V0),V3)))) != V2. % Job 212 ----> UNIT CONFLICT at 2.53 sec ----> 7211 [binary,7209.1,1295.1] $F. Search stopped by max_proofs option. clauses kept 4307 user CPU time 2.53 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V0),f(V2,V1))),f(V2,f(V3,f(f(V0,V2),V3)))) != V2. % Job 213 ----> UNIT CONFLICT at 2.58 sec ----> 7211 [binary,7209.1,1233.1] $F. Search stopped by max_proofs option. clauses kept 4307 user CPU time 2.59 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V0),f(V1,V2))),f(V2,f(V3,f(f(V2,V0),V3)))) != V2. % Job 214 ----> UNIT CONFLICT at 3.56 sec ----> 9063 [binary,9061.1,3602.1] $F. Search stopped by max_proofs option. clauses kept 5581 user CPU time 3.56 (0 hr, 0 min, 3 sec) f(f(V0,f(f(V2,V0),f(V1,V2))),f(V2,f(V3,f(f(V0,V2),V3)))) != V2. % Job 215 ----> UNIT CONFLICT at 3.45 sec ----> 9063 [binary,9061.1,3680.1] $F. Search stopped by max_proofs option. clauses kept 5581 user CPU time 3.45 (0 hr, 0 min, 3 sec) f(f(V0,f(f(V2,V1),f(V2,V0))),f(V2,f(V3,f(V3,f(V2,V0))))) != V2. % Job 216 ----> UNIT CONFLICT at 2.50 sec ----> 7132 [binary,7130.1,1539.1] $F. Search stopped by max_proofs option. clauses kept 4271 user CPU time 2.51 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V0),f(V2,V1))),f(V2,f(V3,f(V3,f(V2,V0))))) != V2. % Job 217 ----> UNIT CONFLICT at 2.54 sec ----> 7211 [binary,7209.1,1522.1] $F. Search stopped by max_proofs option. clauses kept 4307 user CPU time 2.54 (0 hr, 0 min, 2 sec) f(f(V0,f(f(V2,V0),f(V1,V2))),f(V2,f(V3,f(V3,f(V2,V0))))) != V2. % Job 218 ----> UNIT CONFLICT at 3.60 sec ----> 9063 [binary,9061.1,3651.1] $F. Search stopped by max_proofs option. clauses kept 5581 user CPU time 3.60 (0 hr, 0 min, 3 sec) f(f(f(V0,f(V2,V2)),V2),f(f(f(f(V1,V3),V3),f(V1,V2)),V1)) != V2. % Job 219 ----> UNIT CONFLICT at 2.09 sec ----> 8263 [binary,8261.1,858.1] $F. Search stopped by max_proofs option. clauses kept 5016 user CPU time 2.09 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(f(f(f(V1,V3),V1),f(V3,V2)),V3)) != V2. % Job 220 ----> UNIT CONFLICT at 2.03 sec ----> 8263 [binary,8261.1,822.1] $F. Search stopped by max_proofs option. clauses kept 5016 user CPU time 2.03 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(f(f(V1,f(V3,V1)),f(V3,V2)),V3)) != V2. % Job 221 ----> UNIT CONFLICT at 2.03 sec ----> 8263 [binary,8261.1,783.1] $F. Search stopped by max_proofs option. clauses kept 5016 user CPU time 2.03 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(f(f(V1,f(V1,V3)),f(V3,V2)),V3)) != V2. % Job 222 ----> UNIT CONFLICT at 2.06 sec ----> 8263 [binary,8261.1,781.1] $F. Search stopped by max_proofs option. clauses kept 5016 user CPU time 2.06 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(f(f(V1,V2),f(f(V3,V1),V3)),V1)) != V2. % Job 223 ----> UNIT CONFLICT at 2.06 sec ----> 8263 [binary,8261.1,822.1] $F. Search stopped by max_proofs option. clauses kept 5016 user CPU time 2.06 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(f(f(V1,V2),f(f(V1,V3),V3)),V1)) != V2. % Job 224 ----> UNIT CONFLICT at 2.09 sec ----> 8263 [binary,8261.1,858.1] $F. Search stopped by max_proofs option. clauses kept 5016 user CPU time 2.10 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(f(f(V1,V2),f(V3,f(V3,V1))),V1)) != V2. % Job 225 ----> UNIT CONFLICT at 2.11 sec ----> 8263 [binary,8261.1,781.1] $F. Search stopped by max_proofs option. clauses kept 5016 user CPU time 2.11 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(f(f(V1,V2),f(V3,f(V1,V3))),V1)) != V2. % Job 226 ----> UNIT CONFLICT at 2.12 sec ----> 8263 [binary,8261.1,783.1] $F. Search stopped by max_proofs option. clauses kept 5016 user CPU time 2.12 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(V1,f(f(f(V3,V1),V3),f(V2,V1)))) != V2. % Job 227 ----> UNIT CONFLICT at 2.13 sec ----> 8251 [binary,8249.1,849.1] $F. Search stopped by max_proofs option. clauses kept 5007 user CPU time 2.13 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(V1,f(f(f(V1,V3),V3),f(V2,V1)))) != V2. % Job 228 ----> UNIT CONFLICT at 2.06 sec ----> 8251 [binary,8249.1,812.1] $F. Search stopped by max_proofs option. clauses kept 5007 user CPU time 2.07 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(V1,f(f(V3,f(V3,V1)),f(V2,V1)))) != V2. % Job 229 ----> UNIT CONFLICT at 2.04 sec ----> 8251 [binary,8249.1,785.1] $F. Search stopped by max_proofs option. clauses kept 5007 user CPU time 2.04 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(V1,f(f(V3,f(V1,V3)),f(V2,V1)))) != V2. % Job 230 ----> UNIT CONFLICT at 2.07 sec ----> 8251 [binary,8249.1,782.1] $F. Search stopped by max_proofs option. clauses kept 5007 user CPU time 2.07 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(V1,f(f(V2,V1),f(f(V3,V1),V3)))) != V2. % Job 231 ----> UNIT CONFLICT at 2.04 sec ----> 8251 [binary,8249.1,849.1] $F. Search stopped by max_proofs option. clauses kept 5007 user CPU time 2.04 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(V1,f(f(V2,V1),f(f(V1,V3),V3)))) != V2. % Job 232 ----> UNIT CONFLICT at 2.01 sec ----> 8251 [binary,8249.1,812.1] $F. Search stopped by max_proofs option. clauses kept 5007 user CPU time 2.01 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(V1,f(f(V1,V2),f(f(V3,V1),V3)))) != V2. % Job 233 ----> UNIT CONFLICT at 2.03 sec ----> 8251 [binary,8249.1,902.1] $F. Search stopped by max_proofs option. clauses kept 5007 user CPU time 2.03 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(V1,f(f(V1,V2),f(f(V1,V3),V3)))) != V2. % Job 234 ----> UNIT CONFLICT at 2.12 sec ----> 8251 [binary,8249.1,875.1] $F. Search stopped by max_proofs option. clauses kept 5007 user CPU time 2.12 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(V1,f(f(V2,V1),f(V3,f(V3,V1))))) != V2. % Job 235 ----> UNIT CONFLICT at 2.01 sec ----> 8251 [binary,8249.1,785.1] $F. Search stopped by max_proofs option. clauses kept 5007 user CPU time 2.01 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(V1,f(f(V2,V1),f(V3,f(V1,V3))))) != V2. % Job 236 ----> UNIT CONFLICT at 1.97 sec ----> 8251 [binary,8249.1,782.1] $F. Search stopped by max_proofs option. clauses kept 5007 user CPU time 1.98 (0 hr, 0 min, 1 sec) f(f(f(V0,f(V2,V2)),V2),f(V1,f(f(V1,V2),f(V3,f(V3,V1))))) != V2. % Job 237 ----> UNIT CONFLICT at 2.03 sec ----> 8251 [binary,8249.1,851.1] $F. Search stopped by max_proofs option. clauses kept 5007 user CPU time 2.04 (0 hr, 0 min, 2 sec) f(f(f(V0,f(V2,V2)),V2),f(V1,f(f(V1,V2),f(V3,f(V1,V3))))) != V2. % Job 238 ----> UNIT CONFLICT at 2.13 sec ----> 8251 [binary,8249.1,814.1] $F. Search stopped by max_proofs option. clauses kept 5007 user CPU time 2.13 (0 hr, 0 min, 2 sec) Finished ploop3 Thu Nov 21 16:20:40 CST 2002 on lemma.mcs.anl.gov