%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : ALG105+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n032.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:09 EDT 2022 % Result : Theorem 6.06s 1.89s % Output : Proof 11.25s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : ALG105+1 : TPTP v8.1.0. Released v2.7.0. % 0.00/0.10 % Command : ePrincess-casc -timeout=%d %s % 0.09/0.29 % Computer : n032.cluster.edu % 0.09/0.29 % Model : x86_64 x86_64 % 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.29 % Memory : 8042.1875MB % 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.29 % CPULimit : 300 % 0.09/0.29 % WCLimit : 600 % 0.09/0.29 % DateTime : Thu Jun 9 06:32:52 EDT 2022 % 0.09/0.29 % CPUTime : % 0.14/0.47 ____ _ % 0.14/0.47 ___ / __ \_____(_)___ ________ __________ % 0.14/0.47 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.14/0.47 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.14/0.47 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.14/0.47 % 0.14/0.47 A Theorem Prover for First-Order Logic % 0.14/0.47 (ePrincess v.1.0) % 0.14/0.47 % 0.14/0.47 (c) Philipp Rümmer, 2009-2015 % 0.14/0.47 (c) Peter Backeman, 2014-2015 % 0.14/0.47 (contributions by Angelo Brillout, Peter Baumgartner) % 0.14/0.47 Free software under GNU Lesser General Public License (LGPL). % 0.14/0.47 Bug reports to peter@backeman.se % 0.14/0.47 % 0.14/0.47 For more information, visit http://user.uu.se/~petba168/breu/ % 0.14/0.47 % 0.14/0.47 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.14/0.51 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 2.44/1.05 Prover 0: Preprocessing ... % 5.23/1.64 Prover 0: Constructing countermodel ... % 6.06/1.88 Prover 0: proved (1369ms) % 6.06/1.88 % 6.06/1.89 No countermodel exists, formula is valid % 6.06/1.89 % SZS status Theorem for theBenchmark % 6.06/1.89 % 6.06/1.89 Generating proof ... found it (size 274) % 10.47/2.87 % 10.47/2.87 % SZS output start Proof for theBenchmark % 10.47/2.87 Assumed formulas after preprocessing and simplification: % 10.47/2.87 | (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] : ? [v139] : ? [v140] : ? [v141] : ? [v142] : ? [v143] : ? [v144] : ? [v145] : ? [v146] : ? [v147] : ? [v148] : ? [v149] : ? [v150] : ? [v151] : ? [v152] : ? [v153] : ? [v154] : ? [v155] : ? [v156] : ? [v157] : ? [v158] : ? [v159] : ? [v160] : ? [v161] : ? [v162] : ? [v163] : ? [v164] : ? [v165] : ? [v166] : ? [v167] : ? [v168] : ? [v169] : ? [v170] : ? [v171] : ? [v172] : ? [v173] : ? [v174] : ? [v175] : ? [v176] : ? [v177] : ? [v178] : ? [v179] : ? [v180] : ? [v181] : ? [v182] : ? [v183] : ? [v184] : ? [v185] : ( ~ (v13 = v12) & ~ (v13 = v9) & ~ (v13 = e23) & ~ (v13 = e21) & ~ (v12 = v10) & ~ (v12 = v7) & ~ (v12 = e23) & ~ (v12 = e21) & ~ (v11 = v10) & ~ (v11 = v8) & ~ (v11 = e23) & ~ (v11 = e22) & ~ (v10 = v7) & ~ (v10 = e23) & ~ (v10 = e22) & ~ (v9 = v8) & ~ (v9 = v7) & ~ (v9 = e23) & ~ (v9 = e21) & ~ (v8 = v7) & ~ (v8 = e23) & ~ (v8 = e22) & ~ (v7 = e23) & ~ (v6 = v5) & ~ (v6 = v2) & ~ (v6 = e13) & ~ (v6 = e11) & ~ (v5 = v3) & ~ (v5 = v0) & ~ (v5 = e13) & ~ (v5 = e11) & ~ (v4 = v3) & ~ (v4 = v1) & ~ (v4 = e13) & ~ (v4 = e12) & ~ (v3 = v0) & ~ (v3 = e13) & ~ (v3 = e12) & ~ (v2 = v1) & ~ (v2 = v0) & ~ (v2 = e13) & ~ (v2 = e11) & ~ (v1 = v0) & ~ (v1 = e13) & ~ (v1 = e12) & ~ (v0 = e13) & ~ (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(v6, e12) = e12 & op1(v5, e12) = e10 & op1(v4, e11) = e11 & op1(v3, e11) = e10 & op1(v2, e10) = e12 & op1(v1, e10) = e11 & op1(v0, e10) = e10 & op1(e13, e13) = e10 & op1(e13, e12) = e11 & op1(e13, e11) = e12 & op1(e13, e10) = e13 & op1(e12, v6) = v17 & op1(e12, v2) = v16 & op1(e12, e13) = e11 & op1(e12, e12) = v6 & op1(e12, e11) = e13 & op1(e12, e10) = v5 & op1(e11, v4) = v15 & op1(e11, v1) = v14 & op1(e11, e13) = e12 & op1(e11, e12) = e13 & op1(e11, e11) = v4 & op1(e11, e10) = v3 & op1(e10, v5) = v5 & op1(e10, v3) = v3 & op1(e10, v0) = v0 & op1(e10, e13) = e13 & op1(e10, e12) = v2 & op1(e10, e11) = v1 & op1(e10, e10) = v0 & h1(v6) = v39 & h1(v5) = v37 & h1(v4) = v35 & h1(v3) = v33 & h1(v2) = v30 & h1(v1) = v28 & h1(v0) = v26 & h1(e13) = v10 & h1(e12) = e21 & h1(e11) = e20 & h1(e10) = v22 & h2(v6) = v58 & h2(v5) = v56 & h2(v4) = v54 & h2(v3) = v52 & h2(v2) = v49 & h2(v1) = v47 & h2(v0) = v45 & h2(e13) = v12 & h2(e12) = e22 & h2(e11) = e20 & h2(e10) = v23 & h3(v6) = v70 & h3(v5) = v69 & h3(v4) = v68 & h3(v3) = v67 & h3(v2) = v66 & h3(v1) = v65 & h3(v0) = v64 & h3(e13) = e23 & h3(e12) = e23 & h3(e11) = e20 & h3(e10) = e20 & h4(v6) = v84 & h4(v5) = v82 & h4(v4) = v80 & h4(v3) = v78 & h4(v2) = v75 & h4(v1) = v73 & h4(v0) = v71 & h4(e13) = v8 & h4(e12) = e20 & h4(e11) = e21 & h4(e10) = v24 & h5(v6) = v96 & h5(v5) = v95 & h5(v4) = v94 & h5(v3) = v93 & h5(v2) = v92 & h5(v1) = v91 & h5(v0) = v90 & h5(e13) = e23 & h5(e12) = e22 & h5(e11) = e21 & h5(e10) = e20 & h6(v6) = v109 & h6(v5) = v107 & h6(v4) = v106 & h6(v3) = v104 & h6(v2) = v101 & h6(v1) = v99 & h6(v0) = v97 & h6(e13) = e22 & h6(e12) = e23 & h6(e11) = e21 & h6(e10) = v13 & h7(v6) = v124 & h7(v5) = v122 & h7(v4) = v120 & h7(v3) = v118 & h7(v2) = v115 & h7(v1) = v113 & h7(v0) = v111 & h7(e13) = v9 & h7(e12) = e20 & h7(e11) = e22 & h7(e10) = v25 & h8(v6) = v136 & h8(v5) = v135 & h8(v4) = v134 & h8(v3) = v133 & h8(v2) = v132 & h8(v1) = v131 & h8(v0) = v130 & h8(e13) = e23 & h8(e12) = e21 & h8(e11) = e22 & h8(e10) = e20 & h9(v6) = v149 & h9(v5) = v147 & h9(v4) = v146 & h9(v3) = v144 & h9(v2) = v141 & h9(v1) = v139 & h9(v0) = v137 & h9(e13) = e21 & h9(e12) = e23 & h9(e11) = e22 & h9(e10) = v11 & h10(v6) = v157 & h10(v5) = v156 & h10(v4) = v155 & h10(v3) = v154 & h10(v2) = v153 & h10(v1) = v152 & h10(v0) = v151 & h10(e13) = e23 & h10(e12) = e20 & h10(e11) = e23 & h10(e10) = e20 & h11(v6) = v170 & h11(v5) = v168 & h11(v4) = v167 & h11(v3) = v165 & h11(v2) = v162 & h11(v1) = v160 & h11(v0) = v158 & h11(e13) = e22 & h11(e12) = e21 & h11(e11) = e23 & h11(e10) = v13 & h12(v6) = v184 & h12(v5) = v182 & h12(v4) = v181 & h12(v3) = v179 & h12(v2) = v176 & h12(v1) = v174 & h12(v0) = v172 & h12(e13) = e21 & h12(e12) = e22 & h12(e11) = e23 & h12(e10) = v11 & op2(v25, v25) = v112 & op2(v25, v9) = v117 & op2(v25, e22) = v114 & op2(v25, e20) = v116 & op2(v24, v24) = v72 & op2(v24, v8) = v77 & op2(v24, e21) = v74 & op2(v24, e20) = v76 & op2(v23, v23) = v46 & op2(v23, v12) = v51 & op2(v23, e22) = v50 & op2(v23, e20) = v48 & op2(v22, v22) = v27 & op2(v22, v10) = v32 & op2(v22, e21) = v31 & op2(v22, e20) = v29 & op2(v13, v13) = v159 & op2(v13, v13) = v98 & op2(v13, e23) = v161 & op2(v13, e23) = v102 & op2(v13, e22) = v164 & op2(v13, e22) = v103 & op2(v13, e22) = e22 & op2(v13, e21) = v163 & op2(v13, e21) = v100 & op2(v12, v23) = v60 & op2(v12, v12) = v63 & op2(v12, v12) = v23 & op2(v12, e22) = v62 & op2(v12, e22) = e20 & op2(v12, e20) = v61 & op2(v11, v11) = v173 & op2(v11, v11) = v138 & op2(v11, e23) = v175 & op2(v11, e23) = v142 & op2(v11, e22) = v177 & op2(v11, e22) = v140 & op2(v11, e21) = v178 & op2(v11, e21) = v143 & op2(v11, e21) = e21 & op2(v10, v22) = v41 & op2(v10, v10) = v44 & op2(v10, v10) = v22 & op2(v10, e21) = v43 & op2(v10, e21) = e20 & op2(v10, e20) = v42 & op2(v9, v25) = v126 & op2(v9, v9) = v129 & op2(v9, v9) = v25 & op2(v9, e22) = v127 & op2(v9, e20) = v128 & op2(v9, e20) = e22 & op2(v8, v24) = v86 & op2(v8, v8) = v89 & op2(v8, v8) = v24 & op2(v8, e21) = v87 & op2(v8, e20) = v88 & op2(v8, e20) = e21 & op2(v7, e20) = e20 & op2(e23, v13) = v166 & op2(e23, v13) = v108 & op2(e23, v11) = v180 & op2(e23, v11) = v148 & op2(e23, e23) = e20 & op2(e23, e22) = e21 & op2(e23, e21) = e22 & op2(e23, e20) = e23 & op2(e22, v25) = v119 & op2(e22, v23) = v57 & op2(e22, v13) = v171 & op2(e22, v13) = v110 & op2(e22, v13) = v21 & op2(e22, v12) = v59 & op2(e22, v11) = v183 & op2(e22, v11) = v145 & op2(e22, v9) = v121 & op2(e22, v9) = v20 & op2(e22, e23) = e21 & op2(e22, e22) = v13 & op2(e22, e21) = e23 & op2(e22, e20) = v12 & op2(e21, v24) = v79 & op2(e21, v22) = v38 & op2(e21, v13) = v169 & op2(e21, v13) = v105 & op2(e21, v11) = v185 & op2(e21, v11) = v150 & op2(e21, v11) = v19 & op2(e21, v10) = v40 & op2(e21, v8) = v81 & op2(e21, v8) = v18 & op2(e21, e23) = e22 & op2(e21, e22) = e23 & op2(e21, e21) = v11 & op2(e21, e20) = v10 & op2(e20, v25) = v123 & op2(e20, v24) = v83 & op2(e20, v23) = v53 & op2(e20, v22) = v34 & op2(e20, v12) = v55 & op2(e20, v12) = v12 & op2(e20, v10) = v36 & op2(e20, v10) = v10 & op2(e20, v9) = v125 & op2(e20, v8) = v85 & op2(e20, v7) = v7 & op2(e20, e23) = e23 & op2(e20, e22) = v9 & op2(e20, e21) = v8 & op2(e20, e20) = v7 & ! [v186] : ! [v187] : ! [v188] : ! [v189] : (v187 = v186 | ~ (op1(v189, v188) = v187) | ~ (op1(v189, v188) = v186)) & ! [v186] : ! [v187] : ! [v188] : ! [v189] : (v187 = v186 | ~ (op2(v189, v188) = v187) | ~ (op2(v189, v188) = v186)) & ! [v186] : ! [v187] : ! [v188] : (v187 = v186 | ~ (h1(v188) = v187) | ~ (h1(v188) = v186)) & ! [v186] : ! [v187] : ! [v188] : (v187 = v186 | ~ (h2(v188) = v187) | ~ (h2(v188) = v186)) & ! [v186] : ! [v187] : ! [v188] : (v187 = v186 | ~ (h3(v188) = v187) | ~ (h3(v188) = v186)) & ! [v186] : ! [v187] : ! [v188] : (v187 = v186 | ~ (h4(v188) = v187) | ~ (h4(v188) = v186)) & ! [v186] : ! [v187] : ! [v188] : (v187 = v186 | ~ (h5(v188) = v187) | ~ (h5(v188) = v186)) & ! [v186] : ! [v187] : ! [v188] : (v187 = v186 | ~ (h6(v188) = v187) | ~ (h6(v188) = v186)) & ! [v186] : ! [v187] : ! [v188] : (v187 = v186 | ~ (h7(v188) = v187) | ~ (h7(v188) = v186)) & ! [v186] : ! [v187] : ! [v188] : (v187 = v186 | ~ (h8(v188) = v187) | ~ (h8(v188) = v186)) & ! [v186] : ! [v187] : ! [v188] : (v187 = v186 | ~ (h9(v188) = v187) | ~ (h9(v188) = v186)) & ! [v186] : ! [v187] : ! [v188] : (v187 = v186 | ~ (h10(v188) = v187) | ~ (h10(v188) = v186)) & ! [v186] : ! [v187] : ! [v188] : (v187 = v186 | ~ (h11(v188) = v187) | ~ (h11(v188) = v186)) & ! [v186] : ! [v187] : ! [v188] : (v187 = v186 | ~ (h12(v188) = v187) | ~ (h12(v188) = v186)) & ( ~ (v185 = e21) | ~ (v184 = v13) | ~ (v183 = v182) | ~ (v181 = e20) | ~ (v180 = v179) | ~ (v178 = e21) | ~ (v177 = v176) | ~ (v175 = v174) | ~ (v173 = v172) | ~ (v11 = e20)) & ( ~ (v171 = e22) | ~ (v170 = v11) | ~ (v169 = v168) | ~ (v167 = e20) | ~ (v166 = v165) | ~ (v164 = e22) | ~ (v163 = v162) | ~ (v161 = v160) | ~ (v159 = v158) | ~ (v13 = e20)) & ( ~ (v150 = e21) | ~ (v149 = e20) | ~ (v148 = v147) | ~ (v146 = v13) | ~ (v145 = v144) | ~ (v143 = e21) | ~ (v142 = v141) | ~ (v140 = v139) | ~ (v138 = v137) | ~ (v11 = e20)) & ( ~ (v136 = v11) | ~ (v135 = v10) | ~ (v134 = v13) | ~ (v133 = v12) | ~ (v132 = v8) | ~ (v131 = v9) | ~ (v130 = v7)) & ( ~ (v110 = e22) | ~ (v109 = e20) | ~ (v108 = v107) | ~ (v106 = v11) | ~ (v105 = v104) | ~ (v103 = e22) | ~ (v102 = v101) | ~ (v100 = v99) | ~ (v98 = v97) | ~ (v13 = e20)) & ( ~ (v96 = v13) | ~ (v95 = v12) | ~ (v94 = v11) | ~ (v93 = v10) | ~ (v92 = v9) | ~ (v91 = v8) | ~ (v90 = v7)) & (v13 = e22 | v13 = e20) & (v13 = e22 | v12 = e22) & (v13 = e22 | v9 = e22) & (v13 = e20 | v12 = e20) & (v13 = e20 | v9 = e20) & (v12 = e22 | v12 = e20) & (v12 = e22 | v7 = e22) & (v12 = e20 | v10 = e20 | v7 = e20) & (v11 = e21 | v11 = e20) & (v11 = e21 | v10 = e21) & (v11 = e21 | v8 = e21) & (v11 = e20 | v10 = e20) & (v11 = e20 | v8 = e20) & (v10 = e21 | v10 = e20) & (v10 = e21 | v7 = e21) & (v9 = e22 | v9 = e20) & (v9 = e22 | v7 = e22) & (v9 = e20 | v8 = e20 | v7 = e20) & (v8 = e21 | v8 = e20) & (v8 = e21 | v7 = e21) & (v7 = e22 | v7 = e21 | v7 = e20) & (v6 = e12 | v6 = e10) & (v6 = e12 | v5 = e12) & (v6 = e12 | v2 = e12) & (v6 = e10 | v5 = e10) & (v6 = e10 | v2 = e10) & (v5 = e12 | v5 = e10) & (v5 = e12 | v0 = e12) & (v5 = e10 | v3 = e10 | v0 = e10) & (v4 = e11 | v4 = e10) & (v4 = e11 | v3 = e11) & (v4 = e11 | v1 = e11) & (v4 = e10 | v3 = e10) & (v4 = e10 | v1 = e10) & (v3 = e11 | v3 = e10) & (v3 = e11 | v0 = e11) & (v2 = e12 | v2 = e10) & (v2 = e12 | v0 = e12) & (v2 = e10 | v1 = e10 | v0 = e10) & (v1 = e11 | v1 = e10) & (v1 = e11 | v0 = e11) & (v0 = e12 | v0 = e11 | v0 = e10)) % 10.90/2.92 | 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, all_0_139_139, all_0_140_140, all_0_141_141, all_0_142_142, all_0_143_143, all_0_144_144, all_0_145_145, all_0_146_146, all_0_147_147, all_0_148_148, all_0_149_149, all_0_150_150, all_0_151_151, all_0_152_152, all_0_153_153, all_0_154_154, all_0_155_155, all_0_156_156, all_0_157_157, all_0_158_158, all_0_159_159, all_0_160_160, all_0_161_161, all_0_162_162, all_0_163_163, all_0_164_164, all_0_165_165, all_0_166_166, all_0_167_167, all_0_168_168, all_0_169_169, all_0_170_170, all_0_171_171, all_0_172_172, all_0_173_173, all_0_174_174, all_0_175_175, all_0_176_176, all_0_177_177, all_0_178_178, all_0_179_179, all_0_180_180, all_0_181_181, all_0_182_182, all_0_183_183, all_0_184_184, all_0_185_185 yields: % 10.90/2.92 | (1) ~ (all_0_172_172 = all_0_173_173) & ~ (all_0_172_172 = all_0_176_176) & ~ (all_0_172_172 = e23) & ~ (all_0_172_172 = e21) & ~ (all_0_173_173 = all_0_175_175) & ~ (all_0_173_173 = all_0_178_178) & ~ (all_0_173_173 = e23) & ~ (all_0_173_173 = e21) & ~ (all_0_174_174 = all_0_175_175) & ~ (all_0_174_174 = all_0_177_177) & ~ (all_0_174_174 = e23) & ~ (all_0_174_174 = e22) & ~ (all_0_175_175 = all_0_178_178) & ~ (all_0_175_175 = e23) & ~ (all_0_175_175 = e22) & ~ (all_0_176_176 = all_0_177_177) & ~ (all_0_176_176 = all_0_178_178) & ~ (all_0_176_176 = e23) & ~ (all_0_176_176 = e21) & ~ (all_0_177_177 = all_0_178_178) & ~ (all_0_177_177 = e23) & ~ (all_0_177_177 = e22) & ~ (all_0_178_178 = e23) & ~ (all_0_179_179 = all_0_180_180) & ~ (all_0_179_179 = all_0_183_183) & ~ (all_0_179_179 = e13) & ~ (all_0_179_179 = e11) & ~ (all_0_180_180 = all_0_182_182) & ~ (all_0_180_180 = all_0_185_185) & ~ (all_0_180_180 = e13) & ~ (all_0_180_180 = e11) & ~ (all_0_181_181 = all_0_182_182) & ~ (all_0_181_181 = all_0_184_184) & ~ (all_0_181_181 = e13) & ~ (all_0_181_181 = e12) & ~ (all_0_182_182 = all_0_185_185) & ~ (all_0_182_182 = e13) & ~ (all_0_182_182 = e12) & ~ (all_0_183_183 = all_0_184_184) & ~ (all_0_183_183 = all_0_185_185) & ~ (all_0_183_183 = e13) & ~ (all_0_183_183 = e11) & ~ (all_0_184_184 = all_0_185_185) & ~ (all_0_184_184 = e13) & ~ (all_0_184_184 = e12) & ~ (all_0_185_185 = e13) & ~ (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(all_0_179_179, e12) = e12 & op1(all_0_180_180, e12) = e10 & op1(all_0_181_181, e11) = e11 & op1(all_0_182_182, e11) = e10 & op1(all_0_183_183, e10) = e12 & op1(all_0_184_184, e10) = e11 & op1(all_0_185_185, e10) = e10 & op1(e13, e13) = e10 & op1(e13, e12) = e11 & op1(e13, e11) = e12 & op1(e13, e10) = e13 & op1(e12, all_0_179_179) = all_0_168_168 & op1(e12, all_0_183_183) = all_0_169_169 & op1(e12, e13) = e11 & op1(e12, e12) = all_0_179_179 & op1(e12, e11) = e13 & op1(e12, e10) = all_0_180_180 & op1(e11, all_0_181_181) = all_0_170_170 & op1(e11, all_0_184_184) = all_0_171_171 & op1(e11, e13) = e12 & op1(e11, e12) = e13 & op1(e11, e11) = all_0_181_181 & op1(e11, e10) = all_0_182_182 & op1(e10, all_0_180_180) = all_0_180_180 & op1(e10, all_0_182_182) = all_0_182_182 & op1(e10, all_0_185_185) = all_0_185_185 & op1(e10, e13) = e13 & op1(e10, e12) = all_0_183_183 & op1(e10, e11) = all_0_184_184 & op1(e10, e10) = all_0_185_185 & h1(all_0_179_179) = all_0_146_146 & h1(all_0_180_180) = all_0_148_148 & h1(all_0_181_181) = all_0_150_150 & h1(all_0_182_182) = all_0_152_152 & h1(all_0_183_183) = all_0_155_155 & h1(all_0_184_184) = all_0_157_157 & h1(all_0_185_185) = all_0_159_159 & h1(e13) = all_0_175_175 & h1(e12) = e21 & h1(e11) = e20 & h1(e10) = all_0_163_163 & h2(all_0_179_179) = all_0_127_127 & h2(all_0_180_180) = all_0_129_129 & h2(all_0_181_181) = all_0_131_131 & h2(all_0_182_182) = all_0_133_133 & h2(all_0_183_183) = all_0_136_136 & h2(all_0_184_184) = all_0_138_138 & h2(all_0_185_185) = all_0_140_140 & h2(e13) = all_0_173_173 & h2(e12) = e22 & h2(e11) = e20 & h2(e10) = all_0_162_162 & h3(all_0_179_179) = all_0_115_115 & h3(all_0_180_180) = all_0_116_116 & h3(all_0_181_181) = all_0_117_117 & h3(all_0_182_182) = all_0_118_118 & h3(all_0_183_183) = all_0_119_119 & h3(all_0_184_184) = all_0_120_120 & h3(all_0_185_185) = all_0_121_121 & h3(e13) = e23 & h3(e12) = e23 & h3(e11) = e20 & h3(e10) = e20 & h4(all_0_179_179) = all_0_101_101 & h4(all_0_180_180) = all_0_103_103 & h4(all_0_181_181) = all_0_105_105 & h4(all_0_182_182) = all_0_107_107 & h4(all_0_183_183) = all_0_110_110 & h4(all_0_184_184) = all_0_112_112 & h4(all_0_185_185) = all_0_114_114 & h4(e13) = all_0_177_177 & h4(e12) = e20 & h4(e11) = e21 & h4(e10) = all_0_161_161 & h5(all_0_179_179) = all_0_89_89 & h5(all_0_180_180) = all_0_90_90 & h5(all_0_181_181) = all_0_91_91 & h5(all_0_182_182) = all_0_92_92 & h5(all_0_183_183) = all_0_93_93 & h5(all_0_184_184) = all_0_94_94 & h5(all_0_185_185) = all_0_95_95 & h5(e13) = e23 & h5(e12) = e22 & h5(e11) = e21 & h5(e10) = e20 & h6(all_0_179_179) = all_0_76_76 & h6(all_0_180_180) = all_0_78_78 & h6(all_0_181_181) = all_0_79_79 & h6(all_0_182_182) = all_0_81_81 & h6(all_0_183_183) = all_0_84_84 & h6(all_0_184_184) = all_0_86_86 & h6(all_0_185_185) = all_0_88_88 & h6(e13) = e22 & h6(e12) = e23 & h6(e11) = e21 & h6(e10) = all_0_172_172 & h7(all_0_179_179) = all_0_61_61 & h7(all_0_180_180) = all_0_63_63 & h7(all_0_181_181) = all_0_65_65 & h7(all_0_182_182) = all_0_67_67 & h7(all_0_183_183) = all_0_70_70 & h7(all_0_184_184) = all_0_72_72 & h7(all_0_185_185) = all_0_74_74 & h7(e13) = all_0_176_176 & h7(e12) = e20 & h7(e11) = e22 & h7(e10) = all_0_160_160 & h8(all_0_179_179) = all_0_49_49 & h8(all_0_180_180) = all_0_50_50 & h8(all_0_181_181) = all_0_51_51 & h8(all_0_182_182) = all_0_52_52 & h8(all_0_183_183) = all_0_53_53 & h8(all_0_184_184) = all_0_54_54 & h8(all_0_185_185) = all_0_55_55 & h8(e13) = e23 & h8(e12) = e21 & h8(e11) = e22 & h8(e10) = e20 & h9(all_0_179_179) = all_0_36_36 & h9(all_0_180_180) = all_0_38_38 & h9(all_0_181_181) = all_0_39_39 & h9(all_0_182_182) = all_0_41_41 & h9(all_0_183_183) = all_0_44_44 & h9(all_0_184_184) = all_0_46_46 & h9(all_0_185_185) = all_0_48_48 & h9(e13) = e21 & h9(e12) = e23 & h9(e11) = e22 & h9(e10) = all_0_174_174 & h10(all_0_179_179) = all_0_28_28 & h10(all_0_180_180) = all_0_29_29 & h10(all_0_181_181) = all_0_30_30 & h10(all_0_182_182) = all_0_31_31 & h10(all_0_183_183) = all_0_32_32 & h10(all_0_184_184) = all_0_33_33 & h10(all_0_185_185) = all_0_34_34 & h10(e13) = e23 & h10(e12) = e20 & h10(e11) = e23 & h10(e10) = e20 & h11(all_0_179_179) = all_0_15_15 & h11(all_0_180_180) = all_0_17_17 & h11(all_0_181_181) = all_0_18_18 & h11(all_0_182_182) = all_0_20_20 & h11(all_0_183_183) = all_0_23_23 & h11(all_0_184_184) = all_0_25_25 & h11(all_0_185_185) = all_0_27_27 & h11(e13) = e22 & h11(e12) = e21 & h11(e11) = e23 & h11(e10) = all_0_172_172 & h12(all_0_179_179) = all_0_1_1 & h12(all_0_180_180) = all_0_3_3 & h12(all_0_181_181) = all_0_4_4 & h12(all_0_182_182) = all_0_6_6 & h12(all_0_183_183) = all_0_9_9 & h12(all_0_184_184) = all_0_11_11 & h12(all_0_185_185) = all_0_13_13 & h12(e13) = e21 & h12(e12) = e22 & h12(e11) = e23 & h12(e10) = all_0_174_174 & op2(all_0_160_160, all_0_160_160) = all_0_73_73 & op2(all_0_160_160, all_0_176_176) = all_0_68_68 & op2(all_0_160_160, e22) = all_0_71_71 & op2(all_0_160_160, e20) = all_0_69_69 & op2(all_0_161_161, all_0_161_161) = all_0_113_113 & op2(all_0_161_161, all_0_177_177) = all_0_108_108 & op2(all_0_161_161, e21) = all_0_111_111 & op2(all_0_161_161, e20) = all_0_109_109 & op2(all_0_162_162, all_0_162_162) = all_0_139_139 & op2(all_0_162_162, all_0_173_173) = all_0_134_134 & op2(all_0_162_162, e22) = all_0_135_135 & op2(all_0_162_162, e20) = all_0_137_137 & op2(all_0_163_163, all_0_163_163) = all_0_158_158 & op2(all_0_163_163, all_0_175_175) = all_0_153_153 & op2(all_0_163_163, e21) = all_0_154_154 & op2(all_0_163_163, e20) = all_0_156_156 & op2(all_0_172_172, all_0_172_172) = all_0_26_26 & op2(all_0_172_172, all_0_172_172) = all_0_87_87 & op2(all_0_172_172, e23) = all_0_24_24 & op2(all_0_172_172, e23) = all_0_83_83 & op2(all_0_172_172, e22) = all_0_21_21 & op2(all_0_172_172, e22) = all_0_82_82 & op2(all_0_172_172, e22) = e22 & op2(all_0_172_172, e21) = all_0_22_22 & op2(all_0_172_172, e21) = all_0_85_85 & op2(all_0_173_173, all_0_162_162) = all_0_125_125 & op2(all_0_173_173, all_0_173_173) = all_0_122_122 & op2(all_0_173_173, all_0_173_173) = all_0_162_162 & op2(all_0_173_173, e22) = all_0_123_123 & op2(all_0_173_173, e22) = e20 & op2(all_0_173_173, e20) = all_0_124_124 & op2(all_0_174_174, all_0_174_174) = all_0_12_12 & op2(all_0_174_174, all_0_174_174) = all_0_47_47 & op2(all_0_174_174, e23) = all_0_10_10 & op2(all_0_174_174, e23) = all_0_43_43 & op2(all_0_174_174, e22) = all_0_8_8 & op2(all_0_174_174, e22) = all_0_45_45 & op2(all_0_174_174, e21) = all_0_7_7 & op2(all_0_174_174, e21) = all_0_42_42 & op2(all_0_174_174, e21) = e21 & op2(all_0_175_175, all_0_163_163) = all_0_144_144 & op2(all_0_175_175, all_0_175_175) = all_0_141_141 & op2(all_0_175_175, all_0_175_175) = all_0_163_163 & op2(all_0_175_175, e21) = all_0_142_142 & op2(all_0_175_175, e21) = e20 & op2(all_0_175_175, e20) = all_0_143_143 & op2(all_0_176_176, all_0_160_160) = all_0_59_59 & op2(all_0_176_176, all_0_176_176) = all_0_56_56 & op2(all_0_176_176, all_0_176_176) = all_0_160_160 & op2(all_0_176_176, e22) = all_0_58_58 & op2(all_0_176_176, e20) = all_0_57_57 & op2(all_0_176_176, e20) = e22 & op2(all_0_177_177, all_0_161_161) = all_0_99_99 & op2(all_0_177_177, all_0_177_177) = all_0_96_96 & op2(all_0_177_177, all_0_177_177) = all_0_161_161 & op2(all_0_177_177, e21) = all_0_98_98 & op2(all_0_177_177, e20) = all_0_97_97 & op2(all_0_177_177, e20) = e21 & op2(all_0_178_178, e20) = e20 & op2(e23, all_0_172_172) = all_0_19_19 & op2(e23, all_0_172_172) = all_0_77_77 & op2(e23, all_0_174_174) = all_0_5_5 & op2(e23, all_0_174_174) = all_0_37_37 & op2(e23, e23) = e20 & op2(e23, e22) = e21 & op2(e23, e21) = e22 & op2(e23, e20) = e23 & op2(e22, all_0_160_160) = all_0_66_66 & op2(e22, all_0_162_162) = all_0_128_128 & op2(e22, all_0_172_172) = all_0_14_14 & op2(e22, all_0_172_172) = all_0_75_75 & op2(e22, all_0_172_172) = all_0_164_164 & op2(e22, all_0_173_173) = all_0_126_126 & op2(e22, all_0_174_174) = all_0_2_2 & op2(e22, all_0_174_174) = all_0_40_40 & op2(e22, all_0_176_176) = all_0_64_64 & op2(e22, all_0_176_176) = all_0_165_165 & op2(e22, e23) = e21 & op2(e22, e22) = all_0_172_172 & op2(e22, e21) = e23 & op2(e22, e20) = all_0_173_173 & op2(e21, all_0_161_161) = all_0_106_106 & op2(e21, all_0_163_163) = all_0_147_147 & op2(e21, all_0_172_172) = all_0_16_16 & op2(e21, all_0_172_172) = all_0_80_80 & op2(e21, all_0_174_174) = all_0_0_0 & op2(e21, all_0_174_174) = all_0_35_35 & op2(e21, all_0_174_174) = all_0_166_166 & op2(e21, all_0_175_175) = all_0_145_145 & op2(e21, all_0_177_177) = all_0_104_104 & op2(e21, all_0_177_177) = all_0_167_167 & op2(e21, e23) = e22 & op2(e21, e22) = e23 & op2(e21, e21) = all_0_174_174 & op2(e21, e20) = all_0_175_175 & op2(e20, all_0_160_160) = all_0_62_62 & op2(e20, all_0_161_161) = all_0_102_102 & op2(e20, all_0_162_162) = all_0_132_132 & op2(e20, all_0_163_163) = all_0_151_151 & op2(e20, all_0_173_173) = all_0_130_130 & op2(e20, all_0_173_173) = all_0_173_173 & op2(e20, all_0_175_175) = all_0_149_149 & op2(e20, all_0_175_175) = all_0_175_175 & op2(e20, all_0_176_176) = all_0_60_60 & op2(e20, all_0_177_177) = all_0_100_100 & op2(e20, all_0_178_178) = all_0_178_178 & op2(e20, e23) = e23 & op2(e20, e22) = all_0_176_176 & op2(e20, e21) = all_0_177_177 & op2(e20, e20) = all_0_178_178 & ! [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)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h5(v2) = v1) | ~ (h5(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h6(v2) = v1) | ~ (h6(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h7(v2) = v1) | ~ (h7(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h8(v2) = v1) | ~ (h8(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h9(v2) = v1) | ~ (h9(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h10(v2) = v1) | ~ (h10(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h11(v2) = v1) | ~ (h11(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h12(v2) = v1) | ~ (h12(v2) = v0)) & ( ~ (all_0_0_0 = e21) | ~ (all_0_1_1 = all_0_172_172) | ~ (all_0_2_2 = all_0_3_3) | ~ (all_0_4_4 = e20) | ~ (all_0_5_5 = all_0_6_6) | ~ (all_0_7_7 = e21) | ~ (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_174_174 = e20)) & ( ~ (all_0_14_14 = e22) | ~ (all_0_15_15 = all_0_174_174) | ~ (all_0_16_16 = all_0_17_17) | ~ (all_0_18_18 = e20) | ~ (all_0_19_19 = all_0_20_20) | ~ (all_0_21_21 = e22) | ~ (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_172_172 = e20)) & ( ~ (all_0_35_35 = e21) | ~ (all_0_36_36 = e20) | ~ (all_0_37_37 = all_0_38_38) | ~ (all_0_39_39 = all_0_172_172) | ~ (all_0_40_40 = all_0_41_41) | ~ (all_0_42_42 = e21) | ~ (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_174_174 = e20)) & ( ~ (all_0_49_49 = all_0_174_174) | ~ (all_0_50_50 = all_0_175_175) | ~ (all_0_51_51 = all_0_172_172) | ~ (all_0_52_52 = all_0_173_173) | ~ (all_0_53_53 = all_0_177_177) | ~ (all_0_54_54 = all_0_176_176) | ~ (all_0_55_55 = all_0_178_178)) & ( ~ (all_0_75_75 = e22) | ~ (all_0_76_76 = e20) | ~ (all_0_77_77 = all_0_78_78) | ~ (all_0_79_79 = all_0_174_174) | ~ (all_0_80_80 = all_0_81_81) | ~ (all_0_82_82 = e22) | ~ (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_172_172 = e20)) & ( ~ (all_0_89_89 = all_0_172_172) | ~ (all_0_90_90 = all_0_173_173) | ~ (all_0_91_91 = all_0_174_174) | ~ (all_0_92_92 = all_0_175_175) | ~ (all_0_93_93 = all_0_176_176) | ~ (all_0_94_94 = all_0_177_177) | ~ (all_0_95_95 = all_0_178_178)) & (all_0_172_172 = e22 | all_0_172_172 = e20) & (all_0_172_172 = e22 | all_0_173_173 = e22) & (all_0_172_172 = e22 | all_0_176_176 = e22) & (all_0_172_172 = e20 | all_0_173_173 = e20) & (all_0_172_172 = e20 | all_0_176_176 = e20) & (all_0_173_173 = e22 | all_0_173_173 = e20) & (all_0_173_173 = e22 | all_0_178_178 = e22) & (all_0_173_173 = e20 | all_0_175_175 = e20 | all_0_178_178 = e20) & (all_0_174_174 = e21 | all_0_174_174 = e20) & (all_0_174_174 = e21 | all_0_175_175 = e21) & (all_0_174_174 = e21 | all_0_177_177 = e21) & (all_0_174_174 = e20 | all_0_175_175 = e20) & (all_0_174_174 = e20 | all_0_177_177 = e20) & (all_0_175_175 = e21 | all_0_175_175 = e20) & (all_0_175_175 = e21 | all_0_178_178 = e21) & (all_0_176_176 = e22 | all_0_176_176 = e20) & (all_0_176_176 = e22 | all_0_178_178 = e22) & (all_0_176_176 = e20 | all_0_177_177 = e20 | all_0_178_178 = e20) & (all_0_177_177 = e21 | all_0_177_177 = e20) & (all_0_177_177 = e21 | all_0_178_178 = e21) & (all_0_178_178 = e22 | all_0_178_178 = e21 | all_0_178_178 = e20) & (all_0_179_179 = e12 | all_0_179_179 = e10) & (all_0_179_179 = e12 | all_0_180_180 = e12) & (all_0_179_179 = e12 | all_0_183_183 = e12) & (all_0_179_179 = e10 | all_0_180_180 = e10) & (all_0_179_179 = e10 | all_0_183_183 = e10) & (all_0_180_180 = e12 | all_0_180_180 = e10) & (all_0_180_180 = e12 | all_0_185_185 = e12) & (all_0_180_180 = e10 | all_0_182_182 = e10 | all_0_185_185 = e10) & (all_0_181_181 = e11 | all_0_181_181 = e10) & (all_0_181_181 = e11 | all_0_182_182 = e11) & (all_0_181_181 = e11 | all_0_184_184 = e11) & (all_0_181_181 = e10 | all_0_182_182 = e10) & (all_0_181_181 = e10 | all_0_184_184 = e10) & (all_0_182_182 = e11 | all_0_182_182 = e10) & (all_0_182_182 = e11 | all_0_185_185 = e11) & (all_0_183_183 = e12 | all_0_183_183 = e10) & (all_0_183_183 = e12 | all_0_185_185 = e12) & (all_0_183_183 = e10 | all_0_184_184 = e10 | all_0_185_185 = e10) & (all_0_184_184 = e11 | all_0_184_184 = e10) & (all_0_184_184 = e11 | all_0_185_185 = e11) & (all_0_185_185 = e12 | all_0_185_185 = e11 | all_0_185_185 = e10) % 10.90/2.94 | % 10.90/2.94 | Applying alpha-rule on (1) yields: % 10.90/2.94 | (2) h10(all_0_183_183) = all_0_32_32 % 10.90/2.94 | (3) op2(all_0_173_173, all_0_162_162) = all_0_125_125 % 10.90/2.94 | (4) op2(e22, all_0_173_173) = all_0_126_126 % 10.90/2.94 | (5) op2(all_0_160_160, e20) = all_0_69_69 % 10.90/2.94 | (6) op2(e21, all_0_163_163) = all_0_147_147 % 10.90/2.94 | (7) h6(all_0_183_183) = all_0_84_84 % 10.90/2.94 | (8) op2(all_0_173_173, e22) = all_0_123_123 % 10.90/2.94 | (9) op2(all_0_174_174, e21) = e21 % 10.90/2.94 | (10) h3(all_0_184_184) = all_0_120_120 % 10.90/2.94 | (11) ~ (all_0_14_14 = e22) | ~ (all_0_15_15 = all_0_174_174) | ~ (all_0_16_16 = all_0_17_17) | ~ (all_0_18_18 = e20) | ~ (all_0_19_19 = all_0_20_20) | ~ (all_0_21_21 = e22) | ~ (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_172_172 = e20) % 10.90/2.94 | (12) all_0_175_175 = e21 | all_0_178_178 = e21 % 10.90/2.94 | (13) op2(all_0_174_174, e21) = all_0_7_7 % 10.90/2.94 | (14) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h11(v2) = v1) | ~ (h11(v2) = v0)) % 10.90/2.94 | (15) op2(e20, all_0_176_176) = all_0_60_60 % 10.90/2.94 | (16) op2(all_0_177_177, e20) = all_0_97_97 % 10.90/2.94 | (17) h1(all_0_183_183) = all_0_155_155 % 10.90/2.94 | (18) h2(all_0_184_184) = all_0_138_138 % 10.90/2.94 | (19) h8(all_0_182_182) = all_0_52_52 % 10.90/2.94 | (20) op1(e10, e12) = all_0_183_183 % 10.90/2.94 | (21) op2(e21, e20) = all_0_175_175 % 10.90/2.94 | (22) all_0_183_183 = e12 | all_0_185_185 = e12 % 10.90/2.94 | (23) op2(all_0_161_161, e21) = all_0_111_111 % 10.90/2.94 | (24) h8(all_0_185_185) = all_0_55_55 % 10.90/2.94 | (25) h8(all_0_179_179) = all_0_49_49 % 10.90/2.94 | (26) h11(all_0_179_179) = all_0_15_15 % 10.90/2.94 | (27) ~ (all_0_182_182 = e12) % 10.90/2.94 | (28) ~ (e23 = e22) % 10.90/2.94 | (29) op1(e11, e13) = e12 % 10.90/2.94 | (30) op2(e22, all_0_174_174) = all_0_2_2 % 10.90/2.94 | (31) op1(e12, all_0_179_179) = all_0_168_168 % 10.90/2.94 | (32) op2(e20, all_0_175_175) = all_0_175_175 % 10.90/2.94 | (33) op2(all_0_174_174, e23) = all_0_10_10 % 10.90/2.94 | (34) ~ (e21 = e10) % 10.90/2.94 | (35) op2(all_0_175_175, all_0_163_163) = all_0_144_144 % 10.90/2.94 | (36) h4(e10) = all_0_161_161 % 10.90/2.94 | (37) op2(e22, all_0_172_172) = all_0_164_164 % 10.90/2.94 | (38) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h8(v2) = v1) | ~ (h8(v2) = v0)) % 10.90/2.94 | (39) op2(all_0_160_160, all_0_160_160) = all_0_73_73 % 10.90/2.94 | (40) h11(all_0_184_184) = all_0_25_25 % 10.90/2.94 | (41) ~ (all_0_181_181 = all_0_182_182) % 10.90/2.94 | (42) op2(e23, e20) = e23 % 10.90/2.94 | (43) h3(all_0_182_182) = all_0_118_118 % 10.90/2.94 | (44) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h1(v2) = v1) | ~ (h1(v2) = v0)) % 10.90/2.94 | (45) h6(e12) = e23 % 10.90/2.94 | (46) h10(e11) = e23 % 10.90/2.94 | (47) ~ (e22 = e11) % 10.90/2.94 | (48) all_0_174_174 = e20 | all_0_175_175 = e20 % 10.90/2.94 | (49) op2(all_0_163_163, all_0_163_163) = all_0_158_158 % 10.90/2.94 | (50) op2(all_0_173_173, e22) = e20 % 10.90/2.94 | (51) h7(e13) = all_0_176_176 % 10.90/2.94 | (52) op1(e12, e13) = e11 % 10.90/2.94 | (53) ~ (all_0_174_174 = e23) % 10.90/2.94 | (54) ~ (all_0_174_174 = e22) % 10.90/2.94 | (55) op2(all_0_178_178, e20) = e20 % 10.90/2.94 | (56) op1(e10, e11) = all_0_184_184 % 10.90/2.94 | (57) op2(all_0_174_174, all_0_174_174) = all_0_12_12 % 10.90/2.94 | (58) h3(all_0_179_179) = all_0_115_115 % 10.90/2.94 | (59) op2(e21, all_0_174_174) = all_0_0_0 % 10.90/2.94 | (60) op2(all_0_177_177, e21) = all_0_98_98 % 10.90/2.94 | (61) ~ (all_0_183_183 = e11) % 10.90/2.94 | (62) ~ (all_0_180_180 = all_0_182_182) % 10.90/2.94 | (63) h2(e12) = e22 % 10.90/2.94 | (64) h4(all_0_181_181) = all_0_105_105 % 10.90/2.94 | (65) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h10(v2) = v1) | ~ (h10(v2) = v0)) % 10.90/2.94 | (66) h1(all_0_182_182) = all_0_152_152 % 10.90/2.94 | (67) h7(all_0_181_181) = all_0_65_65 % 10.90/2.94 | (68) h11(e13) = e22 % 10.90/2.94 | (69) op2(all_0_162_162, e22) = all_0_135_135 % 10.90/2.94 | (70) all_0_181_181 = e11 | all_0_182_182 = e11 % 10.90/2.94 | (71) all_0_173_173 = e22 | all_0_178_178 = e22 % 10.90/2.94 | (72) op2(e22, e21) = e23 % 10.90/2.94 | (73) op2(e23, e23) = e20 % 10.90/2.94 | (74) h12(all_0_184_184) = all_0_11_11 % 10.90/2.94 | (75) op2(e20, e22) = all_0_176_176 % 10.90/2.94 | (76) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h5(v2) = v1) | ~ (h5(v2) = v0)) % 10.90/2.94 | (77) op2(all_0_175_175, all_0_175_175) = all_0_163_163 % 10.90/2.94 | (78) op2(e23, e22) = e21 % 10.90/2.94 | (79) op2(all_0_176_176, all_0_160_160) = all_0_59_59 % 10.90/2.94 | (80) h5(e13) = e23 % 10.90/2.94 | (81) h6(all_0_180_180) = all_0_78_78 % 10.90/2.94 | (82) h10(all_0_185_185) = all_0_34_34 % 10.90/2.94 | (83) h2(all_0_183_183) = all_0_136_136 % 10.90/2.94 | (84) ~ (all_0_182_182 = all_0_185_185) % 10.90/2.94 | (85) all_0_172_172 = e20 | all_0_173_173 = e20 % 10.90/2.94 | (86) h5(all_0_185_185) = all_0_95_95 % 10.90/2.94 | (87) ~ (all_0_179_179 = e13) % 10.90/2.94 | (88) op2(e20, all_0_178_178) = all_0_178_178 % 10.90/2.94 | (89) all_0_174_174 = e21 | all_0_175_175 = e21 % 10.90/2.94 | (90) op2(all_0_172_172, e21) = all_0_85_85 % 10.90/2.94 | (91) h10(all_0_180_180) = all_0_29_29 % 10.90/2.94 | (92) op2(e23, all_0_172_172) = all_0_77_77 % 10.90/2.94 | (93) h3(e11) = e20 % 10.90/2.94 | (94) h8(all_0_183_183) = all_0_53_53 % 10.90/2.94 | (95) op2(all_0_174_174, e23) = all_0_43_43 % 10.90/2.94 | (96) h7(all_0_182_182) = all_0_67_67 % 10.90/2.95 | (97) op2(all_0_174_174, e21) = all_0_42_42 % 10.90/2.95 | (98) h9(e13) = e21 % 10.90/2.95 | (99) ~ (all_0_185_185 = e13) % 10.90/2.95 | (100) op2(all_0_174_174, e22) = all_0_8_8 % 10.90/2.95 | (101) h5(e10) = e20 % 10.90/2.95 | (102) h12(e12) = e22 % 10.90/2.95 | (103) h8(e10) = e20 % 10.90/2.95 | (104) h6(e11) = e21 % 10.90/2.95 | (105) op2(all_0_175_175, all_0_175_175) = all_0_141_141 % 10.90/2.95 | (106) ~ (all_0_180_180 = all_0_185_185) % 10.90/2.95 | (107) h3(e13) = e23 % 10.90/2.95 | (108) op2(e21, e21) = all_0_174_174 % 10.90/2.95 | (109) op1(all_0_185_185, e10) = e10 % 10.90/2.95 | (110) h9(all_0_185_185) = all_0_48_48 % 10.90/2.95 | (111) ~ (all_0_184_184 = e13) % 10.90/2.95 | (112) op1(e12, e11) = e13 % 10.90/2.95 | (113) h3(all_0_181_181) = all_0_117_117 % 10.90/2.95 | (114) ~ (all_0_177_177 = e23) % 10.90/2.95 | (115) ~ (all_0_75_75 = e22) | ~ (all_0_76_76 = e20) | ~ (all_0_77_77 = all_0_78_78) | ~ (all_0_79_79 = all_0_174_174) | ~ (all_0_80_80 = all_0_81_81) | ~ (all_0_82_82 = e22) | ~ (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_172_172 = e20) % 10.90/2.95 | (116) ~ (all_0_181_181 = e13) % 10.90/2.95 | (117) h4(e11) = e21 % 10.90/2.95 | (118) ~ (e23 = e13) % 10.90/2.95 | (119) h10(e10) = e20 % 10.90/2.95 | (120) ~ (all_0_173_173 = e23) % 10.90/2.95 | (121) ~ (all_0_173_173 = all_0_175_175) % 10.90/2.95 | (122) op2(e21, all_0_174_174) = all_0_35_35 % 10.90/2.95 | (123) all_0_179_179 = e10 | all_0_183_183 = e10 % 10.90/2.95 | (124) op2(all_0_177_177, e20) = e21 % 10.90/2.95 | (125) h7(e11) = e22 % 10.90/2.95 | (126) op1(e12, all_0_183_183) = all_0_169_169 % 10.90/2.95 | (127) ~ (all_0_174_174 = all_0_177_177) % 10.90/2.95 | (128) all_0_174_174 = e20 | all_0_177_177 = e20 % 10.90/2.95 | (129) op2(e22, all_0_160_160) = all_0_66_66 % 10.90/2.95 | (130) h1(all_0_181_181) = all_0_150_150 % 10.90/2.95 | (131) ~ (e22 = e20) % 10.90/2.95 | (132) h8(all_0_184_184) = all_0_54_54 % 10.90/2.95 | (133) all_0_185_185 = e12 | all_0_185_185 = e11 | all_0_185_185 = e10 % 10.90/2.95 | (134) op1(all_0_179_179, e12) = e12 % 10.90/2.95 | (135) h6(all_0_184_184) = all_0_86_86 % 10.90/2.95 | (136) all_0_172_172 = e20 | all_0_176_176 = e20 % 10.90/2.95 | (137) ~ (all_0_181_181 = all_0_184_184) % 10.90/2.95 | (138) h8(all_0_181_181) = all_0_51_51 % 10.90/2.95 | (139) op2(all_0_176_176, e20) = all_0_57_57 % 10.90/2.95 | (140) h5(all_0_181_181) = all_0_91_91 % 10.90/2.95 | (141) h6(e13) = e22 % 10.90/2.95 | (142) op2(all_0_163_163, all_0_175_175) = all_0_153_153 % 10.90/2.95 | (143) op2(all_0_177_177, all_0_161_161) = all_0_99_99 % 10.90/2.95 | (144) ~ (all_0_180_180 = e11) % 10.90/2.95 | (145) h11(all_0_180_180) = all_0_17_17 % 10.90/2.95 | (146) op2(e20, all_0_177_177) = all_0_100_100 % 10.90/2.95 | (147) all_0_180_180 = e12 | all_0_180_180 = e10 % 10.90/2.95 | (148) h3(e12) = e23 % 10.90/2.95 | (149) all_0_181_181 = e10 | all_0_184_184 = e10 % 10.90/2.95 | (150) op2(all_0_177_177, all_0_177_177) = all_0_161_161 % 10.90/2.95 | (151) op2(all_0_160_160, all_0_176_176) = all_0_68_68 % 10.90/2.95 | (152) op2(all_0_161_161, all_0_177_177) = all_0_108_108 % 10.90/2.95 | (153) op2(e21, all_0_172_172) = all_0_16_16 % 10.90/2.95 | (154) h12(e11) = e23 % 10.90/2.95 | (155) ~ (all_0_173_173 = all_0_178_178) % 10.90/2.95 | (156) h12(all_0_181_181) = all_0_4_4 % 10.90/2.95 | (157) h4(all_0_184_184) = all_0_112_112 % 10.90/2.95 | (158) op2(all_0_163_163, e20) = all_0_156_156 % 10.90/2.95 | (159) op2(all_0_175_175, e20) = all_0_143_143 % 10.90/2.95 | (160) all_0_179_179 = e10 | all_0_180_180 = e10 % 10.90/2.95 | (161) ~ (all_0_172_172 = e21) % 10.90/2.95 | (162) op1(all_0_181_181, e11) = e11 % 10.90/2.95 | (163) all_0_183_183 = e10 | all_0_184_184 = e10 | all_0_185_185 = e10 % 10.90/2.95 | (164) all_0_179_179 = e12 | all_0_183_183 = e12 % 10.90/2.95 | (165) op1(all_0_184_184, e10) = e11 % 10.90/2.95 | (166) all_0_177_177 = e21 | all_0_178_178 = e21 % 10.90/2.95 | (167) op2(e20, all_0_173_173) = all_0_130_130 % 10.90/2.95 | (168) all_0_183_183 = e12 | all_0_183_183 = e10 % 10.90/2.95 | (169) h11(all_0_185_185) = all_0_27_27 % 10.90/2.95 | (170) ~ (all_0_174_174 = all_0_175_175) % 10.90/2.95 | (171) op2(all_0_174_174, all_0_174_174) = all_0_47_47 % 10.90/2.95 | (172) op2(e22, all_0_176_176) = all_0_165_165 % 10.90/2.95 | (173) ~ (all_0_177_177 = all_0_178_178) % 10.90/2.95 | (174) h5(e12) = e22 % 10.90/2.95 | (175) h4(all_0_183_183) = all_0_110_110 % 10.90/2.95 | (176) h9(e11) = e22 % 10.90/2.95 | (177) ~ (e21 = e11) % 10.90/2.95 | (178) ~ (all_0_179_179 = all_0_183_183) % 10.90/2.95 | (179) op1(e13, e10) = e13 % 10.90/2.95 | (180) ~ (e12 = e10) % 10.90/2.95 | (181) op1(e11, all_0_181_181) = all_0_170_170 % 10.90/2.95 | (182) all_0_173_173 = e22 | all_0_173_173 = e20 % 10.90/2.95 | (183) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h4(v2) = v1) | ~ (h4(v2) = v0)) % 10.90/2.95 | (184) op2(all_0_172_172, e22) = e22 % 10.90/2.95 | (185) h11(all_0_181_181) = all_0_18_18 % 10.90/2.95 | (186) all_0_181_181 = e11 | all_0_184_184 = e11 % 10.90/2.95 | (187) ~ (e20 = e10) % 10.90/2.95 | (188) ~ (all_0_180_180 = e13) % 10.90/2.95 | (189) h5(all_0_183_183) = all_0_93_93 % 10.90/2.95 | (190) h10(all_0_184_184) = all_0_33_33 % 10.90/2.95 | (191) h9(all_0_182_182) = all_0_41_41 % 10.90/2.95 | (192) op2(e23, e21) = e22 % 10.90/2.95 | (193) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h3(v2) = v1) | ~ (h3(v2) = v0)) % 10.90/2.95 | (194) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op1(v3, v2) = v1) | ~ (op1(v3, v2) = v0)) % 10.90/2.95 | (195) h9(all_0_181_181) = all_0_39_39 % 10.90/2.95 | (196) all_0_174_174 = e21 | all_0_177_177 = e21 % 10.90/2.95 | (197) h6(e10) = all_0_172_172 % 10.90/2.95 | (198) h1(e12) = e21 % 10.90/2.95 | (199) op2(e21, all_0_172_172) = all_0_80_80 % 10.90/2.95 | (200) op2(e22, e20) = all_0_173_173 % 10.90/2.95 | (201) all_0_175_175 = e21 | all_0_175_175 = e20 % 10.90/2.95 | (202) op2(e22, e22) = all_0_172_172 % 10.90/2.95 | (203) op2(all_0_172_172, all_0_172_172) = all_0_26_26 % 10.90/2.95 | (204) h2(all_0_185_185) = all_0_140_140 % 10.90/2.95 | (205) h11(all_0_183_183) = all_0_23_23 % 10.90/2.95 | (206) h2(e13) = all_0_173_173 % 10.90/2.95 | (207) all_0_174_174 = e21 | all_0_174_174 = e20 % 10.90/2.95 | (208) ~ (all_0_183_183 = all_0_185_185) % 10.90/2.95 | (209) op2(all_0_175_175, e21) = all_0_142_142 % 10.90/2.95 | (210) op2(e21, all_0_161_161) = all_0_106_106 % 10.90/2.95 | (211) ~ (all_0_179_179 = all_0_180_180) % 10.90/2.95 | (212) h1(all_0_185_185) = all_0_159_159 % 10.90/2.95 | (213) ~ (all_0_173_173 = e21) % 10.90/2.95 | (214) h7(all_0_183_183) = all_0_70_70 % 10.90/2.95 | (215) ~ (all_0_176_176 = e23) % 10.90/2.95 | (216) op2(e20, all_0_163_163) = all_0_151_151 % 10.90/2.95 | (217) h1(all_0_179_179) = all_0_146_146 % 10.90/2.95 | (218) op1(e10, all_0_180_180) = all_0_180_180 % 10.90/2.95 | (219) op2(all_0_161_161, e20) = all_0_109_109 % 10.90/2.96 | (220) ~ (e13 = e10) % 10.90/2.96 | (221) op2(e20, all_0_173_173) = all_0_173_173 % 10.90/2.96 | (222) op1(e11, e12) = e13 % 10.90/2.96 | (223) op2(all_0_162_162, e20) = all_0_137_137 % 10.90/2.96 | (224) h11(e10) = all_0_172_172 % 10.90/2.96 | (225) op2(all_0_161_161, all_0_161_161) = all_0_113_113 % 10.90/2.96 | (226) h6(all_0_182_182) = all_0_81_81 % 10.90/2.96 | (227) h10(all_0_182_182) = all_0_31_31 % 10.90/2.96 | (228) op1(e13, e11) = e12 % 10.90/2.96 | (229) h2(all_0_180_180) = all_0_129_129 % 10.90/2.96 | (230) op1(e10, e13) = e13 % 10.90/2.96 | (231) op2(all_0_173_173, e20) = all_0_124_124 % 10.90/2.96 | (232) op2(e21, all_0_177_177) = all_0_104_104 % 10.90/2.96 | (233) op2(e22, all_0_162_162) = all_0_128_128 % 10.90/2.96 | (234) ~ (e20 = e13) % 10.90/2.96 | (235) h3(e10) = e20 % 10.90/2.96 | (236) h2(e10) = all_0_162_162 % 10.90/2.96 | (237) h9(all_0_183_183) = all_0_44_44 % 10.90/2.96 | (238) all_0_184_184 = e11 | all_0_185_185 = e11 % 10.90/2.96 | (239) ~ (e20 = e11) % 10.90/2.96 | (240) op2(all_0_160_160, e22) = all_0_71_71 % 10.90/2.96 | (241) h7(e12) = e20 % 10.90/2.96 | (242) op2(all_0_163_163, e21) = all_0_154_154 % 10.90/2.96 | (243) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h7(v2) = v1) | ~ (h7(v2) = v0)) % 10.90/2.96 | (244) h9(e12) = e23 % 10.90/2.96 | (245) op2(e21, e23) = e22 % 10.90/2.96 | (246) ~ (e23 = e10) % 10.90/2.96 | (247) h1(all_0_184_184) = all_0_157_157 % 10.90/2.96 | (248) h3(all_0_180_180) = all_0_116_116 % 10.90/2.96 | (249) op1(e13, e13) = e10 % 10.90/2.96 | (250) h5(all_0_182_182) = all_0_92_92 % 10.90/2.96 | (251) op2(e22, all_0_172_172) = all_0_14_14 % 10.90/2.96 | (252) h9(e10) = all_0_174_174 % 10.90/2.96 | (253) h12(all_0_180_180) = all_0_3_3 % 10.90/2.96 | (254) h10(all_0_181_181) = all_0_30_30 % 10.90/2.96 | (255) h6(all_0_179_179) = all_0_76_76 % 10.90/2.96 | (256) ~ (all_0_183_183 = all_0_184_184) % 10.90/2.96 | (257) ~ (all_0_181_181 = e12) % 10.90/2.96 | (258) h12(e10) = all_0_174_174 % 10.90/2.96 | (259) all_0_172_172 = e22 | all_0_176_176 = e22 % 10.90/2.96 | (260) all_0_184_184 = e11 | all_0_184_184 = e10 % 10.90/2.96 | (261) h9(all_0_179_179) = all_0_36_36 % 10.90/2.96 | (262) h11(e11) = e23 % 10.90/2.96 | (263) h6(all_0_181_181) = all_0_79_79 % 10.90/2.96 | (264) op2(all_0_176_176, all_0_176_176) = all_0_160_160 % 10.90/2.96 | (265) h7(all_0_180_180) = all_0_63_63 % 10.90/2.96 | (266) ~ (e22 = e21) % 10.90/2.96 | (267) h7(all_0_184_184) = all_0_72_72 % 10.90/2.96 | (268) all_0_178_178 = e22 | all_0_178_178 = e21 | all_0_178_178 = e20 % 10.90/2.96 | (269) h9(all_0_180_180) = all_0_38_38 % 10.90/2.96 | (270) ~ (all_0_184_184 = e12) % 10.90/2.96 | (271) all_0_176_176 = e22 | all_0_178_178 = e22 % 10.90/2.96 | (272) h4(all_0_182_182) = all_0_107_107 % 10.90/2.96 | (273) ~ (all_0_176_176 = all_0_177_177) % 10.90/2.96 | (274) all_0_182_182 = e11 | all_0_182_182 = e10 % 10.90/2.96 | (275) h5(e11) = e21 % 10.90/2.96 | (276) op2(e23, all_0_174_174) = all_0_37_37 % 10.90/2.96 | (277) ~ (e23 = e12) % 10.90/2.96 | (278) ~ (all_0_183_183 = e13) % 10.90/2.96 | (279) h10(all_0_179_179) = all_0_28_28 % 10.90/2.96 | (280) h4(e12) = e20 % 10.90/2.96 | (281) h6(all_0_185_185) = all_0_88_88 % 10.90/2.96 | (282) op1(e10, e10) = all_0_185_185 % 10.90/2.96 | (283) op2(all_0_175_175, e21) = e20 % 10.90/2.96 | (284) op2(e20, e20) = all_0_178_178 % 10.90/2.96 | (285) all_0_179_179 = e12 | all_0_180_180 = e12 % 10.90/2.96 | (286) op2(all_0_172_172, e23) = all_0_83_83 % 10.90/2.96 | (287) op2(all_0_172_172, e22) = all_0_82_82 % 10.90/2.96 | (288) h1(all_0_180_180) = all_0_148_148 % 10.90/2.96 | (289) all_0_180_180 = e12 | all_0_185_185 = e12 % 10.90/2.96 | (290) ~ (e20 = e12) % 10.90/2.96 | (291) ~ (e23 = e20) % 10.90/2.96 | (292) ~ (all_0_177_177 = e22) % 10.90/2.96 | (293) ~ (all_0_176_176 = all_0_178_178) % 10.90/2.96 | (294) op2(all_0_162_162, all_0_173_173) = all_0_134_134 % 10.90/2.96 | (295) all_0_181_181 = e11 | all_0_181_181 = e10 % 10.90/2.96 | (296) h11(all_0_182_182) = all_0_20_20 % 10.90/2.96 | (297) h12(all_0_182_182) = all_0_6_6 % 10.90/2.96 | (298) h9(all_0_184_184) = all_0_46_46 % 10.90/2.96 | (299) all_0_176_176 = e22 | all_0_176_176 = e20 % 10.90/2.96 | (300) h1(e10) = all_0_163_163 % 10.90/2.96 | (301) op2(all_0_174_174, e22) = all_0_45_45 % 10.90/2.96 | (302) h2(all_0_181_181) = all_0_131_131 % 10.90/2.96 | (303) ~ (all_0_0_0 = e21) | ~ (all_0_1_1 = all_0_172_172) | ~ (all_0_2_2 = all_0_3_3) | ~ (all_0_4_4 = e20) | ~ (all_0_5_5 = all_0_6_6) | ~ (all_0_7_7 = e21) | ~ (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_174_174 = e20) % 10.90/2.96 | (304) all_0_180_180 = e10 | all_0_182_182 = e10 | all_0_185_185 = e10 % 10.90/2.96 | (305) op2(e23, all_0_174_174) = all_0_5_5 % 10.90/2.96 | (306) ~ (e23 = e21) % 10.90/2.96 | (307) op2(all_0_177_177, all_0_177_177) = all_0_96_96 % 10.90/2.96 | (308) h10(e13) = e23 % 10.90/2.96 | (309) h11(e12) = e21 % 10.90/2.96 | (310) h5(all_0_180_180) = all_0_90_90 % 10.90/2.96 | (311) h4(e13) = all_0_177_177 % 10.90/2.96 | (312) op1(e11, e11) = all_0_181_181 % 10.90/2.96 | (313) h1(e13) = all_0_175_175 % 10.90/2.96 | (314) ~ (e22 = e13) % 10.90/2.96 | (315) h4(all_0_179_179) = all_0_101_101 % 10.90/2.96 | (316) ~ (e22 = e12) % 10.90/2.96 | (317) op2(e22, all_0_174_174) = all_0_40_40 % 10.90/2.96 | (318) h1(e11) = e20 % 10.90/2.96 | (319) h8(e12) = e21 % 10.90/2.96 | (320) ~ (all_0_172_172 = all_0_173_173) % 10.90/2.96 | (321) all_0_177_177 = e21 | all_0_177_177 = e20 % 10.90/2.96 | (322) ~ (e13 = e12) % 10.90/2.96 | (323) op2(e22, all_0_176_176) = all_0_64_64 % 10.90/2.96 | (324) op2(all_0_173_173, all_0_173_173) = all_0_122_122 % 10.90/2.96 | (325) op2(e20, all_0_162_162) = all_0_132_132 % 10.90/2.96 | (326) h5(all_0_179_179) = all_0_89_89 % 10.90/2.96 | (327) op2(e21, e22) = e23 % 10.90/2.96 | (328) op2(all_0_172_172, e21) = all_0_22_22 % 10.90/2.96 | (329) ~ (all_0_35_35 = e21) | ~ (all_0_36_36 = e20) | ~ (all_0_37_37 = all_0_38_38) | ~ (all_0_39_39 = all_0_172_172) | ~ (all_0_40_40 = all_0_41_41) | ~ (all_0_42_42 = e21) | ~ (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_174_174 = e20) % 10.90/2.96 | (330) ~ (e11 = e10) % 10.90/2.97 | (331) ~ (all_0_172_172 = e23) % 10.90/2.97 | (332) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h9(v2) = v1) | ~ (h9(v2) = v0)) % 10.90/2.97 | (333) op1(e10, all_0_185_185) = all_0_185_185 % 10.90/2.97 | (334) h2(all_0_182_182) = all_0_133_133 % 10.90/2.97 | (335) all_0_179_179 = e12 | all_0_179_179 = e10 % 10.90/2.97 | (336) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h12(v2) = v1) | ~ (h12(v2) = v0)) % 10.90/2.97 | (337) ~ (all_0_175_175 = all_0_178_178) % 10.90/2.97 | (338) ~ (e23 = e11) % 10.90/2.97 | (339) op1(all_0_183_183, e10) = e12 % 10.90/2.97 | (340) all_0_172_172 = e22 | all_0_173_173 = e22 % 10.90/2.97 | (341) ~ (all_0_172_172 = all_0_176_176) % 10.90/2.97 | (342) op1(e11, all_0_184_184) = all_0_171_171 % 10.90/2.97 | (343) ~ (all_0_176_176 = e21) % 10.90/2.97 | (344) all_0_181_181 = e10 | all_0_182_182 = e10 % 10.90/2.97 | (345) ~ (e12 = e11) % 10.90/2.97 | (346) op2(all_0_172_172, all_0_172_172) = all_0_87_87 % 10.90/2.97 | (347) h5(all_0_184_184) = all_0_94_94 % 10.90/2.97 | (348) op2(e21, all_0_174_174) = all_0_166_166 % 10.90/2.97 | (349) ~ (all_0_49_49 = all_0_174_174) | ~ (all_0_50_50 = all_0_175_175) | ~ (all_0_51_51 = all_0_172_172) | ~ (all_0_52_52 = all_0_173_173) | ~ (all_0_53_53 = all_0_177_177) | ~ (all_0_54_54 = all_0_176_176) | ~ (all_0_55_55 = all_0_178_178) % 10.90/2.97 | (350) h7(all_0_185_185) = all_0_74_74 % 10.90/2.97 | (351) op1(e12, e10) = all_0_180_180 % 10.90/2.97 | (352) ~ (e21 = e12) % 10.90/2.97 | (353) op2(all_0_173_173, all_0_173_173) = all_0_162_162 % 10.90/2.97 | (354) h7(e10) = all_0_160_160 % 10.90/2.97 | (355) op2(e20, e23) = e23 % 10.90/2.97 | (356) ~ (all_0_175_175 = e22) % 10.90/2.97 | (357) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h6(v2) = v1) | ~ (h6(v2) = v0)) % 10.90/2.97 | (358) h8(e11) = e22 % 10.90/2.97 | (359) ~ (e21 = e20) % 10.90/2.97 | (360) op2(all_0_176_176, e22) = all_0_58_58 % 10.90/2.97 | (361) h4(all_0_185_185) = all_0_114_114 % 10.90/2.97 | (362) all_0_182_182 = e11 | all_0_185_185 = e11 % 10.90/2.97 | (363) op1(all_0_182_182, e11) = e10 % 10.90/2.97 | (364) op2(e20, all_0_160_160) = all_0_62_62 % 10.90/2.97 | (365) op2(e23, all_0_172_172) = all_0_19_19 % 10.90/2.97 | (366) op1(e12, e12) = all_0_179_179 % 10.90/2.97 | (367) h3(all_0_185_185) = all_0_121_121 % 10.90/2.97 | (368) ~ (e21 = e13) % 10.90/2.97 | (369) op1(e11, e10) = all_0_182_182 % 10.90/2.97 | (370) h8(all_0_180_180) = all_0_50_50 % 10.90/2.97 | (371) op1(all_0_180_180, e12) = e10 % 10.90/2.97 | (372) h7(all_0_179_179) = all_0_61_61 % 10.90/2.97 | (373) ~ (all_0_184_184 = all_0_185_185) % 10.90/2.97 | (374) h4(all_0_180_180) = all_0_103_103 % 10.90/2.97 | (375) op2(e21, all_0_175_175) = all_0_145_145 % 10.90/2.97 | (376) ~ (all_0_175_175 = e23) % 10.90/2.97 | (377) h12(e13) = e21 % 10.90/2.97 | (378) all_0_176_176 = e20 | all_0_177_177 = e20 | all_0_178_178 = e20 % 10.90/2.97 | (379) op2(e22, e23) = e21 % 10.90/2.97 | (380) all_0_172_172 = e22 | all_0_172_172 = e20 % 10.90/2.97 | (381) ~ (e13 = e11) % 10.90/2.97 | (382) op2(all_0_176_176, all_0_176_176) = all_0_56_56 % 10.90/2.97 | (383) h2(all_0_179_179) = all_0_127_127 % 10.90/2.97 | (384) h2(e11) = e20 % 10.90/2.97 | (385) op1(e10, all_0_182_182) = all_0_182_182 % 10.90/2.97 | (386) op2(all_0_172_172, e23) = all_0_24_24 % 10.90/2.97 | (387) all_0_173_173 = e20 | all_0_175_175 = e20 | all_0_178_178 = e20 % 10.90/2.97 | (388) ~ (all_0_89_89 = all_0_172_172) | ~ (all_0_90_90 = all_0_173_173) | ~ (all_0_91_91 = all_0_174_174) | ~ (all_0_92_92 = all_0_175_175) | ~ (all_0_93_93 = all_0_176_176) | ~ (all_0_94_94 = all_0_177_177) | ~ (all_0_95_95 = all_0_178_178) % 10.90/2.97 | (389) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op2(v3, v2) = v1) | ~ (op2(v3, v2) = v0)) % 10.90/2.97 | (390) op2(e20, e21) = all_0_177_177 % 10.90/2.97 | (391) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h2(v2) = v1) | ~ (h2(v2) = v0)) % 10.90/2.97 | (392) ~ (all_0_182_182 = e13) % 10.90/2.97 | (393) h10(e12) = e20 % 10.90/2.97 | (394) op2(e22, all_0_172_172) = all_0_75_75 % 10.90/2.97 | (395) op2(e20, all_0_175_175) = all_0_149_149 % 10.90/2.97 | (396) h8(e13) = e23 % 10.90/2.97 | (397) h12(all_0_183_183) = all_0_9_9 % 10.90/2.97 | (398) ~ (all_0_178_178 = e23) % 10.90/2.97 | (399) op2(all_0_172_172, e22) = all_0_21_21 % 10.90/2.97 | (400) h12(all_0_185_185) = all_0_13_13 % 10.90/2.97 | (401) h12(all_0_179_179) = all_0_1_1 % 10.90/2.97 | (402) op1(e13, e12) = e11 % 10.90/2.97 | (403) ~ (all_0_179_179 = e11) % 10.90/2.97 | (404) ~ (e22 = e10) % 10.90/2.97 | (405) op2(all_0_176_176, e20) = e22 % 10.90/2.97 | (406) op2(e20, all_0_161_161) = all_0_102_102 % 10.90/2.97 | (407) op2(all_0_162_162, all_0_162_162) = all_0_139_139 % 10.90/2.97 | (408) op2(e21, all_0_177_177) = all_0_167_167 % 10.90/2.97 | (409) h3(all_0_183_183) = all_0_119_119 % 10.90/2.97 | % 10.90/2.97 | Instantiating formula (389) with all_0_172_172, all_0_172_172, all_0_87_87, all_0_26_26 and discharging atoms op2(all_0_172_172, all_0_172_172) = all_0_26_26, op2(all_0_172_172, all_0_172_172) = all_0_87_87, yields: % 10.90/2.97 | (410) all_0_26_26 = all_0_87_87 % 10.90/2.97 | % 10.90/2.97 | Instantiating formula (389) with all_0_173_173, all_0_173_173, all_0_162_162, all_0_122_122 and discharging atoms op2(all_0_173_173, all_0_173_173) = all_0_122_122, op2(all_0_173_173, all_0_173_173) = all_0_162_162, yields: % 10.90/2.97 | (411) all_0_122_122 = all_0_162_162 % 10.90/2.97 | % 10.90/2.97 | Instantiating formula (389) with all_0_174_174, all_0_174_174, all_0_47_47, all_0_12_12 and discharging atoms op2(all_0_174_174, all_0_174_174) = all_0_12_12, op2(all_0_174_174, all_0_174_174) = all_0_47_47, yields: % 10.90/2.97 | (412) all_0_12_12 = all_0_47_47 % 10.90/2.97 | % 10.90/2.97 | Instantiating formula (389) with all_0_175_175, all_0_175_175, all_0_163_163, all_0_141_141 and discharging atoms op2(all_0_175_175, all_0_175_175) = all_0_141_141, op2(all_0_175_175, all_0_175_175) = all_0_163_163, yields: % 10.90/2.97 | (413) all_0_141_141 = all_0_163_163 % 10.90/2.97 | % 10.90/2.97 | Instantiating formula (389) with all_0_176_176, all_0_176_176, all_0_160_160, all_0_56_56 and discharging atoms op2(all_0_176_176, all_0_176_176) = all_0_56_56, op2(all_0_176_176, all_0_176_176) = all_0_160_160, yields: % 10.90/2.97 | (414) all_0_56_56 = all_0_160_160 % 10.90/2.97 | % 10.90/2.97 | Instantiating formula (389) with all_0_177_177, all_0_177_177, all_0_161_161, all_0_96_96 and discharging atoms op2(all_0_177_177, all_0_177_177) = all_0_96_96, op2(all_0_177_177, all_0_177_177) = all_0_161_161, yields: % 10.90/2.97 | (415) all_0_96_96 = all_0_161_161 % 10.90/2.98 | % 10.90/2.98 | Instantiating formula (389) with e20, all_0_173_173, all_0_173_173, all_0_130_130 and discharging atoms op2(e20, all_0_173_173) = all_0_130_130, op2(e20, all_0_173_173) = all_0_173_173, yields: % 10.90/2.98 | (416) all_0_130_130 = all_0_173_173 % 10.90/2.98 | % 10.90/2.98 | Instantiating formula (389) with e20, all_0_175_175, all_0_175_175, all_0_149_149 and discharging atoms op2(e20, all_0_175_175) = all_0_149_149, op2(e20, all_0_175_175) = all_0_175_175, yields: % 10.90/2.98 | (417) all_0_149_149 = all_0_175_175 % 10.90/2.98 | % 10.90/2.98 | From (410) and (203) follows: % 10.90/2.98 | (346) op2(all_0_172_172, all_0_172_172) = all_0_87_87 % 10.90/2.98 | % 10.90/2.98 | From (411) and (324) follows: % 10.90/2.98 | (353) op2(all_0_173_173, all_0_173_173) = all_0_162_162 % 10.90/2.98 | % 10.90/2.98 | From (412) and (57) follows: % 10.90/2.98 | (171) op2(all_0_174_174, all_0_174_174) = all_0_47_47 % 10.90/2.98 | % 10.90/2.98 | From (413) and (105) follows: % 10.90/2.98 | (77) op2(all_0_175_175, all_0_175_175) = all_0_163_163 % 10.90/2.98 | % 10.90/2.98 | From (414) and (382) follows: % 10.90/2.98 | (264) op2(all_0_176_176, all_0_176_176) = all_0_160_160 % 10.90/2.98 | % 10.90/2.98 | From (415) and (307) follows: % 10.90/2.98 | (150) op2(all_0_177_177, all_0_177_177) = all_0_161_161 % 10.90/2.98 | % 10.90/2.98 | From (416) and (167) follows: % 10.90/2.98 | (221) op2(e20, all_0_173_173) = all_0_173_173 % 10.90/2.98 | % 10.90/2.98 | From (417) and (395) follows: % 10.90/2.98 | (32) op2(e20, all_0_175_175) = all_0_175_175 % 10.90/2.98 | % 10.90/2.98 +-Applying beta-rule and splitting (128), into two cases. % 10.90/2.98 |-Branch one: % 10.90/2.98 | (426) all_0_174_174 = e20 % 10.90/2.98 | % 10.90/2.98 | Equations (426) can reduce 170 to: % 10.90/2.98 | (427) ~ (all_0_175_175 = e20) % 10.90/2.98 | % 10.90/2.98 | Simplifying 427 yields: % 10.90/2.98 | (428) ~ (all_0_175_175 = e20) % 10.90/2.98 | % 10.90/2.98 | Equations (426) can reduce 127 to: % 10.90/2.98 | (429) ~ (all_0_177_177 = e20) % 10.90/2.98 | % 10.90/2.98 | Simplifying 429 yields: % 10.90/2.98 | (430) ~ (all_0_177_177 = e20) % 10.90/2.98 | % 10.90/2.98 | From (426)(426) and (171) follows: % 10.90/2.98 | (431) op2(e20, e20) = all_0_47_47 % 10.90/2.98 | % 10.90/2.98 +-Applying beta-rule and splitting (321), into two cases. % 10.90/2.98 |-Branch one: % 10.90/2.98 | (432) all_0_177_177 = e20 % 10.90/2.98 | % 10.90/2.98 | Equations (432) can reduce 430 to: % 10.90/2.98 | (433) $false % 10.90/2.98 | % 10.90/2.98 |-The branch is then unsatisfiable % 10.90/2.98 |-Branch two: % 10.90/2.98 | (430) ~ (all_0_177_177 = e20) % 10.90/2.98 | (435) all_0_177_177 = e21 % 10.90/2.98 | % 10.90/2.98 +-Applying beta-rule and splitting (201), into two cases. % 10.90/2.98 |-Branch one: % 10.90/2.98 | (436) all_0_175_175 = e20 % 10.90/2.98 | % 10.90/2.98 | Equations (436) can reduce 428 to: % 10.90/2.98 | (433) $false % 10.90/2.98 | % 10.90/2.98 |-The branch is then unsatisfiable % 10.90/2.98 |-Branch two: % 10.90/2.98 | (428) ~ (all_0_175_175 = e20) % 10.90/2.98 | (439) all_0_175_175 = e21 % 10.90/2.98 | % 10.90/2.98 | Equations (439) can reduce 337 to: % 10.90/2.98 | (440) ~ (all_0_178_178 = e21) % 10.90/2.98 | % 10.90/2.98 | Simplifying 440 yields: % 10.90/2.98 | (441) ~ (all_0_178_178 = e21) % 10.90/2.98 | % 10.90/2.98 | Instantiating formula (389) with e20, e20, all_0_47_47, all_0_178_178 and discharging atoms op2(e20, e20) = all_0_47_47, op2(e20, e20) = all_0_178_178, yields: % 10.90/2.98 | (442) all_0_47_47 = all_0_178_178 % 10.90/2.98 | % 10.90/2.98 | From (442) and (431) follows: % 10.90/2.98 | (284) op2(e20, e20) = all_0_178_178 % 10.90/2.98 | % 10.90/2.98 +-Applying beta-rule and splitting (299), into two cases. % 10.90/2.98 |-Branch one: % 10.90/2.98 | (444) all_0_176_176 = e20 % 10.90/2.98 | % 10.90/2.98 | Equations (444) can reduce 341 to: % 10.90/2.98 | (445) ~ (all_0_172_172 = e20) % 10.90/2.98 | % 10.90/2.98 | From (444)(444) and (264) follows: % 10.90/2.98 | (446) op2(e20, e20) = all_0_160_160 % 10.90/2.98 | % 10.90/2.98 +-Applying beta-rule and splitting (380), into two cases. % 10.90/2.98 |-Branch one: % 10.90/2.98 | (447) all_0_172_172 = e20 % 10.90/2.98 | % 10.90/2.98 | Equations (447) can reduce 445 to: % 10.90/2.98 | (433) $false % 10.90/2.98 | % 10.90/2.98 |-The branch is then unsatisfiable % 10.90/2.98 |-Branch two: % 10.90/2.98 | (445) ~ (all_0_172_172 = e20) % 10.90/2.98 | (450) all_0_172_172 = e22 % 10.90/2.98 | % 10.90/2.98 | Equations (450) can reduce 320 to: % 10.90/2.98 | (451) ~ (all_0_173_173 = e22) % 10.90/2.98 | % 10.90/2.98 | Simplifying 451 yields: % 10.90/2.98 | (452) ~ (all_0_173_173 = e22) % 10.90/2.98 | % 10.90/2.98 | Equations (450) can reduce 445 to: % 10.90/2.98 | (131) ~ (e22 = e20) % 10.90/2.98 | % 10.90/2.98 +-Applying beta-rule and splitting (85), into two cases. % 10.90/2.98 |-Branch one: % 10.90/2.98 | (447) all_0_172_172 = e20 % 10.90/2.98 | % 10.90/2.98 | Combining equations (447,450) yields a new equation: % 10.90/2.98 | (455) e22 = e20 % 10.90/2.98 | % 10.90/2.98 | Equations (455) can reduce 131 to: % 10.90/2.98 | (433) $false % 10.90/2.98 | % 10.90/2.98 |-The branch is then unsatisfiable % 10.90/2.98 |-Branch two: % 10.90/2.98 | (445) ~ (all_0_172_172 = e20) % 10.90/2.98 | (458) all_0_173_173 = e20 % 10.90/2.98 | % 10.90/2.98 | Equations (458) can reduce 155 to: % 10.90/2.98 | (459) ~ (all_0_178_178 = e20) % 10.90/2.98 | % 10.90/2.98 | Simplifying 459 yields: % 10.90/2.98 | (460) ~ (all_0_178_178 = e20) % 10.90/2.98 | % 10.90/2.98 | Equations (458) can reduce 452 to: % 10.90/2.98 | (461) ~ (e22 = e20) % 10.90/2.98 | % 10.90/2.98 | Simplifying 461 yields: % 10.90/2.98 | (131) ~ (e22 = e20) % 10.90/2.98 | % 10.90/2.98 | From (458)(458) and (353) follows: % 10.90/2.98 | (463) op2(e20, e20) = all_0_162_162 % 10.90/2.98 | % 10.90/2.98 | From (458)(458) and (221) follows: % 10.90/2.98 | (464) op2(e20, e20) = e20 % 10.90/2.98 | % 10.90/2.98 +-Applying beta-rule and splitting (71), into two cases. % 10.90/2.98 |-Branch one: % 10.90/2.98 | (465) all_0_173_173 = e22 % 10.90/2.98 | % 10.90/2.98 | Combining equations (458,465) yields a new equation: % 10.90/2.98 | (455) e22 = e20 % 10.90/2.98 | % 10.90/2.98 | Equations (455) can reduce 131 to: % 10.90/2.98 | (433) $false % 10.90/2.98 | % 10.90/2.98 |-The branch is then unsatisfiable % 10.90/2.98 |-Branch two: % 10.90/2.98 | (452) ~ (all_0_173_173 = e22) % 10.90/2.98 | (469) all_0_178_178 = e22 % 10.90/2.98 | % 10.90/2.98 | Equations (469) can reduce 460 to: % 10.90/2.98 | (131) ~ (e22 = e20) % 10.90/2.98 | % 10.90/2.98 | From (469) and (284) follows: % 10.90/2.98 | (471) op2(e20, e20) = e22 % 10.90/2.98 | % 10.90/2.98 | Instantiating formula (389) with e20, e20, all_0_162_162, all_0_160_160 and discharging atoms op2(e20, e20) = all_0_160_160, op2(e20, e20) = all_0_162_162, yields: % 10.90/2.98 | (472) all_0_160_160 = all_0_162_162 % 10.90/2.98 | % 10.90/2.98 | Instantiating formula (389) with e20, e20, e22, all_0_162_162 and discharging atoms op2(e20, e20) = all_0_162_162, op2(e20, e20) = e22, yields: % 10.90/2.98 | (473) all_0_162_162 = e22 % 10.90/2.98 | % 10.90/2.98 | Instantiating formula (389) with e20, e20, e20, all_0_160_160 and discharging atoms op2(e20, e20) = all_0_160_160, op2(e20, e20) = e20, yields: % 10.90/2.99 | (474) all_0_160_160 = e20 % 10.90/2.99 | % 10.90/2.99 | Combining equations (472,474) yields a new equation: % 10.90/2.99 | (475) all_0_162_162 = e20 % 10.90/2.99 | % 10.90/2.99 | Simplifying 475 yields: % 10.90/2.99 | (476) all_0_162_162 = e20 % 10.90/2.99 | % 10.90/2.99 | Combining equations (476,473) yields a new equation: % 10.90/2.99 | (455) e22 = e20 % 10.90/2.99 | % 10.90/2.99 | Equations (455) can reduce 131 to: % 10.90/2.99 | (433) $false % 10.90/2.99 | % 10.90/2.99 |-The branch is then unsatisfiable % 10.90/2.99 |-Branch two: % 10.90/2.99 | (479) ~ (all_0_176_176 = e20) % 10.90/2.99 | (480) all_0_176_176 = e22 % 10.90/2.99 | % 10.90/2.99 | Equations (480) can reduce 341 to: % 10.90/2.99 | (481) ~ (all_0_172_172 = e22) % 10.90/2.99 | % 10.90/2.99 +-Applying beta-rule and splitting (380), into two cases. % 10.90/2.99 |-Branch one: % 10.90/2.99 | (447) all_0_172_172 = e20 % 10.90/2.99 | % 10.90/2.99 | Equations (447) can reduce 320 to: % 10.90/2.99 | (483) ~ (all_0_173_173 = e20) % 10.90/2.99 | % 10.90/2.99 | Simplifying 483 yields: % 10.90/2.99 | (484) ~ (all_0_173_173 = e20) % 10.90/2.99 | % 10.90/2.99 +-Applying beta-rule and splitting (182), into two cases. % 10.90/2.99 |-Branch one: % 10.90/2.99 | (458) all_0_173_173 = e20 % 10.90/2.99 | % 10.90/2.99 | Equations (458) can reduce 484 to: % 10.90/2.99 | (433) $false % 10.90/2.99 | % 10.90/2.99 |-The branch is then unsatisfiable % 10.90/2.99 |-Branch two: % 10.90/2.99 | (484) ~ (all_0_173_173 = e20) % 10.90/2.99 | (465) all_0_173_173 = e22 % 10.90/2.99 | % 10.90/2.99 | Equations (465) can reduce 155 to: % 10.90/2.99 | (489) ~ (all_0_178_178 = e22) % 10.90/2.99 | % 10.90/2.99 | Simplifying 489 yields: % 10.90/2.99 | (490) ~ (all_0_178_178 = e22) % 10.90/2.99 | % 10.90/2.99 +-Applying beta-rule and splitting (268), into two cases. % 10.90/2.99 |-Branch one: % 10.90/2.99 | (491) all_0_178_178 = e20 % 10.90/2.99 | % 10.90/2.99 +-Applying beta-rule and splitting (335), into two cases. % 10.90/2.99 |-Branch one: % 10.90/2.99 | (492) all_0_179_179 = e10 % 10.90/2.99 | % 10.90/2.99 | Equations (492) can reduce 211 to: % 10.90/2.99 | (493) ~ (all_0_180_180 = e10) % 10.90/2.99 | % 10.90/2.99 | Simplifying 493 yields: % 10.90/2.99 | (494) ~ (all_0_180_180 = e10) % 10.90/2.99 | % 10.90/2.99 | Equations (492) can reduce 178 to: % 10.90/2.99 | (495) ~ (all_0_183_183 = e10) % 10.90/2.99 | % 10.90/2.99 | Simplifying 495 yields: % 10.90/2.99 | (496) ~ (all_0_183_183 = e10) % 10.90/2.99 | % 10.90/2.99 | From (492) and (326) follows: % 10.90/2.99 | (497) h5(e10) = all_0_89_89 % 10.90/2.99 | % 10.90/2.99 | From (492) and (25) follows: % 10.90/2.99 | (498) h8(e10) = all_0_49_49 % 10.90/2.99 | % 10.90/2.99 +-Applying beta-rule and splitting (168), into two cases. % 10.90/2.99 |-Branch one: % 10.90/2.99 | (499) all_0_183_183 = e10 % 10.90/2.99 | % 10.90/2.99 | Equations (499) can reduce 496 to: % 10.90/2.99 | (433) $false % 10.90/2.99 | % 10.90/2.99 |-The branch is then unsatisfiable % 10.90/2.99 |-Branch two: % 10.90/2.99 | (496) ~ (all_0_183_183 = e10) % 10.90/2.99 | (502) all_0_183_183 = e12 % 10.90/2.99 | % 10.90/2.99 | From (502) and (94) follows: % 10.90/2.99 | (503) h8(e12) = all_0_53_53 % 10.90/2.99 | % 10.90/2.99 +-Applying beta-rule and splitting (147), into two cases. % 10.90/2.99 |-Branch one: % 10.90/2.99 | (504) all_0_180_180 = e10 % 10.90/2.99 | % 10.90/2.99 | Equations (504) can reduce 494 to: % 10.90/2.99 | (433) $false % 10.90/2.99 | % 10.90/2.99 |-The branch is then unsatisfiable % 10.90/2.99 |-Branch two: % 10.90/2.99 | (494) ~ (all_0_180_180 = e10) % 10.90/2.99 | (507) all_0_180_180 = e12 % 10.90/2.99 | % 10.90/2.99 | Equations (507) can reduce 106 to: % 10.90/2.99 | (508) ~ (all_0_185_185 = e12) % 10.90/2.99 | % 10.90/2.99 | Simplifying 508 yields: % 10.90/2.99 | (509) ~ (all_0_185_185 = e12) % 10.90/2.99 | % 10.90/2.99 | From (507) and (370) follows: % 10.90/2.99 | (510) h8(e12) = all_0_50_50 % 10.90/2.99 | % 10.90/2.99 | Instantiating formula (76) with e10, all_0_89_89, e20 and discharging atoms h5(e10) = all_0_89_89, h5(e10) = e20, yields: % 10.90/2.99 | (511) all_0_89_89 = e20 % 10.90/2.99 | % 10.90/2.99 | Instantiating formula (38) with e12, all_0_50_50, e21 and discharging atoms h8(e12) = all_0_50_50, h8(e12) = e21, yields: % 10.90/2.99 | (512) all_0_50_50 = e21 % 10.90/2.99 | % 10.90/2.99 | Instantiating formula (38) with e12, all_0_53_53, all_0_50_50 and discharging atoms h8(e12) = all_0_50_50, h8(e12) = all_0_53_53, yields: % 10.90/2.99 | (513) all_0_50_50 = all_0_53_53 % 10.90/2.99 | % 10.90/2.99 | Instantiating formula (38) with e10, all_0_49_49, e20 and discharging atoms h8(e10) = all_0_49_49, h8(e10) = e20, yields: % 10.90/2.99 | (514) all_0_49_49 = e20 % 10.90/2.99 | % 10.90/2.99 | Combining equations (513,512) yields a new equation: % 10.90/2.99 | (515) all_0_53_53 = e21 % 10.90/2.99 | % 10.90/2.99 | Simplifying 515 yields: % 10.90/2.99 | (516) all_0_53_53 = e21 % 10.90/2.99 | % 10.90/2.99 | From (514) and (498) follows: % 10.90/2.99 | (103) h8(e10) = e20 % 10.90/2.99 | % 10.90/2.99 +-Applying beta-rule and splitting (260), into two cases. % 10.90/2.99 |-Branch one: % 10.90/2.99 | (518) all_0_184_184 = e10 % 10.90/2.99 | % 10.90/2.99 | Equations (518) can reduce 137 to: % 10.90/2.99 | (519) ~ (all_0_181_181 = e10) % 10.90/2.99 | % 10.90/2.99 +-Applying beta-rule and splitting (344), into two cases. % 10.90/2.99 |-Branch one: % 10.90/2.99 | (520) all_0_181_181 = e10 % 10.90/2.99 | % 10.90/2.99 | Equations (520) can reduce 519 to: % 10.90/2.99 | (433) $false % 10.90/2.99 | % 10.90/2.99 |-The branch is then unsatisfiable % 10.90/2.99 |-Branch two: % 10.90/2.99 | (519) ~ (all_0_181_181 = e10) % 10.90/2.99 | (523) all_0_182_182 = e10 % 10.90/2.99 | % 10.90/2.99 | Equations (523) can reduce 84 to: % 10.90/2.99 | (524) ~ (all_0_185_185 = e10) % 11.25/2.99 | % 11.25/2.99 | Simplifying 524 yields: % 11.25/2.99 | (525) ~ (all_0_185_185 = e10) % 11.25/2.99 | % 11.25/2.99 | From (523)(523) and (385) follows: % 11.25/2.99 | (526) op1(e10, e10) = e10 % 11.25/2.99 | % 11.25/2.99 +-Applying beta-rule and splitting (133), into two cases. % 11.25/2.99 |-Branch one: % 11.25/2.99 | (527) all_0_185_185 = e10 % 11.25/2.99 | % 11.25/2.99 | Equations (527) can reduce 525 to: % 11.25/2.99 | (433) $false % 11.25/2.99 | % 11.25/2.99 |-The branch is then unsatisfiable % 11.25/2.99 |-Branch two: % 11.25/2.99 | (525) ~ (all_0_185_185 = e10) % 11.25/2.99 | (530) all_0_185_185 = e12 | all_0_185_185 = e11 % 11.25/2.99 | % 11.25/2.99 +-Applying beta-rule and splitting (530), into two cases. % 11.25/2.99 |-Branch one: % 11.25/2.99 | (531) all_0_185_185 = e12 % 11.25/2.99 | % 11.25/2.99 | Equations (531) can reduce 509 to: % 11.25/2.99 | (433) $false % 11.25/2.99 | % 11.25/2.99 |-The branch is then unsatisfiable % 11.25/2.99 |-Branch two: % 11.25/2.99 | (509) ~ (all_0_185_185 = e12) % 11.25/2.99 | (534) all_0_185_185 = e11 % 11.25/2.99 | % 11.25/2.99 | Equations (534) can reduce 525 to: % 11.25/2.99 | (330) ~ (e11 = e10) % 11.25/2.99 | % 11.25/2.99 | From (534) and (282) follows: % 11.25/2.99 | (536) op1(e10, e10) = e11 % 11.25/2.99 | % 11.25/2.99 | Instantiating formula (194) with e10, e10, e10, e11 and discharging atoms op1(e10, e10) = e11, op1(e10, e10) = e10, yields: % 11.25/2.99 | (537) e11 = e10 % 11.25/2.99 | % 11.25/2.99 | Equations (537) can reduce 330 to: % 11.25/2.99 | (433) $false % 11.25/2.99 | % 11.25/2.99 |-The branch is then unsatisfiable % 11.25/2.99 |-Branch two: % 11.25/2.99 | (539) ~ (all_0_184_184 = e10) % 11.25/2.99 | (540) all_0_184_184 = e11 % 11.25/2.99 | % 11.25/2.99 | Equations (540) can reduce 137 to: % 11.25/2.99 | (541) ~ (all_0_181_181 = e11) % 11.25/2.99 | % 11.25/2.99 | Equations (540) can reduce 539 to: % 11.25/2.99 | (330) ~ (e11 = e10) % 11.25/2.99 | % 11.25/2.99 | From (540) and (132) follows: % 11.25/2.99 | (543) h8(e11) = all_0_54_54 % 11.25/2.99 | % 11.25/2.99 +-Applying beta-rule and splitting (70), into two cases. % 11.25/2.99 |-Branch one: % 11.25/2.99 | (544) all_0_181_181 = e11 % 11.25/2.99 | % 11.25/2.99 | Equations (544) can reduce 541 to: % 11.25/2.99 | (433) $false % 11.25/2.99 | % 11.25/2.99 |-The branch is then unsatisfiable % 11.25/2.99 |-Branch two: % 11.25/2.99 | (541) ~ (all_0_181_181 = e11) % 11.25/2.99 | (547) all_0_182_182 = e11 % 11.25/3.00 | % 11.25/3.00 | Equations (547) can reduce 41 to: % 11.25/3.00 | (541) ~ (all_0_181_181 = e11) % 11.25/3.00 | % 11.25/3.00 | From (547) and (19) follows: % 11.25/3.00 | (549) h8(e11) = all_0_52_52 % 11.25/3.00 | % 11.25/3.00 +-Applying beta-rule and splitting (149), into two cases. % 11.25/3.00 |-Branch one: % 11.25/3.00 | (520) all_0_181_181 = e10 % 11.25/3.00 | % 11.25/3.00 | Equations (520) can reduce 257 to: % 11.25/3.00 | (551) ~ (e12 = e10) % 11.25/3.00 | % 11.25/3.00 | Simplifying 551 yields: % 11.25/3.00 | (180) ~ (e12 = e10) % 11.25/3.00 | % 11.25/3.00 | Equations (520) can reduce 541 to: % 11.25/3.00 | (553) ~ (e11 = e10) % 11.25/3.00 | % 11.25/3.00 | Simplifying 553 yields: % 11.25/3.00 | (330) ~ (e11 = e10) % 11.25/3.00 | % 11.25/3.00 | From (520) and (138) follows: % 11.25/3.00 | (555) h8(e10) = all_0_51_51 % 11.25/3.00 | % 11.25/3.00 +-Applying beta-rule and splitting (163), into two cases. % 11.25/3.00 |-Branch one: % 11.25/3.00 | (499) all_0_183_183 = e10 % 11.25/3.00 | % 11.25/3.00 | Combining equations (502,499) yields a new equation: % 11.25/3.00 | (557) e12 = e10 % 11.25/3.00 | % 11.25/3.00 | Simplifying 557 yields: % 11.25/3.00 | (558) e12 = e10 % 11.25/3.00 | % 11.25/3.00 | Equations (558) can reduce 180 to: % 11.25/3.00 | (433) $false % 11.25/3.00 | % 11.25/3.00 |-The branch is then unsatisfiable % 11.25/3.00 |-Branch two: % 11.25/3.00 | (496) ~ (all_0_183_183 = e10) % 11.25/3.00 | (561) all_0_184_184 = e10 | all_0_185_185 = e10 % 11.25/3.00 | % 11.25/3.00 +-Applying beta-rule and splitting (561), into two cases. % 11.25/3.00 |-Branch one: % 11.25/3.00 | (518) all_0_184_184 = e10 % 11.25/3.00 | % 11.25/3.00 | Combining equations (540,518) yields a new equation: % 11.25/3.00 | (563) e11 = e10 % 11.25/3.00 | % 11.25/3.00 | Simplifying 563 yields: % 11.25/3.00 | (537) e11 = e10 % 11.25/3.00 | % 11.25/3.00 | Equations (537) can reduce 330 to: % 11.25/3.00 | (433) $false % 11.25/3.00 | % 11.25/3.00 |-The branch is then unsatisfiable % 11.25/3.00 |-Branch two: % 11.25/3.00 | (539) ~ (all_0_184_184 = e10) % 11.25/3.00 | (527) all_0_185_185 = e10 % 11.25/3.00 | % 11.25/3.00 | From (527) and (24) follows: % 11.25/3.00 | (568) h8(e10) = all_0_55_55 % 11.25/3.00 | % 11.25/3.00 | Instantiating formula (38) with e11, all_0_52_52, e22 and discharging atoms h8(e11) = all_0_52_52, h8(e11) = e22, yields: % 11.25/3.00 | (569) all_0_52_52 = e22 % 11.25/3.00 | % 11.25/3.00 | Instantiating formula (38) with e11, all_0_54_54, all_0_52_52 and discharging atoms h8(e11) = all_0_52_52, h8(e11) = all_0_54_54, yields: % 11.25/3.00 | (570) all_0_52_52 = all_0_54_54 % 11.25/3.00 | % 11.25/3.00 | Instantiating formula (38) with e10, all_0_51_51, e20 and discharging atoms h8(e10) = all_0_51_51, h8(e10) = e20, yields: % 11.25/3.00 | (571) all_0_51_51 = e20 % 11.25/3.00 | % 11.25/3.00 | Instantiating formula (38) with e10, all_0_55_55, all_0_51_51 and discharging atoms h8(e10) = all_0_51_51, h8(e10) = all_0_55_55, yields: % 11.25/3.00 | (572) all_0_51_51 = all_0_55_55 % 11.25/3.00 | % 11.25/3.00 | Combining equations (572,571) yields a new equation: % 11.25/3.00 | (573) all_0_55_55 = e20 % 11.25/3.00 | % 11.25/3.00 | Simplifying 573 yields: % 11.25/3.00 | (574) all_0_55_55 = e20 % 11.25/3.00 | % 11.25/3.00 | Combining equations (569,570) yields a new equation: % 11.25/3.00 | (575) all_0_54_54 = e22 % 11.25/3.00 | % 11.25/3.00 | Combining equations (575,570) yields a new equation: % 11.25/3.00 | (569) all_0_52_52 = e22 % 11.25/3.00 | % 11.25/3.00 +-Applying beta-rule and splitting (388), into two cases. % 11.25/3.00 |-Branch one: % 11.25/3.00 | (577) ~ (all_0_89_89 = all_0_172_172) % 11.25/3.00 | % 11.25/3.00 | Equations (511,447) can reduce 577 to: % 11.25/3.00 | (433) $false % 11.25/3.00 | % 11.25/3.00 |-The branch is then unsatisfiable % 11.25/3.00 |-Branch two: % 11.25/3.00 | (579) all_0_89_89 = all_0_172_172 % 11.25/3.00 | (580) ~ (all_0_90_90 = all_0_173_173) | ~ (all_0_91_91 = all_0_174_174) | ~ (all_0_92_92 = all_0_175_175) | ~ (all_0_93_93 = all_0_176_176) | ~ (all_0_94_94 = all_0_177_177) | ~ (all_0_95_95 = all_0_178_178) % 11.25/3.00 | % 11.25/3.00 | Combining equations (511,579) yields a new equation: % 11.25/3.00 | (447) all_0_172_172 = e20 % 11.25/3.00 | % 11.25/3.00 +-Applying beta-rule and splitting (349), into two cases. % 11.25/3.00 |-Branch one: % 11.25/3.00 | (582) ~ (all_0_49_49 = all_0_174_174) % 11.25/3.00 | % 11.25/3.00 | Equations (514,426) can reduce 582 to: % 11.25/3.00 | (433) $false % 11.25/3.00 | % 11.25/3.00 |-The branch is then unsatisfiable % 11.25/3.00 |-Branch two: % 11.25/3.00 | (584) all_0_49_49 = all_0_174_174 % 11.25/3.00 | (585) ~ (all_0_50_50 = all_0_175_175) | ~ (all_0_51_51 = all_0_172_172) | ~ (all_0_52_52 = all_0_173_173) | ~ (all_0_53_53 = all_0_177_177) | ~ (all_0_54_54 = all_0_176_176) | ~ (all_0_55_55 = all_0_178_178) % 11.25/3.00 | % 11.25/3.00 +-Applying beta-rule and splitting (585), into two cases. % 11.25/3.00 |-Branch one: % 11.25/3.00 | (586) ~ (all_0_50_50 = all_0_175_175) % 11.25/3.00 | % 11.25/3.00 | Equations (512,439) can reduce 586 to: % 11.25/3.00 | (433) $false % 11.25/3.00 | % 11.25/3.00 |-The branch is then unsatisfiable % 11.25/3.00 |-Branch two: % 11.25/3.00 | (588) all_0_50_50 = all_0_175_175 % 11.25/3.00 | (589) ~ (all_0_51_51 = all_0_172_172) | ~ (all_0_52_52 = all_0_173_173) | ~ (all_0_53_53 = all_0_177_177) | ~ (all_0_54_54 = all_0_176_176) | ~ (all_0_55_55 = all_0_178_178) % 11.25/3.00 | % 11.25/3.00 +-Applying beta-rule and splitting (589), into two cases. % 11.25/3.00 |-Branch one: % 11.25/3.00 | (590) ~ (all_0_51_51 = all_0_172_172) % 11.25/3.00 | % 11.25/3.00 | Equations (571,447) can reduce 590 to: % 11.25/3.00 | (433) $false % 11.25/3.00 | % 11.25/3.00 |-The branch is then unsatisfiable % 11.25/3.00 |-Branch two: % 11.25/3.00 | (592) all_0_51_51 = all_0_172_172 % 11.25/3.00 | (593) ~ (all_0_52_52 = all_0_173_173) | ~ (all_0_53_53 = all_0_177_177) | ~ (all_0_54_54 = all_0_176_176) | ~ (all_0_55_55 = all_0_178_178) % 11.25/3.00 | % 11.25/3.00 +-Applying beta-rule and splitting (593), into two cases. % 11.25/3.00 |-Branch one: % 11.25/3.00 | (594) ~ (all_0_52_52 = all_0_173_173) % 11.25/3.00 | % 11.25/3.00 | Equations (569,465) can reduce 594 to: % 11.25/3.00 | (433) $false % 11.25/3.00 | % 11.25/3.00 |-The branch is then unsatisfiable % 11.25/3.00 |-Branch two: % 11.25/3.00 | (596) all_0_52_52 = all_0_173_173 % 11.25/3.00 | (597) ~ (all_0_53_53 = all_0_177_177) | ~ (all_0_54_54 = all_0_176_176) | ~ (all_0_55_55 = all_0_178_178) % 11.25/3.00 | % 11.25/3.00 +-Applying beta-rule and splitting (597), into two cases. % 11.25/3.00 |-Branch one: % 11.25/3.00 | (598) ~ (all_0_53_53 = all_0_177_177) % 11.25/3.00 | % 11.25/3.00 | Equations (516,435) can reduce 598 to: % 11.25/3.00 | (433) $false % 11.25/3.00 | % 11.25/3.00 |-The branch is then unsatisfiable % 11.25/3.00 |-Branch two: % 11.25/3.00 | (600) all_0_53_53 = all_0_177_177 % 11.25/3.00 | (601) ~ (all_0_54_54 = all_0_176_176) | ~ (all_0_55_55 = all_0_178_178) % 11.25/3.00 | % 11.25/3.00 +-Applying beta-rule and splitting (601), into two cases. % 11.25/3.00 |-Branch one: % 11.25/3.00 | (602) ~ (all_0_54_54 = all_0_176_176) % 11.25/3.00 | % 11.25/3.00 | Equations (575,480) can reduce 602 to: % 11.25/3.00 | (433) $false % 11.25/3.00 | % 11.25/3.00 |-The branch is then unsatisfiable % 11.25/3.00 |-Branch two: % 11.25/3.00 | (604) all_0_54_54 = all_0_176_176 % 11.25/3.00 | (605) ~ (all_0_55_55 = all_0_178_178) % 11.25/3.00 | % 11.25/3.00 | Equations (574,491) can reduce 605 to: % 11.25/3.00 | (433) $false % 11.25/3.00 | % 11.25/3.00 |-The branch is then unsatisfiable % 11.25/3.00 |-Branch two: % 11.25/3.00 | (519) ~ (all_0_181_181 = e10) % 11.25/3.00 | (518) all_0_184_184 = e10 % 11.25/3.00 | % 11.25/3.00 | Combining equations (518,540) yields a new equation: % 11.25/3.00 | (537) e11 = e10 % 11.25/3.00 | % 11.25/3.00 | Equations (537) can reduce 330 to: % 11.25/3.00 | (433) $false % 11.25/3.00 | % 11.25/3.00 |-The branch is then unsatisfiable % 11.25/3.00 |-Branch two: % 11.25/3.00 | (611) ~ (all_0_179_179 = e10) % 11.25/3.00 | (612) all_0_179_179 = e12 % 11.25/3.00 | % 11.25/3.00 | Equations (612) can reduce 178 to: % 11.25/3.00 | (613) ~ (all_0_183_183 = e12) % 11.25/3.00 | % 11.25/3.00 | Simplifying 613 yields: % 11.25/3.01 | (614) ~ (all_0_183_183 = e12) % 11.25/3.01 | % 11.25/3.01 | Equations (612) can reduce 403 to: % 11.25/3.01 | (345) ~ (e12 = e11) % 11.25/3.01 | % 11.25/3.01 +-Applying beta-rule and splitting (22), into two cases. % 11.25/3.01 |-Branch one: % 11.25/3.01 | (502) all_0_183_183 = e12 % 11.25/3.01 | % 11.25/3.01 | Equations (502) can reduce 614 to: % 11.25/3.01 | (433) $false % 11.25/3.01 | % 11.25/3.01 |-The branch is then unsatisfiable % 11.25/3.01 |-Branch two: % 11.25/3.01 | (614) ~ (all_0_183_183 = e12) % 11.25/3.01 | (531) all_0_185_185 = e12 % 11.25/3.01 | % 11.25/3.01 | Equations (531) can reduce 106 to: % 11.25/3.01 | (620) ~ (all_0_180_180 = e12) % 11.25/3.01 | % 11.25/3.01 +-Applying beta-rule and splitting (362), into two cases. % 11.25/3.01 |-Branch one: % 11.25/3.01 | (547) all_0_182_182 = e11 % 11.25/3.01 | % 11.25/3.01 | Equations (547) can reduce 62 to: % 11.25/3.01 | (144) ~ (all_0_180_180 = e11) % 11.25/3.01 | % 11.25/3.01 | Equations (547) can reduce 41 to: % 11.25/3.01 | (541) ~ (all_0_181_181 = e11) % 11.25/3.01 | % 11.25/3.01 +-Applying beta-rule and splitting (147), into two cases. % 11.25/3.01 |-Branch one: % 11.25/3.01 | (504) all_0_180_180 = e10 % 11.25/3.01 | % 11.25/3.01 | Equations (504) can reduce 620 to: % 11.25/3.01 | (551) ~ (e12 = e10) % 11.25/3.01 | % 11.25/3.01 | Simplifying 551 yields: % 11.25/3.01 | (180) ~ (e12 = e10) % 11.25/3.01 | % 11.25/3.01 | Equations (504) can reduce 144 to: % 11.25/3.01 | (553) ~ (e11 = e10) % 11.25/3.01 | % 11.25/3.01 | Simplifying 553 yields: % 11.25/3.01 | (330) ~ (e11 = e10) % 11.25/3.01 | % 11.25/3.01 | From (504)(504) and (218) follows: % 11.25/3.01 | (526) op1(e10, e10) = e10 % 11.25/3.01 | % 11.25/3.01 +-Applying beta-rule and splitting (186), into two cases. % 11.25/3.01 |-Branch one: % 11.25/3.01 | (544) all_0_181_181 = e11 % 11.25/3.01 | % 11.25/3.01 | Equations (544) can reduce 541 to: % 11.25/3.01 | (433) $false % 11.25/3.01 | % 11.25/3.01 |-The branch is then unsatisfiable % 11.25/3.01 |-Branch two: % 11.25/3.01 | (541) ~ (all_0_181_181 = e11) % 11.25/3.01 | (540) all_0_184_184 = e11 % 11.25/3.01 | % 11.25/3.01 | Equations (540) can reduce 137 to: % 11.25/3.01 | (541) ~ (all_0_181_181 = e11) % 11.25/3.01 | % 11.25/3.01 +-Applying beta-rule and splitting (163), into two cases. % 11.25/3.01 |-Branch one: % 11.25/3.01 | (499) all_0_183_183 = e10 % 11.25/3.01 | % 11.25/3.01 | From (499) and (339) follows: % 11.25/3.01 | (636) op1(e10, e10) = e12 % 11.25/3.01 | % 11.25/3.01 +-Applying beta-rule and splitting (295), into two cases. % 11.25/3.01 |-Branch one: % 11.25/3.01 | (520) all_0_181_181 = e10 % 11.25/3.01 | % 11.25/3.01 | Equations (520) can reduce 257 to: % 11.25/3.01 | (551) ~ (e12 = e10) % 11.25/3.01 | % 11.25/3.01 | Simplifying 551 yields: % 11.25/3.01 | (180) ~ (e12 = e10) % 11.25/3.01 | % 11.25/3.01 | Instantiating formula (194) with e10, e10, e10, e12 and discharging atoms op1(e10, e10) = e12, op1(e10, e10) = e10, yields: % 11.25/3.01 | (558) e12 = e10 % 11.25/3.01 | % 11.25/3.01 | Equations (558) can reduce 180 to: % 11.25/3.01 | (433) $false % 11.25/3.01 | % 11.25/3.01 |-The branch is then unsatisfiable % 11.25/3.01 |-Branch two: % 11.25/3.01 | (519) ~ (all_0_181_181 = e10) % 11.25/3.01 | (544) all_0_181_181 = e11 % 11.25/3.01 | % 11.25/3.01 | Equations (544) can reduce 541 to: % 11.25/3.01 | (433) $false % 11.25/3.01 | % 11.25/3.01 |-The branch is then unsatisfiable % 11.25/3.01 |-Branch two: % 11.25/3.01 | (496) ~ (all_0_183_183 = e10) % 11.25/3.01 | (561) all_0_184_184 = e10 | all_0_185_185 = e10 % 11.25/3.01 | % 11.25/3.01 +-Applying beta-rule and splitting (561), into two cases. % 11.25/3.01 |-Branch one: % 11.25/3.01 | (518) all_0_184_184 = e10 % 11.25/3.01 | % 11.25/3.01 | Combining equations (540,518) yields a new equation: % 11.25/3.01 | (563) e11 = e10 % 11.25/3.01 | % 11.25/3.01 | Simplifying 563 yields: % 11.25/3.01 | (537) e11 = e10 % 11.25/3.01 | % 11.25/3.01 | Equations (537) can reduce 330 to: % 11.25/3.01 | (433) $false % 11.25/3.01 | % 11.25/3.01 |-The branch is then unsatisfiable % 11.25/3.01 |-Branch two: % 11.25/3.01 | (539) ~ (all_0_184_184 = e10) % 11.25/3.01 | (527) all_0_185_185 = e10 % 11.25/3.01 | % 11.25/3.01 | Combining equations (527,531) yields a new equation: % 11.25/3.01 | (558) e12 = e10 % 11.25/3.01 | % 11.25/3.01 | Equations (558) can reduce 180 to: % 11.25/3.01 | (433) $false % 11.25/3.01 | % 11.25/3.01 |-The branch is then unsatisfiable % 11.25/3.01 |-Branch two: % 11.25/3.01 | (494) ~ (all_0_180_180 = e10) % 11.25/3.01 | (507) all_0_180_180 = e12 % 11.25/3.01 | % 11.25/3.01 | Equations (507) can reduce 620 to: % 11.25/3.01 | (433) $false % 11.25/3.01 | % 11.25/3.01 |-The branch is then unsatisfiable % 11.25/3.01 |-Branch two: % 11.25/3.01 | (658) ~ (all_0_182_182 = e11) % 11.25/3.01 | (534) all_0_185_185 = e11 % 11.25/3.01 | % 11.25/3.01 | Combining equations (534,531) yields a new equation: % 11.25/3.01 | (660) e12 = e11 % 11.25/3.01 | % 11.25/3.01 | Equations (660) can reduce 345 to: % 11.25/3.01 | (433) $false % 11.25/3.01 | % 11.25/3.01 |-The branch is then unsatisfiable % 11.25/3.01 |-Branch two: % 11.25/3.01 | (460) ~ (all_0_178_178 = e20) % 11.25/3.01 | (663) all_0_178_178 = e22 | all_0_178_178 = e21 % 11.25/3.01 | % 11.25/3.01 +-Applying beta-rule and splitting (663), into two cases. % 11.25/3.01 |-Branch one: % 11.25/3.01 | (469) all_0_178_178 = e22 % 11.25/3.01 | % 11.25/3.01 | Equations (469) can reduce 490 to: % 11.25/3.01 | (433) $false % 11.25/3.01 | % 11.25/3.01 |-The branch is then unsatisfiable % 11.25/3.01 |-Branch two: % 11.25/3.01 | (490) ~ (all_0_178_178 = e22) % 11.25/3.01 | (667) all_0_178_178 = e21 % 11.25/3.01 | % 11.25/3.01 | Equations (667) can reduce 441 to: % 11.25/3.01 | (433) $false % 11.25/3.01 | % 11.25/3.01 |-The branch is then unsatisfiable % 11.25/3.01 |-Branch two: % 11.25/3.01 | (445) ~ (all_0_172_172 = e20) % 11.25/3.01 | (450) all_0_172_172 = e22 % 11.25/3.01 | % 11.25/3.01 | Equations (450) can reduce 481 to: % 11.25/3.01 | (433) $false % 11.25/3.01 | % 11.25/3.01 |-The branch is then unsatisfiable % 11.25/3.01 |-Branch two: % 11.25/3.01 | (672) ~ (all_0_174_174 = e20) % 11.25/3.01 | (432) all_0_177_177 = e20 % 11.25/3.01 | % 11.25/3.01 | Equations (432) can reduce 273 to: % 11.25/3.01 | (479) ~ (all_0_176_176 = e20) % 11.25/3.01 | % 11.25/3.01 | From (432)(432) and (150) follows: % 11.25/3.01 | (675) op2(e20, e20) = all_0_161_161 % 11.25/3.01 | % 11.25/3.01 +-Applying beta-rule and splitting (166), into two cases. % 11.25/3.01 |-Branch one: % 11.25/3.01 | (435) all_0_177_177 = e21 % 11.25/3.01 | % 11.25/3.01 | Combining equations (435,432) yields a new equation: % 11.25/3.01 | (677) e21 = e20 % 11.25/3.01 | % 11.25/3.01 | Simplifying 677 yields: % 11.25/3.01 | (678) e21 = e20 % 11.25/3.01 | % 11.25/3.01 | Equations (678) can reduce 359 to: % 11.25/3.01 | (433) $false % 11.25/3.01 | % 11.25/3.01 |-The branch is then unsatisfiable % 11.25/3.01 |-Branch two: % 11.25/3.01 | (680) ~ (all_0_177_177 = e21) % 11.25/3.01 | (667) all_0_178_178 = e21 % 11.25/3.01 | % 11.25/3.01 | Equations (667) can reduce 337 to: % 11.25/3.01 | (682) ~ (all_0_175_175 = e21) % 11.25/3.01 | % 11.25/3.01 | From (667) and (284) follows: % 11.25/3.01 | (683) op2(e20, e20) = e21 % 11.25/3.01 | % 11.25/3.01 +-Applying beta-rule and splitting (89), into two cases. % 11.25/3.01 |-Branch one: % 11.25/3.01 | (684) all_0_174_174 = e21 % 11.25/3.01 | % 11.25/3.01 | Equations (684) can reduce 170 to: % 11.25/3.01 | (685) ~ (all_0_175_175 = e21) % 11.25/3.01 | % 11.25/3.01 | Simplifying 685 yields: % 11.25/3.01 | (682) ~ (all_0_175_175 = e21) % 11.25/3.02 | % 11.25/3.02 +-Applying beta-rule and splitting (299), into two cases. % 11.25/3.02 |-Branch one: % 11.25/3.02 | (444) all_0_176_176 = e20 % 11.25/3.02 | % 11.25/3.02 | Equations (444) can reduce 479 to: % 11.25/3.02 | (433) $false % 11.25/3.02 | % 11.25/3.02 |-The branch is then unsatisfiable % 11.25/3.02 |-Branch two: % 11.25/3.02 | (479) ~ (all_0_176_176 = e20) % 11.25/3.02 | (480) all_0_176_176 = e22 % 11.25/3.02 | % 11.25/3.02 | Equations (480) can reduce 341 to: % 11.25/3.02 | (481) ~ (all_0_172_172 = e22) % 11.25/3.02 | % 11.25/3.02 +-Applying beta-rule and splitting (340), into two cases. % 11.25/3.02 |-Branch one: % 11.25/3.02 | (450) all_0_172_172 = e22 % 11.25/3.02 | % 11.25/3.02 | Equations (450) can reduce 481 to: % 11.25/3.02 | (433) $false % 11.25/3.02 | % 11.25/3.02 |-The branch is then unsatisfiable % 11.25/3.02 |-Branch two: % 11.25/3.02 | (481) ~ (all_0_172_172 = e22) % 11.25/3.02 | (465) all_0_173_173 = e22 % 11.25/3.02 | % 11.25/3.02 | Equations (465) can reduce 320 to: % 11.25/3.02 | (481) ~ (all_0_172_172 = e22) % 11.25/3.02 | % 11.25/3.02 +-Applying beta-rule and splitting (201), into two cases. % 11.25/3.02 |-Branch one: % 11.25/3.02 | (436) all_0_175_175 = e20 % 11.25/3.02 | % 11.25/3.02 | From (436)(436) and (77) follows: % 11.25/3.02 | (698) op2(e20, e20) = all_0_163_163 % 11.25/3.02 | % 11.25/3.02 | From (436)(436) and (32) follows: % 11.25/3.02 | (464) op2(e20, e20) = e20 % 11.25/3.02 | % 11.25/3.02 +-Applying beta-rule and splitting (380), into two cases. % 11.25/3.02 |-Branch one: % 11.25/3.02 | (447) all_0_172_172 = e20 % 11.25/3.02 | % 11.25/3.02 | Equations (447) can reduce 161 to: % 11.25/3.02 | (701) ~ (e21 = e20) % 11.25/3.02 | % 11.25/3.02 | Simplifying 701 yields: % 11.25/3.02 | (359) ~ (e21 = e20) % 11.25/3.02 | % 11.25/3.02 | From (447)(447) and (346) follows: % 11.25/3.02 | (703) op2(e20, e20) = all_0_87_87 % 11.25/3.02 | % 11.25/3.02 | Instantiating formula (389) with e20, e20, all_0_161_161, all_0_87_87 and discharging atoms op2(e20, e20) = all_0_87_87, op2(e20, e20) = all_0_161_161, yields: % 11.25/3.02 | (704) all_0_87_87 = all_0_161_161 % 11.25/3.02 | % 11.25/3.02 | Instantiating formula (389) with e20, e20, all_0_163_163, all_0_161_161 and discharging atoms op2(e20, e20) = all_0_161_161, op2(e20, e20) = all_0_163_163, yields: % 11.25/3.02 | (705) all_0_161_161 = all_0_163_163 % 11.25/3.02 | % 11.25/3.02 | Instantiating formula (389) with e20, e20, e21, all_0_161_161 and discharging atoms op2(e20, e20) = all_0_161_161, op2(e20, e20) = e21, yields: % 11.25/3.02 | (706) all_0_161_161 = e21 % 11.25/3.02 | % 11.25/3.02 | Instantiating formula (389) with e20, e20, e20, all_0_87_87 and discharging atoms op2(e20, e20) = all_0_87_87, op2(e20, e20) = e20, yields: % 11.25/3.02 | (707) all_0_87_87 = e20 % 11.25/3.02 | % 11.25/3.02 | Combining equations (704,707) yields a new equation: % 11.25/3.02 | (708) all_0_161_161 = e20 % 11.25/3.02 | % 11.25/3.02 | Simplifying 708 yields: % 11.25/3.02 | (709) all_0_161_161 = e20 % 11.25/3.02 | % 11.25/3.02 | Combining equations (706,705) yields a new equation: % 11.25/3.02 | (710) all_0_163_163 = e21 % 11.25/3.02 | % 11.25/3.02 | Combining equations (709,705) yields a new equation: % 11.25/3.02 | (711) all_0_163_163 = e20 % 11.25/3.02 | % 11.25/3.02 | Combining equations (711,710) yields a new equation: % 11.25/3.02 | (678) e21 = e20 % 11.25/3.02 | % 11.25/3.02 | Equations (678) can reduce 359 to: % 11.25/3.02 | (433) $false % 11.25/3.02 | % 11.25/3.02 |-The branch is then unsatisfiable % 11.25/3.02 |-Branch two: % 11.25/3.02 | (445) ~ (all_0_172_172 = e20) % 11.25/3.02 | (450) all_0_172_172 = e22 % 11.25/3.02 | % 11.25/3.02 | Equations (450) can reduce 481 to: % 11.25/3.02 | (433) $false % 11.25/3.02 | % 11.25/3.02 |-The branch is then unsatisfiable % 11.25/3.02 |-Branch two: % 11.25/3.02 | (428) ~ (all_0_175_175 = e20) % 11.25/3.02 | (439) all_0_175_175 = e21 % 11.25/3.02 | % 11.25/3.02 | Equations (439) can reduce 682 to: % 11.25/3.02 | (433) $false % 11.25/3.02 | % 11.25/3.02 |-The branch is then unsatisfiable % 11.25/3.02 |-Branch two: % 11.25/3.02 | (720) ~ (all_0_174_174 = e21) % 11.25/3.02 | (439) all_0_175_175 = e21 % 11.25/3.02 | % 11.25/3.02 | Equations (439) can reduce 682 to: % 11.25/3.02 | (433) $false % 11.25/3.02 | % 11.25/3.02 |-The branch is then unsatisfiable % 11.25/3.02 % SZS output end Proof for theBenchmark % 11.25/3.02 % 11.25/3.02 2538ms %------------------------------------------------------------------------------