%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : COM022+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n004.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 : Fri Jul 15 01:07:53 EDT 2022 % Result : Theorem 18.40s 5.36s % Output : Proof 27.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.14 % Problem : COM022+1 : TPTP v8.1.0. Released v4.0.0. % 0.08/0.14 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.36 % Computer : n004.cluster.edu % 0.13/0.36 % Model : x86_64 x86_64 % 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.36 % Memory : 8042.1875MB % 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.36 % CPULimit : 300 % 0.13/0.36 % WCLimit : 600 % 0.13/0.36 % DateTime : Thu Jun 16 19:55:08 EDT 2022 % 0.13/0.36 % CPUTime : % 0.59/0.62 ____ _ % 0.59/0.62 ___ / __ \_____(_)___ ________ __________ % 0.59/0.62 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.59/0.62 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.59/0.62 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.59/0.62 % 0.59/0.62 A Theorem Prover for First-Order Logic % 0.59/0.62 (ePrincess v.1.0) % 0.59/0.62 % 0.59/0.62 (c) Philipp Rümmer, 2009-2015 % 0.59/0.62 (c) Peter Backeman, 2014-2015 % 0.59/0.62 (contributions by Angelo Brillout, Peter Baumgartner) % 0.59/0.62 Free software under GNU Lesser General Public License (LGPL). % 0.59/0.62 Bug reports to peter@backeman.se % 0.59/0.62 % 0.59/0.62 For more information, visit http://user.uu.se/~petba168/breu/ % 0.59/0.62 % 0.59/0.62 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.68/0.67 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.86/1.04 Prover 0: Preprocessing ... % 2.41/1.26 Prover 0: Constructing countermodel ... % 18.40/5.36 Prover 0: proved (4687ms) % 18.40/5.36 % 18.40/5.36 No countermodel exists, formula is valid % 18.40/5.36 % SZS status Theorem for theBenchmark % 18.40/5.36 % 18.40/5.36 Generating proof ... found it (size 96) % 26.87/7.51 % 26.87/7.51 % SZS output start Proof for theBenchmark % 26.87/7.51 Assumed formulas after preprocessing and simplification: % 26.87/7.51 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (isTerminating0(xR) & isLocallyConfluent0(xR) & sdtmndtasgtdt0(xa, xR, xc) & sdtmndtasgtdt0(xa, xR, xb) & aRewritingSystem0(xR) & aElement0(xc) & aElement0(xb) & aElement0(xa) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ aNormalFormOfIn0(v6, v4, v5) | ~ aReductOfIn0(v7, v6, v5) | ~ aRewritingSystem0(v5) | ~ aElement0(v4)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ isLocallyConfluent0(v4) | ~ aReductOfIn0(v7, v5, v4) | ~ aReductOfIn0(v6, v5, v4) | ~ aRewritingSystem0(v4) | ~ aElement0(v7) | ~ aElement0(v6) | ~ aElement0(v5) | ? [v8] : (sdtmndtasgtdt0(v7, v4, v8) & sdtmndtasgtdt0(v6, v4, v8) & aElement0(v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ isConfluent0(v4) | ~ sdtmndtasgtdt0(v5, v4, v7) | ~ sdtmndtasgtdt0(v5, v4, v6) | ~ aRewritingSystem0(v4) | ~ aElement0(v7) | ~ aElement0(v6) | ~ aElement0(v5) | ? [v8] : (sdtmndtasgtdt0(v7, v4, v8) & sdtmndtasgtdt0(v6, v4, v8) & aElement0(v8))) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ sdtmndtasgtdt0(v6, v5, v7) | ~ sdtmndtasgtdt0(v4, v5, v6) | ~ aRewritingSystem0(v5) | ~ aElement0(v7) | ~ aElement0(v6) | ~ aElement0(v4) | sdtmndtasgtdt0(v4, v5, v7)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ sdtmndtplgtdt0(v7, v5, v6) | ~ aReductOfIn0(v7, v4, v5) | ~ aRewritingSystem0(v5) | ~ aElement0(v7) | ~ aElement0(v6) | ~ aElement0(v4) | sdtmndtplgtdt0(v4, v5, v6)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : ( ~ sdtmndtplgtdt0(v6, v5, v7) | ~ sdtmndtplgtdt0(v4, v5, v6) | ~ aRewritingSystem0(v5) | ~ aElement0(v7) | ~ aElement0(v6) | ~ aElement0(v4) | sdtmndtplgtdt0(v4, v5, v7)) & ! [v4] : ! [v5] : ! [v6] : (v6 = v4 | ~ sdtmndtasgtdt0(v4, v5, v6) | ~ aRewritingSystem0(v5) | ~ aElement0(v6) | ~ aElement0(v4) | sdtmndtplgtdt0(v4, v5, v6)) & ! [v4] : ! [v5] : ! [v6] : ( ~ aNormalFormOfIn0(v6, v4, v5) | ~ aRewritingSystem0(v5) | ~ aElement0(v4) | sdtmndtasgtdt0(v4, v5, v6)) & ! [v4] : ! [v5] : ! [v6] : ( ~ aNormalFormOfIn0(v6, v4, v5) | ~ aRewritingSystem0(v5) | ~ aElement0(v4) | aElement0(v6)) & ! [v4] : ! [v5] : ! [v6] : ( ~ isTerminating0(v4) | ~ sdtmndtplgtdt0(v5, v4, v6) | ~ aRewritingSystem0(v4) | ~ aElement0(v6) | ~ aElement0(v5) | iLess0(v6, v5)) & ! [v4] : ! [v5] : ! [v6] : ( ~ sdtmndtasgtdt0(v4, v5, v6) | ~ aRewritingSystem0(v5) | ~ aElement0(v6) | ~ aElement0(v4) | aNormalFormOfIn0(v6, v4, v5) | ? [v7] : aReductOfIn0(v7, v6, v5)) & ! [v4] : ! [v5] : ! [v6] : ( ~ sdtmndtasgtdt0(v4, xR, v6) | ~ sdtmndtasgtdt0(v4, xR, v5) | ~ iLess0(v4, xa) | ~ aElement0(v6) | ~ aElement0(v5) | ~ aElement0(v4) | ? [v7] : (sdtmndtasgtdt0(v6, xR, v7) & sdtmndtasgtdt0(v5, xR, v7) & aElement0(v7))) & ! [v4] : ! [v5] : ! [v6] : ( ~ sdtmndtplgtdt0(v4, v5, v6) | ~ aRewritingSystem0(v5) | ~ aElement0(v6) | ~ aElement0(v4) | sdtmndtasgtdt0(v4, v5, v6)) & ! [v4] : ! [v5] : ! [v6] : ( ~ sdtmndtplgtdt0(v4, v5, v6) | ~ aRewritingSystem0(v5) | ~ aElement0(v6) | ~ aElement0(v4) | aReductOfIn0(v6, v4, v5) | ? [v7] : (sdtmndtplgtdt0(v7, v5, v6) & aReductOfIn0(v7, v4, v5) & aElement0(v7))) & ! [v4] : ! [v5] : ! [v6] : ( ~ aReductOfIn0(v6, v4, v5) | ~ aRewritingSystem0(v5) | ~ aElement0(v6) | ~ aElement0(v4) | sdtmndtplgtdt0(v4, v5, v6)) & ! [v4] : ! [v5] : ! [v6] : ( ~ aReductOfIn0(v6, v4, v5) | ~ aRewritingSystem0(v5) | ~ aElement0(v4) | aElement0(v6)) & ! [v4] : ! [v5] : ( ~ isTerminating0(v4) | ~ aRewritingSystem0(v4) | ~ aElement0(v5) | ? [v6] : aNormalFormOfIn0(v6, v5, v4)) & ! [v4] : ! [v5] : ( ~ aRewritingSystem0(v5) | ~ aElement0(v4) | sdtmndtasgtdt0(v4, v5, v4)) & ! [v4] : ( ~ sdtmndtasgtdt0(xc, xR, v4) | ~ sdtmndtasgtdt0(xb, xR, v4) | ~ aElement0(v4)) & ! [v4] : ( ~ aRewritingSystem0(v4) | isTerminating0(v4) | ? [v5] : ? [v6] : (sdtmndtplgtdt0(v5, v4, v6) & aElement0(v6) & aElement0(v5) & ~ iLess0(v6, v5))) & ! [v4] : ( ~ aRewritingSystem0(v4) | isLocallyConfluent0(v4) | ? [v5] : ? [v6] : ? [v7] : (aReductOfIn0(v7, v5, v4) & aReductOfIn0(v6, v5, v4) & aElement0(v7) & aElement0(v6) & aElement0(v5) & ! [v8] : ( ~ sdtmndtasgtdt0(v7, v4, v8) | ~ sdtmndtasgtdt0(v6, v4, v8) | ~ aElement0(v8)))) & ! [v4] : ( ~ aRewritingSystem0(v4) | isConfluent0(v4) | ? [v5] : ? [v6] : ? [v7] : (sdtmndtasgtdt0(v5, v4, v7) & sdtmndtasgtdt0(v5, v4, v6) & aElement0(v7) & aElement0(v6) & aElement0(v5) & ! [v8] : ( ~ sdtmndtasgtdt0(v7, v4, v8) | ~ sdtmndtasgtdt0(v6, v4, v8) | ~ aElement0(v8)))) & ( ~ sdtmndtplgtdt0(xa, xR, xc) | ~ sdtmndtplgtdt0(xa, xR, xb) | (aNormalFormOfIn0(v3, v2, xR) & sdtmndtasgtdt0(v1, xR, v2) & sdtmndtasgtdt0(v1, xR, xc) & sdtmndtasgtdt0(v0, xR, v2) & sdtmndtasgtdt0(v0, xR, xb) & sdtmndtasgtdt0(xc, xR, v3) & sdtmndtasgtdt0(xb, xR, v3) & aReductOfIn0(v1, xa, xR) & aReductOfIn0(v0, xa, xR) & aElement0(v2) & aElement0(v1) & aElement0(v0)))) % 26.87/7.53 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3 yields: % 26.87/7.53 | (1) isTerminating0(xR) & isLocallyConfluent0(xR) & sdtmndtasgtdt0(xa, xR, xc) & sdtmndtasgtdt0(xa, xR, xb) & aRewritingSystem0(xR) & aElement0(xc) & aElement0(xb) & aElement0(xa) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ aNormalFormOfIn0(v2, v0, v1) | ~ aReductOfIn0(v3, v2, v1) | ~ aRewritingSystem0(v1) | ~ aElement0(v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ isLocallyConfluent0(v0) | ~ aReductOfIn0(v3, v1, v0) | ~ aReductOfIn0(v2, v1, v0) | ~ aRewritingSystem0(v0) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v1) | ? [v4] : (sdtmndtasgtdt0(v3, v0, v4) & sdtmndtasgtdt0(v2, v0, v4) & aElement0(v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ isConfluent0(v0) | ~ sdtmndtasgtdt0(v1, v0, v3) | ~ sdtmndtasgtdt0(v1, v0, v2) | ~ aRewritingSystem0(v0) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v1) | ? [v4] : (sdtmndtasgtdt0(v3, v0, v4) & sdtmndtasgtdt0(v2, v0, v4) & aElement0(v4))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ sdtmndtasgtdt0(v2, v1, v3) | ~ sdtmndtasgtdt0(v0, v1, v2) | ~ aRewritingSystem0(v1) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v0) | sdtmndtasgtdt0(v0, v1, v3)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ sdtmndtplgtdt0(v3, v1, v2) | ~ aReductOfIn0(v3, v0, v1) | ~ aRewritingSystem0(v1) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v0) | sdtmndtplgtdt0(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ sdtmndtplgtdt0(v2, v1, v3) | ~ sdtmndtplgtdt0(v0, v1, v2) | ~ aRewritingSystem0(v1) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v0) | sdtmndtplgtdt0(v0, v1, v3)) & ! [v0] : ! [v1] : ! [v2] : (v2 = v0 | ~ sdtmndtasgtdt0(v0, v1, v2) | ~ aRewritingSystem0(v1) | ~ aElement0(v2) | ~ aElement0(v0) | sdtmndtplgtdt0(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ aNormalFormOfIn0(v2, v0, v1) | ~ aRewritingSystem0(v1) | ~ aElement0(v0) | sdtmndtasgtdt0(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ aNormalFormOfIn0(v2, v0, v1) | ~ aRewritingSystem0(v1) | ~ aElement0(v0) | aElement0(v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ isTerminating0(v0) | ~ sdtmndtplgtdt0(v1, v0, v2) | ~ aRewritingSystem0(v0) | ~ aElement0(v2) | ~ aElement0(v1) | iLess0(v2, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtasgtdt0(v0, v1, v2) | ~ aRewritingSystem0(v1) | ~ aElement0(v2) | ~ aElement0(v0) | aNormalFormOfIn0(v2, v0, v1) | ? [v3] : aReductOfIn0(v3, v2, v1)) & ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtasgtdt0(v0, xR, v2) | ~ sdtmndtasgtdt0(v0, xR, v1) | ~ iLess0(v0, xa) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : (sdtmndtasgtdt0(v2, xR, v3) & sdtmndtasgtdt0(v1, xR, v3) & aElement0(v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtplgtdt0(v0, v1, v2) | ~ aRewritingSystem0(v1) | ~ aElement0(v2) | ~ aElement0(v0) | sdtmndtasgtdt0(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtplgtdt0(v0, v1, v2) | ~ aRewritingSystem0(v1) | ~ aElement0(v2) | ~ aElement0(v0) | aReductOfIn0(v2, v0, v1) | ? [v3] : (sdtmndtplgtdt0(v3, v1, v2) & aReductOfIn0(v3, v0, v1) & aElement0(v3))) & ! [v0] : ! [v1] : ! [v2] : ( ~ aReductOfIn0(v2, v0, v1) | ~ aRewritingSystem0(v1) | ~ aElement0(v2) | ~ aElement0(v0) | sdtmndtplgtdt0(v0, v1, v2)) & ! [v0] : ! [v1] : ! [v2] : ( ~ aReductOfIn0(v2, v0, v1) | ~ aRewritingSystem0(v1) | ~ aElement0(v0) | aElement0(v2)) & ! [v0] : ! [v1] : ( ~ isTerminating0(v0) | ~ aRewritingSystem0(v0) | ~ aElement0(v1) | ? [v2] : aNormalFormOfIn0(v2, v1, v0)) & ! [v0] : ! [v1] : ( ~ aRewritingSystem0(v1) | ~ aElement0(v0) | sdtmndtasgtdt0(v0, v1, v0)) & ! [v0] : ( ~ sdtmndtasgtdt0(xc, xR, v0) | ~ sdtmndtasgtdt0(xb, xR, v0) | ~ aElement0(v0)) & ! [v0] : ( ~ aRewritingSystem0(v0) | isTerminating0(v0) | ? [v1] : ? [v2] : (sdtmndtplgtdt0(v1, v0, v2) & aElement0(v2) & aElement0(v1) & ~ iLess0(v2, v1))) & ! [v0] : ( ~ aRewritingSystem0(v0) | isLocallyConfluent0(v0) | ? [v1] : ? [v2] : ? [v3] : (aReductOfIn0(v3, v1, v0) & aReductOfIn0(v2, v1, v0) & aElement0(v3) & aElement0(v2) & aElement0(v1) & ! [v4] : ( ~ sdtmndtasgtdt0(v3, v0, v4) | ~ sdtmndtasgtdt0(v2, v0, v4) | ~ aElement0(v4)))) & ! [v0] : ( ~ aRewritingSystem0(v0) | isConfluent0(v0) | ? [v1] : ? [v2] : ? [v3] : (sdtmndtasgtdt0(v1, v0, v3) & sdtmndtasgtdt0(v1, v0, v2) & aElement0(v3) & aElement0(v2) & aElement0(v1) & ! [v4] : ( ~ sdtmndtasgtdt0(v3, v0, v4) | ~ sdtmndtasgtdt0(v2, v0, v4) | ~ aElement0(v4)))) & ( ~ sdtmndtplgtdt0(xa, xR, xc) | ~ sdtmndtplgtdt0(xa, xR, xb) | (aNormalFormOfIn0(all_0_0_0, all_0_1_1, xR) & sdtmndtasgtdt0(all_0_2_2, xR, all_0_1_1) & sdtmndtasgtdt0(all_0_2_2, xR, xc) & sdtmndtasgtdt0(all_0_3_3, xR, all_0_1_1) & sdtmndtasgtdt0(all_0_3_3, xR, xb) & sdtmndtasgtdt0(xc, xR, all_0_0_0) & sdtmndtasgtdt0(xb, xR, all_0_0_0) & aReductOfIn0(all_0_2_2, xa, xR) & aReductOfIn0(all_0_3_3, xa, xR) & aElement0(all_0_1_1) & aElement0(all_0_2_2) & aElement0(all_0_3_3))) % 26.87/7.54 | % 26.87/7.54 | Applying alpha-rule on (1) yields: % 26.87/7.55 | (2) ! [v0] : ! [v1] : ! [v2] : ( ~ aReductOfIn0(v2, v0, v1) | ~ aRewritingSystem0(v1) | ~ aElement0(v2) | ~ aElement0(v0) | sdtmndtplgtdt0(v0, v1, v2)) % 26.87/7.55 | (3) ! [v0] : ( ~ aRewritingSystem0(v0) | isLocallyConfluent0(v0) | ? [v1] : ? [v2] : ? [v3] : (aReductOfIn0(v3, v1, v0) & aReductOfIn0(v2, v1, v0) & aElement0(v3) & aElement0(v2) & aElement0(v1) & ! [v4] : ( ~ sdtmndtasgtdt0(v3, v0, v4) | ~ sdtmndtasgtdt0(v2, v0, v4) | ~ aElement0(v4)))) % 26.87/7.55 | (4) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ sdtmndtplgtdt0(v2, v1, v3) | ~ sdtmndtplgtdt0(v0, v1, v2) | ~ aRewritingSystem0(v1) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v0) | sdtmndtplgtdt0(v0, v1, v3)) % 26.87/7.55 | (5) ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtplgtdt0(v0, v1, v2) | ~ aRewritingSystem0(v1) | ~ aElement0(v2) | ~ aElement0(v0) | aReductOfIn0(v2, v0, v1) | ? [v3] : (sdtmndtplgtdt0(v3, v1, v2) & aReductOfIn0(v3, v0, v1) & aElement0(v3))) % 26.87/7.55 | (6) ! [v0] : ( ~ sdtmndtasgtdt0(xc, xR, v0) | ~ sdtmndtasgtdt0(xb, xR, v0) | ~ aElement0(v0)) % 26.87/7.55 | (7) aElement0(xa) % 26.87/7.55 | (8) ! [v0] : ! [v1] : ! [v2] : ( ~ aNormalFormOfIn0(v2, v0, v1) | ~ aRewritingSystem0(v1) | ~ aElement0(v0) | aElement0(v2)) % 26.87/7.55 | (9) ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtplgtdt0(v0, v1, v2) | ~ aRewritingSystem0(v1) | ~ aElement0(v2) | ~ aElement0(v0) | sdtmndtasgtdt0(v0, v1, v2)) % 26.87/7.55 | (10) ~ sdtmndtplgtdt0(xa, xR, xc) | ~ sdtmndtplgtdt0(xa, xR, xb) | (aNormalFormOfIn0(all_0_0_0, all_0_1_1, xR) & sdtmndtasgtdt0(all_0_2_2, xR, all_0_1_1) & sdtmndtasgtdt0(all_0_2_2, xR, xc) & sdtmndtasgtdt0(all_0_3_3, xR, all_0_1_1) & sdtmndtasgtdt0(all_0_3_3, xR, xb) & sdtmndtasgtdt0(xc, xR, all_0_0_0) & sdtmndtasgtdt0(xb, xR, all_0_0_0) & aReductOfIn0(all_0_2_2, xa, xR) & aReductOfIn0(all_0_3_3, xa, xR) & aElement0(all_0_1_1) & aElement0(all_0_2_2) & aElement0(all_0_3_3)) % 26.87/7.55 | (11) ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtasgtdt0(v0, v1, v2) | ~ aRewritingSystem0(v1) | ~ aElement0(v2) | ~ aElement0(v0) | aNormalFormOfIn0(v2, v0, v1) | ? [v3] : aReductOfIn0(v3, v2, v1)) % 26.87/7.55 | (12) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ aNormalFormOfIn0(v2, v0, v1) | ~ aReductOfIn0(v3, v2, v1) | ~ aRewritingSystem0(v1) | ~ aElement0(v0)) % 26.87/7.55 | (13) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ sdtmndtasgtdt0(v2, v1, v3) | ~ sdtmndtasgtdt0(v0, v1, v2) | ~ aRewritingSystem0(v1) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v0) | sdtmndtasgtdt0(v0, v1, v3)) % 26.87/7.55 | (14) isLocallyConfluent0(xR) % 26.87/7.55 | (15) ! [v0] : ! [v1] : ! [v2] : ( ~ aNormalFormOfIn0(v2, v0, v1) | ~ aRewritingSystem0(v1) | ~ aElement0(v0) | sdtmndtasgtdt0(v0, v1, v2)) % 26.87/7.55 | (16) ! [v0] : ! [v1] : ! [v2] : ( ~ aReductOfIn0(v2, v0, v1) | ~ aRewritingSystem0(v1) | ~ aElement0(v0) | aElement0(v2)) % 26.87/7.55 | (17) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ isConfluent0(v0) | ~ sdtmndtasgtdt0(v1, v0, v3) | ~ sdtmndtasgtdt0(v1, v0, v2) | ~ aRewritingSystem0(v0) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v1) | ? [v4] : (sdtmndtasgtdt0(v3, v0, v4) & sdtmndtasgtdt0(v2, v0, v4) & aElement0(v4))) % 26.87/7.55 | (18) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ isLocallyConfluent0(v0) | ~ aReductOfIn0(v3, v1, v0) | ~ aReductOfIn0(v2, v1, v0) | ~ aRewritingSystem0(v0) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v1) | ? [v4] : (sdtmndtasgtdt0(v3, v0, v4) & sdtmndtasgtdt0(v2, v0, v4) & aElement0(v4))) % 26.87/7.55 | (19) aElement0(xc) % 26.87/7.55 | (20) ! [v0] : ! [v1] : ! [v2] : ( ~ isTerminating0(v0) | ~ sdtmndtplgtdt0(v1, v0, v2) | ~ aRewritingSystem0(v0) | ~ aElement0(v2) | ~ aElement0(v1) | iLess0(v2, v1)) % 26.87/7.55 | (21) aElement0(xb) % 26.87/7.55 | (22) aRewritingSystem0(xR) % 26.87/7.55 | (23) ! [v0] : ( ~ aRewritingSystem0(v0) | isTerminating0(v0) | ? [v1] : ? [v2] : (sdtmndtplgtdt0(v1, v0, v2) & aElement0(v2) & aElement0(v1) & ~ iLess0(v2, v1))) % 26.87/7.55 | (24) ! [v0] : ! [v1] : ( ~ aRewritingSystem0(v1) | ~ aElement0(v0) | sdtmndtasgtdt0(v0, v1, v0)) % 26.87/7.55 | (25) ! [v0] : ( ~ aRewritingSystem0(v0) | isConfluent0(v0) | ? [v1] : ? [v2] : ? [v3] : (sdtmndtasgtdt0(v1, v0, v3) & sdtmndtasgtdt0(v1, v0, v2) & aElement0(v3) & aElement0(v2) & aElement0(v1) & ! [v4] : ( ~ sdtmndtasgtdt0(v3, v0, v4) | ~ sdtmndtasgtdt0(v2, v0, v4) | ~ aElement0(v4)))) % 26.87/7.55 | (26) ! [v0] : ! [v1] : ( ~ isTerminating0(v0) | ~ aRewritingSystem0(v0) | ~ aElement0(v1) | ? [v2] : aNormalFormOfIn0(v2, v1, v0)) % 26.87/7.55 | (27) isTerminating0(xR) % 26.87/7.55 | (28) ! [v0] : ! [v1] : ! [v2] : (v2 = v0 | ~ sdtmndtasgtdt0(v0, v1, v2) | ~ aRewritingSystem0(v1) | ~ aElement0(v2) | ~ aElement0(v0) | sdtmndtplgtdt0(v0, v1, v2)) % 26.87/7.55 | (29) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ sdtmndtplgtdt0(v3, v1, v2) | ~ aReductOfIn0(v3, v0, v1) | ~ aRewritingSystem0(v1) | ~ aElement0(v3) | ~ aElement0(v2) | ~ aElement0(v0) | sdtmndtplgtdt0(v0, v1, v2)) % 26.87/7.55 | (30) sdtmndtasgtdt0(xa, xR, xc) % 26.87/7.55 | (31) sdtmndtasgtdt0(xa, xR, xb) % 26.87/7.55 | (32) ! [v0] : ! [v1] : ! [v2] : ( ~ sdtmndtasgtdt0(v0, xR, v2) | ~ sdtmndtasgtdt0(v0, xR, v1) | ~ iLess0(v0, xa) | ~ aElement0(v2) | ~ aElement0(v1) | ~ aElement0(v0) | ? [v3] : (sdtmndtasgtdt0(v2, xR, v3) & sdtmndtasgtdt0(v1, xR, v3) & aElement0(v3))) % 26.87/7.55 | % 26.87/7.56 | Instantiating formula (26) with xc, xR and discharging atoms isTerminating0(xR), aRewritingSystem0(xR), aElement0(xc), yields: % 26.87/7.56 | (33) ? [v0] : aNormalFormOfIn0(v0, xc, xR) % 26.87/7.56 | % 26.87/7.56 | Instantiating formula (26) with xb, xR and discharging atoms isTerminating0(xR), aRewritingSystem0(xR), aElement0(xb), yields: % 26.87/7.56 | (34) ? [v0] : aNormalFormOfIn0(v0, xb, xR) % 26.87/7.56 | % 26.87/7.56 | Instantiating formula (28) with xc, xR, xa and discharging atoms sdtmndtasgtdt0(xa, xR, xc), aRewritingSystem0(xR), aElement0(xc), aElement0(xa), yields: % 26.87/7.56 | (35) xc = xa | sdtmndtplgtdt0(xa, xR, xc) % 26.87/7.56 | % 26.87/7.56 | Instantiating formula (28) with xb, xR, xa and discharging atoms sdtmndtasgtdt0(xa, xR, xb), aRewritingSystem0(xR), aElement0(xb), aElement0(xa), yields: % 26.87/7.56 | (36) xb = xa | sdtmndtplgtdt0(xa, xR, xb) % 26.87/7.56 | % 26.87/7.56 | Instantiating (34) with all_11_0_5 yields: % 26.87/7.56 | (37) aNormalFormOfIn0(all_11_0_5, xb, xR) % 26.87/7.56 | % 26.87/7.56 | Instantiating (33) with all_13_0_6 yields: % 26.87/7.56 | (38) aNormalFormOfIn0(all_13_0_6, xc, xR) % 26.87/7.56 | % 26.87/7.56 | Instantiating formula (15) with all_13_0_6, xR, xc and discharging atoms aNormalFormOfIn0(all_13_0_6, xc, xR), aRewritingSystem0(xR), aElement0(xc), yields: % 26.87/7.56 | (39) sdtmndtasgtdt0(xc, xR, all_13_0_6) % 26.87/7.56 | % 26.87/7.56 | Instantiating formula (8) with all_13_0_6, xR, xc and discharging atoms aNormalFormOfIn0(all_13_0_6, xc, xR), aRewritingSystem0(xR), aElement0(xc), yields: % 26.87/7.56 | (40) aElement0(all_13_0_6) % 26.87/7.56 | % 26.87/7.56 | Instantiating formula (15) with all_11_0_5, xR, xb and discharging atoms aNormalFormOfIn0(all_11_0_5, xb, xR), aRewritingSystem0(xR), aElement0(xb), yields: % 26.87/7.56 | (41) sdtmndtasgtdt0(xb, xR, all_11_0_5) % 26.87/7.56 | % 26.87/7.56 | Instantiating formula (8) with all_11_0_5, xR, xb and discharging atoms aNormalFormOfIn0(all_11_0_5, xb, xR), aRewritingSystem0(xR), aElement0(xb), yields: % 26.87/7.56 | (42) aElement0(all_11_0_5) % 26.87/7.56 | % 26.87/7.56 | Instantiating formula (13) with all_13_0_6, xc, xR, xa and discharging atoms sdtmndtasgtdt0(xc, xR, all_13_0_6), sdtmndtasgtdt0(xa, xR, xc), aRewritingSystem0(xR), aElement0(all_13_0_6), aElement0(xc), aElement0(xa), yields: % 26.87/7.56 | (43) sdtmndtasgtdt0(xa, xR, all_13_0_6) % 26.87/7.56 | % 26.87/7.56 | Instantiating formula (26) with all_13_0_6, xR and discharging atoms isTerminating0(xR), aRewritingSystem0(xR), aElement0(all_13_0_6), yields: % 26.87/7.56 | (44) ? [v0] : aNormalFormOfIn0(v0, all_13_0_6, xR) % 26.87/7.56 | % 26.87/7.56 | Instantiating formula (13) with all_11_0_5, xb, xR, xa and discharging atoms sdtmndtasgtdt0(xb, xR, all_11_0_5), sdtmndtasgtdt0(xa, xR, xb), aRewritingSystem0(xR), aElement0(all_11_0_5), aElement0(xb), aElement0(xa), yields: % 26.87/7.56 | (45) sdtmndtasgtdt0(xa, xR, all_11_0_5) % 26.87/7.56 | % 26.87/7.56 | Instantiating formula (26) with all_11_0_5, xR and discharging atoms isTerminating0(xR), aRewritingSystem0(xR), aElement0(all_11_0_5), yields: % 26.87/7.56 | (46) ? [v0] : aNormalFormOfIn0(v0, all_11_0_5, xR) % 26.87/7.56 | % 26.87/7.56 | Instantiating (46) with all_27_0_7 yields: % 26.87/7.56 | (47) aNormalFormOfIn0(all_27_0_7, all_11_0_5, xR) % 26.87/7.56 | % 26.87/7.56 | Instantiating (44) with all_31_0_9 yields: % 26.87/7.56 | (48) aNormalFormOfIn0(all_31_0_9, all_13_0_6, xR) % 26.87/7.56 | % 26.87/7.56 | Instantiating formula (15) with all_31_0_9, xR, all_13_0_6 and discharging atoms aNormalFormOfIn0(all_31_0_9, all_13_0_6, xR), aRewritingSystem0(xR), aElement0(all_13_0_6), yields: % 26.87/7.56 | (49) sdtmndtasgtdt0(all_13_0_6, xR, all_31_0_9) % 26.87/7.56 | % 26.87/7.56 | Instantiating formula (8) with all_31_0_9, xR, all_13_0_6 and discharging atoms aNormalFormOfIn0(all_31_0_9, all_13_0_6, xR), aRewritingSystem0(xR), aElement0(all_13_0_6), yields: % 26.87/7.56 | (50) aElement0(all_31_0_9) % 26.87/7.56 | % 26.87/7.56 | Instantiating formula (15) with all_27_0_7, xR, all_11_0_5 and discharging atoms aNormalFormOfIn0(all_27_0_7, all_11_0_5, xR), aRewritingSystem0(xR), aElement0(all_11_0_5), yields: % 26.87/7.56 | (51) sdtmndtasgtdt0(all_11_0_5, xR, all_27_0_7) % 26.87/7.56 | % 26.87/7.56 | Instantiating formula (8) with all_27_0_7, xR, all_11_0_5 and discharging atoms aNormalFormOfIn0(all_27_0_7, all_11_0_5, xR), aRewritingSystem0(xR), aElement0(all_11_0_5), yields: % 26.87/7.56 | (52) aElement0(all_27_0_7) % 26.87/7.56 | % 26.87/7.56 | Instantiating formula (13) with all_31_0_9, all_13_0_6, xR, xc and discharging atoms sdtmndtasgtdt0(all_13_0_6, xR, all_31_0_9), sdtmndtasgtdt0(xc, xR, all_13_0_6), aRewritingSystem0(xR), aElement0(all_31_0_9), aElement0(all_13_0_6), aElement0(xc), yields: % 26.87/7.56 | (53) sdtmndtasgtdt0(xc, xR, all_31_0_9) % 26.87/7.56 | % 26.87/7.56 | Instantiating formula (13) with all_31_0_9, all_13_0_6, xR, xa and discharging atoms sdtmndtasgtdt0(all_13_0_6, xR, all_31_0_9), sdtmndtasgtdt0(xa, xR, all_13_0_6), aRewritingSystem0(xR), aElement0(all_31_0_9), aElement0(all_13_0_6), aElement0(xa), yields: % 26.87/7.56 | (54) sdtmndtasgtdt0(xa, xR, all_31_0_9) % 26.87/7.56 | % 26.87/7.56 | Instantiating formula (26) with all_31_0_9, xR and discharging atoms isTerminating0(xR), aRewritingSystem0(xR), aElement0(all_31_0_9), yields: % 26.87/7.56 | (55) ? [v0] : aNormalFormOfIn0(v0, all_31_0_9, xR) % 26.87/7.56 | % 26.87/7.56 | Instantiating formula (13) with all_27_0_7, all_11_0_5, xR, xb and discharging atoms sdtmndtasgtdt0(all_11_0_5, xR, all_27_0_7), sdtmndtasgtdt0(xb, xR, all_11_0_5), aRewritingSystem0(xR), aElement0(all_27_0_7), aElement0(all_11_0_5), aElement0(xb), yields: % 26.87/7.56 | (56) sdtmndtasgtdt0(xb, xR, all_27_0_7) % 26.87/7.56 | % 26.87/7.56 | Instantiating formula (13) with all_27_0_7, all_11_0_5, xR, xa and discharging atoms sdtmndtasgtdt0(all_11_0_5, xR, all_27_0_7), sdtmndtasgtdt0(xa, xR, all_11_0_5), aRewritingSystem0(xR), aElement0(all_27_0_7), aElement0(all_11_0_5), aElement0(xa), yields: % 26.87/7.56 | (57) sdtmndtasgtdt0(xa, xR, all_27_0_7) % 26.87/7.56 | % 26.87/7.56 | Instantiating formula (26) with all_27_0_7, xR and discharging atoms isTerminating0(xR), aRewritingSystem0(xR), aElement0(all_27_0_7), yields: % 26.87/7.57 | (58) ? [v0] : aNormalFormOfIn0(v0, all_27_0_7, xR) % 26.87/7.57 | % 26.87/7.57 | Instantiating (55) with all_45_0_10 yields: % 26.87/7.57 | (59) aNormalFormOfIn0(all_45_0_10, all_31_0_9, xR) % 26.87/7.57 | % 26.87/7.57 | Instantiating (58) with all_47_0_11 yields: % 26.87/7.57 | (60) aNormalFormOfIn0(all_47_0_11, all_27_0_7, xR) % 26.87/7.57 | % 26.87/7.57 | Instantiating formula (15) with all_47_0_11, xR, all_27_0_7 and discharging atoms aNormalFormOfIn0(all_47_0_11, all_27_0_7, xR), aRewritingSystem0(xR), aElement0(all_27_0_7), yields: % 26.87/7.57 | (61) sdtmndtasgtdt0(all_27_0_7, xR, all_47_0_11) % 26.87/7.57 | % 26.87/7.57 | Instantiating formula (8) with all_47_0_11, xR, all_27_0_7 and discharging atoms aNormalFormOfIn0(all_47_0_11, all_27_0_7, xR), aRewritingSystem0(xR), aElement0(all_27_0_7), yields: % 26.87/7.57 | (62) aElement0(all_47_0_11) % 26.87/7.57 | % 26.87/7.57 | Instantiating formula (15) with all_45_0_10, xR, all_31_0_9 and discharging atoms aNormalFormOfIn0(all_45_0_10, all_31_0_9, xR), aRewritingSystem0(xR), aElement0(all_31_0_9), yields: % 26.87/7.57 | (63) sdtmndtasgtdt0(all_31_0_9, xR, all_45_0_10) % 26.87/7.57 | % 26.87/7.57 | Instantiating formula (8) with all_45_0_10, xR, all_31_0_9 and discharging atoms aNormalFormOfIn0(all_45_0_10, all_31_0_9, xR), aRewritingSystem0(xR), aElement0(all_31_0_9), yields: % 26.87/7.57 | (64) aElement0(all_45_0_10) % 26.87/7.57 | % 26.87/7.57 | Instantiating formula (13) with all_47_0_11, all_27_0_7, xR, xb and discharging atoms sdtmndtasgtdt0(all_27_0_7, xR, all_47_0_11), sdtmndtasgtdt0(xb, xR, all_27_0_7), aRewritingSystem0(xR), aElement0(all_47_0_11), aElement0(all_27_0_7), aElement0(xb), yields: % 26.87/7.57 | (65) sdtmndtasgtdt0(xb, xR, all_47_0_11) % 26.87/7.57 | % 26.87/7.57 | Instantiating formula (13) with all_47_0_11, all_27_0_7, xR, xa and discharging atoms sdtmndtasgtdt0(all_27_0_7, xR, all_47_0_11), sdtmndtasgtdt0(xa, xR, all_27_0_7), aRewritingSystem0(xR), aElement0(all_47_0_11), aElement0(all_27_0_7), aElement0(xa), yields: % 26.87/7.57 | (66) sdtmndtasgtdt0(xa, xR, all_47_0_11) % 26.87/7.57 | % 26.87/7.57 | Instantiating formula (26) with all_47_0_11, xR and discharging atoms isTerminating0(xR), aRewritingSystem0(xR), aElement0(all_47_0_11), yields: % 26.87/7.57 | (67) ? [v0] : aNormalFormOfIn0(v0, all_47_0_11, xR) % 26.87/7.57 | % 26.87/7.57 | Instantiating formula (13) with all_45_0_10, all_31_0_9, xR, xc and discharging atoms sdtmndtasgtdt0(all_31_0_9, xR, all_45_0_10), sdtmndtasgtdt0(xc, xR, all_31_0_9), aRewritingSystem0(xR), aElement0(all_45_0_10), aElement0(all_31_0_9), aElement0(xc), yields: % 26.87/7.57 | (68) sdtmndtasgtdt0(xc, xR, all_45_0_10) % 26.87/7.57 | % 26.87/7.57 | Instantiating formula (13) with all_45_0_10, all_31_0_9, xR, xa and discharging atoms sdtmndtasgtdt0(all_31_0_9, xR, all_45_0_10), sdtmndtasgtdt0(xa, xR, all_31_0_9), aRewritingSystem0(xR), aElement0(all_45_0_10), aElement0(all_31_0_9), aElement0(xa), yields: % 26.87/7.57 | (69) sdtmndtasgtdt0(xa, xR, all_45_0_10) % 26.87/7.57 | % 26.87/7.57 | Instantiating formula (26) with all_45_0_10, xR and discharging atoms isTerminating0(xR), aRewritingSystem0(xR), aElement0(all_45_0_10), yields: % 26.87/7.57 | (70) ? [v0] : aNormalFormOfIn0(v0, all_45_0_10, xR) % 26.87/7.57 | % 26.87/7.57 | Instantiating (67) with all_65_0_14 yields: % 26.87/7.57 | (71) aNormalFormOfIn0(all_65_0_14, all_47_0_11, xR) % 26.87/7.57 | % 26.87/7.57 | Instantiating (70) with all_67_0_15 yields: % 26.87/7.57 | (72) aNormalFormOfIn0(all_67_0_15, all_45_0_10, xR) % 26.87/7.57 | % 26.87/7.57 | Instantiating formula (15) with all_67_0_15, xR, all_45_0_10 and discharging atoms aNormalFormOfIn0(all_67_0_15, all_45_0_10, xR), aRewritingSystem0(xR), aElement0(all_45_0_10), yields: % 26.87/7.57 | (73) sdtmndtasgtdt0(all_45_0_10, xR, all_67_0_15) % 26.87/7.57 | % 26.87/7.57 | Instantiating formula (8) with all_67_0_15, xR, all_45_0_10 and discharging atoms aNormalFormOfIn0(all_67_0_15, all_45_0_10, xR), aRewritingSystem0(xR), aElement0(all_45_0_10), yields: % 26.87/7.57 | (74) aElement0(all_67_0_15) % 26.87/7.57 | % 26.87/7.57 | Instantiating formula (15) with all_65_0_14, xR, all_47_0_11 and discharging atoms aNormalFormOfIn0(all_65_0_14, all_47_0_11, xR), aRewritingSystem0(xR), aElement0(all_47_0_11), yields: % 26.87/7.57 | (75) sdtmndtasgtdt0(all_47_0_11, xR, all_65_0_14) % 26.87/7.57 | % 26.87/7.57 | Instantiating formula (8) with all_65_0_14, xR, all_47_0_11 and discharging atoms aNormalFormOfIn0(all_65_0_14, all_47_0_11, xR), aRewritingSystem0(xR), aElement0(all_47_0_11), yields: % 26.87/7.57 | (76) aElement0(all_65_0_14) % 26.87/7.57 | % 26.87/7.57 | Instantiating formula (13) with all_67_0_15, all_45_0_10, xR, xc and discharging atoms sdtmndtasgtdt0(all_45_0_10, xR, all_67_0_15), sdtmndtasgtdt0(xc, xR, all_45_0_10), aRewritingSystem0(xR), aElement0(all_67_0_15), aElement0(all_45_0_10), aElement0(xc), yields: % 26.87/7.57 | (77) sdtmndtasgtdt0(xc, xR, all_67_0_15) % 26.87/7.57 | % 26.87/7.57 | Instantiating formula (13) with all_67_0_15, all_45_0_10, xR, xa and discharging atoms sdtmndtasgtdt0(all_45_0_10, xR, all_67_0_15), sdtmndtasgtdt0(xa, xR, all_45_0_10), aRewritingSystem0(xR), aElement0(all_67_0_15), aElement0(all_45_0_10), aElement0(xa), yields: % 26.87/7.57 | (78) sdtmndtasgtdt0(xa, xR, all_67_0_15) % 26.87/7.57 | % 26.87/7.57 | Instantiating formula (26) with all_67_0_15, xR and discharging atoms isTerminating0(xR), aRewritingSystem0(xR), aElement0(all_67_0_15), yields: % 26.87/7.57 | (79) ? [v0] : aNormalFormOfIn0(v0, all_67_0_15, xR) % 26.87/7.57 | % 26.87/7.57 | Instantiating formula (13) with all_65_0_14, all_47_0_11, xR, xb and discharging atoms sdtmndtasgtdt0(all_47_0_11, xR, all_65_0_14), sdtmndtasgtdt0(xb, xR, all_47_0_11), aRewritingSystem0(xR), aElement0(all_65_0_14), aElement0(all_47_0_11), aElement0(xb), yields: % 26.87/7.57 | (80) sdtmndtasgtdt0(xb, xR, all_65_0_14) % 26.87/7.57 | % 26.87/7.57 | Instantiating formula (13) with all_65_0_14, all_47_0_11, xR, xa and discharging atoms sdtmndtasgtdt0(all_47_0_11, xR, all_65_0_14), sdtmndtasgtdt0(xa, xR, all_47_0_11), aRewritingSystem0(xR), aElement0(all_65_0_14), aElement0(all_47_0_11), aElement0(xa), yields: % 26.87/7.57 | (81) sdtmndtasgtdt0(xa, xR, all_65_0_14) % 26.87/7.57 | % 26.87/7.57 | Instantiating formula (26) with all_65_0_14, xR and discharging atoms isTerminating0(xR), aRewritingSystem0(xR), aElement0(all_65_0_14), yields: % 26.87/7.57 | (82) ? [v0] : aNormalFormOfIn0(v0, all_65_0_14, xR) % 26.87/7.57 | % 26.87/7.57 | Instantiating (79) with all_81_0_16 yields: % 26.87/7.57 | (83) aNormalFormOfIn0(all_81_0_16, all_67_0_15, xR) % 26.87/7.58 | % 26.87/7.58 | Instantiating (82) with all_85_0_18 yields: % 26.87/7.58 | (84) aNormalFormOfIn0(all_85_0_18, all_65_0_14, xR) % 26.87/7.58 | % 26.87/7.58 | Instantiating formula (15) with all_85_0_18, xR, all_65_0_14 and discharging atoms aNormalFormOfIn0(all_85_0_18, all_65_0_14, xR), aRewritingSystem0(xR), aElement0(all_65_0_14), yields: % 26.87/7.58 | (85) sdtmndtasgtdt0(all_65_0_14, xR, all_85_0_18) % 26.87/7.58 | % 26.87/7.58 | Instantiating formula (8) with all_85_0_18, xR, all_65_0_14 and discharging atoms aNormalFormOfIn0(all_85_0_18, all_65_0_14, xR), aRewritingSystem0(xR), aElement0(all_65_0_14), yields: % 26.87/7.58 | (86) aElement0(all_85_0_18) % 26.87/7.58 | % 26.87/7.58 | Instantiating formula (15) with all_81_0_16, xR, all_67_0_15 and discharging atoms aNormalFormOfIn0(all_81_0_16, all_67_0_15, xR), aRewritingSystem0(xR), aElement0(all_67_0_15), yields: % 26.87/7.58 | (87) sdtmndtasgtdt0(all_67_0_15, xR, all_81_0_16) % 26.87/7.58 | % 26.87/7.58 | Instantiating formula (8) with all_81_0_16, xR, all_67_0_15 and discharging atoms aNormalFormOfIn0(all_81_0_16, all_67_0_15, xR), aRewritingSystem0(xR), aElement0(all_67_0_15), yields: % 26.87/7.58 | (88) aElement0(all_81_0_16) % 26.87/7.58 | % 26.87/7.58 | Instantiating formula (13) with all_85_0_18, all_65_0_14, xR, xb and discharging atoms sdtmndtasgtdt0(all_65_0_14, xR, all_85_0_18), sdtmndtasgtdt0(xb, xR, all_65_0_14), aRewritingSystem0(xR), aElement0(all_85_0_18), aElement0(all_65_0_14), aElement0(xb), yields: % 26.87/7.58 | (89) sdtmndtasgtdt0(xb, xR, all_85_0_18) % 26.87/7.58 | % 26.87/7.58 | Instantiating formula (13) with all_85_0_18, all_65_0_14, xR, xa and discharging atoms sdtmndtasgtdt0(all_65_0_14, xR, all_85_0_18), sdtmndtasgtdt0(xa, xR, all_65_0_14), aRewritingSystem0(xR), aElement0(all_85_0_18), aElement0(all_65_0_14), aElement0(xa), yields: % 26.87/7.58 | (90) sdtmndtasgtdt0(xa, xR, all_85_0_18) % 26.87/7.58 | % 26.87/7.58 | Instantiating formula (26) with all_85_0_18, xR and discharging atoms isTerminating0(xR), aRewritingSystem0(xR), aElement0(all_85_0_18), yields: % 26.87/7.58 | (91) ? [v0] : aNormalFormOfIn0(v0, all_85_0_18, xR) % 26.87/7.58 | % 26.87/7.58 | Instantiating formula (13) with all_81_0_16, all_67_0_15, xR, xc and discharging atoms sdtmndtasgtdt0(all_67_0_15, xR, all_81_0_16), sdtmndtasgtdt0(xc, xR, all_67_0_15), aRewritingSystem0(xR), aElement0(all_81_0_16), aElement0(all_67_0_15), aElement0(xc), yields: % 26.87/7.58 | (92) sdtmndtasgtdt0(xc, xR, all_81_0_16) % 26.87/7.58 | % 26.87/7.58 | Instantiating formula (13) with all_81_0_16, all_67_0_15, xR, xa and discharging atoms sdtmndtasgtdt0(all_67_0_15, xR, all_81_0_16), sdtmndtasgtdt0(xa, xR, all_67_0_15), aRewritingSystem0(xR), aElement0(all_81_0_16), aElement0(all_67_0_15), aElement0(xa), yields: % 26.87/7.58 | (93) sdtmndtasgtdt0(xa, xR, all_81_0_16) % 26.87/7.58 | % 26.87/7.58 | Instantiating formula (26) with all_81_0_16, xR and discharging atoms isTerminating0(xR), aRewritingSystem0(xR), aElement0(all_81_0_16), yields: % 26.87/7.58 | (94) ? [v0] : aNormalFormOfIn0(v0, all_81_0_16, xR) % 26.87/7.58 | % 26.87/7.58 | Instantiating (94) with all_101_0_20 yields: % 26.87/7.58 | (95) aNormalFormOfIn0(all_101_0_20, all_81_0_16, xR) % 26.87/7.58 | % 26.87/7.58 | Instantiating (91) with all_103_0_21 yields: % 26.87/7.58 | (96) aNormalFormOfIn0(all_103_0_21, all_85_0_18, xR) % 26.87/7.58 | % 26.87/7.58 +-Applying beta-rule and splitting (10), into two cases. % 26.87/7.58 |-Branch one: % 26.87/7.58 | (97) ~ sdtmndtplgtdt0(xa, xR, xc) % 26.87/7.58 | % 26.87/7.58 +-Applying beta-rule and splitting (35), into two cases. % 26.87/7.58 |-Branch one: % 26.87/7.58 | (98) sdtmndtplgtdt0(xa, xR, xc) % 26.87/7.58 | % 26.87/7.58 | Using (98) and (97) yields: % 26.87/7.58 | (99) $false % 26.87/7.58 | % 26.87/7.58 |-The branch is then unsatisfiable % 26.87/7.58 |-Branch two: % 26.87/7.58 | (97) ~ sdtmndtplgtdt0(xa, xR, xc) % 26.87/7.58 | (101) xc = xa % 26.87/7.58 | % 26.87/7.58 | From (101) and (19) follows: % 26.87/7.58 | (7) aElement0(xa) % 26.87/7.58 | % 26.87/7.58 | Instantiating formula (15) with all_103_0_21, xR, all_85_0_18 and discharging atoms aNormalFormOfIn0(all_103_0_21, all_85_0_18, xR), aRewritingSystem0(xR), aElement0(all_85_0_18), yields: % 26.87/7.58 | (103) sdtmndtasgtdt0(all_85_0_18, xR, all_103_0_21) % 26.87/7.58 | % 26.87/7.58 | Instantiating formula (8) with all_103_0_21, xR, all_85_0_18 and discharging atoms aNormalFormOfIn0(all_103_0_21, all_85_0_18, xR), aRewritingSystem0(xR), aElement0(all_85_0_18), yields: % 26.87/7.58 | (104) aElement0(all_103_0_21) % 26.87/7.58 | % 26.87/7.58 | Instantiating formula (13) with all_103_0_21, all_85_0_18, xR, xb and discharging atoms sdtmndtasgtdt0(all_85_0_18, xR, all_103_0_21), sdtmndtasgtdt0(xb, xR, all_85_0_18), aRewritingSystem0(xR), aElement0(all_103_0_21), aElement0(all_85_0_18), aElement0(xb), yields: % 26.87/7.58 | (105) sdtmndtasgtdt0(xb, xR, all_103_0_21) % 26.87/7.58 | % 26.87/7.58 | Instantiating formula (13) with all_103_0_21, all_85_0_18, xR, xa and discharging atoms sdtmndtasgtdt0(all_85_0_18, xR, all_103_0_21), sdtmndtasgtdt0(xa, xR, all_85_0_18), aRewritingSystem0(xR), aElement0(all_103_0_21), aElement0(all_85_0_18), aElement0(xa), yields: % 26.87/7.58 | (106) sdtmndtasgtdt0(xa, xR, all_103_0_21) % 26.87/7.58 | % 26.87/7.58 | Instantiating formula (6) with all_103_0_21 and discharging atoms sdtmndtasgtdt0(xb, xR, all_103_0_21), aElement0(all_103_0_21), yields: % 26.87/7.58 | (107) ~ sdtmndtasgtdt0(xc, xR, all_103_0_21) % 26.87/7.58 | % 26.87/7.58 | From (101) and (107) follows: % 26.87/7.59 | (108) ~ sdtmndtasgtdt0(xa, xR, all_103_0_21) % 26.87/7.59 | % 26.87/7.59 | Using (106) and (108) yields: % 26.87/7.59 | (99) $false % 26.87/7.59 | % 26.87/7.59 |-The branch is then unsatisfiable % 26.87/7.59 |-Branch two: % 26.87/7.59 | (98) sdtmndtplgtdt0(xa, xR, xc) % 26.87/7.59 | (111) ~ sdtmndtplgtdt0(xa, xR, xb) | (aNormalFormOfIn0(all_0_0_0, all_0_1_1, xR) & sdtmndtasgtdt0(all_0_2_2, xR, all_0_1_1) & sdtmndtasgtdt0(all_0_2_2, xR, xc) & sdtmndtasgtdt0(all_0_3_3, xR, all_0_1_1) & sdtmndtasgtdt0(all_0_3_3, xR, xb) & sdtmndtasgtdt0(xc, xR, all_0_0_0) & sdtmndtasgtdt0(xb, xR, all_0_0_0) & aReductOfIn0(all_0_2_2, xa, xR) & aReductOfIn0(all_0_3_3, xa, xR) & aElement0(all_0_1_1) & aElement0(all_0_2_2) & aElement0(all_0_3_3)) % 26.87/7.59 | % 26.87/7.59 | Instantiating formula (15) with all_101_0_20, xR, all_81_0_16 and discharging atoms aNormalFormOfIn0(all_101_0_20, all_81_0_16, xR), aRewritingSystem0(xR), aElement0(all_81_0_16), yields: % 26.87/7.59 | (112) sdtmndtasgtdt0(all_81_0_16, xR, all_101_0_20) % 26.87/7.59 | % 26.87/7.59 | Instantiating formula (8) with all_101_0_20, xR, all_81_0_16 and discharging atoms aNormalFormOfIn0(all_101_0_20, all_81_0_16, xR), aRewritingSystem0(xR), aElement0(all_81_0_16), yields: % 26.87/7.59 | (113) aElement0(all_101_0_20) % 26.87/7.59 | % 26.87/7.59 +-Applying beta-rule and splitting (36), into two cases. % 26.87/7.59 |-Branch one: % 26.87/7.59 | (114) sdtmndtplgtdt0(xa, xR, xb) % 26.87/7.59 | % 26.87/7.59 +-Applying beta-rule and splitting (111), into two cases. % 26.87/7.59 |-Branch one: % 26.87/7.59 | (115) ~ sdtmndtplgtdt0(xa, xR, xb) % 26.87/7.59 | % 26.87/7.59 | Using (114) and (115) yields: % 26.87/7.59 | (99) $false % 26.87/7.59 | % 26.87/7.59 |-The branch is then unsatisfiable % 26.87/7.59 |-Branch two: % 26.87/7.59 | (114) sdtmndtplgtdt0(xa, xR, xb) % 26.87/7.59 | (118) aNormalFormOfIn0(all_0_0_0, all_0_1_1, xR) & sdtmndtasgtdt0(all_0_2_2, xR, all_0_1_1) & sdtmndtasgtdt0(all_0_2_2, xR, xc) & sdtmndtasgtdt0(all_0_3_3, xR, all_0_1_1) & sdtmndtasgtdt0(all_0_3_3, xR, xb) & sdtmndtasgtdt0(xc, xR, all_0_0_0) & sdtmndtasgtdt0(xb, xR, all_0_0_0) & aReductOfIn0(all_0_2_2, xa, xR) & aReductOfIn0(all_0_3_3, xa, xR) & aElement0(all_0_1_1) & aElement0(all_0_2_2) & aElement0(all_0_3_3) % 26.87/7.59 | % 26.87/7.59 | Applying alpha-rule on (118) yields: % 26.87/7.59 | (119) sdtmndtasgtdt0(xc, xR, all_0_0_0) % 26.87/7.59 | (120) aElement0(all_0_2_2) % 26.87/7.59 | (121) aElement0(all_0_3_3) % 26.87/7.59 | (122) sdtmndtasgtdt0(xb, xR, all_0_0_0) % 26.87/7.59 | (123) sdtmndtasgtdt0(all_0_2_2, xR, all_0_1_1) % 26.87/7.59 | (124) sdtmndtasgtdt0(all_0_3_3, xR, xb) % 26.87/7.59 | (125) aNormalFormOfIn0(all_0_0_0, all_0_1_1, xR) % 26.87/7.59 | (126) sdtmndtasgtdt0(all_0_3_3, xR, all_0_1_1) % 26.87/7.59 | (127) aElement0(all_0_1_1) % 26.87/7.59 | (128) aReductOfIn0(all_0_2_2, xa, xR) % 26.87/7.59 | (129) aReductOfIn0(all_0_3_3, xa, xR) % 26.87/7.59 | (130) sdtmndtasgtdt0(all_0_2_2, xR, xc) % 26.87/7.59 | % 26.87/7.59 | Instantiating formula (8) with all_0_0_0, xR, all_0_1_1 and discharging atoms aNormalFormOfIn0(all_0_0_0, all_0_1_1, xR), aRewritingSystem0(xR), aElement0(all_0_1_1), yields: % 26.87/7.59 | (131) aElement0(all_0_0_0) % 26.87/7.59 | % 26.87/7.59 | Instantiating formula (6) with all_0_0_0 and discharging atoms sdtmndtasgtdt0(xc, xR, all_0_0_0), sdtmndtasgtdt0(xb, xR, all_0_0_0), aElement0(all_0_0_0), yields: % 26.87/7.59 | (99) $false % 26.87/7.59 | % 26.87/7.59 |-The branch is then unsatisfiable % 26.87/7.59 |-Branch two: % 26.87/7.59 | (115) ~ sdtmndtplgtdt0(xa, xR, xb) % 26.87/7.59 | (134) xb = xa % 26.87/7.59 | % 26.87/7.59 | From (134) and (21) follows: % 26.87/7.59 | (7) aElement0(xa) % 27.37/7.59 | % 27.37/7.59 | Instantiating formula (13) with all_101_0_20, all_81_0_16, xR, xc and discharging atoms sdtmndtasgtdt0(all_81_0_16, xR, all_101_0_20), sdtmndtasgtdt0(xc, xR, all_81_0_16), aRewritingSystem0(xR), aElement0(all_101_0_20), aElement0(all_81_0_16), aElement0(xc), yields: % 27.37/7.59 | (136) sdtmndtasgtdt0(xc, xR, all_101_0_20) % 27.37/7.59 | % 27.37/7.59 | Instantiating formula (13) with all_101_0_20, all_81_0_16, xR, xa and discharging atoms sdtmndtasgtdt0(all_81_0_16, xR, all_101_0_20), sdtmndtasgtdt0(xa, xR, all_81_0_16), aRewritingSystem0(xR), aElement0(all_101_0_20), aElement0(all_81_0_16), aElement0(xa), yields: % 27.37/7.59 | (137) sdtmndtasgtdt0(xa, xR, all_101_0_20) % 27.37/7.59 | % 27.37/7.59 | Instantiating formula (6) with all_101_0_20 and discharging atoms sdtmndtasgtdt0(xc, xR, all_101_0_20), aElement0(all_101_0_20), yields: % 27.37/7.59 | (138) ~ sdtmndtasgtdt0(xb, xR, all_101_0_20) % 27.37/7.59 | % 27.37/7.59 | From (134) and (138) follows: % 27.37/7.59 | (139) ~ sdtmndtasgtdt0(xa, xR, all_101_0_20) % 27.37/7.59 | % 27.37/7.59 | Using (137) and (139) yields: % 27.37/7.59 | (99) $false % 27.37/7.59 | % 27.37/7.59 |-The branch is then unsatisfiable % 27.37/7.59 % SZS output end Proof for theBenchmark % 27.37/7.59 % 27.37/7.59 6965ms %------------------------------------------------------------------------------