%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : GEO016-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 : n027.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:18 EDT 2024
% Result : Unsatisfiable 59.23s 59.25s
% Output : CNFRefutation 59.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GEO016-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 : n027.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 10:00:54 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.20/0.56 start to proof:theBenchmark
% 59.14/59.24 %-------------------------------------------
% 59.14/59.24 % File :CSE---1.7
% 59.14/59.24 % Problem :theBenchmark
% 59.14/59.24 % Transform :cnf
% 59.14/59.24 % Format :tptp:raw
% 59.14/59.24 % Command :java -jar mcs_scs.jar %d %s
% 59.14/59.24
% 59.14/59.24 % Result :Theorem 58.650000s
% 59.14/59.24 % Output :CNFRefutation 58.650000s
% 59.14/59.24 %-------------------------------------------
% 59.23/59.24 %--------------------------------------------------------------------------
% 59.23/59.24 % File : GEO016-2 : TPTP v8.2.0. Released v1.0.0.
% 59.23/59.24 % Domain : Geometry
% 59.23/59.24 % Problem : Equidistance is symmetric within its argument pairs
% 59.23/59.24 % Version : [Qua89] axioms.
% 59.23/59.24 % English : Show that if the distance from A to B equals the distance
% 59.23/59.25 % from C to D, then the distance from B to A equals the
% 59.23/59.25 % distance from C to D.
% 59.23/59.25
% 59.23/59.25 % Refs : [SST83] Schwabbauser et al. (1983), Metamathematische Methoden
% 59.23/59.25 % : [Qua89] Quaife (1989), Automated Development of Tarski's Geome
% 59.23/59.25 % Source : [TPTP]
% 59.23/59.25 % Names :
% 59.23/59.25
% 59.23/59.25 % Status : Unsatisfiable
% 59.23/59.25 % Rating : 0.00 v8.2.0, 0.05 v8.1.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.08 v7.0.0, 0.07 v6.4.0, 0.00 v6.2.0, 0.10 v6.1.0, 0.07 v6.0.0, 0.10 v5.3.0, 0.11 v5.2.0, 0.12 v5.1.0, 0.06 v5.0.0, 0.00 v3.3.0, 0.14 v3.2.0, 0.00 v3.1.0, 0.09 v2.7.0, 0.08 v2.6.0, 0.00 v2.0.0
% 59.23/59.25 % Syntax : Number of clauses : 20 ( 8 unt; 5 nHn; 17 RR)
% 59.23/59.25 % Number of literals : 58 ( 7 equ; 35 neg)
% 59.23/59.25 % Maximal clause size : 8 ( 2 avg)
% 59.23/59.25 % Maximal term depth : 2 ( 1 avg)
% 59.23/59.25 % Number of predicates : 3 ( 2 usr; 0 prp; 2-4 aty)
% 59.23/59.25 % Number of functors : 12 ( 12 usr; 7 con; 0-6 aty)
% 59.23/59.25 % Number of variables : 71 ( 3 sgn)
% 59.23/59.25 % SPC : CNF_UNS_RFO_SEQ_NHN
% 59.23/59.25
% 59.23/59.25 % Comments :
% 59.23/59.25 %--------------------------------------------------------------------------
% 59.23/59.25 %----Include Tarski geometry axioms
% 59.23/59.25 include('Axioms/GEO002-0.ax').
% 59.23/59.25 %--------------------------------------------------------------------------
% 59.23/59.25 cnf(u_to_v_equals_w_to_x,hypothesis,
% 59.23/59.25 equidistant(u,v,w,x) ).
% 59.23/59.25
% 59.23/59.25 cnf(prove_symmetry,negated_conjecture,
% 59.23/59.25 ~ equidistant(v,u,w,x) ).
% 59.23/59.25
% 59.23/59.25 %--------------------------------------------------------------------------
% 59.23/59.25 %-------------------------------------------
% 59.23/59.25 % Proof found
% 59.23/59.25 % SZS status Theorem for theBenchmark
% 59.23/59.25 % SZS output start Proof
% 59.23/59.25 %ClaNum:55(EqnAxiom:35)
% 59.23/59.25 %VarNum:211(SingletonVarNum:71)
% 59.23/59.25 %MaxLitNum:8
% 59.23/59.25 %MaxfuncDepth:1
% 59.23/59.25 %SharedTerms:12
% 59.23/59.25 %goalClause: 43
% 59.23/59.25 %singleGoalClaCount:1
% 59.23/59.25 [36]P1(a1,a10,a11,a12)
% 59.23/59.25 [40]~P2(a6,a8,a9)
% 59.23/59.25 [41]~P2(a8,a9,a6)
% 59.23/59.25 [42]~P2(a9,a6,a8)
% 59.23/59.25 [43]~P1(a10,a1,a11,a12)
% 59.23/59.25 [37]P1(x371,x372,x372,x371)
% 59.23/59.25 [38]P2(x381,x382,f2(x381,x382,x383,x384))
% 59.23/59.25 [39]P1(x391,f2(x392,x391,x393,x394),x393,x394)
% 59.23/59.25 [44]~P2(x441,x442,x441)+E(x441,x442)
% 59.23/59.25 [45]~P1(x451,x452,x453,x453)+E(x451,x452)
% 59.23/59.25 [49]~P2(x495,x491,x494)+~P2(x492,x493,x494)+P2(x491,f7(x492,x493,x494,x491,x495),x492)
% 59.23/59.25 [50]~P2(x505,x504,x503)+~P2(x502,x501,x503)+P2(x501,f7(x502,x501,x503,x504,x505),x505)
% 59.23/59.25 [46]~P1(x465,x466,x461,x462)+P1(x461,x462,x463,x464)+~P1(x465,x466,x463,x464)
% 59.23/59.25 [51]~P2(x514,x512,x513)+~P2(x511,x512,x515)+E(x511,x512)+P2(x511,x513,f3(x511,x514,x512,x513,x515))
% 59.23/59.25 [52]~P2(x523,x522,x524)+~P2(x521,x522,x525)+E(x521,x522)+P2(x521,x523,f4(x521,x523,x522,x524,x525))
% 59.23/59.25 [53]~P2(x533,x532,x534)+~P2(x531,x532,x535)+E(x531,x532)+P2(f4(x531,x533,x532,x534,x535),x535,f3(x531,x533,x532,x534,x535))
% 59.23/59.25 [54]~P2(x543,x544,x545)+~P2(x542,x543,x545)+~P1(x542,x545,x542,x546)+~P1(x542,x543,x542,x541)+P2(x541,f5(x542,x543,x541,x544,x545,x546),x546)
% 59.23/59.25 [55]~P2(x553,x552,x555)+~P2(x551,x553,x555)+~P1(x551,x555,x551,x556)+~P1(x551,x553,x551,x554)+P1(x551,x552,x551,f5(x551,x553,x554,x552,x555,x556))
% 59.23/59.25 [47]P2(x475,x473,x474)+P2(x474,x475,x473)+~P1(x473,x471,x473,x472)+~P1(x475,x471,x475,x472)+~P1(x474,x471,x474,x472)+E(x471,x472)+P2(x473,x474,x475)
% 59.23/59.25 [48]~P2(x481,x482,x483)+~P1(x482,x484,x488,x486)+~P1(x482,x483,x488,x485)+~P1(x481,x484,x487,x486)+~P1(x481,x482,x487,x488)+E(x481,x482)+P1(x483,x484,x485,x486)+~P2(x487,x488,x485)
% 59.23/59.25 %EqnAxiom
% 59.23/59.25 [1]E(x11,x11)
% 59.23/59.25 [2]E(x22,x21)+~E(x21,x22)
% 59.23/59.25 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 59.23/59.25 [4]~E(x41,x42)+E(f2(x41,x43,x44,x45),f2(x42,x43,x44,x45))
% 59.23/59.25 [5]~E(x51,x52)+E(f2(x53,x51,x54,x55),f2(x53,x52,x54,x55))
% 59.23/59.25 [6]~E(x61,x62)+E(f2(x63,x64,x61,x65),f2(x63,x64,x62,x65))
% 59.23/59.25 [7]~E(x71,x72)+E(f2(x73,x74,x75,x71),f2(x73,x74,x75,x72))
% 59.23/59.25 [8]~E(x81,x82)+E(f5(x81,x83,x84,x85,x86,x87),f5(x82,x83,x84,x85,x86,x87))
% 59.23/59.25 [9]~E(x91,x92)+E(f5(x93,x91,x94,x95,x96,x97),f5(x93,x92,x94,x95,x96,x97))
% 59.23/59.25 [10]~E(x101,x102)+E(f5(x103,x104,x101,x105,x106,x107),f5(x103,x104,x102,x105,x106,x107))
% 59.23/59.25 [11]~E(x111,x112)+E(f5(x113,x114,x115,x111,x116,x117),f5(x113,x114,x115,x112,x116,x117))
% 59.23/59.25 [12]~E(x121,x122)+E(f5(x123,x124,x125,x126,x121,x127),f5(x123,x124,x125,x126,x122,x127))
% 59.23/59.25 [13]~E(x131,x132)+E(f5(x133,x134,x135,x136,x137,x131),f5(x133,x134,x135,x136,x137,x132))
% 59.23/59.25 [14]~E(x141,x142)+E(f7(x141,x143,x144,x145,x146),f7(x142,x143,x144,x145,x146))
% 59.23/59.25 [15]~E(x151,x152)+E(f7(x153,x151,x154,x155,x156),f7(x153,x152,x154,x155,x156))
% 59.23/59.25 [16]~E(x161,x162)+E(f7(x163,x164,x161,x165,x166),f7(x163,x164,x162,x165,x166))
% 59.23/59.25 [17]~E(x171,x172)+E(f7(x173,x174,x175,x171,x176),f7(x173,x174,x175,x172,x176))
% 59.23/59.25 [18]~E(x181,x182)+E(f7(x183,x184,x185,x186,x181),f7(x183,x184,x185,x186,x182))
% 59.23/59.25 [19]~E(x191,x192)+E(f3(x191,x193,x194,x195,x196),f3(x192,x193,x194,x195,x196))
% 59.23/59.25 [20]~E(x201,x202)+E(f3(x203,x201,x204,x205,x206),f3(x203,x202,x204,x205,x206))
% 59.23/59.25 [21]~E(x211,x212)+E(f3(x213,x214,x211,x215,x216),f3(x213,x214,x212,x215,x216))
% 59.23/59.25 [22]~E(x221,x222)+E(f3(x223,x224,x225,x221,x226),f3(x223,x224,x225,x222,x226))
% 59.23/59.25 [23]~E(x231,x232)+E(f3(x233,x234,x235,x236,x231),f3(x233,x234,x235,x236,x232))
% 59.23/59.25 [24]~E(x241,x242)+E(f4(x241,x243,x244,x245,x246),f4(x242,x243,x244,x245,x246))
% 59.23/59.25 [25]~E(x251,x252)+E(f4(x253,x251,x254,x255,x256),f4(x253,x252,x254,x255,x256))
% 59.23/59.25 [26]~E(x261,x262)+E(f4(x263,x264,x261,x265,x266),f4(x263,x264,x262,x265,x266))
% 59.23/59.25 [27]~E(x271,x272)+E(f4(x273,x274,x275,x271,x276),f4(x273,x274,x275,x272,x276))
% 59.23/59.25 [28]~E(x281,x282)+E(f4(x283,x284,x285,x286,x281),f4(x283,x284,x285,x286,x282))
% 59.23/59.25 [29]P1(x292,x293,x294,x295)+~E(x291,x292)+~P1(x291,x293,x294,x295)
% 59.23/59.25 [30]P1(x303,x302,x304,x305)+~E(x301,x302)+~P1(x303,x301,x304,x305)
% 59.23/59.25 [31]P1(x313,x314,x312,x315)+~E(x311,x312)+~P1(x313,x314,x311,x315)
% 59.23/59.25 [32]P1(x323,x324,x325,x322)+~E(x321,x322)+~P1(x323,x324,x325,x321)
% 59.23/59.25 [33]P2(x332,x333,x334)+~E(x331,x332)+~P2(x331,x333,x334)
% 59.23/59.25 [34]P2(x343,x342,x344)+~E(x341,x342)+~P2(x343,x341,x344)
% 59.23/59.25 [35]P2(x353,x354,x352)+~E(x351,x352)+~P2(x353,x354,x351)
% 59.23/59.25
% 59.23/59.25 %-------------------------------------------
% 59.23/59.26 cnf(56,plain,
% 59.23/59.26 (P1(a11,a12,a11,a12)),
% 59.23/59.26 inference(scs_inference,[],[36,46])).
% 59.23/59.26 cnf(60,plain,
% 59.23/59.26 (~E(f2(a6,a8,x601,x602),a9)),
% 59.23/59.26 inference(scs_inference,[],[43,36,39,38,40,46,30,35])).
% 59.23/59.26 cnf(61,plain,
% 59.23/59.26 (P2(x611,x612,f2(x611,x612,x613,x614))),
% 59.23/59.26 inference(rename_variables,[],[38])).
% 59.23/59.26 cnf(62,plain,
% 59.23/59.26 (~P1(f2(x621,a10,a11,a12),a1,x622,x622)),
% 59.23/59.26 inference(scs_inference,[],[43,36,39,38,40,46,30,35,45])).
% 59.23/59.26 cnf(64,plain,
% 59.23/59.26 (~P2(f2(x641,a10,a11,a12),a1,f2(x641,a10,a11,a12))),
% 59.23/59.26 inference(scs_inference,[],[43,36,39,38,40,46,30,35,45,44])).
% 59.23/59.26 cnf(66,plain,
% 59.23/59.26 (P1(x661,a10,a11,a12)+~E(a1,x661)),
% 59.23/59.26 inference(scs_inference,[],[43,36,39,38,40,46,30,35,45,44,29])).
% 59.23/59.26 cnf(67,plain,
% 59.23/59.26 (~E(a1,f2(x671,a10,a11,a12))),
% 59.23/59.26 inference(scs_inference,[],[43,36,37,39,38,40,46,30,35,45,44,29,31])).
% 59.23/59.26 cnf(69,plain,
% 59.23/59.26 (P1(a1,a10,a11,x691)+~E(a12,x691)),
% 59.23/59.26 inference(scs_inference,[],[43,36,37,39,38,40,46,30,35,45,44,29,31,32])).
% 59.23/59.26 cnf(70,plain,
% 59.23/59.26 (P2(x701,x702,f2(x703,x702,x704,x705))+~E(x703,x701)),
% 59.23/59.26 inference(scs_inference,[],[43,36,37,39,38,61,40,46,30,35,45,44,29,31,32,33])).
% 59.23/59.26 cnf(76,plain,
% 59.23/59.26 (~P2(a1,f2(x761,a10,a11,a12),a1)),
% 59.23/59.26 inference(scs_inference,[],[67,44])).
% 59.23/59.26 cnf(80,plain,
% 59.23/59.26 (P1(f2(x801,x802,x803,x804),x802,x803,x804)),
% 59.23/59.26 inference(scs_inference,[],[67,37,39,44,45,46])).
% 59.23/59.26 cnf(84,plain,
% 59.23/59.26 (~E(f2(x841,a1,a11,a12),a10)),
% 59.23/59.26 inference(scs_inference,[],[43,67,37,39,44,45,46,29])).
% 59.23/59.26 cnf(85,plain,
% 59.23/59.26 (~E(f2(f2(x851,a10,a11,a12),a1,x852,x853),f2(x851,a10,a11,a12))),
% 59.23/59.26 inference(scs_inference,[],[43,67,37,39,64,38,44,45,46,29,35])).
% 59.23/59.26 cnf(87,plain,
% 59.23/59.26 (P1(a11,a12,x871,a12)+~E(a11,x871)),
% 59.23/59.26 inference(scs_inference,[],[43,67,56,37,39,64,38,44,45,46,29,35,31])).
% 59.23/59.26 cnf(88,plain,
% 59.23/59.26 (P1(a11,a12,a11,x881)+~E(a12,x881)),
% 59.23/59.26 inference(scs_inference,[],[43,67,56,37,39,64,38,44,45,46,29,35,31,32])).
% 59.23/59.26 cnf(89,plain,
% 59.23/59.26 (P1(a11,x891,a11,a12)+~E(a12,x891)),
% 59.23/59.26 inference(scs_inference,[],[43,67,56,37,39,64,38,44,45,46,29,35,31,32,30])).
% 59.23/59.26 cnf(96,plain,
% 59.23/59.26 (~P2(f2(x961,a1,a11,a12),a10,f2(x961,a1,a11,a12))),
% 59.23/59.26 inference(scs_inference,[],[84,44])).
% 59.23/59.26 cnf(100,plain,
% 59.23/59.26 (P1(x1001,x1002,x1001,x1002)),
% 59.23/59.26 inference(scs_inference,[],[80,84,44,45,46])).
% 59.23/59.26 cnf(102,plain,
% 59.23/59.26 (~E(f2(a1,f2(x1021,a10,a11,a12),x1022,x1023),a1)),
% 59.23/59.26 inference(scs_inference,[],[80,84,76,38,44,45,46,35])).
% 59.23/59.26 cnf(103,plain,
% 59.23/59.26 (P2(x1031,x1032,f2(x1031,x1032,x1033,x1034))),
% 59.23/59.26 inference(rename_variables,[],[38])).
% 59.23/59.26 cnf(106,plain,
% 59.23/59.26 (P1(f2(x1061,x1062,x1063,x1064),x1062,x1063,x1064)),
% 59.23/59.26 inference(rename_variables,[],[80])).
% 59.23/59.26 cnf(107,plain,
% 59.23/59.26 (P1(f2(x1071,x1072,x1073,x1074),x1075,x1073,x1074)+~E(x1076,a11)+~E(x1072,x1075)),
% 59.23/59.26 inference(scs_inference,[],[43,80,106,84,76,38,103,44,45,46,35,31,29,30])).
% 59.23/59.26 cnf(109,plain,
% 59.23/59.26 (~P2(f2(a6,a8,x1091,x1092),a9,f2(a6,a8,x1091,x1092))),
% 59.23/59.26 inference(scs_inference,[],[60,44])).
% 59.23/59.26 cnf(111,plain,
% 59.23/59.26 (~P1(f2(f2(x1111,a10,a11,a12),a1,x1112,x1113),f2(x1111,a10,a11,a12),x1114,x1114)),
% 59.23/59.26 inference(scs_inference,[],[85,60,44,45])).
% 59.23/59.26 cnf(113,plain,
% 59.23/59.26 (P1(x1131,x1132,f2(x1133,x1134,x1131,x1132),x1134)),
% 59.23/59.26 inference(scs_inference,[],[80,100,85,60,44,45,46])).
% 59.23/59.27 cnf(116,plain,
% 59.23/59.27 (~E(f2(x1161,a12,a10,a1),a11)),
% 59.23/59.27 inference(scs_inference,[],[43,80,100,85,60,44,45,46,31])).
% 59.23/59.27 cnf(117,plain,
% 59.23/59.27 (~E(f2(f2(x1171,a1,a11,a12),a10,x1172,x1173),f2(x1171,a1,a11,a12))),
% 59.23/59.27 inference(scs_inference,[],[43,80,100,85,96,60,38,44,45,46,31,35])).
% 59.23/59.27 cnf(121,plain,
% 59.23/59.27 (P1(x1211,f2(x1212,x1213,x1214,x1215),x1214,x1215)+~E(x1213,x1211)),
% 59.23/59.27 inference(scs_inference,[],[43,80,100,39,85,96,60,38,44,45,46,31,35,32,29])).
% 59.23/59.27 cnf(122,plain,
% 59.23/59.27 (P1(a1,x1221,a11,a12)+~E(a10,x1221)),
% 59.23/59.27 inference(scs_inference,[],[43,80,100,36,39,85,96,60,38,44,45,46,31,35,32,29,30])).
% 59.23/59.27 cnf(128,plain,
% 59.23/59.27 (~P2(f2(x1281,a12,a10,a1),a11,f2(x1281,a12,a10,a1))),
% 59.23/59.27 inference(scs_inference,[],[116,44])).
% 59.23/59.27 cnf(132,plain,
% 59.23/59.27 (P1(a11,a12,f2(x1321,x1322,a1,a10),x1322)),
% 59.23/59.27 inference(scs_inference,[],[36,113,116,44,45,46])).
% 59.23/59.27 cnf(135,plain,
% 59.23/59.27 (~E(f2(x1351,a10,a11,a12),f2(f2(x1351,a10,a11,a12),a1,x1352,x1353))),
% 59.23/59.27 inference(scs_inference,[],[36,113,116,100,111,44,45,46,29])).
% 59.23/59.27 cnf(138,plain,
% 59.23/59.27 (~E(f2(f2(a6,a8,x1381,x1382),a9,x1383,x1384),f2(a6,a8,x1381,x1382))),
% 59.23/59.27 inference(scs_inference,[],[36,113,116,100,111,109,38,44,45,46,29,35])).
% 59.23/59.27 cnf(141,plain,
% 59.23/59.27 (P1(a1,a10,x1411,a12)+~E(a11,x1411)),
% 59.23/59.27 inference(scs_inference,[],[36,80,113,116,100,111,109,38,44,45,46,29,35,32,31])).
% 59.23/59.27 cnf(154,plain,
% 59.23/59.27 (P1(a11,a12,a1,a10)),
% 59.23/59.27 inference(scs_inference,[],[36,135,100,44,45,46])).
% 59.23/59.27 cnf(157,plain,
% 59.23/59.27 (~E(x1571,f2(x1572,x1571,f2(x1573,a10,a11,a12),a1))),
% 59.23/59.27 inference(scs_inference,[],[36,135,113,100,62,44,45,46,32])).
% 59.23/59.27 cnf(160,plain,
% 59.23/59.27 (~E(f2(f2(x1601,a12,a10,a1),a11,x1602,x1603),f2(x1601,a12,a10,a1))),
% 59.23/59.27 inference(scs_inference,[],[36,135,113,100,62,128,38,44,45,46,32,35])).
% 59.23/59.27 cnf(162,plain,
% 59.23/59.27 (P1(a11,a12,x1621,x1622)+~E(f2(x1623,x1622,a1,a10),x1621)),
% 59.23/59.27 inference(scs_inference,[],[36,135,132,113,100,62,128,38,44,45,46,32,35,31])).
% 59.23/59.27 cnf(175,plain,
% 59.23/59.27 (~P1(x1751,f2(x1752,x1751,f2(x1753,a10,a11,a12),a1),x1754,x1754)),
% 59.23/59.27 inference(scs_inference,[],[157,44,45])).
% 59.23/59.27 cnf(177,plain,
% 59.23/59.27 (P1(x1771,x1772,f2(x1773,x1774,f2(x1775,x1776,x1771,x1772),x1776),x1774)),
% 59.23/59.27 inference(scs_inference,[],[80,157,113,44,45,46])).
% 59.23/59.27 cnf(180,plain,
% 59.23/59.27 (~E(f2(x1801,a12,f2(x1802,x1803,a10,a1),x1803),a11)),
% 59.23/59.27 inference(scs_inference,[],[43,80,157,113,44,45,46,31])).
% 59.23/59.27 cnf(183,plain,
% 59.23/59.27 (P1(a11,a12,a1,x1831)+~E(a10,x1831)),
% 59.23/59.27 inference(scs_inference,[],[43,80,157,154,113,44,45,46,31,29,32])).
% 59.23/59.27 cnf(184,plain,
% 59.23/59.27 (P1(a11,x1841,a1,a10)+~E(a12,x1841)),
% 59.23/59.27 inference(scs_inference,[],[43,80,157,154,113,44,45,46,31,29,32,30])).
% 59.23/59.27 cnf(195,plain,
% 59.23/59.27 (P1(a11,a12,f2(x1951,x1952,f2(x1953,x1954,a1,a10),x1954),x1952)),
% 59.23/59.27 inference(scs_inference,[],[36,177,180,45,46])).
% 59.23/59.27 cnf(198,plain,
% 59.23/59.27 (~E(f2(x1981,x1982,f2(x1983,a10,a11,a12),a1),x1982)),
% 59.23/59.27 inference(scs_inference,[],[36,100,177,180,175,45,46,29])).
% 59.23/59.27 cnf(200,plain,
% 59.23/59.27 (~P1(x2001,f2(x2002,x2001,f2(x2003,a10,a11,a12),a1),x2004,x2004)),
% 59.23/59.27 inference(rename_variables,[],[175])).
% 59.23/59.27 cnf(201,plain,
% 59.23/59.27 (~E(x2011,f2(x2012,f2(x2013,x2011,x2014,x2014),f2(x2015,a10,a11,a12),a1))),
% 59.23/59.27 inference(scs_inference,[],[36,80,100,177,180,175,200,45,46,29,30])).
% 59.23/59.27 cnf(206,plain,
% 59.23/59.27 (P1(a11,a12,x2061,a10)+~E(a1,x2061)),
% 59.23/59.27 inference(scs_inference,[],[36,80,100,177,180,154,175,200,45,46,29,30,44,31])).
% 59.23/59.27 cnf(207,plain,
% 59.23/59.27 (P1(a11,a12,f2(x2071,x2072,a1,a10),x2073)+~E(x2072,x2073)),
% 59.23/59.27 inference(scs_inference,[],[36,80,100,177,180,154,132,175,200,45,46,29,30,44,31,32])).
% 59.23/59.27 cnf(214,plain,
% 59.23/59.27 (~P1(x2141,f2(x2142,f2(x2143,x2141,x2144,x2144),f2(x2145,a10,a11,a12),a1),x2146,x2146)),
% 59.23/59.27 inference(scs_inference,[],[201,45])).
% 59.23/59.27 cnf(216,plain,
% 59.23/59.27 (P1(a11,a12,a10,a1)),
% 59.23/59.27 inference(scs_inference,[],[36,201,37,45,46])).
% 59.23/59.27 cnf(226,plain,
% 59.23/59.27 (~E(f2(x2261,f2(x2262,x2263,x2264,x2264),f2(x2265,a10,a11,a12),a1),x2263)),
% 59.23/59.27 inference(scs_inference,[],[100,198,214,45,32])).
% 59.23/59.27 cnf(229,plain,
% 59.23/59.27 (P1(a11,a12,x2291,a1)+~E(a10,x2291)),
% 59.23/59.27 inference(scs_inference,[],[100,198,216,214,45,32,31])).
% 59.23/59.27 cnf(242,plain,
% 59.23/59.27 (P1(x2421,x2422,x2423,f2(x2424,x2423,x2421,x2422))),
% 59.23/59.27 inference(scs_inference,[],[80,226,37,45,46])).
% 59.23/59.27 cnf(245,plain,
% 59.23/59.27 (~E(f2(x2451,a11,a10,a1),a12)),
% 59.23/59.27 inference(scs_inference,[],[43,80,226,37,45,46,32])).
% 59.23/59.27 cnf(246,plain,
% 59.23/59.27 (~P2(f2(x2461,a11,a10,a1),a12,f2(x2461,a11,a10,a1))),
% 59.23/59.27 inference(scs_inference,[],[43,80,226,37,45,46,32,44])).
% 59.23/59.27 cnf(248,plain,
% 59.23/59.27 (P1(a11,a12,x2481,x2482)+~E(f2(x2483,x2482,f2(x2484,x2485,a1,a10),x2485),x2481)),
% 59.23/59.27 inference(scs_inference,[],[43,80,226,195,37,45,46,32,44,31])).
% 59.23/59.27 cnf(260,plain,
% 59.23/59.27 (P1(x2601,x2602,x2603,f2(x2604,x2603,f2(x2605,x2606,x2601,x2602),x2606))),
% 59.23/59.27 inference(scs_inference,[],[80,242,245,45,46])).
% 59.23/59.27 cnf(263,plain,
% 59.23/59.27 (~E(f2(f2(x2631,a11,a10,a1),a12,x2632,x2633),f2(x2631,a11,a10,a1))),
% 59.23/59.27 inference(scs_inference,[],[80,242,245,38,246,45,46,35])).
% 59.23/59.27 cnf(265,plain,
% 59.23/59.27 (~E(f2(x2651,a11,f2(x2652,x2653,a10,a1),x2653),a12)),
% 59.23/59.27 inference(scs_inference,[],[43,80,242,245,38,246,45,46,35,32])).
% 59.23/59.27 cnf(279,plain,
% 59.23/59.27 (~E(f2(a8,a9,x2791,x2792),a6)),
% 59.23/59.27 inference(scs_inference,[],[265,38,41,45,35])).
% 59.23/59.27 cnf(281,plain,
% 59.23/59.27 (~P2(f2(a8,a9,x2811,x2812),a6,f2(a8,a9,x2811,x2812))),
% 59.23/59.27 inference(scs_inference,[],[265,38,41,45,35,44])).
% 59.23/59.27 cnf(283,plain,
% 59.23/59.27 (P1(x2831,a12,a1,a10)+~E(a11,x2831)),
% 59.23/59.27 inference(scs_inference,[],[154,265,38,41,45,35,44,29])).
% 59.23/59.27 cnf(290,plain,
% 59.23/59.27 (~P1(f2(a6,a8,x2901,x2902),a9,x2903,x2903)),
% 59.23/59.27 inference(scs_inference,[],[60,45])).
% 59.23/59.27 cnf(292,plain,
% 59.23/59.27 (~E(f2(f2(a8,a9,x2921,x2922),a6,x2923,x2924),f2(a8,a9,x2921,x2922))),
% 59.23/59.27 inference(scs_inference,[],[38,60,281,45,35])).
% 59.23/59.27 cnf(295,plain,
% 59.23/59.27 (P1(x2951,x2952,f2(x2953,x2954,x2955,x2956),x2954)+~E(x2955,f2(x2957,x2956,x2951,x2952))),
% 59.23/59.27 inference(scs_inference,[],[80,113,38,60,281,45,35,29,46])).
% 59.23/59.27 cnf(300,plain,
% 59.23/59.27 (~P1(f2(a8,a9,x3001,x3002),a6,x3003,x3003)),
% 59.23/59.27 inference(scs_inference,[],[279,45])).
% 59.23/59.27 cnf(302,plain,
% 59.23/59.27 (~E(f2(a9,a6,x3021,x3022),a8)),
% 59.23/59.27 inference(scs_inference,[],[38,279,42,45,35])).
% 59.23/59.27 cnf(304,plain,
% 59.23/59.27 (~E(a8,a9)),
% 59.23/59.27 inference(scs_inference,[],[80,290,38,279,42,45,35,30])).
% 59.23/59.27 cnf(307,plain,
% 59.23/59.27 (~P2(f2(a9,a6,x3071,x3072),a8,f2(a9,a6,x3071,x3072))),
% 59.23/59.27 inference(scs_inference,[],[80,290,38,279,42,45,35,30,44])).
% 59.23/59.27 cnf(309,plain,
% 59.23/59.27 (P1(a11,a12,a10,x3091)+~E(a1,x3091)),
% 59.23/59.27 inference(scs_inference,[],[80,216,290,38,279,42,45,35,30,44,32])).
% 59.23/59.27 cnf(314,plain,
% 59.23/59.27 (~P2(a8,a9,a8)),
% 59.23/59.27 inference(scs_inference,[],[304,44])).
% 59.23/59.27 cnf(316,plain,
% 59.23/59.27 (~P1(a8,a9,x3161,x3161)),
% 59.23/59.27 inference(scs_inference,[],[304,44,45])).
% 59.23/59.27 cnf(318,plain,
% 59.23/59.27 (~E(f2(f2(a9,a6,x3181,x3182),a8,x3183,x3184),f2(a9,a6,x3181,x3182))),
% 59.23/59.27 inference(scs_inference,[],[304,38,307,44,45,35])).
% 59.23/59.27 cnf(320,plain,
% 59.23/59.27 (~E(a9,a6)),
% 59.23/59.27 inference(scs_inference,[],[80,304,300,38,307,44,45,35,30])).
% 59.23/59.27 cnf(321,plain,
% 59.23/59.27 (P1(f2(x3211,x3212,x3213,x3214),x3212,x3213,x3214)),
% 59.23/59.27 inference(rename_variables,[],[80])).
% 59.23/59.27 cnf(324,plain,
% 59.23/59.27 (P1(x3241,x3242,x3243,f2(x3244,x3243,x3245,x3246))+~E(x3245,f2(x3247,x3246,x3241,x3242))),
% 59.23/59.27 inference(scs_inference,[],[80,321,242,304,300,38,307,44,45,35,30,29,46])).
% 59.23/59.27 cnf(330,plain,
% 59.23/59.27 (~P2(a9,a6,a9)),
% 59.23/59.27 inference(scs_inference,[],[320,44])).
% 59.23/59.27 cnf(334,plain,
% 59.23/59.27 (~E(f2(a8,a9,x3341,x3342),a8)),
% 59.23/59.27 inference(scs_inference,[],[320,38,314,44,45,35])).
% 59.23/59.27 cnf(336,plain,
% 59.23/59.27 (P1(x3361,a12,a10,a1)+~E(a11,x3361)),
% 59.23/59.27 inference(scs_inference,[],[216,320,38,314,44,45,35,29])).
% 59.23/59.27 cnf(342,plain,
% 59.23/59.27 (~P2(f2(a8,a9,x3421,x3422),a8,f2(a8,a9,x3421,x3422))),
% 59.23/59.27 inference(scs_inference,[],[334,44])).
% 59.23/59.27 cnf(344,plain,
% 59.23/59.27 (~P1(f2(f2(a6,a8,x3441,x3442),a9,x3443,x3444),f2(a6,a8,x3441,x3442),x3445,x3445)),
% 59.23/59.27 inference(scs_inference,[],[138,334,44,45])).
% 59.23/59.27 cnf(346,plain,
% 59.23/59.27 (~E(f2(a9,a6,x3461,x3462),a9)),
% 59.23/59.27 inference(scs_inference,[],[38,138,334,330,44,45,35])).
% 59.23/59.27 cnf(354,plain,
% 59.23/59.27 (~P2(f2(a9,a6,x3541,x3542),a9,f2(a9,a6,x3541,x3542))),
% 59.23/59.27 inference(scs_inference,[],[346,44])).
% 59.23/59.27 cnf(356,plain,
% 59.23/59.27 (~P1(f2(f2(a8,a9,x3561,x3562),a6,x3563,x3564),f2(a8,a9,x3561,x3562),x3565,x3565)),
% 59.23/59.27 inference(scs_inference,[],[292,346,44,45])).
% 59.23/59.27 cnf(358,plain,
% 59.23/59.27 (~E(f2(a6,a8,x3581,x3582),f2(f2(a6,a8,x3581,x3582),a9,x3583,x3584))),
% 59.23/59.27 inference(scs_inference,[],[100,344,292,346,44,45,32])).
% 59.23/59.27 cnf(361,plain,
% 59.23/59.27 (~E(f2(f2(a8,a9,x3611,x3612),a8,x3613,x3614),f2(a8,a9,x3611,x3612))),
% 59.23/59.27 inference(scs_inference,[],[100,344,38,292,342,346,44,45,32,35])).
% 59.23/59.27 cnf(376,plain,
% 59.23/59.27 (~E(f2(a8,a9,x3761,x3762),f2(f2(a8,a9,x3761,x3762),a6,x3763,x3764))),
% 59.23/59.27 inference(scs_inference,[],[100,358,356,44,45,32])).
% 59.23/59.27 cnf(379,plain,
% 59.23/59.27 (~E(f2(f2(a9,a6,x3791,x3792),a9,x3793,x3794),f2(a9,a6,x3791,x3792))),
% 59.23/59.27 inference(scs_inference,[],[100,358,356,38,354,44,45,32,35])).
% 59.23/59.27 cnf(394,plain,
% 59.23/59.27 (P1(a11,x3941,a10,a1)+~E(a12,x3941)),
% 59.23/59.27 inference(scs_inference,[],[216,376,44,45,30])).
% 59.23/59.27 cnf(451,plain,
% 59.23/59.27 (~P1(f2(f2(a9,a6,x4511,x4512),a8,x4513,x4514),f2(a9,a6,x4511,x4512),x4515,x4515)),
% 59.23/59.27 inference(scs_inference,[],[318,45])).
% 59.23/59.27 cnf(459,plain,
% 59.23/59.27 (~P1(f2(a9,a6,x4591,x4592),a8,x4593,x4593)),
% 59.23/59.27 inference(scs_inference,[],[302,45])).
% 59.23/59.27 cnf(461,plain,
% 59.23/59.27 (P1(a11,a12,x4611,f2(x4612,x4611,a1,a10))),
% 59.23/59.27 inference(scs_inference,[],[36,242,302,45,46])).
% 59.23/59.27 cnf(464,plain,
% 59.23/59.27 (~E(f2(a9,a6,x4641,x4642),f2(f2(a9,a6,x4641,x4642),a8,x4643,x4644))),
% 59.23/59.27 inference(scs_inference,[],[36,242,37,451,302,45,46,31])).
% 59.23/59.27 cnf(466,plain,
% 59.23/59.27 (~P1(f2(f2(a9,a6,x4661,x4662),a8,x4663,x4664),f2(a9,a6,x4661,x4662),x4665,x4665)),
% 59.23/59.27 inference(rename_variables,[],[451])).
% 59.23/59.27 cnf(469,plain,
% 59.23/59.27 (~P1(f2(f2(a9,a6,x4691,x4692),a8,x4693,x4694),f2(a9,a6,x4691,x4692),x4695,x4695)),
% 59.23/59.27 inference(rename_variables,[],[451])).
% 59.23/59.27 cnf(470,plain,
% 59.23/59.27 (~E(a8,f2(a9,a6,x4701,x4702))),
% 59.23/59.27 inference(scs_inference,[],[36,80,242,37,39,451,466,469,302,45,46,31,29,30])).
% 59.23/59.27 cnf(483,plain,
% 59.23/59.27 (P1(a11,a12,x4831,f2(x4832,x4831,f2(x4833,x4834,a1,a10),x4834))),
% 59.23/59.27 inference(scs_inference,[],[36,260,464,44,45,46])).
% 59.23/59.27 cnf(486,plain,
% 59.23/59.27 (P1(a11,a12,x4861,f2(x4862,x4863,a1,a10))+~E(x4863,x4861)),
% 59.23/59.27 inference(scs_inference,[],[36,260,464,461,44,45,46,31])).
% 59.23/59.27 cnf(493,plain,
% 59.23/59.27 (~P2(a8,f2(a9,a6,x4931,x4932),a8)),
% 59.23/59.27 inference(scs_inference,[],[470,44])).
% 59.23/59.27 cnf(525,plain,
% 59.23/59.27 (~P1(f2(a8,a9,x5251,x5252),a8,x5253,x5253)),
% 59.23/59.27 inference(scs_inference,[],[334,45])).
% 59.23/59.27 cnf(527,plain,
% 59.23/59.27 (~E(a6,a8)),
% 59.23/59.27 inference(scs_inference,[],[80,459,334,45,30])).
% 59.23/59.27 cnf(530,plain,
% 59.23/59.27 (~P2(a6,a8,a6)),
% 59.23/59.27 inference(scs_inference,[],[80,459,334,45,30,44])).
% 59.23/59.27 cnf(542,plain,
% 59.23/59.27 (~E(a9,a8)),
% 59.23/59.27 inference(scs_inference,[],[80,527,525,45,30])).
% 59.23/59.27 cnf(545,plain,
% 59.23/59.27 (~P2(a9,a8,a9)),
% 59.23/59.27 inference(scs_inference,[],[80,527,525,45,30,44])).
% 59.23/59.27 cnf(556,plain,
% 59.23/59.27 (~E(f2(a6,a8,x5561,x5562),a6)),
% 59.23/59.27 inference(scs_inference,[],[542,38,530,45,35])).
% 59.23/59.27 cnf(558,plain,
% 59.23/59.27 (~P2(f2(a6,a8,x5581,x5582),a6,f2(a6,a8,x5581,x5582))),
% 59.23/59.27 inference(scs_inference,[],[542,38,530,45,35,44])).
% 59.23/59.27 cnf(566,plain,
% 59.23/59.27 (~P1(f2(a9,a6,x5661,x5662),a9,x5663,x5663)),
% 59.23/59.27 inference(scs_inference,[],[346,45])).
% 59.23/59.27 cnf(570,plain,
% 59.23/59.27 (~P2(f2(a9,a8,x5701,x5702),a9,f2(a9,a8,x5701,x5702))),
% 59.23/59.27 inference(scs_inference,[],[38,346,545,45,35,44])).
% 59.23/59.27 cnf(581,plain,
% 59.23/59.27 (~P1(f2(f2(a8,a9,x5811,x5812),a8,x5813,x5814),f2(a8,a9,x5811,x5812),x5815,x5815)),
% 59.23/59.27 inference(scs_inference,[],[361,45])).
% 59.23/59.27 cnf(583,plain,
% 59.23/59.27 (~E(f2(f2(a6,a8,x5831,x5832),a6,x5833,x5834),f2(a6,a8,x5831,x5832))),
% 59.23/59.27 inference(scs_inference,[],[38,361,558,45,35])).
% 59.23/59.27 cnf(585,plain,
% 59.23/59.27 (~E(a6,a9)),
% 59.23/59.27 inference(scs_inference,[],[80,566,38,361,558,45,35,30])).
% 59.23/59.27 cnf(588,plain,
% 59.23/59.27 (~P2(a6,a9,a6)),
% 59.23/59.27 inference(scs_inference,[],[80,566,38,361,558,45,35,30,44])).
% 59.23/59.27 cnf(591,plain,
% 59.23/59.27 (~P1(a6,a9,x5911,x5911)),
% 59.23/59.27 inference(scs_inference,[],[585,45])).
% 59.23/59.27 cnf(593,plain,
% 59.23/59.27 (~E(f2(f2(a9,a8,x5931,x5932),a9,x5933,x5934),f2(a9,a8,x5931,x5932))),
% 59.23/59.27 inference(scs_inference,[],[585,38,570,45,35])).
% 59.23/59.27 cnf(595,plain,
% 59.23/59.27 (~E(f2(a8,a9,x5951,x5952),f2(f2(a8,a9,x5951,x5952),a8,x5953,x5954))),
% 59.23/59.27 inference(scs_inference,[],[585,37,581,38,570,45,35,31])).
% 59.23/59.27 cnf(611,plain,
% 59.23/59.27 (~E(f2(a6,a9,x6111,x6112),a6)),
% 59.23/59.27 inference(scs_inference,[],[595,38,588,44,45,35])).
% 59.23/59.27 cnf(632,plain,
% 59.23/59.27 (~P1(f2(f2(a9,a6,x6321,x6322),a9,x6323,x6324),f2(a9,a6,x6321,x6322),x6325,x6325)),
% 59.23/59.27 inference(scs_inference,[],[379,45])).
% 59.23/59.27 cnf(635,plain,
% 59.23/59.27 (~P1(f2(f2(a6,a8,x6351,x6352),a6,x6353,x6354),f2(a6,a8,x6351,x6352),x6355,x6355)),
% 59.23/59.27 inference(scs_inference,[],[583,45])).
% 59.23/59.27 cnf(637,plain,
% 59.23/59.27 (~E(f2(a9,a6,x6371,x6372),f2(f2(a9,a6,x6371,x6372),a9,x6373,x6374))),
% 59.23/59.27 inference(scs_inference,[],[37,632,583,45,31])).
% 59.23/59.27 cnf(655,plain,
% 59.23/59.27 (~P1(f2(f2(a6,a8,x6551,x6552),a6,x6553,x6554),f2(a6,a8,x6551,x6552),x6555,x6555)),
% 59.23/59.27 inference(rename_variables,[],[635])).
% 59.23/59.27 cnf(658,plain,
% 59.23/59.27 (~P1(f2(f2(a6,a8,x6581,x6582),a6,x6583,x6584),f2(a6,a8,x6581,x6582),x6585,x6585)),
% 59.23/59.27 inference(rename_variables,[],[635])).
% 59.23/59.27 cnf(659,plain,
% 59.23/59.27 (~E(a6,f2(a6,a8,x6591,x6592))),
% 59.23/59.27 inference(scs_inference,[],[80,637,37,39,635,655,658,44,45,31,29,30])).
% 59.23/59.27 cnf(681,plain,
% 59.23/59.27 (~P1(a6,f2(a6,a8,x6811,x6812),x6813,x6813)),
% 59.23/59.27 inference(scs_inference,[],[659,44,45])).
% 59.23/59.27 cnf(694,plain,
% 59.23/59.27 (~P1(f2(f2(a9,a8,x6941,x6942),a9,x6943,x6944),f2(a9,a8,x6941,x6942),x6945,x6945)),
% 59.23/59.27 inference(scs_inference,[],[593,45])).
% 59.23/59.27 cnf(700,plain,
% 59.23/59.27 (~P1(f2(f2(x7001,a1,a11,a12),a10,x7002,x7003),f2(x7001,a1,a11,a12),x7004,x7004)),
% 59.23/59.27 inference(scs_inference,[],[117,45])).
% 59.23/59.27 cnf(702,plain,
% 59.23/59.27 (~E(f2(a9,a8,x7021,x7022),f2(f2(a9,a8,x7021,x7022),a9,x7023,x7024))),
% 59.23/59.27 inference(scs_inference,[],[100,694,117,45,32])).
% 59.23/59.27 cnf(721,plain,
% 59.23/59.27 (~E(f2(x7211,a1,a11,a12),f2(f2(x7211,a1,a11,a12),a10,x7212,x7213))),
% 59.23/59.27 inference(scs_inference,[],[702,37,700,44,45,31])).
% 59.23/59.27 cnf(736,plain,
% 59.23/59.27 (P1(f2(x7361,x7362,f2(x7363,x7364,x7365,x7366),x7364),x7362,x7365,x7366)),
% 59.23/59.27 inference(scs_inference,[],[113,80,721,44,45,46])).
% 59.23/59.27 cnf(780,plain,
% 59.23/59.27 (P1(f2(x7801,x7802,x7803,f2(x7804,x7803,x7805,x7806)),x7802,x7805,x7806)),
% 59.23/59.27 inference(scs_inference,[],[113,39,160,45,46])).
% 59.23/59.27 cnf(824,plain,
% 59.23/59.27 (~P1(f2(a6,a8,x8241,x8242),a6,x8243,x8243)),
% 59.23/59.27 inference(scs_inference,[],[556,45])).
% 59.23/59.27 cnf(837,plain,
% 59.23/59.27 (~P1(f2(a6,a9,x8371,x8372),a6,x8373,x8373)),
% 59.23/59.27 inference(scs_inference,[],[611,45])).
% 59.23/59.27 cnf(843,plain,
% 59.23/59.27 (~P1(f2(f2(x8431,a11,a10,a1),a12,x8432,x8433),f2(x8431,a11,a10,a1),x8434,x8434)),
% 59.23/59.27 inference(scs_inference,[],[263,45])).
% 59.23/59.27 cnf(854,plain,
% 59.23/59.27 (~P1(f2(f2(x8541,a11,a10,a1),a12,x8542,x8543),f2(x8541,a11,a10,a1),x8544,x8544)),
% 59.23/59.27 inference(rename_variables,[],[843])).
% 59.23/59.27 cnf(855,plain,
% 59.23/59.27 (~E(a12,f2(x8551,a11,a10,a1))),
% 59.23/59.27 inference(scs_inference,[],[100,80,843,854,102,45,32,30])).
% 59.23/59.27 cnf(912,plain,
% 59.23/59.27 (P1(f2(x9121,x9122,f2(x9123,x9124,a1,a10),x9124),x9122,f2(x9125,x9126,a1,a10),x9126)),
% 59.23/59.27 inference(scs_inference,[],[195,132,46])).
% 59.23/59.27 cnf(922,plain,
% 59.23/59.27 (P1(f2(x9221,x9222,f2(x9223,x9224,a1,a10),x9224),x9222,x9225,f2(x9226,x9225,a1,a10))),
% 59.23/59.27 inference(scs_inference,[],[195,461,46])).
% 59.23/59.27 cnf(947,plain,
% 59.23/59.27 (P1(f2(x9471,x9472,a1,a10),x9472,x9473,f2(x9474,x9473,f2(x9475,x9476,a1,a10),x9476))),
% 59.23/59.27 inference(scs_inference,[],[132,483,46])).
% 59.23/59.27 cnf(960,plain,
% 59.23/59.27 (P1(f2(x9601,x9602,a1,a10),x9602,x9603,f2(x9604,x9603,a1,a10))),
% 59.23/59.27 inference(scs_inference,[],[132,461,46])).
% 59.23/59.27 cnf(962,plain,
% 59.23/59.27 (P1(f2(x9621,x9622,a1,a10),x9622,x9623,f2(x9624,x9625,a1,a10))+~E(x9625,x9623)),
% 59.23/59.27 inference(scs_inference,[],[132,461,46,31])).
% 59.23/59.27 cnf(1007,plain,
% 59.23/59.27 (P1(f2(x10071,x10072,a1,a10),x10073,x10074,f2(x10075,x10074,a1,a10))+~E(x10072,x10073)),
% 59.23/59.27 inference(scs_inference,[],[960,29,30])).
% 59.23/59.27 cnf(1050,plain,
% 59.23/59.27 (P1(f2(x10501,x10502,a1,a10),x10502,f2(x10503,x10504,a11,a12),x10504)),
% 59.23/59.27 inference(scs_inference,[],[132,113,46])).
% 59.23/59.27 cnf(1064,plain,
% 59.23/59.27 (P1(f2(x10641,x10642,a1,a10),x10642,f2(x10643,x10644,f2(x10645,x10646,a11,a12),x10646),x10644)),
% 59.23/59.27 inference(scs_inference,[],[132,177,46])).
% 59.23/59.27 cnf(1076,plain,
% 59.23/59.27 (P1(f2(x10761,x10762,a1,a10),x10762,a11,a12)),
% 59.23/59.27 inference(scs_inference,[],[132,100,46])).
% 59.23/59.27 cnf(1085,plain,
% 59.23/59.27 (P1(f2(x10851,x10852,a1,a10),x10852,f2(x10853,x10854,a11,a12),x10855)+~E(x10854,x10855)),
% 59.23/59.27 inference(scs_inference,[],[43,132,100,1050,46,29,44,45,31,32])).
% 59.23/59.27 cnf(1086,plain,
% 59.23/59.27 (P1(f2(x10861,x10862,a1,a10),x10863,f2(x10864,x10865,a11,a12),x10865)+~E(x10862,x10863)),
% 59.23/59.27 inference(scs_inference,[],[43,132,100,1050,46,29,44,45,31,32,30])).
% 59.23/59.27 cnf(1093,plain,
% 59.23/59.27 (P1(f2(x10931,x10932,a1,a10),x10932,x10933,f2(x10934,x10933,f2(x10935,x10936,a11,a12),x10936))),
% 59.23/59.27 inference(scs_inference,[],[132,260,46])).
% 59.23/59.27 cnf(1107,plain,
% 59.23/59.27 (P1(f2(x11071,x11072,a1,a10),x11072,x11073,f2(x11074,x11073,a11,a12))),
% 59.23/59.27 inference(scs_inference,[],[132,242,46])).
% 59.23/59.27 cnf(1122,plain,
% 59.23/59.27 (P1(f2(x11221,x11222,f2(x11223,x11224,a1,a10),x11224),x11222,f2(x11225,x11226,a11,a12),x11226)),
% 59.23/59.27 inference(scs_inference,[],[113,1050,46])).
% 59.23/59.27 cnf(1126,plain,
% 59.23/59.27 (P1(f2(x11261,x11262,a1,a10),x11262,x11263,f2(x11264,x11265,a11,a12))+~E(x11265,x11263)),
% 59.23/59.27 inference(scs_inference,[],[113,1050,1107,46,31])).
% 59.23/59.27 cnf(1129,plain,
% 59.23/59.27 (P1(f2(x11291,x11292,a1,a10),x11293,a11,a12)+~E(x11292,x11293)),
% 59.23/59.27 inference(scs_inference,[],[113,1050,1076,1064,1107,46,31,32,29,30])).
% 59.23/59.27 cnf(1134,plain,
% 59.23/59.27 (P1(f2(x11341,x11342,f2(x11343,x11344,a1,a10),x11344),x11342,a11,a12)),
% 59.23/59.27 inference(scs_inference,[],[113,1076,46])).
% 59.23/59.27 cnf(1139,plain,
% 59.23/59.27 (~P1(f2(x11391,a1,f2(x11392,x11393,a1,a10),x11393),a10,x11394,x11394)),
% 59.23/59.27 inference(scs_inference,[],[43,113,1076,46,29,45])).
% 59.23/59.27 cnf(1142,plain,
% 59.23/59.27 (P1(f2(x11421,x11422,f2(x11423,x11424,a1,a10),x11424),x11422,f2(x11425,x11426,a11,a12),x11427)+~E(x11426,x11427)),
% 59.23/59.27 inference(scs_inference,[],[43,113,1076,1122,46,29,45,31,32])).
% 59.23/59.27 cnf(1150,plain,
% 59.23/59.27 (P1(f2(x11501,x11502,f2(x11503,x11504,a1,a10),x11504),x11502,x11505,f2(x11506,x11505,a11,a12))),
% 59.23/59.27 inference(scs_inference,[],[113,1107,46])).
% 59.23/59.27 cnf(1155,plain,
% 59.23/59.27 (~E(a1,a10)+~E(a11,a12)),
% 59.23/59.27 inference(scs_inference,[],[113,1134,1107,1139,46,31,30])).
% 59.23/59.27 cnf(1159,plain,
% 59.23/59.27 (~P1(a1,a10,x11591,x11591)+~E(a11,a12)),
% 59.23/59.27 inference(scs_inference,[],[113,1134,1107,1139,46,31,30,44,45])).
% 59.23/59.27 cnf(1163,plain,
% 59.23/59.27 (P1(f2(x11631,x11632,a1,a10),x11632,a12,a11)),
% 59.23/59.27 inference(scs_inference,[],[132,37,46])).
% 59.23/59.27 cnf(1174,plain,
% 59.23/59.27 (P1(f2(x11741,x11742,f2(x11743,x11744,a1,a10),x11744),x11742,a12,a11)),
% 59.23/59.27 inference(scs_inference,[],[113,1163,46])).
% 59.23/59.27 cnf(1175,plain,
% 59.23/59.27 (P1(f2(x11751,x11752,a1,a10),x11752,a12,a11)),
% 59.23/59.27 inference(rename_variables,[],[1163])).
% 59.23/59.27 cnf(1181,plain,
% 59.23/59.27 (P1(f2(x11811,x11812,a1,a10),x11813,a12,a11)+~E(x11812,x11813)),
% 59.23/59.27 inference(scs_inference,[],[113,1163,1175,46,31,32,29,30])).
% 59.23/59.27 cnf(1208,plain,
% 59.23/59.27 (~E(a12,a11)+~E(a1,a10)),
% 59.23/59.27 inference(scs_inference,[],[1155,2])).
% 59.23/59.27 cnf(1231,plain,
% 59.23/59.27 (P1(f2(x12311,x12312,a1,a10),x12313,x12314,f2(x12315,x12314,a11,a12))+~E(x12312,x12313)),
% 59.23/59.27 inference(scs_inference,[],[1107,29,30])).
% 59.23/59.27 cnf(1284,plain,
% 59.23/59.27 (~P1(a1,a10,x12841,x12841)+~E(a12,a11)),
% 59.23/59.27 inference(scs_inference,[],[1208,45])).
% 59.23/59.27 cnf(1381,plain,
% 59.23/59.27 (P1(x13811,f2(x13812,x13811,a1,a10),x13813,f2(x13814,x13813,f2(x13815,x13816,a1,a10),x13816))),
% 59.23/59.27 inference(scs_inference,[],[960,947,46])).
% 59.23/59.27 cnf(1395,plain,
% 59.23/59.27 (P1(x13951,f2(x13952,x13951,a1,a10),f2(x13953,x13954,a11,a12),x13954)),
% 59.23/59.27 inference(scs_inference,[],[960,1050,46])).
% 59.23/59.27 cnf(1399,plain,
% 59.23/59.27 (P1(x13991,f2(x13992,x13991,a1,a10),f2(x13993,x13994,a11,a12),x13995)+~E(x13994,x13995)),
% 59.23/59.27 inference(scs_inference,[],[960,1050,1381,46,31,32])).
% 59.23/59.27 cnf(1410,plain,
% 59.23/59.27 (P1(x14101,f2(x14102,x14101,a1,a10),f2(x14103,x14104,f2(x14105,x14106,a11,a12),x14106),x14104)),
% 59.23/59.27 inference(scs_inference,[],[960,1064,46])).
% 59.23/59.27 cnf(1416,plain,
% 59.23/59.27 (P1(x14161,f2(x14162,x14163,a1,a10),f2(x14164,x14165,a11,a12),x14165)+~E(x14163,x14161)),
% 59.23/59.27 inference(scs_inference,[],[960,1064,1395,46,32,31,30,29])).
% 59.23/59.27 cnf(1424,plain,
% 59.23/59.27 (P1(x14241,f2(x14242,x14241,a1,a10),a12,a11)),
% 59.23/59.27 inference(scs_inference,[],[960,1163,46])).
% 59.23/59.27 cnf(1438,plain,
% 59.23/59.27 (P1(x14381,f2(x14382,x14381,a1,a10),x14383,f2(x14384,x14383,a11,a12))),
% 59.23/59.27 inference(scs_inference,[],[960,1107,46])).
% 59.23/59.27 cnf(1444,plain,
% 59.23/59.27 (P1(x14441,f2(x14442,x14443,a1,a10),a12,a11)+~E(x14443,x14441)),
% 59.23/59.27 inference(scs_inference,[],[960,1107,1424,46,32,30,31,29])).
% 59.23/59.27 cnf(1452,plain,
% 59.23/59.28 (P1(x14521,f2(x14522,x14521,a1,a10),a11,a12)),
% 59.23/59.28 inference(scs_inference,[],[960,1076,46])).
% 59.23/59.28 cnf(1470,plain,
% 59.23/59.28 (P1(x14701,f2(x14702,x14701,a1,a10),a11,a12)),
% 59.23/59.28 inference(rename_variables,[],[1452])).
% 59.23/59.28 cnf(1477,plain,
% 59.23/59.28 (P1(x14771,f2(x14772,x14773,a1,a10),a11,a12)+~E(x14773,x14771)),
% 59.23/59.28 inference(scs_inference,[],[43,960,1093,1452,1470,46,30,44,45,31,32,29])).
% 59.23/59.28 cnf(1485,plain,
% 59.23/59.28 (P1(a1,a10,f2(x14851,x14852,a11,a12),x14852)),
% 59.23/59.28 inference(scs_inference,[],[736,1122,46])).
% 59.23/59.28 cnf(1501,plain,
% 59.23/59.28 (P1(a1,a10,x15011,f2(x15012,x15011,a11,a12))),
% 59.23/59.28 inference(scs_inference,[],[736,1150,46])).
% 59.23/59.28 cnf(1505,plain,
% 59.23/59.28 (P1(a1,a10,f2(x15051,x15052,a11,a12),x15053)+~E(x15052,x15053)),
% 59.23/59.28 inference(scs_inference,[],[736,1150,1485,46,32])).
% 59.23/59.28 cnf(1522,plain,
% 59.23/59.28 (P1(a1,a10,a12,a11)),
% 59.23/59.28 inference(scs_inference,[],[736,1174,46])).
% 59.23/59.28 cnf(1539,plain,
% 59.23/59.28 (P1(f2(x15391,x15392,x15393,f2(x15394,x15393,a1,a10)),x15392,f2(x15395,x15396,a11,a12),x15396)),
% 59.23/59.28 inference(scs_inference,[],[113,1395,46])).
% 59.23/59.28 cnf(1543,plain,
% 59.23/59.28 (P1(a1,a10,a12,x15431)+~E(a11,x15431)),
% 59.23/59.28 inference(scs_inference,[],[113,1395,1522,46,32])).
% 59.23/59.28 cnf(1546,plain,
% 59.23/59.28 (~E(a11,a12)),
% 59.23/59.28 inference(scs_inference,[],[113,1395,1522,46,32,1284,1159])).
% 59.23/59.28 cnf(1555,plain,
% 59.23/59.28 (~P1(a11,a12,x15551,x15551)),
% 59.23/59.28 inference(scs_inference,[],[1546,44,45])).
% 59.23/59.28 cnf(1557,plain,
% 59.23/59.28 (~E(x15571,f2(x15572,x15571,a1,a10))),
% 59.23/59.28 inference(scs_inference,[],[132,1546,44,45,32])).
% 59.23/59.28 cnf(1558,plain,
% 59.23/59.28 (~E(f2(x15581,f2(x15582,x15583,a1,a10),f2(x15584,x15585,a1,a10),x15585),f2(x15582,x15583,a1,a10))),
% 59.23/59.28 inference(scs_inference,[],[132,195,1546,44,45,32,31])).
% 59.23/59.28 cnf(1561,plain,
% 59.23/59.28 (~E(f2(x15611,x15612,a1,a10),x15612)),
% 59.23/59.28 inference(scs_inference,[],[132,195,1546,44,45,32,31,162,5])).
% 59.23/59.28 cnf(1570,plain,
% 59.23/59.28 (~E(a12,a11)),
% 59.23/59.28 inference(scs_inference,[],[1555,88])).
% 59.23/59.28 cnf(1571,plain,
% 59.23/59.28 (~P1(a11,a12,x15711,x15711)),
% 59.23/59.28 inference(rename_variables,[],[1555])).
% 59.23/59.28 cnf(1572,plain,
% 59.23/59.28 (~E(a10,a1)),
% 59.23/59.28 inference(scs_inference,[],[1555,1571,88,183])).
% 59.23/59.28 cnf(1573,plain,
% 59.23/59.28 (~P1(a11,a12,x15731,x15731)),
% 59.23/59.28 inference(rename_variables,[],[1555])).
% 59.23/59.28 cnf(1574,plain,
% 59.23/59.28 (~E(a1,a10)),
% 59.23/59.28 inference(scs_inference,[],[1555,1571,1573,88,183,206])).
% 59.23/59.28 cnf(1575,plain,
% 59.23/59.28 (~P1(a11,a12,x15751,x15751)),
% 59.23/59.28 inference(rename_variables,[],[1555])).
% 59.23/59.28 cnf(1576,plain,
% 59.23/59.28 (~E(f2(x15761,x15762,f2(x15763,x15764,a1,a10),x15764),x15762)),
% 59.23/59.28 inference(scs_inference,[],[1555,1571,1573,1575,88,183,206,248])).
% 59.23/59.28 cnf(1581,plain,
% 59.23/59.28 (~E(x15811,f2(x15812,x15811,f2(x15813,x15814,a1,a10),x15814))),
% 59.23/59.28 inference(scs_inference,[],[195,1558,1557,1555,1571,1573,1575,88,183,206,248,44,45,32])).
% 59.23/59.28 cnf(1583,plain,
% 59.23/59.28 (~E(f2(x15831,x15832,a11,a12),x15832)),
% 59.23/59.28 inference(scs_inference,[],[195,1122,1558,1557,1555,1571,1573,1575,88,183,206,248,44,45,32,31])).
% 59.23/59.28 cnf(1585,plain,
% 59.23/59.28 (~E(x15851,f2(x15852,x15851,a11,a12))),
% 59.23/59.28 inference(scs_inference,[],[195,1122,1558,1557,1555,1571,1573,1575,88,183,206,248,44,45,32,31,1142])).
% 59.23/59.28 cnf(1594,plain,
% 59.23/59.28 (~P2(a10,a1,a10)),
% 59.23/59.28 inference(scs_inference,[],[1572,44])).
% 59.23/59.28 cnf(1596,plain,
% 59.23/59.28 (~P1(x15961,f2(x15962,x15961,a1,a10),x15963,x15963)),
% 59.23/59.28 inference(scs_inference,[],[1557,1572,44,45])).
% 59.23/59.28 cnf(1599,plain,
% 59.23/59.28 (P1(x15991,f2(x15992,x15991,a1,a10),f2(x15993,x15994,f2(x15995,x15996,a11,a12),x15996),x15994)),
% 59.23/59.28 inference(rename_variables,[],[1410])).
% 59.23/59.28 cnf(1600,plain,
% 59.23/59.28 (~E(x16001,f2(x16002,x16001,f2(x16003,x16004,a11,a12),x16004))),
% 59.23/59.28 inference(scs_inference,[],[1557,1572,1410,1599,44,45,31,32])).
% 59.23/59.28 cnf(1612,plain,
% 59.23/59.28 (~P1(f2(x16121,x16122,f2(x16123,x16124,a1,a10),x16124),x16122,x16125,x16125)),
% 59.23/59.28 inference(scs_inference,[],[1576,1581,44,45])).
% 59.23/59.28 cnf(1614,plain,
% 59.23/59.28 (~E(x16141,f2(x16142,f2(x16143,x16141,x16144,x16144),a1,a10))),
% 59.23/59.28 inference(scs_inference,[],[80,1576,1581,1596,44,45,30])).
% 59.23/59.28 cnf(1617,plain,
% 59.23/59.28 (~E(x16171,f2(x16172,f2(x16173,x16171,a1,a10),x16174,x16174))),
% 59.23/59.28 inference(scs_inference,[],[80,1576,1581,1596,44,45,30,5])).
% 59.23/59.28 cnf(1618,plain,
% 59.23/59.28 (P1(x16181,a10,a12,a11)+~E(a1,x16181)),
% 59.23/59.28 inference(scs_inference,[],[80,1576,1581,1522,1596,44,45,30,5,29])).
% 59.23/59.28 cnf(1630,plain,
% 59.23/59.28 (~P1(f2(x16301,x16302,a11,a12),x16302,x16303,x16303)),
% 59.23/59.28 inference(scs_inference,[],[1583,44,45])).
% 59.23/59.28 cnf(1632,plain,
% 59.23/59.28 (~E(x16321,f2(x16321,x16322,a11,a12))),
% 59.23/59.28 inference(scs_inference,[],[1583,38,44,45,33])).
% 59.23/59.28 cnf(1634,plain,
% 59.23/59.28 (~E(x16341,f2(x16342,f2(x16343,x16341,x16344,x16344),f2(x16345,x16346,a1,a10),x16346))),
% 59.23/59.28 inference(scs_inference,[],[1583,39,1612,38,44,45,33,29])).
% 59.23/59.28 cnf(1645,plain,
% 59.23/59.28 (~P1(x16451,f2(x16452,x16451,a11,a12),x16453,x16453)),
% 59.23/59.28 inference(scs_inference,[],[1585,44,45])).
% 59.23/59.28 cnf(1647,plain,
% 59.23/59.28 (~E(x16471,f2(x16472,f2(x16473,x16471,x16474,x16474),a11,a12))),
% 59.23/59.28 inference(scs_inference,[],[1585,39,1630,44,45,29])).
% 59.23/59.28 cnf(1651,plain,
% 59.23/59.28 (P1(a1,a10,x16511,f2(x16512,x16513,a11,a12))+~E(x16513,x16511)),
% 59.23/59.28 inference(scs_inference,[],[1501,1585,39,1630,44,45,29,5,31])).
% 59.23/59.28 cnf(1662,plain,
% 59.23/59.28 (P1(x16621,f2(x16622,x16623,a1,a10),x16624,f2(x16625,x16624,a11,a12))+~E(x16623,x16621)),
% 59.23/59.28 inference(scs_inference,[],[1438,1581,1600,44,45,29])).
% 59.23/59.28 cnf(1686,plain,
% 59.23/59.28 (P1(a1,a10,x16861,a11)+~E(a12,x16861)),
% 59.23/59.28 inference(scs_inference,[],[1600,1647,1522,44,45,31])).
% 59.23/59.28 cnf(1696,plain,
% 59.23/59.28 (P1(f2(x16961,x16962,a1,a10),x16962,f2(x16963,x16964,a1,a10),x16964)),
% 59.23/59.28 inference(scs_inference,[],[912,80,1614,1570,45,44,46])).
% 59.23/59.28 cnf(1702,plain,
% 59.23/59.28 (P1(f2(x17021,x17022,a1,a10),x17022,f2(x17023,x17024,a1,a10),x17025)+~E(x17024,x17025)),
% 59.23/59.28 inference(scs_inference,[],[912,80,1410,1614,1570,45,44,46,29,31,30,32])).
% 59.23/59.28 cnf(1716,plain,
% 59.23/59.28 (P1(a1,x17161,a12,a11)+~E(a10,x17161)),
% 59.23/59.28 inference(scs_inference,[],[1647,1522,1634,44,45,30])).
% 59.23/59.28 cnf(1726,plain,
% 59.23/59.28 (P1(f2(x17261,x17262,a1,a10),x17263,f2(x17264,x17265,a1,a10),x17265)+~E(x17262,x17263)),
% 59.23/59.28 inference(scs_inference,[],[1696,1570,1574,45,44,30])).
% 59.23/59.28 cnf(1733,plain,
% 59.23/59.28 (~P2(f2(x17331,x17332,a1,a10),x17332,f2(x17331,x17332,a1,a10))),
% 59.23/59.28 inference(scs_inference,[],[1561,44])).
% 59.23/59.28 cnf(1750,plain,
% 59.23/59.28 (P1(x17501,f2(x17502,x17503,a1,a10),f2(x17504,x17505,a1,a10),x17505)+~E(x17503,x17501)),
% 59.23/59.28 inference(scs_inference,[],[960,1696,1634,38,1617,1733,45,44,33,46,29])).
% 59.23/59.28 cnf(1765,plain,
% 59.23/59.28 (~P1(f2(x17651,x17652,a1,a10),x17652,x17653,x17653)),
% 59.23/59.28 inference(scs_inference,[],[1561,45])).
% 59.23/59.28 cnf(1906,plain,
% 59.23/59.28 (~E(f2(x19061,x19062,a11,a12),x19061)),
% 59.23/59.28 inference(scs_inference,[],[1632,4,2])).
% 59.23/59.28 cnf(1909,plain,
% 59.23/59.28 (~P1(f2(x19091,x19092,a11,a12),x19091,x19093,x19093)),
% 59.23/59.28 inference(scs_inference,[],[1906,44,45])).
% 59.23/59.28 cnf(2028,plain,
% 59.23/59.28 (P1(a12,a11,x20281,f2(x20282,x20281,a1,a10))),
% 59.23/59.28 inference(scs_inference,[],[37,461,46])).
% 59.23/59.28 cnf(2060,plain,
% 59.23/59.28 (P1(x20601,f2(x20602,x20601,f2(x20603,x20604,a1,a10),x20604),a11,a12)),
% 59.23/59.28 inference(scs_inference,[],[37,1134,46])).
% 59.23/59.28 cnf(2072,plain,
% 59.23/59.28 (P1(a10,a1,f2(x20721,x20722,a11,a12),x20722)),
% 59.23/59.28 inference(scs_inference,[],[37,1485,46])).
% 59.23/59.28 cnf(2075,plain,
% 59.23/59.28 (~E(f2(x20751,a12,a11,a12),a11)),
% 59.23/59.28 inference(scs_inference,[],[37,43,1485,46,31])).
% 59.23/59.28 cnf(2076,plain,
% 59.23/59.28 (~E(f2(x20761,a10,f2(x20762,x20763,a1,a10),x20763),a1)),
% 59.23/59.28 inference(scs_inference,[],[37,43,1485,2060,46,31,30])).
% 59.23/59.28 cnf(2090,plain,
% 59.23/59.28 (P1(a10,a1,x20901,f2(x20902,x20901,a11,a12))),
% 59.23/59.28 inference(scs_inference,[],[37,1501,2076,45,46])).
% 59.23/59.28 cnf(2093,plain,
% 59.23/59.28 (~E(f2(x20931,a11,a11,a12),a12)),
% 59.23/59.28 inference(scs_inference,[],[37,43,1501,2076,45,46,32])).
% 59.23/59.28 cnf(2106,plain,
% 59.23/59.28 (P1(x21061,f2(x21062,x21061,a1,a10),x21063,f2(x21064,x21063,a1,a10))),
% 59.23/59.28 inference(scs_inference,[],[37,960,2093,45,46])).
% 59.23/59.28 cnf(2122,plain,
% 59.23/59.28 (P1(x21221,f2(x21222,x21223,a1,a10),x21224,f2(x21225,x21224,a1,a10))+~E(x21223,x21221)),
% 59.23/59.28 inference(scs_inference,[],[37,912,2106,46,29])).
% 59.23/59.28 cnf(2130,plain,
% 59.23/59.28 (P1(x21301,x21302,f2(x21303,x21304,f2(x21305,x21306,x21302,x21301),x21306),x21304)),
% 59.23/59.28 inference(scs_inference,[],[37,177,46])).
% 59.23/59.28 cnf(2133,plain,
% 59.23/59.28 (~E(x21331,f2(x21332,x21331,f2(x21333,x21334,a12,a11),x21334))),
% 59.23/59.28 inference(scs_inference,[],[37,177,1555,46,32])).
% 59.23/59.28 cnf(2134,plain,
% 59.23/59.28 (~P1(a11,a12,x21341,x21341)),
% 59.23/59.28 inference(rename_variables,[],[1555])).
% 59.23/59.28 cnf(2135,plain,
% 59.23/59.28 (~E(f2(x21351,x21352,f2(x21353,x21354,a12,a11),x21354),x21352)),
% 59.23/59.28 inference(scs_inference,[],[37,177,1555,2134,46,32,31])).
% 59.23/59.28 cnf(2136,plain,
% 59.23/59.28 (P1(x21361,a11,a11,a12)+~E(a12,x21361)),
% 59.23/59.28 inference(scs_inference,[],[37,177,1555,2134,46,32,31,29])).
% 59.23/59.28 cnf(2151,plain,
% 59.23/59.28 (P1(x21511,x21512,f2(x21513,x21514,x21512,x21511),x21514)),
% 59.23/59.28 inference(scs_inference,[],[37,113,2133,45,44,46])).
% 59.23/59.28 cnf(2154,plain,
% 59.23/59.28 (~E(f2(x21541,a12,f2(x21542,x21543,a1,a10),x21543),a11)),
% 59.23/59.28 inference(scs_inference,[],[37,43,113,2130,2133,45,44,46,31])).
% 59.23/59.28 cnf(2155,plain,
% 59.23/59.28 (P1(x21551,x21552,f2(x21553,x21554,f2(x21555,x21556,x21552,x21551),x21556),x21554)),
% 59.23/59.28 inference(rename_variables,[],[2130])).
% 59.23/59.28 cnf(2156,plain,
% 59.23/59.28 (~E(x21561,f2(x21562,x21561,a12,a11))),
% 59.23/59.28 inference(scs_inference,[],[37,43,113,2130,2133,1555,45,44,46,31,32])).
% 59.23/59.28 cnf(2159,plain,
% 59.23/59.28 (P1(a12,x21591,a11,a12)+~E(a11,x21591)),
% 59.23/59.28 inference(scs_inference,[],[37,43,113,2130,2155,2133,1555,45,44,46,31,32,29,30])).
% 59.23/59.28 cnf(2171,plain,
% 59.23/59.28 (P1(x21711,f2(x21712,x21711,f2(x21713,x21714,a1,a10),x21714),x21715,f2(x21716,x21715,a1,a10))),
% 59.23/59.28 inference(scs_inference,[],[37,922,2135,2156,45,44,46])).
% 59.23/59.28 cnf(2175,plain,
% 59.23/59.28 (~E(f2(x21751,a12,a1,a10),a11)),
% 59.23/59.28 inference(scs_inference,[],[37,43,922,2135,2151,2156,45,44,46,31])).
% 59.23/59.28 cnf(2176,plain,
% 59.23/59.28 (P1(x21761,x21762,f2(x21763,x21764,x21762,x21761),x21764)),
% 59.23/59.28 inference(rename_variables,[],[2151])).
% 59.23/59.28 cnf(2178,plain,
% 59.23/59.28 (~E(x21781,f2(x21782,x21781,a12,x21783))+~E(x21783,a11)),
% 59.23/59.28 inference(scs_inference,[],[37,43,922,2135,2151,2176,2156,1555,45,44,46,31,29,32])).
% 59.23/59.28 cnf(2189,plain,
% 59.23/59.28 (P1(x21891,f2(x21892,x21891,x21893,f2(x21894,x21893,x21895,x21896)),x21895,x21896)),
% 59.23/59.28 inference(scs_inference,[],[37,780,2156,2175,45,44,46])).
% 59.23/59.28 cnf(2203,plain,
% 59.23/59.28 (P1(x22031,x22032,x22033,f2(x22034,x22033,f2(x22035,x22036,x22032,x22031),x22036))),
% 59.23/59.28 inference(scs_inference,[],[37,260,2154,45,46])).
% 59.23/59.28 cnf(2208,plain,
% 59.23/59.28 (P1(x22081,f2(x22082,x22081,x22083,f2(x22084,x22083,x22085,x22086)),x22085,x22086)),
% 59.23/59.28 inference(rename_variables,[],[2189])).
% 59.23/59.28 cnf(2210,plain,
% 59.23/59.28 (P1(x22101,a10,a10,a1)+~E(a1,x22101)),
% 59.23/59.28 inference(scs_inference,[],[37,43,260,2189,2208,2154,45,46,32,30,31,29])).
% 59.23/59.28 cnf(2220,plain,
% 59.23/59.28 (P1(x22201,x22202,x22203,f2(x22204,x22203,x22202,x22201))),
% 59.23/59.28 inference(scs_inference,[],[37,242,2175,45,46])).
% 59.23/59.28 cnf(2227,plain,
% 59.23/59.28 (P1(a1,x22271,a10,a1)+~E(a10,x22271)),
% 59.23/59.28 inference(scs_inference,[],[37,43,242,2171,2175,45,46,32,44,29,30])).
% 59.23/59.28 cnf(2274,plain,
% 59.23/59.28 (P1(a12,a11,f2(x22741,x22742,a1,a10),x22742)),
% 59.23/59.28 inference(scs_inference,[],[37,132,46])).
% 59.23/59.28 cnf(2560,plain,
% 59.23/59.28 (~E(f2(x25601,a12,x25602,x25602),a11)),
% 59.23/59.28 inference(scs_inference,[],[2189,2178,45])).
% 59.23/59.28 cnf(2563,plain,
% 59.23/59.28 (~P2(f2(x25631,a12,x25632,x25632),a11,f2(x25631,a12,x25632,x25632))),
% 59.23/59.28 inference(scs_inference,[],[2560,45,44])).
% 59.23/59.28 cnf(2711,plain,
% 59.23/59.28 (P1(f2(x27111,x27112,a11,a12),x27112,x27113,f2(x27114,x27113,a11,a12))),
% 59.23/59.28 inference(scs_inference,[],[2072,2090,46])).
% 59.23/59.28 cnf(2713,plain,
% 59.23/59.28 (P1(f2(x27131,x27132,a11,a12),x27133,x27134,f2(x27135,x27134,a11,a12))+~E(x27132,x27133)),
% 59.23/59.28 inference(scs_inference,[],[2072,2090,46,30])).
% 59.23/59.28 cnf(2721,plain,
% 59.23/59.28 (P1(x27211,x27212,f2(x27213,x27214,x27215,f2(x27216,x27215,x27211,x27212)),x27214)),
% 59.23/59.28 inference(scs_inference,[],[80,2151,46])).
% 59.23/59.28 cnf(2724,plain,
% 59.23/59.28 (~E(x27241,f2(x27242,x27241,x27243,f2(x27244,x27243,a11,a12)))),
% 59.23/59.28 inference(scs_inference,[],[80,2151,1555,46,32])).
% 59.23/59.28 cnf(2725,plain,
% 59.23/59.28 (~P1(a11,a12,x27251,x27251)),
% 59.23/59.28 inference(rename_variables,[],[1555])).
% 59.23/59.28 cnf(2726,plain,
% 59.23/59.28 (~E(f2(x27261,x27262,x27263,f2(x27264,x27263,a11,a12)),x27262)),
% 59.23/59.28 inference(scs_inference,[],[80,2151,1555,2725,46,32,31])).
% 59.23/59.28 cnf(2727,plain,
% 59.23/59.28 (P1(f2(x27271,x27272,a11,a12),x27273,a11,a12)+~E(x27272,x27273)),
% 59.23/59.28 inference(scs_inference,[],[80,2151,1555,2725,46,32,31,30])).
% 59.23/59.28 cnf(2729,plain,
% 59.23/59.28 (~E(f2(x27291,x27292,a11,a12),a10)+~E(x27292,a1)),
% 59.23/59.28 inference(scs_inference,[],[43,80,2151,1555,2725,46,32,31,30,29])).
% 59.23/59.28 cnf(2746,plain,
% 59.23/59.28 (P1(x27461,x27462,x27463,f2(x27464,x27463,x27465,f2(x27466,x27465,x27461,x27462)))),
% 59.23/59.28 inference(scs_inference,[],[43,80,2220,2721,2724,45,44,31,46])).
% 59.23/59.28 cnf(2749,plain,
% 59.23/59.28 (~E(f2(x27491,a11,x27492,f2(x27493,x27492,a10,a1)),a12)),
% 59.23/59.28 inference(scs_inference,[],[43,80,2220,2721,2724,45,44,31,46,32])).
% 59.23/59.28 cnf(2750,plain,
% 59.23/59.28 (P1(f2(x27501,x27502,a10,a1),x27503,a10,a1)+~E(x27502,x27503)),
% 59.23/59.28 inference(scs_inference,[],[43,80,2220,2721,2724,45,44,31,46,32,30])).
% 59.23/59.28 cnf(2761,plain,
% 59.23/59.28 (P1(a1,a10,f2(x27611,x27612,f2(x27613,x27614,a11,a12),x27614),x27612)),
% 59.23/59.28 inference(scs_inference,[],[80,1064,2726,45,46])).
% 59.23/59.28 cnf(2789,plain,
% 59.23/59.28 (P1(f2(x27891,x27892,a1,a10),x27892,f2(x27893,x27894,a12,a11),x27894)),
% 59.23/59.28 inference(scs_inference,[],[132,2151,2749,45,46])).
% 59.23/59.28 cnf(2792,plain,
% 59.23/59.28 (~E(f2(x27921,x27922,a12,a11),x27922)),
% 59.23/59.28 inference(scs_inference,[],[132,2151,2749,1765,45,46,31])).
% 59.23/59.28 cnf(2794,plain,
% 59.23/59.28 (~P2(f2(x27941,x27942,a12,a11),x27942,f2(x27941,x27942,a12,a11))),
% 59.23/59.28 inference(scs_inference,[],[132,2151,2761,2749,1765,45,46,31,30,44])).
% 59.23/59.28 cnf(2796,plain,
% 59.23/59.28 (P1(f2(x27961,x27962,a1,a10),x27962,f2(x27963,x27964,a12,a11),x27965)+~E(x27964,x27965)),
% 59.23/59.28 inference(scs_inference,[],[132,2151,2761,2749,1765,45,46,31,30,44,32])).
% 59.23/59.28 cnf(2806,plain,
% 59.23/59.28 (P1(f2(x28061,x28062,a1,a10),x28062,x28063,f2(x28064,x28063,f2(x28065,x28066,a12,a11),x28066))),
% 59.23/59.28 inference(scs_inference,[],[132,2203,2792,45,46])).
% 59.23/59.28 cnf(2817,plain,
% 59.23/59.28 (P1(f2(x28171,x28172,a1,a10),x28172,x28173,f2(x28174,x28173,a12,a11))),
% 59.23/59.28 inference(scs_inference,[],[132,2220,46])).
% 59.23/59.28 cnf(2820,plain,
% 59.23/59.28 (P1(f2(x28201,x28202,a1,a10),x28203,f2(x28204,x28205,a12,a11),x28205)+~E(x28202,x28203)),
% 59.23/59.28 inference(scs_inference,[],[132,2220,2789,46,30])).
% 59.23/59.28 cnf(2840,plain,
% 59.23/59.28 (~E(f2(x28401,f2(x28402,a1,x28403,x28403),a11,a12),a10)),
% 59.23/59.28 inference(scs_inference,[],[80,2729,45])).
% 59.23/59.28 cnf(2843,plain,
% 59.23/59.28 (P1(f2(x28431,x28432,a1,a10),x28432,f2(x28433,x28434,x28435,f2(x28436,x28435,a11,a12)),x28434)),
% 59.23/59.28 inference(scs_inference,[],[132,2721,2840,45,46])).
% 59.23/59.28 cnf(2846,plain,
% 59.23/59.28 (P1(f2(x28461,x28462,a1,a10),x28463,x28464,f2(x28465,x28464,a12,a11))+~E(x28462,x28463)),
% 59.23/59.28 inference(scs_inference,[],[132,2721,2817,2840,45,46,30])).
% 59.23/59.28 cnf(2854,plain,
% 59.23/59.28 (P1(f2(x28541,x28542,a1,a10),x28542,x28543,f2(x28544,x28543,x28545,f2(x28546,x28545,a11,a12)))),
% 59.23/59.28 inference(scs_inference,[],[132,2746,46])).
% 59.23/59.28 cnf(2877,plain,
% 59.23/59.28 (P1(a1,a10,f2(x28771,x28772,a12,a11),x28772)),
% 59.23/59.28 inference(scs_inference,[],[80,2789,46])).
% 59.23/59.28 cnf(2901,plain,
% 59.23/59.28 (P1(a1,a10,x29011,f2(x29012,x29011,a12,a11))),
% 59.23/59.28 inference(scs_inference,[],[80,2817,46])).
% 59.23/59.28 cnf(3012,plain,
% 59.23/59.28 (P1(f2(x30121,x30122,a11,a12),x30122,x30123,f2(x30124,x30123,a1,a10))),
% 59.23/59.28 inference(scs_inference,[],[1539,80,46])).
% 59.23/59.28 cnf(3015,plain,
% 59.23/59.28 (P1(f2(x30151,x30152,a11,a12),x30153,x30154,f2(x30155,x30154,a1,a10))+~E(x30152,x30153)),
% 59.23/59.28 inference(scs_inference,[],[1539,80,46,30])).
% 59.23/59.28 cnf(3023,plain,
% 59.23/59.28 (P1(f2(x30231,x30232,a11,a12),x30232,a1,a10)),
% 59.23/59.28 inference(scs_inference,[],[1539,780,46])).
% 59.23/59.28 cnf(3026,plain,
% 59.23/59.28 (P1(f2(x30261,x30262,a11,a12),x30263,a1,a10)+~E(x30262,x30263)),
% 59.23/59.28 inference(scs_inference,[],[1539,780,46,30])).
% 59.23/59.28 cnf(3112,plain,
% 59.23/59.28 (P1(f2(x31121,x31122,a11,a12),x31122,f2(x31123,x31124,x31125,f2(x31126,x31125,a1,a10)),x31124)),
% 59.23/59.28 inference(scs_inference,[],[1539,100,46])).
% 59.23/59.28 cnf(3120,plain,
% 59.23/59.28 (P1(f2(x31201,x31202,a11,a12),x31202,f2(x31203,x31204,x31205,f2(x31206,x31205,a1,a10)),x31204)),
% 59.23/59.28 inference(rename_variables,[],[3112])).
% 59.23/59.28 cnf(3121,plain,
% 59.23/59.28 (~P1(f2(x31211,x31212,a11,a12),x31211,x31213,x31213)),
% 59.23/59.28 inference(rename_variables,[],[1909])).
% 59.23/59.28 cnf(3125,plain,
% 59.23/59.28 (P1(f2(x31251,x31252,a11,a12),x31252,x31253,f2(x31254,x31253,x31255,f2(x31256,x31255,a1,a10)))),
% 59.23/59.28 inference(scs_inference,[],[1539,3112,3120,37,1909,3121,31,32,46])).
% 59.23/59.28 cnf(3384,plain,
% 59.23/59.28 (P1(f2(x33841,x33842,a11,a12),x33842,a12,a11)),
% 59.23/59.28 inference(scs_inference,[],[1050,1163,46])).
% 59.23/59.28 cnf(3388,plain,
% 59.23/59.28 (P1(f2(x33881,x33882,a11,a12),x33883,a12,a11)+~E(x33882,x33883)),
% 59.23/59.28 inference(scs_inference,[],[1050,1163,46,29,30])).
% 59.23/59.28 cnf(3396,plain,
% 59.23/59.28 (P1(f2(x33961,x33962,a11,a12),x33962,x33963,f2(x33964,x33963,f2(x33965,x33966,a11,a12),x33966))),
% 59.23/59.28 inference(scs_inference,[],[1050,1093,46])).
% 59.23/59.28 cnf(3418,plain,
% 59.23/59.28 (P1(f2(x34181,x34182,a11,a12),x34182,f2(x34183,x34184,a12,a11),x34184)),
% 59.23/59.28 inference(scs_inference,[],[1050,2789,46])).
% 59.23/59.28 cnf(3421,plain,
% 59.23/59.28 (P1(f2(x34211,x34212,a11,a12),x34213,f2(x34214,x34215,a12,a11),x34215)+~E(x34212,x34213)),
% 59.23/59.28 inference(scs_inference,[],[1050,2789,46,30])).
% 59.23/59.28 cnf(3429,plain,
% 59.23/59.28 (P1(f2(x34291,x34292,a11,a12),x34292,x34293,f2(x34294,x34293,f2(x34295,x34296,a12,a11),x34296))),
% 59.23/59.28 inference(scs_inference,[],[1050,2806,46])).
% 59.23/59.28 cnf(3440,plain,
% 59.23/59.28 (P1(f2(x34401,x34402,a11,a12),x34402,x34403,f2(x34404,x34403,a12,a11))),
% 59.23/59.28 inference(scs_inference,[],[1050,2817,46])).
% 59.23/59.28 cnf(3443,plain,
% 59.23/59.28 (P1(f2(x34431,x34432,a11,a12),x34433,x34434,f2(x34435,x34434,a12,a11))+~E(x34432,x34433)),
% 59.23/59.28 inference(scs_inference,[],[1050,2817,46,30])).
% 59.23/59.28 cnf(3451,plain,
% 59.23/59.28 (P1(f2(x34511,x34512,a11,a12),x34512,f2(x34513,x34514,x34515,f2(x34516,x34515,a11,a12)),x34514)),
% 59.23/59.28 inference(scs_inference,[],[1050,2843,46])).
% 59.23/59.28 cnf(3462,plain,
% 59.23/59.28 (P1(f2(x34621,x34622,a11,a12),x34622,x34623,f2(x34624,x34623,x34625,f2(x34626,x34625,a11,a12)))),
% 59.23/59.28 inference(scs_inference,[],[1050,2854,46])).
% 59.23/59.28 cnf(3507,plain,
% 59.23/59.28 (P1(x35071,f2(x35072,x35071,x35073,f2(x35074,x35073,a12,a11)),x35075,f2(x35076,x35075,a1,a10))),
% 59.23/59.28 inference(scs_inference,[],[2746,2028,46])).
% 59.23/59.28 cnf(3535,plain,
% 59.23/59.28 (P1(x35351,f2(x35352,x35351,x35353,f2(x35354,x35353,a10,a1)),f2(x35355,x35356,a11,a12),x35356)),
% 59.23/59.28 inference(scs_inference,[],[2746,2072,46])).
% 59.23/59.28 cnf(3563,plain,
% 59.23/59.28 (P1(x35631,f2(x35632,x35631,x35633,f2(x35634,x35633,a10,a1)),x35635,f2(x35636,x35635,a11,a12))),
% 59.23/59.28 inference(scs_inference,[],[2746,2090,46])).
% 59.23/59.28 cnf(3592,plain,
% 59.23/59.28 (P1(x35921,f2(x35922,x35921,x35923,f2(x35924,x35923,a12,a11)),f2(x35925,x35926,a1,a10),x35926)),
% 59.23/59.28 inference(scs_inference,[],[2746,2274,46])).
% 59.23/59.28 cnf(3606,plain,
% 59.23/59.28 (P1(x36061,f2(x36062,x36061,a11,a12),x36063,f2(x36064,x36063,a1,a10))),
% 59.23/59.28 inference(scs_inference,[],[2711,3012,46])).
% 59.23/59.28 cnf(3624,plain,
% 59.23/59.28 (P1(x36241,f2(x36242,x36241,a11,a12),a1,a10)),
% 59.23/59.28 inference(scs_inference,[],[2711,3023,46])).
% 59.23/59.28 cnf(3628,plain,
% 59.23/59.28 (P1(x36281,f2(x36282,x36283,a11,a12),x36284,f2(x36285,x36284,a1,a10))+~E(x36283,x36281)),
% 59.23/59.28 inference(scs_inference,[],[2711,3023,3606,46,30,29])).
% 59.23/59.28 cnf(3639,plain,
% 59.23/59.28 (P1(x36391,f2(x36392,x36393,a11,a12),a1,a10)+~E(x36393,x36391)),
% 59.23/59.28 inference(scs_inference,[],[2711,3112,3624,46,30,29])).
% 59.23/59.28 cnf(3646,plain,
% 59.23/59.28 (P1(x36461,f2(x36462,x36461,a11,a12),x36463,f2(x36464,x36463,x36465,f2(x36466,x36465,a1,a10)))),
% 59.23/59.28 inference(scs_inference,[],[2711,3125,46])).
% 59.23/59.28 cnf(3688,plain,
% 59.23/59.28 (P1(x36881,f2(x36882,x36881,a11,a12),a12,a11)),
% 59.23/59.28 inference(scs_inference,[],[2711,3384,46])).
% 59.23/59.28 cnf(3703,plain,
% 59.23/59.28 (P1(x37031,f2(x37032,x37033,a11,a12),a12,a11)+~E(x37033,x37031)),
% 59.23/59.28 inference(scs_inference,[],[2711,3396,3688,46,30,29])).
% 59.23/59.28 cnf(3721,plain,
% 59.23/59.28 (P1(x37211,f2(x37212,x37211,a11,a12),f2(x37213,x37214,a12,a11),x37214)),
% 59.23/59.28 inference(scs_inference,[],[2711,3418,46])).
% 59.23/59.28 cnf(3736,plain,
% 59.23/59.28 (P1(x37361,f2(x37362,x37363,a11,a12),f2(x37364,x37365,a12,a11),x37365)+~E(x37363,x37361)),
% 59.23/59.28 inference(scs_inference,[],[2711,3429,3721,46,30,29])).
% 59.23/59.28 cnf(3743,plain,
% 59.23/59.28 (P1(x37431,f2(x37432,x37431,a12,a11),x37433,f2(x37434,x37433,a1,a10))),
% 59.23/59.28 inference(scs_inference,[],[39,3507,46])).
% 59.23/59.28 cnf(3763,plain,
% 59.23/59.28 (P1(x37631,f2(x37632,x37631,a11,a12),x37633,f2(x37634,x37633,a12,a11))),
% 59.23/59.28 inference(scs_inference,[],[2711,3440,46])).
% 59.23/59.28 cnf(3781,plain,
% 59.23/59.28 (P1(x37811,f2(x37812,x37811,a10,a1),f2(x37813,x37814,a11,a12),x37814)),
% 59.23/59.28 inference(scs_inference,[],[39,3535,46])).
% 59.23/59.28 cnf(3785,plain,
% 59.23/59.28 (P1(x37851,f2(x37852,x37851,a10,a1),f2(x37853,x37854,a11,a12),x37855)+~E(x37854,x37855)),
% 59.23/59.28 inference(scs_inference,[],[39,3535,46,32])).
% 59.23/59.28 cnf(3800,plain,
% 59.23/59.28 (P1(x38001,f2(x38002,x38003,a12,a11),x38004,f2(x38005,x38004,a1,a10))+~E(x38003,x38001)),
% 59.23/59.28 inference(scs_inference,[],[2711,3451,3743,46,30,29])).
% 59.23/59.28 cnf(3811,plain,
% 59.23/59.28 (P1(x38111,f2(x38112,x38113,a11,a12),x38114,f2(x38115,x38114,a12,a11))+~E(x38113,x38111)),
% 59.23/59.28 inference(scs_inference,[],[2711,3462,3763,46,30,29])).
% 59.23/59.28 cnf(3818,plain,
% 59.23/59.28 (P1(x38181,f2(x38182,x38181,a10,a1),x38183,f2(x38184,x38183,a11,a12))),
% 59.23/59.28 inference(scs_inference,[],[39,3563,46])).
% 59.23/59.28 cnf(3834,plain,
% 59.23/59.28 (P1(x38341,f2(x38342,x38341,a12,a11),f2(x38343,x38344,a1,a10),x38344)),
% 59.23/59.28 inference(scs_inference,[],[39,3592,46])).
% 59.23/59.28 cnf(3838,plain,
% 59.23/59.28 (P1(x38381,f2(x38382,x38381,a10,a1),x38383,f2(x38384,x38385,a11,a12))+~E(x38385,x38383)),
% 59.36/59.28 inference(scs_inference,[],[39,3592,3818,46,31])).
% 59.36/59.28 cnf(3862,plain,
% 59.36/59.28 (P1(a11,a12,x38621,f2(x38622,x38621,x38623,f2(x38624,x38623,a1,a10)))),
% 59.36/59.28 inference(scs_inference,[],[39,3646,46])).
% 59.36/59.28 cnf(3867,plain,
% 59.36/59.28 (P1(x38671,f2(x38672,x38673,a10,a1),f2(x38674,x38675,a11,a12),x38675)+~E(x38673,x38671)),
% 59.36/59.28 inference(scs_inference,[],[39,3646,3781,3834,46,30,29])).
% 59.36/59.28 cnf(3887,plain,
% 59.36/59.28 (P1(x38871,f2(x38872,x38873,a10,a1),x38874,f2(x38875,x38874,a11,a12))+~E(x38873,x38871)),
% 59.36/59.28 inference(scs_inference,[],[132,3818,3862,46,30,29])).
% 59.36/59.28 cnf(3916,plain,
% 59.36/59.28 (P1(x39161,f2(x39162,x39163,a12,a11),f2(x39164,x39165,a1,a10),x39165)+~E(x39163,x39161)),
% 59.36/59.28 inference(scs_inference,[],[3834,29])).
% 59.36/59.28 cnf(4000,plain,
% 59.36/59.28 (P1(f2(x40001,x40002,a11,a12),x40002,f2(x40003,x40004,a1,a10),x40004)),
% 59.36/59.28 inference(scs_inference,[],[1050,1696,46])).
% 59.36/59.28 cnf(4003,plain,
% 59.36/59.28 (P1(f2(x40031,x40032,a11,a12),x40033,f2(x40034,x40035,a1,a10),x40035)+~E(x40032,x40033)),
% 59.36/59.28 inference(scs_inference,[],[1050,1696,46,30])).
% 59.36/59.28 cnf(4026,plain,
% 59.36/59.28 (P1(x40261,f2(x40262,x40263,a11,a12),f2(x40264,x40265,a1,a10),x40265)+~E(x40263,x40261)),
% 59.36/59.28 inference(scs_inference,[],[2711,4000,46,30,29])).
% 59.36/59.28 cnf(4088,plain,
% 59.36/59.28 (P1(f2(x40881,x40882,a12,a11),x40883,x40884,f2(x40885,x40884,a12,a11))+~E(x40882,x40883)),
% 59.36/59.28 inference(scs_inference,[],[2877,2901,46,30])).
% 59.36/59.28 cnf(4096,plain,
% 59.36/59.28 (~E(a11,f2(x40961,a12,a11,a12))),
% 59.36/59.28 inference(scs_inference,[],[2075,2])).
% 59.36/59.28 cnf(4097,plain,
% 59.36/59.28 (~E(x40971,f2(x40971,x40972,a12,a11))),
% 59.36/59.28 inference(scs_inference,[],[2794,2075,2,70])).
% 59.36/59.28 cnf(4098,plain,
% 59.36/59.28 (~E(a8,a6)),
% 59.36/59.28 inference(scs_inference,[],[2794,681,2075,2,70,121])).
% 59.36/59.28 cnf(4100,plain,
% 59.36/59.28 (E(x41001,f2(x41002,x41001,x41003,x41003))),
% 59.36/59.28 inference(scs_inference,[],[2794,681,2075,39,2,70,121,45])).
% 59.36/59.28 cnf(4103,plain,
% 59.36/59.28 (~E(f2(x41031,a12,x41032,x41032),f2(x41033,a11,a10,a1))),
% 59.36/59.28 inference(scs_inference,[],[2794,681,2075,855,39,2,70,121,45,3])).
% 59.36/59.28 cnf(4104,plain,
% 59.36/59.28 (~P2(a12,a11,f2(x41041,a12,x41042,x41042))),
% 59.36/59.28 inference(scs_inference,[],[2794,681,2563,2075,855,39,2,70,121,45,3,33])).
% 59.36/59.28 cnf(4107,plain,
% 59.36/59.28 (~P1(a8,a9,x41071,x41071)),
% 59.36/59.28 inference(rename_variables,[],[316])).
% 59.36/59.28 cnf(4113,plain,
% 59.36/59.28 (~E(x41131,f2(x41132,x41131,a10,a1))),
% 59.36/59.28 inference(scs_inference,[],[316,4107,2794,681,2563,2075,1630,3781,855,100,39,2,70,121,45,3,33,32,31,46,30])).
% 59.36/59.28 cnf(4114,plain,
% 59.36/59.28 (P1(x41141,x41142,x41141,x41142)),
% 59.36/59.28 inference(rename_variables,[],[100])).
% 59.36/59.28 cnf(4115,plain,
% 59.36/59.28 (P1(a11,f2(x41151,a12,x41152,x41152),a11,a12)),
% 59.36/59.28 inference(scs_inference,[],[316,4107,2794,681,2563,2075,1630,3781,855,100,39,2,70,121,45,3,33,32,31,46,30,89])).
% 59.36/59.28 cnf(4117,plain,
% 59.36/59.28 (P1(a11,f2(x41171,a12,x41172,x41172),a10,a1)),
% 59.36/59.28 inference(scs_inference,[],[316,4107,2794,681,2563,2075,1630,3781,855,100,39,2,70,121,45,3,33,32,31,46,30,89,184,394])).
% 59.36/59.28 cnf(4172,plain,
% 59.36/59.28 (~E(a6,f2(a6,a9,x41721,x41722))),
% 59.36/59.28 inference(scs_inference,[],[316,4107,2794,681,837,2563,2075,1630,3781,855,100,4114,39,2,70,121,45,3,33,32,31,46,30,89,184,394,2136,1129,1181,1444,1477,2727,2750,3026,3388,3639,3703,295,324,1007,1086,1231,1416,1662,1726,1750,2122,2713,2820,2846,3015,3421,3443,3628,3736,3785,3800,3811,3838,3867,3887,3916,4003,4026,4088,1399,962,1085,1126,1702,69,1686,1505,1651,2796,207,486,88,29])).
% 59.36/59.28 cnf(4174,plain,
% 59.36/59.28 (P1(x41741,x41742,x41741,x41742)),
% 59.36/59.28 inference(rename_variables,[],[100])).
% 59.36/59.28 cnf(4175,plain,
% 59.36/59.28 (~P1(a6,a8,a6,a8)+~P1(a6,a6,a6,f2(a6,a8,a6,a8))),
% 59.36/59.28 inference(scs_inference,[],[316,4107,2794,681,824,837,2563,2075,1630,3781,855,527,2220,100,4114,4174,39,38,2,70,121,45,3,33,32,31,46,30,89,184,394,2136,1129,1181,1444,1477,2727,2750,3026,3388,3639,3703,295,324,1007,1086,1231,1416,1662,1726,1750,2122,2713,2820,2846,3015,3421,3443,3628,3736,3785,3800,3811,3838,3867,3887,3916,4003,4026,4088,1399,962,1085,1126,1702,69,1686,1505,1651,2796,207,486,88,29,48])).
% 59.36/59.28 cnf(4182,plain,
% 59.36/59.28 (P1(f2(x41821,a12,x41822,x41823),f2(x41824,a12,x41825,x41825),x41822,x41823)+~E(x41826,a11)),
% 59.36/59.28 inference(scs_inference,[],[316,4107,2794,681,824,837,2563,2075,1630,3781,855,527,2220,100,4114,4174,39,38,2,70,121,45,3,33,32,31,46,30,89,184,394,2136,1129,1181,1444,1477,2727,2750,3026,3388,3639,3703,295,324,1007,1086,1231,1416,1662,1726,1750,2122,2713,2820,2846,3015,3421,3443,3628,3736,3785,3800,3811,3838,3867,3887,3916,4003,4026,4088,1399,962,1085,1126,1702,69,1686,1505,1651,2796,207,486,88,29,48,107])).
% 59.36/59.28 cnf(4183,plain,
% 59.36/59.28 (P1(f2(x41831,a12,x41832,x41833),f2(x41834,a12,x41835,x41835),x41832,x41833)),
% 59.36/59.28 inference(equality_inference,[],[4182])).
% 59.36/59.28 cnf(4185,plain,
% 59.36/59.28 (E(x41851,f2(x41852,x41851,x41853,x41853))),
% 59.36/59.28 inference(rename_variables,[],[4100])).
% 59.36/59.28 cnf(4187,plain,
% 59.36/59.28 (E(x41871,f2(x41872,x41871,x41873,x41873))),
% 59.36/59.28 inference(rename_variables,[],[4100])).
% 59.36/59.28 cnf(4189,plain,
% 59.36/59.28 (E(x41891,f2(x41892,x41891,x41893,x41893))),
% 59.36/59.28 inference(rename_variables,[],[4100])).
% 59.36/59.28 cnf(4191,plain,
% 59.36/59.28 (E(x41911,f2(x41912,x41911,x41913,x41913))),
% 59.36/59.28 inference(rename_variables,[],[4100])).
% 59.36/59.28 cnf(4193,plain,
% 59.36/59.28 (E(x41931,f2(x41932,x41931,x41933,x41933))),
% 59.36/59.28 inference(rename_variables,[],[4100])).
% 59.36/59.28 cnf(4195,plain,
% 59.36/59.28 (E(x41951,f2(x41952,x41951,x41953,x41953))),
% 59.36/59.28 inference(rename_variables,[],[4100])).
% 59.36/59.28 cnf(4197,plain,
% 59.36/59.28 (E(x41971,f2(x41972,x41971,x41973,x41973))),
% 59.36/59.28 inference(rename_variables,[],[4100])).
% 59.36/59.28 cnf(4199,plain,
% 59.36/59.28 (E(x41991,f2(x41992,x41991,x41993,x41993))),
% 59.36/59.28 inference(rename_variables,[],[4100])).
% 59.36/59.28 cnf(4201,plain,
% 59.36/59.28 (E(x42011,f2(x42012,x42011,x42013,x42013))),
% 59.36/59.28 inference(rename_variables,[],[4100])).
% 59.36/59.28 cnf(4205,plain,
% 59.36/59.28 (E(x42051,f2(x42052,x42051,x42053,x42053))),
% 59.36/59.28 inference(rename_variables,[],[4100])).
% 59.36/59.28 cnf(4207,plain,
% 59.36/59.28 (E(x42071,f2(x42072,x42071,x42073,x42073))),
% 59.36/59.28 inference(rename_variables,[],[4100])).
% 59.36/59.28 cnf(4209,plain,
% 59.36/59.28 (E(x42091,f2(x42092,x42091,x42093,x42093))),
% 59.36/59.28 inference(rename_variables,[],[4100])).
% 59.36/59.28 cnf(4211,plain,
% 59.36/59.28 (E(x42111,f2(x42112,x42111,x42113,x42113))),
% 59.36/59.28 inference(rename_variables,[],[4100])).
% 59.36/59.28 cnf(4213,plain,
% 59.36/59.28 (E(x42131,f2(x42132,x42131,x42133,x42133))),
% 59.36/59.28 inference(rename_variables,[],[4100])).
% 59.36/59.28 cnf(4218,plain,
% 59.36/59.28 (P1(f2(x42181,x42182,a10,a1),f2(x42183,x42182,x42184,x42184),a10,a1)),
% 59.36/59.28 inference(scs_inference,[],[4100,4185,4187,4189,4191,4193,4195,4197,4199,4201,4205,4207,4209,4211,4213,100,66,122,283,336,1618,1716,2159,2210,2227,4175,141,1543,87,229,309,324,1129,3628,2750])).
% 59.36/59.28 cnf(4230,plain,
% 59.36/59.28 (E(x42301,f2(x42302,x42301,x42303,x42303))),
% 59.36/59.28 inference(rename_variables,[],[4100])).
% 59.36/59.28 cnf(4255,plain,
% 59.36/59.28 (E(x42551,f2(x42552,x42551,x42553,x42553))),
% 59.36/59.28 inference(rename_variables,[],[4100])).
% 59.36/59.28 cnf(4272,plain,
% 59.36/59.28 (E(x42721,f2(x42722,x42721,x42723,x42723))),
% 59.36/59.28 inference(rename_variables,[],[4100])).
% 59.36/59.28 cnf(4273,plain,
% 59.36/59.28 (~P2(a8,a6,a8)),
% 59.36/59.28 inference(scs_inference,[],[4098,4100,4185,4187,4189,4191,4193,4195,4197,4199,4201,4205,4207,4209,4211,4213,4230,4255,4272,4183,4097,493,100,66,122,283,336,1618,1716,2159,2210,2227,4175,141,1543,87,229,309,324,1129,3628,2750,3015,3443,962,1181,3026,4003,1750,1726,1085,4026,206,3887,295,2713,3916,1651,1231,1126,1702,3388,3736,1477,1416,3421,486,1444,2846,2727,1007,3800,1086,1399,3867,183,1505,3811,3703,3785,2,2122,2820,207,3838,2796,1662,3639,45,3,34])).
% 59.36/59.28 cnf(4289,plain,
% 59.36/59.28 (E(f2(x42891,x42892,x42893,x42893),x42892)),
% 59.36/59.28 inference(scs_inference,[],[4113,80,2,45])).
% 59.36/59.28 cnf(4292,plain,
% 59.36/59.28 (~E(f2(x42921,a6,x42922,x42922),f2(a6,a9,x42923,x42924))),
% 59.36/59.28 inference(scs_inference,[],[4113,4172,4100,80,2,45,3])).
% 59.36/59.28 cnf(4294,plain,
% 59.36/59.28 (~P2(f2(x42941,a10,x42942,x42942),a1,a10)),
% 59.36/59.28 inference(scs_inference,[],[1594,4113,4172,4100,80,2,45,3,33])).
% 59.36/59.28 cnf(4308,plain,
% 59.36/59.28 (~E(x43081,x43082)+P1(f2(x43083,x43081,x43084,x43085),x43082,x43084,x43085)),
% 59.36/59.28 inference(scs_inference,[],[4289,107])).
% 59.36/59.28 cnf(4311,plain,
% 59.36/59.28 (~E(f2(a6,a9,x43111,x43112),f2(x43113,a6,x43114,x43114))),
% 59.36/59.28 inference(scs_inference,[],[4292,2])).
% 59.36/59.28 cnf(4313,plain,
% 59.36/59.28 (E(f2(x43131,x43132,x43133,x43133),x43132)),
% 59.36/59.28 inference(rename_variables,[],[4289])).
% 59.36/59.28 cnf(4315,plain,
% 59.36/59.28 (E(f2(x43151,x43152,x43153,x43153),x43152)),
% 59.36/59.28 inference(rename_variables,[],[4289])).
% 59.36/59.28 cnf(4317,plain,
% 59.36/59.28 (E(f2(x43171,x43172,x43173,x43173),x43172)),
% 59.36/59.28 inference(rename_variables,[],[4289])).
% 59.36/59.28 cnf(4319,plain,
% 59.36/59.28 (E(f2(x43191,x43192,x43193,x43193),x43192)),
% 59.36/59.28 inference(rename_variables,[],[4289])).
% 59.36/59.28 cnf(4321,plain,
% 59.36/59.28 (E(f2(x43211,x43212,x43213,x43213),x43212)),
% 59.36/59.28 inference(rename_variables,[],[4289])).
% 59.36/59.28 cnf(4325,plain,
% 59.36/59.28 (E(f2(x43251,x43252,x43253,x43253),x43252)),
% 59.36/59.28 inference(rename_variables,[],[4289])).
% 59.36/59.28 cnf(4329,plain,
% 59.36/59.28 (E(f2(x43291,x43292,x43293,x43293),f2(x43294,x43292,x43295,x43295))),
% 59.36/59.28 inference(scs_inference,[],[43,591,4273,4292,4218,4289,4313,4315,4317,4319,4321,4325,4100,2,33,34,35,32,31,46,30,29,4308,45])).
% 59.36/59.28 cnf(4335,plain,
% 59.36/59.28 (~E(f2(x43351,a9,x43352,x43352),f2(x43353,a6,x43354,x43354))),
% 59.36/59.28 inference(scs_inference,[],[4329,4311,4103,2,3])).
% 59.36/59.28 cnf(4365,plain,
% 59.36/59.28 (E(x43651,f2(x43652,x43651,x43653,x43653))),
% 59.36/59.28 inference(rename_variables,[],[4100])).
% 59.36/59.28 cnf(4367,plain,
% 59.36/59.28 (E(f2(x43671,x43672,x43673,x43673),x43672)),
% 59.36/59.28 inference(rename_variables,[],[4289])).
% 59.36/59.28 cnf(4371,plain,
% 59.36/59.28 (~P1(x43711,f2(x43712,x43711,a11,a12),x43713,x43713)),
% 59.36/59.28 inference(rename_variables,[],[1645])).
% 59.36/59.28 cnf(4374,plain,
% 59.36/59.28 ($false),
% 59.36/59.28 inference(scs_inference,[],[43,1645,4371,4335,4096,4104,4294,4115,4117,4329,4289,4367,4100,4365,2,3,33,35,32,31,46]),
% 59.36/59.28 ['proof']).
% 59.36/59.28 % SZS output end Proof
% 59.36/59.28 % Total time :58.650000s
%------------------------------------------------------------------------------