%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWX225+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n011.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:27 PM UTC 2026 % Result : Unknown 11.84s 12.10s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX225+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : otter-tptp-script %s % 0.16/0.33 % Computer : n011.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.33 % CPULimit : 300 % 0.16/0.33 % WCLimit : 300 % 0.16/0.33 % DateTime : Tue May 5 12:42:47 EDT 2026 % 0.16/0.33 % CPUTime : % 1.88/2.10 ----- Otter 3.3f, August 2004 ----- % 1.88/2.10 The process was started by sandbox on n011.cluster.edu, % 1.88/2.10 Tue May 5 12:42:47 2026 % 1.88/2.10 The command was "./otter". The process ID is 20169. % 1.88/2.10 % 1.88/2.10 set(prolog_style_variables). % 1.88/2.10 set(auto). % 1.88/2.10 dependent: set(auto1). % 1.88/2.10 dependent: set(process_input). % 1.88/2.10 dependent: clear(print_kept). % 1.88/2.10 dependent: clear(print_new_demod). % 1.88/2.10 dependent: clear(print_back_demod). % 1.88/2.10 dependent: clear(print_back_sub). % 1.88/2.10 dependent: set(control_memory). % 1.88/2.10 dependent: assign(max_mem, 12000). % 1.88/2.10 dependent: assign(pick_given_ratio, 4). % 1.88/2.10 dependent: assign(stats_level, 1). % 1.88/2.10 dependent: assign(max_seconds, 10800). % 1.88/2.10 clear(print_given). % 1.88/2.10 % 1.88/2.10 formula_list(usable). % 1.88/2.10 all A (A=A). % 1.88/2.10 all X X2 (proj1(x(X,X2))=X). % 1.88/2.10 all X X2 (proj2(x(X,X2))=X2). % 1.88/2.10 all X X2 (x(X,X2)!=theVar). % 1.88/2.10 all X X2 (x(X,X2)!=k). % 1.88/2.10 all X X2 (x(X,X2)!=i). % 1.88/2.10 all X X2 (x(X,X2)!=s). % 1.88/2.10 all X X2 (x(X,X2)!=b). % 1.88/2.10 all X X2 (x(X,X2)!=c). % 1.88/2.10 theVar!=k. % 1.88/2.10 theVar!=i. % 1.88/2.10 theVar!=s. % 1.88/2.10 theVar!=b. % 1.88/2.10 theVar!=c. % 1.88/2.10 k!=i. % 1.88/2.10 k!=s. % 1.88/2.10 k!=b. % 1.88/2.10 k!=c. % 1.88/2.10 i!=s. % 1.88/2.10 i!=b. % 1.88/2.10 i!=c. % 1.88/2.10 s!=b. % 1.88/2.10 s!=c. % 1.88/2.10 b!=c. % 1.88/2.10 all X (proj1Suc(suc(X))=X). % 1.88/2.10 all X (suc(X)!=z). % 1.88/2.10 all X (proj1Just(just(X))=X). % 1.88/2.10 all X (nothing!=just(X)). % 1.88/2.10 all Y Z (fail(Y,Z)=par(Y,Z,step(Y),step(Z))). % 1.88/2.10 all X Y (par(X,Y,nothing,nothing)=nothing). % 1.88/2.10 all X Y U_red (par(X,Y,nothing,just(U_red))=just(x(X,U_red))). % 1.88/2.10 all X Y T_red (par(X,Y,just(T_red),nothing)=just(x(T_red,Y))). % 1.88/2.10 all X Y T_red U_red2 (par(X,Y,just(T_red),just(U_red2))=just(x(T_red,U_red2))). % 1.88/2.10 all X (X!=x(proj1(X),proj2(X))->step(X)=nothing). % 1.88/2.10 all Y Z (Y!=x(proj1(Y),proj2(Y))-> (Y!=i->step(x(Y,Z))=fail(Y,Z))). % 1.88/2.10 all Z X2 G (X2!=x(proj1(X2),proj2(X2))-> (X2!=k->step(x(x(X2,G),Z))=fail(x(X2,G),Z))). % 1.88/2.10 all Z G X3 F (X3!=s-> (X3!=b-> (X3!=c->step(x(x(x(X3,F),G),Z))=fail(x(x(X3,F),G),Z)))). % 1.88/2.10 all Z G F (step(x(x(x(s,F),G),Z))=just(x(x(F,Z),x(G,Z)))). % 1.88/2.10 all Z G F (step(x(x(x(b,F),G),Z))=just(x(F,x(G,Z)))). % 1.88/2.10 all Z G F (step(x(x(x(c,F),G),Z))=just(x(x(F,Z),G))). % 1.88/2.10 all Z G (step(x(x(k,G),Z))=just(G)). % 1.88/2.10 all Z (step(x(i,Z))=just(Z)). % 1.88/2.10 -(exists X (step(X)=just(X))). % 1.88/2.10 end_of_list. % 1.88/2.10 % 1.88/2.10 -------> usable clausifies to: % 1.88/2.10 % 1.88/2.10 list(usable). % 1.88/2.10 0 [] A=A. % 1.88/2.10 0 [] proj1(x(X,X2))=X. % 1.88/2.10 0 [] proj2(x(X,X2))=X2. % 1.88/2.10 0 [] x(X,X2)!=theVar. % 1.88/2.10 0 [] x(X,X2)!=k. % 1.88/2.10 0 [] x(X,X2)!=i. % 1.88/2.10 0 [] x(X,X2)!=s. % 1.88/2.10 0 [] x(X,X2)!=b. % 1.88/2.10 0 [] x(X,X2)!=c. % 1.88/2.10 0 [] theVar!=k. % 1.88/2.10 0 [] theVar!=i. % 1.88/2.10 0 [] theVar!=s. % 1.88/2.10 0 [] theVar!=b. % 1.88/2.10 0 [] theVar!=c. % 1.88/2.10 0 [] k!=i. % 1.88/2.10 0 [] k!=s. % 1.88/2.10 0 [] k!=b. % 1.88/2.10 0 [] k!=c. % 1.88/2.10 0 [] i!=s. % 1.88/2.10 0 [] i!=b. % 1.88/2.10 0 [] i!=c. % 1.88/2.10 0 [] s!=b. % 1.88/2.10 0 [] s!=c. % 1.88/2.10 0 [] b!=c. % 1.88/2.10 0 [] proj1Suc(suc(X))=X. % 1.88/2.10 0 [] suc(X)!=z. % 1.88/2.10 0 [] proj1Just(just(X))=X. % 1.88/2.10 0 [] nothing!=just(X). % 1.88/2.10 0 [] fail(Y,Z)=par(Y,Z,step(Y),step(Z)). % 1.88/2.10 0 [] par(X,Y,nothing,nothing)=nothing. % 1.88/2.10 0 [] par(X,Y,nothing,just(U_red))=just(x(X,U_red)). % 1.88/2.10 0 [] par(X,Y,just(T_red),nothing)=just(x(T_red,Y)). % 1.88/2.10 0 [] par(X,Y,just(T_red),just(U_red2))=just(x(T_red,U_red2)). % 1.88/2.10 0 [] X=x(proj1(X),proj2(X))|step(X)=nothing. % 1.88/2.10 0 [] Y=x(proj1(Y),proj2(Y))|Y=i|step(x(Y,Z))=fail(Y,Z). % 1.88/2.10 0 [] X2=x(proj1(X2),proj2(X2))|X2=k|step(x(x(X2,G),Z))=fail(x(X2,G),Z). % 1.88/2.10 0 [] X3=s|X3=b|X3=c|step(x(x(x(X3,F),G),Z))=fail(x(x(X3,F),G),Z). % 1.88/2.10 0 [] step(x(x(x(s,F),G),Z))=just(x(x(F,Z),x(G,Z))). % 1.88/2.10 0 [] step(x(x(x(b,F),G),Z))=just(x(F,x(G,Z))). % 1.88/2.10 0 [] step(x(x(x(c,F),G),Z))=just(x(x(F,Z),G)). % 1.88/2.10 0 [] step(x(x(k,G),Z))=just(G). % 1.88/2.10 0 [] step(x(i,Z))=just(Z). % 1.88/2.10 0 [] step(X)!=just(X). % 1.88/2.10 end_of_list. % 1.88/2.10 % 1.88/2.10 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=4. % 1.88/2.10 % 1.88/2.10 This ia a non-Horn set with equality. The strategy will be % 1.88/2.10 Knuth-Bendix, ordered hyper_res, factoring, and unit % 1.88/2.10 deletion, with positive clauses in sos and nonpositive % 1.88/2.10 clauses in usable. % 1.88/2.10 % 1.88/2.10 dependent: set(knuth_bendix). % 1.88/2.10 dependent: set(anl_eq). % 1.88/2.10 dependent: set(para_from). % 1.88/2.10 dependent: set(para_into). % 1.88/2.10 dependent: clear(para_from_right). % 1.88/2.10 dependent: clear(para_into_right). % 1.88/2.10 dependent: set(para_from_vars). % 1.88/2.10 dependent: set(eq_units_both_ways). % 1.88/2.10 dependent: set(dynamic_demod_all). % 1.88/2.10 dependent: set(dynamic_demod). % 1.88/2.10 dependent: set(order_eq). % 1.88/2.10 dependent: set(back_demod). % 1.88/2.10 dependent: set(lrpo). % 1.88/2.10 dependent: set(hyper_res). % 1.88/2.10 dependent: set(unit_deletion). % 1.88/2.10 dependent: set(factor). % 1.88/2.10 % 1.88/2.10 ------------> process usable: % 1.88/2.10 ** KEPT (pick-wt=5): 1 [] x(A,B)!=theVar. % 1.88/2.10 ** KEPT (pick-wt=5): 2 [] x(A,B)!=k. % 1.88/2.10 ** KEPT (pick-wt=5): 3 [] x(A,B)!=i. % 1.88/2.10 ** KEPT (pick-wt=5): 4 [] x(A,B)!=s. % 1.88/2.10 ** KEPT (pick-wt=5): 5 [] x(A,B)!=b. % 1.88/2.10 ** KEPT (pick-wt=5): 6 [] x(A,B)!=c. % 1.88/2.10 ** KEPT (pick-wt=3): 7 [] theVar!=k. % 1.88/2.10 ** KEPT (pick-wt=3): 8 [] theVar!=i. % 1.88/2.10 ** KEPT (pick-wt=3): 9 [] theVar!=s. % 1.88/2.10 ** KEPT (pick-wt=3): 10 [] theVar!=b. % 1.88/2.10 ** KEPT (pick-wt=3): 11 [] theVar!=c. % 1.88/2.10 ** KEPT (pick-wt=3): 12 [] k!=i. % 1.88/2.10 ** KEPT (pick-wt=3): 14 [copy,13,flip.1] s!=k. % 1.88/2.10 ** KEPT (pick-wt=3): 15 [] k!=b. % 1.88/2.10 ** KEPT (pick-wt=3): 16 [] k!=c. % 1.88/2.10 ** KEPT (pick-wt=3): 18 [copy,17,flip.1] s!=i. % 1.88/2.10 ** KEPT (pick-wt=3): 19 [] i!=b. % 1.88/2.10 ** KEPT (pick-wt=3): 20 [] i!=c. % 1.88/2.10 ** KEPT (pick-wt=3): 21 [] s!=b. % 1.88/2.10 ** KEPT (pick-wt=3): 22 [] s!=c. % 1.88/2.10 ** KEPT (pick-wt=3): 24 [copy,23,flip.1] c!=b. % 1.88/2.10 ** KEPT (pick-wt=4): 25 [] suc(A)!=z. % 1.88/2.10 ** KEPT (pick-wt=4): 27 [copy,26,flip.1] just(A)!=nothing. % 1.88/2.10 ** KEPT (pick-wt=5): 28 [] step(A)!=just(A). % 1.88/2.10 % 1.88/2.10 ------------> process sos: % 1.88/2.10 ** KEPT (pick-wt=3): 29 [] A=A. % 1.88/2.10 ** KEPT (pick-wt=6): 30 [] proj1(x(A,B))=A. % 1.88/2.10 ---> New Demodulator: 31 [new_demod,30] proj1(x(A,B))=A. % 1.88/2.10 ** KEPT (pick-wt=6): 32 [] proj2(x(A,B))=B. % 1.88/2.10 ---> New Demodulator: 33 [new_demod,32] proj2(x(A,B))=B. % 1.88/2.10 ** KEPT (pick-wt=5): 34 [] proj1Suc(suc(A))=A. % 1.88/2.10 ---> New Demodulator: 35 [new_demod,34] proj1Suc(suc(A))=A. % 1.88/2.10 ** KEPT (pick-wt=5): 36 [] proj1Just(just(A))=A. % 1.88/2.10 ---> New Demodulator: 37 [new_demod,36] proj1Just(just(A))=A. % 1.88/2.10 ** KEPT (pick-wt=11): 38 [] fail(A,B)=par(A,B,step(A),step(B)). % 1.88/2.10 ** KEPT (pick-wt=7): 39 [] par(A,B,nothing,nothing)=nothing. % 1.88/2.10 ---> New Demodulator: 40 [new_demod,39] par(A,B,nothing,nothing)=nothing. % 1.88/2.10 ** KEPT (pick-wt=11): 41 [] par(A,B,nothing,just(C))=just(x(A,C)). % 1.88/2.10 ** KEPT (pick-wt=11): 42 [] par(A,B,just(C),nothing)=just(x(C,B)). % 1.88/2.10 ** KEPT (pick-wt=12): 43 [] par(A,B,just(C),just(D))=just(x(C,D)). % 1.88/2.10 ** KEPT (pick-wt=11): 45 [copy,44,flip.1] x(proj1(A),proj2(A))=A|step(A)=nothing. % 1.88/2.10 ** KEPT (pick-wt=18): 47 [copy,46,flip.1] x(proj1(A),proj2(A))=A|A=i|step(x(A,B))=fail(A,B). % 1.88/2.10 ** KEPT (pick-wt=22): 49 [copy,48,flip.1] x(proj1(A),proj2(A))=A|A=k|step(x(x(A,B),C))=fail(x(A,B),C). % 1.88/2.10 ** KEPT (pick-wt=25): 50 [] A=s|A=b|A=c|step(x(x(x(A,B),C),D))=fail(x(x(A,B),C),D). % 1.88/2.10 ** KEPT (pick-wt=17): 51 [] step(x(x(x(s,A),B),C))=just(x(x(A,C),x(B,C))). % 1.88/2.10 ---> New Demodulator: 52 [new_demod,51] step(x(x(x(s,A),B),C))=just(x(x(A,C),x(B,C))). % 1.88/2.10 ** KEPT (pick-wt=15): 53 [] step(x(x(x(b,A),B),C))=just(x(A,x(B,C))). % 1.88/2.10 ---> New Demodulator: 54 [new_demod,53] step(x(x(x(b,A),B),C))=just(x(A,x(B,C))). % 1.88/2.10 ** KEPT (pick-wt=15): 55 [] step(x(x(x(c,A),B),C))=just(x(x(A,C),B)). % 1.88/2.10 ---> New Demodulator: 56 [new_demod,55] step(x(x(x(c,A),B),C))=just(x(x(A,C),B)). % 1.88/2.10 ** KEPT (pick-wt=9): 57 [] step(x(x(k,A),B))=just(A). % 1.88/2.10 ---> New Demodulator: 58 [new_demod,57] step(x(x(k,A),B))=just(A). % 1.88/2.10 ** KEPT (pick-wt=7): 59 [] step(x(i,A))=just(A). % 1.88/2.10 ---> New Demodulator: 60 [new_demod,59] step(x(i,A))=just(A). % 1.88/2.10 Following clause subsumed by 29 during input processing: 0 [copy,29,flip.1] A=A. % 1.88/2.10 >>>> Starting back demodulation with 31. % 1.88/2.10 >>>> Starting back demodulation with 33. % 1.88/2.10 >>>> Starting back demodulation with 35. % 1.88/2.10 >>>> Starting back demodulation with 37. % 1.88/2.10 ** KEPT (pick-wt=11): 61 [copy,38,flip.1] par(A,B,step(A),step(B))=fail(A,B). % 1.88/2.10 >>>> Starting back demodulation with 40. % 1.88/2.10 ** KEPT (pick-wt=11): 62 [copy,41,flip.1] just(x(A,B))=par(A,C,nothing,just(B)). % 1.88/2.10 ** KEPT (pick-wt=11): 63 [copy,42,flip.1] just(x(A,B))=par(C,B,just(A),nothing). % 1.88/2.10 ** KEPT (pick-wt=12): 64 [copy,43,flip.1] just(x(A,B))=par(C,D,just(A),just(B)). % 1.88/2.10 >>>> Starting back demodulation with 52. % 1.88/2.10 >>>> Starting back demodulation with 54. % 1.88/2.10 >>>> Starting back demodulation with 56. % 1.88/2.10 >>>> Starting back demodulation with 58. % 1.88/2.10 >>>> Starting back demodulation with 60. % 1.88/2.10 Following clause subsumed by 38 during input processing: 0 [copy,61,flip.1] fail(A,B)=par(A,B,step(A),step(B)). % 1.88/2.10 Following clause subsumed by 41 during input processing: 0 [copy,62,flip.1] par(A,B,nothing,just(C))=just(x(A,C)). % 1.88/2.10 Following clause subsumed by 42 during input processing: 0 [copy,63,flip.1] par(A,B,just(C),nothing)=just(x(C,B)). % 1.88/2.10 Following clause subsumed by 43 during input processing: 0 [copy,64,flip.1] par(A,B,just(C),just(D))=just(x(C,D)). % 1.88/2.10 % 1.88/2.10 ======= end of input processing ======= % 1.88/2.10 % 1.88/2.10 =========== start of search =========== % 11.84/12.09 % 11.84/12.09 % 11.84/12.09 Resetting weight limit to 12. % 11.84/12.09 % 11.84/12.09 % 11.84/12.09 Resetting weight limit to 12. % 11.84/12.09 % 11.84/12.09 sos_size=328 % 11.84/12.09 % 11.84/12.09 % 11.84/12.09 Resetting weight limit to 10. % 11.84/12.09 % 11.84/12.09 % 11.84/12.09 Resetting weight limit to 10. % 11.84/12.09 % 11.84/12.09 sos_size=359 % 11.84/12.09 % 11.84/12.09 Search stopped because sos empty. % 11.84/12.09 % 11.84/12.09 % 11.84/12.09 Search stopped because sos empty. % 11.84/12.09 % 11.84/12.09 ============ end of search ============ % 11.84/12.09 % 11.84/12.09 -------------- statistics ------------- % 11.84/12.09 clauses given 519 % 11.84/12.09 clauses generated 654111 % 11.84/12.09 clauses kept 547 % 11.84/12.09 clauses forward subsumed 7176 % 11.84/12.09 clauses back subsumed 1 % 11.84/12.09 Kbytes malloced 7812 % 11.84/12.09 % 11.84/12.09 ----------- times (seconds) ----------- % 11.84/12.09 user CPU time 10.00 (0 hr, 0 min, 9 sec) % 11.84/12.09 system CPU time 0.00 (0 hr, 0 min, 0 sec) % 11.84/12.09 wall-clock time 11 (0 hr, 0 min, 11 sec) % 11.84/12.09 % 11.84/12.09 Process 20169 finished Tue May 5 12:42:58 2026 % 11.84/12.09 Otter interrupted % 11.84/12.09 PROOF NOT FOUND %------------------------------------------------------------------------------