%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWX188+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n005.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 3.85s 4.05s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX188+1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : otter-tptp-script %s % 0.16/0.34 % Computer : n005.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Tue May 5 09:44:30 EDT 2026 % 0.16/0.34 % CPUTime : % 2.18/2.39 ----- Otter 3.3f, August 2004 ----- % 2.18/2.39 The process was started by sandbox on n005.cluster.edu, % 2.18/2.39 Tue May 5 09:44:30 2026 % 2.18/2.39 The command was "./otter". The process ID is 8044. % 2.18/2.39 % 2.18/2.39 set(prolog_style_variables). % 2.18/2.39 set(auto). % 2.18/2.39 dependent: set(auto1). % 2.18/2.39 dependent: set(process_input). % 2.18/2.39 dependent: clear(print_kept). % 2.18/2.39 dependent: clear(print_new_demod). % 2.18/2.39 dependent: clear(print_back_demod). % 2.18/2.39 dependent: clear(print_back_sub). % 2.18/2.39 dependent: set(control_memory). % 2.18/2.39 dependent: assign(max_mem, 12000). % 2.18/2.39 dependent: assign(pick_given_ratio, 4). % 2.18/2.39 dependent: assign(stats_level, 1). % 2.18/2.39 dependent: assign(max_seconds, 10800). % 2.18/2.39 clear(print_given). % 2.18/2.39 % 2.18/2.39 formula_list(usable). % 2.18/2.39 all A (A=A). % 2.18/2.39 all X (proj1S(s(X))=X). % 2.18/2.39 all X (s(X)!=z). % 2.18/2.39 all X (proj1N(n(X))=X). % 2.18/2.39 all X X2 (proj1(x(X,X2))=X). % 2.18/2.39 all X X2 (proj2(x(X,X2))=X2). % 2.18/2.39 all X X2 (proj12(y(X,X2))=X). % 2.18/2.39 all X X2 (proj22(y(X,X2))=X2). % 2.18/2.39 all X X2 X3 (n(X)!=x(X2,X3)). % 2.18/2.39 all X X2 X3 (n(X)!=y(X2,X3)). % 2.18/2.39 all X (n(X)!=x2). % 2.18/2.39 all X X2 X3 X4 (x(X,X2)!=y(X3,X4)). % 2.18/2.39 all X X2 (x(X,X2)!=x2). % 2.18/2.39 all X X2 (y(X,X2)!=x2). % 2.18/2.39 all Y E (Y=E->fail2(Y,E)=y(n(s(s(z))),opt(Y))). % 2.18/2.39 all Y E (Y!=E-> (Y!=x(proj1(Y),proj2(Y))->fail2(Y,E)=x(opt(Y),opt(E)))). % 2.18/2.39 all E A B (x(A,B)!=E->fail2(x(A,B),E)=opt(x(A,x(B,E)))). % 2.18/2.39 all Y E (Y!=n(proj1N(Y))->fail1(Y,E)=fail2(Y,E)). % 2.18/2.39 all E C (E!=n(proj1N(E))->fail1(n(C),E)=fail2(n(C),E)). % 2.18/2.39 all C B2 (fail1(n(C),n(B2))=n(addNat(C,B2))). % 2.18/2.39 all Y E (E!=n(proj1N(E))->fail(Y,E)=fail1(Y,E)). % 2.18/2.39 all Y X2 (fail(Y,n(s(X2)))=fail1(Y,n(s(X2)))). % 2.18/2.39 all Y (fail(Y,n(z))=Y). % 2.18/2.39 all X5 E2 (fail4(X5,E2)=y(opt(X5),opt(E2))). % 2.18/2.39 all X5 E2 (X5!=n(proj1N(X5))-> (X5!=y(proj12(X5),proj22(X5))->fail32(X5,E2)=fail4(X5,E2))). % 2.18/2.39 all E2 A2 (E2!=n(proj1N(E2))->fail32(n(A2),E2)=fail4(n(A2),E2)). % 2.18/2.39 all A2 B3 (fail32(n(A2),n(B3))=n(mulNat(A2,B3))). % 2.18/2.39 all E2 A3 B4 (fail32(y(A3,B4),E2)=opt(y(A3,y(B4,E2)))). % 2.18/2.39 all X5 E2 (E2!=n(proj1N(E2))->fail22(X5,E2)=fail32(X5,E2)). % 2.18/2.39 all X5 X8 (fail22(X5,n(s(s(X8))))=fail32(X5,n(s(s(X8))))). % 2.18/2.39 all X5 (fail22(X5,n(s(z)))=X5). % 2.18/2.39 all X5 (fail22(X5,n(z))=fail32(X5,n(z))). % 2.18/2.39 all X5 E2 (X5!=n(proj1N(X5))->fail12(X5,E2)=fail22(X5,E2)). % 2.18/2.39 all E2 X11 (fail12(n(s(s(X11))),E2)=fail22(n(s(s(X11))),E2)). % 2.18/2.39 all E2 (fail12(n(s(z)),E2)=E2). % 2.18/2.39 all E2 (fail12(n(z),E2)=fail22(n(z),E2)). % 2.18/2.39 all X5 E2 (E2!=n(proj1N(E2))->fail3(X5,E2)=fail12(X5,E2)). % 2.18/2.39 all X5 X13 (fail3(X5,n(s(X13)))=fail12(X5,n(s(X13)))). % 2.18/2.39 all X5 (fail3(X5,n(z))=n(z)). % 2.18/2.39 all Y (d(n(Y))=n(z)). % 2.18/2.39 all F G (d(x(F,G))=x(d(F),d(G))). % 2.18/2.39 all H G2 (d(y(H,G2))=x(y(d(H),G2),y(H,d(G2)))). % 2.18/2.39 d(x2)=n(s(z)). % 2.18/2.39 all Y Z (addNat(s(Z),Y)=s(addNat(Z,Y))). % 2.18/2.39 all Y (addNat(z,Y)=Y). % 2.18/2.39 all Y Z (mulNat(s(Z),Y)=addNat(Y,mulNat(Z,Y))). % 2.18/2.39 all Y (mulNat(z,Y)=z). % 2.18/2.39 all X (X!=x(proj1(X),proj2(X))-> (X!=y(proj12(X),proj22(X))->opt(X)=X)). % 2.18/2.39 all Y E (Y!=n(proj1N(Y))->opt(x(Y,E))=fail(Y,E)). % 2.18/2.39 all E X4 (opt(x(n(s(X4)),E))=fail(n(s(X4)),E)). % 2.18/2.39 all E (opt(x(n(z),E))=E). % 2.18/2.39 all X5 E2 (X5!=n(proj1N(X5))->opt(y(X5,E2))=fail3(X5,E2)). % 2.18/2.39 all E2 X15 (opt(y(n(s(X15)),E2))=fail3(n(s(X15)),E2)). % 2.18/2.39 all E2 (opt(y(n(z),E2))=n(z)). % 2.18/2.39 -(exists E (opt(d(E))=opt(x(n(s(s(z))),x(x2,x2))))). % 2.18/2.39 end_of_list. % 2.18/2.39 % 2.18/2.39 -------> usable clausifies to: % 2.18/2.39 % 2.18/2.39 list(usable). % 2.18/2.39 0 [] A=A. % 2.18/2.39 0 [] proj1S(s(X))=X. % 2.18/2.39 0 [] s(X)!=z. % 2.18/2.39 0 [] proj1N(n(X))=X. % 2.18/2.39 0 [] proj1(x(X,X2))=X. % 2.18/2.39 0 [] proj2(x(X,X2))=X2. % 2.18/2.39 0 [] proj12(y(X,X2))=X. % 2.18/2.39 0 [] proj22(y(X,X2))=X2. % 2.18/2.39 0 [] n(X)!=x(X2,X3). % 2.18/2.39 0 [] n(X)!=y(X2,X3). % 2.18/2.39 0 [] n(X)!=x2. % 2.18/2.39 0 [] x(X,X2)!=y(X3,X4). % 2.18/2.39 0 [] x(X,X2)!=x2. % 2.18/2.39 0 [] y(X,X2)!=x2. % 2.18/2.39 0 [] Y!=E|fail2(Y,E)=y(n(s(s(z))),opt(Y)). % 2.18/2.39 0 [] Y=E|Y=x(proj1(Y),proj2(Y))|fail2(Y,E)=x(opt(Y),opt(E)). % 2.18/2.39 0 [] x(A,B)=E|fail2(x(A,B),E)=opt(x(A,x(B,E))). % 2.18/2.39 0 [] Y=n(proj1N(Y))|fail1(Y,E)=fail2(Y,E). % 2.18/2.39 0 [] E=n(proj1N(E))|fail1(n(C),E)=fail2(n(C),E). % 2.18/2.39 0 [] fail1(n(C),n(B2))=n(addNat(C,B2)). % 2.18/2.39 0 [] E=n(proj1N(E))|fail(Y,E)=fail1(Y,E). % 2.18/2.39 0 [] fail(Y,n(s(X2)))=fail1(Y,n(s(X2))). % 2.18/2.39 0 [] fail(Y,n(z))=Y. % 2.18/2.39 0 [] fail4(X5,E2)=y(opt(X5),opt(E2)). % 2.18/2.39 0 [] X5=n(proj1N(X5))|X5=y(proj12(X5),proj22(X5))|fail32(X5,E2)=fail4(X5,E2). % 2.18/2.39 0 [] E2=n(proj1N(E2))|fail32(n(A2),E2)=fail4(n(A2),E2). % 2.18/2.39 0 [] fail32(n(A2),n(B3))=n(mulNat(A2,B3)). % 2.18/2.39 0 [] fail32(y(A3,B4),E2)=opt(y(A3,y(B4,E2))). % 2.18/2.39 0 [] E2=n(proj1N(E2))|fail22(X5,E2)=fail32(X5,E2). % 2.18/2.39 0 [] fail22(X5,n(s(s(X8))))=fail32(X5,n(s(s(X8)))). % 2.18/2.39 0 [] fail22(X5,n(s(z)))=X5. % 2.18/2.39 0 [] fail22(X5,n(z))=fail32(X5,n(z)). % 2.18/2.39 0 [] X5=n(proj1N(X5))|fail12(X5,E2)=fail22(X5,E2). % 2.18/2.39 0 [] fail12(n(s(s(X11))),E2)=fail22(n(s(s(X11))),E2). % 2.18/2.39 0 [] fail12(n(s(z)),E2)=E2. % 2.18/2.39 0 [] fail12(n(z),E2)=fail22(n(z),E2). % 2.18/2.39 0 [] E2=n(proj1N(E2))|fail3(X5,E2)=fail12(X5,E2). % 2.18/2.39 0 [] fail3(X5,n(s(X13)))=fail12(X5,n(s(X13))). % 2.18/2.39 0 [] fail3(X5,n(z))=n(z). % 2.18/2.39 0 [] d(n(Y))=n(z). % 2.18/2.39 0 [] d(x(F,G))=x(d(F),d(G)). % 2.18/2.39 0 [] d(y(H,G2))=x(y(d(H),G2),y(H,d(G2))). % 2.18/2.39 0 [] d(x2)=n(s(z)). % 2.18/2.39 0 [] addNat(s(Z),Y)=s(addNat(Z,Y)). % 2.18/2.39 0 [] addNat(z,Y)=Y. % 2.18/2.39 0 [] mulNat(s(Z),Y)=addNat(Y,mulNat(Z,Y)). % 2.18/2.39 0 [] mulNat(z,Y)=z. % 2.18/2.39 0 [] X=x(proj1(X),proj2(X))|X=y(proj12(X),proj22(X))|opt(X)=X. % 2.18/2.39 0 [] Y=n(proj1N(Y))|opt(x(Y,E))=fail(Y,E). % 2.18/2.39 0 [] opt(x(n(s(X4)),E))=fail(n(s(X4)),E). % 2.18/2.39 0 [] opt(x(n(z),E))=E. % 2.18/2.39 0 [] X5=n(proj1N(X5))|opt(y(X5,E2))=fail3(X5,E2). % 2.18/2.39 0 [] opt(y(n(s(X15)),E2))=fail3(n(s(X15)),E2). % 2.18/2.39 0 [] opt(y(n(z),E2))=n(z). % 2.18/2.39 0 [] opt(d(E))!=opt(x(n(s(s(z))),x(x2,x2))). % 2.18/2.39 end_of_list. % 2.18/2.39 % 2.18/2.39 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=3. % 2.18/2.39 % 2.18/2.39 This ia a non-Horn set with equality. The strategy will be % 2.18/2.39 Knuth-Bendix, ordered hyper_res, factoring, and unit % 2.18/2.39 deletion, with positive clauses in sos and nonpositive % 2.18/2.39 clauses in usable. % 2.18/2.39 % 2.18/2.39 dependent: set(knuth_bendix). % 2.18/2.39 dependent: set(anl_eq). % 2.18/2.39 dependent: set(para_from). % 2.18/2.39 dependent: set(para_into). % 2.18/2.39 dependent: clear(para_from_right). % 2.18/2.39 dependent: clear(para_into_right). % 2.18/2.39 dependent: set(para_from_vars). % 2.18/2.39 dependent: set(eq_units_both_ways). % 2.18/2.39 dependent: set(dynamic_demod_all). % 2.18/2.39 dependent: set(dynamic_demod). % 2.18/2.39 dependent: set(order_eq). % 2.18/2.39 dependent: set(back_demod). % 2.18/2.39 dependent: set(lrpo). % 2.18/2.39 dependent: set(hyper_res). % 2.18/2.39 dependent: set(unit_deletion). % 2.18/2.39 dependent: set(factor). % 2.18/2.39 % 2.18/2.39 ------------> process usable: % 2.18/2.39 ** KEPT (pick-wt=4): 1 [] s(A)!=z. % 2.18/2.39 ** KEPT (pick-wt=6): 2 [] n(A)!=x(B,C). % 2.18/2.39 ** KEPT (pick-wt=6): 3 [] n(A)!=y(B,C). % 2.18/2.39 ** KEPT (pick-wt=4): 4 [] n(A)!=x2. % 2.18/2.39 ** KEPT (pick-wt=7): 5 [] x(A,B)!=y(C,D). % 2.18/2.39 ** KEPT (pick-wt=5): 6 [] x(A,B)!=x2. % 2.18/2.39 ** KEPT (pick-wt=5): 7 [] y(A,B)!=x2. % 2.18/2.39 ** KEPT (pick-wt=14): 8 [] A!=B|fail2(A,B)=y(n(s(s(z))),opt(A)). % 2.18/2.39 ** KEPT (pick-wt=13): 9 [] opt(d(A))!=opt(x(n(s(s(z))),x(x2,x2))). % 2.18/2.39 ** KEPT (pick-wt=6): 10 [copy,2,flip.1] x(A,B)!=n(C). % 2.18/2.39 ** KEPT (pick-wt=6): 11 [copy,3,flip.1] y(A,B)!=n(C). % 2.18/2.39 ** KEPT (pick-wt=7): 12 [copy,5,flip.1] y(A,B)!=x(C,D). % 2.18/2.39 ** KEPT (pick-wt=13): 13 [copy,9,flip.1] opt(x(n(s(s(z))),x(x2,x2)))!=opt(d(A)). % 2.18/2.39 Following clause subsumed by 2 during input processing: 0 [copy,10,flip.1] n(A)!=x(B,C). % 2.18/2.39 Following clause subsumed by 3 during input processing: 0 [copy,11,flip.1] n(A)!=y(B,C). % 2.18/2.39 Following clause subsumed by 5 during input processing: 0 [copy,12,flip.1] x(A,B)!=y(C,D). % 2.18/2.39 Following clause subsumed by 9 during input processing: 0 [copy,13,flip.1] opt(d(A))!=opt(x(n(s(s(z))),x(x2,x2))). % 2.18/2.39 % 2.18/2.39 ------------> process sos: % 2.18/2.39 ** KEPT (pick-wt=3): 14 [] A=A. % 2.18/2.39 ** KEPT (pick-wt=5): 15 [] proj1S(s(A))=A. % 2.18/2.39 ---> New Demodulator: 16 [new_demod,15] proj1S(s(A))=A. % 2.18/2.39 ** KEPT (pick-wt=5): 17 [] proj1N(n(A))=A. % 2.18/2.39 ---> New Demodulator: 18 [new_demod,17] proj1N(n(A))=A. % 2.18/2.39 ** KEPT (pick-wt=6): 19 [] proj1(x(A,B))=A. % 2.18/2.39 ---> New Demodulator: 20 [new_demod,19] proj1(x(A,B))=A. % 2.18/2.39 ** KEPT (pick-wt=6): 21 [] proj2(x(A,B))=B. % 2.18/2.39 ---> New Demodulator: 22 [new_demod,21] proj2(x(A,B))=B. % 2.18/2.39 ** KEPT (pick-wt=6): 23 [] proj12(y(A,B))=A. % 2.18/2.39 ---> New Demodulator: 24 [new_demod,23] proj12(y(A,B))=A. % 2.18/2.39 ** KEPT (pick-wt=6): 25 [] proj22(y(A,B))=B. % 2.18/2.39 ---> New Demodulator: 26 [new_demod,25] proj22(y(A,B))=B. % 2.18/2.39 ** KEPT (pick-wt=19): 28 [copy,27,flip.2,flip.3] A=B|x(proj1(A),proj2(A))=A|x(opt(A),opt(B))=fail2(A,B). % 2.18/2.39 ** KEPT (pick-wt=17): 30 [copy,29,flip.2] x(A,B)=C|opt(x(A,x(B,C)))=fail2(x(A,B),C). % 2.18/2.39 ** KEPT (pick-wt=12): 32 [copy,31,flip.1,flip.2] n(proj1N(A))=A|fail2(A,B)=fail1(A,B). % 2.18/2.39 ** KEPT (pick-wt=14): 34 [copy,33,flip.1,flip.2] n(proj1N(A))=A|fail2(n(B),A)=fail1(n(B),A). % 2.18/2.39 ** KEPT (pick-wt=10): 36 [copy,35,flip.1] n(addNat(A,B))=fail1(n(A),n(B)). % 2.18/2.39 ---> New Demodulator: 37 [new_demod,36] n(addNat(A,B))=fail1(n(A),n(B)). % 2.18/2.39 ** KEPT (pick-wt=12): 39 [copy,38,flip.1,flip.2] n(proj1N(A))=A|fail1(B,A)=fail(B,A). % 2.18/2.39 ** KEPT (pick-wt=11): 41 [copy,40,flip.1] fail1(A,n(s(B)))=fail(A,n(s(B))). % 2.18/2.39 ---> New Demodulator: 42 [new_demod,41] fail1(A,n(s(B)))=fail(A,n(s(B))). % 2.18/2.39 ** KEPT (pick-wt=6): 43 [] fail(A,n(z))=A. % 2.18/2.39 ---> New Demodulator: 44 [new_demod,43] fail(A,n(z))=A. % 2.18/2.39 ** KEPT (pick-wt=9): 46 [copy,45,flip.1] y(opt(A),opt(B))=fail4(A,B). % 2.18/2.39 ---> New Demodulator: 47 [new_demod,46] y(opt(A),opt(B))=fail4(A,B). % 2.18/2.39 ** KEPT (pick-wt=19): 49 [copy,48,flip.1,flip.2,flip.3] n(proj1N(A))=A|y(proj12(A),proj22(A))=A|fail4(A,B)=fail32(A,B). % 2.18/2.39 ** KEPT (pick-wt=14): 51 [copy,50,flip.1,flip.2] n(proj1N(A))=A|fail4(n(B),A)=fail32(n(B),A). % 2.18/2.39 ** KEPT (pick-wt=10): 53 [copy,52,flip.1] n(mulNat(A,B))=fail32(n(A),n(B)). % 2.18/2.39 ---> New Demodulator: 54 [new_demod,53] n(mulNat(A,B))=fail32(n(A),n(B)). % 2.18/2.39 ** KEPT (pick-wt=12): 56 [copy,55,flip.1] opt(y(A,y(B,C)))=fail32(y(A,B),C). % 2.18/2.39 ---> New Demodulator: 57 [new_demod,56] opt(y(A,y(B,C)))=fail32(y(A,B),C). % 2.18/2.39 ** KEPT (pick-wt=12): 59 [copy,58,flip.1,flip.2] n(proj1N(A))=A|fail32(B,A)=fail22(B,A). % 2.18/2.39 ** KEPT (pick-wt=13): 61 [copy,60,flip.1] fail32(A,n(s(s(B))))=fail22(A,n(s(s(B)))). % 2.18/2.39 ---> New Demodulator: 62 [new_demod,61] fail32(A,n(s(s(B))))=fail22(A,n(s(s(B)))). % 2.18/2.39 ** KEPT (pick-wt=7): 63 [] fail22(A,n(s(z)))=A. % 2.18/2.39 ---> New Demodulator: 64 [new_demod,63] fail22(A,n(s(z)))=A. % 2.18/2.39 ** KEPT (pick-wt=9): 66 [copy,65,flip.1] fail32(A,n(z))=fail22(A,n(z)). % 2.18/2.39 ---> New Demodulator: 67 [new_demod,66] fail32(A,n(z))=fail22(A,n(z)). % 2.18/2.39 ** KEPT (pick-wt=12): 69 [copy,68,flip.1,flip.2] n(proj1N(A))=A|fail22(A,B)=fail12(A,B). % 2.18/2.39 ** KEPT (pick-wt=13): 71 [copy,70,flip.1] fail22(n(s(s(A))),B)=fail12(n(s(s(A))),B). % 2.18/2.39 ---> New Demodulator: 72 [new_demod,71] fail22(n(s(s(A))),B)=fail12(n(s(s(A))),B). % 2.18/2.39 ** KEPT (pick-wt=7): 73 [] fail12(n(s(z)),A)=A. % 2.18/2.39 ---> New Demodulator: 74 [new_demod,73] fail12(n(s(z)),A)=A. % 2.18/2.39 ** KEPT (pick-wt=9): 76 [copy,75,flip.1] fail22(n(z),A)=fail12(n(z),A). % 2.18/2.39 ---> New Demodulator: 77 [new_demod,76] fail22(n(z),A)=fail12(n(z),A). % 2.18/2.39 ** KEPT (pick-wt=12): 79 [copy,78,flip.1] n(proj1N(A))=A|fail3(B,A)=fail12(B,A). % 2.18/2.39 ** KEPT (pick-wt=11): 80 [] fail3(A,n(s(B)))=fail12(A,n(s(B))). % 2.18/2.39 ---> New Demodulator: 81 [new_demod,80] fail3(A,n(s(B)))=fail12(A,n(s(B))). % 2.18/2.39 ** KEPT (pick-wt=7): 82 [] fail3(A,n(z))=n(z). % 2.18/2.39 ---> New Demodulator: 83 [new_demod,82] fail3(A,n(z))=n(z). % 2.18/2.39 ** KEPT (pick-wt=6): 84 [] d(n(A))=n(z). % 2.18/2.39 ** KEPT (pick-wt=10): 85 [] d(x(A,B))=x(d(A),d(B)). % 2.18/2.39 ---> New Demodulator: 86 [new_demod,85] d(x(A,B))=x(d(A),d(B)). % 2.18/2.39 ** KEPT (pick-wt=14): 87 [] d(y(A,B))=x(y(d(A),B),y(A,d(B))). % 2.18/2.39 ---> New Demodulator: 88 [new_demod,87] d(y(A,B))=x(y(d(A),B),y(A,d(B))). % 2.18/2.39 ** KEPT (pick-wt=6): 90 [copy,89,flip.1] n(s(z))=d(x2). % 2.18/2.39 ---> New Demodulator: 91 [new_demod,90] n(s(z))=d(x2). % 2.18/2.39 ** KEPT (pick-wt=9): 93 [copy,92,flip.1] s(addNat(A,B))=addNat(s(A),B). % 2.18/2.39 ---> New Demodulator: 94 [new_demod,93] s(addNat(A,B))=addNat(s(A),B). % 2.18/2.39 ** KEPT (pick-wt=5): 95 [] addNat(z,A)=A. % 2.18/2.39 ---> New Demodulator: 96 [new_demod,95] addNat(z,A)=A. % 2.18/2.39 ** KEPT (pick-wt=10): 97 [] mulNat(s(A),B)=addNat(B,mulNat(A,B)). % 2.18/2.39 ---> New Demodulator: 98 [new_demod,97] mulNat(s(A),B)=addNat(B,mulNat(A,B)). % 2.18/2.39 ** KEPT (pick-wt=5): 99 [] mulNat(z,A)=z. % 2.18/2.39 ---> New Demodulator: 100 [new_demod,99] mulNat(z,A)=z. % 2.18/2.39 ** KEPT (pick-wt=18): 102 [copy,101,flip.1,flip.2] x(proj1(A),proj2(A))=A|y(proj12(A),proj22(A))=A|opt(A)=A. % 2.18/2.39 ** KEPT (pick-wt=13): 104 [copy,103,flip.1] n(proj1N(A))=A|opt(x(A,B))=fail(A,B). % 2.18/2.39 ** KEPT (pick-wt=12): 105 [] opt(x(n(s(A)),B))=fail(n(s(A)),B). % 2.18/2.39 ---> New Demodulator: 106 [new_demod,105] opt(x(n(s(A)),B))=fail(n(s(A)),B). % 2.18/2.39 ** KEPT (pick-wt=7): 107 [] opt(x(n(z),A))=A. % 2.18/2.39 ---> New Demodulator: 108 [new_demod,107] opt(x(n(z),A))=A. % 2.18/2.39 ** KEPT (pick-wt=13): 110 [copy,109,flip.1] n(proj1N(A))=A|opt(y(A,B))=fail3(A,B). % 2.18/2.39 ** KEPT (pick-wt=12): 111 [] opt(y(n(s(A)),B))=fail3(n(s(A)),B). % 2.18/2.39 ---> New Demodulator: 112 [new_demod,111] opt(y(n(s(A)),B))=fail3(n(s(A)),B). % 2.18/2.39 ** KEPT (pick-wt=8): 113 [] opt(y(n(z),A))=n(z). % 2.18/2.39 ---> New Demodulator: 114 [new_demod,113] opt(y(n(z),A))=n(z). % 2.18/2.39 Following clause subsumed by 14 during input processing: 0 [copy,14,flip.1] A=A. % 2.18/2.39 >>>> Starting back demodulation with 16. % 2.18/2.39 >>>> Starting back demodulation with 18. % 2.18/2.39 >>>> Starting back demodulation with 20. % 2.18/2.39 >>>> Starting back demodulation with 22. % 2.18/2.39 >>>> Starting back demodulation with 24. % 3.85/4.04 >>>> Starting back demodulation with 26. % 3.85/4.04 >>>> Starting back demodulation with 37. % 3.85/4.04 >>>> Starting back demodulation with 42. % 3.85/4.04 >>>> Starting back demodulation with 44. % 3.85/4.04 >>>> Starting back demodulation with 47. % 3.85/4.04 >>>> Starting back demodulation with 54. % 3.85/4.04 >>>> Starting back demodulation with 57. % 3.85/4.04 >>>> Starting back demodulation with 62. % 3.85/4.04 >>>> Starting back demodulation with 64. % 3.85/4.04 >>>> Starting back demodulation with 67. % 3.85/4.04 >>>> Starting back demodulation with 72. % 3.85/4.04 >>>> Starting back demodulation with 74. % 3.85/4.04 >>>> Starting back demodulation with 77. % 3.85/4.04 >>>> Starting back demodulation with 81. % 3.85/4.04 >>>> Starting back demodulation with 83. % 3.85/4.04 ** KEPT (pick-wt=6): 115 [copy,84,flip.1] n(z)=d(n(A)). % 3.85/4.04 >>>> Starting back demodulation with 86. % 3.85/4.04 >>>> Starting back demodulation with 88. % 3.85/4.04 >>>> Starting back demodulation with 91. % 3.85/4.04 >> back demodulating 73 with 91. % 3.85/4.04 >> back demodulating 63 with 91. % 3.85/4.04 >>>> Starting back demodulation with 94. % 3.85/4.04 >>>> Starting back demodulation with 96. % 3.85/4.04 >>>> Starting back demodulation with 98. % 3.85/4.04 >>>> Starting back demodulation with 100. % 3.85/4.04 >>>> Starting back demodulation with 106. % 3.85/4.04 >> back demodulating 13 with 106. % 3.85/4.04 >> back demodulating 9 with 106. % 3.85/4.04 >>>> Starting back demodulation with 108. % 3.85/4.04 >>>> Starting back demodulation with 112. % 3.85/4.04 >>>> Starting back demodulation with 114. % 3.85/4.04 Following clause subsumed by 84 during input processing: 0 [copy,115,flip.1] d(n(A))=n(z). % 3.85/4.04 >>>> Starting back demodulation with 117. % 3.85/4.04 >>>> Starting back demodulation with 119. % 3.85/4.04 Following clause subsumed by 121 during input processing: 0 [copy,120,flip.1] opt(d(A))!=fail(n(s(s(z))),x(x2,x2)). % 3.85/4.04 Following clause subsumed by 120 during input processing: 0 [copy,121,flip.1] fail(n(s(s(z))),x(x2,x2))!=opt(d(A)). % 3.85/4.04 % 3.85/4.04 ======= end of input processing ======= % 3.85/4.04 % 3.85/4.04 =========== start of search =========== % 3.85/4.04 % 3.85/4.04 % 3.85/4.04 Resetting weight limit to 8. % 3.85/4.04 % 3.85/4.04 % 3.85/4.04 Resetting weight limit to 8. % 3.85/4.04 % 3.85/4.04 sos_size=277 % 3.85/4.04 % 3.85/4.04 Search stopped because sos empty. % 3.85/4.04 % 3.85/4.04 % 3.85/4.04 Search stopped because sos empty. % 3.85/4.04 % 3.85/4.04 ============ end of search ============ % 3.85/4.04 % 3.85/4.04 -------------- statistics ------------- % 3.85/4.04 clauses given 371 % 3.85/4.04 clauses generated 95252 % 3.85/4.04 clauses kept 562 % 3.85/4.04 clauses forward subsumed 791 % 3.85/4.04 clauses back subsumed 10 % 3.85/4.04 Kbytes malloced 7812 % 3.85/4.04 % 3.85/4.04 ----------- times (seconds) ----------- % 3.85/4.04 user CPU time 1.66 (0 hr, 0 min, 1 sec) % 3.85/4.04 system CPU time 0.00 (0 hr, 0 min, 0 sec) % 3.85/4.04 wall-clock time 4 (0 hr, 0 min, 4 sec) % 3.85/4.04 % 3.85/4.04 Process 8044 finished Tue May 5 09:44:34 2026 % 3.85/4.04 Otter interrupted % 3.85/4.04 PROOF NOT FOUND %------------------------------------------------------------------------------