%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : ALG178+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n025.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Thu Jul 14 15:37:05 EDT 2022 % Result : Theorem 3.01s 1.40s % Output : Proof 7.29s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : ALG178+1 : TPTP v8.1.0. Released v2.7.0. % 0.03/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.33 % Computer : n025.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.34 % DateTime : Wed Jun 8 14:33:34 EDT 2022 % 0.12/0.34 % CPUTime : % 0.52/0.59 ____ _ % 0.52/0.59 ___ / __ \_____(_)___ ________ __________ % 0.52/0.59 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.52/0.59 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.52/0.59 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.52/0.59 % 0.52/0.59 A Theorem Prover for First-Order Logic % 0.52/0.59 (ePrincess v.1.0) % 0.52/0.59 % 0.52/0.59 (c) Philipp Rümmer, 2009-2015 % 0.52/0.59 (c) Peter Backeman, 2014-2015 % 0.52/0.59 (contributions by Angelo Brillout, Peter Baumgartner) % 0.52/0.59 Free software under GNU Lesser General Public License (LGPL). % 0.52/0.59 Bug reports to peter@backeman.se % 0.52/0.59 % 0.52/0.59 For more information, visit http://user.uu.se/~petba168/breu/ % 0.52/0.59 % 0.52/0.59 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.73/0.64 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.43/0.91 Prover 0: Preprocessing ... % 1.86/1.07 Prover 0: Constructing countermodel ... % 3.01/1.40 Prover 0: proved (757ms) % 3.01/1.40 % 3.01/1.40 No countermodel exists, formula is valid % 3.01/1.40 % SZS status Theorem for theBenchmark % 3.01/1.40 % 3.01/1.40 Generating proof ... found it (size 224) % 6.88/2.37 % 6.88/2.37 % SZS output start Proof for theBenchmark % 6.88/2.37 Assumed formulas after preprocessing and simplification: % 6.88/2.37 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ( ~ (v3 = v1) & op2(v0, v2) = v3 & op2(v0, v1) = v2 & sorti2(v1) & sorti2(v0) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v7 = v5 | ~ (op1(v4, v6) = 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))))) % 7.09/2.40 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3 yields: % 7.09/2.40 | (1) ~ (all_0_0_0 = all_0_2_2) & op2(all_0_3_3, all_0_1_1) = 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 = v1 | ~ (op1(v0, v2) = 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)))) % 7.09/2.41 | % 7.09/2.41 | Applying alpha-rule on (1) yields: % 7.09/2.41 | (2) ! [v0] : ( ~ sorti1(v0) | ? [v1] : (j(v1) = v0 & h(v0) = v1)) % 7.09/2.41 | (3) ! [v0] : ( ~ sorti2(v0) | ? [v1] : (j(v0) = v1 & sorti1(v1))) % 7.09/2.41 | (4) op2(all_0_3_3, all_0_1_1) = all_0_0_0 % 7.09/2.41 | (5) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op2(v3, v2) = v1) | ~ (op2(v3, v2) = v0)) % 7.09/2.41 | (6) sorti2(all_0_3_3) % 7.09/2.41 | (7) ! [v0] : ! [v1] : ! [v2] : ( ~ (op2(v0, v1) = v2) | ~ sorti2(v1) | ~ sorti2(v0) | sorti2(v2)) % 7.09/2.41 | (8) ~ (all_0_0_0 = all_0_2_2) % 7.09/2.41 | (9) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h(v2) = v1) | ~ (h(v2) = v0)) % 7.09/2.41 | (10) ! [v0] : ( ~ sorti2(v0) | ? [v1] : (j(v0) = v1 & h(v1) = v0)) % 7.09/2.41 | (11) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v1 | ~ (op1(v0, v2) = v3) | ~ (op1(v0, v1) = v2) | ~ sorti1(v1) | ~ sorti1(v0)) % 7.09/2.41 | (12) op2(all_0_3_3, all_0_2_2) = all_0_1_1 % 7.09/2.41 | (13) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op1(v3, v2) = v1) | ~ (op1(v3, v2) = v0)) % 7.09/2.42 | (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)))) % 7.09/2.42 | (15) ! [v0] : ! [v1] : ! [v2] : ( ~ (op1(v0, v1) = v2) | ~ sorti1(v1) | ~ sorti1(v0) | sorti1(v2)) % 7.09/2.42 | (16) sorti2(all_0_2_2) % 7.09/2.42 | (17) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (j(v2) = v1) | ~ (j(v2) = v0)) % 7.09/2.42 | (18) ! [v0] : ( ~ sorti1(v0) | ? [v1] : (h(v0) = v1 & sorti2(v1))) % 7.09/2.42 | (19) ! [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)))) % 7.09/2.42 | % 7.09/2.42 | Instantiating formula (10) with all_0_2_2 and discharging atoms sorti2(all_0_2_2), yields: % 7.09/2.42 | (20) ? [v0] : (j(all_0_2_2) = v0 & h(v0) = all_0_2_2) % 7.09/2.42 | % 7.09/2.42 | Instantiating formula (3) with all_0_2_2 and discharging atoms sorti2(all_0_2_2), yields: % 7.09/2.42 | (21) ? [v0] : (j(all_0_2_2) = v0 & sorti1(v0)) % 7.09/2.42 | % 7.09/2.42 | Instantiating formula (19) with all_0_2_2 and discharging atoms sorti2(all_0_2_2), yields: % 7.09/2.42 | (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))) % 7.09/2.42 | % 7.09/2.42 | Instantiating formula (7) 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: % 7.09/2.42 | (23) sorti2(all_0_1_1) % 7.09/2.42 | % 7.09/2.42 | Instantiating formula (10) with all_0_3_3 and discharging atoms sorti2(all_0_3_3), yields: % 7.09/2.42 | (24) ? [v0] : (j(all_0_3_3) = v0 & h(v0) = all_0_3_3) % 7.09/2.42 | % 7.09/2.42 | Instantiating formula (3) with all_0_3_3 and discharging atoms sorti2(all_0_3_3), yields: % 7.09/2.42 | (25) ? [v0] : (j(all_0_3_3) = v0 & sorti1(v0)) % 7.09/2.42 | % 7.09/2.42 | Instantiating formula (19) with all_0_3_3 and discharging atoms sorti2(all_0_3_3), yields: % 7.09/2.42 | (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))) % 7.09/2.42 | % 7.09/2.42 | Instantiating (26) with all_9_0_4 yields: % 7.09/2.42 | (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)) % 7.09/2.42 | % 7.09/2.42 | Applying alpha-rule on (27) yields: % 7.09/2.42 | (28) j(all_0_3_3) = all_9_0_4 % 7.09/2.42 | (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)) % 7.09/2.42 | % 7.09/2.42 | Instantiating formula (29) with all_0_2_2 and discharging atoms sorti2(all_0_2_2), yields: % 7.09/2.42 | (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) % 7.09/2.42 | % 7.09/2.42 | Instantiating formula (29) with all_0_3_3 and discharging atoms sorti2(all_0_3_3), yields: % 7.09/2.42 | (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) % 7.09/2.42 | % 7.09/2.42 | Instantiating (25) with all_12_0_5 yields: % 7.09/2.42 | (32) j(all_0_3_3) = all_12_0_5 & sorti1(all_12_0_5) % 7.09/2.43 | % 7.09/2.43 | Applying alpha-rule on (32) yields: % 7.09/2.43 | (33) j(all_0_3_3) = all_12_0_5 % 7.09/2.43 | (34) sorti1(all_12_0_5) % 7.09/2.43 | % 7.09/2.43 | Instantiating (21) with all_14_0_6 yields: % 7.09/2.43 | (35) j(all_0_2_2) = all_14_0_6 & sorti1(all_14_0_6) % 7.09/2.43 | % 7.09/2.43 | Applying alpha-rule on (35) yields: % 7.09/2.43 | (36) j(all_0_2_2) = all_14_0_6 % 7.09/2.43 | (37) sorti1(all_14_0_6) % 7.09/2.43 | % 7.09/2.43 | Instantiating (20) with all_16_0_7 yields: % 7.09/2.43 | (38) j(all_0_2_2) = all_16_0_7 & h(all_16_0_7) = all_0_2_2 % 7.09/2.43 | % 7.09/2.43 | Applying alpha-rule on (38) yields: % 7.09/2.43 | (39) j(all_0_2_2) = all_16_0_7 % 7.09/2.43 | (40) h(all_16_0_7) = all_0_2_2 % 7.09/2.43 | % 7.09/2.43 | Instantiating (24) with all_18_0_8 yields: % 7.09/2.43 | (41) j(all_0_3_3) = all_18_0_8 & h(all_18_0_8) = all_0_3_3 % 7.09/2.43 | % 7.09/2.43 | Applying alpha-rule on (41) yields: % 7.09/2.43 | (42) j(all_0_3_3) = all_18_0_8 % 7.09/2.43 | (43) h(all_18_0_8) = all_0_3_3 % 7.09/2.43 | % 7.09/2.43 | Instantiating (22) with all_20_0_9 yields: % 7.09/2.43 | (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)) % 7.09/2.43 | % 7.09/2.43 | Applying alpha-rule on (44) yields: % 7.09/2.43 | (45) j(all_0_2_2) = all_20_0_9 % 7.09/2.43 | (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)) % 7.09/2.43 | % 7.09/2.43 | Instantiating formula (46) with all_0_2_2 and discharging atoms sorti2(all_0_2_2), yields: % 7.09/2.43 | (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) % 7.09/2.43 | % 7.09/2.43 | Instantiating formula (46) with all_0_3_3 and discharging atoms sorti2(all_0_3_3), yields: % 7.09/2.43 | (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) % 7.09/2.43 | % 7.09/2.43 | Instantiating (31) with all_23_0_10, all_23_1_11, all_23_2_12 yields: % 7.09/2.43 | (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 % 7.09/2.43 | % 7.09/2.43 | Applying alpha-rule on (49) yields: % 7.09/2.43 | (50) j(all_23_2_12) = all_23_1_11 % 7.09/2.43 | (51) j(all_0_3_3) = all_23_0_10 % 7.09/2.43 | (52) op2(all_0_3_3, all_0_3_3) = all_23_2_12 % 7.09/2.43 | (53) op1(all_9_0_4, all_23_0_10) = all_23_1_11 % 7.09/2.43 | % 7.09/2.43 | Instantiating (30) with all_25_0_13, all_25_1_14, all_25_2_15 yields: % 7.09/2.43 | (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 % 7.09/2.43 | % 7.09/2.43 | Applying alpha-rule on (54) yields: % 7.09/2.43 | (55) j(all_25_2_15) = all_25_1_14 % 7.09/2.43 | (56) j(all_0_2_2) = all_25_0_13 % 7.09/2.43 | (57) op2(all_0_3_3, all_0_2_2) = all_25_2_15 % 7.09/2.43 | (58) op1(all_9_0_4, all_25_0_13) = all_25_1_14 % 7.09/2.43 | % 7.09/2.43 | Instantiating (48) with all_27_0_16, all_27_1_17, all_27_2_18 yields: % 7.09/2.43 | (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 % 7.09/2.43 | % 7.09/2.43 | Applying alpha-rule on (59) yields: % 7.09/2.43 | (60) j(all_27_2_18) = all_27_1_17 % 7.09/2.43 | (61) j(all_0_3_3) = all_27_0_16 % 7.09/2.43 | (62) op2(all_0_2_2, all_0_3_3) = all_27_2_18 % 7.09/2.43 | (63) op1(all_20_0_9, all_27_0_16) = all_27_1_17 % 7.09/2.43 | % 7.09/2.43 | Instantiating (47) with all_29_0_19, all_29_1_20, all_29_2_21 yields: % 7.09/2.43 | (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 % 7.09/2.43 | % 7.09/2.43 | Applying alpha-rule on (64) yields: % 7.09/2.43 | (65) j(all_29_2_21) = all_29_1_20 % 7.09/2.43 | (66) j(all_0_2_2) = all_29_0_19 % 7.09/2.43 | (67) op2(all_0_2_2, all_0_2_2) = all_29_2_21 % 7.09/2.43 | (68) op1(all_20_0_9, all_29_0_19) = all_29_1_20 % 7.09/2.43 | % 7.09/2.43 | Instantiating formula (17) 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: % 7.09/2.43 | (69) all_29_0_19 = all_25_0_13 % 7.09/2.43 | % 7.09/2.43 | Instantiating formula (17) 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: % 7.09/2.43 | (70) all_25_0_13 = all_20_0_9 % 7.09/2.43 | % 7.09/2.43 | Instantiating formula (17) 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: % 7.09/2.43 | (71) all_25_0_13 = all_16_0_7 % 7.09/2.43 | % 7.09/2.43 | Instantiating formula (17) 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: % 7.09/2.43 | (72) all_29_0_19 = all_14_0_6 % 7.09/2.43 | % 7.09/2.43 | Instantiating formula (17) 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: % 7.09/2.43 | (73) all_27_0_16 = all_23_0_10 % 7.09/2.43 | % 7.09/2.43 | Instantiating formula (17) 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: % 7.09/2.43 | (74) all_27_0_16 = all_18_0_8 % 7.09/2.43 | % 7.09/2.43 | Instantiating formula (17) 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: % 7.09/2.43 | (75) all_27_0_16 = all_12_0_5 % 7.09/2.43 | % 7.09/2.43 | Instantiating formula (17) 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: % 7.09/2.43 | (76) all_27_0_16 = all_9_0_4 % 7.09/2.43 | % 7.09/2.43 | Instantiating formula (5) 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: % 7.09/2.44 | (77) all_25_2_15 = all_0_1_1 % 7.09/2.44 | % 7.09/2.44 | Combining equations (69,72) yields a new equation: % 7.09/2.44 | (78) all_25_0_13 = all_14_0_6 % 7.09/2.44 | % 7.09/2.44 | Simplifying 78 yields: % 7.09/2.44 | (79) all_25_0_13 = all_14_0_6 % 7.09/2.44 | % 7.09/2.44 | Combining equations (74,73) yields a new equation: % 7.09/2.44 | (80) all_23_0_10 = all_18_0_8 % 7.09/2.44 | % 7.09/2.44 | Combining equations (75,73) yields a new equation: % 7.09/2.44 | (81) all_23_0_10 = all_12_0_5 % 7.09/2.44 | % 7.09/2.44 | Combining equations (76,73) yields a new equation: % 7.09/2.44 | (82) all_23_0_10 = all_9_0_4 % 7.09/2.44 | % 7.09/2.44 | Combining equations (79,70) yields a new equation: % 7.09/2.44 | (83) all_20_0_9 = all_14_0_6 % 7.09/2.44 | % 7.09/2.44 | Combining equations (71,70) yields a new equation: % 7.09/2.44 | (84) all_20_0_9 = all_16_0_7 % 7.09/2.44 | % 7.09/2.44 | Combining equations (81,80) yields a new equation: % 7.09/2.44 | (85) all_18_0_8 = all_12_0_5 % 7.09/2.44 | % 7.09/2.44 | Combining equations (82,80) yields a new equation: % 7.09/2.44 | (86) all_18_0_8 = all_9_0_4 % 7.09/2.44 | % 7.09/2.44 | Combining equations (84,83) yields a new equation: % 7.09/2.44 | (87) all_16_0_7 = all_14_0_6 % 7.09/2.44 | % 7.09/2.44 | Simplifying 87 yields: % 7.09/2.44 | (88) all_16_0_7 = all_14_0_6 % 7.09/2.44 | % 7.09/2.44 | Combining equations (85,86) yields a new equation: % 7.09/2.44 | (89) all_12_0_5 = all_9_0_4 % 7.09/2.44 | % 7.09/2.44 | Simplifying 89 yields: % 7.09/2.44 | (90) all_12_0_5 = all_9_0_4 % 7.09/2.44 | % 7.09/2.44 | Combining equations (86,80) yields a new equation: % 7.09/2.44 | (82) all_23_0_10 = all_9_0_4 % 7.09/2.44 | % 7.09/2.44 | Combining equations (83,70) yields a new equation: % 7.09/2.44 | (79) all_25_0_13 = all_14_0_6 % 7.09/2.44 | % 7.09/2.44 | Combining equations (82,73) yields a new equation: % 7.09/2.44 | (76) all_27_0_16 = all_9_0_4 % 7.09/2.44 | % 7.09/2.44 | From (77) and (55) follows: % 7.09/2.44 | (94) j(all_0_1_1) = all_25_1_14 % 7.09/2.44 | % 7.09/2.44 | From (86) and (43) follows: % 7.09/2.44 | (95) h(all_9_0_4) = all_0_3_3 % 7.09/2.44 | % 7.09/2.44 | From (88) and (40) follows: % 7.09/2.44 | (96) h(all_14_0_6) = all_0_2_2 % 7.09/2.44 | % 7.09/2.44 | From (77) and (57) follows: % 7.09/2.44 | (12) op2(all_0_3_3, all_0_2_2) = all_0_1_1 % 7.09/2.44 | % 7.09/2.44 | From (83)(72) and (68) follows: % 7.09/2.44 | (98) op1(all_14_0_6, all_14_0_6) = all_29_1_20 % 7.09/2.44 | % 7.09/2.44 | From (83)(76) and (63) follows: % 7.29/2.44 | (99) op1(all_14_0_6, all_9_0_4) = all_27_1_17 % 7.29/2.44 | % 7.29/2.44 | From (79) and (58) follows: % 7.29/2.44 | (100) op1(all_9_0_4, all_14_0_6) = all_25_1_14 % 7.29/2.44 | % 7.29/2.44 | From (82) and (53) follows: % 7.29/2.44 | (101) op1(all_9_0_4, all_9_0_4) = all_23_1_11 % 7.29/2.44 | % 7.29/2.44 | From (90) and (34) follows: % 7.29/2.44 | (102) sorti1(all_9_0_4) % 7.29/2.44 | % 7.29/2.44 | Instantiating formula (46) with all_0_1_1 and discharging atoms sorti2(all_0_1_1), yields: % 7.29/2.44 | (103) ? [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) % 7.29/2.44 | % 7.29/2.44 | Instantiating formula (29) with all_0_1_1 and discharging atoms sorti2(all_0_1_1), yields: % 7.29/2.44 | (104) ? [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) % 7.29/2.44 | % 7.29/2.44 | Instantiating formula (10) with all_0_1_1 and discharging atoms sorti2(all_0_1_1), yields: % 7.29/2.44 | (105) ? [v0] : (j(all_0_1_1) = v0 & h(v0) = all_0_1_1) % 7.29/2.44 | % 7.29/2.44 | Instantiating formula (3) with all_0_1_1 and discharging atoms sorti2(all_0_1_1), yields: % 7.29/2.44 | (106) ? [v0] : (j(all_0_1_1) = v0 & sorti1(v0)) % 7.29/2.44 | % 7.29/2.44 | Instantiating formula (19) with all_0_1_1 and discharging atoms sorti2(all_0_1_1), yields: % 7.29/2.44 | (107) ? [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))) % 7.29/2.44 | % 7.29/2.44 | Instantiating formula (15) 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: % 7.29/2.44 | (108) sorti1(all_29_1_20) % 7.29/2.44 | % 7.29/2.44 | Instantiating formula (14) with all_14_0_6 and discharging atoms sorti1(all_14_0_6), yields: % 7.29/2.44 | (109) ? [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))) % 7.29/2.44 | % 7.29/2.44 | Instantiating formula (15) 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: % 7.29/2.44 | (110) sorti1(all_27_1_17) % 7.29/2.44 | % 7.29/2.44 | Instantiating formula (15) 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: % 7.29/2.44 | (111) sorti1(all_23_1_11) % 7.29/2.44 | % 7.29/2.44 | Instantiating formula (14) with all_9_0_4 and discharging atoms sorti1(all_9_0_4), yields: % 7.29/2.44 | (112) ? [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))) % 7.29/2.44 | % 7.29/2.44 | Instantiating (112) with all_41_0_22 yields: % 7.29/2.44 | (113) 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)) % 7.29/2.45 | % 7.29/2.45 | Applying alpha-rule on (113) yields: % 7.29/2.45 | (114) h(all_9_0_4) = all_41_0_22 % 7.29/2.45 | (115) ! [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)) % 7.29/2.45 | % 7.29/2.45 | Instantiating formula (115) with all_14_0_6 and discharging atoms sorti1(all_14_0_6), yields: % 7.29/2.45 | (116) ? [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) % 7.29/2.45 | % 7.29/2.45 | Instantiating formula (115) with all_9_0_4 and discharging atoms sorti1(all_9_0_4), yields: % 7.29/2.45 | (117) ? [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) % 7.29/2.45 | % 7.29/2.45 | Instantiating (107) with all_44_0_23 yields: % 7.29/2.45 | (118) 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)) % 7.29/2.45 | % 7.29/2.45 | Applying alpha-rule on (118) yields: % 7.29/2.45 | (119) j(all_0_1_1) = all_44_0_23 % 7.29/2.45 | (120) ! [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)) % 7.29/2.45 | % 7.29/2.45 | Instantiating formula (120) with all_0_1_1 and discharging atoms sorti2(all_0_1_1), yields: % 7.29/2.45 | (121) ? [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) % 7.29/2.45 | % 7.29/2.45 | Instantiating (109) with all_47_0_24 yields: % 7.29/2.45 | (122) 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)) % 7.29/2.45 | % 7.29/2.45 | Applying alpha-rule on (122) yields: % 7.29/2.45 | (123) h(all_14_0_6) = all_47_0_24 % 7.29/2.45 | (124) ! [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)) % 7.29/2.45 | % 7.29/2.45 | Instantiating formula (124) with all_14_0_6 and discharging atoms sorti1(all_14_0_6), yields: % 7.29/2.45 | (125) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_14_0_6) = v2 & op2(all_47_0_24, v2) = v1 & op1(all_14_0_6, all_14_0_6) = v0) % 7.29/2.45 | % 7.29/2.45 | Instantiating formula (124) with all_9_0_4 and discharging atoms sorti1(all_9_0_4), yields: % 7.29/2.45 | (126) ? [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) % 7.29/2.45 | % 7.29/2.45 | Instantiating (106) with all_50_0_25 yields: % 7.29/2.45 | (127) j(all_0_1_1) = all_50_0_25 & sorti1(all_50_0_25) % 7.29/2.45 | % 7.29/2.45 | Applying alpha-rule on (127) yields: % 7.29/2.45 | (128) j(all_0_1_1) = all_50_0_25 % 7.29/2.45 | (129) sorti1(all_50_0_25) % 7.29/2.45 | % 7.29/2.45 | Instantiating (105) with all_52_0_26 yields: % 7.29/2.45 | (130) j(all_0_1_1) = all_52_0_26 & h(all_52_0_26) = all_0_1_1 % 7.29/2.45 | % 7.29/2.45 | Applying alpha-rule on (130) yields: % 7.29/2.45 | (131) j(all_0_1_1) = all_52_0_26 % 7.29/2.45 | (132) h(all_52_0_26) = all_0_1_1 % 7.29/2.45 | % 7.29/2.45 | Instantiating (104) with all_54_0_27, all_54_1_28, all_54_2_29 yields: % 7.29/2.45 | (133) 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 % 7.29/2.45 | % 7.29/2.45 | Applying alpha-rule on (133) yields: % 7.29/2.45 | (134) j(all_54_2_29) = all_54_1_28 % 7.29/2.45 | (135) j(all_0_1_1) = all_54_0_27 % 7.29/2.45 | (136) op2(all_0_3_3, all_0_1_1) = all_54_2_29 % 7.29/2.45 | (137) op1(all_9_0_4, all_54_0_27) = all_54_1_28 % 7.29/2.45 | % 7.29/2.45 | Instantiating (103) with all_56_0_30, all_56_1_31, all_56_2_32 yields: % 7.29/2.45 | (138) 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 % 7.29/2.45 | % 7.29/2.45 | Applying alpha-rule on (138) yields: % 7.29/2.45 | (139) j(all_56_2_32) = all_56_1_31 % 7.29/2.45 | (140) j(all_0_1_1) = all_56_0_30 % 7.29/2.45 | (141) op2(all_0_2_2, all_0_1_1) = all_56_2_32 % 7.29/2.45 | (142) op1(all_20_0_9, all_56_0_30) = all_56_1_31 % 7.29/2.45 | % 7.29/2.45 | Instantiating (117) with all_58_0_33, all_58_1_34, all_58_2_35 yields: % 7.29/2.45 | (143) 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 % 7.29/2.45 | % 7.29/2.45 | Applying alpha-rule on (143) yields: % 7.29/2.45 | (144) h(all_58_2_35) = all_58_1_34 % 7.29/2.45 | (145) h(all_9_0_4) = all_58_0_33 % 7.29/2.45 | (146) op2(all_41_0_22, all_58_0_33) = all_58_1_34 % 7.29/2.46 | (147) op1(all_9_0_4, all_9_0_4) = all_58_2_35 % 7.29/2.46 | % 7.29/2.46 | Instantiating (116) with all_60_0_36, all_60_1_37, all_60_2_38 yields: % 7.29/2.46 | (148) 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 % 7.29/2.46 | % 7.29/2.46 | Applying alpha-rule on (148) yields: % 7.29/2.46 | (149) h(all_60_2_38) = all_60_1_37 % 7.29/2.46 | (150) h(all_14_0_6) = all_60_0_36 % 7.29/2.46 | (151) op2(all_41_0_22, all_60_0_36) = all_60_1_37 % 7.29/2.46 | (152) op1(all_9_0_4, all_14_0_6) = all_60_2_38 % 7.29/2.46 | % 7.29/2.46 | Instantiating (121) with all_66_0_45, all_66_1_46, all_66_2_47 yields: % 7.29/2.46 | (153) 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 % 7.29/2.46 | % 7.29/2.46 | Applying alpha-rule on (153) yields: % 7.29/2.46 | (154) j(all_66_2_47) = all_66_1_46 % 7.29/2.46 | (155) j(all_0_1_1) = all_66_0_45 % 7.29/2.46 | (156) op2(all_0_1_1, all_0_1_1) = all_66_2_47 % 7.29/2.46 | (157) op1(all_44_0_23, all_66_0_45) = all_66_1_46 % 7.29/2.46 | % 7.29/2.46 | Instantiating (126) with all_68_0_48, all_68_1_49, all_68_2_50 yields: % 7.29/2.46 | (158) 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 % 7.29/2.46 | % 7.29/2.46 | Applying alpha-rule on (158) yields: % 7.29/2.46 | (159) h(all_68_2_50) = all_68_1_49 % 7.29/2.46 | (160) h(all_9_0_4) = all_68_0_48 % 7.29/2.46 | (161) op2(all_47_0_24, all_68_0_48) = all_68_1_49 % 7.29/2.46 | (162) op1(all_14_0_6, all_9_0_4) = all_68_2_50 % 7.29/2.46 | % 7.29/2.46 | Instantiating (125) with all_70_0_51, all_70_1_52, all_70_2_53 yields: % 7.29/2.46 | (163) h(all_70_2_53) = all_70_1_52 & h(all_14_0_6) = all_70_0_51 & op2(all_47_0_24, all_70_0_51) = all_70_1_52 & op1(all_14_0_6, all_14_0_6) = all_70_2_53 % 7.29/2.46 | % 7.29/2.46 | Applying alpha-rule on (163) yields: % 7.29/2.46 | (164) h(all_70_2_53) = all_70_1_52 % 7.29/2.46 | (165) h(all_14_0_6) = all_70_0_51 % 7.29/2.46 | (166) op2(all_47_0_24, all_70_0_51) = all_70_1_52 % 7.29/2.46 | (167) op1(all_14_0_6, all_14_0_6) = all_70_2_53 % 7.29/2.46 | % 7.29/2.46 | Instantiating formula (17) 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: % 7.29/2.46 | (168) all_66_0_45 = all_56_0_30 % 7.29/2.46 | % 7.29/2.46 | Instantiating formula (17) 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: % 7.29/2.46 | (169) all_66_0_45 = all_54_0_27 % 7.29/2.46 | % 7.29/2.46 | Instantiating formula (17) 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: % 7.29/2.46 | (170) all_52_0_26 = all_25_1_14 % 7.29/2.46 | % 7.29/2.46 | Instantiating formula (17) with all_0_1_1, all_52_0_26, all_56_0_30 and discharging atoms j(all_0_1_1) = all_56_0_30, j(all_0_1_1) = all_52_0_26, yields: % 7.29/2.46 | (171) all_56_0_30 = all_52_0_26 % 7.29/2.46 | % 7.29/2.46 | Instantiating formula (17) 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: % 7.29/2.46 | (172) all_56_0_30 = all_50_0_25 % 7.29/2.46 | % 7.29/2.46 | Instantiating formula (17) with all_0_1_1, all_44_0_23, all_66_0_45 and discharging atoms j(all_0_1_1) = all_66_0_45, j(all_0_1_1) = all_44_0_23, yields: % 7.29/2.46 | (173) all_66_0_45 = all_44_0_23 % 7.29/2.46 | % 7.29/2.46 | Instantiating formula (9) with all_14_0_6, all_70_0_51, all_0_2_2 and discharging atoms h(all_14_0_6) = all_70_0_51, h(all_14_0_6) = all_0_2_2, yields: % 7.29/2.46 | (174) all_70_0_51 = all_0_2_2 % 7.29/2.46 | % 7.29/2.46 | Instantiating formula (9) with all_14_0_6, all_60_0_36, all_70_0_51 and discharging atoms h(all_14_0_6) = all_70_0_51, h(all_14_0_6) = all_60_0_36, yields: % 7.29/2.46 | (175) all_70_0_51 = all_60_0_36 % 7.29/2.46 | % 7.29/2.46 | Instantiating formula (9) with all_14_0_6, all_47_0_24, all_60_0_36 and discharging atoms h(all_14_0_6) = all_60_0_36, h(all_14_0_6) = all_47_0_24, yields: % 7.29/2.46 | (176) all_60_0_36 = all_47_0_24 % 7.29/2.46 | % 7.29/2.46 | Instantiating formula (9) 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: % 7.29/2.46 | (177) all_68_0_48 = all_0_3_3 % 7.29/2.46 | % 7.29/2.46 | Instantiating formula (9) 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: % 7.29/2.46 | (178) all_68_0_48 = all_58_0_33 % 7.29/2.46 | % 7.29/2.46 | Instantiating formula (9) 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: % 7.29/2.46 | (179) all_58_0_33 = all_41_0_22 % 7.29/2.46 | % 7.29/2.46 | Instantiating formula (5) with all_0_3_3, all_0_1_1, all_54_2_29, all_0_0_0 and discharging atoms op2(all_0_3_3, all_0_1_1) = all_54_2_29, op2(all_0_3_3, all_0_1_1) = all_0_0_0, yields: % 7.29/2.46 | (180) all_54_2_29 = all_0_0_0 % 7.29/2.46 | % 7.29/2.46 | Instantiating formula (13) with all_14_0_6, all_14_0_6, all_70_2_53, all_29_1_20 and discharging atoms op1(all_14_0_6, all_14_0_6) = all_70_2_53, op1(all_14_0_6, all_14_0_6) = all_29_1_20, yields: % 7.29/2.46 | (181) all_70_2_53 = all_29_1_20 % 7.29/2.46 | % 7.29/2.46 | Instantiating formula (13) 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: % 7.29/2.46 | (182) all_60_2_38 = all_25_1_14 % 7.29/2.46 | % 7.29/2.46 | Combining equations (175,174) yields a new equation: % 7.29/2.46 | (183) all_60_0_36 = all_0_2_2 % 7.29/2.46 | % 7.29/2.46 | Simplifying 183 yields: % 7.29/2.46 | (184) all_60_0_36 = all_0_2_2 % 7.29/2.46 | % 7.29/2.46 | Combining equations (178,177) yields a new equation: % 7.29/2.46 | (185) all_58_0_33 = all_0_3_3 % 7.29/2.46 | % 7.29/2.46 | Simplifying 185 yields: % 7.29/2.46 | (186) all_58_0_33 = all_0_3_3 % 7.29/2.46 | % 7.29/2.46 | Combining equations (173,169) yields a new equation: % 7.29/2.46 | (187) all_54_0_27 = all_44_0_23 % 7.29/2.46 | % 7.29/2.46 | Combining equations (168,169) yields a new equation: % 7.29/2.46 | (188) all_56_0_30 = all_54_0_27 % 7.29/2.47 | % 7.29/2.47 | Simplifying 188 yields: % 7.29/2.47 | (189) all_56_0_30 = all_54_0_27 % 7.29/2.47 | % 7.29/2.47 | Combining equations (176,184) yields a new equation: % 7.29/2.47 | (190) all_47_0_24 = all_0_2_2 % 7.29/2.47 | % 7.29/2.47 | Simplifying 190 yields: % 7.29/2.47 | (191) all_47_0_24 = all_0_2_2 % 7.29/2.47 | % 7.29/2.47 | Combining equations (179,186) yields a new equation: % 7.29/2.47 | (192) all_41_0_22 = all_0_3_3 % 7.29/2.47 | % 7.29/2.47 | Simplifying 192 yields: % 7.29/2.47 | (193) all_41_0_22 = all_0_3_3 % 7.29/2.47 | % 7.29/2.47 | Combining equations (171,172) yields a new equation: % 7.29/2.47 | (194) all_52_0_26 = all_50_0_25 % 7.29/2.47 | % 7.29/2.47 | Simplifying 194 yields: % 7.29/2.47 | (195) all_52_0_26 = all_50_0_25 % 7.29/2.47 | % 7.29/2.47 | Combining equations (189,172) yields a new equation: % 7.29/2.47 | (196) all_54_0_27 = all_50_0_25 % 7.29/2.47 | % 7.29/2.47 | Simplifying 196 yields: % 7.29/2.47 | (197) all_54_0_27 = all_50_0_25 % 7.29/2.47 | % 7.29/2.47 | Combining equations (197,187) yields a new equation: % 7.29/2.47 | (198) all_50_0_25 = all_44_0_23 % 7.29/2.47 | % 7.29/2.47 | Simplifying 198 yields: % 7.29/2.47 | (199) all_50_0_25 = all_44_0_23 % 7.29/2.47 | % 7.29/2.47 | Combining equations (195,170) yields a new equation: % 7.29/2.47 | (200) all_50_0_25 = all_25_1_14 % 7.29/2.47 | % 7.29/2.47 | Simplifying 200 yields: % 7.29/2.47 | (201) all_50_0_25 = all_25_1_14 % 7.29/2.47 | % 7.29/2.47 | Combining equations (201,199) yields a new equation: % 7.29/2.47 | (202) all_44_0_23 = all_25_1_14 % 7.29/2.47 | % 7.29/2.47 | Combining equations (202,199) yields a new equation: % 7.29/2.47 | (201) all_50_0_25 = all_25_1_14 % 7.29/2.47 | % 7.29/2.47 | From (182) and (149) follows: % 7.29/2.47 | (204) h(all_25_1_14) = all_60_1_37 % 7.29/2.47 | % 7.29/2.47 | From (191) and (123) follows: % 7.29/2.47 | (96) h(all_14_0_6) = all_0_2_2 % 7.29/2.47 | % 7.29/2.47 | From (193)(184) and (151) follows: % 7.29/2.47 | (206) op2(all_0_3_3, all_0_2_2) = all_60_1_37 % 7.29/2.47 | % 7.29/2.47 | From (180) and (136) follows: % 7.29/2.47 | (4) op2(all_0_3_3, all_0_1_1) = all_0_0_0 % 7.29/2.47 | % 7.29/2.47 | From (181) and (167) follows: % 7.29/2.47 | (98) op1(all_14_0_6, all_14_0_6) = all_29_1_20 % 7.29/2.47 | % 7.29/2.47 | From (182) and (152) follows: % 7.29/2.47 | (100) op1(all_9_0_4, all_14_0_6) = all_25_1_14 % 7.29/2.47 | % 7.29/2.47 | From (201) and (129) follows: % 7.29/2.47 | (210) sorti1(all_25_1_14) % 7.29/2.47 | % 7.29/2.47 | Instantiating formula (5) with all_0_3_3, all_0_2_2, all_60_1_37, all_0_1_1 and discharging atoms op2(all_0_3_3, all_0_2_2) = all_60_1_37, op2(all_0_3_3, all_0_2_2) = all_0_1_1, yields: % 7.29/2.47 | (211) all_60_1_37 = all_0_1_1 % 7.29/2.47 | % 7.29/2.47 | From (211) and (204) follows: % 7.29/2.47 | (212) h(all_25_1_14) = all_0_1_1 % 7.29/2.47 | % 7.29/2.47 | Instantiating formula (124) with all_29_1_20 and discharging atoms sorti1(all_29_1_20), yields: % 7.29/2.47 | (213) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_29_1_20) = v2 & op2(all_47_0_24, v2) = v1 & op1(all_14_0_6, all_29_1_20) = v0) % 7.29/2.47 | % 7.29/2.47 | Instantiating formula (14) with all_29_1_20 and discharging atoms sorti1(all_29_1_20), yields: % 7.29/2.47 | (214) ? [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.29/2.47 | % 7.29/2.47 | Instantiating formula (14) with all_27_1_17 and discharging atoms sorti1(all_27_1_17), yields: % 7.29/2.47 | (215) ? [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.29/2.47 | % 7.29/2.47 | Instantiating formula (124) with all_25_1_14 and discharging atoms sorti1(all_25_1_14), yields: % 7.29/2.47 | (216) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_25_1_14) = v2 & op2(all_47_0_24, v2) = v1 & op1(all_14_0_6, all_25_1_14) = v0) % 7.29/2.47 | % 7.29/2.47 | Instantiating formula (115) with all_25_1_14 and discharging atoms sorti1(all_25_1_14), yields: % 7.29/2.47 | (217) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_25_1_14) = v2 & op2(all_41_0_22, v2) = v1 & op1(all_9_0_4, all_25_1_14) = v0) % 7.29/2.47 | % 7.29/2.47 | Instantiating formula (14) with all_25_1_14 and discharging atoms sorti1(all_25_1_14), yields: % 7.29/2.47 | (218) ? [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.29/2.47 | % 7.29/2.47 | Instantiating formula (14) with all_23_1_11 and discharging atoms sorti1(all_23_1_11), yields: % 7.29/2.47 | (219) ? [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.29/2.47 | % 7.29/2.47 | Instantiating (219) with all_99_0_70 yields: % 7.29/2.47 | (220) 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.29/2.47 | % 7.29/2.47 | Applying alpha-rule on (220) yields: % 7.29/2.47 | (221) h(all_23_1_11) = all_99_0_70 % 7.29/2.47 | (222) ! [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.29/2.47 | % 7.29/2.47 | Instantiating formula (222) with all_14_0_6 and discharging atoms sorti1(all_14_0_6), yields: % 7.29/2.47 | (223) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_14_0_6) = v2 & op2(all_99_0_70, v2) = v1 & op1(all_23_1_11, all_14_0_6) = v0) % 7.29/2.47 | % 7.29/2.47 | Instantiating (218) with all_104_0_74 yields: % 7.29/2.48 | (224) 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.29/2.48 | % 7.29/2.48 | Applying alpha-rule on (224) yields: % 7.29/2.48 | (225) h(all_25_1_14) = all_104_0_74 % 7.29/2.48 | (226) ! [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.29/2.48 | % 7.29/2.48 | Instantiating formula (226) with all_14_0_6 and discharging atoms sorti1(all_14_0_6), yields: % 7.29/2.48 | (227) ? [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.29/2.48 | % 7.29/2.48 | Instantiating (217) with all_107_0_75, all_107_1_76, all_107_2_77 yields: % 7.29/2.48 | (228) h(all_107_2_77) = all_107_1_76 & h(all_25_1_14) = all_107_0_75 & op2(all_41_0_22, all_107_0_75) = all_107_1_76 & op1(all_9_0_4, all_25_1_14) = all_107_2_77 % 7.29/2.48 | % 7.29/2.48 | Applying alpha-rule on (228) yields: % 7.29/2.48 | (229) h(all_107_2_77) = all_107_1_76 % 7.29/2.48 | (230) h(all_25_1_14) = all_107_0_75 % 7.29/2.48 | (231) op2(all_41_0_22, all_107_0_75) = all_107_1_76 % 7.29/2.48 | (232) op1(all_9_0_4, all_25_1_14) = all_107_2_77 % 7.29/2.48 | % 7.29/2.48 | Instantiating (214) with all_111_0_81 yields: % 7.29/2.48 | (233) 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.29/2.48 | % 7.29/2.48 | Applying alpha-rule on (233) yields: % 7.29/2.48 | (234) h(all_29_1_20) = all_111_0_81 % 7.29/2.48 | (235) ! [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.29/2.48 | % 7.29/2.48 | Instantiating formula (235) with all_25_1_14 and discharging atoms sorti1(all_25_1_14), yields: % 7.29/2.48 | (236) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_25_1_14) = v2 & op2(all_111_0_81, v2) = v1 & op1(all_29_1_20, all_25_1_14) = v0) % 7.29/2.48 | % 7.29/2.48 | Instantiating formula (235) with all_14_0_6 and discharging atoms sorti1(all_14_0_6), yields: % 7.29/2.48 | (237) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_14_0_6) = v2 & op2(all_111_0_81, v2) = v1 & op1(all_29_1_20, all_14_0_6) = v0) % 7.29/2.48 | % 7.29/2.48 | Instantiating (213) with all_138_0_109, all_138_1_110, all_138_2_111 yields: % 7.29/2.48 | (238) h(all_138_2_111) = all_138_1_110 & h(all_29_1_20) = all_138_0_109 & op2(all_47_0_24, all_138_0_109) = all_138_1_110 & op1(all_14_0_6, all_29_1_20) = all_138_2_111 % 7.29/2.48 | % 7.29/2.48 | Applying alpha-rule on (238) yields: % 7.29/2.48 | (239) h(all_138_2_111) = all_138_1_110 % 7.29/2.48 | (240) h(all_29_1_20) = all_138_0_109 % 7.29/2.48 | (241) op2(all_47_0_24, all_138_0_109) = all_138_1_110 % 7.29/2.48 | (242) op1(all_14_0_6, all_29_1_20) = all_138_2_111 % 7.29/2.48 | % 7.29/2.48 | Instantiating (216) with all_143_0_113, all_143_1_114, all_143_2_115 yields: % 7.29/2.48 | (243) h(all_143_2_115) = all_143_1_114 & h(all_25_1_14) = all_143_0_113 & op2(all_47_0_24, all_143_0_113) = all_143_1_114 & op1(all_14_0_6, all_25_1_14) = all_143_2_115 % 7.29/2.48 | % 7.29/2.48 | Applying alpha-rule on (243) yields: % 7.29/2.48 | (244) h(all_143_2_115) = all_143_1_114 % 7.29/2.48 | (245) h(all_25_1_14) = all_143_0_113 % 7.29/2.48 | (246) op2(all_47_0_24, all_143_0_113) = all_143_1_114 % 7.29/2.48 | (247) op1(all_14_0_6, all_25_1_14) = all_143_2_115 % 7.29/2.48 | % 7.29/2.48 | Instantiating (215) with all_145_0_116 yields: % 7.29/2.48 | (248) 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.29/2.48 | % 7.29/2.48 | Applying alpha-rule on (248) yields: % 7.29/2.48 | (249) h(all_27_1_17) = all_145_0_116 % 7.29/2.48 | (250) ! [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.29/2.48 | % 7.29/2.48 | Instantiating formula (250) with all_25_1_14 and discharging atoms sorti1(all_25_1_14), yields: % 7.29/2.48 | (251) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_25_1_14) = v2 & op2(all_145_0_116, v2) = v1 & op1(all_27_1_17, all_25_1_14) = v0) % 7.29/2.48 | % 7.29/2.48 | Instantiating formula (250) with all_14_0_6 and discharging atoms sorti1(all_14_0_6), yields: % 7.29/2.48 | (252) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_14_0_6) = v2 & op2(all_145_0_116, v2) = v1 & op1(all_27_1_17, all_14_0_6) = v0) % 7.29/2.48 | % 7.29/2.48 | Instantiating (223) with all_168_0_147, all_168_1_148, all_168_2_149 yields: % 7.29/2.48 | (253) h(all_168_2_149) = all_168_1_148 & h(all_14_0_6) = all_168_0_147 & op2(all_99_0_70, all_168_0_147) = all_168_1_148 & op1(all_23_1_11, all_14_0_6) = all_168_2_149 % 7.29/2.48 | % 7.29/2.48 | Applying alpha-rule on (253) yields: % 7.29/2.48 | (254) h(all_168_2_149) = all_168_1_148 % 7.29/2.48 | (255) h(all_14_0_6) = all_168_0_147 % 7.29/2.48 | (256) op2(all_99_0_70, all_168_0_147) = all_168_1_148 % 7.29/2.48 | (257) op1(all_23_1_11, all_14_0_6) = all_168_2_149 % 7.29/2.48 | % 7.29/2.48 | Instantiating (227) with all_188_0_177, all_188_1_178, all_188_2_179 yields: % 7.29/2.48 | (258) 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.29/2.48 | % 7.29/2.48 | Applying alpha-rule on (258) yields: % 7.29/2.48 | (259) h(all_188_2_179) = all_188_1_178 % 7.29/2.48 | (260) h(all_14_0_6) = all_188_0_177 % 7.29/2.48 | (261) op2(all_104_0_74, all_188_0_177) = all_188_1_178 % 7.29/2.48 | (262) op1(all_25_1_14, all_14_0_6) = all_188_2_179 % 7.29/2.48 | % 7.29/2.48 | Instantiating (237) with all_192_0_183, all_192_1_184, all_192_2_185 yields: % 7.29/2.48 | (263) h(all_192_2_185) = all_192_1_184 & h(all_14_0_6) = all_192_0_183 & op2(all_111_0_81, all_192_0_183) = all_192_1_184 & op1(all_29_1_20, all_14_0_6) = all_192_2_185 % 7.29/2.48 | % 7.29/2.48 | Applying alpha-rule on (263) yields: % 7.29/2.48 | (264) h(all_192_2_185) = all_192_1_184 % 7.29/2.48 | (265) h(all_14_0_6) = all_192_0_183 % 7.29/2.48 | (266) op2(all_111_0_81, all_192_0_183) = all_192_1_184 % 7.29/2.48 | (267) op1(all_29_1_20, all_14_0_6) = all_192_2_185 % 7.29/2.48 | % 7.29/2.48 | Instantiating (236) with all_196_0_189, all_196_1_190, all_196_2_191 yields: % 7.29/2.48 | (268) h(all_196_2_191) = all_196_1_190 & h(all_25_1_14) = all_196_0_189 & op2(all_111_0_81, all_196_0_189) = all_196_1_190 & op1(all_29_1_20, all_25_1_14) = all_196_2_191 % 7.29/2.48 | % 7.29/2.48 | Applying alpha-rule on (268) yields: % 7.29/2.48 | (269) h(all_196_2_191) = all_196_1_190 % 7.29/2.48 | (270) h(all_25_1_14) = all_196_0_189 % 7.29/2.48 | (271) op2(all_111_0_81, all_196_0_189) = all_196_1_190 % 7.29/2.48 | (272) op1(all_29_1_20, all_25_1_14) = all_196_2_191 % 7.29/2.48 | % 7.29/2.48 | Instantiating (251) with all_248_0_267, all_248_1_268, all_248_2_269 yields: % 7.29/2.48 | (273) h(all_248_2_269) = all_248_1_268 & h(all_25_1_14) = all_248_0_267 & op2(all_145_0_116, all_248_0_267) = all_248_1_268 & op1(all_27_1_17, all_25_1_14) = all_248_2_269 % 7.29/2.48 | % 7.29/2.48 | Applying alpha-rule on (273) yields: % 7.29/2.48 | (274) h(all_248_2_269) = all_248_1_268 % 7.29/2.48 | (275) h(all_25_1_14) = all_248_0_267 % 7.29/2.48 | (276) op2(all_145_0_116, all_248_0_267) = all_248_1_268 % 7.29/2.48 | (277) op1(all_27_1_17, all_25_1_14) = all_248_2_269 % 7.29/2.48 | % 7.29/2.48 | Instantiating (252) with all_252_0_273, all_252_1_274, all_252_2_275 yields: % 7.29/2.48 | (278) h(all_252_2_275) = all_252_1_274 & h(all_14_0_6) = all_252_0_273 & op2(all_145_0_116, all_252_0_273) = all_252_1_274 & op1(all_27_1_17, all_14_0_6) = all_252_2_275 % 7.29/2.48 | % 7.29/2.48 | Applying alpha-rule on (278) yields: % 7.29/2.48 | (279) h(all_252_2_275) = all_252_1_274 % 7.29/2.49 | (280) h(all_14_0_6) = all_252_0_273 % 7.29/2.49 | (281) op2(all_145_0_116, all_252_0_273) = all_252_1_274 % 7.29/2.49 | (282) op1(all_27_1_17, all_14_0_6) = all_252_2_275 % 7.29/2.49 | % 7.29/2.49 | From (193) and (231) follows: % 7.29/2.49 | (283) op2(all_0_3_3, all_107_0_75) = all_107_1_76 % 7.29/2.49 | % 7.29/2.49 | Instantiating formula (9) with all_25_1_14, all_248_0_267, all_0_1_1 and discharging atoms h(all_25_1_14) = all_248_0_267, h(all_25_1_14) = all_0_1_1, yields: % 7.29/2.49 | (284) all_248_0_267 = all_0_1_1 % 7.29/2.49 | % 7.29/2.49 | Instantiating formula (9) with all_25_1_14, all_196_0_189, all_248_0_267 and discharging atoms h(all_25_1_14) = all_248_0_267, h(all_25_1_14) = all_196_0_189, yields: % 7.29/2.49 | (285) all_248_0_267 = all_196_0_189 % 7.29/2.49 | % 7.29/2.49 | Instantiating formula (9) with all_25_1_14, all_143_0_113, all_196_0_189 and discharging atoms h(all_25_1_14) = all_196_0_189, h(all_25_1_14) = all_143_0_113, yields: % 7.29/2.49 | (286) all_196_0_189 = all_143_0_113 % 7.29/2.49 | % 7.29/2.49 | Instantiating formula (9) with all_25_1_14, all_107_0_75, all_196_0_189 and discharging atoms h(all_25_1_14) = all_196_0_189, h(all_25_1_14) = all_107_0_75, yields: % 7.29/2.49 | (287) all_196_0_189 = all_107_0_75 % 7.29/2.49 | % 7.29/2.49 | Instantiating formula (9) with all_14_0_6, all_192_0_183, all_252_0_273 and discharging atoms h(all_14_0_6) = all_252_0_273, h(all_14_0_6) = all_192_0_183, yields: % 7.29/2.49 | (288) all_252_0_273 = all_192_0_183 % 7.29/2.49 | % 7.29/2.49 | Instantiating formula (9) with all_14_0_6, all_188_0_177, all_0_2_2 and discharging atoms h(all_14_0_6) = all_188_0_177, h(all_14_0_6) = all_0_2_2, yields: % 7.29/2.49 | (289) all_188_0_177 = all_0_2_2 % 7.29/2.49 | % 7.29/2.49 | Instantiating formula (9) with all_14_0_6, all_188_0_177, all_252_0_273 and discharging atoms h(all_14_0_6) = all_252_0_273, h(all_14_0_6) = all_188_0_177, yields: % 7.29/2.49 | (290) all_252_0_273 = all_188_0_177 % 7.29/2.49 | % 7.29/2.49 | Instantiating formula (9) with all_14_0_6, all_168_0_147, all_252_0_273 and discharging atoms h(all_14_0_6) = all_252_0_273, h(all_14_0_6) = all_168_0_147, yields: % 7.29/2.49 | (291) all_252_0_273 = all_168_0_147 % 7.29/2.49 | % 7.29/2.49 | Instantiating formula (11) with all_138_2_111, all_29_1_20, all_14_0_6, all_14_0_6 and discharging atoms op1(all_14_0_6, all_29_1_20) = all_138_2_111, op1(all_14_0_6, all_14_0_6) = all_29_1_20, sorti1(all_14_0_6), yields: % 7.29/2.49 | (292) all_138_2_111 = all_14_0_6 % 7.29/2.49 | % 7.29/2.49 | Instantiating formula (11) with all_107_2_77, all_25_1_14, all_14_0_6, all_9_0_4 and discharging atoms op1(all_9_0_4, all_25_1_14) = all_107_2_77, 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.29/2.49 | (293) all_107_2_77 = all_14_0_6 % 7.29/2.49 | % 7.29/2.49 | Combining equations (290,288) yields a new equation: % 7.29/2.49 | (294) all_192_0_183 = all_188_0_177 % 7.29/2.49 | % 7.29/2.49 | Combining equations (291,288) yields a new equation: % 7.29/2.49 | (295) all_192_0_183 = all_168_0_147 % 7.29/2.49 | % 7.29/2.49 | Combining equations (285,284) yields a new equation: % 7.29/2.49 | (296) all_196_0_189 = all_0_1_1 % 7.29/2.49 | % 7.29/2.49 | Simplifying 296 yields: % 7.29/2.49 | (297) all_196_0_189 = all_0_1_1 % 7.29/2.49 | % 7.29/2.49 | Combining equations (287,286) yields a new equation: % 7.29/2.49 | (298) all_143_0_113 = all_107_0_75 % 7.29/2.49 | % 7.29/2.49 | Combining equations (297,286) yields a new equation: % 7.29/2.49 | (299) all_143_0_113 = all_0_1_1 % 7.29/2.49 | % 7.29/2.49 | Combining equations (294,295) yields a new equation: % 7.29/2.49 | (300) all_188_0_177 = all_168_0_147 % 7.29/2.49 | % 7.29/2.49 | Simplifying 300 yields: % 7.29/2.49 | (301) all_188_0_177 = all_168_0_147 % 7.29/2.49 | % 7.29/2.49 | Combining equations (289,301) yields a new equation: % 7.29/2.49 | (302) all_168_0_147 = all_0_2_2 % 7.29/2.49 | % 7.29/2.49 | Combining equations (298,299) yields a new equation: % 7.29/2.49 | (303) all_107_0_75 = all_0_1_1 % 7.29/2.49 | % 7.29/2.49 | Simplifying 303 yields: % 7.29/2.49 | (304) all_107_0_75 = all_0_1_1 % 7.29/2.49 | % 7.29/2.49 | From (292) and (239) follows: % 7.29/2.49 | (305) h(all_14_0_6) = all_138_1_110 % 7.29/2.49 | % 7.29/2.49 | From (293) and (229) follows: % 7.29/2.49 | (306) h(all_14_0_6) = all_107_1_76 % 7.29/2.49 | % 7.29/2.49 | From (302) and (255) follows: % 7.29/2.49 | (96) h(all_14_0_6) = all_0_2_2 % 7.29/2.49 | % 7.29/2.49 | From (304) and (283) follows: % 7.29/2.49 | (308) op2(all_0_3_3, all_0_1_1) = all_107_1_76 % 7.29/2.49 | % 7.29/2.49 | Instantiating formula (9) with all_14_0_6, all_138_1_110, all_0_2_2 and discharging atoms h(all_14_0_6) = all_138_1_110, h(all_14_0_6) = all_0_2_2, yields: % 7.29/2.49 | (309) all_138_1_110 = all_0_2_2 % 7.29/2.49 | % 7.29/2.49 | Instantiating formula (9) with all_14_0_6, all_107_1_76, all_138_1_110 and discharging atoms h(all_14_0_6) = all_138_1_110, h(all_14_0_6) = all_107_1_76, yields: % 7.29/2.49 | (310) all_138_1_110 = all_107_1_76 % 7.29/2.49 | % 7.29/2.49 | Instantiating formula (5) with all_0_3_3, all_0_1_1, all_107_1_76, all_0_0_0 and discharging atoms op2(all_0_3_3, all_0_1_1) = all_107_1_76, op2(all_0_3_3, all_0_1_1) = all_0_0_0, yields: % 7.29/2.49 | (311) all_107_1_76 = all_0_0_0 % 7.29/2.49 | % 7.29/2.49 | Combining equations (310,309) yields a new equation: % 7.29/2.49 | (312) all_107_1_76 = all_0_2_2 % 7.29/2.49 | % 7.29/2.49 | Simplifying 312 yields: % 7.29/2.49 | (313) all_107_1_76 = all_0_2_2 % 7.29/2.49 | % 7.29/2.49 | Combining equations (313,311) yields a new equation: % 7.29/2.49 | (314) all_0_0_0 = all_0_2_2 % 7.29/2.49 | % 7.29/2.49 | Equations (314) can reduce 8 to: % 7.29/2.49 | (315) $false % 7.29/2.49 | % 7.29/2.49 |-The branch is then unsatisfiable % 7.29/2.49 % SZS output end Proof for theBenchmark % 7.29/2.49 % 7.29/2.49 1892ms %------------------------------------------------------------------------------