%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO030-2 : TPTP v8.2.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n025.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 06:03:23 EDT 2024
% Result : Unsatisfiable 60.79s 60.88s
% Output : CNFRefutation 60.90s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO030-2 : TPTP v8.2.0. Released v1.0.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n025.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jun 21 06:15:39 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.19/0.57 start to proof:theBenchmark
% 60.79/60.87 %-------------------------------------------
% 60.79/60.87 % File :CSE---1.7
% 60.79/60.87 % Problem :theBenchmark
% 60.79/60.87 % Transform :cnf
% 60.79/60.87 % Format :tptp:raw
% 60.79/60.87 % Command :java -jar mcs_scs.jar %d %s
% 60.79/60.87
% 60.79/60.87 % Result :Theorem 60.260000s
% 60.79/60.87 % Output :CNFRefutation 60.260000s
% 60.79/60.87 %-------------------------------------------
% 60.79/60.88 %--------------------------------------------------------------------------
% 60.79/60.88 % File : GEO030-2 : TPTP v8.2.0. Released v1.0.0.
% 60.79/60.88 % Domain : Geometry
% 60.79/60.88 % Problem : Corollary to the outer five-segment axiom
% 60.79/60.88 % Version : [Qua89] axioms.
% 60.79/60.88 % English :
% 60.79/60.88
% 60.79/60.88 % Refs : [SST83] Schwabbauser et al. (1983), Metamathematische Methoden
% 60.79/60.88 % : [Qua89] Quaife (1989), Automated Development of Tarski's Geome
% 60.79/60.88 % Source : [TPTP]
% 60.79/60.88 % Names :
% 60.79/60.88
% 60.79/60.88 % Status : Unsatisfiable
% 60.79/60.88 % Rating : 0.15 v8.2.0, 0.19 v8.1.0, 0.11 v7.5.0, 0.21 v7.4.0, 0.18 v7.3.0, 0.25 v7.1.0, 0.17 v7.0.0, 0.13 v6.4.0, 0.20 v6.3.0, 0.09 v6.2.0, 0.20 v6.1.0, 0.21 v6.0.0, 0.20 v5.5.0, 0.35 v5.3.0, 0.39 v5.2.0, 0.31 v5.1.0, 0.29 v4.1.0, 0.31 v4.0.1, 0.45 v4.0.0, 0.36 v3.7.0, 0.30 v3.5.0, 0.27 v3.4.0, 0.17 v3.3.0, 0.29 v3.2.0, 0.00 v3.1.0, 0.27 v2.7.0, 0.25 v2.6.0, 0.40 v2.5.0, 0.17 v2.4.0, 0.22 v2.2.1, 0.44 v2.2.0, 0.33 v2.1.0, 0.56 v2.0.0
% 60.79/60.88 % Syntax : Number of clauses : 23 ( 11 unt; 5 nHn; 20 RR)
% 60.79/60.88 % Number of literals : 61 ( 9 equ; 36 neg)
% 60.79/60.88 % Maximal clause size : 8 ( 2 avg)
% 60.79/60.88 % Maximal term depth : 2 ( 1 avg)
% 60.79/60.88 % Number of predicates : 3 ( 2 usr; 0 prp; 2-4 aty)
% 60.79/60.88 % Number of functors : 12 ( 12 usr; 7 con; 0-6 aty)
% 60.79/60.88 % Number of variables : 71 ( 3 sgn)
% 60.79/60.88 % SPC : CNF_UNS_RFO_SEQ_NHN
% 60.79/60.88
% 60.79/60.88 % Comments : Proving corollaries from axioms is not usual.
% 60.79/60.88 %--------------------------------------------------------------------------
% 60.79/60.88 %----Include Tarski geometry axioms
% 60.79/60.88 include('Axioms/GEO002-0.ax').
% 60.79/60.88 %--------------------------------------------------------------------------
% 60.79/60.88 cnf(v_between_u_and_w,hypothesis,
% 60.79/60.88 between(u,v,w) ).
% 60.79/60.88
% 60.79/60.88 cnf(u_to_w_equals_u_to_w1,hypothesis,
% 60.79/60.88 equidistant(u,w,u,w1) ).
% 60.79/60.88
% 60.79/60.88 cnf(v_to_w_equals_v_to_w1,hypothesis,
% 60.79/60.88 equidistant(v,w,v,w1) ).
% 60.79/60.88
% 60.79/60.88 cnf(u_not_v,hypothesis,
% 60.79/60.88 u != v ).
% 60.79/60.88
% 60.79/60.88 cnf(prove_w_is_w1,negated_conjecture,
% 60.79/60.88 w != w1 ).
% 60.79/60.88
% 60.79/60.88 %--------------------------------------------------------------------------
% 60.79/60.88 %-------------------------------------------
% 60.79/60.88 % Proof found
% 60.79/60.88 % SZS status Theorem for theBenchmark
% 60.79/60.88 % SZS output start Proof
% 60.79/60.89 %ClaNum:58(EqnAxiom:35)
% 60.79/60.89 %VarNum:211(SingletonVarNum:71)
% 60.79/60.89 %MaxLitNum:8
% 60.79/60.89 %MaxfuncDepth:1
% 60.79/60.89 %SharedTerms:15
% 60.79/60.89 %goalClause: 43
% 60.79/60.89 %singleGoalClaCount:1
% 60.79/60.89 [36]P1(a1,a10,a11)
% 60.79/60.89 [37]P2(a1,a11,a1,a12)
% 60.79/60.89 [38]P2(a10,a11,a10,a12)
% 60.79/60.89 [42]~E(a10,a1)
% 60.79/60.89 [43]~E(a12,a11)
% 60.79/60.89 [44]~P1(a6,a8,a9)
% 60.79/60.89 [45]~P1(a8,a9,a6)
% 60.79/60.89 [46]~P1(a9,a6,a8)
% 60.79/60.89 [39]P2(x391,x392,x392,x391)
% 60.79/60.89 [40]P1(x401,x402,f2(x401,x402,x403,x404))
% 60.79/60.89 [41]P2(x411,f2(x412,x411,x413,x414),x413,x414)
% 60.79/60.89 [47]~P1(x471,x472,x471)+E(x471,x472)
% 60.79/60.89 [48]~P2(x481,x482,x483,x483)+E(x481,x482)
% 60.79/60.89 [52]~P1(x525,x521,x524)+~P1(x522,x523,x524)+P1(x521,f7(x522,x523,x524,x521,x525),x522)
% 60.79/60.89 [53]~P1(x535,x534,x533)+~P1(x532,x531,x533)+P1(x531,f7(x532,x531,x533,x534,x535),x535)
% 60.79/60.89 [49]~P2(x495,x496,x491,x492)+P2(x491,x492,x493,x494)+~P2(x495,x496,x493,x494)
% 60.79/60.89 [54]~P1(x544,x542,x543)+~P1(x541,x542,x545)+E(x541,x542)+P1(x541,x543,f3(x541,x544,x542,x543,x545))
% 60.79/60.89 [55]~P1(x553,x552,x554)+~P1(x551,x552,x555)+E(x551,x552)+P1(x551,x553,f4(x551,x553,x552,x554,x555))
% 60.79/60.89 [56]~P1(x563,x562,x564)+~P1(x561,x562,x565)+E(x561,x562)+P1(f4(x561,x563,x562,x564,x565),x565,f3(x561,x563,x562,x564,x565))
% 60.79/60.89 [57]~P1(x573,x574,x575)+~P1(x572,x573,x575)+~P2(x572,x575,x572,x576)+~P2(x572,x573,x572,x571)+P1(x571,f5(x572,x573,x571,x574,x575,x576),x576)
% 60.79/60.89 [58]~P1(x583,x582,x585)+~P1(x581,x583,x585)+~P2(x581,x585,x581,x586)+~P2(x581,x583,x581,x584)+P2(x581,x582,x581,f5(x581,x583,x584,x582,x585,x586))
% 60.79/60.89 [50]P1(x505,x503,x504)+P1(x504,x505,x503)+~P2(x503,x501,x503,x502)+~P2(x505,x501,x505,x502)+~P2(x504,x501,x504,x502)+E(x501,x502)+P1(x503,x504,x505)
% 60.79/60.89 [51]~P1(x511,x512,x513)+~P2(x512,x514,x518,x516)+~P2(x512,x513,x518,x515)+~P2(x511,x514,x517,x516)+~P2(x511,x512,x517,x518)+E(x511,x512)+P2(x513,x514,x515,x516)+~P1(x517,x518,x515)
% 60.79/60.89 %EqnAxiom
% 60.79/60.89 [1]E(x11,x11)
% 60.79/60.89 [2]E(x22,x21)+~E(x21,x22)
% 60.79/60.89 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 60.79/60.89 [4]~E(x41,x42)+E(f2(x41,x43,x44,x45),f2(x42,x43,x44,x45))
% 60.79/60.89 [5]~E(x51,x52)+E(f2(x53,x51,x54,x55),f2(x53,x52,x54,x55))
% 60.79/60.89 [6]~E(x61,x62)+E(f2(x63,x64,x61,x65),f2(x63,x64,x62,x65))
% 60.79/60.89 [7]~E(x71,x72)+E(f2(x73,x74,x75,x71),f2(x73,x74,x75,x72))
% 60.79/60.89 [8]~E(x81,x82)+E(f5(x81,x83,x84,x85,x86,x87),f5(x82,x83,x84,x85,x86,x87))
% 60.79/60.89 [9]~E(x91,x92)+E(f5(x93,x91,x94,x95,x96,x97),f5(x93,x92,x94,x95,x96,x97))
% 60.79/60.89 [10]~E(x101,x102)+E(f5(x103,x104,x101,x105,x106,x107),f5(x103,x104,x102,x105,x106,x107))
% 60.79/60.89 [11]~E(x111,x112)+E(f5(x113,x114,x115,x111,x116,x117),f5(x113,x114,x115,x112,x116,x117))
% 60.79/60.89 [12]~E(x121,x122)+E(f5(x123,x124,x125,x126,x121,x127),f5(x123,x124,x125,x126,x122,x127))
% 60.79/60.89 [13]~E(x131,x132)+E(f5(x133,x134,x135,x136,x137,x131),f5(x133,x134,x135,x136,x137,x132))
% 60.79/60.89 [14]~E(x141,x142)+E(f7(x141,x143,x144,x145,x146),f7(x142,x143,x144,x145,x146))
% 60.79/60.89 [15]~E(x151,x152)+E(f7(x153,x151,x154,x155,x156),f7(x153,x152,x154,x155,x156))
% 60.79/60.89 [16]~E(x161,x162)+E(f7(x163,x164,x161,x165,x166),f7(x163,x164,x162,x165,x166))
% 60.79/60.89 [17]~E(x171,x172)+E(f7(x173,x174,x175,x171,x176),f7(x173,x174,x175,x172,x176))
% 60.79/60.89 [18]~E(x181,x182)+E(f7(x183,x184,x185,x186,x181),f7(x183,x184,x185,x186,x182))
% 60.79/60.89 [19]~E(x191,x192)+E(f3(x191,x193,x194,x195,x196),f3(x192,x193,x194,x195,x196))
% 60.79/60.89 [20]~E(x201,x202)+E(f3(x203,x201,x204,x205,x206),f3(x203,x202,x204,x205,x206))
% 60.79/60.89 [21]~E(x211,x212)+E(f3(x213,x214,x211,x215,x216),f3(x213,x214,x212,x215,x216))
% 60.79/60.89 [22]~E(x221,x222)+E(f3(x223,x224,x225,x221,x226),f3(x223,x224,x225,x222,x226))
% 60.79/60.89 [23]~E(x231,x232)+E(f3(x233,x234,x235,x236,x231),f3(x233,x234,x235,x236,x232))
% 60.79/60.89 [24]~E(x241,x242)+E(f4(x241,x243,x244,x245,x246),f4(x242,x243,x244,x245,x246))
% 60.79/60.89 [25]~E(x251,x252)+E(f4(x253,x251,x254,x255,x256),f4(x253,x252,x254,x255,x256))
% 60.79/60.89 [26]~E(x261,x262)+E(f4(x263,x264,x261,x265,x266),f4(x263,x264,x262,x265,x266))
% 60.79/60.89 [27]~E(x271,x272)+E(f4(x273,x274,x275,x271,x276),f4(x273,x274,x275,x272,x276))
% 60.79/60.89 [28]~E(x281,x282)+E(f4(x283,x284,x285,x286,x281),f4(x283,x284,x285,x286,x282))
% 60.79/60.89 [29]P1(x292,x293,x294)+~E(x291,x292)+~P1(x291,x293,x294)
% 60.79/60.89 [30]P1(x303,x302,x304)+~E(x301,x302)+~P1(x303,x301,x304)
% 60.79/60.89 [31]P1(x313,x314,x312)+~E(x311,x312)+~P1(x313,x314,x311)
% 60.79/60.89 [32]P2(x322,x323,x324,x325)+~E(x321,x322)+~P2(x321,x323,x324,x325)
% 60.79/60.89 [33]P2(x333,x332,x334,x335)+~E(x331,x332)+~P2(x333,x331,x334,x335)
% 60.79/60.89 [34]P2(x343,x344,x342,x345)+~E(x341,x342)+~P2(x343,x344,x341,x345)
% 60.79/60.89 [35]P2(x353,x354,x355,x352)+~E(x351,x352)+~P2(x353,x354,x355,x351)
% 60.79/60.89
% 60.79/60.89 %-------------------------------------------
% 60.90/60.90 cnf(59,plain,
% 60.90/60.90 (~P1(a12,a11,a12)),
% 60.90/60.90 inference(scs_inference,[],[43,47])).
% 60.90/60.90 cnf(61,plain,
% 60.90/60.90 (~P2(a12,a11,x611,x611)),
% 60.90/60.90 inference(scs_inference,[],[43,47,48])).
% 60.90/60.90 cnf(63,plain,
% 60.90/60.90 (P2(x631,x632,x631,x632)),
% 60.90/60.90 inference(scs_inference,[],[43,39,47,48,49])).
% 60.90/60.90 cnf(65,plain,
% 60.90/60.90 (~E(f2(a6,a8,x651,x652),a9)),
% 60.90/60.90 inference(scs_inference,[],[43,39,40,44,47,48,49,31])).
% 60.90/60.90 cnf(66,plain,
% 60.90/60.90 (P1(x661,x662,f2(x661,x662,x663,x664))),
% 60.90/60.90 inference(rename_variables,[],[40])).
% 60.90/60.90 cnf(67,plain,
% 60.90/60.90 (~E(a11,a12)),
% 60.90/60.90 inference(scs_inference,[],[43,39,40,44,47,48,49,31,32])).
% 60.90/60.90 cnf(68,plain,
% 60.90/60.90 (P2(x681,x682,x682,x681)),
% 60.90/60.90 inference(rename_variables,[],[39])).
% 60.90/60.90 cnf(70,plain,
% 60.90/60.90 (P2(x701,f2(x702,x701,x703,x704),x703,x704)),
% 60.90/60.90 inference(rename_variables,[],[41])).
% 60.90/60.90 cnf(71,plain,
% 60.90/60.90 (P1(x711,x712,f2(x713,x712,x714,x715))+~E(x713,x711)),
% 60.90/60.90 inference(scs_inference,[],[43,39,41,40,66,44,47,48,49,31,32,33,29])).
% 60.90/60.90 cnf(72,plain,
% 60.90/60.90 (P1(x721,x722,f2(x721,x723,x724,x725))+~E(x723,x722)),
% 60.90/60.90 inference(scs_inference,[],[43,39,41,40,66,44,47,48,49,31,32,33,29,30])).
% 60.90/60.90 cnf(73,plain,
% 60.90/60.90 (P2(x731,x732,x733,x731)+~E(x732,x733)),
% 60.90/60.90 inference(scs_inference,[],[43,39,68,41,40,66,44,47,48,49,31,32,33,29,30,34])).
% 60.90/60.90 cnf(74,plain,
% 60.90/60.90 (P2(x741,f2(x742,x741,x743,x744),x743,x745)+~E(x744,x745)),
% 60.90/60.90 inference(scs_inference,[],[43,39,68,41,70,40,66,44,47,48,49,31,32,33,29,30,34,35])).
% 60.90/60.90 cnf(79,plain,
% 60.90/60.90 (~P1(f2(a6,a8,x791,x792),a9,f2(a6,a8,x791,x792))),
% 60.90/60.90 inference(scs_inference,[],[65,47])).
% 60.90/60.90 cnf(81,plain,
% 60.90/60.90 (~P2(f2(a6,a8,x811,x812),a9,x813,x813)),
% 60.90/60.90 inference(scs_inference,[],[65,47,48])).
% 60.90/60.90 cnf(83,plain,
% 60.90/60.90 (~E(f2(a12,a11,x831,x832),a12)),
% 60.90/60.90 inference(scs_inference,[],[59,65,40,47,48,31])).
% 60.90/60.90 cnf(85,plain,
% 60.90/60.90 (~E(f2(x851,a12,x852,x852),a11)),
% 60.90/60.90 inference(scs_inference,[],[59,61,65,41,40,47,48,31,33])).
% 60.90/60.90 cnf(87,plain,
% 60.90/60.90 (P1(a1,x871,a11)+~E(a10,x871)),
% 60.90/60.90 inference(scs_inference,[],[59,61,65,36,41,40,47,48,31,33,30])).
% 60.90/60.90 cnf(88,plain,
% 60.90/60.90 (P2(a1,a11,x881,a12)+~E(a1,x881)),
% 60.90/60.90 inference(scs_inference,[],[59,61,65,36,37,41,40,47,48,31,33,30,34])).
% 60.90/60.90 cnf(89,plain,
% 60.90/60.90 (P2(a1,a11,a1,x891)+~E(a12,x891)),
% 60.90/60.90 inference(scs_inference,[],[59,61,65,36,37,41,40,47,48,31,33,30,34,35])).
% 60.90/60.90 cnf(90,plain,
% 60.90/60.90 (P2(x901,a11,a1,a12)+~E(a1,x901)),
% 60.90/60.90 inference(scs_inference,[],[59,61,65,36,37,41,40,47,48,31,33,30,34,35,32])).
% 60.90/60.90 cnf(91,plain,
% 60.90/60.90 (P1(x911,a10,a11)+~E(a1,x911)),
% 60.90/60.90 inference(scs_inference,[],[59,61,65,36,37,41,40,47,48,31,33,30,34,35,32,29])).
% 60.90/60.90 cnf(97,plain,
% 60.90/60.90 (~P1(a11,a12,a11)),
% 60.90/60.90 inference(scs_inference,[],[67,47])).
% 60.90/60.90 cnf(99,plain,
% 60.90/60.90 (~P2(a11,a12,x991,x991)),
% 60.90/60.90 inference(scs_inference,[],[67,47,48])).
% 60.90/60.90 cnf(103,plain,
% 60.90/60.90 (~P2(f2(a6,a8,x1031,x1032),a9,x1033,x1033)),
% 60.90/60.90 inference(rename_variables,[],[81])).
% 60.90/60.90 cnf(104,plain,
% 60.90/60.90 (~E(f2(f2(a6,a8,x1041,x1042),a9,x1043,x1044),f2(a6,a8,x1041,x1042))),
% 60.90/60.90 inference(scs_inference,[],[79,81,63,67,40,47,48,32,31])).
% 60.90/60.90 cnf(106,plain,
% 60.90/60.90 (~E(f2(x1061,f2(a6,a8,x1062,x1063),x1064,x1064),a9)),
% 60.90/60.90 inference(scs_inference,[],[79,81,103,63,67,41,40,47,48,32,31,33])).
% 60.90/60.90 cnf(108,plain,
% 60.90/60.90 (P2(a10,a11,a10,x1081)+~E(a12,x1081)),
% 60.90/60.90 inference(scs_inference,[],[79,81,103,63,67,38,41,40,47,48,32,31,33,35])).
% 60.90/60.90 cnf(109,plain,
% 60.90/60.90 (P2(a10,a11,x1091,a12)+~E(a10,x1091)),
% 60.90/60.90 inference(scs_inference,[],[79,81,103,63,67,38,41,40,47,48,32,31,33,35,34])).
% 60.90/60.90 cnf(117,plain,
% 60.90/60.90 (~P1(f2(x1171,a12,x1172,x1172),a11,f2(x1171,a12,x1172,x1172))),
% 60.90/60.90 inference(scs_inference,[],[85,47])).
% 60.90/60.90 cnf(119,plain,
% 60.90/60.90 (~P2(f2(f2(a6,a8,x1191,x1192),a9,x1193,x1194),f2(a6,a8,x1191,x1192),x1195,x1195)),
% 60.90/60.90 inference(scs_inference,[],[104,85,47,48])).
% 60.90/60.90 cnf(122,plain,
% 60.90/60.90 (P2(x1221,f2(x1222,x1221,x1223,x1224),x1223,x1224)),
% 60.90/60.90 inference(rename_variables,[],[41])).
% 60.90/60.90 cnf(123,plain,
% 60.90/60.90 (~E(f2(a11,a12,x1231,x1232),a11)),
% 60.90/60.90 inference(scs_inference,[],[97,104,85,41,40,47,48,32,31])).
% 60.90/60.90 cnf(125,plain,
% 60.90/60.90 (~E(f2(x1251,a11,x1252,x1252),a12)),
% 60.90/60.90 inference(scs_inference,[],[97,99,104,85,41,122,40,47,48,32,31,33])).
% 60.90/60.90 cnf(126,plain,
% 60.90/60.90 (P2(x1261,f2(x1262,x1261,x1263,x1264),x1263,x1264)),
% 60.90/60.90 inference(rename_variables,[],[41])).
% 60.90/60.90 cnf(127,plain,
% 60.90/60.90 (P2(x1271,f2(x1272,x1271,x1273,x1274),x1275,x1274)+~E(x1273,x1275)),
% 60.90/60.90 inference(scs_inference,[],[97,99,104,85,41,122,126,40,47,48,32,31,33,34])).
% 60.90/60.90 cnf(135,plain,
% 60.90/60.90 (~P1(f2(x1351,a11,x1352,x1352),a12,f2(x1351,a11,x1352,x1352))),
% 60.90/60.91 inference(scs_inference,[],[125,47])).
% 60.90/60.91 cnf(137,plain,
% 60.90/60.91 (~P2(f2(x1371,f2(a6,a8,x1372,x1373),x1374,x1374),a9,x1375,x1375)),
% 60.90/60.91 inference(scs_inference,[],[106,125,47,48])).
% 60.90/60.91 cnf(139,plain,
% 60.90/60.91 (~E(f2(a6,a8,x1391,x1392),f2(f2(a6,a8,x1391,x1392),a9,x1393,x1394))),
% 60.90/60.91 inference(scs_inference,[],[119,63,106,125,47,48,32])).
% 60.90/60.91 cnf(142,plain,
% 60.90/60.91 (~E(f2(f2(x1421,a12,x1422,x1422),a11,x1423,x1424),f2(x1421,a12,x1422,x1422))),
% 60.90/60.91 inference(scs_inference,[],[117,119,63,106,125,40,47,48,32,31])).
% 60.90/60.91 cnf(144,plain,
% 60.90/60.91 (P2(a10,x1441,a10,a12)+~E(a11,x1441)),
% 60.90/60.91 inference(scs_inference,[],[117,119,63,38,106,125,40,47,48,32,31,33])).
% 60.90/60.91 cnf(154,plain,
% 60.90/60.91 (~P2(f2(f2(x1541,a12,x1542,x1542),a11,x1543,x1544),f2(x1541,a12,x1542,x1542),x1545,x1545)),
% 60.90/60.91 inference(scs_inference,[],[142,139,47,48])).
% 60.90/60.91 cnf(156,plain,
% 60.90/60.91 (P2(f2(x1561,x1562,x1563,x1564),x1562,x1563,x1564)),
% 60.90/60.91 inference(scs_inference,[],[39,41,142,139,47,48,49])).
% 60.90/60.91 cnf(158,plain,
% 60.90/60.91 (P2(x1581,x1582,x1582,x1581)),
% 60.90/60.91 inference(rename_variables,[],[39])).
% 60.90/60.91 cnf(160,plain,
% 60.90/60.91 (~E(a9,f2(x1601,f2(a6,a8,x1602,x1603),x1604,x1604))),
% 60.90/60.91 inference(scs_inference,[],[137,39,158,41,142,139,47,48,49,32])).
% 60.90/60.91 cnf(163,plain,
% 60.90/60.91 (~E(f2(f2(x1631,a11,x1632,x1632),a12,x1633,x1634),f2(x1631,a11,x1632,x1632))),
% 60.90/60.91 inference(scs_inference,[],[135,137,39,158,41,142,139,40,47,48,49,32,31])).
% 60.90/60.91 cnf(165,plain,
% 60.90/60.91 (P2(a1,x1651,a1,a12)+~E(a11,x1651)),
% 60.90/60.91 inference(scs_inference,[],[135,137,39,158,37,41,142,139,40,47,48,49,32,31,33])).
% 60.90/60.91 cnf(166,plain,
% 60.90/60.91 (P2(f2(x1661,x1662,x1663,x1664),x1662,x1665,x1664)+~E(x1663,x1665)),
% 60.90/60.91 inference(scs_inference,[],[135,137,39,158,37,41,142,139,40,47,48,49,32,31,33,34])).
% 60.90/60.91 cnf(167,plain,
% 60.90/60.91 (P2(f2(x1671,x1672,x1673,x1674),x1672,x1673,x1675)+~E(x1674,x1675)),
% 60.90/60.91 inference(scs_inference,[],[135,137,39,158,37,41,142,139,40,47,48,49,32,31,33,34,35])).
% 60.90/60.91 cnf(176,plain,
% 60.90/60.91 (~P1(a9,f2(x1761,f2(a6,a8,x1762,x1763),x1764,x1764),a9)),
% 60.90/60.91 inference(scs_inference,[],[160,47])).
% 60.90/60.91 cnf(178,plain,
% 60.90/60.91 (~P2(f2(f2(x1781,a11,x1782,x1782),a12,x1783,x1784),f2(x1781,a11,x1782,x1782),x1785,x1785)),
% 60.90/60.91 inference(scs_inference,[],[163,160,47,48])).
% 60.90/60.91 cnf(180,plain,
% 60.90/60.91 (~E(f2(x1801,a12,x1802,x1802),f2(f2(x1801,a12,x1802,x1802),a11,x1803,x1804))),
% 60.90/60.91 inference(scs_inference,[],[154,63,163,160,47,48,32])).
% 60.90/60.91 cnf(182,plain,
% 60.90/60.91 (~P2(f2(f2(x1821,a12,x1822,x1822),a11,x1823,x1824),f2(x1821,a12,x1822,x1822),x1825,x1825)),
% 60.90/60.91 inference(rename_variables,[],[154])).
% 60.90/60.91 cnf(183,plain,
% 60.90/60.91 (~E(a11,f2(x1831,a12,x1832,x1832))),
% 60.90/60.91 inference(scs_inference,[],[154,182,63,156,163,160,47,48,32,33])).
% 60.90/60.91 cnf(186,plain,
% 60.90/60.91 (P1(a1,a10,x1861)+~E(a11,x1861)),
% 60.90/60.91 inference(scs_inference,[],[154,182,36,63,156,163,160,47,48,32,33,31])).
% 60.90/60.91 cnf(196,plain,
% 60.90/60.91 (~P2(f2(x1961,a12,x1962,x1962),f2(f2(x1961,a12,x1962,x1962),a11,x1963,x1964),x1965,x1965)),
% 60.90/60.91 inference(scs_inference,[],[180,47,48])).
% 60.90/60.91 cnf(198,plain,
% 60.90/60.91 (~E(f2(x1981,a11,x1982,x1982),f2(f2(x1981,a11,x1982,x1982),a12,x1983,x1984))),
% 60.90/60.91 inference(scs_inference,[],[178,39,180,47,48,32])).
% 60.90/60.91 cnf(200,plain,
% 60.90/60.91 (~P2(f2(f2(x2001,a11,x2002,x2002),a12,x2003,x2004),f2(x2001,a11,x2002,x2002),x2005,x2005)),
% 60.90/60.91 inference(rename_variables,[],[178])).
% 60.90/60.91 cnf(201,plain,
% 60.90/60.91 (~E(a12,f2(x2011,a11,x2012,x2012))),
% 60.90/60.91 inference(scs_inference,[],[178,200,39,180,156,47,48,32,33])).
% 60.90/60.91 cnf(216,plain,
% 60.90/60.91 (P2(x2161,a11,a10,a12)+~E(a10,x2161)),
% 60.90/60.91 inference(scs_inference,[],[196,38,198,156,47,48,33,32])).
% 60.90/60.91 cnf(218,plain,
% 60.90/60.91 (~P2(a12,a11,x2181,x2181)),
% 60.90/60.91 inference(rename_variables,[],[61])).
% 60.90/60.91 cnf(219,plain,
% 60.90/60.91 (~E(a10,a12)),
% 60.90/60.91 inference(scs_inference,[],[196,61,218,38,198,156,47,48,33,32,35,34])).
% 60.90/60.91 cnf(228,plain,
% 60.90/60.91 (~P1(a10,a12,a10)),
% 60.90/60.91 inference(scs_inference,[],[219,47])).
% 60.90/60.91 cnf(230,plain,
% 60.90/60.91 (~P2(a10,a12,x2301,x2301)),
% 60.90/60.91 inference(scs_inference,[],[219,47,48])).
% 60.90/60.91 cnf(242,plain,
% 60.90/60.91 (~P1(a11,f2(x2421,a12,x2422,x2422),a11)),
% 60.90/60.91 inference(scs_inference,[],[183,47])).
% 60.90/60.91 cnf(244,plain,
% 60.90/60.91 (~P2(a11,f2(x2441,a12,x2442,x2442),x2443,x2443)),
% 60.90/60.91 inference(scs_inference,[],[183,47,48])).
% 60.90/60.91 cnf(246,plain,
% 60.90/60.91 (~E(a12,a10)),
% 60.90/60.91 inference(scs_inference,[],[230,39,183,47,48,32])).
% 60.90/60.91 cnf(248,plain,
% 60.90/60.91 (~P2(a10,a12,x2481,x2481)),
% 60.90/60.91 inference(rename_variables,[],[230])).
% 60.90/60.91 cnf(249,plain,
% 60.90/60.91 (~E(f2(x2491,a10,x2492,x2492),a12)),
% 60.90/60.91 inference(scs_inference,[],[230,248,39,41,183,47,48,32,33])).
% 60.90/60.91 cnf(258,plain,
% 60.90/60.91 (~P2(a12,a10,x2581,x2581)),
% 60.90/60.91 inference(scs_inference,[],[246,47,48])).
% 60.90/60.91 cnf(260,plain,
% 60.90/60.91 (P2(a10,a12,a11,a10)),
% 60.90/60.91 inference(scs_inference,[],[38,39,246,47,48,49])).
% 60.90/60.91 cnf(263,plain,
% 60.90/60.91 (~E(a10,a11)),
% 60.90/60.91 inference(scs_inference,[],[230,38,39,246,47,48,49,35])).
% 60.90/60.91 cnf(264,plain,
% 60.90/60.91 (~P2(a10,a12,x2641,x2641)),
% 60.90/60.91 inference(rename_variables,[],[230])).
% 60.90/60.91 cnf(265,plain,
% 60.90/60.91 (~E(f2(x2651,f2(x2652,a12,x2653,x2653),x2654,x2654),a11)),
% 60.90/60.91 inference(scs_inference,[],[244,230,38,39,156,246,47,48,49,35,32])).
% 60.90/60.91 cnf(267,plain,
% 60.90/60.91 (~E(a11,a10)),
% 60.90/60.91 inference(scs_inference,[],[244,230,264,38,39,156,246,47,48,49,35,32,34])).
% 60.90/60.91 cnf(269,plain,
% 60.90/60.91 (~E(f2(x2691,a11,x2692,x2692),f2(x2693,a12,x2694,x2694))),
% 60.90/60.91 inference(scs_inference,[],[244,230,264,38,39,41,156,246,47,48,49,35,32,34,33])).
% 60.90/60.91 cnf(276,plain,
% 60.90/60.91 (~P1(f2(x2761,a11,x2762,x2762),f2(x2763,a12,x2764,x2764),f2(x2761,a11,x2762,x2762))),
% 60.90/60.91 inference(scs_inference,[],[269,47])).
% 60.90/60.91 cnf(278,plain,
% 60.90/60.91 (~P2(f2(x2781,a11,x2782,x2782),f2(x2783,a12,x2784,x2784),x2785,x2785)),
% 60.90/60.91 inference(scs_inference,[],[269,47,48])).
% 60.90/60.91 cnf(280,plain,
% 60.90/60.91 (P2(a1,a12,a11,a1)),
% 60.90/60.91 inference(scs_inference,[],[37,39,269,47,48,49])).
% 60.90/60.91 cnf(283,plain,
% 60.90/60.91 (~E(f2(x2831,a12,x2832,x2832),a10)),
% 60.90/60.91 inference(scs_inference,[],[258,37,39,41,269,47,48,49,33])).
% 60.90/60.91 cnf(285,plain,
% 60.90/60.91 (P2(a1,a12,a11,x2851)+~E(a1,x2851)),
% 60.90/60.91 inference(scs_inference,[],[258,37,39,41,269,47,48,49,33,35])).
% 60.90/60.91 cnf(286,plain,
% 60.90/60.91 (~E(a1,a11)),
% 60.90/60.91 inference(scs_inference,[],[258,99,37,39,41,269,47,48,49,33,35,32])).
% 60.90/60.91 cnf(292,plain,
% 60.90/60.91 (~P2(a1,a11,x2921,x2921)),
% 60.90/60.91 inference(scs_inference,[],[286,47,48])).
% 60.90/60.91 cnf(294,plain,
% 60.90/60.91 (P2(a10,a12,a10,a11)),
% 60.90/60.91 inference(scs_inference,[],[38,63,286,47,48,49])).
% 60.90/60.91 cnf(295,plain,
% 60.90/60.91 (P2(x2951,x2952,x2951,x2952)),
% 60.90/60.91 inference(rename_variables,[],[63])).
% 60.90/60.91 cnf(297,plain,
% 60.90/60.91 (~E(a12,a1)),
% 60.90/60.91 inference(scs_inference,[],[38,37,63,286,47,48,49,35])).
% 60.90/60.91 cnf(298,plain,
% 60.90/60.91 (~E(f2(x2981,a12,x2982,x2982),f2(x2983,a11,x2984,x2984))),
% 60.90/60.91 inference(scs_inference,[],[278,38,37,39,63,286,47,48,49,35,32])).
% 60.90/60.91 cnf(300,plain,
% 60.90/60.91 (~P2(f2(x3001,a11,x3002,x3002),f2(x3003,a12,x3004,x3004),x3005,x3005)),
% 60.90/60.91 inference(rename_variables,[],[278])).
% 60.90/60.91 cnf(301,plain,
% 60.90/60.91 (~E(f2(x3011,f2(x3012,a11,x3013,x3013),x3014,x3014),f2(x3015,a12,x3016,x3016))),
% 60.90/60.91 inference(scs_inference,[],[278,300,38,37,39,63,41,286,47,48,49,35,32,33])).
% 60.90/60.91 cnf(303,plain,
% 60.90/60.91 (P2(a1,a12,x3031,a1)+~E(a11,x3031)),
% 60.90/60.91 inference(scs_inference,[],[278,300,38,37,39,63,41,286,280,47,48,49,35,32,33,34])).
% 60.90/60.91 cnf(308,plain,
% 60.90/60.91 (~P1(a10,a11,f2(x3081,a11,x3082,x3082))+~P2(a11,f2(a10,a12,x3083,x3083),a12,f2(a10,a12,x3083,x3083))+~P2(a11,f2(x3081,a11,x3082,x3082),a12,f2(a10,a12,x3083,x3083))),
% 60.90/60.91 inference(scs_inference,[],[278,300,38,37,40,39,63,295,41,286,263,280,47,48,49,35,32,33,51])).
% 60.90/60.91 cnf(310,plain,
% 60.90/60.91 (~E(a1,a12)),
% 60.90/60.91 inference(scs_inference,[],[292,88])).
% 60.90/60.91 cnf(311,plain,
% 60.90/60.91 (~P2(a1,a11,x3111,x3111)),
% 60.90/60.91 inference(rename_variables,[],[292])).
% 60.90/60.91 cnf(312,plain,
% 60.90/60.91 (~P1(a11,a10,a11)),
% 60.90/60.91 inference(scs_inference,[],[292,267,88,47])).
% 60.90/60.91 cnf(314,plain,
% 60.90/60.91 (~P2(a11,a10,x3141,x3141)),
% 60.90/60.91 inference(scs_inference,[],[292,267,88,47,48])).
% 60.90/60.91 cnf(316,plain,
% 60.90/60.91 (~E(a11,a1)),
% 60.90/60.91 inference(scs_inference,[],[292,311,63,267,88,47,48,35])).
% 60.90/60.91 cnf(318,plain,
% 60.90/60.91 (~P2(a1,a11,x3181,x3181)),
% 60.90/60.91 inference(rename_variables,[],[292])).
% 60.90/60.91 cnf(319,plain,
% 60.90/60.91 (~E(f2(x3191,a11,x3192,x3192),a1)),
% 60.90/60.91 inference(scs_inference,[],[292,311,318,63,156,267,88,47,48,35,32])).
% 60.90/60.91 cnf(321,plain,
% 60.90/60.91 (~E(f2(x3211,a1,x3212,x3212),a11)),
% 60.90/60.91 inference(scs_inference,[],[292,311,318,63,41,156,267,88,47,48,35,32,33])).
% 60.90/60.91 cnf(331,plain,
% 60.90/60.91 (~P2(f2(x3311,f2(x3312,a11,x3313,x3313),x3314,x3314),f2(x3315,a12,x3316,x3316),x3317,x3317)),
% 60.90/60.91 inference(scs_inference,[],[301,298,47,48])).
% 60.90/60.91 cnf(333,plain,
% 60.90/60.91 (P2(a1,a12,a1,a11)),
% 60.90/60.91 inference(scs_inference,[],[37,63,301,298,47,48,49])).
% 60.90/60.91 cnf(336,plain,
% 60.90/60.91 (~E(f2(x3361,a10,x3362,x3362),a11)),
% 60.90/60.91 inference(scs_inference,[],[314,37,63,156,301,298,47,48,49,32])).
% 60.90/60.91 cnf(338,plain,
% 60.90/60.91 (~E(f2(x3381,a11,x3382,x3382),a10)),
% 60.90/60.91 inference(scs_inference,[],[314,37,63,41,156,301,298,47,48,49,32,33])).
% 60.90/60.91 cnf(340,plain,
% 60.90/60.91 (P2(a1,a12,x3401,a11)+~E(a1,x3401)),
% 60.90/60.91 inference(scs_inference,[],[314,37,63,41,156,301,298,47,48,49,32,33,34])).
% 60.90/60.91 cnf(341,plain,
% 60.90/60.91 (P2(a1,a12,a1,x3411)+~E(a11,x3411)),
% 60.90/60.91 inference(scs_inference,[],[314,37,63,41,156,301,298,47,48,49,32,33,34,35])).
% 60.90/60.91 cnf(348,plain,
% 60.90/60.91 (P1(a11,f2(a11,a12,x3481,x3482),f3(a11,a11,a12,f2(a11,a12,x3481,x3482),f2(a11,a12,x3481,x3482)))),
% 60.90/60.91 inference(scs_inference,[],[43,40,2,54])).
% 60.90/60.91 cnf(351,plain,
% 60.90/60.91 (~P2(f2(x3511,a12,x3512,x3512),f2(x3513,a11,x3514,x3514),x3515,x3515)),
% 60.90/60.91 inference(scs_inference,[],[298,297,47,48])).
% 60.90/60.91 cnf(354,plain,
% 60.90/60.91 (P1(a11,f2(a11,a12,x3541,x3542),f3(a11,a11,a12,f2(a11,a12,x3541,x3542),f2(a11,a12,x3541,x3542)))),
% 60.90/60.91 inference(rename_variables,[],[348])).
% 60.90/60.91 cnf(356,plain,
% 60.90/60.91 (~E(a12,f2(x3561,f2(x3562,a11,x3563,x3563),x3564,x3564))),
% 60.90/60.91 inference(scs_inference,[],[242,331,348,41,298,297,47,48,31,32])).
% 60.90/60.91 cnf(359,plain,
% 60.90/60.91 (P1(x3591,f2(a11,a12,x3592,x3593),f3(a11,a11,a12,f2(a11,a12,x3592,x3593),f2(a11,a12,x3592,x3593)))+~E(a11,x3591)),
% 60.90/60.91 inference(scs_inference,[],[242,331,348,354,41,298,297,47,48,31,32,29])).
% 60.90/60.91 cnf(361,plain,
% 60.90/60.91 (P2(a10,x3611,a11,a10)+~E(a12,x3611)),
% 60.90/60.91 inference(scs_inference,[],[242,331,348,354,41,260,298,297,47,48,31,32,29,30,33])).
% 60.90/60.91 cnf(371,plain,
% 60.90/60.91 (~P2(a1,a12,x3711,x3711)),
% 60.90/60.91 inference(scs_inference,[],[310,47,48])).
% 60.90/60.91 cnf(373,plain,
% 60.90/60.91 (~E(f2(a11,a10,x3731,x3732),a11)),
% 60.90/60.91 inference(scs_inference,[],[312,40,310,47,48,31])).
% 60.90/60.91 cnf(375,plain,
% 60.90/60.91 (P2(x3751,a12,a11,a10)+~E(a10,x3751)),
% 60.90/60.91 inference(scs_inference,[],[312,40,260,310,47,48,31,32])).
% 60.90/60.91 cnf(376,plain,
% 60.90/60.91 (P2(a12,x3761,a11,a10)+~E(a10,x3761)),
% 60.90/60.91 inference(scs_inference,[],[312,39,40,260,310,47,48,31,32,49])).
% 60.90/60.91 cnf(381,plain,
% 60.90/60.91 (P2(a12,a10,a11,a10)),
% 60.90/60.91 inference(equality_inference,[],[376])).
% 60.90/60.91 cnf(382,plain,
% 60.90/60.91 (~P1(a11,a1,a11)),
% 60.90/60.91 inference(scs_inference,[],[316,47])).
% 60.90/60.91 cnf(384,plain,
% 60.90/60.91 (~P2(a11,a1,x3841,x3841)),
% 60.90/60.91 inference(scs_inference,[],[316,47,48])).
% 60.90/60.91 cnf(387,plain,
% 60.90/60.91 (P2(a12,x3871,a10,a11)+~E(a10,x3871)),
% 60.90/60.91 inference(scs_inference,[],[39,294,316,47,48,32,49])).
% 60.90/60.91 cnf(392,plain,
% 60.90/60.91 (P2(a12,a10,a10,a11)),
% 60.90/60.91 inference(equality_inference,[],[387])).
% 60.90/60.91 cnf(393,plain,
% 60.90/60.91 (~P1(a12,f2(x3931,f2(x3932,a11,x3933,x3933),x3934,x3934),a12)),
% 60.90/60.91 inference(scs_inference,[],[356,47])).
% 60.90/60.91 cnf(397,plain,
% 60.90/60.91 (P2(x3971,a12,a11,a1)+~E(a1,x3971)),
% 60.90/60.91 inference(scs_inference,[],[280,265,356,47,48,32])).
% 60.90/60.91 cnf(398,plain,
% 60.90/60.91 (P2(a12,x3981,a11,a1)+~E(a1,x3981)),
% 60.90/60.91 inference(scs_inference,[],[39,280,265,356,47,48,32,49])).
% 60.90/60.91 cnf(403,plain,
% 60.90/60.91 (P2(a12,a1,a11,a1)),
% 60.90/60.91 inference(equality_inference,[],[398])).
% 60.90/60.91 cnf(404,plain,
% 60.90/60.91 (~P1(a12,f2(x4041,a11,x4042,x4042),a12)),
% 60.90/60.91 inference(scs_inference,[],[201,47])).
% 60.90/60.91 cnf(406,plain,
% 60.90/60.91 (~P2(a12,f2(x4061,a11,x4062,x4062),x4063,x4063)),
% 60.90/60.91 inference(scs_inference,[],[201,47,48])).
% 60.90/60.91 cnf(408,plain,
% 60.90/60.91 (P2(a12,a1,a11,x4081)+~E(a1,x4081)),
% 60.90/60.91 inference(scs_inference,[],[201,403,47,48,35])).
% 60.90/60.91 cnf(414,plain,
% 60.90/60.91 (~P1(f2(x4141,a10,x4142,x4142),a12,f2(x4141,a10,x4142,x4142))),
% 60.90/60.91 inference(scs_inference,[],[249,47])).
% 60.90/60.91 cnf(416,plain,
% 60.90/60.91 (~P2(f2(x4161,a10,x4162,x4162),a12,x4163,x4163)),
% 60.90/60.91 inference(scs_inference,[],[249,47,48])).
% 60.90/60.91 cnf(418,plain,
% 60.90/60.91 (~E(f2(x4181,a12,x4182,x4182),a1)),
% 60.90/60.91 inference(scs_inference,[],[371,156,249,47,48,32])).
% 60.90/60.91 cnf(420,plain,
% 60.90/60.91 (~E(f2(x4201,a1,x4202,x4202),a12)),
% 60.90/60.91 inference(scs_inference,[],[371,156,41,249,47,48,32,33])).
% 60.90/60.91 cnf(422,plain,
% 60.90/60.91 (P2(a12,a1,x4221,a1)+~E(a11,x4221)),
% 60.90/60.91 inference(scs_inference,[],[371,156,41,249,403,47,48,32,33,34])).
% 60.90/60.91 cnf(430,plain,
% 60.90/60.91 (~P2(f2(x4301,a12,x4302,x4302),a10,x4303,x4303)),
% 60.90/60.91 inference(scs_inference,[],[283,47,48])).
% 60.90/60.91 cnf(432,plain,
% 60.90/60.91 (P2(x4321,a12,a1,a11)+~E(a1,x4321)),
% 60.90/60.91 inference(scs_inference,[],[333,283,47,48,32])).
% 60.90/60.91 cnf(433,plain,
% 60.90/60.91 (P2(a12,x4331,a1,a11)+~E(a1,x4331)),
% 60.90/60.91 inference(scs_inference,[],[39,333,283,47,48,32,49])).
% 60.90/60.91 cnf(438,plain,
% 60.90/60.91 (P2(a12,a1,a1,a11)),
% 60.90/60.91 inference(equality_inference,[],[433])).
% 60.90/60.91 cnf(441,plain,
% 60.90/60.91 (~P2(f2(x4411,a11,x4412,x4412),a1,x4413,x4413)),
% 60.90/60.91 inference(scs_inference,[],[319,47,48])).
% 60.90/60.91 cnf(443,plain,
% 60.90/60.91 (P2(a12,a1,a1,x4431)+~E(a11,x4431)),
% 60.90/60.91 inference(scs_inference,[],[319,438,47,48,35])).
% 60.90/60.91 cnf(449,plain,
% 60.90/60.91 (~P1(f2(x4491,a1,x4492,x4492),a11,f2(x4491,a1,x4492,x4492))),
% 60.90/60.91 inference(scs_inference,[],[321,47])).
% 60.90/60.91 cnf(451,plain,
% 60.90/60.91 (~P2(f2(x4511,a1,x4512,x4512),a11,x4513,x4513)),
% 60.90/60.91 inference(scs_inference,[],[321,47,48])).
% 60.90/60.91 cnf(453,plain,
% 60.90/60.91 (P2(a12,a1,x4531,a11)+~E(a1,x4531)),
% 60.90/60.91 inference(scs_inference,[],[321,438,47,48,34])).
% 60.90/60.91 cnf(461,plain,
% 60.90/60.91 (~P2(f2(x4611,a10,x4612,x4612),a11,x4613,x4613)),
% 60.90/60.91 inference(scs_inference,[],[336,47,48])).
% 60.90/60.91 cnf(463,plain,
% 60.90/60.91 (P2(a10,x4631,a10,a11)+~E(a12,x4631)),
% 60.90/60.91 inference(scs_inference,[],[294,336,47,48,33])).
% 60.90/60.91 cnf(464,plain,
% 60.90/60.91 (P2(x4641,a10,a10,a11)+~E(a12,x4641)),
% 60.90/60.91 inference(scs_inference,[],[39,294,336,47,48,33,49])).
% 60.90/60.91 cnf(472,plain,
% 60.90/60.91 (~P2(f2(x4721,a11,x4722,x4722),a10,x4723,x4723)),
% 60.90/60.91 inference(scs_inference,[],[338,47,48])).
% 60.90/60.91 cnf(474,plain,
% 60.90/60.91 (P2(x4741,a1,a11,a1)+~E(a12,x4741)),
% 60.90/60.91 inference(scs_inference,[],[403,338,47,48,32])).
% 60.90/60.91 cnf(475,plain,
% 60.90/60.91 (P2(a1,x4751,a11,a1)+~E(a12,x4751)),
% 60.90/60.91 inference(scs_inference,[],[39,403,338,47,48,32,49])).
% 60.90/60.91 cnf(483,plain,
% 60.90/60.91 (~P2(f2(x4831,a12,x4832,x4832),a1,x4833,x4833)),
% 60.90/60.91 inference(scs_inference,[],[418,47,48])).
% 60.90/60.91 cnf(485,plain,
% 60.90/60.91 (P2(a1,x4851,a1,a11)+~E(a12,x4851)),
% 60.90/60.91 inference(scs_inference,[],[333,418,47,48,33])).
% 60.90/60.91 cnf(486,plain,
% 60.90/60.91 (P2(x4861,a1,a1,a11)+~E(a12,x4861)),
% 60.90/60.91 inference(scs_inference,[],[39,333,418,47,48,33,49])).
% 60.90/60.91 cnf(492,plain,
% 60.90/60.91 (~P1(f2(x4921,a1,x4922,x4922),a12,f2(x4921,a1,x4922,x4922))),
% 60.90/60.91 inference(scs_inference,[],[420,47])).
% 60.90/60.91 cnf(496,plain,
% 60.90/60.91 (P2(x4961,a10,a11,a10)+~E(a12,x4961)),
% 60.90/60.91 inference(scs_inference,[],[381,420,47,48,32])).
% 60.90/60.91 cnf(516,plain,
% 60.90/60.91 (E(f2(f2(x5161,x5162,x5163,x5163),x5164,x5165,x5166),f2(x5162,x5164,x5165,x5166))),
% 60.90/60.91 inference(scs_inference,[],[156,4,48])).
% 60.90/60.91 cnf(517,plain,
% 60.90/60.91 (E(f2(x5171,x5172,x5173,x5174),f2(f2(x5175,x5171,x5176,x5176),x5172,x5173,x5174))),
% 60.90/60.91 inference(scs_inference,[],[516,2])).
% 60.90/60.91 cnf(518,plain,
% 60.90/60.91 (P2(x5181,f2(f2(x5182,x5183,x5184,x5184),x5185,x5186,x5187),f2(x5183,x5185,x5186,x5187),x5181)),
% 60.90/60.91 inference(scs_inference,[],[516,2,73])).
% 60.90/60.91 cnf(533,plain,
% 60.90/60.91 (~P2(f2(a12,a11,x5331,x5332),a12,x5333,x5333)),
% 60.90/60.91 inference(scs_inference,[],[517,83,73,47,48])).
% 60.90/60.91 cnf(547,plain,
% 60.90/60.91 (~P2(f2(a11,a12,x5471,x5472),a11,x5473,x5473)),
% 60.90/60.91 inference(scs_inference,[],[123,47,48])).
% 60.90/60.91 cnf(554,plain,
% 60.90/60.91 (~P2(f2(a11,a10,x5541,x5542),a11,x5543,x5543)),
% 60.90/60.91 inference(scs_inference,[],[373,47,48])).
% 60.90/60.91 cnf(559,plain,
% 60.90/60.91 (~P1(a10,a1,a10)),
% 60.90/60.91 inference(scs_inference,[],[42,47])).
% 60.90/60.91 cnf(566,plain,
% 60.90/60.91 (~P1(a10,a11,a10)),
% 60.90/60.91 inference(scs_inference,[],[263,47])).
% 60.90/60.91 cnf(588,plain,
% 60.90/60.91 (~P2(f2(x5881,a12,x5882,x5882),a11,x5883,x5883)),
% 60.90/60.91 inference(scs_inference,[],[85,48])).
% 60.90/60.91 cnf(598,plain,
% 60.90/60.91 (~P2(a10,a1,x5981,x5981)),
% 60.90/60.91 inference(scs_inference,[],[42,48])).
% 60.90/60.91 cnf(633,plain,
% 60.90/60.91 (~E(f2(a10,a1,x6331,x6332),a10)),
% 60.90/60.91 inference(scs_inference,[],[559,40,31])).
% 60.90/60.91 cnf(1588,plain,
% 60.90/60.91 (~P2(f2(x15881,x15882,x15883,x15883),x15882,a1,a12)),
% 60.90/60.91 inference(scs_inference,[],[371,156,49])).
% 60.90/60.91 cnf(1591,plain,
% 60.90/60.91 (~E(a1,f2(x15911,a11,x15912,x15912))),
% 60.90/60.91 inference(scs_inference,[],[371,37,156,49,32])).
% 60.90/60.91 cnf(1592,plain,
% 60.90/60.91 (~P2(a1,f2(x15921,a11,x15922,x15922),x15923,x15923)),
% 60.90/60.91 inference(scs_inference,[],[371,37,156,49,32,48])).
% 60.90/60.91 cnf(1599,plain,
% 60.90/60.91 (~P2(a1,a11,f2(x15991,x15992,x15993,x15993),x15992)),
% 60.90/60.91 inference(scs_inference,[],[37,1588,49])).
% 60.90/60.91 cnf(1601,plain,
% 60.90/60.91 (~E(a1,f2(x16011,a12,x16012,x16012))),
% 60.90/60.91 inference(scs_inference,[],[37,1588,49,88])).
% 60.90/60.91 cnf(1602,plain,
% 60.90/60.91 (~P2(a1,f2(x16021,a12,x16022,x16022),x16023,x16023)),
% 60.90/60.91 inference(scs_inference,[],[37,1588,49,88,48])).
% 60.90/60.91 cnf(1609,plain,
% 60.90/60.91 (~P2(x16091,x16091,a1,a12)),
% 60.90/60.92 inference(scs_inference,[],[371,39,49])).
% 60.90/60.92 cnf(1621,plain,
% 60.90/60.92 (~P1(a11,f2(x16211,a1,x16212,x16212),a11)),
% 60.90/60.92 inference(scs_inference,[],[371,41,49,165,48,47])).
% 60.90/60.92 cnf(4046,plain,
% 60.90/60.92 (P1(a11,a11,f4(a11,a11,a12,f2(a11,a12,x40461,x40462),f2(a11,a12,x40461,x40462)))),
% 60.90/60.92 inference(scs_inference,[],[43,40,2,55])).
% 60.90/60.92 cnf(4047,plain,
% 60.90/60.92 (P1(x40471,a11,f4(a11,a11,a12,f2(a11,a12,x40472,x40473),f2(a11,a12,x40472,x40473)))+~E(a11,x40471)),
% 60.90/60.92 inference(scs_inference,[],[4046,29])).
% 60.90/60.92 cnf(4049,plain,
% 60.90/60.92 (P1(a11,x40491,f4(a11,a11,a12,f2(a11,a12,x40492,x40493),f2(a11,a12,x40492,x40493)))+~E(a11,x40491)),
% 60.90/60.92 inference(scs_inference,[],[4046,29,31,30])).
% 60.90/60.92 cnf(4058,plain,
% 60.90/60.92 (~E(f2(a8,a9,x40581,x40582),a6)),
% 60.90/60.92 inference(scs_inference,[],[45,40,31])).
% 60.90/60.92 cnf(4406,plain,
% 60.90/60.92 (~E(f2(a9,a6,x44061,x44062),a8)),
% 60.90/60.92 inference(scs_inference,[],[46,40,31])).
% 60.90/60.92 cnf(4935,plain,
% 60.90/60.92 (P1(f2(x49351,x49352,x49353,x49353),x49354,f2(x49352,x49354,x49355,x49356))),
% 60.90/60.92 inference(scs_inference,[],[517,40,2,31])).
% 60.90/60.92 cnf(5072,plain,
% 60.90/60.92 (E(x50721,f2(x50721,x50721,x50722,x50722))),
% 60.90/60.92 inference(scs_inference,[],[4935,47,2])).
% 60.90/60.92 cnf(5073,plain,
% 60.90/60.92 (P1(x50731,f2(x50732,x50732,x50733,x50733),f2(x50731,x50732,x50734,x50735))),
% 60.90/60.92 inference(scs_inference,[],[5072,72])).
% 60.90/60.92 cnf(5074,plain,
% 60.90/60.92 (P2(x50741,f2(x50742,x50741,x50743,x50744),x50743,f2(x50744,x50744,x50745,x50745))),
% 60.90/60.92 inference(scs_inference,[],[5072,72,74])).
% 60.90/60.92 cnf(5075,plain,
% 60.90/60.92 (P2(x50751,f2(x50752,x50751,x50753,x50754),f2(x50753,x50753,x50755,x50755),x50754)),
% 60.90/60.92 inference(scs_inference,[],[5072,72,74,127])).
% 60.90/60.92 cnf(5076,plain,
% 60.90/60.92 (P2(f2(x50761,x50762,x50763,x50764),x50762,f2(x50763,x50763,x50765,x50765),x50764)),
% 60.90/60.92 inference(scs_inference,[],[5072,72,74,127,166])).
% 60.90/60.92 cnf(5077,plain,
% 60.90/60.92 (P2(f2(x50771,x50772,x50773,x50774),x50772,x50773,f2(x50774,x50774,x50775,x50775))),
% 60.90/60.92 inference(scs_inference,[],[5072,72,74,127,166,167])).
% 60.90/60.92 cnf(5078,plain,
% 60.90/60.92 (P1(f2(a11,a11,x50781,x50781),f2(a11,a12,x50782,x50783),f3(a11,a11,a12,f2(a11,a12,x50782,x50783),f2(a11,a12,x50782,x50783)))),
% 60.90/60.92 inference(scs_inference,[],[5072,72,74,127,166,167,359])).
% 60.90/60.92 cnf(5079,plain,
% 60.90/60.92 (E(x50791,f2(x50791,x50791,x50792,x50792))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5081,plain,
% 60.90/60.92 (E(x50811,f2(x50811,x50811,x50812,x50812))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5083,plain,
% 60.90/60.92 (E(x50831,f2(x50831,x50831,x50832,x50832))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5084,plain,
% 60.90/60.92 (E(f2(x50841,x50841,x50842,x50842),x50841)),
% 60.90/60.92 inference(scs_inference,[],[5072,5079,5081,5083,72,74,127,166,167,359,4047,4049,2])).
% 60.90/60.92 cnf(5085,plain,
% 60.90/60.92 (P2(x50851,x50852,f2(x50852,x50852,x50853,x50853),x50851)),
% 60.90/60.92 inference(scs_inference,[],[5072,5079,5081,5083,72,74,127,166,167,359,4047,4049,2,73])).
% 60.90/60.92 cnf(5086,plain,
% 60.90/60.92 (P1(a1,a10,f2(a11,a11,x50861,x50861))),
% 60.90/60.92 inference(scs_inference,[],[5072,5079,5081,5083,36,72,74,127,166,167,359,4047,4049,2,73,31])).
% 60.90/60.92 cnf(5087,plain,
% 60.90/60.92 (E(x50871,f2(x50871,x50871,x50872,x50872))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5088,plain,
% 60.90/60.92 (P1(a1,f2(a10,a10,x50881,x50881),a11)),
% 60.90/60.92 inference(scs_inference,[],[5072,5079,5081,5083,5087,36,72,74,127,166,167,359,4047,4049,2,73,31,30])).
% 60.90/60.92 cnf(5089,plain,
% 60.90/60.92 (E(x50891,f2(x50891,x50891,x50892,x50892))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5094,plain,
% 60.90/60.92 (E(x50941,f2(x50941,x50941,x50942,x50942))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5095,plain,
% 60.90/60.92 (P2(f2(a10,a10,x50951,x50951),a11,a10,a12)),
% 60.90/60.92 inference(scs_inference,[],[371,5072,5079,5081,5083,5087,5089,5094,38,36,72,74,127,166,167,359,4047,4049,2,73,31,30,49,29,32])).
% 60.90/60.92 cnf(5096,plain,
% 60.90/60.92 (E(x50961,f2(x50961,x50961,x50962,x50962))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5097,plain,
% 60.90/60.92 (P2(a10,f2(a11,a11,x50971,x50971),a10,a12)),
% 60.90/60.92 inference(scs_inference,[],[371,5072,5079,5081,5083,5087,5089,5094,5096,38,36,72,74,127,166,167,359,4047,4049,2,73,31,30,49,29,32,33])).
% 60.90/60.92 cnf(5100,plain,
% 60.90/60.92 (E(f2(x51001,x51002,x51003,x51004),f2(f2(x51005,x51001,x51006,x51006),x51002,x51003,x51004))),
% 60.90/60.92 inference(rename_variables,[],[517])).
% 60.90/60.92 cnf(5103,plain,
% 60.90/60.92 (P1(a11,x51031,f2(f2(a11,a11,x51032,x51032),x51031,x51033,x51034))),
% 60.90/60.92 inference(scs_inference,[],[371,517,5100,5072,5079,5081,5083,5087,5089,5094,5096,38,36,72,74,127,166,167,359,4047,4049,2,73,31,30,49,29,32,33,35,34,71])).
% 60.90/60.92 cnf(5112,plain,
% 60.90/60.92 (P2(f2(x51121,x51122,f2(x51123,x51123,x51124,x51124),x51125),x51122,x51123,x51125)),
% 60.90/60.92 inference(scs_inference,[],[5084,166])).
% 60.90/60.92 cnf(5113,plain,
% 60.90/60.92 (P1(x51131,x51132,f2(f2(x51131,x51131,x51133,x51133),x51132,x51134,x51135))),
% 60.90/60.92 inference(scs_inference,[],[5084,166,71])).
% 60.90/60.92 cnf(5114,plain,
% 60.90/60.92 (P1(x51141,x51142,f2(x51141,f2(x51142,x51142,x51143,x51143),x51144,x51145))),
% 60.90/60.92 inference(scs_inference,[],[5084,166,71,72])).
% 60.90/60.92 cnf(5115,plain,
% 60.90/60.92 (P2(f2(x51151,x51152,x51153,f2(x51154,x51154,x51155,x51155)),x51152,x51153,x51154)),
% 60.90/60.92 inference(scs_inference,[],[5084,166,71,72,167])).
% 60.90/60.92 cnf(5116,plain,
% 60.90/60.92 (P2(x51161,f2(x51162,x51161,x51163,f2(x51164,x51164,x51165,x51165)),x51163,x51164)),
% 60.90/60.92 inference(scs_inference,[],[5084,166,71,72,167,74])).
% 60.90/60.92 cnf(5117,plain,
% 60.90/60.92 (P2(x51171,f2(x51172,x51171,f2(x51173,x51173,x51174,x51174),x51175),x51173,x51175)),
% 60.90/60.92 inference(scs_inference,[],[5084,166,71,72,167,74,127])).
% 60.90/60.92 cnf(5118,plain,
% 60.90/60.92 (P2(x51181,f2(x51182,x51182,x51183,x51183),x51182,x51181)),
% 60.90/60.92 inference(scs_inference,[],[5084,166,71,72,167,74,127,73])).
% 60.90/60.92 cnf(5126,plain,
% 60.90/60.92 (P1(x51261,f2(f2(x51262,x51263,x51264,x51264),x51263,x51265,x51265),f2(x51261,x51263,x51266,x51267))),
% 60.90/60.92 inference(scs_inference,[],[276,371,517,5084,5074,5073,5078,166,71,72,167,74,127,73,31,49,30])).
% 60.90/60.92 cnf(5130,plain,
% 60.90/60.92 (E(x51301,f2(x51301,x51301,x51302,x51302))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5132,plain,
% 60.90/60.92 (E(x51321,f2(x51321,x51321,x51322,x51322))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5133,plain,
% 60.90/60.92 (P2(a12,f2(a1,a1,x51331,x51331),a11,a1)),
% 60.90/60.92 inference(scs_inference,[],[276,371,517,5084,5072,5130,5132,403,5074,5073,5078,5103,166,71,72,167,74,127,73,31,49,30,29,32,33])).
% 60.90/60.92 cnf(5134,plain,
% 60.90/60.92 (E(x51341,f2(x51341,x51341,x51342,x51342))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5135,plain,
% 60.90/60.92 (P2(a10,f2(a11,a11,x51351,x51351),a10,f2(a12,a12,x51352,x51352))),
% 60.90/60.92 inference(scs_inference,[],[276,371,517,5084,5072,5130,5132,5134,403,5074,5073,5078,5103,5097,166,71,72,167,74,127,73,31,49,30,29,32,33,35])).
% 60.90/60.92 cnf(5136,plain,
% 60.90/60.92 (E(x51361,f2(x51361,x51361,x51362,x51362))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5137,plain,
% 60.90/60.92 (P2(a10,f2(a11,a11,x51371,x51371),f2(a10,a10,x51372,x51372),a12)),
% 60.90/60.92 inference(scs_inference,[],[276,371,517,5084,5072,5130,5132,5134,5136,403,5074,5073,5078,5103,5097,166,71,72,167,74,127,73,31,49,30,29,32,33,35,34])).
% 60.90/60.92 cnf(5139,plain,
% 60.90/60.92 (~E(a11,f2(x51391,a1,f2(x51392,x51392,x51393,x51393),x51392))),
% 60.90/60.92 inference(scs_inference,[],[276,371,517,5084,5072,5130,5132,5134,5136,403,5074,5073,5078,5103,5097,166,71,72,167,74,127,73,31,49,30,29,32,33,35,34,165])).
% 60.90/60.92 cnf(5146,plain,
% 60.90/60.92 (~E(a12,f2(a10,a10,x51461,x51461))),
% 60.90/60.92 inference(scs_inference,[],[276,371,517,5084,5072,5130,5132,5134,5136,403,246,5074,5073,5078,5103,5097,166,71,72,167,74,127,73,31,49,30,29,32,33,35,34,165,47,48,308,3])).
% 60.90/60.92 cnf(5150,plain,
% 60.90/60.92 (~P1(a12,f2(a10,a10,x51501,x51501),a12)),
% 60.90/60.92 inference(scs_inference,[],[5146,47])).
% 60.90/60.92 cnf(5158,plain,
% 60.90/60.92 (P1(a1,f2(a10,a10,x51581,x51581),f2(a11,a11,x51582,x51582))),
% 60.90/60.92 inference(scs_inference,[],[371,5072,5075,5139,5146,5086,47,48,49,30])).
% 60.90/60.92 cnf(5159,plain,
% 60.90/60.92 (E(x51591,f2(x51591,x51591,x51592,x51592))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5160,plain,
% 60.90/60.92 (~E(f2(f2(a12,a12,x51601,x51601),a11,x51602,x51603),a12)),
% 60.90/60.92 inference(scs_inference,[],[59,371,5072,5075,5113,5139,5146,5086,47,48,49,30,31])).
% 60.90/60.92 cnf(5162,plain,
% 60.90/60.92 (P1(f2(a1,a1,x51621,x51621),f2(a10,a10,x51622,x51622),a11)),
% 60.90/60.92 inference(scs_inference,[],[59,371,5072,5159,5075,5113,5139,5146,5086,5088,47,48,49,30,31,29])).
% 60.90/60.92 cnf(5163,plain,
% 60.90/60.92 (E(x51631,f2(x51631,x51631,x51632,x51632))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5164,plain,
% 60.90/60.92 (P2(f2(a12,a12,x51641,x51641),a1,a1,a11)),
% 60.90/60.92 inference(scs_inference,[],[59,371,5072,5159,5163,438,5075,5113,5139,5146,5086,5088,47,48,49,30,31,29,32])).
% 60.90/60.92 cnf(5165,plain,
% 60.90/60.92 (E(x51651,f2(x51651,x51651,x51652,x51652))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5166,plain,
% 60.90/60.92 (P2(a12,f2(a1,a1,x51661,x51661),a1,a11)),
% 60.90/60.92 inference(scs_inference,[],[59,371,5072,5159,5163,5165,438,5075,5113,5139,5146,5086,5088,47,48,49,30,31,29,32,33])).
% 60.90/60.92 cnf(5167,plain,
% 60.90/60.92 (E(x51671,f2(x51671,x51671,x51672,x51672))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5169,plain,
% 60.90/60.92 (P2(a10,f2(a11,a11,x51691,x51691),a10,f2(a12,a12,x51692,x51692))),
% 60.90/60.92 inference(rename_variables,[],[5135])).
% 60.90/60.92 cnf(5171,plain,
% 60.90/60.92 (P2(a10,f2(a11,a11,x51711,x51711),f2(a10,a10,x51712,x51712),f2(a12,a12,x51713,x51713))),
% 60.90/60.92 inference(scs_inference,[],[59,371,517,5072,5159,5163,5165,5167,438,5075,5113,5139,5135,5169,5146,5086,5088,47,48,49,30,31,29,32,33,35,34])).
% 60.90/60.92 cnf(5173,plain,
% 60.90/60.92 (~E(a11,f2(x51731,a1,x51732,f2(x51732,x51732,x51733,x51733)))),
% 60.90/60.92 inference(scs_inference,[],[59,371,517,5072,5159,5163,5165,5167,438,5075,5113,5139,5135,5169,5146,5086,5088,47,48,49,30,31,29,32,33,35,34,165])).
% 60.90/60.92 cnf(5187,plain,
% 60.90/60.92 (P1(a1,f2(a10,a10,x51871,x51871),f2(a11,a11,x51872,x51872))),
% 60.90/60.92 inference(rename_variables,[],[5158])).
% 60.90/60.92 cnf(5188,plain,
% 60.90/60.92 (E(f2(x51881,x51882,x51883,x51884),f2(f2(x51885,x51881,x51886,x51886),x51882,x51883,x51884))),
% 60.90/60.92 inference(rename_variables,[],[517])).
% 60.90/60.92 cnf(5189,plain,
% 60.90/60.92 (~E(f2(a12,f2(a11,a11,x51891,x51891),x51892,x51893),a12)),
% 60.90/60.92 inference(scs_inference,[],[59,371,517,5076,5114,5158,5173,47,48,49,30,31])).
% 60.90/60.92 cnf(5191,plain,
% 60.90/60.92 (P1(f2(a1,a1,x51911,x51911),f2(a10,a10,x51912,x51912),f2(a11,a11,x51913,x51913))),
% 60.90/60.92 inference(scs_inference,[],[59,371,517,5072,5076,5114,5158,5187,5173,47,48,49,30,31,29])).
% 60.90/60.92 cnf(5192,plain,
% 60.90/60.92 (E(x51921,f2(x51921,x51921,x51922,x51922))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5193,plain,
% 60.90/60.92 (P2(f2(a10,a10,x51931,x51931),a12,a11,a10)),
% 60.90/60.92 inference(scs_inference,[],[59,371,517,5072,5192,260,5076,5114,5158,5187,5173,47,48,49,30,31,29,32])).
% 60.90/60.92 cnf(5194,plain,
% 60.90/60.92 (E(x51941,f2(x51941,x51941,x51942,x51942))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5195,plain,
% 60.90/60.92 (P2(a10,f2(a12,a12,x51951,x51951),a11,a10)),
% 60.90/60.92 inference(scs_inference,[],[59,371,517,5072,5192,5194,260,5076,5114,5158,5187,5173,47,48,49,30,31,29,32,33])).
% 60.90/60.92 cnf(5198,plain,
% 60.90/60.92 (P2(a10,f2(a11,a11,x51981,x51981),f2(a10,a10,x51982,x51982),f2(a12,a12,x51983,x51983))),
% 60.90/60.92 inference(rename_variables,[],[5171])).
% 60.90/60.92 cnf(5199,plain,
% 60.90/60.92 (E(f2(x51991,x51992,x51993,x51994),f2(f2(x51995,x51991,x51996,x51996),x51992,x51993,x51994))),
% 60.90/60.92 inference(rename_variables,[],[517])).
% 60.90/60.92 cnf(5203,plain,
% 60.90/60.92 (~E(a1,f2(x52031,a11,x52032,f2(x52032,x52032,x52033,x52033)))),
% 60.90/60.92 inference(scs_inference,[],[59,371,517,5188,5199,5072,5192,5194,260,5076,5114,5171,5198,5158,5187,5173,47,48,49,30,31,29,32,33,35,34,90])).
% 60.90/60.92 cnf(5217,plain,
% 60.90/60.92 (P1(f2(a1,a1,x52171,x52171),f2(a10,a10,x52172,x52172),f2(a11,a11,x52173,x52173))),
% 60.90/60.92 inference(rename_variables,[],[5191])).
% 60.90/60.92 cnf(5218,plain,
% 60.90/60.92 (E(f2(x52181,x52182,x52183,x52184),f2(f2(x52185,x52181,x52186,x52186),x52182,x52183,x52184))),
% 60.90/60.92 inference(rename_variables,[],[517])).
% 60.90/60.92 cnf(5220,plain,
% 60.90/60.92 (P1(f2(a1,a1,x52201,x52201),f2(a10,a10,x52202,x52202),f2(a11,a11,x52203,x52203))),
% 60.90/60.92 inference(rename_variables,[],[5191])).
% 60.90/60.92 cnf(5221,plain,
% 60.90/60.92 (E(f2(x52211,x52212,x52213,x52214),f2(f2(x52215,x52211,x52216,x52216),x52212,x52213,x52214))),
% 60.90/60.92 inference(rename_variables,[],[517])).
% 60.90/60.92 cnf(5224,plain,
% 60.90/60.92 (E(f2(x52241,x52242,x52243,x52244),f2(f2(x52245,x52241,x52246,x52246),x52242,x52243,x52244))),
% 60.90/60.92 inference(rename_variables,[],[517])).
% 60.90/60.92 cnf(5225,plain,
% 60.90/60.92 (P2(f2(a10,a10,x52251,x52251),a12,a10,a11)),
% 60.90/60.92 inference(scs_inference,[],[371,517,5218,5221,5072,294,5077,5191,5217,5220,5203,47,48,49,30,31,29,32])).
% 60.90/60.92 cnf(5226,plain,
% 60.90/60.92 (E(x52261,f2(x52261,x52261,x52262,x52262))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5227,plain,
% 60.90/60.92 (P2(a10,f2(a12,a12,x52271,x52271),a10,a11)),
% 60.90/60.92 inference(scs_inference,[],[371,517,5218,5221,5072,5226,294,5077,5191,5217,5220,5203,47,48,49,30,31,29,32,33])).
% 60.90/60.92 cnf(5228,plain,
% 60.90/60.92 (E(x52281,f2(x52281,x52281,x52282,x52282))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5234,plain,
% 60.90/60.92 (~E(a1,f2(x52341,a11,f2(x52342,x52342,x52343,x52343),x52342))),
% 60.90/60.92 inference(scs_inference,[],[371,517,5218,5221,5224,5072,5226,5228,294,5077,5191,5217,5220,5203,5137,5133,47,48,49,30,31,29,32,33,35,34,90])).
% 60.90/60.92 cnf(5244,plain,
% 60.90/60.92 (P1(f2(a1,a1,x52441,x52441),f2(a10,a10,x52442,x52442),a11)),
% 60.90/60.92 inference(rename_variables,[],[5162])).
% 60.90/60.92 cnf(5245,plain,
% 60.90/60.92 (E(f2(x52451,x52452,x52453,x52454),f2(f2(x52455,x52451,x52456,x52456),x52452,x52453,x52454))),
% 60.90/60.92 inference(rename_variables,[],[517])).
% 60.90/60.92 cnf(5248,plain,
% 60.90/60.92 (E(f2(x52481,x52482,x52483,x52484),f2(f2(x52485,x52481,x52486,x52486),x52482,x52483,x52484))),
% 60.90/60.92 inference(rename_variables,[],[517])).
% 60.90/60.92 cnf(5252,plain,
% 60.90/60.92 (P2(f2(a1,a1,x52521,x52521),a12,a11,a1)),
% 60.90/60.92 inference(scs_inference,[],[517,5245,5248,5072,280,5162,5244,5234,5158,47,48,30,31,29,32])).
% 60.90/60.92 cnf(5253,plain,
% 60.90/60.92 (E(x52531,f2(x52531,x52531,x52532,x52532))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5254,plain,
% 60.90/60.92 (P2(a1,f2(a12,a12,x52541,x52541),a11,a1)),
% 60.90/60.92 inference(scs_inference,[],[517,5245,5248,5072,5253,280,5162,5244,5234,5158,47,48,30,31,29,32,33])).
% 60.90/60.92 cnf(5269,plain,
% 60.90/60.92 (E(f2(x52691,x52692,x52693,x52694),f2(f2(x52695,x52691,x52696,x52696),x52692,x52693,x52694))),
% 60.90/60.92 inference(rename_variables,[],[517])).
% 60.90/60.92 cnf(5273,plain,
% 60.90/60.92 (P2(f2(a1,a1,x52731,x52731),a12,a1,a11)),
% 60.90/60.92 inference(scs_inference,[],[517,5269,5072,333,5160,5086,5088,48,31,30,32])).
% 60.90/60.92 cnf(5274,plain,
% 60.90/60.92 (E(x52741,f2(x52741,x52741,x52742,x52742))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5275,plain,
% 60.90/60.92 (P2(a1,f2(a12,a12,x52751,x52751),a1,a11)),
% 60.90/60.92 inference(scs_inference,[],[517,5269,5072,5274,333,5160,5086,5088,48,31,30,32,33])).
% 60.90/60.92 cnf(5290,plain,
% 60.90/60.92 (E(x52901,f2(x52901,x52901,x52902,x52902))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5291,plain,
% 60.90/60.92 (P2(a12,f2(a1,a1,x52911,x52911),f2(a1,a1,x52912,x52912),a11)),
% 60.90/60.92 inference(scs_inference,[],[5072,5290,392,5189,5166,48,33,34])).
% 60.90/60.92 cnf(5292,plain,
% 60.90/60.92 (E(x52921,f2(x52921,x52921,x52922,x52922))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5293,plain,
% 60.90/60.92 (P2(a12,f2(a1,a1,x52931,x52931),a1,f2(a11,a11,x52932,x52932))),
% 60.90/60.92 inference(scs_inference,[],[5072,5290,5292,392,5189,5166,48,33,34,35])).
% 60.90/60.92 cnf(5304,plain,
% 60.90/60.92 (E(x53041,f2(x53041,x53041,x53042,x53042))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5305,plain,
% 60.90/60.92 (P2(a12,f2(a1,a1,x53051,x53051),f2(a1,a1,x53052,x53052),f2(a11,a11,x53053,x53053))),
% 60.90/60.92 inference(scs_inference,[],[5072,5304,381,5291,5146,48,33,35])).
% 60.90/60.92 cnf(5307,plain,
% 60.90/60.92 (~E(f2(f2(a10,a10,x53071,x53071),a1,x53072,x53073),a10)),
% 60.90/60.92 inference(scs_inference,[],[559,5072,5304,381,5113,5291,5146,48,33,35,31])).
% 60.90/60.92 cnf(5324,plain,
% 60.90/60.92 (P2(a12,f2(a1,a1,x53241,x53241),f2(a1,a1,x53242,x53242),f2(a11,a11,x53243,x53243))),
% 60.90/60.92 inference(rename_variables,[],[5305])).
% 60.90/60.92 cnf(5325,plain,
% 60.90/60.92 (E(f2(x53251,x53252,x53253,x53254),f2(f2(x53255,x53251,x53256,x53256),x53252,x53253,x53254))),
% 60.90/60.92 inference(rename_variables,[],[517])).
% 60.90/60.92 cnf(5331,plain,
% 60.90/60.92 (~P2(x53311,x53311,a12,a11)),
% 60.90/60.92 inference(scs_inference,[],[61,559,517,5325,39,5305,5324,5307,5114,48,34,31,35,49])).
% 60.90/60.92 cnf(5334,plain,
% 60.90/60.92 (~E(f2(x53341,a12,x53342,f2(x53342,x53342,x53343,x53343)),a11)),
% 60.90/60.92 inference(scs_inference,[],[61,559,517,5325,39,5116,5305,5324,5307,5114,48,34,31,35,49,33])).
% 60.90/60.92 cnf(5336,plain,
% 60.90/60.92 (~E(f2(x53361,a11,f2(x53362,x53362,x53363,x53363),x53362),a12)),
% 60.90/60.92 inference(scs_inference,[],[61,559,517,5325,39,5112,5116,5305,5324,5307,5114,48,34,31,35,49,33,32])).
% 60.90/60.92 cnf(5352,plain,
% 60.90/60.92 (P2(a10,f2(a12,a12,x53521,x53521),f2(a11,a11,x53522,x53522),a10)),
% 60.90/60.92 inference(scs_inference,[],[61,517,5072,41,5117,5334,5293,5195,48,49,35,33,34])).
% 60.90/60.92 cnf(5354,plain,
% 60.90/60.92 (~E(f2(x53541,a11,x53542,f2(x53542,x53542,x53543,x53543)),a12)),
% 60.90/60.92 inference(scs_inference,[],[61,517,5072,41,5115,5117,5334,5293,5195,48,49,35,33,34,32])).
% 60.90/60.92 cnf(5368,plain,
% 60.90/60.92 (P2(a10,f2(a12,a12,x53681,x53681),f2(f2(x53682,a11,x53683,x53683),a11,x53684,x53684),a10)),
% 60.90/60.92 inference(scs_inference,[],[61,517,5072,518,5336,5352,48,49,35,34])).
% 60.90/60.92 cnf(5369,plain,
% 60.90/60.92 (P2(a10,f2(a12,a12,x53691,x53691),f2(a11,a11,x53692,x53692),a10)),
% 60.90/60.92 inference(rename_variables,[],[5352])).
% 60.90/60.92 cnf(5370,plain,
% 60.90/60.92 (E(f2(x53701,x53702,x53703,x53704),f2(f2(x53705,x53701,x53706,x53706),x53702,x53703,x53704))),
% 60.90/60.92 inference(rename_variables,[],[517])).
% 60.90/60.92 cnf(5371,plain,
% 60.90/60.92 (P2(a10,f2(f2(x53711,a12,x53712,x53712),a12,x53713,x53713),f2(a11,a11,x53714,x53714),a10)),
% 60.90/60.92 inference(scs_inference,[],[61,517,5370,5072,518,5336,5352,5369,48,49,35,34,33])).
% 60.90/60.92 cnf(5403,plain,
% 60.90/60.92 (~E(f2(a12,f2(x54031,a11,x54032,x54032),x54033,x54034),a12)),
% 60.90/60.92 inference(scs_inference,[],[393,5126,5354,48,31])).
% 60.90/60.92 cnf(5411,plain,
% 60.90/60.92 (E(x54111,f2(x54111,x54111,x54112,x54112))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5412,plain,
% 60.90/60.92 (P2(a10,f2(a12,a12,x54121,x54121),f2(a10,a10,x54122,x54122),a11)),
% 60.90/60.92 inference(scs_inference,[],[61,393,5072,5411,5126,5354,5227,5074,48,31,49,35,34])).
% 60.90/60.92 cnf(5413,plain,
% 60.90/60.92 (E(x54131,f2(x54131,x54131,x54132,x54132))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5414,plain,
% 60.90/60.92 (P2(f2(a10,a10,x54141,x54141),f2(a11,a11,x54142,x54142),a10,a12)),
% 60.90/60.92 inference(scs_inference,[],[61,393,5072,5411,5413,5126,5354,5095,5227,5074,48,31,49,35,34,33])).
% 60.90/60.92 cnf(5424,plain,
% 60.90/60.92 (~E(f2(a9,f2(a6,a8,x54241,x54242),x54243,x54244),a9)),
% 60.90/60.92 inference(scs_inference,[],[176,5403,5073,48,31])).
% 60.90/60.92 cnf(5476,plain,
% 60.90/60.92 (P2(f2(a10,a10,x54761,x54761),f2(a11,a11,x54762,x54762),a10,f2(a12,a12,x54763,x54763))),
% 60.90/60.92 inference(scs_inference,[],[61,517,5072,5424,5412,5414,5077,48,49,34,35])).
% 60.90/60.92 cnf(5488,plain,
% 60.90/60.92 (P2(f2(a10,a10,x54881,x54881),f2(a11,a11,x54882,x54882),a10,f2(a12,a12,x54883,x54883))),
% 60.90/60.92 inference(rename_variables,[],[5476])).
% 60.90/60.92 cnf(5490,plain,
% 60.90/60.92 (P2(f2(a10,a10,x54901,x54901),f2(a11,a11,x54902,x54902),f2(a10,a10,x54903,x54903),f2(a12,a12,x54904,x54904))),
% 60.90/60.92 inference(scs_inference,[],[517,5072,5476,5488,35,34])).
% 60.90/60.92 cnf(5571,plain,
% 60.90/60.92 (P2(f2(a10,a10,x55711,x55711),f2(a11,a11,x55712,x55712),f2(a10,a10,x55713,x55713),a12)),
% 60.90/60.92 inference(scs_inference,[],[5072,5414,34])).
% 60.90/60.92 cnf(5572,plain,
% 60.90/60.92 (E(x55721,f2(x55721,x55721,x55722,x55722))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5573,plain,
% 60.90/60.92 (P2(f2(a12,a12,x55731,x55731),f2(a1,a1,x55732,x55732),a1,a11)),
% 60.90/60.92 inference(scs_inference,[],[5072,5572,5164,5414,34,33])).
% 60.90/60.92 cnf(5600,plain,
% 60.90/60.92 (E(x56001,f2(x56001,x56001,x56002,x56002))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5601,plain,
% 60.90/60.92 (P2(f2(a12,a12,x56011,x56011),f2(f2(x56012,a1,x56013,x56013),a1,x56014,x56014),a1,a11)),
% 60.90/60.92 inference(scs_inference,[],[517,5072,5573,34,33])).
% 60.90/60.92 cnf(5605,plain,
% 60.90/60.92 (E(x56051,f2(x56051,x56051,x56052,x56052))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5606,plain,
% 60.90/60.92 (P2(f2(a12,a12,x56061,x56061),f2(a1,a1,x56062,x56062),f2(a1,a1,x56063,x56063),f2(a11,a11,x56064,x56064))),
% 60.90/60.92 inference(scs_inference,[],[517,5072,5600,5605,5371,5573,34,33,32,35])).
% 60.90/60.92 cnf(5628,plain,
% 60.90/60.92 (E(x56281,f2(x56281,x56281,x56282,x56282))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5629,plain,
% 60.90/60.92 (P2(f2(a10,a10,x56291,x56291),f2(a12,a12,x56292,x56292),a11,a10)),
% 60.90/60.92 inference(scs_inference,[],[5072,5628,5193,5601,34,33])).
% 60.90/60.92 cnf(5667,plain,
% 60.90/60.92 (E(x56671,f2(x56671,x56671,x56672,x56672))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5668,plain,
% 60.90/60.92 (P2(f2(a10,a10,x56681,x56681),f2(a12,a12,x56682,x56682),a10,a11)),
% 60.90/60.92 inference(scs_inference,[],[5072,5667,5225,5629,34,33])).
% 60.90/60.92 cnf(5669,plain,
% 60.90/60.92 (E(x56691,f2(x56691,x56691,x56692,x56692))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5671,plain,
% 60.90/60.92 (E(x56711,f2(x56711,x56711,x56712,x56712))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5672,plain,
% 60.90/60.92 (P2(f2(a10,a10,x56721,x56721),f2(a12,a12,x56722,x56722),a10,f2(a11,a11,x56723,x56723))),
% 60.90/60.92 inference(scs_inference,[],[5072,5667,5669,5671,5368,5225,5629,34,33,32,35])).
% 60.90/60.92 cnf(5679,plain,
% 60.90/60.92 (P2(f2(a10,a10,x56791,x56791),f2(a12,a12,x56792,x56792),a10,f2(a11,a11,x56793,x56793))),
% 60.90/60.92 inference(rename_variables,[],[5672])).
% 60.90/60.92 cnf(5681,plain,
% 60.90/60.92 (P2(f2(a10,a10,x56811,x56811),f2(a12,a12,x56812,x56812),f2(a10,a10,x56813,x56813),f2(a11,a11,x56814,x56814))),
% 60.90/60.92 inference(scs_inference,[],[517,5072,5672,5679,35,34])).
% 60.90/60.92 cnf(5693,plain,
% 60.90/60.92 (P2(f2(a10,a10,x56931,x56931),f2(a12,a12,x56932,x56932),f2(a10,a10,x56933,x56933),a11)),
% 60.90/60.92 inference(scs_inference,[],[5072,5668,34])).
% 60.90/60.92 cnf(5694,plain,
% 60.90/60.92 (E(x56941,f2(x56941,x56941,x56942,x56942))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5695,plain,
% 60.90/60.92 (P2(f2(a1,a1,x56951,x56951),f2(a12,a12,x56952,x56952),a11,a1)),
% 60.90/60.92 inference(scs_inference,[],[5072,5694,5252,5668,34,33])).
% 60.90/60.92 cnf(5696,plain,
% 60.90/60.92 (E(x56961,f2(x56961,x56961,x56962,x56962))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5700,plain,
% 60.90/60.92 (P2(f2(a1,a1,x57001,x57001),f2(a12,a12,x57002,x57002),a11,f2(a1,a1,x57003,x57003))),
% 60.90/60.92 inference(scs_inference,[],[517,5072,5694,5696,5681,5252,5668,34,33,32,35])).
% 60.90/60.92 cnf(5706,plain,
% 60.90/60.92 (P2(f2(a1,a1,x57061,x57061),f2(a12,a12,x57062,x57062),a11,f2(f2(x57063,a1,x57064,x57064),a1,x57065,x57065))),
% 60.90/60.92 inference(scs_inference,[],[517,5700,35])).
% 60.90/60.92 cnf(5707,plain,
% 60.90/60.92 (P2(f2(a1,a1,x57071,x57071),f2(a12,a12,x57072,x57072),a11,f2(a1,a1,x57073,x57073))),
% 60.90/60.92 inference(rename_variables,[],[5700])).
% 60.90/60.92 cnf(5708,plain,
% 60.90/60.92 (E(f2(x57081,x57082,x57083,x57084),f2(f2(x57085,x57081,x57086,x57086),x57082,x57083,x57084))),
% 60.90/60.92 inference(rename_variables,[],[517])).
% 60.90/60.92 cnf(5711,plain,
% 60.90/60.92 (E(f2(x57111,x57112,x57113,x57114),f2(f2(x57115,x57111,x57116,x57116),x57112,x57113,x57114))),
% 60.90/60.92 inference(rename_variables,[],[517])).
% 60.90/60.92 cnf(5712,plain,
% 60.90/60.92 (P2(f2(a1,a1,x57121,x57121),f2(f2(x57122,a12,x57123,x57123),a12,x57124,x57124),a11,f2(a1,a1,x57125,x57125))),
% 60.90/60.92 inference(scs_inference,[],[517,5708,5711,5693,5700,5707,35,34,33])).
% 60.90/60.92 cnf(5723,plain,
% 60.90/60.92 (E(x57231,f2(x57231,x57231,x57232,x57232))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5725,plain,
% 60.90/60.92 (P2(f2(a1,a1,x57251,x57251),f2(a12,a12,x57252,x57252),a11,a1)),
% 60.90/60.92 inference(rename_variables,[],[5695])).
% 60.90/60.92 cnf(5726,plain,
% 60.90/60.92 (E(f2(x57261,x57262,x57263,x57264),f2(f2(x57265,x57261,x57266,x57266),x57262,x57263,x57264))),
% 60.90/60.92 inference(rename_variables,[],[517])).
% 60.90/60.92 cnf(5730,plain,
% 60.90/60.92 (P2(f2(f2(x57301,a1,x57302,x57302),a1,x57303,x57303),f2(a12,a12,x57304,x57304),a11,f2(a1,a1,x57305,x57305))),
% 60.90/60.92 inference(scs_inference,[],[517,5726,5072,5723,5712,5695,5725,34,33,32,35])).
% 60.90/60.92 cnf(5740,plain,
% 60.90/60.92 (E(f2(x57401,x57402,x57403,x57404),f2(f2(x57405,x57401,x57406,x57406),x57402,x57403,x57404))),
% 60.90/60.92 inference(rename_variables,[],[517])).
% 60.90/60.92 cnf(5741,plain,
% 60.90/60.92 (P2(f2(f2(x57411,a1,x57412,x57412),a1,x57413,x57413),a12,a1,a11)),
% 60.90/60.92 inference(scs_inference,[],[517,5740,5072,5730,5254,5273,34,33,32])).
% 60.90/60.92 cnf(5749,plain,
% 60.90/60.92 (E(x57491,f2(x57491,x57491,x57492,x57492))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5751,plain,
% 60.90/60.92 (E(x57511,f2(x57511,x57511,x57512,x57512))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(5752,plain,
% 60.90/60.92 (P2(f2(a1,a1,x57521,x57521),f2(a12,a12,x57522,x57522),a1,a11)),
% 60.90/60.92 inference(scs_inference,[],[5072,5749,5751,5706,5741,5275,34,33,32])).
% 60.90/60.92 cnf(5760,plain,
% 60.90/60.92 (P2(f2(a1,a1,x57601,x57601),f2(a12,a12,x57602,x57602),a1,f2(a11,a11,x57603,x57603))),
% 60.90/60.92 inference(scs_inference,[],[5072,5752,35])).
% 60.90/60.92 cnf(5774,plain,
% 60.90/60.92 (P2(f2(a1,a1,x57741,x57741),f2(a12,a12,x57742,x57742),a1,f2(a11,a11,x57743,x57743))),
% 60.90/60.92 inference(rename_variables,[],[5760])).
% 60.90/60.92 cnf(5776,plain,
% 60.90/60.92 (P2(f2(a1,a1,x57761,x57761),f2(a12,a12,x57762,x57762),f2(a1,a1,x57763,x57763),f2(a11,a11,x57764,x57764))),
% 60.90/60.92 inference(scs_inference,[],[517,5072,5760,5774,35,34])).
% 60.90/60.92 cnf(6194,plain,
% 60.90/60.92 (E(x61941,f2(x61941,x61941,x61942,x61942))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(6196,plain,
% 60.90/60.92 (E(x61961,f2(x61961,x61961,x61962,x61962))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(6198,plain,
% 60.90/60.92 (E(x61981,f2(x61981,x61981,x61982,x61982))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(6200,plain,
% 60.90/60.92 (E(x62001,f2(x62001,x62001,x62002,x62002))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(6202,plain,
% 60.90/60.92 (E(x62021,f2(x62021,x62021,x62022,x62022))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(6204,plain,
% 60.90/60.92 (E(x62041,f2(x62041,x62041,x62042,x62042))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(6206,plain,
% 60.90/60.92 (E(x62061,f2(x62061,x62061,x62062,x62062))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(6208,plain,
% 60.90/60.92 (E(x62081,f2(x62081,x62081,x62082,x62082))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(6210,plain,
% 60.90/60.92 (E(x62101,f2(x62101,x62101,x62102,x62102))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(6212,plain,
% 60.90/60.92 (E(x62121,f2(x62121,x62121,x62122,x62122))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(6214,plain,
% 60.90/60.92 (E(x62141,f2(x62141,x62141,x62142,x62142))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(6216,plain,
% 60.90/60.92 (E(x62161,f2(x62161,x62161,x62162,x62162))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(6217,plain,
% 60.90/60.92 (~E(a1,a10)),
% 60.90/60.92 inference(scs_inference,[],[598,5072,6194,6196,6198,6200,6202,6204,6206,6208,6210,6212,6214,108,109,408,422,443,453,285,303,340,341,91,89,73])).
% 60.90/60.92 cnf(6220,plain,
% 60.90/60.92 (E(x62201,f2(x62201,x62201,x62202,x62202))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(6221,plain,
% 60.90/60.92 (~E(a6,f2(a8,a9,x62211,x62212))),
% 60.90/60.92 inference(scs_inference,[],[598,4058,5072,6194,6196,6198,6200,6202,6204,6206,6208,6210,6212,6214,6216,108,109,408,422,443,453,285,303,340,341,91,89,73,88,2])).
% 60.90/60.92 cnf(6223,plain,
% 60.90/60.92 (E(x62231,f2(x62231,x62231,x62232,x62232))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(6225,plain,
% 60.90/60.92 (E(x62251,f2(x62251,x62251,x62252,x62252))),
% 60.90/60.92 inference(rename_variables,[],[5072])).
% 60.90/60.92 cnf(6226,plain,
% 60.90/60.92 (E(x62261,f2(x62262,x62261,x62263,x62263))),
% 60.90/60.92 inference(scs_inference,[],[598,4058,5072,6194,6196,6198,6200,6202,6204,6206,6208,6210,6212,6214,6216,6220,6223,41,108,109,408,422,443,453,285,303,340,341,91,89,73,88,2,90,165,48])).
% 60.90/60.92 cnf(6231,plain,
% 60.90/60.92 (~E(f2(a1,a1,x62311,x62311),f2(x62312,a11,x62313,x62313))),
% 60.90/60.92 inference(scs_inference,[],[598,4058,1591,36,5072,6194,6196,6198,6200,6202,6204,6206,6208,6210,6212,6214,6216,6220,6223,6225,41,108,109,408,422,443,453,285,303,340,341,91,89,73,88,2,90,165,48,52,3])).
% 60.90/60.92 cnf(6234,plain,
% 60.90/60.92 (E(f2(x62341,x62341,x62342,x62342),x62341)),
% 60.90/60.92 inference(rename_variables,[],[5084])).
% 60.90/60.92 cnf(6235,plain,
% 60.90/60.92 (~P1(f2(a11,a11,x62351,x62351),a1,a11)),
% 60.90/60.92 inference(scs_inference,[],[382,598,4058,1591,228,5084,6234,36,5072,6194,6196,6198,6200,6202,6204,6206,6208,6210,6212,6214,6216,6220,6223,6225,41,108,109,408,422,443,453,285,303,340,341,91,89,73,88,2,90,165,48,52,3,30,29])).
% 60.90/60.92 cnf(6236,plain,
% 60.90/60.92 (E(f2(x62361,x62361,x62362,x62362),x62361)),
% 60.90/60.92 inference(rename_variables,[],[5084])).
% 60.90/60.92 cnf(6238,plain,
% 60.90/60.92 (E(f2(x62381,x62381,x62382,x62382),x62381)),
% 60.90/60.92 inference(rename_variables,[],[5084])).
% 60.90/60.92 cnf(6239,plain,
% 60.90/60.92 (~P2(f2(a10,a10,x62391,x62391),f2(a11,a11,x62392,x62392),x62393,x62393)),
% 60.90/60.92 inference(scs_inference,[],[382,598,416,4058,1591,5571,228,5084,6234,6236,36,5072,6194,6196,6198,6200,6202,6204,6206,6208,6210,6212,6214,6216,6220,6223,6225,41,108,109,408,422,443,453,285,303,340,341,91,89,73,88,2,90,165,48,52,3,30,29,31,49])).
% 60.90/60.92 cnf(6243,plain,
% 60.90/60.92 (~P2(a11,a1,x62431,f2(x62431,x62431,x62432,x62432))),
% 60.90/60.92 inference(scs_inference,[],[382,384,598,416,4058,1591,5571,228,5084,6234,6236,6238,36,5072,6194,6196,6198,6200,6202,6204,6206,6208,6210,6212,6214,6216,6220,6223,6225,41,108,109,408,422,443,453,285,303,340,341,91,89,73,88,2,90,165,48,52,3,30,29,31,49,35])).
% 60.90/60.92 cnf(6244,plain,
% 60.90/60.92 (E(f2(x62441,x62441,x62442,x62442),x62441)),
% 60.90/60.92 inference(rename_variables,[],[5084])).
% 60.90/60.92 cnf(6245,plain,
% 60.90/60.92 (~P2(a11,a1,f2(x62451,x62451,x62452,x62452),x62451)),
% 60.90/60.92 inference(scs_inference,[],[382,384,598,416,4058,1591,5571,228,5084,6234,6236,6238,6244,36,5072,6194,6196,6198,6200,6202,6204,6206,6208,6210,6212,6214,6216,6220,6223,6225,41,108,109,408,422,443,453,285,303,340,341,91,89,73,88,2,90,165,48,52,3,30,29,31,49,35,34])).
% 60.90/60.92 cnf(6247,plain,
% 60.90/60.92 (P1(a1,a11,f3(a1,a1,a10,a11,a11))),
% 60.90/60.92 inference(scs_inference,[],[382,384,598,416,4058,1591,5571,228,5084,6234,6236,6238,6244,36,5072,6194,6196,6198,6200,6202,6204,6206,6208,6210,6212,6214,6216,6220,6223,6225,41,108,109,408,422,443,453,285,303,340,341,91,89,73,88,2,90,165,48,52,3,30,29,31,49,35,34,54])).
% 60.90/60.92 cnf(6249,plain,
% 60.90/60.92 (P1(a1,a1,f4(a1,a1,a10,a11,a11))),
% 60.90/60.92 inference(scs_inference,[],[382,384,598,416,4058,1591,5571,228,5084,6234,6236,6238,6244,36,5072,6194,6196,6198,6200,6202,6204,6206,6208,6210,6212,6214,6216,6220,6223,6225,41,108,109,408,422,443,453,285,303,340,341,91,89,73,88,2,90,165,48,52,3,30,29,31,49,35,34,54,55])).
% 60.90/60.92 cnf(6256,plain,
% 60.90/60.92 (P2(a12,f2(x62561,a10,x62562,x62562),a11,a10)),
% 60.90/60.92 inference(scs_inference,[],[382,384,598,416,4058,1591,5571,228,5084,6234,6236,6238,6244,36,5072,6194,6196,6198,6200,6202,6204,6206,6208,6210,6212,6214,6216,6220,6223,6225,41,108,109,408,422,443,453,285,303,340,341,91,89,73,88,2,90,165,48,52,3,30,29,31,49,35,34,54,55,56,87,216,375,376])).
% 60.90/60.92 cnf(6267,plain,
% 60.90/60.92 (E(x62671,f2(x62672,x62671,x62673,x62673))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6269,plain,
% 60.90/60.92 (E(x62691,f2(x62692,x62691,x62693,x62693))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6270,plain,
% 60.90/60.92 (P2(a10,f2(x62701,a12,x62702,x62702),a11,a10)),
% 60.90/60.92 inference(scs_inference,[],[6226,6267,6269,186,144,361])).
% 60.90/60.92 cnf(6271,plain,
% 60.90/60.92 (E(x62711,f2(x62712,x62711,x62713,x62713))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6272,plain,
% 60.90/60.92 (P2(f2(x62721,a1,x62722,x62722),a12,a11,a1)),
% 60.90/60.92 inference(scs_inference,[],[6226,6267,6269,6271,186,144,361,397])).
% 60.90/60.92 cnf(6273,plain,
% 60.90/60.92 (E(x62731,f2(x62732,x62731,x62733,x62733))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6274,plain,
% 60.90/60.92 (P2(a12,f2(x62741,a1,x62742,x62742),a11,a1)),
% 60.90/60.92 inference(scs_inference,[],[6226,6267,6269,6271,6273,186,144,361,397,398])).
% 60.90/60.92 cnf(6275,plain,
% 60.90/60.92 (E(x62751,f2(x62752,x62751,x62753,x62753))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6277,plain,
% 60.90/60.92 (P2(f2(x62771,a1,x62772,x62772),a12,a1,a11)),
% 60.90/60.92 inference(scs_inference,[],[6226,6267,6269,6271,6273,6275,186,144,361,397,398,432])).
% 60.90/60.92 cnf(6278,plain,
% 60.90/60.92 (E(x62781,f2(x62782,x62781,x62783,x62783))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6279,plain,
% 60.90/60.92 (P2(a12,f2(x62791,a1,x62792,x62792),a1,a11)),
% 60.90/60.92 inference(scs_inference,[],[6226,6267,6269,6271,6273,6275,6278,186,144,361,397,398,432,433])).
% 60.90/60.92 cnf(6280,plain,
% 60.90/60.92 (E(x62801,f2(x62802,x62801,x62803,x62803))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6283,plain,
% 60.90/60.92 (E(x62831,f2(x62832,x62831,x62833,x62833))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6285,plain,
% 60.90/60.92 (E(x62851,f2(x62852,x62851,x62853,x62853))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6288,plain,
% 60.90/60.92 (E(x62881,f2(x62882,x62881,x62883,x62883))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6290,plain,
% 60.90/60.92 (E(x62901,f2(x62902,x62901,x62903,x62903))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6293,plain,
% 60.90/60.92 (E(x62931,f2(x62932,x62931,x62933,x62933))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6295,plain,
% 60.90/60.92 (E(x62951,f2(x62952,x62951,x62953,x62953))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6298,plain,
% 60.90/60.92 (E(x62981,f2(x62982,x62981,x62983,x62983))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6300,plain,
% 60.90/60.92 (E(x63001,f2(x63002,x63001,x63003,x63003))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6302,plain,
% 60.90/60.92 (E(x63021,f2(x63022,x63021,x63023,x63023))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6304,plain,
% 60.90/60.92 (E(x63041,f2(x63042,x63041,x63043,x63043))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6306,plain,
% 60.90/60.92 (E(x63061,f2(x63062,x63061,x63063,x63063))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6308,plain,
% 60.90/60.92 (E(x63081,f2(x63082,x63081,x63083,x63083))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6310,plain,
% 60.90/60.92 (E(x63101,f2(x63102,x63101,x63103,x63103))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6312,plain,
% 60.90/60.92 (E(x63121,f2(x63122,x63121,x63123,x63123))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6314,plain,
% 60.90/60.92 (E(x63141,f2(x63142,x63141,x63143,x63143))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6316,plain,
% 60.90/60.92 (E(x63161,f2(x63162,x63161,x63163,x63163))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6317,plain,
% 60.90/60.92 (~E(f2(a11,a11,x63171,x63171),f2(a10,a10,x63172,x63172))),
% 60.90/60.92 inference(scs_inference,[],[6226,6267,6269,6271,6273,6275,6278,6280,6283,6285,6288,6290,6293,6295,6298,6300,6302,6304,6306,6308,6310,6312,6314,6239,186,144,361,397,398,432,433,463,464,474,475,485,486,496,303,108,422,443,89,285,453,408,340,73])).
% 60.90/60.92 cnf(6320,plain,
% 60.90/60.92 (E(x63201,f2(x63202,x63201,x63203,x63203))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6322,plain,
% 60.90/60.92 (E(x63221,f2(x63222,x63221,x63223,x63223))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6324,plain,
% 60.90/60.92 (E(x63241,f2(x63242,x63241,x63243,x63243))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6327,plain,
% 60.90/60.92 (E(x63271,f2(x63272,x63271,x63273,x63273))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6329,plain,
% 60.90/60.92 (E(x63291,f2(x63292,x63291,x63293,x63293))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6331,plain,
% 60.90/60.92 (E(x63311,f2(x63312,x63311,x63313,x63313))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6332,plain,
% 60.90/60.92 (E(f2(x63321,x63322,x63323,x63323),x63322)),
% 60.90/60.92 inference(scs_inference,[],[6226,6267,6269,6271,6273,6275,6278,6280,6283,6285,6288,6290,6293,6295,6298,6300,6302,6304,6306,6308,6310,6312,6314,6316,6320,6322,6324,6327,6329,6239,6231,156,186,144,361,397,398,432,433,463,464,474,475,485,486,496,303,108,422,443,89,285,453,408,340,73,109,341,91,2,88,90,165,48])).
% 60.90/60.92 cnf(6335,plain,
% 60.90/60.92 (~P1(f2(a12,a12,x63351,x63351),f2(x63352,a11,x63353,x63353),a12)),
% 60.90/60.92 inference(scs_inference,[],[6226,6267,6269,6271,6273,6275,6278,6280,6283,6285,6288,6290,6293,6295,6298,6300,6302,6304,6306,6308,6310,6312,6314,6316,6320,6322,6324,6327,6329,6239,6231,404,5084,156,186,144,361,397,398,432,433,463,464,474,475,485,486,496,303,108,422,443,89,285,453,408,340,73,109,341,91,2,88,90,165,48,29])).
% 60.90/60.92 cnf(6336,plain,
% 60.90/60.92 (E(f2(x63361,x63361,x63362,x63362),x63361)),
% 60.90/60.92 inference(rename_variables,[],[5084])).
% 60.90/60.92 cnf(6337,plain,
% 60.90/60.92 (~P1(a12,f2(x63371,a11,x63372,x63372),f2(a12,a12,x63373,x63373))),
% 60.90/60.92 inference(scs_inference,[],[6226,6267,6269,6271,6273,6275,6278,6280,6283,6285,6288,6290,6293,6295,6298,6300,6302,6304,6306,6308,6310,6312,6314,6316,6320,6322,6324,6327,6329,6239,6231,404,5084,6336,156,186,144,361,397,398,432,433,463,464,474,475,485,486,496,303,108,422,443,89,285,453,408,340,73,109,341,91,2,88,90,165,48,29,31])).
% 60.90/60.92 cnf(6338,plain,
% 60.90/60.92 (E(f2(x63381,x63381,x63382,x63382),x63381)),
% 60.90/60.92 inference(rename_variables,[],[5084])).
% 60.90/60.92 cnf(6342,plain,
% 60.90/60.92 (~P2(x63421,x63421,a12,f2(a11,a11,x63422,x63422))),
% 60.90/60.92 inference(scs_inference,[],[5331,5118,6226,6267,6269,6271,6273,6275,6278,6280,6283,6285,6288,6290,6293,6295,6298,6300,6302,6304,6306,6308,6310,6312,6314,6316,6320,6322,6324,6327,6329,6239,6231,1592,404,5084,6336,6338,156,186,144,361,397,398,432,433,463,464,474,475,485,486,496,303,108,422,443,89,285,453,408,340,73,109,341,91,2,88,90,165,48,29,31,49,35])).
% 60.90/60.92 cnf(6344,plain,
% 60.90/60.92 (~P2(f2(x63441,a12,x63442,x63442),f2(x63443,a11,x63444,x63444),x63445,f2(x63446,x63445,x63447,x63447))),
% 60.90/60.92 inference(scs_inference,[],[5331,5118,6226,6267,6269,6271,6273,6275,6278,6280,6283,6285,6288,6290,6293,6295,6298,6300,6302,6304,6306,6308,6310,6312,6314,6316,6320,6322,6324,6327,6329,6331,351,6239,6231,1592,404,5084,6336,6338,156,186,144,361,397,398,432,433,463,464,474,475,485,486,496,303,108,422,443,89,285,453,408,340,73,109,341,91,2,88,90,165,48,29,31,49,35,34])).
% 60.90/60.92 cnf(6351,plain,
% 60.90/60.92 (~E(a10,f2(x63511,a12,x63512,x63512))),
% 60.90/60.92 inference(scs_inference,[],[430,73])).
% 60.90/60.92 cnf(6355,plain,
% 60.90/60.92 (E(x63551,f2(x63552,x63551,x63553,x63553))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6356,plain,
% 60.90/60.92 (~P1(f2(a12,a12,x63561,x63561),f2(x63562,a11,x63563,x63563),f2(x63564,a12,x63565,x63565))),
% 60.90/60.92 inference(scs_inference,[],[6332,6317,430,6335,6226,73,2,30,31])).
% 60.90/60.92 cnf(6357,plain,
% 60.90/60.92 (E(f2(x63571,x63572,x63573,x63573),x63572)),
% 60.90/60.92 inference(rename_variables,[],[6332])).
% 60.90/60.92 cnf(6360,plain,
% 60.90/60.92 (~P2(f2(x63601,a12,x63602,x63602),f2(x63603,a11,x63604,x63604),x63605,f2(x63606,x63605,x63607,x63607))),
% 60.90/60.92 inference(rename_variables,[],[6344])).
% 60.90/60.92 cnf(6363,plain,
% 60.90/60.92 (E(x63631,f2(x63632,x63631,x63633,x63633))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6366,plain,
% 60.90/60.92 (~P2(f2(x63661,a12,x63662,x63662),f2(x63663,a11,x63664,x63664),f2(x63665,x63666,x63667,x63667),f2(x63668,x63666,x63669,x63669))),
% 60.90/60.92 inference(scs_inference,[],[5085,6332,6357,6344,6360,6317,430,6335,6226,6355,6363,73,2,30,31,49,32,33,34])).
% 60.90/60.92 cnf(6368,plain,
% 60.90/60.92 (~P1(f2(x63681,a12,x63682,x63682),f2(x63683,a11,x63684,x63684),f2(a12,a12,x63685,x63685))),
% 60.90/60.92 inference(scs_inference,[],[5085,6332,6357,6344,6360,6317,430,6335,6337,6226,6355,6363,73,2,30,31,49,32,33,34,29])).
% 60.90/60.92 cnf(6375,plain,
% 60.90/60.92 (~E(a11,f2(x63751,a10,x63752,x63752))),
% 60.90/60.92 inference(scs_inference,[],[461,73])).
% 60.90/60.92 cnf(6377,plain,
% 60.90/60.92 (~E(a8,f2(a9,a6,x63771,x63772))),
% 60.90/60.92 inference(scs_inference,[],[461,4406,73,2])).
% 60.90/60.92 cnf(6378,plain,
% 60.90/60.92 (~P1(f2(a11,a11,x63781,x63781),f2(x63782,a1,x63783,x63783),a11)),
% 60.90/60.92 inference(scs_inference,[],[461,4406,6235,6332,73,2,30])).
% 60.90/60.92 cnf(6379,plain,
% 60.90/60.92 (E(f2(x63791,x63792,x63793,x63793),x63792)),
% 60.90/60.92 inference(rename_variables,[],[6332])).
% 60.90/60.92 cnf(6380,plain,
% 60.90/60.92 (~P1(a12,f2(x63801,a11,x63802,x63802),f2(x63803,a12,x63804,x63804))),
% 60.90/60.92 inference(scs_inference,[],[6356,461,4406,6235,6332,6226,73,2,30,29])).
% 60.90/60.92 cnf(6381,plain,
% 60.90/60.92 (E(x63811,f2(x63812,x63811,x63813,x63813))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6383,plain,
% 60.90/60.92 (E(f2(x63831,x63832,x63833,x63833),x63832)),
% 60.90/60.92 inference(rename_variables,[],[6332])).
% 60.90/60.92 cnf(6385,plain,
% 60.90/60.92 (~P2(f2(x63851,a12,x63852,x63852),f2(x63853,a11,x63854,x63854),f2(x63855,x63856,x63857,x63857),f2(x63858,x63856,x63859,x63859))),
% 60.90/60.92 inference(rename_variables,[],[6366])).
% 60.90/60.92 cnf(6390,plain,
% 60.90/60.92 (~P2(f2(x63901,a1,x63902,x63902),f2(x63903,a12,x63904,x63904),x63905,x63905)),
% 60.90/60.92 inference(scs_inference,[],[6366,6385,6356,461,1602,4406,1621,6235,5085,6332,6379,6383,6226,6381,73,2,30,29,31,49,35,32])).
% 60.90/60.92 cnf(6391,plain,
% 60.90/60.92 (E(f2(x63911,x63912,x63913,x63913),x63912)),
% 60.90/60.92 inference(rename_variables,[],[6332])).
% 60.90/60.92 cnf(6392,plain,
% 60.90/60.92 (~P2(f2(x63921,a11,x63922,x63922),f2(x63923,a1,x63924,x63924),x63925,x63925)),
% 60.90/60.92 inference(scs_inference,[],[6366,6385,6356,441,461,1602,4406,1621,6235,5085,6332,6379,6383,6391,6226,6381,73,2,30,29,31,49,35,32,33])).
% 60.90/60.92 cnf(6399,plain,
% 60.90/60.92 (~E(f2(x63991,a12,x63992,x63992),f2(x63993,a1,x63994,x63994))),
% 60.90/60.92 inference(scs_inference,[],[6390,73])).
% 60.90/60.92 cnf(6400,plain,
% 60.90/60.92 (~P2(f2(x64001,a1,x64002,x64002),f2(x64003,a12,x64004,x64004),x64005,x64005)),
% 60.90/60.92 inference(rename_variables,[],[6390])).
% 60.90/60.92 cnf(6403,plain,
% 60.90/60.92 (E(x64031,f2(x64032,x64031,x64033,x64033))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6404,plain,
% 60.90/60.92 (~P1(f2(x64041,a12,x64042,x64042),f2(x64043,a11,x64044,x64044),f2(x64045,a12,x64046,x64046))),
% 60.90/60.92 inference(scs_inference,[],[6390,6368,6380,249,6226,6332,73,2,30,29])).
% 60.90/60.92 cnf(6407,plain,
% 60.90/60.92 (E(x64071,f2(x64072,x64071,x64073,x64073))),
% 60.90/60.92 inference(rename_variables,[],[6226])).
% 60.90/60.92 cnf(6408,plain,
% 60.90/60.92 (~P2(a12,f2(x64081,a10,x64082,x64082),x64083,x64083)),
% 60.90/60.92 inference(scs_inference,[],[6390,6368,6380,6256,249,314,6226,6403,6332,73,2,30,29,31,49])).
% 60.90/60.92 cnf(6410,plain,
% 60.90/60.92 (~P2(f2(x64101,a1,x64102,x64102),f2(x64103,a12,x64104,x64104),f2(x64105,x64106,x64107,x64107),x64106)),
% 60.90/60.92 inference(scs_inference,[],[6390,6400,6368,6380,6256,249,314,6226,6403,6407,6332,73,2,30,29,31,49,35])).
% 60.90/60.92 cnf(6411,plain,
% 60.90/60.92 (~P2(f2(x64111,a1,x64112,x64112),f2(x64113,a12,x64114,x64114),x64115,x64115)),
% 60.90/60.92 inference(rename_variables,[],[6390])).
% 60.90/60.92 cnf(6414,plain,
% 60.90/60.92 (~E(f2(x64141,a1,x64142,x64142),a10)),
% 60.90/60.92 inference(scs_inference,[],[6217,6390,6400,6411,6368,6380,6256,249,314,6226,6403,6407,6332,73,2,30,29,31,49,35,34,3])).
% 60.90/60.92 cnf(6423,plain,
% 60.90/60.92 (~E(f2(x64231,a1,x64232,x64232),f2(x64233,a11,x64234,x64234))),
% 60.90/60.92 inference(scs_inference,[],[6392,73])).
% 60.90/60.92 cnf(6427,plain,
% 60.90/60.92 (E(f2(x64271,x64272,x64273,x64273),x64272)),
% 60.90/60.92 inference(rename_variables,[],[6332])).
% 60.90/60.92 cnf(6431,plain,
% 60.90/60.92 (~P1(f2(a11,a11,x64311,x64311),f2(x64312,a1,x64313,x64313),f2(x64314,a11,x64315,x64315))),
% 60.90/60.92 inference(scs_inference,[],[6392,6399,6404,6378,6226,6332,6427,73,2,3,30,31])).
% 60.90/60.92 cnf(6446,plain,
% 60.90/60.92 (~E(f2(x64461,a10,x64462,x64462),f2(x64463,a12,x64464,x64464))),
% 60.90/60.92 inference(scs_inference,[],[6423,472,6351,6226,73,2,3])).
% 60.90/60.92 cnf(6447,plain,
% 60.90/60.93 (E(x64471,f2(x64472,x64471,x64473,x64473))),
% 60.90/60.93 inference(rename_variables,[],[6226])).
% 60.90/60.93 cnf(6448,plain,
% 60.90/60.93 (~P1(f2(a11,a11,x64481,x64481),a1,f2(x64482,a11,x64483,x64483))),
% 60.90/60.93 inference(scs_inference,[],[6423,6431,472,6351,6226,6447,73,2,3,30])).
% 60.90/60.93 cnf(6450,plain,
% 60.90/60.93 (~P2(a10,f2(x64501,a12,x64502,x64502),x64503,x64503)),
% 60.90/60.93 inference(scs_inference,[],[6423,6431,472,6351,6270,314,6226,6447,73,2,3,30,49])).
% 60.90/60.93 cnf(6466,plain,
% 60.90/60.93 (~P1(a10,f2(x64661,a11,x64662,x64662),a10)),
% 60.90/60.93 inference(scs_inference,[],[6446,533,566,6332,73,2,30])).
% 60.90/60.93 cnf(6467,plain,
% 60.90/60.93 (E(f2(x64671,x64672,x64673,x64673),x64672)),
% 60.90/60.93 inference(rename_variables,[],[6332])).
% 60.90/60.93 cnf(6472,plain,
% 60.90/60.93 (E(f2(x64721,x64722,x64723,x64723),x64722)),
% 60.90/60.93 inference(rename_variables,[],[6332])).
% 60.90/60.93 cnf(6473,plain,
% 60.90/60.93 (~P2(f2(x64731,a12,x64732,x64732),f2(x64733,a10,x64734,x64734),x64735,x64735)),
% 60.90/60.93 inference(scs_inference,[],[6410,6446,6408,533,5118,566,6332,6467,6472,73,2,30,49,35,32])).
% 60.90/60.93 cnf(6474,plain,
% 60.90/60.93 (E(f2(x64741,x64742,x64743,x64743),x64742)),
% 60.90/60.93 inference(rename_variables,[],[6332])).
% 60.90/60.93 cnf(6475,plain,
% 60.90/60.93 (~P2(f2(x64751,a1,x64752,x64752),f2(x64753,a11,x64754,x64754),x64755,x64755)),
% 60.90/60.93 inference(scs_inference,[],[6410,6446,451,6408,533,5118,566,6332,6467,6472,6474,73,2,30,49,35,32,33])).
% 60.90/60.93 cnf(6482,plain,
% 60.90/60.93 (~E(a10,f2(x64821,a1,x64822,x64822))),
% 60.90/60.93 inference(scs_inference,[],[547,6414,73,2])).
% 60.90/60.93 cnf(6485,plain,
% 60.90/60.93 (~P2(f2(x64851,a12,x64852,x64852),f2(x64853,a10,x64854,x64854),f2(x64855,x64856,x64857,x64857),x64856)),
% 60.90/60.93 inference(scs_inference,[],[6473,547,6243,6414,6272,6226,73,2,49,35])).
% 60.90/60.93 cnf(6486,plain,
% 60.90/60.93 (~P2(f2(x64861,a12,x64862,x64862),f2(x64863,a10,x64864,x64864),x64865,x64865)),
% 60.90/60.93 inference(rename_variables,[],[6473])).
% 60.90/60.93 cnf(6487,plain,
% 60.90/60.93 (~P2(f2(x64871,a12,x64872,x64872),f2(x64873,a10,x64874,x64874),x64875,f2(x64876,x64875,x64877,x64877))),
% 60.90/60.93 inference(scs_inference,[],[6473,6486,547,6243,6414,6272,6226,73,2,49,35,34])).
% 60.90/60.93 cnf(6489,plain,
% 60.90/60.93 (~P1(a11,a1,f2(x64891,a11,x64892,x64892))),
% 60.90/60.93 inference(scs_inference,[],[6473,6486,547,6448,6243,6414,6272,6226,73,2,49,35,34,29])).
% 60.90/60.93 cnf(6501,plain,
% 60.90/60.93 (~P2(x65011,f2(x65012,x65011,a12,a11),x65013,x65013)),
% 60.90/60.93 inference(scs_inference,[],[406,554,5074,633,73,2,49])).
% 60.90/60.93 cnf(6505,plain,
% 60.90/60.93 (~P2(f2(x65051,a1,x65052,x65052),f2(x65053,a11,x65054,x65054),x65055,f2(x65056,x65055,x65057,x65057))),
% 60.90/60.93 inference(scs_inference,[],[6475,406,554,5074,6332,633,73,2,49,35])).
% 60.90/60.93 cnf(6506,plain,
% 60.90/60.93 (E(f2(x65061,x65062,x65063,x65063),x65062)),
% 60.90/60.93 inference(rename_variables,[],[6332])).
% 60.90/60.93 cnf(6509,plain,
% 60.90/60.93 (~P2(f2(x65091,a10,x65092,x65092),f2(x65093,a12,x65094,x65094),x65095,x65095)),
% 60.90/60.93 inference(scs_inference,[],[6475,406,6450,554,5074,6332,6506,633,73,2,49,35,34,32])).
% 60.90/60.93 cnf(6514,plain,
% 60.90/60.93 (~P2(x65141,f2(x65142,x65141,a12,a11),x65143,x65143)),
% 60.90/60.93 inference(rename_variables,[],[6501])).
% 60.90/60.93 cnf(6515,plain,
% 60.90/60.93 (~E(x65151,f2(x65152,x65151,a12,a11))),
% 60.90/60.93 inference(scs_inference,[],[6501,73,2])).
% 60.90/60.93 cnf(6516,plain,
% 60.90/60.93 (~P2(a12,f2(x65161,a1,x65162,x65162),f2(x65163,x65163,x65164,x65164),x65163)),
% 60.90/60.93 inference(scs_inference,[],[6501,6245,6274,73,2,49])).
% 60.90/60.93 cnf(6519,plain,
% 60.90/60.93 (~P2(x65191,f2(x65192,x65191,a12,a11),x65193,x65193)),
% 60.90/60.93 inference(rename_variables,[],[6501])).
% 60.90/60.93 cnf(6520,plain,
% 60.90/60.93 (~P2(f2(x65201,x65202,x65203,x65203),f2(x65204,x65202,a12,a11),x65205,x65205)),
% 60.90/60.93 inference(scs_inference,[],[6501,6514,6519,6245,6274,6332,73,2,49,35,32])).
% 60.90/60.93 cnf(6521,plain,
% 60.90/60.93 (E(f2(x65211,x65212,x65213,x65213),x65212)),
% 60.90/60.93 inference(rename_variables,[],[6332])).
% 60.90/60.93 cnf(6522,plain,
% 60.90/60.93 (~P2(x65221,f2(x65222,x65221,a12,a11),f2(x65223,x65224,x65225,x65225),x65224)),
% 60.90/60.93 inference(scs_inference,[],[6501,6514,6519,6245,6274,6332,6521,73,2,49,35,32,34])).
% 60.90/60.93 cnf(6523,plain,
% 60.90/60.93 (E(f2(x65231,x65232,x65233,x65233),x65232)),
% 60.90/60.93 inference(rename_variables,[],[6332])).
% 60.90/60.93 cnf(6524,plain,
% 60.90/60.93 (~E(f2(x65241,a11,x65242,x65242),f2(x65243,a10,x65244,x65244))),
% 60.90/60.93 inference(scs_inference,[],[6501,6514,6519,6245,6375,6274,6332,6521,6226,73,2,49,35,32,34,3])).
% 60.90/60.93 cnf(6526,plain,
% 60.90/60.93 (~P1(f2(x65261,a10,x65262,x65262),f2(x65263,a12,x65264,x65264),f2(x65261,a10,x65262,x65262))),
% 60.90/60.93 inference(scs_inference,[],[6501,6514,6519,6245,6375,6274,414,6332,6521,6523,6226,73,2,49,35,32,34,3,30])).
% 60.90/60.93 cnf(6527,plain,
% 60.90/60.93 (E(f2(x65271,x65272,x65273,x65273),x65272)),
% 60.90/60.93 inference(rename_variables,[],[6332])).
% 60.90/60.93 cnf(6528,plain,
% 60.90/60.93 (~P1(a10,f2(x65281,a11,x65282,x65282),f2(x65283,a10,x65284,x65284))),
% 60.90/60.93 inference(scs_inference,[],[6501,6514,6519,6245,6375,6466,6274,414,6332,6521,6523,6527,6226,73,2,49,35,32,34,3,30,31])).
% 60.90/60.93 cnf(6538,plain,
% 60.90/60.93 (~E(f2(x65381,x65382,a12,a11),f2(x65383,x65382,x65384,x65384))),
% 60.90/60.93 inference(scs_inference,[],[6520,73])).
% 60.90/60.93 cnf(6541,plain,
% 60.90/60.93 (~P1(a10,f2(x65411,a12,x65412,x65412),f2(x65413,a10,x65414,x65414))),
% 60.90/60.93 inference(scs_inference,[],[6520,6526,6524,6226,73,2,29])).
% 60.90/60.93 cnf(6542,plain,
% 60.90/60.93 (E(x65421,f2(x65422,x65421,x65423,x65423))),
% 60.90/60.93 inference(rename_variables,[],[6226])).
% 60.90/60.93 cnf(6546,plain,
% 60.90/60.93 (~P1(f2(x65461,a10,x65462,x65462),f2(x65463,a12,x65464,x65464),a10)),
% 60.90/60.93 inference(scs_inference,[],[6520,6505,6526,6524,5606,6226,6542,73,2,29,49,31])).
% 60.90/60.93 cnf(6548,plain,
% 60.90/60.93 (~P2(f2(x65481,a10,x65482,x65482),f2(x65483,a12,x65484,x65484),x65485,f2(x65486,x65485,x65487,x65487))),
% 60.90/60.93 inference(scs_inference,[],[6509,6520,6505,6526,6524,5606,6332,6226,6542,73,2,29,49,31,35])).
% 60.90/60.93 cnf(6560,plain,
% 60.90/60.93 (~P1(f2(x65601,a10,x65602,x65602),f2(x65603,a11,x65604,x65604),f2(x65605,a10,x65606,x65606))),
% 60.90/60.93 inference(scs_inference,[],[6538,6528,6332,2,29])).
% 60.90/60.93 cnf(6561,plain,
% 60.90/60.93 (E(f2(x65611,x65612,x65613,x65613),x65612)),
% 60.90/60.93 inference(rename_variables,[],[6332])).
% 60.90/60.93 cnf(6564,plain,
% 60.90/60.93 (~P1(f2(x65641,a10,x65642,x65642),f2(x65643,a12,x65644,x65644),f2(x65645,a10,x65646,x65646))),
% 60.90/60.93 inference(scs_inference,[],[6538,6528,6546,6277,1599,6332,6561,2,29,49,31])).
% 60.90/60.93 cnf(6565,plain,
% 60.90/60.93 (E(f2(x65651,x65652,x65653,x65653),x65652)),
% 60.90/60.93 inference(rename_variables,[],[6332])).
% 60.90/60.93 cnf(6566,plain,
% 60.90/60.93 (~P2(x65661,f2(x65662,x65661,a12,a11),f2(x65663,x65664,x65665,x65665),f2(x65666,x65664,x65667,x65667))),
% 60.90/60.93 inference(scs_inference,[],[6522,6538,6528,6546,6277,1599,6332,6561,6565,2,29,49,31,35])).
% 60.90/60.93 cnf(6583,plain,
% 60.90/60.93 (~P1(f2(x65831,a10,x65832,x65832),a11,f2(x65833,a10,x65834,x65834))),
% 60.90/60.93 inference(scs_inference,[],[6560,6226,30])).
% 60.90/60.93 cnf(6584,plain,
% 60.90/60.93 (E(x65841,f2(x65842,x65841,x65843,x65843))),
% 60.90/60.93 inference(rename_variables,[],[6226])).
% 60.90/60.93 cnf(6585,plain,
% 60.90/60.93 (~P2(f2(x65851,x65852,a12,a1),x65852,f2(x65853,x65853,x65854,x65854),x65853)),
% 60.90/60.93 inference(scs_inference,[],[6560,6516,5077,6226,30,49])).
% 60.90/60.93 cnf(6592,plain,
% 60.90/60.93 (E(f2(x65921,x65922,x65923,x65923),x65922)),
% 60.90/60.93 inference(rename_variables,[],[6332])).
% 60.90/60.93 cnf(6595,plain,
% 60.90/60.93 (~P2(f2(x65951,a12,x65952,x65952),f2(x65953,a1,x65954,x65954),x65955,x65955)),
% 60.90/60.93 inference(scs_inference,[],[6485,6566,6560,6516,483,5077,6332,6592,6226,6584,30,49,31,35,32,33])).
% 60.90/60.93 cnf(6599,plain,
% 60.90/60.93 (~P1(f2(x65991,a1,x65992,x65992),f2(x65993,a11,x65994,x65994),f2(x65991,a1,x65992,x65992))),
% 60.90/60.93 inference(scs_inference,[],[449,6332,30])).
% 60.90/60.93 cnf(6600,plain,
% 60.90/60.93 (E(f2(x66001,x66002,x66003,x66003),x66002)),
% 60.90/60.93 inference(rename_variables,[],[6332])).
% 60.90/60.93 cnf(6604,plain,
% 60.90/60.93 (E(f2(x66041,x66042,x66043,x66043),x66042)),
% 60.90/60.93 inference(rename_variables,[],[6332])).
% 60.90/60.93 cnf(6605,plain,
% 60.90/60.93 (~P2(f2(x66051,x66052,a12,a1),x66052,f2(x66053,x66053,x66054,x66054),f2(x66055,x66053,x66056,x66056))),
% 60.90/60.93 inference(scs_inference,[],[6585,6279,97,1599,449,6332,6600,6604,30,49,31,35])).
% 60.90/60.93 cnf(6606,plain,
% 60.90/60.93 (~P2(f2(x66061,x66062,a12,a1),x66062,f2(x66063,x66063,x66064,x66064),x66063)),
% 60.90/60.93 inference(rename_variables,[],[6585])).
% 60.90/60.93 cnf(6608,plain,
% 60.90/60.93 (E(x66081,f2(x66082,x66081,x66083,x66083))),
% 60.90/60.93 inference(rename_variables,[],[6226])).
% 60.90/60.93 cnf(6609,plain,
% 60.90/60.93 (~P2(f2(x66091,x66092,a12,a1),f2(x66093,x66092,x66094,x66094),f2(x66095,x66095,x66096,x66096),x66095)),
% 60.90/60.93 inference(scs_inference,[],[6585,6606,6595,6279,97,1599,449,6332,6600,6604,6226,30,49,31,35,32,33])).
% 60.90/60.93 cnf(6610,plain,
% 60.90/60.93 (E(f2(x66101,x66102,x66103,x66103),x66102)),
% 60.90/60.93 inference(rename_variables,[],[6332])).
% 60.90/60.93 cnf(6612,plain,
% 60.90/60.93 (E(x66121,f2(x66122,x66121,x66123,x66123))),
% 60.90/60.93 inference(rename_variables,[],[6226])).
% 60.90/60.93 cnf(6613,plain,
% 60.90/60.93 (P1(a1,a1,a1)),
% 60.90/60.93 inference(scs_inference,[],[43,6585,6606,6595,6279,97,1599,449,6332,6600,6604,6226,6608,333,30,49,31,35,32,33,34,50])).
% 60.90/60.93 cnf(6615,plain,
% 60.90/60.93 (~E(x66151,f2(x66152,x66151,a12,a1))),
% 60.90/60.93 inference(scs_inference,[],[43,6585,6606,6595,6279,97,1599,449,6332,6600,6604,6226,6608,333,30,49,31,35,32,33,34,50,73])).
% 60.90/60.93 cnf(6617,plain,
% 60.90/60.93 (P1(a1,f7(a1,a1,a1,a1,a1),a1)),
% 60.90/60.93 inference(scs_inference,[],[43,6585,6606,6595,6279,97,1599,449,6332,6600,6604,6226,6608,333,30,49,31,35,32,33,34,50,73,2,53])).
% 60.90/60.93 cnf(6619,plain,
% 60.90/60.93 (~E(f2(x66191,a10,x66192,x66192),f2(x66193,a1,x66194,x66194))),
% 60.90/60.93 inference(scs_inference,[],[43,6585,6606,6595,6482,6279,97,1599,449,6332,6600,6604,6226,6608,6612,333,30,49,31,35,32,33,34,50,73,2,53,3])).
% 60.90/60.93 cnf(6621,plain,
% 60.90/60.93 (~P1(f2(x66211,a11,x66212,x66212),a1,f2(x66213,a11,x66214,x66214))),
% 60.90/60.93 inference(scs_inference,[],[43,6585,6606,6595,6482,6279,6489,97,1599,449,6332,6600,6604,6610,6226,6608,6612,333,30,49,31,35,32,33,34,50,73,2,53,3,29])).
% 60.90/60.93 cnf(6623,plain,
% 60.90/60.93 (P1(a1,f5(a1,a1,a1,a1,a1,a1),a1)),
% 60.90/60.93 inference(scs_inference,[],[43,6585,6606,6595,6482,6279,6489,97,1599,449,6332,6600,6604,6610,6226,6608,6612,63,333,30,49,31,35,32,33,34,50,73,2,53,3,29,57])).
% 60.90/60.93 cnf(6627,plain,
% 60.90/60.93 (E(a1,f7(a1,a1,a1,a1,a1))),
% 60.90/60.93 inference(scs_inference,[],[43,6585,6606,6595,6482,6279,6489,97,1599,449,6332,6600,6604,6610,6226,6608,6612,63,333,30,49,31,35,32,33,34,50,73,2,53,3,29,57,47])).
% 60.90/60.93 cnf(6629,plain,
% 60.90/60.93 (P2(f7(a1,a1,a1,a1,a1),a12,a11,a1)),
% 60.90/60.93 inference(scs_inference,[],[43,6585,6606,6595,6482,6279,6489,97,1599,449,6332,6600,6604,6610,6226,6608,6612,63,333,30,49,31,35,32,33,34,50,73,2,53,3,29,57,47,397])).
% 60.90/60.93 cnf(6630,plain,
% 60.90/60.93 (P2(f7(a1,a1,a1,a1,a1),a12,a1,a11)),
% 60.90/60.93 inference(scs_inference,[],[43,6585,6606,6595,6482,6279,6489,97,1599,449,6332,6600,6604,6610,6226,6608,6612,63,333,30,49,31,35,32,33,34,50,73,2,53,3,29,57,47,397,432])).
% 60.90/60.93 cnf(6632,plain,
% 60.90/60.93 (P2(a12,a1,f7(a1,a1,a1,a1,a1),a11)),
% 60.90/60.93 inference(scs_inference,[],[43,6585,6606,6595,6482,6279,6489,97,1599,449,6332,6600,6604,6610,6226,6608,6612,63,333,30,49,31,35,32,33,34,50,73,2,53,3,29,57,47,397,432,408,453])).
% 60.90/60.93 cnf(6636,plain,
% 60.90/60.93 (P2(a1,a11,f7(a1,a1,a1,a1,a1),a12)),
% 60.90/60.93 inference(scs_inference,[],[43,6585,6606,6595,6482,6279,6489,97,1599,449,6332,6600,6604,6610,6226,6608,6612,63,333,30,49,31,35,32,33,34,50,73,2,53,3,29,57,47,397,432,408,453,340,285,91,88])).
% 60.90/60.93 cnf(6637,plain,
% 60.90/60.93 (P2(f7(a1,a1,a1,a1,a1),a11,a1,a12)),
% 60.90/60.93 inference(scs_inference,[],[43,6585,6606,6595,6482,6279,6489,97,1599,449,6332,6600,6604,6610,6226,6608,6612,63,333,30,49,31,35,32,33,34,50,73,2,53,3,29,57,47,397,432,408,453,340,285,91,88,90])).
% 60.90/60.93 cnf(6649,plain,
% 60.90/60.93 (E(a1,f5(a1,a1,a1,a1,a1,a1))),
% 60.90/60.93 inference(scs_inference,[],[6627,6623,398,433,47])).
% 60.90/60.93 cnf(6651,plain,
% 60.90/60.93 (P2(f5(a1,a1,a1,a1,a1,a1),a12,a11,a1)),
% 60.90/60.93 inference(scs_inference,[],[6627,6623,398,433,47,397])).
% 60.90/60.93 cnf(6652,plain,
% 60.90/60.93 (P2(f5(a1,a1,a1,a1,a1,a1),a12,a1,a11)),
% 60.90/60.93 inference(scs_inference,[],[6627,6623,398,433,47,397,432])).
% 60.90/60.93 cnf(6660,plain,
% 60.90/60.93 (~E(f2(x66601,a1,x66602,x66602),f2(x66603,a10,x66604,x66604))),
% 60.90/60.93 inference(scs_inference,[],[6627,6619,6623,398,433,47,397,432,453,408,285,340,91,88,90,2])).
% 60.90/60.93 cnf(6661,plain,
% 60.90/60.93 (~E(f7(a1,a1,a1,a1,a1),f2(x66611,a1,a12,a11))),
% 60.90/60.93 inference(scs_inference,[],[6627,6515,6619,6623,398,433,47,397,432,453,408,285,340,91,88,90,2,3])).
% 60.90/60.93 cnf(6663,plain,
% 60.90/60.93 (P1(f7(a1,a1,a1,a1,a1),a1,a1)),
% 60.90/60.93 inference(scs_inference,[],[6613,6627,6515,6619,6623,398,433,47,397,432,453,408,285,340,91,88,90,2,3,29])).
% 60.90/60.93 cnf(6668,plain,
% 60.90/60.93 (P1(a1,a1,f7(a1,a1,a1,a1,a1))),
% 60.90/60.93 inference(scs_inference,[],[6613,6627,6515,6619,588,6623,5076,398,433,47,397,432,453,408,285,340,91,88,90,2,3,29,49,31])).
% 60.90/60.93 cnf(6693,plain,
% 60.90/60.93 (~E(f5(a1,a1,a1,a1,a1,a1),f2(x66931,a1,a12,a1))),
% 60.90/60.93 inference(scs_inference,[],[6649,6615,6661,433,398,2,3])).
% 60.90/60.93 cnf(6695,plain,
% 60.90/60.93 (~P1(a1,f2(x66951,a11,x66952,x66952),f2(x66953,a1,x66954,x66954))),
% 60.90/60.93 inference(scs_inference,[],[6649,6599,6615,6661,6226,433,398,2,3,29])).
% 60.90/60.93 cnf(6696,plain,
% 60.90/60.93 (~P1(f2(x66961,a1,x66962,x66962),f2(x66963,a11,x66964,x66964),f2(x66961,a1,x66962,x66962))),
% 60.90/60.93 inference(rename_variables,[],[6599])).
% 60.90/60.93 cnf(6697,plain,
% 60.90/60.93 (E(x66971,f2(x66972,x66971,x66973,x66973))),
% 60.90/60.93 inference(rename_variables,[],[6226])).
% 60.90/60.93 cnf(6698,plain,
% 60.90/60.93 (P1(a1,f5(a1,a1,a1,a1,a1,a1),f4(a1,a1,a10,a11,a11))),
% 60.90/60.93 inference(scs_inference,[],[6249,6649,6599,6615,6661,6226,433,398,2,3,29,30])).
% 60.90/60.93 cnf(6699,plain,
% 60.90/60.93 (~P2(f7(a1,a1,a1,a1,a1),a12,x66991,f2(x66991,x66991,x66992,x66992))),
% 60.90/60.93 inference(scs_inference,[],[6249,6649,6599,6615,6629,6661,6243,6226,433,398,2,3,29,30,49])).
% 60.90/60.93 cnf(6701,plain,
% 60.90/60.93 (~P1(f2(x67011,a1,x67012,x67012),f2(x67013,a11,x67014,x67014),a1)),
% 60.90/60.93 inference(scs_inference,[],[6249,6649,6599,6696,6615,6629,6661,6243,6226,6697,433,398,2,3,29,30,49,31])).
% 60.90/60.93 cnf(6706,plain,
% 60.90/60.93 (~P2(f2(x67061,x67062,a12,a1),f2(x67063,x67062,x67064,x67064),f2(x67065,x67065,x67066,x67066),f2(x67067,x67065,x67068,x67068))),
% 60.90/60.93 inference(scs_inference,[],[6249,6649,6605,6599,6696,6615,6629,6661,6342,6243,6226,6697,6332,433,398,2,3,29,30,49,31,32,33])).
% 60.90/60.93 cnf(6714,plain,
% 60.90/60.93 (~E(f5(a1,a1,a1,a1,a1,a1),f2(x67141,a12,x67142,x67142))),
% 60.90/60.93 inference(scs_inference,[],[6693,1601,6649,2,3])).
% 60.90/60.93 cnf(6718,plain,
% 60.90/60.93 (E(x67181,f2(x67182,x67181,x67183,x67183))),
% 60.90/60.93 inference(rename_variables,[],[6226])).
% 60.90/60.93 cnf(6720,plain,
% 60.90/60.93 (~P2(f2(x67201,a12,x67202,x67202),f2(x67203,a10,x67204,x67204),x67205,f2(x67206,x67205,x67207,x67207))),
% 60.90/60.93 inference(rename_variables,[],[6487])).
% 60.90/60.93 cnf(6723,plain,
% 60.90/60.93 (P1(a1,f7(a1,a1,a1,a1,a1),f5(a1,a1,a1,a1,a1,a1))),
% 60.90/60.93 inference(scs_inference,[],[6247,6617,6487,6564,6693,1601,5085,6649,6226,2,3,29,30,49,31])).
% 60.90/60.93 cnf(6725,plain,
% 60.90/60.93 (~P2(f2(x67251,a12,x67252,x67252),f2(x67253,a10,x67254,x67254),x67255,f2(x67256,x67255,x67257,x67257))),
% 60.90/60.93 inference(rename_variables,[],[6487])).
% 60.90/60.93 cnf(6726,plain,
% 60.90/60.93 (E(x67261,f2(x67262,x67261,x67263,x67263))),
% 60.90/60.93 inference(rename_variables,[],[6226])).
% 60.90/60.93 cnf(6729,plain,
% 60.90/60.93 (E(x67291,f2(x67292,x67291,x67293,x67293))),
% 60.90/60.93 inference(rename_variables,[],[6226])).
% 60.90/60.93 cnf(6730,plain,
% 60.90/60.93 (~P2(f2(x67301,x67302,a12,a1),f2(x67303,x67302,x67304,x67304),x67305,x67305)),
% 60.90/60.93 inference(scs_inference,[],[6247,6617,6609,6487,6720,6725,6564,6693,1601,5085,6649,6226,6718,6726,6729,2,3,29,30,49,31,32,33,34])).
% 60.90/60.93 cnf(6733,plain,
% 60.90/60.93 (~E(f2(x67331,x67332,x67333,x67333),f2(x67334,x67332,a12,a1))),
% 60.90/60.93 inference(scs_inference,[],[6247,6617,6609,6487,6720,6725,6564,6693,1601,5085,6649,6226,6718,6726,6729,2,3,29,30,49,31,32,33,34,73])).
% 60.90/60.93 cnf(6737,plain,
% 60.90/60.93 (~E(a1,f2(x67371,a10,x67372,x67372))),
% 60.90/60.93 inference(scs_inference,[],[6714,6660,6332,2,3])).
% 60.90/60.93 cnf(6739,plain,
% 60.90/60.93 (E(f2(x67391,x67392,x67393,x67393),x67392)),
% 60.90/60.93 inference(rename_variables,[],[6332])).
% 60.90/60.93 cnf(6740,plain,
% 60.90/60.93 (~P1(f2(x67401,a1,x67402,x67402),f2(x67403,a11,x67404,x67404),f2(x67405,a1,x67406,x67406))),
% 60.90/60.93 inference(scs_inference,[],[6714,6660,6695,6332,6739,2,3,29])).
% 60.90/60.93 cnf(6741,plain,
% 60.90/60.93 (E(f2(x67411,x67412,x67413,x67413),x67412)),
% 60.90/60.93 inference(rename_variables,[],[6332])).
% 60.90/60.93 cnf(6742,plain,
% 60.90/60.93 (P1(f7(a1,a1,a1,a1,a1),f7(a1,a1,a1,a1,a1),a1)),
% 60.90/60.93 inference(scs_inference,[],[6714,6660,6695,6663,6627,6332,6739,2,3,29,30])).
% 60.90/60.93 cnf(6743,plain,
% 60.90/60.93 (~P2(f7(a1,a1,a1,a1,a1),a12,f2(x67431,x67432,x67433,x67433),x67432)),
% 60.90/60.93 inference(scs_inference,[],[6630,6714,6660,6695,6663,1599,6627,6332,6739,2,3,29,30,49])).
% 60.90/60.93 cnf(6745,plain,
% 60.90/60.93 (~P1(a11,f2(x67451,a12,x67452,x67452),f2(x67453,a11,x67454,x67454))),
% 60.90/60.93 inference(scs_inference,[],[6630,6714,6660,6695,6663,242,1599,6627,6332,6739,6741,2,3,29,30,49,31])).
% 60.90/60.93 cnf(6746,plain,
% 60.90/60.93 (E(f2(x67461,x67462,x67463,x67463),x67462)),
% 60.90/60.93 inference(rename_variables,[],[6332])).
% 60.90/60.93 cnf(6748,plain,
% 60.90/60.93 (~P2(f2(x67481,x67482,a12,a1),f2(x67483,x67482,x67484,x67484),x67485,x67485)),
% 60.90/60.93 inference(rename_variables,[],[6730])).
% 60.90/60.93 cnf(6749,plain,
% 60.90/60.93 (~P2(a1,a12,x67491,f2(x67491,x67491,x67492,x67492))),
% 60.90/60.93 inference(scs_inference,[],[6630,6730,6714,6660,6699,6695,6663,242,1599,6627,6332,6739,6741,2,3,29,30,49,31,35,32])).
% 60.90/60.93 cnf(6752,plain,
% 60.90/60.93 (~P2(f7(a1,a1,a1,a1,a1),f2(x67521,a12,x67522,x67522),x67523,f2(x67523,x67523,x67524,x67524))),
% 60.90/60.93 inference(scs_inference,[],[6630,6730,6748,6714,6660,6699,6695,6663,242,1599,6627,6332,6739,6741,6746,2,3,29,30,49,31,35,32,34,33])).
% 60.90/60.93 cnf(6758,plain,
% 60.90/60.93 (~E(f5(a1,a1,a1,a1,a1,a1),f2(x67581,a10,x67582,x67582))),
% 60.90/60.93 inference(scs_inference,[],[6733,6737,6649,2,3])).
% 60.90/60.93 cnf(6761,plain,
% 60.90/60.93 (E(x67611,f2(x67612,x67611,x67613,x67613))),
% 60.90/60.93 inference(rename_variables,[],[6226])).
% 60.90/60.93 cnf(6762,plain,
% 60.90/60.93 (P1(f5(a1,a1,a1,a1,a1,a1),f5(a1,a1,a1,a1,a1,a1),f4(a1,a1,a10,a11,a11))),
% 60.90/60.93 inference(scs_inference,[],[6733,6740,6698,6737,6649,6226,2,3,30,29])).
% 60.90/60.93 cnf(6766,plain,
% 60.90/60.93 (P1(f7(a1,a1,a1,a1,a1),f7(a1,a1,a1,a1,a1),f5(a1,a1,a1,a1,a1,a1))),
% 60.90/60.93 inference(scs_inference,[],[6548,6733,6740,6698,6742,6737,5490,6649,6226,2,3,30,29,49,31])).
% 60.90/60.93 cnf(6767,plain,
% 60.90/60.93 (~P2(f7(a1,a1,a1,a1,a1),f2(x67671,a12,x67672,x67672),x67673,x67673)),
% 60.90/60.93 inference(scs_inference,[],[6752,6548,6733,6740,6698,6742,6737,5490,6649,6226,6761,2,3,30,29,49,31,35])).
% 60.90/60.93 cnf(6768,plain,
% 60.90/60.93 (~P2(f7(a1,a1,a1,a1,a1),f2(x67681,a12,x67682,x67682),x67683,f2(x67683,x67683,x67684,x67684))),
% 60.90/60.93 inference(rename_variables,[],[6752])).
% 60.90/60.93 cnf(6769,plain,
% 60.90/60.93 (E(x67691,f2(x67692,x67691,x67693,x67693))),
% 60.90/60.93 inference(rename_variables,[],[6226])).
% 60.90/60.93 cnf(6774,plain,
% 60.90/60.93 (~E(f2(x67741,a12,x67742,x67742),f7(a1,a1,a1,a1,a1))),
% 60.90/60.93 inference(scs_inference,[],[6752,6768,6706,6548,6733,6740,6698,6742,6737,5490,6649,6627,6226,6761,6769,2,3,30,29,49,31,35,32,34,73])).
% 60.90/60.93 cnf(6781,plain,
% 60.90/60.93 (~E(f2(x67811,a10,x67812,x67812),f5(a1,a1,a1,a1,a1,a1))),
% 60.90/60.93 inference(scs_inference,[],[6758,2])).
% 60.90/60.93 cnf(6783,plain,
% 60.90/60.93 (E(x67831,f2(x67832,x67831,x67833,x67833))),
% 60.90/60.93 inference(rename_variables,[],[6226])).
% 60.90/60.93 cnf(6784,plain,
% 60.90/60.93 (P1(f5(a1,a1,a1,a1,a1,a1),f7(a1,a1,a1,a1,a1),f5(a1,a1,a1,a1,a1,a1))),
% 60.90/60.93 inference(scs_inference,[],[6758,6723,6221,6649,6226,2,3,29])).
% 60.90/60.93 cnf(6786,plain,
% 60.90/60.93 (~P2(f7(a1,a1,a1,a1,a1),a11,x67861,f2(x67861,x67861,x67862,x67862))),
% 60.90/60.93 inference(scs_inference,[],[6637,6758,6723,6749,6221,6668,6627,6649,6226,2,3,29,30,49])).
% 60.90/60.93 cnf(6790,plain,
% 60.90/60.93 (E(x67901,f2(x67902,x67901,x67903,x67903))),
% 60.90/60.93 inference(rename_variables,[],[6226])).
% 60.90/60.93 cnf(6792,plain,
% 60.90/60.93 (~P2(f7(a1,a1,a1,a1,a1),f2(x67921,a12,x67922,x67922),x67923,x67923)),
% 60.90/60.93 inference(rename_variables,[],[6767])).
% 60.90/60.93 cnf(6795,plain,
% 60.90/60.93 (~P2(f7(a1,a1,a1,a1,a1),a12,x67951,x67951)),
% 60.90/60.93 inference(scs_inference,[],[6637,6767,6792,6758,6723,6541,6749,6221,6668,1609,6627,6649,6226,6783,6790,2,3,29,30,49,31,35,32,33])).
% 60.90/60.93 cnf(6799,plain,
% 60.90/60.93 (E(f5(a1,a1,a1,a1,a1,a1),f7(a1,a1,a1,a1,a1))),
% 60.90/60.93 inference(scs_inference,[],[6637,6767,6792,6758,6723,6541,6749,6221,6668,1609,6627,6649,6226,6783,6790,2,3,29,30,49,31,35,32,33,34,47])).
% 60.90/60.93 cnf(6801,plain,
% 60.90/60.93 (~E(a12,f7(a1,a1,a1,a1,a1))),
% 60.90/60.93 inference(scs_inference,[],[6637,6767,6792,6758,6723,6541,6749,6221,6668,1609,6627,6649,6226,6783,6790,2,3,29,30,49,31,35,32,33,34,47,73])).
% 60.90/60.93 cnf(6817,plain,
% 60.90/60.93 (~P1(f2(x68171,a11,x68172,x68172),f2(x68173,a1,x68174,x68174),f2(x68175,a11,x68176,x68176))),
% 60.90/60.93 inference(scs_inference,[],[6774,6621,6515,6649,6332,2,3,30])).
% 60.90/60.93 cnf(6818,plain,
% 60.90/60.93 (E(f2(x68181,x68182,x68183,x68183),x68182)),
% 60.90/60.93 inference(rename_variables,[],[6332])).
% 60.90/60.93 cnf(6820,plain,
% 60.90/60.93 (E(f2(x68201,x68202,x68203,x68203),x68202)),
% 60.90/60.93 inference(rename_variables,[],[6332])).
% 60.90/60.93 cnf(6824,plain,
% 60.90/60.93 (~P2(f7(a1,a1,a1,a1,a1),a12,f7(a1,a1,a1,a1,a1),f5(a1,a1,a1,a1,a1,a1))),
% 60.90/60.93 inference(scs_inference,[],[6766,6799,6632,6774,6786,6795,6621,6745,6515,6649,6332,6818,2,3,30,29,49,31,35])).
% 60.90/60.93 cnf(6825,plain,
% 60.90/60.93 (~P2(f7(a1,a1,a1,a1,a1),a12,x68251,x68251)),
% 60.90/60.93 inference(rename_variables,[],[6795])).
% 60.90/60.93 cnf(6827,plain,
% 60.90/60.93 (~P2(f7(a1,a1,a1,a1,a1),f2(x68271,a11,x68272,x68272),x68273,f2(x68273,x68273,x68274,x68274))),
% 60.90/60.93 inference(scs_inference,[],[6766,6799,6632,6774,6786,6795,6621,6745,6515,6649,6332,6818,6820,2,3,30,29,49,31,35,32,33])).
% 60.90/60.93 cnf(6829,plain,
% 60.90/60.93 (~P2(f7(a1,a1,a1,a1,a1),a12,f5(a1,a1,a1,a1,a1,a1),f7(a1,a1,a1,a1,a1))),
% 60.90/60.93 inference(scs_inference,[],[6766,6799,6632,6774,6786,6795,6825,6621,6745,6515,6649,6332,6818,6820,2,3,30,29,49,31,35,32,33,34])).
% 60.90/60.93 cnf(6831,plain,
% 60.90/60.93 (~E(a12,f5(a1,a1,a1,a1,a1,a1))),
% 60.90/60.93 inference(scs_inference,[],[6766,6799,6632,6774,6786,6795,6825,6621,6745,6515,6649,6332,6818,6820,2,3,30,29,49,31,35,32,33,34,73])).
% 60.90/60.93 cnf(6840,plain,
% 60.90/60.93 (E(x68401,f2(x68402,x68401,x68403,x68403))),
% 60.90/60.93 inference(rename_variables,[],[6226])).
% 60.90/60.93 cnf(6841,plain,
% 60.90/60.93 (P1(f7(a1,a1,a1,a1,a1),f5(a1,a1,a1,a1,a1,a1),f4(a1,a1,a10,a11,a11))),
% 60.90/60.93 inference(scs_inference,[],[6762,6801,6377,6799,6226,2,3,29])).
% 60.90/60.93 cnf(6847,plain,
% 60.90/60.93 (E(x68471,f2(x68472,x68471,x68473,x68473))),
% 60.90/60.93 inference(rename_variables,[],[6226])).
% 60.90/60.93 cnf(6848,plain,
% 60.90/60.93 (~P2(f7(a1,a1,a1,a1,a1),f2(x68481,a11,x68482,x68482),x68483,x68483)),
% 60.90/60.93 inference(scs_inference,[],[6762,6651,6827,6801,6817,6377,6245,6799,6226,6840,6847,2,3,29,30,49,31,35])).
% 60.90/60.93 cnf(6850,plain,
% 60.90/60.93 (~P2(f5(a1,a1,a1,a1,a1,a1),f2(x68501,a11,x68502,x68502),x68503,f2(x68503,x68503,x68504,x68504))),
% 60.90/60.93 inference(scs_inference,[],[6762,6651,6827,6801,6817,6377,6245,6799,6226,6840,6847,2,3,29,30,49,31,35,32])).
% 60.90/60.93 cnf(6851,plain,
% 60.90/60.93 (~P2(f7(a1,a1,a1,a1,a1),f2(x68511,a11,x68512,x68512),f2(x68513,x68514,x68515,x68515),f2(x68514,x68514,x68516,x68516))),
% 60.90/60.93 inference(scs_inference,[],[6762,6651,6827,6801,6817,6377,6245,6799,6226,6840,6847,6332,2,3,29,30,49,31,35,32,34])).
% 60.90/60.93 cnf(6853,plain,
% 60.90/60.93 (~E(f2(x68531,a11,x68532,x68532),f7(a1,a1,a1,a1,a1))),
% 60.90/60.93 inference(scs_inference,[],[6762,6651,6827,6801,6817,6377,6245,6799,6226,6840,6847,6332,2,3,29,30,49,31,35,32,34,73])).
% 60.90/60.93 cnf(6854,plain,
% 60.90/60.93 (P1(a9,a9,a9)),
% 60.90/60.93 inference(scs_inference,[],[6762,6651,6827,6801,6817,6377,6245,4058,6799,6226,6840,6847,6332,41,2,3,29,30,49,31,35,32,34,73,50])).
% 60.90/60.93 cnf(6868,plain,
% 60.90/60.93 (P1(a9,f7(a9,a9,a9,a9,a9),a9)),
% 60.90/60.93 inference(scs_inference,[],[6854,6853,2,53])).
% 60.90/60.93 cnf(6874,plain,
% 60.90/60.93 (E(x68741,f2(x68742,x68741,x68743,x68743))),
% 60.90/60.93 inference(rename_variables,[],[6226])).
% 60.90/60.93 cnf(6877,plain,
% 60.90/60.93 (E(x68771,f2(x68772,x68771,x68773,x68773))),
% 60.90/60.93 inference(rename_variables,[],[6226])).
% 60.90/60.93 cnf(6878,plain,
% 60.90/60.93 (~P2(a1,a11,f7(a1,a1,a1,a1,a1),f5(a1,a1,a1,a1,a1,a1))),
% 60.90/60.93 inference(scs_inference,[],[6854,6636,6853,6824,6701,6583,6615,6627,6226,6874,2,53,3,29,30,49])).
% 60.90/60.93 cnf(6881,plain,
% 60.90/60.93 (~P2(f5(a1,a1,a1,a1,a1,a1),f2(x68811,a11,x68812,x68812),x68813,x68813)),
% 60.90/60.93 inference(scs_inference,[],[6854,6636,6850,6853,6824,6701,6784,6583,6615,6799,6627,6226,6874,6877,2,53,3,29,30,49,31,35])).
% 60.90/60.93 cnf(6882,plain,
% 60.90/60.93 (~P2(f5(a1,a1,a1,a1,a1,a1),f2(x68821,a11,x68822,x68822),x68823,f2(x68823,x68823,x68824,x68824))),
% 60.90/60.93 inference(rename_variables,[],[6850])).
% 60.90/60.93 cnf(6885,plain,
% 60.90/60.93 (~P2(f7(a1,a1,a1,a1,a1),f2(x68851,a11,x68852,x68852),f5(a1,a1,a1,a1,a1,a1),f7(a1,a1,a1,a1,a1))),
% 60.90/60.93 inference(scs_inference,[],[6854,6636,6850,6882,6848,6853,6824,6701,6784,6583,6615,6799,6627,6649,6226,6874,6877,2,53,3,29,30,49,31,35,32,34])).
% 60.90/60.93 cnf(6889,plain,
% 60.90/60.93 (P2(x68891,x68892,x68891,x68892)),
% 60.90/60.93 inference(rename_variables,[],[63])).
% 60.90/60.93 cnf(6891,plain,
% 60.90/60.93 (P1(a9,f5(a9,a9,a9,a9,a9,a9),a9)),
% 60.90/60.93 inference(scs_inference,[],[6854,6636,6850,6882,6848,6853,6824,6701,6784,6583,6615,6799,6627,6649,63,6889,6226,6874,6877,2,53,3,29,30,49,31,35,32,34,58,57])).
% 60.90/60.93 cnf(6895,plain,
% 60.90/60.93 (E(a9,f7(a9,a9,a9,a9,a9))),
% 60.90/60.93 inference(scs_inference,[],[6854,6636,6850,6882,6848,6853,6824,6701,6784,6583,6615,6799,6627,6649,63,6889,6226,6874,6877,2,53,3,29,30,49,31,35,32,34,58,57,47])).
% 60.90/60.93 cnf(6897,plain,
% 60.90/60.93 (~E(f2(x68971,a11,x68972,x68972),f5(a1,a1,a1,a1,a1,a1))),
% 60.90/60.93 inference(scs_inference,[],[6854,6636,6850,6882,6848,6853,6824,6701,6784,6583,6615,6799,6627,6649,63,6889,6226,6874,6877,2,53,3,29,30,49,31,35,32,34,58,57,47,73])).
% 60.90/60.93 cnf(6898,plain,
% 60.90/60.93 (P1(a10,a10,a10)),
% 60.90/60.93 inference(scs_inference,[],[6854,6636,6850,6882,6848,6853,6824,6701,6784,6583,6615,5135,269,6799,6627,6649,63,6889,6226,6874,6877,2,53,3,29,30,49,31,35,32,34,58,57,47,73,50])).
% 60.90/60.93 cnf(6909,plain,
% 60.90/60.93 (E(a9,f5(a9,a9,a9,a9,a9,a9))),
% 60.90/60.93 inference(scs_inference,[],[6891,47])).
% 60.90/60.93 cnf(6912,plain,
% 60.90/60.93 (P1(a10,f7(a10,a10,a10,a10,a10),a10)),
% 60.90/60.93 inference(scs_inference,[],[6898,6831,6891,47,2,52])).
% 60.90/60.93 cnf(6916,plain,
% 60.90/60.93 (E(f2(x69161,x69162,x69163,x69163),x69162)),
% 60.90/60.93 inference(rename_variables,[],[6332])).
% 60.90/60.93 cnf(6918,plain,
% 60.90/60.93 (P1(f7(a9,a9,a9,a9,a9),f7(a9,a9,a9,a9,a9),a9)),
% 60.90/60.93 inference(scs_inference,[],[6898,6841,6868,6895,6831,6781,6891,6799,6332,47,2,52,3,30,29])).
% 60.90/60.93 cnf(6919,plain,
% 60.90/60.93 (~P2(f5(a1,a1,a1,a1,a1,a1),a12,f7(a1,a1,a1,a1,a1),f5(a1,a1,a1,a1,a1,a1))),
% 60.90/60.93 inference(scs_inference,[],[6898,6841,6652,6868,6895,6831,6781,6891,6878,6799,6332,47,2,52,3,30,29,49])).
% 60.90/60.93 cnf(6921,plain,
% 60.90/60.93 (~P1(a12,f2(a10,a10,x69211,x69211),f2(x69212,a12,x69213,x69213))),
% 60.90/60.93 inference(scs_inference,[],[6898,6841,6652,6868,6895,6831,6781,6891,6878,5150,6799,6332,6916,47,2,52,3,30,29,49,31])).
% 60.90/60.93 cnf(6927,plain,
% 60.90/60.93 (~P2(f5(a1,a1,a1,a1,a1,a1),f2(x69271,a11,x69272,x69272),f2(x69273,x69274,x69275,x69275),f2(x69274,x69274,x69276,x69276))),
% 60.90/60.93 inference(scs_inference,[],[6898,6841,6652,6868,6895,6831,6851,6881,6781,6891,6878,5150,6799,6332,6916,6226,47,2,52,3,30,29,49,31,35,33,32])).
% 60.90/60.93 cnf(6947,plain,
% 60.90/60.93 (E(f2(x69471,x69472,x69473,x69473),x69472)),
% 60.90/60.93 inference(rename_variables,[],[6332])).
% 60.90/60.93 cnf(6949,plain,
% 60.90/60.93 (E(f2(x69491,x69492,x69493,x69493),x69492)),
% 60.90/60.93 inference(rename_variables,[],[6332])).
% 60.90/60.93 cnf(6958,plain,
% 60.90/60.93 (~P2(f2(a1,a1,x69581,x69581),f2(a10,a10,x69582,x69582),f2(a1,a1,x69581,x69581),f2(a10,a10,x69582,x69582))),
% 60.90/60.93 inference(scs_inference,[],[6909,6912,6927,6885,6897,6743,6829,6919,6918,6921,6636,278,6660,6515,5191,5681,5776,492,6649,63,6332,6947,6949,47,2,3,30,29,49,31,35,32,33,34,51])).
% 60.90/60.93 cnf(6977,plain,
% 60.90/60.93 ($false),
% 60.90/60.93 inference(scs_inference,[],[6958,63]),
% 60.90/60.93 ['proof']).
% 60.90/60.93 % SZS output end Proof
% 60.90/60.93 % Total time :60.260000s
%------------------------------------------------------------------------------