%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWX192-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n031.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:23 PM UTC 2026 % Result : Unknown 2.51s 2.60s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX192-1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : otter-tptp-script %s % 0.15/0.33 % Computer : n031.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 10:14:38 EDT 2026 % 0.15/0.34 % CPUTime : % 1.92/2.58 ----- Otter 3.3f, August 2004 ----- % 1.92/2.58 The process was started by sandbox2 on n031.cluster.edu, % 1.92/2.58 Tue May 5 10:14:39 2026 % 1.92/2.58 The command was "./otter". The process ID is 16073. % 1.92/2.58 % 1.92/2.58 set(prolog_style_variables). % 1.92/2.58 set(auto). % 1.92/2.58 dependent: set(auto1). % 1.92/2.58 dependent: set(process_input). % 1.92/2.58 dependent: clear(print_kept). % 1.92/2.58 dependent: clear(print_new_demod). % 1.92/2.58 dependent: clear(print_back_demod). % 1.92/2.58 dependent: clear(print_back_sub). % 1.92/2.58 dependent: set(control_memory). % 1.92/2.58 dependent: assign(max_mem, 12000). % 1.92/2.58 dependent: assign(pick_given_ratio, 4). % 1.92/2.58 dependent: assign(stats_level, 1). % 1.92/2.58 dependent: assign(max_seconds, 10800). % 1.92/2.58 clear(print_given). % 1.92/2.58 % 1.92/2.58 list(usable). % 1.92/2.58 0 [] A=A. % 1.92/2.58 0 [] aux(Y,E,btrue)=y(n(s(s(z))),opt(Y)). % 1.92/2.58 0 [] aux(x(B,C),E,bfalse)=opt(x(B,x(C,E))). % 1.92/2.58 0 [] aux(n(X),E,bfalse)=x(opt(n(X)),opt(E)). % 1.92/2.58 0 [] aux(y(X,X2),E,bfalse)=x(opt(y(X,X2)),opt(E)). % 1.92/2.58 0 [] aux(x2,E,bfalse)=x(opt(x2),opt(E)). % 1.92/2.58 0 [] fail2(Y,E)=aux(Y,E,e_q2(Y,E)). % 1.92/2.58 0 [] fail1(n(A2),n(B2))=n(addNat(A2,B2)). % 1.92/2.58 0 [] fail1(n(A2),x(X,X2))=fail2(n(A2),x(X,X2)). % 1.92/2.58 0 [] fail1(n(A2),y(X,X2))=fail2(n(A2),y(X,X2)). % 1.92/2.58 0 [] fail1(n(A2),x2)=fail2(n(A2),x2). % 1.92/2.58 0 [] fail1(x(X,X2),E)=fail2(x(X,X2),E). % 1.92/2.58 0 [] fail1(y(X,X2),E)=fail2(y(X,X2),E). % 1.92/2.58 0 [] fail1(x2,E)=fail2(x2,E). % 1.92/2.58 0 [] fail(Y,n(s(X2)))=fail1(Y,n(s(X2))). % 1.92/2.58 0 [] fail(Y,n(z))=Y. % 1.92/2.58 0 [] fail(Y,x(X,X2))=fail1(Y,x(X,X2)). % 1.92/2.58 0 [] fail(Y,y(X,X2))=fail1(Y,y(X,X2)). % 1.92/2.58 0 [] fail(Y,x2)=fail1(Y,x2). % 1.92/2.58 0 [] fail4(X5,E2)=y(opt(X5),opt(E2)). % 1.92/2.58 0 [] fail32(n(A3),n(B3))=n(mulNat(A3,B3)). % 1.92/2.58 0 [] fail32(n(A3),x(X,X2))=fail4(n(A3),x(X,X2)). % 1.92/2.58 0 [] fail32(n(A3),y(X,X2))=fail4(n(A3),y(X,X2)). % 1.92/2.58 0 [] fail32(n(A3),x2)=fail4(n(A3),x2). % 1.92/2.58 0 [] fail32(y(A4,B4),E2)=opt(y(A4,y(B4,E2))). % 1.92/2.58 0 [] fail32(x(X,X2),E2)=fail4(x(X,X2),E2). % 1.92/2.58 0 [] fail32(x2,E2)=fail4(x2,E2). % 1.92/2.58 0 [] fail22(X5,n(s(s(X8))))=fail32(X5,n(s(s(X8)))). % 1.92/2.58 0 [] fail22(X5,n(s(z)))=X5. % 1.92/2.58 0 [] fail22(X5,n(z))=fail32(X5,n(z)). % 1.92/2.58 0 [] fail22(X5,x(X,X2))=fail32(X5,x(X,X2)). % 1.92/2.58 0 [] fail22(X5,y(X,X2))=fail32(X5,y(X,X2)). % 1.92/2.58 0 [] fail22(X5,x2)=fail32(X5,x2). % 1.92/2.58 0 [] fail12(n(s(s(X11))),E2)=fail22(n(s(s(X11))),E2). % 1.92/2.58 0 [] fail12(n(s(z)),E2)=E2. % 1.92/2.58 0 [] fail12(n(z),E2)=fail22(n(z),E2). % 1.92/2.58 0 [] fail12(x(X,X2),E2)=fail22(x(X,X2),E2). % 1.92/2.58 0 [] fail12(y(X,X2),E2)=fail22(y(X,X2),E2). % 1.92/2.58 0 [] fail12(x2,E2)=fail22(x2,E2). % 1.92/2.58 0 [] fail3(X5,n(s(X13)))=fail12(X5,n(s(X13))). % 1.92/2.58 0 [] fail3(X5,n(z))=n(z). % 1.92/2.58 0 [] fail3(X5,x(X,X2))=fail12(X5,x(X,X2)). % 1.92/2.58 0 [] fail3(X5,y(X,X2))=fail12(X5,y(X,X2)). % 1.92/2.58 0 [] fail3(X5,x2)=fail12(X5,x2). % 1.92/2.58 0 [] impl(btrue,Q)=Q. % 1.92/2.58 0 [] impl(bfalse,Q)=btrue. % 1.92/2.58 0 [] d(n(Y))=n(z). % 1.92/2.58 0 [] d(x(F,G))=x(d(F),d(G)). % 1.92/2.58 0 [] d(y(H,G2))=x(y(d(H),G2),y(H,d(G2))). % 1.92/2.58 0 [] d(x2)=n(s(z)). % 1.92/2.58 0 [] addNat(s(Z),Y)=s(addNat(Z,Y)). % 1.92/2.58 0 [] addNat(z,Y)=Y. % 1.92/2.58 0 [] mulNat(s(Z),Y)=addNat(Y,mulNat(Z,Y)). % 1.92/2.58 0 [] mulNat(z,Y)=z. % 1.92/2.58 0 [] opt(x(n(s(X4)),E))=fail(n(s(X4)),E). % 1.92/2.58 0 [] opt(x(n(z),E))=E. % 1.92/2.58 0 [] opt(x(x(X,X2),E))=fail(x(X,X2),E). % 1.92/2.58 0 [] opt(x(y(X,X2),E))=fail(y(X,X2),E). % 1.92/2.58 0 [] opt(x(x2,E))=fail(x2,E). % 1.92/2.58 0 [] opt(y(n(s(X15)),E2))=fail3(n(s(X15)),E2). % 1.92/2.58 0 [] opt(y(n(z),E2))=n(z). % 1.92/2.58 0 [] opt(y(x(X,X2),E2))=fail3(x(X,X2),E2). % 1.92/2.58 0 [] opt(y(y(X,X2),E2))=fail3(y(X,X2),E2). % 1.92/2.58 0 [] opt(y(x2,E2))=fail3(x2,E2). % 1.92/2.58 0 [] opt(n(X))=n(X). % 1.92/2.58 0 [] opt(x2)=x2. % 1.92/2.58 0 [] propm5(X)=impl(e_q2(opt(d(X)),x(y(x2,y(x2,y(x2,x2))),y(x2,x(y(x2,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2)))))))),e_q3(btrue,bfalse)). % 1.92/2.58 0 [] e_q3(bfalse,btrue)=bfalse. % 1.92/2.58 0 [] e_q3(btrue,bfalse)=bfalse. % 1.92/2.58 0 [] e_q2(n(X),n(Y))=e_q(X,Y). % 1.92/2.58 0 [] e_q2(X,Z)!=bfalse|e_q2(x(X,Y),x(Z,X2))=bfalse. % 1.92/2.58 0 [] e_q2(X,Z)!=btrue|e_q2(x(X,Y),x(Z,X2))=e_q2(Y,X2). % 1.92/2.58 0 [] e_q2(X,Z)!=bfalse|e_q2(y(X,Y),y(Z,X2))=bfalse. % 1.92/2.58 0 [] e_q2(X,Z)!=btrue|e_q2(y(X,Y),y(Z,X2))=e_q2(Y,X2). % 1.92/2.58 0 [] e_q2(n(X),x(Y,Z))=bfalse. % 1.92/2.58 0 [] e_q2(n(X),y(Y,Z))=bfalse. % 1.92/2.58 0 [] e_q2(n(X),x2)=bfalse. % 1.92/2.58 0 [] e_q2(x(X,Y),n(Z))=bfalse. % 1.92/2.58 0 [] e_q2(x(X,Y),y(Z,X2))=bfalse. % 1.92/2.58 0 [] e_q2(x(X,Y),x2)=bfalse. % 1.92/2.58 0 [] e_q2(y(X,Y),n(Z))=bfalse. % 1.92/2.58 0 [] e_q2(y(X,Y),x(Z,X2))=bfalse. % 1.92/2.58 0 [] e_q2(y(X,Y),x2)=bfalse. % 1.92/2.58 0 [] e_q2(x2,n(X))=bfalse. % 1.92/2.58 0 [] e_q2(x2,x(X,Y))=bfalse. % 1.92/2.58 0 [] e_q2(x2,y(X,Y))=bfalse. % 1.92/2.58 0 [] e_q(s(X),s(Y))=e_q(X,Y). % 1.92/2.58 0 [] e_q(s(X),z)=bfalse. % 1.92/2.58 0 [] e_q(z,s(X))=bfalse. % 1.92/2.58 0 [] e_q(X,X)=btrue. % 1.92/2.58 0 [] e_q2(X,X)=btrue. % 1.92/2.58 0 [] e_q3(X,X)=btrue. % 1.92/2.58 0 [] e_q3(propm5(X),bfalse)!=btrue. % 1.92/2.58 end_of_list. % 1.92/2.58 % 1.92/2.58 SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=2. % 1.92/2.58 % 1.92/2.58 This is a Horn set with equality. The strategy will be % 1.92/2.58 Knuth-Bendix and hyper_res, with positive clauses in % 1.92/2.58 sos and nonpositive clauses in usable. % 1.92/2.58 % 1.92/2.58 dependent: set(knuth_bendix). % 1.92/2.58 dependent: set(anl_eq). % 1.92/2.58 dependent: set(para_from). % 1.92/2.58 dependent: set(para_into). % 1.92/2.58 dependent: clear(para_from_right). % 1.92/2.58 dependent: clear(para_into_right). % 1.92/2.58 dependent: set(para_from_vars). % 1.92/2.58 dependent: set(eq_units_both_ways). % 1.92/2.58 dependent: set(dynamic_demod_all). % 1.92/2.58 dependent: set(dynamic_demod). % 1.92/2.58 dependent: set(order_eq). % 1.92/2.58 dependent: set(back_demod). % 1.92/2.58 dependent: set(lrpo). % 1.92/2.58 dependent: set(hyper_res). % 1.92/2.58 dependent: clear(order_hyper). % 1.92/2.58 % 1.92/2.58 ------------> process usable: % 1.92/2.58 ** KEPT (pick-wt=14): 1 [] e_q2(A,B)!=bfalse|e_q2(x(A,C),x(B,D))=bfalse. % 1.92/2.58 ** KEPT (pick-wt=16): 2 [] e_q2(A,B)!=btrue|e_q2(x(A,C),x(B,D))=e_q2(C,D). % 1.92/2.58 ** KEPT (pick-wt=14): 3 [] e_q2(A,B)!=bfalse|e_q2(y(A,C),y(B,D))=bfalse. % 1.92/2.58 ** KEPT (pick-wt=16): 4 [] e_q2(A,B)!=btrue|e_q2(y(A,C),y(B,D))=e_q2(C,D). % 1.92/2.58 ** KEPT (pick-wt=6): 5 [] e_q3(propm5(A),bfalse)!=btrue. % 1.92/2.58 % 1.92/2.58 ------------> process sos: % 1.92/2.58 ** KEPT (pick-wt=3): 6 [] A=A. % 1.92/2.58 ** KEPT (pick-wt=12): 7 [] aux(A,B,btrue)=y(n(s(s(z))),opt(A)). % 1.92/2.58 ** KEPT (pick-wt=13): 9 [copy,8,flip.1] opt(x(A,x(B,C)))=aux(x(A,B),C,bfalse). % 1.92/2.58 ---> New Demodulator: 10 [new_demod,9] opt(x(A,x(B,C)))=aux(x(A,B),C,bfalse). % 1.92/2.58 ** KEPT (pick-wt=12): 12 [copy,11,flip.1] x(opt(n(A)),opt(B))=aux(n(A),B,bfalse). % 1.92/2.58 ---> New Demodulator: 13 [new_demod,12] x(opt(n(A)),opt(B))=aux(n(A),B,bfalse). % 1.92/2.58 ** KEPT (pick-wt=14): 15 [copy,14,flip.1] x(opt(y(A,B)),opt(C))=aux(y(A,B),C,bfalse). % 1.92/2.58 ---> New Demodulator: 16 [new_demod,15] x(opt(y(A,B)),opt(C))=aux(y(A,B),C,bfalse). % 1.92/2.58 ** KEPT (pick-wt=10): 18 [copy,17,flip.1] x(opt(x2),opt(A))=aux(x2,A,bfalse). % 1.92/2.58 ---> New Demodulator: 19 [new_demod,18] x(opt(x2),opt(A))=aux(x2,A,bfalse). % 1.92/2.58 ** KEPT (pick-wt=10): 20 [] fail2(A,B)=aux(A,B,e_q2(A,B)). % 1.92/2.58 ---> New Demodulator: 21 [new_demod,20] fail2(A,B)=aux(A,B,e_q2(A,B)). % 1.92/2.58 ** KEPT (pick-wt=10): 23 [copy,22,flip.1] n(addNat(A,B))=fail1(n(A),n(B)). % 1.92/2.58 ---> New Demodulator: 24 [new_demod,23] n(addNat(A,B))=fail1(n(A),n(B)). % 1.92/2.58 ** KEPT (pick-wt=19): 26 [copy,25,demod,21] fail1(n(A),x(B,C))=aux(n(A),x(B,C),e_q2(n(A),x(B,C))). % 1.92/2.58 ---> New Demodulator: 27 [new_demod,26] fail1(n(A),x(B,C))=aux(n(A),x(B,C),e_q2(n(A),x(B,C))). % 1.92/2.58 ** KEPT (pick-wt=19): 29 [copy,28,demod,21] fail1(n(A),y(B,C))=aux(n(A),y(B,C),e_q2(n(A),y(B,C))). % 1.92/2.58 ---> New Demodulator: 30 [new_demod,29] fail1(n(A),y(B,C))=aux(n(A),y(B,C),e_q2(n(A),y(B,C))). % 1.92/2.58 ** KEPT (pick-wt=13): 32 [copy,31,demod,21] fail1(n(A),x2)=aux(n(A),x2,e_q2(n(A),x2)). % 1.92/2.58 ---> New Demodulator: 33 [new_demod,32] fail1(n(A),x2)=aux(n(A),x2,e_q2(n(A),x2)). % 1.92/2.58 ** KEPT (pick-wt=16): 35 [copy,34,demod,21] fail1(x(A,B),C)=aux(x(A,B),C,e_q2(x(A,B),C)). % 1.92/2.58 ---> New Demodulator: 36 [new_demod,35] fail1(x(A,B),C)=aux(x(A,B),C,e_q2(x(A,B),C)). % 1.92/2.58 ** KEPT (pick-wt=16): 38 [copy,37,demod,21] fail1(y(A,B),C)=aux(y(A,B),C,e_q2(y(A,B),C)). % 1.92/2.58 ---> New Demodulator: 39 [new_demod,38] fail1(y(A,B),C)=aux(y(A,B),C,e_q2(y(A,B),C)). % 1.92/2.58 ** KEPT (pick-wt=10): 41 [copy,40,demod,21] fail1(x2,A)=aux(x2,A,e_q2(x2,A)). % 1.92/2.58 ---> New Demodulator: 42 [new_demod,41] fail1(x2,A)=aux(x2,A,e_q2(x2,A)). % 1.92/2.58 ** KEPT (pick-wt=11): 44 [copy,43,flip.1] fail1(A,n(s(B)))=fail(A,n(s(B))). % 1.92/2.58 ---> New Demodulator: 45 [new_demod,44] fail1(A,n(s(B)))=fail(A,n(s(B))). % 1.92/2.58 ** KEPT (pick-wt=6): 46 [] fail(A,n(z))=A. % 1.92/2.58 ---> New Demodulator: 47 [new_demod,46] fail(A,n(z))=A. % 1.92/2.58 ** KEPT (pick-wt=11): 49 [copy,48,flip.1] fail1(A,x(B,C))=fail(A,x(B,C)). % 1.92/2.58 ---> New Demodulator: 50 [new_demod,49] fail1(A,x(B,C))=fail(A,x(B,C)). % 1.92/2.58 ** KEPT (pick-wt=11): 52 [copy,51,flip.1] fail1(A,y(B,C))=fail(A,y(B,C)). % 1.92/2.58 ---> New Demodulator: 53 [new_demod,52] fail1(A,y(B,C))=fail(A,y(B,C)). % 1.92/2.58 ** KEPT (pick-wt=7): 55 [copy,54,flip.1] fail1(A,x2)=fail(A,x2). % 1.92/2.58 ---> New Demodulator: 56 [new_demod,55] fail1(A,x2)=fail(A,x2). % 1.92/2.58 ** KEPT (pick-wt=9): 58 [copy,57,flip.1] y(opt(A),opt(B))=fail4(A,B). % 1.92/2.58 ---> New Demodulator: 59 [new_demod,58] y(opt(A),opt(B))=fail4(A,B). % 1.92/2.58 ** KEPT (pick-wt=10): 61 [copy,60,flip.1] n(mulNat(A,B))=fail32(n(A),n(B)). % 1.92/2.58 ---> New Demodulator: 62 [new_demod,61] n(mulNat(A,B))=fail32(n(A),n(B)). % 1.92/2.58 ** KEPT (pick-wt=13): 64 [copy,63,flip.1] fail4(n(A),x(B,C))=fail32(n(A),x(B,C)). % 1.92/2.58 ---> New Demodulator: 65 [new_demod,64] fail4(n(A),x(B,C))=fail32(n(A),x(B,C)). % 1.92/2.58 ** KEPT (pick-wt=13): 67 [copy,66,flip.1] fail4(n(A),y(B,C))=fail32(n(A),y(B,C)). % 1.92/2.58 ---> New Demodulator: 68 [new_demod,67] fail4(n(A),y(B,C))=fail32(n(A),y(B,C)). % 1.92/2.58 ** KEPT (pick-wt=9): 70 [copy,69,flip.1] fail4(n(A),x2)=fail32(n(A),x2). % 1.92/2.58 ---> New Demodulator: 71 [new_demod,70] fail4(n(A),x2)=fail32(n(A),x2). % 1.92/2.58 ** KEPT (pick-wt=12): 73 [copy,72,flip.1] opt(y(A,y(B,C)))=fail32(y(A,B),C). % 1.92/2.58 ---> New Demodulator: 74 [new_demod,73] opt(y(A,y(B,C)))=fail32(y(A,B),C). % 1.92/2.58 ** KEPT (pick-wt=11): 76 [copy,75,flip.1] fail4(x(A,B),C)=fail32(x(A,B),C). % 1.92/2.58 ---> New Demodulator: 77 [new_demod,76] fail4(x(A,B),C)=fail32(x(A,B),C). % 1.92/2.58 ** KEPT (pick-wt=7): 79 [copy,78,flip.1] fail4(x2,A)=fail32(x2,A). % 1.92/2.58 ---> New Demodulator: 80 [new_demod,79] fail4(x2,A)=fail32(x2,A). % 1.92/2.58 ** KEPT (pick-wt=13): 82 [copy,81,flip.1] fail32(A,n(s(s(B))))=fail22(A,n(s(s(B)))). % 1.92/2.58 ---> New Demodulator: 83 [new_demod,82] fail32(A,n(s(s(B))))=fail22(A,n(s(s(B)))). % 1.92/2.58 ** KEPT (pick-wt=7): 84 [] fail22(A,n(s(z)))=A. % 1.92/2.58 ---> New Demodulator: 85 [new_demod,84] fail22(A,n(s(z)))=A. % 1.92/2.58 ** KEPT (pick-wt=9): 87 [copy,86,flip.1] fail32(A,n(z))=fail22(A,n(z)). % 1.92/2.58 ---> New Demodulator: 88 [new_demod,87] fail32(A,n(z))=fail22(A,n(z)). % 1.92/2.58 ** KEPT (pick-wt=11): 90 [copy,89,flip.1] fail32(A,x(B,C))=fail22(A,x(B,C)). % 1.92/2.58 ---> New Demodulator: 91 [new_demod,90] fail32(A,x(B,C))=fail22(A,x(B,C)). % 1.92/2.58 ** KEPT (pick-wt=11): 93 [copy,92,flip.1] fail32(A,y(B,C))=fail22(A,y(B,C)). % 1.92/2.58 ---> New Demodulator: 94 [new_demod,93] fail32(A,y(B,C))=fail22(A,y(B,C)). % 1.92/2.58 ** KEPT (pick-wt=7): 96 [copy,95,flip.1] fail32(A,x2)=fail22(A,x2). % 1.92/2.58 ---> New Demodulator: 97 [new_demod,96] fail32(A,x2)=fail22(A,x2). % 1.92/2.58 ** KEPT (pick-wt=13): 99 [copy,98,flip.1] fail22(n(s(s(A))),B)=fail12(n(s(s(A))),B). % 1.92/2.58 ---> New Demodulator: 100 [new_demod,99] fail22(n(s(s(A))),B)=fail12(n(s(s(A))),B). % 1.92/2.58 ** KEPT (pick-wt=7): 101 [] fail12(n(s(z)),A)=A. % 1.92/2.58 ---> New Demodulator: 102 [new_demod,101] fail12(n(s(z)),A)=A. % 1.92/2.58 ** KEPT (pick-wt=9): 104 [copy,103,flip.1] fail22(n(z),A)=fail12(n(z),A). % 1.92/2.58 ---> New Demodulator: 105 [new_demod,104] fail22(n(z),A)=fail12(n(z),A). % 1.92/2.58 ** KEPT (pick-wt=11): 107 [copy,106,flip.1] fail22(x(A,B),C)=fail12(x(A,B),C). % 1.92/2.58 ---> New Demodulator: 108 [new_demod,107] fail22(x(A,B),C)=fail12(x(A,B),C). % 1.92/2.58 ** KEPT (pick-wt=11): 110 [copy,109,flip.1] fail22(y(A,B),C)=fail12(y(A,B),C). % 1.92/2.58 ---> New Demodulator: 111 [new_demod,110] fail22(y(A,B),C)=fail12(y(A,B),C). % 1.92/2.58 ** KEPT (pick-wt=7): 113 [copy,112,flip.1] fail22(x2,A)=fail12(x2,A). % 1.92/2.58 ---> New Demodulator: 114 [new_demod,113] fail22(x2,A)=fail12(x2,A). % 1.92/2.58 ** KEPT (pick-wt=11): 115 [] fail3(A,n(s(B)))=fail12(A,n(s(B))). % 1.92/2.58 ---> New Demodulator: 116 [new_demod,115] fail3(A,n(s(B)))=fail12(A,n(s(B))). % 1.92/2.58 ** KEPT (pick-wt=7): 117 [] fail3(A,n(z))=n(z). % 1.92/2.58 ---> New Demodulator: 118 [new_demod,117] fail3(A,n(z))=n(z). % 1.92/2.58 ** KEPT (pick-wt=11): 119 [] fail3(A,x(B,C))=fail12(A,x(B,C)). % 1.92/2.58 ---> New Demodulator: 120 [new_demod,119] fail3(A,x(B,C))=fail12(A,x(B,C)). % 1.92/2.58 ** KEPT (pick-wt=11): 121 [] fail3(A,y(B,C))=fail12(A,y(B,C)). % 1.92/2.58 ---> New Demodulator: 122 [new_demod,121] fail3(A,y(B,C))=fail12(A,y(B,C)). % 1.92/2.58 ** KEPT (pick-wt=7): 123 [] fail3(A,x2)=fail12(A,x2). % 1.92/2.58 ---> New Demodulator: 124 [new_demod,123] fail3(A,x2)=fail12(A,x2). % 1.92/2.58 ** KEPT (pick-wt=5): 125 [] impl(btrue,A)=A. % 1.92/2.58 ---> New Demodulator: 126 [new_demod,125] impl(btrue,A)=A. % 1.92/2.58 ** KEPT (pick-wt=5): 127 [] impl(bfalse,A)=btrue. % 1.92/2.58 ---> New Demodulator: 128 [new_demod,127] impl(bfalse,A)=btrue. % 1.92/2.58 ** KEPT (pick-wt=6): 129 [] d(n(A))=n(z). % 1.92/2.58 ** KEPT (pick-wt=10): 130 [] d(x(A,B))=x(d(A),d(B)). % 1.92/2.58 ---> New Demodulator: 131 [new_demod,130] d(x(A,B))=x(d(A),d(B)). % 1.92/2.58 ** KEPT (pick-wt=14): 132 [] d(y(A,B))=x(y(d(A),B),y(A,d(B))). % 1.92/2.58 ---> New Demodulator: 133 [new_demod,132] d(y(A,B))=x(y(d(A),B),y(A,d(B))). % 1.92/2.58 ** KEPT (pick-wt=6): 135 [copy,134,flip.1] n(s(z))=d(x2). % 1.92/2.58 ---> New Demodulator: 136 [new_demod,135] n(s(z))=d(x2). % 1.92/2.58 ** KEPT (pick-wt=9): 138 [copy,137,flip.1] s(addNat(A,B))=addNat(s(A),B). % 1.92/2.58 ---> New Demodulator: 139 [new_demod,138] s(addNat(A,B))=addNat(s(A),B). % 1.92/2.58 ** KEPT (pick-wt=5): 140 [] addNat(z,A)=A. % 1.92/2.58 ---> New Demodulator: 141 [new_demod,140] addNat(z,A)=A. % 1.92/2.58 ** KEPT (pick-wt=10): 142 [] mulNat(s(A),B)=addNat(B,mulNat(A,B)). % 1.92/2.58 ---> New Demodulator: 143 [new_demod,142] mulNat(s(A),B)=addNat(B,mulNat(A,B)). % 1.92/2.58 ** KEPT (pick-wt=5): 144 [] mulNat(z,A)=z. % 1.92/2.58 ---> New Demodulator: 145 [new_demod,144] mulNat(z,A)=z. % 1.92/2.58 ** KEPT (pick-wt=12): 146 [] opt(x(n(s(A)),B))=fail(n(s(A)),B). % 1.92/2.58 ---> New Demodulator: 147 [new_demod,146] opt(x(n(s(A)),B))=fail(n(s(A)),B). % 1.92/2.58 ** KEPT (pick-wt=7): 148 [] opt(x(n(z),A))=A. % 1.92/2.58 ---> New Demodulator: 149 [new_demod,148] opt(x(n(z),A))=A. % 1.92/2.58 ** KEPT (pick-wt=12): 150 [] opt(x(x(A,B),C))=fail(x(A,B),C). % 1.92/2.58 ---> New Demodulator: 151 [new_demod,150] opt(x(x(A,B),C))=fail(x(A,B),C). % 1.92/2.58 ** KEPT (pick-wt=12): 152 [] opt(x(y(A,B),C))=fail(y(A,B),C). % 1.92/2.58 ---> New Demodulator: 153 [new_demod,152] opt(x(y(A,B),C))=fail(y(A,B),C). % 1.92/2.58 ** KEPT (pick-wt=8): 154 [] opt(x(x2,A))=fail(x2,A). % 1.92/2.58 ---> New Demodulator: 155 [new_demod,154] opt(x(x2,A))=fail(x2,A). % 1.92/2.58 ** KEPT (pick-wt=12): 156 [] opt(y(n(s(A)),B))=fail3(n(s(A)),B). % 1.92/2.58 ---> New Demodulator: 157 [new_demod,156] opt(y(n(s(A)),B))=fail3(n(s(A)),B). % 1.92/2.58 ** KEPT (pick-wt=8): 158 [] opt(y(n(z),A))=n(z). % 1.92/2.58 ---> New Demodulator: 159 [new_demod,158] opt(y(n(z),A))=n(z). % 1.92/2.58 ** KEPT (pick-wt=12): 160 [] opt(y(x(A,B),C))=fail3(x(A,B),C). % 1.92/2.58 ---> New Demodulator: 161 [new_demod,160] opt(y(x(A,B),C))=fail3(x(A,B),C). % 1.92/2.58 ** KEPT (pick-wt=12): 162 [] opt(y(y(A,B),C))=fail3(y(A,B),C). % 1.92/2.58 ---> New Demodulator: 163 [new_demod,162] opt(y(y(A,B),C))=fail3(y(A,B),C). % 1.92/2.58 ** KEPT (pick-wt=8): 164 [] opt(y(x2,A))=fail3(x2,A). % 1.92/2.58 ---> New Demodulator: 165 [new_demod,164] opt(y(x2,A))=fail3(x2,A). % 1.92/2.58 ** KEPT (pick-wt=6): 166 [] opt(n(A))=n(A). % 1.92/2.58 ---> New Demodulator: 167 [new_demod,166] opt(n(A))=n(A). % 1.92/2.58 ** KEPT (pick-wt=4): 168 [] opt(x2)=x2. % 1.92/2.58 ---> New Demodulator: 169 [new_demod,168] opt(x2)=x2. % 1.92/2.58 ** KEPT (pick-wt=38): 170 [] propm5(A)=impl(e_q2(opt(d(A)),x(y(x2,y(x2,y(x2,x2))),y(x2,x(y(x2,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2)))))))),e_q3(btrue,bfalse)). % 1.92/2.58 ---> New Demodulator: 171 [new_demod,170] propm5(A)=impl(e_q2(opt(d(A)),x(y(x2,y(x2,y(x2,x2))),y(x2,x(y(x2,y(x2,x2)),y(x2,x(y(x2,x2),y(x2,x(x2,x2)))))))),e_q3(btrue,bfalse)). % 1.92/2.58 ** KEPT (pick-wt=5): 172 [] e_q3(bfalse,btrue)=bfalse. % 1.92/2.58 ---> New Demodulator: 173 [new_demod,172] e_q3(bfalse,btrue)=bfalse. % 1.92/2.58 ** KEPT (pick-wt=5): 174 [] e_q3(btrue,bfalse)=bfalse. % 1.92/2.58 ---> New Demodulator: 175 [new_demod,174] e_q3(btrue,bfalse)=bfalse. % 1.92/2.58 ** KEPT (pick-wt=9): 176 [] e_q2(n(A),n(B))=e_q(A,B). % 1.92/2.58 ---> New Demodulator: 177 [new_demod,176] e_q2(n(A),n(B))=e_q(A,B). % 1.92/2.58 ** KEPT (pick-wt=8): 178 [] e_q2(n(A),x(B,C))=bfalse. % 1.92/2.58 ---> New Demodulator: 179 [new_demod,178] e_q2(n(A),x(B,C))=bfalse. % 1.92/2.58 ** KEPT (pick-wt=8): 180 [] e_q2(n(A),y(B,C))=bfalse. % 1.92/2.58 ---> New Demodulator: 181 [new_demod,180] e_q2(n(A),y(B,C))=bfalse. % 1.92/2.58 ** KEPT (pick-wt=6): 182 [] e_q2(n(A),x2)=bfalse. % 1.92/2.58 ---> New Demodulator: 183 [new_demod,182] e_q2(n(A),x2)=bfalse. % 1.92/2.58 ** KEPT (pick-wt=8): 184 [] e_q2(x(A,B),n(C))=bfalse. % 1.92/2.58 ---> New Demodulator: 185 [new_demod,184] e_q2(x(A,B),n(C))=bfalse. % 1.92/2.58 ** KEPT (pick-wt=9): 186 [] e_q2(x(A,B),y(C,D))=bfalse. % 1.92/2.58 ---> New Demodulator: 187 [new_demod,186] e_q2(x(A,B),y(C,D))=bfalse. % 1.92/2.58 ** KEPT (pick-wt=7): 188 [] e_q2(x(A,B),x2)=bfalse. % 1.92/2.58 ---> New Demodulator: 189 [new_demod,188] e_q2(x(A,B),x2)=bfalse. % 1.92/2.58 ** KEPT (pick-wt=8): 190 [] e_q2(y(A,B),n(C))=bfalse. % 1.92/2.58 ---> New Demodulator: 191 [new_demod,190] e_q2(y(A,B),n(C))=bfalse. % 1.92/2.58 ** KEPT (pick-wt=9): 192 [] e_q2(y(A,B),x(C,D))=bfalse. % 1.92/2.58 ---> New Demodulator: 193 [new_demod,192] e_q2(y(A,B),x(C,D))=bfalse. % 1.92/2.58 ** KEPT (pick-wt=7): 194 [] e_q2(y(A,B),x2)=bfalse. % 1.92/2.58 ---> New Demodulator: 195 [new_demod,194] e_q2(y(A,B),x2)=bfalse. % 1.92/2.58 ** KEPT (pick-wt=6): 196 [] e_q2(x2,n(A))=bfalse. % 1.92/2.58 ---> New Demodulator: 197 [new_demod,196] e_q2(x2,n(A))=bfalse. % 1.92/2.58 ** KEPT (pick-wt=7): 198 [] e_q2(x2,x(A,B))=bfalse. % 1.92/2.58 ---> New Demodulator: 199 [new_demod,198] e_q2(x2,x(A,B))=bfalse. % 1.92/2.58 ** KEPT (pick-wt=7): 200 [] e_q2(x2,y(A,B))=bfalse. % 1.92/2.58 ---> New Demodulator: 201 [new_demod,200] e_q2(x2,y(A,B))=bfalse. % 1.92/2.58 ** KEPT (pick-wt=9): 202 [] e_q(s(A),s(B))=e_q(A,B). % 1.92/2.58 ---> New Demodulator: 203 [new_demod,202] e_q(s(A),s(B))=e_q(A,B). % 1.92/2.58 ** KEPT (pick-wt=6): 204 [] e_q(s(A),z)=bfalse. % 1.92/2.58 ---> New Demodulator: 205 [new_demod,204] e_q(s(A),z)=bfalse. % 1.92/2.58 ** KEPT (pick-wt=6): 206 [] e_q(z,s(A))=bfalse. % 1.92/2.58 ---> New Demodulator: 207 [new_demod,206] e_q(z,s(A))=bfalse. % 1.92/2.58 ** KEPT (pick-wt=5): 208 [] e_q(A,A)=btrue. % 1.92/2.58 ---> New Demodulator: 209 [new_demod,208] e_q(A,A)=btrue. % 1.92/2.58 ** KEPT (pick-wt=5): 210 [] e_q2(A,A)=btrue. % 1.92/2.58 ---> New Demodulator: 211 [new_demod,210] e_q2(A,A)=btrue. % 1.92/2.58 ** KEPT (pick-wt=5): 212 [] e_q3(A,A)=btrue. % 1.92/2.58 ---> New Demodulator: 213 [new_demod,212] e_q3(A,A)=btrue. % 1.92/2.58 Following clause subsumed by 6 during input processing: 0 [copy,6,flip.1] A=A. % 1.92/2.58 ** KEPT (pick-wt=12): 214 [copy,7,flip.1] y(n(s(s(z))),opt(A))=aux(A,B,btrue). % 1.92/2.58 >>>> Starting back demodulation with 10. % 1.92/2.58 >>>> Starting back demodulation with 13. % 1.92/2.58 >>>> Starting back demodulation with 16. % 1.92/2.58 >>>> Starting back demodulation with 19. % 1.92/2.58 >>>> Starting back demodulation with 21. % 1.92/2.58 >>>> Starting back demodulation with 24. % 1.92/2.58 >>>> Starting back demodulation with 27. % 1.92/2.58 >>>> Starting back demodulation with 30. % 1.92/2.58 >>>> Starting back demodulation with 33. % 1.92/2.58 >>>> Starting back demodulation with 36. % 1.92/2.58 >>>> Starting back demodulation with 39. % 1.92/2.58 >>>> Starting back demodulation with 42. % 1.92/2.58 >>>> Starting back demodulation with 45. % 1.92/2.58 >>>> Starting back demodulation with 47. % 1.92/2.58 >>>> Starting back demodulation with 50. % 1.92/2.58 >> back demodulating 26 with 50. % 1.92/2.58 >>>> Starting back demodulation with 53. % 1.92/2.58 >> back demodulating 29 with 53. % 1.92/2.58 >>>> Starting back demodulation with 56. % 1.92/2.58 >> back demodulating 32 with 56. % 1.92/2.58 >>>> Starting back demodulation with 59. % 1.92/2.58 >>>> Starting back demodulation with 62. % 1.92/2.58 >>>> Starting back demodulation with 65. % 1.92/2.58 >>>> Starting back demodulation with 68. % 1.92/2.58 >>>> Starting back demodulation with 71. % 1.92/2.58 >>>> Starting back demodulation with 74. % 1.92/2.58 >>>> Starting back demodulation with 77. % 1.92/2.58 >>>> Starting back demodulation with 80. % 1.92/2.58 >>>> Starting back demodulation with 83. % 1.92/2.58 >>>> Starting back demodulation with 85. % 1.92/2.58 >>>> Starting back demodulation with 88. % 1.92/2.58 >>>> Starting back demodulation with 91. % 1.92/2.58 >> back demodulating 64 with 91. % 1.92/2.58 >>>> Starting back demodulation with 94. % 1.92/2.58 >> back demodulating 67 with 94. % 1.92/2.58 >>>> Starting back demodulation with 97. % 1.92/2.58 >> back demodulating 70 with 97. % 1.92/2.58 >>>> Starting back demodulation with 100. % 1.92/2.58 >>>> Starting back demodulation with 102. % 1.92/2.58 >>>> Starting back demodulation with 105. % 1.92/2.58 >>>> Starting back demodulation with 108. % 1.92/2.58 >>>> Starting back demodulation with 111. % 1.92/2.58 >>>> Starting back demodulation with 114. % 1.92/2.58 >>>> Starting back demodulation with 116. % 1.92/2.58 >>>> Starting back demodulation with 118. % 1.92/2.58 >>>> Starting back demodulation with 120. % 1.92/2.58 >>>> Starting back demodulation with 122. % 1.92/2.58 >>>> Starting back demodulation with 124. % 1.92/2.58 >>>> Starting back demodulation with 126. % 1.92/2.58 >>>> Starting back demodulation with 128. % 1.92/2.58 ** KEPT (pick-wt=6): 227 [copy,129,flip.1] n(z)=d(n(A)). % 1.92/2.58 >>>> Starting back demodulation with 131. % 1.92/2.58 >>>> Starting back demodulation with 133. % 1.92/2.58 >>>> Starting back demodulation with 136. % 1.92/2.58 >> back demodulating 101 with 136. % 1.92/2.58 >> back demodulating 84 with 136. % 1.92/2.58 >>>> Starting back demodulation with 139. % 1.92/2.58 >>>> Starting back demodulation with 141. % 1.92/2.58 >>>> Starting back demodulation with 143. % 1.92/2.58 >>>> Starting back demodulation with 145. % 1.92/2.58 >>>> Starting back demodulation with 147. % 1.92/2.58 >>>> Starting back demodulation with 149. % 1.92/2.58 >>>> Starting back demodulation with 151. % 1.92/2.58 >>>> Starting back demodulation with 153. % 1.92/2.58 >>>> Starting back demodulation with 155. % 1.92/2.58 >>>> Starting back demodulation with 157. % 1.92/2.58 >>>> Starting back demodulation with 159. % 1.92/2.58 >>>> Starting back demodulation with 161. % 1.92/2.58 >>>> Starting back demodulation with 163. % 1.92/2.58 >>>> Starting back demodulation with 165. % 1.92/2.58 >>>> Starting back demodulation with 167. % 1.92/2.58 >> back demodulating 12 with 167. % 1.92/2.58 >>>> Starting back demodulation with 169. % 1.92/2.58 >> back demodulating 18 with 169. % 1.92/2.58 >>>> Starting back demodulation with 171. % 1.92/2.58 >> back demodulating 5 with 171. % 1.92/2.58 >>>> Starting back demodulation with 173. % 1.92/2.58 >>>> Starting back demodulation with 175. % 1.92/2.58 >> back demodulating 170 with 175. % 1.92/2.58 >>>> Starting back demodulation with 177. % 1.92/2.58 >>>> Starting back demodulation with 179. % 1.92/2.58 >>>> Starting back demodulation with 181. % 1.92/2.58 >>>> Starting back demodulation with 183. % 2.51/2.60 >>>> Starting back demodulation with 185. % 2.51/2.60 >>>> Starting back demodulation with 187. % 2.51/2.60 >>>> Starting back demodulation with 189. % 2.51/2.60 >>>> Starting back demodulation with 191. % 2.51/2.60 >>>> Starting back demodulation with 193. % 2.51/2.60 >>>> Starting back demodulation with 195. % 2.51/2.60 >>>> Starting back demodulation with 197. % 2.51/2.60 >>>> Starting back demodulation with 199. % 2.51/2.60 >>>> Starting back demodulation with 201. % 2.51/2.60 >>>> Starting back demodulation with 203. % 2.51/2.60 >>>> Starting back demodulation with 205. % 2.51/2.60 >>>> Starting back demodulation with 207. % 2.51/2.60 >>>> Starting back demodulation with 209. % 2.51/2.60 >>>> Starting back demodulation with 211. % 2.51/2.60 >>>> Starting back demodulation with 213. % 2.51/2.60 Following clause subsumed by 7 during input processing: 0 [copy,214,flip.1] aux(A,B,btrue)=y(n(s(s(z))),opt(A)). % 2.51/2.60 >>>> Starting back demodulation with 216. % 2.51/2.60 >>>> Starting back demodulation with 218. % 2.51/2.60 >>>> Starting back demodulation with 220. % 2.51/2.60 >>>> Starting back demodulation with 222. % 2.51/2.60 >>>> Starting back demodulation with 224. % 2.51/2.60 >>>> Starting back demodulation with 226. % 2.51/2.60 Following clause subsumed by 129 during input processing: 0 [copy,227,flip.1] d(n(A))=n(z). % 2.51/2.60 >>>> Starting back demodulation with 229. % 2.51/2.60 >>>> Starting back demodulation with 231. % 2.51/2.60 >>>> Starting back demodulation with 233. % 2.51/2.60 >>>> Starting back demodulation with 235. % 2.51/2.60 >>>> Starting back demodulation with 238. % 2.51/2.60 % 2.51/2.60 ======= end of input processing ======= % 2.51/2.60 % 2.51/2.60 =========== start of search =========== % 2.51/2.60 % 2.51/2.60 % 2.51/2.60 Resetting weight limit to 9. % 2.51/2.60 % 2.51/2.60 % 2.51/2.60 Resetting weight limit to 9. % 2.51/2.60 % 2.51/2.60 sos_size=155 % 2.51/2.60 % 2.51/2.60 Search stopped because sos empty. % 2.51/2.60 % 2.51/2.60 % 2.51/2.60 Search stopped because sos empty. % 2.51/2.60 % 2.51/2.60 ============ end of search ============ % 2.51/2.60 % 2.51/2.60 -------------- statistics ------------- % 2.51/2.60 clauses given 231 % 2.51/2.60 clauses generated 2994 % 2.51/2.60 clauses kept 280 % 2.51/2.60 clauses forward subsumed 764 % 2.51/2.60 clauses back subsumed 0 % 2.51/2.60 Kbytes malloced 6835 % 2.51/2.60 % 2.51/2.60 ----------- times (seconds) ----------- % 2.51/2.60 user CPU time 0.03 (0 hr, 0 min, 0 sec) % 2.51/2.60 system CPU time 0.00 (0 hr, 0 min, 0 sec) % 2.51/2.60 wall-clock time 2 (0 hr, 0 min, 2 sec) % 2.51/2.60 % 2.51/2.60 Process 16073 finished Tue May 5 10:14:41 2026 % 2.51/2.60 Otter interrupted % 2.51/2.60 PROOF NOT FOUND %------------------------------------------------------------------------------