%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : KLE052+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n022.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 : Sun Jul 17 01:51:09 EDT 2022 % Result : Theorem 36.70s 11.23s % Output : Proof 45.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.14 % Problem : KLE052+1 : TPTP v8.1.0. Released v4.0.0. % 0.09/0.15 % Command : ePrincess-casc -timeout=%d %s % 0.15/0.37 % Computer : n022.cluster.edu % 0.15/0.37 % Model : x86_64 x86_64 % 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.37 % Memory : 8042.1875MB % 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.37 % CPULimit : 300 % 0.15/0.37 % WCLimit : 600 % 0.15/0.37 % DateTime : Thu Jun 16 13:45:17 EDT 2022 % 0.15/0.37 % CPUTime : % 0.64/0.64 ____ _ % 0.64/0.64 ___ / __ \_____(_)___ ________ __________ % 0.64/0.64 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.64/0.64 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.64/0.64 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.64/0.64 % 0.64/0.64 A Theorem Prover for First-Order Logic % 0.64/0.64 (ePrincess v.1.0) % 0.64/0.64 % 0.64/0.64 (c) Philipp Rümmer, 2009-2015 % 0.64/0.64 (c) Peter Backeman, 2014-2015 % 0.64/0.64 (contributions by Angelo Brillout, Peter Baumgartner) % 0.64/0.64 Free software under GNU Lesser General Public License (LGPL). % 0.64/0.64 Bug reports to peter@backeman.se % 0.64/0.64 % 0.64/0.64 For more information, visit http://user.uu.se/~petba168/breu/ % 0.64/0.64 % 0.64/0.64 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.64/0.69 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.51/1.00 Prover 0: Preprocessing ... % 2.20/1.27 Prover 0: Constructing countermodel ... % 18.44/5.98 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 18.83/6.02 Prover 1: Preprocessing ... % 19.26/6.10 Prover 1: Constructing countermodel ... % 20.29/6.37 Prover 1: gave up % 20.29/6.37 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 20.29/6.40 Prover 2: Preprocessing ... % 20.73/6.44 Prover 2: Warning: ignoring some quantifiers % 20.73/6.45 Prover 2: Constructing countermodel ... % 27.56/8.10 Prover 3: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 27.56/8.12 Prover 3: Preprocessing ... % 27.56/8.17 Prover 3: Constructing countermodel ... % 28.55/8.35 Prover 3: gave up % 28.55/8.35 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=complete % 28.55/8.36 Prover 4: Preprocessing ... % 28.87/8.40 Prover 4: Warning: ignoring some quantifiers % 28.87/8.40 Prover 4: Constructing countermodel ... % 34.96/10.63 Prover 0: stopped % 35.48/10.90 Prover 5: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 35.61/10.93 Prover 5: Preprocessing ... % 35.67/10.98 Prover 5: Constructing countermodel ... % 36.70/11.23 Prover 5: proved (329ms) % 36.70/11.23 Prover 4: stopped % 36.70/11.23 Prover 2: stopped % 36.70/11.23 % 36.70/11.23 No countermodel exists, formula is valid % 36.70/11.23 % SZS status Theorem for theBenchmark % 36.70/11.23 % 36.70/11.23 Generating proof ... found it (size 175) % 44.73/13.47 % 44.73/13.47 % SZS output start Proof for theBenchmark % 44.73/13.47 Assumed formulas after preprocessing and simplification: % 44.73/13.47 | (0) domain(zero) = zero & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v3, v2) = v4) | ~ (multiplication(v0, v1) = v3) | ? [v5] : (multiplication(v1, v2) = v5 & multiplication(v0, v5) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v3, v2) = v4) | ~ (addition(v0, v1) = v3) | ? [v5] : ? [v6] : (multiplication(v1, v2) = v6 & multiplication(v0, v2) = v5 & addition(v5, v6) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v1, v2) = v4) | ~ (multiplication(v0, v2) = v3) | ? [v5] : ? [v6] : (multiplication(v5, v2) = v6 & addition(v3, v4) = v6 & addition(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v1, v2) = v4) | ~ (addition(v0, v1) = v3) | ? [v5] : ? [v6] : (multiplication(v3, v2) = v5 & multiplication(v0, v2) = v6 & addition(v6, v4) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v1, v2) = v3) | ~ (multiplication(v0, v3) = v4) | ? [v5] : (multiplication(v5, v2) = v4 & multiplication(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v1, v2) = v3) | ~ (multiplication(v0, v1) = v4) | ? [v5] : (multiplication(v4, v2) = v5 & multiplication(v0, v3) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v0, v3) = v4) | ~ (addition(v1, v2) = v3) | ? [v5] : ? [v6] : (multiplication(v0, v2) = v6 & multiplication(v0, v1) = v5 & addition(v5, v6) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v0, v2) = v4) | ~ (multiplication(v0, v1) = v3) | ? [v5] : ? [v6] : (multiplication(v0, v5) = v6 & addition(v3, v4) = v6 & addition(v1, v2) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v0, v2) = v4) | ~ (addition(v1, v2) = v3) | ? [v5] : ? [v6] : (multiplication(v0, v3) = v5 & multiplication(v0, v1) = v6 & addition(v6, v4) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v0, v2) = v4) | ~ (addition(v0, v1) = v3) | ? [v5] : ? [v6] : (multiplication(v3, v2) = v5 & multiplication(v1, v2) = v6 & addition(v4, v6) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v0, v1) = v4) | ~ (addition(v1, v2) = v3) | ? [v5] : ? [v6] : (multiplication(v0, v3) = v5 & multiplication(v0, v2) = v6 & addition(v4, v6) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (addition(v3, v0) = v4) | ~ (addition(v2, v1) = v3) | ? [v5] : (addition(v2, v5) = v4 & addition(v1, v0) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (addition(v2, v3) = v4) | ~ (addition(v1, v0) = v3) | ? [v5] : (addition(v5, v0) = v4 & addition(v2, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (addition(v2, v1) = v4) | ~ (addition(v1, v0) = v3) | ? [v5] : (addition(v4, v0) = v5 & addition(v2, v3) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (leq(v3, v2) = v1) | ~ (leq(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (multiplication(v3, v2) = v1) | ~ (multiplication(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (addition(v3, v2) = v1) | ~ (addition(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (domain(v1) = v3) | ~ (domain(v0) = v2) | ? [v4] : ? [v5] : (domain(v4) = v5 & addition(v2, v3) = v5 & addition(v0, v1) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (domain(v1) = v2) | ~ (multiplication(v0, v2) = v3) | ? [v4] : ? [v5] : (domain(v4) = v5 & domain(v3) = v5 & multiplication(v0, v1) = v4)) & ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (addition(v0, v1) = v2) | ? [v3] : ( ~ (v3 = 0) & leq(v0, v1) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (leq(v0, v1) = v2) | ? [v3] : ( ~ (v3 = v1) & addition(v0, v1) = v3)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (domain(v2) = v1) | ~ (domain(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (multiplication(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (domain(v5) = v3 & domain(v2) = v3 & domain(v1) = v4 & multiplication(v0, v4) = v5)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (addition(v1, v0) = v2) | addition(v0, v1) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (addition(v0, v1) = v2) | addition(v1, v0) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (addition(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (domain(v2) = v3 & domain(v1) = v5 & domain(v0) = v4 & addition(v4, v5) = v3)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (multiplication(v0, one) = v1)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (multiplication(one, v0) = v1)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (addition(v0, v0) = v1)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (addition(v0, zero) = v1)) & ! [v0] : ! [v1] : (v1 = zero | ~ (multiplication(v0, zero) = v1)) & ! [v0] : ! [v1] : (v1 = zero | ~ (multiplication(zero, v0) = v1)) & ! [v0] : ! [v1] : ( ~ (domain(v0) = v1) | addition(v1, one) = one) & ! [v0] : ! [v1] : ( ~ (domain(v0) = v1) | ? [v2] : (multiplication(v1, v0) = v2 & addition(v0, v2) = v2)) & ! [v0] : ! [v1] : ( ~ (leq(v0, v1) = 0) | addition(v0, v1) = v1) & ! [v0] : ! [v1] : ( ~ (addition(v0, v1) = v1) | leq(v0, v1) = 0) & ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = v0) & domain(v0) = v1 & multiplication(v1, v0) = v2) % 44.73/13.51 | Applying alpha-rule on (0) yields: % 44.73/13.51 | (1) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (leq(v0, v1) = v2) | ? [v3] : ( ~ (v3 = v1) & addition(v0, v1) = v3)) % 44.73/13.51 | (2) ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (addition(v0, v1) = v2) | ? [v3] : ( ~ (v3 = 0) & leq(v0, v1) = v3)) % 44.73/13.51 | (3) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v0, v3) = v4) | ~ (addition(v1, v2) = v3) | ? [v5] : ? [v6] : (multiplication(v0, v2) = v6 & multiplication(v0, v1) = v5 & addition(v5, v6) = v4)) % 44.73/13.51 | (4) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v0, v2) = v4) | ~ (multiplication(v0, v1) = v3) | ? [v5] : ? [v6] : (multiplication(v0, v5) = v6 & addition(v3, v4) = v6 & addition(v1, v2) = v5)) % 44.73/13.51 | (5) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (multiplication(v3, v2) = v1) | ~ (multiplication(v3, v2) = v0)) % 44.73/13.51 | (6) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (addition(v2, v3) = v4) | ~ (addition(v1, v0) = v3) | ? [v5] : (addition(v5, v0) = v4 & addition(v2, v1) = v5)) % 44.73/13.51 | (7) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v1, v2) = v4) | ~ (multiplication(v0, v2) = v3) | ? [v5] : ? [v6] : (multiplication(v5, v2) = v6 & addition(v3, v4) = v6 & addition(v0, v1) = v5)) % 44.73/13.51 | (8) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (addition(v2, v1) = v4) | ~ (addition(v1, v0) = v3) | ? [v5] : (addition(v4, v0) = v5 & addition(v2, v3) = v5)) % 44.73/13.51 | (9) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v1, v2) = v3) | ~ (multiplication(v0, v1) = v4) | ? [v5] : (multiplication(v4, v2) = v5 & multiplication(v0, v3) = v5)) % 44.73/13.52 | (10) ! [v0] : ! [v1] : (v1 = zero | ~ (multiplication(zero, v0) = v1)) % 44.73/13.52 | (11) ! [v0] : ! [v1] : (v1 = v0 | ~ (multiplication(v0, one) = v1)) % 44.73/13.52 | (12) ! [v0] : ! [v1] : ! [v2] : ( ~ (multiplication(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (domain(v5) = v3 & domain(v2) = v3 & domain(v1) = v4 & multiplication(v0, v4) = v5)) % 44.73/13.52 | (13) domain(zero) = zero % 44.73/13.52 | (14) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v3, v2) = v4) | ~ (addition(v0, v1) = v3) | ? [v5] : ? [v6] : (multiplication(v1, v2) = v6 & multiplication(v0, v2) = v5 & addition(v5, v6) = v4)) % 44.73/13.52 | (15) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v1, v2) = v3) | ~ (multiplication(v0, v3) = v4) | ? [v5] : (multiplication(v5, v2) = v4 & multiplication(v0, v1) = v5)) % 44.73/13.52 | (16) ! [v0] : ! [v1] : ( ~ (domain(v0) = v1) | addition(v1, one) = one) % 44.73/13.52 | (17) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (addition(v3, v2) = v1) | ~ (addition(v3, v2) = v0)) % 44.73/13.52 | (18) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (domain(v1) = v2) | ~ (multiplication(v0, v2) = v3) | ? [v4] : ? [v5] : (domain(v4) = v5 & domain(v3) = v5 & multiplication(v0, v1) = v4)) % 44.73/13.52 | (19) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (domain(v1) = v3) | ~ (domain(v0) = v2) | ? [v4] : ? [v5] : (domain(v4) = v5 & addition(v2, v3) = v5 & addition(v0, v1) = v4)) % 44.73/13.52 | (20) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (addition(v3, v0) = v4) | ~ (addition(v2, v1) = v3) | ? [v5] : (addition(v2, v5) = v4 & addition(v1, v0) = v5)) % 44.73/13.52 | (21) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = v0) & domain(v0) = v1 & multiplication(v1, v0) = v2) % 44.73/13.52 | (22) ! [v0] : ! [v1] : (v1 = zero | ~ (multiplication(v0, zero) = v1)) % 44.73/13.52 | (23) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (domain(v2) = v1) | ~ (domain(v2) = v0)) % 44.73/13.52 | (24) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v3, v2) = v4) | ~ (multiplication(v0, v1) = v3) | ? [v5] : (multiplication(v1, v2) = v5 & multiplication(v0, v5) = v4)) % 44.73/13.52 | (25) ! [v0] : ! [v1] : ! [v2] : ( ~ (addition(v0, v1) = v2) | addition(v1, v0) = v2) % 44.73/13.52 | (26) ! [v0] : ! [v1] : ! [v2] : ( ~ (addition(v1, v0) = v2) | addition(v0, v1) = v2) % 44.73/13.52 | (27) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v1, v2) = v4) | ~ (addition(v0, v1) = v3) | ? [v5] : ? [v6] : (multiplication(v3, v2) = v5 & multiplication(v0, v2) = v6 & addition(v6, v4) = v5)) % 44.73/13.52 | (28) ! [v0] : ! [v1] : (v1 = v0 | ~ (addition(v0, v0) = v1)) % 44.73/13.52 | (29) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v0, v2) = v4) | ~ (addition(v0, v1) = v3) | ? [v5] : ? [v6] : (multiplication(v3, v2) = v5 & multiplication(v1, v2) = v6 & addition(v4, v6) = v5)) % 45.16/13.52 | (30) ! [v0] : ! [v1] : ( ~ (addition(v0, v1) = v1) | leq(v0, v1) = 0) % 45.16/13.52 | (31) ! [v0] : ! [v1] : ( ~ (leq(v0, v1) = 0) | addition(v0, v1) = v1) % 45.16/13.52 | (32) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v0, v2) = v4) | ~ (addition(v1, v2) = v3) | ? [v5] : ? [v6] : (multiplication(v0, v3) = v5 & multiplication(v0, v1) = v6 & addition(v6, v4) = v5)) % 45.16/13.52 | (33) ! [v0] : ! [v1] : (v1 = v0 | ~ (multiplication(one, v0) = v1)) % 45.16/13.52 | (34) ! [v0] : ! [v1] : (v1 = v0 | ~ (addition(v0, zero) = v1)) % 45.16/13.52 | (35) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v0, v1) = v4) | ~ (addition(v1, v2) = v3) | ? [v5] : ? [v6] : (multiplication(v0, v3) = v5 & multiplication(v0, v2) = v6 & addition(v4, v6) = v5)) % 45.16/13.52 | (36) ! [v0] : ! [v1] : ( ~ (domain(v0) = v1) | ? [v2] : (multiplication(v1, v0) = v2 & addition(v0, v2) = v2)) % 45.16/13.52 | (37) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (leq(v3, v2) = v1) | ~ (leq(v3, v2) = v0)) % 45.16/13.52 | (38) ! [v0] : ! [v1] : ! [v2] : ( ~ (addition(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (domain(v2) = v3 & domain(v1) = v5 & domain(v0) = v4 & addition(v4, v5) = v3)) % 45.16/13.52 | % 45.16/13.52 | Instantiating (21) with all_2_0_0, all_2_1_1, all_2_2_2 yields: % 45.16/13.52 | (39) ~ (all_2_0_0 = all_2_2_2) & domain(all_2_2_2) = all_2_1_1 & multiplication(all_2_1_1, all_2_2_2) = all_2_0_0 % 45.16/13.53 | % 45.16/13.53 | Applying alpha-rule on (39) yields: % 45.16/13.53 | (40) ~ (all_2_0_0 = all_2_2_2) % 45.16/13.53 | (41) domain(all_2_2_2) = all_2_1_1 % 45.16/13.53 | (42) multiplication(all_2_1_1, all_2_2_2) = all_2_0_0 % 45.16/13.53 | % 45.16/13.53 | Instantiating formula (33) with all_2_0_0, all_2_2_2 yields: % 45.16/13.53 | (43) all_2_0_0 = all_2_2_2 | ~ (multiplication(one, all_2_2_2) = all_2_0_0) % 45.16/13.53 | % 45.16/13.53 | Instantiating formula (16) with all_2_1_1, all_2_2_2 and discharging atoms domain(all_2_2_2) = all_2_1_1, yields: % 45.16/13.53 | (44) addition(all_2_1_1, one) = one % 45.16/13.53 | % 45.16/13.53 | Instantiating formula (36) with all_2_1_1, all_2_2_2 and discharging atoms domain(all_2_2_2) = all_2_1_1, yields: % 45.16/13.53 | (45) ? [v0] : (multiplication(all_2_1_1, all_2_2_2) = v0 & addition(all_2_2_2, v0) = v0) % 45.16/13.53 | % 45.16/13.53 | Instantiating formula (19) with zero, all_2_1_1, zero, all_2_2_2 and discharging atoms domain(all_2_2_2) = all_2_1_1, domain(zero) = zero, yields: % 45.16/13.53 | (46) ? [v0] : ? [v1] : (domain(v0) = v1 & addition(all_2_1_1, zero) = v1 & addition(all_2_2_2, zero) = v0) % 45.16/13.53 | % 45.16/13.53 | Instantiating formula (19) with all_2_1_1, zero, all_2_2_2, zero and discharging atoms domain(all_2_2_2) = all_2_1_1, domain(zero) = zero, yields: % 45.16/13.53 | (47) ? [v0] : ? [v1] : (domain(v0) = v1 & addition(zero, all_2_1_1) = v1 & addition(zero, all_2_2_2) = v0) % 45.16/13.53 | % 45.16/13.53 | Instantiating formula (7) with all_2_0_0, all_2_0_0, all_2_2_2, all_2_1_1, all_2_1_1 and discharging atoms multiplication(all_2_1_1, all_2_2_2) = all_2_0_0, yields: % 45.16/13.53 | (48) ? [v0] : ? [v1] : (multiplication(v0, all_2_2_2) = v1 & addition(all_2_0_0, all_2_0_0) = v1 & addition(all_2_1_1, all_2_1_1) = v0) % 45.16/13.53 | % 45.16/13.53 | Instantiating formula (4) with all_2_0_0, all_2_0_0, all_2_2_2, all_2_2_2, all_2_1_1 and discharging atoms multiplication(all_2_1_1, all_2_2_2) = all_2_0_0, yields: % 45.16/13.53 | (49) ? [v0] : ? [v1] : (multiplication(all_2_1_1, v0) = v1 & addition(all_2_0_0, all_2_0_0) = v1 & addition(all_2_2_2, all_2_2_2) = v0) % 45.16/13.53 | % 45.16/13.53 | Instantiating formula (12) with all_2_0_0, all_2_2_2, all_2_1_1 and discharging atoms multiplication(all_2_1_1, all_2_2_2) = all_2_0_0, yields: % 45.16/13.53 | (50) ? [v0] : ? [v1] : ? [v2] : (domain(v2) = v0 & domain(all_2_0_0) = v0 & domain(all_2_2_2) = v1 & multiplication(all_2_1_1, v1) = v2) % 45.16/13.53 | % 45.16/13.53 | Instantiating (50) with all_10_0_3, all_10_1_4, all_10_2_5 yields: % 45.16/13.53 | (51) domain(all_10_0_3) = all_10_2_5 & domain(all_2_0_0) = all_10_2_5 & domain(all_2_2_2) = all_10_1_4 & multiplication(all_2_1_1, all_10_1_4) = all_10_0_3 % 45.16/13.53 | % 45.16/13.53 | Applying alpha-rule on (51) yields: % 45.16/13.53 | (52) domain(all_10_0_3) = all_10_2_5 % 45.16/13.53 | (53) domain(all_2_0_0) = all_10_2_5 % 45.16/13.53 | (54) domain(all_2_2_2) = all_10_1_4 % 45.16/13.53 | (55) multiplication(all_2_1_1, all_10_1_4) = all_10_0_3 % 45.16/13.53 | % 45.16/13.53 | Instantiating (46) with all_12_0_6, all_12_1_7 yields: % 45.16/13.53 | (56) domain(all_12_1_7) = all_12_0_6 & addition(all_2_1_1, zero) = all_12_0_6 & addition(all_2_2_2, zero) = all_12_1_7 % 45.16/13.53 | % 45.16/13.53 | Applying alpha-rule on (56) yields: % 45.16/13.53 | (57) domain(all_12_1_7) = all_12_0_6 % 45.16/13.53 | (58) addition(all_2_1_1, zero) = all_12_0_6 % 45.16/13.53 | (59) addition(all_2_2_2, zero) = all_12_1_7 % 45.16/13.53 | % 45.16/13.53 | Instantiating (49) with all_14_0_8, all_14_1_9 yields: % 45.16/13.53 | (60) multiplication(all_2_1_1, all_14_1_9) = all_14_0_8 & addition(all_2_0_0, all_2_0_0) = all_14_0_8 & addition(all_2_2_2, all_2_2_2) = all_14_1_9 % 45.16/13.53 | % 45.16/13.53 | Applying alpha-rule on (60) yields: % 45.16/13.53 | (61) multiplication(all_2_1_1, all_14_1_9) = all_14_0_8 % 45.16/13.53 | (62) addition(all_2_0_0, all_2_0_0) = all_14_0_8 % 45.16/13.53 | (63) addition(all_2_2_2, all_2_2_2) = all_14_1_9 % 45.16/13.53 | % 45.16/13.53 | Instantiating (48) with all_16_0_10, all_16_1_11 yields: % 45.16/13.53 | (64) multiplication(all_16_1_11, all_2_2_2) = all_16_0_10 & addition(all_2_0_0, all_2_0_0) = all_16_0_10 & addition(all_2_1_1, all_2_1_1) = all_16_1_11 % 45.16/13.53 | % 45.16/13.53 | Applying alpha-rule on (64) yields: % 45.16/13.53 | (65) multiplication(all_16_1_11, all_2_2_2) = all_16_0_10 % 45.16/13.53 | (66) addition(all_2_0_0, all_2_0_0) = all_16_0_10 % 45.16/13.53 | (67) addition(all_2_1_1, all_2_1_1) = all_16_1_11 % 45.16/13.53 | % 45.16/13.53 | Instantiating (45) with all_18_0_12 yields: % 45.16/13.53 | (68) multiplication(all_2_1_1, all_2_2_2) = all_18_0_12 & addition(all_2_2_2, all_18_0_12) = all_18_0_12 % 45.16/13.53 | % 45.16/13.53 | Applying alpha-rule on (68) yields: % 45.16/13.53 | (69) multiplication(all_2_1_1, all_2_2_2) = all_18_0_12 % 45.16/13.53 | (70) addition(all_2_2_2, all_18_0_12) = all_18_0_12 % 45.16/13.53 | % 45.16/13.53 | Instantiating (47) with all_26_0_18, all_26_1_19 yields: % 45.16/13.53 | (71) domain(all_26_1_19) = all_26_0_18 & addition(zero, all_2_1_1) = all_26_0_18 & addition(zero, all_2_2_2) = all_26_1_19 % 45.16/13.53 | % 45.16/13.53 | Applying alpha-rule on (71) yields: % 45.16/13.53 | (72) domain(all_26_1_19) = all_26_0_18 % 45.16/13.53 | (73) addition(zero, all_2_1_1) = all_26_0_18 % 45.16/13.53 | (74) addition(zero, all_2_2_2) = all_26_1_19 % 45.16/13.53 | % 45.16/13.53 +-Applying beta-rule and splitting (43), into two cases. % 45.16/13.53 |-Branch one: % 45.16/13.53 | (75) ~ (multiplication(one, all_2_2_2) = all_2_0_0) % 45.16/13.53 | % 45.16/13.53 | Instantiating formula (23) with all_2_2_2, all_10_1_4, all_2_1_1 and discharging atoms domain(all_2_2_2) = all_10_1_4, domain(all_2_2_2) = all_2_1_1, yields: % 45.16/13.53 | (76) all_10_1_4 = all_2_1_1 % 45.16/13.53 | % 45.16/13.53 | Instantiating formula (23) with all_2_2_2, all_10_1_4, all_26_0_18 and discharging atoms domain(all_2_2_2) = all_10_1_4, yields: % 45.16/13.53 | (77) all_26_0_18 = all_10_1_4 | ~ (domain(all_2_2_2) = all_26_0_18) % 45.16/13.53 | % 45.16/13.53 | Instantiating formula (5) with all_2_1_1, all_2_2_2, all_18_0_12, all_2_0_0 and discharging atoms multiplication(all_2_1_1, all_2_2_2) = all_18_0_12, multiplication(all_2_1_1, all_2_2_2) = all_2_0_0, yields: % 45.16/13.53 | (78) all_18_0_12 = all_2_0_0 % 45.16/13.53 | % 45.16/13.53 | Instantiating formula (28) with all_16_0_10, all_2_0_0 and discharging atoms addition(all_2_0_0, all_2_0_0) = all_16_0_10, yields: % 45.16/13.53 | (79) all_16_0_10 = all_2_0_0 % 45.16/13.53 | % 45.16/13.53 | Instantiating formula (17) with all_2_0_0, all_2_0_0, all_14_0_8, all_16_0_10 and discharging atoms addition(all_2_0_0, all_2_0_0) = all_16_0_10, addition(all_2_0_0, all_2_0_0) = all_14_0_8, yields: % 45.16/13.53 | (80) all_16_0_10 = all_14_0_8 % 45.16/13.53 | % 45.16/13.53 | Instantiating formula (34) with all_12_0_6, all_2_1_1 and discharging atoms addition(all_2_1_1, zero) = all_12_0_6, yields: % 45.16/13.53 | (81) all_12_0_6 = all_2_1_1 % 45.16/13.53 | % 45.16/13.53 | Instantiating formula (34) with all_12_1_7, all_2_2_2 and discharging atoms addition(all_2_2_2, zero) = all_12_1_7, yields: % 45.16/13.53 | (82) all_12_1_7 = all_2_2_2 % 45.16/13.53 | % 45.16/13.54 | Instantiating formula (17) with zero, all_2_2_2, all_26_1_19, all_2_2_2 and discharging atoms addition(zero, all_2_2_2) = all_26_1_19, yields: % 45.16/13.54 | (83) all_26_1_19 = all_2_2_2 | ~ (addition(zero, all_2_2_2) = all_2_2_2) % 45.16/13.54 | % 45.16/13.54 | Combining equations (79,80) yields a new equation: % 45.16/13.54 | (84) all_14_0_8 = all_2_0_0 % 45.16/13.54 | % 45.16/13.54 | From (76) and (54) follows: % 45.16/13.54 | (41) domain(all_2_2_2) = all_2_1_1 % 45.16/13.54 | % 45.16/13.54 | From (76) and (55) follows: % 45.16/13.54 | (86) multiplication(all_2_1_1, all_2_1_1) = all_10_0_3 % 45.16/13.54 | % 45.16/13.54 | From (78) and (69) follows: % 45.16/13.54 | (42) multiplication(all_2_1_1, all_2_2_2) = all_2_0_0 % 45.16/13.54 | % 45.16/13.54 | From (84) and (62) follows: % 45.16/13.54 | (88) addition(all_2_0_0, all_2_0_0) = all_2_0_0 % 45.16/13.54 | % 45.16/13.54 | From (81) and (58) follows: % 45.16/13.54 | (89) addition(all_2_1_1, zero) = all_2_1_1 % 45.16/13.54 | % 45.16/13.54 | From (78)(78) and (70) follows: % 45.16/13.54 | (90) addition(all_2_2_2, all_2_0_0) = all_2_0_0 % 45.16/13.54 | % 45.16/13.54 | From (82) and (59) follows: % 45.16/13.54 | (91) addition(all_2_2_2, zero) = all_2_2_2 % 45.16/13.54 | % 45.16/13.54 | Instantiating formula (36) with all_26_0_18, all_26_1_19 and discharging atoms domain(all_26_1_19) = all_26_0_18, yields: % 45.16/13.54 | (92) ? [v0] : (multiplication(all_26_0_18, all_26_1_19) = v0 & addition(all_26_1_19, v0) = v0) % 45.16/13.54 | % 45.16/13.54 | Instantiating formula (19) with all_2_1_1, all_10_2_5, all_2_2_2, all_2_0_0 and discharging atoms domain(all_2_0_0) = all_10_2_5, domain(all_2_2_2) = all_2_1_1, yields: % 45.16/13.54 | (93) ? [v0] : ? [v1] : (domain(v0) = v1 & addition(all_10_2_5, all_2_1_1) = v1 & addition(all_2_0_0, all_2_2_2) = v0) % 45.16/13.54 | % 45.16/13.54 | Instantiating formula (19) with all_26_0_18, all_10_2_5, all_26_1_19, all_2_0_0 and discharging atoms domain(all_26_1_19) = all_26_0_18, domain(all_2_0_0) = all_10_2_5, yields: % 45.16/13.54 | (94) ? [v0] : ? [v1] : (domain(v0) = v1 & addition(all_10_2_5, all_26_0_18) = v1 & addition(all_2_0_0, all_26_1_19) = v0) % 45.16/13.54 | % 45.16/13.54 | Instantiating formula (18) with all_10_0_3, all_2_1_1, all_26_1_19, all_2_1_1 and discharging atoms multiplication(all_2_1_1, all_2_1_1) = all_10_0_3, yields: % 45.16/13.54 | (95) ~ (domain(all_26_1_19) = all_2_1_1) | ? [v0] : ? [v1] : (domain(v0) = v1 & domain(all_10_0_3) = v1 & multiplication(all_2_1_1, all_26_1_19) = v0) % 45.16/13.54 | % 45.16/13.54 | Instantiating formula (29) with all_2_0_0, one, all_2_2_2, one, all_2_1_1 and discharging atoms multiplication(all_2_1_1, all_2_2_2) = all_2_0_0, addition(all_2_1_1, one) = one, yields: % 45.16/13.54 | (96) ? [v0] : ? [v1] : (multiplication(one, all_2_2_2) = v1 & multiplication(one, all_2_2_2) = v0 & addition(all_2_0_0, v1) = v0) % 45.16/13.54 | % 45.16/13.54 | Instantiating formula (14) with all_2_0_0, all_2_1_1, all_2_2_2, zero, all_2_1_1 and discharging atoms multiplication(all_2_1_1, all_2_2_2) = all_2_0_0, addition(all_2_1_1, zero) = all_2_1_1, yields: % 45.16/13.54 | (97) ? [v0] : ? [v1] : (multiplication(all_2_1_1, all_2_2_2) = v0 & multiplication(zero, all_2_2_2) = v1 & addition(v0, v1) = all_2_0_0) % 45.16/13.54 | % 45.16/13.54 | Instantiating formula (29) with all_2_0_0, all_2_1_1, all_2_2_2, zero, all_2_1_1 and discharging atoms multiplication(all_2_1_1, all_2_2_2) = all_2_0_0, addition(all_2_1_1, zero) = all_2_1_1, yields: % 45.16/13.54 | (98) ? [v0] : ? [v1] : (multiplication(all_2_1_1, all_2_2_2) = v0 & multiplication(zero, all_2_2_2) = v1 & addition(all_2_0_0, v1) = v0) % 45.16/13.54 | % 45.16/13.54 | Instantiating formula (6) with all_2_0_0, all_2_0_0, all_2_0_0, all_2_2_2, all_2_0_0 and discharging atoms addition(all_2_0_0, all_2_0_0) = all_2_0_0, addition(all_2_2_2, all_2_0_0) = all_2_0_0, yields: % 45.16/13.54 | (99) ? [v0] : (addition(v0, all_2_0_0) = all_2_0_0 & addition(all_2_0_0, all_2_2_2) = v0) % 45.16/13.54 | % 45.16/13.54 | Instantiating formula (26) with all_2_0_0, all_2_2_2, all_2_0_0 and discharging atoms addition(all_2_2_2, all_2_0_0) = all_2_0_0, yields: % 45.16/13.54 | (100) addition(all_2_0_0, all_2_2_2) = all_2_0_0 % 45.16/13.54 | % 45.16/13.54 | Instantiating formula (3) with all_2_0_0, all_2_2_2, zero, all_2_2_2, all_2_1_1 and discharging atoms multiplication(all_2_1_1, all_2_2_2) = all_2_0_0, addition(all_2_2_2, zero) = all_2_2_2, yields: % 45.16/13.54 | (101) ? [v0] : ? [v1] : (multiplication(all_2_1_1, all_2_2_2) = v0 & multiplication(all_2_1_1, zero) = v1 & addition(v0, v1) = all_2_0_0) % 45.16/13.54 | % 45.16/13.54 | Instantiating formula (35) with all_2_0_0, all_2_2_2, zero, all_2_2_2, all_2_1_1 and discharging atoms multiplication(all_2_1_1, all_2_2_2) = all_2_0_0, addition(all_2_2_2, zero) = all_2_2_2, yields: % 45.16/13.54 | (102) ? [v0] : ? [v1] : (multiplication(all_2_1_1, all_2_2_2) = v0 & multiplication(all_2_1_1, zero) = v1 & addition(all_2_0_0, v1) = v0) % 45.16/13.54 | % 45.16/13.54 | Instantiating formula (26) with all_2_2_2, all_2_2_2, zero and discharging atoms addition(all_2_2_2, zero) = all_2_2_2, yields: % 45.16/13.54 | (103) addition(zero, all_2_2_2) = all_2_2_2 % 45.16/13.54 | % 45.16/13.54 | Instantiating formula (14) with all_2_0_0, all_2_1_1, all_2_2_2, all_2_1_1, zero and discharging atoms multiplication(all_2_1_1, all_2_2_2) = all_2_0_0, yields: % 45.16/13.54 | (104) ~ (addition(zero, all_2_1_1) = all_2_1_1) | ? [v0] : ? [v1] : (multiplication(all_2_1_1, all_2_2_2) = v1 & multiplication(zero, all_2_2_2) = v0 & addition(v0, v1) = all_2_0_0) % 45.16/13.54 | % 45.16/13.54 | Instantiating formula (27) with all_2_0_0, all_26_0_18, all_2_2_2, all_2_1_1, zero and discharging atoms multiplication(all_2_1_1, all_2_2_2) = all_2_0_0, addition(zero, all_2_1_1) = all_26_0_18, yields: % 45.16/13.54 | (105) ? [v0] : ? [v1] : (multiplication(all_26_0_18, all_2_2_2) = v0 & multiplication(zero, all_2_2_2) = v1 & addition(v1, all_2_0_0) = v0) % 45.16/13.54 | % 45.16/13.54 | Instantiating formula (14) with all_10_0_3, all_2_1_1, all_2_1_1, all_2_1_1, zero and discharging atoms multiplication(all_2_1_1, all_2_1_1) = all_10_0_3, yields: % 45.16/13.54 | (106) ~ (addition(zero, all_2_1_1) = all_2_1_1) | ? [v0] : ? [v1] : (multiplication(all_2_1_1, all_2_1_1) = v1 & multiplication(zero, all_2_1_1) = v0 & addition(v0, v1) = all_10_0_3) % 45.16/13.54 | % 45.16/13.54 | Instantiating formula (3) with all_2_0_0, all_2_2_2, all_2_2_2, zero, all_2_1_1 and discharging atoms multiplication(all_2_1_1, all_2_2_2) = all_2_0_0, yields: % 45.16/13.54 | (107) ~ (addition(zero, all_2_2_2) = all_2_2_2) | ? [v0] : ? [v1] : (multiplication(all_2_1_1, all_2_2_2) = v1 & multiplication(all_2_1_1, zero) = v0 & addition(v0, v1) = all_2_0_0) % 45.16/13.54 | % 45.16/13.54 | Instantiating formula (32) with all_2_0_0, all_26_1_19, all_2_2_2, zero, all_2_1_1 and discharging atoms multiplication(all_2_1_1, all_2_2_2) = all_2_0_0, addition(zero, all_2_2_2) = all_26_1_19, yields: % 45.16/13.54 | (108) ? [v0] : ? [v1] : (multiplication(all_2_1_1, all_26_1_19) = v0 & multiplication(all_2_1_1, zero) = v1 & addition(v1, all_2_0_0) = v0) % 45.16/13.54 | % 45.16/13.54 | Instantiating formula (30) with all_2_2_2, zero yields: % 45.16/13.54 | (109) ~ (addition(zero, all_2_2_2) = all_2_2_2) | leq(zero, all_2_2_2) = 0 % 45.16/13.54 | % 45.16/13.54 | Instantiating (94) with all_64_0_41, all_64_1_42 yields: % 45.16/13.54 | (110) domain(all_64_1_42) = all_64_0_41 & addition(all_10_2_5, all_26_0_18) = all_64_0_41 & addition(all_2_0_0, all_26_1_19) = all_64_1_42 % 45.16/13.54 | % 45.16/13.54 | Applying alpha-rule on (110) yields: % 45.16/13.54 | (111) domain(all_64_1_42) = all_64_0_41 % 45.16/13.55 | (112) addition(all_10_2_5, all_26_0_18) = all_64_0_41 % 45.16/13.55 | (113) addition(all_2_0_0, all_26_1_19) = all_64_1_42 % 45.16/13.55 | % 45.16/13.55 | Instantiating (92) with all_68_0_45 yields: % 45.16/13.55 | (114) multiplication(all_26_0_18, all_26_1_19) = all_68_0_45 & addition(all_26_1_19, all_68_0_45) = all_68_0_45 % 45.16/13.55 | % 45.16/13.55 | Applying alpha-rule on (114) yields: % 45.16/13.55 | (115) multiplication(all_26_0_18, all_26_1_19) = all_68_0_45 % 45.16/13.55 | (116) addition(all_26_1_19, all_68_0_45) = all_68_0_45 % 45.16/13.55 | % 45.16/13.55 | Instantiating (98) with all_80_0_55, all_80_1_56 yields: % 45.16/13.55 | (117) multiplication(all_2_1_1, all_2_2_2) = all_80_1_56 & multiplication(zero, all_2_2_2) = all_80_0_55 & addition(all_2_0_0, all_80_0_55) = all_80_1_56 % 45.16/13.55 | % 45.16/13.55 | Applying alpha-rule on (117) yields: % 45.16/13.55 | (118) multiplication(all_2_1_1, all_2_2_2) = all_80_1_56 % 45.16/13.55 | (119) multiplication(zero, all_2_2_2) = all_80_0_55 % 45.16/13.55 | (120) addition(all_2_0_0, all_80_0_55) = all_80_1_56 % 45.16/13.55 | % 45.16/13.55 | Instantiating (96) with all_118_0_85, all_118_1_86 yields: % 45.16/13.55 | (121) multiplication(one, all_2_2_2) = all_118_0_85 & multiplication(one, all_2_2_2) = all_118_1_86 & addition(all_2_0_0, all_118_0_85) = all_118_1_86 % 45.16/13.55 | % 45.16/13.55 | Applying alpha-rule on (121) yields: % 45.16/13.55 | (122) multiplication(one, all_2_2_2) = all_118_0_85 % 45.16/13.55 | (123) multiplication(one, all_2_2_2) = all_118_1_86 % 45.16/13.55 | (124) addition(all_2_0_0, all_118_0_85) = all_118_1_86 % 45.16/13.55 | % 45.16/13.55 | Instantiating (105) with all_130_0_97, all_130_1_98 yields: % 45.16/13.55 | (125) multiplication(all_26_0_18, all_2_2_2) = all_130_1_98 & multiplication(zero, all_2_2_2) = all_130_0_97 & addition(all_130_0_97, all_2_0_0) = all_130_1_98 % 45.16/13.55 | % 45.16/13.55 | Applying alpha-rule on (125) yields: % 45.16/13.55 | (126) multiplication(all_26_0_18, all_2_2_2) = all_130_1_98 % 45.16/13.55 | (127) multiplication(zero, all_2_2_2) = all_130_0_97 % 45.16/13.55 | (128) addition(all_130_0_97, all_2_0_0) = all_130_1_98 % 45.16/13.55 | % 45.16/13.55 | Instantiating (99) with all_134_0_100 yields: % 45.16/13.55 | (129) addition(all_134_0_100, all_2_0_0) = all_2_0_0 & addition(all_2_0_0, all_2_2_2) = all_134_0_100 % 45.16/13.55 | % 45.16/13.55 | Applying alpha-rule on (129) yields: % 45.16/13.55 | (130) addition(all_134_0_100, all_2_0_0) = all_2_0_0 % 45.16/13.55 | (131) addition(all_2_0_0, all_2_2_2) = all_134_0_100 % 45.16/13.55 | % 45.16/13.55 | Instantiating (108) with all_142_0_109, all_142_1_110 yields: % 45.16/13.55 | (132) multiplication(all_2_1_1, all_26_1_19) = all_142_1_110 & multiplication(all_2_1_1, zero) = all_142_0_109 & addition(all_142_0_109, all_2_0_0) = all_142_1_110 % 45.16/13.55 | % 45.16/13.55 | Applying alpha-rule on (132) yields: % 45.16/13.55 | (133) multiplication(all_2_1_1, all_26_1_19) = all_142_1_110 % 45.16/13.55 | (134) multiplication(all_2_1_1, zero) = all_142_0_109 % 45.16/13.55 | (135) addition(all_142_0_109, all_2_0_0) = all_142_1_110 % 45.16/13.55 | % 45.16/13.55 | Instantiating (102) with all_170_0_127, all_170_1_128 yields: % 45.16/13.55 | (136) multiplication(all_2_1_1, all_2_2_2) = all_170_1_128 & multiplication(all_2_1_1, zero) = all_170_0_127 & addition(all_2_0_0, all_170_0_127) = all_170_1_128 % 45.16/13.55 | % 45.16/13.55 | Applying alpha-rule on (136) yields: % 45.16/13.55 | (137) multiplication(all_2_1_1, all_2_2_2) = all_170_1_128 % 45.16/13.55 | (138) multiplication(all_2_1_1, zero) = all_170_0_127 % 45.16/13.55 | (139) addition(all_2_0_0, all_170_0_127) = all_170_1_128 % 45.16/13.55 | % 45.16/13.55 | Instantiating (101) with all_182_0_138, all_182_1_139 yields: % 45.16/13.55 | (140) multiplication(all_2_1_1, all_2_2_2) = all_182_1_139 & multiplication(all_2_1_1, zero) = all_182_0_138 & addition(all_182_1_139, all_182_0_138) = all_2_0_0 % 45.16/13.55 | % 45.16/13.55 | Applying alpha-rule on (140) yields: % 45.16/13.55 | (141) multiplication(all_2_1_1, all_2_2_2) = all_182_1_139 % 45.16/13.55 | (142) multiplication(all_2_1_1, zero) = all_182_0_138 % 45.16/13.55 | (143) addition(all_182_1_139, all_182_0_138) = all_2_0_0 % 45.16/13.55 | % 45.16/13.55 | Instantiating (97) with all_184_0_140, all_184_1_141 yields: % 45.16/13.55 | (144) multiplication(all_2_1_1, all_2_2_2) = all_184_1_141 & multiplication(zero, all_2_2_2) = all_184_0_140 & addition(all_184_1_141, all_184_0_140) = all_2_0_0 % 45.16/13.55 | % 45.16/13.55 | Applying alpha-rule on (144) yields: % 45.16/13.55 | (145) multiplication(all_2_1_1, all_2_2_2) = all_184_1_141 % 45.16/13.55 | (146) multiplication(zero, all_2_2_2) = all_184_0_140 % 45.16/13.55 | (147) addition(all_184_1_141, all_184_0_140) = all_2_0_0 % 45.16/13.55 | % 45.16/13.55 | Instantiating (93) with all_200_0_156, all_200_1_157 yields: % 45.16/13.55 | (148) domain(all_200_1_157) = all_200_0_156 & addition(all_10_2_5, all_2_1_1) = all_200_0_156 & addition(all_2_0_0, all_2_2_2) = all_200_1_157 % 45.16/13.55 | % 45.16/13.55 | Applying alpha-rule on (148) yields: % 45.16/13.55 | (149) domain(all_200_1_157) = all_200_0_156 % 45.16/13.55 | (150) addition(all_10_2_5, all_2_1_1) = all_200_0_156 % 45.16/13.55 | (151) addition(all_2_0_0, all_2_2_2) = all_200_1_157 % 45.16/13.55 | % 45.16/13.55 +-Applying beta-rule and splitting (107), into two cases. % 45.16/13.55 |-Branch one: % 45.16/13.55 | (152) ~ (addition(zero, all_2_2_2) = all_2_2_2) % 45.16/13.55 | % 45.16/13.55 | Using (103) and (152) yields: % 45.16/13.55 | (153) $false % 45.16/13.55 | % 45.16/13.55 |-The branch is then unsatisfiable % 45.16/13.55 |-Branch two: % 45.16/13.55 | (103) addition(zero, all_2_2_2) = all_2_2_2 % 45.16/13.55 | (155) ? [v0] : ? [v1] : (multiplication(all_2_1_1, all_2_2_2) = v1 & multiplication(all_2_1_1, zero) = v0 & addition(v0, v1) = all_2_0_0) % 45.16/13.55 | % 45.16/13.55 | Instantiating (155) with all_232_0_181, all_232_1_182 yields: % 45.16/13.55 | (156) multiplication(all_2_1_1, all_2_2_2) = all_232_0_181 & multiplication(all_2_1_1, zero) = all_232_1_182 & addition(all_232_1_182, all_232_0_181) = all_2_0_0 % 45.16/13.55 | % 45.16/13.55 | Applying alpha-rule on (156) yields: % 45.16/13.56 | (157) multiplication(all_2_1_1, all_2_2_2) = all_232_0_181 % 45.16/13.56 | (158) multiplication(all_2_1_1, zero) = all_232_1_182 % 45.16/13.56 | (159) addition(all_232_1_182, all_232_0_181) = all_2_0_0 % 45.16/13.56 | % 45.16/13.56 +-Applying beta-rule and splitting (109), into two cases. % 45.16/13.56 |-Branch one: % 45.16/13.56 | (152) ~ (addition(zero, all_2_2_2) = all_2_2_2) % 45.16/13.56 | % 45.16/13.56 | Using (103) and (152) yields: % 45.16/13.56 | (153) $false % 45.16/13.56 | % 45.16/13.56 |-The branch is then unsatisfiable % 45.16/13.56 |-Branch two: % 45.16/13.56 | (103) addition(zero, all_2_2_2) = all_2_2_2 % 45.16/13.56 | (163) leq(zero, all_2_2_2) = 0 % 45.16/13.56 | % 45.16/13.56 +-Applying beta-rule and splitting (83), into two cases. % 45.16/13.56 |-Branch one: % 45.16/13.56 | (152) ~ (addition(zero, all_2_2_2) = all_2_2_2) % 45.16/13.56 | % 45.16/13.56 | Using (103) and (152) yields: % 45.16/13.56 | (153) $false % 45.16/13.56 | % 45.16/13.56 |-The branch is then unsatisfiable % 45.16/13.56 |-Branch two: % 45.16/13.56 | (103) addition(zero, all_2_2_2) = all_2_2_2 % 45.16/13.56 | (167) all_26_1_19 = all_2_2_2 % 45.16/13.56 | % 45.16/13.56 | From (167) and (72) follows: % 45.16/13.56 | (168) domain(all_2_2_2) = all_26_0_18 % 45.16/13.56 | % 45.16/13.56 | From (167) and (115) follows: % 45.16/13.56 | (169) multiplication(all_26_0_18, all_2_2_2) = all_68_0_45 % 45.16/13.56 | % 45.16/13.56 | From (167) and (133) follows: % 45.16/13.56 | (170) multiplication(all_2_1_1, all_2_2_2) = all_142_1_110 % 45.16/13.56 | % 45.16/13.56 | From (167) and (113) follows: % 45.16/13.56 | (171) addition(all_2_0_0, all_2_2_2) = all_64_1_42 % 45.16/13.56 | % 45.16/13.56 +-Applying beta-rule and splitting (77), into two cases. % 45.16/13.56 |-Branch one: % 45.16/13.56 | (172) ~ (domain(all_2_2_2) = all_26_0_18) % 45.16/13.56 | % 45.16/13.56 | Using (168) and (172) yields: % 45.16/13.56 | (153) $false % 45.16/13.56 | % 45.16/13.56 |-The branch is then unsatisfiable % 45.16/13.56 |-Branch two: % 45.16/13.56 | (168) domain(all_2_2_2) = all_26_0_18 % 45.16/13.56 | (175) all_26_0_18 = all_10_1_4 % 45.16/13.56 | % 45.16/13.56 | Combining equations (76,175) yields a new equation: % 45.16/13.56 | (176) all_26_0_18 = all_2_1_1 % 45.16/13.56 | % 45.16/13.56 | From (176) and (168) follows: % 45.16/13.56 | (41) domain(all_2_2_2) = all_2_1_1 % 45.16/13.56 | % 45.16/13.56 | From (176) and (126) follows: % 45.16/13.56 | (178) multiplication(all_2_1_1, all_2_2_2) = all_130_1_98 % 45.16/13.56 | % 45.16/13.56 | From (176) and (169) follows: % 45.16/13.56 | (179) multiplication(all_2_1_1, all_2_2_2) = all_68_0_45 % 45.16/13.56 | % 45.16/13.56 | From (176) and (73) follows: % 45.16/13.56 | (180) addition(zero, all_2_1_1) = all_2_1_1 % 45.16/13.56 | % 45.16/13.56 +-Applying beta-rule and splitting (95), into two cases. % 45.16/13.56 |-Branch one: % 45.16/13.56 | (181) ~ (domain(all_26_1_19) = all_2_1_1) % 45.16/13.56 | % 45.16/13.56 | From (167) and (181) follows: % 45.16/13.56 | (182) ~ (domain(all_2_2_2) = all_2_1_1) % 45.16/13.56 | % 45.16/13.56 | Using (41) and (182) yields: % 45.16/13.56 | (153) $false % 45.16/13.56 | % 45.16/13.56 |-The branch is then unsatisfiable % 45.16/13.56 |-Branch two: % 45.16/13.56 | (184) domain(all_26_1_19) = all_2_1_1 % 45.16/13.56 | (185) ? [v0] : ? [v1] : (domain(v0) = v1 & domain(all_10_0_3) = v1 & multiplication(all_2_1_1, all_26_1_19) = v0) % 45.16/13.56 | % 45.16/13.56 | Instantiating (185) with all_262_0_186, all_262_1_187 yields: % 45.16/13.56 | (186) domain(all_262_1_187) = all_262_0_186 & domain(all_10_0_3) = all_262_0_186 & multiplication(all_2_1_1, all_26_1_19) = all_262_1_187 % 45.16/13.56 | % 45.16/13.56 | Applying alpha-rule on (186) yields: % 45.16/13.56 | (187) domain(all_262_1_187) = all_262_0_186 % 45.16/13.56 | (188) domain(all_10_0_3) = all_262_0_186 % 45.16/13.56 | (189) multiplication(all_2_1_1, all_26_1_19) = all_262_1_187 % 45.16/13.56 | % 45.16/13.56 | From (167) and (189) follows: % 45.16/13.56 | (190) multiplication(all_2_1_1, all_2_2_2) = all_262_1_187 % 45.16/13.56 | % 45.16/13.56 +-Applying beta-rule and splitting (106), into two cases. % 45.16/13.56 |-Branch one: % 45.16/13.56 | (191) ~ (addition(zero, all_2_1_1) = all_2_1_1) % 45.16/13.56 | % 45.16/13.56 | Using (180) and (191) yields: % 45.16/13.56 | (153) $false % 45.16/13.56 | % 45.16/13.56 |-The branch is then unsatisfiable % 45.16/13.56 |-Branch two: % 45.16/13.56 | (180) addition(zero, all_2_1_1) = all_2_1_1 % 45.16/13.56 | (194) ? [v0] : ? [v1] : (multiplication(all_2_1_1, all_2_1_1) = v1 & multiplication(zero, all_2_1_1) = v0 & addition(v0, v1) = all_10_0_3) % 45.16/13.56 | % 45.16/13.56 +-Applying beta-rule and splitting (104), into two cases. % 45.16/13.56 |-Branch one: % 45.16/13.56 | (191) ~ (addition(zero, all_2_1_1) = all_2_1_1) % 45.16/13.56 | % 45.16/13.56 | Using (180) and (191) yields: % 45.16/13.56 | (153) $false % 45.16/13.56 | % 45.16/13.56 |-The branch is then unsatisfiable % 45.16/13.56 |-Branch two: % 45.16/13.56 | (180) addition(zero, all_2_1_1) = all_2_1_1 % 45.16/13.56 | (198) ? [v0] : ? [v1] : (multiplication(all_2_1_1, all_2_2_2) = v1 & multiplication(zero, all_2_2_2) = v0 & addition(v0, v1) = all_2_0_0) % 45.16/13.56 | % 45.16/13.56 | Instantiating (198) with all_314_0_196, all_314_1_197 yields: % 45.16/13.56 | (199) multiplication(all_2_1_1, all_2_2_2) = all_314_0_196 & multiplication(zero, all_2_2_2) = all_314_1_197 & addition(all_314_1_197, all_314_0_196) = all_2_0_0 % 45.16/13.56 | % 45.16/13.56 | Applying alpha-rule on (199) yields: % 45.16/13.56 | (200) multiplication(all_2_1_1, all_2_2_2) = all_314_0_196 % 45.16/13.56 | (201) multiplication(zero, all_2_2_2) = all_314_1_197 % 45.16/13.56 | (202) addition(all_314_1_197, all_314_0_196) = all_2_0_0 % 45.16/13.56 | % 45.16/13.56 | Instantiating formula (5) with all_2_1_1, all_2_2_2, all_314_0_196, all_2_0_0 and discharging atoms multiplication(all_2_1_1, all_2_2_2) = all_314_0_196, multiplication(all_2_1_1, all_2_2_2) = all_2_0_0, yields: % 45.16/13.56 | (203) all_314_0_196 = all_2_0_0 % 45.16/13.56 | % 45.16/13.56 | Instantiating formula (5) with all_2_1_1, all_2_2_2, all_232_0_181, all_262_1_187 and discharging atoms multiplication(all_2_1_1, all_2_2_2) = all_262_1_187, multiplication(all_2_1_1, all_2_2_2) = all_232_0_181, yields: % 45.16/13.56 | (204) all_262_1_187 = all_232_0_181 % 45.16/13.56 | % 45.16/13.56 | Instantiating formula (5) with all_2_1_1, all_2_2_2, all_182_1_139, all_184_1_141 and discharging atoms multiplication(all_2_1_1, all_2_2_2) = all_184_1_141, multiplication(all_2_1_1, all_2_2_2) = all_182_1_139, yields: % 45.16/13.56 | (205) all_184_1_141 = all_182_1_139 % 45.16/13.56 | % 45.16/13.56 | Instantiating formula (5) with all_2_1_1, all_2_2_2, all_170_1_128, all_262_1_187 and discharging atoms multiplication(all_2_1_1, all_2_2_2) = all_262_1_187, multiplication(all_2_1_1, all_2_2_2) = all_170_1_128, yields: % 45.16/13.56 | (206) all_262_1_187 = all_170_1_128 % 45.16/13.56 | % 45.16/13.56 | Instantiating formula (5) with all_2_1_1, all_2_2_2, all_142_1_110, all_182_1_139 and discharging atoms multiplication(all_2_1_1, all_2_2_2) = all_182_1_139, multiplication(all_2_1_1, all_2_2_2) = all_142_1_110, yields: % 45.16/13.56 | (207) all_182_1_139 = all_142_1_110 % 45.16/13.56 | % 45.16/13.56 | Instantiating formula (5) with all_2_1_1, all_2_2_2, all_142_1_110, all_170_1_128 and discharging atoms multiplication(all_2_1_1, all_2_2_2) = all_170_1_128, multiplication(all_2_1_1, all_2_2_2) = all_142_1_110, yields: % 45.16/13.56 | (208) all_170_1_128 = all_142_1_110 % 45.16/13.56 | % 45.16/13.56 | Instantiating formula (5) with all_2_1_1, all_2_2_2, all_130_1_98, all_262_1_187 and discharging atoms multiplication(all_2_1_1, all_2_2_2) = all_262_1_187, multiplication(all_2_1_1, all_2_2_2) = all_130_1_98, yields: % 45.16/13.56 | (209) all_262_1_187 = all_130_1_98 % 45.16/13.56 | % 45.16/13.56 | Instantiating formula (5) with all_2_1_1, all_2_2_2, all_80_1_56, all_314_0_196 and discharging atoms multiplication(all_2_1_1, all_2_2_2) = all_314_0_196, multiplication(all_2_1_1, all_2_2_2) = all_80_1_56, yields: % 45.16/13.56 | (210) all_314_0_196 = all_80_1_56 % 45.16/13.56 | % 45.16/13.56 | Instantiating formula (5) with all_2_1_1, all_2_2_2, all_80_1_56, all_170_1_128 and discharging atoms multiplication(all_2_1_1, all_2_2_2) = all_170_1_128, multiplication(all_2_1_1, all_2_2_2) = all_80_1_56, yields: % 45.16/13.56 | (211) all_170_1_128 = all_80_1_56 % 45.16/13.56 | % 45.16/13.56 | Instantiating formula (5) with all_2_1_1, all_2_2_2, all_68_0_45, all_184_1_141 and discharging atoms multiplication(all_2_1_1, all_2_2_2) = all_184_1_141, multiplication(all_2_1_1, all_2_2_2) = all_68_0_45, yields: % 45.16/13.56 | (212) all_184_1_141 = all_68_0_45 % 45.16/13.56 | % 45.16/13.56 | Instantiating formula (33) with all_118_0_85, all_2_2_2 and discharging atoms multiplication(one, all_2_2_2) = all_118_0_85, yields: % 45.16/13.56 | (213) all_118_0_85 = all_2_2_2 % 45.16/13.56 | % 45.16/13.56 | Instantiating formula (5) with one, all_2_2_2, all_118_1_86, all_118_0_85 and discharging atoms multiplication(one, all_2_2_2) = all_118_0_85, multiplication(one, all_2_2_2) = all_118_1_86, yields: % 45.16/13.56 | (214) all_118_0_85 = all_118_1_86 % 45.16/13.56 | % 45.16/13.56 | Using (123) and (75) yields: % 45.16/13.56 | (215) ~ (all_118_1_86 = all_2_0_0) % 45.16/13.56 | % 45.16/13.56 | Instantiating formula (17) with all_2_0_0, all_118_0_85, all_118_1_86, all_170_1_128 and discharging atoms addition(all_2_0_0, all_118_0_85) = all_118_1_86, yields: % 45.16/13.56 | (216) all_170_1_128 = all_118_1_86 | ~ (addition(all_2_0_0, all_118_0_85) = all_170_1_128) % 45.16/13.56 | % 45.16/13.56 | Instantiating formula (17) with all_2_0_0, all_2_2_2, all_134_0_100, all_200_1_157 and discharging atoms addition(all_2_0_0, all_2_2_2) = all_200_1_157, addition(all_2_0_0, all_2_2_2) = all_134_0_100, yields: % 45.16/13.56 | (217) all_200_1_157 = all_134_0_100 % 45.16/13.56 | % 45.16/13.56 | Instantiating formula (17) with all_2_0_0, all_2_2_2, all_64_1_42, all_200_1_157 and discharging atoms addition(all_2_0_0, all_2_2_2) = all_200_1_157, addition(all_2_0_0, all_2_2_2) = all_64_1_42, yields: % 45.16/13.57 | (218) all_200_1_157 = all_64_1_42 % 45.16/13.57 | % 45.16/13.57 | Instantiating formula (17) with all_2_0_0, all_2_2_2, all_2_0_0, all_134_0_100 and discharging atoms addition(all_2_0_0, all_2_2_2) = all_134_0_100, addition(all_2_0_0, all_2_2_2) = all_2_0_0, yields: % 45.16/13.57 | (219) all_134_0_100 = all_2_0_0 % 45.16/13.57 | % 45.16/13.57 | Combining equations (210,203) yields a new equation: % 45.16/13.57 | (220) all_80_1_56 = all_2_0_0 % 45.16/13.57 | % 45.16/13.57 | Simplifying 220 yields: % 45.16/13.57 | (221) all_80_1_56 = all_2_0_0 % 45.16/13.57 | % 45.16/13.57 | Combining equations (209,204) yields a new equation: % 45.16/13.57 | (222) all_232_0_181 = all_130_1_98 % 45.16/13.57 | % 45.16/13.57 | Combining equations (206,204) yields a new equation: % 45.16/13.57 | (223) all_232_0_181 = all_170_1_128 % 45.16/13.57 | % 45.16/13.57 | Combining equations (223,222) yields a new equation: % 45.16/13.57 | (224) all_170_1_128 = all_130_1_98 % 45.16/13.57 | % 45.16/13.57 | Simplifying 224 yields: % 45.16/13.57 | (225) all_170_1_128 = all_130_1_98 % 45.16/13.57 | % 45.16/13.57 | Combining equations (217,218) yields a new equation: % 45.16/13.57 | (226) all_134_0_100 = all_64_1_42 % 45.16/13.57 | % 45.16/13.57 | Simplifying 226 yields: % 45.16/13.57 | (227) all_134_0_100 = all_64_1_42 % 45.16/13.57 | % 45.16/13.57 | Combining equations (205,212) yields a new equation: % 45.16/13.57 | (228) all_182_1_139 = all_68_0_45 % 45.16/13.57 | % 45.16/13.57 | Simplifying 228 yields: % 45.16/13.57 | (229) all_182_1_139 = all_68_0_45 % 45.16/13.57 | % 45.16/13.57 | Combining equations (207,229) yields a new equation: % 45.16/13.57 | (230) all_142_1_110 = all_68_0_45 % 45.16/13.57 | % 45.16/13.57 | Simplifying 230 yields: % 45.16/13.57 | (231) all_142_1_110 = all_68_0_45 % 45.16/13.57 | % 45.16/13.57 | Combining equations (208,225) yields a new equation: % 45.16/13.57 | (232) all_142_1_110 = all_130_1_98 % 45.16/13.57 | % 45.16/13.57 | Simplifying 232 yields: % 45.16/13.57 | (233) all_142_1_110 = all_130_1_98 % 45.16/13.57 | % 45.16/13.57 | Combining equations (211,225) yields a new equation: % 45.16/13.57 | (234) all_130_1_98 = all_80_1_56 % 45.16/13.57 | % 45.16/13.57 | Combining equations (233,231) yields a new equation: % 45.16/13.57 | (235) all_130_1_98 = all_68_0_45 % 45.16/13.57 | % 45.16/13.57 | Simplifying 235 yields: % 45.16/13.57 | (236) all_130_1_98 = all_68_0_45 % 45.16/13.57 | % 45.16/13.57 | Combining equations (219,227) yields a new equation: % 45.16/13.57 | (237) all_64_1_42 = all_2_0_0 % 45.16/13.57 | % 45.16/13.57 | Combining equations (234,236) yields a new equation: % 45.16/13.57 | (238) all_80_1_56 = all_68_0_45 % 45.16/13.57 | % 45.16/13.57 | Simplifying 238 yields: % 45.16/13.57 | (239) all_80_1_56 = all_68_0_45 % 45.16/13.57 | % 45.16/13.57 | Combining equations (214,213) yields a new equation: % 45.16/13.57 | (240) all_118_1_86 = all_2_2_2 % 45.16/13.57 | % 45.16/13.57 | Simplifying 240 yields: % 45.16/13.57 | (241) all_118_1_86 = all_2_2_2 % 45.16/13.57 | % 45.16/13.57 | Combining equations (221,239) yields a new equation: % 45.16/13.57 | (242) all_68_0_45 = all_2_0_0 % 45.16/13.57 | % 45.16/13.57 | Combining equations (242,236) yields a new equation: % 45.16/13.57 | (243) all_130_1_98 = all_2_0_0 % 45.16/13.57 | % 45.16/13.57 | Combining equations (243,225) yields a new equation: % 45.16/13.57 | (244) all_170_1_128 = all_2_0_0 % 45.16/13.57 | % 45.16/13.57 | Equations (241) can reduce 215 to: % 45.16/13.57 | (245) ~ (all_2_0_0 = all_2_2_2) % 45.16/13.57 | % 45.16/13.57 | Simplifying 245 yields: % 45.16/13.57 | (40) ~ (all_2_0_0 = all_2_2_2) % 45.16/13.57 | % 45.16/13.57 | From (237) and (171) follows: % 45.16/13.57 | (100) addition(all_2_0_0, all_2_2_2) = all_2_0_0 % 45.16/13.57 | % 45.16/13.57 +-Applying beta-rule and splitting (216), into two cases. % 45.16/13.57 |-Branch one: % 45.16/13.57 | (248) ~ (addition(all_2_0_0, all_118_0_85) = all_170_1_128) % 45.16/13.57 | % 45.16/13.57 | From (213)(244) and (248) follows: % 45.16/13.57 | (249) ~ (addition(all_2_0_0, all_2_2_2) = all_2_0_0) % 45.16/13.57 | % 45.16/13.57 | Using (100) and (249) yields: % 45.16/13.57 | (153) $false % 45.16/13.57 | % 45.16/13.57 |-The branch is then unsatisfiable % 45.16/13.57 |-Branch two: % 45.16/13.57 | (251) addition(all_2_0_0, all_118_0_85) = all_170_1_128 % 45.16/13.57 | (252) all_170_1_128 = all_118_1_86 % 45.16/13.57 | % 45.16/13.57 | Combining equations (252,244) yields a new equation: % 45.16/13.57 | (253) all_118_1_86 = all_2_0_0 % 45.16/13.57 | % 45.16/13.57 | Simplifying 253 yields: % 45.16/13.57 | (254) all_118_1_86 = all_2_0_0 % 45.16/13.57 | % 45.16/13.57 | Combining equations (254,241) yields a new equation: % 45.16/13.57 | (255) all_2_0_0 = all_2_2_2 % 45.16/13.57 | % 45.16/13.57 | Simplifying 255 yields: % 45.16/13.57 | (256) all_2_0_0 = all_2_2_2 % 45.16/13.57 | % 45.16/13.57 | Equations (256) can reduce 40 to: % 45.16/13.57 | (257) $false % 45.16/13.57 | % 45.16/13.57 |-The branch is then unsatisfiable % 45.16/13.57 |-Branch two: % 45.16/13.57 | (258) multiplication(one, all_2_2_2) = all_2_0_0 % 45.16/13.57 | (256) all_2_0_0 = all_2_2_2 % 45.16/13.57 | % 45.16/13.57 | Equations (256) can reduce 40 to: % 45.16/13.57 | (257) $false % 45.16/13.57 | % 45.16/13.57 |-The branch is then unsatisfiable % 45.16/13.57 % SZS output end Proof for theBenchmark % 45.16/13.57 % 45.16/13.57 12918ms %------------------------------------------------------------------------------