%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SYN333+1 : TPTP v8.1.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n020.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:29 EDT 2022 % Result : Theorem 3.21s 1.47s % Output : Proof 4.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SYN333+1 : TPTP v8.1.0. Released v2.0.0. % 0.10/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.13/0.34 % Computer : n020.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Mon Jul 11 18:32:12 EDT 2022 % 0.13/0.34 % CPUTime : % 0.61/0.60 ____ _ % 0.61/0.60 ___ / __ \_____(_)___ ________ __________ % 0.61/0.60 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.61/0.60 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.61/0.60 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.61/0.60 % 0.61/0.60 A Theorem Prover for First-Order Logic % 0.61/0.60 (ePrincess v.1.0) % 0.61/0.60 % 0.61/0.60 (c) Philipp Rümmer, 2009-2015 % 0.61/0.60 (c) Peter Backeman, 2014-2015 % 0.61/0.60 (contributions by Angelo Brillout, Peter Baumgartner) % 0.61/0.60 Free software under GNU Lesser General Public License (LGPL). % 0.61/0.60 Bug reports to peter@backeman.se % 0.61/0.60 % 0.61/0.60 For more information, visit http://user.uu.se/~petba168/breu/ % 0.61/0.60 % 0.61/0.60 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.66/0.67 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.26/0.88 Prover 0: Preprocessing ... % 1.38/0.93 Prover 0: Warning: ignoring some quantifiers % 1.38/0.94 Prover 0: Constructing countermodel ... % 1.57/1.04 Prover 0: gave up % 1.57/1.04 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 1.57/1.05 Prover 1: Preprocessing ... % 1.90/1.10 Prover 1: Constructing countermodel ... % 1.90/1.10 Prover 1: gave up % 1.90/1.10 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.90/1.12 Prover 2: Preprocessing ... % 1.90/1.17 Prover 2: Warning: ignoring some quantifiers % 1.90/1.18 Prover 2: Constructing countermodel ... % 2.32/1.20 Prover 2: gave up % 2.32/1.20 Prover 3: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 2.32/1.21 Prover 3: Preprocessing ... % 2.32/1.22 Prover 3: Warning: ignoring some quantifiers % 2.32/1.22 Prover 3: Constructing countermodel ... % 2.44/1.24 Prover 3: gave up % 2.44/1.25 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=complete % 2.44/1.25 Prover 4: Preprocessing ... % 2.44/1.29 Prover 4: Warning: ignoring some quantifiers % 2.44/1.29 Prover 4: Constructing countermodel ... % 3.21/1.47 Prover 4: proved (225ms) % 3.21/1.47 % 3.21/1.47 No countermodel exists, formula is valid % 3.21/1.47 % SZS status Theorem for theBenchmark % 3.21/1.47 % 3.21/1.47 Generating proof ... Warning: ignoring some quantifiers % 4.41/1.73 found it (size 53) % 4.41/1.73 % 4.41/1.73 % SZS output start Proof for theBenchmark % 4.41/1.73 Assumed formulas after preprocessing and simplification: % 4.41/1.73 | (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] : (v2 = 0 & big_f(v4, v4) = v6 & big_f(v1, v4) = v5 & big_g(v4, v4) = v8 & big_g(v0, v4) = v7 & big_g(v0, v1) = v3 & ( ~ (v6 = 0) | ~ (v5 = 0) | (v3 = 0 & ( ~ (v8 = 0) | ~ (v7 = 0)))))) & ! [v0] : ! [v1] : ! [v2] : ( ~ (big_g(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : (big_f(v3, v3) = v5 & big_f(v1, v3) = v4 & big_f(v0, v1) = 0 & big_g(v3, v3) = v7 & big_g(v0, v3) = v6 & ( ~ (v5 = 0) | ~ (v4 = 0) | (v2 = 0 & ( ~ (v7 = 0) | ~ (v6 = 0)))))) & ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : (big_f(v3, v3) = v5 & big_f(v1, v3) = v4 & big_f(v0, v1) = 0 & big_g(v3, v3) = v7 & big_g(v0, v3) = v6 & big_g(v0, v1) = v2 & ( ~ (v5 = 0) | ~ (v4 = 0) | (v2 = 0 & ( ~ (v7 = 0) | ~ (v6 = 0))))) % 4.41/1.76 | Applying alpha-rule on (0) yields: % 4.41/1.76 | (1) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (big_g(v3, v2) = v1) | ~ (big_g(v3, v2) = v0)) % 4.41/1.76 | (2) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : (big_f(v3, v3) = v5 & big_f(v1, v3) = v4 & big_f(v0, v1) = 0 & big_g(v3, v3) = v7 & big_g(v0, v3) = v6 & big_g(v0, v1) = v2 & ( ~ (v5 = 0) | ~ (v4 = 0) | (v2 = 0 & ( ~ (v7 = 0) | ~ (v6 = 0))))) % 4.41/1.76 | (3) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (big_f(v3, v2) = v1) | ~ (big_f(v3, v2) = v0)) % 4.41/1.76 | (4) ! [v0] : ! [v1] : ! [v2] : ( ~ (big_g(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : (big_f(v3, v3) = v5 & big_f(v1, v3) = v4 & big_f(v0, v1) = 0 & big_g(v3, v3) = v7 & big_g(v0, v3) = v6 & ( ~ (v5 = 0) | ~ (v4 = 0) | (v2 = 0 & ( ~ (v7 = 0) | ~ (v6 = 0)))))) % 4.41/1.76 | (5) ! [v0] : ! [v1] : ! [v2] : ( ~ (big_f(v0, v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : (v2 = 0 & big_f(v4, v4) = v6 & big_f(v1, v4) = v5 & big_g(v4, v4) = v8 & big_g(v0, v4) = v7 & big_g(v0, v1) = v3 & ( ~ (v6 = 0) | ~ (v5 = 0) | (v3 = 0 & ( ~ (v8 = 0) | ~ (v7 = 0)))))) % 4.41/1.77 | % 4.41/1.77 | 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 yields: % 4.41/1.77 | (6) big_f(all_1_4_4, all_1_4_4) = all_1_2_2 & big_f(all_1_6_6, all_1_4_4) = all_1_3_3 & big_f(all_1_7_7, all_1_6_6) = 0 & big_g(all_1_4_4, all_1_4_4) = all_1_0_0 & big_g(all_1_7_7, all_1_4_4) = all_1_1_1 & big_g(all_1_7_7, all_1_6_6) = all_1_5_5 & ( ~ (all_1_2_2 = 0) | ~ (all_1_3_3 = 0) | (all_1_5_5 = 0 & ( ~ (all_1_0_0 = 0) | ~ (all_1_1_1 = 0)))) % 4.41/1.77 | % 4.41/1.77 | Applying alpha-rule on (6) yields: % 4.41/1.77 | (7) ~ (all_1_2_2 = 0) | ~ (all_1_3_3 = 0) | (all_1_5_5 = 0 & ( ~ (all_1_0_0 = 0) | ~ (all_1_1_1 = 0))) % 4.41/1.77 | (8) big_f(all_1_4_4, all_1_4_4) = all_1_2_2 % 4.41/1.77 | (9) big_f(all_1_6_6, all_1_4_4) = all_1_3_3 % 4.41/1.77 | (10) big_g(all_1_4_4, all_1_4_4) = all_1_0_0 % 4.41/1.77 | (11) big_f(all_1_7_7, all_1_6_6) = 0 % 4.41/1.77 | (12) big_g(all_1_7_7, all_1_6_6) = all_1_5_5 % 4.41/1.77 | (13) big_g(all_1_7_7, all_1_4_4) = all_1_1_1 % 4.41/1.77 | % 4.41/1.77 | Instantiating formula (5) with all_1_2_2, all_1_4_4, all_1_4_4 and discharging atoms big_f(all_1_4_4, all_1_4_4) = all_1_2_2, yields: % 4.41/1.77 | (14) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : (all_1_2_2 = 0 & big_f(v1, v1) = v3 & big_f(all_1_4_4, v1) = v2 & big_g(v1, v1) = v5 & big_g(all_1_4_4, v1) = v4 & big_g(all_1_4_4, all_1_4_4) = v0 & ( ~ (v3 = 0) | ~ (v2 = 0) | (v0 = 0 & ( ~ (v5 = 0) | ~ (v4 = 0))))) % 4.41/1.77 | % 4.41/1.77 | Instantiating formula (5) with all_1_3_3, all_1_4_4, all_1_6_6 and discharging atoms big_f(all_1_6_6, all_1_4_4) = all_1_3_3, yields: % 4.41/1.77 | (15) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : (all_1_3_3 = 0 & big_f(v1, v1) = v3 & big_f(all_1_4_4, v1) = v2 & big_g(v1, v1) = v5 & big_g(all_1_6_6, v1) = v4 & big_g(all_1_6_6, all_1_4_4) = v0 & ( ~ (v3 = 0) | ~ (v2 = 0) | (v0 = 0 & ( ~ (v5 = 0) | ~ (v4 = 0))))) % 4.41/1.77 | % 4.41/1.77 | Instantiating formula (4) with all_1_1_1, all_1_4_4, all_1_7_7 and discharging atoms big_g(all_1_7_7, all_1_4_4) = all_1_1_1, yields: % 4.41/1.77 | (16) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : (big_f(v0, v0) = v2 & big_f(all_1_4_4, v0) = v1 & big_f(all_1_7_7, all_1_4_4) = 0 & big_g(v0, v0) = v4 & big_g(all_1_7_7, v0) = v3 & ( ~ (v2 = 0) | ~ (v1 = 0) | (all_1_1_1 = 0 & ( ~ (v4 = 0) | ~ (v3 = 0))))) % 4.41/1.78 | % 4.41/1.78 | Instantiating (15) with all_12_0_19, all_12_1_20, all_12_2_21, all_12_3_22, all_12_4_23, all_12_5_24 yields: % 4.41/1.78 | (17) all_1_3_3 = 0 & big_f(all_12_4_23, all_12_4_23) = all_12_2_21 & big_f(all_1_4_4, all_12_4_23) = all_12_3_22 & big_g(all_12_4_23, all_12_4_23) = all_12_0_19 & big_g(all_1_6_6, all_12_4_23) = all_12_1_20 & big_g(all_1_6_6, all_1_4_4) = all_12_5_24 & ( ~ (all_12_2_21 = 0) | ~ (all_12_3_22 = 0) | (all_12_5_24 = 0 & ( ~ (all_12_0_19 = 0) | ~ (all_12_1_20 = 0)))) % 4.41/1.78 | % 4.41/1.78 | Applying alpha-rule on (17) yields: % 4.41/1.78 | (18) big_g(all_1_6_6, all_12_4_23) = all_12_1_20 % 4.41/1.78 | (19) big_f(all_12_4_23, all_12_4_23) = all_12_2_21 % 4.41/1.78 | (20) big_f(all_1_4_4, all_12_4_23) = all_12_3_22 % 4.41/1.78 | (21) all_1_3_3 = 0 % 4.41/1.78 | (22) big_g(all_12_4_23, all_12_4_23) = all_12_0_19 % 4.41/1.78 | (23) ~ (all_12_2_21 = 0) | ~ (all_12_3_22 = 0) | (all_12_5_24 = 0 & ( ~ (all_12_0_19 = 0) | ~ (all_12_1_20 = 0))) % 4.41/1.78 | (24) big_g(all_1_6_6, all_1_4_4) = all_12_5_24 % 4.41/1.78 | % 4.41/1.78 | Instantiating (16) with all_14_0_25, all_14_1_26, all_14_2_27, all_14_3_28, all_14_4_29 yields: % 4.41/1.78 | (25) big_f(all_14_4_29, all_14_4_29) = all_14_2_27 & big_f(all_1_4_4, all_14_4_29) = all_14_3_28 & big_f(all_1_7_7, all_1_4_4) = 0 & big_g(all_14_4_29, all_14_4_29) = all_14_0_25 & big_g(all_1_7_7, all_14_4_29) = all_14_1_26 & ( ~ (all_14_2_27 = 0) | ~ (all_14_3_28 = 0) | (all_1_1_1 = 0 & ( ~ (all_14_0_25 = 0) | ~ (all_14_1_26 = 0)))) % 4.41/1.78 | % 4.41/1.78 | Applying alpha-rule on (25) yields: % 4.41/1.78 | (26) big_f(all_1_4_4, all_14_4_29) = all_14_3_28 % 4.41/1.78 | (27) big_f(all_14_4_29, all_14_4_29) = all_14_2_27 % 4.41/1.78 | (28) big_f(all_1_7_7, all_1_4_4) = 0 % 4.41/1.78 | (29) ~ (all_14_2_27 = 0) | ~ (all_14_3_28 = 0) | (all_1_1_1 = 0 & ( ~ (all_14_0_25 = 0) | ~ (all_14_1_26 = 0))) % 4.41/1.78 | (30) big_g(all_1_7_7, all_14_4_29) = all_14_1_26 % 4.41/1.78 | (31) big_g(all_14_4_29, all_14_4_29) = all_14_0_25 % 4.41/1.78 | % 4.41/1.78 | Instantiating (14) with all_18_0_35, all_18_1_36, all_18_2_37, all_18_3_38, all_18_4_39, all_18_5_40 yields: % 4.41/1.78 | (32) all_1_2_2 = 0 & big_f(all_18_4_39, all_18_4_39) = all_18_2_37 & big_f(all_1_4_4, all_18_4_39) = all_18_3_38 & big_g(all_18_4_39, all_18_4_39) = all_18_0_35 & big_g(all_1_4_4, all_18_4_39) = all_18_1_36 & big_g(all_1_4_4, all_1_4_4) = all_18_5_40 & ( ~ (all_18_2_37 = 0) | ~ (all_18_3_38 = 0) | (all_18_5_40 = 0 & ( ~ (all_18_0_35 = 0) | ~ (all_18_1_36 = 0)))) % 4.41/1.78 | % 4.41/1.78 | Applying alpha-rule on (32) yields: % 4.41/1.78 | (33) ~ (all_18_2_37 = 0) | ~ (all_18_3_38 = 0) | (all_18_5_40 = 0 & ( ~ (all_18_0_35 = 0) | ~ (all_18_1_36 = 0))) % 4.41/1.78 | (34) big_f(all_18_4_39, all_18_4_39) = all_18_2_37 % 4.41/1.78 | (35) big_f(all_1_4_4, all_18_4_39) = all_18_3_38 % 4.41/1.78 | (36) big_g(all_1_4_4, all_18_4_39) = all_18_1_36 % 4.41/1.79 | (37) all_1_2_2 = 0 % 4.41/1.79 | (38) big_g(all_18_4_39, all_18_4_39) = all_18_0_35 % 4.41/1.79 | (39) big_g(all_1_4_4, all_1_4_4) = all_18_5_40 % 4.41/1.79 | % 4.41/1.79 +-Applying beta-rule and splitting (7), into two cases. % 4.41/1.79 |-Branch one: % 4.41/1.79 | (40) ~ (all_1_2_2 = 0) % 4.41/1.79 | % 4.41/1.79 | Equations (37) can reduce 40 to: % 4.41/1.79 | (41) $false % 4.41/1.79 | % 4.41/1.79 |-The branch is then unsatisfiable % 4.41/1.79 |-Branch two: % 4.41/1.79 | (37) all_1_2_2 = 0 % 4.41/1.79 | (43) ~ (all_1_3_3 = 0) | (all_1_5_5 = 0 & ( ~ (all_1_0_0 = 0) | ~ (all_1_1_1 = 0))) % 4.41/1.79 | % 4.41/1.79 +-Applying beta-rule and splitting (43), into two cases. % 4.41/1.79 |-Branch one: % 4.41/1.79 | (44) ~ (all_1_3_3 = 0) % 4.41/1.79 | % 4.41/1.79 | Equations (21) can reduce 44 to: % 4.41/1.79 | (41) $false % 4.41/1.79 | % 4.41/1.79 |-The branch is then unsatisfiable % 4.41/1.79 |-Branch two: % 4.41/1.79 | (21) all_1_3_3 = 0 % 4.41/1.79 | (47) all_1_5_5 = 0 & ( ~ (all_1_0_0 = 0) | ~ (all_1_1_1 = 0)) % 4.41/1.79 | % 4.41/1.79 | Applying alpha-rule on (47) yields: % 4.41/1.79 | (48) all_1_5_5 = 0 % 4.41/1.79 | (49) ~ (all_1_0_0 = 0) | ~ (all_1_1_1 = 0) % 4.41/1.79 | % 4.41/1.79 | Instantiating formula (1) with all_1_4_4, all_1_4_4, all_18_5_40, all_1_0_0 and discharging atoms big_g(all_1_4_4, all_1_4_4) = all_18_5_40, big_g(all_1_4_4, all_1_4_4) = all_1_0_0, yields: % 4.41/1.79 | (50) all_18_5_40 = all_1_0_0 % 4.41/1.79 | % 4.41/1.79 | Instantiating formula (5) with all_18_2_37, all_18_4_39, all_18_4_39 and discharging atoms big_f(all_18_4_39, all_18_4_39) = all_18_2_37, yields: % 4.41/1.79 | (51) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : (all_18_2_37 = 0 & big_f(v1, v1) = v3 & big_f(all_18_4_39, v1) = v2 & big_g(v1, v1) = v5 & big_g(all_18_4_39, v1) = v4 & big_g(all_18_4_39, all_18_4_39) = v0 & ( ~ (v3 = 0) | ~ (v2 = 0) | (v0 = 0 & ( ~ (v5 = 0) | ~ (v4 = 0))))) % 4.41/1.79 | % 4.41/1.79 | Instantiating formula (5) with all_14_2_27, all_14_4_29, all_14_4_29 and discharging atoms big_f(all_14_4_29, all_14_4_29) = all_14_2_27, yields: % 4.41/1.79 | (52) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : (all_14_2_27 = 0 & big_f(v1, v1) = v3 & big_f(all_14_4_29, v1) = v2 & big_g(v1, v1) = v5 & big_g(all_14_4_29, v1) = v4 & big_g(all_14_4_29, all_14_4_29) = v0 & ( ~ (v3 = 0) | ~ (v2 = 0) | (v0 = 0 & ( ~ (v5 = 0) | ~ (v4 = 0))))) % 4.41/1.79 | % 4.41/1.79 | Instantiating formula (5) with all_18_3_38, all_18_4_39, all_1_4_4 and discharging atoms big_f(all_1_4_4, all_18_4_39) = all_18_3_38, yields: % 4.41/1.80 | (53) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : (all_18_3_38 = 0 & big_f(v1, v1) = v3 & big_f(all_18_4_39, v1) = v2 & big_g(v1, v1) = v5 & big_g(all_1_4_4, v1) = v4 & big_g(all_1_4_4, all_18_4_39) = v0 & ( ~ (v3 = 0) | ~ (v2 = 0) | (v0 = 0 & ( ~ (v5 = 0) | ~ (v4 = 0))))) % 4.70/1.80 | % 4.70/1.80 | Instantiating formula (5) with all_14_3_28, all_14_4_29, all_1_4_4 and discharging atoms big_f(all_1_4_4, all_14_4_29) = all_14_3_28, yields: % 4.70/1.80 | (54) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : (all_14_3_28 = 0 & big_f(v1, v1) = v3 & big_f(all_14_4_29, v1) = v2 & big_g(v1, v1) = v5 & big_g(all_1_4_4, v1) = v4 & big_g(all_1_4_4, all_14_4_29) = v0 & ( ~ (v3 = 0) | ~ (v2 = 0) | (v0 = 0 & ( ~ (v5 = 0) | ~ (v4 = 0))))) % 4.70/1.80 | % 4.70/1.80 | Instantiating (53) with all_63_0_112, all_63_1_113, all_63_2_114, all_63_3_115, all_63_4_116, all_63_5_117 yields: % 4.70/1.80 | (55) all_18_3_38 = 0 & big_f(all_63_4_116, all_63_4_116) = all_63_2_114 & big_f(all_18_4_39, all_63_4_116) = all_63_3_115 & big_g(all_63_4_116, all_63_4_116) = all_63_0_112 & big_g(all_1_4_4, all_63_4_116) = all_63_1_113 & big_g(all_1_4_4, all_18_4_39) = all_63_5_117 & ( ~ (all_63_2_114 = 0) | ~ (all_63_3_115 = 0) | (all_63_5_117 = 0 & ( ~ (all_63_0_112 = 0) | ~ (all_63_1_113 = 0)))) % 4.70/1.80 | % 4.70/1.80 | Applying alpha-rule on (55) yields: % 4.70/1.80 | (56) ~ (all_63_2_114 = 0) | ~ (all_63_3_115 = 0) | (all_63_5_117 = 0 & ( ~ (all_63_0_112 = 0) | ~ (all_63_1_113 = 0))) % 4.70/1.80 | (57) big_f(all_63_4_116, all_63_4_116) = all_63_2_114 % 4.70/1.80 | (58) all_18_3_38 = 0 % 4.70/1.80 | (59) big_g(all_1_4_4, all_63_4_116) = all_63_1_113 % 4.70/1.80 | (60) big_g(all_1_4_4, all_18_4_39) = all_63_5_117 % 4.70/1.80 | (61) big_f(all_18_4_39, all_63_4_116) = all_63_3_115 % 4.70/1.80 | (62) big_g(all_63_4_116, all_63_4_116) = all_63_0_112 % 4.70/1.80 | % 4.70/1.80 | Instantiating (52) with all_67_0_124, all_67_1_125, all_67_2_126, all_67_3_127, all_67_4_128, all_67_5_129 yields: % 4.70/1.80 | (63) all_14_2_27 = 0 & big_f(all_67_4_128, all_67_4_128) = all_67_2_126 & big_f(all_14_4_29, all_67_4_128) = all_67_3_127 & big_g(all_67_4_128, all_67_4_128) = all_67_0_124 & big_g(all_14_4_29, all_67_4_128) = all_67_1_125 & big_g(all_14_4_29, all_14_4_29) = all_67_5_129 & ( ~ (all_67_2_126 = 0) | ~ (all_67_3_127 = 0) | (all_67_5_129 = 0 & ( ~ (all_67_0_124 = 0) | ~ (all_67_1_125 = 0)))) % 4.70/1.80 | % 4.70/1.80 | Applying alpha-rule on (63) yields: % 4.70/1.80 | (64) ~ (all_67_2_126 = 0) | ~ (all_67_3_127 = 0) | (all_67_5_129 = 0 & ( ~ (all_67_0_124 = 0) | ~ (all_67_1_125 = 0))) % 4.70/1.80 | (65) big_g(all_14_4_29, all_67_4_128) = all_67_1_125 % 4.70/1.80 | (66) big_f(all_67_4_128, all_67_4_128) = all_67_2_126 % 4.70/1.80 | (67) big_g(all_14_4_29, all_14_4_29) = all_67_5_129 % 4.70/1.81 | (68) all_14_2_27 = 0 % 4.70/1.81 | (69) big_f(all_14_4_29, all_67_4_128) = all_67_3_127 % 4.70/1.81 | (70) big_g(all_67_4_128, all_67_4_128) = all_67_0_124 % 4.70/1.81 | % 4.70/1.81 | Instantiating (51) with all_71_0_136, all_71_1_137, all_71_2_138, all_71_3_139, all_71_4_140, all_71_5_141 yields: % 4.70/1.81 | (71) all_18_2_37 = 0 & big_f(all_71_4_140, all_71_4_140) = all_71_2_138 & big_f(all_18_4_39, all_71_4_140) = all_71_3_139 & big_g(all_71_4_140, all_71_4_140) = all_71_0_136 & big_g(all_18_4_39, all_71_4_140) = all_71_1_137 & big_g(all_18_4_39, all_18_4_39) = all_71_5_141 & ( ~ (all_71_2_138 = 0) | ~ (all_71_3_139 = 0) | (all_71_5_141 = 0 & ( ~ (all_71_0_136 = 0) | ~ (all_71_1_137 = 0)))) % 4.70/1.81 | % 4.70/1.81 | Applying alpha-rule on (71) yields: % 4.70/1.81 | (72) big_g(all_18_4_39, all_71_4_140) = all_71_1_137 % 4.70/1.81 | (73) all_18_2_37 = 0 % 4.70/1.81 | (74) big_g(all_71_4_140, all_71_4_140) = all_71_0_136 % 4.70/1.81 | (75) big_f(all_71_4_140, all_71_4_140) = all_71_2_138 % 4.70/1.81 | (76) ~ (all_71_2_138 = 0) | ~ (all_71_3_139 = 0) | (all_71_5_141 = 0 & ( ~ (all_71_0_136 = 0) | ~ (all_71_1_137 = 0))) % 4.70/1.81 | (77) big_f(all_18_4_39, all_71_4_140) = all_71_3_139 % 4.70/1.81 | (78) big_g(all_18_4_39, all_18_4_39) = all_71_5_141 % 4.70/1.81 | % 4.70/1.81 | Instantiating (54) with all_83_0_170, all_83_1_171, all_83_2_172, all_83_3_173, all_83_4_174, all_83_5_175 yields: % 4.70/1.81 | (79) all_14_3_28 = 0 & big_f(all_83_4_174, all_83_4_174) = all_83_2_172 & big_f(all_14_4_29, all_83_4_174) = all_83_3_173 & big_g(all_83_4_174, all_83_4_174) = all_83_0_170 & big_g(all_1_4_4, all_83_4_174) = all_83_1_171 & big_g(all_1_4_4, all_14_4_29) = all_83_5_175 & ( ~ (all_83_2_172 = 0) | ~ (all_83_3_173 = 0) | (all_83_5_175 = 0 & ( ~ (all_83_0_170 = 0) | ~ (all_83_1_171 = 0)))) % 4.70/1.81 | % 4.70/1.81 | Applying alpha-rule on (79) yields: % 4.70/1.81 | (80) big_f(all_83_4_174, all_83_4_174) = all_83_2_172 % 4.70/1.81 | (81) ~ (all_83_2_172 = 0) | ~ (all_83_3_173 = 0) | (all_83_5_175 = 0 & ( ~ (all_83_0_170 = 0) | ~ (all_83_1_171 = 0))) % 4.70/1.81 | (82) big_g(all_1_4_4, all_14_4_29) = all_83_5_175 % 4.70/1.81 | (83) big_f(all_14_4_29, all_83_4_174) = all_83_3_173 % 4.70/1.81 | (84) all_14_3_28 = 0 % 4.70/1.81 | (85) big_g(all_1_4_4, all_83_4_174) = all_83_1_171 % 4.70/1.81 | (86) big_g(all_83_4_174, all_83_4_174) = all_83_0_170 % 4.70/1.81 | % 4.70/1.81 +-Applying beta-rule and splitting (29), into two cases. % 4.70/1.81 |-Branch one: % 4.70/1.81 | (87) ~ (all_14_2_27 = 0) % 4.70/1.81 | % 4.70/1.81 | Equations (68) can reduce 87 to: % 4.70/1.81 | (41) $false % 4.70/1.81 | % 4.70/1.81 |-The branch is then unsatisfiable % 4.70/1.81 |-Branch two: % 4.70/1.81 | (68) all_14_2_27 = 0 % 4.70/1.81 | (90) ~ (all_14_3_28 = 0) | (all_1_1_1 = 0 & ( ~ (all_14_0_25 = 0) | ~ (all_14_1_26 = 0))) % 4.70/1.81 | % 4.70/1.81 +-Applying beta-rule and splitting (90), into two cases. % 4.70/1.81 |-Branch one: % 4.70/1.82 | (91) ~ (all_14_3_28 = 0) % 4.70/1.82 | % 4.70/1.82 | Equations (84) can reduce 91 to: % 4.70/1.82 | (41) $false % 4.70/1.82 | % 4.70/1.82 |-The branch is then unsatisfiable % 4.70/1.82 |-Branch two: % 4.70/1.82 | (84) all_14_3_28 = 0 % 4.70/1.82 | (94) all_1_1_1 = 0 & ( ~ (all_14_0_25 = 0) | ~ (all_14_1_26 = 0)) % 4.70/1.82 | % 4.70/1.82 | Applying alpha-rule on (94) yields: % 4.70/1.82 | (95) all_1_1_1 = 0 % 4.70/1.82 | (96) ~ (all_14_0_25 = 0) | ~ (all_14_1_26 = 0) % 4.70/1.82 | % 4.70/1.82 +-Applying beta-rule and splitting (33), into two cases. % 4.70/1.82 |-Branch one: % 4.70/1.82 | (97) ~ (all_18_2_37 = 0) % 4.70/1.82 | % 4.70/1.82 | Equations (73) can reduce 97 to: % 4.70/1.82 | (41) $false % 4.70/1.82 | % 4.70/1.82 |-The branch is then unsatisfiable % 4.70/1.82 |-Branch two: % 4.70/1.82 | (73) all_18_2_37 = 0 % 4.70/1.82 | (100) ~ (all_18_3_38 = 0) | (all_18_5_40 = 0 & ( ~ (all_18_0_35 = 0) | ~ (all_18_1_36 = 0))) % 4.70/1.82 | % 4.70/1.82 +-Applying beta-rule and splitting (49), into two cases. % 4.70/1.82 |-Branch one: % 4.70/1.82 | (101) ~ (all_1_0_0 = 0) % 4.70/1.82 | % 4.70/1.82 +-Applying beta-rule and splitting (100), into two cases. % 4.70/1.82 |-Branch one: % 4.70/1.82 | (102) ~ (all_18_3_38 = 0) % 4.70/1.82 | % 4.70/1.82 | Equations (58) can reduce 102 to: % 4.70/1.82 | (41) $false % 4.70/1.82 | % 4.70/1.82 |-The branch is then unsatisfiable % 4.70/1.82 |-Branch two: % 4.70/1.82 | (58) all_18_3_38 = 0 % 4.70/1.82 | (105) all_18_5_40 = 0 & ( ~ (all_18_0_35 = 0) | ~ (all_18_1_36 = 0)) % 4.70/1.82 | % 4.70/1.82 | Applying alpha-rule on (105) yields: % 4.70/1.82 | (106) all_18_5_40 = 0 % 4.70/1.82 | (107) ~ (all_18_0_35 = 0) | ~ (all_18_1_36 = 0) % 4.70/1.82 | % 4.70/1.82 | Combining equations (50,106) yields a new equation: % 4.70/1.82 | (108) all_1_0_0 = 0 % 4.70/1.82 | % 4.70/1.82 | Simplifying 108 yields: % 4.70/1.82 | (109) all_1_0_0 = 0 % 4.70/1.82 | % 4.70/1.82 | Equations (109) can reduce 101 to: % 4.70/1.82 | (41) $false % 4.70/1.82 | % 4.70/1.82 |-The branch is then unsatisfiable % 4.70/1.82 |-Branch two: % 4.70/1.82 | (109) all_1_0_0 = 0 % 4.70/1.82 | (112) ~ (all_1_1_1 = 0) % 4.70/1.82 | % 4.70/1.82 | Equations (95) can reduce 112 to: % 4.70/1.82 | (41) $false % 4.70/1.82 | % 4.70/1.82 |-The branch is then unsatisfiable % 4.70/1.82 % SZS output end Proof for theBenchmark % 4.70/1.82 % 4.70/1.82 1208ms %------------------------------------------------------------------------------