%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : SYN729+1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n014.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:04:45 EDT 2022 % Result : Theorem 26.95s 8.71s % Output : Proof 27.90s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.14 % Problem : SYN729+1 : TPTP v8.1.0. Released v2.5.0. % 0.04/0.15 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.36 % Computer : n014.cluster.edu % 0.12/0.36 % Model : x86_64 x86_64 % 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.36 % Memory : 8042.1875MB % 0.12/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.36 % CPULimit : 300 % 0.12/0.36 % WCLimit : 600 % 0.12/0.36 % DateTime : Mon Jul 11 13:49:04 EDT 2022 % 0.12/0.36 % CPUTime : % 0.58/0.66 ____ _ % 0.58/0.66 ___ / __ \_____(_)___ ________ __________ % 0.58/0.66 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.58/0.66 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.58/0.66 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.58/0.66 % 0.58/0.66 A Theorem Prover for First-Order Logic % 0.58/0.66 (ePrincess v.1.0) % 0.58/0.66 % 0.58/0.66 (c) Philipp Rümmer, 2009-2015 % 0.58/0.66 (c) Peter Backeman, 2014-2015 % 0.58/0.66 (contributions by Angelo Brillout, Peter Baumgartner) % 0.58/0.66 Free software under GNU Lesser General Public License (LGPL). % 0.58/0.66 Bug reports to peter@backeman.se % 0.58/0.66 % 0.58/0.66 For more information, visit http://user.uu.se/~petba168/breu/ % 0.58/0.66 % 0.58/0.66 Loading /export/starexec/sandbox/benchmark/theBenchmark.p ... % 0.71/0.71 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.31/0.97 Prover 0: Preprocessing ... % 1.40/1.05 Prover 0: Warning: ignoring some quantifiers % 1.56/1.06 Prover 0: Constructing countermodel ... % 16.21/6.00 Prover 1: Options: +triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple +reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=maximal -resolutionMethod=normal +ignoreQuantifiers -generateTriggers=all % 16.21/6.02 Prover 1: Preprocessing ... % 16.43/6.08 Prover 1: Constructing countermodel ... % 26.64/8.60 Prover 2: Options: +triggersInConjecture +genTotalityAxioms +tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation -boolFunsAsPreds -triggerStrategy=allUni -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 26.80/8.61 Prover 2: Preprocessing ... % 26.95/8.66 Prover 2: Warning: ignoring some quantifiers % 26.95/8.66 Prover 2: Constructing countermodel ... % 26.95/8.70 Prover 2: proved (104ms) % 26.95/8.70 Prover 1: stopped % 26.95/8.70 Prover 0: stopped % 26.95/8.71 % 26.95/8.71 No countermodel exists, formula is valid % 26.95/8.71 % SZS status Theorem for theBenchmark % 26.95/8.71 % 26.95/8.71 Generating proof ... Warning: ignoring some quantifiers % 27.85/8.85 found it (size 27) % 27.85/8.85 % 27.85/8.85 % SZS output start Proof for theBenchmark % 27.85/8.85 Assumed formulas after preprocessing and simplification: % 27.85/8.85 | (0) ? [v0] : (p(v0) = 0 & ! [v1] : ! [v2] : ! [v3] : ! [v4] : (v2 = v1 | ~ (l(v4, v3) = v2) | ~ (l(v4, v3) = v1)) & ! [v1] : ! [v2] : ! [v3] : (v2 = v1 | ~ (h(v3) = v2) | ~ (h(v3) = v1)) & ! [v1] : ! [v2] : ! [v3] : (v2 = v1 | ~ (g(v3) = v2) | ~ (g(v3) = v1)) & ! [v1] : ! [v2] : ! [v3] : (v2 = v1 | ~ (p(v3) = v2) | ~ (p(v3) = v1)) & ! [v1] : ! [v2] : ( ~ (h(v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ((v5 = 0 & v4 = 0 & g(v1) = v3 & p(v3) = 0 & p(v2) = 0) | ( ~ (v3 = 0) & p(v1) = v3))) & ! [v1] : ! [v2] : ( ~ (g(v1) = v2) | ? [v3] : ? [v4] : ? [v5] : ((v5 = 0 & v3 = 0 & h(v1) = v4 & p(v4) = 0 & p(v2) = 0) | ( ~ (v3 = 0) & p(v1) = v3))) & ! [v1] : ( ~ (l(v0, v1) = 0) | ? [v2] : ( ~ (v2 = 0) & p(v1) = v2)) & ! [v1] : ( ~ (p(v1) = 0) | ? [v2] : ? [v3] : ? [v4] : (h(v2) = v3 & g(v3) = v4 & l(v1, v4) = 0 & p(v2) = 0)) & ! [v1] : ( ~ (p(v1) = 0) | ? [v2] : ? [v3] : (h(v1) = v3 & g(v1) = v2 & p(v3) = 0 & p(v2) = 0)) & ! [v1] : ( ~ (p(v1) = 0) | ? [v2] : ( ~ (v2 = 0) & l(v0, v1) = v2)) & ? [v1] : ? [v2] : ? [v3] : l(v2, v1) = v3 & ? [v1] : ? [v2] : h(v1) = v2 & ? [v1] : ? [v2] : g(v1) = v2 & ? [v1] : ? [v2] : p(v1) = v2) % 27.90/8.88 | Instantiating (0) with all_0_0_0 yields: % 27.90/8.88 | (1) p(all_0_0_0) = 0 & ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (l(v3, v2) = v1) | ~ (l(v3, v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h(v2) = v1) | ~ (h(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (g(v2) = v1) | ~ (g(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (p(v2) = v1) | ~ (p(v2) = v0)) & ! [v0] : ! [v1] : ( ~ (h(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ((v4 = 0 & v3 = 0 & g(v0) = v2 & p(v2) = 0 & p(v1) = 0) | ( ~ (v2 = 0) & p(v0) = v2))) & ! [v0] : ! [v1] : ( ~ (g(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ((v4 = 0 & v2 = 0 & h(v0) = v3 & p(v3) = 0 & p(v1) = 0) | ( ~ (v2 = 0) & p(v0) = v2))) & ! [v0] : ( ~ (l(all_0_0_0, v0) = 0) | ? [v1] : ( ~ (v1 = 0) & p(v0) = v1)) & ! [v0] : ( ~ (p(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & g(v2) = v3 & l(v0, v3) = 0 & p(v1) = 0)) & ! [v0] : ( ~ (p(v0) = 0) | ? [v1] : ? [v2] : (h(v0) = v2 & g(v0) = v1 & p(v2) = 0 & p(v1) = 0)) & ! [v0] : ( ~ (p(v0) = 0) | ? [v1] : ( ~ (v1 = 0) & l(all_0_0_0, v0) = v1)) & ? [v0] : ? [v1] : ? [v2] : l(v1, v0) = v2 & ? [v0] : ? [v1] : h(v0) = v1 & ? [v0] : ? [v1] : g(v0) = v1 & ? [v0] : ? [v1] : p(v0) = v1 % 27.90/8.89 | % 27.90/8.89 | Applying alpha-rule on (1) yields: % 27.90/8.89 | (2) ! [v0] : ! [v1] : ( ~ (h(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ((v4 = 0 & v3 = 0 & g(v0) = v2 & p(v2) = 0 & p(v1) = 0) | ( ~ (v2 = 0) & p(v0) = v2))) % 27.90/8.89 | (3) ! [v0] : ( ~ (p(v0) = 0) | ? [v1] : ( ~ (v1 = 0) & l(all_0_0_0, v0) = v1)) % 27.90/8.89 | (4) ! [v0] : ( ~ (l(all_0_0_0, v0) = 0) | ? [v1] : ( ~ (v1 = 0) & p(v0) = v1)) % 27.90/8.89 | (5) ? [v0] : ? [v1] : g(v0) = v1 % 27.90/8.89 | (6) ? [v0] : ? [v1] : ? [v2] : l(v1, v0) = v2 % 27.90/8.89 | (7) ! [v0] : ! [v1] : ( ~ (g(v0) = v1) | ? [v2] : ? [v3] : ? [v4] : ((v4 = 0 & v2 = 0 & h(v0) = v3 & p(v3) = 0 & p(v1) = 0) | ( ~ (v2 = 0) & p(v0) = v2))) % 27.90/8.89 | (8) ? [v0] : ? [v1] : h(v0) = v1 % 27.90/8.89 | (9) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (h(v2) = v1) | ~ (h(v2) = v0)) % 27.90/8.89 | (10) ! [v0] : ( ~ (p(v0) = 0) | ? [v1] : ? [v2] : ? [v3] : (h(v1) = v2 & g(v2) = v3 & l(v0, v3) = 0 & p(v1) = 0)) % 27.90/8.89 | (11) ! [v0] : ! [v1] : ! [v2] : ! [v3] : (v1 = v0 | ~ (l(v3, v2) = v1) | ~ (l(v3, v2) = v0)) % 27.90/8.89 | (12) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (g(v2) = v1) | ~ (g(v2) = v0)) % 27.90/8.89 | (13) ! [v0] : ( ~ (p(v0) = 0) | ? [v1] : ? [v2] : (h(v0) = v2 & g(v0) = v1 & p(v2) = 0 & p(v1) = 0)) % 27.90/8.89 | (14) ? [v0] : ? [v1] : p(v0) = v1 % 27.90/8.89 | (15) p(all_0_0_0) = 0 % 27.90/8.89 | (16) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (p(v2) = v1) | ~ (p(v2) = v0)) % 27.90/8.89 | % 27.90/8.89 | Instantiating formula (10) with all_0_0_0 and discharging atoms p(all_0_0_0) = 0, yields: % 27.90/8.89 | (17) ? [v0] : ? [v1] : ? [v2] : (h(v0) = v1 & g(v1) = v2 & l(all_0_0_0, v2) = 0 & p(v0) = 0) % 27.90/8.89 | % 27.90/8.89 | Instantiating (17) with all_20_0_13, all_20_1_14, all_20_2_15 yields: % 27.90/8.89 | (18) h(all_20_2_15) = all_20_1_14 & g(all_20_1_14) = all_20_0_13 & l(all_0_0_0, all_20_0_13) = 0 & p(all_20_2_15) = 0 % 27.90/8.89 | % 27.90/8.89 | Applying alpha-rule on (18) yields: % 27.90/8.89 | (19) h(all_20_2_15) = all_20_1_14 % 27.90/8.89 | (20) g(all_20_1_14) = all_20_0_13 % 27.90/8.89 | (21) l(all_0_0_0, all_20_0_13) = 0 % 27.90/8.89 | (22) p(all_20_2_15) = 0 % 27.90/8.89 | % 27.90/8.89 | Instantiating formula (2) with all_20_1_14, all_20_2_15 and discharging atoms h(all_20_2_15) = all_20_1_14, yields: % 27.90/8.89 | (23) ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v1 = 0 & g(all_20_2_15) = v0 & p(v0) = 0 & p(all_20_1_14) = 0) | ( ~ (v0 = 0) & p(all_20_2_15) = v0)) % 27.90/8.89 | % 27.90/8.89 | Instantiating formula (7) with all_20_0_13, all_20_1_14 and discharging atoms g(all_20_1_14) = all_20_0_13, yields: % 27.90/8.90 | (24) ? [v0] : ? [v1] : ? [v2] : ((v2 = 0 & v0 = 0 & h(all_20_1_14) = v1 & p(v1) = 0 & p(all_20_0_13) = 0) | ( ~ (v0 = 0) & p(all_20_1_14) = v0)) % 27.90/8.90 | % 27.90/8.90 | Instantiating formula (4) with all_20_0_13 and discharging atoms l(all_0_0_0, all_20_0_13) = 0, yields: % 27.90/8.90 | (25) ? [v0] : ( ~ (v0 = 0) & p(all_20_0_13) = v0) % 27.90/8.90 | % 27.90/8.90 | Instantiating (25) with all_45_0_34 yields: % 27.90/8.90 | (26) ~ (all_45_0_34 = 0) & p(all_20_0_13) = all_45_0_34 % 27.90/8.90 | % 27.90/8.90 | Applying alpha-rule on (26) yields: % 27.90/8.90 | (27) ~ (all_45_0_34 = 0) % 27.90/8.90 | (28) p(all_20_0_13) = all_45_0_34 % 27.90/8.90 | % 27.90/8.90 | Instantiating (24) with all_47_0_35, all_47_1_36, all_47_2_37 yields: % 27.90/8.90 | (29) (all_47_0_35 = 0 & all_47_2_37 = 0 & h(all_20_1_14) = all_47_1_36 & p(all_47_1_36) = 0 & p(all_20_0_13) = 0) | ( ~ (all_47_2_37 = 0) & p(all_20_1_14) = all_47_2_37) % 27.90/8.90 | % 27.90/8.90 | Instantiating (23) with all_48_0_38, all_48_1_39, all_48_2_40 yields: % 27.90/8.90 | (30) (all_48_0_38 = 0 & all_48_1_39 = 0 & g(all_20_2_15) = all_48_2_40 & p(all_48_2_40) = 0 & p(all_20_1_14) = 0) | ( ~ (all_48_2_40 = 0) & p(all_20_2_15) = all_48_2_40) % 27.90/8.90 | % 27.90/8.90 +-Applying beta-rule and splitting (29), into two cases. % 27.90/8.90 |-Branch one: % 27.90/8.90 | (31) all_47_0_35 = 0 & all_47_2_37 = 0 & h(all_20_1_14) = all_47_1_36 & p(all_47_1_36) = 0 & p(all_20_0_13) = 0 % 27.90/8.90 | % 27.90/8.90 | Applying alpha-rule on (31) yields: % 27.90/8.90 | (32) all_47_0_35 = 0 % 27.90/8.90 | (33) all_47_2_37 = 0 % 27.90/8.90 | (34) h(all_20_1_14) = all_47_1_36 % 27.90/8.90 | (35) p(all_20_0_13) = 0 % 27.90/8.90 | (36) p(all_47_1_36) = 0 % 27.90/8.90 | % 27.90/8.90 | Instantiating formula (16) with all_20_0_13, 0, all_45_0_34 and discharging atoms p(all_20_0_13) = all_45_0_34, p(all_20_0_13) = 0, yields: % 27.90/8.90 | (37) all_45_0_34 = 0 % 27.90/8.90 | % 27.90/8.90 | Equations (37) can reduce 27 to: % 27.90/8.90 | (38) $false % 27.90/8.90 | % 27.90/8.90 |-The branch is then unsatisfiable % 27.90/8.90 |-Branch two: % 27.90/8.90 | (39) ~ (all_47_2_37 = 0) & p(all_20_1_14) = all_47_2_37 % 27.90/8.90 | % 27.90/8.90 | Applying alpha-rule on (39) yields: % 27.90/8.90 | (40) ~ (all_47_2_37 = 0) % 27.90/8.90 | (41) p(all_20_1_14) = all_47_2_37 % 27.90/8.90 | % 27.90/8.90 +-Applying beta-rule and splitting (30), into two cases. % 27.90/8.90 |-Branch one: % 27.90/8.90 | (42) all_48_0_38 = 0 & all_48_1_39 = 0 & g(all_20_2_15) = all_48_2_40 & p(all_48_2_40) = 0 & p(all_20_1_14) = 0 % 27.90/8.90 | % 27.90/8.90 | Applying alpha-rule on (42) yields: % 27.90/8.90 | (43) all_48_1_39 = 0 % 27.90/8.90 | (44) all_48_0_38 = 0 % 27.90/8.90 | (45) p(all_20_1_14) = 0 % 27.90/8.90 | (46) g(all_20_2_15) = all_48_2_40 % 27.90/8.90 | (47) p(all_48_2_40) = 0 % 27.90/8.90 | % 27.90/8.90 | Instantiating formula (16) with all_20_1_14, 0, all_47_2_37 and discharging atoms p(all_20_1_14) = all_47_2_37, p(all_20_1_14) = 0, yields: % 27.90/8.90 | (33) all_47_2_37 = 0 % 27.90/8.90 | % 27.90/8.90 | Equations (33) can reduce 40 to: % 27.90/8.90 | (38) $false % 27.90/8.90 | % 27.90/8.90 |-The branch is then unsatisfiable % 27.90/8.90 |-Branch two: % 27.90/8.90 | (50) ~ (all_48_2_40 = 0) & p(all_20_2_15) = all_48_2_40 % 27.90/8.90 | % 27.90/8.90 | Applying alpha-rule on (50) yields: % 27.90/8.90 | (51) ~ (all_48_2_40 = 0) % 27.90/8.90 | (52) p(all_20_2_15) = all_48_2_40 % 27.90/8.90 | % 27.90/8.90 | Instantiating formula (16) with all_20_2_15, all_48_2_40, 0 and discharging atoms p(all_20_2_15) = all_48_2_40, p(all_20_2_15) = 0, yields: % 27.90/8.90 | (53) all_48_2_40 = 0 % 27.90/8.90 | % 27.90/8.90 | Equations (53) can reduce 51 to: % 27.90/8.90 | (38) $false % 27.90/8.90 | % 27.90/8.90 |-The branch is then unsatisfiable % 27.90/8.90 % SZS output end Proof for theBenchmark % 27.90/8.90 % 27.90/8.90 8237ms %------------------------------------------------------------------------------