%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PHI009+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 : n003.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:53 EDT 2024 % Result : Theorem 0.51s 0.63s % Output : CNFRefutation 0.51s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : PHI009+1 : TPTP v8.2.0. Released v7.2.0. % 0.04/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n003.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 : 300 % 0.12/0.34 % DateTime : Tue Jun 18 20:17:24 EDT 2024 % 0.12/0.34 % CPUTime : % 0.19/0.54 start to proof:theBenchmark % 0.51/0.63 %------------------------------------------- % 0.51/0.63 % File :CSE---1.7 % 0.51/0.63 % Problem :theBenchmark % 0.51/0.63 % Transform :cnf % 0.51/0.63 % Format :tptp:raw % 0.51/0.63 % Command :java -jar mcs_scs.jar %d %s % 0.51/0.63 % 0.51/0.63 % Result :Theorem 0.020000s % 0.51/0.63 % Output :CNFRefutation 0.020000s % 0.51/0.63 %------------------------------------------- % 0.51/0.63 %------------------------------------------------------------------------------ % 0.51/0.63 % File : PHI009+1 : TPTP v8.2.0. Released v7.2.0. % 0.51/0.63 % Domain : Philosophy % 0.51/0.63 % Problem : Lemma for Anselm's ontological argument % 0.51/0.63 % Version : [Wol16] axioms. % 0.51/0.63 % English : % 0.51/0.63 % 0.51/0.63 % Refs : [OZ11] Oppenheimer & Zalta (2011), A Computationally-Discover % 0.51/0.63 % : [Wol16] Woltzenlogel Paleo (2016), Email to Geoff Sutcliffe % 0.51/0.63 % Source : [Wol16] % 0.51/0.63 % Names : descripthm1.p [Wol16] % 0.51/0.63 % 0.51/0.63 % Status : Theorem % 0.51/0.63 % Rating : 0.11 v8.1.0, 0.06 v7.4.0, 0.07 v7.2.0 % 0.51/0.63 % Syntax : Number of formulae : 2 ( 0 unt; 0 def) % 0.51/0.63 % Number of atoms : 19 ( 2 equ) % 0.51/0.63 % Maximal formula atoms : 11 ( 9 avg) % 0.51/0.63 % Number of connectives : 17 ( 0 ~; 0 |; 9 &) % 0.51/0.63 % ( 1 <=>; 7 =>; 0 <=; 0 <~>) % 0.51/0.63 % Maximal formula depth : 13 ( 12 avg) % 0.51/0.63 % Maximal term depth : 1 ( 1 avg) % 0.51/0.63 % Number of predicates : 5 ( 4 usr; 0 prp; 1-2 aty) % 0.51/0.63 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 0.51/0.63 % Number of variables : 9 ( 6 !; 3 ?) % 0.51/0.63 % SPC : FOF_THM_RFO_SEQ % 0.51/0.63 % 0.51/0.63 % Comments : See http://mally.stanford.edu/cm/ontological-argument/ % 0.51/0.63 %------------------------------------------------------------------------------ % 0.51/0.63 fof(description_axiom_schema_instance,axiom, % 0.51/0.63 ! [F,G,X] : % 0.51/0.63 ( ( property(F) % 0.51/0.63 & property(G) % 0.51/0.63 & object(X) ) % 0.51/0.63 => ( ( is_the(X,F) % 0.51/0.63 & exemplifies_property(G,X) ) % 0.51/0.63 <=> ? [Y] : % 0.51/0.63 ( object(Y) % 0.51/0.63 & exemplifies_property(F,Y) % 0.51/0.63 & ! [Z] : % 0.51/0.63 ( object(Z) % 0.51/0.63 => ( exemplifies_property(F,Z) % 0.51/0.63 => Z = Y ) ) % 0.51/0.63 & exemplifies_property(G,Y) ) ) ) ). % 0.51/0.63 % 0.51/0.63 fof(description_theorem_1,conjecture, % 0.51/0.63 ! [F] : % 0.51/0.63 ( property(F) % 0.51/0.63 => ( ? [Y] : % 0.51/0.63 ( object(Y) % 0.51/0.63 & exemplifies_property(F,Y) % 0.51/0.63 & ! [Z] : % 0.51/0.63 ( object(Z) % 0.51/0.63 => ( exemplifies_property(F,Z) % 0.51/0.63 => Z = Y ) ) ) % 0.51/0.63 => ? [U] : % 0.51/0.63 ( object(U) % 0.51/0.63 & is_the(U,F) ) ) ) ). % 0.51/0.63 % 0.51/0.63 %------------------------------------------------------------------------------ % 0.51/0.63 %------------------------------------------- % 0.51/0.63 % Proof found % 0.51/0.63 % SZS status Theorem for theBenchmark % 0.51/0.63 % SZS output start Proof % 0.51/0.64 %ClaNum:31(EqnAxiom:16) % 0.51/0.64 %VarNum:139(SingletonVarNum:39) % 0.51/0.64 %MaxLitNum:8 % 0.51/0.64 %MaxfuncDepth:1 % 0.51/0.64 %SharedTerms:5 % 0.51/0.64 %goalClause: 17 18 19 20 21 % 0.51/0.64 %singleGoalClaCount:3 % 0.51/0.64 [17]P1(a1) % 0.51/0.64 [18]P2(a4) % 0.51/0.64 [19]P3(a1,a4) % 0.51/0.64 [20]~P2(x201)+~P4(x201,a1) % 0.51/0.64 [21]~P2(x211)+~P3(a1,x211)+E(x211,a4) % 0.51/0.64 [23]~P1(x232)+~P1(x231)+~P2(x233)+~P4(x233,x231)+~P3(x232,x233)+P2(f2(x231,x232,x233)) % 0.51/0.64 [24]~P1(x242)+~P1(x241)+~P2(x243)+~P4(x243,x242)+~P3(x241,x243)+P3(x241,f2(x242,x241,x243)) % 0.51/0.64 [25]~P1(x252)+~P1(x251)+~P2(x253)+~P4(x253,x251)+~P3(x252,x253)+P3(x251,f2(x251,x252,x253)) % 0.51/0.64 [22]~P1(x223)+~P1(x222)+~P2(x224)+~P2(x221)+~P4(x224,x222)+~P3(x223,x224)+~P3(x222,x221)+E(x221,f2(x222,x223,x224)) % 0.51/0.64 [26]~P1(x263)+~P1(x262)+~P2(x264)+~P2(x261)+~P3(x263,x264)+~P3(x262,x264)+P4(x261,x262)+~E(f3(x262,x263,x261,x264),x264) % 0.51/0.64 [27]~P1(x273)+~P1(x271)+~P2(x274)+~P2(x272)+~P3(x273,x274)+~P3(x271,x274)+P3(x271,x272)+~E(f3(x273,x271,x272,x274),x274) % 0.51/0.64 [28]~P1(x283)+~P1(x282)+~P2(x284)+~P2(x281)+~P3(x283,x284)+~P3(x282,x284)+P4(x281,x282)+P2(f3(x282,x283,x281,x284)) % 0.51/0.64 [29]~P1(x293)+~P1(x291)+~P2(x294)+~P2(x292)+~P3(x293,x294)+~P3(x291,x294)+P3(x291,x292)+P2(f3(x293,x291,x292,x294)) % 0.51/0.64 [30]~P1(x303)+~P1(x302)+~P2(x304)+~P2(x301)+~P3(x303,x304)+~P3(x302,x304)+P4(x301,x302)+P3(x302,f3(x302,x303,x301,x304)) % 0.51/0.64 [31]~P1(x313)+~P1(x311)+~P2(x314)+~P2(x312)+~P3(x313,x314)+~P3(x311,x314)+P3(x311,x312)+P3(x313,f3(x313,x311,x312,x314)) % 0.51/0.64 %EqnAxiom % 0.51/0.64 [1]E(x11,x11) % 0.51/0.64 [2]E(x22,x21)+~E(x21,x22) % 0.51/0.64 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.51/0.64 [4]~E(x41,x42)+E(f2(x41,x43,x44),f2(x42,x43,x44)) % 0.51/0.64 [5]~E(x51,x52)+E(f2(x53,x51,x54),f2(x53,x52,x54)) % 0.51/0.64 [6]~E(x61,x62)+E(f2(x63,x64,x61),f2(x63,x64,x62)) % 0.51/0.64 [7]~E(x71,x72)+E(f3(x71,x73,x74,x75),f3(x72,x73,x74,x75)) % 0.51/0.64 [8]~E(x81,x82)+E(f3(x83,x81,x84,x85),f3(x83,x82,x84,x85)) % 0.51/0.64 [9]~E(x91,x92)+E(f3(x93,x94,x91,x95),f3(x93,x94,x92,x95)) % 0.51/0.64 [10]~E(x101,x102)+E(f3(x103,x104,x105,x101),f3(x103,x104,x105,x102)) % 0.51/0.64 [11]~P1(x111)+P1(x112)+~E(x111,x112) % 0.51/0.64 [12]~P2(x121)+P2(x122)+~E(x121,x122) % 0.51/0.64 [13]P3(x132,x133)+~E(x131,x132)+~P3(x131,x133) % 0.51/0.64 [14]P3(x143,x142)+~E(x141,x142)+~P3(x143,x141) % 0.51/0.64 [15]P4(x152,x153)+~E(x151,x152)+~P4(x151,x153) % 0.51/0.64 [16]P4(x163,x162)+~E(x161,x162)+~P4(x163,x161) % 0.51/0.64 % 0.51/0.64 %------------------------------------------- % 0.51/0.64 cnf(36,plain, % 0.51/0.64 (~E(a4,x361)+~P4(x361,a1)), % 0.51/0.64 inference(scs_inference,[],[18,20,12])). % 0.51/0.64 cnf(37,plain, % 0.51/0.64 (~P4(a4,a1)), % 0.51/0.64 inference(equality_inference,[],[36])). % 0.51/0.64 cnf(52,plain, % 0.51/0.64 (P2(f3(a1,a1,a4,a4))), % 0.51/0.64 inference(scs_inference,[],[37,19,17,18,15,28])). % 0.51/0.64 cnf(53,plain, % 0.51/0.64 (P3(a1,f3(a1,a1,a4,a4))), % 0.51/0.64 inference(scs_inference,[],[37,19,17,18,16,30])). % 0.51/0.64 cnf(56,plain, % 0.51/0.64 ($false), % 0.51/0.64 inference(scs_inference,[],[37,19,17,18,52,53,21,26]), % 0.51/0.64 ['proof']). % 0.51/0.64 % SZS output end Proof % 0.51/0.64 % Total time :0.020000s %------------------------------------------------------------------------------