%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : NUM845+1 : TPTP v8.1.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %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 : 600s % DateTime : Mon Jul 18 08:49:06 EDT 2022 % Result : Theorem 4.94s 1.78s % Output : Proof 12.85s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM845+1 : TPTP v8.1.0. Released v4.1.0. % 0.03/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.34 % Computer : n004.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Tue Jul 5 07:29:52 EDT 2022 % 0.12/0.34 % CPUTime : % 0.59/0.58 ____ _ % 0.59/0.58 ___ / __ \_____(_)___ ________ __________ % 0.59/0.58 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.59/0.58 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.59/0.58 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.59/0.58 % 0.59/0.58 A Theorem Prover for First-Order Logic % 0.59/0.58 (ePrincess v.1.0) % 0.59/0.58 % 0.59/0.58 (c) Philipp Rümmer, 2009-2015 % 0.59/0.58 (c) Peter Backeman, 2014-2015 % 0.59/0.58 (contributions by Angelo Brillout, Peter Baumgartner) % 0.59/0.58 Free software under GNU Lesser General Public License (LGPL). % 0.59/0.58 Bug reports to peter@backeman.se % 0.59/0.58 % 0.59/0.58 For more information, visit http://user.uu.se/~petba168/breu/ % 0.59/0.58 % 0.59/0.58 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.59/0.63 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.85/0.99 Prover 0: Preprocessing ... % 3.28/1.45 Prover 0: Warning: ignoring some quantifiers % 3.64/1.48 Prover 0: Constructing countermodel ... % 4.94/1.78 Prover 0: proved (1152ms) % 4.94/1.78 % 4.94/1.78 No countermodel exists, formula is valid % 4.94/1.78 % SZS status Theorem for theBenchmark % 4.94/1.78 % 4.94/1.78 Generating proof ... Warning: ignoring some quantifiers % 11.82/3.36 found it (size 438) % 11.82/3.36 % 11.82/3.36 % SZS output start Proof for theBenchmark % 11.82/3.36 Assumed formulas after preprocessing and simplification: % 11.82/3.36 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ( ~ (v8 = v6) & vsucc(v2) = v5 & vsucc(v1) = v0 & vsucc(vd411) = v0 & vmul(v0, v5) = v6 & vmul(v0, v2) = v3 & vmul(v0, v1) = v0 & vmul(vd411, v5) = v7 & vmul(vd411, v2) = v4 & vmul(vd411, v1) = v1 & vplus(v7, v5) = v8 & vplus(v4, v2) = v3 & vplus(v1, v1) = v0 & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : ( ~ (vplus(v10, v12) = v14) | ~ (vplus(v9, v11) = v13) | ~ geq(v11, v12) | ~ geq(v9, v10) | geq(v13, v14)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : ( ~ (vplus(v10, v12) = v14) | ~ (vplus(v9, v11) = v13) | ~ geq(v11, v12) | ~ greater(v9, v10) | greater(v13, v14)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : ( ~ (vplus(v10, v12) = v14) | ~ (vplus(v9, v11) = v13) | ~ geq(v9, v10) | ~ greater(v11, v12) | greater(v13, v14)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ! [v14] : ( ~ (vplus(v10, v12) = v14) | ~ (vplus(v9, v11) = v13) | ~ greater(v11, v12) | ~ greater(v9, v10) | greater(v13, v14)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (vsucc(v11) = v12) | ~ (vmul(vd411, v9) = v10) | ~ (vplus(v10, v12) = v13) | ~ (vplus(vd411, v9) = v11) | ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : (vsucc(v9) = v16 & vmul(v0, v9) = v14 & vplus(v10, v17) = v18 & vplus(v10, v9) = v15 & vplus(vd411, v16) = v17 & ( ~ (v15 = v14) | v18 = v13))) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (vsucc(v11) = v12) | ~ (vmul(vd411, v9) = v10) | ~ (vplus(v10, v12) = v13) | ~ (vplus(vd411, v9) = v11) | ? [v14] : ? [v15] : ? [v16] : ? [v17] : (vmul(v0, v9) = v14 & vplus(v10, v16) = v17 & vplus(v10, v9) = v15 & vplus(v0, v9) = v16 & ( ~ (v15 = v14) | v17 = v13))) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (vsucc(v9) = v12) | ~ (vmul(vd411, v9) = v10) | ~ (vplus(v11, v12) = v13) | ~ (vplus(v10, vd411) = v11) | ? [v14] : ? [v15] : ? [v16] : ? [v17] : (vmul(v0, v9) = v14 & vmul(vd411, v12) = v16 & vplus(v16, v12) = v17 & vplus(v10, v9) = v15 & ( ~ (v15 = v14) | v17 = v13))) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (vsucc(v9) = v11) | ~ (vmul(vd411, v9) = v10) | ~ (vplus(v12, v11) = v13) | ~ (vplus(v10, vd411) = v12) | ? [v14] : ? [v15] : ? [v16] : ? [v17] : (vmul(v0, v9) = v14 & vplus(v10, v16) = v17 & vplus(v10, v9) = v15 & vplus(vd411, v11) = v16 & ( ~ (v15 = v14) | v17 = v13))) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (vsucc(v9) = v11) | ~ (vmul(vd411, v9) = v10) | ~ (vplus(v10, v12) = v13) | ~ (vplus(vd411, v11) = v12) | ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : (vsucc(v16) = v17 & vmul(v0, v9) = v14 & vplus(v10, v17) = v18 & vplus(v10, v9) = v15 & vplus(vd411, v9) = v16 & ( ~ (v15 = v14) | v18 = v13))) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (vsucc(v9) = v11) | ~ (vmul(vd411, v9) = v10) | ~ (vplus(v10, v12) = v13) | ~ (vplus(vd411, v11) = v12) | ? [v14] : ? [v15] : ? [v16] : ? [v17] : (vmul(v0, v9) = v14 & vplus(v16, v11) = v17 & vplus(v10, v9) = v15 & vplus(v10, vd411) = v16 & ( ~ (v15 = v14) | v17 = v13))) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (vplus(v12, v11) = v13) | ~ (vplus(v9, v10) = v12) | ? [v14] : (vplus(v10, v11) = v14 & vplus(v9, v14) = v13)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (vplus(v10, v11) = v13) | ~ (vplus(v9, v11) = v12) | ~ greater(v12, v13) | greater(v9, v10)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (vplus(v10, v11) = v13) | ~ (vplus(v9, v11) = v12) | ~ greater(v9, v10) | greater(v12, v13)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (vplus(v10, v11) = v13) | ~ (vplus(v9, v11) = v12) | ~ less(v12, v13) | less(v9, v10)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (vplus(v10, v11) = v13) | ~ (vplus(v9, v11) = v12) | ~ less(v9, v10) | less(v12, v13)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ! [v13] : ( ~ (vplus(v10, v11) = v12) | ~ (vplus(v9, v12) = v13) | ? [v14] : (vplus(v14, v11) = v13 & vplus(v9, v10) = v14)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v12 = v11 | ~ (vplus(v9, v10) = v12) | ~ (vplus(v9, v10) = v11)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v10 = v9 | ~ (vmul(v12, v11) = v10) | ~ (vmul(v12, v11) = v9)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v10 = v9 | ~ (vplus(v12, v11) = v10) | ~ (vplus(v12, v11) = v9)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : (v10 = v9 | ~ (vplus(v10, v11) = v12) | ~ (vplus(v9, v11) = v12)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (vsucc(v10) = v11) | ~ (vmul(v9, v11) = v12) | ? [v13] : (vmul(v9, v10) = v13 & vplus(v13, v9) = v12)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (vsucc(v10) = v11) | ~ (vplus(v9, v11) = v12) | ? [v13] : (vsucc(v13) = v12 & vplus(v9, v10) = v13)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (vsucc(v9) = v11) | ~ (vplus(v11, v10) = v12) | ? [v13] : (vsucc(v13) = v12 & vplus(v9, v10) = v13)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (vsucc(v9) = v10) | ~ (vmul(vd411, v10) = v11) | ~ (vplus(v11, v10) = v12) | ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : (vmul(v0, v9) = v13 & vmul(vd411, v9) = v14 & vplus(v16, v10) = v17 & vplus(v14, v9) = v15 & vplus(v14, vd411) = v16 & ( ~ (v15 = v13) | v17 = v12))) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (vmul(v9, v10) = v11) | ~ (vplus(v11, v9) = v12) | ? [v13] : (vsucc(v10) = v13 & vmul(v9, v13) = v12)) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (vmul(vd411, v9) = v10) | ~ (vplus(v10, v11) = v12) | ~ (vplus(v9, v0) = v11) | ? [v13] : ? [v14] : ? [v15] : ? [v16] : (vmul(v0, v9) = v13 & vplus(v10, v15) = v16 & vplus(v10, v9) = v14 & vplus(v0, v9) = v15 & ( ~ (v14 = v13) | v16 = v12))) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (vmul(vd411, v9) = v10) | ~ (vplus(v10, v11) = v12) | ~ (vplus(v9, v0) = v11) | ? [v13] : ? [v14] : ? [v15] : (vmul(v0, v9) = v13 & vplus(v14, v0) = v15 & vplus(v10, v9) = v14 & ( ~ (v14 = v13) | v15 = v12))) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (vmul(vd411, v9) = v10) | ~ (vplus(v10, v11) = v12) | ~ (vplus(v0, v9) = v11) | ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : (vsucc(v15) = v16 & vmul(v0, v9) = v13 & vplus(v10, v16) = v17 & vplus(v10, v9) = v14 & vplus(vd411, v9) = v15 & ( ~ (v14 = v13) | v17 = v12))) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (vmul(vd411, v9) = v10) | ~ (vplus(v10, v11) = v12) | ~ (vplus(v0, v9) = v11) | ? [v13] : ? [v14] : ? [v15] : ? [v16] : (vmul(v0, v9) = v13 & vplus(v10, v15) = v16 & vplus(v10, v9) = v14 & vplus(v9, v0) = v15 & ( ~ (v14 = v13) | v16 = v12))) & ! [v9] : ! [v10] : ! [v11] : ! [v12] : ( ~ (vplus(v10, v12) = v9) | ~ (vplus(v9, v11) = v10)) & ? [v9] : ! [v10] : ! [v11] : ! [v12] : (v10 = v9 | ~ (vplus(v11, v10) = v12) | ? [v13] : ( ~ (v13 = v12) & vplus(v11, v9) = v13)) & ! [v9] : ! [v10] : ! [v11] : (v10 = v9 | ~ (vskolem2(v11) = v10) | ~ (vskolem2(v11) = v9)) & ! [v9] : ! [v10] : ! [v11] : (v10 = v9 | ~ (vsucc(v11) = v10) | ~ (vsucc(v11) = v9)) & ! [v9] : ! [v10] : ! [v11] : (v10 = v9 | ~ (vsucc(v10) = v11) | ~ (vsucc(v9) = v11)) & ! [v9] : ! [v10] : ! [v11] : ( ~ (vmul(vd411, v9) = v10) | ~ (vplus(v10, v9) = v11) | ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : (vsucc(v13) = v14 & vsucc(v9) = v16 & vmul(v0, v9) = v12 & vplus(v10, v17) = v18 & vplus(v10, v14) = v15 & vplus(vd411, v16) = v17 & vplus(vd411, v9) = v13 & ( ~ (v12 = v11) | v18 = v15))) & ! [v9] : ! [v10] : ! [v11] : ( ~ (vmul(vd411, v9) = v10) | ~ (vplus(v10, v9) = v11) | ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : (vsucc(v15) = v16 & vmul(v0, v9) = v12 & vplus(v10, v16) = v17 & vplus(v10, v13) = v14 & vplus(v0, v9) = v13 & vplus(vd411, v9) = v15 & ( ~ (v12 = v11) | v17 = v14))) & ! [v9] : ! [v10] : ! [v11] : ( ~ (vmul(vd411, v9) = v10) | ~ (vplus(v10, v9) = v11) | ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : (vsucc(v9) = v14 & vmul(v0, v9) = v12 & vmul(vd411, v14) = v16 & vplus(v16, v14) = v17 & vplus(v13, v14) = v15 & vplus(v10, vd411) = v13 & ( ~ (v12 = v11) | v17 = v15))) & ! [v9] : ! [v10] : ! [v11] : ( ~ (vmul(vd411, v9) = v10) | ~ (vplus(v10, v9) = v11) | ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : (vsucc(v9) = v13 & vmul(v0, v9) = v12 & vplus(v16, v13) = v17 & vplus(v10, v14) = v15 & vplus(v10, vd411) = v16 & vplus(vd411, v13) = v14 & ( ~ (v12 = v11) | v17 = v15))) & ! [v9] : ! [v10] : ! [v11] : ( ~ (vmul(vd411, v9) = v10) | ~ (vplus(v10, v9) = v11) | ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : (vmul(v0, v9) = v12 & vplus(v10, v15) = v16 & vplus(v10, v13) = v14 & vplus(v9, v0) = v13 & vplus(v0, v9) = v15 & ( ~ (v12 = v11) | v16 = v14))) & ! [v9] : ! [v10] : ! [v11] : ( ~ (vmul(vd411, v9) = v10) | ~ (vplus(v10, v9) = v11) | ? [v12] : ? [v13] : ? [v14] : ? [v15] : (vsucc(v9) = v13 & vmul(v0, v13) = v14 & vmul(v0, v9) = v12 & vplus(v12, v0) = v15 & ( ~ (v12 = v11) | v15 = v14))) & ! [v9] : ! [v10] : ! [v11] : ( ~ (vmul(vd411, v9) = v10) | ~ (vplus(v10, v9) = v11) | ? [v12] : ? [v13] : ? [v14] : ? [v15] : (vmul(v0, v9) = v12 & vplus(v11, v0) = v13 & vplus(v10, v14) = v15 & vplus(v9, v0) = v14 & ( ~ (v12 = v11) | v15 = v13))) & ! [v9] : ! [v10] : ! [v11] : ( ~ (vmul(vd411, v9) = v10) | ~ (vplus(v10, v9) = v11) | ? [v12] : ? [v13] : ? [v14] : (vmul(v0, v9) = v12 & vplus(v12, v0) = v13 & vplus(v11, v0) = v14 & ( ~ (v12 = v11) | v14 = v13))) & ! [v9] : ! [v10] : ! [v11] : ( ~ (vplus(v10, v11) = v9) | less(v10, v9)) & ! [v9] : ! [v10] : ! [v11] : ( ~ (vplus(v10, v9) = v11) | vplus(v9, v10) = v11) & ! [v9] : ! [v10] : ! [v11] : ( ~ (vplus(v10, v1) = v11) | ~ greater(v9, v10) | geq(v9, v11)) & ! [v9] : ! [v10] : ! [v11] : ( ~ (vplus(v10, v1) = v11) | ~ less(v9, v11) | leq(v9, v10)) & ! [v9] : ! [v10] : ! [v11] : ( ~ (vplus(v9, v11) = v10) | greater(v10, v9)) & ! [v9] : ! [v10] : ! [v11] : ( ~ (vplus(v9, v10) = v11) | vplus(v10, v9) = v11) & ! [v9] : ! [v10] : ! [v11] : ( ~ (vplus(v9, v10) = v11) | greater(v11, v9)) & ! [v9] : ! [v10] : ! [v11] : ( ~ (vplus(v9, v10) = v11) | ? [v12] : ? [v13] : (vsucc(v11) = v13 & vsucc(v10) = v12 & vplus(v9, v12) = v13)) & ! [v9] : ! [v10] : ! [v11] : ( ~ (vplus(v9, v10) = v11) | ? [v12] : ? [v13] : (vsucc(v11) = v13 & vsucc(v9) = v12 & vplus(v12, v10) = v13)) & ! [v9] : ! [v10] : ! [v11] : ( ~ leq(v10, v11) | ~ leq(v9, v10) | leq(v9, v11)) & ! [v9] : ! [v10] : ! [v11] : ( ~ leq(v10, v11) | ~ less(v9, v10) | less(v9, v11)) & ! [v9] : ! [v10] : ! [v11] : ( ~ leq(v9, v10) | ~ less(v10, v11) | less(v9, v11)) & ! [v9] : ! [v10] : ! [v11] : ( ~ less(v10, v11) | ~ less(v9, v10) | less(v9, v11)) & ! [v9] : ! [v10] : (v10 = v9 | ~ (vmul(v9, v1) = v10)) & ! [v9] : ! [v10] : (v10 = v9 | ~ (vmul(v1, v9) = v10)) & ! [v9] : ! [v10] : (v10 = v9 | ~ geq(v10, v9) | greater(v10, v9)) & ! [v9] : ! [v10] : (v10 = v9 | ~ leq(v10, v9) | less(v10, v9)) & ! [v9] : ! [v10] : (v9 = v1 | ~ (vskolem2(v9) = v10) | vsucc(v10) = v9) & ! [v9] : ! [v10] : ( ~ (vsucc(v9) = v10) | vplus(v9, v1) = v10) & ! [v9] : ! [v10] : ( ~ (vsucc(v9) = v10) | vplus(v1, v9) = v10) & ! [v9] : ! [v10] : ( ~ (vsucc(v9) = v10) | ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : (vmul(v0, v10) = v14 & vmul(v0, v9) = v11 & vmul(vd411, v9) = v12 & vplus(v12, v9) = v13 & vplus(v11, v0) = v15 & ( ~ (v13 = v11) | v15 = v14))) & ! [v9] : ! [v10] : ( ~ (vmul(v0, v9) = v10) | ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : (vsucc(v13) = v14 & vsucc(v9) = v16 & vmul(vd411, v9) = v11 & vplus(v11, v17) = v18 & vplus(v11, v14) = v15 & vplus(v11, v9) = v12 & vplus(vd411, v16) = v17 & vplus(vd411, v9) = v13 & ( ~ (v12 = v10) | v18 = v15))) & ! [v9] : ! [v10] : ( ~ (vmul(v0, v9) = v10) | ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : (vsucc(v15) = v16 & vmul(vd411, v9) = v11 & vplus(v11, v16) = v17 & vplus(v11, v13) = v14 & vplus(v11, v9) = v12 & vplus(v0, v9) = v13 & vplus(vd411, v9) = v15 & ( ~ (v12 = v10) | v17 = v14))) & ! [v9] : ! [v10] : ( ~ (vmul(v0, v9) = v10) | ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : (vsucc(v9) = v14 & vmul(vd411, v14) = v16 & vmul(vd411, v9) = v11 & vplus(v16, v14) = v17 & vplus(v13, v14) = v15 & vplus(v11, v9) = v12 & vplus(v11, vd411) = v13 & ( ~ (v12 = v10) | v17 = v15))) & ! [v9] : ! [v10] : ( ~ (vmul(v0, v9) = v10) | ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : (vsucc(v9) = v13 & vmul(vd411, v9) = v11 & vplus(v16, v13) = v17 & vplus(v11, v14) = v15 & vplus(v11, v9) = v12 & vplus(v11, vd411) = v16 & vplus(vd411, v13) = v14 & ( ~ (v12 = v10) | v17 = v15))) & ! [v9] : ! [v10] : ( ~ (vmul(v0, v9) = v10) | ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : (vmul(vd411, v9) = v11 & vplus(v11, v15) = v16 & vplus(v11, v13) = v14 & vplus(v11, v9) = v12 & vplus(v9, v0) = v13 & vplus(v0, v9) = v15 & ( ~ (v12 = v10) | v16 = v14))) & ! [v9] : ! [v10] : ( ~ (vmul(v0, v9) = v10) | ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : (vsucc(v9) = v13 & vmul(v0, v13) = v14 & vmul(vd411, v9) = v11 & vplus(v11, v9) = v12 & vplus(v10, v0) = v15 & ( ~ (v12 = v10) | v15 = v14))) & ! [v9] : ! [v10] : ( ~ (vmul(v0, v9) = v10) | ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : (vmul(vd411, v9) = v11 & vplus(v12, v0) = v13 & vplus(v11, v14) = v15 & vplus(v11, v9) = v12 & vplus(v9, v0) = v14 & ( ~ (v12 = v10) | v15 = v13))) & ! [v9] : ! [v10] : ( ~ (vmul(v0, v9) = v10) | ? [v11] : ? [v12] : ? [v13] : ? [v14] : (vmul(vd411, v9) = v11 & vplus(v12, v0) = v14 & vplus(v11, v9) = v12 & vplus(v10, v0) = v13 & ( ~ (v12 = v10) | v14 = v13))) & ! [v9] : ! [v10] : ~ (vplus(v9, v10) = v10) & ! [v9] : ! [v10] : ~ (vplus(v9, v10) = v9) & ! [v9] : ! [v10] : ( ~ (vplus(v9, v1) = v10) | vsucc(v9) = v10) & ! [v9] : ! [v10] : ( ~ (vplus(v1, v9) = v10) | vsucc(v9) = v10) & ! [v9] : ! [v10] : ( ~ geq(v9, v10) | leq(v10, v9)) & ! [v9] : ! [v10] : ( ~ greater(v10, v9) | geq(v10, v9)) & ! [v9] : ! [v10] : ( ~ greater(v10, v9) | ? [v11] : vplus(v9, v11) = v10) & ! [v9] : ! [v10] : ( ~ greater(v9, v10) | ~ less(v9, v10)) & ! [v9] : ! [v10] : ( ~ greater(v9, v10) | less(v10, v9)) & ! [v9] : ! [v10] : ( ~ leq(v9, v10) | geq(v10, v9)) & ! [v9] : ! [v10] : ( ~ less(v10, v9) | leq(v10, v9)) & ! [v9] : ! [v10] : ( ~ less(v10, v9) | ? [v11] : vplus(v10, v11) = v9) & ! [v9] : ! [v10] : ( ~ less(v9, v10) | greater(v10, v9)) & ! [v9] : ~ (vsucc(v9) = v9) & ! [v9] : ~ (vsucc(v9) = v1) & ! [v9] : ~ greater(v9, v9) & ! [v9] : ~ less(v9, v9) & ? [v9] : ? [v10] : (v10 = v9 | greater(v9, v10) | less(v9, v10)) & ? [v9] : ? [v10] : (v10 = v9 | ? [v11] : ? [v12] : ((v12 = v10 & vplus(v9, v11) = v10) | (v12 = v9 & vplus(v10, v11) = v9))) & ? [v9] : geq(v9, v9) & ? [v9] : geq(v9, v1) & ? [v9] : leq(v9, v9)) % 11.98/3.43 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6, all_0_7_7, all_0_8_8 yields: % 11.98/3.43 | (1) ~ (all_0_0_0 = all_0_2_2) & vsucc(all_0_6_6) = all_0_3_3 & vsucc(all_0_7_7) = all_0_8_8 & vsucc(vd411) = all_0_8_8 & vmul(all_0_8_8, all_0_3_3) = all_0_2_2 & vmul(all_0_8_8, all_0_6_6) = all_0_5_5 & vmul(all_0_8_8, v1) = all_0_8_8 & vmul(vd411, all_0_3_3) = all_0_1_1 & vmul(vd411, all_0_6_6) = all_0_4_4 & vmul(vd411, v1) = all_0_7_7 & vplus(all_0_1_1, all_0_3_3) = all_0_0_0 & vplus(all_0_4_4, all_0_6_6) = all_0_5_5 & vplus(all_0_7_7, v1) = all_0_8_8 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (vplus(v1, v3) = v5) | ~ (vplus(v0, v2) = v4) | ~ geq(v2, v3) | ~ geq(v0, v1) | geq(v4, v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (vplus(v1, v3) = v5) | ~ (vplus(v0, v2) = v4) | ~ geq(v2, v3) | ~ greater(v0, v1) | greater(v4, v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (vplus(v1, v3) = v5) | ~ (vplus(v0, v2) = v4) | ~ geq(v0, v1) | ~ greater(v2, v3) | greater(v4, v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (vplus(v1, v3) = v5) | ~ (vplus(v0, v2) = v4) | ~ greater(v2, v3) | ~ greater(v0, v1) | greater(v4, v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (vsucc(v2) = v3) | ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v3) = v4) | ~ (vplus(vd411, v0) = v2) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (vsucc(v0) = v7 & vmul(all_0_8_8, v0) = v5 & vplus(v1, v8) = v9 & vplus(v1, v0) = v6 & vplus(vd411, v7) = v8 & ( ~ (v6 = v5) | v9 = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (vsucc(v2) = v3) | ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v3) = v4) | ~ (vplus(vd411, v0) = v2) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (vmul(all_0_8_8, v0) = v5 & vplus(v1, v7) = v8 & vplus(v1, v0) = v6 & vplus(all_0_8_8, v0) = v7 & ( ~ (v6 = v5) | v8 = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (vsucc(v0) = v3) | ~ (vmul(vd411, v0) = v1) | ~ (vplus(v2, v3) = v4) | ~ (vplus(v1, vd411) = v2) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (vmul(all_0_8_8, v0) = v5 & vmul(vd411, v3) = v7 & vplus(v7, v3) = v8 & vplus(v1, v0) = v6 & ( ~ (v6 = v5) | v8 = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (vsucc(v0) = v2) | ~ (vmul(vd411, v0) = v1) | ~ (vplus(v3, v2) = v4) | ~ (vplus(v1, vd411) = v3) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (vmul(all_0_8_8, v0) = v5 & vplus(v1, v7) = v8 & vplus(v1, v0) = v6 & vplus(vd411, v2) = v7 & ( ~ (v6 = v5) | v8 = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (vsucc(v0) = v2) | ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v3) = v4) | ~ (vplus(vd411, v2) = v3) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (vsucc(v7) = v8 & vmul(all_0_8_8, v0) = v5 & vplus(v1, v8) = v9 & vplus(v1, v0) = v6 & vplus(vd411, v0) = v7 & ( ~ (v6 = v5) | v9 = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (vsucc(v0) = v2) | ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v3) = v4) | ~ (vplus(vd411, v2) = v3) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (vmul(all_0_8_8, v0) = v5 & vplus(v7, v2) = v8 & vplus(v1, v0) = v6 & vplus(v1, vd411) = v7 & ( ~ (v6 = v5) | v8 = v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (vplus(v3, v2) = v4) | ~ (vplus(v0, v1) = v3) | ? [v5] : (vplus(v1, v2) = v5 & vplus(v0, v5) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (vplus(v1, v2) = v4) | ~ (vplus(v0, v2) = v3) | ~ greater(v3, v4) | greater(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (vplus(v1, v2) = v4) | ~ (vplus(v0, v2) = v3) | ~ greater(v0, v1) | greater(v3, v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (vplus(v1, v2) = v4) | ~ (vplus(v0, v2) = v3) | ~ less(v3, v4) | less(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (vplus(v1, v2) = v4) | ~ (vplus(v0, v2) = v3) | ~ less(v0, v1) | less(v3, v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (vplus(v1, v2) = v3) | ~ (vplus(v0, v3) = v4) | ? [v5] : (vplus(v5, v2) = v4 & vplus(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (vplus(v0, v1) = v3) | ~ (vplus(v0, v1) = v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (vmul(v3, v2) = v1) | ~ (vmul(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (vplus(v3, v2) = v1) | ~ (vplus(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (vplus(v1, v2) = v3) | ~ (vplus(v0, v2) = v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (vsucc(v1) = v2) | ~ (vmul(v0, v2) = v3) | ? [v4] : (vmul(v0, v1) = v4 & vplus(v4, v0) = v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (vsucc(v1) = v2) | ~ (vplus(v0, v2) = v3) | ? [v4] : (vsucc(v4) = v3 & vplus(v0, v1) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (vsucc(v0) = v2) | ~ (vplus(v2, v1) = v3) | ? [v4] : (vsucc(v4) = v3 & vplus(v0, v1) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (vsucc(v0) = v1) | ~ (vmul(vd411, v1) = v2) | ~ (vplus(v2, v1) = v3) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (vmul(all_0_8_8, v0) = v4 & vmul(vd411, v0) = v5 & vplus(v7, v1) = v8 & vplus(v5, v0) = v6 & vplus(v5, vd411) = v7 & ( ~ (v6 = v4) | v8 = v3))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (vmul(v0, v1) = v2) | ~ (vplus(v2, v0) = v3) | ? [v4] : (vsucc(v1) = v4 & vmul(v0, v4) = v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v2) = v3) | ~ (vplus(v0, all_0_8_8) = v2) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (vmul(all_0_8_8, v0) = v4 & vplus(v1, v6) = v7 & vplus(v1, v0) = v5 & vplus(all_0_8_8, v0) = v6 & ( ~ (v5 = v4) | v7 = v3))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v2) = v3) | ~ (vplus(v0, all_0_8_8) = v2) | ? [v4] : ? [v5] : ? [v6] : (vmul(all_0_8_8, v0) = v4 & vplus(v5, all_0_8_8) = v6 & vplus(v1, v0) = v5 & ( ~ (v5 = v4) | v6 = v3))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v2) = v3) | ~ (vplus(all_0_8_8, v0) = v2) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (vsucc(v6) = v7 & vmul(all_0_8_8, v0) = v4 & vplus(v1, v7) = v8 & vplus(v1, v0) = v5 & vplus(vd411, v0) = v6 & ( ~ (v5 = v4) | v8 = v3))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v2) = v3) | ~ (vplus(all_0_8_8, v0) = v2) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (vmul(all_0_8_8, v0) = v4 & vplus(v1, v6) = v7 & vplus(v1, v0) = v5 & vplus(v0, all_0_8_8) = v6 & ( ~ (v5 = v4) | v7 = v3))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (vplus(v1, v3) = v0) | ~ (vplus(v0, v2) = v1)) & ? [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (vplus(v2, v1) = v3) | ? [v4] : ( ~ (v4 = v3) & vplus(v2, v0) = v4)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (vskolem2(v2) = v1) | ~ (vskolem2(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (vsucc(v2) = v1) | ~ (vsucc(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (vsucc(v1) = v2) | ~ (vsucc(v0) = v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v0) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (vsucc(v4) = v5 & vsucc(v0) = v7 & vmul(all_0_8_8, v0) = v3 & vplus(v1, v8) = v9 & vplus(v1, v5) = v6 & vplus(vd411, v7) = v8 & vplus(vd411, v0) = v4 & ( ~ (v3 = v2) | v9 = v6))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v0) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (vsucc(v6) = v7 & vmul(all_0_8_8, v0) = v3 & vplus(v1, v7) = v8 & vplus(v1, v4) = v5 & vplus(all_0_8_8, v0) = v4 & vplus(vd411, v0) = v6 & ( ~ (v3 = v2) | v8 = v5))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v0) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (vsucc(v0) = v5 & vmul(all_0_8_8, v0) = v3 & vmul(vd411, v5) = v7 & vplus(v7, v5) = v8 & vplus(v4, v5) = v6 & vplus(v1, vd411) = v4 & ( ~ (v3 = v2) | v8 = v6))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v0) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (vsucc(v0) = v4 & vmul(all_0_8_8, v0) = v3 & vplus(v7, v4) = v8 & vplus(v1, v5) = v6 & vplus(v1, vd411) = v7 & vplus(vd411, v4) = v5 & ( ~ (v3 = v2) | v8 = v6))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v0) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : (vmul(all_0_8_8, v0) = v3 & vplus(v1, v6) = v7 & vplus(v1, v4) = v5 & vplus(v0, all_0_8_8) = v4 & vplus(all_0_8_8, v0) = v6 & ( ~ (v3 = v2) | v7 = v5))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v0) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : (vsucc(v0) = v4 & vmul(all_0_8_8, v4) = v5 & vmul(all_0_8_8, v0) = v3 & vplus(v3, all_0_8_8) = v6 & ( ~ (v3 = v2) | v6 = v5))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v0) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : (vmul(all_0_8_8, v0) = v3 & vplus(v2, all_0_8_8) = v4 & vplus(v1, v5) = v6 & vplus(v0, all_0_8_8) = v5 & ( ~ (v3 = v2) | v6 = v4))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v0) = v2) | ? [v3] : ? [v4] : ? [v5] : (vmul(all_0_8_8, v0) = v3 & vplus(v3, all_0_8_8) = v4 & vplus(v2, all_0_8_8) = v5 & ( ~ (v3 = v2) | v5 = v4))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (vplus(v1, v2) = v0) | less(v1, v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (vplus(v1, v0) = v2) | vplus(v0, v1) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (vplus(v1, v1) = v2) | ~ greater(v0, v1) | geq(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (vplus(v1, v1) = v2) | ~ less(v0, v2) | leq(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (vplus(v0, v2) = v1) | greater(v1, v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (vplus(v0, v1) = v2) | vplus(v1, v0) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (vplus(v0, v1) = v2) | greater(v2, v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (vplus(v0, v1) = v2) | ? [v3] : ? [v4] : (vsucc(v2) = v4 & vsucc(v1) = v3 & vplus(v0, v3) = v4)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (vplus(v0, v1) = v2) | ? [v3] : ? [v4] : (vsucc(v2) = v4 & vsucc(v0) = v3 & vplus(v3, v1) = v4)) & ! [v0] : ! [v1] : ! [v2] : ( ~ leq(v1, v2) | ~ leq(v0, v1) | leq(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ leq(v1, v2) | ~ less(v0, v1) | less(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ leq(v0, v1) | ~ less(v1, v2) | less(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ less(v1, v2) | ~ less(v0, v1) | less(v0, v2)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (vmul(v0, v1) = v1)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (vmul(v1, v0) = v1)) & ! [v0] : ! [v1] : (v1 = v0 | ~ geq(v1, v0) | greater(v1, v0)) & ! [v0] : ! [v1] : (v1 = v0 | ~ leq(v1, v0) | less(v1, v0)) & ! [v0] : ! [v1] : (v0 = v1 | ~ (vskolem2(v0) = v1) | vsucc(v1) = v0) & ! [v0] : ! [v1] : ( ~ (vsucc(v0) = v1) | vplus(v0, v1) = v1) & ! [v0] : ! [v1] : ( ~ (vsucc(v0) = v1) | vplus(v1, v0) = v1) & ! [v0] : ! [v1] : ( ~ (vsucc(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (vmul(all_0_8_8, v1) = v5 & vmul(all_0_8_8, v0) = v2 & vmul(vd411, v0) = v3 & vplus(v3, v0) = v4 & vplus(v2, all_0_8_8) = v6 & ( ~ (v4 = v2) | v6 = v5))) & ! [v0] : ! [v1] : ( ~ (vmul(all_0_8_8, v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (vsucc(v4) = v5 & vsucc(v0) = v7 & vmul(vd411, v0) = v2 & vplus(v2, v8) = v9 & vplus(v2, v5) = v6 & vplus(v2, v0) = v3 & vplus(vd411, v7) = v8 & vplus(vd411, v0) = v4 & ( ~ (v3 = v1) | v9 = v6))) & ! [v0] : ! [v1] : ( ~ (vmul(all_0_8_8, v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (vsucc(v6) = v7 & vmul(vd411, v0) = v2 & vplus(v2, v7) = v8 & vplus(v2, v4) = v5 & vplus(v2, v0) = v3 & vplus(all_0_8_8, v0) = v4 & vplus(vd411, v0) = v6 & ( ~ (v3 = v1) | v8 = v5))) & ! [v0] : ! [v1] : ( ~ (vmul(all_0_8_8, v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (vsucc(v0) = v5 & vmul(vd411, v5) = v7 & vmul(vd411, v0) = v2 & vplus(v7, v5) = v8 & vplus(v4, v5) = v6 & vplus(v2, v0) = v3 & vplus(v2, vd411) = v4 & ( ~ (v3 = v1) | v8 = v6))) & ! [v0] : ! [v1] : ( ~ (vmul(all_0_8_8, v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (vsucc(v0) = v4 & vmul(vd411, v0) = v2 & vplus(v7, v4) = v8 & vplus(v2, v5) = v6 & vplus(v2, v0) = v3 & vplus(v2, vd411) = v7 & vplus(vd411, v4) = v5 & ( ~ (v3 = v1) | v8 = v6))) & ! [v0] : ! [v1] : ( ~ (vmul(all_0_8_8, v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : (vmul(vd411, v0) = v2 & vplus(v2, v6) = v7 & vplus(v2, v4) = v5 & vplus(v2, v0) = v3 & vplus(v0, all_0_8_8) = v4 & vplus(all_0_8_8, v0) = v6 & ( ~ (v3 = v1) | v7 = v5))) & ! [v0] : ! [v1] : ( ~ (vmul(all_0_8_8, v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (vsucc(v0) = v4 & vmul(all_0_8_8, v4) = v5 & vmul(vd411, v0) = v2 & vplus(v2, v0) = v3 & vplus(v1, all_0_8_8) = v6 & ( ~ (v3 = v1) | v6 = v5))) & ! [v0] : ! [v1] : ( ~ (vmul(all_0_8_8, v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (vmul(vd411, v0) = v2 & vplus(v3, all_0_8_8) = v4 & vplus(v2, v5) = v6 & vplus(v2, v0) = v3 & vplus(v0, all_0_8_8) = v5 & ( ~ (v3 = v1) | v6 = v4))) & ! [v0] : ! [v1] : ( ~ (vmul(all_0_8_8, v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (vmul(vd411, v0) = v2 & vplus(v3, all_0_8_8) = v5 & vplus(v2, v0) = v3 & vplus(v1, all_0_8_8) = v4 & ( ~ (v3 = v1) | v5 = v4))) & ! [v0] : ! [v1] : ~ (vplus(v0, v1) = v1) & ! [v0] : ! [v1] : ~ (vplus(v0, v1) = v0) & ! [v0] : ! [v1] : ( ~ (vplus(v0, v1) = v1) | vsucc(v0) = v1) & ! [v0] : ! [v1] : ( ~ (vplus(v1, v0) = v1) | vsucc(v0) = v1) & ! [v0] : ! [v1] : ( ~ geq(v0, v1) | leq(v1, v0)) & ! [v0] : ! [v1] : ( ~ greater(v1, v0) | geq(v1, v0)) & ! [v0] : ! [v1] : ( ~ greater(v1, v0) | ? [v2] : vplus(v0, v2) = v1) & ! [v0] : ! [v1] : ( ~ greater(v0, v1) | ~ less(v0, v1)) & ! [v0] : ! [v1] : ( ~ greater(v0, v1) | less(v1, v0)) & ! [v0] : ! [v1] : ( ~ leq(v0, v1) | geq(v1, v0)) & ! [v0] : ! [v1] : ( ~ less(v1, v0) | leq(v1, v0)) & ! [v0] : ! [v1] : ( ~ less(v1, v0) | ? [v2] : vplus(v1, v2) = v0) & ! [v0] : ! [v1] : ( ~ less(v0, v1) | greater(v1, v0)) & ! [v0] : ~ (vsucc(v0) = v0) & ! [v0] : ~ (vsucc(v0) = v1) & ! [v0] : ~ greater(v0, v0) & ! [v0] : ~ less(v0, v0) & ? [v0] : ? [v1] : (v1 = v0 | greater(v0, v1) | less(v0, v1)) & ? [v0] : ? [v1] : (v1 = v0 | ? [v2] : ? [v3] : ((v3 = v1 & vplus(v0, v2) = v1) | (v3 = v0 & vplus(v1, v2) = v0))) & ? [v0] : geq(v0, v0) & ? [v0] : geq(v0, v1) & ? [v0] : leq(v0, v0) % 12.18/3.45 | % 12.18/3.45 | Applying alpha-rule on (1) yields: % 12.18/3.45 | (2) ! [v0] : ! [v1] : ! [v2] : ( ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v0) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (vsucc(v0) = v5 & vmul(all_0_8_8, v0) = v3 & vmul(vd411, v5) = v7 & vplus(v7, v5) = v8 & vplus(v4, v5) = v6 & vplus(v1, vd411) = v4 & ( ~ (v3 = v2) | v8 = v6))) % 12.18/3.45 | (3) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (vsucc(v0) = v2) | ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v3) = v4) | ~ (vplus(vd411, v2) = v3) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (vsucc(v7) = v8 & vmul(all_0_8_8, v0) = v5 & vplus(v1, v8) = v9 & vplus(v1, v0) = v6 & vplus(vd411, v0) = v7 & ( ~ (v6 = v5) | v9 = v4))) % 12.18/3.45 | (4) ! [v0] : ! [v1] : ( ~ (vplus(v0, v1) = v1) | vsucc(v0) = v1) % 12.18/3.45 | (5) ! [v0] : ! [v1] : ( ~ (vsucc(v0) = v1) | vplus(v0, v1) = v1) % 12.18/3.45 | (6) ! [v0] : ! [v1] : ( ~ (vmul(all_0_8_8, v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (vsucc(v4) = v5 & vsucc(v0) = v7 & vmul(vd411, v0) = v2 & vplus(v2, v8) = v9 & vplus(v2, v5) = v6 & vplus(v2, v0) = v3 & vplus(vd411, v7) = v8 & vplus(vd411, v0) = v4 & ( ~ (v3 = v1) | v9 = v6))) % 12.18/3.45 | (7) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v2) = v3) | ~ (vplus(all_0_8_8, v0) = v2) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (vsucc(v6) = v7 & vmul(all_0_8_8, v0) = v4 & vplus(v1, v7) = v8 & vplus(v1, v0) = v5 & vplus(vd411, v0) = v6 & ( ~ (v5 = v4) | v8 = v3))) % 12.18/3.45 | (8) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (vsucc(v1) = v2) | ~ (vsucc(v0) = v2)) % 12.18/3.45 | (9) ! [v0] : ! [v1] : ! [v2] : ( ~ (vplus(v1, v2) = v0) | less(v1, v0)) % 12.18/3.45 | (10) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (vplus(v1, v3) = v5) | ~ (vplus(v0, v2) = v4) | ~ geq(v2, v3) | ~ geq(v0, v1) | geq(v4, v5)) % 12.18/3.45 | (11) ! [v0] : ! [v1] : ( ~ (vplus(v1, v0) = v1) | vsucc(v0) = v1) % 12.18/3.45 | (12) ! [v0] : ! [v1] : ( ~ (vsucc(v0) = v1) | vplus(v1, v0) = v1) % 12.18/3.45 | (13) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (vsucc(v0) = v2) | ~ (vplus(v2, v1) = v3) | ? [v4] : (vsucc(v4) = v3 & vplus(v0, v1) = v4)) % 12.18/3.45 | (14) ! [v0] : ! [v1] : ( ~ leq(v0, v1) | geq(v1, v0)) % 12.18/3.45 | (15) ! [v0] : ! [v1] : ( ~ geq(v0, v1) | leq(v1, v0)) % 12.18/3.45 | (16) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (vsucc(v0) = v2) | ~ (vmul(vd411, v0) = v1) | ~ (vplus(v3, v2) = v4) | ~ (vplus(v1, vd411) = v3) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (vmul(all_0_8_8, v0) = v5 & vplus(v1, v7) = v8 & vplus(v1, v0) = v6 & vplus(vd411, v2) = v7 & ( ~ (v6 = v5) | v8 = v4))) % 12.18/3.46 | (17) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (vsucc(v0) = v1) | ~ (vmul(vd411, v1) = v2) | ~ (vplus(v2, v1) = v3) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (vmul(all_0_8_8, v0) = v4 & vmul(vd411, v0) = v5 & vplus(v7, v1) = v8 & vplus(v5, v0) = v6 & vplus(v5, vd411) = v7 & ( ~ (v6 = v4) | v8 = v3))) % 12.18/3.46 | (18) ! [v0] : ! [v1] : ( ~ greater(v1, v0) | geq(v1, v0)) % 12.18/3.46 | (19) ? [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (vplus(v2, v1) = v3) | ? [v4] : ( ~ (v4 = v3) & vplus(v2, v0) = v4)) % 12.18/3.46 | (20) ! [v0] : ~ less(v0, v0) % 12.18/3.46 | (21) ! [v0] : ! [v1] : ( ~ (vmul(all_0_8_8, v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (vsucc(v0) = v4 & vmul(vd411, v0) = v2 & vplus(v7, v4) = v8 & vplus(v2, v5) = v6 & vplus(v2, v0) = v3 & vplus(v2, vd411) = v7 & vplus(vd411, v4) = v5 & ( ~ (v3 = v1) | v8 = v6))) % 12.31/3.46 | (22) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (vsucc(v0) = v3) | ~ (vmul(vd411, v0) = v1) | ~ (vplus(v2, v3) = v4) | ~ (vplus(v1, vd411) = v2) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (vmul(all_0_8_8, v0) = v5 & vmul(vd411, v3) = v7 & vplus(v7, v3) = v8 & vplus(v1, v0) = v6 & ( ~ (v6 = v5) | v8 = v4))) % 12.31/3.46 | (23) ! [v0] : ! [v1] : ! [v2] : ( ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v0) = v2) | ? [v3] : ? [v4] : ? [v5] : (vmul(all_0_8_8, v0) = v3 & vplus(v3, all_0_8_8) = v4 & vplus(v2, all_0_8_8) = v5 & ( ~ (v3 = v2) | v5 = v4))) % 12.31/3.46 | (24) ! [v0] : ! [v1] : ! [v2] : ( ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v0) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (vsucc(v4) = v5 & vsucc(v0) = v7 & vmul(all_0_8_8, v0) = v3 & vplus(v1, v8) = v9 & vplus(v1, v5) = v6 & vplus(vd411, v7) = v8 & vplus(vd411, v0) = v4 & ( ~ (v3 = v2) | v9 = v6))) % 12.31/3.46 | (25) ! [v0] : ! [v1] : ! [v2] : ( ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v0) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : (vmul(all_0_8_8, v0) = v3 & vplus(v2, all_0_8_8) = v4 & vplus(v1, v5) = v6 & vplus(v0, all_0_8_8) = v5 & ( ~ (v3 = v2) | v6 = v4))) % 12.31/3.46 | (26) ! [v0] : ! [v1] : ! [v2] : ( ~ (vplus(v0, v1) = v2) | ? [v3] : ? [v4] : (vsucc(v2) = v4 & vsucc(v1) = v3 & vplus(v0, v3) = v4)) % 12.31/3.46 | (27) ! [v0] : ! [v1] : ( ~ less(v1, v0) | ? [v2] : vplus(v1, v2) = v0) % 12.31/3.46 | (28) ! [v0] : ! [v1] : ( ~ (vmul(all_0_8_8, v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (vsucc(v6) = v7 & vmul(vd411, v0) = v2 & vplus(v2, v7) = v8 & vplus(v2, v4) = v5 & vplus(v2, v0) = v3 & vplus(all_0_8_8, v0) = v4 & vplus(vd411, v0) = v6 & ( ~ (v3 = v1) | v8 = v5))) % 12.31/3.46 | (29) ! [v0] : ! [v1] : (v1 = v0 | ~ (vmul(v1, v0) = v1)) % 12.31/3.46 | (30) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (vsucc(v2) = v1) | ~ (vsucc(v2) = v0)) % 12.31/3.46 | (31) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (vplus(v0, v1) = v3) | ~ (vplus(v0, v1) = v2)) % 12.31/3.46 | (32) ! [v0] : ! [v1] : ( ~ greater(v0, v1) | ~ less(v0, v1)) % 12.31/3.46 | (33) ! [v0] : ! [v1] : ! [v2] : ( ~ (vplus(v0, v1) = v2) | ? [v3] : ? [v4] : (vsucc(v2) = v4 & vsucc(v0) = v3 & vplus(v3, v1) = v4)) % 12.31/3.46 | (34) vsucc(vd411) = all_0_8_8 % 12.31/3.46 | (35) ! [v0] : ! [v1] : ! [v2] : ( ~ less(v1, v2) | ~ less(v0, v1) | less(v0, v2)) % 12.31/3.46 | (36) vmul(vd411, all_0_6_6) = all_0_4_4 % 12.31/3.46 | (37) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (vsucc(v0) = v2) | ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v3) = v4) | ~ (vplus(vd411, v2) = v3) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (vmul(all_0_8_8, v0) = v5 & vplus(v7, v2) = v8 & vplus(v1, v0) = v6 & vplus(v1, vd411) = v7 & ( ~ (v6 = v5) | v8 = v4))) % 12.31/3.46 | (38) ? [v0] : ? [v1] : (v1 = v0 | greater(v0, v1) | less(v0, v1)) % 12.31/3.46 | (39) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (vplus(v1, v2) = v4) | ~ (vplus(v0, v2) = v3) | ~ less(v0, v1) | less(v3, v4)) % 12.31/3.46 | (40) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (vplus(v1, v2) = v4) | ~ (vplus(v0, v2) = v3) | ~ less(v3, v4) | less(v0, v1)) % 12.31/3.46 | (41) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (vmul(v3, v2) = v1) | ~ (vmul(v3, v2) = v0)) % 12.31/3.46 | (42) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (vmul(v0, v1) = v2) | ~ (vplus(v2, v0) = v3) | ? [v4] : (vsucc(v1) = v4 & vmul(v0, v4) = v3)) % 12.31/3.46 | (43) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (vplus(v3, v2) = v1) | ~ (vplus(v3, v2) = v0)) % 12.31/3.46 | (44) ! [v0] : ! [v1] : ! [v2] : ( ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v0) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : (vsucc(v0) = v4 & vmul(all_0_8_8, v4) = v5 & vmul(all_0_8_8, v0) = v3 & vplus(v3, all_0_8_8) = v6 & ( ~ (v3 = v2) | v6 = v5))) % 12.31/3.47 | (45) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (vplus(v1, v2) = v3) | ~ (vplus(v0, v3) = v4) | ? [v5] : (vplus(v5, v2) = v4 & vplus(v0, v1) = v5)) % 12.31/3.47 | (46) ! [v0] : ! [v1] : ( ~ (vmul(all_0_8_8, v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (vsucc(v0) = v4 & vmul(all_0_8_8, v4) = v5 & vmul(vd411, v0) = v2 & vplus(v2, v0) = v3 & vplus(v1, all_0_8_8) = v6 & ( ~ (v3 = v1) | v6 = v5))) % 12.31/3.47 | (47) vmul(vd411, v1) = all_0_7_7 % 12.31/3.47 | (48) ! [v0] : ! [v1] : ! [v2] : ( ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v0) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (vsucc(v6) = v7 & vmul(all_0_8_8, v0) = v3 & vplus(v1, v7) = v8 & vplus(v1, v4) = v5 & vplus(all_0_8_8, v0) = v4 & vplus(vd411, v0) = v6 & ( ~ (v3 = v2) | v8 = v5))) % 12.31/3.48 | (49) ? [v0] : ? [v1] : (v1 = v0 | ? [v2] : ? [v3] : ((v3 = v1 & vplus(v0, v2) = v1) | (v3 = v0 & vplus(v1, v2) = v0))) % 12.31/3.48 | (50) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v2) = v3) | ~ (vplus(v0, all_0_8_8) = v2) | ? [v4] : ? [v5] : ? [v6] : (vmul(all_0_8_8, v0) = v4 & vplus(v5, all_0_8_8) = v6 & vplus(v1, v0) = v5 & ( ~ (v5 = v4) | v6 = v3))) % 12.31/3.48 | (51) vplus(all_0_4_4, all_0_6_6) = all_0_5_5 % 12.31/3.48 | (52) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (vsucc(v2) = v3) | ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v3) = v4) | ~ (vplus(vd411, v0) = v2) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : (vmul(all_0_8_8, v0) = v5 & vplus(v1, v7) = v8 & vplus(v1, v0) = v6 & vplus(all_0_8_8, v0) = v7 & ( ~ (v6 = v5) | v8 = v4))) % 12.31/3.48 | (53) ! [v0] : ! [v1] : ! [v2] : ( ~ leq(v1, v2) | ~ less(v0, v1) | less(v0, v2)) % 12.31/3.48 | (54) ! [v0] : ! [v1] : ( ~ less(v0, v1) | greater(v1, v0)) % 12.31/3.48 | (55) ! [v0] : ! [v1] : ( ~ greater(v0, v1) | less(v1, v0)) % 12.31/3.48 | (56) ? [v0] : geq(v0, v1) % 12.31/3.48 | (57) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (vplus(v1, v3) = v5) | ~ (vplus(v0, v2) = v4) | ~ geq(v0, v1) | ~ greater(v2, v3) | greater(v4, v5)) % 12.31/3.48 | (58) vmul(all_0_8_8, all_0_6_6) = all_0_5_5 % 12.31/3.48 | (59) ! [v0] : ! [v1] : ( ~ (vmul(all_0_8_8, v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (vmul(vd411, v0) = v2 & vplus(v3, all_0_8_8) = v4 & vplus(v2, v5) = v6 & vplus(v2, v0) = v3 & vplus(v0, all_0_8_8) = v5 & ( ~ (v3 = v1) | v6 = v4))) % 12.31/3.48 | (60) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v2) = v3) | ~ (vplus(all_0_8_8, v0) = v2) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (vmul(all_0_8_8, v0) = v4 & vplus(v1, v6) = v7 & vplus(v1, v0) = v5 & vplus(v0, all_0_8_8) = v6 & ( ~ (v5 = v4) | v7 = v3))) % 12.31/3.48 | (61) ? [v0] : leq(v0, v0) % 12.31/3.48 | (62) ! [v0] : ! [v1] : ! [v2] : ( ~ (vplus(v1, v1) = v2) | ~ less(v0, v2) | leq(v0, v1)) % 12.31/3.49 | (63) vplus(all_0_1_1, all_0_3_3) = all_0_0_0 % 12.31/3.49 | (64) ! [v0] : ! [v1] : ( ~ less(v1, v0) | leq(v1, v0)) % 12.31/3.49 | (65) ! [v0] : ~ (vsucc(v0) = v0) % 12.31/3.49 | (66) ! [v0] : ! [v1] : ! [v2] : ( ~ (vplus(v0, v1) = v2) | greater(v2, v0)) % 12.31/3.49 | (67) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (vsucc(v2) = v3) | ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v3) = v4) | ~ (vplus(vd411, v0) = v2) | ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (vsucc(v0) = v7 & vmul(all_0_8_8, v0) = v5 & vplus(v1, v8) = v9 & vplus(v1, v0) = v6 & vplus(vd411, v7) = v8 & ( ~ (v6 = v5) | v9 = v4))) % 12.31/3.49 | (68) vplus(all_0_7_7, v1) = all_0_8_8 % 12.31/3.49 | (69) ! [v0] : ! [v1] : ~ (vplus(v0, v1) = v0) % 12.31/3.49 | (70) ! [v0] : ! [v1] : ( ~ greater(v1, v0) | ? [v2] : vplus(v0, v2) = v1) % 12.31/3.49 | (71) ! [v0] : ! [v1] : (v0 = v1 | ~ (vskolem2(v0) = v1) | vsucc(v1) = v0) % 12.31/3.49 | (72) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (vplus(v1, v2) = v4) | ~ (vplus(v0, v2) = v3) | ~ greater(v0, v1) | greater(v3, v4)) % 12.31/3.49 | (73) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (vplus(v1, v2) = v4) | ~ (vplus(v0, v2) = v3) | ~ greater(v3, v4) | greater(v0, v1)) % 12.31/3.49 | (74) ! [v0] : ! [v1] : ( ~ (vmul(all_0_8_8, v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : (vmul(vd411, v0) = v2 & vplus(v2, v6) = v7 & vplus(v2, v4) = v5 & vplus(v2, v0) = v3 & vplus(v0, all_0_8_8) = v4 & vplus(all_0_8_8, v0) = v6 & ( ~ (v3 = v1) | v7 = v5))) % 12.31/3.49 | (75) vmul(all_0_8_8, all_0_3_3) = all_0_2_2 % 12.31/3.49 | (76) vmul(all_0_8_8, v1) = all_0_8_8 % 12.31/3.49 | (77) ! [v0] : ! [v1] : ( ~ (vmul(all_0_8_8, v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : (vmul(vd411, v0) = v2 & vplus(v3, all_0_8_8) = v5 & vplus(v2, v0) = v3 & vplus(v1, all_0_8_8) = v4 & ( ~ (v3 = v1) | v5 = v4))) % 12.31/3.49 | (78) vsucc(all_0_6_6) = all_0_3_3 % 12.31/3.49 | (79) ! [v0] : ! [v1] : ! [v2] : ( ~ leq(v0, v1) | ~ less(v1, v2) | less(v0, v2)) % 12.31/3.49 | (80) ! [v0] : ! [v1] : (v1 = v0 | ~ leq(v1, v0) | less(v1, v0)) % 12.31/3.49 | (81) ! [v0] : ! [v1] : ~ (vplus(v0, v1) = v1) % 12.31/3.49 | (82) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (vskolem2(v2) = v1) | ~ (vskolem2(v2) = v0)) % 12.31/3.49 | (83) ! [v0] : ! [v1] : ! [v2] : ( ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v0) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : (vmul(all_0_8_8, v0) = v3 & vplus(v1, v6) = v7 & vplus(v1, v4) = v5 & vplus(v0, all_0_8_8) = v4 & vplus(all_0_8_8, v0) = v6 & ( ~ (v3 = v2) | v7 = v5))) % 12.31/3.49 | (84) ! [v0] : ! [v1] : (v1 = v0 | ~ (vmul(v0, v1) = v1)) % 12.31/3.49 | (85) ~ (all_0_0_0 = all_0_2_2) % 12.31/3.49 | (86) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v2) = v3) | ~ (vplus(v0, all_0_8_8) = v2) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : (vmul(all_0_8_8, v0) = v4 & vplus(v1, v6) = v7 & vplus(v1, v0) = v5 & vplus(all_0_8_8, v0) = v6 & ( ~ (v5 = v4) | v7 = v3))) % 12.31/3.49 | (87) ! [v0] : ! [v1] : ! [v2] : ( ~ (vplus(v0, v1) = v2) | vplus(v1, v0) = v2) % 12.31/3.49 | (88) ! [v0] : ! [v1] : ! [v2] : ( ~ (vplus(v1, v0) = v2) | vplus(v0, v1) = v2) % 12.31/3.49 | (89) vsucc(all_0_7_7) = all_0_8_8 % 12.31/3.49 | (90) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (vplus(v1, v3) = v5) | ~ (vplus(v0, v2) = v4) | ~ greater(v2, v3) | ~ greater(v0, v1) | greater(v4, v5)) % 12.31/3.49 | (91) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (vsucc(v1) = v2) | ~ (vmul(v0, v2) = v3) | ? [v4] : (vmul(v0, v1) = v4 & vplus(v4, v0) = v3)) % 12.31/3.49 | (92) vmul(vd411, all_0_3_3) = all_0_1_1 % 12.31/3.49 | (93) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (vplus(v3, v2) = v4) | ~ (vplus(v0, v1) = v3) | ? [v5] : (vplus(v1, v2) = v5 & vplus(v0, v5) = v4)) % 12.31/3.49 | (94) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (vsucc(v1) = v2) | ~ (vplus(v0, v2) = v3) | ? [v4] : (vsucc(v4) = v3 & vplus(v0, v1) = v4)) % 12.31/3.49 | (95) ! [v0] : ! [v1] : ! [v2] : ( ~ leq(v1, v2) | ~ leq(v0, v1) | leq(v0, v2)) % 12.31/3.49 | (96) ! [v0] : ! [v1] : ( ~ (vmul(all_0_8_8, v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (vsucc(v0) = v5 & vmul(vd411, v5) = v7 & vmul(vd411, v0) = v2 & vplus(v7, v5) = v8 & vplus(v4, v5) = v6 & vplus(v2, v0) = v3 & vplus(v2, vd411) = v4 & ( ~ (v3 = v1) | v8 = v6))) % 12.31/3.49 | (97) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (vplus(v1, v2) = v3) | ~ (vplus(v0, v2) = v3)) % 12.31/3.49 | (98) ? [v0] : geq(v0, v0) % 12.31/3.49 | (99) ! [v0] : ! [v1] : ( ~ (vsucc(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (vmul(all_0_8_8, v1) = v5 & vmul(all_0_8_8, v0) = v2 & vmul(vd411, v0) = v3 & vplus(v3, v0) = v4 & vplus(v2, all_0_8_8) = v6 & ( ~ (v4 = v2) | v6 = v5))) % 12.31/3.49 | (100) ! [v0] : ! [v1] : ! [v2] : ( ~ (vplus(v0, v2) = v1) | greater(v1, v0)) % 12.31/3.49 | (101) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (vplus(v1, v3) = v5) | ~ (vplus(v0, v2) = v4) | ~ geq(v2, v3) | ~ greater(v0, v1) | greater(v4, v5)) % 12.31/3.49 | (102) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (vplus(v1, v3) = v0) | ~ (vplus(v0, v2) = v1)) % 12.31/3.49 | (103) ! [v0] : ~ (vsucc(v0) = v1) % 12.31/3.49 | (104) ! [v0] : ! [v1] : ! [v2] : ( ~ (vplus(v1, v1) = v2) | ~ greater(v0, v1) | geq(v0, v2)) % 12.31/3.49 | (105) ! [v0] : ! [v1] : ! [v2] : ( ~ (vmul(vd411, v0) = v1) | ~ (vplus(v1, v0) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (vsucc(v0) = v4 & vmul(all_0_8_8, v0) = v3 & vplus(v7, v4) = v8 & vplus(v1, v5) = v6 & vplus(v1, vd411) = v7 & vplus(vd411, v4) = v5 & ( ~ (v3 = v2) | v8 = v6))) % 12.31/3.49 | (106) ! [v0] : ~ greater(v0, v0) % 12.31/3.50 | (107) ! [v0] : ! [v1] : (v1 = v0 | ~ geq(v1, v0) | greater(v1, v0)) % 12.31/3.50 | % 12.31/3.50 | Instantiating formula (99) with all_0_3_3, all_0_6_6 and discharging atoms vsucc(all_0_6_6) = all_0_3_3, yields: % 12.31/3.50 | (108) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (vmul(all_0_8_8, all_0_3_3) = v3 & vmul(all_0_8_8, all_0_6_6) = v0 & vmul(vd411, all_0_6_6) = v1 & vplus(v1, all_0_6_6) = v2 & vplus(v0, all_0_8_8) = v4 & ( ~ (v2 = v0) | v4 = v3)) % 12.31/3.50 | % 12.31/3.50 | Instantiating formula (91) with all_0_2_2, all_0_3_3, all_0_6_6, all_0_8_8 and discharging atoms vsucc(all_0_6_6) = all_0_3_3, vmul(all_0_8_8, all_0_3_3) = all_0_2_2, yields: % 12.31/3.50 | (109) ? [v0] : (vmul(all_0_8_8, all_0_6_6) = v0 & vplus(v0, all_0_8_8) = all_0_2_2) % 12.31/3.50 | % 12.31/3.50 | Instantiating formula (6) with all_0_2_2, all_0_3_3 and discharging atoms vmul(all_0_8_8, all_0_3_3) = all_0_2_2, yields: % 12.31/3.50 | (110) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : (vsucc(v2) = v3 & vsucc(all_0_3_3) = v5 & vmul(vd411, all_0_3_3) = v0 & vplus(v0, v6) = v7 & vplus(v0, v3) = v4 & vplus(v0, all_0_3_3) = v1 & vplus(vd411, v5) = v6 & vplus(vd411, all_0_3_3) = v2 & ( ~ (v1 = all_0_2_2) | v7 = v4)) % 12.31/3.50 | % 12.31/3.50 | Instantiating formula (28) with all_0_2_2, all_0_3_3 and discharging atoms vmul(all_0_8_8, all_0_3_3) = all_0_2_2, yields: % 12.31/3.50 | (111) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (vsucc(v4) = v5 & vmul(vd411, all_0_3_3) = v0 & vplus(v0, v5) = v6 & vplus(v0, v2) = v3 & vplus(v0, all_0_3_3) = v1 & vplus(all_0_8_8, all_0_3_3) = v2 & vplus(vd411, all_0_3_3) = v4 & ( ~ (v1 = all_0_2_2) | v6 = v3)) % 12.31/3.50 | % 12.31/3.50 | Instantiating formula (96) with all_0_2_2, all_0_3_3 and discharging atoms vmul(all_0_8_8, all_0_3_3) = all_0_2_2, yields: % 12.31/3.50 | (112) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (vsucc(all_0_3_3) = v3 & vmul(vd411, v3) = v5 & vmul(vd411, all_0_3_3) = v0 & vplus(v5, v3) = v6 & vplus(v2, v3) = v4 & vplus(v0, all_0_3_3) = v1 & vplus(v0, vd411) = v2 & ( ~ (v1 = all_0_2_2) | v6 = v4)) % 12.31/3.50 | % 12.31/3.50 | Instantiating formula (21) with all_0_2_2, all_0_3_3 and discharging atoms vmul(all_0_8_8, all_0_3_3) = all_0_2_2, yields: % 12.31/3.50 | (113) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (vsucc(all_0_3_3) = v2 & vmul(vd411, all_0_3_3) = v0 & vplus(v5, v2) = v6 & vplus(v0, v3) = v4 & vplus(v0, all_0_3_3) = v1 & vplus(v0, vd411) = v5 & vplus(vd411, v2) = v3 & ( ~ (v1 = all_0_2_2) | v6 = v4)) % 12.31/3.50 | % 12.31/3.50 | Instantiating formula (74) with all_0_2_2, all_0_3_3 and discharging atoms vmul(all_0_8_8, all_0_3_3) = all_0_2_2, yields: % 12.31/3.50 | (114) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : (vmul(vd411, all_0_3_3) = v0 & vplus(v0, v4) = v5 & vplus(v0, v2) = v3 & vplus(v0, all_0_3_3) = v1 & vplus(all_0_3_3, all_0_8_8) = v2 & vplus(all_0_8_8, all_0_3_3) = v4 & ( ~ (v1 = all_0_2_2) | v5 = v3)) % 12.31/3.50 | % 12.31/3.50 | Instantiating formula (46) with all_0_2_2, all_0_3_3 and discharging atoms vmul(all_0_8_8, all_0_3_3) = all_0_2_2, yields: % 12.31/3.50 | (115) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (vsucc(all_0_3_3) = v2 & vmul(all_0_8_8, v2) = v3 & vmul(vd411, all_0_3_3) = v0 & vplus(v0, all_0_3_3) = v1 & vplus(all_0_2_2, all_0_8_8) = v4 & ( ~ (v1 = all_0_2_2) | v4 = v3)) % 12.31/3.50 | % 12.31/3.50 | Instantiating formula (59) with all_0_2_2, all_0_3_3 and discharging atoms vmul(all_0_8_8, all_0_3_3) = all_0_2_2, yields: % 12.31/3.50 | (116) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (vmul(vd411, all_0_3_3) = v0 & vplus(v1, all_0_8_8) = v2 & vplus(v0, v3) = v4 & vplus(v0, all_0_3_3) = v1 & vplus(all_0_3_3, all_0_8_8) = v3 & ( ~ (v1 = all_0_2_2) | v4 = v2)) % 12.31/3.50 | % 12.31/3.50 | Instantiating formula (77) with all_0_2_2, all_0_3_3 and discharging atoms vmul(all_0_8_8, all_0_3_3) = all_0_2_2, yields: % 12.31/3.50 | (117) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (vmul(vd411, all_0_3_3) = v0 & vplus(v1, all_0_8_8) = v3 & vplus(v0, all_0_3_3) = v1 & vplus(all_0_2_2, all_0_8_8) = v2 & ( ~ (v1 = all_0_2_2) | v3 = v2)) % 12.31/3.50 | % 12.31/3.50 | Instantiating formula (6) with all_0_5_5, all_0_6_6 and discharging atoms vmul(all_0_8_8, all_0_6_6) = all_0_5_5, yields: % 12.31/3.50 | (118) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : (vsucc(v2) = v3 & vsucc(all_0_6_6) = v5 & vmul(vd411, all_0_6_6) = v0 & vplus(v0, v6) = v7 & vplus(v0, v3) = v4 & vplus(v0, all_0_6_6) = v1 & vplus(vd411, v5) = v6 & vplus(vd411, all_0_6_6) = v2 & ( ~ (v1 = all_0_5_5) | v7 = v4)) % 12.31/3.50 | % 12.31/3.50 | Instantiating formula (28) with all_0_5_5, all_0_6_6 and discharging atoms vmul(all_0_8_8, all_0_6_6) = all_0_5_5, yields: % 12.31/3.50 | (119) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (vsucc(v4) = v5 & vmul(vd411, all_0_6_6) = v0 & vplus(v0, v5) = v6 & vplus(v0, v2) = v3 & vplus(v0, all_0_6_6) = v1 & vplus(all_0_8_8, all_0_6_6) = v2 & vplus(vd411, all_0_6_6) = v4 & ( ~ (v1 = all_0_5_5) | v6 = v3)) % 12.31/3.50 | % 12.31/3.50 | Instantiating formula (96) with all_0_5_5, all_0_6_6 and discharging atoms vmul(all_0_8_8, all_0_6_6) = all_0_5_5, yields: % 12.31/3.50 | (120) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (vsucc(all_0_6_6) = v3 & vmul(vd411, v3) = v5 & vmul(vd411, all_0_6_6) = v0 & vplus(v5, v3) = v6 & vplus(v2, v3) = v4 & vplus(v0, all_0_6_6) = v1 & vplus(v0, vd411) = v2 & ( ~ (v1 = all_0_5_5) | v6 = v4)) % 12.31/3.50 | % 12.31/3.50 | Instantiating formula (21) with all_0_5_5, all_0_6_6 and discharging atoms vmul(all_0_8_8, all_0_6_6) = all_0_5_5, yields: % 12.31/3.50 | (121) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (vsucc(all_0_6_6) = v2 & vmul(vd411, all_0_6_6) = v0 & vplus(v5, v2) = v6 & vplus(v0, v3) = v4 & vplus(v0, all_0_6_6) = v1 & vplus(v0, vd411) = v5 & vplus(vd411, v2) = v3 & ( ~ (v1 = all_0_5_5) | v6 = v4)) % 12.31/3.50 | % 12.31/3.50 | Instantiating formula (74) with all_0_5_5, all_0_6_6 and discharging atoms vmul(all_0_8_8, all_0_6_6) = all_0_5_5, yields: % 12.31/3.50 | (122) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : (vmul(vd411, all_0_6_6) = v0 & vplus(v0, v4) = v5 & vplus(v0, v2) = v3 & vplus(v0, all_0_6_6) = v1 & vplus(all_0_6_6, all_0_8_8) = v2 & vplus(all_0_8_8, all_0_6_6) = v4 & ( ~ (v1 = all_0_5_5) | v5 = v3)) % 12.31/3.50 | % 12.31/3.50 | Instantiating formula (46) with all_0_5_5, all_0_6_6 and discharging atoms vmul(all_0_8_8, all_0_6_6) = all_0_5_5, yields: % 12.31/3.50 | (123) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (vsucc(all_0_6_6) = v2 & vmul(all_0_8_8, v2) = v3 & vmul(vd411, all_0_6_6) = v0 & vplus(v0, all_0_6_6) = v1 & vplus(all_0_5_5, all_0_8_8) = v4 & ( ~ (v1 = all_0_5_5) | v4 = v3)) % 12.31/3.51 | % 12.31/3.51 | Instantiating formula (59) with all_0_5_5, all_0_6_6 and discharging atoms vmul(all_0_8_8, all_0_6_6) = all_0_5_5, yields: % 12.31/3.51 | (124) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (vmul(vd411, all_0_6_6) = v0 & vplus(v1, all_0_8_8) = v2 & vplus(v0, v3) = v4 & vplus(v0, all_0_6_6) = v1 & vplus(all_0_6_6, all_0_8_8) = v3 & ( ~ (v1 = all_0_5_5) | v4 = v2)) % 12.31/3.51 | % 12.31/3.51 | Instantiating formula (77) with all_0_5_5, all_0_6_6 and discharging atoms vmul(all_0_8_8, all_0_6_6) = all_0_5_5, yields: % 12.31/3.51 | (125) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (vmul(vd411, all_0_6_6) = v0 & vplus(v1, all_0_8_8) = v3 & vplus(v0, all_0_6_6) = v1 & vplus(all_0_5_5, all_0_8_8) = v2 & ( ~ (v1 = all_0_5_5) | v3 = v2)) % 12.31/3.51 | % 12.31/3.51 | Instantiating formula (91) with all_0_1_1, all_0_3_3, all_0_6_6, vd411 and discharging atoms vsucc(all_0_6_6) = all_0_3_3, vmul(vd411, all_0_3_3) = all_0_1_1, yields: % 12.31/3.51 | (126) ? [v0] : (vmul(vd411, all_0_6_6) = v0 & vplus(v0, vd411) = all_0_1_1) % 12.31/3.51 | % 12.31/3.51 | Instantiating formula (17) with all_0_0_0, all_0_1_1, all_0_3_3, all_0_6_6 and discharging atoms vsucc(all_0_6_6) = all_0_3_3, vmul(vd411, all_0_3_3) = all_0_1_1, vplus(all_0_1_1, all_0_3_3) = all_0_0_0, yields: % 12.31/3.51 | (127) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (vmul(all_0_8_8, all_0_6_6) = v0 & vmul(vd411, all_0_6_6) = v1 & vplus(v3, all_0_3_3) = v4 & vplus(v1, all_0_6_6) = v2 & vplus(v1, vd411) = v3 & ( ~ (v2 = v0) | v4 = all_0_0_0)) % 12.31/3.51 | % 12.31/3.51 | Instantiating formula (24) with all_0_0_0, all_0_1_1, all_0_3_3 and discharging atoms vmul(vd411, all_0_3_3) = all_0_1_1, vplus(all_0_1_1, all_0_3_3) = all_0_0_0, yields: % 12.31/3.51 | (128) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (vsucc(v1) = v2 & vsucc(all_0_3_3) = v4 & vmul(all_0_8_8, all_0_3_3) = v0 & vplus(all_0_1_1, v5) = v6 & vplus(all_0_1_1, v2) = v3 & vplus(vd411, v4) = v5 & vplus(vd411, all_0_3_3) = v1 & ( ~ (v0 = all_0_0_0) | v6 = v3)) % 12.31/3.51 | % 12.31/3.51 | Instantiating formula (48) with all_0_0_0, all_0_1_1, all_0_3_3 and discharging atoms vmul(vd411, all_0_3_3) = all_0_1_1, vplus(all_0_1_1, all_0_3_3) = all_0_0_0, yields: % 12.31/3.51 | (129) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : (vsucc(v3) = v4 & vmul(all_0_8_8, all_0_3_3) = v0 & vplus(all_0_1_1, v4) = v5 & vplus(all_0_1_1, v1) = v2 & vplus(all_0_8_8, all_0_3_3) = v1 & vplus(vd411, all_0_3_3) = v3 & ( ~ (v0 = all_0_0_0) | v5 = v2)) % 12.31/3.51 | % 12.31/3.51 | Instantiating formula (24) with all_0_5_5, all_0_4_4, all_0_6_6 and discharging atoms vmul(vd411, all_0_6_6) = all_0_4_4, vplus(all_0_4_4, all_0_6_6) = all_0_5_5, yields: % 12.31/3.51 | (130) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (vsucc(v1) = v2 & vsucc(all_0_6_6) = v4 & vmul(all_0_8_8, all_0_6_6) = v0 & vplus(all_0_4_4, v5) = v6 & vplus(all_0_4_4, v2) = v3 & vplus(vd411, v4) = v5 & vplus(vd411, all_0_6_6) = v1 & ( ~ (v0 = all_0_5_5) | v6 = v3)) % 12.31/3.51 | % 12.31/3.51 | Instantiating formula (48) with all_0_5_5, all_0_4_4, all_0_6_6 and discharging atoms vmul(vd411, all_0_6_6) = all_0_4_4, vplus(all_0_4_4, all_0_6_6) = all_0_5_5, yields: % 12.31/3.51 | (131) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : (vsucc(v3) = v4 & vmul(all_0_8_8, all_0_6_6) = v0 & vplus(all_0_4_4, v4) = v5 & vplus(all_0_4_4, v1) = v2 & vplus(all_0_8_8, all_0_6_6) = v1 & vplus(vd411, all_0_6_6) = v3 & ( ~ (v0 = all_0_5_5) | v5 = v2)) % 12.31/3.51 | % 12.31/3.51 | Instantiating formula (2) with all_0_5_5, all_0_4_4, all_0_6_6 and discharging atoms vmul(vd411, all_0_6_6) = all_0_4_4, vplus(all_0_4_4, all_0_6_6) = all_0_5_5, yields: % 12.31/3.51 | (132) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : (vsucc(all_0_6_6) = v2 & vmul(all_0_8_8, all_0_6_6) = v0 & vmul(vd411, v2) = v4 & vplus(v4, v2) = v5 & vplus(v1, v2) = v3 & vplus(all_0_4_4, vd411) = v1 & ( ~ (v0 = all_0_5_5) | v5 = v3)) % 12.31/3.51 | % 12.31/3.51 | Instantiating formula (105) with all_0_5_5, all_0_4_4, all_0_6_6 and discharging atoms vmul(vd411, all_0_6_6) = all_0_4_4, vplus(all_0_4_4, all_0_6_6) = all_0_5_5, yields: % 12.31/3.51 | (133) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : (vsucc(all_0_6_6) = v1 & vmul(all_0_8_8, all_0_6_6) = v0 & vplus(v4, v1) = v5 & vplus(all_0_4_4, v2) = v3 & vplus(all_0_4_4, vd411) = v4 & vplus(vd411, v1) = v2 & ( ~ (v0 = all_0_5_5) | v5 = v3)) % 12.31/3.51 | % 12.31/3.51 | Instantiating formula (83) with all_0_5_5, all_0_4_4, all_0_6_6 and discharging atoms vmul(vd411, all_0_6_6) = all_0_4_4, vplus(all_0_4_4, all_0_6_6) = all_0_5_5, yields: % 12.31/3.51 | (134) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (vmul(all_0_8_8, all_0_6_6) = v0 & vplus(all_0_4_4, v3) = v4 & vplus(all_0_4_4, v1) = v2 & vplus(all_0_6_6, all_0_8_8) = v1 & vplus(all_0_8_8, all_0_6_6) = v3 & ( ~ (v0 = all_0_5_5) | v4 = v2)) % 12.31/3.51 | % 12.31/3.51 | Instantiating formula (44) with all_0_5_5, all_0_4_4, all_0_6_6 and discharging atoms vmul(vd411, all_0_6_6) = all_0_4_4, vplus(all_0_4_4, all_0_6_6) = all_0_5_5, yields: % 12.31/3.51 | (135) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (vsucc(all_0_6_6) = v1 & vmul(all_0_8_8, v1) = v2 & vmul(all_0_8_8, all_0_6_6) = v0 & vplus(v0, all_0_8_8) = v3 & ( ~ (v0 = all_0_5_5) | v3 = v2)) % 12.31/3.51 | % 12.31/3.51 | Instantiating formula (25) with all_0_5_5, all_0_4_4, all_0_6_6 and discharging atoms vmul(vd411, all_0_6_6) = all_0_4_4, vplus(all_0_4_4, all_0_6_6) = all_0_5_5, yields: % 12.31/3.51 | (136) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (vmul(all_0_8_8, all_0_6_6) = v0 & vplus(all_0_4_4, v2) = v3 & vplus(all_0_5_5, all_0_8_8) = v1 & vplus(all_0_6_6, all_0_8_8) = v2 & ( ~ (v0 = all_0_5_5) | v3 = v1)) % 12.31/3.51 | % 12.31/3.51 | Instantiating formula (23) with all_0_5_5, all_0_4_4, all_0_6_6 and discharging atoms vmul(vd411, all_0_6_6) = all_0_4_4, vplus(all_0_4_4, all_0_6_6) = all_0_5_5, yields: % 12.31/3.51 | (137) ? [v0] : ? [v1] : ? [v2] : (vmul(all_0_8_8, all_0_6_6) = v0 & vplus(v0, all_0_8_8) = v1 & vplus(all_0_5_5, all_0_8_8) = v2 & ( ~ (v0 = all_0_5_5) | v2 = v1)) % 12.31/3.51 | % 12.31/3.51 | Instantiating formula (26) with all_0_5_5, all_0_6_6, all_0_4_4 and discharging atoms vplus(all_0_4_4, all_0_6_6) = all_0_5_5, yields: % 12.31/3.51 | (138) ? [v0] : ? [v1] : (vsucc(all_0_5_5) = v1 & vsucc(all_0_6_6) = v0 & vplus(all_0_4_4, v0) = v1) % 12.31/3.51 | % 12.31/3.51 | Instantiating (117) with all_27_0_26, all_27_1_27, all_27_2_28, all_27_3_29 yields: % 12.31/3.51 | (139) vmul(vd411, all_0_3_3) = all_27_3_29 & vplus(all_27_2_28, all_0_8_8) = all_27_0_26 & vplus(all_27_3_29, all_0_3_3) = all_27_2_28 & vplus(all_0_2_2, all_0_8_8) = all_27_1_27 & ( ~ (all_27_2_28 = all_0_2_2) | all_27_0_26 = all_27_1_27) % 12.31/3.51 | % 12.31/3.51 | Applying alpha-rule on (139) yields: % 12.31/3.51 | (140) vplus(all_27_3_29, all_0_3_3) = all_27_2_28 % 12.31/3.51 | (141) vmul(vd411, all_0_3_3) = all_27_3_29 % 12.31/3.51 | (142) vplus(all_27_2_28, all_0_8_8) = all_27_0_26 % 12.31/3.51 | (143) ~ (all_27_2_28 = all_0_2_2) | all_27_0_26 = all_27_1_27 % 12.31/3.51 | (144) vplus(all_0_2_2, all_0_8_8) = all_27_1_27 % 12.31/3.52 | % 12.31/3.52 | Instantiating (116) with all_29_0_30, all_29_1_31, all_29_2_32, all_29_3_33, all_29_4_34 yields: % 12.31/3.52 | (145) vmul(vd411, all_0_3_3) = all_29_4_34 & vplus(all_29_3_33, all_0_8_8) = all_29_2_32 & vplus(all_29_4_34, all_29_1_31) = all_29_0_30 & vplus(all_29_4_34, all_0_3_3) = all_29_3_33 & vplus(all_0_3_3, all_0_8_8) = all_29_1_31 & ( ~ (all_29_3_33 = all_0_2_2) | all_29_0_30 = all_29_2_32) % 12.31/3.52 | % 12.31/3.52 | Applying alpha-rule on (145) yields: % 12.31/3.52 | (146) vplus(all_29_4_34, all_29_1_31) = all_29_0_30 % 12.31/3.52 | (147) vmul(vd411, all_0_3_3) = all_29_4_34 % 12.31/3.52 | (148) ~ (all_29_3_33 = all_0_2_2) | all_29_0_30 = all_29_2_32 % 12.31/3.52 | (149) vplus(all_29_3_33, all_0_8_8) = all_29_2_32 % 12.31/3.52 | (150) vplus(all_29_4_34, all_0_3_3) = all_29_3_33 % 12.31/3.52 | (151) vplus(all_0_3_3, all_0_8_8) = all_29_1_31 % 12.31/3.52 | % 12.31/3.52 | Instantiating (137) with all_31_0_35, all_31_1_36, all_31_2_37 yields: % 12.31/3.52 | (152) vmul(all_0_8_8, all_0_6_6) = all_31_2_37 & vplus(all_31_2_37, all_0_8_8) = all_31_1_36 & vplus(all_0_5_5, all_0_8_8) = all_31_0_35 & ( ~ (all_31_2_37 = all_0_5_5) | all_31_0_35 = all_31_1_36) % 12.31/3.52 | % 12.31/3.52 | Applying alpha-rule on (152) yields: % 12.31/3.52 | (153) vmul(all_0_8_8, all_0_6_6) = all_31_2_37 % 12.31/3.52 | (154) vplus(all_31_2_37, all_0_8_8) = all_31_1_36 % 12.31/3.52 | (155) vplus(all_0_5_5, all_0_8_8) = all_31_0_35 % 12.31/3.52 | (156) ~ (all_31_2_37 = all_0_5_5) | all_31_0_35 = all_31_1_36 % 12.31/3.52 | % 12.31/3.52 | Instantiating (113) with all_35_0_40, all_35_1_41, all_35_2_42, all_35_3_43, all_35_4_44, all_35_5_45, all_35_6_46 yields: % 12.31/3.52 | (157) vsucc(all_0_3_3) = all_35_4_44 & vmul(vd411, all_0_3_3) = all_35_6_46 & vplus(all_35_1_41, all_35_4_44) = all_35_0_40 & vplus(all_35_6_46, all_35_3_43) = all_35_2_42 & vplus(all_35_6_46, all_0_3_3) = all_35_5_45 & vplus(all_35_6_46, vd411) = all_35_1_41 & vplus(vd411, all_35_4_44) = all_35_3_43 & ( ~ (all_35_5_45 = all_0_2_2) | all_35_0_40 = all_35_2_42) % 12.31/3.52 | % 12.31/3.52 | Applying alpha-rule on (157) yields: % 12.31/3.52 | (158) vplus(all_35_1_41, all_35_4_44) = all_35_0_40 % 12.31/3.52 | (159) vplus(all_35_6_46, all_0_3_3) = all_35_5_45 % 12.31/3.52 | (160) vplus(all_35_6_46, all_35_3_43) = all_35_2_42 % 12.31/3.52 | (161) vmul(vd411, all_0_3_3) = all_35_6_46 % 12.31/3.52 | (162) vsucc(all_0_3_3) = all_35_4_44 % 12.31/3.52 | (163) vplus(vd411, all_35_4_44) = all_35_3_43 % 12.31/3.52 | (164) ~ (all_35_5_45 = all_0_2_2) | all_35_0_40 = all_35_2_42 % 12.31/3.52 | (165) vplus(all_35_6_46, vd411) = all_35_1_41 % 12.31/3.52 | % 12.31/3.52 | Instantiating (111) with all_37_0_47, all_37_1_48, all_37_2_49, all_37_3_50, all_37_4_51, all_37_5_52, all_37_6_53 yields: % 12.31/3.52 | (166) vsucc(all_37_2_49) = all_37_1_48 & vmul(vd411, all_0_3_3) = all_37_6_53 & vplus(all_37_6_53, all_37_1_48) = all_37_0_47 & vplus(all_37_6_53, all_37_4_51) = all_37_3_50 & vplus(all_37_6_53, all_0_3_3) = all_37_5_52 & vplus(all_0_8_8, all_0_3_3) = all_37_4_51 & vplus(vd411, all_0_3_3) = all_37_2_49 & ( ~ (all_37_5_52 = all_0_2_2) | all_37_0_47 = all_37_3_50) % 12.31/3.52 | % 12.31/3.52 | Applying alpha-rule on (166) yields: % 12.31/3.52 | (167) vsucc(all_37_2_49) = all_37_1_48 % 12.31/3.52 | (168) vplus(vd411, all_0_3_3) = all_37_2_49 % 12.31/3.52 | (169) vmul(vd411, all_0_3_3) = all_37_6_53 % 12.31/3.52 | (170) vplus(all_37_6_53, all_37_1_48) = all_37_0_47 % 12.31/3.52 | (171) vplus(all_37_6_53, all_0_3_3) = all_37_5_52 % 12.31/3.52 | (172) vplus(all_0_8_8, all_0_3_3) = all_37_4_51 % 12.31/3.52 | (173) vplus(all_37_6_53, all_37_4_51) = all_37_3_50 % 12.31/3.52 | (174) ~ (all_37_5_52 = all_0_2_2) | all_37_0_47 = all_37_3_50 % 12.31/3.52 | % 12.31/3.52 | Instantiating (110) with all_39_0_54, all_39_1_55, all_39_2_56, all_39_3_57, all_39_4_58, all_39_5_59, all_39_6_60, all_39_7_61 yields: % 12.31/3.52 | (175) vsucc(all_39_5_59) = all_39_4_58 & vsucc(all_0_3_3) = all_39_2_56 & vmul(vd411, all_0_3_3) = all_39_7_61 & vplus(all_39_7_61, all_39_1_55) = all_39_0_54 & vplus(all_39_7_61, all_39_4_58) = all_39_3_57 & vplus(all_39_7_61, all_0_3_3) = all_39_6_60 & vplus(vd411, all_39_2_56) = all_39_1_55 & vplus(vd411, all_0_3_3) = all_39_5_59 & ( ~ (all_39_6_60 = all_0_2_2) | all_39_0_54 = all_39_3_57) % 12.31/3.52 | % 12.31/3.52 | Applying alpha-rule on (175) yields: % 12.31/3.52 | (176) vplus(all_39_7_61, all_0_3_3) = all_39_6_60 % 12.31/3.52 | (177) vmul(vd411, all_0_3_3) = all_39_7_61 % 12.31/3.52 | (178) ~ (all_39_6_60 = all_0_2_2) | all_39_0_54 = all_39_3_57 % 12.31/3.52 | (179) vsucc(all_0_3_3) = all_39_2_56 % 12.31/3.52 | (180) vplus(all_39_7_61, all_39_4_58) = all_39_3_57 % 12.31/3.52 | (181) vplus(vd411, all_0_3_3) = all_39_5_59 % 12.65/3.52 | (182) vplus(all_39_7_61, all_39_1_55) = all_39_0_54 % 12.65/3.52 | (183) vsucc(all_39_5_59) = all_39_4_58 % 12.65/3.52 | (184) vplus(vd411, all_39_2_56) = all_39_1_55 % 12.65/3.52 | % 12.65/3.52 | Instantiating (108) with all_45_0_69, all_45_1_70, all_45_2_71, all_45_3_72, all_45_4_73 yields: % 12.65/3.52 | (185) vmul(all_0_8_8, all_0_3_3) = all_45_1_70 & vmul(all_0_8_8, all_0_6_6) = all_45_4_73 & vmul(vd411, all_0_6_6) = all_45_3_72 & vplus(all_45_3_72, all_0_6_6) = all_45_2_71 & vplus(all_45_4_73, all_0_8_8) = all_45_0_69 & ( ~ (all_45_2_71 = all_45_4_73) | all_45_0_69 = all_45_1_70) % 12.65/3.52 | % 12.65/3.52 | Applying alpha-rule on (185) yields: % 12.65/3.52 | (186) ~ (all_45_2_71 = all_45_4_73) | all_45_0_69 = all_45_1_70 % 12.65/3.52 | (187) vmul(vd411, all_0_6_6) = all_45_3_72 % 12.65/3.52 | (188) vplus(all_45_3_72, all_0_6_6) = all_45_2_71 % 12.65/3.52 | (189) vmul(all_0_8_8, all_0_3_3) = all_45_1_70 % 12.65/3.52 | (190) vplus(all_45_4_73, all_0_8_8) = all_45_0_69 % 12.65/3.52 | (191) vmul(all_0_8_8, all_0_6_6) = all_45_4_73 % 12.65/3.52 | % 12.65/3.52 | Instantiating (112) with all_47_0_74, all_47_1_75, all_47_2_76, all_47_3_77, all_47_4_78, all_47_5_79, all_47_6_80 yields: % 12.65/3.52 | (192) vsucc(all_0_3_3) = all_47_3_77 & vmul(vd411, all_47_3_77) = all_47_1_75 & vmul(vd411, all_0_3_3) = all_47_6_80 & vplus(all_47_1_75, all_47_3_77) = all_47_0_74 & vplus(all_47_4_78, all_47_3_77) = all_47_2_76 & vplus(all_47_6_80, all_0_3_3) = all_47_5_79 & vplus(all_47_6_80, vd411) = all_47_4_78 & ( ~ (all_47_5_79 = all_0_2_2) | all_47_0_74 = all_47_2_76) % 12.65/3.52 | % 12.65/3.52 | Applying alpha-rule on (192) yields: % 12.65/3.52 | (193) vplus(all_47_4_78, all_47_3_77) = all_47_2_76 % 12.65/3.52 | (194) vplus(all_47_1_75, all_47_3_77) = all_47_0_74 % 12.65/3.52 | (195) vplus(all_47_6_80, vd411) = all_47_4_78 % 12.65/3.52 | (196) vsucc(all_0_3_3) = all_47_3_77 % 12.65/3.52 | (197) vmul(vd411, all_0_3_3) = all_47_6_80 % 12.65/3.52 | (198) ~ (all_47_5_79 = all_0_2_2) | all_47_0_74 = all_47_2_76 % 12.65/3.52 | (199) vmul(vd411, all_47_3_77) = all_47_1_75 % 12.65/3.53 | (200) vplus(all_47_6_80, all_0_3_3) = all_47_5_79 % 12.65/3.53 | % 12.65/3.53 | Instantiating (115) with all_49_0_81, all_49_1_82, all_49_2_83, all_49_3_84, all_49_4_85 yields: % 12.65/3.53 | (201) vsucc(all_0_3_3) = all_49_2_83 & vmul(all_0_8_8, all_49_2_83) = all_49_1_82 & vmul(vd411, all_0_3_3) = all_49_4_85 & vplus(all_49_4_85, all_0_3_3) = all_49_3_84 & vplus(all_0_2_2, all_0_8_8) = all_49_0_81 & ( ~ (all_49_3_84 = all_0_2_2) | all_49_0_81 = all_49_1_82) % 12.65/3.53 | % 12.65/3.53 | Applying alpha-rule on (201) yields: % 12.65/3.53 | (202) vsucc(all_0_3_3) = all_49_2_83 % 12.65/3.53 | (203) vplus(all_49_4_85, all_0_3_3) = all_49_3_84 % 12.65/3.53 | (204) vmul(all_0_8_8, all_49_2_83) = all_49_1_82 % 12.65/3.53 | (205) vmul(vd411, all_0_3_3) = all_49_4_85 % 12.65/3.53 | (206) vplus(all_0_2_2, all_0_8_8) = all_49_0_81 % 12.65/3.53 | (207) ~ (all_49_3_84 = all_0_2_2) | all_49_0_81 = all_49_1_82 % 12.65/3.53 | % 12.65/3.53 | Instantiating (109) with all_51_0_86 yields: % 12.65/3.53 | (208) vmul(all_0_8_8, all_0_6_6) = all_51_0_86 & vplus(all_51_0_86, all_0_8_8) = all_0_2_2 % 12.65/3.53 | % 12.65/3.53 | Applying alpha-rule on (208) yields: % 12.65/3.53 | (209) vmul(all_0_8_8, all_0_6_6) = all_51_0_86 % 12.65/3.53 | (210) vplus(all_51_0_86, all_0_8_8) = all_0_2_2 % 12.65/3.53 | % 12.65/3.53 | Instantiating (125) with all_61_0_107, all_61_1_108, all_61_2_109, all_61_3_110 yields: % 12.65/3.53 | (211) vmul(vd411, all_0_6_6) = all_61_3_110 & vplus(all_61_2_109, all_0_8_8) = all_61_0_107 & vplus(all_61_3_110, all_0_6_6) = all_61_2_109 & vplus(all_0_5_5, all_0_8_8) = all_61_1_108 & ( ~ (all_61_2_109 = all_0_5_5) | all_61_0_107 = all_61_1_108) % 12.65/3.53 | % 12.65/3.53 | Applying alpha-rule on (211) yields: % 12.65/3.53 | (212) vmul(vd411, all_0_6_6) = all_61_3_110 % 12.65/3.53 | (213) vplus(all_61_2_109, all_0_8_8) = all_61_0_107 % 12.65/3.53 | (214) vplus(all_61_3_110, all_0_6_6) = all_61_2_109 % 12.65/3.53 | (215) ~ (all_61_2_109 = all_0_5_5) | all_61_0_107 = all_61_1_108 % 12.65/3.53 | (216) vplus(all_0_5_5, all_0_8_8) = all_61_1_108 % 12.65/3.53 | % 12.65/3.53 | Instantiating (123) with all_63_0_111, all_63_1_112, all_63_2_113, all_63_3_114, all_63_4_115 yields: % 12.65/3.53 | (217) vsucc(all_0_6_6) = all_63_2_113 & vmul(all_0_8_8, all_63_2_113) = all_63_1_112 & vmul(vd411, all_0_6_6) = all_63_4_115 & vplus(all_63_4_115, all_0_6_6) = all_63_3_114 & vplus(all_0_5_5, all_0_8_8) = all_63_0_111 & ( ~ (all_63_3_114 = all_0_5_5) | all_63_0_111 = all_63_1_112) % 12.65/3.53 | % 12.65/3.53 | Applying alpha-rule on (217) yields: % 12.65/3.53 | (218) vmul(vd411, all_0_6_6) = all_63_4_115 % 12.65/3.53 | (219) ~ (all_63_3_114 = all_0_5_5) | all_63_0_111 = all_63_1_112 % 12.65/3.53 | (220) vplus(all_0_5_5, all_0_8_8) = all_63_0_111 % 12.65/3.53 | (221) vmul(all_0_8_8, all_63_2_113) = all_63_1_112 % 12.65/3.53 | (222) vplus(all_63_4_115, all_0_6_6) = all_63_3_114 % 12.65/3.53 | (223) vsucc(all_0_6_6) = all_63_2_113 % 12.65/3.53 | % 12.65/3.53 | Instantiating (136) with all_67_0_121, all_67_1_122, all_67_2_123, all_67_3_124 yields: % 12.65/3.53 | (224) vmul(all_0_8_8, all_0_6_6) = all_67_3_124 & vplus(all_0_4_4, all_67_1_122) = all_67_0_121 & vplus(all_0_5_5, all_0_8_8) = all_67_2_123 & vplus(all_0_6_6, all_0_8_8) = all_67_1_122 & ( ~ (all_67_3_124 = all_0_5_5) | all_67_0_121 = all_67_2_123) % 12.65/3.53 | % 12.65/3.53 | Applying alpha-rule on (224) yields: % 12.65/3.53 | (225) ~ (all_67_3_124 = all_0_5_5) | all_67_0_121 = all_67_2_123 % 12.65/3.53 | (226) vplus(all_0_6_6, all_0_8_8) = all_67_1_122 % 12.65/3.53 | (227) vmul(all_0_8_8, all_0_6_6) = all_67_3_124 % 12.65/3.53 | (228) vplus(all_0_4_4, all_67_1_122) = all_67_0_121 % 12.65/3.53 | (229) vplus(all_0_5_5, all_0_8_8) = all_67_2_123 % 12.65/3.53 | % 12.65/3.53 | Instantiating (134) with all_69_0_125, all_69_1_126, all_69_2_127, all_69_3_128, all_69_4_129 yields: % 12.65/3.53 | (230) vmul(all_0_8_8, all_0_6_6) = all_69_4_129 & vplus(all_0_4_4, all_69_1_126) = all_69_0_125 & vplus(all_0_4_4, all_69_3_128) = all_69_2_127 & vplus(all_0_6_6, all_0_8_8) = all_69_3_128 & vplus(all_0_8_8, all_0_6_6) = all_69_1_126 & ( ~ (all_69_4_129 = all_0_5_5) | all_69_0_125 = all_69_2_127) % 12.65/3.53 | % 12.65/3.53 | Applying alpha-rule on (230) yields: % 12.65/3.53 | (231) ~ (all_69_4_129 = all_0_5_5) | all_69_0_125 = all_69_2_127 % 12.65/3.53 | (232) vmul(all_0_8_8, all_0_6_6) = all_69_4_129 % 12.65/3.53 | (233) vplus(all_0_8_8, all_0_6_6) = all_69_1_126 % 12.65/3.53 | (234) vplus(all_0_6_6, all_0_8_8) = all_69_3_128 % 12.65/3.53 | (235) vplus(all_0_4_4, all_69_3_128) = all_69_2_127 % 12.65/3.53 | (236) vplus(all_0_4_4, all_69_1_126) = all_69_0_125 % 12.65/3.53 | % 12.65/3.53 | Instantiating (133) with all_71_0_130, all_71_1_131, all_71_2_132, all_71_3_133, all_71_4_134, all_71_5_135 yields: % 12.65/3.53 | (237) vsucc(all_0_6_6) = all_71_4_134 & vmul(all_0_8_8, all_0_6_6) = all_71_5_135 & vplus(all_71_1_131, all_71_4_134) = all_71_0_130 & vplus(all_0_4_4, all_71_3_133) = all_71_2_132 & vplus(all_0_4_4, vd411) = all_71_1_131 & vplus(vd411, all_71_4_134) = all_71_3_133 & ( ~ (all_71_5_135 = all_0_5_5) | all_71_0_130 = all_71_2_132) % 12.65/3.53 | % 12.65/3.53 | Applying alpha-rule on (237) yields: % 12.65/3.53 | (238) vsucc(all_0_6_6) = all_71_4_134 % 12.65/3.53 | (239) vmul(all_0_8_8, all_0_6_6) = all_71_5_135 % 12.65/3.53 | (240) vplus(all_0_4_4, all_71_3_133) = all_71_2_132 % 12.65/3.53 | (241) vplus(vd411, all_71_4_134) = all_71_3_133 % 12.65/3.53 | (242) ~ (all_71_5_135 = all_0_5_5) | all_71_0_130 = all_71_2_132 % 12.65/3.53 | (243) vplus(all_71_1_131, all_71_4_134) = all_71_0_130 % 12.65/3.53 | (244) vplus(all_0_4_4, vd411) = all_71_1_131 % 12.65/3.53 | % 12.65/3.53 | Instantiating (135) with all_73_0_136, all_73_1_137, all_73_2_138, all_73_3_139 yields: % 12.65/3.53 | (245) vsucc(all_0_6_6) = all_73_2_138 & vmul(all_0_8_8, all_73_2_138) = all_73_1_137 & vmul(all_0_8_8, all_0_6_6) = all_73_3_139 & vplus(all_73_3_139, all_0_8_8) = all_73_0_136 & ( ~ (all_73_3_139 = all_0_5_5) | all_73_0_136 = all_73_1_137) % 12.65/3.53 | % 12.65/3.53 | Applying alpha-rule on (245) yields: % 12.65/3.53 | (246) vmul(all_0_8_8, all_73_2_138) = all_73_1_137 % 12.65/3.53 | (247) vplus(all_73_3_139, all_0_8_8) = all_73_0_136 % 12.65/3.53 | (248) ~ (all_73_3_139 = all_0_5_5) | all_73_0_136 = all_73_1_137 % 12.65/3.53 | (249) vmul(all_0_8_8, all_0_6_6) = all_73_3_139 % 12.65/3.53 | (250) vsucc(all_0_6_6) = all_73_2_138 % 12.65/3.53 | % 12.65/3.53 | Instantiating (132) with all_79_0_151, all_79_1_152, all_79_2_153, all_79_3_154, all_79_4_155, all_79_5_156 yields: % 12.65/3.53 | (251) vsucc(all_0_6_6) = all_79_3_154 & vmul(all_0_8_8, all_0_6_6) = all_79_5_156 & vmul(vd411, all_79_3_154) = all_79_1_152 & vplus(all_79_1_152, all_79_3_154) = all_79_0_151 & vplus(all_79_4_155, all_79_3_154) = all_79_2_153 & vplus(all_0_4_4, vd411) = all_79_4_155 & ( ~ (all_79_5_156 = all_0_5_5) | all_79_0_151 = all_79_2_153) % 12.65/3.54 | % 12.65/3.54 | Applying alpha-rule on (251) yields: % 12.65/3.54 | (252) vsucc(all_0_6_6) = all_79_3_154 % 12.65/3.54 | (253) vmul(vd411, all_79_3_154) = all_79_1_152 % 12.65/3.54 | (254) vmul(all_0_8_8, all_0_6_6) = all_79_5_156 % 12.65/3.54 | (255) ~ (all_79_5_156 = all_0_5_5) | all_79_0_151 = all_79_2_153 % 12.65/3.54 | (256) vplus(all_0_4_4, vd411) = all_79_4_155 % 12.65/3.54 | (257) vplus(all_79_4_155, all_79_3_154) = all_79_2_153 % 12.65/3.54 | (258) vplus(all_79_1_152, all_79_3_154) = all_79_0_151 % 12.65/3.54 | % 12.65/3.54 | Instantiating (130) with all_81_0_157, all_81_1_158, all_81_2_159, all_81_3_160, all_81_4_161, all_81_5_162, all_81_6_163 yields: % 12.65/3.54 | (259) vsucc(all_81_5_162) = all_81_4_161 & vsucc(all_0_6_6) = all_81_2_159 & vmul(all_0_8_8, all_0_6_6) = all_81_6_163 & vplus(all_0_4_4, all_81_1_158) = all_81_0_157 & vplus(all_0_4_4, all_81_4_161) = all_81_3_160 & vplus(vd411, all_81_2_159) = all_81_1_158 & vplus(vd411, all_0_6_6) = all_81_5_162 & ( ~ (all_81_6_163 = all_0_5_5) | all_81_0_157 = all_81_3_160) % 12.65/3.54 | % 12.65/3.54 | Applying alpha-rule on (259) yields: % 12.65/3.54 | (260) vsucc(all_81_5_162) = all_81_4_161 % 12.65/3.54 | (261) ~ (all_81_6_163 = all_0_5_5) | all_81_0_157 = all_81_3_160 % 12.65/3.54 | (262) vplus(vd411, all_81_2_159) = all_81_1_158 % 12.65/3.54 | (263) vmul(all_0_8_8, all_0_6_6) = all_81_6_163 % 12.65/3.54 | (264) vplus(all_0_4_4, all_81_4_161) = all_81_3_160 % 12.65/3.54 | (265) vsucc(all_0_6_6) = all_81_2_159 % 12.65/3.54 | (266) vplus(vd411, all_0_6_6) = all_81_5_162 % 12.65/3.54 | (267) vplus(all_0_4_4, all_81_1_158) = all_81_0_157 % 12.65/3.54 | % 12.65/3.54 | Instantiating (128) with all_83_0_164, all_83_1_165, all_83_2_166, all_83_3_167, all_83_4_168, all_83_5_169, all_83_6_170 yields: % 12.65/3.54 | (268) vsucc(all_83_5_169) = all_83_4_168 & vsucc(all_0_3_3) = all_83_2_166 & vmul(all_0_8_8, all_0_3_3) = all_83_6_170 & vplus(all_0_1_1, all_83_1_165) = all_83_0_164 & vplus(all_0_1_1, all_83_4_168) = all_83_3_167 & vplus(vd411, all_83_2_166) = all_83_1_165 & vplus(vd411, all_0_3_3) = all_83_5_169 & ( ~ (all_83_6_170 = all_0_0_0) | all_83_0_164 = all_83_3_167) % 12.65/3.54 | % 12.65/3.54 | Applying alpha-rule on (268) yields: % 12.65/3.54 | (269) vplus(all_0_1_1, all_83_4_168) = all_83_3_167 % 12.65/3.54 | (270) vplus(vd411, all_0_3_3) = all_83_5_169 % 12.65/3.54 | (271) vplus(vd411, all_83_2_166) = all_83_1_165 % 12.65/3.54 | (272) vsucc(all_0_3_3) = all_83_2_166 % 12.65/3.54 | (273) vmul(all_0_8_8, all_0_3_3) = all_83_6_170 % 12.65/3.54 | (274) vsucc(all_83_5_169) = all_83_4_168 % 12.65/3.54 | (275) ~ (all_83_6_170 = all_0_0_0) | all_83_0_164 = all_83_3_167 % 12.65/3.54 | (276) vplus(all_0_1_1, all_83_1_165) = all_83_0_164 % 12.65/3.54 | % 12.65/3.54 | Instantiating (138) with all_89_0_178, all_89_1_179 yields: % 12.65/3.54 | (277) vsucc(all_0_5_5) = all_89_0_178 & vsucc(all_0_6_6) = all_89_1_179 & vplus(all_0_4_4, all_89_1_179) = all_89_0_178 % 12.65/3.54 | % 12.65/3.54 | Applying alpha-rule on (277) yields: % 12.65/3.54 | (278) vsucc(all_0_5_5) = all_89_0_178 % 12.65/3.54 | (279) vsucc(all_0_6_6) = all_89_1_179 % 12.65/3.54 | (280) vplus(all_0_4_4, all_89_1_179) = all_89_0_178 % 12.65/3.54 | % 12.65/3.54 | Instantiating (127) with all_91_0_180, all_91_1_181, all_91_2_182, all_91_3_183, all_91_4_184 yields: % 12.65/3.54 | (281) vmul(all_0_8_8, all_0_6_6) = all_91_4_184 & vmul(vd411, all_0_6_6) = all_91_3_183 & vplus(all_91_1_181, all_0_3_3) = all_91_0_180 & vplus(all_91_3_183, all_0_6_6) = all_91_2_182 & vplus(all_91_3_183, vd411) = all_91_1_181 & ( ~ (all_91_2_182 = all_91_4_184) | all_91_0_180 = all_0_0_0) % 12.65/3.54 | % 12.65/3.54 | Applying alpha-rule on (281) yields: % 12.65/3.54 | (282) vplus(all_91_1_181, all_0_3_3) = all_91_0_180 % 12.65/3.54 | (283) vmul(vd411, all_0_6_6) = all_91_3_183 % 12.65/3.54 | (284) vplus(all_91_3_183, all_0_6_6) = all_91_2_182 % 12.65/3.54 | (285) vplus(all_91_3_183, vd411) = all_91_1_181 % 12.65/3.54 | (286) ~ (all_91_2_182 = all_91_4_184) | all_91_0_180 = all_0_0_0 % 12.65/3.54 | (287) vmul(all_0_8_8, all_0_6_6) = all_91_4_184 % 12.65/3.54 | % 12.65/3.54 | Instantiating (129) with all_93_0_185, all_93_1_186, all_93_2_187, all_93_3_188, all_93_4_189, all_93_5_190 yields: % 12.65/3.54 | (288) vsucc(all_93_2_187) = all_93_1_186 & vmul(all_0_8_8, all_0_3_3) = all_93_5_190 & vplus(all_0_1_1, all_93_1_186) = all_93_0_185 & vplus(all_0_1_1, all_93_4_189) = all_93_3_188 & vplus(all_0_8_8, all_0_3_3) = all_93_4_189 & vplus(vd411, all_0_3_3) = all_93_2_187 & ( ~ (all_93_5_190 = all_0_0_0) | all_93_0_185 = all_93_3_188) % 12.65/3.54 | % 12.65/3.54 | Applying alpha-rule on (288) yields: % 12.65/3.54 | (289) vsucc(all_93_2_187) = all_93_1_186 % 12.65/3.54 | (290) vplus(all_0_1_1, all_93_1_186) = all_93_0_185 % 12.65/3.54 | (291) vplus(all_0_1_1, all_93_4_189) = all_93_3_188 % 12.65/3.54 | (292) vplus(all_0_8_8, all_0_3_3) = all_93_4_189 % 12.65/3.54 | (293) vplus(vd411, all_0_3_3) = all_93_2_187 % 12.65/3.54 | (294) vmul(all_0_8_8, all_0_3_3) = all_93_5_190 % 12.65/3.54 | (295) ~ (all_93_5_190 = all_0_0_0) | all_93_0_185 = all_93_3_188 % 12.65/3.54 | % 12.65/3.54 | Instantiating (126) with all_95_0_191 yields: % 12.65/3.54 | (296) vmul(vd411, all_0_6_6) = all_95_0_191 & vplus(all_95_0_191, vd411) = all_0_1_1 % 12.65/3.54 | % 12.65/3.54 | Applying alpha-rule on (296) yields: % 12.65/3.54 | (297) vmul(vd411, all_0_6_6) = all_95_0_191 % 12.65/3.54 | (298) vplus(all_95_0_191, vd411) = all_0_1_1 % 12.65/3.54 | % 12.65/3.54 | Instantiating (131) with all_99_0_194, all_99_1_195, all_99_2_196, all_99_3_197, all_99_4_198, all_99_5_199 yields: % 12.65/3.54 | (299) vsucc(all_99_2_196) = all_99_1_195 & vmul(all_0_8_8, all_0_6_6) = all_99_5_199 & vplus(all_0_4_4, all_99_1_195) = all_99_0_194 & vplus(all_0_4_4, all_99_4_198) = all_99_3_197 & vplus(all_0_8_8, all_0_6_6) = all_99_4_198 & vplus(vd411, all_0_6_6) = all_99_2_196 & ( ~ (all_99_5_199 = all_0_5_5) | all_99_0_194 = all_99_3_197) % 12.65/3.54 | % 12.65/3.54 | Applying alpha-rule on (299) yields: % 12.65/3.54 | (300) vmul(all_0_8_8, all_0_6_6) = all_99_5_199 % 12.65/3.55 | (301) ~ (all_99_5_199 = all_0_5_5) | all_99_0_194 = all_99_3_197 % 12.65/3.55 | (302) vplus(all_0_8_8, all_0_6_6) = all_99_4_198 % 12.65/3.55 | (303) vplus(all_0_4_4, all_99_1_195) = all_99_0_194 % 12.65/3.55 | (304) vplus(all_0_4_4, all_99_4_198) = all_99_3_197 % 12.65/3.55 | (305) vplus(vd411, all_0_6_6) = all_99_2_196 % 12.65/3.55 | (306) vsucc(all_99_2_196) = all_99_1_195 % 12.65/3.55 | % 12.65/3.55 | Instantiating (122) with all_115_0_240, all_115_1_241, all_115_2_242, all_115_3_243, all_115_4_244, all_115_5_245 yields: % 12.65/3.55 | (307) vmul(vd411, all_0_6_6) = all_115_5_245 & vplus(all_115_5_245, all_115_1_241) = all_115_0_240 & vplus(all_115_5_245, all_115_3_243) = all_115_2_242 & vplus(all_115_5_245, all_0_6_6) = all_115_4_244 & vplus(all_0_6_6, all_0_8_8) = all_115_3_243 & vplus(all_0_8_8, all_0_6_6) = all_115_1_241 & ( ~ (all_115_4_244 = all_0_5_5) | all_115_0_240 = all_115_2_242) % 12.65/3.55 | % 12.65/3.55 | Applying alpha-rule on (307) yields: % 12.65/3.55 | (308) vplus(all_115_5_245, all_0_6_6) = all_115_4_244 % 12.65/3.55 | (309) vplus(all_115_5_245, all_115_1_241) = all_115_0_240 % 12.65/3.55 | (310) ~ (all_115_4_244 = all_0_5_5) | all_115_0_240 = all_115_2_242 % 12.65/3.55 | (311) vmul(vd411, all_0_6_6) = all_115_5_245 % 12.65/3.55 | (312) vplus(all_0_8_8, all_0_6_6) = all_115_1_241 % 12.65/3.55 | (313) vplus(all_0_6_6, all_0_8_8) = all_115_3_243 % 12.65/3.55 | (314) vplus(all_115_5_245, all_115_3_243) = all_115_2_242 % 12.65/3.55 | % 12.65/3.55 | Instantiating (124) with all_119_0_253, all_119_1_254, all_119_2_255, all_119_3_256, all_119_4_257 yields: % 12.65/3.55 | (315) vmul(vd411, all_0_6_6) = all_119_4_257 & vplus(all_119_3_256, all_0_8_8) = all_119_2_255 & vplus(all_119_4_257, all_119_1_254) = all_119_0_253 & vplus(all_119_4_257, all_0_6_6) = all_119_3_256 & vplus(all_0_6_6, all_0_8_8) = all_119_1_254 & ( ~ (all_119_3_256 = all_0_5_5) | all_119_0_253 = all_119_2_255) % 12.65/3.55 | % 12.65/3.55 | Applying alpha-rule on (315) yields: % 12.65/3.55 | (316) vmul(vd411, all_0_6_6) = all_119_4_257 % 12.65/3.55 | (317) vplus(all_119_4_257, all_119_1_254) = all_119_0_253 % 12.65/3.55 | (318) vplus(all_0_6_6, all_0_8_8) = all_119_1_254 % 12.65/3.55 | (319) ~ (all_119_3_256 = all_0_5_5) | all_119_0_253 = all_119_2_255 % 12.65/3.55 | (320) vplus(all_119_3_256, all_0_8_8) = all_119_2_255 % 12.65/3.55 | (321) vplus(all_119_4_257, all_0_6_6) = all_119_3_256 % 12.65/3.55 | % 12.65/3.55 | Instantiating (114) with all_121_0_258, all_121_1_259, all_121_2_260, all_121_3_261, all_121_4_262, all_121_5_263 yields: % 12.65/3.55 | (322) vmul(vd411, all_0_3_3) = all_121_5_263 & vplus(all_121_5_263, all_121_1_259) = all_121_0_258 & vplus(all_121_5_263, all_121_3_261) = all_121_2_260 & vplus(all_121_5_263, all_0_3_3) = all_121_4_262 & vplus(all_0_3_3, all_0_8_8) = all_121_3_261 & vplus(all_0_8_8, all_0_3_3) = all_121_1_259 & ( ~ (all_121_4_262 = all_0_2_2) | all_121_0_258 = all_121_2_260) % 12.65/3.55 | % 12.65/3.55 | Applying alpha-rule on (322) yields: % 12.65/3.55 | (323) vmul(vd411, all_0_3_3) = all_121_5_263 % 12.65/3.55 | (324) vplus(all_121_5_263, all_121_3_261) = all_121_2_260 % 12.65/3.55 | (325) vplus(all_0_8_8, all_0_3_3) = all_121_1_259 % 12.65/3.55 | (326) vplus(all_121_5_263, all_121_1_259) = all_121_0_258 % 12.65/3.55 | (327) vplus(all_0_3_3, all_0_8_8) = all_121_3_261 % 12.65/3.55 | (328) vplus(all_121_5_263, all_0_3_3) = all_121_4_262 % 12.65/3.55 | (329) ~ (all_121_4_262 = all_0_2_2) | all_121_0_258 = all_121_2_260 % 12.65/3.55 | % 12.65/3.55 | Instantiating (121) with all_129_0_272, all_129_1_273, all_129_2_274, all_129_3_275, all_129_4_276, all_129_5_277, all_129_6_278 yields: % 12.65/3.55 | (330) vsucc(all_0_6_6) = all_129_4_276 & vmul(vd411, all_0_6_6) = all_129_6_278 & vplus(all_129_1_273, all_129_4_276) = all_129_0_272 & vplus(all_129_6_278, all_129_3_275) = all_129_2_274 & vplus(all_129_6_278, all_0_6_6) = all_129_5_277 & vplus(all_129_6_278, vd411) = all_129_1_273 & vplus(vd411, all_129_4_276) = all_129_3_275 & ( ~ (all_129_5_277 = all_0_5_5) | all_129_0_272 = all_129_2_274) % 12.65/3.55 | % 12.65/3.55 | Applying alpha-rule on (330) yields: % 12.65/3.55 | (331) vplus(all_129_6_278, all_129_3_275) = all_129_2_274 % 12.65/3.55 | (332) vsucc(all_0_6_6) = all_129_4_276 % 12.65/3.55 | (333) vplus(vd411, all_129_4_276) = all_129_3_275 % 12.65/3.55 | (334) vplus(all_129_6_278, all_0_6_6) = all_129_5_277 % 12.65/3.55 | (335) ~ (all_129_5_277 = all_0_5_5) | all_129_0_272 = all_129_2_274 % 12.65/3.55 | (336) vmul(vd411, all_0_6_6) = all_129_6_278 % 12.65/3.55 | (337) vplus(all_129_6_278, vd411) = all_129_1_273 % 12.65/3.55 | (338) vplus(all_129_1_273, all_129_4_276) = all_129_0_272 % 12.65/3.55 | % 12.65/3.55 | Instantiating (119) with all_131_0_279, all_131_1_280, all_131_2_281, all_131_3_282, all_131_4_283, all_131_5_284, all_131_6_285 yields: % 12.65/3.55 | (339) vsucc(all_131_2_281) = all_131_1_280 & vmul(vd411, all_0_6_6) = all_131_6_285 & vplus(all_131_6_285, all_131_1_280) = all_131_0_279 & vplus(all_131_6_285, all_131_4_283) = all_131_3_282 & vplus(all_131_6_285, all_0_6_6) = all_131_5_284 & vplus(all_0_8_8, all_0_6_6) = all_131_4_283 & vplus(vd411, all_0_6_6) = all_131_2_281 & ( ~ (all_131_5_284 = all_0_5_5) | all_131_0_279 = all_131_3_282) % 12.65/3.55 | % 12.65/3.55 | Applying alpha-rule on (339) yields: % 12.65/3.55 | (340) vplus(all_131_6_285, all_0_6_6) = all_131_5_284 % 12.65/3.55 | (341) vplus(all_131_6_285, all_131_1_280) = all_131_0_279 % 12.65/3.55 | (342) vplus(vd411, all_0_6_6) = all_131_2_281 % 12.65/3.55 | (343) vplus(all_131_6_285, all_131_4_283) = all_131_3_282 % 12.65/3.55 | (344) ~ (all_131_5_284 = all_0_5_5) | all_131_0_279 = all_131_3_282 % 12.65/3.55 | (345) vplus(all_0_8_8, all_0_6_6) = all_131_4_283 % 12.65/3.55 | (346) vsucc(all_131_2_281) = all_131_1_280 % 12.65/3.55 | (347) vmul(vd411, all_0_6_6) = all_131_6_285 % 12.65/3.55 | % 12.65/3.55 | Instantiating (120) with all_135_0_290, all_135_1_291, all_135_2_292, all_135_3_293, all_135_4_294, all_135_5_295, all_135_6_296 yields: % 12.65/3.55 | (348) vsucc(all_0_6_6) = all_135_3_293 & vmul(vd411, all_135_3_293) = all_135_1_291 & vmul(vd411, all_0_6_6) = all_135_6_296 & vplus(all_135_1_291, all_135_3_293) = all_135_0_290 & vplus(all_135_4_294, all_135_3_293) = all_135_2_292 & vplus(all_135_6_296, all_0_6_6) = all_135_5_295 & vplus(all_135_6_296, vd411) = all_135_4_294 & ( ~ (all_135_5_295 = all_0_5_5) | all_135_0_290 = all_135_2_292) % 12.65/3.56 | % 12.65/3.56 | Applying alpha-rule on (348) yields: % 12.65/3.56 | (349) vplus(all_135_4_294, all_135_3_293) = all_135_2_292 % 12.65/3.56 | (350) vmul(vd411, all_0_6_6) = all_135_6_296 % 12.65/3.56 | (351) vmul(vd411, all_135_3_293) = all_135_1_291 % 12.65/3.56 | (352) ~ (all_135_5_295 = all_0_5_5) | all_135_0_290 = all_135_2_292 % 12.65/3.56 | (353) vplus(all_135_6_296, vd411) = all_135_4_294 % 12.65/3.56 | (354) vplus(all_135_1_291, all_135_3_293) = all_135_0_290 % 12.65/3.56 | (355) vsucc(all_0_6_6) = all_135_3_293 % 12.65/3.56 | (356) vplus(all_135_6_296, all_0_6_6) = all_135_5_295 % 12.65/3.56 | % 12.65/3.56 | Instantiating (118) with all_139_0_301, all_139_1_302, all_139_2_303, all_139_3_304, all_139_4_305, all_139_5_306, all_139_6_307, all_139_7_308 yields: % 12.65/3.56 | (357) vsucc(all_139_5_306) = all_139_4_305 & vsucc(all_0_6_6) = all_139_2_303 & vmul(vd411, all_0_6_6) = all_139_7_308 & vplus(all_139_7_308, all_139_1_302) = all_139_0_301 & vplus(all_139_7_308, all_139_4_305) = all_139_3_304 & vplus(all_139_7_308, all_0_6_6) = all_139_6_307 & vplus(vd411, all_139_2_303) = all_139_1_302 & vplus(vd411, all_0_6_6) = all_139_5_306 & ( ~ (all_139_6_307 = all_0_5_5) | all_139_0_301 = all_139_3_304) % 12.65/3.56 | % 12.65/3.56 | Applying alpha-rule on (357) yields: % 12.65/3.56 | (358) vplus(all_139_7_308, all_139_4_305) = all_139_3_304 % 12.65/3.56 | (359) vplus(all_139_7_308, all_0_6_6) = all_139_6_307 % 12.65/3.56 | (360) vplus(all_139_7_308, all_139_1_302) = all_139_0_301 % 12.65/3.56 | (361) ~ (all_139_6_307 = all_0_5_5) | all_139_0_301 = all_139_3_304 % 12.65/3.56 | (362) vmul(vd411, all_0_6_6) = all_139_7_308 % 12.65/3.56 | (363) vplus(vd411, all_0_6_6) = all_139_5_306 % 12.65/3.56 | (364) vsucc(all_139_5_306) = all_139_4_305 % 12.65/3.56 | (365) vsucc(all_0_6_6) = all_139_2_303 % 12.65/3.56 | (366) vplus(vd411, all_139_2_303) = all_139_1_302 % 12.65/3.56 | % 12.65/3.56 | Instantiating formula (30) with all_0_6_6, all_129_4_276, all_135_3_293 and discharging atoms vsucc(all_0_6_6) = all_135_3_293, vsucc(all_0_6_6) = all_129_4_276, yields: % 12.65/3.56 | (367) all_135_3_293 = all_129_4_276 % 12.65/3.56 | % 12.65/3.56 | Instantiating formula (30) with all_0_6_6, all_89_1_179, all_135_3_293 and discharging atoms vsucc(all_0_6_6) = all_135_3_293, vsucc(all_0_6_6) = all_89_1_179, yields: % 12.65/3.56 | (368) all_135_3_293 = all_89_1_179 % 12.65/3.56 | % 12.65/3.56 | Instantiating formula (30) with all_0_6_6, all_81_2_159, all_129_4_276 and discharging atoms vsucc(all_0_6_6) = all_129_4_276, vsucc(all_0_6_6) = all_81_2_159, yields: % 12.65/3.56 | (369) all_129_4_276 = all_81_2_159 % 12.65/3.56 | % 12.65/3.56 | Instantiating formula (30) with all_0_6_6, all_79_3_154, all_139_2_303 and discharging atoms vsucc(all_0_6_6) = all_139_2_303, vsucc(all_0_6_6) = all_79_3_154, yields: % 12.65/3.56 | (370) all_139_2_303 = all_79_3_154 % 12.65/3.56 | % 12.65/3.56 | Instantiating formula (30) with all_0_6_6, all_79_3_154, all_129_4_276 and discharging atoms vsucc(all_0_6_6) = all_129_4_276, vsucc(all_0_6_6) = all_79_3_154, yields: % 12.65/3.56 | (371) all_129_4_276 = all_79_3_154 % 12.65/3.56 | % 12.65/3.56 | Instantiating formula (30) with all_0_6_6, all_73_2_138, all_139_2_303 and discharging atoms vsucc(all_0_6_6) = all_139_2_303, vsucc(all_0_6_6) = all_73_2_138, yields: % 12.65/3.56 | (372) all_139_2_303 = all_73_2_138 % 12.65/3.56 | % 12.65/3.56 | Instantiating formula (30) with all_0_6_6, all_71_4_134, all_0_3_3 and discharging atoms vsucc(all_0_6_6) = all_71_4_134, vsucc(all_0_6_6) = all_0_3_3, yields: % 12.65/3.56 | (373) all_71_4_134 = all_0_3_3 % 12.65/3.56 | % 12.65/3.56 | Instantiating formula (30) with all_0_6_6, all_71_4_134, all_139_2_303 and discharging atoms vsucc(all_0_6_6) = all_139_2_303, vsucc(all_0_6_6) = all_71_4_134, yields: % 12.65/3.56 | (374) all_139_2_303 = all_71_4_134 % 12.65/3.56 | % 12.65/3.56 | Instantiating formula (30) with all_0_6_6, all_63_2_113, all_129_4_276 and discharging atoms vsucc(all_0_6_6) = all_129_4_276, vsucc(all_0_6_6) = all_63_2_113, yields: % 12.65/3.56 | (375) all_129_4_276 = all_63_2_113 % 12.65/3.56 | % 12.65/3.56 | Instantiating formula (41) with all_0_8_8, all_0_6_6, all_81_6_163, all_99_5_199 and discharging atoms vmul(all_0_8_8, all_0_6_6) = all_99_5_199, vmul(all_0_8_8, all_0_6_6) = all_81_6_163, yields: % 12.65/3.56 | (376) all_99_5_199 = all_81_6_163 % 12.65/3.56 | % 12.65/3.56 | Instantiating formula (41) with all_0_8_8, all_0_6_6, all_79_5_156, all_81_6_163 and discharging atoms vmul(all_0_8_8, all_0_6_6) = all_81_6_163, vmul(all_0_8_8, all_0_6_6) = all_79_5_156, yields: % 12.65/3.56 | (377) all_81_6_163 = all_79_5_156 % 12.65/3.56 | % 12.65/3.56 | Instantiating formula (41) with all_0_8_8, all_0_6_6, all_73_3_139, all_99_5_199 and discharging atoms vmul(all_0_8_8, all_0_6_6) = all_99_5_199, vmul(all_0_8_8, all_0_6_6) = all_73_3_139, yields: % 12.65/3.56 | (378) all_99_5_199 = all_73_3_139 % 12.65/3.56 | % 12.85/3.56 | Instantiating formula (41) with all_0_8_8, all_0_6_6, all_71_5_135, all_0_5_5 and discharging atoms vmul(all_0_8_8, all_0_6_6) = all_71_5_135, vmul(all_0_8_8, all_0_6_6) = all_0_5_5, yields: % 12.85/3.56 | (379) all_71_5_135 = all_0_5_5 % 12.85/3.56 | % 12.85/3.56 | Instantiating formula (41) with all_0_8_8, all_0_6_6, all_69_4_129, all_91_4_184 and discharging atoms vmul(all_0_8_8, all_0_6_6) = all_91_4_184, vmul(all_0_8_8, all_0_6_6) = all_69_4_129, yields: % 12.85/3.56 | (380) all_91_4_184 = all_69_4_129 % 12.85/3.56 | % 12.85/3.56 | Instantiating formula (41) with all_0_8_8, all_0_6_6, all_69_4_129, all_79_5_156 and discharging atoms vmul(all_0_8_8, all_0_6_6) = all_79_5_156, vmul(all_0_8_8, all_0_6_6) = all_69_4_129, yields: % 12.85/3.56 | (381) all_79_5_156 = all_69_4_129 % 12.85/3.56 | % 12.85/3.56 | Instantiating formula (41) with all_0_8_8, all_0_6_6, all_67_3_124, all_91_4_184 and discharging atoms vmul(all_0_8_8, all_0_6_6) = all_91_4_184, vmul(all_0_8_8, all_0_6_6) = all_67_3_124, yields: % 12.85/3.56 | (382) all_91_4_184 = all_67_3_124 % 12.85/3.56 | % 12.85/3.56 | Instantiating formula (41) with all_0_8_8, all_0_6_6, all_51_0_86, all_91_4_184 and discharging atoms vmul(all_0_8_8, all_0_6_6) = all_91_4_184, vmul(all_0_8_8, all_0_6_6) = all_51_0_86, yields: % 12.85/3.56 | (383) all_91_4_184 = all_51_0_86 % 12.85/3.56 | % 12.85/3.56 | Instantiating formula (41) with all_0_8_8, all_0_6_6, all_45_4_73, all_91_4_184 and discharging atoms vmul(all_0_8_8, all_0_6_6) = all_91_4_184, vmul(all_0_8_8, all_0_6_6) = all_45_4_73, yields: % 12.85/3.56 | (384) all_91_4_184 = all_45_4_73 % 12.85/3.56 | % 12.85/3.56 | Instantiating formula (41) with all_0_8_8, all_0_6_6, all_45_4_73, all_71_5_135 and discharging atoms vmul(all_0_8_8, all_0_6_6) = all_71_5_135, vmul(all_0_8_8, all_0_6_6) = all_45_4_73, yields: % 12.85/3.56 | (385) all_71_5_135 = all_45_4_73 % 12.85/3.56 | % 12.85/3.56 | Instantiating formula (41) with all_0_8_8, all_0_6_6, all_31_2_37, all_79_5_156 and discharging atoms vmul(all_0_8_8, all_0_6_6) = all_79_5_156, vmul(all_0_8_8, all_0_6_6) = all_31_2_37, yields: % 12.85/3.56 | (386) all_79_5_156 = all_31_2_37 % 12.85/3.56 | % 12.85/3.56 | Instantiating formula (41) with vd411, all_0_3_3, all_49_4_85, all_121_5_263 and discharging atoms vmul(vd411, all_0_3_3) = all_121_5_263, vmul(vd411, all_0_3_3) = all_49_4_85, yields: % 12.85/3.57 | (387) all_121_5_263 = all_49_4_85 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (41) with vd411, all_0_3_3, all_47_6_80, all_49_4_85 and discharging atoms vmul(vd411, all_0_3_3) = all_49_4_85, vmul(vd411, all_0_3_3) = all_47_6_80, yields: % 12.85/3.57 | (388) all_49_4_85 = all_47_6_80 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (41) with vd411, all_0_3_3, all_39_7_61, all_49_4_85 and discharging atoms vmul(vd411, all_0_3_3) = all_49_4_85, vmul(vd411, all_0_3_3) = all_39_7_61, yields: % 12.85/3.57 | (389) all_49_4_85 = all_39_7_61 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (41) with vd411, all_0_3_3, all_37_6_53, all_121_5_263 and discharging atoms vmul(vd411, all_0_3_3) = all_121_5_263, vmul(vd411, all_0_3_3) = all_37_6_53, yields: % 12.85/3.57 | (390) all_121_5_263 = all_37_6_53 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (41) with vd411, all_0_3_3, all_35_6_46, all_47_6_80 and discharging atoms vmul(vd411, all_0_3_3) = all_47_6_80, vmul(vd411, all_0_3_3) = all_35_6_46, yields: % 12.85/3.57 | (391) all_47_6_80 = all_35_6_46 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (41) with vd411, all_0_3_3, all_29_4_34, all_0_1_1 and discharging atoms vmul(vd411, all_0_3_3) = all_29_4_34, vmul(vd411, all_0_3_3) = all_0_1_1, yields: % 12.85/3.57 | (392) all_29_4_34 = all_0_1_1 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (41) with vd411, all_0_3_3, all_29_4_34, all_49_4_85 and discharging atoms vmul(vd411, all_0_3_3) = all_49_4_85, vmul(vd411, all_0_3_3) = all_29_4_34, yields: % 12.85/3.57 | (393) all_49_4_85 = all_29_4_34 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (41) with vd411, all_0_3_3, all_27_3_29, all_121_5_263 and discharging atoms vmul(vd411, all_0_3_3) = all_121_5_263, vmul(vd411, all_0_3_3) = all_27_3_29, yields: % 12.85/3.57 | (394) all_121_5_263 = all_27_3_29 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (41) with vd411, all_0_6_6, all_135_6_296, all_139_7_308 and discharging atoms vmul(vd411, all_0_6_6) = all_139_7_308, vmul(vd411, all_0_6_6) = all_135_6_296, yields: % 12.85/3.57 | (395) all_139_7_308 = all_135_6_296 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (41) with vd411, all_0_6_6, all_131_6_285, all_139_7_308 and discharging atoms vmul(vd411, all_0_6_6) = all_139_7_308, vmul(vd411, all_0_6_6) = all_131_6_285, yields: % 12.85/3.57 | (396) all_139_7_308 = all_131_6_285 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (41) with vd411, all_0_6_6, all_129_6_278, all_139_7_308 and discharging atoms vmul(vd411, all_0_6_6) = all_139_7_308, vmul(vd411, all_0_6_6) = all_129_6_278, yields: % 12.85/3.57 | (397) all_139_7_308 = all_129_6_278 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (41) with vd411, all_0_6_6, all_119_4_257, all_139_7_308 and discharging atoms vmul(vd411, all_0_6_6) = all_139_7_308, vmul(vd411, all_0_6_6) = all_119_4_257, yields: % 12.85/3.57 | (398) all_139_7_308 = all_119_4_257 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (41) with vd411, all_0_6_6, all_115_5_245, all_119_4_257 and discharging atoms vmul(vd411, all_0_6_6) = all_119_4_257, vmul(vd411, all_0_6_6) = all_115_5_245, yields: % 12.85/3.57 | (399) all_119_4_257 = all_115_5_245 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (41) with vd411, all_0_6_6, all_95_0_191, all_115_5_245 and discharging atoms vmul(vd411, all_0_6_6) = all_115_5_245, vmul(vd411, all_0_6_6) = all_95_0_191, yields: % 12.85/3.57 | (400) all_115_5_245 = all_95_0_191 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (41) with vd411, all_0_6_6, all_91_3_183, all_95_0_191 and discharging atoms vmul(vd411, all_0_6_6) = all_95_0_191, vmul(vd411, all_0_6_6) = all_91_3_183, yields: % 12.85/3.57 | (401) all_95_0_191 = all_91_3_183 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (41) with vd411, all_0_6_6, all_63_4_115, all_0_4_4 and discharging atoms vmul(vd411, all_0_6_6) = all_63_4_115, vmul(vd411, all_0_6_6) = all_0_4_4, yields: % 12.85/3.57 | (402) all_63_4_115 = all_0_4_4 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (41) with vd411, all_0_6_6, all_63_4_115, all_91_3_183 and discharging atoms vmul(vd411, all_0_6_6) = all_91_3_183, vmul(vd411, all_0_6_6) = all_63_4_115, yields: % 12.85/3.57 | (403) all_91_3_183 = all_63_4_115 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (41) with vd411, all_0_6_6, all_61_3_110, all_131_6_285 and discharging atoms vmul(vd411, all_0_6_6) = all_131_6_285, vmul(vd411, all_0_6_6) = all_61_3_110, yields: % 12.85/3.57 | (404) all_131_6_285 = all_61_3_110 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (31) with all_71_1_131, all_79_4_155, vd411, all_0_4_4 and discharging atoms vplus(all_0_4_4, vd411) = all_79_4_155, vplus(all_0_4_4, vd411) = all_71_1_131, yields: % 12.85/3.57 | (405) all_79_4_155 = all_71_1_131 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (31) with all_63_0_111, all_67_2_123, all_0_8_8, all_0_5_5 and discharging atoms vplus(all_0_5_5, all_0_8_8) = all_67_2_123, vplus(all_0_5_5, all_0_8_8) = all_63_0_111, yields: % 12.85/3.57 | (406) all_67_2_123 = all_63_0_111 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (31) with all_61_1_108, all_67_2_123, all_0_8_8, all_0_5_5 and discharging atoms vplus(all_0_5_5, all_0_8_8) = all_67_2_123, vplus(all_0_5_5, all_0_8_8) = all_61_1_108, yields: % 12.85/3.57 | (407) all_67_2_123 = all_61_1_108 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (31) with all_31_0_35, all_63_0_111, all_0_8_8, all_0_5_5 and discharging atoms vplus(all_0_5_5, all_0_8_8) = all_63_0_111, vplus(all_0_5_5, all_0_8_8) = all_31_0_35, yields: % 12.85/3.57 | (408) all_63_0_111 = all_31_0_35 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (31) with all_115_3_243, all_119_1_254, all_0_8_8, all_0_6_6 and discharging atoms vplus(all_0_6_6, all_0_8_8) = all_119_1_254, vplus(all_0_6_6, all_0_8_8) = all_115_3_243, yields: % 12.85/3.57 | (409) all_119_1_254 = all_115_3_243 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (31) with all_69_3_128, all_119_1_254, all_0_8_8, all_0_6_6 and discharging atoms vplus(all_0_6_6, all_0_8_8) = all_119_1_254, vplus(all_0_6_6, all_0_8_8) = all_69_3_128, yields: % 12.85/3.57 | (410) all_119_1_254 = all_69_3_128 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (31) with all_67_1_122, all_115_3_243, all_0_8_8, all_0_6_6 and discharging atoms vplus(all_0_6_6, all_0_8_8) = all_115_3_243, vplus(all_0_6_6, all_0_8_8) = all_67_1_122, yields: % 12.85/3.57 | (411) all_115_3_243 = all_67_1_122 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (31) with all_69_1_126, all_131_4_283, all_0_6_6, all_0_8_8 and discharging atoms vplus(all_0_8_8, all_0_6_6) = all_131_4_283, vplus(all_0_8_8, all_0_6_6) = all_69_1_126, yields: % 12.85/3.57 | (412) all_131_4_283 = all_69_1_126 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (31) with all_83_5_169, all_93_2_187, all_0_3_3, vd411 and discharging atoms vplus(vd411, all_0_3_3) = all_93_2_187, vplus(vd411, all_0_3_3) = all_83_5_169, yields: % 12.85/3.57 | (413) all_93_2_187 = all_83_5_169 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (31) with all_39_5_59, all_83_5_169, all_0_3_3, vd411 and discharging atoms vplus(vd411, all_0_3_3) = all_83_5_169, vplus(vd411, all_0_3_3) = all_39_5_59, yields: % 12.85/3.57 | (414) all_83_5_169 = all_39_5_59 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (31) with all_37_2_49, all_93_2_187, all_0_3_3, vd411 and discharging atoms vplus(vd411, all_0_3_3) = all_93_2_187, vplus(vd411, all_0_3_3) = all_37_2_49, yields: % 12.85/3.57 | (415) all_93_2_187 = all_37_2_49 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (31) with all_131_2_281, all_139_5_306, all_0_6_6, vd411 and discharging atoms vplus(vd411, all_0_6_6) = all_139_5_306, vplus(vd411, all_0_6_6) = all_131_2_281, yields: % 12.85/3.57 | (416) all_139_5_306 = all_131_2_281 % 12.85/3.57 | % 12.85/3.57 | Instantiating formula (31) with all_81_5_162, all_139_5_306, all_0_6_6, vd411 and discharging atoms vplus(vd411, all_0_6_6) = all_139_5_306, vplus(vd411, all_0_6_6) = all_81_5_162, yields: % 12.85/3.57 | (417) all_139_5_306 = all_81_5_162 % 12.85/3.57 | % 12.85/3.58 | Combining equations (370,372) yields a new equation: % 12.85/3.58 | (418) all_79_3_154 = all_73_2_138 % 12.85/3.58 | % 12.85/3.58 | Simplifying 418 yields: % 12.85/3.58 | (419) all_79_3_154 = all_73_2_138 % 12.85/3.58 | % 12.85/3.58 | Combining equations (374,372) yields a new equation: % 12.85/3.58 | (420) all_73_2_138 = all_71_4_134 % 12.85/3.58 | % 12.85/3.58 | Combining equations (416,417) yields a new equation: % 12.85/3.58 | (421) all_131_2_281 = all_81_5_162 % 12.85/3.58 | % 12.85/3.58 | Simplifying 421 yields: % 12.85/3.58 | (422) all_131_2_281 = all_81_5_162 % 12.85/3.58 | % 12.85/3.58 | Combining equations (396,395) yields a new equation: % 12.85/3.58 | (423) all_135_6_296 = all_131_6_285 % 12.85/3.58 | % 12.85/3.58 | Combining equations (398,395) yields a new equation: % 12.85/3.58 | (424) all_135_6_296 = all_119_4_257 % 12.85/3.58 | % 12.85/3.58 | Combining equations (397,395) yields a new equation: % 12.85/3.58 | (425) all_135_6_296 = all_129_6_278 % 12.85/3.58 | % 12.85/3.58 | Combining equations (367,368) yields a new equation: % 12.85/3.58 | (426) all_129_4_276 = all_89_1_179 % 12.85/3.58 | % 12.85/3.58 | Simplifying 426 yields: % 12.85/3.58 | (427) all_129_4_276 = all_89_1_179 % 12.85/3.58 | % 12.85/3.58 | Combining equations (423,425) yields a new equation: % 12.85/3.58 | (428) all_131_6_285 = all_129_6_278 % 12.85/3.58 | % 12.85/3.58 | Simplifying 428 yields: % 12.85/3.58 | (429) all_131_6_285 = all_129_6_278 % 12.85/3.58 | % 12.85/3.58 | Combining equations (424,425) yields a new equation: % 12.85/3.58 | (430) all_129_6_278 = all_119_4_257 % 12.85/3.58 | % 12.85/3.58 | Combining equations (429,404) yields a new equation: % 12.85/3.58 | (431) all_129_6_278 = all_61_3_110 % 12.85/3.58 | % 12.85/3.58 | Simplifying 431 yields: % 12.85/3.58 | (432) all_129_6_278 = all_61_3_110 % 12.85/3.58 | % 12.85/3.58 | Combining equations (369,427) yields a new equation: % 12.85/3.58 | (433) all_89_1_179 = all_81_2_159 % 12.85/3.58 | % 12.85/3.58 | Combining equations (371,427) yields a new equation: % 12.85/3.58 | (434) all_89_1_179 = all_79_3_154 % 12.85/3.58 | % 12.85/3.58 | Combining equations (375,427) yields a new equation: % 12.85/3.58 | (435) all_89_1_179 = all_63_2_113 % 12.85/3.58 | % 12.85/3.58 | Combining equations (430,432) yields a new equation: % 12.85/3.58 | (436) all_119_4_257 = all_61_3_110 % 12.85/3.58 | % 12.85/3.58 | Simplifying 436 yields: % 12.85/3.58 | (437) all_119_4_257 = all_61_3_110 % 12.85/3.58 | % 12.85/3.58 | Combining equations (387,390) yields a new equation: % 12.85/3.58 | (438) all_49_4_85 = all_37_6_53 % 12.85/3.58 | % 12.85/3.58 | Simplifying 438 yields: % 12.85/3.58 | (439) all_49_4_85 = all_37_6_53 % 12.85/3.58 | % 12.85/3.58 | Combining equations (394,390) yields a new equation: % 12.85/3.58 | (440) all_37_6_53 = all_27_3_29 % 12.85/3.58 | % 12.85/3.58 | Combining equations (409,410) yields a new equation: % 12.85/3.58 | (441) all_115_3_243 = all_69_3_128 % 12.85/3.58 | % 12.85/3.58 | Simplifying 441 yields: % 12.85/3.58 | (442) all_115_3_243 = all_69_3_128 % 12.85/3.58 | % 12.85/3.58 | Combining equations (399,437) yields a new equation: % 12.85/3.58 | (443) all_115_5_245 = all_61_3_110 % 12.85/3.58 | % 12.85/3.58 | Simplifying 443 yields: % 12.85/3.58 | (444) all_115_5_245 = all_61_3_110 % 12.85/3.58 | % 12.85/3.58 | Combining equations (442,411) yields a new equation: % 12.85/3.58 | (445) all_69_3_128 = all_67_1_122 % 12.85/3.58 | % 12.85/3.58 | Simplifying 445 yields: % 12.85/3.58 | (446) all_69_3_128 = all_67_1_122 % 12.85/3.58 | % 12.85/3.58 | Combining equations (400,444) yields a new equation: % 12.85/3.58 | (447) all_95_0_191 = all_61_3_110 % 12.85/3.58 | % 12.85/3.58 | Simplifying 447 yields: % 12.85/3.58 | (448) all_95_0_191 = all_61_3_110 % 12.85/3.58 | % 12.85/3.58 | Combining equations (376,378) yields a new equation: % 12.85/3.58 | (449) all_81_6_163 = all_73_3_139 % 12.85/3.58 | % 12.85/3.58 | Simplifying 449 yields: % 12.85/3.58 | (450) all_81_6_163 = all_73_3_139 % 12.85/3.58 | % 12.85/3.58 | Combining equations (401,448) yields a new equation: % 12.85/3.58 | (451) all_91_3_183 = all_61_3_110 % 12.85/3.58 | % 12.85/3.58 | Simplifying 451 yields: % 12.85/3.58 | (452) all_91_3_183 = all_61_3_110 % 12.85/3.58 | % 12.85/3.58 | Combining equations (413,415) yields a new equation: % 12.85/3.58 | (453) all_83_5_169 = all_37_2_49 % 12.85/3.58 | % 12.85/3.58 | Simplifying 453 yields: % 12.85/3.58 | (454) all_83_5_169 = all_37_2_49 % 12.85/3.58 | % 12.85/3.58 | Combining equations (403,452) yields a new equation: % 12.85/3.58 | (455) all_63_4_115 = all_61_3_110 % 12.85/3.58 | % 12.85/3.58 | Simplifying 455 yields: % 12.85/3.58 | (456) all_63_4_115 = all_61_3_110 % 12.85/3.58 | % 12.85/3.58 | Combining equations (380,382) yields a new equation: % 12.85/3.58 | (457) all_69_4_129 = all_67_3_124 % 12.85/3.58 | % 12.85/3.58 | Simplifying 457 yields: % 12.85/3.58 | (458) all_69_4_129 = all_67_3_124 % 12.85/3.58 | % 12.85/3.58 | Combining equations (383,382) yields a new equation: % 12.85/3.58 | (459) all_67_3_124 = all_51_0_86 % 12.85/3.58 | % 12.85/3.58 | Combining equations (384,382) yields a new equation: % 12.85/3.58 | (460) all_67_3_124 = all_45_4_73 % 12.85/3.58 | % 12.85/3.58 | Combining equations (435,433) yields a new equation: % 12.85/3.58 | (461) all_81_2_159 = all_63_2_113 % 12.85/3.58 | % 12.85/3.58 | Combining equations (434,433) yields a new equation: % 12.85/3.58 | (462) all_81_2_159 = all_79_3_154 % 12.85/3.58 | % 12.85/3.58 | Combining equations (414,454) yields a new equation: % 12.85/3.58 | (463) all_39_5_59 = all_37_2_49 % 12.85/3.58 | % 12.85/3.58 | Simplifying 463 yields: % 12.85/3.58 | (464) all_39_5_59 = all_37_2_49 % 12.85/3.58 | % 12.85/3.58 | Combining equations (462,461) yields a new equation: % 12.85/3.58 | (465) all_79_3_154 = all_63_2_113 % 12.85/3.58 | % 12.85/3.58 | Simplifying 465 yields: % 12.85/3.58 | (466) all_79_3_154 = all_63_2_113 % 12.85/3.58 | % 12.85/3.58 | Combining equations (377,450) yields a new equation: % 12.85/3.58 | (467) all_79_5_156 = all_73_3_139 % 12.85/3.58 | % 12.85/3.58 | Simplifying 467 yields: % 12.85/3.58 | (468) all_79_5_156 = all_73_3_139 % 12.85/3.58 | % 12.85/3.58 | Combining equations (419,466) yields a new equation: % 12.85/3.58 | (469) all_73_2_138 = all_63_2_113 % 12.85/3.58 | % 12.85/3.58 | Simplifying 469 yields: % 12.85/3.58 | (470) all_73_2_138 = all_63_2_113 % 12.85/3.58 | % 12.85/3.58 | Combining equations (381,468) yields a new equation: % 12.85/3.58 | (471) all_73_3_139 = all_69_4_129 % 12.85/3.58 | % 12.85/3.58 | Combining equations (386,468) yields a new equation: % 12.85/3.58 | (472) all_73_3_139 = all_31_2_37 % 12.85/3.58 | % 12.85/3.58 | Combining equations (420,470) yields a new equation: % 12.85/3.58 | (473) all_71_4_134 = all_63_2_113 % 12.85/3.58 | % 12.85/3.58 | Simplifying 473 yields: % 12.85/3.58 | (474) all_71_4_134 = all_63_2_113 % 12.85/3.58 | % 12.85/3.58 | Combining equations (471,472) yields a new equation: % 12.85/3.58 | (475) all_69_4_129 = all_31_2_37 % 12.85/3.58 | % 12.85/3.58 | Simplifying 475 yields: % 12.85/3.58 | (476) all_69_4_129 = all_31_2_37 % 12.85/3.58 | % 12.85/3.58 | Combining equations (373,474) yields a new equation: % 12.85/3.58 | (477) all_63_2_113 = all_0_3_3 % 12.85/3.58 | % 12.85/3.58 | Combining equations (385,379) yields a new equation: % 12.85/3.58 | (478) all_45_4_73 = all_0_5_5 % 12.85/3.58 | % 12.85/3.58 | Simplifying 478 yields: % 12.85/3.58 | (479) all_45_4_73 = all_0_5_5 % 12.85/3.58 | % 12.85/3.58 | Combining equations (458,476) yields a new equation: % 12.85/3.58 | (480) all_67_3_124 = all_31_2_37 % 12.85/3.58 | % 12.85/3.58 | Simplifying 480 yields: % 12.85/3.58 | (481) all_67_3_124 = all_31_2_37 % 12.85/3.58 | % 12.85/3.58 | Combining equations (406,407) yields a new equation: % 12.85/3.58 | (482) all_63_0_111 = all_61_1_108 % 12.85/3.58 | % 12.85/3.58 | Simplifying 482 yields: % 12.85/3.58 | (483) all_63_0_111 = all_61_1_108 % 12.85/3.58 | % 12.85/3.59 | Combining equations (481,459) yields a new equation: % 12.85/3.59 | (484) all_51_0_86 = all_31_2_37 % 12.85/3.59 | % 12.85/3.59 | Combining equations (460,459) yields a new equation: % 12.85/3.59 | (485) all_51_0_86 = all_45_4_73 % 12.85/3.59 | % 12.85/3.59 | Combining equations (408,483) yields a new equation: % 12.85/3.59 | (486) all_61_1_108 = all_31_0_35 % 12.85/3.59 | % 12.85/3.59 | Combining equations (402,456) yields a new equation: % 12.85/3.59 | (487) all_61_3_110 = all_0_4_4 % 12.85/3.59 | % 12.85/3.59 | Combining equations (485,484) yields a new equation: % 12.85/3.59 | (488) all_45_4_73 = all_31_2_37 % 12.85/3.59 | % 12.85/3.59 | Simplifying 488 yields: % 12.85/3.59 | (489) all_45_4_73 = all_31_2_37 % 12.85/3.59 | % 12.85/3.59 | Combining equations (393,389) yields a new equation: % 12.85/3.59 | (490) all_39_7_61 = all_29_4_34 % 12.85/3.59 | % 12.85/3.59 | Combining equations (439,389) yields a new equation: % 12.85/3.59 | (491) all_39_7_61 = all_37_6_53 % 12.85/3.59 | % 12.85/3.59 | Combining equations (388,389) yields a new equation: % 12.85/3.59 | (492) all_47_6_80 = all_39_7_61 % 12.85/3.59 | % 12.85/3.59 | Simplifying 492 yields: % 12.85/3.59 | (493) all_47_6_80 = all_39_7_61 % 12.85/3.59 | % 12.85/3.59 | Combining equations (493,391) yields a new equation: % 12.85/3.59 | (494) all_39_7_61 = all_35_6_46 % 12.85/3.59 | % 12.85/3.59 | Simplifying 494 yields: % 12.85/3.59 | (495) all_39_7_61 = all_35_6_46 % 12.85/3.59 | % 12.85/3.59 | Combining equations (489,479) yields a new equation: % 12.85/3.59 | (496) all_31_2_37 = all_0_5_5 % 12.85/3.59 | % 12.85/3.59 | Simplifying 496 yields: % 12.85/3.59 | (497) all_31_2_37 = all_0_5_5 % 12.85/3.59 | % 12.85/3.59 | Combining equations (491,495) yields a new equation: % 12.85/3.59 | (498) all_37_6_53 = all_35_6_46 % 12.85/3.59 | % 12.85/3.59 | Simplifying 498 yields: % 12.85/3.59 | (499) all_37_6_53 = all_35_6_46 % 12.85/3.59 | % 12.85/3.59 | Combining equations (490,495) yields a new equation: % 12.85/3.59 | (500) all_35_6_46 = all_29_4_34 % 12.85/3.59 | % 12.85/3.59 | Combining equations (499,440) yields a new equation: % 12.85/3.59 | (501) all_35_6_46 = all_27_3_29 % 12.85/3.59 | % 12.85/3.59 | Simplifying 501 yields: % 12.85/3.59 | (502) all_35_6_46 = all_27_3_29 % 12.85/3.59 | % 12.85/3.59 | Combining equations (500,502) yields a new equation: % 12.85/3.59 | (503) all_29_4_34 = all_27_3_29 % 12.85/3.59 | % 12.85/3.59 | Simplifying 503 yields: % 12.85/3.59 | (504) all_29_4_34 = all_27_3_29 % 12.85/3.59 | % 12.85/3.59 | Combining equations (392,504) yields a new equation: % 12.85/3.59 | (505) all_27_3_29 = all_0_1_1 % 12.85/3.59 | % 12.85/3.59 | Combining equations (497,484) yields a new equation: % 12.85/3.59 | (506) all_51_0_86 = all_0_5_5 % 12.85/3.59 | % 12.85/3.59 | Combining equations (487,456) yields a new equation: % 12.85/3.59 | (402) all_63_4_115 = all_0_4_4 % 12.85/3.59 | % 12.85/3.59 | Combining equations (506,459) yields a new equation: % 12.85/3.59 | (508) all_67_3_124 = all_0_5_5 % 12.85/3.59 | % 12.85/3.59 | Combining equations (486,407) yields a new equation: % 12.85/3.59 | (509) all_67_2_123 = all_31_0_35 % 12.85/3.59 | % 12.85/3.59 | Combining equations (497,476) yields a new equation: % 12.85/3.59 | (510) all_69_4_129 = all_0_5_5 % 12.85/3.59 | % 12.85/3.59 | Combining equations (477,474) yields a new equation: % 12.85/3.59 | (373) all_71_4_134 = all_0_3_3 % 12.85/3.59 | % 12.85/3.59 | Combining equations (497,472) yields a new equation: % 12.85/3.59 | (512) all_73_3_139 = all_0_5_5 % 12.85/3.59 | % 12.85/3.59 | Combining equations (477,470) yields a new equation: % 12.85/3.59 | (513) all_73_2_138 = all_0_3_3 % 12.85/3.59 | % 12.85/3.59 | Combining equations (512,468) yields a new equation: % 12.85/3.59 | (514) all_79_5_156 = all_0_5_5 % 12.85/3.59 | % 12.85/3.59 | Combining equations (477,466) yields a new equation: % 12.85/3.59 | (515) all_79_3_154 = all_0_3_3 % 12.85/3.59 | % 12.85/3.59 | Combining equations (512,450) yields a new equation: % 12.85/3.59 | (516) all_81_6_163 = all_0_5_5 % 12.85/3.59 | % 12.85/3.59 | Combining equations (477,461) yields a new equation: % 12.85/3.59 | (517) all_81_2_159 = all_0_3_3 % 12.85/3.59 | % 12.85/3.59 | Combining equations (517,433) yields a new equation: % 12.85/3.59 | (518) all_89_1_179 = all_0_3_3 % 12.85/3.59 | % 12.85/3.59 | Combining equations (508,382) yields a new equation: % 12.85/3.59 | (519) all_91_4_184 = all_0_5_5 % 12.85/3.59 | % 12.85/3.59 | Combining equations (487,452) yields a new equation: % 12.85/3.59 | (520) all_91_3_183 = all_0_4_4 % 12.85/3.59 | % 12.85/3.59 | Combining equations (487,444) yields a new equation: % 12.85/3.59 | (521) all_115_5_245 = all_0_4_4 % 12.85/3.59 | % 12.85/3.59 | Combining equations (487,437) yields a new equation: % 12.85/3.59 | (522) all_119_4_257 = all_0_4_4 % 12.85/3.59 | % 12.85/3.59 | Combining equations (446,410) yields a new equation: % 12.85/3.59 | (523) all_119_1_254 = all_67_1_122 % 12.85/3.59 | % 12.85/3.59 | Combining equations (487,432) yields a new equation: % 12.85/3.59 | (524) all_129_6_278 = all_0_4_4 % 12.85/3.59 | % 12.85/3.59 | Combining equations (518,427) yields a new equation: % 12.85/3.59 | (525) all_129_4_276 = all_0_3_3 % 12.85/3.59 | % 12.85/3.59 | Combining equations (487,404) yields a new equation: % 12.85/3.59 | (526) all_131_6_285 = all_0_4_4 % 12.85/3.59 | % 12.85/3.59 | Combining equations (524,425) yields a new equation: % 12.85/3.59 | (527) all_135_6_296 = all_0_4_4 % 12.85/3.59 | % 12.85/3.59 | Combining equations (518,368) yields a new equation: % 12.85/3.59 | (528) all_135_3_293 = all_0_3_3 % 12.85/3.59 | % 12.85/3.59 | Combining equations (527,395) yields a new equation: % 12.85/3.59 | (529) all_139_7_308 = all_0_4_4 % 12.85/3.59 | % 12.85/3.59 | Combining equations (513,372) yields a new equation: % 12.85/3.59 | (530) all_139_2_303 = all_0_3_3 % 12.85/3.59 | % 12.85/3.59 | From (422) and (346) follows: % 12.85/3.59 | (531) vsucc(all_81_5_162) = all_131_1_280 % 12.85/3.59 | % 12.85/3.59 | From (528) and (351) follows: % 12.85/3.59 | (532) vmul(vd411, all_0_3_3) = all_135_1_291 % 12.85/3.59 | % 12.85/3.59 | From (515) and (253) follows: % 12.85/3.59 | (533) vmul(vd411, all_0_3_3) = all_79_1_152 % 12.85/3.59 | % 12.85/3.59 | From (505) and (141) follows: % 12.85/3.59 | (92) vmul(vd411, all_0_3_3) = all_0_1_1 % 12.85/3.59 | % 12.85/3.59 | From (529) and (360) follows: % 12.85/3.59 | (535) vplus(all_0_4_4, all_139_1_302) = all_139_0_301 % 12.85/3.59 | % 12.85/3.59 | From (529) and (359) follows: % 12.85/3.59 | (536) vplus(all_0_4_4, all_0_6_6) = all_139_6_307 % 12.85/3.59 | % 12.85/3.59 | From (528) and (354) follows: % 12.85/3.59 | (537) vplus(all_135_1_291, all_0_3_3) = all_135_0_290 % 12.85/3.59 | % 12.85/3.59 | From (527) and (356) follows: % 12.85/3.59 | (538) vplus(all_0_4_4, all_0_6_6) = all_135_5_295 % 12.85/3.59 | % 12.85/3.59 | From (527) and (353) follows: % 12.85/3.59 | (539) vplus(all_0_4_4, vd411) = all_135_4_294 % 12.85/3.59 | % 12.85/3.59 | From (526) and (341) follows: % 12.85/3.59 | (540) vplus(all_0_4_4, all_131_1_280) = all_131_0_279 % 12.85/3.59 | % 12.85/3.59 | From (526)(412) and (343) follows: % 12.85/3.59 | (541) vplus(all_0_4_4, all_69_1_126) = all_131_3_282 % 12.85/3.59 | % 12.85/3.59 | From (526) and (340) follows: % 12.85/3.59 | (542) vplus(all_0_4_4, all_0_6_6) = all_131_5_284 % 12.85/3.59 | % 12.85/3.59 | From (525) and (338) follows: % 12.85/3.59 | (543) vplus(all_129_1_273, all_0_3_3) = all_129_0_272 % 12.85/3.59 | % 12.85/3.59 | From (524) and (331) follows: % 12.85/3.59 | (544) vplus(all_0_4_4, all_129_3_275) = all_129_2_274 % 12.85/3.59 | % 12.85/3.59 | From (524) and (334) follows: % 12.85/3.59 | (545) vplus(all_0_4_4, all_0_6_6) = all_129_5_277 % 12.85/3.59 | % 12.85/3.59 | From (524) and (337) follows: % 12.85/3.59 | (546) vplus(all_0_4_4, vd411) = all_129_1_273 % 12.85/3.59 | % 12.85/3.59 | From (522)(523) and (317) follows: % 12.85/3.59 | (547) vplus(all_0_4_4, all_67_1_122) = all_119_0_253 % 12.85/3.59 | % 12.85/3.59 | From (522) and (321) follows: % 12.85/3.59 | (548) vplus(all_0_4_4, all_0_6_6) = all_119_3_256 % 12.85/3.59 | % 12.85/3.59 | From (521)(411) and (314) follows: % 12.85/3.59 | (549) vplus(all_0_4_4, all_67_1_122) = all_115_2_242 % 12.85/3.59 | % 12.85/3.59 | From (521) and (308) follows: % 12.85/3.59 | (550) vplus(all_0_4_4, all_0_6_6) = all_115_4_244 % 12.85/3.59 | % 12.85/3.59 | From (520) and (284) follows: % 12.85/3.59 | (551) vplus(all_0_4_4, all_0_6_6) = all_91_2_182 % 12.85/3.59 | % 12.85/3.59 | From (520) and (285) follows: % 12.85/3.59 | (552) vplus(all_0_4_4, vd411) = all_91_1_181 % 12.85/3.59 | % 12.85/3.59 | From (515) and (258) follows: % 12.85/3.59 | (553) vplus(all_79_1_152, all_0_3_3) = all_79_0_151 % 12.85/3.59 | % 12.85/3.59 | From (405)(515) and (257) follows: % 12.85/3.59 | (554) vplus(all_71_1_131, all_0_3_3) = all_79_2_153 % 12.85/3.59 | % 12.85/3.59 | From (512) and (247) follows: % 12.85/3.59 | (555) vplus(all_0_5_5, all_0_8_8) = all_73_0_136 % 12.85/3.59 | % 12.85/3.59 | From (373) and (243) follows: % 12.85/3.59 | (556) vplus(all_71_1_131, all_0_3_3) = all_71_0_130 % 12.85/3.59 | % 12.85/3.59 | From (402) and (222) follows: % 12.85/3.59 | (557) vplus(all_0_4_4, all_0_6_6) = all_63_3_114 % 12.85/3.59 | % 12.85/3.59 | From (506) and (210) follows: % 12.85/3.59 | (558) vplus(all_0_5_5, all_0_8_8) = all_0_2_2 % 12.85/3.59 | % 12.85/3.59 | From (479) and (190) follows: % 12.85/3.59 | (559) vplus(all_0_5_5, all_0_8_8) = all_45_0_69 % 12.85/3.59 | % 12.85/3.59 | From (446) and (235) follows: % 12.85/3.60 | (560) vplus(all_0_4_4, all_67_1_122) = all_69_2_127 % 12.85/3.60 | % 12.85/3.60 | From (405) and (256) follows: % 12.85/3.60 | (244) vplus(all_0_4_4, vd411) = all_71_1_131 % 12.85/3.60 | % 12.85/3.60 | From (486) and (216) follows: % 12.85/3.60 | (155) vplus(all_0_5_5, all_0_8_8) = all_31_0_35 % 12.85/3.60 | % 12.85/3.60 | From (530) and (366) follows: % 12.85/3.60 | (563) vplus(vd411, all_0_3_3) = all_139_1_302 % 12.85/3.60 | % 12.85/3.60 | From (525) and (333) follows: % 12.85/3.60 | (564) vplus(vd411, all_0_3_3) = all_129_3_275 % 12.85/3.60 | % 12.85/3.60 | From (517) and (262) follows: % 12.85/3.60 | (565) vplus(vd411, all_0_3_3) = all_81_1_158 % 12.85/3.60 | % 12.85/3.60 | From (373) and (241) follows: % 12.85/3.60 | (566) vplus(vd411, all_0_3_3) = all_71_3_133 % 12.85/3.60 | % 12.85/3.60 | From (464) and (181) follows: % 12.85/3.60 | (168) vplus(vd411, all_0_3_3) = all_37_2_49 % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (261), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (568) ~ (all_81_6_163 = all_0_5_5) % 12.85/3.60 | % 12.85/3.60 | Equations (516) can reduce 568 to: % 12.85/3.60 | (569) $false % 12.85/3.60 | % 12.85/3.60 |-The branch is then unsatisfiable % 12.85/3.60 |-Branch two: % 12.85/3.60 | (516) all_81_6_163 = all_0_5_5 % 12.85/3.60 | (571) all_81_0_157 = all_81_3_160 % 12.85/3.60 | % 12.85/3.60 | From (571) and (267) follows: % 12.85/3.60 | (572) vplus(all_0_4_4, all_81_1_158) = all_81_3_160 % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (225), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (573) ~ (all_67_3_124 = all_0_5_5) % 12.85/3.60 | % 12.85/3.60 | Equations (508) can reduce 573 to: % 12.85/3.60 | (569) $false % 12.85/3.60 | % 12.85/3.60 |-The branch is then unsatisfiable % 12.85/3.60 |-Branch two: % 12.85/3.60 | (508) all_67_3_124 = all_0_5_5 % 12.85/3.60 | (576) all_67_0_121 = all_67_2_123 % 12.85/3.60 | % 12.85/3.60 | Combining equations (509,576) yields a new equation: % 12.85/3.60 | (577) all_67_0_121 = all_31_0_35 % 12.85/3.60 | % 12.85/3.60 | From (577) and (228) follows: % 12.85/3.60 | (578) vplus(all_0_4_4, all_67_1_122) = all_31_0_35 % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (231), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (579) ~ (all_69_4_129 = all_0_5_5) % 12.85/3.60 | % 12.85/3.60 | Equations (510) can reduce 579 to: % 12.85/3.60 | (569) $false % 12.85/3.60 | % 12.85/3.60 |-The branch is then unsatisfiable % 12.85/3.60 |-Branch two: % 12.85/3.60 | (510) all_69_4_129 = all_0_5_5 % 12.85/3.60 | (582) all_69_0_125 = all_69_2_127 % 12.85/3.60 | % 12.85/3.60 | From (582) and (236) follows: % 12.85/3.60 | (583) vplus(all_0_4_4, all_69_1_126) = all_69_2_127 % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (156), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (584) ~ (all_31_2_37 = all_0_5_5) % 12.85/3.60 | % 12.85/3.60 | Equations (497) can reduce 584 to: % 12.85/3.60 | (569) $false % 12.85/3.60 | % 12.85/3.60 |-The branch is then unsatisfiable % 12.85/3.60 |-Branch two: % 12.85/3.60 | (497) all_31_2_37 = all_0_5_5 % 12.85/3.60 | (587) all_31_0_35 = all_31_1_36 % 12.85/3.60 | % 12.85/3.60 | From (587) and (578) follows: % 12.85/3.60 | (588) vplus(all_0_4_4, all_67_1_122) = all_31_1_36 % 12.85/3.60 | % 12.85/3.60 | From (587) and (155) follows: % 12.85/3.60 | (589) vplus(all_0_5_5, all_0_8_8) = all_31_1_36 % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (242), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (590) ~ (all_71_5_135 = all_0_5_5) % 12.85/3.60 | % 12.85/3.60 | Equations (379) can reduce 590 to: % 12.85/3.60 | (569) $false % 12.85/3.60 | % 12.85/3.60 |-The branch is then unsatisfiable % 12.85/3.60 |-Branch two: % 12.85/3.60 | (379) all_71_5_135 = all_0_5_5 % 12.85/3.60 | (593) all_71_0_130 = all_71_2_132 % 12.85/3.60 | % 12.85/3.60 | From (593) and (556) follows: % 12.85/3.60 | (594) vplus(all_71_1_131, all_0_3_3) = all_71_2_132 % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (255), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (595) ~ (all_79_5_156 = all_0_5_5) % 12.85/3.60 | % 12.85/3.60 | Equations (514) can reduce 595 to: % 12.85/3.60 | (569) $false % 12.85/3.60 | % 12.85/3.60 |-The branch is then unsatisfiable % 12.85/3.60 |-Branch two: % 12.85/3.60 | (514) all_79_5_156 = all_0_5_5 % 12.85/3.60 | (598) all_79_0_151 = all_79_2_153 % 12.85/3.60 | % 12.85/3.60 | From (598) and (553) follows: % 12.85/3.60 | (599) vplus(all_79_1_152, all_0_3_3) = all_79_2_153 % 12.85/3.60 | % 12.85/3.60 +-Applying beta-rule and splitting (248), into two cases. % 12.85/3.60 |-Branch one: % 12.85/3.60 | (600) ~ (all_73_3_139 = all_0_5_5) % 12.85/3.60 | % 12.85/3.60 | Equations (512) can reduce 600 to: % 12.85/3.60 | (569) $false % 12.85/3.60 | % 12.85/3.60 |-The branch is then unsatisfiable % 12.85/3.60 |-Branch two: % 12.85/3.60 | (512) all_73_3_139 = all_0_5_5 % 12.85/3.60 | (603) all_73_0_136 = all_73_1_137 % 12.85/3.60 | % 12.85/3.60 | From (603) and (555) follows: % 12.85/3.60 | (604) vplus(all_0_5_5, all_0_8_8) = all_73_1_137 % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (30) with all_81_5_162, all_131_1_280, all_81_4_161 and discharging atoms vsucc(all_81_5_162) = all_131_1_280, vsucc(all_81_5_162) = all_81_4_161, yields: % 12.85/3.60 | (605) all_131_1_280 = all_81_4_161 % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (41) with vd411, all_0_3_3, all_135_1_291, all_0_1_1 and discharging atoms vmul(vd411, all_0_3_3) = all_135_1_291, vmul(vd411, all_0_3_3) = all_0_1_1, yields: % 12.85/3.60 | (606) all_135_1_291 = all_0_1_1 % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (41) with vd411, all_0_3_3, all_79_1_152, all_135_1_291 and discharging atoms vmul(vd411, all_0_3_3) = all_135_1_291, vmul(vd411, all_0_3_3) = all_79_1_152, yields: % 12.85/3.60 | (607) all_135_1_291 = all_79_1_152 % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (97) with all_79_2_153, all_0_3_3, all_71_1_131, all_79_1_152 and discharging atoms vplus(all_79_1_152, all_0_3_3) = all_79_2_153, vplus(all_71_1_131, all_0_3_3) = all_79_2_153, yields: % 12.85/3.60 | (608) all_79_1_152 = all_71_1_131 % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (31) with all_69_2_127, all_131_3_282, all_69_1_126, all_0_4_4 and discharging atoms vplus(all_0_4_4, all_69_1_126) = all_131_3_282, vplus(all_0_4_4, all_69_1_126) = all_69_2_127, yields: % 12.85/3.60 | (609) all_131_3_282 = all_69_2_127 % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (31) with all_115_2_242, all_119_0_253, all_67_1_122, all_0_4_4 and discharging atoms vplus(all_0_4_4, all_67_1_122) = all_119_0_253, vplus(all_0_4_4, all_67_1_122) = all_115_2_242, yields: % 12.85/3.60 | (610) all_119_0_253 = all_115_2_242 % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (31) with all_69_2_127, all_119_0_253, all_67_1_122, all_0_4_4 and discharging atoms vplus(all_0_4_4, all_67_1_122) = all_119_0_253, vplus(all_0_4_4, all_67_1_122) = all_69_2_127, yields: % 12.85/3.60 | (611) all_119_0_253 = all_69_2_127 % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (31) with all_31_1_36, all_115_2_242, all_67_1_122, all_0_4_4 and discharging atoms vplus(all_0_4_4, all_67_1_122) = all_115_2_242, vplus(all_0_4_4, all_67_1_122) = all_31_1_36, yields: % 12.85/3.60 | (612) all_115_2_242 = all_31_1_36 % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (31) with all_135_5_295, all_139_6_307, all_0_6_6, all_0_4_4 and discharging atoms vplus(all_0_4_4, all_0_6_6) = all_139_6_307, vplus(all_0_4_4, all_0_6_6) = all_135_5_295, yields: % 12.85/3.60 | (613) all_139_6_307 = all_135_5_295 % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (31) with all_131_5_284, all_135_5_295, all_0_6_6, all_0_4_4 and discharging atoms vplus(all_0_4_4, all_0_6_6) = all_135_5_295, vplus(all_0_4_4, all_0_6_6) = all_131_5_284, yields: % 12.85/3.60 | (614) all_135_5_295 = all_131_5_284 % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (31) with all_129_5_277, all_131_5_284, all_0_6_6, all_0_4_4 and discharging atoms vplus(all_0_4_4, all_0_6_6) = all_131_5_284, vplus(all_0_4_4, all_0_6_6) = all_129_5_277, yields: % 12.85/3.60 | (615) all_131_5_284 = all_129_5_277 % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (31) with all_119_3_256, all_129_5_277, all_0_6_6, all_0_4_4 and discharging atoms vplus(all_0_4_4, all_0_6_6) = all_129_5_277, vplus(all_0_4_4, all_0_6_6) = all_119_3_256, yields: % 12.85/3.60 | (616) all_129_5_277 = all_119_3_256 % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (31) with all_115_4_244, all_119_3_256, all_0_6_6, all_0_4_4 and discharging atoms vplus(all_0_4_4, all_0_6_6) = all_119_3_256, vplus(all_0_4_4, all_0_6_6) = all_115_4_244, yields: % 12.85/3.60 | (617) all_119_3_256 = all_115_4_244 % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (31) with all_91_2_182, all_0_5_5, all_0_6_6, all_0_4_4 and discharging atoms vplus(all_0_4_4, all_0_6_6) = all_91_2_182, vplus(all_0_4_4, all_0_6_6) = all_0_5_5, yields: % 12.85/3.60 | (618) all_91_2_182 = all_0_5_5 % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (31) with all_91_2_182, all_115_4_244, all_0_6_6, all_0_4_4 and discharging atoms vplus(all_0_4_4, all_0_6_6) = all_115_4_244, vplus(all_0_4_4, all_0_6_6) = all_91_2_182, yields: % 12.85/3.60 | (619) all_115_4_244 = all_91_2_182 % 12.85/3.60 | % 12.85/3.60 | Instantiating formula (31) with all_63_3_114, all_139_6_307, all_0_6_6, all_0_4_4 and discharging atoms vplus(all_0_4_4, all_0_6_6) = all_139_6_307, vplus(all_0_4_4, all_0_6_6) = all_63_3_114, yields: % 12.85/3.60 | (620) all_139_6_307 = all_63_3_114 % 12.85/3.60 | % 12.85/3.61 | Instantiating formula (31) with all_135_4_294, all_71_1_131, vd411, all_0_4_4 and discharging atoms vplus(all_0_4_4, vd411) = all_135_4_294, vplus(all_0_4_4, vd411) = all_71_1_131, yields: % 12.85/3.61 | (621) all_135_4_294 = all_71_1_131 % 12.85/3.61 | % 12.85/3.61 | Instantiating formula (31) with all_129_1_273, all_135_4_294, vd411, all_0_4_4 and discharging atoms vplus(all_0_4_4, vd411) = all_135_4_294, vplus(all_0_4_4, vd411) = all_129_1_273, yields: % 12.85/3.61 | (622) all_135_4_294 = all_129_1_273 % 12.85/3.61 | % 12.85/3.61 | Instantiating formula (31) with all_91_1_181, all_135_4_294, vd411, all_0_4_4 and discharging atoms vplus(all_0_4_4, vd411) = all_135_4_294, vplus(all_0_4_4, vd411) = all_91_1_181, yields: % 12.85/3.61 | (623) all_135_4_294 = all_91_1_181 % 12.85/3.61 | % 12.85/3.61 | Instantiating formula (31) with all_45_0_69, all_73_1_137, all_0_8_8, all_0_5_5 and discharging atoms vplus(all_0_5_5, all_0_8_8) = all_73_1_137, vplus(all_0_5_5, all_0_8_8) = all_45_0_69, yields: % 12.85/3.61 | (624) all_73_1_137 = all_45_0_69 % 12.85/3.61 | % 12.85/3.61 | Instantiating formula (31) with all_31_1_36, all_45_0_69, all_0_8_8, all_0_5_5 and discharging atoms vplus(all_0_5_5, all_0_8_8) = all_45_0_69, vplus(all_0_5_5, all_0_8_8) = all_31_1_36, yields: % 12.85/3.61 | (625) all_45_0_69 = all_31_1_36 % 12.85/3.61 | % 12.85/3.61 | Instantiating formula (31) with all_0_2_2, all_73_1_137, all_0_8_8, all_0_5_5 and discharging atoms vplus(all_0_5_5, all_0_8_8) = all_73_1_137, vplus(all_0_5_5, all_0_8_8) = all_0_2_2, yields: % 12.85/3.61 | (626) all_73_1_137 = all_0_2_2 % 12.85/3.61 | % 12.85/3.61 | Instantiating formula (31) with all_139_1_302, all_37_2_49, all_0_3_3, vd411 and discharging atoms vplus(vd411, all_0_3_3) = all_139_1_302, vplus(vd411, all_0_3_3) = all_37_2_49, yields: % 12.85/3.61 | (627) all_139_1_302 = all_37_2_49 % 12.85/3.61 | % 12.85/3.61 | Instantiating formula (31) with all_129_3_275, all_139_1_302, all_0_3_3, vd411 and discharging atoms vplus(vd411, all_0_3_3) = all_139_1_302, vplus(vd411, all_0_3_3) = all_129_3_275, yields: % 12.85/3.61 | (628) all_139_1_302 = all_129_3_275 % 12.85/3.61 | % 12.85/3.61 | Instantiating formula (31) with all_81_1_158, all_129_3_275, all_0_3_3, vd411 and discharging atoms vplus(vd411, all_0_3_3) = all_129_3_275, vplus(vd411, all_0_3_3) = all_81_1_158, yields: % 12.85/3.61 | (629) all_129_3_275 = all_81_1_158 % 12.85/3.61 | % 12.85/3.61 | Instantiating formula (31) with all_71_3_133, all_81_1_158, all_0_3_3, vd411 and discharging atoms vplus(vd411, all_0_3_3) = all_81_1_158, vplus(vd411, all_0_3_3) = all_71_3_133, yields: % 12.85/3.61 | (630) all_81_1_158 = all_71_3_133 % 12.85/3.61 | % 12.85/3.61 | Combining equations (628,627) yields a new equation: % 12.85/3.61 | (631) all_129_3_275 = all_37_2_49 % 12.85/3.61 | % 12.85/3.61 | Simplifying 631 yields: % 12.85/3.61 | (632) all_129_3_275 = all_37_2_49 % 12.85/3.61 | % 12.85/3.61 | Combining equations (613,620) yields a new equation: % 12.85/3.61 | (633) all_135_5_295 = all_63_3_114 % 12.85/3.61 | % 12.85/3.61 | Simplifying 633 yields: % 12.85/3.61 | (634) all_135_5_295 = all_63_3_114 % 12.85/3.61 | % 12.85/3.61 | Combining equations (607,606) yields a new equation: % 12.85/3.61 | (635) all_79_1_152 = all_0_1_1 % 12.85/3.61 | % 12.85/3.61 | Simplifying 635 yields: % 12.85/3.61 | (636) all_79_1_152 = all_0_1_1 % 12.85/3.61 | % 12.85/3.61 | Combining equations (623,622) yields a new equation: % 12.85/3.61 | (637) all_129_1_273 = all_91_1_181 % 12.85/3.61 | % 12.85/3.61 | Combining equations (621,622) yields a new equation: % 12.85/3.61 | (638) all_129_1_273 = all_71_1_131 % 12.85/3.61 | % 12.85/3.61 | Combining equations (614,634) yields a new equation: % 12.85/3.61 | (639) all_131_5_284 = all_63_3_114 % 12.85/3.61 | % 12.85/3.61 | Simplifying 639 yields: % 12.85/3.61 | (640) all_131_5_284 = all_63_3_114 % 12.85/3.61 | % 12.85/3.61 | Combining equations (615,640) yields a new equation: % 12.85/3.61 | (641) all_129_5_277 = all_63_3_114 % 12.85/3.61 | % 12.85/3.61 | Simplifying 641 yields: % 12.85/3.61 | (642) all_129_5_277 = all_63_3_114 % 12.85/3.61 | % 12.85/3.61 | Combining equations (638,637) yields a new equation: % 12.85/3.61 | (643) all_91_1_181 = all_71_1_131 % 12.85/3.61 | % 12.85/3.61 | Combining equations (629,632) yields a new equation: % 12.85/3.61 | (644) all_81_1_158 = all_37_2_49 % 12.85/3.61 | % 12.85/3.61 | Simplifying 644 yields: % 12.85/3.61 | (645) all_81_1_158 = all_37_2_49 % 12.85/3.61 | % 12.85/3.61 | Combining equations (616,642) yields a new equation: % 12.85/3.61 | (646) all_119_3_256 = all_63_3_114 % 12.85/3.61 | % 12.85/3.61 | Simplifying 646 yields: % 12.85/3.61 | (647) all_119_3_256 = all_63_3_114 % 12.85/3.61 | % 12.85/3.61 | Combining equations (610,611) yields a new equation: % 12.85/3.61 | (648) all_115_2_242 = all_69_2_127 % 12.85/3.61 | % 12.85/3.61 | Simplifying 648 yields: % 12.85/3.61 | (649) all_115_2_242 = all_69_2_127 % 12.85/3.61 | % 12.85/3.61 | Combining equations (617,647) yields a new equation: % 12.85/3.61 | (650) all_115_4_244 = all_63_3_114 % 12.85/3.61 | % 12.85/3.61 | Simplifying 650 yields: % 12.85/3.61 | (651) all_115_4_244 = all_63_3_114 % 12.85/3.61 | % 12.85/3.61 | Combining equations (612,649) yields a new equation: % 12.85/3.61 | (652) all_69_2_127 = all_31_1_36 % 12.85/3.61 | % 12.85/3.61 | Combining equations (619,651) yields a new equation: % 12.85/3.61 | (653) all_91_2_182 = all_63_3_114 % 12.85/3.61 | % 12.85/3.61 | Simplifying 653 yields: % 12.85/3.61 | (654) all_91_2_182 = all_63_3_114 % 12.85/3.61 | % 12.85/3.61 | Combining equations (618,654) yields a new equation: % 12.85/3.61 | (655) all_63_3_114 = all_0_5_5 % 12.85/3.61 | % 12.85/3.61 | Combining equations (645,630) yields a new equation: % 12.85/3.61 | (656) all_71_3_133 = all_37_2_49 % 12.85/3.61 | % 12.85/3.61 | Combining equations (608,636) yields a new equation: % 12.85/3.61 | (657) all_71_1_131 = all_0_1_1 % 12.85/3.61 | % 12.85/3.61 | Simplifying 657 yields: % 12.85/3.61 | (658) all_71_1_131 = all_0_1_1 % 12.85/3.61 | % 12.85/3.61 | Combining equations (624,626) yields a new equation: % 12.85/3.61 | (659) all_45_0_69 = all_0_2_2 % 12.85/3.61 | % 12.85/3.61 | Simplifying 659 yields: % 12.85/3.61 | (660) all_45_0_69 = all_0_2_2 % 12.85/3.61 | % 12.85/3.61 | Combining equations (660,625) yields a new equation: % 12.85/3.61 | (661) all_31_1_36 = all_0_2_2 % 12.85/3.61 | % 12.85/3.61 | Combining equations (661,652) yields a new equation: % 12.85/3.61 | (662) all_69_2_127 = all_0_2_2 % 12.85/3.61 | % 12.85/3.61 | Combining equations (656,630) yields a new equation: % 12.85/3.61 | (645) all_81_1_158 = all_37_2_49 % 12.85/3.61 | % 12.85/3.61 | Combining equations (655,654) yields a new equation: % 12.85/3.61 | (618) all_91_2_182 = all_0_5_5 % 12.85/3.61 | % 12.85/3.61 | Combining equations (658,643) yields a new equation: % 12.85/3.61 | (665) all_91_1_181 = all_0_1_1 % 12.85/3.61 | % 12.85/3.61 | Combining equations (655,642) yields a new equation: % 12.85/3.61 | (666) all_129_5_277 = all_0_5_5 % 12.85/3.61 | % 12.85/3.61 | Combining equations (665,637) yields a new equation: % 12.85/3.61 | (667) all_129_1_273 = all_0_1_1 % 12.85/3.61 | % 12.85/3.61 | Combining equations (655,640) yields a new equation: % 12.85/3.61 | (668) all_131_5_284 = all_0_5_5 % 12.85/3.61 | % 12.85/3.61 | Combining equations (662,609) yields a new equation: % 12.85/3.61 | (669) all_131_3_282 = all_0_2_2 % 12.85/3.61 | % 12.85/3.61 | Combining equations (655,634) yields a new equation: % 12.85/3.61 | (670) all_135_5_295 = all_0_5_5 % 12.85/3.61 | % 12.85/3.61 | Combining equations (655,620) yields a new equation: % 12.85/3.61 | (671) all_139_6_307 = all_0_5_5 % 12.85/3.61 | % 12.85/3.61 | From (606) and (537) follows: % 12.85/3.61 | (672) vplus(all_0_1_1, all_0_3_3) = all_135_0_290 % 12.85/3.61 | % 12.85/3.61 | From (667) and (543) follows: % 12.85/3.61 | (673) vplus(all_0_1_1, all_0_3_3) = all_129_0_272 % 12.85/3.61 | % 12.85/3.61 | From (665) and (282) follows: % 12.85/3.61 | (674) vplus(all_0_1_1, all_0_3_3) = all_91_0_180 % 12.85/3.61 | % 12.85/3.61 | From (658) and (594) follows: % 12.85/3.61 | (675) vplus(all_0_1_1, all_0_3_3) = all_71_2_132 % 12.85/3.61 | % 12.85/3.61 | From (627) and (535) follows: % 12.85/3.61 | (676) vplus(all_0_4_4, all_37_2_49) = all_139_0_301 % 12.85/3.61 | % 12.85/3.61 | From (605) and (540) follows: % 12.85/3.61 | (677) vplus(all_0_4_4, all_81_4_161) = all_131_0_279 % 12.85/3.61 | % 12.85/3.61 | From (632) and (544) follows: % 12.85/3.61 | (678) vplus(all_0_4_4, all_37_2_49) = all_129_2_274 % 12.85/3.61 | % 12.85/3.61 | From (645) and (572) follows: % 12.85/3.61 | (679) vplus(all_0_4_4, all_37_2_49) = all_81_3_160 % 12.85/3.61 | % 12.85/3.61 +-Applying beta-rule and splitting (286), into two cases. % 12.85/3.61 |-Branch one: % 12.85/3.61 | (680) ~ (all_91_2_182 = all_91_4_184) % 12.85/3.61 | % 12.85/3.61 | Equations (618,519) can reduce 680 to: % 12.85/3.61 | (569) $false % 12.85/3.61 | % 12.85/3.61 |-The branch is then unsatisfiable % 12.85/3.61 |-Branch two: % 12.85/3.61 | (682) all_91_2_182 = all_91_4_184 % 12.85/3.61 | (683) all_91_0_180 = all_0_0_0 % 12.85/3.61 | % 12.85/3.61 | From (683) and (674) follows: % 12.85/3.61 | (63) vplus(all_0_1_1, all_0_3_3) = all_0_0_0 % 12.85/3.61 | % 12.85/3.61 +-Applying beta-rule and splitting (344), into two cases. % 12.85/3.61 |-Branch one: % 12.85/3.61 | (685) ~ (all_131_5_284 = all_0_5_5) % 12.85/3.61 | % 12.85/3.61 | Equations (668) can reduce 685 to: % 12.85/3.61 | (569) $false % 12.85/3.61 | % 12.85/3.61 |-The branch is then unsatisfiable % 12.85/3.61 |-Branch two: % 12.85/3.61 | (668) all_131_5_284 = all_0_5_5 % 12.85/3.61 | (688) all_131_0_279 = all_131_3_282 % 12.85/3.61 | % 12.85/3.61 | Combining equations (669,688) yields a new equation: % 12.85/3.61 | (689) all_131_0_279 = all_0_2_2 % 12.85/3.61 | % 12.85/3.61 | From (689) and (677) follows: % 12.85/3.61 | (690) vplus(all_0_4_4, all_81_4_161) = all_0_2_2 % 12.85/3.61 | % 12.85/3.61 +-Applying beta-rule and splitting (361), into two cases. % 12.85/3.61 |-Branch one: % 12.85/3.61 | (691) ~ (all_139_6_307 = all_0_5_5) % 12.85/3.61 | % 12.85/3.61 | Equations (671) can reduce 691 to: % 12.85/3.61 | (569) $false % 12.85/3.61 | % 12.85/3.61 |-The branch is then unsatisfiable % 12.85/3.61 |-Branch two: % 12.85/3.61 | (671) all_139_6_307 = all_0_5_5 % 12.85/3.61 | (694) all_139_0_301 = all_139_3_304 % 12.85/3.61 | % 12.85/3.61 | From (694) and (676) follows: % 12.85/3.61 | (695) vplus(all_0_4_4, all_37_2_49) = all_139_3_304 % 12.85/3.61 | % 12.85/3.61 +-Applying beta-rule and splitting (352), into two cases. % 12.85/3.61 |-Branch one: % 12.85/3.61 | (696) ~ (all_135_5_295 = all_0_5_5) % 12.85/3.61 | % 12.85/3.61 | Equations (670) can reduce 696 to: % 12.85/3.61 | (569) $false % 12.85/3.61 | % 12.85/3.61 |-The branch is then unsatisfiable % 12.85/3.61 |-Branch two: % 12.85/3.61 | (670) all_135_5_295 = all_0_5_5 % 12.85/3.61 | (699) all_135_0_290 = all_135_2_292 % 12.85/3.61 | % 12.85/3.61 | From (699) and (672) follows: % 12.85/3.61 | (700) vplus(all_0_1_1, all_0_3_3) = all_135_2_292 % 12.85/3.61 | % 12.85/3.61 +-Applying beta-rule and splitting (335), into two cases. % 12.85/3.61 |-Branch one: % 12.85/3.61 | (701) ~ (all_129_5_277 = all_0_5_5) % 12.85/3.61 | % 12.85/3.61 | Equations (666) can reduce 701 to: % 12.85/3.61 | (569) $false % 12.85/3.61 | % 12.85/3.61 |-The branch is then unsatisfiable % 12.85/3.61 |-Branch two: % 12.85/3.61 | (666) all_129_5_277 = all_0_5_5 % 12.85/3.61 | (704) all_129_0_272 = all_129_2_274 % 12.85/3.61 | % 12.85/3.61 | From (704) and (673) follows: % 12.85/3.61 | (705) vplus(all_0_1_1, all_0_3_3) = all_129_2_274 % 12.85/3.61 | % 12.85/3.61 | Instantiating formula (31) with all_135_2_292, all_0_0_0, all_0_3_3, all_0_1_1 and discharging atoms vplus(all_0_1_1, all_0_3_3) = all_135_2_292, vplus(all_0_1_1, all_0_3_3) = all_0_0_0, yields: % 12.85/3.61 | (706) all_135_2_292 = all_0_0_0 % 12.85/3.61 | % 12.85/3.61 | Instantiating formula (31) with all_129_2_274, all_135_2_292, all_0_3_3, all_0_1_1 and discharging atoms vplus(all_0_1_1, all_0_3_3) = all_135_2_292, vplus(all_0_1_1, all_0_3_3) = all_129_2_274, yields: % 12.85/3.61 | (707) all_135_2_292 = all_129_2_274 % 12.85/3.61 | % 12.85/3.61 | Instantiating formula (31) with all_71_2_132, all_135_2_292, all_0_3_3, all_0_1_1 and discharging atoms vplus(all_0_1_1, all_0_3_3) = all_135_2_292, vplus(all_0_1_1, all_0_3_3) = all_71_2_132, yields: % 12.85/3.61 | (708) all_135_2_292 = all_71_2_132 % 12.85/3.61 | % 12.85/3.61 | Instantiating formula (31) with all_0_2_2, all_81_3_160, all_81_4_161, all_0_4_4 and discharging atoms vplus(all_0_4_4, all_81_4_161) = all_81_3_160, vplus(all_0_4_4, all_81_4_161) = all_0_2_2, yields: % 12.85/3.62 | (709) all_81_3_160 = all_0_2_2 % 12.85/3.62 | % 12.85/3.62 | Instantiating formula (31) with all_129_2_274, all_139_3_304, all_37_2_49, all_0_4_4 and discharging atoms vplus(all_0_4_4, all_37_2_49) = all_139_3_304, vplus(all_0_4_4, all_37_2_49) = all_129_2_274, yields: % 12.85/3.62 | (710) all_139_3_304 = all_129_2_274 % 12.85/3.62 | % 12.85/3.62 | Instantiating formula (31) with all_81_3_160, all_139_3_304, all_37_2_49, all_0_4_4 and discharging atoms vplus(all_0_4_4, all_37_2_49) = all_139_3_304, vplus(all_0_4_4, all_37_2_49) = all_81_3_160, yields: % 12.85/3.62 | (711) all_139_3_304 = all_81_3_160 % 12.85/3.62 | % 12.85/3.62 | Combining equations (711,710) yields a new equation: % 12.85/3.62 | (712) all_129_2_274 = all_81_3_160 % 12.85/3.62 | % 12.85/3.62 | Combining equations (708,707) yields a new equation: % 12.85/3.62 | (713) all_129_2_274 = all_71_2_132 % 12.85/3.62 | % 12.85/3.62 | Combining equations (706,707) yields a new equation: % 12.85/3.62 | (714) all_129_2_274 = all_0_0_0 % 12.85/3.62 | % 12.85/3.62 | Combining equations (712,713) yields a new equation: % 12.85/3.62 | (715) all_81_3_160 = all_71_2_132 % 12.85/3.62 | % 12.85/3.62 | Simplifying 715 yields: % 12.85/3.62 | (716) all_81_3_160 = all_71_2_132 % 12.85/3.62 | % 12.85/3.62 | Combining equations (714,713) yields a new equation: % 12.85/3.62 | (717) all_71_2_132 = all_0_0_0 % 12.85/3.62 | % 12.85/3.62 | Combining equations (709,716) yields a new equation: % 12.85/3.62 | (718) all_71_2_132 = all_0_2_2 % 12.85/3.62 | % 12.85/3.62 | Combining equations (718,717) yields a new equation: % 12.85/3.62 | (719) all_0_0_0 = all_0_2_2 % 12.85/3.62 | % 12.85/3.62 | Equations (719) can reduce 85 to: % 12.85/3.62 | (569) $false % 12.85/3.62 | % 12.85/3.62 |-The branch is then unsatisfiable % 12.85/3.62 % SZS output end Proof for theBenchmark % 12.85/3.62 % 12.85/3.62 3028ms %------------------------------------------------------------------------------