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