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