%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWX216-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n017.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:26 PM UTC 2026 % Result : Unknown 2.31s 2.57s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX216-1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : otter-tptp-script %s % 0.15/0.33 % Computer : n017.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 12:11:57 EDT 2026 % 0.15/0.33 % CPUTime : % 2.31/2.50 ----- Otter 3.3f, August 2004 ----- % 2.31/2.50 The process was started by sandbox on n017.cluster.edu, % 2.31/2.50 Tue May 5 12:11:57 2026 % 2.31/2.50 The command was "./otter". The process ID is 10008. % 2.31/2.50 % 2.31/2.50 set(prolog_style_variables). % 2.31/2.50 set(auto). % 2.31/2.50 dependent: set(auto1). % 2.31/2.50 dependent: set(process_input). % 2.31/2.50 dependent: clear(print_kept). % 2.31/2.50 dependent: clear(print_new_demod). % 2.31/2.50 dependent: clear(print_back_demod). % 2.31/2.50 dependent: clear(print_back_sub). % 2.31/2.50 dependent: set(control_memory). % 2.31/2.50 dependent: assign(max_mem, 12000). % 2.31/2.50 dependent: assign(pick_given_ratio, 4). % 2.31/2.50 dependent: assign(stats_level, 1). % 2.31/2.50 dependent: assign(max_seconds, 10800). % 2.31/2.50 clear(print_given). % 2.31/2.50 % 2.31/2.50 list(usable). % 2.31/2.50 0 [] A=A. % 2.31/2.50 0 [] aux(X,Z,Ys,btrue)=del(X,Ys). % 2.31/2.50 0 [] aux(X,Z,Ys,bfalse)=cons(Z,del(X,Ys)). % 2.31/2.50 0 [] aux2(X,Z,E,btrue)=pair2(cons(Z,X),bfalse). % 2.31/2.50 0 [] aux2(X,Z,E,bfalse)=pair2(del(Z,X),bfalse). % 2.31/2.50 0 [] aux3(X,P,Q,pair2(S1,btrue))=pair2(S1,btrue). % 2.31/2.50 0 [] aux3(X,P,Q,pair2(S1,bfalse))=run(S1,Q). % 2.31/2.50 0 [] aux4(X,E2,R,Q2,btrue)=run(X,R). % 2.31/2.50 0 [] aux4(X,E2,R,Q2,bfalse)=run(X,Q2). % 2.31/2.50 0 [] aux5(X,P2,Q3,pair2(S,btrue))=run(S,Q3). % 2.31/2.51 0 [] aux5(X,P2,Q3,pair2(S,bfalse))=pair2(S,bfalse). % 2.31/2.51 0 [] aux6(X,Y,Z,pair2(X2,Y3))=impl(typeCorrect(bfalse,X),e_q5(elem(l,Z),elem(l,X2))). % 2.31/2.51 0 [] aux7(X,Y,pair2(Z,Y2))=aux6(X,Y,Z,run(cons(h,Y),X)). % 2.31/2.51 0 [] orb(btrue,Q)=btrue. % 2.31/2.51 0 [] orb(bfalse,Q)=Q. % 2.31/2.51 0 [] secret(nand(A,B))=orb(secret(A),secret(B)). % 2.31/2.51 0 [] secret(var(high(Z)))=btrue. % 2.31/2.51 0 [] secret(var(low(X2)))=bfalse. % 2.31/2.51 0 [] secret(tT)=bfalse. % 2.31/2.51 0 [] secret(fF)=bfalse. % 2.31/2.51 0 [] notb(btrue)=bfalse. % 2.31/2.51 0 [] notb(bfalse)=btrue. % 2.31/2.51 0 [] l=low(zero). % 2.31/2.51 0 [] impl(btrue,Q)=Q. % 2.31/2.51 0 [] impl(bfalse,Q)=btrue. % 2.31/2.51 0 [] h=high(zero). % 2.31/2.51 0 [] elem(X,nil)=bfalse. % 2.31/2.51 0 [] elem(X,cons(Z,Xs))=orb(e_q2(Z,X),elem(X,Xs)). % 2.31/2.51 0 [] del(X,nil)=nil. % 2.31/2.51 0 [] del(X,cons(Z,Ys))=aux(X,Z,Ys,e_q2(X,Z)). % 2.31/2.51 0 [] andb(btrue,Q)=Q. % 2.31/2.51 0 [] andb(bfalse,Q)=bfalse. % 2.31/2.51 0 [] eval(X,nand(A,B))=notb(andb(eval(X,A),eval(X,B))). % 2.31/2.51 0 [] eval(X,tT)=btrue. % 2.31/2.51 0 [] eval(X,fF)=bfalse. % 2.31/2.51 0 [] eval(X,var(Z))=elem(Z,X). % 2.31/2.51 0 [] run(X,skip)=pair2(X,bfalse). % 2.31/2.51 0 [] run(X,assign(Z,E))=aux2(X,Z,E,eval(X,E)). % 2.31/2.51 0 [] run(X,se_q(P,Q))=aux3(X,P,Q,run(X,P)). % 2.31/2.51 0 [] run(X,ifThenElse(E2,R,Q2))=aux4(X,E2,R,Q2,eval(X,E2)). % 2.31/2.51 0 [] run(X,catch(P2,Q3))=aux5(X,P2,Q3,run(X,P2)). % 2.31/2.51 0 [] run(X,throw)=pair2(X,btrue). % 2.31/2.51 0 [] run(X,while(E3,P3))=run(X,ifThenElse(E3,se_q(P3,while(E3,P3)),skip)). % 2.31/2.51 0 [] typeCorrect(X,assign(high(X2),E))=btrue. % 2.31/2.51 0 [] typeCorrect(X,assign(low(X3),E))=andb(notb(X),notb(secret(E))). % 2.31/2.51 0 [] typeCorrect(X,se_q(P,Q))=andb(typeCorrect(X,P),typeCorrect(X,Q)). % 2.31/2.51 0 [] typeCorrect(X,ifThenElse(C,R,Q2))=andb(typeCorrect(orb(secret(C),X),R),typeCorrect(orb(secret(C),X),Q2)). % 2.31/2.51 0 [] typeCorrect(X,catch(P2,Q3))=andb(typeCorrect(X,P2),typeCorrect(X,Q3)). % 2.31/2.51 0 [] typeCorrect(X,while(E2,P3))=typeCorrect(orb(secret(E2),X),P3). % 2.31/2.51 0 [] typeCorrect(X,skip)=btrue. % 2.31/2.51 0 [] typeCorrect(X,throw)=btrue. % 2.31/2.51 0 [] prop(X,Y)=aux7(X,Y,run(Y,X)). % 2.31/2.51 0 [] e_q3(tT,fF)=bfalse. % 2.31/2.51 0 [] e_q3(fF,tT)=bfalse. % 2.31/2.51 0 [] e_q4(skip,throw)=bfalse. % 2.31/2.51 0 [] e_q4(throw,skip)=bfalse. % 2.31/2.51 0 [] e_q5(bfalse,btrue)=bfalse. % 2.31/2.51 0 [] e_q5(btrue,bfalse)=bfalse. % 2.31/2.51 0 [] e_q3(X,Z)!=bfalse|e_q3(nand(X,Y),nand(Z,X2))=bfalse. % 2.31/2.51 0 [] e_q3(X,Z)!=btrue|e_q3(nand(X,Y),nand(Z,X2))=e_q3(Y,X2). % 2.31/2.51 0 [] e_q3(var(X),var(Y))=e_q2(X,Y). % 2.31/2.51 0 [] e_q3(nand(X,Y),tT)=bfalse. % 2.31/2.51 0 [] e_q3(nand(X,Y),fF)=bfalse. % 2.31/2.51 0 [] e_q3(nand(X,Y),var(Z))=bfalse. % 2.31/2.51 0 [] e_q3(tT,nand(X,Y))=bfalse. % 2.31/2.51 0 [] e_q3(tT,var(X))=bfalse. % 2.31/2.51 0 [] e_q3(fF,nand(X,Y))=bfalse. % 2.31/2.51 0 [] e_q3(fF,var(X))=bfalse. % 2.31/2.51 0 [] e_q3(var(X),nand(Y,Z))=bfalse. % 2.31/2.51 0 [] e_q3(var(X),tT)=bfalse. % 2.31/2.51 0 [] e_q3(var(X),fF)=bfalse. % 2.31/2.51 0 [] e_q2(high(X),high(Y))=e_q(X,Y). % 2.31/2.51 0 [] e_q2(low(X),low(Y))=e_q(X,Y). % 2.31/2.51 0 [] e_q2(high(X),low(Y))=bfalse. % 2.31/2.51 0 [] e_q2(low(X),high(Y))=bfalse. % 2.31/2.51 0 [] e_q(suc(X),suc(Y))=e_q(X,Y). % 2.31/2.51 0 [] e_q(zero,suc(X))=bfalse. % 2.31/2.51 0 [] e_q(suc(X),zero)=bfalse. % 2.31/2.51 0 [] e_q2(X,Z)!=bfalse|e_q4(assign(X,Y),assign(Z,X2))=bfalse. % 2.31/2.51 0 [] e_q2(X,Z)!=btrue|e_q4(assign(X,Y),assign(Z,X2))=e_q3(Y,X2). % 2.31/2.51 0 [] e_q4(X,Z)!=bfalse|e_q4(se_q(X,Y),se_q(Z,X2))=bfalse. % 2.31/2.51 0 [] e_q4(X,Z)!=btrue|e_q4(se_q(X,Y),se_q(Z,X2))=e_q4(Y,X2). % 2.31/2.51 0 [] e_q3(X,X2)!=bfalse|e_q4(ifThenElse(X,Y,Z),ifThenElse(X2,X3,X4))=bfalse. % 2.31/2.51 0 [] e_q3(X,X2)!=btrue|e_q4(Y,X3)!=bfalse|e_q4(ifThenElse(X,Y,Z),ifThenElse(X2,X3,X4))=bfalse. % 2.31/2.51 0 [] e_q3(X,X2)!=btrue|e_q4(Y,X3)!=btrue|e_q4(ifThenElse(X,Y,Z),ifThenElse(X2,X3,X4))=e_q4(Z,X4). % 2.31/2.51 0 [] e_q4(X,Z)!=bfalse|e_q4(catch(X,Y),catch(Z,X2))=bfalse. % 2.31/2.51 0 [] e_q4(X,Z)!=btrue|e_q4(catch(X,Y),catch(Z,X2))=e_q4(Y,X2). % 2.31/2.51 0 [] e_q3(X,Z)!=bfalse|e_q4(while(X,Y),while(Z,X2))=bfalse. % 2.31/2.51 0 [] e_q3(X,Z)!=btrue|e_q4(while(X,Y),while(Z,X2))=e_q4(Y,X2). % 2.31/2.51 0 [] e_q4(skip,assign(X,Y))=bfalse. % 2.31/2.51 0 [] e_q4(skip,se_q(X,Y))=bfalse. % 2.31/2.51 0 [] e_q4(skip,ifThenElse(X,Y,Z))=bfalse. % 2.31/2.51 0 [] e_q4(skip,catch(X,Y))=bfalse. % 2.31/2.51 0 [] e_q4(skip,while(X,Y))=bfalse. % 2.31/2.51 0 [] e_q4(assign(X,Y),skip)=bfalse. % 2.31/2.51 0 [] e_q4(assign(X,Y),se_q(Z,X2))=bfalse. % 2.31/2.51 0 [] e_q4(assign(X,Y),ifThenElse(Z,X2,X3))=bfalse. % 2.31/2.51 0 [] e_q4(assign(X,Y),catch(Z,X2))=bfalse. % 2.31/2.51 0 [] e_q4(assign(X,Y),throw)=bfalse. % 2.31/2.51 0 [] e_q4(assign(X,Y),while(Z,X2))=bfalse. % 2.31/2.51 0 [] e_q4(se_q(X,Y),skip)=bfalse. % 2.31/2.51 0 [] e_q4(se_q(X,Y),assign(Z,X2))=bfalse. % 2.31/2.51 0 [] e_q4(se_q(X,Y),ifThenElse(Z,X2,X3))=bfalse. % 2.31/2.51 0 [] e_q4(se_q(X,Y),catch(Z,X2))=bfalse. % 2.31/2.51 0 [] e_q4(se_q(X,Y),throw)=bfalse. % 2.31/2.51 0 [] e_q4(se_q(X,Y),while(Z,X2))=bfalse. % 2.31/2.51 0 [] e_q4(ifThenElse(X,Y,Z),skip)=bfalse. % 2.31/2.51 0 [] e_q4(ifThenElse(X,Y,Z),assign(X2,X3))=bfalse. % 2.31/2.51 0 [] e_q4(ifThenElse(X,Y,Z),se_q(X2,X3))=bfalse. % 2.31/2.51 0 [] e_q4(ifThenElse(X,Y,Z),catch(X2,X3))=bfalse. % 2.31/2.51 0 [] e_q4(ifThenElse(X,Y,Z),throw)=bfalse. % 2.31/2.51 0 [] e_q4(ifThenElse(X,Y,Z),while(X2,X3))=bfalse. % 2.31/2.51 0 [] e_q4(catch(X,Y),skip)=bfalse. % 2.31/2.51 0 [] e_q4(catch(X,Y),assign(Z,X2))=bfalse. % 2.31/2.51 0 [] e_q4(catch(X,Y),se_q(Z,X2))=bfalse. % 2.31/2.51 0 [] e_q4(catch(X,Y),ifThenElse(Z,X2,X3))=bfalse. % 2.31/2.51 0 [] e_q4(catch(X,Y),throw)=bfalse. % 2.31/2.51 0 [] e_q4(catch(X,Y),while(Z,X2))=bfalse. % 2.31/2.51 0 [] e_q4(throw,assign(X,Y))=bfalse. % 2.31/2.51 0 [] e_q4(throw,se_q(X,Y))=bfalse. % 2.31/2.51 0 [] e_q4(throw,ifThenElse(X,Y,Z))=bfalse. % 2.31/2.51 0 [] e_q4(throw,catch(X,Y))=bfalse. % 2.31/2.51 0 [] e_q4(throw,while(X,Y))=bfalse. % 2.31/2.51 0 [] e_q4(while(X,Y),skip)=bfalse. % 2.31/2.51 0 [] e_q4(while(X,Y),assign(Z,X2))=bfalse. % 2.31/2.51 0 [] e_q4(while(X,Y),se_q(Z,X2))=bfalse. % 2.31/2.51 0 [] e_q4(while(X,Y),ifThenElse(Z,X2,X3))=bfalse. % 2.31/2.51 0 [] e_q4(while(X,Y),catch(Z,X2))=bfalse. % 2.31/2.51 0 [] e_q4(while(X,Y),throw)=bfalse. % 2.31/2.51 0 [] e_q(X,X)=btrue. % 2.31/2.51 0 [] e_q2(X,X)=btrue. % 2.31/2.51 0 [] e_q3(X,X)=btrue. % 2.31/2.51 0 [] e_q4(X,X)=btrue. % 2.31/2.51 0 [] e_q5(X,X)=btrue. % 2.31/2.51 0 [] e_q5(prop(X,Y),bfalse)!=btrue. % 2.31/2.51 end_of_list. % 2.31/2.51 % 2.31/2.51 SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=3. % 2.31/2.51 % 2.31/2.51 This is a Horn set with equality. The strategy will be % 2.31/2.51 Knuth-Bendix and hyper_res, with positive clauses in % 2.31/2.51 sos and nonpositive clauses in usable. % 2.31/2.51 % 2.31/2.51 dependent: set(knuth_bendix). % 2.31/2.51 dependent: set(anl_eq). % 2.31/2.51 dependent: set(para_from). % 2.31/2.51 dependent: set(para_into). % 2.31/2.51 dependent: clear(para_from_right). % 2.31/2.51 dependent: clear(para_into_right). % 2.31/2.51 dependent: set(para_from_vars). % 2.31/2.51 dependent: set(eq_units_both_ways). % 2.31/2.51 dependent: set(dynamic_demod_all). % 2.31/2.51 dependent: set(dynamic_demod). % 2.31/2.51 dependent: set(order_eq). % 2.31/2.51 dependent: set(back_demod). % 2.31/2.51 dependent: set(lrpo). % 2.31/2.51 dependent: set(hyper_res). % 2.31/2.51 dependent: clear(order_hyper). % 2.31/2.51 % 2.31/2.51 ------------> process usable: % 2.31/2.51 ** KEPT (pick-wt=14): 1 [] e_q3(A,B)!=bfalse|e_q3(nand(A,C),nand(B,D))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=16): 2 [] e_q3(A,B)!=btrue|e_q3(nand(A,C),nand(B,D))=e_q3(C,D). % 2.31/2.51 ** KEPT (pick-wt=14): 3 [] e_q2(A,B)!=bfalse|e_q4(assign(A,C),assign(B,D))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=16): 4 [] e_q2(A,B)!=btrue|e_q4(assign(A,C),assign(B,D))=e_q3(C,D). % 2.31/2.51 ** KEPT (pick-wt=14): 5 [] e_q4(A,B)!=bfalse|e_q4(se_q(A,C),se_q(B,D))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=16): 6 [] e_q4(A,B)!=btrue|e_q4(se_q(A,C),se_q(B,D))=e_q4(C,D). % 2.31/2.51 ** KEPT (pick-wt=16): 7 [] e_q3(A,B)!=bfalse|e_q4(ifThenElse(A,C,D),ifThenElse(B,E,F))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=21): 8 [] e_q3(A,B)!=btrue|e_q4(C,D)!=bfalse|e_q4(ifThenElse(A,C,E),ifThenElse(B,D,F))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=23): 9 [] e_q3(A,B)!=btrue|e_q4(C,D)!=btrue|e_q4(ifThenElse(A,C,E),ifThenElse(B,D,F))=e_q4(E,F). % 2.31/2.51 ** KEPT (pick-wt=14): 10 [] e_q4(A,B)!=bfalse|e_q4(catch(A,C),catch(B,D))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=16): 11 [] e_q4(A,B)!=btrue|e_q4(catch(A,C),catch(B,D))=e_q4(C,D). % 2.31/2.51 ** KEPT (pick-wt=14): 12 [] e_q3(A,B)!=bfalse|e_q4(while(A,C),while(B,D))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=16): 13 [] e_q3(A,B)!=btrue|e_q4(while(A,C),while(B,D))=e_q4(C,D). % 2.31/2.51 ** KEPT (pick-wt=7): 14 [] e_q5(prop(A,B),bfalse)!=btrue. % 2.31/2.51 % 2.31/2.51 ------------> process sos: % 2.31/2.51 ** KEPT (pick-wt=3): 15 [] A=A. % 2.31/2.51 ** KEPT (pick-wt=9): 16 [] aux(A,B,C,btrue)=del(A,C). % 2.31/2.51 ** KEPT (pick-wt=11): 18 [copy,17,flip.1] cons(A,del(B,C))=aux(B,A,C,bfalse). % 2.31/2.51 ---> New Demodulator: 19 [new_demod,18] cons(A,del(B,C))=aux(B,A,C,bfalse). % 2.31/2.51 ** KEPT (pick-wt=11): 20 [] aux2(A,B,C,btrue)=pair2(cons(B,A),bfalse). % 2.31/2.51 ** KEPT (pick-wt=11): 21 [] aux2(A,B,C,bfalse)=pair2(del(B,A),bfalse). % 2.31/2.51 ** KEPT (pick-wt=11): 22 [] aux3(A,B,C,pair2(D,btrue))=pair2(D,btrue). % 2.31/2.51 ---> New Demodulator: 23 [new_demod,22] aux3(A,B,C,pair2(D,btrue))=pair2(D,btrue). % 2.31/2.51 ** KEPT (pick-wt=11): 24 [] aux3(A,B,C,pair2(D,bfalse))=run(D,C). % 2.31/2.51 ** KEPT (pick-wt=10): 25 [] aux4(A,B,C,D,btrue)=run(A,C). % 2.31/2.51 ** KEPT (pick-wt=10): 26 [] aux4(A,B,C,D,bfalse)=run(A,D). % 2.31/2.51 ** KEPT (pick-wt=11): 27 [] aux5(A,B,C,pair2(D,btrue))=run(D,C). % 2.31/2.51 ** KEPT (pick-wt=11): 28 [] aux5(A,B,C,pair2(D,bfalse))=pair2(D,bfalse). % 2.31/2.51 ---> New Demodulator: 29 [new_demod,28] aux5(A,B,C,pair2(D,bfalse))=pair2(D,bfalse). % 2.31/2.51 ** KEPT (pick-wt=19): 30 [] aux6(A,B,C,pair2(D,E))=impl(typeCorrect(bfalse,A),e_q5(elem(l,C),elem(l,D))). % 2.31/2.51 ** KEPT (pick-wt=16): 31 [] aux7(A,B,pair2(C,D))=aux6(A,B,C,run(cons(h,B),A)). % 2.31/2.51 ** KEPT (pick-wt=5): 32 [] orb(btrue,A)=btrue. % 2.31/2.51 ---> New Demodulator: 33 [new_demod,32] orb(btrue,A)=btrue. % 2.31/2.51 ** KEPT (pick-wt=5): 34 [] orb(bfalse,A)=A. % 2.31/2.51 ---> New Demodulator: 35 [new_demod,34] orb(bfalse,A)=A. % 2.31/2.51 ** KEPT (pick-wt=10): 36 [] secret(nand(A,B))=orb(secret(A),secret(B)). % 2.31/2.51 ---> New Demodulator: 37 [new_demod,36] secret(nand(A,B))=orb(secret(A),secret(B)). % 2.31/2.51 ** KEPT (pick-wt=6): 38 [] secret(var(high(A)))=btrue. % 2.31/2.51 ---> New Demodulator: 39 [new_demod,38] secret(var(high(A)))=btrue. % 2.31/2.51 ** KEPT (pick-wt=6): 40 [] secret(var(low(A)))=bfalse. % 2.31/2.51 ---> New Demodulator: 41 [new_demod,40] secret(var(low(A)))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=4): 42 [] secret(tT)=bfalse. % 2.31/2.51 ---> New Demodulator: 43 [new_demod,42] secret(tT)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=4): 44 [] secret(fF)=bfalse. % 2.31/2.51 ---> New Demodulator: 45 [new_demod,44] secret(fF)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=4): 46 [] notb(btrue)=bfalse. % 2.31/2.51 ---> New Demodulator: 47 [new_demod,46] notb(btrue)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=4): 48 [] notb(bfalse)=btrue. % 2.31/2.51 ---> New Demodulator: 49 [new_demod,48] notb(bfalse)=btrue. % 2.31/2.51 ** KEPT (pick-wt=4): 51 [copy,50,flip.1] low(zero)=l. % 2.31/2.51 ---> New Demodulator: 52 [new_demod,51] low(zero)=l. % 2.31/2.51 ** KEPT (pick-wt=5): 53 [] impl(btrue,A)=A. % 2.31/2.51 ---> New Demodulator: 54 [new_demod,53] impl(btrue,A)=A. % 2.31/2.51 ** KEPT (pick-wt=5): 55 [] impl(bfalse,A)=btrue. % 2.31/2.51 ---> New Demodulator: 56 [new_demod,55] impl(bfalse,A)=btrue. % 2.31/2.51 ** KEPT (pick-wt=4): 58 [copy,57,flip.1] high(zero)=h. % 2.31/2.51 ---> New Demodulator: 59 [new_demod,58] high(zero)=h. % 2.31/2.51 ** KEPT (pick-wt=5): 60 [] elem(A,nil)=bfalse. % 2.31/2.51 ---> New Demodulator: 61 [new_demod,60] elem(A,nil)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=13): 63 [copy,62,flip.1] orb(e_q2(A,B),elem(B,C))=elem(B,cons(A,C)). % 2.31/2.51 ---> New Demodulator: 64 [new_demod,63] orb(e_q2(A,B),elem(B,C))=elem(B,cons(A,C)). % 2.31/2.51 ** KEPT (pick-wt=5): 65 [] del(A,nil)=nil. % 2.31/2.51 ---> New Demodulator: 66 [new_demod,65] del(A,nil)=nil. % 2.31/2.51 ** KEPT (pick-wt=13): 67 [] del(A,cons(B,C))=aux(A,B,C,e_q2(A,B)). % 2.31/2.51 ** KEPT (pick-wt=5): 68 [] andb(btrue,A)=A. % 2.31/2.51 ---> New Demodulator: 69 [new_demod,68] andb(btrue,A)=A. % 2.31/2.51 ** KEPT (pick-wt=5): 70 [] andb(bfalse,A)=bfalse. % 2.31/2.51 ---> New Demodulator: 71 [new_demod,70] andb(bfalse,A)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=14): 73 [copy,72,flip.1] notb(andb(eval(A,B),eval(A,C)))=eval(A,nand(B,C)). % 2.31/2.51 ---> New Demodulator: 74 [new_demod,73] notb(andb(eval(A,B),eval(A,C)))=eval(A,nand(B,C)). % 2.31/2.51 ** KEPT (pick-wt=5): 75 [] eval(A,tT)=btrue. % 2.31/2.51 ---> New Demodulator: 76 [new_demod,75] eval(A,tT)=btrue. % 2.31/2.51 ** KEPT (pick-wt=5): 77 [] eval(A,fF)=bfalse. % 2.31/2.51 ---> New Demodulator: 78 [new_demod,77] eval(A,fF)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=8): 79 [] eval(A,var(B))=elem(B,A). % 2.31/2.51 ---> New Demodulator: 80 [new_demod,79] eval(A,var(B))=elem(B,A). % 2.31/2.51 ** KEPT (pick-wt=7): 81 [] run(A,skip)=pair2(A,bfalse). % 2.31/2.51 ---> New Demodulator: 82 [new_demod,81] run(A,skip)=pair2(A,bfalse). % 2.31/2.51 ** KEPT (pick-wt=13): 83 [] run(A,assign(B,C))=aux2(A,B,C,eval(A,C)). % 2.31/2.51 ---> New Demodulator: 84 [new_demod,83] run(A,assign(B,C))=aux2(A,B,C,eval(A,C)). % 2.31/2.51 ** KEPT (pick-wt=13): 85 [] run(A,se_q(B,C))=aux3(A,B,C,run(A,B)). % 2.31/2.51 ---> New Demodulator: 86 [new_demod,85] run(A,se_q(B,C))=aux3(A,B,C,run(A,B)). % 2.31/2.51 ** KEPT (pick-wt=15): 87 [] run(A,ifThenElse(B,C,D))=aux4(A,B,C,D,eval(A,B)). % 2.31/2.51 ---> New Demodulator: 88 [new_demod,87] run(A,ifThenElse(B,C,D))=aux4(A,B,C,D,eval(A,B)). % 2.31/2.51 ** KEPT (pick-wt=13): 89 [] run(A,catch(B,C))=aux5(A,B,C,run(A,B)). % 2.31/2.51 ---> New Demodulator: 90 [new_demod,89] run(A,catch(B,C))=aux5(A,B,C,run(A,B)). % 2.31/2.51 ** KEPT (pick-wt=7): 91 [] run(A,throw)=pair2(A,btrue). % 2.31/2.51 ---> New Demodulator: 92 [new_demod,91] run(A,throw)=pair2(A,btrue). % 2.31/2.51 ** KEPT (pick-wt=18): 94 [copy,93,demod,88] run(A,while(B,C))=aux4(A,B,se_q(C,while(B,C)),skip,eval(A,B)). % 2.31/2.51 ** KEPT (pick-wt=8): 95 [] typeCorrect(A,assign(high(B),C))=btrue. % 2.31/2.51 ---> New Demodulator: 96 [new_demod,95] typeCorrect(A,assign(high(B),C))=btrue. % 2.31/2.51 ** KEPT (pick-wt=13): 97 [] typeCorrect(A,assign(low(B),C))=andb(notb(A),notb(secret(C))). % 2.31/2.51 ** KEPT (pick-wt=13): 98 [] typeCorrect(A,se_q(B,C))=andb(typeCorrect(A,B),typeCorrect(A,C)). % 2.31/2.51 ---> New Demodulator: 99 [new_demod,98] typeCorrect(A,se_q(B,C))=andb(typeCorrect(A,B),typeCorrect(A,C)). % 2.31/2.51 ** KEPT (pick-wt=20): 100 [] typeCorrect(A,ifThenElse(B,C,D))=andb(typeCorrect(orb(secret(B),A),C),typeCorrect(orb(secret(B),A),D)). % 2.31/2.51 ** KEPT (pick-wt=13): 101 [] typeCorrect(A,catch(B,C))=andb(typeCorrect(A,B),typeCorrect(A,C)). % 2.31/2.51 ---> New Demodulator: 102 [new_demod,101] typeCorrect(A,catch(B,C))=andb(typeCorrect(A,B),typeCorrect(A,C)). % 2.31/2.51 ** KEPT (pick-wt=12): 103 [] typeCorrect(A,while(B,C))=typeCorrect(orb(secret(B),A),C). % 2.31/2.51 ** KEPT (pick-wt=5): 104 [] typeCorrect(A,skip)=btrue. % 2.31/2.51 ---> New Demodulator: 105 [new_demod,104] typeCorrect(A,skip)=btrue. % 2.31/2.51 ** KEPT (pick-wt=5): 106 [] typeCorrect(A,throw)=btrue. % 2.31/2.51 ---> New Demodulator: 107 [new_demod,106] typeCorrect(A,throw)=btrue. % 2.31/2.51 ** KEPT (pick-wt=10): 109 [copy,108,flip.1] aux7(A,B,run(B,A))=prop(A,B). % 2.31/2.51 ---> New Demodulator: 110 [new_demod,109] aux7(A,B,run(B,A))=prop(A,B). % 2.31/2.51 ** KEPT (pick-wt=5): 111 [] e_q3(tT,fF)=bfalse. % 2.31/2.51 ---> New Demodulator: 112 [new_demod,111] e_q3(tT,fF)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=5): 113 [] e_q3(fF,tT)=bfalse. % 2.31/2.51 ---> New Demodulator: 114 [new_demod,113] e_q3(fF,tT)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=5): 115 [] e_q4(skip,throw)=bfalse. % 2.31/2.51 ---> New Demodulator: 116 [new_demod,115] e_q4(skip,throw)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=5): 117 [] e_q4(throw,skip)=bfalse. % 2.31/2.51 ---> New Demodulator: 118 [new_demod,117] e_q4(throw,skip)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=5): 119 [] e_q5(bfalse,btrue)=bfalse. % 2.31/2.51 ---> New Demodulator: 120 [new_demod,119] e_q5(bfalse,btrue)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=5): 121 [] e_q5(btrue,bfalse)=bfalse. % 2.31/2.51 ---> New Demodulator: 122 [new_demod,121] e_q5(btrue,bfalse)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=9): 123 [] e_q3(var(A),var(B))=e_q2(A,B). % 2.31/2.51 ---> New Demodulator: 124 [new_demod,123] e_q3(var(A),var(B))=e_q2(A,B). % 2.31/2.51 ** KEPT (pick-wt=7): 125 [] e_q3(nand(A,B),tT)=bfalse. % 2.31/2.51 ---> New Demodulator: 126 [new_demod,125] e_q3(nand(A,B),tT)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=7): 127 [] e_q3(nand(A,B),fF)=bfalse. % 2.31/2.51 ---> New Demodulator: 128 [new_demod,127] e_q3(nand(A,B),fF)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=8): 129 [] e_q3(nand(A,B),var(C))=bfalse. % 2.31/2.51 ---> New Demodulator: 130 [new_demod,129] e_q3(nand(A,B),var(C))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=7): 131 [] e_q3(tT,nand(A,B))=bfalse. % 2.31/2.51 ---> New Demodulator: 132 [new_demod,131] e_q3(tT,nand(A,B))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=6): 133 [] e_q3(tT,var(A))=bfalse. % 2.31/2.51 ---> New Demodulator: 134 [new_demod,133] e_q3(tT,var(A))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=7): 135 [] e_q3(fF,nand(A,B))=bfalse. % 2.31/2.51 ---> New Demodulator: 136 [new_demod,135] e_q3(fF,nand(A,B))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=6): 137 [] e_q3(fF,var(A))=bfalse. % 2.31/2.51 ---> New Demodulator: 138 [new_demod,137] e_q3(fF,var(A))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=8): 139 [] e_q3(var(A),nand(B,C))=bfalse. % 2.31/2.51 ---> New Demodulator: 140 [new_demod,139] e_q3(var(A),nand(B,C))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=6): 141 [] e_q3(var(A),tT)=bfalse. % 2.31/2.51 ---> New Demodulator: 142 [new_demod,141] e_q3(var(A),tT)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=6): 143 [] e_q3(var(A),fF)=bfalse. % 2.31/2.51 ---> New Demodulator: 144 [new_demod,143] e_q3(var(A),fF)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=9): 145 [] e_q2(high(A),high(B))=e_q(A,B). % 2.31/2.51 ---> New Demodulator: 146 [new_demod,145] e_q2(high(A),high(B))=e_q(A,B). % 2.31/2.51 ** KEPT (pick-wt=9): 147 [] e_q2(low(A),low(B))=e_q(A,B). % 2.31/2.51 ---> New Demodulator: 148 [new_demod,147] e_q2(low(A),low(B))=e_q(A,B). % 2.31/2.51 ** KEPT (pick-wt=7): 149 [] e_q2(high(A),low(B))=bfalse. % 2.31/2.51 ---> New Demodulator: 150 [new_demod,149] e_q2(high(A),low(B))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=7): 151 [] e_q2(low(A),high(B))=bfalse. % 2.31/2.51 ---> New Demodulator: 152 [new_demod,151] e_q2(low(A),high(B))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=9): 153 [] e_q(suc(A),suc(B))=e_q(A,B). % 2.31/2.51 ---> New Demodulator: 154 [new_demod,153] e_q(suc(A),suc(B))=e_q(A,B). % 2.31/2.51 ** KEPT (pick-wt=6): 155 [] e_q(zero,suc(A))=bfalse. % 2.31/2.51 ---> New Demodulator: 156 [new_demod,155] e_q(zero,suc(A))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=6): 157 [] e_q(suc(A),zero)=bfalse. % 2.31/2.51 ---> New Demodulator: 158 [new_demod,157] e_q(suc(A),zero)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=7): 159 [] e_q4(skip,assign(A,B))=bfalse. % 2.31/2.51 ---> New Demodulator: 160 [new_demod,159] e_q4(skip,assign(A,B))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=7): 161 [] e_q4(skip,se_q(A,B))=bfalse. % 2.31/2.51 ---> New Demodulator: 162 [new_demod,161] e_q4(skip,se_q(A,B))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=8): 163 [] e_q4(skip,ifThenElse(A,B,C))=bfalse. % 2.31/2.51 ---> New Demodulator: 164 [new_demod,163] e_q4(skip,ifThenElse(A,B,C))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=7): 165 [] e_q4(skip,catch(A,B))=bfalse. % 2.31/2.51 ---> New Demodulator: 166 [new_demod,165] e_q4(skip,catch(A,B))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=7): 167 [] e_q4(skip,while(A,B))=bfalse. % 2.31/2.51 ---> New Demodulator: 168 [new_demod,167] e_q4(skip,while(A,B))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=7): 169 [] e_q4(assign(A,B),skip)=bfalse. % 2.31/2.51 ---> New Demodulator: 170 [new_demod,169] e_q4(assign(A,B),skip)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=9): 171 [] e_q4(assign(A,B),se_q(C,D))=bfalse. % 2.31/2.51 ---> New Demodulator: 172 [new_demod,171] e_q4(assign(A,B),se_q(C,D))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=10): 173 [] e_q4(assign(A,B),ifThenElse(C,D,E))=bfalse. % 2.31/2.51 ---> New Demodulator: 174 [new_demod,173] e_q4(assign(A,B),ifThenElse(C,D,E))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=9): 175 [] e_q4(assign(A,B),catch(C,D))=bfalse. % 2.31/2.51 ---> New Demodulator: 176 [new_demod,175] e_q4(assign(A,B),catch(C,D))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=7): 177 [] e_q4(assign(A,B),throw)=bfalse. % 2.31/2.51 ---> New Demodulator: 178 [new_demod,177] e_q4(assign(A,B),throw)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=9): 179 [] e_q4(assign(A,B),while(C,D))=bfalse. % 2.31/2.51 ---> New Demodulator: 180 [new_demod,179] e_q4(assign(A,B),while(C,D))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=7): 181 [] e_q4(se_q(A,B),skip)=bfalse. % 2.31/2.51 ---> New Demodulator: 182 [new_demod,181] e_q4(se_q(A,B),skip)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=9): 183 [] e_q4(se_q(A,B),assign(C,D))=bfalse. % 2.31/2.51 ---> New Demodulator: 184 [new_demod,183] e_q4(se_q(A,B),assign(C,D))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=10): 185 [] e_q4(se_q(A,B),ifThenElse(C,D,E))=bfalse. % 2.31/2.51 ---> New Demodulator: 186 [new_demod,185] e_q4(se_q(A,B),ifThenElse(C,D,E))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=9): 187 [] e_q4(se_q(A,B),catch(C,D))=bfalse. % 2.31/2.51 ---> New Demodulator: 188 [new_demod,187] e_q4(se_q(A,B),catch(C,D))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=7): 189 [] e_q4(se_q(A,B),throw)=bfalse. % 2.31/2.51 ---> New Demodulator: 190 [new_demod,189] e_q4(se_q(A,B),throw)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=9): 191 [] e_q4(se_q(A,B),while(C,D))=bfalse. % 2.31/2.51 ---> New Demodulator: 192 [new_demod,191] e_q4(se_q(A,B),while(C,D))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=8): 193 [] e_q4(ifThenElse(A,B,C),skip)=bfalse. % 2.31/2.51 ---> New Demodulator: 194 [new_demod,193] e_q4(ifThenElse(A,B,C),skip)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=10): 195 [] e_q4(ifThenElse(A,B,C),assign(D,E))=bfalse. % 2.31/2.51 ---> New Demodulator: 196 [new_demod,195] e_q4(ifThenElse(A,B,C),assign(D,E))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=10): 197 [] e_q4(ifThenElse(A,B,C),se_q(D,E))=bfalse. % 2.31/2.51 ---> New Demodulator: 198 [new_demod,197] e_q4(ifThenElse(A,B,C),se_q(D,E))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=10): 199 [] e_q4(ifThenElse(A,B,C),catch(D,E))=bfalse. % 2.31/2.51 ---> New Demodulator: 200 [new_demod,199] e_q4(ifThenElse(A,B,C),catch(D,E))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=8): 201 [] e_q4(ifThenElse(A,B,C),throw)=bfalse. % 2.31/2.51 ---> New Demodulator: 202 [new_demod,201] e_q4(ifThenElse(A,B,C),throw)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=10): 203 [] e_q4(ifThenElse(A,B,C),while(D,E))=bfalse. % 2.31/2.51 ---> New Demodulator: 204 [new_demod,203] e_q4(ifThenElse(A,B,C),while(D,E))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=7): 205 [] e_q4(catch(A,B),skip)=bfalse. % 2.31/2.51 ---> New Demodulator: 206 [new_demod,205] e_q4(catch(A,B),skip)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=9): 207 [] e_q4(catch(A,B),assign(C,D))=bfalse. % 2.31/2.51 ---> New Demodulator: 208 [new_demod,207] e_q4(catch(A,B),assign(C,D))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=9): 209 [] e_q4(catch(A,B),se_q(C,D))=bfalse. % 2.31/2.51 ---> New Demodulator: 210 [new_demod,209] e_q4(catch(A,B),se_q(C,D))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=10): 211 [] e_q4(catch(A,B),ifThenElse(C,D,E))=bfalse. % 2.31/2.51 ---> New Demodulator: 212 [new_demod,211] e_q4(catch(A,B),ifThenElse(C,D,E))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=7): 213 [] e_q4(catch(A,B),throw)=bfalse. % 2.31/2.51 ---> New Demodulator: 214 [new_demod,213] e_q4(catch(A,B),throw)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=9): 215 [] e_q4(catch(A,B),while(C,D))=bfalse. % 2.31/2.51 ---> New Demodulator: 216 [new_demod,215] e_q4(catch(A,B),while(C,D))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=7): 217 [] e_q4(throw,assign(A,B))=bfalse. % 2.31/2.51 ---> New Demodulator: 218 [new_demod,217] e_q4(throw,assign(A,B))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=7): 219 [] e_q4(throw,se_q(A,B))=bfalse. % 2.31/2.51 ---> New Demodulator: 220 [new_demod,219] e_q4(throw,se_q(A,B))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=8): 221 [] e_q4(throw,ifThenElse(A,B,C))=bfalse. % 2.31/2.51 ---> New Demodulator: 222 [new_demod,221] e_q4(throw,ifThenElse(A,B,C))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=7): 223 [] e_q4(throw,catch(A,B))=bfalse. % 2.31/2.51 ---> New Demodulator: 224 [new_demod,223] e_q4(throw,catch(A,B))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=7): 225 [] e_q4(throw,while(A,B))=bfalse. % 2.31/2.51 ---> New Demodulator: 226 [new_demod,225] e_q4(throw,while(A,B))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=7): 227 [] e_q4(while(A,B),skip)=bfalse. % 2.31/2.51 ---> New Demodulator: 228 [new_demod,227] e_q4(while(A,B),skip)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=9): 229 [] e_q4(while(A,B),assign(C,D))=bfalse. % 2.31/2.51 ---> New Demodulator: 230 [new_demod,229] e_q4(while(A,B),assign(C,D))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=9): 231 [] e_q4(while(A,B),se_q(C,D))=bfalse. % 2.31/2.51 ---> New Demodulator: 232 [new_demod,231] e_q4(while(A,B),se_q(C,D))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=10): 233 [] e_q4(while(A,B),ifThenElse(C,D,E))=bfalse. % 2.31/2.51 ---> New Demodulator: 234 [new_demod,233] e_q4(while(A,B),ifThenElse(C,D,E))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=9): 235 [] e_q4(while(A,B),catch(C,D))=bfalse. % 2.31/2.51 ---> New Demodulator: 236 [new_demod,235] e_q4(while(A,B),catch(C,D))=bfalse. % 2.31/2.51 ** KEPT (pick-wt=7): 237 [] e_q4(while(A,B),throw)=bfalse. % 2.31/2.51 ---> New Demodulator: 238 [new_demod,237] e_q4(while(A,B),throw)=bfalse. % 2.31/2.51 ** KEPT (pick-wt=5): 239 [] e_q(A,A)=btrue. % 2.31/2.51 ---> New Demodulator: 240 [new_demod,239] e_q(A,A)=btrue. % 2.31/2.51 ** KEPT (pick-wt=5): 241 [] e_q2(A,A)=btrue. % 2.31/2.51 ---> New Demodulator: 242 [new_demod,241] e_q2(A,A)=btrue. % 2.31/2.51 ** KEPT (pick-wt=5): 243 [] e_q3(A,A)=btrue. % 2.31/2.51 ---> New Demodulator: 244 [new_demod,243] e_q3(A,A)=btrue. % 2.31/2.51 ** KEPT (pick-wt=5): 245 [] e_q4(A,A)=btrue. % 2.31/2.51 ---> New Demodulator: 246 [new_demod,245] e_q4(A,A)=btrue. % 2.31/2.51 ** KEPT (pick-wt=5): 247 [] e_q5(A,A)=btrue. % 2.31/2.51 ---> New Demodulator: 248 [new_demod,247] e_q5(A,A)=btrue. % 2.31/2.51 Following clause subsumed by 15 during input processing: 0 [copy,15,flip.1] A=A. % 2.31/2.51 ** KEPT (pick-wt=9): 249 [copy,16,flip.1] del(A,B)=aux(A,C,B,btrue). % 2.31/2.51 >>>> Starting back demodulation with 19. % 2.31/2.51 ** KEPT (pick-wt=11): 250 [copy,20,flip.1] pair2(cons(A,B),bfalse)=aux2(B,A,C,btrue). % 2.31/2.51 ** KEPT (pick-wt=11): 251 [copy,21,flip.1] pair2(del(A,B),bfalse)=aux2(B,A,C,bfalse). % 2.31/2.51 >>>> Starting back demodulation with 23. % 2.31/2.51 ** KEPT (pick-wt=11): 252 [copy,24,flip.1] run(A,B)=aux3(C,D,B,pair2(A,bfalse)). % 2.31/2.51 ** KEPT (pick-wt=10): 253 [copy,25,flip.1] run(A,B)=aux4(A,C,B,D,btrue). % 2.31/2.51 ** KEPT (pick-wt=10): 254 [copy,26,flip.1] run(A,B)=aux4(A,C,D,B,bfalse). % 2.31/2.51 ** KEPT (pick-wt=11): 255 [copy,27,flip.1] run(A,B)=aux5(C,D,B,pair2(A,btrue)). % 2.31/2.51 >>>> Starting back demodulation with 29. % 2.31/2.51 ** KEPT (pick-wt=19): 256 [copy,30,flip.1] impl(typeCorrect(bfalse,A),e_q5(elem(l,B),elem(l,C)))=aux6(A,D,B,pair2(C,E)). % 2.31/2.51 ** KEPT (pick-wt=16): 257 [copy,31,flip.1] aux6(A,B,C,run(cons(h,B),A))=aux7(A,B,pair2(C,D)). % 2.31/2.51 >>>> Starting back demodulation with 33. % 2.31/2.51 >>>> Starting back demodulation with 35. % 2.31/2.51 >>>> Starting back demodulation with 37. % 2.31/2.51 >>>> Starting back demodulation with 39. % 2.31/2.51 >>>> Starting back demodulation with 41. % 2.31/2.51 >>>> Starting back demodulation with 43. % 2.31/2.51 >>>> Starting back demodulation with 45. % 2.31/2.51 >>>> Starting back demodulation with 47. % 2.31/2.51 >>>> Starting back demodulation with 49. % 2.31/2.51 >>>> Starting back demodulation with 52. % 2.31/2.51 >>>> Starting back demodulation with 54. % 2.31/2.51 >>>> Starting back demodulation with 56. % 2.31/2.51 >>>> Starting back demodulation with 59. % 2.31/2.51 >>>> Starting back demodulation with 61. % 2.31/2.51 >>>> Starting back demodulation with 64. % 2.31/2.51 >>>> Starting back demodulation with 66. % 2.31/2.51 ** KEPT (pick-wt=13): 258 [copy,67,flip.1] aux(A,B,C,e_q2(A,B))=del(A,cons(B,C)). % 2.31/2.51 >>>> Starting back demodulation with 69. % 2.31/2.51 >>>> Starting back demodulation with 71. % 2.31/2.51 >>>> Starting back demodulation with 74. % 2.31/2.51 >>>> Starting back demodulation with 76. % 2.31/2.51 >>>> Starting back demodulation with 78. % 2.31/2.51 >>>> Starting back demodulation with 80. % 2.31/2.51 >>>> Starting back demodulation with 82. % 2.31/2.51 >>>> Starting back demodulation with 84. % 2.31/2.51 >>>> Starting back demodulation with 86. % 2.31/2.51 >>>> Starting back demodulation with 88. % 2.31/2.51 >>>> Starting back demodulation with 90. % 2.31/2.51 >>>> Starting back demodulation with 92. % 2.31/2.51 ** KEPT (pick-wt=18): 259 [copy,94,flip.1] aux4(A,B,se_q(C,while(B,C)),skip,eval(A,B))=run(A,while(B,C)). % 2.31/2.51 >>>> Starting back demodulation with 96. % 2.31/2.51 ** KEPT (pick-wt=13): 260 [copy,97,flip.1] andb(notb(A),notb(secret(B)))=typeCorrect(A,assign(low(C),B)). % 2.31/2.51 >>>> Starting back demodulation with 99. % 2.31/2.51 ** KEPT (pick-wt=20): 261 [copy,100,flip.1] andb(typeCorrect(orb(secret(A),B),C),typeCorrect(orb(secret(A),B),D))=typeCorrect(B,ifThenElse(A,C,D)). % 2.31/2.51 >>>> Starting back demodulation with 102. % 2.31/2.51 ** KEPT (pick-wt=12): 262 [copy,103,flip.1] typeCorrect(orb(secret(A),B),C)=typeCorrect(B,while(A,C)). % 2.31/2.51 >>>> Starting back demodulation with 105. % 2.31/2.51 >>>> Starting back demodulation with 107. % 2.31/2.51 >>>> Starting back demodulation with 110. % 2.31/2.51 >>>> Starting back demodulation with 112. % 2.31/2.51 >>>> Starting back demodulation with 114. % 2.31/2.51 >>>> Starting back demodulation with 116. % 2.31/2.51 >>>> Starting back demodulation with 118. % 2.31/2.51 >>>> Starting back demodulation with 120. % 2.31/2.51 >>>> Starting back demodulation with 122. % 2.31/2.51 >>>> Starting back demodulation with 124. % 2.31/2.51 >>>> Starting back demodulation with 126. % 2.31/2.51 >>>> Starting back demodulation with 128. % 2.31/2.51 >>>> Starting back demodulation with 130. % 2.31/2.51 >>>> Starting back demodulation with 132. % 2.31/2.51 >>>> Starting back demodulation with 134. % 2.31/2.51 >>>> Starting back demodulation with 136. % 2.31/2.51 >>>> Starting back demodulation with 138. % 2.31/2.51 >>>> Starting back demodulation with 140. % 2.31/2.51 >>>> Starting back demodulation with 142. % 2.31/2.51 >>>> Starting back demodulation with 144. % 2.31/2.51 >>>> Starting back demodulation with 146. % 2.31/2.51 >>>> Starting back demodulation with 148. % 2.31/2.51 >>>> Starting back demodulation with 150. % 2.31/2.51 >>>> Starting back demodulation with 152. % 2.31/2.51 >>>> Starting back demodulation with 154. % 2.31/2.51 >>>> Starting back demodulation with 156. % 2.31/2.51 >>>> Starting back demodulation with 158. % 2.31/2.51 >>>> Starting back demodulation with 160. % 2.31/2.51 >>>> Starting back demodulation with 162. % 2.31/2.51 >>>> Starting back demodulation with 164. % 2.31/2.51 >>>> Starting back demodulation with 166. % 2.31/2.51 >>>> Starting back demodulation with 168. % 2.31/2.51 >>>> Starting back demodulation with 170. % 2.31/2.51 >>>> Starting back demodulation with 172. % 2.31/2.51 >>>> Starting back demodulation with 174. % 2.31/2.51 >>>> Starting back demodulation with 176. % 2.31/2.51 >>>> Starting back demodulation with 178. % 2.31/2.51 >>>> Starting back demodulation with 180. % 2.31/2.51 >>>> Starting back demodulation with 182. % 2.31/2.51 >>>> Starting back demodulation with 184. % 2.31/2.51 >>>> Starting back demodulation with 186. % 2.31/2.51 >>>> Starting back demodulation with 188. % 2.31/2.51 >>>> Starting back demodulation with 190. % 2.31/2.51 >>>> Starting back demodulation with 192. % 2.31/2.51 >>>> Starting back demodulation with 194. % 2.31/2.51 >>>> Starting back demodulation with 196. % 2.31/2.51 >>>> Starting back demodulation with 198. % 2.31/2.51 >>>> Starting back demodulation with 200. % 2.31/2.51 >>>> Starting back demodulation with 202. % 2.31/2.51 >>>> Starting back demodulation with 204. % 2.31/2.51 >>>> Starting back demodulation with 206. % 2.31/2.51 >>>> Starting back demodulation with 208. % 2.31/2.51 >>>> Starting back demodulation with 210. % 2.31/2.51 >>>> Starting back demodulation with 212. % 2.31/2.51 >>>> Starting back demodulation with 214. % 2.31/2.51 >>>> Starting back demodulation with 216. % 2.31/2.51 >>>> Starting back demodulation with 218. % 2.31/2.51 >>>> Starting back demodulation with 220. % 2.31/2.51 >>>> Starting back demodulation with 222. % 2.31/2.51 >>>> Starting back demodulation with 224. % 2.31/2.51 >>>> Starting back demodulation with 226. % 2.31/2.51 >>>> Starting back demodulation with 228. % 2.31/2.56 >>>> Starting back demodulation with 230. % 2.31/2.56 >>>> Starting back demodulation with 232. % 2.31/2.56 >>>> Starting back demodulation with 234. % 2.31/2.56 >>>> Starting back demodulation with 236. % 2.31/2.56 >>>> Starting back demodulation with 238. % 2.31/2.56 >>>> Starting back demodulation with 240. % 2.31/2.56 >>>> Starting back demodulation with 242. % 2.31/2.56 >>>> Starting back demodulation with 244. % 2.31/2.56 >>>> Starting back demodulation with 246. % 2.31/2.56 >>>> Starting back demodulation with 248. % 2.31/2.56 Following clause subsumed by 16 during input processing: 0 [copy,249,flip.1] aux(A,B,C,btrue)=del(A,C). % 2.31/2.56 Following clause subsumed by 20 during input processing: 0 [copy,250,flip.1] aux2(A,B,C,btrue)=pair2(cons(B,A),bfalse). % 2.31/2.56 Following clause subsumed by 21 during input processing: 0 [copy,251,flip.1] aux2(A,B,C,bfalse)=pair2(del(B,A),bfalse). % 2.31/2.56 Following clause subsumed by 24 during input processing: 0 [copy,252,flip.1] aux3(A,B,C,pair2(D,bfalse))=run(D,C). % 2.31/2.56 Following clause subsumed by 25 during input processing: 0 [copy,253,flip.1] aux4(A,B,C,D,btrue)=run(A,C). % 2.31/2.56 Following clause subsumed by 26 during input processing: 0 [copy,254,flip.1] aux4(A,B,C,D,bfalse)=run(A,D). % 2.31/2.56 Following clause subsumed by 27 during input processing: 0 [copy,255,flip.1] aux5(A,B,C,pair2(D,btrue))=run(D,C). % 2.31/2.56 Following clause subsumed by 30 during input processing: 0 [copy,256,flip.1] aux6(A,B,C,pair2(D,E))=impl(typeCorrect(bfalse,A),e_q5(elem(l,C),elem(l,D))). % 2.31/2.56 Following clause subsumed by 31 during input processing: 0 [copy,257,flip.1] aux7(A,B,pair2(C,D))=aux6(A,B,C,run(cons(h,B),A)). % 2.31/2.56 Following clause subsumed by 67 during input processing: 0 [copy,258,flip.1] del(A,cons(B,C))=aux(A,B,C,e_q2(A,B)). % 2.31/2.56 Following clause subsumed by 94 during input processing: 0 [copy,259,flip.1] run(A,while(B,C))=aux4(A,B,se_q(C,while(B,C)),skip,eval(A,B)). % 2.31/2.56 Following clause subsumed by 97 during input processing: 0 [copy,260,flip.1] typeCorrect(A,assign(low(B),C))=andb(notb(A),notb(secret(C))). % 2.31/2.56 Following clause subsumed by 100 during input processing: 0 [copy,261,flip.1] typeCorrect(A,ifThenElse(B,C,D))=andb(typeCorrect(orb(secret(B),A),C),typeCorrect(orb(secret(B),A),D)). % 2.31/2.56 Following clause subsumed by 103 during input processing: 0 [copy,262,flip.1] typeCorrect(A,while(B,C))=typeCorrect(orb(secret(B),A),C). % 2.31/2.56 % 2.31/2.56 ======= end of input processing ======= % 2.31/2.56 % 2.31/2.56 =========== start of search =========== % 2.31/2.56 % 2.31/2.56 % 2.31/2.56 Resetting weight limit to 8. % 2.31/2.56 % 2.31/2.56 % 2.31/2.56 Resetting weight limit to 8. % 2.31/2.56 % 2.31/2.56 sos_size=214 % 2.31/2.56 % 2.31/2.56 Search stopped because sos empty. % 2.31/2.56 % 2.31/2.56 % 2.31/2.56 Search stopped because sos empty. % 2.31/2.56 % 2.31/2.56 ============ end of search ============ % 2.31/2.56 % 2.31/2.56 -------------- statistics ------------- % 2.31/2.56 clauses given 316 % 2.31/2.56 clauses generated 6419 % 2.31/2.56 clauses kept 330 % 2.31/2.56 clauses forward subsumed 1706 % 2.31/2.56 clauses back subsumed 0 % 2.31/2.56 Kbytes malloced 5859 % 2.31/2.56 % 2.31/2.56 ----------- times (seconds) ----------- % 2.31/2.56 user CPU time 0.06 (0 hr, 0 min, 0 sec) % 2.31/2.56 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 2.31/2.56 wall-clock time 2 (0 hr, 0 min, 2 sec) % 2.31/2.56 % 2.31/2.56 Process 10008 finished Tue May 5 12:11:59 2026 % 2.31/2.57 Otter interrupted % 2.31/2.57 PROOF NOT FOUND %------------------------------------------------------------------------------