%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : LCL399-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 : n001.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:06 AM UTC 2026
% Result : Unsatisfiable 232.00s 231.92s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL399-1 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.08/0.35 % Computer : n001.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sun Sep 6 00:20:48 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.24/0.52 start to proof:theBenchmark
% 232.00/231.91 %-------------------------------------------
% 232.00/231.91 % File :CSE---1.7
% 232.00/231.91 % Problem :theBenchmark
% 232.00/231.91 % Transform :cnf
% 232.00/231.91 % Format :tptp:raw
% 232.00/231.91 % Command :java -jar mcs_scs.jar %d %s
% 232.00/231.91
% 232.00/231.91 % Result :Theorem 231.408547s
% 232.00/231.91 % Output :CNFRefutation 231.408547s
% 232.00/231.91 %-------------------------------------------
% 232.00/231.91 %--------------------------------------------------------------------------
% 232.00/231.91 % File : LCL399-1 : TPTP v9.3.1. Released v2.3.0.
% 232.00/231.91 % Domain : Logic Calculi (Implication/Negation 2 valued sentential)
% 232.00/231.91 % Problem : CN-65 depends on the Lukasiewicz system
% 232.00/231.91 % Version : [McC92] axioms.
% 232.00/231.91 % English : An axiomatisation of the Implication/Negation 2 valued
% 232.00/231.91 % sentential calculus is {CN-1,CN-2,CN-3} by Lukasiewicz.
% 232.00/231.91 % Show that CN-65 depends on the Lukasiewicz system.
% 232.00/231.91
% 232.00/231.91 % Refs : [Wos96] Wos (1996), Combining Resonance with Heat
% 232.00/231.91 % : [McC92] McCune (1992), Email to G. Sutcliffe
% 232.00/231.91 % Source : [Wos96]
% 232.00/231.91 % Names : thesis_65 [Wos96]
% 232.00/231.92
% 232.00/231.92 % Status : Unsatisfiable
% 232.00/231.92 % 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.08 v5.1.0, 0.19 v5.0.0, 0.20 v4.0.1, 0.00 v2.6.0, 0.29 v2.5.0, 0.00 v2.3.0
% 232.00/231.92 % Syntax : Number of clauses : 5 ( 4 unt; 0 nHn; 2 RR)
% 232.00/231.92 % Number of literals : 7 ( 0 equ; 3 neg)
% 232.00/231.92 % Maximal clause size : 3 ( 1 avg)
% 232.00/231.92 % Maximal term depth : 5 ( 2 avg)
% 232.00/231.92 % Number of predicates : 1 ( 1 usr; 0 prp; 1-1 aty)
% 232.00/231.92 % Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% 232.00/231.92 % Number of variables : 8 ( 1 sgn)
% 232.00/231.92 % SPC : CNF_UNS_RFO_NEQ_HRN
% 232.00/231.92
% 232.00/231.92 % Comments :
% 232.00/231.92 %--------------------------------------------------------------------------
% 232.00/231.92 cnf(condensed_detachment,axiom,
% 232.00/231.92 ( ~ is_a_theorem(implies(X,Y))
% 232.00/231.92 | ~ is_a_theorem(X)
% 232.00/231.92 | is_a_theorem(Y) ) ).
% 232.00/231.92
% 232.00/231.92 cnf(cn_1,axiom,
% 232.00/231.92 is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) ).
% 232.00/231.92
% 232.00/231.92 cnf(cn_2,axiom,
% 232.00/231.92 is_a_theorem(implies(implies(not(X),X),X)) ).
% 232.00/231.92
% 232.00/231.92 cnf(cn_3,axiom,
% 232.00/231.92 is_a_theorem(implies(X,implies(not(X),Y))) ).
% 232.00/231.92
% 232.00/231.92 cnf(prove_cn_65,negated_conjecture,
% 232.00/231.92 ~ is_a_theorem(implies(implies(not(x),not(implies(y,y))),x)) ).
% 232.00/231.92
% 232.00/231.92 %--------------------------------------------------------------------------
% 232.00/231.92 %-------------------------------------------
% 232.00/231.92 % Proof found
% 232.00/231.92 % SZS status Theorem for theBenchmark
% 232.00/231.92 % SZS output start Proof
% 232.00/231.92 %ClaNum:5(EqnAxiom:0)
% 232.00/231.92 %VarNum:16(SingletonVarNum:8)
% 232.00/231.92 %MaxLitNum:3
% 232.00/231.92 %MaxfuncDepth:4
% 232.00/231.92 %SharedTerms:8
% 232.00/231.92 %goalClause: 4
% 232.00/231.92 %singleGoalClaCount:1
% 232.00/231.92 [4]~P1(f2(f2(f1(a3),f1(f2(a4,a4))),a3))
% 232.00/231.92 [2]P1(f2(f2(f1(x21),x21),x21))
% 232.00/231.92 [1]P1(f2(x11,f2(f1(x11),x12)))
% 232.00/231.92 [3]P1(f2(f2(x31,x32),f2(f2(x32,x33),f2(x31,x33))))
% 232.00/231.92 [5]P1(x51)+~P1(x52)+~P1(f2(x52,x51))
% 232.00/231.92 %EqnAxiom
% 232.00/231.92
% 232.00/231.92 %-------------------------------------------
% 232.00/231.93 cnf(6,plain,
% 232.00/231.93 (P1(f2(f2(x61,x62),f2(f2(f1(x61),x61),x62)))),
% 232.00/231.93 inference(scs_inference,[],[2,3,5])).
% 232.00/231.93 cnf(9,plain,
% 232.00/231.93 (P1(f2(f2(f1(x91),x91),f2(f1(x91),x92)))),
% 232.00/231.93 inference(scs_inference,[],[6,1,5])).
% 232.00/231.93 cnf(12,plain,
% 232.00/231.93 (P1(f2(f1(x121),x122))+~P1(f2(f1(x121),x121))),
% 232.00/231.93 inference(scs_inference,[],[9,5])).
% 232.00/231.93 cnf(14,plain,
% 232.00/231.93 (P1(f2(f2(f2(f1(x141),x142),x143),f2(x141,x143)))),
% 232.00/231.93 inference(scs_inference,[],[1,3,5])).
% 232.00/231.93 cnf(17,plain,
% 232.00/231.93 (P1(f2(f2(f1(f2(x171,x172)),f2(x171,x172)),f2(f2(x172,x173),f2(x171,x173))))),
% 232.00/231.93 inference(scs_inference,[],[3,6,5])).
% 232.00/231.93 cnf(20,plain,
% 232.00/231.93 (P1(f2(f2(x201,x202),f2(x203,x202)))+~P1(f2(f1(f2(x203,x201)),f2(x203,x201)))),
% 232.00/231.93 inference(scs_inference,[],[17,5])).
% 232.00/231.93 cnf(22,plain,
% 232.00/231.93 (P1(f2(f2(f1(f2(f1(x221),x221)),f2(f1(x221),x221)),x221))),
% 232.00/231.93 inference(scs_inference,[],[2,6,5])).
% 232.00/231.93 cnf(25,plain,
% 232.00/231.93 (P1(f2(f2(f2(f1(x251),x252),x253),f2(f2(f1(x251),x251),x253)))),
% 232.00/231.93 inference(scs_inference,[],[3,9,5])).
% 232.00/231.93 cnf(28,plain,
% 232.00/231.93 (P1(f2(f2(f1(x281),x281),f2(f2(x282,x283),f2(f1(x281),x283))))),
% 232.00/231.93 inference(scs_inference,[],[3,25,5])).
% 232.00/231.93 cnf(32,plain,
% 232.00/231.93 (P1(f2(f2(x321,x322),f2(f1(x323),x322)))+~P1(f2(f1(x323),x323))),
% 232.00/231.93 inference(scs_inference,[],[28,5])).
% 232.00/231.93 cnf(34,plain,
% 232.00/231.93 (P1(f2(f2(f1(f2(f1(x341),x341)),f2(f1(x341),x341)),f2(f1(x341),x342)))),
% 232.00/231.93 inference(scs_inference,[],[6,9,5])).
% 232.00/231.93 cnf(37,plain,
% 232.00/231.93 (P1(f2(f2(f1(x371),x371),f2(f2(f1(f1(x371)),f1(x371)),x372)))),
% 232.00/231.93 inference(scs_inference,[],[6,25,5])).
% 232.00/231.93 cnf(41,plain,
% 232.00/231.93 (P1(f2(f2(f2(f2(f1(x411),x411),x412),x413),f2(f2(x411,x412),x413)))),
% 232.00/231.93 inference(scs_inference,[],[6,3,5])).
% 232.00/231.93 cnf(44,plain,
% 232.00/231.93 (~P1(f2(f2(f2(f1(f1(a3)),f1(a3)),f1(f2(a4,a4))),a3))),
% 232.00/231.93 inference(scs_inference,[],[41,4,5])).
% 232.00/231.93 cnf(47,plain,
% 232.00/231.93 (P1(f2(f1(x471),x472))+~P1(f2(f1(f2(f1(x471),x471)),f2(f1(x471),x471)))),
% 232.00/231.93 inference(scs_inference,[],[34,5])).
% 232.00/231.93 cnf(49,plain,
% 232.00/231.93 (P1(f2(f2(x491,x492),f2(x493,x492)))+~P1(f2(f1(f2(f1(f2(x493,x491)),f2(x493,x491))),f2(f1(f2(x493,x491)),f2(x493,x491))))),
% 232.00/231.93 inference(scs_inference,[],[34,5,20])).
% 232.00/231.93 cnf(50,plain,
% 232.00/231.93 (~P1(f2(f1(f2(f1(x501),x501)),f2(f1(x501),x501)))+P1(f2(f2(x502,x503),f2(f1(x501),x503)))),
% 232.00/231.93 inference(scs_inference,[],[47,32])).
% 232.00/231.93 cnf(51,plain,
% 232.00/231.93 (P1(f2(f2(f1(f1(x511)),f1(x511)),x512))+~P1(f2(f1(x511),x511))),
% 232.00/231.93 inference(scs_inference,[],[37,5])).
% 232.00/231.93 cnf(53,plain,
% 232.00/231.93 (~P1(f2(f1(f2(f1(x531),x531)),f2(f1(x531),x531)))+P1(f2(f2(f1(f1(x531)),f1(x531)),x532))),
% 232.00/231.93 inference(scs_inference,[],[51,47])).
% 232.00/231.93 cnf(54,plain,
% 232.00/231.93 (~P1(f2(f1(f2(f1(x541),x541)),f2(f1(x541),x541)))+P1(f2(f2(f1(f2(x542,x543)),f2(x542,x543)),f2(f1(x541),x543)))),
% 232.00/231.93 inference(scs_inference,[],[6,50,5])).
% 232.00/231.93 cnf(55,plain,
% 232.00/231.93 (P1(f2(f2(f1(f1(x551)),f1(x551)),x552))+~P1(f2(f2(f1(f1(f2(f1(x551),x551))),x553),f2(f1(x551),x551)))),
% 232.00/231.93 inference(scs_inference,[],[14,53,5])).
% 232.00/231.93 cnf(56,plain,
% 232.00/231.93 (P1(f2(f1(f2(f2(f2(f1(x561),x562),x563),f2(x561,x563))),x564))),
% 232.00/231.93 inference(scs_inference,[],[14,1,5])).
% 232.00/231.93 cnf(59,plain,
% 232.00/231.93 (~P1(f1(f2(f2(f2(f1(x591),x592),x593),f2(x591,x593))))),
% 232.00/231.93 inference(scs_inference,[],[56,4,5])).
% 232.00/231.93 cnf(65,plain,
% 232.00/231.93 (~P1(f2(f1(f2(f1(x651),x651)),f2(f1(x651),x651)))+P1(f2(f2(f1(f2(f1(f1(x651)),f1(x651))),f2(f1(f1(x651)),f1(x651))),x652))),
% 232.00/231.93 inference(scs_inference,[],[6,53,5])).
% 232.00/231.93 cnf(66,plain,
% 232.00/231.93 (~P1(f2(f1(f2(f1(x661),x661)),f2(f1(x661),x661)))+~P1(f2(f1(f1(x661)),f1(x661)))),
% 232.00/231.93 inference(scs_inference,[],[59,53,5])).
% 232.00/231.93 cnf(67,plain,
% 232.00/231.93 (~P1(f2(f1(f2(f1(x671),x671)),f2(f1(x671),x671)))+~P1(f2(f1(f2(f1(f1(x671)),f1(x671))),f2(f1(f1(x671)),f1(x671))))),
% 232.00/231.93 inference(scs_inference,[],[66,47])).
% 232.00/231.93 cnf(71,plain,
% 232.00/231.93 (~P1(f2(f1(f2(f1(f2(x711,x712)),f2(x711,x712))),f2(f1(f2(x711,x712)),f2(x711,x712))))+P1(f2(f2(f1(f2(x712,x713)),f2(x712,x713)),f2(x711,x713)))),
% 232.00/231.93 inference(scs_inference,[],[6,5,49])).
% 232.00/231.93 cnf(74,plain,
% 232.00/231.93 (~P1(f2(f1(f2(f1(x741),x741)),f2(f1(x741),x741)))+~P1(f2(f2(f2(x742,x743),f2(f1(x741),x743)),f1(f2(f2(f2(f1(x744),x745),x746),f2(x744,x746)))))),
% 232.00/231.93 inference(scs_inference,[],[59,5,50])).
% 232.00/231.93 cnf(77,plain,
% 232.00/231.93 (~P1(f2(f1(f2(f1(x771),x771)),f2(f1(x771),x771)))+~P1(f2(f2(f2(f1(f1(x771)),f1(x771)),x772),f2(f2(f1(a3),f1(f2(a4,a4))),a3)))),
% 232.00/231.93 inference(scs_inference,[],[4,5,53])).
% 232.00/231.93 cnf(78,plain,
% 232.00/231.93 (~P1(f2(f1(f2(f1(f2(x781,x782)),f2(x781,x782))),f2(f1(f2(x781,x782)),f2(x781,x782))))+~P1(f2(f2(f2(x782,x783),f2(x781,x783)),f2(f2(f1(a3),f1(f2(a4,a4))),a3)))),
% 232.00/231.93 inference(scs_inference,[],[4,5,49])).
% 232.00/231.93 cnf(79,plain,
% 232.00/231.93 (~P1(f2(f1(f2(f1(x791),x791)),f2(f1(x791),x791)))+~P1(f2(f2(f2(x792,x793),f2(f1(x791),x793)),f2(f2(f1(a3),f1(f2(a4,a4))),a3)))),
% 232.00/231.93 inference(scs_inference,[],[4,5,50])).
% 232.00/231.93 cnf(80,plain,
% 232.00/231.93 (P1(f2(f2(f1(f2(f2(x801,x802),x803)),f2(f2(x801,x802),x803)),f2(f2(f2(f1(x801),x804),x802),x803)))),
% 232.00/231.93 inference(scs_inference,[],[1,56,71,5])).
% 232.00/231.93 cnf(81,plain,
% 232.00/231.93 (~P1(f2(f1(f2(f1(x811),x811)),f2(f1(x811),x811)))+~P1(f2(f2(f2(x812,x813),f2(f1(x811),x813)),f2(f2(f2(f1(f1(a3)),f1(a3)),f1(f2(a4,a4))),a3)))),
% 232.00/231.93 inference(scs_inference,[],[44,50,5])).
% 232.00/231.93 cnf(87,plain,
% 232.00/231.93 (~P1(f2(f1(f2(f1(x871),x871)),f2(f1(x871),x871)))+~P1(f2(f2(f2(f1(f1(x871)),f1(x871)),x872),f2(f2(f2(f1(f1(a3)),f1(a3)),f1(f2(a4,a4))),a3)))),
% 232.00/231.93 inference(scs_inference,[],[44,53,5])).
% 232.00/231.93 cnf(89,plain,
% 232.00/231.93 (~P1(f2(f1(f2(f1(x891),x891)),f2(f1(x891),x891)))+~P1(f2(f2(f2(f1(f1(x891)),f1(x891)),x892),f1(f2(f2(f2(f1(x893),x894),x895),f2(x893,x895)))))),
% 232.00/231.93 inference(scs_inference,[],[59,53,5])).
% 232.00/231.93 cnf(90,plain,
% 232.00/231.93 (P1(f2(f2(f1(f1(x901)),f1(x901)),x902))+~P1(f2(f2(f2(x903,x904),f2(f2(x904,x905),f2(x903,x905))),f2(f1(f2(f1(x901),x901)),f2(f1(x901),x901))))),
% 232.00/231.93 inference(scs_inference,[],[3,53,5])).
% 232.00/231.93 cnf(91,plain,
% 232.00/231.93 (P1(f2(f2(f1(f1(x911)),f1(x911)),x912))+~P1(f2(f2(f2(f1(x913),x913),f2(f1(x913),x914)),f2(f1(f2(f1(x911),x911)),f2(f1(x911),x911))))),
% 232.00/231.93 inference(scs_inference,[],[9,53,5])).
% 232.00/231.93 cnf(92,plain,
% 232.00/231.93 (P1(f2(f2(f1(f1(x921)),f1(x921)),x922))+~P1(f2(f2(f2(f1(f2(x923,x924)),f2(x923,x924)),f2(f2(x924,x925),f2(x923,x925))),f2(f1(f2(f1(x921),x921)),f2(f1(x921),x921))))),
% 232.00/231.93 inference(scs_inference,[],[17,53,5])).
% 232.00/231.93 cnf(96,plain,
% 232.00/231.93 (P1(f2(f2(f1(f1(f2(f2(f2(f1(x961),x962),x963),f2(x961,x963)))),f1(f2(f2(f2(f1(x961),x962),x963),f2(x961,x963)))),x964))),
% 232.00/231.93 inference(scs_inference,[],[56,1,53,5])).
% 232.00/231.93 cnf(98,plain,
% 232.00/231.93 (P1(f2(f2(f1(f2(x981,x982)),f2(x981,x982)),f2(f1(x983),x982)))+~P1(f2(f2(f2(f1(x984),x984),x984),f2(f1(f2(f1(x983),x983)),f2(f1(x983),x983))))),
% 232.00/231.93 inference(scs_inference,[],[2,54,5])).
% 232.00/231.93 cnf(99,plain,
% 232.00/231.94 (P1(f2(f2(f1(f2(x991,x992)),f2(x991,x992)),f2(f1(x993),x992)))+~P1(f2(f2(f2(x994,x995),f2(f2(f1(x994),x994),x995)),f2(f1(f2(f1(x993),x993)),f2(f1(x993),x993))))),
% 232.00/231.94 inference(scs_inference,[],[6,54,5])).
% 232.00/231.94 cnf(100,plain,
% 232.00/231.94 (P1(f2(f2(f1(f2(x1001,x1002)),f2(x1001,x1002)),f2(f1(x1003),x1002)))+~P1(f2(f2(f2(f2(f1(x1004),x1005),x1006),f2(x1004,x1006)),f2(f1(f2(f1(x1003),x1003)),f2(f1(x1003),x1003))))),
% 232.00/231.94 inference(scs_inference,[],[14,54,5])).
% 232.00/231.94 cnf(101,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(x1011),x1011)),f2(f1(x1011),x1011)))+~P1(f2(f2(f2(f2(f1(x1012),x1013),x1014),f2(f2(f1(x1012),x1012),x1014)),f2(f1(f2(f1(f1(x1011)),f1(x1011))),f2(f1(f1(x1011)),f1(x1011)))))),
% 232.00/231.94 inference(scs_inference,[],[25,67,5])).
% 232.00/231.94 cnf(102,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(x1021),x1021)),f2(f1(x1021),x1021)))+~P1(f2(f2(f2(f1(f2(f1(x1022),x1022)),f2(f1(x1022),x1022)),f2(f1(x1022),x1023)),f2(f1(f2(f1(f1(x1021)),f1(x1021))),f2(f1(f1(x1021)),f1(x1021)))))),
% 232.00/231.94 inference(scs_inference,[],[34,67,5])).
% 232.00/231.94 cnf(104,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(x1041),x1041)),f2(f1(x1041),x1041)))+~P1(f2(f2(f1(f2(f2(f2(f1(x1042),x1043),x1044),f2(x1042,x1044))),x1045),f2(f1(f2(f1(f1(x1041)),f1(x1041))),f2(f1(f1(x1041)),f1(x1041)))))),
% 232.00/231.94 inference(scs_inference,[],[56,67,5])).
% 232.00/231.94 cnf(106,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(x1061),x1061)),f2(f1(x1061),x1061)))+~P1(f2(f2(f2(f1(x1062),x1062),x1062),f2(f1(f2(f1(f1(x1061)),f1(x1061))),f2(f1(f1(x1061)),f1(x1061)))))),
% 232.00/231.94 inference(scs_inference,[],[2,67,5])).
% 232.00/231.94 cnf(108,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(x1081),x1081)),f2(f1(x1081),x1081)))+~P1(f2(f2(f2(f2(f1(x1082),x1083),x1084),f2(x1082,x1084)),f2(f1(f2(f1(f1(x1081)),f1(x1081))),f2(f1(f1(x1081)),f1(x1081)))))),
% 232.00/231.94 inference(scs_inference,[],[14,67,5])).
% 232.00/231.94 cnf(110,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(x1101),x1101)),f2(f1(x1101),x1101)))+~P1(f2(f2(f2(f1(x1102),x1102),f2(f2(x1103,x1104),f2(f1(x1102),x1104))),f2(f1(f2(f1(f1(x1101)),f1(x1101))),f2(f1(f1(x1101)),f1(x1101)))))),
% 232.00/231.94 inference(scs_inference,[],[28,67,5])).
% 232.00/231.94 cnf(111,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(x1111),x1111)),f2(f1(x1111),x1111)))+~P1(f2(f2(f2(f1(x1112),x1112),f2(f2(f1(f1(x1112)),f1(x1112)),x1113)),f2(f1(f2(f1(f1(x1111)),f1(x1111))),f2(f1(f1(x1111)),f1(x1111)))))),
% 232.00/231.94 inference(scs_inference,[],[37,67,5])).
% 232.00/231.94 cnf(114,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(x1141),x1141)),f2(f1(x1141),x1141)))+~P1(f2(f2(x1142,f2(f1(x1142),x1143)),f2(f1(f2(f1(f1(x1141)),f1(x1141))),f2(f1(f1(x1141)),f1(x1141)))))),
% 232.00/231.94 inference(scs_inference,[],[1,67,5])).
% 232.00/231.94 cnf(116,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(x1161),x1161)),f2(f1(x1161),x1161)))+~P1(f2(f2(f2(f1(x1162),x1162),f2(f1(x1162),x1163)),f2(f1(f2(f1(f1(x1161)),f1(x1161))),f2(f1(f1(x1161)),f1(x1161)))))),
% 232.00/231.94 inference(scs_inference,[],[9,67,5])).
% 232.00/231.94 cnf(117,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(x1171),x1171)),f2(f1(x1171),x1171)))+~P1(f2(f2(f2(f1(f2(x1172,x1173)),f2(x1172,x1173)),f2(f2(x1173,x1174),f2(x1172,x1174))),f2(f1(f2(f1(f1(x1171)),f1(x1171))),f2(f1(f1(x1171)),f1(x1171)))))),
% 232.00/231.94 inference(scs_inference,[],[17,67,5])).
% 232.00/231.94 cnf(120,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(x1201),x1201)),f2(f1(x1201),x1201)))+~P1(f2(f2(f2(f2(f2(f1(x1202),x1202),x1203),x1204),f2(f2(x1202,x1203),x1204)),f2(f1(f2(f1(f1(x1201)),f1(x1201))),f2(f1(f1(x1201)),f1(x1201)))))),
% 232.00/231.94 inference(scs_inference,[],[41,67,5])).
% 232.00/231.94 cnf(124,plain,
% 232.00/231.94 (P1(f2(f2(f1(f2(x1241,x1242)),f2(x1241,x1242)),f2(x1243,x1242)))+~P1(f2(f2(f2(f1(x1244),x1244),f2(f1(x1244),x1245)),f2(f1(f2(f1(f2(x1243,x1241)),f2(x1243,x1241))),f2(f1(f2(x1243,x1241)),f2(x1243,x1241)))))),
% 232.00/231.94 inference(scs_inference,[],[9,71,5])).
% 232.00/231.94 cnf(125,plain,
% 232.00/231.94 (P1(f2(f2(f1(f2(x1251,x1252)),f2(x1251,x1252)),f2(x1253,x1252)))+~P1(f2(f2(f2(f1(f2(x1254,x1255)),f2(x1254,x1255)),f2(f2(x1255,x1256),f2(x1254,x1256))),f2(f1(f2(f1(f2(x1253,x1251)),f2(x1253,x1251))),f2(f1(f2(x1253,x1251)),f2(x1253,x1251)))))),
% 232.00/231.94 inference(scs_inference,[],[17,71,5])).
% 232.00/231.94 cnf(132,plain,
% 232.00/231.94 (~P1(f2(f1(f1(x1321)),f1(x1321)))+~P1(f2(f2(x1322,f2(f1(x1322),x1323)),f2(f1(f2(f1(x1321),x1321)),f2(f1(x1321),x1321))))),
% 232.00/231.94 inference(scs_inference,[],[1,66,5])).
% 232.00/231.94 cnf(133,plain,
% 232.00/231.94 (~P1(f2(f1(f1(x1331)),f1(x1331)))+~P1(f2(f2(f2(x1332,x1333),f2(f2(x1333,x1334),f2(x1332,x1334))),f2(f1(f2(f1(x1331),x1331)),f2(f1(x1331),x1331))))),
% 232.00/231.94 inference(scs_inference,[],[3,66,5])).
% 232.00/231.94 cnf(135,plain,
% 232.00/231.94 (~P1(f2(f1(f1(x1351)),f1(x1351)))+~P1(f2(f2(f2(f1(f2(x1352,x1353)),f2(x1352,x1353)),f2(f2(x1353,x1354),f2(x1352,x1354))),f2(f1(f2(f1(x1351),x1351)),f2(f1(x1351),x1351))))),
% 232.00/231.94 inference(scs_inference,[],[17,66,5])).
% 232.00/231.94 cnf(161,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(x1611),x1611)),f2(f1(x1611),x1611)))+~P1(f2(f2(f2(x1612,x1613),f2(f2(f1(x1612),x1612),x1613)),f2(f1(f2(f1(f1(x1611)),f1(x1611))),f2(f1(f1(x1611)),f1(x1611)))))),
% 232.00/231.94 inference(scs_inference,[],[6,67,5])).
% 232.00/231.94 cnf(163,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(f1(x1631)),f1(x1631))),f2(f1(f1(x1631)),f1(x1631))))+~P1(f2(f1(f2(f1(f2(f1(x1631),x1631)),f2(f1(x1631),x1631))),f2(f1(f2(f1(x1631),x1631)),f2(f1(x1631),x1631))))),
% 232.00/231.94 inference(scs_inference,[],[34,5,67])).
% 232.00/231.94 cnf(164,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(f2(x1641,x1642)),f2(x1641,x1642))),f2(f1(f2(x1641,x1642)),f2(x1641,x1642))))+~P1(f2(f2(f2(x1642,x1643),f2(x1641,x1643)),f1(f2(f2(f2(f1(x1644),x1645),x1646),f2(x1644,x1646)))))),
% 232.00/231.94 inference(scs_inference,[],[59,49,5])).
% 232.00/231.94 cnf(165,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(f2(x1651,f1(x1652))),f2(x1651,f1(x1652)))),f2(f1(f2(x1651,f1(x1652))),f2(x1651,f1(x1652)))))+P1(f2(x1652,f2(x1651,x1653)))),
% 232.00/231.94 inference(scs_inference,[],[14,5,49])).
% 232.00/231.94 cnf(166,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(f2(x1661,x1662)),f2(x1661,x1662))),f2(f1(f2(x1661,x1662)),f2(x1661,x1662))))+P1(f2(f1(f2(f2(x1662,x1663),f2(x1661,x1663))),x1664))),
% 232.00/231.94 inference(scs_inference,[],[1,5,49])).
% 232.00/231.94 cnf(168,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(f2(x1681,x1682)),f2(x1681,x1682))),f2(f1(f2(x1681,x1682)),f2(x1681,x1682))))+P1(f2(f2(f2(x1681,x1683),x1684),f2(f2(x1682,x1683),x1684)))),
% 232.00/231.94 inference(scs_inference,[],[166,20])).
% 232.00/231.94 cnf(170,plain,
% 232.00/231.94 (P1(f2(f1(f2(f2(x1701,x1702),f2(x1703,x1702))),x1704))+~P1(f2(f2(f2(f1(f2(x1705,x1706)),f2(x1705,x1706)),f2(f2(x1706,x1707),f2(x1705,x1707))),f2(f1(f2(f1(f2(x1703,x1701)),f2(x1703,x1701))),f2(f1(f2(x1703,x1701)),f2(x1703,x1701)))))),
% 232.00/231.94 inference(scs_inference,[],[17,166,5])).
% 232.00/231.94 cnf(171,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(f2(x1711,x1712)),f2(x1711,x1712))),f2(f1(f2(x1711,x1712)),f2(x1711,x1712))))+P1(f2(f2(x1713,x1714),f2(f1(f2(f2(x1712,x1715),f2(x1711,x1715))),x1714)))),
% 232.00/231.94 inference(scs_inference,[],[166,32])).
% 232.00/231.94 cnf(173,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(f2(x1731,x1732)),f2(x1731,x1732))),f2(f1(f2(x1731,x1732)),f2(x1731,x1732))))+P1(f2(f2(f1(f1(f2(f2(x1732,x1733),f2(x1731,x1733)))),f1(f2(f2(x1732,x1733),f2(x1731,x1733)))),x1734))),
% 232.00/231.94 inference(scs_inference,[],[166,51])).
% 232.00/231.94 cnf(178,plain,
% 232.00/231.94 (P1(f2(f1(f2(f2(x1781,x1782),f2(x1783,x1782))),x1784))+~P1(f2(f2(f2(f1(x1785),x1785),f2(f1(x1785),x1786)),f2(f1(f2(f1(f2(x1783,x1781)),f2(x1783,x1781))),f2(f1(f2(x1783,x1781)),f2(x1783,x1781)))))),
% 232.00/231.94 inference(scs_inference,[],[9,166,5])).
% 232.00/231.94 cnf(179,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(f2(x1791,x1792)),f2(x1791,x1792))),f2(f1(f2(x1791,x1792)),f2(x1791,x1792))))+~P1(f2(f2(f2(f2(x1791,x1793),x1794),f2(f2(x1792,x1793),x1794)),f2(f2(f2(f1(f1(a3)),f1(a3)),f1(f2(a4,a4))),a3)))),
% 232.00/231.94 inference(scs_inference,[],[44,168,5])).
% 232.00/231.94 cnf(181,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(f2(x1811,x1812)),f2(x1811,x1812))),f2(f1(f2(x1811,x1812)),f2(x1811,x1812))))+~P1(f2(f2(f2(f2(x1811,x1813),x1814),f2(f2(x1812,x1813),x1814)),f1(f2(f2(f2(f1(x1815),x1816),x1817),f2(x1815,x1817)))))),
% 232.00/231.94 inference(scs_inference,[],[59,168,5])).
% 232.00/231.94 cnf(185,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(f2(x1851,x1852)),f2(x1851,x1852))),f2(f1(f2(x1851,x1852)),f2(x1851,x1852))))+P1(f2(f2(x1852,x1853),f2(f2(x1853,x1854),f2(x1851,x1854))))),
% 232.00/231.94 inference(scs_inference,[],[3,168,5])).
% 232.00/231.94 cnf(186,plain,
% 232.00/231.94 (P1(f2(f2(x1861,x1862),f2(f2(x1862,x1863),f2(x1864,x1863))))+~P1(f2(f2(f2(x1865,x1866),f2(f2(f1(x1865),x1865),x1866)),f2(f1(f2(f1(f2(x1864,x1861)),f2(x1864,x1861))),f2(f1(f2(x1864,x1861)),f2(x1864,x1861)))))),
% 232.00/231.94 inference(scs_inference,[],[6,185,5])).
% 232.00/231.94 cnf(189,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(f2(f1(x1891),x1892)),f2(f1(x1891),x1892))),f2(f1(f2(f1(x1891),x1892)),f2(f1(x1891),x1892))))+P1(f2(f2(x1892,x1891),f2(f2(x1893,x1894),f2(f1(x1891),x1894))))),
% 232.00/231.94 inference(scs_inference,[],[28,168,5])).
% 232.00/231.94 cnf(190,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(f2(f1(x1901),x1902)),f2(f1(x1901),x1902))),f2(f1(f2(f1(x1901),x1902)),f2(f1(x1901),x1902))))+P1(f2(f2(x1902,x1901),f2(f2(f1(f1(x1901)),f1(x1901)),x1903)))),
% 232.00/231.94 inference(scs_inference,[],[37,168,5])).
% 232.00/231.94 cnf(193,plain,
% 232.00/231.94 (P1(f2(f2(x1931,x1932),f2(f2(x1932,x1933),f2(x1934,x1933))))+~P1(f2(f2(f2(f1(x1935),x1935),x1935),f2(f1(f2(f1(f2(x1934,x1931)),f2(x1934,x1931))),f2(f1(f2(x1934,x1931)),f2(x1934,x1931)))))),
% 232.00/231.94 inference(scs_inference,[],[2,185,5])).
% 232.00/231.94 cnf(194,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(x1941),x1941)),f2(f1(x1941),x1941)))+P1(f2(x1942,f2(f1(x1941),x1943)))),
% 232.00/231.94 inference(scs_inference,[],[14,5,50])).
% 232.00/231.94 cnf(195,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(x1951),x1951)),f2(f1(x1951),x1951)))+P1(f2(f1(f2(f1(x1951),x1952)),x1953))),
% 232.00/231.94 inference(scs_inference,[],[12,194])).
% 232.00/231.94 cnf(196,plain,
% 232.00/231.94 (P1(f2(f1(f2(f1(x1961),x1962)),x1963))+~P1(f2(f2(f2(f1(f2(x1964,x1965)),f2(x1964,x1965)),f2(f2(x1965,x1966),f2(x1964,x1966))),f2(f1(f2(f1(x1961),x1961)),f2(f1(x1961),x1961))))),
% 232.00/231.94 inference(scs_inference,[],[17,195,5])).
% 232.00/231.94 cnf(200,plain,
% 232.00/231.94 (P1(f2(x2001,f2(f1(x2002),x2003)))+~P1(f2(f2(x2004,f2(f1(x2004),x2005)),f2(f1(f2(f1(x2002),x2002)),f2(f1(x2002),x2002))))),
% 232.00/231.94 inference(scs_inference,[],[1,194,5])).
% 232.00/231.94 cnf(201,plain,
% 232.00/231.94 (P1(f2(x2011,f2(f1(x2012),x2013)))+~P1(f2(f2(f2(x2014,x2015),f2(f2(x2015,x2016),f2(x2014,x2016))),f2(f1(f2(f1(x2012),x2012)),f2(f1(x2012),x2012))))),
% 232.00/231.94 inference(scs_inference,[],[3,194,5])).
% 232.00/231.94 cnf(203,plain,
% 232.00/231.94 (P1(f2(x2031,f2(f1(x2032),x2033)))+~P1(f2(f2(f2(f1(f2(x2034,x2035)),f2(x2034,x2035)),f2(f2(x2035,x2036),f2(x2034,x2036))),f2(f1(f2(f1(x2032),x2032)),f2(f1(x2032),x2032))))),
% 232.00/231.94 inference(scs_inference,[],[17,194,5])).
% 232.00/231.94 cnf(215,plain,
% 232.00/231.94 (P1(f2(f2(f2(x2151,x2152),x2153),f2(f2(x2153,x2154),f2(f2(f2(f1(x2151),x2155),x2152),x2154))))),
% 232.00/231.94 inference(scs_inference,[],[56,1,185,5])).
% 232.00/231.94 cnf(217,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(x2171),x2171)),f2(f1(x2171),x2171)))+~P1(f1(f2(f1(x2171),x2172)))),
% 232.00/231.94 inference(scs_inference,[],[59,5,195])).
% 232.00/231.94 cnf(218,plain,
% 232.00/231.94 (~P1(f1(f2(f1(x2181),x2182)))+~P1(f2(f2(f2(f1(x2183),x2183),f2(f1(x2183),x2184)),f2(f1(f2(f1(x2181),x2181)),f2(f1(x2181),x2181))))),
% 232.00/231.94 inference(scs_inference,[],[9,217,5])).
% 232.00/231.94 cnf(219,plain,
% 232.00/231.94 (~P1(f1(f2(f1(x2191),x2192)))+~P1(f2(f2(f2(f1(f2(x2193,x2194)),f2(x2193,x2194)),f2(f2(x2194,x2195),f2(x2193,x2195))),f2(f1(f2(f1(x2191),x2191)),f2(f1(x2191),x2191))))),
% 232.00/231.94 inference(scs_inference,[],[17,217,5])).
% 232.00/231.94 cnf(224,plain,
% 232.00/231.94 (~P1(f1(f2(f1(x2241),x2242)))+~P1(f2(f2(f2(f1(x2243),x2243),x2243),f2(f1(f2(f1(x2241),x2241)),f2(f1(x2241),x2241))))),
% 232.00/231.94 inference(scs_inference,[],[2,217,5])).
% 232.00/231.94 cnf(225,plain,
% 232.00/231.94 (~P1(f1(f2(f1(x2251),x2252)))+~P1(f2(f2(x2253,f2(f1(x2253),x2254)),f2(f1(f2(f1(x2251),x2251)),f2(f1(x2251),x2251))))),
% 232.00/231.94 inference(scs_inference,[],[1,217,5])).
% 232.00/231.94 cnf(226,plain,
% 232.00/231.94 (~P1(f1(f2(f1(x2261),x2262)))+~P1(f2(f2(f2(x2263,x2264),f2(f2(x2264,x2265),f2(x2263,x2265))),f2(f1(f2(f1(x2261),x2261)),f2(f1(x2261),x2261))))),
% 232.00/231.94 inference(scs_inference,[],[3,217,5])).
% 232.00/231.94 cnf(228,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(f2(f1(x2281),x2282)),f2(f1(x2281),x2282))),f2(f1(f2(f1(x2281),x2282)),f2(f1(x2281),x2282))))+P1(f2(f2(x2281,x2283),f2(f2(x2282,x2281),x2283)))),
% 232.00/231.94 inference(scs_inference,[],[41,5,168])).
% 232.00/231.94 cnf(232,plain,
% 232.00/231.94 (~P1(f2(f1(f1(x2321)),f1(x2321)))+~P1(f2(f2(f2(f1(x2322),x2322),x2322),f2(f1(f2(f1(x2321),x2321)),f2(f1(x2321),x2321))))),
% 232.00/231.94 inference(scs_inference,[],[2,66,5])).
% 232.00/231.94 cnf(238,plain,
% 232.00/231.94 (P1(f2(x2381,f2(f1(f2(f2(f2(f1(x2382),x2383),x2384),f2(x2382,x2384))),x2385)))),
% 232.00/231.94 inference(scs_inference,[],[56,1,194,5])).
% 232.00/231.94 cnf(240,plain,
% 232.00/231.94 (P1(f2(f2(f1(f1(x2401)),f1(x2401)),x2402))+~P1(f2(f2(x2403,f2(f1(x2403),x2404)),f2(f1(f2(f1(x2401),x2401)),f2(f1(x2401),x2401))))),
% 232.00/231.94 inference(scs_inference,[],[1,53,5])).
% 232.00/231.94 cnf(241,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(f2(x2411,x2412)),f2(x2411,x2412))),f2(f1(f2(x2411,x2412)),f2(x2411,x2412))))+~P1(f2(f2(f2(x2412,x2413),f2(x2411,x2413)),f2(f2(f2(f1(f1(a3)),f1(a3)),f1(f2(a4,a4))),a3)))),
% 232.00/231.94 inference(scs_inference,[],[44,49,5])).
% 232.00/231.94 cnf(255,plain,
% 232.00/231.94 (P1(f2(f2(f2(f2(f2(f1(x2551),x2552),x2553),x2554),x2555),f2(f2(f2(x2551,x2553),x2554),x2555)))),
% 232.00/231.94 inference(scs_inference,[],[56,1,168,5])).
% 232.00/231.94 cnf(256,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(f2(f1(f2(x2561,x2562)),x2563)),f2(f1(f2(x2561,x2562)),x2563))),f2(f1(f2(f1(f2(x2561,x2562)),x2563)),f2(f1(f2(x2561,x2562)),x2563))))+P1(f2(f2(x2563,f2(x2561,x2562)),f2(f2(x2562,x2564),f2(x2561,x2564))))),
% 232.00/231.94 inference(scs_inference,[],[17,168,5])).
% 232.00/231.94 cnf(257,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(f2(x2571,x2572)),f2(x2571,x2572))),f2(f1(f2(x2571,x2572)),f2(x2571,x2572))))+P1(f2(f2(x2572,x2573),f2(f1(f2(x2571,x2573)),x2574)))),
% 232.00/231.94 inference(scs_inference,[],[1,168,5])).
% 232.00/231.94 cnf(259,plain,
% 232.00/231.94 (P1(f2(f2(x2591,x2592),f2(f1(f2(x2593,x2592)),x2594)))+~P1(f2(f2(f2(x2595,x2596),f2(f2(f1(x2595),x2595),x2596)),f2(f1(f2(f1(f2(x2593,x2591)),f2(x2593,x2591))),f2(f1(f2(x2593,x2591)),f2(x2593,x2591)))))),
% 232.00/231.94 inference(scs_inference,[],[6,257,5])).
% 232.00/231.94 cnf(260,plain,
% 232.00/231.94 (P1(f2(f2(x2601,x2602),f2(f1(f2(x2603,x2602)),x2604)))+~P1(f2(f2(f2(f2(f1(x2605),x2606),x2607),f2(x2605,x2607)),f2(f1(f2(f1(f2(x2603,x2601)),f2(x2603,x2601))),f2(f1(f2(x2603,x2601)),f2(x2603,x2601)))))),
% 232.00/231.94 inference(scs_inference,[],[14,257,5])).
% 232.00/231.94 cnf(264,plain,
% 232.00/231.94 (P1(f2(f2(x2641,x2642),f2(f1(f2(x2643,x2642)),x2644)))+~P1(f2(f2(f2(f1(f2(x2645,x2646)),f2(x2645,x2646)),f2(f2(x2646,x2647),f2(x2645,x2647))),f2(f1(f2(f1(f2(x2643,x2641)),f2(x2643,x2641))),f2(f1(f2(x2643,x2641)),f2(x2643,x2641)))))),
% 232.00/231.94 inference(scs_inference,[],[17,257,5])).
% 232.00/231.94 cnf(268,plain,
% 232.00/231.94 (P1(f2(f2(x2681,x2682),f2(f1(f2(x2683,x2682)),x2684)))+~P1(f2(f2(f2(f1(x2685),x2685),f2(f1(x2685),x2686)),f2(f1(f2(f1(f2(x2683,x2681)),f2(x2683,x2681))),f2(f1(f2(x2683,x2681)),f2(x2683,x2681)))))),
% 232.00/231.94 inference(scs_inference,[],[9,257,5])).
% 232.00/231.94 cnf(271,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(x2711),x2711)),f2(f1(x2711),x2711)))+~P1(f2(f2(f2(x2712,x2713),f2(f2(x2713,x2714),f2(x2712,x2714))),f2(f1(f2(f1(f1(x2711)),f1(x2711))),f2(f1(f1(x2711)),f1(x2711)))))),
% 232.00/231.94 inference(scs_inference,[],[3,67,5])).
% 232.00/231.94 cnf(273,plain,
% 232.00/231.94 (P1(f2(f1(f2(f1(x2731),x2732)),x2733))+~P1(f2(f2(f2(f1(x2734),x2734),x2734),f2(f1(f2(f1(x2731),x2731)),f2(f1(x2731),x2731))))),
% 232.00/231.94 inference(scs_inference,[],[2,195,5])).
% 232.00/231.94 cnf(282,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(f2(f1(f2(f1(x2821),x2821)),x2822)),f2(f1(f2(f1(x2821),x2821)),x2822))),f2(f1(f2(f1(f2(f1(x2821),x2821)),x2822)),f2(f1(f2(f1(x2821),x2821)),x2822))))+P1(f2(f2(x2822,f2(f1(x2821),x2821)),x2821))),
% 232.00/231.94 inference(scs_inference,[],[22,168,5])).
% 232.00/231.94 cnf(288,plain,
% 232.00/231.94 (P1(f2(f2(x2881,x2882),f2(f2(x2882,x2883),f2(x2884,x2883))))+~P1(f2(f2(f2(f1(f2(x2885,x2886)),f2(x2885,x2886)),f2(f2(x2886,x2887),f2(x2885,x2887))),f2(f1(f2(f1(f2(x2884,x2881)),f2(x2884,x2881))),f2(f1(f2(x2884,x2881)),f2(x2884,x2881)))))),
% 232.00/231.94 inference(scs_inference,[],[17,185,5])).
% 232.00/231.94 cnf(290,plain,
% 232.00/231.94 (P1(f2(f2(x2901,x2902),f2(f2(x2902,x2903),f2(x2904,x2903))))+~P1(f2(f2(f2(f1(x2905),x2905),f2(f1(x2905),x2906)),f2(f1(f2(f1(f2(x2904,x2901)),f2(x2904,x2901))),f2(f1(f2(x2904,x2901)),f2(x2904,x2901)))))),
% 232.00/231.94 inference(scs_inference,[],[9,185,5])).
% 232.00/231.94 cnf(291,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(f2(x2911,x2912)),f2(x2911,x2912))),f2(f1(f2(x2911,x2912)),f2(x2911,x2912))))+P1(f2(f2(x2912,x2913),f2(f2(f1(x2911),x2911),x2913)))),
% 232.00/231.94 inference(scs_inference,[],[6,168,5])).
% 232.00/231.94 cnf(293,plain,
% 232.00/231.94 (P1(f2(f2(x2931,x2932),f2(f2(f1(x2933),x2933),x2932)))+~P1(f2(f2(f2(f1(f2(x2934,x2935)),f2(x2934,x2935)),f2(f2(x2935,x2936),f2(x2934,x2936))),f2(f1(f2(f1(f2(x2933,x2931)),f2(x2933,x2931))),f2(f1(f2(x2933,x2931)),f2(x2933,x2931)))))),
% 232.00/231.94 inference(scs_inference,[],[17,291,5])).
% 232.00/231.94 cnf(316,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(f2(f1(x3161),x3162)),f2(f1(x3161),x3162))),f2(f1(f2(f1(x3161),x3162)),f2(f1(x3161),x3162))))+P1(f2(f2(x3162,x3161),f2(f1(x3161),x3163)))),
% 232.00/231.94 inference(scs_inference,[],[9,168,5])).
% 232.00/231.94 cnf(318,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(f2(x3181,x3182)),f2(x3181,x3182))),f2(f1(f2(x3181,x3182)),f2(x3181,x3182))))+P1(f2(x3181,f2(f1(x3182),x3183)))),
% 232.00/231.94 inference(scs_inference,[],[1,5,49])).
% 232.00/231.94 cnf(326,plain,
% 232.00/231.94 (P1(f2(f2(f2(f1(x3261),x3262),x3263),f2(f1(f2(x3261,x3263)),x3264)))),
% 232.00/231.94 inference(scs_inference,[],[56,1,318,5])).
% 232.00/231.94 cnf(332,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(f2(x3321,f1(x3322))),f2(x3321,f1(x3322)))),f2(f1(f2(x3321,f1(x3322))),f2(x3321,f1(x3322)))))+P1(f2(f1(f2(x3322,f2(x3321,x3323))),x3324))),
% 232.00/231.94 inference(scs_inference,[],[326,5,49])).
% 232.00/231.94 cnf(333,plain,
% 232.00/231.94 (P1(f2(f2(f1(f1(x3331)),f1(x3331)),x3332))+~P1(f2(f2(f1(f1(x3331)),x3333),x3331))),
% 232.00/231.94 inference(scs_inference,[],[326,5,53])).
% 232.00/231.94 cnf(334,plain,
% 232.00/231.94 (~P1(f2(f2(f1(f1(x3341)),x3342),x3341))+~P1(f2(f2(f2(f1(f1(x3341)),f1(x3341)),x3343),f1(f2(f2(f2(f1(x3344),x3345),x3346),f2(x3344,x3346)))))),
% 232.00/231.94 inference(scs_inference,[],[59,333,5])).
% 232.00/231.94 cnf(336,plain,
% 232.00/231.94 (~P1(f2(f2(f1(f1(x3361)),x3362),x3361))+~P1(f2(f1(f1(x3361)),f1(x3361)))),
% 232.00/231.94 inference(scs_inference,[],[59,333,5])).
% 232.00/231.94 cnf(342,plain,
% 232.00/231.94 (~P1(f2(f1(f1(x3421)),f1(x3421)))+~P1(f2(f2(f2(f1(f2(x3422,x3423)),f2(x3422,x3423)),f2(f2(x3423,x3424),f2(x3422,x3424))),f2(f2(f1(f1(x3421)),x3425),x3421)))),
% 232.00/231.94 inference(scs_inference,[],[17,336,5])).
% 232.00/231.94 cnf(344,plain,
% 232.00/231.94 (~P1(f2(f1(f1(x3441)),f1(x3441)))+~P1(f2(f2(f2(f1(f2(f1(x3442),x3442)),f2(f1(x3442),x3442)),f2(f1(x3442),x3443)),f2(f2(f1(f1(x3441)),x3444),x3441)))),
% 232.00/231.94 inference(scs_inference,[],[34,336,5])).
% 232.00/231.94 cnf(345,plain,
% 232.00/231.94 (~P1(f2(f1(f1(x3451)),f1(x3451)))+~P1(f2(f2(f2(f2(f2(f1(x3452),x3452),x3453),x3454),f2(f2(x3452,x3453),x3454)),f2(f2(f1(f1(x3451)),x3455),x3451)))),
% 232.00/231.94 inference(scs_inference,[],[41,336,5])).
% 232.00/231.94 cnf(356,plain,
% 232.00/231.94 (~P1(f2(f1(f2(f1(f2(f1(x3561),x3562)),f2(f1(x3561),x3562))),f2(f1(f2(f1(x3561),x3562)),f2(f1(x3561),x3562))))+P1(f2(f2(x3562,x3561),x3561))),
% 232.00/231.94 inference(scs_inference,[],[2,5,168])).
% 232.00/231.94 cnf(357,plain,
% 232.00/231.95 (~P1(f2(f1(f2(f1(f2(x3571,f2(x3572,x3573))),f2(x3571,f2(x3572,x3573)))),f2(f1(f2(x3571,f2(x3572,x3573))),f2(x3571,f2(x3572,x3573)))))+P1(f2(x3571,f2(f2(f1(x3572),x3572),x3573)))),
% 232.00/231.95 inference(scs_inference,[],[6,5,49])).
% 232.00/231.95 cnf(358,plain,
% 232.00/231.95 (P1(f2(f1(x3581),x3582))+~P1(f2(f2(f1(f1(x3581)),x3583),x3581))),
% 232.00/231.95 inference(scs_inference,[],[14,5,333])).
% 232.00/231.95 cnf(359,plain,
% 232.00/231.95 (P1(f2(f1(x3591),x3592))+~P1(f2(f2(f2(f1(f2(x3593,x3594)),f2(x3593,x3594)),f2(f2(x3594,x3595),f2(x3593,x3595))),f2(f2(f1(f1(x3591)),x3596),x3591)))),
% 232.00/231.95 inference(scs_inference,[],[17,358,5])).
% 232.00/231.95 cnf(360,plain,
% 232.00/231.95 (P1(f2(f2(x3601,x3602),f2(x3603,x3602)))+~P1(f2(f2(f1(f1(f2(x3603,x3601))),x3604),f2(x3603,x3601)))),
% 232.00/231.95 inference(scs_inference,[],[358,20])).
% 232.00/231.95 cnf(363,plain,
% 232.00/231.95 (P1(f2(f2(x3631,x3632),f2(f1(x3633),x3632)))+~P1(f2(f2(f1(f1(x3633)),x3634),x3633))),
% 232.00/231.95 inference(scs_inference,[],[358,32])).
% 232.00/231.95 cnf(365,plain,
% 232.00/231.95 (P1(f2(f1(f2(f1(x3651),x3652)),x3653))+~P1(f2(f2(f1(f1(x3651)),x3654),x3651))),
% 232.00/231.95 inference(scs_inference,[],[358,363])).
% 232.00/231.95 cnf(368,plain,
% 232.00/231.95 (P1(f2(f1(x3681),x3682))+~P1(f2(f2(f2(f1(x3683),x3683),x3683),f2(f2(f1(f1(x3681)),x3684),x3681)))),
% 232.00/231.95 inference(scs_inference,[],[2,358,5])).
% 232.00/231.95 cnf(369,plain,
% 232.00/231.95 (~P1(f2(f1(f2(f1(x3691),x3691)),f2(f1(x3691),x3691)))+~P1(f2(f2(f1(f1(f1(x3691))),x3692),f1(x3691)))),
% 232.00/231.95 inference(scs_inference,[],[358,66])).
% 232.00/231.95 cnf(370,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(f1(x3701))),x3702),f1(x3701)))+~P1(f2(f2(f1(f1(x3701)),x3703),x3701))),
% 232.00/231.95 inference(scs_inference,[],[369,365])).
% 232.00/231.95 cnf(371,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(x3711)),x3712),x3711))+~P1(f2(f2(f2(f2(f1(x3713),x3714),x3715),f2(x3713,x3715)),f2(f2(f1(f1(f1(x3711))),x3716),f1(x3711))))),
% 232.00/231.95 inference(scs_inference,[],[14,370,5])).
% 232.00/231.95 cnf(372,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(f2(f1(x3721),x3721))),x3722),f2(f1(x3721),x3721)))+P1(f2(x3723,f2(f1(x3721),x3724)))),
% 232.00/231.95 inference(scs_inference,[],[358,194])).
% 232.00/231.95 cnf(373,plain,
% 232.00/231.95 (P1(f2(f1(x3731),x3732))+~P1(f2(f2(f2(f1(x3733),x3733),f2(f2(x3734,x3735),f2(f1(x3733),x3735))),f2(f2(f1(f1(x3731)),x3736),x3731)))),
% 232.00/231.95 inference(scs_inference,[],[28,358,5])).
% 232.00/231.95 cnf(374,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(f2(f1(x3741),x3741))),x3742),f2(f1(x3741),x3741)))+P1(f2(f1(f2(f1(x3741),x3743)),x3744))),
% 232.00/231.95 inference(scs_inference,[],[358,195])).
% 232.00/231.95 cnf(376,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(f2(f1(x3761),x3761))),x3762),f2(f1(x3761),x3761)))+~P1(f1(f2(f1(x3761),x3763)))),
% 232.00/231.95 inference(scs_inference,[],[358,217])).
% 232.00/231.95 cnf(377,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(f1(x3771))),x3772),f1(x3771)))+~P1(f2(f2(f1(f1(f2(f1(x3771),x3771))),x3773),f2(f1(x3771),x3771)))),
% 232.00/231.95 inference(scs_inference,[],[358,369])).
% 232.00/231.95 cnf(379,plain,
% 232.00/231.95 (P1(f2(f1(f2(f1(x3791),x3792)),x3793))+~P1(f2(f2(f2(x3794,x3795),f2(f2(f1(x3794),x3794),x3795)),f2(f2(f1(f1(x3791)),x3796),x3791)))),
% 232.00/231.95 inference(scs_inference,[],[6,365,5])).
% 232.00/231.95 cnf(380,plain,
% 232.00/231.95 (P1(f2(f1(f2(f1(x3801),x3802)),x3803))+~P1(f2(f2(f2(f2(f1(x3804),x3805),x3806),f2(x3804,x3806)),f2(f2(f1(f1(x3801)),x3807),x3801)))),
% 232.00/231.95 inference(scs_inference,[],[14,365,5])).
% 232.00/231.95 cnf(381,plain,
% 232.00/231.95 (P1(f2(f1(f2(f1(x3811),x3812)),x3813))+~P1(f2(f2(f2(f1(f2(f1(x3814),x3814)),f2(f1(x3814),x3814)),x3814),f2(f2(f1(f1(x3811)),x3815),x3811)))),
% 232.00/231.95 inference(scs_inference,[],[22,365,5])).
% 232.00/231.95 cnf(382,plain,
% 232.00/231.95 (P1(f2(f1(f2(f1(x3821),x3822)),x3823))+~P1(f2(f2(f2(f1(x3824),x3824),f2(f2(x3825,x3826),f2(f1(x3824),x3826))),f2(f2(f1(f1(x3821)),x3827),x3821)))),
% 232.00/231.95 inference(scs_inference,[],[28,365,5])).
% 232.00/231.95 cnf(383,plain,
% 232.00/231.95 (P1(f2(f1(f2(f1(x3831),x3832)),x3833))+~P1(f2(f2(f2(f1(x3834),x3834),f2(f2(f1(f1(x3834)),f1(x3834)),x3835)),f2(f2(f1(f1(x3831)),x3836),x3831)))),
% 232.00/231.95 inference(scs_inference,[],[37,365,5])).
% 232.00/231.95 cnf(387,plain,
% 232.00/231.95 (P1(f2(f2(x3871,x3872),f2(f1(x3873),x3872)))+~P1(f2(f2(x3874,f2(f1(x3874),x3875)),f2(f2(f1(f1(x3873)),x3876),x3873)))),
% 232.00/231.95 inference(scs_inference,[],[1,363,5])).
% 232.00/231.95 cnf(389,plain,
% 232.00/231.95 (P1(f2(f2(x3891,x3892),f2(f1(x3893),x3892)))+~P1(f2(f2(f2(f1(x3894),x3894),f2(f1(x3894),x3895)),f2(f2(f1(f1(x3893)),x3896),x3893)))),
% 232.00/231.95 inference(scs_inference,[],[9,363,5])).
% 232.00/231.95 cnf(390,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(x3901)),x3902),x3901))+~P1(f2(f2(f2(x3903,x3904),f2(f1(x3901),x3904)),f1(f2(f2(f2(f1(x3905),x3906),x3907),f2(x3905,x3907)))))),
% 232.00/231.95 inference(scs_inference,[],[59,363,5])).
% 232.00/231.95 cnf(391,plain,
% 232.00/231.95 (P1(f2(f2(x3911,x3912),f2(f1(x3913),x3912)))+~P1(f2(f2(f2(f2(f1(x3914),x3915),x3916),f2(f2(f1(x3914),x3914),x3916)),f2(f2(f1(f1(x3913)),x3917),x3913)))),
% 232.00/231.95 inference(scs_inference,[],[25,363,5])).
% 232.00/231.95 cnf(392,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(x3921)),x3922),x3921))+~P1(f2(f2(f2(x3923,x3924),f2(f1(x3921),x3924)),f2(f2(f1(a3),f1(f2(a4,a4))),a3)))),
% 232.00/231.95 inference(scs_inference,[],[4,363,5])).
% 232.00/231.95 cnf(397,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(x3971)),x3972),x3971))+~P1(f2(f2(f2(x3973,x3974),f2(f2(x3974,x3975),f2(x3973,x3975))),f2(f2(f1(f1(f1(x3971))),x3976),f1(x3971))))),
% 232.00/231.95 inference(scs_inference,[],[3,370,5])).
% 232.00/231.95 cnf(405,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(x4051)),x4052),x4051))+~P1(f2(f2(x4053,f2(f1(x4053),x4054)),f2(f2(f1(f1(f1(x4051))),x4055),f1(x4051))))),
% 232.00/231.95 inference(scs_inference,[],[1,370,5])).
% 232.00/231.95 cnf(406,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(f1(x4061))),x4062),f1(x4061)))+~P1(f2(f2(f2(x4063,x4064),f2(f2(x4064,x4065),f2(x4063,x4065))),f2(f2(f1(f1(x4061)),x4066),x4061)))),
% 232.00/231.95 inference(scs_inference,[],[3,370,5])).
% 232.00/231.95 cnf(407,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(x4071)),x4072),x4071))+~P1(f2(f2(f2(f1(x4073),x4073),f2(f1(x4073),x4074)),f2(f2(f1(f1(f1(x4071))),x4075),f1(x4071))))),
% 232.00/231.95 inference(scs_inference,[],[9,370,5])).
% 232.00/231.95 cnf(414,plain,
% 232.00/231.95 (P1(f2(f2(x4141,x4142),f2(x4143,x4142)))+~P1(f2(f2(f2(f2(f1(x4144),x4145),x4146),f2(f1(f2(x4144,x4146)),x4147)),f2(f2(f1(f1(f2(x4143,x4141))),x4148),f2(x4143,x4141))))),
% 232.00/231.95 inference(scs_inference,[],[326,360,5])).
% 232.00/231.95 cnf(415,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(f2(x4151,x4152))),x4153),f2(x4151,x4152)))+~P1(f2(f2(f2(x4152,x4154),f2(x4151,x4154)),f1(f2(f2(f2(f1(x4155),x4156),x4157),f2(x4155,x4157)))))),
% 232.00/231.95 inference(scs_inference,[],[59,360,5])).
% 232.00/231.95 cnf(416,plain,
% 232.00/231.95 (P1(f2(f2(x4161,x4162),f2(x4163,x4162)))+~P1(f2(f2(f2(x4164,x4165),f2(f2(f1(x4164),x4164),x4165)),f2(f2(f1(f1(f2(x4163,x4161))),x4166),f2(x4163,x4161))))),
% 232.00/231.95 inference(scs_inference,[],[6,360,5])).
% 232.00/231.95 cnf(417,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(f2(x4171,x4172))),x4173),f2(x4171,x4172)))+~P1(f2(f2(f2(x4172,x4174),f2(x4171,x4174)),f2(f2(f2(f1(f1(a3)),f1(a3)),f1(f2(a4,a4))),a3)))),
% 232.00/231.95 inference(scs_inference,[],[44,360,5])).
% 232.00/231.95 cnf(418,plain,
% 232.00/231.95 (P1(f2(f2(x4181,x4182),f2(x4183,x4182)))+~P1(f2(f2(f2(f1(f2(f1(x4184),x4184)),f2(f1(x4184),x4184)),x4184),f2(f2(f1(f1(f2(x4183,x4181))),x4185),f2(x4183,x4181))))),
% 232.00/231.95 inference(scs_inference,[],[22,360,5])).
% 232.00/231.95 cnf(419,plain,
% 232.00/231.95 (P1(f2(f2(x4191,x4192),f2(x4193,x4192)))+~P1(f2(f2(f2(f1(x4194),x4194),f2(f2(x4195,x4196),f2(f1(x4194),x4196))),f2(f2(f1(f1(f2(x4193,x4191))),x4197),f2(x4193,x4191))))),
% 232.00/231.95 inference(scs_inference,[],[28,360,5])).
% 232.00/231.95 cnf(420,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(f2(x4201,f2(f1(x4202),x4202)))),x4203),f2(x4201,f2(f1(x4202),x4202))))+P1(f2(x4201,f2(f2(f1(f1(x4202)),f1(x4202)),x4204)))),
% 232.00/231.95 inference(scs_inference,[],[37,360,5])).
% 232.00/231.95 cnf(424,plain,
% 232.00/231.95 (P1(f2(f1(f2(f1(x4241),x4242)),x4243))+~P1(f2(f2(f2(f1(f2(f1(x4244),x4244)),f2(f1(x4244),x4244)),f2(f1(x4244),x4245)),f2(f2(f1(f1(x4241)),x4246),x4241)))),
% 232.00/231.95 inference(scs_inference,[],[34,365,5])).
% 232.00/231.95 cnf(426,plain,
% 232.00/231.95 (~P1(f2(f1(f2(x4261,f1(f1(f2(x4261,x4262))))),f2(x4261,f1(f1(f2(x4261,x4262))))))+P1(f2(f2(f1(f1(f2(x4261,x4262))),f1(f2(x4261,x4262))),x4263))),
% 232.00/231.95 inference(scs_inference,[],[20,333])).
% 232.00/231.95 cnf(427,plain,
% 232.00/231.95 (~P1(f2(f1(f2(x4271,f1(f1(f2(x4271,x4272))))),f2(x4271,f1(f1(f2(x4271,x4272))))))+~P1(f2(f1(f1(f2(x4271,x4272))),f1(f2(x4271,x4272))))),
% 232.00/231.95 inference(scs_inference,[],[20,336])).
% 232.00/231.95 cnf(429,plain,
% 232.00/231.95 (~P1(f2(f1(f2(x4291,f1(f1(f2(x4291,x4292))))),f2(x4291,f1(f1(f2(x4291,x4292))))))+P1(f2(f1(f2(x4291,x4292)),x4293))),
% 232.00/231.95 inference(scs_inference,[],[20,358])).
% 232.00/231.95 cnf(430,plain,
% 232.00/231.95 (~P1(f2(f1(f2(x4301,f1(f1(f2(x4301,x4302))))),f2(x4301,f1(f1(f2(x4301,x4302))))))+P1(f2(f2(x4302,x4303),f2(x4301,x4303)))),
% 232.00/231.95 inference(scs_inference,[],[20,360])).
% 232.00/231.95 cnf(431,plain,
% 232.00/231.95 (~P1(f2(f1(f2(x4311,f1(f1(f2(x4311,x4312))))),f2(x4311,f1(f1(f2(x4311,x4312))))))+P1(f2(f2(x4313,x4314),f2(f1(f2(x4311,x4312)),x4314)))),
% 232.00/231.95 inference(scs_inference,[],[20,363])).
% 232.00/231.95 cnf(432,plain,
% 232.00/231.95 (~P1(f2(f1(f2(x4321,f1(f1(f2(x4321,x4322))))),f2(x4321,f1(f1(f2(x4321,x4322))))))+P1(f2(f1(f2(f1(f2(x4321,x4322)),x4323)),x4324))),
% 232.00/231.95 inference(scs_inference,[],[20,365])).
% 232.00/231.95 cnf(434,plain,
% 232.00/231.95 (P1(f2(f2(x4341,x4342),f2(f1(x4343),x4342)))+~P1(f2(f2(f2(f2(f1(x4344),x4345),x4346),f2(f1(f2(x4344,x4346)),x4347)),f2(f2(f1(f1(x4343)),x4348),x4343)))),
% 232.00/231.95 inference(scs_inference,[],[326,363,5])).
% 232.00/231.95 cnf(435,plain,
% 232.00/231.95 (~P1(f2(f1(f2(f1(x4351),x4351)),f2(f1(x4351),x4351)))+P1(f2(f1(f2(f1(f2(f1(x4351),x4352)),x4353)),x4354))),
% 232.00/231.95 inference(scs_inference,[],[194,365])).
% 232.00/231.95 cnf(436,plain,
% 232.00/231.95 (~P1(f2(f1(f2(f1(x4361),x4361)),f2(f1(x4361),x4361)))+~P1(f2(f2(f1(f1(f1(f2(f1(x4361),x4362)))),x4363),f1(f2(f1(x4361),x4362))))),
% 232.00/231.95 inference(scs_inference,[],[194,370])).
% 232.00/231.95 cnf(437,plain,
% 232.00/231.95 (P1(f2(x4371,f2(f1(x4372),x4373)))+~P1(f2(f2(f1(f1(x4372)),x4374),x4372))),
% 232.00/231.95 inference(scs_inference,[],[194,365])).
% 232.00/231.95 cnf(439,plain,
% 232.00/231.95 (~P1(f2(f1(f2(f1(x4391),x4391)),f2(f1(x4391),x4391)))+P1(f2(x4392,f2(f1(f2(f1(x4391),x4393)),x4394)))),
% 232.00/231.95 inference(scs_inference,[],[437,194])).
% 232.00/231.95 cnf(440,plain,
% 232.00/231.95 (P1(f2(x4401,f2(f1(x4402),x4403)))+~P1(f2(f2(f2(f1(f2(f1(x4404),x4404)),f2(f1(x4404),x4404)),f2(f1(x4404),x4405)),f2(f2(f1(f1(x4402)),x4406),x4402)))),
% 232.00/231.95 inference(scs_inference,[],[34,437,5])).
% 232.00/231.95 cnf(441,plain,
% 232.00/231.95 (P1(f2(x4411,f2(f1(x4412),x4413)))+~P1(f2(f2(f2(f2(f2(f1(x4414),x4414),x4415),x4416),f2(f2(x4414,x4415),x4416)),f2(f2(f1(f1(x4412)),x4417),x4412)))),
% 232.00/231.95 inference(scs_inference,[],[41,437,5])).
% 232.00/231.95 cnf(443,plain,
% 232.00/231.95 (P1(f2(f2(x4431,x4432),f2(x4433,x4432)))+~P1(f2(f2(x4434,f2(f1(x4434),x4435)),f2(f2(f1(f1(f2(x4433,x4431))),x4436),f2(x4433,x4431))))),
% 232.00/231.95 inference(scs_inference,[],[1,360,5])).
% 232.00/231.95 cnf(444,plain,
% 232.00/231.95 (P1(f2(f2(x4441,x4442),f2(x4443,x4442)))+~P1(f2(f2(f2(x4444,x4445),f2(f2(x4445,x4446),f2(x4444,x4446))),f2(f2(f1(f1(f2(x4443,x4441))),x4447),f2(x4443,x4441))))),
% 232.00/231.95 inference(scs_inference,[],[3,360,5])).
% 232.00/231.95 cnf(445,plain,
% 232.00/231.95 (P1(f2(f2(x4451,x4452),f2(x4453,x4452)))+~P1(f2(f2(f2(f1(x4454),x4454),f2(f1(x4454),x4455)),f2(f2(f1(f1(f2(x4453,x4451))),x4456),f2(x4453,x4451))))),
% 232.00/231.95 inference(scs_inference,[],[9,360,5])).
% 232.00/231.95 cnf(446,plain,
% 232.00/231.95 (P1(f2(f2(x4461,x4462),f2(x4463,x4462)))+~P1(f2(f2(f2(f1(f2(x4464,x4465)),f2(x4464,x4465)),f2(f2(x4465,x4466),f2(x4464,x4466))),f2(f2(f1(f1(f2(x4463,x4461))),x4467),f2(x4463,x4461))))),
% 232.00/231.95 inference(scs_inference,[],[17,360,5])).
% 232.00/231.95 cnf(447,plain,
% 232.00/231.95 (P1(f2(f2(x4471,x4472),f2(x4473,x4472)))+~P1(f2(f2(f2(f2(f1(x4474),x4475),x4476),f2(f2(f1(x4474),x4474),x4476)),f2(f2(f1(f1(f2(x4473,x4471))),x4477),f2(x4473,x4471))))),
% 232.00/231.95 inference(scs_inference,[],[25,360,5])).
% 232.00/231.95 cnf(448,plain,
% 232.00/231.95 (P1(f2(f2(x4481,x4482),f2(x4483,x4482)))+~P1(f2(f2(f2(f1(f2(f1(x4484),x4484)),f2(f1(x4484),x4484)),f2(f1(x4484),x4485)),f2(f2(f1(f1(f2(x4483,x4481))),x4486),f2(x4483,x4481))))),
% 232.00/231.95 inference(scs_inference,[],[34,360,5])).
% 232.00/231.95 cnf(449,plain,
% 232.00/231.95 (P1(f2(f2(x4491,x4492),f2(x4493,x4492)))+~P1(f2(f2(f2(f2(f2(f1(x4494),x4494),x4495),x4496),f2(f2(x4494,x4495),x4496)),f2(f2(f1(f1(f2(x4493,x4491))),x4497),f2(x4493,x4491))))),
% 232.00/231.95 inference(scs_inference,[],[41,360,5])).
% 232.00/231.95 cnf(452,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(f1(x4521))),x4522),f1(x4521)))+~P1(f2(f2(x4523,f2(f1(x4523),x4524)),f2(f1(f2(f1(x4521),x4521)),f2(f1(x4521),x4521))))),
% 232.00/231.95 inference(scs_inference,[],[1,369,5])).
% 232.00/231.95 cnf(453,plain,
% 232.00/231.95 (~P1(f2(f1(f2(f1(x4531),x4531)),f2(f1(x4531),x4531)))+~P1(f2(f2(f2(x4532,x4533),f2(f2(x4533,x4534),f2(x4532,x4534))),f2(f2(f1(f1(f1(x4531))),x4535),f1(x4531))))),
% 232.00/231.95 inference(scs_inference,[],[3,369,5])).
% 232.00/231.95 cnf(454,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(f1(x4541))),x4542),f1(x4541)))+~P1(f2(f2(f2(f1(x4543),x4543),f2(f1(x4543),x4544)),f2(f1(f2(f1(x4541),x4541)),f2(f1(x4541),x4541))))),
% 232.00/231.95 inference(scs_inference,[],[9,369,5])).
% 232.00/231.95 cnf(455,plain,
% 232.00/231.95 (~P1(f2(f1(f2(f1(x4551),x4551)),f2(f1(x4551),x4551)))+~P1(f2(f2(f2(f1(f2(x4552,x4553)),f2(x4552,x4553)),f2(f2(x4553,x4554),f2(x4552,x4554))),f2(f2(f1(f1(f1(x4551))),x4555),f1(x4551))))),
% 232.00/231.95 inference(scs_inference,[],[17,369,5])).
% 232.00/231.95 cnf(457,plain,
% 232.00/231.95 (~P1(f2(f1(f2(f1(x4571),x4571)),f2(f1(x4571),x4571)))+~P1(f2(f2(f2(f1(f2(f1(x4572),x4572)),f2(f1(x4572),x4572)),f2(f1(x4572),x4573)),f2(f2(f1(f1(f1(x4571))),x4574),f1(x4571))))),
% 232.00/231.95 inference(scs_inference,[],[34,369,5])).
% 232.00/231.95 cnf(459,plain,
% 232.00/231.95 (~P1(f2(f1(f2(f1(x4591),x4591)),f2(f1(x4591),x4591)))+~P1(f2(f2(f1(f2(f2(f2(f1(x4592),x4593),x4594),f2(x4592,x4594))),x4595),f2(f2(f1(f1(f1(x4591))),x4596),f1(x4591))))),
% 232.00/231.95 inference(scs_inference,[],[56,369,5])).
% 232.00/231.95 cnf(461,plain,
% 232.00/231.95 (~P1(f2(f1(f2(f1(x4611),x4611)),f2(f1(x4611),x4611)))+~P1(f2(f2(x4612,f2(f1(x4612),x4613)),f2(f2(f1(f1(f1(x4611))),x4614),f1(x4611))))),
% 232.00/231.95 inference(scs_inference,[],[1,369,5])).
% 232.00/231.95 cnf(462,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(f1(x4621))),x4622),f1(x4621)))+~P1(f2(f2(f2(x4623,x4624),f2(f2(x4624,x4625),f2(x4623,x4625))),f2(f1(f2(f1(x4621),x4621)),f2(f1(x4621),x4621))))),
% 232.00/231.95 inference(scs_inference,[],[3,369,5])).
% 232.00/231.95 cnf(463,plain,
% 232.00/231.95 (~P1(f2(f1(f2(f1(x4631),x4631)),f2(f1(x4631),x4631)))+~P1(f2(f2(f2(f1(x4632),x4632),f2(f1(x4632),x4633)),f2(f2(f1(f1(f1(x4631))),x4634),f1(x4631))))),
% 232.00/231.95 inference(scs_inference,[],[9,369,5])).
% 232.00/231.95 cnf(464,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(f1(x4641))),x4642),f1(x4641)))+~P1(f2(f2(f2(f1(f2(x4643,x4644)),f2(x4643,x4644)),f2(f2(x4644,x4645),f2(x4643,x4645))),f2(f1(f2(f1(x4641),x4641)),f2(f1(x4641),x4641))))),
% 232.00/231.95 inference(scs_inference,[],[17,369,5])).
% 232.00/231.95 cnf(468,plain,
% 232.00/231.95 (~P1(f2(f1(f2(f1(x4681),x4681)),f2(f1(x4681),x4681)))+~P1(f2(f2(f2(f2(f1(x4682),x4683),x4684),f2(f1(f2(x4682,x4684)),x4685)),f2(f1(f2(f1(f1(x4681)),f1(x4681))),f2(f1(f1(x4681)),f1(x4681)))))),
% 232.00/231.95 inference(scs_inference,[],[326,67,5])).
% 232.00/231.95 cnf(469,plain,
% 232.00/231.95 (P1(f2(x4691,f2(f1(x4692),x4693)))+~P1(f2(f2(f1(f1(f2(x4691,x4692))),x4694),f2(x4691,x4692)))),
% 232.00/231.95 inference(scs_inference,[],[318,365])).
% 232.00/231.95 cnf(470,plain,
% 232.00/231.95 (P1(f2(x4701,f2(f1(x4702),x4703)))+~P1(f2(f2(f2(x4704,x4705),f2(f2(x4705,x4706),f2(x4704,x4706))),f2(f2(f1(f1(f2(x4701,x4702))),x4707),f2(x4701,x4702))))),
% 232.00/231.95 inference(scs_inference,[],[3,469,5])).
% 232.00/231.95 cnf(474,plain,
% 232.00/231.95 (P1(f2(x4741,f2(f1(x4742),x4743)))+~P1(f2(f2(f2(f2(f1(x4744),x4745),x4746),f2(f2(f1(x4744),x4744),x4746)),f2(f2(f1(f1(f2(x4741,x4742))),x4747),f2(x4741,x4742))))),
% 232.00/231.95 inference(scs_inference,[],[25,469,5])).
% 232.00/231.95 cnf(478,plain,
% 232.00/231.95 (P1(f2(x4781,f2(f1(x4782),x4783)))+~P1(f2(f2(f2(f2(f1(x4784),x4785),x4786),f2(f1(f2(x4784,x4786)),x4787)),f2(f2(f1(f1(f2(x4781,x4782))),x4788),f2(x4781,x4782))))),
% 232.00/231.95 inference(scs_inference,[],[326,469,5])).
% 232.00/231.95 cnf(479,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(f2(f2(x4791,f2(f1(x4791),x4792)),x4793))),x4794),f2(f2(x4791,f2(f1(x4791),x4792)),x4793)))+P1(f2(f1(x4793),x4795))),
% 232.00/231.95 inference(scs_inference,[],[1,469,5])).
% 232.00/231.95 cnf(480,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(f2(f2(f2(x4801,x4802),f2(f2(x4802,x4803),f2(x4801,x4803))),x4804))),x4805),f2(f2(f2(x4801,x4802),f2(f2(x4802,x4803),f2(x4801,x4803))),x4804)))+P1(f2(f1(x4804),x4806))),
% 232.00/231.95 inference(scs_inference,[],[3,469,5])).
% 232.00/231.95 cnf(486,plain,
% 232.00/231.95 (P1(f2(f1(f2(f2(x4861,x4862),f2(x4863,x4862))),x4864))+~P1(f2(f2(f1(f1(f2(x4863,x4861))),x4865),f2(x4863,x4861)))),
% 232.00/231.95 inference(scs_inference,[],[166,365])).
% 232.00/231.95 cnf(487,plain,
% 232.00/231.95 (P1(f2(f2(f2(x4871,x4872),x4873),f2(f2(x4874,x4872),x4873)))+~P1(f2(f2(f1(f1(f2(x4871,x4874))),x4875),f2(x4871,x4874)))),
% 232.00/231.95 inference(scs_inference,[],[486,20])).
% 232.00/231.95 cnf(488,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(f2(x4881,x4882))),x4883),f2(x4881,x4882)))+~P1(f2(f2(f2(f2(x4881,x4884),x4885),f2(f2(x4882,x4884),x4885)),f1(f2(f2(f2(f1(x4886),x4887),x4888),f2(x4886,x4888)))))),
% 232.00/231.95 inference(scs_inference,[],[59,487,5])).
% 232.00/231.95 cnf(491,plain,
% 232.00/231.95 (~P1(f2(f1(f2(f1(x4911),x4911)),f2(f1(x4911),x4911)))+P1(f2(f1(f2(f2(x4912,x4913),f2(f1(x4911),x4913))),x4914))),
% 232.00/231.95 inference(scs_inference,[],[486,194])).
% 232.00/231.95 cnf(494,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(f2(x4941,x4942))),x4943),f2(x4941,x4942)))+~P1(f2(f2(f1(f2(f2(x4942,x4944),f2(x4941,x4944))),x4945),f2(f2(f1(a3),f1(f2(a4,a4))),a3)))),
% 232.00/231.95 inference(scs_inference,[],[4,486,5])).
% 232.00/231.95 cnf(495,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(f2(x4951,x4952))),x4953),f2(x4951,x4952)))+~P1(f2(f2(f1(f2(f2(x4952,x4954),f2(x4951,x4954))),x4955),f2(f2(f2(f1(f1(a3)),f1(a3)),f1(f2(a4,a4))),a3)))),
% 232.00/231.95 inference(scs_inference,[],[44,486,5])).
% 232.00/231.95 cnf(499,plain,
% 232.00/231.95 (P1(f2(f1(f2(f2(x4991,x4992),f2(x4993,x4992))),x4994))+~P1(f2(f2(f2(f1(x4995),x4995),f2(f1(x4995),x4996)),f2(f2(f1(f1(f2(x4993,x4991))),x4997),f2(x4993,x4991))))),
% 232.00/231.95 inference(scs_inference,[],[9,486,5])).
% 232.00/231.95 cnf(500,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(f2(x5001,x5002))),x5003),f2(x5001,x5002)))+~P1(f1(f2(f2(x5002,x5004),f2(x5001,x5004))))),
% 232.00/231.95 inference(scs_inference,[],[4,486,5])).
% 232.00/231.95 cnf(503,plain,
% 232.00/231.95 (~P1(f1(f2(f2(x5031,x5032),f2(x5033,x5032))))+~P1(f2(f2(f2(f1(x5034),x5034),f2(f2(x5035,x5036),f2(f1(x5034),x5036))),f2(f2(f1(f1(f2(x5033,x5031))),x5037),f2(x5033,x5031))))),
% 232.00/231.95 inference(scs_inference,[],[28,500,5])).
% 232.00/231.95 cnf(504,plain,
% 232.00/231.95 (~P1(f2(f1(f2(f1(f2(x5041,x5042)),f2(x5041,x5042))),f2(f1(f2(x5041,x5042)),f2(x5041,x5042))))+~P1(f1(f2(f2(x5042,x5043),f2(x5041,x5043))))),
% 232.00/231.95 inference(scs_inference,[],[500,53])).
% 232.00/231.95 cnf(506,plain,
% 232.00/231.95 (P1(f2(f2(f2(f1(f2(f2(f2(f1(x5061),x5062),x5063),f2(x5061,x5063))),x5064),x5065),f2(f2(x5066,x5064),x5065)))),
% 232.00/231.95 inference(scs_inference,[],[56,487,32])).
% 232.00/231.95 cnf(507,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(f2(x5071,x5072))),x5073),f2(x5071,x5072)))+~P1(f2(f2(f2(f2(x5071,x5074),x5075),f2(f2(x5072,x5074),x5075)),f2(f2(f1(a3),f1(f2(a4,a4))),a3)))),
% 232.00/231.95 inference(scs_inference,[],[4,487,5])).
% 232.00/231.95 cnf(508,plain,
% 232.00/231.95 (~P1(f2(f1(f2(f1(x5081),x5081)),f2(f1(x5081),x5081)))+P1(f2(f2(f2(f1(x5081),x5082),x5083),f2(f2(x5084,x5082),x5083)))),
% 232.00/231.95 inference(scs_inference,[],[487,194])).
% 232.00/231.95 cnf(509,plain,
% 232.00/231.95 (P1(f2(f2(f2(f1(x5091),x5092),x5093),f2(f2(x5094,x5092),x5093)))+~P1(f2(f2(f1(f1(f2(f1(x5091),x5091))),x5095),f2(f1(x5091),x5091)))),
% 232.00/231.95 inference(scs_inference,[],[508,358])).
% 232.00/231.95 cnf(510,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(f2(x5101,x5102))),x5103),f2(x5101,x5102)))+~P1(f2(f2(f2(f2(x5101,x5104),x5105),f2(f2(x5102,x5104),x5105)),f2(f2(f2(f1(f1(a3)),f1(a3)),f1(f2(a4,a4))),a3)))),
% 232.00/231.95 inference(scs_inference,[],[44,487,5])).
% 232.00/231.95 cnf(511,plain,
% 232.00/231.95 (P1(f2(f2(f2(f1(x5111),x5112),x5113),f2(f2(x5114,x5112),x5113)))+~P1(f2(f2(f1(f1(x5111)),x5115),x5111))),
% 232.00/231.95 inference(scs_inference,[],[487,437])).
% 232.00/231.95 cnf(512,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(x5121)),x5122),x5121))+~P1(f2(f2(f2(f2(f1(x5121),x5123),x5124),f2(f2(x5125,x5123),x5124)),f1(f2(f2(f2(f1(x5126),x5127),x5128),f2(x5126,x5128)))))),
% 232.00/231.95 inference(scs_inference,[],[59,511,5])).
% 232.00/231.95 cnf(514,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(x5141)),x5142),x5141))+~P1(f2(f2(f2(f2(f1(x5141),x5143),x5144),f2(f2(x5145,x5143),x5144)),f2(f2(f2(f1(f1(a3)),f1(a3)),f1(f2(a4,a4))),a3)))),
% 232.00/231.95 inference(scs_inference,[],[44,511,5])).
% 232.00/231.95 cnf(515,plain,
% 232.00/231.95 (P1(f2(f2(f2(f1(x5151),x5152),x5153),f2(f2(x5154,x5152),x5153)))+~P1(f2(f2(f2(f2(f2(f1(x5155),x5155),x5156),x5157),f2(f2(x5155,x5156),x5157)),f2(f2(f1(f1(x5151)),x5158),x5151)))),
% 232.00/231.95 inference(scs_inference,[],[41,511,5])).
% 232.00/231.95 cnf(516,plain,
% 232.00/231.95 (P1(f2(f2(x5161,x5162),f2(f2(f1(f1(x5162)),f1(x5162)),x5163)))+~P1(f2(f2(f1(f1(x5162)),x5164),x5162))),
% 232.00/231.95 inference(scs_inference,[],[37,511,5])).
% 232.00/231.95 cnf(518,plain,
% 232.00/231.95 (P1(f2(f2(f2(f1(x5181),x5182),x5183),f2(f2(x5184,x5182),x5183)))+~P1(f2(f2(f2(f2(f1(x5185),x5186),x5187),f2(f1(f2(x5185,x5187)),x5188)),f2(f2(f1(f1(x5181)),x5189),x5181)))),
% 232.00/231.95 inference(scs_inference,[],[326,511,5])).
% 232.00/231.95 cnf(519,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(x5191)),x5192),x5191))+~P1(f2(f2(f1(x5191),f1(f2(a4,a4))),a3))),
% 232.00/231.95 inference(scs_inference,[],[4,511,5])).
% 232.00/231.95 cnf(521,plain,
% 232.00/231.95 (~P1(f2(f1(f2(a4,a4)),f2(a4,a4)))+~P1(f2(f2(f1(f1(f1(f2(a4,a4)))),x5211),f1(f2(a4,a4))))),
% 232.00/231.95 inference(scs_inference,[],[519,51])).
% 232.00/231.95 cnf(523,plain,
% 232.00/231.95 (~P1(f2(f2(f1(f1(x5231)),x5232),x5231))+~P1(f2(f2(f1(f2(f1(x5231),x5233)),f1(f2(a4,a4))),a3))),
% 232.00/231.95 inference(scs_inference,[],[519,437])).
% 232.00/231.96 cnf(524,plain,
% 232.00/231.96 (~P1(f2(f2(f1(f2(f1(x5241),x5242)),f1(f2(a4,a4))),a3))+~P1(f2(f2(f2(f1(f2(x5243,x5244)),f2(x5243,x5244)),f2(f2(x5244,x5245),f2(x5243,x5245))),f2(f2(f1(f1(x5241)),x5246),x5241)))),
% 232.00/231.96 inference(scs_inference,[],[17,523,5])).
% 232.00/231.96 cnf(526,plain,
% 232.00/231.96 (~P1(f2(f2(f1(x5261),f1(f2(a4,a4))),a3))+~P1(f2(f2(f2(f1(f2(f1(x5262),x5262)),f2(f1(x5262),x5262)),f2(f1(x5262),x5263)),f2(f2(f1(f1(x5261)),x5264),x5261)))),
% 232.00/231.96 inference(scs_inference,[],[34,519,5])).
% 232.00/231.96 cnf(527,plain,
% 232.00/231.96 (~P1(f2(f2(f1(x5271),f1(f2(a4,a4))),a3))+~P1(f2(f2(f2(f2(f2(f1(x5272),x5272),x5273),x5274),f2(f2(x5272,x5273),x5274)),f2(f2(f1(f1(x5271)),x5275),x5271)))),
% 232.00/231.96 inference(scs_inference,[],[41,519,5])).
% 232.00/231.96 cnf(528,plain,
% 232.00/231.96 (P1(f2(f2(x5281,x5282),f2(f2(f1(f1(x5282)),f1(x5282)),x5283)))+~P1(f2(f2(f2(f2(f1(x5284),x5285),x5286),f2(f1(f2(x5284,x5286)),x5287)),f2(f2(f1(f1(x5282)),x5288),x5282)))),
% 232.00/231.96 inference(scs_inference,[],[326,516,5])).
% 232.00/231.96 cnf(530,plain,
% 232.00/231.96 (P1(f2(f2(x5301,x5302),f2(f2(f1(f1(x5302)),f1(x5302)),x5303)))+~P1(f2(f2(f2(x5304,x5305),f2(f2(x5305,x5306),f2(x5304,x5306))),f2(f2(f1(f1(x5302)),x5307),x5302)))),
% 232.00/231.96 inference(scs_inference,[],[3,516,5])).
% 232.00/231.96 cnf(532,plain,
% 232.00/231.96 (P1(f2(f2(x5321,x5322),f2(f2(f1(f1(x5322)),f1(x5322)),x5323)))+~P1(f2(f2(f2(f1(f2(x5324,x5325)),f2(x5324,x5325)),f2(f2(x5325,x5326),f2(x5324,x5326))),f2(f2(f1(f1(x5322)),x5327),x5322)))),
% 232.00/231.96 inference(scs_inference,[],[17,516,5])).
% 232.00/231.96 cnf(533,plain,
% 232.00/231.96 (P1(f2(f2(x5331,x5332),f2(f2(f1(f1(x5332)),f1(x5332)),x5333)))+~P1(f2(f2(f2(f2(f1(x5334),x5335),x5336),f2(f2(f1(x5334),x5334),x5336)),f2(f2(f1(f1(x5332)),x5337),x5332)))),
% 232.00/231.96 inference(scs_inference,[],[25,516,5])).
% 232.00/231.96 cnf(534,plain,
% 232.00/231.96 (P1(f2(f2(x5341,x5342),f2(f2(f1(f1(x5342)),f1(x5342)),x5343)))+~P1(f2(f2(f2(f1(f2(f1(x5344),x5344)),f2(f1(x5344),x5344)),f2(f1(x5344),x5345)),f2(f2(f1(f1(x5342)),x5346),x5342)))),
% 232.00/231.96 inference(scs_inference,[],[34,516,5])).
% 232.00/231.96 cnf(535,plain,
% 232.00/231.96 (P1(f2(f2(x5351,x5352),f2(f2(f1(f1(x5352)),f1(x5352)),x5353)))+~P1(f2(f2(f2(f2(f2(f1(x5354),x5354),x5355),x5356),f2(f2(x5354,x5355),x5356)),f2(f2(f1(f1(x5352)),x5357),x5352)))),
% 232.00/231.96 inference(scs_inference,[],[41,516,5])).
% 232.00/231.96 cnf(536,plain,
% 232.00/231.96 (~P1(f2(f2(f1(f1(x5361)),x5362),x5361))+~P1(f2(f2(f2(f2(f1(x5363),x5364),x5365),f2(f1(f2(x5363,x5365)),x5366)),f2(f2(f1(f2(f1(x5361),x5367)),f1(f2(a4,a4))),a3)))),
% 232.00/231.96 inference(scs_inference,[],[326,523,5])).
% 232.00/231.96 cnf(538,plain,
% 232.00/231.96 (~P1(f2(f2(f1(f1(x5381)),x5382),x5381))+~P1(f2(f2(f2(f1(x5383),x5383),x5383),f2(f2(f1(f2(f1(x5381),x5384)),f1(f2(a4,a4))),a3)))),
% 232.00/231.96 inference(scs_inference,[],[2,523,5])).
% 232.00/231.96 cnf(539,plain,
% 232.00/231.96 (~P1(f2(f2(f1(f2(f1(x5391),x5392)),f1(f2(a4,a4))),a3))+~P1(f2(f2(f2(x5393,x5394),f2(f2(f1(x5393),x5393),x5394)),f2(f2(f1(f1(x5391)),x5395),x5391)))),
% 232.00/231.96 inference(scs_inference,[],[6,523,5])).
% 232.00/231.96 cnf(545,plain,
% 232.00/231.96 (~P1(f2(f2(f1(f2(f1(x5451),x5452)),f1(f2(a4,a4))),a3))+~P1(f2(f2(f2(f1(f2(f1(x5453),x5453)),f2(f1(x5453),x5453)),x5453),f2(f2(f1(f1(x5451)),x5454),x5451)))),
% 232.00/231.96 inference(scs_inference,[],[22,523,5])).
% 232.00/231.96 cnf(566,plain,
% 232.00/231.96 (P1(f2(f2(f2(f1(f2(x5661,x5662)),x5663),x5664),f2(f2(f2(f1(x5661),x5665),x5662),x5664)))),
% 232.00/231.96 inference(scs_inference,[],[1,215,5])).
% 232.00/231.96 cnf(572,plain,
% 232.00/231.96 (P1(f2(f1(f2(f2(f1(x5721),x5721),x5721)),x5722))),
% 232.00/231.96 inference(scs_inference,[],[2,1,5])).
% 232.00/231.96 cnf(576,plain,
% 232.00/231.96 (P1(f2(f1(f2(x5761,x5761)),x5762))),
% 232.00/231.96 inference(scs_inference,[],[2,326,5])).
% 232.00/231.96 cnf(579,plain,
% 232.00/231.96 (~P1(f2(f2(f1(f1(f1(f2(a4,a4)))),x5791),f1(f2(a4,a4))))),
% 232.00/231.96 inference(scs_inference,[],[2,326,5,521])).
% 232.00/231.96 cnf(600,plain,
% 232.00/231.96 (P1(f2(f2(f1(f1(f2(x6001,x6001))),f1(f2(x6001,x6001))),x6002))),
% 232.00/231.96 inference(scs_inference,[],[576,51])).
% 232.00/231.96 cnf(615,plain,
% 232.00/231.96 (~P1(f2(f2(f2(x6151,x6152),f2(x6151,x6152)),f2(f2(f2(f1(f1(a3)),f1(a3)),f1(f2(a4,a4))),a3)))),
% 232.00/231.96 inference(scs_inference,[],[6,576,579,51,500,390,510,5,415,417])).
% 232.00/231.96 cnf(632,plain,
% 232.00/231.96 (~P1(f2(f1(f1(f2(x6321,x6321))),f1(f2(x6321,x6321))))),
% 232.00/231.96 inference(scs_inference,[],[59,600,5])).
% 232.00/231.96 cnf(644,plain,
% 232.00/231.96 (P1(f2(f1(f2(x6441,f2(f2(x6442,x6443),f2(f1(x6441),x6443)))),x6444))),
% 232.00/231.96 inference(scs_inference,[],[3,326,5])).
% 232.00/231.96 cnf(649,plain,
% 232.00/231.96 (P1(f2(f2(f2(f2(x6491,x6492),f2(x6493,x6492)),x6494),f2(f2(f2(f1(x6493),x6495),x6491),x6494)))),
% 232.00/231.96 inference(scs_inference,[],[3,215,5])).
% 232.00/231.96 cnf(653,plain,
% 232.00/231.96 (~P1(f2(f2(f2(f1(f2(a4,a4)),x6531),f2(f1(a3),x6531)),a3))),
% 232.00/231.96 inference(scs_inference,[],[44,649,5])).
% 232.00/231.96 cnf(682,plain,
% 232.00/231.96 (P1(f2(x6821,f2(f2(f1(f1(x6821)),f1(x6821)),x6822)))),
% 232.00/231.96 inference(scs_inference,[],[6,14,5])).
% 232.00/231.96 cnf(686,plain,
% 232.00/231.96 (P1(f2(f2(f2(f1(x6861),x6862),x6863),f2(f2(f1(f2(x6863,x6864)),f2(x6863,x6864)),f2(x6861,x6864))))),
% 232.00/231.96 inference(scs_inference,[],[6,649,5])).
% 232.00/231.96 cnf(726,plain,
% 232.00/231.96 (P1(f2(f2(f2(f1(f2(f1(x7261),x7262)),x7263),x7264),f2(x7261,x7264)))),
% 232.00/231.96 inference(scs_inference,[],[56,80,5])).
% 232.00/231.96 cnf(730,plain,
% 232.00/231.96 (P1(f2(x7301,f2(f1(f2(f1(x7301),x7302)),x7303)))),
% 232.00/231.96 inference(scs_inference,[],[9,726,5])).
% 232.00/231.96 cnf(782,plain,
% 232.00/231.96 (P1(f2(x7821,f2(f2(x7822,x7823),f2(f1(x7821),x7823))))),
% 232.00/231.96 inference(scs_inference,[],[17,726,5])).
% 232.00/231.96 cnf(811,plain,
% 232.00/231.96 (P1(f2(f2(f2(f1(x8111),x8112),x8113),f2(f2(x8113,x8114),f2(x8111,x8114))))),
% 232.00/231.96 inference(scs_inference,[],[17,566,5])).
% 232.00/231.96 cnf(815,plain,
% 232.00/231.96 (P1(f2(f2(f2(f2(x8151,x8152),f2(x8153,x8152)),x8154),f2(f2(x8153,x8151),x8154)))),
% 232.00/231.96 inference(scs_inference,[],[17,811,5])).
% 232.00/231.96 cnf(878,plain,
% 232.00/231.96 (P1(f2(x8781,f2(f2(x8782,x8783),f2(f1(f2(f1(x8781),x8784)),x8783))))),
% 232.00/231.96 inference(scs_inference,[],[28,726,5])).
% 232.00/231.96 cnf(882,plain,
% 232.00/231.96 (P1(f2(f2(f2(f1(x8821),x8822),x8823),f2(f2(x8824,x8825),f2(f1(f2(x8821,x8823)),x8825))))),
% 232.00/231.96 inference(scs_inference,[],[28,566,5])).
% 232.00/231.96 cnf(907,plain,
% 232.00/231.96 (P1(f2(f2(f2(f1(x9071),x9072),x9073),f2(f2(f1(f1(f2(x9071,x9073))),f1(f2(x9071,x9073))),x9074)))),
% 232.00/231.96 inference(scs_inference,[],[37,566,5])).
% 232.00/231.96 cnf(936,plain,
% 232.00/231.96 (P1(f2(f2(x9361,f2(f1(x9362),x9362)),f2(f2(x9362,x9363),f2(x9361,x9363))))),
% 232.00/231.96 inference(scs_inference,[],[41,815,5])).
% 232.00/231.96 cnf(948,plain,
% 232.00/231.96 (P1(f2(f2(f2(f1(f2(f2(f1(x9481),x9481),x9481)),x9482),x9483),f2(f2(x9484,x9482),x9483)))),
% 232.00/231.96 inference(scs_inference,[],[730,508,273])).
% 232.00/231.96 cnf(985,plain,
% 232.00/231.96 (P1(f2(f2(f2(f1(x9851),x9852),f2(f2(f1(x9853),x9854),x9855)),f2(f2(f2(x9853,x9855),x9856),f2(x9851,x9856))))),
% 232.00/231.96 inference(scs_inference,[],[255,649,5])).
% 232.00/231.96 cnf(990,plain,
% 232.00/231.96 (P1(f2(f2(x9901,f2(f2(f1(x9902),x9903),x9904)),f2(f2(f2(x9902,x9904),x9905),f2(x9901,x9905))))),
% 232.00/231.96 inference(scs_inference,[],[255,815,5])).
% 232.00/231.96 cnf(1073,plain,
% 232.00/231.96 (P1(f2(f2(x10731,x10732),f2(f1(f2(f2(f1(x10733),x10733),x10733)),x10732)))),
% 232.00/231.96 inference(scs_inference,[],[572,3,5])).
% 232.00/231.96 cnf(1087,plain,
% 232.00/231.96 (P1(f2(x10871,f2(f1(f2(x10872,x10872)),x10873)))),
% 232.00/231.96 inference(scs_inference,[],[576,3,5,500,372])).
% 232.00/231.96 cnf(1093,plain,
% 232.00/231.96 (P1(f2(f2(f2(f1(f2(x10931,x10931)),x10932),x10933),f2(f2(x10934,x10932),x10933)))),
% 232.00/231.96 inference(scs_inference,[],[576,3,5,500,372,374,376,508])).
% 232.00/231.96 cnf(1097,plain,
% 232.00/231.96 (P1(f2(x10971,f2(f1(f2(f1(f2(x10972,x10972)),x10973)),x10974)))),
% 232.00/231.96 inference(scs_inference,[],[576,3,5,500,372,374,376,508,499,439])).
% 232.00/231.96 cnf(1099,plain,
% 232.00/231.96 (P1(f2(f2(x10991,x10992),f2(f2(f1(f1(f2(x10993,x10993))),f1(f2(x10993,x10993))),x10992)))),
% 232.00/231.96 inference(scs_inference,[],[576,3,5,500,372,374,376,508,499,439,291])).
% 232.00/231.96 cnf(1101,plain,
% 232.00/231.96 (P1(f2(f2(x11011,x11012),f2(f2(x11012,x11013),f2(f1(f2(x11014,x11014)),x11013))))),
% 232.00/231.96 inference(scs_inference,[],[576,3,5,500,372,374,376,508,499,439,291,185])).
% 232.00/231.96 cnf(1160,plain,
% 232.00/231.96 (~P1(f2(f2(f1(f2(x11601,x11601)),f2(x11602,x11603)),f2(f2(f2(f1(f1(a3)),f1(a3)),f1(f2(a4,a4))),a3)))),
% 232.00/231.96 inference(scs_inference,[],[615,1093,5])).
% 232.00/231.96 cnf(1173,plain,
% 232.00/231.96 (~P1(f2(f2(x11731,x11731),f2(f2(f2(f1(f1(a3)),f1(a3)),f1(f2(a4,a4))),a3)))),
% 232.00/231.96 inference(scs_inference,[],[6,1160,5])).
% 232.00/231.96 cnf(1186,plain,
% 232.00/231.96 (~P1(f2(f2(f2(f1(f1(a3)),f1(a3)),f1(f2(a4,a4))),f2(f1(a3),a3)))),
% 232.00/231.96 inference(scs_inference,[],[936,1173,5])).
% 232.00/231.96 cnf(1396,plain,
% 232.00/231.96 (P1(f2(f2(f2(x13961,f2(x13962,x13963)),x13964),f2(f2(f2(f1(x13962),x13965),f1(x13961)),x13964)))),
% 232.00/231.96 inference(scs_inference,[],[811,990,5])).
% 232.00/231.96 cnf(1414,plain,
% 232.00/231.96 (P1(f2(f2(f2(x14141,f2(f1(f2(x14142,x14142)),x14143)),x14144),f2(x14145,x14144)))),
% 232.00/231.96 inference(scs_inference,[],[1101,985,5])).
% 232.00/231.96 cnf(1469,plain,
% 232.00/231.96 (~P1(f2(f2(x14691,f2(f1(f2(x14692,x14692)),x14693)),f2(f1(a3),a3)))),
% 232.00/231.96 inference(scs_inference,[],[1186,1414,5])).
% 232.00/231.96 cnf(1473,plain,
% 232.00/231.96 (~P1(f2(f2(f2(f1(x14731),x14731),x14731),f2(f1(f2(f1(a3),a3)),f2(f1(a3),a3))))),
% 232.00/231.96 inference(scs_inference,[],[1469,98])).
% 232.00/231.96 cnf(1480,plain,
% 232.00/231.96 (~P1(f2(f2(f1(f1(a3)),x14801),f1(f2(x14802,x14802))))),
% 232.00/231.96 inference(scs_inference,[],[686,1469,5])).
% 232.00/231.96 cnf(1484,plain,
% 232.00/231.96 (~P1(f2(f2(f1(f2(x14841,x14841)),x14842),f2(f1(a3),a3)))),
% 232.00/231.96 inference(scs_inference,[],[6,1469,5])).
% 232.00/231.96 cnf(1491,plain,
% 232.00/231.96 (~P1(f2(f2(f2(a4,a4),f2(f1(a3),x14911)),f2(f1(a3),a3)))),
% 232.00/231.96 inference(scs_inference,[],[1186,1396,1484,20,5])).
% 232.00/231.96 cnf(1570,plain,
% 232.00/231.96 (~P1(f2(f2(f2(f1(x15701),x15701),x15701),f2(f1(f1(f2(x15702,x15702))),f1(f2(x15702,x15702)))))),
% 232.00/231.96 inference(scs_inference,[],[632,2,5])).
% 232.00/231.96 cnf(1692,plain,
% 232.00/231.96 (~P1(f2(f2(f2(f1(x16921),x16921),x16921),f2(f2(f2(a4,a4),f2(f1(a3),x16922)),f2(f1(a3),a3))))),
% 232.00/231.96 inference(scs_inference,[],[2,1491,5])).
% 232.00/231.96 cnf(1694,plain,
% 232.00/231.96 (~P1(f2(f2(f2(f1(x16941),x16941),x16941),f2(f2(f1(f1(a3)),x16942),f1(f2(x16943,x16943)))))),
% 232.00/231.96 inference(scs_inference,[],[2,1480,5])).
% 232.00/231.96 cnf(1800,plain,
% 232.00/231.96 (~P1(f2(f2(f2(f1(x18001),x18001),x18001),f2(f2(f1(f1(a3)),x18002),f1(f2(x18003,x18003)))))),
% 232.00/231.96 inference(rename_variables,[],[1694])).
% 232.00/231.96 cnf(1803,plain,
% 232.00/231.96 (~P1(f2(f2(f2(f1(x18031),x18031),x18031),f2(f2(f1(f1(a3)),x18032),f1(f2(x18033,x18033)))))),
% 232.00/231.96 inference(rename_variables,[],[1694])).
% 232.00/231.96 cnf(1806,plain,
% 232.00/231.96 (~P1(f2(f2(f2(f1(x18061),x18061),x18061),f2(f2(f1(f1(a3)),x18062),f1(f2(x18063,x18063)))))),
% 232.00/231.96 inference(rename_variables,[],[1694])).
% 232.00/231.96 cnf(1809,plain,
% 232.00/231.96 (~P1(f2(f2(f2(f1(x18091),x18091),x18091),f2(f2(f1(f1(a3)),x18092),f1(f2(x18093,x18093)))))),
% 232.00/231.96 inference(rename_variables,[],[1694])).
% 232.00/231.96 cnf(1812,plain,
% 232.00/231.96 (~P1(f2(f2(f2(f1(x18121),x18121),x18121),f2(f2(f1(f1(a3)),x18122),f1(f2(x18123,x18123)))))),
% 232.00/231.96 inference(rename_variables,[],[1694])).
% 232.00/231.96 cnf(1815,plain,
% 232.00/231.96 (~P1(f2(f2(f2(f1(x18151),x18151),x18151),f2(f2(f1(f1(a3)),x18152),f1(f2(x18153,x18153)))))),
% 232.00/231.96 inference(rename_variables,[],[1694])).
% 232.00/231.96 cnf(1818,plain,
% 232.00/231.96 (~P1(f2(f2(f2(f1(x18181),x18181),x18181),f2(f2(f1(f1(a3)),x18182),f1(f2(x18183,x18183)))))),
% 232.00/231.96 inference(rename_variables,[],[1694])).
% 232.00/231.96 cnf(1821,plain,
% 232.00/231.96 (~P1(f2(f2(f2(f1(x18211),x18211),x18211),f2(f2(f1(f1(a3)),x18212),f1(f2(x18213,x18213)))))),
% 232.00/231.96 inference(rename_variables,[],[1694])).
% 232.00/231.96 cnf(1824,plain,
% 232.00/231.96 (~P1(f2(f2(f2(f1(x18241),x18241),x18241),f2(f2(f1(f1(a3)),x18242),f1(f2(x18243,x18243)))))),
% 232.00/231.96 inference(rename_variables,[],[1694])).
% 232.00/231.96 cnf(1827,plain,
% 232.00/231.96 (P1(f2(x18271,f2(f2(x18272,x18273),f2(f1(x18271),x18273))))),
% 232.00/231.96 inference(rename_variables,[],[782])).
% 232.00/231.96 cnf(1830,plain,
% 232.00/231.96 (P1(f2(x18301,f2(f2(x18302,x18303),f2(f1(x18301),x18303))))),
% 232.00/231.96 inference(rename_variables,[],[782])).
% 232.00/231.96 cnf(1833,plain,
% 232.00/231.96 (P1(f2(x18331,f2(f2(x18332,x18333),f2(f1(x18331),x18333))))),
% 232.00/231.96 inference(rename_variables,[],[782])).
% 232.00/231.96 cnf(1836,plain,
% 232.00/231.96 (P1(f2(x18361,f2(f2(x18362,x18363),f2(f1(x18361),x18363))))),
% 232.00/231.96 inference(rename_variables,[],[782])).
% 232.00/231.96 cnf(1839,plain,
% 232.00/231.96 (P1(f2(x18391,f2(f2(x18392,x18393),f2(f1(x18391),x18393))))),
% 232.00/231.96 inference(rename_variables,[],[782])).
% 232.00/231.96 cnf(1842,plain,
% 232.00/231.96 (P1(f2(f2(f2(x18421,f2(f1(f2(x18422,x18422)),x18423)),x18424),f2(x18425,x18424)))),
% 232.00/231.96 inference(rename_variables,[],[1414])).
% 232.00/231.96 cnf(1845,plain,
% 232.00/231.96 (P1(f2(f2(f2(f1(x18451),x18452),x18453),f2(f2(f1(f1(f2(x18451,x18453))),f1(f2(x18451,x18453))),x18454)))),
% 232.00/231.96 inference(rename_variables,[],[907])).
% 232.00/231.96 cnf(1848,plain,
% 232.00/231.96 (P1(f2(x18481,f2(f1(f2(x18482,x18482)),x18483)))),
% 232.00/231.96 inference(rename_variables,[],[1087])).
% 232.00/231.96 cnf(1851,plain,
% 232.00/231.96 (~P1(f2(f2(f2(f1(x18511),x18511),x18511),f2(f1(f2(f1(a3),a3)),f2(f1(a3),a3))))),
% 232.00/231.96 inference(rename_variables,[],[1473])).
% 232.00/231.96 cnf(1862,plain,
% 232.00/231.96 (P1(f2(x18621,f2(f1(f2(x18622,x18622)),x18623)))),
% 232.00/231.96 inference(rename_variables,[],[1087])).
% 232.00/231.96 cnf(1865,plain,
% 232.00/231.96 (P1(f2(f2(f2(f1(x18651),x18652),x18653),f2(f2(f1(f1(f2(x18651,x18653))),f1(f2(x18651,x18653))),x18654)))),
% 232.00/231.96 inference(rename_variables,[],[907])).
% 232.00/231.96 cnf(1868,plain,
% 232.00/231.96 (P1(f2(f2(x18681,x18682),f2(f2(x18682,x18683),f2(f1(f2(x18684,x18684)),x18683))))),
% 232.00/231.96 inference(rename_variables,[],[1101])).
% 232.00/231.96 cnf(1871,plain,
% 232.00/231.96 (P1(f2(x18711,f2(f2(x18712,x18713),f2(f1(x18711),x18713))))),
% 232.00/231.96 inference(rename_variables,[],[782])).
% 232.00/231.96 cnf(1874,plain,
% 232.00/231.96 (P1(f2(x18741,f2(f2(x18742,x18743),f2(f1(x18741),x18743))))),
% 232.00/231.96 inference(rename_variables,[],[782])).
% 232.00/231.96 cnf(1877,plain,
% 232.00/231.96 (P1(f2(x18771,f2(f2(x18772,x18773),f2(f1(x18771),x18773))))),
% 232.00/231.96 inference(rename_variables,[],[782])).
% 232.00/231.96 cnf(1880,plain,
% 232.00/231.96 (P1(f2(x18801,f2(f2(x18802,x18803),f2(f1(x18801),x18803))))),
% 232.00/231.96 inference(rename_variables,[],[782])).
% 232.00/231.96 cnf(1886,plain,
% 232.00/231.96 (P1(f2(f2(f2(f1(f2(x18861,x18861)),x18862),x18863),f2(f2(x18864,x18862),x18863)))),
% 232.00/231.96 inference(rename_variables,[],[1093])).
% 232.00/231.96 cnf(1889,plain,
% 232.00/231.96 (P1(f2(f2(f2(f1(x18891),x18892),x18893),f2(f2(f1(f1(f2(x18891,x18893))),f1(f2(x18891,x18893))),x18894)))),
% 232.00/231.96 inference(rename_variables,[],[907])).
% 232.00/231.96 cnf(1892,plain,
% 232.00/231.96 (P1(f2(f2(f2(f1(x18921),x18922),x18923),f2(f2(f1(f1(f2(x18921,x18923))),f1(f2(x18921,x18923))),x18924)))),
% 232.00/231.96 inference(rename_variables,[],[907])).
% 232.00/231.96 cnf(1898,plain,
% 232.00/231.96 (P1(f2(x18981,f2(f2(x18982,x18983),f2(f1(x18981),x18983))))),
% 232.00/231.96 inference(rename_variables,[],[782])).
% 232.00/231.96 cnf(1904,plain,
% 232.00/231.96 (P1(f2(x19041,f2(f1(f2(f1(f2(x19042,x19042)),x19043)),x19044)))),
% 232.00/231.96 inference(rename_variables,[],[1097])).
% 232.00/231.96 cnf(1909,plain,
% 232.00/231.96 (P1(f2(f2(f1(f1(f2(x19091,x19091))),f1(f2(x19091,x19091))),x19092))),
% 232.00/231.96 inference(rename_variables,[],[600])).
% 232.00/231.96 cnf(1912,plain,
% 232.00/231.96 (P1(f2(f2(f1(f1(f2(x19121,x19121))),f1(f2(x19121,x19121))),x19122))),
% 232.00/231.96 inference(rename_variables,[],[600])).
% 232.00/231.96 cnf(1918,plain,
% 232.00/231.96 (P1(f2(f2(f2(f1(x19181),x19182),x19183),f2(f2(f1(f1(f2(x19181,x19183))),f1(f2(x19181,x19183))),x19184)))),
% 232.00/231.96 inference(rename_variables,[],[907])).
% 232.00/231.96 cnf(1921,plain,
% 232.00/231.96 (P1(f2(x19211,f2(f1(f2(f1(x19211),x19212)),x19213)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(1924,plain,
% 232.00/231.96 (P1(f2(x19241,f2(f1(f2(f1(x19241),x19242)),x19243)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(1927,plain,
% 232.00/231.96 (P1(f2(x19271,f2(f1(f2(f1(x19271),x19272)),x19273)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(1933,plain,
% 232.00/231.96 (P1(f2(f2(f2(f1(x19331),x19332),x19333),f2(f2(f1(f1(f2(x19331,x19333))),f1(f2(x19331,x19333))),x19334)))),
% 232.00/231.96 inference(rename_variables,[],[907])).
% 232.00/231.96 cnf(1936,plain,
% 232.00/231.96 (P1(f2(f2(f2(x19361,f2(f1(f2(x19362,x19362)),x19363)),x19364),f2(x19365,x19364)))),
% 232.00/231.96 inference(rename_variables,[],[1414])).
% 232.00/231.96 cnf(1939,plain,
% 232.00/231.96 (P1(f2(f2(f1(f1(f2(x19391,x19391))),f1(f2(x19391,x19391))),x19392))),
% 232.00/231.96 inference(rename_variables,[],[600])).
% 232.00/231.96 cnf(1942,plain,
% 232.00/231.96 (P1(f2(x19421,f2(f1(f2(f2(f2(f1(x19422),x19423),x19424),f2(x19422,x19424))),x19425)))),
% 232.00/231.96 inference(rename_variables,[],[238])).
% 232.00/231.96 cnf(1945,plain,
% 232.00/231.96 (P1(f2(x19451,f2(f1(f2(f2(f2(f1(x19452),x19453),x19454),f2(x19452,x19454))),x19455)))),
% 232.00/231.96 inference(rename_variables,[],[238])).
% 232.00/231.96 cnf(1948,plain,
% 232.00/231.96 (P1(f2(x19481,f2(f1(f2(f2(f2(f1(x19482),x19483),x19484),f2(x19482,x19484))),x19485)))),
% 232.00/231.96 inference(rename_variables,[],[238])).
% 232.00/231.96 cnf(1951,plain,
% 232.00/231.96 (P1(f2(x19511,f2(f1(f2(f2(f2(f1(x19512),x19513),x19514),f2(x19512,x19514))),x19515)))),
% 232.00/231.96 inference(rename_variables,[],[238])).
% 232.00/231.96 cnf(1954,plain,
% 232.00/231.96 (P1(f2(x19541,f2(f1(f2(f1(x19541),x19542)),x19543)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(1957,plain,
% 232.00/231.96 (P1(f2(x19571,f2(f1(f2(f1(x19571),x19572)),x19573)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(1960,plain,
% 232.00/231.96 (P1(f2(x19601,f2(f1(f2(f1(x19601),x19602)),x19603)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(1963,plain,
% 232.00/231.96 (P1(f2(x19631,f2(f1(f2(f1(x19631),x19632)),x19633)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(1966,plain,
% 232.00/231.96 (P1(f2(x19661,f2(f1(f2(f1(f2(x19662,x19662)),x19663)),x19664)))),
% 232.00/231.96 inference(rename_variables,[],[1097])).
% 232.00/231.96 cnf(1969,plain,
% 232.00/231.96 (P1(f2(x19691,f2(f1(f2(f1(x19691),x19692)),x19693)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(1972,plain,
% 232.00/231.96 (P1(f2(x19721,f2(f1(f2(f2(f2(f1(x19722),x19723),x19724),f2(x19722,x19724))),x19725)))),
% 232.00/231.96 inference(rename_variables,[],[238])).
% 232.00/231.96 cnf(1975,plain,
% 232.00/231.96 (P1(f2(x19751,f2(f1(f2(f1(x19751),x19752)),x19753)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(1978,plain,
% 232.00/231.96 (P1(f2(x19781,f2(f1(f2(f2(f2(f1(x19782),x19783),x19784),f2(x19782,x19784))),x19785)))),
% 232.00/231.96 inference(rename_variables,[],[238])).
% 232.00/231.96 cnf(1981,plain,
% 232.00/231.96 (P1(f2(x19811,f2(f1(f2(x19812,x19812)),x19813)))),
% 232.00/231.96 inference(rename_variables,[],[1087])).
% 232.00/231.96 cnf(1984,plain,
% 232.00/231.96 (P1(f2(x19841,f2(f1(f2(x19842,x19842)),x19843)))),
% 232.00/231.96 inference(rename_variables,[],[1087])).
% 232.00/231.96 cnf(1987,plain,
% 232.00/231.96 (P1(f2(x19871,f2(f1(f2(f2(f2(f1(x19872),x19873),x19874),f2(x19872,x19874))),x19875)))),
% 232.00/231.96 inference(rename_variables,[],[238])).
% 232.00/231.96 cnf(1990,plain,
% 232.00/231.96 (P1(f2(x19901,f2(f1(f2(f1(x19901),x19902)),x19903)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(1993,plain,
% 232.00/231.96 (P1(f2(x19931,f2(f1(f2(f2(f2(f1(x19932),x19933),x19934),f2(x19932,x19934))),x19935)))),
% 232.00/231.96 inference(rename_variables,[],[238])).
% 232.00/231.96 cnf(1996,plain,
% 232.00/231.96 (P1(f2(x19961,f2(f1(f2(f1(x19961),x19962)),x19963)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(1999,plain,
% 232.00/231.96 (P1(f2(x19991,f2(f1(f2(x19992,x19992)),x19993)))),
% 232.00/231.96 inference(rename_variables,[],[1087])).
% 232.00/231.96 cnf(2002,plain,
% 232.00/231.96 (P1(f2(x20021,f2(f1(f2(x20022,x20022)),x20023)))),
% 232.00/231.96 inference(rename_variables,[],[1087])).
% 232.00/231.96 cnf(2005,plain,
% 232.00/231.96 (P1(f2(x20051,f2(f1(f2(x20052,x20052)),x20053)))),
% 232.00/231.96 inference(rename_variables,[],[1087])).
% 232.00/231.96 cnf(2008,plain,
% 232.00/231.96 (P1(f2(f2(f1(f1(f2(x20081,x20081))),f1(f2(x20081,x20081))),x20082))),
% 232.00/231.96 inference(rename_variables,[],[600])).
% 232.00/231.96 cnf(2011,plain,
% 232.00/231.96 (P1(f2(f2(f1(f1(f2(x20111,x20111))),f1(f2(x20111,x20111))),x20112))),
% 232.00/231.96 inference(rename_variables,[],[600])).
% 232.00/231.96 cnf(2014,plain,
% 232.00/231.96 (P1(f2(f2(f2(x20141,f2(f1(f2(x20142,x20142)),x20143)),x20144),f2(x20145,x20144)))),
% 232.00/231.96 inference(rename_variables,[],[1414])).
% 232.00/231.96 cnf(2017,plain,
% 232.00/231.96 (P1(f2(f2(f1(f1(f2(x20171,x20171))),f1(f2(x20171,x20171))),x20172))),
% 232.00/231.96 inference(rename_variables,[],[600])).
% 232.00/231.96 cnf(2020,plain,
% 232.00/231.96 (P1(f2(x20201,f2(f1(f2(f2(f2(f1(x20202),x20203),x20204),f2(x20202,x20204))),x20205)))),
% 232.00/231.96 inference(rename_variables,[],[238])).
% 232.00/231.96 cnf(2023,plain,
% 232.00/231.96 (P1(f2(x20231,f2(f1(f2(f1(f2(x20232,x20232)),x20233)),x20234)))),
% 232.00/231.96 inference(rename_variables,[],[1097])).
% 232.00/231.96 cnf(2026,plain,
% 232.00/231.96 (P1(f2(f2(f1(f1(f2(x20261,x20261))),f1(f2(x20261,x20261))),x20262))),
% 232.00/231.96 inference(rename_variables,[],[600])).
% 232.00/231.96 cnf(2032,plain,
% 232.00/231.96 (P1(f2(f2(f2(x20321,f2(f1(f2(x20322,x20322)),x20323)),x20324),f2(x20325,x20324)))),
% 232.00/231.96 inference(rename_variables,[],[1414])).
% 232.00/231.96 cnf(2038,plain,
% 232.00/231.96 (P1(f2(x20381,f2(f1(f2(f1(x20381),x20382)),x20383)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(2041,plain,
% 232.00/231.96 (P1(f2(x20411,f2(f1(f2(f1(x20411),x20412)),x20413)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(2044,plain,
% 232.00/231.96 (P1(f2(x20441,f2(f1(f2(f1(x20441),x20442)),x20443)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(2049,plain,
% 232.00/231.96 (P1(f2(x20491,f2(f1(f2(f1(f2(x20492,x20492)),x20493)),x20494)))),
% 232.00/231.96 inference(rename_variables,[],[1097])).
% 232.00/231.96 cnf(2052,plain,
% 232.00/231.96 (P1(f2(x20521,f2(f1(f2(f1(x20521),x20522)),x20523)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(2055,plain,
% 232.00/231.96 (P1(f2(x20551,f2(f1(f2(f1(x20551),x20552)),x20553)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(2058,plain,
% 232.00/231.96 (P1(f2(x20581,f2(f1(f2(f1(x20581),x20582)),x20583)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(2063,plain,
% 232.00/231.96 (P1(f2(x20631,f2(f1(f2(x20632,x20632)),x20633)))),
% 232.00/231.96 inference(rename_variables,[],[1087])).
% 232.00/231.96 cnf(2066,plain,
% 232.00/231.96 (P1(f2(x20661,f2(f1(f2(f1(x20661),x20662)),x20663)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(2069,plain,
% 232.00/231.96 (P1(f2(x20691,f2(f1(f2(f1(x20691),x20692)),x20693)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(2072,plain,
% 232.00/231.96 (P1(f2(x20721,f2(f1(f2(f1(x20721),x20722)),x20723)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(2075,plain,
% 232.00/231.96 (P1(f2(x20751,f2(f1(f2(f1(x20751),x20752)),x20753)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(2078,plain,
% 232.00/231.96 (P1(f2(x20781,f2(f1(f2(f1(x20781),x20782)),x20783)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(2081,plain,
% 232.00/231.96 (P1(f2(x20811,f2(f1(f2(f1(x20811),x20812)),x20813)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(2084,plain,
% 232.00/231.96 (P1(f2(x20841,f2(f1(f2(f1(x20841),x20842)),x20843)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(2087,plain,
% 232.00/231.96 (P1(f2(x20871,f2(f1(f2(f1(x20871),x20872)),x20873)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(2090,plain,
% 232.00/231.96 (P1(f2(x20901,f2(f1(f2(f1(f2(x20902,x20902)),x20903)),x20904)))),
% 232.00/231.96 inference(rename_variables,[],[1097])).
% 232.00/231.96 cnf(2093,plain,
% 232.00/231.96 (P1(f2(x20931,f2(f1(f2(x20932,x20932)),x20933)))),
% 232.00/231.96 inference(rename_variables,[],[1087])).
% 232.00/231.96 cnf(2096,plain,
% 232.00/231.96 (~P1(f2(f2(f1(f2(x20961,x20961)),x20962),f2(f1(a3),a3)))),
% 232.00/231.96 inference(rename_variables,[],[1484])).
% 232.00/231.96 cnf(2099,plain,
% 232.00/231.96 (~P1(f2(f2(f1(f2(x20991,x20991)),x20992),f2(f1(a3),a3)))),
% 232.00/231.96 inference(rename_variables,[],[1484])).
% 232.00/231.96 cnf(2102,plain,
% 232.00/231.96 (P1(f2(x21021,f2(f1(f2(f1(x21021),x21022)),x21023)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(2105,plain,
% 232.00/231.96 (P1(f2(x21051,f2(f1(f2(f1(x21051),x21052)),x21053)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(2108,plain,
% 232.00/231.96 (P1(f2(x21081,f2(f1(f2(f1(x21081),x21082)),x21083)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(2111,plain,
% 232.00/231.96 (P1(f2(x21111,f2(f1(f2(f1(x21111),x21112)),x21113)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(2114,plain,
% 232.00/231.96 (P1(f2(x21141,f2(f1(f2(f1(x21141),x21142)),x21143)))),
% 232.00/231.96 inference(rename_variables,[],[730])).
% 232.00/231.96 cnf(2117,plain,
% 232.00/231.96 (P1(f2(x21171,f2(f1(f2(x21172,x21172)),x21173)))),
% 232.00/231.96 inference(rename_variables,[],[1087])).
% 232.00/231.96 cnf(2120,plain,
% 232.00/231.96 (P1(f2(x21201,f2(f1(f2(x21202,x21202)),x21203)))),
% 232.00/231.96 inference(rename_variables,[],[1087])).
% 232.00/231.96 cnf(2123,plain,
% 232.00/231.96 (P1(f2(x21231,f2(f1(f2(x21232,x21232)),x21233)))),
% 232.00/231.96 inference(rename_variables,[],[1087])).
% 232.00/231.96 cnf(2126,plain,
% 232.00/231.97 (P1(f2(x21261,f2(f1(f2(x21262,x21262)),x21263)))),
% 232.00/231.97 inference(rename_variables,[],[1087])).
% 232.00/231.97 cnf(2129,plain,
% 232.00/231.97 (P1(f2(x21291,f2(f1(f2(x21292,x21292)),x21293)))),
% 232.00/231.97 inference(rename_variables,[],[1087])).
% 232.00/231.97 cnf(2132,plain,
% 232.00/231.97 (P1(f2(x21321,f2(f1(f2(x21322,x21322)),x21323)))),
% 232.00/231.97 inference(rename_variables,[],[1087])).
% 232.00/231.97 cnf(2135,plain,
% 232.00/231.97 (P1(f2(x21351,f2(f1(f2(x21352,x21352)),x21353)))),
% 232.00/231.97 inference(rename_variables,[],[1087])).
% 232.00/231.97 cnf(2138,plain,
% 232.00/231.97 (P1(f2(x21381,f2(f1(f2(x21382,x21382)),x21383)))),
% 232.00/231.97 inference(rename_variables,[],[1087])).
% 232.00/231.97 cnf(2141,plain,
% 232.00/231.97 (P1(f2(x21411,f2(f1(f2(x21412,x21412)),x21413)))),
% 232.00/231.97 inference(rename_variables,[],[1087])).
% 232.00/231.97 cnf(2144,plain,
% 232.00/231.97 (P1(f2(x21441,f2(f1(f2(x21442,x21442)),x21443)))),
% 232.00/231.97 inference(rename_variables,[],[1087])).
% 232.00/231.97 cnf(2147,plain,
% 232.00/231.97 (P1(f2(x21471,f2(f1(f2(x21472,x21472)),x21473)))),
% 232.00/231.97 inference(rename_variables,[],[1087])).
% 232.00/231.97 cnf(2150,plain,
% 232.00/231.97 (P1(f2(x21501,f2(f1(f2(f2(f2(f1(x21502),x21503),x21504),f2(x21502,x21504))),x21505)))),
% 232.00/231.97 inference(rename_variables,[],[238])).
% 232.00/231.97 cnf(2153,plain,
% 232.00/231.97 (P1(f2(x21531,f2(f1(f2(f2(f2(f1(x21532),x21533),x21534),f2(x21532,x21534))),x21535)))),
% 232.00/231.97 inference(rename_variables,[],[238])).
% 232.00/231.97 cnf(2156,plain,
% 232.00/231.97 (P1(f2(x21561,f2(f1(f2(f2(f2(f1(x21562),x21563),x21564),f2(x21562,x21564))),x21565)))),
% 232.00/231.97 inference(rename_variables,[],[238])).
% 232.00/231.97 cnf(2159,plain,
% 232.00/231.97 (P1(f2(x21591,f2(f1(f2(f2(f2(f1(x21592),x21593),x21594),f2(x21592,x21594))),x21595)))),
% 232.00/231.97 inference(rename_variables,[],[238])).
% 232.00/231.97 cnf(2162,plain,
% 232.00/231.97 (P1(f2(x21621,f2(f1(f2(f2(f2(f1(x21622),x21623),x21624),f2(x21622,x21624))),x21625)))),
% 232.00/231.97 inference(rename_variables,[],[238])).
% 232.00/231.97 cnf(2180,plain,
% 232.00/231.97 (P1(f2(f2(f2(x21801,f2(f1(f2(x21802,x21802)),x21803)),x21804),f2(x21805,x21804)))),
% 232.00/231.97 inference(rename_variables,[],[1414])).
% 232.00/231.97 cnf(2182,plain,
% 232.00/231.97 (P1(f2(f1(f2(f1(f2(x21821,f2(f1(f2(x21822,x21822)),x21823))),x21824)),x21825))),
% 232.00/231.97 inference(scs_inference,[],[730,1921,1924,1927,1954,1957,1960,1963,1969,1975,1990,1996,2038,2041,2044,2052,2055,2058,2066,2069,2072,2075,2078,2081,2084,2087,2102,2105,2108,2111,506,238,1942,1945,1948,1951,1972,1978,1987,1993,2020,2150,2153,2156,2159,1093,1886,600,1909,1912,1939,2008,2011,2017,2026,782,1827,1830,1833,1836,1839,1871,1874,1877,1880,1898,682,1491,1484,2096,2099,1414,1842,1936,2014,2032,2180,1101,1087,1848,1862,1981,1984,1999,2002,2005,2063,2093,2117,2120,2123,2126,2129,2132,2135,2138,2141,2144,2147,907,1845,1865,1889,1892,1918,1933,1097,1904,1966,2023,2049,1694,1800,1803,1806,1809,1812,1815,1818,1821,1824,1692,1570,1473,535,534,533,532,530,528,518,515,509,478,474,449,448,447,441,440,435,434,432,431,430,429,426,424,420,419,418,416,414,391,383,382,381,379,373,356,332,316,536,538,539,545,293,290,288,524,526,527,514,512,507,494,495,268,264,260,259,256,452,453,454,455,457,459,461,462,463,464,468,436,427,397,405,406,407,392,228,371,344,345,334,196,193,203,190,189,186,178,170,165,271,232,218,219,224,225,226,125,124,163,161,100,99,132,133,135,92,91,101,102,104,106,108,110,111,114,116,117,120,89,87,81,77,79,65,503,511,487,360,443,380])).
% 232.00/231.97 cnf(2183,plain,
% 232.00/231.97 (P1(f2(f2(f2(x21831,f2(f1(f2(x21832,x21832)),x21833)),x21834),f2(x21835,x21834)))),
% 232.00/231.97 inference(rename_variables,[],[1414])).
% 232.00/231.97 cnf(2186,plain,
% 232.00/231.97 (P1(f2(f2(f2(f1(x21861),x21862),x21863),f2(f2(x21864,x21865),f2(f1(f2(x21861,x21863)),x21865))))),
% 232.00/231.97 inference(rename_variables,[],[882])).
% 232.00/231.97 cnf(2192,plain,
% 232.00/231.97 (P1(f2(f2(x21921,x21922),f2(f1(f2(f2(f1(x21923),x21923),x21923)),x21922)))),
% 232.00/231.97 inference(rename_variables,[],[1073])).
% 232.00/231.97 cnf(2198,plain,
% 232.00/231.97 (P1(f2(x21981,f2(f1(f2(f1(x21981),x21982)),x21983)))),
% 232.00/231.97 inference(rename_variables,[],[730])).
% 232.00/231.97 cnf(2201,plain,
% 232.00/231.97 (P1(f2(x22011,f2(f1(f2(f1(x22011),x22012)),x22013)))),
% 232.00/231.97 inference(rename_variables,[],[730])).
% 232.00/231.97 cnf(2204,plain,
% 232.00/231.97 (P1(f2(f2(f2(x22041,f2(f1(f2(x22042,x22042)),x22043)),x22044),f2(x22045,x22044)))),
% 232.00/231.97 inference(rename_variables,[],[1414])).
% 232.00/231.97 cnf(2213,plain,
% 232.00/231.97 (P1(f2(x22131,f2(f2(x22132,x22133),f2(f1(f2(f1(x22131),x22134)),x22133))))),
% 232.00/231.97 inference(rename_variables,[],[878])).
% 232.00/231.97 cnf(2216,plain,
% 232.00/231.97 (P1(f2(x22161,f2(f1(f2(f1(f2(x22162,x22162)),x22163)),x22164)))),
% 232.00/231.97 inference(rename_variables,[],[1097])).
% 232.00/231.97 cnf(2224,plain,
% 232.00/231.97 (P1(f2(x22241,f2(f1(f2(f2(f2(f1(x22242),x22243),x22244),f2(x22242,x22244))),x22245)))),
% 232.00/231.97 inference(rename_variables,[],[238])).
% 232.00/231.97 cnf(2227,plain,
% 232.00/231.97 (P1(f2(x22271,f2(f1(f2(f2(f2(f1(x22272),x22273),x22274),f2(x22272,x22274))),x22275)))),
% 232.00/231.97 inference(rename_variables,[],[238])).
% 232.00/231.97 cnf(2230,plain,
% 232.00/231.97 (P1(f2(x22301,f2(f1(f2(f2(f2(f1(x22302),x22303),x22304),f2(x22302,x22304))),x22305)))),
% 232.00/231.97 inference(rename_variables,[],[238])).
% 232.00/231.97 cnf(2233,plain,
% 232.00/231.97 (P1(f2(x22331,f2(f1(f2(f2(f2(f1(x22332),x22333),x22334),f2(x22332,x22334))),x22335)))),
% 232.00/231.97 inference(rename_variables,[],[238])).
% 232.00/231.97 cnf(2241,plain,
% 232.00/231.97 (P1(f2(x22411,f2(f1(f2(f2(f2(f1(x22412),x22413),x22414),f2(x22412,x22414))),x22415)))),
% 232.00/231.97 inference(rename_variables,[],[238])).
% 232.00/231.97 cnf(2254,plain,
% 232.00/231.97 (P1(f2(x22541,f2(f1(f2(f2(f2(f1(x22542),x22543),x22544),f2(x22542,x22544))),x22545)))),
% 232.00/231.97 inference(rename_variables,[],[238])).
% 232.00/231.97 cnf(2261,plain,
% 232.00/231.97 (P1(f2(f2(x22611,x22612),f2(f2(f1(f1(f2(x22613,x22613))),f1(f2(x22613,x22613))),x22612)))),
% 232.00/231.97 inference(rename_variables,[],[1099])).
% 232.00/231.97 cnf(2268,plain,
% 232.00/231.97 (P1(f2(x22681,f2(f1(f2(f1(x22681),x22682)),x22683)))),
% 232.00/231.97 inference(rename_variables,[],[730])).
% 232.00/231.97 cnf(2281,plain,
% 232.00/231.97 (~P1(f2(f2(f2(f1(x22811),x22811),x22811),f2(f1(f2(f1(a3),a3)),f2(f1(a3),a3))))),
% 232.00/231.97 inference(rename_variables,[],[1473])).
% 232.00/231.97 cnf(2286,plain,
% 232.00/231.97 (P1(f2(x22861,f2(f1(f2(f2(f2(f1(x22862),x22863),x22864),f2(x22862,x22864))),x22865)))),
% 232.00/231.97 inference(rename_variables,[],[238])).
% 232.00/231.97 cnf(2297,plain,
% 232.00/231.97 (P1(f2(x22971,f2(f1(f2(f2(f2(f1(x22972),x22973),x22974),f2(x22972,x22974))),x22975)))),
% 232.00/231.97 inference(rename_variables,[],[238])).
% 232.00/231.97 cnf(2302,plain,
% 232.00/231.97 (P1(f2(f2(f1(f1(f2(x23021,f2(f2(x23022,x23023),f2(f1(x23021),x23023))))),f1(f2(x23021,f2(f2(x23022,x23023),f2(f1(x23021),x23023))))),x23024))),
% 232.00/231.97 inference(scs_inference,[],[730,1921,1924,1927,1954,1957,1960,1963,1969,1975,1990,1996,2038,2041,2044,2052,2055,2058,2066,2069,2072,2075,2078,2081,2084,2087,2102,2105,2108,2111,2114,2198,2201,2268,506,238,1942,1945,1948,1951,1972,1978,1987,1993,2020,2150,2153,2156,2159,2162,2224,2227,2230,2233,2241,2254,2286,2297,1093,1886,600,1909,1912,1939,2008,2011,2017,2026,782,1827,1830,1833,1836,1839,1871,1874,1877,1880,1898,682,1491,1484,2096,2099,1414,1842,1936,2014,2032,2180,2183,2204,1101,1868,644,1087,1848,1862,1981,1984,1999,2002,2005,2063,2093,2117,2120,2123,2126,2129,2132,2135,2138,2141,2144,2147,948,1099,2261,907,1845,1865,1889,1892,1918,1933,882,2186,1073,2192,878,2213,1097,1904,1966,2023,2049,2090,2216,1694,1800,1803,1806,1809,1812,1815,1818,1821,1824,1692,1570,1473,1851,2281,535,534,533,532,530,528,518,515,509,478,474,449,448,447,441,440,435,434,432,431,430,429,426,424,420,419,418,416,414,391,383,382,381,379,373,356,332,316,536,538,539,545,293,290,288,524,526,527,514,512,507,494,495,268,264,260,259,256,452,453,454,455,457,459,461,462,463,464,468,436,427,397,405,406,407,392,228,371,344,345,334,196,193,203,190,189,186,178,170,165,271,232,218,219,224,225,226,125,124,163,161,100,99,132,133,135,92,91,101,102,104,106,108,110,111,114,116,117,120,89,87,81,77,79,65,503,511,487,360,443,380,359,342,377,55,240,90,470,446,444,445,491,369,173,241,181,179,74,365,368,171,66,504,257,168,166,164,71,49,519,469,53,200,201,358,194,12,387,185,78,523,376,389,488,510,51])).
% 232.00/231.97 cnf(2394,plain,
% 232.00/231.97 ($false),
% 232.00/231.97 inference(scs_inference,[],[653,1694,96,2302,2182,480,479,357,282]),
% 232.00/231.97 ['proof']).
% 232.00/231.97 % SZS output end Proof
% 232.00/231.97 % Total time :231.408547s
%------------------------------------------------------------------------------