%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : ALG030+1 : TPTP v8.1.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n029.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:33:50 EDT 2022 % Result : Theorem 2.38s 1.27s % Output : Proof 4.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : ALG030+1 : TPTP v8.1.0. Released v2.7.0. % 0.10/0.11 % Command : ePrincess-casc -timeout=%d %s % 0.11/0.32 % Computer : n029.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 600 % 0.11/0.32 % DateTime : Thu Jun 9 00:40:21 EDT 2022 % 0.11/0.32 % CPUTime : % 0.17/0.57 ____ _ % 0.17/0.57 ___ / __ \_____(_)___ ________ __________ % 0.17/0.57 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.17/0.57 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.17/0.57 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.17/0.57 % 0.17/0.57 A Theorem Prover for First-Order Logic % 0.17/0.57 (ePrincess v.1.0) % 0.17/0.57 % 0.17/0.57 (c) Philipp Rümmer, 2009-2015 % 0.17/0.57 (c) Peter Backeman, 2014-2015 % 0.17/0.57 (contributions by Angelo Brillout, Peter Baumgartner) % 0.17/0.57 Free software under GNU Lesser General Public License (LGPL). % 0.17/0.57 Bug reports to peter@backeman.se % 0.17/0.57 % 0.17/0.57 For more information, visit http://user.uu.se/~petba168/breu/ % 0.17/0.57 % 0.17/0.57 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.67/0.62 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.42/0.90 Prover 0: Preprocessing ... % 1.75/1.07 Prover 0: Constructing countermodel ... % 2.38/1.27 Prover 0: proved (650ms) % 2.38/1.27 % 2.38/1.27 No countermodel exists, formula is valid % 2.38/1.27 % SZS status Theorem for theBenchmark % 2.38/1.27 % 2.38/1.27 Generating proof ... found it (size 145) % 4.03/1.77 % 4.03/1.77 % SZS output start Proof for theBenchmark % 4.03/1.77 Assumed formulas after preprocessing and simplification: % 4.03/1.77 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ( ~ (v3 = v2) & op1(v1, v0) = v3 & op1(v0, v1) = v2 & sorti1(v1) & sorti1(v0) & ! [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(v5, v4) = v6) | ~ sorti2(v5) | ~ sorti2(v4) | op2(v4, v5) = v6) & ! [v4] : ! [v5] : ! [v6] : ( ~ (op2(v4, v5) = v6) | ~ sorti2(v5) | ~ sorti2(v4) | op2(v5, v4) = v6) & ! [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))))) % 4.44/1.80 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3 yields: % 4.44/1.80 | (1) ~ (all_0_0_0 = all_0_1_1) & op1(all_0_2_2, all_0_3_3) = all_0_0_0 & op1(all_0_3_3, all_0_2_2) = all_0_1_1 & sorti1(all_0_2_2) & sorti1(all_0_3_3) & ! [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(v1, v0) = v2) | ~ sorti2(v1) | ~ sorti2(v0) | op2(v0, v1) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (op2(v0, v1) = v2) | ~ sorti2(v1) | ~ sorti2(v0) | op2(v1, v0) = v2) & ! [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)))) % 4.54/1.81 | % 4.54/1.81 | Applying alpha-rule on (1) yields: % 4.54/1.81 | (2) ! [v0] : ! [v1] : ! [v2] : ( ~ (op2(v0, v1) = v2) | ~ sorti2(v1) | ~ sorti2(v0) | sorti2(v2)) % 4.54/1.81 | (3) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (j(v2) = v1) | ~ (j(v2) = v0)) % 4.54/1.81 | (4) op1(all_0_2_2, all_0_3_3) = all_0_0_0 % 4.54/1.81 | (5) op1(all_0_3_3, all_0_2_2) = all_0_1_1 % 4.54/1.81 | (6) ! [v0] : ( ~ sorti2(v0) | ? [v1] : (j(v0) = v1 & sorti1(v1))) % 4.54/1.81 | (7) sorti1(all_0_3_3) % 4.54/1.81 | (8) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h(v2) = v1) | ~ (h(v2) = v0)) % 4.54/1.81 | (9) ! [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)))) % 4.54/1.81 | (10) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op1(v3, v2) = v1) | ~ (op1(v3, v2) = v0)) % 4.54/1.81 | (11) ! [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)))) % 4.54/1.81 | (12) ! [v0] : ! [v1] : ! [v2] : ( ~ (op2(v1, v0) = v2) | ~ sorti2(v1) | ~ sorti2(v0) | op2(v0, v1) = v2) % 4.54/1.81 | (13) ! [v0] : ( ~ sorti1(v0) | ? [v1] : (h(v0) = v1 & sorti2(v1))) % 4.54/1.81 | (14) sorti1(all_0_2_2) % 4.54/1.81 | (15) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (op2(v3, v2) = v1) | ~ (op2(v3, v2) = v0)) % 4.54/1.81 | (16) ! [v0] : ! [v1] : ! [v2] : ( ~ (op1(v0, v1) = v2) | ~ sorti1(v1) | ~ sorti1(v0) | sorti1(v2)) % 4.54/1.81 | (17) ! [v0] : ! [v1] : ! [v2] : ( ~ (op2(v0, v1) = v2) | ~ sorti2(v1) | ~ sorti2(v0) | op2(v1, v0) = v2) % 4.54/1.81 | (18) ! [v0] : ( ~ sorti1(v0) | ? [v1] : (j(v1) = v0 & h(v0) = v1)) % 4.54/1.81 | (19) ! [v0] : ( ~ sorti2(v0) | ? [v1] : (j(v0) = v1 & h(v1) = v0)) % 4.54/1.81 | (20) ~ (all_0_0_0 = all_0_1_1) % 4.54/1.81 | % 4.54/1.81 | Instantiating formula (13) with all_0_2_2 and discharging atoms sorti1(all_0_2_2), yields: % 4.54/1.81 | (21) ? [v0] : (h(all_0_2_2) = v0 & sorti2(v0)) % 4.54/1.81 | % 4.54/1.81 | Instantiating formula (11) with all_0_2_2 and discharging atoms sorti1(all_0_2_2), yields: % 4.54/1.81 | (22) ? [v0] : (h(all_0_2_2) = v0 & ! [v1] : ( ~ sorti1(v1) | ? [v2] : ? [v3] : ? [v4] : (h(v2) = v3 & h(v1) = v4 & op2(v0, v4) = v3 & op1(all_0_2_2, v1) = v2))) % 4.54/1.81 | % 4.54/1.81 | Instantiating formula (16) with all_0_0_0, all_0_3_3, all_0_2_2 and discharging atoms op1(all_0_2_2, all_0_3_3) = all_0_0_0, sorti1(all_0_2_2), sorti1(all_0_3_3), yields: % 4.54/1.81 | (23) sorti1(all_0_0_0) % 4.54/1.81 | % 4.54/1.81 | Instantiating formula (16) with all_0_1_1, all_0_2_2, all_0_3_3 and discharging atoms op1(all_0_3_3, all_0_2_2) = all_0_1_1, sorti1(all_0_2_2), sorti1(all_0_3_3), yields: % 4.54/1.81 | (24) sorti1(all_0_1_1) % 4.54/1.81 | % 4.54/1.81 | Instantiating formula (18) with all_0_3_3 and discharging atoms sorti1(all_0_3_3), yields: % 4.54/1.81 | (25) ? [v0] : (j(v0) = all_0_3_3 & h(all_0_3_3) = v0) % 4.54/1.81 | % 4.54/1.81 | Instantiating formula (13) with all_0_3_3 and discharging atoms sorti1(all_0_3_3), yields: % 4.54/1.82 | (26) ? [v0] : (h(all_0_3_3) = v0 & sorti2(v0)) % 4.54/1.82 | % 4.54/1.82 | Instantiating formula (11) with all_0_3_3 and discharging atoms sorti1(all_0_3_3), yields: % 4.54/1.82 | (27) ? [v0] : (h(all_0_3_3) = v0 & ! [v1] : ( ~ sorti1(v1) | ? [v2] : ? [v3] : ? [v4] : (h(v2) = v3 & h(v1) = v4 & op2(v0, v4) = v3 & op1(all_0_3_3, v1) = v2))) % 4.54/1.82 | % 4.54/1.82 | Instantiating (21) with all_9_0_4 yields: % 4.54/1.82 | (28) h(all_0_2_2) = all_9_0_4 & sorti2(all_9_0_4) % 4.54/1.82 | % 4.54/1.82 | Applying alpha-rule on (28) yields: % 4.54/1.82 | (29) h(all_0_2_2) = all_9_0_4 % 4.54/1.82 | (30) sorti2(all_9_0_4) % 4.54/1.82 | % 4.54/1.82 | Instantiating (27) with all_11_0_5 yields: % 4.54/1.82 | (31) h(all_0_3_3) = all_11_0_5 & ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_11_0_5, v3) = v2 & op1(all_0_3_3, v0) = v1)) % 4.54/1.82 | % 4.54/1.82 | Applying alpha-rule on (31) yields: % 4.54/1.82 | (32) h(all_0_3_3) = all_11_0_5 % 4.54/1.82 | (33) ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_11_0_5, v3) = v2 & op1(all_0_3_3, v0) = v1)) % 4.54/1.82 | % 4.54/1.82 | Instantiating formula (33) with all_0_2_2 and discharging atoms sorti1(all_0_2_2), yields: % 4.54/1.82 | (34) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_0_2_2) = v2 & op2(all_11_0_5, v2) = v1 & op1(all_0_3_3, all_0_2_2) = v0) % 4.54/1.82 | % 4.54/1.82 | Instantiating formula (33) with all_0_3_3 and discharging atoms sorti1(all_0_3_3), yields: % 4.54/1.82 | (35) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_0_3_3) = v2 & op2(all_11_0_5, v2) = v1 & op1(all_0_3_3, all_0_3_3) = v0) % 4.54/1.82 | % 4.54/1.82 | Instantiating (26) with all_14_0_6 yields: % 4.54/1.82 | (36) h(all_0_3_3) = all_14_0_6 & sorti2(all_14_0_6) % 4.54/1.82 | % 4.54/1.82 | Applying alpha-rule on (36) yields: % 4.54/1.82 | (37) h(all_0_3_3) = all_14_0_6 % 4.54/1.82 | (38) sorti2(all_14_0_6) % 4.54/1.82 | % 4.54/1.82 | Instantiating (25) with all_18_0_8 yields: % 4.54/1.82 | (39) j(all_18_0_8) = all_0_3_3 & h(all_0_3_3) = all_18_0_8 % 4.54/1.82 | % 4.54/1.82 | Applying alpha-rule on (39) yields: % 4.54/1.82 | (40) j(all_18_0_8) = all_0_3_3 % 4.62/1.82 | (41) h(all_0_3_3) = all_18_0_8 % 4.62/1.82 | % 4.62/1.82 | Instantiating (22) with all_20_0_9 yields: % 4.62/1.82 | (42) h(all_0_2_2) = all_20_0_9 & ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_20_0_9, v3) = v2 & op1(all_0_2_2, v0) = v1)) % 4.62/1.82 | % 4.62/1.82 | Applying alpha-rule on (42) yields: % 4.62/1.82 | (43) h(all_0_2_2) = all_20_0_9 % 4.62/1.82 | (44) ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_20_0_9, v3) = v2 & op1(all_0_2_2, v0) = v1)) % 4.62/1.82 | % 4.62/1.82 | Instantiating formula (44) with all_0_2_2 and discharging atoms sorti1(all_0_2_2), yields: % 4.62/1.82 | (45) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_0_2_2) = v2 & op2(all_20_0_9, v2) = v1 & op1(all_0_2_2, all_0_2_2) = v0) % 4.62/1.82 | % 4.62/1.82 | Instantiating formula (44) with all_0_3_3 and discharging atoms sorti1(all_0_3_3), yields: % 4.62/1.82 | (46) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_0_3_3) = v2 & op2(all_20_0_9, v2) = v1 & op1(all_0_2_2, all_0_3_3) = v0) % 4.62/1.82 | % 4.62/1.82 | Instantiating (35) with all_23_0_10, all_23_1_11, all_23_2_12 yields: % 4.62/1.82 | (47) h(all_23_2_12) = all_23_1_11 & h(all_0_3_3) = all_23_0_10 & op2(all_11_0_5, all_23_0_10) = all_23_1_11 & op1(all_0_3_3, all_0_3_3) = all_23_2_12 % 4.62/1.82 | % 4.62/1.82 | Applying alpha-rule on (47) yields: % 4.62/1.82 | (48) h(all_23_2_12) = all_23_1_11 % 4.62/1.82 | (49) h(all_0_3_3) = all_23_0_10 % 4.62/1.82 | (50) op2(all_11_0_5, all_23_0_10) = all_23_1_11 % 4.62/1.82 | (51) op1(all_0_3_3, all_0_3_3) = all_23_2_12 % 4.62/1.82 | % 4.62/1.82 | Instantiating (34) with all_25_0_13, all_25_1_14, all_25_2_15 yields: % 4.62/1.82 | (52) h(all_25_2_15) = all_25_1_14 & h(all_0_2_2) = all_25_0_13 & op2(all_11_0_5, all_25_0_13) = all_25_1_14 & op1(all_0_3_3, all_0_2_2) = all_25_2_15 % 4.62/1.82 | % 4.62/1.82 | Applying alpha-rule on (52) yields: % 4.62/1.82 | (53) h(all_25_2_15) = all_25_1_14 % 4.62/1.82 | (54) h(all_0_2_2) = all_25_0_13 % 4.62/1.82 | (55) op2(all_11_0_5, all_25_0_13) = all_25_1_14 % 4.62/1.82 | (56) op1(all_0_3_3, all_0_2_2) = all_25_2_15 % 4.62/1.82 | % 4.62/1.82 | Instantiating (46) with all_27_0_16, all_27_1_17, all_27_2_18 yields: % 4.62/1.82 | (57) h(all_27_2_18) = all_27_1_17 & h(all_0_3_3) = all_27_0_16 & op2(all_20_0_9, all_27_0_16) = all_27_1_17 & op1(all_0_2_2, all_0_3_3) = all_27_2_18 % 4.62/1.82 | % 4.62/1.82 | Applying alpha-rule on (57) yields: % 4.62/1.82 | (58) h(all_27_2_18) = all_27_1_17 % 4.62/1.82 | (59) h(all_0_3_3) = all_27_0_16 % 4.62/1.82 | (60) op2(all_20_0_9, all_27_0_16) = all_27_1_17 % 4.62/1.82 | (61) op1(all_0_2_2, all_0_3_3) = all_27_2_18 % 4.62/1.82 | % 4.62/1.82 | Instantiating (45) with all_29_0_19, all_29_1_20, all_29_2_21 yields: % 4.62/1.82 | (62) h(all_29_2_21) = all_29_1_20 & h(all_0_2_2) = all_29_0_19 & op2(all_20_0_9, all_29_0_19) = all_29_1_20 & op1(all_0_2_2, all_0_2_2) = all_29_2_21 % 4.62/1.83 | % 4.62/1.83 | Applying alpha-rule on (62) yields: % 4.62/1.83 | (63) h(all_29_2_21) = all_29_1_20 % 4.62/1.83 | (64) h(all_0_2_2) = all_29_0_19 % 4.62/1.83 | (65) op2(all_20_0_9, all_29_0_19) = all_29_1_20 % 4.62/1.83 | (66) op1(all_0_2_2, all_0_2_2) = all_29_2_21 % 4.62/1.83 | % 4.62/1.83 | Instantiating formula (8) with all_0_2_2, all_25_0_13, all_29_0_19 and discharging atoms h(all_0_2_2) = all_29_0_19, h(all_0_2_2) = all_25_0_13, yields: % 4.62/1.83 | (67) all_29_0_19 = all_25_0_13 % 4.62/1.83 | % 4.62/1.83 | Instantiating formula (8) with all_0_2_2, all_20_0_9, all_25_0_13 and discharging atoms h(all_0_2_2) = all_25_0_13, h(all_0_2_2) = all_20_0_9, yields: % 4.62/1.83 | (68) all_25_0_13 = all_20_0_9 % 4.62/1.83 | % 4.62/1.83 | Instantiating formula (8) with all_0_2_2, all_9_0_4, all_29_0_19 and discharging atoms h(all_0_2_2) = all_29_0_19, h(all_0_2_2) = all_9_0_4, yields: % 4.62/1.83 | (69) all_29_0_19 = all_9_0_4 % 4.62/1.83 | % 4.62/1.83 | Instantiating formula (8) with all_0_3_3, all_23_0_10, all_27_0_16 and discharging atoms h(all_0_3_3) = all_27_0_16, h(all_0_3_3) = all_23_0_10, yields: % 4.62/1.83 | (70) all_27_0_16 = all_23_0_10 % 4.62/1.83 | % 4.62/1.83 | Instantiating formula (8) with all_0_3_3, all_18_0_8, all_27_0_16 and discharging atoms h(all_0_3_3) = all_27_0_16, h(all_0_3_3) = all_18_0_8, yields: % 4.62/1.83 | (71) all_27_0_16 = all_18_0_8 % 4.62/1.83 | % 4.62/1.83 | Instantiating formula (8) with all_0_3_3, all_14_0_6, all_27_0_16 and discharging atoms h(all_0_3_3) = all_27_0_16, h(all_0_3_3) = all_14_0_6, yields: % 4.62/1.83 | (72) all_27_0_16 = all_14_0_6 % 4.62/1.83 | % 4.62/1.83 | Instantiating formula (8) with all_0_3_3, all_11_0_5, all_27_0_16 and discharging atoms h(all_0_3_3) = all_27_0_16, h(all_0_3_3) = all_11_0_5, yields: % 4.62/1.83 | (73) all_27_0_16 = all_11_0_5 % 4.62/1.83 | % 4.62/1.83 | Instantiating formula (10) with all_0_2_2, all_0_3_3, all_27_2_18, all_0_0_0 and discharging atoms op1(all_0_2_2, all_0_3_3) = all_27_2_18, op1(all_0_2_2, all_0_3_3) = all_0_0_0, yields: % 4.62/1.83 | (74) all_27_2_18 = all_0_0_0 % 4.62/1.83 | % 4.62/1.83 | Instantiating formula (10) with all_0_3_3, all_0_2_2, all_25_2_15, all_0_1_1 and discharging atoms op1(all_0_3_3, all_0_2_2) = all_25_2_15, op1(all_0_3_3, all_0_2_2) = all_0_1_1, yields: % 4.62/1.83 | (75) all_25_2_15 = all_0_1_1 % 4.62/1.83 | % 4.62/1.83 | Combining equations (67,69) yields a new equation: % 4.62/1.83 | (76) all_25_0_13 = all_9_0_4 % 4.62/1.83 | % 4.62/1.83 | Simplifying 76 yields: % 4.62/1.83 | (77) all_25_0_13 = all_9_0_4 % 4.62/1.83 | % 4.62/1.83 | Combining equations (72,70) yields a new equation: % 4.62/1.83 | (78) all_23_0_10 = all_14_0_6 % 4.62/1.83 | % 4.62/1.83 | Combining equations (71,70) yields a new equation: % 4.62/1.83 | (79) all_23_0_10 = all_18_0_8 % 4.62/1.83 | % 4.62/1.83 | Combining equations (73,70) yields a new equation: % 4.62/1.83 | (80) all_23_0_10 = all_11_0_5 % 4.62/1.83 | % 4.62/1.83 | Combining equations (68,77) yields a new equation: % 4.62/1.83 | (81) all_20_0_9 = all_9_0_4 % 4.62/1.83 | % 4.62/1.83 | Simplifying 81 yields: % 4.62/1.83 | (82) all_20_0_9 = all_9_0_4 % 4.62/1.83 | % 4.62/1.83 | Combining equations (80,79) yields a new equation: % 4.62/1.83 | (83) all_18_0_8 = all_11_0_5 % 4.62/1.83 | % 4.62/1.83 | Combining equations (78,79) yields a new equation: % 4.62/1.83 | (84) all_18_0_8 = all_14_0_6 % 4.62/1.83 | % 4.62/1.83 | Combining equations (84,83) yields a new equation: % 4.62/1.83 | (85) all_14_0_6 = all_11_0_5 % 4.62/1.83 | % 4.62/1.83 | Simplifying 85 yields: % 4.62/1.83 | (86) all_14_0_6 = all_11_0_5 % 4.62/1.83 | % 4.62/1.83 | Combining equations (83,79) yields a new equation: % 4.62/1.83 | (80) all_23_0_10 = all_11_0_5 % 4.62/1.83 | % 4.62/1.83 | Combining equations (80,70) yields a new equation: % 4.62/1.83 | (73) all_27_0_16 = all_11_0_5 % 4.62/1.83 | % 4.62/1.83 | From (74) and (58) follows: % 4.62/1.83 | (89) h(all_0_0_0) = all_27_1_17 % 4.62/1.83 | % 4.62/1.83 | From (75) and (53) follows: % 4.62/1.83 | (90) h(all_0_1_1) = all_25_1_14 % 4.62/1.83 | % 4.62/1.83 | From (82)(73) and (60) follows: % 4.62/1.83 | (91) op2(all_9_0_4, all_11_0_5) = all_27_1_17 % 4.62/1.83 | % 4.62/1.83 | From (77) and (55) follows: % 4.62/1.83 | (92) op2(all_11_0_5, all_9_0_4) = all_25_1_14 % 4.62/1.83 | % 4.62/1.83 | From (86) and (38) follows: % 4.62/1.83 | (93) sorti2(all_11_0_5) % 4.62/1.83 | % 4.62/1.83 | Instantiating formula (9) with all_11_0_5 and discharging atoms sorti2(all_11_0_5), yields: % 4.62/1.83 | (94) ? [v0] : (j(all_11_0_5) = v0 & ! [v1] : ( ~ sorti2(v1) | ? [v2] : ? [v3] : ? [v4] : (j(v2) = v3 & j(v1) = v4 & op2(all_11_0_5, v1) = v2 & op1(v0, v4) = v3))) % 4.62/1.83 | % 4.62/1.83 | Instantiating formula (12) with all_27_1_17, all_9_0_4, all_11_0_5 and discharging atoms op2(all_9_0_4, all_11_0_5) = all_27_1_17, sorti2(all_11_0_5), sorti2(all_9_0_4), yields: % 4.62/1.83 | (95) op2(all_11_0_5, all_9_0_4) = all_27_1_17 % 4.62/1.83 | % 4.62/1.83 | Instantiating formula (9) with all_9_0_4 and discharging atoms sorti2(all_9_0_4), yields: % 4.62/1.83 | (96) ? [v0] : (j(all_9_0_4) = v0 & ! [v1] : ( ~ sorti2(v1) | ? [v2] : ? [v3] : ? [v4] : (j(v2) = v3 & j(v1) = v4 & op2(all_9_0_4, v1) = v2 & op1(v0, v4) = v3))) % 4.62/1.84 | % 4.62/1.84 | Instantiating formula (18) with all_0_0_0 and discharging atoms sorti1(all_0_0_0), yields: % 4.62/1.84 | (97) ? [v0] : (j(v0) = all_0_0_0 & h(all_0_0_0) = v0) % 4.62/1.84 | % 4.62/1.84 | Instantiating formula (11) with all_0_0_0 and discharging atoms sorti1(all_0_0_0), yields: % 4.62/1.84 | (98) ? [v0] : (h(all_0_0_0) = v0 & ! [v1] : ( ~ sorti1(v1) | ? [v2] : ? [v3] : ? [v4] : (h(v2) = v3 & h(v1) = v4 & op2(v0, v4) = v3 & op1(all_0_0_0, v1) = v2))) % 4.62/1.84 | % 4.62/1.84 | Instantiating formula (44) with all_0_1_1 and discharging atoms sorti1(all_0_1_1), yields: % 4.62/1.84 | (99) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_0_1_1) = v2 & op2(all_20_0_9, v2) = v1 & op1(all_0_2_2, all_0_1_1) = v0) % 4.62/1.84 | % 4.62/1.84 | Instantiating formula (33) with all_0_1_1 and discharging atoms sorti1(all_0_1_1), yields: % 4.62/1.84 | (100) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_0_1_1) = v2 & op2(all_11_0_5, v2) = v1 & op1(all_0_3_3, all_0_1_1) = v0) % 4.62/1.84 | % 4.62/1.84 | Instantiating formula (18) with all_0_1_1 and discharging atoms sorti1(all_0_1_1), yields: % 4.62/1.84 | (101) ? [v0] : (j(v0) = all_0_1_1 & h(all_0_1_1) = v0) % 4.62/1.84 | % 4.62/1.84 | Instantiating formula (13) with all_0_1_1 and discharging atoms sorti1(all_0_1_1), yields: % 4.62/1.84 | (102) ? [v0] : (h(all_0_1_1) = v0 & sorti2(v0)) % 4.62/1.84 | % 4.62/1.84 | Instantiating formula (11) with all_0_1_1 and discharging atoms sorti1(all_0_1_1), yields: % 4.62/1.84 | (103) ? [v0] : (h(all_0_1_1) = v0 & ! [v1] : ( ~ sorti1(v1) | ? [v2] : ? [v3] : ? [v4] : (h(v2) = v3 & h(v1) = v4 & op2(v0, v4) = v3 & op1(all_0_1_1, v1) = v2))) % 4.62/1.84 | % 4.62/1.84 | Instantiating (103) with all_41_0_22 yields: % 4.62/1.84 | (104) h(all_0_1_1) = 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_0_1_1, v0) = v1)) % 4.62/1.84 | % 4.62/1.84 | Applying alpha-rule on (104) yields: % 4.62/1.84 | (105) h(all_0_1_1) = all_41_0_22 % 4.62/1.84 | (106) ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_41_0_22, v3) = v2 & op1(all_0_1_1, v0) = v1)) % 4.62/1.84 | % 4.62/1.84 | Instantiating formula (106) with all_0_0_0 and discharging atoms sorti1(all_0_0_0), yields: % 4.62/1.84 | (107) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_0_0_0) = v2 & op2(all_41_0_22, v2) = v1 & op1(all_0_1_1, all_0_0_0) = v0) % 4.62/1.84 | % 4.62/1.84 | Instantiating formula (106) with all_0_1_1 and discharging atoms sorti1(all_0_1_1), yields: % 4.62/1.84 | (108) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_0_1_1) = v2 & op2(all_41_0_22, v2) = v1 & op1(all_0_1_1, all_0_1_1) = v0) % 4.62/1.84 | % 4.62/1.84 | Instantiating (101) with all_44_0_23 yields: % 4.62/1.84 | (109) j(all_44_0_23) = all_0_1_1 & h(all_0_1_1) = all_44_0_23 % 4.62/1.84 | % 4.62/1.84 | Applying alpha-rule on (109) yields: % 4.62/1.84 | (110) j(all_44_0_23) = all_0_1_1 % 4.62/1.84 | (111) h(all_0_1_1) = all_44_0_23 % 4.62/1.84 | % 4.62/1.84 | Instantiating (100) with all_46_0_24, all_46_1_25, all_46_2_26 yields: % 4.62/1.84 | (112) h(all_46_2_26) = all_46_1_25 & h(all_0_1_1) = all_46_0_24 & op2(all_11_0_5, all_46_0_24) = all_46_1_25 & op1(all_0_3_3, all_0_1_1) = all_46_2_26 % 4.62/1.84 | % 4.62/1.84 | Applying alpha-rule on (112) yields: % 4.62/1.84 | (113) h(all_46_2_26) = all_46_1_25 % 4.62/1.84 | (114) h(all_0_1_1) = all_46_0_24 % 4.62/1.84 | (115) op2(all_11_0_5, all_46_0_24) = all_46_1_25 % 4.62/1.84 | (116) op1(all_0_3_3, all_0_1_1) = all_46_2_26 % 4.62/1.84 | % 4.62/1.84 | Instantiating (102) with all_52_0_33 yields: % 4.62/1.84 | (117) h(all_0_1_1) = all_52_0_33 & sorti2(all_52_0_33) % 4.62/1.84 | % 4.62/1.84 | Applying alpha-rule on (117) yields: % 4.62/1.84 | (118) h(all_0_1_1) = all_52_0_33 % 4.62/1.84 | (119) sorti2(all_52_0_33) % 4.62/1.84 | % 4.62/1.84 | Instantiating (94) with all_54_0_34 yields: % 4.62/1.84 | (120) j(all_11_0_5) = all_54_0_34 & ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_11_0_5, v0) = v1 & op1(all_54_0_34, v3) = v2)) % 4.62/1.84 | % 4.62/1.84 | Applying alpha-rule on (120) yields: % 4.62/1.84 | (121) j(all_11_0_5) = all_54_0_34 % 4.62/1.84 | (122) ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_11_0_5, v0) = v1 & op1(all_54_0_34, v3) = v2)) % 4.62/1.84 | % 4.62/1.84 | Instantiating formula (122) with all_9_0_4 and discharging atoms sorti2(all_9_0_4), yields: % 4.62/1.84 | (123) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_9_0_4) = v2 & op2(all_11_0_5, all_9_0_4) = v0 & op1(all_54_0_34, v2) = v1) % 4.62/1.85 | % 4.62/1.85 | Instantiating (99) with all_57_0_35, all_57_1_36, all_57_2_37 yields: % 4.62/1.85 | (124) h(all_57_2_37) = all_57_1_36 & h(all_0_1_1) = all_57_0_35 & op2(all_20_0_9, all_57_0_35) = all_57_1_36 & op1(all_0_2_2, all_0_1_1) = all_57_2_37 % 4.62/1.85 | % 4.62/1.85 | Applying alpha-rule on (124) yields: % 4.62/1.85 | (125) h(all_57_2_37) = all_57_1_36 % 4.62/1.85 | (126) h(all_0_1_1) = all_57_0_35 % 4.62/1.85 | (127) op2(all_20_0_9, all_57_0_35) = all_57_1_36 % 4.62/1.85 | (128) op1(all_0_2_2, all_0_1_1) = all_57_2_37 % 4.62/1.85 | % 4.62/1.85 | Instantiating (98) with all_61_0_39 yields: % 4.62/1.85 | (129) h(all_0_0_0) = all_61_0_39 & ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_61_0_39, v3) = v2 & op1(all_0_0_0, v0) = v1)) % 4.62/1.85 | % 4.62/1.85 | Applying alpha-rule on (129) yields: % 4.62/1.85 | (130) h(all_0_0_0) = all_61_0_39 % 4.62/1.85 | (131) ! [v0] : ( ~ sorti1(v0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & h(v0) = v3 & op2(all_61_0_39, v3) = v2 & op1(all_0_0_0, v0) = v1)) % 4.62/1.85 | % 4.62/1.85 | Instantiating formula (131) with all_0_0_0 and discharging atoms sorti1(all_0_0_0), yields: % 4.62/1.85 | (132) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_0_0_0) = v2 & op2(all_61_0_39, v2) = v1 & op1(all_0_0_0, all_0_0_0) = v0) % 4.62/1.85 | % 4.62/1.85 | Instantiating formula (131) with all_0_1_1 and discharging atoms sorti1(all_0_1_1), yields: % 4.62/1.85 | (133) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & h(all_0_1_1) = v2 & op2(all_61_0_39, v2) = v1 & op1(all_0_0_0, all_0_1_1) = v0) % 4.62/1.85 | % 4.62/1.85 | Instantiating (96) with all_64_0_40 yields: % 4.62/1.85 | (134) j(all_9_0_4) = all_64_0_40 & ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_9_0_4, v0) = v1 & op1(all_64_0_40, v3) = v2)) % 4.62/1.85 | % 4.62/1.85 | Applying alpha-rule on (134) yields: % 4.62/1.85 | (135) j(all_9_0_4) = all_64_0_40 % 4.62/1.85 | (136) ! [v0] : ( ~ sorti2(v0) | ? [v1] : ? [v2] : ? [v3] : (j(v1) = v2 & j(v0) = v3 & op2(all_9_0_4, v0) = v1 & op1(all_64_0_40, v3) = v2)) % 4.62/1.85 | % 4.62/1.85 | Instantiating formula (136) with all_11_0_5 and discharging atoms sorti2(all_11_0_5), yields: % 4.62/1.85 | (137) ? [v0] : ? [v1] : ? [v2] : (j(v0) = v1 & j(all_11_0_5) = v2 & op2(all_9_0_4, all_11_0_5) = v0 & op1(all_64_0_40, v2) = v1) % 4.62/1.85 | % 4.62/1.85 | Instantiating (97) with all_67_0_41 yields: % 4.62/1.85 | (138) j(all_67_0_41) = all_0_0_0 & h(all_0_0_0) = all_67_0_41 % 4.62/1.85 | % 4.62/1.85 | Applying alpha-rule on (138) yields: % 4.62/1.85 | (139) j(all_67_0_41) = all_0_0_0 % 4.62/1.85 | (140) h(all_0_0_0) = all_67_0_41 % 4.62/1.85 | % 4.62/1.85 | Instantiating (108) with all_73_0_48, all_73_1_49, all_73_2_50 yields: % 4.62/1.85 | (141) h(all_73_2_50) = all_73_1_49 & h(all_0_1_1) = all_73_0_48 & op2(all_41_0_22, all_73_0_48) = all_73_1_49 & op1(all_0_1_1, all_0_1_1) = all_73_2_50 % 4.62/1.85 | % 4.62/1.85 | Applying alpha-rule on (141) yields: % 4.62/1.85 | (142) h(all_73_2_50) = all_73_1_49 % 4.62/1.85 | (143) h(all_0_1_1) = all_73_0_48 % 4.62/1.85 | (144) op2(all_41_0_22, all_73_0_48) = all_73_1_49 % 4.62/1.85 | (145) op1(all_0_1_1, all_0_1_1) = all_73_2_50 % 4.62/1.85 | % 4.62/1.85 | Instantiating (107) with all_75_0_51, all_75_1_52, all_75_2_53 yields: % 4.62/1.85 | (146) h(all_75_2_53) = all_75_1_52 & h(all_0_0_0) = all_75_0_51 & op2(all_41_0_22, all_75_0_51) = all_75_1_52 & op1(all_0_1_1, all_0_0_0) = all_75_2_53 % 4.62/1.85 | % 4.62/1.85 | Applying alpha-rule on (146) yields: % 4.62/1.85 | (147) h(all_75_2_53) = all_75_1_52 % 4.62/1.85 | (148) h(all_0_0_0) = all_75_0_51 % 4.62/1.85 | (149) op2(all_41_0_22, all_75_0_51) = all_75_1_52 % 4.62/1.85 | (150) op1(all_0_1_1, all_0_0_0) = all_75_2_53 % 4.62/1.85 | % 4.62/1.85 | Instantiating (123) with all_77_0_54, all_77_1_55, all_77_2_56 yields: % 4.62/1.85 | (151) j(all_77_2_56) = all_77_1_55 & j(all_9_0_4) = all_77_0_54 & op2(all_11_0_5, all_9_0_4) = all_77_2_56 & op1(all_54_0_34, all_77_0_54) = all_77_1_55 % 4.62/1.85 | % 4.62/1.85 | Applying alpha-rule on (151) yields: % 4.62/1.85 | (152) j(all_77_2_56) = all_77_1_55 % 4.62/1.86 | (153) j(all_9_0_4) = all_77_0_54 % 4.62/1.86 | (154) op2(all_11_0_5, all_9_0_4) = all_77_2_56 % 4.62/1.86 | (155) op1(all_54_0_34, all_77_0_54) = all_77_1_55 % 4.62/1.86 | % 4.62/1.86 | Instantiating (133) with all_83_0_63, all_83_1_64, all_83_2_65 yields: % 4.62/1.86 | (156) h(all_83_2_65) = all_83_1_64 & h(all_0_1_1) = all_83_0_63 & op2(all_61_0_39, all_83_0_63) = all_83_1_64 & op1(all_0_0_0, all_0_1_1) = all_83_2_65 % 4.62/1.86 | % 4.62/1.86 | Applying alpha-rule on (156) yields: % 4.62/1.86 | (157) h(all_83_2_65) = all_83_1_64 % 4.62/1.86 | (158) h(all_0_1_1) = all_83_0_63 % 4.62/1.86 | (159) op2(all_61_0_39, all_83_0_63) = all_83_1_64 % 4.62/1.86 | (160) op1(all_0_0_0, all_0_1_1) = all_83_2_65 % 4.62/1.86 | % 4.62/1.86 | Instantiating (132) with all_85_0_66, all_85_1_67, all_85_2_68 yields: % 4.62/1.86 | (161) h(all_85_2_68) = all_85_1_67 & h(all_0_0_0) = all_85_0_66 & op2(all_61_0_39, all_85_0_66) = all_85_1_67 & op1(all_0_0_0, all_0_0_0) = all_85_2_68 % 4.62/1.86 | % 4.62/1.86 | Applying alpha-rule on (161) yields: % 4.62/1.86 | (162) h(all_85_2_68) = all_85_1_67 % 4.62/1.86 | (163) h(all_0_0_0) = all_85_0_66 % 4.62/1.86 | (164) op2(all_61_0_39, all_85_0_66) = all_85_1_67 % 4.62/1.86 | (165) op1(all_0_0_0, all_0_0_0) = all_85_2_68 % 4.62/1.86 | % 4.62/1.86 | Instantiating (137) with all_91_0_75, all_91_1_76, all_91_2_77 yields: % 4.62/1.86 | (166) j(all_91_2_77) = all_91_1_76 & j(all_11_0_5) = all_91_0_75 & op2(all_9_0_4, all_11_0_5) = all_91_2_77 & op1(all_64_0_40, all_91_0_75) = all_91_1_76 % 4.62/1.86 | % 4.62/1.86 | Applying alpha-rule on (166) yields: % 4.62/1.86 | (167) j(all_91_2_77) = all_91_1_76 % 4.62/1.86 | (168) j(all_11_0_5) = all_91_0_75 % 4.62/1.86 | (169) op2(all_9_0_4, all_11_0_5) = all_91_2_77 % 4.62/1.86 | (170) op1(all_64_0_40, all_91_0_75) = all_91_1_76 % 4.62/1.86 | % 4.62/1.86 | Instantiating formula (8) with all_0_0_0, all_75_0_51, all_27_1_17 and discharging atoms h(all_0_0_0) = all_75_0_51, h(all_0_0_0) = all_27_1_17, yields: % 4.62/1.86 | (171) all_75_0_51 = all_27_1_17 % 4.62/1.86 | % 4.62/1.86 | Instantiating formula (8) with all_0_0_0, all_75_0_51, all_85_0_66 and discharging atoms h(all_0_0_0) = all_85_0_66, h(all_0_0_0) = all_75_0_51, yields: % 4.62/1.86 | (172) all_85_0_66 = all_75_0_51 % 4.62/1.86 | % 4.62/1.86 | Instantiating formula (8) with all_0_0_0, all_67_0_41, all_85_0_66 and discharging atoms h(all_0_0_0) = all_85_0_66, h(all_0_0_0) = all_67_0_41, yields: % 4.62/1.86 | (173) all_85_0_66 = all_67_0_41 % 4.62/1.86 | % 4.62/1.86 | Instantiating formula (8) with all_0_1_1, all_83_0_63, all_25_1_14 and discharging atoms h(all_0_1_1) = all_83_0_63, h(all_0_1_1) = all_25_1_14, yields: % 4.62/1.86 | (174) all_83_0_63 = all_25_1_14 % 4.62/1.86 | % 4.62/1.86 | Instantiating formula (8) with all_0_1_1, all_73_0_48, all_83_0_63 and discharging atoms h(all_0_1_1) = all_83_0_63, h(all_0_1_1) = all_73_0_48, yields: % 4.62/1.86 | (175) all_83_0_63 = all_73_0_48 % 4.62/1.86 | % 4.62/1.86 | Instantiating formula (8) with all_0_1_1, all_57_0_35, all_83_0_63 and discharging atoms h(all_0_1_1) = all_83_0_63, h(all_0_1_1) = all_57_0_35, yields: % 4.62/1.86 | (176) all_83_0_63 = all_57_0_35 % 4.62/1.86 | % 4.62/1.86 | Instantiating formula (8) with all_0_1_1, all_46_0_24, all_57_0_35 and discharging atoms h(all_0_1_1) = all_57_0_35, h(all_0_1_1) = all_46_0_24, yields: % 4.62/1.86 | (177) all_57_0_35 = all_46_0_24 % 4.62/1.86 | % 4.62/1.86 | Instantiating formula (8) with all_0_1_1, all_46_0_24, all_52_0_33 and discharging atoms h(all_0_1_1) = all_52_0_33, h(all_0_1_1) = all_46_0_24, yields: % 4.62/1.86 | (178) all_52_0_33 = all_46_0_24 % 4.62/1.86 | % 4.62/1.86 | Instantiating formula (8) with all_0_1_1, all_44_0_23, all_52_0_33 and discharging atoms h(all_0_1_1) = all_52_0_33, h(all_0_1_1) = all_44_0_23, yields: % 4.62/1.86 | (179) all_52_0_33 = all_44_0_23 % 4.62/1.86 | % 4.62/1.86 | Instantiating formula (15) with all_11_0_5, all_9_0_4, all_77_2_56, all_25_1_14 and discharging atoms op2(all_11_0_5, all_9_0_4) = all_77_2_56, op2(all_11_0_5, all_9_0_4) = all_25_1_14, yields: % 4.62/1.86 | (180) all_77_2_56 = all_25_1_14 % 4.62/1.86 | % 4.62/1.86 | Instantiating formula (15) with all_11_0_5, all_9_0_4, all_27_1_17, all_77_2_56 and discharging atoms op2(all_11_0_5, all_9_0_4) = all_77_2_56, op2(all_11_0_5, all_9_0_4) = all_27_1_17, yields: % 4.62/1.87 | (181) all_77_2_56 = all_27_1_17 % 4.62/1.87 | % 4.62/1.87 | Instantiating formula (15) with all_9_0_4, all_11_0_5, all_91_2_77, all_27_1_17 and discharging atoms op2(all_9_0_4, all_11_0_5) = all_91_2_77, op2(all_9_0_4, all_11_0_5) = all_27_1_17, yields: % 4.62/1.87 | (182) all_91_2_77 = all_27_1_17 % 4.62/1.87 | % 4.62/1.87 | Combining equations (172,173) yields a new equation: % 4.62/1.87 | (183) all_75_0_51 = all_67_0_41 % 4.62/1.87 | % 4.62/1.87 | Simplifying 183 yields: % 4.62/1.87 | (184) all_75_0_51 = all_67_0_41 % 4.62/1.87 | % 4.62/1.87 | Combining equations (174,175) yields a new equation: % 4.62/1.87 | (185) all_73_0_48 = all_25_1_14 % 4.62/1.87 | % 4.62/1.87 | Combining equations (176,175) yields a new equation: % 4.62/1.87 | (186) all_73_0_48 = all_57_0_35 % 4.62/1.87 | % 4.62/1.87 | Combining equations (181,180) yields a new equation: % 4.62/1.87 | (187) all_27_1_17 = all_25_1_14 % 4.62/1.87 | % 4.62/1.87 | Simplifying 187 yields: % 4.62/1.87 | (188) all_27_1_17 = all_25_1_14 % 4.62/1.87 | % 4.62/1.87 | Combining equations (171,184) yields a new equation: % 4.62/1.87 | (189) all_67_0_41 = all_27_1_17 % 4.62/1.87 | % 4.62/1.87 | Combining equations (186,185) yields a new equation: % 4.62/1.87 | (190) all_57_0_35 = all_25_1_14 % 4.62/1.87 | % 4.62/1.87 | Simplifying 190 yields: % 4.62/1.87 | (191) all_57_0_35 = all_25_1_14 % 4.62/1.87 | % 4.62/1.87 | Combining equations (177,191) yields a new equation: % 4.62/1.87 | (192) all_46_0_24 = all_25_1_14 % 4.62/1.87 | % 4.62/1.87 | Simplifying 192 yields: % 4.62/1.87 | (193) all_46_0_24 = all_25_1_14 % 4.62/1.87 | % 4.62/1.87 | Combining equations (178,179) yields a new equation: % 4.62/1.87 | (194) all_46_0_24 = all_44_0_23 % 4.62/1.87 | % 4.62/1.87 | Simplifying 194 yields: % 4.62/1.87 | (195) all_46_0_24 = all_44_0_23 % 4.62/1.87 | % 4.62/1.87 | Combining equations (193,195) yields a new equation: % 4.62/1.87 | (196) all_44_0_23 = all_25_1_14 % 4.62/1.87 | % 4.62/1.87 | Combining equations (188,189) yields a new equation: % 4.62/1.87 | (197) all_67_0_41 = all_25_1_14 % 4.62/1.87 | % 4.62/1.87 | Combining equations (188,182) yields a new equation: % 4.62/1.87 | (198) all_91_2_77 = all_25_1_14 % 4.62/1.87 | % 4.62/1.87 | From (198) and (167) follows: % 4.62/1.87 | (199) j(all_25_1_14) = all_91_1_76 % 4.62/1.87 | % 4.62/1.87 | From (180) and (152) follows: % 4.62/1.87 | (200) j(all_25_1_14) = all_77_1_55 % 4.62/1.87 | % 4.62/1.87 | From (197) and (139) follows: % 4.62/1.87 | (201) j(all_25_1_14) = all_0_0_0 % 4.62/1.87 | % 4.62/1.87 | From (196) and (110) follows: % 4.62/1.87 | (202) j(all_25_1_14) = all_0_1_1 % 4.62/1.87 | % 4.62/1.87 | Instantiating formula (3) with all_25_1_14, all_77_1_55, all_91_1_76 and discharging atoms j(all_25_1_14) = all_91_1_76, j(all_25_1_14) = all_77_1_55, yields: % 4.62/1.87 | (203) all_91_1_76 = all_77_1_55 % 4.62/1.87 | % 4.62/1.87 | Instantiating formula (3) with all_25_1_14, all_0_0_0, all_77_1_55 and discharging atoms j(all_25_1_14) = all_77_1_55, j(all_25_1_14) = all_0_0_0, yields: % 4.62/1.87 | (204) all_77_1_55 = all_0_0_0 % 4.62/1.87 | % 4.62/1.87 | Instantiating formula (3) with all_25_1_14, all_0_1_1, all_91_1_76 and discharging atoms j(all_25_1_14) = all_91_1_76, j(all_25_1_14) = all_0_1_1, yields: % 4.62/1.87 | (205) all_91_1_76 = all_0_1_1 % 4.62/1.87 | % 4.62/1.87 | Combining equations (203,205) yields a new equation: % 4.62/1.87 | (206) all_77_1_55 = all_0_1_1 % 4.62/1.87 | % 4.62/1.87 | Simplifying 206 yields: % 4.62/1.87 | (207) all_77_1_55 = all_0_1_1 % 4.62/1.87 | % 4.62/1.87 | Combining equations (204,207) yields a new equation: % 4.62/1.87 | (208) all_0_0_0 = all_0_1_1 % 4.62/1.87 | % 4.62/1.87 | Simplifying 208 yields: % 4.62/1.87 | (209) all_0_0_0 = all_0_1_1 % 4.62/1.87 | % 4.62/1.87 | Equations (209) can reduce 20 to: % 4.62/1.87 | (210) $false % 4.62/1.87 | % 4.62/1.87 |-The branch is then unsatisfiable % 4.62/1.87 % SZS output end Proof for theBenchmark % 4.62/1.87 % 4.62/1.87 1293ms %------------------------------------------------------------------------------