%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL094-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 : n029.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 196.37s 196.43s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL094-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.07/0.34 % Computer : n029.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 : Fri Sep 4 16:22:39 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.25/0.50 start to proof:theBenchmark
% 196.37/196.42 %-------------------------------------------
% 196.37/196.42 % File :CSE---1.7
% 196.37/196.42 % Problem :theBenchmark
% 196.37/196.42 % Transform :cnf
% 196.37/196.42 % Format :tptp:raw
% 196.37/196.42 % Command :java -jar mcs_scs.jar %d %s
% 196.37/196.42
% 196.37/196.42 % Result :Theorem 195.903805s
% 196.37/196.42 % Output :CNFRefutation 195.903805s
% 196.37/196.42 %-------------------------------------------
% 196.37/196.42 %--------------------------------------------------------------------------
% 196.37/196.42 % File : LCL094-1 : TPTP v9.3.1. Released v1.0.0.
% 196.37/196.42 % Domain : Logic Calculi (Implicational propositional)
% 196.37/196.42 % Problem : IC-5 depends on the 4th Lukasiewicz axiom
% 196.37/196.42 % Version : [TPTP] axioms.
% 196.37/196.42 % English : Axiomatisations of the Implicational propositional calculus
% 196.37/196.42 % are {IC-2,IC-3,IC-4} by Tarski-Bernays and single Lukasiewicz
% 196.37/196.42 % axioms.Show that IC-5 depends on the fourth Lukasiewicz
% 196.37/196.43 % axiom.
% 196.37/196.43
% 196.37/196.43 % Refs : [Luk48] Lukasiewicz (1948), The Shortest Axiom of the Implicat
% 196.37/196.43 % : [Pfe88] Pfenning (1988), Single Axioms in the Implicational Pr
% 196.37/196.43 % Source : [TPTP]
% 196.37/196.43 % Names :
% 196.37/196.43
% 196.37/196.43 % Status : Unsatisfiable
% 196.37/196.43 % 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.25 v5.2.0, 0.15 v5.1.0, 0.25 v5.0.0, 0.33 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
% 196.37/196.43 % Syntax : Number of clauses : 3 ( 2 unt; 0 nHn; 2 RR)
% 196.37/196.43 % Number of literals : 5 ( 0 equ; 3 neg)
% 196.37/196.43 % Maximal clause size : 3 ( 1 avg)
% 196.37/196.43 % Maximal term depth : 5 ( 2 avg)
% 196.37/196.43 % Number of predicates : 1 ( 1 usr; 0 prp; 1-1 aty)
% 196.37/196.43 % Number of functors : 3 ( 3 usr; 2 con; 0-2 aty)
% 196.37/196.43 % Number of variables : 7 ( 2 sgn)
% 196.37/196.43 % SPC : CNF_UNS_RFO_NEQ_HRN
% 196.37/196.43
% 196.37/196.43 % Comments :
% 196.37/196.43 %--------------------------------------------------------------------------
% 196.37/196.43 cnf(condensed_detachment,axiom,
% 196.37/196.43 ( ~ is_a_theorem(implies(X,Y))
% 196.37/196.43 | ~ is_a_theorem(X)
% 196.37/196.43 | is_a_theorem(Y) ) ).
% 196.37/196.43
% 196.37/196.43 cnf(ic_JLukasiewicz_4,axiom,
% 196.37/196.43 is_a_theorem(implies(implies(implies(P,Q),implies(R,S)),implies(T,implies(implies(S,P),implies(R,P))))) ).
% 196.37/196.43
% 196.37/196.43 cnf(prove_ic_5,negated_conjecture,
% 196.37/196.43 ~ is_a_theorem(implies(a,implies(implies(a,b),b))) ).
% 196.37/196.43
% 196.37/196.43 %--------------------------------------------------------------------------
% 196.37/196.43 %-------------------------------------------
% 196.37/196.43 % Proof found
% 196.37/196.43 % SZS status Theorem for theBenchmark
% 196.37/196.43 % SZS output start Proof
% 196.37/196.43 %ClaNum:3(EqnAxiom:0)
% 196.37/196.43 %VarNum:13(SingletonVarNum:7)
% 196.37/196.43 %MaxLitNum:3
% 196.37/196.43 %MaxfuncDepth:4
% 196.37/196.43 %SharedTerms:6
% 196.37/196.43 %goalClause: 2
% 196.37/196.43 %singleGoalClaCount:1
% 196.37/196.43 [2]~P1(f1(a2,f1(f1(a2,a3),a3)))
% 196.37/196.43 [1]P1(f1(f1(f1(x11,x12),f1(x13,x14)),f1(x15,f1(f1(x14,x11),f1(x13,x11)))))
% 196.37/196.43 [3]P1(x31)+~P1(x32)+~P1(f1(x32,x31))
% 196.37/196.43 %EqnAxiom
% 196.37/196.43
% 196.37/196.43 %-------------------------------------------
% 196.37/196.44 cnf(4,plain,
% 196.37/196.44 (P1(f1(x41,f1(f1(x42,x43),f1(x44,x43))))+~P1(f1(f1(x43,x45),f1(x44,x42)))),
% 196.37/196.44 inference(scs_inference,[],[1,3])).
% 196.37/196.44 cnf(6,plain,
% 196.37/196.44 (P1(f1(x61,f1(f1(f1(f1(x62,x63),f1(x64,x63)),f1(x63,x65)),f1(x66,f1(x63,x65)))))),
% 196.37/196.44 inference(scs_inference,[],[1,4])).
% 196.37/196.44 cnf(8,plain,
% 196.37/196.44 (~P1(f1(f1(f1(f1(x81,x82),f1(x83,x84)),f1(x85,f1(f1(x84,x81),f1(x83,x81)))),f1(a2,f1(f1(a2,a3),a3))))),
% 196.37/196.44 inference(scs_inference,[],[2,1,4,3])).
% 196.37/196.44 cnf(10,plain,
% 196.37/196.44 (P1(f1(f1(f1(f1(x101,x102),f1(x103,x102)),f1(x102,x104)),f1(x105,f1(x102,x104))))),
% 196.37/196.44 inference(scs_inference,[],[1,6,3])).
% 196.37/196.44 cnf(16,plain,
% 196.37/196.44 (P1(f1(x161,f1(x162,f1(f1(x162,x163),f1(x164,x163)))))),
% 196.37/196.44 inference(scs_inference,[],[10,1,3])).
% 196.37/196.44 cnf(20,plain,
% 196.37/196.44 (P1(f1(x201,f1(f1(x201,x202),f1(x203,x202))))),
% 196.37/196.44 inference(scs_inference,[],[16,6,3])).
% 196.37/196.44 cnf(25,plain,
% 196.37/196.44 (P1(f1(f1(f1(f1(f1(f1(x251,x252),f1(x253,x252)),f1(x252,x254)),f1(x255,f1(x252,x254))),x256),f1(x257,x256)))),
% 196.37/196.44 inference(scs_inference,[],[20,10,3])).
% 196.37/196.44 cnf(34,plain,
% 196.37/196.44 (P1(f1(x341,f1(f1(f1(f1(x342,x343),f1(x344,x343)),x345),f1(x342,x345))))),
% 196.37/196.44 inference(scs_inference,[],[16,1,3])).
% 196.37/196.44 cnf(38,plain,
% 196.37/196.44 (P1(f1(f1(f1(f1(x381,x382),f1(x383,x382)),x384),f1(x381,x384)))),
% 196.37/196.44 inference(scs_inference,[],[34,25,3])).
% 196.37/196.44 cnf(71,plain,
% 196.37/196.44 (P1(f1(f1(f1(f1(f1(f1(x711,x712),f1(x713,x712)),x714),f1(x711,x714)),x715),f1(x716,x715)))),
% 196.37/196.44 inference(scs_inference,[],[20,38,3])).
% 196.37/196.44 cnf(77,plain,
% 196.37/196.44 (P1(f1(x771,f1(x772,f1(f1(x773,x774),f1(x774,f1(x773,x774))))))),
% 196.37/196.44 inference(scs_inference,[],[25,10,3])).
% 196.37/196.44 cnf(81,plain,
% 196.37/196.44 (P1(f1(x811,f1(f1(x812,x813),f1(x813,f1(x812,x813)))))),
% 196.37/196.44 inference(scs_inference,[],[25,77,3])).
% 196.37/196.44 cnf(84,plain,
% 196.37/196.44 (P1(f1(f1(x841,x842),f1(x842,f1(x841,x842))))),
% 196.37/196.44 inference(scs_inference,[],[34,81,3])).
% 196.37/196.44 cnf(90,plain,
% 196.37/196.44 (P1(f1(x901,f1(f1(x902,x903),f1(f1(x901,x903),f1(x902,x903)))))),
% 196.37/196.44 inference(scs_inference,[],[38,84,3])).
% 196.37/196.44 cnf(104,plain,
% 196.37/196.44 (P1(f1(f1(x1041,x1042),f1(f1(f1(f1(f1(f1(x1043,x1044),f1(x1045,x1044)),x1046),f1(x1043,x1046)),x1042),f1(x1041,x1042))))),
% 196.37/196.44 inference(scs_inference,[],[71,84,3])).
% 196.37/196.44 cnf(113,plain,
% 196.37/196.44 (P1(f1(x1131,f1(f1(f1(f1(f1(x1132,x1133),x1134),f1(x1135,x1134)),x1132),f1(f1(x1135,x1134),x1132))))),
% 196.37/196.44 inference(scs_inference,[],[1,90,3])).
% 196.37/196.44 cnf(117,plain,
% 196.37/196.44 (P1(f1(f1(f1(f1(f1(x1171,x1172),x1173),f1(x1174,x1173)),x1171),f1(f1(x1174,x1173),x1171)))),
% 196.37/196.44 inference(scs_inference,[],[1,113,3])).
% 196.37/196.44 cnf(120,plain,
% 196.37/196.44 (P1(f1(f1(x1201,f1(x1202,x1203)),f1(f1(x1202,f1(x1202,x1203)),f1(x1201,f1(x1202,x1203)))))),
% 196.37/196.44 inference(scs_inference,[],[117,71,3])).
% 196.37/196.44 cnf(127,plain,
% 196.37/196.44 (P1(f1(x1271,f1(f1(x1272,f1(x1272,x1273)),f1(f1(x1271,x1273),f1(x1272,x1273)))))),
% 196.37/196.44 inference(scs_inference,[],[120,38,3])).
% 196.37/196.44 cnf(131,plain,
% 196.37/196.44 (P1(f1(f1(x1311,f1(x1311,x1312)),f1(f1(f1(x1313,f1(f1(x1313,x1314),f1(x1315,x1314))),x1312),f1(x1311,x1312))))),
% 196.37/196.44 inference(scs_inference,[],[20,127,3])).
% 196.37/196.44 cnf(134,plain,
% 196.37/196.44 (P1(f1(f1(f1(f1(x1341,x1342),f1(x1343,x1342)),x1344),f1(x1345,f1(x1346,f1(x1341,x1344)))))),
% 196.37/196.44 inference(scs_inference,[],[38,71,3])).
% 196.37/196.44 cnf(138,plain,
% 196.37/196.44 (P1(f1(f1(x1381,f1(x1381,x1382)),f1(f1(f1(f1(f1(f1(x1383,x1384),f1(x1385,x1384)),x1386),f1(x1383,x1386)),x1382),f1(x1381,x1382))))),
% 196.37/196.44 inference(scs_inference,[],[38,127,3])).
% 196.37/196.44 cnf(147,plain,
% 196.37/196.44 (P1(f1(x1471,f1(f1(f1(x1472,f1(x1473,x1472)),x1474),f1(f1(x1473,x1472),x1474))))),
% 196.37/196.44 inference(scs_inference,[],[81,1,3])).
% 196.37/196.44 cnf(153,plain,
% 196.37/196.44 (P1(f1(f1(f1(x1531,f1(x1532,x1531)),x1533),f1(f1(x1532,x1531),x1533)))),
% 196.37/196.44 inference(scs_inference,[],[104,147,3])).
% 196.37/196.44 cnf(159,plain,
% 196.37/196.44 (P1(f1(f1(x1591,f1(x1592,x1591)),f1(x1593,f1(x1591,f1(x1592,x1591)))))),
% 196.37/196.44 inference(scs_inference,[],[117,10,3])).
% 196.37/196.44 cnf(166,plain,
% 196.37/196.44 (P1(f1(f1(x1661,x1662),f1(x1663,f1(x1662,f1(x1661,x1662)))))),
% 196.37/196.44 inference(scs_inference,[],[159,153,3])).
% 196.37/196.44 cnf(169,plain,
% 196.37/196.44 (P1(f1(x1691,f1(f1(f1(x1692,f1(x1693,x1692)),x1693),f1(x1694,x1693))))),
% 196.37/196.44 inference(scs_inference,[],[166,1,3])).
% 196.37/196.44 cnf(172,plain,
% 196.37/196.44 (P1(f1(f1(f1(x1721,f1(x1722,x1721)),x1722),f1(x1723,x1722)))),
% 196.37/196.44 inference(scs_inference,[],[169,134,3])).
% 196.37/196.44 cnf(178,plain,
% 196.37/196.44 (P1(f1(f1(x1781,x1782),f1(f1(f1(x1782,f1(x1781,x1782)),x1783),f1(x1784,x1783))))),
% 196.37/196.44 inference(scs_inference,[],[153,20,3])).
% 196.37/196.44 cnf(191,plain,
% 196.37/196.44 (P1(f1(f1(f1(f1(x1911,x1912),f1(f1(f1(x1913,f1(x1912,x1913)),x1912),f1(x1911,x1912))),x1914),f1(x1915,x1914)))),
% 196.37/196.44 inference(scs_inference,[],[172,178,3])).
% 196.37/196.44 cnf(214,plain,
% 196.37/196.44 (P1(f1(f1(f1(x2141,f1(f1(x2141,x2142),f1(x2143,x2142))),f1(x2144,x2145)),f1(f1(f1(f1(x2146,x2144),f1(x2147,x2144)),f1(x2144,x2145)),f1(x2144,x2145))))),
% 196.37/196.44 inference(scs_inference,[],[10,131,3])).
% 196.37/196.44 cnf(218,plain,
% 196.37/196.44 (P1(f1(x2181,f1(f1(x2182,x2183),f1(x2184,f1(x2183,f1(x2185,x2183))))))),
% 196.37/196.44 inference(scs_inference,[],[25,38,3])).
% 196.37/196.44 cnf(222,plain,
% 196.37/196.44 (P1(f1(f1(x2221,x2222),f1(x2223,f1(x2222,f1(x2224,x2222)))))),
% 196.37/196.44 inference(scs_inference,[],[25,218,3])).
% 196.37/196.44 cnf(229,plain,
% 196.37/196.44 (P1(f1(x2291,f1(f1(x2292,x2293),f1(x2294,f1(x2292,x2293)))))),
% 196.37/196.44 inference(scs_inference,[],[222,191,3])).
% 196.37/196.44 cnf(232,plain,
% 196.37/196.44 (P1(f1(f1(x2321,x2322),f1(x2323,f1(x2321,x2322))))),
% 196.37/196.44 inference(scs_inference,[],[229,214,3])).
% 196.37/196.44 cnf(268,plain,
% 196.37/196.44 (P1(f1(f1(f1(x2681,f1(f1(x2681,x2682),f1(x2683,x2682))),f1(x2684,x2685)),f1(f1(x2684,x2685),f1(x2684,x2685))))),
% 196.37/196.44 inference(scs_inference,[],[131,232,3])).
% 196.37/196.44 cnf(282,plain,
% 196.37/196.44 (P1(f1(f1(x2821,f1(x2822,x2823)),f1(x2824,f1(f1(f1(x2822,x2823),x2822),f1(x2821,x2822)))))),
% 196.37/196.44 inference(scs_inference,[],[153,1,3])).
% 196.37/196.44 cnf(286,plain,
% 196.37/196.44 (P1(f1(x2861,f1(f1(f1(f1(f1(x2862,x2863),x2862),f1(x2864,x2862)),x2864),f1(x2865,x2864))))),
% 196.37/196.44 inference(scs_inference,[],[282,1,3])).
% 196.37/196.44 cnf(291,plain,
% 196.37/196.44 (P1(f1(f1(f1(f1(f1(x2911,x2912),x2911),f1(x2913,x2911)),x2913),f1(x2914,x2913)))),
% 196.37/196.44 inference(scs_inference,[],[138,286,3])).
% 196.37/196.44 cnf(296,plain,
% 196.37/196.44 (P1(f1(f1(f1(f1(f1(f1(f1(x2961,x2962),x2961),f1(x2963,x2961)),x2963),f1(x2964,x2963)),x2965),f1(x2966,x2965)))),
% 196.37/196.44 inference(scs_inference,[],[291,20,3])).
% 196.37/196.44 cnf(326,plain,
% 196.37/196.44 (P1(f1(x3261,f1(x3262,f1(f1(x3263,x3264),f1(x3265,f1(x3263,x3264))))))),
% 196.37/196.44 inference(scs_inference,[],[222,296,3])).
% 196.37/196.44 cnf(335,plain,
% 196.37/196.44 (P1(f1(x3351,f1(f1(f1(f1(x3352,x3353),f1(x3354,f1(x3352,x3353))),x3355),f1(x3356,x3355))))),
% 196.37/196.44 inference(scs_inference,[],[326,1,3])).
% 196.37/196.44 cnf(341,plain,
% 196.37/196.44 (P1(f1(f1(f1(f1(x3411,x3412),f1(x3413,f1(x3411,x3412))),x3414),f1(x3415,x3414)))),
% 196.37/196.44 inference(scs_inference,[],[335,268,3])).
% 196.37/196.44 cnf(346,plain,
% 196.37/196.44 (P1(f1(x3461,f1(f1(f1(x3462,f1(f1(x3462,x3463),f1(x3464,x3463))),f1(x3465,x3466)),f1(f1(x3465,x3466),f1(x3465,x3466)))))),
% 196.37/196.44 inference(scs_inference,[],[341,131,3])).
% 196.37/196.44 cnf(359,plain,
% 196.37/196.44 (P1(f1(x3591,f1(x3592,f1(x3593,f1(f1(x3594,x3593),f1(x3595,x3593))))))),
% 196.37/196.44 inference(scs_inference,[],[341,10,3])).
% 196.37/196.44 cnf(363,plain,
% 196.37/196.44 (P1(f1(x3631,f1(x3632,f1(f1(x3633,x3632),f1(x3634,x3632)))))),
% 196.37/196.44 inference(scs_inference,[],[341,359,3])).
% 196.37/196.44 cnf(368,plain,
% 196.37/196.44 (P1(f1(x3681,f1(f1(x3682,x3681),f1(x3683,x3681))))),
% 196.37/196.44 inference(scs_inference,[],[346,363,3])).
% 196.37/196.44 cnf(371,plain,
% 196.37/196.44 (P1(f1(x3711,f1(f1(f1(f1(x3712,x3713),f1(x3714,x3713)),f1(x3712,x3713)),f1(x3713,f1(x3712,x3713)))))),
% 196.37/196.44 inference(scs_inference,[],[368,282,3])).
% 196.37/196.44 cnf(374,plain,
% 196.37/196.44 (P1(f1(f1(f1(f1(x3741,x3742),f1(x3743,x3742)),f1(x3741,x3742)),f1(x3742,f1(x3741,x3742))))),
% 196.37/196.44 inference(scs_inference,[],[371,368,3])).
% 196.37/196.44 cnf(413,plain,
% 196.37/196.44 (P1(f1(x4131,f1(f1(f1(x4132,f1(x4133,x4134)),x4135),f1(f1(x4133,x4134),x4135))))),
% 196.37/196.44 inference(scs_inference,[],[1,229,3])).
% 196.37/196.44 cnf(420,plain,
% 196.37/196.44 (P1(f1(f1(f1(x4201,f1(x4202,x4203)),x4204),f1(f1(x4202,x4203),x4204)))),
% 196.37/196.44 inference(scs_inference,[],[413,374,3])).
% 196.37/196.44 cnf(471,plain,
% 196.37/196.44 (P1(f1(x4711,f1(f1(x4712,x4713),f1(f1(f1(x4713,f1(x4712,x4713)),x4714),f1(x4715,x4714)))))),
% 196.37/196.44 inference(scs_inference,[],[178,232,3])).
% 196.37/196.44 cnf(484,plain,
% 196.37/196.44 (P1(f1(x4841,f1(x4842,f1(f1(f1(x4843,f1(x4844,x4843)),x4844),f1(x4845,x4844)))))),
% 196.37/196.44 inference(scs_inference,[],[232,169,3])).
% 196.37/196.44 cnf(496,plain,
% 196.37/196.44 (P1(f1(x4961,f1(x4962,f1(f1(f1(f1(f1(x4963,x4964),x4963),f1(x4965,x4963)),x4965),f1(x4966,x4965)))))),
% 196.37/196.44 inference(scs_inference,[],[296,232,3])).
% 196.37/196.44 cnf(526,plain,
% 196.37/196.44 (P1(f1(x5261,f1(f1(x5262,x5263),f1(x5264,f1(x5265,f1(x5262,x5263))))))),
% 196.37/196.44 inference(scs_inference,[],[420,341,3])).
% 196.37/196.44 cnf(530,plain,
% 196.37/196.44 (P1(f1(f1(x5301,x5302),f1(x5303,f1(f1(f1(x5301,x5302),x5301),f1(x5304,x5301)))))),
% 196.37/196.44 inference(scs_inference,[],[420,282,3])).
% 196.37/196.44 cnf(534,plain,
% 196.37/196.44 (P1(f1(f1(x5341,x5342),f1(x5343,f1(x5344,f1(x5341,x5342)))))),
% 196.37/196.44 inference(scs_inference,[],[420,526,3])).
% 196.37/196.44 cnf(539,plain,
% 196.37/196.44 (P1(f1(f1(x5391,x5392),f1(x5393,f1(f1(f1(x5394,f1(x5391,x5392)),x5394),f1(x5395,x5394)))))),
% 196.37/196.44 inference(scs_inference,[],[530,420,3])).
% 196.37/196.44 cnf(546,plain,
% 196.37/196.44 (P1(f1(x5461,f1(f1(f1(f1(f1(x5462,f1(x5463,x5464)),x5462),f1(x5465,x5462)),x5463),f1(x5466,x5463))))),
% 196.37/196.44 inference(scs_inference,[],[539,1,3])).
% 196.37/196.44 cnf(549,plain,
% 196.37/196.44 (P1(f1(f1(f1(f1(f1(x5491,f1(x5492,x5493)),x5491),f1(x5494,x5491)),x5492),f1(x5495,x5492)))),
% 196.37/196.44 inference(scs_inference,[],[546,471,3])).
% 196.37/196.44 cnf(555,plain,
% 196.37/196.44 (P1(f1(x5551,f1(f1(f1(f1(f1(x5552,f1(x5553,x5552)),x5553),f1(x5554,x5553)),x5555),f1(x5556,x5555))))),
% 196.37/196.44 inference(scs_inference,[],[484,1,3])).
% 196.37/196.44 cnf(559,plain,
% 196.37/196.44 (P1(f1(f1(f1(f1(f1(x5591,f1(x5592,x5591)),x5592),f1(x5593,x5592)),x5594),f1(x5595,x5594)))),
% 196.37/196.44 inference(scs_inference,[],[555,496,3])).
% 196.37/196.44 cnf(574,plain,
% 196.37/196.44 (P1(f1(x5741,f1(x5742,f1(x5743,f1(f1(x5744,x5742),f1(x5745,x5742))))))),
% 196.37/196.45 inference(scs_inference,[],[534,10,3])).
% 196.37/196.45 cnf(578,plain,
% 196.37/196.45 (P1(f1(x5781,f1(x5782,f1(f1(x5783,x5781),f1(x5784,x5781)))))),
% 196.37/196.45 inference(scs_inference,[],[574,549,3])).
% 196.37/196.45 cnf(592,plain,
% 196.37/196.45 (P1(f1(f1(f1(x5921,f1(x5922,x5921)),x5922),f1(x5923,f1(x5924,f1(x5925,x5922)))))),
% 196.37/196.45 inference(scs_inference,[],[559,38,3])).
% 196.37/196.45 cnf(596,plain,
% 196.37/196.45 (P1(f1(x5961,f1(x5962,f1(x5963,f1(f1(x5963,x5964),f1(x5965,x5964))))))),
% 196.37/196.45 inference(scs_inference,[],[534,20,3])).
% 196.37/196.45 cnf(613,plain,
% 196.37/196.45 (P1(f1(x6131,f1(f1(f1(x6132,f1(f1(x6133,x6134),f1(x6135,x6134))),x6136),f1(x6134,x6136))))),
% 196.37/196.45 inference(scs_inference,[],[574,1,3])).
% 196.37/196.45 cnf(619,plain,
% 196.37/196.45 (P1(f1(f1(f1(x6191,f1(f1(x6192,x6193),f1(x6194,x6193))),x6195),f1(x6193,x6195)))),
% 196.37/196.45 inference(scs_inference,[],[578,613,3])).
% 196.37/196.45 cnf(624,plain,
% 196.37/196.45 (P1(f1(x6241,f1(f1(f1(x6242,f1(f1(x6242,x6243),f1(x6244,x6243))),x6245),f1(x6246,x6245))))),
% 196.37/196.45 inference(scs_inference,[],[596,1,3])).
% 196.37/196.45 cnf(628,plain,
% 196.37/196.45 (P1(f1(f1(f1(x6281,f1(f1(x6281,x6282),f1(x6283,x6282))),x6284),f1(x6285,x6284)))),
% 196.37/196.45 inference(scs_inference,[],[624,592,3])).
% 196.37/196.45 cnf(636,plain,
% 196.37/196.45 (P1(f1(x6361,f1(f1(f1(x6362,f1(f1(x6363,x6361),f1(x6364,x6361))),x6365),f1(x6366,x6365))))),
% 196.37/196.45 inference(scs_inference,[],[619,20,3])).
% 196.37/196.45 cnf(649,plain,
% 196.37/196.45 (P1(f1(x6491,f1(f1(f1(f1(x6491,x6492),f1(x6493,x6492)),x6494),f1(x6495,x6494))))),
% 196.37/196.45 inference(scs_inference,[],[20,38,3])).
% 196.37/196.45 cnf(665,plain,
% 196.37/196.45 (P1(f1(x6651,f1(x6652,f1(f1(f1(f1(x6653,x6654),f1(x6655,x6654)),x6656),f1(x6653,x6656)))))),
% 196.37/196.45 inference(scs_inference,[],[71,232,3])).
% 196.37/196.45 cnf(692,plain,
% 196.37/196.45 (P1(f1(x6921,f1(f1(f1(f1(x6922,x6923),f1(x6924,x6923)),x6925),f1(x6923,x6925))))),
% 196.37/196.45 inference(scs_inference,[],[363,1,3])).
% 196.37/196.45 cnf(698,plain,
% 196.37/196.45 (P1(f1(f1(f1(f1(x6981,x6982),f1(x6983,x6982)),x6984),f1(x6982,x6984)))),
% 196.37/196.45 inference(scs_inference,[],[374,692,3])).
% 196.37/196.45 cnf(703,plain,
% 196.37/196.45 (P1(f1(f1(x7031,x7032),f1(f1(f1(x7033,f1(x7031,x7032)),x7034),f1(x7035,x7034))))),
% 196.37/196.45 inference(scs_inference,[],[420,20,3])).
% 196.37/196.45 cnf(709,plain,
% 196.37/196.45 (P1(f1(x7091,f1(f1(f1(f1(f1(f1(f1(x7092,x7093),x7092),f1(x7094,x7092)),x7094),f1(x7095,x7094)),x7096),f1(x7097,x7096))))),
% 196.37/196.45 inference(scs_inference,[],[496,1,3])).
% 196.37/196.45 cnf(744,plain,
% 196.37/196.45 (P1(f1(x7441,f1(f1(f1(f1(f1(f1(x7442,x7443),f1(x7444,x7443)),x7445),f1(x7442,x7445)),x7446),f1(x7447,x7446))))),
% 196.37/196.45 inference(scs_inference,[],[665,1,3])).
% 196.37/196.45 cnf(753,plain,
% 196.37/196.45 (P1(f1(x7531,f1(x7532,f1(f1(x7531,x7533),f1(x7534,x7533)))))),
% 196.37/196.45 inference(scs_inference,[],[698,1,3])).
% 196.37/196.45 cnf(786,plain,
% 196.37/196.45 (P1(f1(x7861,f1(f1(f1(x7862,f1(f1(x7861,x7863),f1(x7864,x7863))),x7865),f1(x7866,x7865))))),
% 196.37/196.45 inference(scs_inference,[],[38,703,3])).
% 196.37/196.45 cnf(790,plain,
% 196.37/196.45 (P1(f1(f1(f1(f1(f1(f1(f1(f1(x7901,x7902),f1(x7903,x7902)),x7904),f1(x7901,x7904)),x7905),f1(x7906,x7905)),x7907),f1(x7908,x7907)))),
% 196.37/196.45 inference(scs_inference,[],[38,649,3])).
% 196.37/196.45 cnf(793,plain,
% 196.37/196.45 (P1(f1(x7931,f1(x7932,f1(f1(f1(f1(x7931,x7933),f1(x7934,x7933)),x7935),f1(x7936,x7935)))))),
% 196.37/196.45 inference(scs_inference,[],[38,753,3])).
% 196.37/196.45 cnf(805,plain,
% 196.37/196.45 (P1(f1(x8051,f1(f1(x8052,x8053),f1(x8052,f1(x8054,f1(x8055,x8053))))))),
% 196.37/196.45 inference(scs_inference,[],[71,38,3])).
% 196.37/196.45 cnf(809,plain,
% 196.37/196.45 (P1(f1(f1(x8091,x8092),f1(x8091,f1(x8093,f1(x8094,x8092)))))),
% 196.37/196.45 inference(scs_inference,[],[71,805,3])).
% 196.37/196.45 cnf(839,plain,
% 196.37/196.45 (P1(f1(x8391,f1(x8392,f1(f1(f1(x8393,x8394),x8393),f1(x8395,x8393)))))),
% 196.37/196.45 inference(scs_inference,[],[341,1,3])).
% 196.37/196.45 cnf(843,plain,
% 196.37/196.45 (P1(f1(x8431,f1(f1(f1(x8432,x8433),x8432),f1(x8434,x8432))))),
% 196.37/196.45 inference(scs_inference,[],[839,744,3])).
% 196.37/196.45 cnf(848,plain,
% 196.37/196.45 (P1(f1(f1(f1(x8481,x8482),x8481),f1(x8483,x8481)))),
% 196.37/196.45 inference(scs_inference,[],[636,843,3])).
% 196.37/196.45 cnf(869,plain,
% 196.37/196.45 (P1(f1(x8691,f1(f1(x8692,x8693),f1(x8692,x8693))))),
% 196.37/196.45 inference(scs_inference,[],[420,848,3])).
% 196.37/196.45 cnf(879,plain,
% 196.37/196.45 (P1(f1(f1(x8791,x8792),f1(x8791,x8792)))),
% 196.37/196.45 inference(scs_inference,[],[869,786,3])).
% 196.37/196.45 cnf(932,plain,
% 196.37/196.45 (P1(f1(x9321,f1(x9322,f1(x9323,f1(f1(x9321,x9324),f1(x9325,x9324))))))),
% 196.37/196.45 inference(scs_inference,[],[628,38,3])).
% 196.37/196.45 cnf(948,plain,
% 196.37/196.45 (P1(f1(f1(f1(f1(f1(f1(f1(x9481,x9482),x9481),f1(x9483,x9481)),x9484),f1(x9485,x9484)),x9486),f1(x9487,x9486)))),
% 196.37/196.45 inference(scs_inference,[],[649,848,3])).
% 196.37/196.45 cnf(969,plain,
% 196.37/196.45 (P1(f1(f1(f1(f1(x9691,x9692),f1(x9693,x9692)),x9694),f1(x9695,f1(x9696,f1(x9692,x9694)))))),
% 196.37/196.45 inference(scs_inference,[],[698,809,3])).
% 196.37/196.45 cnf(974,plain,
% 196.37/196.45 (P1(f1(x9741,f1(x9742,f1(f1(f1(f1(x9743,x9741),f1(x9744,x9741)),x9745),f1(x9746,x9745)))))),
% 196.37/196.45 inference(scs_inference,[],[698,753,3])).
% 196.37/196.45 cnf(983,plain,
% 196.37/196.45 (P1(f1(x9831,f1(x9832,f1(x9833,f1(x9834,f1(x9835,x9833))))))),
% 196.37/196.45 inference(scs_inference,[],[969,848,3])).
% 196.37/196.45 cnf(1000,plain,
% 196.37/196.45 (P1(f1(x10001,f1(x10002,f1(x10003,f1(x10004,x10002)))))),
% 196.37/196.45 inference(scs_inference,[],[974,983,3])).
% 196.37/196.45 cnf(1005,plain,
% 196.37/196.45 (P1(f1(x10051,f1(x10052,f1(x10053,x10051))))),
% 196.37/196.45 inference(scs_inference,[],[790,1000,3])).
% 196.37/196.45 cnf(1063,plain,
% 196.37/196.45 (P1(f1(x10631,f1(f1(f1(f1(f1(x10632,x10633),x10632),f1(x10634,x10632)),x10635),f1(x10636,x10635))))),
% 196.37/196.45 inference(scs_inference,[],[848,948,3])).
% 196.37/196.45 cnf(1072,plain,
% 196.37/196.45 (P1(f1(f1(f1(f1(f1(x10721,x10722),x10721),f1(x10723,x10721)),x10724),f1(x10725,x10724)))),
% 196.37/196.45 inference(scs_inference,[],[1063,709,3])).
% 196.37/196.45 cnf(1088,plain,
% 196.37/196.45 (P1(f1(x10881,f1(x10882,f1(f1(f1(f1(x10883,x10884),f1(x10883,x10884)),x10885),f1(x10886,x10885)))))),
% 196.37/196.45 inference(scs_inference,[],[879,932,3])).
% 196.37/196.45 cnf(1136,plain,
% 196.37/196.45 (P1(f1(x11361,f1(x11362,f1(f1(f1(f1(f1(x11363,x11364),x11363),f1(x11365,x11363)),x11366),f1(x11367,x11366)))))),
% 196.37/196.45 inference(scs_inference,[],[1005,1072,3])).
% 196.37/196.45 cnf(1212,plain,
% 196.37/196.45 (P1(f1(x12121,f1(x12122,f1(x12123,f1(x12124,f1(x12125,x12125))))))),
% 196.37/196.45 inference(scs_inference,[],[1072,948,3])).
% 196.37/196.45 cnf(1221,plain,
% 196.37/196.45 (P1(f1(x12211,f1(x12212,f1(x12213,f1(x12214,x12214)))))),
% 196.37/196.45 inference(scs_inference,[],[1072,1212,3])).
% 196.37/196.45 cnf(1228,plain,
% 196.37/196.45 (P1(f1(x12281,f1(x12282,f1(x12283,x12283))))),
% 196.37/196.45 inference(scs_inference,[],[1088,1221,3])).
% 196.37/196.45 cnf(1273,plain,
% 196.37/196.45 (P1(f1(x12731,f1(f1(f1(x12732,f1(x12733,x12733)),x12734),f1(x12735,x12734))))),
% 196.37/196.45 inference(scs_inference,[],[1221,1,3])).
% 196.37/196.45 cnf(1279,plain,
% 196.37/196.45 (P1(f1(f1(f1(x12791,f1(x12792,x12792)),x12793),f1(x12794,x12793)))),
% 196.37/196.45 inference(scs_inference,[],[1228,1273,3])).
% 196.37/196.45 cnf(1290,plain,
% 196.37/196.45 (P1(f1(x12901,f1(f1(f1(f1(f1(f1(f1(x12902,x12903),x12902),f1(x12904,x12902)),x12905),f1(x12906,x12905)),x12907),f1(x12908,x12907))))),
% 196.37/196.45 inference(scs_inference,[],[1136,1,3])).
% 196.37/196.45 cnf(1313,plain,
% 196.37/196.45 (P1(f1(x13131,f1(f1(f1(x13132,f1(x13133,f1(x13134,x13134))),x13135),f1(x13136,x13135))))),
% 196.37/196.45 inference(scs_inference,[],[1279,703,3])).
% 196.37/196.45 cnf(1317,plain,
% 196.37/196.45 (P1(f1(f1(f1(x13171,f1(x13172,f1(x13173,x13173))),x13174),f1(x13175,x13174)))),
% 196.37/196.45 inference(scs_inference,[],[1279,1313,3])).
% 196.37/196.45 cnf(1347,plain,
% 196.37/196.45 (P1(f1(x13471,f1(x13472,f1(f1(f1(x13473,x13473),x13474),f1(x13475,x13474)))))),
% 196.37/196.45 inference(scs_inference,[],[1317,1,3])).
% 196.37/196.45 cnf(1361,plain,
% 196.37/196.45 (P1(f1(x13611,f1(f1(f1(f1(f1(x13612,x13612),x13613),f1(x13614,x13613)),x13615),f1(x13616,x13615))))),
% 196.37/196.45 inference(scs_inference,[],[1347,1,3])).
% 196.37/196.45 cnf(1367,plain,
% 196.37/196.45 (P1(f1(f1(f1(f1(f1(x13671,x13671),x13672),f1(x13673,x13672)),x13674),f1(x13675,x13674)))),
% 196.37/196.45 inference(scs_inference,[],[1347,1361,3])).
% 196.37/196.45 cnf(1383,plain,
% 196.37/196.45 (P1(f1(x13831,f1(x13832,f1(f1(f1(f1(f1(x13833,x13833),x13834),f1(x13835,x13834)),x13836),f1(x13837,x13836)))))),
% 196.37/196.45 inference(scs_inference,[],[1367,753,3])).
% 196.37/196.45 cnf(1392,plain,
% 196.37/196.45 (P1(f1(x13921,f1(f1(f1(x13922,f1(f1(f1(x13923,x13923),x13924),f1(x13925,x13924))),x13926),f1(x13927,x13926))))),
% 196.37/196.45 inference(scs_inference,[],[1367,703,3])).
% 196.37/196.45 cnf(1396,plain,
% 196.37/196.45 (P1(f1(f1(f1(x13961,f1(f1(f1(x13962,x13962),x13963),f1(x13964,x13963))),x13965),f1(x13966,x13965)))),
% 196.37/196.45 inference(scs_inference,[],[1367,1392,3])).
% 196.37/196.45 cnf(1401,plain,
% 196.37/196.45 (P1(f1(x14011,f1(x14012,f1(x14013,f1(x14014,x14013)))))),
% 196.37/196.45 inference(scs_inference,[],[1367,10,3])).
% 196.37/196.45 cnf(1405,plain,
% 196.37/196.45 (P1(f1(x14051,f1(x14052,f1(x14053,x14052))))),
% 196.37/196.45 inference(scs_inference,[],[1401,1396,3])).
% 196.37/196.45 cnf(1412,plain,
% 196.37/196.45 (P1(f1(x14121,f1(x14122,x14121)))),
% 196.37/196.45 inference(scs_inference,[],[1290,1405,3])).
% 196.37/196.45 cnf(1430,plain,
% 196.37/196.45 (P1(f1(f1(f1(x14301,f1(f1(f1(x14302,f1(x14303,x14302)),x14304),f1(x14305,x14304))),x14306),f1(x14307,x14306)))),
% 196.37/196.45 inference(scs_inference,[],[1412,786,3])).
% 196.37/196.45 cnf(1435,plain,
% 196.37/196.45 (P1(f1(x14351,f1(x14352,f1(x14353,f1(f1(x14352,x14354),f1(x14355,x14354))))))),
% 196.37/196.45 inference(scs_inference,[],[1412,753,3])).
% 196.37/196.45 cnf(1438,plain,
% 196.37/196.45 (P1(f1(x14381,f1(f1(f1(f1(f1(x14382,f1(x14383,x14382)),x14384),f1(x14385,x14384)),x14386),f1(x14387,x14386))))),
% 196.37/196.45 inference(scs_inference,[],[1412,793,3])).
% 196.37/196.45 cnf(1443,plain,
% 196.37/196.45 (P1(f1(f1(f1(f1(f1(x14431,f1(x14432,x14431)),x14433),f1(x14434,x14433)),x14435),f1(x14436,x14435)))),
% 196.37/196.45 inference(scs_inference,[],[1412,1438,3])).
% 196.37/196.45 cnf(1449,plain,
% 196.37/196.45 (P1(f1(x14491,f1(x14492,f1(f1(f1(x14493,f1(x14494,x14493)),x14495),f1(x14496,x14495)))))),
% 196.37/196.45 inference(scs_inference,[],[1430,1443,3])).
% 196.37/196.45 cnf(1453,plain,
% 196.37/196.45 (P1(f1(x14531,f1(f1(f1(x14532,f1(x14533,x14532)),x14534),f1(x14535,x14534))))),
% 196.37/196.45 inference(scs_inference,[],[1449,1383,3])).
% 196.37/196.45 cnf(1458,plain,
% 196.37/196.45 (P1(f1(f1(f1(x14581,f1(x14582,x14581)),x14583),f1(x14584,x14583)))),
% 196.37/196.45 inference(scs_inference,[],[1443,1453,3])).
% 196.37/196.45 cnf(1463,plain,
% 196.37/196.45 (P1(f1(x14631,f1(f1(f1(x14632,f1(x14633,f1(x14634,x14633))),x14635),f1(x14636,x14635))))),
% 196.37/196.45 inference(scs_inference,[],[1458,703,3])).
% 196.37/196.45 cnf(1467,plain,
% 196.37/196.45 (P1(f1(f1(f1(x14671,f1(x14672,f1(x14673,x14672))),x14674),f1(x14675,x14674)))),
% 196.37/196.45 inference(scs_inference,[],[1463,1435,3])).
% 196.37/196.45 cnf(1472,plain,
% 196.37/196.45 (P1(f1(f1(f1(x14721,f1(x14722,x14721)),x14723),f1(x14724,f1(x14725,f1(x14726,x14723)))))),
% 196.37/196.45 inference(scs_inference,[],[1458,809,3])).
% 196.37/196.45 cnf(1477,plain,
% 196.37/196.45 (P1(f1(x14771,f1(x14772,f1(f1(f1(x14773,x14774),x14775),f1(x14774,x14775)))))),
% 196.37/196.45 inference(scs_inference,[],[1467,1,3])).
% 196.37/196.45 cnf(1486,plain,
% 196.37/196.45 (P1(f1(x14861,f1(f1(f1(x14862,x14863),x14864),f1(x14863,x14864))))),
% 196.37/196.45 inference(scs_inference,[],[1472,1477,3])).
% 196.37/196.45 cnf(1739,plain,
% 196.37/196.45 (P1(f1(x17391,f1(f1(f1(x17392,x17393),x17394),f1(f1(f1(x17394,x17395),x17393),x17394))))),
% 196.37/196.45 inference(scs_inference,[],[20,4])).
% 196.37/196.45 cnf(1792,plain,
% 196.37/196.45 (P1(f1(f1(f1(x17921,x17922),x17923),f1(f1(f1(x17923,x17924),x17922),x17923)))),
% 196.37/196.45 inference(scs_inference,[],[1,1486,1739,4,3])).
% 196.37/196.45 cnf(2076,plain,
% 196.37/196.45 (~P1(f1(f1(x20761,f1(x20762,x20761)),f1(a2,f1(f1(a2,a3),a3))))),
% 196.37/196.45 inference(scs_inference,[],[8,1458,3])).
% 196.37/196.45 cnf(2544,plain,
% 196.37/196.45 (~P1(f1(f1(f1(f1(a2,a3),a3),x25441),f1(a2,a3)))),
% 196.37/196.45 inference(scs_inference,[],[20,2076,3,4])).
% 196.37/196.45 cnf(2560,plain,
% 196.37/196.45 ($false),
% 196.37/196.45 inference(scs_inference,[],[25,2544,1792,3]),
% 196.37/196.45 ['proof']).
% 196.37/196.45 % SZS output end Proof
% 196.37/196.45 % Total time :195.903805s
%------------------------------------------------------------------------------