%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : ALG071+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:34:13 EDT 2022 % Result : Theorem 4.23s 1.73s % Output : Proof 22.67s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : ALG071+1 : TPTP v8.1.0. Released v2.7.0. % 0.03/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.34 % Computer : n018.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Wed Jun 8 05:14:06 EDT 2022 % 0.12/0.34 % CPUTime : % 0.55/0.59 ____ _ % 0.55/0.59 ___ / __ \_____(_)___ ________ __________ % 0.55/0.59 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.55/0.59 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.55/0.59 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.55/0.59 % 0.55/0.59 A Theorem Prover for First-Order Logic % 0.55/0.59 (ePrincess v.1.0) % 0.55/0.59 % 0.55/0.59 (c) Philipp Rümmer, 2009-2015 % 0.55/0.59 (c) Peter Backeman, 2014-2015 % 0.55/0.59 (contributions by Angelo Brillout, Peter Baumgartner) % 0.55/0.59 Free software under GNU Lesser General Public License (LGPL). % 0.55/0.59 Bug reports to peter@backeman.se % 0.55/0.59 % 0.55/0.59 For more information, visit http://user.uu.se/~petba168/breu/ % 0.55/0.59 % 0.55/0.60 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.74/0.65 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.41/0.94 Prover 0: Preprocessing ... % 1.91/1.11 Prover 0: Constructing countermodel ... % 4.23/1.73 Prover 0: proved (1083ms) % 4.23/1.73 % 4.23/1.73 No countermodel exists, formula is valid % 4.23/1.73 % SZS status Theorem for theBenchmark % 4.23/1.73 % 4.23/1.73 Generating proof ... found it (size 523) % 21.39/7.32 % 21.39/7.32 % SZS output start Proof for theBenchmark % 21.39/7.32 Assumed formulas after preprocessing and simplification: % 21.39/7.32 | (0) ? [v0] : (sorti2(v0) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | ~ (op2(v4, v3) = v2) | ~ (op2(v4, v3) = v1)) & ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | ~ (op1(v4, v3) = v2) | ~ (op1(v4, v3) = v1)) & ! [v1] : ! [v2] : ! [v3] : (v3 = v0 | ~ (op2(v1, v2) = v3) | ~ (op2(v1, v0) = v2) | ~ sorti2(v1) | ? [v4] : ( ~ (v4 = v1) & op2(v0, v2) = v4)) & ! [v1] : ! [v2] : ! [v3] : (v2 = v1 | ~ (j(v3) = v2) | ~ (j(v3) = v1)) & ! [v1] : ! [v2] : ! [v3] : (v2 = v1 | ~ (h(v3) = v2) | ~ (h(v3) = v1)) & ! [v1] : ! [v2] : ! [v3] : ( ~ (op2(v1, v2) = v3) | ~ sorti2(v2) | ~ sorti2(v1) | sorti2(v3)) & ! [v1] : ! [v2] : ! [v3] : ( ~ (op1(v1, v2) = v3) | ~ sorti1(v2) | ~ sorti1(v1) | sorti1(v3)) & ! [v1] : ! [v2] : ( ~ (op2(v1, v0) = v2) | ~ (op2(v0, v2) = v1) | ~ sorti2(v1) | op2(v1, v2) = v0) & ! [v1] : ( ~ sorti2(v1) | ? [v2] : (j(v1) = v2 & h(v2) = v1)) & ! [v1] : ( ~ sorti2(v1) | ? [v2] : (j(v1) = v2 & sorti1(v2))) & ! [v1] : ( ~ sorti2(v1) | ? [v2] : (j(v1) = v2 & ! [v3] : ( ~ sorti2(v3) | ? [v4] : ? [v5] : ? [v6] : (j(v4) = v5 & j(v3) = v6 & op2(v1, v3) = v4 & op1(v2, v6) = v5)))) & ! [v1] : ( ~ sorti1(v1) | ? [v2] : ? [v3] : ? [v4] : ( ~ (v4 = v1) & op1(v2, v3) = v4 & op1(v2, v1) = v3 & op1(v1, v3) = v2 & sorti1(v2))) & ! [v1] : ( ~ sorti1(v1) | ? [v2] : (j(v2) = v1 & h(v1) = v2)) & ! [v1] : ( ~ sorti1(v1) | ? [v2] : (h(v1) = v2 & sorti2(v2))) & ! [v1] : ( ~ sorti1(v1) | ? [v2] : (h(v1) = v2 & ! [v3] : ( ~ sorti1(v3) | ? [v4] : ? [v5] : ? [v6] : (h(v4) = v5 & h(v3) = v6 & op2(v2, v6) = v5 & op1(v1, v3) = v4))))) % 21.74/7.36 | Instantiating (0) with all_0_0_0 yields: % 21.74/7.36 | (1) sorti2(all_0_0_0) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op2(v3, v2) = v1) | ~ (op2(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op1(v3, v2) = v1) | ~ (op1(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v2 = all_0_0_0 | ~ (op2(v0, v1) = v2) | ~ (op2(v0, all_0_0_0) = v1) | ~ sorti2(v0) | ? [v3] : ( ~ (v3 = v0) & op2(all_0_0_0, v1) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (j(v2) = v1) | ~ (j(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h(v2) = v1) | ~ (h(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (op2(v0, v1) = v2) | ~ sorti2(v1) | ~ sorti2(v0) | sorti2(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (op1(v0, v1) = v2) | ~ sorti1(v1) | ~ sorti1(v0) | sorti1(v2)) & ! [v0] : ! [v1] : ( ~ (op2(v0, all_0_0_0) = v1) | ~ (op2(all_0_0_0, v1) = v0) | ~ sorti2(v0) | op2(v0, v1) = all_0_0_0) & ! [v0] : ( ~ sorti2(v0) | ? [v1] : (j(v0) = v1 & h(v1) = v0)) & ! [v0] : ( ~ sorti2(v0) | ? [v1] : (j(v0) = v1 & sorti1(v1))) & ! [v0] : ( ~ sorti2(v0) | ? [v1] : (j(v0) = v1 & ! [v2] : ( ~ sorti2(v2) | ? [v3] : ? [v4] : ? [v5] : (j(v3) = v4 & j(v2) = v5 & op2(v0, v2) = v3 & op1(v1, v5) = v4)))) & ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : ( ~ (v3 = v0) & op1(v1, v2) = v3 & op1(v1, v0) = v2 & op1(v0, v2) = v1 & sorti1(v1))) & ! [v0] : ( ~ sorti1(v0) | ? [v1] : (j(v1) = v0 & h(v0) = v1)) & ! [v0] : ( ~ sorti1(v0) | ? [v1] : (h(v0) = v1 & sorti2(v1))) & ! [v0] : ( ~ sorti1(v0) | ? [v1] : (h(v0) = v1 & ! [v2] : ( ~ sorti1(v2) | ? [v3] : ? [v4] : ? [v5] : (h(v3) = v4 & h(v2) = v5 & op2(v1, v5) = v4 & op1(v0, v2) = v3)))) % 21.74/7.37 | % 21.74/7.37 | Applying alpha-rule on (1) yields: % 21.74/7.37 | (2) ! [v0] : ! [v1] : ! [v2] : (v2 = all_0_0_0 | ~ (op2(v0, v1) = v2) | ~ (op2(v0, all_0_0_0) = v1) | ~ sorti2(v0) | ? [v3] : ( ~ (v3 = v0) & op2(all_0_0_0, v1) = v3)) % 21.74/7.37 | (3) ! [v0] : ( ~ sorti2(v0) | ? [v1] : (j(v0) = v1 & sorti1(v1))) % 21.74/7.37 | (4) ! [v0] : ( ~ sorti1(v0) | ? [v1] : (h(v0) = v1 & sorti2(v1))) % 21.74/7.37 | (5) ! [v0] : ( ~ sorti2(v0) | ? [v1] : (j(v0) = v1 & ! [v2] : ( ~ sorti2(v2) | ? [v3] : ? [v4] : ? [v5] : (j(v3) = v4 & j(v2) = v5 & op2(v0, v2) = v3 & op1(v1, v5) = v4)))) % 21.74/7.37 | (6) ! [v0] : ( ~ sorti1(v0) | ? [v1] : (h(v0) = v1 & ! [v2] : ( ~ sorti1(v2) | ? [v3] : ? [v4] : ? [v5] : (h(v3) = v4 & h(v2) = v5 & op2(v1, v5) = v4 & op1(v0, v2) = v3)))) % 21.74/7.37 | (7) ! [v0] : ( ~ sorti1(v0) | ? [v1] : (j(v1) = v0 & h(v0) = v1)) % 21.74/7.37 | (8) ! [v0] : ! [v1] : ! [v2] : ( ~ (op2(v0, v1) = v2) | ~ sorti2(v1) | ~ sorti2(v0) | sorti2(v2)) % 21.74/7.37 | (9) ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : ( ~ (v3 = v0) & op1(v1, v2) = v3 & op1(v1, v0) = v2 & op1(v0, v2) = v1 & sorti1(v1))) % 21.74/7.37 | (10) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (j(v2) = v1) | ~ (j(v2) = v0)) % 21.74/7.37 | (11) sorti2(all_0_0_0) % 21.74/7.37 | (12) ! [v0] : ( ~ sorti2(v0) | ? [v1] : (j(v0) = v1 & h(v1) = v0)) % 21.74/7.37 | (13) ! [v0] : ! [v1] : ( ~ (op2(v0, all_0_0_0) = v1) | ~ (op2(all_0_0_0, v1) = v0) | ~ sorti2(v0) | op2(v0, v1) = all_0_0_0) % 21.74/7.37 | (14) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h(v2) = v1) | ~ (h(v2) = v0)) % 21.74/7.37 | (15) ! [v0] : ! [v1] : ! [v2] : ( ~ (op1(v0, v1) = v2) | ~ sorti1(v1) | ~ sorti1(v0) | sorti1(v2)) % 21.74/7.37 | (16) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op1(v3, v2) = v1) | ~ (op1(v3, v2) = v0)) % 21.74/7.38 | (17) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op2(v3, v2) = v1) | ~ (op2(v3, v2) = v0)) % 21.89/7.38 | % 21.89/7.38 | Instantiating formula (12) with all_0_0_0 and discharging atoms sorti2(all_0_0_0), yields: % 21.89/7.38 | (18) ? [v0] : (j(all_0_0_0) = v0 & h(v0) = all_0_0_0) % 21.89/7.38 | % 21.89/7.38 | Instantiating formula (3) with all_0_0_0 and discharging atoms sorti2(all_0_0_0), yields: % 21.89/7.38 | (19) ? [v0] : (j(all_0_0_0) = v0 & sorti1(v0)) % 21.89/7.38 | % 21.89/7.38 | Instantiating formula (5) with all_0_0_0 and discharging atoms sorti2(all_0_0_0), yields: % 21.89/7.38 | (20) ? [v0] : (j(all_0_0_0) = v0 & ! [v1] : ( ~ sorti2(v1) | ? [v2] : ? [v3] : ? [v4] : (j(v2) = v3 & j(v1) = v4 & op2(all_0_0_0, v1) = v2 & op1(v0, v4) = v3))) % 21.89/7.38 | % 21.89/7.38 | Instantiating (20) with all_8_0_1 yields: % 21.89/7.38 | (21) j(all_0_0_0) = all_8_0_1 & ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_0_0_0, v0) = v1 & op1(all_8_0_1, v3) = v2)) % 21.89/7.38 | % 21.89/7.38 | Applying alpha-rule on (21) yields: % 21.89/7.38 | (22) j(all_0_0_0) = all_8_0_1 % 21.89/7.38 | (23) ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_0_0_0, v0) = v1 & op1(all_8_0_1, v3) = v2)) % 21.89/7.38 | % 21.89/7.38 | Instantiating formula (23) with all_0_0_0 and discharging atoms sorti2(all_0_0_0), yields: % 21.89/7.38 | (24) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_0_0) = v2 & op2(all_0_0_0, all_0_0_0) = v0 & op1(all_8_0_1, v2) = v1) % 21.89/7.38 | % 21.89/7.38 | Instantiating (19) with all_11_0_2 yields: % 21.89/7.38 | (25) j(all_0_0_0) = all_11_0_2 & sorti1(all_11_0_2) % 21.89/7.38 | % 21.89/7.38 | Applying alpha-rule on (25) yields: % 21.89/7.38 | (26) j(all_0_0_0) = all_11_0_2 % 21.89/7.38 | (27) sorti1(all_11_0_2) % 21.89/7.38 | % 21.89/7.38 | Instantiating (18) with all_13_0_3 yields: % 21.89/7.38 | (28) j(all_0_0_0) = all_13_0_3 & h(all_13_0_3) = all_0_0_0 % 21.89/7.38 | % 21.89/7.38 | Applying alpha-rule on (28) yields: % 21.89/7.38 | (29) j(all_0_0_0) = all_13_0_3 % 21.89/7.38 | (30) h(all_13_0_3) = all_0_0_0 % 21.89/7.38 | % 21.89/7.38 | Instantiating (24) with all_15_0_4, all_15_1_5, all_15_2_6 yields: % 21.89/7.38 | (31) j(all_15_2_6) = all_15_1_5 & j(all_0_0_0) = all_15_0_4 & op2(all_0_0_0, all_0_0_0) = all_15_2_6 & op1(all_8_0_1, all_15_0_4) = all_15_1_5 % 21.89/7.38 | % 21.89/7.38 | Applying alpha-rule on (31) yields: % 21.89/7.38 | (32) j(all_15_2_6) = all_15_1_5 % 21.89/7.38 | (33) j(all_0_0_0) = all_15_0_4 % 21.89/7.38 | (34) op2(all_0_0_0, all_0_0_0) = all_15_2_6 % 21.89/7.38 | (35) op1(all_8_0_1, all_15_0_4) = all_15_1_5 % 21.89/7.38 | % 21.89/7.38 | Instantiating formula (10) with all_0_0_0, all_13_0_3, all_15_0_4 and discharging atoms j(all_0_0_0) = all_15_0_4, j(all_0_0_0) = all_13_0_3, yields: % 21.89/7.38 | (36) all_15_0_4 = all_13_0_3 % 21.89/7.38 | % 21.89/7.38 | Instantiating formula (10) with all_0_0_0, all_11_0_2, all_15_0_4 and discharging atoms j(all_0_0_0) = all_15_0_4, j(all_0_0_0) = all_11_0_2, yields: % 21.89/7.38 | (37) all_15_0_4 = all_11_0_2 % 21.89/7.38 | % 21.89/7.38 | Instantiating formula (10) with all_0_0_0, all_8_0_1, all_13_0_3 and discharging atoms j(all_0_0_0) = all_13_0_3, j(all_0_0_0) = all_8_0_1, yields: % 21.89/7.38 | (38) all_13_0_3 = all_8_0_1 % 21.89/7.38 | % 21.89/7.38 | Combining equations (36,37) yields a new equation: % 21.89/7.38 | (39) all_13_0_3 = all_11_0_2 % 21.89/7.38 | % 21.89/7.38 | Simplifying 39 yields: % 21.89/7.38 | (40) all_13_0_3 = all_11_0_2 % 21.89/7.38 | % 21.89/7.38 | Combining equations (38,40) yields a new equation: % 21.89/7.38 | (41) all_11_0_2 = all_8_0_1 % 21.89/7.38 | % 21.89/7.38 | Combining equations (41,40) yields a new equation: % 21.89/7.38 | (38) all_13_0_3 = all_8_0_1 % 21.89/7.38 | % 21.89/7.38 | Combining equations (41,37) yields a new equation: % 21.89/7.38 | (43) all_15_0_4 = all_8_0_1 % 21.89/7.38 | % 21.89/7.38 | From (41) and (26) follows: % 21.89/7.39 | (22) j(all_0_0_0) = all_8_0_1 % 21.89/7.39 | % 21.89/7.39 | From (38) and (30) follows: % 21.89/7.39 | (45) h(all_8_0_1) = all_0_0_0 % 21.89/7.39 | % 21.89/7.39 | From (43) and (35) follows: % 21.89/7.39 | (46) op1(all_8_0_1, all_8_0_1) = all_15_1_5 % 21.89/7.39 | % 21.89/7.39 | From (41) and (27) follows: % 21.89/7.39 | (47) sorti1(all_8_0_1) % 21.89/7.39 | % 21.89/7.39 | Instantiating formula (8) with all_15_2_6, all_0_0_0, all_0_0_0 and discharging atoms op2(all_0_0_0, all_0_0_0) = all_15_2_6, sorti2(all_0_0_0), yields: % 21.89/7.39 | (48) sorti2(all_15_2_6) % 21.89/7.39 | % 21.89/7.39 | Instantiating formula (15) with all_15_1_5, all_8_0_1, all_8_0_1 and discharging atoms op1(all_8_0_1, all_8_0_1) = all_15_1_5, sorti1(all_8_0_1), yields: % 21.89/7.39 | (49) sorti1(all_15_1_5) % 21.89/7.39 | % 21.89/7.39 | Instantiating formula (9) with all_8_0_1 and discharging atoms sorti1(all_8_0_1), yields: % 21.89/7.39 | (50) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = all_8_0_1) & op1(v0, v1) = v2 & op1(v0, all_8_0_1) = v1 & op1(all_8_0_1, v1) = v0 & sorti1(v0)) % 21.89/7.39 | % 21.89/7.39 | Instantiating formula (6) with all_8_0_1 and discharging atoms sorti1(all_8_0_1), yields: % 21.89/7.39 | (51) ? [v0] : (h(all_8_0_1) = v0 & ! [v1] : ( ~ sorti1(v1) | ? [v2] : ? [v3] : ? [v4] : (h(v2) = v3 & h(v1) = v4 & op2(v0, v4) = v3 & op1(all_8_0_1, v1) = v2))) % 21.89/7.39 | % 21.89/7.39 | Instantiating (51) with all_27_0_7 yields: % 21.89/7.39 | (52) h(all_8_0_1) = all_27_0_7 & ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_27_0_7, v3) = v2 & op1(all_8_0_1, v0) = v1)) % 21.89/7.39 | % 21.89/7.39 | Applying alpha-rule on (52) yields: % 21.89/7.39 | (53) h(all_8_0_1) = all_27_0_7 % 21.89/7.39 | (54) ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_27_0_7, v3) = v2 & op1(all_8_0_1, v0) = v1)) % 21.89/7.39 | % 21.89/7.39 | Instantiating formula (54) with all_8_0_1 and discharging atoms sorti1(all_8_0_1), yields: % 21.89/7.39 | (55) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_8_0_1) = v2 & op2(all_27_0_7, v2) = v1 & op1(all_8_0_1, all_8_0_1) = v0) % 21.89/7.39 | % 21.89/7.39 | Instantiating (50) with all_30_0_8, all_30_1_9, all_30_2_10 yields: % 21.89/7.39 | (56) ~ (all_30_0_8 = all_8_0_1) & op1(all_30_2_10, all_30_1_9) = all_30_0_8 & op1(all_30_2_10, all_8_0_1) = all_30_1_9 & op1(all_8_0_1, all_30_1_9) = all_30_2_10 & sorti1(all_30_2_10) % 21.89/7.39 | % 21.89/7.39 | Applying alpha-rule on (56) yields: % 21.89/7.39 | (57) op1(all_8_0_1, all_30_1_9) = all_30_2_10 % 21.89/7.39 | (58) op1(all_30_2_10, all_8_0_1) = all_30_1_9 % 21.89/7.39 | (59) ~ (all_30_0_8 = all_8_0_1) % 21.89/7.39 | (60) sorti1(all_30_2_10) % 21.89/7.39 | (61) op1(all_30_2_10, all_30_1_9) = all_30_0_8 % 21.89/7.39 | % 21.89/7.39 | Instantiating (55) with all_32_0_11, all_32_1_12, all_32_2_13 yields: % 21.89/7.39 | (62) h(all_32_2_13) = all_32_1_12 & h(all_8_0_1) = all_32_0_11 & op2(all_27_0_7, all_32_0_11) = all_32_1_12 & op1(all_8_0_1, all_8_0_1) = all_32_2_13 % 21.89/7.39 | % 21.89/7.39 | Applying alpha-rule on (62) yields: % 21.89/7.39 | (63) h(all_32_2_13) = all_32_1_12 % 21.89/7.39 | (64) h(all_8_0_1) = all_32_0_11 % 21.89/7.39 | (65) op2(all_27_0_7, all_32_0_11) = all_32_1_12 % 21.89/7.39 | (66) op1(all_8_0_1, all_8_0_1) = all_32_2_13 % 21.89/7.39 | % 21.89/7.39 | Instantiating formula (14) with all_8_0_1, all_32_0_11, all_0_0_0 and discharging atoms h(all_8_0_1) = all_32_0_11, h(all_8_0_1) = all_0_0_0, yields: % 21.89/7.39 | (67) all_32_0_11 = all_0_0_0 % 21.89/7.39 | % 21.89/7.39 | Instantiating formula (14) with all_8_0_1, all_27_0_7, all_32_0_11 and discharging atoms h(all_8_0_1) = all_32_0_11, h(all_8_0_1) = all_27_0_7, yields: % 21.89/7.39 | (68) all_32_0_11 = all_27_0_7 % 21.89/7.39 | % 21.89/7.39 | Instantiating formula (16) with all_8_0_1, all_8_0_1, all_32_2_13, all_15_1_5 and discharging atoms op1(all_8_0_1, all_8_0_1) = all_32_2_13, op1(all_8_0_1, all_8_0_1) = all_15_1_5, yields: % 21.89/7.39 | (69) all_32_2_13 = all_15_1_5 % 21.89/7.39 | % 21.89/7.39 | Combining equations (67,68) yields a new equation: % 21.89/7.39 | (70) all_27_0_7 = all_0_0_0 % 21.89/7.39 | % 21.89/7.39 | Combining equations (70,68) yields a new equation: % 21.89/7.39 | (67) all_32_0_11 = all_0_0_0 % 21.89/7.39 | % 21.89/7.39 | From (69) and (63) follows: % 21.89/7.39 | (72) h(all_15_1_5) = all_32_1_12 % 21.89/7.39 | % 21.89/7.39 | From (70) and (53) follows: % 21.89/7.39 | (45) h(all_8_0_1) = all_0_0_0 % 21.89/7.39 | % 21.89/7.39 | From (70)(67) and (65) follows: % 21.89/7.39 | (74) op2(all_0_0_0, all_0_0_0) = all_32_1_12 % 21.89/7.39 | % 21.89/7.39 | Instantiating formula (17) with all_0_0_0, all_0_0_0, all_32_1_12, all_15_2_6 and discharging atoms op2(all_0_0_0, all_0_0_0) = all_32_1_12, op2(all_0_0_0, all_0_0_0) = all_15_2_6, yields: % 21.89/7.39 | (75) all_32_1_12 = all_15_2_6 % 21.89/7.39 | % 21.89/7.39 | From (75) and (72) follows: % 21.89/7.39 | (76) h(all_15_1_5) = all_15_2_6 % 21.89/7.39 | % 21.89/7.39 | Instantiating formula (23) with all_15_2_6 and discharging atoms sorti2(all_15_2_6), yields: % 21.89/7.39 | (77) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_15_2_6) = v2 & op2(all_0_0_0, all_15_2_6) = v0 & op1(all_8_0_1, v2) = v1) % 21.89/7.40 | % 21.89/7.40 | Instantiating formula (5) with all_15_2_6 and discharging atoms sorti2(all_15_2_6), yields: % 21.89/7.40 | (78) ? [v0] : (j(all_15_2_6) = v0 & ! [v1] : ( ~ sorti2(v1) | ? [v2] : ? [v3] : ? [v4] : (j(v2) = v3 & j(v1) = v4 & op2(all_15_2_6, v1) = v2 & op1(v0, v4) = v3))) % 21.89/7.40 | % 21.89/7.40 | Instantiating formula (15) with all_30_1_9, all_8_0_1, all_30_2_10 and discharging atoms op1(all_30_2_10, all_8_0_1) = all_30_1_9, sorti1(all_30_2_10), sorti1(all_8_0_1), yields: % 21.89/7.40 | (79) sorti1(all_30_1_9) % 21.89/7.40 | % 21.89/7.40 | Instantiating formula (9) with all_30_2_10 and discharging atoms sorti1(all_30_2_10), yields: % 21.89/7.40 | (80) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = all_30_2_10) & op1(v0, v1) = v2 & op1(v0, all_30_2_10) = v1 & op1(all_30_2_10, v1) = v0 & sorti1(v0)) % 21.89/7.40 | % 21.89/7.40 | Instantiating formula (54) with all_30_2_10 and discharging atoms sorti1(all_30_2_10), yields: % 21.89/7.40 | (81) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_30_2_10) = v2 & op2(all_27_0_7, v2) = v1 & op1(all_8_0_1, all_30_2_10) = v0) % 21.89/7.40 | % 21.89/7.40 | Instantiating formula (7) with all_30_2_10 and discharging atoms sorti1(all_30_2_10), yields: % 21.89/7.40 | (82) ? [v0] : (j(v0) = all_30_2_10 & h(all_30_2_10) = v0) % 21.89/7.40 | % 21.89/7.40 | Instantiating formula (4) with all_30_2_10 and discharging atoms sorti1(all_30_2_10), yields: % 21.89/7.40 | (83) ? [v0] : (h(all_30_2_10) = v0 & sorti2(v0)) % 21.89/7.40 | % 21.89/7.40 | Instantiating formula (6) with all_30_2_10 and discharging atoms sorti1(all_30_2_10), yields: % 21.89/7.40 | (84) ? [v0] : (h(all_30_2_10) = v0 & ! [v1] : ( ~ sorti1(v1) | ? [v2] : ? [v3] : ? [v4] : (h(v2) = v3 & h(v1) = v4 & op2(v0, v4) = v3 & op1(all_30_2_10, v1) = v2))) % 21.89/7.40 | % 21.89/7.40 | Instantiating formula (9) with all_15_1_5 and discharging atoms sorti1(all_15_1_5), yields: % 21.89/7.40 | (85) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = all_15_1_5) & op1(v0, v1) = v2 & op1(v0, all_15_1_5) = v1 & op1(all_15_1_5, v1) = v0 & sorti1(v0)) % 21.89/7.40 | % 21.89/7.40 | Instantiating formula (54) with all_15_1_5 and discharging atoms sorti1(all_15_1_5), yields: % 21.89/7.40 | (86) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_15_1_5) = v2 & op2(all_27_0_7, v2) = v1 & op1(all_8_0_1, all_15_1_5) = v0) % 21.89/7.40 | % 21.89/7.40 | Instantiating formula (6) with all_15_1_5 and discharging atoms sorti1(all_15_1_5), yields: % 21.89/7.40 | (87) ? [v0] : (h(all_15_1_5) = v0 & ! [v1] : ( ~ sorti1(v1) | ? [v2] : ? [v3] : ? [v4] : (h(v2) = v3 & h(v1) = v4 & op2(v0, v4) = v3 & op1(all_15_1_5, v1) = v2))) % 21.89/7.40 | % 21.89/7.40 | Instantiating (87) with all_48_0_14 yields: % 21.89/7.40 | (88) h(all_15_1_5) = all_48_0_14 & ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_48_0_14, v3) = v2 & op1(all_15_1_5, v0) = v1)) % 21.89/7.40 | % 21.89/7.40 | Applying alpha-rule on (88) yields: % 21.89/7.40 | (89) h(all_15_1_5) = all_48_0_14 % 21.89/7.40 | (90) ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_48_0_14, v3) = v2 & op1(all_15_1_5, v0) = v1)) % 21.89/7.40 | % 21.89/7.40 | Instantiating formula (90) with all_30_2_10 and discharging atoms sorti1(all_30_2_10), yields: % 21.89/7.40 | (91) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_30_2_10) = v2 & op2(all_48_0_14, v2) = v1 & op1(all_15_1_5, all_30_2_10) = v0) % 21.89/7.40 | % 21.89/7.40 | Instantiating formula (90) with all_15_1_5 and discharging atoms sorti1(all_15_1_5), yields: % 21.89/7.40 | (92) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_15_1_5) = v2 & op2(all_48_0_14, v2) = v1 & op1(all_15_1_5, all_15_1_5) = v0) % 21.89/7.40 | % 21.89/7.40 | Instantiating formula (90) with all_8_0_1 and discharging atoms sorti1(all_8_0_1), yields: % 21.89/7.40 | (93) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_8_0_1) = v2 & op2(all_48_0_14, v2) = v1 & op1(all_15_1_5, all_8_0_1) = v0) % 21.89/7.40 | % 21.89/7.40 | Instantiating (78) with all_51_0_15 yields: % 21.89/7.40 | (94) j(all_15_2_6) = all_51_0_15 & ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_15_2_6, v0) = v1 & op1(all_51_0_15, v3) = v2)) % 21.89/7.40 | % 21.89/7.40 | Applying alpha-rule on (94) yields: % 21.89/7.40 | (95) j(all_15_2_6) = all_51_0_15 % 21.89/7.40 | (96) ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_15_2_6, v0) = v1 & op1(all_51_0_15, v3) = v2)) % 21.89/7.40 | % 21.89/7.40 | Instantiating formula (96) with all_15_2_6 and discharging atoms sorti2(all_15_2_6), yields: % 21.89/7.40 | (97) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_15_2_6) = v2 & op2(all_15_2_6, all_15_2_6) = v0 & op1(all_51_0_15, v2) = v1) % 21.89/7.40 | % 21.89/7.40 | Instantiating formula (96) with all_0_0_0 and discharging atoms sorti2(all_0_0_0), yields: % 21.89/7.40 | (98) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_0_0) = v2 & op2(all_15_2_6, all_0_0_0) = v0 & op1(all_51_0_15, v2) = v1) % 21.89/7.40 | % 21.89/7.40 | Instantiating (77) with all_54_0_16, all_54_1_17, all_54_2_18 yields: % 21.89/7.40 | (99) j(all_54_2_18) = all_54_1_17 & j(all_15_2_6) = all_54_0_16 & op2(all_0_0_0, all_15_2_6) = all_54_2_18 & op1(all_8_0_1, all_54_0_16) = all_54_1_17 % 21.89/7.40 | % 21.89/7.40 | Applying alpha-rule on (99) yields: % 21.89/7.40 | (100) j(all_54_2_18) = all_54_1_17 % 21.89/7.40 | (101) j(all_15_2_6) = all_54_0_16 % 21.89/7.40 | (102) op2(all_0_0_0, all_15_2_6) = all_54_2_18 % 21.89/7.40 | (103) op1(all_8_0_1, all_54_0_16) = all_54_1_17 % 21.89/7.41 | % 21.89/7.41 | Instantiating (86) with all_56_0_19, all_56_1_20, all_56_2_21 yields: % 21.89/7.41 | (104) h(all_56_2_21) = all_56_1_20 & h(all_15_1_5) = all_56_0_19 & op2(all_27_0_7, all_56_0_19) = all_56_1_20 & op1(all_8_0_1, all_15_1_5) = all_56_2_21 % 21.89/7.41 | % 21.89/7.41 | Applying alpha-rule on (104) yields: % 21.89/7.41 | (105) h(all_56_2_21) = all_56_1_20 % 21.89/7.41 | (106) h(all_15_1_5) = all_56_0_19 % 21.89/7.41 | (107) op2(all_27_0_7, all_56_0_19) = all_56_1_20 % 21.89/7.41 | (108) op1(all_8_0_1, all_15_1_5) = all_56_2_21 % 21.89/7.41 | % 21.89/7.41 | Instantiating (85) with all_58_0_22, all_58_1_23, all_58_2_24 yields: % 21.89/7.41 | (109) ~ (all_58_0_22 = all_15_1_5) & op1(all_58_2_24, all_58_1_23) = all_58_0_22 & op1(all_58_2_24, all_15_1_5) = all_58_1_23 & op1(all_15_1_5, all_58_1_23) = all_58_2_24 & sorti1(all_58_2_24) % 21.89/7.41 | % 21.89/7.41 | Applying alpha-rule on (109) yields: % 21.89/7.41 | (110) ~ (all_58_0_22 = all_15_1_5) % 21.89/7.41 | (111) op1(all_15_1_5, all_58_1_23) = all_58_2_24 % 21.89/7.41 | (112) sorti1(all_58_2_24) % 21.89/7.41 | (113) op1(all_58_2_24, all_58_1_23) = all_58_0_22 % 21.89/7.41 | (114) op1(all_58_2_24, all_15_1_5) = all_58_1_23 % 21.89/7.41 | % 21.89/7.41 | Instantiating (84) with all_60_0_25 yields: % 21.89/7.41 | (115) h(all_30_2_10) = all_60_0_25 & ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_60_0_25, v3) = v2 & op1(all_30_2_10, v0) = v1)) % 21.89/7.41 | % 21.89/7.41 | Applying alpha-rule on (115) yields: % 21.89/7.41 | (116) h(all_30_2_10) = all_60_0_25 % 21.89/7.41 | (117) ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_60_0_25, v3) = v2 & op1(all_30_2_10, v0) = v1)) % 21.89/7.41 | % 21.89/7.41 | Instantiating formula (117) with all_30_2_10 and discharging atoms sorti1(all_30_2_10), yields: % 21.89/7.41 | (118) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_30_2_10) = v2 & op2(all_60_0_25, v2) = v1 & op1(all_30_2_10, all_30_2_10) = v0) % 21.89/7.41 | % 21.89/7.41 | Instantiating formula (117) with all_15_1_5 and discharging atoms sorti1(all_15_1_5), yields: % 21.89/7.41 | (119) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_15_1_5) = v2 & op2(all_60_0_25, v2) = v1 & op1(all_30_2_10, all_15_1_5) = v0) % 21.89/7.41 | % 21.89/7.41 | Instantiating formula (117) with all_8_0_1 and discharging atoms sorti1(all_8_0_1), yields: % 21.89/7.41 | (120) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_8_0_1) = v2 & op2(all_60_0_25, v2) = v1 & op1(all_30_2_10, all_8_0_1) = v0) % 21.89/7.41 | % 21.89/7.41 | Instantiating (83) with all_63_0_26 yields: % 21.89/7.41 | (121) h(all_30_2_10) = all_63_0_26 & sorti2(all_63_0_26) % 21.89/7.41 | % 21.89/7.41 | Applying alpha-rule on (121) yields: % 21.89/7.41 | (122) h(all_30_2_10) = all_63_0_26 % 21.89/7.41 | (123) sorti2(all_63_0_26) % 21.89/7.41 | % 21.89/7.41 | Instantiating (80) with all_65_0_27, all_65_1_28, all_65_2_29 yields: % 21.89/7.41 | (124) ~ (all_65_0_27 = all_30_2_10) & op1(all_65_2_29, all_65_1_28) = all_65_0_27 & op1(all_65_2_29, all_30_2_10) = all_65_1_28 & op1(all_30_2_10, all_65_1_28) = all_65_2_29 & sorti1(all_65_2_29) % 21.89/7.41 | % 21.89/7.41 | Applying alpha-rule on (124) yields: % 21.89/7.41 | (125) op1(all_30_2_10, all_65_1_28) = all_65_2_29 % 21.89/7.41 | (126) op1(all_65_2_29, all_30_2_10) = all_65_1_28 % 21.89/7.41 | (127) ~ (all_65_0_27 = all_30_2_10) % 21.89/7.41 | (128) op1(all_65_2_29, all_65_1_28) = all_65_0_27 % 21.89/7.41 | (129) sorti1(all_65_2_29) % 21.89/7.41 | % 21.89/7.41 | Instantiating (82) with all_67_0_30 yields: % 21.89/7.41 | (130) j(all_67_0_30) = all_30_2_10 & h(all_30_2_10) = all_67_0_30 % 21.89/7.41 | % 21.89/7.41 | Applying alpha-rule on (130) yields: % 21.89/7.41 | (131) j(all_67_0_30) = all_30_2_10 % 21.89/7.41 | (132) h(all_30_2_10) = all_67_0_30 % 21.89/7.41 | % 21.89/7.41 | Instantiating (81) with all_69_0_31, all_69_1_32, all_69_2_33 yields: % 21.89/7.41 | (133) h(all_69_2_33) = all_69_1_32 & h(all_30_2_10) = all_69_0_31 & op2(all_27_0_7, all_69_0_31) = all_69_1_32 & op1(all_8_0_1, all_30_2_10) = all_69_2_33 % 21.89/7.41 | % 21.89/7.41 | Applying alpha-rule on (133) yields: % 21.89/7.41 | (134) h(all_69_2_33) = all_69_1_32 % 21.89/7.41 | (135) h(all_30_2_10) = all_69_0_31 % 21.89/7.41 | (136) op2(all_27_0_7, all_69_0_31) = all_69_1_32 % 21.89/7.41 | (137) op1(all_8_0_1, all_30_2_10) = all_69_2_33 % 21.89/7.41 | % 21.89/7.41 | Instantiating (93) with all_71_0_34, all_71_1_35, all_71_2_36 yields: % 21.89/7.41 | (138) h(all_71_2_36) = all_71_1_35 & h(all_8_0_1) = all_71_0_34 & op2(all_48_0_14, all_71_0_34) = all_71_1_35 & op1(all_15_1_5, all_8_0_1) = all_71_2_36 % 21.89/7.41 | % 21.89/7.41 | Applying alpha-rule on (138) yields: % 21.89/7.41 | (139) h(all_71_2_36) = all_71_1_35 % 21.89/7.41 | (140) h(all_8_0_1) = all_71_0_34 % 21.89/7.41 | (141) op2(all_48_0_14, all_71_0_34) = all_71_1_35 % 21.89/7.41 | (142) op1(all_15_1_5, all_8_0_1) = all_71_2_36 % 21.89/7.41 | % 21.89/7.41 | Instantiating (92) with all_73_0_37, all_73_1_38, all_73_2_39 yields: % 21.89/7.41 | (143) h(all_73_2_39) = all_73_1_38 & h(all_15_1_5) = all_73_0_37 & op2(all_48_0_14, all_73_0_37) = all_73_1_38 & op1(all_15_1_5, all_15_1_5) = all_73_2_39 % 21.89/7.41 | % 21.89/7.41 | Applying alpha-rule on (143) yields: % 21.89/7.41 | (144) h(all_73_2_39) = all_73_1_38 % 21.89/7.41 | (145) h(all_15_1_5) = all_73_0_37 % 21.89/7.41 | (146) op2(all_48_0_14, all_73_0_37) = all_73_1_38 % 21.89/7.41 | (147) op1(all_15_1_5, all_15_1_5) = all_73_2_39 % 21.89/7.41 | % 21.89/7.41 | Instantiating (91) with all_75_0_40, all_75_1_41, all_75_2_42 yields: % 21.89/7.41 | (148) h(all_75_2_42) = all_75_1_41 & h(all_30_2_10) = all_75_0_40 & op2(all_48_0_14, all_75_0_40) = all_75_1_41 & op1(all_15_1_5, all_30_2_10) = all_75_2_42 % 21.89/7.41 | % 21.89/7.41 | Applying alpha-rule on (148) yields: % 21.89/7.41 | (149) h(all_75_2_42) = all_75_1_41 % 21.89/7.42 | (150) h(all_30_2_10) = all_75_0_40 % 21.89/7.42 | (151) op2(all_48_0_14, all_75_0_40) = all_75_1_41 % 21.89/7.42 | (152) op1(all_15_1_5, all_30_2_10) = all_75_2_42 % 21.89/7.42 | % 21.89/7.42 | Instantiating (98) with all_77_0_43, all_77_1_44, all_77_2_45 yields: % 21.89/7.42 | (153) j(all_77_2_45) = all_77_1_44 & j(all_0_0_0) = all_77_0_43 & op2(all_15_2_6, all_0_0_0) = all_77_2_45 & op1(all_51_0_15, all_77_0_43) = all_77_1_44 % 21.89/7.42 | % 21.89/7.42 | Applying alpha-rule on (153) yields: % 21.89/7.42 | (154) j(all_77_2_45) = all_77_1_44 % 21.89/7.42 | (155) j(all_0_0_0) = all_77_0_43 % 21.89/7.42 | (156) op2(all_15_2_6, all_0_0_0) = all_77_2_45 % 21.89/7.42 | (157) op1(all_51_0_15, all_77_0_43) = all_77_1_44 % 21.89/7.42 | % 21.89/7.42 | Instantiating (97) with all_79_0_46, all_79_1_47, all_79_2_48 yields: % 21.89/7.42 | (158) j(all_79_2_48) = all_79_1_47 & j(all_15_2_6) = all_79_0_46 & op2(all_15_2_6, all_15_2_6) = all_79_2_48 & op1(all_51_0_15, all_79_0_46) = all_79_1_47 % 21.89/7.42 | % 21.89/7.42 | Applying alpha-rule on (158) yields: % 21.89/7.42 | (159) j(all_79_2_48) = all_79_1_47 % 21.89/7.42 | (160) j(all_15_2_6) = all_79_0_46 % 21.89/7.42 | (161) op2(all_15_2_6, all_15_2_6) = all_79_2_48 % 21.89/7.42 | (162) op1(all_51_0_15, all_79_0_46) = all_79_1_47 % 21.89/7.42 | % 21.89/7.42 | Instantiating (120) with all_81_0_49, all_81_1_50, all_81_2_51 yields: % 21.89/7.42 | (163) h(all_81_2_51) = all_81_1_50 & h(all_8_0_1) = all_81_0_49 & op2(all_60_0_25, all_81_0_49) = all_81_1_50 & op1(all_30_2_10, all_8_0_1) = all_81_2_51 % 21.89/7.42 | % 21.89/7.42 | Applying alpha-rule on (163) yields: % 21.89/7.42 | (164) h(all_81_2_51) = all_81_1_50 % 21.89/7.42 | (165) h(all_8_0_1) = all_81_0_49 % 21.89/7.42 | (166) op2(all_60_0_25, all_81_0_49) = all_81_1_50 % 21.89/7.42 | (167) op1(all_30_2_10, all_8_0_1) = all_81_2_51 % 21.89/7.42 | % 21.89/7.42 | Instantiating (119) with all_83_0_52, all_83_1_53, all_83_2_54 yields: % 21.89/7.42 | (168) h(all_83_2_54) = all_83_1_53 & h(all_15_1_5) = all_83_0_52 & op2(all_60_0_25, all_83_0_52) = all_83_1_53 & op1(all_30_2_10, all_15_1_5) = all_83_2_54 % 21.89/7.42 | % 21.89/7.42 | Applying alpha-rule on (168) yields: % 21.89/7.42 | (169) h(all_83_2_54) = all_83_1_53 % 21.89/7.42 | (170) h(all_15_1_5) = all_83_0_52 % 21.89/7.42 | (171) op2(all_60_0_25, all_83_0_52) = all_83_1_53 % 21.89/7.42 | (172) op1(all_30_2_10, all_15_1_5) = all_83_2_54 % 21.89/7.42 | % 21.89/7.42 | Instantiating (118) with all_85_0_55, all_85_1_56, all_85_2_57 yields: % 21.89/7.42 | (173) h(all_85_2_57) = all_85_1_56 & h(all_30_2_10) = all_85_0_55 & op2(all_60_0_25, all_85_0_55) = all_85_1_56 & op1(all_30_2_10, all_30_2_10) = all_85_2_57 % 21.89/7.42 | % 21.89/7.42 | Applying alpha-rule on (173) yields: % 21.89/7.42 | (174) h(all_85_2_57) = all_85_1_56 % 21.89/7.42 | (175) h(all_30_2_10) = all_85_0_55 % 21.89/7.42 | (176) op2(all_60_0_25, all_85_0_55) = all_85_1_56 % 21.89/7.42 | (177) op1(all_30_2_10, all_30_2_10) = all_85_2_57 % 21.89/7.42 | % 21.89/7.42 | From (70) and (136) follows: % 21.89/7.42 | (178) op2(all_0_0_0, all_69_0_31) = all_69_1_32 % 21.89/7.42 | % 21.89/7.42 | From (70) and (107) follows: % 21.89/7.42 | (179) op2(all_0_0_0, all_56_0_19) = all_56_1_20 % 21.89/7.42 | % 21.89/7.42 | Instantiating formula (10) with all_0_0_0, all_77_0_43, all_8_0_1 and discharging atoms j(all_0_0_0) = all_77_0_43, j(all_0_0_0) = all_8_0_1, yields: % 21.89/7.42 | (180) all_77_0_43 = all_8_0_1 % 21.89/7.42 | % 21.89/7.42 | Instantiating formula (14) with all_30_2_10, all_69_0_31, all_85_0_55 and discharging atoms h(all_30_2_10) = all_85_0_55, h(all_30_2_10) = all_69_0_31, yields: % 21.89/7.42 | (181) all_85_0_55 = all_69_0_31 % 21.89/7.42 | % 21.89/7.42 | Instantiating formula (14) with all_30_2_10, all_67_0_30, all_75_0_40 and discharging atoms h(all_30_2_10) = all_75_0_40, h(all_30_2_10) = all_67_0_30, yields: % 21.89/7.42 | (182) all_75_0_40 = all_67_0_30 % 21.89/7.42 | % 21.89/7.42 | Instantiating formula (14) with all_30_2_10, all_67_0_30, all_69_0_31 and discharging atoms h(all_30_2_10) = all_69_0_31, h(all_30_2_10) = all_67_0_30, yields: % 21.89/7.42 | (183) all_69_0_31 = all_67_0_30 % 21.89/7.42 | % 21.89/7.42 | Instantiating formula (14) with all_30_2_10, all_63_0_26, all_85_0_55 and discharging atoms h(all_30_2_10) = all_85_0_55, h(all_30_2_10) = all_63_0_26, yields: % 21.89/7.42 | (184) all_85_0_55 = all_63_0_26 % 21.89/7.42 | % 21.89/7.42 | Instantiating formula (14) with all_30_2_10, all_60_0_25, all_75_0_40 and discharging atoms h(all_30_2_10) = all_75_0_40, h(all_30_2_10) = all_60_0_25, yields: % 21.89/7.42 | (185) all_75_0_40 = all_60_0_25 % 21.89/7.42 | % 21.89/7.42 | Instantiating formula (14) with all_15_1_5, all_73_0_37, all_15_2_6 and discharging atoms h(all_15_1_5) = all_73_0_37, h(all_15_1_5) = all_15_2_6, yields: % 21.89/7.42 | (186) all_73_0_37 = all_15_2_6 % 21.89/7.42 | % 21.89/7.42 | Instantiating formula (14) with all_15_1_5, all_56_0_19, all_83_0_52 and discharging atoms h(all_15_1_5) = all_83_0_52, h(all_15_1_5) = all_56_0_19, yields: % 21.89/7.42 | (187) all_83_0_52 = all_56_0_19 % 21.89/7.42 | % 21.89/7.42 | Instantiating formula (14) with all_15_1_5, all_56_0_19, all_73_0_37 and discharging atoms h(all_15_1_5) = all_73_0_37, h(all_15_1_5) = all_56_0_19, yields: % 21.89/7.42 | (188) all_73_0_37 = all_56_0_19 % 21.89/7.42 | % 21.89/7.42 | Instantiating formula (14) with all_15_1_5, all_48_0_14, all_83_0_52 and discharging atoms h(all_15_1_5) = all_83_0_52, h(all_15_1_5) = all_48_0_14, yields: % 21.89/7.42 | (189) all_83_0_52 = all_48_0_14 % 21.89/7.42 | % 21.89/7.42 | Instantiating formula (14) with all_8_0_1, all_81_0_49, all_0_0_0 and discharging atoms h(all_8_0_1) = all_81_0_49, h(all_8_0_1) = all_0_0_0, yields: % 21.89/7.42 | (190) all_81_0_49 = all_0_0_0 % 21.89/7.42 | % 21.89/7.42 | Instantiating formula (14) with all_8_0_1, all_71_0_34, all_81_0_49 and discharging atoms h(all_8_0_1) = all_81_0_49, h(all_8_0_1) = all_71_0_34, yields: % 21.89/7.42 | (191) all_81_0_49 = all_71_0_34 % 21.89/7.42 | % 21.89/7.42 | Instantiating formula (16) with all_30_2_10, all_8_0_1, all_81_2_51, all_30_1_9 and discharging atoms op1(all_30_2_10, all_8_0_1) = all_81_2_51, op1(all_30_2_10, all_8_0_1) = all_30_1_9, yields: % 21.89/7.43 | (192) all_81_2_51 = all_30_1_9 % 21.89/7.43 | % 21.89/7.43 | Combining equations (181,184) yields a new equation: % 21.89/7.43 | (193) all_69_0_31 = all_63_0_26 % 21.89/7.43 | % 21.89/7.43 | Simplifying 193 yields: % 21.89/7.43 | (194) all_69_0_31 = all_63_0_26 % 21.89/7.43 | % 21.89/7.43 | Combining equations (187,189) yields a new equation: % 21.89/7.43 | (195) all_56_0_19 = all_48_0_14 % 21.89/7.43 | % 21.89/7.43 | Simplifying 195 yields: % 21.89/7.43 | (196) all_56_0_19 = all_48_0_14 % 21.89/7.43 | % 21.89/7.43 | Combining equations (190,191) yields a new equation: % 21.89/7.43 | (197) all_71_0_34 = all_0_0_0 % 21.89/7.43 | % 21.89/7.43 | Combining equations (182,185) yields a new equation: % 21.89/7.43 | (198) all_67_0_30 = all_60_0_25 % 21.89/7.43 | % 21.89/7.43 | Simplifying 198 yields: % 21.89/7.43 | (199) all_67_0_30 = all_60_0_25 % 21.89/7.43 | % 21.89/7.43 | Combining equations (188,186) yields a new equation: % 21.89/7.43 | (200) all_56_0_19 = all_15_2_6 % 21.89/7.43 | % 21.89/7.43 | Simplifying 200 yields: % 21.89/7.43 | (201) all_56_0_19 = all_15_2_6 % 21.89/7.43 | % 21.89/7.43 | Combining equations (183,194) yields a new equation: % 21.89/7.43 | (202) all_67_0_30 = all_63_0_26 % 21.89/7.43 | % 21.89/7.43 | Simplifying 202 yields: % 21.89/7.43 | (203) all_67_0_30 = all_63_0_26 % 21.89/7.43 | % 21.89/7.43 | Combining equations (199,203) yields a new equation: % 21.89/7.43 | (204) all_63_0_26 = all_60_0_25 % 21.89/7.43 | % 21.89/7.43 | Combining equations (196,201) yields a new equation: % 21.89/7.43 | (205) all_48_0_14 = all_15_2_6 % 22.15/7.43 | % 22.15/7.43 | Simplifying 205 yields: % 22.15/7.43 | (206) all_48_0_14 = all_15_2_6 % 22.15/7.43 | % 22.15/7.43 | Combining equations (204,203) yields a new equation: % 22.15/7.43 | (199) all_67_0_30 = all_60_0_25 % 22.15/7.43 | % 22.15/7.43 | Combining equations (204,194) yields a new equation: % 22.15/7.43 | (208) all_69_0_31 = all_60_0_25 % 22.15/7.43 | % 22.15/7.43 | Combining equations (197,191) yields a new equation: % 22.15/7.43 | (190) all_81_0_49 = all_0_0_0 % 22.15/7.43 | % 22.15/7.43 | Combining equations (206,189) yields a new equation: % 22.15/7.43 | (210) all_83_0_52 = all_15_2_6 % 22.15/7.43 | % 22.15/7.43 | Combining equations (204,184) yields a new equation: % 22.15/7.43 | (211) all_85_0_55 = all_60_0_25 % 22.15/7.43 | % 22.15/7.43 | From (199) and (131) follows: % 22.15/7.43 | (212) j(all_60_0_25) = all_30_2_10 % 22.15/7.43 | % 22.15/7.43 | From (180) and (155) follows: % 22.15/7.43 | (22) j(all_0_0_0) = all_8_0_1 % 22.15/7.43 | % 22.15/7.43 | From (192) and (164) follows: % 22.15/7.43 | (214) h(all_30_1_9) = all_81_1_50 % 22.15/7.43 | % 22.15/7.43 | From (204) and (122) follows: % 22.15/7.43 | (116) h(all_30_2_10) = all_60_0_25 % 22.15/7.43 | % 22.15/7.43 | From (211) and (176) follows: % 22.15/7.43 | (216) op2(all_60_0_25, all_60_0_25) = all_85_1_56 % 22.15/7.43 | % 22.15/7.43 | From (210) and (171) follows: % 22.15/7.43 | (217) op2(all_60_0_25, all_15_2_6) = all_83_1_53 % 22.15/7.43 | % 22.15/7.43 | From (190) and (166) follows: % 22.15/7.43 | (218) op2(all_60_0_25, all_0_0_0) = all_81_1_50 % 22.15/7.43 | % 22.15/7.43 | From (206)(185) and (151) follows: % 22.15/7.43 | (219) op2(all_15_2_6, all_60_0_25) = all_75_1_41 % 22.15/7.43 | % 22.15/7.43 | From (206)(186) and (146) follows: % 22.15/7.43 | (220) op2(all_15_2_6, all_15_2_6) = all_73_1_38 % 22.15/7.43 | % 22.15/7.43 | From (206)(197) and (141) follows: % 22.15/7.43 | (221) op2(all_15_2_6, all_0_0_0) = all_71_1_35 % 22.15/7.43 | % 22.15/7.43 | From (208) and (178) follows: % 22.15/7.43 | (222) op2(all_0_0_0, all_60_0_25) = all_69_1_32 % 22.15/7.43 | % 22.15/7.43 | From (201) and (179) follows: % 22.15/7.43 | (223) op2(all_0_0_0, all_15_2_6) = all_56_1_20 % 22.15/7.43 | % 22.15/7.43 | From (192) and (167) follows: % 22.15/7.43 | (58) op1(all_30_2_10, all_8_0_1) = all_30_1_9 % 22.15/7.43 | % 22.15/7.43 | From (204) and (123) follows: % 22.15/7.43 | (225) sorti2(all_60_0_25) % 22.15/7.43 | % 22.15/7.43 | Instantiating formula (17) with all_15_2_6, all_15_2_6, all_73_1_38, all_79_2_48 and discharging atoms op2(all_15_2_6, all_15_2_6) = all_79_2_48, op2(all_15_2_6, all_15_2_6) = all_73_1_38, yields: % 22.15/7.43 | (226) all_79_2_48 = all_73_1_38 % 22.15/7.43 | % 22.15/7.43 | Instantiating formula (17) with all_15_2_6, all_0_0_0, all_71_1_35, all_77_2_45 and discharging atoms op2(all_15_2_6, all_0_0_0) = all_77_2_45, op2(all_15_2_6, all_0_0_0) = all_71_1_35, yields: % 22.15/7.43 | (227) all_77_2_45 = all_71_1_35 % 22.15/7.43 | % 22.15/7.43 | Instantiating formula (17) with all_0_0_0, all_15_2_6, all_56_1_20, all_54_2_18 and discharging atoms op2(all_0_0_0, all_15_2_6) = all_56_1_20, op2(all_0_0_0, all_15_2_6) = all_54_2_18, yields: % 22.15/7.43 | (228) all_56_1_20 = all_54_2_18 % 22.15/7.43 | % 22.15/7.43 | From (226) and (161) follows: % 22.15/7.43 | (220) op2(all_15_2_6, all_15_2_6) = all_73_1_38 % 22.15/7.43 | % 22.15/7.43 | From (227) and (156) follows: % 22.15/7.44 | (221) op2(all_15_2_6, all_0_0_0) = all_71_1_35 % 22.15/7.44 | % 22.15/7.44 | From (228) and (223) follows: % 22.15/7.44 | (102) op2(all_0_0_0, all_15_2_6) = all_54_2_18 % 22.15/7.44 | % 22.15/7.44 | Instantiating formula (8) with all_73_1_38, all_15_2_6, all_15_2_6 and discharging atoms op2(all_15_2_6, all_15_2_6) = all_73_1_38, sorti2(all_15_2_6), yields: % 22.15/7.44 | (232) sorti2(all_73_1_38) % 22.15/7.44 | % 22.15/7.44 | Instantiating formula (8) with all_71_1_35, all_0_0_0, all_15_2_6 and discharging atoms op2(all_15_2_6, all_0_0_0) = all_71_1_35, sorti2(all_15_2_6), sorti2(all_0_0_0), yields: % 22.15/7.44 | (233) sorti2(all_71_1_35) % 22.15/7.44 | % 22.15/7.44 | Instantiating formula (8) with all_54_2_18, all_15_2_6, all_0_0_0 and discharging atoms op2(all_0_0_0, all_15_2_6) = all_54_2_18, sorti2(all_15_2_6), sorti2(all_0_0_0), yields: % 22.15/7.44 | (234) sorti2(all_54_2_18) % 22.15/7.44 | % 22.15/7.44 | Instantiating formula (8) with all_85_1_56, all_60_0_25, all_60_0_25 and discharging atoms op2(all_60_0_25, all_60_0_25) = all_85_1_56, sorti2(all_60_0_25), yields: % 22.15/7.44 | (235) sorti2(all_85_1_56) % 22.15/7.44 | % 22.15/7.44 | Instantiating formula (8) with all_83_1_53, all_15_2_6, all_60_0_25 and discharging atoms op2(all_60_0_25, all_15_2_6) = all_83_1_53, sorti2(all_60_0_25), sorti2(all_15_2_6), yields: % 22.15/7.44 | (236) sorti2(all_83_1_53) % 22.15/7.44 | % 22.15/7.44 | Instantiating formula (8) with all_75_1_41, all_60_0_25, all_15_2_6 and discharging atoms op2(all_15_2_6, all_60_0_25) = all_75_1_41, sorti2(all_60_0_25), sorti2(all_15_2_6), yields: % 22.15/7.44 | (237) sorti2(all_75_1_41) % 22.15/7.44 | % 22.15/7.44 | Instantiating formula (8) with all_69_1_32, all_60_0_25, all_0_0_0 and discharging atoms op2(all_0_0_0, all_60_0_25) = all_69_1_32, sorti2(all_60_0_25), sorti2(all_0_0_0), yields: % 22.15/7.44 | (238) sorti2(all_69_1_32) % 22.15/7.44 | % 22.15/7.44 | Instantiating formula (96) with all_60_0_25 and discharging atoms sorti2(all_60_0_25), yields: % 22.15/7.44 | (239) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_60_0_25) = v2 & op2(all_15_2_6, all_60_0_25) = v0 & op1(all_51_0_15, v2) = v1) % 22.15/7.44 | % 22.15/7.44 | Instantiating formula (23) with all_60_0_25 and discharging atoms sorti2(all_60_0_25), yields: % 22.15/7.44 | (240) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_60_0_25) = v2 & op2(all_0_0_0, all_60_0_25) = v0 & op1(all_8_0_1, v2) = v1) % 22.15/7.44 | % 22.15/7.44 | Instantiating formula (5) with all_60_0_25 and discharging atoms sorti2(all_60_0_25), yields: % 22.15/7.44 | (241) ? [v0] : (j(all_60_0_25) = v0 & ! [v1] : ( ~ sorti2(v1) | ? [v2] : ? [v3] : ? [v4] : (j(v2) = v3 & j(v1) = v4 & op2(all_60_0_25, v1) = v2 & op1(v0, v4) = v3))) % 22.15/7.44 | % 22.15/7.44 | Instantiating formula (117) with all_65_2_29 and discharging atoms sorti1(all_65_2_29), yields: % 22.15/7.44 | (242) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_65_2_29) = v2 & op2(all_60_0_25, v2) = v1 & op1(all_30_2_10, all_65_2_29) = v0) % 22.15/7.44 | % 22.15/7.44 | Instantiating formula (90) with all_65_2_29 and discharging atoms sorti1(all_65_2_29), yields: % 22.15/7.44 | (243) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_65_2_29) = v2 & op2(all_48_0_14, v2) = v1 & op1(all_15_1_5, all_65_2_29) = v0) % 22.15/7.44 | % 22.15/7.44 | Instantiating formula (54) with all_65_2_29 and discharging atoms sorti1(all_65_2_29), yields: % 22.15/7.44 | (244) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_65_2_29) = v2 & op2(all_27_0_7, v2) = v1 & op1(all_8_0_1, all_65_2_29) = v0) % 22.15/7.44 | % 22.15/7.44 | Instantiating formula (7) with all_65_2_29 and discharging atoms sorti1(all_65_2_29), yields: % 22.15/7.44 | (245) ? [v0] : (j(v0) = all_65_2_29 & h(all_65_2_29) = v0) % 22.15/7.44 | % 22.15/7.44 | Instantiating formula (4) with all_65_2_29 and discharging atoms sorti1(all_65_2_29), yields: % 22.15/7.44 | (246) ? [v0] : (h(all_65_2_29) = v0 & sorti2(v0)) % 22.15/7.44 | % 22.15/7.44 | Instantiating formula (6) with all_65_2_29 and discharging atoms sorti1(all_65_2_29), yields: % 22.15/7.44 | (247) ? [v0] : (h(all_65_2_29) = v0 & ! [v1] : ( ~ sorti1(v1) | ? [v2] : ? [v3] : ? [v4] : (h(v2) = v3 & h(v1) = v4 & op2(v0, v4) = v3 & op1(all_65_2_29, v1) = v2))) % 22.15/7.44 | % 22.15/7.44 | Instantiating formula (117) with all_58_2_24 and discharging atoms sorti1(all_58_2_24), yields: % 22.15/7.44 | (248) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_58_2_24) = v2 & op2(all_60_0_25, v2) = v1 & op1(all_30_2_10, all_58_2_24) = v0) % 22.15/7.44 | % 22.15/7.44 | Instantiating formula (7) with all_58_2_24 and discharging atoms sorti1(all_58_2_24), yields: % 22.15/7.44 | (249) ? [v0] : (j(v0) = all_58_2_24 & h(all_58_2_24) = v0) % 22.15/7.44 | % 22.15/7.44 | Instantiating formula (4) with all_58_2_24 and discharging atoms sorti1(all_58_2_24), yields: % 22.15/7.44 | (250) ? [v0] : (h(all_58_2_24) = v0 & sorti2(v0)) % 22.15/7.44 | % 22.15/7.44 | Instantiating formula (6) with all_58_2_24 and discharging atoms sorti1(all_58_2_24), yields: % 22.15/7.44 | (251) ? [v0] : (h(all_58_2_24) = v0 & ! [v1] : ( ~ sorti1(v1) | ? [v2] : ? [v3] : ? [v4] : (h(v2) = v3 & h(v1) = v4 & op2(v0, v4) = v3 & op1(all_58_2_24, v1) = v2))) % 22.15/7.44 | % 22.15/7.44 | Instantiating formula (117) with all_30_1_9 and discharging atoms sorti1(all_30_1_9), yields: % 22.15/7.44 | (252) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_30_1_9) = v2 & op2(all_60_0_25, v2) = v1 & op1(all_30_2_10, all_30_1_9) = v0) % 22.15/7.44 | % 22.15/7.44 | Instantiating formula (90) with all_30_1_9 and discharging atoms sorti1(all_30_1_9), yields: % 22.15/7.45 | (253) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_30_1_9) = v2 & op2(all_48_0_14, v2) = v1 & op1(all_15_1_5, all_30_1_9) = v0) % 22.15/7.45 | % 22.15/7.45 | Instantiating formula (54) with all_30_1_9 and discharging atoms sorti1(all_30_1_9), yields: % 22.15/7.45 | (254) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_30_1_9) = v2 & op2(all_27_0_7, v2) = v1 & op1(all_8_0_1, all_30_1_9) = v0) % 22.15/7.45 | % 22.15/7.45 | Instantiating formula (7) with all_30_1_9 and discharging atoms sorti1(all_30_1_9), yields: % 22.15/7.45 | (255) ? [v0] : (j(v0) = all_30_1_9 & h(all_30_1_9) = v0) % 22.15/7.45 | % 22.15/7.45 | Instantiating formula (4) with all_30_1_9 and discharging atoms sorti1(all_30_1_9), yields: % 22.15/7.45 | (256) ? [v0] : (h(all_30_1_9) = v0 & sorti2(v0)) % 22.15/7.45 | % 22.15/7.45 | Instantiating formula (6) with all_30_1_9 and discharging atoms sorti1(all_30_1_9), yields: % 22.15/7.45 | (257) ? [v0] : (h(all_30_1_9) = v0 & ! [v1] : ( ~ sorti1(v1) | ? [v2] : ? [v3] : ? [v4] : (h(v2) = v3 & h(v1) = v4 & op2(v0, v4) = v3 & op1(all_30_1_9, v1) = v2))) % 22.15/7.45 | % 22.15/7.45 | Instantiating (249) with all_101_0_58 yields: % 22.15/7.45 | (258) j(all_101_0_58) = all_58_2_24 & h(all_58_2_24) = all_101_0_58 % 22.15/7.45 | % 22.15/7.45 | Applying alpha-rule on (258) yields: % 22.15/7.45 | (259) j(all_101_0_58) = all_58_2_24 % 22.15/7.45 | (260) h(all_58_2_24) = all_101_0_58 % 22.15/7.45 | % 22.15/7.45 | Instantiating (248) with all_105_0_62, all_105_1_63, all_105_2_64 yields: % 22.15/7.45 | (261) h(all_105_2_64) = all_105_1_63 & h(all_58_2_24) = all_105_0_62 & op2(all_60_0_25, all_105_0_62) = all_105_1_63 & op1(all_30_2_10, all_58_2_24) = all_105_2_64 % 22.15/7.45 | % 22.15/7.45 | Applying alpha-rule on (261) yields: % 22.15/7.45 | (262) h(all_105_2_64) = all_105_1_63 % 22.15/7.45 | (263) h(all_58_2_24) = all_105_0_62 % 22.15/7.45 | (264) op2(all_60_0_25, all_105_0_62) = all_105_1_63 % 22.15/7.45 | (265) op1(all_30_2_10, all_58_2_24) = all_105_2_64 % 22.15/7.45 | % 22.15/7.45 | Instantiating (247) with all_107_0_65 yields: % 22.15/7.45 | (266) h(all_65_2_29) = all_107_0_65 & ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_107_0_65, v3) = v2 & op1(all_65_2_29, v0) = v1)) % 22.26/7.45 | % 22.26/7.45 | Applying alpha-rule on (266) yields: % 22.26/7.45 | (267) h(all_65_2_29) = all_107_0_65 % 22.26/7.45 | (268) ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_107_0_65, v3) = v2 & op1(all_65_2_29, v0) = v1)) % 22.26/7.45 | % 22.26/7.45 | Instantiating formula (268) with all_65_2_29 and discharging atoms sorti1(all_65_2_29), yields: % 22.26/7.45 | (269) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_65_2_29) = v2 & op2(all_107_0_65, v2) = v1 & op1(all_65_2_29, all_65_2_29) = v0) % 22.26/7.45 | % 22.26/7.45 | Instantiating formula (268) with all_30_1_9 and discharging atoms sorti1(all_30_1_9), yields: % 22.26/7.45 | (270) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_30_1_9) = v2 & op2(all_107_0_65, v2) = v1 & op1(all_65_2_29, all_30_1_9) = v0) % 22.26/7.45 | % 22.26/7.45 | Instantiating formula (268) with all_30_2_10 and discharging atoms sorti1(all_30_2_10), yields: % 22.26/7.45 | (271) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_30_2_10) = v2 & op2(all_107_0_65, v2) = v1 & op1(all_65_2_29, all_30_2_10) = v0) % 22.26/7.45 | % 22.26/7.45 | Instantiating (241) with all_110_0_66 yields: % 22.26/7.45 | (272) j(all_60_0_25) = all_110_0_66 & ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_60_0_25, v0) = v1 & op1(all_110_0_66, v3) = v2)) % 22.26/7.45 | % 22.26/7.45 | Applying alpha-rule on (272) yields: % 22.26/7.45 | (273) j(all_60_0_25) = all_110_0_66 % 22.26/7.45 | (274) ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_60_0_25, v0) = v1 & op1(all_110_0_66, v3) = v2)) % 22.26/7.45 | % 22.26/7.45 | Instantiating formula (274) with all_60_0_25 and discharging atoms sorti2(all_60_0_25), yields: % 22.26/7.45 | (275) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_60_0_25) = v2 & op2(all_60_0_25, all_60_0_25) = v0 & op1(all_110_0_66, v2) = v1) % 22.26/7.45 | % 22.26/7.45 | Instantiating formula (274) with all_0_0_0 and discharging atoms sorti2(all_0_0_0), yields: % 22.26/7.45 | (276) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_0_0) = v2 & op2(all_60_0_25, all_0_0_0) = v0 & op1(all_110_0_66, v2) = v1) % 22.26/7.45 | % 22.26/7.45 | Instantiating (240) with all_113_0_67, all_113_1_68, all_113_2_69 yields: % 22.26/7.45 | (277) j(all_113_2_69) = all_113_1_68 & j(all_60_0_25) = all_113_0_67 & op2(all_0_0_0, all_60_0_25) = all_113_2_69 & op1(all_8_0_1, all_113_0_67) = all_113_1_68 % 22.26/7.45 | % 22.26/7.45 | Applying alpha-rule on (277) yields: % 22.26/7.45 | (278) j(all_113_2_69) = all_113_1_68 % 22.26/7.46 | (279) j(all_60_0_25) = all_113_0_67 % 22.26/7.46 | (280) op2(all_0_0_0, all_60_0_25) = all_113_2_69 % 22.26/7.46 | (281) op1(all_8_0_1, all_113_0_67) = all_113_1_68 % 22.26/7.46 | % 22.26/7.46 | Instantiating (246) with all_115_0_70 yields: % 22.26/7.46 | (282) h(all_65_2_29) = all_115_0_70 & sorti2(all_115_0_70) % 22.26/7.46 | % 22.26/7.46 | Applying alpha-rule on (282) yields: % 22.26/7.46 | (283) h(all_65_2_29) = all_115_0_70 % 22.26/7.46 | (284) sorti2(all_115_0_70) % 22.26/7.46 | % 22.26/7.46 | Instantiating (239) with all_117_0_71, all_117_1_72, all_117_2_73 yields: % 22.26/7.46 | (285) j(all_117_2_73) = all_117_1_72 & j(all_60_0_25) = all_117_0_71 & op2(all_15_2_6, all_60_0_25) = all_117_2_73 & op1(all_51_0_15, all_117_0_71) = all_117_1_72 % 22.26/7.46 | % 22.26/7.46 | Applying alpha-rule on (285) yields: % 22.26/7.46 | (286) j(all_117_2_73) = all_117_1_72 % 22.26/7.46 | (287) j(all_60_0_25) = all_117_0_71 % 22.26/7.46 | (288) op2(all_15_2_6, all_60_0_25) = all_117_2_73 % 22.26/7.46 | (289) op1(all_51_0_15, all_117_0_71) = all_117_1_72 % 22.26/7.46 | % 22.26/7.46 | Instantiating (257) with all_121_0_77 yields: % 22.26/7.46 | (290) h(all_30_1_9) = all_121_0_77 & ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_121_0_77, v3) = v2 & op1(all_30_1_9, v0) = v1)) % 22.26/7.46 | % 22.26/7.46 | Applying alpha-rule on (290) yields: % 22.26/7.46 | (291) h(all_30_1_9) = all_121_0_77 % 22.26/7.46 | (292) ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_121_0_77, v3) = v2 & op1(all_30_1_9, v0) = v1)) % 22.26/7.46 | % 22.26/7.46 | Instantiating formula (292) with all_65_2_29 and discharging atoms sorti1(all_65_2_29), yields: % 22.26/7.46 | (293) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_65_2_29) = v2 & op2(all_121_0_77, v2) = v1 & op1(all_30_1_9, all_65_2_29) = v0) % 22.26/7.46 | % 22.26/7.46 | Instantiating formula (292) with all_30_1_9 and discharging atoms sorti1(all_30_1_9), yields: % 22.26/7.46 | (294) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_30_1_9) = v2 & op2(all_121_0_77, v2) = v1 & op1(all_30_1_9, all_30_1_9) = v0) % 22.26/7.46 | % 22.26/7.46 | Instantiating formula (292) with all_30_2_10 and discharging atoms sorti1(all_30_2_10), yields: % 22.26/7.46 | (295) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_30_2_10) = v2 & op2(all_121_0_77, v2) = v1 & op1(all_30_1_9, all_30_2_10) = v0) % 22.26/7.46 | % 22.26/7.46 | Instantiating (251) with all_124_0_78 yields: % 22.26/7.46 | (296) h(all_58_2_24) = all_124_0_78 & ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_124_0_78, v3) = v2 & op1(all_58_2_24, v0) = v1)) % 22.26/7.46 | % 22.26/7.46 | Applying alpha-rule on (296) yields: % 22.26/7.46 | (297) h(all_58_2_24) = all_124_0_78 % 22.26/7.46 | (298) ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_124_0_78, v3) = v2 & op1(all_58_2_24, v0) = v1)) % 22.26/7.46 | % 22.26/7.46 | Instantiating formula (298) with all_65_2_29 and discharging atoms sorti1(all_65_2_29), yields: % 22.26/7.46 | (299) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_65_2_29) = v2 & op2(all_124_0_78, v2) = v1 & op1(all_58_2_24, all_65_2_29) = v0) % 22.26/7.46 | % 22.26/7.46 | Instantiating formula (298) with all_30_1_9 and discharging atoms sorti1(all_30_1_9), yields: % 22.26/7.46 | (300) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_30_1_9) = v2 & op2(all_124_0_78, v2) = v1 & op1(all_58_2_24, all_30_1_9) = v0) % 22.26/7.46 | % 22.26/7.46 | Instantiating formula (298) with all_30_2_10 and discharging atoms sorti1(all_30_2_10), yields: % 22.26/7.46 | (301) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_30_2_10) = v2 & op2(all_124_0_78, v2) = v1 & op1(all_58_2_24, all_30_2_10) = v0) % 22.26/7.46 | % 22.26/7.46 | Instantiating (250) with all_127_0_79 yields: % 22.26/7.46 | (302) h(all_58_2_24) = all_127_0_79 & sorti2(all_127_0_79) % 22.26/7.46 | % 22.26/7.46 | Applying alpha-rule on (302) yields: % 22.26/7.46 | (303) h(all_58_2_24) = all_127_0_79 % 22.26/7.46 | (304) sorti2(all_127_0_79) % 22.26/7.46 | % 22.26/7.46 | Instantiating (256) with all_129_0_80 yields: % 22.26/7.46 | (305) h(all_30_1_9) = all_129_0_80 & sorti2(all_129_0_80) % 22.26/7.46 | % 22.26/7.46 | Applying alpha-rule on (305) yields: % 22.26/7.46 | (306) h(all_30_1_9) = all_129_0_80 % 22.26/7.46 | (307) sorti2(all_129_0_80) % 22.26/7.46 | % 22.26/7.46 | Instantiating (255) with all_133_0_84 yields: % 22.26/7.46 | (308) j(all_133_0_84) = all_30_1_9 & h(all_30_1_9) = all_133_0_84 % 22.26/7.46 | % 22.26/7.47 | Applying alpha-rule on (308) yields: % 22.26/7.47 | (309) j(all_133_0_84) = all_30_1_9 % 22.26/7.47 | (310) h(all_30_1_9) = all_133_0_84 % 22.26/7.47 | % 22.26/7.47 | Instantiating (254) with all_135_0_85, all_135_1_86, all_135_2_87 yields: % 22.26/7.47 | (311) h(all_135_2_87) = all_135_1_86 & h(all_30_1_9) = all_135_0_85 & op2(all_27_0_7, all_135_0_85) = all_135_1_86 & op1(all_8_0_1, all_30_1_9) = all_135_2_87 % 22.26/7.47 | % 22.26/7.47 | Applying alpha-rule on (311) yields: % 22.26/7.47 | (312) h(all_135_2_87) = all_135_1_86 % 22.26/7.47 | (313) h(all_30_1_9) = all_135_0_85 % 22.26/7.47 | (314) op2(all_27_0_7, all_135_0_85) = all_135_1_86 % 22.26/7.47 | (315) op1(all_8_0_1, all_30_1_9) = all_135_2_87 % 22.26/7.47 | % 22.26/7.47 | Instantiating (253) with all_139_0_91, all_139_1_92, all_139_2_93 yields: % 22.26/7.47 | (316) h(all_139_2_93) = all_139_1_92 & h(all_30_1_9) = all_139_0_91 & op2(all_48_0_14, all_139_0_91) = all_139_1_92 & op1(all_15_1_5, all_30_1_9) = all_139_2_93 % 22.26/7.47 | % 22.26/7.47 | Applying alpha-rule on (316) yields: % 22.26/7.47 | (317) h(all_139_2_93) = all_139_1_92 % 22.26/7.47 | (318) h(all_30_1_9) = all_139_0_91 % 22.26/7.47 | (319) op2(all_48_0_14, all_139_0_91) = all_139_1_92 % 22.26/7.47 | (320) op1(all_15_1_5, all_30_1_9) = all_139_2_93 % 22.26/7.47 | % 22.26/7.47 | Instantiating (245) with all_141_0_94 yields: % 22.26/7.47 | (321) j(all_141_0_94) = all_65_2_29 & h(all_65_2_29) = all_141_0_94 % 22.26/7.47 | % 22.26/7.47 | Applying alpha-rule on (321) yields: % 22.26/7.47 | (322) j(all_141_0_94) = all_65_2_29 % 22.26/7.47 | (323) h(all_65_2_29) = all_141_0_94 % 22.26/7.47 | % 22.26/7.47 | Instantiating (243) with all_143_0_95, all_143_1_96, all_143_2_97 yields: % 22.26/7.47 | (324) h(all_143_2_97) = all_143_1_96 & h(all_65_2_29) = all_143_0_95 & op2(all_48_0_14, all_143_0_95) = all_143_1_96 & op1(all_15_1_5, all_65_2_29) = all_143_2_97 % 22.26/7.47 | % 22.26/7.47 | Applying alpha-rule on (324) yields: % 22.26/7.47 | (325) h(all_143_2_97) = all_143_1_96 % 22.26/7.47 | (326) h(all_65_2_29) = all_143_0_95 % 22.26/7.47 | (327) op2(all_48_0_14, all_143_0_95) = all_143_1_96 % 22.26/7.47 | (328) op1(all_15_1_5, all_65_2_29) = all_143_2_97 % 22.26/7.47 | % 22.26/7.47 | Instantiating (242) with all_145_0_98, all_145_1_99, all_145_2_100 yields: % 22.26/7.47 | (329) h(all_145_2_100) = all_145_1_99 & h(all_65_2_29) = all_145_0_98 & op2(all_60_0_25, all_145_0_98) = all_145_1_99 & op1(all_30_2_10, all_65_2_29) = all_145_2_100 % 22.26/7.47 | % 22.26/7.47 | Applying alpha-rule on (329) yields: % 22.26/7.47 | (330) h(all_145_2_100) = all_145_1_99 % 22.26/7.47 | (331) h(all_65_2_29) = all_145_0_98 % 22.26/7.47 | (332) op2(all_60_0_25, all_145_0_98) = all_145_1_99 % 22.26/7.47 | (333) op1(all_30_2_10, all_65_2_29) = all_145_2_100 % 22.26/7.47 | % 22.26/7.47 | Instantiating (252) with all_147_0_101, all_147_1_102, all_147_2_103 yields: % 22.26/7.47 | (334) h(all_147_2_103) = all_147_1_102 & h(all_30_1_9) = all_147_0_101 & op2(all_60_0_25, all_147_0_101) = all_147_1_102 & op1(all_30_2_10, all_30_1_9) = all_147_2_103 % 22.26/7.47 | % 22.26/7.47 | Applying alpha-rule on (334) yields: % 22.26/7.47 | (335) h(all_147_2_103) = all_147_1_102 % 22.26/7.47 | (336) h(all_30_1_9) = all_147_0_101 % 22.26/7.47 | (337) op2(all_60_0_25, all_147_0_101) = all_147_1_102 % 22.26/7.47 | (338) op1(all_30_2_10, all_30_1_9) = all_147_2_103 % 22.26/7.47 | % 22.26/7.48 | Instantiating (244) with all_149_0_104, all_149_1_105, all_149_2_106 yields: % 22.26/7.48 | (339) h(all_149_2_106) = all_149_1_105 & h(all_65_2_29) = all_149_0_104 & op2(all_27_0_7, all_149_0_104) = all_149_1_105 & op1(all_8_0_1, all_65_2_29) = all_149_2_106 % 22.26/7.48 | % 22.26/7.48 | Applying alpha-rule on (339) yields: % 22.26/7.48 | (340) h(all_149_2_106) = all_149_1_105 % 22.26/7.48 | (341) h(all_65_2_29) = all_149_0_104 % 22.26/7.48 | (342) op2(all_27_0_7, all_149_0_104) = all_149_1_105 % 22.26/7.48 | (343) op1(all_8_0_1, all_65_2_29) = all_149_2_106 % 22.26/7.48 | % 22.26/7.48 | Instantiating (271) with all_155_0_113, all_155_1_114, all_155_2_115 yields: % 22.26/7.48 | (344) h(all_155_2_115) = all_155_1_114 & h(all_30_2_10) = all_155_0_113 & op2(all_107_0_65, all_155_0_113) = all_155_1_114 & op1(all_65_2_29, all_30_2_10) = all_155_2_115 % 22.26/7.48 | % 22.26/7.48 | Applying alpha-rule on (344) yields: % 22.26/7.48 | (345) h(all_155_2_115) = all_155_1_114 % 22.26/7.48 | (346) h(all_30_2_10) = all_155_0_113 % 22.26/7.48 | (347) op2(all_107_0_65, all_155_0_113) = all_155_1_114 % 22.26/7.48 | (348) op1(all_65_2_29, all_30_2_10) = all_155_2_115 % 22.26/7.48 | % 22.26/7.48 | Instantiating (269) with all_161_0_122, all_161_1_123, all_161_2_124 yields: % 22.26/7.48 | (349) h(all_161_2_124) = all_161_1_123 & h(all_65_2_29) = all_161_0_122 & op2(all_107_0_65, all_161_0_122) = all_161_1_123 & op1(all_65_2_29, all_65_2_29) = all_161_2_124 % 22.26/7.48 | % 22.26/7.48 | Applying alpha-rule on (349) yields: % 22.26/7.48 | (350) h(all_161_2_124) = all_161_1_123 % 22.26/7.48 | (351) h(all_65_2_29) = all_161_0_122 % 22.26/7.48 | (352) op2(all_107_0_65, all_161_0_122) = all_161_1_123 % 22.26/7.48 | (353) op1(all_65_2_29, all_65_2_29) = all_161_2_124 % 22.26/7.48 | % 22.26/7.48 | Instantiating (270) with all_163_0_125, all_163_1_126, all_163_2_127 yields: % 22.26/7.48 | (354) h(all_163_2_127) = all_163_1_126 & h(all_30_1_9) = all_163_0_125 & op2(all_107_0_65, all_163_0_125) = all_163_1_126 & op1(all_65_2_29, all_30_1_9) = all_163_2_127 % 22.26/7.48 | % 22.26/7.48 | Applying alpha-rule on (354) yields: % 22.26/7.48 | (355) h(all_163_2_127) = all_163_1_126 % 22.26/7.48 | (356) h(all_30_1_9) = all_163_0_125 % 22.26/7.48 | (357) op2(all_107_0_65, all_163_0_125) = all_163_1_126 % 22.26/7.48 | (358) op1(all_65_2_29, all_30_1_9) = all_163_2_127 % 22.26/7.48 | % 22.26/7.48 | Instantiating (276) with all_165_0_128, all_165_1_129, all_165_2_130 yields: % 22.26/7.48 | (359) j(all_165_2_130) = all_165_1_129 & j(all_0_0_0) = all_165_0_128 & op2(all_60_0_25, all_0_0_0) = all_165_2_130 & op1(all_110_0_66, all_165_0_128) = all_165_1_129 % 22.26/7.48 | % 22.26/7.48 | Applying alpha-rule on (359) yields: % 22.26/7.48 | (360) j(all_165_2_130) = all_165_1_129 % 22.26/7.48 | (361) j(all_0_0_0) = all_165_0_128 % 22.26/7.48 | (362) op2(all_60_0_25, all_0_0_0) = all_165_2_130 % 22.26/7.48 | (363) op1(all_110_0_66, all_165_0_128) = all_165_1_129 % 22.26/7.48 | % 22.26/7.48 | Instantiating (275) with all_169_0_134, all_169_1_135, all_169_2_136 yields: % 22.26/7.48 | (364) j(all_169_2_136) = all_169_1_135 & j(all_60_0_25) = all_169_0_134 & op2(all_60_0_25, all_60_0_25) = all_169_2_136 & op1(all_110_0_66, all_169_0_134) = all_169_1_135 % 22.26/7.48 | % 22.26/7.48 | Applying alpha-rule on (364) yields: % 22.26/7.48 | (365) j(all_169_2_136) = all_169_1_135 % 22.26/7.48 | (366) j(all_60_0_25) = all_169_0_134 % 22.26/7.48 | (367) op2(all_60_0_25, all_60_0_25) = all_169_2_136 % 22.26/7.48 | (368) op1(all_110_0_66, all_169_0_134) = all_169_1_135 % 22.26/7.48 | % 22.26/7.48 | Instantiating (295) with all_175_0_143, all_175_1_144, all_175_2_145 yields: % 22.26/7.48 | (369) h(all_175_2_145) = all_175_1_144 & h(all_30_2_10) = all_175_0_143 & op2(all_121_0_77, all_175_0_143) = all_175_1_144 & op1(all_30_1_9, all_30_2_10) = all_175_2_145 % 22.26/7.48 | % 22.26/7.48 | Applying alpha-rule on (369) yields: % 22.26/7.48 | (370) h(all_175_2_145) = all_175_1_144 % 22.26/7.48 | (371) h(all_30_2_10) = all_175_0_143 % 22.26/7.48 | (372) op2(all_121_0_77, all_175_0_143) = all_175_1_144 % 22.26/7.48 | (373) op1(all_30_1_9, all_30_2_10) = all_175_2_145 % 22.26/7.48 | % 22.26/7.48 | Instantiating (293) with all_179_0_149, all_179_1_150, all_179_2_151 yields: % 22.26/7.48 | (374) h(all_179_2_151) = all_179_1_150 & h(all_65_2_29) = all_179_0_149 & op2(all_121_0_77, all_179_0_149) = all_179_1_150 & op1(all_30_1_9, all_65_2_29) = all_179_2_151 % 22.26/7.48 | % 22.26/7.48 | Applying alpha-rule on (374) yields: % 22.26/7.48 | (375) h(all_179_2_151) = all_179_1_150 % 22.26/7.48 | (376) h(all_65_2_29) = all_179_0_149 % 22.26/7.48 | (377) op2(all_121_0_77, all_179_0_149) = all_179_1_150 % 22.26/7.48 | (378) op1(all_30_1_9, all_65_2_29) = all_179_2_151 % 22.26/7.48 | % 22.26/7.48 | Instantiating (294) with all_181_0_152, all_181_1_153, all_181_2_154 yields: % 22.26/7.48 | (379) h(all_181_2_154) = all_181_1_153 & h(all_30_1_9) = all_181_0_152 & op2(all_121_0_77, all_181_0_152) = all_181_1_153 & op1(all_30_1_9, all_30_1_9) = all_181_2_154 % 22.26/7.48 | % 22.26/7.48 | Applying alpha-rule on (379) yields: % 22.26/7.48 | (380) h(all_181_2_154) = all_181_1_153 % 22.26/7.49 | (381) h(all_30_1_9) = all_181_0_152 % 22.26/7.49 | (382) op2(all_121_0_77, all_181_0_152) = all_181_1_153 % 22.26/7.49 | (383) op1(all_30_1_9, all_30_1_9) = all_181_2_154 % 22.26/7.49 | % 22.26/7.49 | Instantiating (301) with all_185_0_158, all_185_1_159, all_185_2_160 yields: % 22.26/7.49 | (384) h(all_185_2_160) = all_185_1_159 & h(all_30_2_10) = all_185_0_158 & op2(all_124_0_78, all_185_0_158) = all_185_1_159 & op1(all_58_2_24, all_30_2_10) = all_185_2_160 % 22.26/7.49 | % 22.26/7.49 | Applying alpha-rule on (384) yields: % 22.26/7.49 | (385) h(all_185_2_160) = all_185_1_159 % 22.26/7.49 | (386) h(all_30_2_10) = all_185_0_158 % 22.26/7.49 | (387) op2(all_124_0_78, all_185_0_158) = all_185_1_159 % 22.26/7.49 | (388) op1(all_58_2_24, all_30_2_10) = all_185_2_160 % 22.26/7.49 | % 22.26/7.49 | Instantiating (300) with all_187_0_161, all_187_1_162, all_187_2_163 yields: % 22.26/7.49 | (389) h(all_187_2_163) = all_187_1_162 & h(all_30_1_9) = all_187_0_161 & op2(all_124_0_78, all_187_0_161) = all_187_1_162 & op1(all_58_2_24, all_30_1_9) = all_187_2_163 % 22.26/7.49 | % 22.26/7.49 | Applying alpha-rule on (389) yields: % 22.26/7.49 | (390) h(all_187_2_163) = all_187_1_162 % 22.26/7.49 | (391) h(all_30_1_9) = all_187_0_161 % 22.26/7.49 | (392) op2(all_124_0_78, all_187_0_161) = all_187_1_162 % 22.26/7.49 | (393) op1(all_58_2_24, all_30_1_9) = all_187_2_163 % 22.26/7.49 | % 22.26/7.49 | Instantiating (299) with all_193_0_170, all_193_1_171, all_193_2_172 yields: % 22.26/7.49 | (394) h(all_193_2_172) = all_193_1_171 & h(all_65_2_29) = all_193_0_170 & op2(all_124_0_78, all_193_0_170) = all_193_1_171 & op1(all_58_2_24, all_65_2_29) = all_193_2_172 % 22.26/7.49 | % 22.26/7.49 | Applying alpha-rule on (394) yields: % 22.26/7.49 | (395) h(all_193_2_172) = all_193_1_171 % 22.26/7.49 | (396) h(all_65_2_29) = all_193_0_170 % 22.26/7.49 | (397) op2(all_124_0_78, all_193_0_170) = all_193_1_171 % 22.26/7.49 | (398) op1(all_58_2_24, all_65_2_29) = all_193_2_172 % 22.26/7.49 | % 22.26/7.49 | From (70) and (314) follows: % 22.26/7.49 | (399) op2(all_0_0_0, all_135_0_85) = all_135_1_86 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (10) with all_60_0_25, all_117_0_71, all_169_0_134 and discharging atoms j(all_60_0_25) = all_169_0_134, j(all_60_0_25) = all_117_0_71, yields: % 22.26/7.49 | (400) all_169_0_134 = all_117_0_71 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (10) with all_60_0_25, all_113_0_67, all_30_2_10 and discharging atoms j(all_60_0_25) = all_113_0_67, j(all_60_0_25) = all_30_2_10, yields: % 22.26/7.49 | (401) all_113_0_67 = all_30_2_10 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (10) with all_60_0_25, all_113_0_67, all_117_0_71 and discharging atoms j(all_60_0_25) = all_117_0_71, j(all_60_0_25) = all_113_0_67, yields: % 22.26/7.49 | (402) all_117_0_71 = all_113_0_67 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (10) with all_60_0_25, all_110_0_66, all_169_0_134 and discharging atoms j(all_60_0_25) = all_169_0_134, j(all_60_0_25) = all_110_0_66, yields: % 22.26/7.49 | (403) all_169_0_134 = all_110_0_66 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (10) with all_0_0_0, all_165_0_128, all_8_0_1 and discharging atoms j(all_0_0_0) = all_165_0_128, j(all_0_0_0) = all_8_0_1, yields: % 22.26/7.49 | (404) all_165_0_128 = all_8_0_1 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (14) with all_65_2_29, all_161_0_122, all_179_0_149 and discharging atoms h(all_65_2_29) = all_179_0_149, h(all_65_2_29) = all_161_0_122, yields: % 22.26/7.49 | (405) all_179_0_149 = all_161_0_122 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (14) with all_65_2_29, all_149_0_104, all_179_0_149 and discharging atoms h(all_65_2_29) = all_179_0_149, h(all_65_2_29) = all_149_0_104, yields: % 22.26/7.49 | (406) all_179_0_149 = all_149_0_104 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (14) with all_65_2_29, all_145_0_98, all_149_0_104 and discharging atoms h(all_65_2_29) = all_149_0_104, h(all_65_2_29) = all_145_0_98, yields: % 22.26/7.49 | (407) all_149_0_104 = all_145_0_98 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (14) with all_65_2_29, all_143_0_95, all_193_0_170 and discharging atoms h(all_65_2_29) = all_193_0_170, h(all_65_2_29) = all_143_0_95, yields: % 22.26/7.49 | (408) all_193_0_170 = all_143_0_95 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (14) with all_65_2_29, all_143_0_95, all_145_0_98 and discharging atoms h(all_65_2_29) = all_145_0_98, h(all_65_2_29) = all_143_0_95, yields: % 22.26/7.49 | (409) all_145_0_98 = all_143_0_95 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (14) with all_65_2_29, all_141_0_94, all_179_0_149 and discharging atoms h(all_65_2_29) = all_179_0_149, h(all_65_2_29) = all_141_0_94, yields: % 22.26/7.49 | (410) all_179_0_149 = all_141_0_94 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (14) with all_65_2_29, all_115_0_70, all_145_0_98 and discharging atoms h(all_65_2_29) = all_145_0_98, h(all_65_2_29) = all_115_0_70, yields: % 22.26/7.49 | (411) all_145_0_98 = all_115_0_70 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (14) with all_65_2_29, all_107_0_65, all_193_0_170 and discharging atoms h(all_65_2_29) = all_193_0_170, h(all_65_2_29) = all_107_0_65, yields: % 22.26/7.49 | (412) all_193_0_170 = all_107_0_65 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (14) with all_58_2_24, all_105_0_62, all_127_0_79 and discharging atoms h(all_58_2_24) = all_127_0_79, h(all_58_2_24) = all_105_0_62, yields: % 22.26/7.49 | (413) all_127_0_79 = all_105_0_62 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (14) with all_58_2_24, all_101_0_58, all_127_0_79 and discharging atoms h(all_58_2_24) = all_127_0_79, h(all_58_2_24) = all_101_0_58, yields: % 22.26/7.49 | (414) all_127_0_79 = all_101_0_58 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (14) with all_30_1_9, all_181_0_152, all_187_0_161 and discharging atoms h(all_30_1_9) = all_187_0_161, h(all_30_1_9) = all_181_0_152, yields: % 22.26/7.49 | (415) all_187_0_161 = all_181_0_152 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (14) with all_30_1_9, all_163_0_125, all_181_0_152 and discharging atoms h(all_30_1_9) = all_181_0_152, h(all_30_1_9) = all_163_0_125, yields: % 22.26/7.49 | (416) all_181_0_152 = all_163_0_125 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (14) with all_30_1_9, all_147_0_101, all_181_0_152 and discharging atoms h(all_30_1_9) = all_181_0_152, h(all_30_1_9) = all_147_0_101, yields: % 22.26/7.49 | (417) all_181_0_152 = all_147_0_101 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (14) with all_30_1_9, all_139_0_91, all_147_0_101 and discharging atoms h(all_30_1_9) = all_147_0_101, h(all_30_1_9) = all_139_0_91, yields: % 22.26/7.49 | (418) all_147_0_101 = all_139_0_91 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (14) with all_30_1_9, all_135_0_85, all_139_0_91 and discharging atoms h(all_30_1_9) = all_139_0_91, h(all_30_1_9) = all_135_0_85, yields: % 22.26/7.49 | (419) all_139_0_91 = all_135_0_85 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (14) with all_30_1_9, all_133_0_84, all_81_1_50 and discharging atoms h(all_30_1_9) = all_133_0_84, h(all_30_1_9) = all_81_1_50, yields: % 22.26/7.49 | (420) all_133_0_84 = all_81_1_50 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (14) with all_30_1_9, all_133_0_84, all_135_0_85 and discharging atoms h(all_30_1_9) = all_135_0_85, h(all_30_1_9) = all_133_0_84, yields: % 22.26/7.49 | (421) all_135_0_85 = all_133_0_84 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (14) with all_30_1_9, all_129_0_80, all_187_0_161 and discharging atoms h(all_30_1_9) = all_187_0_161, h(all_30_1_9) = all_129_0_80, yields: % 22.26/7.49 | (422) all_187_0_161 = all_129_0_80 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (14) with all_30_1_9, all_121_0_77, all_133_0_84 and discharging atoms h(all_30_1_9) = all_133_0_84, h(all_30_1_9) = all_121_0_77, yields: % 22.26/7.49 | (423) all_133_0_84 = all_121_0_77 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (14) with all_30_2_10, all_185_0_158, all_60_0_25 and discharging atoms h(all_30_2_10) = all_185_0_158, h(all_30_2_10) = all_60_0_25, yields: % 22.26/7.49 | (424) all_185_0_158 = all_60_0_25 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (14) with all_30_2_10, all_175_0_143, all_185_0_158 and discharging atoms h(all_30_2_10) = all_185_0_158, h(all_30_2_10) = all_175_0_143, yields: % 22.26/7.49 | (425) all_185_0_158 = all_175_0_143 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (14) with all_30_2_10, all_155_0_113, all_185_0_158 and discharging atoms h(all_30_2_10) = all_185_0_158, h(all_30_2_10) = all_155_0_113, yields: % 22.26/7.49 | (426) all_185_0_158 = all_155_0_113 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (17) with all_60_0_25, all_0_0_0, all_165_2_130, all_81_1_50 and discharging atoms op2(all_60_0_25, all_0_0_0) = all_165_2_130, op2(all_60_0_25, all_0_0_0) = all_81_1_50, yields: % 22.26/7.49 | (427) all_165_2_130 = all_81_1_50 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (16) with all_30_2_10, all_30_1_9, all_147_2_103, all_30_0_8 and discharging atoms op1(all_30_2_10, all_30_1_9) = all_147_2_103, op1(all_30_2_10, all_30_1_9) = all_30_0_8, yields: % 22.26/7.49 | (428) all_147_2_103 = all_30_0_8 % 22.26/7.49 | % 22.26/7.49 | Instantiating formula (16) with all_8_0_1, all_30_1_9, all_135_2_87, all_30_2_10 and discharging atoms op1(all_8_0_1, all_30_1_9) = all_135_2_87, op1(all_8_0_1, all_30_1_9) = all_30_2_10, yields: % 22.26/7.49 | (429) all_135_2_87 = all_30_2_10 % 22.26/7.50 | % 22.26/7.50 | Combining equations (408,412) yields a new equation: % 22.26/7.50 | (430) all_143_0_95 = all_107_0_65 % 22.26/7.50 | % 22.26/7.50 | Simplifying 430 yields: % 22.26/7.50 | (431) all_143_0_95 = all_107_0_65 % 22.26/7.50 | % 22.26/7.50 | Combining equations (415,422) yields a new equation: % 22.26/7.50 | (432) all_181_0_152 = all_129_0_80 % 22.26/7.50 | % 22.26/7.50 | Simplifying 432 yields: % 22.26/7.50 | (433) all_181_0_152 = all_129_0_80 % 22.26/7.50 | % 22.26/7.50 | Combining equations (426,425) yields a new equation: % 22.26/7.50 | (434) all_175_0_143 = all_155_0_113 % 22.26/7.50 | % 22.26/7.50 | Combining equations (424,425) yields a new equation: % 22.26/7.50 | (435) all_175_0_143 = all_60_0_25 % 22.26/7.50 | % 22.26/7.50 | Combining equations (417,416) yields a new equation: % 22.26/7.50 | (436) all_163_0_125 = all_147_0_101 % 22.26/7.50 | % 22.26/7.50 | Combining equations (433,416) yields a new equation: % 22.26/7.50 | (437) all_163_0_125 = all_129_0_80 % 22.26/7.50 | % 22.26/7.50 | Combining equations (410,405) yields a new equation: % 22.26/7.50 | (438) all_161_0_122 = all_141_0_94 % 22.26/7.50 | % 22.26/7.50 | Combining equations (406,405) yields a new equation: % 22.26/7.50 | (439) all_161_0_122 = all_149_0_104 % 22.26/7.50 | % 22.26/7.50 | Combining equations (435,434) yields a new equation: % 22.26/7.50 | (440) all_155_0_113 = all_60_0_25 % 22.26/7.50 | % 22.26/7.50 | Combining equations (400,403) yields a new equation: % 22.26/7.50 | (441) all_117_0_71 = all_110_0_66 % 22.26/7.50 | % 22.26/7.50 | Simplifying 441 yields: % 22.26/7.50 | (442) all_117_0_71 = all_110_0_66 % 22.26/7.50 | % 22.26/7.50 | Combining equations (436,437) yields a new equation: % 22.26/7.50 | (443) all_147_0_101 = all_129_0_80 % 22.26/7.50 | % 22.26/7.50 | Simplifying 443 yields: % 22.26/7.50 | (444) all_147_0_101 = all_129_0_80 % 22.26/7.50 | % 22.26/7.50 | Combining equations (439,438) yields a new equation: % 22.26/7.50 | (445) all_149_0_104 = all_141_0_94 % 22.26/7.50 | % 22.26/7.50 | Simplifying 445 yields: % 22.26/7.50 | (446) all_149_0_104 = all_141_0_94 % 22.26/7.50 | % 22.26/7.50 | Combining equations (407,446) yields a new equation: % 22.26/7.50 | (447) all_145_0_98 = all_141_0_94 % 22.26/7.50 | % 22.26/7.50 | Simplifying 447 yields: % 22.26/7.50 | (448) all_145_0_98 = all_141_0_94 % 22.26/7.50 | % 22.26/7.50 | Combining equations (418,444) yields a new equation: % 22.26/7.50 | (449) all_139_0_91 = all_129_0_80 % 22.26/7.50 | % 22.26/7.50 | Simplifying 449 yields: % 22.26/7.50 | (450) all_139_0_91 = all_129_0_80 % 22.26/7.50 | % 22.26/7.50 | Combining equations (409,448) yields a new equation: % 22.26/7.50 | (451) all_143_0_95 = all_141_0_94 % 22.26/7.50 | % 22.26/7.50 | Simplifying 451 yields: % 22.26/7.50 | (452) all_143_0_95 = all_141_0_94 % 22.26/7.50 | % 22.26/7.50 | Combining equations (411,448) yields a new equation: % 22.26/7.50 | (453) all_141_0_94 = all_115_0_70 % 22.26/7.50 | % 22.26/7.50 | Combining equations (452,431) yields a new equation: % 22.26/7.50 | (454) all_141_0_94 = all_107_0_65 % 22.26/7.50 | % 22.26/7.50 | Simplifying 454 yields: % 22.26/7.50 | (455) all_141_0_94 = all_107_0_65 % 22.26/7.50 | % 22.26/7.50 | Combining equations (453,455) yields a new equation: % 22.26/7.50 | (456) all_115_0_70 = all_107_0_65 % 22.26/7.50 | % 22.26/7.50 | Simplifying 456 yields: % 22.26/7.50 | (457) all_115_0_70 = all_107_0_65 % 22.26/7.50 | % 22.26/7.50 | Combining equations (419,450) yields a new equation: % 22.26/7.50 | (458) all_135_0_85 = all_129_0_80 % 22.26/7.50 | % 22.26/7.50 | Simplifying 458 yields: % 22.26/7.50 | (459) all_135_0_85 = all_129_0_80 % 22.26/7.50 | % 22.26/7.50 | Combining equations (421,459) yields a new equation: % 22.26/7.50 | (460) all_133_0_84 = all_129_0_80 % 22.26/7.50 | % 22.26/7.50 | Simplifying 460 yields: % 22.26/7.50 | (461) all_133_0_84 = all_129_0_80 % 22.26/7.50 | % 22.26/7.50 | Combining equations (423,461) yields a new equation: % 22.26/7.50 | (462) all_129_0_80 = all_121_0_77 % 22.26/7.50 | % 22.26/7.50 | Combining equations (420,461) yields a new equation: % 22.26/7.50 | (463) all_129_0_80 = all_81_1_50 % 22.26/7.50 | % 22.26/7.50 | Combining equations (463,462) yields a new equation: % 22.26/7.50 | (464) all_121_0_77 = all_81_1_50 % 22.26/7.50 | % 22.26/7.50 | Combining equations (414,413) yields a new equation: % 22.26/7.50 | (465) all_105_0_62 = all_101_0_58 % 22.26/7.50 | % 22.26/7.50 | Combining equations (402,442) yields a new equation: % 22.26/7.50 | (466) all_113_0_67 = all_110_0_66 % 22.26/7.50 | % 22.26/7.50 | Simplifying 466 yields: % 22.26/7.50 | (467) all_113_0_67 = all_110_0_66 % 22.26/7.50 | % 22.26/7.50 | Combining equations (401,467) yields a new equation: % 22.26/7.50 | (468) all_110_0_66 = all_30_2_10 % 22.26/7.50 | % 22.26/7.50 | Combining equations (465,413) yields a new equation: % 22.26/7.50 | (414) all_127_0_79 = all_101_0_58 % 22.26/7.50 | % 22.26/7.50 | Combining equations (464,462) yields a new equation: % 22.26/7.50 | (463) all_129_0_80 = all_81_1_50 % 22.26/7.50 | % 22.26/7.50 | Combining equations (463,459) yields a new equation: % 22.26/7.50 | (471) all_135_0_85 = all_81_1_50 % 22.26/7.50 | % 22.26/7.50 | Combining equations (463,444) yields a new equation: % 22.26/7.50 | (472) all_147_0_101 = all_81_1_50 % 22.26/7.50 | % 22.26/7.50 | From (427) and (360) follows: % 22.26/7.50 | (473) j(all_81_1_50) = all_165_1_129 % 22.26/7.50 | % 22.26/7.50 | From (404) and (361) follows: % 22.26/7.50 | (22) j(all_0_0_0) = all_8_0_1 % 22.26/7.50 | % 22.26/7.50 | From (429) and (312) follows: % 22.26/7.50 | (475) h(all_30_2_10) = all_135_1_86 % 22.26/7.50 | % 22.26/7.50 | From (440) and (346) follows: % 22.26/7.50 | (116) h(all_30_2_10) = all_60_0_25 % 22.26/7.50 | % 22.26/7.50 | From (472) and (337) follows: % 22.26/7.50 | (477) op2(all_60_0_25, all_81_1_50) = all_147_1_102 % 22.26/7.50 | % 22.26/7.50 | From (427) and (362) follows: % 22.26/7.50 | (218) op2(all_60_0_25, all_0_0_0) = all_81_1_50 % 22.26/7.50 | % 22.26/7.50 | From (471) and (399) follows: % 22.26/7.50 | (479) op2(all_0_0_0, all_81_1_50) = all_135_1_86 % 22.26/7.50 | % 22.26/7.50 | From (468)(404) and (363) follows: % 22.26/7.50 | (480) op1(all_30_2_10, all_8_0_1) = all_165_1_129 % 22.26/7.50 | % 22.26/7.50 | From (428) and (338) follows: % 22.26/7.50 | (61) op1(all_30_2_10, all_30_1_9) = all_30_0_8 % 22.26/7.50 | % 22.26/7.50 | From (463) and (307) follows: % 22.26/7.50 | (482) sorti2(all_81_1_50) % 22.26/7.50 | % 22.26/7.50 | From (414) and (304) follows: % 22.26/7.50 | (483) sorti2(all_101_0_58) % 22.26/7.50 | % 22.26/7.50 | From (457) and (284) follows: % 22.26/7.50 | (484) sorti2(all_107_0_65) % 22.26/7.50 | % 22.26/7.50 | Instantiating formula (14) with all_30_2_10, all_135_1_86, all_60_0_25 and discharging atoms h(all_30_2_10) = all_135_1_86, h(all_30_2_10) = all_60_0_25, yields: % 22.26/7.50 | (485) all_135_1_86 = all_60_0_25 % 22.26/7.50 | % 22.26/7.50 | Instantiating formula (16) with all_30_2_10, all_8_0_1, all_165_1_129, all_30_1_9 and discharging atoms op1(all_30_2_10, all_8_0_1) = all_165_1_129, op1(all_30_2_10, all_8_0_1) = all_30_1_9, yields: % 22.26/7.50 | (486) all_165_1_129 = all_30_1_9 % 22.26/7.50 | % 22.26/7.50 | From (486) and (473) follows: % 22.26/7.50 | (487) j(all_81_1_50) = all_30_1_9 % 22.26/7.50 | % 22.26/7.50 | From (485) and (479) follows: % 22.26/7.50 | (488) op2(all_0_0_0, all_81_1_50) = all_60_0_25 % 22.26/7.50 | % 22.26/7.50 | Instantiating formula (2) with all_147_1_102, all_81_1_50, all_60_0_25 and discharging atoms op2(all_60_0_25, all_81_1_50) = all_147_1_102, op2(all_60_0_25, all_0_0_0) = all_81_1_50, sorti2(all_60_0_25), yields: % 22.26/7.51 | (489) all_147_1_102 = all_0_0_0 | ? [v0] : ( ~ (v0 = all_60_0_25) & op2(all_0_0_0, all_81_1_50) = v0) % 22.26/7.51 | % 22.26/7.51 | Instantiating formula (13) with all_81_1_50, all_60_0_25 and discharging atoms op2(all_60_0_25, all_0_0_0) = all_81_1_50, op2(all_0_0_0, all_81_1_50) = all_60_0_25, sorti2(all_60_0_25), yields: % 22.26/7.51 | (490) op2(all_60_0_25, all_81_1_50) = all_0_0_0 % 22.26/7.51 | % 22.26/7.51 | Instantiating formula (5) with all_107_0_65 and discharging atoms sorti2(all_107_0_65), yields: % 22.26/7.51 | (491) ? [v0] : (j(all_107_0_65) = v0 & ! [v1] : ( ~ sorti2(v1) | ? [v2] : ? [v3] : ? [v4] : (j(v2) = v3 & j(v1) = v4 & op2(all_107_0_65, v1) = v2 & op1(v0, v4) = v3))) % 22.26/7.51 | % 22.26/7.51 | Instantiating formula (5) with all_101_0_58 and discharging atoms sorti2(all_101_0_58), yields: % 22.26/7.51 | (492) ? [v0] : (j(all_101_0_58) = v0 & ! [v1] : ( ~ sorti2(v1) | ? [v2] : ? [v3] : ? [v4] : (j(v2) = v3 & j(v1) = v4 & op2(all_101_0_58, v1) = v2 & op1(v0, v4) = v3))) % 22.26/7.51 | % 22.26/7.51 | Instantiating formula (5) with all_85_1_56 and discharging atoms sorti2(all_85_1_56), yields: % 22.26/7.51 | (493) ? [v0] : (j(all_85_1_56) = v0 & ! [v1] : ( ~ sorti2(v1) | ? [v2] : ? [v3] : ? [v4] : (j(v2) = v3 & j(v1) = v4 & op2(all_85_1_56, v1) = v2 & op1(v0, v4) = v3))) % 22.26/7.51 | % 22.26/7.51 | Instantiating formula (5) with all_83_1_53 and discharging atoms sorti2(all_83_1_53), yields: % 22.26/7.51 | (494) ? [v0] : (j(all_83_1_53) = v0 & ! [v1] : ( ~ sorti2(v1) | ? [v2] : ? [v3] : ? [v4] : (j(v2) = v3 & j(v1) = v4 & op2(all_83_1_53, v1) = v2 & op1(v0, v4) = v3))) % 22.26/7.51 | % 22.26/7.51 | Instantiating formula (274) with all_81_1_50 and discharging atoms sorti2(all_81_1_50), yields: % 22.26/7.51 | (495) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_81_1_50) = v2 & op2(all_60_0_25, all_81_1_50) = v0 & op1(all_110_0_66, v2) = v1) % 22.26/7.51 | % 22.26/7.51 | Instantiating formula (96) with all_81_1_50 and discharging atoms sorti2(all_81_1_50), yields: % 22.26/7.51 | (496) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_81_1_50) = v2 & op2(all_15_2_6, all_81_1_50) = v0 & op1(all_51_0_15, v2) = v1) % 22.26/7.51 | % 22.26/7.51 | Instantiating formula (5) with all_81_1_50 and discharging atoms sorti2(all_81_1_50), yields: % 22.26/7.51 | (497) ? [v0] : (j(all_81_1_50) = v0 & ! [v1] : ( ~ sorti2(v1) | ? [v2] : ? [v3] : ? [v4] : (j(v2) = v3 & j(v1) = v4 & op2(all_81_1_50, v1) = v2 & op1(v0, v4) = v3))) % 22.26/7.51 | % 22.26/7.51 | Instantiating formula (5) with all_75_1_41 and discharging atoms sorti2(all_75_1_41), yields: % 22.26/7.51 | (498) ? [v0] : (j(all_75_1_41) = v0 & ! [v1] : ( ~ sorti2(v1) | ? [v2] : ? [v3] : ? [v4] : (j(v2) = v3 & j(v1) = v4 & op2(all_75_1_41, v1) = v2 & op1(v0, v4) = v3))) % 22.26/7.51 | % 22.26/7.51 | Instantiating formula (5) with all_73_1_38 and discharging atoms sorti2(all_73_1_38), yields: % 22.26/7.51 | (499) ? [v0] : (j(all_73_1_38) = v0 & ! [v1] : ( ~ sorti2(v1) | ? [v2] : ? [v3] : ? [v4] : (j(v2) = v3 & j(v1) = v4 & op2(all_73_1_38, v1) = v2 & op1(v0, v4) = v3))) % 22.26/7.51 | % 22.26/7.51 | Instantiating formula (5) with all_71_1_35 and discharging atoms sorti2(all_71_1_35), yields: % 22.26/7.51 | (500) ? [v0] : (j(all_71_1_35) = v0 & ! [v1] : ( ~ sorti2(v1) | ? [v2] : ? [v3] : ? [v4] : (j(v2) = v3 & j(v1) = v4 & op2(all_71_1_35, v1) = v2 & op1(v0, v4) = v3))) % 22.26/7.51 | % 22.26/7.51 | Instantiating formula (5) with all_69_1_32 and discharging atoms sorti2(all_69_1_32), yields: % 22.26/7.51 | (501) ? [v0] : (j(all_69_1_32) = v0 & ! [v1] : ( ~ sorti2(v1) | ? [v2] : ? [v3] : ? [v4] : (j(v2) = v3 & j(v1) = v4 & op2(all_69_1_32, v1) = v2 & op1(v0, v4) = v3))) % 22.26/7.51 | % 22.26/7.51 | Instantiating formula (5) with all_54_2_18 and discharging atoms sorti2(all_54_2_18), yields: % 22.26/7.51 | (502) ? [v0] : (j(all_54_2_18) = v0 & ! [v1] : ( ~ sorti2(v1) | ? [v2] : ? [v3] : ? [v4] : (j(v2) = v3 & j(v1) = v4 & op2(all_54_2_18, v1) = v2 & op1(v0, v4) = v3))) % 22.26/7.51 | % 22.26/7.51 | Instantiating (494) with all_215_0_182 yields: % 22.26/7.51 | (503) j(all_83_1_53) = all_215_0_182 & ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_83_1_53, v0) = v1 & op1(all_215_0_182, v3) = v2)) % 22.26/7.51 | % 22.26/7.51 | Applying alpha-rule on (503) yields: % 22.26/7.51 | (504) j(all_83_1_53) = all_215_0_182 % 22.26/7.51 | (505) ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_83_1_53, v0) = v1 & op1(all_215_0_182, v3) = v2)) % 22.26/7.51 | % 22.26/7.51 | Instantiating formula (505) with all_81_1_50 and discharging atoms sorti2(all_81_1_50), yields: % 22.26/7.51 | (506) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_81_1_50) = v2 & op2(all_83_1_53, all_81_1_50) = v0 & op1(all_215_0_182, v2) = v1) % 22.26/7.51 | % 22.26/7.51 | Instantiating formula (505) with all_0_0_0 and discharging atoms sorti2(all_0_0_0), yields: % 22.26/7.51 | (507) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_0_0) = v2 & op2(all_83_1_53, all_0_0_0) = v0 & op1(all_215_0_182, v2) = v1) % 22.26/7.51 | % 22.26/7.51 | Instantiating (497) with all_260_0_233 yields: % 22.26/7.51 | (508) j(all_81_1_50) = all_260_0_233 & ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_81_1_50, v0) = v1 & op1(all_260_0_233, v3) = v2)) % 22.26/7.51 | % 22.26/7.51 | Applying alpha-rule on (508) yields: % 22.26/7.51 | (509) j(all_81_1_50) = all_260_0_233 % 22.26/7.51 | (510) ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_81_1_50, v0) = v1 & op1(all_260_0_233, v3) = v2)) % 22.26/7.51 | % 22.26/7.51 | Instantiating formula (510) with all_81_1_50 and discharging atoms sorti2(all_81_1_50), yields: % 22.26/7.51 | (511) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_81_1_50) = v2 & op2(all_81_1_50, all_81_1_50) = v0 & op1(all_260_0_233, v2) = v1) % 22.26/7.51 | % 22.26/7.51 | Instantiating formula (510) with all_0_0_0 and discharging atoms sorti2(all_0_0_0), yields: % 22.26/7.51 | (512) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_0_0) = v2 & op2(all_81_1_50, all_0_0_0) = v0 & op1(all_260_0_233, v2) = v1) % 22.26/7.51 | % 22.26/7.51 | Instantiating (496) with all_263_0_234, all_263_1_235, all_263_2_236 yields: % 22.26/7.51 | (513) j(all_263_2_236) = all_263_1_235 & j(all_81_1_50) = all_263_0_234 & op2(all_15_2_6, all_81_1_50) = all_263_2_236 & op1(all_51_0_15, all_263_0_234) = all_263_1_235 % 22.26/7.51 | % 22.26/7.51 | Applying alpha-rule on (513) yields: % 22.26/7.51 | (514) j(all_263_2_236) = all_263_1_235 % 22.26/7.51 | (515) j(all_81_1_50) = all_263_0_234 % 22.26/7.51 | (516) op2(all_15_2_6, all_81_1_50) = all_263_2_236 % 22.26/7.51 | (517) op1(all_51_0_15, all_263_0_234) = all_263_1_235 % 22.26/7.51 | % 22.26/7.51 | Instantiating (495) with all_267_0_240, all_267_1_241, all_267_2_242 yields: % 22.26/7.51 | (518) j(all_267_2_242) = all_267_1_241 & j(all_81_1_50) = all_267_0_240 & op2(all_60_0_25, all_81_1_50) = all_267_2_242 & op1(all_110_0_66, all_267_0_240) = all_267_1_241 % 22.26/7.51 | % 22.26/7.51 | Applying alpha-rule on (518) yields: % 22.26/7.51 | (519) j(all_267_2_242) = all_267_1_241 % 22.26/7.51 | (520) j(all_81_1_50) = all_267_0_240 % 22.26/7.51 | (521) op2(all_60_0_25, all_81_1_50) = all_267_2_242 % 22.26/7.51 | (522) op1(all_110_0_66, all_267_0_240) = all_267_1_241 % 22.26/7.51 | % 22.26/7.51 | Instantiating (502) with all_334_0_326 yields: % 22.26/7.51 | (523) j(all_54_2_18) = all_334_0_326 & ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_54_2_18, v0) = v1 & op1(all_334_0_326, v3) = v2)) % 22.26/7.51 | % 22.26/7.51 | Applying alpha-rule on (523) yields: % 22.26/7.51 | (524) j(all_54_2_18) = all_334_0_326 % 22.26/7.51 | (525) ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_54_2_18, v0) = v1 & op1(all_334_0_326, v3) = v2)) % 22.26/7.51 | % 22.26/7.51 | Instantiating formula (525) with all_81_1_50 and discharging atoms sorti2(all_81_1_50), yields: % 22.26/7.52 | (526) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_81_1_50) = v2 & op2(all_54_2_18, all_81_1_50) = v0 & op1(all_334_0_326, v2) = v1) % 22.26/7.52 | % 22.26/7.52 | Instantiating formula (525) with all_0_0_0 and discharging atoms sorti2(all_0_0_0), yields: % 22.26/7.52 | (527) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_0_0) = v2 & op2(all_54_2_18, all_0_0_0) = v0 & op1(all_334_0_326, v2) = v1) % 22.26/7.52 | % 22.26/7.52 | Instantiating (501) with all_341_0_333 yields: % 22.26/7.52 | (528) j(all_69_1_32) = all_341_0_333 & ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_69_1_32, v0) = v1 & op1(all_341_0_333, v3) = v2)) % 22.26/7.52 | % 22.26/7.52 | Applying alpha-rule on (528) yields: % 22.26/7.52 | (529) j(all_69_1_32) = all_341_0_333 % 22.26/7.52 | (530) ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_69_1_32, v0) = v1 & op1(all_341_0_333, v3) = v2)) % 22.26/7.52 | % 22.26/7.52 | Instantiating formula (530) with all_81_1_50 and discharging atoms sorti2(all_81_1_50), yields: % 22.26/7.52 | (531) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_81_1_50) = v2 & op2(all_69_1_32, all_81_1_50) = v0 & op1(all_341_0_333, v2) = v1) % 22.26/7.52 | % 22.26/7.52 | Instantiating formula (530) with all_0_0_0 and discharging atoms sorti2(all_0_0_0), yields: % 22.26/7.52 | (532) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_0_0) = v2 & op2(all_69_1_32, all_0_0_0) = v0 & op1(all_341_0_333, v2) = v1) % 22.26/7.52 | % 22.26/7.52 | Instantiating (491) with all_386_0_386 yields: % 22.26/7.52 | (533) j(all_107_0_65) = all_386_0_386 & ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_107_0_65, v0) = v1 & op1(all_386_0_386, v3) = v2)) % 22.26/7.52 | % 22.26/7.52 | Applying alpha-rule on (533) yields: % 22.26/7.52 | (534) j(all_107_0_65) = all_386_0_386 % 22.26/7.52 | (535) ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_107_0_65, v0) = v1 & op1(all_386_0_386, v3) = v2)) % 22.26/7.52 | % 22.26/7.52 | Instantiating formula (535) with all_81_1_50 and discharging atoms sorti2(all_81_1_50), yields: % 22.26/7.52 | (536) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_81_1_50) = v2 & op2(all_107_0_65, all_81_1_50) = v0 & op1(all_386_0_386, v2) = v1) % 22.26/7.52 | % 22.26/7.52 | Instantiating formula (535) with all_0_0_0 and discharging atoms sorti2(all_0_0_0), yields: % 22.26/7.52 | (537) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_0_0) = v2 & op2(all_107_0_65, all_0_0_0) = v0 & op1(all_386_0_386, v2) = v1) % 22.26/7.52 | % 22.26/7.52 | Instantiating (500) with all_412_0_416 yields: % 22.26/7.52 | (538) j(all_71_1_35) = all_412_0_416 & ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_71_1_35, v0) = v1 & op1(all_412_0_416, v3) = v2)) % 22.26/7.52 | % 22.26/7.52 | Applying alpha-rule on (538) yields: % 22.26/7.52 | (539) j(all_71_1_35) = all_412_0_416 % 22.26/7.52 | (540) ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_71_1_35, v0) = v1 & op1(all_412_0_416, v3) = v2)) % 22.26/7.52 | % 22.26/7.52 | Instantiating formula (540) with all_81_1_50 and discharging atoms sorti2(all_81_1_50), yields: % 22.26/7.52 | (541) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_81_1_50) = v2 & op2(all_71_1_35, all_81_1_50) = v0 & op1(all_412_0_416, v2) = v1) % 22.26/7.52 | % 22.26/7.52 | Instantiating formula (540) with all_0_0_0 and discharging atoms sorti2(all_0_0_0), yields: % 22.26/7.52 | (542) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_0_0) = v2 & op2(all_71_1_35, all_0_0_0) = v0 & op1(all_412_0_416, v2) = v1) % 22.26/7.52 | % 22.26/7.52 | Instantiating (493) with all_421_0_426 yields: % 22.26/7.52 | (543) j(all_85_1_56) = all_421_0_426 & ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_85_1_56, v0) = v1 & op1(all_421_0_426, v3) = v2)) % 22.26/7.52 | % 22.26/7.52 | Applying alpha-rule on (543) yields: % 22.26/7.52 | (544) j(all_85_1_56) = all_421_0_426 % 22.26/7.52 | (545) ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_85_1_56, v0) = v1 & op1(all_421_0_426, v3) = v2)) % 22.26/7.52 | % 22.26/7.52 | Instantiating formula (545) with all_81_1_50 and discharging atoms sorti2(all_81_1_50), yields: % 22.26/7.52 | (546) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_81_1_50) = v2 & op2(all_85_1_56, all_81_1_50) = v0 & op1(all_421_0_426, v2) = v1) % 22.26/7.52 | % 22.26/7.52 | Instantiating formula (545) with all_0_0_0 and discharging atoms sorti2(all_0_0_0), yields: % 22.26/7.52 | (547) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_0_0) = v2 & op2(all_85_1_56, all_0_0_0) = v0 & op1(all_421_0_426, v2) = v1) % 22.26/7.52 | % 22.26/7.52 | Instantiating (499) with all_454_0_457 yields: % 22.26/7.52 | (548) j(all_73_1_38) = all_454_0_457 & ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_73_1_38, v0) = v1 & op1(all_454_0_457, v3) = v2)) % 22.26/7.52 | % 22.26/7.52 | Applying alpha-rule on (548) yields: % 22.26/7.52 | (549) j(all_73_1_38) = all_454_0_457 % 22.26/7.52 | (550) ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_73_1_38, v0) = v1 & op1(all_454_0_457, v3) = v2)) % 22.26/7.52 | % 22.26/7.52 | Instantiating formula (550) with all_81_1_50 and discharging atoms sorti2(all_81_1_50), yields: % 22.26/7.52 | (551) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_81_1_50) = v2 & op2(all_73_1_38, all_81_1_50) = v0 & op1(all_454_0_457, v2) = v1) % 22.26/7.52 | % 22.26/7.52 | Instantiating formula (550) with all_0_0_0 and discharging atoms sorti2(all_0_0_0), yields: % 22.26/7.52 | (552) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_0_0) = v2 & op2(all_73_1_38, all_0_0_0) = v0 & op1(all_454_0_457, v2) = v1) % 22.26/7.52 | % 22.26/7.52 | Instantiating (498) with all_463_0_467 yields: % 22.26/7.52 | (553) j(all_75_1_41) = all_463_0_467 & ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_75_1_41, v0) = v1 & op1(all_463_0_467, v3) = v2)) % 22.26/7.52 | % 22.26/7.52 | Applying alpha-rule on (553) yields: % 22.26/7.52 | (554) j(all_75_1_41) = all_463_0_467 % 22.26/7.52 | (555) ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_75_1_41, v0) = v1 & op1(all_463_0_467, v3) = v2)) % 22.26/7.52 | % 22.26/7.52 | Instantiating formula (555) with all_81_1_50 and discharging atoms sorti2(all_81_1_50), yields: % 22.26/7.52 | (556) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_81_1_50) = v2 & op2(all_75_1_41, all_81_1_50) = v0 & op1(all_463_0_467, v2) = v1) % 22.26/7.52 | % 22.26/7.52 | Instantiating formula (555) with all_0_0_0 and discharging atoms sorti2(all_0_0_0), yields: % 22.26/7.52 | (557) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_0_0) = v2 & op2(all_75_1_41, all_0_0_0) = v0 & op1(all_463_0_467, v2) = v1) % 22.26/7.52 | % 22.26/7.52 | Instantiating (492) with all_496_0_513 yields: % 22.26/7.52 | (558) j(all_101_0_58) = all_496_0_513 & ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_101_0_58, v0) = v1 & op1(all_496_0_513, v3) = v2)) % 22.26/7.52 | % 22.26/7.52 | Applying alpha-rule on (558) yields: % 22.26/7.52 | (559) j(all_101_0_58) = all_496_0_513 % 22.26/7.52 | (560) ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_101_0_58, v0) = v1 & op1(all_496_0_513, v3) = v2)) % 22.26/7.52 | % 22.26/7.52 | Instantiating formula (560) with all_81_1_50 and discharging atoms sorti2(all_81_1_50), yields: % 22.26/7.52 | (561) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_81_1_50) = v2 & op2(all_101_0_58, all_81_1_50) = v0 & op1(all_496_0_513, v2) = v1) % 22.26/7.52 | % 22.26/7.52 | Instantiating formula (560) with all_0_0_0 and discharging atoms sorti2(all_0_0_0), yields: % 22.26/7.52 | (562) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_0_0) = v2 & op2(all_101_0_58, all_0_0_0) = v0 & op1(all_496_0_513, v2) = v1) % 22.26/7.52 | % 22.26/7.52 | Instantiating (507) with all_542_0_568, all_542_1_569, all_542_2_570 yields: % 22.26/7.52 | (563) j(all_542_2_570) = all_542_1_569 & j(all_0_0_0) = all_542_0_568 & op2(all_83_1_53, all_0_0_0) = all_542_2_570 & op1(all_215_0_182, all_542_0_568) = all_542_1_569 % 22.26/7.52 | % 22.26/7.52 | Applying alpha-rule on (563) yields: % 22.26/7.52 | (564) j(all_542_2_570) = all_542_1_569 % 22.26/7.52 | (565) j(all_0_0_0) = all_542_0_568 % 22.26/7.52 | (566) op2(all_83_1_53, all_0_0_0) = all_542_2_570 % 22.26/7.52 | (567) op1(all_215_0_182, all_542_0_568) = all_542_1_569 % 22.26/7.52 | % 22.26/7.52 | Instantiating (506) with all_566_0_604, all_566_1_605, all_566_2_606 yields: % 22.26/7.52 | (568) j(all_566_2_606) = all_566_1_605 & j(all_81_1_50) = all_566_0_604 & op2(all_83_1_53, all_81_1_50) = all_566_2_606 & op1(all_215_0_182, all_566_0_604) = all_566_1_605 % 22.26/7.52 | % 22.26/7.52 | Applying alpha-rule on (568) yields: % 22.26/7.52 | (569) j(all_566_2_606) = all_566_1_605 % 22.26/7.52 | (570) j(all_81_1_50) = all_566_0_604 % 22.26/7.52 | (571) op2(all_83_1_53, all_81_1_50) = all_566_2_606 % 22.26/7.52 | (572) op1(all_215_0_182, all_566_0_604) = all_566_1_605 % 22.26/7.52 | % 22.26/7.52 | Instantiating (512) with all_644_0_721, all_644_1_722, all_644_2_723 yields: % 22.26/7.52 | (573) j(all_644_2_723) = all_644_1_722 & j(all_0_0_0) = all_644_0_721 & op2(all_81_1_50, all_0_0_0) = all_644_2_723 & op1(all_260_0_233, all_644_0_721) = all_644_1_722 % 22.26/7.52 | % 22.26/7.52 | Applying alpha-rule on (573) yields: % 22.26/7.52 | (574) j(all_644_2_723) = all_644_1_722 % 22.26/7.52 | (575) j(all_0_0_0) = all_644_0_721 % 22.26/7.52 | (576) op2(all_81_1_50, all_0_0_0) = all_644_2_723 % 22.26/7.52 | (577) op1(all_260_0_233, all_644_0_721) = all_644_1_722 % 22.26/7.52 | % 22.26/7.52 | Instantiating (511) with all_668_0_757, all_668_1_758, all_668_2_759 yields: % 22.26/7.52 | (578) j(all_668_2_759) = all_668_1_758 & j(all_81_1_50) = all_668_0_757 & op2(all_81_1_50, all_81_1_50) = all_668_2_759 & op1(all_260_0_233, all_668_0_757) = all_668_1_758 % 22.26/7.53 | % 22.26/7.53 | Applying alpha-rule on (578) yields: % 22.26/7.53 | (579) j(all_668_2_759) = all_668_1_758 % 22.26/7.53 | (580) j(all_81_1_50) = all_668_0_757 % 22.26/7.53 | (581) op2(all_81_1_50, all_81_1_50) = all_668_2_759 % 22.26/7.53 | (582) op1(all_260_0_233, all_668_0_757) = all_668_1_758 % 22.26/7.53 | % 22.26/7.53 | Instantiating (527) with all_784_0_931, all_784_1_932, all_784_2_933 yields: % 22.26/7.53 | (583) j(all_784_2_933) = all_784_1_932 & j(all_0_0_0) = all_784_0_931 & op2(all_54_2_18, all_0_0_0) = all_784_2_933 & op1(all_334_0_326, all_784_0_931) = all_784_1_932 % 22.26/7.53 | % 22.26/7.53 | Applying alpha-rule on (583) yields: % 22.26/7.53 | (584) j(all_784_2_933) = all_784_1_932 % 22.26/7.53 | (585) j(all_0_0_0) = all_784_0_931 % 22.26/7.53 | (586) op2(all_54_2_18, all_0_0_0) = all_784_2_933 % 22.26/7.53 | (587) op1(all_334_0_326, all_784_0_931) = all_784_1_932 % 22.26/7.53 | % 22.26/7.53 | Instantiating (526) with all_808_0_967, all_808_1_968, all_808_2_969 yields: % 22.26/7.53 | (588) j(all_808_2_969) = all_808_1_968 & j(all_81_1_50) = all_808_0_967 & op2(all_54_2_18, all_81_1_50) = all_808_2_969 & op1(all_334_0_326, all_808_0_967) = all_808_1_968 % 22.26/7.53 | % 22.26/7.53 | Applying alpha-rule on (588) yields: % 22.26/7.53 | (589) j(all_808_2_969) = all_808_1_968 % 22.26/7.53 | (590) j(all_81_1_50) = all_808_0_967 % 22.26/7.53 | (591) op2(all_54_2_18, all_81_1_50) = all_808_2_969 % 22.26/7.53 | (592) op1(all_334_0_326, all_808_0_967) = all_808_1_968 % 22.26/7.53 | % 22.26/7.53 | Instantiating (532) with all_810_0_970, all_810_1_971, all_810_2_972 yields: % 22.26/7.53 | (593) j(all_810_2_972) = all_810_1_971 & j(all_0_0_0) = all_810_0_970 & op2(all_69_1_32, all_0_0_0) = all_810_2_972 & op1(all_341_0_333, all_810_0_970) = all_810_1_971 % 22.26/7.53 | % 22.26/7.53 | Applying alpha-rule on (593) yields: % 22.26/7.53 | (594) j(all_810_2_972) = all_810_1_971 % 22.26/7.53 | (595) j(all_0_0_0) = all_810_0_970 % 22.26/7.53 | (596) op2(all_69_1_32, all_0_0_0) = all_810_2_972 % 22.26/7.53 | (597) op1(all_341_0_333, all_810_0_970) = all_810_1_971 % 22.26/7.53 | % 22.26/7.53 | Instantiating (531) with all_834_0_1006, all_834_1_1007, all_834_2_1008 yields: % 22.26/7.53 | (598) j(all_834_2_1008) = all_834_1_1007 & j(all_81_1_50) = all_834_0_1006 & op2(all_69_1_32, all_81_1_50) = all_834_2_1008 & op1(all_341_0_333, all_834_0_1006) = all_834_1_1007 % 22.26/7.53 | % 22.26/7.53 | Applying alpha-rule on (598) yields: % 22.26/7.53 | (599) j(all_834_2_1008) = all_834_1_1007 % 22.26/7.53 | (600) j(all_81_1_50) = all_834_0_1006 % 22.26/7.53 | (601) op2(all_69_1_32, all_81_1_50) = all_834_2_1008 % 22.26/7.53 | (602) op1(all_341_0_333, all_834_0_1006) = all_834_1_1007 % 22.26/7.53 | % 22.26/7.53 | Instantiating (537) with all_912_0_1123, all_912_1_1124, all_912_2_1125 yields: % 22.26/7.53 | (603) j(all_912_2_1125) = all_912_1_1124 & j(all_0_0_0) = all_912_0_1123 & op2(all_107_0_65, all_0_0_0) = all_912_2_1125 & op1(all_386_0_386, all_912_0_1123) = all_912_1_1124 % 22.26/7.53 | % 22.26/7.53 | Applying alpha-rule on (603) yields: % 22.26/7.53 | (604) j(all_912_2_1125) = all_912_1_1124 % 22.26/7.53 | (605) j(all_0_0_0) = all_912_0_1123 % 22.26/7.53 | (606) op2(all_107_0_65, all_0_0_0) = all_912_2_1125 % 22.26/7.53 | (607) op1(all_386_0_386, all_912_0_1123) = all_912_1_1124 % 22.26/7.53 | % 22.26/7.53 | Instantiating (536) with all_936_0_1159, all_936_1_1160, all_936_2_1161 yields: % 22.26/7.53 | (608) j(all_936_2_1161) = all_936_1_1160 & j(all_81_1_50) = all_936_0_1159 & op2(all_107_0_65, all_81_1_50) = all_936_2_1161 & op1(all_386_0_386, all_936_0_1159) = all_936_1_1160 % 22.26/7.53 | % 22.26/7.53 | Applying alpha-rule on (608) yields: % 22.26/7.53 | (609) j(all_936_2_1161) = all_936_1_1160 % 22.26/7.53 | (610) j(all_81_1_50) = all_936_0_1159 % 22.26/7.53 | (611) op2(all_107_0_65, all_81_1_50) = all_936_2_1161 % 22.26/7.53 | (612) op1(all_386_0_386, all_936_0_1159) = all_936_1_1160 % 22.26/7.53 | % 22.26/7.53 | Instantiating (542) with all_976_0_1219, all_976_1_1220, all_976_2_1221 yields: % 22.26/7.53 | (613) j(all_976_2_1221) = all_976_1_1220 & j(all_0_0_0) = all_976_0_1219 & op2(all_71_1_35, all_0_0_0) = all_976_2_1221 & op1(all_412_0_416, all_976_0_1219) = all_976_1_1220 % 22.26/7.53 | % 22.26/7.53 | Applying alpha-rule on (613) yields: % 22.26/7.53 | (614) j(all_976_2_1221) = all_976_1_1220 % 22.26/7.53 | (615) j(all_0_0_0) = all_976_0_1219 % 22.26/7.53 | (616) op2(all_71_1_35, all_0_0_0) = all_976_2_1221 % 22.26/7.53 | (617) op1(all_412_0_416, all_976_0_1219) = all_976_1_1220 % 22.26/7.53 | % 22.26/7.53 | Instantiating (541) with all_982_0_1228, all_982_1_1229, all_982_2_1230 yields: % 22.26/7.53 | (618) j(all_982_2_1230) = all_982_1_1229 & j(all_81_1_50) = all_982_0_1228 & op2(all_71_1_35, all_81_1_50) = all_982_2_1230 & op1(all_412_0_416, all_982_0_1228) = all_982_1_1229 % 22.26/7.53 | % 22.26/7.53 | Applying alpha-rule on (618) yields: % 22.26/7.53 | (619) j(all_982_2_1230) = all_982_1_1229 % 22.26/7.53 | (620) j(all_81_1_50) = all_982_0_1228 % 22.26/7.53 | (621) op2(all_71_1_35, all_81_1_50) = all_982_2_1230 % 22.26/7.53 | (622) op1(all_412_0_416, all_982_0_1228) = all_982_1_1229 % 22.26/7.53 | % 22.26/7.53 | Instantiating (547) with all_1002_0_1258, all_1002_1_1259, all_1002_2_1260 yields: % 22.26/7.53 | (623) j(all_1002_2_1260) = all_1002_1_1259 & j(all_0_0_0) = all_1002_0_1258 & op2(all_85_1_56, all_0_0_0) = all_1002_2_1260 & op1(all_421_0_426, all_1002_0_1258) = all_1002_1_1259 % 22.26/7.53 | % 22.26/7.53 | Applying alpha-rule on (623) yields: % 22.26/7.53 | (624) j(all_1002_2_1260) = all_1002_1_1259 % 22.26/7.53 | (625) j(all_0_0_0) = all_1002_0_1258 % 22.26/7.53 | (626) op2(all_85_1_56, all_0_0_0) = all_1002_2_1260 % 22.26/7.53 | (627) op1(all_421_0_426, all_1002_0_1258) = all_1002_1_1259 % 22.26/7.53 | % 22.26/7.53 | Instantiating (546) with all_1018_0_1282, all_1018_1_1283, all_1018_2_1284 yields: % 22.26/7.53 | (628) j(all_1018_2_1284) = all_1018_1_1283 & j(all_81_1_50) = all_1018_0_1282 & op2(all_85_1_56, all_81_1_50) = all_1018_2_1284 & op1(all_421_0_426, all_1018_0_1282) = all_1018_1_1283 % 22.26/7.53 | % 22.26/7.53 | Applying alpha-rule on (628) yields: % 22.26/7.53 | (629) j(all_1018_2_1284) = all_1018_1_1283 % 22.26/7.53 | (630) j(all_81_1_50) = all_1018_0_1282 % 22.26/7.53 | (631) op2(all_85_1_56, all_81_1_50) = all_1018_2_1284 % 22.26/7.53 | (632) op1(all_421_0_426, all_1018_0_1282) = all_1018_1_1283 % 22.26/7.53 | % 22.26/7.53 | Instantiating (552) with all_1104_0_1411, all_1104_1_1412, all_1104_2_1413 yields: % 22.26/7.53 | (633) j(all_1104_2_1413) = all_1104_1_1412 & j(all_0_0_0) = all_1104_0_1411 & op2(all_73_1_38, all_0_0_0) = all_1104_2_1413 & op1(all_454_0_457, all_1104_0_1411) = all_1104_1_1412 % 22.26/7.53 | % 22.26/7.53 | Applying alpha-rule on (633) yields: % 22.26/7.53 | (634) j(all_1104_2_1413) = all_1104_1_1412 % 22.26/7.53 | (635) j(all_0_0_0) = all_1104_0_1411 % 22.26/7.53 | (636) op2(all_73_1_38, all_0_0_0) = all_1104_2_1413 % 22.26/7.53 | (637) op1(all_454_0_457, all_1104_0_1411) = all_1104_1_1412 % 22.26/7.53 | % 22.26/7.53 | Instantiating (551) with all_1120_0_1435, all_1120_1_1436, all_1120_2_1437 yields: % 22.26/7.53 | (638) j(all_1120_2_1437) = all_1120_1_1436 & j(all_81_1_50) = all_1120_0_1435 & op2(all_73_1_38, all_81_1_50) = all_1120_2_1437 & op1(all_454_0_457, all_1120_0_1435) = all_1120_1_1436 % 22.26/7.53 | % 22.26/7.53 | Applying alpha-rule on (638) yields: % 22.26/7.53 | (639) j(all_1120_2_1437) = all_1120_1_1436 % 22.26/7.53 | (640) j(all_81_1_50) = all_1120_0_1435 % 22.26/7.53 | (641) op2(all_73_1_38, all_81_1_50) = all_1120_2_1437 % 22.26/7.53 | (642) op1(all_454_0_457, all_1120_0_1435) = all_1120_1_1436 % 22.26/7.53 | % 22.26/7.53 | Instantiating (557) with all_1130_0_1450, all_1130_1_1451, all_1130_2_1452 yields: % 22.26/7.53 | (643) j(all_1130_2_1452) = all_1130_1_1451 & j(all_0_0_0) = all_1130_0_1450 & op2(all_75_1_41, all_0_0_0) = all_1130_2_1452 & op1(all_463_0_467, all_1130_0_1450) = all_1130_1_1451 % 22.26/7.53 | % 22.26/7.53 | Applying alpha-rule on (643) yields: % 22.26/7.53 | (644) j(all_1130_2_1452) = all_1130_1_1451 % 22.26/7.53 | (645) j(all_0_0_0) = all_1130_0_1450 % 22.26/7.53 | (646) op2(all_75_1_41, all_0_0_0) = all_1130_2_1452 % 22.26/7.53 | (647) op1(all_463_0_467, all_1130_0_1450) = all_1130_1_1451 % 22.26/7.53 | % 22.26/7.53 | Instantiating (556) with all_1140_0_1465, all_1140_1_1466, all_1140_2_1467 yields: % 22.26/7.53 | (648) j(all_1140_2_1467) = all_1140_1_1466 & j(all_81_1_50) = all_1140_0_1465 & op2(all_75_1_41, all_81_1_50) = all_1140_2_1467 & op1(all_463_0_467, all_1140_0_1465) = all_1140_1_1466 % 22.26/7.53 | % 22.26/7.53 | Applying alpha-rule on (648) yields: % 22.26/7.53 | (649) j(all_1140_2_1467) = all_1140_1_1466 % 22.26/7.53 | (650) j(all_81_1_50) = all_1140_0_1465 % 22.26/7.53 | (651) op2(all_75_1_41, all_81_1_50) = all_1140_2_1467 % 22.26/7.53 | (652) op1(all_463_0_467, all_1140_0_1465) = all_1140_1_1466 % 22.26/7.53 | % 22.26/7.53 | Instantiating (562) with all_1156_0_1489, all_1156_1_1490, all_1156_2_1491 yields: % 22.26/7.53 | (653) j(all_1156_2_1491) = all_1156_1_1490 & j(all_0_0_0) = all_1156_0_1489 & op2(all_101_0_58, all_0_0_0) = all_1156_2_1491 & op1(all_496_0_513, all_1156_0_1489) = all_1156_1_1490 % 22.26/7.53 | % 22.26/7.53 | Applying alpha-rule on (653) yields: % 22.26/7.53 | (654) j(all_1156_2_1491) = all_1156_1_1490 % 22.26/7.53 | (655) j(all_0_0_0) = all_1156_0_1489 % 22.26/7.53 | (656) op2(all_101_0_58, all_0_0_0) = all_1156_2_1491 % 22.26/7.53 | (657) op1(all_496_0_513, all_1156_0_1489) = all_1156_1_1490 % 22.26/7.53 | % 22.26/7.53 | Instantiating (561) with all_1172_0_1513, all_1172_1_1514, all_1172_2_1515 yields: % 22.26/7.53 | (658) j(all_1172_2_1515) = all_1172_1_1514 & j(all_81_1_50) = all_1172_0_1513 & op2(all_101_0_58, all_81_1_50) = all_1172_2_1515 & op1(all_496_0_513, all_1172_0_1513) = all_1172_1_1514 % 22.26/7.53 | % 22.26/7.53 | Applying alpha-rule on (658) yields: % 22.26/7.53 | (659) j(all_1172_2_1515) = all_1172_1_1514 % 22.26/7.53 | (660) j(all_81_1_50) = all_1172_0_1513 % 22.26/7.53 | (661) op2(all_101_0_58, all_81_1_50) = all_1172_2_1515 % 22.26/7.53 | (662) op1(all_496_0_513, all_1172_0_1513) = all_1172_1_1514 % 22.26/7.53 | % 22.26/7.53 | From (468) and (522) follows: % 22.26/7.53 | (663) op1(all_30_2_10, all_267_0_240) = all_267_1_241 % 22.26/7.53 | % 22.26/7.53 +-Applying beta-rule and splitting (489), into two cases. % 22.26/7.53 |-Branch one: % 22.26/7.53 | (664) all_147_1_102 = all_0_0_0 % 22.26/7.53 | % 22.26/7.53 | From (664) and (477) follows: % 22.26/7.53 | (490) op2(all_60_0_25, all_81_1_50) = all_0_0_0 % 22.26/7.53 | % 22.26/7.53 | Instantiating formula (10) with all_81_1_50, all_1120_0_1435, all_1172_0_1513 and discharging atoms j(all_81_1_50) = all_1172_0_1513, j(all_81_1_50) = all_1120_0_1435, yields: % 22.26/7.53 | (666) all_1172_0_1513 = all_1120_0_1435 % 22.26/7.53 | % 22.26/7.53 | Instantiating formula (10) with all_81_1_50, all_1018_0_1282, all_1120_0_1435 and discharging atoms j(all_81_1_50) = all_1120_0_1435, j(all_81_1_50) = all_1018_0_1282, yields: % 22.26/7.53 | (667) all_1120_0_1435 = all_1018_0_1282 % 22.26/7.53 | % 22.26/7.53 | Instantiating formula (10) with all_81_1_50, all_982_0_1228, all_1018_0_1282 and discharging atoms j(all_81_1_50) = all_1018_0_1282, j(all_81_1_50) = all_982_0_1228, yields: % 22.26/7.53 | (668) all_1018_0_1282 = all_982_0_1228 % 22.26/7.53 | % 22.26/7.53 | Instantiating formula (10) with all_81_1_50, all_936_0_1159, all_982_0_1228 and discharging atoms j(all_81_1_50) = all_982_0_1228, j(all_81_1_50) = all_936_0_1159, yields: % 22.26/7.53 | (669) all_982_0_1228 = all_936_0_1159 % 22.26/7.53 | % 22.26/7.53 | Instantiating formula (10) with all_81_1_50, all_834_0_1006, all_1140_0_1465 and discharging atoms j(all_81_1_50) = all_1140_0_1465, j(all_81_1_50) = all_834_0_1006, yields: % 22.26/7.53 | (670) all_1140_0_1465 = all_834_0_1006 % 22.26/7.53 | % 22.26/7.53 | Instantiating formula (10) with all_81_1_50, all_808_0_967, all_834_0_1006 and discharging atoms j(all_81_1_50) = all_834_0_1006, j(all_81_1_50) = all_808_0_967, yields: % 22.26/7.53 | (671) all_834_0_1006 = all_808_0_967 % 22.26/7.53 | % 22.26/7.53 | Instantiating formula (10) with all_81_1_50, all_668_0_757, all_936_0_1159 and discharging atoms j(all_81_1_50) = all_936_0_1159, j(all_81_1_50) = all_668_0_757, yields: % 22.26/7.53 | (672) all_936_0_1159 = all_668_0_757 % 22.26/7.53 | % 22.26/7.53 | Instantiating formula (10) with all_81_1_50, all_566_0_604, all_808_0_967 and discharging atoms j(all_81_1_50) = all_808_0_967, j(all_81_1_50) = all_566_0_604, yields: % 22.26/7.53 | (673) all_808_0_967 = all_566_0_604 % 22.26/7.53 | % 22.26/7.53 | Instantiating formula (10) with all_81_1_50, all_566_0_604, all_668_0_757 and discharging atoms j(all_81_1_50) = all_668_0_757, j(all_81_1_50) = all_566_0_604, yields: % 22.26/7.53 | (674) all_668_0_757 = all_566_0_604 % 22.26/7.53 | % 22.26/7.53 | Instantiating formula (10) with all_81_1_50, all_267_0_240, all_1172_0_1513 and discharging atoms j(all_81_1_50) = all_1172_0_1513, j(all_81_1_50) = all_267_0_240, yields: % 22.26/7.53 | (675) all_1172_0_1513 = all_267_0_240 % 22.26/7.53 | % 22.26/7.53 | Instantiating formula (10) with all_81_1_50, all_263_0_234, all_30_1_9 and discharging atoms j(all_81_1_50) = all_263_0_234, j(all_81_1_50) = all_30_1_9, yields: % 22.26/7.53 | (676) all_263_0_234 = all_30_1_9 % 22.26/7.53 | % 22.26/7.53 | Instantiating formula (10) with all_81_1_50, all_263_0_234, all_566_0_604 and discharging atoms j(all_81_1_50) = all_566_0_604, j(all_81_1_50) = all_263_0_234, yields: % 22.26/7.53 | (677) all_566_0_604 = all_263_0_234 % 22.26/7.53 | % 22.26/7.53 | Instantiating formula (10) with all_81_1_50, all_260_0_233, all_1140_0_1465 and discharging atoms j(all_81_1_50) = all_1140_0_1465, j(all_81_1_50) = all_260_0_233, yields: % 22.26/7.53 | (678) all_1140_0_1465 = all_260_0_233 % 22.26/7.53 | % 22.26/7.53 | Instantiating formula (10) with all_0_0_0, all_1130_0_1450, all_8_0_1 and discharging atoms j(all_0_0_0) = all_1130_0_1450, j(all_0_0_0) = all_8_0_1, yields: % 22.26/7.53 | (679) all_1130_0_1450 = all_8_0_1 % 22.26/7.53 | % 22.26/7.53 | Instantiating formula (10) with all_0_0_0, all_1130_0_1450, all_1156_0_1489 and discharging atoms j(all_0_0_0) = all_1156_0_1489, j(all_0_0_0) = all_1130_0_1450, yields: % 22.26/7.53 | (680) all_1156_0_1489 = all_1130_0_1450 % 22.26/7.53 | % 22.26/7.53 | Instantiating formula (10) with all_0_0_0, all_1104_0_1411, all_1156_0_1489 and discharging atoms j(all_0_0_0) = all_1156_0_1489, j(all_0_0_0) = all_1104_0_1411, yields: % 22.67/7.53 | (681) all_1156_0_1489 = all_1104_0_1411 % 22.67/7.53 | % 22.67/7.53 | Instantiating formula (10) with all_0_0_0, all_1002_0_1258, all_1130_0_1450 and discharging atoms j(all_0_0_0) = all_1130_0_1450, j(all_0_0_0) = all_1002_0_1258, yields: % 22.67/7.54 | (682) all_1130_0_1450 = all_1002_0_1258 % 22.67/7.54 | % 22.67/7.54 | Instantiating formula (10) with all_0_0_0, all_976_0_1219, all_1002_0_1258 and discharging atoms j(all_0_0_0) = all_1002_0_1258, j(all_0_0_0) = all_976_0_1219, yields: % 22.67/7.54 | (683) all_1002_0_1258 = all_976_0_1219 % 22.67/7.54 | % 22.67/7.54 | Instantiating formula (10) with all_0_0_0, all_912_0_1123, all_976_0_1219 and discharging atoms j(all_0_0_0) = all_976_0_1219, j(all_0_0_0) = all_912_0_1123, yields: % 22.67/7.54 | (684) all_976_0_1219 = all_912_0_1123 % 22.67/7.54 | % 22.67/7.54 | Instantiating formula (10) with all_0_0_0, all_810_0_970, all_912_0_1123 and discharging atoms j(all_0_0_0) = all_912_0_1123, j(all_0_0_0) = all_810_0_970, yields: % 22.67/7.54 | (685) all_912_0_1123 = all_810_0_970 % 22.67/7.54 | % 22.67/7.54 | Instantiating formula (10) with all_0_0_0, all_784_0_931, all_810_0_970 and discharging atoms j(all_0_0_0) = all_810_0_970, j(all_0_0_0) = all_784_0_931, yields: % 22.67/7.54 | (686) all_810_0_970 = all_784_0_931 % 22.67/7.54 | % 22.67/7.54 | Instantiating formula (10) with all_0_0_0, all_644_0_721, all_784_0_931 and discharging atoms j(all_0_0_0) = all_784_0_931, j(all_0_0_0) = all_644_0_721, yields: % 22.67/7.54 | (687) all_784_0_931 = all_644_0_721 % 22.67/7.54 | % 22.67/7.54 | Instantiating formula (10) with all_0_0_0, all_542_0_568, all_644_0_721 and discharging atoms j(all_0_0_0) = all_644_0_721, j(all_0_0_0) = all_542_0_568, yields: % 22.67/7.54 | (688) all_644_0_721 = all_542_0_568 % 22.67/7.54 | % 22.67/7.54 | Instantiating formula (17) with all_60_0_25, all_81_1_50, all_0_0_0, all_267_2_242 and discharging atoms op2(all_60_0_25, all_81_1_50) = all_267_2_242, op2(all_60_0_25, all_81_1_50) = all_0_0_0, yields: % 22.67/7.54 | (689) all_267_2_242 = all_0_0_0 % 22.67/7.54 | % 22.67/7.54 | Combining equations (666,675) yields a new equation: % 22.67/7.54 | (690) all_1120_0_1435 = all_267_0_240 % 22.67/7.54 | % 22.67/7.54 | Simplifying 690 yields: % 22.67/7.54 | (691) all_1120_0_1435 = all_267_0_240 % 22.67/7.54 | % 22.67/7.54 | Combining equations (680,681) yields a new equation: % 22.67/7.54 | (692) all_1130_0_1450 = all_1104_0_1411 % 22.67/7.54 | % 22.67/7.54 | Simplifying 692 yields: % 22.67/7.54 | (693) all_1130_0_1450 = all_1104_0_1411 % 22.67/7.54 | % 22.67/7.54 | Combining equations (670,678) yields a new equation: % 22.67/7.54 | (694) all_834_0_1006 = all_260_0_233 % 22.67/7.54 | % 22.67/7.54 | Simplifying 694 yields: % 22.67/7.54 | (695) all_834_0_1006 = all_260_0_233 % 22.67/7.54 | % 22.67/7.54 | Combining equations (679,693) yields a new equation: % 22.67/7.54 | (696) all_1104_0_1411 = all_8_0_1 % 22.67/7.54 | % 22.67/7.54 | Combining equations (682,693) yields a new equation: % 22.67/7.54 | (697) all_1104_0_1411 = all_1002_0_1258 % 22.67/7.54 | % 22.67/7.54 | Combining equations (667,691) yields a new equation: % 22.67/7.54 | (698) all_1018_0_1282 = all_267_0_240 % 22.67/7.54 | % 22.67/7.54 | Simplifying 698 yields: % 22.67/7.54 | (699) all_1018_0_1282 = all_267_0_240 % 22.67/7.54 | % 22.67/7.54 | Combining equations (697,696) yields a new equation: % 22.67/7.54 | (700) all_1002_0_1258 = all_8_0_1 % 22.67/7.54 | % 22.67/7.54 | Simplifying 700 yields: % 22.67/7.54 | (701) all_1002_0_1258 = all_8_0_1 % 22.67/7.54 | % 22.67/7.54 | Combining equations (668,699) yields a new equation: % 22.67/7.54 | (702) all_982_0_1228 = all_267_0_240 % 22.67/7.54 | % 22.67/7.54 | Simplifying 702 yields: % 22.67/7.54 | (703) all_982_0_1228 = all_267_0_240 % 22.67/7.54 | % 22.67/7.54 | Combining equations (683,701) yields a new equation: % 22.67/7.54 | (704) all_976_0_1219 = all_8_0_1 % 22.67/7.54 | % 22.67/7.54 | Simplifying 704 yields: % 22.67/7.54 | (705) all_976_0_1219 = all_8_0_1 % 22.67/7.54 | % 22.67/7.54 | Combining equations (669,703) yields a new equation: % 22.67/7.54 | (706) all_936_0_1159 = all_267_0_240 % 22.67/7.54 | % 22.67/7.54 | Simplifying 706 yields: % 22.67/7.54 | (707) all_936_0_1159 = all_267_0_240 % 22.67/7.54 | % 22.67/7.54 | Combining equations (684,705) yields a new equation: % 22.67/7.54 | (708) all_912_0_1123 = all_8_0_1 % 22.67/7.54 | % 22.67/7.54 | Simplifying 708 yields: % 22.67/7.54 | (709) all_912_0_1123 = all_8_0_1 % 22.67/7.54 | % 22.67/7.54 | Combining equations (672,707) yields a new equation: % 22.67/7.54 | (710) all_668_0_757 = all_267_0_240 % 22.67/7.54 | % 22.67/7.54 | Simplifying 710 yields: % 22.67/7.54 | (711) all_668_0_757 = all_267_0_240 % 22.67/7.54 | % 22.67/7.54 | Combining equations (685,709) yields a new equation: % 22.67/7.54 | (712) all_810_0_970 = all_8_0_1 % 22.67/7.54 | % 22.67/7.54 | Simplifying 712 yields: % 22.67/7.54 | (713) all_810_0_970 = all_8_0_1 % 22.67/7.54 | % 22.67/7.54 | Combining equations (671,695) yields a new equation: % 22.67/7.54 | (714) all_808_0_967 = all_260_0_233 % 22.67/7.54 | % 22.67/7.54 | Simplifying 714 yields: % 22.67/7.54 | (715) all_808_0_967 = all_260_0_233 % 22.67/7.54 | % 22.67/7.54 | Combining equations (686,713) yields a new equation: % 22.67/7.54 | (716) all_784_0_931 = all_8_0_1 % 22.67/7.54 | % 22.67/7.54 | Simplifying 716 yields: % 22.67/7.54 | (717) all_784_0_931 = all_8_0_1 % 22.67/7.54 | % 22.67/7.54 | Combining equations (673,715) yields a new equation: % 22.67/7.54 | (718) all_566_0_604 = all_260_0_233 % 22.67/7.54 | % 22.67/7.54 | Simplifying 718 yields: % 22.67/7.54 | (719) all_566_0_604 = all_260_0_233 % 22.67/7.54 | % 22.67/7.54 | Combining equations (687,717) yields a new equation: % 22.67/7.54 | (720) all_644_0_721 = all_8_0_1 % 22.67/7.54 | % 22.67/7.54 | Simplifying 720 yields: % 22.67/7.54 | (721) all_644_0_721 = all_8_0_1 % 22.67/7.54 | % 22.67/7.54 | Combining equations (674,711) yields a new equation: % 22.67/7.54 | (722) all_566_0_604 = all_267_0_240 % 22.67/7.54 | % 22.67/7.54 | Simplifying 722 yields: % 22.67/7.54 | (723) all_566_0_604 = all_267_0_240 % 22.67/7.54 | % 22.67/7.54 | Combining equations (688,721) yields a new equation: % 22.67/7.54 | (724) all_542_0_568 = all_8_0_1 % 22.67/7.54 | % 22.67/7.54 | Simplifying 724 yields: % 22.67/7.54 | (725) all_542_0_568 = all_8_0_1 % 22.67/7.54 | % 22.67/7.54 | Combining equations (677,723) yields a new equation: % 22.67/7.54 | (726) all_267_0_240 = all_263_0_234 % 22.67/7.54 | % 22.67/7.54 | Combining equations (719,723) yields a new equation: % 22.67/7.54 | (727) all_267_0_240 = all_260_0_233 % 22.67/7.54 | % 22.67/7.54 | Combining equations (726,727) yields a new equation: % 22.67/7.54 | (728) all_263_0_234 = all_260_0_233 % 22.67/7.54 | % 22.67/7.54 | Simplifying 728 yields: % 22.67/7.54 | (729) all_263_0_234 = all_260_0_233 % 22.67/7.54 | % 22.67/7.54 | Combining equations (676,729) yields a new equation: % 22.67/7.54 | (730) all_260_0_233 = all_30_1_9 % 22.67/7.54 | % 22.67/7.54 | Combining equations (730,727) yields a new equation: % 22.67/7.54 | (731) all_267_0_240 = all_30_1_9 % 22.67/7.54 | % 22.67/7.54 | From (689) and (519) follows: % 22.67/7.54 | (732) j(all_0_0_0) = all_267_1_241 % 22.67/7.54 | % 22.67/7.54 | From (725) and (565) follows: % 22.67/7.54 | (22) j(all_0_0_0) = all_8_0_1 % 22.67/7.54 | % 22.67/7.54 | From (731) and (663) follows: % 22.67/7.54 | (734) op1(all_30_2_10, all_30_1_9) = all_267_1_241 % 22.67/7.54 | % 22.67/7.54 | Instantiating formula (10) with all_0_0_0, all_267_1_241, all_8_0_1 and discharging atoms j(all_0_0_0) = all_267_1_241, j(all_0_0_0) = all_8_0_1, yields: % 22.67/7.54 | (735) all_267_1_241 = all_8_0_1 % 22.67/7.54 | % 22.67/7.54 | Instantiating formula (16) with all_30_2_10, all_30_1_9, all_267_1_241, all_30_0_8 and discharging atoms op1(all_30_2_10, all_30_1_9) = all_267_1_241, op1(all_30_2_10, all_30_1_9) = all_30_0_8, yields: % 22.67/7.54 | (736) all_267_1_241 = all_30_0_8 % 22.67/7.54 | % 22.67/7.54 | Combining equations (735,736) yields a new equation: % 22.67/7.54 | (737) all_30_0_8 = all_8_0_1 % 22.67/7.54 | % 22.67/7.54 | Equations (737) can reduce 59 to: % 22.67/7.54 | (738) $false % 22.67/7.54 | % 22.67/7.54 |-The branch is then unsatisfiable % 22.67/7.54 |-Branch two: % 22.67/7.54 | (739) ~ (all_147_1_102 = all_0_0_0) % 22.67/7.54 | (740) ? [v0] : ( ~ (v0 = all_60_0_25) & op2(all_0_0_0, all_81_1_50) = v0) % 22.67/7.54 | % 22.67/7.54 | Instantiating formula (17) with all_60_0_25, all_81_1_50, all_267_2_242, all_147_1_102 and discharging atoms op2(all_60_0_25, all_81_1_50) = all_267_2_242, op2(all_60_0_25, all_81_1_50) = all_147_1_102, yields: % 22.67/7.54 | (741) all_267_2_242 = all_147_1_102 % 22.67/7.54 | % 22.67/7.54 | Instantiating formula (17) with all_60_0_25, all_81_1_50, all_0_0_0, all_267_2_242 and discharging atoms op2(all_60_0_25, all_81_1_50) = all_267_2_242, op2(all_60_0_25, all_81_1_50) = all_0_0_0, yields: % 22.67/7.54 | (689) all_267_2_242 = all_0_0_0 % 22.67/7.54 | % 22.67/7.54 | Combining equations (689,741) yields a new equation: % 22.67/7.54 | (664) all_147_1_102 = all_0_0_0 % 22.67/7.54 | % 22.67/7.54 | Equations (664) can reduce 739 to: % 22.67/7.54 | (738) $false % 22.67/7.54 | % 22.67/7.54 |-The branch is then unsatisfiable % 22.67/7.54 % SZS output end Proof for theBenchmark % 22.67/7.54 % 22.67/7.54 6938ms %------------------------------------------------------------------------------