%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SYN354+1 : TPTP v8.1.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n022.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:43 EDT 2022 % Result : Theorem 2.70s 1.38s % Output : Proof 3.95s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SYN354+1 : TPTP v8.1.0. Released v2.0.0. % 0.07/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.34 % Computer : n022.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 : Tue Jul 12 07:15:55 EDT 2022 % 0.12/0.34 % CPUTime : % 0.43/0.61 ____ _ % 0.43/0.61 ___ / __ \_____(_)___ ________ __________ % 0.43/0.61 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.43/0.61 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.43/0.61 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.43/0.61 % 0.43/0.61 A Theorem Prover for First-Order Logic % 0.43/0.61 (ePrincess v.1.0) % 0.43/0.61 % 0.43/0.61 (c) Philipp Rümmer, 2009-2015 % 0.43/0.61 (c) Peter Backeman, 2014-2015 % 0.43/0.61 (contributions by Angelo Brillout, Peter Baumgartner) % 0.43/0.61 Free software under GNU Lesser General Public License (LGPL). % 0.43/0.61 Bug reports to peter@backeman.se % 0.43/0.61 % 0.43/0.61 For more information, visit http://user.uu.se/~petba168/breu/ % 0.43/0.61 % 0.43/0.61 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.66/0.66 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.34/0.93 Prover 0: Preprocessing ... % 1.34/0.98 Prover 0: Warning: ignoring some quantifiers % 1.48/1.00 Prover 0: Constructing countermodel ... % 1.68/1.11 Prover 0: gave up % 1.68/1.11 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 1.83/1.12 Prover 1: Preprocessing ... % 1.95/1.18 Prover 1: Constructing countermodel ... % 2.17/1.25 Prover 1: gave up % 2.17/1.25 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 2.17/1.26 Prover 2: Preprocessing ... % 2.35/1.29 Prover 2: Warning: ignoring some quantifiers % 2.35/1.29 Prover 2: Constructing countermodel ... % 2.70/1.38 Prover 2: proved (130ms) % 2.70/1.38 % 2.70/1.38 No countermodel exists, formula is valid % 2.70/1.38 % SZS status Theorem for theBenchmark % 2.70/1.38 % 2.70/1.38 Generating proof ... Warning: ignoring some quantifiers % 3.57/1.67 found it (size 66) % 3.57/1.67 % 3.57/1.67 % SZS output start Proof for theBenchmark % 3.57/1.67 Assumed formulas after preprocessing and simplification: % 3.57/1.67 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (big_f(v0, v1) = v2 & big_g(v0, v1) = v3 & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (big_f(v7, v6) = v5) | ~ (big_f(v7, v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : ! [v7] : (v5 = v4 | ~ (big_g(v7, v6) = v5) | ~ (big_g(v7, v6) = v4)) & ! [v4] : ! [v5] : ! [v6] : ( ~ (big_f(v4, v5) = v6) | ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : (v3 = 0 & v2 = 0 & big_f(v1, v5) = v7 & big_f(v1, v4) = v9 & big_f(v0, v4) = v8 & ( ~ (v9 = 0) | ~ (v8 = 0) | ~ (v6 = 0)) & ( ~ (v6 = 0) | v7 = 0 | (((v12 = 0 & big_g(v5, v10) = 0) | (v11 = 0 & big_g(v1, v10) = 0)) & (( ~ (v12 = 0) & big_g(v5, v10) = v12) | ( ~ (v11 = 0) & big_g(v1, v10) = v11)))) & ((v13 = 0 & big_g(v4, v10) = 0) | ( ~ (v11 = 0) & big_g(v1, v10) = v11)) & ((v11 = 0 & big_g(v1, v10) = 0) | ( ~ (v13 = 0) & big_g(v4, v10) = v13)))) & ? [v4] : ? [v5] : ? [v6] : big_f(v5, v4) = v6 & ? [v4] : ? [v5] : ? [v6] : big_g(v5, v4) = v6) % 3.65/1.70 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3 yields: % 3.65/1.70 | (1) big_f(all_0_3_3, all_0_2_2) = all_0_1_1 & big_g(all_0_3_3, all_0_2_2) = all_0_0_0 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (big_f(v3, v2) = v1) | ~ (big_f(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (big_g(v3, v2) = v1) | ~ (big_g(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (big_f(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (all_0_0_0 = 0 & all_0_1_1 = 0 & big_f(all_0_2_2, v1) = v3 & big_f(all_0_2_2, v0) = v5 & big_f(all_0_3_3, v0) = v4 & ( ~ (v5 = 0) | ~ (v4 = 0) | ~ (v2 = 0)) & ( ~ (v2 = 0) | v3 = 0 | (((v8 = 0 & big_g(v1, v6) = 0) | (v7 = 0 & big_g(all_0_2_2, v6) = 0)) & (( ~ (v8 = 0) & big_g(v1, v6) = v8) | ( ~ (v7 = 0) & big_g(all_0_2_2, v6) = v7)))) & ((v9 = 0 & big_g(v0, v6) = 0) | ( ~ (v7 = 0) & big_g(all_0_2_2, v6) = v7)) & ((v7 = 0 & big_g(all_0_2_2, v6) = 0) | ( ~ (v9 = 0) & big_g(v0, v6) = v9)))) & ? [v0] : ? [v1] : ? [v2] : big_f(v1, v0) = v2 & ? [v0] : ? [v1] : ? [v2] : big_g(v1, v0) = v2 % 3.65/1.70 | % 3.65/1.70 | Applying alpha-rule on (1) yields: % 3.65/1.70 | (2) big_g(all_0_3_3, all_0_2_2) = all_0_0_0 % 3.65/1.70 | (3) ? [v0] : ? [v1] : ? [v2] : big_f(v1, v0) = v2 % 3.65/1.70 | (4) big_f(all_0_3_3, all_0_2_2) = all_0_1_1 % 3.65/1.70 | (5) ? [v0] : ? [v1] : ? [v2] : big_g(v1, v0) = v2 % 3.65/1.70 | (6) ! [v0] : ! [v1] : ! [v2] : ( ~ (big_f(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : (all_0_0_0 = 0 & all_0_1_1 = 0 & big_f(all_0_2_2, v1) = v3 & big_f(all_0_2_2, v0) = v5 & big_f(all_0_3_3, v0) = v4 & ( ~ (v5 = 0) | ~ (v4 = 0) | ~ (v2 = 0)) & ( ~ (v2 = 0) | v3 = 0 | (((v8 = 0 & big_g(v1, v6) = 0) | (v7 = 0 & big_g(all_0_2_2, v6) = 0)) & (( ~ (v8 = 0) & big_g(v1, v6) = v8) | ( ~ (v7 = 0) & big_g(all_0_2_2, v6) = v7)))) & ((v9 = 0 & big_g(v0, v6) = 0) | ( ~ (v7 = 0) & big_g(all_0_2_2, v6) = v7)) & ((v7 = 0 & big_g(all_0_2_2, v6) = 0) | ( ~ (v9 = 0) & big_g(v0, v6) = v9)))) % 3.65/1.71 | (7) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (big_g(v3, v2) = v1) | ~ (big_g(v3, v2) = v0)) % 3.65/1.71 | (8) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (big_f(v3, v2) = v1) | ~ (big_f(v3, v2) = v0)) % 3.65/1.71 | % 3.65/1.71 | Instantiating formula (6) with all_0_1_1, all_0_2_2, all_0_3_3 and discharging atoms big_f(all_0_3_3, all_0_2_2) = all_0_1_1, yields: % 3.65/1.71 | (9) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (all_0_0_0 = 0 & all_0_1_1 = 0 & big_f(all_0_2_2, all_0_2_2) = v0 & big_f(all_0_2_2, all_0_3_3) = v2 & big_f(all_0_3_3, all_0_3_3) = v1 & ( ~ (v2 = 0) | ~ (v1 = 0)) & (v0 = 0 | (((v5 = 0 & big_g(all_0_2_2, v3) = 0) | (v4 = 0 & big_g(all_0_2_2, v3) = 0)) & (( ~ (v5 = 0) & big_g(all_0_2_2, v3) = v5) | ( ~ (v4 = 0) & big_g(all_0_2_2, v3) = v4)))) & ((v6 = 0 & big_g(all_0_3_3, v3) = 0) | ( ~ (v4 = 0) & big_g(all_0_2_2, v3) = v4)) & ((v4 = 0 & big_g(all_0_2_2, v3) = 0) | ( ~ (v6 = 0) & big_g(all_0_3_3, v3) = v6))) % 3.65/1.71 | % 3.65/1.71 | Instantiating (9) with all_12_0_10, all_12_1_11, all_12_2_12, all_12_3_13, all_12_4_14, all_12_5_15, all_12_6_16 yields: % 3.65/1.71 | (10) all_0_0_0 = 0 & all_0_1_1 = 0 & big_f(all_0_2_2, all_0_2_2) = all_12_6_16 & big_f(all_0_2_2, all_0_3_3) = all_12_4_14 & big_f(all_0_3_3, all_0_3_3) = all_12_5_15 & ( ~ (all_12_4_14 = 0) | ~ (all_12_5_15 = 0)) & (all_12_6_16 = 0 | (((all_12_1_11 = 0 & big_g(all_0_2_2, all_12_3_13) = 0) | (all_12_2_12 = 0 & big_g(all_0_2_2, all_12_3_13) = 0)) & (( ~ (all_12_1_11 = 0) & big_g(all_0_2_2, all_12_3_13) = all_12_1_11) | ( ~ (all_12_2_12 = 0) & big_g(all_0_2_2, all_12_3_13) = all_12_2_12)))) & ((all_12_0_10 = 0 & big_g(all_0_3_3, all_12_3_13) = 0) | ( ~ (all_12_2_12 = 0) & big_g(all_0_2_2, all_12_3_13) = all_12_2_12)) & ((all_12_2_12 = 0 & big_g(all_0_2_2, all_12_3_13) = 0) | ( ~ (all_12_0_10 = 0) & big_g(all_0_3_3, all_12_3_13) = all_12_0_10)) % 3.65/1.71 | % 3.65/1.71 | Applying alpha-rule on (10) yields: % 3.65/1.71 | (11) all_0_1_1 = 0 % 3.65/1.71 | (12) (all_12_0_10 = 0 & big_g(all_0_3_3, all_12_3_13) = 0) | ( ~ (all_12_2_12 = 0) & big_g(all_0_2_2, all_12_3_13) = all_12_2_12) % 3.65/1.71 | (13) (all_12_2_12 = 0 & big_g(all_0_2_2, all_12_3_13) = 0) | ( ~ (all_12_0_10 = 0) & big_g(all_0_3_3, all_12_3_13) = all_12_0_10) % 3.65/1.71 | (14) all_0_0_0 = 0 % 3.65/1.71 | (15) big_f(all_0_2_2, all_0_3_3) = all_12_4_14 % 3.65/1.71 | (16) big_f(all_0_3_3, all_0_3_3) = all_12_5_15 % 3.65/1.71 | (17) ~ (all_12_4_14 = 0) | ~ (all_12_5_15 = 0) % 3.65/1.71 | (18) big_f(all_0_2_2, all_0_2_2) = all_12_6_16 % 3.65/1.71 | (19) all_12_6_16 = 0 | (((all_12_1_11 = 0 & big_g(all_0_2_2, all_12_3_13) = 0) | (all_12_2_12 = 0 & big_g(all_0_2_2, all_12_3_13) = 0)) & (( ~ (all_12_1_11 = 0) & big_g(all_0_2_2, all_12_3_13) = all_12_1_11) | ( ~ (all_12_2_12 = 0) & big_g(all_0_2_2, all_12_3_13) = all_12_2_12))) % 3.65/1.72 | % 3.65/1.72 | From (11) and (4) follows: % 3.65/1.72 | (20) big_f(all_0_3_3, all_0_2_2) = 0 % 3.65/1.72 | % 3.65/1.72 | Instantiating formula (6) with all_12_6_16, all_0_2_2, all_0_2_2 and discharging atoms big_f(all_0_2_2, all_0_2_2) = all_12_6_16, yields: % 3.65/1.72 | (21) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (all_0_0_0 = 0 & all_0_1_1 = 0 & big_f(all_0_2_2, all_0_2_2) = v2 & big_f(all_0_2_2, all_0_2_2) = v0 & big_f(all_0_3_3, all_0_2_2) = v1 & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (all_12_6_16 = 0)) & ( ~ (all_12_6_16 = 0) | v0 = 0 | (((v5 = 0 & big_g(all_0_2_2, v3) = 0) | (v4 = 0 & big_g(all_0_2_2, v3) = 0)) & (( ~ (v5 = 0) & big_g(all_0_2_2, v3) = v5) | ( ~ (v4 = 0) & big_g(all_0_2_2, v3) = v4)))) & ((v6 = 0 & big_g(all_0_2_2, v3) = 0) | ( ~ (v4 = 0) & big_g(all_0_2_2, v3) = v4)) & ((v4 = 0 & big_g(all_0_2_2, v3) = 0) | ( ~ (v6 = 0) & big_g(all_0_2_2, v3) = v6))) % 3.65/1.72 | % 3.65/1.72 | Instantiating formula (6) with all_12_4_14, all_0_3_3, all_0_2_2 and discharging atoms big_f(all_0_2_2, all_0_3_3) = all_12_4_14, yields: % 3.65/1.72 | (22) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (all_0_0_0 = 0 & all_0_1_1 = 0 & big_f(all_0_2_2, all_0_2_2) = v2 & big_f(all_0_2_2, all_0_3_3) = v0 & big_f(all_0_3_3, all_0_2_2) = v1 & ( ~ (v2 = 0) | ~ (v1 = 0) | ~ (all_12_4_14 = 0)) & ( ~ (all_12_4_14 = 0) | v0 = 0 | (((v5 = 0 & big_g(all_0_3_3, v3) = 0) | (v4 = 0 & big_g(all_0_2_2, v3) = 0)) & (( ~ (v5 = 0) & big_g(all_0_3_3, v3) = v5) | ( ~ (v4 = 0) & big_g(all_0_2_2, v3) = v4)))) & ((v6 = 0 & big_g(all_0_2_2, v3) = 0) | ( ~ (v4 = 0) & big_g(all_0_2_2, v3) = v4)) & ((v4 = 0 & big_g(all_0_2_2, v3) = 0) | ( ~ (v6 = 0) & big_g(all_0_2_2, v3) = v6))) % 3.65/1.72 | % 3.65/1.72 | Instantiating formula (6) with 0, all_0_2_2, all_0_3_3 and discharging atoms big_f(all_0_3_3, all_0_2_2) = 0, yields: % 3.65/1.72 | (9) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : (all_0_0_0 = 0 & all_0_1_1 = 0 & big_f(all_0_2_2, all_0_2_2) = v0 & big_f(all_0_2_2, all_0_3_3) = v2 & big_f(all_0_3_3, all_0_3_3) = v1 & ( ~ (v2 = 0) | ~ (v1 = 0)) & (v0 = 0 | (((v5 = 0 & big_g(all_0_2_2, v3) = 0) | (v4 = 0 & big_g(all_0_2_2, v3) = 0)) & (( ~ (v5 = 0) & big_g(all_0_2_2, v3) = v5) | ( ~ (v4 = 0) & big_g(all_0_2_2, v3) = v4)))) & ((v6 = 0 & big_g(all_0_3_3, v3) = 0) | ( ~ (v4 = 0) & big_g(all_0_2_2, v3) = v4)) & ((v4 = 0 & big_g(all_0_2_2, v3) = 0) | ( ~ (v6 = 0) & big_g(all_0_3_3, v3) = v6))) % 3.65/1.72 | % 3.65/1.72 | Instantiating (9) with all_21_0_24, all_21_1_25, all_21_2_26, all_21_3_27, all_21_4_28, all_21_5_29, all_21_6_30 yields: % 3.65/1.72 | (24) all_0_0_0 = 0 & all_0_1_1 = 0 & big_f(all_0_2_2, all_0_2_2) = all_21_6_30 & big_f(all_0_2_2, all_0_3_3) = all_21_4_28 & big_f(all_0_3_3, all_0_3_3) = all_21_5_29 & ( ~ (all_21_4_28 = 0) | ~ (all_21_5_29 = 0)) & (all_21_6_30 = 0 | (((all_21_1_25 = 0 & big_g(all_0_2_2, all_21_3_27) = 0) | (all_21_2_26 = 0 & big_g(all_0_2_2, all_21_3_27) = 0)) & (( ~ (all_21_1_25 = 0) & big_g(all_0_2_2, all_21_3_27) = all_21_1_25) | ( ~ (all_21_2_26 = 0) & big_g(all_0_2_2, all_21_3_27) = all_21_2_26)))) & ((all_21_0_24 = 0 & big_g(all_0_3_3, all_21_3_27) = 0) | ( ~ (all_21_2_26 = 0) & big_g(all_0_2_2, all_21_3_27) = all_21_2_26)) & ((all_21_2_26 = 0 & big_g(all_0_2_2, all_21_3_27) = 0) | ( ~ (all_21_0_24 = 0) & big_g(all_0_3_3, all_21_3_27) = all_21_0_24)) % 3.65/1.73 | % 3.65/1.73 | Applying alpha-rule on (24) yields: % 3.65/1.73 | (25) big_f(all_0_2_2, all_0_2_2) = all_21_6_30 % 3.65/1.73 | (11) all_0_1_1 = 0 % 3.65/1.73 | (27) big_f(all_0_2_2, all_0_3_3) = all_21_4_28 % 3.65/1.73 | (28) (all_21_2_26 = 0 & big_g(all_0_2_2, all_21_3_27) = 0) | ( ~ (all_21_0_24 = 0) & big_g(all_0_3_3, all_21_3_27) = all_21_0_24) % 3.65/1.73 | (14) all_0_0_0 = 0 % 3.65/1.73 | (30) ~ (all_21_4_28 = 0) | ~ (all_21_5_29 = 0) % 3.65/1.73 | (31) big_f(all_0_3_3, all_0_3_3) = all_21_5_29 % 3.65/1.73 | (32) (all_21_0_24 = 0 & big_g(all_0_3_3, all_21_3_27) = 0) | ( ~ (all_21_2_26 = 0) & big_g(all_0_2_2, all_21_3_27) = all_21_2_26) % 3.65/1.73 | (33) all_21_6_30 = 0 | (((all_21_1_25 = 0 & big_g(all_0_2_2, all_21_3_27) = 0) | (all_21_2_26 = 0 & big_g(all_0_2_2, all_21_3_27) = 0)) & (( ~ (all_21_1_25 = 0) & big_g(all_0_2_2, all_21_3_27) = all_21_1_25) | ( ~ (all_21_2_26 = 0) & big_g(all_0_2_2, all_21_3_27) = all_21_2_26))) % 3.87/1.73 | % 3.87/1.73 | Instantiating (22) with all_23_0_31, all_23_1_32, all_23_2_33, all_23_3_34, all_23_4_35, all_23_5_36, all_23_6_37 yields: % 3.87/1.73 | (34) all_0_0_0 = 0 & all_0_1_1 = 0 & big_f(all_0_2_2, all_0_2_2) = all_23_4_35 & big_f(all_0_2_2, all_0_3_3) = all_23_6_37 & big_f(all_0_3_3, all_0_2_2) = all_23_5_36 & ( ~ (all_23_4_35 = 0) | ~ (all_23_5_36 = 0) | ~ (all_12_4_14 = 0)) & ( ~ (all_12_4_14 = 0) | all_23_6_37 = 0 | (((all_23_1_32 = 0 & big_g(all_0_3_3, all_23_3_34) = 0) | (all_23_2_33 = 0 & big_g(all_0_2_2, all_23_3_34) = 0)) & (( ~ (all_23_1_32 = 0) & big_g(all_0_3_3, all_23_3_34) = all_23_1_32) | ( ~ (all_23_2_33 = 0) & big_g(all_0_2_2, all_23_3_34) = all_23_2_33)))) & ((all_23_0_31 = 0 & big_g(all_0_2_2, all_23_3_34) = 0) | ( ~ (all_23_2_33 = 0) & big_g(all_0_2_2, all_23_3_34) = all_23_2_33)) & ((all_23_2_33 = 0 & big_g(all_0_2_2, all_23_3_34) = 0) | ( ~ (all_23_0_31 = 0) & big_g(all_0_2_2, all_23_3_34) = all_23_0_31)) % 3.87/1.73 | % 3.87/1.73 | Applying alpha-rule on (34) yields: % 3.87/1.73 | (35) big_f(all_0_3_3, all_0_2_2) = all_23_5_36 % 3.87/1.73 | (11) all_0_1_1 = 0 % 3.87/1.73 | (14) all_0_0_0 = 0 % 3.87/1.73 | (38) big_f(all_0_2_2, all_0_2_2) = all_23_4_35 % 3.87/1.73 | (39) ~ (all_12_4_14 = 0) | all_23_6_37 = 0 | (((all_23_1_32 = 0 & big_g(all_0_3_3, all_23_3_34) = 0) | (all_23_2_33 = 0 & big_g(all_0_2_2, all_23_3_34) = 0)) & (( ~ (all_23_1_32 = 0) & big_g(all_0_3_3, all_23_3_34) = all_23_1_32) | ( ~ (all_23_2_33 = 0) & big_g(all_0_2_2, all_23_3_34) = all_23_2_33))) % 3.87/1.73 | (40) ~ (all_23_4_35 = 0) | ~ (all_23_5_36 = 0) | ~ (all_12_4_14 = 0) % 3.87/1.73 | (41) (all_23_0_31 = 0 & big_g(all_0_2_2, all_23_3_34) = 0) | ( ~ (all_23_2_33 = 0) & big_g(all_0_2_2, all_23_3_34) = all_23_2_33) % 3.87/1.73 | (42) (all_23_2_33 = 0 & big_g(all_0_2_2, all_23_3_34) = 0) | ( ~ (all_23_0_31 = 0) & big_g(all_0_2_2, all_23_3_34) = all_23_0_31) % 3.87/1.73 | (43) big_f(all_0_2_2, all_0_3_3) = all_23_6_37 % 3.87/1.73 | % 3.87/1.73 | Instantiating (21) with all_25_0_38, all_25_1_39, all_25_2_40, all_25_3_41, all_25_4_42, all_25_5_43, all_25_6_44 yields: % 3.87/1.73 | (44) all_0_0_0 = 0 & all_0_1_1 = 0 & big_f(all_0_2_2, all_0_2_2) = all_25_4_42 & big_f(all_0_2_2, all_0_2_2) = all_25_6_44 & big_f(all_0_3_3, all_0_2_2) = all_25_5_43 & ( ~ (all_25_4_42 = 0) | ~ (all_25_5_43 = 0) | ~ (all_12_6_16 = 0)) & ( ~ (all_12_6_16 = 0) | all_25_6_44 = 0 | (((all_25_1_39 = 0 & big_g(all_0_2_2, all_25_3_41) = 0) | (all_25_2_40 = 0 & big_g(all_0_2_2, all_25_3_41) = 0)) & (( ~ (all_25_1_39 = 0) & big_g(all_0_2_2, all_25_3_41) = all_25_1_39) | ( ~ (all_25_2_40 = 0) & big_g(all_0_2_2, all_25_3_41) = all_25_2_40)))) & ((all_25_0_38 = 0 & big_g(all_0_2_2, all_25_3_41) = 0) | ( ~ (all_25_2_40 = 0) & big_g(all_0_2_2, all_25_3_41) = all_25_2_40)) & ((all_25_2_40 = 0 & big_g(all_0_2_2, all_25_3_41) = 0) | ( ~ (all_25_0_38 = 0) & big_g(all_0_2_2, all_25_3_41) = all_25_0_38)) % 3.87/1.73 | % 3.87/1.73 | Applying alpha-rule on (44) yields: % 3.87/1.73 | (11) all_0_1_1 = 0 % 3.87/1.73 | (46) (all_25_2_40 = 0 & big_g(all_0_2_2, all_25_3_41) = 0) | ( ~ (all_25_0_38 = 0) & big_g(all_0_2_2, all_25_3_41) = all_25_0_38) % 3.87/1.74 | (47) big_f(all_0_3_3, all_0_2_2) = all_25_5_43 % 3.87/1.74 | (48) ~ (all_12_6_16 = 0) | all_25_6_44 = 0 | (((all_25_1_39 = 0 & big_g(all_0_2_2, all_25_3_41) = 0) | (all_25_2_40 = 0 & big_g(all_0_2_2, all_25_3_41) = 0)) & (( ~ (all_25_1_39 = 0) & big_g(all_0_2_2, all_25_3_41) = all_25_1_39) | ( ~ (all_25_2_40 = 0) & big_g(all_0_2_2, all_25_3_41) = all_25_2_40))) % 3.87/1.74 | (14) all_0_0_0 = 0 % 3.87/1.74 | (50) ~ (all_25_4_42 = 0) | ~ (all_25_5_43 = 0) | ~ (all_12_6_16 = 0) % 3.87/1.74 | (51) (all_25_0_38 = 0 & big_g(all_0_2_2, all_25_3_41) = 0) | ( ~ (all_25_2_40 = 0) & big_g(all_0_2_2, all_25_3_41) = all_25_2_40) % 3.87/1.74 | (52) big_f(all_0_2_2, all_0_2_2) = all_25_6_44 % 3.87/1.74 | (53) big_f(all_0_2_2, all_0_2_2) = all_25_4_42 % 3.87/1.74 | % 3.87/1.74 | Instantiating formula (8) with all_0_2_2, all_0_2_2, all_25_6_44, all_12_6_16 and discharging atoms big_f(all_0_2_2, all_0_2_2) = all_25_6_44, big_f(all_0_2_2, all_0_2_2) = all_12_6_16, yields: % 3.87/1.74 | (54) all_25_6_44 = all_12_6_16 % 3.87/1.74 | % 3.87/1.74 | Instantiating formula (8) with all_0_2_2, all_0_2_2, all_25_6_44, all_25_4_42 and discharging atoms big_f(all_0_2_2, all_0_2_2) = all_25_4_42, big_f(all_0_2_2, all_0_2_2) = all_25_6_44, yields: % 3.87/1.74 | (55) all_25_4_42 = all_25_6_44 % 3.87/1.74 | % 3.87/1.74 | Instantiating formula (8) with all_0_2_2, all_0_2_2, all_23_4_35, all_25_6_44 and discharging atoms big_f(all_0_2_2, all_0_2_2) = all_25_6_44, big_f(all_0_2_2, all_0_2_2) = all_23_4_35, yields: % 3.87/1.74 | (56) all_25_6_44 = all_23_4_35 % 3.87/1.74 | % 3.87/1.74 | Instantiating formula (8) with all_0_2_2, all_0_2_2, all_21_6_30, all_25_4_42 and discharging atoms big_f(all_0_2_2, all_0_2_2) = all_25_4_42, big_f(all_0_2_2, all_0_2_2) = all_21_6_30, yields: % 3.87/1.74 | (57) all_25_4_42 = all_21_6_30 % 3.87/1.74 | % 3.87/1.74 | Instantiating formula (8) with all_0_3_3, all_0_2_2, all_25_5_43, 0 and discharging atoms big_f(all_0_3_3, all_0_2_2) = all_25_5_43, big_f(all_0_3_3, all_0_2_2) = 0, yields: % 3.87/1.74 | (58) all_25_5_43 = 0 % 3.87/1.74 | % 3.87/1.74 | Combining equations (55,57) yields a new equation: % 3.87/1.74 | (59) all_25_6_44 = all_21_6_30 % 3.87/1.74 | % 3.87/1.74 | Simplifying 59 yields: % 3.87/1.74 | (60) all_25_6_44 = all_21_6_30 % 3.87/1.74 | % 3.87/1.74 | Combining equations (60,56) yields a new equation: % 3.87/1.74 | (61) all_23_4_35 = all_21_6_30 % 3.87/1.74 | % 3.87/1.74 | Combining equations (54,56) yields a new equation: % 3.87/1.74 | (62) all_23_4_35 = all_12_6_16 % 3.87/1.74 | % 3.87/1.74 | Combining equations (62,61) yields a new equation: % 3.87/1.74 | (63) all_21_6_30 = all_12_6_16 % 3.87/1.74 | % 3.87/1.74 | Combining equations (63,57) yields a new equation: % 3.87/1.74 | (64) all_25_4_42 = all_12_6_16 % 3.87/1.74 | % 3.87/1.74 +-Applying beta-rule and splitting (50), into two cases. % 3.87/1.74 |-Branch one: % 3.87/1.74 | (65) ~ (all_25_4_42 = 0) % 3.87/1.74 | % 3.87/1.74 | Equations (64) can reduce 65 to: % 3.87/1.74 | (66) ~ (all_12_6_16 = 0) % 3.87/1.74 | % 3.87/1.74 +-Applying beta-rule and splitting (12), into two cases. % 3.87/1.74 |-Branch one: % 3.87/1.74 | (67) all_12_0_10 = 0 & big_g(all_0_3_3, all_12_3_13) = 0 % 3.87/1.74 | % 3.87/1.74 | Applying alpha-rule on (67) yields: % 3.87/1.74 | (68) all_12_0_10 = 0 % 3.87/1.74 | (69) big_g(all_0_3_3, all_12_3_13) = 0 % 3.87/1.74 | % 3.87/1.74 +-Applying beta-rule and splitting (13), into two cases. % 3.87/1.74 |-Branch one: % 3.87/1.74 | (70) all_12_2_12 = 0 & big_g(all_0_2_2, all_12_3_13) = 0 % 3.87/1.74 | % 3.87/1.74 | Applying alpha-rule on (70) yields: % 3.87/1.74 | (71) all_12_2_12 = 0 % 3.87/1.74 | (72) big_g(all_0_2_2, all_12_3_13) = 0 % 3.87/1.74 | % 3.87/1.74 +-Applying beta-rule and splitting (19), into two cases. % 3.87/1.74 |-Branch one: % 3.87/1.74 | (73) all_12_6_16 = 0 % 3.87/1.74 | % 3.87/1.74 | Equations (73) can reduce 66 to: % 3.87/1.74 | (74) $false % 3.87/1.74 | % 3.87/1.74 |-The branch is then unsatisfiable % 3.87/1.74 |-Branch two: % 3.87/1.74 | (66) ~ (all_12_6_16 = 0) % 3.87/1.74 | (76) ((all_12_1_11 = 0 & big_g(all_0_2_2, all_12_3_13) = 0) | (all_12_2_12 = 0 & big_g(all_0_2_2, all_12_3_13) = 0)) & (( ~ (all_12_1_11 = 0) & big_g(all_0_2_2, all_12_3_13) = all_12_1_11) | ( ~ (all_12_2_12 = 0) & big_g(all_0_2_2, all_12_3_13) = all_12_2_12)) % 3.87/1.74 | % 3.87/1.74 | Applying alpha-rule on (76) yields: % 3.87/1.75 | (77) (all_12_1_11 = 0 & big_g(all_0_2_2, all_12_3_13) = 0) | (all_12_2_12 = 0 & big_g(all_0_2_2, all_12_3_13) = 0) % 3.87/1.75 | (78) ( ~ (all_12_1_11 = 0) & big_g(all_0_2_2, all_12_3_13) = all_12_1_11) | ( ~ (all_12_2_12 = 0) & big_g(all_0_2_2, all_12_3_13) = all_12_2_12) % 3.87/1.75 | % 3.87/1.75 +-Applying beta-rule and splitting (78), into two cases. % 3.87/1.75 |-Branch one: % 3.87/1.75 | (79) ~ (all_12_1_11 = 0) & big_g(all_0_2_2, all_12_3_13) = all_12_1_11 % 3.87/1.75 | % 3.87/1.75 | Applying alpha-rule on (79) yields: % 3.87/1.75 | (80) ~ (all_12_1_11 = 0) % 3.87/1.75 | (81) big_g(all_0_2_2, all_12_3_13) = all_12_1_11 % 3.95/1.75 | % 3.95/1.75 | Instantiating formula (7) with all_0_2_2, all_12_3_13, 0, all_12_1_11 and discharging atoms big_g(all_0_2_2, all_12_3_13) = all_12_1_11, big_g(all_0_2_2, all_12_3_13) = 0, yields: % 3.95/1.75 | (82) all_12_1_11 = 0 % 3.95/1.75 | % 3.95/1.75 | Equations (82) can reduce 80 to: % 3.95/1.75 | (74) $false % 3.95/1.75 | % 3.95/1.75 |-The branch is then unsatisfiable % 3.95/1.75 |-Branch two: % 3.95/1.75 | (84) ~ (all_12_2_12 = 0) & big_g(all_0_2_2, all_12_3_13) = all_12_2_12 % 3.95/1.75 | % 3.95/1.75 | Applying alpha-rule on (84) yields: % 3.95/1.75 | (85) ~ (all_12_2_12 = 0) % 3.95/1.75 | (86) big_g(all_0_2_2, all_12_3_13) = all_12_2_12 % 3.95/1.75 | % 3.95/1.75 | Equations (71) can reduce 85 to: % 3.95/1.75 | (74) $false % 3.95/1.75 | % 3.95/1.75 |-The branch is then unsatisfiable % 3.95/1.75 |-Branch two: % 3.95/1.75 | (88) ~ (all_12_0_10 = 0) & big_g(all_0_3_3, all_12_3_13) = all_12_0_10 % 3.95/1.75 | % 3.95/1.75 | Applying alpha-rule on (88) yields: % 3.95/1.75 | (89) ~ (all_12_0_10 = 0) % 3.95/1.75 | (90) big_g(all_0_3_3, all_12_3_13) = all_12_0_10 % 3.95/1.75 | % 3.95/1.75 | Equations (68) can reduce 89 to: % 3.95/1.75 | (74) $false % 3.95/1.75 | % 3.95/1.75 |-The branch is then unsatisfiable % 3.95/1.75 |-Branch two: % 3.95/1.75 | (84) ~ (all_12_2_12 = 0) & big_g(all_0_2_2, all_12_3_13) = all_12_2_12 % 3.95/1.75 | % 3.95/1.75 | Applying alpha-rule on (84) yields: % 3.95/1.75 | (85) ~ (all_12_2_12 = 0) % 3.95/1.75 | (86) big_g(all_0_2_2, all_12_3_13) = all_12_2_12 % 3.95/1.75 | % 3.95/1.75 +-Applying beta-rule and splitting (19), into two cases. % 3.95/1.75 |-Branch one: % 3.95/1.75 | (73) all_12_6_16 = 0 % 3.95/1.75 | % 3.95/1.75 | Equations (73) can reduce 66 to: % 3.95/1.75 | (74) $false % 3.95/1.75 | % 3.95/1.75 |-The branch is then unsatisfiable % 3.95/1.75 |-Branch two: % 3.95/1.75 | (66) ~ (all_12_6_16 = 0) % 3.95/1.75 | (76) ((all_12_1_11 = 0 & big_g(all_0_2_2, all_12_3_13) = 0) | (all_12_2_12 = 0 & big_g(all_0_2_2, all_12_3_13) = 0)) & (( ~ (all_12_1_11 = 0) & big_g(all_0_2_2, all_12_3_13) = all_12_1_11) | ( ~ (all_12_2_12 = 0) & big_g(all_0_2_2, all_12_3_13) = all_12_2_12)) % 3.95/1.75 | % 3.95/1.75 | Applying alpha-rule on (76) yields: % 3.95/1.75 | (77) (all_12_1_11 = 0 & big_g(all_0_2_2, all_12_3_13) = 0) | (all_12_2_12 = 0 & big_g(all_0_2_2, all_12_3_13) = 0) % 3.95/1.75 | (78) ( ~ (all_12_1_11 = 0) & big_g(all_0_2_2, all_12_3_13) = all_12_1_11) | ( ~ (all_12_2_12 = 0) & big_g(all_0_2_2, all_12_3_13) = all_12_2_12) % 3.95/1.75 | % 3.95/1.75 +-Applying beta-rule and splitting (77), into two cases. % 3.95/1.75 |-Branch one: % 3.95/1.75 | (101) all_12_1_11 = 0 & big_g(all_0_2_2, all_12_3_13) = 0 % 3.95/1.75 | % 3.95/1.75 | Applying alpha-rule on (101) yields: % 3.95/1.75 | (82) all_12_1_11 = 0 % 3.95/1.75 | (72) big_g(all_0_2_2, all_12_3_13) = 0 % 3.95/1.75 | % 3.95/1.75 | Instantiating formula (7) with all_0_2_2, all_12_3_13, 0, all_12_2_12 and discharging atoms big_g(all_0_2_2, all_12_3_13) = all_12_2_12, big_g(all_0_2_2, all_12_3_13) = 0, yields: % 3.95/1.75 | (71) all_12_2_12 = 0 % 3.95/1.75 | % 3.95/1.75 | Equations (71) can reduce 85 to: % 3.95/1.75 | (74) $false % 3.95/1.75 | % 3.95/1.75 |-The branch is then unsatisfiable % 3.95/1.75 |-Branch two: % 3.95/1.75 | (70) all_12_2_12 = 0 & big_g(all_0_2_2, all_12_3_13) = 0 % 3.95/1.75 | % 3.95/1.75 | Applying alpha-rule on (70) yields: % 3.95/1.75 | (71) all_12_2_12 = 0 % 3.95/1.75 | (72) big_g(all_0_2_2, all_12_3_13) = 0 % 3.95/1.75 | % 3.95/1.75 | Equations (71) can reduce 85 to: % 3.95/1.75 | (74) $false % 3.95/1.75 | % 3.95/1.75 |-The branch is then unsatisfiable % 3.95/1.75 |-Branch two: % 3.95/1.75 | (110) all_25_4_42 = 0 % 3.95/1.75 | (111) ~ (all_25_5_43 = 0) | ~ (all_12_6_16 = 0) % 3.95/1.76 | % 3.95/1.76 | Combining equations (110,64) yields a new equation: % 3.95/1.76 | (73) all_12_6_16 = 0 % 3.95/1.76 | % 3.95/1.76 +-Applying beta-rule and splitting (111), into two cases. % 3.95/1.76 |-Branch one: % 3.95/1.76 | (113) ~ (all_25_5_43 = 0) % 3.95/1.76 | % 3.95/1.76 | Equations (58) can reduce 113 to: % 3.95/1.76 | (74) $false % 3.95/1.76 | % 3.95/1.76 |-The branch is then unsatisfiable % 3.95/1.76 |-Branch two: % 3.95/1.76 | (58) all_25_5_43 = 0 % 3.95/1.76 | (66) ~ (all_12_6_16 = 0) % 3.95/1.76 | % 3.95/1.76 | Equations (73) can reduce 66 to: % 3.95/1.76 | (74) $false % 3.95/1.76 | % 3.95/1.76 |-The branch is then unsatisfiable % 3.95/1.76 % SZS output end Proof for theBenchmark % 3.95/1.76 % 3.95/1.76 1137ms %------------------------------------------------------------------------------