%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWX196-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n023.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.62s 2.84s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX196-1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : otter-tptp-script %s % 0.15/0.33 % Computer : n023.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 11:02:53 EDT 2026 % 0.15/0.33 % CPUTime : % 2.62/2.80 ----- Otter 3.3f, August 2004 ----- % 2.62/2.80 The process was started by sandbox2 on n023.cluster.edu, % 2.62/2.80 Tue May 5 11:02:53 2026 % 2.62/2.80 The command was "./otter". The process ID is 8441. % 2.62/2.80 % 2.62/2.80 set(prolog_style_variables). % 2.62/2.80 set(auto). % 2.62/2.80 dependent: set(auto1). % 2.62/2.80 dependent: set(process_input). % 2.62/2.80 dependent: clear(print_kept). % 2.62/2.80 dependent: clear(print_new_demod). % 2.62/2.80 dependent: clear(print_back_demod). % 2.62/2.80 dependent: clear(print_back_sub). % 2.62/2.80 dependent: set(control_memory). % 2.62/2.80 dependent: assign(max_mem, 12000). % 2.62/2.80 dependent: assign(pick_given_ratio, 4). % 2.62/2.80 dependent: assign(stats_level, 1). % 2.62/2.80 dependent: assign(max_seconds, 10800). % 2.62/2.80 clear(print_given). % 2.62/2.80 % 2.62/2.80 list(usable). % 2.62/2.80 0 [] A=A. % 2.62/2.80 0 [] aux(Y,B,btrue)=mul(n(suc(suc(zero))),Y). % 2.62/2.80 0 [] aux(add(C,B1),B,bfalse)=add(C,add(B1,B)). % 2.62/2.80 0 [] aux(n(X),B,bfalse)=add(n(X),B). % 2.62/2.80 0 [] aux(mul(X,X2),B,bfalse)=add(mul(X,X2),B). % 2.62/2.80 0 [] aux(e_q(X,X2),B,bfalse)=add(e_q(X,X2),B). % 2.62/2.80 0 [] aux(v(X),B,bfalse)=add(v(X),B). % 2.62/2.80 0 [] aux2(Y,B,btrue)=mul(n(suc(suc(zero))),Y). % 2.62/2.80 0 [] aux2(add(C,B1),B,bfalse)=add(C,add(B1,B)). % 2.62/2.80 0 [] aux2(n(X),B,bfalse)=add(n(X),B). % 2.62/2.80 0 [] aux2(mul(X,X2),B,bfalse)=add(mul(X,X2),B). % 2.62/2.80 0 [] aux2(e_q(X,X2),B,bfalse)=add(e_q(X,X2),B). % 2.62/2.80 0 [] aux2(v(X),B,bfalse)=add(v(X),B). % 2.62/2.80 0 [] aux3(A3,B3,btrue)=n(suc(zero)). % 2.62/2.80 0 [] aux3(A3,B3,bfalse)=e_q(A3,B3). % 2.62/2.80 0 [] aux4(A,B,n(zero))=b(B). % 2.62/2.80 0 [] aux4(A,B,n(suc(X4)))=fail4(y(A),b(B)). % 2.62/2.80 0 [] aux4(A,B,add(X,X2))=fail4(y(A),b(B)). % 2.62/2.80 0 [] aux4(A,B,mul(X,X2))=fail4(y(A),b(B)). % 2.62/2.80 0 [] aux4(A,B,e_q(X,X2))=fail4(y(A),b(B)). % 2.62/2.80 0 [] aux4(A,B,v(X))=fail4(y(A),b(B)). % 2.62/2.80 0 [] aux5(C,B2,n(zero))=n(zero). % 2.62/2.80 0 [] aux5(C,B2,n(suc(X15)))=fail23(x5(C),b2(B2)). % 2.62/2.80 0 [] aux5(C,B2,add(X,X2))=fail23(x5(C),b2(B2)). % 2.62/2.80 0 [] aux5(C,B2,mul(X,X2))=fail23(x5(C),b2(B2)). % 2.62/2.80 0 [] aux5(C,B2,e_q(X,X2))=fail23(x5(C),b2(B2)). % 2.62/2.80 0 [] aux5(C,B2,v(X))=fail23(x5(C),b2(B2)). % 2.62/2.80 0 [] aux6(A2,B3,btrue)=n(suc(zero)). % 2.62/2.80 0 [] aux6(A2,B3,bfalse)=e_q(a3(A2),b3(B3)). % 2.62/2.80 0 [] aux7(X,A2,B3,btrue)=suc(zero). % 2.62/2.80 0 [] aux7(X,A2,B3,bfalse)=zero. % 2.62/2.80 0 [] fail1(Y,B)=aux(Y,B,e_q3(Y,B)). % 2.62/2.80 0 [] fail(Y,n(zero))=Y. % 2.62/2.80 0 [] fail(Y,n(suc(X2)))=fail1(Y,n(suc(X2))). % 2.62/2.80 0 [] fail(Y,add(X,X2))=fail1(Y,add(X,X2)). % 2.62/2.80 0 [] fail(Y,mul(X,X2))=fail1(Y,mul(X,X2)). % 2.62/2.80 0 [] fail(Y,e_q(X,X2))=fail1(Y,e_q(X,X2)). % 2.62/2.80 0 [] fail(Y,v(X))=fail1(Y,v(X)). % 2.62/2.80 0 [] fail3(mul(A2,B12),B2)=mul(A2,mul(B12,B2)). % 2.62/2.80 0 [] fail3(n(X),B2)=mul(n(X),B2). % 2.62/2.80 0 [] fail3(add(X,X2),B2)=mul(add(X,X2),B2). % 2.62/2.80 0 [] fail3(e_q(X,X2),B2)=mul(e_q(X,X2),B2). % 2.62/2.80 0 [] fail3(v(X),B2)=mul(v(X),B2). % 2.62/2.80 0 [] fail22(X5,n(zero))=fail3(X5,n(zero)). % 2.62/2.80 0 [] fail22(X5,n(suc(zero)))=X5. % 2.62/2.80 0 [] fail22(X5,n(suc(suc(X8))))=fail3(X5,n(suc(suc(X8)))). % 2.62/2.80 0 [] fail22(X5,add(X,X2))=fail3(X5,add(X,X2)). % 2.62/2.80 0 [] fail22(X5,mul(X,X2))=fail3(X5,mul(X,X2)). % 2.62/2.80 0 [] fail22(X5,e_q(X,X2))=fail3(X5,e_q(X,X2)). % 2.62/2.80 0 [] fail22(X5,v(X))=fail3(X5,v(X)). % 2.62/2.80 0 [] fail12(n(zero),B2)=fail22(n(zero),B2). % 2.62/2.80 0 [] fail12(n(suc(zero)),B2)=B2. % 2.62/2.80 0 [] fail12(n(suc(suc(X11))),B2)=fail22(n(suc(suc(X11))),B2). % 2.62/2.80 0 [] fail12(add(X,X2),B2)=fail22(add(X,X2),B2). % 2.62/2.80 0 [] fail12(mul(X,X2),B2)=fail22(mul(X,X2),B2). % 2.62/2.80 0 [] fail12(e_q(X,X2),B2)=fail22(e_q(X,X2),B2). % 2.62/2.80 0 [] fail12(v(X),B2)=fail22(v(X),B2). % 2.62/2.80 0 [] fail2(X5,n(zero))=n(zero). % 2.62/2.80 0 [] fail2(X5,n(suc(X13)))=fail12(X5,n(suc(X13))). % 2.62/2.80 0 [] fail2(X5,add(X,X2))=fail12(X5,add(X,X2)). % 2.62/2.80 0 [] fail2(X5,mul(X,X2))=fail12(X5,mul(X,X2)). % 2.62/2.80 0 [] fail2(X5,e_q(X,X2))=fail12(X5,e_q(X,X2)). % 2.62/2.80 0 [] fail2(X5,v(X))=fail12(X5,v(X)). % 2.62/2.80 0 [] fail13(Y,B)=aux2(Y,B,e_q3(Y,B)). % 2.62/2.80 0 [] fail4(Y,n(zero))=Y. % 2.62/2.80 0 [] fail4(Y,n(suc(X2)))=fail13(Y,n(suc(X2))). % 2.62/2.80 0 [] fail4(Y,add(X,X2))=fail13(Y,add(X,X2)). % 2.62/2.80 0 [] fail4(Y,mul(X,X2))=fail13(Y,mul(X,X2)). % 2.62/2.80 0 [] fail4(Y,e_q(X,X2))=fail13(Y,e_q(X,X2)). % 2.62/2.80 0 [] fail4(Y,v(X))=fail13(Y,v(X)). % 2.62/2.80 0 [] b(B)=simp4(B). % 2.62/2.80 0 [] y(A)=simp4(A). % 2.62/2.80 0 [] fail32(mul(A2,B12),B2)=mul(A2,mul(B12,B2)). % 2.62/2.80 0 [] fail32(n(X),B2)=mul(n(X),B2). % 2.62/2.80 0 [] fail32(add(X,X2),B2)=mul(add(X,X2),B2). % 2.62/2.80 0 [] fail32(e_q(X,X2),B2)=mul(e_q(X,X2),B2). % 2.62/2.80 0 [] fail32(v(X),B2)=mul(v(X),B2). % 2.62/2.80 0 [] fail222(X5,n(zero))=fail32(X5,n(zero)). % 2.62/2.80 0 [] fail222(X5,n(suc(zero)))=X5. % 2.62/2.80 0 [] fail222(X5,n(suc(suc(X8))))=fail32(X5,n(suc(suc(X8)))). % 2.62/2.80 0 [] fail222(X5,add(X,X2))=fail32(X5,add(X,X2)). % 2.62/2.80 0 [] fail222(X5,mul(X,X2))=fail32(X5,mul(X,X2)). % 2.62/2.80 0 [] fail222(X5,e_q(X,X2))=fail32(X5,e_q(X,X2)). % 2.62/2.81 0 [] fail222(X5,v(X))=fail32(X5,v(X)). % 2.62/2.81 0 [] fail122(n(zero),B2)=fail222(n(zero),B2). % 2.62/2.81 0 [] fail122(n(suc(zero)),B2)=B2. % 2.62/2.81 0 [] fail122(n(suc(suc(X11))),B2)=fail222(n(suc(suc(X11))),B2). % 2.62/2.81 0 [] fail122(add(X,X2),B2)=fail222(add(X,X2),B2). % 2.62/2.81 0 [] fail122(mul(X,X2),B2)=fail222(mul(X,X2),B2). % 2.62/2.81 0 [] fail122(e_q(X,X2),B2)=fail222(e_q(X,X2),B2). % 2.62/2.81 0 [] fail122(v(X),B2)=fail222(v(X),B2). % 2.62/2.81 0 [] fail23(X5,n(zero))=n(zero). % 2.62/2.81 0 [] fail23(X5,n(suc(X13)))=fail122(X5,n(suc(X13))). % 2.62/2.81 0 [] fail23(X5,add(X,X2))=fail122(X5,add(X,X2)). % 2.62/2.81 0 [] fail23(X5,mul(X,X2))=fail122(X5,mul(X,X2)). % 2.62/2.81 0 [] fail23(X5,e_q(X,X2))=fail122(X5,e_q(X,X2)). % 2.62/2.81 0 [] fail23(X5,v(X))=fail122(X5,v(X)). % 2.62/2.81 0 [] b2(B2)=simp4(B2). % 2.62/2.81 0 [] x5(C)=simp4(C). % 2.62/2.81 0 [] b3(B3)=simp4(B3). % 2.62/2.81 0 [] a3(A2)=simp4(A2). % 2.62/2.81 0 [] step4(add(n(zero),B))=B. % 2.62/2.81 0 [] step4(add(n(suc(X4)),B))=fail(n(suc(X4)),B). % 2.62/2.81 0 [] step4(add(add(X,X2),B))=fail(add(X,X2),B). % 2.62/2.81 0 [] step4(add(mul(X,X2),B))=fail(mul(X,X2),B). % 2.62/2.81 0 [] step4(add(e_q(X,X2),B))=fail(e_q(X,X2),B). % 2.62/2.81 0 [] step4(add(v(X),B))=fail(v(X),B). % 2.62/2.81 0 [] step4(mul(n(zero),B2))=n(zero). % 2.62/2.81 0 [] step4(mul(n(suc(X15)),B2))=fail2(n(suc(X15)),B2). % 2.62/2.81 0 [] step4(mul(add(X,X2),B2))=fail2(add(X,X2),B2). % 2.62/2.81 0 [] step4(mul(mul(X,X2),B2))=fail2(mul(X,X2),B2). % 2.62/2.81 0 [] step4(mul(e_q(X,X2),B2))=fail2(e_q(X,X2),B2). % 2.62/2.81 0 [] step4(mul(v(X),B2))=fail2(v(X),B2). % 2.62/2.81 0 [] step4(e_q(A3,B3))=aux3(A3,B3,e_q3(A3,B3)). % 2.62/2.81 0 [] step4(n(X))=n(X). % 2.62/2.81 0 [] step4(v(X))=v(X). % 2.62/2.81 0 [] simp4(add(A,B))=aux4(A,B,y(A)). % 2.62/2.81 0 [] simp4(mul(C,B2))=aux5(C,B2,x5(C)). % 2.62/2.81 0 [] simp4(e_q(A2,B3))=aux6(A2,B3,e_q3(a3(A2),b3(B3))). % 2.62/2.81 0 [] simp4(n(X))=n(X). % 2.62/2.81 0 [] simp4(v(X))=v(X). % 2.62/2.81 0 [] fetch(nil,Y)=zero. % 2.62/2.81 0 [] fetch(cons(N,St),zero)=N. % 2.62/2.81 0 [] fetch(cons(N,St),suc(Z))=fetch(St,Z). % 2.62/2.81 0 [] addNat(zero,Y)=Y. % 2.62/2.81 0 [] addNat(suc(Z),Y)=suc(addNat(Z,Y)). % 2.62/2.81 0 [] mulNat(zero,Y)=zero. % 2.62/2.81 0 [] mulNat(suc(Z),Y)=addNat(Y,mulNat(Z,Y)). % 2.62/2.81 0 [] eval(X,n(N))=N. % 2.62/2.81 0 [] eval(X,add(A,B))=addNat(eval(X,A),eval(X,B)). % 2.62/2.81 0 [] eval(X,mul(C,B2))=mulNat(eval(X,C),eval(X,B2)). % 2.62/2.81 0 [] eval(X,e_q(A2,B3))=aux7(X,A2,B3,e_q2(eval(X,A2),eval(X,B3))). % 2.62/2.81 0 [] eval(X,v(Z))=fetch(X,Z). % 2.62/2.81 0 [] prop4(X,Y)=e_q4(e_q2(eval(X,Y),eval(X,simp4(Y))),btrue). % 2.62/2.81 0 [] e_q4(bfalse,btrue)=bfalse. % 2.62/2.81 0 [] e_q4(btrue,bfalse)=bfalse. % 2.62/2.81 0 [] e_q3(n(X),n(Y))=e_q2(X,Y). % 2.62/2.81 0 [] e_q3(X,Z)!=bfalse|e_q3(add(X,Y),add(Z,X2))=bfalse. % 2.62/2.81 0 [] e_q3(X,Z)!=btrue|e_q3(add(X,Y),add(Z,X2))=e_q3(Y,X2). % 2.62/2.81 0 [] e_q3(X,Z)!=bfalse|e_q3(mul(X,Y),mul(Z,X2))=bfalse. % 2.62/2.81 0 [] e_q3(X,Z)!=btrue|e_q3(mul(X,Y),mul(Z,X2))=e_q3(Y,X2). % 2.62/2.81 0 [] e_q3(X,Z)!=bfalse|e_q3(e_q(X,Y),e_q(Z,X2))=bfalse. % 2.62/2.81 0 [] e_q3(X,Z)!=btrue|e_q3(e_q(X,Y),e_q(Z,X2))=e_q3(Y,X2). % 2.62/2.81 0 [] e_q3(v(X),v(Y))=e_q2(X,Y). % 2.62/2.81 0 [] e_q3(n(X),add(Y,Z))=bfalse. % 2.62/2.81 0 [] e_q3(n(X),mul(Y,Z))=bfalse. % 2.62/2.81 0 [] e_q3(n(X),e_q(Y,Z))=bfalse. % 2.62/2.81 0 [] e_q3(n(X),v(Y))=bfalse. % 2.62/2.81 0 [] e_q3(add(X,Y),n(Z))=bfalse. % 2.62/2.81 0 [] e_q3(add(X,Y),mul(Z,X2))=bfalse. % 2.62/2.81 0 [] e_q3(add(X,Y),e_q(Z,X2))=bfalse. % 2.62/2.81 0 [] e_q3(add(X,Y),v(Z))=bfalse. % 2.62/2.81 0 [] e_q3(mul(X,Y),n(Z))=bfalse. % 2.62/2.81 0 [] e_q3(mul(X,Y),add(Z,X2))=bfalse. % 2.62/2.81 0 [] e_q3(mul(X,Y),e_q(Z,X2))=bfalse. % 2.62/2.81 0 [] e_q3(mul(X,Y),v(Z))=bfalse. % 2.62/2.81 0 [] e_q3(e_q(X,Y),n(Z))=bfalse. % 2.62/2.81 0 [] e_q3(e_q(X,Y),add(Z,X2))=bfalse. % 2.62/2.81 0 [] e_q3(e_q(X,Y),mul(Z,X2))=bfalse. % 2.62/2.81 0 [] e_q3(e_q(X,Y),v(Z))=bfalse. % 2.62/2.81 0 [] e_q3(v(X),n(Y))=bfalse. % 2.62/2.81 0 [] e_q3(v(X),add(Y,Z))=bfalse. % 2.62/2.81 0 [] e_q3(v(X),mul(Y,Z))=bfalse. % 2.62/2.81 0 [] e_q3(v(X),e_q(Y,Z))=bfalse. % 2.62/2.81 0 [] e_q2(suc(X),suc(Y))=e_q2(X,Y). % 2.62/2.81 0 [] e_q2(zero,suc(X))=bfalse. % 2.62/2.81 0 [] e_q2(suc(X),zero)=bfalse. % 2.62/2.81 0 [] e_q2(X,X)=btrue. % 2.62/2.81 0 [] e_q3(X,X)=btrue. % 2.62/2.81 0 [] e_q4(X,X)=btrue. % 2.62/2.81 0 [] e_q4(prop4(X,Y),bfalse)!=btrue. % 2.62/2.81 end_of_list. % 2.62/2.81 % 2.62/2.81 SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=2. % 2.62/2.81 % 2.62/2.81 This is a Horn set with equality. The strategy will be % 2.62/2.81 Knuth-Bendix and hyper_res, with positive clauses in % 2.62/2.81 sos and nonpositive clauses in usable. % 2.62/2.81 % 2.62/2.81 dependent: set(knuth_bendix). % 2.62/2.81 dependent: set(anl_eq). % 2.62/2.81 dependent: set(para_from). % 2.62/2.81 dependent: set(para_into). % 2.62/2.81 dependent: clear(para_from_right). % 2.62/2.81 dependent: clear(para_into_right). % 2.62/2.81 dependent: set(para_from_vars). % 2.62/2.81 dependent: set(eq_units_both_ways). % 2.62/2.81 dependent: set(dynamic_demod_all). % 2.62/2.81 dependent: set(dynamic_demod). % 2.62/2.81 dependent: set(order_eq). % 2.62/2.81 dependent: set(back_demod). % 2.62/2.81 dependent: set(lrpo). % 2.62/2.81 dependent: set(hyper_res). % 2.62/2.81 dependent: clear(order_hyper). % 2.62/2.81 % 2.62/2.81 ------------> process usable: % 2.62/2.81 ** KEPT (pick-wt=14): 1 [] e_q3(A,B)!=bfalse|e_q3(add(A,C),add(B,D))=bfalse. % 2.62/2.81 ** KEPT (pick-wt=16): 2 [] e_q3(A,B)!=btrue|e_q3(add(A,C),add(B,D))=e_q3(C,D). % 2.62/2.81 ** KEPT (pick-wt=14): 3 [] e_q3(A,B)!=bfalse|e_q3(mul(A,C),mul(B,D))=bfalse. % 2.62/2.81 ** KEPT (pick-wt=16): 4 [] e_q3(A,B)!=btrue|e_q3(mul(A,C),mul(B,D))=e_q3(C,D). % 2.62/2.81 ** KEPT (pick-wt=14): 5 [] e_q3(A,B)!=bfalse|e_q3(e_q(A,C),e_q(B,D))=bfalse. % 2.62/2.81 ** KEPT (pick-wt=16): 6 [] e_q3(A,B)!=btrue|e_q3(e_q(A,C),e_q(B,D))=e_q3(C,D). % 2.62/2.81 ** KEPT (pick-wt=7): 7 [] e_q4(prop4(A,B),bfalse)!=btrue. % 2.62/2.81 % 2.62/2.81 ------------> process sos: % 2.62/2.81 ** KEPT (pick-wt=3): 8 [] A=A. % 2.62/2.81 ** KEPT (pick-wt=11): 9 [] aux(A,B,btrue)=mul(n(suc(suc(zero))),A). % 2.62/2.81 ** KEPT (pick-wt=12): 11 [copy,10,flip.1] add(A,add(B,C))=aux(add(A,B),C,bfalse). % 2.62/2.81 ---> New Demodulator: 12 [new_demod,11] add(A,add(B,C))=aux(add(A,B),C,bfalse). % 2.62/2.81 ** KEPT (pick-wt=10): 14 [copy,13,flip.1] add(n(A),B)=aux(n(A),B,bfalse). % 2.62/2.81 ---> New Demodulator: 15 [new_demod,14] add(n(A),B)=aux(n(A),B,bfalse). % 2.62/2.81 ** KEPT (pick-wt=12): 17 [copy,16,flip.1] add(mul(A,B),C)=aux(mul(A,B),C,bfalse). % 2.62/2.81 ---> New Demodulator: 18 [new_demod,17] add(mul(A,B),C)=aux(mul(A,B),C,bfalse). % 2.62/2.81 ** KEPT (pick-wt=12): 20 [copy,19,flip.1] add(e_q(A,B),C)=aux(e_q(A,B),C,bfalse). % 2.62/2.81 ---> New Demodulator: 21 [new_demod,20] add(e_q(A,B),C)=aux(e_q(A,B),C,bfalse). % 2.62/2.81 ** KEPT (pick-wt=10): 23 [copy,22,flip.1] add(v(A),B)=aux(v(A),B,bfalse). % 2.62/2.81 ---> New Demodulator: 24 [new_demod,23] add(v(A),B)=aux(v(A),B,bfalse). % 2.62/2.81 ** KEPT (pick-wt=11): 25 [] aux2(A,B,btrue)=mul(n(suc(suc(zero))),A). % 2.62/2.81 ** KEPT (pick-wt=13): 27 [copy,26,demod,12] aux2(add(A,B),C,bfalse)=aux(add(A,B),C,bfalse). % 2.62/2.81 ---> New Demodulator: 28 [new_demod,27] aux2(add(A,B),C,bfalse)=aux(add(A,B),C,bfalse). % 2.62/2.81 ** KEPT (pick-wt=11): 30 [copy,29,demod,15] aux2(n(A),B,bfalse)=aux(n(A),B,bfalse). % 2.62/2.81 ---> New Demodulator: 31 [new_demod,30] aux2(n(A),B,bfalse)=aux(n(A),B,bfalse). % 2.62/2.81 ** KEPT (pick-wt=13): 33 [copy,32,demod,18] aux2(mul(A,B),C,bfalse)=aux(mul(A,B),C,bfalse). % 2.62/2.81 ---> New Demodulator: 34 [new_demod,33] aux2(mul(A,B),C,bfalse)=aux(mul(A,B),C,bfalse). % 2.62/2.81 ** KEPT (pick-wt=13): 36 [copy,35,demod,21] aux2(e_q(A,B),C,bfalse)=aux(e_q(A,B),C,bfalse). % 2.62/2.81 ---> New Demodulator: 37 [new_demod,36] aux2(e_q(A,B),C,bfalse)=aux(e_q(A,B),C,bfalse). % 2.62/2.81 ** KEPT (pick-wt=11): 39 [copy,38,demod,24] aux2(v(A),B,bfalse)=aux(v(A),B,bfalse). % 2.62/2.81 ---> New Demodulator: 40 [new_demod,39] aux2(v(A),B,bfalse)=aux(v(A),B,bfalse). % 2.62/2.81 ** KEPT (pick-wt=8): 41 [] aux3(A,B,btrue)=n(suc(zero)). % 2.62/2.81 ** KEPT (pick-wt=8): 43 [copy,42,flip.1] e_q(A,B)=aux3(A,B,bfalse). % 2.62/2.81 ---> New Demodulator: 44 [new_demod,43] e_q(A,B)=aux3(A,B,bfalse). % 2.62/2.81 ** KEPT (pick-wt=8): 45 [] aux4(A,B,n(zero))=b(B). % 2.62/2.81 ** KEPT (pick-wt=12): 46 [] aux4(A,B,n(suc(C)))=fail4(y(A),b(B)). % 2.62/2.81 ** KEPT (pick-wt=12): 47 [] aux4(A,B,add(C,D))=fail4(y(A),b(B)). % 2.62/2.81 ** KEPT (pick-wt=12): 48 [] aux4(A,B,mul(C,D))=fail4(y(A),b(B)). % 2.62/2.81 ** KEPT (pick-wt=13): 50 [copy,49,demod,44] aux4(A,B,aux3(C,D,bfalse))=fail4(y(A),b(B)). % 2.62/2.81 ** KEPT (pick-wt=11): 51 [] aux4(A,B,v(C))=fail4(y(A),b(B)). % 2.62/2.81 ** KEPT (pick-wt=8): 52 [] aux5(A,B,n(zero))=n(zero). % 2.62/2.81 ---> New Demodulator: 53 [new_demod,52] aux5(A,B,n(zero))=n(zero). % 2.62/2.81 ** KEPT (pick-wt=12): 54 [] aux5(A,B,n(suc(C)))=fail23(x5(A),b2(B)). % 2.62/2.81 ** KEPT (pick-wt=12): 55 [] aux5(A,B,add(C,D))=fail23(x5(A),b2(B)). % 2.62/2.81 ** KEPT (pick-wt=12): 56 [] aux5(A,B,mul(C,D))=fail23(x5(A),b2(B)). % 2.62/2.81 ** KEPT (pick-wt=13): 58 [copy,57,demod,44] aux5(A,B,aux3(C,D,bfalse))=fail23(x5(A),b2(B)). % 2.62/2.81 ** KEPT (pick-wt=11): 59 [] aux5(A,B,v(C))=fail23(x5(A),b2(B)). % 2.62/2.81 ** KEPT (pick-wt=8): 60 [] aux6(A,B,btrue)=n(suc(zero)). % 2.62/2.81 ** KEPT (pick-wt=11): 62 [copy,61,demod,44] aux6(A,B,bfalse)=aux3(a3(A),b3(B),bfalse). % 2.62/2.81 ** KEPT (pick-wt=8): 63 [] aux7(A,B,C,btrue)=suc(zero). % 2.62/2.81 ** KEPT (pick-wt=7): 64 [] aux7(A,B,C,bfalse)=zero. % 2.62/2.81 ---> New Demodulator: 65 [new_demod,64] aux7(A,B,C,bfalse)=zero. % 2.62/2.81 ** KEPT (pick-wt=10): 66 [] fail1(A,B)=aux(A,B,e_q3(A,B)). % 2.62/2.81 ---> New Demodulator: 67 [new_demod,66] fail1(A,B)=aux(A,B,e_q3(A,B)). % 2.62/2.81 ** KEPT (pick-wt=6): 68 [] fail(A,n(zero))=A. % 2.62/2.81 ---> New Demodulator: 69 [new_demod,68] fail(A,n(zero))=A. % 2.62/2.81 ** KEPT (pick-wt=16): 71 [copy,70,demod,67] fail(A,n(suc(B)))=aux(A,n(suc(B)),e_q3(A,n(suc(B)))). % 2.62/2.81 ---> New Demodulator: 72 [new_demod,71] fail(A,n(suc(B)))=aux(A,n(suc(B)),e_q3(A,n(suc(B)))). % 2.62/2.81 ** KEPT (pick-wt=16): 74 [copy,73,demod,67] fail(A,add(B,C))=aux(A,add(B,C),e_q3(A,add(B,C))). % 2.62/2.81 ---> New Demodulator: 75 [new_demod,74] fail(A,add(B,C))=aux(A,add(B,C),e_q3(A,add(B,C))). % 2.62/2.81 ** KEPT (pick-wt=16): 77 [copy,76,demod,67] fail(A,mul(B,C))=aux(A,mul(B,C),e_q3(A,mul(B,C))). % 2.62/2.81 ---> New Demodulator: 78 [new_demod,77] fail(A,mul(B,C))=aux(A,mul(B,C),e_q3(A,mul(B,C))). % 2.62/2.81 ** KEPT (pick-wt=19): 80 [copy,79,demod,44,44,67] fail(A,aux3(B,C,bfalse))=aux(A,aux3(B,C,bfalse),e_q3(A,aux3(B,C,bfalse))). % 2.62/2.81 ---> New Demodulator: 81 [new_demod,80] fail(A,aux3(B,C,bfalse))=aux(A,aux3(B,C,bfalse),e_q3(A,aux3(B,C,bfalse))). % 2.62/2.81 ** KEPT (pick-wt=13): 83 [copy,82,demod,67] fail(A,v(B))=aux(A,v(B),e_q3(A,v(B))). % 2.62/2.81 ---> New Demodulator: 84 [new_demod,83] fail(A,v(B))=aux(A,v(B),e_q3(A,v(B))). % 2.62/2.81 ** KEPT (pick-wt=11): 86 [copy,85,flip.1] mul(A,mul(B,C))=fail3(mul(A,B),C). % 2.62/2.81 ---> New Demodulator: 87 [new_demod,86] mul(A,mul(B,C))=fail3(mul(A,B),C). % 2.62/2.81 ** KEPT (pick-wt=9): 89 [copy,88,flip.1] mul(n(A),B)=fail3(n(A),B). % 2.62/2.81 ---> New Demodulator: 90 [new_demod,89] mul(n(A),B)=fail3(n(A),B). % 2.62/2.81 ** KEPT (pick-wt=11): 92 [copy,91,flip.1] mul(add(A,B),C)=fail3(add(A,B),C). % 2.62/2.81 ---> New Demodulator: 93 [new_demod,92] mul(add(A,B),C)=fail3(add(A,B),C). % 2.62/2.81 ** KEPT (pick-wt=13): 95 [copy,94,demod,44,44,flip.1] mul(aux3(A,B,bfalse),C)=fail3(aux3(A,B,bfalse),C). % 2.62/2.81 ---> New Demodulator: 96 [new_demod,95] mul(aux3(A,B,bfalse),C)=fail3(aux3(A,B,bfalse),C). % 2.62/2.81 ** KEPT (pick-wt=9): 98 [copy,97,flip.1] mul(v(A),B)=fail3(v(A),B). % 2.62/2.81 ---> New Demodulator: 99 [new_demod,98] mul(v(A),B)=fail3(v(A),B). % 2.62/2.81 ** KEPT (pick-wt=9): 101 [copy,100,flip.1] fail3(A,n(zero))=fail22(A,n(zero)). % 2.62/2.81 ---> New Demodulator: 102 [new_demod,101] fail3(A,n(zero))=fail22(A,n(zero)). % 2.62/2.81 ** KEPT (pick-wt=7): 103 [] fail22(A,n(suc(zero)))=A. % 2.62/2.81 ---> New Demodulator: 104 [new_demod,103] fail22(A,n(suc(zero)))=A. % 2.62/2.81 ** KEPT (pick-wt=13): 106 [copy,105,flip.1] fail3(A,n(suc(suc(B))))=fail22(A,n(suc(suc(B)))). % 2.62/2.81 ---> New Demodulator: 107 [new_demod,106] fail3(A,n(suc(suc(B))))=fail22(A,n(suc(suc(B)))). % 2.62/2.81 ** KEPT (pick-wt=11): 109 [copy,108,flip.1] fail3(A,add(B,C))=fail22(A,add(B,C)). % 2.62/2.81 ---> New Demodulator: 110 [new_demod,109] fail3(A,add(B,C))=fail22(A,add(B,C)). % 2.62/2.81 ** KEPT (pick-wt=11): 112 [copy,111,flip.1] fail3(A,mul(B,C))=fail22(A,mul(B,C)). % 2.62/2.81 ---> New Demodulator: 113 [new_demod,112] fail3(A,mul(B,C))=fail22(A,mul(B,C)). % 2.62/2.81 ** KEPT (pick-wt=13): 115 [copy,114,demod,44,44,flip.1] fail3(A,aux3(B,C,bfalse))=fail22(A,aux3(B,C,bfalse)). % 2.62/2.81 ---> New Demodulator: 116 [new_demod,115] fail3(A,aux3(B,C,bfalse))=fail22(A,aux3(B,C,bfalse)). % 2.62/2.81 ** KEPT (pick-wt=9): 118 [copy,117,flip.1] fail3(A,v(B))=fail22(A,v(B)). % 2.62/2.81 ---> New Demodulator: 119 [new_demod,118] fail3(A,v(B))=fail22(A,v(B)). % 2.62/2.81 ** KEPT (pick-wt=9): 121 [copy,120,flip.1] fail22(n(zero),A)=fail12(n(zero),A). % 2.62/2.81 ---> New Demodulator: 122 [new_demod,121] fail22(n(zero),A)=fail12(n(zero),A). % 2.62/2.81 ** KEPT (pick-wt=7): 123 [] fail12(n(suc(zero)),A)=A. % 2.62/2.81 ---> New Demodulator: 124 [new_demod,123] fail12(n(suc(zero)),A)=A. % 2.62/2.81 ** KEPT (pick-wt=13): 126 [copy,125,flip.1] fail22(n(suc(suc(A))),B)=fail12(n(suc(suc(A))),B). % 2.62/2.81 ---> New Demodulator: 127 [new_demod,126] fail22(n(suc(suc(A))),B)=fail12(n(suc(suc(A))),B). % 2.62/2.81 ** KEPT (pick-wt=11): 129 [copy,128,flip.1] fail22(add(A,B),C)=fail12(add(A,B),C). % 2.62/2.81 ---> New Demodulator: 130 [new_demod,129] fail22(add(A,B),C)=fail12(add(A,B),C). % 2.62/2.81 ** KEPT (pick-wt=11): 132 [copy,131,flip.1] fail22(mul(A,B),C)=fail12(mul(A,B),C). % 2.62/2.81 ---> New Demodulator: 133 [new_demod,132] fail22(mul(A,B),C)=fail12(mul(A,B),C). % 2.62/2.81 ** KEPT (pick-wt=13): 135 [copy,134,demod,44,44,flip.1] fail22(aux3(A,B,bfalse),C)=fail12(aux3(A,B,bfalse),C). % 2.62/2.81 ---> New Demodulator: 136 [new_demod,135] fail22(aux3(A,B,bfalse),C)=fail12(aux3(A,B,bfalse),C). % 2.62/2.81 ** KEPT (pick-wt=9): 138 [copy,137,flip.1] fail22(v(A),B)=fail12(v(A),B). % 2.62/2.81 ---> New Demodulator: 139 [new_demod,138] fail22(v(A),B)=fail12(v(A),B). % 2.62/2.81 ** KEPT (pick-wt=7): 140 [] fail2(A,n(zero))=n(zero). % 2.62/2.81 ---> New Demodulator: 141 [new_demod,140] fail2(A,n(zero))=n(zero). % 2.62/2.81 ** KEPT (pick-wt=11): 142 [] fail2(A,n(suc(B)))=fail12(A,n(suc(B))). % 2.62/2.81 ---> New Demodulator: 143 [new_demod,142] fail2(A,n(suc(B)))=fail12(A,n(suc(B))). % 2.62/2.81 ** KEPT (pick-wt=11): 144 [] fail2(A,add(B,C))=fail12(A,add(B,C)). % 2.62/2.81 ---> New Demodulator: 145 [new_demod,144] fail2(A,add(B,C))=fail12(A,add(B,C)). % 2.62/2.81 ** KEPT (pick-wt=11): 146 [] fail2(A,mul(B,C))=fail12(A,mul(B,C)). % 2.62/2.81 ---> New Demodulator: 147 [new_demod,146] fail2(A,mul(B,C))=fail12(A,mul(B,C)). % 2.62/2.81 ** KEPT (pick-wt=13): 149 [copy,148,demod,44,44] fail2(A,aux3(B,C,bfalse))=fail12(A,aux3(B,C,bfalse)). % 2.62/2.81 ---> New Demodulator: 150 [new_demod,149] fail2(A,aux3(B,C,bfalse))=fail12(A,aux3(B,C,bfalse)). % 2.62/2.81 ** KEPT (pick-wt=9): 151 [] fail2(A,v(B))=fail12(A,v(B)). % 2.62/2.81 ---> New Demodulator: 152 [new_demod,151] fail2(A,v(B))=fail12(A,v(B)). % 2.62/2.81 ** KEPT (pick-wt=10): 153 [] fail13(A,B)=aux2(A,B,e_q3(A,B)). % 2.62/2.81 ---> New Demodulator: 154 [new_demod,153] fail13(A,B)=aux2(A,B,e_q3(A,B)). % 2.62/2.81 ** KEPT (pick-wt=6): 155 [] fail4(A,n(zero))=A. % 2.62/2.81 ---> New Demodulator: 156 [new_demod,155] fail4(A,n(zero))=A. % 2.62/2.81 ** KEPT (pick-wt=16): 158 [copy,157,demod,154] fail4(A,n(suc(B)))=aux2(A,n(suc(B)),e_q3(A,n(suc(B)))). % 2.62/2.81 ---> New Demodulator: 159 [new_demod,158] fail4(A,n(suc(B)))=aux2(A,n(suc(B)),e_q3(A,n(suc(B)))). % 2.62/2.81 ** KEPT (pick-wt=16): 161 [copy,160,demod,154] fail4(A,add(B,C))=aux2(A,add(B,C),e_q3(A,add(B,C))). % 2.62/2.81 ---> New Demodulator: 162 [new_demod,161] fail4(A,add(B,C))=aux2(A,add(B,C),e_q3(A,add(B,C))). % 2.62/2.81 ** KEPT (pick-wt=16): 164 [copy,163,demod,154] fail4(A,mul(B,C))=aux2(A,mul(B,C),e_q3(A,mul(B,C))). % 2.62/2.81 ---> New Demodulator: 165 [new_demod,164] fail4(A,mul(B,C))=aux2(A,mul(B,C),e_q3(A,mul(B,C))). % 2.62/2.81 ** KEPT (pick-wt=19): 167 [copy,166,demod,44,44,154] fail4(A,aux3(B,C,bfalse))=aux2(A,aux3(B,C,bfalse),e_q3(A,aux3(B,C,bfalse))). % 2.62/2.81 ---> New Demodulator: 168 [new_demod,167] fail4(A,aux3(B,C,bfalse))=aux2(A,aux3(B,C,bfalse),e_q3(A,aux3(B,C,bfalse))). % 2.62/2.81 ** KEPT (pick-wt=13): 170 [copy,169,demod,154] fail4(A,v(B))=aux2(A,v(B),e_q3(A,v(B))). % 2.62/2.81 ---> New Demodulator: 171 [new_demod,170] fail4(A,v(B))=aux2(A,v(B),e_q3(A,v(B))). % 2.62/2.81 ** KEPT (pick-wt=5): 173 [copy,172,flip.1] simp4(A)=b(A). % 2.62/2.81 ---> New Demodulator: 174 [new_demod,173] simp4(A)=b(A). % 2.62/2.81 ** KEPT (pick-wt=5): 176 [copy,175,demod,174] y(A)=b(A). % 2.62/2.81 ---> New Demodulator: 177 [new_demod,176] y(A)=b(A). % 2.62/2.81 ** KEPT (pick-wt=11): 179 [copy,178,demod,87] fail32(mul(A,B),C)=fail3(mul(A,B),C). % 2.62/2.81 ---> New Demodulator: 180 [new_demod,179] fail32(mul(A,B),C)=fail3(mul(A,B),C). % 2.62/2.81 ** KEPT (pick-wt=9): 182 [copy,181,demod,90] fail32(n(A),B)=fail3(n(A),B). % 2.62/2.81 ---> New Demodulator: 183 [new_demod,182] fail32(n(A),B)=fail3(n(A),B). % 2.62/2.81 ** KEPT (pick-wt=11): 185 [copy,184,demod,93] fail32(add(A,B),C)=fail3(add(A,B),C). % 2.62/2.81 ---> New Demodulator: 186 [new_demod,185] fail32(add(A,B),C)=fail3(add(A,B),C). % 2.62/2.81 ** KEPT (pick-wt=13): 188 [copy,187,demod,44,44,96] fail32(aux3(A,B,bfalse),C)=fail3(aux3(A,B,bfalse),C). % 2.62/2.81 ---> New Demodulator: 189 [new_demod,188] fail32(aux3(A,B,bfalse),C)=fail3(aux3(A,B,bfalse),C). % 2.62/2.81 ** KEPT (pick-wt=9): 191 [copy,190,demod,99] fail32(v(A),B)=fail3(v(A),B). % 2.62/2.81 ---> New Demodulator: 192 [new_demod,191] fail32(v(A),B)=fail3(v(A),B). % 2.62/2.81 ** KEPT (pick-wt=9): 194 [copy,193,flip.1] fail32(A,n(zero))=fail222(A,n(zero)). % 2.62/2.81 ---> New Demodulator: 195 [new_demod,194] fail32(A,n(zero))=fail222(A,n(zero)). % 2.62/2.81 ** KEPT (pick-wt=7): 196 [] fail222(A,n(suc(zero)))=A. % 2.62/2.81 ---> New Demodulator: 197 [new_demod,196] fail222(A,n(suc(zero)))=A. % 2.62/2.81 ** KEPT (pick-wt=13): 199 [copy,198,flip.1] fail32(A,n(suc(suc(B))))=fail222(A,n(suc(suc(B)))). % 2.62/2.81 ---> New Demodulator: 200 [new_demod,199] fail32(A,n(suc(suc(B))))=fail222(A,n(suc(suc(B)))). % 2.62/2.81 ** KEPT (pick-wt=11): 202 [copy,201,flip.1] fail32(A,add(B,C))=fail222(A,add(B,C)). % 2.62/2.81 ---> New Demodulator: 203 [new_demod,202] fail32(A,add(B,C))=fail222(A,add(B,C)). % 2.62/2.81 ** KEPT (pick-wt=11): 205 [copy,204,flip.1] fail32(A,mul(B,C))=fail222(A,mul(B,C)). % 2.62/2.81 ---> New Demodulator: 206 [new_demod,205] fail32(A,mul(B,C))=fail222(A,mul(B,C)). % 2.62/2.81 ** KEPT (pick-wt=13): 208 [copy,207,demod,44,44,flip.1] fail32(A,aux3(B,C,bfalse))=fail222(A,aux3(B,C,bfalse)). % 2.62/2.81 ---> New Demodulator: 209 [new_demod,208] fail32(A,aux3(B,C,bfalse))=fail222(A,aux3(B,C,bfalse)). % 2.62/2.81 ** KEPT (pick-wt=9): 211 [copy,210,flip.1] fail32(A,v(B))=fail222(A,v(B)). % 2.62/2.81 ---> New Demodulator: 212 [new_demod,211] fail32(A,v(B))=fail222(A,v(B)). % 2.62/2.81 ** KEPT (pick-wt=9): 214 [copy,213,flip.1] fail222(n(zero),A)=fail122(n(zero),A). % 2.62/2.81 ---> New Demodulator: 215 [new_demod,214] fail222(n(zero),A)=fail122(n(zero),A). % 2.62/2.81 ** KEPT (pick-wt=7): 216 [] fail122(n(suc(zero)),A)=A. % 2.62/2.81 ---> New Demodulator: 217 [new_demod,216] fail122(n(suc(zero)),A)=A. % 2.62/2.81 ** KEPT (pick-wt=13): 219 [copy,218,flip.1] fail222(n(suc(suc(A))),B)=fail122(n(suc(suc(A))),B). % 2.62/2.81 ---> New Demodulator: 220 [new_demod,219] fail222(n(suc(suc(A))),B)=fail122(n(suc(suc(A))),B). % 2.62/2.81 ** KEPT (pick-wt=11): 222 [copy,221,flip.1] fail222(add(A,B),C)=fail122(add(A,B),C). % 2.62/2.81 ---> New Demodulator: 223 [new_demod,222] fail222(add(A,B),C)=fail122(add(A,B),C). % 2.62/2.81 ** KEPT (pick-wt=11): 225 [copy,224,flip.1] fail222(mul(A,B),C)=fail122(mul(A,B),C). % 2.62/2.81 ---> New Demodulator: 226 [new_demod,225] fail222(mul(A,B),C)=fail122(mul(A,B),C). % 2.62/2.81 ** KEPT (pick-wt=13): 228 [copy,227,demod,44,44,flip.1] fail222(aux3(A,B,bfalse),C)=fail122(aux3(A,B,bfalse),C). % 2.62/2.81 ---> New Demodulator: 229 [new_demod,228] fail222(aux3(A,B,bfalse),C)=fail122(aux3(A,B,bfalse),C). % 2.62/2.81 ** KEPT (pick-wt=9): 231 [copy,230,flip.1] fail222(v(A),B)=fail122(v(A),B). % 2.62/2.81 ---> New Demodulator: 232 [new_demod,231] fail222(v(A),B)=fail122(v(A),B). % 2.62/2.81 ** KEPT (pick-wt=7): 233 [] fail23(A,n(zero))=n(zero). % 2.62/2.81 ---> New Demodulator: 234 [new_demod,233] fail23(A,n(zero))=n(zero). % 2.62/2.81 ** KEPT (pick-wt=11): 235 [] fail23(A,n(suc(B)))=fail122(A,n(suc(B))). % 2.62/2.81 ---> New Demodulator: 236 [new_demod,235] fail23(A,n(suc(B)))=fail122(A,n(suc(B))). % 2.62/2.81 ** KEPT (pick-wt=11): 237 [] fail23(A,add(B,C))=fail122(A,add(B,C)). % 2.62/2.81 ---> New Demodulator: 238 [new_demod,237] fail23(A,add(B,C))=fail122(A,add(B,C)). % 2.62/2.81 ** KEPT (pick-wt=11): 239 [] fail23(A,mul(B,C))=fail122(A,mul(B,C)). % 2.62/2.81 ---> New Demodulator: 240 [new_demod,239] fail23(A,mul(B,C))=fail122(A,mul(B,C)). % 2.62/2.81 ** KEPT (pick-wt=13): 242 [copy,241,demod,44,44] fail23(A,aux3(B,C,bfalse))=fail122(A,aux3(B,C,bfalse)). % 2.62/2.81 ---> New Demodulator: 243 [new_demod,242] fail23(A,aux3(B,C,bfalse))=fail122(A,aux3(B,C,bfalse)). % 2.62/2.81 ** KEPT (pick-wt=9): 244 [] fail23(A,v(B))=fail122(A,v(B)). % 2.62/2.81 ---> New Demodulator: 245 [new_demod,244] fail23(A,v(B))=fail122(A,v(B)). % 2.62/2.81 ** KEPT (pick-wt=5): 247 [copy,246,demod,174] b2(A)=b(A). % 2.62/2.81 ---> New Demodulator: 248 [new_demod,247] b2(A)=b(A). % 2.62/2.81 ** KEPT (pick-wt=5): 250 [copy,249,demod,174] x5(A)=b(A). % 2.62/2.81 ---> New Demodulator: 251 [new_demod,250] x5(A)=b(A). % 2.62/2.81 ** KEPT (pick-wt=5): 253 [copy,252,demod,174] b3(A)=b(A). % 2.62/2.81 ---> New Demodulator: 254 [new_demod,253] b3(A)=b(A). % 2.62/2.81 ** KEPT (pick-wt=5): 256 [copy,255,demod,174,flip.1] b(A)=a3(A). % 2.62/2.81 ---> New Demodulator: 257 [new_demod,256] b(A)=a3(A). % 2.62/2.81 ** KEPT (pick-wt=8): 259 [copy,258,demod,15] step4(aux(n(zero),A,bfalse))=A. % 2.62/2.81 ---> New Demodulator: 260 [new_demod,259] step4(aux(n(zero),A,bfalse))=A. % 2.62/2.81 ** KEPT (pick-wt=13): 262 [copy,261,demod,15] step4(aux(n(suc(A)),B,bfalse))=fail(n(suc(A)),B). % 2.62/2.81 ---> New Demodulator: 263 [new_demod,262] step4(aux(n(suc(A)),B,bfalse))=fail(n(suc(A)),B). % 2.62/2.81 ** KEPT (pick-wt=12): 264 [] step4(add(add(A,B),C))=fail(add(A,B),C). % 2.62/2.81 ---> New Demodulator: 265 [new_demod,264] step4(add(add(A,B),C))=fail(add(A,B),C). % 2.62/2.81 ** KEPT (pick-wt=13): 267 [copy,266,demod,18] step4(aux(mul(A,B),C,bfalse))=fail(mul(A,B),C). % 2.62/2.81 ---> New Demodulator: 268 [new_demod,267] step4(aux(mul(A,B),C,bfalse))=fail(mul(A,B),C). % 2.62/2.81 ** KEPT (pick-wt=14): 270 [copy,269,demod,44,44] step4(add(aux3(A,B,bfalse),C))=fail(aux3(A,B,bfalse),C). % 2.62/2.81 ---> New Demodulator: 271 [new_demod,270] step4(add(aux3(A,B,bfalse),C))=fail(aux3(A,B,bfalse),C). % 2.62/2.81 ** KEPT (pick-wt=11): 273 [copy,272,demod,24] step4(aux(v(A),B,bfalse))=fail(v(A),B). % 2.62/2.81 ---> New Demodulator: 274 [new_demod,273] step4(aux(v(A),B,bfalse))=fail(v(A),B). % 2.62/2.81 ** KEPT (pick-wt=8): 276 [copy,275,demod,90] step4(fail3(n(zero),A))=n(zero). % 2.62/2.81 ---> New Demodulator: 277 [new_demod,276] step4(fail3(n(zero),A))=n(zero). % 2.62/2.81 ** KEPT (pick-wt=12): 279 [copy,278,demod,90] step4(fail3(n(suc(A)),B))=fail2(n(suc(A)),B). % 2.62/2.81 ---> New Demodulator: 280 [new_demod,279] step4(fail3(n(suc(A)),B))=fail2(n(suc(A)),B). % 2.62/2.81 ** KEPT (pick-wt=12): 282 [copy,281,demod,93] step4(fail3(add(A,B),C))=fail2(add(A,B),C). % 2.62/2.81 ---> New Demodulator: 283 [new_demod,282] step4(fail3(add(A,B),C))=fail2(add(A,B),C). % 2.62/2.81 ** KEPT (pick-wt=12): 284 [] step4(mul(mul(A,B),C))=fail2(mul(A,B),C). % 2.62/2.81 ---> New Demodulator: 285 [new_demod,284] step4(mul(mul(A,B),C))=fail2(mul(A,B),C). % 2.62/2.81 ** KEPT (pick-wt=14): 287 [copy,286,demod,44,96,44] step4(fail3(aux3(A,B,bfalse),C))=fail2(aux3(A,B,bfalse),C). % 2.62/2.81 ---> New Demodulator: 288 [new_demod,287] step4(fail3(aux3(A,B,bfalse),C))=fail2(aux3(A,B,bfalse),C). % 2.62/2.81 ** KEPT (pick-wt=10): 290 [copy,289,demod,99] step4(fail3(v(A),B))=fail2(v(A),B). % 2.62/2.81 ---> New Demodulator: 291 [new_demod,290] step4(fail3(v(A),B))=fail2(v(A),B). % 2.62/2.81 ** KEPT (pick-wt=12): 293 [copy,292,demod,44] step4(aux3(A,B,bfalse))=aux3(A,B,e_q3(A,B)). % 2.62/2.81 ---> New Demodulator: 294 [new_demod,293] step4(aux3(A,B,bfalse))=aux3(A,B,e_q3(A,B)). % 2.62/2.81 ** KEPT (pick-wt=6): 295 [] step4(n(A))=n(A). % 2.62/2.81 ---> New Demodulator: 296 [new_demod,295] step4(n(A))=n(A). % 2.62/2.81 ** KEPT (pick-wt=6): 297 [] step4(v(A))=v(A). % 2.62/2.81 ---> New Demodulator: 298 [new_demod,297] step4(v(A))=v(A). % 2.62/2.81 ** KEPT (pick-wt=10): 300 [copy,299,demod,174,257,177,257] a3(add(A,B))=aux4(A,B,a3(A)). % 2.62/2.81 ---> New Demodulator: 301 [new_demod,300] a3(add(A,B))=aux4(A,B,a3(A)). % 2.62/2.81 ** KEPT (pick-wt=10): 303 [copy,302,demod,174,257,251,257] a3(mul(A,B))=aux5(A,B,a3(A)). % 2.62/2.81 ---> New Demodulator: 304 [new_demod,303] a3(mul(A,B))=aux5(A,B,a3(A)). % 2.62/2.81 ** KEPT (pick-wt=14): 306 [copy,305,demod,44,174,257,254,257] a3(aux3(A,B,bfalse))=aux6(A,B,e_q3(a3(A),a3(B))). % 2.62/2.81 ---> New Demodulator: 307 [new_demod,306] a3(aux3(A,B,bfalse))=aux6(A,B,e_q3(a3(A),a3(B))). % 2.62/2.81 ** KEPT (pick-wt=6): 309 [copy,308,demod,174,257] a3(n(A))=n(A). % 2.62/2.81 ---> New Demodulator: 310 [new_demod,309] a3(n(A))=n(A). % 2.62/2.81 ** KEPT (pick-wt=6): 312 [copy,311,demod,174,257] a3(v(A))=v(A). % 2.62/2.81 ---> New Demodulator: 313 [new_demod,312] a3(v(A))=v(A). % 2.62/2.81 ** KEPT (pick-wt=5): 314 [] fetch(nil,A)=zero. % 2.62/2.81 ---> New Demodulator: 315 [new_demod,314] fetch(nil,A)=zero. % 2.62/2.81 ** KEPT (pick-wt=7): 316 [] fetch(cons(A,B),zero)=A. % 2.62/2.81 ---> New Demodulator: 317 [new_demod,316] fetch(cons(A,B),zero)=A. % 2.62/2.81 ** KEPT (pick-wt=10): 318 [] fetch(cons(A,B),suc(C))=fetch(B,C). % 2.62/2.81 ---> New Demodulator: 319 [new_demod,318] fetch(cons(A,B),suc(C))=fetch(B,C). % 2.62/2.81 ** KEPT (pick-wt=5): 320 [] addNat(zero,A)=A. % 2.62/2.81 ---> New Demodulator: 321 [new_demod,320] addNat(zero,A)=A. % 2.62/2.81 ** KEPT (pick-wt=9): 323 [copy,322,flip.1] suc(addNat(A,B))=addNat(suc(A),B). % 2.62/2.81 ---> New Demodulator: 324 [new_demod,323] suc(addNat(A,B))=addNat(suc(A),B). % 2.62/2.81 ** KEPT (pick-wt=5): 325 [] mulNat(zero,A)=zero. % 2.62/2.81 ---> New Demodulator: 326 [new_demod,325] mulNat(zero,A)=zero. % 2.62/2.81 ** KEPT (pick-wt=10): 327 [] mulNat(suc(A),B)=addNat(B,mulNat(A,B)). % 2.62/2.81 ---> New Demodulator: 328 [new_demod,327] mulNat(suc(A),B)=addNat(B,mulNat(A,B)). % 2.62/2.81 ** KEPT (pick-wt=6): 329 [] eval(A,n(B))=B. % 2.62/2.81 ---> New Demodulator: 330 [new_demod,329] eval(A,n(B))=B. % 2.62/2.81 ** KEPT (pick-wt=13): 331 [] eval(A,add(B,C))=addNat(eval(A,B),eval(A,C)). % 2.62/2.81 ---> New Demodulator: 332 [new_demod,331] eval(A,add(B,C))=addNat(eval(A,B),eval(A,C)). % 2.62/2.81 ** KEPT (pick-wt=13): 334 [copy,333,flip.1] mulNat(eval(A,B),eval(A,C))=eval(A,mul(B,C)). % 2.62/2.81 ---> New Demodulator: 335 [new_demod,334] mulNat(eval(A,B),eval(A,C))=eval(A,mul(B,C)). % 2.62/2.81 ** KEPT (pick-wt=18): 337 [copy,336,demod,44] eval(A,aux3(B,C,bfalse))=aux7(A,B,C,e_q2(eval(A,B),eval(A,C))). % 2.62/2.81 ---> New Demodulator: 338 [new_demod,337] eval(A,aux3(B,C,bfalse))=aux7(A,B,C,e_q2(eval(A,B),eval(A,C))). % 2.62/2.81 ** KEPT (pick-wt=8): 339 [] eval(A,v(B))=fetch(A,B). % 2.62/2.81 ** KEPT (pick-wt=14): 341 [copy,340,demod,174,257] prop4(A,B)=e_q4(e_q2(eval(A,B),eval(A,a3(B))),btrue). % 2.62/2.81 ** KEPT (pick-wt=5): 342 [] e_q4(bfalse,btrue)=bfalse. % 2.62/2.81 ---> New Demodulator: 343 [new_demod,342] e_q4(bfalse,btrue)=bfalse. % 2.62/2.81 ** KEPT (pick-wt=5): 344 [] e_q4(btrue,bfalse)=bfalse. % 2.62/2.81 ---> New Demodulator: 345 [new_demod,344] e_q4(btrue,bfalse)=bfalse. % 2.62/2.81 ** KEPT (pick-wt=9): 346 [] e_q3(n(A),n(B))=e_q2(A,B). % 2.62/2.81 ---> New Demodulator: 347 [new_demod,346] e_q3(n(A),n(B))=e_q2(A,B). % 2.62/2.81 ** KEPT (pick-wt=9): 348 [] e_q3(v(A),v(B))=e_q2(A,B). % 2.62/2.81 ---> New Demodulator: 349 [new_demod,348] e_q3(v(A),v(B))=e_q2(A,B). % 2.62/2.81 ** KEPT (pick-wt=8): 350 [] e_q3(n(A),add(B,C))=bfalse. % 2.62/2.81 ---> New Demodulator: 351 [new_demod,350] e_q3(n(A),add(B,C))=bfalse. % 2.62/2.81 ** KEPT (pick-wt=8): 352 [] e_q3(n(A),mul(B,C))=bfalse. % 2.62/2.81 ---> New Demodulator: 353 [new_demod,352] e_q3(n(A),mul(B,C))=bfalse. % 2.62/2.81 ** KEPT (pick-wt=9): 355 [copy,354,demod,44] e_q3(n(A),aux3(B,C,bfalse))=bfalse. % 2.62/2.81 ---> New Demodulator: 356 [new_demod,355] e_q3(n(A),aux3(B,C,bfalse))=bfalse. % 2.62/2.81 ** KEPT (pick-wt=7): 357 [] e_q3(n(A),v(B))=bfalse. % 2.62/2.81 ---> New Demodulator: 358 [new_demod,357] e_q3(n(A),v(B))=bfalse. % 2.62/2.81 ** KEPT (pick-wt=8): 359 [] e_q3(add(A,B),n(C))=bfalse. % 2.62/2.81 ---> New Demodulator: 360 [new_demod,359] e_q3(add(A,B),n(C))=bfalse. % 2.62/2.81 ** KEPT (pick-wt=9): 361 [] e_q3(add(A,B),mul(C,D))=bfalse. % 2.62/2.81 ---> New Demodulator: 362 [new_demod,361] e_q3(add(A,B),mul(C,D))=bfalse. % 2.62/2.81 ** KEPT (pick-wt=10): 364 [copy,363,demod,44] e_q3(add(A,B),aux3(C,D,bfalse))=bfalse. % 2.62/2.81 ---> New Demodulator: 365 [new_demod,364] e_q3(add(A,B),aux3(C,D,bfalse))=bfalse. % 2.62/2.81 ** KEPT (pick-wt=8): 366 [] e_q3(add(A,B),v(C))=bfalse. % 2.62/2.81 ---> New Demodulator: 367 [new_demod,366] e_q3(add(A,B),v(C))=bfalse. % 2.62/2.81 ** KEPT (pick-wt=8): 368 [] e_q3(mul(A,B),n(C))=bfalse. % 2.62/2.81 ---> New Demodulator: 369 [new_demod,368] e_q3(mul(A,B),n(C))=bfalse. % 2.62/2.81 ** KEPT (pick-wt=9): 370 [] e_q3(mul(A,B),add(C,D))=bfalse. % 2.62/2.81 ---> New Demodulator: 371 [new_demod,370] e_q3(mul(A,B),add(C,D))=bfalse. % 2.62/2.81 ** KEPT (pick-wt=10): 373 [copy,372,demod,44] e_q3(mul(A,B),aux3(C,D,bfalse))=bfalse. % 2.62/2.81 ---> New Demodulator: 374 [new_demod,373] e_q3(mul(A,B),aux3(C,D,bfalse))=bfalse. % 2.62/2.81 ** KEPT (pick-wt=8): 375 [] e_q3(mul(A,B),v(C))=bfalse. % 2.62/2.81 ---> New Demodulator: 376 [new_demod,375] e_q3(mul(A,B),v(C))=bfalse. % 2.62/2.81 ** KEPT (pick-wt=9): 378 [copy,377,demod,44] e_q3(aux3(A,B,bfalse),n(C))=bfalse. % 2.62/2.81 ---> New Demodulator: 379 [new_demod,378] e_q3(aux3(A,B,bfalse),n(C))=bfalse. % 2.62/2.81 ** KEPT (pick-wt=10): 381 [copy,380,demod,44] e_q3(aux3(A,B,bfalse),add(C,D))=bfalse. % 2.62/2.81 ---> New Demodulator: 382 [new_demod,381] e_q3(aux3(A,B,bfalse),add(C,D))=bfalse. % 2.62/2.81 ** KEPT (pick-wt=10): 384 [copy,383,demod,44] e_q3(aux3(A,B,bfalse),mul(C,D))=bfalse. % 2.62/2.81 ---> New Demodulator: 385 [new_demod,384] e_q3(aux3(A,B,bfalse),mul(C,D))=bfalse. % 2.62/2.81 ** KEPT (pick-wt=9): 387 [copy,386,demod,44] e_q3(aux3(A,B,bfalse),v(C))=bfalse. % 2.62/2.81 ---> New Demodulator: 388 [new_demod,387] e_q3(aux3(A,B,bfalse),v(C))=bfalse. % 2.62/2.81 ** KEPT (pick-wt=7): 389 [] e_q3(v(A),n(B))=bfalse. % 2.62/2.81 ---> New Demodulator: 390 [new_demod,389] e_q3(v(A),n(B))=bfalse. % 2.62/2.81 ** KEPT (pick-wt=8): 391 [] e_q3(v(A),add(B,C))=bfalse. % 2.62/2.81 ---> New Demodulator: 392 [new_demod,391] e_q3(v(A),add(B,C))=bfalse. % 2.62/2.81 ** KEPT (pick-wt=8): 393 [] e_q3(v(A),mul(B,C))=bfalse. % 2.62/2.81 ---> New Demodulator: 394 [new_demod,393] e_q3(v(A),mul(B,C))=bfalse. % 2.62/2.81 ** KEPT (pick-wt=9): 396 [copy,395,demod,44] e_q3(v(A),aux3(B,C,bfalse))=bfalse. % 2.62/2.81 ---> New Demodulator: 397 [new_demod,396] e_q3(v(A),aux3(B,C,bfalse))=bfalse. % 2.62/2.81 ** KEPT (pick-wt=9): 398 [] e_q2(suc(A),suc(B))=e_q2(A,B). % 2.62/2.81 ---> New Demodulator: 399 [new_demod,398] e_q2(suc(A),suc(B))=e_q2(A,B). % 2.62/2.81 ** KEPT (pick-wt=6): 400 [] e_q2(zero,suc(A))=bfalse. % 2.62/2.81 ---> New Demodulator: 401 [new_demod,400] e_q2(zero,suc(A))=bfalse. % 2.62/2.81 ** KEPT (pick-wt=6): 402 [] e_q2(suc(A),zero)=bfalse. % 2.62/2.81 ---> New Demodulator: 403 [new_demod,402] e_q2(suc(A),zero)=bfalse. % 2.62/2.81 ** KEPT (pick-wt=5): 404 [] e_q2(A,A)=btrue. % 2.62/2.81 ---> New Demodulator: 405 [new_demod,404] e_q2(A,A)=btrue. % 2.62/2.81 ** KEPT (pick-wt=5): 406 [] e_q3(A,A)=btrue. % 2.62/2.81 ---> New Demodulator: 407 [new_demod,406] e_q3(A,A)=btrue. % 2.62/2.81 ** KEPT (pick-wt=5): 408 [] e_q4(A,A)=btrue. % 2.62/2.81 ---> New Demodulator: 409 [new_demod,408] e_q4(A,A)=btrue. % 2.62/2.81 Following clause subsumed by 8 during input processing: 0 [copy,8,flip.1] A=A. % 2.62/2.81 ** KEPT (pick-wt=11): 410 [copy,9,flip.1,demod,90] fail3(n(suc(suc(zero))),A)=aux(A,B,btrue). % 2.62/2.81 >>>> Starting back demodulation with 12. % 2.62/2.81 >>>> Starting back demodulation with 15. % 2.62/2.81 >>>> Starting back demodulation with 18. % 2.62/2.81 >>>> Starting back demodulation with 21. % 2.62/2.81 >>>> Starting back demodulation with 24. % 2.62/2.81 ** KEPT (pick-wt=11): 411 [copy,25,flip.1,demod,90] fail3(n(suc(suc(zero))),A)=aux2(A,B,btrue). % 2.62/2.81 >>>> Starting back demodulation with 28. % 2.62/2.81 >>>> Starting back demodulation with 31. % 2.62/2.81 >>>> Starting back demodulation with 34. % 2.62/2.81 >>>> Starting back demodulation with 37. % 2.62/2.81 >>>> Starting back demodulation with 40. % 2.62/2.81 ** KEPT (pick-wt=8): 412 [copy,41,flip.1] n(suc(zero))=aux3(A,B,btrue). % 2.62/2.81 >>>> Starting back demodulation with 44. % 2.62/2.81 >> back demodulating 36 with 44. % 2.62/2.81 >> back demodulating 20 with 44. % 2.62/2.81 >> back demodulating 6 with 44. % 2.62/2.81 >> back demodulating 5 with 44. % 2.62/2.81 ** KEPT (pick-wt=8): 419 [copy,45,flip.1,demod,257] a3(A)=aux4(B,A,n(zero)). % 2.62/2.81 ** KEPT (pick-wt=12): 420 [copy,46,flip.1,demod,177,257,257] fail4(a3(A),a3(B))=aux4(A,B,n(suc(C))). % 2.62/2.81 ** KEPT (pick-wt=12): 421 [copy,47,flip.1,demod,177,257,257] fail4(a3(A),a3(B))=aux4(A,B,add(C,D)). % 2.62/2.81 ** KEPT (pick-wt=12): 422 [copy,48,flip.1,demod,177,257,257] fail4(a3(A),a3(B))=aux4(A,B,mul(C,D)). % 2.62/2.81 ** KEPT (pick-wt=13): 423 [copy,50,flip.1,demod,177,257,257] fail4(a3(A),a3(B))=aux4(A,B,aux3(C,D,bfalse)). % 2.62/2.81 ** KEPT (pick-wt=11): 424 [copy,51,flip.1,demod,177,257,257] fail4(a3(A),a3(B))=aux4(A,B,v(C)). % 2.62/2.81 >>>> Starting back demodulation with 53. % 2.62/2.81 ** KEPT (pick-wt=12): 425 [copy,54,flip.1,demod,251,257,248,257] fail23(a3(A),a3(B))=aux5(A,B,n(suc(C))). % 2.62/2.81 ** KEPT (pick-wt=12): 426 [copy,55,flip.1,demod,251,257,248,257] fail23(a3(A),a3(B))=aux5(A,B,add(C,D)). % 2.62/2.81 ** KEPT (pick-wt=12): 427 [copy,56,flip.1,demod,251,257,248,257] fail23(a3(A),a3(B))=aux5(A,B,mul(C,D)). % 2.62/2.81 ** KEPT (pick-wt=13): 428 [copy,58,flip.1,demod,251,257,248,257] fail23(a3(A),a3(B))=aux5(A,B,aux3(C,D,bfalse)). % 2.62/2.81 ** KEPT (pick-wt=11): 429 [copy,59,flip.1,demod,251,257,248,257] fail23(a3(A),a3(B))=aux5(A,B,v(C)). % 2.62/2.81 ** KEPT (pick-wt=8): 430 [copy,60,flip.1] n(suc(zero))=aux6(A,B,btrue). % 2.62/2.81 ** KEPT (pick-wt=11): 431 [copy,62,flip.1,demod,254,257] aux3(a3(A),a3(B),bfalse)=aux6(A,B,bfalse). % 2.62/2.81 ** KEPT (pick-wt=8): 432 [copy,63,flip.1] suc(zero)=aux7(A,B,C,btrue). % 2.62/2.81 >>>> Starting back demodulation with 65. % 2.62/2.81 >>>> Starting back demodulation with 67. % 2.62/2.81 >>>> Starting back demodulation with 69. % 2.62/2.81 >>>> Starting back demodulation with 72. % 2.62/2.81 >>>> Starting back demodulation with 75. % 2.62/2.81 >>>> Starting back demodulation with 78. % 2.62/2.81 >>>> Starting back demodulation with 81. % 2.62/2.81 >>>> Starting back demodulation with 84. % 2.62/2.81 >>>> Starting back demodulation with 87. % 2.62/2.81 >>>> Starting back demodulation with 90. % 2.62/2.81 >> back demodulating 25 with 90. % 2.62/2.81 >> back demodulating 9 with 90. % 2.62/2.81 >>>> Starting back demodulation with 93. % 2.62/2.81 >>>> Starting back demodulation with 96. % 2.62/2.81 >>>> Starting back demodulation with 99. % 2.62/2.81 >>>> Starting back demodulation with 102. % 2.62/2.81 >>>> Starting back demodulation with 104. % 2.62/2.81 >>>> Starting back demodulation with 107. % 2.62/2.81 >>>> Starting back demodulation with 110. % 2.62/2.81 >>>> Starting back demodulation with 113. % 2.62/2.81 >>>> Starting back demodulation with 116. % 2.62/2.81 >>>> Starting back demodulation with 119. % 2.62/2.81 >>>> Starting back demodulation with 122. % 2.62/2.81 >>>> Starting back demodulation with 124. % 2.62/2.81 >>>> Starting back demodulation with 127. % 2.62/2.81 >>>> Starting back demodulation with 130. % 2.62/2.81 >>>> Starting back demodulation with 133. % 2.62/2.81 >>>> Starting back demodulation with 136. % 2.62/2.81 >>>> Starting back demodulation with 139. % 2.62/2.81 >>>> Starting back demodulation with 141. % 2.62/2.81 >>>> Starting back demodulation with 143. % 2.62/2.81 >>>> Starting back demodulation with 145. % 2.62/2.81 >>>> Starting back demodulation with 147. % 2.62/2.81 >>>> Starting back demodulation with 150. % 2.62/2.81 >>>> Starting back demodulation with 152. % 2.62/2.81 >>>> Starting back demodulation with 154. % 2.62/2.81 >>>> Starting back demodulation with 156. % 2.62/2.81 >>>> Starting back demodulation with 159. % 2.62/2.81 >>>> Starting back demodulation with 162. % 2.62/2.81 >>>> Starting back demodulation with 165. % 2.62/2.81 >>>> Starting back demodulation with 168. % 2.62/2.81 >>>> Starting back demodulation with 171. % 2.62/2.81 >>>> Starting back demodulation with 174. % 2.62/2.81 >>>> Starting back demodulation with 177. % 2.62/2.81 >> back demodulating 51 with 177. % 2.62/2.81 >> back demodulating 50 with 177. % 2.62/2.81 >> back demodulating 48 with 177. % 2.62/2.81 >> back demodulating 47 with 177. % 2.62/2.81 >> back demodulating 46 with 177. % 2.62/2.81 >>>> Starting back demodulation with 180. % 2.62/2.81 >>>> Starting back demodulation with 183. % 2.62/2.81 >>>> Starting back demodulation with 186. % 2.62/2.81 >>>> Starting back demodulation with 189. % 2.62/2.81 >>>> Starting back demodulation with 192. % 2.62/2.81 >>>> Starting back demodulation with 195. % 2.62/2.81 >>>> Starting back demodulation with 197. % 2.62/2.81 >>>> Starting back demodulation with 200. % 2.62/2.81 >>>> Starting back demodulation with 203. % 2.62/2.81 >>>> Starting back demodulation with 206. % 2.62/2.81 >>>> Starting back demodulation with 209. % 2.62/2.81 >>>> Starting back demodulation with 212. % 2.62/2.81 >>>> Starting back demodulation with 215. % 2.62/2.81 >>>> Starting back demodulation with 217. % 2.62/2.81 >>>> Starting back demodulation with 220. % 2.62/2.81 >>>> Starting back demodulation with 223. % 2.62/2.81 >>>> Starting back demodulation with 226. % 2.62/2.81 >>>> Starting back demodulation with 229. % 2.62/2.81 >>>> Starting back demodulation with 232. % 2.62/2.81 >>>> Starting back demodulation with 234. % 2.62/2.81 >>>> Starting back demodulation with 236. % 2.62/2.81 >>>> Starting back demodulation with 238. % 2.62/2.81 >>>> Starting back demodulation with 240. % 2.62/2.81 >>>> Starting back demodulation with 243. % 2.62/2.81 >>>> Starting back demodulation with 245. % 2.62/2.81 >>>> Starting back demodulation with 248. % 2.62/2.81 >> back demodulating 59 with 248. % 2.62/2.81 >> back demodulating 58 with 248. % 2.62/2.81 >> back demodulating 56 with 248. % 2.62/2.81 >> back demodulating 55 with 248. % 2.62/2.81 >> back demodulating 54 with 248. % 2.62/2.81 >>>> Starting back demodulation with 251. % 2.62/2.81 >>>> Starting back demodulation with 254. % 2.62/2.81 >> back demodulating 62 with 254. % 2.62/2.81 >>>> Starting back demodulation with 257. % 2.62/2.81 >> back demodulating 253 with 257. % 2.62/2.81 >> back demodulating 250 with 257. % 2.62/2.81 >> back demodulating 247 with 257. % 2.62/2.81 >> back demodulating 176 with 257. % 2.62/2.81 >> back demodulating 173 with 257. % 2.62/2.81 >> back demodulating 45 with 257. % 2.62/2.81 >>>> Starting back demodulation with 260. % 2.62/2.81 >>>> Starting back demodulation with 263. % 2.62/2.81 >>>> Starting back demodulation with 265. % 2.62/2.81 >>>> Starting back demodulation with 268. % 2.62/2.81 >>>> Starting back demodulation with 271. % 2.62/2.81 >>>> Starting back demodulation with 274. % 2.62/2.81 >>>> Starting back demodulation with 277. % 2.62/2.81 >>>> Starting back demodulation with 280. % 2.62/2.81 >>>> Starting back demodulation with 283. % 2.62/2.81 >>>> Starting back demodulation with 285. % 2.62/2.81 >>>> Starting back demodulation with 288. % 2.62/2.81 >>>> Starting back demodulation with 291. % 2.62/2.81 >>>> Starting back demodulation with 294. % 2.62/2.81 >>>> Starting back demodulation with 296. % 2.62/2.81 >>>> Starting back demodulation with 298. % 2.62/2.81 >>>> Starting back demodulation with 301. % 2.62/2.81 >>>> Starting back demodulation with 304. % 2.62/2.81 >>>> Starting back demodulation with 307. % 2.62/2.81 >>>> Starting back demodulation with 310. % 2.62/2.81 >>>> Starting back demodulation with 313. % 2.62/2.81 >>>> Starting back demodulation with 315. % 2.62/2.81 >>>> Starting back demodulation with 317. % 2.62/2.81 >>>> Starting back demodulation with 319. % 2.62/2.81 >>>> Starting back demodulation with 321. % 2.62/2.81 >>>> Starting back demodulation with 324. % 2.62/2.81 >>>> Starting back demodulation with 326. % 2.62/2.81 >>>> Starting back demodulation with 328. % 2.62/2.81 >>>> Starting back demodulation with 330. % 2.62/2.81 >>>> Starting back demodulation with 332. % 2.62/2.81 >>>> Starting back demodulation with 335. % 2.62/2.81 >>>> Starting back demodulation with 338. % 2.62/2.81 ** KEPT (pick-wt=8): 457 [copy,339,flip.1] fetch(A,B)=eval(A,v(B)). % 2.62/2.81 ** KEPT (pick-wt=14): 458 [copy,341,flip.1] e_q4(e_q2(eval(A,B),eval(A,a3(B))),btrue)=prop4(A,B). % 2.62/2.81 >>>> Starting back demodulation with 343. % 2.62/2.81 >>>> Starting back demodulation with 345. % 2.62/2.81 >>>> Starting back demodulation with 347. % 2.62/2.81 >>>> Starting back demodulation with 349. % 2.62/2.81 >>>> Starting back demodulation with 351. % 2.62/2.81 >>>> Starting back demodulation with 353. % 2.62/2.81 >>>> Starting back demodulation with 356. % 2.62/2.81 >>>> Starting back demodulation with 358. % 2.62/2.81 >>>> Starting back demodulation with 360. % 2.62/2.81 >>>> Starting back demodulation with 362. % 2.62/2.81 >>>> Starting back demodulation with 365. % 2.62/2.81 >>>> Starting back demodulation with 367. % 2.62/2.81 >>>> Starting back demodulation with 369. % 2.62/2.81 >>>> Starting back demodulation with 371. % 2.62/2.81 >>>> Starting back demodulation with 374. % 2.62/2.81 >>>> Starting back demodulation with 376. % 2.62/2.81 >>>> Starting back demodulation with 379. % 2.62/2.81 >>>> Starting back demodulation with 382. % 2.62/2.81 >>>> Starting back demodulation with 385. % 2.62/2.81 >>>> Starting back demodulation with 388. % 2.62/2.81 >>>> Starting back demodulation with 390. % 2.62/2.81 >>>> Starting back demodulation with 392. % 2.62/2.81 >>>> Starting back demodulation with 394. % 2.62/2.81 >>>> Starting back demodulation with 397. % 2.62/2.81 >>>> Starting back demodulation with 399. % 2.62/2.81 >>>> Starting back demodulation with 401. % 2.62/2.81 >>>> Starting back demodulation with 403. % 2.62/2.81 >>>> Starting back demodulation with 405. % 2.62/2.81 >>>> Starting back demodulation with 407. % 2.62/2.81 >>>> Starting back demodulation with 409. % 2.62/2.81 Following clause subsumed by 434 during input processing: 0 [copy,410,flip.1] aux(A,B,btrue)=fail3(n(suc(suc(zero))),A). % 2.62/2.81 Following clause subsumed by 433 during input processing: 0 [copy,411,flip.1] aux2(A,B,btrue)=fail3(n(suc(suc(zero))),A). % 2.62/2.81 Following clause subsumed by 41 during input processing: 0 [copy,412,flip.1] aux3(A,B,btrue)=n(suc(zero)). % 2.62/2.81 >>>> Starting back demodulation with 414. % 2.62/2.81 >>>> Starting back demodulation with 416. % 2.62/2.81 >> back demodulating 270 with 416. % 2.62/2.81 Following clause subsumed by 456 during input processing: 0 [copy,419,flip.1] aux4(A,B,n(zero))=a3(B). % 2.62/2.81 Following clause subsumed by 439 during input processing: 0 [copy,420,flip.1] aux4(A,B,n(suc(C)))=fail4(a3(A),a3(B)). % 2.62/2.81 Following clause subsumed by 438 during input processing: 0 [copy,421,flip.1] aux4(A,B,add(C,D))=fail4(a3(A),a3(B)). % 2.62/2.81 Following clause subsumed by 437 during input processing: 0 [copy,422,flip.1] aux4(A,B,mul(C,D))=fail4(a3(A),a3(B)). % 2.62/2.81 Following clause subsumed by 436 during input processing: 0 [copy,423,flip.1] aux4(A,B,aux3(C,D,bfalse))=fail4(a3(A),a3(B)). % 2.62/2.81 Following clause subsumed by 435 during input processing: 0 [copy,424,flip.1] aux4(A,B,v(C))=fail4(a3(A),a3(B)). % 2.62/2.81 Following clause subsumed by 444 during input processing: 0 [copy,425,flip.1] aux5(A,B,n(suc(C)))=fail23(a3(A),a3(B)). % 2.62/2.81 Following clause subsumed by 443 during input processing: 0 [copy,426,flip.1] aux5(A,B,add(C,D))=fail23(a3(A),a3(B)). % 2.62/2.81 Following clause subsumed by 442 during input processing: 0 [copy,427,flip.1] aux5(A,B,mul(C,D))=fail23(a3(A),a3(B)). % 2.62/2.81 Following clause subsumed by 441 during input processing: 0 [copy,428,flip.1] aux5(A,B,aux3(C,D,bfalse))=fail23(a3(A),a3(B)). % 2.62/2.81 Following clause subsumed by 440 during input processing: 0 [copy,429,flip.1] aux5(A,B,v(C))=fail23(a3(A),a3(B)). % 2.62/2.81 Following clause subsumed by 60 during input processing: 0 [copy,430,flip.1] aux6(A,B,btrue)=n(suc(zero)). % 2.62/2.81 Following clause subsumed by 445 during input processing: 0 [copy,431,flip.1] aux6(A,B,bfalse)=aux3(a3(A),a3(B),bfalse). % 2.62/2.81 Following clause subsumed by 63 during input processing: 0 [copy,432,flip.1] aux7(A,B,C,btrue)=suc(zero). % 2.62/2.81 Following clause subsumed by 411 during input processing: 0 [copy,433,flip.1] fail3(n(suc(suc(zero))),A)=aux2(A,B,btrue). % 2.62/2.81 Following clause subsumed by 410 during input processing: 0 [copy,434,flip.1] fail3(n(suc(suc(zero))),A)=aux(A,B,btrue). % 2.62/2.81 Following clause subsumed by 424 during input processing: 0 [copy,435,flip.1] fail4(a3(A),a3(B))=aux4(A,B,v(C)). % 2.62/2.81 Following clause subsumed by 423 during input processing: 0 [copy,436,flip.1] fail4(a3(A),a3(B))=aux4(A,B,aux3(C,D,bfalse)). % 2.62/2.81 Following clause subsumed by 422 during input processing: 0 [copy,437,flip.1] fail4(a3(A),a3(B))=aux4(A,B,mul(C,D)). % 2.62/2.81 Following clause subsumed by 421 during input processing: 0 [copy,438,flip.1] fail4(a3(A),a3(B))=aux4(A,B,add(C,D)). % 2.62/2.81 Following clause subsumed by 420 during input processing: 0 [copy,439,flip.1] fail4(a3(A),a3(B))=aux4(A,B,n(suc(C))). % 2.62/2.81 Following clause subsumed by 429 during input processing: 0 [copy,440,flip.1] fail23(a3(A),a3(B))=aux5(A,B,v(C)). % 2.62/2.81 Following clause subsumed by 428 during input processing: 0 [copy,441,flip.1] fail23(a3(A),a3(B))=aux5(A,B,aux3(C,D,bfalse)). % 2.62/2.81 Following clause subsumed by 427 during input processing: 0 [copy,442,flip.1] fail23(a3(A),a3(B))=aux5(A,B,mul(C,D)). % 2.62/2.81 Following clause subsumed by 426 during input processing: 0 [copy,443,flip.1] fail23(a3(A),a3(B))=aux5(A,B,add(C,D)). % 2.62/2.81 Following clause subsumed by 425 during input processing: 0 [copy,444,flip.1] fail23(a3(A),a3(B))=aux5(A,B,n(suc(C))). % 2.62/2.81 Following clause subsumed by 431 during input processing: 0 [copy,445,flip.1] aux3(a3(A),a3(B),bfalse)=aux6(A,B,bfalse). % 2.62/2.81 >>>> Starting back demodulation with 447. % 2.62/2.81 >>>> Starting back demodulation with 449. % 2.62/2.81 >>>> Starting back demodulation with 451. % 2.62/2.81 >>>> Starting back demodulation with 453. % 2.62/2.81 >>>> Starting back demodulation with 455. % 2.62/2.81 Following clause subsumed by 419 during input processing: 0 [copy,456,flip.1] a3(A)=aux4(B,A,n(zero)). % 2.62/2.81 Following clause subsumed by 339 during input processing: 0 [copy,457,flip.1] eval(A,v(B))=fetch(A,B). % 2.62/2.84 Following clause subsumed by 341 during input processing: 0 [copy,458,flip.1] prop4(A,B)=e_q4(e_q2(eval(A,B),eval(A,a3(B))),btrue). % 2.62/2.84 >>>> Starting back demodulation with 460. % 2.62/2.84 % 2.62/2.84 ======= end of input processing ======= % 2.62/2.84 % 2.62/2.84 =========== start of search =========== % 2.62/2.84 % 2.62/2.84 % 2.62/2.84 Resetting weight limit to 6. % 2.62/2.84 % 2.62/2.84 % 2.62/2.84 Resetting weight limit to 6. % 2.62/2.84 % 2.62/2.84 sos_size=191 % 2.62/2.84 % 2.62/2.84 Search stopped because sos empty. % 2.62/2.84 % 2.62/2.84 % 2.62/2.84 Search stopped because sos empty. % 2.62/2.84 % 2.62/2.84 ============ end of search ============ % 2.62/2.84 % 2.62/2.84 -------------- statistics ------------- % 2.62/2.84 clauses given 212 % 2.62/2.84 clauses generated 2349 % 2.62/2.84 clauses kept 242 % 2.62/2.84 clauses forward subsumed 229 % 2.62/2.84 clauses back subsumed 1 % 2.62/2.84 Kbytes malloced 7812 % 2.62/2.84 % 2.62/2.84 ----------- times (seconds) ----------- % 2.62/2.84 user CPU time 0.04 (0 hr, 0 min, 0 sec) % 2.62/2.84 system CPU time 0.00 (0 hr, 0 min, 0 sec) % 2.62/2.84 wall-clock time 3 (0 hr, 0 min, 3 sec) % 2.62/2.84 % 2.62/2.84 Process 8441 finished Tue May 5 11:02:56 2026 % 2.62/2.84 Otter interrupted % 2.62/2.84 PROOF NOT FOUND %------------------------------------------------------------------------------