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