%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL365-1 : TPTP v9.3.1. Released v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n011.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:01 AM UTC 2026
% Result : Unsatisfiable 75.80s 75.97s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL365-1 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.08/0.34 % Computer : n011.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 16:37:13 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.24/0.51 start to proof:theBenchmark
% 75.80/75.96 %-------------------------------------------
% 75.80/75.96 % File :CSE---1.7
% 75.80/75.96 % Problem :theBenchmark
% 75.80/75.96 % Transform :cnf
% 75.80/75.96 % Format :tptp:raw
% 75.80/75.96 % Command :java -jar mcs_scs.jar %d %s
% 75.80/75.96
% 75.80/75.96 % Result :Theorem 75.466588s
% 75.80/75.96 % Output :CNFRefutation 75.466588s
% 75.80/75.96 %-------------------------------------------
% 75.80/75.96 %--------------------------------------------------------------------------
% 75.80/75.96 % File : LCL365-1 : TPTP v9.3.1. Released v2.3.0.
% 75.80/75.96 % Domain : Logic Calculi (Implication/Negation 2 valued sentential)
% 75.80/75.96 % Problem : CN-14 depends on the Lukasiewicz system
% 75.80/75.96 % Version : [McC92] axioms.
% 75.80/75.96 % English : An axiomatisation of the Implication/Negation 2 valued
% 75.80/75.96 % sentential calculus is {CN-1,CN-2,CN-3} by Lukasiewicz.
% 75.80/75.96 % Show that CN-14 depends on the Lukasiewicz system.
% 75.80/75.96
% 75.80/75.96 % Refs : [Wos96] Wos (1996), Combining Resonance with Heat
% 75.80/75.96 % : [McC92] McCune (1992), Email to G. Sutcliffe
% 75.80/75.96 % Source : [Wos96]
% 75.80/75.96 % Names : thesis_14 [Wos96]
% 75.80/75.96
% 75.80/75.96 % Status : Unsatisfiable
% 75.80/75.96 % Rating : 0.00 v9.3.0, 0.24 v9.1.0, 0.27 v8.2.0, 0.29 v8.1.0, 0.25 v7.4.0, 0.33 v7.3.0, 0.25 v6.2.0, 0.17 v6.1.0, 0.29 v6.0.0, 0.33 v5.5.0, 0.38 v5.4.0, 0.44 v5.3.0, 0.60 v5.2.0, 0.38 v5.1.0, 0.50 v5.0.0, 0.53 v4.0.1, 0.29 v3.7.0, 0.14 v3.4.0, 0.20 v3.3.0, 0.00 v2.7.0, 0.12 v2.6.0, 0.43 v2.4.0, 0.25 v2.3.0
% 75.80/75.96 % Syntax : Number of clauses : 5 ( 4 unt; 0 nHn; 2 RR)
% 75.80/75.96 % Number of literals : 7 ( 0 equ; 3 neg)
% 75.80/75.96 % Maximal clause size : 3 ( 1 avg)
% 75.80/75.96 % Maximal term depth : 6 ( 2 avg)
% 75.80/75.96 % Number of predicates : 1 ( 1 usr; 0 prp; 1-1 aty)
% 75.80/75.97 % Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% 75.80/75.97 % Number of variables : 8 ( 1 sgn)
% 75.80/75.97 % SPC : CNF_UNS_RFO_NEQ_HRN
% 75.80/75.97
% 75.80/75.97 % Comments :
% 75.80/75.97 %--------------------------------------------------------------------------
% 75.80/75.97 cnf(condensed_detachment,axiom,
% 75.80/75.97 ( ~ is_a_theorem(implies(X,Y))
% 75.80/75.97 | ~ is_a_theorem(X)
% 75.80/75.97 | is_a_theorem(Y) ) ).
% 75.80/75.97
% 75.80/75.97 cnf(cn_1,axiom,
% 75.80/75.97 is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) ).
% 75.80/75.97
% 75.80/75.97 cnf(cn_2,axiom,
% 75.80/75.97 is_a_theorem(implies(implies(not(X),X),X)) ).
% 75.80/75.97
% 75.80/75.97 cnf(cn_3,axiom,
% 75.80/75.97 is_a_theorem(implies(X,implies(not(X),Y))) ).
% 75.80/75.97
% 75.80/75.97 cnf(prove_cn_14,negated_conjecture,
% 75.80/75.97 ~ is_a_theorem(implies(implies(implies(x,implies(implies(y,z),z)),u),implies(implies(not(z),y),u))) ).
% 75.80/75.97
% 75.80/75.97 %--------------------------------------------------------------------------
% 75.80/75.97 %-------------------------------------------
% 75.80/75.97 % Proof found
% 75.80/75.97 % SZS status Theorem for theBenchmark
% 75.80/75.97 % SZS output start Proof
% 75.80/75.97 %ClaNum:5(EqnAxiom:0)
% 75.80/75.97 %VarNum:16(SingletonVarNum:8)
% 75.80/75.97 %MaxLitNum:3
% 75.80/75.97 %MaxfuncDepth:4
% 75.80/75.97 %SharedTerms:13
% 75.80/75.97 %goalClause: 4
% 75.80/75.97 %singleGoalClaCount:1
% 75.80/75.97 [4]~P1(f2(f2(f2(a3,f2(f2(a5,a6),a6)),a4),f2(f2(f1(a6),a5),a4)))
% 75.80/75.97 [2]P1(f2(f2(f1(x21),x21),x21))
% 75.80/75.97 [1]P1(f2(x11,f2(f1(x11),x12)))
% 75.80/75.97 [3]P1(f2(f2(x31,x32),f2(f2(x32,x33),f2(x31,x33))))
% 75.80/75.97 [5]P1(x51)+~P1(x52)+~P1(f2(x52,x51))
% 75.80/75.97 %EqnAxiom
% 75.80/75.97
% 75.80/75.97 %-------------------------------------------
% 75.80/75.97 cnf(6,plain,
% 75.80/75.97 (~P1(f2(f2(f1(a6),a5),f2(a3,f2(f2(a5,a6),a6))))),
% 75.80/75.97 inference(scs_inference,[],[4,3,5])).
% 75.80/75.97 cnf(9,plain,
% 75.80/75.97 (P1(f2(f1(f2(f2(f1(x91),x91),x91)),x92))),
% 75.80/75.97 inference(scs_inference,[],[2,1,5])).
% 75.80/75.97 cnf(15,plain,
% 75.80/75.97 (P1(f2(f1(f2(f2(x151,x152),f2(f2(x152,x153),f2(x151,x153)))),x154))),
% 75.80/75.97 inference(scs_inference,[],[3,1,5])).
% 75.80/75.97 cnf(25,plain,
% 75.80/75.97 (~P1(f2(f2(x251,f2(f1(x251),x252)),f2(f2(f1(a6),a5),f2(a3,f2(f2(a5,a6),a6)))))),
% 75.80/75.97 inference(scs_inference,[],[1,6,5])).
% 75.80/75.97 cnf(33,plain,
% 75.80/75.97 (P1(f2(f2(x331,x332),f2(f2(f1(x331),x331),x332)))),
% 75.80/75.97 inference(scs_inference,[],[2,3,5])).
% 75.80/75.97 cnf(37,plain,
% 75.80/75.97 (P1(f2(f1(f2(f2(x371,x372),f2(f2(f1(x371),x371),x372))),x373))),
% 75.80/75.97 inference(scs_inference,[],[33,1,5])).
% 75.80/75.97 cnf(40,plain,
% 75.80/75.97 (P1(f2(f2(f2(f2(f1(x401),x401),x402),x403),f2(f2(x401,x402),x403)))),
% 75.80/75.97 inference(scs_inference,[],[33,3,5])).
% 75.80/75.97 cnf(65,plain,
% 75.80/75.97 (P1(f2(f2(x651,x652),f2(f2(x652,x653),f2(f2(f1(x651),x651),x653))))),
% 75.80/75.97 inference(scs_inference,[],[40,3,5])).
% 75.80/75.97 cnf(69,plain,
% 75.80/75.97 (P1(f2(f2(f1(f2(x691,x692)),f2(x691,x692)),f2(f2(x692,x693),f2(f2(f1(x691),x691),x693))))),
% 75.80/75.97 inference(scs_inference,[],[65,33,5])).
% 75.80/75.97 cnf(72,plain,
% 75.80/75.97 (P1(f2(f2(f2(f2(f1(x721),x721),x722),x723),f2(f2(f1(f2(x721,x722)),f2(x721,x722)),x723)))),
% 75.80/75.97 inference(scs_inference,[],[65,33,5])).
% 75.80/75.97 cnf(75,plain,
% 75.80/75.97 (P1(f2(f2(f1(f2(f1(x751),x751)),f2(f1(x751),x751)),x751))),
% 75.80/75.97 inference(scs_inference,[],[2,33,5])).
% 75.80/75.97 cnf(78,plain,
% 75.80/75.97 (P1(f2(f2(f2(f2(x781,x782),f2(x783,x782)),x784),f2(f2(f1(f2(x783,x781)),f2(x783,x781)),x784)))),
% 75.80/75.97 inference(scs_inference,[],[69,15,5])).
% 75.80/75.97 cnf(95,plain,
% 75.80/75.97 (P1(f2(f2(f2(f1(x951),x952),x953),f2(f2(f1(x951),x951),x953)))),
% 75.80/75.97 inference(scs_inference,[],[65,1,5])).
% 75.80/75.97 cnf(103,plain,
% 75.80/75.97 (P1(f2(f2(f1(f2(x1031,x1032)),f2(x1031,x1032)),f2(f2(f1(x1031),x1031),x1032)))),
% 75.80/75.97 inference(scs_inference,[],[72,95,5])).
% 75.80/75.97 cnf(115,plain,
% 75.80/75.97 (P1(f2(f2(f1(f2(x1151,x1152)),f2(x1151,x1152)),f2(f2(x1152,x1153),f2(x1151,x1153))))),
% 75.80/75.97 inference(scs_inference,[],[103,15,5])).
% 75.80/75.97 cnf(125,plain,
% 75.80/75.97 (P1(f2(f2(x1251,x1252),f2(f1(f2(f2(f1(x1251),x1251),x1252)),x1253)))),
% 75.80/75.97 inference(scs_inference,[],[40,1,5])).
% 75.80/75.97 cnf(133,plain,
% 75.80/75.97 (P1(f2(f1(f2(f2(f1(x1331),x1331),f2(f1(x1331),x1332))),x1333))),
% 75.80/75.97 inference(scs_inference,[],[125,1,5])).
% 75.80/75.97 cnf(152,plain,
% 75.80/75.97 (P1(f2(f2(f1(x1521),x1521),f2(f1(f2(f1(x1521),x1522)),x1523)))),
% 75.80/75.97 inference(scs_inference,[],[1,95,5])).
% 75.80/75.97 cnf(163,plain,
% 75.80/75.97 (P1(f2(f2(f1(f2(x1631,x1632)),f2(x1631,x1632)),f2(f2(f1(f2(x1632,x1633)),f2(x1632,x1633)),f2(x1631,x1633))))),
% 75.80/75.97 inference(scs_inference,[],[33,78,5])).
% 75.80/75.97 cnf(169,plain,
% 75.80/75.97 (P1(f2(f2(f1(f2(f2(f2(x1691,x1692),f2(x1693,x1692)),x1694)),f2(f2(f2(x1691,x1692),f2(x1693,x1692)),x1694)),f2(f2(x1693,x1691),x1694)))),
% 75.80/75.97 inference(scs_inference,[],[163,15,5])).
% 75.80/75.97 cnf(177,plain,
% 75.80/75.97 (P1(f2(f2(f1(f2(x1771,x1772)),f2(x1771,x1772)),f2(f2(f2(x1771,x1773),x1774),f2(f2(x1772,x1773),x1774))))),
% 75.80/75.97 inference(scs_inference,[],[78,3,5])).
% 75.80/75.97 cnf(181,plain,
% 75.80/75.97 (P1(f2(f2(f2(f2(x1811,x1812),x1813),x1814),f2(f2(f2(f2(x1812,x1815),f2(x1811,x1815)),x1813),x1814)))),
% 75.80/75.97 inference(scs_inference,[],[177,15,5])).
% 75.80/75.97 cnf(185,plain,
% 75.80/75.97 (P1(f2(f2(f1(f2(x1851,f2(x1852,x1853))),f2(x1851,f2(x1852,x1853))),f2(f2(f2(f2(x1853,x1854),f2(x1852,x1854)),x1855),f2(x1851,x1855))))),
% 75.80/75.97 inference(scs_inference,[],[181,78,5])).
% 75.80/75.98 cnf(201,plain,
% 75.80/75.98 (P1(f2(f2(f2(f2(x2011,x2012),f2(f1(x2013),x2012)),x2014),f2(f2(f1(x2013),x2013),x2014)))),
% 75.80/75.98 inference(scs_inference,[],[185,133,5])).
% 75.80/75.98 cnf(234,plain,
% 75.80/75.98 (P1(f2(f2(f1(f2(x2341,x2342)),f2(x2341,x2342)),f2(f1(f2(f2(x2342,x2343),f2(x2341,x2343))),x2344)))),
% 75.80/75.98 inference(scs_inference,[],[1,78,5])).
% 75.80/75.98 cnf(256,plain,
% 75.80/75.98 (P1(f2(f1(f2(f2(f2(f2(x2561,x2562),f2(x2563,x2562)),x2564),f2(f2(x2563,x2561),x2564))),x2565))),
% 75.80/75.98 inference(scs_inference,[],[15,234,5])).
% 75.80/75.98 cnf(285,plain,
% 75.80/75.98 (P1(f2(f1(f2(f2(f1(f2(x2851,x2852)),f2(x2851,x2852)),f2(f2(f1(f2(x2852,x2853)),f2(x2852,x2853)),f2(x2851,x2853)))),x2854))),
% 75.80/75.98 inference(scs_inference,[],[163,1,5])).
% 75.80/75.98 cnf(288,plain,
% 75.80/75.98 (P1(f2(f2(f2(f2(f2(x2881,x2882),x2883),f2(f2(x2884,x2882),x2883)),x2885),f2(f2(x2881,x2884),x2885)))),
% 75.80/75.98 inference(scs_inference,[],[185,15,5])).
% 75.80/75.98 cnf(317,plain,
% 75.80/75.98 (P1(f2(f2(f2(f2(x3171,x3172),f2(x3173,x3172)),x3174),f2(f2(x3173,x3171),x3174)))),
% 75.80/75.98 inference(scs_inference,[],[2,256,5])).
% 75.80/75.98 cnf(327,plain,
% 75.80/75.98 (~P1(f2(f2(f2(f2(f1(x3271),x3272),x3273),f2(x3271,x3273)),f2(f2(f1(a6),a5),f2(a3,f2(f2(a5,a6),a6)))))),
% 75.80/75.98 inference(scs_inference,[],[25,317,5])).
% 75.80/75.98 cnf(355,plain,
% 75.80/75.98 (P1(f2(f2(x3551,f2(x3552,x3553)),f2(f2(x3554,x3552),f2(x3551,f2(x3554,x3553)))))),
% 75.80/75.98 inference(scs_inference,[],[169,256,5])).
% 75.80/75.98 cnf(359,plain,
% 75.80/75.98 (P1(f2(f2(x3591,f2(f2(f2(x3592,x3593),f2(x3594,x3593)),x3595)),f2(f2(f2(f2(x3594,x3592),x3595),x3596),f2(x3591,x3596))))),
% 75.80/75.98 inference(scs_inference,[],[181,355,5])).
% 75.80/75.98 cnf(363,plain,
% 75.80/75.98 (~P1(f2(f2(f1(a6),a5),f2(f2(f2(x3631,x3632),f2(f1(a3),x3632)),f2(f2(a5,a6),a6))))),
% 75.80/75.98 inference(scs_inference,[],[359,327,5])).
% 75.80/75.98 cnf(371,plain,
% 75.80/75.98 (~P1(f2(f2(f2(f2(f1(a6),x3711),x3712),f2(f2(a5,x3711),x3712)),f2(f2(f2(x3713,x3714),f2(f1(a3),x3714)),f2(f2(a5,a6),a6))))),
% 75.80/75.98 inference(scs_inference,[],[363,288,5])).
% 75.80/75.98 cnf(380,plain,
% 75.80/75.98 (P1(f2(f2(f2(f2(f1(f2(x3801,x3802)),f2(x3801,x3802)),f2(x3803,x3802)),x3804),f2(f2(f1(f2(x3803,x3801)),f2(x3803,x3801)),x3804)))),
% 75.80/75.98 inference(scs_inference,[],[115,285,5])).
% 75.80/75.98 cnf(394,plain,
% 75.80/75.98 (P1(f2(f2(x3941,f2(f1(f2(x3942,x3943)),f2(x3942,x3943))),f2(f2(f1(f2(x3944,x3942)),f2(x3944,x3942)),f2(x3941,f2(x3944,x3943)))))),
% 75.80/75.98 inference(scs_inference,[],[317,380,5])).
% 75.80/75.98 cnf(428,plain,
% 75.80/75.98 (P1(f2(f2(f2(f2(x4281,x4282),f2(f2(x4283,x4284),f2(x4281,x4284))),x4285),f2(f2(f1(f2(x4282,x4283)),f2(x4282,x4283)),x4285)))),
% 75.80/75.98 inference(scs_inference,[],[359,177,5])).
% 75.80/75.98 cnf(450,plain,
% 75.80/75.98 (P1(f2(f2(f1(f2(x4501,x4502)),f2(x4501,x4502)),f2(f2(f1(f2(x4503,x4501)),f2(x4503,x4501)),f2(f2(x4502,x4504),f2(x4503,x4504)))))),
% 75.80/75.98 inference(scs_inference,[],[428,33,5])).
% 75.80/75.98 cnf(462,plain,
% 75.80/75.98 (P1(f2(f2(f1(f2(x4621,f2(x4622,x4623))),f2(x4621,f2(x4622,x4623))),f2(f2(f2(f2(f1(x4622),x4622),x4623),x4624),f2(x4621,x4624))))),
% 75.80/75.98 inference(scs_inference,[],[450,37,5])).
% 75.80/75.98 cnf(466,plain,
% 75.80/75.98 (~P1(f2(f1(f2(f2(f2(x4661,x4662),f2(f1(a3),x4662)),f2(a6,a6))),f2(f2(f2(x4661,x4662),f2(f1(a3),x4662)),f2(a6,a6))))),
% 75.80/75.98 inference(scs_inference,[],[462,371,5])).
% 75.80/75.98 cnf(472,plain,
% 75.80/75.98 (P1(f2(f2(x4721,f1(x4722)),f2(x4722,f2(x4721,x4723))))),
% 75.80/75.98 inference(scs_inference,[],[1,355,5])).
% 75.80/75.98 cnf(477,plain,
% 75.80/75.98 (P1(f2(x4771,f2(f2(f1(f1(x4771)),f1(x4771)),x4772)))),
% 75.80/75.98 inference(scs_inference,[],[2,472,5])).
% 75.80/75.98 cnf(486,plain,
% 75.80/75.98 (P1(f2(f2(f2(f2(f1(f1(x4861)),f1(x4861)),x4862),x4863),f2(x4861,x4863)))),
% 75.80/75.98 inference(scs_inference,[],[3,477,5])).
% 75.80/75.98 cnf(524,plain,
% 75.80/75.98 (~P1(f2(f2(f2(x5241,x5242),f2(f1(a3),x5242)),f2(a6,a6)))),
% 75.80/75.98 inference(scs_inference,[],[466,1,5])).
% 75.80/75.98 cnf(527,plain,
% 75.80/75.98 (~P1(f2(f2(f2(f1(f2(f1(x5271),x5271)),f2(f1(x5271),x5271)),x5271),f2(f2(f2(x5272,x5273),f2(f1(a3),x5273)),f2(a6,a6))))),
% 75.80/75.98 inference(scs_inference,[],[524,75,5])).
% 75.80/75.98 cnf(555,plain,
% 75.80/75.98 (P1(f2(f2(x5551,x5552),f2(f2(f1(f2(x5552,x5553)),f2(x5552,x5553)),f2(x5551,x5553))))),
% 75.80/75.98 inference(scs_inference,[],[169,37,5])).
% 75.80/75.98 cnf(565,plain,
% 75.80/75.98 (P1(f2(f2(f1(f2(f2(f1(x5651),x5652),x5653)),f2(f2(f1(x5651),x5652),x5653)),f2(x5651,x5653)))),
% 75.80/75.98 inference(scs_inference,[],[555,1,5])).
% 75.80/75.98 cnf(590,plain,
% 75.80/75.98 (~P1(f2(f2(f2(x5901,x5902),f2(f1(a3),x5902)),f2(f1(f2(f1(f2(a6,a6)),f2(a6,a6))),f2(f1(f2(a6,a6)),f2(a6,a6)))))),
% 75.80/75.98 inference(scs_inference,[],[527,3,5])).
% 75.80/75.98 cnf(676,plain,
% 75.80/75.98 (P1(f2(x6761,f2(f1(f2(f2(f1(x6762),x6762),x6762)),x6763)))),
% 75.80/75.98 inference(scs_inference,[],[472,9,5])).
% 75.80/75.98 cnf(693,plain,
% 75.80/75.98 (P1(f2(f2(f1(x6931),x6931),f2(x6932,f2(f1(x6931),x6933))))),
% 75.80/75.98 inference(scs_inference,[],[486,201,5])).
% 75.80/75.98 cnf(698,plain,
% 75.80/75.98 (~P1(f2(f1(f2(f1(f2(a6,a6)),f2(a6,a6))),f2(f1(f2(a6,a6)),f2(a6,a6))))),
% 75.80/75.98 inference(scs_inference,[],[590,693,5])).
% 75.80/75.98 cnf(713,plain,
% 75.80/75.98 (~P1(f2(f1(f2(a6,a6)),f2(a6,a6)))),
% 75.80/75.98 inference(scs_inference,[],[698,152,5])).
% 75.80/75.98 cnf(739,plain,
% 75.80/75.98 (~P1(f2(f2(f2(x7391,x7392),f2(f2(f1(f2(x7392,x7393)),f2(x7392,x7393)),f2(x7391,x7393))),f2(f1(f2(a6,a6)),f2(a6,a6))))),
% 75.80/75.98 inference(scs_inference,[],[555,713,5])).
% 75.80/75.98 cnf(751,plain,
% 75.80/75.98 (~P1(f2(f2(f2(f1(f2(x7511,x7512)),f2(x7511,x7512)),f2(f2(f1(f2(x7512,x7513)),f2(x7512,x7513)),f2(x7511,x7513))),f2(f1(f2(a6,a6)),f2(a6,a6))))),
% 75.80/75.98 inference(scs_inference,[],[739,40,5])).
% 75.80/75.98 cnf(759,plain,
% 75.80/75.98 (P1(f2(f2(f1(f2(x7591,f2(f1(x7592),x7592))),f2(x7591,f2(f1(x7592),x7592))),f2(x7593,f2(x7591,x7592))))),
% 75.80/75.98 inference(scs_inference,[],[676,394,5])).
% 75.80/75.98 cnf(804,plain,
% 75.80/75.98 (P1(f2(f1(f2(f2(x8041,f1(x8042)),f2(x8042,f2(x8041,x8043)))),x8044))),
% 75.80/75.98 inference(scs_inference,[],[1,472,5])).
% 75.80/75.98 cnf(814,plain,
% 75.80/75.98 (P1(f2(x8141,f2(x8142,f2(f1(x8141),x8143))))),
% 75.80/75.98 inference(scs_inference,[],[565,804,5])).
% 75.80/75.98 cnf(821,plain,
% 75.80/75.98 (P1(f2(x8211,f2(f2(f1(f2(f1(x8212),x8212)),f2(f1(x8212),x8212)),x8212)))),
% 75.80/75.98 inference(scs_inference,[],[9,759,5])).
% 75.80/75.98 cnf(827,plain,
% 75.80/75.98 (~P1(f2(a6,a6))),
% 75.80/75.98 inference(scs_inference,[],[751,814,5])).
% 75.80/75.98 cnf(834,plain,
% 75.80/75.98 (~P1(f2(f2(x8341,f2(f2(f1(f2(f1(x8342),x8342)),f2(f1(x8342),x8342)),x8342)),f2(a6,a6)))),
% 75.80/75.98 inference(scs_inference,[],[827,821,5])).
% 75.80/75.98 cnf(891,plain,
% 75.80/75.98 ($false),
% 75.80/75.98 inference(scs_inference,[],[814,834,555,5]),
% 75.80/75.98 ['proof']).
% 75.80/75.98 % SZS output end Proof
% 75.80/75.98 % Total time :75.466588s
%------------------------------------------------------------------------------