%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : ALG124+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n018.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:15 EDT 2022 % Result : Theorem 9.70s 2.89s % Output : Proof 16.26s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : ALG124+1 : TPTP v8.1.0. Released v2.7.0. % 0.03/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.34 % Computer : n018.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Wed Jun 8 20:47:22 EDT 2022 % 0.13/0.34 % CPUTime : % 0.59/0.64 ____ _ % 0.59/0.64 ___ / __ \_____(_)___ ________ __________ % 0.59/0.64 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.59/0.64 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.59/0.64 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.59/0.65 % 0.59/0.65 A Theorem Prover for First-Order Logic % 0.74/0.65 (ePrincess v.1.0) % 0.74/0.65 % 0.74/0.65 (c) Philipp Rümmer, 2009-2015 % 0.74/0.65 (c) Peter Backeman, 2014-2015 % 0.74/0.65 (contributions by Angelo Brillout, Peter Baumgartner) % 0.74/0.65 Free software under GNU Lesser General Public License (LGPL). % 0.74/0.65 Bug reports to peter@backeman.se % 0.74/0.65 % 0.74/0.65 For more information, visit http://user.uu.se/~petba168/breu/ % 0.74/0.65 % 0.74/0.65 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.88/0.73 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 3.93/1.53 Prover 0: Preprocessing ... % 7.76/2.41 Prover 0: Constructing countermodel ... % 9.70/2.89 Prover 0: proved (2158ms) % 9.70/2.89 % 9.70/2.89 No countermodel exists, formula is valid % 9.70/2.89 % SZS status Theorem for theBenchmark % 9.70/2.89 % 9.70/2.89 Generating proof ... found it (size 443) % 14.91/4.14 % 14.91/4.14 % SZS output start Proof for theBenchmark % 14.91/4.14 Assumed formulas after preprocessing and simplification: % 14.91/4.14 | (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] : ( ~ (v23 = v22) & ~ (v23 = v21) & ~ (v23 = v20) & ~ (v23 = v17) & ~ (v23 = v14) & ~ (v23 = e23) & ~ (v23 = e22) & ~ (v22 = v21) & ~ (v22 = v19) & ~ (v22 = v16) & ~ (v22 = v13) & ~ (v22 = e22) & ~ (v21 = v18) & ~ (v21 = v15) & ~ (v21 = v12) & ~ (v21 = e22) & ~ (v20 = v19) & ~ (v20 = v18) & ~ (v20 = v17) & ~ (v20 = v14) & ~ (v20 = e21) & ~ (v19 = v18) & ~ (v19 = v16) & ~ (v19 = v13) & ~ (v19 = e22) & ~ (v19 = e21) & ~ (v18 = v15) & ~ (v18 = v12) & ~ (v18 = e21) & ~ (v17 = v16) & ~ (v17 = v15) & ~ (v17 = v14) & ~ (v17 = e20) & ~ (v16 = v15) & ~ (v16 = v13) & ~ (v16 = e20) & ~ (v15 = v12) & ~ (v15 = e21) & ~ (v15 = e20) & ~ (v14 = v13) & ~ (v14 = v12) & ~ (v14 = e23) & ~ (v13 = v12) & ~ (v13 = e23) & ~ (v12 = e23) & ~ (v11 = v10) & ~ (v11 = v9) & ~ (v11 = v8) & ~ (v11 = v5) & ~ (v11 = v2) & ~ (v11 = e13) & ~ (v11 = e12) & ~ (v10 = v9) & ~ (v10 = v7) & ~ (v10 = v4) & ~ (v10 = v1) & ~ (v10 = e12) & ~ (v9 = v6) & ~ (v9 = v3) & ~ (v9 = v0) & ~ (v9 = e12) & ~ (v8 = v7) & ~ (v8 = v6) & ~ (v8 = v5) & ~ (v8 = v2) & ~ (v8 = e11) & ~ (v7 = v6) & ~ (v7 = v4) & ~ (v7 = v1) & ~ (v7 = e12) & ~ (v7 = e11) & ~ (v6 = v3) & ~ (v6 = v0) & ~ (v6 = e11) & ~ (v5 = v4) & ~ (v5 = v3) & ~ (v5 = v2) & ~ (v5 = e10) & ~ (v4 = v3) & ~ (v4 = v1) & ~ (v4 = e10) & ~ (v3 = v0) & ~ (v3 = e11) & ~ (v3 = e10) & ~ (v2 = v1) & ~ (v2 = v0) & ~ (v2 = e13) & ~ (v1 = v0) & ~ (v1 = e13) & ~ (v0 = e13) & ~ (e23 = e22) & ~ (e23 = e21) & ~ (e23 = e20) & ~ (e23 = e13) & ~ (e23 = e12) & ~ (e23 = e11) & ~ (e23 = e10) & ~ (e22 = e21) & ~ (e22 = e20) & ~ (e22 = e13) & ~ (e22 = e12) & ~ (e22 = e11) & ~ (e22 = e10) & ~ (e21 = e20) & ~ (e21 = e13) & ~ (e21 = e12) & ~ (e21 = e11) & ~ (e21 = e10) & ~ (e20 = e13) & ~ (e20 = e12) & ~ (e20 = e11) & ~ (e20 = e10) & ~ (e13 = e12) & ~ (e13 = e11) & ~ (e13 = e10) & ~ (e12 = e11) & ~ (e12 = e10) & ~ (e11 = e10) & op1(e13, e13) = v11 & op1(e13, e12) = v10 & op1(e13, e11) = v9 & op1(e13, e10) = e12 & op1(e12, e13) = v8 & op1(e12, e12) = v7 & op1(e12, e11) = v6 & op1(e12, e10) = e11 & op1(e11, e13) = v5 & op1(e11, e12) = v4 & op1(e11, e11) = v3 & op1(e11, e10) = e10 & op1(e10, e13) = v2 & op1(e10, e12) = v1 & op1(e10, e11) = v0 & op1(e10, e10) = e13 & h1(v11) = v41 & h1(v10) = v40 & h1(v9) = v39 & h1(v8) = v38 & h1(v7) = v37 & h1(v6) = v36 & h1(v5) = v35 & h1(v4) = v34 & h1(v3) = v33 & h1(v2) = v32 & h1(v1) = v31 & h1(v0) = v30 & h1(e13) = e23 & h1(e12) = e22 & h1(e11) = e21 & h1(e10) = e20 & h2(v11) = v67 & h2(v10) = v65 & h2(v9) = v63 & h2(v8) = v60 & h2(v7) = v58 & h2(v6) = v56 & h2(v5) = v53 & h2(v4) = v51 & h2(v3) = v49 & h2(v2) = v46 & h2(v1) = v44 & h2(v0) = v42 & h2(e13) = v15 & h2(e12) = v25 & h2(e11) = v24 & h2(e10) = e21 & h3(v11) = v94 & h3(v10) = v92 & h3(v9) = v90 & h3(v8) = v87 & h3(v7) = v85 & h3(v6) = v83 & h3(v5) = v80 & h3(v4) = v78 & h3(v3) = v76 & h3(v2) = v73 & h3(v1) = v71 & h3(v0) = v69 & h3(e13) = v19 & h3(e12) = v27 & h3(e11) = v26 & h3(e10) = e22 & h4(v11) = v121 & h4(v10) = v119 & h4(v9) = v117 & h4(v8) = v114 & h4(v7) = v112 & h4(v6) = v110 & h4(v5) = v107 & h4(v4) = v105 & h4(v3) = v103 & h4(v2) = v100 & h4(v1) = v98 & h4(v0) = v96 & h4(e13) = v23 & h4(e12) = v29 & h4(e11) = v28 & h4(e10) = e23 & op2(v29, v29) = v113 & op2(v29, v28) = v111 & op2(v29, v23) = v115 & op2(v29, e23) = v109 & op2(v29, e23) = v28 & op2(v28, v29) = v106 & op2(v28, v28) = v104 & op2(v28, v23) = v108 & op2(v28, e23) = v102 & op2(v27, v27) = v86 & op2(v27, v26) = v84 & op2(v27, v19) = v88 & op2(v27, e22) = v82 & op2(v27, e22) = v26 & op2(v26, v27) = v79 & op2(v26, v26) = v77 & op2(v26, v19) = v81 & op2(v26, e22) = v75 & op2(v25, v25) = v59 & op2(v25, v24) = v57 & op2(v25, v15) = v61 & op2(v25, e21) = v55 & op2(v25, e21) = v24 & op2(v24, v25) = v52 & op2(v24, v24) = v50 & op2(v24, v15) = v54 & op2(v24, e21) = v48 & op2(v23, v29) = v120 & op2(v23, v28) = v118 & op2(v23, v23) = v122 & op2(v23, e23) = v116 & op2(v23, e23) = v29 & op2(v19, v27) = v93 & op2(v19, v26) = v91 & op2(v19, v19) = v95 & op2(v19, e22) = v89 & op2(v19, e22) = v27 & op2(v15, v25) = v66 & op2(v15, v24) = v64 & op2(v15, v15) = v68 & op2(v15, e21) = v62 & op2(v15, e21) = v25 & op2(e23, v29) = v99 & op2(e23, v28) = v97 & op2(e23, v23) = v101 & op2(e23, e23) = v23 & op2(e23, e22) = v22 & op2(e23, e21) = v21 & op2(e23, e20) = e22 & op2(e22, v27) = v72 & op2(e22, v26) = v70 & op2(e22, v19) = v74 & op2(e22, e23) = v20 & op2(e22, e22) = v19 & op2(e22, e21) = v18 & op2(e22, e20) = e21 & op2(e21, v25) = v45 & op2(e21, v24) = v43 & op2(e21, v15) = v47 & op2(e21, e23) = v17 & op2(e21, e22) = v16 & op2(e21, e21) = v15 & op2(e21, e20) = e20 & op2(e20, e23) = v14 & op2(e20, e22) = v13 & op2(e20, e21) = v12 & op2(e20, e20) = e23 & ! [v123] : ! [v124] : ! [v125] : ! [v126] : (v124 = v123 | ~ (op1(v126, v125) = v124) | ~ (op1(v126, v125) = v123)) & ! [v123] : ! [v124] : ! [v125] : ! [v126] : (v124 = v123 | ~ (op2(v126, v125) = v124) | ~ (op2(v126, v125) = v123)) & ! [v123] : ! [v124] : ! [v125] : (v124 = v123 | ~ (h1(v125) = v124) | ~ (h1(v125) = v123)) & ! [v123] : ! [v124] : ! [v125] : (v124 = v123 | ~ (h2(v125) = v124) | ~ (h2(v125) = v123)) & ! [v123] : ! [v124] : ! [v125] : (v124 = v123 | ~ (h3(v125) = v124) | ~ (h3(v125) = v123)) & ! [v123] : ! [v124] : ! [v125] : (v124 = v123 | ~ (h4(v125) = v124) | ~ (h4(v125) = v123)) & ( ~ (v122 = v121) | ~ (v120 = v119) | ~ (v118 = v117) | ~ (v116 = v29) | ~ (v115 = v114) | ~ (v113 = v112) | ~ (v111 = v110) | ~ (v109 = v28) | ~ (v108 = v107) | ~ (v106 = v105) | ~ (v104 = v103) | ~ (v102 = e23) | ~ (v101 = v100) | ~ (v99 = v98) | ~ (v97 = v96) | ( ~ (v29 = e22) & ~ (v28 = e22)) | ( ~ (v29 = e21) & ~ (v28 = e21) & ~ (v23 = e21)) | ( ~ (v29 = e20) & ~ (v28 = e20) & ~ (v23 = e20))) & ( ~ (v95 = v94) | ~ (v93 = v92) | ~ (v91 = v90) | ~ (v89 = v27) | ~ (v88 = v87) | ~ (v86 = v85) | ~ (v84 = v83) | ~ (v82 = v26) | ~ (v81 = v80) | ~ (v79 = v78) | ~ (v77 = v76) | ~ (v75 = e22) | ~ (v74 = v73) | ~ (v72 = v71) | ~ (v70 = v69) | ( ~ (v27 = e23) & ~ (v26 = e23) & ~ (v19 = e23)) | ( ~ (v27 = e21) & ~ (v26 = e21)) | ( ~ (v27 = e20) & ~ (v26 = e20) & ~ (v19 = e20))) & ( ~ (v68 = v67) | ~ (v66 = v65) | ~ (v64 = v63) | ~ (v62 = v25) | ~ (v61 = v60) | ~ (v59 = v58) | ~ (v57 = v56) | ~ (v55 = v24) | ~ (v54 = v53) | ~ (v52 = v51) | ~ (v50 = v49) | ~ (v48 = e21) | ~ (v47 = v46) | ~ (v45 = v44) | ~ (v43 = v42) | ( ~ (v25 = e23) & ~ (v24 = e23) & ~ (v15 = e23)) | ( ~ (v25 = e22) & ~ (v24 = e22) & ~ (v15 = e22)) | ( ~ (v25 = e20) & ~ (v24 = e20))) & ( ~ (v41 = v23) | ~ (v40 = v22) | ~ (v39 = v21) | ~ (v38 = v20) | ~ (v37 = v19) | ~ (v36 = v18) | ~ (v35 = v17) | ~ (v34 = v16) | ~ (v33 = v15) | ~ (v32 = v14) | ~ (v31 = v13) | ~ (v30 = v12)) & (v23 = e21 | v23 = e20) & (v23 = e21 | v22 = e21 | v21 = e21) & (v23 = e21 | v17 = e21 | v14 = e21) & (v23 = e20 | v22 = e20 | v21 = e20) & (v23 = e20 | v20 = e20 | v14 = e20) & (v22 = e23 | v22 = e21 | v22 = e20) & (v22 = e23 | v21 = e23) & (v22 = e23 | v19 = e23 | v16 = e23) & (v22 = e21 | v16 = e21 | v13 = e21) & (v22 = e20 | v19 = e20 | v13 = e20) & (v21 = e23 | v21 = e21 | v21 = e20) & (v21 = e23 | v18 = e23 | v15 = e23) & (v21 = e21 | v12 = e21) & (v21 = e20 | v18 = e20 | v12 = e20) & (v20 = e23 | v20 = e22 | v20 = e20) & (v20 = e23 | v19 = e23 | v18 = e23) & (v20 = e23 | v17 = e23) & (v20 = e22 | v18 = e22) & (v20 = e22 | v17 = e22 | v14 = e22) & (v20 = e20 | v19 = e20 | v18 = e20) & (v19 = e23 | v19 = e20) & (v18 = e23 | v18 = e22 | v18 = e20) & (v18 = e22 | v15 = e22 | v12 = e22) & (v17 = e23 | v17 = e22 | v17 = e21) & (v17 = e23 | v16 = e23 | v15 = e23) & (v17 = e22 | v16 = e22 | v15 = e22) & (v17 = e21 | v16 = e21) & (v16 = e23 | v16 = e22 | v16 = e21) & (v16 = e22 | v13 = e22) & (v15 = e23 | v15 = e22) & (v14 = e22 | v14 = e21 | v14 = e20) & (v14 = e22 | v13 = e22 | v12 = e22) & (v14 = e21 | v13 = e21 | v12 = e21) & (v14 = e20 | v13 = e20 | v12 = e20) & (v13 = e22 | v13 = e21 | v13 = e20) & (v12 = e22 | v12 = e21 | v12 = e20) & (v11 = e11 | v11 = e10) & (v11 = e11 | v10 = e11 | v9 = e11) & (v11 = e11 | v5 = e11 | v2 = e11) & (v11 = e10 | v10 = e10 | v9 = e10) & (v11 = e10 | v8 = e10 | v2 = e10) & (v10 = e13 | v10 = e11 | v10 = e10) & (v10 = e13 | v9 = e13) & (v10 = e13 | v7 = e13 | v4 = e13) & (v10 = e11 | v4 = e11 | v1 = e11) & (v10 = e10 | v7 = e10 | v1 = e10) & (v9 = e13 | v9 = e11 | v9 = e10) & (v9 = e13 | v6 = e13 | v3 = e13) & (v9 = e11 | v0 = e11) & (v9 = e10 | v6 = e10 | v0 = e10) & (v8 = e13 | v8 = e12 | v8 = e10) & (v8 = e13 | v7 = e13 | v6 = e13) & (v8 = e13 | v5 = e13) & (v8 = e12 | v6 = e12) & (v8 = e12 | v5 = e12 | v2 = e12) & (v8 = e10 | v7 = e10 | v6 = e10) & (v7 = e13 | v7 = e10) & (v6 = e13 | v6 = e12 | v6 = e10) & (v6 = e12 | v3 = e12 | v0 = e12) & (v5 = e13 | v5 = e12 | v5 = e11) & (v5 = e13 | v4 = e13 | v3 = e13) & (v5 = e12 | v4 = e12 | v3 = e12) & (v5 = e11 | v4 = e11) & (v4 = e13 | v4 = e12 | v4 = e11) & (v4 = e12 | v1 = e12) & (v3 = e13 | v3 = e12) & (v2 = e12 | v2 = e11 | v2 = e10) & (v2 = e12 | v1 = e12 | v0 = e12) & (v2 = e11 | v1 = e11 | v0 = e11) & (v2 = e10 | v1 = e10 | v0 = e10) & (v1 = e12 | v1 = e11 | v1 = e10) & (v0 = e12 | v0 = e11 | v0 = e10) & ((v22 = e20 & ~ (v18 = e22) & ~ (v14 = e22) & ( ~ (v20 = e22) | v19 = e23) & ( ~ (v17 = e22) | v16 = e23) & ( ~ (v15 = e22) | v16 = e21) & ( ~ (v12 = e22) | v13 = e21)) | (v18 = e20 & ~ (v22 = e21) & ~ (v14 = e21) & ( ~ (v23 = e21) | v21 = e23) & ( ~ (v17 = e21) | v15 = e23) & ( ~ (v16 = e21) | v15 = e22) & ( ~ (v13 = e21) | v12 = e22)) | (v14 = e20 & ~ (v22 = e23) & ~ (v18 = e23) & ( ~ (v21 = e23) | v23 = e21) & ( ~ (v19 = e23) | v20 = e22) & ( ~ (v16 = e23) | v17 = e22) & ( ~ (v15 = e23) | v17 = e21)) | ( ~ (v23 = e20) & ~ (v21 = e20) & ~ (v20 = e20) & ~ (v19 = e20) & ~ (v13 = e20) & ~ (v12 = e20))) & ((v10 = e10 & ~ (v6 = e12) & ~ (v2 = e12) & ( ~ (v8 = e12) | v7 = e13) & ( ~ (v5 = e12) | v4 = e13) & ( ~ (v3 = e12) | v4 = e11) & ( ~ (v0 = e12) | v1 = e11)) | (v6 = e10 & ~ (v10 = e11) & ~ (v2 = e11) & ( ~ (v11 = e11) | v9 = e13) & ( ~ (v5 = e11) | v3 = e13) & ( ~ (v4 = e11) | v3 = e12) & ( ~ (v1 = e11) | v0 = e12)) | (v2 = e10 & ~ (v10 = e13) & ~ (v6 = e13) & ( ~ (v9 = e13) | v11 = e11) & ( ~ (v7 = e13) | v8 = e12) & ( ~ (v4 = e13) | v5 = e12) & ( ~ (v3 = e13) | v5 = e11)) | ( ~ (v11 = e10) & ~ (v9 = e10) & ~ (v8 = e10) & ~ (v7 = e10) & ~ (v1 = e10) & ~ (v0 = e10)))) % 15.12/4.22 | 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 yields: % 15.12/4.22 | (1) ~ (all_0_99_99 = all_0_100_100) & ~ (all_0_99_99 = all_0_101_101) & ~ (all_0_99_99 = all_0_102_102) & ~ (all_0_99_99 = all_0_105_105) & ~ (all_0_99_99 = all_0_108_108) & ~ (all_0_99_99 = e23) & ~ (all_0_99_99 = e22) & ~ (all_0_100_100 = all_0_101_101) & ~ (all_0_100_100 = all_0_103_103) & ~ (all_0_100_100 = all_0_106_106) & ~ (all_0_100_100 = all_0_109_109) & ~ (all_0_100_100 = e22) & ~ (all_0_101_101 = all_0_104_104) & ~ (all_0_101_101 = all_0_107_107) & ~ (all_0_101_101 = all_0_110_110) & ~ (all_0_101_101 = e22) & ~ (all_0_102_102 = all_0_103_103) & ~ (all_0_102_102 = all_0_104_104) & ~ (all_0_102_102 = all_0_105_105) & ~ (all_0_102_102 = all_0_108_108) & ~ (all_0_102_102 = e21) & ~ (all_0_103_103 = all_0_104_104) & ~ (all_0_103_103 = all_0_106_106) & ~ (all_0_103_103 = all_0_109_109) & ~ (all_0_103_103 = e22) & ~ (all_0_103_103 = e21) & ~ (all_0_104_104 = all_0_107_107) & ~ (all_0_104_104 = all_0_110_110) & ~ (all_0_104_104 = e21) & ~ (all_0_105_105 = all_0_106_106) & ~ (all_0_105_105 = all_0_107_107) & ~ (all_0_105_105 = all_0_108_108) & ~ (all_0_105_105 = e20) & ~ (all_0_106_106 = all_0_107_107) & ~ (all_0_106_106 = all_0_109_109) & ~ (all_0_106_106 = e20) & ~ (all_0_107_107 = all_0_110_110) & ~ (all_0_107_107 = e21) & ~ (all_0_107_107 = e20) & ~ (all_0_108_108 = all_0_109_109) & ~ (all_0_108_108 = all_0_110_110) & ~ (all_0_108_108 = e23) & ~ (all_0_109_109 = all_0_110_110) & ~ (all_0_109_109 = e23) & ~ (all_0_110_110 = e23) & ~ (all_0_111_111 = all_0_112_112) & ~ (all_0_111_111 = all_0_113_113) & ~ (all_0_111_111 = all_0_114_114) & ~ (all_0_111_111 = all_0_117_117) & ~ (all_0_111_111 = all_0_120_120) & ~ (all_0_111_111 = e13) & ~ (all_0_111_111 = e12) & ~ (all_0_112_112 = all_0_113_113) & ~ (all_0_112_112 = all_0_115_115) & ~ (all_0_112_112 = all_0_118_118) & ~ (all_0_112_112 = all_0_121_121) & ~ (all_0_112_112 = e12) & ~ (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 = e12) & ~ (all_0_114_114 = all_0_115_115) & ~ (all_0_114_114 = all_0_116_116) & ~ (all_0_114_114 = all_0_117_117) & ~ (all_0_114_114 = all_0_120_120) & ~ (all_0_114_114 = e11) & ~ (all_0_115_115 = all_0_116_116) & ~ (all_0_115_115 = all_0_118_118) & ~ (all_0_115_115 = all_0_121_121) & ~ (all_0_115_115 = e12) & ~ (all_0_115_115 = e11) & ~ (all_0_116_116 = all_0_119_119) & ~ (all_0_116_116 = all_0_122_122) & ~ (all_0_116_116 = e11) & ~ (all_0_117_117 = all_0_118_118) & ~ (all_0_117_117 = all_0_119_119) & ~ (all_0_117_117 = all_0_120_120) & ~ (all_0_117_117 = e10) & ~ (all_0_118_118 = all_0_119_119) & ~ (all_0_118_118 = all_0_121_121) & ~ (all_0_118_118 = e10) & ~ (all_0_119_119 = all_0_122_122) & ~ (all_0_119_119 = e11) & ~ (all_0_119_119 = e10) & ~ (all_0_120_120 = all_0_121_121) & ~ (all_0_120_120 = all_0_122_122) & ~ (all_0_120_120 = e13) & ~ (all_0_121_121 = all_0_122_122) & ~ (all_0_121_121 = e13) & ~ (all_0_122_122 = e13) & ~ (e23 = e22) & ~ (e23 = e21) & ~ (e23 = e20) & ~ (e23 = e13) & ~ (e23 = e12) & ~ (e23 = e11) & ~ (e23 = e10) & ~ (e22 = e21) & ~ (e22 = e20) & ~ (e22 = e13) & ~ (e22 = e12) & ~ (e22 = e11) & ~ (e22 = e10) & ~ (e21 = e20) & ~ (e21 = e13) & ~ (e21 = e12) & ~ (e21 = e11) & ~ (e21 = e10) & ~ (e20 = e13) & ~ (e20 = e12) & ~ (e20 = e11) & ~ (e20 = e10) & ~ (e13 = e12) & ~ (e13 = e11) & ~ (e13 = e10) & ~ (e12 = e11) & ~ (e12 = e10) & ~ (e11 = e10) & op1(e13, e13) = all_0_111_111 & op1(e13, e12) = all_0_112_112 & op1(e13, e11) = all_0_113_113 & op1(e13, e10) = e12 & op1(e12, e13) = all_0_114_114 & op1(e12, e12) = all_0_115_115 & op1(e12, e11) = all_0_116_116 & op1(e12, e10) = e11 & op1(e11, e13) = all_0_117_117 & op1(e11, e12) = all_0_118_118 & op1(e11, e11) = all_0_119_119 & op1(e11, e10) = e10 & op1(e10, e13) = all_0_120_120 & op1(e10, e12) = all_0_121_121 & op1(e10, e11) = all_0_122_122 & op1(e10, e10) = e13 & h1(all_0_111_111) = all_0_81_81 & h1(all_0_112_112) = all_0_82_82 & h1(all_0_113_113) = all_0_83_83 & h1(all_0_114_114) = all_0_84_84 & h1(all_0_115_115) = all_0_85_85 & h1(all_0_116_116) = all_0_86_86 & h1(all_0_117_117) = all_0_87_87 & h1(all_0_118_118) = all_0_88_88 & h1(all_0_119_119) = all_0_89_89 & h1(all_0_120_120) = all_0_90_90 & h1(all_0_121_121) = all_0_91_91 & h1(all_0_122_122) = all_0_92_92 & h1(e13) = e23 & h1(e12) = e22 & h1(e11) = e21 & h1(e10) = e20 & h2(all_0_111_111) = all_0_55_55 & h2(all_0_112_112) = all_0_57_57 & h2(all_0_113_113) = all_0_59_59 & h2(all_0_114_114) = all_0_62_62 & h2(all_0_115_115) = all_0_64_64 & h2(all_0_116_116) = all_0_66_66 & h2(all_0_117_117) = all_0_69_69 & h2(all_0_118_118) = all_0_71_71 & h2(all_0_119_119) = all_0_73_73 & h2(all_0_120_120) = all_0_76_76 & h2(all_0_121_121) = all_0_78_78 & h2(all_0_122_122) = all_0_80_80 & h2(e13) = all_0_107_107 & h2(e12) = all_0_97_97 & h2(e11) = all_0_98_98 & h2(e10) = e21 & h3(all_0_111_111) = all_0_28_28 & h3(all_0_112_112) = all_0_30_30 & h3(all_0_113_113) = all_0_32_32 & h3(all_0_114_114) = all_0_35_35 & h3(all_0_115_115) = all_0_37_37 & h3(all_0_116_116) = all_0_39_39 & h3(all_0_117_117) = all_0_42_42 & h3(all_0_118_118) = all_0_44_44 & h3(all_0_119_119) = all_0_46_46 & h3(all_0_120_120) = all_0_49_49 & h3(all_0_121_121) = all_0_51_51 & h3(all_0_122_122) = all_0_53_53 & h3(e13) = all_0_103_103 & h3(e12) = all_0_95_95 & h3(e11) = all_0_96_96 & h3(e10) = e22 & h4(all_0_111_111) = all_0_1_1 & h4(all_0_112_112) = all_0_3_3 & h4(all_0_113_113) = all_0_5_5 & h4(all_0_114_114) = all_0_8_8 & h4(all_0_115_115) = all_0_10_10 & h4(all_0_116_116) = all_0_12_12 & h4(all_0_117_117) = all_0_15_15 & h4(all_0_118_118) = all_0_17_17 & h4(all_0_119_119) = all_0_19_19 & h4(all_0_120_120) = all_0_22_22 & h4(all_0_121_121) = all_0_24_24 & h4(all_0_122_122) = all_0_26_26 & h4(e13) = all_0_99_99 & h4(e12) = all_0_93_93 & h4(e11) = all_0_94_94 & h4(e10) = e23 & op2(all_0_93_93, all_0_93_93) = all_0_9_9 & op2(all_0_93_93, all_0_94_94) = all_0_11_11 & op2(all_0_93_93, all_0_99_99) = all_0_7_7 & op2(all_0_93_93, e23) = all_0_13_13 & op2(all_0_93_93, e23) = all_0_94_94 & op2(all_0_94_94, all_0_93_93) = all_0_16_16 & op2(all_0_94_94, all_0_94_94) = all_0_18_18 & op2(all_0_94_94, all_0_99_99) = all_0_14_14 & op2(all_0_94_94, e23) = all_0_20_20 & op2(all_0_95_95, all_0_95_95) = all_0_36_36 & op2(all_0_95_95, all_0_96_96) = all_0_38_38 & op2(all_0_95_95, all_0_103_103) = all_0_34_34 & op2(all_0_95_95, e22) = all_0_40_40 & op2(all_0_95_95, e22) = all_0_96_96 & op2(all_0_96_96, all_0_95_95) = all_0_43_43 & op2(all_0_96_96, all_0_96_96) = all_0_45_45 & op2(all_0_96_96, all_0_103_103) = all_0_41_41 & op2(all_0_96_96, e22) = all_0_47_47 & op2(all_0_97_97, all_0_97_97) = all_0_63_63 & op2(all_0_97_97, all_0_98_98) = all_0_65_65 & op2(all_0_97_97, all_0_107_107) = all_0_61_61 & op2(all_0_97_97, e21) = all_0_67_67 & op2(all_0_97_97, e21) = all_0_98_98 & op2(all_0_98_98, all_0_97_97) = all_0_70_70 & op2(all_0_98_98, all_0_98_98) = all_0_72_72 & op2(all_0_98_98, all_0_107_107) = all_0_68_68 & op2(all_0_98_98, e21) = all_0_74_74 & op2(all_0_99_99, all_0_93_93) = all_0_2_2 & op2(all_0_99_99, all_0_94_94) = all_0_4_4 & op2(all_0_99_99, all_0_99_99) = all_0_0_0 & op2(all_0_99_99, e23) = all_0_6_6 & op2(all_0_99_99, e23) = all_0_93_93 & op2(all_0_103_103, all_0_95_95) = all_0_29_29 & op2(all_0_103_103, all_0_96_96) = all_0_31_31 & op2(all_0_103_103, all_0_103_103) = all_0_27_27 & op2(all_0_103_103, e22) = all_0_33_33 & op2(all_0_103_103, e22) = all_0_95_95 & op2(all_0_107_107, all_0_97_97) = all_0_56_56 & op2(all_0_107_107, all_0_98_98) = all_0_58_58 & op2(all_0_107_107, all_0_107_107) = all_0_54_54 & op2(all_0_107_107, e21) = all_0_60_60 & op2(all_0_107_107, e21) = all_0_97_97 & op2(e23, all_0_93_93) = all_0_23_23 & op2(e23, all_0_94_94) = all_0_25_25 & op2(e23, all_0_99_99) = all_0_21_21 & op2(e23, e23) = all_0_99_99 & op2(e23, e22) = all_0_100_100 & op2(e23, e21) = all_0_101_101 & op2(e23, e20) = e22 & op2(e22, all_0_95_95) = all_0_50_50 & op2(e22, all_0_96_96) = all_0_52_52 & op2(e22, all_0_103_103) = all_0_48_48 & op2(e22, e23) = all_0_102_102 & op2(e22, e22) = all_0_103_103 & op2(e22, e21) = all_0_104_104 & op2(e22, e20) = e21 & op2(e21, all_0_97_97) = all_0_77_77 & op2(e21, all_0_98_98) = all_0_79_79 & op2(e21, all_0_107_107) = all_0_75_75 & op2(e21, e23) = all_0_105_105 & op2(e21, e22) = all_0_106_106 & op2(e21, e21) = all_0_107_107 & op2(e21, e20) = e20 & op2(e20, e23) = all_0_108_108 & op2(e20, e22) = all_0_109_109 & op2(e20, e21) = all_0_110_110 & op2(e20, e20) = e23 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op1(v3, v2) = v1) | ~ (op1(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op2(v3, v2) = v1) | ~ (op2(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h1(v2) = v1) | ~ (h1(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h2(v2) = v1) | ~ (h2(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h3(v2) = v1) | ~ (h3(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h4(v2) = v1) | ~ (h4(v2) = v0)) & ( ~ (all_0_0_0 = all_0_1_1) | ~ (all_0_2_2 = all_0_3_3) | ~ (all_0_4_4 = all_0_5_5) | ~ (all_0_6_6 = all_0_93_93) | ~ (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_94_94) | ~ (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 = e23) | ~ (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_93_93 = e22) & ~ (all_0_94_94 = e22)) | ( ~ (all_0_93_93 = e21) & ~ (all_0_94_94 = e21) & ~ (all_0_99_99 = e21)) | ( ~ (all_0_93_93 = e20) & ~ (all_0_94_94 = e20) & ~ (all_0_99_99 = e20))) & ( ~ (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_95_95) | ~ (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_96_96) | ~ (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 = e22) | ~ (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_95_95 = e23) & ~ (all_0_96_96 = e23) & ~ (all_0_103_103 = e23)) | ( ~ (all_0_95_95 = e21) & ~ (all_0_96_96 = e21)) | ( ~ (all_0_95_95 = e20) & ~ (all_0_96_96 = e20) & ~ (all_0_103_103 = e20))) & ( ~ (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_97_97) | ~ (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_98_98) | ~ (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 = e21) | ~ (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_97_97 = e23) & ~ (all_0_98_98 = e23) & ~ (all_0_107_107 = e23)) | ( ~ (all_0_97_97 = e22) & ~ (all_0_98_98 = e22) & ~ (all_0_107_107 = e22)) | ( ~ (all_0_97_97 = e20) & ~ (all_0_98_98 = e20))) & ( ~ (all_0_81_81 = all_0_99_99) | ~ (all_0_82_82 = all_0_100_100) | ~ (all_0_83_83 = all_0_101_101) | ~ (all_0_84_84 = all_0_102_102) | ~ (all_0_85_85 = all_0_103_103) | ~ (all_0_86_86 = all_0_104_104) | ~ (all_0_87_87 = all_0_105_105) | ~ (all_0_88_88 = all_0_106_106) | ~ (all_0_89_89 = all_0_107_107) | ~ (all_0_90_90 = all_0_108_108) | ~ (all_0_91_91 = all_0_109_109) | ~ (all_0_92_92 = all_0_110_110)) & (all_0_99_99 = e21 | all_0_99_99 = e20) & (all_0_99_99 = e21 | all_0_100_100 = e21 | all_0_101_101 = e21) & (all_0_99_99 = e21 | all_0_105_105 = e21 | all_0_108_108 = e21) & (all_0_99_99 = e20 | all_0_100_100 = e20 | all_0_101_101 = e20) & (all_0_99_99 = e20 | all_0_102_102 = e20 | all_0_108_108 = e20) & (all_0_100_100 = e23 | all_0_100_100 = e21 | all_0_100_100 = e20) & (all_0_100_100 = e23 | all_0_101_101 = e23) & (all_0_100_100 = e23 | all_0_103_103 = e23 | all_0_106_106 = e23) & (all_0_100_100 = e21 | all_0_106_106 = e21 | all_0_109_109 = e21) & (all_0_100_100 = e20 | all_0_103_103 = e20 | all_0_109_109 = e20) & (all_0_101_101 = e23 | all_0_101_101 = e21 | all_0_101_101 = e20) & (all_0_101_101 = e23 | all_0_104_104 = e23 | all_0_107_107 = e23) & (all_0_101_101 = e21 | all_0_110_110 = e21) & (all_0_101_101 = e20 | all_0_104_104 = e20 | all_0_110_110 = e20) & (all_0_102_102 = e23 | all_0_102_102 = e22 | all_0_102_102 = e20) & (all_0_102_102 = e23 | all_0_103_103 = e23 | all_0_104_104 = e23) & (all_0_102_102 = e23 | all_0_105_105 = e23) & (all_0_102_102 = e22 | all_0_104_104 = e22) & (all_0_102_102 = e22 | all_0_105_105 = e22 | all_0_108_108 = e22) & (all_0_102_102 = e20 | all_0_103_103 = e20 | all_0_104_104 = e20) & (all_0_103_103 = e23 | all_0_103_103 = e20) & (all_0_104_104 = e23 | all_0_104_104 = e22 | all_0_104_104 = e20) & (all_0_104_104 = e22 | all_0_107_107 = e22 | all_0_110_110 = e22) & (all_0_105_105 = e23 | all_0_105_105 = e22 | all_0_105_105 = e21) & (all_0_105_105 = e23 | all_0_106_106 = e23 | all_0_107_107 = e23) & (all_0_105_105 = e22 | all_0_106_106 = e22 | all_0_107_107 = e22) & (all_0_105_105 = e21 | all_0_106_106 = e21) & (all_0_106_106 = e23 | all_0_106_106 = e22 | all_0_106_106 = e21) & (all_0_106_106 = e22 | all_0_109_109 = e22) & (all_0_107_107 = e23 | all_0_107_107 = e22) & (all_0_108_108 = e22 | all_0_108_108 = e21 | all_0_108_108 = e20) & (all_0_108_108 = e22 | all_0_109_109 = e22 | all_0_110_110 = e22) & (all_0_108_108 = e21 | all_0_109_109 = e21 | all_0_110_110 = e21) & (all_0_108_108 = e20 | all_0_109_109 = e20 | all_0_110_110 = e20) & (all_0_109_109 = e22 | all_0_109_109 = e21 | all_0_109_109 = e20) & (all_0_110_110 = e22 | all_0_110_110 = e21 | all_0_110_110 = e20) & (all_0_111_111 = e11 | all_0_111_111 = e10) & (all_0_111_111 = e11 | all_0_112_112 = e11 | all_0_113_113 = e11) & (all_0_111_111 = e11 | all_0_117_117 = e11 | all_0_120_120 = e11) & (all_0_111_111 = e10 | all_0_112_112 = e10 | all_0_113_113 = e10) & (all_0_111_111 = e10 | all_0_114_114 = e10 | all_0_120_120 = e10) & (all_0_112_112 = e13 | all_0_112_112 = e11 | all_0_112_112 = e10) & (all_0_112_112 = e13 | all_0_113_113 = e13) & (all_0_112_112 = e13 | all_0_115_115 = e13 | all_0_118_118 = e13) & (all_0_112_112 = e11 | all_0_118_118 = e11 | all_0_121_121 = e11) & (all_0_112_112 = e10 | all_0_115_115 = e10 | all_0_121_121 = e10) & (all_0_113_113 = e13 | all_0_113_113 = e11 | all_0_113_113 = e10) & (all_0_113_113 = e13 | all_0_116_116 = e13 | all_0_119_119 = e13) & (all_0_113_113 = e11 | all_0_122_122 = e11) & (all_0_113_113 = e10 | all_0_116_116 = e10 | all_0_122_122 = e10) & (all_0_114_114 = e13 | all_0_114_114 = e12 | all_0_114_114 = e10) & (all_0_114_114 = e13 | all_0_115_115 = e13 | all_0_116_116 = e13) & (all_0_114_114 = e13 | all_0_117_117 = e13) & (all_0_114_114 = e12 | all_0_116_116 = e12) & (all_0_114_114 = e12 | all_0_117_117 = e12 | all_0_120_120 = e12) & (all_0_114_114 = e10 | all_0_115_115 = e10 | all_0_116_116 = e10) & (all_0_115_115 = e13 | all_0_115_115 = e10) & (all_0_116_116 = e13 | all_0_116_116 = e12 | all_0_116_116 = e10) & (all_0_116_116 = e12 | all_0_119_119 = e12 | all_0_122_122 = e12) & (all_0_117_117 = e13 | all_0_117_117 = e12 | all_0_117_117 = e11) & (all_0_117_117 = e13 | all_0_118_118 = e13 | all_0_119_119 = e13) & (all_0_117_117 = e12 | all_0_118_118 = e12 | all_0_119_119 = e12) & (all_0_117_117 = e11 | all_0_118_118 = e11) & (all_0_118_118 = e13 | all_0_118_118 = e12 | all_0_118_118 = e11) & (all_0_118_118 = e12 | all_0_121_121 = e12) & (all_0_119_119 = e13 | all_0_119_119 = e12) & (all_0_120_120 = e12 | all_0_120_120 = e11 | all_0_120_120 = e10) & (all_0_120_120 = e12 | all_0_121_121 = e12 | all_0_122_122 = e12) & (all_0_120_120 = e11 | all_0_121_121 = e11 | all_0_122_122 = e11) & (all_0_120_120 = e10 | all_0_121_121 = e10 | all_0_122_122 = e10) & (all_0_121_121 = e12 | all_0_121_121 = e11 | all_0_121_121 = e10) & (all_0_122_122 = e12 | all_0_122_122 = e11 | all_0_122_122 = e10) & ((all_0_100_100 = e20 & ~ (all_0_104_104 = e22) & ~ (all_0_108_108 = e22) & ( ~ (all_0_102_102 = e22) | all_0_103_103 = e23) & ( ~ (all_0_105_105 = e22) | all_0_106_106 = e23) & ( ~ (all_0_107_107 = e22) | all_0_106_106 = e21) & ( ~ (all_0_110_110 = e22) | all_0_109_109 = e21)) | (all_0_104_104 = e20 & ~ (all_0_100_100 = e21) & ~ (all_0_108_108 = e21) & ( ~ (all_0_99_99 = e21) | all_0_101_101 = e23) & ( ~ (all_0_105_105 = e21) | all_0_107_107 = e23) & ( ~ (all_0_106_106 = e21) | all_0_107_107 = e22) & ( ~ (all_0_109_109 = e21) | all_0_110_110 = e22)) | (all_0_108_108 = e20 & ~ (all_0_100_100 = e23) & ~ (all_0_104_104 = e23) & ( ~ (all_0_101_101 = e23) | all_0_99_99 = e21) & ( ~ (all_0_103_103 = e23) | all_0_102_102 = e22) & ( ~ (all_0_106_106 = e23) | all_0_105_105 = e22) & ( ~ (all_0_107_107 = e23) | all_0_105_105 = e21)) | ( ~ (all_0_99_99 = e20) & ~ (all_0_101_101 = e20) & ~ (all_0_102_102 = e20) & ~ (all_0_103_103 = e20) & ~ (all_0_109_109 = e20) & ~ (all_0_110_110 = e20))) & ((all_0_112_112 = e10 & ~ (all_0_116_116 = e12) & ~ (all_0_120_120 = e12) & ( ~ (all_0_114_114 = e12) | all_0_115_115 = e13) & ( ~ (all_0_117_117 = e12) | all_0_118_118 = e13) & ( ~ (all_0_119_119 = e12) | all_0_118_118 = e11) & ( ~ (all_0_122_122 = e12) | all_0_121_121 = e11)) | (all_0_116_116 = e10 & ~ (all_0_112_112 = e11) & ~ (all_0_120_120 = e11) & ( ~ (all_0_111_111 = e11) | all_0_113_113 = e13) & ( ~ (all_0_117_117 = e11) | all_0_119_119 = e13) & ( ~ (all_0_118_118 = e11) | all_0_119_119 = e12) & ( ~ (all_0_121_121 = e11) | all_0_122_122 = e12)) | (all_0_120_120 = e10 & ~ (all_0_112_112 = e13) & ~ (all_0_116_116 = e13) & ( ~ (all_0_113_113 = e13) | all_0_111_111 = e11) & ( ~ (all_0_115_115 = e13) | all_0_114_114 = e12) & ( ~ (all_0_118_118 = e13) | all_0_117_117 = e12) & ( ~ (all_0_119_119 = e13) | all_0_117_117 = e11)) | ( ~ (all_0_111_111 = e10) & ~ (all_0_113_113 = e10) & ~ (all_0_114_114 = e10) & ~ (all_0_115_115 = e10) & ~ (all_0_121_121 = e10) & ~ (all_0_122_122 = e10))) % 15.12/4.24 | % 15.12/4.24 | Applying alpha-rule on (1) yields: % 15.58/4.24 | (2) all_0_120_120 = e12 | all_0_121_121 = e12 | all_0_122_122 = e12 % 15.58/4.24 | (3) h4(all_0_122_122) = all_0_26_26 % 15.58/4.25 | (4) all_0_118_118 = e13 | all_0_118_118 = e12 | all_0_118_118 = e11 % 15.58/4.25 | (5) ~ (all_0_111_111 = all_0_117_117) % 15.58/4.25 | (6) op2(all_0_95_95, all_0_96_96) = all_0_38_38 % 15.58/4.25 | (7) ~ (e22 = e13) % 15.58/4.25 | (8) op2(e22, e20) = e21 % 15.58/4.25 | (9) all_0_114_114 = e13 | all_0_117_117 = e13 % 15.58/4.25 | (10) h4(all_0_121_121) = all_0_24_24 % 15.58/4.25 | (11) op2(all_0_96_96, all_0_103_103) = all_0_41_41 % 15.58/4.25 | (12) h4(all_0_117_117) = all_0_15_15 % 15.58/4.25 | (13) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h1(v2) = v1) | ~ (h1(v2) = v0)) % 15.58/4.25 | (14) all_0_119_119 = e13 | all_0_119_119 = e12 % 15.58/4.25 | (15) all_0_105_105 = e23 | all_0_105_105 = e22 | all_0_105_105 = e21 % 15.58/4.25 | (16) ~ (all_0_118_118 = all_0_121_121) % 15.58/4.25 | (17) ~ (all_0_120_120 = all_0_122_122) % 15.58/4.25 | (18) ~ (all_0_109_109 = e23) % 15.58/4.25 | (19) h4(all_0_118_118) = all_0_17_17 % 15.58/4.25 | (20) all_0_101_101 = e23 | all_0_104_104 = e23 | all_0_107_107 = e23 % 15.58/4.25 | (21) ~ (all_0_115_115 = all_0_118_118) % 15.58/4.25 | (22) h2(all_0_116_116) = all_0_66_66 % 15.58/4.25 | (23) op2(e22, all_0_103_103) = all_0_48_48 % 15.58/4.25 | (24) op2(all_0_95_95, all_0_103_103) = all_0_34_34 % 15.58/4.25 | (25) all_0_108_108 = e21 | all_0_109_109 = e21 | all_0_110_110 = e21 % 15.58/4.25 | (26) op2(all_0_107_107, all_0_107_107) = all_0_54_54 % 15.58/4.25 | (27) all_0_118_118 = e12 | all_0_121_121 = e12 % 15.58/4.25 | (28) ~ (all_0_103_103 = e21) % 15.58/4.25 | (29) ~ (all_0_113_113 = all_0_122_122) % 15.58/4.25 | (30) ~ (e21 = e11) % 15.58/4.25 | (31) op2(all_0_94_94, all_0_99_99) = all_0_14_14 % 15.58/4.25 | (32) ~ (all_0_108_108 = all_0_109_109) % 15.58/4.25 | (33) h3(e11) = all_0_96_96 % 15.58/4.25 | (34) ~ (all_0_102_102 = all_0_108_108) % 15.58/4.25 | (35) all_0_99_99 = e21 | all_0_99_99 = e20 % 15.58/4.25 | (36) all_0_111_111 = e11 | all_0_117_117 = e11 | all_0_120_120 = e11 % 15.58/4.25 | (37) op1(e10, e13) = all_0_120_120 % 15.58/4.25 | (38) all_0_116_116 = e12 | all_0_119_119 = e12 | all_0_122_122 = e12 % 15.58/4.25 | (39) h2(e11) = all_0_98_98 % 15.58/4.25 | (40) h2(all_0_115_115) = all_0_64_64 % 15.58/4.25 | (41) op2(all_0_99_99, e23) = all_0_6_6 % 15.58/4.25 | (42) ~ (all_0_101_101 = all_0_107_107) % 15.58/4.25 | (43) all_0_117_117 = e13 | all_0_118_118 = e13 | all_0_119_119 = e13 % 15.58/4.25 | (44) op2(e21, all_0_97_97) = all_0_77_77 % 15.58/4.25 | (45) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h2(v2) = v1) | ~ (h2(v2) = v0)) % 15.58/4.25 | (46) h3(all_0_122_122) = all_0_53_53 % 15.58/4.25 | (47) all_0_104_104 = e22 | all_0_107_107 = e22 | all_0_110_110 = e22 % 15.58/4.25 | (48) ~ (all_0_101_101 = all_0_110_110) % 15.58/4.25 | (49) h1(all_0_119_119) = all_0_89_89 % 15.58/4.25 | (50) h1(all_0_118_118) = all_0_88_88 % 15.58/4.25 | (51) all_0_113_113 = e10 | all_0_116_116 = e10 | all_0_122_122 = e10 % 15.58/4.25 | (52) ~ (all_0_119_119 = e10) % 15.58/4.25 | (53) h1(all_0_121_121) = all_0_91_91 % 15.58/4.25 | (54) ~ (all_0_121_121 = e13) % 15.58/4.25 | (55) op2(e23, all_0_94_94) = all_0_25_25 % 15.58/4.25 | (56) op2(e23, e23) = all_0_99_99 % 15.58/4.25 | (57) ~ (all_0_113_113 = e12) % 15.58/4.25 | (58) ~ (all_0_107_107 = e21) % 15.58/4.25 | (59) op2(all_0_99_99, e23) = all_0_93_93 % 15.58/4.25 | (60) op2(all_0_98_98, all_0_97_97) = all_0_70_70 % 15.58/4.25 | (61) ~ (all_0_100_100 = all_0_109_109) % 15.58/4.25 | (62) ~ (all_0_99_99 = e22) % 15.58/4.25 | (63) op2(e22, e22) = all_0_103_103 % 15.58/4.25 | (64) op1(e12, e10) = e11 % 15.58/4.25 | (65) all_0_102_102 = e20 | all_0_103_103 = e20 | all_0_104_104 = e20 % 15.58/4.25 | (66) h3(e12) = all_0_95_95 % 15.58/4.25 | (67) ~ (all_0_101_101 = e22) % 15.58/4.25 | (68) h1(all_0_120_120) = all_0_90_90 % 15.58/4.25 | (69) h3(all_0_115_115) = all_0_37_37 % 15.58/4.25 | (70) op2(e21, all_0_98_98) = all_0_79_79 % 15.58/4.26 | (71) ~ (e12 = e11) % 15.58/4.26 | (72) op2(all_0_95_95, e22) = all_0_40_40 % 15.58/4.26 | (73) op2(all_0_96_96, all_0_96_96) = all_0_45_45 % 15.58/4.26 | (74) op2(all_0_103_103, all_0_96_96) = all_0_31_31 % 15.58/4.26 | (75) all_0_100_100 = e23 | all_0_101_101 = e23 % 15.58/4.26 | (76) op1(e13, e13) = all_0_111_111 % 15.58/4.26 | (77) op1(e10, e12) = all_0_121_121 % 15.58/4.26 | (78) h2(all_0_114_114) = all_0_62_62 % 15.58/4.26 | (79) ~ (e23 = e10) % 15.58/4.26 | (80) all_0_114_114 = e10 | all_0_115_115 = e10 | all_0_116_116 = e10 % 15.58/4.26 | (81) all_0_111_111 = e10 | all_0_114_114 = e10 | all_0_120_120 = e10 % 15.58/4.26 | (82) op2(e21, e23) = all_0_105_105 % 15.58/4.26 | (83) h2(all_0_117_117) = all_0_69_69 % 15.58/4.26 | (84) op2(all_0_103_103, e22) = all_0_95_95 % 15.58/4.26 | (85) h1(all_0_114_114) = all_0_84_84 % 15.58/4.26 | (86) op2(all_0_97_97, all_0_97_97) = all_0_63_63 % 15.58/4.26 | (87) ~ (e23 = e13) % 15.58/4.26 | (88) h3(all_0_120_120) = all_0_49_49 % 15.58/4.26 | (89) ~ (e13 = e10) % 15.58/4.26 | (90) all_0_114_114 = e13 | all_0_115_115 = e13 | all_0_116_116 = e13 % 15.58/4.26 | (91) ~ (all_0_111_111 = all_0_114_114) % 15.58/4.26 | (92) h3(e13) = all_0_103_103 % 15.58/4.26 | (93) all_0_103_103 = e23 | all_0_103_103 = e20 % 15.58/4.26 | (94) op2(all_0_93_93, all_0_99_99) = all_0_7_7 % 15.58/4.26 | (95) ~ (all_0_108_108 = e23) % 15.58/4.26 | (96) op2(e23, e22) = all_0_100_100 % 15.58/4.26 | (97) h4(all_0_115_115) = all_0_10_10 % 15.58/4.26 | (98) ~ (all_0_114_114 = all_0_120_120) % 15.58/4.26 | (99) ~ (all_0_111_111 = e13) % 15.58/4.26 | (100) ~ (all_0_100_100 = all_0_103_103) % 15.58/4.26 | (101) all_0_117_117 = e13 | all_0_117_117 = e12 | all_0_117_117 = e11 % 15.58/4.26 | (102) h4(e11) = all_0_94_94 % 15.58/4.26 | (103) ~ (e20 = e11) % 15.58/4.26 | (104) op2(e23, e20) = e22 % 15.58/4.26 | (105) all_0_112_112 = e13 | all_0_113_113 = e13 % 15.58/4.26 | (106) ~ (e21 = e13) % 15.58/4.26 | (107) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h3(v2) = v1) | ~ (h3(v2) = v0)) % 15.58/4.26 | (108) ~ (all_0_118_118 = all_0_119_119) % 15.58/4.26 | (109) ~ (all_0_102_102 = all_0_104_104) % 15.58/4.26 | (110) ~ (e23 = e21) % 15.58/4.26 | (111) ~ (all_0_115_115 = e11) % 15.58/4.26 | (112) op2(e20, e20) = e23 % 15.58/4.26 | (113) h1(all_0_111_111) = all_0_81_81 % 15.58/4.26 | (114) all_0_114_114 = e12 | all_0_116_116 = e12 % 15.58/4.26 | (115) all_0_99_99 = e20 | all_0_102_102 = e20 | all_0_108_108 = e20 % 15.58/4.26 | (116) ~ (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_95_95) | ~ (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_96_96) | ~ (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 = e22) | ~ (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_95_95 = e23) & ~ (all_0_96_96 = e23) & ~ (all_0_103_103 = e23)) | ( ~ (all_0_95_95 = e21) & ~ (all_0_96_96 = e21)) | ( ~ (all_0_95_95 = e20) & ~ (all_0_96_96 = e20) & ~ (all_0_103_103 = e20)) % 15.58/4.26 | (117) ~ (all_0_104_104 = all_0_107_107) % 15.58/4.26 | (118) all_0_106_106 = e23 | all_0_106_106 = e22 | all_0_106_106 = e21 % 15.58/4.26 | (119) op2(all_0_103_103, all_0_103_103) = all_0_27_27 % 15.58/4.26 | (120) ~ (e12 = e10) % 15.58/4.26 | (121) h2(all_0_112_112) = all_0_57_57 % 15.58/4.26 | (122) all_0_114_114 = e12 | all_0_117_117 = e12 | all_0_120_120 = e12 % 15.58/4.26 | (123) h4(all_0_120_120) = all_0_22_22 % 15.58/4.26 | (124) all_0_112_112 = e10 | all_0_115_115 = e10 | all_0_121_121 = e10 % 15.58/4.26 | (125) h2(all_0_122_122) = all_0_80_80 % 15.58/4.26 | (126) op2(all_0_107_107, all_0_97_97) = all_0_56_56 % 15.58/4.26 | (127) ~ (all_0_105_105 = all_0_106_106) % 15.58/4.26 | (128) h4(e10) = e23 % 15.58/4.26 | (129) ~ (all_0_99_99 = e23) % 15.58/4.26 | (130) ~ (all_0_106_106 = e20) % 15.58/4.26 | (131) h3(all_0_112_112) = all_0_30_30 % 15.58/4.26 | (132) h2(e13) = all_0_107_107 % 15.58/4.26 | (133) ~ (all_0_117_117 = e10) % 15.58/4.26 | (134) ~ (all_0_112_112 = e12) % 15.58/4.27 | (135) ~ (all_0_100_100 = all_0_106_106) % 15.58/4.27 | (136) op2(all_0_97_97, all_0_98_98) = all_0_65_65 % 15.58/4.27 | (137) ~ (e21 = e10) % 15.58/4.27 | (138) ~ (all_0_115_115 = all_0_121_121) % 15.58/4.27 | (139) ~ (e21 = e20) % 15.58/4.27 | (140) h3(all_0_121_121) = all_0_51_51 % 15.58/4.27 | (141) op2(all_0_94_94, e23) = all_0_20_20 % 15.58/4.27 | (142) h4(all_0_119_119) = all_0_19_19 % 15.58/4.27 | (143) ~ (all_0_114_114 = e11) % 15.58/4.27 | (144) ~ (all_0_111_111 = all_0_112_112) % 15.58/4.27 | (145) ~ (all_0_107_107 = all_0_110_110) % 15.58/4.27 | (146) op2(e21, all_0_107_107) = all_0_75_75 % 15.58/4.27 | (147) h2(all_0_121_121) = all_0_78_78 % 15.58/4.27 | (148) op2(all_0_98_98, e21) = all_0_74_74 % 15.58/4.27 | (149) op1(e11, e10) = e10 % 15.58/4.27 | (150) all_0_117_117 = e11 | all_0_118_118 = e11 % 15.58/4.27 | (151) all_0_101_101 = e23 | all_0_101_101 = e21 | all_0_101_101 = e20 % 15.58/4.27 | (152) ~ (e20 = e12) % 15.58/4.27 | (153) op1(e11, e11) = all_0_119_119 % 15.58/4.27 | (154) op2(all_0_98_98, all_0_107_107) = all_0_68_68 % 15.58/4.27 | (155) all_0_112_112 = e13 | all_0_112_112 = e11 | all_0_112_112 = e10 % 15.58/4.27 | (156) (all_0_112_112 = e10 & ~ (all_0_116_116 = e12) & ~ (all_0_120_120 = e12) & ( ~ (all_0_114_114 = e12) | all_0_115_115 = e13) & ( ~ (all_0_117_117 = e12) | all_0_118_118 = e13) & ( ~ (all_0_119_119 = e12) | all_0_118_118 = e11) & ( ~ (all_0_122_122 = e12) | all_0_121_121 = e11)) | (all_0_116_116 = e10 & ~ (all_0_112_112 = e11) & ~ (all_0_120_120 = e11) & ( ~ (all_0_111_111 = e11) | all_0_113_113 = e13) & ( ~ (all_0_117_117 = e11) | all_0_119_119 = e13) & ( ~ (all_0_118_118 = e11) | all_0_119_119 = e12) & ( ~ (all_0_121_121 = e11) | all_0_122_122 = e12)) | (all_0_120_120 = e10 & ~ (all_0_112_112 = e13) & ~ (all_0_116_116 = e13) & ( ~ (all_0_113_113 = e13) | all_0_111_111 = e11) & ( ~ (all_0_115_115 = e13) | all_0_114_114 = e12) & ( ~ (all_0_118_118 = e13) | all_0_117_117 = e12) & ( ~ (all_0_119_119 = e13) | all_0_117_117 = e11)) | ( ~ (all_0_111_111 = e10) & ~ (all_0_113_113 = e10) & ~ (all_0_114_114 = e10) & ~ (all_0_115_115 = e10) & ~ (all_0_121_121 = e10) & ~ (all_0_122_122 = e10)) % 15.58/4.27 | (157) h2(e12) = all_0_97_97 % 15.58/4.27 | (158) op2(e20, e22) = all_0_109_109 % 15.58/4.27 | (159) (all_0_100_100 = e20 & ~ (all_0_104_104 = e22) & ~ (all_0_108_108 = e22) & ( ~ (all_0_102_102 = e22) | all_0_103_103 = e23) & ( ~ (all_0_105_105 = e22) | all_0_106_106 = e23) & ( ~ (all_0_107_107 = e22) | all_0_106_106 = e21) & ( ~ (all_0_110_110 = e22) | all_0_109_109 = e21)) | (all_0_104_104 = e20 & ~ (all_0_100_100 = e21) & ~ (all_0_108_108 = e21) & ( ~ (all_0_99_99 = e21) | all_0_101_101 = e23) & ( ~ (all_0_105_105 = e21) | all_0_107_107 = e23) & ( ~ (all_0_106_106 = e21) | all_0_107_107 = e22) & ( ~ (all_0_109_109 = e21) | all_0_110_110 = e22)) | (all_0_108_108 = e20 & ~ (all_0_100_100 = e23) & ~ (all_0_104_104 = e23) & ( ~ (all_0_101_101 = e23) | all_0_99_99 = e21) & ( ~ (all_0_103_103 = e23) | all_0_102_102 = e22) & ( ~ (all_0_106_106 = e23) | all_0_105_105 = e22) & ( ~ (all_0_107_107 = e23) | all_0_105_105 = e21)) | ( ~ (all_0_99_99 = e20) & ~ (all_0_101_101 = e20) & ~ (all_0_102_102 = e20) & ~ (all_0_103_103 = e20) & ~ (all_0_109_109 = e20) & ~ (all_0_110_110 = e20)) % 15.58/4.27 | (160) ~ (all_0_103_103 = all_0_109_109) % 15.58/4.27 | (161) ~ (all_0_112_112 = all_0_121_121) % 15.58/4.27 | (162) all_0_106_106 = e22 | all_0_109_109 = e22 % 15.58/4.27 | (163) ~ (all_0_105_105 = all_0_108_108) % 15.58/4.27 | (164) op2(all_0_107_107, e21) = all_0_97_97 % 15.58/4.27 | (165) ~ (all_0_99_99 = all_0_102_102) % 15.58/4.27 | (166) op2(all_0_94_94, all_0_94_94) = all_0_18_18 % 15.58/4.27 | (167) ~ (all_0_103_103 = all_0_104_104) % 15.58/4.27 | (168) ~ (e23 = e22) % 15.58/4.27 | (169) h1(e12) = e22 % 15.58/4.27 | (170) op1(e12, e13) = all_0_114_114 % 15.58/4.27 | (171) op1(e13, e12) = all_0_112_112 % 15.58/4.27 | (172) all_0_111_111 = e10 | all_0_112_112 = e10 | all_0_113_113 = e10 % 15.58/4.27 | (173) ~ (e22 = e10) % 15.58/4.27 | (174) op2(all_0_93_93, e23) = all_0_94_94 % 15.58/4.27 | (175) h3(e10) = e22 % 15.58/4.27 | (176) ~ (all_0_105_105 = e20) % 15.58/4.27 | (177) ~ (all_0_102_102 = all_0_105_105) % 15.58/4.27 | (178) op2(e22, e23) = all_0_102_102 % 15.58/4.27 | (179) all_0_100_100 = e21 | all_0_106_106 = e21 | all_0_109_109 = e21 % 15.58/4.27 | (180) all_0_115_115 = e13 | all_0_115_115 = e10 % 15.58/4.27 | (181) op2(all_0_93_93, e23) = all_0_13_13 % 15.58/4.27 | (182) ~ (all_0_101_101 = all_0_104_104) % 15.58/4.27 | (183) op2(all_0_99_99, all_0_94_94) = all_0_4_4 % 15.58/4.27 | (184) h3(all_0_119_119) = all_0_46_46 % 15.58/4.27 | (185) h3(all_0_111_111) = all_0_28_28 % 15.58/4.27 | (186) all_0_105_105 = e23 | all_0_106_106 = e23 | all_0_107_107 = e23 % 15.58/4.27 | (187) ~ (all_0_116_116 = e11) % 15.58/4.27 | (188) ~ (all_0_111_111 = all_0_120_120) % 15.58/4.27 | (189) op2(all_0_99_99, all_0_93_93) = all_0_2_2 % 15.58/4.27 | (190) op1(e10, e11) = all_0_122_122 % 15.58/4.28 | (191) ~ (all_0_120_120 = all_0_121_121) % 15.58/4.28 | (192) all_0_121_121 = e12 | all_0_121_121 = e11 | all_0_121_121 = e10 % 15.58/4.28 | (193) all_0_102_102 = e23 | all_0_102_102 = e22 | all_0_102_102 = e20 % 15.58/4.28 | (194) h2(all_0_118_118) = all_0_71_71 % 15.58/4.28 | (195) all_0_102_102 = e22 | all_0_105_105 = e22 | all_0_108_108 = e22 % 15.58/4.28 | (196) op2(all_0_93_93, all_0_93_93) = all_0_9_9 % 15.58/4.28 | (197) h2(all_0_111_111) = all_0_55_55 % 15.58/4.28 | (198) all_0_116_116 = e13 | all_0_116_116 = e12 | all_0_116_116 = e10 % 15.58/4.28 | (199) op2(all_0_96_96, e22) = all_0_47_47 % 15.58/4.28 | (200) h2(all_0_119_119) = all_0_73_73 % 15.58/4.28 | (201) ~ (all_0_111_111 = all_0_113_113) % 15.58/4.28 | (202) op2(e23, all_0_93_93) = all_0_23_23 % 15.58/4.28 | (203) all_0_102_102 = e23 | all_0_105_105 = e23 % 15.58/4.28 | (204) ~ (e23 = e12) % 15.58/4.28 | (205) op1(e13, e11) = all_0_113_113 % 15.58/4.28 | (206) op2(all_0_96_96, all_0_95_95) = all_0_43_43 % 15.58/4.28 | (207) all_0_120_120 = e12 | all_0_120_120 = e11 | all_0_120_120 = e10 % 15.58/4.28 | (208) ~ (all_0_115_115 = e12) % 15.58/4.28 | (209) op2(e22, all_0_95_95) = all_0_50_50 % 15.58/4.28 | (210) all_0_100_100 = e23 | all_0_100_100 = e21 | all_0_100_100 = e20 % 15.58/4.28 | (211) op1(e11, e12) = all_0_118_118 % 15.58/4.28 | (212) all_0_112_112 = e11 | all_0_118_118 = e11 | all_0_121_121 = e11 % 15.58/4.28 | (213) ~ (all_0_116_116 = all_0_122_122) % 15.58/4.28 | (214) ~ (all_0_106_106 = all_0_109_109) % 15.58/4.28 | (215) all_0_120_120 = e10 | all_0_121_121 = e10 | all_0_122_122 = e10 % 15.58/4.28 | (216) all_0_113_113 = e13 | all_0_113_113 = e11 | all_0_113_113 = e10 % 15.58/4.28 | (217) op2(e22, all_0_96_96) = all_0_52_52 % 15.58/4.28 | (218) ~ (e23 = e20) % 15.58/4.28 | (219) h4(e12) = all_0_93_93 % 15.58/4.28 | (220) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op2(v3, v2) = v1) | ~ (op2(v3, v2) = v0)) % 15.58/4.28 | (221) ~ (e22 = e20) % 15.58/4.28 | (222) all_0_108_108 = e22 | all_0_109_109 = e22 | all_0_110_110 = e22 % 15.58/4.28 | (223) ~ (all_0_99_99 = all_0_105_105) % 15.58/4.28 | (224) ~ (all_0_114_114 = all_0_117_117) % 15.58/4.28 | (225) ~ (all_0_113_113 = all_0_116_116) % 15.58/4.28 | (226) ~ (all_0_120_120 = e13) % 15.58/4.28 | (227) ~ (e11 = e10) % 15.58/4.28 | (228) all_0_104_104 = e23 | all_0_104_104 = e22 | all_0_104_104 = e20 % 15.58/4.28 | (229) h1(all_0_112_112) = all_0_82_82 % 15.58/4.28 | (230) ~ (all_0_121_121 = all_0_122_122) % 15.58/4.28 | (231) ~ (e21 = e12) % 15.58/4.28 | (232) ~ (all_0_112_112 = all_0_113_113) % 15.58/4.28 | (233) op2(all_0_97_97, e21) = all_0_67_67 % 15.58/4.28 | (234) all_0_111_111 = e11 | all_0_111_111 = e10 % 15.58/4.28 | (235) all_0_102_102 = e23 | all_0_103_103 = e23 | all_0_104_104 = e23 % 15.58/4.28 | (236) h1(e13) = e23 % 15.58/4.28 | (237) h2(e10) = e21 % 15.58/4.28 | (238) h3(all_0_118_118) = all_0_44_44 % 15.58/4.28 | (239) h3(all_0_113_113) = all_0_32_32 % 15.58/4.28 | (240) all_0_102_102 = e22 | all_0_104_104 = e22 % 15.58/4.28 | (241) h1(all_0_113_113) = all_0_83_83 % 15.58/4.28 | (242) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h4(v2) = v1) | ~ (h4(v2) = v0)) % 15.58/4.28 | (243) ~ (all_0_119_119 = all_0_122_122) % 15.58/4.28 | (244) ~ (all_0_99_99 = all_0_101_101) % 15.58/4.28 | (245) ~ (e22 = e11) % 15.58/4.28 | (246) ~ (e20 = e10) % 15.58/4.28 | (247) ~ (all_0_100_100 = e22) % 15.58/4.28 | (248) op2(all_0_103_103, e22) = all_0_33_33 % 15.58/4.28 | (249) op2(e23, all_0_99_99) = all_0_21_21 % 15.58/4.28 | (250) h3(all_0_116_116) = all_0_39_39 % 15.58/4.28 | (251) all_0_112_112 = e13 | all_0_115_115 = e13 | all_0_118_118 = e13 % 15.58/4.28 | (252) ~ (all_0_117_117 = all_0_120_120) % 15.58/4.28 | (253) all_0_107_107 = e23 | all_0_107_107 = e22 % 15.58/4.28 | (254) all_0_105_105 = e21 | all_0_106_106 = e21 % 15.58/4.28 | (255) all_0_100_100 = e20 | all_0_103_103 = e20 | all_0_109_109 = e20 % 15.58/4.28 | (256) all_0_100_100 = e23 | all_0_103_103 = e23 | all_0_106_106 = e23 % 15.58/4.28 | (257) ~ (all_0_102_102 = e21) % 15.58/4.28 | (258) all_0_99_99 = e21 | all_0_100_100 = e21 | all_0_101_101 = e21 % 15.58/4.28 | (259) op1(e11, e13) = all_0_117_117 % 15.58/4.29 | (260) h2(all_0_120_120) = all_0_76_76 % 15.58/4.29 | (261) ~ (all_0_105_105 = all_0_107_107) % 15.58/4.29 | (262) all_0_114_114 = e13 | all_0_114_114 = e12 | all_0_114_114 = e10 % 15.58/4.29 | (263) h4(all_0_116_116) = all_0_12_12 % 15.58/4.29 | (264) all_0_99_99 = e21 | all_0_105_105 = e21 | all_0_108_108 = e21 % 15.58/4.29 | (265) op2(all_0_94_94, all_0_93_93) = all_0_16_16 % 15.58/4.29 | (266) h1(all_0_117_117) = all_0_87_87 % 15.58/4.29 | (267) all_0_109_109 = e22 | all_0_109_109 = e21 | all_0_109_109 = e20 % 15.58/4.29 | (268) h4(all_0_111_111) = all_0_1_1 % 15.58/4.29 | (269) h1(all_0_115_115) = all_0_85_85 % 15.58/4.29 | (270) ~ (all_0_104_104 = e21) % 15.58/4.29 | (271) ~ (all_0_111_111 = e12) % 15.58/4.29 | (272) ~ (all_0_119_119 = e11) % 15.58/4.29 | (273) ~ (all_0_110_110 = e23) % 15.58/4.29 | (274) op2(all_0_93_93, all_0_94_94) = all_0_11_11 % 15.58/4.29 | (275) h4(all_0_114_114) = all_0_8_8 % 15.58/4.29 | (276) ~ (all_0_100_100 = all_0_101_101) % 15.58/4.29 | (277) op2(all_0_98_98, all_0_98_98) = all_0_72_72 % 15.58/4.29 | (278) all_0_120_120 = e11 | all_0_121_121 = e11 | all_0_122_122 = e11 % 15.58/4.29 | (279) ~ (all_0_116_116 = all_0_119_119) % 15.58/4.29 | (280) all_0_113_113 = e13 | all_0_116_116 = e13 | all_0_119_119 = e13 % 15.58/4.29 | (281) h1(all_0_122_122) = all_0_92_92 % 15.58/4.29 | (282) ~ (e13 = e12) % 15.58/4.29 | (283) all_0_117_117 = e12 | all_0_118_118 = e12 | all_0_119_119 = e12 % 15.58/4.29 | (284) ~ (all_0_113_113 = all_0_119_119) % 15.58/4.29 | (285) ~ (e22 = e21) % 15.58/4.29 | (286) ~ (all_0_115_115 = all_0_116_116) % 15.58/4.29 | (287) ~ (all_0_122_122 = e13) % 15.58/4.29 | (288) h4(all_0_113_113) = all_0_5_5 % 15.58/4.29 | (289) ~ (all_0_109_109 = all_0_110_110) % 15.58/4.29 | (290) op1(e12, e11) = all_0_116_116 % 15.79/4.29 | (291) all_0_105_105 = e22 | all_0_106_106 = e22 | all_0_107_107 = e22 % 15.79/4.29 | (292) op2(e22, e21) = all_0_104_104 % 15.79/4.29 | (293) op2(all_0_95_95, all_0_95_95) = all_0_36_36 % 15.79/4.29 | (294) ~ (e22 = e12) % 15.79/4.29 | (295) ~ (e20 = e13) % 15.79/4.29 | (296) op2(e20, e23) = all_0_108_108 % 15.79/4.29 | (297) ~ (all_0_114_114 = all_0_116_116) % 15.79/4.29 | (298) h3(all_0_117_117) = all_0_42_42 % 15.79/4.29 | (299) ~ (all_0_81_81 = all_0_99_99) | ~ (all_0_82_82 = all_0_100_100) | ~ (all_0_83_83 = all_0_101_101) | ~ (all_0_84_84 = all_0_102_102) | ~ (all_0_85_85 = all_0_103_103) | ~ (all_0_86_86 = all_0_104_104) | ~ (all_0_87_87 = all_0_105_105) | ~ (all_0_88_88 = all_0_106_106) | ~ (all_0_89_89 = all_0_107_107) | ~ (all_0_90_90 = all_0_108_108) | ~ (all_0_91_91 = all_0_109_109) | ~ (all_0_92_92 = all_0_110_110) % 15.79/4.29 | (300) ~ (all_0_99_99 = all_0_100_100) % 15.79/4.29 | (301) op2(all_0_107_107, all_0_98_98) = all_0_58_58 % 15.79/4.29 | (302) all_0_108_108 = e20 | all_0_109_109 = e20 | all_0_110_110 = e20 % 15.79/4.29 | (303) op2(all_0_95_95, e22) = all_0_96_96 % 15.79/4.29 | (304) ~ (all_0_118_118 = e10) % 15.79/4.29 | (305) op2(all_0_99_99, all_0_99_99) = all_0_0_0 % 15.79/4.29 | (306) ~ (e23 = e11) % 15.79/4.29 | (307) ~ (all_0_106_106 = all_0_107_107) % 15.79/4.29 | (308) op2(all_0_97_97, all_0_107_107) = all_0_61_61 % 15.79/4.29 | (309) ~ (all_0_99_99 = all_0_108_108) % 15.79/4.29 | (310) op1(e10, e10) = e13 % 15.79/4.29 | (311) op1(e13, e10) = e12 % 15.79/4.29 | (312) ~ (all_0_103_103 = e22) % 15.79/4.29 | (313) h3(all_0_114_114) = all_0_35_35 % 15.79/4.29 | (314) ~ (all_0_114_114 = all_0_115_115) % 15.79/4.29 | (315) ~ (all_0_112_112 = all_0_118_118) % 15.79/4.29 | (316) all_0_99_99 = e20 | all_0_100_100 = e20 | all_0_101_101 = e20 % 15.79/4.29 | (317) all_0_108_108 = e22 | all_0_108_108 = e21 | all_0_108_108 = e20 % 15.79/4.29 | (318) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op1(v3, v2) = v1) | ~ (op1(v3, v2) = v0)) % 15.79/4.29 | (319) op2(e23, e21) = all_0_101_101 % 15.79/4.29 | (320) ~ (all_0_102_102 = all_0_103_103) % 15.79/4.29 | (321) all_0_122_122 = e12 | all_0_122_122 = e11 | all_0_122_122 = e10 % 15.79/4.29 | (322) ~ (all_0_103_103 = all_0_106_106) % 15.79/4.29 | (323) op2(all_0_103_103, all_0_95_95) = all_0_29_29 % 15.79/4.29 | (324) h2(all_0_113_113) = all_0_59_59 % 15.79/4.30 | (325) all_0_110_110 = e22 | all_0_110_110 = e21 | all_0_110_110 = e20 % 15.79/4.30 | (326) ~ (all_0_107_107 = e20) % 15.79/4.30 | (327) all_0_101_101 = e21 | all_0_110_110 = e21 % 15.79/4.30 | (328) op2(e21, e21) = all_0_107_107 % 15.79/4.30 | (329) ~ (all_0_117_117 = all_0_119_119) % 15.79/4.30 | (330) op1(e12, e12) = all_0_115_115 % 15.79/4.30 | (331) ~ (all_0_108_108 = all_0_110_110) % 15.79/4.30 | (332) op2(all_0_107_107, e21) = all_0_60_60 % 15.79/4.30 | (333) op2(e21, e20) = e20 % 15.79/4.30 | (334) op2(e21, e22) = all_0_106_106 % 15.79/4.30 | (335) ~ (all_0_117_117 = all_0_118_118) % 15.79/4.30 | (336) ~ (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_97_97) | ~ (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_98_98) | ~ (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 = e21) | ~ (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_97_97 = e23) & ~ (all_0_98_98 = e23) & ~ (all_0_107_107 = e23)) | ( ~ (all_0_97_97 = e22) & ~ (all_0_98_98 = e22) & ~ (all_0_107_107 = e22)) | ( ~ (all_0_97_97 = e20) & ~ (all_0_98_98 = e20)) % 15.79/4.30 | (337) h1(e10) = e20 % 15.79/4.30 | (338) op2(e20, e21) = all_0_110_110 % 15.79/4.30 | (339) h4(e13) = all_0_99_99 % 15.79/4.30 | (340) all_0_101_101 = e20 | all_0_104_104 = e20 | all_0_110_110 = e20 % 15.79/4.30 | (341) ~ (all_0_104_104 = all_0_110_110) % 15.79/4.30 | (342) all_0_111_111 = e11 | all_0_112_112 = e11 | all_0_113_113 = e11 % 15.79/4.30 | (343) ~ (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_93_93) | ~ (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_94_94) | ~ (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 = e23) | ~ (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_93_93 = e22) & ~ (all_0_94_94 = e22)) | ( ~ (all_0_93_93 = e21) & ~ (all_0_94_94 = e21) & ~ (all_0_99_99 = e21)) | ( ~ (all_0_93_93 = e20) & ~ (all_0_94_94 = e20) & ~ (all_0_99_99 = e20)) % 15.79/4.30 | (344) ~ (all_0_112_112 = all_0_115_115) % 15.79/4.30 | (345) op2(all_0_97_97, e21) = all_0_98_98 % 15.79/4.30 | (346) h1(e11) = e21 % 15.79/4.30 | (347) ~ (e13 = e11) % 15.79/4.30 | (348) all_0_113_113 = e11 | all_0_122_122 = e11 % 15.79/4.30 | (349) h4(all_0_112_112) = all_0_3_3 % 15.79/4.30 | (350) h1(all_0_116_116) = all_0_86_86 % 15.79/4.30 | % 15.79/4.30 +-Applying beta-rule and splitting (93), into two cases. % 15.79/4.30 |-Branch one: % 15.79/4.30 | (351) all_0_103_103 = e23 % 15.79/4.30 | % 15.79/4.30 | Equations (351) can reduce 100 to: % 15.79/4.30 | (352) ~ (all_0_100_100 = e23) % 15.79/4.30 | % 15.79/4.30 | Equations (351) can reduce 320 to: % 15.79/4.30 | (353) ~ (all_0_102_102 = e23) % 15.79/4.30 | % 15.79/4.30 | Equations (351) can reduce 28 to: % 15.79/4.30 | (110) ~ (e23 = e21) % 15.79/4.30 | % 15.79/4.30 +-Applying beta-rule and splitting (75), into two cases. % 15.79/4.30 |-Branch one: % 15.79/4.30 | (355) all_0_100_100 = e23 % 15.79/4.30 | % 15.79/4.30 | Equations (355) can reduce 352 to: % 15.79/4.30 | (356) $false % 15.79/4.30 | % 15.79/4.30 |-The branch is then unsatisfiable % 15.79/4.30 |-Branch two: % 15.79/4.30 | (352) ~ (all_0_100_100 = e23) % 15.79/4.30 | (358) all_0_101_101 = e23 % 15.79/4.30 | % 15.79/4.30 | Equations (358) can reduce 182 to: % 15.79/4.30 | (359) ~ (all_0_104_104 = e23) % 15.79/4.30 | % 15.79/4.30 | Simplifying 359 yields: % 15.79/4.30 | (360) ~ (all_0_104_104 = e23) % 15.79/4.30 | % 15.79/4.30 | Equations (358) can reduce 48 to: % 15.79/4.30 | (361) ~ (all_0_110_110 = e23) % 15.79/4.30 | % 15.79/4.30 | Simplifying 361 yields: % 15.79/4.30 | (273) ~ (all_0_110_110 = e23) % 15.79/4.30 | % 15.79/4.30 +-Applying beta-rule and splitting (203), into two cases. % 15.79/4.30 |-Branch one: % 15.79/4.30 | (363) all_0_102_102 = e23 % 15.79/4.30 | % 15.79/4.31 | Equations (363) can reduce 353 to: % 15.79/4.31 | (356) $false % 15.79/4.31 | % 15.79/4.31 |-The branch is then unsatisfiable % 15.79/4.31 |-Branch two: % 15.79/4.31 | (353) ~ (all_0_102_102 = e23) % 15.79/4.31 | (366) all_0_105_105 = e23 % 15.79/4.31 | % 15.79/4.31 | Equations (366) can reduce 261 to: % 15.79/4.31 | (367) ~ (all_0_107_107 = e23) % 15.79/4.31 | % 15.79/4.31 | Simplifying 367 yields: % 15.79/4.31 | (368) ~ (all_0_107_107 = e23) % 15.79/4.31 | % 15.79/4.31 | Equations (366) can reduce 163 to: % 15.79/4.31 | (369) ~ (all_0_108_108 = e23) % 15.79/4.31 | % 15.79/4.31 | Simplifying 369 yields: % 15.79/4.31 | (95) ~ (all_0_108_108 = e23) % 15.79/4.31 | % 15.79/4.31 +-Applying beta-rule and splitting (253), into two cases. % 15.79/4.31 |-Branch one: % 15.79/4.31 | (371) all_0_107_107 = e23 % 15.79/4.31 | % 15.79/4.31 | Equations (371) can reduce 368 to: % 15.79/4.31 | (356) $false % 15.79/4.31 | % 15.79/4.31 |-The branch is then unsatisfiable % 15.79/4.31 |-Branch two: % 15.79/4.31 | (368) ~ (all_0_107_107 = e23) % 15.79/4.31 | (374) all_0_107_107 = e22 % 15.79/4.31 | % 15.79/4.31 | Equations (374) can reduce 117 to: % 15.79/4.31 | (375) ~ (all_0_104_104 = e22) % 15.79/4.31 | % 15.79/4.31 | Equations (374) can reduce 307 to: % 15.79/4.31 | (376) ~ (all_0_106_106 = e22) % 15.79/4.31 | % 15.79/4.31 +-Applying beta-rule and splitting (162), into two cases. % 15.79/4.31 |-Branch one: % 15.79/4.31 | (377) all_0_106_106 = e22 % 15.79/4.31 | % 15.79/4.31 | Equations (377) can reduce 376 to: % 15.79/4.31 | (356) $false % 15.79/4.31 | % 15.79/4.31 |-The branch is then unsatisfiable % 15.79/4.31 |-Branch two: % 15.79/4.31 | (376) ~ (all_0_106_106 = e22) % 15.79/4.31 | (380) all_0_109_109 = e22 % 15.79/4.31 | % 15.79/4.31 | Equations (380) can reduce 289 to: % 15.79/4.31 | (381) ~ (all_0_110_110 = e22) % 15.79/4.31 | % 15.79/4.31 | Simplifying 381 yields: % 15.79/4.31 | (382) ~ (all_0_110_110 = e22) % 15.79/4.31 | % 15.79/4.31 +-Applying beta-rule and splitting (240), into two cases. % 15.79/4.31 |-Branch one: % 15.79/4.31 | (383) all_0_102_102 = e22 % 15.79/4.31 | % 15.79/4.31 | Equations (383) can reduce 109 to: % 15.79/4.31 | (384) ~ (all_0_104_104 = e22) % 15.79/4.31 | % 15.79/4.31 | Simplifying 384 yields: % 15.79/4.31 | (375) ~ (all_0_104_104 = e22) % 15.79/4.31 | % 15.79/4.31 | Equations (383) can reduce 34 to: % 15.79/4.31 | (386) ~ (all_0_108_108 = e22) % 15.79/4.31 | % 15.79/4.31 | Simplifying 386 yields: % 15.79/4.31 | (387) ~ (all_0_108_108 = e22) % 15.79/4.31 | % 15.79/4.31 +-Applying beta-rule and splitting (228), into two cases. % 15.79/4.31 |-Branch one: % 15.79/4.31 | (388) all_0_104_104 = e23 % 15.79/4.31 | % 15.79/4.31 | Equations (388) can reduce 360 to: % 15.79/4.31 | (356) $false % 15.79/4.31 | % 15.79/4.31 |-The branch is then unsatisfiable % 15.79/4.31 |-Branch two: % 15.79/4.31 | (360) ~ (all_0_104_104 = e23) % 15.79/4.31 | (391) all_0_104_104 = e22 | all_0_104_104 = e20 % 15.79/4.31 | % 15.79/4.31 +-Applying beta-rule and splitting (391), into two cases. % 15.79/4.31 |-Branch one: % 15.79/4.31 | (392) all_0_104_104 = e22 % 15.79/4.31 | % 15.79/4.31 | Equations (392) can reduce 375 to: % 15.79/4.31 | (356) $false % 15.79/4.31 | % 15.79/4.31 |-The branch is then unsatisfiable % 15.79/4.31 |-Branch two: % 15.79/4.31 | (375) ~ (all_0_104_104 = e22) % 15.79/4.31 | (395) all_0_104_104 = e20 % 15.79/4.31 | % 15.79/4.31 | Equations (395) can reduce 341 to: % 15.79/4.31 | (396) ~ (all_0_110_110 = e20) % 15.79/4.31 | % 15.79/4.31 | Simplifying 396 yields: % 15.79/4.31 | (397) ~ (all_0_110_110 = e20) % 15.79/4.31 | % 15.79/4.31 | Equations (395) can reduce 375 to: % 15.79/4.31 | (398) ~ (e22 = e20) % 15.79/4.31 | % 15.79/4.31 | Simplifying 398 yields: % 15.79/4.31 | (221) ~ (e22 = e20) % 15.79/4.31 | % 15.79/4.31 +-Applying beta-rule and splitting (254), into two cases. % 15.79/4.31 |-Branch one: % 15.79/4.31 | (400) all_0_105_105 = e21 % 15.79/4.31 | % 15.79/4.31 | Combining equations (366,400) yields a new equation: % 15.79/4.31 | (401) e23 = e21 % 15.79/4.31 | % 15.79/4.32 | Simplifying 401 yields: % 15.79/4.32 | (402) e23 = e21 % 15.79/4.32 | % 15.79/4.32 | Equations (402) can reduce 110 to: % 15.79/4.32 | (356) $false % 15.79/4.32 | % 15.79/4.32 |-The branch is then unsatisfiable % 15.79/4.32 |-Branch two: % 15.79/4.32 | (404) ~ (all_0_105_105 = e21) % 15.79/4.32 | (405) all_0_106_106 = e21 % 15.79/4.32 | % 15.79/4.32 +-Applying beta-rule and splitting (325), into two cases. % 15.79/4.32 |-Branch one: % 15.79/4.32 | (406) all_0_110_110 = e22 % 15.79/4.32 | % 15.79/4.32 | Equations (406) can reduce 382 to: % 15.79/4.32 | (356) $false % 15.79/4.32 | % 15.79/4.32 |-The branch is then unsatisfiable % 15.79/4.32 |-Branch two: % 15.79/4.32 | (382) ~ (all_0_110_110 = e22) % 15.79/4.32 | (409) all_0_110_110 = e21 | all_0_110_110 = e20 % 15.79/4.32 | % 15.79/4.32 +-Applying beta-rule and splitting (409), into two cases. % 15.79/4.32 |-Branch one: % 15.79/4.32 | (410) all_0_110_110 = e21 % 15.79/4.32 | % 15.79/4.32 | Equations (410) can reduce 331 to: % 15.79/4.32 | (411) ~ (all_0_108_108 = e21) % 15.79/4.32 | % 15.79/4.32 | Equations (410) can reduce 273 to: % 15.79/4.32 | (412) ~ (e23 = e21) % 15.79/4.32 | % 15.79/4.32 | Simplifying 412 yields: % 15.79/4.32 | (110) ~ (e23 = e21) % 15.79/4.32 | % 15.79/4.32 | Equations (410) can reduce 397 to: % 15.79/4.32 | (139) ~ (e21 = e20) % 15.79/4.32 | % 15.79/4.32 +-Applying beta-rule and splitting (264), into two cases. % 15.79/4.32 |-Branch one: % 15.79/4.32 | (415) all_0_99_99 = e21 % 15.79/4.32 | % 15.79/4.32 +-Applying beta-rule and splitting (115), into two cases. % 15.79/4.32 |-Branch one: % 15.79/4.32 | (416) all_0_99_99 = e20 % 15.79/4.32 | % 15.79/4.32 | Combining equations (415,416) yields a new equation: % 15.79/4.32 | (417) e21 = e20 % 15.79/4.32 | % 15.79/4.32 | Simplifying 417 yields: % 15.79/4.32 | (418) e21 = e20 % 15.79/4.32 | % 15.79/4.32 | Equations (418) can reduce 139 to: % 15.79/4.32 | (356) $false % 15.79/4.32 | % 15.79/4.32 |-The branch is then unsatisfiable % 15.79/4.32 |-Branch two: % 15.79/4.32 | (420) ~ (all_0_99_99 = e20) % 15.79/4.32 | (421) all_0_102_102 = e20 | all_0_108_108 = e20 % 15.79/4.32 | % 15.79/4.32 +-Applying beta-rule and splitting (421), into two cases. % 15.79/4.32 |-Branch one: % 15.79/4.32 | (422) all_0_102_102 = e20 % 15.79/4.32 | % 15.79/4.32 | Combining equations (383,422) yields a new equation: % 15.79/4.32 | (423) e22 = e20 % 15.79/4.32 | % 15.79/4.32 | Simplifying 423 yields: % 15.79/4.32 | (424) e22 = e20 % 15.79/4.32 | % 15.79/4.32 | Equations (424) can reduce 221 to: % 15.79/4.32 | (356) $false % 15.79/4.32 | % 15.79/4.32 |-The branch is then unsatisfiable % 15.79/4.32 |-Branch two: % 15.79/4.32 | (426) ~ (all_0_102_102 = e20) % 15.79/4.32 | (427) all_0_108_108 = e20 % 15.79/4.32 | % 15.79/4.32 | Equations (427) can reduce 95 to: % 15.79/4.32 | (428) ~ (e23 = e20) % 15.79/4.32 | % 15.79/4.32 | Simplifying 428 yields: % 15.79/4.32 | (218) ~ (e23 = e20) % 15.79/4.32 | % 15.79/4.32 | Equations (427) can reduce 387 to: % 15.79/4.32 | (398) ~ (e22 = e20) % 15.79/4.32 | % 15.79/4.32 | Simplifying 398 yields: % 15.79/4.32 | (221) ~ (e22 = e20) % 15.79/4.32 | % 15.79/4.32 +-Applying beta-rule and splitting (255), into two cases. % 15.79/4.32 |-Branch one: % 15.79/4.32 | (432) all_0_100_100 = e20 % 15.79/4.32 | % 15.79/4.32 +-Applying beta-rule and splitting (114), into two cases. % 15.79/4.32 |-Branch one: % 15.79/4.32 | (433) all_0_114_114 = e12 % 15.79/4.32 | % 15.79/4.32 | Equations (433) can reduce 143 to: % 15.79/4.32 | (71) ~ (e12 = e11) % 15.79/4.32 | % 15.79/4.32 | From (433) and (85) follows: % 15.79/4.32 | (435) h1(e12) = all_0_84_84 % 15.79/4.32 | % 15.79/4.32 +-Applying beta-rule and splitting (9), into two cases. % 15.79/4.32 |-Branch one: % 15.79/4.32 | (436) all_0_114_114 = e13 % 15.79/4.32 | % 15.79/4.32 | Combining equations (436,433) yields a new equation: % 15.79/4.32 | (437) e13 = e12 % 15.79/4.32 | % 15.79/4.32 | Simplifying 437 yields: % 15.79/4.32 | (438) e13 = e12 % 15.79/4.32 | % 15.79/4.33 | Equations (438) can reduce 282 to: % 15.79/4.33 | (356) $false % 15.79/4.33 | % 15.79/4.33 |-The branch is then unsatisfiable % 15.79/4.33 |-Branch two: % 15.79/4.33 | (440) ~ (all_0_114_114 = e13) % 15.79/4.33 | (441) all_0_117_117 = e13 % 15.79/4.33 | % 15.79/4.33 | Equations (441) can reduce 335 to: % 15.79/4.33 | (442) ~ (all_0_118_118 = e13) % 15.79/4.33 | % 15.79/4.33 | Simplifying 442 yields: % 15.79/4.33 | (443) ~ (all_0_118_118 = e13) % 15.79/4.33 | % 15.79/4.33 | Equations (441) can reduce 252 to: % 15.79/4.33 | (444) ~ (all_0_120_120 = e13) % 15.79/4.33 | % 15.79/4.33 | Simplifying 444 yields: % 15.79/4.33 | (226) ~ (all_0_120_120 = e13) % 15.79/4.33 | % 15.79/4.33 | From (441) and (266) follows: % 15.79/4.33 | (446) h1(e13) = all_0_87_87 % 15.79/4.33 | % 15.79/4.33 +-Applying beta-rule and splitting (150), into two cases. % 15.79/4.33 |-Branch one: % 15.79/4.33 | (447) all_0_117_117 = e11 % 15.79/4.33 | % 15.79/4.33 | Combining equations (441,447) yields a new equation: % 15.79/4.33 | (448) e13 = e11 % 15.79/4.33 | % 15.79/4.33 | Simplifying 448 yields: % 15.79/4.33 | (449) e13 = e11 % 15.79/4.33 | % 15.79/4.33 | Equations (449) can reduce 347 to: % 15.79/4.33 | (356) $false % 15.79/4.33 | % 15.79/4.33 |-The branch is then unsatisfiable % 15.79/4.33 |-Branch two: % 15.79/4.33 | (451) ~ (all_0_117_117 = e11) % 15.79/4.33 | (452) all_0_118_118 = e11 % 15.79/4.33 | % 15.79/4.33 | Equations (452) can reduce 16 to: % 15.79/4.33 | (453) ~ (all_0_121_121 = e11) % 15.79/4.33 | % 15.79/4.33 | Simplifying 453 yields: % 15.79/4.33 | (454) ~ (all_0_121_121 = e11) % 15.79/4.33 | % 15.79/4.33 | Equations (452) can reduce 443 to: % 15.79/4.33 | (455) ~ (e13 = e11) % 15.79/4.33 | % 15.79/4.33 | Simplifying 455 yields: % 15.79/4.33 | (347) ~ (e13 = e11) % 15.79/4.33 | % 15.79/4.33 | From (452) and (50) follows: % 15.79/4.33 | (457) h1(e11) = all_0_88_88 % 15.79/4.33 | % 15.79/4.33 +-Applying beta-rule and splitting (27), into two cases. % 15.79/4.33 |-Branch one: % 15.79/4.33 | (458) all_0_118_118 = e12 % 15.79/4.33 | % 15.79/4.33 | Combining equations (458,452) yields a new equation: % 15.79/4.33 | (459) e12 = e11 % 15.79/4.33 | % 15.79/4.33 | Simplifying 459 yields: % 15.79/4.33 | (460) e12 = e11 % 15.79/4.33 | % 15.79/4.33 | Equations (460) can reduce 71 to: % 15.79/4.33 | (356) $false % 15.79/4.33 | % 15.79/4.33 |-The branch is then unsatisfiable % 15.79/4.33 |-Branch two: % 15.79/4.33 | (462) ~ (all_0_118_118 = e12) % 15.79/4.33 | (463) all_0_121_121 = e12 % 15.79/4.33 | % 15.79/4.33 | Equations (463) can reduce 191 to: % 15.79/4.33 | (464) ~ (all_0_120_120 = e12) % 15.79/4.33 | % 15.79/4.33 | Equations (463) can reduce 54 to: % 15.79/4.33 | (465) ~ (e13 = e12) % 15.79/4.33 | % 15.79/4.33 | Simplifying 465 yields: % 15.79/4.33 | (282) ~ (e13 = e12) % 15.79/4.33 | % 15.79/4.33 | Equations (463) can reduce 454 to: % 15.79/4.33 | (71) ~ (e12 = e11) % 15.79/4.33 | % 15.79/4.33 | From (463) and (53) follows: % 15.79/4.33 | (468) h1(e12) = all_0_91_91 % 15.79/4.33 | % 15.79/4.33 +-Applying beta-rule and splitting (283), into two cases. % 15.79/4.33 |-Branch one: % 15.79/4.33 | (469) all_0_117_117 = e12 % 15.79/4.33 | % 15.79/4.33 | Combining equations (441,469) yields a new equation: % 15.79/4.33 | (437) e13 = e12 % 15.79/4.33 | % 15.79/4.33 | Simplifying 437 yields: % 15.79/4.33 | (438) e13 = e12 % 15.79/4.33 | % 15.79/4.33 | Equations (438) can reduce 282 to: % 15.79/4.33 | (356) $false % 15.79/4.33 | % 15.79/4.33 |-The branch is then unsatisfiable % 15.79/4.33 |-Branch two: % 15.79/4.33 | (473) ~ (all_0_117_117 = e12) % 15.79/4.33 | (474) all_0_118_118 = e12 | all_0_119_119 = e12 % 15.79/4.33 | % 15.79/4.33 +-Applying beta-rule and splitting (474), into two cases. % 15.79/4.33 |-Branch one: % 15.79/4.33 | (458) all_0_118_118 = e12 % 15.79/4.33 | % 15.79/4.34 | Combining equations (452,458) yields a new equation: % 15.79/4.34 | (460) e12 = e11 % 15.79/4.34 | % 15.79/4.34 | Equations (460) can reduce 71 to: % 15.79/4.34 | (356) $false % 15.79/4.34 | % 15.79/4.34 |-The branch is then unsatisfiable % 15.79/4.34 |-Branch two: % 15.79/4.34 | (462) ~ (all_0_118_118 = e12) % 15.79/4.34 | (479) all_0_119_119 = e12 % 15.79/4.34 | % 15.79/4.34 | Equations (479) can reduce 284 to: % 15.79/4.34 | (57) ~ (all_0_113_113 = e12) % 15.79/4.34 | % 15.79/4.34 | Equations (479) can reduce 52 to: % 15.79/4.34 | (120) ~ (e12 = e10) % 15.79/4.34 | % 15.79/4.34 | From (479) and (49) follows: % 15.79/4.34 | (482) h1(e12) = all_0_89_89 % 15.79/4.34 | % 15.79/4.34 | Instantiating formula (13) with e13, all_0_87_87, e23 and discharging atoms h1(e13) = all_0_87_87, h1(e13) = e23, yields: % 15.79/4.34 | (483) all_0_87_87 = e23 % 15.79/4.34 | % 15.79/4.34 | Instantiating formula (13) with e12, all_0_89_89, e22 and discharging atoms h1(e12) = all_0_89_89, h1(e12) = e22, yields: % 15.79/4.34 | (484) all_0_89_89 = e22 % 15.79/4.34 | % 15.79/4.34 | Instantiating formula (13) with e12, all_0_89_89, all_0_84_84 and discharging atoms h1(e12) = all_0_84_84, h1(e12) = all_0_89_89, yields: % 15.79/4.34 | (485) all_0_84_84 = all_0_89_89 % 15.79/4.34 | % 15.79/4.34 | Instantiating formula (13) with e12, all_0_91_91, all_0_84_84 and discharging atoms h1(e12) = all_0_84_84, h1(e12) = all_0_91_91, yields: % 15.79/4.34 | (486) all_0_84_84 = all_0_91_91 % 15.79/4.34 | % 15.79/4.34 | Instantiating formula (13) with e11, all_0_88_88, e21 and discharging atoms h1(e11) = all_0_88_88, h1(e11) = e21, yields: % 15.79/4.34 | (487) all_0_88_88 = e21 % 15.79/4.34 | % 15.79/4.34 | Combining equations (485,486) yields a new equation: % 15.79/4.34 | (488) all_0_89_89 = all_0_91_91 % 15.79/4.34 | % 15.79/4.34 | Simplifying 488 yields: % 15.79/4.34 | (489) all_0_89_89 = all_0_91_91 % 15.79/4.34 | % 15.79/4.34 | Combining equations (484,489) yields a new equation: % 15.79/4.34 | (490) all_0_91_91 = e22 % 15.79/4.34 | % 15.79/4.34 | Combining equations (490,489) yields a new equation: % 15.79/4.34 | (484) all_0_89_89 = e22 % 15.79/4.34 | % 15.79/4.34 | Combining equations (490,486) yields a new equation: % 15.79/4.34 | (492) all_0_84_84 = e22 % 15.79/4.34 | % 15.79/4.34 | From (483) and (446) follows: % 15.79/4.34 | (236) h1(e13) = e23 % 15.79/4.34 | % 15.79/4.34 | From (487) and (457) follows: % 15.79/4.34 | (346) h1(e11) = e21 % 16.01/4.34 | % 16.01/4.34 +-Applying beta-rule and splitting (105), into two cases. % 16.01/4.34 |-Branch one: % 16.01/4.34 | (495) all_0_112_112 = e13 % 16.01/4.34 | % 16.01/4.34 | Equations (495) can reduce 344 to: % 16.01/4.34 | (496) ~ (all_0_115_115 = e13) % 16.01/4.34 | % 16.01/4.34 | Simplifying 496 yields: % 16.01/4.34 | (497) ~ (all_0_115_115 = e13) % 16.01/4.34 | % 16.01/4.34 +-Applying beta-rule and splitting (180), into two cases. % 16.01/4.34 |-Branch one: % 16.01/4.34 | (498) all_0_115_115 = e10 % 16.01/4.34 | % 16.01/4.34 | Equations (498) can reduce 286 to: % 16.01/4.34 | (499) ~ (all_0_116_116 = e10) % 16.01/4.34 | % 16.01/4.34 | Simplifying 499 yields: % 16.01/4.34 | (500) ~ (all_0_116_116 = e10) % 16.01/4.34 | % 16.01/4.34 | Equations (498) can reduce 497 to: % 16.01/4.34 | (501) ~ (e13 = e10) % 16.01/4.34 | % 16.01/4.34 | Simplifying 501 yields: % 16.01/4.34 | (89) ~ (e13 = e10) % 16.01/4.34 | % 16.01/4.34 +-Applying beta-rule and splitting (198), into two cases. % 16.01/4.34 |-Branch one: % 16.01/4.34 | (503) all_0_116_116 = e10 % 16.01/4.34 | % 16.01/4.35 | Equations (503) can reduce 500 to: % 16.01/4.35 | (356) $false % 16.01/4.35 | % 16.01/4.35 |-The branch is then unsatisfiable % 16.01/4.35 |-Branch two: % 16.01/4.35 | (500) ~ (all_0_116_116 = e10) % 16.01/4.35 | (506) all_0_116_116 = e13 | all_0_116_116 = e12 % 16.01/4.35 | % 16.01/4.35 +-Applying beta-rule and splitting (156), into two cases. % 16.01/4.35 |-Branch one: % 16.01/4.35 | (507) (all_0_112_112 = e10 & ~ (all_0_116_116 = e12) & ~ (all_0_120_120 = e12) & ( ~ (all_0_114_114 = e12) | all_0_115_115 = e13) & ( ~ (all_0_117_117 = e12) | all_0_118_118 = e13) & ( ~ (all_0_119_119 = e12) | all_0_118_118 = e11) & ( ~ (all_0_122_122 = e12) | all_0_121_121 = e11)) | (all_0_116_116 = e10 & ~ (all_0_112_112 = e11) & ~ (all_0_120_120 = e11) & ( ~ (all_0_111_111 = e11) | all_0_113_113 = e13) & ( ~ (all_0_117_117 = e11) | all_0_119_119 = e13) & ( ~ (all_0_118_118 = e11) | all_0_119_119 = e12) & ( ~ (all_0_121_121 = e11) | all_0_122_122 = e12)) | (all_0_120_120 = e10 & ~ (all_0_112_112 = e13) & ~ (all_0_116_116 = e13) & ( ~ (all_0_113_113 = e13) | all_0_111_111 = e11) & ( ~ (all_0_115_115 = e13) | all_0_114_114 = e12) & ( ~ (all_0_118_118 = e13) | all_0_117_117 = e12) & ( ~ (all_0_119_119 = e13) | all_0_117_117 = e11)) % 16.01/4.35 | % 16.01/4.35 +-Applying beta-rule and splitting (507), into two cases. % 16.01/4.35 |-Branch one: % 16.01/4.35 | (508) (all_0_112_112 = e10 & ~ (all_0_116_116 = e12) & ~ (all_0_120_120 = e12) & ( ~ (all_0_114_114 = e12) | all_0_115_115 = e13) & ( ~ (all_0_117_117 = e12) | all_0_118_118 = e13) & ( ~ (all_0_119_119 = e12) | all_0_118_118 = e11) & ( ~ (all_0_122_122 = e12) | all_0_121_121 = e11)) | (all_0_116_116 = e10 & ~ (all_0_112_112 = e11) & ~ (all_0_120_120 = e11) & ( ~ (all_0_111_111 = e11) | all_0_113_113 = e13) & ( ~ (all_0_117_117 = e11) | all_0_119_119 = e13) & ( ~ (all_0_118_118 = e11) | all_0_119_119 = e12) & ( ~ (all_0_121_121 = e11) | all_0_122_122 = e12)) % 16.01/4.35 | % 16.01/4.35 +-Applying beta-rule and splitting (508), into two cases. % 16.01/4.35 |-Branch one: % 16.01/4.35 | (509) all_0_112_112 = e10 & ~ (all_0_116_116 = e12) & ~ (all_0_120_120 = e12) & ( ~ (all_0_114_114 = e12) | all_0_115_115 = e13) & ( ~ (all_0_117_117 = e12) | all_0_118_118 = e13) & ( ~ (all_0_119_119 = e12) | all_0_118_118 = e11) & ( ~ (all_0_122_122 = e12) | all_0_121_121 = e11) % 16.01/4.35 | % 16.01/4.35 | Applying alpha-rule on (509) yields: % 16.01/4.35 | (510) ~ (all_0_116_116 = e12) % 16.01/4.35 | (511) ~ (all_0_119_119 = e12) | all_0_118_118 = e11 % 16.01/4.35 | (512) ~ (all_0_117_117 = e12) | all_0_118_118 = e13 % 16.04/4.35 | (513) ~ (all_0_122_122 = e12) | all_0_121_121 = e11 % 16.04/4.35 | (514) ~ (all_0_114_114 = e12) | all_0_115_115 = e13 % 16.04/4.35 | (515) all_0_112_112 = e10 % 16.04/4.35 | (464) ~ (all_0_120_120 = e12) % 16.04/4.35 | % 16.04/4.35 | Combining equations (495,515) yields a new equation: % 16.04/4.35 | (517) e13 = e10 % 16.04/4.35 | % 16.04/4.35 | Simplifying 517 yields: % 16.04/4.35 | (518) e13 = e10 % 16.04/4.35 | % 16.04/4.35 | Equations (518) can reduce 89 to: % 16.04/4.35 | (356) $false % 16.04/4.35 | % 16.04/4.35 |-The branch is then unsatisfiable % 16.04/4.35 |-Branch two: % 16.04/4.35 | (520) all_0_116_116 = e10 & ~ (all_0_112_112 = e11) & ~ (all_0_120_120 = e11) & ( ~ (all_0_111_111 = e11) | all_0_113_113 = e13) & ( ~ (all_0_117_117 = e11) | all_0_119_119 = e13) & ( ~ (all_0_118_118 = e11) | all_0_119_119 = e12) & ( ~ (all_0_121_121 = e11) | all_0_122_122 = e12) % 16.04/4.35 | % 16.04/4.35 | Applying alpha-rule on (520) yields: % 16.04/4.35 | (521) ~ (all_0_121_121 = e11) | all_0_122_122 = e12 % 16.04/4.35 | (522) ~ (all_0_111_111 = e11) | all_0_113_113 = e13 % 16.04/4.35 | (523) ~ (all_0_117_117 = e11) | all_0_119_119 = e13 % 16.04/4.35 | (503) all_0_116_116 = e10 % 16.04/4.35 | (525) ~ (all_0_112_112 = e11) % 16.04/4.35 | (526) ~ (all_0_118_118 = e11) | all_0_119_119 = e12 % 16.04/4.35 | (527) ~ (all_0_120_120 = e11) % 16.04/4.35 | % 16.04/4.35 | Equations (503) can reduce 500 to: % 16.04/4.35 | (356) $false % 16.04/4.35 | % 16.04/4.35 |-The branch is then unsatisfiable % 16.04/4.35 |-Branch two: % 16.04/4.35 | (529) all_0_120_120 = e10 & ~ (all_0_112_112 = e13) & ~ (all_0_116_116 = e13) & ( ~ (all_0_113_113 = e13) | all_0_111_111 = e11) & ( ~ (all_0_115_115 = e13) | all_0_114_114 = e12) & ( ~ (all_0_118_118 = e13) | all_0_117_117 = e12) & ( ~ (all_0_119_119 = e13) | all_0_117_117 = e11) % 16.04/4.35 | % 16.04/4.35 | Applying alpha-rule on (529) yields: % 16.04/4.35 | (530) ~ (all_0_116_116 = e13) % 16.04/4.35 | (531) ~ (all_0_115_115 = e13) | all_0_114_114 = e12 % 16.04/4.35 | (532) all_0_120_120 = e10 % 16.04/4.35 | (533) ~ (all_0_113_113 = e13) | all_0_111_111 = e11 % 16.04/4.35 | (534) ~ (all_0_119_119 = e13) | all_0_117_117 = e11 % 16.04/4.36 | (535) ~ (all_0_112_112 = e13) % 16.04/4.36 | (536) ~ (all_0_118_118 = e13) | all_0_117_117 = e12 % 16.04/4.36 | % 16.04/4.36 | Equations (495) can reduce 535 to: % 16.04/4.36 | (356) $false % 16.04/4.36 | % 16.04/4.36 |-The branch is then unsatisfiable % 16.04/4.36 |-Branch two: % 16.04/4.36 | (538) ~ (all_0_111_111 = e10) & ~ (all_0_113_113 = e10) & ~ (all_0_114_114 = e10) & ~ (all_0_115_115 = e10) & ~ (all_0_121_121 = e10) & ~ (all_0_122_122 = e10) % 16.04/4.36 | % 16.04/4.36 | Applying alpha-rule on (538) yields: % 16.04/4.36 | (539) ~ (all_0_113_113 = e10) % 16.04/4.36 | (540) ~ (all_0_114_114 = e10) % 16.04/4.36 | (541) ~ (all_0_121_121 = e10) % 16.04/4.36 | (542) ~ (all_0_115_115 = e10) % 16.04/4.36 | (543) ~ (all_0_111_111 = e10) % 16.04/4.36 | (544) ~ (all_0_122_122 = e10) % 16.04/4.36 | % 16.04/4.36 | Equations (498) can reduce 542 to: % 16.04/4.36 | (356) $false % 16.04/4.36 | % 16.04/4.36 |-The branch is then unsatisfiable % 16.04/4.36 |-Branch two: % 16.04/4.36 | (542) ~ (all_0_115_115 = e10) % 16.04/4.36 | (547) all_0_115_115 = e13 % 16.04/4.36 | % 16.04/4.36 | Equations (547) can reduce 497 to: % 16.04/4.36 | (356) $false % 16.04/4.36 | % 16.04/4.36 |-The branch is then unsatisfiable % 16.04/4.36 |-Branch two: % 16.04/4.36 | (535) ~ (all_0_112_112 = e13) % 16.04/4.36 | (550) all_0_113_113 = e13 % 16.04/4.36 | % 16.04/4.36 | Equations (550) can reduce 225 to: % 16.04/4.36 | (551) ~ (all_0_116_116 = e13) % 16.04/4.36 | % 16.04/4.36 | Simplifying 551 yields: % 16.04/4.36 | (530) ~ (all_0_116_116 = e13) % 16.04/4.36 | % 16.04/4.36 | Equations (550) can reduce 57 to: % 16.04/4.36 | (282) ~ (e13 = e12) % 16.04/4.36 | % 16.04/4.36 | From (550) and (241) follows: % 16.04/4.36 | (554) h1(e13) = all_0_83_83 % 16.04/4.36 | % 16.04/4.36 +-Applying beta-rule and splitting (348), into two cases. % 16.04/4.36 |-Branch one: % 16.04/4.36 | (555) all_0_113_113 = e11 % 16.04/4.36 | % 16.04/4.36 | Combining equations (555,550) yields a new equation: % 16.04/4.36 | (449) e13 = e11 % 16.04/4.36 | % 16.04/4.36 | Equations (449) can reduce 347 to: % 16.04/4.36 | (356) $false % 16.04/4.36 | % 16.04/4.36 |-The branch is then unsatisfiable % 16.04/4.36 |-Branch two: % 16.04/4.36 | (558) ~ (all_0_113_113 = e11) % 16.04/4.36 | (559) all_0_122_122 = e11 % 16.04/4.36 | % 16.04/4.36 | Equations (559) can reduce 17 to: % 16.04/4.36 | (527) ~ (all_0_120_120 = e11) % 16.04/4.36 | % 16.04/4.36 | From (559) and (281) follows: % 16.04/4.36 | (561) h1(e11) = all_0_92_92 % 16.04/4.36 | % 16.04/4.36 +-Applying beta-rule and splitting (155), into two cases. % 16.04/4.36 |-Branch one: % 16.04/4.36 | (515) all_0_112_112 = e10 % 16.04/4.36 | % 16.04/4.36 | Equations (515) can reduce 144 to: % 16.04/4.36 | (543) ~ (all_0_111_111 = e10) % 16.04/4.36 | % 16.04/4.36 | Equations (515) can reduce 344 to: % 16.04/4.36 | (564) ~ (all_0_115_115 = e10) % 16.04/4.36 | % 16.04/4.36 | Simplifying 564 yields: % 16.04/4.36 | (542) ~ (all_0_115_115 = e10) % 16.04/4.36 | % 16.04/4.36 | From (515) and (229) follows: % 16.04/4.36 | (566) h1(e10) = all_0_82_82 % 16.04/4.36 | % 16.04/4.36 +-Applying beta-rule and splitting (180), into two cases. % 16.04/4.36 |-Branch one: % 16.04/4.36 | (498) all_0_115_115 = e10 % 16.04/4.36 | % 16.04/4.36 | Equations (498) can reduce 542 to: % 16.04/4.36 | (356) $false % 16.04/4.36 | % 16.04/4.36 |-The branch is then unsatisfiable % 16.04/4.36 |-Branch two: % 16.04/4.37 | (542) ~ (all_0_115_115 = e10) % 16.04/4.37 | (547) all_0_115_115 = e13 % 16.04/4.37 | % 16.04/4.37 | From (547) and (269) follows: % 16.04/4.37 | (571) h1(e13) = all_0_85_85 % 16.04/4.37 | % 16.04/4.37 +-Applying beta-rule and splitting (234), into two cases. % 16.04/4.37 |-Branch one: % 16.04/4.37 | (572) all_0_111_111 = e10 % 16.04/4.37 | % 16.04/4.37 | Equations (572) can reduce 543 to: % 16.04/4.37 | (356) $false % 16.04/4.37 | % 16.04/4.37 |-The branch is then unsatisfiable % 16.04/4.37 |-Branch two: % 16.04/4.37 | (543) ~ (all_0_111_111 = e10) % 16.04/4.37 | (575) all_0_111_111 = e11 % 16.04/4.37 | % 16.04/4.37 | Equations (575) can reduce 188 to: % 16.04/4.37 | (576) ~ (all_0_120_120 = e11) % 16.04/4.37 | % 16.04/4.37 | Simplifying 576 yields: % 16.04/4.37 | (527) ~ (all_0_120_120 = e11) % 16.04/4.37 | % 16.04/4.37 | From (575) and (113) follows: % 16.04/4.37 | (578) h1(e11) = all_0_81_81 % 16.04/4.37 | % 16.04/4.37 +-Applying beta-rule and splitting (207), into two cases. % 16.04/4.37 |-Branch one: % 16.04/4.37 | (532) all_0_120_120 = e10 % 16.04/4.37 | % 16.04/4.37 | Equations (532) can reduce 226 to: % 16.04/4.37 | (501) ~ (e13 = e10) % 16.04/4.37 | % 16.04/4.37 | Simplifying 501 yields: % 16.04/4.37 | (89) ~ (e13 = e10) % 16.04/4.37 | % 16.04/4.37 | Equations (532) can reduce 464 to: % 16.04/4.37 | (582) ~ (e12 = e10) % 16.04/4.37 | % 16.04/4.37 | Simplifying 582 yields: % 16.04/4.37 | (120) ~ (e12 = e10) % 16.04/4.37 | % 16.04/4.37 | From (532) and (68) follows: % 16.04/4.37 | (584) h1(e10) = all_0_90_90 % 16.04/4.37 | % 16.04/4.37 +-Applying beta-rule and splitting (51), into two cases. % 16.04/4.37 |-Branch one: % 16.04/4.37 | (585) all_0_113_113 = e10 % 16.04/4.37 | % 16.04/4.37 | Combining equations (550,585) yields a new equation: % 16.04/4.37 | (517) e13 = e10 % 16.04/4.37 | % 16.04/4.37 | Simplifying 517 yields: % 16.04/4.37 | (518) e13 = e10 % 16.04/4.37 | % 16.04/4.37 | Equations (518) can reduce 89 to: % 16.04/4.37 | (356) $false % 16.04/4.37 | % 16.04/4.37 |-The branch is then unsatisfiable % 16.04/4.37 |-Branch two: % 16.04/4.37 | (539) ~ (all_0_113_113 = e10) % 16.04/4.37 | (590) all_0_116_116 = e10 | all_0_122_122 = e10 % 16.04/4.37 | % 16.04/4.37 | Equations (550) can reduce 539 to: % 16.04/4.37 | (89) ~ (e13 = e10) % 16.04/4.37 | % 16.04/4.37 +-Applying beta-rule and splitting (80), into two cases. % 16.04/4.37 |-Branch one: % 16.04/4.37 | (592) all_0_114_114 = e10 % 16.04/4.37 | % 16.04/4.37 | Combining equations (433,592) yields a new equation: % 16.04/4.37 | (593) e12 = e10 % 16.04/4.37 | % 16.04/4.37 | Simplifying 593 yields: % 16.04/4.37 | (594) e12 = e10 % 16.04/4.37 | % 16.04/4.37 | Equations (594) can reduce 120 to: % 16.04/4.37 | (356) $false % 16.04/4.37 | % 16.04/4.37 |-The branch is then unsatisfiable % 16.04/4.37 |-Branch two: % 16.04/4.37 | (540) ~ (all_0_114_114 = e10) % 16.04/4.37 | (597) all_0_115_115 = e10 | all_0_116_116 = e10 % 16.04/4.37 | % 16.04/4.37 +-Applying beta-rule and splitting (198), into two cases. % 16.04/4.37 |-Branch one: % 16.04/4.37 | (503) all_0_116_116 = e10 % 16.04/4.37 | % 16.04/4.37 | From (503) and (350) follows: % 16.04/4.37 | (599) h1(e10) = all_0_86_86 % 16.04/4.37 | % 16.04/4.37 | Instantiating formula (13) with e13, all_0_83_83, e23 and discharging atoms h1(e13) = all_0_83_83, h1(e13) = e23, yields: % 16.04/4.37 | (600) all_0_83_83 = e23 % 16.04/4.37 | % 16.04/4.37 | Instantiating formula (13) with e13, all_0_85_85, all_0_83_83 and discharging atoms h1(e13) = all_0_83_83, h1(e13) = all_0_85_85, yields: % 16.04/4.37 | (601) all_0_83_83 = all_0_85_85 % 16.04/4.37 | % 16.04/4.37 | Instantiating formula (13) with e11, all_0_81_81, e21 and discharging atoms h1(e11) = all_0_81_81, h1(e11) = e21, yields: % 16.04/4.37 | (602) all_0_81_81 = e21 % 16.04/4.37 | % 16.04/4.37 | Instantiating formula (13) with e11, all_0_92_92, all_0_81_81 and discharging atoms h1(e11) = all_0_81_81, h1(e11) = all_0_92_92, yields: % 16.04/4.37 | (603) all_0_81_81 = all_0_92_92 % 16.04/4.37 | % 16.04/4.37 | Instantiating formula (13) with e10, all_0_82_82, e20 and discharging atoms h1(e10) = all_0_82_82, h1(e10) = e20, yields: % 16.04/4.37 | (604) all_0_82_82 = e20 % 16.04/4.38 | % 16.04/4.38 | Instantiating formula (13) with e10, all_0_86_86, all_0_82_82 and discharging atoms h1(e10) = all_0_82_82, h1(e10) = all_0_86_86, yields: % 16.04/4.38 | (605) all_0_82_82 = all_0_86_86 % 16.04/4.38 | % 16.04/4.38 | Instantiating formula (13) with e10, all_0_90_90, all_0_82_82 and discharging atoms h1(e10) = all_0_82_82, h1(e10) = all_0_90_90, yields: % 16.04/4.38 | (606) all_0_82_82 = all_0_90_90 % 16.04/4.38 | % 16.04/4.38 | Combining equations (602,603) yields a new equation: % 16.04/4.38 | (607) all_0_92_92 = e21 % 16.04/4.38 | % 16.04/4.38 | Combining equations (606,605) yields a new equation: % 16.04/4.38 | (608) all_0_86_86 = all_0_90_90 % 16.04/4.38 | % 16.04/4.38 | Combining equations (604,605) yields a new equation: % 16.04/4.38 | (609) all_0_86_86 = e20 % 16.04/4.38 | % 16.04/4.38 | Combining equations (600,601) yields a new equation: % 16.04/4.38 | (610) all_0_85_85 = e23 % 16.04/4.38 | % 16.04/4.38 | Combining equations (608,609) yields a new equation: % 16.04/4.38 | (611) all_0_90_90 = e20 % 16.04/4.38 | % 16.04/4.38 | Simplifying 611 yields: % 16.04/4.38 | (612) all_0_90_90 = e20 % 16.04/4.38 | % 16.04/4.38 | Combining equations (610,601) yields a new equation: % 16.04/4.38 | (600) all_0_83_83 = e23 % 16.04/4.38 | % 16.04/4.38 | Combining equations (609,605) yields a new equation: % 16.04/4.38 | (604) all_0_82_82 = e20 % 16.04/4.38 | % 16.04/4.38 | Combining equations (607,603) yields a new equation: % 16.04/4.38 | (602) all_0_81_81 = e21 % 16.04/4.38 | % 16.04/4.38 +-Applying beta-rule and splitting (299), into two cases. % 16.04/4.38 |-Branch one: % 16.04/4.38 | (616) ~ (all_0_81_81 = all_0_99_99) % 16.04/4.38 | % 16.04/4.38 | Equations (602,415) can reduce 616 to: % 16.04/4.38 | (356) $false % 16.04/4.38 | % 16.04/4.38 |-The branch is then unsatisfiable % 16.04/4.38 |-Branch two: % 16.04/4.38 | (618) all_0_81_81 = all_0_99_99 % 16.04/4.38 | (619) ~ (all_0_82_82 = all_0_100_100) | ~ (all_0_83_83 = all_0_101_101) | ~ (all_0_84_84 = all_0_102_102) | ~ (all_0_85_85 = all_0_103_103) | ~ (all_0_86_86 = all_0_104_104) | ~ (all_0_87_87 = all_0_105_105) | ~ (all_0_88_88 = all_0_106_106) | ~ (all_0_89_89 = all_0_107_107) | ~ (all_0_90_90 = all_0_108_108) | ~ (all_0_91_91 = all_0_109_109) | ~ (all_0_92_92 = all_0_110_110) % 16.04/4.38 | % 16.04/4.38 +-Applying beta-rule and splitting (619), into two cases. % 16.04/4.38 |-Branch one: % 16.04/4.38 | (620) ~ (all_0_82_82 = all_0_100_100) % 16.04/4.38 | % 16.04/4.38 | Equations (604,432) can reduce 620 to: % 16.04/4.38 | (356) $false % 16.04/4.38 | % 16.04/4.38 |-The branch is then unsatisfiable % 16.04/4.38 |-Branch two: % 16.04/4.38 | (622) all_0_82_82 = all_0_100_100 % 16.04/4.38 | (623) ~ (all_0_83_83 = all_0_101_101) | ~ (all_0_84_84 = all_0_102_102) | ~ (all_0_85_85 = all_0_103_103) | ~ (all_0_86_86 = all_0_104_104) | ~ (all_0_87_87 = all_0_105_105) | ~ (all_0_88_88 = all_0_106_106) | ~ (all_0_89_89 = all_0_107_107) | ~ (all_0_90_90 = all_0_108_108) | ~ (all_0_91_91 = all_0_109_109) | ~ (all_0_92_92 = all_0_110_110) % 16.04/4.38 | % 16.04/4.38 +-Applying beta-rule and splitting (623), into two cases. % 16.04/4.38 |-Branch one: % 16.04/4.38 | (624) ~ (all_0_83_83 = all_0_101_101) % 16.04/4.38 | % 16.04/4.38 | Equations (600,358) can reduce 624 to: % 16.04/4.38 | (356) $false % 16.04/4.38 | % 16.04/4.38 |-The branch is then unsatisfiable % 16.04/4.38 |-Branch two: % 16.04/4.38 | (626) all_0_83_83 = all_0_101_101 % 16.04/4.38 | (627) ~ (all_0_84_84 = all_0_102_102) | ~ (all_0_85_85 = all_0_103_103) | ~ (all_0_86_86 = all_0_104_104) | ~ (all_0_87_87 = all_0_105_105) | ~ (all_0_88_88 = all_0_106_106) | ~ (all_0_89_89 = all_0_107_107) | ~ (all_0_90_90 = all_0_108_108) | ~ (all_0_91_91 = all_0_109_109) | ~ (all_0_92_92 = all_0_110_110) % 16.04/4.38 | % 16.04/4.38 +-Applying beta-rule and splitting (627), into two cases. % 16.04/4.38 |-Branch one: % 16.04/4.38 | (628) ~ (all_0_84_84 = all_0_102_102) % 16.04/4.38 | % 16.04/4.38 | Equations (492,383) can reduce 628 to: % 16.04/4.38 | (356) $false % 16.04/4.38 | % 16.04/4.38 |-The branch is then unsatisfiable % 16.04/4.38 |-Branch two: % 16.04/4.38 | (630) all_0_84_84 = all_0_102_102 % 16.04/4.38 | (631) ~ (all_0_85_85 = all_0_103_103) | ~ (all_0_86_86 = all_0_104_104) | ~ (all_0_87_87 = all_0_105_105) | ~ (all_0_88_88 = all_0_106_106) | ~ (all_0_89_89 = all_0_107_107) | ~ (all_0_90_90 = all_0_108_108) | ~ (all_0_91_91 = all_0_109_109) | ~ (all_0_92_92 = all_0_110_110) % 16.04/4.38 | % 16.04/4.38 +-Applying beta-rule and splitting (631), into two cases. % 16.04/4.38 |-Branch one: % 16.04/4.38 | (632) ~ (all_0_85_85 = all_0_103_103) % 16.04/4.38 | % 16.04/4.38 | Equations (610,351) can reduce 632 to: % 16.04/4.38 | (356) $false % 16.04/4.38 | % 16.04/4.38 |-The branch is then unsatisfiable % 16.04/4.38 |-Branch two: % 16.04/4.38 | (634) all_0_85_85 = all_0_103_103 % 16.04/4.38 | (635) ~ (all_0_86_86 = all_0_104_104) | ~ (all_0_87_87 = all_0_105_105) | ~ (all_0_88_88 = all_0_106_106) | ~ (all_0_89_89 = all_0_107_107) | ~ (all_0_90_90 = all_0_108_108) | ~ (all_0_91_91 = all_0_109_109) | ~ (all_0_92_92 = all_0_110_110) % 16.04/4.38 | % 16.04/4.38 +-Applying beta-rule and splitting (635), into two cases. % 16.04/4.38 |-Branch one: % 16.04/4.38 | (636) ~ (all_0_86_86 = all_0_104_104) % 16.04/4.38 | % 16.04/4.38 | Equations (609,395) can reduce 636 to: % 16.04/4.38 | (356) $false % 16.04/4.38 | % 16.04/4.38 |-The branch is then unsatisfiable % 16.04/4.38 |-Branch two: % 16.04/4.39 | (638) all_0_86_86 = all_0_104_104 % 16.04/4.39 | (639) ~ (all_0_87_87 = all_0_105_105) | ~ (all_0_88_88 = all_0_106_106) | ~ (all_0_89_89 = all_0_107_107) | ~ (all_0_90_90 = all_0_108_108) | ~ (all_0_91_91 = all_0_109_109) | ~ (all_0_92_92 = all_0_110_110) % 16.04/4.39 | % 16.04/4.39 +-Applying beta-rule and splitting (639), into two cases. % 16.04/4.39 |-Branch one: % 16.04/4.39 | (640) ~ (all_0_87_87 = all_0_105_105) % 16.04/4.39 | % 16.04/4.39 | Equations (483,366) can reduce 640 to: % 16.04/4.39 | (356) $false % 16.04/4.39 | % 16.04/4.39 |-The branch is then unsatisfiable % 16.04/4.39 |-Branch two: % 16.04/4.39 | (642) all_0_87_87 = all_0_105_105 % 16.04/4.39 | (643) ~ (all_0_88_88 = all_0_106_106) | ~ (all_0_89_89 = all_0_107_107) | ~ (all_0_90_90 = all_0_108_108) | ~ (all_0_91_91 = all_0_109_109) | ~ (all_0_92_92 = all_0_110_110) % 16.04/4.39 | % 16.04/4.39 +-Applying beta-rule and splitting (643), into two cases. % 16.04/4.39 |-Branch one: % 16.04/4.39 | (644) ~ (all_0_88_88 = all_0_106_106) % 16.04/4.39 | % 16.04/4.39 | Equations (487,405) can reduce 644 to: % 16.04/4.39 | (356) $false % 16.04/4.39 | % 16.04/4.39 |-The branch is then unsatisfiable % 16.04/4.39 |-Branch two: % 16.04/4.39 | (646) all_0_88_88 = all_0_106_106 % 16.04/4.39 | (647) ~ (all_0_89_89 = all_0_107_107) | ~ (all_0_90_90 = all_0_108_108) | ~ (all_0_91_91 = all_0_109_109) | ~ (all_0_92_92 = all_0_110_110) % 16.04/4.39 | % 16.04/4.39 +-Applying beta-rule and splitting (647), into two cases. % 16.04/4.39 |-Branch one: % 16.04/4.39 | (648) ~ (all_0_89_89 = all_0_107_107) % 16.04/4.39 | % 16.04/4.39 | Equations (484,374) can reduce 648 to: % 16.04/4.39 | (356) $false % 16.04/4.39 | % 16.04/4.39 |-The branch is then unsatisfiable % 16.04/4.39 |-Branch two: % 16.04/4.39 | (650) all_0_89_89 = all_0_107_107 % 16.04/4.39 | (651) ~ (all_0_90_90 = all_0_108_108) | ~ (all_0_91_91 = all_0_109_109) | ~ (all_0_92_92 = all_0_110_110) % 16.04/4.39 | % 16.04/4.39 +-Applying beta-rule and splitting (651), into two cases. % 16.04/4.39 |-Branch one: % 16.04/4.39 | (652) ~ (all_0_90_90 = all_0_108_108) % 16.04/4.39 | % 16.04/4.39 | Equations (612,427) can reduce 652 to: % 16.04/4.39 | (356) $false % 16.04/4.39 | % 16.04/4.39 |-The branch is then unsatisfiable % 16.04/4.39 |-Branch two: % 16.04/4.39 | (654) all_0_90_90 = all_0_108_108 % 16.04/4.39 | (655) ~ (all_0_91_91 = all_0_109_109) | ~ (all_0_92_92 = all_0_110_110) % 16.04/4.39 | % 16.04/4.39 +-Applying beta-rule and splitting (655), into two cases. % 16.04/4.39 |-Branch one: % 16.04/4.39 | (656) ~ (all_0_91_91 = all_0_109_109) % 16.04/4.39 | % 16.04/4.39 | Equations (490,380) can reduce 656 to: % 16.04/4.39 | (356) $false % 16.04/4.39 | % 16.04/4.39 |-The branch is then unsatisfiable % 16.04/4.39 |-Branch two: % 16.04/4.39 | (658) all_0_91_91 = all_0_109_109 % 16.04/4.39 | (659) ~ (all_0_92_92 = all_0_110_110) % 16.04/4.39 | % 16.04/4.39 | Equations (607,410) can reduce 659 to: % 16.04/4.39 | (356) $false % 16.04/4.39 | % 16.04/4.39 |-The branch is then unsatisfiable % 16.04/4.39 |-Branch two: % 16.04/4.39 | (500) ~ (all_0_116_116 = e10) % 16.04/4.39 | (506) all_0_116_116 = e13 | all_0_116_116 = e12 % 16.04/4.39 | % 16.04/4.39 +-Applying beta-rule and splitting (597), into two cases. % 16.04/4.39 |-Branch one: % 16.04/4.39 | (498) all_0_115_115 = e10 % 16.04/4.39 | % 16.04/4.39 | Combining equations (547,498) yields a new equation: % 16.04/4.39 | (517) e13 = e10 % 16.04/4.39 | % 16.04/4.39 | Simplifying 517 yields: % 16.04/4.39 | (518) e13 = e10 % 16.04/4.39 | % 16.04/4.39 | Equations (518) can reduce 89 to: % 16.04/4.39 | (356) $false % 16.04/4.39 | % 16.04/4.39 |-The branch is then unsatisfiable % 16.04/4.39 |-Branch two: % 16.04/4.39 | (542) ~ (all_0_115_115 = e10) % 16.04/4.39 | (503) all_0_116_116 = e10 % 16.04/4.39 | % 16.04/4.39 | Equations (503) can reduce 500 to: % 16.04/4.39 | (356) $false % 16.04/4.39 | % 16.04/4.39 |-The branch is then unsatisfiable % 16.04/4.39 |-Branch two: % 16.04/4.39 | (670) ~ (all_0_120_120 = e10) % 16.04/4.39 | (671) all_0_120_120 = e12 | all_0_120_120 = e11 % 16.04/4.39 | % 16.04/4.39 +-Applying beta-rule and splitting (671), into two cases. % 16.04/4.39 |-Branch one: % 16.04/4.39 | (672) all_0_120_120 = e12 % 16.04/4.39 | % 16.04/4.39 | Equations (672) can reduce 464 to: % 16.04/4.39 | (356) $false % 16.04/4.39 | % 16.04/4.39 |-The branch is then unsatisfiable % 16.04/4.39 |-Branch two: % 16.04/4.39 | (464) ~ (all_0_120_120 = e12) % 16.04/4.39 | (675) all_0_120_120 = e11 % 16.04/4.39 | % 16.04/4.39 | Equations (675) can reduce 527 to: % 16.04/4.39 | (356) $false % 16.04/4.39 | % 16.04/4.39 |-The branch is then unsatisfiable % 16.04/4.39 |-Branch two: % 16.04/4.39 | (677) ~ (all_0_112_112 = e10) % 16.04/4.39 | (678) all_0_112_112 = e13 | all_0_112_112 = e11 % 16.04/4.39 | % 16.04/4.39 +-Applying beta-rule and splitting (124), into two cases. % 16.04/4.39 |-Branch one: % 16.04/4.39 | (515) all_0_112_112 = e10 % 16.04/4.39 | % 16.04/4.39 | Equations (515) can reduce 677 to: % 16.04/4.39 | (356) $false % 16.04/4.39 | % 16.04/4.39 |-The branch is then unsatisfiable % 16.04/4.39 |-Branch two: % 16.04/4.39 | (677) ~ (all_0_112_112 = e10) % 16.04/4.39 | (682) all_0_115_115 = e10 | all_0_121_121 = e10 % 16.04/4.39 | % 16.04/4.39 +-Applying beta-rule and splitting (682), into two cases. % 16.04/4.39 |-Branch one: % 16.04/4.39 | (498) all_0_115_115 = e10 % 16.04/4.39 | % 16.04/4.39 +-Applying beta-rule and splitting (207), into two cases. % 16.04/4.39 |-Branch one: % 16.04/4.39 | (532) all_0_120_120 = e10 % 16.04/4.39 | % 16.04/4.39 | Equations (532) can reduce 226 to: % 16.04/4.39 | (501) ~ (e13 = e10) % 16.04/4.39 | % 16.04/4.39 | Simplifying 501 yields: % 16.04/4.39 | (89) ~ (e13 = e10) % 16.04/4.39 | % 16.04/4.39 +-Applying beta-rule and splitting (90), into two cases. % 16.04/4.39 |-Branch one: % 16.04/4.39 | (436) all_0_114_114 = e13 % 16.04/4.39 | % 16.04/4.39 | Combining equations (436,433) yields a new equation: % 16.04/4.39 | (437) e13 = e12 % 16.04/4.39 | % 16.04/4.39 | Simplifying 437 yields: % 16.04/4.39 | (438) e13 = e12 % 16.04/4.39 | % 16.04/4.39 | Equations (438) can reduce 282 to: % 16.04/4.39 | (356) $false % 16.04/4.39 | % 16.04/4.39 |-The branch is then unsatisfiable % 16.04/4.39 |-Branch two: % 16.04/4.39 | (440) ~ (all_0_114_114 = e13) % 16.04/4.39 | (692) all_0_115_115 = e13 | all_0_116_116 = e13 % 16.04/4.39 | % 16.04/4.39 +-Applying beta-rule and splitting (51), into two cases. % 16.04/4.39 |-Branch one: % 16.04/4.39 | (585) all_0_113_113 = e10 % 16.04/4.39 | % 16.04/4.39 | Combining equations (585,550) yields a new equation: % 16.04/4.39 | (518) e13 = e10 % 16.04/4.39 | % 16.04/4.39 | Equations (518) can reduce 89 to: % 16.04/4.39 | (356) $false % 16.04/4.39 | % 16.04/4.39 |-The branch is then unsatisfiable % 16.04/4.39 |-Branch two: % 16.04/4.39 | (539) ~ (all_0_113_113 = e10) % 16.04/4.39 | (590) all_0_116_116 = e10 | all_0_122_122 = e10 % 16.04/4.39 | % 16.04/4.39 | Equations (550) can reduce 539 to: % 16.04/4.39 | (89) ~ (e13 = e10) % 16.04/4.39 | % 16.04/4.39 +-Applying beta-rule and splitting (692), into two cases. % 16.04/4.39 |-Branch one: % 16.04/4.39 | (547) all_0_115_115 = e13 % 16.04/4.40 | % 16.04/4.40 | Combining equations (547,498) yields a new equation: % 16.04/4.40 | (517) e13 = e10 % 16.04/4.40 | % 16.04/4.40 | Simplifying 517 yields: % 16.04/4.40 | (518) e13 = e10 % 16.04/4.40 | % 16.04/4.40 | Equations (518) can reduce 89 to: % 16.04/4.40 | (356) $false % 16.04/4.40 | % 16.04/4.40 |-The branch is then unsatisfiable % 16.04/4.40 |-Branch two: % 16.04/4.40 | (497) ~ (all_0_115_115 = e13) % 16.04/4.40 | (704) all_0_116_116 = e13 % 16.04/4.40 | % 16.04/4.40 | Equations (704) can reduce 530 to: % 16.04/4.40 | (356) $false % 16.04/4.40 | % 16.04/4.40 |-The branch is then unsatisfiable % 16.04/4.40 |-Branch two: % 16.04/4.40 | (670) ~ (all_0_120_120 = e10) % 16.04/4.40 | (671) all_0_120_120 = e12 | all_0_120_120 = e11 % 16.04/4.40 | % 16.04/4.40 +-Applying beta-rule and splitting (671), into two cases. % 16.04/4.40 |-Branch one: % 16.04/4.40 | (672) all_0_120_120 = e12 % 16.04/4.40 | % 16.04/4.40 | Equations (672) can reduce 464 to: % 16.04/4.40 | (356) $false % 16.04/4.40 | % 16.04/4.40 |-The branch is then unsatisfiable % 16.04/4.40 |-Branch two: % 16.04/4.40 | (464) ~ (all_0_120_120 = e12) % 16.04/4.40 | (675) all_0_120_120 = e11 % 16.04/4.40 | % 16.04/4.40 | Equations (675) can reduce 527 to: % 16.04/4.40 | (356) $false % 16.04/4.40 | % 16.04/4.40 |-The branch is then unsatisfiable % 16.04/4.40 |-Branch two: % 16.04/4.40 | (542) ~ (all_0_115_115 = e10) % 16.04/4.40 | (714) all_0_121_121 = e10 % 16.04/4.40 | % 16.04/4.40 | Combining equations (463,714) yields a new equation: % 16.04/4.40 | (593) e12 = e10 % 16.04/4.40 | % 16.04/4.40 | Simplifying 593 yields: % 16.04/4.40 | (594) e12 = e10 % 16.04/4.40 | % 16.04/4.40 | Equations (594) can reduce 120 to: % 16.04/4.40 | (356) $false % 16.04/4.40 | % 16.04/4.40 |-The branch is then unsatisfiable % 16.04/4.40 |-Branch two: % 16.04/4.40 | (718) ~ (all_0_114_114 = e12) % 16.04/4.40 | (719) all_0_116_116 = e12 % 16.04/4.40 | % 16.04/4.40 | Equations (719) can reduce 286 to: % 16.04/4.40 | (208) ~ (all_0_115_115 = e12) % 16.04/4.40 | % 16.04/4.40 | Equations (719) can reduce 279 to: % 16.04/4.40 | (721) ~ (all_0_119_119 = e12) % 16.04/4.40 | % 16.04/4.40 | Simplifying 721 yields: % 16.04/4.40 | (722) ~ (all_0_119_119 = e12) % 16.04/4.40 | % 16.04/4.40 +-Applying beta-rule and splitting (14), into two cases. % 16.04/4.40 |-Branch one: % 16.04/4.40 | (723) all_0_119_119 = e13 % 16.04/4.40 | % 16.04/4.40 | Equations (723) can reduce 284 to: % 16.04/4.40 | (724) ~ (all_0_113_113 = e13) % 16.04/4.40 | % 16.04/4.40 | Equations (723) can reduce 329 to: % 16.04/4.40 | (725) ~ (all_0_117_117 = e13) % 16.04/4.40 | % 16.04/4.40 +-Applying beta-rule and splitting (9), into two cases. % 16.04/4.40 |-Branch one: % 16.04/4.40 | (436) all_0_114_114 = e13 % 16.04/4.40 | % 16.04/4.40 | Equations (436) can reduce 314 to: % 16.04/4.40 | (496) ~ (all_0_115_115 = e13) % 16.04/4.40 | % 16.04/4.40 | Simplifying 496 yields: % 16.04/4.40 | (497) ~ (all_0_115_115 = e13) % 16.04/4.40 | % 16.04/4.40 +-Applying beta-rule and splitting (180), into two cases. % 16.04/4.40 |-Branch one: % 16.04/4.40 | (498) all_0_115_115 = e10 % 16.04/4.40 | % 16.04/4.40 | Equations (498) can reduce 344 to: % 16.04/4.40 | (677) ~ (all_0_112_112 = e10) % 16.04/4.40 | % 16.04/4.40 | Equations (498) can reduce 208 to: % 16.04/4.40 | (582) ~ (e12 = e10) % 16.04/4.40 | % 16.04/4.40 | Simplifying 582 yields: % 16.04/4.40 | (120) ~ (e12 = e10) % 16.04/4.40 | % 16.04/4.40 +-Applying beta-rule and splitting (105), into two cases. % 16.04/4.40 |-Branch one: % 16.04/4.40 | (495) all_0_112_112 = e13 % 16.04/4.40 | % 16.04/4.40 | Equations (495) can reduce 677 to: % 16.04/4.40 | (89) ~ (e13 = e10) % 16.04/4.40 | % 16.04/4.40 +-Applying beta-rule and splitting (156), into two cases. % 16.04/4.40 |-Branch one: % 16.04/4.40 | (507) (all_0_112_112 = e10 & ~ (all_0_116_116 = e12) & ~ (all_0_120_120 = e12) & ( ~ (all_0_114_114 = e12) | all_0_115_115 = e13) & ( ~ (all_0_117_117 = e12) | all_0_118_118 = e13) & ( ~ (all_0_119_119 = e12) | all_0_118_118 = e11) & ( ~ (all_0_122_122 = e12) | all_0_121_121 = e11)) | (all_0_116_116 = e10 & ~ (all_0_112_112 = e11) & ~ (all_0_120_120 = e11) & ( ~ (all_0_111_111 = e11) | all_0_113_113 = e13) & ( ~ (all_0_117_117 = e11) | all_0_119_119 = e13) & ( ~ (all_0_118_118 = e11) | all_0_119_119 = e12) & ( ~ (all_0_121_121 = e11) | all_0_122_122 = e12)) | (all_0_120_120 = e10 & ~ (all_0_112_112 = e13) & ~ (all_0_116_116 = e13) & ( ~ (all_0_113_113 = e13) | all_0_111_111 = e11) & ( ~ (all_0_115_115 = e13) | all_0_114_114 = e12) & ( ~ (all_0_118_118 = e13) | all_0_117_117 = e12) & ( ~ (all_0_119_119 = e13) | all_0_117_117 = e11)) % 16.04/4.40 | % 16.04/4.40 +-Applying beta-rule and splitting (507), into two cases. % 16.04/4.40 |-Branch one: % 16.04/4.40 | (508) (all_0_112_112 = e10 & ~ (all_0_116_116 = e12) & ~ (all_0_120_120 = e12) & ( ~ (all_0_114_114 = e12) | all_0_115_115 = e13) & ( ~ (all_0_117_117 = e12) | all_0_118_118 = e13) & ( ~ (all_0_119_119 = e12) | all_0_118_118 = e11) & ( ~ (all_0_122_122 = e12) | all_0_121_121 = e11)) | (all_0_116_116 = e10 & ~ (all_0_112_112 = e11) & ~ (all_0_120_120 = e11) & ( ~ (all_0_111_111 = e11) | all_0_113_113 = e13) & ( ~ (all_0_117_117 = e11) | all_0_119_119 = e13) & ( ~ (all_0_118_118 = e11) | all_0_119_119 = e12) & ( ~ (all_0_121_121 = e11) | all_0_122_122 = e12)) % 16.04/4.40 | % 16.04/4.40 +-Applying beta-rule and splitting (508), into two cases. % 16.04/4.40 |-Branch one: % 16.04/4.40 | (509) all_0_112_112 = e10 & ~ (all_0_116_116 = e12) & ~ (all_0_120_120 = e12) & ( ~ (all_0_114_114 = e12) | all_0_115_115 = e13) & ( ~ (all_0_117_117 = e12) | all_0_118_118 = e13) & ( ~ (all_0_119_119 = e12) | all_0_118_118 = e11) & ( ~ (all_0_122_122 = e12) | all_0_121_121 = e11) % 16.04/4.40 | % 16.04/4.40 | Applying alpha-rule on (509) yields: % 16.04/4.40 | (510) ~ (all_0_116_116 = e12) % 16.04/4.40 | (511) ~ (all_0_119_119 = e12) | all_0_118_118 = e11 % 16.04/4.40 | (512) ~ (all_0_117_117 = e12) | all_0_118_118 = e13 % 16.04/4.40 | (513) ~ (all_0_122_122 = e12) | all_0_121_121 = e11 % 16.04/4.40 | (514) ~ (all_0_114_114 = e12) | all_0_115_115 = e13 % 16.04/4.40 | (515) all_0_112_112 = e10 % 16.04/4.40 | (464) ~ (all_0_120_120 = e12) % 16.04/4.40 | % 16.04/4.40 | Combining equations (495,515) yields a new equation: % 16.04/4.40 | (517) e13 = e10 % 16.04/4.40 | % 16.04/4.40 | Simplifying 517 yields: % 16.04/4.40 | (518) e13 = e10 % 16.04/4.40 | % 16.04/4.40 | Equations (518) can reduce 89 to: % 16.04/4.40 | (356) $false % 16.04/4.40 | % 16.26/4.40 |-The branch is then unsatisfiable % 16.26/4.40 |-Branch two: % 16.26/4.40 | (520) all_0_116_116 = e10 & ~ (all_0_112_112 = e11) & ~ (all_0_120_120 = e11) & ( ~ (all_0_111_111 = e11) | all_0_113_113 = e13) & ( ~ (all_0_117_117 = e11) | all_0_119_119 = e13) & ( ~ (all_0_118_118 = e11) | all_0_119_119 = e12) & ( ~ (all_0_121_121 = e11) | all_0_122_122 = e12) % 16.26/4.40 | % 16.26/4.40 | Applying alpha-rule on (520) yields: % 16.26/4.40 | (521) ~ (all_0_121_121 = e11) | all_0_122_122 = e12 % 16.26/4.40 | (522) ~ (all_0_111_111 = e11) | all_0_113_113 = e13 % 16.26/4.40 | (523) ~ (all_0_117_117 = e11) | all_0_119_119 = e13 % 16.26/4.40 | (503) all_0_116_116 = e10 % 16.26/4.40 | (525) ~ (all_0_112_112 = e11) % 16.26/4.40 | (526) ~ (all_0_118_118 = e11) | all_0_119_119 = e12 % 16.26/4.40 | (527) ~ (all_0_120_120 = e11) % 16.26/4.41 | % 16.26/4.41 | Combining equations (719,503) yields a new equation: % 16.26/4.41 | (593) e12 = e10 % 16.26/4.41 | % 16.26/4.41 | Simplifying 593 yields: % 16.26/4.41 | (594) e12 = e10 % 16.26/4.41 | % 16.26/4.41 | Equations (594) can reduce 120 to: % 16.26/4.41 | (356) $false % 16.26/4.41 | % 16.26/4.41 |-The branch is then unsatisfiable % 16.26/4.41 |-Branch two: % 16.26/4.41 | (529) all_0_120_120 = e10 & ~ (all_0_112_112 = e13) & ~ (all_0_116_116 = e13) & ( ~ (all_0_113_113 = e13) | all_0_111_111 = e11) & ( ~ (all_0_115_115 = e13) | all_0_114_114 = e12) & ( ~ (all_0_118_118 = e13) | all_0_117_117 = e12) & ( ~ (all_0_119_119 = e13) | all_0_117_117 = e11) % 16.26/4.41 | % 16.26/4.41 | Applying alpha-rule on (529) yields: % 16.26/4.41 | (530) ~ (all_0_116_116 = e13) % 16.26/4.41 | (531) ~ (all_0_115_115 = e13) | all_0_114_114 = e12 % 16.26/4.41 | (532) all_0_120_120 = e10 % 16.26/4.41 | (533) ~ (all_0_113_113 = e13) | all_0_111_111 = e11 % 16.26/4.41 | (534) ~ (all_0_119_119 = e13) | all_0_117_117 = e11 % 16.26/4.41 | (535) ~ (all_0_112_112 = e13) % 16.26/4.41 | (536) ~ (all_0_118_118 = e13) | all_0_117_117 = e12 % 16.26/4.41 | % 16.26/4.41 | Equations (495) can reduce 535 to: % 16.26/4.41 | (356) $false % 16.26/4.41 | % 16.26/4.41 |-The branch is then unsatisfiable % 16.26/4.41 |-Branch two: % 16.26/4.41 | (538) ~ (all_0_111_111 = e10) & ~ (all_0_113_113 = e10) & ~ (all_0_114_114 = e10) & ~ (all_0_115_115 = e10) & ~ (all_0_121_121 = e10) & ~ (all_0_122_122 = e10) % 16.26/4.41 | % 16.26/4.41 | Applying alpha-rule on (538) yields: % 16.26/4.41 | (539) ~ (all_0_113_113 = e10) % 16.26/4.41 | (540) ~ (all_0_114_114 = e10) % 16.26/4.41 | (541) ~ (all_0_121_121 = e10) % 16.26/4.41 | (542) ~ (all_0_115_115 = e10) % 16.26/4.41 | (543) ~ (all_0_111_111 = e10) % 16.26/4.41 | (544) ~ (all_0_122_122 = e10) % 16.26/4.41 | % 16.26/4.41 | Equations (498) can reduce 542 to: % 16.26/4.41 | (356) $false % 16.26/4.41 | % 16.26/4.41 |-The branch is then unsatisfiable % 16.26/4.41 |-Branch two: % 16.26/4.41 | (535) ~ (all_0_112_112 = e13) % 16.26/4.41 | (550) all_0_113_113 = e13 % 16.26/4.41 | % 16.26/4.41 | Equations (550) can reduce 724 to: % 16.26/4.41 | (356) $false % 16.26/4.41 | % 16.26/4.41 |-The branch is then unsatisfiable % 16.26/4.41 |-Branch two: % 16.26/4.41 | (542) ~ (all_0_115_115 = e10) % 16.26/4.41 | (547) all_0_115_115 = e13 % 16.26/4.41 | % 16.26/4.41 | Equations (547) can reduce 497 to: % 16.26/4.41 | (356) $false % 16.26/4.41 | % 16.26/4.41 |-The branch is then unsatisfiable % 16.26/4.41 |-Branch two: % 16.26/4.41 | (440) ~ (all_0_114_114 = e13) % 16.26/4.41 | (441) all_0_117_117 = e13 % 16.26/4.41 | % 16.26/4.41 | Equations (441) can reduce 725 to: % 16.26/4.41 | (356) $false % 16.26/4.41 | % 16.26/4.41 |-The branch is then unsatisfiable % 16.26/4.41 |-Branch two: % 16.26/4.41 | (785) ~ (all_0_119_119 = e13) % 16.26/4.41 | (479) all_0_119_119 = e12 % 16.26/4.41 | % 16.26/4.41 | Equations (479) can reduce 722 to: % 16.26/4.41 | (356) $false % 16.26/4.41 | % 16.26/4.41 |-The branch is then unsatisfiable % 16.26/4.41 |-Branch two: % 16.26/4.41 | (788) ~ (all_0_100_100 = e20) % 16.26/4.41 | (789) all_0_103_103 = e20 | all_0_109_109 = e20 % 16.26/4.41 | % 16.26/4.41 +-Applying beta-rule and splitting (789), into two cases. % 16.26/4.41 |-Branch one: % 16.26/4.41 | (790) all_0_103_103 = e20 % 16.26/4.41 | % 16.26/4.41 | Combining equations (351,790) yields a new equation: % 16.26/4.41 | (791) e23 = e20 % 16.26/4.41 | % 16.26/4.41 | Simplifying 791 yields: % 16.26/4.41 | (792) e23 = e20 % 16.26/4.41 | % 16.26/4.41 | Equations (792) can reduce 218 to: % 16.26/4.41 | (356) $false % 16.26/4.41 | % 16.26/4.41 |-The branch is then unsatisfiable % 16.26/4.41 |-Branch two: % 16.26/4.41 | (794) ~ (all_0_103_103 = e20) % 16.26/4.41 | (795) all_0_109_109 = e20 % 16.26/4.41 | % 16.26/4.41 | Combining equations (380,795) yields a new equation: % 16.26/4.41 | (423) e22 = e20 % 16.26/4.41 | % 16.26/4.41 | Simplifying 423 yields: % 16.26/4.41 | (424) e22 = e20 % 16.26/4.41 | % 16.26/4.41 | Equations (424) can reduce 221 to: % 16.26/4.41 | (356) $false % 16.26/4.41 | % 16.26/4.41 |-The branch is then unsatisfiable % 16.26/4.41 |-Branch two: % 16.26/4.41 | (799) ~ (all_0_99_99 = e21) % 16.26/4.41 | (800) all_0_105_105 = e21 | all_0_108_108 = e21 % 16.26/4.41 | % 16.26/4.41 +-Applying beta-rule and splitting (800), into two cases. % 16.26/4.41 |-Branch one: % 16.26/4.41 | (400) all_0_105_105 = e21 % 16.26/4.41 | % 16.26/4.41 | Combining equations (366,400) yields a new equation: % 16.26/4.41 | (401) e23 = e21 % 16.26/4.41 | % 16.26/4.41 | Simplifying 401 yields: % 16.26/4.41 | (402) e23 = e21 % 16.26/4.41 | % 16.26/4.41 | Equations (402) can reduce 110 to: % 16.26/4.41 | (356) $false % 16.26/4.41 | % 16.26/4.41 |-The branch is then unsatisfiable % 16.26/4.41 |-Branch two: % 16.26/4.41 | (404) ~ (all_0_105_105 = e21) % 16.26/4.41 | (806) all_0_108_108 = e21 % 16.26/4.41 | % 16.26/4.41 | Equations (806) can reduce 411 to: % 16.26/4.41 | (356) $false % 16.26/4.41 | % 16.26/4.41 |-The branch is then unsatisfiable % 16.26/4.41 |-Branch two: % 16.26/4.41 | (808) ~ (all_0_110_110 = e21) % 16.26/4.41 | (809) all_0_110_110 = e20 % 16.26/4.41 | % 16.26/4.41 | Equations (809) can reduce 397 to: % 16.26/4.41 | (356) $false % 16.26/4.41 | % 16.26/4.41 |-The branch is then unsatisfiable % 16.26/4.41 |-Branch two: % 16.26/4.41 | (811) ~ (all_0_102_102 = e22) % 16.26/4.41 | (392) all_0_104_104 = e22 % 16.26/4.41 | % 16.26/4.41 | Equations (392) can reduce 375 to: % 16.26/4.41 | (356) $false % 16.26/4.41 | % 16.26/4.41 |-The branch is then unsatisfiable % 16.26/4.41 |-Branch two: % 16.26/4.41 | (814) ~ (all_0_103_103 = e23) % 16.26/4.41 | (790) all_0_103_103 = e20 % 16.26/4.41 | % 16.26/4.41 | Equations (790) can reduce 100 to: % 16.26/4.41 | (788) ~ (all_0_100_100 = e20) % 16.26/4.41 | % 16.26/4.41 | Equations (790) can reduce 167 to: % 16.26/4.41 | (817) ~ (all_0_104_104 = e20) % 16.26/4.41 | % 16.26/4.41 | Simplifying 817 yields: % 16.26/4.41 | (818) ~ (all_0_104_104 = e20) % 16.26/4.41 | % 16.26/4.41 +-Applying beta-rule and splitting (159), into two cases. % 16.26/4.41 |-Branch one: % 16.26/4.41 | (819) (all_0_100_100 = e20 & ~ (all_0_104_104 = e22) & ~ (all_0_108_108 = e22) & ( ~ (all_0_102_102 = e22) | all_0_103_103 = e23) & ( ~ (all_0_105_105 = e22) | all_0_106_106 = e23) & ( ~ (all_0_107_107 = e22) | all_0_106_106 = e21) & ( ~ (all_0_110_110 = e22) | all_0_109_109 = e21)) | (all_0_104_104 = e20 & ~ (all_0_100_100 = e21) & ~ (all_0_108_108 = e21) & ( ~ (all_0_99_99 = e21) | all_0_101_101 = e23) & ( ~ (all_0_105_105 = e21) | all_0_107_107 = e23) & ( ~ (all_0_106_106 = e21) | all_0_107_107 = e22) & ( ~ (all_0_109_109 = e21) | all_0_110_110 = e22)) | (all_0_108_108 = e20 & ~ (all_0_100_100 = e23) & ~ (all_0_104_104 = e23) & ( ~ (all_0_101_101 = e23) | all_0_99_99 = e21) & ( ~ (all_0_103_103 = e23) | all_0_102_102 = e22) & ( ~ (all_0_106_106 = e23) | all_0_105_105 = e22) & ( ~ (all_0_107_107 = e23) | all_0_105_105 = e21)) % 16.26/4.42 | % 16.26/4.42 +-Applying beta-rule and splitting (819), into two cases. % 16.26/4.42 |-Branch one: % 16.26/4.42 | (820) (all_0_100_100 = e20 & ~ (all_0_104_104 = e22) & ~ (all_0_108_108 = e22) & ( ~ (all_0_102_102 = e22) | all_0_103_103 = e23) & ( ~ (all_0_105_105 = e22) | all_0_106_106 = e23) & ( ~ (all_0_107_107 = e22) | all_0_106_106 = e21) & ( ~ (all_0_110_110 = e22) | all_0_109_109 = e21)) | (all_0_104_104 = e20 & ~ (all_0_100_100 = e21) & ~ (all_0_108_108 = e21) & ( ~ (all_0_99_99 = e21) | all_0_101_101 = e23) & ( ~ (all_0_105_105 = e21) | all_0_107_107 = e23) & ( ~ (all_0_106_106 = e21) | all_0_107_107 = e22) & ( ~ (all_0_109_109 = e21) | all_0_110_110 = e22)) % 16.26/4.42 | % 16.26/4.42 +-Applying beta-rule and splitting (820), into two cases. % 16.26/4.42 |-Branch one: % 16.26/4.42 | (821) all_0_100_100 = e20 & ~ (all_0_104_104 = e22) & ~ (all_0_108_108 = e22) & ( ~ (all_0_102_102 = e22) | all_0_103_103 = e23) & ( ~ (all_0_105_105 = e22) | all_0_106_106 = e23) & ( ~ (all_0_107_107 = e22) | all_0_106_106 = e21) & ( ~ (all_0_110_110 = e22) | all_0_109_109 = e21) % 16.26/4.42 | % 16.26/4.42 | Applying alpha-rule on (821) yields: % 16.26/4.42 | (822) ~ (all_0_110_110 = e22) | all_0_109_109 = e21 % 16.26/4.42 | (823) ~ (all_0_105_105 = e22) | all_0_106_106 = e23 % 16.26/4.42 | (824) ~ (all_0_107_107 = e22) | all_0_106_106 = e21 % 16.26/4.42 | (375) ~ (all_0_104_104 = e22) % 16.26/4.42 | (387) ~ (all_0_108_108 = e22) % 16.26/4.42 | (827) ~ (all_0_102_102 = e22) | all_0_103_103 = e23 % 16.26/4.42 | (432) all_0_100_100 = e20 % 16.26/4.42 | % 16.26/4.42 | Equations (432) can reduce 788 to: % 16.26/4.42 | (356) $false % 16.26/4.42 | % 16.26/4.42 |-The branch is then unsatisfiable % 16.26/4.42 |-Branch two: % 16.26/4.42 | (830) all_0_104_104 = e20 & ~ (all_0_100_100 = e21) & ~ (all_0_108_108 = e21) & ( ~ (all_0_99_99 = e21) | all_0_101_101 = e23) & ( ~ (all_0_105_105 = e21) | all_0_107_107 = e23) & ( ~ (all_0_106_106 = e21) | all_0_107_107 = e22) & ( ~ (all_0_109_109 = e21) | all_0_110_110 = e22) % 16.26/4.42 | % 16.26/4.42 | Applying alpha-rule on (830) yields: % 16.26/4.42 | (831) ~ (all_0_99_99 = e21) | all_0_101_101 = e23 % 16.26/4.42 | (832) ~ (all_0_105_105 = e21) | all_0_107_107 = e23 % 16.26/4.42 | (411) ~ (all_0_108_108 = e21) % 16.26/4.42 | (834) ~ (all_0_100_100 = e21) % 16.26/4.42 | (835) ~ (all_0_109_109 = e21) | all_0_110_110 = e22 % 16.26/4.42 | (836) ~ (all_0_106_106 = e21) | all_0_107_107 = e22 % 16.26/4.42 | (395) all_0_104_104 = e20 % 16.26/4.42 | % 16.26/4.42 | Equations (395) can reduce 818 to: % 16.26/4.42 | (356) $false % 16.26/4.42 | % 16.26/4.42 |-The branch is then unsatisfiable % 16.26/4.42 |-Branch two: % 16.26/4.42 | (839) all_0_108_108 = e20 & ~ (all_0_100_100 = e23) & ~ (all_0_104_104 = e23) & ( ~ (all_0_101_101 = e23) | all_0_99_99 = e21) & ( ~ (all_0_103_103 = e23) | all_0_102_102 = e22) & ( ~ (all_0_106_106 = e23) | all_0_105_105 = e22) & ( ~ (all_0_107_107 = e23) | all_0_105_105 = e21) % 16.26/4.42 | % 16.26/4.42 | Applying alpha-rule on (839) yields: % 16.26/4.42 | (840) ~ (all_0_107_107 = e23) | all_0_105_105 = e21 % 16.26/4.42 | (360) ~ (all_0_104_104 = e23) % 16.26/4.42 | (427) all_0_108_108 = e20 % 16.26/4.42 | (843) ~ (all_0_101_101 = e23) | all_0_99_99 = e21 % 16.26/4.42 | (844) ~ (all_0_103_103 = e23) | all_0_102_102 = e22 % 16.26/4.42 | (352) ~ (all_0_100_100 = e23) % 16.26/4.42 | (846) ~ (all_0_106_106 = e23) | all_0_105_105 = e22 % 16.26/4.42 | % 16.26/4.42 | Equations (427) can reduce 309 to: % 16.26/4.42 | (420) ~ (all_0_99_99 = e20) % 16.26/4.42 | % 16.26/4.42 | Equations (427) can reduce 163 to: % 16.26/4.42 | (176) ~ (all_0_105_105 = e20) % 16.26/4.42 | % 16.26/4.42 +-Applying beta-rule and splitting (235), into two cases. % 16.26/4.42 |-Branch one: % 16.26/4.42 | (363) all_0_102_102 = e23 % 16.26/4.42 | % 16.26/4.42 | Equations (363) can reduce 177 to: % 16.26/4.42 | (850) ~ (all_0_105_105 = e23) % 16.26/4.42 | % 16.26/4.42 | Simplifying 850 yields: % 16.26/4.42 | (851) ~ (all_0_105_105 = e23) % 16.26/4.42 | % 16.26/4.42 +-Applying beta-rule and splitting (75), into two cases. % 16.26/4.42 |-Branch one: % 16.26/4.42 | (355) all_0_100_100 = e23 % 16.26/4.42 | % 16.26/4.42 | Equations (355) can reduce 352 to: % 16.26/4.42 | (356) $false % 16.26/4.42 | % 16.26/4.42 |-The branch is then unsatisfiable % 16.26/4.42 |-Branch two: % 16.26/4.42 | (352) ~ (all_0_100_100 = e23) % 16.26/4.42 | (358) all_0_101_101 = e23 % 16.26/4.42 | % 16.26/4.42 | Equations (358) can reduce 244 to: % 16.26/4.42 | (129) ~ (all_0_99_99 = e23) % 16.26/4.42 | % 16.26/4.42 | Equations (358) can reduce 42 to: % 16.26/4.42 | (367) ~ (all_0_107_107 = e23) % 16.26/4.42 | % 16.26/4.42 | Simplifying 367 yields: % 16.26/4.42 | (368) ~ (all_0_107_107 = e23) % 16.26/4.42 | % 16.26/4.42 | Equations (358) can reduce 48 to: % 16.26/4.42 | (361) ~ (all_0_110_110 = e23) % 16.26/4.42 | % 16.26/4.42 | Simplifying 361 yields: % 16.26/4.42 | (273) ~ (all_0_110_110 = e23) % 16.26/4.42 | % 16.26/4.42 +-Applying beta-rule and splitting (253), into two cases. % 16.26/4.42 |-Branch one: % 16.26/4.42 | (371) all_0_107_107 = e23 % 16.26/4.42 | % 16.26/4.42 | Equations (371) can reduce 368 to: % 16.26/4.42 | (356) $false % 16.26/4.42 | % 16.26/4.42 |-The branch is then unsatisfiable % 16.26/4.42 |-Branch two: % 16.26/4.42 | (368) ~ (all_0_107_107 = e23) % 16.26/4.42 | (374) all_0_107_107 = e22 % 16.26/4.42 | % 16.26/4.42 | Equations (374) can reduce 307 to: % 16.26/4.42 | (376) ~ (all_0_106_106 = e22) % 16.26/4.42 | % 16.26/4.42 +-Applying beta-rule and splitting (162), into two cases. % 16.26/4.42 |-Branch one: % 16.26/4.42 | (377) all_0_106_106 = e22 % 16.26/4.42 | % 16.26/4.42 | Equations (377) can reduce 376 to: % 16.26/4.42 | (356) $false % 16.26/4.42 | % 16.26/4.42 |-The branch is then unsatisfiable % 16.26/4.42 |-Branch two: % 16.26/4.42 | (376) ~ (all_0_106_106 = e22) % 16.26/4.42 | (380) all_0_109_109 = e22 % 16.26/4.42 | % 16.26/4.42 | Equations (380) can reduce 18 to: % 16.26/4.42 | (870) ~ (e23 = e22) % 16.26/4.42 | % 16.26/4.42 | Simplifying 870 yields: % 16.26/4.42 | (168) ~ (e23 = e22) % 16.26/4.42 | % 16.26/4.42 +-Applying beta-rule and splitting (35), into two cases. % 16.26/4.42 |-Branch one: % 16.26/4.42 | (415) all_0_99_99 = e21 % 16.26/4.42 | % 16.26/4.42 | Equations (415) can reduce 223 to: % 16.26/4.42 | (873) ~ (all_0_105_105 = e21) % 16.26/4.42 | % 16.26/4.42 | Simplifying 873 yields: % 16.26/4.42 | (404) ~ (all_0_105_105 = e21) % 16.26/4.42 | % 16.26/4.42 | Equations (415) can reduce 129 to: % 16.26/4.42 | (412) ~ (e23 = e21) % 16.26/4.42 | % 16.26/4.42 | Simplifying 412 yields: % 16.26/4.42 | (110) ~ (e23 = e21) % 16.26/4.42 | % 16.26/4.42 +-Applying beta-rule and splitting (327), into two cases. % 16.26/4.42 |-Branch one: % 16.26/4.42 | (877) all_0_101_101 = e21 % 16.26/4.42 | % 16.26/4.42 | Combining equations (358,877) yields a new equation: % 16.26/4.42 | (401) e23 = e21 % 16.26/4.42 | % 16.26/4.42 | Simplifying 401 yields: % 16.26/4.42 | (402) e23 = e21 % 16.26/4.42 | % 16.26/4.42 | Equations (402) can reduce 110 to: % 16.26/4.42 | (356) $false % 16.26/4.42 | % 16.26/4.42 |-The branch is then unsatisfiable % 16.26/4.42 |-Branch two: % 16.26/4.42 | (881) ~ (all_0_101_101 = e21) % 16.26/4.42 | (410) all_0_110_110 = e21 % 16.26/4.42 | % 16.26/4.42 | Equations (410) can reduce 273 to: % 16.26/4.42 | (412) ~ (e23 = e21) % 16.26/4.42 | % 16.26/4.42 | Simplifying 412 yields: % 16.26/4.42 | (110) ~ (e23 = e21) % 16.26/4.42 | % 16.26/4.42 +-Applying beta-rule and splitting (254), into two cases. % 16.26/4.42 |-Branch one: % 16.26/4.42 | (400) all_0_105_105 = e21 % 16.26/4.42 | % 16.26/4.42 | Equations (400) can reduce 404 to: % 16.26/4.42 | (356) $false % 16.26/4.42 | % 16.26/4.42 |-The branch is then unsatisfiable % 16.26/4.42 |-Branch two: % 16.26/4.42 | (404) ~ (all_0_105_105 = e21) % 16.26/4.42 | (405) all_0_106_106 = e21 % 16.26/4.42 | % 16.26/4.42 +-Applying beta-rule and splitting (186), into two cases. % 16.26/4.42 |-Branch one: % 16.26/4.42 | (366) all_0_105_105 = e23 % 16.26/4.42 | % 16.26/4.42 | Equations (366) can reduce 851 to: % 16.26/4.42 | (356) $false % 16.26/4.42 | % 16.26/4.42 |-The branch is then unsatisfiable % 16.26/4.42 |-Branch two: % 16.26/4.42 | (851) ~ (all_0_105_105 = e23) % 16.26/4.42 | (892) all_0_106_106 = e23 | all_0_107_107 = e23 % 16.26/4.42 | % 16.26/4.42 +-Applying beta-rule and splitting (892), into two cases. % 16.26/4.42 |-Branch one: % 16.26/4.43 | (893) all_0_106_106 = e23 % 16.26/4.43 | % 16.26/4.43 | Combining equations (405,893) yields a new equation: % 16.26/4.43 | (402) e23 = e21 % 16.26/4.43 | % 16.26/4.43 | Equations (402) can reduce 110 to: % 16.26/4.43 | (356) $false % 16.26/4.43 | % 16.26/4.43 |-The branch is then unsatisfiable % 16.26/4.43 |-Branch two: % 16.26/4.43 | (896) ~ (all_0_106_106 = e23) % 16.26/4.43 | (371) all_0_107_107 = e23 % 16.26/4.43 | % 16.26/4.43 | Combining equations (374,371) yields a new equation: % 16.26/4.43 | (898) e23 = e22 % 16.26/4.43 | % 16.26/4.43 | Equations (898) can reduce 168 to: % 16.26/4.43 | (356) $false % 16.26/4.43 | % 16.26/4.43 |-The branch is then unsatisfiable % 16.26/4.43 |-Branch two: % 16.26/4.43 | (799) ~ (all_0_99_99 = e21) % 16.26/4.43 | (416) all_0_99_99 = e20 % 16.26/4.43 | % 16.26/4.43 | Equations (416) can reduce 420 to: % 16.26/4.43 | (356) $false % 16.26/4.43 | % 16.26/4.43 |-The branch is then unsatisfiable % 16.26/4.43 |-Branch two: % 16.26/4.43 | (353) ~ (all_0_102_102 = e23) % 16.26/4.43 | (904) all_0_103_103 = e23 | all_0_104_104 = e23 % 16.26/4.43 | % 16.26/4.43 +-Applying beta-rule and splitting (203), into two cases. % 16.26/4.43 |-Branch one: % 16.26/4.43 | (363) all_0_102_102 = e23 % 16.26/4.43 | % 16.26/4.43 | Equations (363) can reduce 353 to: % 16.26/4.43 | (356) $false % 16.26/4.43 | % 16.26/4.43 |-The branch is then unsatisfiable % 16.26/4.43 |-Branch two: % 16.26/4.43 | (353) ~ (all_0_102_102 = e23) % 16.26/4.43 | (366) all_0_105_105 = e23 % 16.26/4.43 | % 16.26/4.43 | Equations (366) can reduce 176 to: % 16.26/4.43 | (218) ~ (e23 = e20) % 16.26/4.43 | % 16.26/4.43 +-Applying beta-rule and splitting (75), into two cases. % 16.26/4.43 |-Branch one: % 16.26/4.43 | (355) all_0_100_100 = e23 % 16.26/4.43 | % 16.26/4.43 | Equations (355) can reduce 352 to: % 16.26/4.43 | (356) $false % 16.26/4.43 | % 16.26/4.43 |-The branch is then unsatisfiable % 16.26/4.43 |-Branch two: % 16.26/4.43 | (352) ~ (all_0_100_100 = e23) % 16.26/4.43 | (358) all_0_101_101 = e23 % 16.26/4.43 | % 16.26/4.43 | Equations (358) can reduce 182 to: % 16.26/4.43 | (359) ~ (all_0_104_104 = e23) % 16.26/4.43 | % 16.26/4.43 | Simplifying 359 yields: % 16.26/4.43 | (360) ~ (all_0_104_104 = e23) % 16.26/4.43 | % 16.26/4.43 +-Applying beta-rule and splitting (904), into two cases. % 16.26/4.43 |-Branch one: % 16.26/4.43 | (351) all_0_103_103 = e23 % 16.26/4.43 | % 16.26/4.43 | Combining equations (790,351) yields a new equation: % 16.26/4.43 | (792) e23 = e20 % 16.26/4.43 | % 16.26/4.43 | Equations (792) can reduce 218 to: % 16.26/4.43 | (356) $false % 16.26/4.43 | % 16.26/4.43 |-The branch is then unsatisfiable % 16.26/4.43 |-Branch two: % 16.26/4.43 | (814) ~ (all_0_103_103 = e23) % 16.26/4.43 | (388) all_0_104_104 = e23 % 16.26/4.43 | % 16.26/4.43 | Equations (388) can reduce 360 to: % 16.26/4.43 | (356) $false % 16.26/4.43 | % 16.26/4.43 |-The branch is then unsatisfiable % 16.26/4.43 |-Branch two: % 16.26/4.43 | (922) ~ (all_0_99_99 = e20) & ~ (all_0_101_101 = e20) & ~ (all_0_102_102 = e20) & ~ (all_0_103_103 = e20) & ~ (all_0_109_109 = e20) & ~ (all_0_110_110 = e20) % 16.26/4.43 | % 16.26/4.43 | Applying alpha-rule on (922) yields: % 16.26/4.43 | (794) ~ (all_0_103_103 = e20) % 16.26/4.43 | (924) ~ (all_0_109_109 = e20) % 16.26/4.43 | (420) ~ (all_0_99_99 = e20) % 16.26/4.43 | (926) ~ (all_0_101_101 = e20) % 16.26/4.43 | (397) ~ (all_0_110_110 = e20) % 16.26/4.43 | (426) ~ (all_0_102_102 = e20) % 16.26/4.43 | % 16.26/4.43 | Equations (790) can reduce 794 to: % 16.26/4.43 | (356) $false % 16.26/4.43 | % 16.26/4.43 |-The branch is then unsatisfiable % 16.26/4.43 % SZS output end Proof for theBenchmark % 16.26/4.43 % 16.26/4.43 3767ms %------------------------------------------------------------------------------