%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : KRS216+1 : TPTP v8.2.0. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n004.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:54 EDT 2024
% Result : Theorem 117.33s 118.09s
% Output : CNFRefutation 117.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : KRS216+1 : TPTP v8.2.0. Bugfixed v5.4.0.
% 0.10/0.11 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.10/0.33 % Computer : n004.cluster.edu
% 0.10/0.33 % Model : x86_64 x86_64
% 0.10/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.33 % Memory : 8042.1875MB
% 0.10/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.33 % CPULimit : 300
% 0.10/0.33 % WCLimit : 300
% 0.10/0.33 % DateTime : Wed Jun 19 14:27:24 EDT 2024
% 0.10/0.33 % CPUTime :
% 0.18/0.56 start to proof:theBenchmark
% 117.33/118.08 %-------------------------------------------
% 117.33/118.08 % File :CSE---1.7
% 117.33/118.08 % Problem :theBenchmark
% 117.33/118.08 % Transform :cnf
% 117.33/118.08 % Format :tptp:raw
% 117.33/118.08 % Command :java -jar mcs_scs.jar %d %s
% 117.33/118.08
% 117.33/118.08 % Result :Theorem 116.770000s
% 117.33/118.08 % Output :CNFRefutation 116.770000s
% 117.33/118.09 %-------------------------------------------
% 117.33/118.09 %------------------------------------------------------------------------------
% 117.33/118.09 % File : KRS216+1 : TPTP v8.2.0. Bugfixed v5.4.0.
% 117.33/118.09 % Domain : Knowledge Representation
% 117.33/118.09 % Problem : UNS nota THM
% 117.33/118.09 % Version : [Sut08] axioms.
% 117.33/118.09 % English :
% 117.33/118.09
% 117.33/118.09 % Refs : [Sut08] Sutcliffe (2008), The SZS Ontologies for Automated Rea
% 117.33/118.09 % Source : [TPTP]
% 117.33/118.09 % Names :
% 117.33/118.09
% 117.33/118.09 % Status : Theorem
% 117.33/118.09 % Rating : 0.38 v8.2.0, 0.40 v8.1.0, 0.29 v7.5.0, 0.33 v7.4.0, 0.25 v7.3.0, 0.43 v7.2.0, 0.33 v7.1.0, 0.25 v7.0.0, 0.14 v6.3.0, 0.31 v6.2.0, 0.36 v6.1.0, 0.48 v6.0.0, 0.50 v5.4.0
% 117.33/118.09 % Syntax : Number of formulae : 33 ( 3 unt; 0 def)
% 117.33/118.09 % Number of atoms : 107 ( 0 equ)
% 117.33/118.09 % Maximal formula atoms : 7 ( 3 avg)
% 117.33/118.09 % Number of connectives : 96 ( 22 ~; 1 |; 35 &)
% 117.33/118.09 % ( 28 <=>; 8 =>; 0 <=; 2 <~>)
% 117.33/118.09 % Maximal formula depth : 10 ( 6 avg)
% 117.33/118.09 % Maximal term depth : 2 ( 1 avg)
% 117.33/118.09 % Number of predicates : 7 ( 7 usr; 0 prp; 2-3 aty)
% 117.33/118.09 % Number of functors : 20 ( 20 usr; 19 con; 0-1 aty)
% 117.33/118.09 % Number of variables : 122 ( 72 !; 50 ?)
% 117.33/118.09 % SPC : FOF_THM_RFO_NEQ
% 117.33/118.09
% 117.33/118.09 % Comments :
% 117.33/118.09 % Bugfixes : v5.4.0 - Added missing axiom in KRS001+1.ax
% 117.33/118.09 %------------------------------------------------------------------------------
% 117.33/118.09 %----Include SZS success ontology nodes
% 117.33/118.09 include('Axioms/KRS001+0.ax').
% 117.33/118.09 %----Include SZS success ontology node relationships
% 117.33/118.09 include('Axioms/KRS001+1.ax').
% 117.33/118.09 %------------------------------------------------------------------------------
% 117.33/118.09 fof(nota_uns_thm,conjecture,
% 117.33/118.09 nota(uns,thm) ).
% 117.33/118.09
% 117.33/118.09 %------------------------------------------------------------------------------
% 117.33/118.09 %-------------------------------------------
% 117.33/118.09 % Proof found
% 117.33/118.09 % SZS status Theorem for theBenchmark
% 117.33/118.09 % SZS output start Proof
% 117.33/118.10 %ClaNum:109(EqnAxiom:0)
% 117.33/118.10 %VarNum:590(SingletonVarNum:249)
% 117.33/118.10 %MaxLitNum:6
% 117.33/118.10 %MaxfuncDepth:1
% 117.33/118.10 %SharedTerms:52
% 117.33/118.10 %goalClause: 13
% 117.33/118.10 %singleGoalClaCount:1
% 117.33/118.10 [1]P1(a1,a2)
% 117.33/118.10 [2]P1(a55,a56)
% 117.33/118.10 [3]P1(a55,a59)
% 117.33/118.10 [4]P1(a61,a62)
% 117.33/118.10 [5]P1(a66,a65)
% 117.33/118.10 [6]P1(a67,a69)
% 117.33/118.10 [7]P1(a70,a71)
% 117.33/118.10 [9]~P1(a57,a2)
% 117.33/118.10 [10]~P1(a66,a62)
% 117.33/118.10 [11]~P1(a68,a65)
% 117.33/118.10 [12]~P1(a67,a71)
% 117.33/118.10 [13]~P4(a73,a74)
% 117.33/118.10 [8]P1(x81,a3)
% 117.33/118.10 [14]~P1(x141,a58)
% 117.33/118.10 [18]~P1(a63,a56)+~P1(a64,a59)
% 117.33/118.10 [15]~P1(x151,a62)+P1(x151,a65)
% 117.33/118.10 [17]P1(x171,x172)+P1(x171,f75(x172))
% 117.33/118.10 [20]~P1(x201,x202)+~P1(x201,f75(x202))
% 117.33/118.10 [21]P6(x211,x212,a5)+P1(f4(x211),x211)
% 117.33/118.10 [24]P6(x241,x242,a87)+P1(f6(x241,x242),x242)
% 117.33/118.10 [25]P6(x251,x252,a81)+P1(f31(x251,x252),x251)
% 117.33/118.10 [26]P6(x261,x262,a74)+P1(f7(x261,x262),x261)
% 117.33/118.10 [42]P6(x421,x422,a74)+~P1(f7(x421,x422),x422)
% 117.33/118.10 [50]P2(x501,x502)+P6(f41(x501,x502),f47(x501,x502),x501)
% 117.33/118.10 [51]P5(x511,x512)+P6(f48(x511,x512),f51(x511,x512),x512)
% 117.33/118.10 [52]P5(x521,x522)+P6(f48(x521,x522),f51(x521,x522),x521)
% 117.33/118.10 [53]~P6(x531,x532,a83)+P1(f77(x531,x532),x532)
% 117.33/118.10 [54]~P6(x541,x542,a83)+P1(f77(x541,x542),x541)
% 117.33/118.10 [55]~P6(x551,x552,a10)+P1(f11(x551,x552),x551)
% 117.33/118.10 [56]~P6(x561,x562,a82)+P1(f13(x561,x562),x561)
% 117.33/118.10 [57]~P6(x571,x572,a90)+P1(f15(x571,x572),x571)
% 117.33/118.10 [58]~P6(x581,x582,a90)+P1(f17(x581,x582),x582)
% 117.33/118.10 [59]~P6(x591,x592,a76)+P1(f18(x591,x592),x591)
% 117.33/118.10 [60]~P6(x601,x602,a88)+P1(f20(x601,x602),x601)
% 117.33/118.10 [61]~P6(x611,x612,a91)+P1(f25(x611,x612),x611)
% 117.33/118.10 [62]~P6(x621,x622,a91)+P1(f28(x621,x622),x622)
% 117.33/118.10 [63]~P6(x631,x632,a84)+P1(f33(x631,x632),x632)
% 117.33/118.10 [64]~P6(x641,x642,a89)+P1(f34(x641,x642),x642)
% 117.33/118.10 [65]~P6(x651,x652,a9)+P1(f38(x651,x652),x651)
% 117.33/118.10 [66]~P6(x661,x662,a80)+P1(f42(x661,x662),x662)
% 117.33/118.10 [67]~P6(x671,x672,a80)+P1(f42(x671,x672),x671)
% 117.33/118.10 [68]~P6(x681,x682,a80)+P1(f44(x681,x682),x681)
% 117.33/118.10 [69]~P3(x691,x692)+P6(f45(x691,x692),f46(x691,x692),x692)
% 117.33/118.10 [70]~P3(x701,x702)+P6(f45(x701,x702),f46(x701,x702),x701)
% 117.33/118.10 [71]~P4(x711,x712)+P6(f49(x711,x712),f50(x711,x712),x711)
% 117.33/118.10 [72]~P6(x721,x722,a9)+P1(f38(x721,x722),f75(x722))
% 117.33/118.10 [73]~P6(x731,x732,a80)+P1(f44(x731,x732),f75(x732))
% 117.33/118.10 [82]~P6(x821,x822,a90)+~P1(f17(x821,x822),x821)
% 117.33/118.10 [83]~P6(x831,x832,a76)+~P1(f21(x831,x832),x831)
% 117.33/118.10 [84]~P6(x841,x842,a88)+~P1(f26(x841,x842),x841)
% 117.33/118.10 [85]~P6(x851,x852,a91)+~P1(f28(x851,x852),x851)
% 117.33/118.10 [86]~P6(x861,x862,a91)+~P1(f30(x861,x862),x862)
% 117.33/118.10 [87]~P6(x871,x872,a89)+~P1(f39(x871,x872),x872)
% 117.33/118.10 [99]P2(x991,x992)+~P6(f41(x991,x992),f47(x991,x992),x992)
% 117.33/118.10 [102]~P4(x1021,x1022)+~P6(f49(x1021,x1022),f50(x1021,x1022),x1022)
% 117.33/118.10 [22]~P1(x223,x222)+P6(x221,x222,a81)
% 117.33/118.10 [23]~P1(x233,x231)+P6(x231,x232,a87)
% 117.33/118.10 [27]P1(x271,x272)+~P6(x273,x272,a82)
% 117.33/118.10 [28]P1(x281,x282)+~P6(x283,x282,a85)
% 117.33/118.10 [29]P1(x291,x292)+~P6(x293,x292,a88)
% 117.33/118.10 [30]P1(x301,x302)+~P6(x303,x302,a86)
% 117.33/118.10 [31]P1(x311,x312)+~P6(x312,x313,a85)
% 117.33/118.10 [32]P1(x321,x322)+~P6(x322,x323,a73)
% 117.33/118.10 [36]~P1(x361,x362)+~P6(x362,x363,a5)
% 117.33/118.10 [37]~P1(x371,x372)+~P6(x372,x373,a84)
% 117.33/118.10 [38]~P1(x381,x382)+~P6(x382,x383,a86)
% 117.33/118.10 [39]~P1(x391,x392)+~P6(x392,x393,a89)
% 117.33/118.10 [35]~P6(x353,x352,a73)+P1(x351,f75(x352))
% 117.33/118.10 [76]P6(x761,x762,a8)+P1(f60(x761,x762),x761)+P1(f72(x761,x762),x762)
% 117.33/118.10 [93]P6(x931,x932,a86)+P1(f36(x931,x932),x931)+~P1(f37(x931,x932),x932)
% 117.33/118.10 [98]P6(x981,x982,a85)+~P1(f23(x981,x982),x981)+~P1(f24(x981,x982),x982)
% 117.33/118.10 [101]P6(x1011,x1012,a73)+~P1(f40(x1011,x1012),x1011)+~P1(f43(x1011,x1012),f75(x1012))
% 117.33/118.10 [108]P7(x1081,x1082)+P6(f53(x1081,x1082),f54(x1081,x1082),x1082)+~P6(f53(x1081,x1082),f54(x1081,x1082),x1081)
% 117.33/118.10 [109]P7(x1091,x1092)+P6(f53(x1091,x1092),f54(x1091,x1092),x1091)+~P6(f53(x1091,x1092),f54(x1091,x1092),x1092)
% 117.33/118.10 [34]~P1(x343,x341)+~P1(x343,x342)+P6(x341,x342,a83)
% 117.33/118.10 [43]P1(x431,x432)+~P1(x431,x433)+~P6(x433,x432,a74)
% 117.33/118.10 [44]P1(x441,x442)+~P1(x441,x443)+~P6(x442,x443,a10)
% 117.33/118.10 [45]P1(x451,x452)+~P1(x451,x453)+~P6(x452,x453,a76)
% 117.33/118.10 [46]P1(x461,x462)+~P1(x461,x463)+~P6(x463,x462,a10)
% 117.33/118.10 [47]P1(x471,x472)+~P1(x471,x473)+~P6(x473,x472,a90)
% 117.33/118.10 [48]P1(x481,x482)+~P1(x481,x483)+~P6(x483,x482,a76)
% 117.33/118.10 [49]P1(x491,x492)+~P1(x491,x493)+~P6(x493,x492,a91)
% 117.33/118.10 [40]~P1(x403,x401)+P6(x401,x402,a9)+~P1(x403,f75(x402))
% 117.33/118.10 [41]~P1(x413,x412)+P6(x411,x412,a84)+P1(f32(x411,x412),x411)
% 117.33/118.10 [77]~P1(x773,x771)+P6(x771,x772,a82)+~P1(f14(x771,x772),x772)
% 117.33/118.10 [78]~P1(x783,x782)+~P6(x781,x782,a87)+P1(f29(x781,x782),x781)
% 117.33/118.10 [79]~P1(x793,x791)+~P6(x791,x792,a81)+P1(f52(x791,x792),x792)
% 117.33/118.10 [80]~P1(x803,x801)+~P6(x801,x802,a8)+P1(f78(x801,x802),x802)
% 117.33/118.10 [81]~P1(x813,x812)+~P6(x811,x812,a8)+P1(f79(x811,x812),x811)
% 117.33/118.10 [33]~P1(x333,x332)+~P1(x334,x331)+P6(x331,x332,a8)
% 117.33/118.10 [75]~P7(x754,x753)+P6(x751,x752,x753)+P6(x751,x752,x754)
% 117.33/118.10 [91]~P6(x913,x914,x911)+P4(x911,x912)+P6(x913,x914,x912)
% 117.33/118.10 [94]~P6(x941,x942,x944)+P6(x941,x942,x943)+~P2(x944,x943)
% 117.33/118.10 [100]~P6(x1003,x1004,x1001)+P3(x1001,x1002)+~P6(x1003,x1004,x1002)
% 117.33/118.10 [104]~P6(x1043,x1044,x1041)+~P5(x1041,x1042)+~P6(x1043,x1044,x1042)
% 117.33/118.10 [105]~P6(x1053,x1054,x1051)+~P7(x1051,x1052)+~P6(x1053,x1054,x1052)
% 117.33/118.10 [92]~P1(x923,x921)+P6(x921,x922,a10)+P1(f12(x921,x922),x922)+P1(f12(x921,x922),x921)
% 117.33/118.10 [106]~P1(x1063,x1061)+P6(x1061,x1062,a10)+~P1(f12(x1061,x1062),x1062)+~P1(f12(x1061,x1062),x1061)
% 117.33/118.10 [74]P1(x741,x742)+~P1(x744,x742)+P6(x743,x742,a89)+P1(f35(x743,x742),x743)
% 117.33/118.10 [90]P1(x901,x902)+~P1(x904,x902)+P6(x902,x903,a88)+~P1(f22(x902,x903),x903)
% 117.33/118.10 [88]~P1(x881,x883)+P1(x881,x882)+~P1(x884,x882)+P6(x882,x883,a90)+P1(f16(x882,x883),x882)
% 117.33/118.10 [89]~P1(x894,x891)+~P1(x893,x891)+~P1(x894,x892)+P6(x891,x892,a80)+~P1(x893,f75(x892))
% 117.33/118.10 [96]P1(x961,x962)+~P1(x964,x962)+P6(x962,x963,a76)+P1(f19(x962,x963),x963)+P1(f19(x962,x963),x962)
% 117.33/118.10 [97]~P1(x971,x973)+P1(x971,x972)+~P1(x974,x972)+P6(x972,x973,a90)+~P1(f16(x972,x973),x973)
% 117.33/118.10 [107]P1(x1071,x1072)+~P1(x1074,x1072)+P6(x1072,x1073,a76)+~P1(f19(x1072,x1073),x1073)+~P1(f19(x1072,x1073),x1072)
% 117.33/118.10 [95]~P1(x953,x952)+P1(x951,x952)+P1(x953,x954)+~P1(x955,x954)+P6(x954,x952,a91)+P1(f27(x954,x952),x954)
% 117.33/118.10 [103]~P1(x1033,x1032)+P1(x1031,x1032)+P1(x1033,x1034)+~P1(x1035,x1034)+P6(x1034,x1032,a91)+~P1(f27(x1034,x1032),x1032)
% 117.33/118.10 %EqnAxiom
% 117.33/118.10
% 117.33/118.10 %-------------------------------------------
% 117.33/118.11 cnf(110,plain,
% 117.33/118.11 (P6(a58,x1101,a5)),
% 117.33/118.11 inference(scs_inference,[],[14,21])).
% 117.33/118.11 cnf(111,plain,
% 117.33/118.11 (~P1(x1111,a58)),
% 117.33/118.11 inference(rename_variables,[],[14])).
% 117.33/118.11 cnf(113,plain,
% 117.33/118.11 (P6(x1131,a58,a87)),
% 117.33/118.11 inference(scs_inference,[],[14,111,21,24])).
% 117.33/118.11 cnf(114,plain,
% 117.33/118.11 (~P1(x1141,a58)),
% 117.33/118.11 inference(rename_variables,[],[14])).
% 117.33/118.11 cnf(116,plain,
% 117.33/118.11 (P6(a58,x1161,a81)),
% 117.33/118.11 inference(scs_inference,[],[14,111,114,21,24,25])).
% 117.33/118.12 cnf(117,plain,
% 117.33/118.12 (~P1(x1171,a58)),
% 117.33/118.12 inference(rename_variables,[],[14])).
% 117.33/118.12 cnf(119,plain,
% 117.33/118.12 (P6(a58,x1191,a74)),
% 117.33/118.12 inference(scs_inference,[],[14,111,114,117,21,24,25,26])).
% 117.33/118.12 cnf(120,plain,
% 117.33/118.12 (~P1(x1201,a58)),
% 117.33/118.12 inference(rename_variables,[],[14])).
% 117.33/118.12 cnf(122,plain,
% 117.33/118.12 (P6(x1221,a3,a74)),
% 117.33/118.12 inference(scs_inference,[],[8,14,111,114,117,21,24,25,26,42])).
% 117.33/118.12 cnf(123,plain,
% 117.33/118.12 (P1(x1231,a3)),
% 117.33/118.12 inference(rename_variables,[],[8])).
% 117.33/118.12 cnf(125,plain,
% 117.33/118.12 (~P1(a68,a62)),
% 117.33/118.12 inference(scs_inference,[],[8,14,111,114,117,11,21,24,25,26,42,15])).
% 117.33/118.12 cnf(127,plain,
% 117.33/118.12 (~P6(x1271,a58,a83)),
% 117.33/118.12 inference(scs_inference,[],[8,14,111,114,117,120,11,21,24,25,26,42,15,53])).
% 117.33/118.12 cnf(128,plain,
% 117.33/118.12 (~P1(x1281,a58)),
% 117.33/118.12 inference(rename_variables,[],[14])).
% 117.33/118.12 cnf(130,plain,
% 117.33/118.12 (~P6(a58,x1301,a83)),
% 117.33/118.12 inference(scs_inference,[],[8,14,111,114,117,120,128,11,21,24,25,26,42,15,53,54])).
% 117.33/118.12 cnf(131,plain,
% 117.33/118.12 (~P1(x1311,a58)),
% 117.33/118.12 inference(rename_variables,[],[14])).
% 117.33/118.12 cnf(133,plain,
% 117.33/118.12 (~P6(a58,x1331,a10)),
% 117.33/118.12 inference(scs_inference,[],[8,14,111,114,117,120,128,131,11,21,24,25,26,42,15,53,54,55])).
% 117.33/118.12 cnf(134,plain,
% 117.33/118.12 (~P1(x1341,a58)),
% 117.33/118.12 inference(rename_variables,[],[14])).
% 117.33/118.12 cnf(136,plain,
% 117.33/118.12 (~P6(a58,x1361,a82)),
% 117.33/118.12 inference(scs_inference,[],[8,14,111,114,117,120,128,131,134,11,21,24,25,26,42,15,53,54,55,56])).
% 117.33/118.12 cnf(137,plain,
% 117.33/118.12 (~P1(x1371,a58)),
% 117.33/118.12 inference(rename_variables,[],[14])).
% 117.33/118.12 cnf(140,plain,
% 117.33/118.12 (~P1(x1401,a58)),
% 117.33/118.12 inference(rename_variables,[],[14])).
% 117.33/118.12 cnf(142,plain,
% 117.33/118.12 (~P6(x1421,a58,a90)),
% 117.33/118.12 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])).
% 117.33/118.12 cnf(143,plain,
% 117.33/118.12 (~P1(x1431,a58)),
% 117.33/118.12 inference(rename_variables,[],[14])).
% 117.33/118.12 cnf(145,plain,
% 117.33/118.12 (~P6(a58,x1451,a76)),
% 117.33/118.12 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])).
% 117.33/118.12 cnf(146,plain,
% 117.33/118.12 (~P1(x1461,a58)),
% 117.33/118.12 inference(rename_variables,[],[14])).
% 117.33/118.12 cnf(148,plain,
% 117.33/118.12 (~P6(a58,x1481,a88)),
% 117.33/118.12 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])).
% 117.33/118.12 cnf(149,plain,
% 117.33/118.12 (~P1(x1491,a58)),
% 117.33/118.12 inference(rename_variables,[],[14])).
% 117.33/118.12 cnf(152,plain,
% 117.33/118.12 (~P1(x1521,a58)),
% 117.33/118.12 inference(rename_variables,[],[14])).
% 117.33/118.12 cnf(154,plain,
% 117.33/118.12 (~P6(x1541,a58,a91)),
% 117.33/118.12 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])).
% 117.33/118.12 cnf(155,plain,
% 117.33/118.12 (~P1(x1551,a58)),
% 117.33/118.12 inference(rename_variables,[],[14])).
% 117.33/118.12 cnf(157,plain,
% 117.33/118.12 (~P6(x1571,a58,a84)),
% 117.33/118.12 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])).
% 117.33/118.12 cnf(158,plain,
% 117.33/118.12 (~P1(x1581,a58)),
% 117.33/118.12 inference(rename_variables,[],[14])).
% 117.33/118.12 cnf(160,plain,
% 117.33/118.12 (~P6(x1601,a58,a89)),
% 117.33/118.12 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])).
% 117.33/118.12 cnf(161,plain,
% 117.33/118.12 (~P1(x1611,a58)),
% 117.33/118.12 inference(rename_variables,[],[14])).
% 117.33/118.12 cnf(163,plain,
% 117.33/118.12 (~P6(a58,x1631,a9)),
% 117.33/118.12 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])).
% 117.33/118.12 cnf(164,plain,
% 117.33/118.12 (~P1(x1641,a58)),
% 117.33/118.12 inference(rename_variables,[],[14])).
% 117.33/118.12 cnf(166,plain,
% 117.33/118.12 (~P6(x1661,a58,a80)),
% 117.33/118.12 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])).
% 117.33/118.12 cnf(167,plain,
% 117.33/118.12 (~P1(x1671,a58)),
% 117.33/118.12 inference(rename_variables,[],[14])).
% 117.33/118.12 cnf(170,plain,
% 117.33/118.12 (~P1(x1701,a58)),
% 117.33/118.12 inference(rename_variables,[],[14])).
% 117.33/118.12 cnf(172,plain,
% 117.33/118.12 (~P6(a3,x1721,a90)),
% 117.33/118.12 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])).
% 117.33/118.12 cnf(173,plain,
% 117.33/118.12 (P1(x1731,a3)),
% 117.33/118.12 inference(rename_variables,[],[8])).
% 117.33/118.12 cnf(175,plain,
% 117.33/118.12 (~P6(a3,x1751,a76)),
% 117.33/118.12 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])).
% 117.33/118.12 cnf(176,plain,
% 117.33/118.12 (P1(x1761,a3)),
% 117.33/118.12 inference(rename_variables,[],[8])).
% 117.33/118.12 cnf(178,plain,
% 117.33/118.12 (~P6(a3,x1781,a88)),
% 117.33/118.12 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])).
% 117.33/118.12 cnf(179,plain,
% 117.33/118.12 (P1(x1791,a3)),
% 117.33/118.12 inference(rename_variables,[],[8])).
% 117.33/118.12 cnf(181,plain,
% 117.33/118.12 (~P6(a3,x1811,a91)),
% 117.33/118.12 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])).
% 117.33/118.12 cnf(182,plain,
% 117.33/118.12 (P1(x1821,a3)),
% 117.33/118.12 inference(rename_variables,[],[8])).
% 117.33/118.12 cnf(185,plain,
% 117.33/118.12 (P1(x1851,a3)),
% 117.33/118.12 inference(rename_variables,[],[8])).
% 117.33/118.12 cnf(188,plain,
% 117.33/118.12 (P1(x1881,a3)),
% 117.33/118.12 inference(rename_variables,[],[8])).
% 117.33/118.12 cnf(190,plain,
% 117.33/118.12 (P4(a5,a83)),
% 117.33/118.12 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])).
% 117.33/118.12 cnf(194,plain,
% 117.33/118.12 (P6(a58,a3,a86)),
% 117.33/118.12 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])).
% 117.33/118.12 cnf(195,plain,
% 117.33/118.12 (~P1(x1951,a58)),
% 117.33/118.12 inference(rename_variables,[],[14])).
% 117.33/118.12 cnf(196,plain,
% 117.33/118.12 (P1(x1961,a3)),
% 117.33/118.12 inference(rename_variables,[],[8])).
% 117.33/118.12 cnf(198,plain,
% 117.33/118.12 (~P6(a3,a58,a8)),
% 117.33/118.12 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])).
% 117.33/118.12 cnf(199,plain,
% 117.33/118.12 (~P1(x1991,a58)),
% 117.33/118.12 inference(rename_variables,[],[14])).
% 117.33/118.12 cnf(201,plain,
% 117.33/118.12 (~P6(a58,a3,a8)),
% 117.33/118.12 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])).
% 117.33/118.12 cnf(202,plain,
% 117.33/118.12 (~P1(x2021,a58)),
% 117.33/118.12 inference(rename_variables,[],[14])).
% 117.33/118.12 cnf(210,plain,
% 117.33/118.12 (P6(a3,a3,a10)),
% 117.33/118.12 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])).
% 117.33/118.12 cnf(211,plain,
% 117.33/118.12 (P1(x2111,a3)),
% 117.33/118.12 inference(rename_variables,[],[8])).
% 117.33/118.12 cnf(212,plain,
% 117.33/118.12 (P1(x2121,a3)),
% 117.33/118.12 inference(rename_variables,[],[8])).
% 117.33/118.12 cnf(214,plain,
% 117.33/118.12 (P6(a3,a3,a85)),
% 117.33/118.12 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])).
% 117.33/118.12 cnf(215,plain,
% 117.33/118.12 (P1(x2151,a3)),
% 117.33/118.12 inference(rename_variables,[],[8])).
% 117.33/118.12 cnf(218,plain,
% 117.33/118.12 (P6(a3,x2181,a73)+~P1(f43(a3,x2181),f75(x2181))),
% 117.33/118.12 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])).
% 117.33/118.12 cnf(222,plain,
% 117.33/118.12 (~P6(x2221,a58,a73)+P6(a3,a58,a73)),
% 117.33/118.12 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])).
% 117.33/118.12 cnf(230,plain,
% 117.33/118.12 (P6(x2301,a58,a87)),
% 117.33/118.12 inference(rename_variables,[],[113])).
% 117.33/118.12 cnf(231,plain,
% 117.33/118.12 (P6(a58,x2311,a5)),
% 117.33/118.12 inference(rename_variables,[],[110])).
% 117.33/118.12 cnf(234,plain,
% 117.33/118.12 (~P1(x2341,a58)),
% 117.33/118.12 inference(rename_variables,[],[14])).
% 117.33/118.12 cnf(236,plain,
% 117.33/118.12 (~P5(a5,a87)),
% 117.33/118.12 inference(scs_inference,[],[110,231,113,230,1,14,105,80,104])).
% 117.33/118.12 cnf(237,plain,
% 117.33/118.12 (P6(x2371,a58,a87)),
% 117.33/118.12 inference(rename_variables,[],[113])).
% 117.33/118.12 cnf(238,plain,
% 117.33/118.12 (P6(a58,x2381,a5)),
% 117.33/118.12 inference(rename_variables,[],[110])).
% 117.33/118.12 cnf(240,plain,
% 117.33/118.12 (P3(a5,a87)),
% 117.33/118.12 inference(scs_inference,[],[110,231,238,113,230,237,1,14,105,80,104,100])).
% 117.33/118.12 cnf(242,plain,
% 117.33/118.12 (P6(a58,x2421,a5)),
% 117.33/118.12 inference(rename_variables,[],[110])).
% 117.33/118.12 cnf(244,plain,
% 117.33/118.12 (P4(a5,a10)),
% 117.33/118.12 inference(scs_inference,[],[110,231,238,242,113,230,237,133,1,14,105,80,104,100,91])).
% 117.33/118.12 cnf(245,plain,
% 117.33/118.12 (~P6(a58,x2451,a10)),
% 117.33/118.12 inference(rename_variables,[],[133])).
% 117.33/118.12 cnf(247,plain,
% 117.33/118.12 (~P6(a58,a2,a8)),
% 117.33/118.12 inference(scs_inference,[],[110,231,238,242,113,230,237,133,1,14,234,105,80,104,100,91,81])).
% 117.33/118.12 cnf(254,plain,
% 117.33/118.12 (P6(a3,x2541,a85)+~P1(f24(a3,x2541),x2541)),
% 117.33/118.12 inference(scs_inference,[],[110,231,238,242,113,230,237,127,133,245,1,8,14,234,105,80,104,100,91,81,75,98])).
% 117.33/118.12 cnf(278,plain,
% 117.33/118.12 (~P5(a86,a86)),
% 117.33/118.12 inference(scs_inference,[],[194,104])).
% 117.33/118.12 cnf(280,plain,
% 117.33/118.12 (P4(a87,a8)),
% 117.33/118.12 inference(scs_inference,[],[194,113,198,104,91])).
% 117.33/118.12 cnf(285,plain,
% 117.33/118.12 (P3(a86,a86)),
% 117.33/118.12 inference(scs_inference,[],[194,113,198,104,91,105,100])).
% 117.33/118.12 cnf(289,plain,
% 117.33/118.12 (~P6(a56,a58,a8)),
% 117.33/118.12 inference(scs_inference,[],[194,113,198,2,14,104,91,105,100,75,80])).
% 117.33/118.12 cnf(290,plain,
% 117.33/118.12 (~P1(x2901,a58)),
% 117.33/118.12 inference(rename_variables,[],[14])).
% 117.33/118.12 cnf(292,plain,
% 117.33/118.12 (~P6(a58,a56,a8)),
% 117.33/118.12 inference(scs_inference,[],[194,113,198,2,14,290,104,91,105,100,75,80,81])).
% 117.33/118.12 cnf(296,plain,
% 117.33/118.12 (P6(a58,x2961,a81)),
% 117.33/118.12 inference(rename_variables,[],[116])).
% 117.33/118.12 cnf(301,plain,
% 117.33/118.12 (P3(a5,a81)),
% 117.33/118.12 inference(scs_inference,[],[110,116,296,130,136,105,75,100])).
% 117.33/118.12 cnf(302,plain,
% 117.33/118.12 (P6(a58,x3021,a81)),
% 117.33/118.12 inference(rename_variables,[],[116])).
% 117.33/118.12 cnf(304,plain,
% 117.33/118.12 (~P5(a5,a81)),
% 117.33/118.12 inference(scs_inference,[],[110,116,296,302,130,136,105,75,100,104])).
% 117.33/118.12 cnf(307,plain,
% 117.33/118.12 (P4(a5,a8)),
% 117.33/118.12 inference(scs_inference,[],[110,116,296,302,130,201,136,105,75,100,104,91])).
% 117.33/118.12 cnf(310,plain,
% 117.33/118.12 (P3(a5,a74)),
% 117.33/118.12 inference(scs_inference,[],[110,119,100])).
% 117.33/118.12 cnf(311,plain,
% 117.33/118.12 (P6(a58,x3111,a74)),
% 117.33/118.12 inference(rename_variables,[],[119])).
% 117.33/118.12 cnf(313,plain,
% 117.33/118.12 (P4(a5,a90)),
% 117.33/118.12 inference(scs_inference,[],[110,119,142,100,91])).
% 117.33/118.13 cnf(315,plain,
% 117.33/118.13 (P6(a58,x3151,a5)),
% 117.33/118.13 inference(rename_variables,[],[110])).
% 117.33/118.13 cnf(317,plain,
% 117.33/118.13 (~P5(a5,a74)),
% 117.33/118.13 inference(scs_inference,[],[110,315,119,311,142,100,91,104])).
% 117.33/118.13 cnf(318,plain,
% 117.33/118.13 (P6(a58,x3181,a74)),
% 117.33/118.13 inference(rename_variables,[],[119])).
% 117.33/118.13 cnf(320,plain,
% 117.33/118.13 (~P7(a5,a74)),
% 117.33/118.13 inference(scs_inference,[],[110,315,119,311,318,142,100,91,104,105])).
% 117.33/118.13 cnf(326,plain,
% 117.33/118.13 (~P5(a85,a85)),
% 117.33/118.13 inference(scs_inference,[],[214,104])).
% 117.33/118.13 cnf(329,plain,
% 117.33/118.13 (~P6(a58,x3291,a88)),
% 117.33/118.13 inference(rename_variables,[],[148])).
% 117.33/118.13 cnf(333,plain,
% 117.33/118.13 (P3(a85,a85)),
% 117.33/118.13 inference(scs_inference,[],[214,201,148,104,75,105,100])).
% 117.33/118.13 cnf(335,plain,
% 117.33/118.13 (P4(a5,a88)),
% 117.33/118.13 inference(scs_inference,[],[110,214,201,148,329,104,75,105,100,91])).
% 117.33/118.13 cnf(340,plain,
% 117.33/118.13 (P3(a10,a10)),
% 117.33/118.13 inference(scs_inference,[],[210,105,100])).
% 117.33/118.13 cnf(342,plain,
% 117.33/118.13 (P4(a5,a91)),
% 117.33/118.13 inference(scs_inference,[],[110,210,154,105,100,91])).
% 117.33/118.13 cnf(346,plain,
% 117.33/118.13 (~P5(a10,a10)),
% 117.33/118.13 inference(scs_inference,[],[110,210,154,105,100,91,104])).
% 117.33/118.13 cnf(351,plain,
% 117.33/118.13 (P4(a5,a84)),
% 117.33/118.13 inference(scs_inference,[],[110,157,91])).
% 117.33/118.13 cnf(359,plain,
% 117.33/118.13 (P4(a5,a89)),
% 117.33/118.13 inference(scs_inference,[],[110,160,91])).
% 117.33/118.13 cnf(366,plain,
% 117.33/118.13 (P4(a5,a9)),
% 117.33/118.13 inference(scs_inference,[],[110,163,91])).
% 117.33/118.13 cnf(372,plain,
% 117.33/118.13 (P4(a5,a80)),
% 117.33/118.13 inference(scs_inference,[],[110,166,91])).
% 117.33/118.13 cnf(395,plain,
% 117.33/118.13 (P4(a74,a91)),
% 117.33/118.13 inference(scs_inference,[],[122,181,91])).
% 117.33/118.13 cnf(402,plain,
% 117.33/118.13 (P4(a5,a82)),
% 117.33/118.13 inference(scs_inference,[],[110,136,91])).
% 117.33/118.13 cnf(409,plain,
% 117.33/118.13 (P4(a5,a76)),
% 117.33/118.13 inference(scs_inference,[],[110,145,91])).
% 117.33/118.13 cnf(423,plain,
% 117.33/118.13 (P4(a74,a76)),
% 117.33/118.13 inference(scs_inference,[],[122,175,91])).
% 117.33/118.13 cnf(430,plain,
% 117.33/118.13 (P4(a87,a91)),
% 117.33/118.13 inference(scs_inference,[],[113,181,91])).
% 117.33/118.13 cnf(444,plain,
% 117.33/118.13 (P4(a85,a90)),
% 117.33/118.13 inference(scs_inference,[],[214,172,91])).
% 117.33/118.13 cnf(450,plain,
% 117.33/118.13 (P4(a10,a76)),
% 117.33/118.13 inference(scs_inference,[],[210,175,91])).
% 117.33/118.13 cnf(456,plain,
% 117.33/118.13 (P4(a87,a76)),
% 117.33/118.13 inference(scs_inference,[],[113,175,91])).
% 117.33/118.13 cnf(460,plain,
% 117.33/118.13 (~P1(a61,f75(a65))),
% 117.33/118.13 inference(scs_inference,[],[4,20,15])).
% 117.33/118.13 cnf(461,plain,
% 117.33/118.13 (~P6(x4611,a65,a73)),
% 117.33/118.13 inference(scs_inference,[],[460,35])).
% 117.33/118.13 cnf(463,plain,
% 117.33/118.13 (P1(a61,a65)),
% 117.33/118.13 inference(scs_inference,[],[460,35,17])).
% 117.33/118.13 cnf(465,plain,
% 117.33/118.13 (~P1(f43(a3,a65),f75(a65))),
% 117.33/118.13 inference(scs_inference,[],[8,460,35,17,101])).
% 117.33/118.13 cnf(470,plain,
% 117.33/118.13 (~P6(a3,a65,x4701)+P4(x4701,a73)),
% 117.33/118.13 inference(scs_inference,[],[8,460,35,17,101,75,91])).
% 117.33/118.13 cnf(506,plain,
% 117.33/118.13 (P6(a65,x5061,a87)),
% 117.33/118.13 inference(scs_inference,[],[465,23,17])).
% 117.33/118.13 cnf(507,plain,
% 117.33/118.13 (P1(f43(a3,a65),a65)),
% 117.33/118.13 inference(scs_inference,[],[465,17])).
% 117.33/118.13 cnf(511,plain,
% 117.33/118.13 (P3(a87,a87)),
% 117.33/118.13 inference(scs_inference,[],[506,465,17,105,100])).
% 117.33/118.13 cnf(513,plain,
% 117.33/118.13 (~P5(a87,a87)),
% 117.33/118.13 inference(scs_inference,[],[506,465,17,105,100,104])).
% 117.33/118.13 cnf(515,plain,
% 117.33/118.13 (P4(a5,a73)),
% 117.33/118.13 inference(scs_inference,[],[110,506,465,461,17,105,100,104,91])).
% 117.33/118.13 cnf(523,plain,
% 117.33/118.13 (P4(a10,a88)),
% 117.33/118.13 inference(scs_inference,[],[210,178,91])).
% 117.33/118.13 cnf(526,plain,
% 117.33/118.13 (P4(a85,a91)),
% 117.33/118.13 inference(scs_inference,[],[214,181,91])).
% 117.33/118.13 cnf(529,plain,
% 117.33/118.13 (~P6(x5291,a58,a82)),
% 117.33/118.13 inference(scs_inference,[],[110,27,36])).
% 117.33/118.13 cnf(530,plain,
% 117.33/118.13 (P4(a10,a90)),
% 117.33/118.13 inference(scs_inference,[],[210,172,91])).
% 117.33/118.13 cnf(536,plain,
% 117.33/118.13 (P4(a10,a91)),
% 117.33/118.13 inference(scs_inference,[],[210,181,91])).
% 117.33/118.13 cnf(539,plain,
% 117.33/118.13 (P4(a85,a76)),
% 117.33/118.13 inference(scs_inference,[],[214,175,91])).
% 117.33/118.13 cnf(542,plain,
% 117.33/118.13 (~P6(x5421,a58,a88)),
% 117.33/118.13 inference(scs_inference,[],[194,29,38])).
% 117.33/118.13 cnf(543,plain,
% 117.33/118.13 (~P6(f75(a65),x5431,a73)),
% 117.33/118.13 inference(scs_inference,[],[461,32,218])).
% 117.33/118.13 cnf(544,plain,
% 117.33/118.13 (~P6(a59,a58,a8)),
% 117.33/118.13 inference(scs_inference,[],[3,14,80])).
% 117.33/118.13 cnf(545,plain,
% 117.33/118.13 (~P1(x5451,a58)),
% 117.33/118.13 inference(rename_variables,[],[14])).
% 117.33/118.13 cnf(547,plain,
% 117.33/118.13 (~P6(a58,a59,a8)),
% 117.33/118.13 inference(scs_inference,[],[3,14,545,80,81])).
% 117.33/118.13 cnf(554,plain,
% 117.33/118.13 (~P6(a3,x5541,a84)),
% 117.33/118.13 inference(scs_inference,[],[214,37,28])).
% 117.33/118.13 cnf(555,plain,
% 117.33/118.13 (P3(a74,a87)),
% 117.33/118.13 inference(scs_inference,[],[122,506,100])).
% 117.33/118.13 cnf(556,plain,
% 117.33/118.13 (P6(a65,x5561,a87)),
% 117.33/118.13 inference(rename_variables,[],[506])).
% 117.33/118.13 cnf(557,plain,
% 117.33/118.13 (P6(x5571,a3,a74)),
% 117.33/118.13 inference(rename_variables,[],[122])).
% 117.33/118.13 cnf(559,plain,
% 117.33/118.13 (~P5(a74,a87)),
% 117.33/118.13 inference(scs_inference,[],[122,557,506,556,100,104])).
% 117.33/118.13 cnf(560,plain,
% 117.33/118.13 (P6(a65,x5601,a87)),
% 117.33/118.13 inference(rename_variables,[],[506])).
% 117.33/118.13 cnf(561,plain,
% 117.33/118.13 (P6(x5611,a3,a74)),
% 117.33/118.13 inference(rename_variables,[],[122])).
% 117.33/118.13 cnf(571,plain,
% 117.33/118.13 (P4(a10,a84)),
% 117.33/118.13 inference(scs_inference,[],[210,122,557,561,506,556,560,529,554,543,100,104,105,75,91])).
% 117.33/118.13 cnf(574,plain,
% 117.33/118.13 (~P6(a3,x5741,a89)),
% 117.33/118.13 inference(scs_inference,[],[194,39,30])).
% 117.33/118.13 cnf(579,plain,
% 117.33/118.13 (P4(a10,a89)),
% 117.33/118.13 inference(scs_inference,[],[210,542,574,543,75,91])).
% 117.33/118.13 cnf(587,plain,
% 117.33/118.13 (~P6(f49(x5871,a73),f50(x5871,a73),a73)+~P6(a3,a65,x5871)),
% 117.33/118.13 inference(scs_inference,[],[470,102])).
% 117.33/118.13 cnf(589,plain,
% 117.33/118.13 (~P1(x5891,a58)),
% 117.33/118.13 inference(rename_variables,[],[14])).
% 117.33/118.13 cnf(591,plain,
% 117.33/118.13 (~P6(a58,a62,a8)),
% 117.43/118.13 inference(scs_inference,[],[4,14,589,80,81])).
% 117.43/118.13 cnf(594,plain,
% 117.43/118.13 (~P2(a73,a8)+~P6(x5941,a58,a73)),
% 117.43/118.13 inference(scs_inference,[],[198,222,94])).
% 117.43/118.13 cnf(595,plain,
% 117.43/118.13 (~P1(f43(a3,a58),f75(a58))+~P2(a73,a8)),
% 117.43/118.13 inference(scs_inference,[],[594,218])).
% 117.43/118.13 cnf(596,plain,
% 117.43/118.13 (~P6(a65,a58,a8)),
% 117.43/118.13 inference(scs_inference,[],[5,14,80])).
% 117.43/118.13 cnf(597,plain,
% 117.43/118.13 (~P1(x5971,a58)),
% 117.43/118.13 inference(rename_variables,[],[14])).
% 117.43/118.13 cnf(599,plain,
% 117.43/118.13 (~P6(a58,a65,a8)),
% 117.43/118.13 inference(scs_inference,[],[5,14,597,80,81])).
% 117.43/118.13 cnf(603,plain,
% 117.43/118.13 (P6(a3,f75(a58),a85)),
% 117.43/118.13 inference(scs_inference,[],[14,254,17])).
% 117.43/118.13 cnf(604,plain,
% 117.43/118.13 (P1(x6041,f75(a58))),
% 117.43/118.13 inference(scs_inference,[],[603,28])).
% 117.43/118.13 cnf(608,plain,
% 117.43/118.13 (~P6(a69,a58,a8)),
% 117.43/118.13 inference(scs_inference,[],[6,603,14,28,86,80])).
% 117.43/118.13 cnf(609,plain,
% 117.43/118.13 (~P1(x6091,a58)),
% 117.43/118.13 inference(rename_variables,[],[14])).
% 117.43/118.13 cnf(611,plain,
% 117.43/118.13 (~P6(a58,a69,a8)),
% 117.43/118.13 inference(scs_inference,[],[6,603,14,609,28,86,80,81])).
% 117.43/118.13 cnf(614,plain,
% 117.43/118.13 (~P2(a73,a8)),
% 117.43/118.13 inference(scs_inference,[],[604,595])).
% 117.43/118.13 cnf(616,plain,
% 117.43/118.13 (~P6(f75(a58),x6161,a88)),
% 117.43/118.13 inference(scs_inference,[],[604,84])).
% 117.43/118.13 cnf(617,plain,
% 117.43/118.13 (P1(x6171,f75(a58))),
% 117.43/118.13 inference(rename_variables,[],[604])).
% 117.43/118.13 cnf(619,plain,
% 117.43/118.13 (P6(x6191,f75(a58),a74)),
% 117.43/118.13 inference(scs_inference,[],[604,617,84,42])).
% 117.43/118.13 cnf(620,plain,
% 117.43/118.13 (P1(x6201,f75(a58))),
% 117.43/118.13 inference(rename_variables,[],[604])).
% 117.43/118.13 cnf(622,plain,
% 117.43/118.13 (~P6(f75(a58),x6221,a76)),
% 117.43/118.13 inference(scs_inference,[],[604,617,620,84,42,83])).
% 117.43/118.13 cnf(623,plain,
% 117.43/118.13 (P1(x6231,f75(a58))),
% 117.43/118.13 inference(rename_variables,[],[604])).
% 117.43/118.13 cnf(625,plain,
% 117.43/118.13 (~P6(f75(a58),x6251,a91)),
% 117.43/118.13 inference(scs_inference,[],[604,617,620,623,84,42,83,85])).
% 117.43/118.13 cnf(626,plain,
% 117.43/118.13 (P1(x6261,f75(a58))),
% 117.43/118.13 inference(rename_variables,[],[604])).
% 117.43/118.13 cnf(629,plain,
% 117.43/118.13 (P1(x6291,f75(a58))),
% 117.43/118.13 inference(rename_variables,[],[604])).
% 117.43/118.13 cnf(632,plain,
% 117.43/118.13 (P1(x6321,f75(a58))),
% 117.43/118.13 inference(rename_variables,[],[604])).
% 117.43/118.13 cnf(635,plain,
% 117.43/118.13 (P1(x6351,f75(a58))),
% 117.43/118.13 inference(rename_variables,[],[604])).
% 117.43/118.13 cnf(636,plain,
% 117.43/118.13 (P1(x6361,a3)),
% 117.43/118.13 inference(rename_variables,[],[8])).
% 117.43/118.13 cnf(638,plain,
% 117.43/118.13 (P6(a3,a58,a73)),
% 117.43/118.13 inference(scs_inference,[],[8,636,604,617,620,623,626,629,632,635,84,42,83,85,87,82,98,101])).
% 117.43/118.13 cnf(642,plain,
% 117.43/118.13 (P3(a73,a73)),
% 117.43/118.13 inference(scs_inference,[],[8,636,604,617,620,623,626,629,632,635,84,42,83,85,87,82,98,101,100])).
% 117.43/118.13 cnf(644,plain,
% 117.43/118.13 (~P5(a73,a73)),
% 117.43/118.13 inference(scs_inference,[],[8,636,604,617,620,623,626,629,632,635,84,42,83,85,87,82,98,101,100,104])).
% 117.43/118.13 cnf(663,plain,
% 117.43/118.13 (P4(a73,a8)),
% 117.43/118.13 inference(scs_inference,[],[638,198,616,604,461,101,75,91])).
% 117.43/118.13 cnf(667,plain,
% 117.43/118.13 (P6(f48(a5,a5),f51(a5,a5),a5)),
% 117.43/118.13 inference(scs_inference,[],[110,51,104])).
% 117.43/118.13 cnf(668,plain,
% 117.43/118.13 (~P1(x6681,f48(a5,a5))),
% 117.43/118.13 inference(scs_inference,[],[667,36])).
% 117.43/118.13 cnf(674,plain,
% 117.43/118.13 (P4(a74,a73)),
% 117.43/118.13 inference(scs_inference,[],[619,667,622,543,36,68,75,91])).
% 117.43/118.13 cnf(678,plain,
% 117.43/118.13 (P1(x6781,f48(a85,a85))),
% 117.43/118.13 inference(scs_inference,[],[326,52,31])).
% 117.43/118.13 cnf(680,plain,
% 117.43/118.13 (~P1(x6801,f48(a5,a5))),
% 117.43/118.13 inference(rename_variables,[],[668])).
% 117.43/118.13 cnf(682,plain,
% 117.43/118.13 (P6(f48(a5,a5),x6821,a81)),
% 117.43/118.13 inference(scs_inference,[],[668,680,60,25])).
% 117.43/118.13 cnf(683,plain,
% 117.43/118.13 (~P1(x6831,f48(a5,a5))),
% 117.43/118.13 inference(rename_variables,[],[668])).
% 117.43/118.13 cnf(686,plain,
% 117.43/118.13 (~P1(x6861,f48(a5,a5))),
% 117.43/118.13 inference(rename_variables,[],[668])).
% 117.43/118.13 cnf(689,plain,
% 117.43/118.13 (~P1(x6891,f48(a5,a5))),
% 117.43/118.13 inference(rename_variables,[],[668])).
% 117.43/118.14 cnf(692,plain,
% 117.43/118.14 (~P1(x6921,f48(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[668])).
% 117.43/118.14 cnf(695,plain,
% 117.43/118.14 (~P1(x6951,f48(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[668])).
% 117.43/118.14 cnf(698,plain,
% 117.43/118.14 (~P1(x6981,f48(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[668])).
% 117.43/118.14 cnf(701,plain,
% 117.43/118.14 (~P1(x7011,f48(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[668])).
% 117.43/118.14 cnf(703,plain,
% 117.43/118.14 (P6(f48(a5,a5),x7031,a74)),
% 117.43/118.14 inference(scs_inference,[],[668,680,683,686,689,692,695,698,701,60,25,55,66,53,54,57,65,26])).
% 117.43/118.14 cnf(704,plain,
% 117.43/118.14 (~P1(x7041,f48(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[668])).
% 117.43/118.14 cnf(707,plain,
% 117.43/118.14 (~P1(x7071,f48(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[668])).
% 117.43/118.14 cnf(710,plain,
% 117.43/118.14 (~P1(x7101,f48(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[668])).
% 117.43/118.14 cnf(713,plain,
% 117.43/118.14 (~P1(x7131,f48(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[668])).
% 117.43/118.14 cnf(716,plain,
% 117.43/118.14 (P1(x7161,f48(a85,a85))),
% 117.43/118.14 inference(rename_variables,[],[678])).
% 117.43/118.14 cnf(719,plain,
% 117.43/118.14 (~P1(x7191,f48(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[668])).
% 117.43/118.14 cnf(722,plain,
% 117.43/118.14 (~P1(x7221,f48(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[668])).
% 117.43/118.14 cnf(725,plain,
% 117.43/118.14 (~P1(x7251,f48(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[668])).
% 117.43/118.14 cnf(727,plain,
% 117.43/118.14 (~P6(x7271,f48(a85,a85),a89)),
% 117.43/118.14 inference(scs_inference,[],[668,680,683,686,689,692,695,698,701,704,707,710,713,719,722,678,716,60,25,55,66,53,54,57,65,26,59,61,62,83,56,58,64,87])).
% 117.43/118.14 cnf(728,plain,
% 117.43/118.14 (P1(x7281,f48(a85,a85))),
% 117.43/118.14 inference(rename_variables,[],[678])).
% 117.43/118.14 cnf(731,plain,
% 117.43/118.14 (~P1(x7311,f48(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[668])).
% 117.43/118.14 cnf(734,plain,
% 117.43/118.14 (~P1(x7341,f48(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[668])).
% 117.43/118.14 cnf(736,plain,
% 117.43/118.14 (P6(x7361,f48(a5,a5),a87)),
% 117.43/118.14 inference(scs_inference,[],[668,680,683,686,689,692,695,698,701,704,707,710,713,719,722,725,731,734,678,716,60,25,55,66,53,54,57,65,26,59,61,62,83,56,58,64,87,21,63,24])).
% 117.43/118.14 cnf(737,plain,
% 117.43/118.14 (~P1(x7371,f48(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[668])).
% 117.43/118.14 cnf(740,plain,
% 117.43/118.14 (P1(x7401,f48(a85,a85))),
% 117.43/118.14 inference(rename_variables,[],[678])).
% 117.43/118.14 cnf(743,plain,
% 117.43/118.14 (P1(x7431,f48(a85,a85))),
% 117.43/118.14 inference(rename_variables,[],[678])).
% 117.43/118.14 cnf(745,plain,
% 117.43/118.14 (P6(x7451,f48(a85,a85),a74)),
% 117.43/118.14 inference(scs_inference,[],[668,680,683,686,689,692,695,698,701,704,707,710,713,719,722,725,731,734,678,716,728,740,743,60,25,55,66,53,54,57,65,26,59,61,62,83,56,58,64,87,21,63,24,84,85,42])).
% 117.43/118.14 cnf(746,plain,
% 117.43/118.14 (P1(x7461,f48(a85,a85))),
% 117.43/118.14 inference(rename_variables,[],[678])).
% 117.43/118.14 cnf(748,plain,
% 117.43/118.14 (~P6(f48(a85,a85),x7481,a90)),
% 117.43/118.14 inference(scs_inference,[],[668,680,683,686,689,692,695,698,701,704,707,710,713,719,722,725,731,734,678,716,728,740,743,746,60,25,55,66,53,54,57,65,26,59,61,62,83,56,58,64,87,21,63,24,84,85,42,82])).
% 117.43/118.14 cnf(749,plain,
% 117.43/118.14 (P1(x7491,f48(a85,a85))),
% 117.43/118.14 inference(rename_variables,[],[678])).
% 117.43/118.14 cnf(751,plain,
% 117.43/118.14 (~P6(x7511,f48(a85,a85),a91)),
% 117.43/118.14 inference(scs_inference,[],[668,680,683,686,689,692,695,698,701,704,707,710,713,719,722,725,731,734,678,716,728,740,743,746,749,60,25,55,66,53,54,57,65,26,59,61,62,83,56,58,64,87,21,63,24,84,85,42,82,86])).
% 117.43/118.14 cnf(752,plain,
% 117.43/118.14 (P1(x7521,f48(a85,a85))),
% 117.43/118.14 inference(rename_variables,[],[678])).
% 117.43/118.14 cnf(754,plain,
% 117.43/118.14 (P6(a58,f48(a5,a5),a8)),
% 117.43/118.14 inference(scs_inference,[],[14,668,680,683,686,689,692,695,698,701,704,707,710,713,719,722,725,731,734,737,678,716,728,740,743,746,749,60,25,55,66,53,54,57,65,26,59,61,62,83,56,58,64,87,21,63,24,84,85,42,82,86,76])).
% 117.43/118.14 cnf(756,plain,
% 117.43/118.14 (~P1(x7561,f48(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[668])).
% 117.43/118.14 cnf(759,plain,
% 117.43/118.14 (~P1(x7591,f48(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[668])).
% 117.43/118.14 cnf(760,plain,
% 117.43/118.14 (P1(x7601,a3)),
% 117.43/118.14 inference(rename_variables,[],[8])).
% 117.43/118.14 cnf(764,plain,
% 117.43/118.14 (P1(x7641,f48(a85,a85))),
% 117.43/118.14 inference(rename_variables,[],[678])).
% 117.43/118.14 cnf(770,plain,
% 117.43/118.14 (P3(a8,a8)),
% 117.43/118.14 inference(scs_inference,[],[8,760,14,668,680,683,686,689,692,695,698,701,704,707,710,713,719,722,725,731,734,737,756,678,716,728,740,743,746,749,752,764,604,60,25,55,66,53,54,57,65,26,59,61,62,83,56,58,64,87,21,63,24,84,85,42,82,86,76,93,98,101,100])).
% 117.43/118.14 cnf(775,plain,
% 117.43/118.14 (~P5(a8,a8)),
% 117.43/118.14 inference(scs_inference,[],[6,8,760,14,668,680,683,686,689,692,695,698,701,704,707,710,713,719,722,725,731,734,737,756,759,678,716,728,740,743,746,749,752,764,604,60,25,55,66,53,54,57,65,26,59,61,62,83,56,58,64,87,21,63,24,84,85,42,82,86,76,93,98,101,100,81,104])).
% 117.43/118.14 cnf(779,plain,
% 117.43/118.14 (P4(a81,a8)),
% 117.43/118.14 inference(scs_inference,[],[6,8,760,14,668,680,683,686,689,692,695,698,701,704,707,710,713,719,722,725,731,734,737,756,759,678,716,728,740,743,746,749,752,764,625,604,60,25,55,66,53,54,57,65,26,59,61,62,83,56,58,64,87,21,63,24,84,85,42,82,86,76,93,98,101,100,81,104,75,91])).
% 117.43/118.14 cnf(798,plain,
% 117.43/118.14 (P6(f45(a5,a5),f46(a5,a5),a5)),
% 117.43/118.14 inference(scs_inference,[],[110,69,100])).
% 117.43/118.14 cnf(799,plain,
% 117.43/118.14 (~P1(x7991,f45(a5,a5))),
% 117.43/118.14 inference(scs_inference,[],[798,36])).
% 117.43/118.14 cnf(827,plain,
% 117.43/118.14 (~P1(x8271,f45(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[799])).
% 117.43/118.14 cnf(830,plain,
% 117.43/118.14 (~P1(x8301,f45(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[799])).
% 117.43/118.14 cnf(833,plain,
% 117.43/118.14 (~P1(x8331,f45(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[799])).
% 117.43/118.14 cnf(836,plain,
% 117.43/118.14 (~P1(x8361,f45(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[799])).
% 117.43/118.14 cnf(839,plain,
% 117.43/118.14 (~P1(x8391,f45(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[799])).
% 117.43/118.14 cnf(842,plain,
% 117.43/118.14 (~P1(x8421,f45(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[799])).
% 117.43/118.14 cnf(845,plain,
% 117.43/118.14 (~P1(x8451,f45(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[799])).
% 117.43/118.14 cnf(848,plain,
% 117.43/118.14 (~P1(x8481,f45(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[799])).
% 117.43/118.14 cnf(851,plain,
% 117.43/118.14 (~P1(x8511,f45(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[799])).
% 117.43/118.14 cnf(854,plain,
% 117.43/118.14 (~P1(x8541,f45(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[799])).
% 117.43/118.14 cnf(856,plain,
% 117.43/118.14 (P6(x8561,f45(a5,a5),a87)),
% 117.43/118.14 inference(scs_inference,[],[799,827,830,833,836,839,842,845,848,851,854,53,55,57,67,65,66,26,56,60,54,24])).
% 117.43/118.14 cnf(857,plain,
% 117.43/118.14 (~P1(x8571,f45(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[799])).
% 117.43/118.14 cnf(859,plain,
% 117.43/118.14 (P6(f45(a5,a5),x8591,a81)),
% 117.43/118.14 inference(scs_inference,[],[799,827,830,833,836,839,842,845,848,851,854,857,53,55,57,67,65,66,26,56,60,54,24,25])).
% 117.43/118.14 cnf(860,plain,
% 117.43/118.14 (~P1(x8601,f45(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[799])).
% 117.43/118.14 cnf(862,plain,
% 117.43/118.14 (~P6(x8621,f45(a5,a5),a84)),
% 117.43/118.14 inference(scs_inference,[],[799,827,830,833,836,839,842,845,848,851,854,857,860,53,55,57,67,65,66,26,56,60,54,24,25,63])).
% 117.43/118.14 cnf(863,plain,
% 117.43/118.14 (~P1(x8631,f45(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[799])).
% 117.43/118.14 cnf(866,plain,
% 117.43/118.14 (~P1(x8661,f45(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[799])).
% 117.43/118.14 cnf(869,plain,
% 117.43/118.14 (~P1(x8691,f45(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[799])).
% 117.43/118.14 cnf(872,plain,
% 117.43/118.14 (~P1(x8721,f45(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[799])).
% 117.43/118.14 cnf(874,plain,
% 117.43/118.14 (~P6(x8741,f45(a5,a5),a89)),
% 117.43/118.14 inference(scs_inference,[],[799,827,830,833,836,839,842,845,848,851,854,857,860,863,866,869,872,53,55,57,67,65,66,26,56,60,54,24,25,63,59,58,62,64])).
% 117.43/118.14 cnf(875,plain,
% 117.43/118.14 (~P1(x8751,f45(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[799])).
% 117.43/118.14 cnf(878,plain,
% 117.43/118.14 (~P1(x8781,f45(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[799])).
% 117.43/118.14 cnf(882,plain,
% 117.43/118.14 (~P1(x8821,f45(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[799])).
% 117.43/118.14 cnf(885,plain,
% 117.43/118.14 (~P1(x8851,f45(a5,a5))),
% 117.43/118.14 inference(rename_variables,[],[799])).
% 117.43/118.14 cnf(894,plain,
% 117.43/118.14 (P3(a74,a74)),
% 117.43/118.14 inference(scs_inference,[],[6,736,8,14,799,827,830,833,836,839,842,845,848,851,854,857,860,863,866,869,872,875,878,882,885,53,55,57,67,65,66,26,56,60,54,24,25,63,59,58,62,64,21,76,93,105,81,100])).
% 117.43/118.14 cnf(896,plain,
% 117.43/118.14 (~P5(a74,a74)),
% 117.43/118.14 inference(scs_inference,[],[6,736,8,14,799,827,830,833,836,839,842,845,848,851,854,857,860,863,866,869,872,875,878,882,885,53,55,57,67,65,66,26,56,60,54,24,25,63,59,58,62,64,21,76,93,105,81,100,104])).
% 117.43/118.14 cnf(952,plain,
% 117.43/118.14 (P1(x9521,f75(f46(a73,a73)))),
% 117.43/118.14 inference(scs_inference,[],[642,70,35])).
% 117.43/118.14 cnf(953,plain,
% 117.43/118.14 (~P1(x9531,f46(a73,a73))),
% 117.43/118.14 inference(scs_inference,[],[952,20])).
% 117.43/118.14 cnf(971,plain,
% 117.43/118.14 (~P1(x9711,f46(a73,a73))),
% 117.43/118.14 inference(rename_variables,[],[953])).
% 117.43/118.14 cnf(974,plain,
% 117.43/118.14 (~P1(x9741,f46(a73,a73))),
% 117.43/118.14 inference(rename_variables,[],[953])).
% 117.43/118.14 cnf(977,plain,
% 117.43/118.14 (~P1(x9771,f46(a73,a73))),
% 117.43/118.14 inference(rename_variables,[],[953])).
% 117.43/118.14 cnf(980,plain,
% 117.43/118.14 (~P1(x9801,f46(a73,a73))),
% 117.43/118.14 inference(rename_variables,[],[953])).
% 117.43/118.14 cnf(983,plain,
% 117.43/118.14 (~P1(x9831,f46(a73,a73))),
% 117.43/118.14 inference(rename_variables,[],[953])).
% 117.43/118.14 cnf(986,plain,
% 117.43/118.14 (~P1(x9861,f46(a73,a73))),
% 117.43/118.14 inference(rename_variables,[],[953])).
% 117.43/118.14 cnf(988,plain,
% 117.43/118.14 (~P6(f46(a73,a73),x9881,a10)),
% 117.43/118.14 inference(scs_inference,[],[953,971,974,977,980,983,986,65,68,26,56,60,53,55])).
% 117.43/118.14 cnf(989,plain,
% 117.43/118.14 (~P1(x9891,f46(a73,a73))),
% 117.43/118.14 inference(rename_variables,[],[953])).
% 117.43/118.14 cnf(992,plain,
% 117.43/118.14 (~P1(x9921,f46(a73,a73))),
% 117.43/118.14 inference(rename_variables,[],[953])).
% 117.43/118.14 cnf(994,plain,
% 117.43/118.14 (P6(x9941,f46(a73,a73),a87)),
% 117.43/118.14 inference(scs_inference,[],[953,971,974,977,980,983,986,989,992,65,68,26,56,60,53,55,59,24])).
% 117.43/118.14 cnf(995,plain,
% 117.43/118.14 (~P1(x9951,f46(a73,a73))),
% 117.43/118.14 inference(rename_variables,[],[953])).
% 117.43/118.14 cnf(998,plain,
% 117.43/118.14 (~P1(x9981,f46(a73,a73))),
% 117.43/118.14 inference(rename_variables,[],[953])).
% 117.43/118.14 cnf(1001,plain,
% 117.43/118.14 (~P1(x10011,f46(a73,a73))),
% 117.43/118.14 inference(rename_variables,[],[953])).
% 117.43/118.14 cnf(1004,plain,
% 117.43/118.14 (~P1(x10041,f46(a73,a73))),
% 117.43/118.14 inference(rename_variables,[],[953])).
% 117.43/118.14 cnf(1007,plain,
% 117.43/118.14 (~P1(x10071,f46(a73,a73))),
% 117.43/118.14 inference(rename_variables,[],[953])).
% 117.43/118.14 cnf(1010,plain,
% 117.43/118.14 (~P1(x10101,f46(a73,a73))),
% 117.43/118.14 inference(rename_variables,[],[953])).
% 117.43/118.14 cnf(1013,plain,
% 117.43/118.14 (~P1(x10131,f46(a73,a73))),
% 117.43/118.14 inference(rename_variables,[],[953])).
% 117.43/118.14 cnf(1016,plain,
% 117.43/118.14 (~P1(x10161,f46(a73,a73))),
% 117.43/118.14 inference(rename_variables,[],[953])).
% 117.43/118.14 cnf(1019,plain,
% 117.43/118.14 (~P1(x10191,f46(a73,a73))),
% 117.43/118.14 inference(rename_variables,[],[953])).
% 117.43/118.14 cnf(1021,plain,
% 117.43/118.14 (P6(f46(a73,a73),x10211,a5)),
% 117.43/118.14 inference(scs_inference,[],[953,971,974,977,980,983,986,989,992,995,998,1001,1004,1007,1010,1013,1016,1019,65,68,26,56,60,53,55,59,24,66,63,61,54,58,25,62,64,21])).
% 117.43/118.14 cnf(1022,plain,
% 117.43/118.14 (~P1(x10221,f46(a73,a73))),
% 117.43/118.14 inference(rename_variables,[],[953])).
% 117.43/118.14 cnf(1025,plain,
% 117.43/118.14 (~P1(x10251,f46(a73,a73))),
% 117.43/118.14 inference(rename_variables,[],[953])).
% 117.43/118.14 cnf(1029,plain,
% 117.43/118.14 (~P1(x10291,f46(a73,a73))),
% 117.43/118.14 inference(rename_variables,[],[953])).
% 117.43/118.14 cnf(1040,plain,
% 117.43/118.14 (P6(x10401,f48(a85,a85),a74)),
% 117.43/118.14 inference(rename_variables,[],[745])).
% 117.43/118.14 cnf(1042,plain,
% 117.43/118.14 (P3(a74,a81)),
% 117.43/118.14 inference(scs_inference,[],[6,745,1040,8,14,604,953,971,974,977,980,983,986,989,992,995,998,1001,1004,1007,1010,1013,1016,1019,1022,1025,1029,952,65,68,26,56,60,53,55,59,24,66,63,61,54,58,25,62,64,21,93,76,101,80,105,100])).
% 117.43/118.14 cnf(1045,plain,
% 117.43/118.14 (~P5(a81,a81)),
% 117.43/118.14 inference(scs_inference,[],[6,745,1040,8,14,604,953,971,974,977,980,983,986,989,992,995,998,1001,1004,1007,1010,1013,1016,1019,1022,1025,1029,952,65,68,26,56,60,53,55,59,24,66,63,61,54,58,25,62,64,21,93,76,101,80,105,100,104])).
% 117.43/118.14 cnf(1186,plain,
% 117.43/118.14 (~P2(x11861,a73)+~P6(f49(x11862,a73),f50(x11862,a73),x11861)+~P6(a3,a65,x11862)),
% 117.43/118.14 inference(scs_inference,[],[587,94])).
% 117.43/118.14 cnf(1190,plain,
% 117.43/118.14 (P6(a58,x11901,a5)),
% 117.43/118.14 inference(rename_variables,[],[110])).
% 117.43/118.14 cnf(1191,plain,
% 117.43/118.14 (P6(x11911,a58,a87)),
% 117.43/118.14 inference(rename_variables,[],[113])).
% 117.43/118.14 cnf(1193,plain,
% 117.43/118.14 (P3(a87,a5)),
% 117.43/118.14 inference(scs_inference,[],[113,1191,110,1190,105,100])).
% 117.43/118.14 cnf(1194,plain,
% 117.43/118.14 (P6(a58,x11941,a5)),
% 117.43/118.14 inference(rename_variables,[],[110])).
% 117.43/118.14 cnf(1195,plain,
% 117.43/118.14 (P6(x11951,a58,a87)),
% 117.43/118.14 inference(rename_variables,[],[113])).
% 117.43/118.14 cnf(1197,plain,
% 117.43/118.14 (~P5(a87,a5)),
% 117.43/118.14 inference(scs_inference,[],[113,1191,1195,110,1190,1194,105,100,104])).
% 117.43/118.14 cnf(1208,plain,
% 117.43/118.14 (P6(x12081,a58,a87)),
% 117.43/118.14 inference(rename_variables,[],[113])).
% 117.43/118.14 cnf(1210,plain,
% 117.43/118.14 (~P5(a87,a74)),
% 117.43/118.14 inference(scs_inference,[],[113,1208,119,682,105,104])).
% 117.43/118.14 cnf(1211,plain,
% 117.43/118.14 (P6(a58,x12111,a74)),
% 117.43/118.14 inference(rename_variables,[],[119])).
% 117.43/118.14 cnf(1212,plain,
% 117.43/118.14 (P6(x12121,a58,a87)),
% 117.43/118.14 inference(rename_variables,[],[113])).
% 117.43/118.14 cnf(1214,plain,
% 117.43/118.14 (P3(a87,a74)),
% 117.43/118.15 inference(scs_inference,[],[113,1208,1212,119,1211,682,105,104,100])).
% 117.43/118.15 cnf(1223,plain,
% 117.43/118.15 (P3(a87,a81)),
% 117.43/118.15 inference(scs_inference,[],[113,859,100])).
% 117.43/118.15 cnf(1224,plain,
% 117.43/118.15 (P6(f45(a5,a5),x12241,a81)),
% 117.43/118.15 inference(rename_variables,[],[859])).
% 117.43/118.15 cnf(1225,plain,
% 117.43/118.15 (P6(x12251,a58,a87)),
% 117.43/118.15 inference(rename_variables,[],[113])).
% 117.43/118.15 cnf(1227,plain,
% 117.43/118.15 (~P5(a87,a81)),
% 117.43/118.15 inference(scs_inference,[],[113,1225,859,1224,100,104])).
% 117.43/118.15 cnf(1236,plain,
% 117.43/118.15 (P4(a87,a10)),
% 117.43/118.15 inference(scs_inference,[],[113,988,91])).
% 117.43/118.15 cnf(1281,plain,
% 117.43/118.15 (P6(a58,x12811,a5)),
% 117.43/118.15 inference(rename_variables,[],[110])).
% 117.43/118.15 cnf(1283,plain,
% 117.43/118.15 (~P5(a81,a5)),
% 117.43/118.15 inference(scs_inference,[],[116,110,1281,105,104])).
% 117.43/118.15 cnf(1286,plain,
% 117.43/118.15 (P3(a81,a81)),
% 117.43/118.15 inference(scs_inference,[],[116,110,1281,105,104,100])).
% 117.43/118.15 cnf(1288,plain,
% 117.43/118.15 (P4(a81,a83)),
% 117.43/118.15 inference(scs_inference,[],[116,110,1281,130,105,104,100,91])).
% 117.43/118.15 cnf(1293,plain,
% 117.43/118.15 (P6(x12931,f75(a58),a74)),
% 117.43/118.15 inference(rename_variables,[],[619])).
% 117.43/118.15 cnf(1294,plain,
% 117.43/118.15 (P6(a58,x12941,a81)),
% 117.43/118.15 inference(rename_variables,[],[116])).
% 117.43/118.15 cnf(1296,plain,
% 117.43/118.15 (~P5(a81,a74)),
% 117.43/118.15 inference(scs_inference,[],[116,1294,619,1293,105,104])).
% 117.43/118.15 cnf(1298,plain,
% 117.43/118.15 (P6(a58,x12981,a81)),
% 117.43/118.15 inference(rename_variables,[],[116])).
% 117.43/118.15 cnf(1300,plain,
% 117.43/118.15 (P3(a81,a5)),
% 117.43/118.15 inference(scs_inference,[],[116,1294,1298,110,619,1293,105,104,100])).
% 117.43/118.15 cnf(1303,plain,
% 117.43/118.15 (P4(a81,a73)),
% 117.43/118.15 inference(scs_inference,[],[116,1294,1298,110,619,1293,461,105,104,100,91])).
% 117.43/118.15 cnf(1307,plain,
% 117.43/118.15 (~P5(a81,a87)),
% 117.43/118.15 inference(scs_inference,[],[116,856,104])).
% 117.43/118.15 cnf(1308,plain,
% 117.43/118.15 (P6(x13081,f45(a5,a5),a87)),
% 117.43/118.15 inference(rename_variables,[],[856])).
% 117.43/118.15 cnf(1309,plain,
% 117.43/118.15 (P6(a58,x13091,a81)),
% 117.43/118.15 inference(rename_variables,[],[116])).
% 117.43/118.15 cnf(1313,plain,
% 117.43/118.15 (P6(a58,x13131,a81)),
% 117.43/118.15 inference(rename_variables,[],[116])).
% 117.43/118.15 cnf(1315,plain,
% 117.43/118.15 (P3(a81,a74)),
% 117.43/118.15 inference(scs_inference,[],[116,1309,1313,745,856,1308,104,105,100])).
% 117.43/118.15 cnf(1323,plain,
% 117.43/118.15 (P3(a81,a87)),
% 117.43/118.15 inference(scs_inference,[],[116,994,100])).
% 117.43/118.15 cnf(1325,plain,
% 117.43/118.15 (P6(a58,x13251,a81)),
% 117.43/118.15 inference(rename_variables,[],[116])).
% 117.43/118.15 cnf(1327,plain,
% 117.43/118.15 (P4(a81,a84)),
% 117.43/118.15 inference(scs_inference,[],[116,1325,994,862,100,91])).
% 117.43/118.15 cnf(1331,plain,
% 117.43/118.15 (~P6(a62,a3,a76)),
% 117.43/118.15 inference(scs_inference,[],[8,11,45,15])).
% 117.43/118.15 cnf(1332,plain,
% 117.43/118.15 (P4(a81,a89)),
% 117.43/118.15 inference(scs_inference,[],[116,874,91])).
% 117.43/118.15 cnf(1341,plain,
% 117.43/118.15 (~P6(x13411,a58,a76)+P6(x13411,x13412,a5)),
% 117.43/118.15 inference(scs_inference,[],[14,48,21])).
% 117.43/118.15 cnf(1342,plain,
% 117.43/118.15 (P4(a81,a88)),
% 117.43/118.15 inference(scs_inference,[],[116,542,91])).
% 117.43/118.15 cnf(1346,plain,
% 117.43/118.15 (P2(x13461,a5)+~P6(f41(x13461,a5),a58,a76)),
% 117.43/118.15 inference(scs_inference,[],[1341,99])).
% 117.43/118.15 cnf(1347,plain,
% 117.43/118.15 (P4(a81,a91)),
% 117.43/118.15 inference(scs_inference,[],[116,751,91])).
% 117.43/118.15 cnf(1351,plain,
% 117.43/118.15 (~P2(a87,a76)+P2(x13511,a5)),
% 117.43/118.15 inference(scs_inference,[],[113,1346,94])).
% 117.43/118.15 cnf(1460,plain,
% 117.43/118.15 (P6(a58,x14601,a5)),
% 117.43/118.15 inference(rename_variables,[],[110])).
% 117.43/118.15 cnf(1462,plain,
% 117.43/118.15 (~P5(a74,a5)),
% 117.43/118.15 inference(scs_inference,[],[119,110,1460,105,104])).
% 117.43/118.15 cnf(1463,plain,
% 117.43/118.15 (P6(a58,x14631,a5)),
% 117.43/118.15 inference(rename_variables,[],[110])).
% 117.43/118.15 cnf(1465,plain,
% 117.43/118.15 (P3(a74,a5)),
% 117.43/118.15 inference(scs_inference,[],[119,110,1460,1463,105,104,100])).
% 117.43/118.15 cnf(1473,plain,
% 117.43/118.15 (P6(a58,x14731,a81)),
% 117.43/118.15 inference(rename_variables,[],[116])).
% 117.43/118.15 cnf(1475,plain,
% 117.43/118.15 (~P5(a74,a81)),
% 117.43/118.15 inference(scs_inference,[],[119,116,1473,105,104])).
% 117.43/118.15 cnf(1519,plain,
% 117.43/118.15 (P6(x15191,a65,a81)),
% 117.43/118.15 inference(scs_inference,[],[4,15,22])).
% 117.43/118.15 cnf(1521,plain,
% 117.43/118.15 (P6(x15211,a65,a81)),
% 117.43/118.15 inference(rename_variables,[],[1519])).
% 117.43/118.15 cnf(1526,plain,
% 117.43/118.15 (~P6(f49(a81,a73),f50(a81,a73),x15261)+~P2(x15261,a73)),
% 117.43/118.15 inference(scs_inference,[],[133,1519,1521,130,587,75,1186])).
% 117.43/118.15 cnf(1661,plain,
% 117.43/118.15 (~P2(a81,a73)),
% 117.43/118.15 inference(scs_inference,[],[1303,1526,71])).
% 117.43/118.15 cnf(1703,plain,
% 117.43/118.15 (P1(a68,f75(a62))),
% 117.43/118.15 inference(scs_inference,[],[11,15,17])).
% 117.43/118.15 cnf(1708,plain,
% 117.43/118.15 (~P6(a65,x17081,a5)),
% 117.43/118.15 inference(scs_inference,[],[4,15,36])).
% 117.43/118.15 cnf(1717,plain,
% 117.43/118.15 (~P6(x17171,a62,a82)),
% 117.43/118.15 inference(scs_inference,[],[11,15,27])).
% 117.43/118.15 cnf(1718,plain,
% 117.43/118.15 (~P6(a65,x17181,a84)),
% 117.43/118.15 inference(scs_inference,[],[4,15,37])).
% 117.43/118.15 cnf(1722,plain,
% 117.43/118.15 (~P6(x17221,a62,a85)),
% 117.43/118.15 inference(scs_inference,[],[11,15,28])).
% 117.43/118.15 cnf(1723,plain,
% 117.43/118.15 (~P1(f24(a3,a62),a62)),
% 117.43/118.15 inference(scs_inference,[],[1722,254])).
% 117.43/118.15 cnf(1730,plain,
% 117.43/118.15 (~P6(a65,x17301,a86)),
% 117.43/118.15 inference(scs_inference,[],[4,15,38])).
% 117.43/118.15 cnf(1739,plain,
% 117.43/118.15 (~P6(x17391,a62,a88)),
% 117.43/118.15 inference(scs_inference,[],[11,15,29])).
% 117.43/118.15 cnf(1744,plain,
% 117.43/118.15 (~P6(a65,x17441,a89)),
% 117.43/118.15 inference(scs_inference,[],[4,15,39])).
% 117.43/118.15 cnf(1757,plain,
% 117.43/118.15 (P6(a65,a58,a9)),
% 117.43/118.15 inference(scs_inference,[],[4,604,15,40])).
% 117.43/118.15 cnf(1758,plain,
% 117.43/118.15 (~P5(a9,a9)),
% 117.43/118.15 inference(scs_inference,[],[1757,104])).
% 117.43/118.15 cnf(1760,plain,
% 117.43/118.15 (P3(a9,a9)),
% 117.43/118.15 inference(scs_inference,[],[1757,104,100])).
% 117.43/118.15 cnf(1766,plain,
% 117.43/118.15 (~P6(a62,x17661,a85)),
% 117.43/118.15 inference(scs_inference,[],[11,15,31])).
% 117.43/118.15 cnf(1775,plain,
% 117.43/118.15 (P6(a58,a65,a84)),
% 117.43/118.15 inference(scs_inference,[],[4,14,15,41])).
% 117.43/118.15 cnf(1778,plain,
% 117.43/118.15 (~P5(a84,a84)),
% 117.43/118.15 inference(scs_inference,[],[1775,105,104])).
% 117.43/118.15 cnf(1780,plain,
% 117.43/118.15 (P3(a84,a84)),
% 117.43/118.15 inference(scs_inference,[],[1775,105,104,100])).
% 117.43/118.15 cnf(1786,plain,
% 117.43/118.15 (~P6(a62,x17861,a73)),
% 117.43/118.15 inference(scs_inference,[],[11,15,32])).
% 117.43/118.15 cnf(1795,plain,
% 117.43/118.15 (~P6(a62,a3,a10)),
% 117.43/118.15 inference(scs_inference,[],[11,8,15,44])).
% 117.43/118.15 cnf(1806,plain,
% 117.43/118.15 (P6(a65,a3,a82)),
% 117.43/118.15 inference(scs_inference,[],[4,8,15,77])).
% 117.43/118.15 cnf(1807,plain,
% 117.43/118.15 (~P5(a82,a82)),
% 117.43/118.15 inference(scs_inference,[],[1806,104])).
% 117.43/118.15 cnf(1809,plain,
% 117.43/118.15 (P3(a82,a82)),
% 117.43/118.15 inference(scs_inference,[],[1806,104,100])).
% 117.43/118.15 cnf(1815,plain,
% 117.43/118.15 (~P6(a3,a62,a10)),
% 117.43/118.15 inference(scs_inference,[],[11,8,15,46])).
% 117.43/118.15 cnf(1816,plain,
% 117.43/118.15 (~P6(a3,a62,x18161)+P4(x18161,a10)),
% 117.43/118.15 inference(scs_inference,[],[1815,91])).
% 117.43/118.15 cnf(1863,plain,
% 117.43/118.15 (~P6(f49(x18631,a10),f50(x18631,a10),a10)+~P6(a3,a62,x18631)),
% 117.43/118.15 inference(scs_inference,[],[1816,102])).
% 117.43/118.15 cnf(1972,plain,
% 117.43/118.15 (~P6(a58,a65,a87)),
% 117.43/118.15 inference(scs_inference,[],[4,14,15,78])).
% 117.43/118.15 cnf(1977,plain,
% 117.43/118.15 (~P6(a65,a58,a81)),
% 117.43/118.15 inference(scs_inference,[],[4,14,15,79])).
% 117.43/118.15 cnf(1984,plain,
% 117.43/118.15 (P6(a58,a62,a89)),
% 117.43/118.15 inference(scs_inference,[],[11,14,4,15,74])).
% 117.43/118.15 cnf(1987,plain,
% 117.43/118.15 (~P5(a89,a89)),
% 117.43/118.15 inference(scs_inference,[],[1984,105,104])).
% 117.43/118.15 cnf(1989,plain,
% 117.43/118.15 (P3(a89,a89)),
% 117.43/118.15 inference(scs_inference,[],[1984,105,104,100])).
% 117.43/118.15 cnf(1995,plain,
% 117.43/118.15 (P6(a65,a3,a88)),
% 117.43/118.15 inference(scs_inference,[],[4,8,11,15,90])).
% 117.43/118.15 cnf(1996,plain,
% 117.43/118.15 (~P5(a88,a88)),
% 117.43/118.15 inference(scs_inference,[],[1995,104])).
% 117.43/118.15 cnf(1998,plain,
% 117.43/118.15 (P3(a88,a88)),
% 117.43/118.15 inference(scs_inference,[],[1995,104,100])).
% 117.43/118.15 cnf(2009,plain,
% 117.43/118.15 (~P1(f26(a65,a3),a62)),
% 117.43/118.15 inference(scs_inference,[],[1995,15,84])).
% 117.43/118.15 cnf(2014,plain,
% 117.43/118.15 (P6(a62,a3,a88)),
% 117.43/118.15 inference(scs_inference,[],[11,8,4,15,90])).
% 117.43/118.15 cnf(2031,plain,
% 117.43/118.15 (P6(a58,a65,a89)),
% 117.43/118.15 inference(scs_inference,[],[4,14,11,15,74])).
% 117.43/118.15 cnf(2035,plain,
% 117.43/118.15 (~P1(f19(a62,a3),a62)),
% 117.43/118.15 inference(scs_inference,[],[11,8,1331,4,15,107])).
% 117.43/118.15 cnf(2039,plain,
% 117.43/118.15 (~P1(f39(a58,a65),a62)),
% 117.43/118.15 inference(scs_inference,[],[2031,15,87])).
% 117.43/118.15 cnf(2092,plain,
% 117.43/118.15 (~P6(a59,a3,a10)+~P1(a63,a56)),
% 117.43/118.15 inference(scs_inference,[],[8,18,44])).
% 117.43/118.15 cnf(2096,plain,
% 117.43/118.15 (~P2(a74,a10)+~P1(a63,a56)),
% 117.43/118.15 inference(scs_inference,[],[122,2092,94])).
% 117.43/118.15 cnf(2139,plain,
% 117.43/118.15 (~P6(a56,a3,a76)+~P1(a64,a59)),
% 117.43/118.15 inference(scs_inference,[],[8,18,45])).
% 117.43/118.15 cnf(2144,plain,
% 117.43/118.15 (~P2(a74,a76)+~P1(a64,a59)),
% 117.43/118.15 inference(scs_inference,[],[122,2139,94])).
% 117.43/118.15 cnf(2362,plain,
% 117.43/118.15 (P1(x23621,f75(a58))),
% 117.43/118.15 inference(rename_variables,[],[604])).
% 117.43/118.15 cnf(2366,plain,
% 117.43/118.15 (P1(x23661,f75(a58))),
% 117.43/118.15 inference(rename_variables,[],[604])).
% 117.43/118.15 cnf(2369,plain,
% 117.43/118.15 (P1(x23691,f75(a58))),
% 117.43/118.15 inference(rename_variables,[],[604])).
% 117.43/118.15 cnf(2370,plain,
% 117.43/118.15 (P1(x23701,f75(a58))),
% 117.43/118.15 inference(rename_variables,[],[604])).
% 117.43/118.15 cnf(2372,plain,
% 117.43/118.15 (P6(f75(a58),a58,a73)),
% 117.43/118.15 inference(scs_inference,[],[14,604,2362,2366,2370,2369,678,98,93,106,101])).
% 117.43/118.15 cnf(3231,plain,
% 117.43/118.15 (~P5(a86,a5)),
% 117.43/118.15 inference(scs_inference,[],[194,110,104])).
% 117.43/118.15 cnf(3232,plain,
% 117.43/118.15 (P6(a58,x32321,a5)),
% 117.43/118.15 inference(rename_variables,[],[110])).
% 117.43/118.15 cnf(3234,plain,
% 117.43/118.15 (P3(a86,a5)),
% 117.43/118.15 inference(scs_inference,[],[194,110,3232,104,100])).
% 117.43/118.15 cnf(3244,plain,
% 117.43/118.15 (~P5(a86,a74)),
% 117.43/118.15 inference(scs_inference,[],[194,122,104])).
% 117.43/118.15 cnf(3245,plain,
% 117.43/118.15 (P6(x32451,a3,a74)),
% 117.43/118.15 inference(rename_variables,[],[122])).
% 117.43/118.15 cnf(3247,plain,
% 117.43/118.15 (P3(a86,a74)),
% 117.43/118.15 inference(scs_inference,[],[194,122,3245,104,100])).
% 117.43/118.15 cnf(3256,plain,
% 117.43/118.15 (~P5(a86,a81)),
% 117.43/118.15 inference(scs_inference,[],[194,116,104])).
% 117.43/118.15 cnf(3257,plain,
% 117.43/118.15 (P6(a58,x32571,a81)),
% 117.43/118.15 inference(rename_variables,[],[116])).
% 117.43/118.15 cnf(3259,plain,
% 117.43/118.15 (P3(a86,a81)),
% 117.43/118.15 inference(scs_inference,[],[194,116,3257,104,100])).
% 117.43/118.15 cnf(3308,plain,
% 117.43/118.15 (~P5(a10,a74)),
% 117.43/118.15 inference(scs_inference,[],[210,122,104])).
% 117.43/118.15 cnf(3309,plain,
% 117.43/118.15 (P6(x33091,a3,a74)),
% 117.43/118.15 inference(rename_variables,[],[122])).
% 117.43/118.15 cnf(3311,plain,
% 117.43/118.15 (P3(a10,a74)),
% 117.43/118.15 inference(scs_inference,[],[210,122,3309,104,100])).
% 117.43/118.15 cnf(3319,plain,
% 117.43/118.15 (~P5(a85,a74)),
% 117.43/118.15 inference(scs_inference,[],[214,122,104])).
% 117.43/118.15 cnf(3320,plain,
% 117.43/118.15 (P6(x33201,a3,a74)),
% 117.43/118.15 inference(rename_variables,[],[122])).
% 117.43/118.15 cnf(3322,plain,
% 117.43/118.15 (P3(a85,a74)),
% 117.43/118.15 inference(scs_inference,[],[214,122,3320,104,100])).
% 117.43/118.15 cnf(3523,plain,
% 117.43/118.15 (~P2(a87,a76)),
% 117.43/118.15 inference(scs_inference,[],[1708,1519,1351,94])).
% 117.43/118.15 cnf(3549,plain,
% 117.43/118.15 (~P2(a74,a10)+~P6(a56,a3,a10)),
% 117.43/118.15 inference(scs_inference,[],[8,2096,44])).
% 117.43/118.15 cnf(3550,plain,
% 117.43/118.15 (~P2(a74,a10)),
% 117.43/118.15 inference(scs_inference,[],[122,3549,94])).
% 117.43/118.15 cnf(3551,plain,
% 117.43/118.15 (~P2(a74,a76)+~P6(a59,a3,a76)),
% 117.43/118.15 inference(scs_inference,[],[8,2144,45])).
% 117.43/118.15 cnf(3552,plain,
% 117.43/118.15 (~P2(a74,a76)),
% 117.43/118.15 inference(scs_inference,[],[122,3551,94])).
% 117.43/118.15 cnf(3589,plain,
% 117.43/118.15 (~P5(a73,a87)),
% 117.43/118.15 inference(scs_inference,[],[638,113,104])).
% 117.43/118.15 cnf(3590,plain,
% 117.43/118.15 (P6(x35901,a58,a87)),
% 117.43/118.15 inference(rename_variables,[],[113])).
% 117.43/118.15 cnf(3592,plain,
% 117.43/118.15 (P3(a73,a87)),
% 117.43/118.15 inference(scs_inference,[],[638,113,3590,104,100])).
% 117.43/118.15 cnf(4418,plain,
% 117.43/118.15 (P6(f48(a5,a5),f48(a85,a85),a86)),
% 117.43/118.15 inference(scs_inference,[],[678,668,953,80,93])).
% 117.43/118.15 cnf(4420,plain,
% 117.43/118.15 (P1(x44201,f48(a85,a85))),
% 117.43/118.15 inference(rename_variables,[],[678])).
% 117.43/118.15 cnf(4422,plain,
% 117.43/118.15 (P6(f75(a58),f48(a85,a85),a85)),
% 117.43/118.15 inference(scs_inference,[],[678,4420,668,953,604,80,93,98])).
% 117.43/118.15 cnf(4424,plain,
% 117.43/118.15 (P1(x44241,f48(a85,a85))),
% 117.43/118.15 inference(rename_variables,[],[678])).
% 117.43/118.15 cnf(4426,plain,
% 117.43/118.15 (P6(f48(a85,a85),f48(a85,a85),a10)),
% 117.43/118.15 inference(scs_inference,[],[678,4420,4424,668,953,604,80,93,98,106])).
% 117.43/118.15 cnf(4431,plain,
% 117.43/118.15 (P6(f45(a5,a5),f48(a85,a85),a86)),
% 117.43/118.15 inference(scs_inference,[],[678,799,93])).
% 117.43/118.15 cnf(4445,plain,
% 117.43/118.15 (P6(f46(a73,a73),f48(a85,a85),a86)),
% 117.43/118.15 inference(scs_inference,[],[678,953,93])).
% 117.43/118.15 cnf(4447,plain,
% 117.43/118.15 (P1(x44471,f48(a85,a85))),
% 117.43/118.15 inference(rename_variables,[],[678])).
% 117.43/118.15 cnf(4449,plain,
% 117.43/118.15 (P6(f48(a85,a85),f75(a58),a10)),
% 117.43/118.15 inference(scs_inference,[],[678,4447,953,604,93,106])).
% 117.43/118.15 cnf(4482,plain,
% 117.43/118.15 (P3(a8,a5)),
% 117.43/118.15 inference(scs_inference,[],[754,110,100])).
% 117.43/118.15 cnf(4483,plain,
% 117.43/118.15 (P6(a58,x44831,a5)),
% 117.43/118.15 inference(rename_variables,[],[110])).
% 117.43/118.15 cnf(4485,plain,
% 117.43/118.15 (~P5(a8,a5)),
% 117.43/118.15 inference(scs_inference,[],[754,110,4483,100,104])).
% 117.43/118.15 cnf(4495,plain,
% 117.43/118.15 (~P5(a8,a74)),
% 117.43/118.15 inference(scs_inference,[],[754,119,104])).
% 117.43/118.15 cnf(4496,plain,
% 117.43/118.15 (P6(a58,x44961,a74)),
% 117.43/118.15 inference(rename_variables,[],[119])).
% 117.43/118.15 cnf(4498,plain,
% 117.43/118.15 (P3(a8,a74)),
% 117.43/118.15 inference(scs_inference,[],[754,119,4496,104,100])).
% 117.43/118.15 cnf(4508,plain,
% 117.43/118.15 (P3(a8,a87)),
% 117.43/118.15 inference(scs_inference,[],[754,736,100])).
% 117.43/118.15 cnf(4509,plain,
% 117.43/118.15 (P6(x45091,f48(a5,a5),a87)),
% 117.43/118.15 inference(rename_variables,[],[736])).
% 117.43/118.15 cnf(4511,plain,
% 117.43/118.15 (~P5(a8,a87)),
% 117.43/118.15 inference(scs_inference,[],[754,736,4509,100,104])).
% 117.43/118.15 cnf(4909,plain,
% 117.43/118.15 (~P6(x49091,a71,a82)),
% 117.43/118.15 inference(scs_inference,[],[190,236,240,1661,12,50,51,52,69,70,99,102,27])).
% 117.43/118.15 cnf(4911,plain,
% 117.43/118.15 (~P6(a2,x49111,a84)),
% 117.43/118.15 inference(scs_inference,[],[1,190,236,240,1661,12,50,51,52,69,70,99,102,27,37])).
% 117.43/118.15 cnf(4913,plain,
% 117.43/118.15 (~P6(a2,x49131,a89)),
% 117.43/118.15 inference(scs_inference,[],[1,190,236,240,1661,12,50,51,52,69,70,99,102,27,37,39])).
% 117.43/118.15 cnf(4915,plain,
% 117.43/118.15 (~P6(x49151,a71,a88)),
% 117.43/118.15 inference(scs_inference,[],[1,190,236,240,1661,12,50,51,52,69,70,99,102,27,37,39,29])).
% 117.43/118.15 cnf(4917,plain,
% 117.43/118.15 (~P6(a71,x49171,a73)),
% 117.43/118.15 inference(scs_inference,[],[1,190,236,240,1661,12,50,51,52,69,70,99,102,27,37,39,29,32])).
% 117.43/118.15 cnf(4919,plain,
% 117.43/118.15 (~P6(a2,x49191,a86)),
% 117.43/118.15 inference(scs_inference,[],[1,190,236,240,1661,12,50,51,52,69,70,99,102,27,37,39,29,32,38])).
% 117.43/118.15 cnf(4921,plain,
% 117.43/118.15 (P6(a2,x49211,a87)),
% 117.43/118.15 inference(scs_inference,[],[1,190,236,240,1661,12,50,51,52,69,70,99,102,27,37,39,29,32,38,23])).
% 117.43/118.15 cnf(4923,plain,
% 117.43/118.15 (~P6(a71,x49231,a85)),
% 117.43/118.15 inference(scs_inference,[],[1,190,236,240,1661,12,50,51,52,69,70,99,102,27,37,39,29,32,38,23,31])).
% 117.43/118.15 cnf(4925,plain,
% 117.43/118.15 (~P6(x49251,a71,a86)),
% 117.43/118.15 inference(scs_inference,[],[1,190,236,240,1661,12,50,51,52,69,70,99,102,27,37,39,29,32,38,23,31,30])).
% 117.43/118.15 cnf(4927,plain,
% 117.43/118.15 (P6(x49271,a2,a81)),
% 117.43/118.15 inference(scs_inference,[],[1,190,236,240,1661,12,50,51,52,69,70,99,102,27,37,39,29,32,38,23,31,30,22])).
% 117.43/118.15 cnf(4929,plain,
% 117.43/118.15 (~P1(a1,f75(a2))),
% 117.43/118.15 inference(scs_inference,[],[1,190,236,240,1661,12,50,51,52,69,70,99,102,27,37,39,29,32,38,23,31,30,22,20])).
% 117.43/118.15 cnf(4933,plain,
% 117.43/118.15 (P1(f20(a62,a3),a62)),
% 117.43/118.15 inference(scs_inference,[],[1,190,236,240,1661,12,2014,50,51,52,69,70,99,102,27,37,39,29,32,38,23,31,30,22,20,71,60])).
% 117.43/118.15 cnf(4935,plain,
% 117.43/118.15 (~P1(f26(a62,a3),a62)),
% 117.43/118.15 inference(scs_inference,[],[1,190,236,240,1661,12,2014,50,51,52,69,70,99,102,27,37,39,29,32,38,23,31,30,22,20,71,60,84])).
% 117.43/118.15 cnf(4937,plain,
% 117.43/118.15 (~P6(x49371,a71,a85)),
% 117.43/118.15 inference(scs_inference,[],[1,190,236,240,1661,12,2014,50,51,52,69,70,99,102,27,37,39,29,32,38,23,31,30,22,20,71,60,84,28])).
% 117.43/118.15 cnf(4941,plain,
% 117.43/118.15 (~P1(f39(a58,a65),a65)),
% 117.43/118.15 inference(scs_inference,[],[1,190,236,240,1661,12,1972,2014,2031,50,51,52,69,70,99,102,27,37,39,29,32,38,23,31,30,22,20,71,60,84,28,24,87])).
% 117.43/118.15 cnf(4943,plain,
% 117.43/118.15 (P1(f38(a65,a58),a65)),
% 117.43/118.15 inference(scs_inference,[],[1,190,236,240,1661,12,1972,2014,2031,1757,50,51,52,69,70,99,102,27,37,39,29,32,38,23,31,30,22,20,71,60,84,28,24,87,65])).
% 117.43/118.15 cnf(4947,plain,
% 117.43/118.15 (~P6(a2,x49471,a5)),
% 117.43/118.15 inference(scs_inference,[],[1,190,236,240,1661,12,1972,2014,2031,1757,1806,50,51,52,69,70,99,102,27,37,39,29,32,38,23,31,30,22,20,71,60,84,28,24,87,65,56,36])).
% 117.43/118.15 cnf(4967,plain,
% 117.43/118.15 (~P2(a85,a89)),
% 117.43/118.15 inference(scs_inference,[],[1,125,190,236,240,463,1661,10,12,4422,1703,1972,1977,2014,2031,727,1757,1806,460,1775,1708,50,51,52,69,70,99,102,27,37,39,29,32,38,23,31,30,22,20,71,60,84,28,24,87,65,56,36,63,25,64,21,17,45,47,48,49,94])).
% 117.43/118.15 cnf(4970,plain,
% 117.43/118.15 (~P1(f14(a2,a62),a62)),
% 117.43/118.15 inference(scs_inference,[],[1,125,190,236,240,463,1661,10,12,4422,1703,1717,1972,1977,2014,2031,727,1757,1806,460,1775,1708,50,51,52,69,70,99,102,27,37,39,29,32,38,23,31,30,22,20,71,60,84,28,24,87,65,56,36,63,25,64,21,17,45,47,48,49,94,77])).
% 117.43/118.15 cnf(4985,plain,
% 117.43/118.15 (~P6(f75(a65),a65,a10)),
% 117.43/118.15 inference(scs_inference,[],[1,125,190,236,240,463,1661,10,12,4422,1703,1717,1718,1972,1977,2014,2031,727,1757,1806,460,1775,506,1519,1708,953,50,51,52,69,70,99,102,27,37,39,29,32,38,23,31,30,22,20,71,60,84,28,24,87,65,56,36,63,25,64,21,17,45,47,48,49,94,77,78,79,41,46,44])).
% 117.43/118.15 cnf(4991,plain,
% 117.43/118.16 (P1(f60(a59,a58),a59)),
% 117.43/118.16 inference(scs_inference,[],[1,125,190,236,240,463,1661,10,12,4422,1703,1717,544,1718,1972,1977,2014,2031,727,1757,1806,460,1775,506,1519,1708,953,14,50,51,52,69,70,99,102,27,37,39,29,32,38,23,31,30,22,20,71,60,84,28,24,87,65,56,36,63,25,64,21,17,45,47,48,49,94,77,78,79,41,46,44,34,43,76])).
% 117.43/118.16 cnf(4992,plain,
% 117.43/118.16 (~P1(x49921,a58)),
% 117.43/118.16 inference(rename_variables,[],[14])).
% 117.43/118.16 cnf(4994,plain,
% 117.43/118.16 (P3(a74,a86)),
% 117.43/118.16 inference(scs_inference,[],[1,125,190,236,240,463,1661,10,12,4422,4418,1703,1717,703,544,1718,1972,1977,2014,2031,727,1757,1806,460,1775,506,1519,1708,953,14,50,51,52,69,70,99,102,27,37,39,29,32,38,23,31,30,22,20,71,60,84,28,24,87,65,56,36,63,25,64,21,17,45,47,48,49,94,77,78,79,41,46,44,34,43,76,100])).
% 117.43/118.16 cnf(4995,plain,
% 117.43/118.16 (P6(f48(a5,a5),x49951,a74)),
% 117.43/118.16 inference(rename_variables,[],[703])).
% 117.43/118.16 cnf(4997,plain,
% 117.43/118.16 (~P5(a74,a86)),
% 117.43/118.16 inference(scs_inference,[],[1,125,190,236,240,463,1661,10,12,4422,4418,1703,1717,703,4995,544,1718,1972,1977,2014,2031,727,1757,1806,460,1775,506,1519,1708,953,14,50,51,52,69,70,99,102,27,37,39,29,32,38,23,31,30,22,20,71,60,84,28,24,87,65,56,36,63,25,64,21,17,45,47,48,49,94,77,78,79,41,46,44,34,43,76,100,104])).
% 117.43/118.16 cnf(4998,plain,
% 117.43/118.16 (P6(f48(a5,a5),x49981,a74)),
% 117.43/118.16 inference(rename_variables,[],[703])).
% 117.43/118.16 cnf(5001,plain,
% 117.43/118.16 (P1(x50011,a3)),
% 117.43/118.16 inference(rename_variables,[],[8])).
% 117.43/118.16 cnf(5004,plain,
% 117.43/118.16 (~P1(f40(a62,a58),a62)),
% 117.43/118.16 inference(scs_inference,[],[1,125,190,236,240,463,1661,10,12,4422,4418,1703,1717,703,4995,544,1718,1786,1972,1977,2014,2031,727,1757,1806,460,1775,1730,506,1519,1708,953,14,8,604,50,51,52,69,70,99,102,27,37,39,29,32,38,23,31,30,22,20,71,60,84,28,24,87,65,56,36,63,25,64,21,17,45,47,48,49,94,77,78,79,41,46,44,34,43,76,100,104,93,101])).
% 117.43/118.16 cnf(5008,plain,
% 117.43/118.16 (P6(a2,a2,a8)),
% 117.43/118.16 inference(scs_inference,[],[1,125,190,236,240,463,1661,10,12,4422,4418,1703,1717,703,4995,544,1718,1786,1972,1977,2014,2031,727,1757,1806,460,1775,1730,506,1519,1708,953,14,8,604,50,51,52,69,70,99,102,27,37,39,29,32,38,23,31,30,22,20,71,60,84,28,24,87,65,56,36,63,25,64,21,17,45,47,48,49,94,77,78,79,41,46,44,34,43,76,100,104,93,101,33])).
% 117.43/118.16 cnf(5010,plain,
% 117.43/118.16 (~P1(f23(a62,a3),a62)),
% 117.43/118.16 inference(scs_inference,[],[1,125,190,236,240,463,1661,10,12,4422,4418,1703,1717,703,4995,544,1718,1786,1972,1977,2014,2031,727,1757,1806,460,1775,1766,1730,506,1519,1708,953,14,8,5001,604,50,51,52,69,70,99,102,27,37,39,29,32,38,23,31,30,22,20,71,60,84,28,24,87,65,56,36,63,25,64,21,17,45,47,48,49,94,77,78,79,41,46,44,34,43,76,100,104,93,101,33,98])).
% 117.43/118.16 cnf(5011,plain,
% 117.43/118.16 (P1(x50111,a3)),
% 117.43/118.16 inference(rename_variables,[],[8])).
% 117.43/118.16 cnf(5019,plain,
% 117.43/118.16 (~P1(f22(a2,a62),a62)),
% 117.43/118.16 inference(scs_inference,[],[1,125,190,236,240,463,1661,10,12,4422,4418,1703,1717,1739,2372,703,4995,4998,544,1718,1786,1972,1977,2014,2031,727,9,1757,1806,460,1775,1766,1730,506,1519,1708,13,953,14,8,5001,604,50,51,52,69,70,99,102,27,37,39,29,32,38,23,31,30,22,20,71,60,84,28,24,87,65,56,36,63,25,64,21,17,45,47,48,49,94,77,78,79,41,46,44,34,43,76,100,104,93,101,33,98,105,91,90])).
% 117.43/118.16 cnf(5025,plain,
% 117.43/118.16 (~P1(f12(a3,a62),a62)),
% 117.43/118.16 inference(scs_inference,[],[1,125,190,236,240,463,1661,10,12,4422,4418,1703,1717,1739,2372,703,4995,4998,544,1718,1744,1786,1972,1977,2014,2031,727,9,1757,1806,460,1815,1775,1766,1730,506,1519,1708,13,953,14,8,5001,5011,604,50,51,52,69,70,99,102,27,37,39,29,32,38,23,31,30,22,20,71,60,84,28,24,87,65,56,36,63,25,64,21,17,45,47,48,49,94,77,78,79,41,46,44,34,43,76,100,104,93,101,33,98,105,91,90,74,106])).
% 117.43/118.16 cnf(5026,plain,
% 117.43/118.16 (P1(x50261,a3)),
% 117.43/118.16 inference(rename_variables,[],[8])).
% 117.43/118.16 cnf(5027,plain,
% 117.43/118.16 (P1(x50271,a3)),
% 117.43/118.16 inference(rename_variables,[],[8])).
% 117.43/118.16 cnf(5029,plain,
% 117.43/118.16 (~P6(a2,a58,a76)),
% 117.43/118.16 inference(scs_inference,[],[1,125,190,236,240,463,1661,10,12,4422,4418,1703,1717,1739,2372,703,4995,4998,544,1718,1744,1786,1972,1977,2014,2031,727,9,1757,1806,460,1815,1775,1766,1730,506,1519,1708,13,953,14,8,5001,5011,604,50,51,52,69,70,99,102,27,37,39,29,32,38,23,31,30,22,20,71,60,84,28,24,87,65,56,36,63,25,64,21,17,45,47,48,49,94,77,78,79,41,46,44,34,43,76,100,104,93,101,33,98,105,91,90,74,106,1341])).
% 117.43/118.16 cnf(5031,plain,
% 117.43/118.16 (P1(f77(a2,a2),a2)),
% 117.43/118.16 inference(scs_inference,[],[1,125,190,236,240,463,1661,10,12,4422,4418,1703,1717,1739,2372,703,4995,4998,544,1718,1744,1786,1972,1977,2014,2031,727,9,1757,1806,460,1815,1775,1766,1730,506,1519,1708,13,953,14,8,5001,5011,604,50,51,52,69,70,99,102,27,37,39,29,32,38,23,31,30,22,20,71,60,84,28,24,87,65,56,36,63,25,64,21,17,45,47,48,49,94,77,78,79,41,46,44,34,43,76,100,104,93,101,33,98,105,91,90,74,106,1341,53])).
% 117.43/118.16 cnf(5039,plain,
% 117.43/118.16 (P1(f19(a2,a58),a2)),
% 117.43/118.16 inference(scs_inference,[],[1,125,190,236,240,463,1661,10,12,4422,4418,1703,1717,1739,2372,703,4995,4998,544,1718,1744,1786,1972,1977,2014,2031,727,9,1757,1806,460,1815,5,1775,1766,1730,506,1519,1708,13,4,953,14,4992,8,5001,5011,604,50,51,52,69,70,99,102,27,37,39,29,32,38,23,31,30,22,20,71,60,84,28,24,87,65,56,36,63,25,64,21,17,45,47,48,49,94,77,78,79,41,46,44,34,43,76,100,104,93,101,33,98,105,91,90,74,106,1341,53,81,80,88,96])).
% 117.43/118.16 cnf(5042,plain,
% 117.43/118.16 (P6(a2,a3,a90)),
% 117.43/118.16 inference(scs_inference,[],[1,125,190,236,240,463,1661,10,12,4422,4418,1703,1717,1739,2372,703,4995,4998,544,1718,1744,1786,1972,1977,2014,2031,727,9,1757,1806,460,1815,5,1775,1766,1730,506,1519,1708,13,4,953,14,4992,8,5001,5011,5027,5026,604,50,51,52,69,70,99,102,27,37,39,29,32,38,23,31,30,22,20,71,60,84,28,24,87,65,56,36,63,25,64,21,17,45,47,48,49,94,77,78,79,41,46,44,34,43,76,100,104,93,101,33,98,105,91,90,74,106,1341,53,81,80,88,96,97])).
% 117.43/118.16 cnf(5057,plain,
% 117.43/118.16 (~P6(a62,x50571,a84)),
% 117.43/118.16 inference(scs_inference,[],[278,4933,51,37])).
% 117.43/118.16 cnf(5065,plain,
% 117.43/118.16 (~P6(x50651,a65,a82)),
% 117.43/118.16 inference(scs_inference,[],[244,278,285,3550,4933,4941,51,37,99,69,102,27])).
% 117.43/118.16 cnf(5067,plain,
% 117.43/118.16 (~P6(x50671,a65,a88)),
% 117.43/118.16 inference(scs_inference,[],[244,278,285,3550,4933,4941,51,37,99,69,102,27,29])).
% 117.43/118.16 cnf(5071,plain,
% 117.43/118.16 (~P6(a62,x50711,a86)),
% 117.43/118.16 inference(scs_inference,[],[244,278,285,304,3550,4933,4941,51,37,99,69,102,27,29,52,38])).
% 117.43/118.16 cnf(5075,plain,
% 117.43/118.16 (~P6(a65,x50751,a73)),
% 117.43/118.16 inference(scs_inference,[],[244,278,285,304,3550,4933,4941,51,37,99,69,102,27,29,52,38,50,32])).
% 117.43/118.16 cnf(5077,plain,
% 117.43/118.16 (~P6(a62,x50771,a89)),
% 117.43/118.16 inference(scs_inference,[],[244,278,285,304,3550,4933,4941,51,37,99,69,102,27,29,52,38,50,32,39])).
% 117.43/118.16 cnf(5081,plain,
% 117.43/118.16 (P6(a62,x50811,a87)),
% 117.43/118.16 inference(scs_inference,[],[244,278,285,301,304,3550,4933,4941,51,37,99,69,102,27,29,52,38,50,32,39,70,23])).
% 117.43/118.16 cnf(5083,plain,
% 117.43/118.16 (~P6(a65,x50831,a85)),
% 117.43/118.16 inference(scs_inference,[],[244,278,285,301,304,3550,4933,4941,51,37,99,69,102,27,29,52,38,50,32,39,70,23,31])).
% 117.43/118.16 cnf(5087,plain,
% 117.43/118.16 (~P1(f77(a2,a2),f75(a2))),
% 117.43/118.16 inference(scs_inference,[],[244,278,285,301,304,3550,5031,4933,4941,51,37,99,69,102,27,29,52,38,50,32,39,70,23,31,30,20])).
% 117.43/118.16 cnf(5089,plain,
% 117.43/118.16 (P6(x50891,a62,a81)),
% 117.43/118.16 inference(scs_inference,[],[244,278,285,301,304,3550,5031,4933,4941,51,37,99,69,102,27,29,52,38,50,32,39,70,23,31,30,20,22])).
% 117.43/118.16 cnf(5093,plain,
% 117.43/118.16 (~P1(f26(a65,a3),a65)),
% 117.43/118.16 inference(scs_inference,[],[244,278,285,301,304,3550,5031,4933,4941,1995,51,37,99,69,102,27,29,52,38,50,32,39,70,23,31,30,20,22,71,84])).
% 117.43/118.16 cnf(5097,plain,
% 117.43/118.16 (~P6(x50971,a65,a85)),
% 117.43/118.16 inference(scs_inference,[],[244,278,285,301,304,3550,5031,4933,4941,1995,51,37,99,69,102,27,29,52,38,50,32,39,70,23,31,30,20,22,71,84,60,28])).
% 117.43/118.16 cnf(5099,plain,
% 117.43/118.16 (~P1(f17(a2,a3),a2)),
% 117.43/118.16 inference(scs_inference,[],[244,278,285,301,304,3550,5042,5031,4933,4941,1995,51,37,99,69,102,27,29,52,38,50,32,39,70,23,31,30,20,22,71,84,60,28,82])).
% 117.43/118.16 cnf(5103,plain,
% 117.43/118.16 (~P1(f39(a58,a62),a62)),
% 117.43/118.16 inference(scs_inference,[],[244,278,285,301,304,3550,5042,5031,4933,4941,1995,1984,51,37,99,69,102,27,29,52,38,50,32,39,70,23,31,30,20,22,71,84,60,28,82,57,87])).
% 117.43/118.16 cnf(5105,plain,
% 117.43/118.16 (~P6(a62,x51051,a5)),
% 117.43/118.16 inference(scs_inference,[],[244,278,285,301,304,3550,5042,5031,4933,4941,1995,1984,51,37,99,69,102,27,29,52,38,50,32,39,70,23,31,30,20,22,71,84,60,28,82,57,87,36])).
% 117.43/118.16 cnf(5107,plain,
% 117.43/118.16 (P1(f34(a58,a62),a62)),
% 117.43/118.16 inference(scs_inference,[],[244,278,285,301,304,3550,5042,5031,4933,4941,1995,1984,51,37,99,69,102,27,29,52,38,50,32,39,70,23,31,30,20,22,71,84,60,28,82,57,87,36,64])).
% 117.43/118.16 cnf(5111,plain,
% 117.43/118.16 (P1(f39(a58,a65),f75(a65))),
% 117.43/118.16 inference(scs_inference,[],[244,278,285,301,304,3550,4947,5042,5031,4933,4941,1995,1984,51,37,99,69,102,27,29,52,38,50,32,39,70,23,31,30,20,22,71,84,60,28,82,57,87,36,64,21,17])).
% 117.43/118.16 cnf(5118,plain,
% 117.43/118.16 (~P2(a87,a82)),
% 117.43/118.16 inference(scs_inference,[],[1,244,278,285,301,304,3550,4909,4921,4927,4947,5042,5031,4933,4941,4929,1995,1984,51,37,99,69,102,27,29,52,38,50,32,39,70,23,31,30,20,22,71,84,60,28,82,57,87,36,64,21,17,47,79,94])).
% 117.43/118.16 cnf(5119,plain,
% 117.43/118.16 (P6(a2,x51191,a87)),
% 117.43/118.16 inference(rename_variables,[],[4921])).
% 117.43/118.16 cnf(5120,plain,
% 117.43/118.16 (~P6(x51201,a71,a82)),
% 117.43/118.16 inference(rename_variables,[],[4909])).
% 117.43/118.16 cnf(5134,plain,
% 117.43/118.16 (~P1(f14(a2,a71),a71)),
% 117.43/118.16 inference(scs_inference,[],[1,244,278,285,301,304,3550,4909,5120,4911,4921,5119,4927,4947,5042,5031,4933,4941,4929,1995,1984,51,37,99,69,102,27,29,52,38,50,32,39,70,23,31,30,20,22,71,84,60,28,82,57,87,36,64,21,17,47,79,94,48,41,49,45,78,77])).
% 117.43/118.16 cnf(5135,plain,
% 117.43/118.16 (~P6(x51351,a71,a82)),
% 117.43/118.16 inference(rename_variables,[],[4909])).
% 117.43/118.16 cnf(5145,plain,
% 117.43/118.16 (~P1(x51451,f46(a73,a73))),
% 117.43/118.16 inference(rename_variables,[],[953])).
% 117.43/118.16 cnf(5159,plain,
% 117.43/118.16 (~P1(f40(a71,a58),a71)),
% 117.43/118.16 inference(scs_inference,[],[1,244,278,285,301,304,3550,4909,5120,5135,4911,4917,4919,4921,5119,4927,4947,5042,5031,4933,4941,4929,547,1995,1984,678,953,5145,14,604,51,37,99,69,102,27,29,52,38,50,32,39,70,23,31,30,20,22,71,84,60,28,82,57,87,36,64,21,17,47,79,94,48,41,49,45,78,77,46,44,34,81,43,76,75,80,101])).
% 117.43/118.16 cnf(5163,plain,
% 117.43/118.16 (P6(a62,a62,a8)),
% 117.43/118.16 inference(scs_inference,[],[1,244,278,285,301,304,3550,4909,5120,5135,4911,4917,4919,4921,5119,4927,4947,5042,5031,4933,4941,4929,547,1995,1984,678,953,5145,14,604,51,37,99,69,102,27,29,52,38,50,32,39,70,23,31,30,20,22,71,84,60,28,82,57,87,36,64,21,17,47,79,94,48,41,49,45,78,77,46,44,34,81,43,76,75,80,101,33])).
% 117.43/118.16 cnf(5165,plain,
% 117.43/118.16 (~P1(f22(a2,a71),a71)),
% 117.43/118.16 inference(scs_inference,[],[1,244,278,285,301,304,3550,4909,5120,5135,4911,4915,4917,4919,4921,5119,4927,4947,5042,5031,4933,4941,4929,547,1995,1984,9,678,953,5145,14,604,51,37,99,69,102,27,29,52,38,50,32,39,70,23,31,30,20,22,71,84,60,28,82,57,87,36,64,21,17,47,79,94,48,41,49,45,78,77,46,44,34,81,43,76,75,80,101,33,90])).
% 117.43/118.16 cnf(5171,plain,
% 117.43/118.16 (~P1(f12(a62,a3),a62)),
% 117.43/118.16 inference(scs_inference,[],[1,244,278,285,301,304,3550,4909,5120,5135,4911,4913,4915,4917,4919,4921,5119,4927,4947,5042,5031,4933,4941,4929,1795,547,1995,1984,9,678,953,5145,14,8,604,51,37,99,69,102,27,29,52,38,50,32,39,70,23,31,30,20,22,71,84,60,28,82,57,87,36,64,21,17,47,79,94,48,41,49,45,78,77,46,44,34,81,43,76,75,80,101,33,90,74,106])).
% 117.43/118.16 cnf(5174,plain,
% 117.43/118.16 (~P6(a62,a58,a76)),
% 117.43/118.16 inference(scs_inference,[],[1,244,278,285,301,304,3550,4909,5120,5135,4911,4913,4915,4917,4919,4921,5119,4927,4947,5042,5031,4933,4941,4929,1795,547,1995,1984,9,678,953,5145,14,8,604,51,37,99,69,102,27,29,52,38,50,32,39,70,23,31,30,20,22,71,84,60,28,82,57,87,36,64,21,17,47,79,94,48,41,49,45,78,77,46,44,34,81,43,76,75,80,101,33,90,74,106,1341])).
% 117.43/118.16 cnf(5176,plain,
% 117.43/118.16 (P1(f77(a62,a62),a62)),
% 117.43/118.16 inference(scs_inference,[],[1,244,278,285,301,304,3550,4909,5120,5135,4911,4913,4915,4917,4919,4921,5119,4927,4947,5042,5031,4933,4941,4929,1795,547,1995,1984,9,678,953,5145,14,8,604,51,37,99,69,102,27,29,52,38,50,32,39,70,23,31,30,20,22,71,84,60,28,82,57,87,36,64,21,17,47,79,94,48,41,49,45,78,77,46,44,34,81,43,76,75,80,101,33,90,74,106,1341,53])).
% 117.43/118.16 cnf(5187,plain,
% 117.43/118.16 (~P6(x51871,f75(a2),a82)),
% 117.43/118.16 inference(scs_inference,[],[310,5111,5087,37,69,27])).
% 117.43/118.16 cnf(5195,plain,
% 117.43/118.16 (~P6(x51951,f75(a2),a88)),
% 117.43/118.16 inference(scs_inference,[],[310,317,3552,5111,5087,37,69,27,99,38,51,29])).
% 117.43/118.16 cnf(5199,plain,
% 117.43/118.16 (~P6(f75(a2),x51991,a73)),
% 117.43/118.16 inference(scs_inference,[],[310,317,3552,5111,5087,37,69,27,99,38,51,29,52,32])).
% 117.43/118.16 cnf(5209,plain,
% 117.43/118.16 (P6(f75(a65),x52091,a87)),
% 117.43/118.16 inference(scs_inference,[],[280,310,317,3552,5111,5087,37,69,27,99,38,51,29,52,32,102,50,70,39,23])).
% 117.43/118.16 cnf(5213,plain,
% 117.43/118.16 (P6(x52131,f75(a65),a81)),
% 117.43/118.16 inference(scs_inference,[],[280,310,317,3552,5111,5087,37,69,27,99,38,51,29,52,32,102,50,70,39,23,31,22])).
% 117.43/118.16 cnf(5225,plain,
% 117.43/118.16 (P1(f4(a62),a62)),
% 117.43/118.16 inference(scs_inference,[],[280,310,317,3552,5105,5039,5111,5087,37,69,27,99,38,51,29,52,32,102,50,70,39,23,31,22,30,20,71,28,36,21])).
% 117.43/118.16 cnf(5227,plain,
% 117.43/118.16 (P1(f26(a62,a3),f75(a62))),
% 117.43/118.16 inference(scs_inference,[],[280,310,317,3552,5105,5039,5111,5087,4935,37,69,27,99,38,51,29,52,32,102,50,70,39,23,31,22,30,20,71,28,36,21,17])).
% 117.43/118.16 cnf(5229,plain,
% 117.43/118.16 (P1(f32(a62,a2),a62)),
% 117.43/118.16 inference(scs_inference,[],[1,280,310,317,3552,5057,5105,5039,5111,5087,4935,37,69,27,99,38,51,29,52,32,102,50,70,39,23,31,22,30,20,71,28,36,21,17,41])).
% 117.43/118.16 cnf(5232,plain,
% 117.43/118.16 (~P2(a81,a85)),
% 117.43/118.16 inference(scs_inference,[],[1,280,310,317,3552,4923,5057,5089,5105,5039,5111,5087,4935,37,69,27,99,38,51,29,52,32,102,50,70,39,23,31,22,30,20,71,28,36,21,17,41,94])).
% 117.43/118.16 cnf(5234,plain,
% 117.43/118.16 (P6(x52341,a62,a81)),
% 117.43/118.16 inference(rename_variables,[],[5089])).
% 117.43/118.16 cnf(5236,plain,
% 117.43/118.16 (P1(f29(a62,a2),a62)),
% 117.43/118.16 inference(scs_inference,[],[1,280,310,317,3552,4923,5057,5081,5089,5105,5039,5111,5087,4935,37,69,27,99,38,51,29,52,32,102,50,70,39,23,31,22,30,20,71,28,36,21,17,41,94,78])).
% 117.43/118.16 cnf(5243,plain,
% 117.43/118.16 (P1(f52(a2,a62),a62)),
% 117.43/118.16 inference(scs_inference,[],[1,280,310,317,3552,4923,5057,5081,5089,5234,5105,5039,5111,5087,4935,2039,37,69,27,99,38,51,29,52,32,102,50,70,39,23,31,22,30,20,71,28,36,21,17,41,94,78,47,49,79])).
% 117.43/118.16 cnf(5249,plain,
% 117.43/118.16 (P1(x52491,f48(a85,a85))),
% 117.43/118.16 inference(rename_variables,[],[678])).
% 117.43/118.16 cnf(5251,plain,
% 117.43/118.16 (~P1(f14(a2,a65),a65)),
% 117.43/118.16 inference(scs_inference,[],[1,280,310,317,3552,4923,5057,5065,5081,5089,5234,5105,5039,5111,5087,4935,2039,678,37,69,27,99,38,51,29,52,32,102,50,70,39,23,31,22,30,20,71,28,36,21,17,41,94,78,47,49,79,48,45,77])).
% 117.43/118.16 cnf(5257,plain,
% 117.43/118.16 (P1(x52571,f48(a85,a85))),
% 117.43/118.16 inference(rename_variables,[],[678])).
% 117.43/118.16 cnf(5259,plain,
% 117.43/118.16 (P6(a65,a65,a83)),
% 117.43/118.16 inference(scs_inference,[],[1,280,310,317,3552,4923,5057,5065,5081,5089,5234,5105,5039,4943,5111,5087,4935,2039,4929,678,5249,37,69,27,99,38,51,29,52,32,102,50,70,39,23,31,22,30,20,71,28,36,21,17,41,94,78,47,49,79,48,45,77,46,44,34])).
% 117.43/118.16 cnf(5261,plain,
% 117.43/118.16 (P1(f79(a62,a62),a62)),
% 117.43/118.16 inference(scs_inference,[],[1,280,310,317,3552,4923,5057,5065,5081,5089,5234,5105,5163,5039,4943,5176,5111,5087,4935,2039,4929,678,5249,37,69,27,99,38,51,29,52,32,102,50,70,39,23,31,22,30,20,71,28,36,21,17,41,94,78,47,49,79,48,45,77,46,44,34,81])).
% 117.43/118.16 cnf(5266,plain,
% 117.43/118.16 (P1(f60(a69,a58),a69)),
% 117.43/118.16 inference(scs_inference,[],[1,280,310,317,3552,4923,5057,5065,5081,5089,5234,5105,5163,5039,4943,5176,5111,5087,4935,2039,608,4929,678,5249,5257,14,37,69,27,99,38,51,29,52,32,102,50,70,39,23,31,22,30,20,71,28,36,21,17,41,94,78,47,49,79,48,45,77,46,44,34,81,43,76])).
% 117.43/118.16 cnf(5269,plain,
% 117.43/118.16 (P1(f78(a62,a62),a62)),
% 117.43/118.16 inference(scs_inference,[],[1,280,310,317,3552,4923,5057,5065,5081,5089,5234,5105,5163,5039,4943,5176,5111,5087,4935,2039,608,4929,678,5249,5257,14,37,69,27,99,38,51,29,52,32,102,50,70,39,23,31,22,30,20,71,28,36,21,17,41,94,78,47,49,79,48,45,77,46,44,34,81,43,76,80])).
% 117.43/118.16 cnf(5271,plain,
% 117.43/118.16 (~P1(f40(a65,a58),a65)),
% 117.43/118.16 inference(scs_inference,[],[1,280,310,317,3552,4923,5057,5065,5075,5081,5089,5234,5105,5163,5039,4943,5176,5111,5087,4935,2039,608,4929,678,5249,5257,14,604,37,69,27,99,38,51,29,52,32,102,50,70,39,23,31,22,30,20,71,28,36,21,17,41,94,78,47,49,79,48,45,77,46,44,34,81,43,76,80,101])).
% 117.43/118.16 cnf(5275,plain,
% 117.43/118.16 (P6(a65,a65,a8)),
% 117.43/118.16 inference(scs_inference,[],[1,280,310,317,3552,4923,5057,5065,5075,5081,5089,5234,5105,5163,5039,4943,5176,5111,5087,4935,2039,608,4929,678,5249,5257,14,604,37,69,27,99,38,51,29,52,32,102,50,70,39,23,31,22,30,20,71,28,36,21,17,41,94,78,47,49,79,48,45,77,46,44,34,81,43,76,80,101,33])).
% 117.43/118.16 cnf(5277,plain,
% 117.43/118.16 (~P1(f22(a62,a65),a65)),
% 117.43/118.16 inference(scs_inference,[],[1,280,310,317,3552,4923,5057,5065,5067,5075,5081,5089,5234,5105,5163,5039,4943,5176,5111,5087,4935,2039,608,4929,678,5249,5257,14,604,37,69,27,99,38,51,29,52,32,102,50,70,39,23,31,22,30,20,71,28,36,21,17,41,94,78,47,49,79,48,45,77,46,44,34,81,43,76,80,101,33,90])).
% 117.43/118.16 cnf(5280,plain,
% 117.43/118.16 (P1(f35(a62,a62),a62)),
% 117.43/118.16 inference(scs_inference,[],[1,280,310,317,3552,4923,5057,5065,5067,5075,5077,5081,5089,5234,5105,5163,5039,4943,5176,5111,5087,4935,2039,608,4929,678,5249,5257,14,604,37,69,27,99,38,51,29,52,32,102,50,70,39,23,31,22,30,20,71,28,36,21,17,41,94,78,47,49,79,48,45,77,46,44,34,81,43,76,80,101,33,90,74])).
% 117.43/118.16 cnf(5285,plain,
% 117.43/118.16 (P1(f4(a62),a65)),
% 117.43/118.16 inference(scs_inference,[],[1,280,310,317,3552,4923,5057,5065,5067,5075,5077,5081,5089,5234,5105,5163,5039,4943,5176,5111,5087,4935,2039,608,4929,678,5249,5257,14,604,37,69,27,99,38,51,29,52,32,102,50,70,39,23,31,22,30,20,71,28,36,21,17,41,94,78,47,49,79,48,45,77,46,44,34,81,43,76,80,101,33,90,74,1341,15])).
% 117.43/118.16 cnf(5287,plain,
% 117.43/118.16 (P1(f77(a65,a65),a65)),
% 117.43/118.16 inference(scs_inference,[],[1,280,310,317,3552,4923,5057,5065,5067,5075,5077,5081,5089,5234,5105,5163,5039,4943,5176,5111,5087,4935,2039,608,4929,678,5249,5257,14,604,37,69,27,99,38,51,29,52,32,102,50,70,39,23,31,22,30,20,71,28,36,21,17,41,94,78,47,49,79,48,45,77,46,44,34,81,43,76,80,101,33,90,74,1341,15,53])).
% 117.43/118.16 cnf(5292,plain,
% 117.43/118.16 (~P6(x52921,a2,a88)),
% 117.43/118.16 inference(scs_inference,[],[5099,29])).
% 117.43/118.16 cnf(5294,plain,
% 117.43/118.16 (~P6(f75(a62),x52941,a84)),
% 117.43/118.16 inference(scs_inference,[],[5099,5227,29,37])).
% 117.43/118.16 cnf(5298,plain,
% 117.43/118.16 (~P6(x52981,a2,a82)),
% 117.43/118.16 inference(scs_inference,[],[333,5099,5227,29,37,69,27])).
% 117.43/118.16 cnf(5316,plain,
% 117.43/118.16 (P6(f75(a62),x53161,a87)),
% 117.43/118.16 inference(scs_inference,[],[307,333,340,346,513,3523,5099,5227,29,37,69,27,38,32,51,52,99,70,102,50,23])).
% 117.43/118.16 cnf(5320,plain,
% 117.43/118.16 (~P6(a2,x53201,a85)),
% 117.43/118.16 inference(scs_inference,[],[307,333,340,346,513,3523,5099,5227,29,37,69,27,38,32,51,52,99,70,102,50,23,39,31])).
% 117.43/118.16 cnf(5326,plain,
% 117.43/118.16 (~P1(f77(a65,a65),f75(a65))),
% 117.43/118.16 inference(scs_inference,[],[307,333,340,346,513,3523,5099,5287,5227,5229,29,37,69,27,38,32,51,52,99,70,102,50,23,39,31,15,22,20])).
% 117.43/118.16 cnf(5336,plain,
% 117.43/118.16 (P1(f12(a62,a3),f75(a62))),
% 117.43/118.16 inference(scs_inference,[],[307,333,340,346,513,3523,5171,5099,5287,5227,5229,29,37,69,27,38,32,51,52,99,70,102,50,23,39,31,15,22,20,30,71,28,36,17])).
% 117.43/118.16 cnf(5338,plain,
% 117.43/118.16 (~P2(a8,a84)),
% 117.43/118.16 inference(scs_inference,[],[307,333,340,346,513,5008,3523,5171,5099,5287,5227,5229,4911,29,37,69,27,38,32,51,52,99,70,102,50,23,39,31,15,22,20,30,71,28,36,17,94])).
% 117.43/118.16 cnf(5344,plain,
% 117.43/118.16 (~P1(x53441,f46(a73,a73))),
% 117.43/118.16 inference(rename_variables,[],[953])).
% 117.43/118.16 cnf(5355,plain,
% 117.43/118.16 (P6(f75(a62),f75(a62),a83)),
% 117.43/118.16 inference(scs_inference,[],[307,333,340,346,513,5008,3523,5171,5099,5287,5227,5229,507,4911,465,4935,678,953,29,37,69,27,38,32,51,52,99,70,102,50,23,39,31,15,22,20,30,71,28,36,17,94,49,48,47,45,46,44,34])).
% 117.43/118.16 cnf(5367,plain,
% 117.43/118.16 (~P1(f40(a2,a58),a2)),
% 117.43/118.16 inference(scs_inference,[],[307,333,340,346,513,5008,3523,5275,5171,5099,5287,5227,5229,507,599,4911,465,4935,678,953,5344,14,604,29,37,69,27,38,32,51,52,99,70,102,50,23,39,31,15,22,20,30,71,28,36,17,94,49,48,47,45,46,44,34,81,43,76,80,101])).
% 117.43/118.16 cnf(5368,plain,
% 117.43/118.16 (P1(x53681,f75(a58))),
% 117.43/118.16 inference(rename_variables,[],[604])).
% 117.43/118.16 cnf(5372,plain,
% 117.43/118.16 (~P1(f22(a2,a65),a65)),
% 117.43/118.16 inference(scs_inference,[],[1,307,333,340,346,513,5008,3523,5275,5171,5099,5287,5227,5229,507,599,4911,5067,465,4935,678,953,5344,14,604,29,37,69,27,38,32,51,52,99,70,102,50,23,39,31,15,22,20,30,71,28,36,17,94,49,48,47,45,46,44,34,81,43,76,80,101,33,90])).
% 117.43/118.16 cnf(5375,plain,
% 117.43/118.16 (P1(f35(a62,a2),a62)),
% 117.43/118.16 inference(scs_inference,[],[1,307,333,340,346,513,5008,3523,5275,5171,5099,5287,5227,5229,507,599,4911,5067,5077,465,4935,678,953,5344,14,604,29,37,69,27,38,32,51,52,99,70,102,50,23,39,31,15,22,20,30,71,28,36,17,94,49,48,47,45,46,44,34,81,43,76,80,101,33,90,74])).
% 117.43/118.16 cnf(5380,plain,
% 117.43/118.16 (P6(a2,a58,a9)),
% 117.43/118.16 inference(scs_inference,[],[1,307,333,340,346,513,5008,3523,5275,5171,5099,5287,5227,5229,507,599,4911,5067,5077,465,4935,678,953,5344,14,604,5368,29,37,69,27,38,32,51,52,99,70,102,50,23,39,31,15,22,20,30,71,28,36,17,94,49,48,47,45,46,44,34,81,43,76,80,101,33,90,74,1341,40])).
% 117.43/118.16 cnf(5383,plain,
% 117.43/118.16 (P1(f38(a2,a58),a2)),
% 117.43/118.16 inference(scs_inference,[],[1,307,333,340,346,513,5008,3523,5275,5171,5099,5287,5227,5229,507,599,4911,5067,5077,465,4935,678,953,5344,14,604,5368,29,37,69,27,38,32,51,52,99,70,102,50,23,39,31,15,22,20,30,71,28,36,17,94,49,48,47,45,46,44,34,81,43,76,80,101,33,90,74,1341,40,65])).
% 117.43/118.16 cnf(5397,plain,
% 117.43/118.16 (~P6(a59,x53971,a84)),
% 117.43/118.16 inference(scs_inference,[],[511,559,614,5326,4991,51,38,69,29,99,37])).
% 117.43/118.16 cnf(5401,plain,
% 117.43/118.16 (P6(f41(a73,a8),f47(a73,a8),a73)),
% 117.43/118.16 inference(scs_inference,[],[511,559,614,5326,4991,953,51,38,69,29,99,37,32,50])).
% 117.43/118.16 cnf(5411,plain,
% 117.43/118.16 (~P6(a59,x54111,a89)),
% 117.43/118.16 inference(scs_inference,[],[313,511,555,559,614,5326,4991,953,51,38,69,29,99,37,32,50,102,27,70,52,39])).
% 117.43/118.16 cnf(5413,plain,
% 117.43/118.16 (P6(a59,x54131,a87)),
% 117.43/118.16 inference(scs_inference,[],[313,511,555,559,614,5326,4991,953,51,38,69,29,99,37,32,50,102,27,70,52,39,23])).
% 117.43/118.16 cnf(5419,plain,
% 117.43/118.16 (P6(x54191,a59,a81)),
% 117.43/118.16 inference(scs_inference,[],[313,511,555,559,614,5326,4991,5236,953,51,38,69,29,99,37,32,50,102,27,70,52,39,23,31,15,22])).
% 117.43/118.16 cnf(5421,plain,
% 117.43/118.16 (~P1(f4(a62),f75(a62))),
% 117.43/118.16 inference(scs_inference,[],[313,511,555,559,614,5225,5326,4991,5236,953,51,38,69,29,99,37,32,50,102,27,70,52,39,23,31,15,22,20])).
% 117.43/118.16 cnf(5433,plain,
% 117.43/118.16 (P1(f26(a65,a3),f75(a65))),
% 117.43/118.16 inference(scs_inference,[],[313,511,555,559,614,5093,5225,5326,4991,5236,953,51,38,69,29,99,37,32,50,102,27,70,52,39,23,31,15,22,20,30,71,28,36,21,17])).
% 117.43/118.16 cnf(5435,plain,
% 117.43/118.16 (~P1(f14(a2,a2),a2)),
% 117.43/118.16 inference(scs_inference,[],[1,313,511,555,559,5298,614,5093,5225,5326,4991,5236,953,51,38,69,29,99,37,32,50,102,27,70,52,39,23,31,15,22,20,30,71,28,36,21,17,77])).
% 117.43/118.16 cnf(5438,plain,
% 117.43/118.16 (~P2(a9,a76)),
% 117.43/118.16 inference(scs_inference,[],[1,313,511,555,559,5029,5380,5298,614,5093,5225,5326,4991,5236,953,51,38,69,29,99,37,32,50,102,27,70,52,39,23,31,15,22,20,30,71,28,36,21,17,77,94])).
% 117.43/118.16 cnf(5445,plain,
% 117.43/118.16 (P1(x54451,f48(a85,a85))),
% 117.43/118.16 inference(rename_variables,[],[678])).
% 117.43/118.16 cnf(5447,plain,
% 117.43/118.16 (~P6(a69,a71,a90)),
% 117.43/118.16 inference(scs_inference,[],[1,313,511,555,559,5029,5380,5298,614,5093,5225,5326,4991,5236,5287,12,6,678,953,51,38,69,29,99,37,32,50,102,27,70,52,39,23,31,15,22,20,30,71,28,36,21,17,77,94,48,49,45,47])).
% 117.43/118.16 cnf(5453,plain,
% 117.43/118.16 (P1(x54531,f48(a85,a85))),
% 117.43/118.16 inference(rename_variables,[],[678])).
% 117.43/118.16 cnf(5460,plain,
% 117.43/118.16 (P1(f60(a56,a58),a56)),
% 117.43/118.16 inference(scs_inference,[],[1,313,511,555,559,5029,5380,5298,614,5093,5225,5326,4991,5236,289,5287,12,6,678,5445,5453,953,14,51,38,69,29,99,37,32,50,102,27,70,52,39,23,31,15,22,20,30,71,28,36,21,17,77,94,48,49,45,47,46,44,34,43,76])).
% 117.43/118.16 cnf(5461,plain,
% 117.43/118.16 (~P1(x54611,a58)),
% 117.43/118.16 inference(rename_variables,[],[14])).
% 117.43/118.16 cnf(5465,plain,
% 117.43/118.16 (~P1(f22(a2,a2),a2)),
% 117.43/118.16 inference(scs_inference,[],[1,313,511,555,559,5029,5380,5292,5298,614,5093,5225,5326,4991,5236,5367,289,5287,12,6,678,5445,5453,953,14,51,38,69,29,99,37,32,50,102,27,70,52,39,23,31,15,22,20,30,71,28,36,21,17,77,94,48,49,45,47,46,44,34,43,76,33,90])).
% 117.43/118.16 cnf(5468,plain,
% 117.43/118.16 (P1(f19(a62,a58),a62)),
% 117.43/118.16 inference(scs_inference,[],[1,313,511,555,559,5029,5174,5380,5292,5298,614,5093,5225,5326,4991,5236,5367,5103,289,5287,12,6,678,5445,5453,953,14,5461,51,38,69,29,99,37,32,50,102,27,70,52,39,23,31,15,22,20,30,71,28,36,21,17,77,94,48,49,45,47,46,44,34,43,76,33,90,96])).
% 117.43/118.16 cnf(5473,plain,
% 117.43/118.16 (P1(f77(a59,a59),a59)),
% 117.43/118.16 inference(scs_inference,[],[1,313,511,555,559,5029,5174,5380,5292,5298,614,5093,5225,5326,4991,5236,5367,5103,289,5287,12,6,678,5445,5453,953,14,5461,51,38,69,29,99,37,32,50,102,27,70,52,39,23,31,15,22,20,30,71,28,36,21,17,77,94,48,49,45,47,46,44,34,43,76,33,90,96,1341,53])).
% 117.43/118.16 cnf(5483,plain,
% 117.43/118.16 (P3(a83,a83)),
% 117.43/118.16 inference(scs_inference,[],[1,313,511,555,559,5029,5174,5259,5380,5292,5298,614,5093,5225,5326,4991,5236,5266,5367,5103,289,7,5287,12,6,678,5445,5453,953,14,5461,51,38,69,29,99,37,32,50,102,27,70,52,39,23,31,15,22,20,30,71,28,36,21,17,77,94,48,49,45,47,46,44,34,43,76,33,90,96,1341,53,41,81,80,88,100])).
% 117.43/118.16 cnf(5485,plain,
% 117.43/118.16 (~P5(a83,a83)),
% 117.43/118.16 inference(scs_inference,[],[1,313,511,555,559,5029,5174,5259,5380,5292,5298,614,5093,5225,5326,4991,5236,5266,5367,5103,289,7,5287,12,6,678,5445,5453,953,14,5461,51,38,69,29,99,37,32,50,102,27,70,52,39,23,31,15,22,20,30,71,28,36,21,17,77,94,48,49,45,47,46,44,34,43,76,33,90,96,1341,53,41,81,80,88,100,104])).
% 117.43/118.16 cnf(5499,plain,
% 117.43/118.16 (P6(f48(a73,a73),f51(a73,a73),a73)),
% 117.43/118.16 inference(scs_inference,[],[335,644,770,4967,5421,32,102,69,99,51])).
% 117.43/118.16 cnf(5501,plain,
% 117.43/118.16 (~P6(a56,x55011,a86)),
% 117.43/118.16 inference(scs_inference,[],[335,644,770,4967,5421,5460,32,102,69,99,51,38])).
% 117.43/118.16 cnf(5503,plain,
% 117.43/118.16 (~P6(a56,x55031,a84)),
% 117.43/118.16 inference(scs_inference,[],[335,644,770,4967,5421,5460,32,102,69,99,51,38,37])).
% 117.43/118.16 cnf(5515,plain,
% 117.43/118.16 (P6(a56,x55151,a87)),
% 117.43/118.16 inference(scs_inference,[],[335,644,770,775,894,4967,5421,5460,32,102,69,99,51,38,37,52,70,27,29,50,23])).
% 117.43/118.16 cnf(5523,plain,
% 117.43/118.16 (P6(x55231,a56,a81)),
% 117.43/118.16 inference(scs_inference,[],[335,644,770,775,894,4967,5261,5421,5460,32,102,69,99,51,38,37,52,70,27,29,50,23,39,31,15,22])).
% 117.43/118.16 cnf(5537,plain,
% 117.43/118.16 (P1(f40(a71,a58),f75(a71))),
% 117.43/118.16 inference(scs_inference,[],[335,644,770,775,894,4967,5383,5159,5261,5421,5460,32,102,69,99,51,38,37,52,70,27,29,50,23,39,31,15,22,20,30,71,28,36,21,17])).
% 117.43/118.16 cnf(5542,plain,
% 117.43/118.16 (P1(f52(a2,a59),a59)),
% 117.43/118.16 inference(scs_inference,[],[1,335,644,770,775,894,5413,5419,4967,5383,5159,5261,5421,5460,32,102,69,99,51,38,37,52,70,27,29,50,23,39,31,15,22,20,30,71,28,36,21,17,78,79])).
% 117.43/118.16 cnf(5543,plain,
% 117.43/118.16 (P6(x55431,a59,a81)),
% 117.43/118.16 inference(rename_variables,[],[5419])).
% 117.43/118.16 cnf(5552,plain,
% 117.43/118.16 (~P2(a81,a86)),
% 117.43/118.16 inference(scs_inference,[],[1,335,644,770,775,894,5071,5397,5413,5419,5543,4967,5383,5159,5261,5285,5421,5460,32,102,69,99,51,38,37,52,70,27,29,50,23,39,31,15,22,20,30,71,28,36,21,17,78,79,41,49,47,94])).
% 117.43/118.16 cnf(5554,plain,
% 117.43/118.16 (~P6(a62,x55541,a86)),
% 117.43/118.16 inference(rename_variables,[],[5071])).
% 117.43/118.16 cnf(5557,plain,
% 117.43/118.16 (~P1(x55571,f46(a73,a73))),
% 117.43/118.16 inference(rename_variables,[],[953])).
% 117.43/118.16 cnf(5569,plain,
% 117.43/118.16 (~P1(x55691,f46(a73,a73))),
% 117.43/118.16 inference(rename_variables,[],[953])).
% 117.43/118.16 cnf(5572,plain,
% 117.43/118.16 (~P1(x55721,f46(a73,a73))),
% 117.43/118.16 inference(rename_variables,[],[953])).
% 117.43/118.16 cnf(5574,plain,
% 117.43/118.16 (P1(f72(a58,a69),a69)),
% 117.43/118.16 inference(scs_inference,[],[1,335,644,770,775,894,5071,5397,5413,5419,5543,4967,5383,5159,5261,5285,5433,5421,5460,611,678,953,5557,5569,14,32,102,69,99,51,38,37,52,70,27,29,50,23,39,31,15,22,20,30,71,28,36,21,17,78,79,41,49,47,94,48,45,46,44,34,43,81,76])).
% 117.43/118.16 cnf(5577,plain,
% 117.43/118.16 (P1(f36(a62,a3),a62)),
% 117.43/118.16 inference(scs_inference,[],[1,335,644,770,775,894,5071,5554,5397,5413,5419,5543,4967,5383,5159,5261,5285,5433,5421,5460,611,678,953,5557,5569,14,8,32,102,69,99,51,38,37,52,70,27,29,50,23,39,31,15,22,20,30,71,28,36,21,17,78,79,41,49,47,94,48,45,46,44,34,43,81,76,93])).
% 117.43/118.16 cnf(5578,plain,
% 117.43/118.16 (P1(x55781,a3)),
% 117.43/118.16 inference(rename_variables,[],[8])).
% 117.43/118.16 cnf(5584,plain,
% 117.43/118.16 (~P1(f23(a65,a3),a65)),
% 117.43/118.16 inference(scs_inference,[],[1,335,644,770,775,894,5071,5554,5083,5397,5413,5419,5543,4967,5383,5159,5261,5285,5433,5421,5460,611,678,953,5557,5569,5572,14,8,5578,32,102,69,99,51,38,37,52,70,27,29,50,23,39,31,15,22,20,30,71,28,36,21,17,78,79,41,49,47,94,48,45,46,44,34,43,81,76,93,80,98])).
% 117.43/118.16 cnf(5595,plain,
% 117.43/118.16 (~P6(a56,a58,a76)),
% 117.43/118.16 inference(scs_inference,[],[1,335,644,770,775,894,5071,5554,5083,5397,5411,5413,5419,5543,4967,5383,5159,5261,5285,5433,5401,5421,5460,611,7,13,678,953,5557,5569,5572,14,8,5578,32,102,69,99,51,38,37,52,70,27,29,50,23,39,31,15,22,20,30,71,28,36,21,17,78,79,41,49,47,94,48,45,46,44,34,43,81,76,93,80,98,33,91,74,1341])).
% 117.43/118.16 cnf(5609,plain,
% 117.43/118.16 (~P6(f45(a5,a5),x56091,a73)),
% 117.43/118.16 inference(scs_inference,[],[896,1315,5537,799,37,70,51,69,32])).
% 117.43/118.16 cnf(5627,plain,
% 117.43/118.16 (P6(f75(a71),x56271,a87)),
% 117.43/118.16 inference(scs_inference,[],[342,896,1296,1315,5118,5537,799,37,70,51,69,32,102,50,29,38,27,99,52,39,23])).
% 117.43/118.16 cnf(5631,plain,
% 117.43/118.16 (P1(f78(a62,a62),a65)),
% 117.43/118.16 inference(scs_inference,[],[342,896,1296,1315,5118,5269,5537,953,799,37,70,51,69,32,102,50,29,38,27,99,52,39,23,31,15])).
% 117.43/118.16 cnf(5635,plain,
% 117.43/118.16 (~P1(f77(a59,a59),f75(a59))),
% 117.43/118.16 inference(scs_inference,[],[342,896,1296,1315,5118,5473,5269,5537,953,799,37,70,51,69,32,102,50,29,38,27,99,52,39,23,31,15,22,20])).
% 117.43/118.16 cnf(5645,plain,
% 117.43/118.16 (P1(f14(a2,a71),f75(a71))),
% 117.43/118.16 inference(scs_inference,[],[342,896,1296,1315,5118,5473,5269,5134,5537,953,799,37,70,51,69,32,102,50,29,38,27,99,52,39,23,31,15,22,20,30,71,28,36,17])).
% 117.43/118.16 cnf(5647,plain,
% 117.43/118.16 (P1(f29(a56,a2),a56)),
% 117.43/118.16 inference(scs_inference,[],[1,342,896,1296,1315,5515,5118,5473,5269,5134,5537,953,799,37,70,51,69,32,102,50,29,38,27,99,52,39,23,31,15,22,20,30,71,28,36,17,78])).
% 117.43/118.16 cnf(5648,plain,
% 117.43/118.16 (P6(a56,x56481,a87)),
% 117.43/118.16 inference(rename_variables,[],[5515])).
% 117.43/118.16 cnf(5658,plain,
% 117.43/118.16 (~P2(a87,a86)),
% 117.43/118.16 inference(scs_inference,[],[1,342,896,1296,1315,4925,5503,5515,5648,5523,5118,5473,5269,5134,5537,5159,953,799,37,70,51,69,32,102,50,29,38,27,99,52,39,23,31,15,22,20,30,71,28,36,17,78,79,41,49,94])).
% 117.43/118.16 cnf(5708,plain,
% 117.43/118.16 (~P6(a69,x57081,a86)),
% 117.43/118.16 inference(scs_inference,[],[5232,5574,50,38])).
% 117.43/118.16 cnf(5714,plain,
% 117.43/118.16 (~P6(a69,x57141,a84)),
% 117.43/118.16 inference(scs_inference,[],[1307,1323,5232,5574,50,38,51,70,37])).
% 117.43/118.16 cnf(5730,plain,
% 117.43/118.16 (P6(a69,x57301,a87)),
% 117.43/118.16 inference(scs_inference,[],[351,1307,1323,5232,5635,5574,50,38,51,70,37,32,52,99,27,102,29,69,23])).
% 117.43/118.16 cnf(5732,plain,
% 117.43/118.16 (~P6(a69,x57321,a89)),
% 117.43/118.16 inference(scs_inference,[],[351,1307,1323,5232,5635,5574,50,38,51,70,37,32,52,99,27,102,29,69,23,39])).
% 117.43/118.16 cnf(5736,plain,
% 117.43/118.16 (P1(f36(a62,a3),a65)),
% 117.43/118.16 inference(scs_inference,[],[351,1307,1323,5232,5635,5574,5577,50,38,51,70,37,32,52,99,27,102,29,69,23,39,31,15])).
% 117.43/118.16 cnf(5738,plain,
% 117.43/118.16 (P6(x57381,a69,a81)),
% 117.43/118.16 inference(scs_inference,[],[351,1307,1323,5232,5635,5574,5577,50,38,51,70,37,32,52,99,27,102,29,69,23,39,31,15,22])).
% 117.43/118.16 cnf(5740,plain,
% 117.43/118.16 (~P1(f78(a62,a62),f75(a65))),
% 117.43/118.16 inference(scs_inference,[],[351,1307,1323,5232,5635,5631,5574,5577,50,38,51,70,37,32,52,99,27,102,29,69,23,39,31,15,22,20])).
% 117.43/118.16 cnf(5748,plain,
% 117.43/118.16 (~P6(a69,x57481,a5)),
% 117.43/118.16 inference(scs_inference,[],[351,1307,1323,5232,5635,5631,5574,5577,50,38,51,70,37,32,52,99,27,102,29,69,23,39,31,15,22,20,30,71,28,36])).
% 117.43/118.16 cnf(5752,plain,
% 117.43/118.16 (P1(f22(a2,a71),f75(a71))),
% 117.43/118.16 inference(scs_inference,[],[351,1307,1323,5232,5165,5635,5631,5574,5577,50,38,51,70,37,32,52,99,27,102,29,69,23,39,31,15,22,20,30,71,28,36,21,17])).
% 117.43/118.16 cnf(5754,plain,
% 117.43/118.16 (P1(f52(a2,a69),a69)),
% 117.43/118.16 inference(scs_inference,[],[1,351,1307,1323,5232,5165,5635,5631,5574,5577,50,38,51,70,37,32,52,99,27,102,29,69,23,39,31,15,22,20,30,71,28,36,21,17,79])).
% 117.43/118.16 cnf(5756,plain,
% 117.43/118.16 (~P2(a10,a90)),
% 117.43/118.16 inference(scs_inference,[],[1,351,1307,1323,5232,4426,5165,5635,5631,5574,5577,748,50,38,51,70,37,32,52,99,27,102,29,69,23,39,31,15,22,20,30,71,28,36,21,17,79,94])).
% 117.43/118.16 cnf(5772,plain,
% 117.43/118.16 (P6(a69,a69,a83)),
% 117.43/118.16 inference(scs_inference,[],[1,351,1307,1323,5232,4426,5165,5635,5645,5631,5542,5574,5577,748,5473,5134,953,50,38,51,70,37,32,52,99,27,102,29,69,23,39,31,15,22,20,30,71,28,36,21,17,79,94,49,47,45,48,46,44,34])).
% 117.43/118.16 cnf(5779,plain,
% 117.43/118.16 (P6(a69,a69,a8)),
% 117.43/118.16 inference(scs_inference,[],[1,351,1307,1323,5232,4426,5165,5635,5645,5631,5542,5574,5577,247,748,5473,5134,953,14,50,38,51,70,37,32,52,99,27,102,29,69,23,39,31,15,22,20,30,71,28,36,21,17,79,94,49,47,45,48,46,44,34,43,76,33])).
% 117.43/118.16 cnf(5783,plain,
% 117.43/118.16 (~P1(f22(a71,a71),a71)),
% 117.43/118.16 inference(scs_inference,[],[1,351,1307,1323,5232,4426,5165,5499,5635,5645,5631,5542,5574,5577,247,4915,748,5473,5134,7,13,953,14,50,38,51,70,37,32,52,99,27,102,29,69,23,39,31,15,22,20,30,71,28,36,21,17,79,94,49,47,45,48,46,44,34,43,76,33,91,90])).
% 117.43/118.16 cnf(5786,plain,
% 117.43/118.16 (~P6(a69,a58,a76)),
% 117.43/118.16 inference(scs_inference,[],[1,351,1307,1323,5232,4426,5165,5499,5635,5645,5631,5542,5574,5577,247,4915,748,5473,5134,7,13,953,14,50,38,51,70,37,32,52,99,27,102,29,69,23,39,31,15,22,20,30,71,28,36,21,17,79,94,49,47,45,48,46,44,34,43,76,33,91,90,1341])).
% 117.43/118.16 cnf(5788,plain,
% 117.43/118.16 (P1(f77(a69,a69),a69)),
% 117.43/118.16 inference(scs_inference,[],[1,351,1307,1323,5232,4426,5165,5499,5635,5645,5631,5542,5574,5577,247,4915,748,5473,5134,7,13,953,14,50,38,51,70,37,32,52,99,27,102,29,69,23,39,31,15,22,20,30,71,28,36,21,17,79,94,49,47,45,48,46,44,34,43,76,33,91,90,1341,53])).
% 117.43/118.16 cnf(5794,plain,
% 117.43/118.16 (P1(f79(a69,a69),a69)),
% 117.43/118.16 inference(scs_inference,[],[1,351,1307,1323,5232,4426,5165,5499,5336,5635,5645,5631,5542,5574,5577,247,4915,748,5473,5134,7,13,953,14,50,38,51,70,37,32,52,99,27,102,29,69,23,39,31,15,22,20,30,71,28,36,21,17,79,94,49,47,45,48,46,44,34,43,76,33,91,90,1341,53,40,78,81])).
% 117.43/118.16 cnf(5796,plain,
% 117.43/118.16 (P1(f78(a69,a69),a69)),
% 117.43/118.16 inference(scs_inference,[],[1,351,1307,1323,5232,4426,5165,5499,5336,5635,5645,5631,5542,5574,5577,247,4915,748,5473,5134,7,13,953,14,50,38,51,70,37,32,52,99,27,102,29,69,23,39,31,15,22,20,30,71,28,36,21,17,79,94,49,47,45,48,46,44,34,43,76,33,91,90,1341,53,40,78,81,80])).
% 117.43/118.16 cnf(5806,plain,
% 117.43/118.16 (~P6(a71,x58061,a84)),
% 117.43/118.16 inference(scs_inference,[],[1758,7,668,52,27,37])).
% 117.43/118.16 cnf(5808,plain,
% 117.43/118.16 (~P6(a71,x58081,a86)),
% 117.43/118.16 inference(scs_inference,[],[1758,7,668,52,27,37,38])).
% 117.43/118.16 cnf(5812,plain,
% 117.43/118.16 (P6(f48(a84,a84),f51(a84,a84),a84)),
% 117.43/118.16 inference(scs_inference,[],[1758,1778,5338,7,668,52,27,37,38,50,51])).
% 117.43/118.16 cnf(5826,plain,
% 117.43/118.16 (~P6(a71,x58261,a89)),
% 117.43/118.16 inference(scs_inference,[],[359,1758,1760,1778,1780,5338,7,14,668,52,27,37,38,50,51,69,29,32,102,99,70,39])).
% 117.43/118.16 cnf(5828,plain,
% 117.43/118.16 (P6(a71,x58281,a87)),
% 117.43/118.16 inference(scs_inference,[],[359,1758,1760,1778,1780,5338,7,14,668,52,27,37,38,50,51,69,29,32,102,99,70,39,23])).
% 117.43/118.16 cnf(5834,plain,
% 117.43/118.16 (P6(x58341,a71,a81)),
% 117.43/118.16 inference(scs_inference,[],[359,1758,1760,1778,1780,5338,5243,7,799,14,668,52,27,37,38,50,51,69,29,32,102,99,70,39,23,15,31,22])).
% 117.43/118.16 cnf(5836,plain,
% 117.43/118.16 (~P1(f77(a69,a69),f75(a69))),
% 117.43/118.16 inference(scs_inference,[],[359,1758,1760,1778,1780,5338,5788,5243,7,799,14,668,52,27,37,38,50,51,69,29,32,102,99,70,39,23,15,31,22,20])).
% 117.43/118.16 cnf(5842,plain,
% 117.43/118.16 (~P6(x58421,f45(a5,a5),a85)),
% 117.43/118.16 inference(scs_inference,[],[359,1758,1760,1778,1780,5338,5788,5243,7,799,14,668,52,27,37,38,50,51,69,29,32,102,99,70,39,23,15,31,22,20,30,71,28])).
% 117.43/118.16 cnf(5846,plain,
% 117.43/118.16 (P1(f4(a71),a71)),
% 117.43/118.16 inference(scs_inference,[],[359,1758,1760,1778,1780,5338,5788,5243,7,799,14,668,52,27,37,38,50,51,69,29,32,102,99,70,39,23,15,31,22,20,30,71,28,36,21])).
% 117.43/118.16 cnf(5848,plain,
% 117.43/118.16 (P1(f23(a65,a3),f75(a65))),
% 117.43/118.16 inference(scs_inference,[],[359,1758,1760,1778,1780,5338,5788,5584,5243,7,799,14,668,52,27,37,38,50,51,69,29,32,102,99,70,39,23,15,31,22,20,30,71,28,36,21,17])).
% 117.43/118.16 cnf(5854,plain,
% 117.43/118.16 (P6(a69,x58541,a87)),
% 117.43/118.16 inference(rename_variables,[],[5730])).
% 117.43/118.16 cnf(5859,plain,
% 117.43/118.16 (~P2(a87,a85)),
% 117.43/118.16 inference(scs_inference,[],[1,359,1758,1760,1778,1780,5097,5714,5730,5854,5738,5338,5788,5584,5243,7,799,14,668,52,27,37,38,50,51,69,29,32,102,99,70,39,23,15,31,22,20,30,71,28,36,21,17,41,78,79,94])).
% 117.43/118.16 cnf(5867,plain,
% 117.43/118.16 (~P6(a69,a71,a76)),
% 117.43/118.16 inference(scs_inference,[],[1,359,1758,1760,1778,1780,5097,5714,5730,5854,5738,5338,5788,5584,5243,5433,5093,7,12,6,799,14,668,52,27,37,38,50,51,69,29,32,102,99,70,39,23,15,31,22,20,30,71,28,36,21,17,41,78,79,94,47,49,48])).
% 117.43/118.16 cnf(5870,plain,
% 117.43/118.16 (P1(x58701,f48(a85,a85))),
% 117.43/118.16 inference(rename_variables,[],[678])).
% 117.43/118.16 cnf(5873,plain,
% 117.43/118.16 (~P1(x58731,f46(a73,a73))),
% 117.43/118.16 inference(rename_variables,[],[953])).
% 117.43/118.16 cnf(5885,plain,
% 117.43/118.16 (P6(a56,a56,a8)),
% 117.43/118.16 inference(scs_inference,[],[1,359,1758,1760,1778,1780,5097,5714,5730,5854,5738,5338,5788,5740,5647,5584,5465,5243,5631,5433,5093,7,12,6,678,5870,953,5873,799,14,668,52,27,37,38,50,51,69,29,32,102,99,70,39,23,15,31,22,20,30,71,28,36,21,17,41,78,79,94,47,49,48,45,46,44,34,43,81,33])).
% 117.43/118.16 cnf(5893,plain,
% 117.43/118.16 (~P6(a71,a58,a76)),
% 117.43/118.16 inference(scs_inference,[],[1,359,1758,1760,1778,1780,5097,5708,5714,5730,5854,5732,5738,5338,5772,5788,5740,5647,5584,5736,5465,5243,5631,5433,5093,7,12,6,678,5870,953,5873,799,14,668,52,27,37,38,50,51,69,29,32,102,99,70,39,23,15,31,22,20,30,71,28,36,21,17,41,78,79,94,47,49,48,45,46,44,34,43,81,33,91,74,1341])).
% 117.43/118.16 cnf(5895,plain,
% 117.43/118.16 (P1(f77(a56,a56),a56)),
% 117.43/118.16 inference(scs_inference,[],[1,359,1758,1760,1778,1780,5097,5708,5714,5730,5854,5732,5738,5338,5772,5788,5740,5647,5584,5736,5465,5243,5631,5433,5093,7,12,6,678,5870,953,5873,799,14,668,52,27,37,38,50,51,69,29,32,102,99,70,39,23,15,31,22,20,30,71,28,36,21,17,41,78,79,94,47,49,48,45,46,44,34,43,81,33,91,74,1341,53])).
% 117.43/118.16 cnf(5897,plain,
% 117.43/118.16 (P1(f78(a56,a56),a56)),
% 117.43/118.16 inference(scs_inference,[],[1,359,1758,1760,1778,1780,5097,5708,5714,5730,5854,5732,5738,5338,5772,5788,5740,5647,5584,5736,5465,5243,5631,5433,5093,7,12,6,678,5870,953,5873,799,14,668,52,27,37,38,50,51,69,29,32,102,99,70,39,23,15,31,22,20,30,71,28,36,21,17,41,78,79,94,47,49,48,45,46,44,34,43,81,33,91,74,1341,53,80])).
% 117.43/118.16 cnf(5910,plain,
% 117.43/118.16 (~P6(f48(a85,a85),x59101,a84)),
% 117.43/118.16 inference(scs_inference,[],[5836,678,27,37])).
% 117.43/118.16 cnf(5914,plain,
% 117.43/118.16 (P6(f48(a82,a82),f51(a82,a82),a82)),
% 117.43/118.16 inference(scs_inference,[],[1807,5836,678,27,37,38,52])).
% 117.43/118.16 cnf(5924,plain,
% 117.43/118.16 (P6(f48(a89,a89),f51(a89,a89),a89)),
% 117.43/118.16 inference(scs_inference,[],[1807,1809,1987,5658,5836,678,27,37,38,52,29,69,99,32,51])).
% 117.43/118.16 cnf(5932,plain,
% 117.43/118.16 (P6(f48(a85,a85),x59321,a87)),
% 117.43/118.16 inference(scs_inference,[],[366,1807,1809,1987,1989,5658,5836,678,27,37,38,52,29,69,99,32,51,102,50,70,23])).
% 117.43/118.16 cnf(5940,plain,
% 117.43/118.16 (P6(x59401,f48(a85,a85),a81)),
% 117.43/118.16 inference(scs_inference,[],[366,1807,1809,1987,1989,5658,5836,5280,678,27,37,38,52,29,69,99,32,51,102,50,70,23,39,31,15,22])).
% 117.43/118.16 cnf(5942,plain,
% 117.43/118.16 (~P1(f78(a69,a69),f75(a69))),
% 117.43/118.16 inference(scs_inference,[],[366,1807,1809,1987,1989,5658,5796,5836,5280,678,27,37,38,52,29,69,99,32,51,102,50,70,23,39,31,15,22,20])).
% 117.43/118.16 cnf(5954,plain,
% 117.43/118.16 (P1(f32(a71,a2),a71)),
% 117.43/118.16 inference(scs_inference,[],[1,366,1807,1809,1987,1989,5658,5806,5796,5836,5783,5280,678,27,37,38,52,29,69,99,32,51,102,50,70,23,39,31,15,22,20,30,71,28,36,17,41])).
% 117.43/118.16 cnf(5957,plain,
% 117.43/118.16 (P1(f52(a2,a71),a71)),
% 117.43/118.16 inference(scs_inference,[],[1,366,1807,1809,1987,1989,5658,5806,5834,5796,5836,5783,5280,678,27,37,38,52,29,69,99,32,51,102,50,70,23,39,31,15,22,20,30,71,28,36,17,41,79])).
% 117.43/118.16 cnf(5969,plain,
% 117.43/118.16 (~P1(x59691,f46(a73,a73))),
% 117.43/118.16 inference(rename_variables,[],[953])).
% 117.43/118.16 cnf(5979,plain,
% 117.43/118.16 (P6(a71,a71,a83)),
% 117.43/118.16 inference(scs_inference,[],[1,366,1807,1809,1987,1989,5779,5658,5748,5806,5828,5834,5796,5836,5848,5783,5846,5280,5740,5269,5584,5788,678,953,27,37,38,52,29,69,99,32,51,102,50,70,23,39,31,15,22,20,30,71,28,36,17,41,79,47,94,78,48,49,45,46,44,34])).
% 117.43/118.16 cnf(5986,plain,
% 117.43/118.16 (P3(a87,a8)),
% 117.43/118.16 inference(scs_inference,[],[1,366,1807,1809,1987,1989,5779,5658,5748,5806,5828,5834,5885,5796,5836,5895,5848,5783,5846,5280,5730,5740,5269,5584,5788,678,953,5969,27,37,38,52,29,69,99,32,51,102,50,70,23,39,31,15,22,20,30,71,28,36,17,41,79,47,94,78,48,49,45,46,44,34,43,81,100])).
% 117.43/118.16 cnf(5987,plain,
% 117.43/118.16 (P6(a69,x59871,a87)),
% 117.43/118.16 inference(rename_variables,[],[5730])).
% 117.43/118.16 cnf(5989,plain,
% 117.43/118.16 (~P5(a87,a8)),
% 117.43/118.16 inference(scs_inference,[],[1,366,1807,1809,1987,1989,5779,5658,5748,5806,5828,5834,5885,5796,5836,5895,5848,5783,5846,5280,5730,5987,5740,5269,5584,5788,678,953,5969,27,37,38,52,29,69,99,32,51,102,50,70,23,39,31,15,22,20,30,71,28,36,17,41,79,47,94,78,48,49,45,46,44,34,43,81,100,104])).
% 117.43/118.16 cnf(5992,plain,
% 117.43/118.16 (P6(a71,a71,a8)),
% 117.43/118.16 inference(scs_inference,[],[1,366,1807,1809,1987,1989,5779,5658,5748,5806,5828,5834,5885,5796,5836,5895,5848,5783,5846,5280,5730,5987,5740,5269,5584,5788,678,953,5969,27,37,38,52,29,69,99,32,51,102,50,70,23,39,31,15,22,20,30,71,28,36,17,41,79,47,94,78,48,49,45,46,44,34,43,81,100,104,33])).
% 117.43/118.16 cnf(6002,plain,
% 117.43/118.16 (P1(f77(a71,a71),a71)),
% 117.43/118.16 inference(scs_inference,[],[1,366,1807,1809,1987,1989,5779,5658,5748,5806,5826,5828,5834,5885,5893,5796,5836,5895,5848,5783,5846,5280,5730,5987,5740,5269,5435,5584,5788,678,953,5969,14,27,37,38,52,29,69,99,32,51,102,50,70,23,39,31,15,22,20,30,71,28,36,17,41,79,47,94,78,48,49,45,46,44,34,43,81,100,104,33,74,96,1346,53])).
% 117.43/118.16 cnf(6004,plain,
% 117.43/118.16 (P1(f78(a71,a71),a71)),
% 117.43/118.16 inference(scs_inference,[],[1,366,1807,1809,1987,1989,5779,5658,5748,5806,5826,5828,5834,5885,5893,5796,5836,5895,5848,5783,5846,5280,5730,5987,5740,5269,5435,5584,5788,678,953,5969,14,27,37,38,52,29,69,99,32,51,102,50,70,23,39,31,15,22,20,30,71,28,36,17,41,79,47,94,78,48,49,45,46,44,34,43,81,100,104,33,74,96,1346,53,80])).
% 117.43/118.16 cnf(6014,plain,
% 117.43/118.16 (~P6(a3,x60141,a86)),
% 117.43/118.16 inference(scs_inference,[],[5251,8,17,38])).
% 117.43/118.16 cnf(6018,plain,
% 117.43/118.16 (P6(f48(a88,a88),f51(a88,a88),a88)),
% 117.43/118.16 inference(scs_inference,[],[1996,5251,8,604,17,38,37,52])).
% 117.43/118.16 cnf(6036,plain,
% 117.43/118.16 (P6(a3,x60361,a87)),
% 117.43/118.16 inference(scs_inference,[],[372,1996,1998,1210,1214,5438,5251,8,668,604,17,38,37,52,99,32,69,50,51,102,70,39,23])).
% 117.43/118.16 cnf(6046,plain,
% 117.43/118.16 (P6(x60461,a3,a81)),
% 117.43/118.16 inference(scs_inference,[],[372,1996,1998,1210,1214,5438,5794,5251,5375,14,8,668,604,17,38,37,52,99,32,69,50,51,102,70,39,23,31,15,30,20,22])).
% 117.43/118.16 cnf(6050,plain,
% 117.43/118.16 (~P6(x60501,a58,a85)),
% 117.43/118.16 inference(scs_inference,[],[372,1996,1998,1210,1214,5438,5794,5251,5375,14,8,668,604,17,38,37,52,99,32,69,50,51,102,70,39,23,31,15,30,20,22,71,28])).
% 117.43/118.16 cnf(6052,plain,
% 117.43/118.16 (~P6(a3,x60521,a5)),
% 117.43/118.16 inference(scs_inference,[],[372,1996,1998,1210,1214,5438,5794,5251,5375,14,8,668,604,17,38,37,52,99,32,69,50,51,102,70,39,23,31,15,30,20,22,71,28,36])).
% 117.43/118.16 cnf(6056,plain,
% 117.43/118.16 (~P2(a83,a86)),
% 117.43/118.16 inference(scs_inference,[],[1,372,1996,1998,1210,1214,5808,5438,5979,5794,5251,5375,678,14,8,668,604,17,38,37,52,99,32,69,50,51,102,70,39,23,31,15,30,20,22,71,28,36,33,94])).
% 117.43/118.16 cnf(6077,plain,
% 117.43/118.16 (P1(f79(a71,a71),a71)),
% 117.43/118.16 inference(scs_inference,[],[1,372,1996,1998,1210,1214,5808,5438,5979,5992,5794,5897,6002,5942,5251,5375,2009,5796,5433,678,953,14,8,668,604,17,38,37,52,99,32,69,50,51,102,70,39,23,31,15,30,20,22,71,28,36,33,94,48,47,45,49,46,44,34,43,81])).
% 117.43/118.16 cnf(6080,plain,
% 117.43/118.16 (P1(x60801,a3)),
% 117.43/118.16 inference(rename_variables,[],[8])).
% 117.43/118.16 cnf(6083,plain,
% 117.43/118.16 (~P1(f23(a2,a3),a2)),
% 117.43/118.16 inference(scs_inference,[],[1,372,1996,1998,1210,1214,5320,5501,5808,5438,5979,5992,5794,5897,6002,5942,5251,5375,2009,5796,5433,678,953,14,8,6080,668,604,17,38,37,52,99,32,69,50,51,102,70,39,23,31,15,30,20,22,71,28,36,33,94,48,47,45,49,46,44,34,43,81,93,98])).
% 117.43/118.16 cnf(6096,plain,
% 117.43/118.16 (P1(f23(a2,a3),f75(a2))),
% 117.43/118.16 inference(scs_inference,[],[6083,17])).
% 117.43/118.16 cnf(6114,plain,
% 117.43/118.16 (~P6(f49(a74,a91),f50(a74,a91),a91)),
% 117.43/118.16 inference(scs_inference,[],[395,1223,1227,5552,6083,604,17,38,37,52,50,69,99,51,70,102])).
% 117.43/118.16 cnf(6118,plain,
% 117.43/118.16 (P6(f75(a58),x61181,a87)),
% 117.43/118.16 inference(scs_inference,[],[395,1223,1227,5552,6083,604,17,38,37,52,50,69,99,51,70,102,39,23])).
% 117.43/118.16 cnf(6120,plain,
% 117.43/118.16 (~P6(f48(a5,a5),x61201,a85)),
% 117.43/118.16 inference(scs_inference,[],[395,1223,1227,5552,6083,668,604,17,38,37,52,50,69,99,51,70,102,39,23,31])).
% 117.43/118.16 cnf(6122,plain,
% 117.43/118.16 (P1(f19(a62,a58),a65)),
% 117.43/118.16 inference(scs_inference,[],[395,1223,1227,5552,6083,5468,668,604,17,38,37,52,50,69,99,51,70,102,39,23,31,15])).
% 117.43/118.16 cnf(6124,plain,
% 117.43/118.16 (P6(x61241,f75(a58),a81)),
% 117.43/118.16 inference(scs_inference,[],[395,1223,1227,5552,6083,5468,668,604,17,38,37,52,50,69,99,51,70,102,39,23,31,15,22])).
% 117.43/118.16 cnf(6126,plain,
% 117.43/118.16 (~P6(x61261,f48(a5,a5),a86)),
% 117.43/118.16 inference(scs_inference,[],[395,1223,1227,5552,6083,5468,668,604,17,38,37,52,50,69,99,51,70,102,39,23,31,15,22,30])).
% 117.43/118.16 cnf(6128,plain,
% 117.43/118.16 (~P1(a55,f75(a56))),
% 117.43/118.16 inference(scs_inference,[],[2,395,1223,1227,5552,6083,5468,668,604,17,38,37,52,50,69,99,51,70,102,39,23,31,15,22,30,20])).
% 117.43/118.16 cnf(6130,plain,
% 117.43/118.16 (P6(f49(a74,a91),f50(a74,a91),a74)),
% 117.43/118.16 inference(scs_inference,[],[2,395,1223,1227,5552,6083,5468,668,604,17,38,37,52,50,69,99,51,70,102,39,23,31,15,22,30,20,71])).
% 117.43/118.16 cnf(6136,plain,
% 117.43/118.16 (P6(f48(a85,a85),a56,a8)),
% 117.43/118.16 inference(scs_inference,[],[2,395,1223,1227,5552,6083,5468,678,668,604,17,38,37,52,50,69,99,51,70,102,39,23,31,15,22,30,20,71,28,36,33])).
% 117.43/118.16 cnf(6138,plain,
% 117.43/118.16 (~P2(a83,a84)),
% 117.43/118.16 inference(scs_inference,[],[2,395,1223,1227,5552,5355,5294,6083,5468,678,668,604,17,38,37,52,50,69,99,51,70,102,39,23,31,15,22,30,20,71,28,36,33,94])).
% 117.43/118.16 cnf(6148,plain,
% 117.43/118.16 (~P6(a62,a65,a76)),
% 117.43/118.16 inference(scs_inference,[],[2,395,1223,1227,5552,5355,5294,6083,5468,10,5225,5,5421,678,953,668,604,17,38,37,52,50,69,99,51,70,102,39,23,31,15,22,30,20,71,28,36,33,94,47,48,49,45])).
% 117.43/118.16 cnf(6182,plain,
% 117.43/118.16 (P1(f40(a65,a58),f75(a65))),
% 117.43/118.16 inference(scs_inference,[],[5271,17])).
% 117.43/118.16 cnf(6198,plain,
% 117.43/118.16 (~P6(f49(a5,a82),f50(a5,a82),a82)),
% 117.43/118.16 inference(scs_inference,[],[402,1193,1197,5859,6096,5271,17,38,52,50,69,70,51,99,102])).
% 117.43/118.16 cnf(6204,plain,
% 117.43/118.16 (~P1(f19(a62,a58),f75(a65))),
% 117.43/118.16 inference(scs_inference,[],[402,1193,1197,5859,6096,6122,6128,5271,17,38,52,50,69,70,51,99,102,23,31,20])).
% 117.43/118.16 cnf(6208,plain,
% 117.43/118.16 (P6(x62081,f75(a2),a81)),
% 117.43/118.16 inference(scs_inference,[],[402,1193,1197,5859,6096,6122,6128,5271,17,38,52,50,69,70,51,99,102,23,31,20,30,22])).
% 117.43/118.16 cnf(6210,plain,
% 117.43/118.16 (P6(f49(a5,a82),f50(a5,a82),a5)),
% 117.43/118.16 inference(scs_inference,[],[402,1193,1197,5859,6096,6122,6128,5271,17,38,52,50,69,70,51,99,102,23,31,20,30,22,71])).
% 117.43/118.16 cnf(6214,plain,
% 117.43/118.16 (P6(f75(a2),f75(a2),a8)),
% 117.43/118.16 inference(scs_inference,[],[402,1193,1197,5859,6096,6122,6128,5271,17,38,52,50,69,70,51,99,102,23,31,20,30,22,71,36,33])).
% 117.43/118.16 cnf(6216,plain,
% 117.43/118.16 (~P2(a81,a76)),
% 117.43/118.16 inference(scs_inference,[],[402,1193,1197,5859,5867,6096,6122,6128,5271,5834,17,38,52,50,69,70,51,99,102,23,31,20,30,22,71,36,33,94])).
% 117.43/118.16 cnf(6231,plain,
% 117.43/118.16 (P6(f75(a2),f75(a2),a83)),
% 117.43/118.16 inference(scs_inference,[],[2,402,1193,1197,5859,5867,6096,6122,6128,5271,5834,17,38,52,50,69,70,51,99,102,23,31,20,30,22,71,36,33,94,47,48,49,45,46,44,34])).
% 117.43/118.16 cnf(6239,plain,
% 117.43/118.16 (P6(a56,a58,a9)),
% 117.43/118.16 inference(scs_inference,[],[2,402,1193,1197,5859,5867,6096,6122,6128,6004,5754,5271,5447,5834,604,17,38,52,50,69,70,51,99,102,23,31,20,30,22,71,36,33,94,47,48,49,45,46,44,34,43,1341,88,40])).
% 117.43/118.16 cnf(6242,plain,
% 117.43/118.16 (P1(f72(a58,a56),a56)),
% 117.43/118.16 inference(scs_inference,[],[2,402,1193,1197,5859,5867,6096,6122,6128,6004,5754,5271,292,5447,5834,14,604,17,38,52,50,69,70,51,99,102,23,31,20,30,22,71,36,33,94,47,48,49,45,46,44,34,43,1341,88,40,76])).
% 117.43/118.16 cnf(6259,plain,
% 117.43/118.16 (~P6(f49(a5,a76),f50(a5,a76),a76)),
% 117.43/118.16 inference(scs_inference,[],[409,1042,1475,5756,5277,17,52,69,50,70,99,102])).
% 117.43/118.16 cnf(6265,plain,
% 117.43/118.16 (P6(f49(a5,a76),f50(a5,a76),a5)),
% 117.43/118.16 inference(scs_inference,[],[409,1042,1475,5756,6242,5277,17,52,69,50,70,99,102,51,20,71])).
% 117.43/118.16 cnf(6267,plain,
% 117.43/118.16 (P1(f38(a56,a58),a56)),
% 117.43/118.16 inference(scs_inference,[],[409,1042,1475,6239,5756,6242,5277,17,52,69,50,70,99,102,51,20,71,65])).
% 117.43/118.16 cnf(6272,plain,
% 117.43/118.16 (P6(a3,a56,a8)),
% 117.43/118.16 inference(scs_inference,[],[2,409,1042,1475,6239,5756,6242,5277,5515,8,17,52,69,50,70,99,102,51,20,71,65,105,33])).
% 117.43/118.16 cnf(6274,plain,
% 117.43/118.16 (P1(f32(a62,a56),a62)),
% 117.43/118.16 inference(scs_inference,[],[2,409,1042,1475,6239,5756,6242,5277,5057,5515,8,17,52,69,50,70,99,102,51,20,71,65,105,33,41])).
% 117.43/118.16 cnf(6277,plain,
% 117.43/118.16 (~P2(a9,a85)),
% 117.43/118.16 inference(scs_inference,[],[2,409,1042,1475,6239,6050,5756,6242,5277,5057,5515,8,17,52,69,50,70,99,102,51,20,71,65,105,33,41,94])).
% 117.43/118.16 cnf(6280,plain,
% 117.43/118.16 (~P6(a65,a62,a90)),
% 117.43/118.16 inference(scs_inference,[],[2,409,1042,1475,6239,6050,5756,6242,5277,5057,5515,10,5,8,17,52,69,50,70,99,102,51,20,71,65,105,33,41,94,47])).
% 117.43/118.16 cnf(6294,plain,
% 117.43/118.16 (P1(x62941,a3)),
% 117.43/118.16 inference(rename_variables,[],[8])).
% 117.43/118.16 cnf(6298,plain,
% 117.43/118.16 (P1(f78(a3,a56),a56)),
% 117.43/118.16 inference(scs_inference,[],[2,409,1042,1475,6239,6050,5756,6182,6242,6077,5277,5057,5515,5271,2009,10,5473,5,5433,5635,953,8,6294,17,52,69,50,70,99,102,51,20,71,65,105,33,41,94,47,48,49,45,46,44,34,43,80])).
% 117.43/118.16 cnf(6300,plain,
% 117.43/118.16 (P1(f32(a62,a56),a65)),
% 117.43/118.16 inference(scs_inference,[],[2,409,1042,1475,6239,6050,5756,6182,6242,6077,5277,5057,5515,5271,2009,10,5473,5,5433,5635,953,8,6294,17,52,69,50,70,99,102,51,20,71,65,105,33,41,94,47,48,49,45,46,44,34,43,80,15])).
% 117.43/118.16 cnf(6302,plain,
% 117.43/118.16 (P1(f77(a56,a3),a56)),
% 117.43/118.16 inference(scs_inference,[],[2,409,1042,1475,6239,6050,5756,6182,6242,6077,5277,5057,5515,5271,2009,10,5473,5,5433,5635,953,8,6294,17,52,69,50,70,99,102,51,20,71,65,105,33,41,94,47,48,49,45,46,44,34,43,80,15,54])).
% 117.43/118.16 cnf(6305,plain,
% 117.43/118.16 (P1(f22(a2,a65),f75(a65))),
% 117.43/118.16 inference(scs_inference,[],[5372,17])).
% 117.43/118.16 cnf(6327,plain,
% 117.43/118.16 (P1(f52(a56,a2),a2)),
% 117.43/118.16 inference(scs_inference,[],[2,423,1465,1462,6056,6267,5372,4927,678,17,52,69,50,99,51,70,102,20,71,33,79])).
% 117.43/118.16 cnf(6330,plain,
% 117.43/118.16 (P1(f29(a2,a56),a2)),
% 117.43/118.16 inference(scs_inference,[],[2,423,1465,1462,6056,6267,5372,4921,4927,678,17,52,69,50,99,51,70,102,20,71,33,79,78])).
% 117.43/118.16 cnf(6335,plain,
% 117.43/118.16 (~P2(a81,a90)),
% 117.43/118.16 inference(scs_inference,[],[2,423,1465,1462,6056,6280,6267,5372,4921,4927,5089,6083,6096,678,17,52,69,50,99,51,70,102,20,71,33,79,78,47,94])).
% 117.43/118.16 cnf(6350,plain,
% 117.43/118.16 (P1(x63501,f48(a85,a85))),
% 117.43/118.16 inference(rename_variables,[],[678])).
% 117.43/118.16 cnf(6355,plain,
% 117.43/118.16 (P3(a81,a8)),
% 117.43/118.16 inference(scs_inference,[],[2,423,1465,1462,6056,6280,6267,6214,6208,6300,5372,4921,4927,5089,5367,6083,2009,6096,5473,5433,12,5635,6,678,6350,953,17,52,69,50,99,51,70,102,20,71,33,79,78,47,94,48,45,49,46,44,34,43,100])).
% 117.43/118.16 cnf(6356,plain,
% 117.43/118.16 (P6(x63561,f75(a2),a81)),
% 117.43/118.16 inference(rename_variables,[],[6208])).
% 117.43/118.16 cnf(6358,plain,
% 117.43/118.16 (~P5(a81,a8)),
% 117.43/118.16 inference(scs_inference,[],[2,423,1465,1462,6056,6280,6267,6214,6208,6356,6300,5372,4921,4927,5089,5367,6083,2009,6096,5473,5433,12,5635,6,678,6350,953,17,52,69,50,99,51,70,102,20,71,33,79,78,47,94,48,45,49,46,44,34,43,100,104])).
% 117.43/118.16 cnf(6400,plain,
% 117.43/118.17 (~P2(a8,a86)),
% 117.43/118.17 inference(scs_inference,[],[2,430,1045,3244,3247,6138,6272,6327,6014,5107,5025,6128,3,953,604,17,52,69,70,99,50,51,102,20,71,33,47,48,94])).
% 117.43/118.17 cnf(6409,plain,
% 117.43/118.17 (~P6(a62,a65,a10)),
% 117.43/118.17 inference(scs_inference,[],[2,430,1045,3244,3247,6138,6272,6327,6014,5752,5107,5025,5165,10,5,6128,3,953,604,17,52,69,70,99,50,51,102,20,71,33,47,48,94,45,49,46,44])).
% 117.43/118.17 cnf(6411,plain,
% 117.43/118.17 (P6(a56,f75(a58),a83)),
% 117.43/118.17 inference(scs_inference,[],[2,430,1045,3244,3247,6138,6272,6327,6014,5752,5107,5025,5165,10,5,6128,3,953,604,17,52,69,70,99,50,51,102,20,71,33,47,48,94,45,49,46,44,34])).
% 117.43/118.17 cnf(6444,plain,
% 117.43/118.17 (~P1(f14(a56,a65),a65)),
% 117.43/118.17 inference(scs_inference,[],[2,444,1286,1283,1300,6216,6330,5004,5065,17,52,69,99,51,70,102,50,20,71,77])).
% 117.43/118.17 cnf(6449,plain,
% 117.43/118.17 (~P6(f75(a62),a65,a90)),
% 117.43/118.17 inference(scs_inference,[],[2,444,1286,1283,1300,6216,6330,5004,5065,1703,11,8,17,52,69,99,51,70,102,50,20,71,77,33,47])).
% 117.43/118.17 cnf(6451,plain,
% 117.43/118.17 (~P2(a87,a10)),
% 117.43/118.17 inference(scs_inference,[],[2,444,1286,1283,1300,6216,6409,6330,5004,5081,5065,1703,11,8,17,52,69,99,51,70,102,50,20,71,77,33,47,94])).
% 117.43/118.17 cnf(6456,plain,
% 117.43/118.17 (~P6(f75(a62),a65,a91)),
% 117.43/118.17 inference(scs_inference,[],[2,444,1286,1283,1300,6216,6409,6330,5004,5081,5065,5285,1703,5421,11,8,17,52,69,99,51,70,102,50,20,71,77,33,47,94,48,49])).
% 117.43/118.17 cnf(6461,plain,
% 117.43/118.17 (~P6(a71,a69,a10)),
% 117.43/118.17 inference(scs_inference,[],[2,444,1286,1283,1300,6216,6409,6330,5954,5004,5081,5065,5285,1703,12,5421,6,953,11,8,17,52,69,99,51,70,102,50,20,71,77,33,47,94,48,49,46,44])).
% 117.43/118.17 cnf(6463,plain,
% 117.43/118.17 (P6(a3,a56,a83)),
% 117.43/118.17 inference(scs_inference,[],[2,444,1286,1283,1300,6216,6409,6330,5954,5004,5081,5065,5285,1703,12,5421,6,953,11,8,17,52,69,99,51,70,102,50,20,71,77,33,47,94,48,49,46,44,34])).
% 117.43/118.17 cnf(6464,plain,
% 117.43/118.17 (P1(x64641,a3)),
% 117.43/118.17 inference(rename_variables,[],[8])).
% 117.43/118.17 cnf(6468,plain,
% 117.43/118.17 (P1(f79(a56,a3),a56)),
% 117.43/118.17 inference(scs_inference,[],[2,444,1286,1283,1300,6216,6409,6330,5954,5004,5081,5065,2009,5285,1703,5433,12,5421,6,953,11,8,6464,17,52,69,99,51,70,102,50,20,71,77,33,47,94,48,49,46,44,34,43,81])).
% 117.43/118.17 cnf(6477,plain,
% 117.43/118.17 (P1(f77(a3,a56),a56)),
% 117.43/118.17 inference(scs_inference,[],[2,444,1286,1283,1300,6216,6409,6231,6120,6126,5187,6330,5954,5004,5081,5065,2009,5285,1703,5433,12,5421,6,953,11,8,6464,17,52,69,99,51,70,102,50,20,71,77,33,47,94,48,49,46,44,34,43,81,91,75,53])).
% 117.43/118.17 cnf(6485,plain,
% 117.43/118.17 (P6(f48(a73,a87),f51(a73,a87),a73)),
% 117.43/118.17 inference(scs_inference,[],[3589,6444,17,52])).
% 117.43/118.17 cnf(6497,plain,
% 117.43/118.17 (P6(f45(a73,a87),f46(a73,a87),a73)),
% 117.43/118.17 inference(scs_inference,[],[450,3589,3592,6451,6444,17,52,69,50,99,51,102,70])).
% 117.43/118.17 cnf(6503,plain,
% 117.43/118.17 (P6(f75(a65),a65,a9)),
% 117.43/118.17 inference(scs_inference,[],[450,3589,3592,6451,6477,6444,6305,17,52,69,50,99,51,102,70,20,71,40])).
% 117.43/118.17 cnf(6515,plain,
% 117.43/118.17 (~P1(x65151,f46(a73,a73))),
% 117.43/118.17 inference(rename_variables,[],[953])).
% 117.43/118.17 cnf(6522,plain,
% 117.43/118.17 (P1(f60(a65,a58),a65)),
% 117.43/118.17 inference(scs_inference,[],[450,3589,3592,6451,6463,6477,6444,6052,6305,5957,596,10,5,6128,12,6,3,953,6515,14,604,17,52,69,50,99,51,102,70,20,71,40,94,48,46,44,81,43,1346,76])).
% 117.43/118.17 cnf(6541,plain,
% 117.43/118.17 (~P6(f41(a9,a85),f47(a9,a85),a85)),
% 117.43/118.17 inference(scs_inference,[],[3231,3234,6277,4970,17,52,69,99])).
% 117.48/118.17 cnf(6543,plain,
% 117.48/118.17 (P6(f41(a9,a85),f47(a9,a85),a9)),
% 117.48/118.17 inference(scs_inference,[],[3231,3234,6277,4970,17,52,69,99,50])).
% 117.48/118.17 cnf(6555,plain,
% 117.48/118.17 (~P2(a81,a10)),
% 117.48/118.17 inference(scs_inference,[],[456,3231,3234,6461,6277,6522,4970,5738,17,52,69,99,50,70,51,102,20,71,94])).
% 117.48/118.17 cnf(6565,plain,
% 117.48/118.17 (P6(f45(a73,a87),f46(a73,a87),a74)),
% 117.48/118.17 inference(scs_inference,[],[2,456,3231,3234,6461,6277,6497,6522,4970,5738,6083,5285,6096,5421,13,799,17,52,69,99,50,70,51,102,20,71,94,48,46,43,91])).
% 117.48/118.17 cnf(6599,plain,
% 117.48/118.17 (P1(f32(a59,a56),a59)),
% 117.48/118.17 inference(scs_inference,[],[2,515,3256,3259,6335,6411,6124,6468,5010,5397,17,52,69,99,50,102,51,70,20,71,105,41])).
% 117.48/118.17 cnf(6604,plain,
% 117.48/118.17 (~P2(a74,a91)),
% 117.48/118.17 inference(scs_inference,[],[2,515,3256,3259,6335,6411,6124,6130,6114,6468,5010,5397,6128,3,17,52,69,99,50,102,51,70,20,71,105,41,48,94])).
% 117.48/118.17 cnf(6606,plain,
% 117.48/118.17 (~P6(a56,f45(a5,a5),a10)),
% 117.48/118.17 inference(scs_inference,[],[2,515,3256,3259,6335,6411,6124,6130,6114,6468,5010,5397,6128,3,799,17,52,69,99,50,102,51,70,20,71,105,41,48,94,46])).
% 117.48/118.17 cnf(6609,plain,
% 117.48/118.17 (~P6(a62,f46(a73,a73),a74)),
% 117.48/118.17 inference(scs_inference,[],[2,515,3256,3259,6335,6411,6124,6130,6114,6468,5010,5397,6274,6128,3,953,799,17,52,69,99,50,102,51,70,20,71,105,41,48,94,46,43])).
% 117.48/118.17 cnf(6642,plain,
% 117.48/118.17 (P1(f52(a56,a59),a59)),
% 117.48/118.17 inference(scs_inference,[],[2,523,4482,4485,6400,6599,5019,5419,17,69,52,99,102,50,70,51,20,71,79])).
% 117.48/118.17 cnf(6659,plain,
% 117.48/118.17 (P3(a87,a9)),
% 117.48/118.17 inference(scs_inference,[],[2,523,4482,4485,6400,4985,6485,6599,6503,5209,5019,5419,5828,5473,10,5,5635,13,668,17,69,52,99,102,50,70,51,20,71,79,78,48,94,46,43,91,100])).
% 117.48/118.17 cnf(6660,plain,
% 117.48/118.17 (P6(f75(a65),x66601,a87)),
% 117.48/118.17 inference(rename_variables,[],[5209])).
% 117.48/118.17 cnf(6662,plain,
% 117.48/118.17 (~P5(a87,a9)),
% 117.48/118.17 inference(scs_inference,[],[2,523,4482,4485,6400,4985,6485,6599,6503,5209,6660,5019,5419,5828,5473,10,5,5635,13,668,17,69,52,99,102,50,70,51,20,71,79,78,48,94,46,43,91,100,104])).
% 117.48/118.17 cnf(6692,plain,
% 117.48/118.17 (~P2(a5,a82)),
% 117.48/118.17 inference(scs_inference,[],[526,4495,4498,6555,6210,6198,6642,1723,17,69,99,52,102,51,70,50,20,71,94])).
% 117.48/118.17 cnf(6694,plain,
% 117.48/118.17 (~P6(a56,a58,a10)),
% 117.48/118.17 inference(scs_inference,[],[2,526,4495,4498,6555,6210,6198,6642,1723,14,17,69,99,52,102,51,70,50,20,71,94,46])).
% 117.48/118.17 cnf(6703,plain,
% 117.48/118.17 (~P1(f14(a56,a2),a2)),
% 117.48/118.17 inference(scs_inference,[],[2,320,526,4495,4498,6555,6210,6543,6198,6541,6642,6204,1723,5298,5468,14,17,69,99,52,102,51,70,50,20,71,94,46,43,91,108,77])).
% 117.48/118.17 cnf(6733,plain,
% 117.48/118.17 (~P1(a55,f75(a59))),
% 117.48/118.17 inference(scs_inference,[],[3,530,4508,4511,6604,6703,17,69,99,52,51,102,50,70,20])).
% 117.48/118.17 cnf(6739,plain,
% 117.48/118.17 (~P2(a87,a74)),
% 117.48/118.17 inference(scs_inference,[],[3,530,4508,4511,6604,6609,6703,994,678,17,69,99,52,51,102,50,70,20,71,33,94])).
% 117.48/118.17 cnf(6749,plain,
% 117.48/118.17 (P1(f12(a56,a58),a56)),
% 117.48/118.17 inference(scs_inference,[],[3,530,4508,4511,6694,6604,6609,6703,6302,994,6128,678,14,17,69,99,52,51,102,50,70,20,71,33,94,34,46,43,92])).
% 117.48/118.17 cnf(6836,plain,
% 117.48/118.17 (P1(f32(a56,a59),a56)),
% 117.48/118.17 inference(scs_inference,[],[3,536,5483,5485,3319,3322,6692,6136,6749,2035,5503,5523,17,69,52,99,51,70,102,50,20,71,105,41])).
% 117.48/118.17 cnf(6844,plain,
% 117.48/118.17 (~P2(a87,a90)),
% 117.48/118.17 inference(scs_inference,[],[3,536,5483,5485,3319,3322,6692,6136,6449,5316,6749,2035,5503,5523,8,668,17,69,52,99,51,70,102,50,20,71,105,41,33,48,94])).
% 117.48/118.17 cnf(6851,plain,
% 117.48/118.17 (P6(a59,a3,a83)),
% 117.48/118.17 inference(scs_inference,[],[3,536,5483,5485,3319,3322,6692,6136,6449,5316,6749,2035,5503,5523,6733,2,8,668,17,69,52,99,51,70,102,50,20,71,105,41,33,48,94,44,46,34])).
% 117.48/118.17 cnf(6852,plain,
% 117.48/118.17 (P1(x68521,a3)),
% 117.48/118.17 inference(rename_variables,[],[8])).
% 117.48/118.17 cnf(6858,plain,
% 117.48/118.17 (P1(f7(a69,a71),a69)),
% 117.48/118.17 inference(scs_inference,[],[3,536,5483,5485,3319,3322,6692,6136,6449,5316,6749,2035,5503,5523,6733,12,6,2,8,6852,668,17,69,52,99,51,70,102,50,20,71,105,41,33,48,94,44,46,34,43,80,26])).
% 117.48/118.17 cnf(6860,plain,
% 117.48/118.17 (~P1(f7(a69,a71),a71)),
% 117.48/118.17 inference(scs_inference,[],[3,536,5483,5485,3319,3322,6692,6136,6449,5316,6749,2035,5503,5523,6733,12,6,2,8,6852,668,17,69,52,99,51,70,102,50,20,71,105,41,33,48,94,44,46,34,43,80,26,42])).
% 117.48/118.17 cnf(6868,plain,
% 117.48/118.17 (P1(f7(a69,a71),f75(a71))),
% 117.48/118.17 inference(scs_inference,[],[6860,17])).
% 117.48/118.17 cnf(6876,plain,
% 117.48/118.17 (~P6(f41(a87,a74),f47(a87,a74),a74)),
% 117.48/118.17 inference(scs_inference,[],[3308,3311,6739,6860,17,69,52,51,99])).
% 117.48/118.17 cnf(6878,plain,
% 117.48/118.17 (P6(f41(a87,a74),f47(a87,a74),a87)),
% 117.48/118.17 inference(scs_inference,[],[3308,3311,6739,6860,17,69,52,51,99,50])).
% 117.48/118.17 cnf(6882,plain,
% 117.48/118.17 (~P6(f49(a85,a76),f50(a85,a76),a76)),
% 117.48/118.17 inference(scs_inference,[],[539,3308,3311,6739,6860,17,69,52,51,99,50,70,102])).
% 117.48/118.17 cnf(6884,plain,
% 117.48/118.17 (~P1(f32(a56,a59),f75(a56))),
% 117.48/118.17 inference(scs_inference,[],[539,3308,3311,6739,6860,6836,17,69,52,51,99,50,70,102,20])).
% 117.48/118.17 cnf(6886,plain,
% 117.48/118.17 (P6(f49(a85,a76),f50(a85,a76),a85)),
% 117.48/118.17 inference(scs_inference,[],[539,3308,3311,6739,6860,6836,17,69,52,51,99,50,70,102,20,71])).
% 117.48/118.17 cnf(6890,plain,
% 117.48/118.17 (~P2(a5,a76)),
% 117.48/118.17 inference(scs_inference,[],[3,539,3308,3311,6739,6265,6860,6259,6836,8,17,69,52,51,99,50,70,102,20,71,33,94])).
% 117.48/118.17 cnf(6892,plain,
% 117.48/118.17 (~P6(a59,a58,a10)),
% 117.48/118.17 inference(scs_inference,[],[3,539,3308,3311,6739,6265,6860,6259,6836,14,8,17,69,52,51,99,50,70,102,20,71,33,94,46])).
% 117.48/118.17 cnf(6896,plain,
% 117.48/118.17 (P1(x68961,a3)),
% 117.48/118.17 inference(rename_variables,[],[8])).
% 117.48/118.17 cnf(6900,plain,
% 117.48/118.17 (P1(f77(a3,a59),a59)),
% 117.48/118.17 inference(scs_inference,[],[3,539,3308,3311,6739,6265,6860,6259,6836,5225,5421,14,8,17,69,52,51,99,50,70,102,20,71,33,94,46,34,43,53])).
% 117.48/118.17 cnf(6914,plain,
% 117.48/118.17 (P3(a81,a83)),
% 117.48/118.17 inference(scs_inference,[],[3,539,3308,3311,6739,6851,6565,6265,6860,6259,6836,6046,4921,4927,6733,5225,5421,2,14,8,6896,17,69,52,51,99,50,70,102,20,71,33,94,46,34,43,53,79,78,45,81,91,100])).
% 117.48/118.17 cnf(6915,plain,
% 117.48/118.17 (P6(x69151,a3,a81)),
% 117.48/118.17 inference(rename_variables,[],[6046])).
% 117.48/118.17 cnf(6917,plain,
% 117.48/118.17 (~P5(a81,a83)),
% 117.48/118.17 inference(scs_inference,[],[3,539,3308,3311,6739,6851,6565,6265,6860,6259,6836,6046,6915,4921,4927,6733,5225,5421,2,14,8,6896,17,69,52,51,99,50,70,102,20,71,33,94,46,34,43,53,79,78,45,81,91,100,104])).
% 117.48/118.17 cnf(6934,plain,
% 117.48/118.17 (~P6(f49(a10,a84),f50(a10,a84),a84)),
% 117.48/118.17 inference(scs_inference,[],[571,5986,5989,6844,5103,17,69,52,51,99,50,102])).
% 117.48/118.17 cnf(6940,plain,
% 117.48/118.17 (P6(f49(a10,a84),f50(a10,a84),a10)),
% 117.48/118.17 inference(scs_inference,[],[571,5986,5989,6844,6900,5103,17,69,52,51,99,50,102,70,20,71])).
% 117.48/118.17 cnf(6942,plain,
% 117.48/118.17 (~P1(f14(a59,a62),a62)),
% 117.48/118.17 inference(scs_inference,[],[3,571,5986,5989,6844,6900,1717,5103,17,69,52,51,99,50,102,70,20,71,77])).
% 117.48/118.17 cnf(6947,plain,
% 117.48/118.17 (~P2(a87,a91)),
% 117.48/118.17 inference(scs_inference,[],[3,571,5986,5989,6844,6456,6900,5316,1717,5103,604,17,69,52,51,99,50,102,70,20,71,77,33,94])).
% 117.48/118.17 cnf(6961,plain,
% 117.48/118.17 (P1(f12(a59,a58),a59)),
% 117.48/118.17 inference(scs_inference,[],[3,571,5986,5989,6844,6892,6456,6606,6884,5842,6900,5316,1717,5103,1703,678,11,14,604,17,69,52,51,99,50,102,70,20,71,77,33,94,46,34,43,75,92])).
% 117.48/118.17 cnf(6993,plain,
% 117.48/118.17 (~P2(a85,a76)),
% 117.48/118.17 inference(scs_inference,[],[3,579,4994,4997,6890,6961,6886,6882,6942,6868,604,17,69,52,51,99,102,50,70,20,71,40,33,94])).
% 117.48/118.17 cnf(6998,plain,
% 117.48/118.17 (P6(f75(a58),a59,a83)),
% 117.48/118.17 inference(scs_inference,[],[3,579,4994,4997,6890,6961,6886,6882,6942,6868,668,604,17,69,52,51,99,102,50,70,20,71,40,33,94,46,34])).
% 117.48/118.17 cnf(7001,plain,
% 117.48/118.17 (~P6(a65,a62,a74)),
% 117.48/118.17 inference(scs_inference,[],[3,579,4994,4997,6890,6961,6886,6882,6942,6868,10,5,668,604,17,69,52,51,99,102,50,70,20,71,40,33,94,46,34,43])).
% 117.48/118.17 cnf(7003,plain,
% 117.48/118.17 (P1(f7(a65,a62),a65)),
% 117.48/118.17 inference(scs_inference,[],[3,579,4994,4997,6890,6961,6886,6882,6942,6868,10,5,668,604,17,69,52,51,99,102,50,70,20,71,40,33,94,46,34,43,26])).
% 117.48/118.17 cnf(7005,plain,
% 117.48/118.17 (~P1(f7(a65,a62),a62)),
% 117.48/118.17 inference(scs_inference,[],[3,579,4994,4997,6890,6961,6886,6882,6942,6868,10,5,668,604,17,69,52,51,99,102,50,70,20,71,40,33,94,46,34,43,26,42])).
% 117.48/118.17 cnf(7007,plain,
% 117.48/118.17 (P1(f72(a58,a62),a62)),
% 117.48/118.17 inference(scs_inference,[],[3,579,4994,4997,6890,6961,6886,6882,6942,6868,591,10,5,14,668,604,17,69,52,51,99,102,50,70,20,71,40,33,94,46,34,43,26,42,76])).
% 117.48/118.17 cnf(7008,plain,
% 117.48/118.17 (~P1(x70081,a58)),
% 117.48/118.17 inference(rename_variables,[],[14])).
% 117.48/118.17 cnf(7010,plain,
% 117.48/118.17 (P1(x70101,a69)+P1(f19(a69,a58),a69)),
% 117.48/118.17 inference(scs_inference,[],[3,579,4994,4997,6890,6961,6886,6882,6942,5786,6868,6858,591,10,5,14,7008,668,604,17,69,52,51,99,102,50,70,20,71,40,33,94,46,34,43,26,42,76,96])).
% 117.48/118.17 cnf(7015,plain,
% 117.48/118.17 (P1(f19(a69,a58),a69)),
% 117.48/118.17 inference(factoring_inference,[],[7010])).
% 117.48/118.17 cnf(7016,plain,
% 117.48/118.17 (P1(f7(a65,a62),f75(a62))),
% 117.48/118.17 inference(scs_inference,[],[7005,17])).
% 117.48/118.17 cnf(7026,plain,
% 117.48/118.17 (~P6(f49(a73,a8),f50(a73,a8),a8)),
% 117.48/118.17 inference(scs_inference,[],[663,6355,6358,6947,7005,17,69,51,52,99,102])).
% 117.48/118.17 cnf(7032,plain,
% 117.48/118.17 (~P1(f19(a69,a58),f75(a69))),
% 117.48/118.17 inference(scs_inference,[],[663,6355,6358,6947,7015,7005,17,69,51,52,99,102,50,70,20])).
% 117.48/118.17 cnf(7034,plain,
% 117.48/118.17 (P6(f49(a73,a8),f50(a73,a8),a73)),
% 117.48/118.17 inference(scs_inference,[],[663,6355,6358,6947,7015,7005,17,69,51,52,99,102,50,70,20,71])).
% 117.48/118.17 cnf(7036,plain,
% 117.48/118.17 (~P2(a81,a74)),
% 117.48/118.17 inference(scs_inference,[],[663,6355,6358,6947,7001,7015,7005,5089,17,69,51,52,99,102,50,70,20,71,94])).
% 117.48/118.17 cnf(7067,plain,
% 117.48/118.17 (~P1(f7(a65,a62),f75(a65))),
% 117.48/118.17 inference(scs_inference,[],[674,6659,6662,6993,7003,5367,17,69,51,52,50,99,102,70,20])).
% 117.48/118.17 cnf(7074,plain,
% 117.48/118.17 (P1(f32(a69,a59),a69)),
% 117.48/118.17 inference(scs_inference,[],[3,674,6659,6662,6993,4449,5932,7003,5714,5367,17,69,51,52,50,99,102,70,20,71,105,41])).
% 117.48/118.17 cnf(7084,plain,
% 117.48/118.17 (~P2(a10,a84)),
% 117.48/118.17 inference(scs_inference,[],[3,674,6659,6662,6993,7032,7016,6940,6934,4449,5932,7003,5714,5367,678,17,69,51,52,50,99,102,70,20,71,105,41,45,48,44,94])).
% 117.48/118.17 cnf(7090,plain,
% 117.48/118.17 (P6(f49(a73,a8),f50(a73,a8),a74)),
% 117.48/118.17 inference(scs_inference,[],[3,674,6659,6662,6993,7032,7016,6940,7034,6934,4449,5932,7003,5714,5367,6733,13,2,678,17,69,51,52,50,99,102,70,20,71,105,41,45,48,44,94,46,43,91])).
% 117.48/118.17 cnf(7094,plain,
% 117.48/118.17 (~P6(f75(a62),f75(a65),a91)),
% 117.48/118.17 inference(scs_inference,[],[3,674,6659,6662,6993,7032,7016,6940,7034,6934,4449,5932,7003,5714,5367,6733,13,2,678,17,69,51,52,50,99,102,70,20,71,105,41,45,48,44,94,46,43,91,47,49])).
% 117.48/118.17 cnf(7128,plain,
% 117.48/118.17 (~P6(f49(a81,a8),f50(a81,a8),a8)),
% 117.48/118.17 inference(scs_inference,[],[779,6914,6917,7036,5435,17,69,51,52,99,50,102])).
% 117.48/118.17 cnf(7134,plain,
% 117.48/118.17 (P6(f49(a81,a8),f50(a81,a8),a81)),
% 117.48/118.17 inference(scs_inference,[],[779,6914,6917,7036,7074,5435,17,69,51,52,99,50,102,70,20,71])).
% 117.48/118.17 cnf(7137,plain,
% 117.48/118.17 (P1(x71371,f48(a85,a85))),
% 117.48/118.17 inference(rename_variables,[],[678])).
% 117.48/118.17 cnf(7139,plain,
% 117.48/118.17 (~P2(a86,a73)),
% 117.48/118.17 inference(scs_inference,[],[779,6914,6917,7036,7067,5609,7074,4431,5435,678,17,69,51,52,99,50,102,70,20,71,45,94])).
% 117.48/118.17 cnf(7152,plain,
% 117.48/118.17 (P1(f52(a59,a59),a59)),
% 117.48/118.17 inference(scs_inference,[],[3,779,6914,6917,7036,7067,5609,6878,6876,7074,4431,5419,5435,678,7137,14,17,69,51,52,99,50,102,70,20,71,45,94,46,43,91,26,79])).
% 117.48/118.17 cnf(7158,plain,
% 117.48/118.17 (P3(a81,a86)),
% 117.48/118.17 inference(scs_inference,[],[3,779,6914,6917,7036,7067,5609,6878,6876,7074,4431,5940,5081,5419,5435,678,7137,14,17,69,51,52,99,50,102,70,20,71,45,94,46,43,91,26,79,78,100])).
% 117.48/118.17 cnf(7159,plain,
% 117.48/118.17 (P6(x71591,f48(a85,a85),a81)),
% 117.48/118.17 inference(rename_variables,[],[5940])).
% 117.48/118.17 cnf(7161,plain,
% 117.48/118.17 (~P5(a81,a86)),
% 117.48/118.17 inference(scs_inference,[],[3,779,6914,6917,7036,7067,5609,6878,6876,7074,4431,5940,7159,5081,5419,5435,678,7137,14,17,69,51,52,99,50,102,70,20,71,45,94,46,43,91,26,79,78,100,104])).
% 117.48/118.17 cnf(7166,plain,
% 117.48/118.17 (P1(f29(a62,a59),a65)),
% 117.48/118.17 inference(scs_inference,[],[3,779,6914,6917,7036,7067,5609,6878,6876,7074,6148,4431,5940,7159,7007,7005,5081,5419,5435,678,7137,14,17,69,51,52,99,50,102,70,20,71,45,94,46,43,91,26,79,78,100,104,96,15])).
% 117.48/118.17 cnf(7170,plain,
% 117.48/118.17 (P1(f22(a2,a2),f75(a2))),
% 117.48/118.17 inference(scs_inference,[],[5465,17])).
% 117.48/118.17 cnf(7190,plain,
% 117.48/118.17 (~P2(a74,a8)),
% 117.48/118.17 inference(scs_inference,[],[1236,7084,7158,7161,7090,7166,7026,5465,17,69,51,52,99,102,50,70,20,71,94])).
% 117.48/118.17 cnf(7194,plain,
% 117.48/118.17 (~P1(f14(a59,a71),a71)),
% 117.48/118.17 inference(scs_inference,[],[3,1236,7084,7158,7161,7090,7166,7026,4909,7067,5465,7016,17,69,51,52,99,102,50,70,20,71,94,43,77])).
% 117.48/118.17 cnf(7216,plain,
% 117.48/118.17 (P6(f48(a85,a85),f51(a85,a85),a85)),
% 117.48/118.17 inference(scs_inference,[],[7194,301,304,326,17,69,51,52])).
% 117.48/118.17 cnf(7218,plain,
% 117.48/118.17 (~P6(f41(a86,a73),f47(a86,a73),a73)),
% 117.48/118.17 inference(scs_inference,[],[7139,7194,301,304,326,17,69,51,52,99])).
% 117.48/118.17 cnf(7220,plain,
% 117.48/118.17 (P6(f41(a86,a73),f47(a86,a73),a86)),
% 117.48/118.17 inference(scs_inference,[],[7139,7194,301,304,326,17,69,51,52,99,50])).
% 117.48/118.17 cnf(7222,plain,
% 117.48/118.17 (P6(f45(a73,a73),f46(a73,a73),a73)),
% 117.48/118.17 inference(scs_inference,[],[7139,7194,301,304,326,642,17,69,51,52,99,50,70])).
% 117.48/118.17 cnf(7226,plain,
% 117.48/118.17 (~P1(f52(a59,a59),f75(a59))),
% 117.48/118.17 inference(scs_inference,[],[1288,7139,7194,7152,301,304,326,642,17,69,51,52,99,50,70,102,20])).
% 117.48/118.17 cnf(7230,plain,
% 117.48/118.17 (~P2(a81,a91)),
% 117.48/118.17 inference(scs_inference,[],[1288,7139,7094,7194,5213,7152,301,304,326,642,17,69,51,52,99,50,70,102,20,71,94])).
% 117.48/118.17 cnf(7236,plain,
% 117.48/118.17 (P6(f75(a2),a2,a9)),
% 117.48/118.17 inference(scs_inference,[],[3,1288,7139,7094,7170,7194,5213,7152,301,304,326,642,668,17,69,51,52,99,50,70,102,20,71,94,43,40])).
% 117.48/118.17 cnf(7264,plain,
% 117.48/118.17 (~P1(a61,f75(a62))),
% 117.48/118.17 inference(scs_inference,[],[4,1327,7190,555,1296,1210,2039,17,69,52,51,50,99,102,20])).
% 117.48/118.17 cnf(7270,plain,
% 117.48/118.17 (~P2(a81,a8)),
% 117.48/118.17 inference(scs_inference,[],[4,1327,7190,7134,7128,555,1296,1210,2039,678,17,69,52,51,50,99,102,20,71,33,94])).
% 117.48/118.17 cnf(7273,plain,
% 117.48/118.17 (P1(x72731,f48(a85,a85))),
% 117.48/118.17 inference(rename_variables,[],[678])).
% 117.48/118.17 cnf(7281,plain,
% 117.48/118.17 (P6(f45(a73,a73),f46(a73,a73),a74)),
% 117.48/118.17 inference(scs_inference,[],[4,1327,7190,7134,7226,7222,7128,555,1296,1210,2039,13,678,7273,799,17,69,52,51,50,99,102,20,71,33,94,34,46,43,91])).
% 117.48/118.17 cnf(7283,plain,
% 117.48/118.17 (P1(x72831,a56)+P1(f19(a56,a58),a56)),
% 117.48/118.17 inference(scs_inference,[],[4,1327,7190,7134,7226,7222,7128,5595,6298,555,1296,1210,2039,13,678,7273,799,14,17,69,52,51,50,99,102,20,71,33,94,34,46,43,91,96])).
% 117.48/118.17 cnf(7288,plain,
% 117.48/118.17 (P1(f19(a56,a58),a56)),
% 117.48/118.17 inference(factoring_inference,[],[7283])).
% 117.48/118.17 cnf(7301,plain,
% 117.48/118.17 (~P1(f19(a56,a58),f75(a56))),
% 117.48/118.17 inference(scs_inference,[],[1332,7230,7288,3244,1214,2009,17,69,52,50,99,102,20])).
% 117.48/118.17 cnf(7307,plain,
% 117.48/118.17 (~P2(a87,a88)),
% 117.48/118.17 inference(scs_inference,[],[4,1332,7230,7288,5195,5627,3244,1214,2009,678,17,69,52,50,99,102,20,71,33,94])).
% 117.48/118.17 cnf(7312,plain,
% 117.48/118.17 (P1(x73121,f48(a85,a85))),
% 117.48/118.17 inference(rename_variables,[],[678])).
% 117.48/118.17 cnf(7325,plain,
% 117.48/118.17 (P1(f32(a71,a62),a71)),
% 117.48/118.17 inference(scs_inference,[],[4,1332,7230,7288,7264,6998,5195,7220,7218,5627,6118,3244,5806,1214,2009,678,7312,799,17,69,52,50,99,102,20,71,33,94,34,46,43,91,105,41])).
% 117.48/118.17 cnf(7371,plain,
% 117.48/118.17 (P1(x73711,a3)),
% 117.48/118.17 inference(rename_variables,[],[8])).
% 117.48/118.17 cnf(7379,plain,
% 117.48/118.17 (P3(a5,a86)),
% 117.48/118.17 inference(scs_inference,[],[4,1342,7270,7216,7301,5910,7325,4445,1021,3319,1300,5413,5523,5099,678,14,8,17,69,52,99,50,102,20,71,79,78,47,33,49,94,34,46,43,100])).
% 117.48/118.17 cnf(7380,plain,
% 117.48/118.17 (P6(f46(a73,a73),x73801,a5)),
% 117.48/118.17 inference(rename_variables,[],[1021])).
% 117.48/118.17 cnf(7382,plain,
% 117.48/118.17 (~P5(a5,a86)),
% 117.48/118.17 inference(scs_inference,[],[4,1342,7270,7216,7301,5910,7325,4445,1021,7380,3319,1300,5413,5523,5099,678,14,8,17,69,52,99,50,102,20,71,79,78,47,33,49,94,34,46,43,100,104])).
% 117.48/118.17 cnf(7395,plain,
% 117.48/118.17 (P1(f78(a3,a62),a65)),
% 117.48/118.17 inference(scs_inference,[],[4,1342,7270,7216,7301,5910,7325,4445,1021,7380,3319,1300,5413,5523,5099,678,14,8,7371,17,69,52,99,50,102,20,71,79,78,47,33,49,94,34,46,43,100,104,80,27,29,32,31,15])).
% 117.48/118.17 cnf(7405,plain,
% 117.48/118.17 (P1(f77(a62,a3),a62)),
% 117.48/118.17 inference(scs_inference,[],[4,1342,7270,7216,7301,5910,7325,4445,1021,7380,3319,1300,5413,5523,5099,678,14,8,7371,17,69,52,99,50,102,20,71,79,78,47,33,49,94,34,46,43,100,104,80,27,29,32,31,15,30,51,70,28,54])).
% 117.48/118.17 cnf(7437,plain,
% 117.48/118.17 (P6(a3,a62,a83)),
% 117.48/118.17 inference(scs_inference,[],[4,1347,7307,7379,7382,5199,7395,7405,7236,5065,9,8,17,69,15,52,50,99,102,20,71,77,33,94,34])).
% 117.48/118.17 cnf(7737,plain,
% 117.48/118.17 (P1(x77371,f75(a58))),
% 117.48/118.17 inference(rename_variables,[],[604])).
% 117.48/118.17 cnf(7742,plain,
% 117.48/118.17 (P1(x77421,f75(a58))),
% 117.48/118.17 inference(rename_variables,[],[604])).
% 117.48/118.17 cnf(7749,plain,
% 117.48/118.17 ($false),
% 117.48/118.17 inference(scs_inference,[],[604,7737,7742,953,5421,5089,6444,5042,7216,7222,7281,6210,6886,7220,4937,5914,6018,5812,5924,6036,7437,36,28,86,58,35,15,30,83,31,587,32,218,39,254,29,27,38,37,1863,1816,98,80,101,104,93,43]),
% 117.48/118.17 ['proof']).
% 117.48/118.17 % SZS output end Proof
% 117.48/118.17 % Total time :116.770000s
%------------------------------------------------------------------------------