%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL036-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/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:18:33 AM UTC 2026
% Result : Unsatisfiable 81.43s 81.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL036-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/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 : Sat Sep 5 06:40:39 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.24/0.51 start to proof:theBenchmark
% 81.43/81.55 %-------------------------------------------
% 81.43/81.55 % File :CSE---1.7
% 81.43/81.55 % Problem :theBenchmark
% 81.43/81.55 % Transform :cnf
% 81.43/81.55 % Format :tptp:raw
% 81.43/81.55 % Command :java -jar mcs_scs.jar %d %s
% 81.43/81.55
% 81.43/81.55 % Result :Theorem 81.055567s
% 81.43/81.55 % Output :CNFRefutation 81.055567s
% 81.43/81.55 %-------------------------------------------
% 81.43/81.55 %--------------------------------------------------------------------------
% 81.43/81.55 % File : LCL036-1 : TPTP v9.3.1. Released v1.0.0.
% 81.43/81.55 % Domain : Logic Calculi (Implication/Falsehood 2 valued sentential)
% 81.43/81.55 % Problem : C0-5 depends on the Meredith axiom
% 81.43/81.55 % Version : [McC92] axioms.
% 81.43/81.55 % English : Axiomatisations for the Implication/Falsehood 2 valued
% 81.43/81.55 % sentential calculus are {C0-1,C0-2,C0-3,C0-4}
% 81.43/81.55 % by Tarski-Bernays, {C0-2,C0-5,C0-6} by Church, and the single
% 81.43/81.55 % Meredith axioms. Show that C0-5 can be derived from the
% 81.43/81.55 % single Meredith axiom.
% 81.43/81.55
% 81.43/81.55 % Refs : [MW92] McCune & Wos (1992), Experiments in Automated Deductio
% 81.43/81.55 % : [McC92] McCune (1992), Email to G. Sutcliffe
% 81.43/81.55 % Source : [McC92]
% 81.43/81.55 % Names : C0-48 [MW92]
% 81.43/81.55
% 81.43/81.55 % Status : Unsatisfiable
% 81.43/81.55 % Rating : 0.00 v6.1.0, 0.14 v6.0.0, 0.00 v5.5.0, 0.19 v5.4.0, 0.22 v5.3.0, 0.30 v5.2.0, 0.15 v5.1.0, 0.25 v5.0.0, 0.20 v4.1.0, 0.27 v4.0.1, 0.00 v3.1.0, 0.17 v2.7.0, 0.25 v2.6.0, 0.29 v2.5.0, 0.00 v2.4.0, 0.00 v2.3.0, 0.14 v2.2.1, 0.56 v2.1.0, 0.63 v2.0.0
% 81.43/81.55 % Syntax : Number of clauses : 3 ( 2 unt; 0 nHn; 2 RR)
% 81.43/81.55 % Number of literals : 5 ( 0 equ; 3 neg)
% 81.43/81.55 % Maximal clause size : 3 ( 1 avg)
% 81.43/81.55 % Maximal term depth : 6 ( 2 avg)
% 81.43/81.55 % Number of predicates : 1 ( 1 usr; 0 prp; 1-1 aty)
% 81.43/81.55 % Number of functors : 3 ( 3 usr; 2 con; 0-2 aty)
% 81.43/81.55 % Number of variables : 7 ( 2 sgn)
% 81.43/81.55 % SPC : CNF_UNS_RFO_NEQ_HRN
% 81.43/81.55
% 81.43/81.55 % Comments :
% 81.43/81.55 %--------------------------------------------------------------------------
% 81.43/81.55 cnf(condensed_detachment,axiom,
% 81.43/81.55 ( ~ is_a_theorem(implies(X,Y))
% 81.43/81.55 | ~ is_a_theorem(X)
% 81.43/81.55 | is_a_theorem(Y) ) ).
% 81.43/81.55
% 81.43/81.55 cnf(c0_CAMeredith,axiom,
% 81.43/81.55 is_a_theorem(implies(implies(implies(implies(implies(X,Y),implies(Z,falsehood)),U),V),implies(implies(V,X),implies(Z,X)))) ).
% 81.43/81.55
% 81.43/81.55 cnf(prove_c0_5,negated_conjecture,
% 81.43/81.55 ~ is_a_theorem(implies(implies(implies(a,falsehood),falsehood),a)) ).
% 81.43/81.55
% 81.43/81.55 %--------------------------------------------------------------------------
% 81.43/81.56 %-------------------------------------------
% 81.43/81.56 % Proof found
% 81.43/81.56 % SZS status Theorem for theBenchmark
% 81.43/81.56 % SZS output start Proof
% 81.43/81.56 %ClaNum:3(EqnAxiom:0)
% 81.43/81.56 %VarNum:13(SingletonVarNum:7)
% 81.43/81.56 %MaxLitNum:3
% 81.43/81.56 %MaxfuncDepth:3
% 81.43/81.56 %SharedTerms:6
% 81.43/81.56 %goalClause: 2
% 81.43/81.56 %singleGoalClaCount:1
% 81.43/81.56 [2]~P1(f1(f1(f1(a3,a2),a2),a3))
% 81.43/81.56 [1]P1(f1(f1(f1(f1(f1(x11,x12),f1(x13,a2)),x14),x15),f1(f1(x15,x11),f1(x13,x11))))
% 81.43/81.56 [3]P1(x31)+~P1(x32)+~P1(f1(x32,x31))
% 81.43/81.56 %EqnAxiom
% 81.43/81.56
% 81.43/81.56 %-------------------------------------------
% 81.43/81.56 cnf(4,plain,
% 81.43/81.56 (P1(f1(f1(x41,x42),f1(x43,x42)))+~P1(f1(f1(f1(f1(x42,x44),f1(x43,a2)),x45),x41))),
% 81.43/81.56 inference(scs_inference,[],[1,3])).
% 81.43/81.56 cnf(6,plain,
% 81.43/81.56 (P1(f1(f1(f1(f1(x61,x62),f1(x63,x62)),f1(x62,x64)),f1(x65,f1(x62,x64))))),
% 81.43/81.56 inference(scs_inference,[],[1,4])).
% 81.43/81.56 cnf(7,plain,
% 81.43/81.56 (P1(f1(f1(f1(f1(f1(x71,x72),f1(x73,a2)),x74),x75),f1(f1(x75,x71),f1(x73,x71))))),
% 81.43/81.56 inference(rename_variables,[],[1])).
% 81.43/81.56 cnf(9,plain,
% 81.43/81.56 (P1(f1(f1(f1(x91,f1(a2,x92)),x93),f1(x94,x93)))),
% 81.43/81.56 inference(scs_inference,[],[1,7,4,3])).
% 81.43/81.56 cnf(12,plain,
% 81.43/81.56 (P1(f1(f1(f1(x121,x122),x123),f1(a2,x123)))),
% 81.43/81.56 inference(scs_inference,[],[9,4])).
% 81.43/81.56 cnf(13,plain,
% 81.43/81.56 (P1(f1(f1(f1(x131,f1(a2,x132)),x133),f1(x134,x133)))),
% 81.43/81.56 inference(rename_variables,[],[9])).
% 81.43/81.56 cnf(15,plain,
% 81.43/81.56 (P1(f1(x151,f1(f1(a2,x152),f1(x153,f1(a2,x152)))))),
% 81.43/81.56 inference(scs_inference,[],[6,9,13,4,3])).
% 81.43/81.56 cnf(20,plain,
% 81.43/81.56 (P1(f1(x201,f1(f1(a2,x202),f1(x203,f1(a2,x202)))))),
% 81.43/81.56 inference(rename_variables,[],[15])).
% 81.43/81.56 cnf(22,plain,
% 81.43/81.56 (P1(f1(f1(a2,x221),f1(x222,f1(a2,x221))))),
% 81.43/81.56 inference(scs_inference,[],[15,20,12,4,3])).
% 81.43/81.56 cnf(25,plain,
% 81.43/81.56 (P1(f1(f1(f1(a2,x251),x252),f1(x253,x252)))),
% 81.43/81.56 inference(scs_inference,[],[12,4])).
% 81.43/81.56 cnf(34,plain,
% 81.43/81.56 (P1(f1(x341,f1(a2,f1(f1(a2,x342),f1(x343,f1(a2,x342))))))),
% 81.43/81.56 inference(scs_inference,[],[22,15,3])).
% 81.43/81.56 cnf(51,plain,
% 81.43/81.56 (P1(f1(a2,f1(x511,x512)))),
% 81.43/81.56 inference(scs_inference,[],[9,12,3])).
% 81.43/81.56 cnf(54,plain,
% 81.43/81.56 (~P1(a2)),
% 81.43/81.56 inference(scs_inference,[],[51,2,3])).
% 81.43/81.56 cnf(61,plain,
% 81.43/81.56 (P1(f1(x611,f1(x612,f1(x613,x612))))),
% 81.43/81.56 inference(scs_inference,[],[25,6,3])).
% 81.43/81.56 cnf(70,plain,
% 81.43/81.56 (P1(f1(x701,f1(x702,x701)))),
% 81.43/81.56 inference(scs_inference,[],[34,61,3])).
% 81.43/81.56 cnf(80,plain,
% 81.43/81.56 (P1(f1(f1(f1(x801,f1(f1(x802,x801),f1(x803,x801))),x804),f1(x805,x804)))),
% 81.43/81.56 inference(scs_inference,[],[70,6,3,4])).
% 81.43/81.56 cnf(103,plain,
% 81.43/81.56 (P1(f1(f1(f1(x1031,f1(f1(f1(x1032,x1033),f1(x1034,a2)),x1035)),x1032),f1(x1034,x1032)))),
% 81.43/81.56 inference(scs_inference,[],[70,4])).
% 81.43/81.56 cnf(106,plain,
% 81.43/81.56 (P1(f1(f1(f1(x1061,x1062),x1063),f1(f1(f1(x1062,x1064),f1(x1061,a2)),x1063)))),
% 81.43/81.56 inference(scs_inference,[],[103,4])).
% 81.43/81.56 cnf(109,plain,
% 81.43/81.56 (P1(f1(f1(f1(f1(f1(f1(x1091,a2),x1092),f1(f1(x1093,x1094),a2)),x1095),x1093),f1(x1091,x1093)))),
% 81.43/81.56 inference(scs_inference,[],[106,4])).
% 81.43/81.56 cnf(112,plain,
% 81.43/81.56 (P1(f1(f1(f1(x1121,x1122),f1(f1(x1121,a2),x1123)),f1(x1124,f1(f1(x1121,a2),x1123))))),
% 81.43/81.56 inference(scs_inference,[],[109,4])).
% 81.43/81.56 cnf(115,plain,
% 81.43/81.56 (P1(f1(x1151,f1(f1(f1(f1(x1152,x1153),f1(x1154,x1153)),a2),f1(x1153,x1155))))),
% 81.43/81.56 inference(scs_inference,[],[6,109,4,3])).
% 81.43/81.56 cnf(118,plain,
% 81.43/81.56 (P1(f1(f1(f1(x1181,f1(f1(f1(x1182,x1183),a2),x1184)),x1182),f1(x1185,x1182)))),
% 81.43/81.56 inference(scs_inference,[],[112,4])).
% 81.43/81.56 cnf(124,plain,
% 81.43/81.56 (P1(f1(f1(f1(x1241,x1242),x1243),f1(f1(f1(x1242,x1244),a2),x1243)))),
% 81.43/81.56 inference(scs_inference,[],[118,4])).
% 81.43/81.56 cnf(160,plain,
% 81.43/81.56 (P1(f1(x1601,f1(f1(x1602,a2),f1(x1602,x1603))))),
% 81.43/81.56 inference(scs_inference,[],[70,112,3])).
% 81.43/81.56 cnf(164,plain,
% 81.43/81.56 (P1(f1(f1(f1(f1(x1641,a2),f1(x1641,x1642)),x1643),f1(x1644,x1643)))),
% 81.43/81.56 inference(scs_inference,[],[70,112,3,4])).
% 81.43/81.56 cnf(166,plain,
% 81.43/81.56 (P1(f1(f1(f1(x1661,x1662),x1663),f1(x1663,x1663)))),
% 81.43/81.56 inference(scs_inference,[],[164,4])).
% 81.43/81.56 cnf(172,plain,
% 81.43/81.56 (P1(f1(f1(f1(x1721,x1721),x1722),f1(x1723,x1722)))),
% 81.43/81.56 inference(scs_inference,[],[166,4])).
% 81.43/81.56 cnf(173,plain,
% 81.43/81.56 (P1(f1(f1(f1(x1731,x1732),x1733),f1(x1733,x1733)))),
% 81.43/81.56 inference(rename_variables,[],[166])).
% 81.43/81.56 cnf(175,plain,
% 81.43/81.56 (P1(f1(f1(x1751,f1(x1752,x1753)),f1(x1751,f1(x1752,x1753))))),
% 81.43/81.56 inference(scs_inference,[],[70,166,173,4,3])).
% 81.43/81.56 cnf(179,plain,
% 81.43/81.56 (P1(f1(f1(f1(f1(f1(x1791,x1792),f1(x1793,a2)),f1(x1794,x1795)),x1791),f1(x1793,x1791)))),
% 81.43/81.56 inference(scs_inference,[],[175,4])).
% 81.43/81.56 cnf(182,plain,
% 81.43/81.56 (~P1(f1(f1(x1821,x1821),a3))),
% 81.43/81.56 inference(scs_inference,[],[172,175,2,4,3])).
% 81.43/81.56 cnf(185,plain,
% 81.43/81.56 (P1(f1(f1(f1(x1851,x1852),f1(x1852,x1853)),f1(x1854,f1(x1852,x1853))))),
% 81.43/81.56 inference(scs_inference,[],[179,4])).
% 81.43/81.56 cnf(191,plain,
% 81.43/81.56 (P1(f1(f1(f1(x1911,f1(f1(x1912,a2),x1913)),x1914),f1(x1912,x1914)))),
% 81.43/81.56 inference(scs_inference,[],[185,4])).
% 81.43/81.56 cnf(194,plain,
% 81.43/81.56 (P1(f1(f1(x1941,a2),f1(x1941,x1942)))),
% 81.43/81.56 inference(scs_inference,[],[70,185,160,4,3])).
% 81.43/81.56 cnf(197,plain,
% 81.43/81.56 (P1(f1(f1(f1(x1971,x1972),x1973),f1(f1(x1971,a2),x1973)))),
% 81.43/81.56 inference(scs_inference,[],[191,4])).
% 81.43/81.56 cnf(200,plain,
% 81.43/81.56 (~P1(f1(f1(f1(a3,a2),a2),a2))),
% 81.43/81.56 inference(scs_inference,[],[191,194,2,4,3])).
% 81.43/81.56 cnf(204,plain,
% 81.43/81.56 (P1(f1(f1(f1(x2041,x2042),x2043),f1(f1(x2041,a2),x2043)))),
% 81.43/81.56 inference(rename_variables,[],[197])).
% 81.43/81.56 cnf(206,plain,
% 81.43/81.56 (~P1(f1(f1(f1(a3,a2),x2061),a3))),
% 81.43/81.56 inference(scs_inference,[],[197,204,2,4,3])).
% 81.43/81.56 cnf(209,plain,
% 81.43/81.56 (P1(f1(f1(f1(f1(f1(x2091,x2092),f1(x2093,a2)),x2094),x2091),f1(x2093,x2091)))),
% 81.43/81.56 inference(scs_inference,[],[194,4])).
% 81.43/81.56 cnf(229,plain,
% 81.43/81.56 (P1(f1(x2291,f1(x2292,x2292)))),
% 81.43/81.56 inference(scs_inference,[],[80,185,3])).
% 81.43/81.56 cnf(233,plain,
% 81.43/81.56 (P1(f1(x2331,x2331))),
% 81.43/81.56 inference(scs_inference,[],[80,229,3])).
% 81.43/81.56 cnf(421,plain,
% 81.43/81.56 (~P1(f1(f1(f1(f1(f1(f1(x4211,x4212),f1(x4213,a2)),x4214),x4211),f1(x4213,x4211)),f1(f1(x4215,x4215),a3)))),
% 81.43/81.56 inference(scs_inference,[],[182,209,3])).
% 81.43/81.56 cnf(423,plain,
% 81.43/81.56 (~P1(f1(f1(f1(f1(x4231,x4232),f1(x4232,x4233)),f1(x4234,f1(x4232,x4233))),f1(f1(f1(a3,a2),a2),a2)))),
% 81.43/81.56 inference(scs_inference,[],[185,200,3])).
% 81.43/81.56 cnf(439,plain,
% 81.43/81.57 (~P1(f1(f1(f1(f1(x4391,x4392),x4393),f1(f1(x4391,a2),x4393)),f1(f1(f1(a3,a2),x4394),a3)))),
% 81.43/81.57 inference(scs_inference,[],[206,197,3])).
% 81.43/81.57 cnf(587,plain,
% 81.43/81.57 (~P1(f1(f1(x5871,f1(f1(f1(f1(x5872,x5873),f1(x5874,x5873)),a2),f1(x5873,x5875))),a2))),
% 81.43/81.57 inference(scs_inference,[],[54,115,3])).
% 81.43/81.57 cnf(635,plain,
% 81.43/81.57 (P1(f1(f1(f1(f1(f1(x6351,x6352),f1(x6353,a2)),f1(x6354,x6355)),x6354),f1(x6356,x6354)))),
% 81.43/81.57 inference(scs_inference,[],[106,124,3,4])).
% 81.43/81.57 cnf(639,plain,
% 81.43/81.57 (~P1(f1(f1(x6391,f1(f1(f1(a2,x6392),f1(x6391,a2)),x6393)),f1(f1(x6394,x6394),a3)))),
% 81.43/81.57 inference(scs_inference,[],[106,421,3])).
% 81.43/81.57 cnf(643,plain,
% 81.43/81.57 (P1(f1(f1(f1(x6431,x6432),f1(f1(f1(f1(x6433,x6434),f1(x6435,a2)),f1(x6431,x6436)),a2)),f1(x6437,x6431)))),
% 81.43/81.57 inference(scs_inference,[],[106,635,3])).
% 81.43/81.57 cnf(648,plain,
% 81.43/81.57 (P1(f1(f1(f1(x6481,f1(x6482,x6483)),x6482),f1(x6484,x6482)))),
% 81.43/81.57 inference(scs_inference,[],[643,639,233,3,4])).
% 81.43/81.57 cnf(655,plain,
% 81.43/81.57 (P1(f1(f1(f1(x6551,x6552),f1(f1(x6553,f1(x6551,x6554)),a2)),f1(x6555,x6551)))),
% 81.43/81.57 inference(scs_inference,[],[106,648,3])).
% 81.43/81.57 cnf(663,plain,
% 81.43/81.57 (P1(f1(f1(f1(x6631,x6632),x6633),f1(x6632,x6633)))),
% 81.43/81.57 inference(scs_inference,[],[655,587,648,3,4])).
% 81.43/81.57 cnf(666,plain,
% 81.43/81.57 (P1(f1(f1(f1(x6661,x6662),f1(f1(x6663,x6664),a2)),f1(x6664,x6661)))),
% 81.43/81.57 inference(scs_inference,[],[106,663,3])).
% 81.43/81.57 cnf(671,plain,
% 81.43/81.57 (~P1(f1(f1(f1(a3,a2),x6711),f1(f1(f1(a3,a2),a2),a2)))),
% 81.43/81.57 inference(scs_inference,[],[112,423,3])).
% 81.43/81.57 cnf(680,plain,
% 81.43/81.57 ($false),
% 81.43/81.57 inference(scs_inference,[],[112,666,671,439,4,3]),
% 81.43/81.57 ['proof']).
% 81.43/81.57 % SZS output end Proof
% 81.43/81.57 % Total time :81.055567s
%------------------------------------------------------------------------------