%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : ALG102+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n017.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:07 EDT 2022 % Result : Theorem 6.66s 2.01s % Output : Proof 12.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : ALG102+1 : TPTP v8.1.0. Released v2.7.0. % 0.07/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.33 % Computer : n017.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Wed Jun 8 03:36:33 EDT 2022 % 0.12/0.34 % CPUTime : % 0.51/0.58 ____ _ % 0.51/0.58 ___ / __ \_____(_)___ ________ __________ % 0.51/0.58 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.51/0.58 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.51/0.58 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.51/0.58 % 0.51/0.58 A Theorem Prover for First-Order Logic % 0.51/0.58 (ePrincess v.1.0) % 0.51/0.58 % 0.51/0.58 (c) Philipp Rümmer, 2009-2015 % 0.51/0.58 (c) Peter Backeman, 2014-2015 % 0.51/0.58 (contributions by Angelo Brillout, Peter Baumgartner) % 0.51/0.58 Free software under GNU Lesser General Public License (LGPL). % 0.51/0.58 Bug reports to peter@backeman.se % 0.51/0.58 % 0.51/0.58 For more information, visit http://user.uu.se/~petba168/breu/ % 0.51/0.58 % 0.51/0.58 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.51/0.62 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 2.96/1.17 Prover 0: Preprocessing ... % 5.37/1.71 Prover 0: Constructing countermodel ... % 6.66/2.01 Prover 0: proved (1382ms) % 6.66/2.01 % 6.66/2.01 No countermodel exists, formula is valid % 6.66/2.01 % SZS status Theorem for theBenchmark % 6.66/2.01 % 6.66/2.01 Generating proof ... found it (size 744) % 11.00/3.02 % 11.00/3.02 % SZS output start Proof for theBenchmark % 11.00/3.02 Assumed formulas after preprocessing and simplification: % 11.00/3.02 | (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] : ( ~ (v21 = v20) & ~ (v21 = v18) & ~ (v21 = v15) & ~ (v21 = v12) & ~ (v21 = e21) & ~ (v21 = e20) & ~ (v20 = v17) & ~ (v20 = v14) & ~ (v20 = v11) & ~ (v20 = e21) & ~ (v20 = e20) & ~ (v19 = v18) & ~ (v19 = v17) & ~ (v19 = v16) & ~ (v19 = v13) & ~ (v19 = e23) & ~ (v19 = e20) & ~ (v18 = v17) & ~ (v18 = v15) & ~ (v18 = v12) & ~ (v18 = e23) & ~ (v17 = v14) & ~ (v17 = v11) & ~ (v17 = e23) & ~ (v16 = v15) & ~ (v16 = v14) & ~ (v16 = v13) & ~ (v16 = e22) & ~ (v16 = e20) & ~ (v15 = v14) & ~ (v15 = v12) & ~ (v15 = e22) & ~ (v14 = v11) & ~ (v14 = e22) & ~ (v13 = v12) & ~ (v13 = v11) & ~ (v13 = e20) & ~ (v12 = v11) & ~ (v12 = e20) & ~ (v11 = e20) & ~ (v10 = v9) & ~ (v10 = v7) & ~ (v10 = v4) & ~ (v10 = v1) & ~ (v10 = e11) & ~ (v10 = e10) & ~ (v9 = v6) & ~ (v9 = v3) & ~ (v9 = v0) & ~ (v9 = e11) & ~ (v9 = e10) & ~ (v8 = v7) & ~ (v8 = v6) & ~ (v8 = v5) & ~ (v8 = v2) & ~ (v8 = e13) & ~ (v8 = e10) & ~ (v7 = v6) & ~ (v7 = v4) & ~ (v7 = v1) & ~ (v7 = e13) & ~ (v6 = v3) & ~ (v6 = v0) & ~ (v6 = e13) & ~ (v5 = v4) & ~ (v5 = v3) & ~ (v5 = v2) & ~ (v5 = e12) & ~ (v5 = e10) & ~ (v4 = v3) & ~ (v4 = v1) & ~ (v4 = e12) & ~ (v3 = v0) & ~ (v3 = e12) & ~ (v2 = v1) & ~ (v2 = v0) & ~ (v2 = e10) & ~ (v1 = v0) & ~ (v1 = e10) & ~ (v0 = e10) & ~ (e23 = e22) & ~ (e23 = e21) & ~ (e23 = e20) & ~ (e23 = e13) & ~ (e23 = e12) & ~ (e23 = e11) & ~ (e23 = e10) & ~ (e22 = e21) & ~ (e22 = e20) & ~ (e22 = e13) & ~ (e22 = e12) & ~ (e22 = e11) & ~ (e22 = e10) & ~ (e21 = e20) & ~ (e21 = e13) & ~ (e21 = e12) & ~ (e21 = e11) & ~ (e21 = e10) & ~ (e20 = e13) & ~ (e20 = e12) & ~ (e20 = e11) & ~ (e20 = e10) & ~ (e13 = e12) & ~ (e13 = e11) & ~ (e13 = e10) & ~ (e12 = e11) & ~ (e12 = e10) & ~ (e11 = e10) & op1(e13, v10) = v32 & op1(e13, v9) = v31 & op1(e13, e13) = e10 & op1(e13, e12) = v10 & op1(e13, e11) = e11 & op1(e13, e10) = v9 & op1(e12, v8) = v30 & op1(e12, v7) = v29 & op1(e12, v6) = v28 & op1(e12, e13) = v8 & op1(e12, e12) = v7 & op1(e12, e11) = e13 & op1(e12, e10) = v6 & op1(e11, v5) = v27 & op1(e11, v4) = v26 & op1(e11, v3) = v25 & op1(e11, e13) = v5 & op1(e11, e12) = v4 & op1(e11, e11) = e12 & op1(e11, e10) = v3 & op1(e10, v2) = v24 & op1(e10, v1) = v23 & op1(e10, v0) = v22 & op1(e10, e13) = v2 & op1(e10, e12) = v1 & op1(e10, e11) = e10 & op1(e10, e10) = v0 & h1(v10) = v72 & h1(v9) = v69 & h1(v8) = v67 & h1(v7) = v65 & h1(v6) = v62 & h1(v5) = v60 & h1(v4) = v58 & h1(v3) = v56 & h1(v2) = v54 & h1(v1) = v52 & h1(v0) = v49 & h1(e13) = v45 & h1(e12) = v11 & h1(e11) = e20 & h1(e10) = v44 & h2(v10) = v85 & h2(v9) = v84 & h2(v8) = v83 & h2(v7) = v82 & h2(v6) = v81 & h2(v5) = v80 & h2(v4) = v79 & h2(v3) = v78 & h2(v2) = v77 & h2(v1) = v76 & h2(v0) = v75 & h2(e13) = e23 & h2(e12) = e22 & h2(e11) = e21 & h2(e10) = e20 & h3(v10) = v109 & h3(v9) = v106 & h3(v8) = v104 & h3(v7) = v102 & h3(v6) = v99 & h3(v5) = v97 & h3(v4) = v95 & h3(v3) = v93 & h3(v2) = v91 & h3(v1) = v89 & h3(v0) = v86 & h3(e13) = v47 & h3(e12) = v18 & h3(e11) = e22 & h3(e10) = v46 & h4(v10) = v132 & h4(v9) = v129 & h4(v8) = v127 & h4(v7) = v126 & h4(v6) = v124 & h4(v5) = v122 & h4(v4) = v121 & h4(v3) = v119 & h4(v2) = v117 & h4(v1) = v115 & h4(v0) = v112 & h4(e13) = v13 & h4(e12) = e20 & h4(e11) = e23 & h4(e10) = v48 & op2(v48, v48) = v113 & op2(v48, v13) = v118 & op2(v48, e23) = v114 & op2(v48, e20) = v116 & op2(v47, v47) = v111 & op2(v47, v47) = v46 & op2(v47, v46) = v107 & op2(v47, v18) = v110 & op2(v47, e22) = v108 & op2(v46, v47) = v92 & op2(v46, v46) = v87 & op2(v46, v18) = v90 & op2(v46, e22) = v88 & op2(v45, v45) = v74 & op2(v45, v45) = v44 & op2(v45, v44) = v70 & op2(v45, v11) = v73 & op2(v45, e20) = v71 & op2(v44, v45) = v55 & op2(v44, v44) = v50 & op2(v44, v11) = v53 & op2(v44, e20) = v51 & op2(v18, v47) = v105 & op2(v18, v46) = v100 & op2(v18, v18) = v103 & op2(v18, e22) = v101 & op2(v18, e22) = v47 & op2(v13, v48) = v130 & op2(v13, v13) = v134 & op2(v13, v13) = v48 & op2(v13, e23) = v131 & op2(v13, e20) = v133 & op2(v11, v45) = v68 & op2(v11, v44) = v63 & op2(v11, v11) = v66 & op2(v11, e20) = v64 & op2(v11, e20) = v45 & op2(e23, v48) = v120 & op2(e23, v21) = v43 & op2(e23, v20) = v42 & op2(e23, v13) = v123 & op2(e23, e23) = e20 & op2(e23, e22) = v21 & op2(e23, e21) = e21 & op2(e23, e20) = v20 & op2(e22, v47) = v98 & op2(e22, v46) = v94 & op2(e22, v19) = v41 & op2(e22, v18) = v96 & op2(e22, v18) = v40 & op2(e22, v17) = v39 & op2(e22, e23) = v19 & op2(e22, e22) = v18 & op2(e22, e21) = e23 & op2(e22, e20) = v17 & op2(e21, v16) = v38 & op2(e21, v15) = v37 & op2(e21, v14) = v36 & op2(e21, e23) = v16 & op2(e21, e22) = v15 & op2(e21, e21) = e22 & op2(e21, e20) = v14 & op2(e20, v48) = v125 & op2(e20, v45) = v61 & op2(e20, v44) = v57 & op2(e20, v13) = v128 & op2(e20, v13) = v35 & op2(e20, v12) = v34 & op2(e20, v11) = v59 & op2(e20, v11) = v33 & op2(e20, e23) = v13 & op2(e20, e22) = v12 & op2(e20, e21) = e20 & op2(e20, e20) = v11 & ! [v135] : ! [v136] : ! [v137] : ! [v138] : (v136 = v135 | ~ (op1(v138, v137) = v136) | ~ (op1(v138, v137) = v135)) & ! [v135] : ! [v136] : ! [v137] : ! [v138] : (v136 = v135 | ~ (op2(v138, v137) = v136) | ~ (op2(v138, v137) = v135)) & ! [v135] : ! [v136] : ! [v137] : (v136 = v135 | ~ (h1(v137) = v136) | ~ (h1(v137) = v135)) & ! [v135] : ! [v136] : ! [v137] : (v136 = v135 | ~ (h2(v137) = v136) | ~ (h2(v137) = v135)) & ! [v135] : ! [v136] : ! [v137] : (v136 = v135 | ~ (h3(v137) = v136) | ~ (h3(v137) = v135)) & ! [v135] : ! [v136] : ! [v137] : (v136 = v135 | ~ (h4(v137) = v136) | ~ (h4(v137) = v135)) & ( ~ (v134 = v48) | ~ (v133 = v132) | ~ (v131 = e23) | ~ (v130 = v129) | ~ (v128 = v127) | ~ (v126 = v11) | ~ (v125 = v124) | ~ (v123 = v122) | ~ (v121 = v20) | ~ (v120 = v119) | ~ (v118 = v117) | ~ (v116 = v115) | ~ (v114 = v48) | ~ (v113 = v112) | ( ~ (v48 = e22) & ~ (v13 = e22)) | ( ~ (v48 = e21) & ~ (v13 = e21))) & ( ~ (v111 = v46) | ~ (v110 = v109) | ~ (v108 = e22) | ~ (v107 = v106) | ~ (v105 = v104) | ~ (v103 = v102) | ~ (v101 = v47) | ~ (v100 = v99) | ~ (v98 = v97) | ~ (v96 = v95) | ~ (v94 = v93) | ~ (v92 = v91) | ~ (v90 = v89) | ~ (v88 = v46) | ~ (v87 = v86) | ( ~ (v47 = e23) & ~ (v46 = e23)) | ( ~ (v47 = e21) & ~ (v46 = e21) & ~ (v18 = e21)) | ( ~ (v47 = e20) & ~ (v46 = e20) & ~ (v18 = e20))) & ( ~ (v85 = v21) | ~ (v84 = v20) | ~ (v83 = v19) | ~ (v82 = v18) | ~ (v81 = v17) | ~ (v80 = v16) | ~ (v79 = v15) | ~ (v78 = v14) | ~ (v77 = v13) | ~ (v76 = v12) | ~ (v75 = v11)) & ( ~ (v74 = v44) | ~ (v73 = v72) | ~ (v71 = e20) | ~ (v70 = v69) | ~ (v68 = v67) | ~ (v66 = v65) | ~ (v64 = v45) | ~ (v63 = v62) | ~ (v61 = v60) | ~ (v59 = v58) | ~ (v57 = v56) | ~ (v55 = v54) | ~ (v53 = v52) | ~ (v51 = v44) | ~ (v50 = v49) | ( ~ (v45 = e23) & ~ (v44 = e23) & ~ (v11 = e23)) | ( ~ (v45 = e22) & ~ (v44 = e22) & ~ (v11 = e22)) | ( ~ (v45 = e21) & ~ (v44 = e21) & ~ (v11 = e21))) & (v21 = e23 | v21 = e22) & (v21 = e23 | v20 = e23) & (v21 = e23 | v15 = e23 | v12 = e23) & (v21 = e22 | v20 = e22) & (v21 = e22 | v18 = e22 | v12 = e22) & (v20 = e23 | v20 = e22) & (v20 = e23 | v14 = e23 | v11 = e23) & (v20 = e22 | v17 = e22 | v11 = e22) & (v19 = e22 | v19 = e21) & (v19 = e22 | v18 = e22 | v17 = e22) & (v19 = e22 | v13 = e22) & (v19 = e21 | v18 = e21 | v17 = e21) & (v19 = e21 | v16 = e21 | v13 = e21) & (v18 = e22 | v18 = e21 | v18 = e20) & (v18 = e21 | v15 = e21 | v12 = e21) & (v18 = e20 | v17 = e20) & (v18 = e20 | v15 = e20) & (v17 = e22 | v17 = e21 | v17 = e20) & (v17 = e21 | v14 = e21 | v11 = e21) & (v17 = e20 | v14 = e20) & (v16 = e23 | v16 = e21) & (v16 = e23 | v15 = e23 | v14 = e23) & (v16 = e23 | v13 = e23) & (v16 = e21 | v15 = e21 | v14 = e21) & (v15 = e23 | v15 = e21 | v15 = e20) & (v15 = e20 | v14 = e20) & (v14 = e23 | v14 = e21 | v14 = e20) & (v13 = e23 | v13 = e22 | v13 = e21) & (v13 = e23 | v12 = e23 | v11 = e23) & (v13 = e22 | v12 = e22 | v11 = e22) & (v13 = e21 | v12 = e21 | v11 = e21) & (v12 = e23 | v12 = e22 | v12 = e21) & (v11 = e23 | v11 = e22 | v11 = e21) & (v10 = e13 | v10 = e12) & (v10 = e13 | v9 = e13) & (v10 = e13 | v4 = e13 | v1 = e13) & (v10 = e12 | v9 = e12) & (v10 = e12 | v7 = e12 | v1 = e12) & (v9 = e13 | v9 = e12) & (v9 = e13 | v3 = e13 | v0 = e13) & (v9 = e12 | v6 = e12 | v0 = e12) & (v8 = e12 | v8 = e11) & (v8 = e12 | v7 = e12 | v6 = e12) & (v8 = e12 | v2 = e12) & (v8 = e11 | v7 = e11 | v6 = e11) & (v8 = e11 | v5 = e11 | v2 = e11) & (v7 = e12 | v7 = e11 | v7 = e10) & (v7 = e11 | v4 = e11 | v1 = e11) & (v7 = e10 | v6 = e10) & (v7 = e10 | v4 = e10) & (v6 = e12 | v6 = e11 | v6 = e10) & (v6 = e11 | v3 = e11 | v0 = e11) & (v6 = e10 | v3 = e10) & (v5 = e13 | v5 = e11) & (v5 = e13 | v4 = e13 | v3 = e13) & (v5 = e13 | v2 = e13) & (v5 = e11 | v4 = e11 | v3 = e11) & (v4 = e13 | v4 = e11 | v4 = e10) & (v4 = e10 | v3 = e10) & (v3 = e13 | v3 = e11 | v3 = e10) & (v2 = e13 | v2 = e12 | v2 = e11) & (v2 = e13 | v1 = e13 | v0 = e13) & (v2 = e12 | v1 = e12 | v0 = e12) & (v2 = e11 | v1 = e11 | v0 = e11) & (v1 = e13 | v1 = e12 | v1 = e11) & (v0 = e13 | v0 = e12 | v0 = e11) & ((v43 = e22 & v42 = e20 & v20 = e23 & ~ (v19 = e22) & ~ (v16 = e21)) | (v41 = e23 & v40 = e22 & v39 = e20 & v19 = e21 & ~ (v21 = e23)) | (v38 = e23 & v37 = e22 & v36 = e20 & v15 = e21 & v11 = e21) | (v35 = e23 & v34 = e22 & v33 = e20 & v11 = e21 & ~ (v14 = e21) & ( ~ (v17 = e22) | v18 = e20))) & ((v32 = e12 & v31 = e10 & v9 = e13 & ~ (v8 = e12) & ~ (v5 = e11)) | (v30 = e13 & v29 = e12 & v28 = e10 & v8 = e11 & ~ (v10 = e13)) | (v27 = e13 & v26 = e12 & v25 = e10 & v4 = e11 & v0 = e11) | (v24 = e13 & v23 = e12 & v22 = e10 & v0 = e11 & ~ (v3 = e11) & ( ~ (v6 = e12) | v7 = e10))) & ((v21 = e23 & v11 = e22) | (v21 = e23 & ~ (v15 = e21)) | (v19 = e22 & v11 = e23) | (v18 = e21 & ~ (v11 = e21)) | (v18 = e20 & v14 = e21 & ~ (v17 = e22)) | (v17 = e22 & ~ (v20 = e23) & ~ (v18 = e20)) | (v16 = e21 & v11 = e23) | (v14 = e21 & ~ (v20 = e23))) & ((v10 = e13 & v0 = e12) | (v10 = e13 & ~ (v4 = e11)) | (v8 = e12 & v0 = e13) | (v7 = e11 & ~ (v0 = e11)) | (v7 = e10 & v3 = e11 & ~ (v6 = e12)) | (v6 = e12 & ~ (v9 = e13) & ~ (v7 = e10)) | (v5 = e11 & v0 = e13) | (v3 = e11 & ~ (v9 = e13)))) % 11.14/3.08 | 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 yields: % 11.14/3.08 | (1) ~ (all_0_113_113 = all_0_114_114) & ~ (all_0_113_113 = all_0_116_116) & ~ (all_0_113_113 = all_0_119_119) & ~ (all_0_113_113 = all_0_122_122) & ~ (all_0_113_113 = e21) & ~ (all_0_113_113 = e20) & ~ (all_0_114_114 = all_0_117_117) & ~ (all_0_114_114 = all_0_120_120) & ~ (all_0_114_114 = all_0_123_123) & ~ (all_0_114_114 = e21) & ~ (all_0_114_114 = e20) & ~ (all_0_115_115 = all_0_116_116) & ~ (all_0_115_115 = all_0_117_117) & ~ (all_0_115_115 = all_0_118_118) & ~ (all_0_115_115 = all_0_121_121) & ~ (all_0_115_115 = e23) & ~ (all_0_115_115 = e20) & ~ (all_0_116_116 = all_0_117_117) & ~ (all_0_116_116 = all_0_119_119) & ~ (all_0_116_116 = all_0_122_122) & ~ (all_0_116_116 = e23) & ~ (all_0_117_117 = all_0_120_120) & ~ (all_0_117_117 = all_0_123_123) & ~ (all_0_117_117 = e23) & ~ (all_0_118_118 = all_0_119_119) & ~ (all_0_118_118 = all_0_120_120) & ~ (all_0_118_118 = all_0_121_121) & ~ (all_0_118_118 = e22) & ~ (all_0_118_118 = e20) & ~ (all_0_119_119 = all_0_120_120) & ~ (all_0_119_119 = all_0_122_122) & ~ (all_0_119_119 = e22) & ~ (all_0_120_120 = all_0_123_123) & ~ (all_0_120_120 = e22) & ~ (all_0_121_121 = all_0_122_122) & ~ (all_0_121_121 = all_0_123_123) & ~ (all_0_121_121 = e20) & ~ (all_0_122_122 = all_0_123_123) & ~ (all_0_122_122 = e20) & ~ (all_0_123_123 = e20) & ~ (all_0_124_124 = all_0_125_125) & ~ (all_0_124_124 = all_0_127_127) & ~ (all_0_124_124 = all_0_130_130) & ~ (all_0_124_124 = all_0_133_133) & ~ (all_0_124_124 = e11) & ~ (all_0_124_124 = e10) & ~ (all_0_125_125 = all_0_128_128) & ~ (all_0_125_125 = all_0_131_131) & ~ (all_0_125_125 = all_0_134_134) & ~ (all_0_125_125 = e11) & ~ (all_0_125_125 = e10) & ~ (all_0_126_126 = all_0_127_127) & ~ (all_0_126_126 = all_0_128_128) & ~ (all_0_126_126 = all_0_129_129) & ~ (all_0_126_126 = all_0_132_132) & ~ (all_0_126_126 = e13) & ~ (all_0_126_126 = e10) & ~ (all_0_127_127 = all_0_128_128) & ~ (all_0_127_127 = all_0_130_130) & ~ (all_0_127_127 = all_0_133_133) & ~ (all_0_127_127 = e13) & ~ (all_0_128_128 = all_0_131_131) & ~ (all_0_128_128 = all_0_134_134) & ~ (all_0_128_128 = e13) & ~ (all_0_129_129 = all_0_130_130) & ~ (all_0_129_129 = all_0_131_131) & ~ (all_0_129_129 = all_0_132_132) & ~ (all_0_129_129 = e12) & ~ (all_0_129_129 = e10) & ~ (all_0_130_130 = all_0_131_131) & ~ (all_0_130_130 = all_0_133_133) & ~ (all_0_130_130 = e12) & ~ (all_0_131_131 = all_0_134_134) & ~ (all_0_131_131 = e12) & ~ (all_0_132_132 = all_0_133_133) & ~ (all_0_132_132 = all_0_134_134) & ~ (all_0_132_132 = e10) & ~ (all_0_133_133 = all_0_134_134) & ~ (all_0_133_133 = e10) & ~ (all_0_134_134 = e10) & ~ (e23 = e22) & ~ (e23 = e21) & ~ (e23 = e20) & ~ (e23 = e13) & ~ (e23 = e12) & ~ (e23 = e11) & ~ (e23 = e10) & ~ (e22 = e21) & ~ (e22 = e20) & ~ (e22 = e13) & ~ (e22 = e12) & ~ (e22 = e11) & ~ (e22 = e10) & ~ (e21 = e20) & ~ (e21 = e13) & ~ (e21 = e12) & ~ (e21 = e11) & ~ (e21 = e10) & ~ (e20 = e13) & ~ (e20 = e12) & ~ (e20 = e11) & ~ (e20 = e10) & ~ (e13 = e12) & ~ (e13 = e11) & ~ (e13 = e10) & ~ (e12 = e11) & ~ (e12 = e10) & ~ (e11 = e10) & op1(e13, all_0_124_124) = all_0_102_102 & op1(e13, all_0_125_125) = all_0_103_103 & op1(e13, e13) = e10 & op1(e13, e12) = all_0_124_124 & op1(e13, e11) = e11 & op1(e13, e10) = all_0_125_125 & op1(e12, all_0_126_126) = all_0_104_104 & op1(e12, all_0_127_127) = all_0_105_105 & op1(e12, all_0_128_128) = all_0_106_106 & op1(e12, e13) = all_0_126_126 & op1(e12, e12) = all_0_127_127 & op1(e12, e11) = e13 & op1(e12, e10) = all_0_128_128 & op1(e11, all_0_129_129) = all_0_107_107 & op1(e11, all_0_130_130) = all_0_108_108 & op1(e11, all_0_131_131) = all_0_109_109 & op1(e11, e13) = all_0_129_129 & op1(e11, e12) = all_0_130_130 & op1(e11, e11) = e12 & op1(e11, e10) = all_0_131_131 & op1(e10, all_0_132_132) = all_0_110_110 & op1(e10, all_0_133_133) = all_0_111_111 & op1(e10, all_0_134_134) = all_0_112_112 & op1(e10, e13) = all_0_132_132 & op1(e10, e12) = all_0_133_133 & op1(e10, e11) = e10 & op1(e10, e10) = all_0_134_134 & h1(all_0_124_124) = all_0_62_62 & h1(all_0_125_125) = all_0_65_65 & h1(all_0_126_126) = all_0_67_67 & h1(all_0_127_127) = all_0_69_69 & h1(all_0_128_128) = all_0_72_72 & h1(all_0_129_129) = all_0_74_74 & h1(all_0_130_130) = all_0_76_76 & h1(all_0_131_131) = all_0_78_78 & h1(all_0_132_132) = all_0_80_80 & h1(all_0_133_133) = all_0_82_82 & h1(all_0_134_134) = all_0_85_85 & h1(e13) = all_0_89_89 & h1(e12) = all_0_123_123 & h1(e11) = e20 & h1(e10) = all_0_90_90 & h2(all_0_124_124) = all_0_49_49 & h2(all_0_125_125) = all_0_50_50 & h2(all_0_126_126) = all_0_51_51 & h2(all_0_127_127) = all_0_52_52 & h2(all_0_128_128) = all_0_53_53 & h2(all_0_129_129) = all_0_54_54 & h2(all_0_130_130) = all_0_55_55 & h2(all_0_131_131) = all_0_56_56 & h2(all_0_132_132) = all_0_57_57 & h2(all_0_133_133) = all_0_58_58 & h2(all_0_134_134) = all_0_59_59 & h2(e13) = e23 & h2(e12) = e22 & h2(e11) = e21 & h2(e10) = e20 & h3(all_0_124_124) = all_0_25_25 & h3(all_0_125_125) = all_0_28_28 & h3(all_0_126_126) = all_0_30_30 & h3(all_0_127_127) = all_0_32_32 & h3(all_0_128_128) = all_0_35_35 & h3(all_0_129_129) = all_0_37_37 & h3(all_0_130_130) = all_0_39_39 & h3(all_0_131_131) = all_0_41_41 & h3(all_0_132_132) = all_0_43_43 & h3(all_0_133_133) = all_0_45_45 & h3(all_0_134_134) = all_0_48_48 & h3(e13) = all_0_87_87 & h3(e12) = all_0_116_116 & h3(e11) = e22 & h3(e10) = all_0_88_88 & h4(all_0_124_124) = all_0_2_2 & h4(all_0_125_125) = all_0_5_5 & h4(all_0_126_126) = all_0_7_7 & h4(all_0_127_127) = all_0_8_8 & h4(all_0_128_128) = all_0_10_10 & h4(all_0_129_129) = all_0_12_12 & h4(all_0_130_130) = all_0_13_13 & h4(all_0_131_131) = all_0_15_15 & h4(all_0_132_132) = all_0_17_17 & h4(all_0_133_133) = all_0_19_19 & h4(all_0_134_134) = all_0_22_22 & h4(e13) = all_0_121_121 & h4(e12) = e20 & h4(e11) = e23 & h4(e10) = all_0_86_86 & op2(all_0_86_86, all_0_86_86) = all_0_21_21 & op2(all_0_86_86, all_0_121_121) = all_0_16_16 & op2(all_0_86_86, e23) = all_0_20_20 & op2(all_0_86_86, e20) = all_0_18_18 & op2(all_0_87_87, all_0_87_87) = all_0_23_23 & op2(all_0_87_87, all_0_87_87) = all_0_88_88 & op2(all_0_87_87, all_0_88_88) = all_0_27_27 & op2(all_0_87_87, all_0_116_116) = all_0_24_24 & op2(all_0_87_87, e22) = all_0_26_26 & op2(all_0_88_88, all_0_87_87) = all_0_42_42 & op2(all_0_88_88, all_0_88_88) = all_0_47_47 & op2(all_0_88_88, all_0_116_116) = all_0_44_44 & op2(all_0_88_88, e22) = all_0_46_46 & op2(all_0_89_89, all_0_89_89) = all_0_60_60 & op2(all_0_89_89, all_0_89_89) = all_0_90_90 & op2(all_0_89_89, all_0_90_90) = all_0_64_64 & op2(all_0_89_89, all_0_123_123) = all_0_61_61 & op2(all_0_89_89, e20) = all_0_63_63 & op2(all_0_90_90, all_0_89_89) = all_0_79_79 & op2(all_0_90_90, all_0_90_90) = all_0_84_84 & op2(all_0_90_90, all_0_123_123) = all_0_81_81 & op2(all_0_90_90, e20) = all_0_83_83 & op2(all_0_116_116, all_0_87_87) = all_0_29_29 & op2(all_0_116_116, all_0_88_88) = all_0_34_34 & op2(all_0_116_116, all_0_116_116) = all_0_31_31 & op2(all_0_116_116, e22) = all_0_33_33 & op2(all_0_116_116, e22) = all_0_87_87 & op2(all_0_121_121, all_0_86_86) = all_0_4_4 & op2(all_0_121_121, all_0_121_121) = all_0_0_0 & op2(all_0_121_121, all_0_121_121) = all_0_86_86 & op2(all_0_121_121, e23) = all_0_3_3 & op2(all_0_121_121, e20) = all_0_1_1 & op2(all_0_123_123, all_0_89_89) = all_0_66_66 & op2(all_0_123_123, all_0_90_90) = all_0_71_71 & op2(all_0_123_123, all_0_123_123) = all_0_68_68 & op2(all_0_123_123, e20) = all_0_70_70 & op2(all_0_123_123, e20) = all_0_89_89 & op2(e23, all_0_86_86) = all_0_14_14 & op2(e23, all_0_113_113) = all_0_91_91 & op2(e23, all_0_114_114) = all_0_92_92 & op2(e23, all_0_121_121) = all_0_11_11 & op2(e23, e23) = e20 & op2(e23, e22) = all_0_113_113 & op2(e23, e21) = e21 & op2(e23, e20) = all_0_114_114 & op2(e22, all_0_87_87) = all_0_36_36 & op2(e22, all_0_88_88) = all_0_40_40 & op2(e22, all_0_115_115) = all_0_93_93 & op2(e22, all_0_116_116) = all_0_38_38 & op2(e22, all_0_116_116) = all_0_94_94 & op2(e22, all_0_117_117) = all_0_95_95 & op2(e22, e23) = all_0_115_115 & op2(e22, e22) = all_0_116_116 & op2(e22, e21) = e23 & op2(e22, e20) = all_0_117_117 & op2(e21, all_0_118_118) = all_0_96_96 & op2(e21, all_0_119_119) = all_0_97_97 & op2(e21, all_0_120_120) = all_0_98_98 & op2(e21, e23) = all_0_118_118 & op2(e21, e22) = all_0_119_119 & op2(e21, e21) = e22 & op2(e21, e20) = all_0_120_120 & op2(e20, all_0_86_86) = all_0_9_9 & op2(e20, all_0_89_89) = all_0_73_73 & op2(e20, all_0_90_90) = all_0_77_77 & op2(e20, all_0_121_121) = all_0_6_6 & op2(e20, all_0_121_121) = all_0_99_99 & op2(e20, all_0_122_122) = all_0_100_100 & op2(e20, all_0_123_123) = all_0_75_75 & op2(e20, all_0_123_123) = all_0_101_101 & op2(e20, e23) = all_0_121_121 & op2(e20, e22) = all_0_122_122 & op2(e20, e21) = e20 & op2(e20, e20) = all_0_123_123 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op1(v3, v2) = v1) | ~ (op1(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op2(v3, v2) = v1) | ~ (op2(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h1(v2) = v1) | ~ (h1(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h2(v2) = v1) | ~ (h2(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h3(v2) = v1) | ~ (h3(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h4(v2) = v1) | ~ (h4(v2) = v0)) & ( ~ (all_0_0_0 = all_0_86_86) | ~ (all_0_1_1 = all_0_2_2) | ~ (all_0_3_3 = e23) | ~ (all_0_4_4 = all_0_5_5) | ~ (all_0_6_6 = all_0_7_7) | ~ (all_0_8_8 = all_0_123_123) | ~ (all_0_9_9 = all_0_10_10) | ~ (all_0_11_11 = all_0_12_12) | ~ (all_0_13_13 = all_0_114_114) | ~ (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_86_86) | ~ (all_0_21_21 = all_0_22_22) | ( ~ (all_0_86_86 = e22) & ~ (all_0_121_121 = e22)) | ( ~ (all_0_86_86 = e21) & ~ (all_0_121_121 = e21))) & ( ~ (all_0_23_23 = all_0_88_88) | ~ (all_0_24_24 = all_0_25_25) | ~ (all_0_26_26 = e22) | ~ (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_87_87) | ~ (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_88_88) | ~ (all_0_47_47 = all_0_48_48) | ( ~ (all_0_87_87 = e23) & ~ (all_0_88_88 = e23)) | ( ~ (all_0_87_87 = e21) & ~ (all_0_88_88 = e21) & ~ (all_0_116_116 = e21)) | ( ~ (all_0_87_87 = e20) & ~ (all_0_88_88 = e20) & ~ (all_0_116_116 = e20))) & ( ~ (all_0_49_49 = all_0_113_113) | ~ (all_0_50_50 = all_0_114_114) | ~ (all_0_51_51 = all_0_115_115) | ~ (all_0_52_52 = all_0_116_116) | ~ (all_0_53_53 = all_0_117_117) | ~ (all_0_54_54 = all_0_118_118) | ~ (all_0_55_55 = all_0_119_119) | ~ (all_0_56_56 = all_0_120_120) | ~ (all_0_57_57 = all_0_121_121) | ~ (all_0_58_58 = all_0_122_122) | ~ (all_0_59_59 = all_0_123_123)) & ( ~ (all_0_60_60 = all_0_90_90) | ~ (all_0_61_61 = all_0_62_62) | ~ (all_0_63_63 = e20) | ~ (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_89_89) | ~ (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_90_90) | ~ (all_0_84_84 = all_0_85_85) | ( ~ (all_0_89_89 = e23) & ~ (all_0_90_90 = e23) & ~ (all_0_123_123 = e23)) | ( ~ (all_0_89_89 = e22) & ~ (all_0_90_90 = e22) & ~ (all_0_123_123 = e22)) | ( ~ (all_0_89_89 = e21) & ~ (all_0_90_90 = e21) & ~ (all_0_123_123 = e21))) & (all_0_113_113 = e23 | all_0_113_113 = e22) & (all_0_113_113 = e23 | all_0_114_114 = e23) & (all_0_113_113 = e23 | all_0_119_119 = e23 | all_0_122_122 = e23) & (all_0_113_113 = e22 | all_0_114_114 = e22) & (all_0_113_113 = e22 | all_0_116_116 = e22 | all_0_122_122 = e22) & (all_0_114_114 = e23 | all_0_114_114 = e22) & (all_0_114_114 = e23 | all_0_120_120 = e23 | all_0_123_123 = e23) & (all_0_114_114 = e22 | all_0_117_117 = e22 | all_0_123_123 = e22) & (all_0_115_115 = e22 | all_0_115_115 = e21) & (all_0_115_115 = e22 | all_0_116_116 = e22 | all_0_117_117 = e22) & (all_0_115_115 = e22 | all_0_121_121 = e22) & (all_0_115_115 = e21 | all_0_116_116 = e21 | all_0_117_117 = e21) & (all_0_115_115 = e21 | all_0_118_118 = e21 | all_0_121_121 = e21) & (all_0_116_116 = e22 | all_0_116_116 = e21 | all_0_116_116 = e20) & (all_0_116_116 = e21 | all_0_119_119 = e21 | all_0_122_122 = e21) & (all_0_116_116 = e20 | all_0_117_117 = e20) & (all_0_116_116 = e20 | all_0_119_119 = e20) & (all_0_117_117 = e22 | all_0_117_117 = e21 | all_0_117_117 = e20) & (all_0_117_117 = e21 | all_0_120_120 = e21 | all_0_123_123 = e21) & (all_0_117_117 = e20 | all_0_120_120 = e20) & (all_0_118_118 = e23 | all_0_118_118 = e21) & (all_0_118_118 = e23 | all_0_119_119 = e23 | all_0_120_120 = e23) & (all_0_118_118 = e23 | all_0_121_121 = e23) & (all_0_118_118 = e21 | all_0_119_119 = e21 | all_0_120_120 = e21) & (all_0_119_119 = e23 | all_0_119_119 = e21 | all_0_119_119 = e20) & (all_0_119_119 = e20 | all_0_120_120 = e20) & (all_0_120_120 = e23 | all_0_120_120 = e21 | all_0_120_120 = e20) & (all_0_121_121 = e23 | all_0_121_121 = e22 | all_0_121_121 = e21) & (all_0_121_121 = e23 | all_0_122_122 = e23 | all_0_123_123 = e23) & (all_0_121_121 = e22 | all_0_122_122 = e22 | all_0_123_123 = e22) & (all_0_121_121 = e21 | all_0_122_122 = e21 | all_0_123_123 = e21) & (all_0_122_122 = e23 | all_0_122_122 = e22 | all_0_122_122 = e21) & (all_0_123_123 = e23 | all_0_123_123 = e22 | all_0_123_123 = e21) & (all_0_124_124 = e13 | all_0_124_124 = e12) & (all_0_124_124 = e13 | all_0_125_125 = e13) & (all_0_124_124 = e13 | all_0_130_130 = e13 | all_0_133_133 = e13) & (all_0_124_124 = e12 | all_0_125_125 = e12) & (all_0_124_124 = e12 | all_0_127_127 = e12 | all_0_133_133 = e12) & (all_0_125_125 = e13 | all_0_125_125 = e12) & (all_0_125_125 = e13 | all_0_131_131 = e13 | all_0_134_134 = e13) & (all_0_125_125 = e12 | all_0_128_128 = e12 | all_0_134_134 = e12) & (all_0_126_126 = e12 | all_0_126_126 = e11) & (all_0_126_126 = e12 | all_0_127_127 = e12 | all_0_128_128 = e12) & (all_0_126_126 = e12 | all_0_132_132 = e12) & (all_0_126_126 = e11 | all_0_127_127 = e11 | all_0_128_128 = e11) & (all_0_126_126 = e11 | all_0_129_129 = e11 | all_0_132_132 = e11) & (all_0_127_127 = e12 | all_0_127_127 = e11 | all_0_127_127 = e10) & (all_0_127_127 = e11 | all_0_130_130 = e11 | all_0_133_133 = e11) & (all_0_127_127 = e10 | all_0_128_128 = e10) & (all_0_127_127 = e10 | all_0_130_130 = e10) & (all_0_128_128 = e12 | all_0_128_128 = e11 | all_0_128_128 = e10) & (all_0_128_128 = e11 | all_0_131_131 = e11 | all_0_134_134 = e11) & (all_0_128_128 = e10 | all_0_131_131 = e10) & (all_0_129_129 = e13 | all_0_129_129 = e11) & (all_0_129_129 = e13 | all_0_130_130 = e13 | all_0_131_131 = e13) & (all_0_129_129 = e13 | all_0_132_132 = e13) & (all_0_129_129 = e11 | all_0_130_130 = e11 | all_0_131_131 = e11) & (all_0_130_130 = e13 | all_0_130_130 = e11 | all_0_130_130 = e10) & (all_0_130_130 = e10 | all_0_131_131 = e10) & (all_0_131_131 = e13 | all_0_131_131 = e11 | all_0_131_131 = e10) & (all_0_132_132 = e13 | all_0_132_132 = e12 | all_0_132_132 = e11) & (all_0_132_132 = e13 | all_0_133_133 = e13 | all_0_134_134 = e13) & (all_0_132_132 = e12 | all_0_133_133 = e12 | all_0_134_134 = e12) & (all_0_132_132 = e11 | all_0_133_133 = e11 | all_0_134_134 = e11) & (all_0_133_133 = e13 | all_0_133_133 = e12 | all_0_133_133 = e11) & (all_0_134_134 = e13 | all_0_134_134 = e12 | all_0_134_134 = e11) & ((all_0_91_91 = e22 & all_0_92_92 = e20 & all_0_114_114 = e23 & ~ (all_0_115_115 = e22) & ~ (all_0_118_118 = e21)) | (all_0_93_93 = e23 & all_0_94_94 = e22 & all_0_95_95 = e20 & all_0_115_115 = e21 & ~ (all_0_113_113 = e23)) | (all_0_96_96 = e23 & all_0_97_97 = e22 & all_0_98_98 = e20 & all_0_119_119 = e21 & all_0_123_123 = e21) | (all_0_99_99 = e23 & all_0_100_100 = e22 & all_0_101_101 = e20 & all_0_123_123 = e21 & ~ (all_0_120_120 = e21) & ( ~ (all_0_117_117 = e22) | all_0_116_116 = e20))) & ((all_0_102_102 = e12 & all_0_103_103 = e10 & all_0_125_125 = e13 & ~ (all_0_126_126 = e12) & ~ (all_0_129_129 = e11)) | (all_0_104_104 = e13 & all_0_105_105 = e12 & all_0_106_106 = e10 & all_0_126_126 = e11 & ~ (all_0_124_124 = e13)) | (all_0_107_107 = e13 & all_0_108_108 = e12 & all_0_109_109 = e10 & all_0_130_130 = e11 & all_0_134_134 = e11) | (all_0_110_110 = e13 & all_0_111_111 = e12 & all_0_112_112 = e10 & all_0_134_134 = e11 & ~ (all_0_131_131 = e11) & ( ~ (all_0_128_128 = e12) | all_0_127_127 = e10))) & ((all_0_113_113 = e23 & all_0_123_123 = e22) | (all_0_113_113 = e23 & ~ (all_0_119_119 = e21)) | (all_0_115_115 = e22 & all_0_123_123 = e23) | (all_0_116_116 = e21 & ~ (all_0_123_123 = e21)) | (all_0_116_116 = e20 & all_0_120_120 = e21 & ~ (all_0_117_117 = e22)) | (all_0_117_117 = e22 & ~ (all_0_114_114 = e23) & ~ (all_0_116_116 = e20)) | (all_0_118_118 = e21 & all_0_123_123 = e23) | (all_0_120_120 = e21 & ~ (all_0_114_114 = e23))) & ((all_0_124_124 = e13 & all_0_134_134 = e12) | (all_0_124_124 = e13 & ~ (all_0_130_130 = e11)) | (all_0_126_126 = e12 & all_0_134_134 = e13) | (all_0_127_127 = e11 & ~ (all_0_134_134 = e11)) | (all_0_127_127 = e10 & all_0_131_131 = e11 & ~ (all_0_128_128 = e12)) | (all_0_128_128 = e12 & ~ (all_0_125_125 = e13) & ~ (all_0_127_127 = e10)) | (all_0_129_129 = e11 & all_0_134_134 = e13) | (all_0_131_131 = e11 & ~ (all_0_125_125 = e13))) % 11.14/3.10 | % 11.14/3.10 | Applying alpha-rule on (1) yields: % 11.14/3.10 | (2) op2(e23, e21) = e21 % 11.14/3.10 | (3) all_0_133_133 = e13 | all_0_133_133 = e12 | all_0_133_133 = e11 % 11.14/3.10 | (4) op2(all_0_89_89, all_0_89_89) = all_0_90_90 % 11.14/3.10 | (5) ~ (all_0_114_114 = all_0_117_117) % 11.14/3.10 | (6) op1(e13, e11) = e11 % 11.14/3.10 | (7) all_0_126_126 = e12 | all_0_127_127 = e12 | all_0_128_128 = e12 % 11.14/3.10 | (8) h2(all_0_128_128) = all_0_53_53 % 11.14/3.10 | (9) ~ (all_0_128_128 = all_0_134_134) % 11.14/3.10 | (10) ~ (all_0_118_118 = all_0_121_121) % 11.14/3.10 | (11) h3(e11) = e22 % 11.14/3.10 | (12) ~ (e22 = e13) % 11.14/3.10 | (13) h4(all_0_134_134) = all_0_22_22 % 11.14/3.10 | (14) ~ (all_0_125_125 = all_0_131_131) % 11.14/3.10 | (15) all_0_130_130 = e10 | all_0_131_131 = e10 % 11.14/3.10 | (16) op2(all_0_88_88, all_0_87_87) = all_0_42_42 % 11.14/3.10 | (17) op2(e20, all_0_121_121) = all_0_6_6 % 11.14/3.10 | (18) h4(all_0_132_132) = all_0_17_17 % 11.14/3.10 | (19) op2(e20, all_0_123_123) = all_0_101_101 % 11.14/3.10 | (20) all_0_113_113 = e22 | all_0_114_114 = e22 % 11.14/3.10 | (21) all_0_124_124 = e12 | all_0_127_127 = e12 | all_0_133_133 = e12 % 11.14/3.10 | (22) ~ (all_0_127_127 = all_0_133_133) % 11.14/3.10 | (23) op2(all_0_116_116, e22) = all_0_87_87 % 11.14/3.10 | (24) op2(all_0_87_87, all_0_87_87) = all_0_23_23 % 11.14/3.10 | (25) ~ (all_0_115_115 = all_0_121_121) % 11.14/3.10 | (26) op2(all_0_87_87, all_0_116_116) = all_0_24_24 % 11.14/3.10 | (27) op2(all_0_121_121, e20) = all_0_1_1 % 11.14/3.10 | (28) h3(all_0_126_126) = all_0_30_30 % 11.14/3.10 | (29) ~ (all_0_124_124 = all_0_130_130) % 11.14/3.10 | (30) ~ (e21 = e11) % 11.14/3.10 | (31) op1(e13, e10) = all_0_125_125 % 11.14/3.10 | (32) (all_0_91_91 = e22 & all_0_92_92 = e20 & all_0_114_114 = e23 & ~ (all_0_115_115 = e22) & ~ (all_0_118_118 = e21)) | (all_0_93_93 = e23 & all_0_94_94 = e22 & all_0_95_95 = e20 & all_0_115_115 = e21 & ~ (all_0_113_113 = e23)) | (all_0_96_96 = e23 & all_0_97_97 = e22 & all_0_98_98 = e20 & all_0_119_119 = e21 & all_0_123_123 = e21) | (all_0_99_99 = e23 & all_0_100_100 = e22 & all_0_101_101 = e20 & all_0_123_123 = e21 & ~ (all_0_120_120 = e21) & ( ~ (all_0_117_117 = e22) | all_0_116_116 = e20)) % 11.14/3.10 | (33) all_0_119_119 = e20 | all_0_120_120 = e20 % 11.14/3.10 | (34) ~ (all_0_128_128 = e13) % 11.14/3.10 | (35) ~ (all_0_113_113 = all_0_119_119) % 11.14/3.10 | (36) all_0_114_114 = e23 | all_0_120_120 = e23 | all_0_123_123 = e23 % 11.14/3.11 | (37) h3(e10) = all_0_88_88 % 11.14/3.11 | (38) all_0_127_127 = e10 | all_0_130_130 = e10 % 11.14/3.11 | (39) ~ (all_0_126_126 = all_0_128_128) % 11.14/3.11 | (40) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h3(v2) = v1) | ~ (h3(v2) = v0)) % 11.14/3.11 | (41) op2(e20, all_0_121_121) = all_0_99_99 % 11.14/3.11 | (42) all_0_116_116 = e20 | all_0_117_117 = e20 % 11.14/3.11 | (43) ~ (all_0_120_120 = all_0_123_123) % 11.14/3.11 | (44) ~ (all_0_115_115 = all_0_116_116) % 11.14/3.11 | (45) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op1(v3, v2) = v1) | ~ (op1(v3, v2) = v0)) % 11.14/3.11 | (46) all_0_116_116 = e21 | all_0_119_119 = e21 | all_0_122_122 = e21 % 11.14/3.11 | (47) ~ (all_0_121_121 = all_0_122_122) % 11.14/3.11 | (48) all_0_116_116 = e20 | all_0_119_119 = e20 % 11.14/3.11 | (49) op2(all_0_90_90, e20) = all_0_83_83 % 11.14/3.11 | (50) ~ (all_0_129_129 = all_0_132_132) % 11.14/3.11 | (51) ~ (all_0_117_117 = all_0_120_120) % 11.14/3.11 | (52) ~ (all_0_115_115 = all_0_118_118) % 11.14/3.11 | (53) all_0_128_128 = e10 | all_0_131_131 = e10 % 11.14/3.11 | (54) ~ (all_0_119_119 = all_0_122_122) % 11.14/3.11 | (55) op1(e10, e11) = e10 % 11.14/3.11 | (56) ~ (all_0_127_127 = e13) % 11.14/3.11 | (57) op2(e21, e20) = all_0_120_120 % 11.14/3.11 | (58) h1(all_0_134_134) = all_0_85_85 % 11.14/3.11 | (59) h3(all_0_130_130) = all_0_39_39 % 11.14/3.11 | (60) ~ (e12 = e11) % 11.14/3.11 | (61) all_0_134_134 = e13 | all_0_134_134 = e12 | all_0_134_134 = e11 % 11.14/3.11 | (62) all_0_121_121 = e22 | all_0_122_122 = e22 | all_0_123_123 = e22 % 11.14/3.11 | (63) op1(e10, all_0_132_132) = all_0_110_110 % 11.14/3.11 | (64) op2(all_0_123_123, e20) = all_0_70_70 % 11.14/3.11 | (65) ~ (all_0_132_132 = all_0_134_134) % 11.14/3.11 | (66) all_0_119_119 = e23 | all_0_119_119 = e21 | all_0_119_119 = e20 % 11.14/3.11 | (67) ~ (e23 = e10) % 11.14/3.11 | (68) ~ (all_0_127_127 = all_0_130_130) % 11.14/3.11 | (69) h4(all_0_127_127) = all_0_8_8 % 11.14/3.11 | (70) op2(e23, all_0_121_121) = all_0_11_11 % 11.14/3.11 | (71) ~ (all_0_131_131 = e12) % 11.14/3.11 | (72) ~ (all_0_115_115 = e23) % 11.14/3.11 | (73) all_0_118_118 = e21 | all_0_119_119 = e21 | all_0_120_120 = e21 % 11.14/3.11 | (74) h1(e11) = e20 % 11.14/3.11 | (75) h1(all_0_132_132) = all_0_80_80 % 11.14/3.11 | (76) op2(all_0_116_116, all_0_88_88) = all_0_34_34 % 11.14/3.11 | (77) ~ (e23 = e13) % 11.14/3.11 | (78) ~ (e13 = e10) % 11.14/3.11 | (79) h1(all_0_130_130) = all_0_76_76 % 11.14/3.11 | (80) all_0_115_115 = e22 | all_0_121_121 = e22 % 11.14/3.11 | (81) all_0_132_132 = e12 | all_0_133_133 = e12 | all_0_134_134 = e12 % 11.14/3.11 | (82) op2(all_0_121_121, e23) = all_0_3_3 % 11.14/3.11 | (83) op2(e23, e23) = e20 % 11.14/3.11 | (84) ~ (all_0_125_125 = all_0_128_128) % 11.14/3.11 | (85) op1(e11, e13) = all_0_129_129 % 11.14/3.11 | (86) ~ (all_0_114_114 = all_0_123_123) % 11.14/3.11 | (87) (all_0_102_102 = e12 & all_0_103_103 = e10 & all_0_125_125 = e13 & ~ (all_0_126_126 = e12) & ~ (all_0_129_129 = e11)) | (all_0_104_104 = e13 & all_0_105_105 = e12 & all_0_106_106 = e10 & all_0_126_126 = e11 & ~ (all_0_124_124 = e13)) | (all_0_107_107 = e13 & all_0_108_108 = e12 & all_0_109_109 = e10 & all_0_130_130 = e11 & all_0_134_134 = e11) | (all_0_110_110 = e13 & all_0_111_111 = e12 & all_0_112_112 = e10 & all_0_134_134 = e11 & ~ (all_0_131_131 = e11) & ( ~ (all_0_128_128 = e12) | all_0_127_127 = e10)) % 11.14/3.11 | (88) ~ (all_0_116_116 = all_0_117_117) % 11.14/3.11 | (89) all_0_117_117 = e21 | all_0_120_120 = e21 | all_0_123_123 = e21 % 11.14/3.11 | (90) op2(all_0_123_123, e20) = all_0_89_89 % 11.14/3.11 | (91) ~ (all_0_127_127 = all_0_128_128) % 11.14/3.11 | (92) h2(all_0_127_127) = all_0_52_52 % 11.14/3.11 | (93) op1(e11, all_0_129_129) = all_0_107_107 % 11.14/3.11 | (94) all_0_115_115 = e22 | all_0_115_115 = e21 % 11.14/3.11 | (95) all_0_126_126 = e12 | all_0_132_132 = e12 % 11.14/3.11 | (96) op2(all_0_86_86, e20) = all_0_18_18 % 11.14/3.11 | (97) h1(all_0_133_133) = all_0_82_82 % 11.14/3.11 | (98) ~ (all_0_131_131 = all_0_134_134) % 11.14/3.11 | (99) all_0_118_118 = e23 | all_0_121_121 = e23 % 11.14/3.11 | (100) op2(all_0_90_90, all_0_123_123) = all_0_81_81 % 11.14/3.11 | (101) h2(e13) = e23 % 11.14/3.11 | (102) op2(e21, e21) = e22 % 11.14/3.11 | (103) op2(e23, all_0_113_113) = all_0_91_91 % 11.14/3.11 | (104) ~ (e20 = e11) % 11.14/3.11 | (105) all_0_117_117 = e22 | all_0_117_117 = e21 | all_0_117_117 = e20 % 11.14/3.11 | (106) h2(all_0_130_130) = all_0_55_55 % 11.14/3.11 | (107) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h2(v2) = v1) | ~ (h2(v2) = v0)) % 11.14/3.11 | (108) ~ (e21 = e13) % 11.14/3.11 | (109) ~ (all_0_124_124 = all_0_127_127) % 11.14/3.11 | (110) ~ (all_0_124_124 = e11) % 11.14/3.11 | (111) h4(all_0_131_131) = all_0_15_15 % 11.14/3.11 | (112) ~ (all_0_132_132 = e10) % 11.14/3.11 | (113) op2(all_0_90_90, all_0_90_90) = all_0_84_84 % 11.14/3.11 | (114) ~ (e23 = e21) % 11.14/3.11 | (115) op1(e13, all_0_125_125) = all_0_103_103 % 11.14/3.11 | (116) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h4(v2) = v1) | ~ (h4(v2) = v0)) % 11.14/3.11 | (117) all_0_125_125 = e13 | all_0_125_125 = e12 % 11.14/3.11 | (118) all_0_124_124 = e12 | all_0_125_125 = e12 % 11.14/3.11 | (119) ~ (e12 = e10) % 11.14/3.11 | (120) ~ (all_0_114_114 = all_0_120_120) % 11.14/3.11 | (121) op1(e10, all_0_133_133) = all_0_111_111 % 11.14/3.11 | (122) h4(all_0_128_128) = all_0_10_10 % 11.14/3.11 | (123) h1(all_0_126_126) = all_0_67_67 % 11.14/3.11 | (124) h3(all_0_127_127) = all_0_32_32 % 11.14/3.11 | (125) h2(all_0_131_131) = all_0_56_56 % 11.14/3.11 | (126) op2(e22, all_0_117_117) = all_0_95_95 % 11.14/3.11 | (127) h1(all_0_129_129) = all_0_74_74 % 11.14/3.11 | (128) op2(e21, all_0_120_120) = all_0_98_98 % 11.14/3.11 | (129) ~ (all_0_124_124 = all_0_125_125) % 11.14/3.11 | (130) h4(e10) = all_0_86_86 % 11.14/3.11 | (131) ~ (all_0_120_120 = e22) % 11.14/3.11 | (132) op2(e22, e23) = all_0_115_115 % 11.14/3.11 | (133) ~ (all_0_119_119 = e22) % 11.14/3.11 | (134) ~ (e21 = e10) % 11.14/3.11 | (135) all_0_124_124 = e13 | all_0_130_130 = e13 | all_0_133_133 = e13 % 11.14/3.11 | (136) all_0_128_128 = e12 | all_0_128_128 = e11 | all_0_128_128 = e10 % 11.14/3.11 | (137) ~ (all_0_125_125 = e11) % 11.14/3.11 | (138) ~ (all_0_118_118 = all_0_120_120) % 11.14/3.11 | (139) all_0_120_120 = e23 | all_0_120_120 = e21 | all_0_120_120 = e20 % 11.14/3.12 | (140) ~ (e21 = e20) % 11.14/3.12 | (141) op2(all_0_86_86, e23) = all_0_20_20 % 11.14/3.12 | (142) op2(all_0_88_88, e22) = all_0_46_46 % 11.14/3.12 | (143) op2(all_0_121_121, all_0_121_121) = all_0_0_0 % 11.14/3.12 | (144) all_0_125_125 = e12 | all_0_128_128 = e12 | all_0_134_134 = e12 % 11.14/3.12 | (145) h2(all_0_125_125) = all_0_50_50 % 11.14/3.12 | (146) all_0_121_121 = e23 | all_0_121_121 = e22 | all_0_121_121 = e21 % 11.14/3.12 | (147) ~ (all_0_121_121 = e20) % 11.14/3.12 | (148) ~ (all_0_49_49 = all_0_113_113) | ~ (all_0_50_50 = all_0_114_114) | ~ (all_0_51_51 = all_0_115_115) | ~ (all_0_52_52 = all_0_116_116) | ~ (all_0_53_53 = all_0_117_117) | ~ (all_0_54_54 = all_0_118_118) | ~ (all_0_55_55 = all_0_119_119) | ~ (all_0_56_56 = all_0_120_120) | ~ (all_0_57_57 = all_0_121_121) | ~ (all_0_58_58 = all_0_122_122) | ~ (all_0_59_59 = all_0_123_123) % 11.14/3.12 | (149) ~ (e20 = e12) % 11.14/3.12 | (150) h4(all_0_124_124) = all_0_2_2 % 11.14/3.12 | (151) op2(e22, all_0_88_88) = all_0_40_40 % 11.14/3.12 | (152) op2(all_0_90_90, all_0_89_89) = all_0_79_79 % 11.14/3.12 | (153) all_0_126_126 = e11 | all_0_129_129 = e11 | all_0_132_132 = e11 % 11.14/3.12 | (154) op2(e22, e20) = all_0_117_117 % 11.14/3.12 | (155) h1(all_0_128_128) = all_0_72_72 % 11.14/3.12 | (156) ~ (all_0_129_129 = all_0_131_131) % 11.14/3.12 | (157) h3(all_0_124_124) = all_0_25_25 % 11.14/3.12 | (158) all_0_132_132 = e13 | all_0_133_133 = e13 | all_0_134_134 = e13 % 11.14/3.12 | (159) h1(e12) = all_0_123_123 % 11.14/3.12 | (160) op2(e23, e22) = all_0_113_113 % 11.14/3.12 | (161) op1(e12, e12) = all_0_127_127 % 11.14/3.12 | (162) op2(e20, e21) = e20 % 11.14/3.12 | (163) op2(all_0_121_121, all_0_121_121) = all_0_86_86 % 11.14/3.12 | (164) h1(e10) = all_0_90_90 % 11.14/3.12 | (165) ~ (e23 = e22) % 11.14/3.12 | (166) ~ (all_0_134_134 = e10) % 11.14/3.12 | (167) all_0_129_129 = e13 | all_0_130_130 = e13 | all_0_131_131 = e13 % 11.14/3.12 | (168) all_0_128_128 = e11 | all_0_131_131 = e11 | all_0_134_134 = e11 % 11.14/3.12 | (169) all_0_114_114 = e23 | all_0_114_114 = e22 % 11.14/3.12 | (170) (all_0_113_113 = e23 & all_0_123_123 = e22) | (all_0_113_113 = e23 & ~ (all_0_119_119 = e21)) | (all_0_115_115 = e22 & all_0_123_123 = e23) | (all_0_116_116 = e21 & ~ (all_0_123_123 = e21)) | (all_0_116_116 = e20 & all_0_120_120 = e21 & ~ (all_0_117_117 = e22)) | (all_0_117_117 = e22 & ~ (all_0_114_114 = e23) & ~ (all_0_116_116 = e20)) | (all_0_118_118 = e21 & all_0_123_123 = e23) | (all_0_120_120 = e21 & ~ (all_0_114_114 = e23)) % 11.14/3.12 | (171) ~ (all_0_126_126 = all_0_129_129) % 11.14/3.12 | (172) h3(all_0_131_131) = all_0_41_41 % 11.14/3.12 | (173) ~ (all_0_116_116 = all_0_122_122) % 11.14/3.12 | (174) op2(e23, e20) = all_0_114_114 % 11.14/3.12 | (175) ~ (e22 = e10) % 11.14/3.12 | (176) ~ (all_0_130_130 = all_0_133_133) % 11.14/3.12 | (177) all_0_122_122 = e23 | all_0_122_122 = e22 | all_0_122_122 = e21 % 11.14/3.12 | (178) op1(e13, all_0_124_124) = all_0_102_102 % 11.14/3.12 | (179) ~ (all_0_118_118 = e20) % 11.14/3.12 | (180) all_0_113_113 = e22 | all_0_116_116 = e22 | all_0_122_122 = e22 % 11.14/3.12 | (181) ~ (all_0_114_114 = e21) % 11.14/3.12 | (182) ~ (all_0_115_115 = e20) % 11.14/3.12 | (183) op2(e20, e20) = all_0_123_123 % 11.14/3.12 | (184) ~ (all_0_122_122 = all_0_123_123) % 11.14/3.12 | (185) ~ (all_0_126_126 = e10) % 11.14/3.12 | (186) h3(e13) = all_0_87_87 % 11.14/3.12 | (187) h2(e12) = e22 % 11.14/3.12 | (188) ~ (all_0_117_117 = all_0_123_123) % 11.14/3.12 | (189) ~ (all_0_117_117 = e23) % 11.14/3.12 | (190) ~ (all_0_122_122 = e20) % 11.14/3.12 | (191) ~ (all_0_125_125 = all_0_134_134) % 11.14/3.12 | (192) ~ (all_0_124_124 = e10) % 11.14/3.12 | (193) h2(all_0_126_126) = all_0_51_51 % 11.14/3.12 | (194) op1(e11, e11) = e12 % 11.14/3.12 | (195) all_0_121_121 = e21 | all_0_122_122 = e21 | all_0_123_123 = e21 % 11.14/3.12 | (196) ~ (all_0_126_126 = all_0_132_132) % 11.14/3.12 | (197) all_0_113_113 = e23 | all_0_113_113 = e22 % 11.14/3.12 | (198) all_0_124_124 = e13 | all_0_124_124 = e12 % 11.14/3.12 | (199) op2(e22, all_0_116_116) = all_0_94_94 % 11.14/3.12 | (200) all_0_121_121 = e23 | all_0_122_122 = e23 | all_0_123_123 = e23 % 11.14/3.12 | (201) ~ (all_0_23_23 = all_0_88_88) | ~ (all_0_24_24 = all_0_25_25) | ~ (all_0_26_26 = e22) | ~ (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_87_87) | ~ (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_88_88) | ~ (all_0_47_47 = all_0_48_48) | ( ~ (all_0_87_87 = e23) & ~ (all_0_88_88 = e23)) | ( ~ (all_0_87_87 = e21) & ~ (all_0_88_88 = e21) & ~ (all_0_116_116 = e21)) | ( ~ (all_0_87_87 = e20) & ~ (all_0_88_88 = e20) & ~ (all_0_116_116 = e20)) % 11.14/3.12 | (202) h3(all_0_134_134) = all_0_48_48 % 11.14/3.12 | (203) ~ (e23 = e12) % 11.14/3.12 | (204) all_0_115_115 = e22 | all_0_116_116 = e22 | all_0_117_117 = e22 % 11.14/3.12 | (205) h4(all_0_130_130) = all_0_13_13 % 11.14/3.12 | (206) ~ (all_0_113_113 = all_0_114_114) % 11.14/3.12 | (207) h4(all_0_133_133) = all_0_19_19 % 11.14/3.12 | (208) op1(e12, e10) = all_0_128_128 % 11.14/3.12 | (209) ~ (all_0_121_121 = all_0_123_123) % 11.14/3.12 | (210) h3(e12) = all_0_116_116 % 11.14/3.12 | (211) ~ (e23 = e20) % 11.14/3.12 | (212) h2(e11) = e21 % 11.14/3.12 | (213) ~ (e22 = e20) % 11.14/3.12 | (214) all_0_118_118 = e23 | all_0_119_119 = e23 | all_0_120_120 = e23 % 11.14/3.12 | (215) op2(all_0_89_89, all_0_90_90) = all_0_64_64 % 11.14/3.12 | (216) ~ (all_0_129_129 = e10) % 11.14/3.12 | (217) ~ (all_0_126_126 = all_0_127_127) % 11.14/3.12 | (218) all_0_129_129 = e13 | all_0_129_129 = e11 % 11.14/3.12 | (219) ~ (all_0_113_113 = e21) % 11.14/3.12 | (220) op2(all_0_121_121, all_0_86_86) = all_0_4_4 % 11.14/3.12 | (221) op2(e21, all_0_118_118) = all_0_96_96 % 11.14/3.12 | (222) ~ (all_0_126_126 = e13) % 11.14/3.12 | (223) ~ (e11 = e10) % 11.14/3.12 | (224) all_0_126_126 = e11 | all_0_127_127 = e11 | all_0_128_128 = e11 % 11.14/3.12 | (225) op2(e21, e22) = all_0_119_119 % 11.14/3.12 | (226) all_0_113_113 = e23 | all_0_114_114 = e23 % 11.14/3.12 | (227) all_0_115_115 = e21 | all_0_118_118 = e21 | all_0_121_121 = e21 % 11.14/3.12 | (228) h1(all_0_131_131) = all_0_78_78 % 11.14/3.12 | (229) op1(e13, e12) = all_0_124_124 % 11.14/3.12 | (230) ~ (e21 = e12) % 11.14/3.12 | (231) all_0_117_117 = e20 | all_0_120_120 = e20 % 11.14/3.12 | (232) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h1(v2) = v1) | ~ (h1(v2) = v0)) % 11.14/3.12 | (233) op2(e23, all_0_114_114) = all_0_92_92 % 11.14/3.12 | (234) all_0_127_127 = e10 | all_0_128_128 = e10 % 11.14/3.12 | (235) all_0_129_129 = e11 | all_0_130_130 = e11 | all_0_131_131 = e11 % 11.14/3.12 | (236) ~ (all_0_114_114 = e20) % 11.14/3.12 | (237) h4(e11) = e23 % 11.14/3.12 | (238) ~ (all_0_132_132 = all_0_133_133) % 11.14/3.12 | (239) all_0_124_124 = e13 | all_0_125_125 = e13 % 11.14/3.12 | (240) h3(all_0_133_133) = all_0_45_45 % 11.14/3.12 | (241) ~ (all_0_113_113 = e20) % 11.14/3.12 | (242) op2(all_0_89_89, e20) = all_0_63_63 % 11.14/3.12 | (243) op2(e20, all_0_122_122) = all_0_100_100 % 11.14/3.12 | (244) h4(e13) = all_0_121_121 % 11.14/3.12 | (245) all_0_131_131 = e13 | all_0_131_131 = e11 | all_0_131_131 = e10 % 11.14/3.12 | (246) op2(e22, all_0_116_116) = all_0_38_38 % 11.14/3.12 | (247) ~ (e22 = e11) % 11.14/3.12 | (248) ~ (e20 = e10) % 11.14/3.12 | (249) op2(all_0_89_89, all_0_89_89) = all_0_60_60 % 11.14/3.12 | (250) op2(e22, all_0_87_87) = all_0_36_36 % 11.14/3.12 | (251) h2(all_0_132_132) = all_0_57_57 % 11.14/3.12 | (252) op2(all_0_116_116, all_0_87_87) = all_0_29_29 % 11.14/3.12 | (253) h2(all_0_124_124) = all_0_49_49 % 11.14/3.12 | (254) ~ (all_0_124_124 = all_0_133_133) % 11.14/3.13 | (255) ~ (all_0_118_118 = e22) % 11.14/3.13 | (256) op1(e10, e13) = all_0_132_132 % 11.14/3.13 | (257) h1(all_0_125_125) = all_0_65_65 % 11.14/3.13 | (258) h3(all_0_125_125) = all_0_28_28 % 11.14/3.13 | (259) ~ (all_0_113_113 = all_0_116_116) % 11.14/3.13 | (260) op2(all_0_86_86, all_0_86_86) = all_0_21_21 % 11.14/3.13 | (261) ~ (all_0_130_130 = e12) % 11.14/3.13 | (262) op2(e21, all_0_119_119) = all_0_97_97 % 11.14/3.13 | (263) ~ (all_0_115_115 = all_0_117_117) % 11.14/3.13 | (264) ~ (all_0_118_118 = all_0_119_119) % 11.14/3.13 | (265) op2(e20, all_0_86_86) = all_0_9_9 % 11.14/3.13 | (266) h1(all_0_124_124) = all_0_62_62 % 11.14/3.13 | (267) op1(e10, e10) = all_0_134_134 % 11.14/3.13 | (268) (all_0_124_124 = e13 & all_0_134_134 = e12) | (all_0_124_124 = e13 & ~ (all_0_130_130 = e11)) | (all_0_126_126 = e12 & all_0_134_134 = e13) | (all_0_127_127 = e11 & ~ (all_0_134_134 = e11)) | (all_0_127_127 = e10 & all_0_131_131 = e11 & ~ (all_0_128_128 = e12)) | (all_0_128_128 = e12 & ~ (all_0_125_125 = e13) & ~ (all_0_127_127 = e10)) | (all_0_129_129 = e11 & all_0_134_134 = e13) | (all_0_131_131 = e11 & ~ (all_0_125_125 = e13)) % 11.14/3.13 | (269) ~ (all_0_129_129 = e12) % 11.14/3.13 | (270) all_0_114_114 = e22 | all_0_117_117 = e22 | all_0_123_123 = e22 % 11.14/3.13 | (271) h4(all_0_125_125) = all_0_5_5 % 11.14/3.13 | (272) op2(e23, all_0_86_86) = all_0_14_14 % 11.14/3.13 | (273) op2(all_0_123_123, all_0_89_89) = all_0_66_66 % 11.14/3.13 | (274) op1(e13, e13) = e10 % 11.14/3.13 | (275) ~ (all_0_133_133 = e10) % 11.63/3.13 | (276) ~ (e13 = e12) % 11.63/3.13 | (277) h3(all_0_132_132) = all_0_43_43 % 11.63/3.13 | (278) op2(all_0_123_123, all_0_90_90) = all_0_71_71 % 11.63/3.13 | (279) op1(e10, all_0_134_134) = all_0_112_112 % 11.63/3.13 | (280) h2(e10) = e20 % 11.63/3.13 | (281) all_0_127_127 = e11 | all_0_130_130 = e11 | all_0_133_133 = e11 % 11.63/3.13 | (282) ~ (e22 = e21) % 11.63/3.13 | (283) h4(all_0_129_129) = all_0_12_12 % 11.63/3.13 | (284) op2(all_0_86_86, all_0_121_121) = all_0_16_16 % 11.63/3.13 | (285) h1(e13) = all_0_89_89 % 11.63/3.13 | (286) all_0_115_115 = e21 | all_0_116_116 = e21 | all_0_117_117 = e21 % 11.63/3.13 | (287) op2(all_0_88_88, all_0_116_116) = all_0_44_44 % 11.63/3.13 | (288) all_0_132_132 = e13 | all_0_132_132 = e12 | all_0_132_132 = e11 % 11.63/3.13 | (289) all_0_129_129 = e13 | all_0_132_132 = e13 % 11.63/3.13 | (290) ~ (all_0_119_119 = all_0_120_120) % 11.63/3.13 | (291) op2(e21, e23) = all_0_118_118 % 11.63/3.13 | (292) op2(e20, e22) = all_0_122_122 % 11.63/3.13 | (293) ~ (all_0_0_0 = all_0_86_86) | ~ (all_0_1_1 = all_0_2_2) | ~ (all_0_3_3 = e23) | ~ (all_0_4_4 = all_0_5_5) | ~ (all_0_6_6 = all_0_7_7) | ~ (all_0_8_8 = all_0_123_123) | ~ (all_0_9_9 = all_0_10_10) | ~ (all_0_11_11 = all_0_12_12) | ~ (all_0_13_13 = all_0_114_114) | ~ (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_86_86) | ~ (all_0_21_21 = all_0_22_22) | ( ~ (all_0_86_86 = e22) & ~ (all_0_121_121 = e22)) | ( ~ (all_0_86_86 = e21) & ~ (all_0_121_121 = e21)) % 11.63/3.13 | (294) op1(e11, e12) = all_0_130_130 % 11.63/3.13 | (295) op2(e20, all_0_90_90) = all_0_77_77 % 11.63/3.13 | (296) ~ (all_0_133_133 = all_0_134_134) % 11.63/3.13 | (297) op1(e12, all_0_127_127) = all_0_105_105 % 11.63/3.13 | (298) ~ (e22 = e12) % 11.63/3.13 | (299) ~ (e20 = e13) % 11.63/3.13 | (300) op1(e12, e11) = e13 % 11.63/3.13 | (301) h2(all_0_129_129) = all_0_54_54 % 11.63/3.13 | (302) h2(all_0_133_133) = all_0_58_58 % 11.63/3.13 | (303) op2(all_0_87_87, all_0_87_87) = all_0_88_88 % 11.63/3.13 | (304) ~ (all_0_113_113 = all_0_122_122) % 11.63/3.13 | (305) ~ (all_0_128_128 = all_0_131_131) % 11.63/3.13 | (306) ~ (e23 = e11) % 11.63/3.13 | (307) h4(e12) = e20 % 11.63/3.13 | (308) ~ (all_0_130_130 = all_0_131_131) % 11.63/3.13 | (309) ~ (all_0_123_123 = e20) % 11.63/3.13 | (310) op1(e11, e10) = all_0_131_131 % 11.63/3.13 | (311) all_0_130_130 = e13 | all_0_130_130 = e11 | all_0_130_130 = e10 % 11.63/3.13 | (312) op1(e12, e13) = all_0_126_126 % 11.63/3.13 | (313) op2(e20, e23) = all_0_121_121 % 11.63/3.13 | (314) ~ (all_0_60_60 = all_0_90_90) | ~ (all_0_61_61 = all_0_62_62) | ~ (all_0_63_63 = e20) | ~ (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_89_89) | ~ (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_90_90) | ~ (all_0_84_84 = all_0_85_85) | ( ~ (all_0_89_89 = e23) & ~ (all_0_90_90 = e23) & ~ (all_0_123_123 = e23)) | ( ~ (all_0_89_89 = e22) & ~ (all_0_90_90 = e22) & ~ (all_0_123_123 = e22)) | ( ~ (all_0_89_89 = e21) & ~ (all_0_90_90 = e21) & ~ (all_0_123_123 = e21)) % 11.63/3.13 | (315) op2(all_0_88_88, all_0_88_88) = all_0_47_47 % 11.63/3.13 | (316) ~ (all_0_116_116 = e23) % 11.63/3.13 | (317) op1(e12, all_0_126_126) = all_0_104_104 % 11.63/3.13 | (318) op2(all_0_87_87, all_0_88_88) = all_0_27_27 % 11.63/3.13 | (319) op2(all_0_89_89, all_0_123_123) = all_0_61_61 % 11.63/3.13 | (320) op1(e10, e12) = all_0_133_133 % 11.63/3.13 | (321) all_0_127_127 = e12 | all_0_127_127 = e11 | all_0_127_127 = e10 % 11.63/3.13 | (322) h2(all_0_134_134) = all_0_59_59 % 11.63/3.13 | (323) op2(all_0_116_116, e22) = all_0_33_33 % 11.63/3.13 | (324) op2(e20, all_0_89_89) = all_0_73_73 % 11.63/3.13 | (325) h1(all_0_127_127) = all_0_69_69 % 11.63/3.13 | (326) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op2(v3, v2) = v1) | ~ (op2(v3, v2) = v0)) % 11.63/3.13 | (327) h4(all_0_126_126) = all_0_7_7 % 11.63/3.13 | (328) op1(e11, all_0_131_131) = all_0_109_109 % 11.63/3.13 | (329) all_0_126_126 = e12 | all_0_126_126 = e11 % 11.63/3.13 | (330) op2(all_0_87_87, e22) = all_0_26_26 % 11.63/3.13 | (331) all_0_118_118 = e23 | all_0_118_118 = e21 % 11.63/3.13 | (332) op2(e22, e22) = all_0_116_116 % 11.63/3.13 | (333) all_0_132_132 = e11 | all_0_133_133 = e11 | all_0_134_134 = e11 % 11.63/3.13 | (334) all_0_113_113 = e23 | all_0_119_119 = e23 | all_0_122_122 = e23 % 11.63/3.13 | (335) all_0_125_125 = e13 | all_0_131_131 = e13 | all_0_134_134 = e13 % 11.63/3.13 | (336) ~ (all_0_125_125 = e10) % 11.63/3.13 | (337) op1(e12, all_0_128_128) = all_0_106_106 % 11.63/3.13 | (338) ~ (all_0_116_116 = all_0_119_119) % 11.63/3.13 | (339) op2(e22, all_0_115_115) = all_0_93_93 % 11.63/3.13 | (340) h3(all_0_128_128) = all_0_35_35 % 11.63/3.13 | (341) ~ (all_0_129_129 = all_0_130_130) % 11.63/3.13 | (342) op2(all_0_116_116, all_0_116_116) = all_0_31_31 % 11.63/3.13 | (343) op2(e20, all_0_123_123) = all_0_75_75 % 11.63/3.13 | (344) h3(all_0_129_129) = all_0_37_37 % 11.63/3.13 | (345) all_0_116_116 = e22 | all_0_116_116 = e21 | all_0_116_116 = e20 % 11.63/3.13 | (346) op2(all_0_123_123, all_0_123_123) = all_0_68_68 % 11.63/3.13 | (347) ~ (e13 = e11) % 11.63/3.13 | (348) all_0_123_123 = e23 | all_0_123_123 = e22 | all_0_123_123 = e21 % 11.63/3.14 | (349) op1(e11, all_0_130_130) = all_0_108_108 % 11.63/3.14 | (350) op2(e22, e21) = e23 % 11.63/3.14 | % 11.63/3.14 +-Applying beta-rule and splitting (80), into two cases. % 11.63/3.14 |-Branch one: % 11.63/3.14 | (351) all_0_115_115 = e22 % 11.63/3.14 | % 11.63/3.14 | Equations (351) can reduce 44 to: % 11.63/3.14 | (352) ~ (all_0_116_116 = e22) % 11.63/3.14 | % 11.63/3.14 | Simplifying 352 yields: % 11.63/3.14 | (353) ~ (all_0_116_116 = e22) % 11.63/3.14 | % 11.63/3.14 | Equations (351) can reduce 263 to: % 11.63/3.14 | (354) ~ (all_0_117_117 = e22) % 11.63/3.14 | % 11.63/3.14 | Simplifying 354 yields: % 11.63/3.14 | (355) ~ (all_0_117_117 = e22) % 11.63/3.14 | % 11.63/3.14 | Equations (351) can reduce 52 to: % 11.63/3.14 | (356) ~ (all_0_118_118 = e22) % 11.63/3.14 | % 11.63/3.14 | Simplifying 356 yields: % 11.63/3.14 | (255) ~ (all_0_118_118 = e22) % 11.63/3.14 | % 11.63/3.14 +-Applying beta-rule and splitting (169), into two cases. % 11.63/3.14 |-Branch one: % 11.63/3.14 | (358) all_0_114_114 = e22 % 11.63/3.14 | % 11.63/3.14 | Equations (358) can reduce 206 to: % 11.63/3.14 | (359) ~ (all_0_113_113 = e22) % 11.63/3.14 | % 11.63/3.14 | Equations (358) can reduce 5 to: % 11.63/3.14 | (354) ~ (all_0_117_117 = e22) % 11.63/3.14 | % 11.63/3.14 | Simplifying 354 yields: % 11.63/3.14 | (355) ~ (all_0_117_117 = e22) % 11.63/3.14 | % 11.63/3.14 | Equations (358) can reduce 120 to: % 11.63/3.14 | (362) ~ (all_0_120_120 = e22) % 11.63/3.14 | % 11.63/3.14 | Simplifying 362 yields: % 11.63/3.14 | (131) ~ (all_0_120_120 = e22) % 11.63/3.14 | % 11.63/3.14 | Equations (358) can reduce 181 to: % 11.63/3.14 | (282) ~ (e22 = e21) % 11.63/3.14 | % 11.63/3.14 | From (358) and (233) follows: % 11.63/3.14 | (365) op2(e23, e22) = all_0_92_92 % 11.63/3.14 | % 11.63/3.14 +-Applying beta-rule and splitting (197), into two cases. % 11.63/3.14 |-Branch one: % 11.63/3.14 | (366) all_0_113_113 = e22 % 11.63/3.14 | % 11.63/3.14 | Equations (366) can reduce 359 to: % 11.63/3.14 | (367) $false % 11.63/3.14 | % 11.63/3.14 |-The branch is then unsatisfiable % 11.63/3.14 |-Branch two: % 11.63/3.14 | (359) ~ (all_0_113_113 = e22) % 11.63/3.14 | (369) all_0_113_113 = e23 % 11.63/3.14 | % 11.63/3.14 | Equations (369) can reduce 259 to: % 11.63/3.14 | (370) ~ (all_0_116_116 = e23) % 11.63/3.14 | % 11.63/3.14 | Simplifying 370 yields: % 11.63/3.14 | (316) ~ (all_0_116_116 = e23) % 11.63/3.14 | % 11.63/3.14 | Equations (369) can reduce 35 to: % 11.63/3.14 | (372) ~ (all_0_119_119 = e23) % 11.63/3.14 | % 11.63/3.14 | Simplifying 372 yields: % 11.63/3.14 | (373) ~ (all_0_119_119 = e23) % 11.63/3.14 | % 11.63/3.14 | Equations (369) can reduce 359 to: % 11.63/3.14 | (165) ~ (e23 = e22) % 11.63/3.14 | % 11.63/3.14 | From (369) and (160) follows: % 11.63/3.14 | (375) op2(e23, e22) = e23 % 11.63/3.14 | % 11.63/3.14 +-Applying beta-rule and splitting (180), into two cases. % 11.63/3.14 |-Branch one: % 11.63/3.14 | (366) all_0_113_113 = e22 % 11.63/3.14 | % 11.63/3.14 | Combining equations (366,369) yields a new equation: % 11.63/3.14 | (377) e23 = e22 % 11.63/3.14 | % 11.63/3.14 | Equations (377) can reduce 165 to: % 11.63/3.14 | (367) $false % 11.63/3.14 | % 11.63/3.14 |-The branch is then unsatisfiable % 11.63/3.14 |-Branch two: % 11.63/3.14 | (359) ~ (all_0_113_113 = e22) % 11.63/3.14 | (380) all_0_116_116 = e22 | all_0_122_122 = e22 % 11.63/3.14 | % 11.63/3.14 +-Applying beta-rule and splitting (380), into two cases. % 11.63/3.14 |-Branch one: % 11.63/3.14 | (381) all_0_116_116 = e22 % 11.63/3.14 | % 11.63/3.14 | Equations (381) can reduce 353 to: % 11.63/3.14 | (367) $false % 11.63/3.14 | % 11.63/3.14 |-The branch is then unsatisfiable % 11.63/3.14 |-Branch two: % 11.63/3.14 | (353) ~ (all_0_116_116 = e22) % 11.63/3.14 | (384) all_0_122_122 = e22 % 11.63/3.14 | % 11.63/3.14 | Equations (384) can reduce 173 to: % 11.63/3.14 | (353) ~ (all_0_116_116 = e22) % 11.63/3.14 | % 11.63/3.14 | Equations (384) can reduce 54 to: % 11.63/3.14 | (133) ~ (all_0_119_119 = e22) % 11.63/3.14 | % 11.63/3.14 | Instantiating formula (326) with e23, e22, e23, all_0_92_92 and discharging atoms op2(e23, e22) = all_0_92_92, op2(e23, e22) = e23, yields: % 11.63/3.14 | (387) all_0_92_92 = e23 % 11.63/3.14 | % 11.63/3.14 +-Applying beta-rule and splitting (42), into two cases. % 11.63/3.14 |-Branch one: % 11.63/3.14 | (388) all_0_116_116 = e20 % 11.63/3.14 | % 11.63/3.14 | Equations (388) can reduce 338 to: % 11.63/3.14 | (389) ~ (all_0_119_119 = e20) % 11.63/3.14 | % 11.63/3.14 | Simplifying 389 yields: % 11.63/3.14 | (390) ~ (all_0_119_119 = e20) % 11.63/3.14 | % 11.63/3.14 | Equations (388) can reduce 316 to: % 11.63/3.14 | (391) ~ (e23 = e20) % 11.63/3.14 | % 11.63/3.14 | Simplifying 391 yields: % 11.63/3.14 | (211) ~ (e23 = e20) % 11.63/3.14 | % 11.63/3.14 +-Applying beta-rule and splitting (33), into two cases. % 11.63/3.14 |-Branch one: % 11.63/3.14 | (393) all_0_119_119 = e20 % 11.63/3.14 | % 11.63/3.14 | Equations (393) can reduce 390 to: % 11.63/3.14 | (367) $false % 11.63/3.14 | % 11.63/3.14 |-The branch is then unsatisfiable % 11.63/3.14 |-Branch two: % 11.63/3.14 | (390) ~ (all_0_119_119 = e20) % 11.63/3.14 | (396) all_0_120_120 = e20 % 11.63/3.14 | % 11.63/3.14 | Equations (396) can reduce 51 to: % 11.63/3.14 | (397) ~ (all_0_117_117 = e20) % 11.63/3.14 | % 11.63/3.14 | Equations (396) can reduce 131 to: % 11.63/3.14 | (398) ~ (e22 = e20) % 11.63/3.14 | % 11.63/3.14 | Simplifying 398 yields: % 11.63/3.14 | (213) ~ (e22 = e20) % 11.63/3.14 | % 11.63/3.14 +-Applying beta-rule and splitting (46), into two cases. % 11.63/3.14 |-Branch one: % 11.63/3.14 | (400) all_0_116_116 = e21 % 11.63/3.14 | % 11.63/3.14 | Combining equations (388,400) yields a new equation: % 11.63/3.14 | (401) e21 = e20 % 11.63/3.14 | % 11.63/3.14 | Equations (401) can reduce 140 to: % 11.63/3.14 | (367) $false % 11.63/3.14 | % 11.63/3.14 |-The branch is then unsatisfiable % 11.63/3.14 |-Branch two: % 11.63/3.14 | (403) ~ (all_0_116_116 = e21) % 11.63/3.14 | (404) all_0_119_119 = e21 | all_0_122_122 = e21 % 11.63/3.14 | % 11.63/3.14 +-Applying beta-rule and splitting (404), into two cases. % 11.63/3.14 |-Branch one: % 11.63/3.14 | (405) all_0_119_119 = e21 % 11.63/3.14 | % 11.63/3.14 | Equations (405) can reduce 373 to: % 11.63/3.14 | (406) ~ (e23 = e21) % 11.63/3.14 | % 11.63/3.14 | Simplifying 406 yields: % 11.63/3.14 | (114) ~ (e23 = e21) % 11.63/3.14 | % 11.63/3.14 +-Applying beta-rule and splitting (214), into two cases. % 11.63/3.14 |-Branch one: % 11.63/3.14 | (408) all_0_118_118 = e23 % 11.63/3.14 | % 11.63/3.15 | Equations (408) can reduce 10 to: % 11.63/3.15 | (409) ~ (all_0_121_121 = e23) % 11.63/3.15 | % 11.63/3.15 | Simplifying 409 yields: % 11.63/3.15 | (410) ~ (all_0_121_121 = e23) % 11.63/3.15 | % 11.63/3.15 | Equations (408) can reduce 255 to: % 11.63/3.15 | (165) ~ (e23 = e22) % 11.63/3.15 | % 11.63/3.15 +-Applying beta-rule and splitting (200), into two cases. % 11.63/3.15 |-Branch one: % 11.63/3.15 | (412) all_0_121_121 = e23 % 11.63/3.15 | % 11.63/3.15 | Equations (412) can reduce 410 to: % 11.63/3.15 | (367) $false % 11.63/3.15 | % 11.63/3.15 |-The branch is then unsatisfiable % 11.63/3.15 |-Branch two: % 11.63/3.15 | (410) ~ (all_0_121_121 = e23) % 11.63/3.15 | (415) all_0_122_122 = e23 | all_0_123_123 = e23 % 11.63/3.15 | % 11.63/3.15 +-Applying beta-rule and splitting (415), into two cases. % 11.63/3.15 |-Branch one: % 11.63/3.15 | (416) all_0_122_122 = e23 % 11.63/3.15 | % 11.63/3.15 | Combining equations (384,416) yields a new equation: % 11.63/3.15 | (377) e23 = e22 % 11.63/3.15 | % 11.63/3.15 | Equations (377) can reduce 165 to: % 11.63/3.15 | (367) $false % 11.63/3.15 | % 11.63/3.15 |-The branch is then unsatisfiable % 11.63/3.15 |-Branch two: % 11.63/3.15 | (419) ~ (all_0_122_122 = e23) % 11.63/3.15 | (420) all_0_123_123 = e23 % 11.63/3.15 | % 11.63/3.15 | Equations (420) can reduce 188 to: % 11.63/3.15 | (189) ~ (all_0_117_117 = e23) % 11.63/3.15 | % 11.63/3.15 +-Applying beta-rule and splitting (105), into two cases. % 11.63/3.15 |-Branch one: % 11.63/3.15 | (422) all_0_117_117 = e22 % 11.63/3.15 | % 11.63/3.15 | Equations (422) can reduce 355 to: % 11.63/3.15 | (367) $false % 11.63/3.15 | % 11.63/3.15 |-The branch is then unsatisfiable % 11.63/3.15 |-Branch two: % 11.63/3.15 | (355) ~ (all_0_117_117 = e22) % 11.63/3.15 | (425) all_0_117_117 = e21 | all_0_117_117 = e20 % 11.63/3.15 | % 11.63/3.15 +-Applying beta-rule and splitting (425), into two cases. % 11.63/3.15 |-Branch one: % 11.63/3.15 | (426) all_0_117_117 = e21 % 11.63/3.15 | % 11.63/3.15 | Equations (426) can reduce 189 to: % 11.63/3.15 | (406) ~ (e23 = e21) % 11.63/3.15 | % 11.63/3.15 | Simplifying 406 yields: % 11.63/3.15 | (114) ~ (e23 = e21) % 11.63/3.15 | % 11.63/3.15 | Equations (426) can reduce 355 to: % 11.63/3.15 | (429) ~ (e22 = e21) % 11.63/3.15 | % 11.63/3.15 | Simplifying 429 yields: % 11.63/3.15 | (282) ~ (e22 = e21) % 11.63/3.15 | % 11.63/3.15 +-Applying beta-rule and splitting (32), into two cases. % 11.63/3.15 |-Branch one: % 11.63/3.15 | (431) (all_0_91_91 = e22 & all_0_92_92 = e20 & all_0_114_114 = e23 & ~ (all_0_115_115 = e22) & ~ (all_0_118_118 = e21)) | (all_0_93_93 = e23 & all_0_94_94 = e22 & all_0_95_95 = e20 & all_0_115_115 = e21 & ~ (all_0_113_113 = e23)) | (all_0_96_96 = e23 & all_0_97_97 = e22 & all_0_98_98 = e20 & all_0_119_119 = e21 & all_0_123_123 = e21) % 11.63/3.15 | % 11.63/3.15 +-Applying beta-rule and splitting (431), into two cases. % 11.63/3.15 |-Branch one: % 11.63/3.15 | (432) (all_0_91_91 = e22 & all_0_92_92 = e20 & all_0_114_114 = e23 & ~ (all_0_115_115 = e22) & ~ (all_0_118_118 = e21)) | (all_0_93_93 = e23 & all_0_94_94 = e22 & all_0_95_95 = e20 & all_0_115_115 = e21 & ~ (all_0_113_113 = e23)) % 11.63/3.15 | % 11.63/3.15 +-Applying beta-rule and splitting (432), into two cases. % 11.63/3.15 |-Branch one: % 11.63/3.15 | (433) all_0_91_91 = e22 & all_0_92_92 = e20 & all_0_114_114 = e23 & ~ (all_0_115_115 = e22) & ~ (all_0_118_118 = e21) % 11.63/3.15 | % 11.63/3.15 | Applying alpha-rule on (433) yields: % 11.63/3.15 | (434) all_0_114_114 = e23 % 11.63/3.15 | (435) ~ (all_0_115_115 = e22) % 11.63/3.15 | (436) ~ (all_0_118_118 = e21) % 11.63/3.15 | (437) all_0_92_92 = e20 % 11.63/3.15 | (438) all_0_91_91 = e22 % 11.63/3.15 | % 11.63/3.15 | Combining equations (437,387) yields a new equation: % 11.63/3.15 | (439) e23 = e20 % 11.63/3.15 | % 11.63/3.15 | Combining equations (358,434) yields a new equation: % 11.63/3.15 | (377) e23 = e22 % 11.63/3.15 | % 11.63/3.15 | Combining equations (377,439) yields a new equation: % 11.63/3.15 | (441) e22 = e20 % 11.63/3.15 | % 11.63/3.15 | Simplifying 441 yields: % 11.63/3.15 | (442) e22 = e20 % 11.63/3.15 | % 11.63/3.15 | Equations (442) can reduce 213 to: % 11.63/3.15 | (367) $false % 11.63/3.15 | % 11.63/3.15 |-The branch is then unsatisfiable % 11.63/3.15 |-Branch two: % 11.63/3.15 | (444) all_0_93_93 = e23 & all_0_94_94 = e22 & all_0_95_95 = e20 & all_0_115_115 = e21 & ~ (all_0_113_113 = e23) % 11.63/3.15 | % 11.63/3.15 | Applying alpha-rule on (444) yields: % 11.63/3.15 | (445) ~ (all_0_113_113 = e23) % 11.63/3.15 | (446) all_0_93_93 = e23 % 11.63/3.15 | (447) all_0_94_94 = e22 % 11.63/3.15 | (448) all_0_115_115 = e21 % 11.63/3.15 | (449) all_0_95_95 = e20 % 11.63/3.15 | % 11.63/3.15 | Combining equations (351,448) yields a new equation: % 11.63/3.15 | (450) e22 = e21 % 11.63/3.15 | % 11.63/3.15 | Simplifying 450 yields: % 11.63/3.15 | (451) e22 = e21 % 11.63/3.15 | % 11.63/3.15 | Equations (451) can reduce 282 to: % 11.63/3.15 | (367) $false % 11.63/3.15 | % 11.63/3.15 |-The branch is then unsatisfiable % 11.63/3.15 |-Branch two: % 11.63/3.15 | (453) all_0_96_96 = e23 & all_0_97_97 = e22 & all_0_98_98 = e20 & all_0_119_119 = e21 & all_0_123_123 = e21 % 11.63/3.15 | % 11.63/3.15 | Applying alpha-rule on (453) yields: % 11.63/3.15 | (454) all_0_123_123 = e21 % 11.63/3.15 | (455) all_0_98_98 = e20 % 11.63/3.15 | (456) all_0_96_96 = e23 % 11.63/3.15 | (457) all_0_97_97 = e22 % 11.63/3.15 | (405) all_0_119_119 = e21 % 11.63/3.15 | % 11.63/3.15 | Combining equations (420,454) yields a new equation: % 11.63/3.15 | (459) e23 = e21 % 11.63/3.15 | % 11.63/3.15 | Simplifying 459 yields: % 11.63/3.15 | (460) e23 = e21 % 11.63/3.15 | % 11.63/3.15 | Equations (460) can reduce 114 to: % 11.63/3.15 | (367) $false % 11.63/3.15 | % 11.63/3.15 |-The branch is then unsatisfiable % 11.63/3.15 |-Branch two: % 11.63/3.15 | (462) all_0_99_99 = e23 & all_0_100_100 = e22 & all_0_101_101 = e20 & all_0_123_123 = e21 & ~ (all_0_120_120 = e21) & ( ~ (all_0_117_117 = e22) | all_0_116_116 = e20) % 11.63/3.15 | % 11.63/3.15 | Applying alpha-rule on (462) yields: % 11.63/3.15 | (454) all_0_123_123 = e21 % 11.63/3.15 | (464) ~ (all_0_120_120 = e21) % 11.63/3.15 | (465) all_0_100_100 = e22 % 11.63/3.15 | (466) ~ (all_0_117_117 = e22) | all_0_116_116 = e20 % 11.63/3.15 | (467) all_0_101_101 = e20 % 11.63/3.15 | (468) all_0_99_99 = e23 % 11.63/3.15 | % 11.63/3.15 | Combining equations (454,420) yields a new equation: % 11.63/3.15 | (460) e23 = e21 % 11.63/3.15 | % 11.63/3.15 | Equations (460) can reduce 114 to: % 11.63/3.15 | (367) $false % 11.63/3.15 | % 11.63/3.15 |-The branch is then unsatisfiable % 11.63/3.15 |-Branch two: % 11.63/3.15 | (471) ~ (all_0_117_117 = e21) % 11.63/3.15 | (472) all_0_117_117 = e20 % 11.63/3.15 | % 11.63/3.15 | Equations (472) can reduce 397 to: % 11.63/3.15 | (367) $false % 11.63/3.15 | % 11.63/3.15 |-The branch is then unsatisfiable % 11.63/3.15 |-Branch two: % 11.63/3.15 | (474) ~ (all_0_118_118 = e23) % 11.63/3.15 | (475) all_0_119_119 = e23 | all_0_120_120 = e23 % 11.63/3.15 | % 11.63/3.15 +-Applying beta-rule and splitting (475), into two cases. % 11.63/3.15 |-Branch one: % 11.63/3.15 | (476) all_0_119_119 = e23 % 11.63/3.15 | % 11.63/3.15 | Combining equations (476,405) yields a new equation: % 11.63/3.15 | (459) e23 = e21 % 11.63/3.15 | % 11.63/3.15 | Simplifying 459 yields: % 11.63/3.15 | (460) e23 = e21 % 11.63/3.15 | % 11.63/3.15 | Equations (460) can reduce 114 to: % 11.63/3.15 | (367) $false % 11.63/3.15 | % 11.63/3.15 |-The branch is then unsatisfiable % 11.63/3.15 |-Branch two: % 11.63/3.15 | (373) ~ (all_0_119_119 = e23) % 11.63/3.15 | (481) all_0_120_120 = e23 % 11.63/3.15 | % 11.63/3.15 | Combining equations (396,481) yields a new equation: % 11.63/3.15 | (439) e23 = e20 % 11.63/3.15 | % 11.63/3.15 | Equations (439) can reduce 211 to: % 11.63/3.15 | (367) $false % 11.63/3.15 | % 11.63/3.15 |-The branch is then unsatisfiable % 11.63/3.15 |-Branch two: % 11.63/3.16 | (484) ~ (all_0_119_119 = e21) % 11.63/3.16 | (485) all_0_122_122 = e21 % 11.63/3.16 | % 11.63/3.16 | Combining equations (485,384) yields a new equation: % 11.63/3.16 | (451) e22 = e21 % 11.63/3.16 | % 11.63/3.16 | Equations (451) can reduce 282 to: % 11.63/3.16 | (367) $false % 11.63/3.16 | % 11.63/3.16 |-The branch is then unsatisfiable % 11.63/3.16 |-Branch two: % 11.63/3.16 | (488) ~ (all_0_116_116 = e20) % 11.63/3.16 | (472) all_0_117_117 = e20 % 11.63/3.16 | % 11.63/3.16 | Equations (472) can reduce 51 to: % 11.63/3.16 | (490) ~ (all_0_120_120 = e20) % 11.63/3.16 | % 11.63/3.16 | Simplifying 490 yields: % 11.63/3.16 | (491) ~ (all_0_120_120 = e20) % 11.63/3.16 | % 11.63/3.16 +-Applying beta-rule and splitting (33), into two cases. % 11.63/3.16 |-Branch one: % 11.63/3.16 | (393) all_0_119_119 = e20 % 11.63/3.16 | % 11.63/3.16 | Equations (393) can reduce 338 to: % 11.63/3.16 | (488) ~ (all_0_116_116 = e20) % 11.63/3.16 | % 11.63/3.16 | Equations (393) can reduce 290 to: % 11.63/3.16 | (490) ~ (all_0_120_120 = e20) % 11.63/3.16 | % 11.63/3.16 | Simplifying 490 yields: % 11.63/3.16 | (491) ~ (all_0_120_120 = e20) % 11.63/3.16 | % 11.63/3.16 | Equations (393) can reduce 133 to: % 11.63/3.16 | (398) ~ (e22 = e20) % 11.63/3.16 | % 11.63/3.16 | Simplifying 398 yields: % 11.63/3.16 | (213) ~ (e22 = e20) % 11.63/3.16 | % 11.63/3.16 +-Applying beta-rule and splitting (46), into two cases. % 11.63/3.16 |-Branch one: % 11.63/3.16 | (400) all_0_116_116 = e21 % 11.63/3.16 | % 11.63/3.16 | Equations (400) can reduce 353 to: % 11.63/3.16 | (429) ~ (e22 = e21) % 11.63/3.16 | % 11.63/3.16 | Simplifying 429 yields: % 11.63/3.16 | (282) ~ (e22 = e21) % 11.63/3.16 | % 11.63/3.16 | Equations (400) can reduce 488 to: % 11.63/3.16 | (140) ~ (e21 = e20) % 11.63/3.16 | % 11.63/3.16 +-Applying beta-rule and splitting (32), into two cases. % 11.63/3.16 |-Branch one: % 11.63/3.16 | (431) (all_0_91_91 = e22 & all_0_92_92 = e20 & all_0_114_114 = e23 & ~ (all_0_115_115 = e22) & ~ (all_0_118_118 = e21)) | (all_0_93_93 = e23 & all_0_94_94 = e22 & all_0_95_95 = e20 & all_0_115_115 = e21 & ~ (all_0_113_113 = e23)) | (all_0_96_96 = e23 & all_0_97_97 = e22 & all_0_98_98 = e20 & all_0_119_119 = e21 & all_0_123_123 = e21) % 11.63/3.16 | % 11.63/3.16 +-Applying beta-rule and splitting (431), into two cases. % 11.63/3.16 |-Branch one: % 11.63/3.16 | (432) (all_0_91_91 = e22 & all_0_92_92 = e20 & all_0_114_114 = e23 & ~ (all_0_115_115 = e22) & ~ (all_0_118_118 = e21)) | (all_0_93_93 = e23 & all_0_94_94 = e22 & all_0_95_95 = e20 & all_0_115_115 = e21 & ~ (all_0_113_113 = e23)) % 11.63/3.16 | % 11.63/3.16 +-Applying beta-rule and splitting (432), into two cases. % 11.63/3.16 |-Branch one: % 11.63/3.16 | (433) all_0_91_91 = e22 & all_0_92_92 = e20 & all_0_114_114 = e23 & ~ (all_0_115_115 = e22) & ~ (all_0_118_118 = e21) % 11.63/3.16 | % 11.63/3.16 | Applying alpha-rule on (433) yields: % 11.63/3.16 | (434) all_0_114_114 = e23 % 11.63/3.16 | (435) ~ (all_0_115_115 = e22) % 11.63/3.16 | (436) ~ (all_0_118_118 = e21) % 11.63/3.16 | (437) all_0_92_92 = e20 % 11.63/3.16 | (438) all_0_91_91 = e22 % 11.63/3.16 | % 11.63/3.16 | Combining equations (437,387) yields a new equation: % 11.63/3.16 | (439) e23 = e20 % 11.63/3.16 | % 11.63/3.16 | Combining equations (358,434) yields a new equation: % 11.63/3.16 | (377) e23 = e22 % 11.63/3.16 | % 11.63/3.16 | Combining equations (439,377) yields a new equation: % 11.63/3.16 | (442) e22 = e20 % 11.63/3.16 | % 11.63/3.16 | Equations (442) can reduce 213 to: % 11.63/3.16 | (367) $false % 11.63/3.16 | % 11.63/3.16 |-The branch is then unsatisfiable % 11.63/3.16 |-Branch two: % 11.63/3.16 | (444) all_0_93_93 = e23 & all_0_94_94 = e22 & all_0_95_95 = e20 & all_0_115_115 = e21 & ~ (all_0_113_113 = e23) % 11.63/3.16 | % 11.63/3.16 | Applying alpha-rule on (444) yields: % 11.63/3.16 | (445) ~ (all_0_113_113 = e23) % 11.63/3.16 | (446) all_0_93_93 = e23 % 11.63/3.16 | (447) all_0_94_94 = e22 % 11.63/3.16 | (448) all_0_115_115 = e21 % 11.63/3.16 | (449) all_0_95_95 = e20 % 11.63/3.16 | % 11.63/3.16 | Combining equations (351,448) yields a new equation: % 11.63/3.16 | (450) e22 = e21 % 11.63/3.16 | % 11.63/3.16 | Simplifying 450 yields: % 11.63/3.16 | (451) e22 = e21 % 11.63/3.16 | % 11.63/3.16 | Equations (451) can reduce 282 to: % 11.63/3.16 | (367) $false % 11.63/3.16 | % 11.63/3.16 |-The branch is then unsatisfiable % 11.63/3.16 |-Branch two: % 11.63/3.16 | (453) all_0_96_96 = e23 & all_0_97_97 = e22 & all_0_98_98 = e20 & all_0_119_119 = e21 & all_0_123_123 = e21 % 11.63/3.16 | % 11.63/3.16 | Applying alpha-rule on (453) yields: % 11.63/3.16 | (454) all_0_123_123 = e21 % 11.63/3.16 | (455) all_0_98_98 = e20 % 11.63/3.16 | (456) all_0_96_96 = e23 % 11.63/3.16 | (457) all_0_97_97 = e22 % 11.63/3.16 | (405) all_0_119_119 = e21 % 11.63/3.16 | % 11.63/3.16 | Combining equations (405,393) yields a new equation: % 11.63/3.16 | (529) e21 = e20 % 11.63/3.16 | % 11.63/3.16 | Simplifying 529 yields: % 11.63/3.16 | (401) e21 = e20 % 11.63/3.16 | % 11.63/3.16 | Equations (401) can reduce 140 to: % 11.63/3.16 | (367) $false % 11.63/3.16 | % 11.63/3.16 |-The branch is then unsatisfiable % 11.63/3.16 |-Branch two: % 11.63/3.16 | (462) all_0_99_99 = e23 & all_0_100_100 = e22 & all_0_101_101 = e20 & all_0_123_123 = e21 & ~ (all_0_120_120 = e21) & ( ~ (all_0_117_117 = e22) | all_0_116_116 = e20) % 11.63/3.16 | % 11.63/3.16 | Applying alpha-rule on (462) yields: % 11.63/3.16 | (454) all_0_123_123 = e21 % 11.63/3.16 | (464) ~ (all_0_120_120 = e21) % 11.63/3.16 | (465) all_0_100_100 = e22 % 11.63/3.16 | (466) ~ (all_0_117_117 = e22) | all_0_116_116 = e20 % 11.63/3.16 | (467) all_0_101_101 = e20 % 11.63/3.16 | (468) all_0_99_99 = e23 % 11.63/3.16 | % 11.63/3.16 | Equations (454) can reduce 43 to: % 11.63/3.16 | (464) ~ (all_0_120_120 = e21) % 11.63/3.16 | % 11.63/3.16 +-Applying beta-rule and splitting (139), into two cases. % 11.63/3.16 |-Branch one: % 11.63/3.16 | (540) all_0_120_120 = e21 % 11.63/3.16 | % 11.63/3.16 | Equations (540) can reduce 464 to: % 11.63/3.16 | (367) $false % 11.63/3.16 | % 11.63/3.16 |-The branch is then unsatisfiable % 11.63/3.16 |-Branch two: % 11.63/3.16 | (464) ~ (all_0_120_120 = e21) % 11.63/3.16 | (543) all_0_120_120 = e23 | all_0_120_120 = e20 % 11.63/3.16 | % 11.63/3.16 +-Applying beta-rule and splitting (543), into two cases. % 11.63/3.16 |-Branch one: % 11.63/3.16 | (481) all_0_120_120 = e23 % 11.63/3.16 | % 11.63/3.16 | Equations (481) can reduce 138 to: % 11.63/3.16 | (474) ~ (all_0_118_118 = e23) % 11.63/3.16 | % 11.63/3.16 +-Applying beta-rule and splitting (99), into two cases. % 11.63/3.16 |-Branch one: % 11.63/3.16 | (408) all_0_118_118 = e23 % 11.63/3.16 | % 11.63/3.16 | Equations (408) can reduce 474 to: % 11.63/3.16 | (367) $false % 11.63/3.16 | % 11.63/3.16 |-The branch is then unsatisfiable % 11.63/3.16 |-Branch two: % 11.63/3.16 | (474) ~ (all_0_118_118 = e23) % 11.63/3.16 | (412) all_0_121_121 = e23 % 11.63/3.16 | % 11.63/3.16 | Equations (412) can reduce 10 to: % 11.63/3.16 | (474) ~ (all_0_118_118 = e23) % 11.63/3.16 | % 11.63/3.16 +-Applying beta-rule and splitting (331), into two cases. % 11.63/3.16 |-Branch one: % 11.63/3.16 | (551) all_0_118_118 = e21 % 11.63/3.16 | % 11.63/3.16 +-Applying beta-rule and splitting (218), into two cases. % 11.63/3.16 |-Branch one: % 11.63/3.16 | (552) all_0_129_129 = e11 % 11.63/3.16 | % 11.63/3.16 | Equations (552) can reduce 171 to: % 11.63/3.16 | (553) ~ (all_0_126_126 = e11) % 11.63/3.16 | % 11.63/3.16 | Equations (552) can reduce 341 to: % 11.63/3.16 | (554) ~ (all_0_130_130 = e11) % 11.63/3.16 | % 11.63/3.16 | Simplifying 554 yields: % 11.63/3.16 | (555) ~ (all_0_130_130 = e11) % 11.63/3.16 | % 11.63/3.16 | From (552) and (301) follows: % 11.63/3.16 | (556) h2(e11) = all_0_54_54 % 11.63/3.16 | % 11.63/3.16 +-Applying beta-rule and splitting (329), into two cases. % 11.63/3.16 |-Branch one: % 11.63/3.16 | (557) all_0_126_126 = e11 % 11.63/3.16 | % 11.63/3.17 | Equations (557) can reduce 553 to: % 11.63/3.17 | (367) $false % 11.63/3.17 | % 11.63/3.17 |-The branch is then unsatisfiable % 11.63/3.17 |-Branch two: % 11.63/3.17 | (553) ~ (all_0_126_126 = e11) % 11.63/3.17 | (560) all_0_126_126 = e12 % 11.63/3.17 | % 11.63/3.17 | Equations (560) can reduce 217 to: % 11.63/3.17 | (561) ~ (all_0_127_127 = e12) % 11.63/3.17 | % 11.63/3.17 | Simplifying 561 yields: % 11.63/3.17 | (562) ~ (all_0_127_127 = e12) % 11.63/3.17 | % 11.63/3.17 | Equations (560) can reduce 39 to: % 11.63/3.17 | (563) ~ (all_0_128_128 = e12) % 11.63/3.17 | % 11.63/3.17 | Simplifying 563 yields: % 11.63/3.17 | (564) ~ (all_0_128_128 = e12) % 11.63/3.17 | % 11.63/3.17 | Equations (560) can reduce 196 to: % 11.63/3.17 | (565) ~ (all_0_132_132 = e12) % 11.63/3.17 | % 11.63/3.17 | Simplifying 565 yields: % 11.63/3.17 | (566) ~ (all_0_132_132 = e12) % 11.63/3.17 | % 11.63/3.17 | Equations (560) can reduce 553 to: % 11.63/3.17 | (60) ~ (e12 = e11) % 11.63/3.17 | % 11.63/3.17 | From (560) and (193) follows: % 11.63/3.17 | (568) h2(e12) = all_0_51_51 % 11.63/3.17 | % 11.63/3.17 +-Applying beta-rule and splitting (289), into two cases. % 11.63/3.17 |-Branch one: % 11.63/3.17 | (569) all_0_129_129 = e13 % 11.63/3.17 | % 11.63/3.17 | Combining equations (569,552) yields a new equation: % 11.63/3.17 | (570) e13 = e11 % 11.63/3.17 | % 11.63/3.17 | Simplifying 570 yields: % 11.63/3.17 | (571) e13 = e11 % 11.63/3.17 | % 11.63/3.17 | Equations (571) can reduce 347 to: % 11.63/3.17 | (367) $false % 11.63/3.17 | % 11.63/3.17 |-The branch is then unsatisfiable % 11.63/3.17 |-Branch two: % 11.63/3.17 | (573) ~ (all_0_129_129 = e13) % 11.63/3.17 | (574) all_0_132_132 = e13 % 11.63/3.17 | % 11.63/3.17 | Equations (574) can reduce 65 to: % 11.63/3.17 | (575) ~ (all_0_134_134 = e13) % 11.63/3.17 | % 11.63/3.17 | Simplifying 575 yields: % 11.63/3.17 | (576) ~ (all_0_134_134 = e13) % 11.63/3.17 | % 11.63/3.17 | Equations (574) can reduce 566 to: % 11.63/3.17 | (276) ~ (e13 = e12) % 11.63/3.17 | % 11.63/3.17 | From (574) and (251) follows: % 11.63/3.17 | (578) h2(e13) = all_0_57_57 % 11.63/3.17 | % 11.63/3.17 +-Applying beta-rule and splitting (87), into two cases. % 11.63/3.17 |-Branch one: % 11.63/3.17 | (579) (all_0_102_102 = e12 & all_0_103_103 = e10 & all_0_125_125 = e13 & ~ (all_0_126_126 = e12) & ~ (all_0_129_129 = e11)) | (all_0_104_104 = e13 & all_0_105_105 = e12 & all_0_106_106 = e10 & all_0_126_126 = e11 & ~ (all_0_124_124 = e13)) | (all_0_107_107 = e13 & all_0_108_108 = e12 & all_0_109_109 = e10 & all_0_130_130 = e11 & all_0_134_134 = e11) % 11.63/3.17 | % 11.63/3.17 +-Applying beta-rule and splitting (579), into two cases. % 11.63/3.17 |-Branch one: % 11.63/3.17 | (580) (all_0_102_102 = e12 & all_0_103_103 = e10 & all_0_125_125 = e13 & ~ (all_0_126_126 = e12) & ~ (all_0_129_129 = e11)) | (all_0_104_104 = e13 & all_0_105_105 = e12 & all_0_106_106 = e10 & all_0_126_126 = e11 & ~ (all_0_124_124 = e13)) % 11.63/3.17 | % 11.63/3.17 +-Applying beta-rule and splitting (580), into two cases. % 11.63/3.17 |-Branch one: % 11.63/3.17 | (581) all_0_102_102 = e12 & all_0_103_103 = e10 & all_0_125_125 = e13 & ~ (all_0_126_126 = e12) & ~ (all_0_129_129 = e11) % 11.63/3.17 | % 11.63/3.17 | Applying alpha-rule on (581) yields: % 11.63/3.17 | (582) all_0_125_125 = e13 % 11.63/3.17 | (583) ~ (all_0_129_129 = e11) % 11.63/3.17 | (584) all_0_102_102 = e12 % 11.63/3.17 | (585) ~ (all_0_126_126 = e12) % 11.63/3.17 | (586) all_0_103_103 = e10 % 11.63/3.17 | % 11.63/3.17 | Equations (552) can reduce 583 to: % 11.63/3.17 | (367) $false % 11.63/3.17 | % 11.63/3.17 |-The branch is then unsatisfiable % 11.63/3.17 |-Branch two: % 11.63/3.17 | (588) all_0_104_104 = e13 & all_0_105_105 = e12 & all_0_106_106 = e10 & all_0_126_126 = e11 & ~ (all_0_124_124 = e13) % 11.63/3.17 | % 11.63/3.17 | Applying alpha-rule on (588) yields: % 11.63/3.17 | (589) ~ (all_0_124_124 = e13) % 11.63/3.17 | (557) all_0_126_126 = e11 % 11.63/3.17 | (591) all_0_104_104 = e13 % 11.63/3.17 | (592) all_0_106_106 = e10 % 11.63/3.17 | (593) all_0_105_105 = e12 % 11.63/3.17 | % 11.63/3.17 | Combining equations (560,557) yields a new equation: % 11.63/3.17 | (594) e12 = e11 % 11.63/3.17 | % 11.63/3.17 | Simplifying 594 yields: % 11.63/3.17 | (595) e12 = e11 % 11.63/3.17 | % 11.63/3.17 | Equations (595) can reduce 60 to: % 11.63/3.17 | (367) $false % 11.63/3.17 | % 11.63/3.17 |-The branch is then unsatisfiable % 11.63/3.17 |-Branch two: % 11.63/3.17 | (597) all_0_107_107 = e13 & all_0_108_108 = e12 & all_0_109_109 = e10 & all_0_130_130 = e11 & all_0_134_134 = e11 % 11.63/3.17 | % 11.63/3.17 | Applying alpha-rule on (597) yields: % 11.63/3.17 | (598) all_0_130_130 = e11 % 11.63/3.17 | (599) all_0_107_107 = e13 % 11.63/3.17 | (600) all_0_108_108 = e12 % 11.63/3.17 | (601) all_0_134_134 = e11 % 11.63/3.17 | (602) all_0_109_109 = e10 % 11.63/3.17 | % 11.63/3.17 | Equations (598) can reduce 555 to: % 11.63/3.17 | (367) $false % 11.63/3.17 | % 11.63/3.17 |-The branch is then unsatisfiable % 11.63/3.17 |-Branch two: % 11.63/3.17 | (604) all_0_110_110 = e13 & all_0_111_111 = e12 & all_0_112_112 = e10 & all_0_134_134 = e11 & ~ (all_0_131_131 = e11) & ( ~ (all_0_128_128 = e12) | all_0_127_127 = e10) % 11.63/3.17 | % 11.63/3.17 | Applying alpha-rule on (604) yields: % 11.63/3.17 | (605) ~ (all_0_131_131 = e11) % 11.63/3.17 | (606) all_0_111_111 = e12 % 11.63/3.17 | (607) all_0_110_110 = e13 % 11.63/3.17 | (601) all_0_134_134 = e11 % 11.63/3.17 | (609) all_0_112_112 = e10 % 11.63/3.17 | (610) ~ (all_0_128_128 = e12) | all_0_127_127 = e10 % 11.63/3.17 | % 11.63/3.17 | Equations (601) can reduce 98 to: % 11.63/3.17 | (605) ~ (all_0_131_131 = e11) % 11.63/3.17 | % 11.63/3.17 | Equations (601) can reduce 576 to: % 11.63/3.17 | (612) ~ (e13 = e11) % 11.63/3.17 | % 11.63/3.17 | Simplifying 612 yields: % 11.63/3.17 | (347) ~ (e13 = e11) % 11.63/3.17 | % 11.63/3.17 | From (601) and (322) follows: % 11.63/3.17 | (614) h2(e11) = all_0_59_59 % 11.63/3.17 | % 11.63/3.17 +-Applying beta-rule and splitting (268), into two cases. % 11.63/3.17 |-Branch one: % 11.63/3.17 | (615) (all_0_124_124 = e13 & all_0_134_134 = e12) | (all_0_124_124 = e13 & ~ (all_0_130_130 = e11)) | (all_0_126_126 = e12 & all_0_134_134 = e13) | (all_0_127_127 = e11 & ~ (all_0_134_134 = e11)) | (all_0_127_127 = e10 & all_0_131_131 = e11 & ~ (all_0_128_128 = e12)) | (all_0_128_128 = e12 & ~ (all_0_125_125 = e13) & ~ (all_0_127_127 = e10)) | (all_0_129_129 = e11 & all_0_134_134 = e13) % 11.63/3.17 | % 11.63/3.17 +-Applying beta-rule and splitting (615), into two cases. % 11.63/3.17 |-Branch one: % 11.63/3.17 | (616) (all_0_124_124 = e13 & all_0_134_134 = e12) | (all_0_124_124 = e13 & ~ (all_0_130_130 = e11)) | (all_0_126_126 = e12 & all_0_134_134 = e13) | (all_0_127_127 = e11 & ~ (all_0_134_134 = e11)) | (all_0_127_127 = e10 & all_0_131_131 = e11 & ~ (all_0_128_128 = e12)) | (all_0_128_128 = e12 & ~ (all_0_125_125 = e13) & ~ (all_0_127_127 = e10)) % 11.63/3.17 | % 11.63/3.17 +-Applying beta-rule and splitting (616), into two cases. % 11.63/3.17 |-Branch one: % 11.63/3.17 | (617) (all_0_124_124 = e13 & all_0_134_134 = e12) | (all_0_124_124 = e13 & ~ (all_0_130_130 = e11)) | (all_0_126_126 = e12 & all_0_134_134 = e13) | (all_0_127_127 = e11 & ~ (all_0_134_134 = e11)) | (all_0_127_127 = e10 & all_0_131_131 = e11 & ~ (all_0_128_128 = e12)) % 11.63/3.17 | % 11.63/3.17 +-Applying beta-rule and splitting (617), into two cases. % 11.63/3.17 |-Branch one: % 11.63/3.17 | (618) (all_0_124_124 = e13 & all_0_134_134 = e12) | (all_0_124_124 = e13 & ~ (all_0_130_130 = e11)) | (all_0_126_126 = e12 & all_0_134_134 = e13) | (all_0_127_127 = e11 & ~ (all_0_134_134 = e11)) % 11.63/3.18 | % 11.63/3.18 +-Applying beta-rule and splitting (618), into two cases. % 11.63/3.18 |-Branch one: % 11.63/3.18 | (619) (all_0_124_124 = e13 & all_0_134_134 = e12) | (all_0_124_124 = e13 & ~ (all_0_130_130 = e11)) | (all_0_126_126 = e12 & all_0_134_134 = e13) % 11.63/3.18 | % 11.63/3.18 +-Applying beta-rule and splitting (619), into two cases. % 11.63/3.18 |-Branch one: % 11.63/3.18 | (620) (all_0_124_124 = e13 & all_0_134_134 = e12) | (all_0_124_124 = e13 & ~ (all_0_130_130 = e11)) % 11.63/3.18 | % 11.63/3.18 +-Applying beta-rule and splitting (620), into two cases. % 11.63/3.18 |-Branch one: % 11.63/3.18 | (621) all_0_124_124 = e13 & all_0_134_134 = e12 % 11.63/3.18 | % 11.63/3.18 | Applying alpha-rule on (621) yields: % 11.63/3.18 | (622) all_0_124_124 = e13 % 11.63/3.18 | (623) all_0_134_134 = e12 % 11.63/3.18 | % 11.63/3.18 | Combining equations (623,601) yields a new equation: % 11.63/3.18 | (594) e12 = e11 % 11.63/3.18 | % 11.63/3.18 | Simplifying 594 yields: % 11.63/3.18 | (595) e12 = e11 % 11.63/3.18 | % 11.63/3.18 | Equations (595) can reduce 60 to: % 11.63/3.18 | (367) $false % 11.63/3.18 | % 11.63/3.18 |-The branch is then unsatisfiable % 11.63/3.18 |-Branch two: % 11.63/3.18 | (627) all_0_124_124 = e13 & ~ (all_0_130_130 = e11) % 11.63/3.18 | % 11.63/3.18 | Applying alpha-rule on (627) yields: % 11.63/3.18 | (622) all_0_124_124 = e13 % 11.63/3.18 | (555) ~ (all_0_130_130 = e11) % 11.63/3.18 | % 11.63/3.18 | Equations (622) can reduce 129 to: % 11.63/3.18 | (630) ~ (all_0_125_125 = e13) % 11.63/3.18 | % 11.63/3.18 | Simplifying 630 yields: % 11.63/3.18 | (631) ~ (all_0_125_125 = e13) % 11.63/3.18 | % 11.63/3.18 | Equations (622) can reduce 109 to: % 11.63/3.18 | (632) ~ (all_0_127_127 = e13) % 11.63/3.18 | % 11.63/3.18 | Simplifying 632 yields: % 11.63/3.18 | (56) ~ (all_0_127_127 = e13) % 11.63/3.18 | % 11.63/3.18 | Equations (622) can reduce 29 to: % 11.63/3.18 | (634) ~ (all_0_130_130 = e13) % 11.63/3.18 | % 11.63/3.18 | Simplifying 634 yields: % 11.63/3.18 | (635) ~ (all_0_130_130 = e13) % 11.63/3.18 | % 11.63/3.18 | From (622) and (253) follows: % 11.63/3.18 | (636) h2(e13) = all_0_49_49 % 11.63/3.18 | % 11.63/3.18 +-Applying beta-rule and splitting (118), into two cases. % 11.63/3.18 |-Branch one: % 11.63/3.18 | (637) all_0_124_124 = e12 % 11.63/3.18 | % 11.63/3.18 | Combining equations (622,637) yields a new equation: % 11.63/3.18 | (638) e13 = e12 % 11.63/3.18 | % 11.63/3.18 | Simplifying 638 yields: % 11.63/3.18 | (639) e13 = e12 % 11.63/3.18 | % 11.63/3.18 | Equations (639) can reduce 276 to: % 11.63/3.18 | (367) $false % 11.63/3.18 | % 11.63/3.18 |-The branch is then unsatisfiable % 11.63/3.18 |-Branch two: % 11.63/3.18 | (641) ~ (all_0_124_124 = e12) % 11.63/3.18 | (642) all_0_125_125 = e12 % 11.63/3.18 | % 11.63/3.18 | Equations (642) can reduce 631 to: % 11.63/3.18 | (643) ~ (e13 = e12) % 11.63/3.18 | % 11.63/3.18 | Simplifying 643 yields: % 11.63/3.18 | (276) ~ (e13 = e12) % 11.63/3.18 | % 11.63/3.18 | From (642) and (145) follows: % 11.63/3.18 | (645) h2(e12) = all_0_50_50 % 11.63/3.18 | % 11.63/3.18 +-Applying beta-rule and splitting (311), into two cases. % 11.63/3.18 |-Branch one: % 11.63/3.18 | (598) all_0_130_130 = e11 % 11.63/3.18 | % 11.63/3.18 | Equations (598) can reduce 555 to: % 11.63/3.18 | (367) $false % 11.63/3.18 | % 11.63/3.18 |-The branch is then unsatisfiable % 11.63/3.18 |-Branch two: % 11.63/3.18 | (555) ~ (all_0_130_130 = e11) % 11.63/3.18 | (649) all_0_130_130 = e13 | all_0_130_130 = e10 % 11.63/3.18 | % 11.63/3.18 +-Applying beta-rule and splitting (335), into two cases. % 11.63/3.18 |-Branch one: % 11.63/3.18 | (582) all_0_125_125 = e13 % 11.63/3.18 | % 11.63/3.18 | Combining equations (642,582) yields a new equation: % 11.63/3.18 | (639) e13 = e12 % 11.63/3.18 | % 11.63/3.18 | Equations (639) can reduce 276 to: % 11.63/3.18 | (367) $false % 11.63/3.18 | % 11.63/3.18 |-The branch is then unsatisfiable % 11.63/3.18 |-Branch two: % 11.63/3.18 | (631) ~ (all_0_125_125 = e13) % 11.63/3.18 | (654) all_0_131_131 = e13 | all_0_134_134 = e13 % 11.63/3.18 | % 11.63/3.18 | Equations (642) can reduce 631 to: % 11.63/3.18 | (643) ~ (e13 = e12) % 11.63/3.18 | % 11.63/3.18 | Simplifying 643 yields: % 11.63/3.18 | (276) ~ (e13 = e12) % 11.63/3.18 | % 11.63/3.18 +-Applying beta-rule and splitting (81), into two cases. % 11.63/3.18 |-Branch one: % 11.63/3.18 | (657) all_0_132_132 = e12 % 11.63/3.18 | % 11.63/3.18 | Combining equations (574,657) yields a new equation: % 11.63/3.18 | (638) e13 = e12 % 11.63/3.18 | % 11.63/3.18 | Simplifying 638 yields: % 11.63/3.18 | (639) e13 = e12 % 11.63/3.18 | % 11.63/3.18 | Equations (639) can reduce 276 to: % 11.63/3.18 | (367) $false % 11.63/3.18 | % 11.63/3.18 |-The branch is then unsatisfiable % 11.63/3.18 |-Branch two: % 11.63/3.18 | (566) ~ (all_0_132_132 = e12) % 11.63/3.18 | (662) all_0_133_133 = e12 | all_0_134_134 = e12 % 11.63/3.18 | % 11.63/3.18 +-Applying beta-rule and splitting (649), into two cases. % 11.63/3.18 |-Branch one: % 11.63/3.18 | (663) all_0_130_130 = e13 % 11.63/3.18 | % 11.63/3.18 | Equations (663) can reduce 635 to: % 11.63/3.18 | (367) $false % 11.63/3.18 | % 11.63/3.18 |-The branch is then unsatisfiable % 11.63/3.18 |-Branch two: % 11.63/3.18 | (635) ~ (all_0_130_130 = e13) % 11.63/3.18 | (666) all_0_130_130 = e10 % 11.63/3.18 | % 11.63/3.18 | Equations (666) can reduce 68 to: % 11.63/3.18 | (667) ~ (all_0_127_127 = e10) % 11.63/3.18 | % 11.63/3.18 | From (666) and (106) follows: % 11.63/3.18 | (668) h2(e10) = all_0_55_55 % 11.63/3.18 | % 11.63/3.18 +-Applying beta-rule and splitting (234), into two cases. % 11.63/3.18 |-Branch one: % 11.63/3.18 | (669) all_0_127_127 = e10 % 11.63/3.18 | % 11.63/3.18 | Equations (669) can reduce 667 to: % 11.63/3.18 | (367) $false % 11.63/3.18 | % 11.63/3.18 |-The branch is then unsatisfiable % 11.63/3.18 |-Branch two: % 11.63/3.18 | (667) ~ (all_0_127_127 = e10) % 11.63/3.18 | (672) all_0_128_128 = e10 % 11.63/3.18 | % 11.63/3.18 | Equations (672) can reduce 91 to: % 11.63/3.18 | (667) ~ (all_0_127_127 = e10) % 11.63/3.18 | % 11.63/3.18 | From (672) and (8) follows: % 11.63/3.18 | (674) h2(e10) = all_0_53_53 % 11.63/3.18 | % 11.63/3.18 +-Applying beta-rule and splitting (321), into two cases. % 11.63/3.18 |-Branch one: % 11.63/3.18 | (675) all_0_127_127 = e11 % 11.63/3.18 | % 11.63/3.18 | Equations (675) can reduce 56 to: % 11.63/3.18 | (612) ~ (e13 = e11) % 11.63/3.18 | % 11.63/3.18 | Simplifying 612 yields: % 11.63/3.18 | (347) ~ (e13 = e11) % 11.63/3.18 | % 11.63/3.18 | Equations (675) can reduce 562 to: % 11.63/3.18 | (678) ~ (e12 = e11) % 11.63/3.18 | % 11.63/3.18 | Simplifying 678 yields: % 11.63/3.18 | (60) ~ (e12 = e11) % 11.63/3.18 | % 11.63/3.18 | From (675) and (92) follows: % 11.63/3.18 | (680) h2(e11) = all_0_52_52 % 11.63/3.18 | % 11.63/3.18 +-Applying beta-rule and splitting (167), into two cases. % 11.63/3.18 |-Branch one: % 11.63/3.19 | (569) all_0_129_129 = e13 % 11.63/3.19 | % 11.63/3.19 | Combining equations (569,552) yields a new equation: % 11.63/3.19 | (570) e13 = e11 % 11.63/3.19 | % 11.63/3.19 | Simplifying 570 yields: % 11.63/3.19 | (571) e13 = e11 % 11.63/3.19 | % 11.63/3.19 | Equations (571) can reduce 347 to: % 11.63/3.19 | (367) $false % 11.63/3.19 | % 11.63/3.19 |-The branch is then unsatisfiable % 11.63/3.19 |-Branch two: % 11.63/3.19 | (573) ~ (all_0_129_129 = e13) % 11.63/3.19 | (686) all_0_130_130 = e13 | all_0_131_131 = e13 % 11.63/3.19 | % 11.63/3.19 | Equations (552) can reduce 573 to: % 11.63/3.19 | (612) ~ (e13 = e11) % 11.63/3.19 | % 11.63/3.19 | Simplifying 612 yields: % 11.63/3.19 | (347) ~ (e13 = e11) % 11.63/3.19 | % 11.63/3.19 +-Applying beta-rule and splitting (662), into two cases. % 11.63/3.19 |-Branch one: % 11.63/3.19 | (689) all_0_133_133 = e12 % 11.63/3.19 | % 11.63/3.19 | From (689) and (302) follows: % 11.63/3.19 | (690) h2(e12) = all_0_58_58 % 11.63/3.19 | % 11.63/3.19 +-Applying beta-rule and splitting (654), into two cases. % 11.63/3.19 |-Branch one: % 11.63/3.19 | (691) all_0_131_131 = e13 % 11.63/3.19 | % 11.63/3.19 | From (691) and (125) follows: % 11.63/3.19 | (692) h2(e13) = all_0_56_56 % 11.63/3.19 | % 11.63/3.19 | Instantiating formula (107) with e13, all_0_49_49, e23 and discharging atoms h2(e13) = all_0_49_49, h2(e13) = e23, yields: % 11.63/3.19 | (693) all_0_49_49 = e23 % 11.63/3.19 | % 11.63/3.19 | Instantiating formula (107) with e13, all_0_56_56, all_0_49_49 and discharging atoms h2(e13) = all_0_49_49, h2(e13) = all_0_56_56, yields: % 11.63/3.19 | (694) all_0_49_49 = all_0_56_56 % 11.63/3.19 | % 11.63/3.19 | Instantiating formula (107) with e13, all_0_57_57, all_0_49_49 and discharging atoms h2(e13) = all_0_49_49, h2(e13) = all_0_57_57, yields: % 11.63/3.19 | (695) all_0_49_49 = all_0_57_57 % 11.63/3.19 | % 11.63/3.19 | Instantiating formula (107) with e12, all_0_51_51, e22 and discharging atoms h2(e12) = all_0_51_51, h2(e12) = e22, yields: % 11.63/3.19 | (696) all_0_51_51 = e22 % 11.63/3.19 | % 11.63/3.19 | Instantiating formula (107) with e12, all_0_51_51, all_0_50_50 and discharging atoms h2(e12) = all_0_50_50, h2(e12) = all_0_51_51, yields: % 11.63/3.19 | (697) all_0_50_50 = all_0_51_51 % 11.63/3.19 | % 11.63/3.19 | Instantiating formula (107) with e12, all_0_58_58, all_0_50_50 and discharging atoms h2(e12) = all_0_50_50, h2(e12) = all_0_58_58, yields: % 11.63/3.19 | (698) all_0_50_50 = all_0_58_58 % 11.63/3.19 | % 11.63/3.19 | Instantiating formula (107) with e11, all_0_52_52, e21 and discharging atoms h2(e11) = all_0_52_52, h2(e11) = e21, yields: % 11.63/3.19 | (699) all_0_52_52 = e21 % 11.63/3.19 | % 11.63/3.19 | Instantiating formula (107) with e11, all_0_54_54, all_0_52_52 and discharging atoms h2(e11) = all_0_52_52, h2(e11) = all_0_54_54, yields: % 11.63/3.19 | (700) all_0_52_52 = all_0_54_54 % 11.63/3.19 | % 11.63/3.19 | Instantiating formula (107) with e11, all_0_59_59, all_0_54_54 and discharging atoms h2(e11) = all_0_54_54, h2(e11) = all_0_59_59, yields: % 11.63/3.19 | (701) all_0_54_54 = all_0_59_59 % 11.63/3.19 | % 11.63/3.19 | Instantiating formula (107) with e10, all_0_53_53, e20 and discharging atoms h2(e10) = all_0_53_53, h2(e10) = e20, yields: % 11.63/3.19 | (702) all_0_53_53 = e20 % 11.63/3.19 | % 11.63/3.19 | Instantiating formula (107) with e10, all_0_55_55, all_0_53_53 and discharging atoms h2(e10) = all_0_53_53, h2(e10) = all_0_55_55, yields: % 11.63/3.19 | (703) all_0_53_53 = all_0_55_55 % 11.63/3.19 | % 11.63/3.19 | Combining equations (695,694) yields a new equation: % 11.63/3.19 | (704) all_0_56_56 = all_0_57_57 % 11.63/3.19 | % 11.63/3.19 | Combining equations (693,694) yields a new equation: % 11.63/3.19 | (705) all_0_56_56 = e23 % 11.63/3.19 | % 11.63/3.19 | Combining equations (697,698) yields a new equation: % 11.63/3.19 | (706) all_0_51_51 = all_0_58_58 % 11.63/3.19 | % 11.63/3.19 | Simplifying 706 yields: % 11.63/3.19 | (707) all_0_51_51 = all_0_58_58 % 11.63/3.19 | % 11.63/3.19 | Combining equations (696,707) yields a new equation: % 11.63/3.19 | (708) all_0_58_58 = e22 % 11.63/3.19 | % 11.63/3.19 | Combining equations (700,699) yields a new equation: % 11.63/3.19 | (709) all_0_54_54 = e21 % 11.63/3.19 | % 11.63/3.19 | Simplifying 709 yields: % 11.63/3.19 | (710) all_0_54_54 = e21 % 11.63/3.19 | % 11.63/3.19 | Combining equations (703,702) yields a new equation: % 11.63/3.19 | (711) all_0_55_55 = e20 % 11.63/3.19 | % 11.63/3.19 | Simplifying 711 yields: % 11.63/3.19 | (712) all_0_55_55 = e20 % 11.63/3.19 | % 11.63/3.19 | Combining equations (701,710) yields a new equation: % 11.63/3.19 | (713) all_0_59_59 = e21 % 11.63/3.19 | % 11.63/3.19 | Simplifying 713 yields: % 11.63/3.19 | (714) all_0_59_59 = e21 % 11.63/3.19 | % 11.63/3.19 | Combining equations (704,705) yields a new equation: % 11.63/3.19 | (715) all_0_57_57 = e23 % 11.63/3.19 | % 11.63/3.19 | Simplifying 715 yields: % 11.63/3.19 | (716) all_0_57_57 = e23 % 11.63/3.19 | % 11.63/3.19 | Combining equations (708,707) yields a new equation: % 11.63/3.19 | (696) all_0_51_51 = e22 % 11.63/3.19 | % 11.63/3.19 | Combining equations (708,698) yields a new equation: % 11.63/3.19 | (718) all_0_50_50 = e22 % 11.63/3.19 | % 11.63/3.19 | Combining equations (705,694) yields a new equation: % 11.63/3.19 | (693) all_0_49_49 = e23 % 11.63/3.19 | % 11.63/3.19 +-Applying beta-rule and splitting (148), into two cases. % 11.63/3.19 |-Branch one: % 11.63/3.19 | (720) ~ (all_0_49_49 = all_0_113_113) % 11.63/3.19 | % 11.63/3.19 | Equations (693,369) can reduce 720 to: % 11.63/3.19 | (367) $false % 11.63/3.19 | % 11.63/3.19 |-The branch is then unsatisfiable % 11.63/3.19 |-Branch two: % 11.63/3.19 | (722) all_0_49_49 = all_0_113_113 % 11.63/3.19 | (723) ~ (all_0_50_50 = all_0_114_114) | ~ (all_0_51_51 = all_0_115_115) | ~ (all_0_52_52 = all_0_116_116) | ~ (all_0_53_53 = all_0_117_117) | ~ (all_0_54_54 = all_0_118_118) | ~ (all_0_55_55 = all_0_119_119) | ~ (all_0_56_56 = all_0_120_120) | ~ (all_0_57_57 = all_0_121_121) | ~ (all_0_58_58 = all_0_122_122) | ~ (all_0_59_59 = all_0_123_123) % 11.63/3.19 | % 11.63/3.19 +-Applying beta-rule and splitting (723), into two cases. % 11.63/3.19 |-Branch one: % 11.63/3.19 | (724) ~ (all_0_50_50 = all_0_114_114) % 11.63/3.19 | % 11.63/3.19 | Equations (718,358) can reduce 724 to: % 11.63/3.19 | (367) $false % 11.63/3.19 | % 11.63/3.19 |-The branch is then unsatisfiable % 11.63/3.19 |-Branch two: % 11.63/3.19 | (726) all_0_50_50 = all_0_114_114 % 11.63/3.19 | (727) ~ (all_0_51_51 = all_0_115_115) | ~ (all_0_52_52 = all_0_116_116) | ~ (all_0_53_53 = all_0_117_117) | ~ (all_0_54_54 = all_0_118_118) | ~ (all_0_55_55 = all_0_119_119) | ~ (all_0_56_56 = all_0_120_120) | ~ (all_0_57_57 = all_0_121_121) | ~ (all_0_58_58 = all_0_122_122) | ~ (all_0_59_59 = all_0_123_123) % 11.63/3.20 | % 11.63/3.20 +-Applying beta-rule and splitting (727), into two cases. % 11.63/3.20 |-Branch one: % 11.63/3.20 | (728) ~ (all_0_51_51 = all_0_115_115) % 11.63/3.20 | % 11.63/3.20 | Equations (696,351) can reduce 728 to: % 11.63/3.20 | (367) $false % 11.63/3.20 | % 11.63/3.20 |-The branch is then unsatisfiable % 11.63/3.20 |-Branch two: % 11.63/3.20 | (730) all_0_51_51 = all_0_115_115 % 11.63/3.20 | (731) ~ (all_0_52_52 = all_0_116_116) | ~ (all_0_53_53 = all_0_117_117) | ~ (all_0_54_54 = all_0_118_118) | ~ (all_0_55_55 = all_0_119_119) | ~ (all_0_56_56 = all_0_120_120) | ~ (all_0_57_57 = all_0_121_121) | ~ (all_0_58_58 = all_0_122_122) | ~ (all_0_59_59 = all_0_123_123) % 11.63/3.20 | % 11.63/3.20 +-Applying beta-rule and splitting (731), into two cases. % 11.63/3.20 |-Branch one: % 11.63/3.20 | (732) ~ (all_0_52_52 = all_0_116_116) % 11.63/3.20 | % 11.63/3.20 | Equations (699,400) can reduce 732 to: % 11.63/3.20 | (367) $false % 11.63/3.20 | % 11.63/3.20 |-The branch is then unsatisfiable % 11.63/3.20 |-Branch two: % 11.63/3.20 | (734) all_0_52_52 = all_0_116_116 % 11.63/3.20 | (735) ~ (all_0_53_53 = all_0_117_117) | ~ (all_0_54_54 = all_0_118_118) | ~ (all_0_55_55 = all_0_119_119) | ~ (all_0_56_56 = all_0_120_120) | ~ (all_0_57_57 = all_0_121_121) | ~ (all_0_58_58 = all_0_122_122) | ~ (all_0_59_59 = all_0_123_123) % 11.63/3.20 | % 11.63/3.20 +-Applying beta-rule and splitting (735), into two cases. % 11.63/3.20 |-Branch one: % 11.63/3.20 | (736) ~ (all_0_53_53 = all_0_117_117) % 11.63/3.20 | % 11.63/3.20 | Equations (702,472) can reduce 736 to: % 11.63/3.20 | (367) $false % 11.63/3.20 | % 11.63/3.20 |-The branch is then unsatisfiable % 11.63/3.20 |-Branch two: % 11.63/3.20 | (738) all_0_53_53 = all_0_117_117 % 11.63/3.20 | (739) ~ (all_0_54_54 = all_0_118_118) | ~ (all_0_55_55 = all_0_119_119) | ~ (all_0_56_56 = all_0_120_120) | ~ (all_0_57_57 = all_0_121_121) | ~ (all_0_58_58 = all_0_122_122) | ~ (all_0_59_59 = all_0_123_123) % 11.63/3.20 | % 11.63/3.20 +-Applying beta-rule and splitting (739), into two cases. % 11.63/3.20 |-Branch one: % 11.92/3.20 | (740) ~ (all_0_54_54 = all_0_118_118) % 11.92/3.20 | % 11.92/3.20 | Equations (710,551) can reduce 740 to: % 11.92/3.20 | (367) $false % 11.92/3.20 | % 11.92/3.20 |-The branch is then unsatisfiable % 11.92/3.20 |-Branch two: % 11.92/3.20 | (742) all_0_54_54 = all_0_118_118 % 11.92/3.20 | (743) ~ (all_0_55_55 = all_0_119_119) | ~ (all_0_56_56 = all_0_120_120) | ~ (all_0_57_57 = all_0_121_121) | ~ (all_0_58_58 = all_0_122_122) | ~ (all_0_59_59 = all_0_123_123) % 11.92/3.20 | % 11.92/3.20 +-Applying beta-rule and splitting (743), into two cases. % 11.92/3.20 |-Branch one: % 11.92/3.20 | (744) ~ (all_0_55_55 = all_0_119_119) % 11.92/3.20 | % 11.92/3.20 | Equations (712,393) can reduce 744 to: % 11.92/3.20 | (367) $false % 11.92/3.20 | % 11.92/3.20 |-The branch is then unsatisfiable % 11.92/3.20 |-Branch two: % 11.92/3.20 | (746) all_0_55_55 = all_0_119_119 % 11.92/3.20 | (747) ~ (all_0_56_56 = all_0_120_120) | ~ (all_0_57_57 = all_0_121_121) | ~ (all_0_58_58 = all_0_122_122) | ~ (all_0_59_59 = all_0_123_123) % 11.92/3.20 | % 11.92/3.20 +-Applying beta-rule and splitting (747), into two cases. % 11.92/3.20 |-Branch one: % 11.92/3.20 | (748) ~ (all_0_56_56 = all_0_120_120) % 11.92/3.20 | % 11.92/3.20 | Equations (705,481) can reduce 748 to: % 11.92/3.20 | (367) $false % 11.92/3.20 | % 11.92/3.20 |-The branch is then unsatisfiable % 11.92/3.20 |-Branch two: % 11.92/3.20 | (750) all_0_56_56 = all_0_120_120 % 11.92/3.20 | (751) ~ (all_0_57_57 = all_0_121_121) | ~ (all_0_58_58 = all_0_122_122) | ~ (all_0_59_59 = all_0_123_123) % 11.92/3.20 | % 11.92/3.20 +-Applying beta-rule and splitting (751), into two cases. % 11.92/3.20 |-Branch one: % 11.92/3.20 | (752) ~ (all_0_57_57 = all_0_121_121) % 11.92/3.20 | % 11.92/3.20 | Equations (716,412) can reduce 752 to: % 11.92/3.20 | (367) $false % 11.92/3.20 | % 11.92/3.20 |-The branch is then unsatisfiable % 11.92/3.20 |-Branch two: % 11.92/3.20 | (754) all_0_57_57 = all_0_121_121 % 11.92/3.20 | (755) ~ (all_0_58_58 = all_0_122_122) | ~ (all_0_59_59 = all_0_123_123) % 11.92/3.20 | % 11.92/3.20 +-Applying beta-rule and splitting (755), into two cases. % 11.92/3.20 |-Branch one: % 11.92/3.20 | (756) ~ (all_0_58_58 = all_0_122_122) % 11.92/3.20 | % 11.92/3.20 | Equations (708,384) can reduce 756 to: % 11.92/3.20 | (367) $false % 11.92/3.20 | % 11.92/3.20 |-The branch is then unsatisfiable % 11.92/3.20 |-Branch two: % 11.92/3.20 | (758) all_0_58_58 = all_0_122_122 % 11.92/3.20 | (759) ~ (all_0_59_59 = all_0_123_123) % 11.92/3.20 | % 11.92/3.20 | Equations (714,454) can reduce 759 to: % 11.92/3.20 | (367) $false % 11.92/3.20 | % 11.92/3.20 |-The branch is then unsatisfiable % 11.92/3.20 |-Branch two: % 11.92/3.20 | (761) ~ (all_0_131_131 = e13) % 11.92/3.20 | (762) all_0_134_134 = e13 % 11.92/3.20 | % 11.92/3.20 | Combining equations (601,762) yields a new equation: % 11.92/3.20 | (571) e13 = e11 % 11.92/3.20 | % 11.92/3.20 | Equations (571) can reduce 347 to: % 11.92/3.20 | (367) $false % 11.92/3.20 | % 11.92/3.20 |-The branch is then unsatisfiable % 11.92/3.20 |-Branch two: % 11.92/3.20 | (765) ~ (all_0_133_133 = e12) % 11.92/3.20 | (623) all_0_134_134 = e12 % 11.92/3.20 | % 11.92/3.20 | Combining equations (623,601) yields a new equation: % 11.92/3.20 | (594) e12 = e11 % 11.92/3.20 | % 11.92/3.20 | Simplifying 594 yields: % 11.92/3.20 | (595) e12 = e11 % 11.92/3.20 | % 11.92/3.20 | Equations (595) can reduce 60 to: % 11.92/3.20 | (367) $false % 11.92/3.20 | % 11.92/3.20 |-The branch is then unsatisfiable % 11.92/3.20 |-Branch two: % 11.92/3.20 | (770) ~ (all_0_127_127 = e11) % 11.92/3.20 | (771) all_0_127_127 = e12 | all_0_127_127 = e10 % 11.92/3.20 | % 11.92/3.20 +-Applying beta-rule and splitting (771), into two cases. % 11.92/3.20 |-Branch one: % 11.92/3.20 | (772) all_0_127_127 = e12 % 11.92/3.20 | % 11.92/3.21 | Equations (772) can reduce 562 to: % 11.92/3.21 | (367) $false % 11.92/3.21 | % 11.92/3.21 |-The branch is then unsatisfiable % 11.92/3.21 |-Branch two: % 11.92/3.21 | (562) ~ (all_0_127_127 = e12) % 11.92/3.21 | (669) all_0_127_127 = e10 % 11.92/3.21 | % 11.92/3.21 | Equations (669) can reduce 667 to: % 11.92/3.21 | (367) $false % 11.92/3.21 | % 11.92/3.21 |-The branch is then unsatisfiable % 11.92/3.21 |-Branch two: % 11.92/3.21 | (777) all_0_126_126 = e12 & all_0_134_134 = e13 % 11.92/3.21 | % 11.92/3.21 | Applying alpha-rule on (777) yields: % 11.92/3.21 | (560) all_0_126_126 = e12 % 11.92/3.21 | (762) all_0_134_134 = e13 % 11.92/3.21 | % 11.92/3.21 | Combining equations (762,601) yields a new equation: % 11.92/3.21 | (570) e13 = e11 % 11.92/3.21 | % 11.92/3.21 | Simplifying 570 yields: % 11.92/3.21 | (571) e13 = e11 % 11.92/3.21 | % 11.92/3.21 | Equations (571) can reduce 347 to: % 11.92/3.21 | (367) $false % 11.92/3.21 | % 11.92/3.21 |-The branch is then unsatisfiable % 11.92/3.21 |-Branch two: % 11.92/3.21 | (783) all_0_127_127 = e11 & ~ (all_0_134_134 = e11) % 11.92/3.21 | % 11.92/3.21 | Applying alpha-rule on (783) yields: % 11.92/3.21 | (675) all_0_127_127 = e11 % 11.92/3.21 | (785) ~ (all_0_134_134 = e11) % 11.92/3.21 | % 11.92/3.21 | Equations (601) can reduce 785 to: % 11.92/3.21 | (367) $false % 11.92/3.21 | % 11.92/3.21 |-The branch is then unsatisfiable % 11.92/3.21 |-Branch two: % 11.92/3.21 | (787) all_0_127_127 = e10 & all_0_131_131 = e11 & ~ (all_0_128_128 = e12) % 11.92/3.21 | % 11.92/3.21 | Applying alpha-rule on (787) yields: % 11.92/3.21 | (669) all_0_127_127 = e10 % 11.92/3.21 | (789) all_0_131_131 = e11 % 11.92/3.21 | (564) ~ (all_0_128_128 = e12) % 11.92/3.21 | % 11.92/3.21 | Equations (789) can reduce 605 to: % 11.92/3.21 | (367) $false % 11.92/3.21 | % 11.92/3.21 |-The branch is then unsatisfiable % 11.92/3.21 |-Branch two: % 11.92/3.21 | (792) all_0_128_128 = e12 & ~ (all_0_125_125 = e13) & ~ (all_0_127_127 = e10) % 11.92/3.21 | % 11.92/3.21 | Applying alpha-rule on (792) yields: % 11.92/3.21 | (793) all_0_128_128 = e12 % 11.92/3.21 | (631) ~ (all_0_125_125 = e13) % 11.92/3.21 | (667) ~ (all_0_127_127 = e10) % 11.92/3.21 | % 11.92/3.21 | Equations (793) can reduce 564 to: % 11.92/3.21 | (367) $false % 11.92/3.21 | % 11.92/3.21 |-The branch is then unsatisfiable % 11.92/3.21 |-Branch two: % 11.92/3.21 | (797) all_0_129_129 = e11 & all_0_134_134 = e13 % 11.92/3.21 | % 11.92/3.21 | Applying alpha-rule on (797) yields: % 11.92/3.21 | (552) all_0_129_129 = e11 % 11.92/3.21 | (762) all_0_134_134 = e13 % 11.92/3.21 | % 11.92/3.21 | Combining equations (601,762) yields a new equation: % 11.92/3.21 | (571) e13 = e11 % 11.92/3.21 | % 11.92/3.21 | Equations (571) can reduce 347 to: % 11.92/3.21 | (367) $false % 11.92/3.21 | % 11.92/3.21 |-The branch is then unsatisfiable % 11.92/3.21 |-Branch two: % 11.92/3.21 | (802) all_0_131_131 = e11 & ~ (all_0_125_125 = e13) % 11.92/3.21 | % 11.92/3.21 | Applying alpha-rule on (802) yields: % 11.92/3.21 | (789) all_0_131_131 = e11 % 11.92/3.21 | (631) ~ (all_0_125_125 = e13) % 11.92/3.21 | % 11.92/3.21 | Equations (789) can reduce 605 to: % 11.92/3.21 | (367) $false % 11.92/3.21 | % 11.92/3.21 |-The branch is then unsatisfiable % 11.92/3.21 |-Branch two: % 11.92/3.21 | (583) ~ (all_0_129_129 = e11) % 11.92/3.21 | (569) all_0_129_129 = e13 % 11.92/3.21 | % 11.92/3.21 | Equations (569) can reduce 50 to: % 11.92/3.21 | (808) ~ (all_0_132_132 = e13) % 11.92/3.21 | % 11.92/3.21 | Simplifying 808 yields: % 11.92/3.21 | (809) ~ (all_0_132_132 = e13) % 11.92/3.21 | % 11.92/3.21 | Equations (569) can reduce 583 to: % 11.92/3.21 | (347) ~ (e13 = e11) % 11.92/3.21 | % 11.92/3.21 +-Applying beta-rule and splitting (329), into two cases. % 11.92/3.21 |-Branch one: % 11.92/3.21 | (557) all_0_126_126 = e11 % 11.92/3.21 | % 11.92/3.21 | Equations (557) can reduce 217 to: % 11.92/3.21 | (812) ~ (all_0_127_127 = e11) % 11.92/3.21 | % 11.92/3.21 | Simplifying 812 yields: % 11.92/3.21 | (770) ~ (all_0_127_127 = e11) % 11.92/3.21 | % 11.92/3.21 +-Applying beta-rule and splitting (95), into two cases. % 11.92/3.21 |-Branch one: % 11.92/3.21 | (560) all_0_126_126 = e12 % 11.92/3.21 | % 11.92/3.21 | Combining equations (557,560) yields a new equation: % 11.92/3.21 | (595) e12 = e11 % 11.92/3.21 | % 11.92/3.21 | Equations (595) can reduce 60 to: % 11.92/3.21 | (367) $false % 11.92/3.21 | % 11.92/3.21 |-The branch is then unsatisfiable % 11.92/3.21 |-Branch two: % 11.92/3.21 | (585) ~ (all_0_126_126 = e12) % 11.92/3.21 | (657) all_0_132_132 = e12 % 11.92/3.21 | % 11.92/3.21 | Equations (657) can reduce 238 to: % 11.92/3.21 | (819) ~ (all_0_133_133 = e12) % 11.92/3.21 | % 11.92/3.21 | Simplifying 819 yields: % 11.92/3.21 | (765) ~ (all_0_133_133 = e12) % 11.92/3.21 | % 11.92/3.21 | Equations (657) can reduce 65 to: % 11.92/3.21 | (821) ~ (all_0_134_134 = e12) % 11.92/3.21 | % 11.92/3.21 | Simplifying 821 yields: % 11.92/3.21 | (822) ~ (all_0_134_134 = e12) % 11.92/3.21 | % 11.92/3.22 | Equations (657) can reduce 809 to: % 11.92/3.22 | (643) ~ (e13 = e12) % 11.92/3.22 | % 11.92/3.22 | Simplifying 643 yields: % 11.92/3.22 | (276) ~ (e13 = e12) % 11.92/3.22 | % 11.92/3.22 | From (657) and (63) follows: % 11.92/3.22 | (825) op1(e10, e12) = all_0_110_110 % 11.92/3.22 | % 11.92/3.22 | Instantiating formula (45) with e10, e12, all_0_110_110, all_0_133_133 and discharging atoms op1(e10, e12) = all_0_110_110, op1(e10, e12) = all_0_133_133, yields: % 11.92/3.22 | (826) all_0_110_110 = all_0_133_133 % 11.92/3.22 | % 11.92/3.22 +-Applying beta-rule and splitting (198), into two cases. % 11.92/3.22 |-Branch one: % 11.92/3.22 | (622) all_0_124_124 = e13 % 11.92/3.22 | % 11.92/3.22 | Equations (622) can reduce 129 to: % 11.92/3.22 | (630) ~ (all_0_125_125 = e13) % 11.92/3.22 | % 11.92/3.22 | Simplifying 630 yields: % 11.92/3.22 | (631) ~ (all_0_125_125 = e13) % 11.92/3.22 | % 11.92/3.22 | Equations (622) can reduce 254 to: % 11.92/3.22 | (830) ~ (all_0_133_133 = e13) % 11.92/3.22 | % 11.92/3.22 | Simplifying 830 yields: % 11.92/3.22 | (831) ~ (all_0_133_133 = e13) % 11.92/3.22 | % 11.92/3.22 +-Applying beta-rule and splitting (118), into two cases. % 11.92/3.22 |-Branch one: % 11.92/3.22 | (637) all_0_124_124 = e12 % 11.92/3.22 | % 11.92/3.22 | Combining equations (622,637) yields a new equation: % 11.92/3.22 | (638) e13 = e12 % 11.92/3.22 | % 11.92/3.22 | Simplifying 638 yields: % 11.92/3.22 | (639) e13 = e12 % 11.92/3.22 | % 11.92/3.22 | Equations (639) can reduce 276 to: % 11.92/3.22 | (367) $false % 11.92/3.22 | % 11.92/3.22 |-The branch is then unsatisfiable % 11.92/3.22 |-Branch two: % 11.92/3.22 | (641) ~ (all_0_124_124 = e12) % 11.92/3.22 | (642) all_0_125_125 = e12 % 11.92/3.22 | % 11.92/3.22 | Equations (642) can reduce 631 to: % 11.92/3.22 | (643) ~ (e13 = e12) % 11.92/3.22 | % 11.92/3.22 | Simplifying 643 yields: % 11.92/3.22 | (276) ~ (e13 = e12) % 11.92/3.22 | % 11.92/3.22 +-Applying beta-rule and splitting (3), into two cases. % 11.92/3.22 |-Branch one: % 11.92/3.22 | (840) all_0_133_133 = e11 % 11.92/3.22 | % 11.92/3.22 | Combining equations (840,826) yields a new equation: % 11.92/3.22 | (841) all_0_110_110 = e11 % 11.92/3.22 | % 11.92/3.22 | Equations (840) can reduce 296 to: % 11.92/3.22 | (842) ~ (all_0_134_134 = e11) % 11.92/3.22 | % 11.92/3.22 | Simplifying 842 yields: % 11.92/3.22 | (785) ~ (all_0_134_134 = e11) % 11.92/3.22 | % 11.92/3.22 | Equations (840) can reduce 831 to: % 11.92/3.22 | (612) ~ (e13 = e11) % 11.92/3.22 | % 11.92/3.22 | Simplifying 612 yields: % 11.92/3.22 | (347) ~ (e13 = e11) % 11.92/3.22 | % 11.92/3.22 +-Applying beta-rule and splitting (61), into two cases. % 11.92/3.22 |-Branch one: % 11.92/3.22 | (601) all_0_134_134 = e11 % 11.92/3.22 | % 11.92/3.22 | Equations (601) can reduce 785 to: % 11.92/3.22 | (367) $false % 11.92/3.22 | % 11.92/3.22 |-The branch is then unsatisfiable % 11.92/3.22 |-Branch two: % 11.92/3.22 | (785) ~ (all_0_134_134 = e11) % 11.92/3.22 | (849) all_0_134_134 = e13 | all_0_134_134 = e12 % 11.92/3.22 | % 11.92/3.22 +-Applying beta-rule and splitting (87), into two cases. % 11.92/3.22 |-Branch one: % 11.92/3.22 | (579) (all_0_102_102 = e12 & all_0_103_103 = e10 & all_0_125_125 = e13 & ~ (all_0_126_126 = e12) & ~ (all_0_129_129 = e11)) | (all_0_104_104 = e13 & all_0_105_105 = e12 & all_0_106_106 = e10 & all_0_126_126 = e11 & ~ (all_0_124_124 = e13)) | (all_0_107_107 = e13 & all_0_108_108 = e12 & all_0_109_109 = e10 & all_0_130_130 = e11 & all_0_134_134 = e11) % 11.92/3.22 | % 11.92/3.22 +-Applying beta-rule and splitting (579), into two cases. % 11.92/3.22 |-Branch one: % 11.92/3.22 | (580) (all_0_102_102 = e12 & all_0_103_103 = e10 & all_0_125_125 = e13 & ~ (all_0_126_126 = e12) & ~ (all_0_129_129 = e11)) | (all_0_104_104 = e13 & all_0_105_105 = e12 & all_0_106_106 = e10 & all_0_126_126 = e11 & ~ (all_0_124_124 = e13)) % 11.92/3.22 | % 11.92/3.22 +-Applying beta-rule and splitting (580), into two cases. % 11.92/3.22 |-Branch one: % 11.92/3.22 | (581) all_0_102_102 = e12 & all_0_103_103 = e10 & all_0_125_125 = e13 & ~ (all_0_126_126 = e12) & ~ (all_0_129_129 = e11) % 11.92/3.22 | % 11.92/3.22 | Applying alpha-rule on (581) yields: % 11.92/3.22 | (582) all_0_125_125 = e13 % 11.92/3.22 | (583) ~ (all_0_129_129 = e11) % 11.92/3.22 | (584) all_0_102_102 = e12 % 11.92/3.22 | (585) ~ (all_0_126_126 = e12) % 11.92/3.22 | (586) all_0_103_103 = e10 % 11.92/3.22 | % 11.92/3.22 | Combining equations (582,642) yields a new equation: % 11.92/3.22 | (638) e13 = e12 % 11.92/3.22 | % 11.92/3.22 | Simplifying 638 yields: % 11.92/3.22 | (639) e13 = e12 % 11.92/3.22 | % 11.92/3.22 | Equations (639) can reduce 276 to: % 11.92/3.22 | (367) $false % 11.92/3.22 | % 11.92/3.22 |-The branch is then unsatisfiable % 11.92/3.22 |-Branch two: % 11.92/3.22 | (588) all_0_104_104 = e13 & all_0_105_105 = e12 & all_0_106_106 = e10 & all_0_126_126 = e11 & ~ (all_0_124_124 = e13) % 11.92/3.22 | % 11.92/3.22 | Applying alpha-rule on (588) yields: % 11.92/3.22 | (589) ~ (all_0_124_124 = e13) % 11.92/3.22 | (557) all_0_126_126 = e11 % 11.92/3.22 | (591) all_0_104_104 = e13 % 11.92/3.22 | (592) all_0_106_106 = e10 % 11.92/3.22 | (593) all_0_105_105 = e12 % 11.92/3.22 | % 11.92/3.22 | Equations (622) can reduce 589 to: % 11.92/3.22 | (367) $false % 11.92/3.22 | % 11.92/3.22 |-The branch is then unsatisfiable % 11.92/3.22 |-Branch two: % 11.92/3.22 | (597) all_0_107_107 = e13 & all_0_108_108 = e12 & all_0_109_109 = e10 & all_0_130_130 = e11 & all_0_134_134 = e11 % 11.92/3.22 | % 11.92/3.22 | Applying alpha-rule on (597) yields: % 11.92/3.22 | (598) all_0_130_130 = e11 % 11.92/3.22 | (599) all_0_107_107 = e13 % 11.92/3.22 | (600) all_0_108_108 = e12 % 11.92/3.22 | (601) all_0_134_134 = e11 % 11.92/3.22 | (602) all_0_109_109 = e10 % 11.92/3.22 | % 11.92/3.22 | Equations (601) can reduce 785 to: % 11.92/3.22 | (367) $false % 11.92/3.22 | % 11.92/3.22 |-The branch is then unsatisfiable % 11.92/3.22 |-Branch two: % 11.92/3.22 | (604) all_0_110_110 = e13 & all_0_111_111 = e12 & all_0_112_112 = e10 & all_0_134_134 = e11 & ~ (all_0_131_131 = e11) & ( ~ (all_0_128_128 = e12) | all_0_127_127 = e10) % 11.92/3.22 | % 11.92/3.22 | Applying alpha-rule on (604) yields: % 11.92/3.22 | (605) ~ (all_0_131_131 = e11) % 11.92/3.22 | (606) all_0_111_111 = e12 % 11.92/3.22 | (607) all_0_110_110 = e13 % 11.92/3.22 | (601) all_0_134_134 = e11 % 11.92/3.22 | (609) all_0_112_112 = e10 % 11.92/3.22 | (610) ~ (all_0_128_128 = e12) | all_0_127_127 = e10 % 11.92/3.22 | % 11.92/3.22 | Combining equations (841,607) yields a new equation: % 11.92/3.22 | (571) e13 = e11 % 11.92/3.22 | % 11.92/3.22 | Equations (571) can reduce 347 to: % 11.92/3.22 | (367) $false % 11.92/3.22 | % 11.92/3.22 |-The branch is then unsatisfiable % 11.92/3.22 |-Branch two: % 11.92/3.23 | (884) ~ (all_0_133_133 = e11) % 11.92/3.23 | (885) all_0_133_133 = e13 | all_0_133_133 = e12 % 11.92/3.23 | % 11.92/3.23 +-Applying beta-rule and splitting (885), into two cases. % 11.92/3.23 |-Branch one: % 11.92/3.23 | (886) all_0_133_133 = e13 % 11.92/3.23 | % 11.92/3.23 | Equations (886) can reduce 831 to: % 11.92/3.23 | (367) $false % 11.92/3.23 | % 11.92/3.23 |-The branch is then unsatisfiable % 11.92/3.23 |-Branch two: % 11.92/3.23 | (831) ~ (all_0_133_133 = e13) % 11.92/3.23 | (689) all_0_133_133 = e12 % 11.92/3.23 | % 11.92/3.23 | Equations (689) can reduce 765 to: % 11.92/3.23 | (367) $false % 11.92/3.23 | % 11.92/3.23 |-The branch is then unsatisfiable % 11.92/3.23 |-Branch two: % 11.92/3.23 | (589) ~ (all_0_124_124 = e13) % 11.92/3.23 | (637) all_0_124_124 = e12 % 11.92/3.23 | % 11.92/3.23 | Equations (637) can reduce 129 to: % 11.92/3.23 | (893) ~ (all_0_125_125 = e12) % 11.92/3.23 | % 11.92/3.23 | Simplifying 893 yields: % 11.92/3.23 | (894) ~ (all_0_125_125 = e12) % 11.92/3.23 | % 11.92/3.23 | Equations (637) can reduce 109 to: % 11.92/3.23 | (561) ~ (all_0_127_127 = e12) % 11.92/3.23 | % 11.92/3.23 | Simplifying 561 yields: % 11.92/3.23 | (562) ~ (all_0_127_127 = e12) % 11.92/3.23 | % 11.92/3.23 | Equations (637) can reduce 254 to: % 11.92/3.23 | (819) ~ (all_0_133_133 = e12) % 11.92/3.23 | % 11.92/3.23 | Simplifying 819 yields: % 11.92/3.23 | (765) ~ (all_0_133_133 = e12) % 11.92/3.23 | % 11.92/3.23 | Equations (637) can reduce 589 to: % 11.92/3.23 | (643) ~ (e13 = e12) % 11.92/3.23 | % 11.92/3.23 | Simplifying 643 yields: % 11.92/3.23 | (276) ~ (e13 = e12) % 11.92/3.23 | % 11.92/3.23 +-Applying beta-rule and splitting (239), into two cases. % 11.92/3.23 |-Branch one: % 11.92/3.23 | (622) all_0_124_124 = e13 % 11.92/3.23 | % 11.92/3.23 | Combining equations (637,622) yields a new equation: % 11.92/3.23 | (639) e13 = e12 % 11.92/3.23 | % 11.92/3.23 | Equations (639) can reduce 276 to: % 11.92/3.23 | (367) $false % 11.92/3.23 | % 11.92/3.23 |-The branch is then unsatisfiable % 11.92/3.23 |-Branch two: % 11.92/3.23 | (589) ~ (all_0_124_124 = e13) % 11.92/3.23 | (582) all_0_125_125 = e13 % 11.92/3.23 | % 11.92/3.23 | Equations (582) can reduce 191 to: % 11.92/3.23 | (575) ~ (all_0_134_134 = e13) % 11.92/3.23 | % 11.92/3.23 | Simplifying 575 yields: % 11.92/3.23 | (576) ~ (all_0_134_134 = e13) % 11.92/3.23 | % 11.92/3.23 | Equations (582) can reduce 894 to: % 11.92/3.23 | (276) ~ (e13 = e12) % 11.92/3.23 | % 11.92/3.23 +-Applying beta-rule and splitting (158), into two cases. % 11.92/3.23 |-Branch one: % 11.92/3.23 | (574) all_0_132_132 = e13 % 11.92/3.23 | % 11.92/3.23 | Combining equations (574,657) yields a new equation: % 11.92/3.23 | (638) e13 = e12 % 11.92/3.23 | % 11.92/3.23 | Simplifying 638 yields: % 11.92/3.23 | (639) e13 = e12 % 11.92/3.23 | % 11.92/3.23 | Equations (639) can reduce 276 to: % 11.92/3.23 | (367) $false % 11.92/3.23 | % 11.92/3.23 |-The branch is then unsatisfiable % 11.92/3.23 |-Branch two: % 11.92/3.23 | (809) ~ (all_0_132_132 = e13) % 11.92/3.23 | (914) all_0_133_133 = e13 | all_0_134_134 = e13 % 11.92/3.23 | % 11.92/3.23 +-Applying beta-rule and splitting (914), into two cases. % 11.92/3.23 |-Branch one: % 11.92/3.23 | (886) all_0_133_133 = e13 % 11.92/3.23 | % 11.92/3.23 | Equations (886) can reduce 296 to: % 11.92/3.23 | (575) ~ (all_0_134_134 = e13) % 11.92/3.23 | % 11.92/3.23 | Simplifying 575 yields: % 11.92/3.23 | (576) ~ (all_0_134_134 = e13) % 11.92/3.23 | % 11.92/3.23 | Equations (886) can reduce 765 to: % 11.92/3.23 | (276) ~ (e13 = e12) % 11.92/3.23 | % 11.92/3.23 +-Applying beta-rule and splitting (321), into two cases. % 11.92/3.23 |-Branch one: % 11.92/3.23 | (675) all_0_127_127 = e11 % 11.92/3.23 | % 11.92/3.23 | Equations (675) can reduce 770 to: % 11.92/3.23 | (367) $false % 11.92/3.23 | % 11.92/3.23 |-The branch is then unsatisfiable % 11.92/3.23 |-Branch two: % 11.92/3.23 | (770) ~ (all_0_127_127 = e11) % 11.92/3.23 | (771) all_0_127_127 = e12 | all_0_127_127 = e10 % 11.92/3.23 | % 11.92/3.23 +-Applying beta-rule and splitting (771), into two cases. % 11.92/3.23 |-Branch one: % 11.92/3.23 | (772) all_0_127_127 = e12 % 11.92/3.23 | % 11.92/3.23 | Equations (772) can reduce 562 to: % 11.92/3.23 | (367) $false % 11.92/3.23 | % 11.92/3.23 |-The branch is then unsatisfiable % 11.92/3.23 |-Branch two: % 11.92/3.23 | (562) ~ (all_0_127_127 = e12) % 11.92/3.23 | (669) all_0_127_127 = e10 % 11.92/3.23 | % 11.92/3.23 | Equations (669) can reduce 91 to: % 11.92/3.23 | (927) ~ (all_0_128_128 = e10) % 11.92/3.23 | % 11.92/3.23 | Simplifying 927 yields: % 11.92/3.23 | (928) ~ (all_0_128_128 = e10) % 11.92/3.23 | % 11.92/3.23 +-Applying beta-rule and splitting (53), into two cases. % 11.92/3.23 |-Branch one: % 11.92/3.23 | (672) all_0_128_128 = e10 % 11.92/3.23 | % 11.92/3.23 | Equations (672) can reduce 928 to: % 11.92/3.23 | (367) $false % 11.92/3.23 | % 11.92/3.23 |-The branch is then unsatisfiable % 11.92/3.23 |-Branch two: % 11.92/3.23 | (928) ~ (all_0_128_128 = e10) % 11.92/3.23 | (932) all_0_131_131 = e10 % 11.92/3.23 | % 11.92/3.23 | Equations (932) can reduce 98 to: % 11.92/3.23 | (933) ~ (all_0_134_134 = e10) % 11.92/3.23 | % 11.92/3.23 | Simplifying 933 yields: % 11.92/3.23 | (166) ~ (all_0_134_134 = e10) % 11.92/3.23 | % 11.92/3.23 +-Applying beta-rule and splitting (61), into two cases. % 11.92/3.23 |-Branch one: % 11.92/3.23 | (601) all_0_134_134 = e11 % 11.92/3.23 | % 11.92/3.23 | Equations (601) can reduce 576 to: % 11.92/3.23 | (612) ~ (e13 = e11) % 11.92/3.23 | % 11.92/3.23 | Simplifying 612 yields: % 11.92/3.23 | (347) ~ (e13 = e11) % 11.92/3.23 | % 11.92/3.23 | Equations (601) can reduce 822 to: % 11.92/3.23 | (678) ~ (e12 = e11) % 11.92/3.23 | % 11.92/3.23 | Simplifying 678 yields: % 11.92/3.23 | (60) ~ (e12 = e11) % 11.92/3.23 | % 11.92/3.23 | Equations (601) can reduce 166 to: % 11.92/3.23 | (223) ~ (e11 = e10) % 11.92/3.23 | % 11.92/3.23 +-Applying beta-rule and splitting (144), into two cases. % 11.92/3.23 |-Branch one: % 11.92/3.23 | (642) all_0_125_125 = e12 % 11.92/3.23 | % 11.92/3.24 | Combining equations (642,582) yields a new equation: % 11.92/3.24 | (639) e13 = e12 % 11.92/3.24 | % 11.92/3.24 | Equations (639) can reduce 276 to: % 11.92/3.24 | (367) $false % 11.92/3.24 | % 11.92/3.24 |-The branch is then unsatisfiable % 11.92/3.24 |-Branch two: % 11.92/3.24 | (894) ~ (all_0_125_125 = e12) % 11.92/3.24 | (945) all_0_128_128 = e12 | all_0_134_134 = e12 % 11.92/3.24 | % 11.92/3.24 | Equations (582) can reduce 894 to: % 11.92/3.24 | (276) ~ (e13 = e12) % 11.92/3.24 | % 11.92/3.24 +-Applying beta-rule and splitting (268), into two cases. % 11.92/3.24 |-Branch one: % 11.92/3.24 | (615) (all_0_124_124 = e13 & all_0_134_134 = e12) | (all_0_124_124 = e13 & ~ (all_0_130_130 = e11)) | (all_0_126_126 = e12 & all_0_134_134 = e13) | (all_0_127_127 = e11 & ~ (all_0_134_134 = e11)) | (all_0_127_127 = e10 & all_0_131_131 = e11 & ~ (all_0_128_128 = e12)) | (all_0_128_128 = e12 & ~ (all_0_125_125 = e13) & ~ (all_0_127_127 = e10)) | (all_0_129_129 = e11 & all_0_134_134 = e13) % 11.92/3.24 | % 11.92/3.24 +-Applying beta-rule and splitting (615), into two cases. % 11.92/3.24 |-Branch one: % 11.92/3.24 | (616) (all_0_124_124 = e13 & all_0_134_134 = e12) | (all_0_124_124 = e13 & ~ (all_0_130_130 = e11)) | (all_0_126_126 = e12 & all_0_134_134 = e13) | (all_0_127_127 = e11 & ~ (all_0_134_134 = e11)) | (all_0_127_127 = e10 & all_0_131_131 = e11 & ~ (all_0_128_128 = e12)) | (all_0_128_128 = e12 & ~ (all_0_125_125 = e13) & ~ (all_0_127_127 = e10)) % 11.92/3.24 | % 11.92/3.24 +-Applying beta-rule and splitting (616), into two cases. % 11.92/3.24 |-Branch one: % 11.92/3.24 | (617) (all_0_124_124 = e13 & all_0_134_134 = e12) | (all_0_124_124 = e13 & ~ (all_0_130_130 = e11)) | (all_0_126_126 = e12 & all_0_134_134 = e13) | (all_0_127_127 = e11 & ~ (all_0_134_134 = e11)) | (all_0_127_127 = e10 & all_0_131_131 = e11 & ~ (all_0_128_128 = e12)) % 11.92/3.24 | % 11.92/3.24 +-Applying beta-rule and splitting (617), into two cases. % 11.92/3.24 |-Branch one: % 11.92/3.24 | (618) (all_0_124_124 = e13 & all_0_134_134 = e12) | (all_0_124_124 = e13 & ~ (all_0_130_130 = e11)) | (all_0_126_126 = e12 & all_0_134_134 = e13) | (all_0_127_127 = e11 & ~ (all_0_134_134 = e11)) % 11.92/3.24 | % 11.92/3.24 +-Applying beta-rule and splitting (618), into two cases. % 11.92/3.24 |-Branch one: % 11.92/3.24 | (619) (all_0_124_124 = e13 & all_0_134_134 = e12) | (all_0_124_124 = e13 & ~ (all_0_130_130 = e11)) | (all_0_126_126 = e12 & all_0_134_134 = e13) % 11.92/3.24 | % 11.92/3.24 +-Applying beta-rule and splitting (619), into two cases. % 11.92/3.24 |-Branch one: % 11.92/3.24 | (620) (all_0_124_124 = e13 & all_0_134_134 = e12) | (all_0_124_124 = e13 & ~ (all_0_130_130 = e11)) % 11.92/3.24 | % 11.92/3.24 +-Applying beta-rule and splitting (620), into two cases. % 11.92/3.24 |-Branch one: % 11.92/3.24 | (621) all_0_124_124 = e13 & all_0_134_134 = e12 % 11.92/3.24 | % 11.92/3.24 | Applying alpha-rule on (621) yields: % 11.92/3.24 | (622) all_0_124_124 = e13 % 11.92/3.24 | (623) all_0_134_134 = e12 % 11.92/3.24 | % 11.92/3.24 | Combining equations (623,601) yields a new equation: % 11.92/3.24 | (594) e12 = e11 % 11.92/3.24 | % 11.92/3.24 | Simplifying 594 yields: % 11.92/3.24 | (595) e12 = e11 % 11.92/3.24 | % 11.92/3.24 | Equations (595) can reduce 60 to: % 11.92/3.24 | (367) $false % 11.92/3.24 | % 11.92/3.24 |-The branch is then unsatisfiable % 11.92/3.24 |-Branch two: % 11.92/3.24 | (627) all_0_124_124 = e13 & ~ (all_0_130_130 = e11) % 11.92/3.24 | % 11.92/3.24 | Applying alpha-rule on (627) yields: % 11.92/3.24 | (622) all_0_124_124 = e13 % 11.92/3.24 | (555) ~ (all_0_130_130 = e11) % 11.92/3.24 | % 11.92/3.24 | Combining equations (622,637) yields a new equation: % 11.92/3.24 | (638) e13 = e12 % 11.92/3.24 | % 11.92/3.24 | Simplifying 638 yields: % 11.92/3.24 | (639) e13 = e12 % 11.92/3.24 | % 11.92/3.24 | Equations (639) can reduce 276 to: % 11.92/3.24 | (367) $false % 11.92/3.24 | % 11.92/3.24 |-The branch is then unsatisfiable % 11.92/3.24 |-Branch two: % 11.92/3.24 | (777) all_0_126_126 = e12 & all_0_134_134 = e13 % 11.92/3.24 | % 11.92/3.24 | Applying alpha-rule on (777) yields: % 11.92/3.24 | (560) all_0_126_126 = e12 % 11.92/3.24 | (762) all_0_134_134 = e13 % 11.92/3.24 | % 11.92/3.24 | Combining equations (560,557) yields a new equation: % 11.92/3.24 | (594) e12 = e11 % 11.92/3.24 | % 11.92/3.24 | Simplifying 594 yields: % 11.92/3.24 | (595) e12 = e11 % 11.92/3.24 | % 11.92/3.24 | Equations (595) can reduce 60 to: % 11.92/3.24 | (367) $false % 11.92/3.24 | % 11.92/3.24 |-The branch is then unsatisfiable % 11.92/3.24 |-Branch two: % 11.92/3.24 | (783) all_0_127_127 = e11 & ~ (all_0_134_134 = e11) % 11.92/3.24 | % 11.92/3.24 | Applying alpha-rule on (783) yields: % 11.92/3.24 | (675) all_0_127_127 = e11 % 11.92/3.24 | (785) ~ (all_0_134_134 = e11) % 11.92/3.24 | % 11.92/3.24 | Combining equations (669,675) yields a new equation: % 11.92/3.24 | (974) e11 = e10 % 11.92/3.24 | % 11.92/3.24 | Equations (974) can reduce 223 to: % 11.92/3.24 | (367) $false % 11.92/3.24 | % 11.92/3.24 |-The branch is then unsatisfiable % 11.92/3.24 |-Branch two: % 11.92/3.24 | (787) all_0_127_127 = e10 & all_0_131_131 = e11 & ~ (all_0_128_128 = e12) % 11.92/3.24 | % 11.92/3.24 | Applying alpha-rule on (787) yields: % 11.92/3.24 | (669) all_0_127_127 = e10 % 11.92/3.24 | (789) all_0_131_131 = e11 % 11.92/3.24 | (564) ~ (all_0_128_128 = e12) % 11.92/3.24 | % 11.92/3.24 | Combining equations (932,789) yields a new equation: % 11.92/3.24 | (974) e11 = e10 % 11.92/3.24 | % 11.92/3.24 | Equations (974) can reduce 223 to: % 11.92/3.24 | (367) $false % 11.92/3.24 | % 11.92/3.24 |-The branch is then unsatisfiable % 11.92/3.24 |-Branch two: % 11.92/3.24 | (792) all_0_128_128 = e12 & ~ (all_0_125_125 = e13) & ~ (all_0_127_127 = e10) % 11.92/3.24 | % 11.92/3.24 | Applying alpha-rule on (792) yields: % 11.92/3.24 | (793) all_0_128_128 = e12 % 11.92/3.24 | (631) ~ (all_0_125_125 = e13) % 11.92/3.24 | (667) ~ (all_0_127_127 = e10) % 11.92/3.24 | % 11.92/3.24 | Equations (669) can reduce 667 to: % 11.92/3.24 | (367) $false % 11.92/3.24 | % 11.92/3.24 |-The branch is then unsatisfiable % 11.92/3.24 |-Branch two: % 11.92/3.24 | (797) all_0_129_129 = e11 & all_0_134_134 = e13 % 11.92/3.24 | % 11.92/3.24 | Applying alpha-rule on (797) yields: % 11.92/3.24 | (552) all_0_129_129 = e11 % 11.92/3.24 | (762) all_0_134_134 = e13 % 11.92/3.24 | % 11.92/3.24 | Combining equations (601,762) yields a new equation: % 11.92/3.24 | (571) e13 = e11 % 11.92/3.24 | % 11.92/3.24 | Equations (571) can reduce 347 to: % 11.92/3.24 | (367) $false % 11.92/3.24 | % 11.92/3.24 |-The branch is then unsatisfiable % 11.92/3.24 |-Branch two: % 11.92/3.24 | (802) all_0_131_131 = e11 & ~ (all_0_125_125 = e13) % 11.92/3.24 | % 11.92/3.24 | Applying alpha-rule on (802) yields: % 11.92/3.24 | (789) all_0_131_131 = e11 % 11.92/3.24 | (631) ~ (all_0_125_125 = e13) % 11.92/3.24 | % 11.92/3.24 | Combining equations (932,789) yields a new equation: % 11.92/3.24 | (974) e11 = e10 % 11.92/3.25 | % 11.92/3.25 | Equations (974) can reduce 223 to: % 11.92/3.25 | (367) $false % 11.92/3.25 | % 11.92/3.25 |-The branch is then unsatisfiable % 11.92/3.25 |-Branch two: % 11.92/3.25 | (785) ~ (all_0_134_134 = e11) % 11.92/3.25 | (849) all_0_134_134 = e13 | all_0_134_134 = e12 % 11.92/3.25 | % 11.92/3.25 +-Applying beta-rule and splitting (144), into two cases. % 11.92/3.25 |-Branch one: % 11.92/3.25 | (642) all_0_125_125 = e12 % 11.92/3.25 | % 11.92/3.25 | Combining equations (642,582) yields a new equation: % 11.92/3.25 | (639) e13 = e12 % 11.92/3.25 | % 11.92/3.25 | Equations (639) can reduce 276 to: % 11.92/3.25 | (367) $false % 11.92/3.25 | % 11.92/3.25 |-The branch is then unsatisfiable % 11.92/3.25 |-Branch two: % 11.92/3.25 | (894) ~ (all_0_125_125 = e12) % 11.92/3.25 | (945) all_0_128_128 = e12 | all_0_134_134 = e12 % 11.92/3.25 | % 11.92/3.25 +-Applying beta-rule and splitting (945), into two cases. % 11.92/3.25 |-Branch one: % 11.92/3.25 | (793) all_0_128_128 = e12 % 11.92/3.25 | % 11.92/3.25 | Equations (793) can reduce 9 to: % 11.92/3.25 | (821) ~ (all_0_134_134 = e12) % 11.92/3.25 | % 11.92/3.25 | Simplifying 821 yields: % 11.92/3.25 | (822) ~ (all_0_134_134 = e12) % 11.92/3.25 | % 11.92/3.25 +-Applying beta-rule and splitting (849), into two cases. % 11.92/3.25 |-Branch one: % 11.92/3.25 | (762) all_0_134_134 = e13 % 11.92/3.25 | % 11.92/3.25 | Equations (762) can reduce 576 to: % 11.92/3.25 | (367) $false % 11.92/3.25 | % 11.92/3.25 |-The branch is then unsatisfiable % 11.92/3.25 |-Branch two: % 11.92/3.25 | (576) ~ (all_0_134_134 = e13) % 11.92/3.25 | (623) all_0_134_134 = e12 % 11.92/3.25 | % 11.92/3.25 | Equations (623) can reduce 822 to: % 11.92/3.25 | (367) $false % 11.92/3.25 | % 11.92/3.25 |-The branch is then unsatisfiable % 11.92/3.25 |-Branch two: % 11.92/3.25 | (564) ~ (all_0_128_128 = e12) % 11.92/3.25 | (623) all_0_134_134 = e12 % 11.92/3.25 | % 11.92/3.25 | Equations (623) can reduce 822 to: % 11.92/3.25 | (367) $false % 11.92/3.25 | % 11.92/3.25 |-The branch is then unsatisfiable % 11.92/3.25 |-Branch two: % 11.92/3.25 | (831) ~ (all_0_133_133 = e13) % 11.92/3.25 | (762) all_0_134_134 = e13 % 11.92/3.25 | % 11.92/3.25 | Equations (762) can reduce 576 to: % 11.92/3.25 | (367) $false % 11.92/3.25 | % 11.92/3.25 |-The branch is then unsatisfiable % 11.92/3.25 |-Branch two: % 11.92/3.25 | (553) ~ (all_0_126_126 = e11) % 11.92/3.25 | (560) all_0_126_126 = e12 % 11.92/3.25 | % 11.92/3.25 | Equations (560) can reduce 196 to: % 11.92/3.25 | (565) ~ (all_0_132_132 = e12) % 11.92/3.25 | % 11.92/3.25 | Simplifying 565 yields: % 11.92/3.25 | (566) ~ (all_0_132_132 = e12) % 11.92/3.25 | % 11.92/3.25 | Equations (560) can reduce 553 to: % 11.92/3.25 | (60) ~ (e12 = e11) % 11.92/3.25 | % 11.92/3.25 +-Applying beta-rule and splitting (153), into two cases. % 11.92/3.25 |-Branch one: % 11.92/3.25 | (557) all_0_126_126 = e11 % 11.92/3.25 | % 11.92/3.25 | Combining equations (560,557) yields a new equation: % 11.92/3.25 | (594) e12 = e11 % 11.92/3.25 | % 11.92/3.25 | Simplifying 594 yields: % 11.92/3.25 | (595) e12 = e11 % 11.92/3.25 | % 11.92/3.25 | Equations (595) can reduce 60 to: % 11.92/3.25 | (367) $false % 11.92/3.25 | % 11.92/3.25 |-The branch is then unsatisfiable % 11.92/3.25 |-Branch two: % 11.92/3.25 | (553) ~ (all_0_126_126 = e11) % 11.92/3.25 | (1028) all_0_129_129 = e11 | all_0_132_132 = e11 % 11.92/3.25 | % 11.92/3.25 +-Applying beta-rule and splitting (288), into two cases. % 11.92/3.25 |-Branch one: % 11.92/3.25 | (1029) all_0_132_132 = e11 % 11.92/3.25 | % 11.92/3.25 | Equations (1029) can reduce 65 to: % 11.92/3.25 | (842) ~ (all_0_134_134 = e11) % 11.92/3.25 | % 11.92/3.25 | Simplifying 842 yields: % 11.92/3.25 | (785) ~ (all_0_134_134 = e11) % 11.92/3.25 | % 11.92/3.25 | Equations (1029) can reduce 566 to: % 11.92/3.25 | (678) ~ (e12 = e11) % 11.92/3.25 | % 11.92/3.25 | Simplifying 678 yields: % 11.92/3.25 | (60) ~ (e12 = e11) % 11.92/3.25 | % 11.92/3.25 +-Applying beta-rule and splitting (87), into two cases. % 11.92/3.25 |-Branch one: % 11.92/3.25 | (579) (all_0_102_102 = e12 & all_0_103_103 = e10 & all_0_125_125 = e13 & ~ (all_0_126_126 = e12) & ~ (all_0_129_129 = e11)) | (all_0_104_104 = e13 & all_0_105_105 = e12 & all_0_106_106 = e10 & all_0_126_126 = e11 & ~ (all_0_124_124 = e13)) | (all_0_107_107 = e13 & all_0_108_108 = e12 & all_0_109_109 = e10 & all_0_130_130 = e11 & all_0_134_134 = e11) % 11.92/3.25 | % 11.92/3.25 +-Applying beta-rule and splitting (579), into two cases. % 11.92/3.25 |-Branch one: % 11.92/3.25 | (580) (all_0_102_102 = e12 & all_0_103_103 = e10 & all_0_125_125 = e13 & ~ (all_0_126_126 = e12) & ~ (all_0_129_129 = e11)) | (all_0_104_104 = e13 & all_0_105_105 = e12 & all_0_106_106 = e10 & all_0_126_126 = e11 & ~ (all_0_124_124 = e13)) % 11.92/3.25 | % 11.92/3.25 +-Applying beta-rule and splitting (580), into two cases. % 11.92/3.25 |-Branch one: % 11.92/3.25 | (581) all_0_102_102 = e12 & all_0_103_103 = e10 & all_0_125_125 = e13 & ~ (all_0_126_126 = e12) & ~ (all_0_129_129 = e11) % 11.92/3.25 | % 11.92/3.25 | Applying alpha-rule on (581) yields: % 11.92/3.25 | (582) all_0_125_125 = e13 % 11.92/3.25 | (583) ~ (all_0_129_129 = e11) % 11.92/3.25 | (584) all_0_102_102 = e12 % 11.92/3.25 | (585) ~ (all_0_126_126 = e12) % 11.92/3.25 | (586) all_0_103_103 = e10 % 11.92/3.25 | % 11.92/3.25 | Equations (560) can reduce 585 to: % 11.92/3.25 | (367) $false % 11.92/3.25 | % 11.92/3.25 |-The branch is then unsatisfiable % 11.92/3.25 |-Branch two: % 11.92/3.25 | (588) all_0_104_104 = e13 & all_0_105_105 = e12 & all_0_106_106 = e10 & all_0_126_126 = e11 & ~ (all_0_124_124 = e13) % 11.92/3.25 | % 11.92/3.25 | Applying alpha-rule on (588) yields: % 11.92/3.25 | (589) ~ (all_0_124_124 = e13) % 11.92/3.25 | (557) all_0_126_126 = e11 % 11.92/3.25 | (591) all_0_104_104 = e13 % 11.92/3.25 | (592) all_0_106_106 = e10 % 11.92/3.25 | (593) all_0_105_105 = e12 % 11.92/3.26 | % 11.92/3.26 | Combining equations (557,560) yields a new equation: % 11.92/3.26 | (595) e12 = e11 % 11.92/3.26 | % 11.92/3.26 | Equations (595) can reduce 60 to: % 11.92/3.26 | (367) $false % 11.92/3.26 | % 11.92/3.26 |-The branch is then unsatisfiable % 11.92/3.26 |-Branch two: % 11.92/3.26 | (597) all_0_107_107 = e13 & all_0_108_108 = e12 & all_0_109_109 = e10 & all_0_130_130 = e11 & all_0_134_134 = e11 % 11.92/3.26 | % 11.92/3.26 | Applying alpha-rule on (597) yields: % 11.92/3.26 | (598) all_0_130_130 = e11 % 11.92/3.26 | (599) all_0_107_107 = e13 % 11.92/3.26 | (600) all_0_108_108 = e12 % 11.92/3.26 | (601) all_0_134_134 = e11 % 11.92/3.26 | (602) all_0_109_109 = e10 % 11.92/3.26 | % 11.92/3.26 | Equations (601) can reduce 785 to: % 11.92/3.26 | (367) $false % 11.92/3.26 | % 11.92/3.26 |-The branch is then unsatisfiable % 11.92/3.26 |-Branch two: % 11.92/3.26 | (604) all_0_110_110 = e13 & all_0_111_111 = e12 & all_0_112_112 = e10 & all_0_134_134 = e11 & ~ (all_0_131_131 = e11) & ( ~ (all_0_128_128 = e12) | all_0_127_127 = e10) % 11.92/3.26 | % 11.92/3.26 | Applying alpha-rule on (604) yields: % 11.92/3.26 | (605) ~ (all_0_131_131 = e11) % 11.92/3.26 | (606) all_0_111_111 = e12 % 11.92/3.26 | (607) all_0_110_110 = e13 % 11.92/3.26 | (601) all_0_134_134 = e11 % 11.92/3.26 | (609) all_0_112_112 = e10 % 11.92/3.26 | (610) ~ (all_0_128_128 = e12) | all_0_127_127 = e10 % 11.92/3.26 | % 11.92/3.26 | Equations (601) can reduce 785 to: % 11.92/3.26 | (367) $false % 11.92/3.26 | % 11.92/3.26 |-The branch is then unsatisfiable % 11.92/3.26 |-Branch two: % 11.92/3.26 | (1066) ~ (all_0_132_132 = e11) % 11.92/3.26 | (1067) all_0_132_132 = e13 | all_0_132_132 = e12 % 11.92/3.26 | % 11.92/3.26 +-Applying beta-rule and splitting (1028), into two cases. % 11.92/3.26 |-Branch one: % 11.92/3.26 | (552) all_0_129_129 = e11 % 11.92/3.26 | % 11.92/3.26 | Combining equations (552,569) yields a new equation: % 11.92/3.26 | (571) e13 = e11 % 11.92/3.26 | % 11.92/3.26 | Equations (571) can reduce 347 to: % 11.92/3.26 | (367) $false % 11.92/3.26 | % 11.92/3.26 |-The branch is then unsatisfiable % 11.92/3.26 |-Branch two: % 11.92/3.26 | (583) ~ (all_0_129_129 = e11) % 11.92/3.26 | (1029) all_0_132_132 = e11 % 11.92/3.26 | % 11.92/3.26 | Equations (1029) can reduce 1066 to: % 11.92/3.26 | (367) $false % 11.92/3.26 | % 11.92/3.26 |-The branch is then unsatisfiable % 11.92/3.26 |-Branch two: % 11.92/3.26 | (436) ~ (all_0_118_118 = e21) % 11.92/3.26 | (408) all_0_118_118 = e23 % 11.92/3.26 | % 11.92/3.26 | Equations (408) can reduce 474 to: % 11.92/3.26 | (367) $false % 11.92/3.26 | % 11.92/3.26 |-The branch is then unsatisfiable % 11.92/3.26 |-Branch two: % 11.92/3.26 | (1077) ~ (all_0_120_120 = e23) % 11.92/3.26 | (396) all_0_120_120 = e20 % 11.92/3.26 | % 11.92/3.26 | Equations (396) can reduce 491 to: % 11.92/3.26 | (367) $false % 11.92/3.26 | % 11.92/3.26 |-The branch is then unsatisfiable % 11.92/3.26 |-Branch two: % 11.92/3.26 | (403) ~ (all_0_116_116 = e21) % 11.92/3.26 | (404) all_0_119_119 = e21 | all_0_122_122 = e21 % 11.92/3.26 | % 11.92/3.26 +-Applying beta-rule and splitting (404), into two cases. % 11.92/3.26 |-Branch one: % 11.92/3.26 | (405) all_0_119_119 = e21 % 11.92/3.26 | % 11.92/3.26 | Combining equations (405,393) yields a new equation: % 11.92/3.26 | (529) e21 = e20 % 11.92/3.26 | % 11.92/3.26 | Simplifying 529 yields: % 11.92/3.26 | (401) e21 = e20 % 11.92/3.26 | % 11.92/3.26 | Equations (401) can reduce 140 to: % 11.92/3.26 | (367) $false % 11.92/3.26 | % 11.92/3.26 |-The branch is then unsatisfiable % 11.92/3.26 |-Branch two: % 11.92/3.26 | (484) ~ (all_0_119_119 = e21) % 11.92/3.26 | (485) all_0_122_122 = e21 % 11.92/3.26 | % 11.92/3.26 | Combining equations (485,384) yields a new equation: % 11.92/3.26 | (451) e22 = e21 % 11.92/3.26 | % 11.92/3.26 | Equations (451) can reduce 282 to: % 11.92/3.26 | (367) $false % 11.92/3.26 | % 11.92/3.26 |-The branch is then unsatisfiable % 11.92/3.26 |-Branch two: % 11.92/3.26 | (390) ~ (all_0_119_119 = e20) % 11.92/3.26 | (396) all_0_120_120 = e20 % 11.92/3.26 | % 11.92/3.26 | Equations (396) can reduce 491 to: % 11.92/3.26 | (367) $false % 11.92/3.26 | % 11.92/3.26 |-The branch is then unsatisfiable % 11.92/3.26 |-Branch two: % 11.92/3.26 | (1093) ~ (all_0_114_114 = e22) % 11.92/3.26 | (434) all_0_114_114 = e23 % 11.92/3.26 | % 11.92/3.26 | Equations (434) can reduce 206 to: % 11.92/3.26 | (445) ~ (all_0_113_113 = e23) % 11.92/3.26 | % 11.92/3.26 +-Applying beta-rule and splitting (197), into two cases. % 11.92/3.26 |-Branch one: % 11.92/3.26 | (366) all_0_113_113 = e22 % 11.92/3.26 | % 11.92/3.26 | Equations (366) can reduce 445 to: % 11.92/3.26 | (1097) ~ (e23 = e22) % 11.92/3.26 | % 11.92/3.26 | Simplifying 1097 yields: % 11.92/3.26 | (165) ~ (e23 = e22) % 11.92/3.26 | % 11.92/3.26 | Equations (366) can reduce 219 to: % 11.92/3.26 | (282) ~ (e22 = e21) % 11.92/3.26 | % 11.92/3.26 +-Applying beta-rule and splitting (270), into two cases. % 11.92/3.26 |-Branch one: % 11.92/3.26 | (358) all_0_114_114 = e22 % 11.92/3.26 | % 11.92/3.26 | Combining equations (358,434) yields a new equation: % 11.92/3.26 | (377) e23 = e22 % 11.92/3.26 | % 11.92/3.26 | Equations (377) can reduce 165 to: % 11.92/3.26 | (367) $false % 11.92/3.26 | % 11.92/3.26 |-The branch is then unsatisfiable % 11.92/3.26 |-Branch two: % 11.92/3.26 | (1093) ~ (all_0_114_114 = e22) % 11.92/3.26 | (1104) all_0_117_117 = e22 | all_0_123_123 = e22 % 11.92/3.26 | % 11.92/3.26 +-Applying beta-rule and splitting (1104), into two cases. % 11.92/3.26 |-Branch one: % 11.92/3.26 | (422) all_0_117_117 = e22 % 11.92/3.26 | % 11.92/3.26 | Equations (422) can reduce 355 to: % 11.92/3.26 | (367) $false % 11.92/3.26 | % 11.92/3.26 |-The branch is then unsatisfiable % 11.92/3.26 |-Branch two: % 11.92/3.26 | (355) ~ (all_0_117_117 = e22) % 11.92/3.27 | (1108) all_0_123_123 = e22 % 11.92/3.27 | % 11.92/3.27 +-Applying beta-rule and splitting (32), into two cases. % 11.92/3.27 |-Branch one: % 11.92/3.27 | (431) (all_0_91_91 = e22 & all_0_92_92 = e20 & all_0_114_114 = e23 & ~ (all_0_115_115 = e22) & ~ (all_0_118_118 = e21)) | (all_0_93_93 = e23 & all_0_94_94 = e22 & all_0_95_95 = e20 & all_0_115_115 = e21 & ~ (all_0_113_113 = e23)) | (all_0_96_96 = e23 & all_0_97_97 = e22 & all_0_98_98 = e20 & all_0_119_119 = e21 & all_0_123_123 = e21) % 11.92/3.27 | % 11.92/3.27 +-Applying beta-rule and splitting (431), into two cases. % 11.92/3.27 |-Branch one: % 11.92/3.27 | (432) (all_0_91_91 = e22 & all_0_92_92 = e20 & all_0_114_114 = e23 & ~ (all_0_115_115 = e22) & ~ (all_0_118_118 = e21)) | (all_0_93_93 = e23 & all_0_94_94 = e22 & all_0_95_95 = e20 & all_0_115_115 = e21 & ~ (all_0_113_113 = e23)) % 11.92/3.27 | % 11.92/3.27 +-Applying beta-rule and splitting (432), into two cases. % 11.92/3.27 |-Branch one: % 11.92/3.27 | (433) all_0_91_91 = e22 & all_0_92_92 = e20 & all_0_114_114 = e23 & ~ (all_0_115_115 = e22) & ~ (all_0_118_118 = e21) % 11.92/3.27 | % 11.92/3.27 | Applying alpha-rule on (433) yields: % 11.92/3.27 | (434) all_0_114_114 = e23 % 11.92/3.27 | (435) ~ (all_0_115_115 = e22) % 11.92/3.27 | (436) ~ (all_0_118_118 = e21) % 11.92/3.27 | (437) all_0_92_92 = e20 % 11.92/3.27 | (438) all_0_91_91 = e22 % 11.92/3.27 | % 11.92/3.27 | Equations (351) can reduce 435 to: % 11.92/3.27 | (367) $false % 11.92/3.27 | % 11.92/3.27 |-The branch is then unsatisfiable % 11.92/3.27 |-Branch two: % 11.92/3.27 | (444) all_0_93_93 = e23 & all_0_94_94 = e22 & all_0_95_95 = e20 & all_0_115_115 = e21 & ~ (all_0_113_113 = e23) % 11.92/3.27 | % 11.92/3.27 | Applying alpha-rule on (444) yields: % 11.92/3.27 | (445) ~ (all_0_113_113 = e23) % 11.92/3.27 | (446) all_0_93_93 = e23 % 11.92/3.27 | (447) all_0_94_94 = e22 % 11.92/3.27 | (448) all_0_115_115 = e21 % 11.92/3.27 | (449) all_0_95_95 = e20 % 11.92/3.27 | % 12.20/3.27 | Combining equations (351,448) yields a new equation: % 12.20/3.27 | (450) e22 = e21 % 12.20/3.27 | % 12.20/3.27 | Simplifying 450 yields: % 12.20/3.27 | (451) e22 = e21 % 12.20/3.27 | % 12.20/3.27 | Equations (451) can reduce 282 to: % 12.20/3.27 | (367) $false % 12.20/3.27 | % 12.20/3.27 |-The branch is then unsatisfiable % 12.20/3.27 |-Branch two: % 12.20/3.27 | (453) all_0_96_96 = e23 & all_0_97_97 = e22 & all_0_98_98 = e20 & all_0_119_119 = e21 & all_0_123_123 = e21 % 12.20/3.27 | % 12.20/3.27 | Applying alpha-rule on (453) yields: % 12.20/3.27 | (454) all_0_123_123 = e21 % 12.20/3.27 | (455) all_0_98_98 = e20 % 12.20/3.27 | (456) all_0_96_96 = e23 % 12.20/3.27 | (457) all_0_97_97 = e22 % 12.20/3.27 | (405) all_0_119_119 = e21 % 12.20/3.27 | % 12.20/3.27 | Combining equations (1108,454) yields a new equation: % 12.20/3.27 | (450) e22 = e21 % 12.20/3.27 | % 12.20/3.27 | Simplifying 450 yields: % 12.20/3.27 | (451) e22 = e21 % 12.20/3.27 | % 12.20/3.27 | Equations (451) can reduce 282 to: % 12.20/3.27 | (367) $false % 12.20/3.27 | % 12.20/3.27 |-The branch is then unsatisfiable % 12.20/3.27 |-Branch two: % 12.20/3.27 | (462) all_0_99_99 = e23 & all_0_100_100 = e22 & all_0_101_101 = e20 & all_0_123_123 = e21 & ~ (all_0_120_120 = e21) & ( ~ (all_0_117_117 = e22) | all_0_116_116 = e20) % 12.20/3.27 | % 12.20/3.27 | Applying alpha-rule on (462) yields: % 12.20/3.27 | (454) all_0_123_123 = e21 % 12.20/3.27 | (464) ~ (all_0_120_120 = e21) % 12.20/3.27 | (465) all_0_100_100 = e22 % 12.20/3.27 | (466) ~ (all_0_117_117 = e22) | all_0_116_116 = e20 % 12.20/3.27 | (467) all_0_101_101 = e20 % 12.20/3.27 | (468) all_0_99_99 = e23 % 12.20/3.27 | % 12.20/3.27 | Combining equations (454,1108) yields a new equation: % 12.20/3.27 | (451) e22 = e21 % 12.20/3.27 | % 12.20/3.27 | Equations (451) can reduce 282 to: % 12.20/3.27 | (367) $false % 12.20/3.27 | % 12.20/3.27 |-The branch is then unsatisfiable % 12.20/3.27 |-Branch two: % 12.20/3.27 | (359) ~ (all_0_113_113 = e22) % 12.20/3.27 | (369) all_0_113_113 = e23 % 12.20/3.27 | % 12.20/3.27 | Equations (369) can reduce 445 to: % 12.20/3.27 | (367) $false % 12.20/3.27 | % 12.20/3.27 |-The branch is then unsatisfiable % 12.20/3.27 |-Branch two: % 12.20/3.27 | (435) ~ (all_0_115_115 = e22) % 12.20/3.27 | (1149) all_0_121_121 = e22 % 12.20/3.27 | % 12.20/3.27 | Equations (1149) can reduce 25 to: % 12.20/3.27 | (435) ~ (all_0_115_115 = e22) % 12.20/3.27 | % 12.20/3.27 | Equations (1149) can reduce 47 to: % 12.20/3.27 | (1151) ~ (all_0_122_122 = e22) % 12.20/3.27 | % 12.20/3.27 | Simplifying 1151 yields: % 12.20/3.27 | (1152) ~ (all_0_122_122 = e22) % 12.20/3.27 | % 12.20/3.27 +-Applying beta-rule and splitting (94), into two cases. % 12.20/3.27 |-Branch one: % 12.20/3.27 | (351) all_0_115_115 = e22 % 12.20/3.27 | % 12.20/3.27 | Equations (351) can reduce 435 to: % 12.20/3.27 | (367) $false % 12.20/3.27 | % 12.20/3.27 |-The branch is then unsatisfiable % 12.20/3.27 |-Branch two: % 12.20/3.27 | (435) ~ (all_0_115_115 = e22) % 12.20/3.27 | (448) all_0_115_115 = e21 % 12.20/3.27 | % 12.20/3.27 | Equations (448) can reduce 44 to: % 12.20/3.27 | (1157) ~ (all_0_116_116 = e21) % 12.20/3.27 | % 12.20/3.27 | Simplifying 1157 yields: % 12.20/3.27 | (403) ~ (all_0_116_116 = e21) % 12.20/3.27 | % 12.20/3.27 +-Applying beta-rule and splitting (99), into two cases. % 12.20/3.27 |-Branch one: % 12.20/3.27 | (408) all_0_118_118 = e23 % 12.20/3.27 | % 12.20/3.27 | Equations (408) can reduce 264 to: % 12.20/3.27 | (372) ~ (all_0_119_119 = e23) % 12.20/3.27 | % 12.20/3.27 | Simplifying 372 yields: % 12.20/3.27 | (373) ~ (all_0_119_119 = e23) % 12.20/3.27 | % 12.20/3.27 +-Applying beta-rule and splitting (197), into two cases. % 12.20/3.27 |-Branch one: % 12.20/3.27 | (366) all_0_113_113 = e22 % 12.20/3.27 | % 12.20/3.27 | Equations (366) can reduce 206 to: % 12.20/3.27 | (1163) ~ (all_0_114_114 = e22) % 12.20/3.27 | % 12.20/3.27 | Simplifying 1163 yields: % 12.20/3.27 | (1093) ~ (all_0_114_114 = e22) % 12.20/3.27 | % 12.20/3.27 | Equations (366) can reduce 219 to: % 12.20/3.27 | (282) ~ (e22 = e21) % 12.20/3.27 | % 12.20/3.27 +-Applying beta-rule and splitting (169), into two cases. % 12.20/3.27 |-Branch one: % 12.20/3.27 | (358) all_0_114_114 = e22 % 12.20/3.27 | % 12.20/3.27 | Equations (358) can reduce 1093 to: % 12.20/3.27 | (367) $false % 12.20/3.27 | % 12.20/3.27 |-The branch is then unsatisfiable % 12.20/3.27 |-Branch two: % 12.20/3.27 | (1093) ~ (all_0_114_114 = e22) % 12.20/3.27 | (434) all_0_114_114 = e23 % 12.20/3.27 | % 12.20/3.28 | Equations (434) can reduce 1093 to: % 12.20/3.28 | (165) ~ (e23 = e22) % 12.20/3.28 | % 12.20/3.28 | Equations (434) can reduce 181 to: % 12.20/3.28 | (114) ~ (e23 = e21) % 12.20/3.28 | % 12.20/3.28 +-Applying beta-rule and splitting (170), into two cases. % 12.20/3.28 |-Branch one: % 12.20/3.28 | (1172) (all_0_113_113 = e23 & all_0_123_123 = e22) | (all_0_113_113 = e23 & ~ (all_0_119_119 = e21)) | (all_0_115_115 = e22 & all_0_123_123 = e23) | (all_0_116_116 = e21 & ~ (all_0_123_123 = e21)) | (all_0_116_116 = e20 & all_0_120_120 = e21 & ~ (all_0_117_117 = e22)) | (all_0_117_117 = e22 & ~ (all_0_114_114 = e23) & ~ (all_0_116_116 = e20)) | (all_0_118_118 = e21 & all_0_123_123 = e23) % 12.20/3.28 | % 12.20/3.28 +-Applying beta-rule and splitting (1172), into two cases. % 12.20/3.28 |-Branch one: % 12.20/3.28 | (1173) (all_0_113_113 = e23 & all_0_123_123 = e22) | (all_0_113_113 = e23 & ~ (all_0_119_119 = e21)) | (all_0_115_115 = e22 & all_0_123_123 = e23) | (all_0_116_116 = e21 & ~ (all_0_123_123 = e21)) | (all_0_116_116 = e20 & all_0_120_120 = e21 & ~ (all_0_117_117 = e22)) | (all_0_117_117 = e22 & ~ (all_0_114_114 = e23) & ~ (all_0_116_116 = e20)) % 12.20/3.28 | % 12.20/3.28 +-Applying beta-rule and splitting (1173), into two cases. % 12.20/3.28 |-Branch one: % 12.20/3.28 | (1174) (all_0_113_113 = e23 & all_0_123_123 = e22) | (all_0_113_113 = e23 & ~ (all_0_119_119 = e21)) | (all_0_115_115 = e22 & all_0_123_123 = e23) | (all_0_116_116 = e21 & ~ (all_0_123_123 = e21)) | (all_0_116_116 = e20 & all_0_120_120 = e21 & ~ (all_0_117_117 = e22)) % 12.20/3.28 | % 12.20/3.28 +-Applying beta-rule and splitting (1174), into two cases. % 12.20/3.28 |-Branch one: % 12.20/3.28 | (1175) (all_0_113_113 = e23 & all_0_123_123 = e22) | (all_0_113_113 = e23 & ~ (all_0_119_119 = e21)) | (all_0_115_115 = e22 & all_0_123_123 = e23) | (all_0_116_116 = e21 & ~ (all_0_123_123 = e21)) % 12.20/3.28 | % 12.20/3.28 +-Applying beta-rule and splitting (1175), into two cases. % 12.20/3.28 |-Branch one: % 12.20/3.28 | (1176) (all_0_113_113 = e23 & all_0_123_123 = e22) | (all_0_113_113 = e23 & ~ (all_0_119_119 = e21)) | (all_0_115_115 = e22 & all_0_123_123 = e23) % 12.20/3.28 | % 12.20/3.28 +-Applying beta-rule and splitting (1176), into two cases. % 12.20/3.28 |-Branch one: % 12.20/3.28 | (1177) (all_0_113_113 = e23 & all_0_123_123 = e22) | (all_0_113_113 = e23 & ~ (all_0_119_119 = e21)) % 12.20/3.28 | % 12.20/3.28 +-Applying beta-rule and splitting (1177), into two cases. % 12.20/3.28 |-Branch one: % 12.20/3.28 | (1178) all_0_113_113 = e23 & all_0_123_123 = e22 % 12.20/3.28 | % 12.20/3.28 | Applying alpha-rule on (1178) yields: % 12.20/3.28 | (369) all_0_113_113 = e23 % 12.20/3.28 | (1108) all_0_123_123 = e22 % 12.20/3.28 | % 12.20/3.28 | Combining equations (369,366) yields a new equation: % 12.20/3.28 | (1181) e23 = e22 % 12.20/3.28 | % 12.20/3.28 | Simplifying 1181 yields: % 12.20/3.28 | (377) e23 = e22 % 12.20/3.28 | % 12.20/3.28 | Equations (377) can reduce 165 to: % 12.20/3.28 | (367) $false % 12.20/3.28 | % 12.20/3.28 |-The branch is then unsatisfiable % 12.20/3.28 |-Branch two: % 12.20/3.28 | (1184) all_0_113_113 = e23 & ~ (all_0_119_119 = e21) % 12.20/3.28 | % 12.20/3.28 | Applying alpha-rule on (1184) yields: % 12.20/3.28 | (369) all_0_113_113 = e23 % 12.20/3.28 | (484) ~ (all_0_119_119 = e21) % 12.20/3.28 | % 12.20/3.28 | Combining equations (366,369) yields a new equation: % 12.20/3.28 | (377) e23 = e22 % 12.20/3.28 | % 12.20/3.28 | Equations (377) can reduce 165 to: % 12.20/3.28 | (367) $false % 12.20/3.28 | % 12.20/3.28 |-The branch is then unsatisfiable % 12.20/3.28 |-Branch two: % 12.20/3.28 | (1189) all_0_115_115 = e22 & all_0_123_123 = e23 % 12.20/3.28 | % 12.20/3.28 | Applying alpha-rule on (1189) yields: % 12.20/3.28 | (351) all_0_115_115 = e22 % 12.20/3.28 | (420) all_0_123_123 = e23 % 12.20/3.28 | % 12.20/3.28 | Combining equations (448,351) yields a new equation: % 12.20/3.28 | (451) e22 = e21 % 12.20/3.28 | % 12.20/3.28 | Equations (451) can reduce 282 to: % 12.20/3.28 | (367) $false % 12.20/3.28 | % 12.20/3.28 |-The branch is then unsatisfiable % 12.20/3.28 |-Branch two: % 12.20/3.28 | (1194) all_0_116_116 = e21 & ~ (all_0_123_123 = e21) % 12.20/3.28 | % 12.20/3.28 | Applying alpha-rule on (1194) yields: % 12.20/3.28 | (400) all_0_116_116 = e21 % 12.20/3.28 | (1196) ~ (all_0_123_123 = e21) % 12.20/3.28 | % 12.20/3.28 | Equations (400) can reduce 403 to: % 12.20/3.28 | (367) $false % 12.20/3.28 | % 12.20/3.28 |-The branch is then unsatisfiable % 12.20/3.28 |-Branch two: % 12.20/3.28 | (1198) all_0_116_116 = e20 & all_0_120_120 = e21 & ~ (all_0_117_117 = e22) % 12.20/3.28 | % 12.20/3.28 | Applying alpha-rule on (1198) yields: % 12.20/3.28 | (388) all_0_116_116 = e20 % 12.20/3.28 | (540) all_0_120_120 = e21 % 12.20/3.28 | (355) ~ (all_0_117_117 = e22) % 12.20/3.28 | % 12.20/3.28 | Equations (388) can reduce 338 to: % 12.20/3.28 | (389) ~ (all_0_119_119 = e20) % 12.20/3.28 | % 12.20/3.28 | Simplifying 389 yields: % 12.20/3.28 | (390) ~ (all_0_119_119 = e20) % 12.20/3.28 | % 12.20/3.28 | Equations (540) can reduce 290 to: % 12.20/3.28 | (484) ~ (all_0_119_119 = e21) % 12.20/3.28 | % 12.20/3.28 +-Applying beta-rule and splitting (66), into two cases. % 12.20/3.28 |-Branch one: % 12.20/3.28 | (405) all_0_119_119 = e21 % 12.20/3.28 | % 12.20/3.28 | Equations (405) can reduce 484 to: % 12.20/3.28 | (367) $false % 12.20/3.28 | % 12.20/3.28 |-The branch is then unsatisfiable % 12.20/3.28 |-Branch two: % 12.20/3.28 | (484) ~ (all_0_119_119 = e21) % 12.20/3.28 | (1208) all_0_119_119 = e23 | all_0_119_119 = e20 % 12.20/3.28 | % 12.20/3.28 +-Applying beta-rule and splitting (1208), into two cases. % 12.20/3.28 |-Branch one: % 12.20/3.28 | (476) all_0_119_119 = e23 % 12.20/3.28 | % 12.20/3.28 | Equations (476) can reduce 373 to: % 12.20/3.28 | (367) $false % 12.20/3.28 | % 12.20/3.28 |-The branch is then unsatisfiable % 12.20/3.28 |-Branch two: % 12.20/3.28 | (373) ~ (all_0_119_119 = e23) % 12.20/3.28 | (393) all_0_119_119 = e20 % 12.20/3.28 | % 12.20/3.28 | Equations (393) can reduce 390 to: % 12.20/3.28 | (367) $false % 12.20/3.28 | % 12.20/3.28 |-The branch is then unsatisfiable % 12.20/3.28 |-Branch two: % 12.20/3.28 | (1214) all_0_117_117 = e22 & ~ (all_0_114_114 = e23) & ~ (all_0_116_116 = e20) % 12.20/3.28 | % 12.20/3.28 | Applying alpha-rule on (1214) yields: % 12.20/3.28 | (422) all_0_117_117 = e22 % 12.20/3.28 | (1216) ~ (all_0_114_114 = e23) % 12.20/3.28 | (488) ~ (all_0_116_116 = e20) % 12.20/3.29 | % 12.20/3.29 | Equations (434) can reduce 1216 to: % 12.20/3.29 | (367) $false % 12.20/3.29 | % 12.20/3.29 |-The branch is then unsatisfiable % 12.20/3.29 |-Branch two: % 12.20/3.29 | (1219) all_0_118_118 = e21 & all_0_123_123 = e23 % 12.20/3.29 | % 12.20/3.29 | Applying alpha-rule on (1219) yields: % 12.20/3.29 | (551) all_0_118_118 = e21 % 12.20/3.29 | (420) all_0_123_123 = e23 % 12.20/3.29 | % 12.20/3.29 | Combining equations (551,408) yields a new equation: % 12.20/3.29 | (460) e23 = e21 % 12.20/3.29 | % 12.20/3.29 | Equations (460) can reduce 114 to: % 12.20/3.29 | (367) $false % 12.20/3.29 | % 12.20/3.29 |-The branch is then unsatisfiable % 12.20/3.29 |-Branch two: % 12.20/3.29 | (1224) all_0_120_120 = e21 & ~ (all_0_114_114 = e23) % 12.20/3.29 | % 12.20/3.29 | Applying alpha-rule on (1224) yields: % 12.20/3.29 | (540) all_0_120_120 = e21 % 12.20/3.29 | (1216) ~ (all_0_114_114 = e23) % 12.20/3.29 | % 12.20/3.29 | Equations (434) can reduce 1216 to: % 12.20/3.29 | (367) $false % 12.20/3.29 | % 12.20/3.29 |-The branch is then unsatisfiable % 12.20/3.29 |-Branch two: % 12.20/3.29 | (359) ~ (all_0_113_113 = e22) % 12.20/3.29 | (369) all_0_113_113 = e23 % 12.20/3.29 | % 12.20/3.29 | Equations (369) can reduce 206 to: % 12.20/3.29 | (1230) ~ (all_0_114_114 = e23) % 12.20/3.29 | % 12.20/3.29 | Simplifying 1230 yields: % 12.20/3.29 | (1216) ~ (all_0_114_114 = e23) % 12.20/3.29 | % 12.20/3.29 | Equations (369) can reduce 259 to: % 12.20/3.29 | (370) ~ (all_0_116_116 = e23) % 12.20/3.29 | % 12.20/3.29 | Simplifying 370 yields: % 12.20/3.29 | (316) ~ (all_0_116_116 = e23) % 12.20/3.29 | % 12.20/3.29 | Equations (369) can reduce 35 to: % 12.20/3.29 | (372) ~ (all_0_119_119 = e23) % 12.20/3.29 | % 12.20/3.29 | Simplifying 372 yields: % 12.20/3.29 | (373) ~ (all_0_119_119 = e23) % 12.20/3.29 | % 12.20/3.29 | Equations (369) can reduce 304 to: % 12.20/3.29 | (1236) ~ (all_0_122_122 = e23) % 12.20/3.29 | % 12.20/3.29 | Simplifying 1236 yields: % 12.20/3.29 | (419) ~ (all_0_122_122 = e23) % 12.20/3.29 | % 12.20/3.29 +-Applying beta-rule and splitting (169), into two cases. % 12.20/3.29 |-Branch one: % 12.20/3.29 | (358) all_0_114_114 = e22 % 12.20/3.29 | % 12.20/3.29 | Equations (358) can reduce 86 to: % 12.20/3.29 | (1239) ~ (all_0_123_123 = e22) % 12.20/3.29 | % 12.20/3.29 | Simplifying 1239 yields: % 12.20/3.29 | (1240) ~ (all_0_123_123 = e22) % 12.20/3.29 | % 12.20/3.29 +-Applying beta-rule and splitting (177), into two cases. % 12.20/3.29 |-Branch one: % 12.20/3.29 | (384) all_0_122_122 = e22 % 12.20/3.29 | % 12.20/3.29 | Equations (384) can reduce 1152 to: % 12.20/3.29 | (367) $false % 12.20/3.29 | % 12.20/3.29 |-The branch is then unsatisfiable % 12.20/3.29 |-Branch two: % 12.20/3.29 | (1152) ~ (all_0_122_122 = e22) % 12.20/3.29 | (1244) all_0_122_122 = e23 | all_0_122_122 = e21 % 12.20/3.29 | % 12.20/3.29 +-Applying beta-rule and splitting (1244), into two cases. % 12.20/3.29 |-Branch one: % 12.20/3.29 | (485) all_0_122_122 = e21 % 12.20/3.29 | % 12.20/3.29 | Equations (485) can reduce 173 to: % 12.20/3.29 | (403) ~ (all_0_116_116 = e21) % 12.20/3.29 | % 12.20/3.29 | Equations (485) can reduce 54 to: % 12.20/3.29 | (484) ~ (all_0_119_119 = e21) % 12.20/3.29 | % 12.20/3.29 | Equations (485) can reduce 184 to: % 12.20/3.29 | (1248) ~ (all_0_123_123 = e21) % 12.20/3.29 | % 12.20/3.29 | Simplifying 1248 yields: % 12.20/3.29 | (1196) ~ (all_0_123_123 = e21) % 12.20/3.29 | % 12.20/3.29 +-Applying beta-rule and splitting (348), into two cases. % 12.20/3.29 |-Branch one: % 12.20/3.29 | (1108) all_0_123_123 = e22 % 12.20/3.29 | % 12.20/3.29 | Equations (1108) can reduce 1240 to: % 12.20/3.29 | (367) $false % 12.20/3.29 | % 12.20/3.29 |-The branch is then unsatisfiable % 12.20/3.29 |-Branch two: % 12.20/3.29 | (1240) ~ (all_0_123_123 = e22) % 12.20/3.29 | (1253) all_0_123_123 = e23 | all_0_123_123 = e21 % 12.20/3.29 | % 12.20/3.29 +-Applying beta-rule and splitting (1253), into two cases. % 12.20/3.29 |-Branch one: % 12.20/3.29 | (454) all_0_123_123 = e21 % 12.20/3.29 | % 12.20/3.29 | Equations (454) can reduce 1196 to: % 12.20/3.29 | (367) $false % 12.20/3.29 | % 12.20/3.29 |-The branch is then unsatisfiable % 12.20/3.29 |-Branch two: % 12.20/3.29 | (1196) ~ (all_0_123_123 = e21) % 12.20/3.29 | (420) all_0_123_123 = e23 % 12.20/3.29 | % 12.20/3.29 | Equations (420) can reduce 1196 to: % 12.20/3.29 | (114) ~ (e23 = e21) % 12.20/3.29 | % 12.20/3.29 +-Applying beta-rule and splitting (66), into two cases. % 12.20/3.29 |-Branch one: % 12.20/3.29 | (405) all_0_119_119 = e21 % 12.20/3.29 | % 12.20/3.29 | Equations (405) can reduce 484 to: % 12.20/3.29 | (367) $false % 12.20/3.29 | % 12.20/3.29 |-The branch is then unsatisfiable % 12.20/3.29 |-Branch two: % 12.20/3.29 | (484) ~ (all_0_119_119 = e21) % 12.20/3.29 | (1208) all_0_119_119 = e23 | all_0_119_119 = e20 % 12.20/3.29 | % 12.20/3.29 +-Applying beta-rule and splitting (1208), into two cases. % 12.20/3.29 |-Branch one: % 12.20/3.29 | (476) all_0_119_119 = e23 % 12.20/3.29 | % 12.20/3.29 | Equations (476) can reduce 373 to: % 12.20/3.29 | (367) $false % 12.20/3.29 | % 12.20/3.29 |-The branch is then unsatisfiable % 12.20/3.29 |-Branch two: % 12.20/3.29 | (373) ~ (all_0_119_119 = e23) % 12.20/3.29 | (393) all_0_119_119 = e20 % 12.20/3.29 | % 12.20/3.29 | Equations (393) can reduce 338 to: % 12.20/3.29 | (488) ~ (all_0_116_116 = e20) % 12.20/3.29 | % 12.20/3.29 | Equations (393) can reduce 484 to: % 12.20/3.29 | (1268) ~ (e21 = e20) % 12.20/3.29 | % 12.20/3.29 | Simplifying 1268 yields: % 12.20/3.29 | (140) ~ (e21 = e20) % 12.20/3.29 | % 12.20/3.29 +-Applying beta-rule and splitting (345), into two cases. % 12.20/3.29 |-Branch one: % 12.20/3.29 | (381) all_0_116_116 = e22 % 12.20/3.29 | % 12.20/3.29 | Equations (381) can reduce 316 to: % 12.20/3.30 | (1097) ~ (e23 = e22) % 12.20/3.30 | % 12.20/3.30 | Simplifying 1097 yields: % 12.20/3.30 | (165) ~ (e23 = e22) % 12.20/3.30 | % 12.20/3.30 +-Applying beta-rule and splitting (32), into two cases. % 12.20/3.30 |-Branch one: % 12.20/3.30 | (431) (all_0_91_91 = e22 & all_0_92_92 = e20 & all_0_114_114 = e23 & ~ (all_0_115_115 = e22) & ~ (all_0_118_118 = e21)) | (all_0_93_93 = e23 & all_0_94_94 = e22 & all_0_95_95 = e20 & all_0_115_115 = e21 & ~ (all_0_113_113 = e23)) | (all_0_96_96 = e23 & all_0_97_97 = e22 & all_0_98_98 = e20 & all_0_119_119 = e21 & all_0_123_123 = e21) % 12.20/3.30 | % 12.20/3.30 +-Applying beta-rule and splitting (431), into two cases. % 12.20/3.30 |-Branch one: % 12.20/3.30 | (432) (all_0_91_91 = e22 & all_0_92_92 = e20 & all_0_114_114 = e23 & ~ (all_0_115_115 = e22) & ~ (all_0_118_118 = e21)) | (all_0_93_93 = e23 & all_0_94_94 = e22 & all_0_95_95 = e20 & all_0_115_115 = e21 & ~ (all_0_113_113 = e23)) % 12.20/3.30 | % 12.20/3.30 +-Applying beta-rule and splitting (432), into two cases. % 12.20/3.30 |-Branch one: % 12.20/3.30 | (433) all_0_91_91 = e22 & all_0_92_92 = e20 & all_0_114_114 = e23 & ~ (all_0_115_115 = e22) & ~ (all_0_118_118 = e21) % 12.20/3.30 | % 12.20/3.30 | Applying alpha-rule on (433) yields: % 12.20/3.30 | (434) all_0_114_114 = e23 % 12.20/3.30 | (435) ~ (all_0_115_115 = e22) % 12.20/3.30 | (436) ~ (all_0_118_118 = e21) % 12.20/3.30 | (437) all_0_92_92 = e20 % 12.20/3.30 | (438) all_0_91_91 = e22 % 12.20/3.30 | % 12.20/3.30 | Combining equations (358,434) yields a new equation: % 12.20/3.30 | (377) e23 = e22 % 12.20/3.30 | % 12.20/3.30 | Equations (377) can reduce 165 to: % 12.20/3.30 | (367) $false % 12.20/3.30 | % 12.20/3.30 |-The branch is then unsatisfiable % 12.20/3.30 |-Branch two: % 12.20/3.30 | (444) all_0_93_93 = e23 & all_0_94_94 = e22 & all_0_95_95 = e20 & all_0_115_115 = e21 & ~ (all_0_113_113 = e23) % 12.20/3.30 | % 12.20/3.30 | Applying alpha-rule on (444) yields: % 12.20/3.30 | (445) ~ (all_0_113_113 = e23) % 12.20/3.30 | (446) all_0_93_93 = e23 % 12.20/3.30 | (447) all_0_94_94 = e22 % 12.20/3.30 | (448) all_0_115_115 = e21 % 12.20/3.30 | (449) all_0_95_95 = e20 % 12.20/3.30 | % 12.20/3.30 | Equations (369) can reduce 445 to: % 12.20/3.30 | (367) $false % 12.20/3.30 | % 12.20/3.30 |-The branch is then unsatisfiable % 12.20/3.30 |-Branch two: % 12.20/3.30 | (453) all_0_96_96 = e23 & all_0_97_97 = e22 & all_0_98_98 = e20 & all_0_119_119 = e21 & all_0_123_123 = e21 % 12.20/3.30 | % 12.20/3.30 | Applying alpha-rule on (453) yields: % 12.20/3.30 | (454) all_0_123_123 = e21 % 12.20/3.30 | (455) all_0_98_98 = e20 % 12.20/3.30 | (456) all_0_96_96 = e23 % 12.20/3.30 | (457) all_0_97_97 = e22 % 12.20/3.30 | (405) all_0_119_119 = e21 % 12.20/3.30 | % 12.20/3.30 | Combining equations (405,393) yields a new equation: % 12.20/3.30 | (529) e21 = e20 % 12.20/3.30 | % 12.20/3.30 | Simplifying 529 yields: % 12.20/3.30 | (401) e21 = e20 % 12.20/3.30 | % 12.20/3.30 | Equations (401) can reduce 140 to: % 12.20/3.30 | (367) $false % 12.20/3.30 | % 12.20/3.30 |-The branch is then unsatisfiable % 12.20/3.30 |-Branch two: % 12.20/3.30 | (462) all_0_99_99 = e23 & all_0_100_100 = e22 & all_0_101_101 = e20 & all_0_123_123 = e21 & ~ (all_0_120_120 = e21) & ( ~ (all_0_117_117 = e22) | all_0_116_116 = e20) % 12.20/3.30 | % 12.20/3.30 | Applying alpha-rule on (462) yields: % 12.20/3.30 | (454) all_0_123_123 = e21 % 12.20/3.30 | (464) ~ (all_0_120_120 = e21) % 12.20/3.30 | (465) all_0_100_100 = e22 % 12.20/3.30 | (466) ~ (all_0_117_117 = e22) | all_0_116_116 = e20 % 12.20/3.30 | (467) all_0_101_101 = e20 % 12.20/3.30 | (468) all_0_99_99 = e23 % 12.20/3.30 | % 12.20/3.30 | Combining equations (454,420) yields a new equation: % 12.20/3.30 | (460) e23 = e21 % 12.20/3.30 | % 12.20/3.30 | Equations (460) can reduce 114 to: % 12.20/3.30 | (367) $false % 12.20/3.30 | % 12.20/3.30 |-The branch is then unsatisfiable % 12.20/3.30 |-Branch two: % 12.20/3.30 | (353) ~ (all_0_116_116 = e22) % 12.20/3.30 | (1309) all_0_116_116 = e21 | all_0_116_116 = e20 % 12.20/3.30 | % 12.20/3.30 +-Applying beta-rule and splitting (1309), into two cases. % 12.20/3.30 |-Branch one: % 12.20/3.30 | (400) all_0_116_116 = e21 % 12.20/3.30 | % 12.20/3.30 | Equations (400) can reduce 403 to: % 12.20/3.30 | (367) $false % 12.20/3.30 | % 12.20/3.30 |-The branch is then unsatisfiable % 12.20/3.30 |-Branch two: % 12.20/3.30 | (403) ~ (all_0_116_116 = e21) % 12.20/3.30 | (388) all_0_116_116 = e20 % 12.20/3.30 | % 12.20/3.30 | Equations (388) can reduce 488 to: % 12.20/3.30 | (367) $false % 12.20/3.30 | % 12.20/3.30 |-The branch is then unsatisfiable % 12.20/3.30 |-Branch two: % 12.20/3.30 | (1315) ~ (all_0_122_122 = e21) % 12.20/3.30 | (416) all_0_122_122 = e23 % 12.20/3.30 | % 12.20/3.30 | Equations (416) can reduce 419 to: % 12.20/3.30 | (367) $false % 12.20/3.30 | % 12.20/3.30 |-The branch is then unsatisfiable % 12.20/3.30 |-Branch two: % 12.20/3.30 | (1093) ~ (all_0_114_114 = e22) % 12.20/3.30 | (434) all_0_114_114 = e23 % 12.20/3.30 | % 12.20/3.30 | Equations (434) can reduce 1216 to: % 12.20/3.30 | (367) $false % 12.20/3.30 | % 12.20/3.30 |-The branch is then unsatisfiable % 12.20/3.30 |-Branch two: % 12.20/3.30 | (474) ~ (all_0_118_118 = e23) % 12.20/3.30 | (412) all_0_121_121 = e23 % 12.20/3.30 | % 12.20/3.30 | Combining equations (412,1149) yields a new equation: % 12.20/3.30 | (1181) e23 = e22 % 12.20/3.30 | % 12.20/3.30 | Simplifying 1181 yields: % 12.20/3.30 | (377) e23 = e22 % 12.20/3.30 | % 12.20/3.30 | Equations (377) can reduce 165 to: % 12.20/3.30 | (367) $false % 12.20/3.30 | % 12.20/3.30 |-The branch is then unsatisfiable % 12.20/3.30 % SZS output end Proof for theBenchmark % 12.20/3.30 % 12.20/3.30 2717ms %------------------------------------------------------------------------------