%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : ALG179+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n024.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:37:05 EDT 2022 % Result : Theorem 3.03s 1.39s % Output : Proof 7.31s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : ALG179+1 : TPTP v8.1.0. Released v2.7.0. % 0.10/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.33 % Computer : n024.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Tue Jun 7 23:40:34 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.57 ____ _ % 0.18/0.57 ___ / __ \_____(_)___ ________ __________ % 0.18/0.57 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.18/0.57 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.18/0.57 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.18/0.57 % 0.18/0.57 A Theorem Prover for First-Order Logic % 0.18/0.57 (ePrincess v.1.0) % 0.18/0.57 % 0.18/0.57 (c) Philipp Rümmer, 2009-2015 % 0.18/0.57 (c) Peter Backeman, 2014-2015 % 0.18/0.57 (contributions by Angelo Brillout, Peter Baumgartner) % 0.18/0.57 Free software under GNU Lesser General Public License (LGPL). % 0.18/0.57 Bug reports to peter@backeman.se % 0.18/0.57 % 0.18/0.57 For more information, visit http://user.uu.se/~petba168/breu/ % 0.18/0.57 % 0.18/0.57 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.71/0.63 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.42/0.91 Prover 0: Preprocessing ... % 1.72/1.07 Prover 0: Constructing countermodel ... % 3.03/1.39 Prover 0: proved (765ms) % 3.03/1.39 % 3.03/1.39 No countermodel exists, formula is valid % 3.03/1.39 % SZS status Theorem for theBenchmark % 3.03/1.39 % 3.03/1.39 Generating proof ... found it (size 259) % 6.38/2.28 % 6.38/2.28 % SZS output start Proof for theBenchmark % 6.38/2.28 Assumed formulas after preprocessing and simplification: % 6.38/2.28 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ( ~ (v3 = v0) & op2(v2, v1) = v3 & op2(v0, v1) = v2 & sorti2(v1) & sorti2(v0) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = v4 | ~ (op1(v6, v5) = v7) | ~ (op1(v4, v5) = v6) | ~ sorti1(v5) | ~ sorti1(v4)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (op2(v7, v6) = v5) | ~ (op2(v7, v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (op1(v7, v6) = v5) | ~ (op1(v7, v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (j(v6) = v5) | ~ (j(v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (h(v6) = v5) | ~ (h(v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : ( ~ (op2(v4, v5) = v6) | ~ sorti2(v5) | ~ sorti2(v4) | sorti2(v6)) & ! [v4] : ! [v5] : ! [v6] : ( ~ (op1(v4, v5) = v6) | ~ sorti1(v5) | ~ sorti1(v4) | sorti1(v6)) & ! [v4] : ( ~ sorti2(v4) | ? [v5] : (j(v4) = v5 & h(v5) = v4)) & ! [v4] : ( ~ sorti2(v4) | ? [v5] : (j(v4) = v5 & sorti1(v5))) & ! [v4] : ( ~ sorti2(v4) | ? [v5] : (j(v4) = v5 & ! [v6] : ( ~ sorti2(v6) | ? [v7] : ? [v8] : ? [v9] : (j(v7) = v8 & j(v6) = v9 & op2(v4, v6) = v7 & op1(v5, v9) = v8)))) & ! [v4] : ( ~ sorti1(v4) | ? [v5] : (j(v5) = v4 & h(v4) = v5)) & ! [v4] : ( ~ sorti1(v4) | ? [v5] : (h(v4) = v5 & sorti2(v5))) & ! [v4] : ( ~ sorti1(v4) | ? [v5] : (h(v4) = v5 & ! [v6] : ( ~ sorti1(v6) | ? [v7] : ? [v8] : ? [v9] : (h(v7) = v8 & h(v6) = v9 & op2(v5, v9) = v8 & op1(v4, v6) = v7))))) % 6.74/2.31 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3 yields: % 6.74/2.31 | (1) ~ (all_0_0_0 = all_0_3_3) & op2(all_0_1_1, all_0_2_2) = all_0_0_0 & op2(all_0_3_3, all_0_2_2) = all_0_1_1 & sorti2(all_0_2_2) & sorti2(all_0_3_3) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v0 | ~ (op1(v2, v1) = v3) | ~ (op1(v0, v1) = v2) | ~ sorti1(v1) | ~ sorti1(v0)) & ! [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] : (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] : ( ~ 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] : (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)))) % 6.74/2.32 | % 6.74/2.32 | Applying alpha-rule on (1) yields: % 6.74/2.32 | (2) ! [v0] : ( ~ sorti2(v0) | ? [v1] : (j(v0) = v1 & h(v1) = v0)) % 6.74/2.32 | (3) ! [v0] : ( ~ sorti1(v0) | ? [v1] : (j(v1) = v0 & h(v0) = v1)) % 6.74/2.32 | (4) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op1(v3, v2) = v1) | ~ (op1(v3, v2) = v0)) % 6.74/2.32 | (5) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h(v2) = v1) | ~ (h(v2) = v0)) % 6.74/2.32 | (6) ! [v0] : ! [v1] : ! [v2] : ( ~ (op1(v0, v1) = v2) | ~ sorti1(v1) | ~ sorti1(v0) | sorti1(v2)) % 6.74/2.32 | (7) ! [v0] : ( ~ sorti2(v0) | ? [v1] : (j(v0) = v1 & sorti1(v1))) % 6.74/2.32 | (8) op2(all_0_3_3, all_0_2_2) = all_0_1_1 % 6.74/2.32 | (9) ! [v0] : ( ~ sorti1(v0) | ? [v1] : (h(v0) = v1 & sorti2(v1))) % 6.74/2.32 | (10) sorti2(all_0_2_2) % 6.74/2.32 | (11) ~ (all_0_0_0 = all_0_3_3) % 6.74/2.32 | (12) sorti2(all_0_3_3) % 6.74/2.32 | (13) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (j(v2) = v1) | ~ (j(v2) = v0)) % 6.74/2.33 | (14) ! [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)))) % 6.74/2.33 | (15) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op2(v3, v2) = v1) | ~ (op2(v3, v2) = v0)) % 6.74/2.33 | (16) ! [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)))) % 6.74/2.33 | (17) op2(all_0_1_1, all_0_2_2) = all_0_0_0 % 6.74/2.33 | (18) ! [v0] : ! [v1] : ! [v2] : ( ~ (op2(v0, v1) = v2) | ~ sorti2(v1) | ~ sorti2(v0) | sorti2(v2)) % 6.74/2.33 | (19) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v0 | ~ (op1(v2, v1) = v3) | ~ (op1(v0, v1) = v2) | ~ sorti1(v1) | ~ sorti1(v0)) % 6.74/2.33 | % 6.74/2.33 | Instantiating formula (2) with all_0_2_2 and discharging atoms sorti2(all_0_2_2), yields: % 6.74/2.33 | (20) ? [v0] : (j(all_0_2_2) = v0 & h(v0) = all_0_2_2) % 6.74/2.33 | % 6.74/2.33 | Instantiating formula (7) with all_0_2_2 and discharging atoms sorti2(all_0_2_2), yields: % 6.74/2.33 | (21) ? [v0] : (j(all_0_2_2) = v0 & sorti1(v0)) % 6.74/2.33 | % 6.74/2.33 | Instantiating formula (16) with all_0_2_2 and discharging atoms sorti2(all_0_2_2), yields: % 6.74/2.33 | (22) ? [v0] : (j(all_0_2_2) = v0 & ! [v1] : ( ~ sorti2(v1) | ? [v2] : ? [v3] : ? [v4] : (j(v2) = v3 & j(v1) = v4 & op2(all_0_2_2, v1) = v2 & op1(v0, v4) = v3))) % 6.74/2.33 | % 6.74/2.33 | Instantiating formula (18) with all_0_1_1, all_0_2_2, all_0_3_3 and discharging atoms op2(all_0_3_3, all_0_2_2) = all_0_1_1, sorti2(all_0_2_2), sorti2(all_0_3_3), yields: % 6.74/2.33 | (23) sorti2(all_0_1_1) % 6.74/2.33 | % 6.74/2.33 | Instantiating formula (2) with all_0_3_3 and discharging atoms sorti2(all_0_3_3), yields: % 6.74/2.33 | (24) ? [v0] : (j(all_0_3_3) = v0 & h(v0) = all_0_3_3) % 6.74/2.33 | % 6.74/2.33 | Instantiating formula (7) with all_0_3_3 and discharging atoms sorti2(all_0_3_3), yields: % 6.74/2.33 | (25) ? [v0] : (j(all_0_3_3) = v0 & sorti1(v0)) % 6.74/2.33 | % 6.74/2.33 | Instantiating formula (16) with all_0_3_3 and discharging atoms sorti2(all_0_3_3), yields: % 6.74/2.33 | (26) ? [v0] : (j(all_0_3_3) = v0 & ! [v1] : ( ~ sorti2(v1) | ? [v2] : ? [v3] : ? [v4] : (j(v2) = v3 & j(v1) = v4 & op2(all_0_3_3, v1) = v2 & op1(v0, v4) = v3))) % 6.74/2.33 | % 6.74/2.33 | Instantiating (26) with all_9_0_4 yields: % 6.74/2.33 | (27) j(all_0_3_3) = all_9_0_4 & ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_0_3_3, v0) = v1 & op1(all_9_0_4, v3) = v2)) % 6.74/2.33 | % 6.74/2.33 | Applying alpha-rule on (27) yields: % 6.74/2.33 | (28) j(all_0_3_3) = all_9_0_4 % 6.74/2.33 | (29) ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_0_3_3, v0) = v1 & op1(all_9_0_4, v3) = v2)) % 6.74/2.33 | % 6.74/2.33 | Instantiating formula (29) with all_0_2_2 and discharging atoms sorti2(all_0_2_2), yields: % 6.74/2.33 | (30) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_2_2) = v2 & op2(all_0_3_3, all_0_2_2) = v0 & op1(all_9_0_4, v2) = v1) % 6.74/2.33 | % 6.74/2.33 | Instantiating formula (29) with all_0_3_3 and discharging atoms sorti2(all_0_3_3), yields: % 6.74/2.33 | (31) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_3_3) = v2 & op2(all_0_3_3, all_0_3_3) = v0 & op1(all_9_0_4, v2) = v1) % 6.74/2.33 | % 6.74/2.33 | Instantiating (25) with all_12_0_5 yields: % 6.74/2.33 | (32) j(all_0_3_3) = all_12_0_5 & sorti1(all_12_0_5) % 6.74/2.33 | % 6.74/2.33 | Applying alpha-rule on (32) yields: % 6.74/2.33 | (33) j(all_0_3_3) = all_12_0_5 % 6.74/2.33 | (34) sorti1(all_12_0_5) % 6.74/2.33 | % 6.74/2.33 | Instantiating (21) with all_14_0_6 yields: % 6.74/2.33 | (35) j(all_0_2_2) = all_14_0_6 & sorti1(all_14_0_6) % 6.74/2.33 | % 6.74/2.33 | Applying alpha-rule on (35) yields: % 6.74/2.33 | (36) j(all_0_2_2) = all_14_0_6 % 6.74/2.33 | (37) sorti1(all_14_0_6) % 6.74/2.33 | % 6.74/2.33 | Instantiating (20) with all_16_0_7 yields: % 6.74/2.33 | (38) j(all_0_2_2) = all_16_0_7 & h(all_16_0_7) = all_0_2_2 % 6.74/2.33 | % 6.74/2.33 | Applying alpha-rule on (38) yields: % 6.74/2.33 | (39) j(all_0_2_2) = all_16_0_7 % 6.74/2.33 | (40) h(all_16_0_7) = all_0_2_2 % 6.74/2.34 | % 6.74/2.34 | Instantiating (24) with all_18_0_8 yields: % 6.74/2.34 | (41) j(all_0_3_3) = all_18_0_8 & h(all_18_0_8) = all_0_3_3 % 6.74/2.34 | % 6.74/2.34 | Applying alpha-rule on (41) yields: % 6.74/2.34 | (42) j(all_0_3_3) = all_18_0_8 % 6.74/2.34 | (43) h(all_18_0_8) = all_0_3_3 % 6.74/2.34 | % 6.74/2.34 | Instantiating (22) with all_20_0_9 yields: % 6.74/2.34 | (44) j(all_0_2_2) = all_20_0_9 & ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_0_2_2, v0) = v1 & op1(all_20_0_9, v3) = v2)) % 6.74/2.34 | % 6.74/2.34 | Applying alpha-rule on (44) yields: % 6.74/2.34 | (45) j(all_0_2_2) = all_20_0_9 % 6.74/2.34 | (46) ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_0_2_2, v0) = v1 & op1(all_20_0_9, v3) = v2)) % 6.74/2.34 | % 6.74/2.34 | Instantiating formula (46) with all_0_2_2 and discharging atoms sorti2(all_0_2_2), yields: % 6.74/2.34 | (47) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_2_2) = v2 & op2(all_0_2_2, all_0_2_2) = v0 & op1(all_20_0_9, v2) = v1) % 6.74/2.34 | % 6.74/2.34 | Instantiating formula (46) with all_0_3_3 and discharging atoms sorti2(all_0_3_3), yields: % 6.74/2.34 | (48) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_3_3) = v2 & op2(all_0_2_2, all_0_3_3) = v0 & op1(all_20_0_9, v2) = v1) % 6.74/2.34 | % 6.74/2.34 | Instantiating (31) with all_23_0_10, all_23_1_11, all_23_2_12 yields: % 6.74/2.34 | (49) j(all_23_2_12) = all_23_1_11 & j(all_0_3_3) = all_23_0_10 & op2(all_0_3_3, all_0_3_3) = all_23_2_12 & op1(all_9_0_4, all_23_0_10) = all_23_1_11 % 6.74/2.34 | % 6.74/2.34 | Applying alpha-rule on (49) yields: % 6.74/2.34 | (50) j(all_23_2_12) = all_23_1_11 % 6.74/2.34 | (51) j(all_0_3_3) = all_23_0_10 % 6.74/2.34 | (52) op2(all_0_3_3, all_0_3_3) = all_23_2_12 % 6.74/2.34 | (53) op1(all_9_0_4, all_23_0_10) = all_23_1_11 % 6.74/2.34 | % 6.74/2.34 | Instantiating (30) with all_25_0_13, all_25_1_14, all_25_2_15 yields: % 6.74/2.34 | (54) j(all_25_2_15) = all_25_1_14 & j(all_0_2_2) = all_25_0_13 & op2(all_0_3_3, all_0_2_2) = all_25_2_15 & op1(all_9_0_4, all_25_0_13) = all_25_1_14 % 6.74/2.34 | % 6.74/2.34 | Applying alpha-rule on (54) yields: % 6.74/2.34 | (55) j(all_25_2_15) = all_25_1_14 % 6.74/2.34 | (56) j(all_0_2_2) = all_25_0_13 % 6.74/2.34 | (57) op2(all_0_3_3, all_0_2_2) = all_25_2_15 % 6.74/2.34 | (58) op1(all_9_0_4, all_25_0_13) = all_25_1_14 % 6.74/2.34 | % 6.74/2.34 | Instantiating (48) with all_27_0_16, all_27_1_17, all_27_2_18 yields: % 6.74/2.34 | (59) j(all_27_2_18) = all_27_1_17 & j(all_0_3_3) = all_27_0_16 & op2(all_0_2_2, all_0_3_3) = all_27_2_18 & op1(all_20_0_9, all_27_0_16) = all_27_1_17 % 6.74/2.34 | % 6.74/2.34 | Applying alpha-rule on (59) yields: % 6.74/2.34 | (60) j(all_27_2_18) = all_27_1_17 % 6.74/2.34 | (61) j(all_0_3_3) = all_27_0_16 % 6.74/2.34 | (62) op2(all_0_2_2, all_0_3_3) = all_27_2_18 % 6.74/2.34 | (63) op1(all_20_0_9, all_27_0_16) = all_27_1_17 % 6.74/2.34 | % 6.74/2.34 | Instantiating (47) with all_29_0_19, all_29_1_20, all_29_2_21 yields: % 6.74/2.34 | (64) j(all_29_2_21) = all_29_1_20 & j(all_0_2_2) = all_29_0_19 & op2(all_0_2_2, all_0_2_2) = all_29_2_21 & op1(all_20_0_9, all_29_0_19) = all_29_1_20 % 6.74/2.34 | % 6.74/2.34 | Applying alpha-rule on (64) yields: % 6.74/2.34 | (65) j(all_29_2_21) = all_29_1_20 % 6.74/2.34 | (66) j(all_0_2_2) = all_29_0_19 % 6.74/2.34 | (67) op2(all_0_2_2, all_0_2_2) = all_29_2_21 % 6.74/2.34 | (68) op1(all_20_0_9, all_29_0_19) = all_29_1_20 % 6.74/2.34 | % 6.74/2.34 | Instantiating formula (13) with all_0_2_2, all_25_0_13, all_29_0_19 and discharging atoms j(all_0_2_2) = all_29_0_19, j(all_0_2_2) = all_25_0_13, yields: % 6.74/2.34 | (69) all_29_0_19 = all_25_0_13 % 6.74/2.34 | % 6.74/2.34 | Instantiating formula (13) with all_0_2_2, all_20_0_9, all_25_0_13 and discharging atoms j(all_0_2_2) = all_25_0_13, j(all_0_2_2) = all_20_0_9, yields: % 6.74/2.34 | (70) all_25_0_13 = all_20_0_9 % 6.74/2.34 | % 6.74/2.34 | Instantiating formula (13) with all_0_2_2, all_16_0_7, all_25_0_13 and discharging atoms j(all_0_2_2) = all_25_0_13, j(all_0_2_2) = all_16_0_7, yields: % 6.74/2.34 | (71) all_25_0_13 = all_16_0_7 % 6.74/2.34 | % 6.74/2.34 | Instantiating formula (13) with all_0_2_2, all_14_0_6, all_29_0_19 and discharging atoms j(all_0_2_2) = all_29_0_19, j(all_0_2_2) = all_14_0_6, yields: % 6.74/2.34 | (72) all_29_0_19 = all_14_0_6 % 6.74/2.34 | % 6.74/2.34 | Instantiating formula (13) with all_0_3_3, all_23_0_10, all_27_0_16 and discharging atoms j(all_0_3_3) = all_27_0_16, j(all_0_3_3) = all_23_0_10, yields: % 6.74/2.34 | (73) all_27_0_16 = all_23_0_10 % 6.74/2.34 | % 6.74/2.34 | Instantiating formula (13) with all_0_3_3, all_18_0_8, all_27_0_16 and discharging atoms j(all_0_3_3) = all_27_0_16, j(all_0_3_3) = all_18_0_8, yields: % 6.74/2.34 | (74) all_27_0_16 = all_18_0_8 % 6.74/2.34 | % 6.74/2.34 | Instantiating formula (13) with all_0_3_3, all_12_0_5, all_27_0_16 and discharging atoms j(all_0_3_3) = all_27_0_16, j(all_0_3_3) = all_12_0_5, yields: % 6.74/2.34 | (75) all_27_0_16 = all_12_0_5 % 6.74/2.34 | % 6.74/2.34 | Instantiating formula (13) with all_0_3_3, all_9_0_4, all_27_0_16 and discharging atoms j(all_0_3_3) = all_27_0_16, j(all_0_3_3) = all_9_0_4, yields: % 6.74/2.34 | (76) all_27_0_16 = all_9_0_4 % 6.74/2.34 | % 6.74/2.34 | Instantiating formula (15) with all_0_3_3, all_0_2_2, all_25_2_15, all_0_1_1 and discharging atoms op2(all_0_3_3, all_0_2_2) = all_25_2_15, op2(all_0_3_3, all_0_2_2) = all_0_1_1, yields: % 6.74/2.34 | (77) all_25_2_15 = all_0_1_1 % 6.74/2.34 | % 6.74/2.34 | Combining equations (69,72) yields a new equation: % 6.74/2.34 | (78) all_25_0_13 = all_14_0_6 % 6.74/2.34 | % 6.74/2.35 | Simplifying 78 yields: % 6.74/2.35 | (79) all_25_0_13 = all_14_0_6 % 6.74/2.35 | % 6.74/2.35 | Combining equations (74,73) yields a new equation: % 6.74/2.35 | (80) all_23_0_10 = all_18_0_8 % 6.74/2.35 | % 6.74/2.35 | Combining equations (75,73) yields a new equation: % 6.74/2.35 | (81) all_23_0_10 = all_12_0_5 % 6.74/2.35 | % 6.74/2.35 | Combining equations (76,73) yields a new equation: % 6.74/2.35 | (82) all_23_0_10 = all_9_0_4 % 6.74/2.35 | % 6.74/2.35 | Combining equations (79,70) yields a new equation: % 6.74/2.35 | (83) all_20_0_9 = all_14_0_6 % 6.74/2.35 | % 6.74/2.35 | Combining equations (71,70) yields a new equation: % 6.74/2.35 | (84) all_20_0_9 = all_16_0_7 % 6.74/2.35 | % 6.74/2.35 | Combining equations (81,80) yields a new equation: % 6.74/2.35 | (85) all_18_0_8 = all_12_0_5 % 6.74/2.35 | % 6.74/2.35 | Combining equations (82,80) yields a new equation: % 6.74/2.35 | (86) all_18_0_8 = all_9_0_4 % 6.74/2.35 | % 6.74/2.35 | Combining equations (84,83) yields a new equation: % 6.74/2.35 | (87) all_16_0_7 = all_14_0_6 % 6.74/2.35 | % 6.74/2.35 | Simplifying 87 yields: % 6.74/2.35 | (88) all_16_0_7 = all_14_0_6 % 6.74/2.35 | % 6.74/2.35 | Combining equations (85,86) yields a new equation: % 6.74/2.35 | (89) all_12_0_5 = all_9_0_4 % 6.74/2.35 | % 6.74/2.35 | Simplifying 89 yields: % 6.74/2.35 | (90) all_12_0_5 = all_9_0_4 % 6.74/2.35 | % 6.74/2.35 | Combining equations (86,80) yields a new equation: % 6.74/2.35 | (82) all_23_0_10 = all_9_0_4 % 6.74/2.35 | % 6.74/2.35 | Combining equations (83,70) yields a new equation: % 6.74/2.35 | (79) all_25_0_13 = all_14_0_6 % 6.74/2.35 | % 6.74/2.35 | Combining equations (82,73) yields a new equation: % 6.74/2.35 | (76) all_27_0_16 = all_9_0_4 % 6.74/2.35 | % 6.74/2.35 | From (77) and (55) follows: % 6.74/2.35 | (94) j(all_0_1_1) = all_25_1_14 % 6.74/2.35 | % 6.74/2.35 | From (88) and (39) follows: % 6.74/2.35 | (36) j(all_0_2_2) = all_14_0_6 % 6.74/2.35 | % 6.74/2.35 | From (86) and (43) follows: % 6.74/2.35 | (96) h(all_9_0_4) = all_0_3_3 % 6.74/2.35 | % 6.74/2.35 | From (83)(72) and (68) follows: % 6.74/2.35 | (97) op1(all_14_0_6, all_14_0_6) = all_29_1_20 % 6.74/2.35 | % 6.74/2.35 | From (83)(76) and (63) follows: % 6.74/2.35 | (98) op1(all_14_0_6, all_9_0_4) = all_27_1_17 % 6.74/2.35 | % 6.74/2.35 | From (79) and (58) follows: % 6.74/2.35 | (99) op1(all_9_0_4, all_14_0_6) = all_25_1_14 % 6.74/2.35 | % 6.74/2.35 | From (82) and (53) follows: % 6.74/2.35 | (100) op1(all_9_0_4, all_9_0_4) = all_23_1_11 % 6.74/2.35 | % 6.74/2.35 | From (90) and (34) follows: % 6.74/2.35 | (101) sorti1(all_9_0_4) % 6.74/2.35 | % 6.74/2.35 | Instantiating formula (18) with all_29_2_21, all_0_2_2, all_0_2_2 and discharging atoms op2(all_0_2_2, all_0_2_2) = all_29_2_21, sorti2(all_0_2_2), yields: % 6.74/2.35 | (102) sorti2(all_29_2_21) % 6.74/2.35 | % 6.74/2.35 | Instantiating formula (18) with all_27_2_18, all_0_3_3, all_0_2_2 and discharging atoms op2(all_0_2_2, all_0_3_3) = all_27_2_18, sorti2(all_0_2_2), sorti2(all_0_3_3), yields: % 6.74/2.35 | (103) sorti2(all_27_2_18) % 6.74/2.35 | % 6.74/2.35 | Instantiating formula (18) with all_23_2_12, all_0_3_3, all_0_3_3 and discharging atoms op2(all_0_3_3, all_0_3_3) = all_23_2_12, sorti2(all_0_3_3), yields: % 6.74/2.35 | (104) sorti2(all_23_2_12) % 6.74/2.35 | % 6.74/2.35 | Instantiating formula (18) with all_0_0_0, all_0_2_2, all_0_1_1 and discharging atoms op2(all_0_1_1, all_0_2_2) = all_0_0_0, sorti2(all_0_1_1), sorti2(all_0_2_2), yields: % 6.74/2.35 | (105) sorti2(all_0_0_0) % 6.74/2.35 | % 6.74/2.35 | Instantiating formula (46) with all_0_1_1 and discharging atoms sorti2(all_0_1_1), yields: % 6.74/2.35 | (106) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_1_1) = v2 & op2(all_0_2_2, all_0_1_1) = v0 & op1(all_20_0_9, v2) = v1) % 6.74/2.35 | % 6.74/2.35 | Instantiating formula (29) with all_0_1_1 and discharging atoms sorti2(all_0_1_1), yields: % 6.74/2.35 | (107) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_1_1) = v2 & op2(all_0_3_3, all_0_1_1) = v0 & op1(all_9_0_4, v2) = v1) % 6.74/2.35 | % 6.74/2.35 | Instantiating formula (2) with all_0_1_1 and discharging atoms sorti2(all_0_1_1), yields: % 6.74/2.35 | (108) ? [v0] : (j(all_0_1_1) = v0 & h(v0) = all_0_1_1) % 6.74/2.35 | % 6.74/2.35 | Instantiating formula (7) with all_0_1_1 and discharging atoms sorti2(all_0_1_1), yields: % 6.74/2.35 | (109) ? [v0] : (j(all_0_1_1) = v0 & sorti1(v0)) % 6.74/2.35 | % 6.74/2.35 | Instantiating formula (16) with all_0_1_1 and discharging atoms sorti2(all_0_1_1), yields: % 6.74/2.35 | (110) ? [v0] : (j(all_0_1_1) = v0 & ! [v1] : ( ~ sorti2(v1) | ? [v2] : ? [v3] : ? [v4] : (j(v2) = v3 & j(v1) = v4 & op2(all_0_1_1, v1) = v2 & op1(v0, v4) = v3))) % 6.74/2.35 | % 6.74/2.35 | Instantiating formula (6) with all_29_1_20, all_14_0_6, all_14_0_6 and discharging atoms op1(all_14_0_6, all_14_0_6) = all_29_1_20, sorti1(all_14_0_6), yields: % 6.74/2.35 | (111) sorti1(all_29_1_20) % 6.74/2.35 | % 6.74/2.35 | Instantiating formula (14) with all_14_0_6 and discharging atoms sorti1(all_14_0_6), yields: % 6.74/2.35 | (112) ? [v0] : (h(all_14_0_6) = v0 & ! [v1] : ( ~ sorti1(v1) | ? [v2] : ? [v3] : ? [v4] : (h(v2) = v3 & h(v1) = v4 & op2(v0, v4) = v3 & op1(all_14_0_6, v1) = v2))) % 6.74/2.35 | % 6.74/2.35 | Instantiating formula (6) with all_27_1_17, all_9_0_4, all_14_0_6 and discharging atoms op1(all_14_0_6, all_9_0_4) = all_27_1_17, sorti1(all_14_0_6), sorti1(all_9_0_4), yields: % 6.74/2.36 | (113) sorti1(all_27_1_17) % 6.74/2.36 | % 6.74/2.36 | Instantiating formula (6) with all_23_1_11, all_9_0_4, all_9_0_4 and discharging atoms op1(all_9_0_4, all_9_0_4) = all_23_1_11, sorti1(all_9_0_4), yields: % 6.74/2.36 | (114) sorti1(all_23_1_11) % 6.74/2.36 | % 6.74/2.36 | Instantiating formula (14) with all_9_0_4 and discharging atoms sorti1(all_9_0_4), yields: % 6.74/2.36 | (115) ? [v0] : (h(all_9_0_4) = v0 & ! [v1] : ( ~ sorti1(v1) | ? [v2] : ? [v3] : ? [v4] : (h(v2) = v3 & h(v1) = v4 & op2(v0, v4) = v3 & op1(all_9_0_4, v1) = v2))) % 6.74/2.36 | % 6.74/2.36 | Instantiating (115) with all_41_0_22 yields: % 6.74/2.36 | (116) h(all_9_0_4) = all_41_0_22 & ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_41_0_22, v3) = v2 & op1(all_9_0_4, v0) = v1)) % 6.74/2.36 | % 6.74/2.36 | Applying alpha-rule on (116) yields: % 6.74/2.36 | (117) h(all_9_0_4) = all_41_0_22 % 6.74/2.36 | (118) ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_41_0_22, v3) = v2 & op1(all_9_0_4, v0) = v1)) % 6.74/2.36 | % 6.74/2.36 | Instantiating formula (118) with all_14_0_6 and discharging atoms sorti1(all_14_0_6), yields: % 6.74/2.36 | (119) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_14_0_6) = v2 & op2(all_41_0_22, v2) = v1 & op1(all_9_0_4, all_14_0_6) = v0) % 6.74/2.36 | % 6.74/2.36 | Instantiating formula (118) with all_9_0_4 and discharging atoms sorti1(all_9_0_4), yields: % 6.74/2.36 | (120) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_9_0_4) = v2 & op2(all_41_0_22, v2) = v1 & op1(all_9_0_4, all_9_0_4) = v0) % 6.74/2.36 | % 6.74/2.36 | Instantiating (110) with all_44_0_23 yields: % 6.74/2.36 | (121) j(all_0_1_1) = all_44_0_23 & ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_0_1_1, v0) = v1 & op1(all_44_0_23, v3) = v2)) % 6.74/2.36 | % 6.74/2.36 | Applying alpha-rule on (121) yields: % 6.74/2.36 | (122) j(all_0_1_1) = all_44_0_23 % 6.74/2.36 | (123) ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_0_1_1, v0) = v1 & op1(all_44_0_23, v3) = v2)) % 6.74/2.36 | % 6.74/2.36 | Instantiating formula (123) with all_0_1_1 and discharging atoms sorti2(all_0_1_1), yields: % 6.74/2.36 | (124) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_1_1) = v2 & op2(all_0_1_1, all_0_1_1) = v0 & op1(all_44_0_23, v2) = v1) % 6.74/2.36 | % 6.74/2.36 | Instantiating formula (123) with all_0_2_2 and discharging atoms sorti2(all_0_2_2), yields: % 6.74/2.36 | (125) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_2_2) = v2 & op2(all_0_1_1, all_0_2_2) = v0 & op1(all_44_0_23, v2) = v1) % 6.74/2.36 | % 6.74/2.36 | Instantiating (112) with all_47_0_24 yields: % 6.74/2.36 | (126) h(all_14_0_6) = all_47_0_24 & ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_47_0_24, v3) = v2 & op1(all_14_0_6, v0) = v1)) % 6.74/2.36 | % 6.74/2.36 | Applying alpha-rule on (126) yields: % 6.74/2.36 | (127) h(all_14_0_6) = all_47_0_24 % 6.74/2.36 | (128) ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_47_0_24, v3) = v2 & op1(all_14_0_6, v0) = v1)) % 6.74/2.36 | % 6.74/2.36 | Instantiating formula (128) with all_9_0_4 and discharging atoms sorti1(all_9_0_4), yields: % 6.74/2.36 | (129) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_9_0_4) = v2 & op2(all_47_0_24, v2) = v1 & op1(all_14_0_6, all_9_0_4) = v0) % 6.74/2.36 | % 6.74/2.36 | Instantiating (109) with all_50_0_25 yields: % 6.74/2.36 | (130) j(all_0_1_1) = all_50_0_25 & sorti1(all_50_0_25) % 6.74/2.36 | % 6.74/2.36 | Applying alpha-rule on (130) yields: % 6.74/2.36 | (131) j(all_0_1_1) = all_50_0_25 % 6.74/2.36 | (132) sorti1(all_50_0_25) % 6.74/2.36 | % 6.74/2.36 | Instantiating (108) with all_52_0_26 yields: % 6.74/2.36 | (133) j(all_0_1_1) = all_52_0_26 & h(all_52_0_26) = all_0_1_1 % 6.74/2.36 | % 6.74/2.36 | Applying alpha-rule on (133) yields: % 6.74/2.36 | (134) j(all_0_1_1) = all_52_0_26 % 6.74/2.36 | (135) h(all_52_0_26) = all_0_1_1 % 6.74/2.36 | % 6.74/2.36 | Instantiating (107) with all_54_0_27, all_54_1_28, all_54_2_29 yields: % 6.74/2.36 | (136) j(all_54_2_29) = all_54_1_28 & j(all_0_1_1) = all_54_0_27 & op2(all_0_3_3, all_0_1_1) = all_54_2_29 & op1(all_9_0_4, all_54_0_27) = all_54_1_28 % 6.74/2.36 | % 6.74/2.37 | Applying alpha-rule on (136) yields: % 6.74/2.37 | (137) j(all_54_2_29) = all_54_1_28 % 6.74/2.37 | (138) j(all_0_1_1) = all_54_0_27 % 6.74/2.37 | (139) op2(all_0_3_3, all_0_1_1) = all_54_2_29 % 6.74/2.37 | (140) op1(all_9_0_4, all_54_0_27) = all_54_1_28 % 6.74/2.37 | % 6.74/2.37 | Instantiating (106) with all_56_0_30, all_56_1_31, all_56_2_32 yields: % 6.74/2.37 | (141) j(all_56_2_32) = all_56_1_31 & j(all_0_1_1) = all_56_0_30 & op2(all_0_2_2, all_0_1_1) = all_56_2_32 & op1(all_20_0_9, all_56_0_30) = all_56_1_31 % 6.74/2.37 | % 6.74/2.37 | Applying alpha-rule on (141) yields: % 6.74/2.37 | (142) j(all_56_2_32) = all_56_1_31 % 6.74/2.37 | (143) j(all_0_1_1) = all_56_0_30 % 6.74/2.37 | (144) op2(all_0_2_2, all_0_1_1) = all_56_2_32 % 6.74/2.37 | (145) op1(all_20_0_9, all_56_0_30) = all_56_1_31 % 6.74/2.37 | % 6.74/2.37 | Instantiating (120) with all_58_0_33, all_58_1_34, all_58_2_35 yields: % 6.74/2.37 | (146) h(all_58_2_35) = all_58_1_34 & h(all_9_0_4) = all_58_0_33 & op2(all_41_0_22, all_58_0_33) = all_58_1_34 & op1(all_9_0_4, all_9_0_4) = all_58_2_35 % 6.74/2.37 | % 6.74/2.37 | Applying alpha-rule on (146) yields: % 6.74/2.37 | (147) h(all_58_2_35) = all_58_1_34 % 6.74/2.37 | (148) h(all_9_0_4) = all_58_0_33 % 6.74/2.37 | (149) op2(all_41_0_22, all_58_0_33) = all_58_1_34 % 6.74/2.37 | (150) op1(all_9_0_4, all_9_0_4) = all_58_2_35 % 6.74/2.37 | % 6.74/2.37 | Instantiating (119) with all_60_0_36, all_60_1_37, all_60_2_38 yields: % 6.74/2.37 | (151) h(all_60_2_38) = all_60_1_37 & h(all_14_0_6) = all_60_0_36 & op2(all_41_0_22, all_60_0_36) = all_60_1_37 & op1(all_9_0_4, all_14_0_6) = all_60_2_38 % 6.74/2.37 | % 6.74/2.37 | Applying alpha-rule on (151) yields: % 6.74/2.37 | (152) h(all_60_2_38) = all_60_1_37 % 6.74/2.37 | (153) h(all_14_0_6) = all_60_0_36 % 6.74/2.37 | (154) op2(all_41_0_22, all_60_0_36) = all_60_1_37 % 6.74/2.37 | (155) op1(all_9_0_4, all_14_0_6) = all_60_2_38 % 6.74/2.37 | % 6.74/2.37 | Instantiating (125) with all_64_0_42, all_64_1_43, all_64_2_44 yields: % 6.74/2.37 | (156) j(all_64_2_44) = all_64_1_43 & j(all_0_2_2) = all_64_0_42 & op2(all_0_1_1, all_0_2_2) = all_64_2_44 & op1(all_44_0_23, all_64_0_42) = all_64_1_43 % 6.74/2.37 | % 6.74/2.37 | Applying alpha-rule on (156) yields: % 6.74/2.37 | (157) j(all_64_2_44) = all_64_1_43 % 6.74/2.37 | (158) j(all_0_2_2) = all_64_0_42 % 6.74/2.37 | (159) op2(all_0_1_1, all_0_2_2) = all_64_2_44 % 6.74/2.37 | (160) op1(all_44_0_23, all_64_0_42) = all_64_1_43 % 6.74/2.37 | % 6.74/2.37 | Instantiating (124) with all_66_0_45, all_66_1_46, all_66_2_47 yields: % 6.74/2.37 | (161) j(all_66_2_47) = all_66_1_46 & j(all_0_1_1) = all_66_0_45 & op2(all_0_1_1, all_0_1_1) = all_66_2_47 & op1(all_44_0_23, all_66_0_45) = all_66_1_46 % 6.74/2.37 | % 6.74/2.37 | Applying alpha-rule on (161) yields: % 6.74/2.37 | (162) j(all_66_2_47) = all_66_1_46 % 6.74/2.37 | (163) j(all_0_1_1) = all_66_0_45 % 6.74/2.37 | (164) op2(all_0_1_1, all_0_1_1) = all_66_2_47 % 6.74/2.37 | (165) op1(all_44_0_23, all_66_0_45) = all_66_1_46 % 6.74/2.37 | % 6.74/2.37 | Instantiating (129) with all_68_0_48, all_68_1_49, all_68_2_50 yields: % 6.74/2.37 | (166) h(all_68_2_50) = all_68_1_49 & h(all_9_0_4) = all_68_0_48 & op2(all_47_0_24, all_68_0_48) = all_68_1_49 & op1(all_14_0_6, all_9_0_4) = all_68_2_50 % 6.74/2.37 | % 6.74/2.37 | Applying alpha-rule on (166) yields: % 6.74/2.37 | (167) h(all_68_2_50) = all_68_1_49 % 6.74/2.37 | (168) h(all_9_0_4) = all_68_0_48 % 6.74/2.37 | (169) op2(all_47_0_24, all_68_0_48) = all_68_1_49 % 6.74/2.37 | (170) op1(all_14_0_6, all_9_0_4) = all_68_2_50 % 6.74/2.37 | % 6.74/2.37 | Instantiating formula (13) with all_0_1_1, all_56_0_30, all_66_0_45 and discharging atoms j(all_0_1_1) = all_66_0_45, j(all_0_1_1) = all_56_0_30, yields: % 6.74/2.37 | (171) all_66_0_45 = all_56_0_30 % 6.74/2.37 | % 6.74/2.37 | Instantiating formula (13) with all_0_1_1, all_54_0_27, all_66_0_45 and discharging atoms j(all_0_1_1) = all_66_0_45, j(all_0_1_1) = all_54_0_27, yields: % 6.74/2.37 | (172) all_66_0_45 = all_54_0_27 % 6.74/2.37 | % 6.74/2.37 | Instantiating formula (13) with all_0_1_1, all_52_0_26, all_25_1_14 and discharging atoms j(all_0_1_1) = all_52_0_26, j(all_0_1_1) = all_25_1_14, yields: % 6.74/2.37 | (173) all_52_0_26 = all_25_1_14 % 6.74/2.37 | % 6.74/2.37 | Instantiating formula (13) with all_0_1_1, all_52_0_26, all_66_0_45 and discharging atoms j(all_0_1_1) = all_66_0_45, j(all_0_1_1) = all_52_0_26, yields: % 6.74/2.37 | (174) all_66_0_45 = all_52_0_26 % 6.74/2.37 | % 6.74/2.37 | Instantiating formula (13) with all_0_1_1, all_50_0_25, all_56_0_30 and discharging atoms j(all_0_1_1) = all_56_0_30, j(all_0_1_1) = all_50_0_25, yields: % 6.74/2.37 | (175) all_56_0_30 = all_50_0_25 % 6.74/2.37 | % 6.74/2.37 | Instantiating formula (13) with all_0_1_1, all_44_0_23, all_52_0_26 and discharging atoms j(all_0_1_1) = all_52_0_26, j(all_0_1_1) = all_44_0_23, yields: % 6.74/2.38 | (176) all_52_0_26 = all_44_0_23 % 6.74/2.38 | % 6.74/2.38 | Instantiating formula (13) with all_0_2_2, all_64_0_42, all_14_0_6 and discharging atoms j(all_0_2_2) = all_64_0_42, j(all_0_2_2) = all_14_0_6, yields: % 6.74/2.38 | (177) all_64_0_42 = all_14_0_6 % 6.74/2.38 | % 6.74/2.38 | Instantiating formula (5) with all_9_0_4, all_68_0_48, all_0_3_3 and discharging atoms h(all_9_0_4) = all_68_0_48, h(all_9_0_4) = all_0_3_3, yields: % 6.74/2.38 | (178) all_68_0_48 = all_0_3_3 % 6.74/2.38 | % 6.74/2.38 | Instantiating formula (5) with all_9_0_4, all_58_0_33, all_68_0_48 and discharging atoms h(all_9_0_4) = all_68_0_48, h(all_9_0_4) = all_58_0_33, yields: % 6.74/2.38 | (179) all_68_0_48 = all_58_0_33 % 6.74/2.38 | % 6.74/2.38 | Instantiating formula (5) with all_9_0_4, all_41_0_22, all_58_0_33 and discharging atoms h(all_9_0_4) = all_58_0_33, h(all_9_0_4) = all_41_0_22, yields: % 6.74/2.38 | (180) all_58_0_33 = all_41_0_22 % 6.74/2.38 | % 6.74/2.38 | Instantiating formula (15) with all_0_1_1, all_0_2_2, all_64_2_44, all_0_0_0 and discharging atoms op2(all_0_1_1, all_0_2_2) = all_64_2_44, op2(all_0_1_1, all_0_2_2) = all_0_0_0, yields: % 6.74/2.38 | (181) all_64_2_44 = all_0_0_0 % 6.74/2.38 | % 6.74/2.38 | Instantiating formula (4) with all_9_0_4, all_14_0_6, all_60_2_38, all_25_1_14 and discharging atoms op1(all_9_0_4, all_14_0_6) = all_60_2_38, op1(all_9_0_4, all_14_0_6) = all_25_1_14, yields: % 6.74/2.38 | (182) all_60_2_38 = all_25_1_14 % 6.74/2.38 | % 6.74/2.38 | Instantiating formula (4) with all_9_0_4, all_9_0_4, all_58_2_35, all_23_1_11 and discharging atoms op1(all_9_0_4, all_9_0_4) = all_58_2_35, op1(all_9_0_4, all_9_0_4) = all_23_1_11, yields: % 6.74/2.38 | (183) all_58_2_35 = all_23_1_11 % 6.74/2.38 | % 6.74/2.38 | Combining equations (179,178) yields a new equation: % 6.74/2.38 | (184) all_58_0_33 = all_0_3_3 % 6.74/2.38 | % 6.74/2.38 | Simplifying 184 yields: % 6.74/2.38 | (185) all_58_0_33 = all_0_3_3 % 6.74/2.38 | % 6.74/2.38 | Combining equations (174,172) yields a new equation: % 6.74/2.38 | (186) all_54_0_27 = all_52_0_26 % 6.74/2.38 | % 6.74/2.38 | Combining equations (171,172) yields a new equation: % 6.74/2.38 | (187) all_56_0_30 = all_54_0_27 % 6.74/2.38 | % 6.74/2.38 | Simplifying 187 yields: % 6.74/2.38 | (188) all_56_0_30 = all_54_0_27 % 6.74/2.38 | % 6.74/2.38 | Combining equations (180,185) yields a new equation: % 6.74/2.38 | (189) all_41_0_22 = all_0_3_3 % 6.74/2.38 | % 6.74/2.38 | Simplifying 189 yields: % 6.74/2.38 | (190) all_41_0_22 = all_0_3_3 % 6.74/2.38 | % 6.74/2.38 | Combining equations (188,175) yields a new equation: % 6.74/2.38 | (191) all_54_0_27 = all_50_0_25 % 6.74/2.38 | % 6.74/2.38 | Simplifying 191 yields: % 6.74/2.38 | (192) all_54_0_27 = all_50_0_25 % 6.74/2.38 | % 6.74/2.38 | Combining equations (186,192) yields a new equation: % 6.74/2.38 | (193) all_52_0_26 = all_50_0_25 % 6.74/2.38 | % 6.74/2.38 | Simplifying 193 yields: % 6.74/2.38 | (194) all_52_0_26 = all_50_0_25 % 6.74/2.38 | % 6.74/2.38 | Combining equations (173,194) yields a new equation: % 6.74/2.38 | (195) all_50_0_25 = all_25_1_14 % 6.74/2.38 | % 6.74/2.38 | Combining equations (176,194) yields a new equation: % 6.74/2.38 | (196) all_50_0_25 = all_44_0_23 % 6.74/2.38 | % 7.20/2.38 | Combining equations (195,196) yields a new equation: % 7.20/2.38 | (197) all_44_0_23 = all_25_1_14 % 7.20/2.38 | % 7.20/2.38 | Combining equations (197,196) yields a new equation: % 7.20/2.38 | (195) all_50_0_25 = all_25_1_14 % 7.20/2.38 | % 7.20/2.38 | From (181) and (157) follows: % 7.20/2.38 | (199) j(all_0_0_0) = all_64_1_43 % 7.20/2.38 | % 7.20/2.38 | From (190) and (117) follows: % 7.20/2.38 | (96) h(all_9_0_4) = all_0_3_3 % 7.20/2.38 | % 7.20/2.38 | From (197)(177) and (160) follows: % 7.20/2.38 | (201) op1(all_25_1_14, all_14_0_6) = all_64_1_43 % 7.20/2.38 | % 7.20/2.38 | From (182) and (155) follows: % 7.20/2.38 | (99) op1(all_9_0_4, all_14_0_6) = all_25_1_14 % 7.20/2.38 | % 7.20/2.38 | From (183) and (150) follows: % 7.20/2.38 | (100) op1(all_9_0_4, all_9_0_4) = all_23_1_11 % 7.20/2.38 | % 7.20/2.38 | From (195) and (132) follows: % 7.20/2.38 | (204) sorti1(all_25_1_14) % 7.20/2.38 | % 7.20/2.38 | Instantiating formula (19) with all_64_1_43, all_25_1_14, all_14_0_6, all_9_0_4 and discharging atoms op1(all_25_1_14, all_14_0_6) = all_64_1_43, op1(all_9_0_4, all_14_0_6) = all_25_1_14, sorti1(all_14_0_6), sorti1(all_9_0_4), yields: % 7.20/2.38 | (205) all_64_1_43 = all_9_0_4 % 7.20/2.38 | % 7.20/2.38 | From (205) and (199) follows: % 7.20/2.38 | (206) j(all_0_0_0) = all_9_0_4 % 7.20/2.38 | % 7.20/2.38 | Instantiating formula (16) with all_29_2_21 and discharging atoms sorti2(all_29_2_21), yields: % 7.20/2.38 | (207) ? [v0] : (j(all_29_2_21) = v0 & ! [v1] : ( ~ sorti2(v1) | ? [v2] : ? [v3] : ? [v4] : (j(v2) = v3 & j(v1) = v4 & op2(all_29_2_21, v1) = v2 & op1(v0, v4) = v3))) % 7.20/2.39 | % 7.20/2.39 | Instantiating formula (16) with all_27_2_18 and discharging atoms sorti2(all_27_2_18), yields: % 7.20/2.39 | (208) ? [v0] : (j(all_27_2_18) = v0 & ! [v1] : ( ~ sorti2(v1) | ? [v2] : ? [v3] : ? [v4] : (j(v2) = v3 & j(v1) = v4 & op2(all_27_2_18, v1) = v2 & op1(v0, v4) = v3))) % 7.20/2.39 | % 7.20/2.39 | Instantiating formula (16) with all_23_2_12 and discharging atoms sorti2(all_23_2_12), yields: % 7.20/2.39 | (209) ? [v0] : (j(all_23_2_12) = v0 & ! [v1] : ( ~ sorti2(v1) | ? [v2] : ? [v3] : ? [v4] : (j(v2) = v3 & j(v1) = v4 & op2(all_23_2_12, v1) = v2 & op1(v0, v4) = v3))) % 7.20/2.39 | % 7.20/2.39 | Instantiating formula (123) with all_0_0_0 and discharging atoms sorti2(all_0_0_0), yields: % 7.20/2.39 | (210) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_0_0) = v2 & op2(all_0_1_1, all_0_0_0) = v0 & op1(all_44_0_23, v2) = v1) % 7.20/2.39 | % 7.20/2.39 | Instantiating formula (46) with all_0_0_0 and discharging atoms sorti2(all_0_0_0), yields: % 7.20/2.39 | (211) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_0_0) = v2 & op2(all_0_2_2, all_0_0_0) = v0 & op1(all_20_0_9, v2) = v1) % 7.20/2.39 | % 7.20/2.39 | Instantiating formula (29) with all_0_0_0 and discharging atoms sorti2(all_0_0_0), yields: % 7.20/2.39 | (212) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_0_0) = v2 & op2(all_0_3_3, all_0_0_0) = v0 & op1(all_9_0_4, v2) = v1) % 7.20/2.39 | % 7.20/2.39 | Instantiating formula (2) with all_0_0_0 and discharging atoms sorti2(all_0_0_0), yields: % 7.20/2.39 | (213) ? [v0] : (j(all_0_0_0) = v0 & h(v0) = all_0_0_0) % 7.20/2.39 | % 7.20/2.39 | Instantiating formula (16) with all_0_0_0 and discharging atoms sorti2(all_0_0_0), yields: % 7.20/2.39 | (214) ? [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))) % 7.20/2.39 | % 7.20/2.39 | Instantiating formula (14) with all_29_1_20 and discharging atoms sorti1(all_29_1_20), yields: % 7.20/2.39 | (215) ? [v0] : (h(all_29_1_20) = v0 & ! [v1] : ( ~ sorti1(v1) | ? [v2] : ? [v3] : ? [v4] : (h(v2) = v3 & h(v1) = v4 & op2(v0, v4) = v3 & op1(all_29_1_20, v1) = v2))) % 7.20/2.39 | % 7.20/2.39 | Instantiating formula (14) with all_27_1_17 and discharging atoms sorti1(all_27_1_17), yields: % 7.20/2.39 | (216) ? [v0] : (h(all_27_1_17) = v0 & ! [v1] : ( ~ sorti1(v1) | ? [v2] : ? [v3] : ? [v4] : (h(v2) = v3 & h(v1) = v4 & op2(v0, v4) = v3 & op1(all_27_1_17, v1) = v2))) % 7.20/2.39 | % 7.20/2.39 | Instantiating formula (14) with all_25_1_14 and discharging atoms sorti1(all_25_1_14), yields: % 7.20/2.39 | (217) ? [v0] : (h(all_25_1_14) = v0 & ! [v1] : ( ~ sorti1(v1) | ? [v2] : ? [v3] : ? [v4] : (h(v2) = v3 & h(v1) = v4 & op2(v0, v4) = v3 & op1(all_25_1_14, v1) = v2))) % 7.20/2.39 | % 7.20/2.39 | Instantiating formula (14) with all_23_1_11 and discharging atoms sorti1(all_23_1_11), yields: % 7.20/2.39 | (218) ? [v0] : (h(all_23_1_11) = v0 & ! [v1] : ( ~ sorti1(v1) | ? [v2] : ? [v3] : ? [v4] : (h(v2) = v3 & h(v1) = v4 & op2(v0, v4) = v3 & op1(all_23_1_11, v1) = v2))) % 7.20/2.39 | % 7.20/2.39 | Instantiating (207) with all_86_0_54 yields: % 7.20/2.39 | (219) j(all_29_2_21) = all_86_0_54 & ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_29_2_21, v0) = v1 & op1(all_86_0_54, v3) = v2)) % 7.20/2.39 | % 7.20/2.39 | Applying alpha-rule on (219) yields: % 7.20/2.39 | (220) j(all_29_2_21) = all_86_0_54 % 7.20/2.39 | (221) ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_29_2_21, v0) = v1 & op1(all_86_0_54, v3) = v2)) % 7.20/2.39 | % 7.20/2.39 | Instantiating formula (221) with all_0_0_0 and discharging atoms sorti2(all_0_0_0), yields: % 7.20/2.39 | (222) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_0_0) = v2 & op2(all_29_2_21, all_0_0_0) = v0 & op1(all_86_0_54, v2) = v1) % 7.20/2.39 | % 7.20/2.39 | Instantiating (218) with all_99_0_70 yields: % 7.20/2.39 | (223) h(all_23_1_11) = all_99_0_70 & ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_99_0_70, v3) = v2 & op1(all_23_1_11, v0) = v1)) % 7.20/2.39 | % 7.20/2.39 | Applying alpha-rule on (223) yields: % 7.20/2.39 | (224) h(all_23_1_11) = all_99_0_70 % 7.20/2.39 | (225) ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_99_0_70, v3) = v2 & op1(all_23_1_11, v0) = v1)) % 7.20/2.39 | % 7.20/2.39 | Instantiating formula (225) with all_9_0_4 and discharging atoms sorti1(all_9_0_4), yields: % 7.20/2.39 | (226) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_9_0_4) = v2 & op2(all_99_0_70, v2) = v1 & op1(all_23_1_11, all_9_0_4) = v0) % 7.20/2.39 | % 7.20/2.39 | Instantiating (217) with all_104_0_74 yields: % 7.20/2.39 | (227) h(all_25_1_14) = all_104_0_74 & ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_104_0_74, v3) = v2 & op1(all_25_1_14, v0) = v1)) % 7.20/2.39 | % 7.20/2.39 | Applying alpha-rule on (227) yields: % 7.20/2.39 | (228) h(all_25_1_14) = all_104_0_74 % 7.20/2.39 | (229) ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_104_0_74, v3) = v2 & op1(all_25_1_14, v0) = v1)) % 7.20/2.39 | % 7.20/2.39 | Instantiating formula (229) with all_14_0_6 and discharging atoms sorti1(all_14_0_6), yields: % 7.20/2.39 | (230) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_14_0_6) = v2 & op2(all_104_0_74, v2) = v1 & op1(all_25_1_14, all_14_0_6) = v0) % 7.20/2.39 | % 7.20/2.39 | Instantiating formula (229) with all_9_0_4 and discharging atoms sorti1(all_9_0_4), yields: % 7.20/2.39 | (231) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_9_0_4) = v2 & op2(all_104_0_74, v2) = v1 & op1(all_25_1_14, all_9_0_4) = v0) % 7.20/2.39 | % 7.20/2.39 | Instantiating (215) with all_111_0_81 yields: % 7.20/2.39 | (232) h(all_29_1_20) = all_111_0_81 & ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_111_0_81, v3) = v2 & op1(all_29_1_20, v0) = v1)) % 7.20/2.39 | % 7.20/2.39 | Applying alpha-rule on (232) yields: % 7.20/2.39 | (233) h(all_29_1_20) = all_111_0_81 % 7.20/2.39 | (234) ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_111_0_81, v3) = v2 & op1(all_29_1_20, v0) = v1)) % 7.20/2.40 | % 7.20/2.40 | Instantiating formula (234) with all_9_0_4 and discharging atoms sorti1(all_9_0_4), yields: % 7.20/2.40 | (235) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_9_0_4) = v2 & op2(all_111_0_81, v2) = v1 & op1(all_29_1_20, all_9_0_4) = v0) % 7.20/2.40 | % 7.20/2.40 | Instantiating (209) with all_116_0_85 yields: % 7.20/2.40 | (236) j(all_23_2_12) = all_116_0_85 & ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_23_2_12, v0) = v1 & op1(all_116_0_85, v3) = v2)) % 7.20/2.40 | % 7.20/2.40 | Applying alpha-rule on (236) yields: % 7.20/2.40 | (237) j(all_23_2_12) = all_116_0_85 % 7.20/2.40 | (238) ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_23_2_12, v0) = v1 & op1(all_116_0_85, v3) = v2)) % 7.20/2.40 | % 7.20/2.40 | Instantiating formula (238) with all_0_0_0 and discharging atoms sorti2(all_0_0_0), yields: % 7.20/2.40 | (239) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_0_0) = v2 & op2(all_23_2_12, all_0_0_0) = v0 & op1(all_116_0_85, v2) = v1) % 7.20/2.40 | % 7.20/2.40 | Instantiating (208) with all_121_0_89 yields: % 7.20/2.40 | (240) j(all_27_2_18) = all_121_0_89 & ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_27_2_18, v0) = v1 & op1(all_121_0_89, v3) = v2)) % 7.20/2.40 | % 7.20/2.40 | Applying alpha-rule on (240) yields: % 7.20/2.40 | (241) j(all_27_2_18) = all_121_0_89 % 7.20/2.40 | (242) ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_27_2_18, v0) = v1 & op1(all_121_0_89, v3) = v2)) % 7.20/2.40 | % 7.20/2.40 | Instantiating formula (242) with all_0_0_0 and discharging atoms sorti2(all_0_0_0), yields: % 7.20/2.40 | (243) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_0_0) = v2 & op2(all_27_2_18, all_0_0_0) = v0 & op1(all_121_0_89, v2) = v1) % 7.20/2.40 | % 7.20/2.40 | Instantiating (213) with all_134_0_105 yields: % 7.20/2.40 | (244) j(all_0_0_0) = all_134_0_105 & h(all_134_0_105) = all_0_0_0 % 7.20/2.40 | % 7.20/2.40 | Applying alpha-rule on (244) yields: % 7.20/2.40 | (245) j(all_0_0_0) = all_134_0_105 % 7.20/2.40 | (246) h(all_134_0_105) = all_0_0_0 % 7.20/2.40 | % 7.20/2.40 | Instantiating (212) with all_136_0_106, all_136_1_107, all_136_2_108 yields: % 7.20/2.40 | (247) j(all_136_2_108) = all_136_1_107 & j(all_0_0_0) = all_136_0_106 & op2(all_0_3_3, all_0_0_0) = all_136_2_108 & op1(all_9_0_4, all_136_0_106) = all_136_1_107 % 7.20/2.40 | % 7.20/2.40 | Applying alpha-rule on (247) yields: % 7.20/2.40 | (248) j(all_136_2_108) = all_136_1_107 % 7.20/2.40 | (249) j(all_0_0_0) = all_136_0_106 % 7.20/2.40 | (250) op2(all_0_3_3, all_0_0_0) = all_136_2_108 % 7.20/2.40 | (251) op1(all_9_0_4, all_136_0_106) = all_136_1_107 % 7.20/2.40 | % 7.20/2.40 | Instantiating (214) with all_140_0_112 yields: % 7.20/2.40 | (252) j(all_0_0_0) = all_140_0_112 & ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_0_0_0, v0) = v1 & op1(all_140_0_112, v3) = v2)) % 7.20/2.40 | % 7.20/2.40 | Applying alpha-rule on (252) yields: % 7.20/2.40 | (253) j(all_0_0_0) = all_140_0_112 % 7.20/2.40 | (254) ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_0_0_0, v0) = v1 & op1(all_140_0_112, v3) = v2)) % 7.20/2.40 | % 7.20/2.40 | Instantiating formula (254) with all_0_0_0 and discharging atoms sorti2(all_0_0_0), yields: % 7.20/2.40 | (255) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_0_0_0) = v2 & op2(all_0_0_0, all_0_0_0) = v0 & op1(all_140_0_112, v2) = v1) % 7.20/2.40 | % 7.20/2.40 | Instantiating (216) with all_145_0_116 yields: % 7.20/2.40 | (256) h(all_27_1_17) = all_145_0_116 & ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_145_0_116, v3) = v2 & op1(all_27_1_17, v0) = v1)) % 7.20/2.40 | % 7.20/2.40 | Applying alpha-rule on (256) yields: % 7.20/2.40 | (257) h(all_27_1_17) = all_145_0_116 % 7.20/2.40 | (258) ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_145_0_116, v3) = v2 & op1(all_27_1_17, v0) = v1)) % 7.20/2.40 | % 7.20/2.40 | Instantiating formula (258) with all_9_0_4 and discharging atoms sorti1(all_9_0_4), yields: % 7.20/2.40 | (259) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_9_0_4) = v2 & op2(all_145_0_116, v2) = v1 & op1(all_27_1_17, all_9_0_4) = v0) % 7.20/2.40 | % 7.20/2.40 | Instantiating (211) with all_148_0_117, all_148_1_118, all_148_2_119 yields: % 7.20/2.40 | (260) j(all_148_2_119) = all_148_1_118 & j(all_0_0_0) = all_148_0_117 & op2(all_0_2_2, all_0_0_0) = all_148_2_119 & op1(all_20_0_9, all_148_0_117) = all_148_1_118 % 7.20/2.40 | % 7.20/2.40 | Applying alpha-rule on (260) yields: % 7.20/2.40 | (261) j(all_148_2_119) = all_148_1_118 % 7.20/2.40 | (262) j(all_0_0_0) = all_148_0_117 % 7.20/2.40 | (263) op2(all_0_2_2, all_0_0_0) = all_148_2_119 % 7.20/2.40 | (264) op1(all_20_0_9, all_148_0_117) = all_148_1_118 % 7.20/2.40 | % 7.20/2.40 | Instantiating (210) with all_150_0_120, all_150_1_121, all_150_2_122 yields: % 7.20/2.40 | (265) j(all_150_2_122) = all_150_1_121 & j(all_0_0_0) = all_150_0_120 & op2(all_0_1_1, all_0_0_0) = all_150_2_122 & op1(all_44_0_23, all_150_0_120) = all_150_1_121 % 7.20/2.40 | % 7.20/2.40 | Applying alpha-rule on (265) yields: % 7.20/2.40 | (266) j(all_150_2_122) = all_150_1_121 % 7.20/2.40 | (267) j(all_0_0_0) = all_150_0_120 % 7.20/2.40 | (268) op2(all_0_1_1, all_0_0_0) = all_150_2_122 % 7.20/2.40 | (269) op1(all_44_0_23, all_150_0_120) = all_150_1_121 % 7.20/2.40 | % 7.20/2.40 | Instantiating (222) with all_154_0_126, all_154_1_127, all_154_2_128 yields: % 7.20/2.40 | (270) j(all_154_2_128) = all_154_1_127 & j(all_0_0_0) = all_154_0_126 & op2(all_29_2_21, all_0_0_0) = all_154_2_128 & op1(all_86_0_54, all_154_0_126) = all_154_1_127 % 7.20/2.40 | % 7.20/2.40 | Applying alpha-rule on (270) yields: % 7.20/2.40 | (271) j(all_154_2_128) = all_154_1_127 % 7.20/2.40 | (272) j(all_0_0_0) = all_154_0_126 % 7.20/2.40 | (273) op2(all_29_2_21, all_0_0_0) = all_154_2_128 % 7.20/2.40 | (274) op1(all_86_0_54, all_154_0_126) = all_154_1_127 % 7.20/2.40 | % 7.20/2.40 | Instantiating (226) with all_166_0_144, all_166_1_145, all_166_2_146 yields: % 7.20/2.40 | (275) h(all_166_2_146) = all_166_1_145 & h(all_9_0_4) = all_166_0_144 & op2(all_99_0_70, all_166_0_144) = all_166_1_145 & op1(all_23_1_11, all_9_0_4) = all_166_2_146 % 7.20/2.40 | % 7.20/2.40 | Applying alpha-rule on (275) yields: % 7.20/2.40 | (276) h(all_166_2_146) = all_166_1_145 % 7.20/2.40 | (277) h(all_9_0_4) = all_166_0_144 % 7.20/2.40 | (278) op2(all_99_0_70, all_166_0_144) = all_166_1_145 % 7.20/2.40 | (279) op1(all_23_1_11, all_9_0_4) = all_166_2_146 % 7.20/2.40 | % 7.20/2.40 | Instantiating (231) with all_178_0_162, all_178_1_163, all_178_2_164 yields: % 7.20/2.40 | (280) h(all_178_2_164) = all_178_1_163 & h(all_9_0_4) = all_178_0_162 & op2(all_104_0_74, all_178_0_162) = all_178_1_163 & op1(all_25_1_14, all_9_0_4) = all_178_2_164 % 7.20/2.40 | % 7.20/2.40 | Applying alpha-rule on (280) yields: % 7.20/2.40 | (281) h(all_178_2_164) = all_178_1_163 % 7.20/2.40 | (282) h(all_9_0_4) = all_178_0_162 % 7.20/2.40 | (283) op2(all_104_0_74, all_178_0_162) = all_178_1_163 % 7.20/2.40 | (284) op1(all_25_1_14, all_9_0_4) = all_178_2_164 % 7.20/2.40 | % 7.20/2.40 | Instantiating (230) with all_188_0_177, all_188_1_178, all_188_2_179 yields: % 7.31/2.40 | (285) h(all_188_2_179) = all_188_1_178 & h(all_14_0_6) = all_188_0_177 & op2(all_104_0_74, all_188_0_177) = all_188_1_178 & op1(all_25_1_14, all_14_0_6) = all_188_2_179 % 7.31/2.40 | % 7.31/2.40 | Applying alpha-rule on (285) yields: % 7.31/2.40 | (286) h(all_188_2_179) = all_188_1_178 % 7.31/2.40 | (287) h(all_14_0_6) = all_188_0_177 % 7.31/2.40 | (288) op2(all_104_0_74, all_188_0_177) = all_188_1_178 % 7.31/2.40 | (289) op1(all_25_1_14, all_14_0_6) = all_188_2_179 % 7.31/2.40 | % 7.31/2.40 | Instantiating (235) with all_190_0_180, all_190_1_181, all_190_2_182 yields: % 7.31/2.40 | (290) h(all_190_2_182) = all_190_1_181 & h(all_9_0_4) = all_190_0_180 & op2(all_111_0_81, all_190_0_180) = all_190_1_181 & op1(all_29_1_20, all_9_0_4) = all_190_2_182 % 7.31/2.40 | % 7.31/2.40 | Applying alpha-rule on (290) yields: % 7.31/2.40 | (291) h(all_190_2_182) = all_190_1_181 % 7.31/2.40 | (292) h(all_9_0_4) = all_190_0_180 % 7.31/2.40 | (293) op2(all_111_0_81, all_190_0_180) = all_190_1_181 % 7.31/2.41 | (294) op1(all_29_1_20, all_9_0_4) = all_190_2_182 % 7.31/2.41 | % 7.31/2.41 | Instantiating (239) with all_204_0_201, all_204_1_202, all_204_2_203 yields: % 7.31/2.41 | (295) j(all_204_2_203) = all_204_1_202 & j(all_0_0_0) = all_204_0_201 & op2(all_23_2_12, all_0_0_0) = all_204_2_203 & op1(all_116_0_85, all_204_0_201) = all_204_1_202 % 7.31/2.41 | % 7.31/2.41 | Applying alpha-rule on (295) yields: % 7.31/2.41 | (296) j(all_204_2_203) = all_204_1_202 % 7.31/2.41 | (297) j(all_0_0_0) = all_204_0_201 % 7.31/2.41 | (298) op2(all_23_2_12, all_0_0_0) = all_204_2_203 % 7.31/2.41 | (299) op1(all_116_0_85, all_204_0_201) = all_204_1_202 % 7.31/2.41 | % 7.31/2.41 | Instantiating (243) with all_220_0_225, all_220_1_226, all_220_2_227 yields: % 7.31/2.41 | (300) j(all_220_2_227) = all_220_1_226 & j(all_0_0_0) = all_220_0_225 & op2(all_27_2_18, all_0_0_0) = all_220_2_227 & op1(all_121_0_89, all_220_0_225) = all_220_1_226 % 7.31/2.41 | % 7.31/2.41 | Applying alpha-rule on (300) yields: % 7.31/2.41 | (301) j(all_220_2_227) = all_220_1_226 % 7.31/2.41 | (302) j(all_0_0_0) = all_220_0_225 % 7.31/2.41 | (303) op2(all_27_2_18, all_0_0_0) = all_220_2_227 % 7.31/2.41 | (304) op1(all_121_0_89, all_220_0_225) = all_220_1_226 % 7.31/2.41 | % 7.31/2.41 | Instantiating (255) with all_232_0_243, all_232_1_244, all_232_2_245 yields: % 7.31/2.41 | (305) j(all_232_2_245) = all_232_1_244 & j(all_0_0_0) = all_232_0_243 & op2(all_0_0_0, all_0_0_0) = all_232_2_245 & op1(all_140_0_112, all_232_0_243) = all_232_1_244 % 7.31/2.41 | % 7.31/2.41 | Applying alpha-rule on (305) yields: % 7.31/2.41 | (306) j(all_232_2_245) = all_232_1_244 % 7.31/2.41 | (307) j(all_0_0_0) = all_232_0_243 % 7.31/2.41 | (308) op2(all_0_0_0, all_0_0_0) = all_232_2_245 % 7.31/2.41 | (309) op1(all_140_0_112, all_232_0_243) = all_232_1_244 % 7.31/2.41 | % 7.31/2.41 | Instantiating (259) with all_244_0_261, all_244_1_262, all_244_2_263 yields: % 7.31/2.41 | (310) h(all_244_2_263) = all_244_1_262 & h(all_9_0_4) = all_244_0_261 & op2(all_145_0_116, all_244_0_261) = all_244_1_262 & op1(all_27_1_17, all_9_0_4) = all_244_2_263 % 7.31/2.41 | % 7.31/2.41 | Applying alpha-rule on (310) yields: % 7.31/2.41 | (311) h(all_244_2_263) = all_244_1_262 % 7.31/2.41 | (312) h(all_9_0_4) = all_244_0_261 % 7.31/2.41 | (313) op2(all_145_0_116, all_244_0_261) = all_244_1_262 % 7.31/2.41 | (314) op1(all_27_1_17, all_9_0_4) = all_244_2_263 % 7.31/2.41 | % 7.31/2.41 | Instantiating formula (13) with all_0_0_0, all_220_0_225, all_232_0_243 and discharging atoms j(all_0_0_0) = all_232_0_243, j(all_0_0_0) = all_220_0_225, yields: % 7.31/2.41 | (315) all_232_0_243 = all_220_0_225 % 7.31/2.41 | % 7.31/2.41 | Instantiating formula (13) with all_0_0_0, all_204_0_201, all_220_0_225 and discharging atoms j(all_0_0_0) = all_220_0_225, j(all_0_0_0) = all_204_0_201, yields: % 7.31/2.41 | (316) all_220_0_225 = all_204_0_201 % 7.31/2.41 | % 7.31/2.41 | Instantiating formula (13) with all_0_0_0, all_154_0_126, all_204_0_201 and discharging atoms j(all_0_0_0) = all_204_0_201, j(all_0_0_0) = all_154_0_126, yields: % 7.31/2.41 | (317) all_204_0_201 = all_154_0_126 % 7.31/2.41 | % 7.31/2.41 | Instantiating formula (13) with all_0_0_0, all_150_0_120, all_9_0_4 and discharging atoms j(all_0_0_0) = all_150_0_120, j(all_0_0_0) = all_9_0_4, yields: % 7.31/2.41 | (318) all_150_0_120 = all_9_0_4 % 7.31/2.41 | % 7.31/2.41 | Instantiating formula (13) with all_0_0_0, all_148_0_117, all_154_0_126 and discharging atoms j(all_0_0_0) = all_154_0_126, j(all_0_0_0) = all_148_0_117, yields: % 7.31/2.41 | (319) all_154_0_126 = all_148_0_117 % 7.31/2.41 | % 7.31/2.41 | Instantiating formula (13) with all_0_0_0, all_140_0_112, all_232_0_243 and discharging atoms j(all_0_0_0) = all_232_0_243, j(all_0_0_0) = all_140_0_112, yields: % 7.31/2.41 | (320) all_232_0_243 = all_140_0_112 % 7.31/2.41 | % 7.31/2.41 | Instantiating formula (13) with all_0_0_0, all_136_0_106, all_154_0_126 and discharging atoms j(all_0_0_0) = all_154_0_126, j(all_0_0_0) = all_136_0_106, yields: % 7.31/2.41 | (321) all_154_0_126 = all_136_0_106 % 7.31/2.41 | % 7.31/2.41 | Instantiating formula (13) with all_0_0_0, all_136_0_106, all_150_0_120 and discharging atoms j(all_0_0_0) = all_150_0_120, j(all_0_0_0) = all_136_0_106, yields: % 7.31/2.41 | (322) all_150_0_120 = all_136_0_106 % 7.31/2.41 | % 7.31/2.41 | Instantiating formula (13) with all_0_0_0, all_134_0_105, all_148_0_117 and discharging atoms j(all_0_0_0) = all_148_0_117, j(all_0_0_0) = all_134_0_105, yields: % 7.31/2.41 | (323) all_148_0_117 = all_134_0_105 % 7.31/2.41 | % 7.31/2.41 | Instantiating formula (5) with all_9_0_4, all_244_0_261, all_0_3_3 and discharging atoms h(all_9_0_4) = all_244_0_261, h(all_9_0_4) = all_0_3_3, yields: % 7.31/2.41 | (324) all_244_0_261 = all_0_3_3 % 7.31/2.41 | % 7.31/2.41 | Instantiating formula (5) with all_9_0_4, all_190_0_180, all_244_0_261 and discharging atoms h(all_9_0_4) = all_244_0_261, h(all_9_0_4) = all_190_0_180, yields: % 7.31/2.41 | (325) all_244_0_261 = all_190_0_180 % 7.31/2.41 | % 7.31/2.41 | Instantiating formula (5) with all_9_0_4, all_178_0_162, all_190_0_180 and discharging atoms h(all_9_0_4) = all_190_0_180, h(all_9_0_4) = all_178_0_162, yields: % 7.31/2.41 | (326) all_190_0_180 = all_178_0_162 % 7.31/2.41 | % 7.31/2.41 | Instantiating formula (5) with all_9_0_4, all_166_0_144, all_190_0_180 and discharging atoms h(all_9_0_4) = all_190_0_180, h(all_9_0_4) = all_166_0_144, yields: % 7.31/2.41 | (327) all_190_0_180 = all_166_0_144 % 7.31/2.41 | % 7.31/2.41 | Instantiating formula (19) with all_188_2_179, all_25_1_14, all_14_0_6, all_9_0_4 and discharging atoms op1(all_25_1_14, all_14_0_6) = all_188_2_179, op1(all_9_0_4, all_14_0_6) = all_25_1_14, sorti1(all_14_0_6), sorti1(all_9_0_4), yields: % 7.31/2.41 | (328) all_188_2_179 = all_9_0_4 % 7.31/2.41 | % 7.31/2.41 | Instantiating formula (19) with all_166_2_146, all_23_1_11, all_9_0_4, all_9_0_4 and discharging atoms op1(all_23_1_11, all_9_0_4) = all_166_2_146, op1(all_9_0_4, all_9_0_4) = all_23_1_11, sorti1(all_9_0_4), yields: % 7.31/2.41 | (329) all_166_2_146 = all_9_0_4 % 7.31/2.41 | % 7.31/2.41 | Combining equations (325,324) yields a new equation: % 7.31/2.41 | (330) all_190_0_180 = all_0_3_3 % 7.31/2.41 | % 7.31/2.41 | Simplifying 330 yields: % 7.31/2.41 | (331) all_190_0_180 = all_0_3_3 % 7.31/2.41 | % 7.31/2.41 | Combining equations (315,320) yields a new equation: % 7.31/2.41 | (332) all_220_0_225 = all_140_0_112 % 7.31/2.41 | % 7.31/2.41 | Simplifying 332 yields: % 7.31/2.41 | (333) all_220_0_225 = all_140_0_112 % 7.31/2.41 | % 7.31/2.41 | Combining equations (316,333) yields a new equation: % 7.31/2.41 | (334) all_204_0_201 = all_140_0_112 % 7.31/2.41 | % 7.31/2.41 | Simplifying 334 yields: % 7.31/2.41 | (335) all_204_0_201 = all_140_0_112 % 7.31/2.41 | % 7.31/2.41 | Combining equations (317,335) yields a new equation: % 7.31/2.41 | (336) all_154_0_126 = all_140_0_112 % 7.31/2.41 | % 7.31/2.41 | Simplifying 336 yields: % 7.31/2.41 | (337) all_154_0_126 = all_140_0_112 % 7.31/2.41 | % 7.31/2.41 | Combining equations (327,326) yields a new equation: % 7.31/2.41 | (338) all_178_0_162 = all_166_0_144 % 7.31/2.41 | % 7.31/2.41 | Combining equations (331,326) yields a new equation: % 7.31/2.41 | (339) all_178_0_162 = all_0_3_3 % 7.31/2.41 | % 7.31/2.41 | Combining equations (338,339) yields a new equation: % 7.31/2.41 | (340) all_166_0_144 = all_0_3_3 % 7.31/2.41 | % 7.31/2.41 | Simplifying 340 yields: % 7.31/2.41 | (341) all_166_0_144 = all_0_3_3 % 7.31/2.41 | % 7.31/2.41 | Combining equations (321,337) yields a new equation: % 7.31/2.41 | (342) all_140_0_112 = all_136_0_106 % 7.31/2.41 | % 7.31/2.41 | Combining equations (319,337) yields a new equation: % 7.31/2.41 | (343) all_148_0_117 = all_140_0_112 % 7.31/2.41 | % 7.31/2.41 | Simplifying 343 yields: % 7.31/2.41 | (344) all_148_0_117 = all_140_0_112 % 7.31/2.41 | % 7.31/2.41 | Combining equations (322,318) yields a new equation: % 7.31/2.41 | (345) all_136_0_106 = all_9_0_4 % 7.31/2.41 | % 7.31/2.41 | Simplifying 345 yields: % 7.31/2.41 | (346) all_136_0_106 = all_9_0_4 % 7.31/2.41 | % 7.31/2.41 | Combining equations (344,323) yields a new equation: % 7.31/2.41 | (347) all_140_0_112 = all_134_0_105 % 7.31/2.41 | % 7.31/2.41 | Simplifying 347 yields: % 7.31/2.41 | (348) all_140_0_112 = all_134_0_105 % 7.31/2.41 | % 7.31/2.41 | Combining equations (342,348) yields a new equation: % 7.31/2.41 | (349) all_136_0_106 = all_134_0_105 % 7.31/2.41 | % 7.31/2.41 | Simplifying 349 yields: % 7.31/2.41 | (350) all_136_0_106 = all_134_0_105 % 7.31/2.41 | % 7.31/2.41 | Combining equations (350,346) yields a new equation: % 7.31/2.41 | (351) all_134_0_105 = all_9_0_4 % 7.31/2.41 | % 7.31/2.41 | Simplifying 351 yields: % 7.31/2.41 | (352) all_134_0_105 = all_9_0_4 % 7.31/2.41 | % 7.31/2.41 | From (328) and (286) follows: % 7.31/2.41 | (353) h(all_9_0_4) = all_188_1_178 % 7.31/2.41 | % 7.31/2.41 | From (329) and (276) follows: % 7.31/2.41 | (354) h(all_9_0_4) = all_166_1_145 % 7.31/2.41 | % 7.31/2.41 | From (352) and (246) follows: % 7.31/2.41 | (355) h(all_9_0_4) = all_0_0_0 % 7.31/2.41 | % 7.31/2.41 | From (341) and (277) follows: % 7.31/2.41 | (96) h(all_9_0_4) = all_0_3_3 % 7.31/2.41 | % 7.31/2.41 | Instantiating formula (5) with all_9_0_4, all_188_1_178, all_0_3_3 and discharging atoms h(all_9_0_4) = all_188_1_178, h(all_9_0_4) = all_0_3_3, yields: % 7.31/2.41 | (357) all_188_1_178 = all_0_3_3 % 7.31/2.41 | % 7.31/2.41 | Instantiating formula (5) with all_9_0_4, all_166_1_145, all_188_1_178 and discharging atoms h(all_9_0_4) = all_188_1_178, h(all_9_0_4) = all_166_1_145, yields: % 7.31/2.41 | (358) all_188_1_178 = all_166_1_145 % 7.31/2.41 | % 7.31/2.41 | Instantiating formula (5) with all_9_0_4, all_0_0_0, all_166_1_145 and discharging atoms h(all_9_0_4) = all_166_1_145, h(all_9_0_4) = all_0_0_0, yields: % 7.31/2.41 | (359) all_166_1_145 = all_0_0_0 % 7.31/2.42 | % 7.31/2.42 | Combining equations (358,357) yields a new equation: % 7.31/2.42 | (360) all_166_1_145 = all_0_3_3 % 7.31/2.42 | % 7.31/2.42 | Simplifying 360 yields: % 7.31/2.42 | (361) all_166_1_145 = all_0_3_3 % 7.31/2.42 | % 7.31/2.42 | Combining equations (359,361) yields a new equation: % 7.31/2.42 | (362) all_0_0_0 = all_0_3_3 % 7.31/2.42 | % 7.31/2.42 | Simplifying 362 yields: % 7.31/2.42 | (363) all_0_0_0 = all_0_3_3 % 7.31/2.42 | % 7.31/2.42 | Equations (363) can reduce 11 to: % 7.31/2.42 | (364) $false % 7.31/2.42 | % 7.31/2.42 |-The branch is then unsatisfiable % 7.31/2.42 % SZS output end Proof for theBenchmark % 7.31/2.42 % 7.31/2.42 1839ms %------------------------------------------------------------------------------