%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SYN319+1 : TPTP v8.1.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n018.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 : Thu Jul 21 05:01:19 EDT 2022 % Result : Theorem 3.55s 1.58s % Output : Proof 7.58s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : SYN319+1 : TPTP v8.1.0. Released v2.0.0. % 0.04/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.34 % Computer : n018.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 : 600 % 0.12/0.34 % DateTime : Mon Jul 11 21:30:14 EDT 2022 % 0.12/0.34 % CPUTime : % 0.53/0.62 ____ _ % 0.53/0.62 ___ / __ \_____(_)___ ________ __________ % 0.53/0.62 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.53/0.62 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.53/0.62 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.53/0.62 % 0.53/0.62 A Theorem Prover for First-Order Logic % 0.66/0.63 (ePrincess v.1.0) % 0.66/0.63 % 0.66/0.63 (c) Philipp Rümmer, 2009-2015 % 0.66/0.63 (c) Peter Backeman, 2014-2015 % 0.66/0.63 (contributions by Angelo Brillout, Peter Baumgartner) % 0.66/0.63 Free software under GNU Lesser General Public License (LGPL). % 0.66/0.63 Bug reports to peter@backeman.se % 0.66/0.63 % 0.66/0.63 For more information, visit http://user.uu.se/~petba168/breu/ % 0.66/0.63 % 0.66/0.63 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.73/0.69 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.36/0.94 Prover 0: Preprocessing ... % 1.44/1.00 Prover 0: Warning: ignoring some quantifiers % 1.44/1.02 Prover 0: Constructing countermodel ... % 1.69/1.11 Prover 0: gave up % 1.69/1.11 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 1.69/1.13 Prover 1: Preprocessing ... % 2.13/1.19 Prover 1: Constructing countermodel ... % 2.13/1.19 Prover 1: gave up % 2.13/1.20 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 2.13/1.21 Prover 2: Preprocessing ... % 2.42/1.28 Prover 2: Warning: ignoring some quantifiers % 2.42/1.29 Prover 2: Constructing countermodel ... % 2.42/1.31 Prover 2: gave up % 2.42/1.31 Prover 3: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 2.66/1.32 Prover 3: Preprocessing ... % 2.66/1.33 Prover 3: Warning: ignoring some quantifiers % 2.66/1.33 Prover 3: Constructing countermodel ... % 2.66/1.35 Prover 3: gave up % 2.66/1.35 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=complete % 2.66/1.35 Prover 4: Preprocessing ... % 2.83/1.40 Prover 4: Warning: ignoring some quantifiers % 2.83/1.41 Prover 4: Constructing countermodel ... % 3.55/1.58 Prover 4: proved (232ms) % 3.55/1.58 % 3.55/1.58 No countermodel exists, formula is valid % 3.55/1.58 % SZS status Theorem for theBenchmark % 3.55/1.58 % 3.55/1.58 Generating proof ... Warning: ignoring some quantifiers % 7.11/2.39 found it (size 87) % 7.11/2.39 % 7.11/2.39 % SZS output start Proof for theBenchmark % 7.11/2.39 Assumed formulas after preprocessing and simplification: % 7.11/2.39 | (0) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (big_h(v1) = v3) | ~ (big_h(v0) = v2) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ( ~ (v11 = 0) & big_h(v8) = v11 & big_f(v8) = v12 & big_f(v7) = v10 & big_f(v1) = v4 & big_f(v0) = v6 & big_g(v8) = v13 & big_g(v7) = v9 & big_g(v0) = v5 & (v2 = 0 | ( ~ (v6 = 0) & ~ (v5 = 0))) & ((v5 = 0 & ~ (v10 = 0)) | (v4 = 0 & ~ (v9 = 0))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (big_h(v1) = v3) | ~ (big_f(v0) = v2) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ( ~ (v11 = 0) & big_h(v8) = v11 & big_h(v0) = v6 & big_f(v8) = v12 & big_f(v7) = v10 & big_f(v1) = v4 & big_g(v8) = v13 & big_g(v7) = v9 & big_g(v0) = v5 & (v6 = 0 | ( ~ (v5 = 0) & ~ (v2 = 0))) & ((v5 = 0 & ~ (v10 = 0)) | (v4 = 0 & ~ (v9 = 0))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (big_h(v1) = v3) | ~ (big_g(v0) = v2) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ( ~ (v11 = 0) & big_h(v8) = v11 & big_h(v0) = v6 & big_f(v8) = v12 & big_f(v7) = v10 & big_f(v1) = v4 & big_f(v0) = v5 & big_g(v8) = v13 & big_g(v7) = v9 & (v6 = 0 | ( ~ (v5 = 0) & ~ (v2 = 0))) & ((v4 = 0 & ~ (v9 = 0)) | (v2 = 0 & ~ (v10 = 0))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (big_h(v0) = v3) | ~ (big_f(v1) = v2) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ( ~ (v11 = 0) & big_h(v8) = v11 & big_h(v1) = v6 & big_f(v8) = v12 & big_f(v7) = v10 & big_f(v0) = v5 & big_g(v8) = v13 & big_g(v7) = v9 & big_g(v0) = v4 & (v3 = 0 | ( ~ (v5 = 0) & ~ (v4 = 0))) & ((v4 = 0 & ~ (v10 = 0)) | (v2 = 0 & ~ (v9 = 0))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (big_f(v1) = v2) | ~ (big_f(v0) = v3) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ( ~ (v11 = 0) & big_h(v8) = v11 & big_h(v1) = v6 & big_h(v0) = v5 & big_f(v8) = v12 & big_f(v7) = v10 & big_g(v8) = v13 & big_g(v7) = v9 & big_g(v0) = v4 & (v5 = 0 | ( ~ (v4 = 0) & ~ (v3 = 0))) & ((v4 = 0 & ~ (v10 = 0)) | (v2 = 0 & ~ (v9 = 0))))) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (big_f(v1) = v2) | ~ (big_g(v0) = v3) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ( ~ (v11 = 0) & big_h(v8) = v11 & big_h(v1) = v6 & big_h(v0) = v5 & big_f(v8) = v12 & big_f(v7) = v10 & big_f(v0) = v4 & big_g(v8) = v13 & big_g(v7) = v9 & (v5 = 0 | ( ~ (v4 = 0) & ~ (v3 = 0))) & ((v3 = 0 & ~ (v10 = 0)) | (v2 = 0 & ~ (v9 = 0))))) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (big_h(v2) = v1) | ~ (big_h(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (big_f(v2) = v1) | ~ (big_f(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (big_g(v2) = v1) | ~ (big_g(v2) = v0)) & ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ( ~ (v11 = 0) & big_h(v8) = v11 & big_h(v1) = v6 & big_h(v0) = v5 & big_f(v8) = v12 & big_f(v7) = v10 & big_f(v1) = v2 & big_f(v0) = v4 & big_g(v8) = v13 & big_g(v7) = v9 & big_g(v0) = v3 & (v5 = 0 | ( ~ (v4 = 0) & ~ (v3 = 0))) & ((v3 = 0 & ~ (v10 = 0)) | (v2 = 0 & ~ (v9 = 0)))) % 7.11/2.42 | Applying alpha-rule on (0) yields: % 7.11/2.42 | (1) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (big_h(v1) = v3) | ~ (big_h(v0) = v2) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ( ~ (v11 = 0) & big_h(v8) = v11 & big_f(v8) = v12 & big_f(v7) = v10 & big_f(v1) = v4 & big_f(v0) = v6 & big_g(v8) = v13 & big_g(v7) = v9 & big_g(v0) = v5 & (v2 = 0 | ( ~ (v6 = 0) & ~ (v5 = 0))) & ((v5 = 0 & ~ (v10 = 0)) | (v4 = 0 & ~ (v9 = 0))))) % 7.11/2.42 | (2) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ( ~ (v11 = 0) & big_h(v8) = v11 & big_h(v1) = v6 & big_h(v0) = v5 & big_f(v8) = v12 & big_f(v7) = v10 & big_f(v1) = v2 & big_f(v0) = v4 & big_g(v8) = v13 & big_g(v7) = v9 & big_g(v0) = v3 & (v5 = 0 | ( ~ (v4 = 0) & ~ (v3 = 0))) & ((v3 = 0 & ~ (v10 = 0)) | (v2 = 0 & ~ (v9 = 0)))) % 7.11/2.42 | (3) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (big_h(v1) = v3) | ~ (big_f(v0) = v2) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ( ~ (v11 = 0) & big_h(v8) = v11 & big_h(v0) = v6 & big_f(v8) = v12 & big_f(v7) = v10 & big_f(v1) = v4 & big_g(v8) = v13 & big_g(v7) = v9 & big_g(v0) = v5 & (v6 = 0 | ( ~ (v5 = 0) & ~ (v2 = 0))) & ((v5 = 0 & ~ (v10 = 0)) | (v4 = 0 & ~ (v9 = 0))))) % 7.11/2.43 | (4) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (big_f(v1) = v2) | ~ (big_f(v0) = v3) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ( ~ (v11 = 0) & big_h(v8) = v11 & big_h(v1) = v6 & big_h(v0) = v5 & big_f(v8) = v12 & big_f(v7) = v10 & big_g(v8) = v13 & big_g(v7) = v9 & big_g(v0) = v4 & (v5 = 0 | ( ~ (v4 = 0) & ~ (v3 = 0))) & ((v4 = 0 & ~ (v10 = 0)) | (v2 = 0 & ~ (v9 = 0))))) % 7.11/2.43 | (5) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (big_h(v0) = v3) | ~ (big_f(v1) = v2) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ( ~ (v11 = 0) & big_h(v8) = v11 & big_h(v1) = v6 & big_f(v8) = v12 & big_f(v7) = v10 & big_f(v0) = v5 & big_g(v8) = v13 & big_g(v7) = v9 & big_g(v0) = v4 & (v3 = 0 | ( ~ (v5 = 0) & ~ (v4 = 0))) & ((v4 = 0 & ~ (v10 = 0)) | (v2 = 0 & ~ (v9 = 0))))) % 7.11/2.43 | (6) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (big_h(v2) = v1) | ~ (big_h(v2) = v0)) % 7.11/2.43 | (7) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (big_f(v1) = v2) | ~ (big_g(v0) = v3) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ( ~ (v11 = 0) & big_h(v8) = v11 & big_h(v1) = v6 & big_h(v0) = v5 & big_f(v8) = v12 & big_f(v7) = v10 & big_f(v0) = v4 & big_g(v8) = v13 & big_g(v7) = v9 & (v5 = 0 | ( ~ (v4 = 0) & ~ (v3 = 0))) & ((v3 = 0 & ~ (v10 = 0)) | (v2 = 0 & ~ (v9 = 0))))) % 7.11/2.43 | (8) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (big_f(v2) = v1) | ~ (big_f(v2) = v0)) % 7.11/2.43 | (9) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ (big_h(v1) = v3) | ~ (big_g(v0) = v2) | ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ( ~ (v11 = 0) & big_h(v8) = v11 & big_h(v0) = v6 & big_f(v8) = v12 & big_f(v7) = v10 & big_f(v1) = v4 & big_f(v0) = v5 & big_g(v8) = v13 & big_g(v7) = v9 & (v6 = 0 | ( ~ (v5 = 0) & ~ (v2 = 0))) & ((v4 = 0 & ~ (v9 = 0)) | (v2 = 0 & ~ (v10 = 0))))) % 7.11/2.43 | (10) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (big_g(v2) = v1) | ~ (big_g(v2) = v0)) % 7.11/2.43 | % 7.11/2.43 | Instantiating (2) with all_1_0_0, all_1_1_1, all_1_2_2, all_1_3_3, all_1_4_4, all_1_5_5, all_1_6_6, all_1_7_7, all_1_8_8, all_1_9_9, all_1_10_10, all_1_11_11, all_1_12_12, all_1_13_13 yields: % 7.11/2.43 | (11) ~ (all_1_2_2 = 0) & big_h(all_1_5_5) = all_1_2_2 & big_h(all_1_12_12) = all_1_7_7 & big_h(all_1_13_13) = all_1_8_8 & big_f(all_1_5_5) = all_1_1_1 & big_f(all_1_6_6) = all_1_3_3 & big_f(all_1_12_12) = all_1_11_11 & big_f(all_1_13_13) = all_1_9_9 & big_g(all_1_5_5) = all_1_0_0 & big_g(all_1_6_6) = all_1_4_4 & big_g(all_1_13_13) = all_1_10_10 & (all_1_8_8 = 0 | ( ~ (all_1_9_9 = 0) & ~ (all_1_10_10 = 0))) & ((all_1_10_10 = 0 & ~ (all_1_3_3 = 0)) | (all_1_11_11 = 0 & ~ (all_1_4_4 = 0))) % 7.11/2.43 | % 7.11/2.43 | Applying alpha-rule on (11) yields: % 7.11/2.43 | (12) big_g(all_1_13_13) = all_1_10_10 % 7.11/2.43 | (13) big_h(all_1_13_13) = all_1_8_8 % 7.11/2.43 | (14) big_g(all_1_5_5) = all_1_0_0 % 7.11/2.43 | (15) big_h(all_1_12_12) = all_1_7_7 % 7.11/2.43 | (16) ~ (all_1_2_2 = 0) % 7.11/2.43 | (17) big_h(all_1_5_5) = all_1_2_2 % 7.11/2.43 | (18) big_f(all_1_5_5) = all_1_1_1 % 7.11/2.43 | (19) big_f(all_1_12_12) = all_1_11_11 % 7.11/2.43 | (20) (all_1_10_10 = 0 & ~ (all_1_3_3 = 0)) | (all_1_11_11 = 0 & ~ (all_1_4_4 = 0)) % 7.11/2.43 | (21) big_f(all_1_13_13) = all_1_9_9 % 7.11/2.43 | (22) all_1_8_8 = 0 | ( ~ (all_1_9_9 = 0) & ~ (all_1_10_10 = 0)) % 7.11/2.43 | (23) big_f(all_1_6_6) = all_1_3_3 % 7.11/2.43 | (24) big_g(all_1_6_6) = all_1_4_4 % 7.11/2.43 | % 7.11/2.43 | Instantiating formula (1) with all_1_2_2, all_1_2_2, all_1_5_5, all_1_5_5 and discharging atoms big_h(all_1_5_5) = all_1_2_2, yields: % 7.11/2.43 | (25) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ( ~ (v7 = 0) & big_h(v4) = v7 & big_f(v4) = v8 & big_f(v3) = v6 & big_f(all_1_5_5) = v2 & big_f(all_1_5_5) = v0 & big_g(v4) = v9 & big_g(v3) = v5 & big_g(all_1_5_5) = v1 & (all_1_2_2 = 0 | ( ~ (v2 = 0) & ~ (v1 = 0))) & ((v1 = 0 & ~ (v6 = 0)) | (v0 = 0 & ~ (v5 = 0)))) % 7.11/2.43 | % 7.11/2.43 | Instantiating formula (1) with all_1_8_8, all_1_2_2, all_1_13_13, all_1_5_5 and discharging atoms big_h(all_1_5_5) = all_1_2_2, big_h(all_1_13_13) = all_1_8_8, yields: % 7.11/2.43 | (26) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ( ~ (v7 = 0) & big_h(v4) = v7 & big_f(v4) = v8 & big_f(v3) = v6 & big_f(all_1_5_5) = v2 & big_f(all_1_13_13) = v0 & big_g(v4) = v9 & big_g(v3) = v5 & big_g(all_1_5_5) = v1 & (all_1_2_2 = 0 | ( ~ (v2 = 0) & ~ (v1 = 0))) & ((v1 = 0 & ~ (v6 = 0)) | (v0 = 0 & ~ (v5 = 0)))) % 7.11/2.43 | % 7.11/2.43 | Instantiating formula (1) with all_1_2_2, all_1_8_8, all_1_5_5, all_1_13_13 and discharging atoms big_h(all_1_5_5) = all_1_2_2, big_h(all_1_13_13) = all_1_8_8, yields: % 7.11/2.44 | (27) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ( ~ (v7 = 0) & big_h(v4) = v7 & big_f(v4) = v8 & big_f(v3) = v6 & big_f(all_1_5_5) = v0 & big_f(all_1_13_13) = v2 & big_g(v4) = v9 & big_g(v3) = v5 & big_g(all_1_13_13) = v1 & (all_1_8_8 = 0 | ( ~ (v2 = 0) & ~ (v1 = 0))) & ((v1 = 0 & ~ (v6 = 0)) | (v0 = 0 & ~ (v5 = 0)))) % 7.11/2.44 | % 7.11/2.44 | Instantiating formula (3) with all_1_2_2, all_1_3_3, all_1_5_5, all_1_6_6 and discharging atoms big_h(all_1_5_5) = all_1_2_2, big_f(all_1_6_6) = all_1_3_3, yields: % 7.11/2.44 | (28) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ( ~ (v7 = 0) & big_h(v4) = v7 & big_h(all_1_6_6) = v2 & big_f(v4) = v8 & big_f(v3) = v6 & big_f(all_1_5_5) = v0 & big_g(v4) = v9 & big_g(v3) = v5 & big_g(all_1_6_6) = v1 & (v2 = 0 | ( ~ (v1 = 0) & ~ (all_1_3_3 = 0))) & ((v1 = 0 & ~ (v6 = 0)) | (v0 = 0 & ~ (v5 = 0)))) % 7.11/2.44 | % 7.11/2.44 | Instantiating formula (5) with all_1_2_2, all_1_3_3, all_1_6_6, all_1_5_5 and discharging atoms big_h(all_1_5_5) = all_1_2_2, big_f(all_1_6_6) = all_1_3_3, yields: % 7.11/2.44 | (29) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ( ~ (v7 = 0) & big_h(v4) = v7 & big_h(all_1_6_6) = v2 & big_f(v4) = v8 & big_f(v3) = v6 & big_f(all_1_5_5) = v1 & big_g(v4) = v9 & big_g(v3) = v5 & big_g(all_1_5_5) = v0 & (all_1_2_2 = 0 | ( ~ (v1 = 0) & ~ (v0 = 0))) & ((v0 = 0 & ~ (v6 = 0)) | (all_1_3_3 = 0 & ~ (v5 = 0)))) % 7.11/2.44 | % 7.11/2.44 | Instantiating formula (3) with all_1_2_2, all_1_11_11, all_1_5_5, all_1_12_12 and discharging atoms big_h(all_1_5_5) = all_1_2_2, big_f(all_1_12_12) = all_1_11_11, yields: % 7.11/2.44 | (30) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ( ~ (v7 = 0) & big_h(v4) = v7 & big_h(all_1_12_12) = v2 & big_f(v4) = v8 & big_f(v3) = v6 & big_f(all_1_5_5) = v0 & big_g(v4) = v9 & big_g(v3) = v5 & big_g(all_1_12_12) = v1 & (v2 = 0 | ( ~ (v1 = 0) & ~ (all_1_11_11 = 0))) & ((v1 = 0 & ~ (v6 = 0)) | (v0 = 0 & ~ (v5 = 0)))) % 7.11/2.44 | % 7.11/2.44 | Instantiating formula (5) with all_1_2_2, all_1_11_11, all_1_12_12, all_1_5_5 and discharging atoms big_h(all_1_5_5) = all_1_2_2, big_f(all_1_12_12) = all_1_11_11, yields: % 7.11/2.44 | (31) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ( ~ (v7 = 0) & big_h(v4) = v7 & big_h(all_1_12_12) = v2 & big_f(v4) = v8 & big_f(v3) = v6 & big_f(all_1_5_5) = v1 & big_g(v4) = v9 & big_g(v3) = v5 & big_g(all_1_5_5) = v0 & (all_1_2_2 = 0 | ( ~ (v1 = 0) & ~ (v0 = 0))) & ((v0 = 0 & ~ (v6 = 0)) | (all_1_11_11 = 0 & ~ (v5 = 0)))) % 7.11/2.44 | % 7.11/2.44 | Instantiating formula (3) with all_1_2_2, all_1_9_9, all_1_5_5, all_1_13_13 and discharging atoms big_h(all_1_5_5) = all_1_2_2, big_f(all_1_13_13) = all_1_9_9, yields: % 7.11/2.44 | (32) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ( ~ (v7 = 0) & big_h(v4) = v7 & big_h(all_1_13_13) = v2 & big_f(v4) = v8 & big_f(v3) = v6 & big_f(all_1_5_5) = v0 & big_g(v4) = v9 & big_g(v3) = v5 & big_g(all_1_13_13) = v1 & (v2 = 0 | ( ~ (v1 = 0) & ~ (all_1_9_9 = 0))) & ((v1 = 0 & ~ (v6 = 0)) | (v0 = 0 & ~ (v5 = 0)))) % 7.11/2.44 | % 7.11/2.44 | Instantiating formula (5) with all_1_2_2, all_1_9_9, all_1_13_13, all_1_5_5 and discharging atoms big_h(all_1_5_5) = all_1_2_2, big_f(all_1_13_13) = all_1_9_9, yields: % 7.11/2.44 | (33) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ( ~ (v7 = 0) & big_h(v4) = v7 & big_h(all_1_13_13) = v2 & big_f(v4) = v8 & big_f(v3) = v6 & big_f(all_1_5_5) = v1 & big_g(v4) = v9 & big_g(v3) = v5 & big_g(all_1_5_5) = v0 & (all_1_2_2 = 0 | ( ~ (v1 = 0) & ~ (v0 = 0))) & ((v0 = 0 & ~ (v6 = 0)) | (all_1_9_9 = 0 & ~ (v5 = 0)))) % 7.11/2.44 | % 7.11/2.44 | Instantiating formula (9) with all_1_2_2, all_1_10_10, all_1_5_5, all_1_13_13 and discharging atoms big_h(all_1_5_5) = all_1_2_2, big_g(all_1_13_13) = all_1_10_10, yields: % 7.11/2.44 | (34) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ( ~ (v7 = 0) & big_h(v4) = v7 & big_h(all_1_13_13) = v2 & big_f(v4) = v8 & big_f(v3) = v6 & big_f(all_1_5_5) = v0 & big_f(all_1_13_13) = v1 & big_g(v4) = v9 & big_g(v3) = v5 & (v2 = 0 | ( ~ (v1 = 0) & ~ (all_1_10_10 = 0))) & ((v0 = 0 & ~ (v5 = 0)) | (all_1_10_10 = 0 & ~ (v6 = 0)))) % 7.11/2.44 | % 7.11/2.44 | Instantiating (31) with all_18_0_64, all_18_1_65, all_18_2_66, all_18_3_67, all_18_4_68, all_18_5_69, all_18_6_70, all_18_7_71, all_18_8_72, all_18_9_73 yields: % 7.11/2.44 | (35) ~ (all_18_2_66 = 0) & big_h(all_18_5_69) = all_18_2_66 & big_h(all_1_12_12) = all_18_7_71 & big_f(all_18_5_69) = all_18_1_65 & big_f(all_18_6_70) = all_18_3_67 & big_f(all_1_5_5) = all_18_8_72 & big_g(all_18_5_69) = all_18_0_64 & big_g(all_18_6_70) = all_18_4_68 & big_g(all_1_5_5) = all_18_9_73 & (all_1_2_2 = 0 | ( ~ (all_18_8_72 = 0) & ~ (all_18_9_73 = 0))) & ((all_18_9_73 = 0 & ~ (all_18_3_67 = 0)) | (all_1_11_11 = 0 & ~ (all_18_4_68 = 0))) % 7.11/2.44 | % 7.11/2.44 | Applying alpha-rule on (35) yields: % 7.11/2.44 | (36) big_g(all_1_5_5) = all_18_9_73 % 7.11/2.44 | (37) big_g(all_18_5_69) = all_18_0_64 % 7.11/2.44 | (38) big_f(all_18_6_70) = all_18_3_67 % 7.11/2.44 | (39) big_h(all_1_12_12) = all_18_7_71 % 7.11/2.44 | (40) big_f(all_1_5_5) = all_18_8_72 % 7.11/2.44 | (41) all_1_2_2 = 0 | ( ~ (all_18_8_72 = 0) & ~ (all_18_9_73 = 0)) % 7.11/2.44 | (42) big_g(all_18_6_70) = all_18_4_68 % 7.11/2.44 | (43) big_h(all_18_5_69) = all_18_2_66 % 7.11/2.44 | (44) (all_18_9_73 = 0 & ~ (all_18_3_67 = 0)) | (all_1_11_11 = 0 & ~ (all_18_4_68 = 0)) % 7.11/2.44 | (45) ~ (all_18_2_66 = 0) % 7.11/2.44 | (46) big_f(all_18_5_69) = all_18_1_65 % 7.11/2.44 | % 7.11/2.44 | Instantiating (29) with all_24_0_94, all_24_1_95, all_24_2_96, all_24_3_97, all_24_4_98, all_24_5_99, all_24_6_100, all_24_7_101, all_24_8_102, all_24_9_103 yields: % 7.11/2.44 | (47) ~ (all_24_2_96 = 0) & big_h(all_24_5_99) = all_24_2_96 & big_h(all_1_6_6) = all_24_7_101 & big_f(all_24_5_99) = all_24_1_95 & big_f(all_24_6_100) = all_24_3_97 & big_f(all_1_5_5) = all_24_8_102 & big_g(all_24_5_99) = all_24_0_94 & big_g(all_24_6_100) = all_24_4_98 & big_g(all_1_5_5) = all_24_9_103 & (all_1_2_2 = 0 | ( ~ (all_24_8_102 = 0) & ~ (all_24_9_103 = 0))) & ((all_24_9_103 = 0 & ~ (all_24_3_97 = 0)) | (all_1_3_3 = 0 & ~ (all_24_4_98 = 0))) % 7.11/2.44 | % 7.11/2.44 | Applying alpha-rule on (47) yields: % 7.11/2.44 | (48) big_h(all_1_6_6) = all_24_7_101 % 7.11/2.45 | (49) big_f(all_1_5_5) = all_24_8_102 % 7.11/2.45 | (50) all_1_2_2 = 0 | ( ~ (all_24_8_102 = 0) & ~ (all_24_9_103 = 0)) % 7.11/2.45 | (51) big_g(all_24_6_100) = all_24_4_98 % 7.11/2.45 | (52) big_g(all_24_5_99) = all_24_0_94 % 7.11/2.45 | (53) big_g(all_1_5_5) = all_24_9_103 % 7.11/2.45 | (54) big_h(all_24_5_99) = all_24_2_96 % 7.11/2.45 | (55) big_f(all_24_6_100) = all_24_3_97 % 7.11/2.45 | (56) (all_24_9_103 = 0 & ~ (all_24_3_97 = 0)) | (all_1_3_3 = 0 & ~ (all_24_4_98 = 0)) % 7.11/2.45 | (57) big_f(all_24_5_99) = all_24_1_95 % 7.11/2.45 | (58) ~ (all_24_2_96 = 0) % 7.11/2.45 | % 7.11/2.45 | Instantiating (28) with all_26_0_104, all_26_1_105, all_26_2_106, all_26_3_107, all_26_4_108, all_26_5_109, all_26_6_110, all_26_7_111, all_26_8_112, all_26_9_113 yields: % 7.11/2.45 | (59) ~ (all_26_2_106 = 0) & big_h(all_26_5_109) = all_26_2_106 & big_h(all_1_6_6) = all_26_7_111 & big_f(all_26_5_109) = all_26_1_105 & big_f(all_26_6_110) = all_26_3_107 & big_f(all_1_5_5) = all_26_9_113 & big_g(all_26_5_109) = all_26_0_104 & big_g(all_26_6_110) = all_26_4_108 & big_g(all_1_6_6) = all_26_8_112 & (all_26_7_111 = 0 | ( ~ (all_26_8_112 = 0) & ~ (all_1_3_3 = 0))) & ((all_26_8_112 = 0 & ~ (all_26_3_107 = 0)) | (all_26_9_113 = 0 & ~ (all_26_4_108 = 0))) % 7.11/2.45 | % 7.11/2.45 | Applying alpha-rule on (59) yields: % 7.11/2.45 | (60) (all_26_8_112 = 0 & ~ (all_26_3_107 = 0)) | (all_26_9_113 = 0 & ~ (all_26_4_108 = 0)) % 7.11/2.45 | (61) big_f(all_26_5_109) = all_26_1_105 % 7.11/2.45 | (62) big_g(all_26_5_109) = all_26_0_104 % 7.11/2.45 | (63) big_f(all_26_6_110) = all_26_3_107 % 7.11/2.45 | (64) ~ (all_26_2_106 = 0) % 7.11/2.45 | (65) big_h(all_1_6_6) = all_26_7_111 % 7.11/2.45 | (66) big_f(all_1_5_5) = all_26_9_113 % 7.11/2.45 | (67) big_g(all_1_6_6) = all_26_8_112 % 7.11/2.45 | (68) all_26_7_111 = 0 | ( ~ (all_26_8_112 = 0) & ~ (all_1_3_3 = 0)) % 7.11/2.45 | (69) big_h(all_26_5_109) = all_26_2_106 % 7.11/2.45 | (70) big_g(all_26_6_110) = all_26_4_108 % 7.11/2.45 | % 7.11/2.45 | Instantiating (26) with all_28_0_114, all_28_1_115, all_28_2_116, all_28_3_117, all_28_4_118, all_28_5_119, all_28_6_120, all_28_7_121, all_28_8_122, all_28_9_123 yields: % 7.11/2.45 | (71) ~ (all_28_2_116 = 0) & big_h(all_28_5_119) = all_28_2_116 & big_f(all_28_5_119) = all_28_1_115 & big_f(all_28_6_120) = all_28_3_117 & big_f(all_1_5_5) = all_28_7_121 & big_f(all_1_13_13) = all_28_9_123 & big_g(all_28_5_119) = all_28_0_114 & big_g(all_28_6_120) = all_28_4_118 & big_g(all_1_5_5) = all_28_8_122 & (all_1_2_2 = 0 | ( ~ (all_28_7_121 = 0) & ~ (all_28_8_122 = 0))) & ((all_28_8_122 = 0 & ~ (all_28_3_117 = 0)) | (all_28_9_123 = 0 & ~ (all_28_4_118 = 0))) % 7.11/2.45 | % 7.11/2.45 | Applying alpha-rule on (71) yields: % 7.11/2.45 | (72) big_g(all_1_5_5) = all_28_8_122 % 7.11/2.45 | (73) big_f(all_1_5_5) = all_28_7_121 % 7.11/2.45 | (74) big_f(all_28_6_120) = all_28_3_117 % 7.11/2.45 | (75) big_f(all_1_13_13) = all_28_9_123 % 7.11/2.45 | (76) big_f(all_28_5_119) = all_28_1_115 % 7.11/2.45 | (77) big_g(all_28_5_119) = all_28_0_114 % 7.11/2.45 | (78) (all_28_8_122 = 0 & ~ (all_28_3_117 = 0)) | (all_28_9_123 = 0 & ~ (all_28_4_118 = 0)) % 7.11/2.45 | (79) big_g(all_28_6_120) = all_28_4_118 % 7.11/2.45 | (80) ~ (all_28_2_116 = 0) % 7.11/2.45 | (81) all_1_2_2 = 0 | ( ~ (all_28_7_121 = 0) & ~ (all_28_8_122 = 0)) % 7.11/2.45 | (82) big_h(all_28_5_119) = all_28_2_116 % 7.11/2.45 | % 7.11/2.45 | Instantiating (25) with all_30_0_124, all_30_1_125, all_30_2_126, all_30_3_127, all_30_4_128, all_30_5_129, all_30_6_130, all_30_7_131, all_30_8_132, all_30_9_133 yields: % 7.11/2.45 | (83) ~ (all_30_2_126 = 0) & big_h(all_30_5_129) = all_30_2_126 & big_f(all_30_5_129) = all_30_1_125 & big_f(all_30_6_130) = all_30_3_127 & big_f(all_1_5_5) = all_30_7_131 & big_f(all_1_5_5) = all_30_9_133 & big_g(all_30_5_129) = all_30_0_124 & big_g(all_30_6_130) = all_30_4_128 & big_g(all_1_5_5) = all_30_8_132 & (all_1_2_2 = 0 | ( ~ (all_30_7_131 = 0) & ~ (all_30_8_132 = 0))) & ((all_30_8_132 = 0 & ~ (all_30_3_127 = 0)) | (all_30_9_133 = 0 & ~ (all_30_4_128 = 0))) % 7.11/2.45 | % 7.11/2.45 | Applying alpha-rule on (83) yields: % 7.11/2.45 | (84) big_f(all_30_6_130) = all_30_3_127 % 7.11/2.45 | (85) big_f(all_1_5_5) = all_30_9_133 % 7.11/2.45 | (86) big_g(all_30_5_129) = all_30_0_124 % 7.11/2.45 | (87) ~ (all_30_2_126 = 0) % 7.11/2.45 | (88) big_f(all_30_5_129) = all_30_1_125 % 7.11/2.45 | (89) (all_30_8_132 = 0 & ~ (all_30_3_127 = 0)) | (all_30_9_133 = 0 & ~ (all_30_4_128 = 0)) % 7.11/2.45 | (90) big_g(all_1_5_5) = all_30_8_132 % 7.11/2.45 | (91) big_g(all_30_6_130) = all_30_4_128 % 7.11/2.45 | (92) all_1_2_2 = 0 | ( ~ (all_30_7_131 = 0) & ~ (all_30_8_132 = 0)) % 7.11/2.45 | (93) big_h(all_30_5_129) = all_30_2_126 % 7.11/2.45 | (94) big_f(all_1_5_5) = all_30_7_131 % 7.11/2.45 | % 7.11/2.45 | Instantiating (30) with all_36_0_154, all_36_1_155, all_36_2_156, all_36_3_157, all_36_4_158, all_36_5_159, all_36_6_160, all_36_7_161, all_36_8_162, all_36_9_163 yields: % 7.11/2.45 | (95) ~ (all_36_2_156 = 0) & big_h(all_36_5_159) = all_36_2_156 & big_h(all_1_12_12) = all_36_7_161 & big_f(all_36_5_159) = all_36_1_155 & big_f(all_36_6_160) = all_36_3_157 & big_f(all_1_5_5) = all_36_9_163 & big_g(all_36_5_159) = all_36_0_154 & big_g(all_36_6_160) = all_36_4_158 & big_g(all_1_12_12) = all_36_8_162 & (all_36_7_161 = 0 | ( ~ (all_36_8_162 = 0) & ~ (all_1_11_11 = 0))) & ((all_36_8_162 = 0 & ~ (all_36_3_157 = 0)) | (all_36_9_163 = 0 & ~ (all_36_4_158 = 0))) % 7.11/2.45 | % 7.11/2.45 | Applying alpha-rule on (95) yields: % 7.11/2.45 | (96) all_36_7_161 = 0 | ( ~ (all_36_8_162 = 0) & ~ (all_1_11_11 = 0)) % 7.11/2.45 | (97) big_h(all_1_12_12) = all_36_7_161 % 7.11/2.45 | (98) big_f(all_1_5_5) = all_36_9_163 % 7.11/2.45 | (99) big_f(all_36_5_159) = all_36_1_155 % 7.11/2.45 | (100) big_h(all_36_5_159) = all_36_2_156 % 7.11/2.45 | (101) big_g(all_36_5_159) = all_36_0_154 % 7.11/2.45 | (102) big_g(all_36_6_160) = all_36_4_158 % 7.11/2.46 | (103) (all_36_8_162 = 0 & ~ (all_36_3_157 = 0)) | (all_36_9_163 = 0 & ~ (all_36_4_158 = 0)) % 7.11/2.46 | (104) ~ (all_36_2_156 = 0) % 7.11/2.46 | (105) big_g(all_1_12_12) = all_36_8_162 % 7.11/2.46 | (106) big_f(all_36_6_160) = all_36_3_157 % 7.11/2.46 | % 7.11/2.46 | Instantiating (27) with all_42_0_184, all_42_1_185, all_42_2_186, all_42_3_187, all_42_4_188, all_42_5_189, all_42_6_190, all_42_7_191, all_42_8_192, all_42_9_193 yields: % 7.11/2.46 | (107) ~ (all_42_2_186 = 0) & big_h(all_42_5_189) = all_42_2_186 & big_f(all_42_5_189) = all_42_1_185 & big_f(all_42_6_190) = all_42_3_187 & big_f(all_1_5_5) = all_42_9_193 & big_f(all_1_13_13) = all_42_7_191 & big_g(all_42_5_189) = all_42_0_184 & big_g(all_42_6_190) = all_42_4_188 & big_g(all_1_13_13) = all_42_8_192 & (all_1_8_8 = 0 | ( ~ (all_42_7_191 = 0) & ~ (all_42_8_192 = 0))) & ((all_42_8_192 = 0 & ~ (all_42_3_187 = 0)) | (all_42_9_193 = 0 & ~ (all_42_4_188 = 0))) % 7.11/2.46 | % 7.11/2.46 | Applying alpha-rule on (107) yields: % 7.11/2.46 | (108) big_h(all_42_5_189) = all_42_2_186 % 7.11/2.46 | (109) (all_42_8_192 = 0 & ~ (all_42_3_187 = 0)) | (all_42_9_193 = 0 & ~ (all_42_4_188 = 0)) % 7.11/2.46 | (110) big_f(all_1_13_13) = all_42_7_191 % 7.11/2.46 | (111) ~ (all_42_2_186 = 0) % 7.11/2.46 | (112) big_f(all_1_5_5) = all_42_9_193 % 7.11/2.46 | (113) big_g(all_42_6_190) = all_42_4_188 % 7.11/2.46 | (114) big_f(all_42_5_189) = all_42_1_185 % 7.11/2.46 | (115) big_g(all_42_5_189) = all_42_0_184 % 7.11/2.46 | (116) all_1_8_8 = 0 | ( ~ (all_42_7_191 = 0) & ~ (all_42_8_192 = 0)) % 7.11/2.46 | (117) big_g(all_1_13_13) = all_42_8_192 % 7.11/2.46 | (118) big_f(all_42_6_190) = all_42_3_187 % 7.11/2.46 | % 7.11/2.46 | Instantiating (33) with all_52_0_234, all_52_1_235, all_52_2_236, all_52_3_237, all_52_4_238, all_52_5_239, all_52_6_240, all_52_7_241, all_52_8_242, all_52_9_243 yields: % 7.11/2.46 | (119) ~ (all_52_2_236 = 0) & big_h(all_52_5_239) = all_52_2_236 & big_h(all_1_13_13) = all_52_7_241 & big_f(all_52_5_239) = all_52_1_235 & big_f(all_52_6_240) = all_52_3_237 & big_f(all_1_5_5) = all_52_8_242 & big_g(all_52_5_239) = all_52_0_234 & big_g(all_52_6_240) = all_52_4_238 & big_g(all_1_5_5) = all_52_9_243 & (all_1_2_2 = 0 | ( ~ (all_52_8_242 = 0) & ~ (all_52_9_243 = 0))) & ((all_52_9_243 = 0 & ~ (all_52_3_237 = 0)) | (all_1_9_9 = 0 & ~ (all_52_4_238 = 0))) % 7.11/2.46 | % 7.11/2.46 | Applying alpha-rule on (119) yields: % 7.11/2.46 | (120) big_h(all_52_5_239) = all_52_2_236 % 7.11/2.46 | (121) big_h(all_1_13_13) = all_52_7_241 % 7.11/2.46 | (122) (all_52_9_243 = 0 & ~ (all_52_3_237 = 0)) | (all_1_9_9 = 0 & ~ (all_52_4_238 = 0)) % 7.11/2.46 | (123) big_g(all_1_5_5) = all_52_9_243 % 7.11/2.46 | (124) big_g(all_52_6_240) = all_52_4_238 % 7.11/2.46 | (125) big_g(all_52_5_239) = all_52_0_234 % 7.11/2.46 | (126) big_f(all_52_6_240) = all_52_3_237 % 7.11/2.46 | (127) ~ (all_52_2_236 = 0) % 7.11/2.46 | (128) big_f(all_1_5_5) = all_52_8_242 % 7.11/2.46 | (129) all_1_2_2 = 0 | ( ~ (all_52_8_242 = 0) & ~ (all_52_9_243 = 0)) % 7.11/2.46 | (130) big_f(all_52_5_239) = all_52_1_235 % 7.11/2.46 | % 7.11/2.46 | Instantiating (32) with all_54_0_244, all_54_1_245, all_54_2_246, all_54_3_247, all_54_4_248, all_54_5_249, all_54_6_250, all_54_7_251, all_54_8_252, all_54_9_253 yields: % 7.11/2.46 | (131) ~ (all_54_2_246 = 0) & big_h(all_54_5_249) = all_54_2_246 & big_h(all_1_13_13) = all_54_7_251 & big_f(all_54_5_249) = all_54_1_245 & big_f(all_54_6_250) = all_54_3_247 & big_f(all_1_5_5) = all_54_9_253 & big_g(all_54_5_249) = all_54_0_244 & big_g(all_54_6_250) = all_54_4_248 & big_g(all_1_13_13) = all_54_8_252 & (all_54_7_251 = 0 | ( ~ (all_54_8_252 = 0) & ~ (all_1_9_9 = 0))) & ((all_54_8_252 = 0 & ~ (all_54_3_247 = 0)) | (all_54_9_253 = 0 & ~ (all_54_4_248 = 0))) % 7.11/2.46 | % 7.11/2.46 | Applying alpha-rule on (131) yields: % 7.58/2.46 | (132) big_f(all_1_5_5) = all_54_9_253 % 7.58/2.46 | (133) big_h(all_54_5_249) = all_54_2_246 % 7.58/2.46 | (134) big_g(all_54_5_249) = all_54_0_244 % 7.58/2.46 | (135) big_h(all_1_13_13) = all_54_7_251 % 7.58/2.46 | (136) all_54_7_251 = 0 | ( ~ (all_54_8_252 = 0) & ~ (all_1_9_9 = 0)) % 7.58/2.46 | (137) (all_54_8_252 = 0 & ~ (all_54_3_247 = 0)) | (all_54_9_253 = 0 & ~ (all_54_4_248 = 0)) % 7.58/2.46 | (138) ~ (all_54_2_246 = 0) % 7.58/2.46 | (139) big_f(all_54_5_249) = all_54_1_245 % 7.58/2.46 | (140) big_g(all_1_13_13) = all_54_8_252 % 7.58/2.46 | (141) big_g(all_54_6_250) = all_54_4_248 % 7.58/2.46 | (142) big_f(all_54_6_250) = all_54_3_247 % 7.58/2.46 | % 7.58/2.46 | Instantiating (34) with all_74_0_344, all_74_1_345, all_74_2_346, all_74_3_347, all_74_4_348, all_74_5_349, all_74_6_350, all_74_7_351, all_74_8_352, all_74_9_353 yields: % 7.58/2.46 | (143) ~ (all_74_2_346 = 0) & big_h(all_74_5_349) = all_74_2_346 & big_h(all_1_13_13) = all_74_7_351 & big_f(all_74_5_349) = all_74_1_345 & big_f(all_74_6_350) = all_74_3_347 & big_f(all_1_5_5) = all_74_9_353 & big_f(all_1_13_13) = all_74_8_352 & big_g(all_74_5_349) = all_74_0_344 & big_g(all_74_6_350) = all_74_4_348 & (all_74_7_351 = 0 | ( ~ (all_74_8_352 = 0) & ~ (all_1_10_10 = 0))) & ((all_74_9_353 = 0 & ~ (all_74_4_348 = 0)) | (all_1_10_10 = 0 & ~ (all_74_3_347 = 0))) % 7.58/2.46 | % 7.58/2.46 | Applying alpha-rule on (143) yields: % 7.58/2.46 | (144) big_f(all_1_13_13) = all_74_8_352 % 7.58/2.46 | (145) all_74_7_351 = 0 | ( ~ (all_74_8_352 = 0) & ~ (all_1_10_10 = 0)) % 7.58/2.46 | (146) big_f(all_74_6_350) = all_74_3_347 % 7.58/2.46 | (147) ~ (all_74_2_346 = 0) % 7.58/2.46 | (148) big_f(all_74_5_349) = all_74_1_345 % 7.58/2.46 | (149) (all_74_9_353 = 0 & ~ (all_74_4_348 = 0)) | (all_1_10_10 = 0 & ~ (all_74_3_347 = 0)) % 7.58/2.46 | (150) big_f(all_1_5_5) = all_74_9_353 % 7.58/2.46 | (151) big_g(all_74_5_349) = all_74_0_344 % 7.58/2.46 | (152) big_h(all_74_5_349) = all_74_2_346 % 7.58/2.47 | (153) big_g(all_74_6_350) = all_74_4_348 % 7.58/2.47 | (154) big_h(all_1_13_13) = all_74_7_351 % 7.58/2.47 | % 7.58/2.47 +-Applying beta-rule and splitting (81), into two cases. % 7.58/2.47 |-Branch one: % 7.58/2.47 | (155) all_1_2_2 = 0 % 7.58/2.47 | % 7.58/2.47 | Equations (155) can reduce 16 to: % 7.58/2.47 | (156) $false % 7.58/2.47 | % 7.58/2.47 |-The branch is then unsatisfiable % 7.58/2.47 |-Branch two: % 7.58/2.47 | (16) ~ (all_1_2_2 = 0) % 7.58/2.47 | (158) ~ (all_28_7_121 = 0) & ~ (all_28_8_122 = 0) % 7.58/2.47 | % 7.58/2.47 +-Applying beta-rule and splitting (129), into two cases. % 7.58/2.47 |-Branch one: % 7.58/2.47 | (155) all_1_2_2 = 0 % 7.58/2.47 | % 7.58/2.47 | Equations (155) can reduce 16 to: % 7.58/2.47 | (156) $false % 7.58/2.47 | % 7.58/2.47 |-The branch is then unsatisfiable % 7.58/2.47 |-Branch two: % 7.58/2.47 | (16) ~ (all_1_2_2 = 0) % 7.58/2.47 | (162) ~ (all_52_8_242 = 0) & ~ (all_52_9_243 = 0) % 7.58/2.47 | % 7.58/2.47 +-Applying beta-rule and splitting (41), into two cases. % 7.58/2.47 |-Branch one: % 7.58/2.47 | (155) all_1_2_2 = 0 % 7.58/2.47 | % 7.58/2.47 | Equations (155) can reduce 16 to: % 7.58/2.47 | (156) $false % 7.58/2.47 | % 7.58/2.47 |-The branch is then unsatisfiable % 7.58/2.47 |-Branch two: % 7.58/2.47 | (16) ~ (all_1_2_2 = 0) % 7.58/2.47 | (166) ~ (all_18_8_72 = 0) & ~ (all_18_9_73 = 0) % 7.58/2.47 | % 7.58/2.47 | Applying alpha-rule on (166) yields: % 7.58/2.47 | (167) ~ (all_18_8_72 = 0) % 7.58/2.47 | (168) ~ (all_18_9_73 = 0) % 7.58/2.47 | % 7.58/2.47 +-Applying beta-rule and splitting (50), into two cases. % 7.58/2.47 |-Branch one: % 7.58/2.47 | (155) all_1_2_2 = 0 % 7.58/2.47 | % 7.58/2.47 | Equations (155) can reduce 16 to: % 7.58/2.47 | (156) $false % 7.58/2.47 | % 7.58/2.47 |-The branch is then unsatisfiable % 7.58/2.47 |-Branch two: % 7.58/2.47 | (16) ~ (all_1_2_2 = 0) % 7.58/2.47 | (172) ~ (all_24_8_102 = 0) & ~ (all_24_9_103 = 0) % 7.58/2.47 | % 7.58/2.47 +-Applying beta-rule and splitting (92), into two cases. % 7.58/2.47 |-Branch one: % 7.58/2.47 | (155) all_1_2_2 = 0 % 7.58/2.47 | % 7.58/2.47 | Equations (155) can reduce 16 to: % 7.58/2.47 | (156) $false % 7.58/2.47 | % 7.58/2.47 |-The branch is then unsatisfiable % 7.58/2.47 |-Branch two: % 7.58/2.47 | (16) ~ (all_1_2_2 = 0) % 7.58/2.47 | (176) ~ (all_30_7_131 = 0) & ~ (all_30_8_132 = 0) % 7.58/2.47 | % 7.58/2.47 | Applying alpha-rule on (176) yields: % 7.58/2.47 | (177) ~ (all_30_7_131 = 0) % 7.58/2.47 | (178) ~ (all_30_8_132 = 0) % 7.58/2.47 | % 7.58/2.47 +-Applying beta-rule and splitting (89), into two cases. % 7.58/2.47 |-Branch one: % 7.58/2.47 | (179) all_30_8_132 = 0 & ~ (all_30_3_127 = 0) % 7.58/2.47 | % 7.58/2.47 | Applying alpha-rule on (179) yields: % 7.58/2.47 | (180) all_30_8_132 = 0 % 7.58/2.47 | (181) ~ (all_30_3_127 = 0) % 7.58/2.47 | % 7.58/2.47 | Equations (180) can reduce 178 to: % 7.58/2.47 | (156) $false % 7.58/2.47 | % 7.58/2.47 |-The branch is then unsatisfiable % 7.58/2.47 |-Branch two: % 7.58/2.47 | (183) all_30_9_133 = 0 & ~ (all_30_4_128 = 0) % 7.58/2.47 | % 7.58/2.47 | Applying alpha-rule on (183) yields: % 7.58/2.47 | (184) all_30_9_133 = 0 % 7.58/2.47 | (185) ~ (all_30_4_128 = 0) % 7.58/2.47 | % 7.58/2.47 | From (184) and (85) follows: % 7.58/2.47 | (186) big_f(all_1_5_5) = 0 % 7.58/2.47 | % 7.58/2.47 | Instantiating formula (8) with all_1_5_5, all_52_8_242, all_74_9_353 and discharging atoms big_f(all_1_5_5) = all_74_9_353, big_f(all_1_5_5) = all_52_8_242, yields: % 7.58/2.47 | (187) all_74_9_353 = all_52_8_242 % 7.58/2.47 | % 7.58/2.47 | Instantiating formula (8) with all_1_5_5, all_42_9_193, all_54_9_253 and discharging atoms big_f(all_1_5_5) = all_54_9_253, big_f(all_1_5_5) = all_42_9_193, yields: % 7.58/2.47 | (188) all_54_9_253 = all_42_9_193 % 7.58/2.47 | % 7.58/2.47 | Instantiating formula (8) with all_1_5_5, all_42_9_193, all_52_8_242 and discharging atoms big_f(all_1_5_5) = all_52_8_242, big_f(all_1_5_5) = all_42_9_193, yields: % 7.58/2.47 | (189) all_52_8_242 = all_42_9_193 % 7.58/2.47 | % 7.58/2.47 | Instantiating formula (8) with all_1_5_5, all_36_9_163, all_54_9_253 and discharging atoms big_f(all_1_5_5) = all_54_9_253, big_f(all_1_5_5) = all_36_9_163, yields: % 7.58/2.47 | (190) all_54_9_253 = all_36_9_163 % 7.58/2.47 | % 7.58/2.47 | Instantiating formula (8) with all_1_5_5, all_30_7_131, all_54_9_253 and discharging atoms big_f(all_1_5_5) = all_54_9_253, big_f(all_1_5_5) = all_30_7_131, yields: % 7.58/2.47 | (191) all_54_9_253 = all_30_7_131 % 7.58/2.47 | % 7.58/2.47 | Instantiating formula (8) with all_1_5_5, all_28_7_121, all_30_7_131 and discharging atoms big_f(all_1_5_5) = all_30_7_131, big_f(all_1_5_5) = all_28_7_121, yields: % 7.58/2.47 | (192) all_30_7_131 = all_28_7_121 % 7.58/2.47 | % 7.58/2.47 | Instantiating formula (8) with all_1_5_5, all_26_9_113, all_28_7_121 and discharging atoms big_f(all_1_5_5) = all_28_7_121, big_f(all_1_5_5) = all_26_9_113, yields: % 7.58/2.47 | (193) all_28_7_121 = all_26_9_113 % 7.58/2.47 | % 7.58/2.47 | Instantiating formula (8) with all_1_5_5, all_24_8_102, all_28_7_121 and discharging atoms big_f(all_1_5_5) = all_28_7_121, big_f(all_1_5_5) = all_24_8_102, yields: % 7.58/2.47 | (194) all_28_7_121 = all_24_8_102 % 7.58/2.47 | % 7.58/2.47 | Instantiating formula (8) with all_1_5_5, all_18_8_72, all_74_9_353 and discharging atoms big_f(all_1_5_5) = all_74_9_353, big_f(all_1_5_5) = all_18_8_72, yields: % 7.58/2.47 | (195) all_74_9_353 = all_18_8_72 % 7.58/2.47 | % 7.58/2.47 | Instantiating formula (8) with all_1_5_5, 0, all_26_9_113 and discharging atoms big_f(all_1_5_5) = all_26_9_113, big_f(all_1_5_5) = 0, yields: % 7.58/2.47 | (196) all_26_9_113 = 0 % 7.58/2.47 | % 7.58/2.47 | Combining equations (187,195) yields a new equation: % 7.58/2.47 | (197) all_52_8_242 = all_18_8_72 % 7.58/2.47 | % 7.58/2.47 | Simplifying 197 yields: % 7.58/2.47 | (198) all_52_8_242 = all_18_8_72 % 7.58/2.47 | % 7.58/2.47 | Combining equations (188,190) yields a new equation: % 7.58/2.47 | (199) all_42_9_193 = all_36_9_163 % 7.58/2.47 | % 7.58/2.47 | Simplifying 199 yields: % 7.58/2.47 | (200) all_42_9_193 = all_36_9_163 % 7.58/2.47 | % 7.58/2.47 | Combining equations (191,190) yields a new equation: % 7.58/2.47 | (201) all_36_9_163 = all_30_7_131 % 7.58/2.47 | % 7.58/2.47 | Combining equations (189,198) yields a new equation: % 7.58/2.47 | (202) all_42_9_193 = all_18_8_72 % 7.58/2.47 | % 7.58/2.47 | Simplifying 202 yields: % 7.58/2.47 | (203) all_42_9_193 = all_18_8_72 % 7.58/2.47 | % 7.58/2.47 | Combining equations (200,203) yields a new equation: % 7.58/2.47 | (204) all_36_9_163 = all_18_8_72 % 7.58/2.47 | % 7.58/2.47 | Simplifying 204 yields: % 7.58/2.47 | (205) all_36_9_163 = all_18_8_72 % 7.58/2.47 | % 7.58/2.47 | Combining equations (201,205) yields a new equation: % 7.58/2.47 | (206) all_30_7_131 = all_18_8_72 % 7.58/2.47 | % 7.58/2.47 | Simplifying 206 yields: % 7.58/2.47 | (207) all_30_7_131 = all_18_8_72 % 7.58/2.47 | % 7.58/2.47 | Combining equations (192,207) yields a new equation: % 7.58/2.47 | (208) all_28_7_121 = all_18_8_72 % 7.58/2.47 | % 7.58/2.47 | Simplifying 208 yields: % 7.58/2.47 | (209) all_28_7_121 = all_18_8_72 % 7.58/2.47 | % 7.58/2.47 | Combining equations (193,194) yields a new equation: % 7.58/2.47 | (210) all_26_9_113 = all_24_8_102 % 7.58/2.47 | % 7.58/2.47 | Simplifying 210 yields: % 7.58/2.47 | (211) all_26_9_113 = all_24_8_102 % 7.58/2.47 | % 7.58/2.47 | Combining equations (209,194) yields a new equation: % 7.58/2.47 | (212) all_24_8_102 = all_18_8_72 % 7.58/2.47 | % 7.58/2.47 | Combining equations (211,196) yields a new equation: % 7.58/2.47 | (213) all_24_8_102 = 0 % 7.58/2.47 | % 7.58/2.47 | Simplifying 213 yields: % 7.58/2.47 | (214) all_24_8_102 = 0 % 7.58/2.47 | % 7.58/2.47 | Combining equations (214,212) yields a new equation: % 7.58/2.47 | (215) all_18_8_72 = 0 % 7.58/2.47 | % 7.58/2.47 | Equations (215) can reduce 167 to: % 7.58/2.47 | (156) $false % 7.58/2.47 | % 7.58/2.47 |-The branch is then unsatisfiable % 7.58/2.47 % SZS output end Proof for theBenchmark % 7.58/2.47 % 7.58/2.47 1832ms %------------------------------------------------------------------------------