%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWX208-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n004.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:25 PM UTC 2026 % Result : Unknown 1.92s 2.68s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX208-1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : otter-tptp-script %s % 0.16/0.33 % Computer : n004.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.33 % CPULimit : 300 % 0.16/0.33 % WCLimit : 300 % 0.16/0.33 % DateTime : Tue May 5 11:39:47 EDT 2026 % 0.16/0.33 % CPUTime : % 1.92/2.62 ----- Otter 3.3f, August 2004 ----- % 1.92/2.62 The process was started by sandbox on n004.cluster.edu, % 1.92/2.62 Tue May 5 11:39:47 2026 % 1.92/2.62 The command was "./otter". The process ID is 28158. % 1.92/2.62 % 1.92/2.62 set(prolog_style_variables). % 1.92/2.62 set(auto). % 1.92/2.62 dependent: set(auto1). % 1.92/2.62 dependent: set(process_input). % 1.92/2.62 dependent: clear(print_kept). % 1.92/2.62 dependent: clear(print_new_demod). % 1.92/2.62 dependent: clear(print_back_demod). % 1.92/2.62 dependent: clear(print_back_sub). % 1.92/2.62 dependent: set(control_memory). % 1.92/2.62 dependent: assign(max_mem, 12000). % 1.92/2.62 dependent: assign(pick_given_ratio, 4). % 1.92/2.62 dependent: assign(stats_level, 1). % 1.92/2.62 dependent: assign(max_seconds, 10800). % 1.92/2.62 clear(print_given). % 1.92/2.62 % 1.92/2.62 list(usable). % 1.92/2.62 0 [] A=A. % 1.92/2.62 0 [] aux(N,pair2(D1,N2))=pair2(D1,s(N2)). % 1.92/2.62 0 [] aux2(X,left(D))=pair2(D,z). % 1.92/2.62 0 [] aux2(X,right(N))=aux(N,mod10(N)). % 1.92/2.62 0 [] aux3(X,Z,pair2(A1,N))=showNumnum(cons(A1,X),N). % 1.92/2.62 0 [] impl(btrue,Q)=Q. % 1.92/2.62 0 [] impl(bfalse,Q)=btrue. % 1.92/2.62 0 [] append(nil,Y)=Y. % 1.92/2.62 0 [] append(cons(Z,Xs),Y)=cons(Z,append(Xs,Y)). % 1.92/2.62 0 [] x2(z,z)=z. % 1.92/2.62 0 [] x2(z,s(Z))=z. % 1.92/2.62 0 [] x2(s(N),z)=s(N). % 1.92/2.62 0 [] x2(s(N),s(M))=x2(N,M). % 1.92/2.62 0 [] min10(z)=left(dIG0). % 1.92/2.62 0 [] min10(s(z))=left(dIG1). % 1.92/2.62 0 [] min10(s(s(z)))=left(dIG2). % 1.92/2.62 0 [] min10(s(s(s(z))))=left(dIG3). % 1.92/2.62 0 [] min10(s(s(s(s(z)))))=left(dIG4). % 1.92/2.62 0 [] min10(s(s(s(s(s(z))))))=left(dIG5). % 1.92/2.62 0 [] min10(s(s(s(s(s(s(z)))))))=left(dIG6). % 1.92/2.62 0 [] min10(s(s(s(s(s(s(s(z))))))))=left(dIG7). % 1.92/2.62 0 [] min10(s(s(s(s(s(s(s(s(z)))))))))=left(dIG8). % 1.92/2.62 0 [] min10(s(s(s(s(s(s(s(s(s(z))))))))))=left(dIG9). % 1.92/2.62 0 [] min10(s(s(s(s(s(s(s(s(s(s(X9)))))))))))=right(x2(s(s(s(s(s(s(s(s(s(s(X9)))))))))),s(s(s(s(s(s(s(s(s(s(z)))))))))))). % 1.92/2.62 0 [] mod10(X)=aux2(X,min10(X)). % 1.92/2.62 0 [] showNumnum(X,z)=X. % 1.92/2.62 0 [] showNumnum(X,s(Z))=aux3(X,Z,mod10(s(Z))). % 1.92/2.62 0 [] showNum(z)=cons(dIG0,nil). % 1.92/2.62 0 [] showNum(s(Y))=showNumnum(nil,s(Y)). % 1.92/2.62 0 [] show(x)=cons(cHARX,nil). % 1.92/2.62 0 [] show(add(B,C))=append(show(B),append(cons(pLUS,nil),show(C))). % 1.92/2.62 0 [] show(mul(A3,B2))=append(showF(A3),append(cons(mULT,nil),showF(B2))). % 1.92/2.62 0 [] show(num(N))=showNum(N). % 1.92/2.62 0 [] showF(add(Y,Z))=cons(pAR1,append(show(add(Y,Z)),cons(pAR2,nil))). % 1.92/2.62 0 [] showF(x)=show(x). % 1.92/2.62 0 [] showF(mul(X,X2))=show(mul(X,X2)). % 1.92/2.62 0 [] showF(num(X))=show(num(X)). % 1.92/2.62 0 [] prop3(X)=impl(e_q(show(X),cons(pAR1,cons(pAR1,cons(cHARX,cons(pLUS,cons(dIG5,cons(pAR2,cons(pLUS,cons(dIG7,cons(pAR2,cons(mULT,cons(cHARX,nil)))))))))))),e_q5(btrue,bfalse)). % 1.92/2.62 0 [] e_q4(pAR1,pAR2)=bfalse. % 1.92/2.62 0 [] e_q4(pAR1,pLUS)=bfalse. % 1.92/2.62 0 [] e_q4(pAR1,mULT)=bfalse. % 1.92/2.62 0 [] e_q4(pAR1,cHARX)=bfalse. % 1.92/2.62 0 [] e_q4(pAR1,dIG0)=bfalse. % 1.92/2.62 0 [] e_q4(pAR1,dIG1)=bfalse. % 1.92/2.62 0 [] e_q4(pAR1,dIG2)=bfalse. % 1.92/2.62 0 [] e_q4(pAR1,dIG3)=bfalse. % 1.92/2.62 0 [] e_q4(pAR1,dIG4)=bfalse. % 1.92/2.62 0 [] e_q4(pAR1,dIG5)=bfalse. % 1.92/2.62 0 [] e_q4(pAR1,dIG6)=bfalse. % 1.92/2.62 0 [] e_q4(pAR1,dIG7)=bfalse. % 1.92/2.62 0 [] e_q4(pAR1,dIG8)=bfalse. % 1.92/2.62 0 [] e_q4(pAR1,dIG9)=bfalse. % 1.92/2.62 0 [] e_q4(pAR2,pAR1)=bfalse. % 1.92/2.62 0 [] e_q4(pAR2,pLUS)=bfalse. % 1.92/2.62 0 [] e_q4(pAR2,mULT)=bfalse. % 1.92/2.62 0 [] e_q4(pAR2,cHARX)=bfalse. % 1.92/2.62 0 [] e_q4(pAR2,dIG0)=bfalse. % 1.92/2.62 0 [] e_q4(pAR2,dIG1)=bfalse. % 1.92/2.62 0 [] e_q4(pAR2,dIG2)=bfalse. % 1.92/2.62 0 [] e_q4(pAR2,dIG3)=bfalse. % 1.92/2.62 0 [] e_q4(pAR2,dIG4)=bfalse. % 1.92/2.62 0 [] e_q4(pAR2,dIG5)=bfalse. % 1.92/2.62 0 [] e_q4(pAR2,dIG6)=bfalse. % 1.92/2.62 0 [] e_q4(pAR2,dIG7)=bfalse. % 1.92/2.62 0 [] e_q4(pAR2,dIG8)=bfalse. % 1.92/2.62 0 [] e_q4(pAR2,dIG9)=bfalse. % 1.92/2.62 0 [] e_q4(pLUS,pAR1)=bfalse. % 1.92/2.62 0 [] e_q4(pLUS,pAR2)=bfalse. % 1.92/2.62 0 [] e_q4(pLUS,mULT)=bfalse. % 1.92/2.62 0 [] e_q4(pLUS,cHARX)=bfalse. % 1.92/2.62 0 [] e_q4(pLUS,dIG0)=bfalse. % 1.92/2.62 0 [] e_q4(pLUS,dIG1)=bfalse. % 1.92/2.62 0 [] e_q4(pLUS,dIG2)=bfalse. % 1.92/2.62 0 [] e_q4(pLUS,dIG3)=bfalse. % 1.92/2.62 0 [] e_q4(pLUS,dIG4)=bfalse. % 1.92/2.62 0 [] e_q4(pLUS,dIG5)=bfalse. % 1.92/2.62 0 [] e_q4(pLUS,dIG6)=bfalse. % 1.92/2.62 0 [] e_q4(pLUS,dIG7)=bfalse. % 1.92/2.62 0 [] e_q4(pLUS,dIG8)=bfalse. % 1.92/2.62 0 [] e_q4(pLUS,dIG9)=bfalse. % 1.92/2.62 0 [] e_q4(mULT,pAR1)=bfalse. % 1.92/2.62 0 [] e_q4(mULT,pAR2)=bfalse. % 1.92/2.62 0 [] e_q4(mULT,pLUS)=bfalse. % 1.92/2.62 0 [] e_q4(mULT,cHARX)=bfalse. % 1.92/2.62 0 [] e_q4(mULT,dIG0)=bfalse. % 1.92/2.62 0 [] e_q4(mULT,dIG1)=bfalse. % 1.92/2.62 0 [] e_q4(mULT,dIG2)=bfalse. % 1.92/2.62 0 [] e_q4(mULT,dIG3)=bfalse. % 1.92/2.62 0 [] e_q4(mULT,dIG4)=bfalse. % 1.92/2.62 0 [] e_q4(mULT,dIG5)=bfalse. % 1.92/2.62 0 [] e_q4(mULT,dIG6)=bfalse. % 1.92/2.62 0 [] e_q4(mULT,dIG7)=bfalse. % 1.92/2.62 0 [] e_q4(mULT,dIG8)=bfalse. % 1.92/2.62 0 [] e_q4(mULT,dIG9)=bfalse. % 1.92/2.62 0 [] e_q4(cHARX,pAR1)=bfalse. % 1.92/2.62 0 [] e_q4(cHARX,pAR2)=bfalse. % 1.92/2.62 0 [] e_q4(cHARX,pLUS)=bfalse. % 1.92/2.62 0 [] e_q4(cHARX,mULT)=bfalse. % 1.92/2.62 0 [] e_q4(cHARX,dIG0)=bfalse. % 1.92/2.62 0 [] e_q4(cHARX,dIG1)=bfalse. % 1.92/2.62 0 [] e_q4(cHARX,dIG2)=bfalse. % 1.92/2.62 0 [] e_q4(cHARX,dIG3)=bfalse. % 1.92/2.62 0 [] e_q4(cHARX,dIG4)=bfalse. % 1.92/2.62 0 [] e_q4(cHARX,dIG5)=bfalse. % 1.92/2.62 0 [] e_q4(cHARX,dIG6)=bfalse. % 1.92/2.62 0 [] e_q4(cHARX,dIG7)=bfalse. % 1.92/2.62 0 [] e_q4(cHARX,dIG8)=bfalse. % 1.92/2.62 0 [] e_q4(cHARX,dIG9)=bfalse. % 1.92/2.62 0 [] e_q4(dIG0,pAR1)=bfalse. % 1.92/2.62 0 [] e_q4(dIG0,pAR2)=bfalse. % 1.92/2.62 0 [] e_q4(dIG0,pLUS)=bfalse. % 1.92/2.62 0 [] e_q4(dIG0,mULT)=bfalse. % 1.92/2.62 0 [] e_q4(dIG0,cHARX)=bfalse. % 1.92/2.62 0 [] e_q4(dIG0,dIG1)=bfalse. % 1.92/2.62 0 [] e_q4(dIG0,dIG2)=bfalse. % 1.92/2.62 0 [] e_q4(dIG0,dIG3)=bfalse. % 1.92/2.62 0 [] e_q4(dIG0,dIG4)=bfalse. % 1.92/2.62 0 [] e_q4(dIG0,dIG5)=bfalse. % 1.92/2.62 0 [] e_q4(dIG0,dIG6)=bfalse. % 1.92/2.62 0 [] e_q4(dIG0,dIG7)=bfalse. % 1.92/2.62 0 [] e_q4(dIG0,dIG8)=bfalse. % 1.92/2.62 0 [] e_q4(dIG0,dIG9)=bfalse. % 1.92/2.62 0 [] e_q4(dIG1,pAR1)=bfalse. % 1.92/2.62 0 [] e_q4(dIG1,pAR2)=bfalse. % 1.92/2.62 0 [] e_q4(dIG1,pLUS)=bfalse. % 1.92/2.62 0 [] e_q4(dIG1,mULT)=bfalse. % 1.92/2.62 0 [] e_q4(dIG1,cHARX)=bfalse. % 1.92/2.62 0 [] e_q4(dIG1,dIG0)=bfalse. % 1.92/2.62 0 [] e_q4(dIG1,dIG2)=bfalse. % 1.92/2.62 0 [] e_q4(dIG1,dIG3)=bfalse. % 1.92/2.62 0 [] e_q4(dIG1,dIG4)=bfalse. % 1.92/2.62 0 [] e_q4(dIG1,dIG5)=bfalse. % 1.92/2.62 0 [] e_q4(dIG1,dIG6)=bfalse. % 1.92/2.62 0 [] e_q4(dIG1,dIG7)=bfalse. % 1.92/2.62 0 [] e_q4(dIG1,dIG8)=bfalse. % 1.92/2.62 0 [] e_q4(dIG1,dIG9)=bfalse. % 1.92/2.62 0 [] e_q4(dIG2,pAR1)=bfalse. % 1.92/2.62 0 [] e_q4(dIG2,pAR2)=bfalse. % 1.92/2.62 0 [] e_q4(dIG2,pLUS)=bfalse. % 1.92/2.62 0 [] e_q4(dIG2,mULT)=bfalse. % 1.92/2.62 0 [] e_q4(dIG2,cHARX)=bfalse. % 1.92/2.62 0 [] e_q4(dIG2,dIG0)=bfalse. % 1.92/2.62 0 [] e_q4(dIG2,dIG1)=bfalse. % 1.92/2.62 0 [] e_q4(dIG2,dIG3)=bfalse. % 1.92/2.62 0 [] e_q4(dIG2,dIG4)=bfalse. % 1.92/2.62 0 [] e_q4(dIG2,dIG5)=bfalse. % 1.92/2.62 0 [] e_q4(dIG2,dIG6)=bfalse. % 1.92/2.62 0 [] e_q4(dIG2,dIG7)=bfalse. % 1.92/2.62 0 [] e_q4(dIG2,dIG8)=bfalse. % 1.92/2.62 0 [] e_q4(dIG2,dIG9)=bfalse. % 1.92/2.62 0 [] e_q4(dIG3,pAR1)=bfalse. % 1.92/2.62 0 [] e_q4(dIG3,pAR2)=bfalse. % 1.92/2.62 0 [] e_q4(dIG3,pLUS)=bfalse. % 1.92/2.62 0 [] e_q4(dIG3,mULT)=bfalse. % 1.92/2.62 0 [] e_q4(dIG3,cHARX)=bfalse. % 1.92/2.62 0 [] e_q4(dIG3,dIG0)=bfalse. % 1.92/2.62 0 [] e_q4(dIG3,dIG1)=bfalse. % 1.92/2.62 0 [] e_q4(dIG3,dIG2)=bfalse. % 1.92/2.62 0 [] e_q4(dIG3,dIG4)=bfalse. % 1.92/2.62 0 [] e_q4(dIG3,dIG5)=bfalse. % 1.92/2.62 0 [] e_q4(dIG3,dIG6)=bfalse. % 1.92/2.62 0 [] e_q4(dIG3,dIG7)=bfalse. % 1.92/2.62 0 [] e_q4(dIG3,dIG8)=bfalse. % 1.92/2.62 0 [] e_q4(dIG3,dIG9)=bfalse. % 1.92/2.62 0 [] e_q4(dIG4,pAR1)=bfalse. % 1.92/2.62 0 [] e_q4(dIG4,pAR2)=bfalse. % 1.92/2.62 0 [] e_q4(dIG4,pLUS)=bfalse. % 1.92/2.62 0 [] e_q4(dIG4,mULT)=bfalse. % 1.92/2.62 0 [] e_q4(dIG4,cHARX)=bfalse. % 1.92/2.62 0 [] e_q4(dIG4,dIG0)=bfalse. % 1.92/2.62 0 [] e_q4(dIG4,dIG1)=bfalse. % 1.92/2.62 0 [] e_q4(dIG4,dIG2)=bfalse. % 1.92/2.62 0 [] e_q4(dIG4,dIG3)=bfalse. % 1.92/2.62 0 [] e_q4(dIG4,dIG5)=bfalse. % 1.92/2.62 0 [] e_q4(dIG4,dIG6)=bfalse. % 1.92/2.62 0 [] e_q4(dIG4,dIG7)=bfalse. % 1.92/2.62 0 [] e_q4(dIG4,dIG8)=bfalse. % 1.92/2.62 0 [] e_q4(dIG4,dIG9)=bfalse. % 1.92/2.62 0 [] e_q4(dIG5,pAR1)=bfalse. % 1.92/2.62 0 [] e_q4(dIG5,pAR2)=bfalse. % 1.92/2.62 0 [] e_q4(dIG5,pLUS)=bfalse. % 1.92/2.62 0 [] e_q4(dIG5,mULT)=bfalse. % 1.92/2.62 0 [] e_q4(dIG5,cHARX)=bfalse. % 1.92/2.62 0 [] e_q4(dIG5,dIG0)=bfalse. % 1.92/2.62 0 [] e_q4(dIG5,dIG1)=bfalse. % 1.92/2.62 0 [] e_q4(dIG5,dIG2)=bfalse. % 1.92/2.62 0 [] e_q4(dIG5,dIG3)=bfalse. % 1.92/2.62 0 [] e_q4(dIG5,dIG4)=bfalse. % 1.92/2.62 0 [] e_q4(dIG5,dIG6)=bfalse. % 1.92/2.62 0 [] e_q4(dIG5,dIG7)=bfalse. % 1.92/2.62 0 [] e_q4(dIG5,dIG8)=bfalse. % 1.92/2.62 0 [] e_q4(dIG5,dIG9)=bfalse. % 1.92/2.62 0 [] e_q4(dIG6,pAR1)=bfalse. % 1.92/2.62 0 [] e_q4(dIG6,pAR2)=bfalse. % 1.92/2.62 0 [] e_q4(dIG6,pLUS)=bfalse. % 1.92/2.62 0 [] e_q4(dIG6,mULT)=bfalse. % 1.92/2.62 0 [] e_q4(dIG6,cHARX)=bfalse. % 1.92/2.62 0 [] e_q4(dIG6,dIG0)=bfalse. % 1.92/2.62 0 [] e_q4(dIG6,dIG1)=bfalse. % 1.92/2.62 0 [] e_q4(dIG6,dIG2)=bfalse. % 1.92/2.62 0 [] e_q4(dIG6,dIG3)=bfalse. % 1.92/2.62 0 [] e_q4(dIG6,dIG4)=bfalse. % 1.92/2.62 0 [] e_q4(dIG6,dIG5)=bfalse. % 1.92/2.62 0 [] e_q4(dIG6,dIG7)=bfalse. % 1.92/2.62 0 [] e_q4(dIG6,dIG8)=bfalse. % 1.92/2.62 0 [] e_q4(dIG6,dIG9)=bfalse. % 1.92/2.63 0 [] e_q4(dIG7,pAR1)=bfalse. % 1.92/2.63 0 [] e_q4(dIG7,pAR2)=bfalse. % 1.92/2.63 0 [] e_q4(dIG7,pLUS)=bfalse. % 1.92/2.63 0 [] e_q4(dIG7,mULT)=bfalse. % 1.92/2.63 0 [] e_q4(dIG7,cHARX)=bfalse. % 1.92/2.63 0 [] e_q4(dIG7,dIG0)=bfalse. % 1.92/2.63 0 [] e_q4(dIG7,dIG1)=bfalse. % 1.92/2.63 0 [] e_q4(dIG7,dIG2)=bfalse. % 1.92/2.63 0 [] e_q4(dIG7,dIG3)=bfalse. % 1.92/2.63 0 [] e_q4(dIG7,dIG4)=bfalse. % 1.92/2.63 0 [] e_q4(dIG7,dIG5)=bfalse. % 1.92/2.63 0 [] e_q4(dIG7,dIG6)=bfalse. % 1.92/2.63 0 [] e_q4(dIG7,dIG8)=bfalse. % 1.92/2.63 0 [] e_q4(dIG7,dIG9)=bfalse. % 1.92/2.63 0 [] e_q4(dIG8,pAR1)=bfalse. % 1.92/2.63 0 [] e_q4(dIG8,pAR2)=bfalse. % 1.92/2.63 0 [] e_q4(dIG8,pLUS)=bfalse. % 1.92/2.63 0 [] e_q4(dIG8,mULT)=bfalse. % 1.92/2.63 0 [] e_q4(dIG8,cHARX)=bfalse. % 1.92/2.63 0 [] e_q4(dIG8,dIG0)=bfalse. % 1.92/2.63 0 [] e_q4(dIG8,dIG1)=bfalse. % 1.92/2.63 0 [] e_q4(dIG8,dIG2)=bfalse. % 1.92/2.63 0 [] e_q4(dIG8,dIG3)=bfalse. % 1.92/2.63 0 [] e_q4(dIG8,dIG4)=bfalse. % 1.92/2.63 0 [] e_q4(dIG8,dIG5)=bfalse. % 1.92/2.63 0 [] e_q4(dIG8,dIG6)=bfalse. % 1.92/2.63 0 [] e_q4(dIG8,dIG7)=bfalse. % 1.92/2.63 0 [] e_q4(dIG8,dIG9)=bfalse. % 1.92/2.63 0 [] e_q4(dIG9,pAR1)=bfalse. % 1.92/2.63 0 [] e_q4(dIG9,pAR2)=bfalse. % 1.92/2.63 0 [] e_q4(dIG9,pLUS)=bfalse. % 1.92/2.63 0 [] e_q4(dIG9,mULT)=bfalse. % 1.92/2.63 0 [] e_q4(dIG9,cHARX)=bfalse. % 1.92/2.63 0 [] e_q4(dIG9,dIG0)=bfalse. % 1.92/2.63 0 [] e_q4(dIG9,dIG1)=bfalse. % 1.92/2.63 0 [] e_q4(dIG9,dIG2)=bfalse. % 1.92/2.63 0 [] e_q4(dIG9,dIG3)=bfalse. % 1.92/2.63 0 [] e_q4(dIG9,dIG4)=bfalse. % 1.92/2.63 0 [] e_q4(dIG9,dIG5)=bfalse. % 1.92/2.63 0 [] e_q4(dIG9,dIG6)=bfalse. % 1.92/2.63 0 [] e_q4(dIG9,dIG7)=bfalse. % 1.92/2.63 0 [] e_q4(dIG9,dIG8)=bfalse. % 1.92/2.63 0 [] e_q5(bfalse,btrue)=bfalse. % 1.92/2.63 0 [] e_q5(btrue,bfalse)=bfalse. % 1.92/2.63 0 [] e_q3(X,Z)!=bfalse|e_q3(add(X,Y),add(Z,X2))=bfalse. % 1.92/2.63 0 [] e_q3(X,Z)!=btrue|e_q3(add(X,Y),add(Z,X2))=e_q3(Y,X2). % 1.92/2.63 0 [] e_q3(X,Z)!=bfalse|e_q3(mul(X,Y),mul(Z,X2))=bfalse. % 1.92/2.63 0 [] e_q3(X,Z)!=btrue|e_q3(mul(X,Y),mul(Z,X2))=e_q3(Y,X2). % 1.92/2.63 0 [] e_q3(num(X),num(Y))=e_q2(X,Y). % 1.92/2.63 0 [] e_q3(x,add(X,Y))=bfalse. % 1.92/2.63 0 [] e_q3(x,mul(X,Y))=bfalse. % 1.92/2.63 0 [] e_q3(x,num(X))=bfalse. % 1.92/2.63 0 [] e_q3(add(X,Y),x)=bfalse. % 1.92/2.63 0 [] e_q3(add(X,Y),mul(Z,X2))=bfalse. % 1.92/2.63 0 [] e_q3(add(X,Y),num(Z))=bfalse. % 1.92/2.63 0 [] e_q3(mul(X,Y),x)=bfalse. % 1.92/2.63 0 [] e_q3(mul(X,Y),add(Z,X2))=bfalse. % 1.92/2.63 0 [] e_q3(mul(X,Y),num(Z))=bfalse. % 1.92/2.63 0 [] e_q3(num(X),x)=bfalse. % 1.92/2.63 0 [] e_q3(num(X),add(Y,Z))=bfalse. % 1.92/2.63 0 [] e_q3(num(X),mul(Y,Z))=bfalse. % 1.92/2.63 0 [] e_q2(s(X),s(Y))=e_q2(X,Y). % 1.92/2.63 0 [] e_q2(z,s(X))=bfalse. % 1.92/2.63 0 [] e_q2(s(X),z)=bfalse. % 1.92/2.63 0 [] e_q(X,X)=btrue. % 1.92/2.63 0 [] e_q2(X,X)=btrue. % 1.92/2.63 0 [] e_q3(X,X)=btrue. % 1.92/2.63 0 [] e_q4(X,X)=btrue. % 1.92/2.63 0 [] e_q5(X,X)=btrue. % 1.92/2.63 0 [] e_q4(X,Z)!=bfalse|e_q(cons(X,Y),cons(Z,X2))=bfalse. % 1.92/2.63 0 [] e_q4(X,Z)!=btrue|e_q(cons(X,Y),cons(Z,X2))=e_q(Y,X2). % 1.92/2.63 0 [] e_q(nil,cons(X,Y))=bfalse. % 1.92/2.63 0 [] e_q(cons(X,Y),nil)=bfalse. % 1.92/2.63 0 [] e_q5(prop3(X),bfalse)!=btrue. % 1.92/2.63 end_of_list. % 1.92/2.63 % 1.92/2.63 SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=2. % 1.92/2.63 % 1.92/2.63 This is a Horn set with equality. The strategy will be % 1.92/2.63 Knuth-Bendix and hyper_res, with positive clauses in % 1.92/2.63 sos and nonpositive clauses in usable. % 1.92/2.63 % 1.92/2.63 dependent: set(knuth_bendix). % 1.92/2.63 dependent: set(anl_eq). % 1.92/2.63 dependent: set(para_from). % 1.92/2.63 dependent: set(para_into). % 1.92/2.63 dependent: clear(para_from_right). % 1.92/2.63 dependent: clear(para_into_right). % 1.92/2.63 dependent: set(para_from_vars). % 1.92/2.63 dependent: set(eq_units_both_ways). % 1.92/2.63 dependent: set(dynamic_demod_all). % 1.92/2.63 dependent: set(dynamic_demod). % 1.92/2.63 dependent: set(order_eq). % 1.92/2.63 dependent: set(back_demod). % 1.92/2.63 dependent: set(lrpo). % 1.92/2.63 dependent: set(hyper_res). % 1.92/2.63 dependent: clear(order_hyper). % 1.92/2.63 % 1.92/2.63 ------------> process usable: % 1.92/2.63 ** KEPT (pick-wt=14): 1 [] e_q3(A,B)!=bfalse|e_q3(add(A,C),add(B,D))=bfalse. % 1.92/2.63 ** KEPT (pick-wt=16): 2 [] e_q3(A,B)!=btrue|e_q3(add(A,C),add(B,D))=e_q3(C,D). % 1.92/2.63 ** KEPT (pick-wt=14): 3 [] e_q3(A,B)!=bfalse|e_q3(mul(A,C),mul(B,D))=bfalse. % 1.92/2.63 ** KEPT (pick-wt=16): 4 [] e_q3(A,B)!=btrue|e_q3(mul(A,C),mul(B,D))=e_q3(C,D). % 1.92/2.63 ** KEPT (pick-wt=14): 5 [] e_q4(A,B)!=bfalse|e_q(cons(A,C),cons(B,D))=bfalse. % 1.92/2.63 ** KEPT (pick-wt=16): 6 [] e_q4(A,B)!=btrue|e_q(cons(A,C),cons(B,D))=e_q(C,D). % 1.92/2.63 ** KEPT (pick-wt=6): 7 [] e_q5(prop3(A),bfalse)!=btrue. % 1.92/2.63 % 1.92/2.63 ------------> process sos: % 1.92/2.63 ** KEPT (pick-wt=3): 8 [] A=A. % 1.92/2.63 ** KEPT (pick-wt=10): 9 [] aux(A,pair2(B,C))=pair2(B,s(C)). % 1.92/2.63 ** KEPT (pick-wt=8): 10 [] aux2(A,left(B))=pair2(B,z). % 1.92/2.63 ---> New Demodulator: 11 [new_demod,10] aux2(A,left(B))=pair2(B,z). % 1.92/2.63 ** KEPT (pick-wt=9): 12 [] aux2(A,right(B))=aux(B,mod10(B)). % 1.92/2.63 ---> New Demodulator: 13 [new_demod,12] aux2(A,right(B))=aux(B,mod10(B)). % 1.92/2.63 ** KEPT (pick-wt=12): 14 [] aux3(A,B,pair2(C,D))=showNumnum(cons(C,A),D). % 1.92/2.63 ** KEPT (pick-wt=5): 15 [] impl(btrue,A)=A. % 1.92/2.63 ---> New Demodulator: 16 [new_demod,15] impl(btrue,A)=A. % 1.92/2.63 ** KEPT (pick-wt=5): 17 [] impl(bfalse,A)=btrue. % 1.92/2.63 ---> New Demodulator: 18 [new_demod,17] impl(bfalse,A)=btrue. % 1.92/2.63 ** KEPT (pick-wt=5): 19 [] append(nil,A)=A. % 1.92/2.63 ---> New Demodulator: 20 [new_demod,19] append(nil,A)=A. % 1.92/2.63 ** KEPT (pick-wt=11): 22 [copy,21,flip.1] cons(A,append(B,C))=append(cons(A,B),C). % 1.92/2.63 ---> New Demodulator: 23 [new_demod,22] cons(A,append(B,C))=append(cons(A,B),C). % 1.92/2.63 ** KEPT (pick-wt=5): 24 [] x2(z,z)=z. % 1.92/2.63 ---> New Demodulator: 25 [new_demod,24] x2(z,z)=z. % 1.92/2.63 ** KEPT (pick-wt=6): 26 [] x2(z,s(A))=z. % 1.92/2.63 ---> New Demodulator: 27 [new_demod,26] x2(z,s(A))=z. % 1.92/2.63 ** KEPT (pick-wt=7): 28 [] x2(s(A),z)=s(A). % 1.92/2.63 ---> New Demodulator: 29 [new_demod,28] x2(s(A),z)=s(A). % 1.92/2.63 ** KEPT (pick-wt=9): 30 [] x2(s(A),s(B))=x2(A,B). % 1.92/2.63 ---> New Demodulator: 31 [new_demod,30] x2(s(A),s(B))=x2(A,B). % 1.92/2.63 ** KEPT (pick-wt=5): 32 [] min10(z)=left(dIG0). % 1.92/2.63 ---> New Demodulator: 33 [new_demod,32] min10(z)=left(dIG0). % 1.92/2.63 ** KEPT (pick-wt=6): 34 [] min10(s(z))=left(dIG1). % 1.92/2.63 ---> New Demodulator: 35 [new_demod,34] min10(s(z))=left(dIG1). % 1.92/2.63 ** KEPT (pick-wt=7): 36 [] min10(s(s(z)))=left(dIG2). % 1.92/2.63 ---> New Demodulator: 37 [new_demod,36] min10(s(s(z)))=left(dIG2). % 1.92/2.63 ** KEPT (pick-wt=8): 38 [] min10(s(s(s(z))))=left(dIG3). % 1.92/2.63 ---> New Demodulator: 39 [new_demod,38] min10(s(s(s(z))))=left(dIG3). % 1.92/2.63 ** KEPT (pick-wt=9): 40 [] min10(s(s(s(s(z)))))=left(dIG4). % 1.92/2.63 ---> New Demodulator: 41 [new_demod,40] min10(s(s(s(s(z)))))=left(dIG4). % 1.92/2.63 ** KEPT (pick-wt=10): 42 [] min10(s(s(s(s(s(z))))))=left(dIG5). % 1.92/2.63 ---> New Demodulator: 43 [new_demod,42] min10(s(s(s(s(s(z))))))=left(dIG5). % 1.92/2.63 ** KEPT (pick-wt=11): 44 [] min10(s(s(s(s(s(s(z)))))))=left(dIG6). % 1.92/2.63 ---> New Demodulator: 45 [new_demod,44] min10(s(s(s(s(s(s(z)))))))=left(dIG6). % 1.92/2.63 ** KEPT (pick-wt=12): 46 [] min10(s(s(s(s(s(s(s(z))))))))=left(dIG7). % 1.92/2.63 ---> New Demodulator: 47 [new_demod,46] min10(s(s(s(s(s(s(s(z))))))))=left(dIG7). % 1.92/2.63 ** KEPT (pick-wt=13): 48 [] min10(s(s(s(s(s(s(s(s(z)))))))))=left(dIG8). % 1.92/2.63 ---> New Demodulator: 49 [new_demod,48] min10(s(s(s(s(s(s(s(s(z)))))))))=left(dIG8). % 1.92/2.63 ** KEPT (pick-wt=14): 50 [] min10(s(s(s(s(s(s(s(s(s(z))))))))))=left(dIG9). % 1.92/2.63 ---> New Demodulator: 51 [new_demod,50] min10(s(s(s(s(s(s(s(s(s(z))))))))))=left(dIG9). % 1.92/2.63 ** KEPT (pick-wt=17): 53 [copy,52,demod,31,31,31,31,31,31,31,31,31,31] min10(s(s(s(s(s(s(s(s(s(s(A)))))))))))=right(x2(A,z)). % 1.92/2.63 ---> New Demodulator: 54 [new_demod,53] min10(s(s(s(s(s(s(s(s(s(s(A)))))))))))=right(x2(A,z)). % 1.92/2.63 ** KEPT (pick-wt=7): 55 [] mod10(A)=aux2(A,min10(A)). % 1.92/2.63 ---> New Demodulator: 56 [new_demod,55] mod10(A)=aux2(A,min10(A)). % 1.92/2.63 ** KEPT (pick-wt=5): 57 [] showNumnum(A,z)=A. % 1.92/2.63 ---> New Demodulator: 58 [new_demod,57] showNumnum(A,z)=A. % 1.92/2.63 ** KEPT (pick-wt=14): 60 [copy,59,demod,56] showNumnum(A,s(B))=aux3(A,B,aux2(s(B),min10(s(B)))). % 1.92/2.63 ** KEPT (pick-wt=6): 61 [] showNum(z)=cons(dIG0,nil). % 1.92/2.63 ---> New Demodulator: 62 [new_demod,61] showNum(z)=cons(dIG0,nil). % 1.92/2.63 ** KEPT (pick-wt=8): 63 [] showNum(s(A))=showNumnum(nil,s(A)). % 1.92/2.63 ---> New Demodulator: 64 [new_demod,63] showNum(s(A))=showNumnum(nil,s(A)). % 1.92/2.63 ** KEPT (pick-wt=6): 65 [] show(x)=cons(cHARX,nil). % 1.92/2.63 ---> New Demodulator: 66 [new_demod,65] show(x)=cons(cHARX,nil). % 1.92/2.63 ** KEPT (pick-wt=14): 67 [] show(add(A,B))=append(show(A),append(cons(pLUS,nil),show(B))). % 1.92/2.63 ---> New Demodulator: 68 [new_demod,67] show(add(A,B))=append(show(A),append(cons(pLUS,nil),show(B))). % 1.92/2.63 ** KEPT (pick-wt=14): 69 [] show(mul(A,B))=append(showF(A),append(cons(mULT,nil),showF(B))). % 1.92/2.63 ** KEPT (pick-wt=6): 71 [copy,70,flip.1] showNum(A)=show(num(A)). % 1.92/2.63 ---> New Demodulator: 72 [new_demod,71] showNum(A)=show(num(A)). % 1.92/2.63 ** KEPT (pick-wt=20): 74 [copy,73,demod,68,23,23] showF(add(A,B))=append(append(cons(pAR1,show(A)),append(cons(pLUS,nil),show(B))),cons(pAR2,nil)). % 1.92/2.63 ---> New Demodulator: 75 [new_demod,74] showF(add(A,B))=append(append(cons(pAR1,show(A)),append(cons(pLUS,nil),show(B))),cons(pAR2,nil)). % 1.92/2.63 ** KEPT (pick-wt=6): 77 [copy,76,demod,66] showF(x)=cons(cHARX,nil). % 1.92/2.63 ---> New Demodulator: 78 [new_demod,77] showF(x)=cons(cHARX,nil). % 1.92/2.63 ** KEPT (pick-wt=9): 79 [] showF(mul(A,B))=show(mul(A,B)). % 1.92/2.63 ---> New Demodulator: 80 [new_demod,79] showF(mul(A,B))=show(mul(A,B)). % 1.92/2.63 ** KEPT (pick-wt=7): 81 [] showF(num(A))=show(num(A)). % 1.92/2.63 ---> New Demodulator: 82 [new_demod,81] showF(num(A))=show(num(A)). % 1.92/2.63 ** KEPT (pick-wt=33): 84 [copy,83,flip.1] impl(e_q(show(A),cons(pAR1,cons(pAR1,cons(cHARX,cons(pLUS,cons(dIG5,cons(pAR2,cons(pLUS,cons(dIG7,cons(pAR2,cons(mULT,cons(cHARX,nil)))))))))))),e_q5(btrue,bfalse))=prop3(A). % 1.92/2.63 ---> New Demodulator: 85 [new_demod,84] impl(e_q(show(A),cons(pAR1,cons(pAR1,cons(cHARX,cons(pLUS,cons(dIG5,cons(pAR2,cons(pLUS,cons(dIG7,cons(pAR2,cons(mULT,cons(cHARX,nil)))))))))))),e_q5(btrue,bfalse))=prop3(A). % 1.92/2.63 ** KEPT (pick-wt=5): 86 [] e_q4(pAR1,pAR2)=bfalse. % 1.92/2.63 ---> New Demodulator: 87 [new_demod,86] e_q4(pAR1,pAR2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 88 [] e_q4(pAR1,pLUS)=bfalse. % 1.92/2.63 ---> New Demodulator: 89 [new_demod,88] e_q4(pAR1,pLUS)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 90 [] e_q4(pAR1,mULT)=bfalse. % 1.92/2.63 ---> New Demodulator: 91 [new_demod,90] e_q4(pAR1,mULT)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 92 [] e_q4(pAR1,cHARX)=bfalse. % 1.92/2.63 ---> New Demodulator: 93 [new_demod,92] e_q4(pAR1,cHARX)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 94 [] e_q4(pAR1,dIG0)=bfalse. % 1.92/2.63 ---> New Demodulator: 95 [new_demod,94] e_q4(pAR1,dIG0)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 96 [] e_q4(pAR1,dIG1)=bfalse. % 1.92/2.63 ---> New Demodulator: 97 [new_demod,96] e_q4(pAR1,dIG1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 98 [] e_q4(pAR1,dIG2)=bfalse. % 1.92/2.63 ---> New Demodulator: 99 [new_demod,98] e_q4(pAR1,dIG2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 100 [] e_q4(pAR1,dIG3)=bfalse. % 1.92/2.63 ---> New Demodulator: 101 [new_demod,100] e_q4(pAR1,dIG3)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 102 [] e_q4(pAR1,dIG4)=bfalse. % 1.92/2.63 ---> New Demodulator: 103 [new_demod,102] e_q4(pAR1,dIG4)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 104 [] e_q4(pAR1,dIG5)=bfalse. % 1.92/2.63 ---> New Demodulator: 105 [new_demod,104] e_q4(pAR1,dIG5)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 106 [] e_q4(pAR1,dIG6)=bfalse. % 1.92/2.63 ---> New Demodulator: 107 [new_demod,106] e_q4(pAR1,dIG6)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 108 [] e_q4(pAR1,dIG7)=bfalse. % 1.92/2.63 ---> New Demodulator: 109 [new_demod,108] e_q4(pAR1,dIG7)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 110 [] e_q4(pAR1,dIG8)=bfalse. % 1.92/2.63 ---> New Demodulator: 111 [new_demod,110] e_q4(pAR1,dIG8)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 112 [] e_q4(pAR1,dIG9)=bfalse. % 1.92/2.63 ---> New Demodulator: 113 [new_demod,112] e_q4(pAR1,dIG9)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 114 [] e_q4(pAR2,pAR1)=bfalse. % 1.92/2.63 ---> New Demodulator: 115 [new_demod,114] e_q4(pAR2,pAR1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 116 [] e_q4(pAR2,pLUS)=bfalse. % 1.92/2.63 ---> New Demodulator: 117 [new_demod,116] e_q4(pAR2,pLUS)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 118 [] e_q4(pAR2,mULT)=bfalse. % 1.92/2.63 ---> New Demodulator: 119 [new_demod,118] e_q4(pAR2,mULT)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 120 [] e_q4(pAR2,cHARX)=bfalse. % 1.92/2.63 ---> New Demodulator: 121 [new_demod,120] e_q4(pAR2,cHARX)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 122 [] e_q4(pAR2,dIG0)=bfalse. % 1.92/2.63 ---> New Demodulator: 123 [new_demod,122] e_q4(pAR2,dIG0)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 124 [] e_q4(pAR2,dIG1)=bfalse. % 1.92/2.63 ---> New Demodulator: 125 [new_demod,124] e_q4(pAR2,dIG1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 126 [] e_q4(pAR2,dIG2)=bfalse. % 1.92/2.63 ---> New Demodulator: 127 [new_demod,126] e_q4(pAR2,dIG2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 128 [] e_q4(pAR2,dIG3)=bfalse. % 1.92/2.63 ---> New Demodulator: 129 [new_demod,128] e_q4(pAR2,dIG3)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 130 [] e_q4(pAR2,dIG4)=bfalse. % 1.92/2.63 ---> New Demodulator: 131 [new_demod,130] e_q4(pAR2,dIG4)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 132 [] e_q4(pAR2,dIG5)=bfalse. % 1.92/2.63 ---> New Demodulator: 133 [new_demod,132] e_q4(pAR2,dIG5)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 134 [] e_q4(pAR2,dIG6)=bfalse. % 1.92/2.63 ---> New Demodulator: 135 [new_demod,134] e_q4(pAR2,dIG6)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 136 [] e_q4(pAR2,dIG7)=bfalse. % 1.92/2.63 ---> New Demodulator: 137 [new_demod,136] e_q4(pAR2,dIG7)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 138 [] e_q4(pAR2,dIG8)=bfalse. % 1.92/2.63 ---> New Demodulator: 139 [new_demod,138] e_q4(pAR2,dIG8)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 140 [] e_q4(pAR2,dIG9)=bfalse. % 1.92/2.63 ---> New Demodulator: 141 [new_demod,140] e_q4(pAR2,dIG9)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 142 [] e_q4(pLUS,pAR1)=bfalse. % 1.92/2.63 ---> New Demodulator: 143 [new_demod,142] e_q4(pLUS,pAR1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 144 [] e_q4(pLUS,pAR2)=bfalse. % 1.92/2.63 ---> New Demodulator: 145 [new_demod,144] e_q4(pLUS,pAR2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 146 [] e_q4(pLUS,mULT)=bfalse. % 1.92/2.63 ---> New Demodulator: 147 [new_demod,146] e_q4(pLUS,mULT)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 148 [] e_q4(pLUS,cHARX)=bfalse. % 1.92/2.63 ---> New Demodulator: 149 [new_demod,148] e_q4(pLUS,cHARX)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 150 [] e_q4(pLUS,dIG0)=bfalse. % 1.92/2.63 ---> New Demodulator: 151 [new_demod,150] e_q4(pLUS,dIG0)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 152 [] e_q4(pLUS,dIG1)=bfalse. % 1.92/2.63 ---> New Demodulator: 153 [new_demod,152] e_q4(pLUS,dIG1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 154 [] e_q4(pLUS,dIG2)=bfalse. % 1.92/2.63 ---> New Demodulator: 155 [new_demod,154] e_q4(pLUS,dIG2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 156 [] e_q4(pLUS,dIG3)=bfalse. % 1.92/2.63 ---> New Demodulator: 157 [new_demod,156] e_q4(pLUS,dIG3)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 158 [] e_q4(pLUS,dIG4)=bfalse. % 1.92/2.63 ---> New Demodulator: 159 [new_demod,158] e_q4(pLUS,dIG4)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 160 [] e_q4(pLUS,dIG5)=bfalse. % 1.92/2.63 ---> New Demodulator: 161 [new_demod,160] e_q4(pLUS,dIG5)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 162 [] e_q4(pLUS,dIG6)=bfalse. % 1.92/2.63 ---> New Demodulator: 163 [new_demod,162] e_q4(pLUS,dIG6)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 164 [] e_q4(pLUS,dIG7)=bfalse. % 1.92/2.63 ---> New Demodulator: 165 [new_demod,164] e_q4(pLUS,dIG7)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 166 [] e_q4(pLUS,dIG8)=bfalse. % 1.92/2.63 ---> New Demodulator: 167 [new_demod,166] e_q4(pLUS,dIG8)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 168 [] e_q4(pLUS,dIG9)=bfalse. % 1.92/2.63 ---> New Demodulator: 169 [new_demod,168] e_q4(pLUS,dIG9)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 170 [] e_q4(mULT,pAR1)=bfalse. % 1.92/2.63 ---> New Demodulator: 171 [new_demod,170] e_q4(mULT,pAR1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 172 [] e_q4(mULT,pAR2)=bfalse. % 1.92/2.63 ---> New Demodulator: 173 [new_demod,172] e_q4(mULT,pAR2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 174 [] e_q4(mULT,pLUS)=bfalse. % 1.92/2.63 ---> New Demodulator: 175 [new_demod,174] e_q4(mULT,pLUS)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 176 [] e_q4(mULT,cHARX)=bfalse. % 1.92/2.63 ---> New Demodulator: 177 [new_demod,176] e_q4(mULT,cHARX)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 178 [] e_q4(mULT,dIG0)=bfalse. % 1.92/2.63 ---> New Demodulator: 179 [new_demod,178] e_q4(mULT,dIG0)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 180 [] e_q4(mULT,dIG1)=bfalse. % 1.92/2.63 ---> New Demodulator: 181 [new_demod,180] e_q4(mULT,dIG1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 182 [] e_q4(mULT,dIG2)=bfalse. % 1.92/2.63 ---> New Demodulator: 183 [new_demod,182] e_q4(mULT,dIG2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 184 [] e_q4(mULT,dIG3)=bfalse. % 1.92/2.63 ---> New Demodulator: 185 [new_demod,184] e_q4(mULT,dIG3)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 186 [] e_q4(mULT,dIG4)=bfalse. % 1.92/2.63 ---> New Demodulator: 187 [new_demod,186] e_q4(mULT,dIG4)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 188 [] e_q4(mULT,dIG5)=bfalse. % 1.92/2.63 ---> New Demodulator: 189 [new_demod,188] e_q4(mULT,dIG5)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 190 [] e_q4(mULT,dIG6)=bfalse. % 1.92/2.63 ---> New Demodulator: 191 [new_demod,190] e_q4(mULT,dIG6)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 192 [] e_q4(mULT,dIG7)=bfalse. % 1.92/2.63 ---> New Demodulator: 193 [new_demod,192] e_q4(mULT,dIG7)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 194 [] e_q4(mULT,dIG8)=bfalse. % 1.92/2.63 ---> New Demodulator: 195 [new_demod,194] e_q4(mULT,dIG8)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 196 [] e_q4(mULT,dIG9)=bfalse. % 1.92/2.63 ---> New Demodulator: 197 [new_demod,196] e_q4(mULT,dIG9)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 198 [] e_q4(cHARX,pAR1)=bfalse. % 1.92/2.63 ---> New Demodulator: 199 [new_demod,198] e_q4(cHARX,pAR1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 200 [] e_q4(cHARX,pAR2)=bfalse. % 1.92/2.63 ---> New Demodulator: 201 [new_demod,200] e_q4(cHARX,pAR2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 202 [] e_q4(cHARX,pLUS)=bfalse. % 1.92/2.63 ---> New Demodulator: 203 [new_demod,202] e_q4(cHARX,pLUS)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 204 [] e_q4(cHARX,mULT)=bfalse. % 1.92/2.63 ---> New Demodulator: 205 [new_demod,204] e_q4(cHARX,mULT)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 206 [] e_q4(cHARX,dIG0)=bfalse. % 1.92/2.63 ---> New Demodulator: 207 [new_demod,206] e_q4(cHARX,dIG0)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 208 [] e_q4(cHARX,dIG1)=bfalse. % 1.92/2.63 ---> New Demodulator: 209 [new_demod,208] e_q4(cHARX,dIG1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 210 [] e_q4(cHARX,dIG2)=bfalse. % 1.92/2.63 ---> New Demodulator: 211 [new_demod,210] e_q4(cHARX,dIG2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 212 [] e_q4(cHARX,dIG3)=bfalse. % 1.92/2.63 ---> New Demodulator: 213 [new_demod,212] e_q4(cHARX,dIG3)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 214 [] e_q4(cHARX,dIG4)=bfalse. % 1.92/2.63 ---> New Demodulator: 215 [new_demod,214] e_q4(cHARX,dIG4)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 216 [] e_q4(cHARX,dIG5)=bfalse. % 1.92/2.63 ---> New Demodulator: 217 [new_demod,216] e_q4(cHARX,dIG5)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 218 [] e_q4(cHARX,dIG6)=bfalse. % 1.92/2.63 ---> New Demodulator: 219 [new_demod,218] e_q4(cHARX,dIG6)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 220 [] e_q4(cHARX,dIG7)=bfalse. % 1.92/2.63 ---> New Demodulator: 221 [new_demod,220] e_q4(cHARX,dIG7)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 222 [] e_q4(cHARX,dIG8)=bfalse. % 1.92/2.63 ---> New Demodulator: 223 [new_demod,222] e_q4(cHARX,dIG8)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 224 [] e_q4(cHARX,dIG9)=bfalse. % 1.92/2.63 ---> New Demodulator: 225 [new_demod,224] e_q4(cHARX,dIG9)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 226 [] e_q4(dIG0,pAR1)=bfalse. % 1.92/2.63 ---> New Demodulator: 227 [new_demod,226] e_q4(dIG0,pAR1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 228 [] e_q4(dIG0,pAR2)=bfalse. % 1.92/2.63 ---> New Demodulator: 229 [new_demod,228] e_q4(dIG0,pAR2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 230 [] e_q4(dIG0,pLUS)=bfalse. % 1.92/2.63 ---> New Demodulator: 231 [new_demod,230] e_q4(dIG0,pLUS)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 232 [] e_q4(dIG0,mULT)=bfalse. % 1.92/2.63 ---> New Demodulator: 233 [new_demod,232] e_q4(dIG0,mULT)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 234 [] e_q4(dIG0,cHARX)=bfalse. % 1.92/2.63 ---> New Demodulator: 235 [new_demod,234] e_q4(dIG0,cHARX)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 236 [] e_q4(dIG0,dIG1)=bfalse. % 1.92/2.63 ---> New Demodulator: 237 [new_demod,236] e_q4(dIG0,dIG1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 238 [] e_q4(dIG0,dIG2)=bfalse. % 1.92/2.63 ---> New Demodulator: 239 [new_demod,238] e_q4(dIG0,dIG2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 240 [] e_q4(dIG0,dIG3)=bfalse. % 1.92/2.63 ---> New Demodulator: 241 [new_demod,240] e_q4(dIG0,dIG3)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 242 [] e_q4(dIG0,dIG4)=bfalse. % 1.92/2.63 ---> New Demodulator: 243 [new_demod,242] e_q4(dIG0,dIG4)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 244 [] e_q4(dIG0,dIG5)=bfalse. % 1.92/2.63 ---> New Demodulator: 245 [new_demod,244] e_q4(dIG0,dIG5)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 246 [] e_q4(dIG0,dIG6)=bfalse. % 1.92/2.63 ---> New Demodulator: 247 [new_demod,246] e_q4(dIG0,dIG6)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 248 [] e_q4(dIG0,dIG7)=bfalse. % 1.92/2.63 ---> New Demodulator: 249 [new_demod,248] e_q4(dIG0,dIG7)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 250 [] e_q4(dIG0,dIG8)=bfalse. % 1.92/2.63 ---> New Demodulator: 251 [new_demod,250] e_q4(dIG0,dIG8)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 252 [] e_q4(dIG0,dIG9)=bfalse. % 1.92/2.63 ---> New Demodulator: 253 [new_demod,252] e_q4(dIG0,dIG9)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 254 [] e_q4(dIG1,pAR1)=bfalse. % 1.92/2.63 ---> New Demodulator: 255 [new_demod,254] e_q4(dIG1,pAR1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 256 [] e_q4(dIG1,pAR2)=bfalse. % 1.92/2.63 ---> New Demodulator: 257 [new_demod,256] e_q4(dIG1,pAR2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 258 [] e_q4(dIG1,pLUS)=bfalse. % 1.92/2.63 ---> New Demodulator: 259 [new_demod,258] e_q4(dIG1,pLUS)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 260 [] e_q4(dIG1,mULT)=bfalse. % 1.92/2.63 ---> New Demodulator: 261 [new_demod,260] e_q4(dIG1,mULT)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 262 [] e_q4(dIG1,cHARX)=bfalse. % 1.92/2.63 ---> New Demodulator: 263 [new_demod,262] e_q4(dIG1,cHARX)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 264 [] e_q4(dIG1,dIG0)=bfalse. % 1.92/2.63 ---> New Demodulator: 265 [new_demod,264] e_q4(dIG1,dIG0)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 266 [] e_q4(dIG1,dIG2)=bfalse. % 1.92/2.63 ---> New Demodulator: 267 [new_demod,266] e_q4(dIG1,dIG2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 268 [] e_q4(dIG1,dIG3)=bfalse. % 1.92/2.63 ---> New Demodulator: 269 [new_demod,268] e_q4(dIG1,dIG3)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 270 [] e_q4(dIG1,dIG4)=bfalse. % 1.92/2.63 ---> New Demodulator: 271 [new_demod,270] e_q4(dIG1,dIG4)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 272 [] e_q4(dIG1,dIG5)=bfalse. % 1.92/2.63 ---> New Demodulator: 273 [new_demod,272] e_q4(dIG1,dIG5)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 274 [] e_q4(dIG1,dIG6)=bfalse. % 1.92/2.63 ---> New Demodulator: 275 [new_demod,274] e_q4(dIG1,dIG6)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 276 [] e_q4(dIG1,dIG7)=bfalse. % 1.92/2.63 ---> New Demodulator: 277 [new_demod,276] e_q4(dIG1,dIG7)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 278 [] e_q4(dIG1,dIG8)=bfalse. % 1.92/2.63 ---> New Demodulator: 279 [new_demod,278] e_q4(dIG1,dIG8)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 280 [] e_q4(dIG1,dIG9)=bfalse. % 1.92/2.63 ---> New Demodulator: 281 [new_demod,280] e_q4(dIG1,dIG9)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 282 [] e_q4(dIG2,pAR1)=bfalse. % 1.92/2.63 ---> New Demodulator: 283 [new_demod,282] e_q4(dIG2,pAR1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 284 [] e_q4(dIG2,pAR2)=bfalse. % 1.92/2.63 ---> New Demodulator: 285 [new_demod,284] e_q4(dIG2,pAR2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 286 [] e_q4(dIG2,pLUS)=bfalse. % 1.92/2.63 ---> New Demodulator: 287 [new_demod,286] e_q4(dIG2,pLUS)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 288 [] e_q4(dIG2,mULT)=bfalse. % 1.92/2.63 ---> New Demodulator: 289 [new_demod,288] e_q4(dIG2,mULT)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 290 [] e_q4(dIG2,cHARX)=bfalse. % 1.92/2.63 ---> New Demodulator: 291 [new_demod,290] e_q4(dIG2,cHARX)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 292 [] e_q4(dIG2,dIG0)=bfalse. % 1.92/2.63 ---> New Demodulator: 293 [new_demod,292] e_q4(dIG2,dIG0)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 294 [] e_q4(dIG2,dIG1)=bfalse. % 1.92/2.63 ---> New Demodulator: 295 [new_demod,294] e_q4(dIG2,dIG1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 296 [] e_q4(dIG2,dIG3)=bfalse. % 1.92/2.63 ---> New Demodulator: 297 [new_demod,296] e_q4(dIG2,dIG3)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 298 [] e_q4(dIG2,dIG4)=bfalse. % 1.92/2.63 ---> New Demodulator: 299 [new_demod,298] e_q4(dIG2,dIG4)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 300 [] e_q4(dIG2,dIG5)=bfalse. % 1.92/2.63 ---> New Demodulator: 301 [new_demod,300] e_q4(dIG2,dIG5)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 302 [] e_q4(dIG2,dIG6)=bfalse. % 1.92/2.63 ---> New Demodulator: 303 [new_demod,302] e_q4(dIG2,dIG6)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 304 [] e_q4(dIG2,dIG7)=bfalse. % 1.92/2.63 ---> New Demodulator: 305 [new_demod,304] e_q4(dIG2,dIG7)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 306 [] e_q4(dIG2,dIG8)=bfalse. % 1.92/2.63 ---> New Demodulator: 307 [new_demod,306] e_q4(dIG2,dIG8)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 308 [] e_q4(dIG2,dIG9)=bfalse. % 1.92/2.63 ---> New Demodulator: 309 [new_demod,308] e_q4(dIG2,dIG9)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 310 [] e_q4(dIG3,pAR1)=bfalse. % 1.92/2.63 ---> New Demodulator: 311 [new_demod,310] e_q4(dIG3,pAR1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 312 [] e_q4(dIG3,pAR2)=bfalse. % 1.92/2.63 ---> New Demodulator: 313 [new_demod,312] e_q4(dIG3,pAR2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 314 [] e_q4(dIG3,pLUS)=bfalse. % 1.92/2.63 ---> New Demodulator: 315 [new_demod,314] e_q4(dIG3,pLUS)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 316 [] e_q4(dIG3,mULT)=bfalse. % 1.92/2.63 ---> New Demodulator: 317 [new_demod,316] e_q4(dIG3,mULT)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 318 [] e_q4(dIG3,cHARX)=bfalse. % 1.92/2.63 ---> New Demodulator: 319 [new_demod,318] e_q4(dIG3,cHARX)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 320 [] e_q4(dIG3,dIG0)=bfalse. % 1.92/2.63 ---> New Demodulator: 321 [new_demod,320] e_q4(dIG3,dIG0)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 322 [] e_q4(dIG3,dIG1)=bfalse. % 1.92/2.63 ---> New Demodulator: 323 [new_demod,322] e_q4(dIG3,dIG1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 324 [] e_q4(dIG3,dIG2)=bfalse. % 1.92/2.63 ---> New Demodulator: 325 [new_demod,324] e_q4(dIG3,dIG2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 326 [] e_q4(dIG3,dIG4)=bfalse. % 1.92/2.63 ---> New Demodulator: 327 [new_demod,326] e_q4(dIG3,dIG4)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 328 [] e_q4(dIG3,dIG5)=bfalse. % 1.92/2.63 ---> New Demodulator: 329 [new_demod,328] e_q4(dIG3,dIG5)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 330 [] e_q4(dIG3,dIG6)=bfalse. % 1.92/2.63 ---> New Demodulator: 331 [new_demod,330] e_q4(dIG3,dIG6)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 332 [] e_q4(dIG3,dIG7)=bfalse. % 1.92/2.63 ---> New Demodulator: 333 [new_demod,332] e_q4(dIG3,dIG7)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 334 [] e_q4(dIG3,dIG8)=bfalse. % 1.92/2.63 ---> New Demodulator: 335 [new_demod,334] e_q4(dIG3,dIG8)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 336 [] e_q4(dIG3,dIG9)=bfalse. % 1.92/2.63 ---> New Demodulator: 337 [new_demod,336] e_q4(dIG3,dIG9)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 338 [] e_q4(dIG4,pAR1)=bfalse. % 1.92/2.63 ---> New Demodulator: 339 [new_demod,338] e_q4(dIG4,pAR1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 340 [] e_q4(dIG4,pAR2)=bfalse. % 1.92/2.63 ---> New Demodulator: 341 [new_demod,340] e_q4(dIG4,pAR2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 342 [] e_q4(dIG4,pLUS)=bfalse. % 1.92/2.63 ---> New Demodulator: 343 [new_demod,342] e_q4(dIG4,pLUS)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 344 [] e_q4(dIG4,mULT)=bfalse. % 1.92/2.63 ---> New Demodulator: 345 [new_demod,344] e_q4(dIG4,mULT)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 346 [] e_q4(dIG4,cHARX)=bfalse. % 1.92/2.63 ---> New Demodulator: 347 [new_demod,346] e_q4(dIG4,cHARX)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 348 [] e_q4(dIG4,dIG0)=bfalse. % 1.92/2.63 ---> New Demodulator: 349 [new_demod,348] e_q4(dIG4,dIG0)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 350 [] e_q4(dIG4,dIG1)=bfalse. % 1.92/2.63 ---> New Demodulator: 351 [new_demod,350] e_q4(dIG4,dIG1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 352 [] e_q4(dIG4,dIG2)=bfalse. % 1.92/2.63 ---> New Demodulator: 353 [new_demod,352] e_q4(dIG4,dIG2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 354 [] e_q4(dIG4,dIG3)=bfalse. % 1.92/2.63 ---> New Demodulator: 355 [new_demod,354] e_q4(dIG4,dIG3)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 356 [] e_q4(dIG4,dIG5)=bfalse. % 1.92/2.63 ---> New Demodulator: 357 [new_demod,356] e_q4(dIG4,dIG5)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 358 [] e_q4(dIG4,dIG6)=bfalse. % 1.92/2.63 ---> New Demodulator: 359 [new_demod,358] e_q4(dIG4,dIG6)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 360 [] e_q4(dIG4,dIG7)=bfalse. % 1.92/2.63 ---> New Demodulator: 361 [new_demod,360] e_q4(dIG4,dIG7)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 362 [] e_q4(dIG4,dIG8)=bfalse. % 1.92/2.63 ---> New Demodulator: 363 [new_demod,362] e_q4(dIG4,dIG8)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 364 [] e_q4(dIG4,dIG9)=bfalse. % 1.92/2.63 ---> New Demodulator: 365 [new_demod,364] e_q4(dIG4,dIG9)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 366 [] e_q4(dIG5,pAR1)=bfalse. % 1.92/2.63 ---> New Demodulator: 367 [new_demod,366] e_q4(dIG5,pAR1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 368 [] e_q4(dIG5,pAR2)=bfalse. % 1.92/2.63 ---> New Demodulator: 369 [new_demod,368] e_q4(dIG5,pAR2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 370 [] e_q4(dIG5,pLUS)=bfalse. % 1.92/2.63 ---> New Demodulator: 371 [new_demod,370] e_q4(dIG5,pLUS)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 372 [] e_q4(dIG5,mULT)=bfalse. % 1.92/2.63 ---> New Demodulator: 373 [new_demod,372] e_q4(dIG5,mULT)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 374 [] e_q4(dIG5,cHARX)=bfalse. % 1.92/2.63 ---> New Demodulator: 375 [new_demod,374] e_q4(dIG5,cHARX)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 376 [] e_q4(dIG5,dIG0)=bfalse. % 1.92/2.63 ---> New Demodulator: 377 [new_demod,376] e_q4(dIG5,dIG0)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 378 [] e_q4(dIG5,dIG1)=bfalse. % 1.92/2.63 ---> New Demodulator: 379 [new_demod,378] e_q4(dIG5,dIG1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 380 [] e_q4(dIG5,dIG2)=bfalse. % 1.92/2.63 ---> New Demodulator: 381 [new_demod,380] e_q4(dIG5,dIG2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 382 [] e_q4(dIG5,dIG3)=bfalse. % 1.92/2.63 ---> New Demodulator: 383 [new_demod,382] e_q4(dIG5,dIG3)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 384 [] e_q4(dIG5,dIG4)=bfalse. % 1.92/2.63 ---> New Demodulator: 385 [new_demod,384] e_q4(dIG5,dIG4)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 386 [] e_q4(dIG5,dIG6)=bfalse. % 1.92/2.63 ---> New Demodulator: 387 [new_demod,386] e_q4(dIG5,dIG6)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 388 [] e_q4(dIG5,dIG7)=bfalse. % 1.92/2.63 ---> New Demodulator: 389 [new_demod,388] e_q4(dIG5,dIG7)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 390 [] e_q4(dIG5,dIG8)=bfalse. % 1.92/2.63 ---> New Demodulator: 391 [new_demod,390] e_q4(dIG5,dIG8)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 392 [] e_q4(dIG5,dIG9)=bfalse. % 1.92/2.63 ---> New Demodulator: 393 [new_demod,392] e_q4(dIG5,dIG9)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 394 [] e_q4(dIG6,pAR1)=bfalse. % 1.92/2.63 ---> New Demodulator: 395 [new_demod,394] e_q4(dIG6,pAR1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 396 [] e_q4(dIG6,pAR2)=bfalse. % 1.92/2.63 ---> New Demodulator: 397 [new_demod,396] e_q4(dIG6,pAR2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 398 [] e_q4(dIG6,pLUS)=bfalse. % 1.92/2.63 ---> New Demodulator: 399 [new_demod,398] e_q4(dIG6,pLUS)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 400 [] e_q4(dIG6,mULT)=bfalse. % 1.92/2.63 ---> New Demodulator: 401 [new_demod,400] e_q4(dIG6,mULT)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 402 [] e_q4(dIG6,cHARX)=bfalse. % 1.92/2.63 ---> New Demodulator: 403 [new_demod,402] e_q4(dIG6,cHARX)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 404 [] e_q4(dIG6,dIG0)=bfalse. % 1.92/2.63 ---> New Demodulator: 405 [new_demod,404] e_q4(dIG6,dIG0)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 406 [] e_q4(dIG6,dIG1)=bfalse. % 1.92/2.63 ---> New Demodulator: 407 [new_demod,406] e_q4(dIG6,dIG1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 408 [] e_q4(dIG6,dIG2)=bfalse. % 1.92/2.63 ---> New Demodulator: 409 [new_demod,408] e_q4(dIG6,dIG2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 410 [] e_q4(dIG6,dIG3)=bfalse. % 1.92/2.63 ---> New Demodulator: 411 [new_demod,410] e_q4(dIG6,dIG3)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 412 [] e_q4(dIG6,dIG4)=bfalse. % 1.92/2.63 ---> New Demodulator: 413 [new_demod,412] e_q4(dIG6,dIG4)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 414 [] e_q4(dIG6,dIG5)=bfalse. % 1.92/2.63 ---> New Demodulator: 415 [new_demod,414] e_q4(dIG6,dIG5)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 416 [] e_q4(dIG6,dIG7)=bfalse. % 1.92/2.63 ---> New Demodulator: 417 [new_demod,416] e_q4(dIG6,dIG7)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 418 [] e_q4(dIG6,dIG8)=bfalse. % 1.92/2.63 ---> New Demodulator: 419 [new_demod,418] e_q4(dIG6,dIG8)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 420 [] e_q4(dIG6,dIG9)=bfalse. % 1.92/2.63 ---> New Demodulator: 421 [new_demod,420] e_q4(dIG6,dIG9)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 422 [] e_q4(dIG7,pAR1)=bfalse. % 1.92/2.63 ---> New Demodulator: 423 [new_demod,422] e_q4(dIG7,pAR1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 424 [] e_q4(dIG7,pAR2)=bfalse. % 1.92/2.63 ---> New Demodulator: 425 [new_demod,424] e_q4(dIG7,pAR2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 426 [] e_q4(dIG7,pLUS)=bfalse. % 1.92/2.63 ---> New Demodulator: 427 [new_demod,426] e_q4(dIG7,pLUS)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 428 [] e_q4(dIG7,mULT)=bfalse. % 1.92/2.63 ---> New Demodulator: 429 [new_demod,428] e_q4(dIG7,mULT)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 430 [] e_q4(dIG7,cHARX)=bfalse. % 1.92/2.63 ---> New Demodulator: 431 [new_demod,430] e_q4(dIG7,cHARX)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 432 [] e_q4(dIG7,dIG0)=bfalse. % 1.92/2.63 ---> New Demodulator: 433 [new_demod,432] e_q4(dIG7,dIG0)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 434 [] e_q4(dIG7,dIG1)=bfalse. % 1.92/2.63 ---> New Demodulator: 435 [new_demod,434] e_q4(dIG7,dIG1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 436 [] e_q4(dIG7,dIG2)=bfalse. % 1.92/2.63 ---> New Demodulator: 437 [new_demod,436] e_q4(dIG7,dIG2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 438 [] e_q4(dIG7,dIG3)=bfalse. % 1.92/2.63 ---> New Demodulator: 439 [new_demod,438] e_q4(dIG7,dIG3)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 440 [] e_q4(dIG7,dIG4)=bfalse. % 1.92/2.63 ---> New Demodulator: 441 [new_demod,440] e_q4(dIG7,dIG4)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 442 [] e_q4(dIG7,dIG5)=bfalse. % 1.92/2.63 ---> New Demodulator: 443 [new_demod,442] e_q4(dIG7,dIG5)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 444 [] e_q4(dIG7,dIG6)=bfalse. % 1.92/2.63 ---> New Demodulator: 445 [new_demod,444] e_q4(dIG7,dIG6)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 446 [] e_q4(dIG7,dIG8)=bfalse. % 1.92/2.63 ---> New Demodulator: 447 [new_demod,446] e_q4(dIG7,dIG8)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 448 [] e_q4(dIG7,dIG9)=bfalse. % 1.92/2.63 ---> New Demodulator: 449 [new_demod,448] e_q4(dIG7,dIG9)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 450 [] e_q4(dIG8,pAR1)=bfalse. % 1.92/2.63 ---> New Demodulator: 451 [new_demod,450] e_q4(dIG8,pAR1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 452 [] e_q4(dIG8,pAR2)=bfalse. % 1.92/2.63 ---> New Demodulator: 453 [new_demod,452] e_q4(dIG8,pAR2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 454 [] e_q4(dIG8,pLUS)=bfalse. % 1.92/2.63 ---> New Demodulator: 455 [new_demod,454] e_q4(dIG8,pLUS)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 456 [] e_q4(dIG8,mULT)=bfalse. % 1.92/2.63 ---> New Demodulator: 457 [new_demod,456] e_q4(dIG8,mULT)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 458 [] e_q4(dIG8,cHARX)=bfalse. % 1.92/2.63 ---> New Demodulator: 459 [new_demod,458] e_q4(dIG8,cHARX)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 460 [] e_q4(dIG8,dIG0)=bfalse. % 1.92/2.63 ---> New Demodulator: 461 [new_demod,460] e_q4(dIG8,dIG0)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 462 [] e_q4(dIG8,dIG1)=bfalse. % 1.92/2.63 ---> New Demodulator: 463 [new_demod,462] e_q4(dIG8,dIG1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 464 [] e_q4(dIG8,dIG2)=bfalse. % 1.92/2.63 ---> New Demodulator: 465 [new_demod,464] e_q4(dIG8,dIG2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 466 [] e_q4(dIG8,dIG3)=bfalse. % 1.92/2.63 ---> New Demodulator: 467 [new_demod,466] e_q4(dIG8,dIG3)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 468 [] e_q4(dIG8,dIG4)=bfalse. % 1.92/2.63 ---> New Demodulator: 469 [new_demod,468] e_q4(dIG8,dIG4)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 470 [] e_q4(dIG8,dIG5)=bfalse. % 1.92/2.63 ---> New Demodulator: 471 [new_demod,470] e_q4(dIG8,dIG5)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 472 [] e_q4(dIG8,dIG6)=bfalse. % 1.92/2.63 ---> New Demodulator: 473 [new_demod,472] e_q4(dIG8,dIG6)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 474 [] e_q4(dIG8,dIG7)=bfalse. % 1.92/2.63 ---> New Demodulator: 475 [new_demod,474] e_q4(dIG8,dIG7)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 476 [] e_q4(dIG8,dIG9)=bfalse. % 1.92/2.63 ---> New Demodulator: 477 [new_demod,476] e_q4(dIG8,dIG9)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 478 [] e_q4(dIG9,pAR1)=bfalse. % 1.92/2.63 ---> New Demodulator: 479 [new_demod,478] e_q4(dIG9,pAR1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 480 [] e_q4(dIG9,pAR2)=bfalse. % 1.92/2.63 ---> New Demodulator: 481 [new_demod,480] e_q4(dIG9,pAR2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 482 [] e_q4(dIG9,pLUS)=bfalse. % 1.92/2.63 ---> New Demodulator: 483 [new_demod,482] e_q4(dIG9,pLUS)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 484 [] e_q4(dIG9,mULT)=bfalse. % 1.92/2.63 ---> New Demodulator: 485 [new_demod,484] e_q4(dIG9,mULT)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 486 [] e_q4(dIG9,cHARX)=bfalse. % 1.92/2.63 ---> New Demodulator: 487 [new_demod,486] e_q4(dIG9,cHARX)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 488 [] e_q4(dIG9,dIG0)=bfalse. % 1.92/2.63 ---> New Demodulator: 489 [new_demod,488] e_q4(dIG9,dIG0)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 490 [] e_q4(dIG9,dIG1)=bfalse. % 1.92/2.63 ---> New Demodulator: 491 [new_demod,490] e_q4(dIG9,dIG1)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 492 [] e_q4(dIG9,dIG2)=bfalse. % 1.92/2.63 ---> New Demodulator: 493 [new_demod,492] e_q4(dIG9,dIG2)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 494 [] e_q4(dIG9,dIG3)=bfalse. % 1.92/2.63 ---> New Demodulator: 495 [new_demod,494] e_q4(dIG9,dIG3)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 496 [] e_q4(dIG9,dIG4)=bfalse. % 1.92/2.63 ---> New Demodulator: 497 [new_demod,496] e_q4(dIG9,dIG4)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 498 [] e_q4(dIG9,dIG5)=bfalse. % 1.92/2.63 ---> New Demodulator: 499 [new_demod,498] e_q4(dIG9,dIG5)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 500 [] e_q4(dIG9,dIG6)=bfalse. % 1.92/2.63 ---> New Demodulator: 501 [new_demod,500] e_q4(dIG9,dIG6)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 502 [] e_q4(dIG9,dIG7)=bfalse. % 1.92/2.63 ---> New Demodulator: 503 [new_demod,502] e_q4(dIG9,dIG7)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 504 [] e_q4(dIG9,dIG8)=bfalse. % 1.92/2.63 ---> New Demodulator: 505 [new_demod,504] e_q4(dIG9,dIG8)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 506 [] e_q5(bfalse,btrue)=bfalse. % 1.92/2.63 ---> New Demodulator: 507 [new_demod,506] e_q5(bfalse,btrue)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 508 [] e_q5(btrue,bfalse)=bfalse. % 1.92/2.63 ---> New Demodulator: 509 [new_demod,508] e_q5(btrue,bfalse)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=9): 510 [] e_q3(num(A),num(B))=e_q2(A,B). % 1.92/2.63 ---> New Demodulator: 511 [new_demod,510] e_q3(num(A),num(B))=e_q2(A,B). % 1.92/2.63 ** KEPT (pick-wt=7): 512 [] e_q3(x,add(A,B))=bfalse. % 1.92/2.63 ---> New Demodulator: 513 [new_demod,512] e_q3(x,add(A,B))=bfalse. % 1.92/2.63 ** KEPT (pick-wt=7): 514 [] e_q3(x,mul(A,B))=bfalse. % 1.92/2.63 ---> New Demodulator: 515 [new_demod,514] e_q3(x,mul(A,B))=bfalse. % 1.92/2.63 ** KEPT (pick-wt=6): 516 [] e_q3(x,num(A))=bfalse. % 1.92/2.63 ---> New Demodulator: 517 [new_demod,516] e_q3(x,num(A))=bfalse. % 1.92/2.63 ** KEPT (pick-wt=7): 518 [] e_q3(add(A,B),x)=bfalse. % 1.92/2.63 ---> New Demodulator: 519 [new_demod,518] e_q3(add(A,B),x)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=9): 520 [] e_q3(add(A,B),mul(C,D))=bfalse. % 1.92/2.63 ---> New Demodulator: 521 [new_demod,520] e_q3(add(A,B),mul(C,D))=bfalse. % 1.92/2.63 ** KEPT (pick-wt=8): 522 [] e_q3(add(A,B),num(C))=bfalse. % 1.92/2.63 ---> New Demodulator: 523 [new_demod,522] e_q3(add(A,B),num(C))=bfalse. % 1.92/2.63 ** KEPT (pick-wt=7): 524 [] e_q3(mul(A,B),x)=bfalse. % 1.92/2.63 ---> New Demodulator: 525 [new_demod,524] e_q3(mul(A,B),x)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=9): 526 [] e_q3(mul(A,B),add(C,D))=bfalse. % 1.92/2.63 ---> New Demodulator: 527 [new_demod,526] e_q3(mul(A,B),add(C,D))=bfalse. % 1.92/2.63 ** KEPT (pick-wt=8): 528 [] e_q3(mul(A,B),num(C))=bfalse. % 1.92/2.63 ---> New Demodulator: 529 [new_demod,528] e_q3(mul(A,B),num(C))=bfalse. % 1.92/2.63 ** KEPT (pick-wt=6): 530 [] e_q3(num(A),x)=bfalse. % 1.92/2.63 ---> New Demodulator: 531 [new_demod,530] e_q3(num(A),x)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=8): 532 [] e_q3(num(A),add(B,C))=bfalse. % 1.92/2.63 ---> New Demodulator: 533 [new_demod,532] e_q3(num(A),add(B,C))=bfalse. % 1.92/2.63 ** KEPT (pick-wt=8): 534 [] e_q3(num(A),mul(B,C))=bfalse. % 1.92/2.63 ---> New Demodulator: 535 [new_demod,534] e_q3(num(A),mul(B,C))=bfalse. % 1.92/2.63 ** KEPT (pick-wt=9): 536 [] e_q2(s(A),s(B))=e_q2(A,B). % 1.92/2.63 ---> New Demodulator: 537 [new_demod,536] e_q2(s(A),s(B))=e_q2(A,B). % 1.92/2.63 ** KEPT (pick-wt=6): 538 [] e_q2(z,s(A))=bfalse. % 1.92/2.63 ---> New Demodulator: 539 [new_demod,538] e_q2(z,s(A))=bfalse. % 1.92/2.63 ** KEPT (pick-wt=6): 540 [] e_q2(s(A),z)=bfalse. % 1.92/2.63 ---> New Demodulator: 541 [new_demod,540] e_q2(s(A),z)=bfalse. % 1.92/2.63 ** KEPT (pick-wt=5): 542 [] e_q(A,A)=btrue. % 1.92/2.63 ---> New Demodulator: 543 [new_demod,542] e_q(A,A)=btrue. % 1.92/2.63 ** KEPT (pick-wt=5): 544 [] e_q2(A,A)=btrue. % 1.92/2.63 ---> New Demodulator: 545 [new_demod,544] e_q2(A,A)=btrue. % 1.92/2.63 ** KEPT (pick-wt=5): 546 [] e_q3(A,A)=btrue. % 1.92/2.63 ---> New Demodulator: 547 [new_demod,546] e_q3(A,A)=btrue. % 1.92/2.63 ** KEPT (pick-wt=5): 548 [] e_q4(A,A)=btrue. % 1.92/2.63 ---> New Demodulator: 549 [new_demod,548] e_q4(A,A)=btrue. % 1.92/2.63 ** KEPT (pick-wt=5): 550 [] e_q5(A,A)=btrue. % 1.92/2.63 ---> New Demodulator: 551 [new_demod,550] e_q5(A,A)=btrue. % 1.92/2.63 ** KEPT (pick-wt=7): 552 [] e_q(nil,cons(A,B))=bfalse. % 1.92/2.63 ---> New Demodulator: 553 [new_demod,552] e_q(nil,cons(A,B))=bfalse. % 1.92/2.63 ** KEPT (pick-wt=7): 554 [] e_q(cons(A,B),nil)=bfalse. % 1.92/2.63 ---> New Demodulator: 555 [new_demod,554] e_q(cons(A,B),nil)=bfalse. % 1.92/2.63 Following clause subsumed by 8 during input processing: 0 [copy,8,flip.1] A=A. % 1.92/2.63 ** KEPT (pick-wt=10): 556 [copy,9,flip.1] pair2(A,s(B))=aux(C,pair2(A,B)). % 1.92/2.63 >>>> Starting back demodulation with 11. % 1.92/2.63 >>>> Starting back demodulation with 13. % 1.92/2.63 ** KEPT (pick-wt=12): 557 [copy,14,flip.1] showNumnum(cons(A,B),C)=aux3(B,D,pair2(A,C)). % 1.92/2.63 >>>> Starting back demodulation with 16. % 1.92/2.63 >>>> Starting back demodulation with 18. % 1.92/2.63 >>>> Starting back demodulation with 20. % 1.92/2.63 >>>> Starting back demodulation with 23. % 1.92/2.63 >>>> Starting back demodulation with 25. % 1.92/2.63 >>>> Starting back demodulation with 27. % 1.92/2.63 >>>> Starting back demodulation with 29. % 1.92/2.63 >>>> Starting back demodulation with 31. % 1.92/2.63 >>>> Starting back demodulation with 33. % 1.92/2.63 >>>> Starting back demodulation with 35. % 1.92/2.63 >>>> Starting back demodulation with 37. % 1.92/2.63 >>>> Starting back demodulation with 39. % 1.92/2.63 >>>> Starting back demodulation with 41. % 1.92/2.63 >>>> Starting back demodulation with 43. % 1.92/2.63 >>>> Starting back demodulation with 45. % 1.92/2.63 >>>> Starting back demodulation with 47. % 1.92/2.63 >>>> Starting back demodulation with 49. % 1.92/2.63 >>>> Starting back demodulation with 51. % 1.92/2.63 >>>> Starting back demodulation with 54. % 1.92/2.63 >>>> Starting back demodulation with 56. % 1.92/2.63 >> back demodulating 12 with 56. % 1.92/2.63 >>>> Starting back demodulation with 58. % 1.92/2.63 ** KEPT (pick-wt=14): 560 [copy,60,flip.1] aux3(A,B,aux2(s(B),min10(s(B))))=showNumnum(A,s(B)). % 1.92/2.63 >>>> Starting back demodulation with 62. % 1.92/2.63 >>>> Starting back demodulation with 64. % 1.92/2.63 >>>> Starting back demodulation with 66. % 1.92/2.63 >>>> Starting back demodulation with 68. % 1.92/2.63 ** KEPT (pick-wt=14): 561 [copy,69,flip.1] append(showF(A),append(cons(mULT,nil),showF(B)))=show(mul(A,B)). % 1.92/2.63 >>>> Starting back demodulation with 72. % 1.92/2.63 >> back demodulating 63 with 72. % 1.92/2.63 >> back demodulating 61 with 72. % 1.92/2.63 >>>> Starting back demodulation with 75. % 1.92/2.63 >>>> Starting back demodulation with 78. % 1.92/2.63 >>>> Starting back demodulation with 80. % 1.92/2.63 >>>> Starting back demodulation with 82. % 1.92/2.63 >>>> Starting back demodulation with 85. % 1.92/2.63 >>>> Starting back demodulation with 87. % 1.92/2.63 >>>> Starting back demodulation with 89. % 1.92/2.63 >>>> Starting back demodulation with 91. % 1.92/2.63 >>>> Starting back demodulation with 93. % 1.92/2.63 >>>> Starting back demodulation with 95. % 1.92/2.63 >>>> Starting back demodulation with 97. % 1.92/2.63 >>>> Starting back demodulation with 99. % 1.92/2.63 >>>> Starting back demodulation with 101. % 1.92/2.63 >>>> Starting back demodulation with 103. % 1.92/2.63 >>>> Starting back demodulation with 105. % 1.92/2.63 >>>> Starting back demodulation with 107. % 1.92/2.63 >>>> Starting back demodulation with 109. % 1.92/2.63 >>>> Starting back demodulation with 111. % 1.92/2.63 >>>> Starting back demodulation with 113. % 1.92/2.63 >>>> Starting back demodulation with 115. % 1.92/2.63 >>>> Starting back demodulation with 117. % 1.92/2.63 >>>> Starting back demodulation with 119. % 1.92/2.63 >>>> Starting back demodulation with 121. % 1.92/2.63 >>>> Starting back demodulation with 123. % 1.92/2.63 >>>> Starting back demodulation with 125. % 1.92/2.63 >>>> Starting back demodulation with 127. % 1.92/2.63 >>>> Starting back demodulation with 129. % 1.92/2.63 >>>> Starting back demodulation with 131. % 1.92/2.63 >>>> Starting back demodulation with 133. % 1.92/2.63 >>>> Starting back demodulation with 135. % 1.92/2.63 >>>> Starting back demodulation with 137. % 1.92/2.63 >>>> Starting back demodulation with 139. % 1.92/2.63 >>>> Starting back demodulation with 141. % 1.92/2.63 >>>> Starting back demodulation with 143. % 1.92/2.63 >>>> Starting back demodulation with 145. % 1.92/2.63 >>>> Starting back demodulation with 147. % 1.92/2.63 >>>> Starting back demodulation with 149. % 1.92/2.63 >>>> Starting back demodulation with 151. % 1.92/2.63 >>>> Starting back demodulation with 153. % 1.92/2.63 >>>> Starting back demodulation with 155. % 1.92/2.63 >>>> Starting back demodulation with 157. % 1.92/2.63 >>>> Starting back demodulation with 159. % 1.92/2.63 >>>> Starting back demodulation with 161. % 1.92/2.63 >>>> Starting back demodulation with 163. % 1.92/2.63 >>>> Starting back demodulation with 165. % 1.92/2.63 >>>> Starting back demodulation with 167. % 1.92/2.63 >>>> Starting back demodulation with 169. % 1.92/2.63 >>>> Starting back demodulation with 171. % 1.92/2.63 >>>> Starting back demodulation with 173. % 1.92/2.63 >>>> Starting back demodulation with 175. % 1.92/2.63 >>>> Starting back demodulation with 177. % 1.92/2.63 >>>> Starting back demodulation with 179. % 1.92/2.63 >>>> Starting back demodulation with 181. % 1.92/2.63 >>>> Starting back demodulation with 183. % 1.92/2.63 >>>> Starting back demodulation with 185. % 1.92/2.63 >>>> Starting back demodulation with 187. % 1.92/2.63 >>>> Starting back demodulation with 189. % 1.92/2.63 >>>> Starting back demodulation with 191. % 1.92/2.63 >>>> Starting back demodulation with 193. % 1.92/2.63 >>>> Starting back demodulation with 195. % 1.92/2.63 >>>> Starting back demodulation with 197. % 1.92/2.63 >>>> Starting back demodulation with 199. % 1.92/2.63 >>>> Starting back demodulation with 201. % 1.92/2.63 >>>> Starting back demodulation with 203. % 1.92/2.63 >>>> Starting back demodulation with 205. % 1.92/2.63 >>>> Starting back demodulation with 207. % 1.92/2.63 >>>> Starting back demodulation with 209. % 1.92/2.63 >>>> Starting back demodulation with 211. % 1.92/2.63 >>>> Starting back demodulation with 213. % 1.92/2.63 >>>> Starting back demodulation with 215. % 1.92/2.63 >>>> Starting back demodulation with 217. % 1.92/2.63 >>>> Starting back demodulation with 219. % 1.92/2.63 >>>> Starting back demodulation with 221. % 1.92/2.63 >>>> Starting back demodulation with 223. % 1.92/2.63 >>>> Starting back demodulation with 225. % 1.92/2.63 >>>> Starting back demodulation with 227. % 1.92/2.63 >>>> Starting back demodulation with 229. % 1.92/2.63 >>>> Starting back demodulation with 231. % 1.92/2.63 >>>> Starting back demodulation with 233. % 1.92/2.63 >>>> Starting back demodulation with 235. % 1.92/2.63 >>>> Starting back demodulation with 237. % 1.92/2.63 >>>> Starting back demodulation with 239. % 1.92/2.63 >>>> Starting back demodulation with 241. % 1.92/2.63 >>>> Starting back demodulation with 243. % 1.92/2.63 >>>> Starting back demodulation with 245. % 1.92/2.63 >>>> Starting back demodulation with 247. % 1.92/2.63 >>>> Starting back demodulation with 249. % 1.92/2.63 >>>> Starting back demodulation with 251. % 1.92/2.63 >>>> Starting back demodulation with 253. % 1.92/2.63 >>>> Starting back demodulation with 255. % 1.92/2.63 >>>> Starting back demodulation with 257. % 1.92/2.63 >>>> Starting back demodulation with 259. % 1.92/2.63 >>>> Starting back demodulation with 261. % 1.92/2.63 >>>> Starting back demodulation with 263. % 1.92/2.63 >>>> Starting back demodulation with 265. % 1.92/2.63 >>>> Starting back demodulation with 267. % 1.92/2.63 >>>> Starting back demodulation with 269. % 1.92/2.63 >>>> Starting back demodulation with 271. % 1.92/2.63 >>>> Starting back demodulation with 273. % 1.92/2.63 >>>> Starting back demodulation with 275. % 1.92/2.63 >>>> Starting back demodulation with 277. % 1.92/2.63 >>>> Starting back demodulation with 279. % 1.92/2.63 >>>> Starting back demodulation with 281. % 1.92/2.63 >>>> Starting back demodulation with 283. % 1.92/2.63 >>>> Starting back demodulation with 285. % 1.92/2.63 >>>> Starting back demodulation with 287. % 1.92/2.63 >>>> Starting back demodulation with 289. % 1.92/2.63 >>>> Starting back demodulation with 291. % 1.92/2.63 >>>> Starting back demodulation with 293. % 1.92/2.63 >>>> Starting back demodulation with 295. % 1.92/2.63 >>>> Starting back demodulation with 297. % 1.92/2.63 >>>> Starting back demodulation with 299. % 1.92/2.63 >>>> Starting back demodulation with 301. % 1.92/2.63 >>>> Starting back demodulation with 303. % 1.92/2.63 >>>> Starting back demodulation with 305. % 1.92/2.63 >>>> Starting back demodulation with 307. % 1.92/2.63 >>>> Starting back demodulation with 309. % 1.92/2.63 >>>> Starting back demodulation with 311. % 1.92/2.63 >>>> Starting back demodulation with 313. % 1.92/2.63 >>>> Starting back demodulation with 315. % 1.92/2.63 >>>> Starting back demodulation with 317. % 1.92/2.63 >>>> Starting back demodulation with 319. % 1.92/2.63 >>>> Starting back demodulation with 321. % 1.92/2.63 >>>> Starting back demodulation with 323. % 1.92/2.63 >>>> Starting back demodulation with 325. % 1.92/2.63 >>>> Starting back demodulation with 327. % 1.92/2.63 >>>> Starting back demodulation with 329. % 1.92/2.63 >>>> Starting back demodulation with 331. % 1.92/2.63 >>>> Starting back demodulation with 333. % 1.92/2.63 >>>> Starting back demodulation with 335. % 1.92/2.63 >>>> Starting back demodulation with 337. % 1.92/2.63 >>>> Starting back demodulation with 339. % 1.92/2.63 >>>> Starting back demodulation with 341. % 1.92/2.63 >>>> Starting back demodulation with 343. % 1.92/2.63 >>>> Starting back demodulation with 345. % 1.92/2.63 >>>> Starting back demodulation with 347. % 1.92/2.63 >>>> Starting back demodulation with 349. % 1.92/2.63 >>>> Starting back demodulation with 351. % 1.92/2.63 >>>> Starting back demodulation with 353. % 1.92/2.63 >>>> Starting back demodulation with 355. % 1.92/2.63 >>>> Starting back demodulation with 357. % 1.92/2.63 >>>> Starting back demodulation with 359. % 1.92/2.63 >>>> Starting back demodulation with 361. % 1.92/2.63 >>>> Starting back demodulation with 363. % 1.92/2.63 >>>> Starting back demodulation with 365. % 1.92/2.63 >>>> Starting back demodulation with 367. % 1.92/2.63 >>>> Starting back demodulation with 369. % 1.92/2.63 >>>> Starting back demodulation with 371. % 1.92/2.63 >>>> Starting back demodulation with 373. % 1.92/2.63 >>>> Starting back demodulation with 375. % 1.92/2.63 >>>> Starting back demodulation with 377. % 1.92/2.63 >>>> Starting back demodulation with 379. % 1.92/2.63 >>>> Starting back demodulation with 381. % 1.92/2.63 >>>> Starting back demodulation with 383. % 1.92/2.63 >>>> Starting back demodulation with 385. % 1.92/2.63 >>>> Starting back demodulation with 387. % 1.92/2.63 >>>> Starting back demodulation with 389. % 1.92/2.63 >>>> Starting back demodulation with 391. % 1.92/2.63 >>>> Starting back demodulation with 393. % 1.92/2.63 >>>> Starting back demodulation with 395. % 1.92/2.63 >>>> Starting back demodulation with 397. % 1.92/2.63 >>>> Starting back demodulation with 399. % 1.92/2.63 >>>> Starting back demodulation with 401. % 1.92/2.63 >>>> Starting back demodulation with 403. % 1.92/2.63 >>>> Starting back demodulation with 405. % 1.92/2.63 >>>> Starting back demodulation with 407. % 1.92/2.63 >>>> Starting back demodulation with 409. % 1.92/2.63 >>>> Starting back demodulation with 411. % 1.92/2.63 >>>> Starting back demodulation with 413. % 1.92/2.63 >>>> Starting back demodulation with 415. % 1.92/2.63 >>>> Starting back demodulation with 417. % 1.92/2.63 >>>> Starting back demodulation with 419. % 1.92/2.63 >>>> Starting back demodulation with 421. % 1.92/2.63 >>>> Starting back demodulation with 423. % 1.92/2.63 >>>> Starting back demodulation with 425. % 1.92/2.63 >>>> Starting back demodulation with 427. % 1.92/2.63 >>>> Starting back demodulation with 429. % 1.92/2.63 >>>> Starting back demodulation with 431. % 1.92/2.63 >>>> Starting back demodulation with 433. % 1.92/2.63 >>>> Starting back demodulation with 435. % 1.92/2.63 >>>> Starting back demodulation with 437. % 1.92/2.63 >>>> Starting back demodulation with 439. % 1.92/2.63 >>>> Starting back demodulation with 441. % 1.92/2.63 >>>> Starting back demodulation with 443. % 1.92/2.63 >>>> Starting back demodulation with 445. % 1.92/2.63 >>>> Starting back demodulation with 447. % 1.92/2.68 >>>> Starting back demodulation with 449. % 1.92/2.68 >>>> Starting back demodulation with 451. % 1.92/2.68 >>>> Starting back demodulation with 453. % 1.92/2.68 >>>> Starting back demodulation with 455. % 1.92/2.68 >>>> Starting back demodulation with 457. % 1.92/2.68 >>>> Starting back demodulation with 459. % 1.92/2.68 >>>> Starting back demodulation with 461. % 1.92/2.68 >>>> Starting back demodulation with 463. % 1.92/2.68 >>>> Starting back demodulation with 465. % 1.92/2.68 >>>> Starting back demodulation with 467. % 1.92/2.68 >>>> Starting back demodulation with 469. % 1.92/2.68 >>>> Starting back demodulation with 471. % 1.92/2.68 >>>> Starting back demodulation with 473. % 1.92/2.68 >>>> Starting back demodulation with 475. % 1.92/2.68 >>>> Starting back demodulation with 477. % 1.92/2.68 >>>> Starting back demodulation with 479. % 1.92/2.68 >>>> Starting back demodulation with 481. % 1.92/2.68 >>>> Starting back demodulation with 483. % 1.92/2.68 >>>> Starting back demodulation with 485. % 1.92/2.68 >>>> Starting back demodulation with 487. % 1.92/2.68 >>>> Starting back demodulation with 489. % 1.92/2.68 >>>> Starting back demodulation with 491. % 1.92/2.68 >>>> Starting back demodulation with 493. % 1.92/2.68 >>>> Starting back demodulation with 495. % 1.92/2.68 >>>> Starting back demodulation with 497. % 1.92/2.68 >>>> Starting back demodulation with 499. % 1.92/2.68 >>>> Starting back demodulation with 501. % 1.92/2.68 >>>> Starting back demodulation with 503. % 1.92/2.68 >>>> Starting back demodulation with 505. % 1.92/2.68 >>>> Starting back demodulation with 507. % 1.92/2.68 >>>> Starting back demodulation with 509. % 1.92/2.68 >> back demodulating 84 with 509. % 1.92/2.68 >>>> Starting back demodulation with 511. % 1.92/2.68 >>>> Starting back demodulation with 513. % 1.92/2.68 >>>> Starting back demodulation with 515. % 1.92/2.68 >>>> Starting back demodulation with 517. % 1.92/2.68 >>>> Starting back demodulation with 519. % 1.92/2.68 >>>> Starting back demodulation with 521. % 1.92/2.68 >>>> Starting back demodulation with 523. % 1.92/2.68 >>>> Starting back demodulation with 525. % 1.92/2.68 >>>> Starting back demodulation with 527. % 1.92/2.68 >>>> Starting back demodulation with 529. % 1.92/2.68 >>>> Starting back demodulation with 531. % 1.92/2.68 >>>> Starting back demodulation with 533. % 1.92/2.68 >>>> Starting back demodulation with 535. % 1.92/2.68 >>>> Starting back demodulation with 537. % 1.92/2.68 >>>> Starting back demodulation with 539. % 1.92/2.68 >>>> Starting back demodulation with 541. % 1.92/2.68 >>>> Starting back demodulation with 543. % 1.92/2.68 >>>> Starting back demodulation with 545. % 1.92/2.68 >>>> Starting back demodulation with 547. % 1.92/2.68 >>>> Starting back demodulation with 549. % 1.92/2.68 >>>> Starting back demodulation with 551. % 1.92/2.68 >>>> Starting back demodulation with 553. % 1.92/2.68 >>>> Starting back demodulation with 555. % 1.92/2.68 Following clause subsumed by 9 during input processing: 0 [copy,556,flip.1] aux(A,pair2(B,C))=pair2(B,s(C)). % 1.92/2.68 Following clause subsumed by 14 during input processing: 0 [copy,557,flip.1] aux3(A,B,pair2(C,D))=showNumnum(cons(C,A),D). % 1.92/2.68 >>>> Starting back demodulation with 559. % 1.92/2.68 Following clause subsumed by 60 during input processing: 0 [copy,560,flip.1] showNumnum(A,s(B))=aux3(A,B,aux2(s(B),min10(s(B)))). % 1.92/2.68 Following clause subsumed by 69 during input processing: 0 [copy,561,flip.1] show(mul(A,B))=append(showF(A),append(cons(mULT,nil),showF(B))). % 1.92/2.68 >>>> Starting back demodulation with 563. % 1.92/2.68 >>>> Starting back demodulation with 565. % 1.92/2.68 >>>> Starting back demodulation with 567. % 1.92/2.68 % 1.92/2.68 ======= end of input processing ======= % 1.92/2.68 % 1.92/2.68 =========== start of search =========== % 1.92/2.68 % 1.92/2.68 % 1.92/2.68 Resetting weight limit to 9. % 1.92/2.68 % 1.92/2.68 % 1.92/2.68 Resetting weight limit to 9. % 1.92/2.68 % 1.92/2.68 sos_size=294 % 1.92/2.68 % 1.92/2.68 Search stopped because sos empty. % 1.92/2.68 % 1.92/2.68 % 1.92/2.68 Search stopped because sos empty. % 1.92/2.68 % 1.92/2.68 ============ end of search ============ % 1.92/2.68 % 1.92/2.68 -------------- statistics ------------- % 1.92/2.68 clauses given 588 % 1.92/2.68 clauses generated 7962 % 1.92/2.68 clauses kept 606 % 1.92/2.68 clauses forward subsumed 2205 % 1.92/2.68 clauses back subsumed 6 % 1.92/2.68 Kbytes malloced 5859 % 1.92/2.68 % 1.92/2.68 ----------- times (seconds) ----------- % 1.92/2.68 user CPU time 0.06 (0 hr, 0 min, 0 sec) % 1.92/2.68 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 1.92/2.68 wall-clock time 2 (0 hr, 0 min, 2 sec) % 1.92/2.68 % 1.92/2.68 Process 28158 finished Tue May 5 11:39:49 2026 % 1.92/2.68 Otter interrupted % 1.92/2.68 PROOF NOT FOUND %------------------------------------------------------------------------------