%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : KRS215+1 : TPTP v8.2.0. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n008.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 67.17s 67.22s
% Output : CNFRefutation 67.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS215+1 : TPTP v8.2.0. Bugfixed v5.4.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n008.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed Jun 19 14:13:24 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.53/0.57 start to proof:theBenchmark
% 67.17/67.21 %-------------------------------------------
% 67.17/67.21 % File :CSE---1.7
% 67.17/67.21 % Problem :theBenchmark
% 67.17/67.21 % Transform :cnf
% 67.17/67.21 % Format :tptp:raw
% 67.17/67.21 % Command :java -jar mcs_scs.jar %d %s
% 67.17/67.21
% 67.17/67.21 % Result :Theorem 66.580000s
% 67.17/67.21 % Output :CNFRefutation 66.580000s
% 67.17/67.21 %-------------------------------------------
% 67.17/67.22 %------------------------------------------------------------------------------
% 67.17/67.22 % File : KRS215+1 : TPTP v8.2.0. Bugfixed v5.4.0.
% 67.17/67.22 % Domain : Knowledge Representation
% 67.17/67.22 % Problem : CSA nota THM
% 67.17/67.22 % Version : [Sut08] axioms.
% 67.17/67.22 % English :
% 67.17/67.22
% 67.17/67.22 % Refs : [Sut08] Sutcliffe (2008), The SZS Ontologies for Automated Rea
% 67.17/67.22 % Source : [TPTP]
% 67.17/67.22 % Names :
% 67.17/67.22
% 67.17/67.22 % Status : Theorem
% 67.17/67.22 % Rating : 0.12 v8.2.0, 0.13 v8.1.0, 0.07 v7.5.0, 0.19 v7.4.0, 0.12 v7.3.0, 0.29 v7.2.0, 0.17 v7.1.0, 0.25 v7.0.0, 0.21 v6.4.0, 0.07 v6.3.0, 0.15 v6.2.0, 0.27 v6.1.0, 0.40 v6.0.0, 0.50 v5.4.0
% 67.17/67.22 % Syntax : Number of formulae : 33 ( 3 unt; 0 def)
% 67.17/67.22 % Number of atoms : 107 ( 0 equ)
% 67.17/67.22 % Maximal formula atoms : 7 ( 3 avg)
% 67.17/67.22 % Number of connectives : 96 ( 22 ~; 1 |; 35 &)
% 67.17/67.22 % ( 28 <=>; 8 =>; 0 <=; 2 <~>)
% 67.17/67.22 % Maximal formula depth : 10 ( 6 avg)
% 67.17/67.22 % Maximal term depth : 2 ( 1 avg)
% 67.17/67.22 % Number of predicates : 7 ( 7 usr; 0 prp; 2-3 aty)
% 67.17/67.22 % Number of functors : 20 ( 20 usr; 19 con; 0-1 aty)
% 67.17/67.22 % Number of variables : 122 ( 72 !; 50 ?)
% 67.17/67.22 % SPC : FOF_THM_RFO_NEQ
% 67.17/67.22
% 67.17/67.22 % Comments :
% 67.17/67.22 % Bugfixes : v5.4.0 - Added missing axiom in KRS001+1.ax
% 67.17/67.22 %------------------------------------------------------------------------------
% 67.17/67.22 %----Include SZS success ontology nodes
% 67.17/67.22 include('Axioms/KRS001+0.ax').
% 67.17/67.22 %----Include SZS success ontology node relationships
% 67.17/67.22 include('Axioms/KRS001+1.ax').
% 67.17/67.22 %------------------------------------------------------------------------------
% 67.17/67.22 fof(nota_csa_thm,conjecture,
% 67.17/67.22 nota(csa,thm) ).
% 67.17/67.22
% 67.17/67.22 %------------------------------------------------------------------------------
% 67.17/67.22 %-------------------------------------------
% 67.17/67.22 % Proof found
% 67.17/67.22 % SZS status Theorem for theBenchmark
% 67.17/67.22 % SZS output start Proof
% 67.17/67.23 %ClaNum:109(EqnAxiom:0)
% 67.17/67.23 %VarNum:590(SingletonVarNum:249)
% 67.17/67.23 %MaxLitNum:6
% 67.17/67.23 %MaxfuncDepth:1
% 67.17/67.23 %SharedTerms:52
% 67.17/67.23 %goalClause: 13
% 67.17/67.23 %singleGoalClaCount:1
% 67.17/67.23 [1]P1(a1,a2)
% 67.17/67.23 [2]P1(a55,a56)
% 67.17/67.23 [3]P1(a55,a59)
% 67.17/67.23 [4]P1(a61,a62)
% 67.17/67.23 [5]P1(a66,a65)
% 67.17/67.23 [6]P1(a67,a69)
% 67.17/67.23 [7]P1(a70,a71)
% 67.17/67.23 [9]~P1(a57,a2)
% 67.17/67.23 [10]~P1(a66,a62)
% 67.17/67.23 [11]~P1(a68,a65)
% 67.17/67.23 [12]~P1(a67,a71)
% 67.17/67.23 [13]~P4(a4,a73)
% 67.17/67.23 [8]P1(x81,a3)
% 67.17/67.23 [14]~P1(x141,a58)
% 67.17/67.23 [18]~P1(a63,a56)+~P1(a64,a59)
% 67.17/67.23 [15]~P1(x151,a62)+P1(x151,a65)
% 67.17/67.23 [17]P1(x171,x172)+P1(x171,f74(x172))
% 67.17/67.23 [20]~P1(x201,x202)+~P1(x201,f74(x202))
% 67.17/67.23 [21]P6(x211,x212,a5)+P1(f6(x211),x211)
% 67.17/67.23 [24]P6(x241,x242,a86)+P1(f7(x241,x242),x242)
% 67.17/67.23 [25]P6(x251,x252,a80)+P1(f31(x251,x252),x251)
% 67.17/67.23 [26]P6(x261,x262,a73)+P1(f8(x261,x262),x261)
% 67.17/67.23 [42]P6(x421,x422,a73)+~P1(f8(x421,x422),x422)
% 67.17/67.23 [50]P2(x501,x502)+P6(f41(x501,x502),f47(x501,x502),x501)
% 67.17/67.23 [51]P5(x511,x512)+P6(f48(x511,x512),f51(x511,x512),x512)
% 67.17/67.23 [52]P5(x521,x522)+P6(f48(x521,x522),f51(x521,x522),x521)
% 67.17/67.23 [53]~P6(x531,x532,a82)+P1(f76(x531,x532),x532)
% 67.17/67.23 [54]~P6(x541,x542,a82)+P1(f76(x541,x542),x541)
% 67.17/67.23 [55]~P6(x551,x552,a10)+P1(f11(x551,x552),x551)
% 67.17/67.23 [56]~P6(x561,x562,a81)+P1(f13(x561,x562),x561)
% 67.17/67.23 [57]~P6(x571,x572,a90)+P1(f15(x571,x572),x571)
% 67.17/67.23 [58]~P6(x581,x582,a90)+P1(f17(x581,x582),x582)
% 67.17/67.23 [59]~P6(x591,x592,a75)+P1(f18(x591,x592),x591)
% 67.17/67.23 [60]~P6(x601,x602,a87)+P1(f20(x601,x602),x601)
% 67.17/67.23 [61]~P6(x611,x612,a91)+P1(f25(x611,x612),x611)
% 67.17/67.23 [62]~P6(x621,x622,a91)+P1(f28(x621,x622),x622)
% 67.17/67.23 [63]~P6(x631,x632,a83)+P1(f33(x631,x632),x632)
% 67.17/67.23 [64]~P6(x641,x642,a89)+P1(f34(x641,x642),x642)
% 67.17/67.23 [65]~P6(x651,x652,a4)+P1(f38(x651,x652),x651)
% 67.17/67.23 [66]~P6(x661,x662,a79)+P1(f42(x661,x662),x662)
% 67.17/67.23 [67]~P6(x671,x672,a79)+P1(f42(x671,x672),x671)
% 67.17/67.23 [68]~P6(x681,x682,a79)+P1(f44(x681,x682),x681)
% 67.17/67.23 [69]~P3(x691,x692)+P6(f45(x691,x692),f46(x691,x692),x692)
% 67.17/67.23 [70]~P3(x701,x702)+P6(f45(x701,x702),f46(x701,x702),x701)
% 67.17/67.23 [71]~P4(x711,x712)+P6(f49(x711,x712),f50(x711,x712),x711)
% 67.17/67.23 [72]~P6(x721,x722,a4)+P1(f38(x721,x722),f74(x722))
% 67.17/67.23 [73]~P6(x731,x732,a79)+P1(f44(x731,x732),f74(x732))
% 67.17/67.23 [82]~P6(x821,x822,a90)+~P1(f17(x821,x822),x821)
% 67.17/67.23 [83]~P6(x831,x832,a75)+~P1(f21(x831,x832),x831)
% 67.17/67.23 [84]~P6(x841,x842,a87)+~P1(f26(x841,x842),x841)
% 67.17/67.23 [85]~P6(x851,x852,a91)+~P1(f28(x851,x852),x851)
% 67.17/67.23 [86]~P6(x861,x862,a91)+~P1(f30(x861,x862),x862)
% 67.17/67.23 [87]~P6(x871,x872,a89)+~P1(f39(x871,x872),x872)
% 67.17/67.23 [99]P2(x991,x992)+~P6(f41(x991,x992),f47(x991,x992),x992)
% 67.17/67.23 [102]~P4(x1021,x1022)+~P6(f49(x1021,x1022),f50(x1021,x1022),x1022)
% 67.17/67.23 [22]~P1(x223,x222)+P6(x221,x222,a80)
% 67.17/67.23 [23]~P1(x233,x231)+P6(x231,x232,a86)
% 67.17/67.23 [27]P1(x271,x272)+~P6(x273,x272,a81)
% 67.17/67.23 [28]P1(x281,x282)+~P6(x283,x282,a84)
% 67.17/67.23 [29]P1(x291,x292)+~P6(x293,x292,a87)
% 67.17/67.23 [30]P1(x301,x302)+~P6(x303,x302,a85)
% 67.17/67.23 [31]P1(x311,x312)+~P6(x312,x313,a84)
% 67.17/67.23 [32]P1(x321,x322)+~P6(x322,x323,a88)
% 67.17/67.23 [36]~P1(x361,x362)+~P6(x362,x363,a5)
% 67.17/67.23 [37]~P1(x371,x372)+~P6(x372,x373,a83)
% 67.17/67.23 [38]~P1(x381,x382)+~P6(x382,x383,a85)
% 67.17/67.23 [39]~P1(x391,x392)+~P6(x392,x393,a89)
% 67.17/67.23 [35]~P6(x353,x352,a88)+P1(x351,f74(x352))
% 67.17/67.23 [76]P6(x761,x762,a9)+P1(f60(x761,x762),x761)+P1(f72(x761,x762),x762)
% 67.17/67.23 [93]P6(x931,x932,a85)+P1(f36(x931,x932),x931)+~P1(f37(x931,x932),x932)
% 67.17/67.23 [98]P6(x981,x982,a84)+~P1(f23(x981,x982),x981)+~P1(f24(x981,x982),x982)
% 67.17/67.23 [101]P6(x1011,x1012,a88)+~P1(f40(x1011,x1012),x1011)+~P1(f43(x1011,x1012),f74(x1012))
% 67.17/67.23 [108]P7(x1081,x1082)+P6(f53(x1081,x1082),f54(x1081,x1082),x1082)+~P6(f53(x1081,x1082),f54(x1081,x1082),x1081)
% 67.17/67.23 [109]P7(x1091,x1092)+P6(f53(x1091,x1092),f54(x1091,x1092),x1091)+~P6(f53(x1091,x1092),f54(x1091,x1092),x1092)
% 67.17/67.23 [34]~P1(x343,x341)+~P1(x343,x342)+P6(x341,x342,a82)
% 67.17/67.23 [43]P1(x431,x432)+~P1(x431,x433)+~P6(x433,x432,a73)
% 67.17/67.23 [44]P1(x441,x442)+~P1(x441,x443)+~P6(x442,x443,a10)
% 67.17/67.23 [45]P1(x451,x452)+~P1(x451,x453)+~P6(x452,x453,a75)
% 67.17/67.23 [46]P1(x461,x462)+~P1(x461,x463)+~P6(x463,x462,a10)
% 67.17/67.23 [47]P1(x471,x472)+~P1(x471,x473)+~P6(x473,x472,a90)
% 67.17/67.23 [48]P1(x481,x482)+~P1(x481,x483)+~P6(x483,x482,a75)
% 67.17/67.23 [49]P1(x491,x492)+~P1(x491,x493)+~P6(x493,x492,a91)
% 67.17/67.23 [40]~P1(x403,x401)+P6(x401,x402,a4)+~P1(x403,f74(x402))
% 67.17/67.23 [41]~P1(x413,x412)+P6(x411,x412,a83)+P1(f32(x411,x412),x411)
% 67.17/67.23 [77]~P1(x773,x771)+P6(x771,x772,a81)+~P1(f14(x771,x772),x772)
% 67.17/67.23 [78]~P1(x783,x782)+~P6(x781,x782,a86)+P1(f29(x781,x782),x781)
% 67.17/67.23 [79]~P1(x793,x791)+~P6(x791,x792,a80)+P1(f52(x791,x792),x792)
% 67.17/67.23 [80]~P1(x803,x801)+~P6(x801,x802,a9)+P1(f77(x801,x802),x802)
% 67.17/67.23 [81]~P1(x813,x812)+~P6(x811,x812,a9)+P1(f78(x811,x812),x811)
% 67.17/67.23 [33]~P1(x333,x332)+~P1(x334,x331)+P6(x331,x332,a9)
% 67.17/67.23 [75]~P7(x754,x753)+P6(x751,x752,x753)+P6(x751,x752,x754)
% 67.17/67.23 [91]~P6(x913,x914,x911)+P4(x911,x912)+P6(x913,x914,x912)
% 67.17/67.23 [94]~P6(x941,x942,x944)+P6(x941,x942,x943)+~P2(x944,x943)
% 67.17/67.23 [100]~P6(x1003,x1004,x1001)+P3(x1001,x1002)+~P6(x1003,x1004,x1002)
% 67.17/67.23 [104]~P6(x1043,x1044,x1041)+~P5(x1041,x1042)+~P6(x1043,x1044,x1042)
% 67.17/67.23 [105]~P6(x1053,x1054,x1051)+~P7(x1051,x1052)+~P6(x1053,x1054,x1052)
% 67.17/67.23 [92]~P1(x923,x921)+P6(x921,x922,a10)+P1(f12(x921,x922),x922)+P1(f12(x921,x922),x921)
% 67.17/67.23 [106]~P1(x1063,x1061)+P6(x1061,x1062,a10)+~P1(f12(x1061,x1062),x1062)+~P1(f12(x1061,x1062),x1061)
% 67.17/67.23 [74]P1(x741,x742)+~P1(x744,x742)+P6(x743,x742,a89)+P1(f35(x743,x742),x743)
% 67.17/67.23 [90]P1(x901,x902)+~P1(x904,x902)+P6(x902,x903,a87)+~P1(f22(x902,x903),x903)
% 67.17/67.23 [88]~P1(x881,x883)+P1(x881,x882)+~P1(x884,x882)+P6(x882,x883,a90)+P1(f16(x882,x883),x882)
% 67.17/67.23 [89]~P1(x894,x891)+~P1(x893,x891)+~P1(x894,x892)+P6(x891,x892,a79)+~P1(x893,f74(x892))
% 67.17/67.23 [96]P1(x961,x962)+~P1(x964,x962)+P6(x962,x963,a75)+P1(f19(x962,x963),x963)+P1(f19(x962,x963),x962)
% 67.17/67.23 [97]~P1(x971,x973)+P1(x971,x972)+~P1(x974,x972)+P6(x972,x973,a90)+~P1(f16(x972,x973),x973)
% 67.17/67.23 [107]P1(x1071,x1072)+~P1(x1074,x1072)+P6(x1072,x1073,a75)+~P1(f19(x1072,x1073),x1073)+~P1(f19(x1072,x1073),x1072)
% 67.17/67.23 [95]~P1(x953,x952)+P1(x951,x952)+P1(x953,x954)+~P1(x955,x954)+P6(x954,x952,a91)+P1(f27(x954,x952),x954)
% 67.17/67.23 [103]~P1(x1033,x1032)+P1(x1031,x1032)+P1(x1033,x1034)+~P1(x1035,x1034)+P6(x1034,x1032,a91)+~P1(f27(x1034,x1032),x1032)
% 67.17/67.23 %EqnAxiom
% 67.17/67.23
% 67.17/67.23 %-------------------------------------------
% 67.17/67.24 cnf(110,plain,
% 67.17/67.24 (P6(a58,x1101,a5)),
% 67.17/67.24 inference(scs_inference,[],[14,21])).
% 67.17/67.24 cnf(111,plain,
% 67.17/67.24 (~P1(x1111,a58)),
% 67.17/67.24 inference(rename_variables,[],[14])).
% 67.17/67.24 cnf(113,plain,
% 67.17/67.24 (P6(x1131,a58,a86)),
% 67.17/67.24 inference(scs_inference,[],[14,111,21,24])).
% 67.17/67.24 cnf(114,plain,
% 67.17/67.24 (~P1(x1141,a58)),
% 67.17/67.24 inference(rename_variables,[],[14])).
% 67.17/67.24 cnf(116,plain,
% 67.17/67.24 (P6(a58,x1161,a80)),
% 67.17/67.24 inference(scs_inference,[],[14,111,114,21,24,25])).
% 67.17/67.24 cnf(117,plain,
% 67.17/67.24 (~P1(x1171,a58)),
% 67.17/67.24 inference(rename_variables,[],[14])).
% 67.17/67.24 cnf(119,plain,
% 67.17/67.24 (P6(a58,x1191,a73)),
% 67.17/67.24 inference(scs_inference,[],[14,111,114,117,21,24,25,26])).
% 67.17/67.24 cnf(120,plain,
% 67.17/67.24 (~P1(x1201,a58)),
% 67.17/67.24 inference(rename_variables,[],[14])).
% 67.17/67.24 cnf(122,plain,
% 67.17/67.24 (P6(x1221,a3,a73)),
% 67.17/67.24 inference(scs_inference,[],[8,14,111,114,117,21,24,25,26,42])).
% 67.17/67.24 cnf(123,plain,
% 67.17/67.24 (P1(x1231,a3)),
% 67.17/67.24 inference(rename_variables,[],[8])).
% 67.17/67.24 cnf(125,plain,
% 67.17/67.24 (~P1(a68,a62)),
% 67.17/67.24 inference(scs_inference,[],[8,14,111,114,117,11,21,24,25,26,42,15])).
% 67.17/67.24 cnf(127,plain,
% 67.17/67.24 (~P6(x1271,a58,a82)),
% 67.17/67.24 inference(scs_inference,[],[8,14,111,114,117,120,11,21,24,25,26,42,15,53])).
% 67.17/67.24 cnf(128,plain,
% 67.17/67.24 (~P1(x1281,a58)),
% 67.17/67.24 inference(rename_variables,[],[14])).
% 67.17/67.24 cnf(130,plain,
% 67.17/67.24 (~P6(a58,x1301,a82)),
% 67.17/67.24 inference(scs_inference,[],[8,14,111,114,117,120,128,11,21,24,25,26,42,15,53,54])).
% 67.17/67.24 cnf(131,plain,
% 67.17/67.24 (~P1(x1311,a58)),
% 67.17/67.24 inference(rename_variables,[],[14])).
% 67.17/67.24 cnf(133,plain,
% 67.17/67.24 (~P6(a58,x1331,a10)),
% 67.17/67.24 inference(scs_inference,[],[8,14,111,114,117,120,128,131,11,21,24,25,26,42,15,53,54,55])).
% 67.17/67.24 cnf(134,plain,
% 67.17/67.24 (~P1(x1341,a58)),
% 67.17/67.24 inference(rename_variables,[],[14])).
% 67.17/67.24 cnf(136,plain,
% 67.17/67.24 (~P6(a58,x1361,a81)),
% 67.17/67.24 inference(scs_inference,[],[8,14,111,114,117,120,128,131,134,11,21,24,25,26,42,15,53,54,55,56])).
% 67.17/67.24 cnf(137,plain,
% 67.17/67.24 (~P1(x1371,a58)),
% 67.17/67.24 inference(rename_variables,[],[14])).
% 67.17/67.24 cnf(140,plain,
% 67.17/67.24 (~P1(x1401,a58)),
% 67.17/67.24 inference(rename_variables,[],[14])).
% 67.17/67.24 cnf(142,plain,
% 67.17/67.24 (~P6(x1421,a58,a90)),
% 67.17/67.24 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])).
% 67.17/67.24 cnf(143,plain,
% 67.17/67.24 (~P1(x1431,a58)),
% 67.17/67.24 inference(rename_variables,[],[14])).
% 67.17/67.24 cnf(145,plain,
% 67.17/67.24 (~P6(a58,x1451,a75)),
% 67.17/67.24 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])).
% 67.17/67.24 cnf(146,plain,
% 67.17/67.24 (~P1(x1461,a58)),
% 67.17/67.24 inference(rename_variables,[],[14])).
% 67.17/67.24 cnf(148,plain,
% 67.17/67.24 (~P6(a58,x1481,a87)),
% 67.17/67.24 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])).
% 67.17/67.24 cnf(149,plain,
% 67.17/67.24 (~P1(x1491,a58)),
% 67.17/67.24 inference(rename_variables,[],[14])).
% 67.17/67.24 cnf(152,plain,
% 67.17/67.24 (~P1(x1521,a58)),
% 67.17/67.24 inference(rename_variables,[],[14])).
% 67.17/67.24 cnf(154,plain,
% 67.17/67.24 (~P6(x1541,a58,a91)),
% 67.17/67.24 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])).
% 67.17/67.24 cnf(155,plain,
% 67.17/67.24 (~P1(x1551,a58)),
% 67.17/67.24 inference(rename_variables,[],[14])).
% 67.17/67.24 cnf(157,plain,
% 67.17/67.24 (~P6(x1571,a58,a83)),
% 67.17/67.24 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])).
% 67.17/67.24 cnf(158,plain,
% 67.17/67.24 (~P1(x1581,a58)),
% 67.17/67.24 inference(rename_variables,[],[14])).
% 67.17/67.24 cnf(160,plain,
% 67.17/67.24 (~P6(x1601,a58,a89)),
% 67.17/67.24 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])).
% 67.17/67.24 cnf(161,plain,
% 67.17/67.24 (~P1(x1611,a58)),
% 67.17/67.24 inference(rename_variables,[],[14])).
% 67.17/67.24 cnf(163,plain,
% 67.17/67.24 (~P6(a58,x1631,a4)),
% 67.17/67.24 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])).
% 67.17/67.24 cnf(164,plain,
% 67.17/67.24 (~P1(x1641,a58)),
% 67.25/67.24 inference(rename_variables,[],[14])).
% 67.25/67.24 cnf(166,plain,
% 67.25/67.24 (~P6(x1661,a58,a79)),
% 67.25/67.24 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])).
% 67.25/67.24 cnf(167,plain,
% 67.25/67.24 (~P1(x1671,a58)),
% 67.25/67.24 inference(rename_variables,[],[14])).
% 67.25/67.24 cnf(170,plain,
% 67.25/67.24 (~P1(x1701,a58)),
% 67.25/67.24 inference(rename_variables,[],[14])).
% 67.25/67.25 cnf(172,plain,
% 67.25/67.25 (~P6(a3,x1721,a90)),
% 67.25/67.25 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])).
% 67.25/67.25 cnf(173,plain,
% 67.25/67.25 (P1(x1731,a3)),
% 67.25/67.25 inference(rename_variables,[],[8])).
% 67.25/67.25 cnf(175,plain,
% 67.25/67.25 (~P6(a3,x1751,a75)),
% 67.25/67.25 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])).
% 67.25/67.25 cnf(176,plain,
% 67.25/67.25 (P1(x1761,a3)),
% 67.25/67.25 inference(rename_variables,[],[8])).
% 67.25/67.25 cnf(179,plain,
% 67.25/67.25 (P1(x1791,a3)),
% 67.25/67.25 inference(rename_variables,[],[8])).
% 67.25/67.25 cnf(181,plain,
% 67.25/67.25 (~P6(a3,x1811,a91)),
% 67.25/67.25 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])).
% 67.25/67.25 cnf(182,plain,
% 67.25/67.25 (P1(x1821,a3)),
% 67.25/67.25 inference(rename_variables,[],[8])).
% 67.25/67.25 cnf(185,plain,
% 67.25/67.25 (P1(x1851,a3)),
% 67.25/67.25 inference(rename_variables,[],[8])).
% 67.25/67.25 cnf(188,plain,
% 67.25/67.25 (P1(x1881,a3)),
% 67.25/67.25 inference(rename_variables,[],[8])).
% 67.25/67.25 cnf(190,plain,
% 67.25/67.25 (P4(a5,a82)),
% 67.25/67.25 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])).
% 67.25/67.25 cnf(194,plain,
% 67.25/67.25 (P6(a58,a3,a85)),
% 67.25/67.25 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])).
% 67.25/67.25 cnf(195,plain,
% 67.25/67.25 (~P1(x1951,a58)),
% 67.25/67.25 inference(rename_variables,[],[14])).
% 67.25/67.25 cnf(196,plain,
% 67.25/67.25 (P1(x1961,a3)),
% 67.25/67.25 inference(rename_variables,[],[8])).
% 67.25/67.25 cnf(198,plain,
% 67.25/67.25 (~P6(a3,a58,a9)),
% 67.25/67.25 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])).
% 67.25/67.25 cnf(199,plain,
% 67.25/67.25 (~P1(x1991,a58)),
% 67.25/67.25 inference(rename_variables,[],[14])).
% 67.25/67.25 cnf(201,plain,
% 67.25/67.25 (~P6(a58,a3,a9)),
% 67.25/67.25 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])).
% 67.25/67.25 cnf(202,plain,
% 67.25/67.25 (~P1(x2021,a58)),
% 67.25/67.25 inference(rename_variables,[],[14])).
% 67.25/67.25 cnf(210,plain,
% 67.25/67.25 (P6(a3,a3,a10)),
% 67.25/67.25 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])).
% 67.25/67.25 cnf(211,plain,
% 67.25/67.25 (P1(x2111,a3)),
% 67.25/67.25 inference(rename_variables,[],[8])).
% 67.25/67.25 cnf(212,plain,
% 67.25/67.25 (P1(x2121,a3)),
% 67.25/67.25 inference(rename_variables,[],[8])).
% 67.25/67.25 cnf(214,plain,
% 67.25/67.25 (P6(a3,a3,a84)),
% 67.25/67.25 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])).
% 67.25/67.25 cnf(215,plain,
% 67.25/67.25 (P1(x2151,a3)),
% 67.25/67.25 inference(rename_variables,[],[8])).
% 67.25/67.25 cnf(218,plain,
% 67.25/67.25 (P6(a3,x2181,a88)+~P1(f43(a3,x2181),f74(x2181))),
% 67.25/67.25 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])).
% 67.25/67.25 cnf(222,plain,
% 67.25/67.25 (~P6(x2221,a58,a88)+P6(a3,a58,a88)),
% 67.25/67.25 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])).
% 67.25/67.25 cnf(229,plain,
% 67.25/67.25 (~P5(a5,a86)),
% 67.25/67.25 inference(scs_inference,[],[110,113,104])).
% 67.25/67.25 cnf(230,plain,
% 67.25/67.25 (P6(x2301,a58,a86)),
% 67.25/67.25 inference(rename_variables,[],[113])).
% 67.25/67.25 cnf(231,plain,
% 67.25/67.25 (P6(a58,x2311,a5)),
% 67.25/67.25 inference(rename_variables,[],[110])).
% 67.25/67.25 cnf(233,plain,
% 67.25/67.25 (P3(a5,a86)),
% 67.25/67.25 inference(scs_inference,[],[110,231,113,230,104,100])).
% 67.25/67.25 cnf(234,plain,
% 67.25/67.25 (P6(x2341,a58,a86)),
% 67.25/67.25 inference(rename_variables,[],[113])).
% 67.25/67.25 cnf(235,plain,
% 67.25/67.25 (P6(a58,x2351,a5)),
% 67.25/67.25 inference(rename_variables,[],[110])).
% 67.25/67.25 cnf(239,plain,
% 67.25/67.25 (P6(a58,x2391,a5)),
% 67.25/67.25 inference(rename_variables,[],[110])).
% 67.25/67.25 cnf(241,plain,
% 67.25/67.25 (~P6(a2,a58,a9)),
% 67.25/67.25 inference(scs_inference,[],[110,231,235,113,230,234,1,14,104,100,105,80])).
% 67.25/67.25 cnf(242,plain,
% 67.25/67.25 (~P1(x2421,a58)),
% 67.25/67.25 inference(rename_variables,[],[14])).
% 67.25/67.25 cnf(245,plain,
% 67.25/67.25 (~P6(a58,x2451,a10)),
% 67.25/67.25 inference(rename_variables,[],[133])).
% 67.25/67.25 cnf(248,plain,
% 67.25/67.25 (P4(a5,a10)),
% 67.25/67.25 inference(scs_inference,[],[110,231,235,239,113,230,234,127,133,245,1,14,104,100,105,80,75,91])).
% 67.25/67.25 cnf(254,plain,
% 67.25/67.25 (P6(a3,x2541,a84)+~P1(f24(a3,x2541),x2541)),
% 67.25/67.25 inference(scs_inference,[],[110,231,235,239,113,230,234,127,133,245,1,8,14,242,104,100,105,80,75,91,81,98])).
% 67.25/67.25 cnf(278,plain,
% 67.25/67.25 (P3(a85,a85)),
% 67.25/67.25 inference(scs_inference,[],[194,100])).
% 67.25/67.25 cnf(280,plain,
% 67.25/67.25 (~P6(a56,a58,a9)),
% 67.25/67.25 inference(scs_inference,[],[194,2,14,100,80])).
% 67.25/67.25 cnf(283,plain,
% 67.25/67.25 (P4(a86,a9)),
% 67.25/67.25 inference(scs_inference,[],[194,113,198,2,14,100,80,91])).
% 67.25/67.25 cnf(288,plain,
% 67.25/67.25 (~P5(a85,a85)),
% 67.25/67.25 inference(scs_inference,[],[194,113,198,2,14,100,80,91,75,104])).
% 67.25/67.25 cnf(296,plain,
% 67.25/67.25 (P6(a58,x2961,a80)),
% 67.25/67.25 inference(rename_variables,[],[116])).
% 67.25/67.25 cnf(301,plain,
% 67.25/67.25 (P3(a5,a80)),
% 67.25/67.25 inference(scs_inference,[],[110,116,296,130,136,105,75,100])).
% 67.25/67.25 cnf(302,plain,
% 67.25/67.25 (P6(a58,x3021,a80)),
% 67.25/67.25 inference(rename_variables,[],[116])).
% 67.25/67.25 cnf(304,plain,
% 67.25/67.25 (P4(a5,a9)),
% 67.25/67.25 inference(scs_inference,[],[110,116,296,130,201,136,105,75,100,91])).
% 67.25/67.25 cnf(305,plain,
% 67.25/67.25 (P6(a58,x3051,a5)),
% 67.25/67.25 inference(rename_variables,[],[110])).
% 67.25/67.25 cnf(307,plain,
% 67.25/67.25 (~P5(a5,a80)),
% 67.25/67.25 inference(scs_inference,[],[110,305,116,296,302,130,201,136,105,75,100,91,104])).
% 67.25/67.25 cnf(313,plain,
% 67.25/67.25 (P4(a5,a90)),
% 67.25/67.25 inference(scs_inference,[],[110,201,130,142,75,91])).
% 67.25/67.25 cnf(315,plain,
% 67.25/67.25 (P6(a58,x3151,a5)),
% 67.25/67.25 inference(rename_variables,[],[110])).
% 67.25/67.25 cnf(318,plain,
% 67.25/67.25 (P6(a58,x3181,a73)),
% 67.25/67.25 inference(rename_variables,[],[119])).
% 67.25/67.25 cnf(320,plain,
% 67.25/67.25 (P3(a5,a73)),
% 67.25/67.25 inference(scs_inference,[],[110,315,119,318,201,130,142,75,91,105,100])).
% 67.25/67.25 cnf(321,plain,
% 67.25/67.25 (P6(a58,x3211,a73)),
% 67.25/67.25 inference(rename_variables,[],[119])).
% 67.25/67.25 cnf(323,plain,
% 67.25/67.25 (~P5(a5,a73)),
% 67.25/67.25 inference(scs_inference,[],[110,315,119,318,321,201,130,142,75,91,105,100,104])).
% 67.25/67.25 cnf(326,plain,
% 67.25/67.25 (P4(a5,a87)),
% 67.25/67.25 inference(scs_inference,[],[110,148,91])).
% 67.25/67.25 cnf(327,plain,
% 67.25/67.25 (~P6(a58,x3271,a87)),
% 67.25/67.25 inference(rename_variables,[],[148])).
% 67.25/67.25 cnf(332,plain,
% 67.25/67.25 (P3(a84,a84)),
% 67.25/67.25 inference(scs_inference,[],[110,214,201,148,327,91,75,100])).
% 67.25/67.25 cnf(336,plain,
% 67.25/67.25 (~P5(a84,a84)),
% 67.25/67.25 inference(scs_inference,[],[110,214,201,148,327,91,75,100,105,104])).
% 67.25/67.25 cnf(339,plain,
% 67.25/67.25 (~P6(x3391,a58,a91)),
% 67.25/67.25 inference(rename_variables,[],[154])).
% 67.25/67.25 cnf(341,plain,
% 67.25/67.25 (P4(a5,a91)),
% 67.25/67.25 inference(scs_inference,[],[110,198,154,339,75,91])).
% 67.25/67.25 cnf(347,plain,
% 67.25/67.25 (P3(a10,a10)),
% 67.25/67.25 inference(scs_inference,[],[110,210,198,154,339,75,91,105,100])).
% 67.25/67.25 cnf(349,plain,
% 67.25/67.25 (~P5(a10,a10)),
% 67.25/67.25 inference(scs_inference,[],[110,210,198,154,339,75,91,105,100,104])).
% 67.25/67.25 cnf(351,plain,
% 67.25/67.25 (P4(a5,a83)),
% 67.25/67.25 inference(scs_inference,[],[110,157,91])).
% 67.25/67.25 cnf(360,plain,
% 67.25/67.25 (~P6(x3601,a58,a89)),
% 67.25/67.25 inference(rename_variables,[],[160])).
% 67.25/67.25 cnf(362,plain,
% 67.25/67.25 (P4(a5,a89)),
% 67.25/67.25 inference(scs_inference,[],[110,198,160,360,75,91])).
% 67.25/67.25 cnf(366,plain,
% 67.25/67.25 (P4(a5,a4)),
% 67.25/67.25 inference(scs_inference,[],[110,163,91])).
% 67.25/67.25 cnf(373,plain,
% 67.25/67.25 (~P6(x3731,a58,a79)),
% 67.25/67.25 inference(rename_variables,[],[166])).
% 67.25/67.25 cnf(376,plain,
% 67.25/67.25 (P4(a5,a79)),
% 67.25/67.25 inference(scs_inference,[],[110,130,166,373,75,91])).
% 67.25/67.25 cnf(380,plain,
% 67.25/67.25 (P4(a73,a90)),
% 67.25/67.25 inference(scs_inference,[],[122,172,91])).
% 67.25/67.25 cnf(395,plain,
% 67.25/67.25 (P4(a73,a91)),
% 67.25/67.25 inference(scs_inference,[],[122,181,91])).
% 67.25/67.25 cnf(409,plain,
% 67.25/67.25 (P4(a5,a75)),
% 67.25/67.25 inference(scs_inference,[],[110,145,91])).
% 67.25/67.25 cnf(419,plain,
% 67.25/67.25 (P4(a86,a90)),
% 67.25/67.25 inference(scs_inference,[],[113,130,148,172,75,91])).
% 67.25/67.25 cnf(423,plain,
% 67.25/67.25 (P4(a73,a75)),
% 67.25/67.25 inference(scs_inference,[],[122,175,91])).
% 67.25/67.25 cnf(433,plain,
% 67.25/67.25 (P4(a86,a91)),
% 67.25/67.25 inference(scs_inference,[],[113,201,181,136,75,91])).
% 67.25/67.25 cnf(460,plain,
% 67.25/67.25 (~P1(a61,f74(a65))),
% 67.25/67.25 inference(scs_inference,[],[4,20,15])).
% 67.25/67.25 cnf(461,plain,
% 67.25/67.25 (P1(a61,a65)),
% 67.25/67.25 inference(scs_inference,[],[460,17])).
% 67.25/67.25 cnf(463,plain,
% 67.25/67.25 (~P6(x4631,a65,a88)),
% 67.25/67.25 inference(scs_inference,[],[460,17,35])).
% 67.25/67.25 cnf(465,plain,
% 67.25/67.25 (~P1(f43(a3,a65),f74(a65))),
% 67.25/67.25 inference(scs_inference,[],[8,460,17,35,101])).
% 67.25/67.25 cnf(470,plain,
% 67.25/67.25 (~P6(a3,a65,x4701)+P4(x4701,a88)),
% 67.25/67.25 inference(scs_inference,[],[8,460,17,35,101,75,91])).
% 67.25/67.25 cnf(506,plain,
% 67.25/67.25 (P6(a65,x5061,a86)),
% 67.25/67.25 inference(scs_inference,[],[465,23,17])).
% 67.25/67.25 cnf(507,plain,
% 67.25/67.25 (P1(f43(a3,a65),a65)),
% 67.25/67.25 inference(scs_inference,[],[465,17])).
% 67.25/67.25 cnf(509,plain,
% 67.25/67.25 (P3(a86,a86)),
% 67.25/67.25 inference(scs_inference,[],[506,465,17,100])).
% 67.25/67.25 cnf(513,plain,
% 67.25/67.25 (~P5(a86,a86)),
% 67.25/67.25 inference(scs_inference,[],[506,465,17,100,105,104])).
% 67.25/67.25 cnf(523,plain,
% 67.25/67.25 (P3(a73,a86)),
% 67.25/67.25 inference(scs_inference,[],[122,506,100])).
% 67.25/67.25 cnf(524,plain,
% 67.25/67.25 (P6(a65,x5241,a86)),
% 67.25/67.25 inference(rename_variables,[],[506])).
% 67.25/67.25 cnf(525,plain,
% 67.25/67.25 (P6(x5251,a3,a73)),
% 67.25/67.25 inference(rename_variables,[],[122])).
% 67.25/67.25 cnf(528,plain,
% 67.25/67.25 (P6(a65,x5281,a86)),
% 67.25/67.25 inference(rename_variables,[],[506])).
% 67.25/67.25 cnf(529,plain,
% 67.25/67.25 (P6(x5291,a3,a73)),
% 67.25/67.25 inference(rename_variables,[],[122])).
% 67.25/67.25 cnf(531,plain,
% 67.25/67.25 (~P5(a73,a86)),
% 67.25/67.25 inference(scs_inference,[],[122,525,529,506,524,528,100,105,104])).
% 67.25/67.25 cnf(547,plain,
% 67.25/67.25 (~P6(a59,a58,a9)),
% 67.25/67.25 inference(scs_inference,[],[3,14,80])).
% 67.25/67.25 cnf(548,plain,
% 67.25/67.25 (~P1(x5481,a58)),
% 67.25/67.25 inference(rename_variables,[],[14])).
% 67.25/67.25 cnf(550,plain,
% 67.25/67.25 (~P6(a58,a59,a9)),
% 67.25/67.25 inference(scs_inference,[],[3,14,548,80,81])).
% 67.25/67.25 cnf(575,plain,
% 67.25/67.25 (~P6(a62,a58,a9)),
% 67.25/67.25 inference(scs_inference,[],[4,14,80])).
% 67.25/67.25 cnf(581,plain,
% 67.25/67.25 (~P6(f49(x5811,a88),f50(x5811,a88),a88)+~P6(a3,a65,x5811)),
% 67.25/67.25 inference(scs_inference,[],[470,102])).
% 67.25/67.25 cnf(582,plain,
% 67.25/67.25 (~P2(a88,a9)+~P6(x5821,a58,a88)),
% 67.25/67.25 inference(scs_inference,[],[198,222,94])).
% 67.25/67.25 cnf(583,plain,
% 67.25/67.25 (~P6(a58,a65,a9)),
% 67.25/67.25 inference(scs_inference,[],[5,14,81])).
% 67.25/67.25 cnf(589,plain,
% 67.25/67.25 (~P1(f43(a3,a58),f74(a58))+~P2(a88,a9)),
% 67.25/67.25 inference(scs_inference,[],[582,218])).
% 67.25/67.25 cnf(591,plain,
% 67.25/67.25 (~P6(a69,a58,a9)),
% 67.25/67.25 inference(scs_inference,[],[6,14,80])).
% 67.25/67.25 cnf(592,plain,
% 67.25/67.25 (~P1(x5921,a58)),
% 67.25/67.25 inference(rename_variables,[],[14])).
% 67.25/67.25 cnf(594,plain,
% 67.25/67.25 (~P6(a58,a69,a9)),
% 67.25/67.25 inference(scs_inference,[],[6,14,592,80,81])).
% 67.25/67.25 cnf(597,plain,
% 67.25/67.25 (P6(a3,f74(a58),a84)),
% 67.25/67.25 inference(scs_inference,[],[14,254,17])).
% 67.25/67.25 cnf(598,plain,
% 67.25/67.25 (P1(x5981,f74(a58))),
% 67.25/67.25 inference(scs_inference,[],[597,28])).
% 67.25/67.25 cnf(602,plain,
% 67.25/67.25 (~P2(a88,a9)),
% 67.25/67.25 inference(scs_inference,[],[598,589])).
% 67.25/67.25 cnf(605,plain,
% 67.25/67.25 (P1(x6051,f74(a58))),
% 67.25/67.25 inference(rename_variables,[],[598])).
% 67.25/67.25 cnf(608,plain,
% 67.25/67.25 (P1(x6081,f74(a58))),
% 67.25/67.25 inference(rename_variables,[],[598])).
% 67.25/67.25 cnf(611,plain,
% 67.25/67.25 (P1(x6111,f74(a58))),
% 67.25/67.25 inference(rename_variables,[],[598])).
% 67.25/67.25 cnf(614,plain,
% 67.25/67.25 (P1(x6141,f74(a58))),
% 67.25/67.25 inference(rename_variables,[],[598])).
% 67.25/67.25 cnf(617,plain,
% 67.25/67.25 (P1(x6171,f74(a58))),
% 67.25/67.25 inference(rename_variables,[],[598])).
% 67.25/67.25 cnf(619,plain,
% 67.25/67.25 (P6(x6191,f74(a58),a73)),
% 67.25/67.25 inference(scs_inference,[],[598,605,608,611,614,617,84,83,87,85,86,42])).
% 67.25/67.25 cnf(620,plain,
% 67.25/67.25 (P1(x6201,f74(a58))),
% 67.25/67.25 inference(rename_variables,[],[598])).
% 67.25/67.25 cnf(623,plain,
% 67.25/67.25 (P1(x6231,f74(a58))),
% 67.25/67.25 inference(rename_variables,[],[598])).
% 67.25/67.25 cnf(624,plain,
% 67.25/67.25 (P1(x6241,a3)),
% 67.25/67.25 inference(rename_variables,[],[8])).
% 67.25/67.25 cnf(630,plain,
% 67.25/67.25 (P3(a88,a88)),
% 67.25/67.25 inference(scs_inference,[],[8,624,598,605,608,611,614,617,620,623,84,83,87,85,86,42,98,101,100])).
% 67.25/67.25 cnf(632,plain,
% 67.25/67.25 (~P5(a88,a88)),
% 67.25/67.25 inference(scs_inference,[],[8,624,598,605,608,611,614,617,620,623,84,83,87,85,86,42,98,101,100,104])).
% 67.25/67.25 cnf(653,plain,
% 67.25/67.25 (P6(f48(a5,a5),f51(a5,a5),a5)),
% 67.25/67.25 inference(scs_inference,[],[110,51,104])).
% 67.25/67.25 cnf(654,plain,
% 67.25/67.25 (~P1(x6541,f48(a5,a5))),
% 67.25/67.25 inference(scs_inference,[],[653,36])).
% 67.25/67.25 cnf(664,plain,
% 67.25/67.25 (P1(x6641,f48(a84,a84))),
% 67.25/67.25 inference(scs_inference,[],[336,52,31])).
% 67.25/67.25 cnf(665,plain,
% 67.25/67.25 (~P6(x6651,f48(a5,a5),a91)),
% 67.25/67.25 inference(scs_inference,[],[654,62])).
% 67.25/67.25 cnf(666,plain,
% 67.25/67.25 (~P1(x6661,f48(a5,a5))),
% 67.25/67.25 inference(rename_variables,[],[654])).
% 67.25/67.25 cnf(668,plain,
% 67.25/67.25 (P6(f48(a5,a5),x6681,a73)),
% 67.25/67.25 inference(scs_inference,[],[654,666,62,26])).
% 67.25/67.25 cnf(669,plain,
% 67.25/67.25 (~P1(x6691,f48(a5,a5))),
% 67.25/67.25 inference(rename_variables,[],[654])).
% 67.25/67.25 cnf(671,plain,
% 67.25/67.25 (P6(x6711,f48(a5,a5),a86)),
% 67.25/67.25 inference(scs_inference,[],[654,666,669,62,26,24])).
% 67.25/67.25 cnf(672,plain,
% 67.25/67.25 (~P1(x6721,f48(a5,a5))),
% 67.25/67.25 inference(rename_variables,[],[654])).
% 67.25/67.25 cnf(675,plain,
% 67.25/67.25 (~P1(x6751,f48(a5,a5))),
% 67.25/67.25 inference(rename_variables,[],[654])).
% 67.25/67.25 cnf(678,plain,
% 67.28/67.25 (~P1(x6781,f48(a5,a5))),
% 67.28/67.25 inference(rename_variables,[],[654])).
% 67.28/67.25 cnf(681,plain,
% 67.28/67.25 (P1(x6811,f48(a84,a84))),
% 67.28/67.25 inference(rename_variables,[],[664])).
% 67.28/67.25 cnf(684,plain,
% 67.28/67.25 (~P1(x6841,f48(a5,a5))),
% 67.28/67.25 inference(rename_variables,[],[654])).
% 67.28/67.26 cnf(687,plain,
% 67.28/67.26 (~P1(x6871,f48(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[654])).
% 67.28/67.26 cnf(690,plain,
% 67.28/67.26 (~P1(x6901,f48(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[654])).
% 67.28/67.26 cnf(693,plain,
% 67.28/67.26 (~P1(x6931,f48(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[654])).
% 67.28/67.26 cnf(696,plain,
% 67.28/67.26 (P1(x6961,f48(a84,a84))),
% 67.28/67.26 inference(rename_variables,[],[664])).
% 67.28/67.26 cnf(699,plain,
% 67.28/67.26 (~P1(x6991,f48(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[654])).
% 67.28/67.26 cnf(702,plain,
% 67.28/67.26 (~P1(x7021,f48(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[654])).
% 67.28/67.26 cnf(705,plain,
% 67.28/67.26 (~P1(x7051,f48(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[654])).
% 67.28/67.26 cnf(708,plain,
% 67.28/67.26 (~P1(x7081,f48(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[654])).
% 67.28/67.26 cnf(711,plain,
% 67.28/67.26 (~P1(x7111,f48(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[654])).
% 67.28/67.26 cnf(714,plain,
% 67.28/67.26 (~P1(x7141,f48(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[654])).
% 67.28/67.26 cnf(717,plain,
% 67.28/67.26 (~P1(x7171,f48(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[654])).
% 67.28/67.26 cnf(720,plain,
% 67.28/67.26 (P1(x7201,f48(a84,a84))),
% 67.28/67.26 inference(rename_variables,[],[664])).
% 67.28/67.26 cnf(723,plain,
% 67.28/67.26 (P1(x7231,f48(a84,a84))),
% 67.28/67.26 inference(rename_variables,[],[664])).
% 67.28/67.26 cnf(726,plain,
% 67.28/67.26 (~P1(x7261,f48(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[654])).
% 67.28/67.26 cnf(729,plain,
% 67.28/67.26 (P1(x7291,f48(a84,a84))),
% 67.28/67.26 inference(rename_variables,[],[664])).
% 67.28/67.26 cnf(731,plain,
% 67.28/67.26 (P6(f48(a5,a5),x7311,a80)),
% 67.28/67.26 inference(scs_inference,[],[654,666,669,672,675,678,684,687,690,693,699,702,705,708,711,714,717,726,664,681,696,720,723,62,26,24,60,58,83,64,54,53,56,85,59,55,65,66,57,61,63,82,42,21,84,25])).
% 67.28/67.26 cnf(732,plain,
% 67.28/67.26 (~P1(x7321,f48(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[654])).
% 67.28/67.26 cnf(735,plain,
% 67.28/67.26 (P1(x7351,f48(a84,a84))),
% 67.28/67.26 inference(rename_variables,[],[664])).
% 67.28/67.26 cnf(738,plain,
% 67.28/67.26 (P1(x7381,f48(a84,a84))),
% 67.28/67.26 inference(rename_variables,[],[664])).
% 67.28/67.26 cnf(740,plain,
% 67.28/67.26 (P6(a58,f48(a5,a5),a9)),
% 67.28/67.26 inference(scs_inference,[],[14,654,666,669,672,675,678,684,687,690,693,699,702,705,708,711,714,717,726,732,664,681,696,720,723,729,735,62,26,24,60,58,83,64,54,53,56,85,59,55,65,66,57,61,63,82,42,21,84,25,87,86,76])).
% 67.28/67.26 cnf(742,plain,
% 67.28/67.26 (~P1(x7421,f48(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[654])).
% 67.28/67.26 cnf(745,plain,
% 67.28/67.26 (P1(x7451,a3)),
% 67.28/67.26 inference(rename_variables,[],[8])).
% 67.28/67.26 cnf(746,plain,
% 67.28/67.26 (P1(x7461,f48(a84,a84))),
% 67.28/67.26 inference(rename_variables,[],[664])).
% 67.28/67.26 cnf(749,plain,
% 67.28/67.26 (~P1(x7491,f48(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[654])).
% 67.28/67.26 cnf(759,plain,
% 67.28/67.26 (P3(a9,a9)),
% 67.28/67.26 inference(scs_inference,[],[6,8,745,14,654,666,669,672,675,678,684,687,690,693,699,702,705,708,711,714,717,726,732,742,749,664,681,696,720,723,729,735,738,746,598,62,26,24,60,58,83,64,54,53,56,85,59,55,65,66,57,61,63,82,42,21,84,25,87,86,76,98,93,101,81,100])).
% 67.28/67.26 cnf(761,plain,
% 67.28/67.26 (~P5(a9,a9)),
% 67.28/67.26 inference(scs_inference,[],[6,8,745,14,654,666,669,672,675,678,684,687,690,693,699,702,705,708,711,714,717,726,732,742,749,664,681,696,720,723,729,735,738,746,598,62,26,24,60,58,83,64,54,53,56,85,59,55,65,66,57,61,63,82,42,21,84,25,87,86,76,98,93,101,81,100,104])).
% 67.28/67.26 cnf(785,plain,
% 67.28/67.26 (P6(f45(a5,a5),f46(a5,a5),a5)),
% 67.28/67.26 inference(scs_inference,[],[110,69,100])).
% 67.28/67.26 cnf(786,plain,
% 67.28/67.26 (~P1(x7861,f45(a5,a5))),
% 67.28/67.26 inference(scs_inference,[],[785,36])).
% 67.28/67.26 cnf(818,plain,
% 67.28/67.26 (~P1(x8181,f45(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[786])).
% 67.28/67.26 cnf(820,plain,
% 67.28/67.26 (P6(f45(a5,a5),x8201,a73)),
% 67.28/67.26 inference(scs_inference,[],[786,818,68,26])).
% 67.28/67.26 cnf(821,plain,
% 67.28/67.26 (~P1(x8211,f45(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[786])).
% 67.28/67.26 cnf(824,plain,
% 67.28/67.26 (~P1(x8241,f45(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[786])).
% 67.28/67.26 cnf(827,plain,
% 67.28/67.26 (~P1(x8271,f45(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[786])).
% 67.28/67.26 cnf(830,plain,
% 67.28/67.26 (~P1(x8301,f45(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[786])).
% 67.28/67.26 cnf(833,plain,
% 67.28/67.26 (~P1(x8331,f45(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[786])).
% 67.28/67.26 cnf(836,plain,
% 67.28/67.26 (~P1(x8361,f45(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[786])).
% 67.28/67.26 cnf(839,plain,
% 67.28/67.26 (~P1(x8391,f45(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[786])).
% 67.28/67.26 cnf(842,plain,
% 67.28/67.26 (~P1(x8421,f45(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[786])).
% 67.28/67.26 cnf(845,plain,
% 67.28/67.26 (~P1(x8451,f45(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[786])).
% 67.28/67.26 cnf(848,plain,
% 67.28/67.26 (~P1(x8481,f45(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[786])).
% 67.28/67.26 cnf(851,plain,
% 67.28/67.26 (~P1(x8511,f45(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[786])).
% 67.28/67.26 cnf(854,plain,
% 67.28/67.26 (~P1(x8541,f45(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[786])).
% 67.28/67.26 cnf(856,plain,
% 67.28/67.26 (P6(x8561,f45(a5,a5),a86)),
% 67.28/67.26 inference(scs_inference,[],[786,818,821,824,827,830,833,836,839,842,845,848,851,854,68,26,60,59,64,54,65,53,56,25,55,58,62,24])).
% 67.28/67.26 cnf(857,plain,
% 67.28/67.26 (~P1(x8571,f45(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[786])).
% 67.28/67.26 cnf(860,plain,
% 67.28/67.26 (~P1(x8601,f45(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[786])).
% 67.28/67.26 cnf(863,plain,
% 67.28/67.26 (~P1(x8631,f45(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[786])).
% 67.28/67.26 cnf(866,plain,
% 67.28/67.26 (~P1(x8661,f45(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[786])).
% 67.28/67.26 cnf(869,plain,
% 67.28/67.26 (~P1(x8691,f45(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[786])).
% 67.28/67.26 cnf(873,plain,
% 67.28/67.26 (~P1(x8731,f45(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[786])).
% 67.28/67.26 cnf(876,plain,
% 67.28/67.26 (~P1(x8761,f45(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[786])).
% 67.28/67.26 cnf(882,plain,
% 67.28/67.26 (P3(a86,a73)),
% 67.28/67.26 inference(scs_inference,[],[6,671,8,14,786,818,821,824,827,830,833,836,839,842,845,848,851,854,857,860,863,866,869,873,876,68,26,60,59,64,54,65,53,56,25,55,58,62,24,63,21,66,61,76,93,81,100])).
% 67.28/67.26 cnf(883,plain,
% 67.28/67.26 (P6(x8831,f48(a5,a5),a86)),
% 67.28/67.26 inference(rename_variables,[],[671])).
% 67.28/67.26 cnf(888,plain,
% 67.28/67.26 (~P5(a73,a73)),
% 67.28/67.26 inference(scs_inference,[],[6,671,883,8,14,786,818,821,824,827,830,833,836,839,842,845,848,851,854,857,860,863,866,869,873,876,68,26,60,59,64,54,65,53,56,25,55,58,62,24,63,21,66,61,76,93,81,100,105,104])).
% 67.28/67.26 cnf(954,plain,
% 67.28/67.26 (P1(x9541,f74(f46(a88,a88)))),
% 67.28/67.26 inference(scs_inference,[],[630,70,35])).
% 67.28/67.26 cnf(955,plain,
% 67.28/67.26 (~P1(x9551,f46(a88,a88))),
% 67.28/67.26 inference(scs_inference,[],[954,20])).
% 67.28/67.26 cnf(965,plain,
% 67.28/67.26 (~P1(x9651,f46(a88,a88))),
% 67.28/67.26 inference(rename_variables,[],[955])).
% 67.28/67.26 cnf(968,plain,
% 67.28/67.26 (~P1(x9681,f46(a88,a88))),
% 67.28/67.26 inference(rename_variables,[],[955])).
% 67.28/67.26 cnf(971,plain,
% 67.28/67.26 (~P1(x9711,f46(a88,a88))),
% 67.28/67.26 inference(rename_variables,[],[955])).
% 67.28/67.26 cnf(974,plain,
% 67.28/67.26 (~P1(x9741,f46(a88,a88))),
% 67.28/67.26 inference(rename_variables,[],[955])).
% 67.28/67.26 cnf(977,plain,
% 67.28/67.26 (~P1(x9771,f46(a88,a88))),
% 67.28/67.26 inference(rename_variables,[],[955])).
% 67.28/67.26 cnf(980,plain,
% 67.28/67.26 (~P1(x9801,f46(a88,a88))),
% 67.28/67.26 inference(rename_variables,[],[955])).
% 67.28/67.26 cnf(983,plain,
% 67.28/67.26 (~P1(x9831,f46(a88,a88))),
% 67.28/67.26 inference(rename_variables,[],[955])).
% 67.28/67.26 cnf(986,plain,
% 67.28/67.26 (~P1(x9861,f46(a88,a88))),
% 67.28/67.26 inference(rename_variables,[],[955])).
% 67.28/67.26 cnf(988,plain,
% 67.28/67.26 (P6(x9881,f46(a88,a88),a86)),
% 67.28/67.26 inference(scs_inference,[],[955,965,968,971,974,977,980,983,986,26,54,59,57,65,58,53,60,24])).
% 67.28/67.26 cnf(989,plain,
% 67.28/67.26 (~P1(x9891,f46(a88,a88))),
% 67.28/67.26 inference(rename_variables,[],[955])).
% 67.28/67.26 cnf(992,plain,
% 67.28/67.26 (~P1(x9921,f46(a88,a88))),
% 67.28/67.26 inference(rename_variables,[],[955])).
% 67.28/67.26 cnf(994,plain,
% 67.28/67.26 (~P6(f46(a88,a88),x9941,a81)),
% 67.28/67.26 inference(scs_inference,[],[955,965,968,971,974,977,980,983,986,989,992,26,54,59,57,65,58,53,60,24,21,56])).
% 67.28/67.26 cnf(995,plain,
% 67.28/67.26 (~P1(x9951,f46(a88,a88))),
% 67.28/67.26 inference(rename_variables,[],[955])).
% 67.28/67.26 cnf(998,plain,
% 67.28/67.26 (~P1(x9981,f46(a88,a88))),
% 67.28/67.26 inference(rename_variables,[],[955])).
% 67.28/67.26 cnf(1001,plain,
% 67.28/67.26 (~P1(x10011,f46(a88,a88))),
% 67.28/67.26 inference(rename_variables,[],[955])).
% 67.28/67.26 cnf(1004,plain,
% 67.28/67.26 (~P1(x10041,f46(a88,a88))),
% 67.28/67.26 inference(rename_variables,[],[955])).
% 67.28/67.26 cnf(1007,plain,
% 67.28/67.26 (~P1(x10071,f46(a88,a88))),
% 67.28/67.26 inference(rename_variables,[],[955])).
% 67.28/67.26 cnf(1010,plain,
% 67.28/67.26 (~P1(x10101,f46(a88,a88))),
% 67.28/67.26 inference(rename_variables,[],[955])).
% 67.28/67.26 cnf(1013,plain,
% 67.28/67.26 (~P1(x10131,f46(a88,a88))),
% 67.28/67.26 inference(rename_variables,[],[955])).
% 67.28/67.26 cnf(1016,plain,
% 67.28/67.26 (~P1(x10161,f46(a88,a88))),
% 67.28/67.26 inference(rename_variables,[],[955])).
% 67.28/67.26 cnf(1019,plain,
% 67.28/67.26 (~P1(x10191,f46(a88,a88))),
% 67.28/67.26 inference(rename_variables,[],[955])).
% 67.28/67.26 cnf(1023,plain,
% 67.28/67.26 (~P1(x10231,f46(a88,a88))),
% 67.28/67.26 inference(rename_variables,[],[955])).
% 67.28/67.26 cnf(1034,plain,
% 67.28/67.26 (P6(x10341,f45(a5,a5),a86)),
% 67.28/67.26 inference(rename_variables,[],[856])).
% 67.28/67.26 cnf(1036,plain,
% 67.28/67.26 (P3(a73,a73)),
% 67.28/67.26 inference(scs_inference,[],[6,856,8,14,598,955,965,968,971,974,977,980,983,986,989,992,995,998,1001,1004,1007,1010,1013,1016,1019,1023,954,26,54,59,57,65,58,53,60,24,21,56,25,64,62,55,61,63,66,76,93,101,80,105,100])).
% 67.28/67.26 cnf(1038,plain,
% 67.28/67.26 (~P5(a86,a5)),
% 67.28/67.26 inference(scs_inference,[],[6,856,1034,8,14,598,955,965,968,971,974,977,980,983,986,989,992,995,998,1001,1004,1007,1010,1013,1016,1019,1023,954,26,54,59,57,65,58,53,60,24,21,56,25,64,62,55,61,63,66,76,93,101,80,105,100,104])).
% 67.28/67.26 cnf(1184,plain,
% 67.28/67.26 (~P2(x11841,a88)+~P6(f49(x11842,a88),f50(x11842,a88),x11841)+~P6(a3,a65,x11842)),
% 67.28/67.26 inference(scs_inference,[],[581,94])).
% 67.28/67.26 cnf(1185,plain,
% 67.28/67.26 (P3(a86,a5)),
% 67.28/67.26 inference(scs_inference,[],[113,110,100])).
% 67.28/67.26 cnf(1186,plain,
% 67.28/67.26 (P6(a58,x11861,a5)),
% 67.28/67.26 inference(rename_variables,[],[110])).
% 67.28/67.26 cnf(1187,plain,
% 67.28/67.26 (P6(x11871,a58,a86)),
% 67.28/67.26 inference(rename_variables,[],[113])).
% 67.28/67.26 cnf(1191,plain,
% 67.28/67.26 (P6(x11911,a58,a86)),
% 67.28/67.26 inference(rename_variables,[],[113])).
% 67.28/67.26 cnf(1193,plain,
% 67.28/67.26 (~P5(a86,a73)),
% 67.28/67.26 inference(scs_inference,[],[113,1187,1191,110,1186,668,100,105,104])).
% 67.28/67.26 cnf(1202,plain,
% 67.28/67.26 (P3(a86,a80)),
% 67.28/67.26 inference(scs_inference,[],[113,731,100])).
% 67.28/67.26 cnf(1203,plain,
% 67.28/67.26 (P6(f48(a5,a5),x12031,a80)),
% 67.28/67.26 inference(rename_variables,[],[731])).
% 67.28/67.26 cnf(1204,plain,
% 67.28/67.26 (P6(x12041,a58,a86)),
% 67.28/67.26 inference(rename_variables,[],[113])).
% 67.28/67.26 cnf(1206,plain,
% 67.28/67.26 (~P5(a86,a80)),
% 67.28/67.26 inference(scs_inference,[],[113,1204,731,1203,100,104])).
% 67.28/67.26 cnf(1235,plain,
% 67.28/67.26 (P3(a80,a80)),
% 67.28/67.26 inference(scs_inference,[],[116,105,100])).
% 67.28/67.26 cnf(1237,plain,
% 67.28/67.26 (~P5(a80,a80)),
% 67.28/67.26 inference(scs_inference,[],[116,105,100,104])).
% 67.28/67.26 cnf(1244,plain,
% 67.28/67.26 (P6(a58,x12441,a5)),
% 67.28/67.26 inference(rename_variables,[],[110])).
% 67.28/67.26 cnf(1247,plain,
% 67.28/67.26 (P6(a58,x12471,a5)),
% 67.28/67.26 inference(rename_variables,[],[110])).
% 67.28/67.26 cnf(1249,plain,
% 67.28/67.26 (~P5(a80,a5)),
% 67.28/67.26 inference(scs_inference,[],[116,110,1244,1247,105,100,104])).
% 67.28/67.26 cnf(1256,plain,
% 67.28/67.26 (P6(x12561,f74(a58),a73)),
% 67.28/67.26 inference(rename_variables,[],[619])).
% 67.28/67.26 cnf(1257,plain,
% 67.28/67.26 (P6(a58,x12571,a80)),
% 67.28/67.26 inference(rename_variables,[],[116])).
% 67.28/67.26 cnf(1259,plain,
% 67.28/67.26 (P3(a80,a73)),
% 67.28/67.26 inference(scs_inference,[],[116,1257,619,1256,105,100])).
% 67.28/67.26 cnf(1260,plain,
% 67.28/67.26 (P6(x12601,f74(a58),a73)),
% 67.28/67.26 inference(rename_variables,[],[619])).
% 67.28/67.26 cnf(1261,plain,
% 67.28/67.26 (P6(a58,x12611,a80)),
% 67.28/67.26 inference(rename_variables,[],[116])).
% 67.28/67.26 cnf(1263,plain,
% 67.28/67.26 (~P5(a80,a73)),
% 67.28/67.26 inference(scs_inference,[],[116,1257,1261,619,1256,1260,105,100,104])).
% 67.28/67.26 cnf(1265,plain,
% 67.28/67.26 (P6(a58,x12651,a80)),
% 67.28/67.26 inference(rename_variables,[],[116])).
% 67.28/67.26 cnf(1267,plain,
% 67.28/67.26 (P4(a80,a88)),
% 67.28/67.26 inference(scs_inference,[],[116,1257,1261,1265,619,1256,1260,463,105,100,104,91])).
% 67.28/67.26 cnf(1273,plain,
% 67.28/67.26 (P6(x12731,f46(a88,a88),a86)),
% 67.28/67.26 inference(rename_variables,[],[988])).
% 67.28/67.26 cnf(1274,plain,
% 67.28/67.26 (P6(a58,x12741,a80)),
% 67.28/67.26 inference(rename_variables,[],[116])).
% 67.28/67.26 cnf(1276,plain,
% 67.28/67.26 (P3(a80,a86)),
% 67.28/67.26 inference(scs_inference,[],[116,1274,988,1273,105,100])).
% 67.28/67.26 cnf(1277,plain,
% 67.28/67.26 (P6(x12771,f46(a88,a88),a86)),
% 67.28/67.26 inference(rename_variables,[],[988])).
% 67.28/67.26 cnf(1278,plain,
% 67.28/67.26 (P6(a58,x12781,a80)),
% 67.28/67.26 inference(rename_variables,[],[116])).
% 67.28/67.26 cnf(1280,plain,
% 67.28/67.26 (~P5(a80,a86)),
% 67.28/67.26 inference(scs_inference,[],[116,1274,1278,988,1273,1277,105,100,104])).
% 67.28/67.26 cnf(1321,plain,
% 67.28/67.26 (P6(a65,a3,a82)),
% 67.28/67.26 inference(scs_inference,[],[8,4,34,15])).
% 67.28/67.26 cnf(1322,plain,
% 67.28/67.26 (P3(a82,a82)),
% 67.28/67.26 inference(scs_inference,[],[1321,100])).
% 67.28/67.26 cnf(1324,plain,
% 67.28/67.26 (~P5(a82,a82)),
% 67.28/67.26 inference(scs_inference,[],[1321,100,104])).
% 67.28/67.26 cnf(1349,plain,
% 67.28/67.26 (P6(a58,x13491,a80)),
% 67.28/67.26 inference(rename_variables,[],[116])).
% 67.28/67.26 cnf(1351,plain,
% 67.28/67.26 (P3(a73,a80)),
% 67.28/67.26 inference(scs_inference,[],[119,116,1349,105,100])).
% 67.28/67.26 cnf(1352,plain,
% 67.28/67.26 (P6(a58,x13521,a80)),
% 67.28/67.26 inference(rename_variables,[],[116])).
% 67.28/67.26 cnf(1354,plain,
% 67.28/67.26 (~P5(a73,a80)),
% 67.28/67.26 inference(scs_inference,[],[119,116,1349,1352,105,100,104])).
% 67.28/67.26 cnf(1363,plain,
% 67.28/67.26 (~P6(x13631,f46(a88,a88),a81)),
% 67.28/67.26 inference(scs_inference,[],[994,8,77,27])).
% 67.28/67.26 cnf(1505,plain,
% 67.28/67.26 (P6(x15051,a65,a80)),
% 67.28/67.26 inference(scs_inference,[],[4,15,22])).
% 67.28/67.26 cnf(1508,plain,
% 67.28/67.26 (P6(x15081,a65,a80)),
% 67.28/67.26 inference(rename_variables,[],[1505])).
% 67.28/67.26 cnf(1514,plain,
% 67.28/67.26 (~P6(f49(a80,a88),f50(a80,a88),x15141)+~P2(x15141,a88)),
% 67.28/67.26 inference(scs_inference,[],[136,1505,1508,665,581,75,1184])).
% 67.28/67.26 cnf(1632,plain,
% 67.28/67.26 (~P2(a80,a88)),
% 67.28/67.26 inference(scs_inference,[],[1267,1514,71])).
% 67.28/67.26 cnf(1672,plain,
% 67.28/67.26 (P1(a68,f74(a62))),
% 67.28/67.26 inference(scs_inference,[],[11,15,17])).
% 67.28/67.26 cnf(1676,plain,
% 67.28/67.26 (~P6(a65,x16761,a5)),
% 67.28/67.26 inference(scs_inference,[],[4,15,36])).
% 67.28/67.26 cnf(1684,plain,
% 67.28/67.26 (~P6(x16841,a62,a81)),
% 67.28/67.26 inference(scs_inference,[],[11,15,27])).
% 67.28/67.26 cnf(1689,plain,
% 67.28/67.26 (~P6(a65,x16891,a83)),
% 67.28/67.26 inference(scs_inference,[],[4,15,37])).
% 67.28/67.26 cnf(1694,plain,
% 67.28/67.26 (~P6(x16941,a62,a84)),
% 67.28/67.26 inference(scs_inference,[],[11,15,28])).
% 67.28/67.26 cnf(1695,plain,
% 67.28/67.26 (~P1(f24(a3,a62),a62)),
% 67.28/67.26 inference(scs_inference,[],[1694,254])).
% 67.28/67.26 cnf(1698,plain,
% 67.28/67.26 (~P6(a65,x16981,a85)),
% 67.28/67.26 inference(scs_inference,[],[4,15,38])).
% 67.28/67.26 cnf(1707,plain,
% 67.28/67.26 (~P6(x17071,a62,a87)),
% 67.28/67.26 inference(scs_inference,[],[11,15,29])).
% 67.28/67.26 cnf(1708,plain,
% 67.28/67.26 (~P6(a65,x17081,a89)),
% 67.28/67.26 inference(scs_inference,[],[4,15,39])).
% 67.28/67.26 cnf(1722,plain,
% 67.28/67.26 (P6(a65,a58,a4)),
% 67.28/67.26 inference(scs_inference,[],[4,598,15,40])).
% 67.28/67.26 cnf(1725,plain,
% 67.28/67.26 (P3(a4,a4)),
% 67.28/67.26 inference(scs_inference,[],[1722,105,100])).
% 67.28/67.26 cnf(1727,plain,
% 67.28/67.26 (~P5(a4,a4)),
% 67.28/67.26 inference(scs_inference,[],[1722,105,100,104])).
% 67.28/67.26 cnf(1729,plain,
% 67.28/67.26 (~P6(a62,x17291,a84)),
% 67.28/67.26 inference(scs_inference,[],[11,15,31])).
% 67.28/67.26 cnf(1734,plain,
% 67.28/67.26 (P6(a58,a65,a83)),
% 67.28/67.26 inference(scs_inference,[],[4,14,15,41])).
% 67.28/67.26 cnf(1737,plain,
% 67.28/67.26 (P3(a83,a83)),
% 67.28/67.26 inference(scs_inference,[],[1734,105,100])).
% 67.28/67.26 cnf(1739,plain,
% 67.28/67.26 (~P5(a83,a83)),
% 67.28/67.26 inference(scs_inference,[],[1734,105,100,104])).
% 67.28/67.26 cnf(1741,plain,
% 67.28/67.26 (~P6(a62,x17411,a88)),
% 67.28/67.26 inference(scs_inference,[],[11,15,32])).
% 67.28/67.26 cnf(1746,plain,
% 67.28/67.26 (~P6(a62,a3,a10)),
% 67.28/67.26 inference(scs_inference,[],[11,8,15,44])).
% 67.28/67.26 cnf(1751,plain,
% 67.28/67.26 (~P6(a65,a58,a75)),
% 67.28/67.26 inference(scs_inference,[],[4,14,15,48])).
% 67.28/67.26 cnf(1756,plain,
% 67.28/67.26 (~P6(a62,a3,a75)),
% 67.28/67.26 inference(scs_inference,[],[11,8,15,45])).
% 67.28/67.26 cnf(1761,plain,
% 67.28/67.26 (P6(a65,a3,a81)),
% 67.28/67.26 inference(scs_inference,[],[4,8,15,77])).
% 67.28/67.26 cnf(1762,plain,
% 67.28/67.26 (P3(a81,a81)),
% 67.28/67.26 inference(scs_inference,[],[1761,100])).
% 67.28/67.26 cnf(1764,plain,
% 67.28/67.26 (~P5(a81,a81)),
% 67.28/67.26 inference(scs_inference,[],[1761,100,104])).
% 67.28/67.26 cnf(1770,plain,
% 67.28/67.26 (P1(f60(a62,a58),a65)),
% 67.28/67.26 inference(scs_inference,[],[14,575,15,76])).
% 67.28/67.26 cnf(1774,plain,
% 67.28/67.26 (~P6(a58,a65,a86)),
% 67.28/67.26 inference(scs_inference,[],[4,14,15,78])).
% 67.28/67.26 cnf(1782,plain,
% 67.28/67.26 (~P6(a3,a62,a10)),
% 67.28/67.26 inference(scs_inference,[],[11,8,15,46])).
% 67.28/67.26 cnf(1949,plain,
% 67.28/67.26 (~P6(a65,a58,a80)),
% 67.28/67.26 inference(scs_inference,[],[4,14,15,79])).
% 67.28/67.26 cnf(1961,plain,
% 67.28/67.26 (P6(a65,a3,a87)),
% 67.28/67.26 inference(scs_inference,[],[4,8,11,15,90])).
% 67.28/67.26 cnf(1962,plain,
% 67.28/67.26 (P3(a87,a87)),
% 67.28/67.26 inference(scs_inference,[],[1961,100])).
% 67.28/67.26 cnf(1964,plain,
% 67.28/67.26 (~P5(a87,a87)),
% 67.28/67.26 inference(scs_inference,[],[1961,100,104])).
% 67.28/67.26 cnf(1966,plain,
% 67.28/67.26 (P6(a58,a62,a89)),
% 67.28/67.26 inference(scs_inference,[],[11,14,4,15,74])).
% 67.28/67.26 cnf(1969,plain,
% 67.28/67.26 (P3(a89,a89)),
% 67.28/67.26 inference(scs_inference,[],[1966,105,100])).
% 67.28/67.26 cnf(1971,plain,
% 67.28/67.26 (~P5(a89,a89)),
% 67.28/67.26 inference(scs_inference,[],[1966,105,100,104])).
% 67.28/67.26 cnf(1973,plain,
% 67.28/67.26 (~P1(f26(a65,a3),a62)),
% 67.28/67.26 inference(scs_inference,[],[1961,15,84])).
% 67.28/67.26 cnf(1987,plain,
% 67.28/67.26 (P6(a62,a3,a87)),
% 67.28/67.26 inference(scs_inference,[],[11,8,4,15,90])).
% 67.28/67.26 cnf(1992,plain,
% 67.28/67.26 (P6(a58,a65,a89)),
% 67.28/67.26 inference(scs_inference,[],[4,14,11,15,74])).
% 67.28/67.26 cnf(2002,plain,
% 67.28/67.26 (~P1(f39(a58,a65),a62)),
% 67.28/67.26 inference(scs_inference,[],[1992,15,87])).
% 67.28/67.26 cnf(2007,plain,
% 67.28/67.26 (~P1(f19(a62,a3),a62)),
% 67.28/67.26 inference(scs_inference,[],[11,8,1756,4,15,107])).
% 67.28/67.26 cnf(2012,plain,
% 67.28/67.26 (P1(f19(a65,a58),a65)),
% 67.28/67.26 inference(scs_inference,[],[4,14,1751,11,15,96])).
% 67.28/67.26 cnf(2097,plain,
% 67.28/67.26 (P6(a65,a3,a75)+~P1(f19(a65,a3),a62)),
% 67.28/67.26 inference(scs_inference,[],[8,11,15,107])).
% 67.28/67.26 cnf(2102,plain,
% 67.28/67.26 (~P1(f19(a65,a3),a62)),
% 67.28/67.26 inference(scs_inference,[],[11,8,2097,45])).
% 67.28/67.26 cnf(2111,plain,
% 67.28/67.26 (~P6(a59,a3,a10)+~P1(a63,a56)),
% 67.28/67.26 inference(scs_inference,[],[8,18,44])).
% 67.28/67.26 cnf(2116,plain,
% 67.28/67.26 (~P2(a73,a10)+~P1(a63,a56)),
% 67.28/67.26 inference(scs_inference,[],[122,2111,94])).
% 67.28/67.26 cnf(2195,plain,
% 67.28/67.26 (~P6(a59,f74(a58),a10)+~P1(a63,a56)),
% 67.28/67.26 inference(scs_inference,[],[598,18,44])).
% 67.28/67.26 cnf(2200,plain,
% 67.28/67.26 (~P1(f12(a59,f74(a58)),a59)+~P1(a63,a56)),
% 67.28/67.26 inference(scs_inference,[],[598,3,2195,106])).
% 67.28/67.26 cnf(2205,plain,
% 67.28/67.26 (~P6(a59,f74(a58),a75)+~P1(a63,a56)),
% 67.28/67.26 inference(scs_inference,[],[598,2200,45])).
% 67.28/67.26 cnf(2210,plain,
% 67.28/67.26 (~P2(a73,a75)+~P1(a63,a56)),
% 67.28/67.26 inference(scs_inference,[],[619,2205,94])).
% 67.28/67.26 cnf(2248,plain,
% 67.28/67.26 (~P6(f74(a58),a59,a10)+~P1(a63,a56)),
% 67.28/67.26 inference(scs_inference,[],[598,18,46])).
% 67.28/67.26 cnf(2253,plain,
% 67.28/67.26 (~P1(f12(f74(a58),a59),a59)+~P1(a63,a56)),
% 67.28/67.26 inference(scs_inference,[],[598,2248,106])).
% 67.28/67.26 cnf(2258,plain,
% 67.28/67.26 (P6(a59,f74(a58),a87)+~P1(a63,a56)),
% 67.28/67.26 inference(scs_inference,[],[598,3,2253,90])).
% 67.28/67.26 cnf(2263,plain,
% 67.28/67.26 (P1(f20(a59,f74(a58)),a59)+~P1(a63,a56)),
% 67.28/67.26 inference(scs_inference,[],[2258,60])).
% 67.28/67.26 cnf(2268,plain,
% 67.28/67.26 (P6(a59,a58,a4)+~P1(a63,a56)),
% 67.28/67.26 inference(scs_inference,[],[598,2263,40])).
% 67.28/67.26 cnf(2273,plain,
% 67.28/67.26 (P1(f38(a59,a58),a59)+~P1(a63,a56)),
% 67.28/67.26 inference(scs_inference,[],[2268,65])).
% 67.28/67.26 cnf(2278,plain,
% 67.28/67.26 (P6(a58,a59,a83)+~P1(a63,a56)),
% 67.28/67.26 inference(scs_inference,[],[14,2273,41])).
% 67.28/67.26 cnf(2283,plain,
% 67.28/67.26 (P1(f33(a58,a59),a59)+~P1(a63,a56)),
% 67.28/67.26 inference(scs_inference,[],[2278,63])).
% 67.28/67.26 cnf(2284,plain,
% 67.28/67.26 (~P6(a59,a58,a75)+~P1(a63,a56)),
% 67.28/67.26 inference(scs_inference,[],[14,2283,48])).
% 67.28/67.26 cnf(2293,plain,
% 67.28/67.26 (~P2(a86,a75)+~P1(a63,a56)),
% 67.28/67.26 inference(scs_inference,[],[113,2284,94])).
% 67.28/67.26 cnf(3222,plain,
% 67.28/67.26 (P3(a85,a73)),
% 67.28/67.26 inference(scs_inference,[],[194,122,100])).
% 67.28/67.26 cnf(3223,plain,
% 67.28/67.26 (P6(x32231,a3,a73)),
% 67.28/67.26 inference(rename_variables,[],[122])).
% 67.28/67.26 cnf(3226,plain,
% 67.28/67.26 (P6(x32261,a3,a73)),
% 67.28/67.26 inference(rename_variables,[],[122])).
% 67.28/67.26 cnf(3228,plain,
% 67.28/67.26 (~P5(a85,a73)),
% 67.28/67.26 inference(scs_inference,[],[194,122,3223,3226,100,105,104])).
% 67.28/67.26 cnf(3543,plain,
% 67.28/67.26 (~P2(a73,a10)+~P6(a56,a3,a10)),
% 67.28/67.26 inference(scs_inference,[],[8,2116,44])).
% 67.28/67.26 cnf(3544,plain,
% 67.28/67.26 (~P2(a73,a10)),
% 67.28/67.26 inference(scs_inference,[],[122,3543,94])).
% 67.28/67.26 cnf(3545,plain,
% 67.28/67.26 (~P2(a73,a75)+~P6(a56,a3,a75)),
% 67.28/67.26 inference(scs_inference,[],[8,2210,45])).
% 67.28/67.26 cnf(3546,plain,
% 67.28/67.26 (~P2(a73,a75)),
% 67.28/67.26 inference(scs_inference,[],[122,3545,94])).
% 67.28/67.26 cnf(3550,plain,
% 67.28/67.26 (~P6(f74(a58),a56,a10)+~P2(a86,a75)),
% 67.28/67.26 inference(scs_inference,[],[598,2293,46])).
% 67.28/67.26 cnf(3551,plain,
% 67.28/67.26 (~P2(a86,a75)+~P1(f12(f74(a58),a56),a56)),
% 67.28/67.26 inference(scs_inference,[],[598,3550,106])).
% 67.28/67.26 cnf(3552,plain,
% 67.28/67.26 (~P6(a56,a3,a10)+~P2(a86,a75)),
% 67.28/67.26 inference(scs_inference,[],[8,3551,44])).
% 67.28/67.26 cnf(3553,plain,
% 67.28/67.26 (~P2(a86,a75)+~P1(f12(a56,a3),a56)),
% 67.28/67.26 inference(scs_inference,[],[8,2,3552,106])).
% 67.28/67.26 cnf(3554,plain,
% 67.28/67.26 (~P6(a56,a3,a75)+~P2(a86,a75)),
% 67.28/67.26 inference(scs_inference,[],[8,3553,45])).
% 67.28/67.26 cnf(3555,plain,
% 67.28/67.26 (P1(x35551,a56)+~P2(a86,a75)+~P1(f19(a56,a3),a56)),
% 67.28/67.26 inference(scs_inference,[],[8,2,3554,107])).
% 67.28/67.26 cnf(3556,plain,
% 67.28/67.26 (~P6(a3,a56,a10)+P1(x35561,a56)+~P2(a86,a75)),
% 67.28/67.26 inference(scs_inference,[],[8,3555,46])).
% 67.28/67.26 cnf(3557,plain,
% 67.28/67.26 (P1(x35571,a56)+~P2(a86,a75)+~P1(f12(a3,a56),a56)),
% 67.28/67.26 inference(scs_inference,[],[8,3556,106])).
% 67.28/67.26 cnf(3558,plain,
% 67.28/67.26 (P6(a58,a56,a89)+P1(x35581,a56)+~P2(a86,a75)),
% 67.28/67.26 inference(scs_inference,[],[14,2,3557,74])).
% 67.28/67.26 cnf(3563,plain,
% 67.28/67.26 (P1(x35631,a56)+~P2(a86,a75)+P1(f34(a58,a56),a56)),
% 67.28/67.26 inference(scs_inference,[],[3558,64])).
% 67.28/67.26 cnf(3564,plain,
% 67.28/67.26 (P1(f34(a58,a56),a56)+~P2(a86,a75)),
% 67.28/67.26 inference(factoring_inference,[],[3563])).
% 67.28/67.26 cnf(3569,plain,
% 67.28/67.26 (P6(a56,a58,a4)+~P2(a86,a75)),
% 67.28/67.26 inference(scs_inference,[],[598,3564,40])).
% 67.28/67.26 cnf(3570,plain,
% 67.28/67.26 (~P2(a86,a75)+P1(f38(a56,a58),a56)),
% 67.28/67.26 inference(scs_inference,[],[3569,65])).
% 67.28/67.26 cnf(3571,plain,
% 67.28/67.26 (P6(a58,a56,a83)+~P2(a86,a75)),
% 67.28/67.26 inference(scs_inference,[],[14,3570,41])).
% 67.28/67.26 cnf(3584,plain,
% 67.28/67.26 (~P2(a86,a75)+P1(f33(a58,a56),a56)),
% 67.28/67.26 inference(scs_inference,[],[3571,63])).
% 67.28/67.26 cnf(3588,plain,
% 67.28/67.26 (~P6(a56,a58,a75)+~P2(a86,a75)),
% 67.28/67.26 inference(scs_inference,[],[14,3584,48])).
% 67.28/67.26 cnf(3592,plain,
% 67.28/67.26 (~P2(a86,a75)),
% 67.28/67.26 inference(scs_inference,[],[113,3588,94])).
% 67.28/67.26 cnf(4127,plain,
% 67.28/67.26 (P6(a58,x41271,a5)),
% 67.28/67.26 inference(rename_variables,[],[110])).
% 67.28/67.26 cnf(4130,plain,
% 67.28/67.26 (P6(a58,x41301,a5)),
% 67.28/67.26 inference(rename_variables,[],[110])).
% 67.28/67.26 cnf(4132,plain,
% 67.28/67.26 (P3(a9,a5)),
% 67.28/67.26 inference(scs_inference,[],[740,110,4127,4130,130,91,104,105,100])).
% 67.28/67.26 cnf(4714,plain,
% 67.28/67.26 (P1(x47141,f74(f46(a88,a88)))),
% 67.28/67.26 inference(rename_variables,[],[954])).
% 67.28/67.26 cnf(4717,plain,
% 67.28/67.26 (P1(x47171,a3)),
% 67.28/67.26 inference(rename_variables,[],[8])).
% 67.28/67.26 cnf(4718,plain,
% 67.28/67.26 (P1(x47181,f74(f46(a88,a88)))),
% 67.28/67.26 inference(rename_variables,[],[954])).
% 67.28/67.26 cnf(4720,plain,
% 67.28/67.26 (P6(a3,f46(a88,a88),a88)),
% 67.28/67.26 inference(scs_inference,[],[954,4714,4718,654,8,4717,93,98,101])).
% 67.28/67.26 cnf(4772,plain,
% 67.28/67.26 (P6(f45(a5,a5),f46(a88,a88),a9)),
% 67.28/67.26 inference(scs_inference,[],[955,786,76])).
% 67.28/67.26 cnf(5119,plain,
% 67.28/67.26 (~P6(x51191,a71,a81)),
% 67.28/67.26 inference(scs_inference,[],[190,229,233,3544,12,50,51,52,69,70,99,102,27])).
% 67.28/67.26 cnf(5121,plain,
% 67.28/67.26 (~P6(a2,x51211,a83)),
% 67.28/67.26 inference(scs_inference,[],[1,190,229,233,3544,12,50,51,52,69,70,99,102,27,37])).
% 67.28/67.26 cnf(5123,plain,
% 67.28/67.26 (~P6(a2,x51231,a89)),
% 67.28/67.26 inference(scs_inference,[],[1,190,229,233,3544,12,50,51,52,69,70,99,102,27,37,39])).
% 67.28/67.26 cnf(5125,plain,
% 67.28/67.26 (~P6(x51251,a71,a87)),
% 67.28/67.26 inference(scs_inference,[],[1,190,229,233,3544,12,50,51,52,69,70,99,102,27,37,39,29])).
% 67.28/67.26 cnf(5127,plain,
% 67.28/67.26 (~P6(a71,x51271,a88)),
% 67.28/67.26 inference(scs_inference,[],[1,190,229,233,3544,12,50,51,52,69,70,99,102,27,37,39,29,32])).
% 67.28/67.26 cnf(5129,plain,
% 67.28/67.26 (~P6(a2,x51291,a85)),
% 67.28/67.26 inference(scs_inference,[],[1,190,229,233,3544,12,50,51,52,69,70,99,102,27,37,39,29,32,38])).
% 67.28/67.26 cnf(5131,plain,
% 67.28/67.26 (~P1(a1,f74(a2))),
% 67.28/67.26 inference(scs_inference,[],[1,190,229,233,3544,12,50,51,52,69,70,99,102,27,37,39,29,32,38,20])).
% 67.28/67.26 cnf(5133,plain,
% 67.28/67.26 (~P6(x51331,a71,a85)),
% 67.28/67.26 inference(scs_inference,[],[1,190,229,233,3544,12,50,51,52,69,70,99,102,27,37,39,29,32,38,20,30])).
% 67.28/67.26 cnf(5137,plain,
% 67.28/67.26 (P6(x51371,a2,a80)),
% 67.28/67.26 inference(scs_inference,[],[1,190,229,233,3544,12,50,51,52,69,70,99,102,27,37,39,29,32,38,20,30,71,22])).
% 67.28/67.26 cnf(5139,plain,
% 67.28/67.26 (~P6(a71,x51391,a84)),
% 67.28/67.26 inference(scs_inference,[],[1,190,229,233,3544,12,50,51,52,69,70,99,102,27,37,39,29,32,38,20,30,71,22,31])).
% 67.28/67.26 cnf(5141,plain,
% 67.28/67.26 (P6(a2,x51411,a86)),
% 67.28/67.26 inference(scs_inference,[],[1,190,229,233,3544,12,50,51,52,69,70,99,102,27,37,39,29,32,38,20,30,71,22,31,23])).
% 67.28/67.26 cnf(5145,plain,
% 67.28/67.26 (~P1(f39(a58,a65),a65)),
% 67.28/67.26 inference(scs_inference,[],[1,190,229,233,3544,12,1992,1321,50,51,52,69,70,99,102,27,37,39,29,32,38,20,30,71,22,31,23,54,87])).
% 67.28/67.26 cnf(5147,plain,
% 67.28/67.26 (~P6(x51471,a71,a84)),
% 67.28/67.26 inference(scs_inference,[],[1,190,229,233,3544,12,1992,1321,50,51,52,69,70,99,102,27,37,39,29,32,38,20,30,71,22,31,23,54,87,28])).
% 67.28/67.26 cnf(5149,plain,
% 67.28/67.26 (~P1(f26(a62,a3),a62)),
% 67.28/67.26 inference(scs_inference,[],[1,190,229,233,3544,12,1992,1987,1321,50,51,52,69,70,99,102,27,37,39,29,32,38,20,30,71,22,31,23,54,87,28,84])).
% 67.28/67.26 cnf(5159,plain,
% 67.28/67.26 (~P6(a2,x51591,a5)),
% 67.28/67.26 inference(scs_inference,[],[1,190,229,233,3544,12,1949,1992,1987,1321,1761,1722,50,51,52,69,70,99,102,27,37,39,29,32,38,20,30,71,22,31,23,54,87,28,84,65,56,64,25,36])).
% 67.28/67.26 cnf(5167,plain,
% 67.28/67.26 (P1(f20(a62,a3),a62)),
% 67.28/67.26 inference(scs_inference,[],[1,190,229,233,3544,10,12,1949,1774,1992,1987,1321,1761,1722,1676,50,51,52,69,70,99,102,27,37,39,29,32,38,20,30,71,22,31,23,54,87,28,84,65,56,64,25,36,24,17,21,60])).
% 67.28/67.26 cnf(5179,plain,
% 67.28/67.26 (~P2(a88,a81)),
% 67.28/67.26 inference(scs_inference,[],[1,125,190,229,233,3544,10,12,4720,1672,1363,1949,1774,1992,1987,1321,1761,1722,1734,1676,50,51,52,69,70,99,102,27,37,39,29,32,38,20,30,71,22,31,23,54,87,28,84,65,56,64,25,36,24,17,21,60,63,45,47,48,49,94])).
% 67.28/67.26 cnf(5182,plain,
% 67.28/67.26 (~P1(f14(a2,a62),a62)),
% 67.28/67.26 inference(scs_inference,[],[1,125,190,229,233,3544,10,12,4720,1672,1684,1363,1949,1774,1992,1987,1321,1761,1722,1734,1676,50,51,52,69,70,99,102,27,37,39,29,32,38,20,30,71,22,31,23,54,87,28,84,65,56,64,25,36,24,17,21,60,63,45,47,48,49,94,77])).
% 67.28/67.26 cnf(5201,plain,
% 67.28/67.26 (P6(a65,a58,a73)),
% 67.28/67.26 inference(scs_inference,[],[1,125,190,229,233,3544,10,12,4720,1672,1684,1363,1689,1949,1774,1992,1987,1321,1761,1722,1734,1505,506,1676,13,654,50,51,52,69,70,99,102,27,37,39,29,32,38,20,30,71,22,31,23,54,87,28,84,65,56,64,25,36,24,17,21,60,63,45,47,48,49,94,77,34,78,79,41,46,44,91])).
% 67.28/67.26 cnf(5203,plain,
% 67.28/67.26 (~P6(f74(a62),a62,a73)),
% 67.28/67.26 inference(scs_inference,[],[1,125,190,229,233,3544,10,12,4720,1672,1684,1363,1689,1949,1774,1992,1987,1321,1761,1722,1734,1505,506,1676,13,654,50,51,52,69,70,99,102,27,37,39,29,32,38,20,30,71,22,31,23,54,87,28,84,65,56,64,25,36,24,17,21,60,63,45,47,48,49,94,77,34,78,79,41,46,44,91,43])).
% 67.28/67.26 cnf(5206,plain,
% 67.28/67.26 (P6(f45(a5,a5),x52061,a73)),
% 67.28/67.26 inference(rename_variables,[],[820])).
% 67.28/67.26 cnf(5209,plain,
% 67.28/67.26 (P6(f45(a5,a5),x52091,a73)),
% 67.28/67.26 inference(rename_variables,[],[820])).
% 67.28/67.26 cnf(5214,plain,
% 67.28/67.26 (~P1(f23(a62,a3),a62)),
% 67.28/67.26 inference(scs_inference,[],[1,125,190,229,233,3544,10,12,4720,4772,1672,1684,1363,820,5206,5209,1689,1949,1774,1992,1987,1321,1761,1722,1734,1729,1505,506,1676,13,654,8,50,51,52,69,70,99,102,27,37,39,29,32,38,20,30,71,22,31,23,54,87,28,84,65,56,64,25,36,24,17,21,60,63,45,47,48,49,94,77,34,78,79,41,46,44,91,43,100,105,104,98])).
% 67.28/67.26 cnf(5215,plain,
% 67.28/67.26 (P1(x52151,a3)),
% 67.28/67.26 inference(rename_variables,[],[8])).
% 67.28/67.26 cnf(5218,plain,
% 67.28/67.26 (P6(a2,a2,a9)),
% 67.28/67.26 inference(scs_inference,[],[1,125,190,229,233,3544,10,12,4720,4772,1672,1684,1363,820,5206,5209,1689,1949,1774,1992,1987,1321,1761,1722,1734,1729,1505,506,1676,13,654,8,50,51,52,69,70,99,102,27,37,39,29,32,38,20,30,71,22,31,23,54,87,28,84,65,56,64,25,36,24,17,21,60,63,45,47,48,49,94,77,34,78,79,41,46,44,91,43,100,105,104,98,33])).
% 67.28/67.26 cnf(5221,plain,
% 67.28/67.26 (P1(x52211,a3)),
% 67.28/67.26 inference(rename_variables,[],[8])).
% 67.28/67.26 cnf(5224,plain,
% 67.28/67.26 (~P1(f40(a62,a58),a62)),
% 67.28/67.26 inference(scs_inference,[],[1,125,190,229,233,3544,10,12,4720,4772,1672,1684,1363,820,5206,5209,1689,1741,1949,1774,1992,1987,1321,1761,1722,1734,1729,1698,1505,506,1676,13,654,8,5215,598,50,51,52,69,70,99,102,27,37,39,29,32,38,20,30,71,22,31,23,54,87,28,84,65,56,64,25,36,24,17,21,60,63,45,47,48,49,94,77,34,78,79,41,46,44,91,43,100,105,104,98,33,93,101])).
% 67.28/67.26 cnf(5228,plain,
% 67.28/67.26 (P1(f60(a69,a58),a69)),
% 67.28/67.26 inference(scs_inference,[],[1,125,190,229,233,3544,10,12,4720,4772,1672,1684,1363,591,820,5206,5209,1689,1741,1949,1774,1992,1987,1321,1761,1722,1734,1729,1698,1505,506,1676,13,654,8,5215,14,598,50,51,52,69,70,99,102,27,37,39,29,32,38,20,30,71,22,31,23,54,87,28,84,65,56,64,25,36,24,17,21,60,63,45,47,48,49,94,77,34,78,79,41,46,44,91,43,100,105,104,98,33,93,101,76])).
% 67.28/67.26 cnf(5231,plain,
% 67.28/67.26 (~P1(f22(a2,a62),a62)),
% 67.28/67.26 inference(scs_inference,[],[1,125,190,229,233,3544,10,12,4720,4772,1672,1684,1707,1363,591,820,5206,5209,1689,1741,1949,1774,1992,1987,9,1321,1761,1722,1734,1729,1698,1505,506,1676,13,654,8,5215,14,598,50,51,52,69,70,99,102,27,37,39,29,32,38,20,30,71,22,31,23,54,87,28,84,65,56,64,25,36,24,17,21,60,63,45,47,48,49,94,77,34,78,79,41,46,44,91,43,100,105,104,98,33,93,101,76,90])).
% 67.28/67.26 cnf(5237,plain,
% 67.28/67.26 (~P1(f12(a3,a62),a62)),
% 67.28/67.26 inference(scs_inference,[],[1,125,190,229,233,3544,10,12,4720,4772,1672,1684,1707,1363,591,820,5206,5209,1689,1708,1741,1949,1774,1992,1987,9,1321,1761,1782,1722,1734,1729,1698,1505,506,1676,13,654,8,5215,5221,14,598,50,51,52,69,70,99,102,27,37,39,29,32,38,20,30,71,22,31,23,54,87,28,84,65,56,64,25,36,24,17,21,60,63,45,47,48,49,94,77,34,78,79,41,46,44,91,43,100,105,104,98,33,93,101,76,90,74,106])).
% 67.28/67.26 cnf(5238,plain,
% 67.28/67.26 (P1(x52381,a3)),
% 67.28/67.26 inference(rename_variables,[],[8])).
% 67.28/67.26 cnf(5239,plain,
% 67.28/67.26 (P1(x52391,a3)),
% 67.28/67.26 inference(rename_variables,[],[8])).
% 67.28/67.26 cnf(5241,plain,
% 67.28/67.26 (P1(f76(a2,a2),a2)),
% 67.28/67.26 inference(scs_inference,[],[1,125,190,229,233,3544,10,12,4720,4772,1672,1684,1707,1363,591,820,5206,5209,1689,1708,1741,1949,1774,1992,1987,9,1321,1761,1782,1722,1734,1729,1698,1505,506,1676,13,654,8,5215,5221,14,598,50,51,52,69,70,99,102,27,37,39,29,32,38,20,30,71,22,31,23,54,87,28,84,65,56,64,25,36,24,17,21,60,63,45,47,48,49,94,77,34,78,79,41,46,44,91,43,100,105,104,98,33,93,101,76,90,74,106,53])).
% 67.28/67.26 cnf(5243,plain,
% 67.28/67.26 (P1(f78(a2,a2),a2)),
% 67.28/67.26 inference(scs_inference,[],[1,125,190,229,233,3544,10,12,4720,4772,1672,1684,1707,1363,591,820,5206,5209,1689,1708,1741,1949,1774,1992,1987,9,1321,1761,1782,1722,1734,1729,1698,1505,506,1676,13,654,8,5215,5221,14,598,50,51,52,69,70,99,102,27,37,39,29,32,38,20,30,71,22,31,23,54,87,28,84,65,56,64,25,36,24,17,21,60,63,45,47,48,49,94,77,34,78,79,41,46,44,91,43,100,105,104,98,33,93,101,76,90,74,106,53,81])).
% 67.28/67.26 cnf(5247,plain,
% 67.28/67.26 (P6(a2,a3,a90)),
% 67.28/67.26 inference(scs_inference,[],[1,125,190,229,233,3544,10,12,4720,4772,1672,1684,1707,1363,591,820,5206,5209,1689,1708,1741,1949,1774,1992,1987,9,1321,1761,1782,1722,1734,1729,1698,1505,506,1676,13,654,8,5215,5221,5239,5238,14,598,50,51,52,69,70,99,102,27,37,39,29,32,38,20,30,71,22,31,23,54,87,28,84,65,56,64,25,36,24,17,21,60,63,45,47,48,49,94,77,34,78,79,41,46,44,91,43,100,105,104,98,33,93,101,76,90,74,106,53,81,80,97])).
% 67.28/67.26 cnf(5253,plain,
% 67.28/67.26 (P1(f15(a2,a3),a2)),
% 67.28/67.26 inference(scs_inference,[],[1,125,190,229,233,3544,10,12,4720,4772,1672,1684,1707,1363,591,820,5206,5209,1689,1708,1741,1949,1774,1992,1987,9,1321,1761,1782,5,1722,1734,1729,1698,1505,506,1676,13,4,654,8,5215,5221,5239,5238,14,598,50,51,52,69,70,99,102,27,37,39,29,32,38,20,30,71,22,31,23,54,87,28,84,65,56,64,25,36,24,17,21,60,63,45,47,48,49,94,77,34,78,79,41,46,44,91,43,100,105,104,98,33,93,101,76,90,74,106,53,81,80,97,88,57])).
% 67.28/67.26 cnf(5255,plain,
% 67.28/67.26 (~P1(f17(a2,a3),a2)),
% 67.28/67.26 inference(scs_inference,[],[1,125,190,229,233,3544,10,12,4720,4772,1672,1684,1707,1363,591,820,5206,5209,1689,1708,1741,1949,1774,1992,1987,9,1321,1761,1782,5,1722,1734,1729,1698,1505,506,1676,13,4,654,8,5215,5221,5239,5238,14,598,50,51,52,69,70,99,102,27,37,39,29,32,38,20,30,71,22,31,23,54,87,28,84,65,56,64,25,36,24,17,21,60,63,45,47,48,49,94,77,34,78,79,41,46,44,91,43,100,105,104,98,33,93,101,76,90,74,106,53,81,80,97,88,57,82])).
% 67.28/67.26 cnf(5263,plain,
% 67.28/67.26 (~P6(a62,x52631,a85)),
% 67.28/67.26 inference(scs_inference,[],[248,5167,102,38])).
% 67.28/67.26 cnf(5265,plain,
% 67.28/67.26 (~P6(a62,x52651,a89)),
% 67.28/67.26 inference(scs_inference,[],[248,5167,102,38,39])).
% 67.28/67.26 cnf(5285,plain,
% 67.28/67.26 (~P6(a62,x52851,a83)),
% 67.28/67.26 inference(scs_inference,[],[248,278,288,301,307,3546,5131,5167,102,38,39,32,27,29,69,50,52,99,51,70,37])).
% 67.28/67.26 cnf(5287,plain,
% 67.28/67.26 (~P1(f60(a62,a58),f74(a65))),
% 67.28/67.26 inference(scs_inference,[],[248,278,288,301,307,3546,1770,5131,5167,102,38,39,32,27,29,69,50,52,99,51,70,37,20])).
% 67.28/67.26 cnf(5291,plain,
% 67.28/67.26 (P6(x52911,a62,a80)),
% 67.28/67.26 inference(scs_inference,[],[248,278,288,301,307,3546,1770,5131,5167,102,38,39,32,27,29,69,50,52,99,51,70,37,20,30,22])).
% 67.28/67.26 cnf(5297,plain,
% 67.28/67.26 (P6(a62,x52971,a86)),
% 67.28/67.26 inference(scs_inference,[],[248,278,288,301,307,3546,1770,5131,5167,102,38,39,32,27,29,69,50,52,99,51,70,37,20,30,22,71,31,23])).
% 67.28/67.26 cnf(5299,plain,
% 67.28/67.26 (~P1(f39(a58,a62),a62)),
% 67.28/67.26 inference(scs_inference,[],[248,278,288,301,307,3546,1770,5131,5167,1966,102,38,39,32,27,29,69,50,52,99,51,70,37,20,30,22,71,31,23,87])).
% 67.28/67.26 cnf(5303,plain,
% 67.28/67.26 (~P1(f26(a65,a3),a65)),
% 67.28/67.26 inference(scs_inference,[],[248,278,288,301,307,3546,1770,5131,5167,1961,1966,102,38,39,32,27,29,69,50,52,99,51,70,37,20,30,22,71,31,23,87,28,84])).
% 67.28/67.26 cnf(5305,plain,
% 67.28/67.26 (P1(f34(a58,a62),a62)),
% 67.28/67.26 inference(scs_inference,[],[248,278,288,301,307,3546,1770,5131,5167,1961,1966,102,38,39,32,27,29,69,50,52,99,51,70,37,20,30,22,71,31,23,87,28,84,64])).
% 67.28/67.26 cnf(5307,plain,
% 67.28/67.26 (~P6(a62,x53071,a5)),
% 67.28/67.26 inference(scs_inference,[],[248,278,288,301,307,3546,1770,5131,5167,1961,1966,102,38,39,32,27,29,69,50,52,99,51,70,37,20,30,22,71,31,23,87,28,84,64,36])).
% 67.28/67.26 cnf(5309,plain,
% 67.28/67.26 (P1(f24(a3,a62),f74(a62))),
% 67.28/67.26 inference(scs_inference,[],[248,278,288,301,307,3546,1695,1770,5131,5167,1961,1966,102,38,39,32,27,29,69,50,52,99,51,70,37,20,30,22,71,31,23,87,28,84,64,36,17])).
% 67.28/67.26 cnf(5311,plain,
% 67.28/67.26 (P1(f6(a2),a2)),
% 67.28/67.26 inference(scs_inference,[],[248,278,288,301,307,3546,5159,1695,1770,5131,5167,1961,1966,102,38,39,32,27,29,69,50,52,99,51,70,37,20,30,22,71,31,23,87,28,84,64,36,17,21])).
% 67.28/67.26 cnf(5315,plain,
% 67.28/67.26 (~P2(a86,a81)),
% 67.28/67.26 inference(scs_inference,[],[248,278,288,301,307,3546,5119,5141,5159,1695,1770,5131,5167,1961,1966,102,38,39,32,27,29,69,50,52,99,51,70,37,20,30,22,71,31,23,87,28,84,64,36,17,21,60,94])).
% 67.28/67.26 cnf(5316,plain,
% 67.28/67.26 (~P6(x53161,a71,a81)),
% 67.28/67.26 inference(rename_variables,[],[5119])).
% 67.28/67.26 cnf(5317,plain,
% 67.28/67.26 (P6(a2,x53171,a86)),
% 67.28/67.26 inference(rename_variables,[],[5141])).
% 67.28/67.26 cnf(5326,plain,
% 67.28/67.26 (~P1(f14(a2,a71),a71)),
% 67.28/67.26 inference(scs_inference,[],[1,248,278,288,301,307,3546,5119,5316,5141,5317,5159,1695,1770,5131,5167,1961,1966,102,38,39,32,27,29,69,50,52,99,51,70,37,20,30,22,71,31,23,87,28,84,64,36,17,21,60,94,45,78,47,77])).
% 67.28/67.26 cnf(5345,plain,
% 67.28/67.26 (~P1(x53451,f48(a5,a5))),
% 67.28/67.26 inference(rename_variables,[],[654])).
% 67.28/67.26 cnf(5354,plain,
% 67.28/67.26 (P6(a65,a65,a9)),
% 67.28/67.26 inference(scs_inference,[],[1,248,278,288,301,307,3546,5119,5316,5121,5137,5141,5317,5159,1695,1770,5131,5167,1961,1966,654,5345,664,102,38,39,32,27,29,69,50,52,99,51,70,37,20,30,22,71,31,23,87,28,84,64,36,17,21,60,94,45,78,47,77,34,49,79,41,48,46,81,80,44,43,33])).
% 67.28/67.26 cnf(5356,plain,
% 67.28/67.26 (~P1(f40(a71,a58),a71)),
% 67.28/67.26 inference(scs_inference,[],[1,248,278,288,301,307,3546,5119,5316,5121,5127,5137,5141,5317,5159,1695,1770,5131,5167,1961,1966,654,5345,664,598,102,38,39,32,27,29,69,50,52,99,51,70,37,20,30,22,71,31,23,87,28,84,64,36,17,21,60,94,45,78,47,77,34,49,79,41,48,46,81,80,44,43,33,101])).
% 67.28/67.26 cnf(5360,plain,
% 67.28/67.26 (P1(f60(a59,a58),a59)),
% 67.28/67.26 inference(scs_inference,[],[1,248,278,288,301,307,3546,5119,5316,5121,5127,5137,5141,5317,5159,1695,1770,5131,5167,547,1961,1966,654,5345,664,14,598,102,38,39,32,27,29,69,50,52,99,51,70,37,20,30,22,71,31,23,87,28,84,64,36,17,21,60,94,45,78,47,77,34,49,79,41,48,46,81,80,44,43,33,101,76])).
% 67.28/67.26 cnf(5363,plain,
% 67.28/67.26 (~P1(f22(a2,a71),a71)),
% 67.28/67.27 inference(scs_inference,[],[1,248,278,288,301,307,3546,5119,5316,5121,5125,5127,5137,5141,5317,5159,1695,1770,5131,5167,5255,547,1961,1966,654,5345,664,14,598,102,38,39,32,27,29,69,50,52,99,51,70,37,20,30,22,71,31,23,87,28,84,64,36,17,21,60,94,45,78,47,77,34,49,79,41,48,46,81,80,44,43,33,101,76,90])).
% 67.28/67.27 cnf(5366,plain,
% 67.28/67.27 (P1(f35(a2,a2),a2)),
% 67.28/67.27 inference(scs_inference,[],[1,248,278,288,301,307,3546,5119,5316,5121,5123,5125,5127,5137,5141,5317,5159,1695,1770,5131,5167,5255,547,1961,1966,654,5345,664,14,598,102,38,39,32,27,29,69,50,52,99,51,70,37,20,30,22,71,31,23,87,28,84,64,36,17,21,60,94,45,78,47,77,34,49,79,41,48,46,81,80,44,43,33,101,76,90,74])).
% 67.28/67.27 cnf(5378,plain,
% 67.28/67.27 (~P6(f74(a62),x53781,a89)),
% 67.28/67.27 inference(scs_inference,[],[283,320,3592,5309,69,102,99,39])).
% 67.28/67.27 cnf(5380,plain,
% 67.28/67.27 (~P6(a65,x53801,a88)),
% 67.28/67.27 inference(scs_inference,[],[283,320,3592,5309,5145,69,102,99,39,32])).
% 67.28/67.27 cnf(5398,plain,
% 67.28/67.27 (~P1(f19(a65,a58),f74(a65))),
% 67.28/67.27 inference(scs_inference,[],[283,320,323,3592,2012,5309,5287,5145,69,102,99,39,32,38,50,70,37,29,51,27,52,20])).
% 67.28/67.27 cnf(5408,plain,
% 67.28/67.27 (P6(f74(a62),x54081,a86)),
% 67.28/67.27 inference(scs_inference,[],[283,320,323,3592,2012,5309,5287,5145,69,102,99,39,32,38,50,70,37,29,51,27,52,20,30,71,22,31,23])).
% 67.28/67.27 cnf(5414,plain,
% 67.28/67.27 (P1(f26(a65,a3),f74(a62))),
% 67.28/67.27 inference(scs_inference,[],[283,320,323,3592,2012,1973,5309,5287,5145,69,102,99,39,32,38,50,70,37,29,51,27,52,20,30,71,22,31,23,28,36,17])).
% 67.28/67.27 cnf(5416,plain,
% 67.28/67.27 (P1(f6(a62),a62)),
% 67.28/67.27 inference(scs_inference,[],[283,320,323,3592,5307,2012,1973,5309,5287,5145,69,102,99,39,32,38,50,70,37,29,51,27,52,20,30,71,22,31,23,28,36,17,21])).
% 67.28/67.27 cnf(5419,plain,
% 67.28/67.27 (P1(x54191,f48(a84,a84))),
% 67.28/67.27 inference(rename_variables,[],[664])).
% 67.28/67.27 cnf(5421,plain,
% 67.28/67.27 (~P2(a9,a85)),
% 67.28/67.27 inference(scs_inference,[],[283,320,323,5218,3592,5129,5307,2012,1973,5309,5287,5145,664,69,102,99,39,32,38,50,70,37,29,51,27,52,20,30,71,22,31,23,28,36,17,21,45,94])).
% 67.28/67.27 cnf(5424,plain,
% 67.28/67.27 (P6(f74(a62),f74(a62),a82)),
% 67.28/67.27 inference(scs_inference,[],[283,320,323,5218,3592,5129,5307,2012,1973,5309,5287,5145,664,69,102,99,39,32,38,50,70,37,29,51,27,52,20,30,71,22,31,23,28,36,17,21,45,94,34])).
% 67.28/67.27 cnf(5426,plain,
% 67.28/67.27 (~P6(a69,a71,a91)),
% 67.28/67.27 inference(scs_inference,[],[283,320,323,5218,3592,5129,5307,2012,1973,5309,5287,5145,6,12,664,69,102,99,39,32,38,50,70,37,29,51,27,52,20,30,71,22,31,23,28,36,17,21,45,94,34,49])).
% 67.28/67.27 cnf(5428,plain,
% 67.28/67.27 (P1(f52(a2,a62),a62)),
% 67.28/67.27 inference(scs_inference,[],[1,283,320,323,5218,3592,5129,5291,5307,2012,1973,5309,5287,5145,6,12,664,69,102,99,39,32,38,50,70,37,29,51,27,52,20,30,71,22,31,23,28,36,17,21,45,94,34,49,79])).
% 67.28/67.27 cnf(5431,plain,
% 67.28/67.27 (P1(f29(a62,a2),a62)),
% 67.28/67.27 inference(scs_inference,[],[1,283,320,323,5218,3592,5129,5291,5297,5307,2012,1973,5309,5287,5145,6,12,664,69,102,99,39,32,38,50,70,37,29,51,27,52,20,30,71,22,31,23,28,36,17,21,45,94,34,49,79,78])).
% 67.28/67.27 cnf(5434,plain,
% 67.28/67.27 (~P6(a69,a71,a90)),
% 67.28/67.27 inference(scs_inference,[],[1,283,320,323,5218,3592,5129,5291,5297,5307,2012,1973,5309,5287,5145,6,12,664,69,102,99,39,32,38,50,70,37,29,51,27,52,20,30,71,22,31,23,28,36,17,21,45,94,34,49,79,78,47])).
% 67.28/67.27 cnf(5438,plain,
% 67.28/67.27 (P1(f32(a62,a2),a62)),
% 67.28/67.27 inference(scs_inference,[],[1,283,320,323,5218,3592,5129,5285,5291,5297,5307,2012,1973,5309,5287,5145,1770,6,12,664,69,102,99,39,32,38,50,70,37,29,51,27,52,20,30,71,22,31,23,28,36,17,21,45,94,34,49,79,78,47,48,41])).
% 67.28/67.27 cnf(5457,plain,
% 67.28/67.27 (P1(f35(a62,a62),a62)),
% 67.28/67.27 inference(scs_inference,[],[1,283,320,323,5218,3592,5129,5265,5285,5291,5297,5307,5354,2012,1973,5309,5287,5145,5305,241,461,460,1770,6,12,5131,664,5419,14,69,102,99,39,32,38,50,70,37,29,51,27,52,20,30,71,22,31,23,28,36,17,21,45,94,34,49,79,78,47,48,41,46,81,44,80,43,33,76,74])).
% 67.28/67.27 cnf(5462,plain,
% 67.28/67.27 (~P1(f40(a65,a58),a65)),
% 67.28/67.27 inference(scs_inference,[],[1,283,320,323,5218,3592,5129,5265,5285,5291,5297,5307,5354,2012,1973,5309,5287,5145,5305,241,461,460,1770,6,12,5131,664,5419,14,598,69,102,99,39,32,38,50,70,37,29,51,27,52,20,30,71,22,31,23,28,36,17,21,45,94,34,49,79,78,47,48,41,46,81,44,80,43,33,76,74,15,101])).
% 67.28/67.27 cnf(5475,plain,
% 67.28/67.27 (~P6(x54751,a65,a87)),
% 67.28/67.27 inference(scs_inference,[],[332,602,5303,5428,15,50,69,29])).
% 67.28/67.27 cnf(5479,plain,
% 67.28/67.27 (~P6(a59,x54791,a89)),
% 67.28/67.27 inference(scs_inference,[],[304,332,602,5303,5360,5428,15,50,69,29,102,39])).
% 67.28/67.27 cnf(5485,plain,
% 67.28/67.27 (~P6(x54851,a65,a81)),
% 67.28/67.27 inference(scs_inference,[],[304,332,347,602,5303,5360,5428,15,50,69,29,102,39,70,99,27])).
% 67.28/67.27 cnf(5487,plain,
% 67.28/67.27 (~P6(a59,x54871,a85)),
% 67.28/67.27 inference(scs_inference,[],[304,332,347,602,5303,5360,5428,15,50,69,29,102,39,70,99,27,38])).
% 67.28/67.27 cnf(5491,plain,
% 67.28/67.27 (~P6(a2,x54911,a88)),
% 67.28/67.27 inference(scs_inference,[],[304,332,347,349,602,5303,5360,5428,5255,15,50,69,29,102,39,70,99,27,38,51,32])).
% 67.28/67.27 cnf(5495,plain,
% 67.28/67.27 (~P6(a59,x54951,a83)),
% 67.28/67.27 inference(scs_inference,[],[304,332,347,349,513,602,5303,5360,5428,5255,15,50,69,29,102,39,70,99,27,38,51,32,52,37])).
% 67.28/67.27 cnf(5501,plain,
% 67.28/67.27 (P6(x55011,a59,a80)),
% 67.28/67.27 inference(scs_inference,[],[304,332,347,349,513,602,5241,5303,5360,5428,5255,15,50,69,29,102,39,70,99,27,38,51,32,52,37,30,20,22])).
% 67.28/67.27 cnf(5505,plain,
% 67.28/67.27 (~P6(a65,x55051,a84)),
% 67.28/67.27 inference(scs_inference,[],[304,332,347,349,513,602,5241,5303,5360,5428,5255,15,50,69,29,102,39,70,99,27,38,51,32,52,37,30,20,22,71,31])).
% 67.28/67.27 cnf(5507,plain,
% 67.28/67.27 (P6(a59,x55071,a86)),
% 67.28/67.27 inference(scs_inference,[],[304,332,347,349,513,602,5241,5303,5360,5428,5255,15,50,69,29,102,39,70,99,27,38,51,32,52,37,30,20,22,71,31,23])).
% 67.28/67.27 cnf(5513,plain,
% 67.28/67.27 (P1(f6(a59),a59)),
% 67.28/67.27 inference(scs_inference,[],[304,332,347,349,513,602,5241,5303,5360,5428,5255,15,50,69,29,102,39,70,99,27,38,51,32,52,37,30,20,22,71,31,23,28,36,21])).
% 67.28/67.27 cnf(5519,plain,
% 67.28/67.27 (~P1(f14(a2,a65),a65)),
% 67.28/67.27 inference(scs_inference,[],[1,304,332,347,349,513,602,5241,5237,5303,5414,5360,5428,5255,15,50,69,29,102,39,70,99,27,38,51,32,52,37,30,20,22,71,31,23,28,36,21,17,49,77])).
% 67.28/67.27 cnf(5523,plain,
% 67.28/67.27 (~P2(a86,a85)),
% 67.28/67.27 inference(scs_inference,[],[1,304,332,347,349,513,5133,602,5241,5237,5303,5414,5408,5360,5428,5255,15,50,69,29,102,39,70,99,27,38,51,32,52,37,30,20,22,71,31,23,28,36,21,17,49,77,45,94])).
% 67.28/67.27 cnf(5524,plain,
% 67.28/67.27 (~P6(x55241,a71,a85)),
% 67.28/67.27 inference(rename_variables,[],[5133])).
% 67.28/67.27 cnf(5532,plain,
% 67.28/67.27 (~P1(x55321,f48(a5,a5))),
% 67.28/67.27 inference(rename_variables,[],[654])).
% 67.28/67.27 cnf(5534,plain,
% 67.28/67.27 (P1(f32(a59,a2),a59)),
% 67.28/67.27 inference(scs_inference,[],[1,304,332,347,349,513,5133,602,5241,5237,5303,5414,5408,5360,5428,5255,654,15,50,69,29,102,39,70,99,27,38,51,32,52,37,30,20,22,71,31,23,28,36,21,17,49,77,45,94,34,47,48,41])).
% 67.28/67.27 cnf(5537,plain,
% 67.28/67.27 (P1(x55371,f48(a84,a84))),
% 67.28/67.27 inference(rename_variables,[],[664])).
% 67.28/67.27 cnf(5540,plain,
% 67.28/67.27 (~P1(x55401,f48(a5,a5))),
% 67.28/67.27 inference(rename_variables,[],[654])).
% 67.28/67.27 cnf(5546,plain,
% 67.28/67.27 (~P1(x55461,f48(a5,a5))),
% 67.28/67.27 inference(rename_variables,[],[654])).
% 67.28/67.27 cnf(5558,plain,
% 67.28/67.27 (P6(a59,a59,a9)),
% 67.28/67.27 inference(scs_inference,[],[1,304,332,347,349,513,5133,5524,5139,602,5241,5237,5326,5303,5414,5378,5408,5424,5360,5428,5255,654,5532,5540,5546,664,5537,15,50,69,29,102,39,70,99,27,38,51,32,52,37,30,20,22,71,31,23,28,36,21,17,49,77,45,94,34,47,48,41,46,81,44,80,91,43,75,33])).
% 67.28/67.27 cnf(5563,plain,
% 67.28/67.27 (P1(f35(a62,a2),a62)),
% 67.28/67.27 inference(scs_inference,[],[1,304,332,347,349,513,5133,5524,5139,602,5241,5237,5326,5303,5414,5378,5408,5424,5360,5428,550,5265,5255,654,5532,5540,5546,664,5537,14,15,50,69,29,102,39,70,99,27,38,51,32,52,37,30,20,22,71,31,23,28,36,21,17,49,77,45,94,34,47,48,41,46,81,44,80,91,43,75,33,76,74])).
% 67.28/67.27 cnf(5566,plain,
% 67.28/67.27 (P1(f76(a59,a59),a59)),
% 67.28/67.27 inference(scs_inference,[],[1,304,332,347,349,513,5133,5524,5139,602,5241,5237,5326,5303,5414,5378,5408,5424,5360,5428,550,5265,5255,654,5532,5540,5546,664,5537,14,15,50,69,29,102,39,70,99,27,38,51,32,52,37,30,20,22,71,31,23,28,36,21,17,49,77,45,94,34,47,48,41,46,81,44,80,91,43,75,33,76,74,54])).
% 67.28/67.27 cnf(5570,plain,
% 67.28/67.27 (~P1(f22(a62,a71),a71)),
% 67.28/67.27 inference(scs_inference,[],[1,304,332,347,349,513,5133,5524,5139,602,5434,5241,5237,5326,5303,5414,5378,5408,5424,5360,5416,5428,550,5125,5265,5228,7,5255,654,5532,5540,5546,664,5537,14,15,50,69,29,102,39,70,99,27,38,51,32,52,37,30,20,22,71,31,23,28,36,21,17,49,77,45,94,34,47,48,41,46,81,44,80,91,43,75,33,76,74,54,88,90])).
% 67.28/67.27 cnf(5575,plain,
% 67.28/67.27 (P1(f32(a62,a2),a65)),
% 67.28/67.27 inference(scs_inference,[],[5438,15])).
% 67.28/67.27 cnf(5587,plain,
% 67.28/67.27 (~P6(x55871,a2,a87)),
% 67.28/67.27 inference(scs_inference,[],[509,523,531,1632,5438,5228,5255,15,70,38,50,69,52,29])).
% 67.28/67.27 cnf(5595,plain,
% 67.28/67.27 (~P6(a69,x55951,a89)),
% 67.28/67.27 inference(scs_inference,[],[509,523,531,1632,5438,5228,5255,654,15,70,38,50,69,52,29,99,32,51,39])).
% 67.28/67.27 cnf(5599,plain,
% 67.28/67.27 (~P6(x55991,a2,a81)),
% 67.28/67.27 inference(scs_inference,[],[313,509,523,531,1632,5438,5228,5255,654,15,70,38,50,69,52,29,99,32,51,39,102,27])).
% 67.28/67.27 cnf(5601,plain,
% 67.28/67.27 (~P6(a69,x56011,a83)),
% 67.28/67.27 inference(scs_inference,[],[313,509,523,531,1632,5438,5228,5255,654,15,70,38,50,69,52,29,99,32,51,39,102,27,37])).
% 67.28/67.27 cnf(5607,plain,
% 67.28/67.27 (P6(x56071,a69,a80)),
% 67.28/67.27 inference(scs_inference,[],[313,509,523,531,1632,5243,5438,5228,5255,654,15,70,38,50,69,52,29,99,32,51,39,102,27,37,30,20,22])).
% 67.28/67.27 cnf(5613,plain,
% 67.28/67.27 (P6(a69,x56131,a86)),
% 67.28/67.27 inference(scs_inference,[],[313,509,523,531,1632,5243,5438,5228,5255,654,15,70,38,50,69,52,29,99,32,51,39,102,27,37,30,20,22,71,31,23])).
% 67.28/67.27 cnf(5619,plain,
% 67.28/67.27 (P1(f6(a69),a69)),
% 67.28/67.27 inference(scs_inference,[],[313,509,523,531,1632,5243,5438,5228,5255,654,15,70,38,50,69,52,29,99,32,51,39,102,27,37,30,20,22,71,31,23,28,36,21])).
% 67.28/67.27 cnf(5630,plain,
% 67.28/67.27 (P1(x56301,f48(a84,a84))),
% 67.28/67.27 inference(rename_variables,[],[664])).
% 67.28/67.27 cnf(5632,plain,
% 67.28/67.27 (~P1(f14(a59,a65),a65)),
% 67.28/67.27 inference(scs_inference,[],[1,313,509,523,531,5485,5501,5507,1632,5243,5149,5462,5566,5438,5228,5255,654,664,15,70,38,50,69,52,29,99,32,51,39,102,27,37,30,20,22,71,31,23,28,36,21,17,78,79,45,77])).
% 67.28/67.27 cnf(5637,plain,
% 67.28/67.27 (~P2(a73,a88)),
% 67.28/67.27 inference(scs_inference,[],[1,313,509,523,531,5201,5380,5485,5501,5507,1632,5243,5149,5462,5566,5438,5228,5255,654,664,15,70,38,50,69,52,29,99,32,51,39,102,27,37,30,20,22,71,31,23,28,36,21,17,78,79,45,77,34,94])).
% 67.28/67.27 cnf(5657,plain,
% 67.28/67.27 (P6(a62,a62,a9)),
% 67.28/67.27 inference(scs_inference,[],[1,313,509,523,531,5201,5380,5485,5495,5501,5507,1632,5558,5243,5149,5462,5566,5438,10,5228,5255,5,6,12,654,664,5630,15,70,38,50,69,52,29,99,32,51,39,102,27,37,30,20,22,71,31,23,28,36,21,17,78,79,45,77,34,94,48,41,46,81,44,80,43,33])).
% 67.28/67.27 cnf(5659,plain,
% 67.28/67.27 (P1(f60(a56,a58),a56)),
% 67.28/67.27 inference(scs_inference,[],[1,313,509,523,531,5201,5380,5485,5495,5501,5507,1632,5558,5243,5149,5462,5566,5438,280,10,5228,5255,5,6,12,654,664,5630,14,15,70,38,50,69,52,29,99,32,51,39,102,27,37,30,20,22,71,31,23,28,36,21,17,78,79,45,77,34,94,48,41,46,81,44,80,43,33,76])).
% 67.28/67.27 cnf(5668,plain,
% 67.28/67.27 (P1(f76(a62,a62),a62)),
% 67.28/67.27 inference(scs_inference,[],[1,313,509,523,531,5201,5380,5475,5479,5485,5495,5501,5507,1632,5558,5243,5149,5462,5566,5438,280,10,5228,5255,5,6,12,654,664,5630,14,15,70,38,50,69,52,29,99,32,51,39,102,27,37,30,20,22,71,31,23,28,36,21,17,78,79,45,77,34,94,48,41,46,81,44,80,43,33,76,90,74,54])).
% 67.28/67.27 cnf(5697,plain,
% 67.28/67.27 (~P6(a56,x56971,a85)),
% 67.28/67.27 inference(scs_inference,[],[632,759,5637,5668,5659,654,29,15,51,70,50,99,38])).
% 67.28/67.27 cnf(5703,plain,
% 67.28/67.27 (~P6(a56,x57031,a89)),
% 67.28/67.27 inference(scs_inference,[],[326,632,759,761,5637,5668,5659,654,29,15,51,70,50,99,38,102,52,39])).
% 67.28/67.27 cnf(5711,plain,
% 67.28/67.27 (~P6(a56,x57111,a83)),
% 67.28/67.27 inference(scs_inference,[],[326,632,759,761,1036,5637,5668,5659,654,786,29,15,51,70,50,99,38,102,52,39,69,27,32,37])).
% 67.28/67.27 cnf(5717,plain,
% 67.28/67.27 (P6(x57171,a56,a80)),
% 67.28/67.27 inference(scs_inference,[],[326,632,759,761,1036,5637,5253,5668,5659,654,786,29,15,51,70,50,99,38,102,52,39,69,27,32,37,30,20,22])).
% 67.28/67.27 cnf(5723,plain,
% 67.28/67.27 (P6(a56,x57231,a86)),
% 67.28/67.27 inference(scs_inference,[],[326,632,759,761,1036,5637,5253,5668,5659,654,786,29,15,51,70,50,99,38,102,52,39,69,27,32,37,30,20,22,71,31,23])).
% 67.28/67.27 cnf(5727,plain,
% 67.28/67.27 (~P6(a56,x57271,a5)),
% 67.28/67.27 inference(scs_inference,[],[326,632,759,761,1036,5637,5253,5668,5659,654,786,29,15,51,70,50,99,38,102,52,39,69,27,32,37,30,20,22,71,31,23,28,36])).
% 67.28/67.27 cnf(5729,plain,
% 67.28/67.27 (P1(f6(a56),a56)),
% 67.28/67.27 inference(scs_inference,[],[326,632,759,761,1036,5637,5253,5668,5659,654,786,29,15,51,70,50,99,38,102,52,39,69,27,32,37,30,20,22,71,31,23,28,36,21])).
% 67.28/67.27 cnf(5736,plain,
% 67.28/67.27 (P6(a69,x57361,a86)),
% 67.28/67.27 inference(rename_variables,[],[5613])).
% 67.28/67.27 cnf(5738,plain,
% 67.28/67.27 (P1(f52(a2,a69),a69)),
% 67.28/67.27 inference(scs_inference,[],[1,326,632,759,761,1036,5637,5607,5613,5253,5299,5668,5659,507,465,654,786,29,15,51,70,50,99,38,102,52,39,69,27,32,37,30,20,22,71,31,23,28,36,21,17,45,78,79])).
% 67.28/67.27 cnf(5743,plain,
% 67.28/67.27 (~P1(f14(a2,a2),a2)),
% 67.28/67.27 inference(scs_inference,[],[1,326,632,759,761,1036,5637,5599,5607,5613,5253,5299,5668,5619,5659,507,465,654,786,29,15,51,70,50,99,38,102,52,39,69,27,32,37,30,20,22,71,31,23,28,36,21,17,45,78,79,34,77])).
% 67.28/67.27 cnf(5746,plain,
% 67.28/67.27 (~P2(a86,a91)),
% 67.28/67.27 inference(scs_inference,[],[1,326,632,759,761,1036,5637,5426,5599,5607,5613,5736,5253,5299,5668,5619,5659,507,465,654,786,29,15,51,70,50,99,38,102,52,39,69,27,32,37,30,20,22,71,31,23,28,36,21,17,45,78,79,34,77,94])).
% 67.28/67.27 cnf(5750,plain,
% 67.28/67.27 (P1(x57501,f48(a84,a84))),
% 67.28/67.27 inference(rename_variables,[],[664])).
% 67.28/67.27 cnf(5753,plain,
% 67.28/67.27 (~P1(x57531,f48(a5,a5))),
% 67.28/67.27 inference(rename_variables,[],[654])).
% 67.28/67.27 cnf(5758,plain,
% 67.28/67.27 (P1(f78(a62,a62),a62)),
% 67.28/67.27 inference(scs_inference,[],[1,326,632,759,761,1036,5637,5426,5599,5601,5607,5613,5736,5657,5253,5299,5519,5534,5668,5619,5659,507,465,654,664,786,29,15,51,70,50,99,38,102,52,39,69,27,32,37,30,20,22,71,31,23,28,36,21,17,45,78,79,34,77,94,46,48,41,81])).
% 67.28/67.27 cnf(5763,plain,
% 67.28/67.27 (P1(f77(a62,a62),a62)),
% 67.28/67.27 inference(scs_inference,[],[1,326,632,759,761,1036,5637,5426,5599,5601,5607,5613,5736,5657,5253,5299,5519,5534,5668,5619,5659,507,465,654,664,5750,786,29,15,51,70,50,99,38,102,52,39,69,27,32,37,30,20,22,71,31,23,28,36,21,17,45,78,79,34,77,94,46,48,41,81,44,80])).
% 67.28/67.27 cnf(5770,plain,
% 67.28/67.27 (~P1(f23(a65,a3),a65)),
% 67.28/67.27 inference(scs_inference,[],[1,326,632,759,761,1036,5637,5426,5505,5599,5601,5607,5613,5736,5657,5253,5299,5519,5534,5668,5619,5659,507,5247,465,654,5753,664,5750,786,8,29,15,51,70,50,99,38,102,52,39,69,27,32,37,30,20,22,71,31,23,28,36,21,17,45,78,79,34,77,94,46,48,41,81,44,80,43,100,98])).
% 67.28/67.27 cnf(5771,plain,
% 67.28/67.27 (P1(x57711,a3)),
% 67.28/67.27 inference(rename_variables,[],[8])).
% 67.28/67.27 cnf(5774,plain,
% 67.28/67.27 (P6(a69,a69,a9)),
% 67.28/67.27 inference(scs_inference,[],[1,326,632,759,761,1036,5637,5426,5505,5599,5601,5607,5613,5736,5657,5253,5299,5519,5534,5668,5619,5659,507,5247,465,654,5753,664,5750,786,8,29,15,51,70,50,99,38,102,52,39,69,27,32,37,30,20,22,71,31,23,28,36,21,17,45,78,79,34,77,94,46,48,41,81,44,80,43,100,98,33])).
% 67.28/67.27 cnf(5776,plain,
% 67.28/67.27 (P1(f36(a62,a3),a62)),
% 67.28/67.27 inference(scs_inference,[],[1,326,632,759,761,1036,5637,5426,5263,5505,5599,5601,5607,5613,5736,5657,5253,5299,5519,5534,5668,5619,5659,507,5247,465,654,5753,664,5750,786,8,5771,29,15,51,70,50,99,38,102,52,39,69,27,32,37,30,20,22,71,31,23,28,36,21,17,45,78,79,34,77,94,46,48,41,81,44,80,43,100,98,33,93])).
% 67.28/67.27 cnf(5780,plain,
% 67.28/67.27 (~P1(f40(a2,a58),a2)),
% 67.28/67.27 inference(scs_inference,[],[1,326,632,759,761,1036,5637,5426,5263,5491,5505,5599,5601,5607,5613,5736,5657,5253,5299,5519,5534,5668,5619,5659,507,5247,465,654,5753,664,5750,786,8,5771,598,29,15,51,70,50,99,38,102,52,39,69,27,32,37,30,20,22,71,31,23,28,36,21,17,45,78,79,34,77,94,46,48,41,81,44,80,43,100,98,33,93,101])).
% 67.28/67.27 cnf(5787,plain,
% 67.28/67.27 (~P1(f22(a2,a2),a2)),
% 67.28/67.27 inference(scs_inference,[],[1,326,632,759,761,1036,5637,5426,5263,5491,5505,5587,5599,5601,5607,5613,5736,5657,5253,5299,5519,5534,5668,5619,5659,594,507,5247,9,465,654,5753,664,5750,786,8,5771,14,598,29,15,51,70,50,99,38,102,52,39,69,27,32,37,30,20,22,71,31,23,28,36,21,17,45,78,79,34,77,94,46,48,41,81,44,80,43,100,98,33,93,101,76,90])).
% 67.28/67.27 cnf(5793,plain,
% 67.28/67.27 (P1(f76(a69,a69),a69)),
% 67.28/67.27 inference(scs_inference,[],[1,326,632,759,761,1036,5637,5426,5263,5491,5505,5587,5595,5599,5601,5607,5613,5736,5657,5253,5299,5519,5534,5668,5619,5659,594,507,5247,9,465,654,5753,664,5750,786,8,5771,14,598,29,15,51,70,50,99,38,102,52,39,69,27,32,37,30,20,22,71,31,23,28,36,21,17,45,78,79,34,77,94,46,48,41,81,44,80,43,100,98,33,93,101,76,90,74,54])).
% 67.28/67.27 cnf(5802,plain,
% 67.28/67.27 (~P6(a71,x58021,a85)),
% 67.28/67.27 inference(scs_inference,[],[5431,7,15,38])).
% 67.28/67.27 cnf(5816,plain,
% 67.28/67.27 (~P6(a71,x58161,a89)),
% 67.28/67.27 inference(scs_inference,[],[888,1276,5179,5431,7,955,15,38,50,51,99,29,69,70,39])).
% 67.28/67.27 cnf(5826,plain,
% 67.28/67.27 (~P6(a71,x58261,a83)),
% 67.28/67.27 inference(scs_inference,[],[341,888,1276,1280,5179,5431,7,786,955,15,38,50,51,99,29,69,70,39,27,102,32,52,37])).
% 67.28/67.27 cnf(5832,plain,
% 67.28/67.27 (P6(x58321,a71,a80)),
% 67.28/67.27 inference(scs_inference,[],[341,888,1276,1280,5179,5311,5431,7,786,955,15,38,50,51,99,29,69,70,39,27,102,32,52,37,30,20,22])).
% 67.28/67.27 cnf(5838,plain,
% 67.28/67.27 (P6(a71,x58381,a86)),
% 67.28/67.27 inference(scs_inference,[],[341,888,1276,1280,5179,5311,5431,7,786,955,15,38,50,51,99,29,69,70,39,27,102,32,52,37,30,20,22,71,31,23])).
% 67.28/67.27 cnf(5844,plain,
% 67.28/67.27 (P1(f6(a71),a71)),
% 67.28/67.27 inference(scs_inference,[],[341,888,1276,1280,5179,5311,5431,7,786,955,15,38,50,51,99,29,69,70,39,27,102,32,52,37,30,20,22,71,31,23,28,36,21])).
% 67.28/67.27 cnf(5846,plain,
% 67.28/67.27 (P1(f39(a58,a65),f74(a62))),
% 67.28/67.27 inference(scs_inference,[],[341,888,1276,1280,5179,2002,5311,5431,7,786,955,15,38,50,51,99,29,69,70,39,27,102,32,52,37,30,20,22,71,31,23,28,36,21,17])).
% 67.28/67.27 cnf(5848,plain,
% 67.28/67.27 (P6(a2,a58,a4)),
% 67.28/67.27 inference(scs_inference,[],[1,341,888,1276,1280,5179,2002,5311,5431,7,786,955,598,15,38,50,51,99,29,69,70,39,27,102,32,52,37,30,20,22,71,31,23,28,36,21,17,40])).
% 67.28/67.27 cnf(5860,plain,
% 67.28/67.27 (P6(x58601,a56,a80)),
% 67.28/67.27 inference(rename_variables,[],[5717])).
% 67.28/67.27 cnf(5862,plain,
% 67.28/67.27 (~P2(a80,a85)),
% 67.28/67.27 inference(scs_inference,[],[1,341,888,1276,1280,5487,5717,5860,5723,5179,2002,5311,5356,5431,5729,7,664,786,955,598,15,38,50,51,99,29,69,70,39,27,102,32,52,37,30,20,22,71,31,23,28,36,21,17,40,45,34,78,79,94])).
% 67.28/67.27 cnf(5882,plain,
% 67.28/67.27 (P6(a56,a56,a9)),
% 67.28/67.27 inference(scs_inference,[],[1,341,888,1276,1280,5487,5711,5717,5860,5723,5179,5774,2002,5311,5793,5398,5356,5431,5729,7,5414,2012,5303,6,12,664,654,786,955,598,15,38,50,51,99,29,69,70,39,27,102,32,52,37,30,20,22,71,31,23,28,36,21,17,40,45,34,78,79,94,46,48,41,81,44,80,43,33])).
% 67.28/67.27 cnf(5890,plain,
% 67.28/67.27 (~P1(f12(a62,a3),a62)),
% 67.28/67.27 inference(scs_inference,[],[1,341,888,1276,1280,5487,5703,5711,5717,5860,5723,5179,5774,2002,5311,5793,5398,5356,5431,5729,5743,1746,5587,7,5414,2012,5303,6,12,664,654,786,955,8,598,15,38,50,51,99,29,69,70,39,27,102,32,52,37,30,20,22,71,31,23,28,36,21,17,40,45,34,78,79,94,46,48,41,81,44,80,43,33,90,74,106])).
% 67.28/67.27 cnf(5893,plain,
% 67.28/67.27 (P1(f76(a56,a56),a56)),
% 67.28/67.27 inference(scs_inference,[],[1,341,888,1276,1280,5487,5703,5711,5717,5860,5723,5179,5774,2002,5311,5793,5398,5356,5431,5729,5743,1746,5587,7,5414,2012,5303,6,12,664,654,786,955,8,598,15,38,50,51,99,29,69,70,39,27,102,32,52,37,30,20,22,71,31,23,28,36,21,17,40,45,34,78,79,94,46,48,41,81,44,80,43,33,90,74,106,54])).
% 67.28/67.27 cnf(5895,plain,
% 67.28/67.27 (P1(f38(a2,a58),a2)),
% 67.28/67.27 inference(scs_inference,[],[1,341,888,1276,1280,5487,5703,5711,5717,5860,5723,5179,5774,2002,5311,5793,5398,5356,5431,5729,5743,1746,5587,7,5414,2012,5303,6,12,664,654,786,955,8,598,15,38,50,51,99,29,69,70,39,27,102,32,52,37,30,20,22,71,31,23,28,36,21,17,40,45,34,78,79,94,46,48,41,81,44,80,43,33,90,74,106,54,65])).
% 67.28/67.27 cnf(5917,plain,
% 67.28/67.27 (P6(f48(a4,a4),f51(a4,a4),a4)),
% 67.28/67.27 inference(scs_inference,[],[351,1322,1324,1725,1727,5315,5457,664,38,15,99,50,69,51,102,70,52])).
% 67.28/67.27 cnf(5929,plain,
% 67.28/67.27 (P6(x59291,f48(a84,a84),a80)),
% 67.28/67.27 inference(scs_inference,[],[351,1322,1324,1725,1727,5315,5366,5457,664,955,14,38,15,99,50,69,51,102,70,52,32,39,30,37,20,22])).
% 67.28/67.27 cnf(5937,plain,
% 67.28/67.27 (~P6(x59371,a58,a84)),
% 67.28/67.27 inference(scs_inference,[],[351,1322,1324,1725,1727,5315,5366,5457,664,955,14,38,15,99,50,69,51,102,70,52,32,39,30,37,20,22,71,31,23,28])).
% 67.28/67.27 cnf(5948,plain,
% 67.28/67.27 (P6(a71,a71,a82)),
% 67.28/67.27 inference(scs_inference,[],[1,351,1322,1324,1725,1727,5838,5315,5182,5366,5844,5457,10,5,664,955,14,38,15,99,50,69,51,102,70,52,32,39,30,37,20,22,71,31,23,28,36,17,45,78,34])).
% 67.28/67.27 cnf(5951,plain,
% 67.28/67.27 (P6(x59511,a71,a80)),
% 67.28/67.27 inference(rename_variables,[],[5832])).
% 67.28/67.27 cnf(5953,plain,
% 67.28/67.27 (~P2(a80,a84)),
% 67.28/67.27 inference(scs_inference,[],[1,351,1322,1324,1725,1727,5147,5832,5951,5838,5315,5182,5366,5844,5457,10,5,664,955,14,38,15,99,50,69,51,102,70,52,32,39,30,37,20,22,71,31,23,28,36,17,45,78,34,79,94])).
% 67.28/67.27 cnf(5957,plain,
% 67.28/67.27 (P1(x59571,f48(a84,a84))),
% 67.28/67.27 inference(rename_variables,[],[664])).
% 67.28/67.27 cnf(5960,plain,
% 67.28/67.27 (~P1(x59601,f48(a5,a5))),
% 67.28/67.27 inference(rename_variables,[],[654])).
% 67.28/67.27 cnf(5970,plain,
% 67.28/67.27 (P6(a2,a58,a73)),
% 67.28/67.27 inference(scs_inference,[],[1,351,1322,1324,1725,1727,5848,5147,5826,5832,5951,5838,5315,5882,5182,5366,5780,5893,5844,5457,10,5,13,664,5957,654,955,14,38,15,99,50,69,51,102,70,52,32,39,30,37,20,22,71,31,23,28,36,17,45,78,34,79,94,46,48,81,41,44,91])).
% 67.28/67.27 cnf(5972,plain,
% 67.28/67.27 (P1(f77(a56,a56),a56)),
% 67.28/67.27 inference(scs_inference,[],[1,351,1322,1324,1725,1727,5848,5147,5826,5832,5951,5838,5315,5882,5182,5366,5780,5893,5844,5457,10,5,13,664,5957,654,955,14,38,15,99,50,69,51,102,70,52,32,39,30,37,20,22,71,31,23,28,36,17,45,78,34,79,94,46,48,81,41,44,91,80])).
% 67.28/67.27 cnf(5980,plain,
% 67.28/67.27 (P6(a71,a71,a9)),
% 67.28/67.27 inference(scs_inference,[],[1,351,1322,1324,1725,1727,5848,5147,5826,5832,5951,5838,5315,5882,5182,5366,5780,5893,5844,5457,5141,10,5,13,664,5957,654,5960,955,14,38,15,99,50,69,51,102,70,52,32,39,30,37,20,22,71,31,23,28,36,17,45,78,34,79,94,46,48,81,41,44,91,80,43,105,33])).
% 67.28/67.27 cnf(5988,plain,
% 67.28/67.27 (P1(f76(a71,a71),a71)),
% 67.28/67.27 inference(scs_inference,[],[1,351,1322,1324,1725,1727,5848,5147,5816,5826,5832,5951,5838,5315,5882,5182,5366,5780,5893,5844,5457,583,5141,10,5,13,664,5957,654,5960,955,14,38,15,99,50,69,51,102,70,52,32,39,30,37,20,22,71,31,23,28,36,17,45,78,34,79,94,46,48,81,41,44,91,80,43,105,33,76,74,54])).
% 67.28/67.27 cnf(6017,plain,
% 67.28/67.27 (~P6(x60171,a58,a85)),
% 67.28/67.27 inference(scs_inference,[],[362,1737,1739,1762,1764,5421,5563,8,14,598,15,69,99,38,51,50,102,39,70,52,37,30])).
% 67.28/67.27 cnf(6019,plain,
% 67.28/67.27 (~P1(f6(a59),f74(a59))),
% 67.28/67.27 inference(scs_inference,[],[362,1737,1739,1762,1764,5421,5513,5563,8,14,598,15,69,99,38,51,50,102,39,70,52,37,30,20])).
% 67.28/67.27 cnf(6021,plain,
% 67.28/67.27 (P6(x60211,a3,a80)),
% 67.28/67.27 inference(scs_inference,[],[362,1737,1739,1762,1764,5421,5513,5563,8,14,598,15,69,99,38,51,50,102,39,70,52,37,30,20,22])).
% 67.28/67.27 cnf(6031,plain,
% 67.28/67.27 (~P6(a3,x60311,a5)),
% 67.28/67.27 inference(scs_inference,[],[362,1737,1739,1762,1764,5421,5513,5563,8,14,598,15,69,99,38,51,50,102,39,70,52,37,30,20,22,71,31,23,28,36])).
% 67.28/67.27 cnf(6039,plain,
% 67.28/67.27 (~P6(a2,f48(a84,a84),a75)),
% 67.28/67.27 inference(scs_inference,[],[362,1737,1739,1762,1764,5421,5513,5563,5224,5787,664,8,14,598,15,69,99,38,51,50,102,39,70,52,37,30,20,22,71,31,23,28,36,17,49,47,45])).
% 67.28/67.27 cnf(6040,plain,
% 67.28/67.27 (P1(x60401,f48(a84,a84))),
% 67.28/67.27 inference(rename_variables,[],[664])).
% 67.28/67.27 cnf(6043,plain,
% 67.28/67.27 (P1(x60431,f48(a84,a84))),
% 67.28/67.27 inference(rename_variables,[],[664])).
% 67.28/67.27 cnf(6049,plain,
% 67.28/67.27 (~P6(a71,x60491,a85)),
% 67.28/67.27 inference(rename_variables,[],[5802])).
% 67.28/67.27 cnf(6064,plain,
% 67.28/67.27 (P1(x60641,f48(a84,a84))),
% 67.28/67.27 inference(rename_variables,[],[664])).
% 67.28/67.27 cnf(6066,plain,
% 67.28/67.27 (P6(a2,f48(a84,a84),a9)),
% 67.28/67.27 inference(scs_inference,[],[1,362,1737,1739,1762,1764,5802,6049,5421,5948,5980,5513,5988,5846,5563,5224,5363,5787,5145,654,664,6040,6043,6064,786,8,14,598,15,69,99,38,51,50,102,39,70,52,37,30,20,22,71,31,23,28,36,17,49,47,45,34,48,94,46,81,44,91,80,43,33])).
% 67.28/67.27 cnf(6083,plain,
% 67.28/67.27 (P1(f78(a62,a62),a65)),
% 67.28/67.27 inference(scs_inference,[],[1962,5523,5758,69,99,15])).
% 67.28/67.27 cnf(6111,plain,
% 67.28/67.27 (P1(f19(a65,a3),f74(a62))),
% 67.28/67.27 inference(scs_inference,[],[366,1962,1964,1969,1971,5523,5895,6019,5758,2102,598,69,99,15,102,51,50,38,52,70,30,20,71,22,31,23,36,17])).
% 67.28/67.27 cnf(6125,plain,
% 67.28/67.27 (~P2(a80,a5)),
% 67.28/67.27 inference(scs_inference,[],[1,366,1962,1964,1969,1971,6021,6031,5523,5895,5738,6019,5758,2102,5513,460,4,654,664,598,69,99,15,102,51,50,38,52,70,30,20,71,22,31,23,36,17,47,49,45,34,48,94])).
% 67.28/67.27 cnf(6159,plain,
% 67.28/67.27 (P1(f77(a62,a62),a65)),
% 67.28/67.27 inference(scs_inference,[],[376,1259,5862,5763,99,69,50,102,15])).
% 67.28/67.27 cnf(6167,plain,
% 67.28/67.27 (~P1(f78(a62,a62),f74(a65))),
% 67.28/67.27 inference(scs_inference,[],[376,1259,1263,5862,6083,5763,99,69,50,102,15,51,52,70,20])).
% 67.28/67.27 cnf(6182,plain,
% 67.28/67.27 (~P2(a73,a85)),
% 67.28/67.27 inference(scs_inference,[],[1,376,1259,1263,5862,6017,5970,6083,5763,5214,6019,5513,6,12,8,99,69,50,102,15,51,52,70,20,71,17,33,34,45,48,94])).
% 67.28/67.27 cnf(6185,plain,
% 67.28/67.27 (~P6(f74(a62),a62,a10)),
% 67.28/67.27 inference(scs_inference,[],[1,376,1259,1263,5862,6017,5970,6111,6083,5763,5214,2102,6019,5513,6,12,8,99,69,50,102,15,51,52,70,20,71,17,33,34,45,48,94,46])).
% 67.28/67.27 cnf(6227,plain,
% 67.28/67.27 (P1(f36(a62,a3),a65)),
% 67.28/67.27 inference(scs_inference,[],[380,1354,1351,5953,5776,69,99,51,50,102,15])).
% 67.28/67.27 cnf(6233,plain,
% 67.28/67.27 (~P1(a55,f74(a56))),
% 67.28/67.27 inference(scs_inference,[],[2,380,1354,1351,5953,5776,69,99,51,50,102,15,52,70,20])).
% 67.28/67.27 cnf(6250,plain,
% 67.28/67.27 (P1(x62501,f48(a84,a84))),
% 67.28/67.27 inference(rename_variables,[],[664])).
% 67.28/67.27 cnf(6255,plain,
% 67.28/67.27 (~P1(x62551,f48(a5,a5))),
% 67.28/67.27 inference(rename_variables,[],[654])).
% 67.28/67.27 cnf(6257,plain,
% 67.28/67.27 (P1(f32(a2,a56),a2)),
% 67.28/67.27 inference(scs_inference,[],[2,380,1354,1351,5953,6167,6159,5776,5231,5121,5758,654,664,69,99,51,50,102,15,52,70,20,71,31,28,17,33,47,49,34,45,48,41])).
% 67.28/67.27 cnf(6260,plain,
% 67.28/67.27 (~P2(a9,a75)),
% 67.28/67.27 inference(scs_inference,[],[2,380,1354,1351,5953,6039,6167,6066,6159,5776,5231,5121,5758,654,664,69,99,51,50,102,15,52,70,20,71,31,28,17,33,47,49,34,45,48,41,94])).
% 67.28/67.27 cnf(6263,plain,
% 67.28/67.27 (~P1(x62631,f48(a5,a5))),
% 67.28/67.27 inference(rename_variables,[],[654])).
% 67.28/67.27 cnf(6267,plain,
% 67.28/67.27 (~P6(a71,f48(a84,a84),a10)),
% 67.28/67.27 inference(scs_inference,[],[2,380,1354,1351,5953,6039,6167,6066,6159,5776,5231,5570,5121,6083,5758,654,6255,664,6250,598,69,99,51,50,102,15,52,70,20,71,31,28,17,33,47,49,34,45,48,41,94,81,46,44])).
% 67.28/67.27 cnf(6283,plain,
% 67.28/67.27 (P6(a56,a58,a4)),
% 67.28/67.27 inference(scs_inference,[],[2,380,1354,1351,5953,6039,6167,6066,6159,5917,5776,5231,5570,5121,6083,5758,13,654,6255,6263,664,6250,598,69,99,51,50,102,15,52,70,20,71,31,28,17,33,47,49,34,45,48,41,94,81,46,44,91,43,29,27,32,30,40])).
% 67.28/67.27 cnf(6317,plain,
% 67.28/67.27 (~P1(f36(a62,a3),f74(a65))),
% 67.28/67.27 inference(scs_inference,[],[395,882,1193,5746,6227,99,69,50,102,51,52,70,20])).
% 67.28/67.27 cnf(6338,plain,
% 67.28/67.27 (~P2(a4,a85)),
% 67.28/67.27 inference(scs_inference,[],[2,395,882,1193,6283,5746,6233,6227,5697,5770,3,664,99,69,50,102,51,52,70,20,71,65,17,33,47,49,34,45,48,94])).
% 67.28/67.27 cnf(6345,plain,
% 67.28/67.27 (P6(a56,a58,a73)),
% 67.28/67.27 inference(scs_inference,[],[2,395,882,1193,6283,5746,6233,6227,5697,5770,13,3,664,99,69,50,102,51,52,70,20,71,65,17,33,47,49,34,45,48,94,46,44,91])).
% 67.28/67.27 cnf(6443,plain,
% 67.28/67.27 (P6(a56,a3,a9)),
% 67.28/67.27 inference(scs_inference,[],[2,409,1206,1202,6125,6257,5632,8,99,50,69,102,51,52,70,71,20,17,33])).
% 67.28/67.27 cnf(6446,plain,
% 67.28/67.27 (P1(x64461,a3)),
% 67.28/67.27 inference(rename_variables,[],[8])).
% 67.28/67.27 cnf(6461,plain,
% 67.28/67.27 (P1(f76(a3,a56),a56)),
% 67.28/67.27 inference(scs_inference,[],[2,409,1206,1202,6125,6345,5937,6257,5972,5632,5846,5145,654,786,8,6446,99,50,69,102,51,52,70,71,20,17,33,34,48,46,94,81,43,53])).
% 67.28/67.27 cnf(6485,plain,
% 67.28/67.27 (P1(f19(a62,a3),f74(a62))),
% 67.28/67.27 inference(scs_inference,[],[419,1038,1185,6182,6461,2007,99,50,69,51,102,52,70,71,20,17])).
% 67.28/67.27 cnf(6490,plain,
% 67.28/67.27 (P1(x64901,a3)),
% 67.28/67.27 inference(rename_variables,[],[8])).
% 67.28/67.27 cnf(6500,plain,
% 67.28/67.27 (P1(f77(a3,a56),a56)),
% 67.28/67.27 inference(scs_inference,[],[2,419,1038,1185,6182,6267,5929,6461,2007,5416,6,12,654,8,6490,99,50,69,51,102,52,70,71,20,17,33,34,48,46,94,80])).
% 67.28/67.27 cnf(6536,plain,
% 67.28/67.27 (~P1(f77(a3,a56),f74(a56))),
% 67.28/67.27 inference(scs_inference,[],[423,1237,1235,3222,3228,6260,6500,50,99,69,51,102,52,70,20])).
% 67.28/67.27 cnf(6542,plain,
% 67.28/67.27 (P6(f74(a62),a62,a4)),
% 67.28/67.27 inference(scs_inference,[],[423,1237,1235,3222,3228,6260,6485,6500,5890,50,99,69,51,102,52,70,20,71,17,40])).
% 67.28/67.27 cnf(6544,plain,
% 67.28/67.27 (~P1(f14(a56,a65),a65)),
% 67.28/67.27 inference(scs_inference,[],[2,423,1237,1235,3222,3228,6260,6485,6500,5890,5485,50,99,69,51,102,52,70,20,71,17,40,77])).
% 67.28/67.27 cnf(6555,plain,
% 67.28/67.27 (P1(f32(a62,a56),a62)),
% 67.28/67.27 inference(scs_inference,[],[2,423,1237,1235,3222,3228,6260,6485,6500,5890,5507,5285,5291,5485,598,50,99,69,51,102,52,70,20,71,17,40,77,78,33,79,41])).
% 67.28/67.27 cnf(6559,plain,
% 67.28/67.27 (P1(x65591,f74(a58))),
% 67.28/67.27 inference(rename_variables,[],[598])).
% 67.28/67.27 cnf(6565,plain,
% 67.28/67.27 (~P1(x65651,f48(a5,a5))),
% 67.28/67.27 inference(rename_variables,[],[654])).
% 67.28/67.27 cnf(6575,plain,
% 67.28/67.27 (P1(f52(a56,a62),a65)),
% 67.28/67.27 inference(scs_inference,[],[2,423,1237,1235,3222,3228,6260,6443,6485,6500,5727,5575,5890,5507,5285,5291,5485,6019,5513,654,6565,955,598,6559,50,99,69,51,102,52,70,20,71,17,40,77,78,33,79,41,34,48,46,94,80,43,15])).
% 67.28/67.27 cnf(6624,plain,
% 67.28/67.27 ($false),
% 67.28/67.27 inference(scs_inference,[],[2,433,4132,1249,6338,6185,6536,6575,6544,6555,6542,5203,6317,5776,13,664,786,598,50,15,99,51,69,102,52,70,71,20,17,33,45,34,48,46,94,91]),
% 67.28/67.27 ['proof']).
% 67.28/67.27 % SZS output end Proof
% 67.28/67.27 % Total time :66.580000s
%------------------------------------------------------------------------------