%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PHI015+1 : TPTP v8.2.0. Released v7.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n010.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 17.21s 17.31s % Output : CNFRefutation 17.27s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : PHI015+1 : TPTP v8.2.0. Released v7.2.0. % 0.12/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n010.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 : 300 % 0.13/0.34 % DateTime : Tue Jun 18 20:16:09 EDT 2024 % 0.13/0.34 % CPUTime : % 0.20/0.57 start to proof:theBenchmark % 17.21/17.30 %------------------------------------------- % 17.21/17.30 % File :CSE---1.7 % 17.21/17.30 % Problem :theBenchmark % 17.21/17.30 % Transform :cnf % 17.21/17.30 % Format :tptp:raw % 17.21/17.30 % Command :java -jar mcs_scs.jar %d %s % 17.21/17.30 % 17.21/17.30 % Result :Theorem 16.680000s % 17.21/17.30 % Output :CNFRefutation 16.680000s % 17.21/17.30 %------------------------------------------- % 17.21/17.31 %------------------------------------------------------------------------------ % 17.21/17.31 % File : PHI015+1 : TPTP v8.2.0. Released v7.2.0. % 17.21/17.31 % Domain : Philosophy % 17.21/17.31 % Problem : Anselm's ontological argument, from the axioms % 17.21/17.31 % Version : [Wol16] axioms. % 17.21/17.31 % English : % 17.21/17.31 % 17.21/17.31 % Refs : [OZ11] Oppenheimer & Zalta (2011), A Computationally-Discover % 17.21/17.31 % : [Wol16] Woltzenlogel Paleo (2016), Email to Geoff Sutcliffe % 17.21/17.31 % Source : [Wol16] % 17.21/17.31 % Names : ontological.p [Wol16] % 17.21/17.31 % 17.21/17.31 % Status : Theorem % 17.21/17.31 % Rating : 0.11 v8.2.0, 0.08 v8.1.0, 0.06 v7.4.0, 0.07 v7.2.0 % 17.21/17.31 % Syntax : Number of formulae : 11 ( 2 unt; 0 def) % 17.21/17.31 % Number of atoms : 51 ( 5 equ) % 17.21/17.31 % Maximal formula atoms : 11 ( 4 avg) % 17.21/17.31 % Number of connectives : 43 ( 3 ~; 2 |; 22 &) % 17.21/17.31 % ( 3 <=>; 13 =>; 0 <=; 0 <~>) % 17.21/17.31 % Maximal formula depth : 13 ( 6 avg) % 17.21/17.31 % Maximal term depth : 1 ( 1 avg) % 17.21/17.31 % Number of predicates : 6 ( 5 usr; 0 prp; 1-3 aty) % 17.21/17.31 % Number of functors : 5 ( 5 usr; 5 con; 0-0 aty) % 17.21/17.31 % Number of variables : 22 ( 17 !; 5 ?) % 17.21/17.31 % SPC : FOF_THM_RFO_SEQ % 17.21/17.31 % 17.21/17.31 % Comments : See http://mally.stanford.edu/cm/ontological-argument/ % 17.21/17.31 %------------------------------------------------------------------------------ % 17.21/17.31 fof(objects_are_not_properties,axiom, % 17.21/17.31 ! [X] : % 17.21/17.31 ( object(X) % 17.21/17.31 => ~ property(X) ) ). % 17.21/17.31 % 17.21/17.31 fof(exemplifier_is_object_and_exemplified_is_property,axiom, % 17.21/17.31 ! [X,F] : % 17.21/17.31 ( exemplifies_property(F,X) % 17.21/17.31 => ( property(F) % 17.21/17.31 & object(X) ) ) ). % 17.21/17.31 % 17.21/17.31 fof(description_is_property_and_described_is_object,axiom, % 17.21/17.31 ! [X,F] : % 17.21/17.31 ( is_the(X,F) % 17.21/17.31 => ( property(F) % 17.21/17.31 & object(X) ) ) ). % 17.21/17.31 % 17.21/17.31 fof(description_axiom_schema_instance,axiom, % 17.21/17.31 ! [F,G,X] : % 17.21/17.31 ( ( property(F) % 17.21/17.31 & property(G) % 17.21/17.31 & object(X) ) % 17.21/17.31 => ( ( is_the(X,F) % 17.21/17.31 & exemplifies_property(G,X) ) % 17.21/17.31 <=> ? [Y] : % 17.21/17.31 ( object(Y) % 17.21/17.31 & exemplifies_property(F,Y) % 17.21/17.31 & ! [Z] : % 17.21/17.31 ( object(Z) % 17.21/17.31 => ( exemplifies_property(F,Z) % 17.21/17.31 => Z = Y ) ) % 17.21/17.31 & exemplifies_property(G,Y) ) ) ) ). % 17.21/17.31 % 17.21/17.31 fof(description_axiom_identity_instance,axiom, % 17.21/17.31 ! [F,X,W] : % 17.21/17.31 ( ( property(F) % 17.21/17.31 & object(X) % 17.21/17.31 & object(W) ) % 17.21/17.31 => ( ( is_the(X,F) % 17.21/17.31 & X = W ) % 17.21/17.31 <=> ? [Y] : % 17.21/17.31 ( object(Y) % 17.21/17.31 & exemplifies_property(F,Y) % 17.21/17.31 & ! [Z] : % 17.21/17.31 ( object(Z) % 17.21/17.31 => ( exemplifies_property(F,Z) % 17.21/17.31 => Z = Y ) ) % 17.21/17.31 & Y = W ) ) ) ). % 17.21/17.31 % 17.21/17.31 fof(connectedness_of_greater_than,axiom, % 17.21/17.31 ! [X,Y] : % 17.21/17.31 ( ( object(X) % 17.21/17.31 & object(Y) ) % 17.21/17.31 => ( exemplifies_relation(greater_than,X,Y) % 17.21/17.31 | exemplifies_relation(greater_than,Y,X) % 17.21/17.31 | X = Y ) ) ). % 17.21/17.31 % 17.21/17.31 fof(definition_none_greater,axiom, % 17.21/17.31 ! [X] : % 17.21/17.31 ( object(X) % 17.21/17.31 => ( exemplifies_property(none_greater,X) % 17.21/17.31 <=> ( exemplifies_property(conceivable,X) % 17.21/17.31 & ~ ? [Y] : % 17.21/17.31 ( object(Y) % 17.21/17.31 & exemplifies_relation(greater_than,Y,X) % 17.21/17.31 & exemplifies_property(conceivable,Y) ) ) ) ) ). % 17.21/17.31 % 17.21/17.31 fof(premise_1,axiom, % 17.21/17.31 ? [X] : % 17.21/17.31 ( object(X) % 17.21/17.31 & exemplifies_property(none_greater,X) ) ). % 17.21/17.31 % 17.21/17.31 fof(premise_2,axiom, % 17.21/17.31 ! [X] : % 17.21/17.31 ( object(X) % 17.21/17.31 => ( ( is_the(X,none_greater) % 17.21/17.31 & ~ exemplifies_property(existence,X) ) % 17.21/17.31 => ? [Y] : % 17.21/17.31 ( object(Y) % 17.21/17.31 & exemplifies_relation(greater_than,Y,X) % 17.21/17.31 & exemplifies_property(conceivable,Y) ) ) ) ). % 17.21/17.31 % 17.21/17.31 fof(definition_god,axiom, % 17.21/17.31 is_the(god,none_greater) ). % 17.21/17.31 % 17.21/17.31 fof(god_exists,conjecture, % 17.21/17.31 exemplifies_property(existence,god) ). % 17.21/17.31 % 17.21/17.31 %------------------------------------------------------------------------------ % 17.21/17.31 %------------------------------------------- % 17.21/17.31 % Proof found % 17.21/17.31 % SZS status Theorem for theBenchmark % 17.21/17.31 % SZS output start Proof % 17.21/17.31 %ClaNum:66(EqnAxiom:28) % 17.21/17.31 %VarNum:325(SingletonVarNum:94) % 17.21/17.31 %MaxLitNum:8 % 17.21/17.31 %MaxfuncDepth:1 % 17.21/17.31 %SharedTerms:10 % 17.21/17.31 %goalClause: 32 % 17.21/17.31 %singleGoalClaCount:1 % 17.21/17.31 [29]P1(a1) % 17.21/17.31 [30]P2(a8,a1) % 17.21/17.32 [31]P3(a9,a8) % 17.21/17.32 [32]~P2(a10,a9) % 17.21/17.32 [33]~P5(x331)+~P1(x331) % 17.21/17.32 [34]P1(x341)+~P2(x342,x341) % 17.21/17.32 [35]P1(x351)+~P3(x351,x352) % 17.21/17.32 [36]P5(x361)+~P2(x361,x362) % 17.21/17.32 [37]P5(x371)+~P3(x372,x371) % 17.21/17.32 [38]~P1(x381)+~P2(a8,x381)+P2(a2,x381) % 17.21/17.32 [39]~P1(x391)+P2(a10,x391)+~P3(x391,a8)+P1(f11(x391)) % 17.21/17.32 [40]~P1(x401)+P2(a8,x401)+~P2(a2,x401)+P1(f3(x401)) % 17.21/17.32 [41]~P1(x411)+~P3(x411,a8)+P2(a10,x411)+P2(a2,f11(x411)) % 17.21/17.32 [42]~P1(x421)+~P2(a2,x421)+P2(a8,x421)+P2(a2,f3(x421)) % 17.21/17.32 [43]~P1(x431)+~P3(x431,a8)+P2(a10,x431)+P4(a12,f11(x431),x431) % 17.21/17.32 [44]~P1(x441)+~P2(a2,x441)+P2(a8,x441)+P4(a12,f3(x441),x441) % 17.21/17.32 [46]~P1(x462)+~P1(x461)+E(x461,x462)+P4(a12,x462,x461)+P4(a12,x461,x462) % 17.21/17.32 [48]~P1(x481)+~P1(x482)+~P4(a12,x482,x481)+~P2(a8,x481)+~P2(a2,x482) % 17.21/17.32 [45]~E(x452,x453)+~P1(x453)+~P1(x452)+~P5(x451)+~P3(x452,x451)+E(f4(x451,x452,x453),x453) % 17.21/17.32 [50]~E(x502,x503)+~P1(x503)+~P1(x502)+~P5(x501)+~P3(x502,x501)+P1(f4(x501,x502,x503)) % 17.21/17.32 [51]~E(x512,x513)+~P1(x513)+~P1(x512)+~P5(x511)+~P3(x512,x511)+P2(x511,f4(x511,x512,x513)) % 17.21/17.32 [52]~P1(x523)+~P5(x522)+~P5(x521)+~P2(x522,x523)+~P3(x523,x521)+P1(f5(x521,x522,x523)) % 17.21/17.32 [53]~P1(x533)+~P5(x532)+~P5(x531)+~P2(x531,x533)+~P3(x533,x532)+P2(x531,f5(x532,x531,x533)) % 17.21/17.32 [54]~P1(x543)+~P5(x542)+~P5(x541)+~P2(x542,x543)+~P3(x543,x541)+P2(x541,f5(x541,x542,x543)) % 17.21/17.32 [47]~E(x473,x474)+~P1(x474)+~P1(x473)+~P1(x471)+~P5(x472)+~P2(x472,x471)+~P3(x473,x472)+E(x471,f4(x472,x473,x474)) % 17.21/17.32 [49]~P1(x494)+~P1(x491)+~P5(x493)+~P5(x492)+~P2(x493,x494)+~P2(x492,x491)+~P3(x494,x492)+E(x491,f5(x492,x493,x494)) % 17.21/17.32 [55]~P1(x553)+~P1(x552)+~P1(x551)+~P5(x554)+~P2(x554,x553)+E(x551,x552)+~E(x552,x553)+~E(f7(x554,x551,x552,x553),x553) % 17.21/17.32 [56]~P1(x564)+~P1(x563)+~P1(x561)+~P5(x562)+~P2(x562,x564)+P3(x561,x562)+~E(x563,x564)+~E(f7(x562,x561,x563,x564),x564) % 17.21/17.32 [57]~P1(x574)+~P1(x572)+~P5(x573)+~P5(x571)+~P2(x573,x574)+~P2(x571,x574)+P2(x571,x572)+~E(f6(x573,x571,x572,x574),x574) % 17.21/17.32 [58]~P1(x584)+~P1(x581)+~P5(x583)+~P5(x582)+~P2(x583,x584)+~P2(x582,x584)+P3(x581,x582)+~E(f6(x582,x583,x581,x584),x584) % 17.21/17.32 [59]~E(x592,x594)+~P1(x594)+~P1(x592)+~P1(x591)+~P5(x593)+~P2(x593,x594)+E(x591,x592)+P1(f7(x593,x591,x592,x594)) % 17.21/17.32 [60]~E(x602,x604)+~P1(x604)+~P1(x602)+~P1(x601)+~P5(x603)+~P2(x603,x604)+E(x601,x602)+P2(x603,f7(x603,x601,x602,x604)) % 17.21/17.32 [61]~E(x613,x614)+~P1(x614)+~P1(x613)+~P1(x611)+~P5(x612)+~P2(x612,x614)+P3(x611,x612)+P1(f7(x612,x611,x613,x614)) % 17.21/17.32 [62]~E(x623,x624)+~P1(x624)+~P1(x623)+~P1(x621)+~P5(x622)+~P2(x622,x624)+P3(x621,x622)+P2(x622,f7(x622,x621,x623,x624)) % 17.21/17.32 [63]~P1(x634)+~P1(x632)+~P5(x633)+~P5(x631)+~P2(x633,x634)+~P2(x631,x634)+P2(x631,x632)+P1(f6(x633,x631,x632,x634)) % 17.21/17.32 [64]~P1(x644)+~P1(x641)+~P5(x643)+~P5(x642)+~P2(x643,x644)+~P2(x642,x644)+P3(x641,x642)+P1(f6(x642,x643,x641,x644)) % 17.21/17.32 [65]~P1(x654)+~P1(x652)+~P5(x653)+~P5(x651)+~P2(x653,x654)+~P2(x651,x654)+P2(x651,x652)+P2(x653,f6(x653,x651,x652,x654)) % 17.27/17.32 [66]~P1(x664)+~P1(x661)+~P5(x663)+~P5(x662)+~P2(x663,x664)+~P2(x662,x664)+P3(x661,x662)+P2(x662,f6(x662,x663,x661,x664)) % 17.27/17.32 %EqnAxiom % 17.27/17.32 [1]E(x11,x11) % 17.27/17.32 [2]E(x22,x21)+~E(x21,x22) % 17.27/17.32 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 17.27/17.32 [4]~E(x41,x42)+E(f11(x41),f11(x42)) % 17.27/17.32 [5]~E(x51,x52)+E(f3(x51),f3(x52)) % 17.27/17.32 [6]~E(x61,x62)+E(f6(x61,x63,x64,x65),f6(x62,x63,x64,x65)) % 17.27/17.32 [7]~E(x71,x72)+E(f6(x73,x71,x74,x75),f6(x73,x72,x74,x75)) % 17.27/17.32 [8]~E(x81,x82)+E(f6(x83,x84,x81,x85),f6(x83,x84,x82,x85)) % 17.27/17.32 [9]~E(x91,x92)+E(f6(x93,x94,x95,x91),f6(x93,x94,x95,x92)) % 17.27/17.32 [10]~E(x101,x102)+E(f7(x101,x103,x104,x105),f7(x102,x103,x104,x105)) % 17.27/17.32 [11]~E(x111,x112)+E(f7(x113,x111,x114,x115),f7(x113,x112,x114,x115)) % 17.27/17.32 [12]~E(x121,x122)+E(f7(x123,x124,x121,x125),f7(x123,x124,x122,x125)) % 17.27/17.32 [13]~E(x131,x132)+E(f7(x133,x134,x135,x131),f7(x133,x134,x135,x132)) % 17.27/17.32 [14]~E(x141,x142)+E(f5(x141,x143,x144),f5(x142,x143,x144)) % 17.27/17.32 [15]~E(x151,x152)+E(f5(x153,x151,x154),f5(x153,x152,x154)) % 17.27/17.32 [16]~E(x161,x162)+E(f5(x163,x164,x161),f5(x163,x164,x162)) % 17.27/17.32 [17]~E(x171,x172)+E(f4(x171,x173,x174),f4(x172,x173,x174)) % 17.27/17.32 [18]~E(x181,x182)+E(f4(x183,x181,x184),f4(x183,x182,x184)) % 17.27/17.32 [19]~E(x191,x192)+E(f4(x193,x194,x191),f4(x193,x194,x192)) % 17.27/17.32 [20]~P1(x201)+P1(x202)+~E(x201,x202) % 17.27/17.32 [21]P2(x212,x213)+~E(x211,x212)+~P2(x211,x213) % 17.27/17.32 [22]P2(x223,x222)+~E(x221,x222)+~P2(x223,x221) % 17.27/17.32 [23]P3(x232,x233)+~E(x231,x232)+~P3(x231,x233) % 17.27/17.32 [24]P3(x243,x242)+~E(x241,x242)+~P3(x243,x241) % 17.27/17.32 [25]~P5(x251)+P5(x252)+~E(x251,x252) % 17.27/17.32 [26]P4(x262,x263,x264)+~E(x261,x262)+~P4(x261,x263,x264) % 17.27/17.32 [27]P4(x273,x272,x274)+~E(x271,x272)+~P4(x273,x271,x274) % 17.27/17.32 [28]P4(x283,x284,x282)+~E(x281,x282)+~P4(x283,x284,x281) % 17.27/17.32 % 17.27/17.32 %------------------------------------------- % 17.27/17.33 cnf(67,plain, % 17.27/17.33 (~P1(x671)+~P1(x671)+~P3(x671,x672)+~P5(x672)+E(f4(x672,x671,x671),x671)), % 17.27/17.33 inference(equality_inference,[],[45])). % 17.27/17.33 cnf(68,plain, % 17.27/17.33 (~P1(x681)+~P1(x681)+~P2(x682,x683)+~P3(x681,x682)+~P1(x683)+~P5(x682)+E(x683,f4(x682,x681,x681))), % 17.27/17.33 inference(equality_inference,[],[47])). % 17.27/17.33 cnf(87,plain, % 17.27/17.33 (P3(x871,a8)+~E(a9,x871)), % 17.27/17.33 inference(scs_inference,[],[29,30,31,33,36,37,21,38,48,22,23])). % 17.27/17.33 cnf(5951,plain, % 17.27/17.33 (P1(f11(a9))+~P1(a9)), % 17.27/17.33 inference(scs_inference,[],[31,32,34,41])). % 17.27/17.33 cnf(8521,plain, % 17.27/17.33 (P1(x85211)+~E(a9,x85211)), % 17.27/17.33 inference(scs_inference,[],[35,87])). % 17.27/17.33 cnf(8522,plain, % 17.27/17.33 (P1(a9)), % 17.27/17.33 inference(equality_inference,[],[8521])). % 17.27/17.33 cnf(8536,plain, % 17.27/17.33 (P1(f11(a9))), % 17.27/17.33 inference(scs_inference,[],[8522,5951])). % 17.27/17.33 cnf(17196,plain, % 17.27/17.33 (P4(a12,f11(a9),a9)), % 17.27/17.33 inference(scs_inference,[],[31,32,35,43])). % 17.27/17.33 cnf(19147,plain, % 17.27/17.33 (P2(a2,f11(a9))), % 17.27/17.33 inference(scs_inference,[],[31,32,35,41])). % 17.27/17.33 cnf(19152,plain, % 17.27/17.33 (~E(a1,a9)), % 17.27/17.33 inference(scs_inference,[],[17196,19147,30,29,8536,48,27,28,2])). % 17.27/17.33 cnf(19160,plain, % 17.27/17.33 (~P5(a8)+~E(a1,f4(a8,a9,a9))), % 17.27/17.33 inference(scs_inference,[],[31,19152,8522,3,67])). % 17.27/17.33 cnf(19463,plain, % 17.27/17.33 (~P5(a8)), % 17.27/17.33 inference(scs_inference,[],[31,29,8522,30,19160,68])). % 17.27/17.33 cnf(19464,plain, % 17.27/17.33 ($false), % 17.27/17.33 inference(scs_inference,[],[30,19463,36]), % 17.27/17.33 ['proof']). % 17.27/17.33 % SZS output end Proof % 17.27/17.33 % Total time :16.680000s %------------------------------------------------------------------------------