%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PHI013+1 : TPTP v8.2.0. Released v7.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n017.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 : 300s % DateTime : Mon Jun 24 13:33:54 EDT 2024 % Result : Theorem 7.30s 7.42s % Output : CNFRefutation 7.30s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : PHI013+1 : TPTP v8.2.0. Released v7.2.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n017.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Tue Jun 18 20:17:09 EDT 2024 % 0.12/0.34 % CPUTime : % 0.56/0.63 start to proof:theBenchmark % 7.22/7.41 %------------------------------------------- % 7.22/7.41 % File :CSE---1.7 % 7.22/7.41 % Problem :theBenchmark % 7.22/7.41 % Transform :cnf % 7.22/7.41 % Format :tptp:raw % 7.22/7.41 % Command :java -jar mcs_scs.jar %d %s % 7.22/7.41 % 7.22/7.41 % Result :Theorem 6.700000s % 7.22/7.41 % Output :CNFRefutation 6.700000s % 7.22/7.41 %------------------------------------------- % 7.30/7.41 %------------------------------------------------------------------------------ % 7.30/7.41 % File : PHI013+1 : TPTP v8.2.0. Released v7.2.0. % 7.30/7.41 % Domain : Philosophy % 7.30/7.41 % Problem : Anselm's ontological argument % 7.30/7.41 % Version : [Wol16] axioms. % 7.30/7.41 % English : % 7.30/7.41 % 7.30/7.41 % Refs : [OZ11] Oppenheimer & Zalta (2011), A Computationally-Discover % 7.30/7.41 % : [Wol16] Woltzenlogel Paleo (2016), Email to Geoff Sutcliffe % 7.30/7.41 % Source : [Wol16] % 7.30/7.41 % Names : ontological.p [Wol16] % 7.30/7.41 % 7.30/7.41 % Status : Theorem % 7.30/7.41 % Rating : 0.06 v7.4.0, 0.07 v7.2.0 % 7.30/7.41 % Syntax : Number of formulae : 9 ( 2 unt; 0 def) % 7.30/7.41 % Number of atoms : 40 ( 2 equ) % 7.30/7.41 % Maximal formula atoms : 8 ( 4 avg) % 7.30/7.41 % Number of connectives : 33 ( 2 ~; 0 |; 15 &) % 7.30/7.41 % ( 1 <=>; 15 =>; 0 <=; 0 <~>) % 7.30/7.41 % Maximal formula depth : 10 ( 6 avg) % 7.30/7.41 % Maximal term depth : 1 ( 1 avg) % 7.30/7.41 % Number of predicates : 6 ( 5 usr; 0 prp; 1-3 aty) % 7.30/7.41 % Number of functors : 5 ( 5 usr; 5 con; 0-0 aty) % 7.30/7.41 % Number of variables : 17 ( 9 !; 8 ?) % 7.30/7.41 % SPC : FOF_THM_RFO_SEQ % 7.30/7.41 % 7.30/7.41 % Comments : See http://mally.stanford.edu/cm/ontological-argument/ % 7.30/7.41 %------------------------------------------------------------------------------ % 7.30/7.41 fof(description_theorem_1,axiom, % 7.30/7.41 ! [F] : % 7.30/7.41 ( property(F) % 7.30/7.41 => ( ? [Y] : % 7.30/7.41 ( object(Y) % 7.30/7.41 & exemplifies_property(F,Y) % 7.30/7.41 & ! [Z] : % 7.30/7.41 ( object(Z) % 7.30/7.41 => ( exemplifies_property(F,Z) % 7.30/7.41 => Z = Y ) ) ) % 7.30/7.41 => ? [U] : % 7.30/7.41 ( object(U) % 7.30/7.41 & is_the(U,F) ) ) ) ). % 7.30/7.41 % 7.30/7.41 fof(description_theorem_2,axiom, % 7.30/7.41 ! [F] : % 7.30/7.41 ( property(F) % 7.30/7.41 => ( ? [Y] : % 7.30/7.41 ( object(Y) % 7.30/7.41 & is_the(Y,F) ) % 7.30/7.41 => ! [Z] : % 7.30/7.41 ( object(Z) % 7.30/7.41 => ( is_the(Z,F) % 7.30/7.41 => exemplifies_property(F,Z) ) ) ) ) ). % 7.30/7.41 % 7.30/7.41 fof(description_is_property_and_described_is_object,axiom, % 7.30/7.41 ! [X,F] : % 7.30/7.41 ( is_the(X,F) % 7.30/7.41 => ( property(F) % 7.30/7.41 & object(X) ) ) ). % 7.30/7.41 % 7.30/7.41 fof(definition_none_greater,axiom, % 7.30/7.41 ! [X] : % 7.30/7.41 ( object(X) % 7.30/7.41 => ( exemplifies_property(none_greater,X) % 7.30/7.41 <=> ( exemplifies_property(conceivable,X) % 7.30/7.41 & ~ ? [Y] : % 7.30/7.41 ( object(Y) % 7.30/7.41 & exemplifies_relation(greater_than,Y,X) % 7.30/7.41 & exemplifies_property(conceivable,Y) ) ) ) ) ). % 7.30/7.41 % 7.30/7.41 fof(premise_1,axiom, % 7.30/7.41 ? [X] : % 7.30/7.41 ( object(X) % 7.30/7.42 & exemplifies_property(none_greater,X) ) ). % 7.30/7.42 % 7.30/7.42 fof(lemma_2,axiom, % 7.30/7.42 ( ? [X] : % 7.30/7.42 ( object(X) % 7.30/7.42 & exemplifies_property(none_greater,X) ) % 7.30/7.42 => ? [X] : % 7.30/7.42 ( object(X) % 7.30/7.42 & exemplifies_property(none_greater,X) % 7.30/7.42 & ! [Y] : % 7.30/7.42 ( object(Y) % 7.30/7.42 => ( exemplifies_property(none_greater,Y) % 7.30/7.42 => Y = X ) ) ) ) ). % 7.30/7.42 % 7.30/7.42 fof(premise_2,axiom, % 7.30/7.42 ! [X] : % 7.30/7.42 ( object(X) % 7.30/7.42 => ( ( is_the(X,none_greater) % 7.30/7.42 & ~ exemplifies_property(existence,X) ) % 7.30/7.42 => ? [Y] : % 7.30/7.42 ( object(Y) % 7.30/7.42 & exemplifies_relation(greater_than,Y,X) % 7.30/7.42 & exemplifies_property(conceivable,Y) ) ) ) ). % 7.30/7.42 % 7.30/7.42 fof(definition_god,axiom, % 7.30/7.42 is_the(god,none_greater) ). % 7.30/7.42 % 7.30/7.42 fof(god_exists,conjecture, % 7.30/7.42 exemplifies_property(existence,god) ). % 7.30/7.42 % 7.30/7.42 %------------------------------------------------------------------------------ % 7.30/7.42 %------------------------------------------- % 7.30/7.42 % Proof found % 7.30/7.42 % SZS status Theorem for theBenchmark % 7.30/7.42 % SZS output start Proof % 7.30/7.42 %ClaNum:41(EqnAxiom:17) % 7.30/7.42 %VarNum:108(SingletonVarNum:32) % 7.30/7.42 %MaxLitNum:6 % 7.30/7.42 %MaxfuncDepth:1 % 7.30/7.42 %SharedTerms:13 % 7.30/7.42 %goalClause: 21 % 7.30/7.42 %singleGoalClaCount:1 % 7.30/7.42 [18]P1(a1) % 7.30/7.42 [19]P2(a6,a1) % 7.30/7.42 [20]P3(a7,a6) % 7.30/7.42 [21]~P2(a8,a7) % 7.30/7.42 [22]P5(x221)+~P3(x222,x221) % 7.30/7.42 [23]P1(x231)+~P3(x231,x232) % 7.30/7.42 [24]~P1(x241)+~P2(a6,x241)+P1(a9) % 7.30/7.42 [25]~P1(x251)+~P2(a6,x251)+P2(a6,a9) % 7.30/7.42 [26]~P1(x261)+~P2(a6,x261)+P2(a2,x261) % 7.30/7.42 [27]~P1(x271)+P2(a8,x271)+~P3(x271,a6)+P1(f10(x271)) % 7.30/7.42 [28]~P1(x281)+P2(a6,x281)+~P2(a2,x281)+P1(f3(x281)) % 7.30/7.42 [30]~P1(x301)+~P3(x301,a6)+P2(a8,x301)+P2(a2,f10(x301)) % 7.30/7.42 [31]~P1(x311)+~P2(a2,x311)+P2(a6,x311)+P2(a2,f3(x311)) % 7.30/7.42 [39]~P1(x391)+~P3(x391,a6)+P2(a8,x391)+P4(a11,f10(x391),x391) % 7.30/7.42 [40]~P1(x401)+~P2(a2,x401)+P2(a6,x401)+P4(a11,f3(x401),x401) % 7.30/7.42 [29]~P1(x291)+~P1(x292)+~P2(a6,x292)+~P2(a6,x291)+E(x291,a9) % 7.30/7.42 [41]~P1(x411)+~P1(x412)+~P4(a11,x412,x411)+~P2(a6,x411)+~P2(a2,x412) % 7.30/7.42 [32]~P5(x321)+~P1(x322)+~P2(x321,x322)+~E(f5(x321,x322),x322)+P1(f4(x321)) % 7.30/7.42 [33]~P5(x331)+~P1(x332)+~P2(x331,x332)+P1(f4(x331))+P1(f5(x331,x332)) % 7.30/7.42 [35]~P5(x351)+~P1(x352)+~P2(x351,x352)+P3(f4(x351),x351)+~E(f5(x351,x352),x352) % 7.30/7.42 [36]~P5(x361)+~P1(x362)+~P2(x361,x362)+P2(x361,f5(x361,x362))+P1(f4(x361)) % 7.30/7.42 [37]~P5(x371)+~P1(x372)+~P2(x371,x372)+P3(f4(x371),x371)+P1(f5(x371,x372)) % 7.30/7.42 [38]~P5(x381)+~P1(x382)+~P2(x381,x382)+P3(f4(x381),x381)+P2(x381,f5(x381,x382)) % 7.30/7.42 [34]~P5(x341)+~P1(x342)+~P3(x342,x341)+~P3(x343,x341)+P2(x341,x342)+~P1(x343) % 7.30/7.42 %EqnAxiom % 7.30/7.42 [1]E(x11,x11) % 7.30/7.42 [2]E(x22,x21)+~E(x21,x22) % 7.30/7.42 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 7.30/7.42 [4]~E(x41,x42)+E(f10(x41),f10(x42)) % 7.30/7.42 [5]~E(x51,x52)+E(f3(x51),f3(x52)) % 7.30/7.42 [6]~E(x61,x62)+E(f5(x61,x63),f5(x62,x63)) % 7.30/7.42 [7]~E(x71,x72)+E(f5(x73,x71),f5(x73,x72)) % 7.30/7.42 [8]~E(x81,x82)+E(f4(x81),f4(x82)) % 7.30/7.42 [9]~P1(x91)+P1(x92)+~E(x91,x92) % 7.30/7.42 [10]P2(x102,x103)+~E(x101,x102)+~P2(x101,x103) % 7.30/7.42 [11]P2(x113,x112)+~E(x111,x112)+~P2(x113,x111) % 7.30/7.42 [12]P3(x122,x123)+~E(x121,x122)+~P3(x121,x123) % 7.30/7.42 [13]P3(x133,x132)+~E(x131,x132)+~P3(x133,x131) % 7.30/7.42 [14]~P5(x141)+P5(x142)+~E(x141,x142) % 7.30/7.42 [15]P4(x152,x153,x154)+~E(x151,x152)+~P4(x151,x153,x154) % 7.30/7.42 [16]P4(x163,x162,x164)+~E(x161,x162)+~P4(x163,x161,x164) % 7.30/7.42 [17]P4(x173,x174,x172)+~E(x171,x172)+~P4(x173,x174,x171) % 7.30/7.42 % 7.30/7.42 %------------------------------------------- % 7.30/7.42 cnf(42,plain, % 7.30/7.42 (P2(a2,a1)), % 7.30/7.42 inference(scs_inference,[],[18,19,26])). % 7.30/7.42 cnf(44,plain, % 7.30/7.42 (E(a1,a9)), % 7.30/7.42 inference(scs_inference,[],[18,19,26,29])). % 7.30/7.42 cnf(48,plain, % 7.30/7.42 (E(a9,a1)), % 7.30/7.42 inference(scs_inference,[],[18,19,26,29,41,2])). % 7.30/7.42 cnf(50,plain, % 7.30/7.42 (P2(a6,a9)), % 7.30/7.42 inference(scs_inference,[],[18,19,26,29,41,2,10,11])). % 7.30/7.42 cnf(51,plain, % 7.30/7.42 (P1(a9)), % 7.30/7.42 inference(scs_inference,[],[18,19,26,29,41,2,10,11,9])). % 7.30/7.42 cnf(52,plain, % 7.30/7.42 (P3(x521,a6)+~E(a7,x521)), % 7.30/7.42 inference(scs_inference,[],[18,19,20,26,29,41,2,10,11,9,12])). % 7.30/7.42 cnf(85,plain, % 7.30/7.42 (P2(a6,a7)+~P5(a6)+~P3(a1,a6)+~P1(a7)), % 7.30/7.42 inference(scs_inference,[],[20,18,34])). % 7.30/7.42 cnf(143,plain, % 7.30/7.42 (P1(f10(a7))), % 7.30/7.42 inference(scs_inference,[],[20,21,23,27])). % 7.30/7.42 cnf(1414,plain, % 7.30/7.42 (~E(a6,x14141)+P5(x14141)), % 7.30/7.42 inference(scs_inference,[],[20,22,14])). % 7.30/7.42 cnf(1415,plain, % 7.30/7.42 (P5(a6)), % 7.30/7.42 inference(equality_inference,[],[1414])). % 7.30/7.42 cnf(1419,plain, % 7.30/7.42 (P2(a6,a7)+~P3(a1,a6)+~P1(a7)), % 7.30/7.42 inference(scs_inference,[],[1415,85])). % 7.30/7.42 cnf(1447,plain, % 7.30/7.42 (~P1(a7)+~P3(a1,a6)+P2(a2,a7)), % 7.30/7.42 inference(scs_inference,[],[1419,26])). % 7.30/7.42 cnf(1495,plain, % 7.30/7.42 (~P3(a1,a6)+P2(a2,a7)), % 7.30/7.42 inference(scs_inference,[],[20,1447,23])). % 7.30/7.42 cnf(1511,plain, % 7.30/7.42 (P2(a2,a7)+~E(a7,a1)), % 7.30/7.42 inference(scs_inference,[],[1495,52])). % 7.30/7.42 cnf(1527,plain, % 7.30/7.42 (~E(a1,a7)+P2(a2,a7)), % 7.30/7.42 inference(scs_inference,[],[1511,2])). % 7.30/7.42 cnf(1543,plain, % 7.30/7.42 (~E(a9,a7)+P2(a2,a7)), % 7.30/7.42 inference(scs_inference,[],[44,1527,3])). % 7.30/7.42 cnf(1559,plain, % 7.30/7.42 (~E(a7,a9)+P2(a2,a7)), % 7.30/7.42 inference(scs_inference,[],[1543,2])). % 7.30/7.42 cnf(1575,plain, % 7.30/7.42 (~E(a2,a8)+~E(a7,a9)), % 7.30/7.42 inference(scs_inference,[],[21,1559,10])). % 7.30/7.42 cnf(1591,plain, % 7.30/7.42 (~E(a7,a1)+~E(a2,a8)), % 7.30/7.42 inference(scs_inference,[],[44,1575,3])). % 7.30/7.42 cnf(1607,plain, % 7.30/7.42 (~E(a8,a2)+~E(a7,a1)), % 7.30/7.42 inference(scs_inference,[],[1591,2])). % 7.30/7.42 cnf(1623,plain, % 7.30/7.42 (~E(a7,a9)+~E(a8,a2)), % 7.30/7.42 inference(scs_inference,[],[48,1607,3])). % 7.30/7.42 cnf(1639,plain, % 7.30/7.42 (~P1(a7)+~E(a8,a2)+~P2(a6,a7)), % 7.30/7.42 inference(scs_inference,[],[50,51,1623,29])). % 7.30/7.42 cnf(1688,plain, % 7.30/7.42 (~E(a2,a8)+~P2(a6,a7)+~P1(a7)), % 7.30/7.42 inference(scs_inference,[],[1639,2])). % 7.30/7.42 cnf(1704,plain, % 7.30/7.42 (~E(a2,a8)+~P2(a6,a7)), % 7.30/7.42 inference(scs_inference,[],[20,1688,23])). % 7.30/7.42 cnf(1720,plain, % 7.30/7.42 (~E(a8,a2)+~P2(a6,a7)), % 7.30/7.42 inference(scs_inference,[],[1704,2])). % 7.30/7.42 cnf(3628,plain, % 7.30/7.42 (P1(a7)), % 7.30/7.42 inference(scs_inference,[],[20,23])). % 7.30/7.42 cnf(3642,plain, % 7.30/7.42 (P2(a6,a7)), % 7.30/7.42 inference(scs_inference,[],[3628,20,1415,34])). % 7.30/7.42 cnf(3647,plain, % 7.30/7.42 (P2(a2,a7)), % 7.30/7.42 inference(scs_inference,[],[3628,21,20,1415,34,1704,1720,10,26])). % 7.30/7.42 cnf(3649,plain, % 7.30/7.42 (~P4(a11,a1,a7)), % 7.30/7.42 inference(scs_inference,[],[3628,21,20,42,1415,18,34,1704,1720,10,26,41])). % 7.30/7.42 cnf(3673,plain, % 7.30/7.42 (~P4(a11,x36731,a7)+~E(x36731,a7)), % 7.30/7.42 inference(scs_inference,[],[3647,3642,3628,41,16])). % 7.30/7.42 cnf(3714,plain, % 7.30/7.42 (P2(a2,f10(a7))), % 7.30/7.42 inference(scs_inference,[],[20,21,23,30])). % 7.30/7.42 cnf(3723,plain, % 7.30/7.42 (P4(a11,f10(a7),a7)), % 7.30/7.42 inference(scs_inference,[],[20,21,23,39])). % 7.30/7.42 cnf(3727,plain, % 7.30/7.42 ($false), % 7.30/7.42 inference(scs_inference,[],[3642,3723,3714,143,3649,3628,3673,2,16,41]), % 7.30/7.42 ['proof']). % 7.30/7.42 % SZS output end Proof % 7.30/7.42 % Total time :6.700000s %------------------------------------------------------------------------------