%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL236-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n026.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:51 AM UTC 2026
% Result : Unsatisfiable 58.39s 58.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL236-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% 0.00/0.02 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.07/0.34 % Computer : n026.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 : Sat Sep 5 07:34:10 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.23/0.51 start to proof:theBenchmark
% 58.39/58.59 %-------------------------------------------
% 58.39/58.59 % File :CSE---1.7
% 58.39/58.59 % Problem :theBenchmark
% 58.39/58.59 % Transform :cnf
% 58.39/58.59 % Format :tptp:raw
% 58.39/58.59 % Command :java -jar mcs_scs.jar %d %s
% 58.39/58.59
% 58.39/58.59 % Result :Theorem 58.094862s
% 58.39/58.59 % Output :CNFRefutation 58.094862s
% 58.39/58.59 %-------------------------------------------
% 58.39/58.59 %--------------------------------------------------------------------------
% 58.39/58.59 % File : LCL236-1 : TPTP v9.3.1. Bugfixed v2.3.0.
% 58.39/58.59 % Domain : Logic Calculi (Propositional)
% 58.39/58.59 % Problem : Principia Mathematica 3.14
% 58.39/58.59 % Version : [WR27] axioms : Reduced & Augmented.
% 58.39/58.59 % English :
% 58.39/58.59
% 58.39/58.59 % Refs : [WR27] Whitehead & Russell (1927), Principia Mathematica
% 58.39/58.60 % : [NSS63] Newell et al. (1963), Empirical Explorations with the
% 58.39/58.60 % : [ORo89] O'Rourke (1989), LT Revisited: Explanation-Based Learn
% 58.39/58.60 % : [SE94] Segre & Elkan (1994), A High-Performance Explanation-B
% 58.39/58.60 % Source : [SE94]
% 58.39/58.60 % Names : Problem 3.14 [WR27]
% 58.39/58.60
% 58.39/58.60 % Status : Unsatisfiable
% 58.39/58.60 % Rating : 0.00 v5.5.0, 0.06 v5.4.0, 0.11 v5.3.0, 0.15 v5.2.0, 0.08 v5.1.0, 0.06 v5.0.0, 0.07 v4.0.1, 0.00 v2.3.0
% 58.39/58.60 % Syntax : Number of clauses : 9 ( 6 unt; 0 nHn; 4 RR)
% 58.39/58.60 % Number of literals : 14 ( 0 equ; 6 neg)
% 58.39/58.60 % Maximal clause size : 3 ( 1 avg)
% 58.39/58.60 % Maximal term depth : 6 ( 2 avg)
% 58.39/58.60 % Number of predicates : 2 ( 2 usr; 0 prp; 1-1 aty)
% 58.39/58.60 % Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% 58.39/58.60 % Number of variables : 17 ( 1 sgn)
% 58.39/58.60 % SPC : CNF_UNS_RFO_NEQ_HRN
% 58.39/58.60
% 58.39/58.60 % Comments : Reduced to use only or and not, and includes a redundant rule
% 58.39/58.60 % of transitivity of implication, and a reduced rule of
% 58.39/58.60 % detachment.
% 58.39/58.60 % Bugfixes : v2.3.0 - Function and/2 removed from prove_this
% 58.39/58.60 %--------------------------------------------------------------------------
% 58.39/58.60 %----Include axioms of propositional logic
% 58.39/58.60 include('Axioms/LCL003-0.ax').
% 58.39/58.60 %--------------------------------------------------------------------------
% 58.39/58.60 cnf(prove_this,negated_conjecture,
% 58.39/58.60 ~ theorem(or(not(or(not(p),not(q))),not(not(or(not(p),not(q)))))) ).
% 58.39/58.60
% 58.39/58.60 %--------------------------------------------------------------------------
% 58.39/58.60 %-------------------------------------------
% 58.39/58.60 % Proof found
% 58.39/58.60 % SZS status Theorem for theBenchmark
% 58.39/58.60 % SZS output start Proof
% 58.39/58.60 %ClaNum:9(EqnAxiom:0)
% 58.39/58.60 %VarNum:34(SingletonVarNum:17)
% 58.39/58.60 %MaxLitNum:3
% 58.39/58.60 %MaxfuncDepth:5
% 58.49/58.60 %SharedTerms:9
% 58.49/58.60 %goalClause: 6
% 58.49/58.60 %singleGoalClaCount:1
% 58.49/58.60 [6]~P2(f2(f1(f2(f1(a3),f1(a4))),f1(f1(f2(f1(a3),f1(a4))))))
% 58.49/58.60 [2]P1(f2(f1(f2(x21,x21)),x21))
% 58.49/58.60 [1]P1(f2(f1(x11),f2(x12,x11)))
% 58.49/58.60 [3]P1(f2(f1(f2(x31,x32)),f2(x32,x31)))
% 58.49/58.60 [4]P1(f2(f1(f2(x41,f2(x42,x43))),f2(x42,f2(x41,x43))))
% 58.49/58.60 [5]P1(f2(f1(f2(f1(x51),x52)),f2(f1(f2(x53,x51)),f2(x53,x52))))
% 58.49/58.60 [7]~P1(x71)+P2(x71)
% 58.49/58.60 [8]P2(x81)+~P2(x82)+~P1(f2(f1(x82),x81))
% 58.49/58.60 [9]~P2(f2(f1(x93),x92))+P2(f2(f1(x91),x92))+~P1(f2(f1(x91),x93))
% 58.49/58.60 %EqnAxiom
% 58.49/58.60
% 58.49/58.60 %-------------------------------------------
% 58.49/58.61 cnf(12,plain,
% 58.49/58.61 (~P2(f2(f1(f1(f2(f1(a3),f1(a4)))),f1(f2(f1(a3),f1(a4)))))),
% 58.49/58.61 inference(scs_inference,[],[6,3,7,8])).
% 58.49/58.61 cnf(17,plain,
% 58.49/58.61 (~P2(f1(f1(f2(f1(a3),f1(a4)))))),
% 58.49/58.61 inference(scs_inference,[],[6,1,7,8])).
% 58.49/58.61 cnf(22,plain,
% 58.49/58.61 (P2(f2(x221,f2(x222,x223)))+~P2(f2(x222,f2(x221,x223)))),
% 58.49/58.61 inference(scs_inference,[],[6,4,7,8])).
% 58.49/58.61 cnf(24,plain,
% 58.49/58.61 (~P2(f2(x241,f2(f1(x242),x243)))+P2(f2(f1(f2(x242,x242)),f2(x241,x243)))),
% 58.49/58.61 inference(scs_inference,[],[6,2,4,7,8,9])).
% 58.49/58.61 cnf(28,plain,
% 58.49/58.61 (P2(f2(f1(f2(x281,x282)),f2(x281,x283)))+~P2(f2(f1(x282),x283))),
% 58.49/58.61 inference(scs_inference,[],[6,5,7,8])).
% 58.49/58.61 cnf(30,plain,
% 58.49/58.61 (~P2(f2(x301,f2(f1(x302),x303)))+P2(f2(f1(f2(x304,f2(x302,x302))),f2(x304,f2(x301,x303))))),
% 58.49/58.61 inference(scs_inference,[],[6,5,7,8,24])).
% 58.49/58.61 cnf(56,plain,
% 58.49/58.61 (P2(f2(x561,f2(f1(f2(x562,f2(x561,x563))),f2(x562,x563))))),
% 58.49/58.61 inference(scs_inference,[],[4,22,7])).
% 58.49/58.61 cnf(57,plain,
% 58.49/58.61 (P2(f2(f1(f2(x571,f2(x572,x573))),f2(x572,f2(x571,x573))))),
% 58.49/58.61 inference(scs_inference,[],[56,22])).
% 58.49/58.61 cnf(59,plain,
% 58.49/58.61 (P2(f2(f1(f2(x591,x592)),f2(x591,f2(f1(f2(x593,f2(f1(x592),x594))),f2(x593,x594)))))),
% 58.49/58.61 inference(scs_inference,[],[56,22,28])).
% 58.49/58.61 cnf(66,plain,
% 58.49/58.61 (P2(f2(f1(f2(x661,f2(x662,f2(x663,x664)))),f2(x661,f2(x663,f2(x662,x664)))))),
% 58.49/58.61 inference(scs_inference,[],[57,59,22,28])).
% 58.49/58.61 cnf(70,plain,
% 58.49/58.61 (P2(f2(f1(f2(f1(x701),x702)),f2(x703,f2(f1(f2(x703,x701)),x702))))),
% 58.49/58.61 inference(scs_inference,[],[6,5,57,59,22,28,7,9])).
% 58.49/58.61 cnf(73,plain,
% 58.49/58.61 (P2(f2(x731,f2(f1(f2(x731,f2(x732,f2(x733,x734)))),f2(x733,f2(x732,x734)))))),
% 58.49/58.61 inference(scs_inference,[],[66,22])).
% 58.49/58.61 cnf(77,plain,
% 58.49/58.61 (P2(f2(f1(f2(x771,f2(x772,f2(x773,x774)))),f2(x772,f2(x773,f2(x771,x774)))))),
% 58.49/58.61 inference(scs_inference,[],[6,4,66,22,7,9])).
% 58.49/58.61 cnf(81,plain,
% 58.49/58.61 (P2(f2(x811,f2(f1(f2(x812,f2(x811,f2(x813,x814)))),f2(x813,f2(x812,x814)))))),
% 58.49/58.61 inference(scs_inference,[],[77,22])).
% 58.49/58.61 cnf(85,plain,
% 58.49/58.61 (P2(f2(f1(f2(f1(x851),x852)),f2(x853,f2(f1(f2(x853,f2(x854,x851))),f2(x854,x852)))))),
% 58.49/58.61 inference(scs_inference,[],[6,5,77,70,22,7,9])).
% 58.49/58.61 cnf(92,plain,
% 58.49/58.61 (P2(f2(f1(f2(x921,f2(f1(x922),x923))),f2(x924,f2(f1(f2(x924,x922)),f2(x921,x923)))))),
% 58.49/58.61 inference(scs_inference,[],[6,4,85,70,22,7,9])).
% 58.49/58.61 cnf(100,plain,
% 58.49/58.61 (P2(f2(f1(f2(f1(x1001),f2(x1002,x1003))),f2(f1(f2(x1004,x1001)),f2(x1002,f2(x1004,x1003)))))),
% 58.49/58.61 inference(scs_inference,[],[6,5,92,66,22,7,9])).
% 58.49/58.61 cnf(104,plain,
% 58.49/58.61 (P2(f2(f1(f2(x1041,x1042)),f2(f1(f2(f1(x1042),f2(x1043,x1044))),f2(x1043,f2(x1041,x1044)))))),
% 58.49/58.61 inference(scs_inference,[],[100,22])).
% 58.49/58.61 cnf(108,plain,
% 58.49/58.61 (P2(f2(f1(f2(x1081,f2(f1(x1082),x1083))),f2(f1(f2(x1084,x1082)),f2(x1081,f2(x1084,x1083)))))),
% 58.49/58.61 inference(scs_inference,[],[6,4,100,22,7,9])).
% 58.49/58.61 cnf(112,plain,
% 58.49/58.61 (P2(f2(f1(f2(x1121,x1122)),f2(f1(f2(x1123,f2(f1(x1122),x1124))),f2(x1123,f2(x1121,x1124)))))),
% 58.49/58.61 inference(scs_inference,[],[108,22])).
% 58.49/58.61 cnf(116,plain,
% 58.49/58.61 (P2(f2(f1(f2(f1(x1161),x1162)),f2(f1(f2(x1163,x1164)),f2(f1(f2(f1(x1164),x1161)),f2(x1163,x1162)))))),
% 58.49/58.61 inference(scs_inference,[],[6,5,108,22,7,9])).
% 58.49/58.61 cnf(120,plain,
% 58.49/58.61 (P2(f2(f1(f2(x1201,x1202)),f2(f1(f2(f1(x1203),x1204)),f2(f1(f2(f1(x1202),x1203)),f2(x1201,x1204)))))),
% 58.49/58.61 inference(scs_inference,[],[116,22])).
% 58.49/58.61 cnf(124,plain,
% 58.49/58.61 (P2(f2(f1(f2(x1241,f2(x1242,x1243))),f2(f1(f2(f1(f2(x1241,x1243)),f2(x1244,x1245))),f2(x1244,f2(x1242,x1245)))))),
% 58.49/58.61 inference(scs_inference,[],[6,4,104,116,22,7,9])).
% 58.49/58.61 cnf(127,plain,
% 58.49/58.61 (P2(f2(f1(f2(f1(f2(x1271,x1272)),f2(x1273,x1274))),f2(f1(f2(x1271,f2(x1275,x1272))),f2(x1273,f2(x1275,x1274)))))),
% 58.49/58.61 inference(scs_inference,[],[124,22])).
% 58.49/58.61 cnf(131,plain,
% 58.49/58.61 (P2(f2(f1(f2(f1(x1311),x1312)),f2(f1(f2(x1313,f2(x1314,x1311))),f2(x1314,f2(x1313,x1312)))))),
% 58.49/58.61 inference(scs_inference,[],[6,5,124,100,22,7,9])).
% 58.49/58.61 cnf(134,plain,
% 58.49/58.61 (P2(f2(f1(f2(x1341,f2(x1342,x1343))),f2(f1(f2(f1(x1343),x1344)),f2(x1342,f2(x1341,x1344)))))),
% 58.49/58.61 inference(scs_inference,[],[131,22])).
% 58.49/58.61 cnf(138,plain,
% 58.49/58.61 (P2(f2(f1(f2(x1381,f2(x1382,x1383))),f2(x1381,f2(x1382,x1383))))),
% 58.49/58.61 inference(scs_inference,[],[6,4,131,57,22,7,9])).
% 58.49/58.61 cnf(141,plain,
% 58.49/58.61 (P2(f2(x1411,f2(f1(f2(x1411,f2(x1412,x1413))),f2(x1412,x1413))))),
% 58.49/58.61 inference(scs_inference,[],[138,22])).
% 58.49/58.61 cnf(145,plain,
% 58.49/58.61 (P2(f2(f1(f2(f1(x1451),x1452)),f2(f1(f2(x1453,x1451)),f2(x1453,x1452))))),
% 58.49/58.61 inference(scs_inference,[],[6,5,138,22,7,9])).
% 58.49/58.61 cnf(150,plain,
% 58.49/58.61 (P2(f2(f1(f2(x1501,x1502)),f2(x1501,f2(f1(f2(f1(x1502),f2(x1503,x1504))),f2(x1503,x1504)))))),
% 58.49/58.61 inference(scs_inference,[],[141,28])).
% 58.49/58.61 cnf(151,plain,
% 58.49/58.61 (P2(f2(x1511,f2(f1(f2(x1511,f2(x1512,x1513))),f2(x1512,x1513))))),
% 58.49/58.61 inference(rename_variables,[],[141])).
% 58.49/58.61 cnf(153,plain,
% 58.49/58.61 (P2(f2(f1(f2(x1531,x1532)),f2(f1(f2(f1(x1532),x1533)),f2(x1531,x1533))))),
% 58.49/58.61 inference(scs_inference,[],[141,145,28,22])).
% 58.49/58.61 cnf(157,plain,
% 58.49/58.61 (P2(f2(f1(f2(x1571,f2(x1572,x1573))),f2(f1(f2(f1(f2(x1572,f2(x1571,x1573))),f2(x1574,x1575))),f2(x1574,x1575))))),
% 58.49/58.61 inference(scs_inference,[],[6,4,141,151,145,28,22,7,9])).
% 58.49/58.61 cnf(160,plain,
% 58.49/58.62 (P2(f2(f1(f2(x1601,f2(x1602,x1603))),f2(x1601,f2(f1(f2(f1(x1603),x1604)),f2(x1602,x1604)))))),
% 58.49/58.62 inference(scs_inference,[],[153,28])).
% 58.49/58.62 cnf(166,plain,
% 58.49/58.62 (P2(f2(f1(f2(f1(x1661),x1662)),f2(f1(f2(x1663,f2(x1664,x1661))),f2(x1663,f2(x1664,x1662)))))),
% 58.49/58.62 inference(scs_inference,[],[6,5,153,157,127,28,22,7,9])).
% 58.49/58.62 cnf(169,plain,
% 58.49/58.62 (P2(f2(f1(f2(x1691,f2(f1(x1692),x1693))),f2(x1691,f2(f1(f2(x1694,x1692)),f2(x1694,x1693)))))),
% 58.49/58.62 inference(scs_inference,[],[145,28])).
% 58.49/58.62 cnf(175,plain,
% 58.49/58.62 (P2(f2(f1(f2(x1751,f2(x1752,x1753))),f2(f1(f2(f1(x1753),x1754)),f2(x1751,f2(x1752,x1754)))))),
% 58.49/58.62 inference(scs_inference,[],[6,4,134,150,145,28,22,7,9])).
% 58.49/58.62 cnf(179,plain,
% 58.49/58.62 (P2(f2(x1791,f2(f1(f2(x1791,f2(x1792,x1793))),f2(f1(f2(f1(x1793),x1794)),f2(x1792,x1794)))))),
% 58.49/58.62 inference(scs_inference,[],[160,22])).
% 58.49/58.62 cnf(183,plain,
% 58.49/58.62 (P2(f2(f1(f2(f1(x1831),x1832)),f2(f1(f2(x1833,x1831)),f2(f1(f2(f1(x1832),x1834)),f2(x1833,x1834)))))),
% 58.49/58.62 inference(scs_inference,[],[6,5,160,22,7,9])).
% 58.49/58.62 cnf(186,plain,
% 58.49/58.62 (P2(f2(x1861,f2(f1(f2(x1861,f2(f1(x1862),x1863))),f2(f1(f2(x1864,x1862)),f2(x1864,x1863)))))),
% 58.49/58.62 inference(scs_inference,[],[169,22])).
% 58.49/58.62 cnf(190,plain,
% 58.49/58.62 (P2(f2(f1(f2(f1(x1901),f2(x1902,x1903))),f2(x1902,f2(f1(f2(x1904,x1901)),f2(x1904,x1903)))))),
% 58.49/58.62 inference(scs_inference,[],[6,4,169,22,7,9])).
% 58.49/58.62 cnf(198,plain,
% 58.49/58.62 (P2(f2(f1(f2(f1(x1981),x1982)),f2(f1(f2(f1(x1982),x1983)),f2(f1(f2(x1984,x1981)),f2(x1984,x1983)))))),
% 58.49/58.62 inference(scs_inference,[],[6,5,175,183,22,7,9])).
% 58.49/58.62 cnf(201,plain,
% 58.49/58.62 (P2(f2(x2011,f2(f1(f2(f1(x2012),f2(x2011,x2013))),f2(f1(f2(x2014,x2012)),f2(x2014,x2013)))))),
% 58.49/58.62 inference(scs_inference,[],[190,22])).
% 58.49/58.62 cnf(205,plain,
% 58.49/58.62 (P2(f2(f1(f2(x2051,f2(x2052,x2053))),f2(f1(f2(f1(f2(x2051,x2053)),x2054)),f2(x2052,x2054))))),
% 58.49/58.62 inference(scs_inference,[],[6,4,190,153,22,7,9])).
% 58.49/58.62 cnf(208,plain,
% 58.49/58.62 (P2(f2(f1(f2(f1(f2(x2081,x2082)),x2083)),f2(f1(f2(x2081,f2(x2084,x2082))),f2(x2084,x2083))))),
% 58.49/58.62 inference(scs_inference,[],[205,22])).
% 58.49/58.62 cnf(212,plain,
% 58.49/58.62 (P2(f2(f1(f2(f1(x2121),x2122)),f2(f1(f2(f1(f2(f1(f2(x2123,x2121)),f2(x2123,x2122))),f2(x2124,x2125))),f2(x2124,x2125))))),
% 58.49/58.62 inference(scs_inference,[],[6,5,205,141,22,7,9])).
% 58.49/58.62 cnf(219,plain,
% 58.49/58.62 (P2(f2(f1(f2(x2191,f2(x2192,x2193))),f2(x2192,f2(f1(f2(f1(f2(x2191,x2193)),f2(x2194,x2195))),f2(x2194,x2195)))))),
% 58.49/58.62 inference(scs_inference,[],[6,4,212,150,22,7,9])).
% 58.49/58.62 cnf(222,plain,
% 58.49/58.62 (P2(f2(f1(f2(f1(x2221),x2222)),f2(f1(f2(f1(x2223),x2221)),f2(f1(f2(x2224,x2223)),f2(x2224,x2222)))))),
% 58.49/58.62 inference(scs_inference,[],[198,22])).
% 58.49/58.62 cnf(233,plain,
% 58.49/58.62 (P2(f2(f1(f2(x2331,f2(f1(x2332),x2333))),f2(f1(f2(x2334,x2332)),f2(x2334,f2(x2331,x2333)))))),
% 58.49/58.62 inference(scs_inference,[],[6,4,219,145,22,7,9])).
% 58.49/58.62 cnf(244,plain,
% 58.49/58.62 (P2(f2(f1(f2(x2441,x2442)),f2(f1(f2(x2443,f2(f1(x2442),x2444))),f2(x2441,f2(x2443,x2444)))))),
% 58.49/58.62 inference(scs_inference,[],[233,22])).
% 58.49/58.62 cnf(265,plain,
% 58.49/58.62 (P2(f2(f1(f2(f2(x2651,x2652),f2(x2651,x2652))),f2(f1(f2(f1(x2652),x2653)),f2(x2651,x2653))))),
% 58.49/58.62 inference(scs_inference,[],[5,7,24])).
% 58.49/58.62 cnf(266,plain,
% 58.49/58.62 (P2(f2(f1(f2(f1(x2661),x2662)),f2(f1(f2(f2(x2663,x2661),f2(x2663,x2661))),f2(x2663,x2662))))),
% 58.49/58.62 inference(scs_inference,[],[265,22])).
% 58.49/58.62 cnf(270,plain,
% 58.49/58.62 (P2(f2(f1(f2(x2701,f2(f2(x2701,x2702),x2702))),f2(f1(f2(f1(x2702),x2703)),f2(x2701,x2703))))),
% 58.49/58.62 inference(scs_inference,[],[6,4,265,22,7,9])).
% 58.49/58.62 cnf(274,plain,
% 58.49/58.62 (P2(f2(f1(f2(f1(x2741),x2742)),f2(f1(f2(x2743,f2(f2(x2743,x2741),x2741))),f2(x2743,x2742))))),
% 58.49/58.62 inference(scs_inference,[],[270,22])).
% 58.49/58.62 cnf(335,plain,
% 58.49/58.62 (P2(f2(f1(f2(x3351,x3351)),f2(f1(f2(x3352,f2(f1(x3351),x3353))),f2(x3352,x3353))))),
% 58.49/58.62 inference(scs_inference,[],[4,7,24])).
% 58.49/58.62 cnf(336,plain,
% 58.49/58.62 (P2(f2(f1(f2(x3361,f2(f1(x3362),x3363))),f2(f1(f2(x3362,x3362)),f2(x3361,x3363))))),
% 58.49/58.62 inference(scs_inference,[],[335,22])).
% 58.49/58.62 cnf(398,plain,
% 58.49/58.62 (P2(f2(f1(f2(f2(f1(x3981),x3982),f2(f1(x3981),x3982))),f2(f1(f2(f2(x3983,x3981),f2(x3983,x3981))),f2(x3983,x3982))))),
% 58.49/58.62 inference(scs_inference,[],[266,22,24])).
% 58.49/58.62 cnf(399,plain,
% 58.49/58.62 (P2(f2(f1(f2(f2(x3991,x3992),f2(x3991,x3992))),f2(f1(f2(f2(f1(x3992),x3993),f2(f1(x3992),x3993))),f2(x3991,x3993))))),
% 58.49/58.62 inference(scs_inference,[],[398,22])).
% 58.49/58.62 cnf(415,plain,
% 58.49/58.62 (P2(f2(f1(f2(x4151,x4152)),f2(f1(f2(f2(f1(x4152),x4153),f2(f1(x4152),x4153))),f2(x4151,x4153))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,399,7,9])).
% 58.49/58.62 cnf(422,plain,
% 58.49/58.62 (P2(f2(f1(x4221),f2(f1(f2(x4222,f2(f2(x4222,x4223),x4223))),f2(x4222,x4221))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,274,7,9])).
% 58.49/58.62 cnf(426,plain,
% 58.49/58.62 (P2(f2(f1(f2(x4261,f2(f2(x4261,x4262),x4262))),f2(f1(x4263),f2(x4261,x4263))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,274,7,9,22])).
% 58.49/58.62 cnf(428,plain,
% 58.49/58.62 (P2(f2(f1(f2(x4281,x4282)),f2(x4281,f2(f1(f2(x4283,f2(f2(x4283,x4284),x4284))),f2(x4283,x4282)))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,274,7,9,22,28])).
% 58.49/58.62 cnf(434,plain,
% 58.49/58.62 (P2(f2(f1(x4341),f2(f1(f2(f2(f1(x4341),x4342),f2(f1(x4341),x4342))),f2(x4343,x4342))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,415,428,22,7,9])).
% 58.49/58.62 cnf(437,plain,
% 58.49/58.62 (P2(f2(f1(f2(f2(f1(x4371),x4372),f2(f1(x4371),x4372))),f2(f1(x4371),f2(x4373,x4372))))),
% 58.49/58.62 inference(scs_inference,[],[434,22])).
% 58.49/58.62 cnf(441,plain,
% 58.49/58.62 (P2(f2(f1(f2(f1(x4411),x4412)),f2(f1(f2(x4411,x4411)),f2(x4413,x4412))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,336,434,22,7,9])).
% 58.49/58.62 cnf(445,plain,
% 58.49/58.62 (P2(f2(f1(f2(x4451,f2(f1(x4452),x4453))),f2(x4451,f2(f1(f2(x4452,x4452)),f2(x4454,x4453)))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,336,434,22,7,9,28])).
% 58.49/58.62 cnf(447,plain,
% 58.49/58.62 (P2(f2(f1(f2(x4471,x4471)),f2(f1(f2(f1(x4471),x4472)),f2(x4473,x4472))))),
% 58.49/58.62 inference(scs_inference,[],[441,22])).
% 58.49/58.62 cnf(451,plain,
% 58.49/58.62 (P2(f2(f1(x4511),f2(f1(f2(x4512,f2(f2(x4512,x4513),x4513))),f2(x4512,f2(x4514,x4511)))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,422,441,22,7,9])).
% 58.49/58.62 cnf(454,plain,
% 58.49/58.62 (P2(f2(f1(f2(x4541,f2(x4542,x4542))),f2(x4541,f2(f1(f2(f1(x4542),x4543)),f2(x4544,x4543)))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,422,441,22,7,9,28])).
% 58.49/58.62 cnf(456,plain,
% 58.49/58.62 (P2(f2(x4561,f2(f1(f2(x4561,f2(f1(x4562),x4563))),f2(f1(f2(x4562,x4562)),f2(x4564,x4563)))))),
% 58.49/58.62 inference(scs_inference,[],[445,22])).
% 58.49/58.62 cnf(460,plain,
% 58.49/58.62 (P2(f2(f1(f2(f2(x4601,x4602),x4602)),f2(f1(x4603),f2(x4601,x4603))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,426,445,22,7,9])).
% 58.49/58.62 cnf(464,plain,
% 58.49/58.62 (P2(f2(f1(f2(x4641,f2(f2(x4642,x4643),x4643))),f2(x4641,f2(f1(x4644),f2(x4642,x4644)))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,426,445,22,7,9,28])).
% 58.49/58.62 cnf(470,plain,
% 58.49/58.62 (P2(f2(f1(f2(f1(x4701),x4702)),f2(f1(x4701),f2(x4703,x4702))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,437,460,22,7,9])).
% 58.49/58.62 cnf(473,plain,
% 58.49/58.62 (P2(f2(f1(f2(x4731,x4732)),f2(x4731,f2(f1(f2(f2(x4733,x4734),x4734)),f2(x4733,x4732)))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,437,460,22,7,9,28])).
% 58.49/58.62 cnf(477,plain,
% 58.49/58.62 (P2(f2(f1(x4771),f2(f1(f2(f1(x4771),x4772)),f2(x4773,x4772))))),
% 58.49/58.62 inference(scs_inference,[],[470,28,22])).
% 58.49/58.62 cnf(481,plain,
% 58.49/58.62 (P2(f2(f1(x4811),f2(f1(f2(x4812,f2(x4813,x4814))),f2(x4813,x4811))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,208,470,28,22,7,9])).
% 58.49/58.62 cnf(485,plain,
% 58.49/58.62 (P2(f2(f1(f2(x4851,x4852)),f2(x4851,f2(f1(f2(f1(x4852),x4853)),f2(x4854,x4853)))))),
% 58.49/58.62 inference(scs_inference,[],[477,28])).
% 58.49/58.62 cnf(487,plain,
% 58.49/58.62 (P2(f2(f1(f2(x4871,f2(x4872,x4873))),f2(f1(x4874),f2(x4872,x4874))))),
% 58.49/58.62 inference(scs_inference,[],[477,481,28,22])).
% 58.49/58.62 cnf(494,plain,
% 58.49/58.62 (P2(f2(x4941,f2(f1(x4942),x4942)))),
% 58.49/58.62 inference(scs_inference,[],[1,22,7])).
% 58.49/58.62 cnf(495,plain,
% 58.49/58.62 (P2(f2(f1(f2(x4951,f2(x4952,f2(x4953,x4954)))),f2(x4951,f2(f1(x4955),f2(x4953,x4955)))))),
% 58.49/58.62 inference(scs_inference,[],[487,28])).
% 58.49/58.62 cnf(497,plain,
% 58.49/58.62 (P2(f2(f1(x4971),f2(x4972,x4971)))),
% 58.49/58.62 inference(scs_inference,[],[487,494,28,22])).
% 58.49/58.62 cnf(504,plain,
% 58.49/58.62 (P2(f2(f1(f2(x5041,x5042)),f2(x5041,f2(x5043,x5042))))),
% 58.49/58.62 inference(scs_inference,[],[497,28])).
% 58.49/58.62 cnf(506,plain,
% 58.49/58.62 (P2(f2(f1(f2(x5061,f2(f2(x5061,x5062),x5062))),f2(f1(x5063),f2(x5061,f2(x5064,x5063)))))),
% 58.49/58.62 inference(scs_inference,[],[497,451,28,22])).
% 58.49/58.62 cnf(510,plain,
% 58.49/58.62 (P2(f2(f1(x5101),f2(x5102,f2(x5103,x5101))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,497,451,28,22,7,9])).
% 58.49/58.62 cnf(513,plain,
% 58.49/58.62 (P2(f2(f1(f2(x5131,f2(x5132,x5133))),f2(x5131,f2(x5132,f2(x5134,x5133)))))),
% 58.49/58.62 inference(scs_inference,[],[504,28])).
% 58.49/58.62 cnf(515,plain,
% 58.49/58.62 (P2(f2(x5151,f2(f1(f2(x5151,x5152)),f2(x5153,x5152))))),
% 58.49/58.62 inference(scs_inference,[],[504,28,22])).
% 58.49/58.62 cnf(519,plain,
% 58.49/58.62 (P2(f2(f1(x5191),f2(x5192,f2(x5193,f2(x5194,x5191)))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,504,510,28,22,7,9])).
% 58.49/58.62 cnf(524,plain,
% 58.49/58.62 (P2(f2(x5241,f2(f1(f2(x5241,f2(x5242,x5242))),f2(f1(f2(f1(x5242),x5243)),f2(x5244,x5243)))))),
% 58.49/58.62 inference(scs_inference,[],[6,454,7,22])).
% 58.49/58.62 cnf(526,plain,
% 58.49/58.62 (P2(f2(f1(f2(x5261,x5262)),f2(x5261,f2(x5263,f2(x5264,f2(x5265,x5262))))))),
% 58.49/58.62 inference(scs_inference,[],[6,454,519,7,22,28])).
% 58.49/58.62 cnf(528,plain,
% 58.49/58.62 (P2(f2(f1(x5281),f2(f1(f2(f1(f2(x5282,x5281)),x5283)),f2(x5284,x5283))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,515,454,519,7,22,28,9])).
% 58.49/58.62 cnf(533,plain,
% 58.49/58.62 (P2(f2(f1(f2(x5331,x5332)),f2(x5331,f2(f1(f2(f1(f2(x5333,x5332)),x5334)),f2(x5335,x5334)))))),
% 58.49/58.62 inference(scs_inference,[],[528,22,28])).
% 58.49/58.62 cnf(537,plain,
% 58.49/58.62 (P2(f2(f1(x5371),f2(f1(f2(f1(f2(x5372,f2(x5373,x5371))),x5374)),f2(x5375,x5374))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,528,22,28,7,9])).
% 58.49/58.62 cnf(542,plain,
% 58.49/58.62 (P2(f2(f1(f2(x5421,x5422)),f2(x5421,f2(f1(x5423),x5423))))),
% 58.49/58.62 inference(scs_inference,[],[6,494,7,28])).
% 58.49/58.62 cnf(545,plain,
% 58.49/58.62 (P2(f2(f1(f2(f1(f2(x5451,f2(x5452,x5453))),x5454)),f2(f1(x5453),f2(x5455,x5454))))),
% 58.49/58.62 inference(scs_inference,[],[6,537,494,7,28,22])).
% 58.49/58.62 cnf(547,plain,
% 58.49/58.62 (P2(f2(f1(x5471),f2(f1(f2(f1(f2(x5472,x5471)),f2(x5473,f2(x5474,x5475)))),f2(x5474,f2(x5473,x5475)))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,537,73,494,7,28,22,9])).
% 58.49/58.62 cnf(550,plain,
% 58.49/58.62 (P2(f2(f1(f2(x5501,f2(x5502,x5503))),f2(x5501,f2(x5502,f2(f1(x5504),x5504)))))),
% 58.49/58.62 inference(scs_inference,[],[542,28])).
% 58.49/58.62 cnf(552,plain,
% 58.49/58.62 (P2(f2(x5521,f2(f1(f2(x5521,f2(f2(x5522,x5523),x5523))),f2(f1(x5524),f2(x5522,x5524)))))),
% 58.49/58.62 inference(scs_inference,[],[464,542,28,22])).
% 58.49/58.62 cnf(556,plain,
% 58.49/58.62 (P2(f2(f1(x5561),f2(f1(f2(x5562,f2(f1(f2(x5563,x5561)),f2(x5564,x5565)))),f2(x5564,f2(x5562,x5565)))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,81,464,542,28,22,7,9])).
% 58.49/58.62 cnf(563,plain,
% 58.49/58.62 (P2(f2(f1(f2(x5631,x5632)),f2(x5631,f2(x5633,f2(x5634,x5632)))))),
% 58.49/58.62 inference(scs_inference,[],[6,473,510,7,22,28])).
% 58.49/58.62 cnf(565,plain,
% 58.49/58.62 (P2(f2(f1(x5651),f2(f1(f2(x5652,f2(f1(x5651),x5653))),f2(x5652,f2(x5654,x5653)))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,112,473,510,7,22,28,9])).
% 58.49/58.62 cnf(568,plain,
% 58.49/58.62 (P2(f2(f1(f2(f1(f2(x5681,x5682)),f2(x5683,f2(x5684,x5685)))),f2(f1(x5682),f2(x5684,f2(x5683,x5685)))))),
% 58.49/58.62 inference(scs_inference,[],[547,22])).
% 58.49/58.62 cnf(570,plain,
% 58.49/58.62 (P2(f2(f1(f2(x5701,f2(x5702,x5703))),f2(x5701,f2(x5702,f2(x5704,f2(x5705,x5703))))))),
% 58.49/58.62 inference(scs_inference,[],[547,563,22,28])).
% 58.49/58.62 cnf(574,plain,
% 58.49/58.62 (P2(f2(f1(x5741),f2(f1(f2(f1(x5742),x5743)),f2(f1(f2(f1(x5741),x5742)),f2(x5744,x5743)))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,120,547,563,22,28,7,9])).
% 58.49/58.62 cnf(579,plain,
% 58.49/58.62 (P2(f2(f1(f2(x5791,f2(f1(f2(x5792,x5793)),f2(x5794,x5795)))),f2(f1(x5793),f2(x5794,f2(x5791,x5795)))))),
% 58.49/58.62 inference(scs_inference,[],[6,556,7,22])).
% 58.49/58.62 cnf(581,plain,
% 58.49/58.62 (P2(f2(f1(x5811),f2(f1(f2(f1(f2(x5812,x5811)),f2(x5813,x5814))),f2(f1(f2(f1(x5814),x5815)),f2(x5813,x5815)))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,179,556,7,22,9])).
% 58.49/58.62 cnf(586,plain,
% 58.49/58.62 (P2(f2(f1(f2(f1(f2(x5861,x5862)),f2(x5863,x5864))),f2(f1(x5862),f2(f1(f2(f1(x5864),x5865)),f2(x5863,x5865)))))),
% 58.49/58.62 inference(scs_inference,[],[6,581,7,22])).
% 58.49/58.62 cnf(588,plain,
% 58.49/58.62 (P2(f2(f1(x5881),f2(f1(f2(f1(f2(x5882,x5881)),f2(f1(x5883),x5884))),f2(f1(f2(x5885,x5883)),f2(x5885,x5884)))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,186,581,7,22,9])).
% 58.49/58.62 cnf(591,plain,
% 58.49/58.62 (P2(f2(f1(f2(f1(f2(x5911,x5912)),f2(f1(x5913),x5914))),f2(f1(x5912),f2(f1(f2(x5915,x5913)),f2(x5915,x5914)))))),
% 58.49/58.62 inference(scs_inference,[],[588,22])).
% 58.49/58.62 cnf(602,plain,
% 58.49/58.62 (P2(f2(f1(x6021),f2(f1(f2(x6022,f2(f1(x6021),x6023))),f2(x6024,f2(x6022,x6023)))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,244,485,7,22,9])).
% 58.49/58.62 cnf(605,plain,
% 58.49/58.62 (P2(f2(x6051,f2(f1(f2(x6051,f2(x6052,x6053))),f2(x6052,f2(x6054,x6053)))))),
% 58.49/58.62 inference(scs_inference,[],[513,22])).
% 58.49/58.62 cnf(609,plain,
% 58.49/58.62 (P2(f2(f1(x6091),f2(f1(f2(f1(f2(x6092,x6091)),f2(f1(x6093),x6094))),f2(f1(f2(x6093,x6093)),f2(x6095,x6094)))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,456,513,22,7,9])).
% 58.49/58.62 cnf(612,plain,
% 58.49/58.62 (P2(f2(f1(f2(x6121,x6122)),f2(x6121,f2(f1(f2(f1(x6122),f2(x6123,x6124))),f2(x6123,f2(x6125,x6124))))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,456,513,22,7,9,28])).
% 58.49/58.62 cnf(616,plain,
% 58.49/58.62 (P2(f2(f1(f2(f1(f2(x6161,x6162)),f2(f1(x6163),x6164))),f2(f1(x6162),f2(f1(f2(x6163,x6163)),f2(x6165,x6164)))))),
% 58.49/58.62 inference(scs_inference,[],[6,609,7,22])).
% 58.49/58.62 cnf(618,plain,
% 58.49/58.62 (P2(f2(f1(f2(f2(x6181,x6182),x6182)),f2(f1(x6183),f2(x6181,f2(x6184,x6183)))))),
% 58.49/58.62 inference(scs_inference,[],[1,6,506,609,7,22,9])).
% 58.49/58.62 cnf(627,plain,
% 58.49/58.63 (P2(f2(f1(x6271),f2(f1(f2(f1(f2(x6272,x6271)),f2(x6273,x6273))),f2(f1(f2(f1(x6273),x6274)),f2(x6275,x6274)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,524,565,22,7,9])).
% 58.49/58.63 cnf(632,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(f2(x6321,x6322)),f2(x6323,x6323))),f2(f1(x6322),f2(f1(f2(f1(x6323),x6324)),f2(x6325,x6324)))))),
% 58.49/58.63 inference(scs_inference,[],[6,627,7,22])).
% 58.49/58.63 cnf(634,plain,
% 58.49/58.63 (P2(f2(f1(x6341),f2(f1(f2(f1(f2(x6342,x6341)),f2(f2(x6343,x6344),x6344))),f2(f1(x6345),f2(x6343,x6345)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,552,627,7,22,9])).
% 58.49/58.63 cnf(637,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(f2(x6371,x6372)),f2(f2(x6373,x6374),x6374))),f2(f1(x6372),f2(f1(x6375),f2(x6373,x6375)))))),
% 58.49/58.63 inference(scs_inference,[],[634,22])).
% 58.49/58.63 cnf(641,plain,
% 58.49/58.63 (P2(f2(f1(f2(x6411,f2(x6412,x6413))),f2(f1(x6414),f2(x6412,f2(x6411,x6413)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,568,634,22,7,9])).
% 58.49/58.63 cnf(648,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(f2(x6481,x6482)),f2(x6483,x6484))),f2(f1(x6482),f2(x6483,f2(x6485,x6484)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,579,574,7,22,9])).
% 58.49/58.63 cnf(652,plain,
% 58.49/58.63 (P2(f2(f1(f2(x6521,f2(f1(x6522),x6523))),f2(f1(x6522),f2(x6524,f2(x6521,x6523)))))),
% 58.49/58.63 inference(scs_inference,[],[602,22])).
% 58.49/58.63 cnf(656,plain,
% 58.49/58.63 (P2(f2(f1(f2(x6561,x6562)),f2(f1(x6563),f2(f1(f2(f1(x6562),x6564)),f2(x6561,x6564)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,586,602,22,7,9])).
% 58.49/58.63 cnf(663,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(x6631),x6632)),f2(f1(x6633),f2(f1(f2(x6634,x6631)),f2(x6634,x6632)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,591,641,7,22,9])).
% 58.49/58.63 cnf(666,plain,
% 58.49/58.63 (P2(f2(f1(f2(x6661,x6662)),f2(x6661,f2(f1(f2(x6663,f2(x6664,x6665))),f2(x6664,f2(x6663,x6665))))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,591,641,7,22,9,28])).
% 58.49/58.63 cnf(672,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(x6721),x6722)),f2(f1(x6723),f2(f1(f2(x6721,x6721)),f2(x6724,x6722)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,616,656,22,7,9])).
% 58.49/58.63 cnf(679,plain,
% 58.49/58.63 (P2(f2(f1(f2(x6791,x6791)),f2(f1(x6792),f2(f1(f2(f1(x6791),x6793)),f2(x6794,x6793)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,632,663,7,22,9])).
% 58.49/58.63 cnf(686,plain,
% 58.49/58.63 (P2(f2(f1(f2(f2(x6861,x6862),x6862)),f2(f1(x6863),f2(f1(x6864),f2(x6861,x6864)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,637,672,22,7,9])).
% 58.49/58.63 cnf(693,plain,
% 58.49/58.63 (P2(f2(f1(x6931),f2(f1(f2(f1(f2(x6932,x6931)),f2(x6933,x6934))),f2(x6933,f2(x6935,x6934)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,605,679,7,22,9])).
% 58.49/58.63 cnf(700,plain,
% 58.49/58.63 (P2(f2(f1(x7001),f2(f1(x7002),f2(x7003,f2(x7004,x7002)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,618,686,22,7,9])).
% 58.49/58.63 cnf(704,plain,
% 58.49/58.63 (P2(f2(f1(f2(x7041,x7042)),f2(x7041,f2(f1(f2(f2(x7043,x7044),x7044)),f2(f1(x7045),f2(x7043,x7045))))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,618,686,22,7,9,28])).
% 58.49/58.63 cnf(710,plain,
% 58.49/58.63 (P2(f2(x7101,f2(f1(f2(x7101,f2(x7102,f2(x7103,x7104)))),f2(f1(x7105),f2(x7103,x7105)))))),
% 58.49/58.63 inference(scs_inference,[],[6,495,700,28,7,22])).
% 58.49/58.63 cnf(712,plain,
% 58.49/58.63 (P2(f2(f1(f2(x7121,f2(x7122,x7123))),f2(x7124,f2(f1(x7125),f2(x7122,x7125)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,495,700,28,7,22,9])).
% 58.49/58.63 cnf(720,plain,
% 58.49/58.63 (P2(f2(f1(x7201),f2(x7202,f2(f1(f2(f1(f2(x7203,x7201)),x7204)),f2(x7205,x7204)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,533,22,7,9])).
% 58.49/58.63 cnf(727,plain,
% 58.49/58.63 (P2(f2(f1(f2(x7271,x7272)),f2(f1(x7273),f2(x7271,f2(x7274,x7272)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,648,712,7,22,9])).
% 58.49/58.63 cnf(732,plain,
% 58.49/58.63 (P2(f2(f1(f2(x7321,f2(x7322,x7323))),f2(x7321,f2(f1(x7324),f2(x7322,f2(x7325,x7323))))))),
% 58.49/58.63 inference(scs_inference,[],[727,28])).
% 58.49/58.63 cnf(734,plain,
% 58.49/58.63 (P2(f2(f1(x7341),f2(f1(f2(x7342,x7343)),f2(x7342,f2(x7344,x7343)))))),
% 58.49/58.63 inference(scs_inference,[],[727,28,22])).
% 58.49/58.63 cnf(738,plain,
% 58.49/58.63 (P2(f2(f1(x7381),f2(f1(f2(f1(f2(x7382,f2(x7383,x7381))),f2(x7384,x7385))),f2(x7384,f2(x7386,x7385)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,693,727,28,22,7,9])).
% 58.49/58.63 cnf(748,plain,
% 58.49/58.63 (P2(f2(f1(x7481),f2(f1(f2(f1(f2(x7482,x7481)),f2(x7483,f2(x7484,x7485)))),f2(f1(x7486),f2(x7484,x7486)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,710,734,738,28,7,22,9])).
% 58.49/58.63 cnf(755,plain,
% 58.49/58.63 (P2(f2(f1(x7551),f2(x7552,f2(f1(f2(f1(x7551),f2(x7553,x7554))),f2(x7553,f2(x7555,x7554))))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,748,612,7,22,9])).
% 58.49/58.63 cnf(762,plain,
% 58.49/58.63 (P2(f2(f1(x7621),f2(x7622,f2(f1(f2(x7623,f2(x7624,x7625))),f2(x7624,f2(x7623,x7625))))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,720,666,7,22,9])).
% 58.49/58.63 cnf(769,plain,
% 58.49/58.63 (P2(f2(f1(x7691),f2(x7692,f2(f1(f2(f2(x7693,x7694),x7694)),f2(f1(x7695),f2(x7693,x7695))))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,704,22,7,9])).
% 58.49/58.63 cnf(776,plain,
% 58.49/58.63 (P2(f2(f1(f2(x7761,x7762)),f2(x7763,f2(x7761,f2(f1(x7764),x7764)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,550,7,22,9])).
% 58.49/58.63 cnf(780,plain,
% 58.49/58.63 (P2(f2(x7801,f2(f1(f2(x7801,f2(x7802,x7803))),f2(x7802,f2(x7804,f2(x7805,x7803))))))),
% 58.49/58.63 inference(scs_inference,[],[570,22])).
% 58.49/58.63 cnf(789,plain,
% 58.49/58.63 (P2(f2(x7891,f2(f1(f2(x7891,f2(x7892,x7893))),f2(f1(x7894),f2(x7892,f2(x7895,x7893))))))),
% 58.49/58.63 inference(scs_inference,[],[6,732,7,22])).
% 58.49/58.63 cnf(791,plain,
% 58.49/58.63 (P2(f2(f1(f2(x7911,x7912)),f2(x7913,f2(f1(x7914),f2(x7911,f2(x7915,x7912))))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,732,7,22,9])).
% 58.49/58.63 cnf(806,plain,
% 58.49/58.63 (P2(f2(f1(x8061),f2(x8062,f2(f1(f2(f1(f2(x8063,x8061)),f2(x8064,x8065))),f2(x8064,f2(x8066,x8065))))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,755,7,22,9])).
% 58.49/58.63 cnf(813,plain,
% 58.49/58.63 (P2(f2(f1(x8131),f2(f1(f2(f1(f2(x8132,x8131)),f2(x8133,x8134))),f2(x8133,f2(x8135,f2(x8136,x8134))))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,762,780,22,7,9])).
% 58.49/58.63 cnf(820,plain,
% 58.49/58.63 (P2(f2(f1(x8201),f2(f1(f2(f1(f2(x8202,x8201)),f2(x8203,x8204))),f2(f1(x8205),f2(x8203,f2(x8206,x8204))))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,769,789,7,22,9])).
% 58.49/58.63 cnf(834,plain,
% 58.49/58.63 (P2(f2(f1(x8341),f2(x8342,f2(x8343,f2(f1(x8344),x8344)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,776,7,22,9])).
% 58.49/58.63 cnf(841,plain,
% 58.49/58.63 (P2(f2(f1(x8411),f2(x8412,f2(x8413,f2(x8414,f2(x8415,x8411))))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,806,526,22,7,9])).
% 58.49/58.63 cnf(846,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(f2(x8461,x8462)),f2(x8463,x8464))),f2(f1(x8462),f2(x8463,f2(x8465,f2(x8466,x8464))))))),
% 58.49/58.63 inference(scs_inference,[],[6,813,7,22])).
% 58.49/58.63 cnf(856,plain,
% 58.49/58.63 (P2(f2(f1(f2(x8561,x8562)),f2(f1(x8563),f2(x8561,f2(x8564,f2(x8565,x8562))))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,820,846,22,7,9])).
% 58.49/58.63 cnf(863,plain,
% 58.49/58.63 (P2(f2(f1(f2(f2(x8631,x8632),x8632)),f2(f1(f2(f1(x8632),x8633)),f2(x8631,x8633))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,791,270,7,22,9])).
% 58.49/58.63 cnf(871,plain,
% 58.49/58.63 (P2(f2(f1(f2(x8711,x8712)),f2(f1(f2(f1(f2(x8711,f2(x8713,x8712))),f2(x8714,x8715))),f2(x8714,x8715))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,863,157,22,7,9])).
% 58.49/58.63 cnf(879,plain,
% 58.49/58.63 (P2(f2(f1(x8791),f2(f1(f2(f1(f2(x8792,f2(x8793,x8791))),f2(x8794,x8795))),f2(x8794,x8795))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,871,7,22,9])).
% 58.49/58.63 cnf(950,plain,
% 58.49/58.63 (P2(f2(f1(x9501),f2(x9502,f2(f1(f2(x9503,f2(f1(x9501),x9504))),f2(x9503,x9504)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,856,59,7,22,9])).
% 58.49/58.63 cnf(957,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(x9571),x9572)),f2(x9573,f2(f1(f2(x9573,x9571)),f2(x9574,x9572)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,950,92,7,22,9])).
% 58.49/58.63 cnf(963,plain,
% 58.49/58.63 (P2(f2(x9631,f2(f1(f2(f1(x9632),x9633)),f2(f1(f2(x9631,x9632)),f2(x9634,x9633)))))),
% 58.49/58.63 inference(scs_inference,[],[6,957,7,22])).
% 58.49/58.63 cnf(965,plain,
% 58.49/58.63 (P2(f2(f1(f2(x9651,x9652)),f2(f1(f2(f1(f2(x9653,x9652)),f2(x9654,x9655))),f2(x9654,f2(x9651,x9655)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,957,124,7,22,9])).
% 58.49/58.63 cnf(971,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(f2(x9711,x9712)),f2(x9713,x9714))),f2(f1(f2(x9715,x9712)),f2(x9713,f2(x9715,x9714)))))),
% 58.49/58.63 inference(scs_inference,[],[6,965,7,22])).
% 58.49/58.63 cnf(973,plain,
% 58.49/58.63 (P2(f2(f1(f2(x9731,x9732)),f2(f1(f2(f1(x9732),x9733)),f2(x9731,f2(x9734,x9733)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,965,134,7,22,9])).
% 58.49/58.63 cnf(980,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(x9801),x9802)),f2(f1(f2(x9803,x9801)),f2(x9803,f2(x9804,x9802)))))),
% 58.49/58.63 inference(scs_inference,[],[6,973,7,22])).
% 58.49/58.63 cnf(982,plain,
% 58.49/58.63 (P2(f2(f1(x9821),f2(f1(f2(f1(x9821),x9822)),f2(x9823,f2(x9824,x9822)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,973,7,22,9])).
% 58.49/58.63 cnf(985,plain,
% 58.49/58.63 (P2(f2(f1(f2(x9851,x9852)),f2(x9851,f2(f1(f2(f1(x9852),x9853)),f2(x9854,f2(x9855,x9853))))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,973,7,22,9,28])).
% 58.49/58.63 cnf(991,plain,
% 58.49/58.63 (P2(f2(f1(x9911),f2(f1(f2(f1(f2(x9912,x9911)),x9913)),f2(x9914,f2(x9915,x9913)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,982,985,7,22,9])).
% 58.49/58.63 cnf(996,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(f2(x9961,x9962)),x9963)),f2(f1(x9962),f2(x9964,f2(x9965,x9963)))))),
% 58.49/58.63 inference(scs_inference,[],[6,991,7,22])).
% 58.49/58.63 cnf(998,plain,
% 58.49/58.63 (P2(f2(f1(f2(x9981,x9982)),f2(f1(f2(f1(x9982),x9983)),f2(x9984,f2(x9981,x9983)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,991,175,7,22,9])).
% 58.49/58.63 cnf(1004,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(x10041),x10042)),f2(f1(f2(x10043,x10041)),f2(x10044,f2(x10043,x10042)))))),
% 58.49/58.63 inference(scs_inference,[],[6,998,7,22])).
% 58.49/58.63 cnf(1006,plain,
% 58.49/58.63 (P2(f2(f1(x10061),f2(f1(f2(x10062,x10063)),f2(f1(f2(f1(x10061),x10064)),f2(x10062,x10064)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,998,183,7,22,9])).
% 58.49/58.63 cnf(1012,plain,
% 58.49/58.63 (P2(f2(f1(f2(x10121,x10122)),f2(f1(x10123),f2(f1(f2(f1(x10123),x10124)),f2(x10121,x10124)))))),
% 58.49/58.63 inference(scs_inference,[],[6,1006,7,22])).
% 58.49/58.63 cnf(1014,plain,
% 58.49/58.63 (P2(f2(f1(f2(x10141,x10142)),f2(x10141,f2(f1(f2(f1(f2(x10143,x10142)),f2(x10144,x10145))),f2(x10144,x10145)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,1006,219,7,22,9])).
% 58.49/58.63 cnf(1022,plain,
% 58.49/58.63 (P2(f2(f1(x10221),f2(x10222,f2(f1(f2(f1(f2(x10223,x10221)),f2(x10224,x10225))),f2(x10224,x10225)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,1014,7,22,9])).
% 58.49/58.63 cnf(1029,plain,
% 58.49/58.63 (P2(f2(f1(x10291),f2(f1(x10292),f2(f1(f2(f1(x10292),x10293)),f2(x10294,x10293)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,1012,1022,7,22,9])).
% 58.49/58.63 cnf(1036,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(x10361),x10362)),f2(x10363,f2(f1(f2(x10361,x10361)),f2(x10364,x10362)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,1029,445,7,22,9])).
% 58.49/58.63 cnf(1044,plain,
% 58.49/58.63 (P2(f2(f1(f2(x10441,x10441)),f2(x10442,f2(f1(f2(f1(x10441),x10443)),f2(x10444,x10443)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,1036,454,7,22,9])).
% 58.49/58.63 cnf(1052,plain,
% 58.49/58.63 (P2(f2(f1(x10521),f2(x10522,f2(f1(f2(f1(x10521),x10523)),f2(x10524,x10523)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,1044,7,22,9])).
% 58.49/58.63 cnf(1056,plain,
% 58.49/58.63 (P2(f2(f1(f2(x10561,x10562)),f2(x10561,f2(x10563,f2(f1(f2(f1(x10562),x10564)),f2(x10565,x10564))))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,1044,7,22,9,28])).
% 58.49/58.63 cnf(1062,plain,
% 58.49/58.63 (P2(f2(f1(x10621),f2(x10622,f2(x10623,f2(f1(f2(f1(x10621),x10624)),f2(x10625,x10624))))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,1052,1056,7,22,9])).
% 58.49/58.63 cnf(1069,plain,
% 58.49/58.63 (P2(f2(f1(f2(x10691,x10692)),f2(x10693,f2(x10691,f2(x10694,x10692)))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,1062,513,7,22,9])).
% 58.49/58.63 cnf(1073,plain,
% 58.49/58.63 (P2(f2(f1(f2(x10731,f2(x10732,x10733))),f2(x10731,f2(x10734,f2(x10732,f2(x10735,x10733))))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,1062,513,7,22,9,28])).
% 58.49/58.63 cnf(1077,plain,
% 58.49/58.63 (P2(f2(x10771,f2(f1(f2(x10772,x10773)),f2(x10772,f2(x10774,x10773)))))),
% 58.49/58.63 inference(scs_inference,[],[6,1069,7,22])).
% 58.49/58.63 cnf(1079,plain,
% 58.49/58.63 (P2(f2(f1(f2(x10791,x10792)),f2(x10793,f2(x10794,f2(x10791,f2(x10795,x10792))))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,1069,1073,7,22,9])).
% 58.49/58.63 cnf(1102,plain,
% 58.49/58.63 (P2(f2(f1(f2(x11021,x11022)),f2(x11023,f2(x11021,f2(x11024,f2(x11025,x11022))))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,834,570,7,22,9])).
% 58.49/58.63 cnf(1110,plain,
% 58.49/58.63 (P2(f2(f1(x11101),f2(x11102,f2(f1(f2(f1(x11101),x11103)),f2(x11104,f2(x11105,x11103))))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,1102,985,7,22,9])).
% 58.49/58.63 cnf(1117,plain,
% 58.49/58.63 (P2(f2(f1(x11171),f2(f1(f2(x11172,f2(f1(f2(x11173,x11171)),x11174))),f2(x11172,x11174))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,1110,56,7,22,9])).
% 58.49/58.63 cnf(1124,plain,
% 58.49/58.63 (P2(f2(f1(x11241),f2(f1(f2(f1(f2(x11242,x11241)),f2(x11243,x11244))),f2(x11243,x11244))))),
% 58.49/58.63 inference(scs_inference,[],[1,6,1117,141,7,22,9])).
% 58.49/58.63 cnf(1129,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(f2(x11291,x11292)),f2(x11293,x11294))),f2(f1(x11292),f2(x11293,x11294))))),
% 58.49/58.63 inference(scs_inference,[],[6,1124,7,22])).
% 58.49/58.63 cnf(1190,plain,
% 58.49/58.63 (P2(f2(x11901,f2(f1(f2(x11901,x11902)),f2(x11903,f2(x11904,x11902)))))),
% 58.49/58.63 inference(scs_inference,[],[6,563,7,22])).
% 58.49/58.63 cnf(1237,plain,
% 58.49/58.63 (P2(f2(f1(f2(f2(f1(f2(x12371,x12372)),f2(x12373,x12374)),f2(f1(f2(x12371,x12372)),f2(x12373,x12374)))),f2(f1(x12372),f2(x12373,x12374))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,1129,7,9])).
% 58.49/58.63 cnf(1248,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(x12481),f2(f1(x12482),x12483))),f2(f1(f2(x12482,x12482)),f2(f1(f2(x12484,x12481)),f2(x12484,x12483)))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,4,1237,201,7,8,9,22])).
% 58.49/58.63 cnf(1263,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(x12631),x12632)),f2(f1(f2(x12633,x12633)),f2(f1(f2(f1(x12633),x12631)),f2(x12634,x12632)))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,963,7,9,22])).
% 58.49/58.63 cnf(1270,plain,
% 58.49/58.63 (P2(f2(f1(f2(x12701,x12702)),f2(f1(f2(f2(f1(x12702),x12703),f2(f1(x12702),x12703))),f2(x12701,f2(x12704,x12703)))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,980,7,9,22])).
% 58.49/58.63 cnf(1277,plain,
% 58.49/58.63 (P2(f2(f1(f2(x12771,x12772)),f2(f1(f2(f2(f1(x12772),x12773),f2(f1(x12772),x12773))),f2(x12774,f2(x12771,x12773)))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,1004,7,9,22])).
% 58.49/58.63 cnf(1281,plain,
% 58.49/58.63 (P2(f2(f1(f2(x12811,x12811)),f2(f1(f2(f1(x12811),x12812)),f2(x12813,f2(x12814,x12812)))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,1190,7,9])).
% 58.49/58.63 cnf(1291,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(x12911),x12912)),f2(f1(f2(f2(x12911,x12911),f2(x12911,x12911))),f2(x12913,f2(x12914,x12912)))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,1281,7,9,22])).
% 58.49/58.63 cnf(1351,plain,
% 58.49/58.63 (P2(f2(f1(f2(f2(x13511,x13511),f2(x13511,x13511))),f2(f1(f2(f1(x13511),x13512)),f2(x13513,x13512))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,447,7,9])).
% 58.49/58.63 cnf(1356,plain,
% 58.49/58.63 (P2(f2(x13561,f2(f1(f2(f2(x13561,x13562),f2(x13561,x13562))),x13562)))),
% 58.49/58.63 inference(scs_inference,[],[2,22,7])).
% 58.49/58.63 cnf(1357,plain,
% 58.49/58.63 (P2(f2(f1(f2(f2(x13571,x13572),f2(x13571,x13572))),f2(x13571,x13572)))),
% 58.49/58.63 inference(scs_inference,[],[1356,22])).
% 58.49/58.63 cnf(1361,plain,
% 58.49/58.63 (P2(f2(f1(f2(f2(f2(x13611,x13611),f2(x13611,x13611)),f2(f2(x13611,x13611),f2(x13611,x13611)))),f2(f1(f2(f1(x13611),x13612)),f2(x13613,x13612))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,1351,1356,22,7,9])).
% 58.49/58.63 cnf(1364,plain,
% 58.49/58.63 (P2(f2(f1(f2(x13641,f2(f2(x13642,x13643),f2(x13642,x13643)))),f2(x13641,f2(x13642,x13643))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,1351,1356,22,7,9,28])).
% 58.49/58.63 cnf(1373,plain,
% 58.49/58.63 (P2(f2(f1(f2(x13731,f2(f2(f2(x13732,x13733),f2(x13732,x13733)),f2(f2(x13732,x13733),f2(x13732,x13733))))),f2(x13731,f2(x13732,x13733))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,1357,1364,22,7,9,28])).
% 58.49/58.63 cnf(1391,plain,
% 58.49/58.63 (P2(f2(f1(f2(x13911,x13911)),f2(f1(f2(f1(f2(x13912,x13911)),f2(x13913,x13914))),f2(x13913,x13914))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,1124,7,9])).
% 58.49/58.63 cnf(1394,plain,
% 58.49/58.63 (P2(f2(f1(f2(x13941,f2(x13942,x13942))),f2(x13941,f2(f1(f2(f1(f2(x13943,x13942)),f2(x13944,x13945))),f2(x13944,x13945)))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,1124,7,9,28])).
% 58.49/58.63 cnf(1396,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(f2(x13961,x13962)),f2(x13963,x13964))),f2(f1(f2(x13962,x13962)),f2(x13963,x13964))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,1124,7,9,28,22])).
% 58.49/58.63 cnf(1404,plain,
% 58.49/58.63 (P2(f2(f1(f2(f2(x14041,x14041),f2(x14041,x14041))),f2(f1(f2(f1(f2(x14042,x14041)),f2(x14043,x14044))),f2(x14043,x14044))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,1391,1396,1394,28,22,7,9])).
% 58.49/58.63 cnf(1411,plain,
% 58.49/58.63 (P2(f2(f1(f2(f2(f2(x14111,x14111),f2(x14111,x14111)),f2(f2(x14111,x14111),f2(x14111,x14111)))),f2(f1(f2(f1(f2(x14112,x14111)),f2(x14113,x14114))),f2(x14113,x14114))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,1404,22,7,9])).
% 58.49/58.63 cnf(1426,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(f2(x14261,f2(x14262,x14263))),x14264)),f2(f1(f2(x14263,x14263)),f2(x14265,x14264))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,537,7,9,22])).
% 58.49/58.63 cnf(1433,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(x14331),f2(x14332,f2(x14333,x14334)))),f2(f1(f2(x14331,x14331)),f2(x14333,f2(x14332,x14334)))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,73,7,9,22])).
% 58.49/58.63 cnf(1440,plain,
% 58.49/58.63 (P2(f2(f1(f2(x14401,f2(f1(x14402),f2(x14403,x14404)))),f2(f1(f2(x14402,x14402)),f2(x14403,f2(x14401,x14404)))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,81,7,9,22])).
% 58.49/58.63 cnf(1447,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(x14471),f2(x14472,x14473))),f2(f1(f2(f2(x14474,x14471),f2(x14474,x14471))),f2(x14472,f2(x14474,x14473)))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,104,7,9,22])).
% 58.49/58.63 cnf(1454,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(x14541),f2(x14542,x14543))),f2(f1(f2(x14541,x14541)),f2(f1(f2(f1(x14543),x14544)),f2(x14542,x14544)))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,179,7,9,22])).
% 58.49/58.63 cnf(1461,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(x14611),f2(f1(x14612),x14613))),f2(f1(f2(x14611,x14611)),f2(f1(f2(x14614,x14612)),f2(x14614,x14613)))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,186,7,9,22])).
% 58.49/58.63 cnf(1468,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(x14681),f2(f1(x14682),x14683))),f2(f1(f2(x14681,x14681)),f2(f1(f2(x14682,x14682)),f2(x14684,x14683)))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,456,7,9,22])).
% 58.49/58.63 cnf(1479,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(x14791),f2(x14792,x14792))),f2(f1(f2(x14791,x14791)),f2(f1(f2(f1(x14792),x14793)),f2(x14794,x14793)))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,4,1361,524,7,8,9,22])).
% 58.49/58.63 cnf(1489,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(f2(x14891,x14892)),f2(x14893,f2(x14894,x14895)))),f2(f1(f2(x14892,x14892)),f2(x14894,f2(x14893,x14895)))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,4,1373,547,7,8,9,22])).
% 58.49/58.63 cnf(1496,plain,
% 58.49/58.63 (P2(f2(f1(f2(x14961,f2(f1(f2(x14962,x14963)),f2(x14964,x14965)))),f2(f1(f2(x14963,x14963)),f2(x14964,f2(x14961,x14965)))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,556,7,9,22])).
% 58.49/58.63 cnf(1531,plain,
% 58.49/58.63 (P2(f2(f1(f2(x15311,f2(f1(x15312),x15313))),f2(f1(f2(x15312,x15312)),f2(x15311,f2(x15314,x15313)))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,565,7,9,22])).
% 58.49/58.63 cnf(1542,plain,
% 58.49/58.63 (P2(f2(f1(f2(x15421,x15421)),f2(f1(f2(f1(x15421),f2(x15422,x15423))),f2(x15422,f2(x15424,x15423)))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,605,7,9])).
% 58.49/58.63 cnf(1552,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(x15521),f2(x15522,x15523))),f2(f1(f2(f2(x15521,x15521),f2(x15521,x15521))),f2(x15522,f2(x15524,x15523)))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,1542,7,9,22])).
% 58.49/58.63 cnf(1578,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(x15781),x15782)),f2(f1(f2(f2(x15783,x15781),f2(x15783,x15781))),f2(x15784,f2(x15783,x15782)))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,998,7,9,22])).
% 58.49/58.63 cnf(1646,plain,
% 58.49/58.63 (P2(f2(f1(f2(f2(x16461,x16462),f2(x16461,x16462))),f2(x16463,f2(x16461,f2(x16464,x16462)))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,1069,7,9])).
% 58.49/58.63 cnf(1651,plain,
% 58.49/58.63 (P2(f2(f1(f2(x16511,x16512)),f2(x16511,f2(f1(f2(f2(x16513,x16514),f2(x16513,x16514))),f2(x16513,f2(x16515,x16514))))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,1069,7,9,22,28])).
% 58.49/58.63 cnf(1657,plain,
% 58.49/58.63 (P2(f2(f1(f2(f2(f2(x16571,x16572),f2(x16571,x16572)),f2(f2(x16571,x16572),f2(x16571,x16572)))),f2(x16573,f2(x16571,f2(x16574,x16572)))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,1646,1651,22,7,9])).
% 58.49/58.63 cnf(1664,plain,
% 58.49/58.63 (P2(f2(f1(f2(x16641,x16641)),f2(x16642,f2(f1(f2(f1(f2(x16643,x16641)),x16644)),f2(x16645,x16644)))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,1657,720,22,7,9])).
% 58.49/58.63 cnf(1671,plain,
% 58.49/58.63 (P2(f2(f1(f2(x16711,x16711)),f2(f1(f2(f1(f2(x16712,x16711)),x16713)),f2(x16714,f2(x16715,x16713)))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,1664,991,22,7,9])).
% 58.49/58.63 cnf(1674,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(f2(x16741,x16742)),x16743)),f2(f1(f2(x16742,x16742)),f2(x16744,f2(x16745,x16743)))))),
% 58.49/58.63 inference(scs_inference,[],[1671,22])).
% 58.49/58.63 cnf(1678,plain,
% 58.49/58.63 (P2(f2(f1(f2(x16781,x16781)),f2(f1(f2(f1(x16781),f2(x16782,x16783))),f2(x16782,f2(x16784,f2(x16785,x16783))))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,1671,780,22,7,9])).
% 58.49/58.63 cnf(1681,plain,
% 58.49/58.63 (P2(f2(f1(f2(f1(x16811),f2(x16812,x16813))),f2(f1(f2(x16811,x16811)),f2(x16812,f2(x16814,f2(x16815,x16813))))))),
% 58.49/58.63 inference(scs_inference,[],[1678,22])).
% 58.49/58.63 cnf(1685,plain,
% 58.49/58.63 (P2(f2(f1(f2(x16851,x16851)),f2(x16852,f2(x16853,f2(f1(f2(f1(x16851),x16854)),f2(x16855,x16854))))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,1678,1062,22,7,9])).
% 58.49/58.63 cnf(1696,plain,
% 58.49/58.63 (P2(f2(f1(f2(f2(x16961,x16962),f2(x16961,x16962))),f2(x16963,f2(x16964,f2(x16961,f2(x16965,x16962))))))),
% 58.49/58.63 inference(scs_inference,[],[2,6,4,1411,1685,1079,22,7,8,9])).
% 58.49/58.63 cnf(1703,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x17031,x17032),f2(x17031,x17032))),f2(x17033,f2(x17031,f2(x17034,f2(x17035,x17032))))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1696,1102,22,7,9])).
% 58.49/58.64 cnf(1710,plain,
% 58.49/58.64 (P2(f2(f1(f2(x17101,x17101)),f2(x17102,f2(f1(f2(f1(x17101),x17103)),f2(x17104,f2(x17105,x17103))))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1703,1110,22,7,9])).
% 58.49/58.64 cnf(1717,plain,
% 58.49/58.64 (P2(f2(f1(f2(x17171,x17171)),f2(x17172,f2(x17173,f2(x17174,f2(x17175,x17171))))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1710,841,22,7,9])).
% 58.49/58.64 cnf(1724,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x17241,x17241),f2(x17241,x17241))),f2(x17242,f2(x17243,f2(x17244,f2(x17245,x17241))))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1717,22,7,9])).
% 58.49/58.64 cnf(1731,plain,
% 58.49/58.64 (P2(f2(f1(f2(x17311,x17311)),f2(x17312,x17311)))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1724,497,22,7,9])).
% 58.49/58.64 cnf(1734,plain,
% 58.49/58.64 (P2(f2(f1(f2(x17341,f2(x17342,x17342))),f2(x17341,f2(x17343,x17342))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1724,497,22,7,9,28])).
% 58.49/58.64 cnf(1736,plain,
% 58.49/58.64 (P2(f2(f1(f2(x17361,f2(x17362,f2(x17363,x17363)))),f2(x17361,f2(x17362,f2(x17364,x17363)))))),
% 58.49/58.64 inference(scs_inference,[],[1734,28])).
% 58.49/58.64 cnf(1738,plain,
% 58.49/58.64 (P2(f2(x17381,f2(f1(f2(x17382,x17382)),x17382)))),
% 58.49/58.64 inference(scs_inference,[],[1731,1734,28,22])).
% 58.49/58.64 cnf(1742,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x17421,x17421),f2(x17421,x17421))),f2(x17422,x17421)))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1731,1734,28,22,7,9])).
% 58.49/58.64 cnf(1745,plain,
% 58.49/58.64 (P2(f2(f1(f2(x17451,f2(f2(x17452,x17452),f2(x17452,x17452)))),f2(x17451,f2(x17453,x17452))))),
% 58.49/58.64 inference(scs_inference,[],[1742,28])).
% 58.49/58.64 cnf(1751,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(f2(x17511,x17511),f2(x17511,x17511)),f2(f2(x17511,x17511),f2(x17511,x17511)))),f2(x17512,x17511)))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1742,28,22,7,9])).
% 58.49/58.64 cnf(1754,plain,
% 58.49/58.64 (P2(f2(f1(f2(x17541,f2(f2(f2(x17542,x17542),f2(x17542,x17542)),f2(f2(x17542,x17542),f2(x17542,x17542))))),f2(x17541,f2(x17543,x17542))))),
% 58.49/58.64 inference(scs_inference,[],[1751,28])).
% 58.49/58.64 cnf(1760,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x17601,f2(x17602,x17602)),f2(x17601,f2(x17602,x17602)))),f2(x17601,f2(x17603,x17602))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1751,1745,1734,28,22,7,9])).
% 58.49/58.64 cnf(1763,plain,
% 58.49/58.64 (P2(f2(f1(f2(x17631,x17632)),f2(x17631,f2(f1(f2(x17633,x17633)),x17633))))),
% 58.49/58.64 inference(scs_inference,[],[1738,28])).
% 58.49/58.64 cnf(1773,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(f2(x17731,x17732),f2(x17731,x17732)),f2(f2(x17731,x17732),f2(x17731,x17732)))),f2(f1(f2(f1(x17732),x17733)),f2(x17731,x17733))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,4,1754,1760,1738,265,28,22,7,8,9])).
% 58.49/58.64 cnf(1776,plain,
% 58.49/58.64 (P2(f2(x17761,f2(f1(f2(x17761,f2(x17762,f2(x17763,x17763)))),f2(x17762,f2(x17764,x17763)))))),
% 58.49/58.64 inference(scs_inference,[],[1736,22])).
% 58.49/58.64 cnf(1780,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x17801,x17802),f2(x17801,x17802))),f2(x17801,f2(f1(f2(x17803,x17803)),x17803))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1736,1763,22,7,9])).
% 58.49/58.64 cnf(1787,plain,
% 58.49/58.64 (P2(f2(f1(f2(x17871,x17871)),f2(f1(f2(f1(x17871),f2(x17872,f2(x17873,x17873)))),f2(x17872,f2(x17874,x17873)))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1776,1780,22,7,9])).
% 58.49/58.64 cnf(1790,plain,
% 58.49/58.64 (P2(f2(f1(f2(f1(x17901),f2(x17902,f2(x17903,x17903)))),f2(f1(f2(x17901,x17901)),f2(x17902,f2(x17904,x17903)))))),
% 58.49/58.64 inference(scs_inference,[],[1787,22])).
% 58.49/58.64 cnf(1794,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x17941,x17942),f2(x17941,x17942))),f2(f1(f2(f1(f2(x17941,f2(x17943,x17942))),f2(x17944,x17945))),f2(x17944,x17945))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1787,871,22,7,9])).
% 58.49/58.64 cnf(1801,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x18011,x18012),f2(x18011,x18012))),f2(x18011,f2(x18013,x18012))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1794,504,22,7,9])).
% 58.49/58.64 cnf(1804,plain,
% 58.49/58.64 (P2(f2(f1(f2(x18041,f2(f2(x18042,x18043),f2(x18042,x18043)))),f2(x18041,f2(x18042,f2(x18044,x18043)))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1794,504,22,7,9,28])).
% 58.49/58.64 cnf(1810,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(f2(x18101,x18102),f2(x18101,x18102)),f2(f2(x18101,x18102),f2(x18101,x18102)))),f2(x18101,f2(x18103,x18102))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1801,22,7,9])).
% 58.49/58.64 cnf(1821,plain,
% 58.49/58.64 (P2(f2(f1(f2(x18211,x18211)),f2(f1(f2(f1(f2(x18212,f2(x18213,x18211))),f2(x18214,x18215))),f2(x18214,x18215))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,4,1773,1810,879,22,7,8,9])).
% 58.49/58.64 cnf(1828,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x18281,x18281),f2(x18281,x18281))),f2(f1(f2(f1(f2(x18282,f2(x18283,x18281))),f2(x18284,x18285))),f2(x18284,x18285))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1821,22,7,9])).
% 58.49/58.64 cnf(1835,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(f1(x18351),f2(x18352,x18353)),f2(f1(x18351),f2(x18352,x18353)))),f2(x18352,f2(f1(f2(x18354,x18351)),f2(x18354,x18353)))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1828,190,22,7,9])).
% 58.49/58.64 cnf(1842,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x18421,x18422),f2(x18421,x18422))),f2(x18421,f2(f1(f2(f1(f2(x18423,x18422)),f2(x18424,x18425))),f2(x18424,x18425)))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1835,1014,22,7,9])).
% 58.49/58.64 cnf(1849,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x18491,f2(x18492,x18493)),f2(x18491,f2(x18492,x18493)))),f2(x18491,f2(x18492,f2(x18494,x18493)))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1804,513,22,7,9])).
% 58.49/58.64 cnf(1856,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x18561,x18562),f2(x18561,x18562))),f2(f1(f2(f1(x18562),x18563)),f2(x18561,f2(x18564,x18563)))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1849,973,22,7,9])).
% 58.49/58.64 cnf(1859,plain,
% 58.49/58.64 (P2(f2(f1(f2(f1(x18591),x18592)),f2(f1(f2(f2(x18593,x18591),f2(x18593,x18591))),f2(x18593,f2(x18594,x18592)))))),
% 58.49/58.64 inference(scs_inference,[],[1856,22])).
% 58.49/58.64 cnf(1863,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x18631,x18631),f2(x18631,x18631))),f2(x18632,f2(f1(f2(f1(x18631),x18633)),f2(x18634,x18633)))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1856,1044,22,7,9])).
% 58.49/58.64 cnf(1870,plain,
% 58.49/58.64 (P2(f2(f1(f2(x18701,x18701)),f2(x18702,f2(f1(f2(f1(f2(x18703,x18701)),f2(x18704,x18705))),f2(x18704,x18705)))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1863,1022,22,7,9])).
% 58.49/58.64 cnf(1877,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x18771,x18771),f2(x18771,x18771))),f2(x18772,f2(f1(f2(f1(f2(x18773,x18771)),f2(x18774,x18775))),f2(x18774,x18775)))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1842,1870,22,7,9])).
% 58.49/58.64 cnf(1884,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x18841,x18842),f2(x18841,x18842))),f2(x18841,f2(x18843,f2(x18844,x18842)))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1877,563,22,7,9])).
% 58.49/58.64 cnf(1891,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(f2(x18911,x18912),f2(x18911,x18912)),f2(f2(x18911,x18912),f2(x18911,x18912)))),f2(x18911,f2(x18913,f2(x18914,x18912)))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1884,22,7,9])).
% 58.49/58.64 cnf(1898,plain,
% 58.49/58.64 (P2(f2(f1(f2(x18981,x18981)),f2(x18982,f2(x18983,f2(x18984,x18981)))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1891,519,22,7,9])).
% 58.49/58.64 cnf(1907,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x19071,x19071),f2(x19071,x19071))),f2(x19072,f2(x19073,f2(x19074,x19071)))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1898,22,7,9])).
% 58.49/58.64 cnf(1910,plain,
% 58.49/58.64 (P2(f2(f1(f2(x19101,x19102)),f2(x19101,f2(f1(f2(x19103,x19103)),f2(x19104,f2(x19105,x19103))))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1898,22,7,9,28])).
% 58.49/58.64 cnf(1916,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(f2(x19161,x19161),f2(x19161,x19161)),f2(f2(x19161,x19161),f2(x19161,x19161)))),f2(x19162,f2(x19163,f2(x19164,x19161)))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1907,22,7,9])).
% 58.49/58.64 cnf(1919,plain,
% 58.49/58.64 (P2(f2(f1(f2(x19191,x19192)),f2(x19191,f2(f1(f2(f2(x19193,x19193),f2(x19193,x19193))),f2(x19194,f2(x19195,x19193))))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1907,22,7,9,28])).
% 58.49/58.64 cnf(1925,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x19251,x19252),f2(x19251,x19252))),f2(x19251,f2(f1(f2(x19253,x19253)),f2(x19254,f2(x19255,x19253))))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1916,1910,22,7,9])).
% 58.49/58.64 cnf(1933,plain,
% 58.49/58.64 (P2(f2(f1(f2(x19331,x19331)),f2(x19332,f2(f1(f2(f1(x19331),f2(x19333,x19334))),f2(x19333,f2(x19335,x19334))))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1919,755,22,7,9])).
% 58.49/58.64 cnf(1940,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x19401,x19402),f2(x19401,x19402))),f2(x19401,f2(x19403,f2(x19404,f2(x19405,x19402))))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1925,526,22,7,9])).
% 58.49/58.64 cnf(1947,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x19471,f2(x19472,x19473)),f2(x19471,f2(x19472,x19473)))),f2(x19472,f2(x19471,x19473))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1933,57,22,7,9])).
% 58.49/58.64 cnf(1954,plain,
% 58.49/58.64 (P2(f2(f1(f2(x19541,x19541)),f2(f1(f2(f1(x19541),f2(x19542,x19543))),f2(x19542,x19543))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1947,141,22,7,9])).
% 58.49/58.64 cnf(1957,plain,
% 58.49/58.64 (P2(f2(f1(f2(x19571,f2(x19572,x19572))),f2(x19571,f2(f1(f2(f1(x19572),f2(x19573,x19574))),f2(x19573,x19574)))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1947,141,22,7,9,28])).
% 58.49/58.64 cnf(1959,plain,
% 58.49/58.64 (P2(f2(f1(f2(f1(x19591),f2(x19592,x19593))),f2(f1(f2(x19591,x19591)),f2(x19592,x19593))))),
% 58.49/58.64 inference(scs_inference,[],[1954,22])).
% 58.49/58.64 cnf(1963,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x19631,x19631),f2(x19631,x19631))),f2(f1(f2(f1(x19631),f2(x19632,x19633))),f2(x19632,x19633))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1954,22,7,9])).
% 58.49/58.64 cnf(1968,plain,
% 58.49/58.64 (P2(f2(f1(f2(f1(x19681),f2(x19682,x19683))),f2(f1(f2(f2(x19681,x19681),f2(x19681,x19681))),f2(x19682,x19683))))),
% 58.49/58.64 inference(scs_inference,[],[1963,22])).
% 58.49/58.64 cnf(1972,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(f2(x19721,x19721),f2(x19721,x19721)),f2(f2(x19721,x19721),f2(x19721,x19721)))),f2(f1(f2(f1(x19721),f2(x19722,x19723))),f2(x19722,x19723))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1963,22,7,9])).
% 58.49/58.64 cnf(1982,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(f1(x19821),f2(x19822,x19823)),f2(f1(x19821),f2(x19822,x19823)))),f2(f1(f2(f2(x19821,x19821),f2(x19821,x19821))),f2(x19822,x19823))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,4,1972,1968,1957,22,7,8,9])).
% 58.49/58.64 cnf(1996,plain,
% 58.49/58.64 (P2(f2(f1(f2(x19961,x19961)),f2(f1(f2(f1(f2(x19962,x19961)),x19963)),f2(x19964,x19963))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1940,528,22,7,9])).
% 58.49/58.64 cnf(2003,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x20031,x20031),f2(x20031,x20031))),f2(f1(f2(f1(f2(x20032,x20031)),x20033)),f2(x20034,x20033))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,1996,22,7,9])).
% 58.49/58.64 cnf(2010,plain,
% 58.49/58.64 (P2(f2(f1(f2(x20101,x20101)),f2(x20102,f2(x20103,x20101))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,2003,510,22,7,9])).
% 58.49/58.64 cnf(2013,plain,
% 58.49/58.64 (P2(f2(f1(f2(x20131,f2(x20132,x20132))),f2(x20131,f2(x20133,f2(x20134,x20132)))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,2003,510,22,7,9,28])).
% 58.49/58.64 cnf(2019,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x20191,x20191),f2(x20191,x20191))),f2(x20192,f2(x20193,x20191))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,2010,22,7,9])).
% 58.49/58.64 cnf(2022,plain,
% 58.49/58.64 (P2(f2(f1(f2(x20221,x20222)),f2(x20221,f2(f1(f2(x20223,x20223)),f2(x20224,x20223)))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,2010,22,7,9,28])).
% 58.49/58.64 cnf(2026,plain,
% 58.49/58.64 (P2(f2(x20261,f2(f1(f2(f2(x20262,x20262),f2(x20262,x20262))),f2(x20263,x20262))))),
% 58.49/58.64 inference(scs_inference,[],[2019,28,22])).
% 58.49/58.64 cnf(2030,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(f2(x20301,x20301),f2(x20301,x20301)),f2(f2(x20301,x20301),f2(x20301,x20301)))),f2(x20302,f2(x20303,x20301))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,2019,28,22,7,9])).
% 58.49/58.64 cnf(2033,plain,
% 58.49/58.64 (P2(f2(f1(f2(x20331,x20332)),f2(x20331,f2(f1(f2(f2(x20333,x20333),f2(x20333,x20333))),f2(x20334,x20333)))))),
% 58.49/58.64 inference(scs_inference,[],[2026,28])).
% 58.49/58.64 cnf(2040,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x20401,f2(x20402,x20402)),f2(x20401,f2(x20402,x20402)))),f2(x20401,f2(x20403,f2(x20404,x20402)))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,2030,2026,2013,28,22,7,9])).
% 58.49/58.64 cnf(2049,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x20491,x20492),f2(x20491,x20492))),f2(x20491,f2(f1(f2(f2(x20493,x20493),f2(x20493,x20493))),f2(x20494,x20493)))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,2040,2033,2022,28,22,7,9])).
% 58.49/58.64 cnf(2060,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x20601,x20602),f2(x20601,x20602))),f2(x20601,f2(f1(f2(x20603,x20603)),f2(x20604,x20603)))))),
% 58.49/58.64 inference(scs_inference,[],[2,6,4,1982,2049,2022,22,7,8,9])).
% 58.49/58.64 cnf(2186,plain,
% 58.49/58.64 (P2(f2(f1(f2(x21861,f1(f2(x21862,f2(x21863,x21864))))),f2(f1(f2(x21864,x21864)),f2(x21865,x21861))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,1426,2060,22,7,9])).
% 58.49/58.64 cnf(2194,plain,
% 58.49/58.64 (P2(f2(f1(f2(x21941,f1(f2(x21942,f2(x21943,x21944))))),f2(f1(x21944),f2(x21945,x21941))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2186,545,7,22,9])).
% 58.49/58.64 cnf(2202,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x22021,x22022),f1(x22023))),f2(f1(f2(f2(x22024,x22023),f2(x22024,x22023))),f2(x22021,f2(x22024,x22022)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2194,1447,22,7,9])).
% 58.49/58.64 cnf(2209,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x22091,x22092),f1(x22093))),f2(f1(f2(f2(x22093,x22093),f2(x22093,x22093))),f2(x22091,f2(x22094,x22092)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,1552,2202,7,22,9])).
% 58.49/58.64 cnf(2216,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(f1(x22161),x22162),f1(x22163))),f2(f1(f2(x22161,x22161)),f2(f1(f2(x22164,x22163)),f2(x22164,x22162)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2209,1248,22,7,9])).
% 58.49/58.64 cnf(2223,plain,
% 58.49/58.64 (P2(f2(f1(f2(x22231,x22232)),f2(f1(f2(f2(f1(x22231),x22233),f2(f1(x22231),x22233))),f2(x22232,f2(x22234,x22233)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,1270,2216,7,22,9])).
% 58.49/58.64 cnf(2230,plain,
% 58.49/58.64 (P2(f2(f1(f2(x22301,x22302)),f2(f1(f2(f2(f1(x22301),x22303),f2(f1(x22301),x22303))),f2(x22304,f2(x22302,x22303)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,1277,2223,22,7,9])).
% 58.49/58.64 cnf(2237,plain,
% 58.49/58.64 (P2(f2(f1(f2(x22371,f1(x22372))),f2(f1(f2(f2(x22372,x22372),f2(x22372,x22372))),f2(x22373,f2(x22374,x22371)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,1291,2230,7,22,9])).
% 58.49/58.64 cnf(2245,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x22451,f2(x22452,x22453)),f1(x22454))),f2(f1(f2(x22454,x22454)),f2(x22452,f2(x22451,x22453)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,1433,2237,22,7,9])).
% 58.49/58.64 cnf(2252,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(f1(x22521),f2(x22522,x22523)),x22524)),f2(f1(f2(x22521,x22521)),f2(x22522,f2(x22524,x22523)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,1440,2245,22,7,9])).
% 58.49/58.64 cnf(2260,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x22601,x22602),f1(x22603))),f2(f1(f2(x22603,x22603)),f2(f1(f2(f1(x22602),x22604)),f2(x22601,x22604)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,1454,2252,22,7,9])).
% 58.49/58.64 cnf(2267,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(f1(x22671),x22672),f1(x22673))),f2(f1(f2(x22673,x22673)),f2(f1(f2(x22674,x22671)),f2(x22674,x22672)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,1461,2260,22,7,9])).
% 58.49/58.64 cnf(2274,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(f1(x22741),x22742),f1(x22743))),f2(f1(f2(x22743,x22743)),f2(f1(f2(x22741,x22741)),f2(x22744,x22742)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,1468,2267,22,7,9])).
% 58.49/58.64 cnf(2277,plain,
% 58.49/58.64 (P2(f2(x22771,f2(f1(f2(x22772,x22771)),x22772)))),
% 58.49/58.64 inference(scs_inference,[],[3,22,7])).
% 58.49/58.64 cnf(2282,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x22821,x22821),f1(x22822))),f2(f1(f2(x22822,x22822)),f2(f1(f2(f1(x22821),x22823)),f2(x22824,x22823)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,1479,2274,22,7,9])).
% 58.49/58.64 cnf(2289,plain,
% 58.49/58.64 (P2(f2(f1(f2(x22891,f1(x22892))),f2(f1(f2(f2(x22893,x22892),f2(x22893,x22892))),f2(x22894,f2(x22893,x22891)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,1578,2282,22,7,9])).
% 58.49/58.64 cnf(2297,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x22971,f2(x22972,x22972)),f1(x22973))),f2(f1(f2(x22973,x22973)),f2(x22971,f2(x22974,x22972)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,1790,2289,22,7,9])).
% 58.49/58.64 cnf(2304,plain,
% 58.49/58.64 (P2(f2(f1(f2(x23041,f1(x23042))),f2(f1(f2(f2(x23043,x23042),f2(x23043,x23042))),f2(x23043,f2(x23044,x23041)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,1859,2297,7,22,9])).
% 58.49/58.64 cnf(2312,plain,
% 58.49/58.64 (P2(f2(f1(f2(x23121,f1(x23122))),f2(f1(f2(x23123,f2(x23124,x23122))),f2(x23123,f2(x23124,x23121)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2304,166,22,7,9])).
% 58.49/58.64 cnf(2318,plain,
% 58.49/58.64 (P2(f2(f1(f2(x23181,x23182)),f2(x23182,x23181)))),
% 58.49/58.64 inference(scs_inference,[],[6,2277,7,22])).
% 58.49/58.64 cnf(2320,plain,
% 58.49/58.64 (P2(f2(f1(f2(x23201,f1(x23202))),f2(f1(f2(f1(x23203),x23202)),f2(f1(f2(x23204,x23203)),f2(x23204,x23201)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,222,2277,7,22,9])).
% 58.49/58.64 cnf(2324,plain,
% 58.49/58.64 (P2(f2(f1(f2(x23241,f2(x23242,x23243))),f2(x23241,f2(x23243,x23242))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,222,2277,7,22,9,28])).
% 58.49/58.64 cnf(2326,plain,
% 58.49/58.64 (P2(f2(f1(f2(x23261,f2(x23262,f2(x23263,x23264)))),f2(x23261,f2(x23262,f2(x23264,x23263)))))),
% 58.49/58.64 inference(scs_inference,[],[2324,28])).
% 58.49/58.64 cnf(2330,plain,
% 58.49/58.64 (P2(f2(x23301,f2(f1(f2(x23301,f2(x23302,x23303))),f2(x23303,x23302))))),
% 58.49/58.64 inference(scs_inference,[],[6,2324,28,7,22])).
% 58.49/58.64 cnf(2332,plain,
% 58.49/58.64 (P2(f2(f1(f2(x23321,x23322)),f2(x23321,x23322)))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2318,2324,28,7,22,9])).
% 58.49/58.64 cnf(2335,plain,
% 58.49/58.64 (P2(f2(f1(f2(x23351,x23352)),f2(x23351,f2(f1(f2(f1(x23352),f2(x23353,x23354))),f2(x23354,x23353)))))),
% 58.49/58.64 inference(scs_inference,[],[2330,28])).
% 58.49/58.64 cnf(2336,plain,
% 58.49/58.64 (P2(f2(x23361,f2(f1(f2(x23361,f2(x23362,x23363))),f2(x23363,x23362))))),
% 58.49/58.64 inference(rename_variables,[],[2330])).
% 58.49/58.64 cnf(2342,plain,
% 58.49/58.64 (P2(f2(f1(f2(x23421,x23422)),f2(f1(f2(f1(f2(x23422,x23421)),f2(x23423,x23424))),f2(x23424,x23423))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2332,2330,2336,28,7,22,9])).
% 58.49/58.64 cnf(2349,plain,
% 58.49/58.64 (P2(f2(f1(f2(f1(f2(x23491,x23492)),f2(x23493,x23494))),f2(f1(f2(x23492,x23491)),f2(x23494,x23493))))),
% 58.49/58.64 inference(scs_inference,[],[6,2342,28,7,22])).
% 58.49/58.64 cnf(2359,plain,
% 58.49/58.64 (P2(f2(f1(f2(x23591,f2(x23592,x23593))),f2(f1(f2(x23594,f1(x23593))),f2(x23591,f2(x23592,x23594)))))),
% 58.49/58.64 inference(scs_inference,[],[6,2349,2312,28,7,22])).
% 58.49/58.64 cnf(2361,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x23611,x23612),f1(f2(x23613,x23614)))),f2(f1(f2(x23614,x23613)),f2(x23612,x23611))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2349,2312,28,7,22,9])).
% 58.49/58.64 cnf(2366,plain,
% 58.49/58.64 (P2(f2(f1(f2(x23661,x23662)),f2(f1(f2(f2(x23663,x23664),f1(f2(x23662,x23661)))),f2(x23664,x23663))))),
% 58.49/58.64 inference(scs_inference,[],[6,2361,7,22])).
% 58.49/58.64 cnf(2368,plain,
% 58.49/58.64 (P2(f2(f1(f2(x23681,f1(x23682))),f2(f1(f2(x23683,x23683)),f2(f1(f2(f1(x23683),x23682)),f2(x23684,x23681)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2361,1263,7,22,9])).
% 58.49/58.64 cnf(2374,plain,
% 58.49/58.64 (P2(f2(f1(f2(f1(x23741),x23742)),f2(f1(f2(x23743,f1(x23742))),f2(f1(f2(x23744,x23741)),f2(x23744,x23743)))))),
% 58.49/58.64 inference(scs_inference,[],[6,2320,7,22])).
% 58.49/58.64 cnf(2376,plain,
% 58.49/58.64 (P2(f2(f1(f2(x23761,x23762)),f2(f1(f2(f2(x23763,x23764),f1(f2(x23761,x23762)))),f2(x23764,x23763))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2366,2320,7,22,9])).
% 58.49/58.64 cnf(2383,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x23831,f2(x23832,x23833)),f1(f2(x23834,x23835)))),f2(f1(f2(x23835,x23835)),f2(x23832,f2(x23831,x23833)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2376,1489,7,22,9])).
% 58.49/58.64 cnf(2388,plain,
% 58.49/58.64 (P2(f2(x23881,f2(f1(f2(x23881,f2(x23882,f2(x23883,x23884)))),f2(x23882,f2(x23884,x23883)))))),
% 58.49/58.64 inference(scs_inference,[],[6,2326,7,22])).
% 58.49/58.64 cnf(2390,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(f1(f2(x23901,x23902)),f2(x23903,x23904)),x23905)),f2(f1(f2(x23902,x23902)),f2(x23903,f2(x23905,x23904)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,1496,2326,7,22,9])).
% 58.49/58.64 cnf(2398,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(f1(x23981),x23982),x23983)),f2(f1(f2(x23981,x23981)),f2(x23983,f2(x23984,x23982)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,1531,2335,7,22,9])).
% 58.49/58.64 cnf(2427,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x24271,x24272),x24273)),f2(f1(f2(x24274,f1(x24272))),f2(x24273,f2(x24271,x24274)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2359,2368,7,22,9])).
% 58.49/58.64 cnf(2435,plain,
% 58.49/58.64 (P2(f2(f1(f2(x24351,f1(x24352))),f2(f1(f2(x24353,f1(x24351))),f2(f1(f2(x24354,x24352)),f2(x24354,x24353)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2374,2383,7,22,9])).
% 58.49/58.64 cnf(2443,plain,
% 58.49/58.64 (P2(f2(f1(f2(x24431,x24432)),f2(f1(f2(f1(f2(x24432,x24431)),f2(x24433,f2(x24434,x24435)))),f2(x24433,f2(x24435,x24434)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2388,2390,7,22,9])).
% 58.49/58.64 cnf(2450,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x24501,x24502),f1(f2(x24503,x24504)))),f2(f1(f2(x24505,x24504)),f2(x24501,f2(x24505,x24502)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2398,971,7,22,9])).
% 58.49/58.64 cnf(2470,plain,
% 58.49/58.64 (P2(f2(f1(f2(x24701,f1(x24702))),f2(f1(f2(f2(x24703,x24702),x24704)),f2(x24704,f2(x24703,x24701)))))),
% 58.49/58.64 inference(scs_inference,[],[6,2427,7,22])).
% 58.49/58.64 cnf(2472,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(f1(x24721),x24722),x24723)),f2(f1(x24721),f2(x24724,f2(x24723,x24722)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2427,652,7,22,9])).
% 58.49/58.64 cnf(2478,plain,
% 58.49/58.64 (P2(f2(f1(f2(x24781,f1(x24782))),f2(f1(f2(x24782,f1(x24783))),f2(f1(f2(x24784,x24783)),f2(x24784,x24781)))))),
% 58.49/58.64 inference(scs_inference,[],[6,2435,7,22])).
% 58.49/58.64 cnf(2480,plain,
% 58.49/58.64 (P2(f2(f1(f2(f1(x24801),x24802)),f2(f1(f2(f2(x24803,x24801),x24804)),f2(x24804,f2(x24803,x24802)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2435,2470,7,22,9])).
% 58.49/58.64 cnf(2486,plain,
% 58.49/58.64 (P2(f2(f1(f2(f1(f2(x24861,x24862)),f2(x24863,f2(x24864,x24865)))),f2(f1(f2(x24862,x24861)),f2(x24863,f2(x24865,x24864)))))),
% 58.49/58.64 inference(scs_inference,[],[6,2443,7,22])).
% 58.49/58.64 cnf(2488,plain,
% 58.49/58.64 (P2(f2(f1(f2(f1(x24881),x24882)),f2(f1(f2(x24881,f1(x24883))),f2(f1(f2(x24884,x24883)),f2(x24884,x24882)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2443,2478,7,22,9])).
% 58.49/58.64 cnf(2496,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x24961,f2(x24962,x24963)),f1(f2(x24964,x24965)))),f2(f1(f2(x24965,x24964)),f2(x24961,f2(x24963,x24962)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2480,2486,7,22,9])).
% 58.49/58.64 cnf(2503,plain,
% 58.49/58.64 (P2(f2(f1(f2(x25031,f1(f2(x25032,x25033)))),f2(f1(f2(x25033,x25033)),f2(x25034,f2(x25035,x25031)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2488,1674,7,22,9])).
% 58.49/58.64 cnf(2509,plain,
% 58.49/58.64 (P2(f2(f1(f2(x25091,x25092)),f2(f1(f2(f2(x25093,f2(x25094,x25095)),f1(f2(x25092,x25091)))),f2(x25093,f2(x25095,x25094)))))),
% 58.49/58.64 inference(scs_inference,[],[6,2496,7,22])).
% 58.49/58.64 cnf(2511,plain,
% 58.49/58.64 (P2(f2(f1(f2(x25111,f1(f2(x25112,x25113)))),f2(f1(x25113),f2(x25114,f2(x25115,x25111)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2496,996,7,22,9])).
% 58.49/58.64 cnf(2517,plain,
% 58.49/58.64 (P2(f2(f1(f2(x25171,x25172)),f2(f1(f2(f2(x25173,x25174),f1(f2(x25175,x25172)))),f2(x25173,f2(x25171,x25174)))))),
% 58.49/58.64 inference(scs_inference,[],[6,2450,7,22])).
% 58.49/58.64 cnf(2519,plain,
% 58.49/58.64 (P2(f2(f1(f2(x25191,x25192)),f2(f1(f2(f2(x25193,f2(x25194,x25195)),f1(f2(x25191,x25192)))),f2(x25193,f2(x25195,x25194)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2509,2450,7,22,9])).
% 58.49/58.64 cnf(2527,plain,
% 58.49/58.64 (P2(f2(f1(f2(x25271,x25272)),f2(f1(f2(f2(x25273,x25274),f1(f2(x25275,x25271)))),f2(x25273,f2(x25272,x25274)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2519,2517,7,22,9])).
% 58.49/58.64 cnf(2541,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x25411,x25412),f1(x25413))),f2(f1(f2(x25413,x25413)),f2(x25411,f2(x25414,f2(x25415,x25412))))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2527,1681,7,22,9])).
% 58.49/58.64 cnf(2563,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(f2(f2(x25631,x25632),f2(x25631,x25632)),f2(f2(x25631,x25632),f2(x25631,x25632))),x25633)),f2(x25633,f2(x25631,x25632))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2472,1373,7,22,9])).
% 58.49/58.64 cnf(2571,plain,
% 58.49/58.64 (P2(f2(x25711,f2(f1(f2(f2(f2(f2(x25712,x25713),f2(x25712,x25713)),f2(f2(x25712,x25713),f2(x25712,x25713))),x25711)),f2(x25712,x25713))))),
% 58.49/58.64 inference(scs_inference,[],[6,4,2563,2503,7,22,8])).
% 58.49/58.64 cnf(2586,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x25861,x25862),f1(x25863))),f2(f1(f2(f2(x25863,x25863),f2(x25863,x25863))),f2(x25861,x25862))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,5,2571,2511,1968,7,22,8,9])).
% 58.49/58.64 cnf(2591,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x25911,x25911),f2(x25911,x25911))),f2(f1(f2(f2(x25912,x25913),f1(x25911))),f2(x25912,x25913))))),
% 58.49/58.64 inference(scs_inference,[],[6,2586,7,22])).
% 58.49/58.64 cnf(2692,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x26921,x26922),f1(x26923))),f2(f1(f2(x26923,x26923)),f2(x26921,x26922))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2541,1959,7,22,9])).
% 58.49/58.64 cnf(2695,plain,
% 58.49/58.64 (P2(f2(f1(f2(x26951,f2(f2(x26952,x26953),f1(x26954)))),f2(x26951,f2(f1(f2(x26954,x26954)),f2(x26952,x26953)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2541,1959,7,22,9,28])).
% 58.49/58.64 cnf(2699,plain,
% 58.49/58.64 (P2(f2(f1(f2(x26991,x26991)),f2(f1(f2(f2(x26992,x26993),f1(x26991))),f2(x26992,x26993))))),
% 58.49/58.64 inference(scs_inference,[],[6,2692,7,22])).
% 58.49/58.64 cnf(2701,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(f2(x27011,x27012),f1(x27013)),x27014)),f2(x27014,f2(f1(f2(x27013,x27013)),f2(x27011,x27012)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2692,2695,7,22,9])).
% 58.49/58.64 cnf(2705,plain,
% 58.49/58.64 (P2(f2(f1(f2(x27051,f2(x27052,x27052))),f2(x27051,f2(f1(f2(f2(x27053,x27054),f1(x27052))),f2(x27053,x27054)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2692,2695,7,22,9,28])).
% 58.49/58.64 cnf(2711,plain,
% 58.49/58.64 (P2(f2(f1(f2(f2(x27111,x27111),x27112)),f2(x27112,f2(f1(f2(f2(x27113,x27114),f1(x27111))),f2(x27113,x27114)))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2701,2705,7,22,9])).
% 58.49/58.64 cnf(2719,plain,
% 58.49/58.64 (P2(f2(f1(f2(x27191,f1(f2(x27192,x27193)))),f2(f1(f2(x27192,f2(x27194,x27193))),f2(x27194,x27191))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2711,208,7,22,9])).
% 58.49/58.64 cnf(2727,plain,
% 58.49/58.64 (P2(f2(f1(f2(x27271,f1(x27272))),f2(f1(f2(x27272,x27272)),f2(x27273,x27271))))),
% 58.49/58.64 inference(scs_inference,[],[3,6,2719,441,7,22,9])).
% 58.49/58.64 cnf(2735,plain,
% 58.49/58.64 (P2(f2(f1(f2(x27351,x27351)),f2(f1(f2(x27352,f1(x27351))),f2(x27353,x27352))))),
% 58.49/58.64 inference(scs_inference,[],[6,2727,7,22])).
% 58.49/58.64 cnf(2978,plain,
% 58.49/58.64 (P2(f2(f1(f2(x29781,x29781)),x29781))),
% 58.49/58.64 inference(scs_inference,[],[2699,2735,2,30,24,7])).
% 58.49/58.64 cnf(2991,plain,
% 58.49/58.64 ($false),
% 58.49/58.64 inference(scs_inference,[],[1,2978,17,1077,2591,12,30,24,8,9]),
% 58.49/58.64 ['proof']).
% 58.49/58.64 % SZS output end Proof
% 58.49/58.64 % Total time :58.094862s
%------------------------------------------------------------------------------