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