%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL491+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 : n031.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:15 AM UTC 2026
% Result : Theorem 0.25s 0.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL491+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.08/0.34 % Computer : n031.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 14:13:09 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.25/0.50 start to proof:theBenchmark
% 0.25/0.50 %-------------------------------------------
% 0.25/0.50 % File :CSE---1.7
% 0.25/0.50 % Problem :theBenchmark
% 0.25/0.50 % Transform :cnf
% 0.25/0.50 % Format :tptp:raw
% 0.25/0.50 % Command :java -jar mcs_scs.jar %d %s
% 0.25/0.50
% 0.25/0.50 % Result :Theorem 0.011553s
% 0.25/0.50 % Output :CNFRefutation 0.011553s
% 0.25/0.50 %-------------------------------------------
% 0.25/0.50 %------------------------------------------------------------------------------
% 0.25/0.50 % File : LCL491+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.25/0.50 % Domain : Logic Calculi (Propositional)
% 0.25/0.50 % Problem : Prove Hilbert's or_2 axiom from Principia's axiomatization
% 0.25/0.50 % Version : [RW10] axioms.
% 0.25/0.50 % English :
% 0.25/0.50
% 0.25/0.50 % Refs : [RW10] Russell & Whitehead (1910), Principia Mathmatica
% 0.25/0.51 % : [Hal] Halleck (URL), John Halleck's Logic Systems
% 0.25/0.51 % Source : [TPTP]
% 0.25/0.51 % Names :
% 0.25/0.51
% 0.25/0.51 % Status : Theorem
% 0.25/0.51 % Rating : 0.00 v9.3.0
% 0.25/0.51 % Syntax : Number of formulae : 45 ( 14 unt; 0 def)
% 0.25/0.51 % Number of atoms : 79 ( 6 equ)
% 0.25/0.51 % Maximal formula atoms : 4 ( 1 avg)
% 0.25/0.51 % Number of connectives : 34 ( 0 ~; 0 |; 1 &)
% 0.25/0.51 % ( 26 <=>; 7 =>; 0 <=; 0 <~>)
% 0.25/0.51 % Maximal formula depth : 6 ( 3 avg)
% 0.25/0.51 % Maximal term depth : 5 ( 2 avg)
% 0.25/0.51 % Number of predicates : 33 ( 32 usr; 31 prp; 0-2 aty)
% 0.25/0.51 % Number of functors : 5 ( 5 usr; 0 con; 1-2 aty)
% 0.25/0.51 % Number of variables : 65 ( 65 !; 0 ?)
% 0.25/0.51 % SPC : FOF_THM_RFO_SEQ
% 0.25/0.51
% 0.25/0.51 % Comments :
% 0.25/0.51 % Bugfixes : v9.2.0 - Bugfix in LCL006+4.ax
% 0.25/0.51 %------------------------------------------------------------------------------
% 0.25/0.51 %----Include axioms of propositional logic
% 0.25/0.51 include('Axioms/LCL006+0.ax').
% 0.25/0.51 include('Axioms/LCL006+1.ax').
% 0.25/0.51 %----Include Principia's axiomatization of propositional logic
% 0.25/0.51 include('Axioms/LCL006+4.ax').
% 0.25/0.51 %------------------------------------------------------------------------------
% 0.25/0.51 %----Operator definitions to reduce everything to and & not
% 0.25/0.51 fof(hilbert_op_or,axiom,
% 0.25/0.51 op_or ).
% 0.25/0.51
% 0.25/0.51 fof(hilbert_op_implies_and,axiom,
% 0.25/0.51 op_implies_and ).
% 0.25/0.51
% 0.25/0.51 fof(hilbert_op_equiv,axiom,
% 0.25/0.51 op_equiv ).
% 0.25/0.51
% 0.25/0.51 fof(hilbert_or_2,conjecture,
% 0.25/0.51 or_2 ).
% 0.25/0.51
% 0.25/0.51 %------------------------------------------------------------------------------
% 0.25/0.51 %-------------------------------------------
% 0.25/0.51 % Proof found
% 0.25/0.51 % SZS status Theorem for theBenchmark
% 0.25/0.51 % SZS output start Proof
% 0.25/0.51 %ClaNum:118(EqnAxiom:44)
% 0.25/0.51 %VarNum:128(SingletonVarNum:63)
% 0.25/0.51 %MaxLitNum:4
% 0.25/0.51 %MaxfuncDepth:4
% 0.25/0.51 %SharedTerms:230
% 0.25/0.51 %goalClause: 58
% 0.25/0.51 %singleGoalClaCount:1
% 0.25/0.51 [45]P1(a5000)
% 0.25/0.51 [46]P18(a5000)
% 0.25/0.51 [47]P19(a5000)
% 0.25/0.51 [48]P29(a5000)
% 0.25/0.51 [49]P30(a5000)
% 0.25/0.51 [50]P31(a5000)
% 0.25/0.51 [51]P32(a5000)
% 0.25/0.51 [52]P20(a5000)
% 0.25/0.51 [53]P21(a5000)
% 0.25/0.51 [54]P23(a5000)
% 0.25/0.51 [55]P25(a5000)
% 0.25/0.51 [57]P24(a5000)
% 0.25/0.51 [58]~P26(a5000)
% 0.25/0.51 [80]P3(a5000)+~P2(f47(a48,f47(a57,a48)))
% 0.25/0.51 [81]P27(a5000)+~P2(f47(a17,f60(a17,a18)))
% 0.25/0.51 [82]P26(a5000)+~P2(f47(a19,f60(a20,a19)))
% 0.25/0.51 [83]P15(a5000)+~P2(f47(a27,f5(a27,a27)))
% 0.25/0.51 [85]P5(a5000)+~P2(f47(f5(a6,a11),a6))
% 0.25/0.51 [86]P4(a5000)+~P2(f47(f5(a12,a13),a13))
% 0.25/0.51 [87]P16(a5000)+~P2(f47(f5(a31,a32),a31))
% 0.25/0.51 [96]P11(a5000)+~P2(f47(f4(a21,a25),f47(a21,a25)))
% 0.25/0.51 [97]P10(a5000)+~P2(f47(f4(a26,a28),f47(a28,a26)))
% 0.25/0.51 [101]P22(a5000)+~P2(f47(f47(f59(a49),f59(a50)),f47(a50,a49)))
% 0.25/0.51 [104]P13(a5000)+~P2(f47(f47(a58,f47(a58,a7)),f47(a58,a7)))
% 0.25/0.51 [91]P6(a5000)+~P2(f47(a40,f47(f59(a40),a43)))
% 0.25/0.51 [92]P9(a5000)+~P2(f47(f47(f59(a44),a44),a44))
% 0.25/0.51 [103]P7(a5000)+~P2(f47(a14,f47(a15,f5(a14,a15))))
% 0.25/0.51 [110]P14(a5000)+~P2(f47(f47(a8,a9),f47(f47(a9,a10),f47(a8,a10))))
% 0.25/0.51 [111]P12(a5000)+~P2(f47(f47(a29,a30),f47(f47(a30,a29),f4(a29,a30))))
% 0.25/0.51 [112]P8(a5000)+~P2(f47(f47(a33,a41),f47(f47(a41,a42),f47(a33,a42))))
% 0.25/0.51 [117]P28(a5000)+~P2(f47(f47(a22,a23),f47(f47(a24,a23),f47(f60(a22,a24),a23))))
% 0.25/0.51 [118]P17(a5000)+~P2(f47(f47(a34,a35),f47(f59(f5(a35,a36)),f59(f5(a36,a34)))))
% 0.25/0.51 [72]~P15(a5000)+P2(f47(x721,f5(x721,x721)))
% 0.25/0.51 [79]~P19(a5000)+P2(f47(f60(x791,x791),x791))
% 0.25/0.51 [90]~P9(a5000)+P2(f47(f47(f59(x901),x901),x901))
% 0.25/0.51 [64]E(f60(f59(x641),x642),f47(x641,x642))+~P25(a5000)
% 0.25/0.51 [70]E(f5(f47(x701,x702),f47(x702,x701)),f4(x701,x702))+~P24(a5000)
% 0.25/0.51 [71]~P3(a5000)+P2(f47(x711,f47(x712,x711)))
% 0.25/0.51 [74]~P29(a5000)+P2(f47(x741,f60(x742,x741)))
% 0.25/0.51 [75]~P27(a5000)+P2(f47(x751,f60(x751,x752)))
% 0.25/0.51 [76]~P4(a5000)+P2(f47(f5(x761,x762),x762))
% 0.25/0.51 [77]~P5(a5000)+P2(f47(f5(x771,x772),x771))
% 0.25/0.51 [78]~P16(a5000)+P2(f47(f5(x781,x782),x781))
% 0.25/0.51 [93]~P10(a5000)+P2(f47(f4(x931,x932),f47(x932,x931)))
% 0.25/0.51 [94]~P11(a5000)+P2(f47(f4(x941,x942),f47(x941,x942)))
% 0.25/0.51 [95]~P30(a5000)+P2(f47(f60(x951,x952),f60(x952,x951)))
% 0.25/0.51 [99]~P22(a5000)+P2(f47(f47(f59(x991),f59(x992)),f47(x992,x991)))
% 0.25/0.51 [102]~P13(a5000)+P2(f47(f47(x1021,f47(x1021,x1022)),f47(x1021,x1022)))
% 0.25/0.51 [66]~P23(a5000)+E(f59(f5(x661,f59(x662))),f47(x661,x662))
% 0.25/0.51 [68]~P21(a5000)+E(f59(f60(f59(x681),f59(x682))),f5(x681,x682))
% 0.25/0.51 [69]~P20(a5000)+E(f59(f5(f59(x691),f59(x692))),f60(x691,x692))
% 0.25/0.51 [89]~P6(a5000)+P2(f47(x891,f47(f59(x891),x892)))
% 0.25/0.51 [100]~P7(a5000)+P2(f47(x1001,f47(x1002,f5(x1001,x1002))))
% 0.25/0.51 [107]~P12(a5000)+P2(f47(f47(x1071,x1072),f47(f47(x1072,x1071),f4(x1071,x1072))))
% 0.25/0.51 [105]~P14(a5000)+P2(f47(f47(x1051,x1052),f47(f47(x1052,x1053),f47(x1051,x1053))))
% 0.25/0.51 [106]~P8(a5000)+P2(f47(f47(x1061,x1062),f47(f47(x1062,x1063),f47(x1061,x1063))))
% 0.25/0.51 [108]~P32(a5000)+P2(f47(f47(x1081,x1082),f47(f60(x1083,x1081),f60(x1083,x1082))))
% 0.25/0.51 [109]~P31(a5000)+P2(f47(f60(x1091,f60(x1092,x1093)),f60(x1092,f60(x1091,x1093))))
% 0.25/0.51 [115]~P28(a5000)+P2(f47(f47(x1151,x1152),f47(f47(x1153,x1152),f47(f60(x1151,x1153),x1152))))
% 0.25/0.51 [116]~P17(a5000)+P2(f47(f47(x1161,x1162),f47(f59(f5(x1162,x1163)),f59(f5(x1163,x1161)))))
% 0.25/0.51 [65]E(x651,x652)+~P18(a5000)+~P2(f4(x651,x652))
% 0.25/0.51 [67]P2(x671)+~P2(x672)+~P1(a5000)+~P2(f47(x672,x671))
% 0.25/0.51 %EqnAxiom
% 0.25/0.51 [1]E(x11,x11)
% 0.25/0.51 [2]E(x22,x21)+~E(x21,x22)
% 0.25/0.51 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.25/0.51 [4]~E(x41,x42)+E(f47(x41,x43),f47(x42,x43))
% 0.25/0.51 [5]~E(x51,x52)+E(f47(x53,x51),f47(x53,x52))
% 0.25/0.51 [6]~E(x61,x62)+E(f4(x61,x63),f4(x62,x63))
% 0.25/0.51 [7]~E(x71,x72)+E(f4(x73,x71),f4(x73,x72))
% 0.25/0.51 [8]~E(x81,x82)+E(f59(x81),f59(x82))
% 0.25/0.51 [9]~E(x91,x92)+E(f60(x91,x93),f60(x92,x93))
% 0.25/0.51 [10]~E(x101,x102)+E(f60(x103,x101),f60(x103,x102))
% 0.25/0.51 [11]~E(x111,x112)+E(f5(x111,x113),f5(x112,x113))
% 0.25/0.51 [12]~E(x121,x122)+E(f5(x123,x121),f5(x123,x122))
% 0.25/0.51 [13]~P1(x131)+P1(x132)+~E(x131,x132)
% 0.25/0.51 [14]~P18(x141)+P18(x142)+~E(x141,x142)
% 0.25/0.51 [15]~P19(x151)+P19(x152)+~E(x151,x152)
% 0.25/0.51 [16]~P29(x161)+P29(x162)+~E(x161,x162)
% 0.25/0.51 [17]~P30(x171)+P30(x172)+~E(x171,x172)
% 0.25/0.51 [18]~P31(x181)+P31(x182)+~E(x181,x182)
% 0.25/0.51 [19]~P32(x191)+P32(x192)+~E(x191,x192)
% 0.25/0.51 [20]~P20(x201)+P20(x202)+~E(x201,x202)
% 0.25/0.51 [21]~P21(x211)+P21(x212)+~E(x211,x212)
% 0.25/0.51 [22]~P23(x221)+P23(x222)+~E(x221,x222)
% 0.25/0.51 [23]~P25(x231)+P25(x232)+~E(x231,x232)
% 0.25/0.51 [24]~P24(x241)+P24(x242)+~E(x241,x242)
% 0.25/0.51 [25]~P2(x251)+P2(x252)+~E(x251,x252)
% 0.25/0.51 [26]~P26(x261)+P26(x262)+~E(x261,x262)
% 0.25/0.51 [27]~P17(x271)+P17(x272)+~E(x271,x272)
% 0.25/0.51 [28]~P8(x281)+P8(x282)+~E(x281,x282)
% 0.25/0.51 [29]~P14(x291)+P14(x292)+~E(x291,x292)
% 0.25/0.51 [30]~P16(x301)+P16(x302)+~E(x301,x302)
% 0.25/0.51 [31]~P13(x311)+P13(x312)+~E(x311,x312)
% 0.25/0.51 [32]~P7(x321)+P7(x322)+~E(x321,x322)
% 0.25/0.51 [33]~P4(x331)+P4(x332)+~E(x331,x332)
% 0.25/0.51 [34]~P22(x341)+P22(x342)+~E(x341,x342)
% 0.25/0.51 [35]~P5(x351)+P5(x352)+~E(x351,x352)
% 0.25/0.51 [36]~P27(x361)+P27(x362)+~E(x361,x362)
% 0.25/0.51 [37]~P28(x371)+P28(x372)+~E(x371,x372)
% 0.25/0.51 [38]~P10(x381)+P10(x382)+~E(x381,x382)
% 0.25/0.51 [39]~P11(x391)+P11(x392)+~E(x391,x392)
% 0.25/0.51 [40]~P12(x401)+P12(x402)+~E(x401,x402)
% 0.25/0.51 [41]~P3(x411)+P3(x412)+~E(x411,x412)
% 0.25/0.51 [42]~P15(x421)+P15(x422)+~E(x421,x422)
% 0.25/0.51 [43]~P6(x431)+P6(x432)+~E(x431,x432)
% 0.25/0.52 [44]~P9(x441)+P9(x442)+~E(x441,x442)
% 0.25/0.52
% 0.25/0.52 %-------------------------------------------
% 0.25/0.52 cnf(128,plain,
% 0.25/0.52 (P2(f47(x1281,f60(x1282,x1281)))),
% 0.25/0.52 inference(scs_inference,[],[48,74])).
% 0.25/0.52 cnf(130,plain,
% 0.25/0.52 (~P2(f47(a19,f60(a20,a19)))),
% 0.25/0.52 inference(scs_inference,[],[58,82])).
% 0.25/0.52 cnf(134,plain,
% 0.25/0.52 ($false),
% 0.25/0.52 inference(scs_inference,[],[130,128]),
% 0.25/0.52 ['proof']).
% 0.25/0.52 % SZS output end Proof
% 0.25/0.52 % Total time :0.011553s
%------------------------------------------------------------------------------