%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL090-1 : TPTP v9.3.1. Released v1.0.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:18:37 AM UTC 2026
% Result : Unsatisfiable 245.13s 245.25s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL090-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.08/0.35 % Computer : n031.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Fri Sep 4 23:20:09 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.23/0.52 start to proof:theBenchmark
% 245.13/245.25 %-------------------------------------------
% 245.13/245.25 % File :CSE---1.7
% 245.13/245.25 % Problem :theBenchmark
% 245.13/245.25 % Transform :cnf
% 245.13/245.25 % Format :tptp:raw
% 245.13/245.25 % Command :java -jar mcs_scs.jar %d %s
% 245.13/245.25
% 245.13/245.25 % Result :Theorem 244.650267s
% 245.13/245.25 % Output :CNFRefutation 244.650267s
% 245.13/245.25 %-------------------------------------------
% 245.13/245.25 %--------------------------------------------------------------------------
% 245.13/245.25 % File : LCL090-1 : TPTP v9.3.1. Released v1.0.0.
% 245.13/245.25 % Domain : Logic Calculi (Implicational propositional)
% 245.13/245.25 % Problem : IC-1 depends on the 5th Lukasiewicz axiom
% 245.13/245.25 % Version : [TPTP] axioms.
% 245.13/245.25 % English : Axiomatisations of the Implicational propositional calculus
% 245.13/245.25 % are {IC-2,IC-3,IC-4} by Tarski-Bernays and single Lukasiewicz
% 245.13/245.25 % axioms.Show that IC-1 depends on the fifth Lukasiewicz axiom.
% 245.13/245.25
% 245.13/245.25 % Refs : [Luk48] Lukasiewicz (1948), The Shortest Axiom of the Implicat
% 245.13/245.25 % : [Pfe88] Pfenning (1988), Single Axioms in the Implicational Pr
% 245.13/245.25 % Source : [TPTP]
% 245.13/245.25 % Names :
% 245.13/245.25
% 245.13/245.25 % Status : Unsatisfiable
% 245.13/245.25 % 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 v2.7.0, 0.12 v2.6.0, 0.29 v2.5.0, 0.00 v2.4.0, 0.00 v2.3.0, 0.14 v2.2.1, 0.44 v2.1.0, 0.50 v2.0.0
% 245.13/245.25 % Syntax : Number of clauses : 3 ( 2 unt; 0 nHn; 2 RR)
% 245.13/245.25 % Number of literals : 5 ( 0 equ; 3 neg)
% 245.13/245.25 % Maximal clause size : 3 ( 1 avg)
% 245.13/245.25 % Maximal term depth : 5 ( 2 avg)
% 245.13/245.25 % Number of predicates : 1 ( 1 usr; 0 prp; 1-1 aty)
% 245.13/245.25 % Number of functors : 2 ( 2 usr; 1 con; 0-2 aty)
% 245.13/245.25 % Number of variables : 7 ( 2 sgn)
% 245.13/245.25 % SPC : CNF_UNS_RFO_NEQ_HRN
% 245.13/245.25
% 245.13/245.25 % Comments :
% 245.13/245.25 %--------------------------------------------------------------------------
% 245.13/245.25 cnf(condensed_detachment,axiom,
% 245.13/245.25 ( ~ is_a_theorem(implies(X,Y))
% 245.13/245.25 | ~ is_a_theorem(X)
% 245.13/245.25 | is_a_theorem(Y) ) ).
% 245.13/245.25
% 245.13/245.25 cnf(ic_JLukasiewicz_5,axiom,
% 245.13/245.25 is_a_theorem(implies(implies(implies(P,Q),implies(R,S)),implies(implies(S,P),implies(T,implies(R,P))))) ).
% 245.13/245.25
% 245.13/245.25 cnf(prove_ic_1,negated_conjecture,
% 245.13/245.25 ~ is_a_theorem(implies(a,a)) ).
% 245.13/245.25
% 245.13/245.25 %--------------------------------------------------------------------------
% 245.13/245.25 %-------------------------------------------
% 245.13/245.25 % Proof found
% 245.13/245.25 % SZS status Theorem for theBenchmark
% 245.13/245.25 % SZS output start Proof
% 245.13/245.25 %ClaNum:3(EqnAxiom:0)
% 245.13/245.25 %VarNum:13(SingletonVarNum:7)
% 245.13/245.25 %MaxLitNum:3
% 245.13/245.25 %MaxfuncDepth:4
% 245.13/245.25 %SharedTerms:3
% 245.13/245.26 %goalClause: 2
% 245.13/245.26 %singleGoalClaCount:1
% 245.13/245.26 [2]~P1(f1(a2,a2))
% 245.13/245.26 [1]P1(f1(f1(f1(x11,x12),f1(x13,x14)),f1(f1(x14,x11),f1(x15,f1(x13,x11)))))
% 245.13/245.26 [3]P1(x31)+~P1(x32)+~P1(f1(x32,x31))
% 245.13/245.26 %EqnAxiom
% 245.13/245.26
% 245.13/245.26 %-------------------------------------------
% 245.13/245.26 cnf(4,plain,
% 245.13/245.26 (P1(f1(f1(x41,x42),f1(x43,f1(x44,x42))))+~P1(f1(f1(x42,x45),f1(x44,x41)))),
% 245.13/245.26 inference(scs_inference,[],[1,3])).
% 245.13/245.26 cnf(6,plain,
% 245.13/245.26 (P1(f1(f1(f1(x61,f1(x62,x63)),f1(x63,x64)),f1(x65,f1(f1(x66,x63),f1(x63,x64)))))),
% 245.13/245.26 inference(scs_inference,[],[1,4])).
% 245.13/245.26 cnf(8,plain,
% 245.13/245.26 (~P1(f1(f1(f1(f1(x81,x82),f1(x83,x84)),f1(f1(x84,x81),f1(x85,f1(x83,x81)))),f1(a2,a2)))),
% 245.13/245.26 inference(scs_inference,[],[1,2,4,3])).
% 245.13/245.26 cnf(10,plain,
% 245.13/245.26 (P1(f1(f1(f1(f1(x101,x102),f1(x102,x103)),f1(x104,f1(x105,x102))),f1(x106,f1(x107,f1(x104,f1(x105,x102))))))),
% 245.13/245.26 inference(scs_inference,[],[6,4])).
% 245.13/245.26 cnf(12,plain,
% 245.13/245.26 (P1(f1(f1(f1(x121,f1(x122,f1(x123,x124))),f1(f1(x125,x124),f1(x124,x126))),f1(x127,f1(x128,f1(f1(x125,x124),f1(x124,x126))))))),
% 245.13/245.26 inference(scs_inference,[],[10,4])).
% 245.13/245.26 cnf(20,plain,
% 245.13/245.26 (~P1(f1(f1(f1(f1(x201,x202),f1(x203,x204)),f1(f1(x204,x201),f1(x205,f1(x203,x201)))),f1(f1(f1(f1(x206,x207),f1(x208,x209)),f1(f1(x209,x206),f1(x2010,f1(x208,x206)))),f1(a2,a2))))),
% 245.13/245.26 inference(scs_inference,[],[1,12,8,4,3])).
% 245.13/245.26 cnf(28,plain,
% 245.13/245.26 (~P1(f1(f1(f1(f1(x281,x282),f1(x283,x284)),f1(f1(x284,x281),f1(x285,f1(x283,x281)))),f1(f1(f1(f1(x286,x287),f1(x288,x289)),f1(f1(x289,x286),f1(x2810,f1(x288,x286)))),f1(f1(f1(f1(x2811,x2812),f1(x2813,x2814)),f1(f1(x2814,x2811),f1(x2815,f1(x2813,x2811)))),f1(a2,a2)))))),
% 245.13/245.26 inference(scs_inference,[],[1,20,3])).
% 245.13/245.26 cnf(248,plain,
% 245.13/245.26 (~P1(f1(f1(f1(f1(x2481,x2482),f1(x2483,x2484)),f1(f1(x2484,x2481),f1(x2485,f1(x2483,x2481)))),f1(f1(f1(f1(x2486,x2487),f1(x2488,x2489)),f1(f1(x2489,x2486),f1(x24810,f1(x2488,x2486)))),f1(f1(f1(f1(x24811,x24812),f1(x24813,x24814)),f1(f1(x24814,x24811),f1(x24815,f1(x24813,x24811)))),f1(f1(f1(f1(x24816,x24817),f1(x24818,x24819)),f1(f1(x24819,x24816),f1(x24820,f1(x24818,x24816)))),f1(a2,a2))))))),
% 245.13/245.26 inference(scs_inference,[],[1,28,3])).
% 245.13/245.26 cnf(332,plain,
% 245.13/245.26 (P1(f1(x3321,f1(f1(x3322,x3323),f1(x3323,x3324))))+~P1(f1(f1(x3325,f1(x3326,x3323)),f1(x3323,x3324)))),
% 245.13/245.26 inference(scs_inference,[],[6,3])).
% 245.13/245.26 cnf(334,plain,
% 245.13/245.26 (P1(f1(f1(f1(x3341,f1(f1(x3342,x3343),f1(x3343,x3341))),x3344),f1(x3345,f1(f1(x3346,x3341),x3344))))),
% 245.13/245.26 inference(scs_inference,[],[6,332,4])).
% 245.13/245.26 cnf(335,plain,
% 245.13/245.26 (P1(f1(x3351,f1(f1(x3352,x3353),f1(x3353,f1(f1(x3354,x3355),f1(x3355,x3353))))))),
% 245.13/245.26 inference(scs_inference,[],[1,332,4])).
% 245.13/245.26 cnf(336,plain,
% 245.13/245.26 (P1(f1(x3361,f1(f1(x3362,x3363),f1(x3363,f1(f1(x3364,x3365),f1(x3366,x3363))))))),
% 245.13/245.26 inference(scs_inference,[],[334,332])).
% 245.13/245.26 cnf(339,plain,
% 245.13/245.26 (P1(f1(f1(x3391,x3392),f1(x3392,f1(f1(x3393,x3394),f1(x3394,x3392)))))),
% 245.13/245.26 inference(scs_inference,[],[1,334,335,332,3])).
% 245.13/245.26 cnf(342,plain,
% 245.13/245.26 (P1(f1(f1(f1(f1(x3421,x3422),f1(x3422,f1(f1(x3423,x3424),f1(x3425,x3422)))),x3426),f1(x3427,f1(f1(x3428,f1(x3421,x3422)),x3426))))),
% 245.13/245.26 inference(scs_inference,[],[336,4,332])).
% 245.13/245.26 cnf(343,plain,
% 245.13/245.26 (P1(f1(f1(f1(f1(x3431,x3432),f1(x3432,x3433)),x3434),f1(x3435,f1(x3433,x3434))))),
% 245.13/245.26 inference(scs_inference,[],[1,339,3])).
% 245.13/245.26 cnf(346,plain,
% 245.13/245.26 (P1(f1(f1(f1(x3461,f1(x3462,f1(x3463,x3461))),x3464),f1(x3465,f1(f1(x3466,x3461),x3464))))),
% 245.13/245.26 inference(scs_inference,[],[343,4,332])).
% 245.13/245.26 cnf(347,plain,
% 245.13/245.26 (P1(f1(f1(f1(f1(x3471,x3472),x3473),f1(x3472,f1(x3474,f1(x3475,x3472)))),f1(x3476,f1(x3477,f1(x3472,f1(x3474,f1(x3475,x3472)))))))),
% 245.13/245.26 inference(scs_inference,[],[1,346,3])).
% 245.13/245.26 cnf(350,plain,
% 245.13/245.26 (P1(f1(x3501,f1(x3502,f1(f1(x3502,x3503),f1(x3504,f1(x3505,x3503))))))),
% 245.13/245.26 inference(scs_inference,[],[1,343,3])).
% 245.13/245.26 cnf(351,plain,
% 245.13/245.26 (P1(f1(f1(f1(f1(x3511,x3512),f1(x3512,x3513)),x3514),f1(x3515,f1(x3513,x3514))))),
% 245.13/245.26 inference(rename_variables,[],[343])).
% 245.13/245.26 cnf(354,plain,
% 245.13/245.26 (P1(f1(x3541,f1(f1(x3542,x3543),f1(x3543,f1(x3544,f1(x3545,x3543))))))),
% 245.13/245.26 inference(scs_inference,[],[1,343,351,3,332])).
% 245.13/245.26 cnf(357,plain,
% 245.13/245.26 (P1(f1(x3571,f1(f1(x3571,x3572),f1(x3573,f1(x3574,x3572)))))),
% 245.13/245.26 inference(scs_inference,[],[1,350,3])).
% 245.13/245.26 cnf(360,plain,
% 245.13/245.26 (P1(f1(f1(f1(x3601,f1(x3602,x3603)),x3604),f1(x3605,f1(f1(f1(x3604,x3606),x3603),x3604))))),
% 245.13/245.26 inference(scs_inference,[],[1,357,3])).
% 245.13/245.26 cnf(364,plain,
% 245.13/245.26 (P1(f1(f1(x3641,x3642),f1(x3642,f1(x3643,f1(x3644,x3642)))))),
% 245.13/245.26 inference(scs_inference,[],[1,354,3])).
% 245.13/245.26 cnf(367,plain,
% 245.13/245.26 (P1(f1(f1(f1(x3671,f1(x3672,x3673)),x3674),f1(x3675,f1(x3673,x3674))))),
% 245.13/245.26 inference(scs_inference,[],[1,364,3])).
% 245.13/245.26 cnf(370,plain,
% 245.13/245.26 (P1(f1(f1(f1(x3701,x3702),f1(x3703,f1(x3704,x3701))),f1(x3705,f1(x3706,f1(x3703,f1(x3704,x3701))))))),
% 245.13/245.26 inference(scs_inference,[],[1,367,3])).
% 245.13/245.26 cnf(373,plain,
% 245.13/245.26 (P1(f1(f1(f1(x3731,f1(x3732,f1(x3733,x3734))),f1(x3734,x3735)),f1(x3736,f1(x3737,f1(x3734,x3735)))))),
% 245.13/245.26 inference(scs_inference,[],[1,370,3])).
% 245.13/245.26 cnf(376,plain,
% 245.13/245.26 (P1(f1(f1(f1(x3761,f1(x3762,x3763)),f1(x3764,f1(x3765,f1(x3766,x3762)))),f1(x3767,f1(x3768,f1(x3764,f1(x3765,f1(x3766,x3762)))))))),
% 245.13/245.26 inference(scs_inference,[],[1,373,3])).
% 245.13/245.26 cnf(411,plain,
% 245.13/245.26 (P1(f1(x4111,f1(x4112,f1(x4113,f1(f1(x4114,x4115),f1(x4115,f1(x4116,x4115)))))))),
% 245.13/245.26 inference(scs_inference,[],[6,370,3])).
% 245.13/245.26 cnf(415,plain,
% 245.13/245.26 (P1(f1(x4151,f1(x4152,f1(f1(x4153,x4154),f1(x4154,f1(x4155,x4154))))))),
% 245.13/245.26 inference(scs_inference,[],[6,411,3])).
% 245.13/245.26 cnf(418,plain,
% 245.13/245.26 (P1(f1(x4181,f1(f1(x4182,x4183),f1(x4183,f1(x4184,x4183)))))),
% 245.13/245.26 inference(scs_inference,[],[6,415,3])).
% 245.13/245.26 cnf(421,plain,
% 245.13/245.26 (P1(f1(f1(x4211,x4212),f1(x4212,f1(x4213,x4212))))),
% 245.13/245.26 inference(scs_inference,[],[6,418,3])).
% 245.13/245.26 cnf(446,plain,
% 245.13/245.26 (P1(f1(x4461,f1(x4462,f1(f1(x4463,x4463),f1(x4464,f1(x4465,f1(x4463,x4463)))))))),
% 245.13/245.26 inference(scs_inference,[],[10,347,3])).
% 245.13/245.26 cnf(450,plain,
% 245.13/245.26 (P1(f1(x4501,f1(f1(x4502,x4502),f1(x4503,f1(x4504,f1(x4502,x4502))))))),
% 245.13/245.26 inference(scs_inference,[],[10,446,3])).
% 245.13/245.26 cnf(453,plain,
% 245.13/245.26 (P1(f1(f1(x4531,x4531),f1(x4532,f1(x4533,f1(x4531,x4531)))))),
% 245.13/245.26 inference(scs_inference,[],[10,450,3])).
% 245.13/245.26 cnf(456,plain,
% 245.13/245.26 (P1(f1(f1(x4561,f1(x4562,f1(x4563,f1(x4564,x4565)))),f1(x4566,f1(x4561,f1(x4562,f1(x4563,f1(x4564,x4565)))))))),
% 245.13/245.26 inference(scs_inference,[],[10,421,3])).
% 245.13/245.26 cnf(459,plain,
% 245.13/245.26 (P1(f1(x4591,f1(f1(f1(f1(x4592,x4593),f1(x4593,x4594)),f1(x4595,f1(x4596,x4593))),f1(x4597,f1(x4598,f1(x4595,f1(x4596,x4593)))))))),
% 245.13/245.26 inference(scs_inference,[],[10,456,3])).
% 245.13/245.26 cnf(462,plain,
% 245.13/245.26 (P1(f1(x4621,f1(x4622,f1(x4623,f1(x4624,f1(f1(x4625,x4626),f1(x4625,x4626)))))))),
% 245.13/245.26 inference(scs_inference,[],[10,376,3])).
% 245.13/245.26 cnf(466,plain,
% 245.13/245.26 (P1(f1(x4661,f1(x4662,f1(x4663,f1(f1(x4664,x4665),f1(x4664,x4665))))))),
% 245.13/245.26 inference(scs_inference,[],[10,462,3])).
% 245.13/245.26 cnf(469,plain,
% 245.13/245.26 (P1(f1(x4691,f1(x4692,f1(f1(x4693,x4694),f1(x4693,x4694)))))),
% 245.13/245.26 inference(scs_inference,[],[10,466,3])).
% 245.13/245.26 cnf(472,plain,
% 245.13/245.26 (P1(f1(x4721,f1(f1(x4722,x4723),f1(x4722,x4723))))),
% 245.13/245.26 inference(scs_inference,[],[10,469,3])).
% 245.13/245.26 cnf(475,plain,
% 245.13/245.26 (P1(f1(f1(x4751,x4752),f1(x4751,x4752)))),
% 245.13/245.26 inference(scs_inference,[],[10,472,3])).
% 245.13/245.26 cnf(478,plain,
% 245.13/245.26 (P1(f1(x4781,f1(x4782,f1(f1(x4783,x4784),f1(x4784,x4784)))))),
% 245.13/245.26 inference(scs_inference,[],[10,475,3])).
% 245.13/245.26 cnf(484,plain,
% 245.13/245.26 (P1(f1(x4841,f1(x4842,f1(x4843,f1(f1(x4844,x4845),f1(x4845,x4845))))))),
% 245.13/245.26 inference(scs_inference,[],[10,478,3])).
% 245.13/245.26 cnf(488,plain,
% 245.13/245.27 (P1(f1(x4881,f1(f1(x4882,x4883),f1(x4883,x4883))))),
% 245.13/245.27 inference(scs_inference,[],[10,478,3])).
% 245.13/245.27 cnf(491,plain,
% 245.13/245.27 (P1(f1(f1(x4911,x4912),f1(x4912,x4912)))),
% 245.13/245.27 inference(scs_inference,[],[12,488,3])).
% 245.13/245.27 cnf(498,plain,
% 245.13/245.27 (P1(f1(f1(f1(x4981,f1(x4982,f1(f1(x4983,x4981),f1(x4983,x4981)))),x4984),f1(x4985,f1(f1(x4986,x4981),x4984))))),
% 245.13/245.27 inference(scs_inference,[],[453,4,332])).
% 245.13/245.27 cnf(499,plain,
% 245.13/245.27 (P1(f1(f1(f1(f1(x4991,x4992),f1(x4992,x4992)),x4993),f1(x4994,f1(x4995,x4993))))),
% 245.13/245.27 inference(scs_inference,[],[491,357,3])).
% 245.13/245.27 cnf(502,plain,
% 245.13/245.27 (P1(f1(x5021,f1(f1(f1(f1(x5022,f1(x5023,f1(x5024,x5025))),x5026),x5025),f1(x5022,f1(x5023,f1(x5024,x5025))))))),
% 245.13/245.27 inference(scs_inference,[],[499,360,3])).
% 245.13/245.27 cnf(506,plain,
% 245.13/245.27 (P1(f1(f1(f1(f1(x5061,f1(x5062,f1(x5063,x5064))),x5065),x5064),f1(x5061,f1(x5062,f1(x5063,x5064)))))),
% 245.13/245.27 inference(scs_inference,[],[498,502,3])).
% 245.13/245.27 cnf(509,plain,
% 245.13/245.27 (P1(f1(x5091,f1(f1(x5092,x5093),f1(x5093,f1(x5094,f1(x5095,f1(x5096,x5093)))))))),
% 245.13/245.27 inference(scs_inference,[],[498,502,3,332])).
% 245.13/245.27 cnf(511,plain,
% 245.13/245.27 (P1(f1(f1(x5111,x5112),f1(x5112,f1(x5113,f1(x5114,f1(x5115,x5112))))))),
% 245.13/245.27 inference(scs_inference,[],[506,509,3])).
% 245.13/245.27 cnf(515,plain,
% 245.13/245.27 (P1(f1(f1(x5151,f1(f1(x5152,f1(x5153,x5154)),x5155)),f1(x5156,f1(x5151,f1(f1(x5152,f1(x5153,x5154)),x5155)))))),
% 245.13/245.27 inference(scs_inference,[],[342,421,3])).
% 245.13/245.27 cnf(518,plain,
% 245.13/245.27 (P1(f1(f1(f1(x5181,f1(x5182,f1(f1(x5183,x5184),f1(x5184,x5184)))),x5185),f1(x5186,f1(f1(x5187,x5181),x5185))))),
% 245.13/245.27 inference(scs_inference,[],[484,4,332])).
% 245.13/245.27 cnf(519,plain,
% 245.13/245.27 (P1(f1(f1(x5191,f1(f1(x5192,x5193),x5194)),f1(x5195,f1(x5196,f1(x5191,f1(f1(x5192,x5193),x5194))))))),
% 245.13/245.27 inference(scs_inference,[],[518,364,3])).
% 245.13/245.27 cnf(522,plain,
% 245.13/245.27 (P1(f1(x5221,f1(x5222,f1(x5223,f1(x5224,f1(x5225,f1(x5226,f1(x5227,x5224))))))))),
% 245.13/245.27 inference(scs_inference,[],[511,506,3])).
% 245.13/245.27 cnf(526,plain,
% 245.13/245.27 (P1(f1(x5261,f1(x5262,f1(x5263,f1(x5264,f1(x5265,f1(x5266,x5263)))))))),
% 245.13/245.27 inference(scs_inference,[],[515,522,3])).
% 245.13/245.27 cnf(529,plain,
% 245.13/245.27 (P1(f1(x5291,f1(x5292,f1(x5293,f1(x5294,f1(x5295,x5292))))))),
% 245.13/245.27 inference(scs_inference,[],[519,526,3])).
% 245.13/245.27 cnf(538,plain,
% 245.13/245.27 (P1(f1(x5381,f1(x5382,f1(x5383,f1(x5384,x5381)))))),
% 245.13/245.27 inference(scs_inference,[],[459,529,3])).
% 245.13/245.27 cnf(541,plain,
% 245.13/245.27 (P1(f1(f1(f1(x5411,f1(x5412,f1(x5413,f1(x5414,f1(x5415,x5411))))),x5416),f1(x5417,f1(f1(x5418,x5411),x5416))))),
% 245.13/245.27 inference(scs_inference,[],[538,4,332])).
% 245.13/245.27 cnf(542,plain,
% 245.13/245.27 (P1(f1(x5421,f1(x5422,f1(x5423,f1(x5424,f1(f1(x5425,x5421),x5421))))))),
% 245.13/245.27 inference(scs_inference,[],[541,506,3])).
% 245.13/245.27 cnf(546,plain,
% 245.13/245.27 (P1(f1(f1(f1(x5461,f1(x5462,f1(x5463,f1(f1(x5464,f1(x5465,f1(x5466,x5461))),f1(x5465,f1(x5466,x5461)))))),x5467),f1(x5468,f1(f1(x5469,x5461),x5467))))),
% 245.13/245.27 inference(scs_inference,[],[542,4,332])).
% 245.13/245.27 cnf(547,plain,
% 245.13/245.27 ($false),
% 245.13/245.27 inference(scs_inference,[],[248,546,376,3]),
% 245.13/245.27 ['proof']).
% 245.13/245.27 % SZS output end Proof
% 245.13/245.27 % Total time :244.650267s
%------------------------------------------------------------------------------