%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWX187-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n016.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:22 PM UTC 2026 % Result : Unknown 1.95s 2.18s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX187-1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : otter-tptp-script %s % 0.15/0.33 % Computer : n016.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.33 % CPULimit : 300 % 0.15/0.33 % WCLimit : 300 % 0.15/0.33 % DateTime : Tue May 5 09:42:06 EDT 2026 % 0.15/0.33 % CPUTime : % 1.86/2.08 ----- Otter 3.3f, August 2004 ----- % 1.86/2.08 The process was started by sandbox on n016.cluster.edu, % 1.86/2.08 Tue May 5 09:42:06 2026 % 1.86/2.08 The command was "./otter". The process ID is 12915. % 1.86/2.08 % 1.86/2.08 set(prolog_style_variables). % 1.86/2.08 set(auto). % 1.86/2.08 dependent: set(auto1). % 1.86/2.08 dependent: set(process_input). % 1.86/2.08 dependent: clear(print_kept). % 1.86/2.08 dependent: clear(print_new_demod). % 1.86/2.08 dependent: clear(print_back_demod). % 1.86/2.08 dependent: clear(print_back_sub). % 1.86/2.08 dependent: set(control_memory). % 1.86/2.08 dependent: assign(max_mem, 12000). % 1.86/2.08 dependent: assign(pick_given_ratio, 4). % 1.86/2.08 dependent: assign(stats_level, 1). % 1.86/2.08 dependent: assign(max_seconds, 10800). % 1.86/2.08 clear(print_given). % 1.86/2.08 % 1.86/2.08 list(usable). % 1.86/2.08 0 [] A=A. % 1.86/2.08 0 [] notb(btrue)=bfalse. % 1.86/2.08 0 [] notb(bfalse)=btrue. % 1.86/2.08 0 [] length(nil)=z. % 1.86/2.08 0 [] length(cons(Y,Xs))=s(length(Xs)). % 1.86/2.08 0 [] impl(btrue,Q)=Q. % 1.86/2.08 0 [] impl(bfalse,Q)=btrue. % 1.86/2.08 0 [] x2(s(Z),s(Y2))=x2(Z,Y2). % 1.86/2.08 0 [] x2(s(Z),z)=bfalse. % 1.86/2.08 0 [] x2(z,s(X2))=btrue. % 1.86/2.08 0 [] x2(z,z)=bfalse. % 1.86/2.08 0 [] x(nil,Y)=Y. % 1.86/2.08 0 [] x(cons(Z,Xs),Y)=cons(Z,x(Xs,Y)). % 1.86/2.08 0 [] rotate(s(Z),nil)=nil. % 1.86/2.08 0 [] rotate(s(Z),cons(X2,X3))=rotate(Z,x(X3,cons(X2,nil))). % 1.86/2.08 0 [] rotate(z,Y)=Y. % 1.86/2.08 0 [] prop_rot_inj0(X,Y,Z,X2)=impl(e_q3(x2(X,length(X2)),btrue),impl(e_q3(x2(Y,length(Z)),btrue),impl(e_q(X2,Z),impl(notb(e_q(rotate(s(z),X2),X2)),impl(e_q(rotate(X,X2),rotate(Y,Z)),e_q2(X,Y)))))). % 1.86/2.08 0 [] e_q3(bfalse,btrue)=bfalse. % 1.86/2.08 0 [] e_q3(btrue,bfalse)=bfalse. % 1.86/2.08 0 [] e_q2(s(X),s(Y))=e_q2(X,Y). % 1.86/2.08 0 [] e_q2(s(X),z)=bfalse. % 1.86/2.08 0 [] e_q2(z,s(X))=bfalse. % 1.86/2.08 0 [] e_q(X,X)=btrue. % 1.86/2.08 0 [] e_q2(X,X)=btrue. % 1.86/2.08 0 [] e_q3(X,X)=btrue. % 1.86/2.08 0 [] e_q2(X,Z)!=bfalse|e_q(cons(X,Y),cons(Z,X2))=bfalse. % 1.86/2.08 0 [] e_q2(X,Z)!=btrue|e_q(cons(X,Y),cons(Z,X2))=e_q(Y,X2). % 1.86/2.08 0 [] e_q(nil,cons(X,Y))=bfalse. % 1.86/2.08 0 [] e_q(cons(X,Y),nil)=bfalse. % 1.86/2.08 0 [] e_q3(prop_rot_inj0(X,Y,Z,X2),bfalse)!=btrue. % 1.86/2.08 end_of_list. % 1.86/2.08 % 1.86/2.08 SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=2. % 1.86/2.08 % 1.86/2.08 This is a Horn set with equality. The strategy will be % 1.86/2.08 Knuth-Bendix and hyper_res, with positive clauses in % 1.86/2.08 sos and nonpositive clauses in usable. % 1.86/2.08 % 1.86/2.08 dependent: set(knuth_bendix). % 1.86/2.08 dependent: set(anl_eq). % 1.86/2.08 dependent: set(para_from). % 1.86/2.08 dependent: set(para_into). % 1.86/2.08 dependent: clear(para_from_right). % 1.86/2.08 dependent: clear(para_into_right). % 1.86/2.08 dependent: set(para_from_vars). % 1.86/2.08 dependent: set(eq_units_both_ways). % 1.86/2.08 dependent: set(dynamic_demod_all). % 1.86/2.08 dependent: set(dynamic_demod). % 1.86/2.08 dependent: set(order_eq). % 1.86/2.08 dependent: set(back_demod). % 1.86/2.08 dependent: set(lrpo). % 1.86/2.08 dependent: set(hyper_res). % 1.86/2.08 dependent: clear(order_hyper). % 1.86/2.08 % 1.86/2.08 ------------> process usable: % 1.86/2.08 ** KEPT (pick-wt=14): 1 [] e_q2(A,B)!=bfalse|e_q(cons(A,C),cons(B,D))=bfalse. % 1.86/2.08 ** KEPT (pick-wt=16): 2 [] e_q2(A,B)!=btrue|e_q(cons(A,C),cons(B,D))=e_q(C,D). % 1.86/2.08 ** KEPT (pick-wt=9): 3 [] e_q3(prop_rot_inj0(A,B,C,D),bfalse)!=btrue. % 1.86/2.08 % 1.86/2.08 ------------> process sos: % 1.86/2.08 ** KEPT (pick-wt=3): 4 [] A=A. % 1.86/2.08 ** KEPT (pick-wt=4): 5 [] notb(btrue)=bfalse. % 1.86/2.08 ---> New Demodulator: 6 [new_demod,5] notb(btrue)=bfalse. % 1.86/2.08 ** KEPT (pick-wt=4): 7 [] notb(bfalse)=btrue. % 1.86/2.08 ---> New Demodulator: 8 [new_demod,7] notb(bfalse)=btrue. % 1.86/2.08 ** KEPT (pick-wt=4): 9 [] length(nil)=z. % 1.86/2.08 ---> New Demodulator: 10 [new_demod,9] length(nil)=z. % 1.86/2.08 ** KEPT (pick-wt=8): 11 [] length(cons(A,B))=s(length(B)). % 1.86/2.08 ** KEPT (pick-wt=5): 12 [] impl(btrue,A)=A. % 1.86/2.08 ---> New Demodulator: 13 [new_demod,12] impl(btrue,A)=A. % 1.86/2.08 ** KEPT (pick-wt=5): 14 [] impl(bfalse,A)=btrue. % 1.86/2.08 ---> New Demodulator: 15 [new_demod,14] impl(bfalse,A)=btrue. % 1.86/2.08 ** KEPT (pick-wt=9): 16 [] x2(s(A),s(B))=x2(A,B). % 1.86/2.08 ---> New Demodulator: 17 [new_demod,16] x2(s(A),s(B))=x2(A,B). % 1.86/2.08 ** KEPT (pick-wt=6): 18 [] x2(s(A),z)=bfalse. % 1.86/2.08 ---> New Demodulator: 19 [new_demod,18] x2(s(A),z)=bfalse. % 1.86/2.08 ** KEPT (pick-wt=6): 20 [] x2(z,s(A))=btrue. % 1.86/2.08 ---> New Demodulator: 21 [new_demod,20] x2(z,s(A))=btrue. % 1.86/2.08 ** KEPT (pick-wt=5): 22 [] x2(z,z)=bfalse. % 1.86/2.08 ---> New Demodulator: 23 [new_demod,22] x2(z,z)=bfalse. % 1.86/2.08 ** KEPT (pick-wt=5): 24 [] x(nil,A)=A. % 1.86/2.08 ---> New Demodulator: 25 [new_demod,24] x(nil,A)=A. % 1.86/2.08 ** KEPT (pick-wt=11): 26 [] x(cons(A,B),C)=cons(A,x(B,C)). % 1.86/2.08 ---> New Demodulator: 27 [new_demod,26] x(cons(A,B),C)=cons(A,x(B,C)). % 1.86/2.08 ** KEPT (pick-wt=6): 28 [] rotate(s(A),nil)=nil. % 1.86/2.08 ---> New Demodulator: 29 [new_demod,28] rotate(s(A),nil)=nil. % 1.86/2.08 ** KEPT (pick-wt=14): 30 [] rotate(s(A),cons(B,C))=rotate(A,x(C,cons(B,nil))). % 1.95/2.18 ** KEPT (pick-wt=5): 31 [] rotate(z,A)=A. % 1.95/2.18 ---> New Demodulator: 32 [new_demod,31] rotate(z,A)=A. % 1.95/2.18 ** KEPT (pick-wt=43): 34 [copy,33,flip.1] impl(e_q3(x2(A,length(B)),btrue),impl(e_q3(x2(C,length(D)),btrue),impl(e_q(B,D),impl(notb(e_q(rotate(s(z),B),B)),impl(e_q(rotate(A,B),rotate(C,D)),e_q2(A,C))))))=prop_rot_inj0(A,C,D,B). % 1.95/2.18 ---> New Demodulator: 35 [new_demod,34] impl(e_q3(x2(A,length(B)),btrue),impl(e_q3(x2(C,length(D)),btrue),impl(e_q(B,D),impl(notb(e_q(rotate(s(z),B),B)),impl(e_q(rotate(A,B),rotate(C,D)),e_q2(A,C))))))=prop_rot_inj0(A,C,D,B). % 1.95/2.18 ** KEPT (pick-wt=5): 36 [] e_q3(bfalse,btrue)=bfalse. % 1.95/2.18 ---> New Demodulator: 37 [new_demod,36] e_q3(bfalse,btrue)=bfalse. % 1.95/2.18 ** KEPT (pick-wt=5): 38 [] e_q3(btrue,bfalse)=bfalse. % 1.95/2.18 ---> New Demodulator: 39 [new_demod,38] e_q3(btrue,bfalse)=bfalse. % 1.95/2.18 ** KEPT (pick-wt=9): 40 [] e_q2(s(A),s(B))=e_q2(A,B). % 1.95/2.18 ---> New Demodulator: 41 [new_demod,40] e_q2(s(A),s(B))=e_q2(A,B). % 1.95/2.18 ** KEPT (pick-wt=6): 42 [] e_q2(s(A),z)=bfalse. % 1.95/2.18 ---> New Demodulator: 43 [new_demod,42] e_q2(s(A),z)=bfalse. % 1.95/2.18 ** KEPT (pick-wt=6): 44 [] e_q2(z,s(A))=bfalse. % 1.95/2.18 ---> New Demodulator: 45 [new_demod,44] e_q2(z,s(A))=bfalse. % 1.95/2.18 ** KEPT (pick-wt=5): 46 [] e_q(A,A)=btrue. % 1.95/2.18 ---> New Demodulator: 47 [new_demod,46] e_q(A,A)=btrue. % 1.95/2.18 ** KEPT (pick-wt=5): 48 [] e_q2(A,A)=btrue. % 1.95/2.18 ---> New Demodulator: 49 [new_demod,48] e_q2(A,A)=btrue. % 1.95/2.18 ** KEPT (pick-wt=5): 50 [] e_q3(A,A)=btrue. % 1.95/2.18 ---> New Demodulator: 51 [new_demod,50] e_q3(A,A)=btrue. % 1.95/2.18 ** KEPT (pick-wt=7): 52 [] e_q(nil,cons(A,B))=bfalse. % 1.95/2.18 ---> New Demodulator: 53 [new_demod,52] e_q(nil,cons(A,B))=bfalse. % 1.95/2.18 ** KEPT (pick-wt=7): 54 [] e_q(cons(A,B),nil)=bfalse. % 1.95/2.18 ---> New Demodulator: 55 [new_demod,54] e_q(cons(A,B),nil)=bfalse. % 1.95/2.18 Following clause subsumed by 4 during input processing: 0 [copy,4,flip.1] A=A. % 1.95/2.18 >>>> Starting back demodulation with 6. % 1.95/2.18 >>>> Starting back demodulation with 8. % 1.95/2.18 >>>> Starting back demodulation with 10. % 1.95/2.18 ** KEPT (pick-wt=8): 56 [copy,11,flip.1] s(length(A))=length(cons(B,A)). % 1.95/2.18 >>>> Starting back demodulation with 13. % 1.95/2.18 >>>> Starting back demodulation with 15. % 1.95/2.18 >>>> Starting back demodulation with 17. % 1.95/2.18 >>>> Starting back demodulation with 19. % 1.95/2.18 >>>> Starting back demodulation with 21. % 1.95/2.18 >>>> Starting back demodulation with 23. % 1.95/2.18 >>>> Starting back demodulation with 25. % 1.95/2.18 >>>> Starting back demodulation with 27. % 1.95/2.18 >>>> Starting back demodulation with 29. % 1.95/2.18 ** KEPT (pick-wt=14): 57 [copy,30,flip.1] rotate(A,x(B,cons(C,nil)))=rotate(s(A),cons(C,B)). % 1.95/2.18 >>>> Starting back demodulation with 32. % 1.95/2.18 >>>> Starting back demodulation with 35. % 1.95/2.18 >>>> Starting back demodulation with 37. % 1.95/2.18 >>>> Starting back demodulation with 39. % 1.95/2.18 >>>> Starting back demodulation with 41. % 1.95/2.18 >>>> Starting back demodulation with 43. % 1.95/2.18 >>>> Starting back demodulation with 45. % 1.95/2.18 >>>> Starting back demodulation with 47. % 1.95/2.18 >>>> Starting back demodulation with 49. % 1.95/2.18 >>>> Starting back demodulation with 51. % 1.95/2.18 >>>> Starting back demodulation with 53. % 1.95/2.18 >>>> Starting back demodulation with 55. % 1.95/2.18 Following clause subsumed by 11 during input processing: 0 [copy,56,flip.1] length(cons(A,B))=s(length(B)). % 1.95/2.18 Following clause subsumed by 30 during input processing: 0 [copy,57,flip.1] rotate(s(A),cons(B,C))=rotate(A,x(C,cons(B,nil))). % 1.95/2.18 % 1.95/2.18 ======= end of input processing ======= % 1.95/2.18 % 1.95/2.18 =========== start of search =========== % 1.95/2.18 % 1.95/2.18 % 1.95/2.18 Resetting weight limit to 11. % 1.95/2.18 % 1.95/2.18 % 1.95/2.18 Resetting weight limit to 11. % 1.95/2.18 % 1.95/2.18 sos_size=93 % 1.95/2.18 % 1.95/2.18 Search stopped because sos empty. % 1.95/2.18 % 1.95/2.18 % 1.95/2.18 Search stopped because sos empty. % 1.95/2.18 % 1.95/2.18 ============ end of search ============ % 1.95/2.18 % 1.95/2.18 -------------- statistics ------------- % 1.95/2.18 clauses given 152 % 1.95/2.18 clauses generated 5179 % 1.95/2.18 clauses kept 163 % 1.95/2.18 clauses forward subsumed 848 % 1.95/2.18 clauses back subsumed 6 % 1.95/2.18 Kbytes malloced 6835 % 1.95/2.18 % 1.95/2.18 ----------- times (seconds) ----------- % 1.95/2.18 user CPU time 0.10 (0 hr, 0 min, 0 sec) % 1.95/2.18 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 1.95/2.18 wall-clock time 2 (0 hr, 0 min, 2 sec) % 1.95/2.18 % 1.95/2.18 Process 12915 finished Tue May 5 09:42:08 2026 % 1.95/2.18 Otter interrupted % 1.95/2.18 PROOF NOT FOUND %------------------------------------------------------------------------------