%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : KLE083+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n015.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:17 EDT 2022 % Result : Theorem 34.00s 13.55s % Output : Proof 66.00s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : KLE083+1 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.14/0.34 % Computer : n015.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Thu Jun 16 15:44:11 EDT 2022 % 0.14/0.34 % CPUTime : % 0.20/0.60 ____ _ % 0.20/0.60 ___ / __ \_____(_)___ ________ __________ % 0.20/0.60 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.20/0.60 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.20/0.60 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.20/0.60 % 0.20/0.60 A Theorem Prover for First-Order Logic % 0.20/0.60 (ePrincess v.1.0) % 0.20/0.60 % 0.20/0.60 (c) Philipp Rümmer, 2009-2015 % 0.20/0.60 (c) Peter Backeman, 2014-2015 % 0.20/0.60 (contributions by Angelo Brillout, Peter Baumgartner) % 0.20/0.60 Free software under GNU Lesser General Public License (LGPL). % 0.20/0.60 Bug reports to peter@backeman.se % 0.20/0.60 % 0.20/0.60 For more information, visit http://user.uu.se/~petba168/breu/ % 0.20/0.60 % 0.20/0.60 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.71/0.65 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.53/0.92 Prover 0: Preprocessing ... % 2.37/1.18 Prover 0: Constructing countermodel ... % 10.79/5.94 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 10.79/5.97 Prover 1: Preprocessing ... % 11.00/6.07 Prover 1: Constructing countermodel ... % 11.64/6.16 Prover 1: gave up % 11.64/6.16 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 11.64/6.18 Prover 2: Preprocessing ... % 12.08/6.24 Prover 2: Warning: ignoring some quantifiers % 12.08/6.24 Prover 2: Constructing countermodel ... % 18.92/7.91 Prover 3: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 18.92/7.93 Prover 3: Preprocessing ... % 19.37/8.00 Prover 3: Constructing countermodel ... % 19.74/8.06 Prover 3: gave up % 19.74/8.06 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=complete % 19.74/8.08 Prover 4: Preprocessing ... % 20.20/8.14 Prover 4: Warning: ignoring some quantifiers % 20.20/8.15 Prover 4: Constructing countermodel ... % 27.38/10.35 Prover 0: stopped % 27.84/10.55 Prover 5: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=none +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allMinimal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 27.84/10.58 Prover 5: Preprocessing ... % 28.08/10.63 Prover 5: Constructing countermodel ... % 34.00/13.54 Prover 5: proved (2989ms) % 34.00/13.54 Prover 2: stopped % 34.00/13.54 Prover 4: stopped % 34.00/13.54 % 34.00/13.54 No countermodel exists, formula is valid % 34.00/13.55 % SZS status Theorem for theBenchmark % 34.00/13.55 % 34.00/13.55 Generating proof ... found it (size 176) % 65.57/31.84 % 65.57/31.84 % SZS output start Proof for theBenchmark % 65.57/31.84 Assumed formulas after preprocessing and simplification: % 65.57/31.84 | (0) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (coantidomain(v2) = v3) | ~ (coantidomain(v0) = v2) | ~ (multiplication(v3, v1) = v4) | ? [v5] : ? [v6] : ? [v7] : (coantidomain(v5) = v6 & coantidomain(v4) = v7 & multiplication(v0, v1) = v5 & addition(v6, v7) = v7)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (antidomain(v2) = v3) | ~ (antidomain(v1) = v2) | ~ (multiplication(v0, v3) = v4) | ? [v5] : ? [v6] : ? [v7] : (antidomain(v5) = v6 & antidomain(v4) = v7 & multiplication(v0, v1) = v5 & addition(v6, v7) = v7)) & ! [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] : (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 | ~ (codomain(v2) = v1) | ~ (codomain(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (coantidomain(v2) = v1) | ~ (coantidomain(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (domain(v2) = v1) | ~ (domain(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (antidomain(v2) = v1) | ~ (antidomain(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (multiplication(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : (coantidomain(v6) = v7 & coantidomain(v4) = v5 & coantidomain(v2) = v3 & coantidomain(v0) = v4 & multiplication(v5, v1) = v6 & addition(v3, v7) = v7)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (multiplication(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : (antidomain(v6) = v7 & antidomain(v4) = v5 & antidomain(v2) = v3 & antidomain(v1) = v4 & multiplication(v0, v5) = v6 & addition(v3, v7) = v7)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (addition(v1, v0) = v2) | addition(v0, v1) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (addition(v0, v1) = v2) | addition(v1, v0) = v2) & ! [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] : ( ~ (codomain(v0) = v1) | ? [v2] : (coantidomain(v2) = v1 & coantidomain(v0) = v2)) & ! [v0] : ! [v1] : ( ~ (coantidomain(v0) = v1) | multiplication(v0, v1) = zero) & ! [v0] : ! [v1] : ( ~ (coantidomain(v0) = v1) | ? [v2] : (codomain(v0) = v2 & coantidomain(v1) = v2)) & ! [v0] : ! [v1] : ( ~ (coantidomain(v0) = v1) | ? [v2] : (coantidomain(v1) = v2 & addition(v2, v1) = one)) & ! [v0] : ! [v1] : ( ~ (domain(v0) = v1) | ? [v2] : (antidomain(v2) = v1 & antidomain(v0) = v2)) & ! [v0] : ! [v1] : ( ~ (antidomain(v0) = v1) | multiplication(v1, v0) = zero) & ! [v0] : ! [v1] : ( ~ (antidomain(v0) = v1) | ? [v2] : (domain(v0) = v2 & antidomain(v1) = v2)) & ! [v0] : ! [v1] : ( ~ (antidomain(v0) = v1) | ? [v2] : (antidomain(v1) = v2 & addition(v2, v1) = one)) & ! [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) % 65.62/31.88 | Applying alpha-rule on (0) yields: % 65.62/31.88 | (1) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (antidomain(v2) = v1) | ~ (antidomain(v2) = v0)) % 65.62/31.88 | (2) ! [v0] : ! [v1] : ( ~ (domain(v0) = v1) | ? [v2] : (antidomain(v2) = v1 & antidomain(v0) = v2)) % 65.62/31.89 | (3) ! [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)) % 65.62/31.89 | (4) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ (leq(v0, v1) = v2) | ? [v3] : ( ~ (v3 = v1) & addition(v0, v1) = v3)) % 65.62/31.89 | (5) ! [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)) % 65.62/31.89 | (6) ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ (addition(v0, v1) = v2) | ? [v3] : ( ~ (v3 = 0) & leq(v0, v1) = v3)) % 65.62/31.89 | (7) ! [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)) % 65.62/31.89 | (8) ! [v0] : ! [v1] : (v1 = v0 | ~ (multiplication(v0, one) = v1)) % 65.62/31.89 | (9) ! [v0] : ! [v1] : (v1 = zero | ~ (multiplication(v0, zero) = v1)) % 65.62/31.89 | (10) ! [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)) % 65.62/31.89 | (11) ! [v0] : ! [v1] : ( ~ (coantidomain(v0) = v1) | multiplication(v0, v1) = zero) % 65.62/31.89 | (12) ! [v0] : ! [v1] : (v1 = v0 | ~ (multiplication(one, v0) = v1)) % 65.62/31.89 | (13) ! [v0] : ! [v1] : ( ~ (addition(v0, v1) = v1) | leq(v0, v1) = 0) % 65.62/31.89 | (14) ! [v0] : ! [v1] : ( ~ (leq(v0, v1) = 0) | addition(v0, v1) = v1) % 65.62/31.89 | (15) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (addition(v3, v0) = v4) | ~ (addition(v2, v1) = v3) | ? [v5] : (addition(v2, v5) = v4 & addition(v1, v0) = v5)) % 65.62/31.89 | (16) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (leq(v3, v2) = v1) | ~ (leq(v3, v2) = v0)) % 65.62/31.89 | (17) ! [v0] : ! [v1] : ! [v2] : ( ~ (multiplication(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : (antidomain(v6) = v7 & antidomain(v4) = v5 & antidomain(v2) = v3 & antidomain(v1) = v4 & multiplication(v0, v5) = v6 & addition(v3, v7) = v7)) % 65.62/31.89 | (18) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (multiplication(v3, v2) = v1) | ~ (multiplication(v3, v2) = v0)) % 65.62/31.89 | (19) ! [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)) % 65.62/31.89 | (20) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (domain(v2) = v1) | ~ (domain(v2) = v0)) % 65.62/31.89 | (21) ! [v0] : ! [v1] : (v1 = v0 | ~ (addition(v0, zero) = v1)) % 65.62/31.89 | (22) ! [v0] : ! [v1] : ( ~ (antidomain(v0) = v1) | ? [v2] : (antidomain(v1) = v2 & addition(v2, v1) = one)) % 65.62/31.89 | (23) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (codomain(v2) = v1) | ~ (codomain(v2) = v0)) % 65.62/31.89 | (24) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (addition(v3, v2) = v1) | ~ (addition(v3, v2) = v0)) % 65.62/31.89 | (25) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (antidomain(v2) = v3) | ~ (antidomain(v1) = v2) | ~ (multiplication(v0, v3) = v4) | ? [v5] : ? [v6] : ? [v7] : (antidomain(v5) = v6 & antidomain(v4) = v7 & multiplication(v0, v1) = v5 & addition(v6, v7) = v7)) % 65.62/31.89 | (26) ! [v0] : ! [v1] : ( ~ (codomain(v0) = v1) | ? [v2] : (coantidomain(v2) = v1 & coantidomain(v0) = v2)) % 65.62/31.89 | (27) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (coantidomain(v2) = v1) | ~ (coantidomain(v2) = v0)) % 65.62/31.89 | (28) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (coantidomain(v2) = v3) | ~ (coantidomain(v0) = v2) | ~ (multiplication(v3, v1) = v4) | ? [v5] : ? [v6] : ? [v7] : (coantidomain(v5) = v6 & coantidomain(v4) = v7 & multiplication(v0, v1) = v5 & addition(v6, v7) = v7)) % 65.62/31.89 | (29) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v1, v2) = v3) | ~ (multiplication(v0, v1) = v4) | ? [v5] : (multiplication(v4, v2) = v5 & multiplication(v0, v3) = v5)) % 65.62/31.89 | (30) ! [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)) % 65.62/31.90 | (31) ! [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)) % 65.62/31.90 | (32) ? [v0] : ? [v1] : ? [v2] : ( ~ (v2 = v0) & domain(v0) = v1 & multiplication(v1, v0) = v2) % 65.62/31.90 | (33) ! [v0] : ! [v1] : ( ~ (coantidomain(v0) = v1) | ? [v2] : (coantidomain(v1) = v2 & addition(v2, v1) = one)) % 65.62/31.90 | (34) ! [v0] : ! [v1] : (v1 = v0 | ~ (addition(v0, v0) = v1)) % 65.62/31.90 | (35) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (addition(v2, v3) = v4) | ~ (addition(v1, v0) = v3) | ? [v5] : (addition(v5, v0) = v4 & addition(v2, v1) = v5)) % 65.62/31.90 | (36) ! [v0] : ! [v1] : ( ~ (coantidomain(v0) = v1) | ? [v2] : (codomain(v0) = v2 & coantidomain(v1) = v2)) % 65.62/31.90 | (37) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (addition(v2, v1) = v4) | ~ (addition(v1, v0) = v3) | ? [v5] : (addition(v4, v0) = v5 & addition(v2, v3) = v5)) % 65.62/31.90 | (38) ! [v0] : ! [v1] : ! [v2] : ( ~ (addition(v0, v1) = v2) | addition(v1, v0) = v2) % 65.62/31.90 | (39) ! [v0] : ! [v1] : ! [v2] : ( ~ (addition(v1, v0) = v2) | addition(v0, v1) = v2) % 65.62/31.90 | (40) ! [v0] : ! [v1] : ( ~ (antidomain(v0) = v1) | multiplication(v1, v0) = zero) % 65.62/31.90 | (41) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v3, v2) = v4) | ~ (multiplication(v0, v1) = v3) | ? [v5] : (multiplication(v1, v2) = v5 & multiplication(v0, v5) = v4)) % 65.62/31.90 | (42) ! [v0] : ! [v1] : ( ~ (antidomain(v0) = v1) | ? [v2] : (domain(v0) = v2 & antidomain(v1) = v2)) % 65.62/31.90 | (43) ! [v0] : ! [v1] : (v1 = zero | ~ (multiplication(zero, v0) = v1)) % 65.62/31.90 | (44) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (multiplication(v1, v2) = v3) | ~ (multiplication(v0, v3) = v4) | ? [v5] : (multiplication(v5, v2) = v4 & multiplication(v0, v1) = v5)) % 65.62/31.90 | (45) ! [v0] : ! [v1] : ! [v2] : ( ~ (multiplication(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : (coantidomain(v6) = v7 & coantidomain(v4) = v5 & coantidomain(v2) = v3 & coantidomain(v0) = v4 & multiplication(v5, v1) = v6 & addition(v3, v7) = v7)) % 65.62/31.90 | (46) ! [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)) % 65.62/31.90 | % 65.62/31.90 | Instantiating (32) with all_1_0_0, all_1_1_1, all_1_2_2 yields: % 65.62/31.90 | (47) ~ (all_1_0_0 = all_1_2_2) & domain(all_1_2_2) = all_1_1_1 & multiplication(all_1_1_1, all_1_2_2) = all_1_0_0 % 65.62/31.90 | % 65.62/31.90 | Applying alpha-rule on (47) yields: % 65.62/31.90 | (48) ~ (all_1_0_0 = all_1_2_2) % 65.62/31.90 | (49) domain(all_1_2_2) = all_1_1_1 % 65.62/31.90 | (50) multiplication(all_1_1_1, all_1_2_2) = all_1_0_0 % 65.62/31.90 | % 65.62/31.90 | Instantiating formula (2) with all_1_1_1, all_1_2_2 and discharging atoms domain(all_1_2_2) = all_1_1_1, yields: % 65.62/31.90 | (51) ? [v0] : (antidomain(v0) = all_1_1_1 & antidomain(all_1_2_2) = v0) % 65.62/31.90 | % 65.62/31.90 | Instantiating formula (3) with all_1_0_0, all_1_0_0, all_1_2_2, all_1_1_1, all_1_1_1 and discharging atoms multiplication(all_1_1_1, all_1_2_2) = all_1_0_0, yields: % 65.62/31.90 | (52) ? [v0] : ? [v1] : (multiplication(v0, all_1_2_2) = v1 & addition(all_1_0_0, all_1_0_0) = v1 & addition(all_1_1_1, all_1_1_1) = v0) % 65.62/31.90 | % 65.62/31.90 | Instantiating formula (5) with all_1_0_0, all_1_0_0, all_1_2_2, all_1_2_2, all_1_1_1 and discharging atoms multiplication(all_1_1_1, all_1_2_2) = all_1_0_0, yields: % 65.62/31.90 | (53) ? [v0] : ? [v1] : (multiplication(all_1_1_1, v0) = v1 & addition(all_1_0_0, all_1_0_0) = v1 & addition(all_1_2_2, all_1_2_2) = v0) % 65.62/31.90 | % 65.62/31.90 | Instantiating formula (45) with all_1_0_0, all_1_2_2, all_1_1_1 and discharging atoms multiplication(all_1_1_1, all_1_2_2) = all_1_0_0, yields: % 65.62/31.90 | (54) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (coantidomain(v3) = v4 & coantidomain(v1) = v2 & coantidomain(all_1_0_0) = v0 & coantidomain(all_1_1_1) = v1 & multiplication(v2, all_1_2_2) = v3 & addition(v0, v4) = v4) % 65.62/31.90 | % 65.62/31.90 | Instantiating formula (17) with all_1_0_0, all_1_2_2, all_1_1_1 and discharging atoms multiplication(all_1_1_1, all_1_2_2) = all_1_0_0, yields: % 65.62/31.90 | (55) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (antidomain(v3) = v4 & antidomain(v1) = v2 & antidomain(all_1_0_0) = v0 & antidomain(all_1_2_2) = v1 & multiplication(all_1_1_1, v2) = v3 & addition(v0, v4) = v4) % 65.62/31.90 | % 65.62/31.90 | Instantiating (55) with all_8_0_3, all_8_1_4, all_8_2_5, all_8_3_6, all_8_4_7 yields: % 65.62/31.90 | (56) antidomain(all_8_1_4) = all_8_0_3 & antidomain(all_8_3_6) = all_8_2_5 & antidomain(all_1_0_0) = all_8_4_7 & antidomain(all_1_2_2) = all_8_3_6 & multiplication(all_1_1_1, all_8_2_5) = all_8_1_4 & addition(all_8_4_7, all_8_0_3) = all_8_0_3 % 65.62/31.90 | % 65.62/31.90 | Applying alpha-rule on (56) yields: % 65.62/31.90 | (57) addition(all_8_4_7, all_8_0_3) = all_8_0_3 % 65.62/31.90 | (58) antidomain(all_8_1_4) = all_8_0_3 % 65.62/31.90 | (59) antidomain(all_1_2_2) = all_8_3_6 % 65.62/31.90 | (60) antidomain(all_8_3_6) = all_8_2_5 % 65.62/31.90 | (61) multiplication(all_1_1_1, all_8_2_5) = all_8_1_4 % 65.62/31.90 | (62) antidomain(all_1_0_0) = all_8_4_7 % 65.62/31.90 | % 65.62/31.90 | Instantiating (53) with all_10_0_8, all_10_1_9 yields: % 65.62/31.90 | (63) multiplication(all_1_1_1, all_10_1_9) = all_10_0_8 & addition(all_1_0_0, all_1_0_0) = all_10_0_8 & addition(all_1_2_2, all_1_2_2) = all_10_1_9 % 65.62/31.90 | % 65.62/31.90 | Applying alpha-rule on (63) yields: % 65.62/31.90 | (64) multiplication(all_1_1_1, all_10_1_9) = all_10_0_8 % 65.62/31.90 | (65) addition(all_1_0_0, all_1_0_0) = all_10_0_8 % 65.62/31.90 | (66) addition(all_1_2_2, all_1_2_2) = all_10_1_9 % 65.62/31.90 | % 65.62/31.90 | Instantiating (52) with all_12_0_10, all_12_1_11 yields: % 65.62/31.90 | (67) multiplication(all_12_1_11, all_1_2_2) = all_12_0_10 & addition(all_1_0_0, all_1_0_0) = all_12_0_10 & addition(all_1_1_1, all_1_1_1) = all_12_1_11 % 65.62/31.90 | % 65.62/31.90 | Applying alpha-rule on (67) yields: % 65.62/31.90 | (68) multiplication(all_12_1_11, all_1_2_2) = all_12_0_10 % 65.62/31.90 | (69) addition(all_1_0_0, all_1_0_0) = all_12_0_10 % 65.62/31.90 | (70) addition(all_1_1_1, all_1_1_1) = all_12_1_11 % 65.62/31.90 | % 65.62/31.90 | Instantiating (51) with all_14_0_12 yields: % 65.62/31.90 | (71) antidomain(all_14_0_12) = all_1_1_1 & antidomain(all_1_2_2) = all_14_0_12 % 65.62/31.91 | % 65.62/31.91 | Applying alpha-rule on (71) yields: % 65.62/31.91 | (72) antidomain(all_14_0_12) = all_1_1_1 % 65.62/31.91 | (73) antidomain(all_1_2_2) = all_14_0_12 % 65.62/31.91 | % 65.62/31.91 | Instantiating (54) with all_16_0_13, all_16_1_14, all_16_2_15, all_16_3_16, all_16_4_17 yields: % 65.62/31.91 | (74) coantidomain(all_16_1_14) = all_16_0_13 & coantidomain(all_16_3_16) = all_16_2_15 & coantidomain(all_1_0_0) = all_16_4_17 & coantidomain(all_1_1_1) = all_16_3_16 & multiplication(all_16_2_15, all_1_2_2) = all_16_1_14 & addition(all_16_4_17, all_16_0_13) = all_16_0_13 % 65.62/31.91 | % 65.62/31.91 | Applying alpha-rule on (74) yields: % 65.62/31.91 | (75) coantidomain(all_1_0_0) = all_16_4_17 % 65.62/31.91 | (76) multiplication(all_16_2_15, all_1_2_2) = all_16_1_14 % 65.62/31.91 | (77) coantidomain(all_16_1_14) = all_16_0_13 % 65.62/31.91 | (78) coantidomain(all_1_1_1) = all_16_3_16 % 65.62/31.91 | (79) addition(all_16_4_17, all_16_0_13) = all_16_0_13 % 65.62/31.91 | (80) coantidomain(all_16_3_16) = all_16_2_15 % 65.62/31.91 | % 65.62/31.91 | Instantiating formula (1) with all_8_3_6, all_8_2_5, all_1_1_1 and discharging atoms antidomain(all_8_3_6) = all_8_2_5, yields: % 65.62/31.91 | (81) all_8_2_5 = all_1_1_1 | ~ (antidomain(all_8_3_6) = all_1_1_1) % 65.62/31.91 | % 65.62/31.91 | Instantiating formula (1) with all_1_2_2, all_8_3_6, all_14_0_12 and discharging atoms antidomain(all_1_2_2) = all_14_0_12, antidomain(all_1_2_2) = all_8_3_6, yields: % 65.62/31.91 | (82) all_14_0_12 = all_8_3_6 % 65.62/31.91 | % 65.62/31.91 | Instantiating formula (34) with all_12_0_10, all_1_0_0 and discharging atoms addition(all_1_0_0, all_1_0_0) = all_12_0_10, yields: % 65.62/31.91 | (83) all_12_0_10 = all_1_0_0 % 65.62/31.91 | % 65.62/31.91 | Instantiating formula (24) with all_1_0_0, all_1_0_0, all_10_0_8, all_12_0_10 and discharging atoms addition(all_1_0_0, all_1_0_0) = all_12_0_10, addition(all_1_0_0, all_1_0_0) = all_10_0_8, yields: % 65.62/31.91 | (84) all_12_0_10 = all_10_0_8 % 65.62/31.91 | % 65.62/31.91 | Instantiating formula (34) with all_10_1_9, all_1_2_2 and discharging atoms addition(all_1_2_2, all_1_2_2) = all_10_1_9, yields: % 65.62/31.91 | (85) all_10_1_9 = all_1_2_2 % 65.62/31.91 | % 65.62/31.91 | Combining equations (83,84) yields a new equation: % 65.62/31.91 | (86) all_10_0_8 = all_1_0_0 % 65.62/31.91 | % 65.62/31.91 | From (82) and (72) follows: % 65.62/31.91 | (87) antidomain(all_8_3_6) = all_1_1_1 % 65.62/31.91 | % 65.62/31.91 | From (82) and (73) follows: % 65.62/31.91 | (59) antidomain(all_1_2_2) = all_8_3_6 % 65.62/31.91 | % 65.62/31.91 | From (85)(86) and (64) follows: % 65.62/31.91 | (50) multiplication(all_1_1_1, all_1_2_2) = all_1_0_0 % 65.62/31.91 | % 65.62/31.91 | From (85) and (66) follows: % 65.62/31.91 | (90) addition(all_1_2_2, all_1_2_2) = all_1_2_2 % 65.62/31.91 | % 65.62/31.91 +-Applying beta-rule and splitting (81), into two cases. % 65.62/31.91 |-Branch one: % 65.62/31.91 | (91) ~ (antidomain(all_8_3_6) = all_1_1_1) % 65.62/31.91 | % 65.62/31.91 | Using (87) and (91) yields: % 65.62/31.91 | (92) $false % 65.62/31.91 | % 65.62/31.91 |-The branch is then unsatisfiable % 65.62/31.91 |-Branch two: % 65.62/31.91 | (87) antidomain(all_8_3_6) = all_1_1_1 % 65.62/31.91 | (94) all_8_2_5 = all_1_1_1 % 65.62/31.91 | % 65.62/31.91 | From (94) and (60) follows: % 65.62/31.91 | (87) antidomain(all_8_3_6) = all_1_1_1 % 65.62/31.91 | % 65.62/31.91 | From (94) and (61) follows: % 65.62/31.91 | (96) multiplication(all_1_1_1, all_1_1_1) = all_8_1_4 % 65.62/31.91 | % 65.62/31.91 | Instantiating formula (36) with all_16_2_15, all_16_3_16 and discharging atoms coantidomain(all_16_3_16) = all_16_2_15, yields: % 65.62/31.91 | (97) ? [v0] : (codomain(all_16_3_16) = v0 & coantidomain(all_16_2_15) = v0) % 65.62/31.91 | % 65.62/31.91 | Instantiating formula (33) with all_16_2_15, all_16_3_16 and discharging atoms coantidomain(all_16_3_16) = all_16_2_15, yields: % 65.62/31.91 | (98) ? [v0] : (coantidomain(all_16_2_15) = v0 & addition(v0, all_16_2_15) = one) % 65.62/31.91 | % 65.62/31.91 | Instantiating formula (36) with all_16_3_16, all_1_1_1 and discharging atoms coantidomain(all_1_1_1) = all_16_3_16, yields: % 65.62/31.91 | (99) ? [v0] : (codomain(all_1_1_1) = v0 & coantidomain(all_16_3_16) = v0) % 65.62/31.91 | % 65.62/31.91 | Instantiating formula (33) with all_16_3_16, all_1_1_1 and discharging atoms coantidomain(all_1_1_1) = all_16_3_16, yields: % 65.62/31.91 | (100) ? [v0] : (coantidomain(all_16_3_16) = v0 & addition(v0, all_16_3_16) = one) % 65.62/31.91 | % 65.62/31.91 | Instantiating formula (40) with all_1_1_1, all_8_3_6 and discharging atoms antidomain(all_8_3_6) = all_1_1_1, yields: % 65.62/31.91 | (101) multiplication(all_1_1_1, all_8_3_6) = zero % 65.62/31.91 | % 65.62/31.91 | Instantiating formula (22) with all_1_1_1, all_8_3_6 and discharging atoms antidomain(all_8_3_6) = all_1_1_1, yields: % 65.62/31.91 | (102) ? [v0] : (antidomain(all_1_1_1) = v0 & addition(v0, all_1_1_1) = one) % 65.62/31.91 | % 65.62/31.91 | Instantiating formula (40) with all_8_3_6, all_1_2_2 and discharging atoms antidomain(all_1_2_2) = all_8_3_6, yields: % 65.62/31.91 | (103) multiplication(all_8_3_6, all_1_2_2) = zero % 65.62/31.91 | % 65.62/31.91 | Instantiating formula (22) with all_8_3_6, all_1_2_2 and discharging atoms antidomain(all_1_2_2) = all_8_3_6, yields: % 65.62/31.91 | (104) ? [v0] : (antidomain(all_8_3_6) = v0 & addition(v0, all_8_3_6) = one) % 65.62/31.91 | % 65.62/31.91 | Instantiating formula (3) with all_1_0_0, all_16_1_14, all_1_2_2, all_1_1_1, all_16_2_15 and discharging atoms multiplication(all_16_2_15, all_1_2_2) = all_16_1_14, multiplication(all_1_1_1, all_1_2_2) = all_1_0_0, yields: % 65.62/31.91 | (105) ? [v0] : ? [v1] : (multiplication(v0, all_1_2_2) = v1 & addition(all_16_1_14, all_1_0_0) = v1 & addition(all_16_2_15, all_1_1_1) = v0) % 65.62/31.91 | % 65.62/31.91 | Instantiating formula (45) with all_16_1_14, all_1_2_2, all_16_2_15 and discharging atoms multiplication(all_16_2_15, all_1_2_2) = all_16_1_14, yields: % 65.62/31.91 | (106) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (coantidomain(v3) = v4 & coantidomain(v1) = v2 & coantidomain(all_16_1_14) = v0 & coantidomain(all_16_2_15) = v1 & multiplication(v2, all_1_2_2) = v3 & addition(v0, v4) = v4) % 65.62/31.91 | % 65.62/31.91 | Instantiating formula (5) with all_1_0_0, all_8_1_4, all_1_2_2, all_1_1_1, all_1_1_1 and discharging atoms multiplication(all_1_1_1, all_1_1_1) = all_8_1_4, multiplication(all_1_1_1, all_1_2_2) = all_1_0_0, yields: % 65.62/31.91 | (107) ? [v0] : ? [v1] : (multiplication(all_1_1_1, v0) = v1 & addition(all_8_1_4, all_1_0_0) = v1 & addition(all_1_1_1, all_1_2_2) = v0) % 65.62/31.91 | % 65.62/31.91 | Instantiating formula (17) with all_8_1_4, all_1_1_1, all_1_1_1 and discharging atoms multiplication(all_1_1_1, all_1_1_1) = all_8_1_4, yields: % 65.62/31.91 | (108) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (antidomain(v3) = v4 & antidomain(v1) = v2 & antidomain(all_8_1_4) = v0 & antidomain(all_1_1_1) = v1 & multiplication(all_1_1_1, v2) = v3 & addition(v0, v4) = v4) % 65.62/31.91 | % 65.62/31.91 | Instantiating formula (30) with all_16_1_14, all_1_2_2, all_1_2_2, all_1_2_2, all_16_2_15 and discharging atoms multiplication(all_16_2_15, all_1_2_2) = all_16_1_14, addition(all_1_2_2, all_1_2_2) = all_1_2_2, yields: % 65.62/31.91 | (109) ? [v0] : ? [v1] : (multiplication(all_16_2_15, all_1_2_2) = v1 & multiplication(all_16_2_15, all_1_2_2) = v0 & addition(v0, v1) = all_16_1_14) % 65.62/31.91 | % 65.62/31.91 | Instantiating formula (46) with all_16_1_14, all_1_2_2, all_1_2_2, all_1_2_2, all_16_2_15 and discharging atoms multiplication(all_16_2_15, all_1_2_2) = all_16_1_14, addition(all_1_2_2, all_1_2_2) = all_1_2_2, yields: % 65.62/31.91 | (110) ? [v0] : ? [v1] : (multiplication(all_16_2_15, all_1_2_2) = v1 & multiplication(all_16_2_15, all_1_2_2) = v0 & addition(v1, all_16_1_14) = v0) % 65.62/31.92 | % 65.62/31.92 | Instantiating formula (31) with all_16_1_14, all_1_2_2, all_1_2_2, all_1_2_2, all_16_2_15 and discharging atoms multiplication(all_16_2_15, all_1_2_2) = all_16_1_14, addition(all_1_2_2, all_1_2_2) = all_1_2_2, yields: % 65.62/31.92 | (111) ? [v0] : ? [v1] : (multiplication(all_16_2_15, all_1_2_2) = v1 & multiplication(all_16_2_15, all_1_2_2) = v0 & addition(all_16_1_14, v1) = v0) % 65.62/31.92 | % 65.62/31.92 | Instantiating (111) with all_38_0_19, all_38_1_20 yields: % 65.62/31.92 | (112) multiplication(all_16_2_15, all_1_2_2) = all_38_0_19 & multiplication(all_16_2_15, all_1_2_2) = all_38_1_20 & addition(all_16_1_14, all_38_0_19) = all_38_1_20 % 65.62/31.92 | % 65.62/31.92 | Applying alpha-rule on (112) yields: % 65.62/31.92 | (113) multiplication(all_16_2_15, all_1_2_2) = all_38_0_19 % 65.62/31.92 | (114) multiplication(all_16_2_15, all_1_2_2) = all_38_1_20 % 65.62/31.92 | (115) addition(all_16_1_14, all_38_0_19) = all_38_1_20 % 65.62/31.92 | % 65.62/31.92 | Instantiating (105) with all_42_0_22, all_42_1_23 yields: % 65.62/31.92 | (116) multiplication(all_42_1_23, all_1_2_2) = all_42_0_22 & addition(all_16_1_14, all_1_0_0) = all_42_0_22 & addition(all_16_2_15, all_1_1_1) = all_42_1_23 % 65.62/31.92 | % 65.62/31.92 | Applying alpha-rule on (116) yields: % 65.62/31.92 | (117) multiplication(all_42_1_23, all_1_2_2) = all_42_0_22 % 65.62/31.92 | (118) addition(all_16_1_14, all_1_0_0) = all_42_0_22 % 65.62/31.92 | (119) addition(all_16_2_15, all_1_1_1) = all_42_1_23 % 65.62/31.92 | % 65.62/31.92 | Instantiating (104) with all_44_0_24 yields: % 65.62/31.92 | (120) antidomain(all_8_3_6) = all_44_0_24 & addition(all_44_0_24, all_8_3_6) = one % 65.62/31.92 | % 65.62/31.92 | Applying alpha-rule on (120) yields: % 65.62/31.92 | (121) antidomain(all_8_3_6) = all_44_0_24 % 65.62/31.92 | (122) addition(all_44_0_24, all_8_3_6) = one % 65.62/31.92 | % 65.62/31.92 | Instantiating (110) with all_60_0_33, all_60_1_34 yields: % 65.62/31.92 | (123) multiplication(all_16_2_15, all_1_2_2) = all_60_0_33 & multiplication(all_16_2_15, all_1_2_2) = all_60_1_34 & addition(all_60_0_33, all_16_1_14) = all_60_1_34 % 65.62/31.92 | % 65.62/31.92 | Applying alpha-rule on (123) yields: % 65.62/31.92 | (124) multiplication(all_16_2_15, all_1_2_2) = all_60_0_33 % 65.62/31.92 | (125) multiplication(all_16_2_15, all_1_2_2) = all_60_1_34 % 65.62/31.92 | (126) addition(all_60_0_33, all_16_1_14) = all_60_1_34 % 65.62/31.92 | % 65.62/31.92 | Instantiating (109) with all_62_0_35, all_62_1_36 yields: % 65.62/31.92 | (127) multiplication(all_16_2_15, all_1_2_2) = all_62_0_35 & multiplication(all_16_2_15, all_1_2_2) = all_62_1_36 & addition(all_62_1_36, all_62_0_35) = all_16_1_14 % 65.62/31.92 | % 65.62/31.92 | Applying alpha-rule on (127) yields: % 65.62/31.92 | (128) multiplication(all_16_2_15, all_1_2_2) = all_62_0_35 % 65.62/31.92 | (129) multiplication(all_16_2_15, all_1_2_2) = all_62_1_36 % 65.62/31.92 | (130) addition(all_62_1_36, all_62_0_35) = all_16_1_14 % 65.62/31.92 | % 65.62/31.92 | Instantiating (108) with all_64_0_37, all_64_1_38, all_64_2_39, all_64_3_40, all_64_4_41 yields: % 65.62/31.92 | (131) antidomain(all_64_1_38) = all_64_0_37 & antidomain(all_64_3_40) = all_64_2_39 & antidomain(all_8_1_4) = all_64_4_41 & antidomain(all_1_1_1) = all_64_3_40 & multiplication(all_1_1_1, all_64_2_39) = all_64_1_38 & addition(all_64_4_41, all_64_0_37) = all_64_0_37 % 65.62/31.92 | % 65.62/31.92 | Applying alpha-rule on (131) yields: % 65.62/31.92 | (132) antidomain(all_1_1_1) = all_64_3_40 % 65.62/31.92 | (133) addition(all_64_4_41, all_64_0_37) = all_64_0_37 % 65.62/31.92 | (134) multiplication(all_1_1_1, all_64_2_39) = all_64_1_38 % 65.62/31.92 | (135) antidomain(all_8_1_4) = all_64_4_41 % 65.62/31.92 | (136) antidomain(all_64_3_40) = all_64_2_39 % 65.62/31.92 | (137) antidomain(all_64_1_38) = all_64_0_37 % 65.62/31.92 | % 65.62/31.92 | Instantiating (100) with all_72_0_46 yields: % 65.62/31.92 | (138) coantidomain(all_16_3_16) = all_72_0_46 & addition(all_72_0_46, all_16_3_16) = one % 65.62/31.92 | % 65.62/31.92 | Applying alpha-rule on (138) yields: % 65.62/31.92 | (139) coantidomain(all_16_3_16) = all_72_0_46 % 65.62/31.92 | (140) addition(all_72_0_46, all_16_3_16) = one % 65.62/31.92 | % 65.62/31.92 | Instantiating (99) with all_74_0_47 yields: % 65.62/31.92 | (141) codomain(all_1_1_1) = all_74_0_47 & coantidomain(all_16_3_16) = all_74_0_47 % 65.62/31.92 | % 65.62/31.92 | Applying alpha-rule on (141) yields: % 65.62/31.92 | (142) codomain(all_1_1_1) = all_74_0_47 % 65.62/31.92 | (143) coantidomain(all_16_3_16) = all_74_0_47 % 65.62/31.92 | % 65.62/31.92 | Instantiating (106) with all_82_0_56, all_82_1_57, all_82_2_58, all_82_3_59, all_82_4_60 yields: % 65.62/31.92 | (144) coantidomain(all_82_1_57) = all_82_0_56 & coantidomain(all_82_3_59) = all_82_2_58 & coantidomain(all_16_1_14) = all_82_4_60 & coantidomain(all_16_2_15) = all_82_3_59 & multiplication(all_82_2_58, all_1_2_2) = all_82_1_57 & addition(all_82_4_60, all_82_0_56) = all_82_0_56 % 65.62/31.92 | % 65.62/31.92 | Applying alpha-rule on (144) yields: % 65.62/31.92 | (145) coantidomain(all_16_1_14) = all_82_4_60 % 65.62/31.92 | (146) coantidomain(all_16_2_15) = all_82_3_59 % 65.62/31.92 | (147) addition(all_82_4_60, all_82_0_56) = all_82_0_56 % 65.62/31.92 | (148) coantidomain(all_82_3_59) = all_82_2_58 % 65.62/31.92 | (149) coantidomain(all_82_1_57) = all_82_0_56 % 65.62/31.92 | (150) multiplication(all_82_2_58, all_1_2_2) = all_82_1_57 % 65.62/31.92 | % 65.62/31.92 | Instantiating (98) with all_92_0_67 yields: % 65.62/31.92 | (151) coantidomain(all_16_2_15) = all_92_0_67 & addition(all_92_0_67, all_16_2_15) = one % 65.62/31.92 | % 65.62/31.92 | Applying alpha-rule on (151) yields: % 65.62/31.92 | (152) coantidomain(all_16_2_15) = all_92_0_67 % 65.62/31.92 | (153) addition(all_92_0_67, all_16_2_15) = one % 65.62/31.92 | % 65.62/31.92 | Instantiating (97) with all_94_0_68 yields: % 65.62/31.92 | (154) codomain(all_16_3_16) = all_94_0_68 & coantidomain(all_16_2_15) = all_94_0_68 % 66.00/31.92 | % 66.00/31.92 | Applying alpha-rule on (154) yields: % 66.00/31.92 | (155) codomain(all_16_3_16) = all_94_0_68 % 66.00/31.92 | (156) coantidomain(all_16_2_15) = all_94_0_68 % 66.00/31.92 | % 66.00/31.92 | Instantiating (107) with all_98_0_74, all_98_1_75 yields: % 66.00/31.92 | (157) multiplication(all_1_1_1, all_98_1_75) = all_98_0_74 & addition(all_8_1_4, all_1_0_0) = all_98_0_74 & addition(all_1_1_1, all_1_2_2) = all_98_1_75 % 66.00/31.92 | % 66.00/31.92 | Applying alpha-rule on (157) yields: % 66.00/31.92 | (158) multiplication(all_1_1_1, all_98_1_75) = all_98_0_74 % 66.00/31.92 | (159) addition(all_8_1_4, all_1_0_0) = all_98_0_74 % 66.00/31.92 | (160) addition(all_1_1_1, all_1_2_2) = all_98_1_75 % 66.00/31.92 | % 66.00/31.92 | Instantiating (102) with all_102_0_78 yields: % 66.00/31.92 | (161) antidomain(all_1_1_1) = all_102_0_78 & addition(all_102_0_78, all_1_1_1) = one % 66.00/31.92 | % 66.00/31.92 | Applying alpha-rule on (161) yields: % 66.00/31.92 | (162) antidomain(all_1_1_1) = all_102_0_78 % 66.00/31.92 | (163) addition(all_102_0_78, all_1_1_1) = one % 66.00/31.92 | % 66.00/31.92 | Instantiating formula (27) with all_16_2_15, all_92_0_67, all_94_0_68 and discharging atoms coantidomain(all_16_2_15) = all_94_0_68, coantidomain(all_16_2_15) = all_92_0_67, yields: % 66.00/31.92 | (164) all_94_0_68 = all_92_0_67 % 66.00/31.92 | % 66.00/31.92 | Instantiating formula (27) with all_16_2_15, all_82_3_59, all_94_0_68 and discharging atoms coantidomain(all_16_2_15) = all_94_0_68, coantidomain(all_16_2_15) = all_82_3_59, yields: % 66.00/31.92 | (165) all_94_0_68 = all_82_3_59 % 66.00/31.92 | % 66.00/31.92 | Instantiating formula (27) with all_16_3_16, all_74_0_47, all_16_2_15 and discharging atoms coantidomain(all_16_3_16) = all_74_0_47, coantidomain(all_16_3_16) = all_16_2_15, yields: % 66.00/31.92 | (166) all_74_0_47 = all_16_2_15 % 66.00/31.92 | % 66.00/31.92 | Instantiating formula (27) with all_16_3_16, all_72_0_46, all_74_0_47 and discharging atoms coantidomain(all_16_3_16) = all_74_0_47, coantidomain(all_16_3_16) = all_72_0_46, yields: % 66.00/31.93 | (167) all_74_0_47 = all_72_0_46 % 66.00/31.93 | % 66.00/31.93 | Instantiating formula (1) with all_8_3_6, all_44_0_24, all_1_1_1 and discharging atoms antidomain(all_8_3_6) = all_44_0_24, antidomain(all_8_3_6) = all_1_1_1, yields: % 66.00/31.93 | (168) all_44_0_24 = all_1_1_1 % 66.00/31.93 | % 66.00/31.93 | Instantiating formula (1) with all_1_1_1, all_64_3_40, all_102_0_78 and discharging atoms antidomain(all_1_1_1) = all_102_0_78, antidomain(all_1_1_1) = all_64_3_40, yields: % 66.00/31.93 | (169) all_102_0_78 = all_64_3_40 % 66.00/31.93 | % 66.00/31.93 | Instantiating formula (18) with all_16_2_15, all_1_2_2, all_62_1_36, all_62_0_35 and discharging atoms multiplication(all_16_2_15, all_1_2_2) = all_62_0_35, multiplication(all_16_2_15, all_1_2_2) = all_62_1_36, yields: % 66.00/31.93 | (170) all_62_0_35 = all_62_1_36 % 66.00/31.93 | % 66.00/31.93 | Instantiating formula (18) with all_16_2_15, all_1_2_2, all_60_0_33, all_16_1_14 and discharging atoms multiplication(all_16_2_15, all_1_2_2) = all_60_0_33, multiplication(all_16_2_15, all_1_2_2) = all_16_1_14, yields: % 66.00/31.93 | (171) all_60_0_33 = all_16_1_14 % 66.00/31.93 | % 66.00/31.93 | Instantiating formula (18) with all_16_2_15, all_1_2_2, all_60_0_33, all_62_1_36 and discharging atoms multiplication(all_16_2_15, all_1_2_2) = all_62_1_36, multiplication(all_16_2_15, all_1_2_2) = all_60_0_33, yields: % 66.00/31.93 | (172) all_62_1_36 = all_60_0_33 % 66.00/31.93 | % 66.00/31.93 | Instantiating formula (18) with all_16_2_15, all_1_2_2, all_60_1_34, all_62_0_35 and discharging atoms multiplication(all_16_2_15, all_1_2_2) = all_62_0_35, multiplication(all_16_2_15, all_1_2_2) = all_60_1_34, yields: % 66.00/31.93 | (173) all_62_0_35 = all_60_1_34 % 66.00/31.93 | % 66.00/31.93 | Instantiating formula (18) with all_16_2_15, all_1_2_2, all_38_0_19, all_60_0_33 and discharging atoms multiplication(all_16_2_15, all_1_2_2) = all_60_0_33, multiplication(all_16_2_15, all_1_2_2) = all_38_0_19, yields: % 66.00/31.93 | (174) all_60_0_33 = all_38_0_19 % 66.00/31.93 | % 66.00/31.93 | Instantiating formula (18) with all_16_2_15, all_1_2_2, all_38_1_20, all_62_1_36 and discharging atoms multiplication(all_16_2_15, all_1_2_2) = all_62_1_36, multiplication(all_16_2_15, all_1_2_2) = all_38_1_20, yields: % 66.00/31.93 | (175) all_62_1_36 = all_38_1_20 % 66.00/31.93 | % 66.00/31.93 | Combining equations (164,165) yields a new equation: % 66.00/31.93 | (176) all_92_0_67 = all_82_3_59 % 66.00/31.93 | % 66.00/31.93 | Simplifying 176 yields: % 66.00/31.93 | (177) all_92_0_67 = all_82_3_59 % 66.00/31.93 | % 66.00/31.93 | Combining equations (166,167) yields a new equation: % 66.00/31.93 | (178) all_72_0_46 = all_16_2_15 % 66.00/31.93 | % 66.00/31.93 | Combining equations (170,173) yields a new equation: % 66.00/31.93 | (179) all_62_1_36 = all_60_1_34 % 66.00/31.93 | % 66.00/31.93 | Simplifying 179 yields: % 66.00/31.93 | (180) all_62_1_36 = all_60_1_34 % 66.00/31.93 | % 66.00/31.93 | Combining equations (172,180) yields a new equation: % 66.00/31.93 | (181) all_60_0_33 = all_60_1_34 % 66.00/31.93 | % 66.00/31.93 | Simplifying 181 yields: % 66.00/31.93 | (182) all_60_0_33 = all_60_1_34 % 66.00/31.93 | % 66.00/31.93 | Combining equations (175,180) yields a new equation: % 66.00/31.93 | (183) all_60_1_34 = all_38_1_20 % 66.00/31.93 | % 66.00/31.93 | Combining equations (171,174) yields a new equation: % 66.00/31.93 | (184) all_38_0_19 = all_16_1_14 % 66.00/31.93 | % 66.00/31.93 | Combining equations (182,174) yields a new equation: % 66.00/31.93 | (185) all_60_1_34 = all_38_0_19 % 66.00/31.93 | % 66.00/31.93 | Simplifying 185 yields: % 66.00/31.93 | (186) all_60_1_34 = all_38_0_19 % 66.00/31.93 | % 66.00/31.93 | Combining equations (186,183) yields a new equation: % 66.00/31.93 | (187) all_38_0_19 = all_38_1_20 % 66.00/31.93 | % 66.00/31.93 | Simplifying 187 yields: % 66.00/31.93 | (188) all_38_0_19 = all_38_1_20 % 66.00/31.93 | % 66.00/31.93 | Combining equations (184,188) yields a new equation: % 66.00/31.93 | (189) all_38_1_20 = all_16_1_14 % 66.00/31.93 | % 66.00/31.93 | From (189) and (114) follows: % 66.00/31.93 | (76) multiplication(all_16_2_15, all_1_2_2) = all_16_1_14 % 66.00/31.93 | % 66.00/31.93 | From (169) and (163) follows: % 66.00/31.93 | (191) addition(all_64_3_40, all_1_1_1) = one % 66.00/31.93 | % 66.00/31.93 | From (177) and (153) follows: % 66.00/31.93 | (192) addition(all_82_3_59, all_16_2_15) = one % 66.00/31.93 | % 66.00/31.93 | From (178) and (140) follows: % 66.00/31.93 | (193) addition(all_16_2_15, all_16_3_16) = one % 66.00/31.93 | % 66.00/31.93 | From (168) and (122) follows: % 66.00/31.93 | (194) addition(all_1_1_1, all_8_3_6) = one % 66.00/31.93 | % 66.00/31.93 | Instantiating formula (19) with all_16_1_14, one, all_1_2_2, all_16_2_15, all_82_3_59 and discharging atoms multiplication(all_16_2_15, all_1_2_2) = all_16_1_14, addition(all_82_3_59, all_16_2_15) = one, yields: % 66.00/31.93 | (195) ? [v0] : ? [v1] : (multiplication(all_82_3_59, all_1_2_2) = v1 & multiplication(one, all_1_2_2) = v0 & addition(v1, all_16_1_14) = v0) % 66.00/31.93 | % 66.00/31.93 | Instantiating formula (19) with all_1_0_0, one, all_1_2_2, all_1_1_1, all_64_3_40 and discharging atoms multiplication(all_1_1_1, all_1_2_2) = all_1_0_0, addition(all_64_3_40, all_1_1_1) = one, yields: % 66.00/31.93 | (196) ? [v0] : ? [v1] : (multiplication(all_64_3_40, all_1_2_2) = v1 & multiplication(one, all_1_2_2) = v0 & addition(v1, all_1_0_0) = v0) % 66.00/31.93 | % 66.00/31.93 | Instantiating formula (7) with zero, one, all_1_2_2, all_1_1_1, all_8_3_6 and discharging atoms multiplication(all_8_3_6, all_1_2_2) = zero, yields: % 66.00/31.93 | (197) ~ (addition(all_8_3_6, all_1_1_1) = one) | ? [v0] : ? [v1] : (multiplication(all_1_1_1, all_1_2_2) = v1 & multiplication(one, all_1_2_2) = v0 & addition(zero, v1) = v0) % 66.00/31.93 | % 66.00/31.93 | Instantiating formula (31) with zero, one, all_1_1_1, all_8_3_6, all_1_1_1 and discharging atoms multiplication(all_1_1_1, all_8_3_6) = zero, yields: % 66.00/31.93 | (198) ~ (addition(all_8_3_6, all_1_1_1) = one) | ? [v0] : ? [v1] : (multiplication(all_1_1_1, all_1_1_1) = v1 & multiplication(all_1_1_1, one) = v0 & addition(zero, v1) = v0) % 66.00/31.93 | % 66.00/31.93 | Instantiating formula (7) with all_16_1_14, one, all_1_2_2, all_16_3_16, all_16_2_15 and discharging atoms multiplication(all_16_2_15, all_1_2_2) = all_16_1_14, addition(all_16_2_15, all_16_3_16) = one, yields: % 66.00/31.93 | (199) ? [v0] : ? [v1] : (multiplication(all_16_3_16, all_1_2_2) = v1 & multiplication(one, all_1_2_2) = v0 & addition(all_16_1_14, v1) = v0) % 66.00/31.93 | % 66.00/31.93 | Instantiating formula (39) with all_42_1_23, all_16_2_15, all_1_1_1 and discharging atoms addition(all_16_2_15, all_1_1_1) = all_42_1_23, yields: % 66.00/31.93 | (200) addition(all_1_1_1, all_16_2_15) = all_42_1_23 % 66.00/31.93 | % 66.00/31.93 | Instantiating formula (10) with all_42_0_22, all_42_1_23, all_1_2_2, all_16_2_15, all_1_1_1 and discharging atoms multiplication(all_42_1_23, all_1_2_2) = all_42_0_22, yields: % 66.00/31.93 | (201) ~ (addition(all_1_1_1, all_16_2_15) = all_42_1_23) | ? [v0] : ? [v1] : (multiplication(all_16_2_15, all_1_2_2) = v1 & multiplication(all_1_1_1, all_1_2_2) = v0 & addition(v0, v1) = all_42_0_22) % 66.00/31.93 | % 66.00/31.93 | Instantiating formula (7) with all_1_0_0, one, all_1_2_2, all_8_3_6, all_1_1_1 and discharging atoms multiplication(all_1_1_1, all_1_2_2) = all_1_0_0, addition(all_1_1_1, all_8_3_6) = one, yields: % 66.00/31.93 | (202) ? [v0] : ? [v1] : (multiplication(all_8_3_6, all_1_2_2) = v1 & multiplication(one, all_1_2_2) = v0 & addition(all_1_0_0, v1) = v0) % 66.00/31.93 | % 66.00/31.93 | Instantiating formula (19) with zero, one, all_1_2_2, all_8_3_6, all_1_1_1 and discharging atoms multiplication(all_8_3_6, all_1_2_2) = zero, addition(all_1_1_1, all_8_3_6) = one, yields: % 66.00/31.93 | (203) ? [v0] : ? [v1] : (multiplication(all_1_1_1, all_1_2_2) = v1 & multiplication(one, all_1_2_2) = v0 & addition(v1, zero) = v0) % 66.00/31.93 | % 66.00/31.93 | Instantiating formula (39) with one, all_1_1_1, all_8_3_6 and discharging atoms addition(all_1_1_1, all_8_3_6) = one, yields: % 66.00/31.93 | (204) addition(all_8_3_6, all_1_1_1) = one % 66.00/31.93 | % 66.00/31.93 | Instantiating formula (39) with all_98_1_75, all_1_1_1, all_1_2_2 and discharging atoms addition(all_1_1_1, all_1_2_2) = all_98_1_75, yields: % 66.00/31.94 | (205) addition(all_1_2_2, all_1_1_1) = all_98_1_75 % 66.00/31.94 | % 66.00/31.94 | Instantiating formula (30) with all_98_0_74, all_98_1_75, all_1_1_1, all_1_2_2, all_1_1_1 and discharging atoms multiplication(all_1_1_1, all_98_1_75) = all_98_0_74, yields: % 66.00/31.94 | (206) ~ (addition(all_1_2_2, all_1_1_1) = all_98_1_75) | ? [v0] : ? [v1] : (multiplication(all_1_1_1, all_1_1_1) = v1 & multiplication(all_1_1_1, all_1_2_2) = v0 & addition(v0, v1) = all_98_0_74) % 66.00/31.94 | % 66.00/31.94 | Instantiating (203) with all_150_0_90, all_150_1_91 yields: % 66.00/31.94 | (207) multiplication(all_1_1_1, all_1_2_2) = all_150_0_90 & multiplication(one, all_1_2_2) = all_150_1_91 & addition(all_150_0_90, zero) = all_150_1_91 % 66.00/31.94 | % 66.00/31.94 | Applying alpha-rule on (207) yields: % 66.00/31.94 | (208) multiplication(all_1_1_1, all_1_2_2) = all_150_0_90 % 66.00/31.94 | (209) multiplication(one, all_1_2_2) = all_150_1_91 % 66.00/31.94 | (210) addition(all_150_0_90, zero) = all_150_1_91 % 66.00/31.94 | % 66.00/31.94 | Instantiating (195) with all_408_0_343, all_408_1_344 yields: % 66.00/31.94 | (211) multiplication(all_82_3_59, all_1_2_2) = all_408_0_343 & multiplication(one, all_1_2_2) = all_408_1_344 & addition(all_408_0_343, all_16_1_14) = all_408_1_344 % 66.00/31.94 | % 66.00/31.94 | Applying alpha-rule on (211) yields: % 66.00/31.94 | (212) multiplication(all_82_3_59, all_1_2_2) = all_408_0_343 % 66.00/31.94 | (213) multiplication(one, all_1_2_2) = all_408_1_344 % 66.00/31.94 | (214) addition(all_408_0_343, all_16_1_14) = all_408_1_344 % 66.00/31.94 | % 66.00/31.94 | Instantiating (199) with all_568_0_498, all_568_1_499 yields: % 66.00/31.94 | (215) multiplication(all_16_3_16, all_1_2_2) = all_568_0_498 & multiplication(one, all_1_2_2) = all_568_1_499 & addition(all_16_1_14, all_568_0_498) = all_568_1_499 % 66.00/31.94 | % 66.00/31.94 | Applying alpha-rule on (215) yields: % 66.00/31.94 | (216) multiplication(all_16_3_16, all_1_2_2) = all_568_0_498 % 66.00/31.94 | (217) multiplication(one, all_1_2_2) = all_568_1_499 % 66.00/31.94 | (218) addition(all_16_1_14, all_568_0_498) = all_568_1_499 % 66.00/31.94 | % 66.00/31.94 | Instantiating (202) with all_782_0_671, all_782_1_672 yields: % 66.00/31.94 | (219) multiplication(all_8_3_6, all_1_2_2) = all_782_0_671 & multiplication(one, all_1_2_2) = all_782_1_672 & addition(all_1_0_0, all_782_0_671) = all_782_1_672 % 66.00/31.94 | % 66.00/31.94 | Applying alpha-rule on (219) yields: % 66.00/31.94 | (220) multiplication(all_8_3_6, all_1_2_2) = all_782_0_671 % 66.00/31.94 | (221) multiplication(one, all_1_2_2) = all_782_1_672 % 66.00/31.94 | (222) addition(all_1_0_0, all_782_0_671) = all_782_1_672 % 66.00/31.94 | % 66.00/31.94 | Instantiating (196) with all_854_0_726, all_854_1_727 yields: % 66.00/31.94 | (223) multiplication(all_64_3_40, all_1_2_2) = all_854_0_726 & multiplication(one, all_1_2_2) = all_854_1_727 & addition(all_854_0_726, all_1_0_0) = all_854_1_727 % 66.00/31.94 | % 66.00/31.94 | Applying alpha-rule on (223) yields: % 66.00/31.94 | (224) multiplication(all_64_3_40, all_1_2_2) = all_854_0_726 % 66.00/31.94 | (225) multiplication(one, all_1_2_2) = all_854_1_727 % 66.00/31.94 | (226) addition(all_854_0_726, all_1_0_0) = all_854_1_727 % 66.00/31.94 | % 66.00/31.94 +-Applying beta-rule and splitting (201), into two cases. % 66.00/31.94 |-Branch one: % 66.00/31.94 | (227) ~ (addition(all_1_1_1, all_16_2_15) = all_42_1_23) % 66.00/31.94 | % 66.00/31.94 | Using (200) and (227) yields: % 66.00/31.94 | (92) $false % 66.00/31.94 | % 66.00/31.94 |-The branch is then unsatisfiable % 66.00/31.94 |-Branch two: % 66.00/31.94 | (200) addition(all_1_1_1, all_16_2_15) = all_42_1_23 % 66.00/31.94 | (230) ? [v0] : ? [v1] : (multiplication(all_16_2_15, all_1_2_2) = v1 & multiplication(all_1_1_1, all_1_2_2) = v0 & addition(v0, v1) = all_42_0_22) % 66.00/31.94 | % 66.00/31.94 | Instantiating (230) with all_1244_0_1139, all_1244_1_1140 yields: % 66.00/31.94 | (231) multiplication(all_16_2_15, all_1_2_2) = all_1244_0_1139 & multiplication(all_1_1_1, all_1_2_2) = all_1244_1_1140 & addition(all_1244_1_1140, all_1244_0_1139) = all_42_0_22 % 66.00/31.94 | % 66.00/31.94 | Applying alpha-rule on (231) yields: % 66.00/31.94 | (232) multiplication(all_16_2_15, all_1_2_2) = all_1244_0_1139 % 66.00/31.94 | (233) multiplication(all_1_1_1, all_1_2_2) = all_1244_1_1140 % 66.00/31.94 | (234) addition(all_1244_1_1140, all_1244_0_1139) = all_42_0_22 % 66.00/31.94 | % 66.00/31.94 +-Applying beta-rule and splitting (198), into two cases. % 66.00/31.94 |-Branch one: % 66.00/31.94 | (235) ~ (addition(all_8_3_6, all_1_1_1) = one) % 66.00/31.94 | % 66.00/31.94 | Using (204) and (235) yields: % 66.00/31.94 | (92) $false % 66.00/31.94 | % 66.00/31.94 |-The branch is then unsatisfiable % 66.00/31.94 |-Branch two: % 66.00/31.94 | (204) addition(all_8_3_6, all_1_1_1) = one % 66.00/31.94 | (238) ? [v0] : ? [v1] : (multiplication(all_1_1_1, all_1_1_1) = v1 & multiplication(all_1_1_1, one) = v0 & addition(zero, v1) = v0) % 66.00/31.94 | % 66.00/31.94 +-Applying beta-rule and splitting (206), into two cases. % 66.00/31.94 |-Branch one: % 66.00/31.94 | (239) ~ (addition(all_1_2_2, all_1_1_1) = all_98_1_75) % 66.00/31.94 | % 66.00/31.94 | Using (205) and (239) yields: % 66.00/31.94 | (92) $false % 66.00/31.94 | % 66.00/31.94 |-The branch is then unsatisfiable % 66.00/31.94 |-Branch two: % 66.00/31.94 | (205) addition(all_1_2_2, all_1_1_1) = all_98_1_75 % 66.00/31.94 | (242) ? [v0] : ? [v1] : (multiplication(all_1_1_1, all_1_1_1) = v1 & multiplication(all_1_1_1, all_1_2_2) = v0 & addition(v0, v1) = all_98_0_74) % 66.00/31.94 | % 66.00/31.94 | Instantiating (242) with all_1256_0_1143, all_1256_1_1144 yields: % 66.00/31.94 | (243) multiplication(all_1_1_1, all_1_1_1) = all_1256_0_1143 & multiplication(all_1_1_1, all_1_2_2) = all_1256_1_1144 & addition(all_1256_1_1144, all_1256_0_1143) = all_98_0_74 % 66.00/31.94 | % 66.00/31.94 | Applying alpha-rule on (243) yields: % 66.00/31.94 | (244) multiplication(all_1_1_1, all_1_1_1) = all_1256_0_1143 % 66.00/31.94 | (245) multiplication(all_1_1_1, all_1_2_2) = all_1256_1_1144 % 66.00/31.94 | (246) addition(all_1256_1_1144, all_1256_0_1143) = all_98_0_74 % 66.00/31.94 | % 66.00/31.94 +-Applying beta-rule and splitting (197), into two cases. % 66.00/31.94 |-Branch one: % 66.00/31.94 | (235) ~ (addition(all_8_3_6, all_1_1_1) = one) % 66.00/31.94 | % 66.00/31.94 | Using (204) and (235) yields: % 66.00/31.94 | (92) $false % 66.00/31.94 | % 66.00/31.94 |-The branch is then unsatisfiable % 66.00/31.94 |-Branch two: % 66.00/31.94 | (204) addition(all_8_3_6, all_1_1_1) = one % 66.00/31.94 | (250) ? [v0] : ? [v1] : (multiplication(all_1_1_1, all_1_2_2) = v1 & multiplication(one, all_1_2_2) = v0 & addition(zero, v1) = v0) % 66.00/31.94 | % 66.00/31.94 | Instantiating (250) with all_1262_0_1145, all_1262_1_1146 yields: % 66.00/31.94 | (251) multiplication(all_1_1_1, all_1_2_2) = all_1262_0_1145 & multiplication(one, all_1_2_2) = all_1262_1_1146 & addition(zero, all_1262_0_1145) = all_1262_1_1146 % 66.00/31.94 | % 66.00/31.94 | Applying alpha-rule on (251) yields: % 66.00/31.94 | (252) multiplication(all_1_1_1, all_1_2_2) = all_1262_0_1145 % 66.00/31.94 | (253) multiplication(one, all_1_2_2) = all_1262_1_1146 % 66.00/31.94 | (254) addition(zero, all_1262_0_1145) = all_1262_1_1146 % 66.00/31.95 | % 66.00/31.95 | Instantiating formula (18) with all_1_1_1, all_1_2_2, all_1262_0_1145, all_1_0_0 and discharging atoms multiplication(all_1_1_1, all_1_2_2) = all_1262_0_1145, multiplication(all_1_1_1, all_1_2_2) = all_1_0_0, yields: % 66.00/31.95 | (255) all_1262_0_1145 = all_1_0_0 % 66.00/31.95 | % 66.00/31.95 | Instantiating formula (18) with all_1_1_1, all_1_2_2, all_1256_1_1144, all_1262_0_1145 and discharging atoms multiplication(all_1_1_1, all_1_2_2) = all_1262_0_1145, multiplication(all_1_1_1, all_1_2_2) = all_1256_1_1144, yields: % 66.00/31.95 | (256) all_1262_0_1145 = all_1256_1_1144 % 66.00/31.95 | % 66.00/31.95 | Instantiating formula (18) with all_1_1_1, all_1_2_2, all_1244_1_1140, all_1262_0_1145 and discharging atoms multiplication(all_1_1_1, all_1_2_2) = all_1262_0_1145, multiplication(all_1_1_1, all_1_2_2) = all_1244_1_1140, yields: % 66.00/31.95 | (257) all_1262_0_1145 = all_1244_1_1140 % 66.00/31.95 | % 66.00/31.95 | Instantiating formula (18) with all_1_1_1, all_1_2_2, all_150_0_90, all_1244_1_1140 and discharging atoms multiplication(all_1_1_1, all_1_2_2) = all_1244_1_1140, multiplication(all_1_1_1, all_1_2_2) = all_150_0_90, yields: % 66.00/31.95 | (258) all_1244_1_1140 = all_150_0_90 % 66.00/31.95 | % 66.00/31.95 | Instantiating formula (18) with one, all_1_2_2, all_854_1_727, all_1262_1_1146 and discharging atoms multiplication(one, all_1_2_2) = all_1262_1_1146, multiplication(one, all_1_2_2) = all_854_1_727, yields: % 66.00/31.95 | (259) all_1262_1_1146 = all_854_1_727 % 66.00/31.95 | % 66.00/31.95 | Instantiating formula (18) with one, all_1_2_2, all_782_1_672, all_1262_1_1146 and discharging atoms multiplication(one, all_1_2_2) = all_1262_1_1146, multiplication(one, all_1_2_2) = all_782_1_672, yields: % 66.00/31.95 | (260) all_1262_1_1146 = all_782_1_672 % 66.00/31.95 | % 66.00/31.95 | Instantiating formula (18) with one, all_1_2_2, all_568_1_499, all_854_1_727 and discharging atoms multiplication(one, all_1_2_2) = all_854_1_727, multiplication(one, all_1_2_2) = all_568_1_499, yields: % 66.00/31.95 | (261) all_854_1_727 = all_568_1_499 % 66.00/31.95 | % 66.00/31.95 | Instantiating formula (12) with all_568_1_499, all_1_2_2 and discharging atoms multiplication(one, all_1_2_2) = all_568_1_499, yields: % 66.00/31.95 | (262) all_568_1_499 = all_1_2_2 % 66.00/31.95 | % 66.00/31.95 | Instantiating formula (18) with one, all_1_2_2, all_408_1_344, all_854_1_727 and discharging atoms multiplication(one, all_1_2_2) = all_854_1_727, multiplication(one, all_1_2_2) = all_408_1_344, yields: % 66.00/31.95 | (263) all_854_1_727 = all_408_1_344 % 66.00/31.95 | % 66.00/31.95 | Instantiating formula (18) with one, all_1_2_2, all_150_1_91, all_568_1_499 and discharging atoms multiplication(one, all_1_2_2) = all_568_1_499, multiplication(one, all_1_2_2) = all_150_1_91, yields: % 66.00/31.95 | (264) all_568_1_499 = all_150_1_91 % 66.00/31.95 | % 66.00/31.95 | Instantiating formula (21) with all_150_1_91, all_150_0_90 and discharging atoms addition(all_150_0_90, zero) = all_150_1_91, yields: % 66.00/31.95 | (265) all_150_0_90 = all_150_1_91 % 66.00/31.95 | % 66.00/31.95 | Combining equations (255,256) yields a new equation: % 66.00/31.95 | (266) all_1256_1_1144 = all_1_0_0 % 66.00/31.95 | % 66.00/31.95 | Combining equations (257,256) yields a new equation: % 66.00/31.95 | (267) all_1256_1_1144 = all_1244_1_1140 % 66.00/31.95 | % 66.00/31.95 | Combining equations (259,260) yields a new equation: % 66.00/31.95 | (268) all_854_1_727 = all_782_1_672 % 66.00/31.95 | % 66.00/31.95 | Simplifying 268 yields: % 66.00/31.95 | (269) all_854_1_727 = all_782_1_672 % 66.00/31.95 | % 66.00/31.95 | Combining equations (267,266) yields a new equation: % 66.00/31.95 | (270) all_1244_1_1140 = all_1_0_0 % 66.00/31.95 | % 66.00/31.95 | Simplifying 270 yields: % 66.00/31.95 | (271) all_1244_1_1140 = all_1_0_0 % 66.00/31.95 | % 66.00/31.95 | Combining equations (271,258) yields a new equation: % 66.00/31.95 | (272) all_150_0_90 = all_1_0_0 % 66.00/31.95 | % 66.00/31.95 | Combining equations (263,269) yields a new equation: % 66.00/31.95 | (273) all_782_1_672 = all_408_1_344 % 66.00/31.95 | % 66.00/31.95 | Combining equations (261,269) yields a new equation: % 66.00/31.95 | (274) all_782_1_672 = all_568_1_499 % 66.00/31.95 | % 66.00/31.95 | Combining equations (274,273) yields a new equation: % 66.00/31.95 | (275) all_568_1_499 = all_408_1_344 % 66.00/31.95 | % 66.00/31.95 | Simplifying 275 yields: % 66.00/31.95 | (276) all_568_1_499 = all_408_1_344 % 66.00/31.95 | % 66.00/31.95 | Combining equations (264,276) yields a new equation: % 66.00/31.95 | (277) all_408_1_344 = all_150_1_91 % 66.00/31.95 | % 66.00/31.95 | Combining equations (262,276) yields a new equation: % 66.00/31.95 | (278) all_408_1_344 = all_1_2_2 % 66.00/31.95 | % 66.00/31.95 | Combining equations (278,277) yields a new equation: % 66.00/31.95 | (279) all_150_1_91 = all_1_2_2 % 66.00/31.95 | % 66.00/31.95 | Combining equations (265,272) yields a new equation: % 66.00/31.95 | (280) all_150_1_91 = all_1_0_0 % 66.00/31.95 | % 66.00/31.95 | Simplifying 280 yields: % 66.00/31.95 | (281) all_150_1_91 = all_1_0_0 % 66.00/31.95 | % 66.00/31.95 | Combining equations (281,279) yields a new equation: % 66.00/31.95 | (282) all_1_0_0 = all_1_2_2 % 66.00/31.95 | % 66.00/31.95 | Simplifying 282 yields: % 66.00/31.95 | (283) all_1_0_0 = all_1_2_2 % 66.00/31.95 | % 66.00/31.95 | Equations (283) can reduce 48 to: % 66.00/31.95 | (284) $false % 66.00/31.95 | % 66.00/31.95 |-The branch is then unsatisfiable % 66.00/31.95 % SZS output end Proof for theBenchmark % 66.00/31.95 % 66.00/31.95 31341ms %------------------------------------------------------------------------------