%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWX214+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n015.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue May 5 07:05:26 PM UTC 2026 % Result : Unknown 107.12s 107.44s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : SWX214+1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : otter-tptp-script %s % 0.17/0.35 % Computer : n015.cluster.edu % 0.17/0.35 % Model : x86_64 x86_64 % 0.17/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.35 % Memory : 8042.1875MB % 0.17/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.35 % CPULimit : 300 % 0.17/0.35 % WCLimit : 300 % 0.17/0.35 % DateTime : Tue May 5 12:04:31 EDT 2026 % 0.17/0.35 % CPUTime : % 1.51/2.40 ----- Otter 3.3f, August 2004 ----- % 1.51/2.40 The process was started by sandbox on n015.cluster.edu, % 1.51/2.40 Tue May 5 12:04:31 2026 % 1.51/2.40 The command was "./otter". The process ID is 26282. % 1.51/2.40 % 1.51/2.40 set(prolog_style_variables). % 1.51/2.40 set(auto). % 1.51/2.40 dependent: set(auto1). % 1.51/2.40 dependent: set(process_input). % 1.51/2.40 dependent: clear(print_kept). % 1.51/2.40 dependent: clear(print_new_demod). % 1.51/2.40 dependent: clear(print_back_demod). % 1.51/2.40 dependent: clear(print_back_sub). % 1.51/2.40 dependent: set(control_memory). % 1.51/2.40 dependent: assign(max_mem, 12000). % 1.51/2.40 dependent: assign(pick_given_ratio, 4). % 1.51/2.40 dependent: assign(stats_level, 1). % 1.51/2.40 dependent: assign(max_seconds, 10800). % 1.51/2.40 clear(print_given). % 1.51/2.40 % 1.51/2.40 formula_list(usable). % 1.51/2.40 all A (A=A). % 1.51/2.40 all X X2 (head(cons(X,X2))=X). % 1.51/2.40 all X X2 (tail(cons(X,X2))=X2). % 1.51/2.40 all X X2 (nil!=cons(X,X2)). % 1.51/2.40 a!=b. % 1.51/2.40 a!=c. % 1.51/2.40 b!=c. % 1.51/2.40 all X (proj1Atom(atom(X))=X). % 1.51/2.40 all X X2 (proj1(x(X,X2))=X). % 1.51/2.40 all X X2 (proj2(x(X,X2))=X2). % 1.51/2.40 all X X2 (proj12(y(X,X2))=X). % 1.51/2.40 all X X2 (proj22(y(X,X2))=X2). % 1.51/2.40 all X (proj1Star(star(X))=X). % 1.51/2.40 nil2!=eps. % 1.51/2.40 all X (nil2!=atom(X)). % 1.51/2.40 all X X2 (nil2!=x(X,X2)). % 1.51/2.40 all X X2 (nil2!=y(X,X2)). % 1.51/2.40 all X (nil2!=star(X)). % 1.51/2.40 all X (eps!=atom(X)). % 1.51/2.40 all X X2 (eps!=x(X,X2)). % 1.51/2.40 all X X2 (eps!=y(X,X2)). % 1.51/2.40 all X (eps!=star(X)). % 1.51/2.40 all X X2 X3 (atom(X)!=x(X2,X3)). % 1.51/2.40 all X X2 X3 (atom(X)!=y(X2,X3)). % 1.51/2.40 all X X2 (atom(X)!=star(X2)). % 1.51/2.40 all X X2 X3 X4 (x(X,X2)!=y(X3,X4)). % 1.51/2.40 all X X2 X3 (x(X,X2)!=star(X3)). % 1.51/2.40 all X X2 X3 (y(X,X2)!=star(X3)). % 1.51/2.40 all X Y (X!=nil2-> (Y!=nil2-> (X!=eps-> (Y!=eps->z(X,Y)=y(X,Y))))). % 1.51/2.40 all X (X!=nil2-> (X!=eps->z(X,eps)=X)). % 1.51/2.40 all Y (Y!=nil2->z(eps,Y)=Y). % 1.51/2.40 all X (X!=nil2->z(X,nil2)=nil2). % 1.51/2.40 all Y (z(nil2,Y)=nil2). % 1.51/2.40 all X Y (X!=nil2-> (Y!=nil2->x2(X,Y)=x(X,Y))). % 1.51/2.40 all X (X!=nil2->x2(X,nil2)=X). % 1.51/2.40 all Y (x2(nil2,Y)=Y). % 1.51/2.40 all X (X!=eps-> (X!=x(proj1(X),proj2(X))-> (X!=y(proj12(X),proj22(X))-> (X!=star(proj1Star(X))-> -eps2(X))))). % 1.51/2.40 eps2(eps). % 1.51/2.40 all P Q (eps2(x(P,Q))<->eps2(P)|eps2(Q)). % 1.51/2.40 all R Q2 (eps2(y(R,Q2))<->eps2(R)&eps2(Q2)). % 1.51/2.40 all Y eps2(star(Y)). % 1.51/2.40 all X Y (X!=atom(proj1Atom(X))-> (X!=x(proj1(X),proj2(X))-> (X!=y(proj12(X),proj22(X))-> (X!=star(proj1Star(X))->step(X,Y)=nil2)))). % 1.51/2.40 all Y B (B=Y->step(atom(B),Y)=eps). % 1.51/2.40 all Y B (B!=Y->step(atom(B),Y)=nil2). % 1.51/2.40 all Y P Q (step(x(P,Q),Y)=x(step(P,Y),step(Q,Y))). % 1.51/2.40 all Y R Q2 (eps2(R)->step(y(R,Q2),Y)=x(y(step(R,Y),Q2),step(Q2,Y))). % 1.51/2.40 all Y R Q2 (-eps2(R)->step(y(R,Q2),Y)=x(y(step(R,Y),Q2),nil2)). % 1.51/2.40 all Y P2 (step(star(P2),Y)=y(step(P2,Y),star(P2))). % 1.51/2.40 all X (rec(X,nil)<->eps2(X)). % 1.51/2.40 all X Z Xs (rec(X,cons(Z,Xs))<->rec(step(X,Z),Xs)). % 1.51/2.40 -(exists P Q A B (-(rec(star(x(P,Q)),cons(A,cons(B,nil)))<->rec(x(star(P),star(Q)),cons(A,cons(B,nil)))))). % 1.51/2.40 end_of_list. % 1.51/2.40 % 1.51/2.40 -------> usable clausifies to: % 1.51/2.40 % 1.51/2.40 list(usable). % 1.51/2.40 0 [] A=A. % 1.51/2.40 0 [] head(cons(X,X2))=X. % 1.51/2.40 0 [] tail(cons(X,X2))=X2. % 1.51/2.40 0 [] nil!=cons(X,X2). % 1.51/2.40 0 [] a!=b. % 1.51/2.40 0 [] a!=c. % 1.51/2.40 0 [] b!=c. % 1.51/2.40 0 [] proj1Atom(atom(X))=X. % 1.51/2.40 0 [] proj1(x(X,X2))=X. % 1.51/2.40 0 [] proj2(x(X,X2))=X2. % 1.51/2.40 0 [] proj12(y(X,X2))=X. % 1.51/2.40 0 [] proj22(y(X,X2))=X2. % 1.51/2.40 0 [] proj1Star(star(X))=X. % 1.51/2.40 0 [] nil2!=eps. % 1.51/2.40 0 [] nil2!=atom(X). % 1.51/2.40 0 [] nil2!=x(X,X2). % 1.51/2.40 0 [] nil2!=y(X,X2). % 1.51/2.40 0 [] nil2!=star(X). % 1.51/2.40 0 [] eps!=atom(X). % 1.51/2.40 0 [] eps!=x(X,X2). % 1.51/2.40 0 [] eps!=y(X,X2). % 1.51/2.40 0 [] eps!=star(X). % 1.51/2.40 0 [] atom(X)!=x(X2,X3). % 1.51/2.40 0 [] atom(X)!=y(X2,X3). % 1.51/2.40 0 [] atom(X)!=star(X2). % 1.51/2.40 0 [] x(X,X2)!=y(X3,X4). % 1.51/2.40 0 [] x(X,X2)!=star(X3). % 1.51/2.40 0 [] y(X,X2)!=star(X3). % 1.51/2.40 0 [] X=nil2|Y=nil2|X=eps|Y=eps|z(X,Y)=y(X,Y). % 1.51/2.40 0 [] X=nil2|X=eps|z(X,eps)=X. % 1.51/2.40 0 [] Y=nil2|z(eps,Y)=Y. % 1.51/2.40 0 [] X=nil2|z(X,nil2)=nil2. % 1.51/2.40 0 [] z(nil2,Y)=nil2. % 1.51/2.40 0 [] X=nil2|Y=nil2|x2(X,Y)=x(X,Y). % 1.51/2.40 0 [] X=nil2|x2(X,nil2)=X. % 1.51/2.40 0 [] x2(nil2,Y)=Y. % 1.51/2.40 0 [] X=eps|X=x(proj1(X),proj2(X))|X=y(proj12(X),proj22(X))|X=star(proj1Star(X))| -eps2(X). % 1.51/2.40 0 [] eps2(eps). % 1.51/2.40 0 [] -eps2(x(P,Q))|eps2(P)|eps2(Q). % 1.51/2.40 0 [] eps2(x(P,Q))| -eps2(P). % 1.51/2.40 0 [] eps2(x(P,Q))| -eps2(Q). % 1.51/2.40 0 [] -eps2(y(R,Q2))|eps2(R). % 1.51/2.40 0 [] -eps2(y(R,Q2))|eps2(Q2). % 1.51/2.40 0 [] eps2(y(R,Q2))| -eps2(R)| -eps2(Q2). % 1.51/2.40 0 [] eps2(star(Y)). % 1.51/2.40 0 [] X=atom(proj1Atom(X))|X=x(proj1(X),proj2(X))|X=y(proj12(X),proj22(X))|X=star(proj1Star(X))|step(X,Y)=nil2. % 1.51/2.40 0 [] B!=Y|step(atom(B),Y)=eps. % 1.51/2.40 0 [] B=Y|step(atom(B),Y)=nil2. % 1.51/2.40 0 [] step(x(P,Q),Y)=x(step(P,Y),step(Q,Y)). % 1.51/2.40 0 [] -eps2(R)|step(y(R,Q2),Y)=x(y(step(R,Y),Q2),step(Q2,Y)). % 1.51/2.40 0 [] eps2(R)|step(y(R,Q2),Y)=x(y(step(R,Y),Q2),nil2). % 1.51/2.40 0 [] step(star(P2),Y)=y(step(P2,Y),star(P2)). % 1.51/2.40 0 [] -rec(X,nil)|eps2(X). % 1.51/2.40 0 [] rec(X,nil)| -eps2(X). % 1.51/2.40 0 [] -rec(X,cons(Z,Xs))|rec(step(X,Z),Xs). % 1.51/2.40 0 [] rec(X,cons(Z,Xs))| -rec(step(X,Z),Xs). % 1.51/2.40 0 [] -rec(star(x(P,Q)),cons(A,cons(B,nil)))|rec(x(star(P),star(Q)),cons(A,cons(B,nil))). % 1.51/2.40 0 [] rec(star(x(P,Q)),cons(A,cons(B,nil)))| -rec(x(star(P),star(Q)),cons(A,cons(B,nil))). % 1.51/2.40 end_of_list. % 1.51/2.40 % 1.51/2.40 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=5. % 1.51/2.40 % 1.51/2.40 This ia a non-Horn set with equality. The strategy will be % 1.51/2.40 Knuth-Bendix, ordered hyper_res, factoring, and unit % 1.51/2.40 deletion, with positive clauses in sos and nonpositive % 1.51/2.40 clauses in usable. % 1.51/2.40 % 1.51/2.40 dependent: set(knuth_bendix). % 1.51/2.40 dependent: set(anl_eq). % 1.51/2.40 dependent: set(para_from). % 1.51/2.40 dependent: set(para_into). % 1.51/2.40 dependent: clear(para_from_right). % 1.51/2.40 dependent: clear(para_into_right). % 1.51/2.40 dependent: set(para_from_vars). % 1.51/2.40 dependent: set(eq_units_both_ways). % 1.51/2.40 dependent: set(dynamic_demod_all). % 1.51/2.40 dependent: set(dynamic_demod). % 1.51/2.40 dependent: set(order_eq). % 1.51/2.40 dependent: set(back_demod). % 1.51/2.40 dependent: set(lrpo). % 1.51/2.40 dependent: set(hyper_res). % 1.51/2.40 dependent: set(unit_deletion). % 1.51/2.40 dependent: set(factor). % 1.51/2.40 % 1.51/2.40 ------------> process usable: % 1.51/2.40 ** KEPT (pick-wt=5): 2 [copy,1,flip.1] cons(A,B)!=nil. % 1.51/2.40 ** KEPT (pick-wt=3): 4 [copy,3,flip.1] b!=a. % 1.51/2.40 ** KEPT (pick-wt=3): 6 [copy,5,flip.1] c!=a. % 1.51/2.40 ** KEPT (pick-wt=3): 8 [copy,7,flip.1] c!=b. % 1.51/2.40 ** KEPT (pick-wt=3): 9 [] nil2!=eps. % 1.51/2.40 ** KEPT (pick-wt=4): 11 [copy,10,flip.1] atom(A)!=nil2. % 1.51/2.40 ** KEPT (pick-wt=5): 13 [copy,12,flip.1] x(A,B)!=nil2. % 1.51/2.40 ** KEPT (pick-wt=5): 15 [copy,14,flip.1] y(A,B)!=nil2. % 1.51/2.40 ** KEPT (pick-wt=4): 17 [copy,16,flip.1] star(A)!=nil2. % 1.51/2.40 ** KEPT (pick-wt=4): 19 [copy,18,flip.1] atom(A)!=eps. % 1.51/2.40 ** KEPT (pick-wt=5): 21 [copy,20,flip.1] x(A,B)!=eps. % 1.51/2.40 ** KEPT (pick-wt=5): 23 [copy,22,flip.1] y(A,B)!=eps. % 1.51/2.40 ** KEPT (pick-wt=4): 25 [copy,24,flip.1] star(A)!=eps. % 1.51/2.40 ** KEPT (pick-wt=6): 26 [] atom(A)!=x(B,C). % 1.51/2.40 ** KEPT (pick-wt=6): 27 [] atom(A)!=y(B,C). % 1.51/2.40 ** KEPT (pick-wt=5): 28 [] atom(A)!=star(B). % 1.51/2.40 ** KEPT (pick-wt=7): 29 [] x(A,B)!=y(C,D). % 1.51/2.40 ** KEPT (pick-wt=6): 30 [] x(A,B)!=star(C). % 1.51/2.40 ** KEPT (pick-wt=6): 31 [] y(A,B)!=star(C). % 1.51/2.40 ** KEPT (pick-wt=24): 33 [copy,32,flip.2,flip.3,flip.4] A=eps|x(proj1(A),proj2(A))=A|y(proj12(A),proj22(A))=A|star(proj1Star(A))=A| -eps2(A). % 1.51/2.40 ** KEPT (pick-wt=8): 34 [] -eps2(x(A,B))|eps2(A)|eps2(B). % 1.51/2.40 ** KEPT (pick-wt=6): 35 [] eps2(x(A,B))| -eps2(A). % 1.51/2.40 ** KEPT (pick-wt=6): 36 [] eps2(x(A,B))| -eps2(B). % 1.51/2.40 ** KEPT (pick-wt=6): 37 [] -eps2(y(A,B))|eps2(A). % 1.51/2.40 ** KEPT (pick-wt=6): 38 [] -eps2(y(A,B))|eps2(B). % 1.51/2.40 ** KEPT (pick-wt=8): 39 [] eps2(y(A,B))| -eps2(A)| -eps2(B). % 1.51/2.40 ** KEPT (pick-wt=9): 40 [] A!=B|step(atom(A),B)=eps. % 1.51/2.40 ** KEPT (pick-wt=17): 42 [copy,41,flip.2] -eps2(A)|x(y(step(A,B),C),step(C,B))=step(y(A,C),B). % 1.51/2.40 ** KEPT (pick-wt=5): 43 [] -rec(A,nil)|eps2(A). % 1.51/2.40 ** KEPT (pick-wt=5): 44 [] rec(A,nil)| -eps2(A). % 1.51/2.40 ** KEPT (pick-wt=10): 45 [] -rec(A,cons(B,C))|rec(step(A,B),C). % 1.51/2.40 ** KEPT (pick-wt=10): 46 [] rec(A,cons(B,C))| -rec(step(A,B),C). % 1.51/2.40 ** KEPT (pick-wt=21): 47 [] -rec(star(x(A,B)),cons(C,cons(D,nil)))|rec(x(star(A),star(B)),cons(C,cons(D,nil))). % 1.51/2.40 ** KEPT (pick-wt=21): 48 [] rec(star(x(A,B)),cons(C,cons(D,nil)))| -rec(x(star(A),star(B)),cons(C,cons(D,nil))). % 1.51/2.40 ** KEPT (pick-wt=6): 49 [copy,26,flip.1] x(A,B)!=atom(C). % 1.51/2.40 ** KEPT (pick-wt=6): 50 [copy,27,flip.1] y(A,B)!=atom(C). % 1.51/2.40 ** KEPT (pick-wt=5): 51 [copy,28,flip.1] star(A)!=atom(B). % 1.51/2.40 ** KEPT (pick-wt=7): 52 [copy,29,flip.1] y(A,B)!=x(C,D). % 1.51/2.40 ** KEPT (pick-wt=6): 53 [copy,30,flip.1] star(A)!=x(B,C). % 1.51/2.40 ** KEPT (pick-wt=6): 54 [copy,31,flip.1] star(A)!=y(B,C). % 1.51/2.40 Following clause subsumed by 26 during input processing: 0 [copy,49,flip.1] atom(A)!=x(B,C). % 1.51/2.40 Following clause subsumed by 27 during input processing: 0 [copy,50,flip.1] atom(A)!=y(B,C). % 1.51/2.40 Following clause subsumed by 28 during input processing: 0 [copy,51,flip.1] atom(A)!=star(B). % 1.51/2.40 Following clause subsumed by 29 during input processing: 0 [copy,52,flip.1] x(A,B)!=y(C,D). % 1.51/2.40 Following clause subsumed by 30 during input processing: 0 [copy,53,flip.1] x(A,B)!=star(C). % 1.51/2.40 Following clause subsumed by 31 during input processing: 0 [copy,54,flip.1] y(A,B)!=star(C). % 1.51/2.40 % 1.51/2.40 ------------> process sos: % 1.51/2.40 ** KEPT (pick-wt=3): 57 [] A=A. % 107.12/107.44 ** KEPT (pick-wt=6): 58 [] head(cons(A,B))=A. % 107.12/107.44 ---> New Demodulator: 59 [new_demod,58] head(cons(A,B))=A. % 107.12/107.44 ** KEPT (pick-wt=6): 60 [] tail(cons(A,B))=B. % 107.12/107.44 ---> New Demodulator: 61 [new_demod,60] tail(cons(A,B))=B. % 107.12/107.44 ** KEPT (pick-wt=5): 62 [] proj1Atom(atom(A))=A. % 107.12/107.44 ---> New Demodulator: 63 [new_demod,62] proj1Atom(atom(A))=A. % 107.12/107.44 ** KEPT (pick-wt=6): 64 [] proj1(x(A,B))=A. % 107.12/107.44 ---> New Demodulator: 65 [new_demod,64] proj1(x(A,B))=A. % 107.12/107.44 ** KEPT (pick-wt=6): 66 [] proj2(x(A,B))=B. % 107.12/107.44 ---> New Demodulator: 67 [new_demod,66] proj2(x(A,B))=B. % 107.12/107.44 ** KEPT (pick-wt=6): 68 [] proj12(y(A,B))=A. % 107.12/107.44 ---> New Demodulator: 69 [new_demod,68] proj12(y(A,B))=A. % 107.12/107.44 ** KEPT (pick-wt=6): 70 [] proj22(y(A,B))=B. % 107.12/107.44 ---> New Demodulator: 71 [new_demod,70] proj22(y(A,B))=B. % 107.12/107.44 ** KEPT (pick-wt=5): 72 [] proj1Star(star(A))=A. % 107.12/107.44 ---> New Demodulator: 73 [new_demod,72] proj1Star(star(A))=A. % 107.12/107.44 ** KEPT (pick-wt=19): 74 [] A=nil2|B=nil2|A=eps|B=eps|z(A,B)=y(A,B). % 107.12/107.44 ** KEPT (pick-wt=11): 75 [] A=nil2|A=eps|z(A,eps)=A. % 107.12/107.44 ** KEPT (pick-wt=8): 76 [] A=nil2|z(eps,A)=A. % 107.12/107.44 ** KEPT (pick-wt=8): 77 [] A=nil2|z(A,nil2)=nil2. % 107.12/107.44 ** KEPT (pick-wt=5): 78 [] z(nil2,A)=nil2. % 107.12/107.44 ---> New Demodulator: 79 [new_demod,78] z(nil2,A)=nil2. % 107.12/107.44 ** KEPT (pick-wt=13): 80 [] A=nil2|B=nil2|x2(A,B)=x(A,B). % 107.12/107.44 ** KEPT (pick-wt=8): 81 [] A=nil2|x2(A,nil2)=A. % 107.12/107.44 ** KEPT (pick-wt=5): 82 [] x2(nil2,A)=A. % 107.12/107.44 ---> New Demodulator: 83 [new_demod,82] x2(nil2,A)=A. % 107.12/107.44 ** KEPT (pick-wt=2): 84 [] eps2(eps). % 107.12/107.44 ** KEPT (pick-wt=3): 85 [] eps2(star(A)). % 107.12/107.44 ** KEPT (pick-wt=29): 87 [copy,86,flip.1,flip.2,flip.3,flip.4] atom(proj1Atom(A))=A|x(proj1(A),proj2(A))=A|y(proj12(A),proj22(A))=A|star(proj1Star(A))=A|step(A,B)=nil2. % 107.12/107.44 ** KEPT (pick-wt=9): 88 [] A=B|step(atom(A),B)=nil2. % 107.12/107.44 ** KEPT (pick-wt=13): 90 [copy,89,flip.1] x(step(A,B),step(C,B))=step(x(A,C),B). % 107.12/107.44 ---> New Demodulator: 91 [new_demod,90] x(step(A,B),step(C,B))=step(x(A,C),B). % 107.12/107.44 ** KEPT (pick-wt=15): 93 [copy,92,flip.2] eps2(A)|x(y(step(A,B),C),nil2)=step(y(A,C),B). % 107.12/107.44 ** KEPT (pick-wt=11): 95 [copy,94,flip.1] y(step(A,B),star(A))=step(star(A),B). % 107.12/107.44 ---> New Demodulator: 96 [new_demod,95] y(step(A,B),star(A))=step(star(A),B). % 107.12/107.44 Following clause subsumed by 57 during input processing: 0 [copy,57,flip.1] A=A. % 107.12/107.44 >>>> Starting back demodulation with 59. % 107.12/107.44 >>>> Starting back demodulation with 61. % 107.12/107.44 >>>> Starting back demodulation with 63. % 107.12/107.44 >>>> Starting back demodulation with 65. % 107.12/107.44 >>>> Starting back demodulation with 67. % 107.12/107.44 >>>> Starting back demodulation with 69. % 107.12/107.44 >>>> Starting back demodulation with 71. % 107.12/107.44 >>>> Starting back demodulation with 73. % 107.12/107.44 >>>> Starting back demodulation with 79. % 107.12/107.44 >>>> Starting back demodulation with 83. % 107.12/107.44 >>>> Starting back demodulation with 91. % 107.12/107.44 >>>> Starting back demodulation with 96. % 107.12/107.44 % 107.12/107.44 ======= end of input processing ======= % 107.12/107.44 % 107.12/107.44 =========== start of search =========== % 107.12/107.44 % 107.12/107.44 % 107.12/107.44 Resetting weight limit to 7. % 107.12/107.44 % 107.12/107.44 % 107.12/107.44 Resetting weight limit to 7. % 107.12/107.44 % 107.12/107.44 sos_size=736 % 107.12/107.44 % 107.12/107.44 Search stopped because sos empty. % 107.12/107.44 % 107.12/107.44 % 107.12/107.44 Search stopped because sos empty. % 107.12/107.44 % 107.12/107.44 ============ end of search ============ % 107.12/107.44 % 107.12/107.44 -------------- statistics ------------- % 107.12/107.44 clauses given 807 % 107.12/107.44 clauses generated 3712624 % 107.12/107.44 clauses kept 868 % 107.12/107.44 clauses forward subsumed 9986 % 107.12/107.44 clauses back subsumed 17 % 107.12/107.44 Kbytes malloced 6835 % 107.12/107.44 % 107.12/107.44 ----------- times (seconds) ----------- % 107.12/107.44 user CPU time 104.92 (0 hr, 1 min, 44 sec) % 107.12/107.44 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 107.12/107.44 wall-clock time 107 (0 hr, 1 min, 47 sec) % 107.12/107.44 % 107.12/107.44 Process 26282 finished Tue May 5 12:06:18 2026 % 107.12/107.44 Otter interrupted % 107.12/107.44 PROOF NOT FOUND %------------------------------------------------------------------------------