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