%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : PHI022+1 : TPTP v8.2.0. Released v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %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 : 300s
% DateTime : Mon Jun 24 13:33:55 EDT 2024
% Result : Theorem 0.49s 0.58s
% Output : CNFRefutation 0.49s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.10 % Problem : PHI022+1 : TPTP v8.2.0. Released v7.4.0.
% 0.05/0.10 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.10/0.30 % Computer : n021.cluster.edu
% 0.10/0.30 % Model : x86_64 x86_64
% 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.30 % Memory : 8042.1875MB
% 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.30 % CPULimit : 300
% 0.10/0.30 % WCLimit : 300
% 0.10/0.30 % DateTime : Tue Jun 18 20:25:09 EDT 2024
% 0.10/0.31 % CPUTime :
% 0.16/0.52 start to proof:theBenchmark
% 0.49/0.58 %-------------------------------------------
% 0.49/0.58 % File :CSE---1.7
% 0.49/0.58 % Problem :theBenchmark
% 0.49/0.58 % Transform :cnf
% 0.49/0.58 % Format :tptp:raw
% 0.49/0.58 % Command :java -jar mcs_scs.jar %d %s
% 0.49/0.58
% 0.49/0.58 % Result :Theorem 0.020000s
% 0.49/0.58 % Output :CNFRefutation 0.020000s
% 0.49/0.58 %-------------------------------------------
% 0.49/0.58 %------------------------------------------------------------------------------
% 0.49/0.58 % File : PHI022+1 : TPTP v8.2.0. Released v7.4.0.
% 0.49/0.58 % Domain : Philosophy
% 0.49/0.58 % Problem : Proof of SE from the DAPI conjoined with AA1, AA4, AA7, and AA8
% 0.49/0.58 % Version : [Hor19] axioms.
% 0.49/0.58 % English :
% 0.49/0.58
% 0.49/0.58 % Refs : [Hor19] Horner (2019), A Computationally Assisted Reconstructi
% 0.49/0.58 % [Hor20] Horner (2020), Email to Geoff Sutcliffe
% 0.49/0.58 % Source : [Hor20]
% 0.49/0.58 % Names : APPENDIX 7 [Hor19]
% 0.49/0.58
% 0.49/0.58 % Status : Theorem
% 0.49/0.58 % Rating : 0.08 v7.5.0, 0.09 v7.4.0
% 0.49/0.58 % Syntax : Number of formulae : 22 ( 0 unt; 0 def)
% 0.49/0.58 % Number of atoms : 72 ( 2 equ)
% 0.49/0.58 % Maximal formula atoms : 6 ( 3 avg)
% 0.49/0.58 % Number of connectives : 60 ( 10 ~; 4 |; 21 &)
% 0.49/0.58 % ( 12 <=>; 13 =>; 0 <=; 0 <~>)
% 0.49/0.58 % Maximal formula depth : 8 ( 5 avg)
% 0.49/0.58 % Maximal term depth : 1 ( 1 avg)
% 0.49/0.58 % Number of predicates : 49 ( 48 usr; 0 prp; 1-2 aty)
% 0.49/0.58 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 0.49/0.58 % Number of variables : 34 ( 34 !; 0 ?)
% 0.49/0.58 % SPC : FOF_THM_EPR_SEQ
% 0.49/0.58
% 0.49/0.58 % Comments :
% 0.49/0.58 %------------------------------------------------------------------------------
% 0.49/0.58 include('Axioms/PHI002+0.ax').
% 0.49/0.58 include('Axioms/PHI002+1.ax').
% 0.49/0.58 %------------------------------------------------------------------------------
% 0.49/0.58 fof(has_substance_being,axiom,
% 0.49/0.58 ! [X] :
% 0.49/0.58 ( substance(X)
% 0.49/0.58 => being(X) ) ).
% 0.49/0.58
% 0.49/0.58 fof(is_in_itself_is_self_caused,axiom,
% 0.49/0.58 ! [X] :
% 0.49/0.58 ( inItself(X)
% 0.49/0.58 => selfCaused(X) ) ).
% 0.49/0.58
% 0.49/0.58 fof(being_has_essense,axiom,
% 0.49/0.58 ! [X] :
% 0.49/0.58 ( being(X)
% 0.49/0.58 => hasEssence(X) ) ).
% 0.49/0.58
% 0.49/0.58 fof(essence_involves_existence_exists,axiom,
% 0.49/0.58 ! [X] :
% 0.49/0.58 ( ( essenceInvExistence(X)
% 0.49/0.58 & hasEssence(X) )
% 0.49/0.58 => exists(X) ) ).
% 0.49/0.58
% 0.49/0.58 fof(has_substance_exists,conjecture,
% 0.49/0.58 ! [X] :
% 0.49/0.58 ( substance(X)
% 0.49/0.58 => exists(X) ) ).
% 0.49/0.58
% 0.49/0.58 %------------------------------------------------------------------------------
% 0.49/0.58 %-------------------------------------------
% 0.49/0.58 % Proof found
% 0.49/0.58 % SZS status Theorem for theBenchmark
% 0.49/0.58 % SZS output start Proof
% 0.49/0.58 %ClaNum:130(EqnAxiom:70)
% 0.49/0.58 %VarNum:193(SingletonVarNum:94)
% 0.49/0.58 %MaxLitNum:5
% 0.49/0.59 %MaxfuncDepth:0
% 0.49/0.59 %SharedTerms:3
% 0.49/0.59 %goalClause: 71 72
% 0.49/0.59 %singleGoalClaCount:2
% 0.49/0.59 [71]P1(a1)
% 0.49/0.59 [72]~P2(a1)
% 0.49/0.59 [73]~P25(x731)+P24(x731)
% 0.49/0.59 [74]~P24(x741)+P3(x741)
% 0.49/0.59 [75]~P24(x751)+P37(x751)
% 0.49/0.59 [76]~P4(x761)+P1(x761)
% 0.49/0.59 [77]~P1(x771)+P25(x771)
% 0.49/0.59 [78]~P1(x781)+P5(x781)
% 0.49/0.59 [79]~P38(x791)+P6(x791)
% 0.49/0.59 [80]~P6(x801)+P38(x801)
% 0.49/0.59 [81]~P1(x811)+P8(x811)
% 0.49/0.59 [82]~P26(x821)+P8(x821)
% 0.49/0.59 [83]~P26(x831)+P4(x831)
% 0.49/0.59 [84]~P4(x841)+P14(x841)
% 0.49/0.59 [85]~P29(x851)+P27(x851)
% 0.49/0.59 [86]~P23(x861)+P22(x861)
% 0.49/0.59 [87]~P22(x871)+P23(x871)
% 0.49/0.59 [88]~P8(x881)+P34(x881)
% 0.49/0.59 [89]~P10(x891)+~P3(x891)
% 0.49/0.59 [108]~P28(x1081,x1081)+P2(x1081)
% 0.49/0.59 [96]~P30(x961)+P12(x961,x962)
% 0.49/0.59 [97]~P30(x971)+P46(x971,x972)
% 0.49/0.59 [98]~P45(x982)+P31(x981,x982)
% 0.49/0.59 [99]~P45(x991)+P16(x991,x992)
% 0.49/0.59 [100]~P45(x1001)+P17(x1001,x1002)
% 0.49/0.59 [101]~P18(x1012)+P20(x1011,x1012)
% 0.49/0.59 [102]~P42(x1021)+P41(x1021,x1022)
% 0.49/0.59 [103]~P48(x1031)+P19(x1031,x1032)
% 0.49/0.59 [109]P42(x1091)+~P41(x1091,x1092)
% 0.49/0.59 [110]P11(x1101,x1101)+P11(x1101,x1102)
% 0.49/0.59 [123]~P13(x1232,x1231)+~P36(x1231,x1232)
% 0.49/0.59 [124]~P15(x1242,x1241)+~P36(x1241,x1242)
% 0.49/0.59 [125]~P13(x1251,x1252)+~P36(x1251,x1252)
% 0.49/0.59 [126]~P15(x1261,x1262)+~P36(x1261,x1262)
% 0.49/0.59 [92]~P3(x921)+~P37(x921)+P24(x921)
% 0.49/0.59 [93]~P25(x931)+~P5(x931)+P1(x931)
% 0.49/0.59 [94]~P8(x941)+~P4(x941)+P26(x941)
% 0.49/0.59 [95]~P3(x951)+~P34(x951)+P2(x951)
% 0.49/0.59 [90]P40(x901)+P39(x901)+~P45(x902)
% 0.49/0.59 [107]~P27(x1071)+P29(x1071)+P7(x1072,x1071)
% 0.49/0.59 [111]P2(x1111)+~P28(x1111,x1112)+E(x1111,x1112)
% 0.49/0.59 [114]~P44(x1141,x1142)+P43(x1141)+~P1(x1142)
% 0.49/0.59 [115]~P9(x1151,x1152)+P32(x1151)+~P4(x1152)
% 0.49/0.59 [116]~P9(x1161,x1162)+P33(x1161)+~P4(x1162)
% 0.49/0.59 [117]~P27(x1171)+P29(x1171)+~P21(x1172,x1171)
% 0.49/0.59 [120]P28(x1201,x1201)+~P2(x1201)+P28(x1201,x1202)
% 0.49/0.59 [121]P47(x1211,x1212)+~P48(x1212)+P35(x1211,x1212)
% 0.49/0.59 [122]~P29(x1222)+~P7(x1221,x1222)+P21(x1221,x1222)
% 0.49/0.59 [127]~P46(x1271,x1272)+P30(x1271)+~P12(x1271,x1272)
% 0.49/0.59 [128]~P11(x1281,x1282)+P43(x1281)+~P28(x1281,x1282)
% 0.49/0.59 [105]~P43(x1052)+P1(x1051)+P28(x1052,x1053)
% 0.49/0.59 [106]~P43(x1062)+P1(x1061)+P11(x1062,x1063)
% 0.49/0.59 [118]~P43(x1181)+P44(x1181,x1182)+P28(x1181,x1183)
% 0.49/0.59 [119]~P43(x1191)+P44(x1191,x1192)+P11(x1191,x1193)
% 0.49/0.59 [113]~P1(x1131)+~P14(x1131)+P4(x1131)+P9(x1132,x1131)
% 0.49/0.59 [112]~P1(x1121)+~P14(x1121)+~P33(x1122)+P4(x1121)+~P32(x1122)
% 0.49/0.59 [129]~P31(x1292,x1291)+~P16(x1291,x1292)+~P17(x1291,x1292)+P45(x1291)+~P39(x1292)
% 0.49/0.59 [130]~P31(x1302,x1301)+~P16(x1301,x1302)+~P17(x1301,x1302)+P45(x1301)+~P40(x1302)
% 0.49/0.59 %EqnAxiom
% 0.49/0.59 [1]E(x11,x11)
% 0.49/0.59 [2]E(x22,x21)+~E(x21,x22)
% 0.49/0.59 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.49/0.59 [4]~P1(x41)+P1(x42)+~E(x41,x42)
% 0.49/0.59 [5]~P2(x51)+P2(x52)+~E(x51,x52)
% 0.49/0.59 [6]~P24(x61)+P24(x62)+~E(x61,x62)
% 0.49/0.59 [7]~P25(x71)+P25(x72)+~E(x71,x72)
% 0.49/0.59 [8]~P3(x81)+P3(x82)+~E(x81,x82)
% 0.49/0.59 [9]~P30(x91)+P30(x92)+~E(x91,x92)
% 0.49/0.59 [10]~P37(x101)+P37(x102)+~E(x101,x102)
% 0.49/0.59 [11]P15(x112,x113)+~E(x111,x112)+~P15(x111,x113)
% 0.49/0.59 [12]P15(x123,x122)+~E(x121,x122)+~P15(x123,x121)
% 0.49/0.59 [13]P17(x132,x133)+~E(x131,x132)+~P17(x131,x133)
% 0.49/0.59 [14]P17(x143,x142)+~E(x141,x142)+~P17(x143,x141)
% 0.49/0.59 [15]~P4(x151)+P4(x152)+~E(x151,x152)
% 0.49/0.59 [16]P13(x162,x163)+~E(x161,x162)+~P13(x161,x163)
% 0.49/0.59 [17]P13(x173,x172)+~E(x171,x172)+~P13(x173,x171)
% 0.49/0.59 [18]P16(x182,x183)+~E(x181,x182)+~P16(x181,x183)
% 0.49/0.59 [19]P16(x193,x192)+~E(x191,x192)+~P16(x193,x191)
% 0.49/0.59 [20]~P5(x201)+P5(x202)+~E(x201,x202)
% 0.49/0.59 [21]P31(x212,x213)+~E(x211,x212)+~P31(x211,x213)
% 0.49/0.59 [22]P31(x223,x222)+~E(x221,x222)+~P31(x223,x221)
% 0.49/0.59 [23]~P6(x231)+P6(x232)+~E(x231,x232)
% 0.49/0.59 [24]~P38(x241)+P38(x242)+~E(x241,x242)
% 0.49/0.59 [25]P44(x252,x253)+~E(x251,x252)+~P44(x251,x253)
% 0.49/0.59 [26]P44(x263,x262)+~E(x261,x262)+~P44(x263,x261)
% 0.49/0.59 [27]P9(x272,x273)+~E(x271,x272)+~P9(x271,x273)
% 0.49/0.59 [28]P9(x283,x282)+~E(x281,x282)+~P9(x283,x281)
% 0.49/0.59 [29]~P8(x291)+P8(x292)+~E(x291,x292)
% 0.49/0.59 [30]~P40(x301)+P40(x302)+~E(x301,x302)
% 0.49/0.59 [31]~P32(x311)+P32(x312)+~E(x311,x312)
% 0.49/0.59 [32]~P26(x321)+P26(x322)+~E(x321,x322)
% 0.49/0.59 [33]P35(x332,x333)+~E(x331,x332)+~P35(x331,x333)
% 0.49/0.59 [34]P35(x343,x342)+~E(x341,x342)+~P35(x343,x341)
% 0.49/0.59 [35]P11(x352,x353)+~E(x351,x352)+~P11(x351,x353)
% 0.49/0.59 [36]P11(x363,x362)+~E(x361,x362)+~P11(x363,x361)
% 0.49/0.59 [37]~P14(x371)+P14(x372)+~E(x371,x372)
% 0.49/0.59 [38]P12(x382,x383)+~E(x381,x382)+~P12(x381,x383)
% 0.49/0.59 [39]P12(x393,x392)+~E(x391,x392)+~P12(x393,x391)
% 0.49/0.59 [40]~P27(x401)+P27(x402)+~E(x401,x402)
% 0.49/0.59 [41]~P29(x411)+P29(x412)+~E(x411,x412)
% 0.49/0.59 [42]~P22(x421)+P22(x422)+~E(x421,x422)
% 0.49/0.59 [43]~P23(x431)+P23(x432)+~E(x431,x432)
% 0.49/0.59 [44]P7(x442,x443)+~E(x441,x442)+~P7(x441,x443)
% 0.49/0.59 [45]P7(x453,x452)+~E(x451,x452)+~P7(x453,x451)
% 0.49/0.59 [46]P41(x462,x463)+~E(x461,x462)+~P41(x461,x463)
% 0.49/0.59 [47]P41(x473,x472)+~E(x471,x472)+~P41(x473,x471)
% 0.49/0.59 [48]~P34(x481)+P34(x482)+~E(x481,x482)
% 0.49/0.59 [49]~P45(x491)+P45(x492)+~E(x491,x492)
% 0.49/0.59 [50]P21(x502,x503)+~E(x501,x502)+~P21(x501,x503)
% 0.49/0.59 [51]P21(x513,x512)+~E(x511,x512)+~P21(x513,x511)
% 0.49/0.59 [52]~P10(x521)+P10(x522)+~E(x521,x522)
% 0.49/0.59 [53]~P39(x531)+P39(x532)+~E(x531,x532)
% 0.49/0.59 [54]P28(x542,x543)+~E(x541,x542)+~P28(x541,x543)
% 0.49/0.59 [55]P28(x553,x552)+~E(x551,x552)+~P28(x553,x551)
% 0.49/0.59 [56]~P33(x561)+P33(x562)+~E(x561,x562)
% 0.49/0.59 [57]P47(x572,x573)+~E(x571,x572)+~P47(x571,x573)
% 0.49/0.59 [58]P47(x583,x582)+~E(x581,x582)+~P47(x583,x581)
% 0.49/0.59 [59]P36(x592,x593)+~E(x591,x592)+~P36(x591,x593)
% 0.49/0.59 [60]P36(x603,x602)+~E(x601,x602)+~P36(x603,x601)
% 0.49/0.59 [61]~P48(x611)+P48(x612)+~E(x611,x612)
% 0.49/0.59 [62]~P42(x621)+P42(x622)+~E(x621,x622)
% 0.49/0.59 [63]~P43(x631)+P43(x632)+~E(x631,x632)
% 0.49/0.59 [64]P20(x642,x643)+~E(x641,x642)+~P20(x641,x643)
% 0.49/0.59 [65]P20(x653,x652)+~E(x651,x652)+~P20(x653,x651)
% 0.49/0.59 [66]P19(x662,x663)+~E(x661,x662)+~P19(x661,x663)
% 0.49/0.59 [67]P19(x673,x672)+~E(x671,x672)+~P19(x673,x671)
% 0.49/0.59 [68]~P18(x681)+P18(x682)+~E(x681,x682)
% 0.49/0.59 [69]P46(x692,x693)+~E(x691,x692)+~P46(x691,x693)
% 0.49/0.59 [70]P46(x703,x702)+~E(x701,x702)+~P46(x703,x701)
% 0.49/0.59
% 0.49/0.59 %-------------------------------------------
% 0.49/0.59 cnf(140,plain,
% 0.49/0.59 (P34(a1)),
% 0.49/0.59 inference(scs_inference,[],[71,81,88])).
% 0.49/0.59 cnf(145,plain,
% 0.49/0.59 (~P25(a1)),
% 0.49/0.59 inference(scs_inference,[],[72,140,95,74,73])).
% 0.49/0.59 cnf(148,plain,
% 0.49/0.59 ($false),
% 0.49/0.59 inference(scs_inference,[],[71,145,77]),
% 0.49/0.59 ['proof']).
% 0.49/0.59 % SZS output end Proof
% 0.49/0.59 % Total time :0.020000s
%------------------------------------------------------------------------------