%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWX201-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n024.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:24 PM UTC 2026 % Result : Unknown 1.16s 1.51s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.06 % Problem : SWX201-1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.06 % Command : otter-tptp-script %s % 0.07/0.24 % Computer : n024.cluster.edu % 0.07/0.24 % Model : x86_64 x86_64 % 0.07/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.24 % Memory : 8042.1875MB % 0.07/0.24 % OS : Linux 3.10.0-693.el7.x86_64 % 0.07/0.24 % CPULimit : 300 % 0.07/0.24 % WCLimit : 300 % 0.07/0.24 % DateTime : Tue May 5 06:18:56 EDT 2026 % 0.07/0.25 % CPUTime : % 0.88/1.49 ----- Otter 3.3f, August 2004 ----- % 0.88/1.49 The process was started by sandbox on n024.cluster.edu, % 0.88/1.49 Tue May 5 06:18:56 2026 % 0.88/1.49 The command was "./otter". The process ID is 21959. % 0.88/1.49 % 0.88/1.49 set(prolog_style_variables). % 0.88/1.49 set(auto). % 0.88/1.49 dependent: set(auto1). % 0.88/1.49 dependent: set(process_input). % 0.88/1.49 dependent: clear(print_kept). % 0.88/1.49 dependent: clear(print_new_demod). % 0.88/1.49 dependent: clear(print_back_demod). % 0.88/1.49 dependent: clear(print_back_sub). % 0.88/1.49 dependent: set(control_memory). % 0.88/1.49 dependent: assign(max_mem, 12000). % 0.88/1.49 dependent: assign(pick_given_ratio, 4). % 0.88/1.49 dependent: assign(stats_level, 1). % 0.88/1.49 dependent: assign(max_seconds, 10800). % 0.88/1.49 clear(print_given). % 0.88/1.49 % 0.88/1.49 list(usable). % 0.88/1.49 0 [] A=A. % 0.88/1.49 0 [] aux(Z,X2,X3,pair2(Ys1,Zs))=pair2(cons(X2,Ys1),Zs). % 0.88/1.49 0 [] aux2(Z,Xs,Y2,Ys,btrue)=cons(Z,merge(Xs,cons(Y2,Ys))). % 0.88/1.49 0 [] aux2(Z,Xs,Y2,Ys,bfalse)=cons(Y2,merge(cons(Z,Xs),Ys)). % 0.88/1.49 0 [] aux3(Y,X2,X3,pair2(Ys1,Zs))=merge(msort(Ys1),msort(Zs)). % 0.88/1.49 0 [] aux4(X,Z,Xs,btrue)=s(count(X,Xs)). % 0.88/1.49 0 [] aux4(X,Z,Xs,bfalse)=count(X,Xs). % 0.88/1.49 0 [] splitAtNat(z,Y)=pair2(nil,Y). % 0.88/1.49 0 [] splitAtNat(s(Z),nil)=pair2(nil,nil). % 0.88/1.49 0 [] splitAtNat(s(Z),cons(X2,X3))=aux(Z,X2,X3,splitAtNat(Z,X3)). % 0.88/1.49 0 [] le_qNat(z,Y)=btrue. % 0.88/1.49 0 [] le_qNat(s(Z),z)=bfalse. % 0.88/1.49 0 [] le_qNat(s(Z),s(M))=le_qNat(Z,M). % 0.88/1.49 0 [] merge(nil,Y)=Y. % 0.88/1.49 0 [] merge(cons(Z,Xs),nil)=cons(Z,Xs). % 0.88/1.49 0 [] merge(cons(Z,Xs),cons(Y2,Ys))=aux2(Z,Xs,Y2,Ys,le_qNat(Z,Y2)). % 0.88/1.49 0 [] lengthNat(nil)=z. % 0.88/1.49 0 [] lengthNat(cons(Y,Xs))=s(lengthNat(Xs)). % 0.88/1.49 0 [] impl(btrue,Q)=Q. % 0.88/1.49 0 [] impl(bfalse,Q)=btrue. % 0.88/1.49 0 [] div2(z)=z. % 0.88/1.49 0 [] div2(s(z))=z. % 0.88/1.49 0 [] div2(s(s(N)))=s(div2(N)). % 0.88/1.49 0 [] msort(nil)=nil. % 0.88/1.49 0 [] msort(cons(Y,nil))=cons(Y,nil). % 0.88/1.49 0 [] msort(cons(Y,cons(X2,X3)))=aux3(Y,X2,X3,splitAtNat(div2(lengthNat(cons(Y,cons(X2,X3)))),cons(Y,cons(X2,X3)))). % 0.88/1.49 0 [] count(X,nil)=z. % 0.88/1.49 0 [] count(X,cons(Z,Xs))=aux4(X,Z,Xs,e_q(Z,X)). % 0.88/1.49 0 [] prop_msort_permutation_wrong1(X,Y)=impl(e_q2(le_qNat(count(Y,X),s(s(s(s(s(z)))))),bfalse),e_q(count(Y,X),count(s(Y),msort(X)))). % 0.88/1.49 0 [] e_q2(bfalse,btrue)=bfalse. % 0.88/1.49 0 [] e_q2(btrue,bfalse)=bfalse. % 0.88/1.49 0 [] e_q(s(X),s(Y))=e_q(X,Y). % 0.88/1.49 0 [] e_q(z,s(X))=bfalse. % 0.88/1.49 0 [] e_q(s(X),z)=bfalse. % 0.88/1.49 0 [] e_q(X,X)=btrue. % 0.88/1.49 0 [] e_q2(X,X)=btrue. % 0.88/1.49 0 [] e_q2(prop_msort_permutation_wrong1(X,Y),bfalse)!=btrue. % 0.88/1.49 end_of_list. % 0.88/1.49 % 0.88/1.49 SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=1. % 0.88/1.49 % 0.88/1.49 All clauses are units, and equality is present; the % 0.88/1.49 strategy will be Knuth-Bendix with positive clauses in sos. % 0.88/1.49 % 0.88/1.49 dependent: set(knuth_bendix). % 0.88/1.49 dependent: set(anl_eq). % 0.88/1.49 dependent: set(para_from). % 0.88/1.49 dependent: set(para_into). % 0.88/1.49 dependent: clear(para_from_right). % 0.88/1.49 dependent: clear(para_into_right). % 0.88/1.49 dependent: set(para_from_vars). % 0.88/1.49 dependent: set(eq_units_both_ways). % 0.88/1.49 dependent: set(dynamic_demod_all). % 0.88/1.49 dependent: set(dynamic_demod). % 0.88/1.49 dependent: set(order_eq). % 0.88/1.49 dependent: set(back_demod). % 0.88/1.49 dependent: set(lrpo). % 0.88/1.49 % 0.88/1.49 ------------> process usable: % 0.88/1.49 ** KEPT (pick-wt=7): 1 [] e_q2(prop_msort_permutation_wrong1(A,B),bfalse)!=btrue. % 0.88/1.49 % 0.88/1.49 ------------> process sos: % 0.88/1.49 ** KEPT (pick-wt=3): 2 [] A=A. % 0.88/1.49 ** KEPT (pick-wt=13): 3 [] aux(A,B,C,pair2(D,E))=pair2(cons(B,D),E). % 0.88/1.49 ** KEPT (pick-wt=14): 5 [copy,4,flip.1] cons(A,merge(B,cons(C,D)))=aux2(A,B,C,D,btrue). % 0.88/1.49 ---> New Demodulator: 6 [new_demod,5] cons(A,merge(B,cons(C,D)))=aux2(A,B,C,D,btrue). % 0.88/1.49 ** KEPT (pick-wt=14): 8 [copy,7,flip.1] cons(A,merge(cons(B,C),D))=aux2(B,C,A,D,bfalse). % 0.88/1.49 ---> New Demodulator: 9 [new_demod,8] cons(A,merge(cons(B,C),D))=aux2(B,C,A,D,bfalse). % 0.88/1.49 ** KEPT (pick-wt=13): 10 [] aux3(A,B,C,pair2(D,E))=merge(msort(D),msort(E)). % 0.88/1.49 ** KEPT (pick-wt=10): 11 [] aux4(A,B,C,btrue)=s(count(A,C)). % 0.88/1.49 ** KEPT (pick-wt=9): 12 [] aux4(A,B,C,bfalse)=count(A,C). % 0.88/1.49 ** KEPT (pick-wt=7): 13 [] splitAtNat(z,A)=pair2(nil,A). % 0.88/1.49 ---> New Demodulator: 14 [new_demod,13] splitAtNat(z,A)=pair2(nil,A). % 0.88/1.49 ** KEPT (pick-wt=8): 15 [] splitAtNat(s(A),nil)=pair2(nil,nil). % 0.88/1.49 ---> New Demodulator: 16 [new_demod,15] splitAtNat(s(A),nil)=pair2(nil,nil). % 0.88/1.49 ** KEPT (pick-wt=14): 17 [] splitAtNat(s(A),cons(B,C))=aux(A,B,C,splitAtNat(A,C)). % 0.88/1.49 ---> New Demodulator: 18 [new_demod,17] splitAtNat(s(A),cons(B,C))=aux(A,B,C,splitAtNat(A,C)). % 0.88/1.49 ** KEPT (pick-wt=5): 19 [] le_qNat(z,A)=btrue. % 0.88/1.49 ---> New Demodulator: 20 [new_demod,19] le_qNat(z,A)=btrue. % 0.88/1.49 ** KEPT (pick-wt=6): 21 [] le_qNat(s(A),z)=bfalse. % 0.88/1.49 ---> New Demodulator: 22 [new_demod,21] le_qNat(s(A),z)=bfalse. % 0.88/1.49 ** KEPT (pick-wt=9): 23 [] le_qNat(s(A),s(B))=le_qNat(A,B). % 0.88/1.49 ---> New Demodulator: 24 [new_demod,23] le_qNat(s(A),s(B))=le_qNat(A,B). % 0.88/1.49 ** KEPT (pick-wt=5): 25 [] merge(nil,A)=A. % 0.88/1.49 ---> New Demodulator: 26 [new_demod,25] merge(nil,A)=A. % 0.88/1.49 ** KEPT (pick-wt=9): 27 [] merge(cons(A,B),nil)=cons(A,B). % 0.88/1.49 ---> New Demodulator: 28 [new_demod,27] merge(cons(A,B),nil)=cons(A,B). % 0.88/1.49 ** KEPT (pick-wt=16): 29 [] merge(cons(A,B),cons(C,D))=aux2(A,B,C,D,le_qNat(A,C)). % 0.88/1.49 ---> New Demodulator: 30 [new_demod,29] merge(cons(A,B),cons(C,D))=aux2(A,B,C,D,le_qNat(A,C)). % 0.88/1.49 ** KEPT (pick-wt=4): 31 [] lengthNat(nil)=z. % 0.88/1.49 ---> New Demodulator: 32 [new_demod,31] lengthNat(nil)=z. % 0.88/1.49 ** KEPT (pick-wt=8): 33 [] lengthNat(cons(A,B))=s(lengthNat(B)). % 0.88/1.49 ** KEPT (pick-wt=5): 34 [] impl(btrue,A)=A. % 0.88/1.49 ---> New Demodulator: 35 [new_demod,34] impl(btrue,A)=A. % 0.88/1.49 ** KEPT (pick-wt=5): 36 [] impl(bfalse,A)=btrue. % 0.88/1.49 ---> New Demodulator: 37 [new_demod,36] impl(bfalse,A)=btrue. % 0.88/1.49 ** KEPT (pick-wt=4): 38 [] div2(z)=z. % 0.88/1.49 ---> New Demodulator: 39 [new_demod,38] div2(z)=z. % 0.88/1.49 ** KEPT (pick-wt=5): 40 [] div2(s(z))=z. % 0.88/1.49 ---> New Demodulator: 41 [new_demod,40] div2(s(z))=z. % 0.88/1.49 ** KEPT (pick-wt=8): 42 [] div2(s(s(A)))=s(div2(A)). % 0.88/1.49 ---> New Demodulator: 43 [new_demod,42] div2(s(s(A)))=s(div2(A)). % 0.88/1.49 ** KEPT (pick-wt=4): 44 [] msort(nil)=nil. % 0.88/1.49 ---> New Demodulator: 45 [new_demod,44] msort(nil)=nil. % 0.88/1.49 ** KEPT (pick-wt=8): 46 [] msort(cons(A,nil))=cons(A,nil). % 0.88/1.49 ---> New Demodulator: 47 [new_demod,46] msort(cons(A,nil))=cons(A,nil). % 0.88/1.49 ** KEPT (pick-wt=24): 48 [] msort(cons(A,cons(B,C)))=aux3(A,B,C,splitAtNat(div2(lengthNat(cons(A,cons(B,C)))),cons(A,cons(B,C)))). % 0.88/1.49 ---> New Demodulator: 49 [new_demod,48] msort(cons(A,cons(B,C)))=aux3(A,B,C,splitAtNat(div2(lengthNat(cons(A,cons(B,C)))),cons(A,cons(B,C)))). % 0.88/1.49 ** KEPT (pick-wt=5): 50 [] count(A,nil)=z. % 0.88/1.49 ---> New Demodulator: 51 [new_demod,50] count(A,nil)=z. % 0.88/1.49 ** KEPT (pick-wt=13): 52 [] count(A,cons(B,C))=aux4(A,B,C,e_q(B,A)). % 0.88/1.49 ** KEPT (pick-wt=26): 53 [] prop_msort_permutation_wrong1(A,B)=impl(e_q2(le_qNat(count(B,A),s(s(s(s(s(z)))))),bfalse),e_q(count(B,A),count(s(B),msort(A)))). % 0.88/1.49 ** KEPT (pick-wt=5): 54 [] e_q2(bfalse,btrue)=bfalse. % 0.88/1.49 ---> New Demodulator: 55 [new_demod,54] e_q2(bfalse,btrue)=bfalse. % 0.88/1.49 ** KEPT (pick-wt=5): 56 [] e_q2(btrue,bfalse)=bfalse. % 0.88/1.49 ---> New Demodulator: 57 [new_demod,56] e_q2(btrue,bfalse)=bfalse. % 0.88/1.49 ** KEPT (pick-wt=9): 58 [] e_q(s(A),s(B))=e_q(A,B). % 0.88/1.49 ---> New Demodulator: 59 [new_demod,58] e_q(s(A),s(B))=e_q(A,B). % 0.88/1.49 ** KEPT (pick-wt=6): 60 [] e_q(z,s(A))=bfalse. % 0.88/1.49 ---> New Demodulator: 61 [new_demod,60] e_q(z,s(A))=bfalse. % 0.88/1.49 ** KEPT (pick-wt=6): 62 [] e_q(s(A),z)=bfalse. % 0.88/1.49 ---> New Demodulator: 63 [new_demod,62] e_q(s(A),z)=bfalse. % 0.88/1.49 ** KEPT (pick-wt=5): 64 [] e_q(A,A)=btrue. % 0.88/1.49 ---> New Demodulator: 65 [new_demod,64] e_q(A,A)=btrue. % 0.88/1.49 ** KEPT (pick-wt=5): 66 [] e_q2(A,A)=btrue. % 0.88/1.49 ---> New Demodulator: 67 [new_demod,66] e_q2(A,A)=btrue. % 0.88/1.49 Following clause subsumed by 2 during input processing: 0 [copy,2,flip.1] A=A. % 0.88/1.49 ** KEPT (pick-wt=13): 68 [copy,3,flip.1] pair2(cons(A,B),C)=aux(D,A,E,pair2(B,C)). % 0.88/1.49 >>>> Starting back demodulation with 6. % 0.88/1.49 >>>> Starting back demodulation with 9. % 0.88/1.49 ** KEPT (pick-wt=13): 69 [copy,10,flip.1] merge(msort(A),msort(B))=aux3(C,D,E,pair2(A,B)). % 0.88/1.49 ** KEPT (pick-wt=10): 70 [copy,11,flip.1] s(count(A,B))=aux4(A,C,B,btrue). % 0.88/1.49 ** KEPT (pick-wt=9): 71 [copy,12,flip.1] count(A,B)=aux4(A,C,B,bfalse). % 0.88/1.49 >>>> Starting back demodulation with 14. % 0.88/1.49 >>>> Starting back demodulation with 16. % 0.88/1.49 >>>> Starting back demodulation with 18. % 0.88/1.49 >>>> Starting back demodulation with 20. % 0.88/1.49 >>>> Starting back demodulation with 22. % 0.88/1.49 >>>> Starting back demodulation with 24. % 0.88/1.49 >>>> Starting back demodulation with 26. % 0.88/1.49 >>>> Starting back demodulation with 28. % 0.88/1.49 >>>> Starting back demodulation with 30. % 0.88/1.49 >>>> Starting back demodulation with 32. % 0.88/1.49 ** KEPT (pick-wt=8): 72 [copy,33,flip.1] s(lengthNat(A))=lengthNat(cons(B,A)). % 0.88/1.49 >>>> Starting back demodulation with 35. % 0.88/1.49 >>>> Starting back demodulation with 37. % 0.88/1.49 >>>> Starting back demodulation with 39. % 0.88/1.49 >>>> Starting back demodulation with 41. % 0.88/1.49 >>>> Starting back demodulation with 43. % 1.16/1.51 >>>> Starting back demodulation with 45. % 1.16/1.51 >>>> Starting back demodulation with 47. % 1.16/1.51 >>>> Starting back demodulation with 49. % 1.16/1.51 >>>> Starting back demodulation with 51. % 1.16/1.51 ** KEPT (pick-wt=13): 73 [copy,52,flip.1] aux4(A,B,C,e_q(B,A))=count(A,cons(B,C)). % 1.16/1.51 ** KEPT (pick-wt=26): 74 [copy,53,flip.1] impl(e_q2(le_qNat(count(A,B),s(s(s(s(s(z)))))),bfalse),e_q(count(A,B),count(s(A),msort(B))))=prop_msort_permutation_wrong1(B,A). % 1.16/1.51 >>>> Starting back demodulation with 55. % 1.16/1.51 >>>> Starting back demodulation with 57. % 1.16/1.51 >>>> Starting back demodulation with 59. % 1.16/1.51 >>>> Starting back demodulation with 61. % 1.16/1.51 >>>> Starting back demodulation with 63. % 1.16/1.51 >>>> Starting back demodulation with 65. % 1.16/1.51 >>>> Starting back demodulation with 67. % 1.16/1.51 Following clause subsumed by 3 during input processing: 0 [copy,68,flip.1] aux(A,B,C,pair2(D,E))=pair2(cons(B,D),E). % 1.16/1.51 Following clause subsumed by 10 during input processing: 0 [copy,69,flip.1] aux3(A,B,C,pair2(D,E))=merge(msort(D),msort(E)). % 1.16/1.51 Following clause subsumed by 11 during input processing: 0 [copy,70,flip.1] aux4(A,B,C,btrue)=s(count(A,C)). % 1.16/1.51 Following clause subsumed by 12 during input processing: 0 [copy,71,flip.1] aux4(A,B,C,bfalse)=count(A,C). % 1.16/1.51 Following clause subsumed by 33 during input processing: 0 [copy,72,flip.1] lengthNat(cons(A,B))=s(lengthNat(B)). % 1.16/1.51 Following clause subsumed by 52 during input processing: 0 [copy,73,flip.1] count(A,cons(B,C))=aux4(A,B,C,e_q(B,A)). % 1.16/1.51 Following clause subsumed by 53 during input processing: 0 [copy,74,flip.1] prop_msort_permutation_wrong1(A,B)=impl(e_q2(le_qNat(count(B,A),s(s(s(s(s(z)))))),bfalse),e_q(count(B,A),count(s(B),msort(A)))). % 1.16/1.51 % 1.16/1.51 ======= end of input processing ======= % 1.16/1.51 % 1.16/1.51 =========== start of search =========== % 1.16/1.51 % 1.16/1.51 % 1.16/1.51 Resetting weight limit to 11. % 1.16/1.51 % 1.16/1.51 % 1.16/1.51 Resetting weight limit to 11. % 1.16/1.51 % 1.16/1.51 sos_size=115 % 1.16/1.51 % 1.16/1.51 Search stopped because sos empty. % 1.16/1.51 % 1.16/1.51 % 1.16/1.51 Search stopped because sos empty. % 1.16/1.51 % 1.16/1.51 ============ end of search ============ % 1.16/1.51 % 1.16/1.51 -------------- statistics ------------- % 1.16/1.51 clauses given 210 % 1.16/1.51 clauses generated 3405 % 1.16/1.51 clauses kept 219 % 1.16/1.51 clauses forward subsumed 1025 % 1.16/1.51 clauses back subsumed 0 % 1.16/1.51 Kbytes malloced 6835 % 1.16/1.51 % 1.16/1.51 ----------- times (seconds) ----------- % 1.16/1.51 user CPU time 0.02 (0 hr, 0 min, 0 sec) % 1.16/1.51 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 1.16/1.51 wall-clock time 1 (0 hr, 0 min, 1 sec) % 1.16/1.51 % 1.16/1.51 Process 21959 finished Tue May 5 06:18:57 2026 % 1.16/1.51 Otter interrupted % 1.16/1.51 PROOF NOT FOUND %------------------------------------------------------------------------------