%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : ALG110+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n025.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Thu Jul 14 15:35:11 EDT 2022 % Result : Theorem 5.96s 1.82s % Output : Proof 9.26s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : ALG110+1 : TPTP v8.1.0. Released v2.7.0. % 0.00/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.11/0.33 % Computer : n025.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 600 % 0.11/0.33 % DateTime : Wed Jun 8 12:31:34 EDT 2022 % 0.11/0.33 % CPUTime : % 0.56/0.58 ____ _ % 0.56/0.58 ___ / __ \_____(_)___ ________ __________ % 0.56/0.58 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.56/0.58 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.56/0.58 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.56/0.58 % 0.56/0.58 A Theorem Prover for First-Order Logic % 0.56/0.58 (ePrincess v.1.0) % 0.56/0.58 % 0.56/0.58 (c) Philipp Rümmer, 2009-2015 % 0.56/0.58 (c) Peter Backeman, 2014-2015 % 0.56/0.58 (contributions by Angelo Brillout, Peter Baumgartner) % 0.56/0.58 Free software under GNU Lesser General Public License (LGPL). % 0.56/0.58 Bug reports to peter@backeman.se % 0.56/0.58 % 0.56/0.58 For more information, visit http://user.uu.se/~petba168/breu/ % 0.56/0.58 % 0.56/0.58 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.62/0.63 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 2.62/1.13 Prover 0: Preprocessing ... % 4.70/1.58 Prover 0: Constructing countermodel ... % 5.96/1.81 Prover 0: proved (1189ms) % 5.96/1.82 % 5.96/1.82 No countermodel exists, formula is valid % 5.96/1.82 % SZS status Theorem for theBenchmark % 5.96/1.82 % 5.96/1.82 Generating proof ... found it (size 279) % 8.76/2.50 % 8.76/2.50 % SZS output start Proof for theBenchmark % 8.76/2.50 Assumed formulas after preprocessing and simplification: % 8.76/2.50 | (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] : ( ~ (v21 = v20) & ~ (v21 = v19) & ~ (v21 = v16) & ~ (v21 = v13) & ~ (v21 = e23) & ~ (v21 = e20) & ~ (v20 = v19) & ~ (v20 = v18) & ~ (v20 = v15) & ~ (v20 = v12) & ~ (v20 = e20) & ~ (v19 = v17) & ~ (v19 = v14) & ~ (v19 = v11) & ~ (v19 = e20) & ~ (v18 = v17) & ~ (v18 = v15) & ~ (v18 = v12) & ~ (v18 = e23) & ~ (v18 = e22) & ~ (v17 = v14) & ~ (v17 = v11) & ~ (v17 = e23) & ~ (v17 = e22) & ~ (v16 = v15) & ~ (v16 = v14) & ~ (v16 = v13) & ~ (v16 = e23) & ~ (v15 = v14) & ~ (v15 = v12) & ~ (v15 = e23) & ~ (v14 = v11) & ~ (v14 = e23) & ~ (v13 = v12) & ~ (v13 = v11) & ~ (v13 = e23) & ~ (v13 = e21) & ~ (v12 = v11) & ~ (v12 = e21) & ~ (v11 = e21) & ~ (v10 = v9) & ~ (v10 = v8) & ~ (v10 = v5) & ~ (v10 = v2) & ~ (v10 = e13) & ~ (v10 = e10) & ~ (v9 = v8) & ~ (v9 = v7) & ~ (v9 = v4) & ~ (v9 = v1) & ~ (v9 = e10) & ~ (v8 = v6) & ~ (v8 = v3) & ~ (v8 = v0) & ~ (v8 = e10) & ~ (v7 = v6) & ~ (v7 = v4) & ~ (v7 = v1) & ~ (v7 = e13) & ~ (v7 = e12) & ~ (v6 = v3) & ~ (v6 = v0) & ~ (v6 = e13) & ~ (v6 = e12) & ~ (v5 = v4) & ~ (v5 = v3) & ~ (v5 = v2) & ~ (v5 = e13) & ~ (v4 = v3) & ~ (v4 = v1) & ~ (v4 = e13) & ~ (v3 = v0) & ~ (v3 = e13) & ~ (v2 = v1) & ~ (v2 = v0) & ~ (v2 = e13) & ~ (v2 = e11) & ~ (v1 = v0) & ~ (v1 = e11) & ~ (v0 = e11) & ~ (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) = e10 & op1(e13, e12) = v10 & op1(e13, e11) = v9 & op1(e13, e10) = v8 & op1(e12, e13) = e12 & op1(e12, e12) = e13 & op1(e12, e11) = v7 & op1(e12, e10) = v6 & op1(e11, e13) = e13 & op1(e11, e12) = v5 & op1(e11, e11) = v4 & op1(e11, e10) = v3 & op1(e10, e13) = e11 & op1(e10, e12) = v2 & op1(e10, e11) = v1 & op1(e10, e10) = v0 & h1(v10) = v50 & h1(v9) = v48 & h1(v8) = v46 & h1(v7) = v43 & h1(v6) = v41 & h1(v5) = v38 & h1(v4) = v36 & h1(v3) = v34 & h1(v2) = v31 & h1(v1) = v29 & h1(v0) = v27 & h1(e13) = v11 & h1(e12) = e20 & h1(e11) = v23 & h1(e10) = v22 & h2(v10) = v76 & h2(v9) = v74 & h2(v8) = v72 & h2(v7) = v69 & h2(v6) = v67 & h2(v5) = v64 & h2(v4) = v62 & h2(v3) = v60 & h2(v2) = v57 & h2(v1) = v55 & h2(v0) = v53 & h2(e13) = v15 & h2(e12) = e21 & h2(e11) = v25 & h2(e10) = v24 & h3(v10) = v89 & h3(v9) = v88 & h3(v8) = v87 & h3(v7) = v86 & h3(v6) = v85 & h3(v5) = v84 & h3(v4) = v83 & h3(v3) = v82 & h3(v2) = v81 & h3(v1) = v80 & h3(v0) = v79 & h3(e13) = e23 & h3(e12) = e22 & h3(e11) = e21 & h3(e10) = e20 & h4(v10) = v112 & h4(v9) = v110 & h4(v8) = v108 & h4(v7) = v106 & h4(v6) = v104 & h4(v5) = v101 & h4(v4) = v99 & h4(v3) = v97 & h4(v2) = v94 & h4(v1) = v92 & h4(v0) = v90 & h4(e13) = e20 & h4(e12) = e23 & h4(e11) = v26 & h4(e10) = v11 & op2(v26, v26) = v100 & op2(v26, v11) = v98 & op2(v26, e23) = v102 & op2(v26, e20) = v103 & op2(v25, v25) = v63 & op2(v25, v24) = v61 & op2(v25, v15) = v66 & op2(v25, e21) = v65 & op2(v24, v25) = v56 & op2(v24, v24) = v54 & op2(v24, v15) = v59 & op2(v24, v15) = v25 & op2(v24, e21) = v58 & op2(v23, v23) = v37 & op2(v23, v22) = v35 & op2(v23, v11) = v40 & op2(v23, e20) = v39 & op2(v22, v23) = v30 & op2(v22, v22) = v28 & op2(v22, v11) = v33 & op2(v22, v11) = v23 & op2(v22, e20) = v32 & op2(v15, v25) = v75 & op2(v15, v24) = v73 & op2(v15, v15) = v78 & op2(v15, v15) = v24 & op2(v15, e21) = v77 & op2(v11, v26) = v93 & op2(v11, v23) = v49 & op2(v11, v22) = v47 & op2(v11, v11) = v91 & op2(v11, v11) = v52 & op2(v11, v11) = v22 & op2(v11, e23) = v95 & op2(v11, e20) = v96 & op2(v11, e20) = v51 & op2(v11, e20) = v26 & op2(e23, v26) = v107 & op2(e23, v11) = v105 & op2(e23, e23) = e20 & op2(e23, e22) = v21 & op2(e23, e21) = v20 & op2(e23, e20) = v19 & op2(e22, e23) = e22 & op2(e22, e22) = e23 & op2(e22, e21) = v18 & op2(e22, e20) = v17 & op2(e21, v25) = v70 & op2(e21, v24) = v68 & op2(e21, v15) = v71 & op2(e21, e23) = e23 & op2(e21, e22) = v16 & op2(e21, e21) = v15 & op2(e21, e20) = v14 & op2(e20, v26) = v111 & op2(e20, v23) = v44 & op2(e20, v22) = v42 & op2(e20, v11) = v109 & op2(e20, v11) = v45 & op2(e20, e23) = e21 & op2(e20, e22) = v13 & op2(e20, e21) = v12 & op2(e20, e20) = v11 & ! [v113] : ! [v114] : ! [v115] : ! [v116] : (v114 = v113 | ~ (op1(v116, v115) = v114) | ~ (op1(v116, v115) = v113)) & ! [v113] : ! [v114] : ! [v115] : ! [v116] : (v114 = v113 | ~ (op2(v116, v115) = v114) | ~ (op2(v116, v115) = v113)) & ! [v113] : ! [v114] : ! [v115] : (v114 = v113 | ~ (h1(v115) = v114) | ~ (h1(v115) = v113)) & ! [v113] : ! [v114] : ! [v115] : (v114 = v113 | ~ (h2(v115) = v114) | ~ (h2(v115) = v113)) & ! [v113] : ! [v114] : ! [v115] : (v114 = v113 | ~ (h3(v115) = v114) | ~ (h3(v115) = v113)) & ! [v113] : ! [v114] : ! [v115] : (v114 = v113 | ~ (h4(v115) = v114) | ~ (h4(v115) = v113)) & ( ~ (v112 = e21) | ~ (v111 = v110) | ~ (v109 = v108) | ~ (v107 = v106) | ~ (v105 = v104) | ~ (v103 = e20) | ~ (v102 = v101) | ~ (v100 = v99) | ~ (v98 = v97) | ~ (v96 = e21) | ~ (v95 = v94) | ~ (v93 = v92) | ~ (v91 = v90) | ~ (v26 = e21) | ~ (v19 = e23) | ~ (v11 = e22)) & ( ~ (v89 = v21) | ~ (v88 = v20) | ~ (v87 = v19) | ~ (v86 = v18) | ~ (v85 = v17) | ~ (v84 = v16) | ~ (v83 = v15) | ~ (v82 = v14) | ~ (v81 = v13) | ~ (v80 = v12) | ~ (v79 = v11)) & ( ~ (v78 = v24) | ~ (v77 = v76) | ~ (v75 = v74) | ~ (v73 = v72) | ~ (v71 = e21) | ~ (v70 = v69) | ~ (v68 = v67) | ~ (v66 = v15) | ~ (v65 = v64) | ~ (v63 = v62) | ~ (v61 = v60) | ~ (v59 = v25) | ~ (v58 = v57) | ~ (v56 = v55) | ~ (v54 = v53) | ( ~ (v25 = e23) & ~ (v24 = e23)) | ( ~ (v25 = e22) & ~ (v24 = e22) & ~ (v15 = e22)) | ( ~ (v25 = e20) & ~ (v24 = e20) & ~ (v15 = e20))) & ( ~ (v52 = v22) | ~ (v51 = v50) | ~ (v49 = v48) | ~ (v47 = v46) | ~ (v45 = e20) | ~ (v44 = v43) | ~ (v42 = v41) | ~ (v40 = v11) | ~ (v39 = v38) | ~ (v37 = v36) | ~ (v35 = v34) | ~ (v33 = v23) | ~ (v32 = v31) | ~ (v30 = v29) | ~ (v28 = v27) | ( ~ (v23 = e23) & ~ (v22 = e23) & ~ (v11 = e23)) | ( ~ (v23 = e22) & ~ (v22 = e22) & ~ (v11 = e22)) | ( ~ (v23 = e21) & ~ (v22 = e21))) & (v21 = e22 | v21 = e21) & (v21 = e22 | v20 = e22 | v19 = e22) & (v21 = e22 | v16 = e22 | v13 = e22) & (v21 = e21 | v20 = e21 | v19 = e21) & (v21 = e21 | v16 = e21) & (v20 = e23 | v20 = e22 | v20 = e21) & (v20 = e23 | v19 = e23) & (v20 = e23 | v12 = e23) & (v20 = e23 | (v12 = e20 & ~ (v14 = e21))) & (v20 = e22 | v15 = e22 | v12 = e22) & (v20 = e21 | v18 = e21 | v15 = e21) & (v19 = e23 | v19 = e22 | v19 = e21) & (v19 = e23 | v11 = e23) & (v19 = e23 | (v14 = e21 & ~ (v12 = e20))) & (v19 = e22 | v14 = e22 | v11 = e22) & (v19 = e21 | v17 = e21 | v14 = e21) & (v18 = e21 | v18 = e20) & (v18 = e21 | v17 = e21) & (v18 = e20 | v17 = e20) & (v18 = e20 | v15 = e20 | v12 = e20) & (v17 = e21 | v17 = e20) & (v17 = e20 | v14 = e20 | v11 = e20) & (v16 = e22 | v16 = e21 | v16 = e20) & (v16 = e22 | v15 = e22 | v14 = e22) & (v16 = e21 | v15 = e21 | v14 = e21) & (v16 = e21 | v13 = e20) & (v16 = e20 | v15 = e20 | v14 = e20) & (v16 = e20 | v13 = e20) & (v15 = e22 | v15 = e21 | v15 = e20) & (v14 = e22 | v14 = e21 | v14 = e20) & (v13 = e22 | v13 = e20) & (v13 = e22 | v12 = e22 | v11 = e22) & (v13 = e20 | v12 = e20 | v11 = e20) & (v12 = e23 | v12 = e22 | v12 = e20) & (v12 = e23 | v11 = e23) & (v11 = e23 | v11 = e22 | v11 = e20) & (v10 = e12 | v10 = e11) & (v10 = e12 | v9 = e12 | v8 = e12) & (v10 = e12 | v5 = e12 | v2 = e12) & (v10 = e11 | v9 = e11 | v8 = e11) & (v10 = e11 | v5 = e11) & (v9 = e13 | v9 = e12 | v9 = e11) & (v9 = e13 | v8 = e13) & (v9 = e13 | v1 = e13) & (v9 = e13 | (v1 = e10 & ~ (v3 = e11))) & (v9 = e12 | v4 = e12 | v1 = e12) & (v9 = e11 | v7 = e11 | v4 = e11) & (v8 = e13 | v8 = e12 | v8 = e11) & (v8 = e13 | v0 = e13) & (v8 = e13 | (v3 = e11 & ~ (v1 = e10))) & (v8 = e12 | v3 = e12 | v0 = e12) & (v8 = e11 | v6 = e11 | v3 = e11) & (v7 = e11 | v7 = e10) & (v7 = e11 | v6 = e11) & (v7 = e10 | v6 = e10) & (v7 = e10 | v4 = e10 | v1 = e10) & (v6 = e11 | v6 = e10) & (v6 = e10 | v3 = e10 | v0 = e10) & (v5 = e12 | v5 = e11 | v5 = e10) & (v5 = e12 | v4 = e12 | v3 = e12) & (v5 = e11 | v4 = e11 | v3 = e11) & (v5 = e11 | v2 = e10) & (v5 = e10 | v4 = e10 | v3 = e10) & (v5 = e10 | v2 = e10) & (v4 = e12 | v4 = e11 | v4 = e10) & (v3 = e12 | v3 = e11 | v3 = e10) & (v2 = e12 | v2 = e10) & (v2 = e12 | v1 = e12 | v0 = e12) & (v2 = e10 | v1 = e10 | v0 = e10) & (v1 = e13 | v1 = e12 | v1 = e10) & (v1 = e13 | v0 = e13) & (v0 = e13 | v0 = e12 | v0 = e10)) % 8.76/2.55 | 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 yields: % 8.76/2.55 | (1) ~ (all_0_91_91 = all_0_92_92) & ~ (all_0_91_91 = all_0_93_93) & ~ (all_0_91_91 = all_0_96_96) & ~ (all_0_91_91 = all_0_99_99) & ~ (all_0_91_91 = e23) & ~ (all_0_91_91 = e20) & ~ (all_0_92_92 = all_0_93_93) & ~ (all_0_92_92 = all_0_94_94) & ~ (all_0_92_92 = all_0_97_97) & ~ (all_0_92_92 = all_0_100_100) & ~ (all_0_92_92 = e20) & ~ (all_0_93_93 = all_0_95_95) & ~ (all_0_93_93 = all_0_98_98) & ~ (all_0_93_93 = all_0_101_101) & ~ (all_0_93_93 = e20) & ~ (all_0_94_94 = all_0_95_95) & ~ (all_0_94_94 = all_0_97_97) & ~ (all_0_94_94 = all_0_100_100) & ~ (all_0_94_94 = e23) & ~ (all_0_94_94 = e22) & ~ (all_0_95_95 = all_0_98_98) & ~ (all_0_95_95 = all_0_101_101) & ~ (all_0_95_95 = e23) & ~ (all_0_95_95 = e22) & ~ (all_0_96_96 = all_0_97_97) & ~ (all_0_96_96 = all_0_98_98) & ~ (all_0_96_96 = all_0_99_99) & ~ (all_0_96_96 = e23) & ~ (all_0_97_97 = all_0_98_98) & ~ (all_0_97_97 = all_0_100_100) & ~ (all_0_97_97 = e23) & ~ (all_0_98_98 = all_0_101_101) & ~ (all_0_98_98 = e23) & ~ (all_0_99_99 = all_0_100_100) & ~ (all_0_99_99 = all_0_101_101) & ~ (all_0_99_99 = e23) & ~ (all_0_99_99 = e21) & ~ (all_0_100_100 = all_0_101_101) & ~ (all_0_100_100 = e21) & ~ (all_0_101_101 = e21) & ~ (all_0_102_102 = all_0_103_103) & ~ (all_0_102_102 = all_0_104_104) & ~ (all_0_102_102 = all_0_107_107) & ~ (all_0_102_102 = all_0_110_110) & ~ (all_0_102_102 = e13) & ~ (all_0_102_102 = e10) & ~ (all_0_103_103 = all_0_104_104) & ~ (all_0_103_103 = all_0_105_105) & ~ (all_0_103_103 = all_0_108_108) & ~ (all_0_103_103 = all_0_111_111) & ~ (all_0_103_103 = e10) & ~ (all_0_104_104 = all_0_106_106) & ~ (all_0_104_104 = all_0_109_109) & ~ (all_0_104_104 = all_0_112_112) & ~ (all_0_104_104 = e10) & ~ (all_0_105_105 = all_0_106_106) & ~ (all_0_105_105 = all_0_108_108) & ~ (all_0_105_105 = all_0_111_111) & ~ (all_0_105_105 = e13) & ~ (all_0_105_105 = e12) & ~ (all_0_106_106 = all_0_109_109) & ~ (all_0_106_106 = all_0_112_112) & ~ (all_0_106_106 = e13) & ~ (all_0_106_106 = e12) & ~ (all_0_107_107 = all_0_108_108) & ~ (all_0_107_107 = all_0_109_109) & ~ (all_0_107_107 = all_0_110_110) & ~ (all_0_107_107 = e13) & ~ (all_0_108_108 = all_0_109_109) & ~ (all_0_108_108 = all_0_111_111) & ~ (all_0_108_108 = e13) & ~ (all_0_109_109 = all_0_112_112) & ~ (all_0_109_109 = e13) & ~ (all_0_110_110 = all_0_111_111) & ~ (all_0_110_110 = all_0_112_112) & ~ (all_0_110_110 = e13) & ~ (all_0_110_110 = e11) & ~ (all_0_111_111 = all_0_112_112) & ~ (all_0_111_111 = e11) & ~ (all_0_112_112 = e11) & ~ (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) = e10 & op1(e13, e12) = all_0_102_102 & op1(e13, e11) = all_0_103_103 & op1(e13, e10) = all_0_104_104 & op1(e12, e13) = e12 & op1(e12, e12) = e13 & op1(e12, e11) = all_0_105_105 & op1(e12, e10) = all_0_106_106 & op1(e11, e13) = e13 & op1(e11, e12) = all_0_107_107 & op1(e11, e11) = all_0_108_108 & op1(e11, e10) = all_0_109_109 & op1(e10, e13) = e11 & op1(e10, e12) = all_0_110_110 & op1(e10, e11) = all_0_111_111 & op1(e10, e10) = all_0_112_112 & h1(all_0_102_102) = all_0_62_62 & h1(all_0_103_103) = all_0_64_64 & h1(all_0_104_104) = all_0_66_66 & h1(all_0_105_105) = all_0_69_69 & h1(all_0_106_106) = all_0_71_71 & h1(all_0_107_107) = all_0_74_74 & h1(all_0_108_108) = all_0_76_76 & h1(all_0_109_109) = all_0_78_78 & h1(all_0_110_110) = all_0_81_81 & h1(all_0_111_111) = all_0_83_83 & h1(all_0_112_112) = all_0_85_85 & h1(e13) = all_0_101_101 & h1(e12) = e20 & h1(e11) = all_0_89_89 & h1(e10) = all_0_90_90 & h2(all_0_102_102) = all_0_36_36 & h2(all_0_103_103) = all_0_38_38 & h2(all_0_104_104) = all_0_40_40 & h2(all_0_105_105) = all_0_43_43 & h2(all_0_106_106) = all_0_45_45 & h2(all_0_107_107) = all_0_48_48 & h2(all_0_108_108) = all_0_50_50 & h2(all_0_109_109) = all_0_52_52 & h2(all_0_110_110) = all_0_55_55 & h2(all_0_111_111) = all_0_57_57 & h2(all_0_112_112) = all_0_59_59 & h2(e13) = all_0_97_97 & h2(e12) = e21 & h2(e11) = all_0_87_87 & h2(e10) = all_0_88_88 & h3(all_0_102_102) = all_0_23_23 & h3(all_0_103_103) = all_0_24_24 & h3(all_0_104_104) = all_0_25_25 & h3(all_0_105_105) = all_0_26_26 & h3(all_0_106_106) = all_0_27_27 & h3(all_0_107_107) = all_0_28_28 & h3(all_0_108_108) = all_0_29_29 & h3(all_0_109_109) = all_0_30_30 & h3(all_0_110_110) = all_0_31_31 & h3(all_0_111_111) = all_0_32_32 & h3(all_0_112_112) = all_0_33_33 & h3(e13) = e23 & h3(e12) = e22 & h3(e11) = e21 & h3(e10) = e20 & h4(all_0_102_102) = all_0_0_0 & h4(all_0_103_103) = all_0_2_2 & h4(all_0_104_104) = all_0_4_4 & h4(all_0_105_105) = all_0_6_6 & h4(all_0_106_106) = all_0_8_8 & h4(all_0_107_107) = all_0_11_11 & h4(all_0_108_108) = all_0_13_13 & h4(all_0_109_109) = all_0_15_15 & h4(all_0_110_110) = all_0_18_18 & h4(all_0_111_111) = all_0_20_20 & h4(all_0_112_112) = all_0_22_22 & h4(e13) = e20 & h4(e12) = e23 & h4(e11) = all_0_86_86 & h4(e10) = all_0_101_101 & op2(all_0_86_86, all_0_86_86) = all_0_12_12 & op2(all_0_86_86, all_0_101_101) = all_0_14_14 & op2(all_0_86_86, e23) = all_0_10_10 & op2(all_0_86_86, e20) = all_0_9_9 & op2(all_0_87_87, all_0_87_87) = all_0_49_49 & op2(all_0_87_87, all_0_88_88) = all_0_51_51 & op2(all_0_87_87, all_0_97_97) = all_0_46_46 & op2(all_0_87_87, e21) = all_0_47_47 & op2(all_0_88_88, all_0_87_87) = all_0_56_56 & op2(all_0_88_88, all_0_88_88) = all_0_58_58 & op2(all_0_88_88, all_0_97_97) = all_0_53_53 & op2(all_0_88_88, all_0_97_97) = all_0_87_87 & op2(all_0_88_88, e21) = all_0_54_54 & op2(all_0_89_89, all_0_89_89) = all_0_75_75 & op2(all_0_89_89, all_0_90_90) = all_0_77_77 & op2(all_0_89_89, all_0_101_101) = all_0_72_72 & op2(all_0_89_89, e20) = all_0_73_73 & op2(all_0_90_90, all_0_89_89) = all_0_82_82 & op2(all_0_90_90, all_0_90_90) = all_0_84_84 & op2(all_0_90_90, all_0_101_101) = all_0_79_79 & op2(all_0_90_90, all_0_101_101) = all_0_89_89 & op2(all_0_90_90, e20) = all_0_80_80 & op2(all_0_97_97, all_0_87_87) = all_0_37_37 & op2(all_0_97_97, all_0_88_88) = all_0_39_39 & op2(all_0_97_97, all_0_97_97) = all_0_34_34 & op2(all_0_97_97, all_0_97_97) = all_0_88_88 & op2(all_0_97_97, e21) = all_0_35_35 & op2(all_0_101_101, all_0_86_86) = all_0_19_19 & op2(all_0_101_101, all_0_89_89) = all_0_63_63 & op2(all_0_101_101, all_0_90_90) = all_0_65_65 & op2(all_0_101_101, all_0_101_101) = all_0_21_21 & op2(all_0_101_101, all_0_101_101) = all_0_60_60 & op2(all_0_101_101, all_0_101_101) = all_0_90_90 & op2(all_0_101_101, e23) = all_0_17_17 & op2(all_0_101_101, e20) = all_0_16_16 & op2(all_0_101_101, e20) = all_0_61_61 & op2(all_0_101_101, e20) = all_0_86_86 & op2(e23, all_0_86_86) = all_0_5_5 & op2(e23, all_0_101_101) = all_0_7_7 & op2(e23, e23) = e20 & op2(e23, e22) = all_0_91_91 & op2(e23, e21) = all_0_92_92 & op2(e23, e20) = all_0_93_93 & op2(e22, e23) = e22 & op2(e22, e22) = e23 & op2(e22, e21) = all_0_94_94 & op2(e22, e20) = all_0_95_95 & op2(e21, all_0_87_87) = all_0_42_42 & op2(e21, all_0_88_88) = all_0_44_44 & op2(e21, all_0_97_97) = all_0_41_41 & op2(e21, e23) = e23 & op2(e21, e22) = all_0_96_96 & op2(e21, e21) = all_0_97_97 & op2(e21, e20) = all_0_98_98 & op2(e20, all_0_86_86) = all_0_1_1 & op2(e20, all_0_89_89) = all_0_68_68 & op2(e20, all_0_90_90) = all_0_70_70 & op2(e20, all_0_101_101) = all_0_3_3 & op2(e20, all_0_101_101) = all_0_67_67 & op2(e20, e23) = e21 & op2(e20, e22) = all_0_99_99 & op2(e20, e21) = all_0_100_100 & op2(e20, e20) = all_0_101_101 & ! [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 = e21) | ~ (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 = e20) | ~ (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 = e21) | ~ (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_86_86 = e21) | ~ (all_0_93_93 = e23) | ~ (all_0_101_101 = e22)) & ( ~ (all_0_23_23 = all_0_91_91) | ~ (all_0_24_24 = all_0_92_92) | ~ (all_0_25_25 = all_0_93_93) | ~ (all_0_26_26 = all_0_94_94) | ~ (all_0_27_27 = all_0_95_95) | ~ (all_0_28_28 = all_0_96_96) | ~ (all_0_29_29 = all_0_97_97) | ~ (all_0_30_30 = all_0_98_98) | ~ (all_0_31_31 = all_0_99_99) | ~ (all_0_32_32 = all_0_100_100) | ~ (all_0_33_33 = all_0_101_101)) & ( ~ (all_0_34_34 = all_0_88_88) | ~ (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 = e21) | ~ (all_0_42_42 = all_0_43_43) | ~ (all_0_44_44 = all_0_45_45) | ~ (all_0_46_46 = all_0_97_97) | ~ (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_87_87) | ~ (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_87_87 = e23) & ~ (all_0_88_88 = e23)) | ( ~ (all_0_87_87 = e22) & ~ (all_0_88_88 = e22) & ~ (all_0_97_97 = e22)) | ( ~ (all_0_87_87 = e20) & ~ (all_0_88_88 = e20) & ~ (all_0_97_97 = e20))) & ( ~ (all_0_60_60 = all_0_90_90) | ~ (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 = e20) | ~ (all_0_68_68 = all_0_69_69) | ~ (all_0_70_70 = all_0_71_71) | ~ (all_0_72_72 = all_0_101_101) | ~ (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_89_89) | ~ (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_89_89 = e23) & ~ (all_0_90_90 = e23) & ~ (all_0_101_101 = e23)) | ( ~ (all_0_89_89 = e22) & ~ (all_0_90_90 = e22) & ~ (all_0_101_101 = e22)) | ( ~ (all_0_89_89 = e21) & ~ (all_0_90_90 = e21))) & (all_0_91_91 = e22 | all_0_91_91 = e21) & (all_0_91_91 = e22 | all_0_92_92 = e22 | all_0_93_93 = e22) & (all_0_91_91 = e22 | all_0_96_96 = e22 | all_0_99_99 = e22) & (all_0_91_91 = e21 | all_0_92_92 = e21 | all_0_93_93 = e21) & (all_0_91_91 = e21 | all_0_96_96 = e21) & (all_0_92_92 = e23 | all_0_92_92 = e22 | all_0_92_92 = e21) & (all_0_92_92 = e23 | all_0_93_93 = e23) & (all_0_92_92 = e23 | all_0_100_100 = e23) & (all_0_92_92 = e23 | (all_0_100_100 = e20 & ~ (all_0_98_98 = e21))) & (all_0_92_92 = e22 | all_0_97_97 = e22 | all_0_100_100 = e22) & (all_0_92_92 = e21 | all_0_94_94 = e21 | all_0_97_97 = e21) & (all_0_93_93 = e23 | all_0_93_93 = e22 | all_0_93_93 = e21) & (all_0_93_93 = e23 | all_0_101_101 = e23) & (all_0_93_93 = e23 | (all_0_98_98 = e21 & ~ (all_0_100_100 = e20))) & (all_0_93_93 = e22 | all_0_98_98 = e22 | all_0_101_101 = e22) & (all_0_93_93 = e21 | all_0_95_95 = e21 | all_0_98_98 = e21) & (all_0_94_94 = e21 | all_0_94_94 = e20) & (all_0_94_94 = e21 | all_0_95_95 = e21) & (all_0_94_94 = e20 | all_0_95_95 = e20) & (all_0_94_94 = e20 | all_0_97_97 = e20 | all_0_100_100 = e20) & (all_0_95_95 = e21 | all_0_95_95 = e20) & (all_0_95_95 = e20 | all_0_98_98 = e20 | all_0_101_101 = e20) & (all_0_96_96 = e22 | all_0_96_96 = e21 | all_0_96_96 = e20) & (all_0_96_96 = e22 | all_0_97_97 = e22 | all_0_98_98 = e22) & (all_0_96_96 = e21 | all_0_97_97 = e21 | all_0_98_98 = e21) & (all_0_96_96 = e21 | all_0_99_99 = e20) & (all_0_96_96 = e20 | all_0_97_97 = e20 | all_0_98_98 = e20) & (all_0_96_96 = e20 | all_0_99_99 = e20) & (all_0_97_97 = e22 | all_0_97_97 = e21 | all_0_97_97 = e20) & (all_0_98_98 = e22 | all_0_98_98 = e21 | all_0_98_98 = e20) & (all_0_99_99 = e22 | all_0_99_99 = e20) & (all_0_99_99 = e22 | all_0_100_100 = e22 | all_0_101_101 = e22) & (all_0_99_99 = e20 | all_0_100_100 = e20 | all_0_101_101 = e20) & (all_0_100_100 = e23 | all_0_100_100 = e22 | all_0_100_100 = e20) & (all_0_100_100 = e23 | all_0_101_101 = e23) & (all_0_101_101 = e23 | all_0_101_101 = e22 | all_0_101_101 = e20) & (all_0_102_102 = e12 | all_0_102_102 = e11) & (all_0_102_102 = e12 | all_0_103_103 = e12 | all_0_104_104 = e12) & (all_0_102_102 = e12 | all_0_107_107 = e12 | all_0_110_110 = e12) & (all_0_102_102 = e11 | all_0_103_103 = e11 | all_0_104_104 = e11) & (all_0_102_102 = e11 | all_0_107_107 = e11) & (all_0_103_103 = e13 | all_0_103_103 = e12 | all_0_103_103 = e11) & (all_0_103_103 = e13 | all_0_104_104 = e13) & (all_0_103_103 = e13 | all_0_111_111 = e13) & (all_0_103_103 = e13 | (all_0_111_111 = e10 & ~ (all_0_109_109 = e11))) & (all_0_103_103 = e12 | all_0_108_108 = e12 | all_0_111_111 = e12) & (all_0_103_103 = e11 | all_0_105_105 = e11 | all_0_108_108 = e11) & (all_0_104_104 = e13 | all_0_104_104 = e12 | all_0_104_104 = e11) & (all_0_104_104 = e13 | all_0_112_112 = e13) & (all_0_104_104 = e13 | (all_0_109_109 = e11 & ~ (all_0_111_111 = e10))) & (all_0_104_104 = e12 | all_0_109_109 = e12 | all_0_112_112 = e12) & (all_0_104_104 = e11 | all_0_106_106 = e11 | all_0_109_109 = e11) & (all_0_105_105 = e11 | all_0_105_105 = e10) & (all_0_105_105 = e11 | all_0_106_106 = e11) & (all_0_105_105 = e10 | all_0_106_106 = e10) & (all_0_105_105 = e10 | all_0_108_108 = e10 | all_0_111_111 = e10) & (all_0_106_106 = e11 | all_0_106_106 = e10) & (all_0_106_106 = e10 | all_0_109_109 = e10 | all_0_112_112 = e10) & (all_0_107_107 = e12 | all_0_107_107 = e11 | all_0_107_107 = e10) & (all_0_107_107 = e12 | all_0_108_108 = e12 | all_0_109_109 = e12) & (all_0_107_107 = e11 | all_0_108_108 = e11 | all_0_109_109 = e11) & (all_0_107_107 = e11 | all_0_110_110 = e10) & (all_0_107_107 = e10 | all_0_108_108 = e10 | all_0_109_109 = e10) & (all_0_107_107 = e10 | all_0_110_110 = e10) & (all_0_108_108 = e12 | all_0_108_108 = e11 | all_0_108_108 = e10) & (all_0_109_109 = e12 | all_0_109_109 = e11 | all_0_109_109 = e10) & (all_0_110_110 = e12 | all_0_110_110 = e10) & (all_0_110_110 = e12 | all_0_111_111 = e12 | all_0_112_112 = e12) & (all_0_110_110 = e10 | all_0_111_111 = e10 | all_0_112_112 = e10) & (all_0_111_111 = e13 | all_0_111_111 = e12 | all_0_111_111 = e10) & (all_0_111_111 = e13 | all_0_112_112 = e13) & (all_0_112_112 = e13 | all_0_112_112 = e12 | all_0_112_112 = e10) % 8.76/2.56 | % 8.76/2.56 | Applying alpha-rule on (1) yields: % 8.76/2.56 | (2) all_0_96_96 = e21 | all_0_97_97 = e21 | all_0_98_98 = e21 % 8.76/2.56 | (3) h3(e11) = e21 % 8.76/2.56 | (4) op2(all_0_97_97, all_0_88_88) = all_0_39_39 % 8.76/2.56 | (5) op2(all_0_86_86, all_0_86_86) = all_0_12_12 % 8.76/2.56 | (6) h4(all_0_112_112) = all_0_22_22 % 8.76/2.56 | (7) ~ (e22 = e13) % 8.76/2.56 | (8) op2(e21, e23) = e23 % 8.76/2.56 | (9) all_0_102_102 = e11 | all_0_107_107 = e11 % 8.76/2.56 | (10) ~ (all_0_106_106 = all_0_112_112) % 8.76/2.56 | (11) op1(e12, e12) = e13 % 8.76/2.56 | (12) ~ (all_0_94_94 = all_0_97_97) % 8.76/2.56 | (13) op2(all_0_101_101, all_0_101_101) = all_0_60_60 % 8.76/2.56 | (14) h2(e12) = e21 % 8.76/2.56 | (15) h2(all_0_109_109) = all_0_52_52 % 8.76/2.56 | (16) all_0_94_94 = e21 | all_0_94_94 = e20 % 8.76/2.56 | (17) ~ (all_0_103_103 = e10) % 8.76/2.56 | (18) ~ (all_0_93_93 = e20) % 8.76/2.56 | (19) h2(e13) = all_0_97_97 % 8.76/2.56 | (20) op2(e22, e23) = e22 % 8.76/2.56 | (21) op2(e20, all_0_90_90) = all_0_70_70 % 8.76/2.56 | (22) all_0_105_105 = e11 | all_0_106_106 = e11 % 8.76/2.56 | (23) h1(all_0_112_112) = all_0_85_85 % 8.76/2.56 | (24) ~ (all_0_103_103 = all_0_111_111) % 8.76/2.56 | (25) ~ (all_0_96_96 = all_0_97_97) % 8.76/2.56 | (26) h3(all_0_109_109) = all_0_30_30 % 8.76/2.56 | (27) ~ (all_0_95_95 = e22) % 8.76/2.56 | (28) all_0_97_97 = e22 | all_0_97_97 = e21 | all_0_97_97 = e20 % 8.76/2.56 | (29) ~ (all_0_102_102 = all_0_103_103) % 8.76/2.56 | (30) op2(all_0_101_101, all_0_89_89) = all_0_63_63 % 8.76/2.56 | (31) op2(all_0_86_86, e20) = all_0_9_9 % 8.76/2.56 | (32) ~ (all_0_91_91 = all_0_99_99) % 8.76/2.56 | (33) ~ (e21 = e11) % 8.76/2.56 | (34) h2(all_0_102_102) = all_0_36_36 % 8.76/2.56 | (35) ~ (all_0_98_98 = all_0_101_101) % 8.76/2.57 | (36) op1(e13, e10) = all_0_104_104 % 8.76/2.57 | (37) ~ (all_0_102_102 = all_0_107_107) % 8.76/2.57 | (38) ~ (all_0_60_60 = all_0_90_90) | ~ (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 = e20) | ~ (all_0_68_68 = all_0_69_69) | ~ (all_0_70_70 = all_0_71_71) | ~ (all_0_72_72 = all_0_101_101) | ~ (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_89_89) | ~ (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_89_89 = e23) & ~ (all_0_90_90 = e23) & ~ (all_0_101_101 = e23)) | ( ~ (all_0_89_89 = e22) & ~ (all_0_90_90 = e22) & ~ (all_0_101_101 = e22)) | ( ~ (all_0_89_89 = e21) & ~ (all_0_90_90 = e21)) % 8.76/2.57 | (39) all_0_109_109 = e12 | all_0_109_109 = e11 | all_0_109_109 = e10 % 8.76/2.57 | (40) all_0_98_98 = e22 | all_0_98_98 = e21 | all_0_98_98 = e20 % 8.76/2.57 | (41) ~ (all_0_109_109 = e13) % 8.76/2.57 | (42) op2(e21, e21) = all_0_97_97 % 8.76/2.57 | (43) ~ (all_0_92_92 = all_0_94_94) % 8.76/2.57 | (44) op2(all_0_90_90, all_0_90_90) = all_0_84_84 % 8.76/2.57 | (45) h4(all_0_102_102) = all_0_0_0 % 8.76/2.57 | (46) all_0_91_91 = e21 | all_0_96_96 = e21 % 8.76/2.57 | (47) all_0_96_96 = e22 | all_0_97_97 = e22 | all_0_98_98 = e22 % 8.76/2.57 | (48) op2(e21, e20) = all_0_98_98 % 8.76/2.57 | (49) all_0_102_102 = e12 | all_0_102_102 = e11 % 8.76/2.57 | (50) all_0_104_104 = e12 | all_0_109_109 = e12 | all_0_112_112 = e12 % 8.76/2.57 | (51) h2(all_0_105_105) = all_0_43_43 % 8.76/2.57 | (52) h1(all_0_106_106) = all_0_71_71 % 8.76/2.57 | (53) h4(all_0_106_106) = all_0_8_8 % 8.76/2.57 | (54) all_0_95_95 = e20 | all_0_98_98 = e20 | all_0_101_101 = e20 % 8.76/2.57 | (55) h4(all_0_105_105) = all_0_6_6 % 8.76/2.57 | (56) op2(e20, all_0_101_101) = all_0_3_3 % 8.76/2.57 | (57) op2(all_0_86_86, all_0_101_101) = all_0_14_14 % 8.76/2.57 | (58) ~ (e12 = e11) % 8.76/2.57 | (59) op2(all_0_101_101, all_0_90_90) = all_0_65_65 % 8.76/2.57 | (60) h1(all_0_104_104) = all_0_66_66 % 8.76/2.57 | (61) ~ (all_0_97_97 = all_0_100_100) % 8.76/2.57 | (62) h3(all_0_105_105) = all_0_26_26 % 8.76/2.57 | (63) ~ (all_0_105_105 = e13) % 8.76/2.57 | (64) ~ (e23 = e10) % 8.76/2.57 | (65) op2(e23, all_0_101_101) = all_0_7_7 % 8.76/2.57 | (66) op2(all_0_88_88, e21) = all_0_54_54 % 8.76/2.57 | (67) all_0_100_100 = e23 | all_0_101_101 = e23 % 8.76/2.57 | (68) all_0_108_108 = e12 | all_0_108_108 = e11 | all_0_108_108 = e10 % 8.76/2.57 | (69) op2(all_0_89_89, all_0_89_89) = all_0_75_75 % 8.76/2.57 | (70) h4(all_0_111_111) = all_0_20_20 % 8.76/2.57 | (71) all_0_110_110 = e10 | all_0_111_111 = e10 | all_0_112_112 = e10 % 8.76/2.57 | (72) h2(all_0_103_103) = all_0_38_38 % 8.76/2.57 | (73) op1(e13, e12) = all_0_102_102 % 8.76/2.57 | (74) ~ (e23 = e13) % 8.76/2.57 | (75) all_0_95_95 = e21 | all_0_95_95 = e20 % 8.76/2.57 | (76) h3(e12) = e22 % 8.76/2.57 | (77) ~ (all_0_92_92 = e20) % 8.76/2.57 | (78) all_0_107_107 = e12 | all_0_108_108 = e12 | all_0_109_109 = e12 % 8.76/2.57 | (79) ~ (e13 = e10) % 8.76/2.57 | (80) all_0_103_103 = e13 | all_0_104_104 = e13 % 8.76/2.57 | (81) all_0_105_105 = e10 | all_0_108_108 = e10 | all_0_111_111 = e10 % 8.76/2.57 | (82) ~ (all_0_104_104 = all_0_109_109) % 8.76/2.57 | (83) op2(e20, e22) = all_0_99_99 % 8.76/2.57 | (84) op2(all_0_89_89, all_0_90_90) = all_0_77_77 % 8.76/2.57 | (85) ~ (all_0_107_107 = all_0_109_109) % 8.76/2.57 | (86) op1(e13, e11) = all_0_103_103 % 8.76/2.57 | (87) ~ (all_0_99_99 = all_0_101_101) % 8.76/2.57 | (88) ~ (all_0_103_103 = all_0_105_105) % 8.76/2.57 | (89) all_0_99_99 = e20 | all_0_100_100 = e20 | all_0_101_101 = e20 % 8.76/2.57 | (90) ~ (all_0_95_95 = e23) % 8.76/2.57 | (91) all_0_102_102 = e11 | all_0_103_103 = e11 | all_0_104_104 = e11 % 8.76/2.57 | (92) op2(e23, e22) = all_0_91_91 % 8.76/2.57 | (93) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h2(v2) = v1) | ~ (h2(v2) = v0)) % 8.76/2.57 | (94) op2(all_0_97_97, e21) = all_0_35_35 % 8.76/2.57 | (95) ~ (all_0_105_105 = all_0_108_108) % 8.76/2.57 | (96) h1(all_0_102_102) = all_0_62_62 % 8.76/2.57 | (97) all_0_92_92 = e21 | all_0_94_94 = e21 | all_0_97_97 = e21 % 8.76/2.57 | (98) ~ (all_0_23_23 = all_0_91_91) | ~ (all_0_24_24 = all_0_92_92) | ~ (all_0_25_25 = all_0_93_93) | ~ (all_0_26_26 = all_0_94_94) | ~ (all_0_27_27 = all_0_95_95) | ~ (all_0_28_28 = all_0_96_96) | ~ (all_0_29_29 = all_0_97_97) | ~ (all_0_30_30 = all_0_98_98) | ~ (all_0_31_31 = all_0_99_99) | ~ (all_0_32_32 = all_0_100_100) | ~ (all_0_33_33 = all_0_101_101) % 8.76/2.57 | (99) ~ (e20 = e11) % 8.76/2.57 | (100) op2(all_0_101_101, e20) = all_0_86_86 % 8.76/2.57 | (101) all_0_110_110 = e12 | all_0_111_111 = e12 | all_0_112_112 = e12 % 8.76/2.57 | (102) all_0_105_105 = e10 | all_0_106_106 = e10 % 8.76/2.57 | (103) h1(all_0_103_103) = all_0_64_64 % 8.76/2.57 | (104) ~ (all_0_0_0 = e21) | ~ (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 = e20) | ~ (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 = e21) | ~ (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_86_86 = e21) | ~ (all_0_93_93 = e23) | ~ (all_0_101_101 = e22) % 8.76/2.57 | (105) ~ (e21 = e13) % 8.76/2.57 | (106) ~ (all_0_104_104 = e10) % 8.76/2.57 | (107) ~ (all_0_111_111 = e11) % 8.76/2.57 | (108) ~ (e23 = e21) % 8.76/2.57 | (109) all_0_96_96 = e20 | all_0_99_99 = e20 % 8.76/2.57 | (110) ~ (all_0_106_106 = all_0_109_109) % 8.76/2.57 | (111) ~ (all_0_107_107 = e13) % 8.76/2.57 | (112) h2(all_0_107_107) = all_0_48_48 % 8.76/2.57 | (113) all_0_93_93 = e21 | all_0_95_95 = e21 | all_0_98_98 = e21 % 8.76/2.57 | (114) ~ (all_0_96_96 = e23) % 8.76/2.57 | (115) h2(e10) = all_0_88_88 % 8.76/2.57 | (116) all_0_93_93 = e22 | all_0_98_98 = e22 | all_0_101_101 = e22 % 8.76/2.57 | (117) op2(e21, e22) = all_0_96_96 % 8.76/2.57 | (118) ~ (e12 = e10) % 8.76/2.57 | (119) all_0_92_92 = e23 | all_0_93_93 = e23 % 8.76/2.57 | (120) op2(all_0_87_87, all_0_88_88) = all_0_51_51 % 8.76/2.58 | (121) op2(all_0_101_101, all_0_101_101) = all_0_90_90 % 8.76/2.58 | (122) all_0_100_100 = e23 | all_0_100_100 = e22 | all_0_100_100 = e20 % 8.76/2.58 | (123) h1(e12) = e20 % 8.76/2.58 | (124) all_0_112_112 = e13 | all_0_112_112 = e12 | all_0_112_112 = e10 % 8.76/2.58 | (125) op2(e20, e23) = e21 % 8.76/2.58 | (126) h4(all_0_108_108) = all_0_13_13 % 8.76/2.58 | (127) h1(all_0_110_110) = all_0_81_81 % 8.76/2.58 | (128) op2(all_0_90_90, all_0_101_101) = all_0_79_79 % 8.76/2.58 | (129) ~ (all_0_98_98 = e23) % 8.76/2.58 | (130) all_0_96_96 = e21 | all_0_99_99 = e20 % 8.76/2.58 | (131) ~ (e21 = e10) % 8.76/2.58 | (132) ~ (all_0_91_91 = all_0_92_92) % 8.76/2.58 | (133) ~ (all_0_97_97 = e23) % 8.76/2.58 | (134) ~ (e21 = e20) % 8.76/2.58 | (135) ~ (all_0_100_100 = all_0_101_101) % 8.76/2.58 | (136) ~ (all_0_102_102 = e10) % 8.76/2.58 | (137) all_0_93_93 = e23 | (all_0_98_98 = e21 & ~ (all_0_100_100 = e20)) % 8.76/2.58 | (138) all_0_104_104 = e11 | all_0_106_106 = e11 | all_0_109_109 = e11 % 8.76/2.58 | (139) h1(e11) = all_0_89_89 % 8.76/2.58 | (140) h1(all_0_108_108) = all_0_76_76 % 8.76/2.58 | (141) all_0_96_96 = e22 | all_0_96_96 = e21 | all_0_96_96 = e20 % 8.76/2.58 | (142) all_0_102_102 = e12 | all_0_107_107 = e12 | all_0_110_110 = e12 % 8.76/2.58 | (143) op2(e22, e21) = all_0_94_94 % 8.76/2.58 | (144) ~ (all_0_92_92 = all_0_97_97) % 8.76/2.58 | (145) all_0_107_107 = e11 | all_0_108_108 = e11 | all_0_109_109 = e11 % 8.76/2.58 | (146) ~ (all_0_108_108 = all_0_111_111) % 8.76/2.58 | (147) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h1(v2) = v1) | ~ (h1(v2) = v0)) % 8.76/2.58 | (148) ~ (all_0_94_94 = e23) % 8.76/2.58 | (149) ~ (all_0_100_100 = e21) % 8.76/2.58 | (150) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h3(v2) = v1) | ~ (h3(v2) = v0)) % 8.76/2.58 | (151) h1(all_0_105_105) = all_0_69_69 % 8.76/2.58 | (152) op2(e20, e20) = all_0_101_101 % 8.76/2.58 | (153) op1(e13, e13) = e10 % 8.76/2.58 | (154) ~ (e20 = e12) % 8.76/2.58 | (155) h4(e10) = all_0_101_101 % 8.76/2.58 | (156) h2(all_0_108_108) = all_0_50_50 % 8.76/2.58 | (157) ~ (all_0_107_107 = all_0_108_108) % 8.76/2.58 | (158) op2(e21, all_0_88_88) = all_0_44_44 % 8.76/2.58 | (159) op2(all_0_88_88, all_0_87_87) = all_0_56_56 % 8.76/2.58 | (160) op2(e22, e20) = all_0_95_95 % 8.76/2.58 | (161) all_0_96_96 = e20 | all_0_97_97 = e20 | all_0_98_98 = e20 % 8.76/2.58 | (162) op1(e12, e10) = all_0_106_106 % 8.76/2.58 | (163) h3(all_0_103_103) = all_0_24_24 % 8.76/2.58 | (164) ~ (e23 = e22) % 8.76/2.58 | (165) op2(all_0_101_101, all_0_101_101) = all_0_21_21 % 8.76/2.58 | (166) all_0_101_101 = e23 | all_0_101_101 = e22 | all_0_101_101 = e20 % 8.76/2.58 | (167) ~ (all_0_34_34 = all_0_88_88) | ~ (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 = e21) | ~ (all_0_42_42 = all_0_43_43) | ~ (all_0_44_44 = all_0_45_45) | ~ (all_0_46_46 = all_0_97_97) | ~ (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_87_87) | ~ (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_87_87 = e23) & ~ (all_0_88_88 = e23)) | ( ~ (all_0_87_87 = e22) & ~ (all_0_88_88 = e22) & ~ (all_0_97_97 = e22)) | ( ~ (all_0_87_87 = e20) & ~ (all_0_88_88 = e20) & ~ (all_0_97_97 = e20)) % 8.76/2.58 | (168) op2(e23, e20) = all_0_93_93 % 8.76/2.58 | (169) op1(e10, e12) = all_0_110_110 % 8.76/2.58 | (170) h2(all_0_106_106) = all_0_45_45 % 8.76/2.58 | (171) all_0_94_94 = e20 | all_0_95_95 = e20 % 8.76/2.58 | (172) all_0_103_103 = e13 | all_0_111_111 = e13 % 8.76/2.58 | (173) all_0_92_92 = e23 | (all_0_100_100 = e20 & ~ (all_0_98_98 = e21)) % 8.76/2.58 | (174) ~ (e22 = e10) % 8.76/2.58 | (175) h3(all_0_102_102) = all_0_23_23 % 8.76/2.58 | (176) all_0_99_99 = e22 | all_0_100_100 = e22 | all_0_101_101 = e22 % 8.76/2.58 | (177) ~ (all_0_93_93 = all_0_101_101) % 8.76/2.58 | (178) ~ (all_0_97_97 = all_0_98_98) % 8.76/2.58 | (179) all_0_111_111 = e13 | all_0_112_112 = e13 % 8.76/2.58 | (180) ~ (all_0_91_91 = all_0_96_96) % 8.76/2.58 | (181) h4(e11) = all_0_86_86 % 8.76/2.58 | (182) all_0_92_92 = e23 | all_0_92_92 = e22 | all_0_92_92 = e21 % 8.76/2.58 | (183) op2(all_0_97_97, all_0_97_97) = all_0_34_34 % 8.76/2.58 | (184) all_0_99_99 = e22 | all_0_99_99 = e20 % 8.76/2.58 | (185) h3(all_0_111_111) = all_0_32_32 % 8.76/2.58 | (186) ~ (all_0_92_92 = all_0_93_93) % 8.76/2.58 | (187) all_0_91_91 = e22 | all_0_92_92 = e22 | all_0_93_93 = e22 % 8.76/2.58 | (188) all_0_94_94 = e20 | all_0_97_97 = e20 | all_0_100_100 = e20 % 8.76/2.58 | (189) ~ (all_0_109_109 = all_0_112_112) % 8.76/2.58 | (190) op2(all_0_88_88, all_0_97_97) = all_0_53_53 % 8.76/2.58 | (191) op2(all_0_101_101, e20) = all_0_16_16 % 8.76/2.58 | (192) ~ (all_0_106_106 = e12) % 8.76/2.58 | (193) op2(all_0_101_101, e20) = all_0_61_61 % 8.76/2.58 | (194) h4(e13) = e20 % 8.76/2.58 | (195) all_0_91_91 = e22 | all_0_96_96 = e22 | all_0_99_99 = e22 % 8.76/2.58 | (196) ~ (e23 = e12) % 8.76/2.58 | (197) op1(e10, e11) = all_0_111_111 % 8.76/2.58 | (198) ~ (all_0_110_110 = all_0_111_111) % 8.76/2.58 | (199) h2(all_0_112_112) = all_0_59_59 % 8.76/2.58 | (200) h3(e13) = e23 % 8.76/2.58 | (201) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op2(v3, v2) = v1) | ~ (op2(v3, v2) = v0)) % 8.76/2.58 | (202) ~ (all_0_93_93 = all_0_98_98) % 8.76/2.58 | (203) op1(e11, e12) = all_0_107_107 % 8.76/2.58 | (204) ~ (e23 = e20) % 8.76/2.58 | (205) op2(all_0_97_97, all_0_97_97) = all_0_88_88 % 8.76/2.58 | (206) op2(e20, all_0_101_101) = all_0_67_67 % 8.76/2.58 | (207) ~ (e22 = e20) % 8.76/2.58 | (208) ~ (all_0_94_94 = all_0_100_100) % 8.76/2.58 | (209) ~ (all_0_92_92 = all_0_100_100) % 8.76/2.58 | (210) h1(e13) = all_0_101_101 % 8.76/2.58 | (211) ~ (all_0_105_105 = all_0_111_111) % 8.76/2.58 | (212) h3(all_0_110_110) = all_0_31_31 % 8.76/2.58 | (213) h3(all_0_107_107) = all_0_28_28 % 8.76/2.58 | (214) h2(e11) = all_0_87_87 % 8.76/2.58 | (215) h2(all_0_104_104) = all_0_40_40 % 8.76/2.58 | (216) ~ (all_0_101_101 = e21) % 8.76/2.58 | (217) ~ (all_0_99_99 = all_0_100_100) % 8.76/2.58 | (218) ~ (all_0_110_110 = e13) % 8.76/2.58 | (219) ~ (e11 = e10) % 8.76/2.58 | (220) op2(all_0_89_89, e20) = all_0_73_73 % 8.76/2.58 | (221) op2(all_0_88_88, all_0_97_97) = all_0_87_87 % 8.76/2.58 | (222) ~ (all_0_102_102 = e13) % 8.76/2.58 | (223) ~ (e21 = e12) % 8.76/2.58 | (224) h3(all_0_108_108) = all_0_29_29 % 8.76/2.58 | (225) all_0_104_104 = e13 | (all_0_109_109 = e11 & ~ (all_0_111_111 = e10)) % 8.76/2.58 | (226) ~ (all_0_107_107 = all_0_110_110) % 8.76/2.58 | (227) h1(e10) = all_0_90_90 % 8.76/2.58 | (228) h4(all_0_107_107) = all_0_11_11 % 8.76/2.59 | (229) all_0_103_103 = e13 | (all_0_111_111 = e10 & ~ (all_0_109_109 = e11)) % 8.76/2.59 | (230) op2(e20, all_0_86_86) = all_0_1_1 % 8.76/2.59 | (231) op2(all_0_89_89, all_0_101_101) = all_0_72_72 % 8.76/2.59 | (232) h4(all_0_109_109) = all_0_15_15 % 8.76/2.59 | (233) ~ (all_0_94_94 = all_0_95_95) % 8.76/2.59 | (234) all_0_91_91 = e22 | all_0_91_91 = e21 % 8.76/2.59 | (235) ~ (all_0_105_105 = all_0_106_106) % 8.76/2.59 | (236) ~ (all_0_102_102 = all_0_110_110) % 8.76/2.59 | (237) ~ (e22 = e11) % 8.76/2.59 | (238) ~ (e20 = e10) % 8.76/2.59 | (239) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op1(v3, v2) = v1) | ~ (op1(v3, v2) = v0)) % 8.76/2.59 | (240) op2(all_0_97_97, all_0_87_87) = all_0_37_37 % 8.76/2.59 | (241) ~ (all_0_99_99 = e23) % 8.76/2.59 | (242) all_0_106_106 = e10 | all_0_109_109 = e10 | all_0_112_112 = e10 % 8.76/2.59 | (243) ~ (all_0_103_103 = all_0_104_104) % 8.76/2.59 | (244) h3(e10) = e20 % 8.76/2.59 | (245) op2(e23, e21) = all_0_92_92 % 8.76/2.59 | (246) h4(all_0_103_103) = all_0_2_2 % 8.76/2.59 | (247) op2(all_0_90_90, all_0_101_101) = all_0_89_89 % 8.76/2.59 | (248) ~ (all_0_108_108 = e13) % 8.76/2.59 | (249) ~ (all_0_104_104 = all_0_106_106) % 8.76/2.59 | (250) op2(all_0_87_87, all_0_97_97) = all_0_46_46 % 8.76/2.59 | (251) op2(all_0_88_88, all_0_88_88) = all_0_58_58 % 8.76/2.59 | (252) ~ (all_0_95_95 = all_0_101_101) % 8.76/2.59 | (253) ~ (all_0_96_96 = all_0_99_99) % 8.76/2.59 | (254) ~ (all_0_110_110 = e11) % 8.76/2.59 | (255) all_0_92_92 = e23 | all_0_100_100 = e23 % 8.76/2.59 | (256) ~ (all_0_105_105 = e12) % 8.76/2.59 | (257) all_0_107_107 = e10 | all_0_110_110 = e10 % 8.76/2.59 | (258) op1(e10, e10) = all_0_112_112 % 8.76/2.59 | (259) ~ (all_0_108_108 = all_0_109_109) % 8.76/2.59 | (260) all_0_102_102 = e12 | all_0_103_103 = e12 | all_0_104_104 = e12 % 8.76/2.59 | (261) all_0_107_107 = e12 | all_0_107_107 = e11 | all_0_107_107 = e10 % 8.76/2.59 | (262) ~ (all_0_110_110 = all_0_112_112) % 8.76/2.59 | (263) all_0_104_104 = e13 | all_0_104_104 = e12 | all_0_104_104 = e11 % 8.76/2.59 | (264) op2(all_0_101_101, e23) = all_0_17_17 % 8.76/2.59 | (265) h3(all_0_112_112) = all_0_33_33 % 8.76/2.59 | (266) all_0_92_92 = e22 | all_0_97_97 = e22 | all_0_100_100 = e22 % 8.76/2.59 | (267) op1(e11, e10) = all_0_109_109 % 8.76/2.59 | (268) all_0_93_93 = e23 | all_0_93_93 = e22 | all_0_93_93 = e21 % 8.76/2.59 | (269) all_0_106_106 = e11 | all_0_106_106 = e10 % 8.76/2.59 | (270) ~ (e13 = e12) % 8.76/2.59 | (271) h4(all_0_104_104) = all_0_4_4 % 8.76/2.59 | (272) ~ (e22 = e21) % 8.76/2.59 | (273) all_0_111_111 = e13 | all_0_111_111 = e12 | all_0_111_111 = e10 % 8.76/2.59 | (274) op2(e23, e23) = e20 % 8.76/2.59 | (275) op2(all_0_90_90, all_0_89_89) = all_0_82_82 % 8.76/2.59 | (276) ~ (all_0_111_111 = all_0_112_112) % 8.76/2.59 | (277) h2(all_0_110_110) = all_0_55_55 % 8.76/2.59 | (278) ~ (all_0_96_96 = all_0_98_98) % 8.76/2.59 | (279) h1(all_0_111_111) = all_0_83_83 % 8.76/2.59 | (280) ~ (e22 = e12) % 8.76/2.59 | (281) ~ (e20 = e13) % 8.76/2.59 | (282) all_0_110_110 = e12 | all_0_110_110 = e10 % 8.76/2.59 | (283) ~ (all_0_112_112 = e11) % 8.76/2.59 | (284) ~ (all_0_104_104 = all_0_112_112) % 8.76/2.59 | (285) h1(all_0_107_107) = all_0_74_74 % 8.76/2.59 | (286) op1(e11, e11) = all_0_108_108 % 8.76/2.59 | (287) h3(all_0_104_104) = all_0_25_25 % 8.76/2.59 | (288) all_0_103_103 = e12 | all_0_108_108 = e12 | all_0_111_111 = e12 % 8.76/2.59 | (289) ~ (e23 = e11) % 8.76/2.59 | (290) h4(e12) = e23 % 8.76/2.59 | (291) op2(all_0_101_101, all_0_86_86) = all_0_19_19 % 8.76/2.59 | (292) all_0_93_93 = e23 | all_0_101_101 = e23 % 8.76/2.59 | (293) op2(e23, all_0_86_86) = all_0_5_5 % 8.76/2.59 | (294) op2(e20, e21) = all_0_100_100 % 8.76/2.59 | (295) ~ (all_0_106_106 = e13) % 8.76/2.59 | (296) op2(e22, e22) = e23 % 8.76/2.59 | (297) op1(e10, e13) = e11 % 8.76/2.59 | (298) ~ (all_0_95_95 = all_0_98_98) % 8.76/2.59 | (299) all_0_103_103 = e11 | all_0_105_105 = e11 | all_0_108_108 = e11 % 8.76/2.59 | (300) ~ (all_0_91_91 = e20) % 8.76/2.59 | (301) h2(all_0_111_111) = all_0_57_57 % 8.76/2.59 | (302) ~ (all_0_93_93 = all_0_95_95) % 8.76/2.59 | (303) all_0_94_94 = e21 | all_0_95_95 = e21 % 8.76/2.59 | (304) ~ (all_0_91_91 = e23) % 8.76/2.59 | (305) op2(e20, all_0_89_89) = all_0_68_68 % 8.76/2.59 | (306) ~ (all_0_103_103 = all_0_108_108) % 8.76/2.59 | (307) ~ (all_0_102_102 = all_0_104_104) % 8.76/2.59 | (308) op2(all_0_86_86, e23) = all_0_10_10 % 8.76/2.59 | (309) op2(e21, all_0_87_87) = all_0_42_42 % 8.76/2.59 | (310) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h4(v2) = v1) | ~ (h4(v2) = v0)) % 8.76/2.59 | (311) all_0_107_107 = e10 | all_0_108_108 = e10 | all_0_109_109 = e10 % 8.76/2.59 | (312) ~ (all_0_91_91 = all_0_93_93) % 8.76/2.59 | (313) h4(all_0_110_110) = all_0_18_18 % 8.76/2.59 | (314) op2(all_0_90_90, e20) = all_0_80_80 % 8.76/2.59 | (315) all_0_103_103 = e13 | all_0_103_103 = e12 | all_0_103_103 = e11 % 8.76/2.59 | (316) op2(all_0_87_87, e21) = all_0_47_47 % 8.76/2.59 | (317) all_0_105_105 = e11 | all_0_105_105 = e10 % 9.23/2.59 | (318) all_0_91_91 = e21 | all_0_92_92 = e21 | all_0_93_93 = e21 % 9.23/2.59 | (319) h3(all_0_106_106) = all_0_27_27 % 9.23/2.59 | (320) op1(e12, e11) = all_0_105_105 % 9.23/2.59 | (321) ~ (all_0_94_94 = e22) % 9.23/2.59 | (322) ~ (all_0_99_99 = e21) % 9.23/2.59 | (323) op2(e21, all_0_97_97) = all_0_41_41 % 9.23/2.59 | (324) all_0_104_104 = e13 | all_0_112_112 = e13 % 9.23/2.59 | (325) op1(e12, e13) = e12 % 9.23/2.59 | (326) op2(all_0_87_87, all_0_87_87) = all_0_49_49 % 9.23/2.59 | (327) op1(e11, e13) = e13 % 9.23/2.59 | (328) ~ (e13 = e11) % 9.23/2.59 | (329) h1(all_0_109_109) = all_0_78_78 % 9.23/2.59 | (330) all_0_107_107 = e11 | all_0_110_110 = e10 % 9.23/2.59 | % 9.23/2.59 +-Applying beta-rule and splitting (184), into two cases. % 9.23/2.59 |-Branch one: % 9.23/2.59 | (331) all_0_99_99 = e20 % 9.23/2.59 | % 9.23/2.60 | Equations (331) can reduce 32 to: % 9.23/2.60 | (300) ~ (all_0_91_91 = e20) % 9.23/2.60 | % 9.23/2.60 | Equations (331) can reduce 253 to: % 9.23/2.60 | (333) ~ (all_0_96_96 = e20) % 9.23/2.60 | % 9.23/2.60 | Equations (331) can reduce 217 to: % 9.23/2.60 | (334) ~ (all_0_100_100 = e20) % 9.23/2.60 | % 9.23/2.60 | Simplifying 334 yields: % 9.23/2.60 | (335) ~ (all_0_100_100 = e20) % 9.23/2.60 | % 9.23/2.60 +-Applying beta-rule and splitting (173), into two cases. % 9.23/2.60 |-Branch one: % 9.23/2.60 | (336) all_0_92_92 = e23 % 9.23/2.60 | % 9.23/2.60 | Equations (336) can reduce 186 to: % 9.23/2.60 | (337) ~ (all_0_93_93 = e23) % 9.23/2.60 | % 9.24/2.60 | Simplifying 337 yields: % 9.24/2.60 | (338) ~ (all_0_93_93 = e23) % 9.24/2.60 | % 9.24/2.60 +-Applying beta-rule and splitting (292), into two cases. % 9.24/2.60 |-Branch one: % 9.24/2.60 | (339) all_0_93_93 = e23 % 9.24/2.60 | % 9.24/2.60 | Equations (339) can reduce 338 to: % 9.24/2.60 | (340) $false % 9.24/2.60 | % 9.24/2.60 |-The branch is then unsatisfiable % 9.24/2.60 |-Branch two: % 9.24/2.60 | (338) ~ (all_0_93_93 = e23) % 9.24/2.60 | (342) all_0_101_101 = e23 % 9.24/2.60 | % 9.24/2.60 | Equations (342) can reduce 177 to: % 9.24/2.60 | (338) ~ (all_0_93_93 = e23) % 9.24/2.60 | % 9.24/2.60 | Equations (342) can reduce 135 to: % 9.24/2.60 | (344) ~ (all_0_100_100 = e23) % 9.24/2.60 | % 9.24/2.60 +-Applying beta-rule and splitting (176), into two cases. % 9.24/2.60 |-Branch one: % 9.24/2.60 | (345) all_0_99_99 = e22 % 9.24/2.60 | % 9.24/2.60 | Combining equations (345,331) yields a new equation: % 9.24/2.60 | (346) e22 = e20 % 9.24/2.60 | % 9.24/2.60 | Simplifying 346 yields: % 9.24/2.60 | (347) e22 = e20 % 9.24/2.60 | % 9.24/2.60 | Equations (347) can reduce 207 to: % 9.24/2.60 | (340) $false % 9.24/2.60 | % 9.24/2.60 |-The branch is then unsatisfiable % 9.24/2.60 |-Branch two: % 9.24/2.60 | (349) ~ (all_0_99_99 = e22) % 9.24/2.60 | (350) all_0_100_100 = e22 | all_0_101_101 = e22 % 9.24/2.60 | % 9.24/2.60 +-Applying beta-rule and splitting (350), into two cases. % 9.24/2.60 |-Branch one: % 9.24/2.60 | (351) all_0_100_100 = e22 % 9.24/2.60 | % 9.24/2.60 | Equations (351) can reduce 208 to: % 9.24/2.60 | (321) ~ (all_0_94_94 = e22) % 9.24/2.60 | % 9.24/2.60 | Equations (351) can reduce 344 to: % 9.24/2.60 | (353) ~ (e23 = e22) % 9.24/2.60 | % 9.24/2.60 | Simplifying 353 yields: % 9.24/2.60 | (164) ~ (e23 = e22) % 9.24/2.60 | % 9.24/2.60 | Equations (351) can reduce 149 to: % 9.24/2.60 | (272) ~ (e22 = e21) % 9.24/2.60 | % 9.24/2.60 +-Applying beta-rule and splitting (137), into two cases. % 9.24/2.60 |-Branch one: % 9.26/2.60 | (339) all_0_93_93 = e23 % 9.26/2.60 | % 9.26/2.60 | Equations (339) can reduce 338 to: % 9.26/2.60 | (340) $false % 9.26/2.60 | % 9.26/2.60 |-The branch is then unsatisfiable % 9.26/2.60 |-Branch two: % 9.26/2.60 | (338) ~ (all_0_93_93 = e23) % 9.26/2.60 | (359) all_0_98_98 = e21 & ~ (all_0_100_100 = e20) % 9.26/2.60 | % 9.26/2.60 | Applying alpha-rule on (359) yields: % 9.26/2.60 | (360) all_0_98_98 = e21 % 9.26/2.60 | (335) ~ (all_0_100_100 = e20) % 9.26/2.60 | % 9.26/2.60 | Equations (360) can reduce 278 to: % 9.26/2.60 | (362) ~ (all_0_96_96 = e21) % 9.26/2.60 | % 9.26/2.60 +-Applying beta-rule and splitting (46), into two cases. % 9.26/2.60 |-Branch one: % 9.26/2.60 | (363) all_0_91_91 = e21 % 9.26/2.60 | % 9.26/2.60 | Equations (363) can reduce 300 to: % 9.26/2.60 | (134) ~ (e21 = e20) % 9.26/2.60 | % 9.26/2.60 +-Applying beta-rule and splitting (187), into two cases. % 9.26/2.60 |-Branch one: % 9.26/2.60 | (365) all_0_91_91 = e22 % 9.26/2.60 | % 9.26/2.60 | Combining equations (365,363) yields a new equation: % 9.26/2.60 | (366) e22 = e21 % 9.26/2.60 | % 9.26/2.60 | Simplifying 366 yields: % 9.26/2.60 | (367) e22 = e21 % 9.26/2.60 | % 9.26/2.60 | Equations (367) can reduce 272 to: % 9.26/2.60 | (340) $false % 9.26/2.60 | % 9.26/2.60 |-The branch is then unsatisfiable % 9.26/2.60 |-Branch two: % 9.26/2.60 | (369) ~ (all_0_91_91 = e22) % 9.26/2.60 | (370) all_0_92_92 = e22 | all_0_93_93 = e22 % 9.26/2.60 | % 9.26/2.60 +-Applying beta-rule and splitting (370), into two cases. % 9.26/2.60 |-Branch one: % 9.26/2.60 | (371) all_0_92_92 = e22 % 9.26/2.60 | % 9.26/2.60 | Combining equations (336,371) yields a new equation: % 9.26/2.60 | (372) e23 = e22 % 9.26/2.60 | % 9.26/2.60 | Simplifying 372 yields: % 9.26/2.60 | (373) e23 = e22 % 9.26/2.60 | % 9.26/2.60 | Equations (373) can reduce 164 to: % 9.26/2.60 | (340) $false % 9.26/2.60 | % 9.26/2.60 |-The branch is then unsatisfiable % 9.26/2.60 |-Branch two: % 9.26/2.60 | (375) ~ (all_0_92_92 = e22) % 9.26/2.60 | (376) all_0_93_93 = e22 % 9.26/2.60 | % 9.26/2.60 | Equations (376) can reduce 302 to: % 9.26/2.60 | (377) ~ (all_0_95_95 = e22) % 9.26/2.60 | % 9.26/2.60 | Simplifying 377 yields: % 9.26/2.60 | (27) ~ (all_0_95_95 = e22) % 9.26/2.60 | % 9.26/2.60 +-Applying beta-rule and splitting (161), into two cases. % 9.26/2.60 |-Branch one: % 9.26/2.60 | (379) all_0_96_96 = e20 % 9.26/2.60 | % 9.26/2.60 | Equations (379) can reduce 333 to: % 9.26/2.60 | (340) $false % 9.26/2.60 | % 9.26/2.60 |-The branch is then unsatisfiable % 9.26/2.60 |-Branch two: % 9.26/2.60 | (333) ~ (all_0_96_96 = e20) % 9.26/2.60 | (382) all_0_97_97 = e20 | all_0_98_98 = e20 % 9.26/2.60 | % 9.26/2.60 +-Applying beta-rule and splitting (382), into two cases. % 9.26/2.60 |-Branch one: % 9.26/2.60 | (383) all_0_97_97 = e20 % 9.26/2.60 | % 9.26/2.60 | Equations (383) can reduce 12 to: % 9.26/2.60 | (384) ~ (all_0_94_94 = e20) % 9.26/2.60 | % 9.26/2.60 +-Applying beta-rule and splitting (16), into two cases. % 9.26/2.60 |-Branch one: % 9.26/2.60 | (385) all_0_94_94 = e20 % 9.26/2.60 | % 9.26/2.60 | Equations (385) can reduce 384 to: % 9.26/2.60 | (340) $false % 9.26/2.60 | % 9.26/2.60 |-The branch is then unsatisfiable % 9.26/2.60 |-Branch two: % 9.26/2.60 | (384) ~ (all_0_94_94 = e20) % 9.26/2.60 | (388) all_0_94_94 = e21 % 9.26/2.60 | % 9.26/2.60 | Equations (388) can reduce 321 to: % 9.26/2.60 | (389) ~ (e22 = e21) % 9.26/2.60 | % 9.26/2.60 | Simplifying 389 yields: % 9.26/2.60 | (272) ~ (e22 = e21) % 9.26/2.60 | % 9.26/2.60 | Equations (388) can reduce 384 to: % 9.26/2.60 | (134) ~ (e21 = e20) % 9.26/2.60 | % 9.26/2.60 +-Applying beta-rule and splitting (171), into two cases. % 9.26/2.60 |-Branch one: % 9.26/2.60 | (385) all_0_94_94 = e20 % 9.26/2.60 | % 9.26/2.60 | Combining equations (388,385) yields a new equation: % 9.26/2.60 | (393) e21 = e20 % 9.26/2.60 | % 9.26/2.60 | Simplifying 393 yields: % 9.26/2.60 | (394) e21 = e20 % 9.26/2.60 | % 9.26/2.60 | Equations (394) can reduce 134 to: % 9.26/2.60 | (340) $false % 9.26/2.60 | % 9.26/2.60 |-The branch is then unsatisfiable % 9.26/2.60 |-Branch two: % 9.26/2.60 | (384) ~ (all_0_94_94 = e20) % 9.26/2.60 | (397) all_0_95_95 = e20 % 9.26/2.60 | % 9.26/2.60 | Equations (397) can reduce 27 to: % 9.26/2.60 | (398) ~ (e22 = e20) % 9.26/2.60 | % 9.26/2.60 | Simplifying 398 yields: % 9.26/2.60 | (207) ~ (e22 = e20) % 9.26/2.60 | % 9.26/2.60 +-Applying beta-rule and splitting (195), into two cases. % 9.26/2.60 |-Branch one: % 9.26/2.60 | (365) all_0_91_91 = e22 % 9.26/2.61 | % 9.26/2.61 | Combining equations (363,365) yields a new equation: % 9.26/2.61 | (367) e22 = e21 % 9.26/2.61 | % 9.26/2.61 | Equations (367) can reduce 272 to: % 9.26/2.61 | (340) $false % 9.26/2.61 | % 9.26/2.61 |-The branch is then unsatisfiable % 9.26/2.61 |-Branch two: % 9.26/2.61 | (369) ~ (all_0_91_91 = e22) % 9.26/2.61 | (404) all_0_96_96 = e22 | all_0_99_99 = e22 % 9.26/2.61 | % 9.26/2.61 +-Applying beta-rule and splitting (404), into two cases. % 9.26/2.61 |-Branch one: % 9.26/2.61 | (405) all_0_96_96 = e22 % 9.26/2.61 | % 9.26/2.61 +-Applying beta-rule and splitting (330), into two cases. % 9.26/2.61 |-Branch one: % 9.26/2.61 | (406) all_0_107_107 = e11 % 9.26/2.61 | % 9.26/2.61 | Equations (406) can reduce 37 to: % 9.26/2.61 | (407) ~ (all_0_102_102 = e11) % 9.26/2.61 | % 9.26/2.61 | Equations (406) can reduce 85 to: % 9.26/2.61 | (408) ~ (all_0_109_109 = e11) % 9.26/2.61 | % 9.26/2.61 | Simplifying 408 yields: % 9.26/2.61 | (409) ~ (all_0_109_109 = e11) % 9.26/2.61 | % 9.26/2.61 | Equations (406) can reduce 111 to: % 9.26/2.61 | (410) ~ (e13 = e11) % 9.26/2.61 | % 9.26/2.61 | Simplifying 410 yields: % 9.26/2.61 | (328) ~ (e13 = e11) % 9.26/2.61 | % 9.26/2.61 +-Applying beta-rule and splitting (225), into two cases. % 9.26/2.61 |-Branch one: % 9.26/2.61 | (412) all_0_104_104 = e13 % 9.26/2.61 | % 9.26/2.61 | Equations (412) can reduce 243 to: % 9.26/2.61 | (413) ~ (all_0_103_103 = e13) % 9.26/2.61 | % 9.26/2.61 +-Applying beta-rule and splitting (91), into two cases. % 9.26/2.61 |-Branch one: % 9.26/2.61 | (414) all_0_102_102 = e11 % 9.26/2.61 | % 9.26/2.61 | Equations (414) can reduce 407 to: % 9.26/2.61 | (340) $false % 9.26/2.61 | % 9.26/2.61 |-The branch is then unsatisfiable % 9.26/2.61 |-Branch two: % 9.26/2.61 | (407) ~ (all_0_102_102 = e11) % 9.26/2.61 | (417) all_0_103_103 = e11 | all_0_104_104 = e11 % 9.26/2.61 | % 9.26/2.61 +-Applying beta-rule and splitting (417), into two cases. % 9.26/2.61 |-Branch one: % 9.26/2.61 | (418) all_0_103_103 = e11 % 9.26/2.61 | % 9.26/2.61 | Equations (418) can reduce 88 to: % 9.26/2.61 | (419) ~ (all_0_105_105 = e11) % 9.26/2.61 | % 9.26/2.61 | Simplifying 419 yields: % 9.26/2.61 | (420) ~ (all_0_105_105 = e11) % 9.26/2.61 | % 9.26/2.61 | Equations (418) can reduce 413 to: % 9.26/2.61 | (410) ~ (e13 = e11) % 9.26/2.61 | % 9.26/2.61 | Simplifying 410 yields: % 9.26/2.61 | (328) ~ (e13 = e11) % 9.26/2.61 | % 9.26/2.61 +-Applying beta-rule and splitting (317), into two cases. % 9.26/2.61 |-Branch one: % 9.26/2.61 | (423) all_0_105_105 = e11 % 9.26/2.61 | % 9.26/2.61 | Equations (423) can reduce 420 to: % 9.26/2.61 | (340) $false % 9.26/2.61 | % 9.26/2.61 |-The branch is then unsatisfiable % 9.26/2.61 |-Branch two: % 9.26/2.61 | (420) ~ (all_0_105_105 = e11) % 9.26/2.61 | (426) all_0_105_105 = e10 % 9.26/2.61 | % 9.26/2.61 | Equations (426) can reduce 211 to: % 9.26/2.61 | (427) ~ (all_0_111_111 = e10) % 9.26/2.61 | % 9.26/2.61 | Simplifying 427 yields: % 9.26/2.61 | (428) ~ (all_0_111_111 = e10) % 9.26/2.61 | % 9.26/2.61 +-Applying beta-rule and splitting (229), into two cases. % 9.26/2.61 |-Branch one: % 9.26/2.61 | (429) all_0_103_103 = e13 % 9.26/2.61 | % 9.26/2.61 | Combining equations (418,429) yields a new equation: % 9.26/2.61 | (430) e13 = e11 % 9.26/2.61 | % 9.26/2.61 | Equations (430) can reduce 328 to: % 9.26/2.61 | (340) $false % 9.26/2.61 | % 9.26/2.61 |-The branch is then unsatisfiable % 9.26/2.61 |-Branch two: % 9.26/2.61 | (413) ~ (all_0_103_103 = e13) % 9.26/2.61 | (433) all_0_111_111 = e10 & ~ (all_0_109_109 = e11) % 9.26/2.61 | % 9.26/2.61 | Applying alpha-rule on (433) yields: % 9.26/2.61 | (434) all_0_111_111 = e10 % 9.26/2.61 | (409) ~ (all_0_109_109 = e11) % 9.26/2.61 | % 9.26/2.61 | Equations (434) can reduce 428 to: % 9.26/2.61 | (340) $false % 9.26/2.61 | % 9.26/2.61 |-The branch is then unsatisfiable % 9.26/2.61 |-Branch two: % 9.26/2.61 | (437) ~ (all_0_103_103 = e11) % 9.26/2.61 | (438) all_0_104_104 = e11 % 9.26/2.61 | % 9.26/2.61 | Combining equations (412,438) yields a new equation: % 9.26/2.61 | (439) e13 = e11 % 9.26/2.61 | % 9.26/2.61 | Simplifying 439 yields: % 9.26/2.61 | (430) e13 = e11 % 9.26/2.61 | % 9.26/2.61 | Equations (430) can reduce 328 to: % 9.26/2.61 | (340) $false % 9.26/2.61 | % 9.26/2.61 |-The branch is then unsatisfiable % 9.26/2.61 |-Branch two: % 9.26/2.61 | (442) ~ (all_0_104_104 = e13) % 9.26/2.61 | (443) all_0_109_109 = e11 & ~ (all_0_111_111 = e10) % 9.26/2.61 | % 9.26/2.61 | Applying alpha-rule on (443) yields: % 9.26/2.61 | (444) all_0_109_109 = e11 % 9.26/2.61 | (428) ~ (all_0_111_111 = e10) % 9.26/2.61 | % 9.26/2.61 | Equations (444) can reduce 409 to: % 9.26/2.61 | (340) $false % 9.26/2.61 | % 9.26/2.61 |-The branch is then unsatisfiable % 9.26/2.61 |-Branch two: % 9.26/2.61 | (447) ~ (all_0_107_107 = e11) % 9.26/2.61 | (448) all_0_110_110 = e10 % 9.26/2.61 | % 9.26/2.61 | Equations (448) can reduce 236 to: % 9.26/2.61 | (136) ~ (all_0_102_102 = e10) % 9.26/2.61 | % 9.26/2.61 | Equations (448) can reduce 226 to: % 9.26/2.61 | (450) ~ (all_0_107_107 = e10) % 9.26/2.61 | % 9.26/2.61 | Equations (448) can reduce 198 to: % 9.26/2.61 | (427) ~ (all_0_111_111 = e10) % 9.26/2.61 | % 9.26/2.61 | Simplifying 427 yields: % 9.26/2.61 | (428) ~ (all_0_111_111 = e10) % 9.26/2.61 | % 9.26/2.61 | From (448) and (212) follows: % 9.26/2.61 | (453) h3(e10) = all_0_31_31 % 9.26/2.61 | % 9.26/2.61 +-Applying beta-rule and splitting (261), into two cases. % 9.26/2.61 |-Branch one: % 9.26/2.61 | (406) all_0_107_107 = e11 % 9.26/2.61 | % 9.26/2.61 | Equations (406) can reduce 447 to: % 9.26/2.61 | (340) $false % 9.26/2.61 | % 9.26/2.61 |-The branch is then unsatisfiable % 9.26/2.61 |-Branch two: % 9.26/2.61 | (447) ~ (all_0_107_107 = e11) % 9.26/2.61 | (457) all_0_107_107 = e12 | all_0_107_107 = e10 % 9.26/2.61 | % 9.26/2.61 +-Applying beta-rule and splitting (457), into two cases. % 9.26/2.61 |-Branch one: % 9.26/2.61 | (458) all_0_107_107 = e10 % 9.26/2.61 | % 9.26/2.61 | Equations (458) can reduce 450 to: % 9.26/2.61 | (340) $false % 9.26/2.61 | % 9.26/2.61 |-The branch is then unsatisfiable % 9.26/2.61 |-Branch two: % 9.26/2.61 | (450) ~ (all_0_107_107 = e10) % 9.26/2.61 | (461) all_0_107_107 = e12 % 9.26/2.61 | % 9.26/2.61 | Equations (461) can reduce 157 to: % 9.26/2.61 | (462) ~ (all_0_108_108 = e12) % 9.26/2.61 | % 9.26/2.61 | Simplifying 462 yields: % 9.26/2.61 | (463) ~ (all_0_108_108 = e12) % 9.26/2.61 | % 9.26/2.61 | Equations (461) can reduce 111 to: % 9.26/2.61 | (464) ~ (e13 = e12) % 9.26/2.61 | % 9.26/2.61 | Simplifying 464 yields: % 9.26/2.61 | (270) ~ (e13 = e12) % 9.26/2.61 | % 9.26/2.61 | Equations (461) can reduce 447 to: % 9.26/2.61 | (58) ~ (e12 = e11) % 9.26/2.61 | % 9.26/2.61 | From (461) and (213) follows: % 9.26/2.61 | (467) h3(e12) = all_0_28_28 % 9.26/2.61 | % 9.26/2.61 +-Applying beta-rule and splitting (9), into two cases. % 9.26/2.61 |-Branch one: % 9.26/2.61 | (414) all_0_102_102 = e11 % 9.26/2.61 | % 9.26/2.61 | Equations (414) can reduce 136 to: % 9.26/2.61 | (219) ~ (e11 = e10) % 9.26/2.61 | % 9.26/2.61 | From (414) and (175) follows: % 9.26/2.61 | (470) h3(e11) = all_0_23_23 % 9.26/2.61 | % 9.26/2.61 +-Applying beta-rule and splitting (229), into two cases. % 9.26/2.61 |-Branch one: % 9.26/2.61 | (429) all_0_103_103 = e13 % 9.26/2.61 | % 9.26/2.61 | Equations (429) can reduce 243 to: % 9.26/2.61 | (472) ~ (all_0_104_104 = e13) % 9.26/2.61 | % 9.26/2.61 | Simplifying 472 yields: % 9.26/2.61 | (442) ~ (all_0_104_104 = e13) % 9.26/2.61 | % 9.26/2.61 | From (429) and (163) follows: % 9.26/2.61 | (474) h3(e13) = all_0_24_24 % 9.26/2.62 | % 9.26/2.62 +-Applying beta-rule and splitting (225), into two cases. % 9.26/2.62 |-Branch one: % 9.26/2.62 | (412) all_0_104_104 = e13 % 9.26/2.62 | % 9.26/2.62 | Equations (412) can reduce 442 to: % 9.26/2.62 | (340) $false % 9.26/2.62 | % 9.26/2.62 |-The branch is then unsatisfiable % 9.26/2.62 |-Branch two: % 9.26/2.62 | (442) ~ (all_0_104_104 = e13) % 9.26/2.62 | (443) all_0_109_109 = e11 & ~ (all_0_111_111 = e10) % 9.26/2.62 | % 9.26/2.62 | Applying alpha-rule on (443) yields: % 9.26/2.62 | (444) all_0_109_109 = e11 % 9.26/2.62 | (428) ~ (all_0_111_111 = e10) % 9.26/2.62 | % 9.26/2.62 | Equations (444) can reduce 110 to: % 9.26/2.62 | (481) ~ (all_0_106_106 = e11) % 9.26/2.62 | % 9.26/2.62 | From (444) and (26) follows: % 9.26/2.62 | (482) h3(e11) = all_0_30_30 % 9.26/2.62 | % 9.26/2.62 +-Applying beta-rule and splitting (22), into two cases. % 9.26/2.62 |-Branch one: % 9.26/2.62 | (423) all_0_105_105 = e11 % 9.26/2.62 | % 9.26/2.62 | Equations (423) can reduce 95 to: % 9.26/2.62 | (484) ~ (all_0_108_108 = e11) % 9.26/2.62 | % 9.26/2.62 | Simplifying 484 yields: % 9.26/2.62 | (485) ~ (all_0_108_108 = e11) % 9.26/2.62 | % 9.26/2.62 | Equations (423) can reduce 211 to: % 9.26/2.62 | (486) ~ (all_0_111_111 = e11) % 9.26/2.62 | % 9.26/2.62 | Simplifying 486 yields: % 9.26/2.62 | (107) ~ (all_0_111_111 = e11) % 9.26/2.62 | % 9.26/2.62 | From (423) and (62) follows: % 9.26/2.62 | (488) h3(e11) = all_0_26_26 % 9.26/2.62 | % 9.26/2.62 +-Applying beta-rule and splitting (102), into two cases. % 9.26/2.62 |-Branch one: % 9.26/2.62 | (426) all_0_105_105 = e10 % 9.26/2.62 | % 9.26/2.62 | Combining equations (423,426) yields a new equation: % 9.26/2.62 | (490) e11 = e10 % 9.26/2.62 | % 9.26/2.62 | Simplifying 490 yields: % 9.26/2.62 | (491) e11 = e10 % 9.26/2.62 | % 9.26/2.62 | Equations (491) can reduce 219 to: % 9.26/2.62 | (340) $false % 9.26/2.62 | % 9.26/2.62 |-The branch is then unsatisfiable % 9.26/2.62 |-Branch two: % 9.26/2.62 | (493) ~ (all_0_105_105 = e10) % 9.26/2.62 | (494) all_0_106_106 = e10 % 9.26/2.62 | % 9.26/2.62 | From (494) and (319) follows: % 9.26/2.62 | (495) h3(e10) = all_0_27_27 % 9.26/2.62 | % 9.26/2.62 +-Applying beta-rule and splitting (324), into two cases. % 9.26/2.62 |-Branch one: % 9.26/2.62 | (412) all_0_104_104 = e13 % 9.26/2.62 | % 9.26/2.62 | Equations (412) can reduce 442 to: % 9.26/2.62 | (340) $false % 9.26/2.62 | % 9.26/2.62 |-The branch is then unsatisfiable % 9.26/2.62 |-Branch two: % 9.26/2.62 | (442) ~ (all_0_104_104 = e13) % 9.26/2.62 | (499) all_0_112_112 = e13 % 9.26/2.62 | % 9.26/2.62 | Equations (499) can reduce 276 to: % 9.26/2.62 | (500) ~ (all_0_111_111 = e13) % 9.26/2.62 | % 9.26/2.62 | From (499) and (265) follows: % 9.26/2.62 | (501) h3(e13) = all_0_33_33 % 9.26/2.62 | % 9.26/2.62 +-Applying beta-rule and splitting (68), into two cases. % 9.26/2.62 |-Branch one: % 9.26/2.62 | (502) all_0_108_108 = e11 % 9.26/2.62 | % 9.26/2.62 | Equations (502) can reduce 485 to: % 9.26/2.62 | (340) $false % 9.26/2.62 | % 9.26/2.62 |-The branch is then unsatisfiable % 9.26/2.62 |-Branch two: % 9.26/2.62 | (485) ~ (all_0_108_108 = e11) % 9.26/2.62 | (505) all_0_108_108 = e12 | all_0_108_108 = e10 % 9.26/2.62 | % 9.26/2.62 +-Applying beta-rule and splitting (505), into two cases. % 9.26/2.62 |-Branch one: % 9.26/2.62 | (506) all_0_108_108 = e10 % 9.26/2.62 | % 9.26/2.62 | Equations (506) can reduce 463 to: % 9.26/2.62 | (507) ~ (e12 = e10) % 9.26/2.62 | % 9.26/2.62 | Simplifying 507 yields: % 9.26/2.62 | (118) ~ (e12 = e10) % 9.26/2.62 | % 9.26/2.62 | From (506) and (224) follows: % 9.26/2.62 | (509) h3(e10) = all_0_29_29 % 9.26/2.62 | % 9.26/2.62 +-Applying beta-rule and splitting (101), into two cases. % 9.26/2.62 |-Branch one: % 9.26/2.62 | (510) all_0_110_110 = e12 % 9.26/2.62 | % 9.26/2.62 | Combining equations (448,510) yields a new equation: % 9.26/2.62 | (511) e12 = e10 % 9.26/2.62 | % 9.26/2.62 | Equations (511) can reduce 118 to: % 9.26/2.62 | (340) $false % 9.26/2.62 | % 9.26/2.62 |-The branch is then unsatisfiable % 9.26/2.62 |-Branch two: % 9.26/2.62 | (513) ~ (all_0_110_110 = e12) % 9.26/2.62 | (514) all_0_111_111 = e12 | all_0_112_112 = e12 % 9.26/2.62 | % 9.26/2.62 +-Applying beta-rule and splitting (514), into two cases. % 9.26/2.62 |-Branch one: % 9.26/2.62 | (515) all_0_111_111 = e12 % 9.26/2.62 | % 9.26/2.62 | Equations (515) can reduce 500 to: % 9.26/2.62 | (464) ~ (e13 = e12) % 9.26/2.62 | % 9.26/2.62 | Simplifying 464 yields: % 9.26/2.62 | (270) ~ (e13 = e12) % 9.26/2.62 | % 9.26/2.62 | Equations (515) can reduce 107 to: % 9.26/2.62 | (58) ~ (e12 = e11) % 9.26/2.62 | % 9.26/2.62 | From (515) and (185) follows: % 9.26/2.62 | (519) h3(e12) = all_0_32_32 % 9.26/2.62 | % 9.26/2.62 +-Applying beta-rule and splitting (50), into two cases. % 9.26/2.62 |-Branch one: % 9.26/2.62 | (520) all_0_104_104 = e12 % 9.26/2.62 | % 9.26/2.62 | From (520) and (287) follows: % 9.26/2.62 | (521) h3(e12) = all_0_25_25 % 9.26/2.62 | % 9.26/2.62 | Instantiating formula (150) with e13, all_0_24_24, e23 and discharging atoms h3(e13) = all_0_24_24, h3(e13) = e23, yields: % 9.26/2.62 | (522) all_0_24_24 = e23 % 9.26/2.62 | % 9.26/2.62 | Instantiating formula (150) with e13, all_0_33_33, all_0_24_24 and discharging atoms h3(e13) = all_0_24_24, h3(e13) = all_0_33_33, yields: % 9.26/2.62 | (523) all_0_24_24 = all_0_33_33 % 9.26/2.62 | % 9.26/2.62 | Instantiating formula (150) with e12, all_0_25_25, e22 and discharging atoms h3(e12) = all_0_25_25, h3(e12) = e22, yields: % 9.26/2.62 | (524) all_0_25_25 = e22 % 9.26/2.62 | % 9.26/2.62 | Instantiating formula (150) with e12, all_0_28_28, all_0_25_25 and discharging atoms h3(e12) = all_0_25_25, h3(e12) = all_0_28_28, yields: % 9.26/2.62 | (525) all_0_25_25 = all_0_28_28 % 9.26/2.62 | % 9.26/2.62 | Instantiating formula (150) with e12, all_0_32_32, all_0_25_25 and discharging atoms h3(e12) = all_0_25_25, h3(e12) = all_0_32_32, yields: % 9.26/2.62 | (526) all_0_25_25 = all_0_32_32 % 9.26/2.62 | % 9.26/2.62 | Instantiating formula (150) with e11, all_0_26_26, e21 and discharging atoms h3(e11) = all_0_26_26, h3(e11) = e21, yields: % 9.26/2.62 | (527) all_0_26_26 = e21 % 9.26/2.62 | % 9.26/2.62 | Instantiating formula (150) with e11, all_0_26_26, all_0_23_23 and discharging atoms h3(e11) = all_0_23_23, h3(e11) = all_0_26_26, yields: % 9.26/2.62 | (528) all_0_23_23 = all_0_26_26 % 9.26/2.62 | % 9.26/2.62 | Instantiating formula (150) with e11, all_0_30_30, all_0_23_23 and discharging atoms h3(e11) = all_0_23_23, h3(e11) = all_0_30_30, yields: % 9.26/2.62 | (529) all_0_23_23 = all_0_30_30 % 9.26/2.62 | % 9.26/2.62 | Instantiating formula (150) with e10, all_0_27_27, e20 and discharging atoms h3(e10) = all_0_27_27, h3(e10) = e20, yields: % 9.26/2.62 | (530) all_0_27_27 = e20 % 9.26/2.62 | % 9.26/2.62 | Instantiating formula (150) with e10, all_0_29_29, all_0_27_27 and discharging atoms h3(e10) = all_0_27_27, h3(e10) = all_0_29_29, yields: % 9.26/2.62 | (531) all_0_27_27 = all_0_29_29 % 9.26/2.62 | % 9.26/2.62 | Instantiating formula (150) with e10, all_0_31_31, all_0_27_27 and discharging atoms h3(e10) = all_0_27_27, h3(e10) = all_0_31_31, yields: % 9.26/2.62 | (532) all_0_27_27 = all_0_31_31 % 9.26/2.62 | % 9.26/2.62 | Combining equations (528,529) yields a new equation: % 9.26/2.62 | (533) all_0_26_26 = all_0_30_30 % 9.26/2.62 | % 9.26/2.62 | Simplifying 533 yields: % 9.26/2.62 | (534) all_0_26_26 = all_0_30_30 % 9.26/2.62 | % 9.26/2.62 | Combining equations (523,522) yields a new equation: % 9.26/2.62 | (535) all_0_33_33 = e23 % 9.26/2.62 | % 9.26/2.62 | Simplifying 535 yields: % 9.26/2.62 | (536) all_0_33_33 = e23 % 9.26/2.62 | % 9.26/2.62 | Combining equations (524,525) yields a new equation: % 9.26/2.62 | (537) all_0_28_28 = e22 % 9.26/2.62 | % 9.26/2.62 | Combining equations (526,525) yields a new equation: % 9.26/2.62 | (538) all_0_28_28 = all_0_32_32 % 9.26/2.62 | % 9.26/2.63 | Combining equations (527,534) yields a new equation: % 9.26/2.63 | (539) all_0_30_30 = e21 % 9.26/2.63 | % 9.26/2.63 | Combining equations (530,531) yields a new equation: % 9.26/2.63 | (540) all_0_29_29 = e20 % 9.26/2.63 | % 9.26/2.63 | Combining equations (532,531) yields a new equation: % 9.26/2.63 | (541) all_0_29_29 = all_0_31_31 % 9.26/2.63 | % 9.26/2.63 | Combining equations (538,537) yields a new equation: % 9.26/2.63 | (542) all_0_32_32 = e22 % 9.26/2.63 | % 9.26/2.63 | Simplifying 542 yields: % 9.26/2.63 | (543) all_0_32_32 = e22 % 9.26/2.63 | % 9.26/2.63 | Combining equations (541,540) yields a new equation: % 9.26/2.63 | (544) all_0_31_31 = e20 % 9.26/2.63 | % 9.26/2.63 | Simplifying 544 yields: % 9.26/2.63 | (545) all_0_31_31 = e20 % 9.26/2.63 | % 9.26/2.63 | Combining equations (540,531) yields a new equation: % 9.26/2.63 | (530) all_0_27_27 = e20 % 9.26/2.63 | % 9.26/2.63 | Combining equations (539,534) yields a new equation: % 9.26/2.63 | (527) all_0_26_26 = e21 % 9.26/2.63 | % 9.26/2.63 | Combining equations (537,525) yields a new equation: % 9.26/2.63 | (524) all_0_25_25 = e22 % 9.26/2.63 | % 9.26/2.63 | Combining equations (539,529) yields a new equation: % 9.26/2.63 | (549) all_0_23_23 = e21 % 9.26/2.63 | % 9.26/2.63 +-Applying beta-rule and splitting (98), into two cases. % 9.26/2.63 |-Branch one: % 9.26/2.63 | (550) ~ (all_0_23_23 = all_0_91_91) % 9.26/2.63 | % 9.26/2.63 | Equations (549,363) can reduce 550 to: % 9.26/2.63 | (340) $false % 9.26/2.63 | % 9.26/2.63 |-The branch is then unsatisfiable % 9.26/2.63 |-Branch two: % 9.26/2.63 | (552) all_0_23_23 = all_0_91_91 % 9.26/2.63 | (553) ~ (all_0_24_24 = all_0_92_92) | ~ (all_0_25_25 = all_0_93_93) | ~ (all_0_26_26 = all_0_94_94) | ~ (all_0_27_27 = all_0_95_95) | ~ (all_0_28_28 = all_0_96_96) | ~ (all_0_29_29 = all_0_97_97) | ~ (all_0_30_30 = all_0_98_98) | ~ (all_0_31_31 = all_0_99_99) | ~ (all_0_32_32 = all_0_100_100) | ~ (all_0_33_33 = all_0_101_101) % 9.26/2.63 | % 9.26/2.63 +-Applying beta-rule and splitting (553), into two cases. % 9.26/2.63 |-Branch one: % 9.26/2.63 | (554) ~ (all_0_24_24 = all_0_92_92) % 9.26/2.63 | % 9.26/2.63 | Equations (522,336) can reduce 554 to: % 9.26/2.63 | (340) $false % 9.26/2.63 | % 9.26/2.63 |-The branch is then unsatisfiable % 9.26/2.63 |-Branch two: % 9.26/2.63 | (556) all_0_24_24 = all_0_92_92 % 9.26/2.63 | (557) ~ (all_0_25_25 = all_0_93_93) | ~ (all_0_26_26 = all_0_94_94) | ~ (all_0_27_27 = all_0_95_95) | ~ (all_0_28_28 = all_0_96_96) | ~ (all_0_29_29 = all_0_97_97) | ~ (all_0_30_30 = all_0_98_98) | ~ (all_0_31_31 = all_0_99_99) | ~ (all_0_32_32 = all_0_100_100) | ~ (all_0_33_33 = all_0_101_101) % 9.26/2.63 | % 9.26/2.63 +-Applying beta-rule and splitting (557), into two cases. % 9.26/2.63 |-Branch one: % 9.26/2.63 | (558) ~ (all_0_25_25 = all_0_93_93) % 9.26/2.63 | % 9.26/2.63 | Equations (524,376) can reduce 558 to: % 9.26/2.63 | (340) $false % 9.26/2.63 | % 9.26/2.63 |-The branch is then unsatisfiable % 9.26/2.63 |-Branch two: % 9.26/2.63 | (560) all_0_25_25 = all_0_93_93 % 9.26/2.63 | (561) ~ (all_0_26_26 = all_0_94_94) | ~ (all_0_27_27 = all_0_95_95) | ~ (all_0_28_28 = all_0_96_96) | ~ (all_0_29_29 = all_0_97_97) | ~ (all_0_30_30 = all_0_98_98) | ~ (all_0_31_31 = all_0_99_99) | ~ (all_0_32_32 = all_0_100_100) | ~ (all_0_33_33 = all_0_101_101) % 9.26/2.63 | % 9.26/2.63 +-Applying beta-rule and splitting (561), into two cases. % 9.26/2.63 |-Branch one: % 9.26/2.63 | (562) ~ (all_0_26_26 = all_0_94_94) % 9.26/2.63 | % 9.26/2.63 | Equations (527,388) can reduce 562 to: % 9.26/2.63 | (340) $false % 9.26/2.63 | % 9.26/2.63 |-The branch is then unsatisfiable % 9.26/2.63 |-Branch two: % 9.26/2.63 | (564) all_0_26_26 = all_0_94_94 % 9.26/2.63 | (565) ~ (all_0_27_27 = all_0_95_95) | ~ (all_0_28_28 = all_0_96_96) | ~ (all_0_29_29 = all_0_97_97) | ~ (all_0_30_30 = all_0_98_98) | ~ (all_0_31_31 = all_0_99_99) | ~ (all_0_32_32 = all_0_100_100) | ~ (all_0_33_33 = all_0_101_101) % 9.26/2.63 | % 9.26/2.63 +-Applying beta-rule and splitting (565), into two cases. % 9.26/2.63 |-Branch one: % 9.26/2.63 | (566) ~ (all_0_27_27 = all_0_95_95) % 9.26/2.63 | % 9.26/2.63 | Equations (530,397) can reduce 566 to: % 9.26/2.63 | (340) $false % 9.26/2.63 | % 9.26/2.63 |-The branch is then unsatisfiable % 9.26/2.63 |-Branch two: % 9.26/2.63 | (568) all_0_27_27 = all_0_95_95 % 9.26/2.63 | (569) ~ (all_0_28_28 = all_0_96_96) | ~ (all_0_29_29 = all_0_97_97) | ~ (all_0_30_30 = all_0_98_98) | ~ (all_0_31_31 = all_0_99_99) | ~ (all_0_32_32 = all_0_100_100) | ~ (all_0_33_33 = all_0_101_101) % 9.26/2.63 | % 9.26/2.63 +-Applying beta-rule and splitting (569), into two cases. % 9.26/2.63 |-Branch one: % 9.26/2.63 | (570) ~ (all_0_28_28 = all_0_96_96) % 9.26/2.63 | % 9.26/2.63 | Equations (537,405) can reduce 570 to: % 9.26/2.63 | (340) $false % 9.26/2.63 | % 9.26/2.63 |-The branch is then unsatisfiable % 9.26/2.63 |-Branch two: % 9.26/2.63 | (572) all_0_28_28 = all_0_96_96 % 9.26/2.63 | (573) ~ (all_0_29_29 = all_0_97_97) | ~ (all_0_30_30 = all_0_98_98) | ~ (all_0_31_31 = all_0_99_99) | ~ (all_0_32_32 = all_0_100_100) | ~ (all_0_33_33 = all_0_101_101) % 9.26/2.63 | % 9.26/2.63 +-Applying beta-rule and splitting (573), into two cases. % 9.26/2.63 |-Branch one: % 9.26/2.63 | (574) ~ (all_0_29_29 = all_0_97_97) % 9.26/2.63 | % 9.26/2.63 | Equations (540,383) can reduce 574 to: % 9.26/2.63 | (340) $false % 9.26/2.63 | % 9.26/2.63 |-The branch is then unsatisfiable % 9.26/2.63 |-Branch two: % 9.26/2.63 | (576) all_0_29_29 = all_0_97_97 % 9.26/2.63 | (577) ~ (all_0_30_30 = all_0_98_98) | ~ (all_0_31_31 = all_0_99_99) | ~ (all_0_32_32 = all_0_100_100) | ~ (all_0_33_33 = all_0_101_101) % 9.26/2.63 | % 9.26/2.63 +-Applying beta-rule and splitting (577), into two cases. % 9.26/2.63 |-Branch one: % 9.26/2.63 | (578) ~ (all_0_30_30 = all_0_98_98) % 9.26/2.63 | % 9.26/2.63 | Equations (539,360) can reduce 578 to: % 9.26/2.63 | (340) $false % 9.26/2.63 | % 9.26/2.63 |-The branch is then unsatisfiable % 9.26/2.63 |-Branch two: % 9.26/2.63 | (580) all_0_30_30 = all_0_98_98 % 9.26/2.63 | (581) ~ (all_0_31_31 = all_0_99_99) | ~ (all_0_32_32 = all_0_100_100) | ~ (all_0_33_33 = all_0_101_101) % 9.26/2.63 | % 9.26/2.63 +-Applying beta-rule and splitting (581), into two cases. % 9.26/2.63 |-Branch one: % 9.26/2.63 | (582) ~ (all_0_31_31 = all_0_99_99) % 9.26/2.63 | % 9.26/2.63 | Equations (545,331) can reduce 582 to: % 9.26/2.63 | (340) $false % 9.26/2.63 | % 9.26/2.63 |-The branch is then unsatisfiable % 9.26/2.63 |-Branch two: % 9.26/2.63 | (584) all_0_31_31 = all_0_99_99 % 9.26/2.63 | (585) ~ (all_0_32_32 = all_0_100_100) | ~ (all_0_33_33 = all_0_101_101) % 9.26/2.63 | % 9.26/2.63 +-Applying beta-rule and splitting (585), into two cases. % 9.26/2.63 |-Branch one: % 9.26/2.63 | (586) ~ (all_0_32_32 = all_0_100_100) % 9.26/2.63 | % 9.26/2.63 | Equations (543,351) can reduce 586 to: % 9.26/2.63 | (340) $false % 9.26/2.63 | % 9.26/2.63 |-The branch is then unsatisfiable % 9.26/2.63 |-Branch two: % 9.26/2.63 | (588) all_0_32_32 = all_0_100_100 % 9.26/2.63 | (589) ~ (all_0_33_33 = all_0_101_101) % 9.26/2.63 | % 9.26/2.63 | Equations (536,342) can reduce 589 to: % 9.26/2.63 | (340) $false % 9.26/2.63 | % 9.26/2.63 |-The branch is then unsatisfiable % 9.26/2.63 |-Branch two: % 9.26/2.63 | (591) ~ (all_0_104_104 = e12) % 9.26/2.63 | (592) all_0_109_109 = e12 | all_0_112_112 = e12 % 9.26/2.63 | % 9.26/2.63 +-Applying beta-rule and splitting (592), into two cases. % 9.26/2.63 |-Branch one: % 9.26/2.63 | (593) all_0_109_109 = e12 % 9.26/2.63 | % 9.26/2.63 | Combining equations (444,593) yields a new equation: % 9.26/2.63 | (594) e12 = e11 % 9.26/2.63 | % 9.26/2.63 | Equations (594) can reduce 58 to: % 9.26/2.63 | (340) $false % 9.26/2.63 | % 9.26/2.63 |-The branch is then unsatisfiable % 9.26/2.63 |-Branch two: % 9.26/2.63 | (596) ~ (all_0_109_109 = e12) % 9.26/2.63 | (597) all_0_112_112 = e12 % 9.26/2.63 | % 9.26/2.63 | Combining equations (597,499) yields a new equation: % 9.26/2.64 | (598) e13 = e12 % 9.26/2.64 | % 9.26/2.64 | Equations (598) can reduce 270 to: % 9.26/2.64 | (340) $false % 9.26/2.64 | % 9.26/2.64 |-The branch is then unsatisfiable % 9.26/2.64 |-Branch two: % 9.26/2.64 | (600) ~ (all_0_111_111 = e12) % 9.26/2.64 | (597) all_0_112_112 = e12 % 9.26/2.64 | % 9.26/2.64 | Combining equations (597,499) yields a new equation: % 9.26/2.64 | (598) e13 = e12 % 9.26/2.64 | % 9.26/2.64 | Equations (598) can reduce 270 to: % 9.26/2.64 | (340) $false % 9.26/2.64 | % 9.26/2.64 |-The branch is then unsatisfiable % 9.26/2.64 |-Branch two: % 9.26/2.64 | (604) ~ (all_0_108_108 = e10) % 9.26/2.64 | (605) all_0_108_108 = e12 % 9.26/2.64 | % 9.26/2.64 | Equations (605) can reduce 463 to: % 9.26/2.64 | (340) $false % 9.26/2.64 | % 9.26/2.64 |-The branch is then unsatisfiable % 9.26/2.64 |-Branch two: % 9.26/2.64 | (420) ~ (all_0_105_105 = e11) % 9.26/2.64 | (608) all_0_106_106 = e11 % 9.26/2.64 | % 9.26/2.64 | Equations (608) can reduce 481 to: % 9.26/2.64 | (340) $false % 9.26/2.64 | % 9.26/2.64 |-The branch is then unsatisfiable % 9.26/2.64 |-Branch two: % 9.26/2.64 | (413) ~ (all_0_103_103 = e13) % 9.26/2.64 | (433) all_0_111_111 = e10 & ~ (all_0_109_109 = e11) % 9.26/2.64 | % 9.26/2.64 | Applying alpha-rule on (433) yields: % 9.26/2.64 | (434) all_0_111_111 = e10 % 9.26/2.64 | (409) ~ (all_0_109_109 = e11) % 9.26/2.64 | % 9.26/2.64 | Equations (434) can reduce 428 to: % 9.26/2.64 | (340) $false % 9.26/2.64 | % 9.26/2.64 |-The branch is then unsatisfiable % 9.26/2.64 |-Branch two: % 9.26/2.64 | (407) ~ (all_0_102_102 = e11) % 9.26/2.64 | (406) all_0_107_107 = e11 % 9.26/2.64 | % 9.26/2.64 | Combining equations (461,406) yields a new equation: % 9.26/2.64 | (617) e12 = e11 % 9.26/2.64 | % 9.26/2.64 | Simplifying 617 yields: % 9.26/2.64 | (594) e12 = e11 % 9.26/2.64 | % 9.26/2.64 | Equations (594) can reduce 58 to: % 9.26/2.64 | (340) $false % 9.26/2.64 | % 9.26/2.64 |-The branch is then unsatisfiable % 9.26/2.64 |-Branch two: % 9.26/2.64 | (620) ~ (all_0_96_96 = e22) % 9.26/2.64 | (345) all_0_99_99 = e22 % 9.26/2.64 | % 9.26/2.64 | Combining equations (331,345) yields a new equation: % 9.26/2.64 | (347) e22 = e20 % 9.26/2.64 | % 9.26/2.64 | Equations (347) can reduce 207 to: % 9.26/2.64 | (340) $false % 9.26/2.64 | % 9.26/2.64 |-The branch is then unsatisfiable % 9.26/2.64 |-Branch two: % 9.26/2.64 | (624) ~ (all_0_97_97 = e20) % 9.26/2.64 | (625) all_0_98_98 = e20 % 9.26/2.64 | % 9.26/2.64 | Combining equations (360,625) yields a new equation: % 9.26/2.64 | (393) e21 = e20 % 9.26/2.64 | % 9.26/2.64 | Simplifying 393 yields: % 9.26/2.64 | (394) e21 = e20 % 9.26/2.64 | % 9.26/2.64 | Equations (394) can reduce 134 to: % 9.26/2.64 | (340) $false % 9.26/2.64 | % 9.26/2.64 |-The branch is then unsatisfiable % 9.26/2.64 |-Branch two: % 9.26/2.64 | (629) ~ (all_0_91_91 = e21) % 9.26/2.64 | (630) all_0_96_96 = e21 % 9.26/2.64 | % 9.26/2.64 | Equations (630) can reduce 362 to: % 9.26/2.64 | (340) $false % 9.26/2.64 | % 9.26/2.64 |-The branch is then unsatisfiable % 9.26/2.64 |-Branch two: % 9.26/2.64 | (632) ~ (all_0_100_100 = e22) % 9.26/2.64 | (633) all_0_101_101 = e22 % 9.26/2.64 | % 9.26/2.64 | Combining equations (342,633) yields a new equation: % 9.26/2.64 | (372) e23 = e22 % 9.26/2.64 | % 9.26/2.64 | Simplifying 372 yields: % 9.26/2.64 | (373) e23 = e22 % 9.26/2.64 | % 9.26/2.64 | Equations (373) can reduce 164 to: % 9.26/2.64 | (340) $false % 9.26/2.64 | % 9.26/2.64 |-The branch is then unsatisfiable % 9.26/2.64 |-Branch two: % 9.26/2.64 | (637) ~ (all_0_92_92 = e23) % 9.26/2.64 | (638) all_0_100_100 = e20 & ~ (all_0_98_98 = e21) % 9.26/2.64 | % 9.26/2.64 | Applying alpha-rule on (638) yields: % 9.26/2.64 | (639) all_0_100_100 = e20 % 9.26/2.64 | (640) ~ (all_0_98_98 = e21) % 9.26/2.64 | % 9.26/2.64 | Equations (639) can reduce 335 to: % 9.26/2.64 | (340) $false % 9.26/2.64 | % 9.26/2.64 |-The branch is then unsatisfiable % 9.26/2.64 |-Branch two: % 9.26/2.64 | (642) ~ (all_0_99_99 = e20) % 9.26/2.64 | (345) all_0_99_99 = e22 % 9.26/2.64 | % 9.26/2.64 | Equations (345) can reduce 253 to: % 9.26/2.64 | (620) ~ (all_0_96_96 = e22) % 9.26/2.64 | % 9.26/2.64 | Equations (345) can reduce 642 to: % 9.26/2.64 | (207) ~ (e22 = e20) % 9.26/2.64 | % 9.26/2.64 +-Applying beta-rule and splitting (109), into two cases. % 9.26/2.64 |-Branch one: % 9.26/2.64 | (379) all_0_96_96 = e20 % 9.26/2.64 | % 9.26/2.64 | Equations (379) can reduce 620 to: % 9.26/2.64 | (398) ~ (e22 = e20) % 9.26/2.64 | % 9.26/2.64 | Simplifying 398 yields: % 9.26/2.64 | (207) ~ (e22 = e20) % 9.26/2.64 | % 9.26/2.64 +-Applying beta-rule and splitting (130), into two cases. % 9.26/2.64 |-Branch one: % 9.26/2.64 | (331) all_0_99_99 = e20 % 9.26/2.64 | % 9.26/2.64 | Combining equations (331,345) yields a new equation: % 9.26/2.64 | (347) e22 = e20 % 9.26/2.64 | % 9.26/2.64 | Equations (347) can reduce 207 to: % 9.26/2.64 | (340) $false % 9.26/2.64 | % 9.26/2.64 |-The branch is then unsatisfiable % 9.26/2.64 |-Branch two: % 9.26/2.64 | (642) ~ (all_0_99_99 = e20) % 9.26/2.64 | (630) all_0_96_96 = e21 % 9.26/2.64 | % 9.26/2.64 | Combining equations (379,630) yields a new equation: % 9.26/2.64 | (394) e21 = e20 % 9.26/2.64 | % 9.26/2.64 | Equations (394) can reduce 134 to: % 9.26/2.64 | (340) $false % 9.26/2.64 | % 9.26/2.64 |-The branch is then unsatisfiable % 9.26/2.64 |-Branch two: % 9.26/2.64 | (333) ~ (all_0_96_96 = e20) % 9.26/2.64 | (331) all_0_99_99 = e20 % 9.26/2.64 | % 9.26/2.64 | Combining equations (331,345) yields a new equation: % 9.26/2.64 | (347) e22 = e20 % 9.26/2.64 | % 9.26/2.64 | Equations (347) can reduce 207 to: % 9.26/2.64 | (340) $false % 9.26/2.64 | % 9.26/2.64 |-The branch is then unsatisfiable % 9.26/2.64 % SZS output end Proof for theBenchmark % 9.26/2.64 % 9.26/2.64 2055ms %------------------------------------------------------------------------------