%------------------------------------------------------------------------------ % File : ePrincess---1.0 % Problem : KRS180+1 : TPTP v8.1.0. Bugfixed v5.4.0. % Transfm : none % Format : tptp:raw % Command : ePrincess-casc -timeout=%d %s % Computer : n021.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 : Sun Jul 17 02:56:49 EDT 2022 % Result : Theorem 8.86s 2.76s % Output : Proof 10.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : KRS180+1 : TPTP v8.1.0. Bugfixed v5.4.0. % 0.07/0.13 % Command : ePrincess-casc -timeout=%d %s % 0.12/0.34 % Computer : n021.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 Jun 7 11:13:21 EDT 2022 % 0.12/0.34 % CPUTime : % 0.47/0.58 ____ _ % 0.47/0.58 ___ / __ \_____(_)___ ________ __________ % 0.47/0.58 / _ \/ /_/ / ___/ / __ \/ ___/ _ \/ ___/ ___/ % 0.47/0.58 / __/ ____/ / / / / / / /__/ __(__ |__ ) % 0.47/0.58 \___/_/ /_/ /_/_/ /_/\___/\___/____/____/ % 0.47/0.58 % 0.47/0.58 A Theorem Prover for First-Order Logic % 0.47/0.59 (ePrincess v.1.0) % 0.47/0.59 % 0.47/0.59 (c) Philipp Rümmer, 2009-2015 % 0.47/0.59 (c) Peter Backeman, 2014-2015 % 0.47/0.59 (contributions by Angelo Brillout, Peter Baumgartner) % 0.47/0.59 Free software under GNU Lesser General Public License (LGPL). % 0.47/0.59 Bug reports to peter@backeman.se % 0.47/0.59 % 0.47/0.59 For more information, visit http://user.uu.se/~petba168/breu/ % 0.47/0.59 % 0.47/0.59 Loading /export/starexec/sandbox2/benchmark/theBenchmark.p ... % 0.47/0.63 Prover 0: Options: -triggersInConjecture -genTotalityAxioms -tightFunctionScopes -clausifier=simple -reverseFunctionalityPropagation +boolFunsAsPreds -triggerStrategy=allMaximal -resolutionMethod=nonUnifying +ignoreQuantifiers -generateTriggers=all % 1.49/0.92 Prover 0: Preprocessing ... % 2.03/1.07 Prover 0: Warning: ignoring some quantifiers % 2.07/1.09 Prover 0: Constructing countermodel ... % 8.86/2.76 Prover 0: proved (2127ms) % 8.86/2.76 % 8.86/2.76 No countermodel exists, formula is valid % 8.86/2.76 % SZS status Theorem for theBenchmark % 8.86/2.76 % 8.86/2.76 Generating proof ... Warning: ignoring some quantifiers % 9.77/2.96 found it (size 15) % 9.77/2.96 % 9.77/2.96 % SZS output start Proof for theBenchmark % 9.77/2.96 Assumed formulas after preprocessing and simplification: % 9.77/2.96 | (0) ? [v0] : ? [v1] : ? [v2] : ? [v3] : ? [v4] : ? [v5] : ? [v6] : ? [v7] : ? [v8] : ? [v9] : ? [v10] : ? [v11] : ? [v12] : ? [v13] : ? [v14] : ? [v15] : ? [v16] : ? [v17] : ? [v18] : ? [v19] : (model(v18, v16) & model(v14, v12) & model(v14, v11) & model(v10, v6) & model(v9, v7) & model(v5, v4) & model(v2, v3) & isa(v0, v1) & ~ model(v17, v16) & ~ model(v9, v6) & ~ model(v8, v7) & ~ model(v2, v4) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ( ~ xora(v20, v21) | ~ status(v22, v23, v21) | ~ status(v22, v23, v20)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ( ~ nevera(v20, v21) | ~ status(v22, v23, v21) | ~ status(v22, v23, v20)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ( ~ isa(v20, v21) | ~ status(v22, v23, v20) | status(v22, v23, v21)) & ! [v20] : ! [v21] : ! [v22] : ! [v23] : ( ~ status(v22, v23, v21) | ~ status(v22, v23, v20) | mighta(v20, v21)) & ? [v20] : ! [v21] : ! [v22] : ! [v23] : ( ~ status(v22, v23, v21) | nota(v21, v20) | status(v22, v23, v20)) & ! [v20] : ! [v21] : ! [v22] : (v21 = v20 | ~ (not(v22) = v21) | ~ (not(v22) = v20)) & ! [v20] : ! [v21] : ! [v22] : ( ~ (not(v21) = v22) | ~ model(v20, v22) | ~ model(v20, v21)) & ? [v20] : ? [v21] : ! [v22] : ! [v23] : ( ~ xora(v22, v23) | status(v20, v21, v23) | status(v20, v21, v22)) & ? [v20] : ! [v21] : ! [v22] : ( ~ (not(v21) = v22) | model(v20, v22) | model(v20, v21)) & ! [v20] : ! [v21] : ( ~ nota(v20, v21) | ? [v22] : ? [v23] : (status(v22, v23, v20) & ~ status(v22, v23, v21))) & ! [v20] : ! [v21] : ( ~ mighta(v20, v21) | ? [v22] : ? [v23] : (status(v22, v23, v21) & status(v22, v23, v20))) & ! [v20] : ~ model(v20, v15) & ! [v20] : ( ~ model(v20, v6) | model(v20, v7)) & ? [v20] : ? [v21] : (xora(v20, v21) | ? [v22] : ? [v23] : (( ~ status(v22, v23, v21) | status(v22, v23, v20)) & ( ~ status(v22, v23, v20) | status(v22, v23, v21)))) & ? [v20] : ? [v21] : (nevera(v20, v21) | ? [v22] : ? [v23] : (status(v22, v23, v21) & status(v22, v23, v20))) & ? [v20] : ? [v21] : (isa(v20, v21) | ? [v22] : ? [v23] : (status(v22, v23, v20) & ~ status(v22, v23, v21))) & ? [v20] : ? [v21] : status(v20, v21, v0) & ? [v20] : model(v20, v19) & ( ~ model(v13, v12) | ~ model(v13, v11)) & (xora(v0, v1) | nevera(v0, v1) | nota(v0, v1))) % 10.16/3.01 | Instantiating (0) with all_0_0_0, all_0_1_1, all_0_2_2, all_0_3_3, all_0_4_4, all_0_5_5, all_0_6_6, all_0_7_7, all_0_8_8, all_0_9_9, all_0_10_10, all_0_11_11, all_0_12_12, all_0_13_13, all_0_14_14, all_0_15_15, all_0_16_16, all_0_17_17, all_0_18_18, all_0_19_19 yields: % 10.16/3.01 | (1) model(all_0_1_1, all_0_3_3) & model(all_0_5_5, all_0_7_7) & model(all_0_5_5, all_0_8_8) & model(all_0_9_9, all_0_13_13) & model(all_0_10_10, all_0_12_12) & model(all_0_14_14, all_0_15_15) & model(all_0_17_17, all_0_16_16) & isa(all_0_19_19, all_0_18_18) & ~ model(all_0_2_2, all_0_3_3) & ~ model(all_0_10_10, all_0_13_13) & ~ model(all_0_11_11, all_0_12_12) & ~ model(all_0_17_17, all_0_15_15) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ xora(v0, v1) | ~ status(v2, v3, v1) | ~ status(v2, v3, v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ nevera(v0, v1) | ~ status(v2, v3, v1) | ~ status(v2, v3, v0)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ isa(v0, v1) | ~ status(v2, v3, v0) | status(v2, v3, v1)) & ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ status(v2, v3, v1) | ~ status(v2, v3, v0) | mighta(v0, v1)) & ? [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ status(v2, v3, v1) | nota(v1, v0) | status(v2, v3, v0)) & ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (not(v2) = v1) | ~ (not(v2) = v0)) & ! [v0] : ! [v1] : ! [v2] : ( ~ (not(v1) = v2) | ~ model(v0, v2) | ~ model(v0, v1)) & ? [v0] : ? [v1] : ! [v2] : ! [v3] : ( ~ xora(v2, v3) | status(v0, v1, v3) | status(v0, v1, v2)) & ? [v0] : ! [v1] : ! [v2] : ( ~ (not(v1) = v2) | model(v0, v2) | model(v0, v1)) & ! [v0] : ! [v1] : ( ~ nota(v0, v1) | ? [v2] : ? [v3] : (status(v2, v3, v0) & ~ status(v2, v3, v1))) & ! [v0] : ! [v1] : ( ~ mighta(v0, v1) | ? [v2] : ? [v3] : (status(v2, v3, v1) & status(v2, v3, v0))) & ! [v0] : ~ model(v0, all_0_4_4) & ! [v0] : ( ~ model(v0, all_0_13_13) | model(v0, all_0_12_12)) & ? [v0] : ? [v1] : (xora(v0, v1) | ? [v2] : ? [v3] : (( ~ status(v2, v3, v1) | status(v2, v3, v0)) & ( ~ status(v2, v3, v0) | status(v2, v3, v1)))) & ? [v0] : ? [v1] : (nevera(v0, v1) | ? [v2] : ? [v3] : (status(v2, v3, v1) & status(v2, v3, v0))) & ? [v0] : ? [v1] : (isa(v0, v1) | ? [v2] : ? [v3] : (status(v2, v3, v0) & ~ status(v2, v3, v1))) & ? [v0] : ? [v1] : status(v0, v1, all_0_19_19) & ? [v0] : model(v0, all_0_0_0) & ( ~ model(all_0_6_6, all_0_7_7) | ~ model(all_0_6_6, all_0_8_8)) & (xora(all_0_19_19, all_0_18_18) | nevera(all_0_19_19, all_0_18_18) | nota(all_0_19_19, all_0_18_18)) % 10.16/3.01 | % 10.16/3.01 | Applying alpha-rule on (1) yields: % 10.16/3.01 | (2) model(all_0_9_9, all_0_13_13) % 10.16/3.01 | (3) ! [v0] : ! [v1] : ! [v2] : (v1 = v0 | ~ (not(v2) = v1) | ~ (not(v2) = v0)) % 10.16/3.01 | (4) ~ model(all_0_2_2, all_0_3_3) % 10.16/3.01 | (5) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ status(v2, v3, v1) | ~ status(v2, v3, v0) | mighta(v0, v1)) % 10.16/3.01 | (6) ? [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ status(v2, v3, v1) | nota(v1, v0) | status(v2, v3, v0)) % 10.16/3.01 | (7) isa(all_0_19_19, all_0_18_18) % 10.16/3.01 | (8) ~ model(all_0_17_17, all_0_15_15) % 10.16/3.01 | (9) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ xora(v0, v1) | ~ status(v2, v3, v1) | ~ status(v2, v3, v0)) % 10.16/3.01 | (10) ? [v0] : ! [v1] : ! [v2] : ( ~ (not(v1) = v2) | model(v0, v2) | model(v0, v1)) % 10.16/3.01 | (11) model(all_0_5_5, all_0_8_8) % 10.16/3.01 | (12) xora(all_0_19_19, all_0_18_18) | nevera(all_0_19_19, all_0_18_18) | nota(all_0_19_19, all_0_18_18) % 10.16/3.01 | (13) ! [v0] : ! [v1] : ( ~ mighta(v0, v1) | ? [v2] : ? [v3] : (status(v2, v3, v1) & status(v2, v3, v0))) % 10.16/3.02 | (14) ~ model(all_0_10_10, all_0_13_13) % 10.16/3.02 | (15) ? [v0] : model(v0, all_0_0_0) % 10.16/3.02 | (16) ? [v0] : ? [v1] : (nevera(v0, v1) | ? [v2] : ? [v3] : (status(v2, v3, v1) & status(v2, v3, v0))) % 10.16/3.02 | (17) ? [v0] : ? [v1] : (isa(v0, v1) | ? [v2] : ? [v3] : (status(v2, v3, v0) & ~ status(v2, v3, v1))) % 10.16/3.02 | (18) ~ model(all_0_6_6, all_0_7_7) | ~ model(all_0_6_6, all_0_8_8) % 10.16/3.02 | (19) model(all_0_5_5, all_0_7_7) % 10.16/3.02 | (20) ! [v0] : ( ~ model(v0, all_0_13_13) | model(v0, all_0_12_12)) % 10.16/3.02 | (21) ! [v0] : ! [v1] : ! [v2] : ( ~ (not(v1) = v2) | ~ model(v0, v2) | ~ model(v0, v1)) % 10.16/3.02 | (22) ! [v0] : ~ model(v0, all_0_4_4) % 10.16/3.02 | (23) ! [v0] : ! [v1] : ( ~ nota(v0, v1) | ? [v2] : ? [v3] : (status(v2, v3, v0) & ~ status(v2, v3, v1))) % 10.16/3.02 | (24) model(all_0_14_14, all_0_15_15) % 10.16/3.02 | (25) model(all_0_10_10, all_0_12_12) % 10.16/3.02 | (26) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ nevera(v0, v1) | ~ status(v2, v3, v1) | ~ status(v2, v3, v0)) % 10.16/3.02 | (27) ~ model(all_0_11_11, all_0_12_12) % 10.16/3.02 | (28) ? [v0] : ? [v1] : (xora(v0, v1) | ? [v2] : ? [v3] : (( ~ status(v2, v3, v1) | status(v2, v3, v0)) & ( ~ status(v2, v3, v0) | status(v2, v3, v1)))) % 10.16/3.02 | (29) ! [v0] : ! [v1] : ! [v2] : ! [v3] : ( ~ isa(v0, v1) | ~ status(v2, v3, v0) | status(v2, v3, v1)) % 10.16/3.02 | (30) ? [v0] : ? [v1] : ! [v2] : ! [v3] : ( ~ xora(v2, v3) | status(v0, v1, v3) | status(v0, v1, v2)) % 10.16/3.02 | (31) model(all_0_17_17, all_0_16_16) % 10.16/3.02 | (32) model(all_0_1_1, all_0_3_3) % 10.16/3.02 | (33) ? [v0] : ? [v1] : status(v0, v1, all_0_19_19) % 10.16/3.02 | % 10.16/3.02 | Instantiating (33) with all_7_0_25, all_7_1_26 yields: % 10.16/3.02 | (34) status(all_7_1_26, all_7_0_25, all_0_19_19) % 10.16/3.02 | % 10.16/3.02 | Instantiating formula (29) with all_7_0_25, all_7_1_26, all_0_18_18, all_0_19_19 and discharging atoms isa(all_0_19_19, all_0_18_18), status(all_7_1_26, all_7_0_25, all_0_19_19), yields: % 10.16/3.02 | (35) status(all_7_1_26, all_7_0_25, all_0_18_18) % 10.16/3.02 | % 10.16/3.02 +-Applying beta-rule and splitting (12), into two cases. % 10.16/3.02 |-Branch one: % 10.16/3.02 | (36) xora(all_0_19_19, all_0_18_18) % 10.16/3.02 | % 10.16/3.02 | Instantiating formula (9) with all_7_0_25, all_7_1_26, all_0_18_18, all_0_19_19 and discharging atoms xora(all_0_19_19, all_0_18_18), status(all_7_1_26, all_7_0_25, all_0_18_18), status(all_7_1_26, all_7_0_25, all_0_19_19), yields: % 10.16/3.02 | (37) $false % 10.16/3.02 | % 10.16/3.02 |-The branch is then unsatisfiable % 10.16/3.02 |-Branch two: % 10.16/3.02 | (38) ~ xora(all_0_19_19, all_0_18_18) % 10.16/3.02 | (39) nevera(all_0_19_19, all_0_18_18) | nota(all_0_19_19, all_0_18_18) % 10.16/3.02 | % 10.16/3.02 +-Applying beta-rule and splitting (39), into two cases. % 10.16/3.02 |-Branch one: % 10.16/3.02 | (40) nevera(all_0_19_19, all_0_18_18) % 10.16/3.02 | % 10.16/3.02 | Instantiating formula (26) with all_7_0_25, all_7_1_26, all_0_18_18, all_0_19_19 and discharging atoms nevera(all_0_19_19, all_0_18_18), status(all_7_1_26, all_7_0_25, all_0_18_18), status(all_7_1_26, all_7_0_25, all_0_19_19), yields: % 10.16/3.02 | (37) $false % 10.16/3.02 | % 10.16/3.02 |-The branch is then unsatisfiable % 10.16/3.02 |-Branch two: % 10.16/3.02 | (42) ~ nevera(all_0_19_19, all_0_18_18) % 10.16/3.02 | (43) nota(all_0_19_19, all_0_18_18) % 10.16/3.02 | % 10.16/3.02 | Instantiating formula (23) with all_0_18_18, all_0_19_19 and discharging atoms nota(all_0_19_19, all_0_18_18), yields: % 10.16/3.02 | (44) ? [v0] : ? [v1] : (status(v0, v1, all_0_19_19) & ~ status(v0, v1, all_0_18_18)) % 10.16/3.02 | % 10.16/3.02 | Instantiating (44) with all_138_0_45, all_138_1_46 yields: % 10.16/3.02 | (45) status(all_138_1_46, all_138_0_45, all_0_19_19) & ~ status(all_138_1_46, all_138_0_45, all_0_18_18) % 10.16/3.02 | % 10.16/3.02 | Applying alpha-rule on (45) yields: % 10.16/3.02 | (46) status(all_138_1_46, all_138_0_45, all_0_19_19) % 10.16/3.02 | (47) ~ status(all_138_1_46, all_138_0_45, all_0_18_18) % 10.16/3.02 | % 10.16/3.02 | Instantiating formula (29) with all_138_0_45, all_138_1_46, all_0_18_18, all_0_19_19 and discharging atoms isa(all_0_19_19, all_0_18_18), status(all_138_1_46, all_138_0_45, all_0_19_19), ~ status(all_138_1_46, all_138_0_45, all_0_18_18), yields: % 10.16/3.02 | (37) $false % 10.16/3.02 | % 10.16/3.02 |-The branch is then unsatisfiable % 10.16/3.02 % SZS output end Proof for theBenchmark % 10.16/3.03 % 10.16/3.03 2429ms %------------------------------------------------------------------------------