%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL364-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 : n007.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 250.76s 250.70s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL364-1 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.02 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.11/0.37 % Computer : n007.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Fri Sep 4 20:30:39 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.24/0.53 start to proof:theBenchmark
% 250.65/250.70 %-------------------------------------------
% 250.65/250.70 % File :CSE---1.7
% 250.65/250.70 % Problem :theBenchmark
% 250.65/250.70 % Transform :cnf
% 250.65/250.70 % Format :tptp:raw
% 250.76/250.70 % Command :java -jar mcs_scs.jar %d %s
% 250.76/250.70
% 250.76/250.70 % Result :Theorem 250.176271s
% 250.76/250.70 % Output :CNFRefutation 250.176271s
% 250.76/250.70 %-------------------------------------------
% 250.76/250.70 %--------------------------------------------------------------------------
% 250.76/250.70 % File : LCL364-1 : TPTP v9.3.1. Released v2.3.0.
% 250.76/250.70 % Domain : Logic Calculi (Implication/Negation 2 valued sentential)
% 250.76/250.70 % Problem : CN-13 depends on the Lukasiewicz system
% 250.76/250.70 % Version : [McC92] axioms.
% 250.76/250.70 % English : An axiomatisation of the Implication/Negation 2 valued
% 250.76/250.70 % sentential calculus is {CN-1,CN-2,CN-3} by Lukasiewicz.
% 250.76/250.70 % Show that CN-13 depends on the Lukasiewicz system.
% 250.76/250.70
% 250.76/250.70 % Refs : [Wos96] Wos (1996), Combining Resonance with Heat
% 250.76/250.70 % : [McC92] McCune (1992), Email to G. Sutcliffe
% 250.76/250.70 % Source : [Wos96]
% 250.76/250.70 % Names : thesis_13 [Wos96]
% 250.76/250.70
% 250.76/250.70 % Status : Unsatisfiable
% 250.76/250.70 % Rating : 0.00 v6.1.0, 0.07 v6.0.0, 0.00 v5.5.0, 0.12 v5.4.0, 0.17 v5.3.0, 0.25 v5.2.0, 0.15 v5.1.0, 0.25 v5.0.0, 0.27 v4.1.0, 0.20 v4.0.1, 0.00 v2.6.0, 0.29 v2.5.0, 0.00 v2.3.0
% 250.76/250.70 % Syntax : Number of clauses : 5 ( 4 unt; 0 nHn; 2 RR)
% 250.76/250.70 % Number of literals : 7 ( 0 equ; 3 neg)
% 250.76/250.70 % Maximal clause size : 3 ( 1 avg)
% 250.76/250.70 % Maximal term depth : 5 ( 2 avg)
% 250.76/250.70 % Number of predicates : 1 ( 1 usr; 0 prp; 1-1 aty)
% 250.76/250.70 % Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% 250.76/250.70 % Number of variables : 8 ( 1 sgn)
% 250.76/250.70 % SPC : CNF_UNS_RFO_NEQ_HRN
% 250.76/250.70
% 250.76/250.70 % Comments :
% 250.76/250.70 %--------------------------------------------------------------------------
% 250.76/250.70 cnf(condensed_detachment,axiom,
% 250.76/250.70 ( ~ is_a_theorem(implies(X,Y))
% 250.76/250.70 | ~ is_a_theorem(X)
% 250.76/250.70 | is_a_theorem(Y) ) ).
% 250.76/250.70
% 250.76/250.70 cnf(cn_1,axiom,
% 250.76/250.70 is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) ).
% 250.76/250.70
% 250.76/250.70 cnf(cn_2,axiom,
% 250.76/250.70 is_a_theorem(implies(implies(not(X),X),X)) ).
% 250.76/250.70
% 250.76/250.70 cnf(cn_3,axiom,
% 250.76/250.70 is_a_theorem(implies(X,implies(not(X),Y))) ).
% 250.76/250.70
% 250.76/250.70 cnf(prove_cn_13,negated_conjecture,
% 250.76/250.70 ~ is_a_theorem(implies(implies(not(x),y),implies(z,implies(implies(y,x),x)))) ).
% 250.76/250.70
% 250.76/250.70 %--------------------------------------------------------------------------
% 250.76/250.70 %-------------------------------------------
% 250.76/250.70 % Proof found
% 250.76/250.70 % SZS status Theorem for theBenchmark
% 250.76/250.70 % SZS output start Proof
% 250.76/250.70 %ClaNum:5(EqnAxiom:0)
% 250.76/250.70 %VarNum:16(SingletonVarNum:8)
% 250.76/250.70 %MaxLitNum:3
% 250.76/250.70 %MaxfuncDepth:4
% 250.76/250.70 %SharedTerms:10
% 250.76/250.70 %goalClause: 4
% 250.76/250.70 %singleGoalClaCount:1
% 250.76/250.70 [4]~P1(f2(f2(f1(a3),a4),f2(a5,f2(f2(a4,a3),a3))))
% 250.76/250.70 [2]P1(f2(f2(f1(x21),x21),x21))
% 250.76/250.70 [1]P1(f2(x11,f2(f1(x11),x12)))
% 250.76/250.70 [3]P1(f2(f2(x31,x32),f2(f2(x32,x33),f2(x31,x33))))
% 250.76/250.70 [5]P1(x51)+~P1(x52)+~P1(f2(x52,x51))
% 250.76/250.70 %EqnAxiom
% 250.76/250.70
% 250.76/250.70 %-------------------------------------------
% 250.76/250.71 cnf(6,plain,
% 250.76/250.71 (P1(f2(f2(x61,x62),f2(f2(f1(x61),x61),x62)))),
% 250.76/250.71 inference(scs_inference,[],[2,3,5])).
% 250.76/250.71 cnf(9,plain,
% 250.76/250.71 (P1(f2(f2(f1(x91),x91),f2(f1(x91),x92)))),
% 250.76/250.71 inference(scs_inference,[],[6,1,5])).
% 250.76/250.71 cnf(12,plain,
% 250.76/250.71 (P1(f2(f1(x121),x122))+~P1(f2(f1(x121),x121))),
% 250.76/250.71 inference(scs_inference,[],[9,5])).
% 250.76/250.71 cnf(14,plain,
% 250.76/250.71 (P1(f2(f2(f2(f1(x141),x142),x143),f2(x141,x143)))),
% 250.76/250.71 inference(scs_inference,[],[1,3,5])).
% 250.76/250.71 cnf(17,plain,
% 250.76/250.71 (P1(f2(f2(f1(f2(x171,x172)),f2(x171,x172)),f2(f2(x172,x173),f2(x171,x173))))),
% 250.76/250.71 inference(scs_inference,[],[3,6,5])).
% 250.76/250.71 cnf(20,plain,
% 250.76/250.71 (P1(f2(f2(x201,x202),f2(x203,x202)))+~P1(f2(f1(f2(x203,x201)),f2(x203,x201)))),
% 250.76/250.71 inference(scs_inference,[],[17,5])).
% 250.76/250.71 cnf(22,plain,
% 250.76/250.71 (P1(f2(f2(f1(f2(f1(x221),x221)),f2(f1(x221),x221)),f2(f1(x221),x222)))),
% 250.76/250.71 inference(scs_inference,[],[9,6,5])).
% 250.76/250.71 cnf(25,plain,
% 250.76/250.71 (P1(f2(f2(f2(f1(x251),x252),x253),f2(f2(f1(x251),x251),x253)))),
% 250.76/250.71 inference(scs_inference,[],[9,3,5])).
% 250.76/250.71 cnf(28,plain,
% 250.76/250.71 (P1(f2(f1(x281),x282))+~P1(f2(f1(f2(f1(x281),x281)),f2(f1(x281),x281)))),
% 250.76/250.71 inference(scs_inference,[],[22,5])).
% 250.76/250.71 cnf(30,plain,
% 250.76/250.71 (P1(f2(f2(x301,x302),f2(x303,x302)))+~P1(f2(f1(f2(f1(f2(x303,x301)),f2(x303,x301))),f2(f1(f2(x303,x301)),f2(x303,x301))))),
% 250.76/250.71 inference(scs_inference,[],[22,5,20])).
% 250.76/250.71 cnf(40,plain,
% 250.76/250.71 (P1(f2(f2(f2(f2(x401,x402),f2(x403,x402)),x404),f2(f2(f1(f2(x403,x401)),f2(x403,x401)),x404)))),
% 250.76/250.71 inference(scs_inference,[],[17,3,5])).
% 250.76/250.71 cnf(43,plain,
% 250.76/250.71 (P1(f2(f2(f1(f2(x431,f1(x432))),f2(x431,f1(x432))),f2(f2(f1(x432),x432),f2(x431,x433))))),
% 250.76/250.71 inference(scs_inference,[],[40,25,5])).
% 250.76/250.71 cnf(47,plain,
% 250.76/250.71 (P1(f2(f2(f1(x471),x471),f2(x472,x473)))+~P1(f2(f1(f2(x472,f1(x471))),f2(x472,f1(x471))))),
% 250.76/250.71 inference(scs_inference,[],[43,5])).
% 250.76/250.71 cnf(49,plain,
% 250.76/250.71 (~P1(f2(f1(f2(f1(f2(x491,f1(x492))),f2(x491,f1(x492)))),f2(f1(f2(x491,f1(x492))),f2(x491,f1(x492)))))+P1(f2(f2(f1(x492),x492),f2(x491,x493)))),
% 250.76/250.71 inference(scs_inference,[],[28,47])).
% 250.76/250.71 cnf(50,plain,
% 250.76/250.71 (~P1(f2(f1(f2(f1(f2(x501,f2(x502,x503))),f2(x501,f2(x502,x503)))),f2(f1(f2(x501,f2(x502,x503))),f2(x501,f2(x502,x503)))))+P1(f2(f2(f1(f2(x504,x502)),f2(x504,x502)),f2(x501,f2(x504,x503))))),
% 250.76/250.71 inference(scs_inference,[],[40,30,5])).
% 250.76/250.71 cnf(51,plain,
% 250.76/250.71 (P1(f2(f2(x511,f1(x512)),f2(f2(f1(x512),x512),f2(x511,x513))))),
% 250.76/250.71 inference(scs_inference,[],[43,14,5])).
% 250.76/250.71 cnf(60,plain,
% 250.76/250.71 (P1(f2(x601,f2(f2(f1(x602),x602),f2(f1(x601),x603))))),
% 250.76/250.71 inference(scs_inference,[],[51,14,5])).
% 250.76/250.71 cnf(64,plain,
% 250.76/250.71 (P1(f2(f2(f2(f2(f1(x641),x641),f2(x642,x643)),x644),f2(f2(x642,f1(x641)),x644)))),
% 250.76/250.71 inference(scs_inference,[],[51,3,5])).
% 250.76/250.71 cnf(67,plain,
% 250.76/250.71 (~P1(f2(f1(f2(f1(f2(x671,f2(f1(x672),x672))),f2(x671,f2(f1(x672),x672)))),f2(f1(f2(x671,f2(f1(x672),x672))),f2(x671,f2(f1(x672),x672)))))+P1(f2(f2(x673,f1(x672)),f2(x671,f2(x673,x674))))),
% 250.76/250.71 inference(scs_inference,[],[64,30,5])).
% 250.76/250.71 cnf(69,plain,
% 250.76/250.71 (P1(f2(f2(f2(f2(f1(x691),x691),f2(f1(x692),x693)),x694),f2(x692,x694)))),
% 250.76/250.71 inference(scs_inference,[],[60,3,5])).
% 250.76/250.71 cnf(72,plain,
% 250.76/250.71 (~P1(f2(f1(f2(f1(f2(x721,f2(f2(f2(f1(x722),x722),f2(x723,x724)),x725))),f2(x721,f2(f2(f2(f1(x722),x722),f2(x723,x724)),x725)))),f2(f1(f2(x721,f2(f2(f2(f1(x722),x722),f2(x723,x724)),x725))),f2(x721,f2(f2(f2(f1(x722),x722),f2(x723,x724)),x725)))))+P1(f2(x721,f2(f2(x723,f1(x722)),x725)))),
% 250.76/250.71 inference(scs_inference,[],[64,30,5])).
% 250.76/250.71 cnf(74,plain,
% 250.76/250.71 (P1(f2(x741,f2(f1(f2(f1(x741),x742)),x743)))),
% 250.76/250.71 inference(scs_inference,[],[1,14,5])).
% 250.76/250.71 cnf(78,plain,
% 250.76/250.71 (~P1(f2(f1(f2(f1(f2(x781,x782)),f2(x781,x782))),f2(f1(f2(x781,x782)),f2(x781,x782))))+P1(f2(f1(f2(f2(x782,x783),f2(x781,x783))),x784))),
% 250.76/250.71 inference(scs_inference,[],[1,30,5])).
% 250.76/250.71 cnf(80,plain,
% 250.76/250.71 (P1(f2(f2(f1(f2(f1(x801),x801)),f2(f1(x801),x801)),x801))),
% 250.76/250.71 inference(scs_inference,[],[2,6,5])).
% 250.76/250.71 cnf(83,plain,
% 250.76/250.71 (P1(f2(f2(f1(x831),x831),f2(f2(f1(f1(x831)),f1(x831)),x832)))),
% 250.76/250.71 inference(scs_inference,[],[2,51,5])).
% 250.76/250.71 cnf(88,plain,
% 250.76/250.71 (P1(f2(x881,x881))),
% 250.76/250.71 inference(scs_inference,[],[2,14,5])).
% 250.76/250.71 cnf(91,plain,
% 250.76/250.71 (P1(f2(f1(f2(f2(f1(x911),x911),x911)),x912))),
% 250.76/250.71 inference(scs_inference,[],[2,1,5])).
% 250.76/250.71 cnf(94,plain,
% 250.76/250.71 (~P1(f2(f1(f2(f1(f2(x941,x942)),f2(x941,x942))),f2(f1(f2(x941,x942)),f2(x941,x942))))+P1(f2(f2(f2(x941,x943),x944),f2(f2(x942,x943),x944)))),
% 250.76/250.71 inference(scs_inference,[],[78,20])).
% 250.76/250.71 cnf(99,plain,
% 250.76/250.71 (P1(f2(f2(f1(f2(x991,x992)),f2(x991,x992)),f2(f2(f2(x991,x993),x994),f2(f2(x992,x993),x994))))),
% 250.76/250.71 inference(scs_inference,[],[3,40,5])).
% 250.76/250.71 cnf(103,plain,
% 250.76/250.71 (P1(f2(f2(f2(f2(f1(x1031),x1031),x1032),x1033),f2(f2(x1031,x1032),x1033)))),
% 250.76/250.71 inference(scs_inference,[],[99,91,5])).
% 250.76/250.71 cnf(107,plain,
% 250.76/250.71 (~P1(f2(f1(f2(f1(f2(x1071,x1072)),f2(x1071,x1072))),f2(f1(f2(x1071,x1072)),f2(x1071,x1072))))+P1(f2(f2(f2(f2(x1072,x1073),x1074),x1075),f2(f2(f2(x1071,x1073),x1074),x1075)))),
% 250.76/250.71 inference(scs_inference,[],[3,94,5])).
% 250.76/250.72 cnf(108,plain,
% 250.76/250.72 (P1(f2(f2(x1081,x1082),f2(f2(x1082,x1083),f2(f2(f1(x1081),x1081),x1083))))),
% 250.76/250.72 inference(scs_inference,[],[3,103,5])).
% 250.76/250.72 cnf(116,plain,
% 250.76/250.72 (~P1(f2(f1(f2(f1(f2(x1161,x1162)),f2(x1161,x1162))),f2(f1(f2(x1161,x1162)),f2(x1161,x1162))))+P1(f2(f2(x1162,x1163),f2(f2(x1163,x1164),f2(x1161,x1164))))),
% 250.76/250.72 inference(scs_inference,[],[3,94,5])).
% 250.76/250.72 cnf(124,plain,
% 250.76/250.72 (P1(f2(f2(f2(f2(x1241,x1242),f2(x1243,x1242)),x1244),f2(f2(x1243,x1241),x1244)))),
% 250.76/250.72 inference(scs_inference,[],[3,1,5,20])).
% 250.76/250.72 cnf(126,plain,
% 250.76/250.72 (P1(f2(f2(x1261,x1262),f2(f2(f2(x1261,x1263),x1264),f2(f2(x1262,x1263),x1264))))),
% 250.76/250.72 inference(scs_inference,[],[3,124,5])).
% 250.76/250.72 cnf(134,plain,
% 250.76/250.72 (~P1(f2(f1(f2(f1(f2(x1341,x1342)),f2(x1341,x1342))),f2(f1(f2(x1341,x1342)),f2(x1341,x1342))))+~P1(f2(f2(f2(f2(x1341,x1343),x1344),f2(f2(x1342,x1343),x1344)),f2(f2(f1(a3),a4),f2(a5,f2(f2(a4,a3),a3)))))),
% 250.76/250.72 inference(scs_inference,[],[4,5,94])).
% 250.76/250.72 cnf(135,plain,
% 250.76/250.72 (P1(f2(f2(x1351,x1352),f2(f2(f1(f2(x1352,x1353)),f2(x1352,x1353)),f2(x1351,x1353))))),
% 250.76/250.72 inference(scs_inference,[],[6,124,5])).
% 250.76/250.72 cnf(144,plain,
% 250.76/250.72 (~P1(f2(f1(f2(f1(f2(x1441,x1442)),f2(x1441,x1442))),f2(f1(f2(x1441,x1442)),f2(x1441,x1442))))+P1(f2(f2(f1(f2(x1442,x1443)),f2(x1442,x1443)),f2(x1441,x1443)))),
% 250.76/250.72 inference(scs_inference,[],[6,5,30])).
% 250.76/250.72 cnf(145,plain,
% 250.76/250.72 (P1(f2(f2(f1(f2(x1451,x1452)),f2(x1451,x1452)),f2(f2(f1(f2(x1452,x1453)),f2(x1452,x1453)),f2(x1451,x1453))))),
% 250.76/250.72 inference(scs_inference,[],[6,40,5])).
% 250.76/250.72 cnf(149,plain,
% 250.76/250.72 (P1(f2(x1491,f2(f2(f1(f1(x1491)),f1(x1491)),x1492)))),
% 250.76/250.72 inference(scs_inference,[],[6,14,5])).
% 250.76/250.72 cnf(156,plain,
% 250.76/250.72 (P1(f2(x1561,f2(x1562,f2(f1(x1561),x1563))))),
% 250.76/250.72 inference(scs_inference,[],[14,69,5])).
% 250.76/250.72 cnf(160,plain,
% 250.76/250.72 (P1(f2(f2(x1601,f1(x1602)),f2(x1602,f2(x1601,x1603))))),
% 250.76/250.72 inference(scs_inference,[],[14,124,5])).
% 250.76/250.72 cnf(164,plain,
% 250.76/250.72 (P1(f2(f2(x1641,x1642),f2(f2(x1642,x1643),f2(x1644,x1643))))+~P1(f2(f2(f1(f1(f2(f1(f2(x1644,x1641)),f2(x1644,x1641)))),x1645),f2(f1(f2(x1644,x1641)),f2(x1644,x1641))))),
% 250.76/250.72 inference(scs_inference,[],[14,116,5])).
% 250.76/250.72 cnf(169,plain,
% 250.76/250.72 (P1(f2(f2(x1691,f2(x1692,x1693)),f2(f2(f1(f2(x1694,x1692)),f2(x1694,x1692)),f2(x1691,f2(x1694,x1693)))))),
% 250.76/250.72 inference(scs_inference,[],[40,124,5])).
% 250.76/250.72 cnf(173,plain,
% 250.76/250.72 (P1(f2(f2(x1731,f2(f1(x1732),x1732)),f2(f2(x1733,f1(x1732)),f2(x1731,f2(x1733,x1734)))))),
% 250.76/250.72 inference(scs_inference,[],[64,124,5])).
% 250.76/250.72 cnf(182,plain,
% 250.76/250.72 (~P1(f2(f1(f2(f1(f2(x1821,f2(f1(x1822),x1822))),f2(x1821,f2(f1(x1822),x1822)))),f2(f1(f2(x1821,f2(f1(x1822),x1822))),f2(x1821,f2(f1(x1822),x1822)))))+P1(f2(x1821,f2(f2(f1(f1(x1822)),f1(x1822)),x1823)))),
% 250.76/250.72 inference(scs_inference,[],[83,30,5])).
% 250.76/250.72 cnf(189,plain,
% 250.76/250.72 (P1(f2(x1891,f2(f1(f2(x1892,x1892)),x1893)))),
% 250.76/250.72 inference(scs_inference,[],[88,156,5])).
% 250.76/250.72 cnf(192,plain,
% 250.76/250.72 (P1(f2(f1(f2(x1921,x1921)),x1922))),
% 250.76/250.72 inference(scs_inference,[],[88,156,5,28])).
% 250.76/250.72 cnf(196,plain,
% 250.76/250.72 (P1(f2(f1(f2(f1(f2(x1961,x1961)),x1962)),x1963))),
% 250.76/250.72 inference(scs_inference,[],[189,12])).
% 250.76/250.72 cnf(199,plain,
% 250.76/250.72 (~P1(f1(f2(x1991,x1991)))),
% 250.76/250.72 inference(scs_inference,[],[192,189,4,12,5])).
% 250.76/250.72 cnf(205,plain,
% 250.76/250.72 (P1(f2(f2(f1(f2(x2051,x2052)),f2(x2051,x2052)),f2(f2(f1(x2051),x2051),x2052)))),
% 250.76/250.72 inference(scs_inference,[],[91,145,5])).
% 250.76/250.72 cnf(214,plain,
% 250.76/250.72 (~P1(f2(f2(x2141,f2(f1(x2141),x2142)),f1(f2(x2143,x2143))))),
% 250.76/250.72 inference(scs_inference,[],[1,199,5])).
% 250.76/250.72 cnf(270,plain,
% 250.76/250.72 (~P1(f2(f2(f1(f2(x2701,x2701)),x2702),f1(f2(x2703,x2703))))),
% 250.76/250.72 inference(scs_inference,[],[199,192,5])).
% 250.76/250.72 cnf(310,plain,
% 250.76/250.72 (~P1(f2(f2(x3101,x3101),f1(f2(x3102,x3102))))),
% 250.76/250.72 inference(scs_inference,[],[199,88,5])).
% 250.76/250.72 cnf(315,plain,
% 250.76/250.72 (P1(f2(f2(f2(f2(f1(f1(x3151)),f1(x3151)),x3152),x3153),f2(f2(x3153,x3154),f2(x3151,x3154))))),
% 250.76/250.72 inference(scs_inference,[],[149,74,116,5])).
% 250.76/250.72 cnf(333,plain,
% 250.76/250.72 (P1(f2(f2(f2(f2(x3331,x3332),f2(x3333,x3332)),x3334),f2(f2(x3334,x3335),f2(f2(x3333,x3331),x3335))))),
% 250.76/250.72 inference(scs_inference,[],[3,74,116,5])).
% 250.76/250.72 cnf(357,plain,
% 250.76/250.72 (P1(f2(f2(f2(f2(f1(f1(x3571)),f1(x3571)),x3572),x3573),f2(x3571,x3573)))),
% 250.76/250.72 inference(scs_inference,[],[315,196,5,30])).
% 250.76/250.72 cnf(358,plain,
% 250.76/250.72 (~P1(f2(f2(f2(f1(x3581),x3581),x3581),f2(f2(x3582,x3582),f1(f2(x3583,x3583)))))),
% 250.76/250.72 inference(scs_inference,[],[310,2,5])).
% 250.76/250.72 cnf(372,plain,
% 250.76/250.72 (~P1(f2(f2(x3721,x3721),f2(f2(x3722,x3722),f1(f2(x3723,x3723)))))),
% 250.76/250.72 inference(scs_inference,[],[88,310,5])).
% 250.76/250.72 cnf(396,plain,
% 250.76/250.72 (P1(f2(f2(f2(f1(x3961),x3962),x3963),f2(f2(x3963,x3964),f2(x3961,x3964))))),
% 250.76/250.72 inference(scs_inference,[],[1,156,116,5])).
% 250.76/250.72 cnf(457,plain,
% 250.76/250.72 (P1(f2(x4571,f2(f2(x4572,f1(x4573)),f2(f2(f1(f1(x4571)),f1(x4571)),f2(x4572,x4574)))))),
% 250.76/250.72 inference(scs_inference,[],[357,173,5])).
% 250.76/250.72 cnf(471,plain,
% 250.76/250.72 (~P1(f2(f2(f2(f1(f1(a3)),f1(a3)),a4),f2(a5,f2(f2(a4,a3),a3))))),
% 250.76/250.72 inference(scs_inference,[],[4,103,5])).
% 250.76/250.72 cnf(478,plain,
% 250.76/250.72 (P1(f2(f2(f1(f2(x4781,x4782)),f2(x4781,x4782)),f2(f2(f2(f1(x4782),x4783),x4784),f2(x4781,x4784))))),
% 250.76/250.72 inference(scs_inference,[],[14,169,5])).
% 250.76/250.72 cnf(481,plain,
% 250.76/250.72 (P1(f2(f2(f1(x4811),x4811),f2(f2(f2(f1(x4811),x4812),x4813),f2(f2(x4814,x4812),x4813))))),
% 250.76/250.72 inference(scs_inference,[],[25,126,5])).
% 250.76/250.72 cnf(489,plain,
% 250.76/250.72 (P1(f2(f2(x4891,f1(x4892)),f2(f2(f2(x4891,x4893),x4894),f2(x4892,x4894))))),
% 250.76/250.72 inference(scs_inference,[],[64,396,5])).
% 250.76/250.72 cnf(493,plain,
% 250.76/250.72 (P1(f2(f1(f2(f2(f2(f2(f2(x4931,x4932),x4933),f2(x4934,x4933)),x4935),f2(f2(x4931,f1(x4934)),x4935))),x4936))),
% 250.76/250.72 inference(scs_inference,[],[74,489,5,78])).
% 250.76/250.72 cnf(504,plain,
% 250.76/250.72 (P1(f2(f2(f2(f1(f2(x5041,x5041)),x5042),x5043),f2(f2(x5044,x5042),x5043)))),
% 250.76/250.72 inference(scs_inference,[],[481,192,5])).
% 250.76/250.72 cnf(508,plain,
% 250.76/250.72 (P1(f2(f2(x5081,f2(x5082,x5082)),f2(f2(f2(f1(x5082),x5083),x5084),f2(x5082,x5084))))),
% 250.76/250.72 inference(scs_inference,[],[478,504,5])).
% 250.76/250.72 cnf(518,plain,
% 250.76/250.72 (P1(f2(f2(f2(f2(f1(f2(x5181,x5182)),f2(x5181,x5182)),f2(x5183,x5182)),x5184),f2(f2(x5183,x5181),x5184)))),
% 250.76/250.72 inference(scs_inference,[],[135,3,5])).
% 250.76/250.72 cnf(521,plain,
% 250.76/250.72 (P1(f2(f2(f1(f2(x5211,x5212)),f2(x5211,x5212)),f2(f2(x5213,f1(x5212)),f2(x5211,f2(x5213,x5214)))))),
% 250.76/250.72 inference(scs_inference,[],[160,169,5])).
% 250.76/250.72 cnf(524,plain,
% 250.76/250.72 (P1(f2(f2(x5241,f1(f2(x5242,x5242))),f2(x5243,f2(x5241,x5244))))),
% 250.76/250.72 inference(scs_inference,[],[189,173,5])).
% 250.76/250.72 cnf(538,plain,
% 250.76/250.72 (P1(f2(f2(f2(f1(f2(x5381,x5381)),x5382),x5383),f2(x5384,x5383)))),
% 250.76/250.72 inference(scs_inference,[],[489,192,5])).
% 250.76/250.72 cnf(547,plain,
% 250.76/250.72 (P1(f2(x5471,f2(f2(f2(f1(x5472),x5473),x5474),f2(x5472,x5474))))),
% 250.76/250.72 inference(scs_inference,[],[538,508,5])).
% 250.76/250.72 cnf(551,plain,
% 250.76/250.72 (P1(f2(f2(x5511,f1(f2(x5512,x5513))),f2(f2(f2(f1(x5512),x5514),x5513),f2(x5511,x5515))))),
% 250.76/250.72 inference(scs_inference,[],[547,521,5])).
% 250.76/250.72 cnf(572,plain,
% 250.76/250.72 (P1(f2(f2(f2(f2(f2(f1(x5721),x5722),x5723),f2(x5721,x5723)),x5724),f2(f2(x5725,x5726),x5724)))),
% 250.76/250.72 inference(scs_inference,[],[333,547,5])).
% 250.76/250.72 cnf(576,plain,
% 250.76/250.72 (~P1(f2(f2(f2(f2(f1(x5761),x5762),x5763),f2(x5761,x5763)),f2(a5,f2(f2(a4,a3),a3))))),
% 250.76/250.72 inference(scs_inference,[],[572,471,5])).
% 250.76/250.72 cnf(579,plain,
% 250.76/250.72 (P1(f2(f2(f2(f2(f2(f1(x5791),x5792),x5793),f2(x5794,x5793)),x5795),f2(f2(x5794,x5791),x5795)))),
% 250.76/250.72 inference(scs_inference,[],[478,396,5])).
% 250.76/250.72 cnf(582,plain,
% 250.76/250.72 (P1(f2(f2(f2(f2(f2(x5821,x5822),x5823),f2(x5824,x5823)),x5825),f2(f2(x5821,f1(x5824)),x5825)))),
% 250.76/250.72 inference(scs_inference,[],[333,396,5])).
% 250.76/250.72 cnf(587,plain,
% 250.76/250.72 (~P1(f2(f2(f1(f2(a4,a3)),x5871),f1(a5)))),
% 250.76/250.72 inference(scs_inference,[],[576,489,5])).
% 250.76/250.72 cnf(591,plain,
% 250.76/250.72 (P1(f2(f2(x5911,x5912),f2(f2(f2(f1(x5912),x5913),x5914),f2(x5911,x5914))))),
% 250.76/250.72 inference(scs_inference,[],[579,196,5,30])).
% 250.76/250.72 cnf(594,plain,
% 250.76/250.72 (P1(f2(f2(f2(f1(x5941),x5942),f1(x5943)),f2(f2(x5944,x5941),f2(x5943,f2(x5944,x5945)))))),
% 250.76/250.72 inference(scs_inference,[],[582,579,5])).
% 250.76/250.72 cnf(598,plain,
% 250.76/250.72 (P1(f2(f2(x5981,f2(f1(f1(x5982)),f1(x5982))),f2(x5982,f2(x5981,x5983))))),
% 250.76/250.72 inference(scs_inference,[],[594,80,5])).
% 250.76/250.72 cnf(604,plain,
% 250.76/250.72 (~P1(f2(f2(f2(f2(f1(f2(a4,a3)),x6041),x6042),f2(x6043,x6042)),f1(a5)))),
% 250.76/250.72 inference(scs_inference,[],[587,582,5])).
% 250.76/250.72 cnf(608,plain,
% 250.76/250.72 (P1(f2(f2(f2(x6081,f2(f1(x6082),x6083)),x6084),f2(x6082,x6084)))),
% 250.76/250.72 inference(scs_inference,[],[396,598,5])).
% 250.76/250.72 cnf(622,plain,
% 250.76/250.72 (P1(f2(x6221,f2(f2(f2(f1(f2(x6222,x6222)),x6223),x6224),f2(x6225,x6224))))),
% 250.76/250.72 inference(scs_inference,[],[489,538,5])).
% 250.76/250.72 cnf(626,plain,
% 250.76/250.72 (P1(f2(f2(x6261,x6262),f2(x6263,f2(x6261,x6262))))),
% 250.76/250.72 inference(scs_inference,[],[518,538,5])).
% 250.76/250.72 cnf(633,plain,
% 250.76/250.72 (P1(f2(f2(x6331,x6332),f2(x6333,f2(f2(f1(f2(x6332,x6334)),f2(x6332,x6334)),f2(x6331,x6334)))))),
% 250.76/250.72 inference(scs_inference,[],[518,626,5])).
% 250.76/250.72 cnf(638,plain,
% 250.76/250.72 (~P1(f2(f2(f2(f2(f1(x6381),x6382),x6383),f2(x6381,x6383)),f1(a5)))),
% 250.76/250.72 inference(scs_inference,[],[604,572,5])).
% 250.76/250.72 cnf(641,plain,
% 250.76/250.72 (P1(f2(f2(f2(f2(f2(f1(f2(x6411,x6411)),x6412),x6413),f2(x6414,x6413)),x6415),f2(x6416,x6415)))),
% 250.76/250.72 inference(scs_inference,[],[622,315,5])).
% 250.76/250.72 cnf(656,plain,
% 250.76/250.72 (P1(f2(f2(f2(f1(x6561),x6562),x6563),f2(f1(f2(x6561,x6563)),x6564)))),
% 250.76/250.72 inference(scs_inference,[],[551,88,5])).
% 250.76/250.72 cnf(660,plain,
% 250.76/250.72 (P1(f2(f1(f2(x6601,f2(f1(x6601),x6602))),x6603))),
% 250.76/250.72 inference(scs_inference,[],[656,196,5,30])).
% 250.76/250.72 cnf(665,plain,
% 250.76/250.72 (P1(f2(f2(x6651,x6652),f2(x6653,f2(f2(f2(f1(x6654),x6655),x6656),f2(x6654,x6656)))))),
% 250.76/250.72 inference(scs_inference,[],[572,626,5])).
% 250.76/250.72 cnf(673,plain,
% 250.76/250.72 (P1(f2(x6731,f2(x6732,f2(f2(f2(f1(x6733),x6734),x6735),f2(x6733,x6735)))))),
% 250.76/250.72 inference(scs_inference,[],[665,641,5])).
% 250.76/250.72 cnf(677,plain,
% 250.76/250.72 (P1(f2(f2(x6771,x6772),f2(f2(x6773,x6774),f2(f2(x6774,x6775),f2(x6773,x6775)))))),
% 250.76/250.72 inference(scs_inference,[],[572,518,5])).
% 250.76/250.72 cnf(681,plain,
% 250.76/250.72 (~P1(f2(a5,f2(f2(a4,a3),a3)))),
% 250.76/250.72 inference(scs_inference,[],[576,626,5])).
% 250.76/250.72 cnf(684,plain,
% 250.76/250.72 (~P1(f2(f2(f2(x6841,x6842),f2(x6843,f2(x6841,x6842))),f2(a5,f2(f2(a4,a3),a3))))),
% 250.76/250.72 inference(scs_inference,[],[681,626,5])).
% 250.76/250.72 cnf(686,plain,
% 250.76/250.72 (~P1(f2(f2(f1(f2(x6861,f2(a4,a3))),x6862),f1(a5)))),
% 250.76/250.72 inference(scs_inference,[],[684,594,5])).
% 250.76/250.72 cnf(690,plain,
% 250.76/250.72 (P1(f2(x6901,f2(f2(x6902,x6903),f2(f2(x6903,x6904),f2(x6902,x6904)))))),
% 250.76/250.72 inference(scs_inference,[],[677,641,5])).
% 250.76/250.72 cnf(705,plain,
% 250.76/250.72 (~P1(f2(f1(f2(f2(x7051,f2(a4,a3)),f1(a5))),f2(f2(x7051,f2(a4,a3)),f1(a5))))),
% 250.76/250.72 inference(scs_inference,[],[686,205,5])).
% 250.76/250.72 cnf(710,plain,
% 250.76/250.72 (P1(f2(f1(x7101),f2(x7101,f2(x7102,x7103))))),
% 250.76/250.72 inference(scs_inference,[],[608,598,5])).
% 250.76/250.72 cnf(714,plain,
% 250.76/250.72 (~P1(f2(f2(x7141,f2(a4,a3)),f1(a5)))),
% 250.76/250.72 inference(scs_inference,[],[705,1,5])).
% 250.76/250.72 cnf(719,plain,
% 250.76/250.72 (P1(f2(f2(f2(x7191,f2(x7192,x7193)),x7194),f2(f2(f1(f1(x7191)),f1(x7191)),x7194)))),
% 250.76/250.72 inference(scs_inference,[],[710,108,5])).
% 250.76/250.72 cnf(724,plain,
% 250.76/250.72 (P1(f2(f2(f1(f1(x7241)),f1(x7241)),f2(x7242,f2(x7241,f2(x7243,x7244)))))),
% 250.76/250.72 inference(scs_inference,[],[626,719,5])).
% 250.76/250.72 cnf(728,plain,
% 250.76/250.72 (~P1(f2(f1(f1(a5)),f1(a5)))),
% 250.76/250.72 inference(scs_inference,[],[724,684,5])).
% 250.76/250.72 cnf(731,plain,
% 250.76/250.72 (~P1(f2(f1(f2(f1(f1(a5)),f1(a5))),f2(f1(f1(a5)),f1(a5))))),
% 250.76/250.72 inference(scs_inference,[],[724,684,5,28])).
% 250.76/250.72 cnf(733,plain,
% 250.76/250.72 (~P1(f2(f2(f2(x7331,x7332),f2(x7333,f2(x7331,x7332))),f2(f1(f1(a5)),f1(a5))))),
% 250.76/250.72 inference(scs_inference,[],[626,728,5])).
% 250.76/250.72 cnf(735,plain,
% 250.76/250.72 (~P1(f2(f1(f2(f1(f2(f1(f1(a5)),f1(a5))),f2(f1(f1(a5)),f1(a5)))),f2(f1(f2(f1(f1(a5)),f1(a5))),f2(f1(f1(a5)),f1(a5)))))),
% 250.76/250.72 inference(scs_inference,[],[731,12,28])).
% 250.76/250.72 cnf(736,plain,
% 250.76/250.72 (P1(f2(x7361,f2(x7362,f2(f2(x7363,x7364),f2(f2(x7364,x7365),f2(x7363,x7365))))))),
% 250.76/250.72 inference(scs_inference,[],[626,690,5])).
% 250.76/250.72 cnf(740,plain,
% 250.76/250.72 (~P1(f2(f2(f1(f1(f1(a5))),x7401),f1(a5)))),
% 250.76/250.72 inference(scs_inference,[],[731,656,5])).
% 250.76/250.72 cnf(745,plain,
% 250.76/250.72 (P1(f2(x7451,f2(f1(x7452),f2(x7452,f2(x7453,x7454)))))),
% 250.76/250.72 inference(scs_inference,[],[626,710,5])).
% 250.76/250.72 cnf(748,plain,
% 250.76/250.72 (P1(f2(f2(f2(x7481,f2(x7482,x7483)),x7484),f2(f1(x7481),x7484)))),
% 250.76/250.72 inference(scs_inference,[],[626,710,5,20])).
% 250.76/250.72 cnf(750,plain,
% 250.76/250.73 (P1(f2(f1(f2(f1(x7501),f2(x7501,f2(x7502,x7503)))),x7504))),
% 250.76/250.73 inference(scs_inference,[],[626,710,5,20,12])).
% 250.76/250.73 cnf(752,plain,
% 250.76/250.73 (~P1(f2(f2(f1(a5),f2(x7521,x7522)),f1(a5)))),
% 250.76/250.73 inference(scs_inference,[],[748,728,5])).
% 250.76/250.73 cnf(760,plain,
% 250.76/250.73 (P1(f2(f2(x7601,f1(f2(x7602,f2(x7603,x7604)))),f2(f1(x7602),f2(x7601,x7605))))),
% 250.76/250.73 inference(scs_inference,[],[745,521,5])).
% 250.76/250.73 cnf(764,plain,
% 250.76/250.73 (~P1(f2(f2(f2(x7641,x7642),f2(x7643,f2(x7641,x7642))),f2(f2(f1(a5),f2(x7644,x7645)),f1(a5))))),
% 250.76/250.73 inference(scs_inference,[],[626,752,5])).
% 250.76/250.73 cnf(768,plain,
% 250.76/250.73 (P1(f2(x7681,f2(f2(f1(f2(x7682,x7683)),f2(x7682,x7683)),f2(x7682,x7683))))),
% 250.76/250.73 inference(scs_inference,[],[633,88,5])).
% 250.76/250.73 cnf(777,plain,
% 250.76/250.73 (~P1(f2(f2(f2(f1(f1(a5)),f1(a5)),f2(x7771,x7772)),f2(f1(f1(a5)),f1(a5))))),
% 250.76/250.73 inference(scs_inference,[],[748,731,5])).
% 250.76/250.73 cnf(781,plain,
% 250.76/250.73 (P1(f2(f2(f2(f2(f1(f2(x7811,x7812)),f2(x7811,x7812)),f2(x7811,x7812)),x7813),f2(x7814,x7813)))),
% 250.76/250.73 inference(scs_inference,[],[768,315,5])).
% 250.76/250.73 cnf(785,plain,
% 250.76/250.73 (~P1(f2(f2(f1(f2(x7851,x7851)),x7852),f2(f2(f2(f2(f1(x7853),x7854),x7855),f2(x7853,x7855)),f1(a5))))),
% 250.76/250.73 inference(scs_inference,[],[638,192,5])).
% 250.76/250.73 cnf(787,plain,
% 250.76/250.73 (~P1(f2(f2(f2(f1(f2(x7871,x7872)),f2(x7871,x7872)),f2(x7871,x7872)),f1(a5)))),
% 250.76/250.73 inference(scs_inference,[],[638,781,5])).
% 250.76/250.73 cnf(849,plain,
% 250.76/250.73 (~P1(f2(f2(f1(x8491),f2(x8491,f2(x8492,x8493))),f2(a5,f2(f2(a4,a3),a3))))),
% 250.76/250.73 inference(scs_inference,[],[681,710,5])).
% 250.76/250.73 cnf(858,plain,
% 250.76/250.73 (~P1(f2(f2(f1(f2(x8581,x8581)),x8582),f2(a5,f2(f2(a4,a3),a3))))),
% 250.76/250.73 inference(scs_inference,[],[681,192,5])).
% 250.76/250.73 cnf(863,plain,
% 250.76/250.73 (P1(f2(f2(f1(f1(x8631)),f1(x8631)),f2(x8631,f2(x8632,x8633))))),
% 250.76/250.73 inference(scs_inference,[],[745,205,5])).
% 250.76/250.73 cnf(905,plain,
% 250.76/250.73 (~P1(f2(f2(f1(x9051),f2(x9051,f2(x9052,x9053))),f2(f1(f1(a5)),f1(a5))))),
% 250.76/250.73 inference(scs_inference,[],[710,728,5])).
% 250.76/250.73 cnf(920,plain,
% 250.76/250.73 (~P1(f2(f2(x9201,x9201),f2(f2(f2(x9202,x9203),f2(x9204,f2(x9202,x9203))),f2(f1(f1(a5)),f1(a5)))))),
% 250.76/250.73 inference(scs_inference,[],[733,88,5])).
% 250.76/250.73 cnf(927,plain,
% 250.76/250.73 (~P1(f2(f2(f2(f2(x9271,f2(a4,a3)),f1(a5)),f2(x9272,x9273)),f2(f2(x9271,f2(a4,a3)),f1(a5))))),
% 250.76/250.73 inference(scs_inference,[],[748,705,5])).
% 250.76/250.73 cnf(935,plain,
% 250.76/250.73 (~P1(f2(f2(f2(x9351,x9352),f2(x9353,f2(x9351,x9352))),f1(a5)))),
% 250.76/250.73 inference(scs_inference,[],[920,591,5])).
% 250.76/250.73 cnf(947,plain,
% 250.76/250.73 (P1(f2(f1(x9471),f2(f1(f2(x9471,f2(x9472,x9473))),x9474)))),
% 250.76/250.73 inference(scs_inference,[],[760,88,5])).
% 250.76/250.73 cnf(951,plain,
% 250.76/250.73 (~P1(f2(f2(f2(f1(f2(x9511,x9512)),f2(x9511,x9512)),f2(x9513,f2(x9511,x9512))),f1(a5)))),
% 250.76/250.73 inference(scs_inference,[],[935,103,5])).
% 250.76/250.73 cnf(956,plain,
% 250.76/250.73 (P1(f2(f1(f2(x9561,f2(x9562,x9563))),x9564))+~P1(f1(x9561))),
% 250.76/250.73 inference(scs_inference,[],[947,5])).
% 250.76/250.73 cnf(958,plain,
% 250.76/250.73 (P1(f2(f2(f2(f2(x9581,x9582),x9583),x9584),f2(f2(f2(x9585,x9582),x9583),x9584)))+~P1(f1(f1(f2(x9585,x9581))))),
% 250.76/250.73 inference(scs_inference,[],[947,5,107])).
% 250.76/250.73 cnf(968,plain,
% 250.76/250.73 (~P1(f2(f2(x9681,x9681),f2(f2(f2(f1(f1(a5)),f1(a5)),f2(x9682,x9683)),f2(f1(f1(a5)),f1(a5)))))),
% 250.76/250.73 inference(scs_inference,[],[777,88,5])).
% 250.76/250.73 cnf(971,plain,
% 250.76/250.73 (~P1(f2(f2(f2(f1(f2(x9711,x9712)),f2(x9711,x9712)),f2(x9711,x9712)),f2(f1(f1(a5)),f1(a5))))),
% 250.76/250.73 inference(scs_inference,[],[781,905,5])).
% 250.76/250.73 cnf(975,plain,
% 250.76/250.73 (P1(f2(f2(f1(f2(x9751,x9752)),f1(x9753)),f2(x9754,f2(x9753,f2(x9751,x9752)))))),
% 250.76/250.73 inference(scs_inference,[],[781,582,5])).
% 250.76/250.73 cnf(983,plain,
% 250.76/250.73 (~P1(f2(f2(f2(f1(f2(x9831,x9832)),f2(x9831,x9832)),f2(x9831,x9832)),f2(f2(x9833,f2(a4,a3)),f1(a5))))),
% 250.76/250.73 inference(scs_inference,[],[781,927,5])).
% 250.76/250.73 cnf(987,plain,
% 250.76/250.73 (P1(f2(x9871,f2(x9872,f2(f1(x9873),f2(x9873,f2(x9874,x9875))))))),
% 250.76/250.73 inference(scs_inference,[],[975,750,5])).
% 250.76/250.73 cnf(991,plain,
% 250.76/250.73 (P1(f2(f2(f2(f1(x9911),f2(x9911,f2(x9912,x9913))),x9914),f2(x9915,x9914)))),
% 250.76/250.73 inference(scs_inference,[],[975,750,5,20])).
% 250.76/250.73 cnf(994,plain,
% 250.76/250.73 (~P1(f2(f2(x9941,x9941),f2(f2(f2(f1(f2(x9942,x9943)),f2(x9942,x9943)),f2(x9944,f2(x9942,x9943))),f1(a5))))),
% 250.76/250.73 inference(scs_inference,[],[951,88,5])).
% 250.76/250.73 cnf(997,plain,
% 250.76/250.73 (~P1(f2(f2(f2(f1(f2(x9971,x9972)),f2(x9971,x9972)),f2(x9971,x9972)),f2(f2(f1(a5),f2(x9973,x9974)),f1(a5))))),
% 250.76/250.73 inference(scs_inference,[],[781,764,5])).
% 250.76/250.73 cnf(1001,plain,
% 250.76/250.73 (P1(f2(x10011,f2(x10012,f2(x10013,f2(f1(x10013),x10014)))))),
% 250.76/250.73 inference(scs_inference,[],[975,660,5])).
% 250.76/250.73 cnf(1005,plain,
% 250.76/250.73 (P1(f2(f2(f2(x10051,f2(f1(x10051),x10052)),x10053),f2(x10054,x10053)))),
% 250.76/250.73 inference(scs_inference,[],[975,660,5,20])).
% 250.76/250.73 cnf(1020,plain,
% 250.76/250.73 (~P1(f2(f2(f1(f2(x10201,x10201)),x10202),f2(f2(f2(f1(f2(x10203,x10204)),f2(x10203,x10204)),f2(x10203,x10204)),f1(a5))))),
% 250.76/250.73 inference(scs_inference,[],[787,192,5])).
% 250.76/250.73 cnf(1023,plain,
% 250.76/250.73 (~P1(f2(f2(x10231,f2(f1(x10231),x10232)),f1(a5)))),
% 250.76/250.73 inference(scs_inference,[],[787,1005,5])).
% 250.76/250.73 cnf(1036,plain,
% 250.76/250.73 (~P1(f2(f2(f1(x10361),f2(x10361,f2(x10362,x10363))),f1(a5)))),
% 250.76/250.73 inference(scs_inference,[],[1023,991,5])).
% 250.76/250.73 cnf(1044,plain,
% 250.76/250.73 (~P1(f2(f1(f2(f2(a4,a3),a3)),f1(a5)))),
% 250.76/250.73 inference(scs_inference,[],[849,975,5])).
% 250.76/250.73 cnf(1048,plain,
% 250.76/250.73 (~P1(f2(f2(f1(f2(x10481,x10481)),x10482),f2(f1(f2(f2(a4,a3),a3)),f1(a5))))),
% 250.76/250.73 inference(scs_inference,[],[1044,192,5])).
% 250.76/250.73 cnf(1054,plain,
% 250.76/250.73 (~P1(f2(f2(f2(x10541,x10542),f2(x10541,x10542)),f2(f2(x10543,f2(a4,a3)),f1(a5))))),
% 250.76/250.73 inference(scs_inference,[],[1001,983,94,5])).
% 250.76/250.73 cnf(1074,plain,
% 250.76/250.73 (~P1(f2(f2(x10741,x10741),f2(f2(f2(x10742,x10743),f2(x10742,x10743)),f2(f2(x10744,f2(a4,a3)),f1(a5)))))),
% 250.76/250.73 inference(scs_inference,[],[1054,88,5])).
% 250.76/250.73 cnf(1174,plain,
% 250.76/250.73 (~P1(f2(f2(x11741,x11741),f2(f2(f1(x11742),f2(x11742,f2(x11743,x11744))),f2(f1(f1(a5)),f1(a5)))))),
% 250.76/250.73 inference(scs_inference,[],[905,88,5])).
% 250.76/250.73 cnf(1176,plain,
% 250.76/250.73 (~P1(f2(f2(f1(f1(f2(x11761,x11762))),f2(x11761,x11762)),f2(f2(f1(a5),f2(x11763,x11764)),f1(a5))))),
% 250.76/250.73 inference(scs_inference,[],[987,997,94,5])).
% 250.76/250.73 cnf(1211,plain,
% 250.76/250.73 (~P1(f2(f2(f1(a5),f2(x12111,x12112)),f1(f2(x12113,x12113))))),
% 250.76/250.73 inference(scs_inference,[],[1176,524,5])).
% 250.76/250.73 cnf(1219,plain,
% 250.76/250.73 (~P1(f2(f2(f1(f2(x12191,x12191)),x12192),f2(f2(f1(a5),f2(x12193,x12194)),f1(f2(x12195,x12195)))))),
% 250.76/250.73 inference(scs_inference,[],[1211,192,5])).
% 250.76/250.73 cnf(1230,plain,
% 250.76/250.73 (~P1(f2(f2(x12301,x12301),f2(f2(f2(f1(f2(x12302,x12303)),f2(x12302,x12303)),f2(x12302,x12303)),f2(f1(f1(a5)),f1(a5)))))),
% 250.76/250.73 inference(scs_inference,[],[971,88,5])).
% 250.76/250.73 cnf(1241,plain,
% 250.76/250.73 (P1(f2(x12411,f2(x12412,f2(f2(f1(x12413),x12413),x12413))))),
% 250.76/250.73 inference(scs_inference,[],[975,91,5])).
% 250.76/250.73 cnf(1246,plain,
% 250.76/250.73 (P1(f2(x12461,f2(f2(f1(x12462),x12462),x12462)))),
% 250.76/250.73 inference(scs_inference,[],[1241,457,5])).
% 250.76/250.73 cnf(1249,plain,
% 250.76/250.73 (~P1(f2(f2(x12491,f2(f2(f1(x12492),x12492),x12492)),f2(f2(f1(a5),f2(x12493,x12494)),f1(a5))))),
% 250.76/250.73 inference(scs_inference,[],[1246,752,5])).
% 250.76/250.73 cnf(1252,plain,
% 250.76/250.73 (P1(f2(f2(f2(f2(f1(x12521),x12521),x12521),x12522),f2(x12523,x12522)))),
% 250.76/250.73 inference(scs_inference,[],[1241,17,5])).
% 250.76/250.73 cnf(1296,plain,
% 250.76/250.73 (~P1(f1(f1(f2(x12961,x12962))))+P1(f2(f2(f2(x12961,f2(f1(x12962),x12963)),x12964),f2(x12965,x12964)))),
% 250.76/250.73 inference(scs_inference,[],[1005,5,958])).
% 250.76/250.73 cnf(1366,plain,
% 250.76/250.73 (~P1(f2(f2(f1(f2(x13661,x13661)),x13662),f2(f2(f1(x13663),f2(x13663,f2(x13664,x13665))),f1(a5))))),
% 250.76/250.73 inference(scs_inference,[],[1036,192,5])).
% 250.76/250.73 cnf(1442,plain,
% 250.76/250.73 (~P1(f1(f1(f2(x14421,x14422))))+P1(f2(f2(x14422,x14423),f2(f2(x14423,x14424),f2(x14421,x14424))))),
% 250.76/250.73 inference(scs_inference,[],[116,956])).
% 250.76/250.73 cnf(1544,plain,
% 250.76/250.73 (~P1(f2(f1(f2(f2(f2(f1(f2(x15441,x15442)),f2(x15441,x15442)),f2(x15443,f2(x15441,x15442))),f1(a5))),f2(f2(f2(f1(f2(x15441,x15442)),f2(x15441,x15442)),f2(x15443,f2(x15441,x15442))),f1(a5))))),
% 250.76/250.73 inference(scs_inference,[],[994,20])).
% 250.76/250.73 cnf(1559,plain,
% 250.76/250.73 (P1(f2(f2(f1(f2(f2(x15591,f2(x15592,x15593)),x15594)),f2(f2(x15591,f2(x15592,x15593)),x15594)),f2(f2(x15592,x15593),x15594)))),
% 250.76/250.73 inference(scs_inference,[],[156,626,1074,20,5,144])).
% 250.76/250.73 cnf(1574,plain,
% 250.76/250.73 (P1(f2(x15741,f2(f1(f2(f2(x15742,f1(x15743)),f2(x15743,f2(x15742,x15744)))),x15745)))),
% 250.76/250.73 inference(scs_inference,[],[156,160,5])).
% 250.76/250.73 cnf(1584,plain,
% 250.76/250.73 (P1(f2(x15841,f2(f1(f2(f1(f2(x15842,x15842)),x15843)),x15844)))),
% 250.76/250.73 inference(scs_inference,[],[156,192,5])).
% 250.76/250.73 cnf(1588,plain,
% 250.76/250.73 (P1(f2(x15881,f2(f1(f2(f2(f1(x15882),x15882),f2(f1(x15882),x15883))),x15884)))),
% 250.76/250.73 inference(scs_inference,[],[156,9,5])).
% 250.76/250.73 cnf(1591,plain,
% 250.76/250.73 (P1(f2(x15911,f2(f1(f2(f2(f1(f1(x15912)),f1(x15912)),f2(x15912,f2(x15913,x15914)))),x15915)))),
% 250.76/250.73 inference(scs_inference,[],[156,863,5])).
% 250.76/250.73 cnf(1778,plain,
% 250.76/250.73 (P1(f2(f2(f2(x17781,f2(f1(x17782),x17783)),x17784),f2(x17785,x17784)))+~P1(f2(f2(x17786,f2(f1(x17786),x17787)),f1(f1(f2(x17781,x17782)))))),
% 250.76/250.73 inference(scs_inference,[],[1,1296,5])).
% 250.76/250.73 cnf(1914,plain,
% 250.76/250.73 (P1(f2(x19141,f2(f1(f2(x19142,f2(f1(x19143),x19144))),x19145)))+~P1(f2(f2(x19146,f2(f1(x19146),x19147)),f1(f1(f2(x19142,x19143)))))),
% 250.76/250.73 inference(scs_inference,[],[1,1778,5])).
% 250.76/250.73 cnf(1917,plain,
% 250.76/250.73 (P1(f2(x19171,f2(f1(f2(x19172,f2(f1(x19173),x19174))),x19175)))+~P1(f2(f2(x19176,f2(f1(x19176),x19177)),f2(f2(x19178,f2(f1(x19178),x19179)),f1(f1(f2(x19172,x19173))))))),
% 250.76/250.73 inference(scs_inference,[],[1,1914,5])).
% 250.76/250.73 cnf(1920,plain,
% 250.76/250.73 (P1(f2(x19201,f2(f1(f2(x19202,f2(f1(x19203),x19204))),x19205)))+~P1(f2(f2(f2(f2(f1(x19206),x19207),x19208),f2(x19206,x19208)),f2(f2(x19209,f2(f1(x19209),x192010)),f1(f1(f2(x19202,x19203))))))),
% 250.76/250.73 inference(scs_inference,[],[14,1914,5])).
% 250.76/250.73 cnf(1923,plain,
% 250.76/250.73 (P1(f2(x19231,f2(f1(f2(x19232,f2(f1(x19233),x19234))),x19235)))+~P1(f2(f2(x19236,f2(x19237,f2(f1(x19236),x19238))),f2(f2(x19239,f2(f1(x19239),x192310)),f1(f1(f2(x19232,x19233))))))),
% 250.76/250.73 inference(scs_inference,[],[156,1914,5])).
% 250.76/250.73 cnf(2084,plain,
% 250.76/250.73 (P1(f2(f1(f2(x20841,f2(f1(x20842),x20843))),x20844))+~P1(f2(f2(x20845,f2(f1(x20845),x20846)),f2(f2(x20847,f2(f1(x20847),x20848)),f1(f1(f2(x20841,x20842))))))),
% 250.76/250.73 inference(scs_inference,[],[40,1917,5])).
% 250.76/250.73 cnf(2372,plain,
% 250.76/250.73 (~P1(f2(f2(f2(f1(x23721),x23721),x23721),f2(f2(x23722,f2(f1(x23722),x23723)),f1(f2(x23724,x23724)))))),
% 250.76/250.73 inference(scs_inference,[],[214,2,5])).
% 250.76/250.73 cnf(2439,plain,
% 250.76/250.73 (~P1(f2(f2(f2(f1(x24391),x24391),x24391),f2(f2(f1(f2(x24392,x24392)),x24393),f1(f2(x24394,x24394)))))),
% 250.76/250.73 inference(scs_inference,[],[270,2,5])).
% 250.76/250.73 cnf(2444,plain,
% 250.76/250.73 (~P1(f2(f2(f1(f2(x24441,x24441)),x24442),f2(f2(f1(f2(x24443,x24443)),x24444),f1(f2(x24445,x24445)))))),
% 250.76/250.73 inference(scs_inference,[],[270,192,5])).
% 250.76/250.73 cnf(2454,plain,
% 250.76/250.73 (P1(f2(f2(x24541,x24542),f2(f2(x24542,x24543),f2(x24544,x24543))))+~P1(f2(f2(x24545,f2(x24546,f2(f1(x24545),x24547))),f1(f1(f2(x24544,x24541)))))),
% 250.76/250.73 inference(scs_inference,[],[156,1442,5])).
% 250.76/250.73 cnf(2511,plain,
% 250.76/250.73 (~P1(f2(f2(f2(f1(x25111),x25111),x25111),f2(f2(x25112,f2(a4,a3)),f1(a5))))),
% 250.76/250.73 inference(scs_inference,[],[2,714,5])).
% 250.76/250.73 cnf(2513,plain,
% 250.76/250.73 (~P1(f2(f2(f2(f1(x25131),x25131),x25131),f2(f2(f1(a5),f2(x25132,x25133)),f1(a5))))),
% 250.76/250.73 inference(scs_inference,[],[2,752,5])).
% 250.76/250.73 cnf(2515,plain,
% 250.76/250.73 (~P1(f2(f2(f2(f1(x25151),x25151),x25151),f2(f1(f1(a5)),f1(a5))))),
% 250.76/250.73 inference(scs_inference,[],[2,728,5])).
% 250.76/250.73 cnf(2524,plain,
% 250.76/250.73 (~P1(f2(f2(f2(x25241,x25242),f2(x25241,x25242)),f2(f2(f2(f1(x25243),x25243),x25243),f2(f1(f1(a5)),f1(a5)))))),
% 250.76/250.73 inference(scs_inference,[],[189,2515,30,5])).
% 250.76/250.73 cnf(2530,plain,
% 250.76/250.73 (P1(f2(f2(f2(f2(x25301,x25302),f2(f2(x25302,x25303),f2(x25301,x25303))),x25304),f2(x25305,x25304)))),
% 250.76/250.73 inference(scs_inference,[],[736,20])).
% 250.76/250.73 cnf(2557,plain,
% 250.76/250.73 (~P1(f2(f2(x25571,f2(f1(x25571),x25572)),f2(f2(f2(f1(x25573),x25573),x25573),f2(f2(x25574,f2(a4,a3)),f1(a5)))))),
% 250.76/250.73 inference(scs_inference,[],[1,2511,5])).
% 250.76/250.73 cnf(2563,plain,
% 250.76/250.73 (~P1(f2(f2(x25631,f2(f1(x25631),x25632)),f2(f2(f2(f1(x25633),x25633),x25633),f2(f2(f1(a5),f2(x25634,x25635)),f1(a5)))))),
% 250.76/250.73 inference(scs_inference,[],[1,2513,5])).
% 250.76/250.73 cnf(2605,plain,
% 250.76/250.73 (~P1(f2(f2(x26051,f2(f1(x26051),x26052)),f2(f2(f2(f1(x26053),x26053),x26053),f2(f1(f1(a5)),f1(a5)))))),
% 250.76/250.73 inference(scs_inference,[],[1,2515,5])).
% 250.76/250.73 cnf(2767,plain,
% 250.76/250.73 (~P1(f2(f2(x27671,f2(f1(x27671),x27672)),f2(f2(f1(f1(f1(a5))),x27673),f1(a5))))),
% 250.76/250.73 inference(scs_inference,[],[1,740,5])).
% 250.76/250.73 cnf(2813,plain,
% 250.76/250.73 (~P1(f2(f1(f2(f2(f1(a3),a4),f1(a5))),f2(f2(f1(a3),a4),f1(a5))))),
% 250.76/250.73 inference(scs_inference,[],[710,4,5,20])).
% 250.76/250.73 cnf(2821,plain,
% 250.76/250.73 (~P1(f2(f2(f1(f2(x28211,x28211)),x28212),f2(f2(f1(a3),a4),f2(a5,f2(f2(a4,a3),a3)))))),
% 250.76/250.73 inference(scs_inference,[],[4,192,5])).
% 250.76/250.73 cnf(2829,plain,
% 250.76/250.73 (P1(f2(x28291,f2(f2(x28292,x28293),f2(f2(f2(x28292,x28294),x28295),f2(f2(x28293,x28294),x28295)))))),
% 250.76/250.73 inference(scs_inference,[],[2530,736,5,30])).
% 250.76/250.73 cnf(2840,plain,
% 250.76/250.73 (~P1(f2(f1(f2(f1(f2(f2(f1(x28401),f2(x28401,f2(x28402,x28403))),f2(f1(f1(a5)),f1(a5)))),f2(f2(f1(x28401),f2(x28401,f2(x28402,x28403))),f2(f1(f1(a5)),f1(a5))))),f2(f1(f2(f2(f1(x28401),f2(x28401,f2(x28402,x28403))),f2(f1(f1(a5)),f1(a5)))),f2(f2(f1(x28401),f2(x28401,f2(x28402,x28403))),f2(f1(f1(a5)),f1(a5))))))),
% 250.76/250.73 inference(scs_inference,[],[64,1174,5,30])).
% 250.76/250.73 cnf(2843,plain,
% 250.76/250.73 (~P1(f2(f1(f2(f1(f2(f2(x28431,f2(f1(x28431),x28432)),f2(f1(f1(a5)),f1(a5)))),f2(f2(x28431,f2(f1(x28431),x28432)),f2(f1(f1(a5)),f1(a5))))),f2(f1(f2(f2(x28431,f2(f1(x28431),x28432)),f2(f1(f1(a5)),f1(a5)))),f2(f2(x28431,f2(f1(x28431),x28432)),f2(f1(f1(a5)),f1(a5))))))),
% 250.76/250.73 inference(scs_inference,[],[83,2767,5,30])).
% 250.76/250.73 cnf(3096,plain,
% 250.76/250.73 (~P1(f2(f1(f2(f1(f2(f1(f2(f1(f1(a5)),f1(a5))),f1(a5))),f2(f1(f2(f1(f1(a5)),f1(a5))),f1(a5)))),f2(f1(f2(f1(f2(f1(f1(a5)),f1(a5))),f1(a5))),f2(f1(f2(f1(f1(a5)),f1(a5))),f1(a5)))))),
% 250.76/250.73 inference(scs_inference,[],[1,731,5,30])).
% 250.76/250.73 cnf(3129,plain,
% 250.76/250.73 (~P1(f2(f2(f1(f2(x31291,x31291)),x31292),f2(f1(f2(f2(a4,a3),a3)),f1(a5))))),
% 250.76/250.73 inference(rename_variables,[],[1048])).
% 250.76/250.73 cnf(3137,plain,
% 250.76/250.73 (~P1(f2(f1(f2(f1(f2(f1(f1(a5)),f2(f1(f1(a5)),f1(a5)))),f2(f1(f1(a5)),f2(f1(f1(a5)),f1(a5))))),f2(f1(f2(f1(f1(a5)),f2(f1(f1(a5)),f1(a5)))),f2(f1(f1(a5)),f2(f1(f1(a5)),f1(a5))))))),
% 250.76/250.73 inference(scs_inference,[],[673,358,2524,1048,372,2843,1923,1920,1917,1914,72,49,182,30,116])).
% 250.76/250.73 cnf(3138,plain,
% 250.76/250.73 (~P1(f2(f2(f2(x31381,x31382),f2(x31381,x31382)),f2(f2(f2(f1(x31383),x31383),x31383),f2(f1(f1(a5)),f1(a5)))))),
% 250.76/250.73 inference(rename_variables,[],[2524])).
% 250.76/250.73 cnf(3146,plain,
% 250.76/250.73 (~P1(f2(f1(f2(f1(f2(f2(f2(x31461,x31462),f2(x31463,f2(x31461,x31462))),f2(f1(f1(a5)),f1(a5)))),f2(f2(f2(x31461,x31462),f2(x31463,f2(x31461,x31462))),f2(f1(f1(a5)),f1(a5))))),f2(f1(f2(f2(f2(x31461,x31462),f2(x31463,f2(x31461,x31462))),f2(f1(f1(a5)),f1(a5)))),f2(f2(f2(x31461,x31462),f2(x31463,f2(x31461,x31462))),f2(f1(f1(a5)),f1(a5))))))),
% 250.76/250.73 inference(scs_inference,[],[673,358,2524,3138,1048,920,2557,372,2843,1923,1920,1917,1914,72,49,182,30,116,2454,164,67])).
% 250.76/250.73 cnf(3149,plain,
% 250.76/250.73 (~P1(f2(f1(f2(f1(f2(f1(f1(f2(x31491,x31491))),f1(f2(x31492,x31492)))),f2(f1(f1(f2(x31491,x31491))),f1(f2(x31492,x31492))))),f2(f1(f2(f1(f1(f2(x31491,x31491))),f1(f2(x31492,x31492)))),f2(f1(f1(f2(x31491,x31491))),f1(f2(x31492,x31492))))))),
% 250.76/250.73 inference(scs_inference,[],[673,358,2524,3138,1048,920,2557,372,2439,2843,1923,1920,1917,1914,72,49,182,30,116,2454,164,67,94])).
% 250.76/250.73 cnf(3162,plain,
% 250.76/250.73 (~P1(f2(f1(f2(f1(f2(f1(f2(f2(a4,a3),a3)),f1(a5))),f2(f1(f2(f2(a4,a3),a3)),f1(a5)))),f2(f1(f2(f1(f2(f2(a4,a3),a3)),f1(a5))),f2(f1(f2(f2(a4,a3),a3)),f1(a5)))))),
% 250.76/250.73 inference(scs_inference,[],[673,736,358,2524,3138,858,705,1048,3129,920,2557,372,2439,3096,2843,1923,1920,1917,1914,72,49,182,30,116,2454,164,67,94,28,134,50,2084,144])).
% 250.76/250.73 cnf(3186,plain,
% 250.76/250.73 (P1(f2(x31861,f2(x31862,f2(f2(f1(x31863),x31863),x31863))))),
% 250.76/250.73 inference(rename_variables,[],[1241])).
% 250.76/250.73 cnf(3191,plain,
% 250.76/250.73 (~P1(f2(f2(f1(f2(x31911,x31911)),x31912),f2(f2(f2(f1(f2(x31913,x31914)),f2(x31913,x31914)),f2(x31913,x31914)),f1(a5))))),
% 250.76/250.73 inference(rename_variables,[],[1020])).
% 250.76/250.73 cnf(3202,plain,
% 250.76/250.73 (~P1(f2(f1(f2(f1(f2(f2(f2(f1(x32021),x32021),x32021),f2(f1(f1(a5)),f1(a5)))),f2(f2(f2(f1(x32021),x32021),x32021),f2(f1(f1(a5)),f1(a5))))),f2(f1(f2(f2(f2(f1(x32021),x32021),x32021),f2(f1(f1(a5)),f1(a5)))),f2(f2(f2(f1(x32021),x32021),x32021),f2(f1(f1(a5)),f1(a5))))))),
% 250.76/250.73 inference(scs_inference,[],[1241,3186,2524,2605,1020,3191,2563,1230,3162,3137,1917,1920,1923,164,116,134,2084,144,182,67,49,30])).
% 250.76/250.73 cnf(3207,plain,
% 250.76/250.73 (~P1(f2(f1(f2(f1(f2(f1(f2(f1(f1(a5)),f1(a5))),f2(f1(f1(a5)),f1(a5)))),f2(f1(f2(f1(f1(a5)),f1(a5))),f2(f1(f1(a5)),f1(a5))))),f2(f1(f2(f1(f2(f1(f1(a5)),f1(a5))),f2(f1(f1(a5)),f1(a5)))),f2(f1(f2(f1(f1(a5)),f1(a5))),f2(f1(f1(a5)),f1(a5))))))),
% 250.76/250.73 inference(scs_inference,[],[1241,3186,2524,2605,1020,3191,2563,1230,735,3162,3137,3146,1917,1920,1923,164,116,134,2084,144,182,67,49,30,1914,28])).
% 250.76/250.73 cnf(3232,plain,
% 250.76/250.73 (P1(f2(x32321,f2(f1(f2(f2(f1(f1(x32322)),f1(x32322)),f2(x32322,f2(x32323,x32324)))),x32325)))),
% 250.76/250.73 inference(rename_variables,[],[1591])).
% 250.76/250.73 cnf(3235,plain,
% 250.76/250.73 (~P1(f2(f2(f1(f2(x32351,x32351)),x32352),f2(f2(f2(f2(f1(x32353),x32354),x32355),f2(x32353,x32355)),f1(a5))))),
% 250.76/250.73 inference(rename_variables,[],[785])).
% 250.76/250.73 cnf(3237,plain,
% 250.76/250.73 (~P1(f2(f1(f2(f1(f2(f2(f2(f1(f1(a5)),f1(a5)),f2(x32371,x32372)),f2(f1(f1(a5)),f1(a5)))),f2(f2(f2(f1(f1(a5)),f1(a5)),f2(x32371,x32372)),f2(f1(f1(a5)),f1(a5))))),f2(f1(f2(f2(f2(f1(f1(a5)),f1(a5)),f2(x32371,x32372)),f2(f1(f1(a5)),f1(a5)))),f2(f2(f2(f1(f1(a5)),f1(a5)),f2(x32371,x32372)),f2(f1(f1(a5)),f1(a5))))))),
% 250.76/250.73 inference(scs_inference,[],[785,3137,1591,968,3146,1917,1920,1923,2084,134,144,67])).
% 250.76/250.73 cnf(3251,plain,
% 250.76/250.73 (~P1(f2(f1(f2(f2(x32511,f2(a4,a3)),f2(f1(f1(a5)),f1(a5)))),f2(f2(x32511,f2(a4,a3)),f2(f1(f1(a5)),f1(a5)))))),
% 250.76/250.73 inference(scs_inference,[],[2563,785,3235,3137,1591,3232,2511,968,3146,3202,1917,1920,1923,2084,134,144,67,182,164,1914,49,20])).
% 250.76/250.73 cnf(3256,plain,
% 250.76/250.73 (~P1(f2(f1(f2(f1(f2(f2(f2(f1(x32561),x32561),x32561),f1(a5))),f2(f2(f2(f1(x32561),x32561),x32561),f1(a5)))),f2(f1(f2(f2(f2(f1(x32561),x32561),x32561),f1(a5))),f2(f2(f2(f1(x32561),x32561),x32561),f1(a5)))))),
% 250.76/250.73 inference(scs_inference,[],[2605,2563,785,3235,3137,1591,3232,2511,968,3146,2813,3202,1917,1920,1923,2084,134,144,67,182,164,1914,49,20,28,30])).
% 250.76/250.73 cnf(3288,plain,
% 250.76/250.73 (~P1(f2(f1(f2(f1(f2(f2(x32881,f2(a4,a3)),f2(f1(f1(a5)),f1(a5)))),f2(f2(x32881,f2(a4,a3)),f2(f1(f1(a5)),f1(a5))))),f2(f1(f2(f2(x32881,f2(a4,a3)),f2(f1(f1(a5)),f1(a5)))),f2(f2(x32881,f2(a4,a3)),f2(f1(f1(a5)),f1(a5))))))),
% 250.76/250.73 inference(scs_inference,[],[2511,2557,1219,1588,1574,3202,1544,3251,2840,1917,1920,1923,144,2084,182,134,1914,164,28,30])).
% 250.76/250.73 cnf(3308,plain,
% 250.76/250.73 (~P1(f2(f1(f2(f1(f2(f2(f1(a5),f2(x33081,x33082)),f2(f1(f1(a5)),f1(a5)))),f2(f2(f1(a5),f2(x33081,x33082)),f2(f1(f1(a5)),f1(a5))))),f2(f1(f2(f2(f1(a5),f2(x33081,x33082)),f2(f1(f1(a5)),f1(a5)))),f2(f2(f1(a5),f2(x33081,x33082)),f2(f1(f1(a5)),f1(a5))))))),
% 250.76/250.74 inference(scs_inference,[],[2840,1249,3237,1917,1920,1923,144])).
% 250.76/250.74 cnf(3350,plain,
% 250.76/250.74 (~P1(f2(f1(f2(f2(x33501,f2(f1(x33501),x33502)),f2(f1(f1(f2(x33503,x33503))),f1(f2(x33503,x33503))))),f2(f2(x33501,f2(f1(x33501),x33502)),f2(f1(f1(f2(x33503,x33503))),f1(f2(x33503,x33503))))))),
% 250.76/250.74 inference(scs_inference,[],[2372,3237,1366,3308,3149,3207,1917,144,2084,1923,1920,1914,20])).
% 250.76/250.74 cnf(3420,plain,
% 250.76/250.74 (~P1(f2(f1(f2(f1(f2(f2(f1(a3),a4),f1(f2(x34201,x34201)))),f2(f2(f1(a3),a4),f1(f2(x34201,x34201))))),f2(f1(f2(f2(f1(a3),a4),f1(f2(x34201,x34201)))),f2(f2(f1(a3),a4),f1(f2(x34201,x34201))))))),
% 250.76/250.74 inference(scs_inference,[],[2444,2821,3288,3350,144,1920,2084,1923,49])).
% 250.76/250.74 cnf(3647,plain,
% 250.76/250.74 (~P1(f2(f1(f2(f2(x36471,f2(f1(a3),a4)),f2(a5,f2(f2(a4,a3),a3)))),f2(f2(x36471,f2(f1(a3),a4)),f2(a5,f2(f2(a4,a3),a3)))))),
% 250.76/250.74 inference(scs_inference,[],[4,3256,1559,493,1584,2444,12,47,956,20,5])).
% 250.76/250.74 cnf(3730,plain,
% 250.76/250.74 (P1(f2(f2(f2(f2(f2(x37301,x37302),x37303),f2(f2(x37304,x37302),x37303)),x37305),f2(f2(x37301,x37304),x37305)))),
% 250.76/250.74 inference(scs_inference,[],[3647,2829,673,12,956,20])).
% 250.76/250.74 cnf(3740,plain,
% 250.76/250.74 ($false),
% 250.76/250.74 inference(scs_inference,[],[4,3420,3730,1252,956,5]),
% 250.76/250.74 ['proof']).
% 250.76/250.74 % SZS output end Proof
% 250.76/250.74 % Total time :250.176271s
%------------------------------------------------------------------------------