%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : KRS203+1 : TPTP v8.2.0. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n002.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 10:08:52 EDT 2024
% Result : Theorem 106.42s 106.59s
% Output : CNFRefutation 106.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : KRS203+1 : TPTP v8.2.0. Bugfixed v5.4.0.
% 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.11/0.33 % Computer : n002.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Wed Jun 19 13:25:39 EDT 2024
% 0.11/0.33 % CPUTime :
% 0.19/0.56 start to proof:theBenchmark
% 106.42/106.58 %-------------------------------------------
% 106.42/106.58 % File :CSE---1.7
% 106.42/106.58 % Problem :theBenchmark
% 106.42/106.58 % Transform :cnf
% 106.42/106.58 % Format :tptp:raw
% 106.42/106.58 % Command :java -jar mcs_scs.jar %d %s
% 106.42/106.58
% 106.42/106.58 % Result :Theorem 105.880000s
% 106.42/106.58 % Output :CNFRefutation 105.880000s
% 106.42/106.58 %-------------------------------------------
% 106.42/106.58 %------------------------------------------------------------------------------
% 106.42/106.58 % File : KRS203+1 : TPTP v8.2.0. Bugfixed v5.4.0.
% 106.42/106.58 % Domain : Knowledge Representation
% 106.42/106.58 % Problem : SAT nota THM
% 106.42/106.58 % Version : [Sut08] axioms.
% 106.42/106.58 % English :
% 106.42/106.58
% 106.42/106.58 % Refs : [Sut08] Sutcliffe (2008), The SZS Ontologies for Automated Rea
% 106.42/106.58 % Source : [TPTP]
% 106.42/106.58 % Names :
% 106.42/106.58
% 106.42/106.58 % Status : Theorem
% 106.42/106.58 % Rating : 0.19 v8.2.0, 0.27 v8.1.0, 0.14 v7.5.0, 0.24 v7.4.0, 0.12 v7.3.0, 0.29 v7.2.0, 0.17 v7.1.0, 0.25 v7.0.0, 0.07 v6.3.0, 0.08 v6.2.0, 0.27 v6.1.0, 0.32 v6.0.0, 0.50 v5.5.0, 0.42 v5.4.0
% 106.42/106.58 % Syntax : Number of formulae : 33 ( 3 unt; 0 def)
% 106.42/106.58 % Number of atoms : 107 ( 0 equ)
% 106.42/106.58 % Maximal formula atoms : 7 ( 3 avg)
% 106.42/106.58 % Number of connectives : 96 ( 22 ~; 1 |; 35 &)
% 106.42/106.58 % ( 28 <=>; 8 =>; 0 <=; 2 <~>)
% 106.42/106.59 % Maximal formula depth : 10 ( 6 avg)
% 106.42/106.59 % Maximal term depth : 2 ( 1 avg)
% 106.42/106.59 % Number of predicates : 7 ( 7 usr; 0 prp; 2-3 aty)
% 106.42/106.59 % Number of functors : 20 ( 20 usr; 19 con; 0-1 aty)
% 106.42/106.59 % Number of variables : 122 ( 72 !; 50 ?)
% 106.42/106.59 % SPC : FOF_THM_RFO_NEQ
% 106.42/106.59
% 106.42/106.59 % Comments :
% 106.42/106.59 % Bugfixes : v5.4.0 - Added missing axiom in KRS001+1.ax
% 106.42/106.59 %------------------------------------------------------------------------------
% 106.42/106.59 %----Include SZS success ontology nodes
% 106.42/106.59 include('Axioms/KRS001+0.ax').
% 106.42/106.59 %----Include SZS success ontology node relationships
% 106.42/106.59 include('Axioms/KRS001+1.ax').
% 106.42/106.59 %------------------------------------------------------------------------------
% 106.42/106.59 fof(nota_sat_thm,conjecture,
% 106.42/106.59 nota(sat,thm) ).
% 106.42/106.59
% 106.42/106.59 %------------------------------------------------------------------------------
% 106.42/106.59 %-------------------------------------------
% 106.42/106.59 % Proof found
% 106.42/106.59 % SZS status Theorem for theBenchmark
% 106.42/106.59 % SZS output start Proof
% 106.42/106.59 %ClaNum:109(EqnAxiom:0)
% 106.42/106.59 %VarNum:590(SingletonVarNum:249)
% 106.42/106.59 %MaxLitNum:6
% 106.42/106.59 %MaxfuncDepth:1
% 106.42/106.59 %SharedTerms:52
% 106.42/106.59 %goalClause: 13
% 106.42/106.59 %singleGoalClaCount:1
% 106.42/106.59 [1]P1(a1,a2)
% 106.42/106.59 [2]P1(a55,a56)
% 106.42/106.59 [3]P1(a55,a59)
% 106.42/106.59 [4]P1(a61,a62)
% 106.42/106.59 [5]P1(a66,a65)
% 106.42/106.59 [6]P1(a67,a69)
% 106.42/106.59 [7]P1(a70,a71)
% 106.42/106.59 [9]~P1(a57,a2)
% 106.42/106.59 [10]~P1(a66,a62)
% 106.42/106.59 [11]~P1(a68,a65)
% 106.42/106.59 [12]~P1(a67,a71)
% 106.42/106.59 [13]~P4(a73,a81)
% 106.42/106.59 [8]P1(x81,a3)
% 106.42/106.59 [14]~P1(x141,a58)
% 106.42/106.59 [18]~P1(a63,a56)+~P1(a64,a59)
% 106.42/106.59 [15]~P1(x151,a62)+P1(x151,a65)
% 106.42/106.59 [17]P1(x171,x172)+P1(x171,f74(x172))
% 106.42/106.59 [20]~P1(x201,x202)+~P1(x201,f74(x202))
% 106.42/106.59 [21]P6(x211,x212,a5)+P1(f4(x211),x211)
% 106.42/106.59 [24]P6(x241,x242,a86)+P1(f6(x241,x242),x242)
% 106.42/106.59 [25]P6(x251,x252,a80)+P1(f31(x251,x252),x251)
% 106.42/106.59 [26]P6(x261,x262,a81)+P1(f7(x261,x262),x261)
% 106.42/106.59 [42]P6(x421,x422,a81)+~P1(f7(x421,x422),x422)
% 106.42/106.59 [50]P2(x501,x502)+P6(f41(x501,x502),f47(x501,x502),x501)
% 106.42/106.59 [51]P5(x511,x512)+P6(f48(x511,x512),f51(x511,x512),x512)
% 106.42/106.59 [52]P5(x521,x522)+P6(f48(x521,x522),f51(x521,x522),x521)
% 106.42/106.59 [53]~P6(x531,x532,a73)+P1(f76(x531,x532),x532)
% 106.42/106.59 [54]~P6(x541,x542,a73)+P1(f76(x541,x542),x541)
% 106.42/106.59 [55]~P6(x551,x552,a10)+P1(f11(x551,x552),x551)
% 106.42/106.59 [56]~P6(x561,x562,a82)+P1(f13(x561,x562),x561)
% 106.42/106.59 [57]~P6(x571,x572,a90)+P1(f15(x571,x572),x571)
% 106.42/106.59 [58]~P6(x581,x582,a90)+P1(f17(x581,x582),x582)
% 106.42/106.59 [59]~P6(x591,x592,a75)+P1(f18(x591,x592),x591)
% 106.42/106.59 [60]~P6(x601,x602,a87)+P1(f20(x601,x602),x601)
% 106.42/106.59 [61]~P6(x611,x612,a91)+P1(f25(x611,x612),x611)
% 106.42/106.59 [62]~P6(x621,x622,a91)+P1(f28(x621,x622),x622)
% 106.42/106.59 [63]~P6(x631,x632,a83)+P1(f33(x631,x632),x632)
% 106.42/106.59 [64]~P6(x641,x642,a89)+P1(f34(x641,x642),x642)
% 106.42/106.59 [65]~P6(x651,x652,a9)+P1(f38(x651,x652),x651)
% 106.42/106.59 [66]~P6(x661,x662,a79)+P1(f42(x661,x662),x662)
% 106.42/106.59 [67]~P6(x671,x672,a79)+P1(f42(x671,x672),x671)
% 106.42/106.59 [68]~P6(x681,x682,a79)+P1(f44(x681,x682),x681)
% 106.42/106.59 [69]~P3(x691,x692)+P6(f45(x691,x692),f46(x691,x692),x692)
% 106.42/106.59 [70]~P3(x701,x702)+P6(f45(x701,x702),f46(x701,x702),x701)
% 106.42/106.59 [71]~P4(x711,x712)+P6(f49(x711,x712),f50(x711,x712),x711)
% 106.42/106.59 [72]~P6(x721,x722,a9)+P1(f38(x721,x722),f74(x722))
% 106.42/106.59 [73]~P6(x731,x732,a79)+P1(f44(x731,x732),f74(x732))
% 106.42/106.59 [82]~P6(x821,x822,a90)+~P1(f17(x821,x822),x821)
% 106.42/106.59 [83]~P6(x831,x832,a75)+~P1(f21(x831,x832),x831)
% 106.42/106.59 [84]~P6(x841,x842,a87)+~P1(f26(x841,x842),x841)
% 106.42/106.59 [85]~P6(x851,x852,a91)+~P1(f28(x851,x852),x851)
% 106.42/106.59 [86]~P6(x861,x862,a91)+~P1(f30(x861,x862),x862)
% 106.42/106.59 [87]~P6(x871,x872,a89)+~P1(f39(x871,x872),x872)
% 106.42/106.59 [99]P2(x991,x992)+~P6(f41(x991,x992),f47(x991,x992),x992)
% 106.42/106.59 [102]~P4(x1021,x1022)+~P6(f49(x1021,x1022),f50(x1021,x1022),x1022)
% 106.42/106.59 [22]~P1(x223,x222)+P6(x221,x222,a80)
% 106.42/106.59 [23]~P1(x233,x231)+P6(x231,x232,a86)
% 106.42/106.59 [27]P1(x271,x272)+~P6(x273,x272,a82)
% 106.42/106.59 [28]P1(x281,x282)+~P6(x283,x282,a84)
% 106.42/106.59 [29]P1(x291,x292)+~P6(x293,x292,a87)
% 106.42/106.59 [30]P1(x301,x302)+~P6(x303,x302,a85)
% 106.42/106.59 [31]P1(x311,x312)+~P6(x312,x313,a84)
% 106.42/106.59 [32]P1(x321,x322)+~P6(x322,x323,a88)
% 106.42/106.59 [36]~P1(x361,x362)+~P6(x362,x363,a5)
% 106.42/106.59 [37]~P1(x371,x372)+~P6(x372,x373,a83)
% 106.42/106.59 [38]~P1(x381,x382)+~P6(x382,x383,a85)
% 106.42/106.59 [39]~P1(x391,x392)+~P6(x392,x393,a89)
% 106.42/106.59 [35]~P6(x353,x352,a88)+P1(x351,f74(x352))
% 106.42/106.59 [76]P6(x761,x762,a8)+P1(f60(x761,x762),x761)+P1(f72(x761,x762),x762)
% 106.42/106.59 [93]P6(x931,x932,a85)+P1(f36(x931,x932),x931)+~P1(f37(x931,x932),x932)
% 106.42/106.59 [98]P6(x981,x982,a84)+~P1(f23(x981,x982),x981)+~P1(f24(x981,x982),x982)
% 106.42/106.59 [101]P6(x1011,x1012,a88)+~P1(f40(x1011,x1012),x1011)+~P1(f43(x1011,x1012),f74(x1012))
% 106.42/106.59 [108]P7(x1081,x1082)+P6(f53(x1081,x1082),f54(x1081,x1082),x1082)+~P6(f53(x1081,x1082),f54(x1081,x1082),x1081)
% 106.42/106.59 [109]P7(x1091,x1092)+P6(f53(x1091,x1092),f54(x1091,x1092),x1091)+~P6(f53(x1091,x1092),f54(x1091,x1092),x1092)
% 106.42/106.59 [34]~P1(x343,x341)+~P1(x343,x342)+P6(x341,x342,a73)
% 106.42/106.59 [43]P1(x431,x432)+~P1(x431,x433)+~P6(x433,x432,a81)
% 106.42/106.59 [44]P1(x441,x442)+~P1(x441,x443)+~P6(x442,x443,a10)
% 106.42/106.59 [45]P1(x451,x452)+~P1(x451,x453)+~P6(x452,x453,a75)
% 106.42/106.59 [46]P1(x461,x462)+~P1(x461,x463)+~P6(x463,x462,a10)
% 106.42/106.59 [47]P1(x471,x472)+~P1(x471,x473)+~P6(x473,x472,a90)
% 106.42/106.59 [48]P1(x481,x482)+~P1(x481,x483)+~P6(x483,x482,a75)
% 106.42/106.59 [49]P1(x491,x492)+~P1(x491,x493)+~P6(x493,x492,a91)
% 106.42/106.59 [40]~P1(x403,x401)+P6(x401,x402,a9)+~P1(x403,f74(x402))
% 106.42/106.59 [41]~P1(x413,x412)+P6(x411,x412,a83)+P1(f32(x411,x412),x411)
% 106.42/106.59 [77]~P1(x773,x771)+P6(x771,x772,a82)+~P1(f14(x771,x772),x772)
% 106.42/106.59 [78]~P1(x783,x782)+~P6(x781,x782,a86)+P1(f29(x781,x782),x781)
% 106.42/106.59 [79]~P1(x793,x791)+~P6(x791,x792,a80)+P1(f52(x791,x792),x792)
% 106.42/106.59 [80]~P1(x803,x801)+~P6(x801,x802,a8)+P1(f77(x801,x802),x802)
% 106.42/106.59 [81]~P1(x813,x812)+~P6(x811,x812,a8)+P1(f78(x811,x812),x811)
% 106.42/106.59 [33]~P1(x333,x332)+~P1(x334,x331)+P6(x331,x332,a8)
% 106.42/106.59 [75]~P7(x754,x753)+P6(x751,x752,x753)+P6(x751,x752,x754)
% 106.42/106.59 [91]~P6(x913,x914,x911)+P4(x911,x912)+P6(x913,x914,x912)
% 106.42/106.59 [94]~P6(x941,x942,x944)+P6(x941,x942,x943)+~P2(x944,x943)
% 106.42/106.59 [100]~P6(x1003,x1004,x1001)+P3(x1001,x1002)+~P6(x1003,x1004,x1002)
% 106.42/106.59 [104]~P6(x1043,x1044,x1041)+~P5(x1041,x1042)+~P6(x1043,x1044,x1042)
% 106.42/106.59 [105]~P6(x1053,x1054,x1051)+~P7(x1051,x1052)+~P6(x1053,x1054,x1052)
% 106.42/106.59 [92]~P1(x923,x921)+P6(x921,x922,a10)+P1(f12(x921,x922),x922)+P1(f12(x921,x922),x921)
% 106.42/106.59 [106]~P1(x1063,x1061)+P6(x1061,x1062,a10)+~P1(f12(x1061,x1062),x1062)+~P1(f12(x1061,x1062),x1061)
% 106.42/106.59 [74]P1(x741,x742)+~P1(x744,x742)+P6(x743,x742,a89)+P1(f35(x743,x742),x743)
% 106.42/106.59 [90]P1(x901,x902)+~P1(x904,x902)+P6(x902,x903,a87)+~P1(f22(x902,x903),x903)
% 106.42/106.59 [88]~P1(x881,x883)+P1(x881,x882)+~P1(x884,x882)+P6(x882,x883,a90)+P1(f16(x882,x883),x882)
% 106.42/106.59 [89]~P1(x894,x891)+~P1(x893,x891)+~P1(x894,x892)+P6(x891,x892,a79)+~P1(x893,f74(x892))
% 106.42/106.59 [96]P1(x961,x962)+~P1(x964,x962)+P6(x962,x963,a75)+P1(f19(x962,x963),x963)+P1(f19(x962,x963),x962)
% 106.42/106.59 [97]~P1(x971,x973)+P1(x971,x972)+~P1(x974,x972)+P6(x972,x973,a90)+~P1(f16(x972,x973),x973)
% 106.42/106.59 [107]P1(x1071,x1072)+~P1(x1074,x1072)+P6(x1072,x1073,a75)+~P1(f19(x1072,x1073),x1073)+~P1(f19(x1072,x1073),x1072)
% 106.42/106.59 [95]~P1(x953,x952)+P1(x951,x952)+P1(x953,x954)+~P1(x955,x954)+P6(x954,x952,a91)+P1(f27(x954,x952),x954)
% 106.42/106.59 [103]~P1(x1033,x1032)+P1(x1031,x1032)+P1(x1033,x1034)+~P1(x1035,x1034)+P6(x1034,x1032,a91)+~P1(f27(x1034,x1032),x1032)
% 106.42/106.59 %EqnAxiom
% 106.42/106.59
% 106.42/106.59 %-------------------------------------------
% 106.56/106.61 cnf(110,plain,
% 106.56/106.61 (P6(a58,x1101,a5)),
% 106.56/106.62 inference(scs_inference,[],[14,21])).
% 106.56/106.62 cnf(111,plain,
% 106.56/106.62 (~P1(x1111,a58)),
% 106.56/106.62 inference(rename_variables,[],[14])).
% 106.56/106.62 cnf(113,plain,
% 106.56/106.62 (P6(x1131,a58,a86)),
% 106.56/106.62 inference(scs_inference,[],[14,111,21,24])).
% 106.56/106.62 cnf(114,plain,
% 106.56/106.62 (~P1(x1141,a58)),
% 106.56/106.62 inference(rename_variables,[],[14])).
% 106.56/106.62 cnf(116,plain,
% 106.56/106.62 (P6(a58,x1161,a80)),
% 106.56/106.62 inference(scs_inference,[],[14,111,114,21,24,25])).
% 106.56/106.62 cnf(117,plain,
% 106.56/106.62 (~P1(x1171,a58)),
% 106.56/106.62 inference(rename_variables,[],[14])).
% 106.56/106.62 cnf(119,plain,
% 106.56/106.62 (P6(a58,x1191,a81)),
% 106.56/106.62 inference(scs_inference,[],[14,111,114,117,21,24,25,26])).
% 106.56/106.62 cnf(120,plain,
% 106.56/106.62 (~P1(x1201,a58)),
% 106.56/106.62 inference(rename_variables,[],[14])).
% 106.56/106.62 cnf(122,plain,
% 106.56/106.62 (P6(x1221,a3,a81)),
% 106.56/106.62 inference(scs_inference,[],[8,14,111,114,117,21,24,25,26,42])).
% 106.56/106.62 cnf(123,plain,
% 106.56/106.62 (P1(x1231,a3)),
% 106.56/106.62 inference(rename_variables,[],[8])).
% 106.56/106.62 cnf(125,plain,
% 106.56/106.62 (~P1(a68,a62)),
% 106.56/106.62 inference(scs_inference,[],[8,14,111,114,117,11,21,24,25,26,42,15])).
% 106.56/106.62 cnf(127,plain,
% 106.56/106.62 (~P6(x1271,a58,a73)),
% 106.56/106.62 inference(scs_inference,[],[8,14,111,114,117,120,11,21,24,25,26,42,15,53])).
% 106.56/106.62 cnf(128,plain,
% 106.56/106.62 (~P1(x1281,a58)),
% 106.56/106.62 inference(rename_variables,[],[14])).
% 106.56/106.62 cnf(130,plain,
% 106.56/106.62 (~P6(a58,x1301,a73)),
% 106.56/106.62 inference(scs_inference,[],[8,14,111,114,117,120,128,11,21,24,25,26,42,15,53,54])).
% 106.56/106.62 cnf(131,plain,
% 106.56/106.62 (~P1(x1311,a58)),
% 106.56/106.62 inference(rename_variables,[],[14])).
% 106.56/106.62 cnf(133,plain,
% 106.56/106.62 (~P6(a58,x1331,a10)),
% 106.56/106.62 inference(scs_inference,[],[8,14,111,114,117,120,128,131,11,21,24,25,26,42,15,53,54,55])).
% 106.56/106.62 cnf(134,plain,
% 106.56/106.62 (~P1(x1341,a58)),
% 106.56/106.62 inference(rename_variables,[],[14])).
% 106.56/106.62 cnf(136,plain,
% 106.56/106.62 (~P6(a58,x1361,a82)),
% 106.56/106.62 inference(scs_inference,[],[8,14,111,114,117,120,128,131,134,11,21,24,25,26,42,15,53,54,55,56])).
% 106.56/106.62 cnf(137,plain,
% 106.56/106.62 (~P1(x1371,a58)),
% 106.56/106.62 inference(rename_variables,[],[14])).
% 106.56/106.62 cnf(139,plain,
% 106.56/106.62 (~P6(a58,x1391,a90)),
% 106.56/106.62 inference(scs_inference,[],[8,14,111,114,117,120,128,131,134,137,11,21,24,25,26,42,15,53,54,55,56,57])).
% 106.56/106.62 cnf(140,plain,
% 106.56/106.62 (~P1(x1401,a58)),
% 106.56/106.62 inference(rename_variables,[],[14])).
% 106.56/106.62 cnf(142,plain,
% 106.56/106.62 (~P6(x1421,a58,a90)),
% 106.56/106.62 inference(scs_inference,[],[8,14,111,114,117,120,128,131,134,137,140,11,21,24,25,26,42,15,53,54,55,56,57,58])).
% 106.56/106.62 cnf(143,plain,
% 106.56/106.62 (~P1(x1431,a58)),
% 106.56/106.62 inference(rename_variables,[],[14])).
% 106.56/106.62 cnf(145,plain,
% 106.56/106.62 (~P6(a58,x1451,a75)),
% 106.56/106.62 inference(scs_inference,[],[8,14,111,114,117,120,128,131,134,137,140,143,11,21,24,25,26,42,15,53,54,55,56,57,58,59])).
% 106.56/106.62 cnf(146,plain,
% 106.56/106.62 (~P1(x1461,a58)),
% 106.56/106.62 inference(rename_variables,[],[14])).
% 106.56/106.62 cnf(148,plain,
% 106.56/106.62 (~P6(a58,x1481,a87)),
% 106.56/106.62 inference(scs_inference,[],[8,14,111,114,117,120,128,131,134,137,140,143,146,11,21,24,25,26,42,15,53,54,55,56,57,58,59,60])).
% 106.56/106.62 cnf(149,plain,
% 106.56/106.62 (~P1(x1491,a58)),
% 106.56/106.62 inference(rename_variables,[],[14])).
% 106.56/106.62 cnf(152,plain,
% 106.56/106.62 (~P1(x1521,a58)),
% 106.56/106.62 inference(rename_variables,[],[14])).
% 106.56/106.62 cnf(154,plain,
% 106.56/106.62 (~P6(x1541,a58,a91)),
% 106.56/106.62 inference(scs_inference,[],[8,14,111,114,117,120,128,131,134,137,140,143,146,149,152,11,21,24,25,26,42,15,53,54,55,56,57,58,59,60,61,62])).
% 106.56/106.62 cnf(155,plain,
% 106.56/106.62 (~P1(x1551,a58)),
% 106.56/106.62 inference(rename_variables,[],[14])).
% 106.56/106.62 cnf(157,plain,
% 106.56/106.62 (~P6(x1571,a58,a83)),
% 106.56/106.62 inference(scs_inference,[],[8,14,111,114,117,120,128,131,134,137,140,143,146,149,152,155,11,21,24,25,26,42,15,53,54,55,56,57,58,59,60,61,62,63])).
% 106.56/106.62 cnf(158,plain,
% 106.56/106.62 (~P1(x1581,a58)),
% 106.56/106.62 inference(rename_variables,[],[14])).
% 106.56/106.62 cnf(160,plain,
% 106.56/106.62 (~P6(x1601,a58,a89)),
% 106.56/106.62 inference(scs_inference,[],[8,14,111,114,117,120,128,131,134,137,140,143,146,149,152,155,158,11,21,24,25,26,42,15,53,54,55,56,57,58,59,60,61,62,63,64])).
% 106.56/106.62 cnf(161,plain,
% 106.56/106.62 (~P1(x1611,a58)),
% 106.56/106.62 inference(rename_variables,[],[14])).
% 106.56/106.62 cnf(163,plain,
% 106.56/106.62 (~P6(a58,x1631,a9)),
% 106.56/106.62 inference(scs_inference,[],[8,14,111,114,117,120,128,131,134,137,140,143,146,149,152,155,158,161,11,21,24,25,26,42,15,53,54,55,56,57,58,59,60,61,62,63,64,65])).
% 106.56/106.62 cnf(164,plain,
% 106.56/106.62 (~P1(x1641,a58)),
% 106.56/106.62 inference(rename_variables,[],[14])).
% 106.56/106.62 cnf(166,plain,
% 106.56/106.62 (~P6(x1661,a58,a79)),
% 106.56/106.62 inference(scs_inference,[],[8,14,111,114,117,120,128,131,134,137,140,143,146,149,152,155,158,161,164,11,21,24,25,26,42,15,53,54,55,56,57,58,59,60,61,62,63,64,65,66])).
% 106.56/106.62 cnf(167,plain,
% 106.56/106.62 (~P1(x1671,a58)),
% 106.56/106.62 inference(rename_variables,[],[14])).
% 106.56/106.62 cnf(170,plain,
% 106.56/106.62 (~P1(x1701,a58)),
% 106.56/106.62 inference(rename_variables,[],[14])).
% 106.56/106.62 cnf(172,plain,
% 106.56/106.62 (~P6(a3,x1721,a90)),
% 106.56/106.62 inference(scs_inference,[],[8,123,14,111,114,117,120,128,131,134,137,140,143,146,149,152,155,158,161,164,167,11,21,24,25,26,42,15,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,82])).
% 106.56/106.62 cnf(173,plain,
% 106.56/106.62 (P1(x1731,a3)),
% 106.56/106.62 inference(rename_variables,[],[8])).
% 106.56/106.62 cnf(175,plain,
% 106.56/106.62 (~P6(a3,x1751,a75)),
% 106.56/106.62 inference(scs_inference,[],[8,123,173,14,111,114,117,120,128,131,134,137,140,143,146,149,152,155,158,161,164,167,11,21,24,25,26,42,15,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,82,83])).
% 106.56/106.62 cnf(176,plain,
% 106.56/106.62 (P1(x1761,a3)),
% 106.56/106.62 inference(rename_variables,[],[8])).
% 106.56/106.62 cnf(178,plain,
% 106.56/106.62 (~P6(a3,x1781,a87)),
% 106.56/106.62 inference(scs_inference,[],[8,123,173,176,14,111,114,117,120,128,131,134,137,140,143,146,149,152,155,158,161,164,167,11,21,24,25,26,42,15,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,82,83,84])).
% 106.56/106.62 cnf(179,plain,
% 106.56/106.62 (P1(x1791,a3)),
% 106.56/106.62 inference(rename_variables,[],[8])).
% 106.56/106.62 cnf(181,plain,
% 106.56/106.62 (~P6(a3,x1811,a91)),
% 106.56/106.62 inference(scs_inference,[],[8,123,173,176,179,14,111,114,117,120,128,131,134,137,140,143,146,149,152,155,158,161,164,167,11,21,24,25,26,42,15,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,82,83,84,85])).
% 106.56/106.62 cnf(182,plain,
% 106.56/106.62 (P1(x1821,a3)),
% 106.56/106.62 inference(rename_variables,[],[8])).
% 106.56/106.62 cnf(185,plain,
% 106.56/106.62 (P1(x1851,a3)),
% 106.56/106.62 inference(rename_variables,[],[8])).
% 106.56/106.62 cnf(188,plain,
% 106.56/106.62 (P1(x1881,a3)),
% 106.56/106.62 inference(rename_variables,[],[8])).
% 106.56/106.62 cnf(190,plain,
% 106.56/106.62 (P4(a5,a73)),
% 106.56/106.62 inference(scs_inference,[],[8,123,173,176,179,182,185,14,111,114,117,120,128,131,134,137,140,143,146,149,152,155,158,161,164,167,11,21,24,25,26,42,15,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,82,83,84,85,86,87,91])).
% 106.56/106.62 cnf(194,plain,
% 106.56/106.62 (P6(a58,a3,a85)),
% 106.56/106.62 inference(scs_inference,[],[8,123,173,176,179,182,185,188,14,111,114,117,120,128,131,134,137,140,143,146,149,152,155,158,161,164,167,170,11,21,24,25,26,42,15,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,82,83,84,85,86,87,91,75,93])).
% 106.56/106.62 cnf(195,plain,
% 106.56/106.62 (~P1(x1951,a58)),
% 106.56/106.62 inference(rename_variables,[],[14])).
% 106.56/106.62 cnf(196,plain,
% 106.56/106.62 (P1(x1961,a3)),
% 106.56/106.62 inference(rename_variables,[],[8])).
% 106.56/106.62 cnf(198,plain,
% 106.56/106.62 (~P6(a3,a58,a8)),
% 106.56/106.62 inference(scs_inference,[],[8,123,173,176,179,182,185,188,196,14,111,114,117,120,128,131,134,137,140,143,146,149,152,155,158,161,164,167,170,195,11,21,24,25,26,42,15,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,82,83,84,85,86,87,91,75,93,80])).
% 106.56/106.62 cnf(199,plain,
% 106.56/106.62 (~P1(x1991,a58)),
% 106.56/106.62 inference(rename_variables,[],[14])).
% 106.56/106.62 cnf(201,plain,
% 106.56/106.62 (~P6(a58,a3,a8)),
% 106.56/106.62 inference(scs_inference,[],[8,123,173,176,179,182,185,188,196,14,111,114,117,120,128,131,134,137,140,143,146,149,152,155,158,161,164,167,170,195,199,11,21,24,25,26,42,15,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,82,83,84,85,86,87,91,75,93,80,81])).
% 106.56/106.62 cnf(202,plain,
% 106.56/106.62 (~P1(x2021,a58)),
% 106.56/106.62 inference(rename_variables,[],[14])).
% 106.56/106.62 cnf(210,plain,
% 106.56/106.62 (P6(a3,a3,a10)),
% 106.56/106.62 inference(scs_inference,[],[8,123,173,176,179,182,185,188,196,14,111,114,117,120,128,131,134,137,140,143,146,149,152,155,158,161,164,167,170,195,199,11,21,24,25,26,42,15,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,82,83,84,85,86,87,91,75,93,80,81,100,104,105,106])).
% 106.56/106.62 cnf(211,plain,
% 106.56/106.62 (P1(x2111,a3)),
% 106.56/106.62 inference(rename_variables,[],[8])).
% 106.56/106.62 cnf(212,plain,
% 106.56/106.62 (P1(x2121,a3)),
% 106.56/106.62 inference(rename_variables,[],[8])).
% 106.56/106.62 cnf(214,plain,
% 106.56/106.62 (P6(a3,a3,a84)),
% 106.56/106.62 inference(scs_inference,[],[8,123,173,176,179,182,185,188,196,212,211,14,111,114,117,120,128,131,134,137,140,143,146,149,152,155,158,161,164,167,170,195,199,11,21,24,25,26,42,15,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,82,83,84,85,86,87,91,75,93,80,81,100,104,105,106,98])).
% 106.56/106.62 cnf(215,plain,
% 106.56/106.62 (P1(x2151,a3)),
% 106.56/106.62 inference(rename_variables,[],[8])).
% 106.56/106.62 cnf(218,plain,
% 106.56/106.62 (P6(a3,x2181,a88)+~P1(f43(a3,x2181),f74(x2181))),
% 106.56/106.62 inference(scs_inference,[],[8,123,173,176,179,182,185,188,196,212,215,211,14,111,114,117,120,128,131,134,137,140,143,146,149,152,155,158,161,164,167,170,195,199,11,21,24,25,26,42,15,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,82,83,84,85,86,87,91,75,93,80,81,100,104,105,106,98,101])).
% 106.56/106.62 cnf(222,plain,
% 106.56/106.62 (~P6(x2221,a58,a88)+P6(a3,a58,a88)),
% 106.56/106.62 inference(scs_inference,[],[8,123,173,176,179,182,185,188,196,212,215,211,14,111,114,117,120,128,131,134,137,140,143,146,149,152,155,158,161,164,167,170,195,199,202,11,21,24,25,26,42,15,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,82,83,84,85,86,87,91,75,93,80,81,100,104,105,106,98,101,17,35])).
% 106.56/106.62 cnf(229,plain,
% 106.56/106.62 (P3(a5,a86)),
% 106.56/106.62 inference(scs_inference,[],[110,113,100])).
% 106.56/106.62 cnf(230,plain,
% 106.56/106.62 (P6(x2301,a58,a86)),
% 106.56/106.62 inference(rename_variables,[],[113])).
% 106.56/106.62 cnf(231,plain,
% 106.56/106.62 (P6(a58,x2311,a5)),
% 106.56/106.62 inference(rename_variables,[],[110])).
% 106.56/106.62 cnf(233,plain,
% 106.56/106.62 (~P5(a5,a86)),
% 106.56/106.62 inference(scs_inference,[],[110,231,113,230,100,104])).
% 106.56/106.62 cnf(234,plain,
% 106.56/106.62 (P6(x2341,a58,a86)),
% 106.56/106.62 inference(rename_variables,[],[113])).
% 106.56/106.62 cnf(235,plain,
% 106.56/106.62 (P6(a58,x2351,a5)),
% 106.56/106.62 inference(rename_variables,[],[110])).
% 106.56/106.62 cnf(237,plain,
% 106.56/106.62 (~P6(a58,a2,a8)),
% 106.56/106.62 inference(scs_inference,[],[110,231,113,230,1,14,100,104,81])).
% 106.56/106.62 cnf(238,plain,
% 106.56/106.62 (~P1(x2381,a58)),
% 106.56/106.62 inference(rename_variables,[],[14])).
% 106.56/106.62 cnf(240,plain,
% 106.56/106.62 (P4(a5,a10)),
% 106.56/106.62 inference(scs_inference,[],[110,231,235,113,230,133,1,14,100,104,81,91])).
% 106.56/106.62 cnf(241,plain,
% 106.56/106.62 (~P6(a58,x2411,a10)),
% 106.56/106.62 inference(rename_variables,[],[133])).
% 106.56/106.62 cnf(243,plain,
% 106.56/106.62 (~P6(a2,a58,a8)),
% 106.56/106.62 inference(scs_inference,[],[110,231,235,113,230,133,1,14,238,100,104,81,91,80])).
% 106.56/106.62 cnf(254,plain,
% 106.56/106.62 (P6(a3,x2541,a84)+~P1(f24(a3,x2541),x2541)),
% 106.56/106.62 inference(scs_inference,[],[110,231,235,113,230,234,127,133,241,1,8,14,238,100,104,81,91,80,75,105,98])).
% 106.56/106.62 cnf(278,plain,
% 106.56/106.62 (P3(a85,a85)),
% 106.56/106.62 inference(scs_inference,[],[194,100])).
% 106.56/106.62 cnf(280,plain,
% 106.56/106.62 (P4(a86,a8)),
% 106.56/106.62 inference(scs_inference,[],[194,113,198,100,91])).
% 106.56/106.62 cnf(283,plain,
% 106.56/106.62 (~P5(a85,a85)),
% 106.56/106.62 inference(scs_inference,[],[194,113,198,100,91,104])).
% 106.56/106.62 cnf(289,plain,
% 106.56/106.62 (~P5(a5,a80)),
% 106.56/106.62 inference(scs_inference,[],[110,116,104])).
% 106.56/106.62 cnf(290,plain,
% 106.56/106.62 (P6(a58,x2901,a80)),
% 106.56/106.62 inference(rename_variables,[],[116])).
% 106.56/106.62 cnf(292,plain,
% 106.56/106.62 (P3(a5,a80)),
% 106.56/106.62 inference(scs_inference,[],[110,116,290,104,100])).
% 106.56/106.62 cnf(293,plain,
% 106.56/106.62 (P6(a58,x2931,a80)),
% 106.56/106.62 inference(rename_variables,[],[116])).
% 106.56/106.62 cnf(298,plain,
% 106.56/106.62 (P4(a5,a8)),
% 106.56/106.62 inference(scs_inference,[],[110,116,290,293,201,104,100,105,91])).
% 106.56/106.62 cnf(305,plain,
% 106.56/106.62 (~P6(a58,x3051,a82)),
% 106.56/106.62 inference(rename_variables,[],[136])).
% 106.56/106.62 cnf(307,plain,
% 106.56/106.62 (~P5(a5,a81)),
% 106.56/106.62 inference(scs_inference,[],[110,119,130,136,75,104])).
% 106.56/106.62 cnf(308,plain,
% 106.56/106.62 (P6(a58,x3081,a81)),
% 106.56/106.62 inference(rename_variables,[],[119])).
% 106.56/106.62 cnf(311,plain,
% 106.56/106.62 (P6(a58,x3111,a81)),
% 106.56/106.62 inference(rename_variables,[],[119])).
% 106.56/106.62 cnf(313,plain,
% 106.56/106.62 (P4(a5,a82)),
% 106.56/106.62 inference(scs_inference,[],[110,119,308,130,136,305,75,104,105,91])).
% 106.56/106.62 cnf(316,plain,
% 106.56/106.62 (P3(a5,a81)),
% 106.56/106.62 inference(scs_inference,[],[110,119,308,311,130,136,305,75,104,105,91,100])).
% 106.56/106.62 cnf(319,plain,
% 106.56/106.62 (P4(a5,a90)),
% 106.56/106.62 inference(scs_inference,[],[110,142,91])).
% 106.56/106.62 cnf(320,plain,
% 106.56/106.62 (~P6(x3201,a58,a90)),
% 106.56/106.62 inference(rename_variables,[],[142])).
% 106.56/106.62 cnf(323,plain,
% 106.56/106.62 (P3(a84,a84)),
% 106.56/106.62 inference(scs_inference,[],[110,214,142,91,100])).
% 106.56/106.62 cnf(330,plain,
% 106.56/106.62 (~P5(a84,a84)),
% 106.56/106.62 inference(scs_inference,[],[110,214,198,142,320,91,100,105,75,104])).
% 106.56/106.62 cnf(334,plain,
% 106.56/106.62 (~P7(a87,a8)),
% 106.56/106.62 inference(scs_inference,[],[210,201,148,105,75])).
% 106.56/106.62 cnf(335,plain,
% 106.56/106.62 (~P6(a58,x3351,a87)),
% 106.56/106.62 inference(rename_variables,[],[148])).
% 106.56/106.62 cnf(337,plain,
% 106.56/106.62 (~P5(a10,a10)),
% 106.56/106.62 inference(scs_inference,[],[210,201,148,105,75,104])).
% 106.56/106.62 cnf(339,plain,
% 106.56/106.62 (P4(a5,a87)),
% 106.56/106.62 inference(scs_inference,[],[110,210,201,148,335,105,75,104,91])).
% 106.56/106.62 cnf(342,plain,
% 106.56/106.62 (P3(a10,a10)),
% 106.56/106.62 inference(scs_inference,[],[110,210,201,148,335,105,75,104,91,100])).
% 106.56/106.62 cnf(344,plain,
% 106.56/106.62 (P4(a5,a91)),
% 106.56/106.62 inference(scs_inference,[],[110,154,91])).
% 106.56/106.62 cnf(352,plain,
% 106.56/106.62 (P4(a5,a83)),
% 106.56/106.62 inference(scs_inference,[],[110,157,91])).
% 106.56/106.62 cnf(359,plain,
% 106.56/106.62 (P4(a5,a89)),
% 106.56/106.62 inference(scs_inference,[],[110,160,91])).
% 106.56/106.62 cnf(367,plain,
% 106.56/106.62 (P4(a5,a9)),
% 106.56/106.62 inference(scs_inference,[],[110,163,91])).
% 106.56/106.62 cnf(373,plain,
% 106.56/106.62 (P4(a5,a79)),
% 106.56/106.62 inference(scs_inference,[],[110,166,91])).
% 106.56/106.62 cnf(380,plain,
% 106.56/106.62 (P4(a81,a90)),
% 106.56/106.62 inference(scs_inference,[],[122,172,91])).
% 106.56/106.62 cnf(394,plain,
% 106.56/106.62 (P4(a5,a75)),
% 106.56/106.62 inference(scs_inference,[],[110,145,91])).
% 106.56/106.62 cnf(400,plain,
% 106.56/106.62 (P4(a81,a75)),
% 106.56/106.62 inference(scs_inference,[],[122,175,91])).
% 106.56/106.62 cnf(408,plain,
% 106.56/106.62 (P4(a86,a90)),
% 106.56/106.62 inference(scs_inference,[],[113,172,91])).
% 106.56/106.62 cnf(415,plain,
% 106.56/106.62 (P4(a81,a87)),
% 106.56/106.62 inference(scs_inference,[],[122,178,91])).
% 106.56/106.62 cnf(422,plain,
% 106.56/106.62 (P4(a86,a91)),
% 106.56/106.62 inference(scs_inference,[],[113,181,91])).
% 106.56/106.62 cnf(429,plain,
% 106.56/106.62 (P4(a81,a91)),
% 106.56/106.62 inference(scs_inference,[],[122,181,91])).
% 106.56/106.62 cnf(442,plain,
% 106.56/106.62 (P4(a10,a75)),
% 106.56/106.62 inference(scs_inference,[],[210,175,91])).
% 106.56/106.62 cnf(445,plain,
% 106.56/106.62 (P4(a86,a75)),
% 106.56/106.62 inference(scs_inference,[],[113,175,91])).
% 106.56/106.62 cnf(449,plain,
% 106.56/106.62 (~P1(a61,f74(a65))),
% 106.56/106.62 inference(scs_inference,[],[4,20,15])).
% 106.56/106.62 cnf(450,plain,
% 106.56/106.62 (~P6(x4501,a65,a88)),
% 106.56/106.62 inference(scs_inference,[],[449,35])).
% 106.56/106.62 cnf(452,plain,
% 106.56/106.62 (P1(a61,a65)),
% 106.56/106.62 inference(scs_inference,[],[449,35,17])).
% 106.56/106.62 cnf(454,plain,
% 106.56/106.62 (~P1(f43(a3,a65),f74(a65))),
% 106.56/106.62 inference(scs_inference,[],[8,449,35,17,101])).
% 106.56/106.62 cnf(459,plain,
% 106.56/106.62 (~P6(a3,a65,x4591)+P4(x4591,a88)),
% 106.56/106.62 inference(scs_inference,[],[8,449,35,17,101,75,91])).
% 106.56/106.62 cnf(478,plain,
% 106.56/106.62 (P6(a65,x4781,a86)),
% 106.56/106.62 inference(scs_inference,[],[454,23,17])).
% 106.56/106.62 cnf(479,plain,
% 106.56/106.62 (P1(f43(a3,a65),a65)),
% 106.56/106.62 inference(scs_inference,[],[454,17])).
% 106.56/106.62 cnf(481,plain,
% 106.56/106.62 (~P5(a81,a86)),
% 106.56/106.62 inference(scs_inference,[],[122,478,454,17,104])).
% 106.56/106.62 cnf(482,plain,
% 106.56/106.62 (P6(a65,x4821,a86)),
% 106.56/106.62 inference(rename_variables,[],[478])).
% 106.56/106.62 cnf(483,plain,
% 106.56/106.62 (P6(x4831,a3,a81)),
% 106.56/106.62 inference(rename_variables,[],[122])).
% 106.56/106.62 cnf(485,plain,
% 106.56/106.62 (P3(a81,a86)),
% 106.56/106.62 inference(scs_inference,[],[122,483,478,482,454,17,104,100])).
% 106.56/106.62 cnf(486,plain,
% 106.56/106.62 (P6(a65,x4861,a86)),
% 106.56/106.62 inference(rename_variables,[],[478])).
% 106.56/106.62 cnf(487,plain,
% 106.56/106.62 (P6(x4871,a3,a81)),
% 106.56/106.62 inference(rename_variables,[],[122])).
% 106.56/106.62 cnf(493,plain,
% 106.56/106.62 (P4(a5,a88)),
% 106.56/106.62 inference(scs_inference,[],[110,122,483,487,478,482,486,454,450,17,104,100,105,91])).
% 106.56/106.62 cnf(501,plain,
% 106.56/106.62 (P4(a10,a87)),
% 106.56/106.62 inference(scs_inference,[],[210,178,91])).
% 106.56/106.62 cnf(508,plain,
% 106.56/106.62 (P4(a10,a90)),
% 106.56/106.62 inference(scs_inference,[],[210,172,91])).
% 106.56/106.62 cnf(514,plain,
% 106.56/106.62 (P4(a10,a91)),
% 106.56/106.62 inference(scs_inference,[],[210,181,91])).
% 106.56/106.62 cnf(520,plain,
% 106.56/106.62 (~P6(x5201,a58,a87)),
% 106.56/106.62 inference(scs_inference,[],[194,29,38])).
% 106.56/106.62 cnf(521,plain,
% 106.56/106.62 (~P6(a56,a58,a8)),
% 106.56/106.62 inference(scs_inference,[],[2,14,80])).
% 106.56/106.62 cnf(522,plain,
% 106.56/106.62 (~P1(x5221,a58)),
% 106.56/106.62 inference(rename_variables,[],[14])).
% 106.56/106.62 cnf(524,plain,
% 106.56/106.62 (~P6(a58,a56,a8)),
% 106.56/106.62 inference(scs_inference,[],[2,14,522,80,81])).
% 106.56/106.62 cnf(530,plain,
% 106.56/106.62 (~P6(f74(a65),x5301,a88)),
% 106.56/106.62 inference(scs_inference,[],[450,32,218])).
% 106.56/106.62 cnf(531,plain,
% 106.56/106.62 (P4(a81,a88)),
% 106.56/106.62 inference(scs_inference,[],[122,530,91])).
% 106.56/106.62 cnf(543,plain,
% 106.56/106.62 (~P6(a3,x5431,a83)),
% 106.56/106.62 inference(scs_inference,[],[214,37,28])).
% 106.56/106.62 cnf(544,plain,
% 106.56/106.62 (~P6(a59,a58,a8)),
% 106.56/106.62 inference(scs_inference,[],[3,14,80])).
% 106.56/106.62 cnf(545,plain,
% 106.56/106.62 (~P1(x5451,a58)),
% 106.56/106.62 inference(rename_variables,[],[14])).
% 106.56/106.62 cnf(547,plain,
% 106.56/106.62 (~P6(a58,a59,a8)),
% 106.56/106.62 inference(scs_inference,[],[3,14,545,80,81])).
% 106.56/106.62 cnf(550,plain,
% 106.56/106.62 (P4(a10,a83)),
% 106.56/106.62 inference(scs_inference,[],[3,210,14,545,543,80,81,91])).
% 106.56/106.62 cnf(553,plain,
% 106.56/106.62 (~P6(a3,x5531,a89)),
% 106.56/106.62 inference(scs_inference,[],[194,39,30])).
% 106.56/106.62 cnf(554,plain,
% 106.56/106.62 (P4(a10,a89)),
% 106.56/106.62 inference(scs_inference,[],[210,553,91])).
% 106.56/106.62 cnf(562,plain,
% 106.56/106.62 (~P6(f49(x5621,a88),f50(x5621,a88),a88)+~P6(a3,a65,x5621)),
% 106.56/106.62 inference(scs_inference,[],[459,102])).
% 106.56/106.62 cnf(563,plain,
% 106.56/106.62 (~P6(a62,a58,a8)),
% 106.56/106.63 inference(scs_inference,[],[4,14,80])).
% 106.56/106.63 cnf(564,plain,
% 106.56/106.63 (~P1(x5641,a58)),
% 106.56/106.63 inference(rename_variables,[],[14])).
% 106.56/106.63 cnf(566,plain,
% 106.56/106.63 (~P6(a58,a62,a8)),
% 106.56/106.63 inference(scs_inference,[],[4,14,564,80,81])).
% 106.56/106.63 cnf(569,plain,
% 106.56/106.63 (~P2(a88,a8)+~P6(x5691,a58,a88)),
% 106.56/106.63 inference(scs_inference,[],[198,222,94])).
% 106.56/106.63 cnf(570,plain,
% 106.56/106.63 (~P1(f43(a3,a58),f74(a58))+~P2(a88,a8)),
% 106.56/106.63 inference(scs_inference,[],[569,218])).
% 106.56/106.63 cnf(571,plain,
% 106.56/106.63 (~P6(a65,a58,a8)),
% 106.56/106.63 inference(scs_inference,[],[5,14,80])).
% 106.56/106.63 cnf(572,plain,
% 106.56/106.63 (~P1(x5721,a58)),
% 106.56/106.63 inference(rename_variables,[],[14])).
% 106.56/106.63 cnf(574,plain,
% 106.56/106.63 (~P6(a58,a65,a8)),
% 106.56/106.63 inference(scs_inference,[],[5,14,572,80,81])).
% 106.56/106.63 cnf(578,plain,
% 106.56/106.63 (P6(a3,f74(a58),a84)),
% 106.56/106.63 inference(scs_inference,[],[14,254,17])).
% 106.56/106.63 cnf(579,plain,
% 106.56/106.63 (P1(x5791,f74(a58))),
% 106.56/106.63 inference(scs_inference,[],[578,28])).
% 106.56/106.63 cnf(583,plain,
% 106.56/106.63 (~P6(a69,a58,a8)),
% 106.56/106.63 inference(scs_inference,[],[6,578,14,28,84,80])).
% 106.56/106.63 cnf(584,plain,
% 106.56/106.63 (~P1(x5841,a58)),
% 106.56/106.63 inference(rename_variables,[],[14])).
% 106.56/106.63 cnf(586,plain,
% 106.56/106.63 (~P6(a58,a69,a8)),
% 106.56/106.63 inference(scs_inference,[],[6,578,14,584,28,84,80,81])).
% 106.56/106.63 cnf(589,plain,
% 106.56/106.63 (~P2(a88,a8)),
% 106.56/106.63 inference(scs_inference,[],[579,570])).
% 106.56/106.63 cnf(592,plain,
% 106.56/106.63 (P1(x5921,f74(a58))),
% 106.56/106.63 inference(rename_variables,[],[579])).
% 106.56/106.63 cnf(595,plain,
% 106.56/106.63 (P1(x5951,f74(a58))),
% 106.56/106.63 inference(rename_variables,[],[579])).
% 106.56/106.63 cnf(598,plain,
% 106.56/106.63 (P1(x5981,f74(a58))),
% 106.56/106.63 inference(rename_variables,[],[579])).
% 106.56/106.63 cnf(601,plain,
% 106.56/106.63 (P1(x6011,f74(a58))),
% 106.56/106.63 inference(rename_variables,[],[579])).
% 106.56/106.63 cnf(604,plain,
% 106.56/106.63 (P1(x6041,f74(a58))),
% 106.56/106.63 inference(rename_variables,[],[579])).
% 106.56/106.63 cnf(606,plain,
% 106.56/106.63 (~P6(x6061,f74(a58),a91)),
% 106.56/106.63 inference(scs_inference,[],[579,592,595,598,601,604,83,42,82,87,85,86])).
% 106.56/106.63 cnf(607,plain,
% 106.56/106.63 (P1(x6071,f74(a58))),
% 106.56/106.63 inference(rename_variables,[],[579])).
% 106.56/106.63 cnf(610,plain,
% 106.56/106.63 (P1(x6101,f74(a58))),
% 106.56/106.63 inference(rename_variables,[],[579])).
% 106.56/106.63 cnf(611,plain,
% 106.56/106.63 (P1(x6111,a3)),
% 106.56/106.63 inference(rename_variables,[],[8])).
% 106.56/106.63 cnf(613,plain,
% 106.56/106.63 (P6(a3,a58,a88)),
% 106.56/106.63 inference(scs_inference,[],[8,611,579,592,595,598,601,604,607,610,83,42,82,87,85,86,98,101])).
% 106.56/106.63 cnf(617,plain,
% 106.56/106.63 (P3(a88,a88)),
% 106.56/106.63 inference(scs_inference,[],[8,611,579,592,595,598,601,604,607,610,83,42,82,87,85,86,98,101,100])).
% 106.56/106.63 cnf(619,plain,
% 106.56/106.63 (~P5(a88,a88)),
% 106.56/106.63 inference(scs_inference,[],[8,611,579,592,595,598,601,604,607,610,83,42,82,87,85,86,98,101,100,104])).
% 106.56/106.63 cnf(638,plain,
% 106.56/106.63 (P6(f48(a5,a5),f51(a5,a5),a5)),
% 106.56/106.63 inference(scs_inference,[],[110,51,104])).
% 106.56/106.63 cnf(639,plain,
% 106.56/106.63 (~P1(x6391,f48(a5,a5))),
% 106.56/106.63 inference(scs_inference,[],[638,36])).
% 106.56/106.63 cnf(648,plain,
% 106.56/106.63 (P1(x6481,f48(a84,a84))),
% 106.56/106.63 inference(scs_inference,[],[330,52,31])).
% 106.56/106.63 cnf(649,plain,
% 106.56/106.63 (~P6(f48(a5,a5),x6491,a73)),
% 106.56/106.63 inference(scs_inference,[],[639,54])).
% 106.56/106.63 cnf(650,plain,
% 106.56/106.63 (~P1(x6501,f48(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[639])).
% 106.56/106.63 cnf(652,plain,
% 106.56/106.63 (~P6(x6521,f48(a5,a5),a89)),
% 106.56/106.63 inference(scs_inference,[],[639,650,54,64])).
% 106.56/106.63 cnf(653,plain,
% 106.56/106.63 (~P1(x6531,f48(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[639])).
% 106.56/106.63 cnf(656,plain,
% 106.56/106.63 (~P1(x6561,f48(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[639])).
% 106.56/106.63 cnf(659,plain,
% 106.56/106.63 (~P1(x6591,f48(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[639])).
% 106.56/106.63 cnf(661,plain,
% 106.56/106.63 (P6(f48(a5,a5),x6611,a81)),
% 106.56/106.63 inference(scs_inference,[],[639,650,653,656,659,54,64,55,53,26])).
% 106.56/106.63 cnf(662,plain,
% 106.56/106.63 (~P1(x6621,f48(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[639])).
% 106.56/106.63 cnf(665,plain,
% 106.56/106.63 (~P1(x6651,f48(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[639])).
% 106.56/106.63 cnf(668,plain,
% 106.56/106.63 (~P1(x6681,f48(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[639])).
% 106.56/106.63 cnf(671,plain,
% 106.56/106.63 (~P1(x6711,f48(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[639])).
% 106.56/106.63 cnf(673,plain,
% 106.56/106.63 (~P6(f48(a5,a5),x6731,a75)),
% 106.56/106.63 inference(scs_inference,[],[639,650,653,656,659,662,665,668,671,54,64,55,53,26,60,25,63,59])).
% 106.56/106.63 cnf(674,plain,
% 106.56/106.63 (~P1(x6741,f48(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[639])).
% 106.56/106.63 cnf(677,plain,
% 106.56/106.63 (~P1(x6771,f48(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[639])).
% 106.56/106.63 cnf(680,plain,
% 106.56/106.63 (~P1(x6801,f48(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[639])).
% 106.56/106.63 cnf(683,plain,
% 106.56/106.63 (~P1(x6831,f48(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[639])).
% 106.56/106.63 cnf(686,plain,
% 106.56/106.63 (~P1(x6861,f48(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[639])).
% 106.56/106.63 cnf(689,plain,
% 106.56/106.63 (~P1(x6891,f48(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[639])).
% 106.56/106.63 cnf(692,plain,
% 106.56/106.63 (~P1(x6921,f48(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[639])).
% 106.56/106.63 cnf(694,plain,
% 106.56/106.63 (P6(x6941,f48(a5,a5),a86)),
% 106.56/106.63 inference(scs_inference,[],[639,650,653,656,659,662,665,668,671,674,677,680,683,686,689,692,54,64,55,53,26,60,25,63,59,58,56,61,21,65,57,24])).
% 106.56/106.63 cnf(695,plain,
% 106.56/106.63 (~P1(x6951,f48(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[639])).
% 106.56/106.63 cnf(698,plain,
% 106.56/106.63 (P1(x6981,f48(a84,a84))),
% 106.56/106.63 inference(rename_variables,[],[648])).
% 106.56/106.63 cnf(701,plain,
% 106.56/106.63 (~P1(x7011,f48(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[639])).
% 106.56/106.63 cnf(703,plain,
% 106.56/106.63 (~P6(x7031,f48(a5,a5),a79)),
% 106.56/106.63 inference(scs_inference,[],[639,650,653,656,659,662,665,668,671,674,677,680,683,686,689,692,695,701,648,54,64,55,53,26,60,25,63,59,58,56,61,21,65,57,24,83,62,66])).
% 106.56/106.63 cnf(704,plain,
% 106.56/106.63 (~P1(x7041,f48(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[639])).
% 106.56/106.63 cnf(707,plain,
% 106.56/106.63 (P1(x7071,f48(a84,a84))),
% 106.56/106.63 inference(rename_variables,[],[648])).
% 106.56/106.63 cnf(710,plain,
% 106.56/106.63 (P1(x7101,f48(a84,a84))),
% 106.56/106.63 inference(rename_variables,[],[648])).
% 106.56/106.63 cnf(713,plain,
% 106.56/106.63 (P1(x7131,f48(a84,a84))),
% 106.56/106.63 inference(rename_variables,[],[648])).
% 106.56/106.63 cnf(715,plain,
% 106.56/106.63 (P6(x7151,f48(a84,a84),a81)),
% 106.56/106.63 inference(scs_inference,[],[639,650,653,656,659,662,665,668,671,674,677,680,683,686,689,692,695,701,648,698,707,710,713,54,64,55,53,26,60,25,63,59,58,56,61,21,65,57,24,83,62,66,82,85,87,42])).
% 106.56/106.63 cnf(716,plain,
% 106.56/106.63 (P1(x7161,f48(a84,a84))),
% 106.56/106.63 inference(rename_variables,[],[648])).
% 106.56/106.63 cnf(719,plain,
% 106.56/106.63 (P1(x7191,f48(a84,a84))),
% 106.56/106.63 inference(rename_variables,[],[648])).
% 106.56/106.63 cnf(722,plain,
% 106.56/106.63 (P1(x7221,f48(a84,a84))),
% 106.56/106.63 inference(rename_variables,[],[648])).
% 106.56/106.63 cnf(724,plain,
% 106.56/106.63 (P6(a58,f48(a5,a5),a8)),
% 106.56/106.63 inference(scs_inference,[],[14,639,650,653,656,659,662,665,668,671,674,677,680,683,686,689,692,695,701,704,648,698,707,710,713,716,719,54,64,55,53,26,60,25,63,59,58,56,61,21,65,57,24,83,62,66,82,85,87,42,84,86,76])).
% 106.56/106.63 cnf(726,plain,
% 106.56/106.63 (~P1(x7261,f48(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[639])).
% 106.56/106.63 cnf(729,plain,
% 106.56/106.63 (~P1(x7291,f48(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[639])).
% 106.56/106.63 cnf(730,plain,
% 106.56/106.63 (P1(x7301,a3)),
% 106.56/106.63 inference(rename_variables,[],[8])).
% 106.56/106.63 cnf(734,plain,
% 106.56/106.63 (P1(x7341,f48(a84,a84))),
% 106.56/106.63 inference(rename_variables,[],[648])).
% 106.56/106.63 cnf(743,plain,
% 106.56/106.63 (P3(a81,a81)),
% 106.56/106.63 inference(scs_inference,[],[122,8,730,14,639,650,653,656,659,662,665,668,671,674,677,680,683,686,689,692,695,701,704,726,648,698,707,710,713,716,719,722,734,579,54,64,55,53,26,60,25,63,59,58,56,61,21,65,57,24,83,62,66,82,85,87,42,84,86,76,93,98,101,105,100])).
% 106.56/106.63 cnf(748,plain,
% 106.56/106.63 (~P5(a81,a81)),
% 106.56/106.63 inference(scs_inference,[],[6,122,8,730,14,639,650,653,656,659,662,665,668,671,674,677,680,683,686,689,692,695,701,704,726,729,648,698,707,710,713,716,719,722,734,579,54,64,55,53,26,60,25,63,59,58,56,61,21,65,57,24,83,62,66,82,85,87,42,84,86,76,93,98,101,105,100,81,104])).
% 106.56/106.63 cnf(775,plain,
% 106.56/106.63 (P6(f45(a5,a5),f46(a5,a5),a5)),
% 106.56/106.63 inference(scs_inference,[],[110,69,100])).
% 106.56/106.63 cnf(776,plain,
% 106.56/106.63 (~P1(x7761,f45(a5,a5))),
% 106.56/106.63 inference(scs_inference,[],[775,36])).
% 106.56/106.63 cnf(788,plain,
% 106.56/106.63 (P3(a8,a8)),
% 106.56/106.63 inference(scs_inference,[],[775,724,8,14,639,648,36,26,76,98,100])).
% 106.56/106.63 cnf(790,plain,
% 106.56/106.63 (~P5(a8,a8)),
% 106.56/106.63 inference(scs_inference,[],[775,724,8,14,639,648,36,26,76,98,100,104])).
% 106.56/106.63 cnf(811,plain,
% 106.56/106.63 (~P1(x8111,f45(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[776])).
% 106.56/106.63 cnf(813,plain,
% 106.56/106.63 (~P6(x8131,f45(a5,a5),a83)),
% 106.56/106.63 inference(scs_inference,[],[776,811,67,63])).
% 106.56/106.63 cnf(814,plain,
% 106.56/106.63 (~P1(x8141,f45(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[776])).
% 106.56/106.63 cnf(816,plain,
% 106.56/106.63 (~P6(f45(a5,a5),x8161,a10)),
% 106.56/106.63 inference(scs_inference,[],[776,811,814,67,63,55])).
% 106.56/106.63 cnf(817,plain,
% 106.56/106.63 (~P1(x8171,f45(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[776])).
% 106.56/106.63 cnf(820,plain,
% 106.56/106.63 (~P1(x8201,f45(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[776])).
% 106.56/106.63 cnf(823,plain,
% 106.56/106.63 (~P1(x8231,f45(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[776])).
% 106.56/106.63 cnf(826,plain,
% 106.56/106.63 (~P1(x8261,f45(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[776])).
% 106.56/106.63 cnf(829,plain,
% 106.56/106.63 (~P1(x8291,f45(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[776])).
% 106.56/106.63 cnf(831,plain,
% 106.56/106.63 (~P6(x8311,f45(a5,a5),a89)),
% 106.56/106.63 inference(scs_inference,[],[776,811,814,817,820,823,826,829,67,63,55,59,53,54,25,64])).
% 106.56/106.63 cnf(832,plain,
% 106.56/106.63 (~P1(x8321,f45(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[776])).
% 106.56/106.63 cnf(834,plain,
% 106.56/106.63 (~P6(x8341,f45(a5,a5),a91)),
% 106.56/106.63 inference(scs_inference,[],[776,811,814,817,820,823,826,829,832,67,63,55,59,53,54,25,64,62])).
% 106.56/106.63 cnf(835,plain,
% 106.56/106.63 (~P1(x8351,f45(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[776])).
% 106.56/106.63 cnf(838,plain,
% 106.56/106.63 (~P1(x8381,f45(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[776])).
% 106.56/106.63 cnf(840,plain,
% 106.56/106.63 (~P6(x8401,f45(a5,a5),a90)),
% 106.56/106.63 inference(scs_inference,[],[776,811,814,817,820,823,826,829,832,835,838,67,63,55,59,53,54,25,64,62,65,58])).
% 106.56/106.63 cnf(841,plain,
% 106.56/106.63 (~P1(x8411,f45(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[776])).
% 106.56/106.63 cnf(844,plain,
% 106.56/106.63 (~P1(x8441,f45(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[776])).
% 106.56/106.63 cnf(847,plain,
% 106.56/106.63 (~P1(x8471,f45(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[776])).
% 106.56/106.63 cnf(850,plain,
% 106.56/106.63 (~P1(x8501,f45(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[776])).
% 106.56/106.63 cnf(853,plain,
% 106.56/106.63 (~P1(x8531,f45(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[776])).
% 106.56/106.63 cnf(856,plain,
% 106.56/106.63 (~P1(x8561,f45(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[776])).
% 106.56/106.63 cnf(859,plain,
% 106.56/106.63 (~P1(x8591,f45(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[776])).
% 106.56/106.63 cnf(862,plain,
% 106.56/106.63 (~P1(x8621,f45(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[776])).
% 106.56/106.63 cnf(865,plain,
% 106.56/106.63 (~P1(x8651,f45(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[776])).
% 106.56/106.63 cnf(870,plain,
% 106.56/106.63 (~P1(x8701,f45(a5,a5))),
% 106.56/106.63 inference(rename_variables,[],[776])).
% 106.56/106.63 cnf(873,plain,
% 106.56/106.63 (P6(x8731,a3,a81)),
% 106.56/106.63 inference(rename_variables,[],[122])).
% 106.56/106.63 cnf(878,plain,
% 106.56/106.63 (P3(a80,a80)),
% 106.56/106.63 inference(scs_inference,[],[6,122,8,14,776,811,814,817,820,823,826,829,832,835,838,841,844,847,850,853,856,859,862,865,870,67,63,55,59,53,54,25,64,62,65,58,21,61,60,56,57,66,24,93,76,105,81,100])).
% 106.56/106.63 cnf(880,plain,
% 106.56/106.63 (~P5(a80,a80)),
% 106.56/106.63 inference(scs_inference,[],[6,122,8,14,776,811,814,817,820,823,826,829,832,835,838,841,844,847,850,853,856,859,862,865,870,67,63,55,59,53,54,25,64,62,65,58,21,61,60,56,57,66,24,93,76,105,81,100,104])).
% 106.56/106.63 cnf(885,plain,
% 106.56/106.63 (P4(a81,a10)),
% 106.56/106.63 inference(scs_inference,[],[6,122,873,8,14,776,811,814,817,820,823,826,829,832,835,838,841,844,847,850,853,856,859,862,865,870,649,673,67,63,55,59,53,54,25,64,62,65,58,21,61,60,56,57,66,24,93,76,105,81,100,104,75,91])).
% 106.56/106.63 cnf(914,plain,
% 106.56/106.63 (P1(x9141,f74(f46(a88,a88)))),
% 106.56/106.63 inference(scs_inference,[],[617,70,35])).
% 106.56/106.63 cnf(915,plain,
% 106.56/106.63 (~P1(x9151,f46(a88,a88))),
% 106.56/106.63 inference(scs_inference,[],[914,20])).
% 106.56/106.63 cnf(926,plain,
% 106.56/106.63 (~P1(x9261,f46(a88,a88))),
% 106.56/106.63 inference(rename_variables,[],[915])).
% 106.56/106.63 cnf(929,plain,
% 106.56/106.63 (~P1(x9291,f46(a88,a88))),
% 106.56/106.63 inference(rename_variables,[],[915])).
% 106.56/106.63 cnf(932,plain,
% 106.56/106.63 (~P1(x9321,f46(a88,a88))),
% 106.56/106.63 inference(rename_variables,[],[915])).
% 106.56/106.63 cnf(935,plain,
% 106.56/106.63 (~P1(x9351,f46(a88,a88))),
% 106.56/106.63 inference(rename_variables,[],[915])).
% 106.56/106.63 cnf(938,plain,
% 106.56/106.63 (~P1(x9381,f46(a88,a88))),
% 106.56/106.63 inference(rename_variables,[],[915])).
% 106.56/106.63 cnf(941,plain,
% 106.56/106.63 (~P1(x9411,f46(a88,a88))),
% 106.56/106.63 inference(rename_variables,[],[915])).
% 106.56/106.63 cnf(944,plain,
% 106.56/106.63 (~P1(x9441,f46(a88,a88))),
% 106.56/106.63 inference(rename_variables,[],[915])).
% 106.56/106.63 cnf(947,plain,
% 106.56/106.63 (~P1(x9471,f46(a88,a88))),
% 106.56/106.63 inference(rename_variables,[],[915])).
% 106.56/106.63 cnf(949,plain,
% 106.56/106.63 (~P6(f46(a88,a88),x9491,a73)),
% 106.56/106.63 inference(scs_inference,[],[915,926,929,932,935,938,941,944,947,53,64,59,55,62,25,63,26,54])).
% 106.56/106.63 cnf(950,plain,
% 106.56/106.63 (~P1(x9501,f46(a88,a88))),
% 106.56/106.63 inference(rename_variables,[],[915])).
% 106.56/106.63 cnf(953,plain,
% 106.56/106.63 (~P1(x9531,f46(a88,a88))),
% 106.56/106.63 inference(rename_variables,[],[915])).
% 106.56/106.63 cnf(956,plain,
% 106.56/106.63 (~P1(x9561,f46(a88,a88))),
% 106.56/106.63 inference(rename_variables,[],[915])).
% 106.56/106.63 cnf(959,plain,
% 106.56/106.63 (~P1(x9591,f46(a88,a88))),
% 106.56/106.63 inference(rename_variables,[],[915])).
% 106.56/106.63 cnf(962,plain,
% 106.56/106.63 (~P1(x9621,f46(a88,a88))),
% 106.56/106.63 inference(rename_variables,[],[915])).
% 106.56/106.63 cnf(965,plain,
% 106.56/106.63 (~P1(x9651,f46(a88,a88))),
% 106.56/106.63 inference(rename_variables,[],[915])).
% 106.56/106.63 cnf(968,plain,
% 106.56/106.63 (~P1(x9681,f46(a88,a88))),
% 106.56/106.63 inference(rename_variables,[],[915])).
% 106.56/106.63 cnf(971,plain,
% 106.56/106.63 (~P1(x9711,f46(a88,a88))),
% 106.56/106.63 inference(rename_variables,[],[915])).
% 106.56/106.63 cnf(974,plain,
% 106.56/106.63 (~P1(x9741,f46(a88,a88))),
% 106.56/106.63 inference(rename_variables,[],[915])).
% 106.56/106.63 cnf(977,plain,
% 106.56/106.63 (~P1(x9771,f46(a88,a88))),
% 106.56/106.63 inference(rename_variables,[],[915])).
% 106.56/106.63 cnf(980,plain,
% 106.56/106.63 (~P1(x9801,f46(a88,a88))),
% 106.56/106.63 inference(rename_variables,[],[915])).
% 106.56/106.63 cnf(984,plain,
% 106.56/106.63 (~P1(x9841,f46(a88,a88))),
% 106.56/106.63 inference(rename_variables,[],[915])).
% 106.56/106.63 cnf(995,plain,
% 106.56/106.63 (P6(x9951,a3,a81)),
% 106.56/106.63 inference(rename_variables,[],[122])).
% 106.56/106.63 cnf(997,plain,
% 106.56/106.63 (P3(a81,a80)),
% 106.56/106.63 inference(scs_inference,[],[6,122,995,8,14,579,915,926,929,932,935,938,941,944,947,950,953,956,959,962,965,968,971,974,977,980,984,914,53,64,59,55,62,25,63,26,54,60,61,21,24,65,58,56,66,57,93,76,101,80,105,100])).
% 106.56/106.63 cnf(1098,plain,
% 106.56/106.63 (~P2(x10981,a88)+~P6(f49(x10982,a88),f50(x10982,a88),x10981)+~P6(a3,a65,x10982)),
% 106.56/106.63 inference(scs_inference,[],[562,94])).
% 106.56/106.63 cnf(1103,plain,
% 106.56/106.63 (P3(a86,a86)),
% 106.56/106.63 inference(scs_inference,[],[113,105,100])).
% 106.56/106.63 cnf(1105,plain,
% 106.56/106.63 (~P5(a86,a86)),
% 106.56/106.63 inference(scs_inference,[],[113,105,100,104])).
% 106.56/106.63 cnf(1113,plain,
% 106.56/106.63 (P6(a58,x11131,a5)),
% 106.56/106.63 inference(rename_variables,[],[110])).
% 106.56/106.63 cnf(1114,plain,
% 106.56/106.63 (P6(x11141,a58,a86)),
% 106.56/106.63 inference(rename_variables,[],[113])).
% 106.56/106.63 cnf(1116,plain,
% 106.56/106.63 (P3(a86,a5)),
% 106.56/106.63 inference(scs_inference,[],[113,1114,110,1113,105,100])).
% 106.56/106.63 cnf(1117,plain,
% 106.56/106.63 (P6(a58,x11171,a5)),
% 106.56/106.63 inference(rename_variables,[],[110])).
% 106.56/106.63 cnf(1118,plain,
% 106.56/106.63 (P6(x11181,a58,a86)),
% 106.56/106.63 inference(rename_variables,[],[113])).
% 106.56/106.63 cnf(1120,plain,
% 106.56/106.63 (~P5(a86,a5)),
% 106.56/106.63 inference(scs_inference,[],[113,1114,1118,110,1113,1117,105,100,104])).
% 106.56/106.63 cnf(1129,plain,
% 106.56/106.63 (P6(a58,x11291,a81)),
% 106.56/106.63 inference(rename_variables,[],[119])).
% 106.56/106.63 cnf(1130,plain,
% 106.56/106.63 (P6(x11301,a58,a86)),
% 106.56/106.63 inference(rename_variables,[],[113])).
% 106.56/106.63 cnf(1132,plain,
% 106.56/106.63 (~P5(a86,a81)),
% 106.56/106.63 inference(scs_inference,[],[113,1130,119,1129,105,104])).
% 106.56/106.63 cnf(1133,plain,
% 106.56/106.63 (P6(a58,x11331,a81)),
% 106.56/106.63 inference(rename_variables,[],[119])).
% 106.56/106.63 cnf(1134,plain,
% 106.56/106.63 (P6(x11341,a58,a86)),
% 106.56/106.63 inference(rename_variables,[],[113])).
% 106.56/106.63 cnf(1136,plain,
% 106.56/106.63 (P3(a86,a81)),
% 106.56/106.63 inference(scs_inference,[],[113,1130,1134,119,1129,1133,105,104,100])).
% 106.56/106.63 cnf(1146,plain,
% 106.56/106.63 (P6(a58,x11461,a80)),
% 106.56/106.63 inference(rename_variables,[],[116])).
% 106.56/106.63 cnf(1147,plain,
% 106.56/106.63 (P6(x11471,a58,a86)),
% 106.56/106.63 inference(rename_variables,[],[113])).
% 106.56/106.63 cnf(1149,plain,
% 106.56/106.63 (P3(a86,a80)),
% 106.56/106.63 inference(scs_inference,[],[113,1147,116,1146,105,100])).
% 106.56/106.63 cnf(1150,plain,
% 106.56/106.63 (P6(a58,x11501,a80)),
% 106.56/106.63 inference(rename_variables,[],[116])).
% 106.56/106.63 cnf(1151,plain,
% 106.56/106.63 (P6(x11511,a58,a86)),
% 106.56/106.63 inference(rename_variables,[],[113])).
% 106.56/106.63 cnf(1153,plain,
% 106.56/106.63 (~P5(a86,a80)),
% 106.56/106.63 inference(scs_inference,[],[113,1147,1151,116,1146,1150,105,100,104])).
% 106.56/106.63 cnf(1155,plain,
% 106.56/106.63 (P6(x11551,a58,a86)),
% 106.56/106.63 inference(rename_variables,[],[113])).
% 106.56/106.63 cnf(1157,plain,
% 106.56/106.63 (P4(a86,a10)),
% 106.56/106.63 inference(scs_inference,[],[113,1147,1151,1155,116,1146,1150,816,105,100,104,91])).
% 106.56/106.63 cnf(1199,plain,
% 106.56/106.63 (~P5(a80,a5)),
% 106.56/106.63 inference(scs_inference,[],[116,110,105,104])).
% 106.56/106.63 cnf(1200,plain,
% 106.56/106.63 (P6(a58,x12001,a5)),
% 106.56/106.63 inference(rename_variables,[],[110])).
% 106.56/106.63 cnf(1202,plain,
% 106.56/106.63 (P3(a80,a5)),
% 106.56/106.63 inference(scs_inference,[],[116,110,1200,105,104,100])).
% 106.56/106.63 cnf(1211,plain,
% 106.56/106.63 (P3(a80,a81)),
% 106.56/106.63 inference(scs_inference,[],[116,110,122,105,100])).
% 106.56/106.63 cnf(1212,plain,
% 106.56/106.63 (P6(x12121,a3,a81)),
% 106.56/106.63 inference(rename_variables,[],[122])).
% 106.56/106.63 cnf(1213,plain,
% 106.56/106.63 (P6(a58,x12131,a80)),
% 106.56/106.63 inference(rename_variables,[],[116])).
% 106.56/106.63 cnf(1215,plain,
% 106.56/106.63 (~P5(a80,a81)),
% 106.56/106.63 inference(scs_inference,[],[116,1213,110,122,1212,105,100,104])).
% 106.56/106.63 cnf(1217,plain,
% 106.56/106.63 (P6(a58,x12171,a80)),
% 106.56/106.63 inference(rename_variables,[],[116])).
% 106.56/106.63 cnf(1219,plain,
% 106.56/106.63 (P4(a80,a8)),
% 106.56/106.63 inference(scs_inference,[],[116,1213,1217,110,122,1212,201,105,100,104,91])).
% 106.56/106.63 cnf(1222,plain,
% 106.56/106.63 (P6(a65,a3,a73)),
% 106.56/106.63 inference(scs_inference,[],[8,4,34,15])).
% 106.56/106.63 cnf(1225,plain,
% 106.56/106.63 (P6(a58,x12251,a80)),
% 106.56/106.63 inference(rename_variables,[],[116])).
% 106.56/106.63 cnf(1227,plain,
% 106.56/106.63 (P3(a80,a86)),
% 106.56/106.63 inference(scs_inference,[],[116,1225,122,113,105,100])).
% 106.56/106.63 cnf(1228,plain,
% 106.56/106.63 (P6(x12281,a58,a86)),
% 106.56/106.63 inference(rename_variables,[],[113])).
% 106.56/106.63 cnf(1229,plain,
% 106.56/106.63 (P6(a58,x12291,a80)),
% 106.56/106.63 inference(rename_variables,[],[116])).
% 106.56/106.63 cnf(1231,plain,
% 106.56/106.63 (~P5(a80,a86)),
% 106.56/106.63 inference(scs_inference,[],[116,1225,1229,122,113,1228,105,100,104])).
% 106.56/106.63 cnf(1233,plain,
% 106.56/106.63 (P6(a58,x12331,a80)),
% 106.56/106.63 inference(rename_variables,[],[116])).
% 106.56/106.63 cnf(1235,plain,
% 106.56/106.63 (P4(a80,a88)),
% 106.56/106.63 inference(scs_inference,[],[116,1225,1229,1233,122,113,1228,450,105,100,104,91])).
% 106.56/106.63 cnf(1244,plain,
% 106.56/106.63 (P3(a73,a73)),
% 106.56/106.63 inference(scs_inference,[],[116,113,1222,105,100])).
% 106.56/106.63 cnf(1246,plain,
% 106.56/106.63 (~P5(a73,a73)),
% 106.56/106.63 inference(scs_inference,[],[116,113,1222,105,100,104])).
% 106.56/106.63 cnf(1253,plain,
% 106.56/106.63 (P4(a80,a83)),
% 106.56/106.63 inference(scs_inference,[],[116,813,91])).
% 106.56/106.63 cnf(1257,plain,
% 106.56/106.63 (~P6(x12571,a58,a75)+P6(x12571,x12572,a5)),
% 106.56/106.63 inference(scs_inference,[],[14,48,21])).
% 106.56/106.63 cnf(1258,plain,
% 106.56/106.63 (P4(a80,a89)),
% 106.56/106.63 inference(scs_inference,[],[116,831,91])).
% 106.56/106.63 cnf(1262,plain,
% 106.56/106.63 (P2(x12621,a5)+~P6(f41(x12621,a5),a58,a75)),
% 106.56/106.63 inference(scs_inference,[],[1257,99])).
% 106.56/106.63 cnf(1267,plain,
% 106.56/106.63 (~P2(a86,a75)+P2(x12671,a5)),
% 106.56/106.63 inference(scs_inference,[],[113,1262,94])).
% 106.56/106.63 cnf(1268,plain,
% 106.56/106.63 (P4(a80,a87)),
% 106.56/106.63 inference(scs_inference,[],[116,520,91])).
% 106.56/106.63 cnf(1273,plain,
% 106.56/106.63 (P4(a80,a91)),
% 106.56/106.63 inference(scs_inference,[],[116,606,91])).
% 106.56/106.63 cnf(1278,plain,
% 106.56/106.63 (P4(a80,a90)),
% 106.56/106.63 inference(scs_inference,[],[116,840,91])).
% 106.56/106.63 cnf(1292,plain,
% 106.56/106.63 (~P6(x12921,a58,a84)),
% 106.56/106.63 inference(scs_inference,[],[113,14,78,28])).
% 106.56/106.63 cnf(1297,plain,
% 106.56/106.63 (P4(a80,a75)),
% 106.56/106.63 inference(scs_inference,[],[116,130,145,1292,75,91])).
% 106.56/106.63 cnf(1300,plain,
% 106.56/106.63 (~P6(x13001,a58,a85)),
% 106.56/106.63 inference(scs_inference,[],[116,14,79,30])).
% 106.56/106.63 cnf(1302,plain,
% 106.56/106.63 (~P6(x13021,a58,a85)),
% 106.56/106.63 inference(rename_variables,[],[1300])).
% 106.56/106.63 cnf(1305,plain,
% 106.56/106.63 (P4(a80,a85)),
% 106.56/106.63 inference(scs_inference,[],[116,130,1300,1302,75,91])).
% 106.56/106.63 cnf(1310,plain,
% 106.56/106.63 (P4(a80,a84)),
% 106.56/106.63 inference(scs_inference,[],[116,1292,91])).
% 106.56/106.63 cnf(1348,plain,
% 106.56/106.63 (P3(a81,a5)),
% 106.56/106.63 inference(scs_inference,[],[119,110,100])).
% 106.56/106.63 cnf(1349,plain,
% 106.56/106.63 (P6(a58,x13491,a5)),
% 106.56/106.63 inference(rename_variables,[],[110])).
% 106.56/106.63 cnf(1351,plain,
% 106.56/106.63 (~P5(a81,a5)),
% 106.56/106.63 inference(scs_inference,[],[119,110,1349,100,104])).
% 106.56/106.63 cnf(1358,plain,
% 106.56/106.63 (~P5(a81,a80)),
% 106.56/106.63 inference(scs_inference,[],[119,116,104])).
% 106.56/106.63 cnf(1419,plain,
% 106.56/106.63 (P6(x14191,a65,a80)),
% 106.56/106.63 inference(scs_inference,[],[4,15,22])).
% 106.56/106.63 cnf(1421,plain,
% 106.56/106.63 (P6(x14211,a65,a80)),
% 106.56/106.63 inference(rename_variables,[],[1419])).
% 106.56/106.63 cnf(1427,plain,
% 106.56/106.63 (~P6(f49(a80,a88),f50(a80,a88),x14271)+~P2(x14271,a88)),
% 106.56/106.63 inference(scs_inference,[],[133,1419,1421,834,562,75,1098])).
% 106.56/106.63 cnf(1458,plain,
% 106.56/106.63 (~P2(a80,a88)),
% 106.56/106.63 inference(scs_inference,[],[1235,1427,71])).
% 106.56/106.63 cnf(1567,plain,
% 106.56/106.63 (P1(a68,f74(a62))),
% 106.56/106.63 inference(scs_inference,[],[11,15,17])).
% 106.56/106.63 cnf(1571,plain,
% 106.56/106.63 (~P6(a65,x15711,a5)),
% 106.56/106.63 inference(scs_inference,[],[4,15,36])).
% 106.56/106.63 cnf(1580,plain,
% 106.56/106.63 (~P6(x15801,a62,a82)),
% 106.56/106.63 inference(scs_inference,[],[11,15,27])).
% 106.56/106.63 cnf(1584,plain,
% 106.56/106.63 (~P6(a65,x15841,a83)),
% 106.56/106.63 inference(scs_inference,[],[4,15,37])).
% 106.56/106.63 cnf(1588,plain,
% 106.56/106.63 (~P6(x15881,a62,a84)),
% 106.56/106.63 inference(scs_inference,[],[11,15,28])).
% 106.56/106.63 cnf(1589,plain,
% 106.56/106.63 (~P1(f24(a3,a62),a62)),
% 106.56/106.63 inference(scs_inference,[],[1588,254])).
% 106.56/106.63 cnf(1596,plain,
% 106.56/106.63 (~P6(a65,x15961,a85)),
% 106.56/106.63 inference(scs_inference,[],[4,15,38])).
% 106.56/106.63 cnf(1601,plain,
% 106.56/106.63 (~P6(x16011,a62,a87)),
% 106.56/106.63 inference(scs_inference,[],[11,15,29])).
% 106.56/106.63 cnf(1602,plain,
% 106.56/106.63 (~P6(a65,x16021,a89)),
% 106.56/106.63 inference(scs_inference,[],[4,15,39])).
% 106.56/106.63 cnf(1611,plain,
% 106.56/106.63 (P6(a65,a58,a9)),
% 106.56/106.63 inference(scs_inference,[],[4,579,15,40])).
% 106.56/106.63 cnf(1612,plain,
% 106.56/106.63 (P3(a9,a9)),
% 106.56/106.63 inference(scs_inference,[],[1611,100])).
% 106.56/106.63 cnf(1614,plain,
% 106.56/106.63 (~P5(a9,a9)),
% 106.56/106.63 inference(scs_inference,[],[1611,100,104])).
% 106.56/106.63 cnf(1620,plain,
% 106.56/106.63 (~P6(a62,x16201,a84)),
% 106.56/106.63 inference(scs_inference,[],[11,15,31])).
% 106.56/106.63 cnf(1625,plain,
% 106.56/106.63 (P6(a58,a65,a83)),
% 106.56/106.63 inference(scs_inference,[],[4,14,15,41])).
% 106.56/106.63 cnf(1628,plain,
% 106.56/106.63 (P3(a83,a83)),
% 106.56/106.63 inference(scs_inference,[],[1625,105,100])).
% 106.56/106.63 cnf(1630,plain,
% 106.56/106.63 (~P5(a83,a83)),
% 106.56/106.63 inference(scs_inference,[],[1625,105,100,104])).
% 106.56/106.63 cnf(1636,plain,
% 106.56/106.63 (~P6(a62,x16361,a88)),
% 106.56/106.63 inference(scs_inference,[],[11,15,32])).
% 106.56/106.63 cnf(1645,plain,
% 106.56/106.63 (~P6(a62,a3,a10)),
% 106.56/106.63 inference(scs_inference,[],[11,8,15,44])).
% 106.56/106.63 cnf(1650,plain,
% 106.56/106.63 (~P6(a65,a58,a75)),
% 106.56/106.63 inference(scs_inference,[],[4,14,15,48])).
% 106.56/106.63 cnf(1654,plain,
% 106.56/106.63 (~P6(a62,a3,a75)),
% 106.56/106.63 inference(scs_inference,[],[11,8,15,45])).
% 106.56/106.63 cnf(1659,plain,
% 106.56/106.63 (P6(a65,a3,a82)),
% 106.56/106.63 inference(scs_inference,[],[4,8,15,77])).
% 106.56/106.63 cnf(1660,plain,
% 106.56/106.63 (P3(a82,a82)),
% 106.56/106.63 inference(scs_inference,[],[1659,100])).
% 106.56/106.63 cnf(1662,plain,
% 106.56/106.63 (~P5(a82,a82)),
% 106.56/106.63 inference(scs_inference,[],[1659,100,104])).
% 106.56/106.63 cnf(1667,plain,
% 106.56/106.63 (P1(f60(a62,a58),a65)),
% 106.56/106.63 inference(scs_inference,[],[14,563,15,76])).
% 106.56/106.63 cnf(1671,plain,
% 106.56/106.63 (~P6(a58,a65,a86)),
% 106.56/106.63 inference(scs_inference,[],[4,14,15,78])).
% 106.56/106.63 cnf(1679,plain,
% 106.56/106.63 (~P6(a3,a62,a10)),
% 106.56/106.63 inference(scs_inference,[],[11,8,15,46])).
% 106.56/106.63 cnf(1754,plain,
% 106.56/106.63 (~P6(a65,a58,a80)),
% 106.56/106.63 inference(scs_inference,[],[4,14,15,79])).
% 106.56/106.63 cnf(1767,plain,
% 106.56/106.63 (P6(a58,a65,a89)),
% 106.56/106.63 inference(scs_inference,[],[4,14,11,15,74])).
% 106.56/106.63 cnf(1770,plain,
% 106.56/106.63 (P3(a89,a89)),
% 106.56/106.63 inference(scs_inference,[],[1767,105,100])).
% 106.56/106.63 cnf(1772,plain,
% 106.56/106.63 (~P5(a89,a89)),
% 106.56/106.63 inference(scs_inference,[],[1767,105,100,104])).
% 106.56/106.63 cnf(1778,plain,
% 106.56/106.63 (P6(a62,a3,a87)),
% 106.56/106.63 inference(scs_inference,[],[11,8,4,15,90])).
% 106.56/106.63 cnf(1779,plain,
% 106.56/106.63 (P3(a87,a87)),
% 106.56/106.63 inference(scs_inference,[],[1778,100])).
% 106.56/106.63 cnf(1781,plain,
% 106.56/106.63 (~P5(a87,a87)),
% 106.56/106.63 inference(scs_inference,[],[1778,100,104])).
% 106.56/106.63 cnf(1787,plain,
% 106.56/106.63 (~P1(f39(a58,a65),a62)),
% 106.56/106.63 inference(scs_inference,[],[1767,15,87])).
% 106.56/106.63 cnf(1803,plain,
% 106.56/106.63 (P6(a58,a62,a89)),
% 106.56/106.63 inference(scs_inference,[],[11,14,4,15,74])).
% 106.56/106.63 cnf(1808,plain,
% 106.56/106.63 (P6(a65,a3,a87)),
% 106.56/106.63 inference(scs_inference,[],[4,8,11,15,90])).
% 106.56/106.63 cnf(1813,plain,
% 106.56/106.63 (~P1(f26(a65,a3),a62)),
% 106.56/106.63 inference(scs_inference,[],[1808,15,84])).
% 106.56/106.63 cnf(1817,plain,
% 106.56/106.63 (~P1(f19(a62,a3),a62)),
% 106.56/106.63 inference(scs_inference,[],[11,8,1654,4,15,107])).
% 106.56/106.63 cnf(1822,plain,
% 106.56/106.63 (P1(f19(a65,a58),a65)),
% 106.56/106.63 inference(scs_inference,[],[4,14,1650,11,15,96])).
% 106.56/106.63 cnf(1864,plain,
% 106.56/106.63 (P6(a65,a3,a75)+~P1(f19(a65,a3),a62)),
% 106.56/106.63 inference(scs_inference,[],[8,11,15,107])).
% 106.56/106.63 cnf(1865,plain,
% 106.56/106.63 (~P1(f19(a65,a3),a62)),
% 106.56/106.63 inference(scs_inference,[],[11,8,1864,45])).
% 106.56/106.63 cnf(1873,plain,
% 106.56/106.63 (~P6(a59,a3,a10)+~P1(a63,a56)),
% 106.56/106.63 inference(scs_inference,[],[8,18,44])).
% 106.56/106.63 cnf(1877,plain,
% 106.56/106.63 (~P2(a81,a10)+~P1(a63,a56)),
% 106.56/106.63 inference(scs_inference,[],[122,1873,94])).
% 106.56/106.63 cnf(1896,plain,
% 106.56/106.63 (~P6(a56,a3,a75)+~P1(a64,a59)),
% 106.56/106.63 inference(scs_inference,[],[8,18,45])).
% 106.56/106.63 cnf(1901,plain,
% 106.56/106.63 (~P2(a81,a75)+~P1(a64,a59)),
% 106.56/106.63 inference(scs_inference,[],[122,1896,94])).
% 106.56/106.63 cnf(2107,plain,
% 106.56/106.63 (P1(x21071,f74(a58))),
% 106.56/106.63 inference(rename_variables,[],[579])).
% 106.56/106.63 cnf(2109,plain,
% 106.56/106.63 (P6(a58,f74(a58),a85)),
% 106.56/106.63 inference(scs_inference,[],[14,579,2107,648,98,93])).
% 106.56/106.63 cnf(2944,plain,
% 106.56/106.63 (P6(a58,x29441,a5)),
% 106.56/106.63 inference(rename_variables,[],[110])).
% 106.56/106.63 cnf(2949,plain,
% 106.56/106.63 (~P5(a85,a5)),
% 106.56/106.63 inference(scs_inference,[],[194,110,2944,130,105,91,104])).
% 106.56/106.63 cnf(2950,plain,
% 106.56/106.63 (P6(a58,x29501,a5)),
% 106.56/106.63 inference(rename_variables,[],[110])).
% 106.56/106.63 cnf(2952,plain,
% 106.56/106.63 (P3(a85,a5)),
% 106.56/106.63 inference(scs_inference,[],[194,110,2944,2950,130,105,91,104,100])).
% 106.56/106.63 cnf(2958,plain,
% 106.56/106.63 (~P5(a85,a81)),
% 106.56/106.63 inference(scs_inference,[],[194,122,201,91,104])).
% 106.56/106.63 cnf(2959,plain,
% 106.56/106.63 (P6(x29591,a3,a81)),
% 106.56/106.63 inference(rename_variables,[],[122])).
% 106.56/106.63 cnf(2962,plain,
% 106.56/106.63 (P6(x29621,a3,a81)),
% 106.56/106.63 inference(rename_variables,[],[122])).
% 106.56/106.63 cnf(2964,plain,
% 106.56/106.63 (P3(a85,a81)),
% 106.56/106.63 inference(scs_inference,[],[194,122,2959,2962,201,91,104,105,100])).
% 106.56/106.63 cnf(2968,plain,
% 106.56/106.63 (~P5(a85,a80)),
% 106.56/106.63 inference(scs_inference,[],[194,116,104])).
% 106.56/106.63 cnf(2969,plain,
% 106.56/106.63 (P6(a58,x29691,a80)),
% 106.56/106.63 inference(rename_variables,[],[116])).
% 106.56/106.63 cnf(2975,plain,
% 106.56/106.63 (P6(a58,x29751,a80)),
% 106.56/106.63 inference(rename_variables,[],[116])).
% 106.56/106.63 cnf(2977,plain,
% 106.56/106.63 (P3(a85,a80)),
% 106.56/106.63 inference(scs_inference,[],[194,116,2969,2975,139,104,91,105,100])).
% 106.56/106.63 cnf(3027,plain,
% 106.56/106.63 (~P5(a10,a81)),
% 106.56/106.63 inference(scs_inference,[],[210,122,104])).
% 106.56/106.63 cnf(3028,plain,
% 106.56/106.63 (P6(x30281,a3,a81)),
% 106.56/106.63 inference(rename_variables,[],[122])).
% 106.56/106.63 cnf(3031,plain,
% 106.56/106.63 (P6(x30311,a3,a81)),
% 106.56/106.63 inference(rename_variables,[],[122])).
% 106.56/106.63 cnf(3033,plain,
% 106.56/106.63 (P3(a10,a81)),
% 106.56/106.63 inference(scs_inference,[],[210,122,3028,3031,104,105,100])).
% 106.56/106.63 cnf(3038,plain,
% 106.56/106.63 (~P5(a84,a81)),
% 106.56/106.63 inference(scs_inference,[],[214,122,104])).
% 106.56/106.63 cnf(3039,plain,
% 106.56/106.63 (P6(x30391,a3,a81)),
% 106.56/106.63 inference(rename_variables,[],[122])).
% 106.56/106.63 cnf(3042,plain,
% 106.56/106.63 (P6(x30421,a3,a81)),
% 106.56/106.63 inference(rename_variables,[],[122])).
% 106.56/106.63 cnf(3044,plain,
% 106.56/106.63 (P3(a84,a81)),
% 106.56/106.63 inference(scs_inference,[],[214,122,3039,3042,104,105,100])).
% 106.56/106.63 cnf(3262,plain,
% 106.56/106.63 (~P2(a86,a75)),
% 106.56/106.63 inference(scs_inference,[],[1571,1419,1267,94])).
% 106.56/106.63 cnf(3286,plain,
% 106.56/106.63 (~P2(a81,a10)+~P6(a56,a3,a10)),
% 106.56/106.63 inference(scs_inference,[],[8,1877,44])).
% 106.56/106.63 cnf(3287,plain,
% 106.56/106.63 (~P2(a81,a10)),
% 106.56/106.63 inference(scs_inference,[],[122,3286,94])).
% 106.56/106.63 cnf(3288,plain,
% 106.56/106.63 (~P2(a81,a75)+~P6(a59,a3,a75)),
% 106.56/106.63 inference(scs_inference,[],[8,1901,45])).
% 106.56/106.63 cnf(3289,plain,
% 106.56/106.63 (~P2(a81,a75)),
% 106.56/106.63 inference(scs_inference,[],[122,3288,94])).
% 106.56/106.63 cnf(3310,plain,
% 106.56/106.63 (~P5(a88,a86)),
% 106.56/106.63 inference(scs_inference,[],[613,113,104])).
% 106.56/106.63 cnf(3311,plain,
% 106.56/106.63 (P6(x33111,a58,a86)),
% 106.56/106.63 inference(rename_variables,[],[113])).
% 106.56/106.63 cnf(3314,plain,
% 106.56/106.63 (P6(x33141,a58,a86)),
% 106.56/106.63 inference(rename_variables,[],[113])).
% 106.56/106.63 cnf(3316,plain,
% 106.56/106.63 (P3(a88,a86)),
% 106.56/106.63 inference(scs_inference,[],[613,113,3311,3314,104,105,100])).
% 106.56/106.63 cnf(3377,plain,
% 106.56/106.63 (P6(f46(a88,a88),f48(a5,a5),a8)),
% 106.56/106.63 inference(scs_inference,[],[639,915,76])).
% 106.56/106.63 cnf(3805,plain,
% 106.56/106.63 (P1(x38051,f48(a84,a84))),
% 106.56/106.63 inference(rename_variables,[],[648])).
% 106.56/106.63 cnf(3810,plain,
% 106.56/106.63 (P6(a58,f48(a84,a84),a85)),
% 106.56/106.63 inference(scs_inference,[],[648,3805,14,579,915,98,80,93])).
% 106.56/106.63 cnf(3833,plain,
% 106.56/106.63 (P6(f48(a5,a5),f48(a84,a84),a85)),
% 106.56/106.63 inference(scs_inference,[],[648,639,93])).
% 106.56/106.63 cnf(3873,plain,
% 106.56/106.63 (~P5(a8,a5)),
% 106.56/106.63 inference(scs_inference,[],[724,110,104])).
% 106.56/106.63 cnf(3874,plain,
% 106.56/106.63 (P6(a58,x38741,a5)),
% 106.56/106.63 inference(rename_variables,[],[110])).
% 106.56/106.63 cnf(3880,plain,
% 106.56/106.63 (P6(a58,x38801,a5)),
% 106.56/106.63 inference(rename_variables,[],[110])).
% 106.56/106.63 cnf(3882,plain,
% 106.56/106.63 (P3(a8,a5)),
% 106.56/106.63 inference(scs_inference,[],[724,110,3874,3880,130,104,91,105,100])).
% 106.56/106.63 cnf(3886,plain,
% 106.56/106.63 (~P5(a8,a81)),
% 106.56/106.63 inference(scs_inference,[],[724,119,104])).
% 106.56/106.63 cnf(3887,plain,
% 106.56/106.63 (P6(a58,x38871,a81)),
% 106.56/106.63 inference(rename_variables,[],[119])).
% 106.56/106.63 cnf(3893,plain,
% 106.56/106.63 (P6(a58,x38931,a81)),
% 106.56/106.63 inference(rename_variables,[],[119])).
% 106.56/106.63 cnf(3895,plain,
% 106.56/106.63 (P3(a8,a81)),
% 106.56/106.63 inference(scs_inference,[],[724,119,3887,3893,139,104,91,105,100])).
% 106.56/106.63 cnf(3899,plain,
% 106.56/106.63 (~P5(a8,a80)),
% 106.56/106.63 inference(scs_inference,[],[724,116,104])).
% 106.56/106.63 cnf(3900,plain,
% 106.56/106.63 (P6(a58,x39001,a80)),
% 106.56/106.63 inference(rename_variables,[],[116])).
% 106.56/106.63 cnf(3906,plain,
% 106.56/106.63 (P6(a58,x39061,a80)),
% 106.56/106.63 inference(rename_variables,[],[116])).
% 106.56/106.63 cnf(3908,plain,
% 106.56/106.63 (P3(a8,a80)),
% 106.56/106.63 inference(scs_inference,[],[724,116,3900,3906,703,104,91,105,100])).
% 106.56/106.63 cnf(3912,plain,
% 106.56/106.63 (~P5(a8,a86)),
% 106.56/106.63 inference(scs_inference,[],[724,694,104])).
% 106.56/106.63 cnf(3913,plain,
% 106.56/106.63 (P6(x39131,f48(a5,a5),a86)),
% 106.56/106.63 inference(rename_variables,[],[694])).
% 106.56/106.63 cnf(3919,plain,
% 106.56/106.63 (P6(x39191,f48(a5,a5),a86)),
% 106.56/106.63 inference(rename_variables,[],[694])).
% 106.56/106.63 cnf(3921,plain,
% 106.56/106.63 (P3(a8,a86)),
% 106.56/106.63 inference(scs_inference,[],[724,694,3913,3919,652,104,91,105,100])).
% 106.56/106.63 cnf(5161,plain,
% 106.56/106.63 (~P6(x51611,a71,a82)),
% 106.56/106.63 inference(scs_inference,[],[190,229,233,3287,12,50,51,52,69,70,99,102,27])).
% 106.56/106.63 cnf(5163,plain,
% 106.56/106.63 (~P6(a2,x51631,a83)),
% 106.56/106.63 inference(scs_inference,[],[1,190,229,233,3287,12,50,51,52,69,70,99,102,27,37])).
% 106.56/106.63 cnf(5165,plain,
% 106.56/106.63 (~P6(x51651,a71,a87)),
% 106.56/106.63 inference(scs_inference,[],[1,190,229,233,3287,12,50,51,52,69,70,99,102,27,37,29])).
% 106.56/106.63 cnf(5167,plain,
% 106.56/106.63 (~P6(a2,x51671,a89)),
% 106.56/106.63 inference(scs_inference,[],[1,190,229,233,3287,12,50,51,52,69,70,99,102,27,37,29,39])).
% 106.56/106.63 cnf(5169,plain,
% 106.56/106.63 (~P6(a71,x51691,a88)),
% 106.56/106.63 inference(scs_inference,[],[1,190,229,233,3287,12,50,51,52,69,70,99,102,27,37,29,39,32])).
% 106.56/106.63 cnf(5173,plain,
% 106.56/106.63 (P6(a2,x51731,a86)),
% 106.56/106.63 inference(scs_inference,[],[1,190,229,233,3287,12,50,51,52,69,70,99,102,27,37,29,39,32,38,23])).
% 106.56/106.63 cnf(5175,plain,
% 106.56/106.63 (~P6(x51751,a71,a85)),
% 106.56/106.63 inference(scs_inference,[],[1,190,229,233,3287,12,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30])).
% 106.56/106.63 cnf(5177,plain,
% 106.56/106.63 (~P1(a1,f74(a2))),
% 106.56/106.63 inference(scs_inference,[],[1,190,229,233,3287,12,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30,20])).
% 106.56/106.63 cnf(5181,plain,
% 106.56/106.63 (~P6(a71,x51811,a84)),
% 106.56/106.63 inference(scs_inference,[],[1,190,229,233,3287,12,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30,20,71,31])).
% 106.56/106.63 cnf(5183,plain,
% 106.56/106.63 (~P6(x51831,a71,a84)),
% 106.56/106.63 inference(scs_inference,[],[1,190,229,233,3287,12,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30,20,71,31,28])).
% 106.56/106.63 cnf(5185,plain,
% 106.56/106.63 (~P6(a2,x51851,a5)),
% 106.56/106.63 inference(scs_inference,[],[1,190,229,233,3287,12,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30,20,71,31,28,36])).
% 106.56/106.63 cnf(5187,plain,
% 106.56/106.63 (~P1(f39(a58,a62),a62)),
% 106.56/106.63 inference(scs_inference,[],[1,190,229,233,3287,12,1803,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30,20,71,31,28,36,87])).
% 106.56/106.63 cnf(5189,plain,
% 106.56/106.63 (P6(x51891,a2,a80)),
% 106.56/106.63 inference(scs_inference,[],[1,190,229,233,3287,12,1803,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30,20,71,31,28,36,87,22])).
% 106.56/106.63 cnf(5193,plain,
% 106.56/106.63 (P1(f34(a58,a62),a62)),
% 106.56/106.63 inference(scs_inference,[],[1,190,229,233,3287,12,1803,1625,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30,20,71,31,28,36,87,22,63,64])).
% 106.56/106.63 cnf(5197,plain,
% 106.56/106.63 (~P1(f26(a65,a3),a65)),
% 106.56/106.63 inference(scs_inference,[],[1,190,229,233,3287,12,1803,1808,1222,1625,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30,20,71,31,28,36,87,22,63,64,54,84])).
% 106.56/106.63 cnf(5209,plain,
% 106.56/106.63 (P1(a66,f74(a62))),
% 106.56/106.63 inference(scs_inference,[],[1,190,229,233,3287,10,12,1754,1671,1803,1808,1611,1222,1625,1571,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30,20,71,31,28,36,87,22,63,64,54,84,25,65,24,21,60,17])).
% 106.56/106.63 cnf(5215,plain,
% 106.56/106.63 (~P6(f74(a62),a62,a90)),
% 106.56/106.63 inference(scs_inference,[],[1,125,190,229,233,452,3287,10,12,1567,1754,1671,1803,1808,1611,449,1222,1659,1625,1571,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30,20,71,31,28,36,87,22,63,64,54,84,25,65,24,21,60,17,56,45,47])).
% 106.56/106.63 cnf(5219,plain,
% 106.56/106.63 (~P6(f74(a62),a62,a91)),
% 106.56/106.63 inference(scs_inference,[],[1,125,190,229,233,452,3287,10,12,1567,1754,1671,1803,1808,1611,449,1222,1659,1625,1571,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30,20,71,31,28,36,87,22,63,64,54,84,25,65,24,21,60,17,56,45,47,48,49])).
% 106.56/106.63 cnf(5221,plain,
% 106.56/106.63 (~P2(a8,a73)),
% 106.56/106.63 inference(scs_inference,[],[1,125,190,229,233,452,3287,10,12,1567,3377,949,1754,1671,1803,1808,1611,449,1222,1659,1625,1571,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30,20,71,31,28,36,87,22,63,64,54,84,25,65,24,21,60,17,56,45,47,48,49,94])).
% 106.56/106.63 cnf(5224,plain,
% 106.56/106.63 (~P1(f14(a2,a62),a62)),
% 106.56/106.63 inference(scs_inference,[],[1,125,190,229,233,452,3287,10,12,1567,3377,1580,949,1754,1671,1803,1808,1611,449,1222,1659,1625,1571,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30,20,71,31,28,36,87,22,63,64,54,84,25,65,24,21,60,17,56,45,47,48,49,94,77])).
% 106.56/106.63 cnf(5236,plain,
% 106.56/106.63 (~P1(f40(a62,a58),a62)),
% 106.56/106.63 inference(scs_inference,[],[1,125,190,229,233,452,3287,10,12,1567,3377,1580,949,1584,1636,1754,1671,1803,1808,1611,449,1222,1659,1625,478,1419,1571,579,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30,20,71,31,28,36,87,22,63,64,54,84,25,65,24,21,60,17,56,45,47,48,49,94,77,78,79,41,101])).
% 106.56/106.63 cnf(5240,plain,
% 106.56/106.63 (P6(a2,a2,a8)),
% 106.56/106.63 inference(scs_inference,[],[1,125,190,229,233,452,3287,10,12,1567,3377,1580,949,1584,1636,1754,1671,1803,1808,1611,449,1222,1659,1625,478,1419,1571,579,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30,20,71,31,28,36,87,22,63,64,54,84,25,65,24,21,60,17,56,45,47,48,49,94,77,78,79,41,101,33])).
% 106.56/106.63 cnf(5245,plain,
% 106.56/106.63 (~P6(f74(a65),a65,a10)),
% 106.56/106.63 inference(scs_inference,[],[1,125,190,229,233,452,3287,10,12,1567,3377,1580,949,1584,1636,1754,1671,1803,1808,1611,449,1222,1659,1625,478,1419,1571,776,579,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30,20,71,31,28,36,87,22,63,64,54,84,25,65,24,21,60,17,56,45,47,48,49,94,77,78,79,41,101,33,46,44])).
% 106.56/106.63 cnf(5247,plain,
% 106.56/106.63 (P1(f60(a56,a58),a56)),
% 106.56/106.63 inference(scs_inference,[],[1,125,190,229,233,452,3287,10,12,1567,3377,1580,521,949,1584,1636,1754,1671,1803,1808,1611,449,1222,1659,1625,478,1419,1571,776,14,579,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30,20,71,31,28,36,87,22,63,64,54,84,25,65,24,21,60,17,56,45,47,48,49,94,77,78,79,41,101,33,46,44,76])).
% 106.56/106.63 cnf(5250,plain,
% 106.56/106.63 (P1(f78(a2,a2),a2)),
% 106.56/106.63 inference(scs_inference,[],[1,125,190,229,233,452,3287,10,12,1567,3377,1580,521,949,1584,1636,1754,1671,1803,1808,1611,449,1222,1659,1625,478,1419,1571,776,14,579,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30,20,71,31,28,36,87,22,63,64,54,84,25,65,24,21,60,17,56,45,47,48,49,94,77,78,79,41,101,33,46,44,76,81])).
% 106.56/106.63 cnf(5252,plain,
% 106.56/106.63 (~P6(f74(a62),a62,a81)),
% 106.56/106.63 inference(scs_inference,[],[1,125,190,229,233,452,3287,10,12,1567,3377,1580,521,949,1584,1636,1754,1671,1803,1808,1611,449,1222,1659,1625,478,1419,1571,776,14,579,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30,20,71,31,28,36,87,22,63,64,54,84,25,65,24,21,60,17,56,45,47,48,49,94,77,78,79,41,101,33,46,44,76,81,43])).
% 106.56/106.63 cnf(5254,plain,
% 106.56/106.63 (~P1(f23(a62,a3),a62)),
% 106.56/106.63 inference(scs_inference,[],[1,125,190,229,233,452,3287,10,12,1567,3377,1580,521,949,1584,1620,1636,1754,1671,1803,1808,1611,449,1222,1659,1625,478,1419,1571,776,14,8,579,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30,20,71,31,28,36,87,22,63,64,54,84,25,65,24,21,60,17,56,45,47,48,49,94,77,78,79,41,101,33,46,44,76,81,43,98])).
% 106.56/106.63 cnf(5255,plain,
% 106.56/106.63 (P1(x52551,a3)),
% 106.56/106.63 inference(rename_variables,[],[8])).
% 106.56/106.63 cnf(5260,plain,
% 106.56/106.63 (P6(a2,a2,a73)),
% 106.56/106.64 inference(scs_inference,[],[1,125,190,229,233,452,3287,10,12,1567,3377,1580,521,949,1584,1620,1636,1754,1671,1803,1808,1611,449,1222,1659,1625,478,1419,1571,776,14,8,579,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30,20,71,31,28,36,87,22,63,64,54,84,25,65,24,21,60,17,56,45,47,48,49,94,77,78,79,41,101,33,46,44,76,81,43,98,80,34])).
% 106.56/106.64 cnf(5262,plain,
% 106.56/106.64 (~P5(a81,a85)),
% 106.56/106.64 inference(scs_inference,[],[1,125,190,229,233,452,3287,10,12,1567,3377,1580,3833,521,661,949,1584,1620,1636,1754,1671,1803,1808,1611,449,1222,1659,1625,478,1419,1571,776,14,8,579,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30,20,71,31,28,36,87,22,63,64,54,84,25,65,24,21,60,17,56,45,47,48,49,94,77,78,79,41,101,33,46,44,76,81,43,98,80,34,104])).
% 106.56/106.64 cnf(5263,plain,
% 106.56/106.64 (P6(f48(a5,a5),x52631,a81)),
% 106.56/106.64 inference(rename_variables,[],[661])).
% 106.56/106.64 cnf(5265,plain,
% 106.56/106.64 (P3(a81,a85)),
% 106.56/106.64 inference(scs_inference,[],[1,125,190,229,233,452,3287,10,12,1567,3377,1580,3833,521,661,5263,949,1584,1620,1636,1754,1671,1803,1808,1611,449,1222,1659,1625,478,1419,1571,776,14,8,579,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30,20,71,31,28,36,87,22,63,64,54,84,25,65,24,21,60,17,56,45,47,48,49,94,77,78,79,41,101,33,46,44,76,81,43,98,80,34,104,100])).
% 106.56/106.64 cnf(5269,plain,
% 106.56/106.64 (P1(x52691,a3)),
% 106.56/106.64 inference(rename_variables,[],[8])).
% 106.56/106.64 cnf(5275,plain,
% 106.56/106.64 (~P1(f12(a3,a62),a62)),
% 106.56/106.64 inference(scs_inference,[],[1,125,190,229,233,452,3287,10,12,1567,3377,1580,3833,521,661,5263,949,9,1584,1596,1602,1620,1636,1754,1671,1803,1808,1611,449,1222,1659,1625,1679,478,1419,1571,776,14,8,5255,5269,579,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30,20,71,31,28,36,87,22,63,64,54,84,25,65,24,21,60,17,56,45,47,48,49,94,77,78,79,41,101,33,46,44,76,81,43,98,80,34,104,100,93,74,106])).
% 106.56/106.64 cnf(5276,plain,
% 106.56/106.64 (P1(x52761,a3)),
% 106.56/106.64 inference(rename_variables,[],[8])).
% 106.56/106.64 cnf(5277,plain,
% 106.56/106.64 (P1(x52771,a3)),
% 106.56/106.64 inference(rename_variables,[],[8])).
% 106.56/106.64 cnf(5279,plain,
% 106.56/106.64 (~P1(f22(a2,a62),a62)),
% 106.56/106.64 inference(scs_inference,[],[1,125,190,229,233,452,3287,10,12,1567,3377,1580,1601,3833,521,661,5263,949,9,1584,1596,1602,1620,1636,1754,1671,1803,1808,1611,449,1222,1659,1625,1679,478,1419,1571,776,14,8,5255,5269,579,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30,20,71,31,28,36,87,22,63,64,54,84,25,65,24,21,60,17,56,45,47,48,49,94,77,78,79,41,101,33,46,44,76,81,43,98,80,34,104,100,93,74,106,90])).
% 106.56/106.64 cnf(5288,plain,
% 106.56/106.64 (P6(a2,a3,a90)),
% 106.56/106.64 inference(scs_inference,[],[1,125,190,229,233,452,3287,10,12,1567,3377,1580,1601,3833,521,661,5263,949,9,1584,1596,1602,1620,1636,1754,1671,1803,1808,1611,449,1222,1659,5,1625,1679,478,1419,1571,4,776,14,8,5255,5269,5277,5276,579,50,51,52,69,70,99,102,27,37,29,39,32,38,23,30,20,71,31,28,36,87,22,63,64,54,84,25,65,24,21,60,17,56,45,47,48,49,94,77,78,79,41,101,33,46,44,76,81,43,98,80,34,104,100,93,74,106,90,1257,53,88,97])).
% 106.56/106.64 cnf(5305,plain,
% 106.56/106.64 (~P6(a62,x53051,a89)),
% 106.56/106.64 inference(scs_inference,[],[278,5193,70,39])).
% 106.56/106.64 cnf(5313,plain,
% 106.56/106.64 (~P6(x53131,a65,a87)),
% 106.56/106.64 inference(scs_inference,[],[278,283,292,3289,5193,5197,70,39,52,99,69,29])).
% 106.56/106.64 cnf(5315,plain,
% 106.56/106.64 (~P6(a62,x53151,a83)),
% 106.56/106.64 inference(scs_inference,[],[278,283,292,3289,5193,5197,70,39,52,99,69,29,37])).
% 106.56/106.64 cnf(5317,plain,
% 106.56/106.64 (~P6(a62,x53171,a85)),
% 106.56/106.64 inference(scs_inference,[],[278,283,292,3289,5193,5197,70,39,52,99,69,29,37,38])).
% 106.56/106.64 cnf(5321,plain,
% 106.56/106.64 (~P6(x53211,a65,a82)),
% 106.56/106.64 inference(scs_inference,[],[278,283,292,3289,5193,5197,70,39,52,99,69,29,37,38,50,27])).
% 106.56/106.64 cnf(5327,plain,
% 106.56/106.64 (~P6(a65,x53271,a88)),
% 106.56/106.64 inference(scs_inference,[],[240,278,283,289,292,3289,5193,5197,70,39,52,99,69,29,37,38,50,27,51,102,32])).
% 106.56/106.64 cnf(5329,plain,
% 106.56/106.64 (P6(a62,x53291,a86)),
% 106.56/106.64 inference(scs_inference,[],[240,278,283,289,292,3289,5193,5197,70,39,52,99,69,29,37,38,50,27,51,102,32,23])).
% 106.56/106.64 cnf(5331,plain,
% 106.56/106.64 (~P6(x53311,a65,a85)),
% 106.56/106.64 inference(scs_inference,[],[240,278,283,289,292,3289,5193,5197,70,39,52,99,69,29,37,38,50,27,51,102,32,23,30])).
% 106.56/106.64 cnf(5335,plain,
% 106.56/106.64 (~P1(f60(a62,a58),f74(a65))),
% 106.56/106.64 inference(scs_inference,[],[240,278,283,289,292,3289,1667,5193,5197,70,39,52,99,69,29,37,38,50,27,51,102,32,23,30,71,20])).
% 106.56/106.64 cnf(5337,plain,
% 106.56/106.64 (~P6(a65,x53371,a84)),
% 106.56/106.64 inference(scs_inference,[],[240,278,283,289,292,3289,1667,5193,5197,70,39,52,99,69,29,37,38,50,27,51,102,32,23,30,71,20,31])).
% 106.56/106.64 cnf(5341,plain,
% 106.56/106.64 (~P6(a62,x53411,a5)),
% 106.56/106.64 inference(scs_inference,[],[240,278,283,289,292,3289,1667,5193,5197,70,39,52,99,69,29,37,38,50,27,51,102,32,23,30,71,20,31,28,36])).
% 106.56/106.64 cnf(5343,plain,
% 106.56/106.64 (~P1(f39(a58,a65),a65)),
% 106.56/106.64 inference(scs_inference,[],[240,278,283,289,292,3289,1667,5193,5197,1767,70,39,52,99,69,29,37,38,50,27,51,102,32,23,30,71,20,31,28,36,87])).
% 106.56/106.64 cnf(5345,plain,
% 106.56/106.64 (P6(x53451,a62,a80)),
% 106.56/106.64 inference(scs_inference,[],[240,278,283,289,292,3289,1667,5193,5197,1767,70,39,52,99,69,29,37,38,50,27,51,102,32,23,30,71,20,31,28,36,87,22])).
% 106.56/106.64 cnf(5347,plain,
% 106.56/106.64 (~P1(f17(a2,a3),a2)),
% 106.56/106.64 inference(scs_inference,[],[240,278,283,289,292,3289,5288,1667,5193,5197,1767,70,39,52,99,69,29,37,38,50,27,51,102,32,23,30,71,20,31,28,36,87,22,82])).
% 106.56/106.64 cnf(5351,plain,
% 106.56/106.64 (~P1(f26(a62,a3),a62)),
% 106.56/106.64 inference(scs_inference,[],[240,278,283,289,292,3289,5288,1667,5193,5197,1778,1767,70,39,52,99,69,29,37,38,50,27,51,102,32,23,30,71,20,31,28,36,87,22,82,64,84])).
% 106.56/106.64 cnf(5355,plain,
% 106.56/106.64 (P1(f20(a62,a3),a62)),
% 106.56/106.64 inference(scs_inference,[],[240,278,283,289,292,3289,5185,5288,1667,5193,5197,1778,1767,70,39,52,99,69,29,37,38,50,27,51,102,32,23,30,71,20,31,28,36,87,22,82,64,84,21,60])).
% 106.56/106.64 cnf(5359,plain,
% 106.56/106.64 (P1(f26(a65,a3),f74(a65))),
% 106.56/106.64 inference(scs_inference,[],[240,278,283,289,292,3289,5185,5288,1667,5193,5197,1778,1767,70,39,52,99,69,29,37,38,50,27,51,102,32,23,30,71,20,31,28,36,87,22,82,64,84,21,60,57,17])).
% 106.56/106.64 cnf(5365,plain,
% 106.56/106.64 (~P2(a86,a82)),
% 106.56/106.64 inference(scs_inference,[],[1,240,278,283,289,292,3289,5161,5173,5185,5288,1667,5193,5197,5177,1778,1767,70,39,52,99,69,29,37,38,50,27,51,102,32,23,30,71,20,31,28,36,87,22,82,64,84,21,60,57,17,48,49,94])).
% 106.56/106.64 cnf(5366,plain,
% 106.56/106.64 (P6(a2,x53661,a86)),
% 106.56/106.64 inference(rename_variables,[],[5173])).
% 106.56/106.64 cnf(5367,plain,
% 106.56/106.64 (~P6(x53671,a71,a82)),
% 106.56/106.64 inference(rename_variables,[],[5161])).
% 106.56/106.64 cnf(5377,plain,
% 106.56/106.64 (~P1(f14(a2,a71),a71)),
% 106.56/106.64 inference(scs_inference,[],[1,240,278,283,289,292,3289,5161,5367,5173,5366,5185,5189,5288,1667,5193,5197,5177,1778,1767,70,39,52,99,69,29,37,38,50,27,51,102,32,23,30,71,20,31,28,36,87,22,82,64,84,21,60,57,17,48,49,94,47,78,79,77])).
% 106.56/106.64 cnf(5385,plain,
% 106.56/106.64 (~P1(f40(a71,a58),a71)),
% 106.56/106.64 inference(scs_inference,[],[1,240,278,283,289,292,3289,5161,5367,5163,5169,5173,5366,5185,5189,5288,1667,5193,5197,5177,1778,1767,579,70,39,52,99,69,29,37,38,50,27,51,102,32,23,30,71,20,31,28,36,87,22,82,64,84,21,60,57,17,48,49,94,47,78,79,77,41,45,101])).
% 106.56/106.64 cnf(5389,plain,
% 106.56/106.64 (P6(a65,a65,a8)),
% 106.56/106.64 inference(scs_inference,[],[1,240,278,283,289,292,3289,5161,5367,5163,5169,5173,5366,5185,5189,5288,479,1667,5193,5197,5177,1778,1767,579,70,39,52,99,69,29,37,38,50,27,51,102,32,23,30,71,20,31,28,36,87,22,82,64,84,21,60,57,17,48,49,94,47,78,79,77,41,45,101,33])).
% 106.56/106.64 cnf(5394,plain,
% 106.56/106.64 (P1(f72(a58,a56),a56)),
% 106.56/106.64 inference(scs_inference,[],[1,240,278,283,289,292,3289,5161,5367,5163,5169,5173,5366,5185,5189,5288,479,1667,5193,5197,5177,524,1778,1767,648,14,579,70,39,52,99,69,29,37,38,50,27,51,102,32,23,30,71,20,31,28,36,87,22,82,64,84,21,60,57,17,48,49,94,47,78,79,77,41,45,101,33,46,76])).
% 106.56/106.64 cnf(5397,plain,
% 106.56/106.64 (~P6(f74(a2),a2,a10)),
% 106.56/106.64 inference(scs_inference,[],[1,240,278,283,289,292,3289,5161,5367,5163,5169,5173,5366,5185,5189,5288,479,1667,5193,5197,5177,524,1778,1767,648,14,579,70,39,52,99,69,29,37,38,50,27,51,102,32,23,30,71,20,31,28,36,87,22,82,64,84,21,60,57,17,48,49,94,47,78,79,77,41,45,101,33,46,76,44])).
% 106.56/106.64 cnf(5403,plain,
% 106.56/106.64 (P1(f77(a65,a65),a65)),
% 106.56/106.64 inference(scs_inference,[],[1,240,278,283,289,292,3289,5161,5367,5163,5169,5173,5366,5185,5189,5288,479,1667,5193,5197,5177,524,1778,1767,648,14,579,70,39,52,99,69,29,37,38,50,27,51,102,32,23,30,71,20,31,28,36,87,22,82,64,84,21,60,57,17,48,49,94,47,78,79,77,41,45,101,33,46,76,44,81,43,80])).
% 106.56/106.64 cnf(5405,plain,
% 106.56/106.64 (P6(a65,a65,a73)),
% 106.56/106.64 inference(scs_inference,[],[1,240,278,283,289,292,3289,5161,5367,5163,5169,5173,5366,5185,5189,5288,479,1667,5193,5197,5177,524,1778,1767,648,14,579,70,39,52,99,69,29,37,38,50,27,51,102,32,23,30,71,20,31,28,36,87,22,82,64,84,21,60,57,17,48,49,94,47,78,79,77,41,45,101,33,46,76,44,81,43,80,34])).
% 106.56/106.64 cnf(5412,plain,
% 106.56/106.64 (~P1(f12(a62,a3),a62)),
% 106.56/106.64 inference(scs_inference,[],[1,240,278,283,289,292,3289,5161,5367,5163,5167,5169,5173,5366,5185,5189,5260,5288,479,1667,5193,5197,5177,1645,524,1778,1767,9,13,648,14,8,579,70,39,52,99,69,29,37,38,50,27,51,102,32,23,30,71,20,31,28,36,87,22,82,64,84,21,60,57,17,48,49,94,47,78,79,77,41,45,101,33,46,76,44,81,43,80,34,91,74,106])).
% 106.56/106.64 cnf(5415,plain,
% 106.56/106.64 (~P1(f22(a2,a71),a71)),
% 106.56/106.64 inference(scs_inference,[],[1,240,278,283,289,292,3289,5161,5367,5163,5165,5167,5169,5173,5366,5185,5189,5260,5288,479,1667,5193,5197,5177,1645,524,1778,1767,9,13,648,14,8,579,70,39,52,99,69,29,37,38,50,27,51,102,32,23,30,71,20,31,28,36,87,22,82,64,84,21,60,57,17,48,49,94,47,78,79,77,41,45,101,33,46,76,44,81,43,80,34,91,74,106,90])).
% 106.56/106.64 cnf(5418,plain,
% 106.56/106.64 (~P6(a62,a58,a75)),
% 106.56/106.64 inference(scs_inference,[],[1,240,278,283,289,292,3289,5161,5367,5163,5165,5167,5169,5173,5366,5185,5189,5260,5288,479,1667,5193,5197,5177,1645,524,1778,1767,9,13,648,14,8,579,70,39,52,99,69,29,37,38,50,27,51,102,32,23,30,71,20,31,28,36,87,22,82,64,84,21,60,57,17,48,49,94,47,78,79,77,41,45,101,33,46,76,44,81,43,80,34,91,74,106,90,1257])).
% 106.56/106.64 cnf(5451,plain,
% 106.56/106.64 (~P6(a2,x54511,a88)),
% 106.56/106.64 inference(scs_inference,[],[307,316,3262,5335,5359,5347,52,69,99,29,70,51,39,27,50,38,37,32])).
% 106.56/106.64 cnf(5459,plain,
% 106.56/106.64 (~P1(f19(a65,a58),f74(a65))),
% 106.56/106.64 inference(scs_inference,[],[280,307,316,3262,1822,5335,5359,5347,52,69,99,29,70,51,39,27,50,38,37,32,102,23,30,20])).
% 106.56/106.64 cnf(5469,plain,
% 106.56/106.64 (P6(x54691,f74(a65),a80)),
% 106.56/106.64 inference(scs_inference,[],[280,307,316,3262,1822,5335,5359,5347,52,69,99,29,70,51,39,27,50,38,37,32,102,23,30,20,71,31,28,36,22])).
% 106.56/106.64 cnf(5471,plain,
% 106.56/106.64 (P1(f4(a62),a62)),
% 106.56/106.64 inference(scs_inference,[],[280,307,316,3262,5341,1822,5335,5359,5347,52,69,99,29,70,51,39,27,50,38,37,32,102,23,30,20,71,31,28,36,22,21])).
% 106.56/106.64 cnf(5473,plain,
% 106.56/106.64 (P1(f39(a58,a62),f74(a62))),
% 106.56/106.64 inference(scs_inference,[],[280,307,316,3262,5341,1822,5335,5359,5187,5347,52,69,99,29,70,51,39,27,50,38,37,32,102,23,30,20,71,31,28,36,22,21,17])).
% 106.56/106.64 cnf(5477,plain,
% 106.56/106.64 (~P6(a65,f74(a65),a90)),
% 106.56/106.64 inference(scs_inference,[],[280,307,316,3262,5341,1822,5335,5359,5187,5347,1813,1667,52,69,99,29,70,51,39,27,50,38,37,32,102,23,30,20,71,31,28,36,22,21,17,49,47])).
% 106.56/106.64 cnf(5479,plain,
% 106.56/106.64 (~P2(a86,a85)),
% 106.56/106.64 inference(scs_inference,[],[280,307,316,3262,5175,5329,5341,1822,5335,5359,5187,5347,1813,1667,52,69,99,29,70,51,39,27,50,38,37,32,102,23,30,20,71,31,28,36,22,21,17,49,47,94])).
% 106.56/106.64 cnf(5481,plain,
% 106.56/106.64 (P6(a62,x54811,a86)),
% 106.56/106.64 inference(rename_variables,[],[5329])).
% 106.56/106.64 cnf(5483,plain,
% 106.56/106.64 (~P6(a65,f45(a5,a5),a75)),
% 106.56/106.64 inference(scs_inference,[],[280,307,316,3262,5175,5329,5341,1822,5335,5359,5187,5347,1813,1667,776,52,69,99,29,70,51,39,27,50,38,37,32,102,23,30,20,71,31,28,36,22,21,17,49,47,94,48])).
% 106.56/106.64 cnf(5486,plain,
% 106.56/106.64 (~P1(f14(a2,a65),a65)),
% 106.56/106.64 inference(scs_inference,[],[1,280,307,316,3262,5175,5321,5329,5341,1822,5335,5359,5187,5347,1813,1667,776,52,69,99,29,70,51,39,27,50,38,37,32,102,23,30,20,71,31,28,36,22,21,17,49,47,94,48,77])).
% 106.56/106.64 cnf(5489,plain,
% 106.56/106.64 (P1(f32(a62,a2),a62)),
% 106.56/106.64 inference(scs_inference,[],[1,280,307,316,3262,5175,5315,5321,5329,5341,1822,5335,5359,5187,5347,1813,1667,776,52,69,99,29,70,51,39,27,50,38,37,32,102,23,30,20,71,31,28,36,22,21,17,49,47,94,48,77,41])).
% 106.56/106.64 cnf(5492,plain,
% 106.56/106.64 (P1(f52(a2,a62),a62)),
% 106.56/106.64 inference(scs_inference,[],[1,280,307,316,3262,5175,5315,5321,5329,5341,5345,1822,5335,5359,5187,5347,1813,1667,776,52,69,99,29,70,51,39,27,50,38,37,32,102,23,30,20,71,31,28,36,22,21,17,49,47,94,48,77,41,79])).
% 106.56/106.64 cnf(5495,plain,
% 106.56/106.64 (~P6(a62,f48(a84,a84),a75)),
% 106.56/106.64 inference(scs_inference,[],[1,280,307,316,3262,5175,5315,5321,5329,5341,5345,1822,5335,5359,5187,5347,1813,1667,648,776,52,69,99,29,70,51,39,27,50,38,37,32,102,23,30,20,71,31,28,36,22,21,17,49,47,94,48,77,41,79,45])).
% 106.56/106.64 cnf(5498,plain,
% 106.56/106.64 (P1(f29(a62,a2),a62)),
% 106.56/106.64 inference(scs_inference,[],[1,280,307,316,3262,5175,5315,5321,5329,5481,5341,5345,1822,5335,5359,5187,5347,1813,1667,648,776,52,69,99,29,70,51,39,27,50,38,37,32,102,23,30,20,71,31,28,36,22,21,17,49,47,94,48,77,41,79,45,78])).
% 106.56/106.64 cnf(5501,plain,
% 106.56/106.64 (~P1(f40(a65,a58),a65)),
% 106.56/106.64 inference(scs_inference,[],[1,280,307,316,3262,5175,5315,5321,5327,5329,5481,5341,5345,1822,5335,5359,5187,5347,1813,1667,648,776,579,52,69,99,29,70,51,39,27,50,38,37,32,102,23,30,20,71,31,28,36,22,21,17,49,47,94,48,77,41,79,45,78,101])).
% 106.56/106.64 cnf(5507,plain,
% 106.56/106.64 (~P6(a2,f74(a2),a10)),
% 106.56/106.64 inference(scs_inference,[],[1,280,307,316,3262,5175,5315,5321,5327,5329,5481,5341,5345,1822,5335,5359,5187,5347,1813,1667,5177,648,776,579,52,69,99,29,70,51,39,27,50,38,37,32,102,23,30,20,71,31,28,36,22,21,17,49,47,94,48,77,41,79,45,78,101,33,46])).
% 106.56/106.64 cnf(5509,plain,
% 106.56/106.64 (P1(f60(a69,a58),a69)),
% 106.56/106.64 inference(scs_inference,[],[1,280,307,316,3262,5175,5315,5321,5327,5329,5481,5341,5345,1822,5335,5359,5187,5347,1813,583,1667,5177,648,776,14,579,52,69,99,29,70,51,39,27,50,38,37,32,102,23,30,20,71,31,28,36,22,21,17,49,47,94,48,77,41,79,45,78,101,33,46,76])).
% 106.56/106.64 cnf(5516,plain,
% 106.56/106.64 (P6(f74(a65),f74(a65),a73)),
% 106.56/106.64 inference(scs_inference,[],[1,280,307,316,3262,5175,5315,5321,5327,5329,5481,5341,5345,1822,5335,5359,5187,5347,1813,583,1667,5177,648,776,14,579,52,69,99,29,70,51,39,27,50,38,37,32,102,23,30,20,71,31,28,36,22,21,17,49,47,94,48,77,41,79,45,78,101,33,46,76,44,43,34])).
% 106.56/106.64 cnf(5523,plain,
% 106.56/106.64 (P1(f35(a62,a62),a62)),
% 106.56/106.64 inference(scs_inference,[],[1,280,307,316,3262,5240,5175,5305,5315,5321,5327,5329,5481,5341,5345,5405,1822,5335,5359,5187,5355,5347,1813,583,5173,1667,5177,13,648,776,14,579,52,69,99,29,70,51,39,27,50,38,37,32,102,23,30,20,71,31,28,36,22,21,17,49,47,94,48,77,41,79,45,78,101,33,46,76,44,43,34,105,91,74])).
% 106.56/106.64 cnf(5526,plain,
% 106.56/106.64 (~P1(f22(a62,a65),a65)),
% 106.56/106.64 inference(scs_inference,[],[1,280,307,316,3262,5240,5175,5305,5313,5315,5321,5327,5329,5481,5341,5345,5405,1822,5335,5359,5187,5355,5347,1813,583,5173,1667,5177,13,648,776,14,579,52,69,99,29,70,51,39,27,50,38,37,32,102,23,30,20,71,31,28,36,22,21,17,49,47,94,48,77,41,79,45,78,101,33,46,76,44,43,34,105,91,74,90])).
% 106.56/106.64 cnf(5531,plain,
% 106.56/106.64 (P1(f4(a62),a65)),
% 106.56/106.64 inference(scs_inference,[],[1,280,307,316,3262,5240,5175,5305,5313,5315,5321,5327,5329,5481,5341,5345,5405,1822,5335,5359,5187,5355,5347,1813,583,5173,1667,5177,13,648,776,14,579,52,69,99,29,70,51,39,27,50,38,37,32,102,23,30,20,71,31,28,36,22,21,17,49,47,94,48,77,41,79,45,78,101,33,46,76,44,43,34,105,91,74,90,1257,15])).
% 106.56/106.64 cnf(5546,plain,
% 106.56/106.64 (~P6(x55461,a2,a87)),
% 106.56/106.64 inference(scs_inference,[],[323,589,5347,99,70,29])).
% 106.56/106.64 cnf(5562,plain,
% 106.56/106.64 (~P6(x55621,a2,a82)),
% 106.56/106.64 inference(scs_inference,[],[323,337,342,481,589,5473,5347,99,70,29,52,51,69,37,38,50,39,27])).
% 106.56/106.64 cnf(5566,plain,
% 106.56/106.64 (~P6(f74(a2),x55661,a88)),
% 106.56/106.64 inference(scs_inference,[],[298,323,337,342,481,589,5473,5347,5177,99,70,29,52,51,69,37,38,50,39,27,102,32])).
% 106.56/106.64 cnf(5568,plain,
% 106.56/106.64 (P6(f74(a62),x55681,a86)),
% 106.56/106.64 inference(scs_inference,[],[298,323,337,342,481,589,5473,5347,5177,99,70,29,52,51,69,37,38,50,39,27,102,32,23])).
% 106.56/106.64 cnf(5570,plain,
% 106.56/106.64 (~P6(x55701,a2,a85)),
% 106.56/106.64 inference(scs_inference,[],[298,323,337,342,481,589,5473,5347,5177,99,70,29,52,51,69,37,38,50,39,27,102,32,23,30])).
% 106.56/106.64 cnf(5574,plain,
% 106.56/106.64 (~P1(f60(a56,a58),f74(a56))),
% 106.56/106.64 inference(scs_inference,[],[298,323,337,342,481,589,5473,5247,5347,5177,99,70,29,52,51,69,37,38,50,39,27,102,32,23,30,71,20])).
% 106.56/106.64 cnf(5578,plain,
% 106.56/106.64 (~P6(a2,x55781,a84)),
% 106.56/106.64 inference(scs_inference,[],[298,323,337,342,481,589,5473,5247,5489,5347,5177,99,70,29,52,51,69,37,38,50,39,27,102,32,23,30,71,20,15,31])).
% 106.56/106.64 cnf(5580,plain,
% 106.56/106.64 (~P6(x55801,a2,a84)),
% 106.56/106.64 inference(scs_inference,[],[298,323,337,342,481,589,5473,5247,5489,5347,5177,99,70,29,52,51,69,37,38,50,39,27,102,32,23,30,71,20,15,31,28])).
% 106.56/106.64 cnf(5586,plain,
% 106.56/106.64 (P1(f39(a58,a65),f74(a65))),
% 106.56/106.64 inference(scs_inference,[],[298,323,337,342,481,589,5343,5473,5247,5489,5347,5177,99,70,29,52,51,69,37,38,50,39,27,102,32,23,30,71,20,15,31,28,36,22,17])).
% 106.56/106.64 cnf(5592,plain,
% 106.56/106.64 (~P2(a8,a85)),
% 106.56/106.64 inference(scs_inference,[],[298,323,337,342,481,5389,5331,589,5343,5459,5473,5247,5489,5347,10,1822,5,5177,99,70,29,52,51,69,37,38,50,39,27,102,32,23,30,71,20,15,31,28,36,22,17,48,49,94])).
% 106.56/106.64 cnf(5597,plain,
% 106.56/106.64 (~P6(a65,a62,a90)),
% 106.56/106.64 inference(scs_inference,[],[298,323,337,342,481,5389,5331,589,5343,5459,5473,5247,5489,5347,10,1822,5,5187,5177,99,70,29,52,51,69,37,38,50,39,27,102,32,23,30,71,20,15,31,28,36,22,17,48,49,94,45,47])).
% 106.56/106.64 cnf(5599,plain,
% 106.56/106.64 (~P1(f40(a2,a58),a2)),
% 106.56/106.64 inference(scs_inference,[],[298,323,337,342,481,5389,5331,5451,589,5343,5459,5473,5247,5489,5347,10,1822,5,5187,5177,579,99,70,29,52,51,69,37,38,50,39,27,102,32,23,30,71,20,15,31,28,36,22,17,48,49,94,45,47,101])).
% 106.56/106.64 cnf(5607,plain,
% 106.56/106.64 (P1(f60(a59,a58),a59)),
% 106.56/106.64 inference(scs_inference,[],[298,323,337,342,481,5389,5331,5451,589,5343,5459,5473,5247,5489,544,5347,10,1822,5,5187,5177,14,579,99,70,29,52,51,69,37,38,50,39,27,102,32,23,30,71,20,15,31,28,36,22,17,48,49,94,45,47,101,33,46,76])).
% 106.56/106.64 cnf(5616,plain,
% 106.56/106.64 (P6(f74(a62),f74(a62),a73)),
% 106.56/106.64 inference(scs_inference,[],[298,323,337,342,481,5389,5331,5451,589,5343,5459,5473,5247,5489,544,5347,10,1822,5,5187,5177,648,915,14,579,99,70,29,52,51,69,37,38,50,39,27,102,32,23,30,71,20,15,31,28,36,22,17,48,49,94,45,47,101,33,46,76,44,43,34])).
% 106.56/106.64 cnf(5620,plain,
% 106.56/106.64 (P1(f35(a62,a2),a62)),
% 106.56/106.64 inference(scs_inference,[],[1,298,323,337,342,481,5389,5331,5451,589,5343,5459,5473,5516,5247,5489,544,5305,5347,10,1822,5,5187,5177,13,648,915,14,579,99,70,29,52,51,69,37,38,50,39,27,102,32,23,30,71,20,15,31,28,36,22,17,48,49,94,45,47,101,33,46,76,44,43,34,91,74])).
% 106.56/106.64 cnf(5623,plain,
% 106.56/106.64 (~P1(f22(a2,a65),a65)),
% 106.56/106.64 inference(scs_inference,[],[1,298,323,337,342,481,5389,5331,5451,589,5343,5459,5473,5516,5247,5489,544,5305,5313,5347,10,1822,5,5187,5177,13,648,915,14,579,99,70,29,52,51,69,37,38,50,39,27,102,32,23,30,71,20,15,31,28,36,22,17,48,49,94,45,47,101,33,46,76,44,43,34,91,74,90])).
% 106.56/106.64 cnf(5649,plain,
% 106.56/106.64 (~P6(a56,x56491,a89)),
% 106.56/106.64 inference(scs_inference,[],[485,619,748,1458,5574,5394,51,29,52,69,99,70,27,39])).
% 106.56/106.64 cnf(5653,plain,
% 106.56/106.64 (~P6(a56,x56531,a83)),
% 106.56/106.64 inference(scs_inference,[],[485,619,748,1458,5574,5394,51,29,52,69,99,70,27,39,50,37])).
% 106.56/106.64 cnf(5655,plain,
% 106.56/106.64 (~P6(a56,x56551,a85)),
% 106.56/106.64 inference(scs_inference,[],[485,619,748,1458,5574,5394,51,29,52,69,99,70,27,39,50,37,38])).
% 106.56/106.64 cnf(5659,plain,
% 106.56/106.64 (~P6(f49(a5,a82),f50(a5,a82),a82)),
% 106.56/106.64 inference(scs_inference,[],[313,485,619,748,1458,5574,5394,51,29,52,69,99,70,27,39,50,37,38,32,102])).
% 106.56/106.64 cnf(5661,plain,
% 106.56/106.64 (P6(a56,x56611,a86)),
% 106.56/106.64 inference(scs_inference,[],[313,485,619,748,1458,5574,5394,51,29,52,69,99,70,27,39,50,37,38,32,102,23])).
% 106.56/106.64 cnf(5665,plain,
% 106.56/106.64 (~P1(f4(a62),f74(a62))),
% 106.56/106.64 inference(scs_inference,[],[313,485,619,748,1458,5471,5574,5394,51,29,52,69,99,70,27,39,50,37,38,32,102,23,30,20])).
% 106.56/106.64 cnf(5667,plain,
% 106.56/106.64 (P6(f49(a5,a82),f50(a5,a82),a5)),
% 106.56/106.64 inference(scs_inference,[],[313,485,619,748,1458,5471,5574,5394,51,29,52,69,99,70,27,39,50,37,38,32,102,23,30,20,71])).
% 106.56/106.64 cnf(5675,plain,
% 106.56/106.64 (~P6(a56,x56751,a5)),
% 106.56/106.64 inference(scs_inference,[],[313,485,619,748,1458,5471,5574,5394,5492,51,29,52,69,99,70,27,39,50,37,38,32,102,23,30,20,71,15,31,28,36])).
% 106.56/106.64 cnf(5677,plain,
% 106.56/106.64 (P6(x56771,a56,a80)),
% 106.56/106.64 inference(scs_inference,[],[313,485,619,748,1458,5471,5574,5394,5492,51,29,52,69,99,70,27,39,50,37,38,32,102,23,30,20,71,15,31,28,36,22])).
% 106.56/106.64 cnf(5679,plain,
% 106.56/106.64 (P1(f4(a56),a56)),
% 106.56/106.64 inference(scs_inference,[],[313,485,619,748,1458,5471,5574,5394,5492,51,29,52,69,99,70,27,39,50,37,38,32,102,23,30,20,71,15,31,28,36,22,21])).
% 106.56/106.64 cnf(5681,plain,
% 106.56/106.64 (P1(f22(a2,a71),f74(a71))),
% 106.56/106.64 inference(scs_inference,[],[313,485,619,748,1458,5471,5415,5574,5394,5492,51,29,52,69,99,70,27,39,50,37,38,32,102,23,30,20,71,15,31,28,36,22,21,17])).
% 106.56/106.64 cnf(5683,plain,
% 106.56/106.64 (P6(a2,a58,a9)),
% 106.56/106.64 inference(scs_inference,[],[1,313,485,619,748,1458,5471,5415,5574,5394,5492,579,51,29,52,69,99,70,27,39,50,37,38,32,102,23,30,20,71,15,31,28,36,22,21,17,40])).
% 106.56/106.64 cnf(5686,plain,
% 106.56/106.64 (~P1(f14(a2,a2),a2)),
% 106.56/106.64 inference(scs_inference,[],[1,313,485,619,748,5562,1458,5471,5415,5574,5394,5492,579,51,29,52,69,99,70,27,39,50,37,38,32,102,23,30,20,71,15,31,28,36,22,21,17,40,77])).
% 106.56/106.64 cnf(5690,plain,
% 106.56/106.64 (~P1(x56901,f45(a5,a5))),
% 106.56/106.64 inference(rename_variables,[],[776])).
% 106.56/106.64 cnf(5692,plain,
% 106.56/106.64 (~P2(a80,a84)),
% 106.56/106.64 inference(scs_inference,[],[1,313,485,619,748,5181,5562,1458,5471,5415,5469,5574,5394,5492,776,579,51,29,52,69,99,70,27,39,50,37,38,32,102,23,30,20,71,15,31,28,36,22,21,17,40,77,48,94])).
% 106.56/106.64 cnf(5697,plain,
% 106.56/106.64 (P1(x56971,f48(a84,a84))),
% 106.56/106.64 inference(rename_variables,[],[648])).
% 106.56/106.64 cnf(5713,plain,
% 106.56/106.64 (~P1(x57131,a58)),
% 106.56/106.64 inference(rename_variables,[],[14])).
% 106.56/106.64 cnf(5715,plain,
% 106.56/106.64 (P1(f78(a62,a62),a62)),
% 106.56/106.64 inference(scs_inference,[],[1,313,485,619,748,5181,5562,1458,5471,5415,5469,5574,5209,5394,5492,243,5247,10,648,776,5690,14,579,51,29,52,69,99,70,27,39,50,37,38,32,102,23,30,20,71,15,31,28,36,22,21,17,40,77,48,94,45,47,49,41,33,46,44,76,81])).
% 106.56/106.64 cnf(5720,plain,
% 106.56/106.64 (P1(f77(a62,a62),a62)),
% 106.56/106.64 inference(scs_inference,[],[1,313,485,619,748,5181,5562,1458,5471,5415,5469,5574,5209,5394,5492,243,5247,10,648,5697,776,5690,14,579,51,29,52,69,99,70,27,39,50,37,38,32,102,23,30,20,71,15,31,28,36,22,21,17,40,77,48,94,45,47,49,41,33,46,44,76,81,43,80])).
% 106.56/106.64 cnf(5726,plain,
% 106.56/106.64 (~P1(f22(a2,a2),a2)),
% 106.56/106.64 inference(scs_inference,[],[1,313,485,619,748,5181,5546,5562,1458,5471,5415,5469,5574,5616,5209,5394,5492,5599,243,5247,10,13,648,5697,776,5690,14,579,51,29,52,69,99,70,27,39,50,37,38,32,102,23,30,20,71,15,31,28,36,22,21,17,40,77,48,94,45,47,49,41,33,46,44,76,81,43,80,34,91,90])).
% 106.56/106.64 cnf(5729,plain,
% 106.56/106.64 (~P6(a56,a58,a75)),
% 106.56/106.64 inference(scs_inference,[],[1,313,485,619,748,5181,5546,5562,1458,5471,5415,5469,5574,5616,5209,5394,5492,5599,243,5247,10,13,648,5697,776,5690,14,579,51,29,52,69,99,70,27,39,50,37,38,32,102,23,30,20,71,15,31,28,36,22,21,17,40,77,48,94,45,47,49,41,33,46,44,76,81,43,80,34,91,90,1257])).
% 106.56/106.64 cnf(5731,plain,
% 106.56/106.64 (P1(f76(a62,a62),a62)),
% 106.56/106.64 inference(scs_inference,[],[1,313,485,619,748,5181,5546,5562,1458,5471,5415,5469,5574,5616,5209,5394,5492,5599,243,5247,10,13,648,5697,776,5690,14,579,51,29,52,69,99,70,27,39,50,37,38,32,102,23,30,20,71,15,31,28,36,22,21,17,40,77,48,94,45,47,49,41,33,46,44,76,81,43,80,34,91,90,1257,53])).
% 106.56/106.64 cnf(5733,plain,
% 106.56/106.64 (P1(f38(a2,a58),a2)),
% 106.56/106.64 inference(scs_inference,[],[1,313,485,619,748,5181,5546,5562,1458,5471,5415,5469,5574,5616,5209,5394,5492,5599,243,5247,10,13,648,5697,776,5690,14,579,51,29,52,69,99,70,27,39,50,37,38,32,102,23,30,20,71,15,31,28,36,22,21,17,40,77,48,94,45,47,49,41,33,46,44,76,81,43,80,34,91,90,1257,53,65])).
% 106.56/106.64 cnf(5739,plain,
% 106.56/106.64 (P1(f19(a62,a58),a62)),
% 106.56/106.64 inference(scs_inference,[],[1,313,485,619,748,5418,5181,5546,5562,1458,5597,5471,5415,5531,5469,5574,5616,5209,5394,5486,5492,5599,5412,243,5247,10,13,648,5697,776,5690,14,5713,579,51,29,52,69,99,70,27,39,50,37,38,32,102,23,30,20,71,15,31,28,36,22,21,17,40,77,48,94,45,47,49,41,33,46,44,76,81,43,80,34,91,90,1257,53,65,79,88,96])).
% 106.56/106.64 cnf(5742,plain,
% 106.56/106.64 (~P5(a90,a90)),
% 106.56/106.64 inference(scs_inference,[],[1,313,485,619,748,5418,5181,5546,5562,1458,5597,5471,5415,5531,5469,5574,5616,5209,5394,5486,5492,5599,5412,243,5288,5247,10,13,648,5697,776,5690,14,5713,579,51,29,52,69,99,70,27,39,50,37,38,32,102,23,30,20,71,15,31,28,36,22,21,17,40,77,48,94,45,47,49,41,33,46,44,76,81,43,80,34,91,90,1257,53,65,79,88,96,104])).
% 106.56/106.64 cnf(5744,plain,
% 106.56/106.64 (P3(a90,a90)),
% 106.56/106.64 inference(scs_inference,[],[1,313,485,619,748,5418,5181,5546,5562,1458,5597,5471,5415,5531,5469,5574,5616,5209,5394,5486,5492,5599,5412,243,5288,5247,10,13,648,5697,776,5690,14,5713,579,51,29,52,69,99,70,27,39,50,37,38,32,102,23,30,20,71,15,31,28,36,22,21,17,40,77,48,94,45,47,49,41,33,46,44,76,81,43,80,34,91,90,1257,53,65,79,88,96,104,100])).
% 106.56/106.64 cnf(5763,plain,
% 106.56/106.64 (~P6(f74(a71),x57631,a83)),
% 106.56/106.64 inference(scs_inference,[],[743,788,790,1105,5221,5681,5665,99,29,52,51,69,27,70,37])).
% 106.56/106.64 cnf(5773,plain,
% 106.56/106.64 (~P6(f49(a5,a90),f50(a5,a90),a90)),
% 106.56/106.64 inference(scs_inference,[],[319,743,788,790,1105,5221,5681,5665,99,29,52,51,69,27,70,37,39,38,50,32,102])).
% 106.56/106.64 cnf(5777,plain,
% 106.56/106.64 (P6(f74(a71),x57771,a86)),
% 106.56/106.64 inference(scs_inference,[],[319,743,788,790,1105,5221,5681,5665,99,29,52,51,69,27,70,37,39,38,50,32,102,30,23])).
% 106.56/106.64 cnf(5779,plain,
% 106.56/106.64 (P6(f49(a5,a90),f50(a5,a90),a5)),
% 106.56/106.64 inference(scs_inference,[],[319,743,788,790,1105,5221,5681,5665,99,29,52,51,69,27,70,37,39,38,50,32,102,30,23,71])).
% 106.56/106.64 cnf(5781,plain,
% 106.56/106.64 (~P1(f76(a62,a62),f74(a62))),
% 106.56/106.64 inference(scs_inference,[],[319,743,788,790,1105,5221,5731,5681,5665,99,29,52,51,69,27,70,37,39,38,50,32,102,30,23,71,20])).
% 106.56/106.64 cnf(5783,plain,
% 106.56/106.64 (P1(f76(a62,a62),a65)),
% 106.56/106.64 inference(scs_inference,[],[319,743,788,790,1105,5221,5731,5681,5665,99,29,52,51,69,27,70,37,39,38,50,32,102,30,23,71,20,15])).
% 106.56/106.64 cnf(5793,plain,
% 106.56/106.64 (P1(f14(a2,a2),f74(a2))),
% 106.56/106.64 inference(scs_inference,[],[319,743,788,790,1105,5221,5686,5731,5681,5665,99,29,52,51,69,27,70,37,39,38,50,32,102,30,23,71,20,15,31,28,36,22,17])).
% 106.56/106.64 cnf(5797,plain,
% 106.56/106.64 (~P2(a9,a84)),
% 106.56/106.64 inference(scs_inference,[],[319,743,788,790,1105,5683,5578,5221,5686,5731,5681,5665,5531,99,29,52,51,69,27,70,37,39,38,50,32,102,30,23,71,20,15,31,28,36,22,17,48,94])).
% 106.56/106.64 cnf(5798,plain,
% 106.56/106.64 (~P6(a2,x57981,a84)),
% 106.56/106.64 inference(rename_variables,[],[5578])).
% 106.56/106.64 cnf(5815,plain,
% 106.56/106.64 (P6(f74(a71),f74(a71),a8)),
% 106.56/106.64 inference(scs_inference,[],[1,319,743,788,790,1105,5683,5578,5653,5661,5677,5221,5686,5731,5586,5681,5665,1787,5531,5415,99,29,52,51,69,27,70,37,39,38,50,32,102,30,23,71,20,15,31,28,36,22,17,48,94,78,79,41,45,47,49,33])).
% 106.56/106.64 cnf(5818,plain,
% 106.56/106.64 (P1(x58181,f48(a84,a84))),
% 106.56/106.64 inference(rename_variables,[],[648])).
% 106.56/106.64 cnf(5820,plain,
% 106.56/106.64 (P1(f72(a58,a59),a59)),
% 106.56/106.64 inference(scs_inference,[],[1,319,743,788,790,1105,5683,5578,5653,5661,5677,5221,5686,5731,5586,5681,5665,1787,547,5531,5415,648,14,99,29,52,51,69,27,70,37,39,38,50,32,102,30,23,71,20,15,31,28,36,22,17,48,94,78,79,41,45,47,49,33,46,76])).
% 106.56/106.64 cnf(5821,plain,
% 106.56/106.64 (~P1(x58211,a58)),
% 106.56/106.64 inference(rename_variables,[],[14])).
% 106.56/106.64 cnf(5827,plain,
% 106.56/106.64 (~P1(x58271,f46(a88,a88))),
% 106.56/106.64 inference(rename_variables,[],[915])).
% 106.56/106.64 cnf(5830,plain,
% 106.56/106.64 (~P1(x58301,f46(a88,a88))),
% 106.56/106.64 inference(rename_variables,[],[915])).
% 106.56/106.64 cnf(5832,plain,
% 106.56/106.64 (~P1(f23(a65,a3),a65)),
% 106.56/106.64 inference(scs_inference,[],[1,319,743,788,790,1105,5683,5337,5578,5653,5661,5677,5221,5686,5731,5586,5681,5665,5509,1787,547,5531,5415,648,5818,915,5827,14,8,99,29,52,51,69,27,70,37,39,38,50,32,102,30,23,71,20,15,31,28,36,22,17,48,94,78,79,41,45,47,49,33,46,76,44,81,43,98])).
% 106.56/106.64 cnf(5833,plain,
% 106.56/106.64 (P1(x58331,a3)),
% 106.56/106.64 inference(rename_variables,[],[8])).
% 106.56/106.64 cnf(5839,plain,
% 106.56/106.64 (P6(f74(a71),f74(a71),a73)),
% 106.56/106.64 inference(scs_inference,[],[1,319,743,788,790,1105,5683,5337,5578,5653,5661,5677,5221,5686,5731,5586,5681,5665,5509,5607,1787,547,5531,5415,648,5818,915,5827,5830,14,8,99,29,52,51,69,27,70,37,39,38,50,32,102,30,23,71,20,15,31,28,36,22,17,48,94,78,79,41,45,47,49,33,46,76,44,81,43,98,80,34])).
% 106.56/106.64 cnf(5841,plain,
% 106.56/106.64 (P1(f36(a62,a3),a62)),
% 106.56/106.64 inference(scs_inference,[],[1,319,743,788,790,1105,5683,5317,5337,5578,5653,5661,5677,5221,5686,5731,5586,5681,5665,5509,5607,1787,547,5531,5415,648,5818,915,5827,5830,14,8,5833,99,29,52,51,69,27,70,37,39,38,50,32,102,30,23,71,20,15,31,28,36,22,17,48,94,78,79,41,45,47,49,33,46,76,44,81,43,98,80,34,93])).
% 106.56/106.64 cnf(5853,plain,
% 106.56/106.64 (P1(x58531,a56)+P1(f19(a56,a58),a56)),
% 106.56/106.64 inference(scs_inference,[],[1,319,743,788,790,1105,5729,5683,5317,5337,5578,5798,5649,5653,5661,5677,5221,5686,5731,5586,5681,5665,5509,5607,5679,1787,547,5531,5415,648,5818,915,5827,5830,14,5821,8,5833,99,29,52,51,69,27,70,37,39,38,50,32,102,30,23,71,20,15,31,28,36,22,17,48,94,78,79,41,45,47,49,33,46,76,44,81,43,98,80,34,93,91,74,1257,96])).
% 106.56/106.64 cnf(5857,plain,
% 106.56/106.64 (P1(f19(a56,a58),a56)),
% 106.56/106.64 inference(factoring_inference,[],[5853])).
% 106.56/106.64 cnf(5888,plain,
% 106.56/106.64 (~P1(f19(a56,a58),f74(a56))),
% 106.56/106.64 inference(scs_inference,[],[339,1103,1211,1215,5365,5857,5793,5177,915,29,52,69,99,51,70,27,37,38,39,32,102,50,23,30,20])).
% 106.56/106.64 cnf(5900,plain,
% 106.56/106.64 (P6(x59001,f74(a2),a80)),
% 106.56/106.64 inference(scs_inference,[],[339,1103,1211,1215,5365,5857,5720,5793,5177,915,29,52,69,99,51,70,27,37,38,39,32,102,50,23,30,20,71,31,15,36,28,22])).
% 106.56/106.64 cnf(5902,plain,
% 106.56/106.64 (P1(f14(a2,a71),f74(a71))),
% 106.56/106.64 inference(scs_inference,[],[339,1103,1211,1215,5365,5857,5720,5377,5793,5177,915,29,52,69,99,51,70,27,37,38,39,32,102,50,23,30,20,71,31,15,36,28,22,17])).
% 106.56/106.64 cnf(5904,plain,
% 106.56/106.64 (~P2(a86,a84)),
% 106.56/106.64 inference(scs_inference,[],[339,1103,1211,1215,5183,5365,5857,5720,5377,5793,5777,5177,915,29,52,69,99,51,70,27,37,38,39,32,102,50,23,30,20,71,31,15,36,28,22,17,94])).
% 106.56/106.64 cnf(5909,plain,
% 106.56/106.64 (~P1(x59091,f46(a88,a88))),
% 106.56/106.64 inference(rename_variables,[],[915])).
% 106.56/106.64 cnf(5912,plain,
% 106.56/106.64 (P1(x59121,f48(a84,a84))),
% 106.56/106.64 inference(rename_variables,[],[648])).
% 106.56/106.64 cnf(5918,plain,
% 106.56/106.64 (P6(a56,a56,a8)),
% 106.56/106.64 inference(scs_inference,[],[339,1103,1211,1215,5183,5365,5857,5720,5377,5501,5783,5781,5793,5777,5177,648,915,29,52,69,99,51,70,27,37,38,39,32,102,50,23,30,20,71,31,15,36,28,22,17,94,48,45,49,47,33])).
% 106.56/106.64 cnf(5933,plain,
% 106.56/106.64 (P1(f77(a56,a56),a56)),
% 106.56/106.64 inference(scs_inference,[],[339,1103,1211,1215,5183,5570,5580,5365,5857,5720,5377,5501,5783,5781,5793,5777,5177,648,5912,915,5909,29,52,69,99,51,70,27,37,38,39,32,102,50,23,30,20,71,31,15,36,28,22,17,94,48,45,49,47,33,46,44,81,75,43,80])).
% 106.56/106.64 cnf(5935,plain,
% 106.56/106.64 (P6(a56,a56,a73)),
% 106.56/106.64 inference(scs_inference,[],[339,1103,1211,1215,5183,5570,5580,5365,5857,5720,5377,5501,5783,5781,5793,5777,5177,648,5912,915,5909,29,52,69,99,51,70,27,37,38,39,32,102,50,23,30,20,71,31,15,36,28,22,17,94,48,45,49,47,33,46,44,81,75,43,80,34])).
% 106.56/106.64 cnf(5941,plain,
% 106.56/106.64 (P1(f76(a56,a56),a56)),
% 106.56/106.64 inference(scs_inference,[],[339,1103,1211,1215,5183,5570,5580,5365,5857,5720,5377,5501,5783,5781,5793,5777,5839,5177,13,648,5912,915,5909,29,52,69,99,51,70,27,37,38,39,32,102,50,23,30,20,71,31,15,36,28,22,17,94,48,45,49,47,33,46,44,81,75,43,80,34,91,1257,53])).
% 106.56/106.64 cnf(5961,plain,
% 106.56/106.64 (~P6(a59,x59611,a83)),
% 106.56/106.64 inference(scs_inference,[],[1227,1231,5479,5820,639,52,69,51,29,99,27,70,37])).
% 106.56/106.64 cnf(5963,plain,
% 106.56/106.64 (~P6(a59,x59631,a89)),
% 106.56/106.64 inference(scs_inference,[],[1227,1231,5479,5820,639,52,69,51,29,99,27,70,37,39])).
% 106.56/106.64 cnf(5969,plain,
% 106.56/106.64 (~P6(a59,x59691,a85)),
% 106.56/106.64 inference(scs_inference,[],[344,1227,1231,5479,5820,639,52,69,51,29,99,27,70,37,39,102,50,38])).
% 106.56/106.64 cnf(5975,plain,
% 106.56/106.64 (P6(a59,x59751,a86)),
% 106.56/106.64 inference(scs_inference,[],[344,1227,1231,5479,5820,639,52,69,51,29,99,27,70,37,39,102,50,38,32,30,23])).
% 106.56/106.64 cnf(5989,plain,
% 106.56/106.64 (P6(x59891,a59,a80)),
% 106.56/106.64 inference(scs_inference,[],[344,1227,1231,5479,5733,5715,5820,639,52,69,51,29,99,27,70,37,39,102,50,38,32,30,23,71,20,15,31,28,36,22])).
% 106.56/106.64 cnf(5991,plain,
% 106.56/106.64 (P1(f4(a59),a59)),
% 106.56/106.64 inference(scs_inference,[],[344,1227,1231,5479,5733,5715,5820,639,52,69,51,29,99,27,70,37,39,102,50,38,32,30,23,71,20,15,31,28,36,22,21])).
% 106.56/106.64 cnf(5993,plain,
% 106.56/106.64 (P1(f40(a71,a58),f74(a71))),
% 106.56/106.64 inference(scs_inference,[],[344,1227,1231,5479,5733,5715,5385,5820,639,52,69,51,29,99,27,70,37,39,102,50,38,32,30,23,71,20,15,31,28,36,22,21,17])).
% 106.56/106.64 cnf(6001,plain,
% 106.56/106.64 (~P2(a73,a85)),
% 106.56/106.64 inference(scs_inference,[],[1,344,1227,1231,5655,5479,5935,5733,5715,5385,5888,5820,5857,639,52,69,51,29,99,27,70,37,39,102,50,38,32,30,23,71,20,15,31,28,36,22,21,17,79,41,48,94])).
% 106.56/106.64 cnf(6012,plain,
% 106.56/106.64 (P6(a59,a59,a8)),
% 106.56/106.64 inference(scs_inference,[],[1,344,1227,1231,5655,5479,5935,5733,5715,5385,5888,5902,5820,5377,5343,5586,5857,639,52,69,51,29,99,27,70,37,39,102,50,38,32,30,23,71,20,15,31,28,36,22,21,17,79,41,48,94,78,49,47,45,33])).
% 106.56/106.64 cnf(6015,plain,
% 106.56/106.64 (P1(x60151,f48(a84,a84))),
% 106.56/106.64 inference(rename_variables,[],[648])).
% 106.56/106.64 cnf(6020,plain,
% 106.56/106.64 (P1(f78(a59,a59),a59)),
% 106.56/106.64 inference(scs_inference,[],[1,344,1227,1231,5655,5479,5935,5733,5715,5385,5888,5902,5820,5377,5343,5586,5857,648,6015,639,52,69,51,29,99,27,70,37,39,102,50,38,32,30,23,71,20,15,31,28,36,22,21,17,79,41,48,94,78,49,47,45,33,46,44,81])).
% 106.56/106.64 cnf(6025,plain,
% 106.56/106.64 (P1(f77(a59,a59),a59)),
% 106.56/106.64 inference(scs_inference,[],[1,344,1227,1231,5655,5479,5935,5733,5715,5385,5888,5902,5820,5377,5343,5586,5857,648,6015,639,52,69,51,29,99,27,70,37,39,102,50,38,32,30,23,71,20,15,31,28,36,22,21,17,79,41,48,94,78,49,47,45,33,46,44,81,43,80])).
% 106.56/106.64 cnf(6027,plain,
% 106.56/106.64 (P6(a59,a59,a73)),
% 106.56/106.64 inference(scs_inference,[],[1,344,1227,1231,5655,5479,5935,5733,5715,5385,5888,5902,5820,5377,5343,5586,5857,648,6015,639,52,69,51,29,99,27,70,37,39,102,50,38,32,30,23,71,20,15,31,28,36,22,21,17,79,41,48,94,78,49,47,45,33,46,44,81,43,80,34])).
% 106.56/106.64 cnf(6032,plain,
% 106.56/106.64 (P6(a56,a56,a81)),
% 106.56/106.64 inference(scs_inference,[],[1,344,1227,1231,5655,5479,5918,5935,5733,5715,5385,5888,5902,5820,5677,5377,5343,5586,5857,13,648,6015,639,52,69,51,29,99,27,70,37,39,102,50,38,32,30,23,71,20,15,31,28,36,22,21,17,79,41,48,94,78,49,47,45,33,46,44,81,43,80,34,105,91])).
% 106.56/106.64 cnf(6037,plain,
% 106.56/106.64 (~P6(a59,a58,a75)),
% 106.56/106.64 inference(scs_inference,[],[1,344,1227,1231,5655,5479,5918,5935,5733,5715,5385,5888,5902,5820,5167,5677,7,5377,5343,5586,5857,13,648,6015,639,52,69,51,29,99,27,70,37,39,102,50,38,32,30,23,71,20,15,31,28,36,22,21,17,79,41,48,94,78,49,47,45,33,46,44,81,43,80,34,105,91,74,1257])).
% 106.56/106.64 cnf(6039,plain,
% 106.56/106.64 (P1(f76(a59,a59),a59)),
% 106.56/106.64 inference(scs_inference,[],[1,344,1227,1231,5655,5479,5918,5935,5733,5715,5385,5888,5902,5820,5167,5677,7,5377,5343,5586,5857,13,648,6015,639,52,69,51,29,99,27,70,37,39,102,50,38,32,30,23,71,20,15,31,28,36,22,21,17,79,41,48,94,78,49,47,45,33,46,44,81,43,80,34,105,91,74,1257,53])).
% 106.56/106.64 cnf(6044,plain,
% 106.56/106.64 (~P1(f22(a71,a71),a71)),
% 106.56/106.64 inference(scs_inference,[],[1,344,1227,1231,5655,5479,5918,5935,5733,5715,5385,5888,5902,5820,574,5165,5167,5677,7,5377,5343,5586,5857,13,648,6015,639,14,52,69,51,29,99,27,70,37,39,102,50,38,32,30,23,71,20,15,31,28,36,22,21,17,79,41,48,94,78,49,47,45,33,46,44,81,43,80,34,105,91,74,1257,53,76,90])).
% 106.56/106.64 cnf(6056,plain,
% 106.56/106.64 (P6(f45(a73,a73),f46(a73,a73),a73)),
% 106.56/106.64 inference(scs_inference,[],[1244,69])).
% 106.56/106.64 cnf(6070,plain,
% 106.56/106.64 (~P6(a69,x60701,a83)),
% 106.56/106.64 inference(scs_inference,[],[1244,1246,1612,1614,5592,5509,776,915,69,51,99,52,29,70,27,37])).
% 106.56/106.64 cnf(6074,plain,
% 106.56/106.64 (~P6(f45(a5,a5),x60741,a88)),
% 106.56/106.64 inference(scs_inference,[],[352,1244,1246,1612,1614,5592,5509,776,915,69,51,99,52,29,70,27,37,102,32])).
% 106.56/106.64 cnf(6076,plain,
% 106.56/106.64 (~P6(a69,x60761,a85)),
% 106.56/106.64 inference(scs_inference,[],[352,1244,1246,1612,1614,5592,5509,776,915,69,51,99,52,29,70,27,37,102,32,38])).
% 106.56/106.64 cnf(6078,plain,
% 106.56/106.64 (~P6(a69,x60781,a89)),
% 106.56/106.64 inference(scs_inference,[],[352,1244,1246,1612,1614,5592,5509,776,915,69,51,99,52,29,70,27,37,102,32,38,39])).
% 106.56/106.64 cnf(6082,plain,
% 106.56/106.64 (P6(a69,x60821,a86)),
% 106.56/106.64 inference(scs_inference,[],[352,1244,1246,1612,1614,5592,5509,776,915,69,51,99,52,29,70,27,37,102,32,38,39,50,23])).
% 106.56/106.64 cnf(6084,plain,
% 106.56/106.64 (~P6(x60841,f45(a5,a5),a85)),
% 106.56/106.64 inference(scs_inference,[],[352,1244,1246,1612,1614,5592,5509,776,915,69,51,99,52,29,70,27,37,102,32,38,39,50,23,30])).
% 106.56/106.64 cnf(6086,plain,
% 106.56/106.64 (~P1(f76(a56,a56),f74(a56))),
% 106.56/106.64 inference(scs_inference,[],[352,1244,1246,1612,1614,5592,5941,5509,776,915,69,51,99,52,29,70,27,37,102,32,38,39,50,23,30,20])).
% 106.56/106.64 cnf(6090,plain,
% 106.56/106.64 (~P6(f45(a5,a5),x60901,a84)),
% 106.56/106.64 inference(scs_inference,[],[352,1244,1246,1612,1614,5592,5941,5509,776,915,69,51,99,52,29,70,27,37,102,32,38,39,50,23,30,20,71,31])).
% 106.56/106.64 cnf(6092,plain,
% 106.56/106.64 (P1(f29(a62,a2),a65)),
% 106.56/106.64 inference(scs_inference,[],[352,1244,1246,1612,1614,5592,5941,5498,5509,776,915,69,51,99,52,29,70,27,37,102,32,38,39,50,23,30,20,71,31,15])).
% 106.56/106.64 cnf(6094,plain,
% 106.56/106.64 (~P6(a69,x60941,a5)),
% 106.56/106.64 inference(scs_inference,[],[352,1244,1246,1612,1614,5592,5941,5498,5509,776,915,69,51,99,52,29,70,27,37,102,32,38,39,50,23,30,20,71,31,15,36])).
% 106.56/106.64 cnf(6096,plain,
% 106.56/106.64 (~P6(x60961,f45(a5,a5),a84)),
% 106.56/106.64 inference(scs_inference,[],[352,1244,1246,1612,1614,5592,5941,5498,5509,776,915,69,51,99,52,29,70,27,37,102,32,38,39,50,23,30,20,71,31,15,36,28])).
% 106.56/106.64 cnf(6098,plain,
% 106.56/106.64 (P6(x60981,a69,a80)),
% 106.56/106.64 inference(scs_inference,[],[352,1244,1246,1612,1614,5592,5941,5498,5509,776,915,69,51,99,52,29,70,27,37,102,32,38,39,50,23,30,20,71,31,15,36,28,22])).
% 106.56/106.64 cnf(6102,plain,
% 106.56/106.64 (P1(f22(a2,a2),f74(a2))),
% 106.56/106.64 inference(scs_inference,[],[352,1244,1246,1612,1614,5592,5941,5498,5726,5509,776,915,69,51,99,52,29,70,27,37,102,32,38,39,50,23,30,20,71,31,15,36,28,22,21,17])).
% 106.56/106.64 cnf(6108,plain,
% 106.56/106.64 (~P1(x61081,f45(a5,a5))),
% 106.56/106.64 inference(rename_variables,[],[776])).
% 106.56/106.64 cnf(6110,plain,
% 106.56/106.64 (~P2(a86,a83)),
% 106.56/106.64 inference(scs_inference,[],[352,1244,1246,1612,1614,5592,5961,5975,5989,5941,5498,5726,5509,776,915,69,51,99,52,29,70,27,37,102,32,38,39,50,23,30,20,71,31,15,36,28,22,21,17,79,48,94])).
% 106.56/106.64 cnf(6111,plain,
% 106.56/106.64 (~P6(a59,x61111,a83)),
% 106.56/106.64 inference(rename_variables,[],[5961])).
% 106.56/106.64 cnf(6120,plain,
% 106.56/106.64 (P1(x61201,f48(a84,a84))),
% 106.56/106.64 inference(rename_variables,[],[648])).
% 106.56/106.64 cnf(6126,plain,
% 106.56/106.64 (P6(a69,a69,a8)),
% 106.56/106.64 inference(scs_inference,[],[352,1244,1246,1612,1614,5592,5961,6111,5975,5989,5941,5498,5726,5509,5343,5586,5686,5793,648,776,915,69,51,99,52,29,70,27,37,102,32,38,39,50,23,30,20,71,31,15,36,28,22,21,17,79,48,94,41,78,45,49,47,33])).
% 106.56/106.64 cnf(6138,plain,
% 106.56/106.64 (P1(f77(a69,a69),a69)),
% 106.56/106.64 inference(scs_inference,[],[352,1244,1246,1612,1614,5592,5961,6111,5975,5989,5941,5498,5726,5993,5509,5343,5586,5686,5385,5793,648,6120,776,6108,915,69,51,99,52,29,70,27,37,102,32,38,39,50,23,30,20,71,31,15,36,28,22,21,17,79,48,94,41,78,45,49,47,33,46,44,81,43,80])).
% 106.56/106.64 cnf(6140,plain,
% 106.56/106.64 (P6(a69,a69,a73)),
% 106.56/106.64 inference(scs_inference,[],[352,1244,1246,1612,1614,5592,5961,6111,5975,5989,5941,5498,5726,5993,5509,5343,5586,5686,5385,5793,648,6120,776,6108,915,69,51,99,52,29,70,27,37,102,32,38,39,50,23,30,20,71,31,15,36,28,22,21,17,79,48,94,41,78,45,49,47,33,46,44,81,43,80,34])).
% 106.56/106.64 cnf(6149,plain,
% 106.56/106.64 (P1(f76(a69,a69),a69)),
% 106.56/106.64 inference(scs_inference,[],[1,352,1244,1246,1612,1614,5592,5961,6111,5963,5975,5989,6027,5941,5498,5726,5993,5509,5343,5586,5686,5385,5793,13,648,6120,776,6108,915,69,51,99,52,29,70,27,37,102,32,38,39,50,23,30,20,71,31,15,36,28,22,21,17,79,48,94,41,78,45,49,47,33,46,44,81,43,80,34,91,74,1257,53])).
% 106.56/106.64 cnf(6167,plain,
% 106.56/106.64 (~P6(a71,x61671,a83)),
% 106.56/106.64 inference(scs_inference,[],[1628,1630,1660,1662,5904,7,915,52,51,99,69,29,70,37])).
% 106.56/106.64 cnf(6173,plain,
% 106.56/106.64 (~P6(a58,x61731,a88)),
% 106.56/106.64 inference(scs_inference,[],[359,1628,1630,1660,1662,5904,7,915,14,52,51,99,69,29,70,37,38,102,32])).
% 106.56/106.64 cnf(6177,plain,
% 106.56/106.64 (~P6(a71,x61771,a89)),
% 106.56/106.64 inference(scs_inference,[],[359,1628,1630,1660,1662,5904,7,915,14,52,51,99,69,29,70,37,38,102,32,50,39])).
% 106.56/106.64 cnf(6181,plain,
% 106.56/106.64 (P6(a71,x61811,a86)),
% 106.56/106.64 inference(scs_inference,[],[359,1628,1630,1660,1662,5904,7,915,14,52,51,99,69,29,70,37,38,102,32,50,39,30,23])).
% 106.56/106.64 cnf(6183,plain,
% 106.56/106.64 (~P1(f76(a59,a59),f74(a59))),
% 106.56/106.64 inference(scs_inference,[],[359,1628,1630,1660,1662,5904,6039,7,915,14,52,51,99,69,29,70,37,38,102,32,50,39,30,23,20])).
% 106.56/106.64 cnf(6195,plain,
% 106.56/106.64 (P6(x61951,a71,a80)),
% 106.56/106.64 inference(scs_inference,[],[359,1628,1630,1660,1662,5904,6039,5739,7,915,14,52,51,99,69,29,70,37,38,102,32,50,39,30,23,20,71,31,15,36,28,22])).
% 106.56/106.64 cnf(6197,plain,
% 106.56/106.64 (P1(f4(a71),a71)),
% 106.56/106.64 inference(scs_inference,[],[359,1628,1630,1660,1662,5904,6039,5739,7,915,14,52,51,99,69,29,70,37,38,102,32,50,39,30,23,20,71,31,15,36,28,22,21])).
% 106.56/106.64 cnf(6204,plain,
% 106.56/106.64 (P6(x62041,a69,a80)),
% 106.56/106.64 inference(rename_variables,[],[6098])).
% 106.56/106.64 cnf(6206,plain,
% 106.56/106.64 (P1(f32(a69,a2),a69)),
% 106.56/106.64 inference(scs_inference,[],[1,359,1628,1630,1660,1662,5904,6070,6098,6039,5739,5623,1787,7,5586,915,14,52,51,99,69,29,70,37,38,102,32,50,39,30,23,20,71,31,15,36,28,22,21,17,48,79,41])).
% 106.56/106.64 cnf(6209,plain,
% 106.56/106.64 (~P2(a80,a85)),
% 106.56/106.64 inference(scs_inference,[],[1,359,1628,1630,1660,1662,5904,5969,6070,6098,6204,6039,5739,5623,1787,7,5586,915,14,52,51,99,69,29,70,37,38,102,32,50,39,30,23,20,71,31,15,36,28,22,21,17,48,79,41,94])).
% 106.56/106.64 cnf(6213,plain,
% 106.56/106.64 (P1(f29(a69,a2),a69)),
% 106.56/106.64 inference(scs_inference,[],[1,359,1628,1630,1660,1662,5904,5969,6070,6082,6098,6204,6039,5739,5623,1787,7,5586,915,14,52,51,99,69,29,70,37,38,102,32,50,39,30,23,20,71,31,15,36,28,22,21,17,48,79,41,94,78])).
% 106.56/106.64 cnf(6222,plain,
% 106.56/106.64 (P6(f74(a2),f74(a2),a8)),
% 106.56/106.64 inference(scs_inference,[],[1,359,1628,1630,1660,1662,5904,5969,6070,6082,6098,6204,6039,6102,5739,5623,1787,7,5781,5531,5726,5586,5731,5665,915,14,52,51,99,69,29,70,37,38,102,32,50,39,30,23,20,71,31,15,36,28,22,21,17,48,79,41,94,78,45,47,49,33])).
% 106.56/106.64 cnf(6229,plain,
% 106.56/106.64 (~P1(x62291,f46(a88,a88))),
% 106.56/106.64 inference(rename_variables,[],[915])).
% 106.56/106.64 cnf(6234,plain,
% 106.56/106.64 (P6(f74(a2),f74(a2),a73)),
% 106.56/106.64 inference(scs_inference,[],[1,359,1628,1630,1660,1662,5904,5969,6070,6082,6098,6204,6039,6086,6102,5739,5623,1787,7,5781,5531,5726,5586,5731,5941,5665,915,6229,14,52,51,99,69,29,70,37,38,102,32,50,39,30,23,20,71,31,15,36,28,22,21,17,48,79,41,94,78,45,47,49,33,46,44,81,43,34])).
% 106.56/106.64 cnf(6236,plain,
% 106.56/106.64 (P6(a69,a69,a81)),
% 106.56/106.64 inference(scs_inference,[],[1,359,1628,1630,1660,1662,5904,5969,6070,6082,6098,6204,6140,6039,6086,6102,5739,5623,1787,7,5781,5531,5726,5586,5731,5941,5665,13,915,6229,14,52,51,99,69,29,70,37,38,102,32,50,39,30,23,20,71,31,15,36,28,22,21,17,48,79,41,94,78,45,47,49,33,46,44,81,43,34,91])).
% 106.56/106.64 cnf(6243,plain,
% 106.56/106.64 (~P6(a71,a58,a75)),
% 106.56/106.64 inference(scs_inference,[],[1,359,1628,1630,1660,1662,5904,5969,6070,6078,6082,6098,6204,6140,6039,6086,6102,5739,5623,5599,1787,7,5781,5531,5726,5586,5731,5941,5665,13,915,6229,14,52,51,99,69,29,70,37,38,102,32,50,39,30,23,20,71,31,15,36,28,22,21,17,48,79,41,94,78,45,47,49,33,46,44,81,43,34,91,74,27,1257])).
% 106.56/106.64 cnf(6245,plain,
% 106.56/106.64 (P6(a59,a58,a9)),
% 106.56/106.64 inference(scs_inference,[],[1,359,1628,1630,1660,1662,5904,5969,6070,6078,6082,6098,6204,6140,6039,6086,6102,5739,5623,5599,1787,7,5781,5531,5726,5586,5731,5941,5665,13,915,6229,14,579,52,51,99,69,29,70,37,38,102,32,50,39,30,23,20,71,31,15,36,28,22,21,17,48,79,41,94,78,45,47,49,33,46,44,81,43,34,91,74,27,1257,40])).
% 106.56/106.64 cnf(6248,plain,
% 106.56/106.64 (~P5(a80,a8)),
% 106.56/106.64 inference(scs_inference,[],[1,359,1628,1630,1660,1662,6012,5904,5969,6070,6078,6082,6098,6204,6140,6039,6086,6102,5739,5623,5989,5599,1787,7,5781,5531,5726,5586,5731,5941,5665,13,915,6229,14,579,52,51,99,69,29,70,37,38,102,32,50,39,30,23,20,71,31,15,36,28,22,21,17,48,79,41,94,78,45,47,49,33,46,44,81,43,34,91,74,27,1257,40,104])).
% 106.56/106.64 cnf(6249,plain,
% 106.56/106.64 (P6(x62491,a59,a80)),
% 106.56/106.64 inference(rename_variables,[],[5989])).
% 106.56/106.64 cnf(6251,plain,
% 106.56/106.64 (P3(a80,a8)),
% 106.56/106.64 inference(scs_inference,[],[1,359,1628,1630,1660,1662,6012,5904,5969,6070,6078,6082,6098,6204,6140,6039,6086,6102,5739,5623,5989,6249,5599,1787,7,5781,5531,5726,5586,5731,5941,5665,13,915,6229,14,579,52,51,99,69,29,70,37,38,102,32,50,39,30,23,20,71,31,15,36,28,22,21,17,48,79,41,94,78,45,47,49,33,46,44,81,43,34,91,74,27,1257,40,104,100])).
% 106.56/106.64 cnf(6291,plain,
% 106.56/106.64 (~P1(f77(a56,a56),f74(a56))),
% 106.56/106.64 inference(scs_inference,[],[367,1770,1772,1779,1781,5692,5933,6183,648,69,51,52,99,29,70,32,50,37,102,38,39,30,20])).
% 106.56/106.64 cnf(6293,plain,
% 106.56/106.64 (P6(f48(a84,a84),x62931,a86)),
% 106.56/106.64 inference(scs_inference,[],[367,1770,1772,1779,1781,5692,5933,6183,648,69,51,52,99,29,70,32,50,37,102,38,39,30,20,23])).
% 106.56/106.64 cnf(6312,plain,
% 106.56/106.64 (~P1(x63121,f45(a5,a5))),
% 106.56/106.64 inference(rename_variables,[],[776])).
% 106.56/106.64 cnf(6327,plain,
% 106.56/106.64 (~P2(a9,a75)),
% 106.56/106.64 inference(scs_inference,[],[1,367,1770,1772,1779,1781,6245,6037,6167,6181,6195,5692,5933,6025,6183,5523,5832,6039,648,776,69,51,52,99,29,70,32,50,37,102,38,39,30,20,23,71,31,15,36,28,22,65,17,48,41,78,79,47,45,94])).
% 106.56/106.64 cnf(6342,plain,
% 106.56/106.64 (P1(f77(a71,a71),a71)),
% 106.56/106.64 inference(scs_inference,[],[1,367,1770,1772,1779,1781,6245,6037,6167,6181,6195,5692,5933,6025,6183,5523,5832,6197,6039,648,776,6312,69,51,52,99,29,70,32,50,37,102,38,39,30,20,23,71,31,15,36,28,22,65,17,48,41,78,79,47,45,94,49,33,46,44,81,43,80])).
% 106.56/106.64 cnf(6357,plain,
% 106.56/106.64 (P1(f19(a71,a58),a71)),
% 106.56/106.64 inference(scs_inference,[],[1,367,1770,1772,1779,1781,6245,6037,6076,6167,6177,6181,6195,5692,6243,5933,6025,6056,6183,6092,5523,5832,6044,6197,6039,13,648,776,6312,14,8,69,51,52,99,29,70,32,50,37,102,38,39,30,20,23,71,31,15,36,28,22,65,17,48,41,78,79,47,45,94,49,33,46,44,81,43,80,34,91,54,93,74,96])).
% 106.56/106.64 cnf(6379,plain,
% 106.56/106.64 (~P6(a3,x63791,a85)),
% 106.56/106.64 inference(scs_inference,[],[1132,1136,5797,8,99,51,69,52,38])).
% 106.56/106.64 cnf(6391,plain,
% 106.56/106.64 (P6(a3,x63911,a86)),
% 106.56/106.64 inference(scs_inference,[],[373,1132,1136,5797,8,579,99,51,69,52,38,102,70,37,50,39,23])).
% 106.56/106.64 cnf(6395,plain,
% 106.56/106.64 (~P1(a55,f74(a56))),
% 106.56/106.64 inference(scs_inference,[],[2,373,1132,1136,5797,8,579,99,51,69,52,38,102,70,37,50,39,23,71,20])).
% 106.56/106.64 cnf(6397,plain,
% 106.56/106.64 (~P6(a58,x63971,a84)),
% 106.56/106.64 inference(scs_inference,[],[2,373,1132,1136,5797,14,8,579,99,51,69,52,38,102,70,37,50,39,23,71,20,31])).
% 106.56/106.64 cnf(6401,plain,
% 106.56/106.64 (~P6(a3,x64011,a5)),
% 106.56/106.64 inference(scs_inference,[],[2,373,1132,1136,5797,5620,14,8,579,99,51,69,52,38,102,70,37,50,39,23,71,20,31,15,36])).
% 106.56/106.64 cnf(6403,plain,
% 106.56/106.64 (P6(x64031,a3,a80)),
% 106.56/106.64 inference(scs_inference,[],[2,373,1132,1136,5797,5620,14,8,579,99,51,69,52,38,102,70,37,50,39,23,71,20,31,15,36,22])).
% 106.56/106.64 cnf(6407,plain,
% 106.56/106.64 (~P1(f14(a56,a71),a71)),
% 106.56/106.64 inference(scs_inference,[],[2,373,1132,1136,5797,5620,5224,5161,14,8,579,99,51,69,52,38,102,70,37,50,39,23,71,20,31,15,36,22,17,77])).
% 106.56/106.64 cnf(6410,plain,
% 106.56/106.64 (P1(f29(a56,a56),a56)),
% 106.56/106.64 inference(scs_inference,[],[2,373,1132,1136,5797,5620,5224,5161,5661,14,8,579,99,51,69,52,38,102,70,37,50,39,23,71,20,31,15,36,22,17,77,78])).
% 106.56/106.64 cnf(6428,plain,
% 106.56/106.64 (~P6(a69,a71,a91)),
% 106.56/106.64 inference(scs_inference,[],[2,373,1132,1136,6126,5797,6291,5620,6094,5224,5161,5163,5661,6098,5933,5902,5377,5781,5731,12,6,14,8,579,99,51,69,52,38,102,70,37,50,39,23,71,20,31,15,36,22,17,77,78,48,41,47,94,45,79,49])).
% 106.56/106.64 cnf(6430,plain,
% 106.56/106.64 (P6(f48(a84,a84),a56,a8)),
% 106.56/106.64 inference(scs_inference,[],[2,373,1132,1136,6126,5797,6291,5620,6094,5224,5161,5163,5661,6098,5933,5902,5377,5781,5731,12,6,648,14,8,579,99,51,69,52,38,102,70,37,50,39,23,71,20,31,15,36,22,17,77,78,48,41,47,94,45,79,49,33])).
% 106.56/106.64 cnf(6481,plain,
% 106.56/106.64 (~P1(f78(a59,a59),f74(a59))),
% 106.56/106.64 inference(scs_inference,[],[380,1149,1153,6001,6020,579,99,52,51,69,38,102,70,50,23,71,20])).
% 106.56/106.64 cnf(6489,plain,
% 106.56/106.64 (P1(f14(a56,a71),f74(a71))),
% 106.56/106.64 inference(scs_inference,[],[380,1149,1153,6001,6020,5841,6407,579,99,52,51,69,38,102,70,50,23,71,20,15,36,22,17])).
% 106.56/106.64 cnf(6492,plain,
% 106.56/106.64 (~P1(x64921,f45(a5,a5))),
% 106.56/106.64 inference(rename_variables,[],[776])).
% 106.56/106.64 cnf(6496,plain,
% 106.56/106.64 (~P6(a69,a71,a90)),
% 106.56/106.64 inference(scs_inference,[],[380,1149,1153,6001,6020,6149,5841,6407,12,6,776,579,99,52,51,69,38,102,70,50,23,71,20,15,36,22,17,48,45,47])).
% 106.56/106.64 cnf(6503,plain,
% 106.56/106.64 (P6(a56,f48(a84,a84),a8)),
% 106.56/106.64 inference(scs_inference,[],[2,380,1149,1153,6391,6401,6001,6020,6149,5841,6407,1567,12,6,648,776,11,579,99,52,51,69,38,102,70,50,23,71,20,15,36,22,17,48,45,47,94,49,33])).
% 106.56/106.64 cnf(6512,plain,
% 106.56/106.64 (P6(f48(a84,a84),a56,a73)),
% 106.56/106.64 inference(scs_inference,[],[2,380,1149,1153,6391,6401,6001,6020,6149,6395,5841,6407,1567,5781,5731,12,6,648,776,6492,11,579,99,52,51,69,38,102,70,50,23,71,20,15,36,22,17,48,45,47,94,49,33,44,46,43,34])).
% 106.56/106.64 cnf(6519,plain,
% 106.56/106.64 (P1(f72(a58,a69),a69)),
% 106.56/106.64 inference(scs_inference,[],[2,380,1149,1153,6391,6401,6001,6020,6149,6234,6395,5841,6407,586,1567,5781,5731,12,6,13,648,776,6492,11,14,579,99,52,51,69,38,102,70,50,23,71,20,15,36,22,17,48,45,47,94,49,33,44,46,43,34,91,1262,76])).
% 106.56/106.64 cnf(6522,plain,
% 106.56/106.64 (P1(x65221,a56)+P1(f35(a56,a56),a56)),
% 106.56/106.64 inference(scs_inference,[],[2,380,1149,1153,6391,6401,6001,6020,6149,6234,6395,5841,6407,586,5649,1567,5781,5731,12,6,13,648,776,6492,11,14,579,99,52,51,69,38,102,70,50,23,71,20,15,36,22,17,48,45,47,94,49,33,44,46,43,34,91,1262,76,74])).
% 106.56/106.64 cnf(6526,plain,
% 106.56/106.64 (P1(f35(a56,a56),a56)),
% 106.56/106.64 inference(factoring_inference,[],[6522])).
% 106.56/106.64 cnf(6566,plain,
% 106.56/106.64 (P1(f77(a3,a56),a56)),
% 106.56/106.64 inference(scs_inference,[],[2,394,1116,1120,6032,6110,6526,6481,6489,5675,5236,6020,6395,6407,10,5,12,6,3,8,52,99,102,51,69,70,50,20,71,17,45,47,48,94,49,33,46,44,43,80])).
% 106.56/106.64 cnf(6578,plain,
% 106.56/106.64 (P1(f29(a69,a56),a69)),
% 106.56/106.64 inference(scs_inference,[],[2,394,1116,1120,6032,6110,6526,6222,6481,5566,6489,5675,5236,6082,6020,6395,6407,10,5,12,6,3,8,52,99,102,51,69,70,50,20,71,17,45,47,48,94,49,33,46,44,43,80,34,91,1262,54,78])).
% 106.56/106.64 cnf(6608,plain,
% 106.56/106.64 (~P1(x66081,f46(a88,a88))),
% 106.56/106.64 inference(rename_variables,[],[915])).
% 106.56/106.64 cnf(6610,plain,
% 106.56/106.64 (~P2(a80,a91)),
% 106.56/106.64 inference(scs_inference,[],[400,997,1358,6428,6209,6566,6578,5254,6195,1567,915,11,99,52,70,51,102,50,69,20,71,17,47,48,94])).
% 106.56/106.64 cnf(6620,plain,
% 106.56/106.64 (P1(f78(a56,a3),a56)),
% 106.56/106.64 inference(scs_inference,[],[2,400,997,1358,6428,6209,6566,6578,5254,6195,1567,10,5,915,6608,11,8,99,52,70,51,102,50,69,20,71,17,47,48,94,33,46,44,81])).
% 106.56/106.64 cnf(6622,plain,
% 106.56/106.64 (~P6(f48(a84,a84),a62,a81)),
% 106.56/106.64 inference(scs_inference,[],[2,400,997,1358,6428,6209,6566,6578,5254,6195,1567,10,5,648,915,6608,11,8,99,52,70,51,102,50,69,20,71,17,47,48,94,33,46,44,81,43])).
% 106.56/106.64 cnf(6625,plain,
% 106.56/106.64 (P6(a3,a56,a73)),
% 106.56/106.64 inference(scs_inference,[],[2,400,997,1358,6428,6209,6566,6578,5254,6195,1567,10,5,648,915,6608,11,8,99,52,70,51,102,50,69,20,71,17,47,48,94,33,46,44,81,43,34])).
% 106.56/106.64 cnf(6628,plain,
% 106.56/106.64 (P1(f76(a3,a56),a56)),
% 106.56/106.64 inference(scs_inference,[],[2,400,997,1358,6428,6209,6566,6578,5254,6195,1567,10,5,648,915,6608,11,8,99,52,70,51,102,50,69,20,71,17,47,48,94,33,46,44,81,43,34,53])).
% 106.56/106.64 cnf(6630,plain,
% 106.56/106.64 (P6(a56,a58,a9)),
% 106.56/106.64 inference(scs_inference,[],[2,400,997,1358,6428,6209,6566,6578,5254,6195,1567,10,5,648,915,6608,11,8,579,99,52,70,51,102,50,69,20,71,17,47,48,94,33,46,44,81,43,34,53,40])).
% 106.56/106.64 cnf(6663,plain,
% 106.56/106.64 (P1(f38(a56,a58),a56)),
% 106.56/106.64 inference(scs_inference,[],[408,1348,1351,6630,6327,6620,52,99,51,102,50,70,69,71,20,65])).
% 106.56/106.64 cnf(6669,plain,
% 106.56/106.64 (~P6(a69,a71,a75)),
% 106.56/106.64 inference(scs_inference,[],[408,1348,1351,6630,6327,6620,5279,449,12,6,4,52,99,51,102,50,70,69,71,20,65,17,47,48])).
% 106.56/106.64 cnf(6671,plain,
% 106.56/106.64 (~P2(a9,a83)),
% 106.56/106.64 inference(scs_inference,[],[408,1348,1351,6630,6327,6620,5279,5653,449,12,6,4,52,99,51,102,50,70,69,71,20,65,17,47,48,94])).
% 106.56/106.64 cnf(6674,plain,
% 106.56/106.64 (P3(a81,a8)),
% 106.56/106.64 inference(scs_inference,[],[408,1348,1351,6630,6327,6503,6620,5279,715,5653,449,12,6,4,52,99,51,102,50,70,69,71,20,65,17,47,48,94,100])).
% 106.56/106.64 cnf(6675,plain,
% 106.56/106.64 (P6(x66751,f48(a84,a84),a81)),
% 106.56/106.64 inference(rename_variables,[],[715])).
% 106.56/106.64 cnf(6684,plain,
% 106.56/106.64 (~P1(x66841,f48(a5,a5))),
% 106.56/106.64 inference(rename_variables,[],[639])).
% 106.56/106.64 cnf(6689,plain,
% 106.56/106.64 (~P5(a81,a8)),
% 106.56/106.64 inference(scs_inference,[],[2,408,1348,1351,6630,6327,6503,6620,6519,5279,715,6675,5653,6489,6407,449,1567,12,6,4,639,6684,11,579,52,99,51,102,50,70,69,71,20,65,17,47,48,94,100,33,46,44,81,43,104])).
% 106.56/106.64 cnf(6695,plain,
% 106.56/106.64 (P6(a3,a56,a81)),
% 106.56/106.64 inference(scs_inference,[],[2,408,1348,1351,6630,6327,6625,6503,6620,6519,5279,715,6675,5653,6489,6407,449,1567,12,6,13,4,639,6684,11,579,52,99,51,102,50,70,69,71,20,65,17,47,48,94,100,33,46,44,81,43,104,34,91])).
% 106.56/106.64 cnf(6725,plain,
% 106.56/106.64 (~P2(a86,a90)),
% 106.56/106.64 inference(scs_inference,[],[415,880,878,2964,2958,6496,6610,6663,6342,1589,6082,776,52,99,102,51,69,50,70,71,20,17,48,94])).
% 106.56/106.64 cnf(6750,plain,
% 106.56/106.64 (~P6(f41(a9,a83),f47(a9,a83),a83)),
% 106.56/106.64 inference(scs_inference,[],[1199,6671,52,51,99])).
% 106.56/106.64 cnf(6754,plain,
% 106.56/106.64 (P6(f41(a9,a83),f47(a9,a83),a9)),
% 106.56/106.64 inference(scs_inference,[],[422,1199,6671,52,51,99,102,50])).
% 106.56/106.64 cnf(6766,plain,
% 106.56/106.64 (~P1(f14(a56,a65),a65)),
% 106.56/106.64 inference(scs_inference,[],[2,422,1199,1202,6671,6628,1865,5321,52,51,99,102,50,70,69,20,71,17,77])).
% 106.56/106.64 cnf(6769,plain,
% 106.56/106.64 (P1(f32(a62,a56),a62)),
% 106.56/106.64 inference(scs_inference,[],[2,422,1199,1202,6671,6628,1865,5315,5321,52,51,99,102,50,70,69,20,71,17,77,41])).
% 106.56/106.64 cnf(6772,plain,
% 106.56/106.64 (P1(f52(a56,a2),a2)),
% 106.56/106.64 inference(scs_inference,[],[2,422,1199,1202,6671,6628,1865,5315,5321,5189,52,51,99,102,50,70,69,20,71,17,77,41,79])).
% 106.56/106.64 cnf(6778,plain,
% 106.56/106.64 (~P2(a81,a83)),
% 106.56/106.64 inference(scs_inference,[],[2,422,1199,1202,6236,6671,6628,1865,5315,5321,6070,5189,639,52,51,99,102,50,70,69,20,71,17,77,41,79,48,94])).
% 106.56/106.64 cnf(6791,plain,
% 106.56/106.64 (P1(f32(a62,a56),a65)),
% 106.56/106.64 inference(scs_inference,[],[2,422,1199,1202,6236,6671,6512,6074,6090,6628,6138,1865,5315,5321,6070,5189,1813,5359,13,915,639,52,51,99,102,50,70,69,20,71,17,77,41,79,48,94,46,75,43,91,15])).
% 106.56/106.64 cnf(6819,plain,
% 106.56/106.64 (P1(f14(a56,a65),f74(a65))),
% 106.56/106.64 inference(scs_inference,[],[429,3310,3316,6725,6791,6766,52,51,99,102,70,69,50,20,71,17])).
% 106.56/106.64 cnf(6824,plain,
% 106.56/106.64 (P1(f72(a58,a2),a2)),
% 106.56/106.64 inference(scs_inference,[],[429,3310,3316,6725,6791,6766,6772,237,776,14,52,51,99,102,70,69,50,20,71,17,48,76])).
% 106.56/106.64 cnf(6827,plain,
% 106.56/106.64 (~P2(a80,a75)),
% 106.56/106.64 inference(scs_inference,[],[429,3310,3316,6669,6725,6791,6766,6772,237,6195,776,14,52,51,99,102,70,69,50,20,71,17,48,76,94])).
% 106.56/106.64 cnf(6864,plain,
% 106.56/106.64 (~P2(a81,a85)),
% 106.56/106.64 inference(scs_inference,[],[442,3882,3873,6379,6695,6778,6824,1817,52,51,99,70,102,50,69,20,71,17,94])).
% 106.56/106.64 cnf(6867,plain,
% 106.56/106.64 (~P6(a69,a71,a10)),
% 106.56/106.64 inference(scs_inference,[],[442,3882,3873,6379,6695,6778,6824,1817,12,6,52,51,99,70,102,50,69,20,71,17,94,46])).
% 106.56/106.64 cnf(6872,plain,
% 106.56/106.64 (P6(f74(a65),a65,a9)),
% 106.56/106.64 inference(scs_inference,[],[442,3882,3873,6379,6695,6778,6819,6824,1817,12,6,915,52,51,99,70,102,50,69,20,71,17,94,46,43,40])).
% 106.56/106.64 cnf(6903,plain,
% 106.56/106.64 (~P1(f32(a62,a56),f74(a62))),
% 106.56/106.64 inference(scs_inference,[],[445,3895,3886,6827,6769,52,51,99,102,70,69,50,20])).
% 106.56/106.64 cnf(6909,plain,
% 106.56/106.64 (~P2(a86,a10)),
% 106.56/106.64 inference(scs_inference,[],[445,3895,3886,6827,6867,6769,5526,6082,52,51,99,102,70,69,50,20,71,17,94])).
% 106.56/106.64 cnf(6938,plain,
% 106.56/106.64 (~P1(f4(a59),f74(a59))),
% 106.56/106.64 inference(scs_inference,[],[493,3908,3899,6909,5991,51,52,99,102,70,69,50,20])).
% 106.56/106.64 cnf(6944,plain,
% 106.56/106.64 (~P2(a8,a83)),
% 106.56/106.64 inference(scs_inference,[],[493,3908,3899,6909,5815,5763,5991,5351,51,52,99,102,70,69,50,20,71,17,94])).
% 106.56/106.64 cnf(6950,plain,
% 106.56/106.64 (~P6(a56,a58,a10)),
% 106.56/106.64 inference(scs_inference,[],[2,493,3908,3899,6909,5815,6903,5763,5991,5351,648,14,51,52,99,102,70,69,50,20,71,17,94,44,46])).
% 106.56/106.64 cnf(6981,plain,
% 106.56/106.64 (~P1(a55,f74(a59))),
% 106.56/106.64 inference(scs_inference,[],[3,501,3921,3912,6864,51,52,99,102,70,69,50,20])).
% 106.56/106.64 cnf(6987,plain,
% 106.56/106.64 (~P1(f14(a59,a2),a2)),
% 106.56/106.64 inference(scs_inference,[],[3,501,3921,3912,6864,5562,5275,51,52,99,102,70,69,50,20,71,17,77])).
% 106.56/106.64 cnf(6990,plain,
% 106.56/106.64 (P1(f32(a59,a59),a59)),
% 106.56/106.64 inference(scs_inference,[],[3,501,3921,3912,6864,5562,5961,5275,51,52,99,102,70,69,50,20,71,17,77,41])).
% 106.56/106.64 cnf(6993,plain,
% 106.56/106.64 (P1(f52(a59,a62),a62)),
% 106.56/106.64 inference(scs_inference,[],[3,501,3921,3912,6864,5562,5961,5345,5275,51,52,99,102,70,69,50,20,71,17,77,41,79])).
% 106.56/106.64 cnf(6997,plain,
% 106.56/106.64 (P1(x69971,f48(a84,a84))),
% 106.56/106.64 inference(rename_variables,[],[648])).
% 106.56/106.64 cnf(7003,plain,
% 106.56/106.64 (~P2(a86,a91)),
% 106.56/106.64 inference(scs_inference,[],[3,501,3921,3912,6864,5219,6938,5568,5562,5961,5345,5275,6395,648,6997,51,52,99,102,70,69,50,20,71,17,77,41,79,45,48,33,94])).
% 106.56/106.64 cnf(7019,plain,
% 106.56/106.64 (P1(f12(a56,a58),a56)),
% 106.56/106.64 inference(scs_inference,[],[3,501,3921,3912,6950,6397,6864,5219,6938,6084,6754,6750,5568,6410,5562,5961,5345,6903,6791,5275,6395,648,6997,14,51,52,99,102,70,69,50,20,71,17,77,41,79,45,48,33,94,75,46,43,34,91,92])).
% 106.56/106.64 cnf(7022,plain,
% 106.56/106.64 (P1(f52(a59,a62),a65)),
% 106.56/106.64 inference(scs_inference,[],[3,501,3921,3912,6950,6397,6864,5219,6938,6084,6754,6750,5568,6410,5562,5961,5345,6903,6791,5275,6395,648,6997,14,51,52,99,102,70,69,50,20,71,17,77,41,79,45,48,33,94,75,46,43,34,91,92,15])).
% 106.56/106.64 cnf(7046,plain,
% 106.56/106.64 (P1(f14(a59,a2),f74(a2))),
% 106.56/106.64 inference(scs_inference,[],[508,2952,2949,6944,7019,6987,51,52,99,102,70,69,50,71,20,17])).
% 106.56/106.64 cnf(7055,plain,
% 106.56/106.64 (~P2(a5,a82)),
% 106.56/106.64 inference(scs_inference,[],[3,508,2952,2949,6944,6981,7019,5667,7022,5659,6987,2,648,915,51,52,99,102,70,69,50,71,20,17,49,48,33,94])).
% 106.56/106.64 cnf(7102,plain,
% 106.56/106.64 (~P1(x71021,f48(a5,a5))),
% 106.56/106.64 inference(rename_variables,[],[639])).
% 106.56/106.64 cnf(7106,plain,
% 106.56/106.64 (~P2(a9,a10)),
% 106.56/106.64 inference(scs_inference,[],[3,514,2977,2968,7003,5245,6872,6990,5412,639,8,51,52,99,102,70,69,50,71,20,17,48,33,94])).
% 106.56/106.64 cnf(7113,plain,
% 106.56/106.64 (P6(a3,a59,a73)),
% 106.56/106.64 inference(scs_inference,[],[3,514,2977,2968,7003,5245,7046,6872,6990,6987,5412,639,7102,8,51,52,99,102,70,69,50,71,20,17,48,33,94,46,43,34])).
% 106.56/106.64 cnf(7119,plain,
% 106.56/106.64 (P1(f76(a3,a59),a59)),
% 106.56/106.64 inference(scs_inference,[],[3,514,2977,2968,7003,5245,7046,6872,6173,6990,3810,6987,5412,639,7102,8,51,52,99,102,70,69,50,71,20,17,48,33,94,46,43,34,91,53])).
% 106.56/106.64 cnf(7121,plain,
% 106.56/106.64 (P6(f74(a2),a2,a9)),
% 106.56/106.64 inference(scs_inference,[],[3,514,2977,2968,7003,5245,7046,6872,6173,6990,3810,6987,5412,639,7102,8,51,52,99,102,70,69,50,71,20,17,48,33,94,46,43,34,91,53,40])).
% 106.56/106.64 cnf(7145,plain,
% 106.56/106.64 (~P6(f49(a81,a88),f50(a81,a88),a88)),
% 106.56/106.64 inference(scs_inference,[],[531,3038,3044,7055,51,52,99,70,102])).
% 106.56/106.64 cnf(7151,plain,
% 106.56/106.64 (P6(f49(a81,a88),f50(a81,a88),a81)),
% 106.56/106.64 inference(scs_inference,[],[531,3038,3044,7055,51,52,99,70,102,69,50,71])).
% 106.56/106.64 cnf(7157,plain,
% 106.56/106.64 (~P6(a65,a62,a75)),
% 106.56/106.64 inference(scs_inference,[],[531,3038,3044,7055,7119,5599,10,5,51,52,99,70,102,69,50,71,20,17,48])).
% 106.56/106.64 cnf(7161,plain,
% 106.56/106.64 (~P2(a5,a90)),
% 106.56/106.64 inference(scs_inference,[],[3,531,3038,3044,7055,5779,7119,5773,5599,10,5,8,51,52,99,70,102,69,50,71,20,17,48,33,94])).
% 106.56/106.64 cnf(7163,plain,
% 106.56/106.64 (~P6(a59,a58,a10)),
% 106.56/106.64 inference(scs_inference,[],[3,531,3038,3044,7055,5779,7119,5773,5599,10,5,14,8,51,52,99,70,102,69,50,71,20,17,48,33,94,46])).
% 106.56/106.64 cnf(7169,plain,
% 106.56/106.64 (P6(a59,a3,a73)),
% 106.56/106.64 inference(scs_inference,[],[3,531,3038,3044,7055,5779,7119,5773,6206,5599,10,5,776,14,8,51,52,99,70,102,69,50,71,20,17,48,33,94,46,43,34])).
% 106.56/106.64 cnf(7170,plain,
% 106.56/106.64 (P1(x71701,a3)),
% 106.56/106.64 inference(rename_variables,[],[8])).
% 106.56/106.64 cnf(7174,plain,
% 106.56/106.64 (P1(f76(a59,a3),a59)),
% 106.56/106.64 inference(scs_inference,[],[3,531,3038,3044,7055,7113,5779,7119,5773,6206,5599,10,5,13,776,14,8,51,52,99,70,102,69,50,71,20,17,48,33,94,46,43,34,91,54])).
% 106.56/106.64 cnf(7176,plain,
% 106.56/106.64 (P1(f77(a3,a59),a59)),
% 106.56/106.64 inference(scs_inference,[],[3,531,3038,3044,7055,7113,5779,7119,5773,6206,5599,10,5,13,776,14,8,7170,51,52,99,70,102,69,50,71,20,17,48,33,94,46,43,34,91,54,80])).
% 106.56/106.64 cnf(7203,plain,
% 106.56/106.64 (~P1(x72031,f46(a88,a88))),
% 106.56/106.64 inference(rename_variables,[],[915])).
% 106.56/106.64 cnf(7205,plain,
% 106.56/106.64 (P6(a59,f74(a58),a8)),
% 106.56/106.64 inference(scs_inference,[],[3,550,6251,6248,7106,7174,5486,915,579,51,52,99,102,70,69,50,71,20,17,48,33])).
% 106.56/106.64 cnf(7207,plain,
% 106.56/106.64 (~P2(a80,a90)),
% 106.56/106.64 inference(scs_inference,[],[3,550,6251,6248,7106,5477,7174,5469,5486,915,579,51,52,99,102,70,69,50,71,20,17,48,33,94])).
% 106.56/106.64 cnf(7215,plain,
% 106.56/106.64 (~P5(a80,a73)),
% 106.56/106.64 inference(scs_inference,[],[3,550,6251,6248,7106,7169,5477,7174,6403,5250,5469,5486,6395,915,7203,579,51,52,99,102,70,69,50,71,20,17,48,33,94,46,43,104])).
% 106.56/106.64 cnf(7216,plain,
% 106.56/106.64 (P6(x72161,a3,a80)),
% 106.56/106.64 inference(rename_variables,[],[6403])).
% 106.56/106.64 cnf(7218,plain,
% 106.56/106.64 (P6(f74(a58),a59,a73)),
% 106.56/106.64 inference(scs_inference,[],[3,550,6251,6248,7106,7169,5477,7174,6403,5250,5469,5486,6395,915,7203,579,51,52,99,102,70,69,50,71,20,17,48,33,94,46,43,104,34])).
% 106.56/106.64 cnf(7223,plain,
% 106.56/106.64 (P3(a80,a73)),
% 106.56/106.64 inference(scs_inference,[],[3,550,6251,6248,7106,7169,5477,5397,7174,6403,7216,7121,5250,5469,5486,6395,915,7203,579,51,52,99,102,70,69,50,71,20,17,48,33,94,46,43,104,34,91,100])).
% 106.56/106.64 cnf(7255,plain,
% 106.56/106.64 (~P1(f14(a59,a62),a62)),
% 106.56/106.64 inference(scs_inference,[],[3,554,3033,3027,7161,7176,1580,6044,51,52,102,99,70,69,50,71,20,17,77])).
% 106.56/106.64 cnf(7258,plain,
% 106.56/106.64 (P1(f52(a59,a56),a56)),
% 106.56/106.64 inference(scs_inference,[],[3,554,3033,3027,7161,7176,1580,5677,6044,51,52,102,99,70,69,50,71,20,17,77,79])).
% 106.56/106.64 cnf(7267,plain,
% 106.56/106.64 (~P1(x72671,f48(a5,a5))),
% 106.56/106.64 inference(rename_variables,[],[639])).
% 106.56/106.64 cnf(7274,plain,
% 106.56/106.64 (~P2(a81,a88)),
% 106.56/106.64 inference(scs_inference,[],[3,554,3033,3027,7161,5483,6096,7151,7145,7176,6213,6167,1580,5677,6044,6981,2,639,579,51,52,102,99,70,69,50,71,20,17,77,79,41,45,48,75,33,94])).
% 106.56/106.64 cnf(7284,plain,
% 106.56/106.64 (P1(f12(a59,a58),a59)),
% 106.56/106.64 inference(scs_inference,[],[3,554,7163,3033,3027,7161,5483,6096,7151,7145,7218,7176,6213,6167,1580,5677,6044,6981,13,2,639,7267,14,579,51,52,102,99,70,69,50,71,20,17,77,79,41,45,48,75,33,94,43,34,91,92])).
% 106.56/106.64 cnf(7310,plain,
% 106.56/106.64 (P1(f14(a59,a62),f74(a62))),
% 106.56/106.64 inference(scs_inference,[],[885,7274,5744,5742,6674,6689,7284,7255,51,52,102,70,99,69,50,71,20,17])).
% 106.56/106.64 cnf(7312,plain,
% 106.56/106.64 (P1(f29(a56,a59),a56)),
% 106.56/106.64 inference(scs_inference,[],[3,885,7274,5744,5742,6674,6689,7284,7255,5661,51,52,102,70,99,69,50,71,20,17,78])).
% 106.56/106.64 cnf(7317,plain,
% 106.56/106.64 (P1(f72(a58,a62),a62)),
% 106.56/106.64 inference(scs_inference,[],[3,885,7274,5744,5742,6674,6689,7284,7255,566,5661,6981,2,14,51,52,102,70,99,69,50,71,20,17,78,47,76])).
% 106.56/106.64 cnf(7320,plain,
% 106.56/106.64 (~P2(a80,a10)),
% 106.56/106.64 inference(scs_inference,[],[3,885,7274,5744,5742,6674,6689,5507,7284,7255,5900,566,5661,6981,2,14,51,52,102,70,99,69,50,71,20,17,78,47,76,94])).
% 106.56/106.64 cnf(7323,plain,
% 106.56/106.64 (~P6(a69,a71,a81)),
% 106.56/106.64 inference(scs_inference,[],[3,885,7274,5744,5742,6674,6689,5507,7284,7255,5900,566,5661,6981,12,6,2,14,51,52,102,70,99,69,50,71,20,17,78,47,76,94,43])).
% 106.56/106.64 cnf(7328,plain,
% 106.56/106.64 (~P1(f7(a69,a71),a71)),
% 106.56/106.64 inference(scs_inference,[],[3,885,7274,5744,5742,6674,6689,5507,7284,7255,5900,2109,6397,566,5661,6981,12,6,2,14,51,52,102,70,99,69,50,71,20,17,78,47,76,94,43,91,42])).
% 106.56/106.64 cnf(7330,plain,
% 106.56/106.64 (P1(f7(a69,a71),a69)),
% 106.56/106.64 inference(scs_inference,[],[3,885,7274,5744,5742,6674,6689,5507,7284,7255,5900,2109,6397,566,5661,6981,12,6,2,14,51,52,102,70,99,69,50,71,20,17,78,47,76,94,43,91,42,26])).
% 106.56/106.64 cnf(7354,plain,
% 106.56/106.64 (P1(f7(a69,a71),f74(a71))),
% 106.56/106.64 inference(scs_inference,[],[1157,5262,5265,7207,7317,7328,52,51,102,70,69,99,50,71,20,17])).
% 106.56/106.64 cnf(7356,plain,
% 106.56/106.64 (P6(f74(a62),a62,a9)),
% 106.56/106.64 inference(scs_inference,[],[1157,5262,5265,7207,7310,7317,7328,52,51,102,70,69,99,50,71,20,17,40])).
% 106.56/106.64 cnf(7371,plain,
% 106.56/106.64 (P6(f48(a80,a73),f51(a80,a73),a73)),
% 106.56/106.64 inference(scs_inference,[],[7215,52,51])).
% 106.56/106.64 cnf(7373,plain,
% 106.56/106.64 (~P6(f49(a80,a8),f50(a80,a8),a8)),
% 106.56/106.64 inference(scs_inference,[],[1219,7215,52,51,102])).
% 106.56/106.64 cnf(7377,plain,
% 106.56/106.64 (P6(f45(a80,a73),f46(a80,a73),a73)),
% 106.56/106.64 inference(scs_inference,[],[1219,7215,7223,52,51,102,70,69])).
% 106.56/106.64 cnf(7383,plain,
% 106.56/106.64 (P6(f49(a80,a8),f50(a80,a8),a80)),
% 106.56/106.64 inference(scs_inference,[],[1219,7215,7223,7320,52,51,102,70,69,99,50,71])).
% 106.56/106.64 cnf(7385,plain,
% 106.56/106.64 (~P1(f7(a69,a71),f74(a69))),
% 106.56/106.64 inference(scs_inference,[],[1219,7215,7223,7320,7330,52,51,102,70,69,99,50,71,20])).
% 106.56/106.64 cnf(7400,plain,
% 106.56/106.64 (~P2(a80,a81)),
% 106.56/106.64 inference(scs_inference,[],[1219,7215,7223,7320,7323,7354,7330,6357,6195,5501,915,52,51,102,70,69,99,50,71,20,17,47,45,49,48,44,94])).
% 106.56/106.64 cnf(7428,plain,
% 106.56/106.64 (P6(f48(a84,a84),f51(a84,a84),a84)),
% 106.56/106.64 inference(scs_inference,[],[289,330,52,51])).
% 106.56/106.64 cnf(7450,plain,
% 106.56/106.64 (P3(a86,a8)),
% 106.56/106.64 inference(scs_inference,[],[1253,7400,7385,6430,6293,7312,289,292,330,617,7330,1813,52,51,102,70,69,99,50,71,20,17,47,45,100])).
% 106.56/106.64 cnf(7451,plain,
% 106.56/106.64 (P6(f48(a84,a84),x74511,a86)),
% 106.56/106.64 inference(rename_variables,[],[6293])).
% 106.56/106.64 cnf(7461,plain,
% 106.56/106.64 (~P2(a8,a89)),
% 106.56/106.64 inference(scs_inference,[],[1253,7400,7205,7385,6430,6293,7312,289,292,330,617,5963,7330,1813,52,51,102,70,69,99,50,71,20,17,47,45,100,49,48,44,46,94])).
% 106.56/106.64 cnf(7469,plain,
% 106.56/106.64 (~P5(a86,a8)),
% 106.56/106.64 inference(scs_inference,[],[1253,7400,7205,7385,7371,6430,6293,7451,7312,5403,289,292,330,617,5963,7330,1813,13,639,52,51,102,70,69,99,50,71,20,17,47,45,100,49,48,44,46,94,43,91,104])).
% 106.56/106.64 cnf(7503,plain,
% 106.56/106.64 (~P1(f14(a59,a71),a71)),
% 106.56/106.64 inference(scs_inference,[],[3,1258,7450,7461,7469,7377,7258,5161,1787,13,52,51,102,70,69,99,50,71,20,17,91,77])).
% 106.56/106.64 cnf(7509,plain,
% 106.56/106.64 (P1(f32(a2,a59),a2)),
% 106.56/106.64 inference(scs_inference,[],[3,1258,7450,7461,7469,7377,7258,5161,5163,5989,1787,13,52,51,102,70,69,99,50,71,20,17,91,77,79,41])).
% 106.56/106.64 cnf(7516,plain,
% 106.56/106.64 (~P2(a9,a90)),
% 106.56/106.64 inference(scs_inference,[],[3,1258,7450,7461,7469,5215,7377,7258,7356,5161,5163,5989,1787,6981,10,5,13,2,52,51,102,70,69,99,50,71,20,17,91,77,79,41,48,46,94])).
% 106.56/106.64 cnf(7549,plain,
% 106.56/106.64 (~P1(a61,f74(a62))),
% 106.56/106.64 inference(scs_inference,[],[4,1268,7516,481,1211,6674,6689,52,51,102,70,69,50,99,71,20])).
% 106.56/106.64 cnf(7556,plain,
% 106.56/106.64 (P1(f60(a65,a58),a65)),
% 106.56/106.64 inference(scs_inference,[],[4,1268,7516,7503,481,1211,6674,6689,5975,571,14,52,51,102,70,69,50,99,71,20,17,78,76])).
% 106.56/106.64 cnf(7563,plain,
% 106.56/106.64 (~P2(a80,a8)),
% 106.56/106.64 inference(scs_inference,[],[4,1268,7516,7383,7373,7503,481,1211,6674,6689,5975,571,7354,7385,648,14,52,51,102,70,69,50,99,71,20,17,78,76,48,33,94])).
% 106.56/106.64 cnf(7570,plain,
% 106.56/106.64 (P6(a62,f48(a84,a84),a73)),
% 106.56/106.64 inference(scs_inference,[],[4,1268,7516,7383,7373,7503,7509,481,1211,6674,6689,5975,571,7354,6981,7385,2,648,776,14,52,51,102,70,69,50,99,71,20,17,78,76,48,33,94,46,43,34])).
% 106.56/106.64 cnf(7604,plain,
% 106.56/106.64 (~P1(x76041,f46(a88,a88))),
% 106.56/106.64 inference(rename_variables,[],[915])).
% 106.56/106.64 cnf(7611,plain,
% 106.56/106.64 (~P2(a9,a81)),
% 106.56/106.64 inference(scs_inference,[],[4,1273,7563,5252,7549,7556,2964,2958,6993,7356,9,648,915,7604,8,52,102,69,99,50,71,20,17,44,48,33,46,94])).
% 106.56/106.64 cnf(7615,plain,
% 106.56/106.64 (P6(f48(a84,a84),a62,a73)),
% 106.56/106.64 inference(scs_inference,[],[4,1273,7563,5252,7549,7556,2964,2958,6993,7356,9,648,915,7604,8,52,102,69,99,50,71,20,17,44,48,33,46,94,43,34])).
% 106.56/106.64 cnf(7616,plain,
% 106.56/106.64 (P1(x76161,f48(a84,a84))),
% 106.56/106.64 inference(rename_variables,[],[648])).
% 106.56/106.64 cnf(7620,plain,
% 106.56/106.64 (P6(a62,a58,a9)),
% 106.56/106.64 inference(scs_inference,[],[4,334,1273,7563,5252,7549,7556,2964,2958,6993,7356,9,648,915,7604,8,579,52,102,69,99,50,71,20,17,44,48,33,46,94,43,34,109,40])).
% 106.56/106.64 cnf(7626,plain,
% 106.56/106.64 (P1(f38(a62,a58),a62)),
% 106.56/106.64 inference(scs_inference,[],[4,334,1273,7563,5252,7549,7556,2964,2958,6993,7356,9,648,7616,915,7604,8,579,52,102,69,99,50,71,20,17,44,48,33,46,94,43,34,109,40,45,65])).
% 106.56/106.64 cnf(7631,plain,
% 106.56/106.64 (P1(f38(a62,a58),a65)),
% 106.56/106.64 inference(scs_inference,[],[7626,15])).
% 106.56/106.64 cnf(7639,plain,
% 106.56/106.64 (~P1(f38(a62,a58),f74(a62))),
% 106.56/106.64 inference(scs_inference,[],[1278,7611,7626,15,102,50,99,20])).
% 106.56/106.64 cnf(7646,plain,
% 106.56/106.64 (~P6(a62,x76461,a85)),
% 106.56/106.64 inference(rename_variables,[],[5317])).
% 106.56/106.64 cnf(7649,plain,
% 106.56/106.64 (~P1(x76491,f48(a5,a5))),
% 106.56/106.64 inference(rename_variables,[],[639])).
% 106.56/106.64 cnf(7651,plain,
% 106.56/106.64 (P6(a3,a62,a8)),
% 106.56/106.64 inference(scs_inference,[],[4,1278,7611,7620,7626,5317,5347,639,8,15,102,50,99,20,71,17,91,48,33])).
% 106.56/106.64 cnf(7655,plain,
% 106.56/106.64 (~P2(a9,a85)),
% 106.56/106.64 inference(scs_inference,[],[4,1278,7611,7620,7626,5317,7646,7354,7385,5347,639,8,15,102,50,99,20,71,17,91,48,33,46,94])).
% 106.56/106.64 cnf(7664,plain,
% 106.56/106.64 (P1(f76(a62,a3),a62)),
% 106.56/106.64 inference(scs_inference,[],[4,1278,7611,7620,7626,5317,7646,7354,7385,5347,639,7649,8,15,102,50,99,20,71,17,91,48,33,46,94,43,34,54])).
% 106.56/106.64 cnf(7674,plain,
% 106.56/106.64 (P1(f76(a62,a3),a65)),
% 106.56/106.64 inference(scs_inference,[],[1297,7664,102,15])).
% 106.56/106.64 cnf(7687,plain,
% 106.56/106.64 (P6(f48(a84,a84),x76871,a86)),
% 106.56/106.64 inference(rename_variables,[],[6293])).
% 106.56/106.64 cnf(7689,plain,
% 106.56/106.64 (P6(a62,a3,a8)),
% 106.56/106.64 inference(scs_inference,[],[4,1297,7655,7428,7631,7664,6293,12,8,102,15,99,50,71,20,17,100,33])).
% 106.56/106.64 cnf(7694,plain,
% 106.56/106.64 (~P2(a73,a75)),
% 106.56/106.64 inference(scs_inference,[],[4,1297,7655,5495,7428,7570,7639,7631,7664,6293,12,648,8,102,15,99,50,71,20,17,100,33,46,94])).
% 106.56/106.64 cnf(7696,plain,
% 106.56/106.64 (P1(f77(a3,a62),a62)),
% 106.56/106.64 inference(scs_inference,[],[4,1297,7651,7655,5495,7428,7570,7639,7631,7664,6293,12,648,8,102,15,99,50,71,20,17,100,33,46,94,80])).
% 106.56/106.64 cnf(7701,plain,
% 106.56/106.64 (P6(a3,a62,a73)),
% 106.56/106.64 inference(scs_inference,[],[4,1297,7651,7655,5495,7428,7570,7639,7631,7664,6293,12,648,14,8,102,15,99,50,71,20,17,100,33,46,94,80,43,34])).
% 106.56/106.64 cnf(7702,plain,
% 106.56/106.64 (P1(x77021,a3)),
% 106.56/106.64 inference(rename_variables,[],[8])).
% 106.56/106.64 cnf(7706,plain,
% 106.56/106.64 (P1(f7(a62,a58),a62)),
% 106.56/106.64 inference(scs_inference,[],[4,1297,7651,7655,5495,7428,7570,7639,7631,7664,6293,12,648,14,8,102,15,99,50,71,20,17,100,33,46,94,80,43,34,70,26])).
% 106.56/106.64 cnf(7723,plain,
% 106.56/106.64 (~P1(f14(a62,a65),a65)),
% 106.56/106.64 inference(scs_inference,[],[4,1297,7651,7655,5495,7428,7570,7639,7631,7664,6293,7687,7157,5321,5623,12,648,14,8,7702,102,15,99,50,71,20,17,100,33,46,94,80,43,34,70,26,69,53,81,104,107,52,51,77])).
% 106.56/106.64 cnf(7758,plain,
% 106.56/106.64 (~P2(a8,a10)),
% 106.56/106.64 inference(scs_inference,[],[4,1305,7689,7694,7701,7674,7706,7723,1645,13,639,579,102,15,99,50,71,20,17,91,33,46,94])).
% 106.56/106.64 cnf(7769,plain,
% 106.56/106.64 (P1(f60(a62,a58),a62)),
% 106.56/106.64 inference(scs_inference,[],[4,1305,7689,7694,7701,7674,7706,7723,1645,6181,563,13,776,639,14,579,102,15,99,50,71,20,17,91,33,46,94,43,34,78,76])).
% 106.56/106.64 cnf(7790,plain,
% 106.56/106.64 ($false),
% 106.56/106.64 inference(scs_inference,[],[1310,7758,7615,7769,6622,7696,13,11,102,15,99,50,71,20,17,91]),
% 106.56/106.64 ['proof']).
% 106.56/106.65 % SZS output end Proof
% 106.56/106.65 % Total time :105.880000s
%------------------------------------------------------------------------------