%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL506+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n004.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:16 AM UTC 2026
% Result : Theorem 0.24s 0.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL506+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.09/0.35 % Computer : n004.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Fri Sep 4 22:27:14 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.24/0.51 start to proof:theBenchmark
% 0.24/0.51 %-------------------------------------------
% 0.24/0.51 % File :CSE---1.7
% 0.24/0.51 % Problem :theBenchmark
% 0.24/0.51 % Transform :cnf
% 0.24/0.51 % Format :tptp:raw
% 0.24/0.51 % Command :java -jar mcs_scs.jar %d %s
% 0.24/0.51
% 0.24/0.51 % Result :Theorem 0.010618s
% 0.24/0.51 % Output :CNFRefutation 0.010618s
% 0.24/0.51 %-------------------------------------------
% 0.24/0.51 %------------------------------------------------------------------------------
% 0.24/0.51 % File : LCL506+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.24/0.51 % Domain : Logic Calculi (Propositional)
% 0.24/0.51 % Problem : Prove Hilbert's and_1 axiom from Rosser's axiomatization
% 0.24/0.51 % Version : [Zem73] axioms.
% 0.24/0.51 % English :
% 0.24/0.51
% 0.24/0.51 % Refs : [Zem73] Zeman (1973), Modal Logic, the Lewis-Modal systems
% 0.24/0.51 % : [Hal] Halleck (URL), John Halleck's Logic Systems
% 0.24/0.51 % Source : [TPTP]
% 0.24/0.51 % Names :
% 0.24/0.51
% 0.24/0.51 % Status : Theorem
% 0.24/0.51 % Rating : 0.00 v9.3.0
% 0.24/0.51 % Syntax : Number of formulae : 43 ( 12 unt; 0 def)
% 0.24/0.51 % Number of atoms : 77 ( 6 equ)
% 0.24/0.51 % Maximal formula atoms : 4 ( 1 avg)
% 0.24/0.51 % Number of connectives : 34 ( 0 ~; 0 |; 1 &)
% 0.24/0.51 % ( 26 <=>; 7 =>; 0 <=; 0 <~>)
% 0.24/0.51 % Maximal formula depth : 6 ( 3 avg)
% 0.24/0.51 % Maximal term depth : 5 ( 2 avg)
% 0.24/0.51 % Number of predicates : 33 ( 32 usr; 31 prp; 0-2 aty)
% 0.24/0.51 % Number of functors : 5 ( 5 usr; 0 con; 1-2 aty)
% 0.24/0.51 % Number of variables : 65 ( 65 !; 0 ?)
% 0.24/0.51 % SPC : FOF_THM_RFO_SEQ
% 0.24/0.51
% 0.24/0.51 % Comments :
% 0.24/0.51 % Bugfixes : v9.2.0 - Bugfix in LCL006+5.ax
% 0.24/0.51 %------------------------------------------------------------------------------
% 0.24/0.51 %----Include axioms of propositional logic
% 0.24/0.51 include('Axioms/LCL006+0.ax').
% 0.24/0.52 include('Axioms/LCL006+1.ax').
% 0.24/0.52 %----Include Rosser's axiomatization of propositional logic
% 0.24/0.52 include('Axioms/LCL006+5.ax').
% 0.24/0.52 %------------------------------------------------------------------------------
% 0.24/0.52 %----Operator definitions to reduce everything to and & not
% 0.24/0.52 fof(hilbert_op_or,axiom,
% 0.24/0.52 op_or ).
% 0.24/0.52
% 0.24/0.52 fof(hilbert_op_implies_and,axiom,
% 0.24/0.52 op_implies_and ).
% 0.24/0.52
% 0.24/0.52 fof(hilbert_op_equiv,axiom,
% 0.24/0.52 op_equiv ).
% 0.24/0.52
% 0.24/0.52 fof(hilbert_and_1,conjecture,
% 0.24/0.52 and_1 ).
% 0.24/0.52
% 0.24/0.52 %------------------------------------------------------------------------------
% 0.24/0.52 %-------------------------------------------
% 0.24/0.52 % Proof found
% 0.24/0.52 % SZS status Theorem for theBenchmark
% 0.24/0.52 % SZS output start Proof
% 0.24/0.52 %ClaNum:116(EqnAxiom:44)
% 0.24/0.52 %VarNum:128(SingletonVarNum:63)
% 0.24/0.52 %MaxLitNum:4
% 0.24/0.52 %MaxfuncDepth:4
% 0.24/0.52 %SharedTerms:228
% 0.24/0.52 %goalClause: 56
% 0.24/0.52 %singleGoalClaCount:1
% 0.24/0.52 [45]P1(a5000)
% 0.24/0.52 [46]P18(a5000)
% 0.24/0.52 [47]P2(a5000)
% 0.24/0.52 [48]P16(a5000)
% 0.24/0.52 [49]P17(a5000)
% 0.24/0.52 [51]P19(a5000)
% 0.24/0.52 [53]P20(a5000)
% 0.24/0.52 [55]P21(a5000)
% 0.24/0.52 [56]~P3(a5000)
% 0.24/0.52 [78]P5(a5000)+~P4(f47(a48,f47(a57,a48)))
% 0.24/0.52 [79]P26(a5000)+~P4(f47(a17,f60(a17,a18)))
% 0.24/0.52 [80]P25(a5000)+~P4(f47(a19,f60(a20,a19)))
% 0.24/0.52 [82]P27(a5000)+~P4(f47(a37,f60(a38,a37)))
% 0.24/0.52 [83]P3(a5000)+~P4(f47(f5(a6,a11),a6))
% 0.24/0.52 [84]P6(a5000)+~P4(f47(f5(a12,a13),a13))
% 0.24/0.52 [86]P28(a5000)+~P4(f47(f60(a39,a39),a39))
% 0.24/0.52 [94]P12(a5000)+~P4(f47(f4(a21,a25),f47(a21,a25)))
% 0.24/0.52 [95]P11(a5000)+~P4(f47(f4(a26,a28),f47(a28,a26)))
% 0.24/0.52 [96]P30(a5000)+~P4(f47(f60(a45,a46),f60(a46,a45)))
% 0.24/0.52 [99]P23(a5000)+~P4(f47(f47(f59(a49),f59(a50)),f47(a50,a49)))
% 0.24/0.52 [102]P14(a5000)+~P4(f47(f47(a58,f47(a58,a7)),f47(a58,a7)))
% 0.24/0.52 [89]P7(a5000)+~P4(f47(a40,f47(f59(a40),a43)))
% 0.24/0.52 [90]P10(a5000)+~P4(f47(f47(f59(a44),a44),a44))
% 0.24/0.52 [101]P8(a5000)+~P4(f47(a14,f47(a15,f5(a14,a15))))
% 0.24/0.52 [108]P15(a5000)+~P4(f47(f47(a8,a9),f47(f47(a9,a10),f47(a8,a10))))
% 0.24/0.52 [109]P13(a5000)+~P4(f47(f47(a29,a30),f47(f47(a30,a29),f4(a29,a30))))
% 0.24/0.52 [110]P9(a5000)+~P4(f47(f47(a33,a41),f47(f47(a41,a42),f47(a33,a42))))
% 0.24/0.52 [111]P31(a5000)+~P4(f47(f47(a51,a56),f47(f60(a52,a51),f60(a52,a56))))
% 0.24/0.52 [112]P32(a5000)+~P4(f47(f60(a53,f60(a54,a55)),f60(a54,f60(a53,a55))))
% 0.24/0.52 [115]P29(a5000)+~P4(f47(f47(a22,a23),f47(f47(a24,a23),f47(f60(a22,a24),a23))))
% 0.24/0.52 [70]~P2(a5000)+P4(f47(x701,f5(x701,x701)))
% 0.24/0.52 [77]~P28(a5000)+P4(f47(f60(x771,x771),x771))
% 0.24/0.52 [88]~P10(a5000)+P4(f47(f47(f59(x881),x881),x881))
% 0.24/0.52 [62]E(f60(f59(x621),x622),f47(x621,x622))+~P24(a5000)
% 0.24/0.52 [68]E(f5(f47(x681,x682),f47(x682,x681)),f4(x681,x682))+~P21(a5000)
% 0.24/0.52 [69]~P5(a5000)+P4(f47(x691,f47(x692,x691)))
% 0.24/0.52 [71]~P25(a5000)+P4(f47(x711,f60(x712,x711)))
% 0.24/0.52 [72]~P27(a5000)+P4(f47(x721,f60(x722,x721)))
% 0.24/0.52 [73]~P26(a5000)+P4(f47(x731,f60(x731,x732)))
% 0.24/0.52 [74]~P6(a5000)+P4(f47(f5(x741,x742),x742))
% 0.24/0.52 [76]~P16(a5000)+P4(f47(f5(x761,x762),x761))
% 0.24/0.52 [91]~P11(a5000)+P4(f47(f4(x911,x912),f47(x912,x911)))
% 0.24/0.52 [92]~P12(a5000)+P4(f47(f4(x921,x922),f47(x921,x922)))
% 0.24/0.52 [93]~P30(a5000)+P4(f47(f60(x931,x932),f60(x932,x931)))
% 0.24/0.52 [97]~P23(a5000)+P4(f47(f47(f59(x971),f59(x972)),f47(x972,x971)))
% 0.24/0.52 [100]~P14(a5000)+P4(f47(f47(x1001,f47(x1001,x1002)),f47(x1001,x1002)))
% 0.24/0.52 [64]~P20(a5000)+E(f59(f5(x641,f59(x642))),f47(x641,x642))
% 0.24/0.52 [66]~P22(a5000)+E(f59(f60(f59(x661),f59(x662))),f5(x661,x662))
% 0.24/0.52 [67]~P19(a5000)+E(f59(f5(f59(x671),f59(x672))),f60(x671,x672))
% 0.24/0.52 [87]~P7(a5000)+P4(f47(x871,f47(f59(x871),x872)))
% 0.24/0.52 [98]~P8(a5000)+P4(f47(x981,f47(x982,f5(x981,x982))))
% 0.24/0.52 [105]~P13(a5000)+P4(f47(f47(x1051,x1052),f47(f47(x1052,x1051),f4(x1051,x1052))))
% 0.24/0.52 [103]~P15(a5000)+P4(f47(f47(x1031,x1032),f47(f47(x1032,x1033),f47(x1031,x1033))))
% 0.24/0.52 [104]~P9(a5000)+P4(f47(f47(x1041,x1042),f47(f47(x1042,x1043),f47(x1041,x1043))))
% 0.24/0.52 [106]~P31(a5000)+P4(f47(f47(x1061,x1062),f47(f60(x1063,x1061),f60(x1063,x1062))))
% 0.24/0.52 [107]~P32(a5000)+P4(f47(f60(x1071,f60(x1072,x1073)),f60(x1072,f60(x1071,x1073))))
% 0.24/0.52 [113]~P29(a5000)+P4(f47(f47(x1131,x1132),f47(f47(x1133,x1132),f47(f60(x1131,x1133),x1132))))
% 0.24/0.52 [114]~P17(a5000)+P4(f47(f47(x1141,x1142),f47(f59(f5(x1142,x1143)),f59(f5(x1143,x1141)))))
% 0.24/0.52 [63]E(x631,x632)+~P18(a5000)+~P4(f4(x631,x632))
% 0.24/0.52 [65]P4(x651)+~P4(x652)+~P1(a5000)+~P4(f47(x652,x651))
% 0.24/0.52 %EqnAxiom
% 0.24/0.52 [1]E(x11,x11)
% 0.24/0.52 [2]E(x22,x21)+~E(x21,x22)
% 0.24/0.52 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.24/0.52 [4]~E(x41,x42)+E(f47(x41,x43),f47(x42,x43))
% 0.24/0.52 [5]~E(x51,x52)+E(f47(x53,x51),f47(x53,x52))
% 0.24/0.52 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63))
% 0.24/0.52 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72))
% 0.24/0.52 [8]~E(x81,x82)+E(f59(x81),f59(x82))
% 0.24/0.52 [9]~E(x91,x92)+E(f60(x91,x93),f60(x92,x93))
% 0.24/0.52 [10]~E(x101,x102)+E(f60(x103,x101),f60(x103,x102))
% 0.24/0.52 [11]~E(x111,x112)+E(f5(x111,x113),f5(x112,x113))
% 0.24/0.52 [12]~E(x121,x122)+E(f5(x123,x121),f5(x123,x122))
% 0.24/0.52 [13]~P1(x131)+P1(x132)+~E(x131,x132)
% 0.24/0.52 [14]~P18(x141)+P18(x142)+~E(x141,x142)
% 0.24/0.52 [15]~P2(x151)+P2(x152)+~E(x151,x152)
% 0.24/0.52 [16]~P16(x161)+P16(x162)+~E(x161,x162)
% 0.24/0.52 [17]~P17(x171)+P17(x172)+~E(x171,x172)
% 0.24/0.52 [18]~P19(x181)+P19(x182)+~E(x181,x182)
% 0.24/0.52 [19]~P9(x191)+P9(x192)+~E(x191,x192)
% 0.24/0.52 [20]~P20(x201)+P20(x202)+~E(x201,x202)
% 0.24/0.52 [21]~P4(x211)+P4(x212)+~E(x211,x212)
% 0.24/0.52 [22]~P21(x221)+P21(x222)+~E(x221,x222)
% 0.24/0.52 [23]~P25(x231)+P25(x232)+~E(x231,x232)
% 0.24/0.52 [24]~P3(x241)+P3(x242)+~E(x241,x242)
% 0.24/0.52 [25]~P31(x251)+P31(x252)+~E(x251,x252)
% 0.24/0.52 [26]~P32(x261)+P32(x262)+~E(x261,x262)
% 0.24/0.52 [27]~P28(x271)+P28(x272)+~E(x271,x272)
% 0.24/0.52 [28]~P13(x281)+P13(x282)+~E(x281,x282)
% 0.24/0.52 [29]~P6(x291)+P6(x292)+~E(x291,x292)
% 0.24/0.52 [30]~P15(x301)+P15(x302)+~E(x301,x302)
% 0.24/0.52 [31]~P14(x311)+P14(x312)+~E(x311,x312)
% 0.24/0.52 [32]~P8(x321)+P8(x322)+~E(x321,x322)
% 0.24/0.52 [33]~P5(x331)+P5(x332)+~E(x331,x332)
% 0.24/0.52 [34]~P24(x341)+P24(x342)+~E(x341,x342)
% 0.24/0.52 [35]~P29(x351)+P29(x352)+~E(x351,x352)
% 0.24/0.52 [36]~P23(x361)+P23(x362)+~E(x361,x362)
% 0.24/0.52 [37]~P7(x371)+P7(x372)+~E(x371,x372)
% 0.24/0.52 [38]~P10(x381)+P10(x382)+~E(x381,x382)
% 0.24/0.52 [39]~P26(x391)+P26(x392)+~E(x391,x392)
% 0.24/0.52 [40]~P27(x401)+P27(x402)+~E(x401,x402)
% 0.24/0.52 [41]~P30(x411)+P30(x412)+~E(x411,x412)
% 0.24/0.52 [42]~P22(x421)+P22(x422)+~E(x421,x422)
% 0.24/0.52 [43]~P11(x431)+P11(x432)+~E(x431,x432)
% 0.24/0.52 [44]~P12(x441)+P12(x442)+~E(x441,x442)
% 0.24/0.52
% 0.24/0.52 %-------------------------------------------
% 0.24/0.52 cnf(125,plain,
% 0.24/0.52 (P4(f47(f5(x1251,x1252),x1251))),
% 0.24/0.52 inference(scs_inference,[],[48,76])).
% 0.24/0.52 cnf(126,plain,
% 0.24/0.52 (~P4(f47(f5(a6,a11),a6))),
% 0.24/0.52 inference(scs_inference,[],[56,83])).
% 0.24/0.52 cnf(128,plain,
% 0.24/0.52 ($false),
% 0.24/0.52 inference(scs_inference,[],[126,125]),
% 0.24/0.52 ['proof']).
% 0.24/0.52 % SZS output end Proof
% 0.24/0.52 % Total time :0.010618s
%------------------------------------------------------------------------------