% LAWS CONCERNING THE RELATION "leq" Proof of Lemma A1 (cancellation law, proved without definitional extensions): ----> UNIT CONFLICT at 0.23 sec ----> 195 [binary,193.1,3.1] $F. Length of proof is 10. Level of proof is 4. ---------------- PROOF ---------------- 3 [] $c2!=$c1. 6,5 [] pluz(pluz(x,y),z)=pluz(x,pluz(y,z)). 7 [] pluz(x,e)=x. 9 [] pluz(x,rvz(x))=e. 11 [] pluz(x,y)=pluz(y,x). 13 [] pluz($c3,$c2)=pluz($c3,$c1). 39 [para_from,9.1.1,5.1.1.1,flip.1] pluz(x,pluz(rvz(x),y))=pluz(e,y). 42 [para_into,11.1.1,9.1.1,flip.1] pluz(rvz(x),x)=e. 45,44 [para_into,11.1.1,7.1.1,flip.1] pluz(e,x)=x. 48 [back_demod,39,demod,45] pluz(x,pluz(rvz(x),y))=y. 56 [para_from,42.1.1,5.1.1.1,demod,45,flip.1] pluz(rvz(x),pluz(x,y))=y. 60 [para_into,13.1.1,11.1.1,flip.1] pluz($c3,$c1)=pluz($c2,$c3). 89 [para_into,60.1.1,11.1.1,flip.1] pluz($c2,$c3)=pluz($c1,$c3). 95 [para_into,89.1.1,11.1.1] pluz($c3,$c2)=pluz($c1,$c3). 162,161 [para_into,48.1.1,11.1.1,demod,6] pluz(rvz(x),pluz(y,x))=y. 193 [para_into,56.1.1.2,95.1.1,demod,162,flip.1] $c2=$c1. 195 [binary,193.1,3.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 22 clauses generated 433 clauses kept 171 clauses forward subsumed 298 clauses back subsumed 10 Kbytes malloced 191 ----------- times (seconds) ----------- user CPU time 0.43 (0 hr, 0 min, 0 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 0 (0 hr, 0 min, 0 sec) hyper_res time 0.00 para_into time 0.00 para_from time 0.00 for_sub time 0.03 back_sub time 0.00 conflict time 0.13 demod time 0.02 The job finished Sun Nov 10 13:42:44 2002 Proof of Lemma B (proved without definitional extensions): ----> UNIT CONFLICT at 689.37 sec ----> 7698 [binary,7696.1,4.1] $F. Length of proof is 8. Level of proof is 4. ---------------- PROOF ---------------- 4 [] rvz(pluz($c2,rvz($c1)))!=pluz($c1,rvz($c2)). 6 [] pluz(pluz(x,y),z)=pluz(x,pluz(y,z)). 9,8 [] pluz(x,e)=x. 10 [] pluz(x,rvz(x))=e. 12 [] pluz(x,y)=pluz(y,x). 45 [para_into,10.1.1,6.1.1] pluz(x,pluz(y,rvz(pluz(x,y))))=e. 48 [para_from,10.1.1,6.1.1.1,flip.1] pluz(x,pluz(rvz(x),y))=pluz(e,y). 52 [para_into,12.1.1,10.1.1,flip.1] pluz(rvz(x),x)=e. 55,54 [para_into,12.1.1,8.1.1,flip.1] pluz(e,x)=x. 59 [back_demod,48,demod,55] pluz(x,pluz(rvz(x),y))=y. 73 [para_from,52.1.1,6.1.1.1,demod,55,flip.1] pluz(rvz(x),pluz(x,y))=y. 2798 [para_from,45.1.1,73.1.1.2,demod,9,flip.1] pluz(x,rvz(pluz(y,x)))=rvz(y). 7696 [para_from,2798.1.1,59.1.1.2,flip.1] rvz(pluz(x,rvz(y)))=pluz(y,rvz(x)). 7698 [binary,7696.1,4.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 298 clauses generated 79933 clauses kept 7662 clauses forward subsumed 21029 clauses back subsumed 372 Kbytes malloced 4297 ----------- times (seconds) ----------- user CPU time 689.65 (0 hr, 11 min, 29 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 688 (0 hr, 11 min, 28 sec) hyper_res time 1.77 para_into time 0.50 para_from time 0.70 for_sub time 192.52 back_sub time 53.98 conflict time 0.50 demod time 3.08 The job finished Sun Nov 10 13:27:46 2002 Proof of Lemma C (totality): ----> UNIT CONFLICT at 4.90 sec ----> 2025 [binary,2024.1,8.1] $F. Length of proof is 9. Level of proof is 4. ---------------- PROOF ---------------- 5 [] leq(x,y)| -nneg(pluz(y,rvz(x))). 6 [] pluz(x,y)!=pluz(x,z)|y=z. 7 [] -leq($c2,$c1). 8 [] -leq($c1,$c2). 13,12 [] pluz(x,e)=x. 14 [] pluz(x,rvz(x))=e. 16 [] pluz(x,y)=pluz(y,x). 17 [] nneg(x)|nneg(rvz(x)). 21,20 [] rvz(pluz(x,rvz(y)))=pluz(y,rvz(x)). 35 [para_into,12.1.1,6.2.1,demod,13] x=y|pluz(z,y)!=pluz(z,x). 41 [hyper,17,5,demod,21] nneg(pluz(x,rvz(y)))|leq(x,y). 70,69 [para_into,16.1.1,12.1.1,flip.1] pluz(e,x)=x. 87,86 [para_into,69.1.1,14.1.1,flip.1] rvz(e)=e. 128,127 [para_into,20.1.1.1,69.1.1,demod,87,13] rvz(rvz(x))=x. 1360 [para_into,35.2.1,69.1.1,demod,70] x=y|y!=x. 1510 [para_from,1360.1.1,7.1.1] -leq(x,$c1)|x!=$c2. 1982 [hyper,41,5] leq(x,y)|leq(y,x). 2024 [hyper,1982,1510,127,demod,128] leq($c1,$c2). 2025 [binary,2024.1,8.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 72 clauses generated 3567 clauses kept 2004 clauses forward subsumed 1557 clauses back subsumed 36 Kbytes malloced 1086 ----------- times (seconds) ----------- user CPU time 5.07 (0 hr, 0 min, 5 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 5 (0 hr, 0 min, 5 sec) hyper_res time 0.03 para_into time 0.00 para_from time 0.05 for_sub time 1.90 back_sub time 1.40 conflict time 0.13 demod time 0.03 The job finished Sun Nov 10 13:50:55 2002 Proof of Lemma D (reflexivity): ----> UNIT CONFLICT at 0.02 sec ----> 23 [binary,22.1,7.1] $F. Length of proof is 1. Level of proof is 1. ---------------- PROOF ---------------- 1 [] -nneg(x)| -nneg(y)|nneg(pluz(x,y)). 2 [] -nneg(x)| -nneg(rvz(x))|x=e. 7 [] -leq($c1,$c1). 21 [] leq(x,y)|leq(y,x). 22 [factor,21,1,2] leq(x,x). 23 [binary,22.1,7.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 0 clauses generated 2 clauses kept 17 clauses forward subsumed 1 clauses back subsumed 0 Kbytes malloced 79 ----------- times (seconds) ----------- user CPU time 0.32 (0 hr, 0 min, 0 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 0 (0 hr, 0 min, 0 sec) hyper_res time 0.00 para_into time 0.00 para_from time 0.00 for_sub time 0.00 back_sub time 0.00 conflict time 0.23 demod time 0.00 The job finished Sun Nov 10 13:51:53 2002 Proof of Lemma E (transitivity): ----> UNIT CONFLICT at 153.30 sec ----> 9506 [binary,9504.1,29.1] $F. Length of proof is 15. Level of proof is 7. ---------------- PROOF ---------------- 2 [] -nneg(x)| -nneg(rvz(x))|x=e. 3 [] -nneg(x)|abs(x)=x. 4 [] -leq(x,y)|nneg(pluz(y,rvz(x))). 6 [] pluz(x,y)!=pluz(x,z)|y=z. 8 [] $c3!=$c2. 13,12 [] pluz(x,e)=x. 15,14 [] pluz(x,rvz(x))=e. 16 [] pluz(x,y)=pluz(y,x). 20 [] rvz(pluz(x,rvz(y)))=pluz(y,rvz(x)). 23 [] leq(x,x). 24 [] leq($c3,$c2). 25 [] leq($c2,$c1). 27,26 [] $c3=$c1. 28 [back_demod,24,demod,27] leq($c1,$c2). 29 [back_demod,8,demod,27,flip.1] $c2!=$c1. 40 [hyper,23,4,demod,15] nneg(e). 42,41 [hyper,40,3] abs(e)=e. 44 [hyper,25,4] nneg(pluz($c1,rvz($c2))). 60 [hyper,28,4] nneg(pluz($c2,rvz($c1))). 75 [para_from,14.1.1,6.1.1,flip.1] pluz(x,y)!=e|rvz(x)=y. 93 [hyper,44,3] abs(pluz($c1,rvz($c2)))=pluz($c1,rvz($c2)). 129 [para_into,16.1.1,12.1.1,flip.1] pluz(e,x)=x. 148,147 [para_into,129.1.1,14.1.1,flip.1] rvz(e)=e. 331,330 [para_into,20.1.1.1,129.1.1,demod,148,13] rvz(rvz(x))=x. 358,357 [para_from,330.1.1,20.1.1.1.2] rvz(pluz(x,y))=pluz(rvz(y),rvz(x)). 9426 [para_into,93.1.1.1,2.3.1,demod,42,358,331,unit_del,44,60,flip.1] pluz($c1,rvz($c2))=e. 9444 [hyper,9426,75,flip.1] rvz($c2)=rvz($c1). 9504 [para_from,9444.1.1,330.1.1.1,demod,331,flip.1] $c2=$c1. 9506 [binary,9504.1,29.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 204 clauses generated 37506 clauses kept 9475 clauses forward subsumed 13127 clauses back subsumed 518 Kbytes malloced 4345 ----------- times (seconds) ----------- user CPU time 153.52 (0 hr, 2 min, 33 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 153 (0 hr, 2 min, 33 sec) hyper_res time 0.60 para_into time 0.08 para_from time 0.10 for_sub time 70.15 back_sub time 19.67 conflict time 0.17 demod time 0.93 The job finished Sun Nov 10 13:56:19 2002 Proof of Lemma E1 (transitivity): ----> UNIT CONFLICT at 153.30 sec ----> 9506 [binary,9504.1,29.1] $F. Length of proof is 15. Level of proof is 7. ---------------- PROOF ---------------- 2 [] -nneg(x)| -nneg(rvz(x))|x=e. 3 [] -nneg(x)|abs(x)=x. 4 [] -leq(x,y)|nneg(pluz(y,rvz(x))). 6 [] pluz(x,y)!=pluz(x,z)|y=z. 8 [] $c3!=$c2. 13,12 [] pluz(x,e)=x. 15,14 [] pluz(x,rvz(x))=e. 16 [] pluz(x,y)=pluz(y,x). 20 [] rvz(pluz(x,rvz(y)))=pluz(y,rvz(x)). 23 [] leq(x,x). 24 [] leq($c3,$c2). 25 [] leq($c2,$c1). 27,26 [] $c3=$c1. 28 [back_demod,24,demod,27] leq($c1,$c2). 29 [back_demod,8,demod,27,flip.1] $c2!=$c1. 40 [hyper,23,4,demod,15] nneg(e). 42,41 [hyper,40,3] abs(e)=e. 44 [hyper,25,4] nneg(pluz($c1,rvz($c2))). 60 [hyper,28,4] nneg(pluz($c2,rvz($c1))). 75 [para_from,14.1.1,6.1.1,flip.1] pluz(x,y)!=e|rvz(x)=y. 93 [hyper,44,3] abs(pluz($c1,rvz($c2)))=pluz($c1,rvz($c2)). 129 [para_into,16.1.1,12.1.1,flip.1] pluz(e,x)=x. 148,147 [para_into,129.1.1,14.1.1,flip.1] rvz(e)=e. 331,330 [para_into,20.1.1.1,129.1.1,demod,148,13] rvz(rvz(x))=x. 358,357 [para_from,330.1.1,20.1.1.1.2] rvz(pluz(x,y))=pluz(rvz(y),rvz(x)). 9426 [para_into,93.1.1.1,2.3.1,demod,42,358,331,unit_del,44,60,flip.1] pluz($c1,rvz($c2))=e. 9444 [hyper,9426,75,flip.1] rvz($c2)=rvz($c1). 9504 [para_from,9444.1.1,330.1.1.1,demod,331,flip.1] $c2=$c1. 9506 [binary,9504.1,29.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 204 clauses generated 37506 clauses kept 9475 clauses forward subsumed 13127 clauses back subsumed 518 Kbytes malloced 4345 ----------- times (seconds) ----------- user CPU time 153.52 (0 hr, 2 min, 33 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 153 (0 hr, 2 min, 33 sec) hyper_res time 0.60 para_into time 0.08 para_from time 0.10 for_sub time 70.15 back_sub time 19.67 conflict time 0.17 demod time 0.93 The job finished Sun Nov 10 13:56:19 2002 Proof of Lemma E2 (transitivity): ----> UNIT CONFLICT at 0.13 sec ----> 77 [binary,75.1,9.1] $F. Length of proof is 3. Level of proof is 2. ---------------- PROOF ---------------- 8 [] -leq(x,y)|x=y| -leq(y,z)|x!=z. 9 [] $c2!=$c1. 13 [] pluz(x,e)=x. 25 [] leq($c3,$c2). 26 [] leq($c2,$c1). 28,27 [] $c3=$c1. 29 [back_demod,25,demod,28] leq($c1,$c2). 61 [para_into,13.1.1,13.1.1] x=x. 75 [hyper,61,8,29,26,flip.1] $c2=$c1. 77 [binary,75.1,9.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 8 clauses generated 80 clauses kept 67 clauses forward subsumed 37 clauses back subsumed 9 Kbytes malloced 127 ----------- times (seconds) ----------- user CPU time 0.50 (0 hr, 0 min, 0 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 1 (0 hr, 0 min, 1 sec) hyper_res time 0.00 para_into time 0.00 para_from time 0.00 for_sub time 0.02 back_sub time 0.00 conflict time 0.30 demod time 0.00 The job finished Sun Nov 10 14:06:53 2002 Proof of Lemma F (additivity): ----> UNIT CONFLICT at 11.12 sec ----> 2965 [binary,2964.1,18.1] $F. Length of proof is 17. Level of proof is 8. ---------------- PROOF ---------------- 1 [] -nneg(x)| -nneg(y)|nneg(pluz(x,y)). 3 [] -nneg(x)|abs(x)=x. 4 [] -leq(x,y)|nneg(pluz(y,rvz(x))). 5 [] leq(x,y)| -nneg(pluz(y,rvz(x))). 8 [] -leq(x,y)|x=y| -leq(y,z)|x!=z. 9 [] -leq(x,y)| -leq(y,z)|y=z|x!=z. 10 [] -leq(pluz($c3,$c1),pluz($c2,$c1)). 12 [] pluz(pluz(x,y),z)=pluz(x,pluz(y,z)). 15,14 [] pluz(x,e)=x. 16 [] pluz(x,rvz(x))=e. 18 [] pluz(x,y)=pluz(y,x). 22 [] rvz(pluz(x,rvz(y)))=pluz(y,rvz(x)). 24 [] leq(x,y)|leq(y,x). 25 [] leq(x,x). 26 [] leq($c3,$c2). 38 [para_from,12.1.1,4.2.1] -leq(x,pluz(y,z))|nneg(pluz(y,pluz(z,rvz(x)))). 68 [para_into,14.1.1,14.1.1] x=x. 125 [para_from,16.1.1,12.1.1.1,flip.1] pluz(x,pluz(rvz(x),y))=pluz(e,y). 131,130 [para_into,18.1.1,14.1.1,flip.1] pluz(e,x)=x. 138,137 [back_demod,125,demod,131] pluz(x,pluz(rvz(x),y))=y. 144 [para_from,18.1.1,10.1.1] -leq(pluz($c1,$c3),pluz($c2,$c1)). 153,152 [para_into,130.1.1,16.1.1,flip.1] rvz(e)=e. 279 [hyper,24,10] leq(pluz($c2,$c1),pluz($c3,$c1)). 322 [para_into,22.1.1.1,130.1.1,demod,153,15] rvz(rvz(x))=x. 353,352 [para_from,322.1.1,22.1.1.1.2] rvz(pluz(x,y))=pluz(rvz(y),rvz(x)). 1610 [hyper,144,24] leq(pluz($c2,$c1),pluz($c1,$c3)). 1644 [para_into,144.1.2,8.2.1] -leq(pluz($c1,$c3),x)| -leq(pluz($c2,$c1),x)| -leq(x,y)|pluz($c2,$c1)!=y. 1651 [factor,1644,1,3,unit_del,25,1610] pluz($c2,$c1)!=pluz($c1,$c3). 2437 [hyper,279,38,demod,353,138] nneg(pluz($c3,rvz($c2))). 2552 [hyper,2437,5] leq($c2,$c3). 2602,2601 [hyper,2552,9,26,68,flip.1] $c3=$c2. 2964 [back_demod,1651,demod,2602] pluz($c2,$c1)!=pluz($c1,$c2). 2965 [binary,2964.1,18.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 68 clauses generated 5594 clauses kept 2940 clauses forward subsumed 3246 clauses back subsumed 80 Kbytes malloced 1621 ----------- times (seconds) ----------- user CPU time 11.40 (0 hr, 0 min, 11 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 11 (0 hr, 0 min, 11 sec) hyper_res time 0.02 para_into time 0.07 para_from time 0.02 for_sub time 4.88 back_sub time 1.12 conflict time 0.25 demod time 0.05 The job finished Sun Nov 10 14:07:40 2002 Proof of Lemma A2 (cancellation law): ----> UNIT CONFLICT at 10.83 sec ----> 2175 [binary,2173.1,11.1] $F. Length of proof is 3. Level of proof is 3. ---------------- PROOF ---------------- 6 [] pluz(x,y)!=pluz(x,z)|y=z. 11 [] $c3!=$c2. 19 [] pluz(x,y)=pluz(y,x). 27 [] pluz($c3,$c1)=pluz($c2,$c1). 357 [para_into,27.1.1,19.1.1,flip.1] pluz($c2,$c1)=pluz($c1,$c3). 1638 [para_into,357.1.1,19.1.1,flip.1] pluz($c1,$c3)=pluz($c1,$c2). 2173 [hyper,1638,6] $c3=$c2. 2175 [binary,2173.1,11.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 69 clauses generated 6597 clauses kept 2150 clauses forward subsumed 4511 clauses back subsumed 45 Kbytes malloced 1334 ----------- times (seconds) ----------- user CPU time 11.12 (0 hr, 0 min, 11 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 11 (0 hr, 0 min, 11 sec) hyper_res time 0.08 para_into time 0.00 para_from time 0.02 for_sub time 3.22 back_sub time 0.68 conflict time 0.22 demod time 0.17 The job finished Sun Nov 10 14:08:28 2002 Proof of Lemma F1 (strict additivity): ----> UNIT CONFLICT at 0.38 sec ----> 450 [binary,448.1,12.1] $F. Length of proof is 1. Level of proof is 1. ---------------- PROOF ---------------- 11 [] pluz(x,y)!=pluz(z,y)|x=z. 12 [] $c3!=$c2. 29 [] pluz($c3,$c1)=pluz($c2,$c1). 448 [hyper,29,11] $c3=$c2. 450 [binary,448.1,12.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 26 clauses generated 963 clauses kept 425 clauses forward subsumed 603 clauses back subsumed 15 Kbytes malloced 311 ----------- times (seconds) ----------- user CPU time 0.62 (0 hr, 0 min, 0 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 1 (0 hr, 0 min, 1 sec) hyper_res time 0.02 para_into time 0.00 para_from time 0.00 for_sub time 0.13 back_sub time 0.00 conflict time 0.15 demod time 0.02 The job finished Sun Nov 10 14:10:05 2002 % LAWS CONCERNING THE OPERATIONS "abs" and "nneg": Proof of Lemma 1: ----> UNIT CONFLICT at 0.12 sec ----> 51 [binary,49.1,28.1] $F. Length of proof is 3. Level of proof is 2. ---------------- PROOF ---------------- 3 [] -nneg(x)|abs(x)=x. 4 [] -leq(x,y)|nneg(pluz(y,rvz(x))). 12 [] abs(pluz($c1,rvz($c1)))!=e. 19,18 [] pluz(x,rvz(x))=e. 27 [] leq(x,x). 28 [back_demod,12,demod,19] abs(e)!=e. 48 [hyper,27,4,demod,19] nneg(e). 49 [hyper,48,3] abs(e)=e. 51 [binary,49.1,28.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 3 clauses generated 38 clauses kept 44 clauses forward subsumed 17 clauses back subsumed 1 Kbytes malloced 111 ----------- times (seconds) ----------- user CPU time 0.33 (0 hr, 0 min, 0 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 0 (0 hr, 0 min, 0 sec) hyper_res time 0.00 para_into time 0.00 para_from time 0.00 for_sub time 0.00 back_sub time 0.00 conflict time 0.15 demod time 0.00 The job finished Sun Nov 10 14:11:20 2002 Proof of Lemma 2: ----> UNIT CONFLICT at 4.82 sec ----> 1902 [binary,1901.1,27.1] $F. Length of proof is 14. Level of proof is 8. ---------------- PROOF ---------------- 1 [] -nneg(x)| -nneg(y)|nneg(pluz(x,y)). 2 [] -nneg(x)| -nneg(rvz(x))|x=e. 3 [] -nneg(x)|abs(x)=x. 5 [] leq(x,y)| -nneg(pluz(y,rvz(x))). 12 [] -leq($c1,abs($c1)). 13 [factor,1,1,2] -nneg(x)|nneg(pluz(x,x)). 17,16 [] pluz(x,e)=x. 19,18 [] pluz(x,rvz(x))=e. 20 [] pluz(x,y)=pluz(y,x). 21 [] nneg(x)|nneg(rvz(x)). 22 [] nneg(x)|abs(x)=rvz(x). 23 [copy,22,flip.2] nneg(x)|rvz(x)=abs(x). 24 [] rvz(pluz(x,rvz(y)))=pluz(y,rvz(x)). 27 [] leq(x,x). 28 [] abs(pluz(x,rvz(x)))=e. 29 [copy,28,demod,19] abs(e)=e. 77 [hyper,21,13] nneg(rvz(x))|nneg(pluz(x,x)). 79 [hyper,21,3] nneg(rvz(x))|abs(x)=x. 119 [para_into,20.1.1,16.1.1,flip.1] pluz(e,x)=x. 164,163 [para_into,119.1.1,18.1.1,flip.1] rvz(e)=e. 304,303 [para_into,24.1.1.1,119.1.1,demod,164,17] rvz(rvz(x))=x. 1038 [hyper,77,5,demod,304] nneg(x)|leq(x,rvz(x)). 1144 [para_into,1038.2.2,23.2.1,factor_simp] nneg(x)|leq(x,abs(x)). 1396 [para_from,79.2.1,12.1.2,unit_del,27] nneg(rvz($c1)). 1403,1402 [hyper,1396,2,1144,unit_del,12,flip.1] e=$c1. 1869,1868 [back_demod,29,demod,1403,1403] abs($c1)=$c1. 1901 [back_demod,12,demod,1869] -leq($c1,$c1). 1902 [binary,1901.1,27.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 49 clauses generated 3066 clauses kept 1871 clauses forward subsumed 1848 clauses back subsumed 40 Kbytes malloced 1118 ----------- times (seconds) ----------- user CPU time 5.07 (0 hr, 0 min, 5 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 5 (0 hr, 0 min, 5 sec) hyper_res time 0.00 para_into time 0.00 para_from time 0.02 for_sub time 1.88 back_sub time 0.60 conflict time 0.18 demod time 0.08 The job finished Sun Nov 10 14:11:55 2002 Proof of Lemma 3: ----> UNIT CONFLICT at 4.68 sec ----> 1831 [binary,1830.1,65.1] $F. Length of proof is 16. Level of proof is 8. ---------------- PROOF ---------------- 3 [] -nneg(x)|abs(x)=x. 4 [] -leq(x,y)|nneg(pluz(y,rvz(x))). 5 [] leq(x,y)| -nneg(pluz(y,rvz(x))). 11 [] pluz(x,y)!=pluz(z,y)|x=z. 12 [] abs(abs($c1))!=abs($c1). 17,16 [] pluz(x,e)=x. 18 [] pluz(x,rvz(x))=e. 20 [] pluz(x,y)=pluz(y,x). 21 [] nneg(x)|nneg(rvz(x)). 22 [] nneg(x)|abs(x)=rvz(x). 23 [copy,22,flip.2] nneg(x)|rvz(x)=abs(x). 24 [] rvz(pluz(x,rvz(y)))=pluz(y,rvz(x)). 65 [hyper,16,11,demod,17] x=x. 88 [hyper,21,3] nneg(rvz(x))|abs(x)=x. 189 [para_into,20.1.1,16.1.1,flip.1] pluz(e,x)=x. 242,241 [para_into,189.1.1,18.1.1,flip.1] rvz(e)=e. 245 [para_from,189.1.1,5.2.1] leq(x,e)| -nneg(rvz(x)). 246 [para_from,189.1.1,4.2.1] -leq(x,e)|nneg(rvz(x)). 321,320 [para_into,24.1.1.1,189.1.1,demod,242,17] rvz(rvz(x))=x. 504 [para_into,245.2.1,320.1.1] leq(rvz(x),e)| -nneg(x). 513 [para_into,246.2.1,320.1.1] -leq(rvz(x),e)|nneg(x). 991 [para_into,513.1.1,23.2.1,factor_simp] -leq(abs(x),e)|nneg(x). 1526 [para_from,88.2.1,12.1.1,unit_del,65] nneg(rvz(abs($c1))). 1599 [hyper,1526,504,demod,321] leq(abs($c1),e). 1750 [hyper,1599,991] nneg($c1). 1773,1772 [hyper,1750,3] abs($c1)=$c1. 1830 [back_demod,12,demod,1773,1773,1773] $c1!=$c1. 1831 [binary,1830.1,65.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 59 clauses generated 3879 clauses kept 1800 clauses forward subsumed 2201 clauses back subsumed 52 Kbytes malloced 1174 ----------- times (seconds) ----------- user CPU time 4.90 (0 hr, 0 min, 4 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 5 (0 hr, 0 min, 5 sec) hyper_res time 0.05 para_into time 0.00 para_from time 0.02 for_sub time 1.68 back_sub time 0.52 conflict time 0.13 demod time 0.10 The job finished Sun Nov 10 14:12:36 2002 Proof of Lemma 4: ----> UNIT CONFLICT at 0.48 sec ----> 505 [binary,503.1,419.1] $F. Length of proof is 13. Level of proof is 6. ---------------- PROOF ---------------- 3 [] -nneg(x)|abs(x)=x. 11 [] pluz(x,y)!=pluz(z,y)|x=z. 12 [] abs($c1)!=e|$c1!=e. 13 [copy,12,flip.2] abs($c1)!=e|e!=$c1. 18,17 [] pluz(x,e)=x. 20,19 [] pluz(x,rvz(x))=e. 21 [] pluz(x,y)=pluz(y,x). 23 [] nneg(x)|abs(x)=rvz(x). 24 [copy,23,flip.2] nneg(x)|rvz(x)=abs(x). 25 [] rvz(pluz(x,rvz(y)))=pluz(y,rvz(x)). 29 [] abs(pluz(x,rvz(x)))=e. 30 [copy,29,demod,20] abs(e)=e. 35 [] abs($c1)=e|$c1=e. 36 [copy,35,flip.2] abs($c1)=e|e=$c1. 70 [hyper,17,11,demod,18] x=x. 127 [para_into,21.1.1,17.1.1,flip.1] pluz(e,x)=x. 154,153 [para_into,127.1.1,19.1.1,flip.1] rvz(e)=e. 291 [para_into,25.1.1.1,127.1.1,demod,154,18] rvz(rvz(x))=x. 418,417 [para_from,36.2.1,30.1.1.1,factor_simp] abs($c1)=e. 419 [back_demod,13,demod,418,unit_del,70] e!=$c1. 429 [para_into,417.1.1,3.2.1,unit_del,419] -nneg($c1). 432 [hyper,429,24,demod,418] rvz($c1)=e. 503 [para_from,432.1.1,291.1.1.1,demod,154] e=$c1. 505 [binary,503.1,419.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 32 clauses generated 1293 clauses kept 477 clauses forward subsumed 890 clauses back subsumed 75 Kbytes malloced 351 ----------- times (seconds) ----------- user CPU time 0.73 (0 hr, 0 min, 0 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 1 (0 hr, 0 min, 1 sec) hyper_res time 0.03 para_into time 0.00 para_from time 0.00 for_sub time 0.12 back_sub time 0.03 conflict time 0.18 demod time 0.03 The job finished Sun Nov 10 14:13:08 2002 Proof of Lemma 5: ----> UNIT CONFLICT at 0.27 sec ----> 360 [binary,359.1,70.1] $F. Length of proof is 12. Level of proof is 7. ---------------- PROOF ---------------- 2 [] -nneg(x)| -nneg(rvz(x))|x=e. 3 [] -nneg(x)|abs(x)=x. 11 [] pluz(x,y)!=pluz(z,y)|x=z. 14 [] abs(rvz($c1))!=abs($c1). 19,18 [] pluz(x,e)=x. 20 [] pluz(x,rvz(x))=e. 22 [] pluz(x,y)=pluz(y,x). 24 [] nneg(x)|abs(x)=rvz(x). 25 [copy,24,flip.2] nneg(x)|rvz(x)=abs(x). 26 [] rvz(pluz(x,rvz(y)))=pluz(y,rvz(x)). 35,34 [] abs(abs(x))=abs(x). 70 [hyper,18,11,demod,19] x=x. 131 [para_into,22.1.1,18.1.1,flip.1] pluz(e,x)=x. 160,159 [para_into,131.1.1,20.1.1,flip.1] rvz(e)=e. 202 [para_from,25.2.1,14.1.1.1,demod,35,unit_del,70] nneg($c1). 210,209 [hyper,202,3] abs($c1)=$c1. 211 [hyper,202,2,25,flip.1] e=$c1|rvz(rvz($c1))=abs(rvz($c1)). 219 [back_demod,14,demod,210] abs(rvz($c1))!=$c1. 273,272 [para_into,26.1.1.1,131.1.1,demod,160,19] rvz(rvz(x))=x. 289,288 [back_demod,211,demod,273,unit_del,219] e=$c1. 323,322 [back_demod,159,demod,289,289] rvz($c1)=$c1. 359 [back_demod,219,demod,323,210] $c1!=$c1. 360 [binary,359.1,70.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 21 clauses generated 504 clauses kept 332 clauses forward subsumed 286 clauses back subsumed 13 Kbytes malloced 263 ----------- times (seconds) ----------- user CPU time 0.48 (0 hr, 0 min, 0 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 0 (0 hr, 0 min, 0 sec) hyper_res time 0.00 para_into time 0.03 para_from time 0.00 for_sub time 0.07 back_sub time 0.00 conflict time 0.15 demod time 0.02 The job finished Sun Nov 10 14:15:32 2002 Proof of Lemma 6: ----> UNIT CONFLICT at 27.63 sec ----> 3710 [binary,3709.1,149.1] $F. Length of proof is 20. Level of proof is 8. ---------------- PROOF ---------------- 3 [] -nneg(x)|abs(x)=x. 5 [] leq(x,y)| -nneg(pluz(y,rvz(x))). 7 [] -leq(x,y)| -leq(y,z)|leq(x,z). 10 [] -leq(x,y)|leq(pluz(x,z),pluz(y,z)). 14 [] -leq(pluz($c2,$c1),pluz(abs($c2),abs($c1))). 19,18 [] pluz(x,e)=x. 20 [] pluz(x,rvz(x))=e. 22 [] pluz(x,y)=pluz(y,x). 23 [] nneg(x)|nneg(rvz(x)). 24 [] nneg(x)|abs(x)=rvz(x). 25 [copy,24,flip.2] nneg(x)|rvz(x)=abs(x). 26 [] rvz(pluz(x,rvz(y)))=pluz(y,rvz(x)). 33 [] leq(x,abs(x)). 34 [] abs(abs(x))=abs(x). 86 [hyper,33,10] leq(pluz(x,y),pluz(abs(x),y)). 97 [hyper,23,3] nneg(rvz(x))|abs(x)=x. 132,131 [para_into,22.1.1,18.1.1,flip.1] pluz(e,x)=x. 149 [para_from,22.1.1,14.1.1] -leq(pluz($c1,$c2),pluz(abs($c2),abs($c1))). 162,161 [para_into,131.1.1,20.1.1,flip.1] rvz(e)=e. 165 [para_from,131.1.1,5.2.1] leq(x,e)| -nneg(rvz(x)). 173 [para_from,161.1.1,5.2.1.2,demod,19] leq(e,x)| -nneg(x). 204 [para_from,25.2.1,23.2.1,factor_simp] nneg(x)|nneg(abs(x)). 285 [para_from,34.1.1,204.2.1,factor_simp] nneg(abs(x)). 296,295 [para_into,26.1.1.1,131.1.1,demod,162,19] rvz(rvz(x))=x. 316 [hyper,285,173] leq(e,abs(x)). 332 [hyper,316,10,demod,132] leq(x,pluz(abs(y),x)). 662 [para_into,165.2.1,295.1.1] leq(rvz(x),e)| -nneg(x). 1003 [para_into,332.1.2,22.1.1] leq(x,pluz(x,abs(y))). 1915 [para_from,97.2.1,14.1.2.2,unit_del,86] nneg(rvz($c1)). 1970 [hyper,1915,662,demod,296] leq($c1,e). 1976 [hyper,1970,10,demod,132] leq(pluz($c1,x),x). 2097 [hyper,1976,7,33] leq(pluz($c1,x),abs(x)). 3709 [hyper,2097,7,1003] leq(pluz($c1,x),pluz(abs(x),abs(y))). 3710 [binary,3709.1,149.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 118 clauses generated 10966 clauses kept 3675 clauses forward subsumed 7292 clauses back subsumed 194 Kbytes malloced 2292 ----------- times (seconds) ----------- user CPU time 28.00 (0 hr, 0 min, 28 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 27 (0 hr, 0 min, 27 sec) hyper_res time 0.18 para_into time 0.03 para_from time 0.02 for_sub time 9.60 back_sub time 2.67 conflict time 0.50 demod time 0.17 The job finished Sun Nov 10 14:17:47 2002 Proof of Lemma 7a (technical lemma, helpful to reach 7): ----> UNIT CONFLICT at 0.15 sec ----> 102 [binary,101.1,38.1] $F. Length of proof is 2. Level of proof is 2. ---------------- PROOF ---------------- 3 [] -nneg(x)|abs(x)=x. 14 [] -leq(abs(pluz($c2,$c1)),pluz(abs($c2),abs($c1))). 38 [] leq(pluz(x,y),pluz(abs(x),abs(y))). 39 [] nneg(pluz($c2,$c1)). 99,98 [hyper,39,3] abs(pluz($c2,$c1))=pluz($c2,$c1). 101 [back_demod,14,demod,99] -leq(pluz($c2,$c1),pluz(abs($c2),abs($c1))). 102 [binary,101.1,38.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 9 clauses generated 135 clauses kept 90 clauses forward subsumed 74 clauses back subsumed 9 Kbytes malloced 143 ----------- times (seconds) ----------- user CPU time 0.37 (0 hr, 0 min, 0 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 0 (0 hr, 0 min, 0 sec) hyper_res time 0.00 para_into time 0.00 para_from time 0.00 for_sub time 0.00 back_sub time 0.00 conflict time 0.15 demod time 0.00 The job finished Sun Nov 10 15:22:23 2002 Proof of Lemma 7b (technical lemma, helpful to reach 7): ----> UNIT CONFLICT at 0.47 sec ----> 559 [binary,558.1,407.1] $F. Length of proof is 12. Level of proof is 6. ---------------- PROOF ---------------- 3 [] -nneg(x)|abs(x)=x. 15 [] -nneg(pluz($c2,$c1)). 16 [] -nneg(pluz(rvz($c2),rvz($c1))). 21,20 [] pluz(x,e)=x. 22 [] pluz(x,rvz(x))=e. 24 [] pluz(x,y)=pluz(y,x). 25 [] nneg(x)|nneg(rvz(x)). 26 [] nneg(x)|abs(x)=rvz(x). 27 [copy,26,flip.2] nneg(x)|rvz(x)=abs(x). 28 [] rvz(pluz(x,rvz(y)))=pluz(y,rvz(x)). 36 [] abs(abs(x))=abs(x). 39,38 [] abs(rvz(x))=abs(x). 102 [hyper,25,15] nneg(rvz(pluz($c2,$c1))). 125 [hyper,102,3,demod,39,flip.1] rvz(pluz($c2,$c1))=abs(pluz($c2,$c1)). 197 [para_into,24.1.1,20.1.1,flip.1] pluz(e,x)=x. 216 [para_from,24.1.1,16.1.1] -nneg(pluz(rvz($c1),rvz($c2))). 312 [para_from,27.2.1,25.2.1,factor_simp] nneg(x)|nneg(abs(x)). 321,320 [para_into,197.1.1,22.1.1,flip.1] rvz(e)=e. 407 [para_into,312.2.1,36.1.1,factor_simp] nneg(abs(x)). 427 [para_into,28.1.1.1,197.1.1,demod,321,21] rvz(rvz(x))=x. 537,536 [para_from,427.1.1,28.1.1.1.2] rvz(pluz(x,y))=pluz(rvz(y),rvz(x)). 554,553 [back_demod,125,demod,537] pluz(rvz($c1),rvz($c2))=abs(pluz($c2,$c1)). 558 [back_demod,216,demod,554] -nneg(abs(pluz($c2,$c1))). 559 [binary,558.1,407.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 32 clauses generated 1398 clauses kept 527 clauses forward subsumed 960 clauses back subsumed 124 Kbytes malloced 351 ----------- times (seconds) ----------- user CPU time 0.70 (0 hr, 0 min, 0 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 1 (0 hr, 0 min, 1 sec) hyper_res time 0.00 para_into time 0.00 para_from time 0.00 for_sub time 0.12 back_sub time 0.03 conflict time 0.17 demod time 0.02 The job finished Sun Nov 10 15:23:20 2002 Proof of Lemma 7c (technical lemma, helpful to reach 7, proved without earlier laws on "leq"): ----> UNIT CONFLICT at 0.55 sec ----> 709 [binary,708.1,32.1] $F. Length of proof is 3. Level of proof is 2. ---------------- PROOF ---------------- 8 [] -nneg(pluz(x,y))|leq(abs(pluz(x,y)),pluz(abs(x),abs(y))). 9 [] -nneg(pluz($c2,$c1)). 10 [] -leq(abs(pluz(rvz($c2),rvz($c1))),pluz(abs(rvz($c2)),abs(rvz($c1)))). 29,28 [] abs(rvz(x))=abs(x). 31 [] nneg(pluz(x,y))|nneg(pluz(rvz(x),rvz(y))). 32 [back_demod,10,demod,29,29] -leq(abs(pluz(rvz($c2),rvz($c1))),pluz(abs($c2),abs($c1))). 295 [hyper,31,9] nneg(pluz(rvz($c2),rvz($c1))). 708 [hyper,295,8,demod,29,29] leq(abs(pluz(rvz($c2),rvz($c1))),pluz(abs($c2),abs($c1))). 709 [binary,708.1,32.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 63 clauses generated 1306 clauses kept 685 clauses forward subsumed 657 clauses back subsumed 86 Kbytes malloced 423 ----------- times (seconds) ----------- user CPU time 0.80 (0 hr, 0 min, 0 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 0 (0 hr, 0 min, 0 sec) hyper_res time 0.03 para_into time 0.00 para_from time 0.00 for_sub time 0.08 back_sub time 0.03 conflict time 0.17 demod time 0.03 The job finished Sun Nov 10 15:24:50 2002 Proof of Lemma 7d (technical lemma, helpful to reach 7): ----> UNIT CONFLICT at 0.70 sec ----> 803 [binary,802.1,219.1] $F. Length of proof is 11. Level of proof is 6. ---------------- PROOF ---------------- 3 [] -nneg(x)|abs(x)=x. 15 [] -nneg(pluz($c2,$c1)). 16 [] -leq(abs(pluz($c2,$c1)),pluz(abs($c2),abs($c1))). 21,20 [] pluz(x,e)=x. 22 [] pluz(x,rvz(x))=e. 24 [] pluz(x,y)=pluz(y,x). 25 [] nneg(x)|nneg(rvz(x)). 28 [] rvz(pluz(x,rvz(y)))=pluz(y,rvz(x)). 37,36 [] abs(abs(x))=abs(x). 39,38 [] abs(rvz(x))=abs(x). 42 [] nneg(pluz(x,y))|leq(abs(pluz(rvz(x),rvz(y))),pluz(abs(rvz(x)),abs(rvz(y)))). 43 [copy,42,demod,39,39] nneg(pluz(x,y))|leq(abs(pluz(rvz(x),rvz(y))),pluz(abs(x),abs(y))). 104 [hyper,25,15] nneg(rvz(pluz($c2,$c1))). 127 [hyper,104,3,demod,39,flip.1] rvz(pluz($c2,$c1))=abs(pluz($c2,$c1)). 200 [para_into,24.1.1,20.1.1,flip.1] pluz(e,x)=x. 219 [para_from,24.1.1,16.1.2] -leq(abs(pluz($c2,$c1)),pluz(abs($c1),abs($c2))). 222 [para_from,24.1.1,15.1.1] -nneg(pluz($c1,$c2)). 320,319 [para_into,200.1.1,22.1.1,flip.1] rvz(e)=e. 426 [para_into,28.1.1.1,200.1.1,demod,320,21] rvz(rvz(x))=x. 534,533 [para_from,426.1.1,28.1.1.1.2] rvz(pluz(x,y))=pluz(rvz(y),rvz(x)). 551,550 [back_demod,127,demod,534] pluz(rvz($c1),rvz($c2))=abs(pluz($c2,$c1)). 802 [hyper,43,222,demod,551,37] leq(abs(pluz($c2,$c1)),pluz(abs($c1),abs($c2))). 803 [binary,802.1,219.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 41 clauses generated 1880 clauses kept 770 clauses forward subsumed 1199 clauses back subsumed 126 Kbytes malloced 471 ----------- times (seconds) ----------- user CPU time 0.92 (0 hr, 0 min, 0 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 1 (0 hr, 0 min, 1 sec) hyper_res time 0.00 para_into time 0.02 para_from time 0.00 for_sub time 0.12 back_sub time 0.10 conflict time 0.15 demod time 0.02 The job finished Sun Nov 10 15:25:34 2002 Proof of Lemma 7: ----> UNIT CONFLICT at 0.97 sec ----> 875 [binary,874.1,15.1] $F. Length of proof is 1. Level of proof is 1. ---------------- PROOF ---------------- 14 [] -nneg(pluz(x,y))|leq(abs(pluz(x,y)),pluz(abs(x),abs(y))). 15 [] -leq(abs(pluz($c2,$c1)),pluz(abs($c2),abs($c1))). 43 [] nneg(pluz(x,y))|leq(abs(pluz(x,y)),pluz(abs(x),abs(y))). 874 [hyper,43,14,factor_simp] leq(abs(pluz(x,y)),pluz(abs(x),abs(y))). 875 [binary,874.1,15.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 41 clauses generated 1991 clauses kept 846 clauses forward subsumed 1209 clauses back subsumed 73 Kbytes malloced 527 ----------- times (seconds) ----------- user CPU time 1.18 (0 hr, 0 min, 1 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 1 (0 hr, 0 min, 1 sec) hyper_res time 0.05 para_into time 0.02 para_from time 0.00 for_sub time 0.27 back_sub time 0.13 conflict time 0.15 demod time 0.03 The job finished Sun Nov 10 15:31:04 2002 Proof of Lemma 8a (technical lemma, helpful to get 8, proved without the axioms): ----> UNIT CONFLICT at 0.58 sec ----> 628 [binary,627.1,81.1] $F. Length of proof is 7. Level of proof is 3. ---------------- PROOF ---------------- 11 [] pluz(x,y)!=pluz(z,y)|x=z. 15 [] pluz($c3,$c1)!=pluz(pluz($c3,rvz($c2)),pluz($c2,$c1)). 16 [copy,15,flip.1] pluz(pluz($c3,rvz($c2)),pluz($c2,$c1))!=pluz($c3,$c1). 19,18 [] pluz(pluz(x,y),z)=pluz(x,pluz(y,z)). 21,20 [] pluz(x,e)=x. 22 [] pluz(x,rvz(x))=e. 24 [] pluz(x,y)=pluz(y,x). 46 [back_demod,16,demod,19] pluz($c3,pluz(rvz($c2),pluz($c2,$c1)))!=pluz($c3,$c1). 81 [hyper,20,11,demod,21] x=x. 138 [para_into,24.1.1,22.1.1,flip.1] pluz(rvz(x),x)=e. 141,140 [para_into,24.1.1,20.1.1,flip.1] pluz(e,x)=x. 624,623 [para_from,138.1.1,18.1.1.1,demod,141,flip.1] pluz(rvz(x),pluz(x,y))=y. 627 [back_demod,46,demod,624] pluz($c3,$c1)!=pluz($c3,$c1). 628 [binary,627.1,81.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 34 clauses generated 1559 clauses kept 599 clauses forward subsumed 1018 clauses back subsumed 66 Kbytes malloced 399 ----------- times (seconds) ----------- user CPU time 0.82 (0 hr, 0 min, 0 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 1 (0 hr, 0 min, 1 sec) hyper_res time 0.05 para_into time 0.00 para_from time 0.00 for_sub time 0.10 back_sub time 0.05 conflict time 0.17 demod time 0.03 The job finished Sun Nov 10 15:34:07 2002 Proof of Lemma 8: ----> UNIT CONFLICT at 0.80 sec ----> 655 [binary,654.1,13.1] $F. Length of proof is 2. Level of proof is 2. ---------------- PROOF ---------------- 13 [] -leq(abs(pluz($c3,rvz($c1))),pluz(abs(pluz($c3,rvz($c2))),abs(pluz($c2,rvz($c1))))). 32 [] leq(abs(pluz(x,y)),pluz(abs(x),abs(y))). 33 [] pluz(x,y)=pluz(pluz(x,rvz(z)),pluz(z,y)). 34 [copy,33,flip.1] pluz(pluz(x,rvz(y)),pluz(y,z))=pluz(x,z). 654 [para_from,34.1.1,32.1.1.1] leq(abs(pluz(x,y)),pluz(abs(pluz(x,rvz(z))),abs(pluz(z,y)))). 655 [binary,654.1,13.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 36 clauses generated 1850 clauses kept 632 clauses forward subsumed 1251 clauses back subsumed 14 Kbytes malloced 455 ----------- times (seconds) ----------- user CPU time 1.02 (0 hr, 0 min, 1 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 1 (0 hr, 0 min, 1 sec) hyper_res time 0.00 para_into time 0.02 para_from time 0.00 for_sub time 0.17 back_sub time 0.03 conflict time 0.15 demod time 0.07 The job finished Sun Nov 10 15:40:40 2002 Proof of Lemma 9: ----> UNIT CONFLICT at 0.52 sec ----> 517 [binary,516.1,510.1] $F. Length of proof is 15. Level of proof is 8. ---------------- PROOF ---------------- 4 [] -leq(x,y)|nneg(pluz(y,rvz(x))). 5 [] leq(x,y)| -nneg(pluz(y,rvz(x))). 7 [] -leq(x,y)| -leq(y,z)|leq(x,z). 10 [] -leq(x,y)|leq(pluz(x,z),pluz(y,z)). 15 [] -nneg($c2). 16 [] -leq($c2,abs($c1))|$c2=abs($c1). 17 [copy,16,flip.2] -leq($c2,abs($c1))|abs($c1)=$c2. 22,21 [] pluz(x,e)=x. 23 [] pluz(x,rvz(x))=e. 25 [] pluz(x,y)=pluz(y,x). 26 [] nneg(x)|nneg(rvz(x)). 27 [] nneg(x)|abs(x)=rvz(x). 28 [copy,27,flip.2] nneg(x)|rvz(x)=abs(x). 31 [] leq(x,y)|leq(y,x). 37 [] abs(abs(x))=abs(x). 207,206 [para_into,25.1.1,21.1.1,flip.1] pluz(e,x)=x. 235 [para_into,206.1.1,23.1.1,flip.1] rvz(e)=e. 247 [para_from,235.1.1,5.2.1.2,demod,22] leq(e,x)| -nneg(x). 248 [para_from,235.1.1,4.2.1.2,demod,22] -leq(e,x)|nneg(x). 291 [para_from,28.2.1,26.2.1,factor_simp] nneg(x)|nneg(abs(x)). 295 [hyper,248,31] nneg(x)|leq(x,e). 347 [hyper,295,15] leq($c2,e). 374 [hyper,347,10,demod,207] leq(pluz($c2,x),x). 426 [para_into,374.1.1,25.1.1] leq(pluz(x,$c2),x). 497 [para_from,37.1.1,291.2.1,factor_simp] nneg(abs(x)). 498 [hyper,497,247] leq(e,abs(x)). 510 [para_into,497.1.1,17.2.1,unit_del,15] -leq($c2,abs($c1)). 516 [hyper,498,7,426,demod,207] leq($c2,abs(x)). 517 [binary,516.1,510.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 33 clauses generated 1488 clauses kept 486 clauses forward subsumed 1089 clauses back subsumed 94 Kbytes malloced 343 ----------- times (seconds) ----------- user CPU time 0.75 (0 hr, 0 min, 0 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 1 (0 hr, 0 min, 1 sec) hyper_res time 0.02 para_into time 0.03 para_from time 0.00 for_sub time 0.07 back_sub time 0.05 conflict time 0.18 demod time 0.03 The job finished Sun Nov 10 15:41:56 2002 Proof of Lemma 10: ----> UNIT CONFLICT at 3.12 sec ----> 1754 [binary,1753.1,238.1] $F. Length of proof is 10. Level of proof is 8. ---------------- PROOF ---------------- 5 [] leq(x,y)| -nneg(pluz(y,rvz(x))). 7 [] -leq(x,y)| -leq(y,z)|leq(x,z). 10 [] -leq(x,y)|leq(pluz(x,z),pluz(y,z)). 16 [] -leq(pluz($c2,rvz($c1)),pluz($c2,$c1)). 21,20 [] pluz(x,e)=x. 22 [] pluz(x,rvz(x))=e. 24 [] pluz(x,y)=pluz(y,x). 51 [] nneg($c1). 220,219 [para_into,24.1.1,20.1.1,flip.1] pluz(e,x)=x. 238 [para_from,24.1.1,16.1.1] -leq(pluz(rvz($c1),$c2),pluz($c2,$c1)). 304 [para_into,219.1.1,22.1.1,flip.1] rvz(e)=e. 316 [para_from,304.1.1,5.2.1.2,demod,21] leq(e,x)| -nneg(x). 357 [hyper,316,51] leq(e,$c1). 365 [hyper,357,10,demod,220] leq(x,pluz($c1,x)). 440 [para_into,365.1.2,24.1.1] leq(x,pluz(x,$c1)). 441 [para_into,365.1.2,22.1.1] leq(rvz($c1),e). 448 [hyper,441,10,demod,220] leq(pluz(rvz($c1),x),x). 1753 [hyper,448,7,440] leq(pluz(rvz($c1),x),pluz(x,$c1)). 1754 [binary,1753.1,238.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 69 clauses generated 4400 clauses kept 1718 clauses forward subsumed 2757 clauses back subsumed 49 Kbytes malloced 974 ----------- times (seconds) ----------- user CPU time 3.33 (0 hr, 0 min, 3 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 4 (0 hr, 0 min, 4 sec) hyper_res time 0.08 para_into time 0.00 para_from time 0.02 for_sub time 0.95 back_sub time 0.33 conflict time 0.17 demod time 0.12 The job finished Sun Nov 10 15:42:36 2002 Proof of Lemma 11a: ----> UNIT CONFLICT at 1.98 sec ----> 1397 [binary,1396.1,541.1] $F. Length of proof is 15. Level of proof is 5. ---------------- PROOF ---------------- 1 [] -nneg(x)| -nneg(y)|nneg(pluz(x,y)). 3 [] -nneg(x)|abs(x)=x. 15 [] nneg(x)|x!=abs(y). 17 [] -nneg($c1). 18 [] -leq(abs(pluz(abs($c2),rvz(abs($c1)))),abs(pluz($c2,rvz($c1)))). 23,22 [] pluz(x,e)=x. 24 [] pluz(x,rvz(x))=e. 26 [] pluz(x,y)=pluz(y,x). 27 [] nneg(x)|nneg(rvz(x)). 30 [] rvz(pluz(x,rvz(y)))=pluz(y,rvz(x)). 41,40 [] abs(rvz(x))=abs(x). 47 [] leq(abs(pluz(x,y)),pluz(abs(x),abs(y))). 53 [] nneg($c2). 78,77 [hyper,53,3] abs($c2)=$c2. 79 [back_demod,18,demod,78] -leq(abs(pluz($c2,rvz(abs($c1)))),abs(pluz($c2,rvz($c1)))). 94 [hyper,22,15,demod,23] nneg(abs(x)). 113 [hyper,94,1,53] nneg(pluz($c2,abs(x))). 190 [hyper,27,17] nneg(rvz($c1)). 233 [para_into,26.1.1,22.1.1,flip.1] pluz(e,x)=x. 263,262 [hyper,190,3,demod,41,flip.1] rvz($c1)=abs($c1). 264 [back_demod,79,demod,263] -leq(abs(pluz($c2,rvz(abs($c1)))),abs(pluz($c2,abs($c1)))). 268,267 [hyper,113,3] abs(pluz($c2,abs(x)))=pluz($c2,abs(x)). 280 [back_demod,264,demod,268] -leq(abs(pluz($c2,rvz(abs($c1)))),pluz($c2,abs($c1))). 327,326 [para_into,233.1.1,24.1.1,flip.1] rvz(e)=e. 418 [para_into,30.1.1.1,233.1.1,demod,327,23] rvz(rvz(x))=x. 535,534 [para_into,418.1.1.1,262.1.1] rvz(abs($c1))=$c1. 541 [back_demod,280,demod,535] -leq(abs(pluz($c2,$c1)),pluz($c2,abs($c1))). 1396 [para_into,47.1.2.1,77.1.1] leq(abs(pluz($c2,x)),pluz($c2,abs(x))). 1397 [binary,1396.1,541.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 61 clauses generated 3613 clauses kept 1358 clauses forward subsumed 2353 clauses back subsumed 34 Kbytes malloced 766 ----------- times (seconds) ----------- user CPU time 2.28 (0 hr, 0 min, 2 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 3 (0 hr, 0 min, 3 sec) hyper_res time 0.00 para_into time 0.02 para_from time 0.02 for_sub time 0.62 back_sub time 0.18 conflict time 0.17 demod time 0.07 The job finished Sun Nov 10 15:44:03 2002 Proof of Lemma 11b: ----> UNIT CONFLICT at 0.15 sec ----> 117 [binary,116.1,98.1] $F. Length of proof is 5. Level of proof is 3. ---------------- PROOF ---------------- 3 [] -nneg(x)|abs(x)=x. 11 [] pluz(x,y)!=pluz(z,y)|x=z. 18 [] abs(pluz(abs($c2),rvz(abs($c1))))!=abs(pluz($c2,rvz($c1))). 23,22 [] pluz(x,e)=x. 53 [] nneg($c2). 54 [] nneg($c1). 81,80 [hyper,53,3] abs($c2)=$c2. 83 [back_demod,18,demod,81] abs(pluz($c2,rvz(abs($c1))))!=abs(pluz($c2,rvz($c1))). 94,93 [hyper,54,3] abs($c1)=$c1. 98 [back_demod,83,demod,94] abs(pluz($c2,rvz($c1)))!=abs(pluz($c2,rvz($c1))). 116 [hyper,22,11,demod,23] x=x. 117 [binary,116.1,98.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 6 clauses generated 92 clauses kept 102 clauses forward subsumed 38 clauses back subsumed 7 Kbytes malloced 159 ----------- times (seconds) ----------- user CPU time 0.35 (0 hr, 0 min, 0 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 1 (0 hr, 0 min, 1 sec) hyper_res time 0.00 para_into time 0.00 para_from time 0.00 for_sub time 0.00 back_sub time 0.00 conflict time 0.13 demod time 0.00 The job finished Sun Nov 10 15:44:55 2002 Proof of Lemma 11c: ----> UNIT CONFLICT at 0.50 sec ----> 544 [binary,543.1,100.1] $F. Length of proof is 12. Level of proof is 5. ---------------- PROOF ---------------- 3 [] -nneg(x)|abs(x)=x. 11 [] pluz(x,y)!=pluz(z,y)|x=z. 19 [] -nneg($c2). 20 [] -nneg($c1). 21 [] abs(pluz(abs(rvz($c2)),rvz(abs(rvz($c1)))))!=abs(pluz(rvz($c2),$c1)). 27,26 [] pluz(x,e)=x. 28 [] pluz(x,rvz(x))=e. 30 [] pluz(x,y)=pluz(y,x). 31 [] nneg(x)|nneg(rvz(x)). 34 [] rvz(pluz(x,rvz(y)))=pluz(y,rvz(x)). 45,44 [] abs(rvz(x))=abs(x). 58 [back_demod,21,demod,45,45] abs(pluz(abs($c2),rvz(abs($c1))))!=abs(pluz(rvz($c2),$c1)). 100 [hyper,26,11,demod,27] x=x. 134 [hyper,31,20] nneg(rvz($c1)). 135 [hyper,31,19] nneg(rvz($c2)). 211 [hyper,134,3,demod,45,flip.1] rvz($c1)=abs($c1). 229,228 [hyper,135,3,demod,45,flip.1] rvz($c2)=abs($c2). 230 [back_demod,58,demod,229] abs(pluz(abs($c2),rvz(abs($c1))))!=abs(pluz(abs($c2),$c1)). 281 [para_into,30.1.1,26.1.1,flip.1] pluz(e,x)=x. 327,326 [para_into,281.1.1,28.1.1,flip.1] rvz(e)=e. 453 [para_into,34.1.1.1,281.1.1,demod,327,27] rvz(rvz(x))=x. 535,534 [para_into,453.1.1.1,211.1.1] rvz(abs($c1))=$c1. 543 [back_demod,230,demod,535] abs(pluz(abs($c2),$c1))!=abs(pluz(abs($c2),$c1)). 544 [binary,543.1,100.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 32 clauses generated 1474 clauses kept 497 clauses forward subsumed 1103 clauses back subsumed 20 Kbytes malloced 375 ----------- times (seconds) ----------- user CPU time 0.75 (0 hr, 0 min, 0 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 1 (0 hr, 0 min, 1 sec) hyper_res time 0.00 para_into time 0.00 para_from time 0.02 for_sub time 0.05 back_sub time 0.07 conflict time 0.20 demod time 0.03 The job finished Sun Nov 10 15:48:47 2002 Proof of Lemma 11 (proved under strongly inhibited hypotheses): ----> UNIT CONFLICT at 0.50 sec ----> 389 [binary,388.1,8.1] $F. Length of proof is 18. Level of proof is 8. ---------------- PROOF ---------------- 1 [] -nneg(x)|nneg(y)|leq(abs(pluz(abs(x),rvz(abs(y)))),abs(pluz(x,rvz(y)))). 2 [] -nneg(x)| -nneg(y)|abs(pluz(abs(x),rvz(abs(y))))=abs(pluz(x,rvz(y))). 3 [] -leq(abs(pluz(abs($c2),rvz(abs($c1)))),abs(pluz($c2,rvz($c1)))). 5 [] pluz(x,y)=pluz(y,x). 6 [] rvz(pluz(x,rvz(y)))=pluz(y,rvz(x)). 8 [] leq(x,x). 10,9 [] abs(rvz(x))=abs(x). 11 [] nneg(x)|nneg(y)|abs(pluz(abs(rvz(x)),rvz(abs(rvz(y)))))=abs(pluz(rvz(x),y)). 12 [copy,11,demod,10,10] nneg(x)|nneg(y)|abs(pluz(abs(x),rvz(abs(y))))=abs(pluz(rvz(x),y)). 16 [para_from,5.1.1,3.1.2.1] -leq(abs(pluz(abs($c2),rvz(abs($c1)))),abs(pluz(rvz($c1),$c2))). 18 [para_from,5.1.1,1.3.2.1] -nneg(x)|nneg(y)|leq(abs(pluz(abs(x),rvz(abs(y)))),abs(pluz(rvz(y),x))). 29 [para_into,6.1.1.1,5.1.1] rvz(pluz(rvz(x),y))=pluz(x,rvz(y)). 31 [para_from,6.1.1,9.1.1.1] abs(pluz(x,rvz(y)))=abs(pluz(y,rvz(x))). 38 [para_from,29.1.1,9.1.1.1] abs(pluz(x,rvz(y)))=abs(pluz(rvz(x),y)). 46 [para_from,31.1.1,3.1.2] -leq(abs(pluz(abs($c2),rvz(abs($c1)))),abs(pluz($c1,rvz($c2)))). 47 [para_from,31.1.1,3.1.1] -leq(abs(pluz(abs($c1),rvz(abs($c2)))),abs(pluz($c2,rvz($c1)))). 72 [para_from,38.1.1,3.1.2] -leq(abs(pluz(abs($c2),rvz(abs($c1)))),abs(pluz(rvz($c2),$c1))). 288 [para_into,46.1.1,31.1.1] -leq(abs(pluz(abs($c1),rvz(abs($c2)))),abs(pluz($c1,rvz($c2)))). 293 [para_into,47.1.2,38.1.1] -leq(abs(pluz(abs($c1),rvz(abs($c2)))),abs(pluz(rvz($c2),$c1))). 295 [para_into,72.1.1,12.3.1,unit_del,8] nneg($c2)|nneg($c1). 337 [hyper,295,18] nneg($c1)|nneg(x)|leq(abs(pluz(abs($c2),rvz(abs(x)))),abs(pluz(rvz(x),$c2))). 347 [hyper,295,18] nneg($c2)|nneg(x)|leq(abs(pluz(abs($c1),rvz(abs(x)))),abs(pluz(rvz(x),$c1))). 357 [factor,337,1,2,unit_del,16] nneg($c1). 358 [factor,347,1,2,unit_del,293] nneg($c2). 377,376 [hyper,358,2,357] abs(pluz(abs($c1),rvz(abs($c2))))=abs(pluz($c1,rvz($c2))). 388 [back_demod,288,demod,377] -leq(abs(pluz($c1,rvz($c2))),abs(pluz($c1,rvz($c2)))). 389 [binary,388.1,8.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 29 clauses generated 684 clauses kept 374 clauses forward subsumed 360 clauses back subsumed 25 Kbytes malloced 423 ----------- times (seconds) ----------- user CPU time 0.73 (0 hr, 0 min, 0 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 1 (0 hr, 0 min, 1 sec) hyper_res time 0.02 para_into time 0.00 para_from time 0.02 for_sub time 0.10 back_sub time 0.03 conflict time 0.17 demod time 0.00 The job finished Sun Nov 10 16:00:54 2002 Proof of Lemma 12: ----> UNIT CONFLICT at 219.13 sec ----> 6699 [binary,6698.1,270.1] $F. Length of proof is 20. Level of proof is 9. ---------------- PROOF ---------------- 5 [] leq(x,y)| -nneg(pluz(y,rvz(x))). 7 [] -leq(x,y)| -leq(y,z)|leq(x,z). 10 [] -leq(x,y)|leq(pluz(x,z),pluz(y,z)). 15 [] nneg(x)|x!=abs(y). 19 [] -leq(pluz(abs($c2),rvz(abs(pluz(abs($c1),rvz(abs($c2)))))),abs($c1)). 22 [] pluz(pluz(x,y),z)=pluz(x,pluz(y,z)). 25,24 [] pluz(x,e)=x. 26 [] pluz(x,rvz(x))=e. 28 [] pluz(x,y)=pluz(y,x). 30 [] nneg(x)|abs(x)=rvz(x). 31 [copy,30,flip.2] nneg(x)|rvz(x)=abs(x). 32 [] rvz(pluz(x,rvz(y)))=pluz(y,rvz(x)). 35 [] leq(x,x). 98 [hyper,24,15,demod,25] nneg(abs(x)). 183 [para_from,26.1.1,22.1.1.1,flip.1] pluz(x,pluz(rvz(x),y))=pluz(e,y). 252,251 [para_into,28.1.1,24.1.1,flip.1] pluz(e,x)=x. 261 [back_demod,183,demod,252] pluz(x,pluz(rvz(x),y))=y. 270 [para_from,28.1.1,19.1.1.2.1.1] -leq(pluz(abs($c2),rvz(abs(pluz(rvz(abs($c2)),abs($c1))))),abs($c1)). 334,333 [para_into,251.1.1,26.1.1,flip.1] rvz(e)=e. 381 [para_from,333.1.1,5.2.1.2,demod,25] leq(e,x)| -nneg(x). 383 [hyper,381,98] leq(e,abs(x)). 391 [hyper,383,10,demod,252] leq(x,pluz(abs(y),x)). 418 [para_into,32.1.1.1,251.1.1,demod,334,25] rvz(rvz(x))=x. 478 [para_into,418.1.1.1,31.2.1] rvz(abs(x))=x|nneg(x). 1376 [para_into,391.1.2,26.1.1] leq(rvz(abs(x)),e). 1383 [hyper,1376,10,demod,252] leq(pluz(rvz(abs(x)),y),y). 3613 [para_from,478.1.1,19.1.1.2] -leq(pluz(abs($c2),pluz(abs($c1),rvz(abs($c2)))),abs($c1))|nneg(pluz(abs($c1),rvz(abs($c2)))). 4844 [para_into,1383.1.1,28.1.1] leq(pluz(x,rvz(abs(y))),x). 6674,6673 [para_into,261.1.1.2,28.1.1] pluz(x,pluz(y,rvz(x)))=y. 6677 [back_demod,3613,demod,6674,unit_del,35] nneg(pluz(abs($c1),rvz(abs($c2)))). 6688 [hyper,6677,5] leq(abs($c2),abs($c1)). 6698 [hyper,6688,7,4844] leq(pluz(abs($c2),rvz(abs(x))),abs($c1)). 6699 [binary,6698.1,270.1] $F. ------------ end of proof ------------- Search stopped by max_proofs option. ============ end of search ============ -------------- statistics ------------- clauses given 267 clauses generated 55841 clauses kept 6608 clauses forward subsumed 22549 clauses back subsumed 188 Kbytes malloced 4217 ----------- times (seconds) ----------- user CPU time 219.35 (0 hr, 3 min, 39 sec) system CPU time 0.00 (0 hr, 0 min, 0 sec) wall-clock time 219 (0 hr, 3 min, 39 sec) hyper_res time 1.37 para_into time 0.23 para_from time 0.35 for_sub time 36.62 back_sub time 9.23 conflict time 0.52 demod time 2.08 The job finished Sun Nov 10 16:36:08 2002