%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SYN315+1 : TPTP v8.1.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n009.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:16 EDT 2022 % Result : Theorem 2.84s 1.44s % Output : Proof 3.88s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN315+1 : TPTP v8.1.0. Released v2.0.0. % 0.07/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.34 % Computer : n009.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 14:54:37 EDT 2022 % 0.12/0.34 % CPUTime : % 0.20/0.58 ____ _ % 0.20/0.58 ___ / __ \_____(_)___ ________ __________ % 0.20/0.58 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.20/0.58 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.20/0.58 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.20/0.58 % 0.20/0.58 A Theorem Prover for First-Order Logic % 0.20/0.58 (ePrincess v.1.0) % 0.20/0.58 % 0.20/0.58 (c) Philipp Rümmer, 2009-2015 % 0.20/0.58 (c) Peter Backeman, 2014-2015 % 0.20/0.58 (contributions by Angelo Brillout, Peter Baumgartner) % 0.20/0.58 Free software under GNU Lesser General Public License (LGPL). % 0.20/0.58 Bug reports to peter@backeman.se % 0.20/0.58 % 0.20/0.58 For more information, visit http://user.uu.se/~petba168/breu/ % 0.20/0.58 % 0.20/0.59 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.74/0.64 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.24/0.91 Prover 0: Preprocessing ... % 1.33/0.96 Prover 0: Warning: ignoring some quantifiers % 1.33/0.97 Prover 0: Constructing countermodel ... % 1.47/1.05 Prover 0: gave up % 1.47/1.05 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 1.68/1.07 Prover 1: Preprocessing ... % 1.68/1.10 Prover 1: Constructing countermodel ... % 1.68/1.11 Prover 1: gave up % 1.68/1.11 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.68/1.12 Prover 2: Preprocessing ... % 1.68/1.14 Prover 2: Warning: ignoring some quantifiers % 1.68/1.14 Prover 2: Constructing countermodel ... % 1.68/1.16 Prover 2: gave up % 1.68/1.16 Prover 3: Options: -triggersInConjecture -genTotalityAxioms +tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.68/1.16 Prover 3: Preprocessing ... % 1.68/1.17 Prover 3: Warning: ignoring some quantifiers % 1.68/1.17 Prover 3: Constructing countermodel ... % 2.18/1.19 Prover 3: gave up % 2.18/1.19 Prover 4: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=complete % 2.18/1.19 Prover 4: Preprocessing ... % 2.29/1.22 Prover 4: Warning: ignoring some quantifiers % 2.29/1.22 Prover 4: Constructing countermodel ... % 2.84/1.43 Prover 4: proved (246ms) % 2.84/1.44 % 2.84/1.44 No countermodel exists, formula is valid % 2.84/1.44 % SZS status Theorem for theBenchmark % 2.84/1.44 % 2.84/1.44 Generating proof ... Warning: ignoring some quantifiers % 3.65/1.67 found it (size 95) % 3.65/1.67 % 3.65/1.67 % SZS output start Proof for theBenchmark % 3.65/1.67 Assumed formulas after preprocessing and simplification: % 3.65/1.67 | (0) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (big_f(v2) = v1) | ~ (big_f(v2) = v0)) & ! [v0] : ! [v1] : ( ~ (big_f(v0) = v1) | ? [v2] : ? [v3] : (big_f(v2) = v3 & ( ~ (v3 = 0) | ~ p) & ( ~ (v1 = 0) | p) & (v3 = 0 | p) & (v1 = 0 | ~ p))) & ? [v0] : ? [v1] : ? [v2] : ? [v3] : (big_f(v2) = v3 & big_f(v0) = v1 & ( ~ (v3 = 0) | ~ p) & ( ~ (v1 = 0) | p) & (v3 = 0 | p) & (v1 = 0 | ~ p)) % 3.88/1.70 | Applying alpha-rule on (0) yields: % 3.88/1.70 | (1) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (big_f(v2) = v1) | ~ (big_f(v2) = v0)) % 3.88/1.70 | (2) ! [v0] : ! [v1] : ( ~ (big_f(v0) = v1) | ? [v2] : ? [v3] : (big_f(v2) = v3 & ( ~ (v3 = 0) | ~ p) & ( ~ (v1 = 0) | p) & (v3 = 0 | p) & (v1 = 0 | ~ p))) % 3.88/1.70 | (3) ? [v0] : ? [v1] : ? [v2] : ? [v3] : (big_f(v2) = v3 & big_f(v0) = v1 & ( ~ (v3 = 0) | ~ p) & ( ~ (v1 = 0) | p) & (v3 = 0 | p) & (v1 = 0 | ~ p)) % 3.88/1.70 | % 3.88/1.70 | Instantiating (3) with all_1_0_0, all_1_1_1, all_1_2_2, all_1_3_3 yields: % 3.88/1.70 | (4) big_f(all_1_1_1) = all_1_0_0 & big_f(all_1_3_3) = all_1_2_2 & ( ~ (all_1_0_0 = 0) | ~ p) & ( ~ (all_1_2_2 = 0) | p) & (all_1_0_0 = 0 | p) & (all_1_2_2 = 0 | ~ p) % 3.88/1.70 | % 3.88/1.70 | Applying alpha-rule on (4) yields: % 3.88/1.70 | (5) big_f(all_1_3_3) = all_1_2_2 % 3.88/1.70 | (6) all_1_2_2 = 0 | ~ p % 3.88/1.70 | (7) ~ (all_1_2_2 = 0) | p % 3.88/1.70 | (8) big_f(all_1_1_1) = all_1_0_0 % 3.88/1.70 | (9) ~ (all_1_0_0 = 0) | ~ p % 3.88/1.70 | (10) all_1_0_0 = 0 | p % 3.88/1.70 | % 3.88/1.70 | Instantiating formula (2) with all_1_0_0, all_1_1_1 and discharging atoms big_f(all_1_1_1) = all_1_0_0, yields: % 3.88/1.70 | (11) ? [v0] : ? [v1] : (big_f(v0) = v1 & ( ~ (v1 = 0) | ~ p) & ( ~ (all_1_0_0 = 0) | p) & (v1 = 0 | p) & (all_1_0_0 = 0 | ~ p)) % 3.88/1.70 | % 3.88/1.70 | Instantiating formula (2) with all_1_2_2, all_1_3_3 and discharging atoms big_f(all_1_3_3) = all_1_2_2, yields: % 3.88/1.70 | (12) ? [v0] : ? [v1] : (big_f(v0) = v1 & ( ~ (v1 = 0) | ~ p) & ( ~ (all_1_2_2 = 0) | p) & (v1 = 0 | p) & (all_1_2_2 = 0 | ~ p)) % 3.88/1.71 | % 3.88/1.71 | Instantiating (12) with all_8_0_4, all_8_1_5 yields: % 3.88/1.71 | (13) big_f(all_8_1_5) = all_8_0_4 & ( ~ (all_8_0_4 = 0) | ~ p) & ( ~ (all_1_2_2 = 0) | p) & (all_8_0_4 = 0 | p) & (all_1_2_2 = 0 | ~ p) % 3.88/1.71 | % 3.88/1.71 | Applying alpha-rule on (13) yields: % 3.88/1.71 | (6) all_1_2_2 = 0 | ~ p % 3.88/1.71 | (15) ~ (all_8_0_4 = 0) | ~ p % 3.88/1.71 | (7) ~ (all_1_2_2 = 0) | p % 3.88/1.71 | (17) all_8_0_4 = 0 | p % 3.88/1.71 | (18) big_f(all_8_1_5) = all_8_0_4 % 3.88/1.71 | % 3.88/1.71 | Instantiating (11) with all_10_0_6, all_10_1_7 yields: % 3.88/1.71 | (19) big_f(all_10_1_7) = all_10_0_6 & ( ~ (all_10_0_6 = 0) | ~ p) & ( ~ (all_1_0_0 = 0) | p) & (all_10_0_6 = 0 | p) & (all_1_0_0 = 0 | ~ p) % 3.88/1.71 | % 3.88/1.71 | Applying alpha-rule on (19) yields: % 3.88/1.71 | (20) ~ (all_1_0_0 = 0) | p % 3.88/1.71 | (21) big_f(all_10_1_7) = all_10_0_6 % 3.88/1.71 | (22) ~ (all_10_0_6 = 0) | ~ p % 3.88/1.71 | (23) all_10_0_6 = 0 | p % 3.88/1.71 | (24) all_1_0_0 = 0 | ~ p % 3.88/1.71 | % 3.88/1.71 | Instantiating formula (2) with all_10_0_6, all_10_1_7 and discharging atoms big_f(all_10_1_7) = all_10_0_6, yields: % 3.88/1.71 | (25) ? [v0] : ? [v1] : (big_f(v0) = v1 & ( ~ (v1 = 0) | ~ p) & ( ~ (all_10_0_6 = 0) | p) & (v1 = 0 | p) & (all_10_0_6 = 0 | ~ p)) % 3.88/1.71 | % 3.88/1.71 | Instantiating formula (2) with all_8_0_4, all_8_1_5 and discharging atoms big_f(all_8_1_5) = all_8_0_4, yields: % 3.88/1.71 | (26) ? [v0] : ? [v1] : (big_f(v0) = v1 & ( ~ (v1 = 0) | ~ p) & ( ~ (all_8_0_4 = 0) | p) & (v1 = 0 | p) & (all_8_0_4 = 0 | ~ p)) % 3.88/1.71 | % 3.88/1.71 | Instantiating (26) with all_17_0_8, all_17_1_9 yields: % 3.88/1.71 | (27) big_f(all_17_1_9) = all_17_0_8 & ( ~ (all_17_0_8 = 0) | ~ p) & ( ~ (all_8_0_4 = 0) | p) & (all_17_0_8 = 0 | p) & (all_8_0_4 = 0 | ~ p) % 3.88/1.71 | % 3.88/1.71 | Applying alpha-rule on (27) yields: % 3.88/1.71 | (28) ~ (all_8_0_4 = 0) | p % 3.88/1.71 | (29) big_f(all_17_1_9) = all_17_0_8 % 3.88/1.71 | (30) all_17_0_8 = 0 | p % 3.88/1.71 | (31) all_8_0_4 = 0 | ~ p % 3.88/1.71 | (32) ~ (all_17_0_8 = 0) | ~ p % 3.88/1.71 | % 3.88/1.71 | Instantiating (25) with all_19_0_10, all_19_1_11 yields: % 3.88/1.71 | (33) big_f(all_19_1_11) = all_19_0_10 & ( ~ (all_19_0_10 = 0) | ~ p) & ( ~ (all_10_0_6 = 0) | p) & (all_19_0_10 = 0 | p) & (all_10_0_6 = 0 | ~ p) % 3.88/1.71 | % 3.88/1.71 | Applying alpha-rule on (33) yields: % 3.88/1.71 | (34) all_10_0_6 = 0 | ~ p % 3.88/1.71 | (35) all_19_0_10 = 0 | p % 3.88/1.71 | (36) big_f(all_19_1_11) = all_19_0_10 % 3.88/1.71 | (37) ~ (all_19_0_10 = 0) | ~ p % 3.88/1.71 | (38) ~ (all_10_0_6 = 0) | p % 3.88/1.71 | % 3.88/1.71 | Instantiating formula (2) with all_19_0_10, all_19_1_11 and discharging atoms big_f(all_19_1_11) = all_19_0_10, yields: % 3.88/1.71 | (39) ? [v0] : ? [v1] : (big_f(v0) = v1 & ( ~ (v1 = 0) | ~ p) & ( ~ (all_19_0_10 = 0) | p) & (v1 = 0 | p) & (all_19_0_10 = 0 | ~ p)) % 3.88/1.71 | % 3.88/1.71 | Instantiating formula (2) with all_17_0_8, all_17_1_9 and discharging atoms big_f(all_17_1_9) = all_17_0_8, yields: % 3.88/1.71 | (40) ? [v0] : ? [v1] : (big_f(v0) = v1 & ( ~ (v1 = 0) | ~ p) & ( ~ (all_17_0_8 = 0) | p) & (v1 = 0 | p) & (all_17_0_8 = 0 | ~ p)) % 3.88/1.72 | % 3.88/1.72 | Instantiating (40) with all_26_0_12, all_26_1_13 yields: % 3.88/1.72 | (41) big_f(all_26_1_13) = all_26_0_12 & ( ~ (all_26_0_12 = 0) | ~ p) & ( ~ (all_17_0_8 = 0) | p) & (all_26_0_12 = 0 | p) & (all_17_0_8 = 0 | ~ p) % 3.88/1.72 | % 3.88/1.72 | Applying alpha-rule on (41) yields: % 3.88/1.72 | (42) ~ (all_17_0_8 = 0) | p % 3.88/1.72 | (43) ~ (all_26_0_12 = 0) | ~ p % 3.88/1.72 | (44) big_f(all_26_1_13) = all_26_0_12 % 3.88/1.72 | (45) all_17_0_8 = 0 | ~ p % 3.88/1.72 | (46) all_26_0_12 = 0 | p % 3.88/1.72 | % 3.88/1.72 | Instantiating (39) with all_28_0_14, all_28_1_15 yields: % 3.88/1.72 | (47) big_f(all_28_1_15) = all_28_0_14 & ( ~ (all_28_0_14 = 0) | ~ p) & ( ~ (all_19_0_10 = 0) | p) & (all_28_0_14 = 0 | p) & (all_19_0_10 = 0 | ~ p) % 3.88/1.72 | % 3.88/1.72 | Applying alpha-rule on (47) yields: % 3.88/1.72 | (48) ~ (all_19_0_10 = 0) | p % 3.88/1.72 | (49) all_28_0_14 = 0 | p % 3.88/1.72 | (50) ~ (all_28_0_14 = 0) | ~ p % 3.88/1.72 | (51) all_19_0_10 = 0 | ~ p % 3.88/1.72 | (52) big_f(all_28_1_15) = all_28_0_14 % 3.88/1.72 | % 3.88/1.72 | Instantiating formula (2) with all_28_0_14, all_28_1_15 and discharging atoms big_f(all_28_1_15) = all_28_0_14, yields: % 3.88/1.72 | (53) ? [v0] : ? [v1] : (big_f(v0) = v1 & ( ~ (v1 = 0) | ~ p) & ( ~ (all_28_0_14 = 0) | p) & (v1 = 0 | p) & (all_28_0_14 = 0 | ~ p)) % 3.88/1.72 | % 3.88/1.72 | Instantiating formula (2) with all_26_0_12, all_26_1_13 and discharging atoms big_f(all_26_1_13) = all_26_0_12, yields: % 3.88/1.72 | (54) ? [v0] : ? [v1] : (big_f(v0) = v1 & ( ~ (v1 = 0) | ~ p) & ( ~ (all_26_0_12 = 0) | p) & (v1 = 0 | p) & (all_26_0_12 = 0 | ~ p)) % 3.88/1.72 | % 3.88/1.72 | Instantiating (54) with all_35_0_16, all_35_1_17 yields: % 3.88/1.72 | (55) big_f(all_35_1_17) = all_35_0_16 & ( ~ (all_35_0_16 = 0) | ~ p) & ( ~ (all_26_0_12 = 0) | p) & (all_35_0_16 = 0 | p) & (all_26_0_12 = 0 | ~ p) % 3.88/1.72 | % 3.88/1.72 | Applying alpha-rule on (55) yields: % 3.88/1.72 | (56) big_f(all_35_1_17) = all_35_0_16 % 3.88/1.72 | (57) ~ (all_26_0_12 = 0) | p % 3.88/1.72 | (58) ~ (all_35_0_16 = 0) | ~ p % 3.88/1.72 | (59) all_26_0_12 = 0 | ~ p % 3.88/1.72 | (60) all_35_0_16 = 0 | p % 3.88/1.72 | % 3.88/1.72 | Instantiating (53) with all_37_0_18, all_37_1_19 yields: % 3.88/1.72 | (61) big_f(all_37_1_19) = all_37_0_18 & ( ~ (all_37_0_18 = 0) | ~ p) & ( ~ (all_28_0_14 = 0) | p) & (all_37_0_18 = 0 | p) & (all_28_0_14 = 0 | ~ p) % 3.88/1.72 | % 3.88/1.72 | Applying alpha-rule on (61) yields: % 3.88/1.72 | (62) all_28_0_14 = 0 | ~ p % 3.88/1.72 | (63) ~ (all_37_0_18 = 0) | ~ p % 3.88/1.72 | (64) all_37_0_18 = 0 | p % 3.88/1.72 | (65) big_f(all_37_1_19) = all_37_0_18 % 3.88/1.72 | (66) ~ (all_28_0_14 = 0) | p % 3.88/1.72 | % 3.88/1.72 | Instantiating formula (2) with all_37_0_18, all_37_1_19 and discharging atoms big_f(all_37_1_19) = all_37_0_18, yields: % 3.88/1.72 | (67) ? [v0] : ? [v1] : (big_f(v0) = v1 & ( ~ (v1 = 0) | ~ p) & ( ~ (all_37_0_18 = 0) | p) & (v1 = 0 | p) & (all_37_0_18 = 0 | ~ p)) % 3.88/1.72 | % 3.88/1.72 | Instantiating formula (2) with all_35_0_16, all_35_1_17 and discharging atoms big_f(all_35_1_17) = all_35_0_16, yields: % 3.88/1.72 | (68) ? [v0] : ? [v1] : (big_f(v0) = v1 & ( ~ (v1 = 0) | ~ p) & ( ~ (all_35_0_16 = 0) | p) & (v1 = 0 | p) & (all_35_0_16 = 0 | ~ p)) % 3.88/1.72 | % 3.88/1.72 | Instantiating (68) with all_44_0_20, all_44_1_21 yields: % 3.88/1.72 | (69) big_f(all_44_1_21) = all_44_0_20 & ( ~ (all_44_0_20 = 0) | ~ p) & ( ~ (all_35_0_16 = 0) | p) & (all_44_0_20 = 0 | p) & (all_35_0_16 = 0 | ~ p) % 3.88/1.72 | % 3.88/1.72 | Applying alpha-rule on (69) yields: % 3.88/1.72 | (70) all_35_0_16 = 0 | ~ p % 3.88/1.73 | (71) ~ (all_44_0_20 = 0) | ~ p % 3.88/1.73 | (72) ~ (all_35_0_16 = 0) | p % 3.88/1.73 | (73) big_f(all_44_1_21) = all_44_0_20 % 3.88/1.73 | (74) all_44_0_20 = 0 | p % 3.88/1.73 | % 3.88/1.73 | Instantiating (67) with all_46_0_22, all_46_1_23 yields: % 3.88/1.73 | (75) big_f(all_46_1_23) = all_46_0_22 & ( ~ (all_46_0_22 = 0) | ~ p) & ( ~ (all_37_0_18 = 0) | p) & (all_46_0_22 = 0 | p) & (all_37_0_18 = 0 | ~ p) % 3.88/1.73 | % 3.88/1.73 | Applying alpha-rule on (75) yields: % 3.88/1.73 | (76) ~ (all_37_0_18 = 0) | p % 3.88/1.73 | (77) all_37_0_18 = 0 | ~ p % 3.88/1.73 | (78) all_46_0_22 = 0 | p % 3.88/1.73 | (79) ~ (all_46_0_22 = 0) | ~ p % 3.88/1.73 | (80) big_f(all_46_1_23) = all_46_0_22 % 3.88/1.73 | % 3.88/1.73 | Instantiating formula (2) with all_46_0_22, all_46_1_23 and discharging atoms big_f(all_46_1_23) = all_46_0_22, yields: % 3.88/1.73 | (81) ? [v0] : ? [v1] : (big_f(v0) = v1 & ( ~ (v1 = 0) | ~ p) & ( ~ (all_46_0_22 = 0) | p) & (v1 = 0 | p) & (all_46_0_22 = 0 | ~ p)) % 3.88/1.73 | % 3.88/1.73 | Instantiating formula (2) with all_44_0_20, all_44_1_21 and discharging atoms big_f(all_44_1_21) = all_44_0_20, yields: % 3.88/1.73 | (82) ? [v0] : ? [v1] : (big_f(v0) = v1 & ( ~ (v1 = 0) | ~ p) & ( ~ (all_44_0_20 = 0) | p) & (v1 = 0 | p) & (all_44_0_20 = 0 | ~ p)) % 3.88/1.73 | % 3.88/1.73 | Instantiating (82) with all_53_0_24, all_53_1_25 yields: % 3.88/1.73 | (83) big_f(all_53_1_25) = all_53_0_24 & ( ~ (all_53_0_24 = 0) | ~ p) & ( ~ (all_44_0_20 = 0) | p) & (all_53_0_24 = 0 | p) & (all_44_0_20 = 0 | ~ p) % 3.88/1.73 | % 3.88/1.73 | Applying alpha-rule on (83) yields: % 3.88/1.73 | (84) all_44_0_20 = 0 | ~ p % 3.88/1.73 | (85) big_f(all_53_1_25) = all_53_0_24 % 3.88/1.73 | (86) ~ (all_44_0_20 = 0) | p % 3.88/1.73 | (87) ~ (all_53_0_24 = 0) | ~ p % 3.88/1.73 | (88) all_53_0_24 = 0 | p % 3.88/1.73 | % 3.88/1.73 | Instantiating (81) with all_55_0_26, all_55_1_27 yields: % 3.88/1.73 | (89) big_f(all_55_1_27) = all_55_0_26 & ( ~ (all_55_0_26 = 0) | ~ p) & ( ~ (all_46_0_22 = 0) | p) & (all_55_0_26 = 0 | p) & (all_46_0_22 = 0 | ~ p) % 3.88/1.73 | % 3.88/1.73 | Applying alpha-rule on (89) yields: % 3.88/1.73 | (90) all_46_0_22 = 0 | ~ p % 3.88/1.73 | (91) ~ (all_46_0_22 = 0) | p % 3.88/1.73 | (92) ~ (all_55_0_26 = 0) | ~ p % 3.88/1.73 | (93) big_f(all_55_1_27) = all_55_0_26 % 3.88/1.73 | (94) all_55_0_26 = 0 | p % 3.88/1.73 | % 3.88/1.73 | Instantiating formula (2) with all_55_0_26, all_55_1_27 and discharging atoms big_f(all_55_1_27) = all_55_0_26, yields: % 3.88/1.73 | (95) ? [v0] : ? [v1] : (big_f(v0) = v1 & ( ~ (v1 = 0) | ~ p) & ( ~ (all_55_0_26 = 0) | p) & (v1 = 0 | p) & (all_55_0_26 = 0 | ~ p)) % 3.88/1.73 | % 3.88/1.73 | Instantiating formula (2) with all_53_0_24, all_53_1_25 and discharging atoms big_f(all_53_1_25) = all_53_0_24, yields: % 3.88/1.73 | (96) ? [v0] : ? [v1] : (big_f(v0) = v1 & ( ~ (v1 = 0) | ~ p) & ( ~ (all_53_0_24 = 0) | p) & (v1 = 0 | p) & (all_53_0_24 = 0 | ~ p)) % 3.88/1.73 | % 3.88/1.73 | Instantiating (96) with all_62_0_28, all_62_1_29 yields: % 3.88/1.73 | (97) big_f(all_62_1_29) = all_62_0_28 & ( ~ (all_62_0_28 = 0) | ~ p) & ( ~ (all_53_0_24 = 0) | p) & (all_62_0_28 = 0 | p) & (all_53_0_24 = 0 | ~ p) % 3.88/1.73 | % 3.88/1.73 | Applying alpha-rule on (97) yields: % 3.88/1.73 | (98) ~ (all_53_0_24 = 0) | p % 3.88/1.73 | (99) big_f(all_62_1_29) = all_62_0_28 % 3.88/1.73 | (100) ~ (all_62_0_28 = 0) | ~ p % 3.88/1.73 | (101) all_62_0_28 = 0 | p % 3.88/1.73 | (102) all_53_0_24 = 0 | ~ p % 3.88/1.73 | % 3.88/1.73 | Instantiating (95) with all_64_0_30, all_64_1_31 yields: % 3.88/1.73 | (103) big_f(all_64_1_31) = all_64_0_30 & ( ~ (all_64_0_30 = 0) | ~ p) & ( ~ (all_55_0_26 = 0) | p) & (all_64_0_30 = 0 | p) & (all_55_0_26 = 0 | ~ p) % 3.88/1.73 | % 3.88/1.73 | Applying alpha-rule on (103) yields: % 3.88/1.73 | (104) all_55_0_26 = 0 | ~ p % 3.88/1.73 | (105) ~ (all_64_0_30 = 0) | ~ p % 3.88/1.74 | (106) all_64_0_30 = 0 | p % 3.88/1.74 | (107) ~ (all_55_0_26 = 0) | p % 3.88/1.74 | (108) big_f(all_64_1_31) = all_64_0_30 % 3.88/1.74 | % 3.88/1.74 | Instantiating formula (2) with all_62_0_28, all_62_1_29 and discharging atoms big_f(all_62_1_29) = all_62_0_28, yields: % 3.88/1.74 | (109) ? [v0] : ? [v1] : (big_f(v0) = v1 & ( ~ (v1 = 0) | ~ p) & ( ~ (all_62_0_28 = 0) | p) & (v1 = 0 | p) & (all_62_0_28 = 0 | ~ p)) % 3.88/1.74 | % 3.88/1.74 | Instantiating (109) with all_71_0_32, all_71_1_33 yields: % 3.88/1.74 | (110) big_f(all_71_1_33) = all_71_0_32 & ( ~ (all_71_0_32 = 0) | ~ p) & ( ~ (all_62_0_28 = 0) | p) & (all_71_0_32 = 0 | p) & (all_62_0_28 = 0 | ~ p) % 3.88/1.74 | % 3.88/1.74 | Applying alpha-rule on (110) yields: % 3.88/1.74 | (111) big_f(all_71_1_33) = all_71_0_32 % 3.88/1.74 | (112) all_62_0_28 = 0 | ~ p % 3.88/1.74 | (113) all_71_0_32 = 0 | p % 3.88/1.74 | (114) ~ (all_62_0_28 = 0) | p % 3.88/1.74 | (115) ~ (all_71_0_32 = 0) | ~ p % 3.88/1.74 | % 3.88/1.74 | Instantiating formula (2) with all_71_0_32, all_71_1_33 and discharging atoms big_f(all_71_1_33) = all_71_0_32, yields: % 3.88/1.74 | (116) ? [v0] : ? [v1] : (big_f(v0) = v1 & ( ~ (v1 = 0) | ~ p) & ( ~ (all_71_0_32 = 0) | p) & (v1 = 0 | p) & (all_71_0_32 = 0 | ~ p)) % 3.88/1.74 | % 3.88/1.74 | Instantiating (116) with all_80_0_36, all_80_1_37 yields: % 3.88/1.74 | (117) big_f(all_80_1_37) = all_80_0_36 & ( ~ (all_80_0_36 = 0) | ~ p) & ( ~ (all_71_0_32 = 0) | p) & (all_80_0_36 = 0 | p) & (all_71_0_32 = 0 | ~ p) % 3.88/1.74 | % 3.88/1.74 | Applying alpha-rule on (117) yields: % 3.88/1.74 | (118) ~ (all_80_0_36 = 0) | ~ p % 3.88/1.74 | (119) all_71_0_32 = 0 | ~ p % 3.88/1.74 | (120) big_f(all_80_1_37) = all_80_0_36 % 3.88/1.74 | (121) all_80_0_36 = 0 | p % 3.88/1.74 | (122) ~ (all_71_0_32 = 0) | p % 3.88/1.74 | % 3.88/1.74 +-Applying beta-rule and splitting (9), into two cases. % 3.88/1.74 |-Branch one: % 3.88/1.74 | (123) ~ p % 3.88/1.74 | % 3.88/1.74 +-Applying beta-rule and splitting (121), into two cases. % 3.88/1.74 |-Branch one: % 3.88/1.74 | (124) p % 3.88/1.74 | % 3.88/1.74 | Using (124) and (123) yields: % 3.88/1.74 | (125) $false % 3.88/1.74 | % 3.88/1.74 |-The branch is then unsatisfiable % 3.88/1.74 |-Branch two: % 3.88/1.74 | (123) ~ p % 3.88/1.74 | (127) all_80_0_36 = 0 % 3.88/1.74 | % 3.88/1.74 +-Applying beta-rule and splitting (10), into two cases. % 3.88/1.74 |-Branch one: % 3.88/1.74 | (124) p % 3.88/1.74 | % 3.88/1.74 | Using (124) and (123) yields: % 3.88/1.74 | (125) $false % 3.88/1.74 | % 3.88/1.74 |-The branch is then unsatisfiable % 3.88/1.74 |-Branch two: % 3.88/1.74 | (123) ~ p % 3.88/1.74 | (131) all_1_0_0 = 0 % 3.88/1.74 | % 3.88/1.74 +-Applying beta-rule and splitting (7), into two cases. % 3.88/1.74 |-Branch one: % 3.88/1.74 | (124) p % 3.88/1.74 | % 3.88/1.74 | Using (124) and (123) yields: % 3.88/1.74 | (125) $false % 3.88/1.74 | % 3.88/1.74 |-The branch is then unsatisfiable % 3.88/1.74 |-Branch two: % 3.88/1.74 | (123) ~ p % 3.88/1.74 | (135) ~ (all_1_2_2 = 0) % 3.88/1.74 | % 3.88/1.74 +-Applying beta-rule and splitting (46), into two cases. % 3.88/1.74 |-Branch one: % 3.88/1.74 | (124) p % 3.88/1.74 | % 3.88/1.74 | Using (124) and (123) yields: % 3.88/1.74 | (125) $false % 3.88/1.74 | % 3.88/1.74 |-The branch is then unsatisfiable % 3.88/1.74 |-Branch two: % 3.88/1.74 | (123) ~ p % 3.88/1.74 | (139) all_26_0_12 = 0 % 3.88/1.74 | % 3.88/1.74 +-Applying beta-rule and splitting (78), into two cases. % 3.88/1.74 |-Branch one: % 3.88/1.74 | (124) p % 3.88/1.74 | % 3.88/1.74 | Using (124) and (123) yields: % 3.88/1.74 | (125) $false % 3.88/1.74 | % 3.88/1.74 |-The branch is then unsatisfiable % 3.88/1.74 |-Branch two: % 3.88/1.74 | (123) ~ p % 3.88/1.74 | (143) all_46_0_22 = 0 % 3.88/1.74 | % 3.88/1.74 +-Applying beta-rule and splitting (86), into two cases. % 3.88/1.74 |-Branch one: % 3.88/1.74 | (124) p % 3.88/1.75 | % 3.88/1.75 | Using (124) and (123) yields: % 3.88/1.75 | (125) $false % 3.88/1.75 | % 3.88/1.75 |-The branch is then unsatisfiable % 3.88/1.75 |-Branch two: % 3.88/1.75 | (123) ~ p % 3.88/1.75 | (147) ~ (all_44_0_20 = 0) % 3.88/1.75 | % 3.88/1.75 +-Applying beta-rule and splitting (17), into two cases. % 3.88/1.75 |-Branch one: % 3.88/1.75 | (124) p % 3.88/1.75 | % 3.88/1.75 | Using (124) and (123) yields: % 3.88/1.75 | (125) $false % 3.88/1.75 | % 3.88/1.75 |-The branch is then unsatisfiable % 3.88/1.75 |-Branch two: % 3.88/1.75 | (123) ~ p % 3.88/1.75 | (151) all_8_0_4 = 0 % 3.88/1.75 | % 3.88/1.75 +-Applying beta-rule and splitting (30), into two cases. % 3.88/1.75 |-Branch one: % 3.88/1.75 | (124) p % 3.88/1.75 | % 3.88/1.75 | Using (124) and (123) yields: % 3.88/1.75 | (125) $false % 3.88/1.75 | % 3.88/1.75 |-The branch is then unsatisfiable % 3.88/1.75 |-Branch two: % 3.88/1.75 | (123) ~ p % 3.88/1.75 | (155) all_17_0_8 = 0 % 3.88/1.75 | % 3.88/1.75 +-Applying beta-rule and splitting (113), into two cases. % 3.88/1.75 |-Branch one: % 3.88/1.75 | (124) p % 3.88/1.75 | % 3.88/1.75 | Using (124) and (123) yields: % 3.88/1.75 | (125) $false % 3.88/1.75 | % 3.88/1.75 |-The branch is then unsatisfiable % 3.88/1.75 |-Branch two: % 3.88/1.75 | (123) ~ p % 3.88/1.75 | (159) all_71_0_32 = 0 % 3.88/1.75 | % 3.88/1.75 +-Applying beta-rule and splitting (107), into two cases. % 3.88/1.75 |-Branch one: % 3.88/1.75 | (124) p % 3.88/1.75 | % 3.88/1.75 | Using (124) and (123) yields: % 3.88/1.75 | (125) $false % 3.88/1.75 | % 3.88/1.75 |-The branch is then unsatisfiable % 3.88/1.75 |-Branch two: % 3.88/1.75 | (123) ~ p % 3.88/1.75 | (163) ~ (all_55_0_26 = 0) % 3.88/1.75 | % 3.88/1.75 +-Applying beta-rule and splitting (57), into two cases. % 3.88/1.75 |-Branch one: % 3.88/1.75 | (124) p % 3.88/1.75 | % 3.88/1.75 | Using (124) and (123) yields: % 3.88/1.75 | (125) $false % 3.88/1.75 | % 3.88/1.75 |-The branch is then unsatisfiable % 3.88/1.75 |-Branch two: % 3.88/1.75 | (123) ~ p % 3.88/1.75 | (167) ~ (all_26_0_12 = 0) % 3.88/1.75 | % 3.88/1.75 | Equations (139) can reduce 167 to: % 3.88/1.75 | (168) $false % 3.88/1.75 | % 3.88/1.75 |-The branch is then unsatisfiable % 3.88/1.75 |-Branch two: % 3.88/1.75 | (124) p % 3.88/1.75 | (170) ~ (all_1_0_0 = 0) % 3.88/1.75 | % 3.88/1.75 +-Applying beta-rule and splitting (6), into two cases. % 3.88/1.75 |-Branch one: % 3.88/1.75 | (123) ~ p % 3.88/1.75 | % 3.88/1.75 | Using (124) and (123) yields: % 3.88/1.75 | (125) $false % 3.88/1.75 | % 3.88/1.75 |-The branch is then unsatisfiable % 3.88/1.75 |-Branch two: % 3.88/1.75 | (124) p % 3.88/1.75 | (174) all_1_2_2 = 0 % 3.88/1.75 | % 3.88/1.75 +-Applying beta-rule and splitting (24), into two cases. % 3.88/1.75 |-Branch one: % 3.88/1.75 | (123) ~ p % 3.88/1.75 | % 3.88/1.75 | Using (124) and (123) yields: % 3.88/1.75 | (125) $false % 3.88/1.75 | % 3.88/1.75 |-The branch is then unsatisfiable % 3.88/1.75 |-Branch two: % 3.88/1.75 | (124) p % 3.88/1.75 | (131) all_1_0_0 = 0 % 3.88/1.75 | % 3.88/1.75 | Equations (131) can reduce 170 to: % 3.88/1.75 | (168) $false % 3.88/1.75 | % 3.88/1.75 |-The branch is then unsatisfiable % 3.88/1.75 % SZS output end Proof for theBenchmark % 3.88/1.75 % 3.88/1.75 1160ms %------------------------------------------------------------------------------