%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL456+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 11:19:13 AM UTC 2026
% Result : Theorem 49.18s 49.32s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL456+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.02 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.08/0.34 % Computer : n002.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Fri Sep 4 18:45:20 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.25/0.51 start to proof:theBenchmark
% 49.18/49.31 %-------------------------------------------
% 49.18/49.31 % File :CSE---1.7
% 49.18/49.31 % Problem :theBenchmark
% 49.18/49.31 % Transform :cnf
% 49.18/49.31 % Format :tptp:raw
% 49.18/49.31 % Command :java -jar mcs_scs.jar %d %s
% 49.18/49.31
% 49.18/49.31 % Result :Theorem 48.809614s
% 49.18/49.31 % Output :CNFRefutation 48.809614s
% 49.18/49.31 %-------------------------------------------
% 49.18/49.32 %------------------------------------------------------------------------------
% 49.18/49.32 % File : LCL456+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 49.18/49.32 % Domain : Logic calculi
% 49.18/49.32 % Problem : Prove Principia's r3 axiom from Hilbert's axiomatization
% 49.18/49.32 % Version : [HB34] axioms.
% 49.18/49.32 % English :
% 49.18/49.32
% 49.18/49.32 % Refs : [HB34] Hilbert & Bernays (1934), Grundlagen der Mathematick
% 49.18/49.32 % : [Hal] Halleck (URL), John Halleck's Logic Systems
% 49.18/49.32 % Source : [TPTP]
% 49.18/49.32 % Names :
% 49.18/49.32
% 49.18/49.32 % Status : Theorem
% 49.18/49.32 % Rating : 1.00 v9.3.0
% 49.18/49.32 % Syntax : Number of formulae : 53 ( 22 unt; 0 def)
% 49.18/49.32 % Number of atoms : 87 ( 6 equ)
% 49.18/49.32 % Maximal formula atoms : 4 ( 1 avg)
% 49.18/49.32 % Number of connectives : 34 ( 0 ~; 0 |; 1 &)
% 49.18/49.32 % ( 26 <=>; 7 =>; 0 <=; 0 <~>)
% 49.18/49.32 % Maximal formula depth : 6 ( 3 avg)
% 49.18/49.32 % Maximal term depth : 5 ( 2 avg)
% 49.18/49.32 % Number of predicates : 33 ( 32 usr; 31 prp; 0-2 aty)
% 49.18/49.32 % Number of functors : 5 ( 5 usr; 0 con; 1-2 aty)
% 49.18/49.32 % Number of variables : 65 ( 65 !; 0 ?)
% 49.18/49.32 % SPC : FOF_THM_RFO_SEQ
% 49.18/49.32
% 49.18/49.32 % Comments :
% 49.18/49.32 % Bugfixes : v9.2.0 - Bugfix in LCL006+2.ax
% 49.18/49.32 %------------------------------------------------------------------------------
% 49.18/49.32 %----Include axioms of propositional logic
% 49.18/49.32 include('Axioms/LCL006+0.ax').
% 49.18/49.32 include('Axioms/LCL006+1.ax').
% 49.18/49.32 %----Include Hilbert's axiomatization of propositional logic
% 49.18/49.32 include('Axioms/LCL006+2.ax').
% 49.18/49.32 %------------------------------------------------------------------------------
% 49.18/49.32 %----Operator definitions to reduce everything to and & not
% 49.18/49.32 fof(principia_op_implies_or,axiom,
% 49.18/49.32 op_implies_or ).
% 49.18/49.32
% 49.18/49.32 fof(principia_op_and,axiom,
% 49.18/49.32 op_and ).
% 49.18/49.32
% 49.18/49.32 fof(principia_op_equiv,axiom,
% 49.18/49.32 op_equiv ).
% 49.18/49.32
% 49.18/49.32 fof(principia_r3,conjecture,
% 49.18/49.32 r3 ).
% 49.18/49.32
% 49.18/49.32 %------------------------------------------------------------------------------
% 49.18/49.32 %-------------------------------------------
% 49.18/49.32 % Proof found
% 49.18/49.32 % SZS status Theorem for theBenchmark
% 49.18/49.32 % SZS output start Proof
% 49.18/49.32 %ClaNum:126(EqnAxiom:44)
% 49.18/49.32 %VarNum:127(SingletonVarNum:63)
% 49.18/49.32 %MaxLitNum:4
% 49.18/49.32 %MaxfuncDepth:4
% 49.18/49.32 %SharedTerms:230
% 49.18/49.32 %goalClause: 66
% 49.18/49.32 %singleGoalClaCount:1
% 49.18/49.32 [45]P1(a5000)
% 49.18/49.32 [46]P18(a5000)
% 49.18/49.32 [47]P19(a5000)
% 49.18/49.32 [48]P2(a5000)
% 49.18/49.32 [49]P12(a5000)
% 49.18/49.32 [50]P13(a5000)
% 49.18/49.32 [51]P3(a5000)
% 49.18/49.32 [52]P4(a5000)
% 49.18/49.32 [53]P5(a5000)
% 49.18/49.32 [54]P20(a5000)
% 49.18/49.32 [55]P26(a5000)
% 49.18/49.32 [56]P27(a5000)
% 49.18/49.32 [57]P6(a5000)
% 49.18/49.32 [58]P10(a5000)
% 49.18/49.32 [59]P11(a5000)
% 49.18/49.32 [60]P21(a5000)
% 49.18/49.32 [61]P22(a5000)
% 49.18/49.32 [62]P23(a5000)
% 49.18/49.32 [63]P25(a5000)
% 49.18/49.32 [65]P24(a5000)
% 49.18/49.32 [66]~P28(a5000)
% 49.18/49.32 [91]P15(a5000)+~P14(f47(a27,f5(a27,a27)))
% 49.18/49.32 [92]P29(a5000)+~P14(f47(a37,f60(a38,a37)))
% 49.18/49.32 [95]P16(a5000)+~P14(f47(f5(a31,a32),a31))
% 49.18/49.32 [96]P30(a5000)+~P14(f47(f60(a39,a39),a39))
% 49.18/49.32 [106]P28(a5000)+~P14(f47(f60(a45,a46),f60(a46,a45)))
% 49.18/49.32 [99]P7(a5000)+~P14(f47(a40,f47(f59(a40),a43)))
% 49.18/49.32 [100]P9(a5000)+~P14(f47(f47(f59(a44),a44),a44))
% 49.18/49.32 [120]P8(a5000)+~P14(f47(f47(a33,a41),f47(f47(a41,a42),f47(a33,a42))))
% 49.18/49.32 [121]P31(a5000)+~P14(f47(f47(a51,a56),f47(f60(a52,a51),f60(a52,a56))))
% 49.18/49.32 [122]P32(a5000)+~P14(f47(f60(a53,f60(a54,a55)),f60(a54,f60(a53,a55))))
% 49.18/49.32 [126]P17(a5000)+~P14(f47(f47(a34,a35),f47(f59(f5(a35,a36)),f59(f5(a36,a34)))))
% 49.18/49.32 [80]~P15(a5000)+P14(f47(x801,f5(x801,x801)))
% 49.18/49.32 [87]~P30(a5000)+P14(f47(f60(x871,x871),x871))
% 49.18/49.32 [98]~P9(a5000)+P14(f47(f47(f59(x981),x981),x981))
% 49.18/49.32 [72]E(f60(f59(x721),x722),f47(x721,x722))+~P25(a5000)
% 49.18/49.32 [78]E(f5(f47(x781,x782),f47(x782,x781)),f4(x781,x782))+~P24(a5000)
% 49.18/49.32 [79]~P2(a5000)+P14(f47(x791,f47(x792,x791)))
% 49.18/49.32 [81]~P26(a5000)+P14(f47(x811,f60(x812,x811)))
% 49.18/49.32 [82]~P29(a5000)+P14(f47(x821,f60(x822,x821)))
% 49.18/49.32 [83]~P20(a5000)+P14(f47(x831,f60(x831,x832)))
% 49.18/49.32 [84]~P4(a5000)+P14(f47(f5(x841,x842),x842))
% 49.18/49.32 [85]~P3(a5000)+P14(f47(f5(x851,x852),x851))
% 49.18/49.32 [86]~P16(a5000)+P14(f47(f5(x861,x862),x861))
% 49.18/49.32 [101]~P10(a5000)+P14(f47(f4(x1011,x1012),f47(x1012,x1011)))
% 49.18/49.32 [102]~P6(a5000)+P14(f47(f4(x1021,x1022),f47(x1021,x1022)))
% 49.18/49.32 [107]~P19(a5000)+P14(f47(f47(f59(x1071),f59(x1072)),f47(x1072,x1071)))
% 49.18/49.32 [110]~P12(a5000)+P14(f47(f47(x1101,f47(x1101,x1102)),f47(x1101,x1102)))
% 49.18/49.32 [74]~P23(a5000)+E(f59(f5(x741,f59(x742))),f47(x741,x742))
% 49.18/49.32 [76]~P22(a5000)+E(f59(f60(f59(x761),f59(x762))),f5(x761,x762))
% 49.18/49.32 [77]~P21(a5000)+E(f59(f5(f59(x771),f59(x772))),f60(x771,x772))
% 49.18/49.32 [97]~P7(a5000)+P14(f47(x971,f47(f59(x971),x972)))
% 49.18/49.32 [108]~P5(a5000)+P14(f47(x1081,f47(x1082,f5(x1081,x1082))))
% 49.18/49.32 [115]~P11(a5000)+P14(f47(f47(x1151,x1152),f47(f47(x1152,x1151),f4(x1151,x1152))))
% 49.18/49.32 [113]~P13(a5000)+P14(f47(f47(x1131,x1132),f47(f47(x1132,x1133),f47(x1131,x1133))))
% 49.18/49.32 [114]~P8(a5000)+P14(f47(f47(x1141,x1142),f47(f47(x1142,x1143),f47(x1141,x1143))))
% 49.18/49.32 [116]~P31(a5000)+P14(f47(f47(x1161,x1162),f47(f60(x1163,x1161),f60(x1163,x1162))))
% 49.18/49.33 [117]~P32(a5000)+P14(f47(f60(x1171,f60(x1172,x1173)),f60(x1172,f60(x1171,x1173))))
% 49.18/49.33 [123]~P27(a5000)+P14(f47(f47(x1231,x1232),f47(f47(x1233,x1232),f47(f60(x1231,x1233),x1232))))
% 49.18/49.33 [124]~P17(a5000)+P14(f47(f47(x1241,x1242),f47(f59(f5(x1242,x1243)),f59(f5(x1243,x1241)))))
% 49.18/49.33 [73]E(x731,x732)+~P18(a5000)+~P14(f4(x731,x732))
% 49.18/49.33 [75]P14(x751)+~P14(x752)+~P1(a5000)+~P14(f47(x752,x751))
% 49.18/49.33 %EqnAxiom
% 49.18/49.33 [1]E(x11,x11)
% 49.18/49.33 [2]E(x22,x21)+~E(x21,x22)
% 49.18/49.33 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 49.18/49.33 [4]~E(x41,x42)+E(f47(x41,x43),f47(x42,x43))
% 49.18/49.33 [5]~E(x51,x52)+E(f47(x53,x51),f47(x53,x52))
% 49.18/49.33 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63))
% 49.18/49.33 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72))
% 49.18/49.33 [8]~E(x81,x82)+E(f59(x81),f59(x82))
% 49.18/49.33 [9]~E(x91,x92)+E(f60(x91,x93),f60(x92,x93))
% 49.18/49.33 [10]~E(x101,x102)+E(f60(x103,x101),f60(x103,x102))
% 49.18/49.33 [11]~E(x111,x112)+E(f5(x111,x113),f5(x112,x113))
% 49.18/49.33 [12]~E(x121,x122)+E(f5(x123,x121),f5(x123,x122))
% 49.18/49.33 [13]~P1(x131)+P1(x132)+~E(x131,x132)
% 49.18/49.33 [14]~P18(x141)+P18(x142)+~E(x141,x142)
% 49.18/49.33 [15]~P19(x151)+P19(x152)+~E(x151,x152)
% 49.18/49.33 [16]~P2(x161)+P2(x162)+~E(x161,x162)
% 49.18/49.33 [17]~P12(x171)+P12(x172)+~E(x171,x172)
% 49.18/49.33 [18]~P13(x181)+P13(x182)+~E(x181,x182)
% 49.18/49.33 [19]~P3(x191)+P3(x192)+~E(x191,x192)
% 49.18/49.33 [20]~P4(x201)+P4(x202)+~E(x201,x202)
% 49.18/49.33 [21]~P5(x211)+P5(x212)+~E(x211,x212)
% 49.18/49.33 [22]~P20(x221)+P20(x222)+~E(x221,x222)
% 49.18/49.33 [23]~P26(x231)+P26(x232)+~E(x231,x232)
% 49.18/49.33 [24]~P27(x241)+P27(x242)+~E(x241,x242)
% 49.18/49.33 [25]~P6(x251)+P6(x252)+~E(x251,x252)
% 49.18/49.33 [26]~P10(x261)+P10(x262)+~E(x261,x262)
% 49.18/49.33 [27]~P11(x271)+P11(x272)+~E(x271,x272)
% 49.18/49.33 [28]~P21(x281)+P21(x282)+~E(x281,x282)
% 49.18/49.33 [29]~P22(x291)+P22(x292)+~E(x291,x292)
% 49.18/49.33 [30]~P23(x301)+P23(x302)+~E(x301,x302)
% 49.18/49.33 [31]~P25(x311)+P25(x312)+~E(x311,x312)
% 49.18/49.33 [32]~P24(x321)+P24(x322)+~E(x321,x322)
% 49.18/49.33 [33]~P14(x331)+P14(x332)+~E(x331,x332)
% 49.18/49.33 [34]~P28(x341)+P28(x342)+~E(x341,x342)
% 49.18/49.33 [35]~P17(x351)+P17(x352)+~E(x351,x352)
% 49.18/49.33 [36]~P32(x361)+P32(x362)+~E(x361,x362)
% 49.18/49.33 [37]~P15(x371)+P15(x372)+~E(x371,x372)
% 49.18/49.33 [38]~P29(x381)+P29(x382)+~E(x381,x382)
% 49.18/49.33 [39]~P9(x391)+P9(x392)+~E(x391,x392)
% 49.18/49.33 [40]~P7(x401)+P7(x402)+~E(x401,x402)
% 49.18/49.33 [41]~P31(x411)+P31(x412)+~E(x411,x412)
% 49.18/49.33 [42]~P8(x421)+P8(x422)+~E(x421,x422)
% 49.18/49.33 [43]~P30(x431)+P30(x432)+~E(x431,x432)
% 49.18/49.33 [44]~P16(x441)+P16(x442)+~E(x441,x442)
% 49.18/49.33
% 49.18/49.33 %-------------------------------------------
% 49.18/49.33 cnf(132,plain,
% 49.18/49.33 (P14(x1321)+~P14(x1322)+~P14(f47(x1322,x1321))),
% 49.18/49.33 inference(scs_inference,[],[45,75])).
% 49.18/49.33 cnf(137,plain,
% 49.18/49.33 (P14(f47(x1371,f60(x1372,x1371)))),
% 49.18/49.33 inference(scs_inference,[],[55,81])).
% 49.18/49.33 cnf(138,plain,
% 49.18/49.33 (P14(f47(x1381,f60(x1381,x1382)))),
% 49.18/49.33 inference(scs_inference,[],[54,83])).
% 49.18/49.33 cnf(143,plain,
% 49.18/49.33 (~P14(f47(f60(a45,a46),f60(a46,a45)))),
% 49.18/49.33 inference(scs_inference,[],[66,106])).
% 49.18/49.33 cnf(149,plain,
% 49.18/49.33 (P14(f47(f47(x1491,x1492),f47(f47(x1493,x1492),f47(f60(x1491,x1493),x1492))))),
% 49.18/49.33 inference(scs_inference,[],[56,123])).
% 49.18/49.33 cnf(3934,plain,
% 49.18/49.33 (P14(f47(f47(x39341,f60(x39342,x39343)),f47(f60(x39343,x39341),f60(x39342,x39343))))),
% 49.18/49.33 inference(scs_inference,[],[137,149,132])).
% 49.18/49.33 cnf(3949,plain,
% 49.18/49.33 ($false),
% 49.18/49.33 inference(scs_inference,[],[3934,143,138,132]),
% 49.18/49.33 ['proof']).
% 49.18/49.33 % SZS output end Proof
% 49.18/49.33 % Total time :48.809614s
%------------------------------------------------------------------------------