%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : ALG210+2 : TPTP v8.1.0. Released v3.1.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:37:32 EDT 2022 % Result : Theorem 9.73s 3.14s % Output : Proof 33.90s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : ALG210+2 : TPTP v8.1.0. Released v3.1.0. % 0.06/0.12 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.33 % Computer : n029.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Wed Jun 8 22:38:51 EDT 2022 % 0.13/0.34 % CPUTime : % 0.48/0.58 ____ _ % 0.48/0.58 ___ / __ \_____(_)___ ________ __________ % 0.48/0.58 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.48/0.58 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.48/0.58 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.48/0.58 % 0.48/0.58 A Theorem Prover for First-Order Logic % 0.48/0.58 (ePrincess v.1.0) % 0.48/0.58 % 0.48/0.58 (c) Philipp Rümmer, 2009-2015 % 0.48/0.58 (c) Peter Backeman, 2014-2015 % 0.48/0.58 (contributions by Angelo Brillout, Peter Baumgartner) % 0.48/0.58 Free software under GNU Lesser General Public License (LGPL). % 0.48/0.58 Bug reports to peter@backeman.se % 0.48/0.58 % 0.48/0.58 For more information, visit http://user.uu.se/~petba168/breu/ % 0.48/0.58 % 0.48/0.58 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.72/0.64 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.19/0.90 Prover 0: Preprocessing ... % 1.55/1.04 Prover 0: Constructing countermodel ... % 2.75/1.39 Prover 0: gave up % 2.75/1.39 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 2.75/1.40 Prover 1: Preprocessing ... % 2.96/1.44 Prover 1: Constructing countermodel ... % 9.73/3.14 Prover 1: proved (1748ms) % 9.73/3.14 % 9.73/3.14 No countermodel exists, formula is valid % 9.73/3.14 % SZS status Theorem for theBenchmark % 9.73/3.14 % 9.73/3.14 Generating proof ... found it (size 418) % 33.37/10.21 % 33.37/10.21 % SZS output start Proof for theBenchmark % 33.37/10.21 Assumed formulas after preprocessing and simplification: % 33.37/10.21 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ( ~ (v3 = 0) & element(v2) = v3 & element(v1) = 0 & element(v0) = 0 & times(v0, v1) = v2 & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ! [v8] : ( ~ (times(v7, v6) = v8) | ~ (times(v4, v5) = v7) | ? [v9] : (times(v6, v4) = v9 & times(v5, v9) = v8)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (times(v7, v6) = v5) | ~ (times(v7, v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : (v5 = v4 | ~ (element(v6) = v5) | ~ (element(v6) = v4)) & ! [v4] : ! [v5] : (v5 = 0 | ~ (element(v4) = v5) | ? [v6] : (times(v4, v4) = v6 & ~ (times(v4, v6) = v4))) & ! [v4] : ( ~ (element(v4) = 0) | ? [v5] : (times(v4, v5) = v4 & times(v4, v4) = v5))) % 33.47/10.23 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3 yields: % 33.47/10.23 | (1) ~ (all_0_0_0 = 0) & element(all_0_1_1) = all_0_0_0 & element(all_0_2_2) = 0 & element(all_0_3_3) = 0 & times(all_0_3_3, all_0_2_2) = all_0_1_1 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (times(v3, v2) = v4) | ~ (times(v0, v1) = v3) | ? [v5] : (times(v2, v0) = v5 & times(v1, v5) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (times(v3, v2) = v1) | ~ (times(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (element(v2) = v1) | ~ (element(v2) = v0)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (element(v0) = v1) | ? [v2] : (times(v0, v0) = v2 & ~ (times(v0, v2) = v0))) & ! [v0] : ( ~ (element(v0) = 0) | ? [v1] : (times(v0, v1) = v0 & times(v0, v0) = v1)) % 33.47/10.24 | % 33.47/10.24 | Applying alpha-rule on (1) yields: % 33.47/10.24 | (2) times(all_0_3_3, all_0_2_2) = all_0_1_1 % 33.47/10.24 | (3) ! [v0] : ! [v1] : (v1 = 0 | ~ (element(v0) = v1) | ? [v2] : (times(v0, v0) = v2 & ~ (times(v0, v2) = v0))) % 33.47/10.24 | (4) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (times(v3, v2) = v4) | ~ (times(v0, v1) = v3) | ? [v5] : (times(v2, v0) = v5 & times(v1, v5) = v4)) % 33.47/10.24 | (5) ! [v0] : ( ~ (element(v0) = 0) | ? [v1] : (times(v0, v1) = v0 & times(v0, v0) = v1)) % 33.47/10.24 | (6) element(all_0_2_2) = 0 % 33.47/10.24 | (7) element(all_0_1_1) = all_0_0_0 % 33.47/10.24 | (8) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (times(v3, v2) = v1) | ~ (times(v3, v2) = v0)) % 33.47/10.24 | (9) element(all_0_3_3) = 0 % 33.47/10.24 | (10) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (element(v2) = v1) | ~ (element(v2) = v0)) % 33.47/10.24 | (11) ~ (all_0_0_0 = 0) % 33.47/10.24 | % 33.47/10.24 | Instantiating formula (3) with all_0_0_0, all_0_1_1 and discharging atoms element(all_0_1_1) = all_0_0_0, yields: % 33.47/10.24 | (12) all_0_0_0 = 0 | ? [v0] : (times(all_0_1_1, all_0_1_1) = v0 & ~ (times(all_0_1_1, v0) = all_0_1_1)) % 33.47/10.24 | % 33.47/10.24 | Instantiating formula (5) with all_0_2_2 and discharging atoms element(all_0_2_2) = 0, yields: % 33.47/10.24 | (13) ? [v0] : (times(all_0_2_2, v0) = all_0_2_2 & times(all_0_2_2, all_0_2_2) = v0) % 33.47/10.24 | % 33.47/10.24 | Instantiating formula (5) with all_0_3_3 and discharging atoms element(all_0_3_3) = 0, yields: % 33.47/10.24 | (14) ? [v0] : (times(all_0_3_3, v0) = all_0_3_3 & times(all_0_3_3, all_0_3_3) = v0) % 33.47/10.24 | % 33.47/10.24 | Instantiating (14) with all_8_0_4 yields: % 33.47/10.24 | (15) times(all_0_3_3, all_8_0_4) = all_0_3_3 & times(all_0_3_3, all_0_3_3) = all_8_0_4 % 33.47/10.24 | % 33.47/10.24 | Applying alpha-rule on (15) yields: % 33.47/10.24 | (16) times(all_0_3_3, all_8_0_4) = all_0_3_3 % 33.47/10.24 | (17) times(all_0_3_3, all_0_3_3) = all_8_0_4 % 33.47/10.24 | % 33.47/10.25 | Instantiating (13) with all_10_0_5 yields: % 33.47/10.25 | (18) times(all_0_2_2, all_10_0_5) = all_0_2_2 & times(all_0_2_2, all_0_2_2) = all_10_0_5 % 33.47/10.25 | % 33.47/10.25 | Applying alpha-rule on (18) yields: % 33.47/10.25 | (19) times(all_0_2_2, all_10_0_5) = all_0_2_2 % 33.47/10.25 | (20) times(all_0_2_2, all_0_2_2) = all_10_0_5 % 33.47/10.25 | % 33.47/10.25 +-Applying beta-rule and splitting (12), into two cases. % 33.47/10.25 |-Branch one: % 33.47/10.25 | (21) all_0_0_0 = 0 % 33.47/10.25 | % 33.47/10.25 | Equations (21) can reduce 11 to: % 33.47/10.25 | (22) $false % 33.47/10.25 | % 33.47/10.25 |-The branch is then unsatisfiable % 33.47/10.25 |-Branch two: % 33.47/10.25 | (11) ~ (all_0_0_0 = 0) % 33.47/10.25 | (24) ? [v0] : (times(all_0_1_1, all_0_1_1) = v0 & ~ (times(all_0_1_1, v0) = all_0_1_1)) % 33.47/10.25 | % 33.47/10.25 | Instantiating (24) with all_16_0_6 yields: % 33.47/10.25 | (25) times(all_0_1_1, all_0_1_1) = all_16_0_6 & ~ (times(all_0_1_1, all_16_0_6) = all_0_1_1) % 33.47/10.25 | % 33.47/10.25 | Applying alpha-rule on (25) yields: % 33.47/10.25 | (26) times(all_0_1_1, all_0_1_1) = all_16_0_6 % 33.47/10.25 | (27) ~ (times(all_0_1_1, all_16_0_6) = all_0_1_1) % 33.47/10.25 | % 33.47/10.25 | Instantiating formula (4) with all_16_0_6, all_0_1_1, all_0_1_1, all_0_2_2, all_0_3_3 and discharging atoms times(all_0_1_1, all_0_1_1) = all_16_0_6, times(all_0_3_3, all_0_2_2) = all_0_1_1, yields: % 33.47/10.25 | (28) ? [v0] : (times(all_0_1_1, all_0_3_3) = v0 & times(all_0_2_2, v0) = all_16_0_6) % 33.47/10.25 | % 33.47/10.25 | Instantiating formula (4) with all_0_2_2, all_0_2_2, all_10_0_5, all_10_0_5, all_0_2_2 and discharging atoms times(all_0_2_2, all_10_0_5) = all_0_2_2, yields: % 33.47/10.25 | (29) ? [v0] : (times(all_10_0_5, v0) = all_0_2_2 & times(all_10_0_5, all_0_2_2) = v0) % 33.47/10.25 | % 33.47/10.25 | Instantiating formula (4) with all_10_0_5, all_0_2_2, all_0_2_2, all_10_0_5, all_0_2_2 and discharging atoms times(all_0_2_2, all_10_0_5) = all_0_2_2, times(all_0_2_2, all_0_2_2) = all_10_0_5, yields: % 33.47/10.25 | (30) ? [v0] : (times(all_10_0_5, v0) = all_10_0_5 & times(all_0_2_2, all_0_2_2) = v0) % 33.47/10.25 | % 33.47/10.25 | Instantiating formula (4) with all_0_1_1, all_0_3_3, all_0_2_2, all_8_0_4, all_0_3_3 and discharging atoms times(all_0_3_3, all_8_0_4) = all_0_3_3, times(all_0_3_3, all_0_2_2) = all_0_1_1, yields: % 33.47/10.25 | (31) ? [v0] : (times(all_8_0_4, v0) = all_0_1_1 & times(all_0_2_2, all_0_3_3) = v0) % 33.47/10.25 | % 33.47/10.25 | Instantiating formula (4) with all_0_3_3, all_0_3_3, all_8_0_4, all_8_0_4, all_0_3_3 and discharging atoms times(all_0_3_3, all_8_0_4) = all_0_3_3, yields: % 33.47/10.25 | (32) ? [v0] : (times(all_8_0_4, v0) = all_0_3_3 & times(all_8_0_4, all_0_3_3) = v0) % 33.47/10.25 | % 33.47/10.25 | Instantiating formula (4) with all_8_0_4, all_0_3_3, all_0_3_3, all_8_0_4, all_0_3_3 and discharging atoms times(all_0_3_3, all_8_0_4) = all_0_3_3, times(all_0_3_3, all_0_3_3) = all_8_0_4, yields: % 33.47/10.25 | (33) ? [v0] : (times(all_8_0_4, v0) = all_8_0_4 & times(all_0_3_3, all_0_3_3) = v0) % 33.47/10.25 | % 33.47/10.25 | Instantiating (33) with all_23_0_7 yields: % 33.47/10.25 | (34) times(all_8_0_4, all_23_0_7) = all_8_0_4 & times(all_0_3_3, all_0_3_3) = all_23_0_7 % 33.47/10.25 | % 33.47/10.25 | Applying alpha-rule on (34) yields: % 33.47/10.25 | (35) times(all_8_0_4, all_23_0_7) = all_8_0_4 % 33.47/10.25 | (36) times(all_0_3_3, all_0_3_3) = all_23_0_7 % 33.47/10.25 | % 33.47/10.25 | Instantiating (32) with all_25_0_8 yields: % 33.47/10.25 | (37) times(all_8_0_4, all_25_0_8) = all_0_3_3 & times(all_8_0_4, all_0_3_3) = all_25_0_8 % 33.47/10.26 | % 33.47/10.26 | Applying alpha-rule on (37) yields: % 33.47/10.26 | (38) times(all_8_0_4, all_25_0_8) = all_0_3_3 % 33.47/10.26 | (39) times(all_8_0_4, all_0_3_3) = all_25_0_8 % 33.47/10.26 | % 33.47/10.26 | Instantiating (29) with all_27_0_9 yields: % 33.47/10.26 | (40) times(all_10_0_5, all_27_0_9) = all_0_2_2 & times(all_10_0_5, all_0_2_2) = all_27_0_9 % 33.47/10.26 | % 33.47/10.26 | Applying alpha-rule on (40) yields: % 33.47/10.26 | (41) times(all_10_0_5, all_27_0_9) = all_0_2_2 % 33.47/10.26 | (42) times(all_10_0_5, all_0_2_2) = all_27_0_9 % 33.47/10.26 | % 33.47/10.26 | Instantiating (28) with all_29_0_10 yields: % 33.47/10.26 | (43) times(all_0_1_1, all_0_3_3) = all_29_0_10 & times(all_0_2_2, all_29_0_10) = all_16_0_6 % 33.47/10.26 | % 33.47/10.26 | Applying alpha-rule on (43) yields: % 33.47/10.26 | (44) times(all_0_1_1, all_0_3_3) = all_29_0_10 % 33.47/10.26 | (45) times(all_0_2_2, all_29_0_10) = all_16_0_6 % 33.47/10.26 | % 33.47/10.26 | Instantiating (31) with all_31_0_11 yields: % 33.47/10.26 | (46) times(all_8_0_4, all_31_0_11) = all_0_1_1 & times(all_0_2_2, all_0_3_3) = all_31_0_11 % 33.47/10.26 | % 33.47/10.26 | Applying alpha-rule on (46) yields: % 33.47/10.26 | (47) times(all_8_0_4, all_31_0_11) = all_0_1_1 % 33.47/10.26 | (48) times(all_0_2_2, all_0_3_3) = all_31_0_11 % 33.47/10.26 | % 33.47/10.26 | Instantiating (30) with all_33_0_12 yields: % 33.47/10.26 | (49) times(all_10_0_5, all_33_0_12) = all_10_0_5 & times(all_0_2_2, all_0_2_2) = all_33_0_12 % 33.47/10.26 | % 33.47/10.26 | Applying alpha-rule on (49) yields: % 33.47/10.26 | (50) times(all_10_0_5, all_33_0_12) = all_10_0_5 % 33.47/10.26 | (51) times(all_0_2_2, all_0_2_2) = all_33_0_12 % 33.47/10.26 | % 33.47/10.26 | Instantiating formula (8) with all_0_2_2, all_0_2_2, all_33_0_12, all_10_0_5 and discharging atoms times(all_0_2_2, all_0_2_2) = all_33_0_12, times(all_0_2_2, all_0_2_2) = all_10_0_5, yields: % 33.47/10.26 | (52) all_33_0_12 = all_10_0_5 % 33.47/10.26 | % 33.47/10.26 | Instantiating formula (8) with all_0_3_3, all_0_3_3, all_23_0_7, all_8_0_4 and discharging atoms times(all_0_3_3, all_0_3_3) = all_23_0_7, times(all_0_3_3, all_0_3_3) = all_8_0_4, yields: % 33.47/10.26 | (53) all_23_0_7 = all_8_0_4 % 33.47/10.26 | % 33.47/10.26 | From (52) and (50) follows: % 33.47/10.26 | (54) times(all_10_0_5, all_10_0_5) = all_10_0_5 % 33.47/10.26 | % 33.47/10.26 | From (53) and (35) follows: % 33.47/10.26 | (55) times(all_8_0_4, all_8_0_4) = all_8_0_4 % 33.47/10.26 | % 33.47/10.26 | From (52) and (51) follows: % 33.47/10.26 | (20) times(all_0_2_2, all_0_2_2) = all_10_0_5 % 33.47/10.26 | % 33.47/10.26 | From (53) and (36) follows: % 33.47/10.26 | (17) times(all_0_3_3, all_0_3_3) = all_8_0_4 % 33.47/10.26 | % 33.47/10.26 | Instantiating formula (4) with all_0_2_2, all_10_0_5, all_27_0_9, all_0_2_2, all_0_2_2 and discharging atoms times(all_10_0_5, all_27_0_9) = all_0_2_2, times(all_0_2_2, all_0_2_2) = all_10_0_5, yields: % 33.47/10.26 | (58) ? [v0] : (times(all_27_0_9, all_0_2_2) = v0 & times(all_0_2_2, v0) = all_0_2_2) % 33.47/10.26 | % 33.47/10.26 | Instantiating formula (4) with all_10_0_5, all_0_2_2, all_0_2_2, all_27_0_9, all_10_0_5 and discharging atoms times(all_10_0_5, all_27_0_9) = all_0_2_2, times(all_0_2_2, all_0_2_2) = all_10_0_5, yields: % 33.47/10.26 | (59) ? [v0] : (times(all_27_0_9, v0) = all_10_0_5 & times(all_0_2_2, all_10_0_5) = v0) % 33.47/10.26 | % 33.47/10.26 | Instantiating formula (4) with all_0_2_2, all_10_0_5, all_27_0_9, all_10_0_5, all_10_0_5 and discharging atoms times(all_10_0_5, all_27_0_9) = all_0_2_2, times(all_10_0_5, all_10_0_5) = all_10_0_5, yields: % 33.47/10.26 | (60) ? [v0] : (times(all_27_0_9, all_10_0_5) = v0 & times(all_10_0_5, v0) = all_0_2_2) % 33.47/10.26 | % 33.47/10.26 | Instantiating formula (4) with all_27_0_9, all_10_0_5, all_0_2_2, all_0_2_2, all_0_2_2 and discharging atoms times(all_10_0_5, all_0_2_2) = all_27_0_9, times(all_0_2_2, all_0_2_2) = all_10_0_5, yields: % 33.47/10.26 | (61) ? [v0] : (times(all_0_2_2, v0) = all_27_0_9 & times(all_0_2_2, all_0_2_2) = v0) % 33.47/10.26 | % 33.47/10.26 | Instantiating formula (4) with all_16_0_6, all_0_1_1, all_0_1_1, all_31_0_11, all_8_0_4 and discharging atoms times(all_8_0_4, all_31_0_11) = all_0_1_1, times(all_0_1_1, all_0_1_1) = all_16_0_6, yields: % 33.47/10.26 | (62) ? [v0] : (times(all_31_0_11, v0) = all_16_0_6 & times(all_0_1_1, all_8_0_4) = v0) % 33.47/10.26 | % 33.47/10.26 | Instantiating formula (4) with all_0_1_1, all_8_0_4, all_31_0_11, all_0_3_3, all_0_3_3 and discharging atoms times(all_8_0_4, all_31_0_11) = all_0_1_1, times(all_0_3_3, all_0_3_3) = all_8_0_4, yields: % 33.47/10.26 | (63) ? [v0] : (times(all_31_0_11, all_0_3_3) = v0 & times(all_0_3_3, v0) = all_0_1_1) % 33.47/10.27 | % 33.47/10.27 | Instantiating formula (4) with all_0_1_1, all_8_0_4, all_31_0_11, all_8_0_4, all_8_0_4 and discharging atoms times(all_8_0_4, all_31_0_11) = all_0_1_1, times(all_8_0_4, all_8_0_4) = all_8_0_4, yields: % 33.47/10.27 | (64) ? [v0] : (times(all_31_0_11, all_8_0_4) = v0 & times(all_8_0_4, v0) = all_0_1_1) % 33.47/10.27 | % 33.47/10.27 | Instantiating formula (4) with all_0_3_3, all_0_3_3, all_8_0_4, all_25_0_8, all_8_0_4 and discharging atoms times(all_8_0_4, all_25_0_8) = all_0_3_3, times(all_0_3_3, all_8_0_4) = all_0_3_3, yields: % 33.47/10.27 | (65) ? [v0] : (times(all_25_0_8, v0) = all_0_3_3 & times(all_8_0_4, all_8_0_4) = v0) % 33.47/10.27 | % 33.47/10.27 | Instantiating formula (4) with all_0_1_1, all_0_3_3, all_0_2_2, all_25_0_8, all_8_0_4 and discharging atoms times(all_8_0_4, all_25_0_8) = all_0_3_3, times(all_0_3_3, all_0_2_2) = all_0_1_1, yields: % 33.47/10.27 | (66) ? [v0] : (times(all_25_0_8, v0) = all_0_1_1 & times(all_0_2_2, all_8_0_4) = v0) % 33.47/10.27 | % 33.47/10.27 | Instantiating formula (4) with all_0_3_3, all_8_0_4, all_25_0_8, all_0_3_3, all_0_3_3 and discharging atoms times(all_8_0_4, all_25_0_8) = all_0_3_3, times(all_0_3_3, all_0_3_3) = all_8_0_4, yields: % 33.47/10.27 | (67) ? [v0] : (times(all_25_0_8, all_0_3_3) = v0 & times(all_0_3_3, v0) = all_0_3_3) % 33.47/10.27 | % 33.47/10.27 | Instantiating formula (4) with all_8_0_4, all_0_3_3, all_0_3_3, all_25_0_8, all_8_0_4 and discharging atoms times(all_8_0_4, all_25_0_8) = all_0_3_3, times(all_0_3_3, all_0_3_3) = all_8_0_4, yields: % 33.47/10.27 | (68) ? [v0] : (times(all_25_0_8, v0) = all_8_0_4 & times(all_0_3_3, all_8_0_4) = v0) % 33.47/10.27 | % 33.47/10.27 | Instantiating formula (4) with all_0_3_3, all_8_0_4, all_25_0_8, all_8_0_4, all_8_0_4 and discharging atoms times(all_8_0_4, all_25_0_8) = all_0_3_3, times(all_8_0_4, all_8_0_4) = all_8_0_4, yields: % 33.47/10.27 | (69) ? [v0] : (times(all_25_0_8, all_8_0_4) = v0 & times(all_8_0_4, v0) = all_0_3_3) % 33.47/10.27 | % 33.47/10.27 | Instantiating formula (4) with all_25_0_8, all_8_0_4, all_0_3_3, all_0_3_3, all_0_3_3 and discharging atoms times(all_8_0_4, all_0_3_3) = all_25_0_8, times(all_0_3_3, all_0_3_3) = all_8_0_4, yields: % 33.47/10.27 | (70) ? [v0] : (times(all_0_3_3, v0) = all_25_0_8 & times(all_0_3_3, all_0_3_3) = v0) % 33.47/10.27 | % 33.47/10.27 | Instantiating formula (4) with all_29_0_10, all_0_1_1, all_0_3_3, all_0_2_2, all_0_3_3 and discharging atoms times(all_0_1_1, all_0_3_3) = all_29_0_10, times(all_0_3_3, all_0_2_2) = all_0_1_1, yields: % 33.47/10.27 | (71) ? [v0] : (times(all_0_2_2, v0) = all_29_0_10 & times(all_0_3_3, all_0_3_3) = v0) % 33.47/10.27 | % 33.47/10.27 | Instantiating formula (4) with all_29_0_10, all_0_1_1, all_0_3_3, all_31_0_11, all_8_0_4 and discharging atoms times(all_8_0_4, all_31_0_11) = all_0_1_1, times(all_0_1_1, all_0_3_3) = all_29_0_10, yields: % 33.47/10.27 | (72) ? [v0] : (times(all_31_0_11, v0) = all_29_0_10 & times(all_0_3_3, all_8_0_4) = v0) % 33.47/10.27 | % 33.47/10.27 | Instantiating formula (4) with all_16_0_6, all_0_2_2, all_29_0_10, all_10_0_5, all_0_2_2 and discharging atoms times(all_0_2_2, all_29_0_10) = all_16_0_6, times(all_0_2_2, all_10_0_5) = all_0_2_2, yields: % 33.47/10.27 | (73) ? [v0] : (times(all_29_0_10, all_0_2_2) = v0 & times(all_10_0_5, v0) = all_16_0_6) % 33.47/10.27 | % 33.47/10.27 | Instantiating formula (4) with all_16_0_6, all_0_2_2, all_29_0_10, all_27_0_9, all_10_0_5 and discharging atoms times(all_10_0_5, all_27_0_9) = all_0_2_2, times(all_0_2_2, all_29_0_10) = all_16_0_6, yields: % 33.47/10.27 | (74) ? [v0] : (times(all_29_0_10, all_10_0_5) = v0 & times(all_27_0_9, v0) = all_16_0_6) % 33.47/10.27 | % 33.47/10.27 | Instantiating formula (4) with all_31_0_11, all_0_2_2, all_0_3_3, all_10_0_5, all_0_2_2 and discharging atoms times(all_0_2_2, all_10_0_5) = all_0_2_2, times(all_0_2_2, all_0_3_3) = all_31_0_11, yields: % 33.47/10.27 | (75) ? [v0] : (times(all_10_0_5, v0) = all_31_0_11 & times(all_0_3_3, all_0_2_2) = v0) % 33.47/10.27 | % 33.47/10.27 | Instantiating formula (4) with all_31_0_11, all_0_2_2, all_0_3_3, all_27_0_9, all_10_0_5 and discharging atoms times(all_10_0_5, all_27_0_9) = all_0_2_2, times(all_0_2_2, all_0_3_3) = all_31_0_11, yields: % 33.47/10.27 | (76) ? [v0] : (times(all_27_0_9, v0) = all_31_0_11 & times(all_0_3_3, all_10_0_5) = v0) % 33.47/10.27 | % 33.47/10.27 | Instantiating (76) with all_44_0_13 yields: % 33.47/10.27 | (77) times(all_27_0_9, all_44_0_13) = all_31_0_11 & times(all_0_3_3, all_10_0_5) = all_44_0_13 % 33.47/10.27 | % 33.47/10.27 | Applying alpha-rule on (77) yields: % 33.47/10.27 | (78) times(all_27_0_9, all_44_0_13) = all_31_0_11 % 33.47/10.27 | (79) times(all_0_3_3, all_10_0_5) = all_44_0_13 % 33.47/10.27 | % 33.47/10.27 | Instantiating (75) with all_46_0_14 yields: % 33.47/10.27 | (80) times(all_10_0_5, all_46_0_14) = all_31_0_11 & times(all_0_3_3, all_0_2_2) = all_46_0_14 % 33.47/10.27 | % 33.47/10.27 | Applying alpha-rule on (80) yields: % 33.47/10.27 | (81) times(all_10_0_5, all_46_0_14) = all_31_0_11 % 33.47/10.28 | (82) times(all_0_3_3, all_0_2_2) = all_46_0_14 % 33.47/10.28 | % 33.47/10.28 | Instantiating (66) with all_48_0_15 yields: % 33.47/10.28 | (83) times(all_25_0_8, all_48_0_15) = all_0_1_1 & times(all_0_2_2, all_8_0_4) = all_48_0_15 % 33.47/10.28 | % 33.47/10.28 | Applying alpha-rule on (83) yields: % 33.47/10.28 | (84) times(all_25_0_8, all_48_0_15) = all_0_1_1 % 33.47/10.28 | (85) times(all_0_2_2, all_8_0_4) = all_48_0_15 % 33.47/10.28 | % 33.47/10.28 | Instantiating (63) with all_50_0_16 yields: % 33.47/10.28 | (86) times(all_31_0_11, all_0_3_3) = all_50_0_16 & times(all_0_3_3, all_50_0_16) = all_0_1_1 % 33.47/10.28 | % 33.47/10.28 | Applying alpha-rule on (86) yields: % 33.47/10.28 | (87) times(all_31_0_11, all_0_3_3) = all_50_0_16 % 33.47/10.28 | (88) times(all_0_3_3, all_50_0_16) = all_0_1_1 % 33.47/10.28 | % 33.47/10.28 | Instantiating (62) with all_52_0_17 yields: % 33.47/10.28 | (89) times(all_31_0_11, all_52_0_17) = all_16_0_6 & times(all_0_1_1, all_8_0_4) = all_52_0_17 % 33.47/10.28 | % 33.47/10.28 | Applying alpha-rule on (89) yields: % 33.47/10.28 | (90) times(all_31_0_11, all_52_0_17) = all_16_0_6 % 33.47/10.28 | (91) times(all_0_1_1, all_8_0_4) = all_52_0_17 % 33.47/10.28 | % 33.47/10.28 | Instantiating (65) with all_54_0_18 yields: % 33.47/10.28 | (92) times(all_25_0_8, all_54_0_18) = all_0_3_3 & times(all_8_0_4, all_8_0_4) = all_54_0_18 % 33.47/10.28 | % 33.47/10.28 | Applying alpha-rule on (92) yields: % 33.47/10.28 | (93) times(all_25_0_8, all_54_0_18) = all_0_3_3 % 33.47/10.28 | (94) times(all_8_0_4, all_8_0_4) = all_54_0_18 % 33.47/10.28 | % 33.47/10.28 | Instantiating (61) with all_56_0_19 yields: % 33.47/10.28 | (95) times(all_0_2_2, all_56_0_19) = all_27_0_9 & times(all_0_2_2, all_0_2_2) = all_56_0_19 % 33.47/10.28 | % 33.47/10.28 | Applying alpha-rule on (95) yields: % 33.47/10.28 | (96) times(all_0_2_2, all_56_0_19) = all_27_0_9 % 33.47/10.28 | (97) times(all_0_2_2, all_0_2_2) = all_56_0_19 % 33.47/10.28 | % 33.47/10.28 | Instantiating (60) with all_58_0_20 yields: % 33.47/10.28 | (98) times(all_27_0_9, all_10_0_5) = all_58_0_20 & times(all_10_0_5, all_58_0_20) = all_0_2_2 % 33.47/10.28 | % 33.47/10.28 | Applying alpha-rule on (98) yields: % 33.47/10.28 | (99) times(all_27_0_9, all_10_0_5) = all_58_0_20 % 33.47/10.28 | (100) times(all_10_0_5, all_58_0_20) = all_0_2_2 % 33.47/10.28 | % 33.47/10.28 | Instantiating (64) with all_62_0_22 yields: % 33.47/10.28 | (101) times(all_31_0_11, all_8_0_4) = all_62_0_22 & times(all_8_0_4, all_62_0_22) = all_0_1_1 % 33.47/10.28 | % 33.47/10.28 | Applying alpha-rule on (101) yields: % 33.47/10.28 | (102) times(all_31_0_11, all_8_0_4) = all_62_0_22 % 33.47/10.28 | (103) times(all_8_0_4, all_62_0_22) = all_0_1_1 % 33.47/10.28 | % 33.47/10.28 | Instantiating (74) with all_64_0_23 yields: % 33.47/10.28 | (104) times(all_29_0_10, all_10_0_5) = all_64_0_23 & times(all_27_0_9, all_64_0_23) = all_16_0_6 % 33.47/10.28 | % 33.47/10.28 | Applying alpha-rule on (104) yields: % 33.47/10.28 | (105) times(all_29_0_10, all_10_0_5) = all_64_0_23 % 33.47/10.28 | (106) times(all_27_0_9, all_64_0_23) = all_16_0_6 % 33.47/10.28 | % 33.47/10.28 | Instantiating (59) with all_68_0_25 yields: % 33.47/10.28 | (107) times(all_27_0_9, all_68_0_25) = all_10_0_5 & times(all_0_2_2, all_10_0_5) = all_68_0_25 % 33.47/10.28 | % 33.47/10.28 | Applying alpha-rule on (107) yields: % 33.47/10.28 | (108) times(all_27_0_9, all_68_0_25) = all_10_0_5 % 33.47/10.28 | (109) times(all_0_2_2, all_10_0_5) = all_68_0_25 % 33.47/10.28 | % 33.47/10.28 | Instantiating (58) with all_70_0_26 yields: % 33.47/10.28 | (110) times(all_27_0_9, all_0_2_2) = all_70_0_26 & times(all_0_2_2, all_70_0_26) = all_0_2_2 % 33.47/10.28 | % 33.47/10.28 | Applying alpha-rule on (110) yields: % 33.47/10.28 | (111) times(all_27_0_9, all_0_2_2) = all_70_0_26 % 33.47/10.28 | (112) times(all_0_2_2, all_70_0_26) = all_0_2_2 % 33.47/10.28 | % 33.47/10.28 | Instantiating (73) with all_74_0_28 yields: % 33.47/10.28 | (113) times(all_29_0_10, all_0_2_2) = all_74_0_28 & times(all_10_0_5, all_74_0_28) = all_16_0_6 % 33.47/10.28 | % 33.47/10.28 | Applying alpha-rule on (113) yields: % 33.47/10.28 | (114) times(all_29_0_10, all_0_2_2) = all_74_0_28 % 33.47/10.28 | (115) times(all_10_0_5, all_74_0_28) = all_16_0_6 % 33.47/10.28 | % 33.47/10.28 | Instantiating (72) with all_76_0_29 yields: % 33.47/10.28 | (116) times(all_31_0_11, all_76_0_29) = all_29_0_10 & times(all_0_3_3, all_8_0_4) = all_76_0_29 % 33.47/10.28 | % 33.47/10.28 | Applying alpha-rule on (116) yields: % 33.47/10.28 | (117) times(all_31_0_11, all_76_0_29) = all_29_0_10 % 33.47/10.28 | (118) times(all_0_3_3, all_8_0_4) = all_76_0_29 % 33.47/10.28 | % 33.47/10.28 | Instantiating (71) with all_78_0_30 yields: % 33.47/10.28 | (119) times(all_0_2_2, all_78_0_30) = all_29_0_10 & times(all_0_3_3, all_0_3_3) = all_78_0_30 % 33.47/10.28 | % 33.47/10.28 | Applying alpha-rule on (119) yields: % 33.47/10.28 | (120) times(all_0_2_2, all_78_0_30) = all_29_0_10 % 33.47/10.28 | (121) times(all_0_3_3, all_0_3_3) = all_78_0_30 % 33.47/10.28 | % 33.47/10.28 | Instantiating (70) with all_80_0_31 yields: % 33.47/10.28 | (122) times(all_0_3_3, all_80_0_31) = all_25_0_8 & times(all_0_3_3, all_0_3_3) = all_80_0_31 % 33.47/10.28 | % 33.47/10.28 | Applying alpha-rule on (122) yields: % 33.47/10.28 | (123) times(all_0_3_3, all_80_0_31) = all_25_0_8 % 33.47/10.28 | (124) times(all_0_3_3, all_0_3_3) = all_80_0_31 % 33.47/10.28 | % 33.47/10.28 | Instantiating (69) with all_82_0_32 yields: % 33.47/10.28 | (125) times(all_25_0_8, all_8_0_4) = all_82_0_32 & times(all_8_0_4, all_82_0_32) = all_0_3_3 % 33.47/10.28 | % 33.47/10.28 | Applying alpha-rule on (125) yields: % 33.47/10.28 | (126) times(all_25_0_8, all_8_0_4) = all_82_0_32 % 33.47/10.28 | (127) times(all_8_0_4, all_82_0_32) = all_0_3_3 % 33.47/10.28 | % 33.47/10.28 | Instantiating (68) with all_84_0_33 yields: % 33.47/10.28 | (128) times(all_25_0_8, all_84_0_33) = all_8_0_4 & times(all_0_3_3, all_8_0_4) = all_84_0_33 % 33.47/10.28 | % 33.47/10.28 | Applying alpha-rule on (128) yields: % 33.47/10.28 | (129) times(all_25_0_8, all_84_0_33) = all_8_0_4 % 33.47/10.28 | (130) times(all_0_3_3, all_8_0_4) = all_84_0_33 % 33.47/10.29 | % 33.47/10.29 | Instantiating (67) with all_86_0_34 yields: % 33.47/10.29 | (131) times(all_25_0_8, all_0_3_3) = all_86_0_34 & times(all_0_3_3, all_86_0_34) = all_0_3_3 % 33.47/10.29 | % 33.47/10.29 | Applying alpha-rule on (131) yields: % 33.47/10.29 | (132) times(all_25_0_8, all_0_3_3) = all_86_0_34 % 33.47/10.29 | (133) times(all_0_3_3, all_86_0_34) = all_0_3_3 % 33.47/10.29 | % 33.47/10.29 | Instantiating formula (8) with all_31_0_11, all_0_3_3, all_50_0_16, all_29_0_10 and discharging atoms times(all_31_0_11, all_0_3_3) = all_50_0_16, yields: % 33.47/10.29 | (134) all_50_0_16 = all_29_0_10 | ~ (times(all_31_0_11, all_0_3_3) = all_29_0_10) % 33.47/10.29 | % 33.47/10.29 | Instantiating formula (8) with all_8_0_4, all_8_0_4, all_54_0_18, all_8_0_4 and discharging atoms times(all_8_0_4, all_8_0_4) = all_54_0_18, times(all_8_0_4, all_8_0_4) = all_8_0_4, yields: % 33.47/10.29 | (135) all_54_0_18 = all_8_0_4 % 33.47/10.29 | % 33.47/10.29 | Instantiating formula (8) with all_0_2_2, all_10_0_5, all_27_0_9, all_0_2_2 and discharging atoms times(all_0_2_2, all_10_0_5) = all_0_2_2, yields: % 33.47/10.29 | (136) all_27_0_9 = all_0_2_2 | ~ (times(all_0_2_2, all_10_0_5) = all_27_0_9) % 33.47/10.29 | % 33.47/10.29 | Instantiating formula (8) with all_0_2_2, all_10_0_5, all_68_0_25, all_0_2_2 and discharging atoms times(all_0_2_2, all_10_0_5) = all_68_0_25, times(all_0_2_2, all_10_0_5) = all_0_2_2, yields: % 33.47/10.29 | (137) all_68_0_25 = all_0_2_2 % 33.47/10.29 | % 33.47/10.29 | Instantiating formula (8) with all_0_2_2, all_10_0_5, all_68_0_25, all_58_0_20 and discharging atoms times(all_0_2_2, all_10_0_5) = all_68_0_25, yields: % 33.47/10.29 | (138) all_68_0_25 = all_58_0_20 | ~ (times(all_0_2_2, all_10_0_5) = all_58_0_20) % 33.47/10.29 | % 33.47/10.29 | Instantiating formula (8) with all_0_2_2, all_8_0_4, all_48_0_15, all_29_0_10 and discharging atoms times(all_0_2_2, all_8_0_4) = all_48_0_15, yields: % 33.47/10.29 | (139) all_48_0_15 = all_29_0_10 | ~ (times(all_0_2_2, all_8_0_4) = all_29_0_10) % 33.47/10.29 | % 33.47/10.29 | Instantiating formula (8) with all_0_2_2, all_0_2_2, all_56_0_19, all_10_0_5 and discharging atoms times(all_0_2_2, all_0_2_2) = all_56_0_19, times(all_0_2_2, all_0_2_2) = all_10_0_5, yields: % 33.47/10.29 | (140) all_56_0_19 = all_10_0_5 % 33.47/10.29 | % 33.47/10.29 | Instantiating formula (8) with all_0_2_2, all_0_2_2, all_56_0_19, all_70_0_26 and discharging atoms times(all_0_2_2, all_0_2_2) = all_56_0_19, yields: % 33.47/10.29 | (141) all_70_0_26 = all_56_0_19 | ~ (times(all_0_2_2, all_0_2_2) = all_70_0_26) % 33.47/10.29 | % 33.47/10.29 | Instantiating formula (8) with all_0_3_3, all_80_0_31, all_25_0_8, all_0_3_3 and discharging atoms times(all_0_3_3, all_80_0_31) = all_25_0_8, yields: % 33.47/10.29 | (142) all_25_0_8 = all_0_3_3 | ~ (times(all_0_3_3, all_80_0_31) = all_0_3_3) % 33.47/10.29 | % 33.47/10.29 | Instantiating formula (8) with all_0_3_3, all_8_0_4, all_84_0_33, all_0_3_3 and discharging atoms times(all_0_3_3, all_8_0_4) = all_84_0_33, times(all_0_3_3, all_8_0_4) = all_0_3_3, yields: % 33.47/10.29 | (143) all_84_0_33 = all_0_3_3 % 33.47/10.29 | % 33.47/10.29 | Instantiating formula (8) with all_0_3_3, all_8_0_4, all_76_0_29, all_82_0_32 and discharging atoms times(all_0_3_3, all_8_0_4) = all_76_0_29, yields: % 33.47/10.29 | (144) all_82_0_32 = all_76_0_29 | ~ (times(all_0_3_3, all_8_0_4) = all_82_0_32) % 33.47/10.29 | % 33.47/10.29 | Instantiating formula (8) with all_0_3_3, all_8_0_4, all_76_0_29, all_84_0_33 and discharging atoms times(all_0_3_3, all_8_0_4) = all_84_0_33, times(all_0_3_3, all_8_0_4) = all_76_0_29, yields: % 33.47/10.29 | (145) all_84_0_33 = all_76_0_29 % 33.47/10.29 | % 33.47/10.29 | Instantiating formula (8) with all_0_3_3, all_0_2_2, all_46_0_14, all_0_1_1 and discharging atoms times(all_0_3_3, all_0_2_2) = all_46_0_14, times(all_0_3_3, all_0_2_2) = all_0_1_1, yields: % 33.47/10.29 | (146) all_46_0_14 = all_0_1_1 % 33.47/10.29 | % 33.47/10.29 | Instantiating formula (8) with all_0_3_3, all_0_3_3, all_80_0_31, all_8_0_4 and discharging atoms times(all_0_3_3, all_0_3_3) = all_80_0_31, times(all_0_3_3, all_0_3_3) = all_8_0_4, yields: % 33.47/10.29 | (147) all_80_0_31 = all_8_0_4 % 33.47/10.29 | % 33.47/10.29 | Instantiating formula (8) with all_0_3_3, all_0_3_3, all_80_0_31, all_86_0_34 and discharging atoms times(all_0_3_3, all_0_3_3) = all_80_0_31, yields: % 33.47/10.29 | (148) all_86_0_34 = all_80_0_31 | ~ (times(all_0_3_3, all_0_3_3) = all_86_0_34) % 33.47/10.29 | % 33.47/10.29 | Instantiating formula (8) with all_0_3_3, all_0_3_3, all_78_0_30, all_80_0_31 and discharging atoms times(all_0_3_3, all_0_3_3) = all_80_0_31, times(all_0_3_3, all_0_3_3) = all_78_0_30, yields: % 33.47/10.29 | (149) all_80_0_31 = all_78_0_30 % 33.47/10.29 | % 33.47/10.29 | Combining equations (145,143) yields a new equation: % 33.47/10.29 | (150) all_76_0_29 = all_0_3_3 % 33.47/10.29 | % 33.47/10.29 | Simplifying 150 yields: % 33.47/10.29 | (151) all_76_0_29 = all_0_3_3 % 33.47/10.29 | % 33.47/10.29 | Combining equations (147,149) yields a new equation: % 33.47/10.29 | (152) all_78_0_30 = all_8_0_4 % 33.47/10.29 | % 33.47/10.29 | Combining equations (152,149) yields a new equation: % 33.47/10.29 | (147) all_80_0_31 = all_8_0_4 % 33.47/10.29 | % 33.47/10.29 | From (151) and (117) follows: % 33.47/10.29 | (154) times(all_31_0_11, all_0_3_3) = all_29_0_10 % 33.47/10.29 | % 33.47/10.29 | From (146) and (81) follows: % 33.47/10.29 | (155) times(all_10_0_5, all_0_1_1) = all_31_0_11 % 33.47/10.29 | % 33.47/10.29 | From (135) and (94) follows: % 33.47/10.29 | (55) times(all_8_0_4, all_8_0_4) = all_8_0_4 % 33.47/10.29 | % 33.47/10.29 | From (152) and (120) follows: % 33.47/10.29 | (157) times(all_0_2_2, all_8_0_4) = all_29_0_10 % 33.47/10.29 | % 33.47/10.29 | From (140) and (96) follows: % 33.47/10.29 | (158) times(all_0_2_2, all_10_0_5) = all_27_0_9 % 33.47/10.29 | % 33.47/10.29 | From (151) and (118) follows: % 33.47/10.29 | (16) times(all_0_3_3, all_8_0_4) = all_0_3_3 % 33.47/10.29 | % 33.47/10.29 | From (146) and (82) follows: % 33.47/10.29 | (2) times(all_0_3_3, all_0_2_2) = all_0_1_1 % 33.47/10.29 | % 33.47/10.29 +-Applying beta-rule and splitting (142), into two cases. % 33.47/10.29 |-Branch one: % 33.47/10.29 | (161) ~ (times(all_0_3_3, all_80_0_31) = all_0_3_3) % 33.47/10.29 | % 33.47/10.29 | From (147) and (161) follows: % 33.47/10.29 | (162) ~ (times(all_0_3_3, all_8_0_4) = all_0_3_3) % 33.47/10.29 | % 33.47/10.29 | Using (16) and (162) yields: % 33.47/10.29 | (163) $false % 33.47/10.29 | % 33.47/10.29 |-The branch is then unsatisfiable % 33.47/10.29 |-Branch two: % 33.47/10.29 | (164) times(all_0_3_3, all_80_0_31) = all_0_3_3 % 33.47/10.29 | (165) all_25_0_8 = all_0_3_3 % 33.47/10.29 | % 33.47/10.29 | From (165) and (126) follows: % 33.47/10.29 | (166) times(all_0_3_3, all_8_0_4) = all_82_0_32 % 33.47/10.29 | % 33.47/10.29 | From (165) and (132) follows: % 33.47/10.29 | (167) times(all_0_3_3, all_0_3_3) = all_86_0_34 % 33.47/10.29 | % 33.47/10.29 +-Applying beta-rule and splitting (148), into two cases. % 33.47/10.29 |-Branch one: % 33.47/10.29 | (168) ~ (times(all_0_3_3, all_0_3_3) = all_86_0_34) % 33.47/10.30 | % 33.47/10.30 | Using (167) and (168) yields: % 33.47/10.30 | (163) $false % 33.47/10.30 | % 33.47/10.30 |-The branch is then unsatisfiable % 33.47/10.30 |-Branch two: % 33.47/10.30 | (167) times(all_0_3_3, all_0_3_3) = all_86_0_34 % 33.47/10.30 | (171) all_86_0_34 = all_80_0_31 % 33.47/10.30 | % 33.47/10.30 | Combining equations (147,171) yields a new equation: % 33.47/10.30 | (172) all_86_0_34 = all_8_0_4 % 33.47/10.30 | % 33.47/10.30 | From (172) and (167) follows: % 33.47/10.30 | (17) times(all_0_3_3, all_0_3_3) = all_8_0_4 % 33.47/10.30 | % 33.47/10.30 +-Applying beta-rule and splitting (139), into two cases. % 33.47/10.30 |-Branch one: % 33.47/10.30 | (174) ~ (times(all_0_2_2, all_8_0_4) = all_29_0_10) % 33.47/10.30 | % 33.47/10.30 | Using (157) and (174) yields: % 33.47/10.30 | (163) $false % 33.47/10.30 | % 33.47/10.30 |-The branch is then unsatisfiable % 33.47/10.30 |-Branch two: % 33.47/10.30 | (157) times(all_0_2_2, all_8_0_4) = all_29_0_10 % 33.47/10.30 | (177) all_48_0_15 = all_29_0_10 % 33.47/10.30 | % 33.47/10.30 | From (177) and (85) follows: % 33.47/10.30 | (157) times(all_0_2_2, all_8_0_4) = all_29_0_10 % 33.47/10.30 | % 33.47/10.30 +-Applying beta-rule and splitting (136), into two cases. % 33.47/10.30 |-Branch one: % 33.47/10.30 | (179) ~ (times(all_0_2_2, all_10_0_5) = all_27_0_9) % 33.47/10.30 | % 33.47/10.30 | Using (158) and (179) yields: % 33.47/10.30 | (163) $false % 33.47/10.30 | % 33.47/10.30 |-The branch is then unsatisfiable % 33.47/10.30 |-Branch two: % 33.47/10.30 | (158) times(all_0_2_2, all_10_0_5) = all_27_0_9 % 33.47/10.30 | (182) all_27_0_9 = all_0_2_2 % 33.47/10.30 | % 33.47/10.30 | From (182) and (106) follows: % 33.47/10.30 | (183) times(all_0_2_2, all_64_0_23) = all_16_0_6 % 33.47/10.30 | % 33.47/10.30 | From (182) and (78) follows: % 33.47/10.30 | (184) times(all_0_2_2, all_44_0_13) = all_31_0_11 % 33.47/10.30 | % 33.47/10.30 | From (182) and (99) follows: % 33.47/10.30 | (185) times(all_0_2_2, all_10_0_5) = all_58_0_20 % 33.47/10.30 | % 33.47/10.30 | From (182) and (111) follows: % 33.47/10.30 | (186) times(all_0_2_2, all_0_2_2) = all_70_0_26 % 33.47/10.30 | % 33.47/10.30 +-Applying beta-rule and splitting (144), into two cases. % 33.47/10.30 |-Branch one: % 33.47/10.30 | (187) ~ (times(all_0_3_3, all_8_0_4) = all_82_0_32) % 33.47/10.30 | % 33.47/10.30 | Using (166) and (187) yields: % 33.47/10.30 | (163) $false % 33.47/10.30 | % 33.47/10.30 |-The branch is then unsatisfiable % 33.47/10.30 |-Branch two: % 33.47/10.30 | (166) times(all_0_3_3, all_8_0_4) = all_82_0_32 % 33.47/10.30 | (190) all_82_0_32 = all_76_0_29 % 33.47/10.30 | % 33.47/10.30 | Combining equations (151,190) yields a new equation: % 33.47/10.30 | (191) all_82_0_32 = all_0_3_3 % 33.47/10.30 | % 33.47/10.30 | From (191) and (127) follows: % 33.47/10.30 | (192) times(all_8_0_4, all_0_3_3) = all_0_3_3 % 33.47/10.30 | % 33.47/10.30 | From (191) and (166) follows: % 33.47/10.30 | (16) times(all_0_3_3, all_8_0_4) = all_0_3_3 % 33.47/10.30 | % 33.47/10.30 +-Applying beta-rule and splitting (141), into two cases. % 33.47/10.30 |-Branch one: % 33.47/10.30 | (194) ~ (times(all_0_2_2, all_0_2_2) = all_70_0_26) % 33.47/10.30 | % 33.47/10.30 | Using (186) and (194) yields: % 33.47/10.30 | (163) $false % 33.47/10.30 | % 33.47/10.30 |-The branch is then unsatisfiable % 33.47/10.30 |-Branch two: % 33.47/10.30 | (186) times(all_0_2_2, all_0_2_2) = all_70_0_26 % 33.47/10.30 | (197) all_70_0_26 = all_56_0_19 % 33.47/10.30 | % 33.47/10.30 | Combining equations (140,197) yields a new equation: % 33.47/10.30 | (198) all_70_0_26 = all_10_0_5 % 33.47/10.30 | % 33.47/10.30 | From (198) and (186) follows: % 33.47/10.30 | (20) times(all_0_2_2, all_0_2_2) = all_10_0_5 % 33.47/10.30 | % 33.47/10.30 +-Applying beta-rule and splitting (138), into two cases. % 33.47/10.30 |-Branch one: % 33.47/10.30 | (200) ~ (times(all_0_2_2, all_10_0_5) = all_58_0_20) % 33.47/10.30 | % 33.47/10.30 | Using (185) and (200) yields: % 33.47/10.30 | (163) $false % 33.47/10.30 | % 33.47/10.30 |-The branch is then unsatisfiable % 33.47/10.30 |-Branch two: % 33.47/10.30 | (185) times(all_0_2_2, all_10_0_5) = all_58_0_20 % 33.47/10.30 | (203) all_68_0_25 = all_58_0_20 % 33.47/10.30 | % 33.47/10.30 | Combining equations (203,137) yields a new equation: % 33.47/10.30 | (204) all_58_0_20 = all_0_2_2 % 33.47/10.30 | % 33.47/10.30 | Simplifying 204 yields: % 33.47/10.30 | (205) all_58_0_20 = all_0_2_2 % 33.47/10.30 | % 33.47/10.30 | From (205) and (100) follows: % 33.47/10.30 | (206) times(all_10_0_5, all_0_2_2) = all_0_2_2 % 33.47/10.30 | % 33.47/10.30 | From (205) and (185) follows: % 33.47/10.30 | (19) times(all_0_2_2, all_10_0_5) = all_0_2_2 % 33.47/10.30 | % 33.47/10.30 +-Applying beta-rule and splitting (134), into two cases. % 33.47/10.30 |-Branch one: % 33.47/10.30 | (208) ~ (times(all_31_0_11, all_0_3_3) = all_29_0_10) % 33.47/10.30 | % 33.47/10.30 | Using (154) and (208) yields: % 33.47/10.30 | (163) $false % 33.47/10.30 | % 33.47/10.30 |-The branch is then unsatisfiable % 33.47/10.30 |-Branch two: % 33.47/10.30 | (154) times(all_31_0_11, all_0_3_3) = all_29_0_10 % 33.47/10.30 | (211) all_50_0_16 = all_29_0_10 % 33.47/10.30 | % 33.47/10.30 | From (211) and (87) follows: % 33.47/10.30 | (154) times(all_31_0_11, all_0_3_3) = all_29_0_10 % 33.47/10.30 | % 33.47/10.30 | From (211) and (88) follows: % 33.47/10.30 | (213) times(all_0_3_3, all_29_0_10) = all_0_1_1 % 33.47/10.30 | % 33.47/10.30 | Instantiating formula (4) with all_16_0_6, all_31_0_11, all_52_0_17, all_0_3_3, all_0_2_2 and discharging atoms times(all_31_0_11, all_52_0_17) = all_16_0_6, times(all_0_2_2, all_0_3_3) = all_31_0_11, yields: % 33.47/10.30 | (214) ? [v0] : (times(all_52_0_17, all_0_2_2) = v0 & times(all_0_3_3, v0) = all_16_0_6) % 33.47/10.30 | % 33.47/10.30 | Instantiating formula (4) with all_16_0_6, all_31_0_11, all_52_0_17, all_8_0_4, all_31_0_11 and discharging atoms times(all_31_0_11, all_52_0_17) = all_16_0_6, yields: % 33.47/10.30 | (215) ~ (times(all_31_0_11, all_8_0_4) = all_31_0_11) | ? [v0] : (times(all_52_0_17, all_31_0_11) = v0 & times(all_8_0_4, v0) = all_16_0_6) % 33.47/10.30 | % 33.47/10.30 | Instantiating formula (4) with all_31_0_11, all_31_0_11, all_8_0_4, all_8_0_4, all_31_0_11 yields: % 33.47/10.30 | (216) ~ (times(all_31_0_11, all_8_0_4) = all_31_0_11) | ? [v0] : (times(all_8_0_4, v0) = all_31_0_11 & times(all_8_0_4, all_31_0_11) = v0) % 33.47/10.30 | % 33.47/10.30 | Instantiating formula (4) with all_29_0_10, all_31_0_11, all_0_3_3, all_0_3_3, all_0_2_2 and discharging atoms times(all_31_0_11, all_0_3_3) = all_29_0_10, times(all_0_2_2, all_0_3_3) = all_31_0_11, yields: % 33.47/10.30 | (217) ? [v0] : (times(all_0_3_3, v0) = all_29_0_10 & times(all_0_3_3, all_0_2_2) = v0) % 33.47/10.30 | % 33.47/10.30 | Instantiating formula (4) with all_29_0_10, all_31_0_11, all_0_3_3, all_8_0_4, all_31_0_11 and discharging atoms times(all_31_0_11, all_0_3_3) = all_29_0_10, yields: % 33.47/10.30 | (218) ~ (times(all_31_0_11, all_8_0_4) = all_31_0_11) | ? [v0] : (times(all_8_0_4, v0) = all_29_0_10 & times(all_0_3_3, all_31_0_11) = v0) % 33.47/10.31 | % 33.47/10.31 | Instantiating formula (4) with all_64_0_23, all_29_0_10, all_10_0_5, all_0_3_3, all_0_1_1 and discharging atoms times(all_29_0_10, all_10_0_5) = all_64_0_23, times(all_0_1_1, all_0_3_3) = all_29_0_10, yields: % 33.47/10.31 | (219) ? [v0] : (times(all_10_0_5, all_0_1_1) = v0 & times(all_0_3_3, v0) = all_64_0_23) % 33.47/10.31 | % 33.47/10.31 | Instantiating formula (4) with all_74_0_28, all_29_0_10, all_0_2_2, all_10_0_5, all_29_0_10 and discharging atoms times(all_29_0_10, all_0_2_2) = all_74_0_28, yields: % 33.47/10.31 | (220) ~ (times(all_29_0_10, all_10_0_5) = all_29_0_10) | ? [v0] : (times(all_10_0_5, v0) = all_74_0_28 & times(all_0_2_2, all_29_0_10) = v0) % 33.47/10.31 | % 33.47/10.31 | Instantiating formula (4) with all_16_0_6, all_10_0_5, all_74_0_28, all_0_2_2, all_0_2_2 and discharging atoms times(all_10_0_5, all_74_0_28) = all_16_0_6, times(all_0_2_2, all_0_2_2) = all_10_0_5, yields: % 33.47/10.31 | (221) ? [v0] : (times(all_74_0_28, all_0_2_2) = v0 & times(all_0_2_2, v0) = all_16_0_6) % 33.47/10.31 | % 33.47/10.31 | Instantiating formula (4) with all_31_0_11, all_10_0_5, all_0_1_1, all_0_2_2, all_0_2_2 and discharging atoms times(all_10_0_5, all_0_1_1) = all_31_0_11, times(all_0_2_2, all_0_2_2) = all_10_0_5, yields: % 33.47/10.31 | (222) ? [v0] : (times(all_0_1_1, all_0_2_2) = v0 & times(all_0_2_2, v0) = all_31_0_11) % 33.47/10.31 | % 33.47/10.31 | Instantiating formula (4) with all_31_0_11, all_8_0_4, all_0_1_1, all_0_3_3, all_0_3_3 and discharging atoms times(all_0_3_3, all_0_3_3) = all_8_0_4, yields: % 33.47/10.31 | (223) ~ (times(all_8_0_4, all_0_1_1) = all_31_0_11) | ? [v0] : (times(all_0_1_1, all_0_3_3) = v0 & times(all_0_3_3, v0) = all_31_0_11) % 33.47/10.31 | % 33.47/10.31 | Instantiating formula (4) with all_62_0_22, all_31_0_11, all_8_0_4, all_0_1_1, all_10_0_5 and discharging atoms times(all_31_0_11, all_8_0_4) = all_62_0_22, times(all_10_0_5, all_0_1_1) = all_31_0_11, yields: % 33.47/10.31 | (224) ? [v0] : (times(all_8_0_4, all_10_0_5) = v0 & times(all_0_1_1, v0) = all_62_0_22) % 33.47/10.31 | % 33.47/10.31 | Instantiating formula (4) with all_16_0_6, all_0_1_1, all_0_1_1, all_62_0_22, all_8_0_4 and discharging atoms times(all_8_0_4, all_62_0_22) = all_0_1_1, times(all_0_1_1, all_0_1_1) = all_16_0_6, yields: % 33.47/10.31 | (225) ? [v0] : (times(all_62_0_22, v0) = all_16_0_6 & times(all_0_1_1, all_8_0_4) = v0) % 33.47/10.31 | % 33.47/10.31 | Instantiating formula (4) with all_52_0_17, all_0_1_1, all_8_0_4, all_31_0_11, all_8_0_4 and discharging atoms times(all_8_0_4, all_31_0_11) = all_0_1_1, times(all_0_1_1, all_8_0_4) = all_52_0_17, yields: % 33.47/10.31 | (226) ? [v0] : (times(all_31_0_11, v0) = all_52_0_17 & times(all_8_0_4, all_8_0_4) = v0) % 33.47/10.31 | % 33.47/10.31 | Instantiating formula (4) with all_52_0_17, all_0_1_1, all_8_0_4, all_0_2_2, all_0_3_3 and discharging atoms times(all_0_1_1, all_8_0_4) = all_52_0_17, times(all_0_3_3, all_0_2_2) = all_0_1_1, yields: % 33.47/10.31 | (227) ? [v0] : (times(all_8_0_4, all_0_3_3) = v0 & times(all_0_2_2, v0) = all_52_0_17) % 33.47/10.31 | % 33.47/10.31 | Instantiating formula (4) with all_16_0_6, all_31_0_11, all_31_0_11, all_8_0_4, all_0_1_1 yields: % 33.47/10.31 | (228) ~ (times(all_31_0_11, all_31_0_11) = all_16_0_6) | ~ (times(all_0_1_1, all_8_0_4) = all_31_0_11) | ? [v0] : (times(all_31_0_11, all_0_1_1) = v0 & times(all_8_0_4, v0) = all_16_0_6) % 33.47/10.31 | % 33.47/10.31 | Instantiating formula (4) with all_62_0_22, all_31_0_11, all_8_0_4, all_8_0_4, all_0_1_1 and discharging atoms times(all_31_0_11, all_8_0_4) = all_62_0_22, yields: % 33.47/10.31 | (229) ~ (times(all_0_1_1, all_8_0_4) = all_31_0_11) | ? [v0] : (times(all_8_0_4, v0) = all_62_0_22 & times(all_8_0_4, all_0_1_1) = v0) % 33.47/10.31 | % 33.47/10.31 | Instantiating formula (4) with all_29_0_10, all_31_0_11, all_0_3_3, all_8_0_4, all_0_1_1 and discharging atoms times(all_31_0_11, all_0_3_3) = all_29_0_10, yields: % 33.47/10.31 | (230) ~ (times(all_0_1_1, all_8_0_4) = all_31_0_11) | ? [v0] : (times(all_8_0_4, v0) = all_29_0_10 & times(all_0_3_3, all_0_1_1) = v0) % 33.47/10.31 | % 33.47/10.31 | Instantiating formula (4) with all_52_0_17, all_0_1_1, all_8_0_4, all_62_0_22, all_8_0_4 and discharging atoms times(all_8_0_4, all_62_0_22) = all_0_1_1, times(all_0_1_1, all_8_0_4) = all_52_0_17, yields: % 33.47/10.31 | (231) ? [v0] : (times(all_62_0_22, v0) = all_52_0_17 & times(all_8_0_4, all_8_0_4) = v0) % 33.47/10.31 | % 33.47/10.31 | Instantiating formula (4) with all_16_0_6, all_0_2_2, all_64_0_23, all_10_0_5, all_0_2_2 and discharging atoms times(all_0_2_2, all_64_0_23) = all_16_0_6, times(all_0_2_2, all_10_0_5) = all_0_2_2, yields: % 33.47/10.31 | (232) ? [v0] : (times(all_64_0_23, all_0_2_2) = v0 & times(all_10_0_5, v0) = all_16_0_6) % 33.47/10.31 | % 33.47/10.31 | Instantiating formula (4) with all_16_0_6, all_0_2_2, all_64_0_23, all_0_2_2, all_10_0_5 and discharging atoms times(all_10_0_5, all_0_2_2) = all_0_2_2, times(all_0_2_2, all_64_0_23) = all_16_0_6, yields: % 33.47/10.31 | (233) ? [v0] : (times(all_64_0_23, all_10_0_5) = v0 & times(all_0_2_2, v0) = all_16_0_6) % 33.47/10.31 | % 33.47/10.31 | Instantiating formula (4) with all_16_0_6, all_31_0_11, all_52_0_17, all_44_0_13, all_0_2_2 and discharging atoms times(all_31_0_11, all_52_0_17) = all_16_0_6, times(all_0_2_2, all_44_0_13) = all_31_0_11, yields: % 33.47/10.31 | (234) ? [v0] : (times(all_52_0_17, all_0_2_2) = v0 & times(all_44_0_13, v0) = all_16_0_6) % 33.47/10.31 | % 33.47/10.31 | Instantiating formula (4) with all_29_0_10, all_31_0_11, all_0_3_3, all_44_0_13, all_0_2_2 and discharging atoms times(all_31_0_11, all_0_3_3) = all_29_0_10, times(all_0_2_2, all_44_0_13) = all_31_0_11, yields: % 33.47/10.31 | (235) ? [v0] : (times(all_44_0_13, v0) = all_29_0_10 & times(all_0_3_3, all_0_2_2) = v0) % 33.47/10.31 | % 33.47/10.31 | Instantiating formula (4) with all_74_0_28, all_29_0_10, all_0_2_2, all_8_0_4, all_0_2_2 and discharging atoms times(all_29_0_10, all_0_2_2) = all_74_0_28, times(all_0_2_2, all_8_0_4) = all_29_0_10, yields: % 33.47/10.31 | (236) ? [v0] : (times(all_8_0_4, v0) = all_74_0_28 & times(all_0_2_2, all_0_2_2) = v0) % 33.47/10.31 | % 33.47/10.31 | Instantiating formula (4) with all_29_0_10, all_0_2_2, all_8_0_4, all_0_2_2, all_10_0_5 and discharging atoms times(all_10_0_5, all_0_2_2) = all_0_2_2, times(all_0_2_2, all_8_0_4) = all_29_0_10, yields: % 33.47/10.31 | (237) ? [v0] : (times(all_8_0_4, all_10_0_5) = v0 & times(all_0_2_2, v0) = all_29_0_10) % 33.47/10.31 | % 33.47/10.31 | Instantiating formula (4) with all_29_0_10, all_0_1_1, all_0_3_3, all_29_0_10, all_0_3_3 and discharging atoms times(all_0_1_1, all_0_3_3) = all_29_0_10, times(all_0_3_3, all_29_0_10) = all_0_1_1, yields: % 33.47/10.31 | (238) ? [v0] : (times(all_29_0_10, v0) = all_29_0_10 & times(all_0_3_3, all_0_3_3) = v0) % 33.47/10.31 | % 33.47/10.31 | Instantiating formula (4) with all_0_1_1, all_0_3_3, all_29_0_10, all_8_0_4, all_0_3_3 and discharging atoms times(all_0_3_3, all_29_0_10) = all_0_1_1, times(all_0_3_3, all_8_0_4) = all_0_3_3, yields: % 33.47/10.31 | (239) ? [v0] : (times(all_29_0_10, all_0_3_3) = v0 & times(all_8_0_4, v0) = all_0_1_1) % 33.47/10.31 | % 33.47/10.31 | Instantiating formula (4) with all_0_1_1, all_0_3_3, all_29_0_10, all_0_3_3, all_8_0_4 and discharging atoms times(all_8_0_4, all_0_3_3) = all_0_3_3, times(all_0_3_3, all_29_0_10) = all_0_1_1, yields: % 33.47/10.31 | (240) ? [v0] : (times(all_29_0_10, all_8_0_4) = v0 & times(all_0_3_3, v0) = all_0_1_1) % 33.47/10.31 | % 33.47/10.31 | Instantiating formula (4) with all_52_0_17, all_0_1_1, all_8_0_4, all_29_0_10, all_0_3_3 and discharging atoms times(all_0_1_1, all_8_0_4) = all_52_0_17, times(all_0_3_3, all_29_0_10) = all_0_1_1, yields: % 33.47/10.31 | (241) ? [v0] : (times(all_29_0_10, v0) = all_52_0_17 & times(all_8_0_4, all_0_3_3) = v0) % 33.47/10.31 | % 33.47/10.31 | Instantiating (241) with all_131_0_36 yields: % 33.47/10.31 | (242) times(all_29_0_10, all_131_0_36) = all_52_0_17 & times(all_8_0_4, all_0_3_3) = all_131_0_36 % 33.47/10.31 | % 33.47/10.31 | Applying alpha-rule on (242) yields: % 33.47/10.32 | (243) times(all_29_0_10, all_131_0_36) = all_52_0_17 % 33.47/10.32 | (244) times(all_8_0_4, all_0_3_3) = all_131_0_36 % 33.47/10.32 | % 33.47/10.32 | Instantiating (239) with all_133_0_37 yields: % 33.47/10.32 | (245) times(all_29_0_10, all_0_3_3) = all_133_0_37 & times(all_8_0_4, all_133_0_37) = all_0_1_1 % 33.47/10.32 | % 33.47/10.32 | Applying alpha-rule on (245) yields: % 33.47/10.32 | (246) times(all_29_0_10, all_0_3_3) = all_133_0_37 % 33.47/10.32 | (247) times(all_8_0_4, all_133_0_37) = all_0_1_1 % 33.47/10.32 | % 33.47/10.32 | Instantiating (236) with all_139_0_40 yields: % 33.47/10.32 | (248) times(all_8_0_4, all_139_0_40) = all_74_0_28 & times(all_0_2_2, all_0_2_2) = all_139_0_40 % 33.47/10.32 | % 33.47/10.32 | Applying alpha-rule on (248) yields: % 33.47/10.32 | (249) times(all_8_0_4, all_139_0_40) = all_74_0_28 % 33.47/10.32 | (250) times(all_0_2_2, all_0_2_2) = all_139_0_40 % 33.47/10.32 | % 33.47/10.32 | Instantiating (240) with all_147_0_44 yields: % 33.47/10.32 | (251) times(all_29_0_10, all_8_0_4) = all_147_0_44 & times(all_0_3_3, all_147_0_44) = all_0_1_1 % 33.47/10.32 | % 33.47/10.32 | Applying alpha-rule on (251) yields: % 33.47/10.32 | (252) times(all_29_0_10, all_8_0_4) = all_147_0_44 % 33.47/10.32 | (253) times(all_0_3_3, all_147_0_44) = all_0_1_1 % 33.47/10.32 | % 33.47/10.32 | Instantiating (238) with all_149_0_45 yields: % 33.47/10.32 | (254) times(all_29_0_10, all_149_0_45) = all_29_0_10 & times(all_0_3_3, all_0_3_3) = all_149_0_45 % 33.47/10.32 | % 33.47/10.32 | Applying alpha-rule on (254) yields: % 33.47/10.32 | (255) times(all_29_0_10, all_149_0_45) = all_29_0_10 % 33.90/10.32 | (256) times(all_0_3_3, all_0_3_3) = all_149_0_45 % 33.90/10.32 | % 33.90/10.32 | Instantiating (237) with all_151_0_46 yields: % 33.90/10.32 | (257) times(all_8_0_4, all_10_0_5) = all_151_0_46 & times(all_0_2_2, all_151_0_46) = all_29_0_10 % 33.90/10.32 | % 33.90/10.32 | Applying alpha-rule on (257) yields: % 33.90/10.32 | (258) times(all_8_0_4, all_10_0_5) = all_151_0_46 % 33.90/10.32 | (259) times(all_0_2_2, all_151_0_46) = all_29_0_10 % 33.90/10.32 | % 33.90/10.32 | Instantiating (235) with all_153_0_47 yields: % 33.90/10.32 | (260) times(all_44_0_13, all_153_0_47) = all_29_0_10 & times(all_0_3_3, all_0_2_2) = all_153_0_47 % 33.90/10.32 | % 33.90/10.32 | Applying alpha-rule on (260) yields: % 33.90/10.32 | (261) times(all_44_0_13, all_153_0_47) = all_29_0_10 % 33.90/10.32 | (262) times(all_0_3_3, all_0_2_2) = all_153_0_47 % 33.90/10.32 | % 33.90/10.32 | Instantiating (234) with all_157_0_49 yields: % 33.90/10.32 | (263) times(all_52_0_17, all_0_2_2) = all_157_0_49 & times(all_44_0_13, all_157_0_49) = all_16_0_6 % 33.90/10.32 | % 33.90/10.32 | Applying alpha-rule on (263) yields: % 33.90/10.32 | (264) times(all_52_0_17, all_0_2_2) = all_157_0_49 % 33.90/10.32 | (265) times(all_44_0_13, all_157_0_49) = all_16_0_6 % 33.90/10.32 | % 33.90/10.32 | Instantiating (233) with all_163_0_52 yields: % 33.90/10.32 | (266) times(all_64_0_23, all_10_0_5) = all_163_0_52 & times(all_0_2_2, all_163_0_52) = all_16_0_6 % 33.90/10.32 | % 33.90/10.32 | Applying alpha-rule on (266) yields: % 33.90/10.32 | (267) times(all_64_0_23, all_10_0_5) = all_163_0_52 % 33.90/10.32 | (268) times(all_0_2_2, all_163_0_52) = all_16_0_6 % 33.90/10.32 | % 33.90/10.32 | Instantiating (231) with all_167_0_54 yields: % 33.90/10.32 | (269) times(all_62_0_22, all_167_0_54) = all_52_0_17 & times(all_8_0_4, all_8_0_4) = all_167_0_54 % 33.90/10.32 | % 33.90/10.32 | Applying alpha-rule on (269) yields: % 33.90/10.32 | (270) times(all_62_0_22, all_167_0_54) = all_52_0_17 % 33.90/10.32 | (271) times(all_8_0_4, all_8_0_4) = all_167_0_54 % 33.90/10.32 | % 33.90/10.32 | Instantiating (227) with all_169_0_55 yields: % 33.90/10.32 | (272) times(all_8_0_4, all_0_3_3) = all_169_0_55 & times(all_0_2_2, all_169_0_55) = all_52_0_17 % 33.90/10.32 | % 33.90/10.32 | Applying alpha-rule on (272) yields: % 33.90/10.32 | (273) times(all_8_0_4, all_0_3_3) = all_169_0_55 % 33.90/10.32 | (274) times(all_0_2_2, all_169_0_55) = all_52_0_17 % 33.90/10.32 | % 33.90/10.32 | Instantiating (232) with all_171_0_56 yields: % 33.90/10.32 | (275) times(all_64_0_23, all_0_2_2) = all_171_0_56 & times(all_10_0_5, all_171_0_56) = all_16_0_6 % 33.90/10.32 | % 33.90/10.32 | Applying alpha-rule on (275) yields: % 33.90/10.32 | (276) times(all_64_0_23, all_0_2_2) = all_171_0_56 % 33.90/10.32 | (277) times(all_10_0_5, all_171_0_56) = all_16_0_6 % 33.90/10.32 | % 33.90/10.32 | Instantiating (226) with all_173_0_57 yields: % 33.90/10.32 | (278) times(all_31_0_11, all_173_0_57) = all_52_0_17 & times(all_8_0_4, all_8_0_4) = all_173_0_57 % 33.90/10.32 | % 33.90/10.32 | Applying alpha-rule on (278) yields: % 33.90/10.32 | (279) times(all_31_0_11, all_173_0_57) = all_52_0_17 % 33.90/10.32 | (280) times(all_8_0_4, all_8_0_4) = all_173_0_57 % 33.90/10.32 | % 33.90/10.32 | Instantiating (224) with all_175_0_58 yields: % 33.90/10.32 | (281) times(all_8_0_4, all_10_0_5) = all_175_0_58 & times(all_0_1_1, all_175_0_58) = all_62_0_22 % 33.90/10.32 | % 33.90/10.32 | Applying alpha-rule on (281) yields: % 33.90/10.32 | (282) times(all_8_0_4, all_10_0_5) = all_175_0_58 % 33.90/10.32 | (283) times(all_0_1_1, all_175_0_58) = all_62_0_22 % 33.90/10.32 | % 33.90/10.32 | Instantiating (219) with all_179_0_60 yields: % 33.90/10.32 | (284) times(all_10_0_5, all_0_1_1) = all_179_0_60 & times(all_0_3_3, all_179_0_60) = all_64_0_23 % 33.90/10.32 | % 33.90/10.32 | Applying alpha-rule on (284) yields: % 33.90/10.32 | (285) times(all_10_0_5, all_0_1_1) = all_179_0_60 % 33.90/10.32 | (286) times(all_0_3_3, all_179_0_60) = all_64_0_23 % 33.90/10.32 | % 33.90/10.33 | Instantiating (214) with all_185_0_63 yields: % 33.90/10.33 | (287) times(all_52_0_17, all_0_2_2) = all_185_0_63 & times(all_0_3_3, all_185_0_63) = all_16_0_6 % 33.90/10.33 | % 33.90/10.33 | Applying alpha-rule on (287) yields: % 33.90/10.33 | (288) times(all_52_0_17, all_0_2_2) = all_185_0_63 % 33.90/10.33 | (289) times(all_0_3_3, all_185_0_63) = all_16_0_6 % 33.90/10.33 | % 33.90/10.33 | Instantiating (217) with all_187_0_64 yields: % 33.90/10.33 | (290) times(all_0_3_3, all_187_0_64) = all_29_0_10 & times(all_0_3_3, all_0_2_2) = all_187_0_64 % 33.90/10.33 | % 33.90/10.33 | Applying alpha-rule on (290) yields: % 33.90/10.33 | (291) times(all_0_3_3, all_187_0_64) = all_29_0_10 % 33.90/10.33 | (292) times(all_0_3_3, all_0_2_2) = all_187_0_64 % 33.90/10.33 | % 33.90/10.33 | Instantiating (225) with all_193_0_67 yields: % 33.90/10.33 | (293) times(all_62_0_22, all_193_0_67) = all_16_0_6 & times(all_0_1_1, all_8_0_4) = all_193_0_67 % 33.90/10.33 | % 33.90/10.33 | Applying alpha-rule on (293) yields: % 33.90/10.33 | (294) times(all_62_0_22, all_193_0_67) = all_16_0_6 % 33.90/10.33 | (295) times(all_0_1_1, all_8_0_4) = all_193_0_67 % 33.90/10.33 | % 33.90/10.33 | Instantiating (222) with all_197_0_69 yields: % 33.90/10.33 | (296) times(all_0_1_1, all_0_2_2) = all_197_0_69 & times(all_0_2_2, all_197_0_69) = all_31_0_11 % 33.90/10.33 | % 33.90/10.33 | Applying alpha-rule on (296) yields: % 33.90/10.33 | (297) times(all_0_1_1, all_0_2_2) = all_197_0_69 % 33.90/10.33 | (298) times(all_0_2_2, all_197_0_69) = all_31_0_11 % 33.90/10.33 | % 33.90/10.33 | Instantiating (221) with all_199_0_70 yields: % 33.90/10.33 | (299) times(all_74_0_28, all_0_2_2) = all_199_0_70 & times(all_0_2_2, all_199_0_70) = all_16_0_6 % 33.90/10.33 | % 33.90/10.33 | Applying alpha-rule on (299) yields: % 33.90/10.33 | (300) times(all_74_0_28, all_0_2_2) = all_199_0_70 % 33.90/10.33 | (301) times(all_0_2_2, all_199_0_70) = all_16_0_6 % 33.90/10.33 | % 33.90/10.33 | Instantiating formula (8) with all_29_0_10, all_10_0_5, all_163_0_52, all_29_0_10 yields: % 33.90/10.33 | (302) all_163_0_52 = all_29_0_10 | ~ (times(all_29_0_10, all_10_0_5) = all_163_0_52) | ~ (times(all_29_0_10, all_10_0_5) = all_29_0_10) % 33.90/10.33 | % 33.90/10.33 | Instantiating formula (8) with all_29_0_10, all_0_2_2, all_171_0_56, all_74_0_28 and discharging atoms times(all_29_0_10, all_0_2_2) = all_74_0_28, yields: % 33.90/10.33 | (303) all_171_0_56 = all_74_0_28 | ~ (times(all_29_0_10, all_0_2_2) = all_171_0_56) % 33.90/10.33 | % 33.90/10.33 | Instantiating formula (8) with all_52_0_17, all_0_2_2, all_157_0_49, all_185_0_63 and discharging atoms times(all_52_0_17, all_0_2_2) = all_185_0_63, times(all_52_0_17, all_0_2_2) = all_157_0_49, yields: % 33.90/10.33 | (304) all_185_0_63 = all_157_0_49 % 33.90/10.33 | % 33.90/10.33 | Instantiating formula (8) with all_31_0_11, all_8_0_4, all_52_0_17, all_62_0_22 and discharging atoms times(all_31_0_11, all_8_0_4) = all_62_0_22, yields: % 33.90/10.33 | (305) all_62_0_22 = all_52_0_17 | ~ (times(all_31_0_11, all_8_0_4) = all_52_0_17) % 33.90/10.33 | % 33.90/10.33 | Instantiating formula (8) with all_29_0_10, all_8_0_4, all_147_0_44, all_29_0_10 and discharging atoms times(all_29_0_10, all_8_0_4) = all_147_0_44, yields: % 33.90/10.33 | (306) all_147_0_44 = all_29_0_10 | ~ (times(all_29_0_10, all_8_0_4) = all_29_0_10) % 33.90/10.33 | % 33.90/10.33 | Instantiating formula (8) with all_29_0_10, all_0_3_3, all_133_0_37, all_52_0_17 and discharging atoms times(all_29_0_10, all_0_3_3) = all_133_0_37, yields: % 33.90/10.33 | (307) all_133_0_37 = all_52_0_17 | ~ (times(all_29_0_10, all_0_3_3) = all_52_0_17) % 33.90/10.33 | % 33.90/10.33 | Instantiating formula (8) with all_10_0_5, all_0_1_1, all_179_0_60, all_31_0_11 and discharging atoms times(all_10_0_5, all_0_1_1) = all_179_0_60, times(all_10_0_5, all_0_1_1) = all_31_0_11, yields: % 33.90/10.33 | (308) all_179_0_60 = all_31_0_11 % 33.90/10.33 | % 33.90/10.33 | Instantiating formula (8) with all_8_0_4, all_10_0_5, all_175_0_58, all_74_0_28 and discharging atoms times(all_8_0_4, all_10_0_5) = all_175_0_58, yields: % 33.90/10.33 | (309) all_175_0_58 = all_74_0_28 | ~ (times(all_8_0_4, all_10_0_5) = all_74_0_28) % 33.90/10.33 | % 33.90/10.33 | Instantiating formula (8) with all_8_0_4, all_10_0_5, all_151_0_46, all_175_0_58 and discharging atoms times(all_8_0_4, all_10_0_5) = all_175_0_58, times(all_8_0_4, all_10_0_5) = all_151_0_46, yields: % 33.90/10.33 | (310) all_175_0_58 = all_151_0_46 % 33.90/10.33 | % 33.90/10.33 | Instantiating formula (8) with all_8_0_4, all_8_0_4, all_173_0_57, all_8_0_4 and discharging atoms times(all_8_0_4, all_8_0_4) = all_173_0_57, times(all_8_0_4, all_8_0_4) = all_8_0_4, yields: % 33.90/10.33 | (311) all_173_0_57 = all_8_0_4 % 33.90/10.33 | % 33.90/10.33 | Instantiating formula (8) with all_8_0_4, all_8_0_4, all_167_0_54, all_173_0_57 and discharging atoms times(all_8_0_4, all_8_0_4) = all_173_0_57, times(all_8_0_4, all_8_0_4) = all_167_0_54, yields: % 33.90/10.33 | (312) all_173_0_57 = all_167_0_54 % 33.90/10.33 | % 33.90/10.33 | Instantiating formula (8) with all_8_0_4, all_0_3_3, all_169_0_55, all_0_3_3 and discharging atoms times(all_8_0_4, all_0_3_3) = all_169_0_55, times(all_8_0_4, all_0_3_3) = all_0_3_3, yields: % 33.90/10.33 | (313) all_169_0_55 = all_0_3_3 % 33.90/10.33 | % 33.90/10.33 | Instantiating formula (8) with all_8_0_4, all_0_3_3, all_131_0_36, all_169_0_55 and discharging atoms times(all_8_0_4, all_0_3_3) = all_169_0_55, times(all_8_0_4, all_0_3_3) = all_131_0_36, yields: % 33.90/10.33 | (314) all_169_0_55 = all_131_0_36 % 33.90/10.33 | % 33.90/10.33 | Instantiating formula (8) with all_0_1_1, all_8_0_4, all_193_0_67, all_52_0_17 and discharging atoms times(all_0_1_1, all_8_0_4) = all_193_0_67, times(all_0_1_1, all_8_0_4) = all_52_0_17, yields: % 33.90/10.33 | (315) all_193_0_67 = all_52_0_17 % 33.90/10.33 | % 33.90/10.33 | Instantiating formula (8) with all_0_1_1, all_0_2_2, all_197_0_69, all_157_0_49 and discharging atoms times(all_0_1_1, all_0_2_2) = all_197_0_69, yields: % 33.90/10.33 | (316) all_197_0_69 = all_157_0_49 | ~ (times(all_0_1_1, all_0_2_2) = all_157_0_49) % 33.90/10.33 | % 33.90/10.33 | Instantiating formula (8) with all_0_2_2, all_169_0_55, all_52_0_17, all_31_0_11 and discharging atoms times(all_0_2_2, all_169_0_55) = all_52_0_17, yields: % 33.90/10.33 | (317) all_52_0_17 = all_31_0_11 | ~ (times(all_0_2_2, all_169_0_55) = all_31_0_11) % 33.90/10.33 | % 33.90/10.33 | Instantiating formula (8) with all_0_2_2, all_0_2_2, all_139_0_40, all_10_0_5 and discharging atoms times(all_0_2_2, all_0_2_2) = all_139_0_40, times(all_0_2_2, all_0_2_2) = all_10_0_5, yields: % 33.90/10.33 | (318) all_139_0_40 = all_10_0_5 % 33.90/10.33 | % 33.90/10.33 | Instantiating formula (8) with all_0_3_3, all_0_2_2, all_187_0_64, all_0_1_1 and discharging atoms times(all_0_3_3, all_0_2_2) = all_187_0_64, times(all_0_3_3, all_0_2_2) = all_0_1_1, yields: % 33.90/10.33 | (319) all_187_0_64 = all_0_1_1 % 33.90/10.33 | % 33.90/10.33 | Instantiating formula (8) with all_0_3_3, all_0_2_2, all_153_0_47, all_187_0_64 and discharging atoms times(all_0_3_3, all_0_2_2) = all_187_0_64, times(all_0_3_3, all_0_2_2) = all_153_0_47, yields: % 33.90/10.33 | (320) all_187_0_64 = all_153_0_47 % 33.90/10.33 | % 33.90/10.33 | Instantiating formula (8) with all_0_3_3, all_0_3_3, all_149_0_45, all_8_0_4 and discharging atoms times(all_0_3_3, all_0_3_3) = all_149_0_45, times(all_0_3_3, all_0_3_3) = all_8_0_4, yields: % 33.90/10.33 | (321) all_149_0_45 = all_8_0_4 % 33.90/10.33 | % 33.90/10.33 | Combining equations (319,320) yields a new equation: % 33.90/10.33 | (322) all_153_0_47 = all_0_1_1 % 33.90/10.34 | % 33.90/10.34 | Combining equations (311,312) yields a new equation: % 33.90/10.34 | (323) all_167_0_54 = all_8_0_4 % 33.90/10.34 | % 33.90/10.34 | Combining equations (314,313) yields a new equation: % 33.90/10.34 | (324) all_131_0_36 = all_0_3_3 % 33.90/10.34 | % 33.90/10.34 | Simplifying 324 yields: % 33.90/10.34 | (325) all_131_0_36 = all_0_3_3 % 33.90/10.34 | % 33.90/10.34 | Combining equations (323,312) yields a new equation: % 33.90/10.34 | (311) all_173_0_57 = all_8_0_4 % 33.90/10.34 | % 33.90/10.34 | Combining equations (322,320) yields a new equation: % 33.90/10.34 | (319) all_187_0_64 = all_0_1_1 % 33.90/10.34 | % 33.90/10.34 | From (304) and (288) follows: % 33.90/10.34 | (264) times(all_52_0_17, all_0_2_2) = all_157_0_49 % 33.90/10.34 | % 33.90/10.34 | From (311) and (279) follows: % 33.90/10.34 | (329) times(all_31_0_11, all_8_0_4) = all_52_0_17 % 33.90/10.34 | % 33.90/10.34 | From (321) and (255) follows: % 33.90/10.34 | (330) times(all_29_0_10, all_8_0_4) = all_29_0_10 % 33.90/10.34 | % 33.90/10.34 | From (325) and (243) follows: % 33.90/10.34 | (331) times(all_29_0_10, all_0_3_3) = all_52_0_17 % 33.90/10.34 | % 33.90/10.34 | From (318) and (249) follows: % 33.90/10.34 | (332) times(all_8_0_4, all_10_0_5) = all_74_0_28 % 33.90/10.34 | % 33.90/10.34 | From (310) and (283) follows: % 33.90/10.34 | (333) times(all_0_1_1, all_151_0_46) = all_62_0_22 % 33.90/10.34 | % 33.90/10.34 | From (315) and (295) follows: % 33.90/10.34 | (91) times(all_0_1_1, all_8_0_4) = all_52_0_17 % 33.90/10.34 | % 33.90/10.34 | From (319) and (291) follows: % 33.90/10.34 | (335) times(all_0_3_3, all_0_1_1) = all_29_0_10 % 33.90/10.34 | % 33.90/10.34 | From (308) and (286) follows: % 33.90/10.34 | (336) times(all_0_3_3, all_31_0_11) = all_64_0_23 % 33.90/10.34 | % 33.90/10.34 +-Applying beta-rule and splitting (317), into two cases. % 33.90/10.34 |-Branch one: % 33.90/10.34 | (337) ~ (times(all_0_2_2, all_169_0_55) = all_31_0_11) % 33.90/10.34 | % 33.90/10.34 | From (313) and (337) follows: % 33.90/10.34 | (338) ~ (times(all_0_2_2, all_0_3_3) = all_31_0_11) % 33.90/10.34 | % 33.90/10.34 | Using (48) and (338) yields: % 33.90/10.34 | (163) $false % 33.90/10.34 | % 33.90/10.34 |-The branch is then unsatisfiable % 33.90/10.34 |-Branch two: % 33.90/10.34 | (340) times(all_0_2_2, all_169_0_55) = all_31_0_11 % 33.90/10.34 | (341) all_52_0_17 = all_31_0_11 % 33.90/10.34 | % 33.90/10.34 | From (341) and (264) follows: % 33.90/10.34 | (342) times(all_31_0_11, all_0_2_2) = all_157_0_49 % 33.90/10.34 | % 33.90/10.34 | From (341) and (90) follows: % 33.90/10.34 | (343) times(all_31_0_11, all_31_0_11) = all_16_0_6 % 33.90/10.34 | % 33.90/10.34 | From (341) and (329) follows: % 33.90/10.34 | (344) times(all_31_0_11, all_8_0_4) = all_31_0_11 % 33.90/10.34 | % 33.90/10.34 | From (341) and (331) follows: % 33.90/10.34 | (345) times(all_29_0_10, all_0_3_3) = all_31_0_11 % 33.90/10.34 | % 33.90/10.34 | From (341) and (91) follows: % 33.90/10.34 | (346) times(all_0_1_1, all_8_0_4) = all_31_0_11 % 33.90/10.34 | % 33.90/10.34 +-Applying beta-rule and splitting (215), into two cases. % 33.90/10.34 |-Branch one: % 33.90/10.34 | (347) ~ (times(all_31_0_11, all_8_0_4) = all_31_0_11) % 33.90/10.34 | % 33.90/10.34 | Using (344) and (347) yields: % 33.90/10.34 | (163) $false % 33.90/10.34 | % 33.90/10.34 |-The branch is then unsatisfiable % 33.90/10.34 |-Branch two: % 33.90/10.34 | (344) times(all_31_0_11, all_8_0_4) = all_31_0_11 % 33.90/10.34 | (350) ? [v0] : (times(all_52_0_17, all_31_0_11) = v0 & times(all_8_0_4, v0) = all_16_0_6) % 33.90/10.34 | % 33.90/10.34 +-Applying beta-rule and splitting (218), into two cases. % 33.90/10.34 |-Branch one: % 33.90/10.34 | (347) ~ (times(all_31_0_11, all_8_0_4) = all_31_0_11) % 33.90/10.34 | % 33.90/10.34 | Using (344) and (347) yields: % 33.90/10.34 | (163) $false % 33.90/10.34 | % 33.90/10.34 |-The branch is then unsatisfiable % 33.90/10.34 |-Branch two: % 33.90/10.34 | (344) times(all_31_0_11, all_8_0_4) = all_31_0_11 % 33.90/10.34 | (354) ? [v0] : (times(all_8_0_4, v0) = all_29_0_10 & times(all_0_3_3, all_31_0_11) = v0) % 33.90/10.34 | % 33.90/10.34 | Instantiating (354) with all_229_0_75 yields: % 33.90/10.34 | (355) times(all_8_0_4, all_229_0_75) = all_29_0_10 & times(all_0_3_3, all_31_0_11) = all_229_0_75 % 33.90/10.34 | % 33.90/10.34 | Applying alpha-rule on (355) yields: % 33.90/10.34 | (356) times(all_8_0_4, all_229_0_75) = all_29_0_10 % 33.90/10.34 | (357) times(all_0_3_3, all_31_0_11) = all_229_0_75 % 33.90/10.34 | % 33.90/10.34 +-Applying beta-rule and splitting (228), into two cases. % 33.90/10.34 |-Branch one: % 33.90/10.34 | (358) ~ (times(all_31_0_11, all_31_0_11) = all_16_0_6) % 33.90/10.34 | % 33.90/10.34 | Using (343) and (358) yields: % 33.90/10.34 | (163) $false % 33.90/10.34 | % 33.90/10.34 |-The branch is then unsatisfiable % 33.90/10.34 |-Branch two: % 33.90/10.34 | (343) times(all_31_0_11, all_31_0_11) = all_16_0_6 % 33.90/10.34 | (361) ~ (times(all_0_1_1, all_8_0_4) = all_31_0_11) | ? [v0] : (times(all_31_0_11, all_0_1_1) = v0 & times(all_8_0_4, v0) = all_16_0_6) % 33.90/10.35 | % 33.90/10.35 +-Applying beta-rule and splitting (230), into two cases. % 33.90/10.35 |-Branch one: % 33.90/10.35 | (362) ~ (times(all_0_1_1, all_8_0_4) = all_31_0_11) % 33.90/10.35 | % 33.90/10.35 | Using (346) and (362) yields: % 33.90/10.35 | (163) $false % 33.90/10.35 | % 33.90/10.35 |-The branch is then unsatisfiable % 33.90/10.35 |-Branch two: % 33.90/10.35 | (346) times(all_0_1_1, all_8_0_4) = all_31_0_11 % 33.90/10.35 | (365) ? [v0] : (times(all_8_0_4, v0) = all_29_0_10 & times(all_0_3_3, all_0_1_1) = v0) % 33.90/10.35 | % 33.90/10.35 | Instantiating (365) with all_238_0_76 yields: % 33.90/10.35 | (366) times(all_8_0_4, all_238_0_76) = all_29_0_10 & times(all_0_3_3, all_0_1_1) = all_238_0_76 % 33.90/10.35 | % 33.90/10.35 | Applying alpha-rule on (366) yields: % 33.90/10.35 | (367) times(all_8_0_4, all_238_0_76) = all_29_0_10 % 33.90/10.35 | (368) times(all_0_3_3, all_0_1_1) = all_238_0_76 % 33.90/10.35 | % 33.90/10.35 +-Applying beta-rule and splitting (361), into two cases. % 33.90/10.35 |-Branch one: % 33.90/10.35 | (362) ~ (times(all_0_1_1, all_8_0_4) = all_31_0_11) % 33.90/10.35 | % 33.90/10.35 | Using (346) and (362) yields: % 33.90/10.35 | (163) $false % 33.90/10.35 | % 33.90/10.35 |-The branch is then unsatisfiable % 33.90/10.35 |-Branch two: % 33.90/10.35 | (346) times(all_0_1_1, all_8_0_4) = all_31_0_11 % 33.90/10.35 | (372) ? [v0] : (times(all_31_0_11, all_0_1_1) = v0 & times(all_8_0_4, v0) = all_16_0_6) % 33.90/10.35 | % 33.90/10.35 | Instantiating (372) with all_243_0_77 yields: % 33.90/10.35 | (373) times(all_31_0_11, all_0_1_1) = all_243_0_77 & times(all_8_0_4, all_243_0_77) = all_16_0_6 % 33.90/10.35 | % 33.90/10.35 | Applying alpha-rule on (373) yields: % 33.90/10.35 | (374) times(all_31_0_11, all_0_1_1) = all_243_0_77 % 33.90/10.35 | (375) times(all_8_0_4, all_243_0_77) = all_16_0_6 % 33.90/10.35 | % 33.90/10.35 +-Applying beta-rule and splitting (216), into two cases. % 33.90/10.35 |-Branch one: % 33.90/10.35 | (347) ~ (times(all_31_0_11, all_8_0_4) = all_31_0_11) % 33.90/10.35 | % 33.90/10.35 | Using (344) and (347) yields: % 33.90/10.35 | (163) $false % 33.90/10.35 | % 33.90/10.35 |-The branch is then unsatisfiable % 33.90/10.35 |-Branch two: % 33.90/10.35 | (344) times(all_31_0_11, all_8_0_4) = all_31_0_11 % 33.90/10.35 | (379) ? [v0] : (times(all_8_0_4, v0) = all_31_0_11 & times(all_8_0_4, all_31_0_11) = v0) % 33.90/10.35 | % 33.90/10.35 | Instantiating (379) with all_249_0_78 yields: % 33.90/10.35 | (380) times(all_8_0_4, all_249_0_78) = all_31_0_11 & times(all_8_0_4, all_31_0_11) = all_249_0_78 % 33.90/10.35 | % 33.90/10.35 | Applying alpha-rule on (380) yields: % 33.90/10.35 | (381) times(all_8_0_4, all_249_0_78) = all_31_0_11 % 33.90/10.35 | (382) times(all_8_0_4, all_31_0_11) = all_249_0_78 % 33.90/10.35 | % 33.90/10.35 +-Applying beta-rule and splitting (309), into two cases. % 33.90/10.35 |-Branch one: % 33.90/10.35 | (383) ~ (times(all_8_0_4, all_10_0_5) = all_74_0_28) % 33.90/10.35 | % 33.90/10.35 | Using (332) and (383) yields: % 33.90/10.35 | (163) $false % 33.90/10.35 | % 33.90/10.35 |-The branch is then unsatisfiable % 33.90/10.35 |-Branch two: % 33.90/10.35 | (332) times(all_8_0_4, all_10_0_5) = all_74_0_28 % 33.90/10.35 | (386) all_175_0_58 = all_74_0_28 % 33.90/10.35 | % 33.90/10.35 | Combining equations (310,386) yields a new equation: % 33.90/10.35 | (387) all_151_0_46 = all_74_0_28 % 33.90/10.35 | % 33.90/10.35 | Simplifying 387 yields: % 33.90/10.35 | (388) all_151_0_46 = all_74_0_28 % 33.90/10.35 | % 33.90/10.35 | From (388) and (333) follows: % 33.90/10.35 | (389) times(all_0_1_1, all_74_0_28) = all_62_0_22 % 33.90/10.35 | % 33.90/10.35 +-Applying beta-rule and splitting (229), into two cases. % 33.90/10.35 |-Branch one: % 33.90/10.35 | (362) ~ (times(all_0_1_1, all_8_0_4) = all_31_0_11) % 33.90/10.35 | % 33.90/10.35 | Using (346) and (362) yields: % 33.90/10.35 | (163) $false % 33.90/10.35 | % 33.90/10.35 |-The branch is then unsatisfiable % 33.90/10.35 |-Branch two: % 33.90/10.36 | (346) times(all_0_1_1, all_8_0_4) = all_31_0_11 % 33.90/10.36 | (393) ? [v0] : (times(all_8_0_4, v0) = all_62_0_22 & times(all_8_0_4, all_0_1_1) = v0) % 33.90/10.36 | % 33.90/10.36 | Instantiating (393) with all_262_0_79 yields: % 33.90/10.36 | (394) times(all_8_0_4, all_262_0_79) = all_62_0_22 & times(all_8_0_4, all_0_1_1) = all_262_0_79 % 33.90/10.36 | % 33.90/10.36 | Applying alpha-rule on (394) yields: % 33.90/10.36 | (395) times(all_8_0_4, all_262_0_79) = all_62_0_22 % 33.90/10.36 | (396) times(all_8_0_4, all_0_1_1) = all_262_0_79 % 33.90/10.36 | % 33.90/10.36 +-Applying beta-rule and splitting (306), into two cases. % 33.90/10.36 |-Branch one: % 33.90/10.36 | (397) ~ (times(all_29_0_10, all_8_0_4) = all_29_0_10) % 33.90/10.36 | % 33.90/10.36 | Using (330) and (397) yields: % 33.90/10.36 | (163) $false % 33.90/10.36 | % 33.90/10.36 |-The branch is then unsatisfiable % 33.90/10.36 |-Branch two: % 33.90/10.36 | (330) times(all_29_0_10, all_8_0_4) = all_29_0_10 % 33.90/10.36 | (400) all_147_0_44 = all_29_0_10 % 33.90/10.36 | % 33.90/10.36 | From (400) and (252) follows: % 33.90/10.36 | (330) times(all_29_0_10, all_8_0_4) = all_29_0_10 % 33.90/10.36 | % 33.90/10.36 +-Applying beta-rule and splitting (307), into two cases. % 33.90/10.36 |-Branch one: % 33.90/10.36 | (402) ~ (times(all_29_0_10, all_0_3_3) = all_52_0_17) % 33.90/10.36 | % 33.90/10.36 | From (341) and (402) follows: % 33.90/10.36 | (403) ~ (times(all_29_0_10, all_0_3_3) = all_31_0_11) % 33.90/10.36 | % 33.90/10.36 | Using (345) and (403) yields: % 33.90/10.36 | (163) $false % 33.90/10.36 | % 33.90/10.36 |-The branch is then unsatisfiable % 33.90/10.36 |-Branch two: % 33.90/10.36 | (331) times(all_29_0_10, all_0_3_3) = all_52_0_17 % 33.90/10.36 | (406) all_133_0_37 = all_52_0_17 % 33.90/10.36 | % 33.90/10.36 | From (341) and (331) follows: % 33.90/10.36 | (345) times(all_29_0_10, all_0_3_3) = all_31_0_11 % 33.90/10.36 | % 33.90/10.36 +-Applying beta-rule and splitting (305), into two cases. % 33.90/10.36 |-Branch one: % 33.90/10.36 | (408) ~ (times(all_31_0_11, all_8_0_4) = all_52_0_17) % 33.90/10.36 | % 33.90/10.36 | From (341) and (408) follows: % 33.90/10.36 | (347) ~ (times(all_31_0_11, all_8_0_4) = all_31_0_11) % 33.90/10.36 | % 33.90/10.36 | Using (344) and (347) yields: % 33.90/10.36 | (163) $false % 33.90/10.36 | % 33.90/10.36 |-The branch is then unsatisfiable % 33.90/10.36 |-Branch two: % 33.90/10.36 | (329) times(all_31_0_11, all_8_0_4) = all_52_0_17 % 33.90/10.36 | (412) all_62_0_22 = all_52_0_17 % 33.90/10.36 | % 33.90/10.36 | Combining equations (341,412) yields a new equation: % 33.90/10.36 | (413) all_62_0_22 = all_31_0_11 % 33.90/10.36 | % 33.90/10.36 | From (413) and (395) follows: % 33.90/10.36 | (414) times(all_8_0_4, all_262_0_79) = all_31_0_11 % 33.90/10.36 | % 33.90/10.36 | From (413) and (103) follows: % 33.90/10.36 | (47) times(all_8_0_4, all_31_0_11) = all_0_1_1 % 33.90/10.36 | % 33.90/10.36 | From (413) and (389) follows: % 33.90/10.36 | (416) times(all_0_1_1, all_74_0_28) = all_31_0_11 % 33.90/10.36 | % 33.90/10.36 | Instantiating formula (8) with all_0_1_1, all_0_1_1, all_243_0_77, all_16_0_6 and discharging atoms times(all_0_1_1, all_0_1_1) = all_16_0_6, yields: % 33.90/10.36 | (417) all_243_0_77 = all_16_0_6 | ~ (times(all_0_1_1, all_0_1_1) = all_243_0_77) % 33.90/10.36 | % 33.90/10.36 | Instantiating formula (8) with all_8_0_4, all_31_0_11, all_31_0_11, all_0_1_1 and discharging atoms times(all_8_0_4, all_31_0_11) = all_0_1_1, yields: % 33.90/10.36 | (418) all_31_0_11 = all_0_1_1 | ~ (times(all_8_0_4, all_31_0_11) = all_31_0_11) % 33.90/10.36 | % 33.90/10.36 | Instantiating formula (8) with all_8_0_4, all_31_0_11, all_249_0_78, all_0_1_1 and discharging atoms times(all_8_0_4, all_31_0_11) = all_249_0_78, times(all_8_0_4, all_31_0_11) = all_0_1_1, yields: % 33.90/10.36 | (419) all_249_0_78 = all_0_1_1 % 33.90/10.36 | % 33.90/10.36 | Instantiating formula (8) with all_8_0_4, all_0_1_1, all_262_0_79, all_31_0_11 and discharging atoms times(all_8_0_4, all_0_1_1) = all_262_0_79, yields: % 33.90/10.36 | (420) all_262_0_79 = all_31_0_11 | ~ (times(all_8_0_4, all_0_1_1) = all_31_0_11) % 33.90/10.36 | % 33.90/10.36 | Instantiating formula (8) with all_0_3_3, all_31_0_11, all_229_0_75, all_64_0_23 and discharging atoms times(all_0_3_3, all_31_0_11) = all_229_0_75, times(all_0_3_3, all_31_0_11) = all_64_0_23, yields: % 33.90/10.36 | (421) all_229_0_75 = all_64_0_23 % 33.90/10.36 | % 33.90/10.36 | Instantiating formula (8) with all_0_3_3, all_0_1_1, all_238_0_76, all_29_0_10 and discharging atoms times(all_0_3_3, all_0_1_1) = all_238_0_76, times(all_0_3_3, all_0_1_1) = all_29_0_10, yields: % 33.90/10.36 | (422) all_238_0_76 = all_29_0_10 % 33.90/10.36 | % 33.90/10.36 | Instantiating formula (8) with all_0_3_3, all_0_1_1, all_238_0_76, all_229_0_75 and discharging atoms times(all_0_3_3, all_0_1_1) = all_238_0_76, yields: % 33.90/10.36 | (423) all_238_0_76 = all_229_0_75 | ~ (times(all_0_3_3, all_0_1_1) = all_229_0_75) % 33.90/10.36 | % 33.90/10.36 | From (419) and (381) follows: % 33.90/10.36 | (424) times(all_8_0_4, all_0_1_1) = all_31_0_11 % 33.90/10.36 | % 33.90/10.36 | From (421) and (357) follows: % 33.90/10.36 | (336) times(all_0_3_3, all_31_0_11) = all_64_0_23 % 33.90/10.36 | % 33.90/10.36 +-Applying beta-rule and splitting (223), into two cases. % 33.90/10.36 |-Branch one: % 33.90/10.36 | (426) ~ (times(all_8_0_4, all_0_1_1) = all_31_0_11) % 33.90/10.36 | % 33.90/10.36 | Using (424) and (426) yields: % 33.90/10.36 | (163) $false % 33.90/10.36 | % 33.90/10.36 |-The branch is then unsatisfiable % 33.90/10.36 |-Branch two: % 33.90/10.36 | (424) times(all_8_0_4, all_0_1_1) = all_31_0_11 % 33.90/10.36 | (429) ? [v0] : (times(all_0_1_1, all_0_3_3) = v0 & times(all_0_3_3, v0) = all_31_0_11) % 33.90/10.36 | % 33.90/10.36 +-Applying beta-rule and splitting (420), into two cases. % 33.90/10.36 |-Branch one: % 33.90/10.36 | (426) ~ (times(all_8_0_4, all_0_1_1) = all_31_0_11) % 33.90/10.36 | % 33.90/10.36 | Using (424) and (426) yields: % 33.90/10.37 | (163) $false % 33.90/10.37 | % 33.90/10.37 |-The branch is then unsatisfiable % 33.90/10.37 |-Branch two: % 33.90/10.37 | (424) times(all_8_0_4, all_0_1_1) = all_31_0_11 % 33.90/10.37 | (433) all_262_0_79 = all_31_0_11 % 33.90/10.37 | % 33.90/10.37 | From (433) and (414) follows: % 33.90/10.37 | (434) times(all_8_0_4, all_31_0_11) = all_31_0_11 % 33.90/10.37 | % 33.90/10.37 +-Applying beta-rule and splitting (418), into two cases. % 33.90/10.37 |-Branch one: % 33.90/10.37 | (435) ~ (times(all_8_0_4, all_31_0_11) = all_31_0_11) % 33.90/10.37 | % 33.90/10.37 | Using (434) and (435) yields: % 33.90/10.37 | (163) $false % 33.90/10.37 | % 33.90/10.37 |-The branch is then unsatisfiable % 33.90/10.37 |-Branch two: % 33.90/10.37 | (434) times(all_8_0_4, all_31_0_11) = all_31_0_11 % 33.90/10.37 | (438) all_31_0_11 = all_0_1_1 % 33.90/10.37 | % 33.90/10.37 | From (438) and (374) follows: % 33.90/10.37 | (439) times(all_0_1_1, all_0_1_1) = all_243_0_77 % 33.90/10.37 | % 33.90/10.37 | From (438) and (342) follows: % 33.90/10.37 | (440) times(all_0_1_1, all_0_2_2) = all_157_0_49 % 33.90/10.37 | % 33.90/10.37 | From (438) and (345) follows: % 33.90/10.37 | (441) times(all_29_0_10, all_0_3_3) = all_0_1_1 % 33.90/10.37 | % 33.90/10.37 | From (438) and (416) follows: % 33.90/10.37 | (442) times(all_0_1_1, all_74_0_28) = all_0_1_1 % 33.90/10.37 | % 33.90/10.37 | From (438) and (336) follows: % 33.90/10.37 | (443) times(all_0_3_3, all_0_1_1) = all_64_0_23 % 33.90/10.37 | % 33.90/10.37 +-Applying beta-rule and splitting (423), into two cases. % 33.90/10.37 |-Branch one: % 33.90/10.37 | (444) ~ (times(all_0_3_3, all_0_1_1) = all_229_0_75) % 33.90/10.37 | % 33.90/10.37 | From (421) and (444) follows: % 33.90/10.37 | (445) ~ (times(all_0_3_3, all_0_1_1) = all_64_0_23) % 33.90/10.37 | % 33.90/10.37 | Using (443) and (445) yields: % 33.90/10.37 | (163) $false % 33.90/10.37 | % 33.90/10.37 |-The branch is then unsatisfiable % 33.90/10.37 |-Branch two: % 33.90/10.37 | (447) times(all_0_3_3, all_0_1_1) = all_229_0_75 % 33.90/10.37 | (448) all_238_0_76 = all_229_0_75 % 33.90/10.37 | % 33.90/10.37 | Combining equations (448,422) yields a new equation: % 33.90/10.37 | (449) all_229_0_75 = all_29_0_10 % 33.90/10.37 | % 33.90/10.37 | Simplifying 449 yields: % 33.90/10.37 | (450) all_229_0_75 = all_29_0_10 % 33.90/10.37 | % 33.90/10.37 | Combining equations (450,421) yields a new equation: % 33.90/10.37 | (451) all_64_0_23 = all_29_0_10 % 33.90/10.37 | % 33.90/10.37 | From (451) and (267) follows: % 33.90/10.37 | (452) times(all_29_0_10, all_10_0_5) = all_163_0_52 % 33.90/10.37 | % 33.90/10.37 | From (451) and (276) follows: % 33.90/10.37 | (453) times(all_29_0_10, all_0_2_2) = all_171_0_56 % 33.90/10.37 | % 33.90/10.37 | From (451) and (105) follows: % 33.90/10.37 | (454) times(all_29_0_10, all_10_0_5) = all_29_0_10 % 33.90/10.37 | % 33.90/10.37 +-Applying beta-rule and splitting (316), into two cases. % 33.90/10.37 |-Branch one: % 33.90/10.37 | (455) ~ (times(all_0_1_1, all_0_2_2) = all_157_0_49) % 33.90/10.37 | % 33.90/10.37 | Using (440) and (455) yields: % 33.90/10.37 | (163) $false % 33.90/10.37 | % 33.90/10.37 |-The branch is then unsatisfiable % 33.90/10.37 |-Branch two: % 33.90/10.37 | (440) times(all_0_1_1, all_0_2_2) = all_157_0_49 % 33.90/10.37 | (458) all_197_0_69 = all_157_0_49 % 33.90/10.37 | % 33.90/10.37 | From (458) and (297) follows: % 33.90/10.37 | (440) times(all_0_1_1, all_0_2_2) = all_157_0_49 % 33.90/10.37 | % 33.90/10.37 +-Applying beta-rule and splitting (417), into two cases. % 33.90/10.37 |-Branch one: % 33.90/10.37 | (460) ~ (times(all_0_1_1, all_0_1_1) = all_243_0_77) % 33.90/10.37 | % 33.90/10.37 | Using (439) and (460) yields: % 33.90/10.37 | (163) $false % 33.90/10.37 | % 33.90/10.37 |-The branch is then unsatisfiable % 33.90/10.37 |-Branch two: % 33.90/10.37 | (439) times(all_0_1_1, all_0_1_1) = all_243_0_77 % 33.90/10.37 | (463) all_243_0_77 = all_16_0_6 % 33.90/10.37 | % 33.90/10.37 | From (463) and (375) follows: % 33.90/10.37 | (464) times(all_8_0_4, all_16_0_6) = all_16_0_6 % 33.90/10.37 | % 33.90/10.37 +-Applying beta-rule and splitting (302), into two cases. % 33.90/10.37 |-Branch one: % 33.90/10.37 | (465) ~ (times(all_29_0_10, all_10_0_5) = all_163_0_52) % 33.90/10.37 | % 33.90/10.37 | Using (452) and (465) yields: % 33.90/10.37 | (163) $false % 33.90/10.37 | % 33.90/10.37 |-The branch is then unsatisfiable % 33.90/10.37 |-Branch two: % 33.90/10.37 | (452) times(all_29_0_10, all_10_0_5) = all_163_0_52 % 33.90/10.37 | (468) all_163_0_52 = all_29_0_10 | ~ (times(all_29_0_10, all_10_0_5) = all_29_0_10) % 33.90/10.37 | % 33.90/10.37 +-Applying beta-rule and splitting (468), into two cases. % 33.90/10.37 |-Branch one: % 33.90/10.37 | (469) ~ (times(all_29_0_10, all_10_0_5) = all_29_0_10) % 33.90/10.37 | % 33.90/10.37 | Using (454) and (469) yields: % 33.90/10.37 | (163) $false % 33.90/10.37 | % 33.90/10.37 |-The branch is then unsatisfiable % 33.90/10.37 |-Branch two: % 33.90/10.37 | (454) times(all_29_0_10, all_10_0_5) = all_29_0_10 % 33.90/10.37 | (472) all_163_0_52 = all_29_0_10 % 33.90/10.37 | % 33.90/10.37 | From (472) and (452) follows: % 33.90/10.37 | (454) times(all_29_0_10, all_10_0_5) = all_29_0_10 % 33.90/10.37 | % 33.90/10.37 | From (472) and (268) follows: % 33.90/10.37 | (45) times(all_0_2_2, all_29_0_10) = all_16_0_6 % 33.90/10.37 | % 33.90/10.37 +-Applying beta-rule and splitting (303), into two cases. % 33.90/10.37 |-Branch one: % 33.90/10.37 | (475) ~ (times(all_29_0_10, all_0_2_2) = all_171_0_56) % 33.90/10.37 | % 33.90/10.37 | Using (453) and (475) yields: % 33.90/10.37 | (163) $false % 33.90/10.37 | % 33.90/10.37 |-The branch is then unsatisfiable % 33.90/10.37 |-Branch two: % 33.90/10.37 | (453) times(all_29_0_10, all_0_2_2) = all_171_0_56 % 33.90/10.37 | (478) all_171_0_56 = all_74_0_28 % 33.90/10.37 | % 33.90/10.37 | From (478) and (453) follows: % 33.90/10.37 | (114) times(all_29_0_10, all_0_2_2) = all_74_0_28 % 33.90/10.37 | % 33.90/10.37 +-Applying beta-rule and splitting (220), into two cases. % 33.90/10.37 |-Branch one: % 33.90/10.37 | (469) ~ (times(all_29_0_10, all_10_0_5) = all_29_0_10) % 33.90/10.37 | % 33.90/10.37 | Using (454) and (469) yields: % 33.90/10.37 | (163) $false % 33.90/10.37 | % 33.90/10.37 |-The branch is then unsatisfiable % 33.90/10.37 |-Branch two: % 33.90/10.37 | (454) times(all_29_0_10, all_10_0_5) = all_29_0_10 % 33.90/10.37 | (483) ? [v0] : (times(all_10_0_5, v0) = all_74_0_28 & times(all_0_2_2, all_29_0_10) = v0) % 33.90/10.37 | % 33.90/10.37 | Instantiating (483) with all_342_0_81 yields: % 33.90/10.37 | (484) times(all_10_0_5, all_342_0_81) = all_74_0_28 & times(all_0_2_2, all_29_0_10) = all_342_0_81 % 33.90/10.37 | % 33.90/10.37 | Applying alpha-rule on (484) yields: % 33.90/10.37 | (485) times(all_10_0_5, all_342_0_81) = all_74_0_28 % 33.90/10.37 | (486) times(all_0_2_2, all_29_0_10) = all_342_0_81 % 33.90/10.37 | % 33.90/10.37 | Using (442) and (27) yields: % 33.90/10.37 | (487) ~ (all_74_0_28 = all_16_0_6) % 33.90/10.37 | % 33.90/10.37 | Instantiating formula (8) with all_0_2_2, all_29_0_10, all_342_0_81, all_16_0_6 and discharging atoms times(all_0_2_2, all_29_0_10) = all_342_0_81, times(all_0_2_2, all_29_0_10) = all_16_0_6, yields: % 33.90/10.37 | (488) all_342_0_81 = all_16_0_6 % 33.90/10.37 | % 33.90/10.37 | From (488) and (486) follows: % 33.90/10.37 | (45) times(all_0_2_2, all_29_0_10) = all_16_0_6 % 33.90/10.37 | % 33.90/10.37 | Instantiating formula (8) with all_8_0_4, all_16_0_6, all_74_0_28, all_16_0_6 and discharging atoms times(all_8_0_4, all_16_0_6) = all_16_0_6, yields: % 33.90/10.37 | (490) all_74_0_28 = all_16_0_6 | ~ (times(all_8_0_4, all_16_0_6) = all_74_0_28) % 33.90/10.37 | % 33.90/10.37 | Instantiating formula (4) with all_199_0_70, all_74_0_28, all_0_2_2, all_0_2_2, all_29_0_10 and discharging atoms times(all_74_0_28, all_0_2_2) = all_199_0_70, times(all_29_0_10, all_0_2_2) = all_74_0_28, yields: % 33.90/10.37 | (491) ? [v0] : (times(all_0_2_2, v0) = all_199_0_70 & times(all_0_2_2, all_29_0_10) = v0) % 33.90/10.37 | % 33.90/10.37 | Instantiating formula (4) with all_74_0_28, all_29_0_10, all_0_2_2, all_8_0_4, all_29_0_10 and discharging atoms times(all_29_0_10, all_8_0_4) = all_29_0_10, times(all_29_0_10, all_0_2_2) = all_74_0_28, yields: % 33.90/10.37 | (492) ? [v0] : (times(all_8_0_4, v0) = all_74_0_28 & times(all_0_2_2, all_29_0_10) = v0) % 33.90/10.37 | % 33.90/10.37 | Instantiating formula (4) with all_157_0_49, all_0_1_1, all_0_2_2, all_0_3_3, all_29_0_10 and discharging atoms times(all_29_0_10, all_0_3_3) = all_0_1_1, times(all_0_1_1, all_0_2_2) = all_157_0_49, yields: % 33.90/10.37 | (493) ? [v0] : (times(all_0_2_2, all_29_0_10) = v0 & times(all_0_3_3, v0) = all_157_0_49) % 33.90/10.37 | % 33.90/10.37 | Instantiating (493) with all_537_0_96 yields: % 33.90/10.37 | (494) times(all_0_2_2, all_29_0_10) = all_537_0_96 & times(all_0_3_3, all_537_0_96) = all_157_0_49 % 33.90/10.38 | % 33.90/10.38 | Applying alpha-rule on (494) yields: % 33.90/10.38 | (495) times(all_0_2_2, all_29_0_10) = all_537_0_96 % 33.90/10.38 | (496) times(all_0_3_3, all_537_0_96) = all_157_0_49 % 33.90/10.38 | % 33.90/10.38 | Instantiating (492) with all_717_0_186 yields: % 33.90/10.38 | (497) times(all_8_0_4, all_717_0_186) = all_74_0_28 & times(all_0_2_2, all_29_0_10) = all_717_0_186 % 33.90/10.38 | % 33.90/10.38 | Applying alpha-rule on (497) yields: % 33.90/10.38 | (498) times(all_8_0_4, all_717_0_186) = all_74_0_28 % 33.90/10.38 | (499) times(all_0_2_2, all_29_0_10) = all_717_0_186 % 33.90/10.38 | % 33.90/10.38 | Instantiating (491) with all_721_0_188 yields: % 33.90/10.38 | (500) times(all_0_2_2, all_721_0_188) = all_199_0_70 & times(all_0_2_2, all_29_0_10) = all_721_0_188 % 33.90/10.38 | % 33.90/10.38 | Applying alpha-rule on (500) yields: % 33.90/10.38 | (501) times(all_0_2_2, all_721_0_188) = all_199_0_70 % 33.90/10.38 | (502) times(all_0_2_2, all_29_0_10) = all_721_0_188 % 33.90/10.38 | % 33.90/10.38 | Instantiating formula (8) with all_0_2_2, all_29_0_10, all_721_0_188, all_16_0_6 and discharging atoms times(all_0_2_2, all_29_0_10) = all_721_0_188, times(all_0_2_2, all_29_0_10) = all_16_0_6, yields: % 33.90/10.38 | (503) all_721_0_188 = all_16_0_6 % 33.90/10.38 | % 33.90/10.38 | Instantiating formula (8) with all_0_2_2, all_29_0_10, all_717_0_186, all_721_0_188 and discharging atoms times(all_0_2_2, all_29_0_10) = all_721_0_188, times(all_0_2_2, all_29_0_10) = all_717_0_186, yields: % 33.90/10.38 | (504) all_721_0_188 = all_717_0_186 % 33.90/10.38 | % 33.90/10.38 | Instantiating formula (8) with all_0_2_2, all_29_0_10, all_537_0_96, all_721_0_188 and discharging atoms times(all_0_2_2, all_29_0_10) = all_721_0_188, times(all_0_2_2, all_29_0_10) = all_537_0_96, yields: % 33.90/10.38 | (505) all_721_0_188 = all_537_0_96 % 33.90/10.38 | % 33.90/10.38 | Combining equations (505,504) yields a new equation: % 33.90/10.38 | (506) all_717_0_186 = all_537_0_96 % 33.90/10.38 | % 33.90/10.38 | Combining equations (503,504) yields a new equation: % 33.90/10.38 | (507) all_717_0_186 = all_16_0_6 % 33.90/10.38 | % 33.90/10.38 | Combining equations (507,506) yields a new equation: % 33.90/10.38 | (508) all_537_0_96 = all_16_0_6 % 33.90/10.38 | % 33.90/10.38 | Combining equations (508,506) yields a new equation: % 33.90/10.38 | (507) all_717_0_186 = all_16_0_6 % 33.90/10.38 | % 33.90/10.38 | From (507) and (498) follows: % 33.90/10.38 | (510) times(all_8_0_4, all_16_0_6) = all_74_0_28 % 33.90/10.38 | % 33.90/10.38 +-Applying beta-rule and splitting (490), into two cases. % 33.90/10.38 |-Branch one: % 33.90/10.38 | (511) ~ (times(all_8_0_4, all_16_0_6) = all_74_0_28) % 33.90/10.38 | % 33.90/10.38 | Using (510) and (511) yields: % 33.90/10.38 | (163) $false % 33.90/10.38 | % 33.90/10.38 |-The branch is then unsatisfiable % 33.90/10.38 |-Branch two: % 33.90/10.38 | (510) times(all_8_0_4, all_16_0_6) = all_74_0_28 % 33.90/10.38 | (514) all_74_0_28 = all_16_0_6 % 33.90/10.38 | % 33.90/10.38 | Equations (514) can reduce 487 to: % 33.90/10.38 | (22) $false % 33.90/10.38 | % 33.90/10.38 |-The branch is then unsatisfiable % 33.90/10.38 % SZS output end Proof for theBenchmark % 33.90/10.38 % 33.90/10.38 9784ms %------------------------------------------------------------------------------