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