%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : KLE070+1 : TPTP v8.1.0. Released v4.0.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 : Sun Jul 17 01:51:14 EDT 2022 % Result : Theorem 136.30s 102.69s % Output : Proof 181.11s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : KLE070+1 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.34 % Computer : n029.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Thu Jun 16 12:14:27 EDT 2022 % 0.13/0.34 % CPUTime : % 0.55/0.58 ____ _ % 0.55/0.58 ___ / __ \_____(_)___ ________ __________ % 0.55/0.58 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.55/0.58 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.55/0.58 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.55/0.58 % 0.55/0.58 A Theorem Prover for First-Order Logic % 0.55/0.59 (ePrincess v.1.0) % 0.55/0.59 % 0.55/0.59 (c) Philipp Rümmer, 2009-2015 % 0.55/0.59 (c) Peter Backeman, 2014-2015 % 0.55/0.59 (contributions by Angelo Brillout, Peter Baumgartner) % 0.55/0.59 Free software under GNU Lesser General Public License (LGPL). % 0.55/0.59 Bug reports to peter@backeman.se % 0.55/0.59 % 0.55/0.59 For more information, visit http://user.uu.se/~petba168/breu/ % 0.55/0.59 % 0.55/0.59 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.76/0.64 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.45/0.93 Prover 0: Preprocessing ... % 2.20/1.19 Prover 0: Constructing countermodel ... % 17.88/5.93 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 17.88/5.96 Prover 1: Preprocessing ... % 18.29/6.05 Prover 1: Constructing countermodel ... % 25.94/8.52 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 25.94/8.55 Prover 2: Preprocessing ... % 26.18/8.62 Prover 2: Warning: ignoring some quantifiers % 26.18/8.62 Prover 2: Constructing countermodel ... % 33.11/11.54 Prover 0: stopped % 33.27/11.74 Prover 3: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 33.27/11.76 Prover 3: Preprocessing ... % 33.52/11.80 Prover 3: Constructing countermodel ... % 78.50/53.07 Prover 3: stopped % 78.75/53.27 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=complete % 78.75/53.29 Prover 4: Preprocessing ... % 78.96/53.36 Prover 4: Warning: ignoring some quantifiers % 78.96/53.36 Prover 4: Constructing countermodel ... % 133.81/101.10 Prover 1: stopped % 133.98/101.31 Prover 5: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 133.98/101.32 Prover 5: Preprocessing ... % 134.19/101.37 Prover 5: Constructing countermodel ... % 136.30/102.68 Prover 5: proved (1378ms) % 136.30/102.69 Prover 2: stopped % 136.30/102.69 Prover 4: stopped % 136.30/102.69 % 136.30/102.69 No countermodel exists, formula is valid % 136.30/102.69 % SZS status Theorem for theBenchmark % 136.30/102.69 % 136.30/102.69 Generating proof ... found it (size 244) % 180.28/133.27 % 180.28/133.27 % SZS output start Proof for theBenchmark % 180.28/133.27 Assumed formulas after preprocessing and simplification: % 180.28/133.27 | (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] : ? [v3] : ? [v4] : ? [v5] : ( ~ (v5 = v2) & domain(v1) = v3 & domain(v0) = v2 & multiplication(v2, v3) = v4 & addition(v2, v4) = v5) % 180.47/133.31 | Applying alpha-rule on (0) yields: % 180.47/133.31 | (1) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ( ~ (v5 = v2) & domain(v1) = v3 & domain(v0) = v2 & multiplication(v2, v3) = v4 & addition(v2, v4) = v5) % 180.47/133.31 | (2) ! [v0] : ! [v1] : ( ~ (addition(v0, v1) = v1) | leq(v0, v1) = 0) % 180.47/133.31 | (3) ! [v0] : ! [v1] : ( ~ (leq(v0, v1) = 0) | addition(v0, v1) = v1) % 180.47/133.31 | (4) ! [v0] : ! [v1] : (v1 = v0 | ~ (addition(v0, v0) = v1)) % 180.47/133.31 | (5) ! [v0] : ! [v1] : ( ~ (domain(v0) = v1) | ? [v2] : (multiplication(v1, v0) = v2 & addition(v0, v2) = v2)) % 180.47/133.32 | (6) ! [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)) % 180.47/133.32 | (7) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v3, v2) = v4) | ~ (multiplication(v0, v1) = v3) | ? [v5] : (multiplication(v1, v2) = v5 & multiplication(v0, v5) = v4)) % 180.47/133.32 | (8) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v1, v2) = v3) | ~ (multiplication(v0, v3) = v4) | ? [v5] : (multiplication(v5, v2) = v4 & multiplication(v0, v1) = v5)) % 180.47/133.32 | (9) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (multiplication(v3, v2) = v1) | ~ (multiplication(v3, v2) = v0)) % 180.47/133.32 | (10) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (addition(v2, v3) = v4) | ~ (addition(v1, v0) = v3) | ? [v5] : (addition(v5, v0) = v4 & addition(v2, v1) = v5)) % 180.47/133.32 | (11) ! [v0] : ! [v1] : ( ~ (domain(v0) = v1) | addition(v1, one) = one) % 180.47/133.32 | (12) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (leq(v3, v2) = v1) | ~ (leq(v3, v2) = v0)) % 180.47/133.32 | (13) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (addition(v3, v0) = v4) | ~ (addition(v2, v1) = v3) | ? [v5] : (addition(v2, v5) = v4 & addition(v1, v0) = v5)) % 180.47/133.32 | (14) ! [v0] : ! [v1] : (v1 = v0 | ~ (multiplication(one, v0) = v1)) % 180.47/133.32 | (15) ! [v0] : ! [v1] : (v1 = zero | ~ (multiplication(zero, v0) = v1)) % 180.47/133.32 | (16) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v1, v2) = v3) | ~ (multiplication(v0, v1) = v4) | ? [v5] : (multiplication(v4, v2) = v5 & multiplication(v0, v3) = v5)) % 180.47/133.32 | (17) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (domain(v1) = v2) | ~ (multiplication(v0, v2) = v3) | ? [v4] : ? [v5] : (domain(v4) = v5 & domain(v3) = v5 & multiplication(v0, v1) = v4)) % 180.47/133.32 | (18) domain(zero) = zero % 180.47/133.32 | (19) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (domain(v2) = v1) | ~ (domain(v2) = v0)) % 180.47/133.33 | (20) ! [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)) % 180.47/133.33 | (21) ! [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)) % 180.47/133.33 | (22) ! [v0] : ! [v1] : (v1 = v0 | ~ (addition(v0, zero) = v1)) % 180.47/133.33 | (23) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (domain(v1) = v3) | ~ (domain(v0) = v2) | ? [v4] : ? [v5] : (domain(v4) = v5 & addition(v2, v3) = v5 & addition(v0, v1) = v4)) % 180.47/133.33 | (24) ! [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)) % 180.47/133.33 | (25) ! [v0] : ! [v1] : (v1 = zero | ~ (multiplication(v0, zero) = v1)) % 180.47/133.33 | (26) ! [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)) % 180.47/133.33 | (27) ! [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)) % 180.47/133.33 | (28) ! [v0] : ! [v1] : ! [v2] : ( ~ (multiplication(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (domain(v5) = v3 & domain(v2) = v3 & domain(v1) = v4 & multiplication(v0, v4) = v5)) % 180.47/133.33 | (29) ! [v0] : ! [v1] : ! [v2] : ( ~ (addition(v0, v1) = v2) | addition(v1, v0) = v2) % 180.47/133.33 | (30) ! [v0] : ! [v1] : ! [v2] : ( ~ (addition(v1, v0) = v2) | addition(v0, v1) = v2) % 180.47/133.33 | (31) ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (addition(v0, v1) = v2) | ? [v3] : ( ~ (v3 = 0) & leq(v0, v1) = v3)) % 180.47/133.33 | (32) ! [v0] : ! [v1] : ! [v2] : ( ~ (addition(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : (domain(v2) = v3 & domain(v1) = v5 & domain(v0) = v4 & addition(v4, v5) = v3)) % 180.47/133.33 | (33) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (addition(v2, v1) = v4) | ~ (addition(v1, v0) = v3) | ? [v5] : (addition(v4, v0) = v5 & addition(v2, v3) = v5)) % 180.47/133.34 | (34) ! [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)) % 180.47/133.34 | (35) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (addition(v3, v2) = v1) | ~ (addition(v3, v2) = v0)) % 180.47/133.34 | (36) ! [v0] : ! [v1] : (v1 = v0 | ~ (multiplication(v0, one) = v1)) % 180.47/133.34 | (37) ! [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)) % 180.47/133.34 | (38) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (leq(v0, v1) = v2) | ? [v3] : ( ~ (v3 = v1) & addition(v0, v1) = v3)) % 180.47/133.34 | % 180.47/133.34 | Instantiating (1) with all_2_0_0, all_2_1_1, all_2_2_2, all_2_3_3, all_2_4_4, all_2_5_5 yields: % 180.47/133.34 | (39) ~ (all_2_0_0 = all_2_3_3) & domain(all_2_4_4) = all_2_2_2 & domain(all_2_5_5) = all_2_3_3 & multiplication(all_2_3_3, all_2_2_2) = all_2_1_1 & addition(all_2_3_3, all_2_1_1) = all_2_0_0 % 180.47/133.34 | % 180.47/133.34 | Applying alpha-rule on (39) yields: % 180.47/133.34 | (40) multiplication(all_2_3_3, all_2_2_2) = all_2_1_1 % 180.47/133.34 | (41) addition(all_2_3_3, all_2_1_1) = all_2_0_0 % 180.47/133.34 | (42) domain(all_2_5_5) = all_2_3_3 % 180.47/133.34 | (43) domain(all_2_4_4) = all_2_2_2 % 180.47/133.34 | (44) ~ (all_2_0_0 = all_2_3_3) % 180.47/133.34 | % 180.47/133.34 | Instantiating formula (4) with all_2_0_0, all_2_3_3 yields: % 180.47/133.34 | (45) all_2_0_0 = all_2_3_3 | ~ (addition(all_2_3_3, all_2_3_3) = all_2_0_0) % 180.47/133.34 | % 180.47/133.34 | Instantiating formula (23) with all_2_2_2, all_2_2_2, all_2_4_4, all_2_4_4 and discharging atoms domain(all_2_4_4) = all_2_2_2, yields: % 180.47/133.34 | (46) ? [v0] : ? [v1] : (domain(v0) = v1 & addition(all_2_2_2, all_2_2_2) = v1 & addition(all_2_4_4, all_2_4_4) = v0) % 180.47/133.34 | % 180.47/133.34 | Instantiating formula (11) with all_2_2_2, all_2_4_4 and discharging atoms domain(all_2_4_4) = all_2_2_2, yields: % 180.47/133.34 | (47) addition(all_2_2_2, one) = one % 180.47/133.34 | % 180.47/133.34 | Instantiating formula (23) with all_2_2_2, all_2_3_3, all_2_4_4, all_2_5_5 and discharging atoms domain(all_2_4_4) = all_2_2_2, domain(all_2_5_5) = all_2_3_3, yields: % 180.47/133.34 | (48) ? [v0] : ? [v1] : (domain(v0) = v1 & addition(all_2_3_3, all_2_2_2) = v1 & addition(all_2_5_5, all_2_4_4) = v0) % 180.47/133.34 | % 180.47/133.34 | Instantiating formula (23) with all_2_3_3, all_2_3_3, all_2_5_5, all_2_5_5 and discharging atoms domain(all_2_5_5) = all_2_3_3, yields: % 180.47/133.34 | (49) ? [v0] : ? [v1] : (domain(v0) = v1 & addition(all_2_3_3, all_2_3_3) = v1 & addition(all_2_5_5, all_2_5_5) = v0) % 180.47/133.34 | % 180.47/133.34 | Instantiating formula (5) with all_2_3_3, all_2_5_5 and discharging atoms domain(all_2_5_5) = all_2_3_3, yields: % 180.47/133.34 | (50) ? [v0] : (multiplication(all_2_3_3, all_2_5_5) = v0 & addition(all_2_5_5, v0) = v0) % 180.47/133.34 | % 180.47/133.34 | Instantiating formula (23) with zero, all_2_3_3, zero, all_2_5_5 and discharging atoms domain(all_2_5_5) = all_2_3_3, domain(zero) = zero, yields: % 180.47/133.34 | (51) ? [v0] : ? [v1] : (domain(v0) = v1 & addition(all_2_3_3, zero) = v1 & addition(all_2_5_5, zero) = v0) % 180.47/133.34 | % 180.47/133.34 | Instantiating formula (23) with all_2_3_3, zero, all_2_5_5, zero and discharging atoms domain(all_2_5_5) = all_2_3_3, domain(zero) = zero, yields: % 180.47/133.34 | (52) ? [v0] : ? [v1] : (domain(v0) = v1 & addition(zero, all_2_3_3) = v1 & addition(zero, all_2_5_5) = v0) % 180.47/133.34 | % 180.47/133.34 | Instantiating formula (34) with all_2_1_1, all_2_1_1, all_2_2_2, all_2_3_3, all_2_3_3 and discharging atoms multiplication(all_2_3_3, all_2_2_2) = all_2_1_1, yields: % 180.47/133.34 | (53) ? [v0] : ? [v1] : (multiplication(v0, all_2_2_2) = v1 & addition(all_2_1_1, all_2_1_1) = v1 & addition(all_2_3_3, all_2_3_3) = v0) % 180.47/133.34 | % 180.47/133.34 | Instantiating formula (21) with all_2_1_1, all_2_1_1, all_2_2_2, all_2_2_2, all_2_3_3 and discharging atoms multiplication(all_2_3_3, all_2_2_2) = all_2_1_1, yields: % 180.47/133.35 | (54) ? [v0] : ? [v1] : (multiplication(all_2_3_3, v0) = v1 & addition(all_2_1_1, all_2_1_1) = v1 & addition(all_2_2_2, all_2_2_2) = v0) % 180.47/133.35 | % 180.47/133.35 | Instantiating formula (17) with all_2_1_1, all_2_2_2, all_2_4_4, all_2_3_3 and discharging atoms domain(all_2_4_4) = all_2_2_2, multiplication(all_2_3_3, all_2_2_2) = all_2_1_1, yields: % 180.47/133.35 | (55) ? [v0] : ? [v1] : (domain(v0) = v1 & domain(all_2_1_1) = v1 & multiplication(all_2_3_3, all_2_4_4) = v0) % 180.47/133.35 | % 180.47/133.35 | Instantiating formula (28) with all_2_1_1, all_2_2_2, all_2_3_3 and discharging atoms multiplication(all_2_3_3, all_2_2_2) = all_2_1_1, yields: % 180.47/133.35 | (56) ? [v0] : ? [v1] : ? [v2] : (domain(v2) = v0 & domain(all_2_1_1) = v0 & domain(all_2_2_2) = v1 & multiplication(all_2_3_3, v1) = v2) % 180.47/133.35 | % 180.47/133.35 | Instantiating formula (20) with all_2_1_1, all_2_0_0, all_2_2_2, all_2_1_1, all_2_3_3 and discharging atoms multiplication(all_2_3_3, all_2_2_2) = all_2_1_1, addition(all_2_3_3, all_2_1_1) = all_2_0_0, yields: % 180.47/133.35 | (57) ? [v0] : ? [v1] : (multiplication(all_2_0_0, all_2_2_2) = v0 & multiplication(all_2_1_1, all_2_2_2) = v1 & addition(all_2_1_1, v1) = v0) % 180.47/133.35 | % 180.47/133.35 | Instantiating formula (30) with all_2_0_0, all_2_3_3, all_2_1_1 and discharging atoms addition(all_2_3_3, all_2_1_1) = all_2_0_0, yields: % 180.47/133.35 | (58) addition(all_2_1_1, all_2_3_3) = all_2_0_0 % 180.47/133.35 | % 180.47/133.35 | Instantiating formula (32) with all_2_0_0, all_2_1_1, all_2_3_3 and discharging atoms addition(all_2_3_3, all_2_1_1) = all_2_0_0, yields: % 180.47/133.35 | (59) ? [v0] : ? [v1] : ? [v2] : (domain(all_2_0_0) = v0 & domain(all_2_1_1) = v2 & domain(all_2_3_3) = v1 & addition(v1, v2) = v0) % 180.47/133.35 | % 180.47/133.35 | Instantiating (52) with all_12_0_8, all_12_1_9 yields: % 180.47/133.35 | (60) domain(all_12_1_9) = all_12_0_8 & addition(zero, all_2_3_3) = all_12_0_8 & addition(zero, all_2_5_5) = all_12_1_9 % 180.47/133.35 | % 180.47/133.35 | Applying alpha-rule on (60) yields: % 180.47/133.35 | (61) domain(all_12_1_9) = all_12_0_8 % 180.47/133.35 | (62) addition(zero, all_2_3_3) = all_12_0_8 % 180.47/133.35 | (63) addition(zero, all_2_5_5) = all_12_1_9 % 180.47/133.35 | % 180.47/133.35 | Instantiating (50) with all_16_0_12 yields: % 180.47/133.35 | (64) multiplication(all_2_3_3, all_2_5_5) = all_16_0_12 & addition(all_2_5_5, all_16_0_12) = all_16_0_12 % 180.47/133.35 | % 180.47/133.35 | Applying alpha-rule on (64) yields: % 180.47/133.35 | (65) multiplication(all_2_3_3, all_2_5_5) = all_16_0_12 % 180.47/133.35 | (66) addition(all_2_5_5, all_16_0_12) = all_16_0_12 % 180.47/133.35 | % 180.47/133.35 | Instantiating (51) with all_18_0_13, all_18_1_14 yields: % 180.47/133.35 | (67) domain(all_18_1_14) = all_18_0_13 & addition(all_2_3_3, zero) = all_18_0_13 & addition(all_2_5_5, zero) = all_18_1_14 % 180.47/133.35 | % 180.47/133.35 | Applying alpha-rule on (67) yields: % 180.47/133.35 | (68) domain(all_18_1_14) = all_18_0_13 % 180.47/133.35 | (69) addition(all_2_3_3, zero) = all_18_0_13 % 180.47/133.35 | (70) addition(all_2_5_5, zero) = all_18_1_14 % 180.47/133.35 | % 180.47/133.35 | Instantiating (57) with all_20_0_15, all_20_1_16 yields: % 180.47/133.35 | (71) multiplication(all_2_0_0, all_2_2_2) = all_20_1_16 & multiplication(all_2_1_1, all_2_2_2) = all_20_0_15 & addition(all_2_1_1, all_20_0_15) = all_20_1_16 % 180.47/133.35 | % 180.47/133.35 | Applying alpha-rule on (71) yields: % 180.47/133.35 | (72) multiplication(all_2_0_0, all_2_2_2) = all_20_1_16 % 180.47/133.35 | (73) multiplication(all_2_1_1, all_2_2_2) = all_20_0_15 % 180.47/133.35 | (74) addition(all_2_1_1, all_20_0_15) = all_20_1_16 % 180.47/133.35 | % 180.47/133.35 | Instantiating (56) with all_22_0_17, all_22_1_18, all_22_2_19 yields: % 180.47/133.35 | (75) domain(all_22_0_17) = all_22_2_19 & domain(all_2_1_1) = all_22_2_19 & domain(all_2_2_2) = all_22_1_18 & multiplication(all_2_3_3, all_22_1_18) = all_22_0_17 % 180.47/133.35 | % 180.47/133.35 | Applying alpha-rule on (75) yields: % 180.47/133.35 | (76) domain(all_22_0_17) = all_22_2_19 % 180.47/133.35 | (77) domain(all_2_1_1) = all_22_2_19 % 180.47/133.35 | (78) domain(all_2_2_2) = all_22_1_18 % 180.47/133.35 | (79) multiplication(all_2_3_3, all_22_1_18) = all_22_0_17 % 180.47/133.35 | % 180.47/133.35 | Instantiating (54) with all_24_0_20, all_24_1_21 yields: % 180.47/133.35 | (80) multiplication(all_2_3_3, all_24_1_21) = all_24_0_20 & addition(all_2_1_1, all_2_1_1) = all_24_0_20 & addition(all_2_2_2, all_2_2_2) = all_24_1_21 % 180.47/133.35 | % 180.47/133.35 | Applying alpha-rule on (80) yields: % 180.47/133.35 | (81) multiplication(all_2_3_3, all_24_1_21) = all_24_0_20 % 180.47/133.35 | (82) addition(all_2_1_1, all_2_1_1) = all_24_0_20 % 180.47/133.35 | (83) addition(all_2_2_2, all_2_2_2) = all_24_1_21 % 180.47/133.35 | % 180.47/133.35 | Instantiating (55) with all_26_0_22, all_26_1_23 yields: % 180.47/133.35 | (84) domain(all_26_1_23) = all_26_0_22 & domain(all_2_1_1) = all_26_0_22 & multiplication(all_2_3_3, all_2_4_4) = all_26_1_23 % 180.47/133.35 | % 180.47/133.35 | Applying alpha-rule on (84) yields: % 180.47/133.35 | (85) domain(all_26_1_23) = all_26_0_22 % 180.47/133.35 | (86) domain(all_2_1_1) = all_26_0_22 % 180.47/133.35 | (87) multiplication(all_2_3_3, all_2_4_4) = all_26_1_23 % 180.47/133.35 | % 180.47/133.35 | Instantiating (46) with all_28_0_24, all_28_1_25 yields: % 180.47/133.35 | (88) domain(all_28_1_25) = all_28_0_24 & addition(all_2_2_2, all_2_2_2) = all_28_0_24 & addition(all_2_4_4, all_2_4_4) = all_28_1_25 % 180.47/133.35 | % 180.47/133.35 | Applying alpha-rule on (88) yields: % 180.47/133.35 | (89) domain(all_28_1_25) = all_28_0_24 % 180.47/133.35 | (90) addition(all_2_2_2, all_2_2_2) = all_28_0_24 % 180.47/133.35 | (91) addition(all_2_4_4, all_2_4_4) = all_28_1_25 % 180.47/133.35 | % 180.47/133.35 | Instantiating (53) with all_32_0_28, all_32_1_29 yields: % 180.47/133.35 | (92) multiplication(all_32_1_29, all_2_2_2) = all_32_0_28 & addition(all_2_1_1, all_2_1_1) = all_32_0_28 & addition(all_2_3_3, all_2_3_3) = all_32_1_29 % 180.47/133.35 | % 180.47/133.35 | Applying alpha-rule on (92) yields: % 180.47/133.35 | (93) multiplication(all_32_1_29, all_2_2_2) = all_32_0_28 % 180.47/133.35 | (94) addition(all_2_1_1, all_2_1_1) = all_32_0_28 % 180.47/133.35 | (95) addition(all_2_3_3, all_2_3_3) = all_32_1_29 % 180.47/133.36 | % 180.47/133.36 | Instantiating (49) with all_36_0_31, all_36_1_32 yields: % 180.47/133.36 | (96) domain(all_36_1_32) = all_36_0_31 & addition(all_2_3_3, all_2_3_3) = all_36_0_31 & addition(all_2_5_5, all_2_5_5) = all_36_1_32 % 180.47/133.36 | % 180.47/133.36 | Applying alpha-rule on (96) yields: % 180.47/133.36 | (97) domain(all_36_1_32) = all_36_0_31 % 180.47/133.36 | (98) addition(all_2_3_3, all_2_3_3) = all_36_0_31 % 180.47/133.36 | (99) addition(all_2_5_5, all_2_5_5) = all_36_1_32 % 180.47/133.36 | % 180.47/133.36 | Instantiating (48) with all_38_0_33, all_38_1_34 yields: % 180.47/133.36 | (100) domain(all_38_1_34) = all_38_0_33 & addition(all_2_3_3, all_2_2_2) = all_38_0_33 & addition(all_2_5_5, all_2_4_4) = all_38_1_34 % 180.47/133.36 | % 180.47/133.36 | Applying alpha-rule on (100) yields: % 180.47/133.36 | (101) domain(all_38_1_34) = all_38_0_33 % 180.47/133.36 | (102) addition(all_2_3_3, all_2_2_2) = all_38_0_33 % 180.47/133.36 | (103) addition(all_2_5_5, all_2_4_4) = all_38_1_34 % 180.47/133.36 | % 180.47/133.36 | Instantiating (59) with all_40_0_35, all_40_1_36, all_40_2_37 yields: % 180.47/133.36 | (104) domain(all_2_0_0) = all_40_2_37 & domain(all_2_1_1) = all_40_0_35 & domain(all_2_3_3) = all_40_1_36 & addition(all_40_1_36, all_40_0_35) = all_40_2_37 % 180.47/133.36 | % 180.47/133.36 | Applying alpha-rule on (104) yields: % 180.47/133.36 | (105) domain(all_2_0_0) = all_40_2_37 % 180.47/133.36 | (106) domain(all_2_1_1) = all_40_0_35 % 180.47/133.36 | (107) domain(all_2_3_3) = all_40_1_36 % 180.47/133.36 | (108) addition(all_40_1_36, all_40_0_35) = all_40_2_37 % 180.47/133.36 | % 180.47/133.36 +-Applying beta-rule and splitting (45), into two cases. % 180.47/133.36 |-Branch one: % 180.47/133.36 | (109) ~ (addition(all_2_3_3, all_2_3_3) = all_2_0_0) % 180.47/133.36 | % 180.47/133.36 | Instantiating formula (19) with all_2_1_1, all_40_0_35, all_26_0_22 and discharging atoms domain(all_2_1_1) = all_40_0_35, domain(all_2_1_1) = all_26_0_22, yields: % 180.47/133.36 | (110) all_40_0_35 = all_26_0_22 % 180.47/133.36 | % 180.47/133.36 | Instantiating formula (19) with all_2_1_1, all_40_0_35, all_22_2_19 and discharging atoms domain(all_2_1_1) = all_40_0_35, domain(all_2_1_1) = all_22_2_19, yields: % 180.47/133.36 | (111) all_40_0_35 = all_22_2_19 % 180.47/133.36 | % 180.47/133.36 | Instantiating formula (4) with all_32_0_28, all_2_1_1 and discharging atoms addition(all_2_1_1, all_2_1_1) = all_32_0_28, yields: % 180.47/133.36 | (112) all_32_0_28 = all_2_1_1 % 180.47/133.36 | % 180.47/133.36 | Instantiating formula (35) with all_2_1_1, all_2_1_1, all_24_0_20, all_32_0_28 and discharging atoms addition(all_2_1_1, all_2_1_1) = all_32_0_28, addition(all_2_1_1, all_2_1_1) = all_24_0_20, yields: % 180.47/133.36 | (113) all_32_0_28 = all_24_0_20 % 180.47/133.36 | % 180.47/133.36 | Instantiating formula (4) with all_28_0_24, all_2_2_2 and discharging atoms addition(all_2_2_2, all_2_2_2) = all_28_0_24, yields: % 180.47/133.36 | (114) all_28_0_24 = all_2_2_2 % 180.47/133.36 | % 180.47/133.36 | Instantiating formula (35) with all_2_2_2, all_2_2_2, all_24_1_21, all_28_0_24 and discharging atoms addition(all_2_2_2, all_2_2_2) = all_28_0_24, addition(all_2_2_2, all_2_2_2) = all_24_1_21, yields: % 180.47/133.36 | (115) all_28_0_24 = all_24_1_21 % 180.47/133.36 | % 180.47/133.36 | Instantiating formula (4) with all_36_0_31, all_2_3_3 and discharging atoms addition(all_2_3_3, all_2_3_3) = all_36_0_31, yields: % 180.47/133.36 | (116) all_36_0_31 = all_2_3_3 % 180.47/133.36 | % 180.47/133.36 | Instantiating formula (35) with all_2_3_3, all_2_3_3, all_32_1_29, all_36_0_31 and discharging atoms addition(all_2_3_3, all_2_3_3) = all_36_0_31, addition(all_2_3_3, all_2_3_3) = all_32_1_29, yields: % 180.47/133.36 | (117) all_36_0_31 = all_32_1_29 % 180.47/133.36 | % 180.47/133.36 | Instantiating formula (22) with all_18_0_13, all_2_3_3 and discharging atoms addition(all_2_3_3, zero) = all_18_0_13, yields: % 180.47/133.36 | (118) all_18_0_13 = all_2_3_3 % 180.47/133.36 | % 180.47/133.36 | Instantiating formula (22) with all_18_1_14, all_2_5_5 and discharging atoms addition(all_2_5_5, zero) = all_18_1_14, yields: % 180.47/133.36 | (119) all_18_1_14 = all_2_5_5 % 180.47/133.36 | % 180.47/133.36 | Instantiating formula (35) with zero, all_2_3_3, all_12_0_8, all_2_3_3 and discharging atoms addition(zero, all_2_3_3) = all_12_0_8, yields: % 180.47/133.36 | (120) all_12_0_8 = all_2_3_3 | ~ (addition(zero, all_2_3_3) = all_2_3_3) % 180.47/133.36 | % 180.47/133.36 | Combining equations (110,111) yields a new equation: % 180.47/133.36 | (121) all_26_0_22 = all_22_2_19 % 180.47/133.36 | % 180.47/133.36 | Simplifying 121 yields: % 180.47/133.36 | (122) all_26_0_22 = all_22_2_19 % 180.47/133.36 | % 180.47/133.36 | Combining equations (117,116) yields a new equation: % 180.47/133.36 | (123) all_32_1_29 = all_2_3_3 % 180.47/133.36 | % 180.47/133.36 | Simplifying 123 yields: % 180.47/133.36 | (124) all_32_1_29 = all_2_3_3 % 180.47/133.36 | % 180.47/133.36 | Combining equations (112,113) yields a new equation: % 180.47/133.36 | (125) all_24_0_20 = all_2_1_1 % 180.47/133.36 | % 180.47/133.36 | Combining equations (114,115) yields a new equation: % 180.47/133.36 | (126) all_24_1_21 = all_2_2_2 % 180.47/133.36 | % 180.47/133.36 | From (119)(118) and (68) follows: % 180.47/133.36 | (42) domain(all_2_5_5) = all_2_3_3 % 180.47/133.36 | % 180.47/133.36 | From (122) and (86) follows: % 180.47/133.36 | (77) domain(all_2_1_1) = all_22_2_19 % 180.47/133.36 | % 180.47/133.36 | From (126)(125) and (81) follows: % 180.47/133.36 | (40) multiplication(all_2_3_3, all_2_2_2) = all_2_1_1 % 180.47/133.36 | % 180.47/133.36 | From (125) and (82) follows: % 180.47/133.36 | (130) addition(all_2_1_1, all_2_1_1) = all_2_1_1 % 180.47/133.36 | % 180.47/133.36 | From (124) and (95) follows: % 180.47/133.36 | (131) addition(all_2_3_3, all_2_3_3) = all_2_3_3 % 180.47/133.36 | % 180.47/133.36 | From (118) and (69) follows: % 180.47/133.36 | (132) addition(all_2_3_3, zero) = all_2_3_3 % 180.47/133.36 | % 180.47/133.36 | Instantiating formula (23) with all_12_0_8, all_2_3_3, all_12_1_9, all_2_5_5 and discharging atoms domain(all_12_1_9) = all_12_0_8, domain(all_2_5_5) = all_2_3_3, yields: % 180.86/133.36 | (133) ? [v0] : ? [v1] : (domain(v0) = v1 & addition(all_2_3_3, all_12_0_8) = v1 & addition(all_2_5_5, all_12_1_9) = v0) % 180.86/133.36 | % 180.86/133.36 | Instantiating formula (23) with all_2_3_3, all_12_0_8, all_2_5_5, all_12_1_9 and discharging atoms domain(all_12_1_9) = all_12_0_8, domain(all_2_5_5) = all_2_3_3, yields: % 180.86/133.36 | (134) ? [v0] : ? [v1] : (domain(v0) = v1 & addition(all_12_0_8, all_2_3_3) = v1 & addition(all_12_1_9, all_2_5_5) = v0) % 180.86/133.36 | % 180.86/133.36 | Instantiating formula (23) with all_12_0_8, all_12_0_8, all_12_1_9, all_12_1_9 and discharging atoms domain(all_12_1_9) = all_12_0_8, yields: % 180.86/133.37 | (135) ? [v0] : ? [v1] : (domain(v0) = v1 & addition(all_12_0_8, all_12_0_8) = v1 & addition(all_12_1_9, all_12_1_9) = v0) % 180.86/133.37 | % 180.86/133.37 | Instantiating formula (23) with all_40_2_37, all_40_1_36, all_2_0_0, all_2_3_3 and discharging atoms domain(all_2_0_0) = all_40_2_37, domain(all_2_3_3) = all_40_1_36, yields: % 180.86/133.37 | (136) ? [v0] : ? [v1] : (domain(v0) = v1 & addition(all_40_1_36, all_40_2_37) = v1 & addition(all_2_3_3, all_2_0_0) = v0) % 180.86/133.37 | % 180.86/133.37 | Instantiating formula (23) with all_40_1_36, all_22_2_19, all_2_3_3, all_2_1_1 and discharging atoms domain(all_2_1_1) = all_22_2_19, domain(all_2_3_3) = all_40_1_36, yields: % 180.86/133.37 | (137) ? [v0] : ? [v1] : (domain(v0) = v1 & addition(all_22_2_19, all_40_1_36) = v1 & addition(all_2_1_1, all_2_3_3) = v0) % 180.86/133.37 | % 180.86/133.37 | Instantiating formula (23) with all_40_1_36, all_40_1_36, all_2_3_3, all_2_3_3 and discharging atoms domain(all_2_3_3) = all_40_1_36, yields: % 180.86/133.37 | (138) ? [v0] : ? [v1] : (domain(v0) = v1 & addition(all_40_1_36, all_40_1_36) = v1 & addition(all_2_3_3, all_2_3_3) = v0) % 180.86/133.37 | % 180.86/133.37 | Instantiating formula (34) with all_20_1_16, all_2_1_1, all_2_2_2, all_2_0_0, all_2_3_3 and discharging atoms multiplication(all_2_0_0, all_2_2_2) = all_20_1_16, multiplication(all_2_3_3, all_2_2_2) = all_2_1_1, yields: % 180.86/133.37 | (139) ? [v0] : ? [v1] : (multiplication(v0, all_2_2_2) = v1 & addition(all_2_1_1, all_20_1_16) = v1 & addition(all_2_3_3, all_2_0_0) = v0) % 180.86/133.37 | % 180.86/133.37 | Instantiating formula (34) with all_22_0_17, all_22_0_17, all_22_1_18, all_2_3_3, all_2_3_3 and discharging atoms multiplication(all_2_3_3, all_22_1_18) = all_22_0_17, yields: % 180.86/133.37 | (140) ? [v0] : ? [v1] : (multiplication(v0, all_22_1_18) = v1 & addition(all_22_0_17, all_22_0_17) = v1 & addition(all_2_3_3, all_2_3_3) = v0) % 180.86/133.37 | % 180.86/133.37 | Instantiating formula (34) with all_26_1_23, all_26_1_23, all_2_4_4, all_2_3_3, all_2_3_3 and discharging atoms multiplication(all_2_3_3, all_2_4_4) = all_26_1_23, yields: % 180.86/133.37 | (141) ? [v0] : ? [v1] : (multiplication(v0, all_2_4_4) = v1 & addition(all_26_1_23, all_26_1_23) = v1 & addition(all_2_3_3, all_2_3_3) = v0) % 180.86/133.37 | % 180.86/133.37 | Instantiating formula (34) with all_16_0_12, all_16_0_12, all_2_5_5, all_2_3_3, all_2_3_3 and discharging atoms multiplication(all_2_3_3, all_2_5_5) = all_16_0_12, yields: % 180.86/133.37 | (142) ? [v0] : ? [v1] : (multiplication(v0, all_2_5_5) = v1 & addition(all_16_0_12, all_16_0_12) = v1 & addition(all_2_3_3, all_2_3_3) = v0) % 180.86/133.37 | % 180.86/133.37 | Instantiating formula (10) with all_2_0_0, all_2_1_1, all_2_3_3, all_2_1_1, all_2_1_1 and discharging atoms addition(all_2_1_1, all_2_1_1) = all_2_1_1, addition(all_2_3_3, all_2_1_1) = all_2_0_0, yields: % 180.86/133.37 | (143) ? [v0] : (addition(v0, all_2_1_1) = all_2_0_0 & addition(all_2_3_3, all_2_1_1) = v0) % 180.86/133.37 | % 180.86/133.37 | Instantiating formula (33) with all_2_0_0, all_2_1_1, all_2_3_3, all_2_1_1, all_2_1_1 and discharging atoms addition(all_2_1_1, all_2_1_1) = all_2_1_1, addition(all_2_3_3, all_2_1_1) = all_2_0_0, yields: % 180.86/133.37 | (144) ? [v0] : (addition(all_2_0_0, all_2_1_1) = v0 & addition(all_2_3_3, all_2_1_1) = v0) % 180.86/133.37 | % 180.86/133.37 | Instantiating formula (33) with all_2_0_0, all_2_0_0, all_2_3_3, all_2_1_1, all_2_3_3 and discharging atoms addition(all_2_1_1, all_2_3_3) = all_2_0_0, addition(all_2_3_3, all_2_1_1) = all_2_0_0, yields: % 180.86/133.37 | (145) ? [v0] : (addition(all_2_0_0, all_2_3_3) = v0 & addition(all_2_3_3, all_2_0_0) = v0) % 180.86/133.37 | % 180.86/133.37 | Instantiating formula (33) with all_2_1_1, all_2_0_0, all_2_1_1, all_2_1_1, all_2_3_3 and discharging atoms addition(all_2_1_1, all_2_1_1) = all_2_1_1, addition(all_2_1_1, all_2_3_3) = all_2_0_0, yields: % 180.86/133.37 | (146) ? [v0] : (addition(all_2_1_1, all_2_0_0) = v0 & addition(all_2_1_1, all_2_3_3) = v0) % 180.86/133.37 | % 180.86/133.37 | Instantiating formula (13) with all_2_0_0, all_2_3_3, all_2_3_3, all_2_3_3, all_2_1_1 and discharging atoms addition(all_2_3_3, all_2_1_1) = all_2_0_0, addition(all_2_3_3, all_2_3_3) = all_2_3_3, yields: % 180.86/133.37 | (147) ? [v0] : (addition(all_2_3_3, v0) = all_2_0_0 & addition(all_2_3_3, all_2_1_1) = v0) % 180.86/133.37 | % 180.86/133.37 | Instantiating formula (33) with all_2_3_3, all_2_0_0, all_2_3_3, all_2_3_3, all_2_1_1 and discharging atoms addition(all_2_3_3, all_2_1_1) = all_2_0_0, addition(all_2_3_3, all_2_3_3) = all_2_3_3, yields: % 180.86/133.37 | (148) ? [v0] : (addition(all_2_3_3, all_2_0_0) = v0 & addition(all_2_3_3, all_2_1_1) = v0) % 180.86/133.37 | % 180.86/133.37 | Instantiating formula (33) with all_2_0_0, all_2_3_3, all_2_1_1, all_2_3_3, all_2_3_3 and discharging atoms addition(all_2_1_1, all_2_3_3) = all_2_0_0, addition(all_2_3_3, all_2_3_3) = all_2_3_3, yields: % 180.86/133.37 | (149) ? [v0] : (addition(all_2_0_0, all_2_3_3) = v0 & addition(all_2_1_1, all_2_3_3) = v0) % 180.86/133.37 | % 180.86/133.37 | Instantiating formula (37) with all_2_1_1, one, one, all_2_2_2, all_2_3_3 and discharging atoms multiplication(all_2_3_3, all_2_2_2) = all_2_1_1, addition(all_2_2_2, one) = one, yields: % 180.86/133.37 | (150) ? [v0] : ? [v1] : (multiplication(all_2_3_3, one) = v1 & multiplication(all_2_3_3, one) = v0 & addition(all_2_1_1, v1) = v0) % 180.86/133.37 | % 180.86/133.37 | Instantiating formula (33) with all_2_0_0, all_2_3_3, all_2_1_1, all_2_3_3, zero and discharging atoms addition(all_2_1_1, all_2_3_3) = all_2_0_0, addition(all_2_3_3, zero) = all_2_3_3, yields: % 180.86/133.37 | (151) ? [v0] : (addition(all_2_0_0, zero) = v0 & addition(all_2_1_1, all_2_3_3) = v0) % 180.86/133.37 | % 180.86/133.37 | Instantiating formula (30) with all_2_3_3, all_2_3_3, zero and discharging atoms addition(all_2_3_3, zero) = all_2_3_3, yields: % 180.86/133.37 | (152) addition(zero, all_2_3_3) = all_2_3_3 % 180.86/133.37 | % 180.86/133.37 | Instantiating formula (24) with all_16_0_12, all_2_3_3, all_2_5_5, all_2_3_3, zero and discharging atoms multiplication(all_2_3_3, all_2_5_5) = all_16_0_12, yields: % 180.86/133.37 | (153) ~ (addition(zero, all_2_3_3) = all_2_3_3) | ? [v0] : ? [v1] : (multiplication(all_2_3_3, all_2_5_5) = v1 & multiplication(zero, all_2_5_5) = v0 & addition(v0, v1) = all_16_0_12) % 180.86/133.37 | % 180.86/133.37 | Instantiating formula (13) with all_2_0_0, all_2_3_3, zero, all_2_3_3, all_2_1_1 and discharging atoms addition(all_2_3_3, all_2_1_1) = all_2_0_0, yields: % 180.86/133.37 | (154) ~ (addition(zero, all_2_3_3) = all_2_3_3) | ? [v0] : (addition(all_2_3_3, all_2_1_1) = v0 & addition(zero, v0) = all_2_0_0) % 180.86/133.37 | % 180.86/133.37 | Instantiating formula (33) with all_12_0_8, all_2_0_0, zero, all_2_3_3, all_2_1_1 and discharging atoms addition(all_2_3_3, all_2_1_1) = all_2_0_0, addition(zero, all_2_3_3) = all_12_0_8, yields: % 180.86/133.37 | (155) ? [v0] : (addition(all_12_0_8, all_2_1_1) = v0 & addition(zero, all_2_0_0) = v0) % 180.86/133.37 | % 180.86/133.37 | Instantiating formula (33) with all_12_0_8, all_2_3_3, zero, all_2_3_3, all_2_3_3 and discharging atoms addition(all_2_3_3, all_2_3_3) = all_2_3_3, addition(zero, all_2_3_3) = all_12_0_8, yields: % 180.86/133.37 | (156) ? [v0] : (addition(all_12_0_8, all_2_3_3) = v0 & addition(zero, all_2_3_3) = v0) % 180.86/133.37 | % 180.86/133.37 | Instantiating formula (13) with all_38_0_33, all_2_3_3, zero, all_2_3_3, all_2_2_2 and discharging atoms addition(all_2_3_3, all_2_2_2) = all_38_0_33, yields: % 180.86/133.37 | (157) ~ (addition(zero, all_2_3_3) = all_2_3_3) | ? [v0] : (addition(all_2_3_3, all_2_2_2) = v0 & addition(zero, v0) = all_38_0_33) % 180.86/133.37 | % 180.86/133.37 | Instantiating formula (33) with all_2_3_3, all_12_0_8, all_2_3_3, zero, all_2_3_3 and discharging atoms addition(all_2_3_3, zero) = all_2_3_3, addition(zero, all_2_3_3) = all_12_0_8, yields: % 180.86/133.38 | (158) ? [v0] : (addition(all_2_3_3, all_12_0_8) = v0 & addition(all_2_3_3, all_2_3_3) = v0) % 180.86/133.38 | % 180.86/133.38 | Instantiating formula (2) with all_2_3_3, zero yields: % 180.86/133.38 | (159) ~ (addition(zero, all_2_3_3) = all_2_3_3) | leq(zero, all_2_3_3) = 0 % 180.86/133.38 | % 180.86/133.38 | Instantiating (138) with all_120_0_76, all_120_1_77 yields: % 180.86/133.38 | (160) domain(all_120_1_77) = all_120_0_76 & addition(all_40_1_36, all_40_1_36) = all_120_0_76 & addition(all_2_3_3, all_2_3_3) = all_120_1_77 % 180.86/133.38 | % 180.86/133.38 | Applying alpha-rule on (160) yields: % 180.86/133.38 | (161) domain(all_120_1_77) = all_120_0_76 % 180.86/133.38 | (162) addition(all_40_1_36, all_40_1_36) = all_120_0_76 % 180.86/133.38 | (163) addition(all_2_3_3, all_2_3_3) = all_120_1_77 % 180.86/133.38 | % 180.86/133.38 | Instantiating (137) with all_122_0_78, all_122_1_79 yields: % 180.86/133.38 | (164) domain(all_122_1_79) = all_122_0_78 & addition(all_22_2_19, all_40_1_36) = all_122_0_78 & addition(all_2_1_1, all_2_3_3) = all_122_1_79 % 180.86/133.38 | % 180.86/133.38 | Applying alpha-rule on (164) yields: % 180.86/133.38 | (165) domain(all_122_1_79) = all_122_0_78 % 180.86/133.38 | (166) addition(all_22_2_19, all_40_1_36) = all_122_0_78 % 180.86/133.38 | (167) addition(all_2_1_1, all_2_3_3) = all_122_1_79 % 180.86/133.38 | % 180.86/133.38 | Instantiating (148) with all_132_0_87 yields: % 180.86/133.38 | (168) addition(all_2_3_3, all_2_0_0) = all_132_0_87 & addition(all_2_3_3, all_2_1_1) = all_132_0_87 % 180.86/133.38 | % 180.86/133.38 | Applying alpha-rule on (168) yields: % 180.86/133.38 | (169) addition(all_2_3_3, all_2_0_0) = all_132_0_87 % 180.86/133.38 | (170) addition(all_2_3_3, all_2_1_1) = all_132_0_87 % 180.86/133.38 | % 180.86/133.38 | Instantiating (140) with all_186_0_142, all_186_1_143 yields: % 180.86/133.38 | (171) multiplication(all_186_1_143, all_22_1_18) = all_186_0_142 & addition(all_22_0_17, all_22_0_17) = all_186_0_142 & addition(all_2_3_3, all_2_3_3) = all_186_1_143 % 180.86/133.38 | % 180.86/133.38 | Applying alpha-rule on (171) yields: % 180.86/133.38 | (172) multiplication(all_186_1_143, all_22_1_18) = all_186_0_142 % 180.86/133.38 | (173) addition(all_22_0_17, all_22_0_17) = all_186_0_142 % 180.86/133.38 | (174) addition(all_2_3_3, all_2_3_3) = all_186_1_143 % 180.86/133.38 | % 180.86/133.38 | Instantiating (142) with all_200_0_157, all_200_1_158 yields: % 180.86/133.38 | (175) multiplication(all_200_1_158, all_2_5_5) = all_200_0_157 & addition(all_16_0_12, all_16_0_12) = all_200_0_157 & addition(all_2_3_3, all_2_3_3) = all_200_1_158 % 180.86/133.38 | % 180.86/133.38 | Applying alpha-rule on (175) yields: % 180.86/133.38 | (176) multiplication(all_200_1_158, all_2_5_5) = all_200_0_157 % 180.86/133.38 | (177) addition(all_16_0_12, all_16_0_12) = all_200_0_157 % 180.86/133.38 | (178) addition(all_2_3_3, all_2_3_3) = all_200_1_158 % 180.86/133.38 | % 180.86/133.38 | Instantiating (146) with all_248_0_201 yields: % 180.86/133.38 | (179) addition(all_2_1_1, all_2_0_0) = all_248_0_201 & addition(all_2_1_1, all_2_3_3) = all_248_0_201 % 180.86/133.38 | % 180.86/133.38 | Applying alpha-rule on (179) yields: % 180.86/133.38 | (180) addition(all_2_1_1, all_2_0_0) = all_248_0_201 % 180.86/133.38 | (181) addition(all_2_1_1, all_2_3_3) = all_248_0_201 % 180.86/133.38 | % 180.86/133.38 | Instantiating (151) with all_270_0_218 yields: % 180.86/133.38 | (182) addition(all_2_0_0, zero) = all_270_0_218 & addition(all_2_1_1, all_2_3_3) = all_270_0_218 % 180.86/133.38 | % 180.86/133.38 | Applying alpha-rule on (182) yields: % 180.86/133.38 | (183) addition(all_2_0_0, zero) = all_270_0_218 % 180.86/133.38 | (184) addition(all_2_1_1, all_2_3_3) = all_270_0_218 % 180.86/133.38 | % 180.86/133.38 | Instantiating (141) with all_282_0_227, all_282_1_228 yields: % 180.86/133.38 | (185) multiplication(all_282_1_228, all_2_4_4) = all_282_0_227 & addition(all_26_1_23, all_26_1_23) = all_282_0_227 & addition(all_2_3_3, all_2_3_3) = all_282_1_228 % 180.86/133.38 | % 180.86/133.38 | Applying alpha-rule on (185) yields: % 180.86/133.38 | (186) multiplication(all_282_1_228, all_2_4_4) = all_282_0_227 % 180.86/133.38 | (187) addition(all_26_1_23, all_26_1_23) = all_282_0_227 % 180.86/133.38 | (188) addition(all_2_3_3, all_2_3_3) = all_282_1_228 % 180.86/133.38 | % 180.86/133.38 | Instantiating (145) with all_332_0_275 yields: % 180.86/133.38 | (189) addition(all_2_0_0, all_2_3_3) = all_332_0_275 & addition(all_2_3_3, all_2_0_0) = all_332_0_275 % 180.86/133.38 | % 180.86/133.38 | Applying alpha-rule on (189) yields: % 180.86/133.38 | (190) addition(all_2_0_0, all_2_3_3) = all_332_0_275 % 180.86/133.38 | (191) addition(all_2_3_3, all_2_0_0) = all_332_0_275 % 180.86/133.38 | % 180.86/133.38 | Instantiating (149) with all_402_0_337 yields: % 180.86/133.38 | (192) addition(all_2_0_0, all_2_3_3) = all_402_0_337 & addition(all_2_1_1, all_2_3_3) = all_402_0_337 % 180.86/133.38 | % 180.86/133.38 | Applying alpha-rule on (192) yields: % 180.86/133.38 | (193) addition(all_2_0_0, all_2_3_3) = all_402_0_337 % 180.86/133.38 | (194) addition(all_2_1_1, all_2_3_3) = all_402_0_337 % 180.86/133.38 | % 180.86/133.38 | Instantiating (150) with all_412_0_345, all_412_1_346 yields: % 180.86/133.38 | (195) multiplication(all_2_3_3, one) = all_412_0_345 & multiplication(all_2_3_3, one) = all_412_1_346 & addition(all_2_1_1, all_412_0_345) = all_412_1_346 % 180.86/133.38 | % 180.86/133.38 | Applying alpha-rule on (195) yields: % 180.86/133.38 | (196) multiplication(all_2_3_3, one) = all_412_0_345 % 180.86/133.38 | (197) multiplication(all_2_3_3, one) = all_412_1_346 % 180.86/133.38 | (198) addition(all_2_1_1, all_412_0_345) = all_412_1_346 % 180.86/133.38 | % 180.86/133.38 | Instantiating (147) with all_424_0_358 yields: % 180.86/133.38 | (199) addition(all_2_3_3, all_424_0_358) = all_2_0_0 & addition(all_2_3_3, all_2_1_1) = all_424_0_358 % 180.86/133.38 | % 180.86/133.38 | Applying alpha-rule on (199) yields: % 180.86/133.38 | (200) addition(all_2_3_3, all_424_0_358) = all_2_0_0 % 180.86/133.38 | (201) addition(all_2_3_3, all_2_1_1) = all_424_0_358 % 180.86/133.38 | % 180.86/133.38 | Instantiating (144) with all_432_0_365 yields: % 180.95/133.38 | (202) addition(all_2_0_0, all_2_1_1) = all_432_0_365 & addition(all_2_3_3, all_2_1_1) = all_432_0_365 % 180.95/133.38 | % 180.95/133.38 | Applying alpha-rule on (202) yields: % 180.95/133.38 | (203) addition(all_2_0_0, all_2_1_1) = all_432_0_365 % 180.95/133.38 | (204) addition(all_2_3_3, all_2_1_1) = all_432_0_365 % 180.95/133.38 | % 180.95/133.38 | Instantiating (136) with all_482_0_402, all_482_1_403 yields: % 180.95/133.38 | (205) domain(all_482_1_403) = all_482_0_402 & addition(all_40_1_36, all_40_2_37) = all_482_0_402 & addition(all_2_3_3, all_2_0_0) = all_482_1_403 % 180.95/133.38 | % 180.95/133.38 | Applying alpha-rule on (205) yields: % 180.95/133.38 | (206) domain(all_482_1_403) = all_482_0_402 % 180.95/133.38 | (207) addition(all_40_1_36, all_40_2_37) = all_482_0_402 % 180.95/133.38 | (208) addition(all_2_3_3, all_2_0_0) = all_482_1_403 % 180.95/133.38 | % 180.95/133.38 | Instantiating (139) with all_514_0_433, all_514_1_434 yields: % 180.95/133.38 | (209) multiplication(all_514_1_434, all_2_2_2) = all_514_0_433 & addition(all_2_1_1, all_20_1_16) = all_514_0_433 & addition(all_2_3_3, all_2_0_0) = all_514_1_434 % 180.95/133.38 | % 180.95/133.38 | Applying alpha-rule on (209) yields: % 180.95/133.38 | (210) multiplication(all_514_1_434, all_2_2_2) = all_514_0_433 % 180.95/133.39 | (211) addition(all_2_1_1, all_20_1_16) = all_514_0_433 % 180.95/133.39 | (212) addition(all_2_3_3, all_2_0_0) = all_514_1_434 % 180.95/133.39 | % 180.95/133.39 | Instantiating (143) with all_560_0_476 yields: % 180.95/133.39 | (213) addition(all_560_0_476, all_2_1_1) = all_2_0_0 & addition(all_2_3_3, all_2_1_1) = all_560_0_476 % 180.95/133.39 | % 180.95/133.39 | Applying alpha-rule on (213) yields: % 180.95/133.39 | (214) addition(all_560_0_476, all_2_1_1) = all_2_0_0 % 180.95/133.39 | (215) addition(all_2_3_3, all_2_1_1) = all_560_0_476 % 180.95/133.39 | % 180.95/133.39 | Instantiating (158) with all_708_0_607 yields: % 180.95/133.39 | (216) addition(all_2_3_3, all_12_0_8) = all_708_0_607 & addition(all_2_3_3, all_2_3_3) = all_708_0_607 % 180.95/133.39 | % 180.95/133.39 | Applying alpha-rule on (216) yields: % 180.95/133.39 | (217) addition(all_2_3_3, all_12_0_8) = all_708_0_607 % 180.95/133.39 | (218) addition(all_2_3_3, all_2_3_3) = all_708_0_607 % 180.95/133.39 | % 180.95/133.39 | Instantiating (156) with all_724_0_619 yields: % 180.95/133.39 | (219) addition(all_12_0_8, all_2_3_3) = all_724_0_619 & addition(zero, all_2_3_3) = all_724_0_619 % 180.95/133.39 | % 180.95/133.39 | Applying alpha-rule on (219) yields: % 180.95/133.39 | (220) addition(all_12_0_8, all_2_3_3) = all_724_0_619 % 180.95/133.39 | (221) addition(zero, all_2_3_3) = all_724_0_619 % 180.95/133.39 | % 180.95/133.39 | Instantiating (133) with all_732_0_626, all_732_1_627 yields: % 180.95/133.39 | (222) domain(all_732_1_627) = all_732_0_626 & addition(all_2_3_3, all_12_0_8) = all_732_0_626 & addition(all_2_5_5, all_12_1_9) = all_732_1_627 % 180.95/133.39 | % 180.95/133.39 | Applying alpha-rule on (222) yields: % 180.95/133.39 | (223) domain(all_732_1_627) = all_732_0_626 % 180.95/133.39 | (224) addition(all_2_3_3, all_12_0_8) = all_732_0_626 % 180.95/133.39 | (225) addition(all_2_5_5, all_12_1_9) = all_732_1_627 % 180.95/133.39 | % 180.95/133.39 | Instantiating (155) with all_744_0_635 yields: % 180.95/133.39 | (226) addition(all_12_0_8, all_2_1_1) = all_744_0_635 & addition(zero, all_2_0_0) = all_744_0_635 % 180.95/133.39 | % 180.95/133.39 | Applying alpha-rule on (226) yields: % 180.95/133.39 | (227) addition(all_12_0_8, all_2_1_1) = all_744_0_635 % 180.95/133.39 | (228) addition(zero, all_2_0_0) = all_744_0_635 % 180.95/133.39 | % 180.95/133.39 | Instantiating (135) with all_788_0_678, all_788_1_679 yields: % 180.95/133.39 | (229) domain(all_788_1_679) = all_788_0_678 & addition(all_12_0_8, all_12_0_8) = all_788_0_678 & addition(all_12_1_9, all_12_1_9) = all_788_1_679 % 180.95/133.39 | % 180.95/133.39 | Applying alpha-rule on (229) yields: % 180.95/133.39 | (230) domain(all_788_1_679) = all_788_0_678 % 180.95/133.39 | (231) addition(all_12_0_8, all_12_0_8) = all_788_0_678 % 180.95/133.39 | (232) addition(all_12_1_9, all_12_1_9) = all_788_1_679 % 180.95/133.39 | % 180.95/133.39 | Instantiating (134) with all_852_0_731, all_852_1_732 yields: % 180.95/133.39 | (233) domain(all_852_1_732) = all_852_0_731 & addition(all_12_0_8, all_2_3_3) = all_852_0_731 & addition(all_12_1_9, all_2_5_5) = all_852_1_732 % 180.95/133.39 | % 180.95/133.39 | Applying alpha-rule on (233) yields: % 180.95/133.39 | (234) domain(all_852_1_732) = all_852_0_731 % 180.95/133.39 | (235) addition(all_12_0_8, all_2_3_3) = all_852_0_731 % 180.95/133.39 | (236) addition(all_12_1_9, all_2_5_5) = all_852_1_732 % 180.95/133.39 | % 180.95/133.39 +-Applying beta-rule and splitting (159), into two cases. % 180.95/133.39 |-Branch one: % 180.95/133.39 | (237) ~ (addition(zero, all_2_3_3) = all_2_3_3) % 180.95/133.39 | % 180.95/133.39 | Using (152) and (237) yields: % 180.95/133.39 | (238) $false % 180.95/133.39 | % 180.95/133.39 |-The branch is then unsatisfiable % 180.95/133.39 |-Branch two: % 180.95/133.39 | (152) addition(zero, all_2_3_3) = all_2_3_3 % 180.95/133.39 | (240) leq(zero, all_2_3_3) = 0 % 180.95/133.39 | % 180.95/133.39 +-Applying beta-rule and splitting (153), into two cases. % 180.95/133.39 |-Branch one: % 180.95/133.39 | (237) ~ (addition(zero, all_2_3_3) = all_2_3_3) % 180.95/133.39 | % 180.95/133.39 | Using (152) and (237) yields: % 180.95/133.39 | (238) $false % 180.95/133.39 | % 180.95/133.39 |-The branch is then unsatisfiable % 180.95/133.39 |-Branch two: % 180.95/133.39 | (152) addition(zero, all_2_3_3) = all_2_3_3 % 180.95/133.39 | (244) ? [v0] : ? [v1] : (multiplication(all_2_3_3, all_2_5_5) = v1 & multiplication(zero, all_2_5_5) = v0 & addition(v0, v1) = all_16_0_12) % 180.95/133.39 | % 180.95/133.39 +-Applying beta-rule and splitting (154), into two cases. % 180.95/133.39 |-Branch one: % 180.95/133.39 | (237) ~ (addition(zero, all_2_3_3) = all_2_3_3) % 180.95/133.39 | % 180.95/133.39 | Using (152) and (237) yields: % 180.95/133.39 | (238) $false % 180.95/133.39 | % 180.95/133.39 |-The branch is then unsatisfiable % 180.95/133.39 |-Branch two: % 180.95/133.39 | (152) addition(zero, all_2_3_3) = all_2_3_3 % 180.95/133.39 | (248) ? [v0] : (addition(all_2_3_3, all_2_1_1) = v0 & addition(zero, v0) = all_2_0_0) % 180.95/133.39 | % 180.95/133.39 | Instantiating (248) with all_1040_0_853 yields: % 180.95/133.39 | (249) addition(all_2_3_3, all_2_1_1) = all_1040_0_853 & addition(zero, all_1040_0_853) = all_2_0_0 % 180.95/133.39 | % 180.95/133.39 | Applying alpha-rule on (249) yields: % 180.95/133.39 | (250) addition(all_2_3_3, all_2_1_1) = all_1040_0_853 % 180.95/133.39 | (251) addition(zero, all_1040_0_853) = all_2_0_0 % 180.95/133.39 | % 180.95/133.39 +-Applying beta-rule and splitting (157), into two cases. % 180.95/133.39 |-Branch one: % 180.95/133.39 | (237) ~ (addition(zero, all_2_3_3) = all_2_3_3) % 180.95/133.39 | % 180.95/133.39 | Using (152) and (237) yields: % 180.95/133.39 | (238) $false % 180.95/133.39 | % 180.95/133.39 |-The branch is then unsatisfiable % 180.95/133.39 |-Branch two: % 180.95/133.39 | (152) addition(zero, all_2_3_3) = all_2_3_3 % 180.95/133.39 | (255) ? [v0] : (addition(all_2_3_3, all_2_2_2) = v0 & addition(zero, v0) = all_38_0_33) % 180.95/133.39 | % 180.95/133.39 +-Applying beta-rule and splitting (120), into two cases. % 180.95/133.39 |-Branch one: % 180.95/133.39 | (237) ~ (addition(zero, all_2_3_3) = all_2_3_3) % 180.95/133.39 | % 180.95/133.39 | Using (152) and (237) yields: % 180.95/133.39 | (238) $false % 180.95/133.39 | % 180.95/133.39 |-The branch is then unsatisfiable % 180.95/133.39 |-Branch two: % 180.95/133.39 | (152) addition(zero, all_2_3_3) = all_2_3_3 % 180.95/133.40 | (259) all_12_0_8 = all_2_3_3 % 180.95/133.40 | % 180.95/133.40 | From (259)(259) and (231) follows: % 180.95/133.40 | (260) addition(all_2_3_3, all_2_3_3) = all_788_0_678 % 180.95/133.40 | % 180.95/133.40 | From (259) and (227) follows: % 180.95/133.40 | (261) addition(all_2_3_3, all_2_1_1) = all_744_0_635 % 180.95/133.40 | % 180.95/133.40 | From (259) and (235) follows: % 180.95/133.40 | (262) addition(all_2_3_3, all_2_3_3) = all_852_0_731 % 180.95/133.40 | % 180.95/133.40 | From (259) and (220) follows: % 180.95/133.40 | (263) addition(all_2_3_3, all_2_3_3) = all_724_0_619 % 180.95/133.40 | % 180.95/133.40 | From (259) and (224) follows: % 180.95/133.40 | (264) addition(all_2_3_3, all_2_3_3) = all_732_0_626 % 180.95/133.40 | % 180.95/133.40 | From (259) and (217) follows: % 180.95/133.40 | (218) addition(all_2_3_3, all_2_3_3) = all_708_0_607 % 180.95/133.40 | % 180.95/133.40 | Instantiating formula (36) with all_412_0_345, all_2_3_3 and discharging atoms multiplication(all_2_3_3, one) = all_412_0_345, yields: % 180.95/133.40 | (266) all_412_0_345 = all_2_3_3 % 180.95/133.40 | % 180.95/133.40 | Instantiating formula (9) with all_2_3_3, one, all_412_1_346, all_412_0_345 and discharging atoms multiplication(all_2_3_3, one) = all_412_0_345, multiplication(all_2_3_3, one) = all_412_1_346, yields: % 180.95/133.40 | (267) all_412_0_345 = all_412_1_346 % 180.95/133.40 | % 180.95/133.40 | Instantiating formula (35) with all_2_0_0, all_2_3_3, all_332_0_275, all_402_0_337 and discharging atoms addition(all_2_0_0, all_2_3_3) = all_402_0_337, addition(all_2_0_0, all_2_3_3) = all_332_0_275, yields: % 180.95/133.40 | (268) all_402_0_337 = all_332_0_275 % 180.95/133.40 | % 180.95/133.40 | Instantiating formula (35) with all_2_1_1, all_2_3_3, all_270_0_218, all_402_0_337 and discharging atoms addition(all_2_1_1, all_2_3_3) = all_402_0_337, addition(all_2_1_1, all_2_3_3) = all_270_0_218, yields: % 180.95/133.40 | (269) all_402_0_337 = all_270_0_218 % 180.95/133.40 | % 180.95/133.40 | Instantiating formula (35) with all_2_1_1, all_2_3_3, all_248_0_201, all_412_1_346 and discharging atoms addition(all_2_1_1, all_2_3_3) = all_248_0_201, yields: % 180.95/133.40 | (270) all_412_1_346 = all_248_0_201 | ~ (addition(all_2_1_1, all_2_3_3) = all_412_1_346) % 180.95/133.40 | % 180.95/133.40 | Instantiating formula (35) with all_2_1_1, all_2_3_3, all_248_0_201, all_270_0_218 and discharging atoms addition(all_2_1_1, all_2_3_3) = all_270_0_218, addition(all_2_1_1, all_2_3_3) = all_248_0_201, yields: % 180.95/133.40 | (271) all_270_0_218 = all_248_0_201 % 180.95/133.40 | % 180.95/133.40 | Instantiating formula (35) with all_2_1_1, all_2_3_3, all_122_1_79, all_402_0_337 and discharging atoms addition(all_2_1_1, all_2_3_3) = all_402_0_337, addition(all_2_1_1, all_2_3_3) = all_122_1_79, yields: % 180.95/133.40 | (272) all_402_0_337 = all_122_1_79 % 180.95/133.40 | % 180.95/133.40 | Instantiating formula (35) with all_2_3_3, all_2_0_0, all_482_1_403, all_514_1_434 and discharging atoms addition(all_2_3_3, all_2_0_0) = all_514_1_434, addition(all_2_3_3, all_2_0_0) = all_482_1_403, yields: % 180.95/133.40 | (273) all_514_1_434 = all_482_1_403 % 180.95/133.40 | % 180.95/133.40 | Instantiating formula (35) with all_2_3_3, all_2_0_0, all_332_0_275, all_482_1_403 and discharging atoms addition(all_2_3_3, all_2_0_0) = all_482_1_403, addition(all_2_3_3, all_2_0_0) = all_332_0_275, yields: % 180.95/133.40 | (274) all_482_1_403 = all_332_0_275 % 180.95/133.40 | % 180.95/133.40 | Instantiating formula (35) with all_2_3_3, all_2_0_0, all_132_0_87, all_514_1_434 and discharging atoms addition(all_2_3_3, all_2_0_0) = all_514_1_434, addition(all_2_3_3, all_2_0_0) = all_132_0_87, yields: % 180.95/133.40 | (275) all_514_1_434 = all_132_0_87 % 180.95/133.40 | % 180.95/133.40 | Instantiating formula (35) with all_2_3_3, all_2_1_1, all_744_0_635, all_2_0_0 and discharging atoms addition(all_2_3_3, all_2_1_1) = all_744_0_635, addition(all_2_3_3, all_2_1_1) = all_2_0_0, yields: % 180.95/133.40 | (276) all_744_0_635 = all_2_0_0 % 180.95/133.40 | % 180.95/133.40 | Instantiating formula (35) with all_2_3_3, all_2_1_1, all_560_0_476, all_132_0_87 and discharging atoms addition(all_2_3_3, all_2_1_1) = all_560_0_476, addition(all_2_3_3, all_2_1_1) = all_132_0_87, yields: % 180.95/133.40 | (277) all_560_0_476 = all_132_0_87 % 180.95/133.40 | % 180.95/133.40 | Instantiating formula (35) with all_2_3_3, all_2_1_1, all_560_0_476, all_1040_0_853 and discharging atoms addition(all_2_3_3, all_2_1_1) = all_1040_0_853, addition(all_2_3_3, all_2_1_1) = all_560_0_476, yields: % 180.95/133.40 | (278) all_1040_0_853 = all_560_0_476 % 180.95/133.40 | % 180.95/133.40 | Instantiating formula (35) with all_2_3_3, all_2_1_1, all_432_0_365, all_744_0_635 and discharging atoms addition(all_2_3_3, all_2_1_1) = all_744_0_635, addition(all_2_3_3, all_2_1_1) = all_432_0_365, yields: % 180.95/133.40 | (279) all_744_0_635 = all_432_0_365 % 180.95/133.40 | % 180.95/133.40 | Instantiating formula (35) with all_2_3_3, all_2_1_1, all_432_0_365, all_560_0_476 and discharging atoms addition(all_2_3_3, all_2_1_1) = all_560_0_476, addition(all_2_3_3, all_2_1_1) = all_432_0_365, yields: % 180.95/133.40 | (280) all_560_0_476 = all_432_0_365 % 180.95/133.40 | % 180.95/133.40 | Instantiating formula (35) with all_2_3_3, all_2_1_1, all_424_0_358, all_1040_0_853 and discharging atoms addition(all_2_3_3, all_2_1_1) = all_1040_0_853, addition(all_2_3_3, all_2_1_1) = all_424_0_358, yields: % 180.95/133.40 | (281) all_1040_0_853 = all_424_0_358 % 180.95/133.40 | % 180.95/133.40 | Instantiating formula (35) with all_2_3_3, all_2_3_3, all_732_0_626, all_788_0_678 and discharging atoms addition(all_2_3_3, all_2_3_3) = all_788_0_678, addition(all_2_3_3, all_2_3_3) = all_732_0_626, yields: % 180.95/133.40 | (282) all_788_0_678 = all_732_0_626 % 180.95/133.40 | % 180.95/133.40 | Instantiating formula (35) with all_2_3_3, all_2_3_3, all_724_0_619, all_852_0_731 and discharging atoms addition(all_2_3_3, all_2_3_3) = all_852_0_731, addition(all_2_3_3, all_2_3_3) = all_724_0_619, yields: % 180.95/133.40 | (283) all_852_0_731 = all_724_0_619 % 180.95/133.40 | % 180.95/133.40 | Instantiating formula (35) with all_2_3_3, all_2_3_3, all_724_0_619, all_732_0_626 and discharging atoms addition(all_2_3_3, all_2_3_3) = all_732_0_626, addition(all_2_3_3, all_2_3_3) = all_724_0_619, yields: % 180.95/133.40 | (284) all_732_0_626 = all_724_0_619 % 180.95/133.40 | % 180.95/133.40 | Instantiating formula (35) with all_2_3_3, all_2_3_3, all_708_0_607, all_852_0_731 and discharging atoms addition(all_2_3_3, all_2_3_3) = all_852_0_731, addition(all_2_3_3, all_2_3_3) = all_708_0_607, yields: % 180.95/133.40 | (285) all_852_0_731 = all_708_0_607 % 180.95/133.40 | % 180.95/133.40 | Instantiating formula (35) with all_2_3_3, all_2_3_3, all_282_1_228, all_852_0_731 and discharging atoms addition(all_2_3_3, all_2_3_3) = all_852_0_731, addition(all_2_3_3, all_2_3_3) = all_282_1_228, yields: % 180.95/133.40 | (286) all_852_0_731 = all_282_1_228 % 180.95/133.40 | % 180.95/133.40 | Instantiating formula (35) with all_2_3_3, all_2_3_3, all_200_1_158, all_282_1_228 and discharging atoms addition(all_2_3_3, all_2_3_3) = all_282_1_228, addition(all_2_3_3, all_2_3_3) = all_200_1_158, yields: % 180.95/133.40 | (287) all_282_1_228 = all_200_1_158 % 180.95/133.40 | % 180.95/133.40 | Instantiating formula (4) with all_200_1_158, all_2_3_3 and discharging atoms addition(all_2_3_3, all_2_3_3) = all_200_1_158, yields: % 180.95/133.40 | (288) all_200_1_158 = all_2_3_3 % 180.95/133.40 | % 180.95/133.40 | Instantiating formula (35) with all_2_3_3, all_2_3_3, all_186_1_143, all_788_0_678 and discharging atoms addition(all_2_3_3, all_2_3_3) = all_788_0_678, addition(all_2_3_3, all_2_3_3) = all_186_1_143, yields: % 180.95/133.40 | (289) all_788_0_678 = all_186_1_143 % 180.95/133.40 | % 180.95/133.40 | Instantiating formula (35) with all_2_3_3, all_2_3_3, all_120_1_77, all_200_1_158 and discharging atoms addition(all_2_3_3, all_2_3_3) = all_200_1_158, addition(all_2_3_3, all_2_3_3) = all_120_1_77, yields: % 180.95/133.40 | (290) all_200_1_158 = all_120_1_77 % 180.95/133.40 | % 180.95/133.40 | Using (163) and (109) yields: % 180.95/133.40 | (291) ~ (all_120_1_77 = all_2_0_0) % 180.95/133.40 | % 180.95/133.40 | Combining equations (278,281) yields a new equation: % 180.95/133.40 | (292) all_560_0_476 = all_424_0_358 % 180.95/133.40 | % 180.95/133.40 | Simplifying 292 yields: % 180.95/133.40 | (293) all_560_0_476 = all_424_0_358 % 180.95/133.41 | % 180.95/133.41 | Combining equations (283,285) yields a new equation: % 180.95/133.41 | (294) all_724_0_619 = all_708_0_607 % 180.95/133.41 | % 180.95/133.41 | Simplifying 294 yields: % 180.95/133.41 | (295) all_724_0_619 = all_708_0_607 % 180.95/133.41 | % 180.95/133.41 | Combining equations (286,285) yields a new equation: % 180.95/133.41 | (296) all_708_0_607 = all_282_1_228 % 180.95/133.41 | % 180.95/133.41 | Combining equations (282,289) yields a new equation: % 180.95/133.41 | (297) all_732_0_626 = all_186_1_143 % 180.95/133.41 | % 180.95/133.41 | Simplifying 297 yields: % 180.95/133.41 | (298) all_732_0_626 = all_186_1_143 % 180.95/133.41 | % 180.95/133.41 | Combining equations (279,276) yields a new equation: % 180.95/133.41 | (299) all_432_0_365 = all_2_0_0 % 180.95/133.41 | % 180.95/133.41 | Simplifying 299 yields: % 180.95/133.41 | (300) all_432_0_365 = all_2_0_0 % 180.95/133.41 | % 180.95/133.41 | Combining equations (284,298) yields a new equation: % 180.95/133.41 | (301) all_724_0_619 = all_186_1_143 % 180.95/133.41 | % 180.95/133.41 | Simplifying 301 yields: % 180.95/133.41 | (302) all_724_0_619 = all_186_1_143 % 180.95/133.41 | % 180.95/133.41 | Combining equations (295,302) yields a new equation: % 180.95/133.41 | (303) all_708_0_607 = all_186_1_143 % 180.95/133.41 | % 180.95/133.41 | Simplifying 303 yields: % 180.95/133.41 | (304) all_708_0_607 = all_186_1_143 % 180.95/133.41 | % 180.95/133.41 | Combining equations (296,304) yields a new equation: % 180.95/133.41 | (305) all_282_1_228 = all_186_1_143 % 180.95/133.41 | % 180.95/133.41 | Simplifying 305 yields: % 180.95/133.41 | (306) all_282_1_228 = all_186_1_143 % 180.95/133.41 | % 180.95/133.41 | Combining equations (280,293) yields a new equation: % 180.95/133.41 | (307) all_432_0_365 = all_424_0_358 % 180.95/133.41 | % 180.95/133.41 | Simplifying 307 yields: % 180.95/133.41 | (308) all_432_0_365 = all_424_0_358 % 180.95/133.41 | % 180.95/133.41 | Combining equations (277,293) yields a new equation: % 180.95/133.41 | (309) all_424_0_358 = all_132_0_87 % 180.95/133.41 | % 180.95/133.41 | Combining equations (273,275) yields a new equation: % 180.95/133.41 | (310) all_482_1_403 = all_132_0_87 % 180.95/133.41 | % 180.95/133.41 | Simplifying 310 yields: % 180.95/133.41 | (311) all_482_1_403 = all_132_0_87 % 180.95/133.41 | % 180.95/133.41 | Combining equations (274,311) yields a new equation: % 180.95/133.41 | (312) all_332_0_275 = all_132_0_87 % 180.95/133.41 | % 180.95/133.41 | Simplifying 312 yields: % 180.95/133.41 | (313) all_332_0_275 = all_132_0_87 % 180.95/133.41 | % 180.95/133.41 | Combining equations (308,300) yields a new equation: % 180.95/133.41 | (314) all_424_0_358 = all_2_0_0 % 180.95/133.41 | % 180.95/133.41 | Simplifying 314 yields: % 180.95/133.41 | (315) all_424_0_358 = all_2_0_0 % 180.95/133.41 | % 180.95/133.41 | Combining equations (309,315) yields a new equation: % 180.95/133.41 | (316) all_132_0_87 = all_2_0_0 % 180.95/133.41 | % 180.95/133.41 | Simplifying 316 yields: % 180.95/133.41 | (317) all_132_0_87 = all_2_0_0 % 180.95/133.41 | % 180.95/133.41 | Combining equations (267,266) yields a new equation: % 180.95/133.41 | (318) all_412_1_346 = all_2_3_3 % 180.95/133.41 | % 180.95/133.41 | Simplifying 318 yields: % 180.95/133.41 | (319) all_412_1_346 = all_2_3_3 % 180.95/133.41 | % 180.95/133.41 | Combining equations (268,272) yields a new equation: % 180.95/133.41 | (320) all_332_0_275 = all_122_1_79 % 180.95/133.41 | % 180.95/133.41 | Simplifying 320 yields: % 180.95/133.41 | (321) all_332_0_275 = all_122_1_79 % 180.95/133.41 | % 180.95/133.41 | Combining equations (269,272) yields a new equation: % 180.95/133.41 | (322) all_270_0_218 = all_122_1_79 % 180.95/133.41 | % 180.95/133.41 | Simplifying 322 yields: % 180.95/133.41 | (323) all_270_0_218 = all_122_1_79 % 180.95/133.41 | % 180.95/133.41 | Combining equations (313,321) yields a new equation: % 180.95/133.41 | (324) all_132_0_87 = all_122_1_79 % 180.95/133.41 | % 180.95/133.41 | Simplifying 324 yields: % 180.95/133.41 | (325) all_132_0_87 = all_122_1_79 % 180.95/133.41 | % 180.95/133.41 | Combining equations (287,306) yields a new equation: % 180.95/133.41 | (326) all_200_1_158 = all_186_1_143 % 180.95/133.41 | % 180.95/133.41 | Simplifying 326 yields: % 180.95/133.41 | (327) all_200_1_158 = all_186_1_143 % 180.95/133.41 | % 180.95/133.41 | Combining equations (271,323) yields a new equation: % 180.95/133.41 | (328) all_248_0_201 = all_122_1_79 % 180.95/133.41 | % 180.95/133.41 | Simplifying 328 yields: % 180.95/133.41 | (329) all_248_0_201 = all_122_1_79 % 180.95/133.41 | % 180.95/133.41 | Combining equations (288,327) yields a new equation: % 180.95/133.41 | (330) all_186_1_143 = all_2_3_3 % 180.95/133.41 | % 180.95/133.41 | Combining equations (290,327) yields a new equation: % 180.95/133.41 | (331) all_186_1_143 = all_120_1_77 % 180.95/133.41 | % 180.95/133.41 | Combining equations (331,330) yields a new equation: % 180.95/133.41 | (332) all_120_1_77 = all_2_3_3 % 180.95/133.41 | % 180.95/133.41 | Simplifying 332 yields: % 180.95/133.41 | (333) all_120_1_77 = all_2_3_3 % 180.95/133.41 | % 180.95/133.41 | Combining equations (325,317) yields a new equation: % 180.95/133.41 | (334) all_122_1_79 = all_2_0_0 % 180.95/133.41 | % 180.95/133.41 | Simplifying 334 yields: % 180.95/133.41 | (335) all_122_1_79 = all_2_0_0 % 180.95/133.41 | % 180.95/133.41 | Combining equations (335,329) yields a new equation: % 180.95/133.41 | (336) all_248_0_201 = all_2_0_0 % 180.95/133.41 | % 180.95/133.42 | Equations (333) can reduce 291 to: % 180.95/133.42 | (337) ~ (all_2_0_0 = all_2_3_3) % 180.95/133.42 | % 180.95/133.42 | Simplifying 337 yields: % 180.95/133.42 | (44) ~ (all_2_0_0 = all_2_3_3) % 180.95/133.42 | % 180.95/133.42 | From (266)(319) and (198) follows: % 180.95/133.42 | (339) addition(all_2_1_1, all_2_3_3) = all_2_3_3 % 180.95/133.42 | % 180.95/133.42 +-Applying beta-rule and splitting (270), into two cases. % 180.95/133.42 |-Branch one: % 181.11/133.42 | (340) ~ (addition(all_2_1_1, all_2_3_3) = all_412_1_346) % 181.11/133.42 | % 181.11/133.42 | From (319) and (340) follows: % 181.11/133.42 | (341) ~ (addition(all_2_1_1, all_2_3_3) = all_2_3_3) % 181.11/133.42 | % 181.11/133.42 | Using (339) and (341) yields: % 181.11/133.42 | (238) $false % 181.11/133.42 | % 181.11/133.42 |-The branch is then unsatisfiable % 181.11/133.42 |-Branch two: % 181.11/133.42 | (343) addition(all_2_1_1, all_2_3_3) = all_412_1_346 % 181.11/133.42 | (344) all_412_1_346 = all_248_0_201 % 181.11/133.42 | % 181.11/133.42 | Combining equations (319,344) yields a new equation: % 181.11/133.42 | (345) all_248_0_201 = all_2_3_3 % 181.11/133.42 | % 181.11/133.42 | Combining equations (345,336) yields a new equation: % 181.11/133.42 | (346) all_2_0_0 = all_2_3_3 % 181.11/133.42 | % 181.11/133.42 | Equations (346) can reduce 44 to: % 181.11/133.42 | (347) $false % 181.11/133.42 | % 181.11/133.42 |-The branch is then unsatisfiable % 181.11/133.42 |-Branch two: % 181.11/133.42 | (348) addition(all_2_3_3, all_2_3_3) = all_2_0_0 % 181.11/133.42 | (346) all_2_0_0 = all_2_3_3 % 181.11/133.42 | % 181.11/133.42 | Equations (346) can reduce 44 to: % 181.11/133.42 | (347) $false % 181.11/133.42 | % 181.11/133.42 |-The branch is then unsatisfiable % 181.11/133.42 % SZS output end Proof for theBenchmark % 181.11/133.42 % 181.11/133.42 132824ms %------------------------------------------------------------------------------