%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : ALG118+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n025.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 : Thu Jul 14 15:35:13 EDT 2022 % Result : Theorem 6.55s 2.03s % Output : Proof 12.02s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.07 % Problem : ALG118+1 : TPTP v8.1.0. Released v2.7.0. % 0.00/0.07 % Command : ePrincess-casc -timeout=%d %s % 0.06/0.26 % Computer : n025.cluster.edu % 0.06/0.26 % Model : x86_64 x86_64 % 0.06/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.26 % Memory : 8042.1875MB % 0.06/0.26 % OS : Linux 3.10.0-693.el7.x86_64 % 0.06/0.26 % CPULimit : 300 % 0.06/0.26 % WCLimit : 600 % 0.06/0.26 % DateTime : Wed Jun 8 08:14:04 EDT 2022 % 0.06/0.26 % CPUTime : % 0.10/0.50 ____ _ % 0.10/0.50 ___ / __ \_____(_)___ ________ __________ % 0.10/0.50 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.10/0.50 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.10/0.50 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.10/0.50 % 0.10/0.50 A Theorem Prover for First-Order Logic % 0.10/0.50 (ePrincess v.1.0) % 0.10/0.50 % 0.10/0.50 (c) Philipp Rümmer, 2009-2015 % 0.10/0.50 (c) Peter Backeman, 2014-2015 % 0.10/0.50 (contributions by Angelo Brillout, Peter Baumgartner) % 0.10/0.50 Free software under GNU Lesser General Public License (LGPL). % 0.10/0.50 Bug reports to peter@backeman.se % 0.10/0.50 % 0.10/0.50 For more information, visit http://user.uu.se/~petba168/breu/ % 0.10/0.50 % 0.10/0.50 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.63/0.55 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 3.12/1.23 Prover 0: Preprocessing ... % 5.57/1.79 Prover 0: Constructing countermodel ... % 6.55/2.03 Prover 0: proved (1475ms) % 6.55/2.03 % 6.55/2.03 No countermodel exists, formula is valid % 6.55/2.03 % SZS status Theorem for theBenchmark % 6.55/2.03 % 6.55/2.03 Generating proof ... found it (size 487) % 11.06/3.03 % 11.06/3.03 % SZS output start Proof for theBenchmark % 11.06/3.04 Assumed formulas after preprocessing and simplification: % 11.06/3.04 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : ? [v19] : ? [v20] : ? [v21] : ? [v22] : ? [v23] : ? [v24] : ? [v25] : ? [v26] : ? [v27] : ? [v28] : ? [v29] : ? [v30] : ? [v31] : ? [v32] : ? [v33] : ? [v34] : ? [v35] : ? [v36] : ? [v37] : ? [v38] : ? [v39] : ? [v40] : ? [v41] : ? [v42] : ? [v43] : ? [v44] : ? [v45] : ? [v46] : ? [v47] : ? [v48] : ? [v49] : ? [v50] : ? [v51] : ? [v52] : ? [v53] : ? [v54] : ? [v55] : ? [v56] : ? [v57] : ? [v58] : ? [v59] : ? [v60] : ? [v61] : ? [v62] : ? [v63] : ? [v64] : ? [v65] : ? [v66] : ? [v67] : ? [v68] : ? [v69] : ? [v70] : ? [v71] : ? [v72] : ? [v73] : ? [v74] : ? [v75] : ? [v76] : ? [v77] : ? [v78] : ? [v79] : ? [v80] : ? [v81] : ? [v82] : ? [v83] : ? [v84] : ? [v85] : ? [v86] : ? [v87] : ? [v88] : ? [v89] : ? [v90] : ? [v91] : ? [v92] : ? [v93] : ? [v94] : ? [v95] : ? [v96] : ? [v97] : ? [v98] : ? [v99] : ? [v100] : ? [v101] : ? [v102] : ? [v103] : ? [v104] : ? [v105] : ? [v106] : ? [v107] : ? [v108] : ? [v109] : ? [v110] : ? [v111] : ? [v112] : ? [v113] : ? [v114] : ? [v115] : ? [v116] : ? [v117] : ? [v118] : ? [v119] : ? [v120] : ? [v121] : ? [v122] : ? [v123] : ? [v124] : ? [v125] : ? [v126] : ? [v127] : ? [v128] : ? [v129] : ? [v130] : ? [v131] : ? [v132] : ? [v133] : ? [v134] : ? [v135] : ? [v136] : ? [v137] : ? [v138] : ( ~ (v21 = v20) & ~ (v21 = v19) & ~ (v21 = v16) & ~ (v21 = v13) & ~ (v21 = e22) & ~ (v21 = e21) & ~ (v20 = v18) & ~ (v20 = v15) & ~ (v20 = v12) & ~ (v20 = e22) & ~ (v20 = e21) & ~ (v19 = v18) & ~ (v19 = v17) & ~ (v19 = v16) & ~ (v19 = v13) & ~ (v19 = e22) & ~ (v18 = v17) & ~ (v18 = v15) & ~ (v18 = v12) & ~ (v18 = e22) & ~ (v17 = v14) & ~ (v17 = v11) & ~ (v17 = e22) & ~ (v16 = v15) & ~ (v16 = v14) & ~ (v16 = v13) & ~ (v16 = e20) & ~ (v15 = v14) & ~ (v15 = v12) & ~ (v15 = e20) & ~ (v14 = v11) & ~ (v14 = e22) & ~ (v14 = e20) & ~ (v13 = v12) & ~ (v13 = v11) & ~ (v13 = e23) & ~ (v12 = v11) & ~ (v12 = e23) & ~ (v11 = e23) & ~ (v11 = e22) & ~ (v10 = v9) & ~ (v10 = v8) & ~ (v10 = v5) & ~ (v10 = v2) & ~ (v10 = e12) & ~ (v10 = e11) & ~ (v9 = v7) & ~ (v9 = v4) & ~ (v9 = v1) & ~ (v9 = e12) & ~ (v9 = e11) & ~ (v8 = v7) & ~ (v8 = v6) & ~ (v8 = v5) & ~ (v8 = v2) & ~ (v8 = e12) & ~ (v7 = v6) & ~ (v7 = v4) & ~ (v7 = v1) & ~ (v7 = e12) & ~ (v6 = v3) & ~ (v6 = v0) & ~ (v6 = e12) & ~ (v5 = v4) & ~ (v5 = v3) & ~ (v5 = v2) & ~ (v5 = e10) & ~ (v4 = v3) & ~ (v4 = v1) & ~ (v4 = e10) & ~ (v3 = v0) & ~ (v3 = e12) & ~ (v3 = e10) & ~ (v2 = v1) & ~ (v2 = v0) & ~ (v2 = e13) & ~ (v1 = v0) & ~ (v1 = e13) & ~ (v0 = e13) & ~ (v0 = e12) & ~ (e23 = e22) & ~ (e23 = e21) & ~ (e23 = e20) & ~ (e23 = e13) & ~ (e23 = e12) & ~ (e23 = e11) & ~ (e23 = e10) & ~ (e22 = e21) & ~ (e22 = e20) & ~ (e22 = e13) & ~ (e22 = e12) & ~ (e22 = e11) & ~ (e22 = e10) & ~ (e21 = e20) & ~ (e21 = e13) & ~ (e21 = e12) & ~ (e21 = e11) & ~ (e21 = e10) & ~ (e20 = e13) & ~ (e20 = e12) & ~ (e20 = e11) & ~ (e20 = e10) & ~ (e13 = e12) & ~ (e13 = e11) & ~ (e13 = e10) & ~ (e12 = e11) & ~ (e12 = e10) & ~ (e11 = e10) & op1(e13, v10) = v32 & op1(e13, v9) = v31 & op1(e13, e13) = v10 & op1(e13, e12) = v9 & op1(e13, e11) = e11 & op1(e13, e10) = e12 & op1(e12, v8) = v30 & op1(e12, v7) = v29 & op1(e12, v6) = v28 & op1(e12, e13) = v8 & op1(e12, e12) = v7 & op1(e12, e11) = e12 & op1(e12, e10) = v6 & op1(e11, v5) = v27 & op1(e11, v4) = v26 & op1(e11, v3) = v25 & op1(e11, e13) = v5 & op1(e11, e12) = v4 & op1(e11, e11) = e10 & op1(e11, e10) = v3 & op1(e10, v2) = v24 & op1(e10, v1) = v23 & op1(e10, v0) = v22 & op1(e10, e13) = v2 & op1(e10, e12) = v1 & op1(e10, e11) = e13 & op1(e10, e10) = v0 & h1(v10) = v74 & h1(v9) = v72 & h1(v8) = v68 & h1(v7) = v66 & h1(v6) = v63 & h1(v5) = v61 & h1(v4) = v59 & h1(v3) = v57 & h1(v2) = v55 & h1(v1) = v53 & h1(v0) = v50 & h1(e13) = v45 & h1(e12) = v44 & h1(e11) = e20 & h1(e10) = v11 & h2(v10) = v86 & h2(v9) = v85 & h2(v8) = v84 & h2(v7) = v83 & h2(v6) = v82 & h2(v5) = v81 & h2(v4) = v80 & h2(v3) = v79 & h2(v2) = v78 & h2(v1) = v77 & h2(v0) = v76 & h2(e13) = e23 & h2(e12) = e22 & h2(e11) = e21 & h2(e10) = e20 & h3(v10) = v111 & h3(v9) = v109 & h3(v8) = v105 & h3(v7) = v103 & h3(v6) = v100 & h3(v5) = v98 & h3(v4) = v96 & h3(v3) = v94 & h3(v2) = v92 & h3(v1) = v90 & h3(v0) = v87 & h3(e13) = v47 & h3(e12) = v46 & h3(e11) = e22 & h3(e10) = v18 & h4(v10) = v137 & h4(v9) = v135 & h4(v8) = v131 & h4(v7) = v129 & h4(v6) = v126 & h4(v5) = v124 & h4(v4) = v122 & h4(v3) = v120 & h4(v2) = v118 & h4(v1) = v116 & h4(v0) = v113 & h4(e13) = v49 & h4(e12) = v48 & h4(e11) = e23 & h4(e10) = v21 & op2(v49, v49) = v138 & op2(v49, v48) = v136 & op2(v49, v21) = v133 & op2(v49, v21) = v48 & op2(v49, e23) = v134 & op2(v48, v49) = v132 & op2(v48, v48) = v130 & op2(v48, v21) = v127 & op2(v48, e23) = v128 & op2(v47, v47) = v112 & op2(v47, v46) = v110 & op2(v47, v18) = v107 & op2(v47, v18) = v46 & op2(v47, e22) = v108 & op2(v46, v47) = v106 & op2(v46, v46) = v104 & op2(v46, v18) = v101 & op2(v46, e22) = v102 & op2(v45, v45) = v75 & op2(v45, v44) = v73 & op2(v45, v11) = v70 & op2(v45, v11) = v44 & op2(v45, e20) = v71 & op2(v44, v45) = v69 & op2(v44, v44) = v67 & op2(v44, v11) = v64 & op2(v44, e20) = v65 & op2(v21, v49) = v119 & op2(v21, v48) = v117 & op2(v21, v21) = v114 & op2(v21, e23) = v115 & op2(v21, e23) = v49 & op2(v18, v47) = v93 & op2(v18, v46) = v91 & op2(v18, v18) = v88 & op2(v18, e22) = v89 & op2(v18, e22) = v47 & op2(v11, v45) = v56 & op2(v11, v44) = v54 & op2(v11, v11) = v51 & op2(v11, e20) = v52 & op2(v11, e20) = v45 & op2(e23, v49) = v125 & op2(e23, v48) = v123 & op2(e23, v21) = v121 & op2(e23, v21) = v43 & op2(e23, v20) = v42 & op2(e23, e23) = v21 & op2(e23, e22) = v20 & op2(e23, e21) = e21 & op2(e23, e20) = e22 & op2(e22, v47) = v99 & op2(e22, v46) = v97 & op2(e22, v19) = v41 & op2(e22, v18) = v95 & op2(e22, v18) = v40 & op2(e22, v17) = v39 & op2(e22, e23) = v19 & op2(e22, e22) = v18 & op2(e22, e21) = e22 & op2(e22, e20) = v17 & op2(e21, v16) = v38 & op2(e21, v15) = v37 & op2(e21, v14) = v36 & op2(e21, e23) = v16 & op2(e21, e22) = v15 & op2(e21, e21) = e20 & op2(e21, e20) = v14 & op2(e20, v45) = v62 & op2(e20, v44) = v60 & op2(e20, v13) = v35 & op2(e20, v12) = v34 & op2(e20, v11) = v58 & op2(e20, v11) = v33 & op2(e20, e23) = v13 & op2(e20, e22) = v12 & op2(e20, e21) = e23 & op2(e20, e20) = v11 & ! [v139] : ! [v140] : ! [v141] : ! [v142] : (v140 = v139 | ~ (op1(v142, v141) = v140) | ~ (op1(v142, v141) = v139)) & ! [v139] : ! [v140] : ! [v141] : ! [v142] : (v140 = v139 | ~ (op2(v142, v141) = v140) | ~ (op2(v142, v141) = v139)) & ! [v139] : ! [v140] : ! [v141] : (v140 = v139 | ~ (h1(v141) = v140) | ~ (h1(v141) = v139)) & ! [v139] : ! [v140] : ! [v141] : (v140 = v139 | ~ (h2(v141) = v140) | ~ (h2(v141) = v139)) & ! [v139] : ! [v140] : ! [v141] : (v140 = v139 | ~ (h3(v141) = v140) | ~ (h3(v141) = v139)) & ! [v139] : ! [v140] : ! [v141] : (v140 = v139 | ~ (h4(v141) = v140) | ~ (h4(v141) = v139)) & ( ~ (v138 = v137) | ~ (v136 = v135) | ~ (v134 = e23) | ~ (v133 = v48) | ~ (v132 = v131) | ~ (v130 = v129) | ~ (v128 = v48) | ~ (v127 = v126) | ~ (v125 = v124) | ~ (v123 = v122) | ~ (v121 = v120) | ~ (v119 = v118) | ~ (v117 = v116) | ~ (v115 = v49) | ~ (v114 = v113) | ( ~ (v49 = e22) & ~ (v48 = e22)) | ( ~ (v49 = e21) & ~ (v48 = e21)) | ( ~ (v49 = e20) & ~ (v48 = e20) & ~ (v21 = e20))) & ( ~ (v112 = v111) | ~ (v110 = v109) | ~ (v108 = e22) | ~ (v107 = v46) | ~ (v106 = v105) | ~ (v104 = v103) | ~ (v102 = v46) | ~ (v101 = v100) | ~ (v99 = v98) | ~ (v97 = v96) | ~ (v95 = v94) | ~ (v93 = v92) | ~ (v91 = v90) | ~ (v89 = v47) | ~ (v88 = v87) | ( ~ (v47 = e23) & ~ (v46 = e23) & ~ (v18 = e23)) | ( ~ (v47 = e21) & ~ (v46 = e21) & ~ (v18 = e21)) | ( ~ (v47 = e20) & ~ (v46 = e20) & ~ (v18 = e20))) & ( ~ (v86 = v21) | ~ (v85 = v20) | ~ (v84 = v19) | ~ (v83 = v18) | ~ (v82 = v17) | ~ (v81 = v16) | ~ (v80 = v15) | ~ (v79 = v14) | ~ (v78 = v13) | ~ (v77 = v12) | ~ (v76 = v11)) & ( ~ (v75 = v74) | ~ (v73 = v72) | ~ (v71 = e20) | ~ (v70 = v44) | ~ (v69 = v68) | ~ (v67 = v66) | ~ (v65 = v44) | ~ (v64 = v63) | ~ (v62 = v61) | ~ (v60 = v59) | ~ (v58 = v57) | ~ (v56 = v55) | ~ (v54 = v53) | ~ (v52 = v45) | ~ (v51 = v50) | ( ~ (v45 = e23) & ~ (v44 = e23)) | ( ~ (v45 = e22) & ~ (v44 = e22)) | ( ~ (v45 = e21) & ~ (v44 = e21) & ~ (v11 = e21))) & (v21 = e23 | v21 = e20) & (v21 = e23 | v20 = e23) & (v21 = e23 | v19 = e23 | v16 = e23) & (v21 = e23 | v16 = e21 | v13 = e20) & (v21 = e23 | v11 = e20 | (v20 = e23 & v19 = e23 & v16 = e21) | (v20 = e23 & v19 = e23 & v15 = e22) | (v17 = e20 & v15 = e22 & v12 = e20) | (v16 = e21 & v15 = e22)) & (v21 = e20 | v20 = e20) & (v21 = e20 | v19 = e20 | v13 = e20) & (v20 = e23 | v20 = e20) & (v20 = e23 | v18 = e23 | v15 = e23) & (v20 = e23 | v15 = e21 | v12 = e20) & (v20 = e20 | v18 = e20 | v12 = e20) & (v19 = e23 | v19 = e21 | v19 = e20) & (v19 = e23 | v18 = e23 | v17 = e23) & (v19 = e21 | v18 = e21 | v17 = e21) & (v19 = e21 | v16 = e21 | v13 = e21) & (v19 = e20 | v18 = e20 | v17 = e20) & (v18 = e23 | v18 = e21 | v18 = e20) & (v18 = e21 | v15 = e21 | v12 = e21) & (v17 = e23 | v17 = e21 | v17 = e20) & (v17 = e23 | v14 = e23) & (v17 = e21 | v14 = e21 | v11 = e21) & (v17 = e20 | v11 = e20) & (v16 = e23 | v16 = e22 | v16 = e21) & (v16 = e23 | v15 = e23 | v14 = e23) & (v16 = e22 | v15 = e22) & (v16 = e22 | v13 = e22) & (v16 = e21 | v15 = e21 | v14 = e21) & (v15 = e23 | v15 = e22 | v15 = e21) & (v15 = e22 | v12 = e22) & (v14 = e23 | v14 = e21) & (v14 = e21 | v11 = e20) & (v13 = e22 | v13 = e21 | v13 = e20) & (v13 = e22 | v12 = e22) & (v13 = e21 | v12 = e21 | v11 = e21) & (v13 = e20 | v12 = e20 | v11 = e20) & (v12 = e22 | v12 = e21 | v12 = e20) & (v11 = e21 | v11 = e20) & (v10 = e13 | v10 = e10) & (v10 = e13 | v9 = e13) & (v10 = e13 | v8 = e13 | v5 = e13) & (v10 = e13 | v5 = e11 | v2 = e10) & (v10 = e13 | v0 = e10 | (v9 = e13 & v8 = e13 & v5 = e11) | (v9 = e13 & v8 = e13 & v4 = e12) | (v6 = e10 & v4 = e12 & v1 = e10) | (v5 = e11 & v4 = e12)) & (v10 = e10 | v9 = e10) & (v10 = e10 | v8 = e10 | v2 = e10) & (v9 = e13 | v9 = e10) & (v9 = e13 | v7 = e13 | v4 = e13) & (v9 = e13 | v4 = e11 | v1 = e10) & (v9 = e10 | v7 = e10 | v1 = e10) & (v8 = e13 | v8 = e11 | v8 = e10) & (v8 = e13 | v7 = e13 | v6 = e13) & (v8 = e11 | v7 = e11 | v6 = e11) & (v8 = e11 | v5 = e11 | v2 = e11) & (v8 = e10 | v7 = e10 | v6 = e10) & (v7 = e13 | v7 = e11 | v7 = e10) & (v7 = e11 | v4 = e11 | v1 = e11) & (v6 = e13 | v6 = e11 | v6 = e10) & (v6 = e13 | v3 = e13) & (v6 = e11 | v3 = e11 | v0 = e11) & (v6 = e10 | v0 = e10) & (v5 = e13 | v5 = e12 | v5 = e11) & (v5 = e13 | v4 = e13 | v3 = e13) & (v5 = e12 | v4 = e12) & (v5 = e12 | v2 = e12) & (v5 = e11 | v4 = e11 | v3 = e11) & (v4 = e13 | v4 = e12 | v4 = e11) & (v4 = e12 | v1 = e12) & (v3 = e13 | v3 = e11) & (v3 = e11 | v0 = e10) & (v2 = e12 | v2 = e11 | v2 = e10) & (v2 = e12 | v1 = e12) & (v2 = e11 | v1 = e11 | v0 = e11) & (v2 = e10 | v1 = e10 | v0 = e10) & (v1 = e12 | v1 = e11 | v1 = e10) & (v0 = e11 | v0 = e10) & (( ~ (v41 = e23) & ~ (v40 = e22) & ~ (v39 = e20) & ~ (v18 = e21)) | ( ~ (v38 = e23) & ~ (v37 = e22) & ~ (v36 = e20) & ~ (v14 = e21)) | ( ~ (v35 = e23) & ~ (v34 = e22) & ~ (v33 = e20) & ~ (v13 = e21))) & (( ~ (v30 = e13) & ~ (v29 = e12) & ~ (v28 = e10) & ~ (v7 = e11)) | ( ~ (v27 = e13) & ~ (v26 = e12) & ~ (v25 = e10) & ~ (v3 = e11)) | ( ~ (v24 = e13) & ~ (v23 = e12) & ~ (v22 = e10) & ~ (v2 = e11)))) % 11.39/3.11 | 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, all_0_9_9, all_0_10_10, all_0_11_11, all_0_12_12, all_0_13_13, all_0_14_14, all_0_15_15, all_0_16_16, all_0_17_17, all_0_18_18, all_0_19_19, all_0_20_20, all_0_21_21, all_0_22_22, all_0_23_23, all_0_24_24, all_0_25_25, all_0_26_26, all_0_27_27, all_0_28_28, all_0_29_29, all_0_30_30, all_0_31_31, all_0_32_32, all_0_33_33, all_0_34_34, all_0_35_35, all_0_36_36, all_0_37_37, all_0_38_38, all_0_39_39, all_0_40_40, all_0_41_41, all_0_42_42, all_0_43_43, all_0_44_44, all_0_45_45, all_0_46_46, all_0_47_47, all_0_48_48, all_0_49_49, all_0_50_50, all_0_51_51, all_0_52_52, all_0_53_53, all_0_54_54, all_0_55_55, all_0_56_56, all_0_57_57, all_0_58_58, all_0_59_59, all_0_60_60, all_0_61_61, all_0_62_62, all_0_63_63, all_0_64_64, all_0_65_65, all_0_66_66, all_0_67_67, all_0_68_68, all_0_69_69, all_0_70_70, all_0_71_71, all_0_72_72, all_0_73_73, all_0_74_74, all_0_75_75, all_0_76_76, all_0_77_77, all_0_78_78, all_0_79_79, all_0_80_80, all_0_81_81, all_0_82_82, all_0_83_83, all_0_84_84, all_0_85_85, all_0_86_86, all_0_87_87, all_0_88_88, all_0_89_89, all_0_90_90, all_0_91_91, all_0_92_92, all_0_93_93, all_0_94_94, all_0_95_95, all_0_96_96, all_0_97_97, all_0_98_98, all_0_99_99, all_0_100_100, all_0_101_101, all_0_102_102, all_0_103_103, all_0_104_104, all_0_105_105, all_0_106_106, all_0_107_107, all_0_108_108, all_0_109_109, all_0_110_110, all_0_111_111, all_0_112_112, all_0_113_113, all_0_114_114, all_0_115_115, all_0_116_116, all_0_117_117, all_0_118_118, all_0_119_119, all_0_120_120, all_0_121_121, all_0_122_122, all_0_123_123, all_0_124_124, all_0_125_125, all_0_126_126, all_0_127_127, all_0_128_128, all_0_129_129, all_0_130_130, all_0_131_131, all_0_132_132, all_0_133_133, all_0_134_134, all_0_135_135, all_0_136_136, all_0_137_137, all_0_138_138 yields: % 11.39/3.11 | (1) ~ (all_0_117_117 = all_0_118_118) & ~ (all_0_117_117 = all_0_119_119) & ~ (all_0_117_117 = all_0_122_122) & ~ (all_0_117_117 = all_0_125_125) & ~ (all_0_117_117 = e22) & ~ (all_0_117_117 = e21) & ~ (all_0_118_118 = all_0_120_120) & ~ (all_0_118_118 = all_0_123_123) & ~ (all_0_118_118 = all_0_126_126) & ~ (all_0_118_118 = e22) & ~ (all_0_118_118 = e21) & ~ (all_0_119_119 = all_0_120_120) & ~ (all_0_119_119 = all_0_121_121) & ~ (all_0_119_119 = all_0_122_122) & ~ (all_0_119_119 = all_0_125_125) & ~ (all_0_119_119 = e22) & ~ (all_0_120_120 = all_0_121_121) & ~ (all_0_120_120 = all_0_123_123) & ~ (all_0_120_120 = all_0_126_126) & ~ (all_0_120_120 = e22) & ~ (all_0_121_121 = all_0_124_124) & ~ (all_0_121_121 = all_0_127_127) & ~ (all_0_121_121 = e22) & ~ (all_0_122_122 = all_0_123_123) & ~ (all_0_122_122 = all_0_124_124) & ~ (all_0_122_122 = all_0_125_125) & ~ (all_0_122_122 = e20) & ~ (all_0_123_123 = all_0_124_124) & ~ (all_0_123_123 = all_0_126_126) & ~ (all_0_123_123 = e20) & ~ (all_0_124_124 = all_0_127_127) & ~ (all_0_124_124 = e22) & ~ (all_0_124_124 = e20) & ~ (all_0_125_125 = all_0_126_126) & ~ (all_0_125_125 = all_0_127_127) & ~ (all_0_125_125 = e23) & ~ (all_0_126_126 = all_0_127_127) & ~ (all_0_126_126 = e23) & ~ (all_0_127_127 = e23) & ~ (all_0_127_127 = e22) & ~ (all_0_128_128 = all_0_129_129) & ~ (all_0_128_128 = all_0_130_130) & ~ (all_0_128_128 = all_0_133_133) & ~ (all_0_128_128 = all_0_136_136) & ~ (all_0_128_128 = e12) & ~ (all_0_128_128 = e11) & ~ (all_0_129_129 = all_0_131_131) & ~ (all_0_129_129 = all_0_134_134) & ~ (all_0_129_129 = all_0_137_137) & ~ (all_0_129_129 = e12) & ~ (all_0_129_129 = e11) & ~ (all_0_130_130 = all_0_131_131) & ~ (all_0_130_130 = all_0_132_132) & ~ (all_0_130_130 = all_0_133_133) & ~ (all_0_130_130 = all_0_136_136) & ~ (all_0_130_130 = e12) & ~ (all_0_131_131 = all_0_132_132) & ~ (all_0_131_131 = all_0_134_134) & ~ (all_0_131_131 = all_0_137_137) & ~ (all_0_131_131 = e12) & ~ (all_0_132_132 = all_0_135_135) & ~ (all_0_132_132 = all_0_138_138) & ~ (all_0_132_132 = e12) & ~ (all_0_133_133 = all_0_134_134) & ~ (all_0_133_133 = all_0_135_135) & ~ (all_0_133_133 = all_0_136_136) & ~ (all_0_133_133 = e10) & ~ (all_0_134_134 = all_0_135_135) & ~ (all_0_134_134 = all_0_137_137) & ~ (all_0_134_134 = e10) & ~ (all_0_135_135 = all_0_138_138) & ~ (all_0_135_135 = e12) & ~ (all_0_135_135 = e10) & ~ (all_0_136_136 = all_0_137_137) & ~ (all_0_136_136 = all_0_138_138) & ~ (all_0_136_136 = e13) & ~ (all_0_137_137 = all_0_138_138) & ~ (all_0_137_137 = e13) & ~ (all_0_138_138 = e13) & ~ (all_0_138_138 = e12) & ~ (e23 = e22) & ~ (e23 = e21) & ~ (e23 = e20) & ~ (e23 = e13) & ~ (e23 = e12) & ~ (e23 = e11) & ~ (e23 = e10) & ~ (e22 = e21) & ~ (e22 = e20) & ~ (e22 = e13) & ~ (e22 = e12) & ~ (e22 = e11) & ~ (e22 = e10) & ~ (e21 = e20) & ~ (e21 = e13) & ~ (e21 = e12) & ~ (e21 = e11) & ~ (e21 = e10) & ~ (e20 = e13) & ~ (e20 = e12) & ~ (e20 = e11) & ~ (e20 = e10) & ~ (e13 = e12) & ~ (e13 = e11) & ~ (e13 = e10) & ~ (e12 = e11) & ~ (e12 = e10) & ~ (e11 = e10) & op1(e13, all_0_128_128) = all_0_106_106 & op1(e13, all_0_129_129) = all_0_107_107 & op1(e13, e13) = all_0_128_128 & op1(e13, e12) = all_0_129_129 & op1(e13, e11) = e11 & op1(e13, e10) = e12 & op1(e12, all_0_130_130) = all_0_108_108 & op1(e12, all_0_131_131) = all_0_109_109 & op1(e12, all_0_132_132) = all_0_110_110 & op1(e12, e13) = all_0_130_130 & op1(e12, e12) = all_0_131_131 & op1(e12, e11) = e12 & op1(e12, e10) = all_0_132_132 & op1(e11, all_0_133_133) = all_0_111_111 & op1(e11, all_0_134_134) = all_0_112_112 & op1(e11, all_0_135_135) = all_0_113_113 & op1(e11, e13) = all_0_133_133 & op1(e11, e12) = all_0_134_134 & op1(e11, e11) = e10 & op1(e11, e10) = all_0_135_135 & op1(e10, all_0_136_136) = all_0_114_114 & op1(e10, all_0_137_137) = all_0_115_115 & op1(e10, all_0_138_138) = all_0_116_116 & op1(e10, e13) = all_0_136_136 & op1(e10, e12) = all_0_137_137 & op1(e10, e11) = e13 & op1(e10, e10) = all_0_138_138 & h1(all_0_128_128) = all_0_64_64 & h1(all_0_129_129) = all_0_66_66 & h1(all_0_130_130) = all_0_70_70 & h1(all_0_131_131) = all_0_72_72 & h1(all_0_132_132) = all_0_75_75 & h1(all_0_133_133) = all_0_77_77 & h1(all_0_134_134) = all_0_79_79 & h1(all_0_135_135) = all_0_81_81 & h1(all_0_136_136) = all_0_83_83 & h1(all_0_137_137) = all_0_85_85 & h1(all_0_138_138) = all_0_88_88 & h1(e13) = all_0_93_93 & h1(e12) = all_0_94_94 & h1(e11) = e20 & h1(e10) = all_0_127_127 & h2(all_0_128_128) = all_0_52_52 & h2(all_0_129_129) = all_0_53_53 & h2(all_0_130_130) = all_0_54_54 & h2(all_0_131_131) = all_0_55_55 & h2(all_0_132_132) = all_0_56_56 & h2(all_0_133_133) = all_0_57_57 & h2(all_0_134_134) = all_0_58_58 & h2(all_0_135_135) = all_0_59_59 & h2(all_0_136_136) = all_0_60_60 & h2(all_0_137_137) = all_0_61_61 & h2(all_0_138_138) = all_0_62_62 & h2(e13) = e23 & h2(e12) = e22 & h2(e11) = e21 & h2(e10) = e20 & h3(all_0_128_128) = all_0_27_27 & h3(all_0_129_129) = all_0_29_29 & h3(all_0_130_130) = all_0_33_33 & h3(all_0_131_131) = all_0_35_35 & h3(all_0_132_132) = all_0_38_38 & h3(all_0_133_133) = all_0_40_40 & h3(all_0_134_134) = all_0_42_42 & h3(all_0_135_135) = all_0_44_44 & h3(all_0_136_136) = all_0_46_46 & h3(all_0_137_137) = all_0_48_48 & h3(all_0_138_138) = all_0_51_51 & h3(e13) = all_0_91_91 & h3(e12) = all_0_92_92 & h3(e11) = e22 & h3(e10) = all_0_120_120 & h4(all_0_128_128) = all_0_1_1 & h4(all_0_129_129) = all_0_3_3 & h4(all_0_130_130) = all_0_7_7 & h4(all_0_131_131) = all_0_9_9 & h4(all_0_132_132) = all_0_12_12 & h4(all_0_133_133) = all_0_14_14 & h4(all_0_134_134) = all_0_16_16 & h4(all_0_135_135) = all_0_18_18 & h4(all_0_136_136) = all_0_20_20 & h4(all_0_137_137) = all_0_22_22 & h4(all_0_138_138) = all_0_25_25 & h4(e13) = all_0_89_89 & h4(e12) = all_0_90_90 & h4(e11) = e23 & h4(e10) = all_0_117_117 & op2(all_0_89_89, all_0_89_89) = all_0_0_0 & op2(all_0_89_89, all_0_90_90) = all_0_2_2 & op2(all_0_89_89, all_0_117_117) = all_0_5_5 & op2(all_0_89_89, all_0_117_117) = all_0_90_90 & op2(all_0_89_89, e23) = all_0_4_4 & op2(all_0_90_90, all_0_89_89) = all_0_6_6 & op2(all_0_90_90, all_0_90_90) = all_0_8_8 & op2(all_0_90_90, all_0_117_117) = all_0_11_11 & op2(all_0_90_90, e23) = all_0_10_10 & op2(all_0_91_91, all_0_91_91) = all_0_26_26 & op2(all_0_91_91, all_0_92_92) = all_0_28_28 & op2(all_0_91_91, all_0_120_120) = all_0_31_31 & op2(all_0_91_91, all_0_120_120) = all_0_92_92 & op2(all_0_91_91, e22) = all_0_30_30 & op2(all_0_92_92, all_0_91_91) = all_0_32_32 & op2(all_0_92_92, all_0_92_92) = all_0_34_34 & op2(all_0_92_92, all_0_120_120) = all_0_37_37 & op2(all_0_92_92, e22) = all_0_36_36 & op2(all_0_93_93, all_0_93_93) = all_0_63_63 & op2(all_0_93_93, all_0_94_94) = all_0_65_65 & op2(all_0_93_93, all_0_127_127) = all_0_68_68 & op2(all_0_93_93, all_0_127_127) = all_0_94_94 & op2(all_0_93_93, e20) = all_0_67_67 & op2(all_0_94_94, all_0_93_93) = all_0_69_69 & op2(all_0_94_94, all_0_94_94) = all_0_71_71 & op2(all_0_94_94, all_0_127_127) = all_0_74_74 & op2(all_0_94_94, e20) = all_0_73_73 & op2(all_0_117_117, all_0_89_89) = all_0_19_19 & op2(all_0_117_117, all_0_90_90) = all_0_21_21 & op2(all_0_117_117, all_0_117_117) = all_0_24_24 & op2(all_0_117_117, e23) = all_0_23_23 & op2(all_0_117_117, e23) = all_0_89_89 & op2(all_0_120_120, all_0_91_91) = all_0_45_45 & op2(all_0_120_120, all_0_92_92) = all_0_47_47 & op2(all_0_120_120, all_0_120_120) = all_0_50_50 & op2(all_0_120_120, e22) = all_0_49_49 & op2(all_0_120_120, e22) = all_0_91_91 & op2(all_0_127_127, all_0_93_93) = all_0_82_82 & op2(all_0_127_127, all_0_94_94) = all_0_84_84 & op2(all_0_127_127, all_0_127_127) = all_0_87_87 & op2(all_0_127_127, e20) = all_0_86_86 & op2(all_0_127_127, e20) = all_0_93_93 & op2(e23, all_0_89_89) = all_0_13_13 & op2(e23, all_0_90_90) = all_0_15_15 & op2(e23, all_0_117_117) = all_0_17_17 & op2(e23, all_0_117_117) = all_0_95_95 & op2(e23, all_0_118_118) = all_0_96_96 & op2(e23, e23) = all_0_117_117 & op2(e23, e22) = all_0_118_118 & op2(e23, e21) = e21 & op2(e23, e20) = e22 & op2(e22, all_0_91_91) = all_0_39_39 & op2(e22, all_0_92_92) = all_0_41_41 & op2(e22, all_0_119_119) = all_0_97_97 & op2(e22, all_0_120_120) = all_0_43_43 & op2(e22, all_0_120_120) = all_0_98_98 & op2(e22, all_0_121_121) = all_0_99_99 & op2(e22, e23) = all_0_119_119 & op2(e22, e22) = all_0_120_120 & op2(e22, e21) = e22 & op2(e22, e20) = all_0_121_121 & op2(e21, all_0_122_122) = all_0_100_100 & op2(e21, all_0_123_123) = all_0_101_101 & op2(e21, all_0_124_124) = all_0_102_102 & op2(e21, e23) = all_0_122_122 & op2(e21, e22) = all_0_123_123 & op2(e21, e21) = e20 & op2(e21, e20) = all_0_124_124 & op2(e20, all_0_93_93) = all_0_76_76 & op2(e20, all_0_94_94) = all_0_78_78 & op2(e20, all_0_125_125) = all_0_103_103 & op2(e20, all_0_126_126) = all_0_104_104 & op2(e20, all_0_127_127) = all_0_80_80 & op2(e20, all_0_127_127) = all_0_105_105 & op2(e20, e23) = all_0_125_125 & op2(e20, e22) = all_0_126_126 & op2(e20, e21) = e23 & op2(e20, e20) = all_0_127_127 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op1(v3, v2) = v1) | ~ (op1(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op2(v3, v2) = v1) | ~ (op2(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h1(v2) = v1) | ~ (h1(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h2(v2) = v1) | ~ (h2(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h3(v2) = v1) | ~ (h3(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h4(v2) = v1) | ~ (h4(v2) = v0)) & ( ~ (all_0_0_0 = all_0_1_1) | ~ (all_0_2_2 = all_0_3_3) | ~ (all_0_4_4 = e23) | ~ (all_0_5_5 = all_0_90_90) | ~ (all_0_6_6 = all_0_7_7) | ~ (all_0_8_8 = all_0_9_9) | ~ (all_0_10_10 = all_0_90_90) | ~ (all_0_11_11 = all_0_12_12) | ~ (all_0_13_13 = all_0_14_14) | ~ (all_0_15_15 = all_0_16_16) | ~ (all_0_17_17 = all_0_18_18) | ~ (all_0_19_19 = all_0_20_20) | ~ (all_0_21_21 = all_0_22_22) | ~ (all_0_23_23 = all_0_89_89) | ~ (all_0_24_24 = all_0_25_25) | ( ~ (all_0_89_89 = e22) & ~ (all_0_90_90 = e22)) | ( ~ (all_0_89_89 = e21) & ~ (all_0_90_90 = e21)) | ( ~ (all_0_89_89 = e20) & ~ (all_0_90_90 = e20) & ~ (all_0_117_117 = e20))) & ( ~ (all_0_26_26 = all_0_27_27) | ~ (all_0_28_28 = all_0_29_29) | ~ (all_0_30_30 = e22) | ~ (all_0_31_31 = all_0_92_92) | ~ (all_0_32_32 = all_0_33_33) | ~ (all_0_34_34 = all_0_35_35) | ~ (all_0_36_36 = all_0_92_92) | ~ (all_0_37_37 = all_0_38_38) | ~ (all_0_39_39 = all_0_40_40) | ~ (all_0_41_41 = all_0_42_42) | ~ (all_0_43_43 = all_0_44_44) | ~ (all_0_45_45 = all_0_46_46) | ~ (all_0_47_47 = all_0_48_48) | ~ (all_0_49_49 = all_0_91_91) | ~ (all_0_50_50 = all_0_51_51) | ( ~ (all_0_91_91 = e23) & ~ (all_0_92_92 = e23) & ~ (all_0_120_120 = e23)) | ( ~ (all_0_91_91 = e21) & ~ (all_0_92_92 = e21) & ~ (all_0_120_120 = e21)) | ( ~ (all_0_91_91 = e20) & ~ (all_0_92_92 = e20) & ~ (all_0_120_120 = e20))) & ( ~ (all_0_52_52 = all_0_117_117) | ~ (all_0_53_53 = all_0_118_118) | ~ (all_0_54_54 = all_0_119_119) | ~ (all_0_55_55 = all_0_120_120) | ~ (all_0_56_56 = all_0_121_121) | ~ (all_0_57_57 = all_0_122_122) | ~ (all_0_58_58 = all_0_123_123) | ~ (all_0_59_59 = all_0_124_124) | ~ (all_0_60_60 = all_0_125_125) | ~ (all_0_61_61 = all_0_126_126) | ~ (all_0_62_62 = all_0_127_127)) & ( ~ (all_0_63_63 = all_0_64_64) | ~ (all_0_65_65 = all_0_66_66) | ~ (all_0_67_67 = e20) | ~ (all_0_68_68 = all_0_94_94) | ~ (all_0_69_69 = all_0_70_70) | ~ (all_0_71_71 = all_0_72_72) | ~ (all_0_73_73 = all_0_94_94) | ~ (all_0_74_74 = all_0_75_75) | ~ (all_0_76_76 = all_0_77_77) | ~ (all_0_78_78 = all_0_79_79) | ~ (all_0_80_80 = all_0_81_81) | ~ (all_0_82_82 = all_0_83_83) | ~ (all_0_84_84 = all_0_85_85) | ~ (all_0_86_86 = all_0_93_93) | ~ (all_0_87_87 = all_0_88_88) | ( ~ (all_0_93_93 = e23) & ~ (all_0_94_94 = e23)) | ( ~ (all_0_93_93 = e22) & ~ (all_0_94_94 = e22)) | ( ~ (all_0_93_93 = e21) & ~ (all_0_94_94 = e21) & ~ (all_0_127_127 = e21))) & (all_0_117_117 = e23 | all_0_117_117 = e20) & (all_0_117_117 = e23 | all_0_118_118 = e23) & (all_0_117_117 = e23 | all_0_119_119 = e23 | all_0_122_122 = e23) & (all_0_117_117 = e23 | all_0_122_122 = e21 | all_0_125_125 = e20) & (all_0_117_117 = e23 | all_0_127_127 = e20 | (all_0_118_118 = e23 & all_0_119_119 = e23 & all_0_122_122 = e21) | (all_0_118_118 = e23 & all_0_119_119 = e23 & all_0_123_123 = e22) | (all_0_121_121 = e20 & all_0_123_123 = e22 & all_0_126_126 = e20) | (all_0_122_122 = e21 & all_0_123_123 = e22)) & (all_0_117_117 = e20 | all_0_118_118 = e20) & (all_0_117_117 = e20 | all_0_119_119 = e20 | all_0_125_125 = e20) & (all_0_118_118 = e23 | all_0_118_118 = e20) & (all_0_118_118 = e23 | all_0_120_120 = e23 | all_0_123_123 = e23) & (all_0_118_118 = e23 | all_0_123_123 = e21 | all_0_126_126 = e20) & (all_0_118_118 = e20 | all_0_120_120 = e20 | all_0_126_126 = e20) & (all_0_119_119 = e23 | all_0_119_119 = e21 | all_0_119_119 = e20) & (all_0_119_119 = e23 | all_0_120_120 = e23 | all_0_121_121 = e23) & (all_0_119_119 = e21 | all_0_120_120 = e21 | all_0_121_121 = e21) & (all_0_119_119 = e21 | all_0_122_122 = e21 | all_0_125_125 = e21) & (all_0_119_119 = e20 | all_0_120_120 = e20 | all_0_121_121 = e20) & (all_0_120_120 = e23 | all_0_120_120 = e21 | all_0_120_120 = e20) & (all_0_120_120 = e21 | all_0_123_123 = e21 | all_0_126_126 = e21) & (all_0_121_121 = e23 | all_0_121_121 = e21 | all_0_121_121 = e20) & (all_0_121_121 = e23 | all_0_124_124 = e23) & (all_0_121_121 = e21 | all_0_124_124 = e21 | all_0_127_127 = e21) & (all_0_121_121 = e20 | all_0_127_127 = e20) & (all_0_122_122 = e23 | all_0_122_122 = e22 | all_0_122_122 = e21) & (all_0_122_122 = e23 | all_0_123_123 = e23 | all_0_124_124 = e23) & (all_0_122_122 = e22 | all_0_123_123 = e22) & (all_0_122_122 = e22 | all_0_125_125 = e22) & (all_0_122_122 = e21 | all_0_123_123 = e21 | all_0_124_124 = e21) & (all_0_123_123 = e23 | all_0_123_123 = e22 | all_0_123_123 = e21) & (all_0_123_123 = e22 | all_0_126_126 = e22) & (all_0_124_124 = e23 | all_0_124_124 = e21) & (all_0_124_124 = e21 | all_0_127_127 = e20) & (all_0_125_125 = e22 | all_0_125_125 = e21 | all_0_125_125 = e20) & (all_0_125_125 = e22 | all_0_126_126 = e22) & (all_0_125_125 = e21 | all_0_126_126 = e21 | all_0_127_127 = e21) & (all_0_125_125 = e20 | all_0_126_126 = e20 | all_0_127_127 = e20) & (all_0_126_126 = e22 | all_0_126_126 = e21 | all_0_126_126 = e20) & (all_0_127_127 = e21 | all_0_127_127 = e20) & (all_0_128_128 = e13 | all_0_128_128 = e10) & (all_0_128_128 = e13 | all_0_129_129 = e13) & (all_0_128_128 = e13 | all_0_130_130 = e13 | all_0_133_133 = e13) & (all_0_128_128 = e13 | all_0_133_133 = e11 | all_0_136_136 = e10) & (all_0_128_128 = e13 | all_0_138_138 = e10 | (all_0_129_129 = e13 & all_0_130_130 = e13 & all_0_133_133 = e11) | (all_0_129_129 = e13 & all_0_130_130 = e13 & all_0_134_134 = e12) | (all_0_132_132 = e10 & all_0_134_134 = e12 & all_0_137_137 = e10) | (all_0_133_133 = e11 & all_0_134_134 = e12)) & (all_0_128_128 = e10 | all_0_129_129 = e10) & (all_0_128_128 = e10 | all_0_130_130 = e10 | all_0_136_136 = e10) & (all_0_129_129 = e13 | all_0_129_129 = e10) & (all_0_129_129 = e13 | all_0_131_131 = e13 | all_0_134_134 = e13) & (all_0_129_129 = e13 | all_0_134_134 = e11 | all_0_137_137 = e10) & (all_0_129_129 = e10 | all_0_131_131 = e10 | all_0_137_137 = e10) & (all_0_130_130 = e13 | all_0_130_130 = e11 | all_0_130_130 = e10) & (all_0_130_130 = e13 | all_0_131_131 = e13 | all_0_132_132 = e13) & (all_0_130_130 = e11 | all_0_131_131 = e11 | all_0_132_132 = e11) & (all_0_130_130 = e11 | all_0_133_133 = e11 | all_0_136_136 = e11) & (all_0_130_130 = e10 | all_0_131_131 = e10 | all_0_132_132 = e10) & (all_0_131_131 = e13 | all_0_131_131 = e11 | all_0_131_131 = e10) & (all_0_131_131 = e11 | all_0_134_134 = e11 | all_0_137_137 = e11) & (all_0_132_132 = e13 | all_0_132_132 = e11 | all_0_132_132 = e10) & (all_0_132_132 = e13 | all_0_135_135 = e13) & (all_0_132_132 = e11 | all_0_135_135 = e11 | all_0_138_138 = e11) & (all_0_132_132 = e10 | all_0_138_138 = e10) & (all_0_133_133 = e13 | all_0_133_133 = e12 | all_0_133_133 = e11) & (all_0_133_133 = e13 | all_0_134_134 = e13 | all_0_135_135 = e13) & (all_0_133_133 = e12 | all_0_134_134 = e12) & (all_0_133_133 = e12 | all_0_136_136 = e12) & (all_0_133_133 = e11 | all_0_134_134 = e11 | all_0_135_135 = e11) & (all_0_134_134 = e13 | all_0_134_134 = e12 | all_0_134_134 = e11) & (all_0_134_134 = e12 | all_0_137_137 = e12) & (all_0_135_135 = e13 | all_0_135_135 = e11) & (all_0_135_135 = e11 | all_0_138_138 = e10) & (all_0_136_136 = e12 | all_0_136_136 = e11 | all_0_136_136 = e10) & (all_0_136_136 = e12 | all_0_137_137 = e12) & (all_0_136_136 = e11 | all_0_137_137 = e11 | all_0_138_138 = e11) & (all_0_136_136 = e10 | all_0_137_137 = e10 | all_0_138_138 = e10) & (all_0_137_137 = e12 | all_0_137_137 = e11 | all_0_137_137 = e10) & (all_0_138_138 = e11 | all_0_138_138 = e10) & (( ~ (all_0_97_97 = e23) & ~ (all_0_98_98 = e22) & ~ (all_0_99_99 = e20) & ~ (all_0_120_120 = e21)) | ( ~ (all_0_100_100 = e23) & ~ (all_0_101_101 = e22) & ~ (all_0_102_102 = e20) & ~ (all_0_124_124 = e21)) | ( ~ (all_0_103_103 = e23) & ~ (all_0_104_104 = e22) & ~ (all_0_105_105 = e20) & ~ (all_0_125_125 = e21))) & (( ~ (all_0_108_108 = e13) & ~ (all_0_109_109 = e12) & ~ (all_0_110_110 = e10) & ~ (all_0_131_131 = e11)) | ( ~ (all_0_111_111 = e13) & ~ (all_0_112_112 = e12) & ~ (all_0_113_113 = e10) & ~ (all_0_135_135 = e11)) | ( ~ (all_0_114_114 = e13) & ~ (all_0_115_115 = e12) & ~ (all_0_116_116 = e10) & ~ (all_0_136_136 = e11))) % 11.39/3.13 | % 11.39/3.13 | Applying alpha-rule on (1) yields: % 11.39/3.13 | (2) ~ (all_0_122_122 = all_0_125_125) % 11.39/3.13 | (3) all_0_136_136 = e12 | all_0_137_137 = e12 % 11.39/3.13 | (4) all_0_132_132 = e10 | all_0_138_138 = e10 % 11.39/3.13 | (5) ~ (all_0_125_125 = all_0_127_127) % 11.39/3.13 | (6) all_0_129_129 = e13 | all_0_131_131 = e13 | all_0_134_134 = e13 % 11.39/3.13 | (7) all_0_117_117 = e23 | all_0_122_122 = e21 | all_0_125_125 = e20 % 11.39/3.13 | (8) op2(all_0_91_91, all_0_120_120) = all_0_31_31 % 11.39/3.13 | (9) ~ (all_0_26_26 = all_0_27_27) | ~ (all_0_28_28 = all_0_29_29) | ~ (all_0_30_30 = e22) | ~ (all_0_31_31 = all_0_92_92) | ~ (all_0_32_32 = all_0_33_33) | ~ (all_0_34_34 = all_0_35_35) | ~ (all_0_36_36 = all_0_92_92) | ~ (all_0_37_37 = all_0_38_38) | ~ (all_0_39_39 = all_0_40_40) | ~ (all_0_41_41 = all_0_42_42) | ~ (all_0_43_43 = all_0_44_44) | ~ (all_0_45_45 = all_0_46_46) | ~ (all_0_47_47 = all_0_48_48) | ~ (all_0_49_49 = all_0_91_91) | ~ (all_0_50_50 = all_0_51_51) | ( ~ (all_0_91_91 = e23) & ~ (all_0_92_92 = e23) & ~ (all_0_120_120 = e23)) | ( ~ (all_0_91_91 = e21) & ~ (all_0_92_92 = e21) & ~ (all_0_120_120 = e21)) | ( ~ (all_0_91_91 = e20) & ~ (all_0_92_92 = e20) & ~ (all_0_120_120 = e20)) % 11.39/3.13 | (10) ~ (all_0_125_125 = all_0_126_126) % 11.39/3.13 | (11) all_0_126_126 = e22 | all_0_126_126 = e21 | all_0_126_126 = e20 % 11.39/3.13 | (12) ~ (all_0_118_118 = all_0_120_120) % 11.39/3.13 | (13) ~ (all_0_121_121 = e22) % 11.39/3.13 | (14) h3(all_0_133_133) = all_0_40_40 % 11.39/3.13 | (15) op2(all_0_127_127, e20) = all_0_93_93 % 11.39/3.13 | (16) op2(all_0_93_93, all_0_94_94) = all_0_65_65 % 11.39/3.13 | (17) op2(all_0_117_117, e23) = all_0_23_23 % 11.39/3.13 | (18) ~ (all_0_124_124 = e22) % 11.39/3.13 | (19) op1(e13, e12) = all_0_129_129 % 11.39/3.13 | (20) op2(all_0_92_92, all_0_92_92) = all_0_34_34 % 11.39/3.13 | (21) op2(e22, all_0_91_91) = all_0_39_39 % 11.39/3.13 | (22) all_0_128_128 = e10 | all_0_130_130 = e10 | all_0_136_136 = e10 % 11.39/3.13 | (23) ~ (all_0_117_117 = all_0_119_119) % 11.39/3.13 | (24) op1(e12, all_0_132_132) = all_0_110_110 % 11.39/3.13 | (25) ~ (e23 = e22) % 11.39/3.13 | (26) ~ (e21 = e10) % 11.39/3.13 | (27) ~ (all_0_123_123 = all_0_126_126) % 11.39/3.13 | (28) all_0_128_128 = e13 | all_0_129_129 = e13 % 11.39/3.13 | (29) all_0_131_131 = e13 | all_0_131_131 = e11 | all_0_131_131 = e10 % 11.39/3.13 | (30) op2(e22, e22) = all_0_120_120 % 11.39/3.13 | (31) all_0_133_133 = e11 | all_0_134_134 = e11 | all_0_135_135 = e11 % 11.39/3.13 | (32) op2(e23, e23) = all_0_117_117 % 11.39/3.13 | (33) all_0_129_129 = e13 | all_0_134_134 = e11 | all_0_137_137 = e10 % 11.39/3.13 | (34) all_0_118_118 = e23 | all_0_120_120 = e23 | all_0_123_123 = e23 % 11.39/3.13 | (35) ~ (all_0_117_117 = all_0_118_118) % 11.39/3.13 | (36) op1(e10, e11) = e13 % 11.39/3.13 | (37) ~ (all_0_129_129 = all_0_134_134) % 11.39/3.13 | (38) op2(all_0_90_90, e23) = all_0_10_10 % 11.39/3.13 | (39) all_0_135_135 = e13 | all_0_135_135 = e11 % 11.39/3.13 | (40) ~ (all_0_134_134 = all_0_135_135) % 11.39/3.13 | (41) op2(e22, e21) = e22 % 11.39/3.13 | (42) ~ (e22 = e11) % 11.39/3.13 | (43) ~ (all_0_138_138 = e13) % 11.39/3.13 | (44) h4(e11) = e23 % 11.39/3.13 | (45) h3(all_0_129_129) = all_0_29_29 % 11.39/3.13 | (46) h4(all_0_137_137) = all_0_22_22 % 11.39/3.13 | (47) all_0_117_117 = e20 | all_0_119_119 = e20 | all_0_125_125 = e20 % 11.39/3.13 | (48) op2(all_0_120_120, e22) = all_0_49_49 % 11.39/3.13 | (49) all_0_133_133 = e12 | all_0_136_136 = e12 % 11.39/3.13 | (50) op1(e12, e12) = all_0_131_131 % 11.39/3.13 | (51) op2(e22, e20) = all_0_121_121 % 11.39/3.13 | (52) all_0_130_130 = e11 | all_0_133_133 = e11 | all_0_136_136 = e11 % 11.39/3.13 | (53) op2(all_0_94_94, all_0_94_94) = all_0_71_71 % 11.39/3.13 | (54) all_0_121_121 = e21 | all_0_124_124 = e21 | all_0_127_127 = e21 % 11.39/3.13 | (55) all_0_128_128 = e13 | all_0_133_133 = e11 | all_0_136_136 = e10 % 11.39/3.13 | (56) all_0_117_117 = e23 | all_0_127_127 = e20 | (all_0_118_118 = e23 & all_0_119_119 = e23 & all_0_122_122 = e21) | (all_0_118_118 = e23 & all_0_119_119 = e23 & all_0_123_123 = e22) | (all_0_121_121 = e20 & all_0_123_123 = e22 & all_0_126_126 = e20) | (all_0_122_122 = e21 & all_0_123_123 = e22) % 11.39/3.13 | (57) op2(all_0_91_91, all_0_92_92) = all_0_28_28 % 11.39/3.13 | (58) h3(all_0_138_138) = all_0_51_51 % 11.39/3.13 | (59) op2(all_0_89_89, e23) = all_0_4_4 % 11.39/3.13 | (60) op1(e13, e13) = all_0_128_128 % 11.39/3.13 | (61) ~ (all_0_129_129 = e11) % 11.39/3.13 | (62) all_0_120_120 = e23 | all_0_120_120 = e21 | all_0_120_120 = e20 % 11.39/3.13 | (63) h3(all_0_134_134) = all_0_42_42 % 11.39/3.13 | (64) all_0_119_119 = e20 | all_0_120_120 = e20 | all_0_121_121 = e20 % 11.39/3.13 | (65) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h3(v2) = v1) | ~ (h3(v2) = v0)) % 11.39/3.13 | (66) ~ (all_0_120_120 = all_0_123_123) % 11.39/3.13 | (67) op2(all_0_117_117, all_0_90_90) = all_0_21_21 % 11.39/3.13 | (68) op2(all_0_127_127, e20) = all_0_86_86 % 11.39/3.13 | (69) ~ (all_0_128_128 = e12) % 11.39/3.14 | (70) h4(all_0_129_129) = all_0_3_3 % 11.39/3.14 | (71) all_0_128_128 = e13 | all_0_130_130 = e13 | all_0_133_133 = e13 % 11.39/3.14 | (72) h1(all_0_135_135) = all_0_81_81 % 11.39/3.14 | (73) all_0_132_132 = e13 | all_0_132_132 = e11 | all_0_132_132 = e10 % 11.39/3.14 | (74) all_0_137_137 = e12 | all_0_137_137 = e11 | all_0_137_137 = e10 % 11.39/3.14 | (75) ~ (all_0_119_119 = all_0_125_125) % 11.39/3.14 | (76) op1(e11, all_0_135_135) = all_0_113_113 % 11.39/3.14 | (77) op1(e11, all_0_133_133) = all_0_111_111 % 11.39/3.14 | (78) h1(all_0_129_129) = all_0_66_66 % 11.39/3.14 | (79) h4(e10) = all_0_117_117 % 11.39/3.14 | (80) all_0_138_138 = e11 | all_0_138_138 = e10 % 11.39/3.14 | (81) ~ (all_0_123_123 = e20) % 11.39/3.14 | (82) ~ (all_0_138_138 = e12) % 11.39/3.14 | (83) ~ (all_0_117_117 = e21) % 11.39/3.14 | (84) all_0_118_118 = e23 | all_0_123_123 = e21 | all_0_126_126 = e20 % 11.39/3.14 | (85) op2(e21, e23) = all_0_122_122 % 11.39/3.14 | (86) all_0_136_136 = e10 | all_0_137_137 = e10 | all_0_138_138 = e10 % 11.39/3.14 | (87) h2(e11) = e21 % 11.39/3.14 | (88) op2(e22, all_0_92_92) = all_0_41_41 % 11.39/3.14 | (89) h1(all_0_138_138) = all_0_88_88 % 11.39/3.14 | (90) op2(e22, all_0_120_120) = all_0_43_43 % 11.39/3.14 | (91) ~ (all_0_135_135 = e12) % 11.39/3.14 | (92) ~ (all_0_130_130 = all_0_133_133) % 11.39/3.14 | (93) ~ (all_0_129_129 = all_0_131_131) % 11.39/3.14 | (94) all_0_118_118 = e20 | all_0_120_120 = e20 | all_0_126_126 = e20 % 11.39/3.14 | (95) ( ~ (all_0_108_108 = e13) & ~ (all_0_109_109 = e12) & ~ (all_0_110_110 = e10) & ~ (all_0_131_131 = e11)) | ( ~ (all_0_111_111 = e13) & ~ (all_0_112_112 = e12) & ~ (all_0_113_113 = e10) & ~ (all_0_135_135 = e11)) | ( ~ (all_0_114_114 = e13) & ~ (all_0_115_115 = e12) & ~ (all_0_116_116 = e10) & ~ (all_0_136_136 = e11)) % 11.39/3.14 | (96) ~ (all_0_130_130 = all_0_136_136) % 11.39/3.14 | (97) ~ (all_0_132_132 = all_0_138_138) % 11.39/3.14 | (98) ~ (all_0_129_129 = all_0_137_137) % 11.39/3.14 | (99) ~ (all_0_130_130 = e12) % 11.39/3.14 | (100) h2(e10) = e20 % 11.39/3.14 | (101) h3(all_0_131_131) = all_0_35_35 % 11.39/3.14 | (102) all_0_125_125 = e22 | all_0_126_126 = e22 % 11.39/3.14 | (103) ~ (e23 = e13) % 11.39/3.14 | (104) all_0_119_119 = e21 | all_0_122_122 = e21 | all_0_125_125 = e21 % 11.39/3.14 | (105) op2(all_0_91_91, all_0_120_120) = all_0_92_92 % 11.39/3.14 | (106) ~ (all_0_125_125 = e23) % 11.39/3.14 | (107) h1(all_0_132_132) = all_0_75_75 % 11.39/3.14 | (108) all_0_130_130 = e13 | all_0_131_131 = e13 | all_0_132_132 = e13 % 11.39/3.14 | (109) h4(all_0_133_133) = all_0_14_14 % 11.39/3.14 | (110) h4(all_0_135_135) = all_0_18_18 % 11.39/3.14 | (111) all_0_125_125 = e20 | all_0_126_126 = e20 | all_0_127_127 = e20 % 11.39/3.14 | (112) op2(all_0_93_93, e20) = all_0_67_67 % 11.39/3.14 | (113) op2(all_0_127_127, all_0_93_93) = all_0_82_82 % 11.39/3.14 | (114) op1(e13, all_0_128_128) = all_0_106_106 % 11.39/3.14 | (115) ~ (all_0_117_117 = e22) % 11.39/3.14 | (116) h1(all_0_133_133) = all_0_77_77 % 11.39/3.14 | (117) h2(all_0_128_128) = all_0_52_52 % 11.39/3.14 | (118) ~ (e22 = e20) % 11.39/3.14 | (119) all_0_129_129 = e13 | all_0_129_129 = e10 % 11.39/3.14 | (120) h1(all_0_128_128) = all_0_64_64 % 11.39/3.14 | (121) ~ (all_0_117_117 = all_0_125_125) % 11.39/3.14 | (122) op2(all_0_92_92, all_0_91_91) = all_0_32_32 % 11.39/3.14 | (123) all_0_130_130 = e10 | all_0_131_131 = e10 | all_0_132_132 = e10 % 11.39/3.14 | (124) h2(e12) = e22 % 11.39/3.14 | (125) h4(e12) = all_0_90_90 % 11.39/3.14 | (126) all_0_129_129 = e10 | all_0_131_131 = e10 | all_0_137_137 = e10 % 11.39/3.14 | (127) op2(all_0_91_91, e22) = all_0_30_30 % 11.39/3.14 | (128) op1(e11, e12) = all_0_134_134 % 11.39/3.14 | (129) op1(e10, all_0_136_136) = all_0_114_114 % 11.39/3.14 | (130) all_0_133_133 = e13 | all_0_133_133 = e12 | all_0_133_133 = e11 % 11.39/3.14 | (131) h4(all_0_134_134) = all_0_16_16 % 11.39/3.14 | (132) all_0_132_132 = e11 | all_0_135_135 = e11 | all_0_138_138 = e11 % 11.39/3.14 | (133) op2(all_0_89_89, all_0_90_90) = all_0_2_2 % 11.39/3.14 | (134) ~ (all_0_121_121 = all_0_124_124) % 11.39/3.14 | (135) op2(e20, all_0_127_127) = all_0_105_105 % 11.39/3.14 | (136) op1(e10, e10) = all_0_138_138 % 11.39/3.14 | (137) ~ (all_0_126_126 = all_0_127_127) % 11.39/3.14 | (138) h1(all_0_130_130) = all_0_70_70 % 11.39/3.14 | (139) ~ (all_0_131_131 = all_0_132_132) % 11.39/3.14 | (140) ~ (all_0_119_119 = e22) % 11.39/3.14 | (141) all_0_120_120 = e21 | all_0_123_123 = e21 | all_0_126_126 = e21 % 11.39/3.14 | (142) all_0_118_118 = e23 | all_0_118_118 = e20 % 11.39/3.14 | (143) op2(all_0_89_89, all_0_117_117) = all_0_5_5 % 11.39/3.14 | (144) ~ (all_0_118_118 = all_0_123_123) % 11.39/3.15 | (145) op2(e20, all_0_127_127) = all_0_80_80 % 11.39/3.15 | (146) all_0_119_119 = e21 | all_0_120_120 = e21 | all_0_121_121 = e21 % 11.39/3.15 | (147) ~ (all_0_131_131 = all_0_134_134) % 11.39/3.15 | (148) op2(e23, e20) = e22 % 11.39/3.15 | (149) all_0_125_125 = e22 | all_0_125_125 = e21 | all_0_125_125 = e20 % 11.39/3.15 | (150) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h1(v2) = v1) | ~ (h1(v2) = v0)) % 11.39/3.15 | (151) op2(e20, e23) = all_0_125_125 % 11.39/3.15 | (152) op2(all_0_120_120, all_0_120_120) = all_0_50_50 % 11.39/3.15 | (153) h2(all_0_130_130) = all_0_54_54 % 11.39/3.15 | (154) ~ (all_0_133_133 = e10) % 11.39/3.15 | (155) ~ (e21 = e11) % 11.39/3.15 | (156) all_0_133_133 = e13 | all_0_134_134 = e13 | all_0_135_135 = e13 % 11.39/3.15 | (157) h2(all_0_134_134) = all_0_58_58 % 11.39/3.15 | (158) ~ (all_0_133_133 = all_0_134_134) % 11.39/3.15 | (159) ~ (all_0_136_136 = all_0_137_137) % 11.39/3.15 | (160) ~ (e12 = e10) % 11.39/3.15 | (161) op2(all_0_120_120, all_0_91_91) = all_0_45_45 % 11.39/3.15 | (162) ~ (all_0_128_128 = all_0_136_136) % 11.39/3.15 | (163) h3(all_0_135_135) = all_0_44_44 % 11.39/3.15 | (164) ~ (all_0_137_137 = all_0_138_138) % 11.39/3.15 | (165) all_0_119_119 = e23 | all_0_119_119 = e21 | all_0_119_119 = e20 % 11.39/3.15 | (166) ~ (e20 = e10) % 11.39/3.15 | (167) all_0_117_117 = e23 | all_0_118_118 = e23 % 11.39/3.15 | (168) all_0_122_122 = e23 | all_0_122_122 = e22 | all_0_122_122 = e21 % 11.39/3.15 | (169) ~ (all_0_119_119 = all_0_120_120) % 11.39/3.15 | (170) op2(e20, e21) = e23 % 11.39/3.15 | (171) h3(all_0_136_136) = all_0_46_46 % 11.39/3.15 | (172) ~ (all_0_135_135 = e10) % 11.39/3.15 | (173) h2(e13) = e23 % 11.39/3.15 | (174) op2(e21, all_0_122_122) = all_0_100_100 % 11.39/3.15 | (175) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op2(v3, v2) = v1) | ~ (op2(v3, v2) = v0)) % 11.39/3.15 | (176) all_0_130_130 = e13 | all_0_130_130 = e11 | all_0_130_130 = e10 % 11.39/3.15 | (177) ~ (all_0_133_133 = all_0_135_135) % 11.39/3.15 | (178) all_0_132_132 = e13 | all_0_135_135 = e13 % 11.39/3.15 | (179) op2(all_0_120_120, all_0_92_92) = all_0_47_47 % 11.39/3.15 | (180) op2(all_0_90_90, all_0_117_117) = all_0_11_11 % 11.39/3.15 | (181) ~ (all_0_119_119 = all_0_122_122) % 11.39/3.15 | (182) op2(e21, all_0_123_123) = all_0_101_101 % 11.39/3.15 | (183) all_0_124_124 = e21 | all_0_127_127 = e20 % 11.39/3.15 | (184) all_0_127_127 = e21 | all_0_127_127 = e20 % 11.39/3.15 | (185) op2(all_0_117_117, e23) = all_0_89_89 % 11.39/3.15 | (186) op2(e23, all_0_117_117) = all_0_17_17 % 11.39/3.15 | (187) all_0_121_121 = e23 | all_0_121_121 = e21 | all_0_121_121 = e20 % 11.39/3.15 | (188) op2(e23, all_0_117_117) = all_0_95_95 % 11.39/3.15 | (189) ~ (all_0_131_131 = e12) % 11.39/3.15 | (190) op2(all_0_91_91, all_0_91_91) = all_0_26_26 % 11.39/3.15 | (191) h2(all_0_135_135) = all_0_59_59 % 11.39/3.15 | (192) h1(e10) = all_0_127_127 % 11.39/3.15 | (193) op2(e23, all_0_89_89) = all_0_13_13 % 11.39/3.15 | (194) h2(all_0_131_131) = all_0_55_55 % 11.39/3.15 | (195) ~ (all_0_126_126 = e23) % 11.39/3.15 | (196) op2(e20, all_0_93_93) = all_0_76_76 % 11.39/3.15 | (197) ~ (e13 = e10) % 11.39/3.15 | (198) all_0_134_134 = e13 | all_0_134_134 = e12 | all_0_134_134 = e11 % 11.39/3.15 | (199) op2(all_0_117_117, all_0_89_89) = all_0_19_19 % 11.39/3.15 | (200) ~ (all_0_134_134 = e10) % 11.39/3.15 | (201) ~ (all_0_52_52 = all_0_117_117) | ~ (all_0_53_53 = all_0_118_118) | ~ (all_0_54_54 = all_0_119_119) | ~ (all_0_55_55 = all_0_120_120) | ~ (all_0_56_56 = all_0_121_121) | ~ (all_0_57_57 = all_0_122_122) | ~ (all_0_58_58 = all_0_123_123) | ~ (all_0_59_59 = all_0_124_124) | ~ (all_0_60_60 = all_0_125_125) | ~ (all_0_61_61 = all_0_126_126) | ~ (all_0_62_62 = all_0_127_127) % 11.39/3.15 | (202) h3(all_0_128_128) = all_0_27_27 % 11.39/3.15 | (203) ~ (all_0_128_128 = all_0_129_129) % 11.39/3.15 | (204) h3(e13) = all_0_91_91 % 11.39/3.15 | (205) op1(e13, e10) = e12 % 11.39/3.15 | (206) op2(all_0_94_94, all_0_127_127) = all_0_74_74 % 11.39/3.15 | (207) all_0_130_130 = e11 | all_0_131_131 = e11 | all_0_132_132 = e11 % 11.39/3.15 | (208) op2(all_0_93_93, all_0_93_93) = all_0_63_63 % 11.39/3.15 | (209) op2(all_0_90_90, all_0_89_89) = all_0_6_6 % 11.39/3.15 | (210) ~ (all_0_122_122 = all_0_124_124) % 11.39/3.15 | (211) op2(all_0_89_89, all_0_117_117) = all_0_90_90 % 11.39/3.15 | (212) all_0_122_122 = e23 | all_0_123_123 = e23 | all_0_124_124 = e23 % 11.39/3.15 | (213) all_0_121_121 = e20 | all_0_127_127 = e20 % 11.39/3.15 | (214) ~ (e20 = e13) % 11.39/3.15 | (215) ~ (all_0_136_136 = e13) % 11.39/3.15 | (216) all_0_117_117 = e23 | all_0_119_119 = e23 | all_0_122_122 = e23 % 11.39/3.15 | (217) op1(e10, all_0_138_138) = all_0_116_116 % 11.39/3.15 | (218) ~ (e20 = e11) % 11.39/3.15 | (219) op1(e12, e10) = all_0_132_132 % 11.39/3.15 | (220) h3(e10) = all_0_120_120 % 11.39/3.15 | (221) all_0_123_123 = e23 | all_0_123_123 = e22 | all_0_123_123 = e21 % 11.39/3.15 | (222) op2(e23, all_0_118_118) = all_0_96_96 % 11.39/3.15 | (223) ~ (e23 = e10) % 11.39/3.15 | (224) op2(all_0_93_93, all_0_127_127) = all_0_68_68 % 11.39/3.15 | (225) op1(e11, e10) = all_0_135_135 % 11.39/3.15 | (226) all_0_125_125 = e21 | all_0_126_126 = e21 | all_0_127_127 = e21 % 11.39/3.15 | (227) ~ (all_0_119_119 = all_0_121_121) % 11.39/3.15 | (228) h1(e12) = all_0_94_94 % 11.39/3.15 | (229) all_0_122_122 = e21 | all_0_123_123 = e21 | all_0_124_124 = e21 % 11.39/3.15 | (230) h4(all_0_128_128) = all_0_1_1 % 11.39/3.15 | (231) all_0_124_124 = e23 | all_0_124_124 = e21 % 11.39/3.15 | (232) h1(e13) = all_0_93_93 % 11.39/3.15 | (233) h3(all_0_130_130) = all_0_33_33 % 11.39/3.15 | (234) ( ~ (all_0_97_97 = e23) & ~ (all_0_98_98 = e22) & ~ (all_0_99_99 = e20) & ~ (all_0_120_120 = e21)) | ( ~ (all_0_100_100 = e23) & ~ (all_0_101_101 = e22) & ~ (all_0_102_102 = e20) & ~ (all_0_124_124 = e21)) | ( ~ (all_0_103_103 = e23) & ~ (all_0_104_104 = e22) & ~ (all_0_105_105 = e20) & ~ (all_0_125_125 = e21)) % 11.39/3.15 | (235) ~ (all_0_122_122 = e20) % 11.39/3.15 | (236) op1(e12, all_0_131_131) = all_0_109_109 % 11.39/3.15 | (237) op2(e23, e22) = all_0_118_118 % 11.39/3.15 | (238) h1(e11) = e20 % 11.39/3.15 | (239) op1(e10, all_0_137_137) = all_0_115_115 % 11.39/3.15 | (240) op2(e20, all_0_126_126) = all_0_104_104 % 11.39/3.15 | (241) op2(all_0_127_127, all_0_127_127) = all_0_87_87 % 11.39/3.15 | (242) ~ (all_0_120_120 = all_0_126_126) % 11.39/3.15 | (243) op2(e21, e20) = all_0_124_124 % 11.39/3.15 | (244) op2(all_0_120_120, e22) = all_0_91_91 % 11.39/3.15 | (245) ~ (all_0_117_117 = all_0_122_122) % 11.39/3.16 | (246) op2(e21, all_0_124_124) = all_0_102_102 % 11.39/3.16 | (247) all_0_135_135 = e11 | all_0_138_138 = e10 % 11.39/3.16 | (248) op1(e13, e11) = e11 % 11.39/3.16 | (249) ~ (e22 = e21) % 11.39/3.16 | (250) op2(e21, e22) = all_0_123_123 % 11.39/3.16 | (251) h3(all_0_132_132) = all_0_38_38 % 11.39/3.16 | (252) op1(e12, e11) = e12 % 11.39/3.16 | (253) op2(all_0_92_92, all_0_120_120) = all_0_37_37 % 11.39/3.16 | (254) h1(all_0_137_137) = all_0_85_85 % 11.39/3.16 | (255) h4(all_0_138_138) = all_0_25_25 % 11.39/3.16 | (256) op1(e10, e13) = all_0_136_136 % 11.39/3.16 | (257) ~ (e23 = e12) % 11.39/3.16 | (258) ~ (all_0_132_132 = e12) % 11.39/3.16 | (259) ~ (all_0_128_128 = all_0_133_133) % 11.39/3.16 | (260) ~ (all_0_123_123 = all_0_124_124) % 11.39/3.16 | (261) ~ (all_0_127_127 = e22) % 11.39/3.16 | (262) ~ (all_0_133_133 = all_0_136_136) % 11.39/3.16 | (263) op2(all_0_127_127, all_0_94_94) = all_0_84_84 % 11.39/3.16 | (264) all_0_136_136 = e12 | all_0_136_136 = e11 | all_0_136_136 = e10 % 11.39/3.16 | (265) ~ (e20 = e12) % 11.39/3.16 | (266) ~ (e23 = e20) % 11.39/3.16 | (267) op1(e11, e13) = all_0_133_133 % 11.39/3.16 | (268) ~ (all_0_124_124 = e20) % 11.39/3.16 | (269) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h2(v2) = v1) | ~ (h2(v2) = v0)) % 11.39/3.16 | (270) ~ (all_0_118_118 = all_0_126_126) % 11.39/3.16 | (271) ~ (all_0_118_118 = e21) % 11.39/3.16 | (272) ~ (all_0_0_0 = all_0_1_1) | ~ (all_0_2_2 = all_0_3_3) | ~ (all_0_4_4 = e23) | ~ (all_0_5_5 = all_0_90_90) | ~ (all_0_6_6 = all_0_7_7) | ~ (all_0_8_8 = all_0_9_9) | ~ (all_0_10_10 = all_0_90_90) | ~ (all_0_11_11 = all_0_12_12) | ~ (all_0_13_13 = all_0_14_14) | ~ (all_0_15_15 = all_0_16_16) | ~ (all_0_17_17 = all_0_18_18) | ~ (all_0_19_19 = all_0_20_20) | ~ (all_0_21_21 = all_0_22_22) | ~ (all_0_23_23 = all_0_89_89) | ~ (all_0_24_24 = all_0_25_25) | ( ~ (all_0_89_89 = e22) & ~ (all_0_90_90 = e22)) | ( ~ (all_0_89_89 = e21) & ~ (all_0_90_90 = e21)) | ( ~ (all_0_89_89 = e20) & ~ (all_0_90_90 = e20) & ~ (all_0_117_117 = e20)) % 11.39/3.16 | (273) op2(e21, e21) = e20 % 11.39/3.16 | (274) h3(e11) = e22 % 11.39/3.16 | (275) op1(e11, all_0_134_134) = all_0_112_112 % 11.39/3.16 | (276) ~ (all_0_135_135 = all_0_138_138) % 11.39/3.16 | (277) h2(all_0_138_138) = all_0_62_62 % 11.39/3.16 | (278) ~ (e23 = e21) % 11.39/3.16 | (279) op2(e20, all_0_94_94) = all_0_78_78 % 11.39/3.16 | (280) h2(all_0_133_133) = all_0_57_57 % 11.39/3.16 | (281) op2(all_0_94_94, all_0_93_93) = all_0_69_69 % 11.39/3.16 | (282) op2(e22, all_0_119_119) = all_0_97_97 % 11.39/3.16 | (283) ~ (e22 = e13) % 11.39/3.16 | (284) h2(all_0_132_132) = all_0_56_56 % 11.39/3.16 | (285) ~ (e22 = e12) % 11.39/3.16 | (286) op2(e22, all_0_120_120) = all_0_98_98 % 11.39/3.16 | (287) ~ (e13 = e12) % 11.39/3.16 | (288) h3(e12) = all_0_92_92 % 11.39/3.16 | (289) op2(all_0_90_90, all_0_90_90) = all_0_8_8 % 11.39/3.16 | (290) h4(all_0_131_131) = all_0_9_9 % 11.39/3.16 | (291) op2(e20, e20) = all_0_127_127 % 11.39/3.16 | (292) ~ (e11 = e10) % 11.39/3.16 | (293) all_0_136_136 = e11 | all_0_137_137 = e11 | all_0_138_138 = e11 % 11.39/3.16 | (294) all_0_134_134 = e12 | all_0_137_137 = e12 % 11.39/3.16 | (295) op2(all_0_117_117, all_0_117_117) = all_0_24_24 % 11.39/3.16 | (296) all_0_121_121 = e23 | all_0_124_124 = e23 % 11.39/3.16 | (297) all_0_128_128 = e13 | all_0_138_138 = e10 | (all_0_129_129 = e13 & all_0_130_130 = e13 & all_0_133_133 = e11) | (all_0_129_129 = e13 & all_0_130_130 = e13 & all_0_134_134 = e12) | (all_0_132_132 = e10 & all_0_134_134 = e12 & all_0_137_137 = e10) | (all_0_133_133 = e11 & all_0_134_134 = e12) % 11.39/3.16 | (298) op1(e11, e11) = e10 % 11.39/3.16 | (299) ~ (e23 = e11) % 11.39/3.16 | (300) ~ (all_0_63_63 = all_0_64_64) | ~ (all_0_65_65 = all_0_66_66) | ~ (all_0_67_67 = e20) | ~ (all_0_68_68 = all_0_94_94) | ~ (all_0_69_69 = all_0_70_70) | ~ (all_0_71_71 = all_0_72_72) | ~ (all_0_73_73 = all_0_94_94) | ~ (all_0_74_74 = all_0_75_75) | ~ (all_0_76_76 = all_0_77_77) | ~ (all_0_78_78 = all_0_79_79) | ~ (all_0_80_80 = all_0_81_81) | ~ (all_0_82_82 = all_0_83_83) | ~ (all_0_84_84 = all_0_85_85) | ~ (all_0_86_86 = all_0_93_93) | ~ (all_0_87_87 = all_0_88_88) | ( ~ (all_0_93_93 = e23) & ~ (all_0_94_94 = e23)) | ( ~ (all_0_93_93 = e22) & ~ (all_0_94_94 = e22)) | ( ~ (all_0_93_93 = e21) & ~ (all_0_94_94 = e21) & ~ (all_0_127_127 = e21)) % 11.39/3.16 | (301) all_0_119_119 = e23 | all_0_120_120 = e23 | all_0_121_121 = e23 % 11.39/3.16 | (302) op2(e20, e22) = all_0_126_126 % 11.39/3.16 | (303) ~ (all_0_130_130 = all_0_131_131) % 11.39/3.16 | (304) ~ (e12 = e11) % 11.39/3.16 | (305) h1(all_0_131_131) = all_0_72_72 % 11.39/3.16 | (306) ~ (all_0_120_120 = all_0_121_121) % 11.39/3.16 | (307) ~ (all_0_121_121 = all_0_127_127) % 11.39/3.16 | (308) all_0_133_133 = e12 | all_0_134_134 = e12 % 11.39/3.16 | (309) ~ (e21 = e12) % 11.39/3.16 | (310) all_0_128_128 = e13 | all_0_128_128 = e10 % 11.39/3.16 | (311) h3(all_0_137_137) = all_0_48_48 % 11.39/3.16 | (312) all_0_122_122 = e22 | all_0_125_125 = e22 % 11.39/3.16 | (313) ~ (all_0_128_128 = e11) % 11.39/3.16 | (314) op2(all_0_89_89, all_0_89_89) = all_0_0_0 % 11.39/3.16 | (315) op2(e22, all_0_121_121) = all_0_99_99 % 11.39/3.16 | (316) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op1(v3, v2) = v1) | ~ (op1(v3, v2) = v0)) % 11.39/3.16 | (317) op2(e20, all_0_125_125) = all_0_103_103 % 11.39/3.16 | (318) ~ (all_0_132_132 = all_0_135_135) % 11.39/3.16 | (319) ~ (all_0_129_129 = e12) % 11.39/3.16 | (320) ~ (e21 = e20) % 11.39/3.16 | (321) op2(e23, all_0_90_90) = all_0_15_15 % 11.39/3.16 | (322) h4(e13) = all_0_89_89 % 11.39/3.16 | (323) h1(all_0_134_134) = all_0_79_79 % 11.39/3.16 | (324) h4(all_0_132_132) = all_0_12_12 % 11.39/3.16 | (325) ~ (all_0_124_124 = all_0_127_127) % 11.39/3.16 | (326) op1(e12, all_0_130_130) = all_0_108_108 % 11.39/3.16 | (327) ~ (all_0_122_122 = all_0_123_123) % 11.39/3.16 | (328) all_0_123_123 = e22 | all_0_126_126 = e22 % 11.39/3.16 | (329) op2(e22, e23) = all_0_119_119 % 11.39/3.16 | (330) ~ (all_0_137_137 = e13) % 11.39/3.16 | (331) ~ (e21 = e13) % 11.39/3.16 | (332) ~ (all_0_131_131 = all_0_137_137) % 11.39/3.16 | (333) all_0_117_117 = e20 | all_0_118_118 = e20 % 11.39/3.16 | (334) all_0_122_122 = e22 | all_0_123_123 = e22 % 11.39/3.16 | (335) ~ (all_0_128_128 = all_0_130_130) % 11.39/3.16 | (336) h2(all_0_136_136) = all_0_60_60 % 11.39/3.16 | (337) ~ (all_0_127_127 = e23) % 11.39/3.16 | (338) ~ (all_0_134_134 = all_0_137_137) % 11.39/3.16 | (339) h4(all_0_136_136) = all_0_20_20 % 11.39/3.16 | (340) ~ (all_0_120_120 = e22) % 11.39/3.16 | (341) ~ (all_0_136_136 = all_0_138_138) % 11.39/3.16 | (342) all_0_128_128 = e10 | all_0_129_129 = e10 % 11.39/3.16 | (343) ~ (e13 = e11) % 11.39/3.16 | (344) ~ (all_0_130_130 = all_0_132_132) % 11.39/3.16 | (345) ~ (all_0_118_118 = e22) % 11.39/3.17 | (346) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h4(v2) = v1) | ~ (h4(v2) = v0)) % 11.39/3.17 | (347) h4(all_0_130_130) = all_0_7_7 % 11.39/3.17 | (348) all_0_131_131 = e11 | all_0_134_134 = e11 | all_0_137_137 = e11 % 11.39/3.17 | (349) h1(all_0_136_136) = all_0_83_83 % 11.39/3.17 | (350) op2(all_0_93_93, all_0_127_127) = all_0_94_94 % 11.39/3.17 | (351) op1(e12, e13) = all_0_130_130 % 11.39/3.17 | (352) op2(all_0_92_92, e22) = all_0_36_36 % 11.39/3.17 | (353) h2(all_0_129_129) = all_0_53_53 % 11.39/3.17 | (354) op2(e23, e21) = e21 % 11.39/3.17 | (355) ~ (e22 = e10) % 11.39/3.17 | (356) all_0_117_117 = e23 | all_0_117_117 = e20 % 11.39/3.17 | (357) op1(e13, all_0_129_129) = all_0_107_107 % 11.39/3.17 | (358) h2(all_0_137_137) = all_0_61_61 % 11.39/3.17 | (359) op2(all_0_94_94, e20) = all_0_73_73 % 11.39/3.17 | (360) op1(e10, e12) = all_0_137_137 % 11.39/3.17 | % 11.78/3.17 | Instantiating formula (175) with all_0_127_127, e20, all_0_93_93, all_0_86_86 and discharging atoms op2(all_0_127_127, e20) = all_0_86_86, op2(all_0_127_127, e20) = all_0_93_93, yields: % 11.78/3.17 | (361) all_0_86_86 = all_0_93_93 % 11.78/3.17 | % 11.78/3.17 | Instantiating formula (175) with e20, all_0_127_127, all_0_105_105, all_0_80_80 and discharging atoms op2(e20, all_0_127_127) = all_0_80_80, op2(e20, all_0_127_127) = all_0_105_105, yields: % 11.78/3.17 | (362) all_0_80_80 = all_0_105_105 % 11.78/3.17 | % 11.78/3.17 | From (361) and (68) follows: % 11.78/3.17 | (15) op2(all_0_127_127, e20) = all_0_93_93 % 11.78/3.17 | % 11.78/3.17 | From (362) and (145) follows: % 11.78/3.17 | (135) op2(e20, all_0_127_127) = all_0_105_105 % 11.78/3.17 | % 11.78/3.17 +-Applying beta-rule and splitting (183), into two cases. % 11.78/3.17 |-Branch one: % 11.78/3.17 | (365) all_0_127_127 = e20 % 11.78/3.17 | % 11.78/3.17 | Equations (365) can reduce 307 to: % 11.78/3.17 | (366) ~ (all_0_121_121 = e20) % 11.78/3.17 | % 11.78/3.17 | Equations (365) can reduce 137 to: % 11.78/3.17 | (367) ~ (all_0_126_126 = e20) % 11.78/3.17 | % 11.78/3.17 | Equations (365) can reduce 337 to: % 11.78/3.17 | (368) ~ (e23 = e20) % 11.78/3.17 | % 11.78/3.17 | Simplifying 368 yields: % 11.78/3.17 | (266) ~ (e23 = e20) % 11.78/3.17 | % 11.78/3.17 | From (365)(365) and (241) follows: % 11.78/3.17 | (370) op2(e20, e20) = all_0_87_87 % 11.78/3.17 | % 11.78/3.17 | From (365) and (15) follows: % 11.78/3.17 | (371) op2(e20, e20) = all_0_93_93 % 11.78/3.17 | % 11.78/3.17 | From (365) and (135) follows: % 11.78/3.17 | (372) op2(e20, e20) = all_0_105_105 % 11.78/3.17 | % 11.78/3.17 | From (365) and (291) follows: % 11.78/3.17 | (373) op2(e20, e20) = e20 % 11.78/3.17 | % 11.78/3.17 | Instantiating formula (175) with e20, e20, all_0_93_93, all_0_87_87 and discharging atoms op2(e20, e20) = all_0_87_87, op2(e20, e20) = all_0_93_93, yields: % 11.78/3.17 | (374) all_0_87_87 = all_0_93_93 % 11.78/3.17 | % 11.78/3.17 | Instantiating formula (175) with e20, e20, all_0_105_105, all_0_93_93 and discharging atoms op2(e20, e20) = all_0_93_93, op2(e20, e20) = all_0_105_105, yields: % 11.78/3.17 | (375) all_0_93_93 = all_0_105_105 % 11.78/3.17 | % 11.78/3.17 | Instantiating formula (175) with e20, e20, e20, all_0_87_87 and discharging atoms op2(e20, e20) = all_0_87_87, op2(e20, e20) = e20, yields: % 11.78/3.17 | (376) all_0_87_87 = e20 % 11.78/3.17 | % 11.78/3.17 | Combining equations (374,376) yields a new equation: % 11.78/3.17 | (377) all_0_93_93 = e20 % 11.78/3.17 | % 11.78/3.17 | Simplifying 377 yields: % 11.78/3.17 | (378) all_0_93_93 = e20 % 11.78/3.17 | % 11.78/3.17 | Combining equations (375,378) yields a new equation: % 11.78/3.17 | (379) all_0_105_105 = e20 % 11.78/3.17 | % 11.78/3.17 | Simplifying 379 yields: % 11.78/3.17 | (380) all_0_105_105 = e20 % 11.78/3.17 | % 11.78/3.17 +-Applying beta-rule and splitting (142), into two cases. % 11.78/3.17 |-Branch one: % 11.78/3.17 | (381) all_0_118_118 = e20 % 11.78/3.17 | % 11.78/3.17 | Equations (381) can reduce 12 to: % 11.78/3.17 | (382) ~ (all_0_120_120 = e20) % 11.78/3.17 | % 11.78/3.17 | Simplifying 382 yields: % 11.78/3.17 | (383) ~ (all_0_120_120 = e20) % 11.78/3.17 | % 11.78/3.17 | Equations (381) can reduce 144 to: % 11.78/3.17 | (384) ~ (all_0_123_123 = e20) % 11.78/3.17 | % 11.78/3.17 | Simplifying 384 yields: % 11.78/3.17 | (81) ~ (all_0_123_123 = e20) % 11.78/3.17 | % 11.78/3.17 | Equations (381) can reduce 270 to: % 11.78/3.17 | (386) ~ (all_0_126_126 = e20) % 11.78/3.17 | % 11.78/3.17 | Simplifying 386 yields: % 11.78/3.17 | (367) ~ (all_0_126_126 = e20) % 11.78/3.17 | % 11.78/3.17 +-Applying beta-rule and splitting (167), into two cases. % 11.78/3.17 |-Branch one: % 11.78/3.17 | (388) all_0_117_117 = e23 % 11.78/3.17 | % 11.78/3.17 | Equations (388) can reduce 23 to: % 11.78/3.17 | (389) ~ (all_0_119_119 = e23) % 11.78/3.17 | % 11.78/3.17 | Simplifying 389 yields: % 11.78/3.17 | (390) ~ (all_0_119_119 = e23) % 11.78/3.17 | % 11.78/3.17 +-Applying beta-rule and splitting (64), into two cases. % 11.78/3.17 |-Branch one: % 11.78/3.17 | (391) all_0_119_119 = e20 % 11.78/3.17 | % 11.78/3.17 | Equations (391) can reduce 169 to: % 11.78/3.17 | (382) ~ (all_0_120_120 = e20) % 11.78/3.17 | % 11.78/3.17 | Simplifying 382 yields: % 11.78/3.17 | (383) ~ (all_0_120_120 = e20) % 11.78/3.17 | % 11.78/3.17 | Equations (391) can reduce 227 to: % 11.78/3.17 | (394) ~ (all_0_121_121 = e20) % 11.78/3.17 | % 11.78/3.17 | Simplifying 394 yields: % 11.78/3.17 | (366) ~ (all_0_121_121 = e20) % 11.78/3.17 | % 11.78/3.17 | Equations (391) can reduce 390 to: % 11.78/3.17 | (368) ~ (e23 = e20) % 11.78/3.17 | % 11.78/3.17 | Simplifying 368 yields: % 11.78/3.17 | (266) ~ (e23 = e20) % 11.78/3.17 | % 11.78/3.17 +-Applying beta-rule and splitting (84), into two cases. % 11.78/3.17 |-Branch one: % 11.78/3.17 | (398) all_0_126_126 = e20 % 11.78/3.17 | % 11.78/3.17 | Equations (398) can reduce 367 to: % 11.78/3.17 | (399) $false % 11.78/3.18 | % 11.82/3.18 |-The branch is then unsatisfiable % 11.82/3.18 |-Branch two: % 11.82/3.18 | (367) ~ (all_0_126_126 = e20) % 11.82/3.18 | (401) all_0_118_118 = e23 | all_0_123_123 = e21 % 11.82/3.18 | % 11.82/3.18 +-Applying beta-rule and splitting (401), into two cases. % 11.82/3.18 |-Branch one: % 11.82/3.18 | (402) all_0_118_118 = e23 % 11.82/3.18 | % 11.82/3.18 | Combining equations (402,381) yields a new equation: % 11.82/3.18 | (403) e23 = e20 % 11.82/3.18 | % 11.82/3.18 | Simplifying 403 yields: % 11.82/3.18 | (404) e23 = e20 % 11.82/3.18 | % 11.82/3.18 | Equations (404) can reduce 266 to: % 11.82/3.18 | (399) $false % 11.82/3.18 | % 11.82/3.18 |-The branch is then unsatisfiable % 11.82/3.18 |-Branch two: % 11.82/3.18 | (406) ~ (all_0_118_118 = e23) % 11.82/3.18 | (407) all_0_123_123 = e21 % 11.82/3.18 | % 11.82/3.18 | Equations (407) can reduce 66 to: % 11.82/3.18 | (408) ~ (all_0_120_120 = e21) % 11.82/3.18 | % 11.82/3.18 | Equations (407) can reduce 260 to: % 11.82/3.18 | (409) ~ (all_0_124_124 = e21) % 11.82/3.18 | % 11.82/3.18 | Simplifying 409 yields: % 11.82/3.18 | (410) ~ (all_0_124_124 = e21) % 11.82/3.18 | % 11.82/3.18 | Equations (407) can reduce 81 to: % 11.82/3.18 | (320) ~ (e21 = e20) % 11.82/3.18 | % 11.82/3.18 +-Applying beta-rule and splitting (62), into two cases. % 11.82/3.18 |-Branch one: % 11.82/3.18 | (412) all_0_120_120 = e20 % 11.82/3.18 | % 11.82/3.18 | Equations (412) can reduce 383 to: % 11.82/3.18 | (399) $false % 11.82/3.18 | % 11.82/3.18 |-The branch is then unsatisfiable % 11.82/3.18 |-Branch two: % 11.82/3.18 | (383) ~ (all_0_120_120 = e20) % 11.82/3.18 | (415) all_0_120_120 = e23 | all_0_120_120 = e21 % 11.82/3.18 | % 11.82/3.18 +-Applying beta-rule and splitting (415), into two cases. % 11.82/3.18 |-Branch one: % 11.82/3.18 | (416) all_0_120_120 = e23 % 11.82/3.18 | % 11.82/3.18 | Equations (416) can reduce 306 to: % 11.82/3.18 | (417) ~ (all_0_121_121 = e23) % 11.82/3.18 | % 11.82/3.18 | Simplifying 417 yields: % 11.82/3.18 | (418) ~ (all_0_121_121 = e23) % 11.82/3.18 | % 11.82/3.18 +-Applying beta-rule and splitting (296), into two cases. % 11.82/3.18 |-Branch one: % 11.82/3.18 | (419) all_0_121_121 = e23 % 11.82/3.18 | % 11.82/3.18 | Equations (419) can reduce 418 to: % 11.82/3.18 | (399) $false % 11.82/3.18 | % 11.82/3.18 |-The branch is then unsatisfiable % 11.82/3.18 |-Branch two: % 11.82/3.18 | (418) ~ (all_0_121_121 = e23) % 11.82/3.18 | (422) all_0_124_124 = e23 % 11.82/3.18 | % 11.82/3.18 | Equations (422) can reduce 410 to: % 11.82/3.18 | (278) ~ (e23 = e21) % 11.82/3.18 | % 11.82/3.18 +-Applying beta-rule and splitting (328), into two cases. % 11.82/3.18 |-Branch one: % 11.82/3.18 | (424) all_0_123_123 = e22 % 11.82/3.18 | % 11.82/3.18 | Combining equations (407,424) yields a new equation: % 11.82/3.18 | (425) e22 = e21 % 11.82/3.18 | % 11.82/3.18 | Equations (425) can reduce 249 to: % 11.82/3.18 | (399) $false % 11.82/3.18 | % 11.82/3.18 |-The branch is then unsatisfiable % 11.82/3.18 |-Branch two: % 11.82/3.18 | (427) ~ (all_0_123_123 = e22) % 11.82/3.18 | (428) all_0_126_126 = e22 % 11.82/3.18 | % 11.82/3.18 | Equations (428) can reduce 10 to: % 11.82/3.18 | (429) ~ (all_0_125_125 = e22) % 11.82/3.18 | % 11.82/3.18 +-Applying beta-rule and splitting (312), into two cases. % 11.82/3.18 |-Branch one: % 11.82/3.18 | (430) all_0_122_122 = e22 % 11.82/3.18 | % 11.82/3.18 +-Applying beta-rule and splitting (54), into two cases. % 11.82/3.18 |-Branch one: % 11.82/3.18 | (431) all_0_121_121 = e21 % 11.82/3.18 | % 11.82/3.18 | Equations (431) can reduce 13 to: % 11.82/3.18 | (432) ~ (e22 = e21) % 11.82/3.18 | % 11.82/3.18 | Simplifying 432 yields: % 11.82/3.18 | (249) ~ (e22 = e21) % 11.82/3.18 | % 11.82/3.18 | Equations (431) can reduce 366 to: % 11.82/3.18 | (320) ~ (e21 = e20) % 11.82/3.18 | % 11.82/3.18 +-Applying beta-rule and splitting (226), into two cases. % 11.82/3.18 |-Branch one: % 11.82/3.18 | (435) all_0_125_125 = e21 % 11.82/3.18 | % 11.82/3.18 +-Applying beta-rule and splitting (247), into two cases. % 11.82/3.18 |-Branch one: % 11.82/3.18 | (436) all_0_135_135 = e11 % 11.82/3.18 | % 11.82/3.18 | Equations (436) can reduce 177 to: % 11.82/3.18 | (437) ~ (all_0_133_133 = e11) % 11.82/3.18 | % 11.82/3.18 | Equations (436) can reduce 40 to: % 11.82/3.18 | (438) ~ (all_0_134_134 = e11) % 11.82/3.18 | % 11.82/3.18 +-Applying beta-rule and splitting (178), into two cases. % 11.82/3.18 |-Branch one: % 11.82/3.18 | (439) all_0_132_132 = e13 % 11.82/3.18 | % 11.82/3.18 +-Applying beta-rule and splitting (4), into two cases. % 11.82/3.18 |-Branch one: % 11.82/3.18 | (440) all_0_132_132 = e10 % 11.82/3.18 | % 11.82/3.18 | Combining equations (439,440) yields a new equation: % 11.82/3.18 | (441) e13 = e10 % 11.82/3.18 | % 11.82/3.18 | Simplifying 441 yields: % 11.82/3.18 | (442) e13 = e10 % 11.82/3.18 | % 11.82/3.18 | Equations (442) can reduce 197 to: % 11.82/3.18 | (399) $false % 11.82/3.18 | % 11.82/3.18 |-The branch is then unsatisfiable % 11.82/3.18 |-Branch two: % 11.82/3.18 | (444) ~ (all_0_132_132 = e10) % 11.82/3.18 | (445) all_0_138_138 = e10 % 11.82/3.18 | % 11.82/3.18 | Equations (445) can reduce 164 to: % 11.82/3.18 | (446) ~ (all_0_137_137 = e10) % 11.82/3.18 | % 11.82/3.18 +-Applying beta-rule and splitting (55), into two cases. % 11.82/3.18 |-Branch one: % 11.82/3.18 | (447) all_0_133_133 = e11 % 11.82/3.18 | % 11.82/3.18 | Equations (447) can reduce 437 to: % 11.82/3.18 | (399) $false % 11.82/3.18 | % 11.82/3.18 |-The branch is then unsatisfiable % 11.82/3.18 |-Branch two: % 11.82/3.18 | (437) ~ (all_0_133_133 = e11) % 11.82/3.18 | (450) all_0_128_128 = e13 | all_0_136_136 = e10 % 11.82/3.18 | % 11.82/3.18 +-Applying beta-rule and splitting (33), into two cases. % 11.82/3.18 |-Branch one: % 11.82/3.18 | (451) all_0_134_134 = e11 % 11.82/3.18 | % 11.82/3.18 | Equations (451) can reduce 438 to: % 11.82/3.18 | (399) $false % 11.82/3.18 | % 11.82/3.18 |-The branch is then unsatisfiable % 11.82/3.18 |-Branch two: % 11.82/3.18 | (438) ~ (all_0_134_134 = e11) % 11.82/3.18 | (454) all_0_129_129 = e13 | all_0_137_137 = e10 % 11.82/3.18 | % 11.82/3.18 +-Applying beta-rule and splitting (454), into two cases. % 11.82/3.18 |-Branch one: % 11.82/3.18 | (455) all_0_129_129 = e13 % 11.82/3.18 | % 11.82/3.18 | Equations (455) can reduce 37 to: % 11.82/3.18 | (456) ~ (all_0_134_134 = e13) % 11.82/3.18 | % 11.82/3.18 | Simplifying 456 yields: % 11.82/3.18 | (457) ~ (all_0_134_134 = e13) % 11.82/3.18 | % 11.82/3.18 | Equations (455) can reduce 319 to: % 11.82/3.18 | (287) ~ (e13 = e12) % 11.82/3.18 | % 11.82/3.18 | Equations (455) can reduce 61 to: % 11.82/3.18 | (343) ~ (e13 = e11) % 11.82/3.18 | % 11.82/3.18 +-Applying beta-rule and splitting (156), into two cases. % 11.82/3.18 |-Branch one: % 11.82/3.18 | (460) all_0_133_133 = e13 % 11.82/3.18 | % 11.82/3.18 | Equations (460) can reduce 259 to: % 11.82/3.18 | (461) ~ (all_0_128_128 = e13) % 11.82/3.18 | % 11.82/3.18 | Equations (460) can reduce 154 to: % 11.82/3.18 | (197) ~ (e13 = e10) % 11.82/3.18 | % 11.82/3.18 +-Applying beta-rule and splitting (342), into two cases. % 11.82/3.18 |-Branch one: % 11.82/3.18 | (463) all_0_128_128 = e10 % 11.82/3.18 | % 11.82/3.18 | Equations (463) can reduce 461 to: % 11.82/3.18 | (464) ~ (e13 = e10) % 11.82/3.18 | % 11.82/3.18 | Simplifying 464 yields: % 11.82/3.18 | (197) ~ (e13 = e10) % 11.82/3.18 | % 11.82/3.18 +-Applying beta-rule and splitting (49), into two cases. % 11.82/3.18 |-Branch one: % 11.82/3.18 | (466) all_0_133_133 = e12 % 11.82/3.18 | % 11.82/3.18 | Combining equations (460,466) yields a new equation: % 11.82/3.18 | (467) e13 = e12 % 11.82/3.18 | % 11.82/3.18 | Simplifying 467 yields: % 11.82/3.18 | (468) e13 = e12 % 11.82/3.18 | % 11.82/3.18 | Equations (468) can reduce 287 to: % 11.82/3.18 | (399) $false % 11.82/3.18 | % 11.82/3.18 |-The branch is then unsatisfiable % 11.82/3.18 |-Branch two: % 11.82/3.18 | (470) ~ (all_0_133_133 = e12) % 11.82/3.18 | (471) all_0_136_136 = e12 % 11.82/3.18 | % 11.82/3.18 | Equations (471) can reduce 159 to: % 11.82/3.18 | (472) ~ (all_0_137_137 = e12) % 11.82/3.18 | % 11.82/3.18 | Simplifying 472 yields: % 11.82/3.18 | (473) ~ (all_0_137_137 = e12) % 11.82/3.18 | % 11.82/3.18 +-Applying beta-rule and splitting (294), into two cases. % 11.82/3.18 |-Branch one: % 11.82/3.18 | (474) all_0_134_134 = e12 % 11.82/3.18 | % 11.82/3.18 | Equations (474) can reduce 200 to: % 11.82/3.18 | (160) ~ (e12 = e10) % 11.82/3.18 | % 11.82/3.18 +-Applying beta-rule and splitting (450), into two cases. % 11.82/3.18 |-Branch one: % 11.82/3.18 | (476) all_0_128_128 = e13 % 11.82/3.18 | % 11.82/3.18 | Combining equations (463,476) yields a new equation: % 11.82/3.18 | (442) e13 = e10 % 11.82/3.18 | % 11.82/3.18 | Equations (442) can reduce 197 to: % 11.82/3.18 | (399) $false % 11.82/3.18 | % 11.82/3.18 |-The branch is then unsatisfiable % 11.82/3.18 |-Branch two: % 11.82/3.18 | (461) ~ (all_0_128_128 = e13) % 11.82/3.18 | (480) all_0_136_136 = e10 % 11.82/3.18 | % 11.82/3.18 | Combining equations (471,480) yields a new equation: % 11.82/3.18 | (481) e12 = e10 % 11.82/3.18 | % 11.82/3.18 | Simplifying 481 yields: % 11.82/3.19 | (482) e12 = e10 % 11.82/3.19 | % 11.82/3.19 | Equations (482) can reduce 160 to: % 11.82/3.19 | (399) $false % 11.82/3.19 | % 11.82/3.19 |-The branch is then unsatisfiable % 11.82/3.19 |-Branch two: % 11.82/3.19 | (484) ~ (all_0_134_134 = e12) % 11.82/3.19 | (485) all_0_137_137 = e12 % 11.82/3.19 | % 11.82/3.19 | Equations (485) can reduce 473 to: % 11.82/3.19 | (399) $false % 11.82/3.19 | % 11.82/3.19 |-The branch is then unsatisfiable % 11.82/3.19 |-Branch two: % 11.82/3.19 | (487) ~ (all_0_128_128 = e10) % 11.82/3.19 | (488) all_0_129_129 = e10 % 11.82/3.19 | % 11.82/3.19 | Combining equations (455,488) yields a new equation: % 11.82/3.19 | (441) e13 = e10 % 11.82/3.19 | % 11.82/3.19 | Simplifying 441 yields: % 11.82/3.19 | (442) e13 = e10 % 11.82/3.19 | % 11.82/3.19 | Equations (442) can reduce 197 to: % 11.82/3.19 | (399) $false % 11.82/3.19 | % 11.82/3.19 |-The branch is then unsatisfiable % 11.82/3.19 |-Branch two: % 11.82/3.19 | (492) ~ (all_0_133_133 = e13) % 11.82/3.19 | (493) all_0_134_134 = e13 | all_0_135_135 = e13 % 11.82/3.19 | % 11.82/3.19 +-Applying beta-rule and splitting (493), into two cases. % 11.82/3.19 |-Branch one: % 11.82/3.19 | (494) all_0_134_134 = e13 % 11.82/3.19 | % 11.82/3.19 | Equations (494) can reduce 457 to: % 11.82/3.19 | (399) $false % 11.82/3.19 | % 11.82/3.19 |-The branch is then unsatisfiable % 11.82/3.19 |-Branch two: % 11.82/3.19 | (457) ~ (all_0_134_134 = e13) % 11.82/3.19 | (497) all_0_135_135 = e13 % 11.82/3.19 | % 11.82/3.19 | Combining equations (436,497) yields a new equation: % 11.82/3.19 | (498) e13 = e11 % 11.82/3.19 | % 11.82/3.19 | Equations (498) can reduce 343 to: % 11.82/3.19 | (399) $false % 11.82/3.19 | % 11.82/3.19 |-The branch is then unsatisfiable % 11.82/3.19 |-Branch two: % 11.82/3.19 | (500) ~ (all_0_129_129 = e13) % 11.82/3.19 | (501) all_0_137_137 = e10 % 11.82/3.19 | % 11.82/3.19 | Equations (501) can reduce 446 to: % 11.82/3.19 | (399) $false % 11.82/3.19 | % 11.82/3.19 |-The branch is then unsatisfiable % 11.82/3.19 |-Branch two: % 11.82/3.19 | (503) ~ (all_0_132_132 = e13) % 11.82/3.19 | (497) all_0_135_135 = e13 % 11.82/3.19 | % 11.82/3.19 | Combining equations (497,436) yields a new equation: % 11.82/3.19 | (505) e13 = e11 % 11.82/3.19 | % 11.82/3.19 | Simplifying 505 yields: % 11.82/3.19 | (498) e13 = e11 % 11.82/3.19 | % 11.82/3.19 | Equations (498) can reduce 343 to: % 11.82/3.19 | (399) $false % 11.82/3.19 | % 11.82/3.19 |-The branch is then unsatisfiable % 11.82/3.19 |-Branch two: % 11.82/3.19 | (508) ~ (all_0_135_135 = e11) % 11.82/3.19 | (445) all_0_138_138 = e10 % 11.82/3.19 | % 11.82/3.19 | Equations (445) can reduce 97 to: % 11.82/3.19 | (444) ~ (all_0_132_132 = e10) % 11.82/3.19 | % 11.82/3.19 | Equations (445) can reduce 341 to: % 11.82/3.19 | (511) ~ (all_0_136_136 = e10) % 11.82/3.19 | % 11.82/3.19 | From (445) and (217) follows: % 11.82/3.19 | (512) op1(e10, e10) = all_0_116_116 % 11.82/3.19 | % 11.82/3.19 | From (445) and (136) follows: % 11.82/3.19 | (513) op1(e10, e10) = e10 % 11.82/3.19 | % 11.82/3.19 | From (445) and (277) follows: % 11.82/3.19 | (514) h2(e10) = all_0_62_62 % 11.82/3.19 | % 11.82/3.19 +-Applying beta-rule and splitting (39), into two cases. % 11.82/3.19 |-Branch one: % 11.82/3.19 | (436) all_0_135_135 = e11 % 11.82/3.19 | % 11.82/3.19 | Equations (436) can reduce 508 to: % 11.82/3.19 | (399) $false % 11.82/3.19 | % 11.82/3.19 |-The branch is then unsatisfiable % 11.82/3.19 |-Branch two: % 11.82/3.19 | (508) ~ (all_0_135_135 = e11) % 11.82/3.19 | (497) all_0_135_135 = e13 % 11.82/3.19 | % 11.82/3.19 | Equations (497) can reduce 318 to: % 11.82/3.19 | (503) ~ (all_0_132_132 = e13) % 11.82/3.19 | % 11.82/3.19 | From (497) and (191) follows: % 11.82/3.19 | (520) h2(e13) = all_0_59_59 % 11.82/3.19 | % 11.82/3.19 +-Applying beta-rule and splitting (132), into two cases. % 11.82/3.19 |-Branch one: % 11.82/3.19 | (521) all_0_132_132 = e11 % 11.82/3.19 | % 11.82/3.19 | Equations (521) can reduce 344 to: % 11.82/3.19 | (522) ~ (all_0_130_130 = e11) % 11.82/3.19 | % 11.82/3.19 | Equations (521) can reduce 258 to: % 11.82/3.19 | (523) ~ (e12 = e11) % 11.82/3.19 | % 11.82/3.19 | Simplifying 523 yields: % 11.82/3.19 | (304) ~ (e12 = e11) % 11.82/3.19 | % 11.82/3.19 | From (521) and (284) follows: % 11.82/3.19 | (525) h2(e11) = all_0_56_56 % 11.82/3.19 | % 11.82/3.19 | Instantiating formula (316) with e10, e10, e10, all_0_116_116 and discharging atoms op1(e10, e10) = all_0_116_116, op1(e10, e10) = e10, yields: % 11.82/3.19 | (526) all_0_116_116 = e10 % 11.82/3.19 | % 11.82/3.19 | Instantiating formula (269) with e13, all_0_59_59, e23 and discharging atoms h2(e13) = all_0_59_59, h2(e13) = e23, yields: % 11.82/3.19 | (527) all_0_59_59 = e23 % 11.82/3.19 | % 11.82/3.19 | Instantiating formula (269) with e11, all_0_56_56, e21 and discharging atoms h2(e11) = all_0_56_56, h2(e11) = e21, yields: % 11.82/3.19 | (528) all_0_56_56 = e21 % 11.82/3.19 | % 11.82/3.19 | Instantiating formula (269) with e10, all_0_62_62, e20 and discharging atoms h2(e10) = all_0_62_62, h2(e10) = e20, yields: % 11.82/3.19 | (529) all_0_62_62 = e20 % 11.82/3.19 | % 11.82/3.19 | From (527) and (520) follows: % 11.82/3.19 | (173) h2(e13) = e23 % 11.82/3.19 | % 11.82/3.19 | From (528) and (525) follows: % 11.82/3.19 | (87) h2(e11) = e21 % 11.82/3.19 | % 11.82/3.19 | From (529) and (514) follows: % 11.82/3.19 | (100) h2(e10) = e20 % 11.82/3.19 | % 11.82/3.19 +-Applying beta-rule and splitting (119), into two cases. % 11.82/3.19 |-Branch one: % 11.82/3.19 | (455) all_0_129_129 = e13 % 11.82/3.19 | % 11.82/3.19 | Equations (455) can reduce 203 to: % 11.82/3.19 | (461) ~ (all_0_128_128 = e13) % 11.82/3.19 | % 11.82/3.19 +-Applying beta-rule and splitting (71), into two cases. % 11.82/3.19 |-Branch one: % 11.82/3.19 | (476) all_0_128_128 = e13 % 11.82/3.19 | % 11.82/3.19 | Equations (476) can reduce 461 to: % 11.82/3.19 | (399) $false % 11.82/3.19 | % 11.82/3.19 |-The branch is then unsatisfiable % 11.82/3.19 |-Branch two: % 11.82/3.19 | (461) ~ (all_0_128_128 = e13) % 11.82/3.19 | (538) all_0_130_130 = e13 | all_0_133_133 = e13 % 11.82/3.19 | % 11.82/3.19 +-Applying beta-rule and splitting (310), into two cases. % 11.82/3.19 |-Branch one: % 11.82/3.19 | (476) all_0_128_128 = e13 % 11.82/3.19 | % 11.82/3.19 | Equations (476) can reduce 461 to: % 11.82/3.19 | (399) $false % 11.82/3.19 | % 11.82/3.19 |-The branch is then unsatisfiable % 11.82/3.19 |-Branch two: % 11.82/3.19 | (461) ~ (all_0_128_128 = e13) % 11.82/3.19 | (463) all_0_128_128 = e10 % 11.82/3.19 | % 11.82/3.19 | Equations (463) can reduce 335 to: % 11.82/3.19 | (543) ~ (all_0_130_130 = e10) % 11.82/3.19 | % 11.82/3.19 | Simplifying 543 yields: % 11.82/3.19 | (544) ~ (all_0_130_130 = e10) % 11.82/3.19 | % 11.82/3.19 | Equations (463) can reduce 162 to: % 11.82/3.19 | (545) ~ (all_0_136_136 = e10) % 11.82/3.19 | % 11.82/3.19 | Simplifying 545 yields: % 11.82/3.19 | (511) ~ (all_0_136_136 = e10) % 11.82/3.19 | % 11.82/3.19 +-Applying beta-rule and splitting (176), into two cases. % 11.82/3.19 |-Branch one: % 11.82/3.19 | (547) all_0_130_130 = e11 % 11.82/3.19 | % 11.82/3.19 | Equations (547) can reduce 522 to: % 11.82/3.19 | (399) $false % 11.82/3.19 | % 11.82/3.19 |-The branch is then unsatisfiable % 11.82/3.19 |-Branch two: % 11.82/3.19 | (522) ~ (all_0_130_130 = e11) % 11.82/3.19 | (550) all_0_130_130 = e13 | all_0_130_130 = e10 % 11.82/3.19 | % 11.82/3.19 +-Applying beta-rule and splitting (108), into two cases. % 11.82/3.19 |-Branch one: % 11.82/3.19 | (551) all_0_130_130 = e13 % 11.82/3.19 | % 11.82/3.19 | Equations (551) can reduce 544 to: % 11.82/3.19 | (197) ~ (e13 = e10) % 11.82/3.19 | % 11.82/3.19 | From (551) and (326) follows: % 11.82/3.19 | (553) op1(e12, e13) = all_0_108_108 % 11.82/3.19 | % 11.82/3.19 | From (551) and (351) follows: % 11.82/3.19 | (554) op1(e12, e13) = e13 % 11.82/3.19 | % 11.82/3.19 +-Applying beta-rule and splitting (55), into two cases. % 11.82/3.19 |-Branch one: % 11.82/3.19 | (447) all_0_133_133 = e11 % 11.82/3.19 | % 11.82/3.19 +-Applying beta-rule and splitting (49), into two cases. % 11.82/3.19 |-Branch one: % 11.82/3.19 | (466) all_0_133_133 = e12 % 11.82/3.19 | % 11.82/3.19 | Combining equations (466,447) yields a new equation: % 11.82/3.19 | (557) e12 = e11 % 11.82/3.20 | % 11.82/3.20 | Simplifying 557 yields: % 11.82/3.20 | (558) e12 = e11 % 11.82/3.20 | % 11.82/3.20 | Equations (558) can reduce 304 to: % 11.82/3.20 | (399) $false % 11.82/3.20 | % 11.82/3.20 |-The branch is then unsatisfiable % 11.82/3.20 |-Branch two: % 11.82/3.20 | (470) ~ (all_0_133_133 = e12) % 11.82/3.20 | (471) all_0_136_136 = e12 % 11.82/3.20 | % 11.82/3.20 | Equations (471) can reduce 159 to: % 11.82/3.20 | (472) ~ (all_0_137_137 = e12) % 11.82/3.20 | % 11.82/3.20 | Simplifying 472 yields: % 11.82/3.20 | (473) ~ (all_0_137_137 = e12) % 11.82/3.20 | % 11.82/3.20 +-Applying beta-rule and splitting (294), into two cases. % 11.82/3.20 |-Branch one: % 11.82/3.20 | (474) all_0_134_134 = e12 % 11.82/3.20 | % 11.82/3.20 | From (474) and (275) follows: % 11.82/3.20 | (565) op1(e11, e12) = all_0_112_112 % 11.82/3.20 | % 11.82/3.20 | From (474) and (128) follows: % 11.82/3.20 | (566) op1(e11, e12) = e12 % 11.82/3.20 | % 11.82/3.20 | Instantiating formula (316) with e12, e13, e13, all_0_108_108 and discharging atoms op1(e12, e13) = all_0_108_108, op1(e12, e13) = e13, yields: % 11.82/3.20 | (567) all_0_108_108 = e13 % 11.82/3.20 | % 11.82/3.20 | Instantiating formula (316) with e11, e12, e12, all_0_112_112 and discharging atoms op1(e11, e12) = all_0_112_112, op1(e11, e12) = e12, yields: % 11.82/3.20 | (568) all_0_112_112 = e12 % 11.82/3.20 | % 11.82/3.20 +-Applying beta-rule and splitting (95), into two cases. % 11.82/3.20 |-Branch one: % 11.82/3.20 | (569) ( ~ (all_0_108_108 = e13) & ~ (all_0_109_109 = e12) & ~ (all_0_110_110 = e10) & ~ (all_0_131_131 = e11)) | ( ~ (all_0_111_111 = e13) & ~ (all_0_112_112 = e12) & ~ (all_0_113_113 = e10) & ~ (all_0_135_135 = e11)) % 11.82/3.20 | % 11.82/3.20 +-Applying beta-rule and splitting (569), into two cases. % 11.82/3.20 |-Branch one: % 11.82/3.20 | (570) ~ (all_0_108_108 = e13) & ~ (all_0_109_109 = e12) & ~ (all_0_110_110 = e10) & ~ (all_0_131_131 = e11) % 11.82/3.20 | % 11.82/3.20 | Applying alpha-rule on (570) yields: % 11.82/3.20 | (571) ~ (all_0_108_108 = e13) % 11.82/3.20 | (572) ~ (all_0_109_109 = e12) % 11.82/3.20 | (573) ~ (all_0_110_110 = e10) % 11.82/3.20 | (574) ~ (all_0_131_131 = e11) % 11.82/3.20 | % 11.82/3.20 | Equations (567) can reduce 571 to: % 11.82/3.20 | (399) $false % 11.82/3.20 | % 11.82/3.20 |-The branch is then unsatisfiable % 11.82/3.20 |-Branch two: % 11.82/3.20 | (576) ~ (all_0_111_111 = e13) & ~ (all_0_112_112 = e12) & ~ (all_0_113_113 = e10) & ~ (all_0_135_135 = e11) % 11.82/3.20 | % 11.82/3.20 | Applying alpha-rule on (576) yields: % 11.82/3.20 | (577) ~ (all_0_111_111 = e13) % 11.82/3.20 | (578) ~ (all_0_112_112 = e12) % 11.82/3.20 | (579) ~ (all_0_113_113 = e10) % 11.82/3.20 | (508) ~ (all_0_135_135 = e11) % 11.82/3.20 | % 11.82/3.20 | Equations (568) can reduce 578 to: % 11.82/3.20 | (399) $false % 11.82/3.20 | % 11.82/3.20 |-The branch is then unsatisfiable % 11.82/3.20 |-Branch two: % 11.82/3.20 | (582) ~ (all_0_114_114 = e13) & ~ (all_0_115_115 = e12) & ~ (all_0_116_116 = e10) & ~ (all_0_136_136 = e11) % 11.82/3.20 | % 11.82/3.20 | Applying alpha-rule on (582) yields: % 11.82/3.20 | (583) ~ (all_0_114_114 = e13) % 11.82/3.20 | (584) ~ (all_0_115_115 = e12) % 11.82/3.20 | (585) ~ (all_0_116_116 = e10) % 11.82/3.20 | (586) ~ (all_0_136_136 = e11) % 11.82/3.20 | % 11.82/3.20 | Equations (526) can reduce 585 to: % 11.82/3.20 | (399) $false % 11.82/3.20 | % 11.82/3.20 |-The branch is then unsatisfiable % 11.82/3.20 |-Branch two: % 11.82/3.20 | (484) ~ (all_0_134_134 = e12) % 11.82/3.20 | (485) all_0_137_137 = e12 % 11.82/3.20 | % 11.82/3.20 | Equations (485) can reduce 473 to: % 11.82/3.20 | (399) $false % 11.82/3.20 | % 11.82/3.20 |-The branch is then unsatisfiable % 11.82/3.20 |-Branch two: % 11.82/3.20 | (437) ~ (all_0_133_133 = e11) % 11.82/3.20 | (450) all_0_128_128 = e13 | all_0_136_136 = e10 % 11.82/3.20 | % 11.82/3.20 +-Applying beta-rule and splitting (450), into two cases. % 11.82/3.20 |-Branch one: % 11.82/3.20 | (476) all_0_128_128 = e13 % 11.82/3.20 | % 11.82/3.20 | Combining equations (476,463) yields a new equation: % 11.82/3.20 | (441) e13 = e10 % 11.82/3.20 | % 11.82/3.20 | Simplifying 441 yields: % 11.82/3.20 | (442) e13 = e10 % 11.82/3.20 | % 11.82/3.20 | Equations (442) can reduce 197 to: % 11.82/3.20 | (399) $false % 11.82/3.20 | % 11.82/3.20 |-The branch is then unsatisfiable % 11.82/3.20 |-Branch two: % 11.82/3.20 | (461) ~ (all_0_128_128 = e13) % 11.82/3.20 | (480) all_0_136_136 = e10 % 11.82/3.20 | % 11.82/3.20 | Equations (480) can reduce 511 to: % 11.82/3.20 | (399) $false % 11.82/3.20 | % 11.82/3.20 |-The branch is then unsatisfiable % 11.82/3.20 |-Branch two: % 11.82/3.20 | (600) ~ (all_0_130_130 = e13) % 11.82/3.20 | (601) all_0_131_131 = e13 | all_0_132_132 = e13 % 11.82/3.20 | % 11.82/3.20 +-Applying beta-rule and splitting (550), into two cases. % 11.82/3.20 |-Branch one: % 11.82/3.20 | (551) all_0_130_130 = e13 % 11.82/3.20 | % 11.82/3.20 | Equations (551) can reduce 600 to: % 11.82/3.20 | (399) $false % 11.82/3.20 | % 11.82/3.20 |-The branch is then unsatisfiable % 11.82/3.20 |-Branch two: % 11.82/3.20 | (600) ~ (all_0_130_130 = e13) % 11.82/3.20 | (605) all_0_130_130 = e10 % 11.82/3.20 | % 11.82/3.20 | Equations (605) can reduce 544 to: % 11.82/3.20 | (399) $false % 11.82/3.20 | % 11.82/3.20 |-The branch is then unsatisfiable % 11.82/3.20 |-Branch two: % 11.82/3.20 | (500) ~ (all_0_129_129 = e13) % 11.82/3.20 | (488) all_0_129_129 = e10 % 11.82/3.20 | % 11.82/3.20 | Equations (488) can reduce 93 to: % 11.82/3.20 | (609) ~ (all_0_131_131 = e10) % 11.82/3.20 | % 11.82/3.20 | Simplifying 609 yields: % 11.82/3.20 | (610) ~ (all_0_131_131 = e10) % 11.82/3.20 | % 11.82/3.20 | Equations (488) can reduce 98 to: % 11.82/3.20 | (611) ~ (all_0_137_137 = e10) % 11.82/3.20 | % 11.82/3.20 | Simplifying 611 yields: % 11.82/3.20 | (446) ~ (all_0_137_137 = e10) % 11.82/3.20 | % 11.82/3.20 | Equations (488) can reduce 500 to: % 11.82/3.20 | (464) ~ (e13 = e10) % 11.82/3.20 | % 11.82/3.20 | Simplifying 464 yields: % 11.82/3.20 | (197) ~ (e13 = e10) % 11.82/3.20 | % 11.82/3.20 | From (488) and (353) follows: % 11.82/3.20 | (615) h2(e10) = all_0_53_53 % 11.82/3.20 | % 11.82/3.20 +-Applying beta-rule and splitting (28), into two cases. % 11.82/3.20 |-Branch one: % 11.82/3.20 | (476) all_0_128_128 = e13 % 11.82/3.20 | % 11.82/3.20 | Equations (476) can reduce 335 to: % 11.82/3.20 | (617) ~ (all_0_130_130 = e13) % 11.82/3.20 | % 11.82/3.20 | Simplifying 617 yields: % 11.82/3.20 | (600) ~ (all_0_130_130 = e13) % 11.82/3.20 | % 11.82/3.20 | Equations (476) can reduce 259 to: % 11.82/3.20 | (619) ~ (all_0_133_133 = e13) % 11.82/3.20 | % 11.82/3.20 | Simplifying 619 yields: % 11.82/3.20 | (492) ~ (all_0_133_133 = e13) % 11.82/3.20 | % 11.82/3.20 | Equations (476) can reduce 162 to: % 11.82/3.20 | (621) ~ (all_0_136_136 = e13) % 11.82/3.20 | % 11.82/3.20 | Simplifying 621 yields: % 11.82/3.20 | (215) ~ (all_0_136_136 = e13) % 11.82/3.20 | % 11.82/3.20 | Equations (476) can reduce 313 to: % 11.82/3.20 | (343) ~ (e13 = e11) % 11.82/3.20 | % 11.82/3.20 | From (476) and (117) follows: % 11.82/3.20 | (624) h2(e13) = all_0_52_52 % 11.82/3.20 | % 11.82/3.20 +-Applying beta-rule and splitting (176), into two cases. % 11.82/3.20 |-Branch one: % 11.82/3.20 | (547) all_0_130_130 = e11 % 11.82/3.20 | % 11.82/3.20 | Equations (547) can reduce 522 to: % 11.82/3.20 | (399) $false % 11.82/3.20 | % 11.82/3.20 |-The branch is then unsatisfiable % 11.82/3.20 |-Branch two: % 11.82/3.20 | (522) ~ (all_0_130_130 = e11) % 11.82/3.20 | (550) all_0_130_130 = e13 | all_0_130_130 = e10 % 11.82/3.20 | % 11.82/3.20 +-Applying beta-rule and splitting (33), into two cases. % 11.82/3.20 |-Branch one: % 11.82/3.20 | (451) all_0_134_134 = e11 % 11.82/3.20 | % 11.82/3.20 | Equations (451) can reduce 338 to: % 11.82/3.20 | (630) ~ (all_0_137_137 = e11) % 11.82/3.20 | % 11.82/3.20 | Simplifying 630 yields: % 11.82/3.20 | (631) ~ (all_0_137_137 = e11) % 11.82/3.20 | % 11.82/3.20 | From (451) and (157) follows: % 11.82/3.20 | (632) h2(e11) = all_0_58_58 % 11.82/3.20 | % 11.82/3.20 +-Applying beta-rule and splitting (74), into two cases. % 11.82/3.20 |-Branch one: % 11.82/3.20 | (633) all_0_137_137 = e11 % 11.82/3.20 | % 11.82/3.20 | Equations (633) can reduce 631 to: % 11.82/3.20 | (399) $false % 11.82/3.20 | % 11.82/3.20 |-The branch is then unsatisfiable % 11.82/3.20 |-Branch two: % 11.82/3.21 | (631) ~ (all_0_137_137 = e11) % 11.82/3.21 | (636) all_0_137_137 = e12 | all_0_137_137 = e10 % 11.82/3.21 | % 11.82/3.21 +-Applying beta-rule and splitting (294), into two cases. % 11.82/3.21 |-Branch one: % 11.82/3.21 | (474) all_0_134_134 = e12 % 11.82/3.21 | % 11.94/3.21 | Combining equations (474,451) yields a new equation: % 11.94/3.21 | (557) e12 = e11 % 11.94/3.21 | % 11.94/3.21 | Simplifying 557 yields: % 11.94/3.21 | (558) e12 = e11 % 11.94/3.21 | % 11.94/3.21 | Equations (558) can reduce 304 to: % 11.94/3.21 | (399) $false % 11.94/3.21 | % 11.94/3.21 |-The branch is then unsatisfiable % 11.94/3.21 |-Branch two: % 11.94/3.21 | (484) ~ (all_0_134_134 = e12) % 11.94/3.21 | (485) all_0_137_137 = e12 % 11.94/3.21 | % 11.94/3.21 | Equations (485) can reduce 631 to: % 11.94/3.21 | (304) ~ (e12 = e11) % 11.94/3.21 | % 11.94/3.21 | From (485) and (358) follows: % 11.94/3.21 | (644) h2(e12) = all_0_61_61 % 11.94/3.21 | % 11.94/3.21 +-Applying beta-rule and splitting (308), into two cases. % 11.94/3.21 |-Branch one: % 11.94/3.21 | (466) all_0_133_133 = e12 % 11.94/3.21 | % 11.94/3.21 | Equations (466) can reduce 262 to: % 11.94/3.21 | (646) ~ (all_0_136_136 = e12) % 11.94/3.21 | % 11.94/3.21 | Simplifying 646 yields: % 11.94/3.21 | (647) ~ (all_0_136_136 = e12) % 11.94/3.21 | % 11.94/3.21 | From (466) and (280) follows: % 11.94/3.21 | (648) h2(e12) = all_0_57_57 % 11.94/3.21 | % 11.94/3.21 +-Applying beta-rule and splitting (108), into two cases. % 11.94/3.21 |-Branch one: % 11.94/3.21 | (551) all_0_130_130 = e13 % 11.94/3.21 | % 11.94/3.21 | Equations (551) can reduce 600 to: % 11.94/3.21 | (399) $false % 11.94/3.21 | % 11.94/3.21 |-The branch is then unsatisfiable % 11.94/3.21 |-Branch two: % 11.94/3.21 | (600) ~ (all_0_130_130 = e13) % 11.94/3.21 | (601) all_0_131_131 = e13 | all_0_132_132 = e13 % 11.94/3.21 | % 11.94/3.21 +-Applying beta-rule and splitting (264), into two cases. % 11.94/3.21 |-Branch one: % 11.94/3.21 | (653) all_0_136_136 = e11 % 11.94/3.21 | % 11.94/3.21 | Equations (653) can reduce 215 to: % 11.94/3.21 | (654) ~ (e13 = e11) % 11.94/3.21 | % 11.94/3.21 | Simplifying 654 yields: % 11.94/3.21 | (343) ~ (e13 = e11) % 11.94/3.21 | % 11.94/3.21 | Equations (653) can reduce 511 to: % 11.94/3.21 | (292) ~ (e11 = e10) % 11.94/3.21 | % 11.94/3.21 | From (653) and (336) follows: % 11.94/3.21 | (657) h2(e11) = all_0_60_60 % 11.94/3.21 | % 11.94/3.21 +-Applying beta-rule and splitting (123), into two cases. % 11.94/3.21 |-Branch one: % 11.94/3.21 | (605) all_0_130_130 = e10 % 11.94/3.21 | % 11.94/3.21 | Equations (605) can reduce 600 to: % 11.94/3.21 | (464) ~ (e13 = e10) % 11.94/3.21 | % 11.94/3.21 | Simplifying 464 yields: % 11.94/3.21 | (197) ~ (e13 = e10) % 11.94/3.21 | % 11.94/3.21 | From (605) and (153) follows: % 11.94/3.21 | (661) h2(e10) = all_0_54_54 % 11.94/3.21 | % 11.94/3.21 +-Applying beta-rule and splitting (6), into two cases. % 11.94/3.21 |-Branch one: % 11.94/3.21 | (455) all_0_129_129 = e13 % 11.94/3.21 | % 11.94/3.21 | Combining equations (488,455) yields a new equation: % 11.94/3.21 | (442) e13 = e10 % 11.94/3.21 | % 11.94/3.21 | Equations (442) can reduce 197 to: % 11.94/3.21 | (399) $false % 11.94/3.21 | % 11.94/3.21 |-The branch is then unsatisfiable % 11.94/3.21 |-Branch two: % 11.94/3.21 | (500) ~ (all_0_129_129 = e13) % 11.94/3.21 | (666) all_0_131_131 = e13 | all_0_134_134 = e13 % 11.94/3.21 | % 11.94/3.21 +-Applying beta-rule and splitting (666), into two cases. % 11.94/3.21 |-Branch one: % 11.94/3.21 | (667) all_0_131_131 = e13 % 11.94/3.21 | % 11.94/3.21 | From (667) and (194) follows: % 11.94/3.21 | (668) h2(e13) = all_0_55_55 % 11.94/3.21 | % 11.94/3.21 | Instantiating formula (269) with e13, all_0_52_52, e23 and discharging atoms h2(e13) = all_0_52_52, h2(e13) = e23, yields: % 11.94/3.21 | (669) all_0_52_52 = e23 % 11.94/3.21 | % 11.94/3.21 | Instantiating formula (269) with e13, all_0_55_55, all_0_52_52 and discharging atoms h2(e13) = all_0_52_52, h2(e13) = all_0_55_55, yields: % 11.94/3.21 | (670) all_0_52_52 = all_0_55_55 % 11.94/3.21 | % 11.94/3.21 | Instantiating formula (269) with e12, all_0_57_57, e22 and discharging atoms h2(e12) = all_0_57_57, h2(e12) = e22, yields: % 11.94/3.21 | (671) all_0_57_57 = e22 % 11.94/3.21 | % 11.94/3.21 | Instantiating formula (269) with e12, all_0_61_61, all_0_57_57 and discharging atoms h2(e12) = all_0_57_57, h2(e12) = all_0_61_61, yields: % 11.94/3.21 | (672) all_0_57_57 = all_0_61_61 % 11.94/3.21 | % 11.94/3.21 | Instantiating formula (269) with e11, all_0_58_58, e21 and discharging atoms h2(e11) = all_0_58_58, h2(e11) = e21, yields: % 11.94/3.21 | (673) all_0_58_58 = e21 % 11.94/3.21 | % 11.94/3.21 | Instantiating formula (269) with e11, all_0_60_60, all_0_58_58 and discharging atoms h2(e11) = all_0_58_58, h2(e11) = all_0_60_60, yields: % 11.94/3.21 | (674) all_0_58_58 = all_0_60_60 % 11.94/3.21 | % 11.94/3.21 | Instantiating formula (269) with e10, all_0_53_53, e20 and discharging atoms h2(e10) = all_0_53_53, h2(e10) = e20, yields: % 11.94/3.21 | (675) all_0_53_53 = e20 % 11.94/3.21 | % 11.94/3.21 | Instantiating formula (269) with e10, all_0_54_54, all_0_53_53 and discharging atoms h2(e10) = all_0_53_53, h2(e10) = all_0_54_54, yields: % 11.94/3.21 | (676) all_0_53_53 = all_0_54_54 % 11.94/3.21 | % 11.94/3.21 | Combining equations (669,670) yields a new equation: % 11.94/3.21 | (677) all_0_55_55 = e23 % 11.94/3.21 | % 11.94/3.21 | Combining equations (675,676) yields a new equation: % 11.94/3.21 | (678) all_0_54_54 = e20 % 11.94/3.21 | % 11.94/3.21 | Combining equations (672,671) yields a new equation: % 11.94/3.21 | (679) all_0_61_61 = e22 % 11.94/3.21 | % 11.94/3.21 | Simplifying 679 yields: % 11.94/3.21 | (680) all_0_61_61 = e22 % 11.94/3.21 | % 11.94/3.21 | Combining equations (674,673) yields a new equation: % 11.94/3.21 | (681) all_0_60_60 = e21 % 11.94/3.21 | % 11.94/3.21 | Simplifying 681 yields: % 11.94/3.21 | (682) all_0_60_60 = e21 % 11.94/3.21 | % 11.94/3.21 | Combining equations (678,676) yields a new equation: % 11.94/3.21 | (675) all_0_53_53 = e20 % 11.94/3.21 | % 11.94/3.21 | Combining equations (677,670) yields a new equation: % 11.94/3.21 | (669) all_0_52_52 = e23 % 11.94/3.21 | % 11.94/3.21 +-Applying beta-rule and splitting (201), into two cases. % 11.94/3.21 |-Branch one: % 11.94/3.21 | (685) ~ (all_0_52_52 = all_0_117_117) % 11.94/3.21 | % 11.94/3.21 | Equations (669,388) can reduce 685 to: % 11.94/3.21 | (399) $false % 11.94/3.21 | % 11.94/3.21 |-The branch is then unsatisfiable % 11.94/3.21 |-Branch two: % 11.94/3.21 | (687) all_0_52_52 = all_0_117_117 % 11.94/3.21 | (688) ~ (all_0_53_53 = all_0_118_118) | ~ (all_0_54_54 = all_0_119_119) | ~ (all_0_55_55 = all_0_120_120) | ~ (all_0_56_56 = all_0_121_121) | ~ (all_0_57_57 = all_0_122_122) | ~ (all_0_58_58 = all_0_123_123) | ~ (all_0_59_59 = all_0_124_124) | ~ (all_0_60_60 = all_0_125_125) | ~ (all_0_61_61 = all_0_126_126) | ~ (all_0_62_62 = all_0_127_127) % 11.94/3.21 | % 11.94/3.21 +-Applying beta-rule and splitting (688), into two cases. % 11.94/3.21 |-Branch one: % 11.94/3.21 | (689) ~ (all_0_53_53 = all_0_118_118) % 11.94/3.21 | % 11.94/3.21 | Equations (675,381) can reduce 689 to: % 11.94/3.21 | (399) $false % 11.94/3.21 | % 11.94/3.21 |-The branch is then unsatisfiable % 11.94/3.21 |-Branch two: % 11.94/3.21 | (691) all_0_53_53 = all_0_118_118 % 11.94/3.21 | (692) ~ (all_0_54_54 = all_0_119_119) | ~ (all_0_55_55 = all_0_120_120) | ~ (all_0_56_56 = all_0_121_121) | ~ (all_0_57_57 = all_0_122_122) | ~ (all_0_58_58 = all_0_123_123) | ~ (all_0_59_59 = all_0_124_124) | ~ (all_0_60_60 = all_0_125_125) | ~ (all_0_61_61 = all_0_126_126) | ~ (all_0_62_62 = all_0_127_127) % 11.94/3.21 | % 11.94/3.21 +-Applying beta-rule and splitting (692), into two cases. % 11.94/3.21 |-Branch one: % 11.94/3.21 | (693) ~ (all_0_54_54 = all_0_119_119) % 11.94/3.21 | % 11.94/3.21 | Equations (678,391) can reduce 693 to: % 11.94/3.21 | (399) $false % 11.94/3.21 | % 11.94/3.21 |-The branch is then unsatisfiable % 11.94/3.21 |-Branch two: % 11.94/3.21 | (695) all_0_54_54 = all_0_119_119 % 11.94/3.22 | (696) ~ (all_0_55_55 = all_0_120_120) | ~ (all_0_56_56 = all_0_121_121) | ~ (all_0_57_57 = all_0_122_122) | ~ (all_0_58_58 = all_0_123_123) | ~ (all_0_59_59 = all_0_124_124) | ~ (all_0_60_60 = all_0_125_125) | ~ (all_0_61_61 = all_0_126_126) | ~ (all_0_62_62 = all_0_127_127) % 11.94/3.22 | % 11.94/3.22 +-Applying beta-rule and splitting (696), into two cases. % 11.94/3.22 |-Branch one: % 11.94/3.22 | (697) ~ (all_0_55_55 = all_0_120_120) % 11.94/3.22 | % 11.94/3.22 | Equations (677,416) can reduce 697 to: % 11.94/3.22 | (399) $false % 11.94/3.22 | % 11.94/3.22 |-The branch is then unsatisfiable % 11.94/3.22 |-Branch two: % 11.94/3.22 | (699) all_0_55_55 = all_0_120_120 % 11.94/3.22 | (700) ~ (all_0_56_56 = all_0_121_121) | ~ (all_0_57_57 = all_0_122_122) | ~ (all_0_58_58 = all_0_123_123) | ~ (all_0_59_59 = all_0_124_124) | ~ (all_0_60_60 = all_0_125_125) | ~ (all_0_61_61 = all_0_126_126) | ~ (all_0_62_62 = all_0_127_127) % 11.94/3.22 | % 11.94/3.22 +-Applying beta-rule and splitting (700), into two cases. % 11.94/3.22 |-Branch one: % 11.94/3.22 | (701) ~ (all_0_56_56 = all_0_121_121) % 11.94/3.22 | % 11.94/3.22 | Equations (528,431) can reduce 701 to: % 11.94/3.22 | (399) $false % 11.94/3.22 | % 11.94/3.22 |-The branch is then unsatisfiable % 11.94/3.22 |-Branch two: % 11.94/3.22 | (703) all_0_56_56 = all_0_121_121 % 11.94/3.22 | (704) ~ (all_0_57_57 = all_0_122_122) | ~ (all_0_58_58 = all_0_123_123) | ~ (all_0_59_59 = all_0_124_124) | ~ (all_0_60_60 = all_0_125_125) | ~ (all_0_61_61 = all_0_126_126) | ~ (all_0_62_62 = all_0_127_127) % 11.94/3.22 | % 11.94/3.22 +-Applying beta-rule and splitting (704), into two cases. % 11.94/3.22 |-Branch one: % 11.94/3.22 | (705) ~ (all_0_57_57 = all_0_122_122) % 11.94/3.22 | % 11.94/3.22 | Equations (671,430) can reduce 705 to: % 11.94/3.22 | (399) $false % 11.94/3.22 | % 11.94/3.22 |-The branch is then unsatisfiable % 11.94/3.22 |-Branch two: % 11.94/3.22 | (707) all_0_57_57 = all_0_122_122 % 11.94/3.22 | (708) ~ (all_0_58_58 = all_0_123_123) | ~ (all_0_59_59 = all_0_124_124) | ~ (all_0_60_60 = all_0_125_125) | ~ (all_0_61_61 = all_0_126_126) | ~ (all_0_62_62 = all_0_127_127) % 11.94/3.22 | % 11.94/3.22 +-Applying beta-rule and splitting (708), into two cases. % 11.94/3.22 |-Branch one: % 11.94/3.22 | (709) ~ (all_0_58_58 = all_0_123_123) % 11.94/3.22 | % 11.94/3.22 | Equations (673,407) can reduce 709 to: % 11.94/3.22 | (399) $false % 11.94/3.22 | % 11.94/3.22 |-The branch is then unsatisfiable % 11.94/3.22 |-Branch two: % 11.94/3.22 | (711) all_0_58_58 = all_0_123_123 % 11.94/3.22 | (712) ~ (all_0_59_59 = all_0_124_124) | ~ (all_0_60_60 = all_0_125_125) | ~ (all_0_61_61 = all_0_126_126) | ~ (all_0_62_62 = all_0_127_127) % 11.94/3.22 | % 11.94/3.22 +-Applying beta-rule and splitting (712), into two cases. % 11.94/3.22 |-Branch one: % 11.94/3.22 | (713) ~ (all_0_59_59 = all_0_124_124) % 11.94/3.22 | % 11.94/3.22 | Equations (527,422) can reduce 713 to: % 11.94/3.22 | (399) $false % 11.94/3.22 | % 11.94/3.22 |-The branch is then unsatisfiable % 11.94/3.22 |-Branch two: % 11.94/3.22 | (715) all_0_59_59 = all_0_124_124 % 11.94/3.22 | (716) ~ (all_0_60_60 = all_0_125_125) | ~ (all_0_61_61 = all_0_126_126) | ~ (all_0_62_62 = all_0_127_127) % 11.94/3.22 | % 11.94/3.22 +-Applying beta-rule and splitting (716), into two cases. % 11.94/3.22 |-Branch one: % 11.94/3.22 | (717) ~ (all_0_60_60 = all_0_125_125) % 11.94/3.22 | % 11.94/3.22 | Equations (682,435) can reduce 717 to: % 11.94/3.22 | (399) $false % 11.94/3.22 | % 11.94/3.22 |-The branch is then unsatisfiable % 11.94/3.22 |-Branch two: % 11.94/3.22 | (719) all_0_60_60 = all_0_125_125 % 11.94/3.22 | (720) ~ (all_0_61_61 = all_0_126_126) | ~ (all_0_62_62 = all_0_127_127) % 11.94/3.22 | % 11.94/3.22 +-Applying beta-rule and splitting (720), into two cases. % 11.94/3.22 |-Branch one: % 11.94/3.22 | (721) ~ (all_0_61_61 = all_0_126_126) % 11.94/3.22 | % 11.94/3.22 | Equations (680,428) can reduce 721 to: % 11.94/3.22 | (399) $false % 11.94/3.22 | % 11.94/3.22 |-The branch is then unsatisfiable % 11.94/3.22 |-Branch two: % 11.94/3.22 | (723) all_0_61_61 = all_0_126_126 % 11.94/3.22 | (724) ~ (all_0_62_62 = all_0_127_127) % 11.94/3.22 | % 11.94/3.22 | Equations (529,365) can reduce 724 to: % 11.94/3.22 | (399) $false % 11.94/3.22 | % 11.94/3.22 |-The branch is then unsatisfiable % 11.94/3.22 |-Branch two: % 11.94/3.22 | (726) ~ (all_0_131_131 = e13) % 11.94/3.22 | (494) all_0_134_134 = e13 % 11.94/3.22 | % 11.94/3.22 | Combining equations (451,494) yields a new equation: % 11.94/3.22 | (498) e13 = e11 % 11.94/3.22 | % 11.94/3.22 | Equations (498) can reduce 343 to: % 11.94/3.22 | (399) $false % 11.94/3.22 | % 11.94/3.22 |-The branch is then unsatisfiable % 11.94/3.22 |-Branch two: % 11.94/3.22 | (544) ~ (all_0_130_130 = e10) % 11.94/3.22 | (731) all_0_131_131 = e10 | all_0_132_132 = e10 % 11.94/3.22 | % 11.94/3.22 +-Applying beta-rule and splitting (731), into two cases. % 11.94/3.22 |-Branch one: % 11.94/3.22 | (732) all_0_131_131 = e10 % 11.94/3.22 | % 11.94/3.22 | Equations (732) can reduce 610 to: % 11.94/3.22 | (399) $false % 11.94/3.22 | % 11.94/3.22 |-The branch is then unsatisfiable % 11.94/3.22 |-Branch two: % 11.94/3.22 | (610) ~ (all_0_131_131 = e10) % 11.94/3.22 | (440) all_0_132_132 = e10 % 11.94/3.22 | % 11.94/3.22 | Combining equations (521,440) yields a new equation: % 11.94/3.22 | (736) e11 = e10 % 11.94/3.22 | % 11.94/3.22 | Simplifying 736 yields: % 11.94/3.22 | (737) e11 = e10 % 11.94/3.22 | % 11.94/3.22 | Equations (737) can reduce 292 to: % 11.94/3.22 | (399) $false % 11.94/3.22 | % 11.94/3.22 |-The branch is then unsatisfiable % 11.94/3.22 |-Branch two: % 11.94/3.22 | (586) ~ (all_0_136_136 = e11) % 11.94/3.22 | (740) all_0_136_136 = e12 | all_0_136_136 = e10 % 11.94/3.22 | % 11.94/3.22 +-Applying beta-rule and splitting (740), into two cases. % 11.94/3.22 |-Branch one: % 11.94/3.22 | (480) all_0_136_136 = e10 % 11.94/3.22 | % 11.94/3.22 | Equations (480) can reduce 511 to: % 11.94/3.22 | (399) $false % 11.94/3.22 | % 11.94/3.22 |-The branch is then unsatisfiable % 11.94/3.22 |-Branch two: % 11.94/3.22 | (511) ~ (all_0_136_136 = e10) % 11.94/3.22 | (471) all_0_136_136 = e12 % 11.94/3.22 | % 11.94/3.22 | Equations (471) can reduce 647 to: % 11.94/3.22 | (399) $false % 11.94/3.22 | % 11.94/3.22 |-The branch is then unsatisfiable % 11.94/3.22 |-Branch two: % 11.94/3.22 | (470) ~ (all_0_133_133 = e12) % 11.94/3.22 | (474) all_0_134_134 = e12 % 11.94/3.22 | % 11.94/3.22 | Combining equations (474,451) yields a new equation: % 11.94/3.22 | (557) e12 = e11 % 11.94/3.22 | % 11.94/3.22 | Simplifying 557 yields: % 11.94/3.22 | (558) e12 = e11 % 11.94/3.22 | % 11.94/3.22 | Equations (558) can reduce 304 to: % 11.94/3.22 | (399) $false % 11.94/3.22 | % 11.94/3.22 |-The branch is then unsatisfiable % 11.94/3.22 |-Branch two: % 11.94/3.22 | (438) ~ (all_0_134_134 = e11) % 11.94/3.22 | (454) all_0_129_129 = e13 | all_0_137_137 = e10 % 11.94/3.22 | % 11.94/3.22 +-Applying beta-rule and splitting (123), into two cases. % 11.94/3.22 |-Branch one: % 11.94/3.22 | (605) all_0_130_130 = e10 % 11.94/3.22 | % 11.94/3.22 | Equations (605) can reduce 303 to: % 11.94/3.22 | (609) ~ (all_0_131_131 = e10) % 11.94/3.22 | % 11.94/3.22 | Simplifying 609 yields: % 11.94/3.22 | (610) ~ (all_0_131_131 = e10) % 11.94/3.22 | % 11.94/3.22 | Equations (605) can reduce 600 to: % 11.94/3.22 | (464) ~ (e13 = e10) % 11.94/3.22 | % 11.94/3.22 | Simplifying 464 yields: % 11.94/3.22 | (197) ~ (e13 = e10) % 11.94/3.22 | % 11.94/3.22 +-Applying beta-rule and splitting (198), into two cases. % 11.94/3.22 |-Branch one: % 11.94/3.22 | (451) all_0_134_134 = e11 % 11.94/3.22 | % 11.94/3.22 | Equations (451) can reduce 438 to: % 11.94/3.22 | (399) $false % 11.94/3.22 | % 11.94/3.22 |-The branch is then unsatisfiable % 11.94/3.22 |-Branch two: % 11.94/3.23 | (438) ~ (all_0_134_134 = e11) % 11.94/3.23 | (761) all_0_134_134 = e13 | all_0_134_134 = e12 % 11.94/3.23 | % 11.94/3.23 +-Applying beta-rule and splitting (31), into two cases. % 11.94/3.23 |-Branch one: % 11.94/3.23 | (447) all_0_133_133 = e11 % 11.94/3.23 | % 11.94/3.23 | Equations (447) can reduce 492 to: % 11.94/3.23 | (654) ~ (e13 = e11) % 11.94/3.23 | % 11.94/3.23 | Simplifying 654 yields: % 11.94/3.23 | (343) ~ (e13 = e11) % 11.94/3.23 | % 11.94/3.23 +-Applying beta-rule and splitting (108), into two cases. % 11.94/3.23 |-Branch one: % 11.94/3.23 | (551) all_0_130_130 = e13 % 11.94/3.23 | % 11.94/3.23 | Combining equations (605,551) yields a new equation: % 11.94/3.23 | (442) e13 = e10 % 11.94/3.23 | % 11.94/3.23 | Equations (442) can reduce 197 to: % 11.94/3.23 | (399) $false % 11.94/3.23 | % 11.94/3.23 |-The branch is then unsatisfiable % 11.94/3.23 |-Branch two: % 11.94/3.23 | (600) ~ (all_0_130_130 = e13) % 11.94/3.23 | (601) all_0_131_131 = e13 | all_0_132_132 = e13 % 11.94/3.23 | % 11.94/3.23 +-Applying beta-rule and splitting (601), into two cases. % 11.94/3.23 |-Branch one: % 11.94/3.23 | (667) all_0_131_131 = e13 % 11.94/3.23 | % 11.94/3.23 | Equations (667) can reduce 610 to: % 11.94/3.23 | (197) ~ (e13 = e10) % 11.94/3.23 | % 11.94/3.23 +-Applying beta-rule and splitting (454), into two cases. % 11.94/3.23 |-Branch one: % 12.02/3.23 | (455) all_0_129_129 = e13 % 12.02/3.23 | % 12.02/3.23 | Combining equations (488,455) yields a new equation: % 12.02/3.23 | (442) e13 = e10 % 12.02/3.23 | % 12.02/3.23 | Equations (442) can reduce 197 to: % 12.02/3.23 | (399) $false % 12.02/3.23 | % 12.02/3.23 |-The branch is then unsatisfiable % 12.02/3.23 |-Branch two: % 12.02/3.23 | (500) ~ (all_0_129_129 = e13) % 12.02/3.23 | (501) all_0_137_137 = e10 % 12.02/3.23 | % 12.02/3.23 | Equations (501) can reduce 446 to: % 12.02/3.23 | (399) $false % 12.02/3.23 | % 12.02/3.23 |-The branch is then unsatisfiable % 12.02/3.23 |-Branch two: % 12.02/3.23 | (726) ~ (all_0_131_131 = e13) % 12.02/3.23 | (439) all_0_132_132 = e13 % 12.02/3.23 | % 12.02/3.23 | Combining equations (521,439) yields a new equation: % 12.02/3.23 | (498) e13 = e11 % 12.02/3.23 | % 12.02/3.23 | Equations (498) can reduce 343 to: % 12.02/3.23 | (399) $false % 12.02/3.23 | % 12.02/3.23 |-The branch is then unsatisfiable % 12.02/3.23 |-Branch two: % 12.02/3.23 | (437) ~ (all_0_133_133 = e11) % 12.02/3.23 | (783) all_0_134_134 = e11 | all_0_135_135 = e11 % 12.02/3.23 | % 12.02/3.23 +-Applying beta-rule and splitting (783), into two cases. % 12.02/3.23 |-Branch one: % 12.02/3.23 | (451) all_0_134_134 = e11 % 12.02/3.23 | % 12.02/3.23 | Equations (451) can reduce 438 to: % 12.02/3.23 | (399) $false % 12.02/3.23 | % 12.02/3.23 |-The branch is then unsatisfiable % 12.02/3.23 |-Branch two: % 12.02/3.23 | (438) ~ (all_0_134_134 = e11) % 12.02/3.23 | (436) all_0_135_135 = e11 % 12.02/3.23 | % 12.02/3.23 | Combining equations (436,497) yields a new equation: % 12.02/3.23 | (498) e13 = e11 % 12.02/3.23 | % 12.02/3.23 | Equations (498) can reduce 343 to: % 12.02/3.23 | (399) $false % 12.02/3.23 | % 12.02/3.23 |-The branch is then unsatisfiable % 12.02/3.23 |-Branch two: % 12.02/3.23 | (544) ~ (all_0_130_130 = e10) % 12.02/3.23 | (731) all_0_131_131 = e10 | all_0_132_132 = e10 % 12.02/3.23 | % 12.02/3.23 +-Applying beta-rule and splitting (108), into two cases. % 12.02/3.23 |-Branch one: % 12.02/3.23 | (551) all_0_130_130 = e13 % 12.02/3.23 | % 12.02/3.23 | Equations (551) can reduce 600 to: % 12.02/3.23 | (399) $false % 12.02/3.23 | % 12.02/3.23 |-The branch is then unsatisfiable % 12.02/3.23 |-Branch two: % 12.02/3.23 | (600) ~ (all_0_130_130 = e13) % 12.02/3.23 | (601) all_0_131_131 = e13 | all_0_132_132 = e13 % 12.02/3.23 | % 12.02/3.23 +-Applying beta-rule and splitting (550), into two cases. % 12.02/3.23 |-Branch one: % 12.02/3.23 | (551) all_0_130_130 = e13 % 12.02/3.23 | % 12.02/3.23 | Equations (551) can reduce 600 to: % 12.02/3.23 | (399) $false % 12.02/3.23 | % 12.02/3.23 |-The branch is then unsatisfiable % 12.02/3.23 |-Branch two: % 12.02/3.23 | (600) ~ (all_0_130_130 = e13) % 12.02/3.23 | (605) all_0_130_130 = e10 % 12.02/3.23 | % 12.02/3.23 | Equations (605) can reduce 544 to: % 12.02/3.23 | (399) $false % 12.02/3.23 | % 12.02/3.23 |-The branch is then unsatisfiable % 12.02/3.23 |-Branch two: % 12.02/3.23 | (461) ~ (all_0_128_128 = e13) % 12.02/3.23 | (455) all_0_129_129 = e13 % 12.02/3.23 | % 12.02/3.23 | Combining equations (488,455) yields a new equation: % 12.02/3.23 | (442) e13 = e10 % 12.02/3.23 | % 12.02/3.23 | Equations (442) can reduce 197 to: % 12.02/3.23 | (399) $false % 12.02/3.23 | % 12.02/3.23 |-The branch is then unsatisfiable % 12.02/3.23 |-Branch two: % 12.02/3.23 | (805) ~ (all_0_132_132 = e11) % 12.02/3.23 | (806) all_0_135_135 = e11 | all_0_138_138 = e11 % 12.02/3.23 | % 12.02/3.23 +-Applying beta-rule and splitting (73), into two cases. % 12.02/3.23 |-Branch one: % 12.02/3.23 | (521) all_0_132_132 = e11 % 12.02/3.23 | % 12.02/3.23 | Equations (521) can reduce 805 to: % 12.02/3.23 | (399) $false % 12.02/3.23 | % 12.02/3.23 |-The branch is then unsatisfiable % 12.02/3.23 |-Branch two: % 12.02/3.23 | (805) ~ (all_0_132_132 = e11) % 12.02/3.23 | (810) all_0_132_132 = e13 | all_0_132_132 = e10 % 12.02/3.23 | % 12.02/3.23 +-Applying beta-rule and splitting (810), into two cases. % 12.02/3.23 |-Branch one: % 12.02/3.23 | (439) all_0_132_132 = e13 % 12.02/3.23 | % 12.02/3.23 | Equations (439) can reduce 503 to: % 12.02/3.23 | (399) $false % 12.02/3.23 | % 12.02/3.23 |-The branch is then unsatisfiable % 12.02/3.23 |-Branch two: % 12.02/3.23 | (503) ~ (all_0_132_132 = e13) % 12.02/3.23 | (440) all_0_132_132 = e10 % 12.02/3.23 | % 12.02/3.23 | Equations (440) can reduce 444 to: % 12.02/3.23 | (399) $false % 12.02/3.23 | % 12.02/3.23 |-The branch is then unsatisfiable % 12.02/3.23 |-Branch two: % 12.02/3.23 | (816) ~ (all_0_125_125 = e21) % 12.02/3.23 | (817) all_0_126_126 = e21 | all_0_127_127 = e21 % 12.02/3.23 | % 12.02/3.23 +-Applying beta-rule and splitting (817), into two cases. % 12.02/3.23 |-Branch one: % 12.02/3.23 | (818) all_0_126_126 = e21 % 12.02/3.23 | % 12.02/3.23 | Combining equations (428,818) yields a new equation: % 12.02/3.23 | (819) e22 = e21 % 12.02/3.23 | % 12.02/3.23 | Simplifying 819 yields: % 12.02/3.23 | (425) e22 = e21 % 12.02/3.23 | % 12.02/3.23 | Equations (425) can reduce 249 to: % 12.02/3.23 | (399) $false % 12.02/3.23 | % 12.02/3.23 |-The branch is then unsatisfiable % 12.02/3.23 |-Branch two: % 12.02/3.23 | (822) ~ (all_0_126_126 = e21) % 12.02/3.23 | (823) all_0_127_127 = e21 % 12.02/3.23 | % 12.02/3.23 | Combining equations (823,365) yields a new equation: % 12.02/3.23 | (824) e21 = e20 % 12.02/3.23 | % 12.02/3.23 | Simplifying 824 yields: % 12.02/3.23 | (825) e21 = e20 % 12.02/3.23 | % 12.02/3.23 | Equations (825) can reduce 320 to: % 12.02/3.23 | (399) $false % 12.02/3.23 | % 12.02/3.23 |-The branch is then unsatisfiable % 12.02/3.23 |-Branch two: % 12.02/3.23 | (827) ~ (all_0_121_121 = e21) % 12.02/3.23 | (828) all_0_124_124 = e21 | all_0_127_127 = e21 % 12.02/3.23 | % 12.02/3.23 +-Applying beta-rule and splitting (828), into two cases. % 12.02/3.23 |-Branch one: % 12.02/3.23 | (829) all_0_124_124 = e21 % 12.02/3.23 | % 12.02/3.23 | Combining equations (422,829) yields a new equation: % 12.02/3.23 | (830) e23 = e21 % 12.02/3.23 | % 12.02/3.23 | Simplifying 830 yields: % 12.02/3.24 | (831) e23 = e21 % 12.02/3.24 | % 12.02/3.24 | Equations (831) can reduce 278 to: % 12.02/3.24 | (399) $false % 12.02/3.24 | % 12.02/3.24 |-The branch is then unsatisfiable % 12.02/3.24 |-Branch two: % 12.02/3.24 | (410) ~ (all_0_124_124 = e21) % 12.02/3.24 | (823) all_0_127_127 = e21 % 12.02/3.24 | % 12.02/3.24 | Combining equations (823,365) yields a new equation: % 12.02/3.24 | (824) e21 = e20 % 12.02/3.24 | % 12.02/3.24 | Simplifying 824 yields: % 12.02/3.24 | (825) e21 = e20 % 12.02/3.24 | % 12.02/3.24 | Equations (825) can reduce 320 to: % 12.02/3.24 | (399) $false % 12.02/3.24 | % 12.02/3.24 |-The branch is then unsatisfiable % 12.02/3.24 |-Branch two: % 12.02/3.24 | (838) ~ (all_0_122_122 = e22) % 12.02/3.24 | (839) all_0_125_125 = e22 % 12.02/3.24 | % 12.02/3.24 | Equations (839) can reduce 429 to: % 12.02/3.24 | (399) $false % 12.02/3.24 | % 12.02/3.24 |-The branch is then unsatisfiable % 12.02/3.24 |-Branch two: % 12.02/3.24 | (841) ~ (all_0_120_120 = e23) % 12.02/3.24 | (842) all_0_120_120 = e21 % 12.02/3.24 | % 12.02/3.24 | Equations (842) can reduce 408 to: % 12.02/3.24 | (399) $false % 12.02/3.24 | % 12.02/3.24 |-The branch is then unsatisfiable % 12.02/3.24 |-Branch two: % 12.02/3.24 | (844) ~ (all_0_119_119 = e20) % 12.02/3.24 | (845) all_0_120_120 = e20 | all_0_121_121 = e20 % 12.02/3.24 | % 12.02/3.24 +-Applying beta-rule and splitting (845), into two cases. % 12.02/3.24 |-Branch one: % 12.02/3.24 | (412) all_0_120_120 = e20 % 12.02/3.24 | % 12.02/3.24 | Equations (412) can reduce 383 to: % 12.02/3.24 | (399) $false % 12.02/3.24 | % 12.02/3.24 |-The branch is then unsatisfiable % 12.02/3.24 |-Branch two: % 12.02/3.24 | (383) ~ (all_0_120_120 = e20) % 12.02/3.24 | (849) all_0_121_121 = e20 % 12.02/3.24 | % 12.02/3.24 | Equations (849) can reduce 366 to: % 12.02/3.24 | (399) $false % 12.02/3.24 | % 12.02/3.24 |-The branch is then unsatisfiable % 12.02/3.24 |-Branch two: % 12.02/3.24 | (851) ~ (all_0_117_117 = e23) % 12.02/3.24 | (402) all_0_118_118 = e23 % 12.02/3.24 | % 12.02/3.24 | Combining equations (381,402) yields a new equation: % 12.02/3.24 | (404) e23 = e20 % 12.02/3.24 | % 12.02/3.24 | Equations (404) can reduce 266 to: % 12.02/3.24 | (399) $false % 12.02/3.24 | % 12.02/3.24 |-The branch is then unsatisfiable % 12.02/3.24 |-Branch two: % 12.02/3.24 | (855) ~ (all_0_118_118 = e20) % 12.02/3.24 | (402) all_0_118_118 = e23 % 12.02/3.24 | % 12.02/3.24 | Equations (402) can reduce 35 to: % 12.02/3.24 | (851) ~ (all_0_117_117 = e23) % 12.02/3.24 | % 12.02/3.24 | Equations (402) can reduce 12 to: % 12.02/3.24 | (858) ~ (all_0_120_120 = e23) % 12.02/3.24 | % 12.02/3.24 | Simplifying 858 yields: % 12.02/3.24 | (841) ~ (all_0_120_120 = e23) % 12.02/3.24 | % 12.02/3.24 | Equations (402) can reduce 855 to: % 12.02/3.24 | (266) ~ (e23 = e20) % 12.02/3.24 | % 12.02/3.24 +-Applying beta-rule and splitting (333), into two cases. % 12.02/3.24 |-Branch one: % 12.02/3.24 | (861) all_0_117_117 = e20 % 12.02/3.24 | % 12.02/3.24 | Equations (861) can reduce 121 to: % 12.02/3.24 | (862) ~ (all_0_125_125 = e20) % 12.02/3.24 | % 12.02/3.24 | Simplifying 862 yields: % 12.02/3.24 | (863) ~ (all_0_125_125 = e20) % 12.02/3.24 | % 12.02/3.24 | Equations (861) can reduce 851 to: % 12.02/3.24 | (368) ~ (e23 = e20) % 12.02/3.24 | % 12.02/3.24 | Simplifying 368 yields: % 12.02/3.24 | (266) ~ (e23 = e20) % 12.02/3.24 | % 12.02/3.24 +-Applying beta-rule and splitting (94), into two cases. % 12.02/3.24 |-Branch one: % 12.02/3.24 | (381) all_0_118_118 = e20 % 12.02/3.24 | % 12.02/3.24 | Combining equations (402,381) yields a new equation: % 12.02/3.24 | (403) e23 = e20 % 12.02/3.24 | % 12.02/3.24 | Simplifying 403 yields: % 12.02/3.24 | (404) e23 = e20 % 12.02/3.24 | % 12.02/3.24 | Equations (404) can reduce 266 to: % 12.02/3.24 | (399) $false % 12.02/3.24 | % 12.02/3.24 |-The branch is then unsatisfiable % 12.02/3.24 |-Branch two: % 12.02/3.24 | (855) ~ (all_0_118_118 = e20) % 12.02/3.24 | (871) all_0_120_120 = e20 | all_0_126_126 = e20 % 12.02/3.24 | % 12.02/3.24 +-Applying beta-rule and splitting (871), into two cases. % 12.02/3.24 |-Branch one: % 12.02/3.24 | (412) all_0_120_120 = e20 % 12.02/3.24 | % 12.02/3.24 | Equations (412) can reduce 169 to: % 12.02/3.24 | (844) ~ (all_0_119_119 = e20) % 12.02/3.24 | % 12.02/3.24 | Equations (412) can reduce 841 to: % 12.02/3.24 | (368) ~ (e23 = e20) % 12.02/3.24 | % 12.02/3.24 | Simplifying 368 yields: % 12.02/3.24 | (266) ~ (e23 = e20) % 12.02/3.24 | % 12.02/3.24 +-Applying beta-rule and splitting (7), into two cases. % 12.02/3.24 |-Branch one: % 12.02/3.24 | (876) all_0_125_125 = e20 % 12.02/3.24 | % 12.02/3.24 | Equations (876) can reduce 863 to: % 12.02/3.24 | (399) $false % 12.02/3.24 | % 12.02/3.24 |-The branch is then unsatisfiable % 12.02/3.24 |-Branch two: % 12.02/3.24 | (863) ~ (all_0_125_125 = e20) % 12.02/3.24 | (879) all_0_117_117 = e23 | all_0_122_122 = e21 % 12.02/3.24 | % 12.02/3.24 +-Applying beta-rule and splitting (879), into two cases. % 12.02/3.24 |-Branch one: % 12.02/3.24 | (388) all_0_117_117 = e23 % 12.02/3.24 | % 12.02/3.24 | Combining equations (861,388) yields a new equation: % 12.02/3.24 | (404) e23 = e20 % 12.02/3.24 | % 12.02/3.24 | Equations (404) can reduce 266 to: % 12.02/3.24 | (399) $false % 12.02/3.24 | % 12.02/3.24 |-The branch is then unsatisfiable % 12.02/3.24 |-Branch two: % 12.02/3.24 | (851) ~ (all_0_117_117 = e23) % 12.02/3.24 | (884) all_0_122_122 = e21 % 12.02/3.24 | % 12.02/3.24 | Equations (884) can reduce 181 to: % 12.02/3.24 | (885) ~ (all_0_119_119 = e21) % 12.02/3.24 | % 12.02/3.24 +-Applying beta-rule and splitting (165), into two cases. % 12.02/3.24 |-Branch one: % 12.02/3.24 | (391) all_0_119_119 = e20 % 12.02/3.24 | % 12.02/3.24 | Equations (391) can reduce 844 to: % 12.02/3.24 | (399) $false % 12.02/3.24 | % 12.02/3.24 |-The branch is then unsatisfiable % 12.02/3.24 |-Branch two: % 12.02/3.24 | (844) ~ (all_0_119_119 = e20) % 12.02/3.24 | (889) all_0_119_119 = e23 | all_0_119_119 = e21 % 12.02/3.24 | % 12.02/3.24 +-Applying beta-rule and splitting (889), into two cases. % 12.02/3.24 |-Branch one: % 12.02/3.24 | (890) all_0_119_119 = e23 % 12.02/3.24 | % 12.02/3.24 | From (890) and (282) follows: % 12.02/3.24 | (891) op2(e22, e23) = all_0_97_97 % 12.02/3.24 | % 12.02/3.24 | From (890) and (329) follows: % 12.02/3.24 | (892) op2(e22, e23) = e23 % 12.02/3.24 | % 12.02/3.24 +-Applying beta-rule and splitting (334), into two cases. % 12.02/3.24 |-Branch one: % 12.02/3.24 | (430) all_0_122_122 = e22 % 12.02/3.24 | % 12.02/3.24 | Combining equations (884,430) yields a new equation: % 12.02/3.24 | (425) e22 = e21 % 12.02/3.24 | % 12.02/3.24 | Equations (425) can reduce 249 to: % 12.02/3.24 | (399) $false % 12.02/3.24 | % 12.02/3.24 |-The branch is then unsatisfiable % 12.02/3.24 |-Branch two: % 12.02/3.24 | (838) ~ (all_0_122_122 = e22) % 12.02/3.24 | (424) all_0_123_123 = e22 % 12.02/3.24 | % 12.02/3.24 | From (424) and (182) follows: % 12.02/3.24 | (898) op2(e21, e22) = all_0_101_101 % 12.02/3.24 | % 12.02/3.24 | From (424) and (250) follows: % 12.02/3.24 | (899) op2(e21, e22) = e22 % 12.02/3.24 | % 12.02/3.24 | Instantiating formula (175) with e22, e23, e23, all_0_97_97 and discharging atoms op2(e22, e23) = all_0_97_97, op2(e22, e23) = e23, yields: % 12.02/3.24 | (900) all_0_97_97 = e23 % 12.02/3.24 | % 12.02/3.24 | Instantiating formula (175) with e21, e22, e22, all_0_101_101 and discharging atoms op2(e21, e22) = all_0_101_101, op2(e21, e22) = e22, yields: % 12.02/3.25 | (901) all_0_101_101 = e22 % 12.02/3.25 | % 12.02/3.25 +-Applying beta-rule and splitting (234), into two cases. % 12.02/3.25 |-Branch one: % 12.02/3.25 | (902) ( ~ (all_0_97_97 = e23) & ~ (all_0_98_98 = e22) & ~ (all_0_99_99 = e20) & ~ (all_0_120_120 = e21)) | ( ~ (all_0_100_100 = e23) & ~ (all_0_101_101 = e22) & ~ (all_0_102_102 = e20) & ~ (all_0_124_124 = e21)) % 12.02/3.25 | % 12.02/3.25 +-Applying beta-rule and splitting (902), into two cases. % 12.02/3.25 |-Branch one: % 12.02/3.25 | (903) ~ (all_0_97_97 = e23) & ~ (all_0_98_98 = e22) & ~ (all_0_99_99 = e20) & ~ (all_0_120_120 = e21) % 12.02/3.25 | % 12.02/3.25 | Applying alpha-rule on (903) yields: % 12.02/3.25 | (904) ~ (all_0_97_97 = e23) % 12.02/3.25 | (905) ~ (all_0_98_98 = e22) % 12.02/3.25 | (906) ~ (all_0_99_99 = e20) % 12.02/3.25 | (408) ~ (all_0_120_120 = e21) % 12.02/3.25 | % 12.02/3.25 | Equations (900) can reduce 904 to: % 12.02/3.25 | (399) $false % 12.02/3.25 | % 12.02/3.25 |-The branch is then unsatisfiable % 12.02/3.25 |-Branch two: % 12.02/3.25 | (909) ~ (all_0_100_100 = e23) & ~ (all_0_101_101 = e22) & ~ (all_0_102_102 = e20) & ~ (all_0_124_124 = e21) % 12.02/3.25 | % 12.02/3.25 | Applying alpha-rule on (909) yields: % 12.02/3.25 | (910) ~ (all_0_100_100 = e23) % 12.02/3.25 | (911) ~ (all_0_101_101 = e22) % 12.02/3.25 | (912) ~ (all_0_102_102 = e20) % 12.02/3.25 | (410) ~ (all_0_124_124 = e21) % 12.02/3.25 | % 12.02/3.25 | Equations (901) can reduce 911 to: % 12.02/3.25 | (399) $false % 12.02/3.25 | % 12.02/3.25 |-The branch is then unsatisfiable % 12.02/3.25 |-Branch two: % 12.02/3.25 | (915) ~ (all_0_103_103 = e23) & ~ (all_0_104_104 = e22) & ~ (all_0_105_105 = e20) & ~ (all_0_125_125 = e21) % 12.02/3.25 | % 12.02/3.25 | Applying alpha-rule on (915) yields: % 12.02/3.25 | (916) ~ (all_0_103_103 = e23) % 12.02/3.25 | (917) ~ (all_0_104_104 = e22) % 12.02/3.25 | (918) ~ (all_0_105_105 = e20) % 12.02/3.25 | (816) ~ (all_0_125_125 = e21) % 12.02/3.25 | % 12.02/3.25 | Equations (380) can reduce 918 to: % 12.02/3.25 | (399) $false % 12.02/3.25 | % 12.02/3.25 |-The branch is then unsatisfiable % 12.02/3.25 |-Branch two: % 12.02/3.25 | (390) ~ (all_0_119_119 = e23) % 12.02/3.25 | (922) all_0_119_119 = e21 % 12.02/3.25 | % 12.02/3.25 | Equations (922) can reduce 885 to: % 12.02/3.25 | (399) $false % 12.02/3.25 | % 12.02/3.25 |-The branch is then unsatisfiable % 12.02/3.25 |-Branch two: % 12.02/3.25 | (383) ~ (all_0_120_120 = e20) % 12.02/3.25 | (398) all_0_126_126 = e20 % 12.02/3.25 | % 12.02/3.25 | Equations (398) can reduce 367 to: % 12.02/3.25 | (399) $false % 12.02/3.25 | % 12.02/3.25 |-The branch is then unsatisfiable % 12.02/3.25 |-Branch two: % 12.02/3.25 | (927) ~ (all_0_117_117 = e20) % 12.02/3.25 | (381) all_0_118_118 = e20 % 12.02/3.25 | % 12.02/3.25 | Combining equations (402,381) yields a new equation: % 12.02/3.25 | (403) e23 = e20 % 12.02/3.25 | % 12.02/3.25 | Simplifying 403 yields: % 12.02/3.25 | (404) e23 = e20 % 12.02/3.25 | % 12.02/3.25 | Equations (404) can reduce 266 to: % 12.02/3.25 | (399) $false % 12.02/3.25 | % 12.02/3.25 |-The branch is then unsatisfiable % 12.02/3.25 |-Branch two: % 12.02/3.25 | (932) ~ (all_0_127_127 = e20) % 12.02/3.25 | (829) all_0_124_124 = e21 % 12.02/3.25 | % 12.02/3.25 | Equations (829) can reduce 325 to: % 12.02/3.25 | (934) ~ (all_0_127_127 = e21) % 12.02/3.25 | % 12.02/3.25 | Simplifying 934 yields: % 12.02/3.25 | (935) ~ (all_0_127_127 = e21) % 12.02/3.25 | % 12.02/3.25 +-Applying beta-rule and splitting (213), into two cases. % 12.02/3.25 |-Branch one: % 12.02/3.25 | (849) all_0_121_121 = e20 % 12.02/3.25 | % 12.02/3.25 | Equations (849) can reduce 307 to: % 12.02/3.25 | (937) ~ (all_0_127_127 = e20) % 12.02/3.25 | % 12.02/3.25 | Simplifying 937 yields: % 12.02/3.25 | (932) ~ (all_0_127_127 = e20) % 12.02/3.25 | % 12.02/3.25 +-Applying beta-rule and splitting (184), into two cases. % 12.02/3.25 |-Branch one: % 12.02/3.25 | (365) all_0_127_127 = e20 % 12.02/3.25 | % 12.02/3.25 | Equations (365) can reduce 932 to: % 12.02/3.25 | (399) $false % 12.02/3.25 | % 12.02/3.25 |-The branch is then unsatisfiable % 12.02/3.25 |-Branch two: % 12.02/3.25 | (932) ~ (all_0_127_127 = e20) % 12.02/3.25 | (823) all_0_127_127 = e21 % 12.02/3.25 | % 12.02/3.25 | Equations (823) can reduce 935 to: % 12.02/3.25 | (399) $false % 12.02/3.25 | % 12.02/3.25 |-The branch is then unsatisfiable % 12.02/3.25 |-Branch two: % 12.02/3.25 | (366) ~ (all_0_121_121 = e20) % 12.02/3.25 | (365) all_0_127_127 = e20 % 12.02/3.25 | % 12.02/3.25 | Equations (365) can reduce 932 to: % 12.02/3.25 | (399) $false % 12.02/3.25 | % 12.02/3.25 |-The branch is then unsatisfiable % 12.02/3.25 % SZS output end Proof for theBenchmark % 12.02/3.25 % 12.02/3.25 2742ms %------------------------------------------------------------------------------