%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWX240_1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n005.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue May 5 07:05:29 PM UTC 2026 % Result : Timeout 299.87s 300.02s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX240_1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : otter-tptp-script %s % 0.17/0.34 % Computer : n005.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Tue May 5 13:22:45 EDT 2026 % 0.17/0.34 % CPUTime : % 1.93/2.14 ----- Otter 3.3f, August 2004 ----- % 1.93/2.14 The process was started by sandbox on n005.cluster.edu, % 1.93/2.14 Tue May 5 13:22:45 2026 % 1.93/2.14 The command was "./otter". The process ID is 29868. % 1.93/2.14 % 1.93/2.14 set(prolog_style_variables). % 1.93/2.14 set(auto). % 1.93/2.14 dependent: set(auto1). % 1.93/2.14 dependent: set(process_input). % 1.93/2.14 dependent: clear(print_kept). % 1.93/2.14 dependent: clear(print_new_demod). % 1.93/2.14 dependent: clear(print_back_demod). % 1.93/2.14 dependent: clear(print_back_sub). % 1.93/2.14 dependent: set(control_memory). % 1.93/2.14 dependent: assign(max_mem, 12000). % 1.93/2.14 dependent: assign(pick_given_ratio, 4). % 1.93/2.14 dependent: assign(stats_level, 1). % 1.93/2.14 dependent: assign(max_seconds, 10800). % 1.93/2.14 clear(print_given). % 1.93/2.14 % 1.93/2.14 formula_list(usable). % 1.93/2.14 all A (A=A). % 1.93/2.14 all X X2 (head(cons(X,X2))=X). % 1.93/2.14 all X X2 (tail(cons(X,X2))=X2). % 1.93/2.14 all X X2 (nil!=cons(X,X2)). % 1.93/2.14 all X (proj1Suc(suc(X))=X). % 1.93/2.14 all X (zero!=suc(X)). % 1.93/2.14 all X (proj1High(high(X))=X). % 1.93/2.14 all X (proj1Low(low(X))=X). % 1.93/2.14 all X X2 (high(X)!=low(X2)). % 1.93/2.14 all X X2 (proj1Nand(nand(X,X2))=X). % 1.93/2.14 all X X2 (proj2Nand(nand(X,X2))=X2). % 1.93/2.14 all X (proj1Var(var(X))=X). % 1.93/2.14 all X X2 (nand(X,X2)!=tT). % 1.93/2.14 all X X2 (nand(X,X2)!=fF). % 1.93/2.14 all X X2 X3 (nand(X,X2)!=var(X3)). % 1.93/2.14 tT!=fF. % 1.93/2.14 all X (tT!=var(X)). % 1.93/2.14 all X (fF!=var(X)). % 1.93/2.14 all X X2 (proj1Assign(assign(X,X2))=X). % 1.93/2.14 all X X2 (proj2Assign(assign(X,X2))=X2). % 1.93/2.14 all X X2 (proj1Se_q(se_q(X,X2))=X). % 1.93/2.14 all X X2 (proj2Se_q(se_q(X,X2))=X2). % 1.93/2.14 all X X2 X3 (proj1IfThenElse(ifThenElse(X,X2,X3))=X). % 1.93/2.14 all X X2 X3 (proj2IfThenElse(ifThenElse(X,X2,X3))=X2). % 1.93/2.14 all X X2 X3 (proj3IfThenElse(ifThenElse(X,X2,X3))=X3). % 1.93/2.14 all X X2 (skip!=assign(X,X2)). % 1.93/2.14 all X X2 (skip!=se_q(X,X2)). % 1.93/2.14 all X X2 X3 (skip!=ifThenElse(X,X2,X3)). % 1.93/2.14 all X X2 X3 X4 (assign(X,X2)!=se_q(X3,X4)). % 1.93/2.14 all X X2 X3 X4 X5 (assign(X,X2)!=ifThenElse(X3,X4,X5)). % 1.93/2.14 all X X2 X3 X4 X5 (se_q(X,X2)!=ifThenElse(X3,X4,X5)). % 1.93/2.14 all X (X!=nand(proj1Nand(X),proj2Nand(X))-> (X!=var(proj1Var(X))-> -secret(X))). % 1.93/2.14 all A B (secret(nand(A,B))<->secret(A)|secret(B)). % 1.93/2.14 all Z secret(var(high(Z))). % 1.93/2.14 all X2 (-secret(var(low(X2)))). % 1.93/2.14 typeCorrect(skip). % 1.93/2.14 all E Z typeCorrect(assign(high(Z),E)). % 1.93/2.14 all E X2 (typeCorrect(assign(low(X2),E))<-> -secret(E)). % 1.93/2.14 all P Q (typeCorrect(se_q(P,Q))<->typeCorrect(P)&typeCorrect(Q)). % 1.93/2.14 all C R Q2 (typeCorrect(ifThenElse(C,R,Q2))<->typeCorrect(R)&typeCorrect(Q2)). % 1.93/2.14 l=low(zero). % 1.93/2.14 h=high(zero). % 1.93/2.14 all X (-elem(X,nil)). % 1.93/2.14 all X Z Xs (elem(X,cons(Z,Xs))<->Z=X|elem(X,Xs)). % 1.93/2.14 all X A B (eval(X,nand(A,B))<-> -eval(X,A)| -eval(X,B)). % 1.93/2.14 all X eval(X,tT). % 1.93/2.14 all X (-eval(X,fF)). % 1.93/2.14 all X Z (eval(X,var(Z))<->elem(Z,X)). % 1.93/2.14 all X (del(X,nil)=nil). % 1.93/2.14 all X Z Ys (X=Z->del(X,cons(Z,Ys))=del(X,Ys)). % 1.93/2.14 all X Z Ys (X!=Z->del(X,cons(Z,Ys))=cons(Z,del(X,Ys))). % 1.93/2.14 all X (run(X,skip)=X). % 1.93/2.14 all X Z E (eval(X,E)->run(X,assign(Z,E))=cons(Z,X)). % 1.93/2.14 all X Z E (-eval(X,E)->run(X,assign(Z,E))=del(Z,X)). % 1.93/2.14 all X P Q (run(X,se_q(P,Q))=run(run(X,P),Q)). % 1.93/2.14 all X E2 R Q2 (eval(X,E2)->run(X,ifThenElse(E2,R,Q2))=run(X,R)). % 1.93/2.14 all X E2 R Q2 (-eval(X,E2)->run(X,ifThenElse(E2,R,Q2))=run(X,Q2)). % 1.93/2.14 -(exists P S (-(typeCorrect(P)-> (elem(l,run(S,P))<->elem(l,run(cons(h,S),P)))))). % 1.93/2.14 end_of_list. % 1.93/2.14 % 1.93/2.14 -------> usable clausifies to: % 1.93/2.14 % 1.93/2.14 list(usable). % 1.93/2.14 0 [] A=A. % 1.93/2.14 0 [] head(cons(X,X2))=X. % 1.93/2.14 0 [] tail(cons(X,X2))=X2. % 1.93/2.14 0 [] nil!=cons(X,X2). % 1.93/2.14 0 [] proj1Suc(suc(X))=X. % 1.93/2.14 0 [] zero!=suc(X). % 1.93/2.14 0 [] proj1High(high(X))=X. % 1.93/2.14 0 [] proj1Low(low(X))=X. % 1.93/2.14 0 [] high(X)!=low(X2). % 1.93/2.14 0 [] proj1Nand(nand(X,X2))=X. % 1.93/2.14 0 [] proj2Nand(nand(X,X2))=X2. % 1.93/2.14 0 [] proj1Var(var(X))=X. % 1.93/2.14 0 [] nand(X,X2)!=tT. % 1.93/2.14 0 [] nand(X,X2)!=fF. % 1.93/2.14 0 [] nand(X,X2)!=var(X3). % 1.93/2.14 0 [] tT!=fF. % 1.93/2.14 0 [] tT!=var(X). % 1.93/2.14 0 [] fF!=var(X). % 1.93/2.14 0 [] proj1Assign(assign(X,X2))=X. % 1.93/2.14 0 [] proj2Assign(assign(X,X2))=X2. % 1.93/2.14 0 [] proj1Se_q(se_q(X,X2))=X. % 1.93/2.14 0 [] proj2Se_q(se_q(X,X2))=X2. % 1.93/2.14 0 [] proj1IfThenElse(ifThenElse(X,X2,X3))=X. % 1.93/2.14 0 [] proj2IfThenElse(ifThenElse(X,X2,X3))=X2. % 1.93/2.14 0 [] proj3IfThenElse(ifThenElse(X,X2,X3))=X3. % 1.93/2.14 0 [] skip!=assign(X,X2). % 1.93/2.14 0 [] skip!=se_q(X,X2). % 1.93/2.14 0 [] skip!=ifThenElse(X,X2,X3). % 1.93/2.14 0 [] assign(X,X2)!=se_q(X3,X4). % 1.93/2.14 0 [] assign(X,X2)!=ifThenElse(X3,X4,X5). % 1.93/2.14 0 [] se_q(X,X2)!=ifThenElse(X3,X4,X5). % 1.93/2.14 0 [] X=nand(proj1Nand(X),proj2Nand(X))|X=var(proj1Var(X))| -secret(X). % 1.93/2.14 0 [] -secret(nand(A,B))|secret(A)|secret(B). % 1.93/2.14 0 [] secret(nand(A,B))| -secret(A). % 1.93/2.14 0 [] secret(nand(A,B))| -secret(B). % 1.93/2.14 0 [] secret(var(high(Z))). % 1.93/2.14 0 [] -secret(var(low(X2))). % 1.93/2.14 0 [] typeCorrect(skip). % 1.93/2.15 0 [] typeCorrect(assign(high(Z),E)). % 1.93/2.15 0 [] -typeCorrect(assign(low(X2),E))| -secret(E). % 1.93/2.15 0 [] typeCorrect(assign(low(X2),E))|secret(E). % 1.93/2.15 0 [] -typeCorrect(se_q(P,Q))|typeCorrect(P). % 1.93/2.15 0 [] -typeCorrect(se_q(P,Q))|typeCorrect(Q). % 1.93/2.15 0 [] typeCorrect(se_q(P,Q))| -typeCorrect(P)| -typeCorrect(Q). % 1.93/2.15 0 [] -typeCorrect(ifThenElse(C,R,Q2))|typeCorrect(R). % 1.93/2.15 0 [] -typeCorrect(ifThenElse(C,R,Q2))|typeCorrect(Q2). % 1.93/2.15 0 [] typeCorrect(ifThenElse(C,R,Q2))| -typeCorrect(R)| -typeCorrect(Q2). % 1.93/2.15 0 [] l=low(zero). % 1.93/2.15 0 [] h=high(zero). % 1.93/2.15 0 [] -elem(X,nil). % 1.93/2.15 0 [] -elem(X,cons(Z,Xs))|Z=X|elem(X,Xs). % 1.93/2.15 0 [] elem(X,cons(Z,Xs))|Z!=X. % 1.93/2.15 0 [] elem(X,cons(Z,Xs))| -elem(X,Xs). % 1.93/2.15 0 [] -eval(X,nand(A,B))| -eval(X,A)| -eval(X,B). % 1.93/2.15 0 [] eval(X,nand(A,B))|eval(X,A). % 1.93/2.15 0 [] eval(X,nand(A,B))|eval(X,B). % 1.93/2.15 0 [] eval(X,tT). % 1.93/2.15 0 [] -eval(X,fF). % 1.93/2.15 0 [] -eval(X,var(Z))|elem(Z,X). % 1.93/2.15 0 [] eval(X,var(Z))| -elem(Z,X). % 1.93/2.15 0 [] del(X,nil)=nil. % 1.93/2.15 0 [] X!=Z|del(X,cons(Z,Ys))=del(X,Ys). % 1.93/2.15 0 [] X=Z|del(X,cons(Z,Ys))=cons(Z,del(X,Ys)). % 1.93/2.15 0 [] run(X,skip)=X. % 1.93/2.15 0 [] -eval(X,E)|run(X,assign(Z,E))=cons(Z,X). % 1.93/2.15 0 [] eval(X,E)|run(X,assign(Z,E))=del(Z,X). % 1.93/2.15 0 [] run(X,se_q(P,Q))=run(run(X,P),Q). % 1.93/2.15 0 [] -eval(X,E2)|run(X,ifThenElse(E2,R,Q2))=run(X,R). % 1.93/2.15 0 [] eval(X,E2)|run(X,ifThenElse(E2,R,Q2))=run(X,Q2). % 1.93/2.15 0 [] -typeCorrect(P)| -elem(l,run(S,P))|elem(l,run(cons(h,S),P)). % 1.93/2.15 0 [] -typeCorrect(P)|elem(l,run(S,P))| -elem(l,run(cons(h,S),P)). % 1.93/2.15 end_of_list. % 1.93/2.15 % 1.93/2.15 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=3. % 1.93/2.15 % 1.93/2.15 This ia a non-Horn set with equality. The strategy will be % 1.93/2.15 Knuth-Bendix, ordered hyper_res, factoring, and unit % 1.93/2.15 deletion, with positive clauses in sos and nonpositive % 1.93/2.15 clauses in usable. % 1.93/2.15 % 1.93/2.15 dependent: set(knuth_bendix). % 1.93/2.15 dependent: set(anl_eq). % 1.93/2.15 dependent: set(para_from). % 1.93/2.15 dependent: set(para_into). % 1.93/2.15 dependent: clear(para_from_right). % 1.93/2.15 dependent: clear(para_into_right). % 1.93/2.15 dependent: set(para_from_vars). % 1.93/2.15 dependent: set(eq_units_both_ways). % 1.93/2.15 dependent: set(dynamic_demod_all). % 1.93/2.15 dependent: set(dynamic_demod). % 1.93/2.15 dependent: set(order_eq). % 1.93/2.15 dependent: set(back_demod). % 1.93/2.15 dependent: set(lrpo). % 1.93/2.15 dependent: set(hyper_res). % 1.93/2.15 dependent: set(unit_deletion). % 1.93/2.15 dependent: set(factor). % 1.93/2.15 % 1.93/2.15 ------------> process usable: % 1.93/2.15 ** KEPT (pick-wt=5): 2 [copy,1,flip.1] cons(A,B)!=nil. % 1.93/2.15 ** KEPT (pick-wt=4): 4 [copy,3,flip.1] suc(A)!=zero. % 1.93/2.15 ** KEPT (pick-wt=5): 5 [] high(A)!=low(B). % 1.93/2.15 ** KEPT (pick-wt=5): 6 [] nand(A,B)!=tT. % 1.93/2.15 ** KEPT (pick-wt=5): 7 [] nand(A,B)!=fF. % 1.93/2.15 ** KEPT (pick-wt=6): 8 [] nand(A,B)!=var(C). % 1.93/2.15 ** KEPT (pick-wt=3): 9 [] tT!=fF. % 1.93/2.15 ** KEPT (pick-wt=4): 11 [copy,10,flip.1] var(A)!=tT. % 1.93/2.15 ** KEPT (pick-wt=4): 13 [copy,12,flip.1] var(A)!=fF. % 1.93/2.15 ** KEPT (pick-wt=5): 15 [copy,14,flip.1] assign(A,B)!=skip. % 1.93/2.15 ** KEPT (pick-wt=5): 17 [copy,16,flip.1] se_q(A,B)!=skip. % 1.93/2.15 ** KEPT (pick-wt=6): 19 [copy,18,flip.1] ifThenElse(A,B,C)!=skip. % 1.93/2.15 ** KEPT (pick-wt=7): 20 [] assign(A,B)!=se_q(C,D). % 1.93/2.15 ** KEPT (pick-wt=8): 21 [] assign(A,B)!=ifThenElse(C,D,E). % 1.93/2.15 ** KEPT (pick-wt=8): 22 [] se_q(A,B)!=ifThenElse(C,D,E). % 1.93/2.15 ** KEPT (pick-wt=14): 24 [copy,23,flip.1,flip.2] nand(proj1Nand(A),proj2Nand(A))=A|var(proj1Var(A))=A| -secret(A). % 1.93/2.15 ** KEPT (pick-wt=8): 25 [] -secret(nand(A,B))|secret(A)|secret(B). % 1.93/2.15 ** KEPT (pick-wt=6): 26 [] secret(nand(A,B))| -secret(A). % 1.93/2.15 ** KEPT (pick-wt=6): 27 [] secret(nand(A,B))| -secret(B). % 1.93/2.15 ** KEPT (pick-wt=4): 28 [] -secret(var(low(A))). % 1.93/2.15 ** KEPT (pick-wt=7): 29 [] -typeCorrect(assign(low(A),B))| -secret(B). % 1.93/2.15 ** KEPT (pick-wt=6): 30 [] -typeCorrect(se_q(A,B))|typeCorrect(A). % 1.93/2.15 ** KEPT (pick-wt=6): 31 [] -typeCorrect(se_q(A,B))|typeCorrect(B). % 1.93/2.15 ** KEPT (pick-wt=8): 32 [] typeCorrect(se_q(A,B))| -typeCorrect(A)| -typeCorrect(B). % 1.93/2.15 ** KEPT (pick-wt=7): 33 [] -typeCorrect(ifThenElse(A,B,C))|typeCorrect(B). % 1.93/2.15 ** KEPT (pick-wt=7): 34 [] -typeCorrect(ifThenElse(A,B,C))|typeCorrect(C). % 1.93/2.15 ** KEPT (pick-wt=9): 35 [] typeCorrect(ifThenElse(A,B,C))| -typeCorrect(B)| -typeCorrect(C). % 1.93/2.15 ** KEPT (pick-wt=3): 36 [] -elem(A,nil). % 1.93/2.15 ** KEPT (pick-wt=11): 37 [] -elem(A,cons(B,C))|B=A|elem(A,C). % 1.93/2.15 ** KEPT (pick-wt=8): 38 [] elem(A,cons(B,C))|B!=A. % 1.93/2.15 ** KEPT (pick-wt=8): 39 [] elem(A,cons(B,C))| -elem(A,C). % 1.93/2.15 ** KEPT (pick-wt=11): 40 [] -eval(A,nand(B,C))| -eval(A,B)| -eval(A,C). % 1.93/2.15 ** KEPT (pick-wt=3): 41 [] -eval(A,fF). % 1.93/2.15 ** KEPT (pick-wt=7): 42 [] -eval(A,var(B))|elem(B,A). % 1.93/2.15 ** KEPT (pick-wt=7): 43 [] eval(A,var(B))| -elem(B,A). % 1.93/2.15 ** KEPT (pick-wt=12): 44 [] A!=B|del(A,cons(B,C))=del(A,C). % 1.93/2.15 ** KEPT (pick-wt=12): 45 [] -eval(A,B)|run(A,assign(C,B))=cons(C,A). % 1.93/2.15 ** KEPT (pick-wt=13): 46 [] -eval(A,B)|run(A,ifThenElse(B,C,D))=run(A,C). % 1.93/2.15 ** KEPT (pick-wt=14): 47 [] -typeCorrect(A)| -elem(l,run(B,A))|elem(l,run(cons(h,B),A)). % 1.93/2.15 ** KEPT (pick-wt=14): 48 [] -typeCorrect(A)|elem(l,run(B,A))| -elem(l,run(cons(h,B),A)). % 1.93/2.15 ** KEPT (pick-wt=5): 49 [copy,5,flip.1] low(A)!=high(B). % 1.93/2.15 ** KEPT (pick-wt=6): 50 [copy,8,flip.1] var(A)!=nand(B,C). % 1.93/2.15 ** KEPT (pick-wt=7): 51 [copy,20,flip.1] se_q(A,B)!=assign(C,D). % 1.93/2.15 ** KEPT (pick-wt=8): 52 [copy,21,flip.1] ifThenElse(A,B,C)!=assign(D,E). % 1.93/2.15 ** KEPT (pick-wt=8): 53 [copy,22,flip.1] ifThenElse(A,B,C)!=se_q(D,E). % 1.93/2.15 Following clause subsumed by 5 during input processing: 0 [copy,49,flip.1] high(A)!=low(B). % 1.93/2.15 Following clause subsumed by 8 during input processing: 0 [copy,50,flip.1] nand(A,B)!=var(C). % 1.93/2.15 Following clause subsumed by 20 during input processing: 0 [copy,51,flip.1] assign(A,B)!=se_q(C,D). % 1.93/2.15 Following clause subsumed by 21 during input processing: 0 [copy,52,flip.1] assign(A,B)!=ifThenElse(C,D,E). % 1.93/2.15 Following clause subsumed by 22 during input processing: 0 [copy,53,flip.1] se_q(A,B)!=ifThenElse(C,D,E). % 1.93/2.15 % 1.93/2.15 ------------> process sos: % 1.93/2.15 ** KEPT (pick-wt=3): 58 [] A=A. % 1.93/2.15 ** KEPT (pick-wt=6): 59 [] head(cons(A,B))=A. % 1.93/2.15 ---> New Demodulator: 60 [new_demod,59] head(cons(A,B))=A. % 1.93/2.15 ** KEPT (pick-wt=6): 61 [] tail(cons(A,B))=B. % 1.93/2.15 ---> New Demodulator: 62 [new_demod,61] tail(cons(A,B))=B. % 1.93/2.15 ** KEPT (pick-wt=5): 63 [] proj1Suc(suc(A))=A. % 1.93/2.15 ---> New Demodulator: 64 [new_demod,63] proj1Suc(suc(A))=A. % 1.93/2.15 ** KEPT (pick-wt=5): 65 [] proj1High(high(A))=A. % 1.93/2.15 ---> New Demodulator: 66 [new_demod,65] proj1High(high(A))=A. % 1.93/2.15 ** KEPT (pick-wt=5): 67 [] proj1Low(low(A))=A. % 1.93/2.15 ---> New Demodulator: 68 [new_demod,67] proj1Low(low(A))=A. % 1.93/2.15 ** KEPT (pick-wt=6): 69 [] proj1Nand(nand(A,B))=A. % 1.93/2.15 ---> New Demodulator: 70 [new_demod,69] proj1Nand(nand(A,B))=A. % 1.93/2.15 ** KEPT (pick-wt=6): 71 [] proj2Nand(nand(A,B))=B. % 1.93/2.15 ---> New Demodulator: 72 [new_demod,71] proj2Nand(nand(A,B))=B. % 1.93/2.15 ** KEPT (pick-wt=5): 73 [] proj1Var(var(A))=A. % 1.93/2.15 ---> New Demodulator: 74 [new_demod,73] proj1Var(var(A))=A. % 1.93/2.15 ** KEPT (pick-wt=6): 75 [] proj1Assign(assign(A,B))=A. % 1.93/2.15 ---> New Demodulator: 76 [new_demod,75] proj1Assign(assign(A,B))=A. % 1.93/2.15 ** KEPT (pick-wt=6): 77 [] proj2Assign(assign(A,B))=B. % 1.93/2.15 ---> New Demodulator: 78 [new_demod,77] proj2Assign(assign(A,B))=B. % 1.93/2.15 ** KEPT (pick-wt=6): 79 [] proj1Se_q(se_q(A,B))=A. % 1.93/2.15 ---> New Demodulator: 80 [new_demod,79] proj1Se_q(se_q(A,B))=A. % 1.93/2.15 ** KEPT (pick-wt=6): 81 [] proj2Se_q(se_q(A,B))=B. % 1.93/2.15 ---> New Demodulator: 82 [new_demod,81] proj2Se_q(se_q(A,B))=B. % 1.93/2.15 ** KEPT (pick-wt=7): 83 [] proj1IfThenElse(ifThenElse(A,B,C))=A. % 1.93/2.15 ---> New Demodulator: 84 [new_demod,83] proj1IfThenElse(ifThenElse(A,B,C))=A. % 1.93/2.15 ** KEPT (pick-wt=7): 85 [] proj2IfThenElse(ifThenElse(A,B,C))=B. % 1.93/2.15 ---> New Demodulator: 86 [new_demod,85] proj2IfThenElse(ifThenElse(A,B,C))=B. % 1.93/2.15 ** KEPT (pick-wt=7): 87 [] proj3IfThenElse(ifThenElse(A,B,C))=C. % 1.93/2.15 ---> New Demodulator: 88 [new_demod,87] proj3IfThenElse(ifThenElse(A,B,C))=C. % 1.93/2.15 ** KEPT (pick-wt=4): 89 [] secret(var(high(A))). % 1.93/2.15 ** KEPT (pick-wt=2): 90 [] typeCorrect(skip). % 1.93/2.15 ** KEPT (pick-wt=5): 91 [] typeCorrect(assign(high(A),B)). % 1.93/2.15 ** KEPT (pick-wt=7): 92 [] typeCorrect(assign(low(A),B))|secret(B). % 1.93/2.15 ** KEPT (pick-wt=4): 94 [copy,93,flip.1] low(zero)=l. % 1.93/2.15 ---> New Demodulator: 95 [new_demod,94] low(zero)=l. % 1.93/2.15 ** KEPT (pick-wt=4): 97 [copy,96,flip.1] high(zero)=h. % 1.93/2.15 ---> New Demodulator: 98 [new_demod,97] high(zero)=h. % 1.93/2.15 ** KEPT (pick-wt=8): 99 [] eval(A,nand(B,C))|eval(A,B). % 1.93/2.15 ** KEPT (pick-wt=8): 100 [] eval(A,nand(B,C))|eval(A,C). % 1.93/2.15 ** KEPT (pick-wt=3): 101 [] eval(A,tT). % 1.93/2.15 ** KEPT (pick-wt=5): 102 [] del(A,nil)=nil. % 1.93/2.15 ---> New Demodulator: 103 [new_demod,102] del(A,nil)=nil. % 1.93/2.15 ** KEPT (pick-wt=14): 104 [] A=B|del(A,cons(B,C))=cons(B,del(A,C)). % 1.93/2.15 ** KEPT (pick-wt=5): 105 [] run(A,skip)=A. % 1.93/2.15 ---> New Demodulator: 106 [new_demod,105] run(A,skip)=A. % 1.93/2.15 ** KEPT (pick-wt=12): 107 [] Terminated % 299.87/300.02 Otter interrupted % 299.87/300.02 PROOF NOT FOUND %------------------------------------------------------------------------------