%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SWX047+1 : TPTP v9.1.0. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n027.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 : 300s % DateTime : Tue Apr 1 02:13:00 AM UTC 2025 % Result : Theorem 16.86s 4.69s % Output : Proof 156.34s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SWX047+1 : TPTP v9.1.0. Released v9.1.0. % 0.12/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.34 % Computer : n027.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Mon Mar 31 14:56:06 EDT 2025 % 0.12/0.34 % CPUTime : % 0.19/0.58 ____ _ % 0.19/0.58 ___ / __ \_____(_)___ ________ __________ % 0.19/0.58 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.19/0.58 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.19/0.58 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.19/0.58 % 0.19/0.58 A Theorem Prover for First-Order Logic % 0.19/0.58 (ePrincess v.1.0) % 0.19/0.58 % 0.19/0.58 (c) Philipp Rümmer, 2009-2015 % 0.19/0.58 (c) Peter Backeman, 2014-2015 % 0.19/0.58 (contributions by Angelo Brillout, Peter Baumgartner) % 0.19/0.58 Free software under GNU Lesser General Public License (LGPL). % 0.19/0.58 Bug reports to peter@backeman.se % 0.19/0.58 % 0.19/0.58 For more information, visit http://user.uu.se/~petba168/breu/ % 0.19/0.58 % 0.19/0.58 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.68/0.63 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 2.20/1.07 Prover 0: Preprocessing ... % 4.36/1.61 Prover 0: Warning: ignoring some quantifiers % 4.47/1.64 Prover 0: Constructing countermodel ... % 16.86/4.69 Prover 0: proved (4057ms) % 16.86/4.69 % 16.86/4.69 No countermodel exists, formula is valid % 16.86/4.69 % SZS status Theorem for theBenchmark % 16.86/4.69 % 16.86/4.69 Generating proof ... Warning: ignoring some quantifiers % 155.51/109.16 found it (size 37) % 155.51/109.16 % 155.51/109.16 % SZS output start Proof for theBenchmark % 155.51/109.16 Assumed formulas after preprocessing and simplification: % 155.51/109.16 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ( ~ (v1 = 0) & @*(v1, v3) = v5 & @*(v1, v2) = v4 & s(0) = v0 & nat_succeeds(v3) & nat_succeeds(v1) & nat_succeeds(0) & @<_succeeds(v2, v3) & gr(0) & ~ nat_fails(0) & ~ @<_succeeds(v4, v5) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ( ~ (@*(v15, v14) = v17) | ~ (@*(v15, v13) = v16) | ~ (@+(v16, v17) = v18) | ~ nat_succeeds(v15) | ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | ? [v19] : (@*(v15, v19) = v18 & @+(v13, v14) = v19)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ( ~ (@*(v14, v15) = v17) | ~ (@*(v13, v15) = v16) | ~ (@+(v16, v17) = v18) | ~ nat_succeeds(v15) | ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | ? [v19] : (@*(v19, v15) = v18 & @+(v13, v14) = v19)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ( ~ (@+(v15, v16) = v18) | ~ (@+(v13, v14) = v17) | ~ nat_succeeds(v15) | ~ @<_succeeds(v14, v16) | ~ @<_succeeds(v13, v15) | @<_succeeds(v17, v18)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ( ~ (@+(v15, v16) = v18) | ~ (@+(v13, v14) = v17) | ~ nat_succeeds(v15) | ~ @<_succeeds(v14, v16) | ~ @=<_succeeds(v13, v15) | @<_succeeds(v17, v18)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ( ~ (@+(v15, v16) = v18) | ~ (@+(v13, v14) = v17) | ~ nat_succeeds(v15) | ~ @<_succeeds(v13, v15) | ~ @=<_succeeds(v14, v16) | @<_succeeds(v17, v18)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ! [v18] : ( ~ (@+(v15, v16) = v18) | ~ (@+(v13, v14) = v17) | ~ nat_succeeds(v15) | ~ @=<_succeeds(v14, v16) | ~ @=<_succeeds(v13, v15) | @=<_succeeds(v17, v18)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (@*(v16, v15) = v17) | ~ (@*(v13, v14) = v16) | ~ nat_succeeds(v15) | ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | ? [v18] : (@*(v14, v15) = v18 & @*(v13, v18) = v17)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (@*(v16, v15) = v17) | ~ (@+(v13, v14) = v16) | ~ nat_succeeds(v15) | ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | ? [v18] : ? [v19] : (@*(v14, v15) = v19 & @*(v13, v15) = v18 & @+(v18, v19) = v17)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (@*(v15, v16) = v17) | ~ (@+(v13, v14) = v16) | ~ nat_succeeds(v15) | ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | ? [v18] : ? [v19] : (@*(v15, v14) = v19 & @*(v15, v13) = v18 & @+(v18, v19) = v17)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (@*(v14, v15) = v17) | ~ (@*(v13, v15) = v16) | ~ nat_succeeds(v15) | ~ nat_succeeds(v14) | ~ @=<_succeeds(v13, v14) | @=<_succeeds(v16, v17)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (@*(v14, v15) = v16) | ~ (@*(v13, v16) = v17) | ~ nat_succeeds(v15) | ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | ? [v18] : (@*(v18, v15) = v17 & @*(v13, v14) = v18)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (@*(v13, v15) = v17) | ~ (@*(v13, v14) = v16) | ~ nat_succeeds(v15) | ~ nat_succeeds(v13) | ~ @=<_succeeds(v14, v15) | @=<_succeeds(v16, v17)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (@+(v16, v15) = v17) | ~ (@+(v13, v14) = v16) | ~ nat_succeeds(v15) | ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | ? [v18] : (@+(v14, v15) = v18 & @+(v13, v18) = v17)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (@+(v14, v15) = v17) | ~ (@+(v13, v15) = v16) | ~ nat_succeeds(v15) | ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | ~ @<_succeeds(v16, v17) | @<_succeeds(v13, v14)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (@+(v14, v15) = v17) | ~ (@+(v13, v15) = v16) | ~ nat_succeeds(v15) | ~ nat_succeeds(v14) | ~ @<_succeeds(v13, v14) | @<_succeeds(v16, v17)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (@+(v14, v15) = v17) | ~ (@+(v13, v15) = v16) | ~ nat_succeeds(v15) | ~ nat_succeeds(v14) | ~ @=<_succeeds(v13, v14) | @=<_succeeds(v16, v17)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (@+(v14, v15) = v16) | ~ (@+(v13, v16) = v17) | ~ nat_succeeds(v15) | ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | ? [v18] : (@+(v18, v15) = v17 & @+(v13, v14) = v18)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (@+(v13, v15) = v17) | ~ (@+(v13, v14) = v16) | ~ nat_succeeds(v13) | ~ @<_succeeds(v16, v17) | @<_succeeds(v14, v15)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (@+(v13, v15) = v17) | ~ (@+(v13, v14) = v16) | ~ nat_succeeds(v13) | ~ @<_succeeds(v14, v15) | @<_succeeds(v16, v17)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (@+(v13, v15) = v17) | ~ (@+(v13, v14) = v16) | ~ nat_succeeds(v13) | ~ @=<_succeeds(v16, v17) | @=<_succeeds(v14, v15)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (@+(v13, v15) = v17) | ~ (@+(v13, v14) = v16) | ~ nat_succeeds(v13) | ~ @=<_succeeds(v14, v15) | @=<_succeeds(v16, v17)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (s(v17) = v15) | ~ (s(v16) = v13) | ~ plus_terminates(v13, v14, v15) | plus_terminates(v16, v14, v17)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (s(v17) = v15) | ~ (s(v16) = v13) | ~ plus_fails(v13, v14, v15) | plus_fails(v16, v14, v17)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (s(v17) = v15) | ~ (s(v16) = v13) | ~ plus_succeeds(v16, v14, v17) | plus_succeeds(v13, v14, v15)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (s(v16) = v13) | ~ plus_succeeds(v14, v17, v15) | ~ times_succeeds(v16, v14, v17) | times_succeeds(v13, v14, v15)) & ? [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (s(v17) = v14) | ~ times_terminates(v14, v15, v16) | plus_terminates(v15, v13, v16) | times_fails(v17, v15, v13)) & ? [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (s(v17) = v14) | ~ times_terminates(v14, v15, v16) | times_terminates(v17, v15, v13)) & ? [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : ( ~ (s(v17) = v14) | ~ times_fails(v14, v15, v16) | plus_fails(v15, v13, v16) | times_fails(v17, v15, v13)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : (v16 = v15 | ~ (@*(v13, v14) = v16) | ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | ~ times_succeeds(v13, v14, v15)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : (v16 = v15 | ~ (@+(v13, v14) = v16) | ~ nat_succeeds(v13) | ~ plus_succeeds(v13, v14, v15)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : (v16 = v15 | ~ plus_succeeds(v13, v14, v16) | ~ plus_succeeds(v13, v14, v15)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : (v16 = v15 | ~ times_succeeds(v13, v14, v16) | ~ times_succeeds(v13, v14, v15)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : (v15 = v14 | ~ (@+(v13, v15) = v16) | ~ (@+(v13, v14) = v16) | ~ nat_succeeds(v13)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : (v14 = v13 | ~ (@*(v16, v15) = v14) | ~ (@*(v16, v15) = v13)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : (v14 = v13 | ~ (@+(v16, v15) = v14) | ~ (@+(v16, v15) = v13)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ (@*(v15, v14) = v16) | ~ (s(v13) = v15) | ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | ? [v17] : (@*(v13, v14) = v17 & @+(v14, v17) = v16)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ (@*(v13, v15) = v16) | ~ (s(v14) = v15) | ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | ? [v17] : (@*(v13, v14) = v17 & @+(v17, v13) = v16)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ (@*(v13, v14) = v15) | ~ (@+(v15, v13) = v16) | ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | ? [v17] : (@*(v13, v17) = v16 & s(v14) = v17)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ (@*(v13, v14) = v15) | ~ (@+(v14, v15) = v16) | ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | ? [v17] : (@*(v17, v14) = v16 & s(v13) = v17)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ (@+(v15, v14) = v16) | ~ (s(v13) = v15) | ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | ? [v17] : (@+(v13, v17) = v16 & s(v14) = v17)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ (@+(v15, v14) = v16) | ~ (s(v13) = v15) | ~ nat_succeeds(v13) | ? [v17] : (@+(v13, v14) = v17 & s(v17) = v16)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ (@+(v13, v15) = v16) | ~ (s(v14) = v15) | ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | ? [v17] : (@+(v17, v14) = v16 & s(v13) = v17)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ (@+(v13, v15) = v16) | ~ (s(v14) = v15) | ~ nat_succeeds(v13) | @<_succeeds(v13, v16)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ (s(v16) = v14) | ~ (s(v15) = v13) | ~ @<_terminates(v13, v14) | @<_terminates(v15, v16)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ (s(v16) = v14) | ~ (s(v15) = v13) | ~ @<_fails(v13, v14) | @<_fails(v15, v16)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ (s(v16) = v14) | ~ (s(v15) = v13) | ~ @<_succeeds(v15, v16) | @<_succeeds(v13, v14)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ (s(v16) = v14) | ~ (s(v15) = v13) | ~ @=<_terminates(v13, v14) | @=<_terminates(v15, v16)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ (s(v16) = v14) | ~ (s(v15) = v13) | ~ @=<_fails(v13, v14) | @=<_fails(v15, v16)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ (s(v16) = v14) | ~ (s(v15) = v13) | ~ @=<_succeeds(v15, v16) | @=<_succeeds(v13, v14)) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : ( ~ (s(v15) = v16) | ~ @<_succeeds(v14, v16) | ~ @<_succeeds(v13, v14) | @<_succeeds(v13, v15)) & ! [v13] : ! [v14] : ! [v15] : (v15 = v14 | ~ plus_succeeds(v13, v14, v15) | ? [v16] : ? [v17] : (s(v17) = v15 & s(v16) = v13 & plus_succeeds(v16, v14, v17))) & ! [v13] : ! [v14] : ! [v15] : (v15 = 0 | ~ times_succeeds(v13, v14, v15) | ? [v16] : ? [v17] : (s(v16) = v13 & plus_succeeds(v14, v17, v15) & times_succeeds(v16, v14, v17))) & ! [v13] : ! [v14] : ! [v15] : (v14 = v13 | ~ (s(v15) = v14) | ~ (s(v15) = v13)) & ! [v13] : ! [v14] : ! [v15] : (v14 = v13 | ~ (s(v14) = v15) | ~ (s(v13) = v15)) & ! [v13] : ! [v14] : ! [v15] : (v14 = v13 | ~ (s(v14) = v15) | ~ nat_succeeds(v14) | ~ @<_succeeds(v13, v15) | @<_succeeds(v13, v14)) & ! [v13] : ! [v14] : ! [v15] : (v13 = 0 | ~ plus_succeeds(v13, v14, v15) | ? [v16] : ? [v17] : (s(v17) = v15 & s(v16) = v13 & plus_succeeds(v16, v14, v17))) & ! [v13] : ! [v14] : ! [v15] : (v13 = 0 | ~ times_succeeds(v13, v14, v15) | ? [v16] : ? [v17] : (s(v16) = v13 & plus_succeeds(v14, v17, v15) & times_succeeds(v16, v14, v17))) & ! [v13] : ! [v14] : ! [v15] : ( ~ (@*(v14, v13) = v15) | ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | @*(v13, v14) = v15) & ! [v13] : ! [v14] : ! [v15] : ( ~ (@*(v13, v14) = v15) | ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | @*(v14, v13) = v15) & ! [v13] : ! [v14] : ! [v15] : ( ~ (@*(v13, v14) = v15) | ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | nat_succeeds(v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ (@*(v13, v14) = v15) | ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | times_succeeds(v13, v14, v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ (@+(v14, v13) = v15) | ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | ~ @<_succeeds(0, v14) | @<_succeeds(v13, v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ (@+(v14, v13) = v15) | ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | @+(v13, v14) = v15) & ! [v13] : ! [v14] : ! [v15] : ( ~ (@+(v13, v14) = v15) | ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | @+(v14, v13) = v15) & ! [v13] : ! [v14] : ! [v15] : ( ~ (@+(v13, v14) = v15) | ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | nat_succeeds(v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ (@+(v13, v14) = v15) | ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | @=<_succeeds(v14, v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ (@+(v13, v14) = v15) | ~ nat_succeeds(v13) | @=<_succeeds(v13, v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ (@+(v13, v14) = v15) | ~ nat_succeeds(v13) | plus_succeeds(v13, v14, v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ (@+(v13, v14) = v15) | ~ nat_succeeds(v13) | ? [v16] : ? [v17] : (@+(v16, v14) = v17 & s(v15) = v17 & s(v13) = v16)) & ! [v13] : ! [v14] : ! [v15] : ( ~ (s(v14) = v15) | ~ @<_succeeds(v13, v14) | @<_succeeds(v13, v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ nat_succeeds(v15) | ~ plus_succeeds(v13, v14, v15) | nat_succeeds(v14)) & ! [v13] : ! [v14] : ! [v15] : ( ~ nat_succeeds(v14) | ~ plus_succeeds(v13, v14, v15) | nat_succeeds(v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ nat_succeeds(v14) | ~ times_succeeds(v13, v14, v15) | nat_succeeds(v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ @<_succeeds(v14, v15) | ~ @<_succeeds(v13, v14) | @<_succeeds(v13, v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ @<_succeeds(v14, v15) | ~ @=<_succeeds(v13, v14) | @<_succeeds(v13, v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ @<_succeeds(v13, v14) | ~ @=<_succeeds(v14, v15) | @<_succeeds(v13, v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ @=<_succeeds(v14, v15) | ~ @=<_succeeds(v13, v14) | @=<_succeeds(v13, v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ plus_terminates(v13, v14, v15) | plus_fails(v13, v14, v15) | plus_succeeds(v13, v14, v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ plus_fails(v13, v14, v15) | ~ plus_succeeds(v13, v14, v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ plus_succeeds(v13, v14, v15) | ~ gr(v15) | gr(v14)) & ! [v13] : ! [v14] : ! [v15] : ( ~ plus_succeeds(v13, v14, v15) | ~ gr(v14) | gr(v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ plus_succeeds(v13, v14, v15) | nat_succeeds(v13)) & ! [v13] : ! [v14] : ! [v15] : ( ~ plus_succeeds(v13, v14, v15) | plus_terminates(v13, v14, v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ plus_succeeds(v13, v14, v15) | gr(v13)) & ! [v13] : ! [v14] : ! [v15] : ( ~ times_terminates(v13, v14, v15) | times_fails(v13, v14, v15) | times_succeeds(v13, v14, v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ times_fails(v13, v14, v15) | ~ times_succeeds(v13, v14, v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ times_succeeds(v13, v14, v15) | ~ gr(v14) | gr(v15)) & ! [v13] : ! [v14] : ! [v15] : ( ~ times_succeeds(v13, v14, v15) | nat_succeeds(v13)) & ! [v13] : ! [v14] : ! [v15] : ( ~ times_succeeds(v13, v14, v15) | gr(v13)) & ? [v13] : ! [v14] : ! [v15] : ( ~ nat_succeeds(v15) | ~ nat_succeeds(v14) | times_terminates(v14, v15, v13)) & ! [v13] : ! [v14] : (v14 = v13 | ~ (@*(v13, v0) = v14) | ~ nat_succeeds(v13)) & ! [v13] : ! [v14] : (v14 = v13 | ~ (@*(v0, v13) = v14) | ~ nat_succeeds(v13)) & ! [v13] : ! [v14] : (v14 = v13 | ~ (@+(v13, 0) = v14) | ~ nat_succeeds(v13)) & ! [v13] : ! [v14] : (v14 = v13 | ~ (@+(0, v13) = v14)) & ! [v13] : ! [v14] : (v14 = v13 | ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | @<_succeeds(v14, v13) | @<_succeeds(v13, v14)) & ! [v13] : ! [v14] : (v14 = v13 | ~ nat_succeeds(v14) | ~ @=<_succeeds(v13, v14) | @<_succeeds(v13, v14)) & ! [v13] : ! [v14] : (v14 = v13 | ~ @=<_succeeds(v14, v13) | ~ @=<_succeeds(v13, v14)) & ! [v13] : ! [v14] : (v14 = 0 | ~ (@*(v13, 0) = v14) | ~ nat_succeeds(v13)) & ! [v13] : ! [v14] : (v14 = 0 | ~ (@*(0, v13) = v14) | ~ nat_succeeds(v13)) & ! [v13] : ! [v14] : (v13 = 0 | ~ @=<_succeeds(v13, v14) | ? [v15] : ? [v16] : (s(v16) = v14 & s(v15) = v13 & @=<_succeeds(v15, v16))) & ! [v13] : ! [v14] : ( ~ (s(v14) = v13) | ~ nat_terminates(v13) | nat_terminates(v14)) & ! [v13] : ! [v14] : ( ~ (s(v14) = v13) | ~ nat_fails(v13) | nat_fails(v14)) & ! [v13] : ! [v14] : ( ~ (s(v14) = v13) | ~ nat_succeeds(v14) | nat_succeeds(v13)) & ! [v13] : ! [v14] : ( ~ (s(v14) = v13) | ~ @<_fails(0, v13)) & ! [v13] : ! [v14] : ( ~ (s(v14) = v13) | @<_succeeds(0, v13)) & ! [v13] : ! [v14] : ( ~ (s(v13) = v14) | ~ nat_succeeds(v13) | @<_succeeds(v13, v14)) & ! [v13] : ! [v14] : ( ~ (s(v13) = v14) | ~ nat_succeeds(v13) | @=<_fails(v14, v13)) & ! [v13] : ! [v14] : ( ~ (s(v13) = v14) | ~ nat_succeeds(v13) | @=<_succeeds(v13, v14)) & ! [v13] : ! [v14] : ( ~ (s(v13) = v14) | ~ gr(v14) | gr(v13)) & ! [v13] : ! [v14] : ( ~ (s(v13) = v14) | ~ gr(v13) | gr(v14)) & ! [v13] : ! [v14] : ( ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | ~ @=<_fails(v13, v14) | @=<_succeeds(v14, v13)) & ! [v13] : ! [v14] : ( ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | @<_succeeds(v13, v14) | @=<_succeeds(v14, v13)) & ! [v13] : ! [v14] : ( ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | @=<_succeeds(v14, v13) | @=<_succeeds(v13, v14)) & ! [v13] : ! [v14] : ( ~ nat_succeeds(v14) | ~ nat_succeeds(v13) | ? [v15] : times_succeeds(v13, v14, v15)) & ! [v13] : ! [v14] : ( ~ @<_terminates(v13, v14) | @<_fails(v13, v14) | @<_succeeds(v13, v14)) & ! [v13] : ! [v14] : ( ~ @<_fails(v13, v14) | ~ @<_succeeds(v13, v14)) & ! [v13] : ! [v14] : ( ~ @<_succeeds(v13, v14) | nat_succeeds(v13)) & ! [v13] : ! [v14] : ( ~ @<_succeeds(v13, v14) | @=<_succeeds(v13, v14)) & ! [v13] : ! [v14] : ( ~ @<_succeeds(v13, v14) | ? [v15] : ? [v16] : ? [v17] : ? [v18] : ((v18 = v14 & v17 = v13 & s(v16) = v14 & s(v15) = v13 & @<_succeeds(v15, v16)) | (v16 = v14 & v13 = 0 & s(v15) = v14))) & ! [v13] : ! [v14] : ( ~ @<_succeeds(v13, v14) | ? [v15] : ? [v16] : (@+(v13, v16) = v14 & s(v15) = v16)) & ! [v13] : ! [v14] : ( ~ @<_succeeds(v13, v14) | ? [v15] : ? [v16] : (s(v15) = v16 & plus_succeeds(v13, v16, v14))) & ! [v13] : ! [v14] : ( ~ @<_succeeds(v13, v14) | ? [v15] : s(v15) = v14) & ! [v13] : ! [v14] : ( ~ @=<_terminates(v13, v14) | @=<_fails(v13, v14) | @=<_succeeds(v13, v14)) & ! [v13] : ! [v14] : ( ~ @=<_fails(v13, v14) | ~ @=<_succeeds(v13, v14)) & ! [v13] : ! [v14] : ( ~ @=<_succeeds(v13, v14) | nat_succeeds(v13)) & ! [v13] : ! [v14] : ( ~ @=<_succeeds(v13, v14) | ? [v15] : @+(v13, v15) = v14) & ! [v13] : ! [v14] : ( ~ @=<_succeeds(v13, v14) | ? [v15] : plus_succeeds(v13, v15, v14)) & ? [v13] : ? [v14] : ! [v15] : ( ~ nat_succeeds(v15) | plus_terminates(v15, v13, v14)) & ? [v13] : ? [v14] : ! [v15] : ( ~ nat_succeeds(v15) | plus_terminates(v13, v14, v15)) & ? [v13] : ! [v14] : ( ~ nat_succeeds(v14) | @<_terminates(v14, v13)) & ? [v13] : ! [v14] : ( ~ nat_succeeds(v14) | @<_terminates(v13, v14)) & ? [v13] : ! [v14] : ( ~ nat_succeeds(v14) | @=<_terminates(v14, v13)) & ? [v13] : ! [v14] : ( ~ nat_succeeds(v14) | @=<_terminates(v13, v14)) & ? [v13] : ! [v14] : ( ~ nat_succeeds(v14) | ? [v15] : plus_succeeds(v14, v13, v15)) & ! [v13] : (v13 = 0 | ~ nat_succeeds(v13) | @<_succeeds(0, v13)) & ! [v13] : (v13 = 0 | ~ nat_succeeds(v13) | ? [v14] : (s(v14) = v13 & nat_succeeds(v14))) & ! [v13] : ~ (s(v13) = 0) & ! [v13] : ( ~ nat_terminates(v13) | nat_fails(v13) | nat_succeeds(v13)) & ! [v13] : ( ~ nat_fails(v13) | ~ nat_succeeds(v13)) & ! [v13] : ( ~ nat_succeeds(v13) | ~ @<_succeeds(v13, v13)) & ! [v13] : ( ~ nat_succeeds(v13) | nat_terminates(v13)) & ! [v13] : ( ~ nat_succeeds(v13) | @<_fails(v13, v13)) & ! [v13] : ( ~ nat_succeeds(v13) | @=<_succeeds(v13, v13)) & ! [v13] : ( ~ nat_succeeds(v13) | gr(v13)) & ! [v13] : ~ @=<_fails(0, v13) & ! [v13] : ~ plus_fails(0, v13, v13) & ! [v13] : ~ times_fails(0, v13, 0) & ? [v13] : ? [v14] : ? [v15] : (v15 = v14 | plus_fails(v13, v14, v15) | ? [v16] : ? [v17] : (s(v17) = v15 & s(v16) = v13 & ~ plus_fails(v16, v14, v17))) & ? [v13] : ? [v14] : ? [v15] : (v15 = 0 | times_fails(v13, v14, v15) | ? [v16] : ? [v17] : (s(v16) = v13 & ~ plus_fails(v14, v17, v15) & ~ times_fails(v16, v14, v17))) & ? [v13] : ? [v14] : ? [v15] : (v13 = 0 | plus_fails(v13, v14, v15) | ? [v16] : ? [v17] : (s(v17) = v15 & s(v16) = v13 & ~ plus_fails(v16, v14, v17))) & ? [v13] : ? [v14] : ? [v15] : (v13 = 0 | times_fails(v13, v14, v15) | ? [v16] : ? [v17] : (s(v16) = v13 & ~ plus_fails(v14, v17, v15) & ~ times_fails(v16, v14, v17))) & ? [v13] : ? [v14] : ? [v15] : (plus_terminates(v13, v14, v15) | ? [v16] : ? [v17] : (s(v17) = v15 & s(v16) = v13 & ~ plus_terminates(v16, v14, v17))) & ? [v13] : ? [v14] : ? [v15] : (times_terminates(v13, v14, v15) | ? [v16] : ? [v17] : (s(v16) = v13 & ( ~ times_terminates(v16, v14, v17) | ( ~ plus_terminates(v14, v17, v15) & ~ times_fails(v16, v14, v17))))) & ? [v13] : ? [v14] : (v13 = 0 | @=<_fails(v13, v14) | ? [v15] : ? [v16] : (s(v16) = v14 & s(v15) = v13 & ~ @=<_fails(v15, v16))) & ? [v13] : ? [v14] : (@<_terminates(v13, v14) | ? [v15] : ? [v16] : (s(v16) = v14 & s(v15) = v13 & ~ @<_terminates(v15, v16))) & ? [v13] : ? [v14] : (@<_fails(v13, v14) | ? [v15] : ? [v16] : ? [v17] : ? [v18] : ((v18 = v14 & v17 = v13 & s(v16) = v14 & s(v15) = v13 & ~ @<_fails(v15, v16)) | (v16 = v14 & v13 = 0 & s(v15) = v14))) & ? [v13] : ? [v14] : (@=<_terminates(v13, v14) | ? [v15] : ? [v16] : (s(v16) = v14 & s(v15) = v13 & ~ @=<_terminates(v15, v16))) & ? [v13] : (v13 = 0 | nat_fails(v13) | ? [v14] : (s(v14) = v13 & ~ nat_fails(v14))) & ? [v13] : (nat_terminates(v13) | ? [v14] : (s(v14) = v13 & ~ nat_terminates(v14))) & ? [v13] : @=<_succeeds(0, v13) & ? [v13] : plus_succeeds(0, v13, v13) & ? [v13] : times_succeeds(0, v13, 0) & ( ! [v13] : ! [v14] : ! [v15] : ! [v16] : ! [v17] : (v13 = 0 | ~ (@*(v13, v15) = v17) | ~ (@*(v13, v14) = v16) | ~ nat_succeeds(v15) | ~ nat_succeeds(v13) | ~ @<_succeeds(v14, v15) | @<_succeeds(v16, v17)) | (v12 = v6 & ~ (v6 = 0) & @*(v6, v8) = v10 & @*(v6, v7) = v9 & s(v11) = v6 & nat_succeeds(v11) & nat_succeeds(v8) & @<_succeeds(v7, v8) & ~ @<_succeeds(v9, v10) & ! [v13] : ! [v14] : ! [v15] : ! [v16] : (v11 = 0 | ~ (@*(v11, v14) = v16) | ~ (@*(v11, v13) = v15) | ~ nat_succeeds(v14) | ~ @<_succeeds(v13, v14) | @<_succeeds(v15, v16))))) % 155.76/109.25 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6, all_0_7_7, all_0_8_8, all_0_9_9, all_0_10_10, all_0_11_11, all_0_12_12 yields: % 155.76/109.25 | (1) ~ (all_0_11_11 = 0) & @*(all_0_11_11, all_0_9_9) = all_0_7_7 & @*(all_0_11_11, all_0_10_10) = all_0_8_8 & s(0) = all_0_12_12 & nat_succeeds(all_0_9_9) & nat_succeeds(all_0_11_11) & nat_succeeds(0) & @<_succeeds(all_0_10_10, all_0_9_9) & gr(0) & ~ nat_fails(0) & ~ @<_succeeds(all_0_8_8, all_0_7_7) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (@*(v2, v1) = v4) | ~ (@*(v2, v0) = v3) | ~ (@+(v3, v4) = v5) | ~ nat_succeeds(v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v6] : (@*(v2, v6) = v5 & @+(v0, v1) = v6)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (@*(v1, v2) = v4) | ~ (@*(v0, v2) = v3) | ~ (@+(v3, v4) = v5) | ~ nat_succeeds(v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v6] : (@*(v6, v2) = v5 & @+(v0, v1) = v6)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (@+(v2, v3) = v5) | ~ (@+(v0, v1) = v4) | ~ nat_succeeds(v2) | ~ @<_succeeds(v1, v3) | ~ @<_succeeds(v0, v2) | @<_succeeds(v4, v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (@+(v2, v3) = v5) | ~ (@+(v0, v1) = v4) | ~ nat_succeeds(v2) | ~ @<_succeeds(v1, v3) | ~ @=<_succeeds(v0, v2) | @<_succeeds(v4, v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (@+(v2, v3) = v5) | ~ (@+(v0, v1) = v4) | ~ nat_succeeds(v2) | ~ @<_succeeds(v0, v2) | ~ @=<_succeeds(v1, v3) | @<_succeeds(v4, v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (@+(v2, v3) = v5) | ~ (@+(v0, v1) = v4) | ~ nat_succeeds(v2) | ~ @=<_succeeds(v1, v3) | ~ @=<_succeeds(v0, v2) | @=<_succeeds(v4, v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@*(v3, v2) = v4) | ~ (@*(v0, v1) = v3) | ~ nat_succeeds(v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v5] : (@*(v1, v2) = v5 & @*(v0, v5) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@*(v3, v2) = v4) | ~ (@+(v0, v1) = v3) | ~ nat_succeeds(v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v5] : ? [v6] : (@*(v1, v2) = v6 & @*(v0, v2) = v5 & @+(v5, v6) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@*(v2, v3) = v4) | ~ (@+(v0, v1) = v3) | ~ nat_succeeds(v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v5] : ? [v6] : (@*(v2, v1) = v6 & @*(v2, v0) = v5 & @+(v5, v6) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@*(v1, v2) = v4) | ~ (@*(v0, v2) = v3) | ~ nat_succeeds(v2) | ~ nat_succeeds(v1) | ~ @=<_succeeds(v0, v1) | @=<_succeeds(v3, v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@*(v1, v2) = v3) | ~ (@*(v0, v3) = v4) | ~ nat_succeeds(v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v5] : (@*(v5, v2) = v4 & @*(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@*(v0, v2) = v4) | ~ (@*(v0, v1) = v3) | ~ nat_succeeds(v2) | ~ nat_succeeds(v0) | ~ @=<_succeeds(v1, v2) | @=<_succeeds(v3, v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@+(v3, v2) = v4) | ~ (@+(v0, v1) = v3) | ~ nat_succeeds(v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v5] : (@+(v1, v2) = v5 & @+(v0, v5) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@+(v1, v2) = v4) | ~ (@+(v0, v2) = v3) | ~ nat_succeeds(v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ~ @<_succeeds(v3, v4) | @<_succeeds(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@+(v1, v2) = v4) | ~ (@+(v0, v2) = v3) | ~ nat_succeeds(v2) | ~ nat_succeeds(v1) | ~ @<_succeeds(v0, v1) | @<_succeeds(v3, v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@+(v1, v2) = v4) | ~ (@+(v0, v2) = v3) | ~ nat_succeeds(v2) | ~ nat_succeeds(v1) | ~ @=<_succeeds(v0, v1) | @=<_succeeds(v3, v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@+(v1, v2) = v3) | ~ (@+(v0, v3) = v4) | ~ nat_succeeds(v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v5] : (@+(v5, v2) = v4 & @+(v0, v1) = v5)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@+(v0, v2) = v4) | ~ (@+(v0, v1) = v3) | ~ nat_succeeds(v0) | ~ @<_succeeds(v3, v4) | @<_succeeds(v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@+(v0, v2) = v4) | ~ (@+(v0, v1) = v3) | ~ nat_succeeds(v0) | ~ @<_succeeds(v1, v2) | @<_succeeds(v3, v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@+(v0, v2) = v4) | ~ (@+(v0, v1) = v3) | ~ nat_succeeds(v0) | ~ @=<_succeeds(v3, v4) | @=<_succeeds(v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@+(v0, v2) = v4) | ~ (@+(v0, v1) = v3) | ~ nat_succeeds(v0) | ~ @=<_succeeds(v1, v2) | @=<_succeeds(v3, v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (s(v4) = v2) | ~ (s(v3) = v0) | ~ plus_terminates(v0, v1, v2) | plus_terminates(v3, v1, v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (s(v4) = v2) | ~ (s(v3) = v0) | ~ plus_fails(v0, v1, v2) | plus_fails(v3, v1, v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (s(v4) = v2) | ~ (s(v3) = v0) | ~ plus_succeeds(v3, v1, v4) | plus_succeeds(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (s(v3) = v0) | ~ plus_succeeds(v1, v4, v2) | ~ times_succeeds(v3, v1, v4) | times_succeeds(v0, v1, v2)) & ? [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (s(v4) = v1) | ~ times_terminates(v1, v2, v3) | plus_terminates(v2, v0, v3) | times_fails(v4, v2, v0)) & ? [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (s(v4) = v1) | ~ times_terminates(v1, v2, v3) | times_terminates(v4, v2, v0)) & ? [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (s(v4) = v1) | ~ times_fails(v1, v2, v3) | plus_fails(v2, v0, v3) | times_fails(v4, v2, v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (@*(v0, v1) = v3) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ~ times_succeeds(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (@+(v0, v1) = v3) | ~ nat_succeeds(v0) | ~ plus_succeeds(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ plus_succeeds(v0, v1, v3) | ~ plus_succeeds(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ times_succeeds(v0, v1, v3) | ~ times_succeeds(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = v1 | ~ (@+(v0, v2) = v3) | ~ (@+(v0, v1) = v3) | ~ nat_succeeds(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (@*(v3, v2) = v1) | ~ (@*(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (@+(v3, v2) = v1) | ~ (@+(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (@*(v2, v1) = v3) | ~ (s(v0) = v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v4] : (@*(v0, v1) = v4 & @+(v1, v4) = v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (@*(v0, v2) = v3) | ~ (s(v1) = v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v4] : (@*(v0, v1) = v4 & @+(v4, v0) = v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (@*(v0, v1) = v2) | ~ (@+(v2, v0) = v3) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v4] : (@*(v0, v4) = v3 & s(v1) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (@*(v0, v1) = v2) | ~ (@+(v1, v2) = v3) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v4] : (@*(v4, v1) = v3 & s(v0) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (@+(v2, v1) = v3) | ~ (s(v0) = v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v4] : (@+(v0, v4) = v3 & s(v1) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (@+(v2, v1) = v3) | ~ (s(v0) = v2) | ~ nat_succeeds(v0) | ? [v4] : (@+(v0, v1) = v4 & s(v4) = v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (@+(v0, v2) = v3) | ~ (s(v1) = v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v4] : (@+(v4, v1) = v3 & s(v0) = v4)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (@+(v0, v2) = v3) | ~ (s(v1) = v2) | ~ nat_succeeds(v0) | @<_succeeds(v0, v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (s(v3) = v1) | ~ (s(v2) = v0) | ~ @<_terminates(v0, v1) | @<_terminates(v2, v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (s(v3) = v1) | ~ (s(v2) = v0) | ~ @<_fails(v0, v1) | @<_fails(v2, v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (s(v3) = v1) | ~ (s(v2) = v0) | ~ @<_succeeds(v2, v3) | @<_succeeds(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (s(v3) = v1) | ~ (s(v2) = v0) | ~ @=<_terminates(v0, v1) | @=<_terminates(v2, v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (s(v3) = v1) | ~ (s(v2) = v0) | ~ @=<_fails(v0, v1) | @=<_fails(v2, v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (s(v3) = v1) | ~ (s(v2) = v0) | ~ @=<_succeeds(v2, v3) | @=<_succeeds(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (s(v2) = v3) | ~ @<_succeeds(v1, v3) | ~ @<_succeeds(v0, v1) | @<_succeeds(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ plus_succeeds(v0, v1, v2) | ? [v3] : ? [v4] : (s(v4) = v2 & s(v3) = v0 & plus_succeeds(v3, v1, v4))) & ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ times_succeeds(v0, v1, v2) | ? [v3] : ? [v4] : (s(v3) = v0 & plus_succeeds(v1, v4, v2) & times_succeeds(v3, v1, v4))) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v2) = v1) | ~ (s(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v1) = v2) | ~ (s(v0) = v2)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v1) = v2) | ~ nat_succeeds(v1) | ~ @<_succeeds(v0, v2) | @<_succeeds(v0, v1)) & ! [v0] : ! [v1] : ! [v2] : (v0 = 0 | ~ plus_succeeds(v0, v1, v2) | ? [v3] : ? [v4] : (s(v4) = v2 & s(v3) = v0 & plus_succeeds(v3, v1, v4))) & ! [v0] : ! [v1] : ! [v2] : (v0 = 0 | ~ times_succeeds(v0, v1, v2) | ? [v3] : ? [v4] : (s(v3) = v0 & plus_succeeds(v1, v4, v2) & times_succeeds(v3, v1, v4))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (@*(v1, v0) = v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | @*(v0, v1) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (@*(v0, v1) = v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | @*(v1, v0) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (@*(v0, v1) = v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | nat_succeeds(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (@*(v0, v1) = v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | times_succeeds(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (@+(v1, v0) = v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ~ @<_succeeds(0, v1) | @<_succeeds(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (@+(v1, v0) = v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | @+(v0, v1) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (@+(v0, v1) = v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | @+(v1, v0) = v2) & ! [v0] : ! [v1] : ! [v2] : ( ~ (@+(v0, v1) = v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | nat_succeeds(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (@+(v0, v1) = v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | @=<_succeeds(v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (@+(v0, v1) = v2) | ~ nat_succeeds(v0) | @=<_succeeds(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (@+(v0, v1) = v2) | ~ nat_succeeds(v0) | plus_succeeds(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (@+(v0, v1) = v2) | ~ nat_succeeds(v0) | ? [v3] : ? [v4] : (@+(v3, v1) = v4 & s(v2) = v4 & s(v0) = v3)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (s(v1) = v2) | ~ @<_succeeds(v0, v1) | @<_succeeds(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ nat_succeeds(v2) | ~ plus_succeeds(v0, v1, v2) | nat_succeeds(v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ nat_succeeds(v1) | ~ plus_succeeds(v0, v1, v2) | nat_succeeds(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ nat_succeeds(v1) | ~ times_succeeds(v0, v1, v2) | nat_succeeds(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ @<_succeeds(v1, v2) | ~ @<_succeeds(v0, v1) | @<_succeeds(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ @<_succeeds(v1, v2) | ~ @=<_succeeds(v0, v1) | @<_succeeds(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ @<_succeeds(v0, v1) | ~ @=<_succeeds(v1, v2) | @<_succeeds(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ @=<_succeeds(v1, v2) | ~ @=<_succeeds(v0, v1) | @=<_succeeds(v0, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ plus_terminates(v0, v1, v2) | plus_fails(v0, v1, v2) | plus_succeeds(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ plus_fails(v0, v1, v2) | ~ plus_succeeds(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ plus_succeeds(v0, v1, v2) | ~ gr(v2) | gr(v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ plus_succeeds(v0, v1, v2) | ~ gr(v1) | gr(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ plus_succeeds(v0, v1, v2) | nat_succeeds(v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ plus_succeeds(v0, v1, v2) | plus_terminates(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ plus_succeeds(v0, v1, v2) | gr(v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ times_terminates(v0, v1, v2) | times_fails(v0, v1, v2) | times_succeeds(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ times_fails(v0, v1, v2) | ~ times_succeeds(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ times_succeeds(v0, v1, v2) | ~ gr(v1) | gr(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ times_succeeds(v0, v1, v2) | nat_succeeds(v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ times_succeeds(v0, v1, v2) | gr(v0)) & ? [v0] : ! [v1] : ! [v2] : ( ~ nat_succeeds(v2) | ~ nat_succeeds(v1) | times_terminates(v1, v2, v0)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (@*(v0, all_0_12_12) = v1) | ~ nat_succeeds(v0)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (@*(all_0_12_12, v0) = v1) | ~ nat_succeeds(v0)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (@+(v0, 0) = v1) | ~ nat_succeeds(v0)) & ! [v0] : ! [v1] : (v1 = v0 | ~ (@+(0, v0) = v1)) & ! [v0] : ! [v1] : (v1 = v0 | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | @<_succeeds(v1, v0) | @<_succeeds(v0, v1)) & ! [v0] : ! [v1] : (v1 = v0 | ~ nat_succeeds(v1) | ~ @=<_succeeds(v0, v1) | @<_succeeds(v0, v1)) & ! [v0] : ! [v1] : (v1 = v0 | ~ @=<_succeeds(v1, v0) | ~ @=<_succeeds(v0, v1)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (@*(v0, 0) = v1) | ~ nat_succeeds(v0)) & ! [v0] : ! [v1] : (v1 = 0 | ~ (@*(0, v0) = v1) | ~ nat_succeeds(v0)) & ! [v0] : ! [v1] : (v0 = 0 | ~ @=<_succeeds(v0, v1) | ? [v2] : ? [v3] : (s(v3) = v1 & s(v2) = v0 & @=<_succeeds(v2, v3))) & ! [v0] : ! [v1] : ( ~ (s(v1) = v0) | ~ nat_terminates(v0) | nat_terminates(v1)) & ! [v0] : ! [v1] : ( ~ (s(v1) = v0) | ~ nat_fails(v0) | nat_fails(v1)) & ! [v0] : ! [v1] : ( ~ (s(v1) = v0) | ~ nat_succeeds(v1) | nat_succeeds(v0)) & ! [v0] : ! [v1] : ( ~ (s(v1) = v0) | ~ @<_fails(0, v0)) & ! [v0] : ! [v1] : ( ~ (s(v1) = v0) | @<_succeeds(0, v0)) & ! [v0] : ! [v1] : ( ~ (s(v0) = v1) | ~ nat_succeeds(v0) | @<_succeeds(v0, v1)) & ! [v0] : ! [v1] : ( ~ (s(v0) = v1) | ~ nat_succeeds(v0) | @=<_fails(v1, v0)) & ! [v0] : ! [v1] : ( ~ (s(v0) = v1) | ~ nat_succeeds(v0) | @=<_succeeds(v0, v1)) & ! [v0] : ! [v1] : ( ~ (s(v0) = v1) | ~ gr(v1) | gr(v0)) & ! [v0] : ! [v1] : ( ~ (s(v0) = v1) | ~ gr(v0) | gr(v1)) & ! [v0] : ! [v1] : ( ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ~ @=<_fails(v0, v1) | @=<_succeeds(v1, v0)) & ! [v0] : ! [v1] : ( ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | @<_succeeds(v0, v1) | @=<_succeeds(v1, v0)) & ! [v0] : ! [v1] : ( ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | @=<_succeeds(v1, v0) | @=<_succeeds(v0, v1)) & ! [v0] : ! [v1] : ( ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v2] : times_succeeds(v0, v1, v2)) & ! [v0] : ! [v1] : ( ~ @<_terminates(v0, v1) | @<_fails(v0, v1) | @<_succeeds(v0, v1)) & ! [v0] : ! [v1] : ( ~ @<_fails(v0, v1) | ~ @<_succeeds(v0, v1)) & ! [v0] : ! [v1] : ( ~ @<_succeeds(v0, v1) | nat_succeeds(v0)) & ! [v0] : ! [v1] : ( ~ @<_succeeds(v0, v1) | @=<_succeeds(v0, v1)) & ! [v0] : ! [v1] : ( ~ @<_succeeds(v0, v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ((v5 = v1 & v4 = v0 & s(v3) = v1 & s(v2) = v0 & @<_succeeds(v2, v3)) | (v3 = v1 & v0 = 0 & s(v2) = v1))) & ! [v0] : ! [v1] : ( ~ @<_succeeds(v0, v1) | ? [v2] : ? [v3] : (@+(v0, v3) = v1 & s(v2) = v3)) & ! [v0] : ! [v1] : ( ~ @<_succeeds(v0, v1) | ? [v2] : ? [v3] : (s(v2) = v3 & plus_succeeds(v0, v3, v1))) & ! [v0] : ! [v1] : ( ~ @<_succeeds(v0, v1) | ? [v2] : s(v2) = v1) & ! [v0] : ! [v1] : ( ~ @=<_terminates(v0, v1) | @=<_fails(v0, v1) | @=<_succeeds(v0, v1)) & ! [v0] : ! [v1] : ( ~ @=<_fails(v0, v1) | ~ @=<_succeeds(v0, v1)) & ! [v0] : ! [v1] : ( ~ @=<_succeeds(v0, v1) | nat_succeeds(v0)) & ! [v0] : ! [v1] : ( ~ @=<_succeeds(v0, v1) | ? [v2] : @+(v0, v2) = v1) & ! [v0] : ! [v1] : ( ~ @=<_succeeds(v0, v1) | ? [v2] : plus_succeeds(v0, v2, v1)) & ? [v0] : ? [v1] : ! [v2] : ( ~ nat_succeeds(v2) | plus_terminates(v2, v0, v1)) & ? [v0] : ? [v1] : ! [v2] : ( ~ nat_succeeds(v2) | plus_terminates(v0, v1, v2)) & ? [v0] : ! [v1] : ( ~ nat_succeeds(v1) | @<_terminates(v1, v0)) & ? [v0] : ! [v1] : ( ~ nat_succeeds(v1) | @<_terminates(v0, v1)) & ? [v0] : ! [v1] : ( ~ nat_succeeds(v1) | @=<_terminates(v1, v0)) & ? [v0] : ! [v1] : ( ~ nat_succeeds(v1) | @=<_terminates(v0, v1)) & ? [v0] : ! [v1] : ( ~ nat_succeeds(v1) | ? [v2] : plus_succeeds(v1, v0, v2)) & ! [v0] : (v0 = 0 | ~ nat_succeeds(v0) | @<_succeeds(0, v0)) & ! [v0] : (v0 = 0 | ~ nat_succeeds(v0) | ? [v1] : (s(v1) = v0 & nat_succeeds(v1))) & ! [v0] : ~ (s(v0) = 0) & ! [v0] : ( ~ nat_terminates(v0) | nat_fails(v0) | nat_succeeds(v0)) & ! [v0] : ( ~ nat_fails(v0) | ~ nat_succeeds(v0)) & ! [v0] : ( ~ nat_succeeds(v0) | ~ @<_succeeds(v0, v0)) & ! [v0] : ( ~ nat_succeeds(v0) | nat_terminates(v0)) & ! [v0] : ( ~ nat_succeeds(v0) | @<_fails(v0, v0)) & ! [v0] : ( ~ nat_succeeds(v0) | @=<_succeeds(v0, v0)) & ! [v0] : ( ~ nat_succeeds(v0) | gr(v0)) & ! [v0] : ~ @=<_fails(0, v0) & ! [v0] : ~ plus_fails(0, v0, v0) & ! [v0] : ~ times_fails(0, v0, 0) & ? [v0] : ? [v1] : ? [v2] : (v2 = v1 | plus_fails(v0, v1, v2) | ? [v3] : ? [v4] : (s(v4) = v2 & s(v3) = v0 & ~ plus_fails(v3, v1, v4))) & ? [v0] : ? [v1] : ? [v2] : (v2 = 0 | times_fails(v0, v1, v2) | ? [v3] : ? [v4] : (s(v3) = v0 & ~ plus_fails(v1, v4, v2) & ~ times_fails(v3, v1, v4))) & ? [v0] : ? [v1] : ? [v2] : (v0 = 0 | plus_fails(v0, v1, v2) | ? [v3] : ? [v4] : (s(v4) = v2 & s(v3) = v0 & ~ plus_fails(v3, v1, v4))) & ? [v0] : ? [v1] : ? [v2] : (v0 = 0 | times_fails(v0, v1, v2) | ? [v3] : ? [v4] : (s(v3) = v0 & ~ plus_fails(v1, v4, v2) & ~ times_fails(v3, v1, v4))) & ? [v0] : ? [v1] : ? [v2] : (plus_terminates(v0, v1, v2) | ? [v3] : ? [v4] : (s(v4) = v2 & s(v3) = v0 & ~ plus_terminates(v3, v1, v4))) & ? [v0] : ? [v1] : ? [v2] : (times_terminates(v0, v1, v2) | ? [v3] : ? [v4] : (s(v3) = v0 & ( ~ times_terminates(v3, v1, v4) | ( ~ plus_terminates(v1, v4, v2) & ~ times_fails(v3, v1, v4))))) & ? [v0] : ? [v1] : (v0 = 0 | @=<_fails(v0, v1) | ? [v2] : ? [v3] : (s(v3) = v1 & s(v2) = v0 & ~ @=<_fails(v2, v3))) & ? [v0] : ? [v1] : (@<_terminates(v0, v1) | ? [v2] : ? [v3] : (s(v3) = v1 & s(v2) = v0 & ~ @<_terminates(v2, v3))) & ? [v0] : ? [v1] : (@<_fails(v0, v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ((v5 = v1 & v4 = v0 & s(v3) = v1 & s(v2) = v0 & ~ @<_fails(v2, v3)) | (v3 = v1 & v0 = 0 & s(v2) = v1))) & ? [v0] : ? [v1] : (@=<_terminates(v0, v1) | ? [v2] : ? [v3] : (s(v3) = v1 & s(v2) = v0 & ~ @=<_terminates(v2, v3))) & ? [v0] : (v0 = 0 | nat_fails(v0) | ? [v1] : (s(v1) = v0 & ~ nat_fails(v1))) & ? [v0] : (nat_terminates(v0) | ? [v1] : (s(v1) = v0 & ~ nat_terminates(v1))) & ? [v0] : @=<_succeeds(0, v0) & ? [v0] : plus_succeeds(0, v0, v0) & ? [v0] : times_succeeds(0, v0, 0) & ( ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v0 = 0 | ~ (@*(v0, v2) = v4) | ~ (@*(v0, v1) = v3) | ~ nat_succeeds(v2) | ~ nat_succeeds(v0) | ~ @<_succeeds(v1, v2) | @<_succeeds(v3, v4)) | (all_0_0_0 = all_0_6_6 & ~ (all_0_6_6 = 0) & @*(all_0_6_6, all_0_4_4) = all_0_2_2 & @*(all_0_6_6, all_0_5_5) = all_0_3_3 & s(all_0_1_1) = all_0_6_6 & nat_succeeds(all_0_1_1) & nat_succeeds(all_0_4_4) & @<_succeeds(all_0_5_5, all_0_4_4) & ~ @<_succeeds(all_0_3_3, all_0_2_2) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (all_0_1_1 = 0 | ~ (@*(all_0_1_1, v1) = v3) | ~ (@*(all_0_1_1, v0) = v2) | ~ nat_succeeds(v1) | ~ @<_succeeds(v0, v1) | @<_succeeds(v2, v3)))) % 156.31/109.31 | % 156.31/109.31 | Applying alpha-rule on (1) yields: % 156.31/109.31 | (2) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@+(v1, v2) = v3) | ~ (@+(v0, v3) = v4) | ~ nat_succeeds(v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v5] : (@+(v5, v2) = v4 & @+(v0, v1) = v5)) % 156.31/109.31 | (3) ? [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (s(v4) = v1) | ~ times_terminates(v1, v2, v3) | plus_terminates(v2, v0, v3) | times_fails(v4, v2, v0)) % 156.31/109.31 | (4) ! [v0] : ! [v1] : ! [v2] : ( ~ (@*(v1, v0) = v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | @*(v0, v1) = v2) % 156.31/109.31 | (5) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (s(v3) = v0) | ~ plus_succeeds(v1, v4, v2) | ~ times_succeeds(v3, v1, v4) | times_succeeds(v0, v1, v2)) % 156.31/109.31 | (6) ! [v0] : ! [v1] : ( ~ (s(v0) = v1) | ~ nat_succeeds(v0) | @=<_succeeds(v0, v1)) % 156.31/109.31 | (7) ! [v0] : ! [v1] : ! [v2] : ( ~ (@+(v1, v0) = v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | @+(v0, v1) = v2) % 156.31/109.31 | (8) ! [v0] : ! [v1] : ! [v2] : (v2 = 0 | ~ times_succeeds(v0, v1, v2) | ? [v3] : ? [v4] : (s(v3) = v0 & plus_succeeds(v1, v4, v2) & times_succeeds(v3, v1, v4))) % 156.31/109.31 | (9) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ plus_succeeds(v0, v1, v3) | ~ plus_succeeds(v0, v1, v2)) % 156.31/109.31 | (10) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v1) = v2) | ~ nat_succeeds(v1) | ~ @<_succeeds(v0, v2) | @<_succeeds(v0, v1)) % 156.31/109.31 | (11) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (@+(v3, v2) = v1) | ~ (@+(v3, v2) = v0)) % 156.31/109.31 | (12) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (s(v4) = v2) | ~ (s(v3) = v0) | ~ plus_terminates(v0, v1, v2) | plus_terminates(v3, v1, v4)) % 156.31/109.31 | (13) ! [v0] : ~ (s(v0) = 0) % 156.31/109.31 | (14) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v0 = 0 | ~ (@*(v0, v2) = v4) | ~ (@*(v0, v1) = v3) | ~ nat_succeeds(v2) | ~ nat_succeeds(v0) | ~ @<_succeeds(v1, v2) | @<_succeeds(v3, v4)) | (all_0_0_0 = all_0_6_6 & ~ (all_0_6_6 = 0) & @*(all_0_6_6, all_0_4_4) = all_0_2_2 & @*(all_0_6_6, all_0_5_5) = all_0_3_3 & s(all_0_1_1) = all_0_6_6 & nat_succeeds(all_0_1_1) & nat_succeeds(all_0_4_4) & @<_succeeds(all_0_5_5, all_0_4_4) & ~ @<_succeeds(all_0_3_3, all_0_2_2) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (all_0_1_1 = 0 | ~ (@*(all_0_1_1, v1) = v3) | ~ (@*(all_0_1_1, v0) = v2) | ~ nat_succeeds(v1) | ~ @<_succeeds(v0, v1) | @<_succeeds(v2, v3))) % 156.34/109.31 | (15) ! [v0] : ! [v1] : ! [v2] : ( ~ (@*(v0, v1) = v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | @*(v1, v0) = v2) % 156.34/109.31 | (16) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (s(v3) = v1) | ~ (s(v2) = v0) | ~ @=<_fails(v0, v1) | @=<_fails(v2, v3)) % 156.34/109.31 | (17) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (@*(v1, v2) = v4) | ~ (@*(v0, v2) = v3) | ~ (@+(v3, v4) = v5) | ~ nat_succeeds(v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v6] : (@*(v6, v2) = v5 & @+(v0, v1) = v6)) % 156.34/109.31 | (18) ? [v0] : ? [v1] : ! [v2] : ( ~ nat_succeeds(v2) | plus_terminates(v0, v1, v2)) % 156.34/109.31 | (19) ! [v0] : ! [v1] : ( ~ @<_succeeds(v0, v1) | ? [v2] : s(v2) = v1) % 156.34/109.31 | (20) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (s(v3) = v1) | ~ (s(v2) = v0) | ~ @<_fails(v0, v1) | @<_fails(v2, v3)) % 156.34/109.31 | (21) ? [v0] : ? [v1] : ? [v2] : (v0 = 0 | times_fails(v0, v1, v2) | ? [v3] : ? [v4] : (s(v3) = v0 & ~ plus_fails(v1, v4, v2) & ~ times_fails(v3, v1, v4))) % 156.34/109.31 | (22) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (@+(v2, v3) = v5) | ~ (@+(v0, v1) = v4) | ~ nat_succeeds(v2) | ~ @<_succeeds(v1, v3) | ~ @=<_succeeds(v0, v2) | @<_succeeds(v4, v5)) % 156.34/109.31 | (23) ? [v0] : ? [v1] : (@<_terminates(v0, v1) | ? [v2] : ? [v3] : (s(v3) = v1 & s(v2) = v0 & ~ @<_terminates(v2, v3))) % 156.34/109.31 | (24) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@*(v2, v3) = v4) | ~ (@+(v0, v1) = v3) | ~ nat_succeeds(v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v5] : ? [v6] : (@*(v2, v1) = v6 & @*(v2, v0) = v5 & @+(v5, v6) = v4)) % 156.34/109.31 | (25) ! [v0] : ! [v1] : (v1 = v0 | ~ (@+(v0, 0) = v1) | ~ nat_succeeds(v0)) % 156.34/109.31 | (26) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@*(v1, v2) = v3) | ~ (@*(v0, v3) = v4) | ~ nat_succeeds(v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v5] : (@*(v5, v2) = v4 & @*(v0, v1) = v5)) % 156.34/109.31 | (27) ! [v0] : ! [v1] : ( ~ @<_succeeds(v0, v1) | ? [v2] : ? [v3] : (s(v2) = v3 & plus_succeeds(v0, v3, v1))) % 156.34/109.31 | (28) ! [v0] : ! [v1] : ( ~ (s(v1) = v0) | @<_succeeds(0, v0)) % 156.34/109.31 | (29) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (@+(v2, v1) = v3) | ~ (s(v0) = v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v4] : (@+(v0, v4) = v3 & s(v1) = v4)) % 156.34/109.31 | (30) ! [v0] : ! [v1] : ( ~ (s(v0) = v1) | ~ nat_succeeds(v0) | @<_succeeds(v0, v1)) % 156.34/109.32 | (31) ! [v0] : ! [v1] : ! [v2] : ( ~ (@+(v0, v1) = v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | @+(v1, v0) = v2) % 156.34/109.32 | (32) ! [v0] : ! [v1] : ! [v2] : ( ~ plus_terminates(v0, v1, v2) | plus_fails(v0, v1, v2) | plus_succeeds(v0, v1, v2)) % 156.34/109.32 | (33) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (@*(v2, v1) = v3) | ~ (s(v0) = v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v4] : (@*(v0, v1) = v4 & @+(v1, v4) = v3)) % 156.34/109.32 | (34) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@+(v1, v2) = v4) | ~ (@+(v0, v2) = v3) | ~ nat_succeeds(v2) | ~ nat_succeeds(v1) | ~ @=<_succeeds(v0, v1) | @=<_succeeds(v3, v4)) % 156.34/109.32 | (35) ! [v0] : ( ~ nat_succeeds(v0) | nat_terminates(v0)) % 156.34/109.32 | (36) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (@+(v0, v2) = v3) | ~ (s(v1) = v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v4] : (@+(v4, v1) = v3 & s(v0) = v4)) % 156.34/109.32 | (37) ! [v0] : ! [v1] : ! [v2] : ( ~ plus_fails(v0, v1, v2) | ~ plus_succeeds(v0, v1, v2)) % 156.34/109.32 | (38) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@+(v1, v2) = v4) | ~ (@+(v0, v2) = v3) | ~ nat_succeeds(v2) | ~ nat_succeeds(v1) | ~ @<_succeeds(v0, v1) | @<_succeeds(v3, v4)) % 156.34/109.32 | (39) nat_succeeds(0) % 156.34/109.32 | (40) ! [v0] : ! [v1] : ( ~ @=<_succeeds(v0, v1) | ? [v2] : plus_succeeds(v0, v2, v1)) % 156.34/109.32 | (41) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (@*(v3, v2) = v1) | ~ (@*(v3, v2) = v0)) % 156.34/109.32 | (42) ? [v0] : ! [v1] : ( ~ nat_succeeds(v1) | @<_terminates(v0, v1)) % 156.34/109.32 | (43) ! [v0] : ! [v1] : ! [v2] : ( ~ (@+(v0, v1) = v2) | ~ nat_succeeds(v0) | @=<_succeeds(v0, v2)) % 156.34/109.32 | (44) ! [v0] : ! [v1] : ! [v2] : ( ~ times_fails(v0, v1, v2) | ~ times_succeeds(v0, v1, v2)) % 156.34/109.32 | (45) ? [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (s(v4) = v1) | ~ times_terminates(v1, v2, v3) | times_terminates(v4, v2, v0)) % 156.34/109.32 | (46) @*(all_0_11_11, all_0_10_10) = all_0_8_8 % 156.34/109.32 | (47) ? [v0] : ? [v1] : ? [v2] : (v2 = 0 | times_fails(v0, v1, v2) | ? [v3] : ? [v4] : (s(v3) = v0 & ~ plus_fails(v1, v4, v2) & ~ times_fails(v3, v1, v4))) % 156.34/109.32 | (48) ! [v0] : ! [v1] : ( ~ @=<_terminates(v0, v1) | @=<_fails(v0, v1) | @=<_succeeds(v0, v1)) % 156.34/109.32 | (49) ! [v0] : ! [v1] : ( ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | @=<_succeeds(v1, v0) | @=<_succeeds(v0, v1)) % 156.34/109.32 | (50) ! [v0] : ! [v1] : ! [v2] : ( ~ @<_succeeds(v1, v2) | ~ @<_succeeds(v0, v1) | @<_succeeds(v0, v2)) % 156.34/109.32 | (51) ! [v0] : (v0 = 0 | ~ nat_succeeds(v0) | @<_succeeds(0, v0)) % 156.34/109.32 | (52) ! [v0] : ! [v1] : ( ~ @<_succeeds(v0, v1) | nat_succeeds(v0)) % 156.34/109.32 | (53) ! [v0] : ! [v1] : (v1 = 0 | ~ (@*(v0, 0) = v1) | ~ nat_succeeds(v0)) % 156.34/109.32 | (54) ! [v0] : ! [v1] : ( ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v2] : times_succeeds(v0, v1, v2)) % 156.34/109.32 | (55) ? [v0] : ? [v1] : ? [v2] : (times_terminates(v0, v1, v2) | ? [v3] : ? [v4] : (s(v3) = v0 & ( ~ times_terminates(v3, v1, v4) | ( ~ plus_terminates(v1, v4, v2) & ~ times_fails(v3, v1, v4))))) % 156.34/109.32 | (56) ! [v0] : ! [v1] : ! [v2] : ( ~ (@+(v0, v1) = v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | nat_succeeds(v2)) % 156.34/109.32 | (57) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (s(v3) = v1) | ~ (s(v2) = v0) | ~ @<_terminates(v0, v1) | @<_terminates(v2, v3)) % 156.34/109.32 | (58) ! [v0] : ! [v1] : ( ~ (s(v0) = v1) | ~ gr(v0) | gr(v1)) % 156.34/109.32 | (59) ! [v0] : ! [v1] : ( ~ (s(v0) = v1) | ~ gr(v1) | gr(v0)) % 156.34/109.32 | (60) ! [v0] : ! [v1] : ( ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ~ @=<_fails(v0, v1) | @=<_succeeds(v1, v0)) % 156.34/109.32 | (61) @*(all_0_11_11, all_0_9_9) = all_0_7_7 % 156.34/109.32 | (62) ! [v0] : ! [v1] : ! [v2] : ( ~ (@+(v0, v1) = v2) | ~ nat_succeeds(v0) | ? [v3] : ? [v4] : (@+(v3, v1) = v4 & s(v2) = v4 & s(v0) = v3)) % 156.34/109.32 | (63) @<_succeeds(all_0_10_10, all_0_9_9) % 156.34/109.32 | (64) ! [v0] : ! [v1] : (v1 = v0 | ~ @=<_succeeds(v1, v0) | ~ @=<_succeeds(v0, v1)) % 156.34/109.32 | (65) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v1) = v2) | ~ (s(v0) = v2)) % 156.34/109.32 | (66) ! [v0] : ( ~ nat_terminates(v0) | nat_fails(v0) | nat_succeeds(v0)) % 156.34/109.32 | (67) ! [v0] : ! [v1] : ! [v2] : ( ~ (s(v1) = v2) | ~ @<_succeeds(v0, v1) | @<_succeeds(v0, v2)) % 156.34/109.32 | (68) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (@*(v2, v1) = v4) | ~ (@*(v2, v0) = v3) | ~ (@+(v3, v4) = v5) | ~ nat_succeeds(v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v6] : (@*(v2, v6) = v5 & @+(v0, v1) = v6)) % 156.34/109.33 | (69) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (@*(v0, v1) = v2) | ~ (@+(v2, v0) = v3) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v4] : (@*(v0, v4) = v3 & s(v1) = v4)) % 156.34/109.33 | (70) ! [v0] : ! [v1] : ( ~ @<_succeeds(v0, v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ((v5 = v1 & v4 = v0 & s(v3) = v1 & s(v2) = v0 & @<_succeeds(v2, v3)) | (v3 = v1 & v0 = 0 & s(v2) = v1))) % 156.34/109.33 | (71) ! [v0] : ( ~ nat_succeeds(v0) | @<_fails(v0, v0)) % 156.34/109.33 | (72) ? [v0] : ! [v1] : ( ~ nat_succeeds(v1) | @<_terminates(v1, v0)) % 156.34/109.33 | (73) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (s(v4) = v2) | ~ (s(v3) = v0) | ~ plus_succeeds(v3, v1, v4) | plus_succeeds(v0, v1, v2)) % 156.34/109.33 | (74) ! [v0] : ! [v1] : ! [v2] : ( ~ times_succeeds(v0, v1, v2) | ~ gr(v1) | gr(v2)) % 156.34/109.33 | (75) ! [v0] : ! [v1] : ( ~ (s(v1) = v0) | ~ nat_terminates(v0) | nat_terminates(v1)) % 156.34/109.33 | (76) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (s(v3) = v1) | ~ (s(v2) = v0) | ~ @=<_succeeds(v2, v3) | @=<_succeeds(v0, v1)) % 156.34/109.33 | (77) ? [v0] : @=<_succeeds(0, v0) % 156.34/109.33 | (78) ? [v0] : ! [v1] : ! [v2] : ( ~ nat_succeeds(v2) | ~ nat_succeeds(v1) | times_terminates(v1, v2, v0)) % 156.34/109.33 | (79) ? [v0] : ! [v1] : ( ~ nat_succeeds(v1) | ? [v2] : plus_succeeds(v1, v0, v2)) % 156.34/109.33 | (80) ! [v0] : ! [v1] : ( ~ @=<_succeeds(v0, v1) | ? [v2] : @+(v0, v2) = v1) % 156.34/109.33 | (81) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@+(v0, v2) = v4) | ~ (@+(v0, v1) = v3) | ~ nat_succeeds(v0) | ~ @=<_succeeds(v1, v2) | @=<_succeeds(v3, v4)) % 156.34/109.33 | (82) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@+(v0, v2) = v4) | ~ (@+(v0, v1) = v3) | ~ nat_succeeds(v0) | ~ @=<_succeeds(v3, v4) | @=<_succeeds(v1, v2)) % 156.34/109.33 | (83) ! [v0] : ! [v1] : ! [v2] : ( ~ @=<_succeeds(v1, v2) | ~ @=<_succeeds(v0, v1) | @=<_succeeds(v0, v2)) % 156.34/109.33 | (84) ! [v0] : ~ plus_fails(0, v0, v0) % 156.34/109.33 | (85) ! [v0] : ! [v1] : ( ~ @=<_succeeds(v0, v1) | nat_succeeds(v0)) % 156.34/109.33 | (86) ! [v0] : ! [v1] : ! [v2] : (v0 = 0 | ~ plus_succeeds(v0, v1, v2) | ? [v3] : ? [v4] : (s(v4) = v2 & s(v3) = v0 & plus_succeeds(v3, v1, v4))) % 156.34/109.33 | (87) ! [v0] : ! [v1] : ( ~ @<_succeeds(v0, v1) | @=<_succeeds(v0, v1)) % 156.34/109.33 | (88) ! [v0] : ! [v1] : ! [v2] : ( ~ times_succeeds(v0, v1, v2) | nat_succeeds(v0)) % 156.34/109.33 | (89) ? [v0] : ? [v1] : ! [v2] : ( ~ nat_succeeds(v2) | plus_terminates(v2, v0, v1)) % 156.34/109.33 | (90) ! [v0] : ! [v1] : (v1 = 0 | ~ (@*(0, v0) = v1) | ~ nat_succeeds(v0)) % 156.34/109.33 | (91) ! [v0] : ! [v1] : ( ~ (s(v1) = v0) | ~ nat_succeeds(v1) | nat_succeeds(v0)) % 156.34/109.33 | (92) ! [v0] : ! [v1] : (v0 = 0 | ~ @=<_succeeds(v0, v1) | ? [v2] : ? [v3] : (s(v3) = v1 & s(v2) = v0 & @=<_succeeds(v2, v3))) % 156.34/109.33 | (93) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (s(v3) = v1) | ~ (s(v2) = v0) | ~ @=<_terminates(v0, v1) | @=<_terminates(v2, v3)) % 156.34/109.33 | (94) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (@*(v0, v2) = v3) | ~ (s(v1) = v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v4] : (@*(v0, v1) = v4 & @+(v4, v0) = v3)) % 156.34/109.33 | (95) ! [v0] : ! [v1] : ! [v2] : ( ~ nat_succeeds(v1) | ~ times_succeeds(v0, v1, v2) | nat_succeeds(v2)) % 156.34/109.33 | (96) ? [v0] : (nat_terminates(v0) | ? [v1] : (s(v1) = v0 & ~ nat_terminates(v1))) % 156.34/109.33 | (97) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v2 = v1 | ~ (@+(v0, v2) = v3) | ~ (@+(v0, v1) = v3) | ~ nat_succeeds(v0)) % 156.34/109.33 | (98) ! [v0] : ( ~ nat_succeeds(v0) | gr(v0)) % 156.34/109.33 | (99) ! [v0] : ( ~ nat_succeeds(v0) | @=<_succeeds(v0, v0)) % 156.34/109.33 | (100) ! [v0] : ! [v1] : ! [v2] : ( ~ nat_succeeds(v1) | ~ plus_succeeds(v0, v1, v2) | nat_succeeds(v2)) % 156.34/109.33 | (101) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (s(v2) = v3) | ~ @<_succeeds(v1, v3) | ~ @<_succeeds(v0, v1) | @<_succeeds(v0, v2)) % 156.34/109.33 | (102) ? [v0] : ? [v1] : ? [v2] : (v0 = 0 | plus_fails(v0, v1, v2) | ? [v3] : ? [v4] : (s(v4) = v2 & s(v3) = v0 & ~ plus_fails(v3, v1, v4))) % 156.34/109.33 | (103) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (@+(v2, v3) = v5) | ~ (@+(v0, v1) = v4) | ~ nat_succeeds(v2) | ~ @<_succeeds(v0, v2) | ~ @=<_succeeds(v1, v3) | @<_succeeds(v4, v5)) % 156.34/109.33 | (104) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@+(v1, v2) = v4) | ~ (@+(v0, v2) = v3) | ~ nat_succeeds(v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ~ @<_succeeds(v3, v4) | @<_succeeds(v0, v1)) % 156.34/109.33 | (105) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (@+(v2, v3) = v5) | ~ (@+(v0, v1) = v4) | ~ nat_succeeds(v2) | ~ @=<_succeeds(v1, v3) | ~ @=<_succeeds(v0, v2) | @=<_succeeds(v4, v5)) % 156.34/109.33 | (106) ! [v0] : ! [v1] : ! [v2] : ( ~ (@*(v0, v1) = v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | nat_succeeds(v2)) % 156.34/109.34 | (107) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@*(v3, v2) = v4) | ~ (@+(v0, v1) = v3) | ~ nat_succeeds(v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v5] : ? [v6] : (@*(v1, v2) = v6 & @*(v0, v2) = v5 & @+(v5, v6) = v4)) % 156.34/109.34 | (108) ? [v0] : plus_succeeds(0, v0, v0) % 156.34/109.34 | (109) ! [v0] : ( ~ nat_succeeds(v0) | ~ @<_succeeds(v0, v0)) % 156.34/109.34 | (110) ? [v0] : (v0 = 0 | nat_fails(v0) | ? [v1] : (s(v1) = v0 & ~ nat_fails(v1))) % 156.34/109.34 | (111) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (s(v3) = v1) | ~ (s(v2) = v0) | ~ @<_succeeds(v2, v3) | @<_succeeds(v0, v1)) % 156.34/109.34 | (112) ! [v0] : ! [v1] : ! [v2] : ( ~ @<_succeeds(v0, v1) | ~ @=<_succeeds(v1, v2) | @<_succeeds(v0, v2)) % 156.34/109.34 | (113) ? [v0] : times_succeeds(0, v0, 0) % 156.34/109.34 | (114) ! [v0] : ! [v1] : ( ~ @=<_fails(v0, v1) | ~ @=<_succeeds(v0, v1)) % 156.34/109.34 | (115) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@*(v3, v2) = v4) | ~ (@*(v0, v1) = v3) | ~ nat_succeeds(v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v5] : (@*(v1, v2) = v5 & @*(v0, v5) = v4)) % 156.34/109.34 | (116) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@*(v1, v2) = v4) | ~ (@*(v0, v2) = v3) | ~ nat_succeeds(v2) | ~ nat_succeeds(v1) | ~ @=<_succeeds(v0, v1) | @=<_succeeds(v3, v4)) % 156.34/109.34 | (117) ! [v0] : ~ times_fails(0, v0, 0) % 156.34/109.34 | (118) ! [v0] : ! [v1] : ! [v2] : ( ~ (@*(v0, v1) = v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | times_succeeds(v0, v1, v2)) % 156.34/109.34 | (119) nat_succeeds(all_0_9_9) % 156.34/109.34 | (120) ? [v0] : ? [v1] : (@=<_terminates(v0, v1) | ? [v2] : ? [v3] : (s(v3) = v1 & s(v2) = v0 & ~ @=<_terminates(v2, v3))) % 156.34/109.34 | (121) ~ (all_0_11_11 = 0) % 156.34/109.34 | (122) ! [v0] : ! [v1] : ! [v2] : (v2 = v1 | ~ plus_succeeds(v0, v1, v2) | ? [v3] : ? [v4] : (s(v4) = v2 & s(v3) = v0 & plus_succeeds(v3, v1, v4))) % 156.34/109.34 | (123) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (@*(v0, v1) = v3) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ~ times_succeeds(v0, v1, v2)) % 156.34/109.34 | (124) ? [v0] : ! [v1] : ( ~ nat_succeeds(v1) | @=<_terminates(v1, v0)) % 156.34/109.34 | (125) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (@+(v0, v2) = v3) | ~ (s(v1) = v2) | ~ nat_succeeds(v0) | @<_succeeds(v0, v3)) % 156.34/109.34 | (126) gr(0) % 156.34/109.34 | (127) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@+(v0, v2) = v4) | ~ (@+(v0, v1) = v3) | ~ nat_succeeds(v0) | ~ @<_succeeds(v1, v2) | @<_succeeds(v3, v4)) % 156.34/109.34 | (128) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@+(v0, v2) = v4) | ~ (@+(v0, v1) = v3) | ~ nat_succeeds(v0) | ~ @<_succeeds(v3, v4) | @<_succeeds(v1, v2)) % 156.34/109.34 | (129) s(0) = all_0_12_12 % 156.34/109.34 | (130) ! [v0] : ! [v1] : ( ~ (s(v0) = v1) | ~ nat_succeeds(v0) | @=<_fails(v1, v0)) % 156.34/109.34 | (131) ! [v0] : ! [v1] : (v1 = v0 | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | @<_succeeds(v1, v0) | @<_succeeds(v0, v1)) % 156.34/109.34 | (132) ! [v0] : ! [v1] : ! [v2] : ( ~ plus_succeeds(v0, v1, v2) | gr(v0)) % 156.34/109.34 | (133) ! [v0] : ! [v1] : (v1 = v0 | ~ (@*(all_0_12_12, v0) = v1) | ~ nat_succeeds(v0)) % 156.34/109.34 | (134) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@+(v3, v2) = v4) | ~ (@+(v0, v1) = v3) | ~ nat_succeeds(v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v5] : (@+(v1, v2) = v5 & @+(v0, v5) = v4)) % 156.34/109.35 | (135) ! [v0] : ! [v1] : (v1 = v0 | ~ nat_succeeds(v1) | ~ @=<_succeeds(v0, v1) | @<_succeeds(v0, v1)) % 156.34/109.35 | (136) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (s(v2) = v1) | ~ (s(v2) = v0)) % 156.34/109.35 | (137) ? [v0] : ? [v1] : (@<_fails(v0, v1) | ? [v2] : ? [v3] : ? [v4] : ? [v5] : ((v5 = v1 & v4 = v0 & s(v3) = v1 & s(v2) = v0 & ~ @<_fails(v2, v3)) | (v3 = v1 & v0 = 0 & s(v2) = v1))) % 156.34/109.35 | (138) ! [v0] : ! [v1] : (v1 = v0 | ~ (@*(v0, all_0_12_12) = v1) | ~ nat_succeeds(v0)) % 156.34/109.35 | (139) ! [v0] : ! [v1] : ! [v2] : ( ~ plus_succeeds(v0, v1, v2) | nat_succeeds(v0)) % 156.34/109.35 | (140) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (@*(v0, v2) = v4) | ~ (@*(v0, v1) = v3) | ~ nat_succeeds(v2) | ~ nat_succeeds(v0) | ~ @=<_succeeds(v1, v2) | @=<_succeeds(v3, v4)) % 156.34/109.35 | (141) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (@+(v2, v1) = v3) | ~ (s(v0) = v2) | ~ nat_succeeds(v0) | ? [v4] : (@+(v0, v1) = v4 & s(v4) = v3)) % 156.34/109.35 | (142) ? [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (s(v4) = v1) | ~ times_fails(v1, v2, v3) | plus_fails(v2, v0, v3) | times_fails(v4, v2, v0)) % 156.34/109.35 | (143) ! [v0] : ! [v1] : ! [v2] : ( ~ times_succeeds(v0, v1, v2) | gr(v0)) % 156.34/109.35 | (144) ~ @<_succeeds(all_0_8_8, all_0_7_7) % 156.34/109.35 | (145) ! [v0] : ! [v1] : ! [v2] : ( ~ @<_succeeds(v1, v2) | ~ @=<_succeeds(v0, v1) | @<_succeeds(v0, v2)) % 156.34/109.35 | (146) ! [v0] : ! [v1] : ! [v2] : ( ~ plus_succeeds(v0, v1, v2) | ~ gr(v1) | gr(v2)) % 156.34/109.35 | (147) ! [v0] : ! [v1] : ! [v2] : ( ~ plus_succeeds(v0, v1, v2) | ~ gr(v2) | gr(v1)) % 156.34/109.35 | (148) ! [v0] : ! [v1] : ! [v2] : (v0 = 0 | ~ times_succeeds(v0, v1, v2) | ? [v3] : ? [v4] : (s(v3) = v0 & plus_succeeds(v1, v4, v2) & times_succeeds(v3, v1, v4))) % 156.34/109.35 | (149) ! [v0] : ! [v1] : ! [v2] : ( ~ times_terminates(v0, v1, v2) | times_fails(v0, v1, v2) | times_succeeds(v0, v1, v2)) % 156.34/109.35 | (150) ! [v0] : ! [v1] : ( ~ @<_fails(v0, v1) | ~ @<_succeeds(v0, v1)) % 156.34/109.35 | (151) ! [v0] : (v0 = 0 | ~ nat_succeeds(v0) | ? [v1] : (s(v1) = v0 & nat_succeeds(v1))) % 156.34/109.35 | (152) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ (@+(v0, v1) = v3) | ~ nat_succeeds(v0) | ~ plus_succeeds(v0, v1, v2)) % 156.34/109.35 | (153) ! [v0] : ~ @=<_fails(0, v0) % 156.34/109.35 | (154) ~ nat_fails(0) % 156.34/109.35 | (155) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ( ~ (s(v4) = v2) | ~ (s(v3) = v0) | ~ plus_fails(v0, v1, v2) | plus_fails(v3, v1, v4)) % 156.34/109.35 | (156) ! [v0] : ! [v1] : ( ~ (s(v1) = v0) | ~ @<_fails(0, v0)) % 156.34/109.35 | (157) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ! [v4] : ! [v5] : ( ~ (@+(v2, v3) = v5) | ~ (@+(v0, v1) = v4) | ~ nat_succeeds(v2) | ~ @<_succeeds(v1, v3) | ~ @<_succeeds(v0, v2) | @<_succeeds(v4, v5)) % 156.34/109.35 | (158) ! [v0] : ( ~ nat_fails(v0) | ~ nat_succeeds(v0)) % 156.34/109.35 | (159) ? [v0] : ! [v1] : ( ~ nat_succeeds(v1) | @=<_terminates(v0, v1)) % 156.34/109.35 | (160) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v3 = v2 | ~ times_succeeds(v0, v1, v3) | ~ times_succeeds(v0, v1, v2)) % 156.34/109.35 | (161) ? [v0] : ? [v1] : (v0 = 0 | @=<_fails(v0, v1) | ? [v2] : ? [v3] : (s(v3) = v1 & s(v2) = v0 & ~ @=<_fails(v2, v3))) % 156.34/109.35 | (162) ! [v0] : ! [v1] : ! [v2] : ( ~ plus_succeeds(v0, v1, v2) | plus_terminates(v0, v1, v2)) % 156.34/109.35 | (163) ! [v0] : ! [v1] : ! [v2] : ( ~ (@+(v0, v1) = v2) | ~ nat_succeeds(v0) | plus_succeeds(v0, v1, v2)) % 156.34/109.35 | (164) ! [v0] : ! [v1] : ( ~ @<_terminates(v0, v1) | @<_fails(v0, v1) | @<_succeeds(v0, v1)) % 156.34/109.35 | (165) ! [v0] : ! [v1] : ( ~ (s(v1) = v0) | ~ nat_fails(v0) | nat_fails(v1)) % 156.34/109.35 | (166) ? [v0] : ? [v1] : ? [v2] : (v2 = v1 | plus_fails(v0, v1, v2) | ? [v3] : ? [v4] : (s(v4) = v2 & s(v3) = v0 & ~ plus_fails(v3, v1, v4))) % 156.34/109.35 | (167) ! [v0] : ! [v1] : (v1 = v0 | ~ (@+(0, v0) = v1)) % 156.34/109.35 | (168) ! [v0] : ! [v1] : ! [v2] : ( ~ (@+(v0, v1) = v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | @=<_succeeds(v1, v2)) % 156.34/109.35 | (169) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (@*(v0, v1) = v2) | ~ (@+(v1, v2) = v3) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ? [v4] : (@*(v4, v1) = v3 & s(v0) = v4)) % 156.34/109.35 | (170) ! [v0] : ! [v1] : ! [v2] : ( ~ nat_succeeds(v2) | ~ plus_succeeds(v0, v1, v2) | nat_succeeds(v1)) % 156.34/109.35 | (171) ! [v0] : ! [v1] : ! [v2] : ( ~ (@+(v1, v0) = v2) | ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | ~ @<_succeeds(0, v1) | @<_succeeds(v0, v2)) % 156.34/109.35 | (172) ? [v0] : ? [v1] : ? [v2] : (plus_terminates(v0, v1, v2) | ? [v3] : ? [v4] : (s(v4) = v2 & s(v3) = v0 & ~ plus_terminates(v3, v1, v4))) % 156.34/109.35 | (173) ! [v0] : ! [v1] : ( ~ nat_succeeds(v1) | ~ nat_succeeds(v0) | @<_succeeds(v0, v1) | @=<_succeeds(v1, v0)) % 156.34/109.35 | (174) ! [v0] : ! [v1] : ( ~ @<_succeeds(v0, v1) | ? [v2] : ? [v3] : (@+(v0, v3) = v1 & s(v2) = v3)) % 156.34/109.35 | (175) nat_succeeds(all_0_11_11) % 156.34/109.35 | % 156.34/109.36 | Instantiating formula (4) with all_0_7_7, all_0_11_11, all_0_9_9 and discharging atoms @*(all_0_11_11, all_0_9_9) = all_0_7_7, nat_succeeds(all_0_9_9), nat_succeeds(all_0_11_11), yields: % 156.34/109.36 | (176) @*(all_0_9_9, all_0_11_11) = all_0_7_7 % 156.34/109.36 | % 156.34/109.36 | Instantiating formula (106) with all_0_7_7, all_0_9_9, all_0_11_11 and discharging atoms @*(all_0_11_11, all_0_9_9) = all_0_7_7, nat_succeeds(all_0_9_9), nat_succeeds(all_0_11_11), yields: % 156.34/109.36 | (177) nat_succeeds(all_0_7_7) % 156.34/109.36 | % 156.34/109.36 | Instantiating formula (151) with all_0_11_11 and discharging atoms nat_succeeds(all_0_11_11), yields: % 156.34/109.36 | (178) all_0_11_11 = 0 | ? [v0] : (s(v0) = all_0_11_11 & nat_succeeds(v0)) % 156.34/109.36 | % 156.34/109.36 | Instantiating formula (52) with all_0_9_9, all_0_10_10 and discharging atoms @<_succeeds(all_0_10_10, all_0_9_9), yields: % 156.34/109.36 | (179) nat_succeeds(all_0_10_10) % 156.34/109.36 | % 156.34/109.36 | Instantiating formula (87) with all_0_9_9, all_0_10_10 and discharging atoms @<_succeeds(all_0_10_10, all_0_9_9), yields: % 156.34/109.36 | (180) @=<_succeeds(all_0_10_10, all_0_9_9) % 156.34/109.36 | % 156.34/109.36 +-Applying beta-rule and splitting (178), into two cases. % 156.34/109.36 |-Branch one: % 156.34/109.36 | (181) all_0_11_11 = 0 % 156.34/109.36 | % 156.34/109.36 | Equations (181) can reduce 121 to: % 156.34/109.36 | (182) $false % 156.34/109.36 | % 156.34/109.36 |-The branch is then unsatisfiable % 156.34/109.36 |-Branch two: % 156.34/109.36 | (121) ~ (all_0_11_11 = 0) % 156.34/109.36 | (184) ? [v0] : (s(v0) = all_0_11_11 & nat_succeeds(v0)) % 156.34/109.36 | % 156.34/109.36 | Instantiating (184) with all_92_0_80 yields: % 156.34/109.36 | (185) s(all_92_0_80) = all_0_11_11 & nat_succeeds(all_92_0_80) % 156.34/109.36 | % 156.34/109.36 | Applying alpha-rule on (185) yields: % 156.34/109.36 | (186) s(all_92_0_80) = all_0_11_11 % 156.34/109.36 | (187) nat_succeeds(all_92_0_80) % 156.34/109.36 | % 156.34/109.36 | Instantiating formula (33) with all_0_7_7, all_0_11_11, all_0_9_9, all_92_0_80 and discharging atoms @*(all_0_11_11, all_0_9_9) = all_0_7_7, s(all_92_0_80) = all_0_11_11, nat_succeeds(all_92_0_80), nat_succeeds(all_0_9_9), yields: % 156.34/109.36 | (188) ? [v0] : (@*(all_92_0_80, all_0_9_9) = v0 & @+(all_0_9_9, v0) = all_0_7_7) % 156.34/109.36 | % 156.34/109.36 | Instantiating formula (94) with all_0_7_7, all_0_11_11, all_92_0_80, all_0_9_9 and discharging atoms @*(all_0_9_9, all_0_11_11) = all_0_7_7, s(all_92_0_80) = all_0_11_11, nat_succeeds(all_92_0_80), nat_succeeds(all_0_9_9), yields: % 156.34/109.36 | (189) ? [v0] : (@*(all_0_9_9, all_92_0_80) = v0 & @+(v0, all_0_9_9) = all_0_7_7) % 156.34/109.36 | % 156.34/109.36 | Instantiating formula (54) with all_0_9_9, all_92_0_80 and discharging atoms nat_succeeds(all_92_0_80), nat_succeeds(all_0_9_9), yields: % 156.34/109.36 | (190) ? [v0] : times_succeeds(all_92_0_80, all_0_9_9, v0) % 156.34/109.36 | % 156.34/109.36 | Instantiating formula (33) with all_0_8_8, all_0_11_11, all_0_10_10, all_92_0_80 and discharging atoms @*(all_0_11_11, all_0_10_10) = all_0_8_8, s(all_92_0_80) = all_0_11_11, nat_succeeds(all_92_0_80), nat_succeeds(all_0_10_10), yields: % 156.34/109.36 | (191) ? [v0] : (@*(all_92_0_80, all_0_10_10) = v0 & @+(all_0_10_10, v0) = all_0_8_8) % 156.34/109.36 | % 156.34/109.36 | Instantiating formula (140) with all_0_7_7, all_0_8_8, all_0_9_9, all_0_10_10, all_0_11_11 and discharging atoms @*(all_0_11_11, all_0_9_9) = all_0_7_7, @*(all_0_11_11, all_0_10_10) = all_0_8_8, nat_succeeds(all_0_9_9), nat_succeeds(all_0_11_11), @=<_succeeds(all_0_10_10, all_0_9_9), yields: % 156.34/109.36 | (192) @=<_succeeds(all_0_8_8, all_0_7_7) % 156.34/109.36 | % 156.34/109.36 | Instantiating (189) with all_108_0_84 yields: % 156.34/109.36 | (193) @*(all_0_9_9, all_92_0_80) = all_108_0_84 & @+(all_108_0_84, all_0_9_9) = all_0_7_7 % 156.34/109.36 | % 156.34/109.36 | Applying alpha-rule on (193) yields: % 156.34/109.36 | (194) @*(all_0_9_9, all_92_0_80) = all_108_0_84 % 156.34/109.36 | (195) @+(all_108_0_84, all_0_9_9) = all_0_7_7 % 156.34/109.36 | % 156.34/109.36 | Instantiating (191) with all_139_0_107 yields: % 156.34/109.36 | (196) @*(all_92_0_80, all_0_10_10) = all_139_0_107 & @+(all_0_10_10, all_139_0_107) = all_0_8_8 % 156.34/109.36 | % 156.34/109.36 | Applying alpha-rule on (196) yields: % 156.34/109.36 | (197) @*(all_92_0_80, all_0_10_10) = all_139_0_107 % 156.34/109.36 | (198) @+(all_0_10_10, all_139_0_107) = all_0_8_8 % 156.34/109.36 | % 156.34/109.36 | Instantiating (190) with all_185_0_131 yields: % 156.34/109.36 | (199) times_succeeds(all_92_0_80, all_0_9_9, all_185_0_131) % 156.34/109.36 | % 156.34/109.36 | Instantiating (188) with all_212_0_148 yields: % 156.34/109.36 | (200) @*(all_92_0_80, all_0_9_9) = all_212_0_148 & @+(all_0_9_9, all_212_0_148) = all_0_7_7 % 156.34/109.36 | % 156.34/109.36 | Applying alpha-rule on (200) yields: % 156.34/109.36 | (201) @*(all_92_0_80, all_0_9_9) = all_212_0_148 % 156.34/109.36 | (202) @+(all_0_9_9, all_212_0_148) = all_0_7_7 % 156.34/109.36 | % 156.34/109.36 | Instantiating formula (123) with all_212_0_148, all_185_0_131, all_0_9_9, all_92_0_80 and discharging atoms @*(all_92_0_80, all_0_9_9) = all_212_0_148, nat_succeeds(all_92_0_80), nat_succeeds(all_0_9_9), times_succeeds(all_92_0_80, all_0_9_9, all_185_0_131), yields: % 156.34/109.36 | (203) all_212_0_148 = all_185_0_131 % 156.34/109.36 | % 156.34/109.36 | From (203) and (201) follows: % 156.34/109.36 | (204) @*(all_92_0_80, all_0_9_9) = all_185_0_131 % 156.34/109.36 | % 156.34/109.36 | From (203) and (202) follows: % 156.34/109.36 | (205) @+(all_0_9_9, all_185_0_131) = all_0_7_7 % 156.34/109.36 | % 156.34/109.36 | Instantiating formula (4) with all_185_0_131, all_92_0_80, all_0_9_9 and discharging atoms @*(all_92_0_80, all_0_9_9) = all_185_0_131, nat_succeeds(all_92_0_80), nat_succeeds(all_0_9_9), yields: % 156.34/109.36 | (206) @*(all_0_9_9, all_92_0_80) = all_185_0_131 % 156.34/109.36 | % 156.34/109.36 | Instantiating formula (140) with all_185_0_131, all_139_0_107, all_0_9_9, all_0_10_10, all_92_0_80 and discharging atoms @*(all_92_0_80, all_0_9_9) = all_185_0_131, @*(all_92_0_80, all_0_10_10) = all_139_0_107, nat_succeeds(all_92_0_80), nat_succeeds(all_0_9_9), @=<_succeeds(all_0_10_10, all_0_9_9), yields: % 156.34/109.36 | (207) @=<_succeeds(all_139_0_107, all_185_0_131) % 156.34/109.37 | % 156.34/109.37 | Instantiating formula (135) with all_0_7_7, all_0_8_8 and discharging atoms nat_succeeds(all_0_7_7), @=<_succeeds(all_0_8_8, all_0_7_7), ~ @<_succeeds(all_0_8_8, all_0_7_7), yields: % 156.34/109.37 | (208) all_0_7_7 = all_0_8_8 % 156.34/109.37 | % 156.34/109.37 | From (208) and (205) follows: % 156.34/109.37 | (209) @+(all_0_9_9, all_185_0_131) = all_0_8_8 % 156.34/109.37 | % 156.34/109.37 | From (208) and (144) follows: % 156.34/109.37 | (210) ~ @<_succeeds(all_0_8_8, all_0_8_8) % 156.34/109.37 | % 156.34/109.37 | Instantiating formula (41) with all_0_9_9, all_92_0_80, all_185_0_131, all_108_0_84 and discharging atoms @*(all_0_9_9, all_92_0_80) = all_185_0_131, @*(all_0_9_9, all_92_0_80) = all_108_0_84, yields: % 156.34/109.37 | (211) all_185_0_131 = all_108_0_84 % 156.34/109.37 | % 156.34/109.37 | From (211) and (209) follows: % 156.34/109.37 | (212) @+(all_0_9_9, all_108_0_84) = all_0_8_8 % 156.34/109.37 | % 156.34/109.37 | From (211) and (207) follows: % 156.34/109.37 | (213) @=<_succeeds(all_139_0_107, all_108_0_84) % 156.34/109.37 | % 156.34/109.37 | Instantiating formula (103) with all_0_8_8, all_0_8_8, all_108_0_84, all_0_9_9, all_139_0_107, all_0_10_10 and discharging atoms @+(all_0_9_9, all_108_0_84) = all_0_8_8, @+(all_0_10_10, all_139_0_107) = all_0_8_8, nat_succeeds(all_0_9_9), @<_succeeds(all_0_10_10, all_0_9_9), @=<_succeeds(all_139_0_107, all_108_0_84), ~ @<_succeeds(all_0_8_8, all_0_8_8), yields: % 156.34/109.37 | (214) $false % 156.34/109.37 | % 156.34/109.37 |-The branch is then unsatisfiable % 156.34/109.37 % SZS output end Proof for theBenchmark % 156.34/109.37 % 156.34/109.37 108774ms %------------------------------------------------------------------------------