%------------------------------------------------------------------------------ % 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 : n006.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 2.48s 2.76s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : SWX208+1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : otter-tptp-script %s % 0.18/0.35 % Computer : n006.cluster.edu % 0.18/0.35 % Model : x86_64 x86_64 % 0.18/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.35 % Memory : 8042.1875MB % 0.18/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.18/0.35 % CPULimit : 300 % 0.18/0.35 % WCLimit : 300 % 0.18/0.35 % DateTime : Tue May 5 11:37:15 EDT 2026 % 0.18/0.35 % CPUTime : % 1.88/2.14 ----- Otter 3.3f, August 2004 ----- % 1.88/2.14 The process was started by sandbox on n006.cluster.edu, % 1.88/2.14 Tue May 5 11:37:16 2026 % 1.88/2.14 The command was "./otter". The process ID is 13812. % 1.88/2.14 % 1.88/2.14 set(prolog_style_variables). % 1.88/2.14 set(auto). % 1.88/2.14 dependent: set(auto1). % 1.88/2.14 dependent: set(process_input). % 1.88/2.14 dependent: clear(print_kept). % 1.88/2.14 dependent: clear(print_new_demod). % 1.88/2.14 dependent: clear(print_back_demod). % 1.88/2.14 dependent: clear(print_back_sub). % 1.88/2.14 dependent: set(control_memory). % 1.88/2.14 dependent: assign(max_mem, 12000). % 1.88/2.14 dependent: assign(pick_given_ratio, 4). % 1.88/2.14 dependent: assign(stats_level, 1). % 1.88/2.14 dependent: assign(max_seconds, 10800). % 1.88/2.14 clear(print_given). % 1.88/2.14 % 1.88/2.14 formula_list(usable). % 1.88/2.14 all A (A=A). % 1.88/2.14 all X X2 (proj1pair(pair2(X,X2))=X). % 1.88/2.14 all X X2 (proj2pair(pair2(X,X2))=X2). % 1.88/2.14 all X X2 (head(cons(X,X2))=X). % 1.88/2.14 all X X2 (tail(cons(X,X2))=X2). % 1.88/2.14 all X X2 (nil!=cons(X,X2)). % 1.88/2.14 all X (proj1S(s(X))=X). % 1.88/2.14 all X (z!=s(X)). % 1.88/2.14 all X X2 (proj1Add(add(X,X2))=X). % 1.88/2.14 all X X2 (proj2Add(add(X,X2))=X2). % 1.88/2.14 all X X2 (proj1Mul(mul(X,X2))=X). % 1.88/2.14 all X X2 (proj2Mul(mul(X,X2))=X2). % 1.88/2.14 all X (proj1Num(num(X))=X). % 1.88/2.14 all X X2 (x!=add(X,X2)). % 1.88/2.14 all X X2 (x!=mul(X,X2)). % 1.88/2.14 all X (x!=num(X)). % 1.88/2.14 all X X2 X3 X4 (add(X,X2)!=mul(X3,X4)). % 1.88/2.14 all X X2 X3 (add(X,X2)!=num(X3)). % 1.88/2.14 all X X2 X3 (mul(X,X2)!=num(X3)). % 1.88/2.14 all X (proj1Left(left(X))=X). % 1.88/2.14 all X (proj1Right(right(X))=X). % 1.88/2.14 all X X2 (left(X)!=right(X2)). % 1.88/2.14 pAR1!=pAR2. % 1.88/2.14 pAR1!=pLUS. % 1.88/2.14 pAR1!=mULT. % 1.88/2.14 pAR1!=cHARX. % 1.88/2.14 pAR1!=dIG0. % 1.88/2.14 pAR1!=dIG1. % 1.88/2.14 pAR1!=dIG2. % 1.88/2.14 pAR1!=dIG3. % 1.88/2.14 pAR1!=dIG4. % 1.88/2.14 pAR1!=dIG5. % 1.88/2.14 pAR1!=dIG6. % 1.88/2.14 pAR1!=dIG7. % 1.88/2.14 pAR1!=dIG8. % 1.88/2.14 pAR1!=dIG9. % 1.88/2.14 pAR2!=pLUS. % 1.88/2.14 pAR2!=mULT. % 1.88/2.14 pAR2!=cHARX. % 1.88/2.14 pAR2!=dIG0. % 1.88/2.14 pAR2!=dIG1. % 1.88/2.14 pAR2!=dIG2. % 1.88/2.14 pAR2!=dIG3. % 1.88/2.14 pAR2!=dIG4. % 1.88/2.14 pAR2!=dIG5. % 1.88/2.14 pAR2!=dIG6. % 1.88/2.14 pAR2!=dIG7. % 1.88/2.14 pAR2!=dIG8. % 1.88/2.14 pAR2!=dIG9. % 1.88/2.14 pLUS!=mULT. % 1.88/2.14 pLUS!=cHARX. % 1.88/2.14 pLUS!=dIG0. % 1.88/2.14 pLUS!=dIG1. % 1.88/2.14 pLUS!=dIG2. % 1.88/2.14 pLUS!=dIG3. % 1.88/2.14 pLUS!=dIG4. % 1.88/2.14 pLUS!=dIG5. % 1.88/2.14 pLUS!=dIG6. % 1.88/2.14 pLUS!=dIG7. % 1.88/2.14 pLUS!=dIG8. % 1.88/2.14 pLUS!=dIG9. % 1.88/2.14 mULT!=cHARX. % 1.88/2.14 mULT!=dIG0. % 1.88/2.14 mULT!=dIG1. % 1.88/2.14 mULT!=dIG2. % 1.88/2.14 mULT!=dIG3. % 1.88/2.14 mULT!=dIG4. % 1.88/2.14 mULT!=dIG5. % 1.88/2.14 mULT!=dIG6. % 1.88/2.14 mULT!=dIG7. % 1.88/2.14 mULT!=dIG8. % 1.88/2.14 mULT!=dIG9. % 1.88/2.14 cHARX!=dIG0. % 1.88/2.14 cHARX!=dIG1. % 1.88/2.14 cHARX!=dIG2. % 1.88/2.14 cHARX!=dIG3. % 1.88/2.14 cHARX!=dIG4. % 1.88/2.14 cHARX!=dIG5. % 1.88/2.14 cHARX!=dIG6. % 1.88/2.14 cHARX!=dIG7. % 1.88/2.14 cHARX!=dIG8. % 1.88/2.14 cHARX!=dIG9. % 1.88/2.14 dIG0!=dIG1. % 1.88/2.14 dIG0!=dIG2. % 1.88/2.14 dIG0!=dIG3. % 1.88/2.14 dIG0!=dIG4. % 1.88/2.14 dIG0!=dIG5. % 1.88/2.14 dIG0!=dIG6. % 1.88/2.14 dIG0!=dIG7. % 1.88/2.14 dIG0!=dIG8. % 1.88/2.14 dIG0!=dIG9. % 1.88/2.14 dIG1!=dIG2. % 1.88/2.14 dIG1!=dIG3. % 1.88/2.14 dIG1!=dIG4. % 1.88/2.14 dIG1!=dIG5. % 1.88/2.14 dIG1!=dIG6. % 1.88/2.14 dIG1!=dIG7. % 1.88/2.14 dIG1!=dIG8. % 1.88/2.14 dIG1!=dIG9. % 1.88/2.14 dIG2!=dIG3. % 1.88/2.14 dIG2!=dIG4. % 1.88/2.14 dIG2!=dIG5. % 1.88/2.14 dIG2!=dIG6. % 1.88/2.14 dIG2!=dIG7. % 1.88/2.14 dIG2!=dIG8. % 1.88/2.14 dIG2!=dIG9. % 1.88/2.14 dIG3!=dIG4. % 1.88/2.14 dIG3!=dIG5. % 1.88/2.14 dIG3!=dIG6. % 1.88/2.14 dIG3!=dIG7. % 1.88/2.14 dIG3!=dIG8. % 1.88/2.14 dIG3!=dIG9. % 1.88/2.14 dIG4!=dIG5. % 1.88/2.14 dIG4!=dIG6. % 1.88/2.14 dIG4!=dIG7. % 1.88/2.14 dIG4!=dIG8. % 1.88/2.14 dIG4!=dIG9. % 1.88/2.14 dIG5!=dIG6. % 1.88/2.14 dIG5!=dIG7. % 1.88/2.14 dIG5!=dIG8. % 1.88/2.14 dIG5!=dIG9. % 1.88/2.14 dIG6!=dIG7. % 1.88/2.14 dIG6!=dIG8. % 1.88/2.14 dIG6!=dIG9. % 1.88/2.14 dIG7!=dIG8. % 1.88/2.14 dIG7!=dIG9. % 1.88/2.14 dIG8!=dIG9. % 1.88/2.14 all Y (append(nil,Y)=Y). % 1.88/2.14 all Y Z Xs (append(cons(Z,Xs),Y)=cons(Z,append(Xs,Y))). % 1.88/2.14 x2(z,z)=z. % 1.88/2.14 all Z (x2(z,s(Z))=z). % 1.88/2.14 all N (x2(s(N),z)=s(N)). % 1.88/2.14 all N M (x2(s(N),s(M))=x2(N,M)). % 1.88/2.14 min10(z)=left(dIG0). % 1.88/2.14 min10(s(z))=left(dIG1). % 1.88/2.14 min10(s(s(z)))=left(dIG2). % 1.88/2.14 min10(s(s(s(z))))=left(dIG3). % 1.88/2.14 min10(s(s(s(s(z)))))=left(dIG4). % 1.88/2.14 min10(s(s(s(s(s(z))))))=left(dIG5). % 1.88/2.14 min10(s(s(s(s(s(s(z)))))))=left(dIG6). % 1.88/2.14 min10(s(s(s(s(s(s(s(z))))))))=left(dIG7). % 1.88/2.14 min10(s(s(s(s(s(s(s(s(z)))))))))=left(dIG8). % 1.88/2.14 min10(s(s(s(s(s(s(s(s(s(z))))))))))=left(dIG9). % 1.88/2.14 all X9 (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.88/2.14 all X D (min10(X)=left(D)->mod10(X)=pair2(D,z)). % 1.88/2.14 all X N D1 N2 (min10(X)=right(N)-> (mod10(N)=pair2(D1,N2)->mod10(X)=pair2(D1,s(N2)))). % 1.88/2.14 all X (showNumnum(X,z)=X). % 1.88/2.14 all X Z A1 N (mod10(s(Z))=pair2(A1,N)->showNumnum(X,s(Z))=showNumnum(cons(A1,X),N)). % 1.88/2.14 showNum(z)=cons(dIG0,nil). % 1.88/2.14 all Y (showNum(s(Y))=showNumnum(nil,s(Y))). % 1.88/2.14 show(x)=cons(cHARX,nil). % 1.88/2.14 all B C (show(add(B,C))=append(show(B),append(cons(pLUS,nil),show(C)))). % 1.88/2.14 all A3 B2 (show(mul(A3,B2))=append(showF(A3),append(cons(mULT,nil),showF(B2)))). % 1.88/2.14 all N (show(num(N))=showNum(N)). % 1.88/2.14 all X (X!=add(proj1Add(X),proj2Add(X))->showF(X)=show(X)). % 1.88/2.14 all Y Z (showF(add(Y,Z))=cons(pAR1,append(show(add(Y,Z)),cons(pAR2,nil)))). % 1.88/2.14 -(exists E (show(E)=cons(pAR1,cons(pAR1,cons(cHARX,cons(pLUS,cons(dIG5,cons(pAR2,cons(pLUS,cons(dIG7,cons(pAR2,cons(mULT,cons(cHARX,nil))))))))))))). % 1.88/2.14 end_of_list. % 1.88/2.14 % 1.88/2.14 -------> usable clausifies to: % 1.88/2.14 % 1.88/2.14 list(usable). % 1.88/2.14 0 [] A=A. % 1.88/2.14 0 [] proj1pair(pair2(X,X2))=X. % 1.88/2.14 0 [] proj2pair(pair2(X,X2))=X2. % 1.88/2.14 0 [] head(cons(X,X2))=X. % 1.88/2.14 0 [] tail(cons(X,X2))=X2. % 1.88/2.14 0 [] nil!=cons(X,X2). % 1.88/2.14 0 [] proj1S(s(X))=X. % 1.88/2.14 0 [] z!=s(X). % 1.88/2.14 0 [] proj1Add(add(X,X2))=X. % 1.88/2.14 0 [] proj2Add(add(X,X2))=X2. % 1.88/2.14 0 [] proj1Mul(mul(X,X2))=X. % 1.88/2.14 0 [] proj2Mul(mul(X,X2))=X2. % 1.88/2.14 0 [] proj1Num(num(X))=X. % 1.88/2.14 0 [] x!=add(X,X2). % 1.88/2.14 0 [] x!=mul(X,X2). % 1.88/2.14 0 [] x!=num(X). % 1.88/2.14 0 [] add(X,X2)!=mul(X3,X4). % 1.88/2.14 0 [] add(X,X2)!=num(X3). % 1.88/2.14 0 [] mul(X,X2)!=num(X3). % 1.88/2.14 0 [] proj1Left(left(X))=X. % 1.88/2.14 0 [] proj1Right(right(X))=X. % 1.88/2.14 0 [] left(X)!=right(X2). % 1.88/2.14 0 [] pAR1!=pAR2. % 1.88/2.14 0 [] pAR1!=pLUS. % 1.88/2.14 0 [] pAR1!=mULT. % 1.88/2.14 0 [] pAR1!=cHARX. % 1.88/2.14 0 [] pAR1!=dIG0. % 1.88/2.14 0 [] pAR1!=dIG1. % 1.88/2.14 0 [] pAR1!=dIG2. % 1.88/2.14 0 [] pAR1!=dIG3. % 1.88/2.14 0 [] pAR1!=dIG4. % 1.88/2.14 0 [] pAR1!=dIG5. % 1.88/2.14 0 [] pAR1!=dIG6. % 1.88/2.14 0 [] pAR1!=dIG7. % 1.88/2.14 0 [] pAR1!=dIG8. % 1.88/2.14 0 [] pAR1!=dIG9. % 1.88/2.14 0 [] pAR2!=pLUS. % 1.88/2.14 0 [] pAR2!=mULT. % 1.88/2.14 0 [] pAR2!=cHARX. % 1.88/2.14 0 [] pAR2!=dIG0. % 1.88/2.14 0 [] pAR2!=dIG1. % 1.88/2.14 0 [] pAR2!=dIG2. % 1.88/2.14 0 [] pAR2!=dIG3. % 1.88/2.14 0 [] pAR2!=dIG4. % 1.88/2.14 0 [] pAR2!=dIG5. % 1.88/2.14 0 [] pAR2!=dIG6. % 1.88/2.14 0 [] pAR2!=dIG7. % 1.88/2.14 0 [] pAR2!=dIG8. % 1.88/2.14 0 [] pAR2!=dIG9. % 1.88/2.14 0 [] pLUS!=mULT. % 1.88/2.14 0 [] pLUS!=cHARX. % 1.88/2.14 0 [] pLUS!=dIG0. % 1.88/2.14 0 [] pLUS!=dIG1. % 1.88/2.14 0 [] pLUS!=dIG2. % 1.88/2.14 0 [] pLUS!=dIG3. % 1.88/2.14 0 [] pLUS!=dIG4. % 1.88/2.14 0 [] pLUS!=dIG5. % 1.88/2.14 0 [] pLUS!=dIG6. % 1.88/2.14 0 [] pLUS!=dIG7. % 1.88/2.14 0 [] pLUS!=dIG8. % 1.88/2.14 0 [] pLUS!=dIG9. % 1.88/2.14 0 [] mULT!=cHARX. % 1.88/2.14 0 [] mULT!=dIG0. % 1.88/2.14 0 [] mULT!=dIG1. % 1.88/2.14 0 [] mULT!=dIG2. % 1.88/2.14 0 [] mULT!=dIG3. % 1.88/2.14 0 [] mULT!=dIG4. % 1.88/2.14 0 [] mULT!=dIG5. % 1.88/2.14 0 [] mULT!=dIG6. % 1.88/2.14 0 [] mULT!=dIG7. % 1.88/2.14 0 [] mULT!=dIG8. % 1.88/2.14 0 [] mULT!=dIG9. % 1.88/2.14 0 [] cHARX!=dIG0. % 1.88/2.14 0 [] cHARX!=dIG1. % 1.88/2.14 0 [] cHARX!=dIG2. % 1.88/2.14 0 [] cHARX!=dIG3. % 1.88/2.14 0 [] cHARX!=dIG4. % 1.88/2.14 0 [] cHARX!=dIG5. % 1.88/2.14 0 [] cHARX!=dIG6. % 1.88/2.14 0 [] cHARX!=dIG7. % 1.88/2.14 0 [] cHARX!=dIG8. % 1.88/2.14 0 [] cHARX!=dIG9. % 1.88/2.14 0 [] dIG0!=dIG1. % 1.88/2.14 0 [] dIG0!=dIG2. % 1.88/2.14 0 [] dIG0!=dIG3. % 1.88/2.14 0 [] dIG0!=dIG4. % 1.88/2.14 0 [] dIG0!=dIG5. % 1.88/2.14 0 [] dIG0!=dIG6. % 1.88/2.14 0 [] dIG0!=dIG7. % 1.88/2.14 0 [] dIG0!=dIG8. % 1.88/2.14 0 [] dIG0!=dIG9. % 1.88/2.14 0 [] dIG1!=dIG2. % 1.88/2.14 0 [] dIG1!=dIG3. % 1.88/2.14 0 [] dIG1!=dIG4. % 1.88/2.14 0 [] dIG1!=dIG5. % 1.88/2.14 0 [] dIG1!=dIG6. % 1.88/2.14 0 [] dIG1!=dIG7. % 1.88/2.14 0 [] dIG1!=dIG8. % 1.88/2.14 0 [] dIG1!=dIG9. % 1.88/2.14 0 [] dIG2!=dIG3. % 1.88/2.14 0 [] dIG2!=dIG4. % 1.88/2.14 0 [] dIG2!=dIG5. % 1.88/2.14 0 [] dIG2!=dIG6. % 1.88/2.14 0 [] dIG2!=dIG7. % 1.88/2.14 0 [] dIG2!=dIG8. % 1.88/2.14 0 [] dIG2!=dIG9. % 1.88/2.14 0 [] dIG3!=dIG4. % 1.88/2.14 0 [] dIG3!=dIG5. % 1.88/2.14 0 [] dIG3!=dIG6. % 1.88/2.14 0 [] dIG3!=dIG7. % 1.88/2.14 0 [] dIG3!=dIG8. % 1.88/2.14 0 [] dIG3!=dIG9. % 1.88/2.14 0 [] dIG4!=dIG5. % 1.88/2.14 0 [] dIG4!=dIG6. % 1.88/2.14 0 [] dIG4!=dIG7. % 1.88/2.14 0 [] dIG4!=dIG8. % 1.88/2.14 0 [] dIG4!=dIG9. % 1.88/2.14 0 [] dIG5!=dIG6. % 1.88/2.14 0 [] dIG5!=dIG7. % 1.88/2.14 0 [] dIG5!=dIG8. % 1.88/2.14 0 [] dIG5!=dIG9. % 1.88/2.14 0 [] dIG6!=dIG7. % 1.88/2.14 0 [] dIG6!=dIG8. % 1.88/2.14 0 [] dIG6!=dIG9. % 1.88/2.14 0 [] dIG7!=dIG8. % 1.88/2.14 0 [] dIG7!=dIG9. % 1.88/2.14 0 [] dIG8!=dIG9. % 1.88/2.14 0 [] append(nil,Y)=Y. % 1.88/2.14 0 [] append(cons(Z,Xs),Y)=cons(Z,append(Xs,Y)). % 1.88/2.14 0 [] x2(z,z)=z. % 1.88/2.14 0 [] x2(z,s(Z))=z. % 1.88/2.14 0 [] x2(s(N),z)=s(N). % 1.88/2.14 0 [] x2(s(N),s(M))=x2(N,M). % 1.88/2.14 0 [] min10(z)=left(dIG0). % 1.88/2.14 0 [] min10(s(z))=left(dIG1). % 1.88/2.14 0 [] min10(s(s(z)))=left(dIG2). % 1.88/2.14 0 [] min10(s(s(s(z))))=left(dIG3). % 1.88/2.14 0 [] min10(s(s(s(s(z)))))=left(dIG4). % 1.88/2.14 0 [] min10(s(s(s(s(s(z))))))=left(dIG5). % 1.88/2.14 0 [] min10(s(s(s(s(s(s(z)))))))=left(dIG6). % 1.88/2.14 0 [] min10(s(s(s(s(s(s(s(z))))))))=left(dIG7). % 1.88/2.14 0 [] min10(s(s(s(s(s(s(s(s(z)))))))))=left(dIG8). % 1.88/2.14 0 [] min10(s(s(s(s(s(s(s(s(s(z))))))))))=left(dIG9). % 1.88/2.14 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.88/2.14 0 [] min10(X)!=left(D)|mod10(X)=pair2(D,z). % 1.88/2.14 0 [] min10(X)!=right(N)|mod10(N)!=pair2(D1,N2)|mod10(X)=pair2(D1,s(N2)). % 1.88/2.14 0 [] showNumnum(X,z)=X. % 1.88/2.14 0 [] mod10(s(Z))!=pair2(A1,N)|showNumnum(X,s(Z))=showNumnum(cons(A1,X),N). % 1.88/2.14 0 [] showNum(z)=cons(dIG0,nil). % 1.88/2.14 0 [] showNum(s(Y))=showNumnum(nil,s(Y)). % 1.88/2.14 0 [] show(x)=cons(cHARX,nil). % 1.88/2.14 0 [] show(add(B,C))=append(show(B),append(cons(pLUS,nil),show(C))). % 1.88/2.14 0 [] show(mul(A3,B2))=append(showF(A3),append(cons(mULT,nil),showF(B2))). % 1.88/2.14 0 [] show(num(N))=showNum(N). % 1.88/2.14 0 [] X=add(proj1Add(X),proj2Add(X))|showF(X)=show(X). % 1.88/2.14 0 [] showF(add(Y,Z))=cons(pAR1,append(show(add(Y,Z)),cons(pAR2,nil))). % 1.88/2.14 0 [] show(E)!=cons(pAR1,cons(pAR1,cons(cHARX,cons(pLUS,cons(dIG5,cons(pAR2,cons(pLUS,cons(dIG7,cons(pAR2,cons(mULT,cons(cHARX,nil))))))))))). % 1.88/2.14 end_of_list. % 1.88/2.14 % 1.88/2.14 SCAN INPUT: prop=0, horn=0, equality=1, symmetry=0, max_lits=3. % 1.88/2.14 % 1.88/2.14 This ia a non-Horn set with equality. The strategy will be % 1.88/2.14 Knuth-Bendix, ordered hyper_res, factoring, and unit % 1.88/2.14 deletion, with positive clauses in sos and nonpositive % 1.88/2.14 clauses in usable. % 1.88/2.14 % 1.88/2.14 dependent: set(knuth_bendix). % 1.88/2.14 dependent: set(anl_eq). % 1.88/2.14 dependent: set(para_from). % 1.88/2.14 dependent: set(para_into). % 1.88/2.14 dependent: clear(para_from_right). % 1.88/2.14 dependent: clear(para_into_right). % 1.88/2.14 dependent: set(para_from_vars). % 1.88/2.14 dependent: set(eq_units_both_ways). % 1.88/2.14 dependent: set(dynamic_demod_all). % 1.88/2.14 dependent: set(dynamic_demod). % 1.88/2.14 dependent: set(order_eq). % 1.88/2.14 dependent: set(back_demod). % 1.88/2.14 dependent: set(lrpo). % 1.88/2.14 dependent: set(hyper_res). % 1.88/2.14 dependent: set(unit_deletion). % 1.88/2.14 dependent: set(factor). % 1.88/2.14 % 1.88/2.14 ------------> process usable: % 1.88/2.14 ** KEPT (pick-wt=5): 2 [copy,1,flip.1] cons(A,B)!=nil. % 1.88/2.14 ** KEPT (pick-wt=4): 4 [copy,3,flip.1] s(A)!=z. % 1.88/2.14 ** KEPT (pick-wt=5): 6 [copy,5,flip.1] add(A,B)!=x. % 1.88/2.14 ** KEPT (pick-wt=5): 8 [copy,7,flip.1] mul(A,B)!=x. % 1.88/2.14 ** KEPT (pick-wt=4): 10 [copy,9,flip.1] num(A)!=x. % 1.88/2.14 ** KEPT (pick-wt=7): 11 [] add(A,B)!=mul(C,D). % 1.88/2.14 ** KEPT (pick-wt=6): 12 [] add(A,B)!=num(C). % 1.88/2.14 ** KEPT (pick-wt=6): 13 [] mul(A,B)!=num(C). % 1.88/2.14 ** KEPT (pick-wt=5): 14 [] left(A)!=right(B). % 1.88/2.14 ** KEPT (pick-wt=3): 16 [copy,15,flip.1] pAR2!=pAR1. % 1.88/2.14 ** KEPT (pick-wt=3): 18 [copy,17,flip.1] pLUS!=pAR1. % 1.88/2.14 ** KEPT (pick-wt=3): 19 [] pAR1!=mULT. % 1.88/2.14 ** KEPT (pick-wt=3): 20 [] pAR1!=cHARX. % 1.88/2.14 ** KEPT (pick-wt=3): 21 [] pAR1!=dIG0. % 1.88/2.14 ** KEPT (pick-wt=3): 22 [] pAR1!=dIG1. % 1.88/2.14 ** KEPT (pick-wt=3): 23 [] pAR1!=dIG2. % 1.88/2.14 ** KEPT (pick-wt=3): 24 [] pAR1!=dIG3. % 1.88/2.14 ** KEPT (pick-wt=3): 25 [] pAR1!=dIG4. % 1.88/2.14 ** KEPT (pick-wt=3): 26 [] pAR1!=dIG5. % 1.88/2.14 ** KEPT (pick-wt=3): 27 [] pAR1!=dIG6. % 1.88/2.14 ** KEPT (pick-wt=3): 28 [] pAR1!=dIG7. % 1.88/2.14 ** KEPT (pick-wt=3): 29 [] pAR1!=dIG8. % 1.88/2.14 ** KEPT (pick-wt=3): 30 [] pAR1!=dIG9. % 1.88/2.14 ** KEPT (pick-wt=3): 32 [copy,31,flip.1] pLUS!=pAR2. % 1.88/2.14 ** KEPT (pick-wt=3): 33 [] pAR2!=mULT. % 1.88/2.14 ** KEPT (pick-wt=3): 34 [] pAR2!=cHARX. % 1.88/2.14 ** KEPT (pick-wt=3): 35 [] pAR2!=dIG0. % 1.88/2.14 ** KEPT (pick-wt=3): 36 [] pAR2!=dIG1. % 1.88/2.14 ** KEPT (pick-wt=3): 37 [] pAR2!=dIG2. % 1.88/2.14 ** KEPT (pick-wt=3): 38 [] pAR2!=dIG3. % 1.88/2.14 ** KEPT (pick-wt=3): 39 [] pAR2!=dIG4. % 1.88/2.14 ** KEPT (pick-wt=3): 40 [] pAR2!=dIG5. % 1.88/2.14 ** KEPT (pick-wt=3): 41 [] pAR2!=dIG6. % 1.88/2.14 ** KEPT (pick-wt=3): 42 [] pAR2!=dIG7. % 1.88/2.14 ** KEPT (pick-wt=3): 43 [] pAR2!=dIG8. % 1.88/2.14 ** KEPT (pick-wt=3): 44 [] pAR2!=dIG9. % 1.88/2.14 ** KEPT (pick-wt=3): 45 [] pLUS!=mULT. % 1.88/2.14 ** KEPT (pick-wt=3): 46 [] pLUS!=cHARX. % 1.88/2.14 ** KEPT (pick-wt=3): 47 [] pLUS!=dIG0. % 1.88/2.14 ** KEPT (pick-wt=3): 48 [] pLUS!=dIG1. % 1.88/2.14 ** KEPT (pick-wt=3): 49 [] pLUS!=dIG2. % 1.88/2.14 ** KEPT (pick-wt=3): 50 [] pLUS!=dIG3. % 1.88/2.14 ** KEPT (pick-wt=3): 51 [] pLUS!=dIG4. % 1.88/2.14 ** KEPT (pick-wt=3): 52 [] pLUS!=dIG5. % 1.88/2.14 ** KEPT (pick-wt=3): 53 [] pLUS!=dIG6. % 1.88/2.14 ** KEPT (pick-wt=3): 54 [] pLUS!=dIG7. % 1.88/2.14 ** KEPT (pick-wt=3): 55 [] pLUS!=dIG8. % 1.88/2.14 ** KEPT (pick-wt=3): 56 [] pLUS!=dIG9. % 1.88/2.14 ** KEPT (pick-wt=3): 57 [] mULT!=cHARX. % 1.88/2.14 ** KEPT (pick-wt=3): 58 [] mULT!=dIG0. % 1.88/2.14 ** KEPT (pick-wt=3): 59 [] mULT!=dIG1. % 1.88/2.14 ** KEPT (pick-wt=3): 60 [] mULT!=dIG2. % 1.88/2.14 ** KEPT (pick-wt=3): 61 [] mULT!=dIG3. % 1.88/2.14 ** KEPT (pick-wt=3): 62 [] mULT!=dIG4. % 1.88/2.14 ** KEPT (pick-wt=3): 63 [] mULT!=dIG5. % 1.88/2.14 ** KEPT (pick-wt=3): 64 [] mULT!=dIG6. % 1.88/2.14 ** KEPT (pick-wt=3): 65 [] mULT!=dIG7. % 1.88/2.14 ** KEPT (pick-wt=3): 66 [] mULT!=dIG8. % 1.88/2.14 ** KEPT (pick-wt=3): 67 [] mULT!=dIG9. % 1.88/2.14 ** KEPT (pick-wt=3): 69 [copy,68,flip.1] dIG0!=cHARX. % 1.88/2.14 ** KEPT (pick-wt=3): 71 [copy,70,flip.1] dIG1!=cHARX. % 1.88/2.14 ** KEPT (pick-wt=3): 73 [copy,72,flip.1] dIG2!=cHARX. % 1.88/2.14 ** KEPT (pick-wt=3): 75 [copy,74,flip.1] dIG3!=cHARX. % 1.88/2.14 ** KEPT (pick-wt=3): 77 [copy,76,flip.1] dIG4!=cHARX. % 1.88/2.14 ** KEPT (pick-wt=3): 79 [copy,78,flip.1] dIG5!=cHARX. % 1.88/2.14 ** KEPT (pick-wt=3): 81 [copy,80,flip.1] dIG6!=cHARX. % 1.88/2.14 ** KEPT (pick-wt=3): 83 [copy,82,flip.1] dIG7!=cHARX. % 1.88/2.14 ** KEPT (pick-wt=3): 85 [copy,84,flip.1] dIG8!=cHARX. % 1.88/2.14 ** KEPT (pick-wt=3): 87 [copy,86,flip.1] dIG9!=cHARX. % 1.88/2.14 ** KEPT (pick-wt=3): 89 [copy,88,flip.1] dIG1!=dIG0. % 1.88/2.14 ** KEPT (pick-wt=3): 91 [copy,90,flip.1] dIG2!=dIG0. % 1.88/2.14 ** KEPT (pick-wt=3): 93 [copy,92,flip.1] dIG3!=dIG0. % 1.88/2.14 ** KEPT (pick-wt=3): 95 [copy,94,flip.1] dIG4!=dIG0. % 1.88/2.14 ** KEPT (pick-wt=3): 97 [copy,96,flip.1] dIG5!=dIG0. % 1.88/2.14 ** KEPT (pick-wt=3): 99 [copy,98,flip.1] dIG6!=dIG0. % 1.88/2.14 ** KEPT (pick-wt=3): 101 [copy,100,flip.1] dIG7!=dIG0. % 1.88/2.14 ** KEPT (pick-wt=3): 103 [copy,102,flip.1] dIG8!=dIG0. % 1.88/2.14 ** KEPT (pick-wt=3): 105 [copy,104,flip.1] dIG9!=dIG0. % 1.88/2.14 ** KEPT (pick-wt=3): 107 [copy,106,flip.1] dIG2!=dIG1. % 1.88/2.14 ** KEPT (pick-wt=3): 109 [copy,108,flip.1] dIG3!=dIG1. % 1.88/2.14 ** KEPT (pick-wt=3): 111 [copy,110,flip.1] dIG4!=dIG1. % 1.88/2.14 ** KEPT (pick-wt=3): 113 [copy,112,flip.1] dIG5!=dIG1. % 1.88/2.14 ** KEPT (pick-wt=3): 115 [copy,114,flip.1] dIG6!=dIG1. % 1.88/2.14 ** KEPT (pick-wt=3): 117 [copy,116,flip.1] dIG7!=dIG1. % 1.88/2.14 ** KEPT (pick-wt=3): 119 [copy,118,flip.1] dIG8!=dIG1. % 1.88/2.14 ** KEPT (pick-wt=3): 121 [copy,120,flip.1] dIG9!=dIG1. % 1.88/2.14 ** KEPT (pick-wt=3): 123 [copy,122,flip.1] dIG3!=dIG2. % 1.88/2.14 ** KEPT (pick-wt=3): 125 [copy,124,flip.1] dIG4!=dIG2. % 1.88/2.14 ** KEPT (pick-wt=3): 127 [copy,126,flip.1] dIG5!=dIG2. % 1.88/2.14 ** KEPT (pick-wt=3): 129 [copy,128,flip.1] dIG6!=dIG2. % 1.88/2.14 ** KEPT (pick-wt=3): 131 [copy,130,flip.1] dIG7!=dIG2. % 1.88/2.14 ** KEPT (pick-wt=3): 133 [copy,132,flip.1] dIG8!=dIG2. % 1.88/2.14 ** KEPT (pick-wt=3): 135 [copy,134,flip.1] dIG9!=dIG2. % 1.88/2.14 ** KEPT (pick-wt=3): 137 [copy,136,flip.1] dIG4!=dIG3. % 1.88/2.14 ** KEPT (pick-wt=3): 139 [copy,138,flip.1] dIG5!=dIG3. % 1.88/2.14 ** KEPT (pick-wt=3): 141 [copy,140,flip.1] dIG6!=dIG3. % 1.88/2.14 ** KEPT (pick-wt=3): 143 [copy,142,flip.1] dIG7!=dIG3. % 1.88/2.14 ** KEPT (pick-wt=3): 145 [copy,144,flip.1] dIG8!=dIG3. % 1.88/2.14 ** KEPT (pick-wt=3): 147 [copy,146,flip.1] dIG9!=dIG3. % 1.88/2.14 ** KEPT (pick-wt=3): 149 [copy,148,flip.1] dIG5!=dIG4. % 1.88/2.14 ** KEPT (pick-wt=3): 151 [copy,150,flip.1] dIG6!=dIG4. % 1.88/2.14 ** KEPT (pick-wt=3): 153 [copy,152,flip.1] dIG7!=dIG4. % 1.88/2.14 ** KEPT (pick-wt=3): 155 [copy,154,flip.1] dIG8!=dIG4. % 1.88/2.14 ** KEPT (pick-wt=3): 157 [copy,156,flip.1] dIG9!=dIG4. % 1.88/2.14 ** KEPT (pick-wt=3): 159 [copy,158,flip.1] dIG6!=dIG5. % 1.88/2.14 ** KEPT (pick-wt=3): 161 [copy,160,flip.1] dIG7!=dIG5. % 1.88/2.14 ** KEPT (pick-wt=3): 163 [copy,162,flip.1] dIG8!=dIG5. % 1.88/2.14 ** KEPT (pick-wt=3): 165 [copy,164,flip.1] dIG9!=dIG5. % 1.88/2.14 ** KEPT (pick-wt=3): 167 [copy,166,flip.1] dIG7!=dIG6. % 1.88/2.14 ** KEPT (pick-wt=3): 169 [copy,168,flip.1] dIG8!=dIG6. % 1.88/2.14 ** KEPT (pick-wt=3): 171 [copy,170,flip.1] dIG9!=dIG6. % 1.88/2.14 ** KEPT (pick-wt=3): 173 [copy,172,flip.1] dIG8!=dIG7. % 1.88/2.14 ** KEPT (pick-wt=3): 175 [copy,174,flip.1] dIG9!=dIG7. % 1.88/2.14 ** KEPT (pick-wt=3): 177 [copy,176,flip.1] dIG9!=dIG8. % 1.88/2.14 ** KEPT (pick-wt=11): 178 [] min10(A)!=left(B)|mod10(A)=pair2(B,z). % 1.88/2.14 ** KEPT (pick-wt=18): 179 [] min10(A)!=right(B)|mod10(B)!=pair2(C,D)|mod10(A)=pair2(C,s(D)). % 1.88/2.14 ** KEPT (pick-wt=17): 180 [] mod10(s(A))!=pair2(B,C)|showNumnum(D,s(A))=showNumnum(cons(B,D),C). % 1.88/2.14 ** KEPT (pick-wt=26): 181 [] 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))))))))))). % 1.88/2.14 ** KEPT (pick-wt=7): 182 [copy,11,flip.1] mul(A,B)!=add(C,D). % 1.88/2.14 ** KEPT (pick-wt=6): 183 [copy,12,flip.1] num(A)!=add(B,C). % 1.88/2.14 ** KEPT (pick-wt=6): 184 [copy,13,flip.1] num(A)!=mul(B,C). % 1.88/2.14 ** KEPT (pick-wt=5): 185 [copy,14,flip.1] right(A)!=left(B). % 1.88/2.14 Following clause subsumed by 11 during input processing: 0 [copy,182,flip.1] add(A,B)!=mul(C,D). % 1.88/2.14 Following clause subsumed by 12 during input processing: 0 [copy,183,flip.1] add(A,B)!=num(C). % 1.88/2.14 Following clause subsumed by 13 during input processing: 0 [copy,184,flip.1] mul(A,B)!=num(C). % 1.88/2.14 Following clause subsumed by 14 during input processing: 0 [copy,185,flip.1] left(A)!=right(B). % 1.88/2.14 % 1.88/2.14 ------------> process sos: % 1.88/2.14 ** KEPT (pick-wt=3): 186 [] A=A. % 1.88/2.14 ** KEPT (pick-wt=6): 187 [] proj1pair(pair2(A,B))=A. % 1.88/2.14 ---> New Demodulator: 188 [new_demod,187] proj1pair(pair2(A,B))=A. % 1.88/2.14 ** KEPT (pick-wt=6): 189 [] proj2pair(pair2(A,B))=B. % 1.88/2.14 ---> New Demodulator: 190 [new_demod,189] proj2pair(pair2(A,B))=B. % 1.88/2.14 ** KEPT (pick-wt=6): 191 [] head(cons(A,B))=A. % 1.88/2.14 ---> New Demodulator: 192 [new_demod,191] head(cons(A,B))=A. % 1.88/2.14 ** KEPT (pick-wt=6): 193 [] tail(cons(A,B))=B. % 1.88/2.14 ---> New Demodulator: 194 [new_demod,193] tail(cons(A,B))=B. % 1.88/2.14 ** KEPT (pick-wt=5): 195 [] proj1S(s(A))=A. % 1.88/2.14 ---> New Demodulator: 196 [new_demod,195] proj1S(s(A))=A. % 1.88/2.14 ** KEPT (pick-wt=6): 197 [] proj1Add(add(A,B))=A. % 1.88/2.14 ---> New Demodulator: 198 [new_demod,197] proj1Add(add(A,B))=A. % 1.88/2.14 ** KEPT (pick-wt=6): 199 [] proj2Add(add(A,B))=B. % 1.88/2.14 ---> New Demodulator: 200 [new_demod,199] proj2Add(add(A,B))=B. % 1.88/2.14 ** KEPT (pick-wt=6): 201 [] proj1Mul(mul(A,B))=A. % 1.88/2.14 ---> New Demodulator: 202 [new_demod,201] proj1Mul(mul(A,B))=A. % 1.88/2.14 ** KEPT (pick-wt=6): 203 [] proj2Mul(mul(A,B))=B. % 1.88/2.14 ---> New Demodulator: 204 [new_demod,203] proj2Mul(mul(A,B))=B. % 1.88/2.14 ** KEPT (pick-wt=5): 205 [] proj1Num(num(A))=A. % 1.88/2.14 ---> New Demodulator: 206 [new_demod,205] proj1Num(num(A))=A. % 1.88/2.14 ** KEPT (pick-wt=5): 207 [] proj1Left(left(A))=A. % 1.88/2.14 ---> New Demodulator: 208 [new_demod,207] proj1Left(left(A))=A. % 1.88/2.14 ** KEPT (pick-wt=5): 209 [] proj1Right(right(A))=A. % 1.88/2.14 ---> New Demodulator: 210 [new_demod,209] proj1Right(right(A))=A. % 1.88/2.14 ** KEPT (pick-wt=5): 211 [] append(nil,A)=A. % 1.88/2.14 ---> New Demodulator: 212 [new_demod,211] append(nil,A)=A. % 1.88/2.14 ** KEPT (pick-wt=11): 214 [copy,213,flip.1] cons(A,append(B,C))=append(cons(A,B),C). % 1.88/2.14 ---> New Demodulator: 215 [new_demod,214] cons(A,append(B,C))=append(cons(A,B),C). % 1.88/2.14 ** KEPT (pick-wt=5): 216 [] x2(z,z)=z. % 1.88/2.14 ---> New Demodulator: 217 [new_demod,216] x2(z,z)=z. % 1.88/2.14 ** KEPT (pick-wt=6): 218 [] x2(z,s(A))=z. % 1.88/2.14 ---> New Demodulator: 219 [new_demod,218] x2(z,s(A))=z. % 1.88/2.14 ** KEPT (pick-wt=7): 220 [] x2(s(A),z)=s(A). % 1.88/2.14 ---> New Demodulator: 221 [new_demod,220] x2(s(A),z)=s(A). % 1.88/2.14 ** KEPT (pick-wt=9): 222 [] x2(s(A),s(B))=x2(A,B). % 1.88/2.14 ---> New Demodulator: 223 [new_demod,222] x2(s(A),s(B))=x2(A,B). % 1.88/2.14 ** KEPT (pick-wt=5): 224 [] min10(z)=left(dIG0). % 1.88/2.14 ---> New Demodulator: 225 [new_demod,224] min10(z)=left(dIG0). % 1.88/2.14 ** KEPT (pick-wt=6): 226 [] min10(s(z))=left(dIG1). % 1.88/2.14 ---> New Demodulator: 227 [new_demod,226] min10(s(z))=left(dIG1). % 1.88/2.14 ** KEPT (pick-wt=7): 228 [] min10(s(s(z)))=left(dIG2). % 1.88/2.14 ---> New Demodulator: 229 [new_demod,228] min10(s(s(z)))=left(dIG2). % 1.88/2.14 ** KEPT (pick-wt=8): 230 [] min10(s(s(s(z))))=left(dIG3). % 1.88/2.14 ---> New Demodulator: 231 [new_demod,230] min10(s(s(s(z))))=left(dIG3). % 1.88/2.14 ** KEPT (pick-wt=9): 232 [] min10(s(s(s(s(z)))))=left(dIG4). % 1.88/2.14 ---> New Demodulator: 233 [new_demod,232] min10(s(s(s(s(z)))))=left(dIG4). % 1.88/2.14 ** KEPT (pick-wt=10): 234 [] min10(s(s(s(s(s(z))))))=left(dIG5). % 1.88/2.14 ---> New Demodulator: 235 [new_demod,234] min10(s(s(s(s(s(z))))))=left(dIG5). % 1.88/2.14 ** KEPT (pick-wt=11): 236 [] min10(s(s(s(s(s(s(z)))))))=left(dIG6). % 1.88/2.14 ---> New Demodulator: 237 [new_demod,236] min10(s(s(s(s(s(s(z)))))))=left(dIG6). % 1.88/2.14 ** KEPT (pick-wt=12): 238 [] min10(s(s(s(s(s(s(s(z))))))))=left(dIG7). % 1.88/2.14 ---> New Demodulator: 239 [new_demod,238] min10(s(s(s(s(s(s(s(z))))))))=left(dIG7). % 1.88/2.14 ** KEPT (pick-wt=13): 240 [] min10(s(s(s(s(s(s(s(s(z)))))))))=left(dIG8). % 1.88/2.14 ---> New Demodulator: 241 [new_demod,240] min10(s(s(s(s(s(s(s(s(z)))))))))=left(dIG8). % 1.88/2.14 ** KEPT (pick-wt=14): 242 [] min10(s(s(s(s(s(s(s(s(s(z))))))))))=left(dIG9). % 1.88/2.14 ---> New Demodulator: 243 [new_demod,242] min10(s(s(s(s(s(s(s(s(s(z))))))))))=left(dIG9). % 1.88/2.14 ** KEPT (pick-wt=17): 245 [copy,244,demod,223,223,223,223,223,223,223,223,223,223] min10(s(s(s(s(s(s(s(s(s(s(A)))))))))))=right(x2(A,z)). % 1.88/2.14 ---> New Demodulator: 246 [new_demod,245] min10(s(s(s(s(s(s(s(s(s(s(A)))))))))))=right(x2(A,z)). % 1.88/2.14 ** KEPT (pick-wt=5): 247 [] showNumnum(A,z)=A. % 1.88/2.14 ---> New Demodulator: 248 [new_demod,247] showNumnum(A,z)=A. % 1.88/2.14 ** KEPT (pick-wt=6): 249 [] showNum(z)=cons(dIG0,nil). % 1.88/2.14 ---> New Demodulator: 250 [new_demod,249] showNum(z)=cons(dIG0,nil). % 1.88/2.14 ** KEPT (pick-wt=8): 251 [] showNum(s(A))=showNumnum(nil,s(A)). % 1.88/2.14 ---> New Demodulator: 252 [new_demod,251] showNum(s(A))=showNumnum(nil,s(A)). % 1.88/2.14 ** KEPT (pick-wt=6): 253 [] show(x)=cons(cHARX,nil). % 1.88/2.14 ---> New Demodulator: 254 [new_demod,253] show(x)=cons(cHARX,nil). % 1.88/2.14 ** KEPT (pick-wt=14): 255 [] show(add(A,B))=append(show(A),append(cons(pLUS,nil),show(B))). % 1.88/2.14 ---> New Demodulator: 256 [new_demod,255] show(add(A,B))=append(show(A),append(cons(pLUS,nil),show(B))). % 1.88/2.14 ** KEPT (pick-wt=14): 257 [] show(mul(A,B))=append(showF(A),append(cons(mULT,nil),showF(B))). % 1.88/2.14 ** KEPT (pick-wt=6): 259 [copy,258,flip.1] showNum(A)=show(num(A)). % 1.88/2.14 ---> New Demodulator: 260 [new_demod,259] showNum(A)=show(num(A)). % 1.88/2.14 ** KEPT (pick-wt=12): 262 [copy,261,flip.1] add(proj1Add(A),proj2Add(A))=A|showF(A)=show(A). % 1.88/2.14 ** KEPT (pick-wt=20): 264 [copy,263,demod,256,215,215] showF(add(A,B))=append(append(cons(pAR1,show(A)),append(cons(pLUS,nil),show(B))),cons(pAR2,nil)). % 1.88/2.14 ---> New Demodulator: 265 [new_demod,264] showF(add(A,B))=append(append(cons(pAR1,show(A)),append(cons(pLUS,nil),show(B))),cons(pAR2,nil)). % 1.88/2.14 Following clause subsumed by 186 during input processing: 0 [copy,186,flip.1] A=A. % 1.88/2.14 >>>> Starting back demodulation with 188. % 1.88/2.14 >>>> Starting back demodulation with 190. % 1.88/2.14 >>>> Starting back demodulation with 192. % 1.88/2.14 >>>> Starting back demodulation with 194. % 1.88/2.14 >>>> Starting back demodulation with 196. % 2.48/2.75 >>>> Starting back demodulation with 198. % 2.48/2.75 >>>> Starting back demodulation with 200. % 2.48/2.75 >>>> Starting back demodulation with 202. % 2.48/2.75 >>>> Starting back demodulation with 204. % 2.48/2.75 >>>> Starting back demodulation with 206. % 2.48/2.75 >>>> Starting back demodulation with 208. % 2.48/2.75 >>>> Starting back demodulation with 210. % 2.48/2.75 >>>> Starting back demodulation with 212. % 2.48/2.75 >>>> Starting back demodulation with 215. % 2.48/2.75 >>>> Starting back demodulation with 217. % 2.48/2.75 >>>> Starting back demodulation with 219. % 2.48/2.75 >>>> Starting back demodulation with 221. % 2.48/2.75 >>>> Starting back demodulation with 223. % 2.48/2.75 >>>> Starting back demodulation with 225. % 2.48/2.75 >>>> Starting back demodulation with 227. % 2.48/2.75 >>>> Starting back demodulation with 229. % 2.48/2.75 >>>> Starting back demodulation with 231. % 2.48/2.75 >>>> Starting back demodulation with 233. % 2.48/2.75 >>>> Starting back demodulation with 235. % 2.48/2.75 >>>> Starting back demodulation with 237. % 2.48/2.75 >>>> Starting back demodulation with 239. % 2.48/2.75 >>>> Starting back demodulation with 241. % 2.48/2.75 >>>> Starting back demodulation with 243. % 2.48/2.75 >>>> Starting back demodulation with 246. % 2.48/2.75 >>>> Starting back demodulation with 248. % 2.48/2.75 >>>> Starting back demodulation with 250. % 2.48/2.75 >>>> Starting back demodulation with 252. % 2.48/2.75 >>>> Starting back demodulation with 254. % 2.48/2.75 >>>> Starting back demodulation with 256. % 2.48/2.75 ** KEPT (pick-wt=14): 266 [copy,257,flip.1] append(showF(A),append(cons(mULT,nil),showF(B)))=show(mul(A,B)). % 2.48/2.75 >>>> Starting back demodulation with 260. % 2.48/2.75 >> back demodulating 251 with 260. % 2.48/2.75 >> back demodulating 249 with 260. % 2.48/2.75 >>>> Starting back demodulation with 265. % 2.48/2.75 Following clause subsumed by 257 during input processing: 0 [copy,266,flip.1] show(mul(A,B))=append(showF(A),append(cons(mULT,nil),showF(B))). % 2.48/2.75 >>>> Starting back demodulation with 268. % 2.48/2.75 >>>> Starting back demodulation with 270. % 2.48/2.75 % 2.48/2.75 ======= end of input processing ======= % 2.48/2.75 % 2.48/2.75 =========== start of search =========== % 2.48/2.75 % 2.48/2.75 % 2.48/2.75 Resetting weight limit to 10. % 2.48/2.75 % 2.48/2.75 % 2.48/2.75 Resetting weight limit to 10. % 2.48/2.75 % 2.48/2.75 sos_size=283 % 2.48/2.75 % 2.48/2.75 Search stopped because sos empty. % 2.48/2.75 % 2.48/2.75 % 2.48/2.75 Search stopped because sos empty. % 2.48/2.75 % 2.48/2.75 ============ end of search ============ % 2.48/2.75 % 2.48/2.75 -------------- statistics ------------- % 2.48/2.75 clauses given 1708 % 2.48/2.75 clauses generated 142314 % 2.48/2.75 clauses kept 1844 % 2.48/2.75 clauses forward subsumed 9277 % 2.48/2.75 clauses back subsumed 32 % 2.48/2.75 Kbytes malloced 6835 % 2.48/2.75 % 2.48/2.75 ----------- times (seconds) ----------- % 2.48/2.75 user CPU time 0.61 (0 hr, 0 min, 0 sec) % 2.48/2.75 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 2.48/2.75 wall-clock time 2 (0 hr, 0 min, 2 sec) % 2.48/2.75 % 2.48/2.75 Process 13812 finished Tue May 5 11:37:18 2026 % 2.48/2.75 Otter interrupted % 2.48/2.75 PROOF NOT FOUND %------------------------------------------------------------------------------