%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWX217-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n008.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 1.95s 2.15s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX217-1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : otter-tptp-script %s % 0.16/0.33 % Computer : n008.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:16:28 EDT 2026 % 0.16/0.34 % CPUTime : % 1.92/2.12 ----- Otter 3.3f, August 2004 ----- % 1.92/2.12 The process was started by sandbox2 on n008.cluster.edu, % 1.92/2.12 Tue May 5 12:16:28 2026 % 1.92/2.12 The command was "./otter". The process ID is 12887. % 1.92/2.12 % 1.92/2.12 set(prolog_style_variables). % 1.92/2.12 set(auto). % 1.92/2.12 dependent: set(auto1). % 1.92/2.12 dependent: set(process_input). % 1.92/2.12 dependent: clear(print_kept). % 1.92/2.12 dependent: clear(print_new_demod). % 1.92/2.12 dependent: clear(print_back_demod). % 1.92/2.12 dependent: clear(print_back_sub). % 1.92/2.12 dependent: set(control_memory). % 1.92/2.12 dependent: assign(max_mem, 12000). % 1.92/2.12 dependent: assign(pick_given_ratio, 4). % 1.92/2.12 dependent: assign(stats_level, 1). % 1.92/2.12 dependent: assign(max_seconds, 10800). % 1.92/2.12 clear(print_given). % 1.92/2.12 % 1.92/2.12 list(usable). % 1.92/2.12 0 [] A=A. % 1.92/2.12 0 [] aux(Y,btrue)=cons(o,shw(half(suc(Y)))). % 1.92/2.12 0 [] aux(Y,bfalse)=cons(i,shw(half(suc(Y)))). % 1.92/2.12 0 [] notb(btrue)=bfalse. % 1.92/2.12 0 [] notb(bfalse)=btrue. % 1.92/2.12 0 [] half(zero)=zero. % 1.92/2.12 0 [] half(suc(zero))=zero. % 1.92/2.12 0 [] half(suc(suc(N)))=suc(half(N)). % 1.92/2.12 0 [] evenNat(zero)=btrue. % 1.92/2.12 0 [] evenNat(suc(N))=notb(evenNat(N)). % 1.92/2.12 0 [] shw(zero)=nil. % 1.92/2.12 0 [] shw(suc(Y))=aux(Y,evenNat(suc(Y))). % 1.92/2.12 0 [] append(nil,Y)=Y. % 1.92/2.12 0 [] append(cons(Z,Xs),Y)=cons(Z,append(Xs,Y)). % 1.92/2.12 0 [] addNat(zero,Y)=Y. % 1.92/2.12 0 [] addNat(suc(Z),Y)=suc(addNat(Z,Y)). % 1.92/2.12 0 [] double(X)=addNat(X,X). % 1.92/2.12 0 [] rd(nil)=zero. % 1.92/2.12 0 [] rd(cons(i,Xs))=suc(double(rd(Xs))). % 1.92/2.12 0 [] rd(cons(o,Xs))=double(rd(Xs)). % 1.92/2.12 0 [] x(X,Y)=rd(append(shw(X),shw(Y))). % 1.92/2.12 0 [] sat_comm(X,Y)=e_q(x(X,Y),x(Y,X)). % 1.92/2.12 0 [] e_q2(bfalse,btrue)=bfalse. % 1.92/2.12 0 [] e_q2(btrue,bfalse)=bfalse. % 1.92/2.12 0 [] e_q3(i,o)=bfalse. % 1.92/2.12 0 [] e_q3(o,i)=bfalse. % 1.92/2.12 0 [] e_q(suc(X),suc(Y))=e_q(X,Y). % 1.92/2.12 0 [] e_q(zero,suc(X))=bfalse. % 1.92/2.12 0 [] e_q(suc(X),zero)=bfalse. % 1.92/2.12 0 [] e_q(X,X)=btrue. % 1.92/2.12 0 [] e_q2(X,X)=btrue. % 1.92/2.12 0 [] e_q3(X,X)=btrue. % 1.92/2.12 0 [] e_q2(sat_comm(X,Y),bfalse)!=btrue. % 1.92/2.12 end_of_list. % 1.92/2.12 % 1.92/2.12 SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=1. % 1.92/2.12 % 1.92/2.12 All clauses are units, and equality is present; the % 1.92/2.12 strategy will be Knuth-Bendix with positive clauses in sos. % 1.92/2.12 % 1.92/2.12 dependent: set(knuth_bendix). % 1.92/2.12 dependent: set(anl_eq). % 1.92/2.12 dependent: set(para_from). % 1.92/2.12 dependent: set(para_into). % 1.92/2.12 dependent: clear(para_from_right). % 1.92/2.12 dependent: clear(para_into_right). % 1.92/2.12 dependent: set(para_from_vars). % 1.92/2.12 dependent: set(eq_units_both_ways). % 1.92/2.12 dependent: set(dynamic_demod_all). % 1.92/2.12 dependent: set(dynamic_demod). % 1.92/2.12 dependent: set(order_eq). % 1.92/2.12 dependent: set(back_demod). % 1.92/2.12 dependent: set(lrpo). % 1.92/2.12 % 1.92/2.12 ------------> process usable: % 1.92/2.12 ** KEPT (pick-wt=7): 1 [] e_q2(sat_comm(A,B),bfalse)!=btrue. % 1.92/2.12 % 1.92/2.12 ------------> process sos: % 1.92/2.12 ** KEPT (pick-wt=3): 2 [] A=A. % 1.92/2.12 ** KEPT (pick-wt=10): 4 [copy,3,flip.1] cons(o,shw(half(suc(A))))=aux(A,btrue). % 1.92/2.12 ---> New Demodulator: 5 [new_demod,4] cons(o,shw(half(suc(A))))=aux(A,btrue). % 1.92/2.12 ** KEPT (pick-wt=10): 7 [copy,6,flip.1] cons(i,shw(half(suc(A))))=aux(A,bfalse). % 1.92/2.12 ---> New Demodulator: 8 [new_demod,7] cons(i,shw(half(suc(A))))=aux(A,bfalse). % 1.92/2.12 ** KEPT (pick-wt=4): 9 [] notb(btrue)=bfalse. % 1.92/2.12 ---> New Demodulator: 10 [new_demod,9] notb(btrue)=bfalse. % 1.92/2.12 ** KEPT (pick-wt=4): 11 [] notb(bfalse)=btrue. % 1.92/2.12 ---> New Demodulator: 12 [new_demod,11] notb(bfalse)=btrue. % 1.92/2.12 ** KEPT (pick-wt=4): 13 [] half(zero)=zero. % 1.92/2.12 ---> New Demodulator: 14 [new_demod,13] half(zero)=zero. % 1.92/2.12 ** KEPT (pick-wt=5): 15 [] half(suc(zero))=zero. % 1.92/2.12 ---> New Demodulator: 16 [new_demod,15] half(suc(zero))=zero. % 1.92/2.12 ** KEPT (pick-wt=8): 17 [] half(suc(suc(A)))=suc(half(A)). % 1.92/2.12 ---> New Demodulator: 18 [new_demod,17] half(suc(suc(A)))=suc(half(A)). % 1.92/2.12 ** KEPT (pick-wt=4): 19 [] evenNat(zero)=btrue. % 1.92/2.12 ---> New Demodulator: 20 [new_demod,19] evenNat(zero)=btrue. % 1.92/2.12 ** KEPT (pick-wt=7): 21 [] evenNat(suc(A))=notb(evenNat(A)). % 1.92/2.12 ---> New Demodulator: 22 [new_demod,21] evenNat(suc(A))=notb(evenNat(A)). % 1.92/2.12 ** KEPT (pick-wt=4): 23 [] shw(zero)=nil. % 1.92/2.12 ---> New Demodulator: 24 [new_demod,23] shw(zero)=nil. % 1.92/2.12 ** KEPT (pick-wt=9): 26 [copy,25,demod,22] shw(suc(A))=aux(A,notb(evenNat(A))). % 1.92/2.12 ---> New Demodulator: 27 [new_demod,26] shw(suc(A))=aux(A,notb(evenNat(A))). % 1.92/2.12 ** KEPT (pick-wt=5): 28 [] append(nil,A)=A. % 1.92/2.12 ---> New Demodulator: 29 [new_demod,28] append(nil,A)=A. % 1.92/2.12 ** KEPT (pick-wt=11): 31 [copy,30,flip.1] cons(A,append(B,C))=append(cons(A,B),C). % 1.92/2.12 ---> New Demodulator: 32 [new_demod,31] cons(A,append(B,C))=append(cons(A,B),C). % 1.92/2.12 ** KEPT (pick-wt=5): 33 [] addNat(zero,A)=A. % 1.95/2.15 ---> New Demodulator: 34 [new_demod,33] addNat(zero,A)=A. % 1.95/2.15 ** KEPT (pick-wt=9): 36 [copy,35,flip.1] suc(addNat(A,B))=addNat(suc(A),B). % 1.95/2.15 ---> New Demodulator: 37 [new_demod,36] suc(addNat(A,B))=addNat(suc(A),B). % 1.95/2.15 ** KEPT (pick-wt=6): 38 [] double(A)=addNat(A,A). % 1.95/2.15 ---> New Demodulator: 39 [new_demod,38] double(A)=addNat(A,A). % 1.95/2.15 ** KEPT (pick-wt=4): 40 [] rd(nil)=zero. % 1.95/2.15 ---> New Demodulator: 41 [new_demod,40] rd(nil)=zero. % 1.95/2.15 ** KEPT (pick-wt=11): 43 [copy,42,demod,39,37,flip.1] addNat(suc(rd(A)),rd(A))=rd(cons(i,A)). % 1.95/2.15 ---> New Demodulator: 44 [new_demod,43] addNat(suc(rd(A)),rd(A))=rd(cons(i,A)). % 1.95/2.15 ** KEPT (pick-wt=10): 46 [copy,45,demod,39] rd(cons(o,A))=addNat(rd(A),rd(A)). % 1.95/2.15 ---> New Demodulator: 47 [new_demod,46] rd(cons(o,A))=addNat(rd(A),rd(A)). % 1.95/2.15 ** KEPT (pick-wt=10): 49 [copy,48,flip.1] rd(append(shw(A),shw(B)))=x(A,B). % 1.95/2.15 ---> New Demodulator: 50 [new_demod,49] rd(append(shw(A),shw(B)))=x(A,B). % 1.95/2.15 ** KEPT (pick-wt=11): 52 [copy,51,flip.1] e_q(x(A,B),x(B,A))=sat_comm(A,B). % 1.95/2.15 ---> New Demodulator: 53 [new_demod,52] e_q(x(A,B),x(B,A))=sat_comm(A,B). % 1.95/2.15 ** KEPT (pick-wt=5): 54 [] e_q2(bfalse,btrue)=bfalse. % 1.95/2.15 ---> New Demodulator: 55 [new_demod,54] e_q2(bfalse,btrue)=bfalse. % 1.95/2.15 ** KEPT (pick-wt=5): 56 [] e_q2(btrue,bfalse)=bfalse. % 1.95/2.15 ---> New Demodulator: 57 [new_demod,56] e_q2(btrue,bfalse)=bfalse. % 1.95/2.15 ** KEPT (pick-wt=5): 58 [] e_q3(i,o)=bfalse. % 1.95/2.15 ---> New Demodulator: 59 [new_demod,58] e_q3(i,o)=bfalse. % 1.95/2.15 ** KEPT (pick-wt=5): 60 [] e_q3(o,i)=bfalse. % 1.95/2.15 ---> New Demodulator: 61 [new_demod,60] e_q3(o,i)=bfalse. % 1.95/2.15 ** KEPT (pick-wt=9): 62 [] e_q(suc(A),suc(B))=e_q(A,B). % 1.95/2.15 ---> New Demodulator: 63 [new_demod,62] e_q(suc(A),suc(B))=e_q(A,B). % 1.95/2.15 ** KEPT (pick-wt=6): 64 [] e_q(zero,suc(A))=bfalse. % 1.95/2.15 ---> New Demodulator: 65 [new_demod,64] e_q(zero,suc(A))=bfalse. % 1.95/2.15 ** KEPT (pick-wt=6): 66 [] e_q(suc(A),zero)=bfalse. % 1.95/2.15 ---> New Demodulator: 67 [new_demod,66] e_q(suc(A),zero)=bfalse. % 1.95/2.15 ** KEPT (pick-wt=5): 68 [] e_q(A,A)=btrue. % 1.95/2.15 ---> New Demodulator: 69 [new_demod,68] e_q(A,A)=btrue. % 1.95/2.15 ** KEPT (pick-wt=5): 70 [] e_q2(A,A)=btrue. % 1.95/2.15 ---> New Demodulator: 71 [new_demod,70] e_q2(A,A)=btrue. % 1.95/2.15 ** KEPT (pick-wt=5): 72 [] e_q3(A,A)=btrue. % 1.95/2.15 ---> New Demodulator: 73 [new_demod,72] e_q3(A,A)=btrue. % 1.95/2.15 Following clause subsumed by 2 during input processing: 0 [copy,2,flip.1] A=A. % 1.95/2.15 >>>> Starting back demodulation with 5. % 1.95/2.15 >>>> Starting back demodulation with 8. % 1.95/2.15 >>>> Starting back demodulation with 10. % 1.95/2.15 >>>> Starting back demodulation with 12. % 1.95/2.15 >>>> Starting back demodulation with 14. % 1.95/2.15 >>>> Starting back demodulation with 16. % 1.95/2.15 >>>> Starting back demodulation with 18. % 1.95/2.15 >>>> Starting back demodulation with 20. % 1.95/2.15 >>>> Starting back demodulation with 22. % 1.95/2.15 >>>> Starting back demodulation with 24. % 1.95/2.15 >>>> Starting back demodulation with 27. % 1.95/2.15 >>>> Starting back demodulation with 29. % 1.95/2.15 >>>> Starting back demodulation with 32. % 1.95/2.15 >>>> Starting back demodulation with 34. % 1.95/2.15 >>>> Starting back demodulation with 37. % 1.95/2.15 >>>> Starting back demodulation with 39. % 1.95/2.15 >>>> Starting back demodulation with 41. % 1.95/2.15 >>>> Starting back demodulation with 44. % 1.95/2.15 >>>> Starting back demodulation with 47. % 1.95/2.15 >>>> Starting back demodulation with 50. % 1.95/2.15 >>>> Starting back demodulation with 53. % 1.95/2.15 >>>> Starting back demodulation with 55. % 1.95/2.15 >>>> Starting back demodulation with 57. % 1.95/2.15 >>>> Starting back demodulation with 59. % 1.95/2.15 >>>> Starting back demodulation with 61. % 1.95/2.15 >>>> Starting back demodulation with 63. % 1.95/2.15 >>>> Starting back demodulation with 65. % 1.95/2.15 >>>> Starting back demodulation with 67. % 1.95/2.15 >>>> Starting back demodulation with 69. % 1.95/2.15 >>>> Starting back demodulation with 71. % 1.95/2.15 >>>> Starting back demodulation with 73. % 1.95/2.15 % 1.95/2.15 ======= end of input processing ======= % 1.95/2.15 % 1.95/2.15 =========== start of search =========== % 1.95/2.15 % 1.95/2.15 % 1.95/2.15 Resetting weight limit to 15. % 1.95/2.15 % 1.95/2.15 % 1.95/2.15 Resetting weight limit to 15. % 1.95/2.15 % 1.95/2.15 sos_size=58 % 1.95/2.15 % 1.95/2.15 Search stopped because sos empty. % 1.95/2.15 % 1.95/2.15 % 1.95/2.15 Search stopped because sos empty. % 1.95/2.15 % 1.95/2.15 ============ end of search ============ % 1.95/2.15 % 1.95/2.15 -------------- statistics ------------- % 1.95/2.15 clauses given 153 % 1.95/2.15 clauses generated 1800 % 1.95/2.15 clauses kept 227 % 1.95/2.15 clauses forward subsumed 568 % 1.95/2.15 clauses back subsumed 0 % 1.95/2.15 Kbytes malloced 5859 % 1.95/2.15 % 1.95/2.15 ----------- times (seconds) ----------- % 1.95/2.15 user CPU time 0.03 (0 hr, 0 min, 0 sec) % 1.95/2.15 system CPU time 0.00 (0 hr, 0 min, 0 sec) % 1.95/2.15 wall-clock time 2 (0 hr, 0 min, 2 sec) % 1.95/2.15 % 1.95/2.15 Process 12887 finished Tue May 5 12:16:30 2026 % 1.95/2.15 Otter interrupted % 1.95/2.15 PROOF NOT FOUND %------------------------------------------------------------------------------