%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : KRS202+1 : TPTP v8.2.0. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : 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:52 EDT 2024
% Result : Theorem 97.93s 97.98s
% Output : CNFRefutation 97.93s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : KRS202+1 : TPTP v8.2.0. Bugfixed v5.4.0.
% 0.08/0.14 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.14/0.36 % Computer : n008.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed Jun 19 12:16:09 EDT 2024
% 0.14/0.36 % CPUTime :
% 0.53/0.62 start to proof:theBenchmark
% 97.93/97.97 %-------------------------------------------
% 97.93/97.97 % File :CSE---1.7
% 97.93/97.97 % Problem :theBenchmark
% 97.93/97.97 % Transform :cnf
% 97.93/97.97 % Format :tptp:raw
% 97.93/97.97 % Command :java -jar mcs_scs.jar %d %s
% 97.93/97.97
% 97.93/97.97 % Result :Theorem 97.260000s
% 97.93/97.97 % Output :CNFRefutation 97.260000s
% 97.93/97.97 %-------------------------------------------
% 97.93/97.98 %------------------------------------------------------------------------------
% 97.93/97.98 % File : KRS202+1 : TPTP v8.2.0. Bugfixed v5.4.0.
% 97.93/97.98 % Domain : Knowledge Representation
% 97.93/97.98 % Problem : ESA nota THM
% 97.93/97.98 % Version : [Sut08] axioms.
% 97.93/97.98 % English :
% 97.93/97.98
% 97.93/97.98 % Refs : [Sut08] Sutcliffe (2008), The SZS Ontologies for Automated Rea
% 97.93/97.98 % Source : [TPTP]
% 97.93/97.98 % Names :
% 97.93/97.98
% 97.93/97.98 % Status : Theorem
% 97.93/97.98 % Rating : 0.19 v8.2.0, 0.27 v8.1.0, 0.14 v7.5.0, 0.24 v7.4.0, 0.12 v7.3.0, 0.29 v7.2.0, 0.17 v7.1.0, 0.25 v7.0.0, 0.14 v6.4.0, 0.07 v6.3.0, 0.08 v6.2.0, 0.27 v6.1.0, 0.28 v6.0.0, 0.50 v5.5.0, 0.42 v5.4.0
% 97.93/97.98 % Syntax : Number of formulae : 33 ( 3 unt; 0 def)
% 97.93/97.98 % Number of atoms : 107 ( 0 equ)
% 97.93/97.98 % Maximal formula atoms : 7 ( 3 avg)
% 97.93/97.98 % Number of connectives : 96 ( 22 ~; 1 |; 35 &)
% 97.93/97.98 % ( 28 <=>; 8 =>; 0 <=; 2 <~>)
% 97.93/97.98 % Maximal formula depth : 10 ( 6 avg)
% 97.93/97.98 % Maximal term depth : 2 ( 1 avg)
% 97.93/97.98 % Number of predicates : 7 ( 7 usr; 0 prp; 2-3 aty)
% 97.93/97.98 % Number of functors : 20 ( 20 usr; 19 con; 0-1 aty)
% 97.93/97.98 % Number of variables : 122 ( 72 !; 50 ?)
% 97.93/97.98 % SPC : FOF_THM_RFO_NEQ
% 97.93/97.98
% 97.93/97.98 % Comments :
% 97.93/97.98 % Bugfixes : v5.4.0 - Added missing axiom in KRS001+1.ax
% 97.93/97.98 %------------------------------------------------------------------------------
% 97.93/97.98 %----Include SZS success ontology nodes
% 97.93/97.98 include('Axioms/KRS001+0.ax').
% 97.93/97.98 %----Include SZS success ontology node relationships
% 97.93/97.98 include('Axioms/KRS001+1.ax').
% 97.93/97.98 %------------------------------------------------------------------------------
% 97.93/97.98 fof(nota_esa_thm,conjecture,
% 97.93/97.98 nota(esa,thm) ).
% 97.93/97.98
% 97.93/97.98 %------------------------------------------------------------------------------
% 97.93/97.98 %-------------------------------------------
% 97.93/97.98 % Proof found
% 97.93/97.98 % SZS status Theorem for theBenchmark
% 97.93/97.98 % SZS output start Proof
% 97.93/97.99 %ClaNum:109(EqnAxiom:0)
% 97.93/97.99 %VarNum:590(SingletonVarNum:249)
% 97.93/97.99 %MaxLitNum:6
% 97.93/97.99 %MaxfuncDepth:1
% 97.93/97.99 %SharedTerms:52
% 97.93/97.99 %goalClause: 13
% 97.93/97.99 %singleGoalClaCount:1
% 97.93/97.99 [1]P1(a1,a2)
% 97.93/97.99 [2]P1(a55,a56)
% 97.93/97.99 [3]P1(a55,a59)
% 97.93/97.99 [4]P1(a61,a62)
% 97.93/97.99 [5]P1(a66,a65)
% 97.93/97.99 [6]P1(a67,a69)
% 97.93/97.99 [7]P1(a70,a71)
% 97.93/97.99 [9]~P1(a57,a2)
% 97.93/97.99 [10]~P1(a66,a62)
% 97.93/97.99 [11]~P1(a68,a65)
% 97.93/97.99 [12]~P1(a67,a71)
% 97.93/97.99 [13]~P4(a4,a73)
% 97.93/97.99 [8]P1(x81,a3)
% 97.93/97.99 [14]~P1(x141,a58)
% 97.93/97.99 [18]~P1(a63,a56)+~P1(a64,a59)
% 97.93/97.99 [15]~P1(x151,a62)+P1(x151,a65)
% 97.93/97.99 [17]P1(x171,x172)+P1(x171,f74(x172))
% 97.93/97.99 [20]~P1(x201,x202)+~P1(x201,f74(x202))
% 97.93/97.99 [21]P6(x211,x212,a5)+P1(f8(x211),x211)
% 97.93/97.99 [24]P6(x241,x242,a86)+P1(f9(x241,x242),x242)
% 97.93/97.99 [25]P6(x251,x252,a80)+P1(f31(x251,x252),x251)
% 97.93/97.99 [26]P6(x261,x262,a73)+P1(f10(x261,x262),x261)
% 97.93/97.99 [42]P6(x421,x422,a73)+~P1(f10(x421,x422),x422)
% 97.93/97.99 [50]P2(x501,x502)+P6(f41(x501,x502),f47(x501,x502),x501)
% 97.93/97.99 [51]P5(x511,x512)+P6(f48(x511,x512),f51(x511,x512),x512)
% 97.93/97.99 [52]P5(x521,x522)+P6(f48(x521,x522),f51(x521,x522),x521)
% 97.93/97.99 [53]~P6(x531,x532,a82)+P1(f76(x531,x532),x532)
% 97.93/97.99 [54]~P6(x541,x542,a82)+P1(f76(x541,x542),x541)
% 97.93/97.99 [55]~P6(x551,x552,a7)+P1(f11(x551,x552),x551)
% 97.93/97.99 [56]~P6(x561,x562,a81)+P1(f13(x561,x562),x561)
% 97.93/97.99 [57]~P6(x571,x572,a90)+P1(f15(x571,x572),x571)
% 97.93/97.99 [58]~P6(x581,x582,a90)+P1(f17(x581,x582),x582)
% 97.93/97.99 [59]~P6(x591,x592,a75)+P1(f18(x591,x592),x591)
% 97.93/97.99 [60]~P6(x601,x602,a87)+P1(f20(x601,x602),x601)
% 97.93/97.99 [61]~P6(x611,x612,a91)+P1(f25(x611,x612),x611)
% 97.93/97.99 [62]~P6(x621,x622,a91)+P1(f28(x621,x622),x622)
% 97.93/97.99 [63]~P6(x631,x632,a83)+P1(f33(x631,x632),x632)
% 97.93/97.99 [64]~P6(x641,x642,a89)+P1(f34(x641,x642),x642)
% 97.93/97.99 [65]~P6(x651,x652,a6)+P1(f38(x651,x652),x651)
% 97.93/97.99 [66]~P6(x661,x662,a79)+P1(f42(x661,x662),x662)
% 97.93/97.99 [67]~P6(x671,x672,a79)+P1(f42(x671,x672),x671)
% 97.93/97.99 [68]~P6(x681,x682,a79)+P1(f44(x681,x682),x681)
% 97.93/97.99 [69]~P3(x691,x692)+P6(f45(x691,x692),f46(x691,x692),x692)
% 97.93/97.99 [70]~P3(x701,x702)+P6(f45(x701,x702),f46(x701,x702),x701)
% 97.93/97.99 [71]~P4(x711,x712)+P6(f49(x711,x712),f50(x711,x712),x711)
% 97.93/97.99 [72]~P6(x721,x722,a6)+P1(f38(x721,x722),f74(x722))
% 97.93/97.99 [73]~P6(x731,x732,a79)+P1(f44(x731,x732),f74(x732))
% 97.93/97.99 [82]~P6(x821,x822,a90)+~P1(f17(x821,x822),x821)
% 97.93/97.99 [83]~P6(x831,x832,a75)+~P1(f21(x831,x832),x831)
% 97.93/97.99 [84]~P6(x841,x842,a87)+~P1(f26(x841,x842),x841)
% 97.93/97.99 [85]~P6(x851,x852,a91)+~P1(f28(x851,x852),x851)
% 97.93/97.99 [86]~P6(x861,x862,a91)+~P1(f30(x861,x862),x862)
% 97.93/97.99 [87]~P6(x871,x872,a89)+~P1(f39(x871,x872),x872)
% 97.93/97.99 [99]P2(x991,x992)+~P6(f41(x991,x992),f47(x991,x992),x992)
% 97.93/97.99 [102]~P4(x1021,x1022)+~P6(f49(x1021,x1022),f50(x1021,x1022),x1022)
% 97.93/97.99 [22]~P1(x223,x222)+P6(x221,x222,a80)
% 97.93/97.99 [23]~P1(x233,x231)+P6(x231,x232,a86)
% 97.93/97.99 [27]P1(x271,x272)+~P6(x273,x272,a81)
% 97.93/97.99 [28]P1(x281,x282)+~P6(x283,x282,a84)
% 97.93/97.99 [29]P1(x291,x292)+~P6(x293,x292,a87)
% 97.93/97.99 [30]P1(x301,x302)+~P6(x303,x302,a85)
% 97.93/97.99 [31]P1(x311,x312)+~P6(x312,x313,a84)
% 97.93/97.99 [32]P1(x321,x322)+~P6(x322,x323,a88)
% 97.93/97.99 [36]~P1(x361,x362)+~P6(x362,x363,a5)
% 97.93/97.99 [37]~P1(x371,x372)+~P6(x372,x373,a83)
% 97.93/97.99 [38]~P1(x381,x382)+~P6(x382,x383,a85)
% 97.93/97.99 [39]~P1(x391,x392)+~P6(x392,x393,a89)
% 97.93/97.99 [35]~P6(x353,x352,a88)+P1(x351,f74(x352))
% 97.93/97.99 [76]P6(x761,x762,a4)+P1(f60(x761,x762),x761)+P1(f72(x761,x762),x762)
% 97.93/97.99 [93]P6(x931,x932,a85)+P1(f36(x931,x932),x931)+~P1(f37(x931,x932),x932)
% 97.93/97.99 [98]P6(x981,x982,a84)+~P1(f23(x981,x982),x981)+~P1(f24(x981,x982),x982)
% 97.93/97.99 [101]P6(x1011,x1012,a88)+~P1(f40(x1011,x1012),x1011)+~P1(f43(x1011,x1012),f74(x1012))
% 97.93/97.99 [108]P7(x1081,x1082)+P6(f53(x1081,x1082),f54(x1081,x1082),x1082)+~P6(f53(x1081,x1082),f54(x1081,x1082),x1081)
% 97.93/97.99 [109]P7(x1091,x1092)+P6(f53(x1091,x1092),f54(x1091,x1092),x1091)+~P6(f53(x1091,x1092),f54(x1091,x1092),x1092)
% 97.93/97.99 [34]~P1(x343,x341)+~P1(x343,x342)+P6(x341,x342,a82)
% 97.93/97.99 [43]P1(x431,x432)+~P1(x431,x433)+~P6(x433,x432,a73)
% 97.93/97.99 [44]P1(x441,x442)+~P1(x441,x443)+~P6(x442,x443,a7)
% 97.93/97.99 [45]P1(x451,x452)+~P1(x451,x453)+~P6(x452,x453,a75)
% 97.93/97.99 [46]P1(x461,x462)+~P1(x461,x463)+~P6(x463,x462,a7)
% 97.93/97.99 [47]P1(x471,x472)+~P1(x471,x473)+~P6(x473,x472,a90)
% 97.93/97.99 [48]P1(x481,x482)+~P1(x481,x483)+~P6(x483,x482,a75)
% 97.93/97.99 [49]P1(x491,x492)+~P1(x491,x493)+~P6(x493,x492,a91)
% 97.93/97.99 [40]~P1(x403,x401)+P6(x401,x402,a6)+~P1(x403,f74(x402))
% 97.93/97.99 [41]~P1(x413,x412)+P6(x411,x412,a83)+P1(f32(x411,x412),x411)
% 97.93/97.99 [77]~P1(x773,x771)+P6(x771,x772,a81)+~P1(f14(x771,x772),x772)
% 97.93/97.99 [78]~P1(x783,x782)+~P6(x781,x782,a86)+P1(f29(x781,x782),x781)
% 97.93/97.99 [79]~P1(x793,x791)+~P6(x791,x792,a80)+P1(f52(x791,x792),x792)
% 97.93/97.99 [80]~P1(x803,x801)+~P6(x801,x802,a4)+P1(f77(x801,x802),x802)
% 97.93/97.99 [81]~P1(x813,x812)+~P6(x811,x812,a4)+P1(f78(x811,x812),x811)
% 97.93/97.99 [33]~P1(x333,x332)+~P1(x334,x331)+P6(x331,x332,a4)
% 97.93/97.99 [75]~P7(x754,x753)+P6(x751,x752,x753)+P6(x751,x752,x754)
% 97.93/97.99 [91]~P6(x913,x914,x911)+P4(x911,x912)+P6(x913,x914,x912)
% 97.93/97.99 [94]~P6(x941,x942,x944)+P6(x941,x942,x943)+~P2(x944,x943)
% 97.93/97.99 [100]~P6(x1003,x1004,x1001)+P3(x1001,x1002)+~P6(x1003,x1004,x1002)
% 97.93/97.99 [104]~P6(x1043,x1044,x1041)+~P5(x1041,x1042)+~P6(x1043,x1044,x1042)
% 97.93/97.99 [105]~P6(x1053,x1054,x1051)+~P7(x1051,x1052)+~P6(x1053,x1054,x1052)
% 97.93/97.99 [92]~P1(x923,x921)+P6(x921,x922,a7)+P1(f12(x921,x922),x922)+P1(f12(x921,x922),x921)
% 97.93/97.99 [106]~P1(x1063,x1061)+P6(x1061,x1062,a7)+~P1(f12(x1061,x1062),x1062)+~P1(f12(x1061,x1062),x1061)
% 97.93/97.99 [74]P1(x741,x742)+~P1(x744,x742)+P6(x743,x742,a89)+P1(f35(x743,x742),x743)
% 97.93/97.99 [90]P1(x901,x902)+~P1(x904,x902)+P6(x902,x903,a87)+~P1(f22(x902,x903),x903)
% 97.93/97.99 [88]~P1(x881,x883)+P1(x881,x882)+~P1(x884,x882)+P6(x882,x883,a90)+P1(f16(x882,x883),x882)
% 97.93/97.99 [89]~P1(x894,x891)+~P1(x893,x891)+~P1(x894,x892)+P6(x891,x892,a79)+~P1(x893,f74(x892))
% 97.93/97.99 [96]P1(x961,x962)+~P1(x964,x962)+P6(x962,x963,a75)+P1(f19(x962,x963),x963)+P1(f19(x962,x963),x962)
% 97.93/97.99 [97]~P1(x971,x973)+P1(x971,x972)+~P1(x974,x972)+P6(x972,x973,a90)+~P1(f16(x972,x973),x973)
% 97.93/97.99 [107]P1(x1071,x1072)+~P1(x1074,x1072)+P6(x1072,x1073,a75)+~P1(f19(x1072,x1073),x1073)+~P1(f19(x1072,x1073),x1072)
% 97.93/97.99 [95]~P1(x953,x952)+P1(x951,x952)+P1(x953,x954)+~P1(x955,x954)+P6(x954,x952,a91)+P1(f27(x954,x952),x954)
% 97.93/97.99 [103]~P1(x1033,x1032)+P1(x1031,x1032)+P1(x1033,x1034)+~P1(x1035,x1034)+P6(x1034,x1032,a91)+~P1(f27(x1034,x1032),x1032)
% 97.93/97.99 %EqnAxiom
% 97.93/97.99
% 97.93/97.99 %-------------------------------------------
% 97.93/98.00 cnf(110,plain,
% 97.93/98.00 (P6(a58,x1101,a5)),
% 97.93/98.00 inference(scs_inference,[],[14,21])).
% 97.93/98.00 cnf(111,plain,
% 97.93/98.00 (~P1(x1111,a58)),
% 97.93/98.00 inference(rename_variables,[],[14])).
% 97.93/98.00 cnf(113,plain,
% 97.93/98.00 (P6(x1131,a58,a86)),
% 97.93/98.00 inference(scs_inference,[],[14,111,21,24])).
% 97.93/98.00 cnf(114,plain,
% 97.93/98.00 (~P1(x1141,a58)),
% 97.93/98.00 inference(rename_variables,[],[14])).
% 97.93/98.00 cnf(116,plain,
% 97.93/98.00 (P6(a58,x1161,a80)),
% 97.93/98.00 inference(scs_inference,[],[14,111,114,21,24,25])).
% 97.93/98.00 cnf(117,plain,
% 97.93/98.00 (~P1(x1171,a58)),
% 97.93/98.00 inference(rename_variables,[],[14])).
% 97.93/98.00 cnf(119,plain,
% 97.93/98.00 (P6(a58,x1191,a73)),
% 97.93/98.00 inference(scs_inference,[],[14,111,114,117,21,24,25,26])).
% 97.93/98.00 cnf(120,plain,
% 97.93/98.00 (~P1(x1201,a58)),
% 97.93/98.00 inference(rename_variables,[],[14])).
% 97.93/98.00 cnf(122,plain,
% 97.93/98.00 (P6(x1221,a3,a73)),
% 97.93/98.00 inference(scs_inference,[],[8,14,111,114,117,21,24,25,26,42])).
% 97.93/98.00 cnf(123,plain,
% 97.93/98.00 (P1(x1231,a3)),
% 97.93/98.00 inference(rename_variables,[],[8])).
% 97.93/98.00 cnf(125,plain,
% 97.93/98.00 (~P1(a68,a62)),
% 97.93/98.00 inference(scs_inference,[],[8,14,111,114,117,11,21,24,25,26,42,15])).
% 97.93/98.00 cnf(127,plain,
% 97.93/98.00 (~P6(x1271,a58,a82)),
% 97.93/98.00 inference(scs_inference,[],[8,14,111,114,117,120,11,21,24,25,26,42,15,53])).
% 97.93/98.00 cnf(128,plain,
% 97.93/98.00 (~P1(x1281,a58)),
% 97.93/98.00 inference(rename_variables,[],[14])).
% 97.93/98.00 cnf(130,plain,
% 97.93/98.00 (~P6(a58,x1301,a82)),
% 97.93/98.00 inference(scs_inference,[],[8,14,111,114,117,120,128,11,21,24,25,26,42,15,53,54])).
% 97.93/98.00 cnf(131,plain,
% 97.93/98.00 (~P1(x1311,a58)),
% 97.93/98.00 inference(rename_variables,[],[14])).
% 97.93/98.00 cnf(133,plain,
% 97.93/98.00 (~P6(a58,x1331,a7)),
% 97.93/98.00 inference(scs_inference,[],[8,14,111,114,117,120,128,131,11,21,24,25,26,42,15,53,54,55])).
% 97.93/98.00 cnf(134,plain,
% 97.93/98.00 (~P1(x1341,a58)),
% 97.93/98.00 inference(rename_variables,[],[14])).
% 97.93/98.00 cnf(136,plain,
% 97.93/98.00 (~P6(a58,x1361,a81)),
% 97.93/98.00 inference(scs_inference,[],[8,14,111,114,117,120,128,131,134,11,21,24,25,26,42,15,53,54,55,56])).
% 97.93/98.00 cnf(137,plain,
% 97.93/98.00 (~P1(x1371,a58)),
% 97.93/98.00 inference(rename_variables,[],[14])).
% 97.93/98.00 cnf(140,plain,
% 97.93/98.00 (~P1(x1401,a58)),
% 97.93/98.00 inference(rename_variables,[],[14])).
% 97.93/98.00 cnf(142,plain,
% 97.93/98.00 (~P6(x1421,a58,a90)),
% 97.93/98.00 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])).
% 97.93/98.00 cnf(143,plain,
% 97.93/98.00 (~P1(x1431,a58)),
% 97.93/98.00 inference(rename_variables,[],[14])).
% 97.93/98.00 cnf(145,plain,
% 97.93/98.00 (~P6(a58,x1451,a75)),
% 97.93/98.00 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])).
% 97.93/98.00 cnf(146,plain,
% 97.93/98.00 (~P1(x1461,a58)),
% 97.93/98.01 inference(rename_variables,[],[14])).
% 97.93/98.01 cnf(148,plain,
% 97.93/98.01 (~P6(a58,x1481,a87)),
% 97.93/98.01 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])).
% 97.93/98.01 cnf(149,plain,
% 97.93/98.01 (~P1(x1491,a58)),
% 97.93/98.01 inference(rename_variables,[],[14])).
% 97.93/98.01 cnf(152,plain,
% 97.93/98.01 (~P1(x1521,a58)),
% 97.93/98.01 inference(rename_variables,[],[14])).
% 97.93/98.01 cnf(154,plain,
% 97.93/98.01 (~P6(x1541,a58,a91)),
% 97.93/98.01 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])).
% 97.93/98.01 cnf(155,plain,
% 97.93/98.01 (~P1(x1551,a58)),
% 97.93/98.01 inference(rename_variables,[],[14])).
% 97.93/98.01 cnf(157,plain,
% 97.93/98.01 (~P6(x1571,a58,a83)),
% 97.93/98.01 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])).
% 97.93/98.01 cnf(158,plain,
% 97.93/98.01 (~P1(x1581,a58)),
% 97.93/98.01 inference(rename_variables,[],[14])).
% 97.93/98.01 cnf(160,plain,
% 97.93/98.01 (~P6(x1601,a58,a89)),
% 97.93/98.01 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])).
% 97.93/98.01 cnf(161,plain,
% 97.93/98.01 (~P1(x1611,a58)),
% 97.93/98.01 inference(rename_variables,[],[14])).
% 97.93/98.01 cnf(163,plain,
% 97.93/98.01 (~P6(a58,x1631,a6)),
% 97.93/98.01 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])).
% 97.93/98.01 cnf(164,plain,
% 97.93/98.01 (~P1(x1641,a58)),
% 97.93/98.01 inference(rename_variables,[],[14])).
% 97.93/98.01 cnf(166,plain,
% 97.93/98.01 (~P6(x1661,a58,a79)),
% 97.93/98.01 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])).
% 97.93/98.01 cnf(167,plain,
% 97.93/98.01 (~P1(x1671,a58)),
% 97.93/98.01 inference(rename_variables,[],[14])).
% 97.93/98.01 cnf(169,plain,
% 97.93/98.01 (~P6(a58,x1691,a79)),
% 97.93/98.01 inference(scs_inference,[],[8,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])).
% 97.93/98.01 cnf(170,plain,
% 97.93/98.01 (~P1(x1701,a58)),
% 97.93/98.01 inference(rename_variables,[],[14])).
% 97.93/98.01 cnf(172,plain,
% 97.93/98.01 (~P6(a3,x1721,a90)),
% 97.93/98.01 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])).
% 97.93/98.01 cnf(173,plain,
% 97.93/98.01 (P1(x1731,a3)),
% 97.93/98.01 inference(rename_variables,[],[8])).
% 97.93/98.01 cnf(175,plain,
% 97.93/98.01 (~P6(a3,x1751,a75)),
% 97.93/98.01 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])).
% 97.93/98.01 cnf(176,plain,
% 97.93/98.01 (P1(x1761,a3)),
% 97.93/98.01 inference(rename_variables,[],[8])).
% 97.93/98.01 cnf(178,plain,
% 97.93/98.01 (~P6(a3,x1781,a87)),
% 97.93/98.01 inference(scs_inference,[],[8,123,173,176,14,111,114,117,120,128,131,134,137,140,143,146,149,152,155,158,161,164,167,11,21,24,25,26,42,15,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,82,83,84])).
% 97.93/98.01 cnf(179,plain,
% 97.93/98.01 (P1(x1791,a3)),
% 97.93/98.01 inference(rename_variables,[],[8])).
% 97.93/98.01 cnf(181,plain,
% 97.93/98.01 (~P6(a3,x1811,a91)),
% 97.93/98.01 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])).
% 97.93/98.01 cnf(182,plain,
% 97.93/98.01 (P1(x1821,a3)),
% 97.93/98.01 inference(rename_variables,[],[8])).
% 97.93/98.01 cnf(185,plain,
% 97.93/98.01 (P1(x1851,a3)),
% 97.93/98.01 inference(rename_variables,[],[8])).
% 97.93/98.01 cnf(187,plain,
% 97.93/98.01 (~P6(x1871,a3,a89)),
% 97.93/98.01 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])).
% 97.93/98.01 cnf(188,plain,
% 97.93/98.01 (P1(x1881,a3)),
% 97.93/98.01 inference(rename_variables,[],[8])).
% 97.93/98.01 cnf(190,plain,
% 97.93/98.01 (P4(a5,a82)),
% 97.93/98.01 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])).
% 97.93/98.01 cnf(194,plain,
% 97.93/98.01 (P6(a58,a3,a85)),
% 97.93/98.01 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])).
% 97.93/98.01 cnf(195,plain,
% 97.93/98.01 (~P1(x1951,a58)),
% 97.93/98.01 inference(rename_variables,[],[14])).
% 97.93/98.01 cnf(196,plain,
% 97.93/98.01 (P1(x1961,a3)),
% 97.93/98.01 inference(rename_variables,[],[8])).
% 97.93/98.01 cnf(198,plain,
% 97.93/98.01 (~P6(a3,a58,a4)),
% 97.93/98.01 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])).
% 97.93/98.01 cnf(199,plain,
% 97.93/98.01 (~P1(x1991,a58)),
% 97.93/98.01 inference(rename_variables,[],[14])).
% 97.93/98.01 cnf(201,plain,
% 97.93/98.01 (~P6(a58,a3,a4)),
% 97.93/98.01 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])).
% 97.93/98.01 cnf(202,plain,
% 97.93/98.01 (~P1(x2021,a58)),
% 97.93/98.01 inference(rename_variables,[],[14])).
% 97.93/98.01 cnf(210,plain,
% 97.93/98.01 (P6(a3,a3,a7)),
% 97.93/98.01 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])).
% 97.93/98.01 cnf(211,plain,
% 97.93/98.01 (P1(x2111,a3)),
% 97.93/98.01 inference(rename_variables,[],[8])).
% 97.93/98.01 cnf(212,plain,
% 97.93/98.01 (P1(x2121,a3)),
% 97.93/98.01 inference(rename_variables,[],[8])).
% 97.93/98.01 cnf(214,plain,
% 97.93/98.01 (P6(a3,a3,a84)),
% 97.93/98.01 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])).
% 97.93/98.01 cnf(215,plain,
% 97.93/98.01 (P1(x2151,a3)),
% 97.93/98.01 inference(rename_variables,[],[8])).
% 97.93/98.01 cnf(218,plain,
% 97.93/98.01 (P6(a3,x2181,a88)+~P1(f43(a3,x2181),f74(x2181))),
% 97.93/98.01 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])).
% 97.93/98.01 cnf(222,plain,
% 97.93/98.01 (~P6(x2221,a58,a88)+P6(a3,a58,a88)),
% 97.93/98.01 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])).
% 97.93/98.01 cnf(229,plain,
% 97.93/98.01 (P3(a5,a86)),
% 97.93/98.01 inference(scs_inference,[],[110,113,100])).
% 97.93/98.01 cnf(230,plain,
% 97.93/98.01 (P6(x2301,a58,a86)),
% 97.93/98.01 inference(rename_variables,[],[113])).
% 97.93/98.01 cnf(231,plain,
% 97.93/98.01 (P6(a58,x2311,a5)),
% 97.93/98.01 inference(rename_variables,[],[110])).
% 97.93/98.01 cnf(233,plain,
% 97.93/98.01 (~P6(a2,a58,a4)),
% 97.93/98.01 inference(scs_inference,[],[110,113,1,14,100,80])).
% 97.93/98.01 cnf(234,plain,
% 97.93/98.01 (~P1(x2341,a58)),
% 97.93/98.01 inference(rename_variables,[],[14])).
% 97.93/98.01 cnf(237,plain,
% 97.93/98.01 (~P6(a58,x2371,a7)),
% 97.93/98.01 inference(rename_variables,[],[133])).
% 97.93/98.01 cnf(240,plain,
% 97.93/98.01 (~P6(a58,a2,a4)),
% 97.93/98.01 inference(scs_inference,[],[110,113,127,133,1,14,234,100,80,75,81])).
% 97.93/98.01 cnf(243,plain,
% 97.93/98.01 (P4(a5,a7)),
% 97.93/98.01 inference(scs_inference,[],[110,231,113,127,133,237,1,14,234,100,80,75,81,91])).
% 97.93/98.01 cnf(246,plain,
% 97.93/98.01 (~P5(a5,a86)),
% 97.93/98.01 inference(scs_inference,[],[110,231,113,230,127,133,237,1,14,234,100,80,75,81,91,104])).
% 97.93/98.01 cnf(247,plain,
% 97.93/98.01 (P6(x2471,a58,a86)),
% 97.93/98.01 inference(rename_variables,[],[113])).
% 97.93/98.01 cnf(248,plain,
% 97.93/98.01 (P6(a58,x2481,a5)),
% 97.93/98.01 inference(rename_variables,[],[110])).
% 97.93/98.01 cnf(254,plain,
% 97.93/98.01 (P6(a3,x2541,a84)+~P1(f24(a3,x2541),x2541)),
% 97.93/98.01 inference(scs_inference,[],[110,231,248,113,230,247,127,133,237,1,8,14,234,100,80,75,81,91,104,105,98])).
% 97.93/98.01 cnf(278,plain,
% 97.93/98.01 (~P6(a56,a58,a4)),
% 97.93/98.01 inference(scs_inference,[],[2,14,80])).
% 97.93/98.01 cnf(279,plain,
% 97.93/98.01 (~P1(x2791,a58)),
% 97.93/98.01 inference(rename_variables,[],[14])).
% 97.93/98.01 cnf(281,plain,
% 97.93/98.01 (P3(a85,a85)),
% 97.93/98.01 inference(scs_inference,[],[194,2,14,80,100])).
% 97.93/98.01 cnf(285,plain,
% 97.93/98.01 (~P6(a58,a56,a4)),
% 97.93/98.01 inference(scs_inference,[],[194,198,2,14,279,80,100,75,81])).
% 97.93/98.01 cnf(288,plain,
% 97.93/98.01 (~P5(a85,a85)),
% 97.93/98.01 inference(scs_inference,[],[194,198,2,14,279,80,100,75,81,104])).
% 97.93/98.01 cnf(290,plain,
% 97.93/98.01 (P4(a86,a4)),
% 97.93/98.01 inference(scs_inference,[],[194,113,198,2,14,279,80,100,75,81,104,91])).
% 97.93/98.01 cnf(295,plain,
% 97.93/98.01 (P3(a5,a80)),
% 97.93/98.01 inference(scs_inference,[],[110,116,100])).
% 97.93/98.01 cnf(296,plain,
% 97.93/98.01 (P6(a58,x2961,a80)),
% 97.93/98.01 inference(rename_variables,[],[116])).
% 97.93/98.01 cnf(301,plain,
% 97.93/98.01 (P4(a5,a4)),
% 97.93/98.01 inference(scs_inference,[],[110,116,130,201,136,100,75,91])).
% 97.93/98.01 cnf(302,plain,
% 97.93/98.01 (P6(a58,x3021,a5)),
% 97.93/98.01 inference(rename_variables,[],[110])).
% 97.93/98.01 cnf(304,plain,
% 97.93/98.01 (~P5(a5,a80)),
% 97.93/98.01 inference(scs_inference,[],[110,302,116,296,130,201,136,100,75,91,104])).
% 97.93/98.01 cnf(305,plain,
% 97.93/98.01 (P6(a58,x3051,a80)),
% 97.93/98.01 inference(rename_variables,[],[116])).
% 97.93/98.01 cnf(307,plain,
% 97.93/98.01 (~P7(a5,a80)),
% 97.93/98.01 inference(scs_inference,[],[110,302,116,296,305,130,201,136,100,75,91,104,105])).
% 97.93/98.01 cnf(310,plain,
% 97.93/98.01 (P3(a5,a73)),
% 97.93/98.01 inference(scs_inference,[],[110,119,100])).
% 97.93/98.01 cnf(311,plain,
% 97.93/98.01 (P6(a58,x3111,a73)),
% 97.93/98.01 inference(rename_variables,[],[119])).
% 97.93/98.01 cnf(316,plain,
% 97.93/98.01 (~P5(a5,a73)),
% 97.93/98.01 inference(scs_inference,[],[110,119,311,201,130,100,75,104])).
% 97.93/98.01 cnf(319,plain,
% 97.93/98.01 (P4(a5,a90)),
% 97.93/98.01 inference(scs_inference,[],[110,119,311,201,130,142,100,75,104,91])).
% 97.93/98.01 cnf(326,plain,
% 97.93/98.01 (P3(a84,a84)),
% 97.93/98.01 inference(scs_inference,[],[214,100])).
% 97.93/98.01 cnf(329,plain,
% 97.93/98.01 (~P6(a58,x3291,a87)),
% 97.93/98.01 inference(rename_variables,[],[148])).
% 97.93/98.01 cnf(331,plain,
% 97.93/98.01 (P4(a5,a87)),
% 97.93/98.01 inference(scs_inference,[],[110,214,201,148,329,100,75,91])).
% 97.93/98.01 cnf(334,plain,
% 97.93/98.01 (~P5(a84,a84)),
% 97.93/98.01 inference(scs_inference,[],[110,214,201,148,329,100,75,91,104])).
% 97.93/98.01 cnf(338,plain,
% 97.93/98.01 (~P7(a91,a4)),
% 97.93/98.01 inference(scs_inference,[],[198,154,75])).
% 97.93/98.01 cnf(339,plain,
% 97.93/98.01 (~P6(x3391,a58,a91)),
% 97.93/98.01 inference(rename_variables,[],[154])).
% 97.93/98.01 cnf(341,plain,
% 97.93/98.01 (P3(a7,a7)),
% 97.93/98.01 inference(scs_inference,[],[210,198,154,75,100])).
% 97.93/98.01 cnf(343,plain,
% 97.93/98.01 (~P5(a7,a7)),
% 97.93/98.01 inference(scs_inference,[],[210,198,154,75,100,104])).
% 97.93/98.01 cnf(345,plain,
% 97.93/98.01 (P4(a5,a91)),
% 97.93/98.01 inference(scs_inference,[],[110,210,198,154,339,75,100,104,91])).
% 97.93/98.01 cnf(352,plain,
% 97.93/98.01 (~P6(x3521,a58,a83)),
% 97.93/98.01 inference(rename_variables,[],[157])).
% 97.93/98.01 cnf(355,plain,
% 97.93/98.01 (P4(a5,a83)),
% 97.93/98.01 inference(scs_inference,[],[110,130,157,352,75,91])).
% 97.93/98.01 cnf(360,plain,
% 97.93/98.01 (~P6(x3601,a58,a89)),
% 97.93/98.01 inference(rename_variables,[],[160])).
% 97.93/98.01 cnf(362,plain,
% 97.93/98.01 (P4(a5,a89)),
% 97.93/98.01 inference(scs_inference,[],[110,198,160,360,75,91])).
% 97.93/98.01 cnf(367,plain,
% 97.93/98.01 (~P6(a58,x3671,a6)),
% 97.93/98.01 inference(rename_variables,[],[163])).
% 97.93/98.01 cnf(369,plain,
% 97.93/98.01 (P4(a5,a6)),
% 97.93/98.01 inference(scs_inference,[],[110,201,163,367,75,91])).
% 97.93/98.01 cnf(373,plain,
% 97.93/98.01 (~P6(x3731,a58,a79)),
% 97.93/98.01 inference(rename_variables,[],[166])).
% 97.93/98.01 cnf(376,plain,
% 97.93/98.01 (P4(a5,a79)),
% 97.93/98.01 inference(scs_inference,[],[110,130,166,373,75,91])).
% 97.93/98.01 cnf(383,plain,
% 97.93/98.01 (P4(a73,a90)),
% 97.93/98.01 inference(scs_inference,[],[122,201,169,172,75,91])).
% 97.93/98.01 cnf(395,plain,
% 97.93/98.01 (P4(a73,a91)),
% 97.93/98.01 inference(scs_inference,[],[122,181,91])).
% 97.93/98.01 cnf(406,plain,
% 97.93/98.01 (P4(a5,a81)),
% 97.93/98.01 inference(scs_inference,[],[110,130,187,136,75,91])).
% 97.93/98.01 cnf(409,plain,
% 97.93/98.01 (P4(a5,a75)),
% 97.93/98.01 inference(scs_inference,[],[110,145,91])).
% 97.93/98.01 cnf(423,plain,
% 97.93/98.01 (P4(a73,a75)),
% 97.93/98.01 inference(scs_inference,[],[122,175,91])).
% 97.93/98.01 cnf(433,plain,
% 97.93/98.01 (P4(a86,a91)),
% 97.93/98.01 inference(scs_inference,[],[113,201,181,136,75,91])).
% 97.93/98.01 cnf(437,plain,
% 97.93/98.01 (P4(a73,a87)),
% 97.93/98.01 inference(scs_inference,[],[122,178,91])).
% 97.93/98.01 cnf(450,plain,
% 97.93/98.01 (P4(a7,a75)),
% 97.93/98.01 inference(scs_inference,[],[210,175,91])).
% 97.93/98.01 cnf(456,plain,
% 97.93/98.01 (P4(a86,a75)),
% 97.93/98.01 inference(scs_inference,[],[113,175,91])).
% 97.93/98.01 cnf(460,plain,
% 97.93/98.01 (~P1(a61,f74(a65))),
% 97.93/98.01 inference(scs_inference,[],[4,20,15])).
% 97.93/98.01 cnf(461,plain,
% 97.93/98.01 (~P6(x4611,a65,a88)),
% 97.93/98.01 inference(scs_inference,[],[460,35])).
% 97.93/98.01 cnf(465,plain,
% 97.93/98.01 (~P1(f43(a3,a65),f74(a65))),
% 97.93/98.01 inference(scs_inference,[],[8,460,35,17,101])).
% 97.93/98.01 cnf(484,plain,
% 97.93/98.01 (P6(a65,x4841,a86)),
% 97.93/98.01 inference(scs_inference,[],[465,23,17])).
% 97.93/98.01 cnf(485,plain,
% 97.93/98.01 (P1(f43(a3,a65),a65)),
% 97.93/98.01 inference(scs_inference,[],[465,17])).
% 97.93/98.01 cnf(487,plain,
% 97.93/98.01 (P3(a73,a86)),
% 97.93/98.01 inference(scs_inference,[],[122,484,465,17,100])).
% 97.93/98.01 cnf(488,plain,
% 97.93/98.01 (P6(a65,x4881,a86)),
% 97.93/98.01 inference(rename_variables,[],[484])).
% 97.93/98.01 cnf(489,plain,
% 97.93/98.01 (P6(x4891,a3,a73)),
% 97.93/98.01 inference(rename_variables,[],[122])).
% 97.93/98.01 cnf(491,plain,
% 97.93/98.01 (~P5(a73,a86)),
% 97.93/98.01 inference(scs_inference,[],[122,489,484,488,465,17,100,104])).
% 97.93/98.01 cnf(492,plain,
% 97.93/98.01 (P6(a65,x4921,a86)),
% 97.93/98.01 inference(rename_variables,[],[484])).
% 97.93/98.01 cnf(493,plain,
% 97.93/98.01 (P6(x4931,a3,a73)),
% 97.93/98.01 inference(rename_variables,[],[122])).
% 97.93/98.01 cnf(500,plain,
% 97.93/98.01 (~P6(x5001,a65,a88)),
% 97.93/98.01 inference(rename_variables,[],[461])).
% 97.93/98.01 cnf(503,plain,
% 97.93/98.01 (P4(a5,a88)),
% 97.93/98.01 inference(scs_inference,[],[110,122,489,493,484,488,492,465,130,461,500,17,100,104,105,75,91])).
% 97.93/98.01 cnf(507,plain,
% 97.93/98.01 (P4(a7,a87)),
% 97.93/98.01 inference(scs_inference,[],[210,178,91])).
% 97.93/98.01 cnf(513,plain,
% 97.93/98.01 (~P6(x5131,a58,a81)),
% 97.93/98.01 inference(scs_inference,[],[110,27,36])).
% 97.93/98.01 cnf(514,plain,
% 97.93/98.01 (P4(a7,a90)),
% 97.93/98.01 inference(scs_inference,[],[210,172,91])).
% 97.93/98.01 cnf(520,plain,
% 97.93/98.01 (P4(a7,a91)),
% 97.93/98.01 inference(scs_inference,[],[210,181,91])).
% 97.93/98.01 cnf(526,plain,
% 97.93/98.01 (~P6(x5261,a58,a87)),
% 97.93/98.01 inference(scs_inference,[],[194,29,38])).
% 97.93/98.01 cnf(527,plain,
% 97.93/98.01 (~P6(f74(a65),x5271,a88)),
% 97.93/98.01 inference(scs_inference,[],[461,32,218])).
% 97.93/98.01 cnf(528,plain,
% 97.93/98.01 (~P6(a59,a58,a4)),
% 97.93/98.01 inference(scs_inference,[],[3,14,80])).
% 97.93/98.01 cnf(529,plain,
% 97.93/98.01 (~P1(x5291,a58)),
% 97.93/98.01 inference(rename_variables,[],[14])).
% 97.93/98.01 cnf(531,plain,
% 97.93/98.01 (~P6(a58,a59,a4)),
% 97.93/98.01 inference(scs_inference,[],[3,14,529,80,81])).
% 97.93/98.01 cnf(534,plain,
% 97.93/98.01 (P4(a73,a88)),
% 97.93/98.01 inference(scs_inference,[],[3,122,14,529,527,80,81,91])).
% 97.93/98.01 cnf(538,plain,
% 97.93/98.01 (~P6(a3,x5381,a83)),
% 97.93/98.01 inference(scs_inference,[],[214,37,28])).
% 97.93/98.01 cnf(543,plain,
% 97.93/98.01 (P4(a7,a83)),
% 97.93/98.01 inference(scs_inference,[],[210,513,538,527,75,91])).
% 97.93/98.01 cnf(546,plain,
% 97.93/98.01 (~P6(a3,x5461,a89)),
% 97.93/98.01 inference(scs_inference,[],[194,39,30])).
% 97.93/98.01 cnf(551,plain,
% 97.93/98.01 (P4(a7,a89)),
% 97.93/98.01 inference(scs_inference,[],[210,526,546,527,75,91])).
% 97.93/98.01 cnf(560,plain,
% 97.93/98.01 (~P6(a62,a58,a4)),
% 97.93/98.01 inference(scs_inference,[],[4,14,80])).
% 97.93/98.01 cnf(561,plain,
% 97.93/98.01 (~P1(x5611,a58)),
% 97.93/98.01 inference(rename_variables,[],[14])).
% 97.93/98.01 cnf(563,plain,
% 97.93/98.01 (~P6(a58,a62,a4)),
% 97.93/98.01 inference(scs_inference,[],[4,14,561,80,81])).
% 97.93/98.01 cnf(566,plain,
% 97.93/98.01 (~P2(a88,a4)+~P6(x5661,a58,a88)),
% 97.93/98.01 inference(scs_inference,[],[198,222,94])).
% 97.93/98.01 cnf(567,plain,
% 97.93/98.01 (~P1(f43(a3,a58),f74(a58))+~P2(a88,a4)),
% 97.93/98.01 inference(scs_inference,[],[566,218])).
% 97.93/98.01 cnf(568,plain,
% 97.93/98.01 (~P6(a58,a65,a4)),
% 97.93/98.01 inference(scs_inference,[],[5,14,81])).
% 97.93/98.01 cnf(569,plain,
% 97.93/98.01 (~P1(x5691,a58)),
% 97.93/98.01 inference(rename_variables,[],[14])).
% 97.93/98.01 cnf(571,plain,
% 97.93/98.01 (~P6(a65,a58,a4)),
% 97.93/98.01 inference(scs_inference,[],[5,14,569,81,80])).
% 97.93/98.01 cnf(575,plain,
% 97.93/98.01 (P6(a3,f74(a58),a84)),
% 97.93/98.01 inference(scs_inference,[],[14,254,17])).
% 97.93/98.01 cnf(576,plain,
% 97.93/98.01 (P1(x5761,f74(a58))),
% 97.93/98.02 inference(scs_inference,[],[575,28])).
% 97.93/98.02 cnf(580,plain,
% 97.93/98.02 (~P6(a69,a58,a4)),
% 97.93/98.02 inference(scs_inference,[],[6,575,14,28,84,80])).
% 97.93/98.02 cnf(581,plain,
% 97.93/98.02 (~P1(x5811,a58)),
% 97.93/98.02 inference(rename_variables,[],[14])).
% 97.93/98.02 cnf(583,plain,
% 97.93/98.02 (~P6(a58,a69,a4)),
% 97.93/98.02 inference(scs_inference,[],[6,575,14,581,28,84,80,81])).
% 97.93/98.02 cnf(586,plain,
% 97.93/98.02 (~P2(a88,a4)),
% 97.93/98.02 inference(scs_inference,[],[576,567])).
% 97.93/98.02 cnf(589,plain,
% 97.93/98.02 (P1(x5891,f74(a58))),
% 97.93/98.02 inference(rename_variables,[],[576])).
% 97.93/98.02 cnf(592,plain,
% 97.93/98.02 (P1(x5921,f74(a58))),
% 97.93/98.02 inference(rename_variables,[],[576])).
% 97.93/98.02 cnf(594,plain,
% 97.93/98.02 (~P6(x5941,f74(a58),a91)),
% 97.93/98.02 inference(scs_inference,[],[576,589,592,82,87,86])).
% 97.93/98.02 cnf(595,plain,
% 97.93/98.02 (P1(x5951,f74(a58))),
% 97.93/98.02 inference(rename_variables,[],[576])).
% 97.93/98.02 cnf(598,plain,
% 97.93/98.02 (P1(x5981,f74(a58))),
% 97.93/98.02 inference(rename_variables,[],[576])).
% 97.93/98.02 cnf(600,plain,
% 97.93/98.02 (P6(x6001,f74(a58),a73)),
% 97.93/98.02 inference(scs_inference,[],[576,589,592,595,598,82,87,86,83,42])).
% 97.93/98.02 cnf(601,plain,
% 97.93/98.02 (P1(x6011,f74(a58))),
% 97.93/98.02 inference(rename_variables,[],[576])).
% 97.93/98.02 cnf(604,plain,
% 97.93/98.02 (P1(x6041,f74(a58))),
% 97.93/98.02 inference(rename_variables,[],[576])).
% 97.93/98.02 cnf(606,plain,
% 97.93/98.02 (P6(a3,a58,a88)),
% 97.93/98.02 inference(scs_inference,[],[8,576,589,592,595,598,601,604,82,87,86,83,42,85,101])).
% 97.93/98.02 cnf(607,plain,
% 97.93/98.02 (P1(x6071,a3)),
% 97.93/98.02 inference(rename_variables,[],[8])).
% 97.93/98.02 cnf(608,plain,
% 97.93/98.02 (P1(x6081,f74(a58))),
% 97.93/98.02 inference(rename_variables,[],[576])).
% 97.93/98.02 cnf(614,plain,
% 97.93/98.02 (P3(a88,a88)),
% 97.93/98.02 inference(scs_inference,[],[8,607,576,589,592,595,598,601,604,608,82,87,86,83,42,85,101,98,100])).
% 97.93/98.02 cnf(616,plain,
% 97.93/98.02 (~P5(a88,a88)),
% 97.93/98.02 inference(scs_inference,[],[8,607,576,589,592,595,598,601,604,608,82,87,86,83,42,85,101,98,100,104])).
% 97.93/98.02 cnf(635,plain,
% 97.93/98.02 (P6(f48(a5,a5),f51(a5,a5),a5)),
% 97.93/98.02 inference(scs_inference,[],[110,51,104])).
% 97.93/98.02 cnf(636,plain,
% 97.93/98.02 (~P1(x6361,f48(a5,a5))),
% 97.93/98.02 inference(scs_inference,[],[635,36])).
% 97.93/98.02 cnf(647,plain,
% 97.93/98.02 (P1(x6471,f48(a84,a84))),
% 97.93/98.02 inference(scs_inference,[],[334,52,31])).
% 97.93/98.02 cnf(649,plain,
% 97.93/98.02 (~P1(x6491,f48(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[636])).
% 97.93/98.02 cnf(652,plain,
% 97.93/98.02 (~P1(x6521,f48(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[636])).
% 97.93/98.02 cnf(655,plain,
% 97.93/98.02 (~P1(x6551,f48(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[636])).
% 97.93/98.02 cnf(658,plain,
% 97.93/98.02 (~P1(x6581,f48(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[636])).
% 97.93/98.02 cnf(661,plain,
% 97.93/98.02 (P1(x6611,f48(a84,a84))),
% 97.93/98.02 inference(rename_variables,[],[647])).
% 97.93/98.02 cnf(664,plain,
% 97.93/98.02 (~P1(x6641,f48(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[636])).
% 97.93/98.02 cnf(667,plain,
% 97.93/98.02 (~P1(x6671,f48(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[636])).
% 97.93/98.02 cnf(670,plain,
% 97.93/98.02 (~P1(x6701,f48(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[636])).
% 97.93/98.02 cnf(672,plain,
% 97.93/98.02 (P6(f48(a5,a5),x6721,a73)),
% 97.93/98.02 inference(scs_inference,[],[636,649,652,655,658,664,667,670,647,56,24,66,61,84,65,64,60,26])).
% 97.93/98.02 cnf(673,plain,
% 97.93/98.02 (~P1(x6731,f48(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[636])).
% 97.93/98.02 cnf(676,plain,
% 97.93/98.02 (~P1(x6761,f48(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[636])).
% 97.93/98.02 cnf(678,plain,
% 97.93/98.02 (~P6(x6781,f48(a84,a84),a89)),
% 97.93/98.02 inference(scs_inference,[],[636,649,652,655,658,664,667,670,673,647,661,56,24,66,61,84,65,64,60,26,59,87])).
% 97.93/98.02 cnf(679,plain,
% 97.93/98.02 (P1(x6791,f48(a84,a84))),
% 97.93/98.02 inference(rename_variables,[],[647])).
% 97.93/98.02 cnf(682,plain,
% 97.93/98.02 (~P1(x6821,f48(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[636])).
% 97.93/98.02 cnf(685,plain,
% 97.93/98.02 (~P1(x6851,f48(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[636])).
% 97.93/98.02 cnf(688,plain,
% 97.93/98.02 (~P1(x6881,f48(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[636])).
% 97.93/98.02 cnf(691,plain,
% 97.93/98.02 (~P1(x6911,f48(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[636])).
% 97.93/98.02 cnf(694,plain,
% 97.93/98.02 (P1(x6941,f48(a84,a84))),
% 97.93/98.02 inference(rename_variables,[],[647])).
% 97.93/98.02 cnf(697,plain,
% 97.93/98.02 (~P1(x6971,f48(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[636])).
% 97.93/98.02 cnf(700,plain,
% 97.93/98.02 (~P1(x7001,f48(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[636])).
% 97.93/98.02 cnf(703,plain,
% 97.93/98.02 (~P1(x7031,f48(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[636])).
% 97.93/98.02 cnf(706,plain,
% 97.93/98.02 (~P1(x7061,f48(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[636])).
% 97.93/98.02 cnf(709,plain,
% 97.93/98.02 (P1(x7091,f48(a84,a84))),
% 97.93/98.02 inference(rename_variables,[],[647])).
% 97.93/98.02 cnf(712,plain,
% 97.93/98.02 (~P1(x7121,f48(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[636])).
% 97.93/98.02 cnf(715,plain,
% 97.93/98.02 (P1(x7151,f48(a84,a84))),
% 97.93/98.02 inference(rename_variables,[],[647])).
% 97.93/98.02 cnf(718,plain,
% 97.93/98.02 (P1(x7181,f48(a84,a84))),
% 97.93/98.02 inference(rename_variables,[],[647])).
% 97.93/98.02 cnf(721,plain,
% 97.93/98.02 (P1(x7211,f48(a84,a84))),
% 97.93/98.02 inference(rename_variables,[],[647])).
% 97.93/98.02 cnf(723,plain,
% 97.93/98.02 (P6(a58,f48(a5,a5),a4)),
% 97.93/98.02 inference(scs_inference,[],[14,636,649,652,655,658,664,667,670,673,676,682,685,688,691,697,700,703,706,712,647,661,679,694,709,715,718,56,24,66,61,84,65,64,60,26,59,87,21,55,25,62,82,58,57,63,54,83,53,86,42,85,76])).
% 97.93/98.02 cnf(725,plain,
% 97.93/98.02 (~P1(x7251,f48(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[636])).
% 97.93/98.02 cnf(728,plain,
% 97.93/98.02 (~P1(x7281,f48(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[636])).
% 97.93/98.02 cnf(729,plain,
% 97.93/98.02 (P1(x7291,a3)),
% 97.93/98.02 inference(rename_variables,[],[8])).
% 97.93/98.02 cnf(734,plain,
% 97.93/98.02 (P3(a73,a73)),
% 97.93/98.02 inference(scs_inference,[],[6,122,8,14,636,649,652,655,658,664,667,670,673,676,682,685,688,691,697,700,703,706,712,725,728,647,661,679,694,709,715,718,56,24,66,61,84,65,64,60,26,59,87,21,55,25,62,82,58,57,63,54,83,53,86,42,85,76,93,81,100])).
% 97.93/98.02 cnf(738,plain,
% 97.93/98.02 (P1(x7381,f48(a84,a84))),
% 97.93/98.02 inference(rename_variables,[],[647])).
% 97.93/98.02 cnf(745,plain,
% 97.93/98.02 (~P5(a73,a73)),
% 97.93/98.02 inference(scs_inference,[],[6,122,8,729,14,576,636,649,652,655,658,664,667,670,673,676,682,685,688,691,697,700,703,706,712,725,728,647,661,679,694,709,715,718,721,738,56,24,66,61,84,65,64,60,26,59,87,21,55,25,62,82,58,57,63,54,83,53,86,42,85,76,93,81,100,98,101,104])).
% 97.93/98.02 cnf(778,plain,
% 97.93/98.02 (P6(f45(a5,a5),f46(a5,a5),a5)),
% 97.93/98.02 inference(scs_inference,[],[110,69,100])).
% 97.93/98.02 cnf(779,plain,
% 97.93/98.02 (~P1(x7791,f45(a5,a5))),
% 97.93/98.02 inference(scs_inference,[],[778,36])).
% 97.93/98.02 cnf(787,plain,
% 97.93/98.02 (P3(a4,a4)),
% 97.93/98.02 inference(scs_inference,[],[778,723,14,636,36,59,76,100])).
% 97.93/98.02 cnf(789,plain,
% 97.93/98.02 (~P5(a4,a4)),
% 97.93/98.02 inference(scs_inference,[],[778,723,14,636,36,59,76,100,104])).
% 97.93/98.02 cnf(809,plain,
% 97.93/98.02 (~P1(x8091,f45(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[779])).
% 97.93/98.02 cnf(812,plain,
% 97.93/98.02 (~P1(x8121,f45(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[779])).
% 97.93/98.02 cnf(815,plain,
% 97.93/98.02 (~P1(x8151,f45(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[779])).
% 97.93/98.02 cnf(818,plain,
% 97.93/98.02 (~P1(x8181,f45(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[779])).
% 97.93/98.02 cnf(821,plain,
% 97.93/98.02 (~P1(x8211,f45(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[779])).
% 97.93/98.02 cnf(824,plain,
% 97.93/98.02 (~P1(x8241,f45(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[779])).
% 97.93/98.02 cnf(827,plain,
% 97.93/98.02 (~P1(x8271,f45(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[779])).
% 97.93/98.02 cnf(830,plain,
% 97.93/98.02 (~P1(x8301,f45(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[779])).
% 97.93/98.02 cnf(833,plain,
% 97.93/98.02 (~P1(x8331,f45(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[779])).
% 97.93/98.02 cnf(835,plain,
% 97.93/98.02 (P6(f45(a5,a5),x8351,a80)),
% 97.93/98.02 inference(scs_inference,[],[779,809,812,815,818,821,824,827,830,833,68,24,56,61,66,62,65,26,55,25])).
% 97.93/98.02 cnf(836,plain,
% 97.93/98.02 (~P1(x8361,f45(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[779])).
% 97.93/98.02 cnf(839,plain,
% 97.93/98.02 (~P1(x8391,f45(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[779])).
% 97.93/98.02 cnf(842,plain,
% 97.93/98.02 (~P1(x8421,f45(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[779])).
% 97.93/98.02 cnf(845,plain,
% 97.93/98.02 (~P1(x8451,f45(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[779])).
% 97.93/98.02 cnf(848,plain,
% 97.93/98.02 (~P1(x8481,f45(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[779])).
% 97.93/98.02 cnf(851,plain,
% 97.93/98.02 (~P1(x8511,f45(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[779])).
% 97.93/98.02 cnf(853,plain,
% 97.93/98.02 (~P6(x8531,f45(a5,a5),a89)),
% 97.93/98.02 inference(scs_inference,[],[779,809,812,815,818,821,824,827,830,833,836,839,842,845,848,851,68,24,56,61,66,62,65,26,55,25,63,57,54,21,53,64])).
% 97.93/98.02 cnf(854,plain,
% 97.93/98.02 (~P1(x8541,f45(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[779])).
% 97.93/98.02 cnf(857,plain,
% 97.93/98.02 (~P1(x8571,f45(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[779])).
% 97.93/98.02 cnf(860,plain,
% 97.93/98.02 (~P1(x8601,f45(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[779])).
% 97.93/98.02 cnf(863,plain,
% 97.93/98.02 (~P1(x8631,f45(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[779])).
% 97.93/98.02 cnf(868,plain,
% 97.93/98.02 (~P1(x8681,f45(a5,a5))),
% 97.93/98.02 inference(rename_variables,[],[779])).
% 97.93/98.02 cnf(873,plain,
% 97.93/98.02 (P3(a73,a80)),
% 97.93/98.02 inference(scs_inference,[],[6,122,8,14,779,809,812,815,818,821,824,827,830,833,836,839,842,845,848,851,854,857,860,863,868,68,24,56,61,66,62,65,26,55,25,63,57,54,21,53,64,60,58,93,76,81,100])).
% 97.93/98.02 cnf(876,plain,
% 97.93/98.02 (~P5(a80,a80)),
% 97.93/98.02 inference(scs_inference,[],[6,122,8,14,779,809,812,815,818,821,824,827,830,833,836,839,842,845,848,851,854,857,860,863,868,68,24,56,61,66,62,65,26,55,25,63,57,54,21,53,64,60,58,93,76,81,100,104])).
% 97.93/98.02 cnf(950,plain,
% 97.93/98.02 (P1(x9501,f74(f46(a88,a88)))),
% 97.93/98.02 inference(scs_inference,[],[614,70,35])).
% 97.93/98.02 cnf(951,plain,
% 97.93/98.02 (~P1(x9511,f46(a88,a88))),
% 97.93/98.02 inference(scs_inference,[],[950,20])).
% 97.93/98.02 cnf(953,plain,
% 97.93/98.02 (P6(x9531,f46(a88,a88),a86)),
% 97.93/98.02 inference(scs_inference,[],[950,20,24])).
% 97.93/98.02 cnf(972,plain,
% 97.93/98.02 (~P1(x9721,f46(a88,a88))),
% 97.93/98.02 inference(rename_variables,[],[951])).
% 97.93/98.02 cnf(975,plain,
% 97.93/98.02 (~P1(x9751,f46(a88,a88))),
% 97.93/98.02 inference(rename_variables,[],[951])).
% 97.93/98.02 cnf(978,plain,
% 97.93/98.02 (~P1(x9781,f46(a88,a88))),
% 97.93/98.02 inference(rename_variables,[],[951])).
% 97.93/98.02 cnf(980,plain,
% 97.93/98.02 (P6(f46(a88,a88),x9801,a80)),
% 97.93/98.02 inference(scs_inference,[],[951,972,975,978,59,68,61,25])).
% 97.93/98.02 cnf(981,plain,
% 97.93/98.02 (~P1(x9811,f46(a88,a88))),
% 97.93/98.02 inference(rename_variables,[],[951])).
% 97.93/98.02 cnf(984,plain,
% 97.93/98.02 (~P1(x9841,f46(a88,a88))),
% 97.93/98.02 inference(rename_variables,[],[951])).
% 97.93/98.02 cnf(986,plain,
% 97.93/98.02 (~P6(f46(a88,a88),x9861,a7)),
% 97.93/98.02 inference(scs_inference,[],[951,972,975,978,981,984,59,68,61,25,56,55])).
% 97.93/98.02 cnf(987,plain,
% 97.93/98.02 (~P1(x9871,f46(a88,a88))),
% 97.93/98.02 inference(rename_variables,[],[951])).
% 97.93/98.02 cnf(990,plain,
% 97.93/98.02 (~P1(x9901,f46(a88,a88))),
% 97.93/98.02 inference(rename_variables,[],[951])).
% 97.93/98.02 cnf(993,plain,
% 97.93/98.02 (~P1(x9931,f46(a88,a88))),
% 97.93/98.02 inference(rename_variables,[],[951])).
% 97.93/98.02 cnf(995,plain,
% 97.93/98.02 (~P6(x9951,f46(a88,a88),a83)),
% 97.93/98.02 inference(scs_inference,[],[951,972,975,978,981,984,987,990,993,59,68,61,25,56,55,66,54,63])).
% 97.93/98.02 cnf(996,plain,
% 97.93/98.02 (~P1(x9961,f46(a88,a88))),
% 97.93/98.02 inference(rename_variables,[],[951])).
% 97.93/98.02 cnf(999,plain,
% 97.93/98.02 (~P1(x9991,f46(a88,a88))),
% 97.93/98.02 inference(rename_variables,[],[951])).
% 97.93/98.02 cnf(1002,plain,
% 97.93/98.02 (~P1(x10021,f46(a88,a88))),
% 97.93/98.02 inference(rename_variables,[],[951])).
% 97.93/98.02 cnf(1005,plain,
% 97.93/98.02 (~P1(x10051,f46(a88,a88))),
% 97.93/98.02 inference(rename_variables,[],[951])).
% 97.93/98.02 cnf(1008,plain,
% 97.93/98.02 (~P1(x10081,f46(a88,a88))),
% 97.93/98.02 inference(rename_variables,[],[951])).
% 97.93/98.02 cnf(1011,plain,
% 97.93/98.02 (~P1(x10111,f46(a88,a88))),
% 97.93/98.02 inference(rename_variables,[],[951])).
% 97.93/98.02 cnf(1014,plain,
% 97.93/98.02 (~P1(x10141,f46(a88,a88))),
% 97.93/98.02 inference(rename_variables,[],[951])).
% 97.93/98.02 cnf(1017,plain,
% 97.93/98.02 (~P1(x10171,f46(a88,a88))),
% 97.93/98.02 inference(rename_variables,[],[951])).
% 97.93/98.02 cnf(1019,plain,
% 97.93/98.02 (~P6(x10191,f46(a88,a88),a90)),
% 97.93/98.02 inference(scs_inference,[],[951,972,975,978,981,984,987,990,993,996,999,1002,1005,1008,1011,1014,1017,59,68,61,25,56,55,66,54,63,57,21,26,62,65,64,53,58])).
% 97.93/98.02 cnf(1020,plain,
% 97.93/98.02 (~P1(x10201,f46(a88,a88))),
% 97.93/98.02 inference(rename_variables,[],[951])).
% 97.93/98.02 cnf(1023,plain,
% 97.93/98.02 (~P1(x10231,f46(a88,a88))),
% 97.93/98.02 inference(rename_variables,[],[951])).
% 97.93/98.02 cnf(1026,plain,
% 97.93/98.02 (~P1(x10261,f46(a88,a88))),
% 97.93/98.02 inference(rename_variables,[],[951])).
% 97.93/98.02 cnf(1030,plain,
% 97.93/98.02 (~P1(x10301,f46(a88,a88))),
% 97.93/98.02 inference(rename_variables,[],[951])).
% 97.93/98.02 cnf(1036,plain,
% 97.93/98.02 (P3(a73,a5)),
% 97.93/98.02 inference(scs_inference,[],[6,122,14,8,951,972,975,978,981,984,987,990,993,996,999,1002,1005,1008,1011,1014,1017,1020,1023,1026,1030,59,68,61,25,56,55,66,54,63,57,21,26,62,65,64,53,58,60,93,76,80,100])).
% 97.93/98.02 cnf(1037,plain,
% 97.93/98.02 (P6(x10371,a3,a73)),
% 97.93/98.02 inference(rename_variables,[],[122])).
% 97.93/98.02 cnf(1043,plain,
% 97.93/98.02 (~P5(a73,a80)),
% 97.93/98.02 inference(scs_inference,[],[6,122,1037,14,8,576,951,972,975,978,981,984,987,990,993,996,999,1002,1005,1008,1011,1014,1017,1020,1023,1026,1030,950,59,68,61,25,56,55,66,54,63,57,21,26,62,65,64,53,58,60,93,76,80,100,101,104])).
% 97.93/98.02 cnf(1044,plain,
% 97.93/98.02 (P6(x10441,a3,a73)),
% 97.93/98.02 inference(rename_variables,[],[122])).
% 97.93/98.02 cnf(1046,plain,
% 97.93/98.02 (P4(a73,a7)),
% 97.93/98.02 inference(scs_inference,[],[6,122,1037,1044,14,8,576,951,972,975,978,981,984,987,990,993,996,999,1002,1005,1008,1011,1014,1017,1020,1023,1026,1030,950,59,68,61,25,56,55,66,54,63,57,21,26,62,65,64,53,58,60,93,76,80,100,101,104,91])).
% 97.93/98.02 cnf(1210,plain,
% 97.93/98.02 (P3(a86,a86)),
% 97.93/98.02 inference(scs_inference,[],[113,100])).
% 97.93/98.02 cnf(1214,plain,
% 97.93/98.02 (~P5(a86,a86)),
% 97.93/98.02 inference(scs_inference,[],[113,100,105,104])).
% 97.93/98.02 cnf(1221,plain,
% 97.93/98.02 (P3(a86,a5)),
% 97.93/98.02 inference(scs_inference,[],[113,110,100])).
% 97.93/98.02 cnf(1222,plain,
% 97.93/98.02 (P6(a58,x12221,a5)),
% 97.93/98.02 inference(rename_variables,[],[110])).
% 97.93/98.02 cnf(1223,plain,
% 97.93/98.02 (P6(x12231,a58,a86)),
% 97.93/98.02 inference(rename_variables,[],[113])).
% 97.93/98.02 cnf(1226,plain,
% 97.93/98.02 (P6(a58,x12261,a5)),
% 97.93/98.02 inference(rename_variables,[],[110])).
% 97.93/98.02 cnf(1227,plain,
% 97.93/98.02 (P6(x12271,a58,a86)),
% 97.93/98.02 inference(rename_variables,[],[113])).
% 97.93/98.02 cnf(1229,plain,
% 97.93/98.02 (~P5(a86,a5)),
% 97.93/98.02 inference(scs_inference,[],[113,1223,1227,110,1222,1226,100,105,104])).
% 97.93/98.02 cnf(1238,plain,
% 97.93/98.02 (P3(a86,a73)),
% 97.93/98.02 inference(scs_inference,[],[113,119,100])).
% 97.93/98.02 cnf(1239,plain,
% 97.93/98.02 (P6(a58,x12391,a73)),
% 97.93/98.02 inference(rename_variables,[],[119])).
% 97.93/98.02 cnf(1240,plain,
% 97.93/98.02 (P6(x12401,a58,a86)),
% 97.93/98.02 inference(rename_variables,[],[113])).
% 97.93/98.02 cnf(1243,plain,
% 97.93/98.02 (P6(a58,x12431,a73)),
% 97.93/98.02 inference(rename_variables,[],[119])).
% 97.93/98.02 cnf(1244,plain,
% 97.93/98.02 (P6(x12441,a58,a86)),
% 97.93/98.02 inference(rename_variables,[],[113])).
% 97.93/98.02 cnf(1246,plain,
% 97.93/98.02 (~P5(a86,a73)),
% 97.93/98.02 inference(scs_inference,[],[113,1240,1244,119,1239,1243,100,105,104])).
% 97.93/98.02 cnf(1248,plain,
% 97.93/98.02 (P6(x12481,a58,a86)),
% 97.93/98.02 inference(rename_variables,[],[113])).
% 97.93/98.02 cnf(1250,plain,
% 97.93/98.02 (P4(a86,a7)),
% 97.93/98.02 inference(scs_inference,[],[113,1240,1244,1248,119,1239,1243,986,100,105,104,91])).
% 97.93/98.02 cnf(1255,plain,
% 97.93/98.02 (P3(a86,a80)),
% 97.93/98.02 inference(scs_inference,[],[113,116,100])).
% 97.93/98.02 cnf(1256,plain,
% 97.93/98.02 (P6(a58,x12561,a80)),
% 97.93/98.02 inference(rename_variables,[],[116])).
% 97.93/98.02 cnf(1257,plain,
% 97.93/98.02 (P6(x12571,a58,a86)),
% 97.93/98.02 inference(rename_variables,[],[113])).
% 97.93/98.02 cnf(1260,plain,
% 97.93/98.02 (P6(a58,x12601,a80)),
% 97.93/98.02 inference(rename_variables,[],[116])).
% 97.93/98.02 cnf(1261,plain,
% 97.93/98.02 (P6(x12611,a58,a86)),
% 97.93/98.02 inference(rename_variables,[],[113])).
% 97.93/98.02 cnf(1263,plain,
% 97.93/98.02 (~P5(a86,a80)),
% 97.93/98.02 inference(scs_inference,[],[113,1257,1261,116,1256,1260,100,105,104])).
% 97.93/98.02 cnf(1312,plain,
% 97.93/98.02 (P3(a80,a80)),
% 97.93/98.02 inference(scs_inference,[],[116,100])).
% 97.93/98.02 cnf(1315,plain,
% 97.93/98.02 (P6(a58,x13151,a5)),
% 97.93/98.02 inference(rename_variables,[],[110])).
% 97.93/98.02 cnf(1317,plain,
% 97.93/98.02 (~P5(a80,a5)),
% 97.93/98.02 inference(scs_inference,[],[116,110,1315,100,105,104])).
% 97.93/98.02 cnf(1324,plain,
% 97.93/98.02 (P3(a80,a5)),
% 97.93/98.02 inference(scs_inference,[],[116,110,100])).
% 97.93/98.02 cnf(1328,plain,
% 97.93/98.02 (P6(x13281,a3,a73)),
% 97.93/98.02 inference(rename_variables,[],[122])).
% 97.93/98.02 cnf(1329,plain,
% 97.93/98.02 (P6(a58,x13291,a80)),
% 97.93/98.02 inference(rename_variables,[],[116])).
% 97.93/98.02 cnf(1331,plain,
% 97.93/98.02 (~P5(a80,a73)),
% 97.93/98.02 inference(scs_inference,[],[116,1329,110,122,1328,100,105,104])).
% 97.93/98.02 cnf(1333,plain,
% 97.93/98.02 (P6(a58,x13331,a80)),
% 97.93/98.02 inference(rename_variables,[],[116])).
% 97.93/98.02 cnf(1335,plain,
% 97.93/98.02 (P4(a80,a4)),
% 97.93/98.02 inference(scs_inference,[],[116,1329,1333,110,122,1328,201,100,105,104,91])).
% 97.93/98.02 cnf(1339,plain,
% 97.93/98.02 (P3(a80,a73)),
% 97.93/98.02 inference(scs_inference,[],[116,122,100])).
% 97.93/98.02 cnf(1341,plain,
% 97.93/98.02 (P6(a58,x13411,a80)),
% 97.93/98.02 inference(rename_variables,[],[116])).
% 97.93/98.02 cnf(1344,plain,
% 97.93/98.02 (P6(x13441,a58,a86)),
% 97.93/98.02 inference(rename_variables,[],[113])).
% 97.93/98.02 cnf(1345,plain,
% 97.93/98.02 (P6(a58,x13451,a80)),
% 97.93/98.02 inference(rename_variables,[],[116])).
% 97.93/98.02 cnf(1347,plain,
% 97.93/98.02 (~P5(a80,a86)),
% 97.93/98.02 inference(scs_inference,[],[116,1341,1345,122,113,1344,100,105,104])).
% 97.93/98.02 cnf(1349,plain,
% 97.93/98.02 (P6(a58,x13491,a80)),
% 97.93/98.02 inference(rename_variables,[],[116])).
% 97.93/98.02 cnf(1351,plain,
% 97.93/98.02 (P4(a80,a88)),
% 97.93/98.02 inference(scs_inference,[],[116,1341,1345,1349,122,113,1344,461,100,105,104,91])).
% 97.93/98.02 cnf(1356,plain,
% 97.93/98.02 (P3(a80,a86)),
% 97.93/98.02 inference(scs_inference,[],[116,113,100])).
% 97.93/98.02 cnf(1365,plain,
% 97.93/98.02 (P4(a80,a83)),
% 97.93/98.02 inference(scs_inference,[],[116,995,91])).
% 97.93/98.02 cnf(1370,plain,
% 97.93/98.02 (P4(a80,a89)),
% 97.93/98.02 inference(scs_inference,[],[116,853,91])).
% 97.93/98.02 cnf(1380,plain,
% 97.93/98.02 (P4(a80,a87)),
% 97.93/98.02 inference(scs_inference,[],[116,526,91])).
% 97.93/98.02 cnf(1384,plain,
% 97.93/98.02 (P4(a80,a91)),
% 97.93/98.02 inference(scs_inference,[],[116,594,91])).
% 97.93/98.02 cnf(1388,plain,
% 97.93/98.02 (P6(a65,a3,a82)),
% 97.93/98.02 inference(scs_inference,[],[8,4,34,15])).
% 97.93/98.02 cnf(1389,plain,
% 97.93/98.02 (P3(a82,a82)),
% 97.93/98.02 inference(scs_inference,[],[1388,100])).
% 97.93/98.02 cnf(1391,plain,
% 97.93/98.02 (~P5(a82,a82)),
% 97.93/98.02 inference(scs_inference,[],[1388,100,104])).
% 97.93/98.02 cnf(1397,plain,
% 97.93/98.02 (P4(a80,a90)),
% 97.93/98.02 inference(scs_inference,[],[116,1019,91])).
% 97.93/98.02 cnf(1405,plain,
% 97.93/98.02 (~P6(x14051,a58,a75)+P6(x14051,x14052,a5)),
% 97.93/98.02 inference(scs_inference,[],[14,48,21])).
% 97.93/98.02 cnf(1406,plain,
% 97.93/98.02 (P4(a80,a75)),
% 97.93/98.02 inference(scs_inference,[],[116,145,91])).
% 97.93/98.02 cnf(1409,plain,
% 97.93/98.02 (P2(x14091,a5)+~P6(f41(x14091,a5),a58,a75)),
% 97.93/98.02 inference(scs_inference,[],[1405,99])).
% 97.93/98.02 cnf(1449,plain,
% 97.93/98.02 (P4(a88,a4)),
% 97.93/98.02 inference(scs_inference,[],[606,198,91])).
% 97.93/98.02 cnf(1453,plain,
% 97.93/98.02 (P6(a58,x14531,a5)),
% 97.93/98.02 inference(rename_variables,[],[110])).
% 97.93/98.02 cnf(1455,plain,
% 97.93/98.02 (~P5(a73,a5)),
% 97.93/98.02 inference(scs_inference,[],[119,110,1453,105,104])).
% 97.93/98.02 cnf(1478,plain,
% 97.93/98.02 (~P6(x14781,a58,a84)),
% 97.93/98.02 inference(scs_inference,[],[113,14,78,28])).
% 97.93/98.02 cnf(1497,plain,
% 97.93/98.02 (P4(a5,a84)),
% 97.93/98.02 inference(scs_inference,[],[110,1478,91])).
% 97.93/98.02 cnf(1563,plain,
% 97.93/98.02 (P6(x15631,a65,a80)),
% 97.93/98.02 inference(scs_inference,[],[4,15,22])).
% 97.93/98.02 cnf(1602,plain,
% 97.93/98.02 (P1(a68,f74(a62))),
% 97.93/98.02 inference(scs_inference,[],[11,15,17])).
% 97.93/98.02 cnf(1606,plain,
% 97.93/98.02 (~P6(a65,x16061,a5)),
% 97.93/98.02 inference(scs_inference,[],[4,15,36])).
% 97.93/98.02 cnf(1614,plain,
% 97.93/98.02 (~P6(x16141,a62,a81)),
% 97.93/98.02 inference(scs_inference,[],[11,15,27])).
% 97.93/98.02 cnf(1618,plain,
% 97.93/98.02 (~P6(a65,x16181,a83)),
% 97.93/98.02 inference(scs_inference,[],[4,15,37])).
% 97.93/98.02 cnf(1623,plain,
% 97.93/98.02 (~P6(x16231,a62,a84)),
% 97.93/98.02 inference(scs_inference,[],[11,15,28])).
% 97.93/98.02 cnf(1624,plain,
% 97.93/98.02 (~P1(f24(a3,a62),a62)),
% 97.93/98.02 inference(scs_inference,[],[1623,254])).
% 97.93/98.02 cnf(1631,plain,
% 97.93/98.02 (~P6(a65,x16311,a85)),
% 97.93/98.02 inference(scs_inference,[],[4,15,38])).
% 97.93/98.02 cnf(1639,plain,
% 97.93/98.02 (~P6(x16391,a62,a87)),
% 97.93/98.02 inference(scs_inference,[],[11,15,29])).
% 97.93/98.02 cnf(1648,plain,
% 97.93/98.02 (~P6(a65,x16481,a89)),
% 97.93/98.02 inference(scs_inference,[],[4,15,39])).
% 97.93/98.02 cnf(1649,plain,
% 97.93/98.02 (~P6(x16491,a62,a85)),
% 97.93/98.02 inference(scs_inference,[],[11,15,30])).
% 97.93/98.02 cnf(1654,plain,
% 97.93/98.02 (P6(a65,a58,a6)),
% 97.93/98.02 inference(scs_inference,[],[4,576,15,40])).
% 97.93/98.02 cnf(1655,plain,
% 97.93/98.02 (P3(a6,a6)),
% 97.93/98.02 inference(scs_inference,[],[1654,100])).
% 97.93/98.02 cnf(1657,plain,
% 97.93/98.02 (~P5(a6,a6)),
% 97.93/98.02 inference(scs_inference,[],[1654,100,104])).
% 97.93/98.02 cnf(1663,plain,
% 97.93/98.02 (~P6(a62,x16631,a84)),
% 97.93/98.02 inference(scs_inference,[],[11,15,31])).
% 97.93/98.02 cnf(1671,plain,
% 97.93/98.02 (P6(a58,a65,a83)),
% 97.93/98.02 inference(scs_inference,[],[4,14,15,41])).
% 97.93/98.02 cnf(1674,plain,
% 97.93/98.02 (P3(a83,a83)),
% 97.93/98.02 inference(scs_inference,[],[1671,105,100])).
% 97.93/98.02 cnf(1676,plain,
% 97.93/98.02 (~P5(a83,a83)),
% 97.93/98.02 inference(scs_inference,[],[1671,105,100,104])).
% 97.93/98.02 cnf(1682,plain,
% 97.93/98.02 (~P6(a62,x16821,a88)),
% 97.93/98.02 inference(scs_inference,[],[11,15,32])).
% 97.93/98.02 cnf(1692,plain,
% 97.93/98.02 (~P6(a62,a3,a7)),
% 97.93/98.02 inference(scs_inference,[],[11,8,15,44])).
% 97.93/98.02 cnf(1696,plain,
% 97.93/98.02 (~P6(a65,a58,a75)),
% 97.93/98.02 inference(scs_inference,[],[4,14,15,48])).
% 97.93/98.02 cnf(1700,plain,
% 97.93/98.02 (~P6(a62,a3,a75)),
% 97.93/98.02 inference(scs_inference,[],[11,8,15,45])).
% 97.93/98.02 cnf(1704,plain,
% 97.93/98.02 (P6(a65,a3,a81)),
% 97.93/98.02 inference(scs_inference,[],[4,8,15,77])).
% 97.93/98.02 cnf(1705,plain,
% 97.93/98.02 (P3(a81,a81)),
% 97.93/98.02 inference(scs_inference,[],[1704,100])).
% 97.93/98.02 cnf(1707,plain,
% 97.93/98.02 (~P5(a81,a81)),
% 97.93/98.02 inference(scs_inference,[],[1704,100,104])).
% 97.93/98.02 cnf(1712,plain,
% 97.93/98.02 (P1(f60(a62,a58),a65)),
% 97.93/98.02 inference(scs_inference,[],[14,560,15,76])).
% 97.93/98.02 cnf(1716,plain,
% 97.93/98.02 (~P6(a58,a65,a86)),
% 97.93/98.02 inference(scs_inference,[],[4,14,15,78])).
% 97.93/98.02 cnf(1724,plain,
% 97.93/98.02 (~P6(a3,a62,a7)),
% 97.93/98.02 inference(scs_inference,[],[11,8,15,46])).
% 97.93/98.02 cnf(1807,plain,
% 97.93/98.02 (~P6(a65,a58,a80)),
% 97.93/98.02 inference(scs_inference,[],[4,14,15,79])).
% 97.93/98.02 cnf(1815,plain,
% 97.93/98.02 (P1(f72(a58,a62),a65)),
% 97.93/98.02 inference(scs_inference,[],[14,563,15,76])).
% 97.93/98.02 cnf(1820,plain,
% 97.93/98.02 (P6(a58,a65,a89)),
% 97.93/98.02 inference(scs_inference,[],[4,14,11,15,74])).
% 97.93/98.02 cnf(1823,plain,
% 97.93/98.02 (P3(a89,a89)),
% 97.93/98.02 inference(scs_inference,[],[1820,105,100])).
% 97.93/98.02 cnf(1825,plain,
% 97.93/98.02 (~P5(a89,a89)),
% 97.93/98.02 inference(scs_inference,[],[1820,105,100,104])).
% 97.93/98.02 cnf(1831,plain,
% 97.93/98.02 (P6(a62,a3,a87)),
% 97.93/98.02 inference(scs_inference,[],[11,8,4,15,90])).
% 97.93/98.02 cnf(1832,plain,
% 97.93/98.02 (P3(a87,a87)),
% 97.93/98.02 inference(scs_inference,[],[1831,100])).
% 97.93/98.02 cnf(1834,plain,
% 97.93/98.02 (~P5(a87,a87)),
% 97.93/98.02 inference(scs_inference,[],[1831,100,104])).
% 97.93/98.02 cnf(1840,plain,
% 97.93/98.02 (~P1(f39(a58,a65),a62)),
% 97.93/98.02 inference(scs_inference,[],[1820,15,87])).
% 97.93/98.02 cnf(1858,plain,
% 97.93/98.02 (P6(a58,a62,a89)),
% 97.93/98.02 inference(scs_inference,[],[11,14,4,15,74])).
% 97.93/98.02 cnf(1862,plain,
% 97.93/98.02 (P6(a65,a3,a87)),
% 97.93/98.02 inference(scs_inference,[],[4,8,11,15,90])).
% 97.93/98.02 cnf(1866,plain,
% 97.93/98.02 (P1(f34(a58,a62),a65)),
% 97.93/98.02 inference(scs_inference,[],[1858,15,64])).
% 97.93/98.02 cnf(1871,plain,
% 97.93/98.02 (~P1(f26(a65,a3),a62)),
% 97.93/98.02 inference(scs_inference,[],[1862,15,84])).
% 97.93/98.02 cnf(1876,plain,
% 97.93/98.02 (~P1(f19(a62,a3),a62)),
% 97.93/98.02 inference(scs_inference,[],[11,8,1700,4,15,107])).
% 97.93/98.02 cnf(1877,plain,
% 97.93/98.02 (P1(f19(a65,a58),a65)),
% 97.93/98.02 inference(scs_inference,[],[4,14,1696,11,15,96])).
% 97.93/98.02 cnf(1917,plain,
% 97.93/98.02 (P6(a65,a3,a75)+~P1(f19(a65,a3),a62)),
% 97.93/98.02 inference(scs_inference,[],[8,11,15,107])).
% 97.93/98.02 cnf(1922,plain,
% 97.93/98.02 (~P1(f19(a65,a3),a62)),
% 97.93/98.02 inference(scs_inference,[],[11,8,1917,45])).
% 97.93/98.02 cnf(1927,plain,
% 97.93/98.02 (~P6(a59,a3,a7)+~P1(a63,a56)),
% 97.93/98.02 inference(scs_inference,[],[8,18,44])).
% 97.93/98.02 cnf(1932,plain,
% 97.93/98.02 (~P2(a73,a7)+~P1(a63,a56)),
% 97.93/98.02 inference(scs_inference,[],[122,1927,94])).
% 97.93/98.02 cnf(1950,plain,
% 97.93/98.02 (~P6(a56,a3,a75)+~P1(a64,a59)),
% 97.93/98.02 inference(scs_inference,[],[8,18,45])).
% 97.93/98.02 cnf(1955,plain,
% 97.93/98.02 (~P2(a73,a75)+~P1(a64,a59)),
% 97.93/98.02 inference(scs_inference,[],[122,1950,94])).
% 97.93/98.02 cnf(4177,plain,
% 97.93/98.02 (P6(a58,x41771,a5)),
% 97.93/98.02 inference(rename_variables,[],[110])).
% 97.93/98.02 cnf(4181,plain,
% 97.93/98.02 (P3(a85,a5)),
% 97.93/98.02 inference(scs_inference,[],[194,110,4177,201,105,91,100])).
% 97.93/98.02 cnf(4182,plain,
% 97.93/98.02 (P6(a58,x41821,a5)),
% 97.93/98.02 inference(rename_variables,[],[110])).
% 97.93/98.02 cnf(4184,plain,
% 97.93/98.02 (~P5(a85,a5)),
% 97.93/98.02 inference(scs_inference,[],[194,110,4177,4182,201,105,91,100,104])).
% 97.93/98.02 cnf(4189,plain,
% 97.93/98.02 (P6(x41891,a3,a73)),
% 97.93/98.02 inference(rename_variables,[],[122])).
% 97.93/98.02 cnf(4194,plain,
% 97.93/98.02 (P3(a85,a73)),
% 97.93/98.02 inference(scs_inference,[],[194,122,4189,130,105,91,100])).
% 97.93/98.02 cnf(4195,plain,
% 97.93/98.02 (P6(x41951,a3,a73)),
% 97.93/98.02 inference(rename_variables,[],[122])).
% 97.93/98.02 cnf(4197,plain,
% 97.93/98.02 (~P5(a85,a73)),
% 97.93/98.02 inference(scs_inference,[],[194,122,4189,4195,130,105,91,100,104])).
% 97.93/98.02 cnf(4201,plain,
% 97.93/98.02 (P6(a58,x42011,a80)),
% 97.93/98.02 inference(rename_variables,[],[116])).
% 97.93/98.02 cnf(4206,plain,
% 97.93/98.02 (P3(a85,a80)),
% 97.93/98.02 inference(scs_inference,[],[194,116,4201,136,105,91,100])).
% 97.93/98.02 cnf(4207,plain,
% 97.93/98.02 (P6(a58,x42071,a80)),
% 97.93/98.02 inference(rename_variables,[],[116])).
% 97.93/98.02 cnf(4209,plain,
% 97.93/98.02 (~P5(a85,a80)),
% 97.93/98.02 inference(scs_inference,[],[194,116,4201,4207,136,105,91,100,104])).
% 97.93/98.02 cnf(4267,plain,
% 97.93/98.02 (P6(x42671,a3,a73)),
% 97.93/98.02 inference(rename_variables,[],[122])).
% 97.93/98.02 cnf(4269,plain,
% 97.93/98.02 (~P5(a7,a73)),
% 97.93/98.02 inference(scs_inference,[],[210,122,4267,105,104])).
% 97.93/98.02 cnf(4270,plain,
% 97.93/98.02 (P6(x42701,a3,a73)),
% 97.93/98.02 inference(rename_variables,[],[122])).
% 97.93/98.02 cnf(4272,plain,
% 97.93/98.02 (P3(a7,a73)),
% 97.93/98.02 inference(scs_inference,[],[210,122,4267,4270,105,104,100])).
% 97.93/98.02 cnf(4278,plain,
% 97.93/98.02 (P6(x42781,a3,a73)),
% 97.93/98.02 inference(rename_variables,[],[122])).
% 97.93/98.02 cnf(4283,plain,
% 97.93/98.02 (~P5(a84,a73)),
% 97.93/98.02 inference(scs_inference,[],[214,122,4278,187,105,91,104])).
% 97.93/98.02 cnf(4284,plain,
% 97.93/98.02 (P6(x42841,a3,a73)),
% 97.93/98.02 inference(rename_variables,[],[122])).
% 97.93/98.02 cnf(4286,plain,
% 97.93/98.02 (P3(a84,a73)),
% 97.93/98.02 inference(scs_inference,[],[214,122,4278,4284,187,105,91,104,100])).
% 97.93/98.02 cnf(4389,plain,
% 97.93/98.02 (~P2(a73,a7)+~P6(a56,a3,a7)),
% 97.93/98.02 inference(scs_inference,[],[8,1932,44])).
% 97.93/98.02 cnf(4390,plain,
% 97.93/98.02 (~P2(a73,a7)),
% 97.93/98.02 inference(scs_inference,[],[122,4389,94])).
% 97.93/98.02 cnf(4391,plain,
% 97.93/98.02 (~P2(a73,a75)+~P6(a59,a3,a75)),
% 97.93/98.02 inference(scs_inference,[],[8,1955,45])).
% 97.93/98.02 cnf(4396,plain,
% 97.93/98.02 (~P2(a73,a75)),
% 97.93/98.02 inference(scs_inference,[],[122,4391,94])).
% 97.93/98.02 cnf(4503,plain,
% 97.93/98.02 (P6(x45031,a58,a86)),
% 97.93/98.02 inference(rename_variables,[],[113])).
% 97.93/98.02 cnf(4505,plain,
% 97.93/98.02 (~P5(a88,a86)),
% 97.93/98.02 inference(scs_inference,[],[606,113,4503,105,104])).
% 97.93/98.02 cnf(4506,plain,
% 97.93/98.02 (P6(x45061,a58,a86)),
% 97.93/98.02 inference(rename_variables,[],[113])).
% 97.93/98.02 cnf(4511,plain,
% 97.93/98.02 (P3(a88,a86)),
% 97.93/98.02 inference(scs_inference,[],[606,113,4503,4506,127,105,104,91,100])).
% 97.93/98.02 cnf(4967,plain,
% 97.93/98.02 (P6(f74(a58),f48(a84,a84),a84)),
% 97.93/98.02 inference(scs_inference,[],[647,576,98])).
% 97.93/98.02 cnf(4969,plain,
% 97.93/98.02 (P1(x49691,f48(a84,a84))),
% 97.93/98.02 inference(rename_variables,[],[647])).
% 97.93/98.02 cnf(4971,plain,
% 97.93/98.02 (P6(f48(a5,a5),f48(a84,a84),a85)),
% 97.93/98.02 inference(scs_inference,[],[647,4969,576,636,98,93])).
% 97.93/98.02 cnf(4980,plain,
% 97.93/98.02 (P6(f45(a5,a5),f48(a84,a84),a85)),
% 97.93/98.02 inference(scs_inference,[],[647,779,93])).
% 97.93/98.02 cnf(4994,plain,
% 97.93/98.02 (P6(f46(a88,a88),f48(a84,a84),a85)),
% 97.93/98.02 inference(scs_inference,[],[647,951,93])).
% 97.93/98.02 cnf(5040,plain,
% 97.93/98.02 (~P6(x50401,a71,a81)),
% 97.93/98.02 inference(scs_inference,[],[190,229,246,4390,12,50,51,52,69,70,71,99,102,27])).
% 97.93/98.02 cnf(5042,plain,
% 97.93/98.02 (~P6(a2,x50421,a83)),
% 97.93/98.02 inference(scs_inference,[],[1,190,229,246,4390,12,50,51,52,69,70,71,99,102,27,37])).
% 97.93/98.02 cnf(5044,plain,
% 97.93/98.02 (~P6(x50441,a71,a87)),
% 97.93/98.02 inference(scs_inference,[],[1,190,229,246,4390,12,50,51,52,69,70,71,99,102,27,37,29])).
% 97.93/98.02 cnf(5046,plain,
% 97.93/98.02 (~P6(a2,x50461,a89)),
% 97.93/98.02 inference(scs_inference,[],[1,190,229,246,4390,12,50,51,52,69,70,71,99,102,27,37,29,39])).
% 97.93/98.02 cnf(5048,plain,
% 97.93/98.02 (~P6(a71,x50481,a88)),
% 97.93/98.02 inference(scs_inference,[],[1,190,229,246,4390,12,50,51,52,69,70,71,99,102,27,37,29,39,32])).
% 97.93/98.02 cnf(5052,plain,
% 97.93/98.02 (P6(a2,x50521,a86)),
% 97.93/98.02 inference(scs_inference,[],[1,190,229,246,4390,12,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23])).
% 97.93/98.02 cnf(5054,plain,
% 97.93/98.02 (~P6(x50541,a71,a84)),
% 97.93/98.02 inference(scs_inference,[],[1,190,229,246,4390,12,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28])).
% 97.93/98.02 cnf(5056,plain,
% 97.93/98.02 (P1(f9(a58,a65),a65)),
% 97.93/98.02 inference(scs_inference,[],[1,190,229,246,4390,12,1716,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28,24])).
% 97.93/98.02 cnf(5058,plain,
% 97.93/98.02 (~P1(a1,f74(a2))),
% 97.93/98.02 inference(scs_inference,[],[1,190,229,246,4390,12,1716,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28,24,20])).
% 97.93/98.02 cnf(5060,plain,
% 97.93/98.02 (~P6(x50601,a71,a85)),
% 97.93/98.02 inference(scs_inference,[],[1,190,229,246,4390,12,1716,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28,24,20,30])).
% 97.93/98.02 cnf(5062,plain,
% 97.93/98.02 (~P6(a71,x50621,a84)),
% 97.93/98.02 inference(scs_inference,[],[1,190,229,246,4390,12,1716,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28,24,20,30,31])).
% 97.93/98.02 cnf(5064,plain,
% 97.93/98.02 (~P1(f26(a65,a3),a65)),
% 97.93/98.02 inference(scs_inference,[],[1,190,229,246,4390,12,1716,1862,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28,24,20,30,31,84])).
% 97.93/98.02 cnf(5066,plain,
% 97.93/98.02 (~P6(a2,x50661,a5)),
% 97.93/98.02 inference(scs_inference,[],[1,190,229,246,4390,12,1716,1862,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28,24,20,30,31,84,36])).
% 97.93/98.02 cnf(5068,plain,
% 97.93/98.02 (~P1(f39(a58,a62),a62)),
% 97.93/98.02 inference(scs_inference,[],[1,190,229,246,4390,12,1716,1858,1862,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28,24,20,30,31,84,36,87])).
% 97.93/98.02 cnf(5070,plain,
% 97.93/98.02 (P6(x50701,a2,a80)),
% 97.93/98.02 inference(scs_inference,[],[1,190,229,246,4390,12,1716,1858,1862,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28,24,20,30,31,84,36,87,22])).
% 97.93/98.02 cnf(5072,plain,
% 97.93/98.02 (P1(f33(a58,a65),a65)),
% 97.93/98.02 inference(scs_inference,[],[1,190,229,246,4390,12,1716,1858,1862,1671,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28,24,20,30,31,84,36,87,22,63])).
% 97.93/98.02 cnf(5086,plain,
% 97.93/98.02 (P1(f34(a58,a62),a62)),
% 97.93/98.02 inference(scs_inference,[],[1,190,229,246,4390,10,12,1807,1716,1858,1862,1654,1704,1388,1671,1606,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28,24,20,30,31,84,36,87,22,63,25,56,17,21,54,65,64])).
% 97.93/98.02 cnf(5092,plain,
% 97.93/98.02 (~P6(f74(a62),a62,a90)),
% 97.93/98.02 inference(scs_inference,[],[1,125,190,229,246,4390,10,12,485,1602,1807,1716,1858,1862,1654,1704,1388,1671,465,1606,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28,24,20,30,31,84,36,87,22,63,25,56,17,21,54,65,64,60,45,47])).
% 97.93/98.02 cnf(5098,plain,
% 97.93/98.02 (~P2(a84,a89)),
% 97.93/98.02 inference(scs_inference,[],[1,125,190,229,246,4390,10,12,485,4967,1602,1807,1716,1858,1862,678,1654,1704,1388,1671,465,1606,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28,24,20,30,31,84,36,87,22,63,25,56,17,21,54,65,64,60,45,47,48,49,94])).
% 97.93/98.02 cnf(5110,plain,
% 97.93/98.02 (~P1(f14(a2,a62),a62)),
% 97.93/98.02 inference(scs_inference,[],[1,125,190,229,246,4390,10,12,485,4967,1602,1614,1618,1807,1716,1858,1862,678,1654,1704,1388,1671,465,484,1563,1606,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28,24,20,30,31,84,36,87,22,63,25,56,17,21,54,65,64,60,45,47,48,49,94,78,79,41,77])).
% 97.93/98.02 cnf(5113,plain,
% 97.93/98.02 (~P6(f74(a62),a62,a73)),
% 97.93/98.02 inference(scs_inference,[],[1,125,190,229,246,4390,10,12,485,4967,1602,1614,1618,1807,1716,1858,1862,678,1654,1704,1388,1671,465,484,1563,1606,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28,24,20,30,31,84,36,87,22,63,25,56,17,21,54,65,64,60,45,47,48,49,94,78,79,41,77,43])).
% 97.93/98.02 cnf(5123,plain,
% 97.93/98.02 (~P6(f74(a65),a65,a7)),
% 97.93/98.02 inference(scs_inference,[],[1,125,190,229,246,4390,10,12,485,4967,1602,1614,1618,1807,1716,1858,1862,678,1654,1704,1388,1671,465,484,1563,1606,779,951,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28,24,20,30,31,84,36,87,22,63,25,56,17,21,54,65,64,60,45,47,48,49,94,78,79,41,77,43,34,76,46,44])).
% 97.93/98.02 cnf(5125,plain,
% 97.93/98.02 (~P1(f40(a62,a58),a62)),
% 97.93/98.02 inference(scs_inference,[],[1,125,190,229,246,4390,10,12,485,4967,1602,1614,1618,1682,1807,1716,1858,1862,678,1654,1704,1388,1671,465,484,1563,1606,576,779,951,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28,24,20,30,31,84,36,87,22,63,25,56,17,21,54,65,64,60,45,47,48,49,94,78,79,41,77,43,34,76,46,44,101])).
% 97.93/98.02 cnf(5129,plain,
% 97.93/98.02 (~P5(a73,a85)),
% 97.93/98.02 inference(scs_inference,[],[1,125,190,229,246,4390,10,12,485,4967,4971,1602,1614,672,1618,1682,1807,1716,1858,1862,678,1654,1704,1388,1671,465,484,1563,1606,576,779,951,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28,24,20,30,31,84,36,87,22,63,25,56,17,21,54,65,64,60,45,47,48,49,94,78,79,41,77,43,34,76,46,44,101,104])).
% 97.93/98.02 cnf(5130,plain,
% 97.93/98.02 (P6(f48(a5,a5),x51301,a73)),
% 97.93/98.02 inference(rename_variables,[],[672])).
% 97.93/98.02 cnf(5133,plain,
% 97.93/98.02 (P1(x51331,a3)),
% 97.93/98.02 inference(rename_variables,[],[8])).
% 97.93/98.02 cnf(5137,plain,
% 97.93/98.02 (P6(f48(a5,a5),x51371,a73)),
% 97.93/98.02 inference(rename_variables,[],[672])).
% 97.93/98.02 cnf(5139,plain,
% 97.93/98.02 (P3(a73,a85)),
% 97.93/98.02 inference(scs_inference,[],[1,125,190,229,246,4390,10,12,485,4967,4971,1602,1614,672,5130,5137,1618,1682,1807,1716,1858,1862,678,1663,1654,1704,1388,1671,465,484,1563,1606,576,779,951,8,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28,24,20,30,31,84,36,87,22,63,25,56,17,21,54,65,64,60,45,47,48,49,94,78,79,41,77,43,34,76,46,44,101,104,98,105,100])).
% 97.93/98.02 cnf(5142,plain,
% 97.93/98.02 (P6(a2,a2,a4)),
% 97.93/98.02 inference(scs_inference,[],[1,125,190,229,246,4390,10,12,485,4967,4971,1602,1614,672,5130,5137,1618,1682,1807,1716,1858,1862,678,1663,1654,1704,1388,1671,465,484,1563,1606,576,779,951,8,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28,24,20,30,31,84,36,87,22,63,25,56,17,21,54,65,64,60,45,47,48,49,94,78,79,41,77,43,34,76,46,44,101,104,98,105,100,33])).
% 97.93/98.02 cnf(5145,plain,
% 97.93/98.02 (P1(x51451,a3)),
% 97.93/98.02 inference(rename_variables,[],[8])).
% 97.93/98.02 cnf(5148,plain,
% 97.93/98.02 (~P1(f22(a2,a62),a62)),
% 97.93/98.02 inference(scs_inference,[],[1,125,190,229,246,4390,10,12,485,4967,4971,1602,1614,1639,672,5130,5137,1618,1682,1807,1716,1858,1862,678,9,1631,1663,1654,1704,1388,1671,465,484,1563,1606,576,779,951,8,5133,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28,24,20,30,31,84,36,87,22,63,25,56,17,21,54,65,64,60,45,47,48,49,94,78,79,41,77,43,34,76,46,44,101,104,98,105,100,33,93,90])).
% 97.93/98.02 cnf(5151,plain,
% 97.93/98.02 (~P1(f12(a3,a62),a62)),
% 97.93/98.02 inference(scs_inference,[],[1,125,190,229,246,4390,10,12,485,4967,4971,1602,1614,1639,672,5130,5137,1618,1682,1807,1716,1858,1862,678,1724,9,1631,1663,1654,1704,1388,1671,465,484,1563,1606,576,779,951,8,5133,5145,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28,24,20,30,31,84,36,87,22,63,25,56,17,21,54,65,64,60,45,47,48,49,94,78,79,41,77,43,34,76,46,44,101,104,98,105,100,33,93,90,106])).
% 97.93/98.02 cnf(5152,plain,
% 97.93/98.02 (P1(x51521,a3)),
% 97.93/98.02 inference(rename_variables,[],[8])).
% 97.93/98.02 cnf(5153,plain,
% 97.93/98.02 (P1(x51531,a3)),
% 97.93/98.02 inference(rename_variables,[],[8])).
% 97.93/98.02 cnf(5158,plain,
% 97.93/98.02 (~P6(a2,a58,a75)),
% 97.93/98.02 inference(scs_inference,[],[1,125,190,229,246,4390,10,12,485,4967,4971,1602,1614,1639,672,5130,5137,1618,1648,1682,1807,1716,1858,1862,678,1724,9,1631,1663,1654,1704,1388,1671,465,484,1563,1606,576,779,951,8,5133,5145,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28,24,20,30,31,84,36,87,22,63,25,56,17,21,54,65,64,60,45,47,48,49,94,78,79,41,77,43,34,76,46,44,101,104,98,105,100,33,93,90,106,74,1405])).
% 97.93/98.02 cnf(5160,plain,
% 97.93/98.02 (P1(f76(a2,a2),a2)),
% 97.93/98.02 inference(scs_inference,[],[1,125,190,229,246,4390,10,12,485,4967,4971,1602,1614,1639,672,5130,5137,1618,1648,1682,1807,1716,1858,1862,678,1724,9,1631,1663,1654,1704,1388,1671,465,484,1563,1606,576,779,951,8,5133,5145,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28,24,20,30,31,84,36,87,22,63,25,56,17,21,54,65,64,60,45,47,48,49,94,78,79,41,77,43,34,76,46,44,101,104,98,105,100,33,93,90,106,74,1405,53])).
% 97.93/98.02 cnf(5162,plain,
% 97.93/98.03 (P1(f78(a2,a2),a2)),
% 97.93/98.03 inference(scs_inference,[],[1,125,190,229,246,4390,10,12,485,4967,4971,1602,1614,1639,672,5130,5137,1618,1648,1682,1807,1716,1858,1862,678,1724,9,1631,1663,1654,1704,1388,1671,465,484,1563,1606,576,779,951,8,5133,5145,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28,24,20,30,31,84,36,87,22,63,25,56,17,21,54,65,64,60,45,47,48,49,94,78,79,41,77,43,34,76,46,44,101,104,98,105,100,33,93,90,106,74,1405,53,81])).
% 97.93/98.03 cnf(5164,plain,
% 97.93/98.03 (P1(f77(a2,a2),a2)),
% 97.93/98.03 inference(scs_inference,[],[1,125,190,229,246,4390,10,12,485,4967,4971,1602,1614,1639,672,5130,5137,1618,1648,1682,1807,1716,1858,1862,678,1724,9,1631,1663,1654,1704,1388,1671,465,484,1563,1606,576,779,951,8,5133,5145,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28,24,20,30,31,84,36,87,22,63,25,56,17,21,54,65,64,60,45,47,48,49,94,78,79,41,77,43,34,76,46,44,101,104,98,105,100,33,93,90,106,74,1405,53,81,80])).
% 97.93/98.03 cnf(5168,plain,
% 97.93/98.03 (P6(a2,a3,a90)),
% 97.93/98.03 inference(scs_inference,[],[1,125,190,229,246,4390,10,12,485,4967,4971,1602,1614,1639,672,5130,5137,1618,1648,1682,1807,1716,1858,1862,678,1724,9,1631,1663,1654,1704,1388,5,1671,465,484,1563,1606,4,576,779,951,8,5133,5145,5153,5152,50,51,52,69,70,71,99,102,27,37,29,39,32,38,23,28,24,20,30,31,84,36,87,22,63,25,56,17,21,54,65,64,60,45,47,48,49,94,78,79,41,77,43,34,76,46,44,101,104,98,105,100,33,93,90,106,74,1405,53,81,80,88,97])).
% 97.93/98.03 cnf(5192,plain,
% 97.93/98.03 (~P6(a62,x51921,a89)),
% 97.93/98.03 inference(scs_inference,[],[243,288,304,4396,5058,5086,50,29,51,52,102,27,39])).
% 97.93/98.03 cnf(5198,plain,
% 97.93/98.03 (~P6(a62,x51981,a85)),
% 97.93/98.03 inference(scs_inference,[],[243,281,288,304,4396,5058,5086,50,29,51,52,102,27,39,69,32,38])).
% 97.93/98.03 cnf(5206,plain,
% 97.93/98.03 (~P6(a62,x52061,a83)),
% 97.93/98.03 inference(scs_inference,[],[243,281,288,295,304,4396,5058,5086,50,29,51,52,102,27,39,69,32,38,70,99,71,37])).
% 97.93/98.03 cnf(5208,plain,
% 97.93/98.03 (P6(a62,x52081,a86)),
% 97.93/98.03 inference(scs_inference,[],[243,281,288,295,304,4396,5058,5086,50,29,51,52,102,27,39,69,32,38,70,99,71,37,23])).
% 97.93/98.03 cnf(5212,plain,
% 97.93/98.03 (~P1(f60(a62,a58),f74(a65))),
% 97.93/98.03 inference(scs_inference,[],[243,281,288,295,304,4396,1712,5058,5086,50,29,51,52,102,27,39,69,32,38,70,99,71,37,23,28,20])).
% 97.93/98.03 cnf(5216,plain,
% 97.93/98.03 (~P6(f74(a2),x52161,a84)),
% 97.93/98.03 inference(scs_inference,[],[243,281,288,295,304,4396,1712,5058,5086,50,29,51,52,102,27,39,69,32,38,70,99,71,37,23,28,20,30,31])).
% 97.93/98.03 cnf(5218,plain,
% 97.93/98.03 (~P1(f26(a62,a3),a62)),
% 97.93/98.03 inference(scs_inference,[],[243,281,288,295,304,4396,1712,5058,5086,1831,50,29,51,52,102,27,39,69,32,38,70,99,71,37,23,28,20,30,31,84])).
% 97.93/98.03 cnf(5220,plain,
% 97.93/98.03 (~P6(a62,x52201,a5)),
% 97.93/98.03 inference(scs_inference,[],[243,281,288,295,304,4396,1712,5058,5086,1831,50,29,51,52,102,27,39,69,32,38,70,99,71,37,23,28,20,30,31,84,36])).
% 97.93/98.03 cnf(5222,plain,
% 97.93/98.03 (~P1(f39(a58,a65),a65)),
% 97.93/98.03 inference(scs_inference,[],[243,281,288,295,304,4396,1712,5058,5086,1831,1820,50,29,51,52,102,27,39,69,32,38,70,99,71,37,23,28,20,30,31,84,36,87])).
% 97.93/98.03 cnf(5224,plain,
% 97.93/98.03 (P6(x52241,a62,a80)),
% 97.93/98.03 inference(scs_inference,[],[243,281,288,295,304,4396,1712,5058,5086,1831,1820,50,29,51,52,102,27,39,69,32,38,70,99,71,37,23,28,20,30,31,84,36,87,22])).
% 97.93/98.03 cnf(5226,plain,
% 97.93/98.03 (~P1(f17(a2,a3),a2)),
% 97.93/98.03 inference(scs_inference,[],[243,281,288,295,304,4396,5168,1712,5058,5086,1831,1820,50,29,51,52,102,27,39,69,32,38,70,99,71,37,23,28,20,30,31,84,36,87,22,82])).
% 97.93/98.03 cnf(5228,plain,
% 97.93/98.03 (P1(f15(a2,a3),a2)),
% 97.93/98.03 inference(scs_inference,[],[243,281,288,295,304,4396,5168,1712,5058,5086,1831,1820,50,29,51,52,102,27,39,69,32,38,70,99,71,37,23,28,20,30,31,84,36,87,22,82,57])).
% 97.93/98.03 cnf(5230,plain,
% 97.93/98.03 (P1(f26(a65,a3),f74(a65))),
% 97.93/98.03 inference(scs_inference,[],[243,281,288,295,304,4396,5168,1712,5058,5064,5086,1831,1820,50,29,51,52,102,27,39,69,32,38,70,99,71,37,23,28,20,30,31,84,36,87,22,82,57,17])).
% 97.93/98.03 cnf(5236,plain,
% 97.93/98.03 (P1(f20(a62,a3),a62)),
% 97.93/98.03 inference(scs_inference,[],[243,281,288,295,304,4396,5066,5168,1712,5058,5064,5086,1831,1820,50,29,51,52,102,27,39,69,32,38,70,99,71,37,23,28,20,30,31,84,36,87,22,82,57,17,21,64,60])).
% 97.93/98.03 cnf(5245,plain,
% 97.93/98.03 (P6(a2,x52451,a86)),
% 97.93/98.03 inference(rename_variables,[],[5052])).
% 97.93/98.03 cnf(5247,plain,
% 97.93/98.03 (~P1(f14(a2,a71),a71)),
% 97.93/98.03 inference(scs_inference,[],[1,243,281,288,295,304,4396,5040,5052,5066,5168,1712,5058,5064,5086,1831,1820,50,29,51,52,102,27,39,69,32,38,70,99,71,37,23,28,20,30,31,84,36,87,22,82,57,17,21,64,60,48,49,47,78,77])).
% 97.93/98.03 cnf(5248,plain,
% 97.93/98.03 (~P6(x52481,a71,a81)),
% 97.93/98.03 inference(rename_variables,[],[5040])).
% 97.93/98.03 cnf(5250,plain,
% 97.93/98.03 (~P6(f74(a2),a2,a75)),
% 97.93/98.03 inference(scs_inference,[],[1,243,281,288,295,304,4396,5040,5052,5066,5168,1712,5058,5064,5086,1831,1820,50,29,51,52,102,27,39,69,32,38,70,99,71,37,23,28,20,30,31,84,36,87,22,82,57,17,21,64,60,48,49,47,78,77,45])).
% 97.93/98.03 cnf(5258,plain,
% 97.93/98.03 (~P2(a86,a81)),
% 97.93/98.03 inference(scs_inference,[],[1,243,281,288,295,304,4396,5040,5248,5042,5052,5245,5066,5070,5168,1712,5058,5064,5086,1831,1820,50,29,51,52,102,27,39,69,32,38,70,99,71,37,23,28,20,30,31,84,36,87,22,82,57,17,21,64,60,48,49,47,78,77,45,79,41,94])).
% 97.93/98.03 cnf(5266,plain,
% 97.93/98.03 (P1(f60(a59,a58),a59)),
% 97.93/98.03 inference(scs_inference,[],[1,243,281,288,295,304,4396,5040,5248,5042,5052,5245,5066,5070,5168,1712,5058,5064,5086,528,1831,1820,14,50,29,51,52,102,27,39,69,32,38,70,99,71,37,23,28,20,30,31,84,36,87,22,82,57,17,21,64,60,48,49,47,78,77,45,79,41,94,43,34,76])).
% 97.93/98.03 cnf(5267,plain,
% 97.93/98.03 (~P1(x52671,a58)),
% 97.93/98.03 inference(rename_variables,[],[14])).
% 97.93/98.03 cnf(5271,plain,
% 97.93/98.03 (~P6(f74(a2),a2,a7)),
% 97.93/98.03 inference(scs_inference,[],[1,243,281,288,295,304,4396,5040,5248,5042,5052,5245,5066,5070,5168,1712,5058,5064,5086,528,1831,1820,14,50,29,51,52,102,27,39,69,32,38,70,99,71,37,23,28,20,30,31,84,36,87,22,82,57,17,21,64,60,48,49,47,78,77,45,79,41,94,43,34,76,46,44])).
% 97.93/98.03 cnf(5274,plain,
% 97.93/98.03 (~P1(x52741,f45(a5,a5))),
% 97.93/98.03 inference(rename_variables,[],[779])).
% 97.93/98.03 cnf(5279,plain,
% 97.93/98.03 (P6(a2,a2,a73)),
% 97.93/98.03 inference(scs_inference,[],[1,243,281,288,295,304,4396,5040,5248,5042,5052,5245,5066,5070,5142,5168,1712,5058,5064,5086,528,1831,1820,13,779,5274,14,50,29,51,52,102,27,39,69,32,38,70,99,71,37,23,28,20,30,31,84,36,87,22,82,57,17,21,64,60,48,49,47,78,77,45,79,41,94,43,34,76,46,44,81,80,91])).
% 97.93/98.03 cnf(5281,plain,
% 97.93/98.03 (~P1(f40(a71,a58),a71)),
% 97.93/98.03 inference(scs_inference,[],[1,243,281,288,295,304,4396,5040,5248,5042,5048,5052,5245,5066,5070,5142,5168,1712,5058,5064,5086,528,1831,1820,13,576,779,5274,14,50,29,51,52,102,27,39,69,32,38,70,99,71,37,23,28,20,30,31,84,36,87,22,82,57,17,21,64,60,48,49,47,78,77,45,79,41,94,43,34,76,46,44,81,80,91,101])).
% 97.93/98.03 cnf(5285,plain,
% 97.93/98.03 (P6(a65,a65,a4)),
% 97.93/98.03 inference(scs_inference,[],[1,243,281,288,295,304,4396,5040,5248,5042,5048,5052,5245,5066,5070,5142,5168,1712,5058,5064,5086,528,1831,1820,13,576,779,5274,14,50,29,51,52,102,27,39,69,32,38,70,99,71,37,23,28,20,30,31,84,36,87,22,82,57,17,21,64,60,48,49,47,78,77,45,79,41,94,43,34,76,46,44,81,80,91,101,33])).
% 97.93/98.03 cnf(5287,plain,
% 97.93/98.03 (~P1(f22(a2,a71),a71)),
% 97.93/98.03 inference(scs_inference,[],[1,243,281,288,295,304,4396,5040,5248,5042,5044,5048,5052,5245,5066,5070,5142,5168,1712,5058,5064,5086,528,1831,1820,9,13,576,779,5274,14,50,29,51,52,102,27,39,69,32,38,70,99,71,37,23,28,20,30,31,84,36,87,22,82,57,17,21,64,60,48,49,47,78,77,45,79,41,94,43,34,76,46,44,81,80,91,101,33,90])).
% 97.93/98.03 cnf(5290,plain,
% 97.93/98.03 (~P1(f12(a62,a3),a62)),
% 97.93/98.03 inference(scs_inference,[],[1,243,281,288,295,304,4396,5040,5248,5042,5044,5048,5052,5245,5066,5070,5142,5168,1712,5058,5064,5086,1692,528,1831,1820,9,13,576,779,5274,14,8,50,29,51,52,102,27,39,69,32,38,70,99,71,37,23,28,20,30,31,84,36,87,22,82,57,17,21,64,60,48,49,47,78,77,45,79,41,94,43,34,76,46,44,81,80,91,101,33,90,106])).
% 97.93/98.03 cnf(5299,plain,
% 97.93/98.03 (~P6(a62,a58,a75)),
% 97.93/98.03 inference(scs_inference,[],[1,243,281,288,295,304,4396,5040,5248,5042,5044,5046,5048,5052,5245,5066,5070,5142,5158,5168,1712,5058,5064,5086,1692,528,1831,1820,9,13,576,779,5274,14,5267,8,50,29,51,52,102,27,39,69,32,38,70,99,71,37,23,28,20,30,31,84,36,87,22,82,57,17,21,64,60,48,49,47,78,77,45,79,41,94,43,34,76,46,44,81,80,91,101,33,90,106,74,96,1405])).
% 97.93/98.03 cnf(5301,plain,
% 97.93/98.03 (P1(f76(a65,a65),a65)),
% 97.93/98.03 inference(scs_inference,[],[1,243,281,288,295,304,4396,5040,5248,5042,5044,5046,5048,5052,5245,5066,5070,5142,5158,5168,1712,5058,5064,5086,1692,528,1831,1820,9,13,576,779,5274,14,5267,8,50,29,51,52,102,27,39,69,32,38,70,99,71,37,23,28,20,30,31,84,36,87,22,82,57,17,21,64,60,48,49,47,78,77,45,79,41,94,43,34,76,46,44,81,80,91,101,33,90,106,74,96,1405,54])).
% 97.93/98.03 cnf(5310,plain,
% 97.93/98.03 (~P6(x53101,f74(a65),a87)),
% 97.93/98.03 inference(scs_inference,[],[586,5212,50,29])).
% 97.93/98.03 cnf(5336,plain,
% 97.93/98.03 (P6(f74(a65),x53361,a86)),
% 97.93/98.03 inference(scs_inference,[],[290,310,316,586,5212,5230,5222,50,29,51,52,70,69,32,102,99,39,27,71,37,38,23])).
% 97.93/98.03 cnf(5340,plain,
% 97.93/98.03 (~P1(f34(a58,a62),f74(a65))),
% 97.93/98.03 inference(scs_inference,[],[290,310,316,586,1866,5212,5230,5222,50,29,51,52,70,69,32,102,99,39,27,71,37,38,23,28,20])).
% 97.93/98.03 cnf(5348,plain,
% 97.93/98.03 (P6(x53481,f74(a65),a80)),
% 97.93/98.03 inference(scs_inference,[],[290,310,316,586,1866,5212,5230,5222,50,29,51,52,70,69,32,102,99,39,27,71,37,38,23,28,20,30,31,36,22])).
% 97.93/98.03 cnf(5350,plain,
% 97.93/98.03 (P1(f22(a2,a71),f74(a71))),
% 97.93/98.03 inference(scs_inference,[],[290,310,316,586,1866,5287,5212,5230,5222,50,29,51,52,70,69,32,102,99,39,27,71,37,38,23,28,20,30,31,36,22,17])).
% 97.93/98.03 cnf(5352,plain,
% 97.93/98.03 (P1(f8(a62),a62)),
% 97.93/98.03 inference(scs_inference,[],[290,310,316,5220,586,1866,5287,5212,5230,5222,50,29,51,52,70,69,32,102,99,39,27,71,37,38,23,28,20,30,31,36,22,17,21])).
% 97.93/98.03 cnf(5358,plain,
% 97.93/98.03 (P1(f29(a62,a2),a62)),
% 97.93/98.03 inference(scs_inference,[],[1,290,310,316,5208,5220,586,1866,5287,5212,5230,5222,1871,1712,50,29,51,52,70,69,32,102,99,39,27,71,37,38,23,28,20,30,31,36,22,17,21,49,48,78])).
% 97.93/98.03 cnf(5359,plain,
% 97.93/98.03 (P6(a62,x53591,a86)),
% 97.93/98.03 inference(rename_variables,[],[5208])).
% 97.93/98.03 cnf(5361,plain,
% 97.93/98.03 (P1(f52(a2,a62),a62)),
% 97.93/98.03 inference(scs_inference,[],[1,290,310,316,5208,5220,5224,586,1866,5287,5212,5230,5222,1871,1712,50,29,51,52,70,69,32,102,99,39,27,71,37,38,23,28,20,30,31,36,22,17,21,49,48,78,79])).
% 97.93/98.03 cnf(5365,plain,
% 97.93/98.03 (P1(x53651,f48(a84,a84))),
% 97.93/98.03 inference(rename_variables,[],[647])).
% 97.93/98.03 cnf(5367,plain,
% 97.93/98.03 (P1(f32(a62,a2),a62)),
% 97.93/98.03 inference(scs_inference,[],[1,290,310,316,5206,5208,5220,5224,586,1866,5287,5212,5230,5222,1871,1712,647,50,29,51,52,70,69,32,102,99,39,27,71,37,38,23,28,20,30,31,36,22,17,21,49,48,78,79,45,41])).
% 97.93/98.03 cnf(5370,plain,
% 97.93/98.03 (~P6(a65,f74(a65),a90)),
% 97.93/98.03 inference(scs_inference,[],[1,290,310,316,5206,5208,5220,5224,586,1866,5287,5212,5230,5222,1871,1712,647,50,29,51,52,70,69,32,102,99,39,27,71,37,38,23,28,20,30,31,36,22,17,21,49,48,78,79,45,41,47])).
% 97.93/98.03 cnf(5372,plain,
% 97.93/98.03 (~P2(a86,a84)),
% 97.93/98.03 inference(scs_inference,[],[1,290,310,316,5054,5206,5208,5359,5220,5224,586,1866,5287,5212,5230,5222,1871,1712,647,50,29,51,52,70,69,32,102,99,39,27,71,37,38,23,28,20,30,31,36,22,17,21,49,48,78,79,45,41,47,94])).
% 97.93/98.03 cnf(5377,plain,
% 97.93/98.03 (P1(x53771,f48(a84,a84))),
% 97.93/98.03 inference(rename_variables,[],[647])).
% 97.93/98.03 cnf(5379,plain,
% 97.93/98.03 (P6(f74(a65),f74(a65),a82)),
% 97.93/98.03 inference(scs_inference,[],[1,290,310,316,5054,5206,5208,5359,5220,5224,586,1866,5287,5212,5230,5222,1871,1712,647,5365,50,29,51,52,70,69,32,102,99,39,27,71,37,38,23,28,20,30,31,36,22,17,21,49,48,78,79,45,41,47,94,43,34])).
% 97.93/98.03 cnf(5382,plain,
% 97.93/98.03 (P1(x53821,f48(a84,a84))),
% 97.93/98.03 inference(rename_variables,[],[647])).
% 97.93/98.03 cnf(5384,plain,
% 97.93/98.03 (P1(f60(a69,a58),a69)),
% 97.93/98.03 inference(scs_inference,[],[1,290,310,316,5054,5206,5208,5359,5220,5224,586,1866,5287,5212,5230,5222,1871,580,1712,647,5365,5377,14,50,29,51,52,70,69,32,102,99,39,27,71,37,38,23,28,20,30,31,36,22,17,21,49,48,78,79,45,41,47,94,43,34,46,76])).
% 97.93/98.03 cnf(5390,plain,
% 97.93/98.03 (P1(f78(a65,a65),a65)),
% 97.93/98.03 inference(scs_inference,[],[1,290,310,316,5054,5206,5208,5359,5220,5224,586,5285,1866,5287,5212,5230,5222,1871,580,1712,647,5365,5377,5382,14,50,29,51,52,70,69,32,102,99,39,27,71,37,38,23,28,20,30,31,36,22,17,21,49,48,78,79,45,41,47,94,43,34,46,76,44,81])).
% 97.93/98.03 cnf(5392,plain,
% 97.93/98.03 (P1(f77(a65,a65),a65)),
% 97.93/98.03 inference(scs_inference,[],[1,290,310,316,5054,5206,5208,5359,5220,5224,586,5285,1866,5287,5212,5230,5222,1871,580,1712,647,5365,5377,5382,14,50,29,51,52,70,69,32,102,99,39,27,71,37,38,23,28,20,30,31,36,22,17,21,49,48,78,79,45,41,47,94,43,34,46,76,44,81,80])).
% 97.93/98.03 cnf(5394,plain,
% 97.93/98.03 (P6(a65,a65,a73)),
% 97.93/98.03 inference(scs_inference,[],[1,290,310,316,5054,5206,5208,5359,5220,5224,586,5285,1866,5287,5212,5230,5222,1871,580,1712,13,647,5365,5377,5382,14,50,29,51,52,70,69,32,102,99,39,27,71,37,38,23,28,20,30,31,36,22,17,21,49,48,78,79,45,41,47,94,43,34,46,76,44,81,80,91])).
% 97.93/98.03 cnf(5398,plain,
% 97.93/98.03 (P1(f35(a62,a71),a62)),
% 97.93/98.03 inference(scs_inference,[],[1,290,310,316,5054,5192,5206,5208,5359,5220,5224,586,5285,1866,5287,5212,5230,5222,1871,580,7,1712,13,647,5365,5377,5382,14,50,29,51,52,70,69,32,102,99,39,27,71,37,38,23,28,20,30,31,36,22,17,21,49,48,78,79,45,41,47,94,43,34,46,76,44,81,80,91,33,74])).
% 97.93/98.03 cnf(5405,plain,
% 97.93/98.03 (~P1(f40(a65,a58),a65)),
% 97.93/98.03 inference(scs_inference,[],[1,290,310,316,5054,5192,5206,5208,5359,5220,5224,586,5285,1866,5287,5212,5230,5222,1871,580,7,1712,13,647,5365,5377,5382,576,14,50,29,51,52,70,69,32,102,99,39,27,71,37,38,23,28,20,30,31,36,22,17,21,49,48,78,79,45,41,47,94,43,34,46,76,44,81,80,91,33,74,1405,15,101])).
% 97.93/98.03 cnf(5419,plain,
% 97.93/98.03 (~P6(x54191,a2,a87)),
% 97.93/98.03 inference(scs_inference,[],[5098,5226,50,29])).
% 97.93/98.03 cnf(5425,plain,
% 97.93/98.03 (~P6(x54251,a2,a81)),
% 97.93/98.03 inference(scs_inference,[],[343,491,5098,5226,50,29,51,52,27])).
% 97.93/98.03 cnf(5433,plain,
% 97.93/98.03 (~P6(a2,x54331,a88)),
% 97.93/98.03 inference(scs_inference,[],[301,326,343,491,5098,5226,50,29,51,52,27,102,99,70,32])).
% 97.93/98.03 cnf(5445,plain,
% 97.93/98.03 (P6(f74(a71),x54451,a86)),
% 97.93/98.03 inference(scs_inference,[],[301,326,341,343,491,5098,5226,5350,50,29,51,52,27,102,99,70,32,71,69,39,37,38,23])).
% 97.93/98.03 cnf(5455,plain,
% 97.93/98.03 (~P6(a2,x54551,a84)),
% 97.93/98.03 inference(scs_inference,[],[301,326,341,343,491,5098,1877,5226,5350,5367,50,29,51,52,27,102,99,70,32,71,69,39,37,38,23,28,15,20,30,31])).
% 97.93/98.03 cnf(5461,plain,
% 97.93/98.03 (P1(f39(a58,a62),f74(a62))),
% 97.93/98.03 inference(scs_inference,[],[301,326,341,343,491,5098,1877,5068,5226,5350,5367,50,29,51,52,27,102,99,70,32,71,69,39,37,38,23,28,15,20,30,31,36,22,17])).
% 97.93/98.03 cnf(5463,plain,
% 97.93/98.03 (~P1(f14(a2,a2),a2)),
% 97.93/98.03 inference(scs_inference,[],[1,301,326,341,343,491,5098,1877,5068,5226,5350,5367,50,29,51,52,27,102,99,70,32,71,69,39,37,38,23,28,15,20,30,31,36,22,17,77])).
% 97.93/98.03 cnf(5467,plain,
% 97.93/98.03 (~P6(f74(a71),a71,a91)),
% 97.93/98.03 inference(scs_inference,[],[1,301,326,341,343,491,5098,1877,5068,5226,5350,5367,5287,50,29,51,52,27,102,99,70,32,71,69,39,37,38,23,28,15,20,30,31,36,22,17,77,45,49])).
% 97.93/98.03 cnf(5470,plain,
% 97.93/98.03 (~P1(x54701,f45(a5,a5))),
% 97.93/98.03 inference(rename_variables,[],[779])).
% 97.93/98.03 cnf(5472,plain,
% 97.93/98.03 (~P6(f74(a71),a71,a90)),
% 97.93/98.03 inference(scs_inference,[],[1,301,326,341,343,491,5098,1877,5068,5226,5350,5367,5287,779,50,29,51,52,27,102,99,70,32,71,69,39,37,38,23,28,15,20,30,31,36,22,17,77,45,49,48,47])).
% 97.93/98.03 cnf(5474,plain,
% 97.93/98.03 (~P2(a73,a83)),
% 97.93/98.03 inference(scs_inference,[],[1,301,326,341,343,491,5098,5279,1877,5068,5226,5350,5367,5042,5287,779,50,29,51,52,27,102,99,70,32,71,69,39,37,38,23,28,15,20,30,31,36,22,17,77,45,49,48,47,94])).
% 97.93/98.03 cnf(5478,plain,
% 97.93/98.03 (~P1(x54781,f45(a5,a5))),
% 97.93/98.03 inference(rename_variables,[],[779])).
% 97.93/98.03 cnf(5483,plain,
% 97.93/98.03 (~P1(x54831,f45(a5,a5))),
% 97.93/98.03 inference(rename_variables,[],[779])).
% 97.93/98.03 cnf(5486,plain,
% 97.93/98.03 (~P1(x54861,a58)),
% 97.93/98.03 inference(rename_variables,[],[14])).
% 97.93/98.03 cnf(5491,plain,
% 97.93/98.03 (~P1(x54911,f45(a5,a5))),
% 97.93/98.03 inference(rename_variables,[],[779])).
% 97.93/98.03 cnf(5499,plain,
% 97.93/98.03 (P6(a62,a62,a4)),
% 97.93/98.03 inference(scs_inference,[],[1,301,326,341,343,491,5098,5279,1877,5068,5236,5226,5350,5367,5310,5379,531,5042,5287,779,5470,5478,5483,5491,14,50,29,51,52,27,102,99,70,32,71,69,39,37,38,23,28,15,20,30,31,36,22,17,77,45,49,48,47,94,43,34,46,76,44,81,80,91,33])).
% 97.93/98.03 cnf(5501,plain,
% 97.93/98.03 (P1(f35(a62,a2),a62)),
% 97.93/98.03 inference(scs_inference,[],[1,301,326,341,343,491,5098,5279,1877,5068,5236,5226,5350,5367,5310,5379,531,5042,5192,5287,779,5470,5478,5483,5491,14,50,29,51,52,27,102,99,70,32,71,69,39,37,38,23,28,15,20,30,31,36,22,17,77,45,49,48,47,94,43,34,46,76,44,81,80,91,33,74])).
% 97.93/98.03 cnf(5504,plain,
% 97.93/98.03 (P1(f19(a62,a58),a62)),
% 97.93/98.03 inference(scs_inference,[],[1,301,326,341,343,491,5299,5098,5279,1877,5068,5236,5226,5350,5367,5310,5379,531,5042,5192,5287,779,5470,5478,5483,5491,14,5486,50,29,51,52,27,102,99,70,32,71,69,39,37,38,23,28,15,20,30,31,36,22,17,77,45,49,48,47,94,43,34,46,76,44,81,80,91,33,74,96])).
% 97.93/98.03 cnf(5509,plain,
% 97.93/98.03 (P1(f76(a62,a62),a62)),
% 97.93/98.03 inference(scs_inference,[],[1,301,326,341,343,491,5299,5098,5279,1877,5068,5236,5226,5350,5367,5310,5379,531,5042,5192,5287,779,5470,5478,5483,5491,14,5486,50,29,51,52,27,102,99,70,32,71,69,39,37,38,23,28,15,20,30,31,36,22,17,77,45,49,48,47,94,43,34,46,76,44,81,80,91,33,74,96,1405,54])).
% 97.93/98.03 cnf(5511,plain,
% 97.93/98.03 (~P1(f22(a62,a71),a71)),
% 97.93/98.03 inference(scs_inference,[],[1,301,326,341,343,491,5299,5098,5279,1877,5068,5236,5226,5350,5367,5310,5379,531,5042,5044,5192,5287,779,5470,5478,5483,5491,14,5486,50,29,51,52,27,102,99,70,32,71,69,39,37,38,23,28,15,20,30,31,36,22,17,77,45,49,48,47,94,43,34,46,76,44,81,80,91,33,74,96,1405,54,90])).
% 97.93/98.03 cnf(5518,plain,
% 97.93/98.03 (~P6(x55181,a65,a87)),
% 97.93/98.03 inference(scs_inference,[],[5258,5405,50,29])).
% 97.93/98.03 cnf(5528,plain,
% 97.93/98.03 (~P6(x55281,a65,a81)),
% 97.93/98.03 inference(scs_inference,[],[487,616,745,5258,5405,50,29,51,69,52,70,27])).
% 97.93/98.03 cnf(5544,plain,
% 97.93/98.03 (P6(f74(a62),x55441,a86)),
% 97.93/98.03 inference(scs_inference,[],[319,487,616,745,5258,5405,5461,779,50,29,51,69,52,70,27,32,99,102,39,71,37,38,23])).
% 97.93/98.03 cnf(5546,plain,
% 97.93/98.03 (~P6(x55461,a65,a84)),
% 97.93/98.03 inference(scs_inference,[],[319,487,616,745,5258,5405,5461,779,50,29,51,69,52,70,27,32,99,102,39,71,37,38,23,28])).
% 97.93/98.03 cnf(5554,plain,
% 97.93/98.03 (~P6(a65,x55541,a84)),
% 97.93/98.03 inference(scs_inference,[],[319,487,616,745,5258,5160,5405,5509,5461,779,50,29,51,69,52,70,27,32,99,102,39,71,37,38,23,28,15,20,30,31])).
% 97.93/98.03 cnf(5558,plain,
% 97.93/98.03 (P6(x55581,f74(a62),a80)),
% 97.93/98.03 inference(scs_inference,[],[319,487,616,745,5258,5160,5405,5509,5461,779,50,29,51,69,52,70,27,32,99,102,39,71,37,38,23,28,15,20,30,31,36,22])).
% 97.93/98.03 cnf(5560,plain,
% 97.93/98.03 (P1(f12(a62,a3),f74(a62))),
% 97.93/98.03 inference(scs_inference,[],[319,487,616,745,5258,5160,5290,5405,5509,5461,779,50,29,51,69,52,70,27,32,99,102,39,71,37,38,23,28,15,20,30,31,36,22,17])).
% 97.93/98.03 cnf(5562,plain,
% 97.93/98.03 (P6(a2,a58,a6)),
% 97.93/98.03 inference(scs_inference,[],[1,319,487,616,745,5258,5160,5290,5405,5509,5461,576,779,50,29,51,69,52,70,27,32,99,102,39,71,37,38,23,28,15,20,30,31,36,22,17,40])).
% 97.93/98.03 cnf(5565,plain,
% 97.93/98.03 (~P1(f14(a65,a2),a2)),
% 97.93/98.03 inference(scs_inference,[],[1,319,487,616,745,5425,5258,5160,5301,5290,5405,5509,5461,576,779,50,29,51,69,52,70,27,32,99,102,39,71,37,38,23,28,15,20,30,31,36,22,17,40,77])).
% 97.93/98.03 cnf(5571,plain,
% 97.93/98.03 (P1(x55711,f48(a84,a84))),
% 97.93/98.03 inference(rename_variables,[],[647])).
% 97.93/98.03 cnf(5573,plain,
% 97.93/98.03 (~P6(f74(a65),a65,a91)),
% 97.93/98.03 inference(scs_inference,[],[1,319,487,616,745,5425,5258,5160,5301,5290,5405,5509,5461,5064,5230,647,576,779,50,29,51,69,52,70,27,32,99,102,39,71,37,38,23,28,15,20,30,31,36,22,17,40,77,47,45,49])).
% 97.93/98.03 cnf(5577,plain,
% 97.93/98.03 (~P2(a86,a85)),
% 97.93/98.03 inference(scs_inference,[],[1,319,487,616,745,5060,5425,5258,5160,5301,5290,5405,5509,5461,5336,5064,1871,5230,647,576,779,50,29,51,69,52,70,27,32,99,102,39,71,37,38,23,28,15,20,30,31,36,22,17,40,77,47,45,49,48,94])).
% 97.93/98.03 cnf(5581,plain,
% 97.93/98.03 (~P6(f48(a84,a84),a62,a73)),
% 97.93/98.03 inference(scs_inference,[],[1,319,487,616,745,5060,5425,5258,5160,5301,5290,5405,5509,5461,5336,5064,1871,5230,647,5571,576,779,50,29,51,69,52,70,27,32,99,102,39,71,37,38,23,28,15,20,30,31,36,22,17,40,77,47,45,49,48,94,43])).
% 97.93/98.03 cnf(5582,plain,
% 97.93/98.03 (P1(x55821,f48(a84,a84))),
% 97.93/98.03 inference(rename_variables,[],[647])).
% 97.93/98.03 cnf(5584,plain,
% 97.93/98.03 (P6(f74(a62),f74(a62),a82)),
% 97.93/98.03 inference(scs_inference,[],[1,319,487,616,745,5060,5425,5258,5160,5301,5290,5405,5509,5461,5336,5064,1871,5230,647,5571,576,779,50,29,51,69,52,70,27,32,99,102,39,71,37,38,23,28,15,20,30,31,36,22,17,40,77,47,45,49,48,94,43,34])).
% 97.93/98.03 cnf(5590,plain,
% 97.93/98.03 (P1(x55901,f48(a84,a84))),
% 97.93/98.03 inference(rename_variables,[],[647])).
% 97.93/98.03 cnf(5592,plain,
% 97.93/98.03 (~P6(f48(a84,a84),a62,a7)),
% 97.93/98.03 inference(scs_inference,[],[1,319,487,616,745,5060,5425,5258,5160,5301,5290,5405,5509,5461,5336,233,5064,1871,5230,647,5571,5582,5590,576,779,14,50,29,51,69,52,70,27,32,99,102,39,71,37,38,23,28,15,20,30,31,36,22,17,40,77,47,45,49,48,94,43,34,76,44,46])).
% 97.93/98.03 cnf(5595,plain,
% 97.93/98.03 (P1(f78(a62,a62),a62)),
% 97.93/98.03 inference(scs_inference,[],[1,319,487,616,745,5060,5425,5258,5499,5160,5301,5290,5352,5405,5509,5461,5336,233,5064,1871,5230,647,5571,5582,5590,576,779,14,50,29,51,69,52,70,27,32,99,102,39,71,37,38,23,28,15,20,30,31,36,22,17,40,77,47,45,49,48,94,43,34,76,44,46,81])).
% 97.93/98.03 cnf(5597,plain,
% 97.93/98.03 (P1(f77(a62,a62),a62)),
% 97.93/98.03 inference(scs_inference,[],[1,319,487,616,745,5060,5425,5258,5499,5160,5301,5290,5352,5405,5509,5461,5336,233,5064,1871,5230,647,5571,5582,5590,576,779,14,50,29,51,69,52,70,27,32,99,102,39,71,37,38,23,28,15,20,30,31,36,22,17,40,77,47,45,49,48,94,43,34,76,44,46,81,80])).
% 97.93/98.03 cnf(5599,plain,
% 97.93/98.03 (P6(a62,a62,a73)),
% 97.93/98.03 inference(scs_inference,[],[1,319,487,616,745,5060,5425,5258,5499,5160,5301,5290,5352,5405,5509,5461,5336,233,5064,1871,5230,13,647,5571,5582,5590,576,779,14,50,29,51,69,52,70,27,32,99,102,39,71,37,38,23,28,15,20,30,31,36,22,17,40,77,47,45,49,48,94,43,34,76,44,46,81,80,91])).
% 97.93/98.03 cnf(5601,plain,
% 97.93/98.03 (P6(f74(a62),f74(a62),a4)),
% 97.93/98.03 inference(scs_inference,[],[1,319,487,616,745,5060,5425,5258,5499,5160,5301,5290,5352,5405,5509,5461,5336,233,5064,1871,5230,13,647,5571,5582,5590,576,779,14,50,29,51,69,52,70,27,32,99,102,39,71,37,38,23,28,15,20,30,31,36,22,17,40,77,47,45,49,48,94,43,34,76,44,46,81,80,91,33])).
% 97.93/98.03 cnf(5603,plain,
% 97.93/98.03 (~P1(f22(a62,a2),a2)),
% 97.93/98.03 inference(scs_inference,[],[1,319,487,616,745,5060,5419,5425,5258,5499,5160,5301,5290,5352,5405,5509,5461,5336,233,5064,1871,5230,13,647,5571,5582,5590,576,779,14,50,29,51,69,52,70,27,32,99,102,39,71,37,38,23,28,15,20,30,31,36,22,17,40,77,47,45,49,48,94,43,34,76,44,46,81,80,91,33,90])).
% 97.93/98.03 cnf(5610,plain,
% 97.93/98.03 (~P5(a80,a85)),
% 97.93/98.03 inference(scs_inference,[],[1,319,487,616,745,5060,5419,5425,5258,5499,5160,5301,5290,4980,5352,5405,5509,5461,5336,233,835,5064,1871,5230,13,647,5571,5582,5590,576,779,14,50,29,51,69,52,70,27,32,99,102,39,71,37,38,23,28,15,20,30,31,36,22,17,40,77,47,45,49,48,94,43,34,76,44,46,81,80,91,33,90,1405,65,104])).
% 97.93/98.03 cnf(5613,plain,
% 97.93/98.03 (P1(f36(a62,a3),a62)),
% 97.93/98.03 inference(scs_inference,[],[1,319,487,616,745,5060,5198,5419,5425,5258,5499,5160,5301,5290,4980,5352,5405,5509,5461,5336,233,835,5064,1871,5230,13,647,5571,5582,5590,576,779,14,8,50,29,51,69,52,70,27,32,99,102,39,71,37,38,23,28,15,20,30,31,36,22,17,40,77,47,45,49,48,94,43,34,76,44,46,81,80,91,33,90,1405,65,104,93])).
% 97.93/98.03 cnf(5634,plain,
% 97.93/98.03 (~P6(a59,x56341,a89)),
% 97.93/98.03 inference(scs_inference,[],[734,789,5372,5266,779,50,29,51,69,39])).
% 97.93/98.03 cnf(5648,plain,
% 97.93/98.03 (~P6(a59,x56481,a83)),
% 97.93/98.03 inference(scs_inference,[],[331,734,787,789,1214,5372,5266,779,951,50,29,51,69,39,32,52,99,70,27,71,37])).
% 97.93/98.03 cnf(5652,plain,
% 97.93/98.03 (~P6(a59,x56521,a85)),
% 97.93/98.03 inference(scs_inference,[],[331,734,787,789,1214,5372,5266,779,951,50,29,51,69,39,32,52,99,70,27,71,37,102,38])).
% 97.93/98.03 cnf(5654,plain,
% 97.93/98.03 (P6(a59,x56541,a86)),
% 97.93/98.03 inference(scs_inference,[],[331,734,787,789,1214,5372,5266,779,951,50,29,51,69,39,32,52,99,70,27,71,37,102,38,23])).
% 97.93/98.03 cnf(5668,plain,
% 97.93/98.03 (P6(x56681,a59,a80)),
% 97.93/98.03 inference(scs_inference,[],[331,734,787,789,1214,5372,5056,5266,5358,779,951,50,29,51,69,39,32,52,99,70,27,71,37,102,38,23,28,15,20,30,31,36,22])).
% 97.93/98.03 cnf(5672,plain,
% 97.93/98.03 (P1(f8(a59),a59)),
% 97.93/98.03 inference(scs_inference,[],[331,734,787,789,1214,5372,5056,5218,5266,5358,779,951,50,29,51,69,39,32,52,99,70,27,71,37,102,38,23,28,15,20,30,31,36,22,17,21])).
% 97.93/98.03 cnf(5676,plain,
% 97.93/98.03 (P1(f32(a59,a2),a59)),
% 97.93/98.03 inference(scs_inference,[],[1,331,734,787,789,1214,5372,5056,5218,5266,5358,779,951,50,29,51,69,39,32,52,99,70,27,71,37,102,38,23,28,15,20,30,31,36,22,17,21,79,41])).
% 97.93/98.03 cnf(5680,plain,
% 97.93/98.03 (~P6(a65,a62,a90)),
% 97.93/98.03 inference(scs_inference,[],[1,331,734,787,789,1214,5372,5056,5218,5266,5358,10,5,779,951,50,29,51,69,39,32,52,99,70,27,71,37,102,38,23,28,15,20,30,31,36,22,17,21,79,41,49,47])).
% 97.93/98.03 cnf(5682,plain,
% 97.93/98.03 (~P1(f14(a2,a65),a65)),
% 97.93/98.03 inference(scs_inference,[],[1,331,734,787,789,1214,5528,5372,5056,5218,5266,5358,10,5,779,951,50,29,51,69,39,32,52,99,70,27,71,37,102,38,23,28,15,20,30,31,36,22,17,21,79,41,49,47,77])).
% 97.93/98.03 cnf(5688,plain,
% 97.93/98.03 (~P1(x56881,f45(a5,a5))),
% 97.93/98.03 inference(rename_variables,[],[779])).
% 97.93/98.03 cnf(5690,plain,
% 97.93/98.03 (~P2(a6,a88)),
% 97.93/98.03 inference(scs_inference,[],[1,331,734,787,789,1214,5562,5433,5528,5372,5056,5218,5228,5560,5266,5358,10,5,5290,779,951,50,29,51,69,39,32,52,99,70,27,71,37,102,38,23,28,15,20,30,31,36,22,17,21,79,41,49,47,77,45,48,94])).
% 97.93/98.03 cnf(5691,plain,
% 97.93/98.03 (~P6(a2,x56911,a88)),
% 97.93/98.03 inference(rename_variables,[],[5433])).
% 97.93/98.03 cnf(5694,plain,
% 97.93/98.03 (~P1(x56941,f45(a5,a5))),
% 97.93/98.03 inference(rename_variables,[],[779])).
% 97.93/98.03 cnf(5702,plain,
% 97.93/98.03 (~P1(x57021,f45(a5,a5))),
% 97.93/98.03 inference(rename_variables,[],[779])).
% 97.93/98.03 cnf(5704,plain,
% 97.93/98.03 (~P6(a62,f74(a62),a7)),
% 97.93/98.03 inference(scs_inference,[],[1,331,734,787,789,1214,5562,5433,5528,5372,5056,5218,5228,5560,5266,5358,568,10,5,5290,779,5688,5694,951,14,50,29,51,69,39,32,52,99,70,27,71,37,102,38,23,28,15,20,30,31,36,22,17,21,79,41,49,47,77,45,48,94,43,34,76,46,44])).
% 97.93/98.03 cnf(5707,plain,
% 97.93/98.03 (~P1(x57071,f45(a5,a5))),
% 97.93/98.03 inference(rename_variables,[],[779])).
% 97.93/98.03 cnf(5715,plain,
% 97.93/98.03 (~P1(f23(a71,a3),a71)),
% 97.93/98.03 inference(scs_inference,[],[1,331,734,787,789,1214,5562,5062,5433,5691,5528,5372,5056,5218,5228,5560,5266,5358,568,10,5,5290,779,5688,5694,5702,5707,951,14,8,50,29,51,69,39,32,52,99,70,27,71,37,102,38,23,28,15,20,30,31,36,22,17,21,79,41,49,47,77,45,48,94,43,34,76,46,44,81,80,91,98])).
% 97.93/98.03 cnf(5720,plain,
% 97.93/98.03 (P6(f46(a88,a88),x57201,a80)),
% 97.93/98.03 inference(rename_variables,[],[980])).
% 97.93/98.03 cnf(5722,plain,
% 97.93/98.03 (P3(a80,a85)),
% 97.93/98.03 inference(scs_inference,[],[1,331,734,787,789,1214,5562,5062,5433,5691,5528,5372,5056,5218,5228,4994,5560,5266,5358,568,980,5720,10,5,5290,779,5688,5694,5702,5707,951,14,8,50,29,51,69,39,32,52,99,70,27,71,37,102,38,23,28,15,20,30,31,36,22,17,21,79,41,49,47,77,45,48,94,43,34,76,46,44,81,80,91,98,105,100])).
% 97.93/98.03 cnf(5725,plain,
% 97.93/98.03 (P6(a59,a59,a4)),
% 97.93/98.03 inference(scs_inference,[],[1,331,734,787,789,1214,5562,5062,5433,5691,5528,5372,5056,5218,5228,4994,5560,5266,5358,568,980,5720,10,5,5290,779,5688,5694,5702,5707,951,14,8,50,29,51,69,39,32,52,99,70,27,71,37,102,38,23,28,15,20,30,31,36,22,17,21,79,41,49,47,77,45,48,94,43,34,76,46,44,81,80,91,98,105,100,33])).
% 97.93/98.03 cnf(5727,plain,
% 97.93/98.03 (~P1(f22(a2,a65),a65)),
% 97.93/98.03 inference(scs_inference,[],[1,331,734,787,789,1214,5562,5062,5433,5691,5518,5528,5372,5056,5218,5228,4994,5463,5560,5266,5358,568,980,5720,10,5,5290,779,5688,5694,5702,5707,951,14,8,50,29,51,69,39,32,52,99,70,27,71,37,102,38,23,28,15,20,30,31,36,22,17,21,79,41,49,47,77,45,48,94,43,34,76,46,44,81,80,91,98,105,100,33,90])).
% 97.93/98.03 cnf(5730,plain,
% 97.93/98.03 (~P6(a59,a58,a75)),
% 97.93/98.03 inference(scs_inference,[],[1,331,734,787,789,1214,5562,5062,5433,5691,5518,5528,5372,5056,5218,5228,4994,5463,5560,5266,5358,568,980,5720,10,5,5290,779,5688,5694,5702,5707,951,14,8,50,29,51,69,39,32,52,99,70,27,71,37,102,38,23,28,15,20,30,31,36,22,17,21,79,41,49,47,77,45,48,94,43,34,76,46,44,81,80,91,98,105,100,33,90,1405])).
% 97.93/98.03 cnf(5732,plain,
% 97.93/98.03 (P1(f76(a59,a59),a59)),
% 97.93/98.03 inference(scs_inference,[],[1,331,734,787,789,1214,5562,5062,5433,5691,5518,5528,5372,5056,5218,5228,4994,5463,5560,5266,5358,568,980,5720,10,5,5290,779,5688,5694,5702,5707,951,14,8,50,29,51,69,39,32,52,99,70,27,71,37,102,38,23,28,15,20,30,31,36,22,17,21,79,41,49,47,77,45,48,94,43,34,76,46,44,81,80,91,98,105,100,33,90,1405,54])).
% 97.93/98.03 cnf(5755,plain,
% 97.93/98.03 (~P6(a69,x57551,a89)),
% 97.93/98.03 inference(scs_inference,[],[1331,5474,5384,951,14,50,29,51,32,39])).
% 97.93/98.03 cnf(5771,plain,
% 97.93/98.03 (~P6(a69,x57711,a83)),
% 97.93/98.03 inference(scs_inference,[],[345,1210,1331,1339,5474,5384,951,14,636,50,29,51,32,39,69,70,52,27,71,99,102,37])).
% 97.93/98.03 cnf(5773,plain,
% 97.93/98.03 (P6(a69,x57731,a86)),
% 97.93/98.03 inference(scs_inference,[],[345,1210,1331,1339,5474,5384,951,14,636,50,29,51,32,39,69,70,52,27,71,99,102,37,23])).
% 97.93/98.03 cnf(5775,plain,
% 97.93/98.03 (~P6(a69,x57751,a85)),
% 97.93/98.03 inference(scs_inference,[],[345,1210,1331,1339,5474,5384,951,14,636,50,29,51,32,39,69,70,52,27,71,99,102,37,23,38])).
% 97.93/98.03 cnf(5789,plain,
% 97.93/98.03 (P6(x57891,a69,a80)),
% 97.93/98.03 inference(scs_inference,[],[345,1210,1331,1339,5474,5390,5361,5384,951,14,636,50,29,51,32,39,69,70,52,27,71,99,102,37,23,38,28,15,20,30,31,36,22])).
% 97.93/98.03 cnf(5793,plain,
% 97.93/98.03 (P1(f8(a69),a69)),
% 97.93/98.03 inference(scs_inference,[],[345,1210,1331,1339,5474,5390,5151,5361,5384,951,14,636,50,29,51,32,39,69,70,52,27,71,99,102,37,23,38,28,15,20,30,31,36,22,17,21])).
% 97.93/98.03 cnf(5802,plain,
% 97.93/98.03 (P6(a59,x58021,a86)),
% 97.93/98.03 inference(rename_variables,[],[5654])).
% 97.93/98.03 cnf(5804,plain,
% 97.93/98.03 (~P6(a69,a71,a91)),
% 97.93/98.03 inference(scs_inference,[],[345,1210,1331,1339,5648,5654,5668,5474,5390,5151,5361,5384,12,6,951,14,636,50,29,51,32,39,69,70,52,27,71,99,102,37,23,38,28,15,20,30,31,36,22,17,21,41,79,78,49])).
% 97.93/98.03 cnf(5809,plain,
% 97.93/98.03 (P1(x58091,f48(a84,a84))),
% 97.93/98.03 inference(rename_variables,[],[647])).
% 97.93/98.03 cnf(5813,plain,
% 97.93/98.03 (~P2(a86,a75)),
% 97.93/98.03 inference(scs_inference,[],[345,1210,1331,1339,5730,5648,5654,5802,5668,5474,5390,5151,5361,5727,5384,1871,12,6,5230,647,951,14,636,50,29,51,32,39,69,70,52,27,71,99,102,37,23,38,28,15,20,30,31,36,22,17,21,41,79,78,49,47,45,48,94])).
% 97.93/98.03 cnf(5818,plain,
% 97.93/98.03 (P6(a69,a69,a82)),
% 97.93/98.03 inference(scs_inference,[],[345,1210,1331,1339,5730,5648,5654,5802,5668,5474,5390,5151,5340,5361,5727,5384,1871,1866,12,6,5230,647,951,14,636,50,29,51,32,39,69,70,52,27,71,99,102,37,23,38,28,15,20,30,31,36,22,17,21,41,79,78,49,47,45,48,94,43,34])).
% 97.93/98.03 cnf(5820,plain,
% 97.93/98.03 (P1(f60(a56,a58),a56)),
% 97.93/98.03 inference(scs_inference,[],[345,1210,1331,1339,5730,5648,5654,5802,5668,5474,5390,5151,5340,5361,5727,5384,278,1871,1866,12,6,5230,647,951,14,636,50,29,51,32,39,69,70,52,27,71,99,102,37,23,38,28,15,20,30,31,36,22,17,21,41,79,78,49,47,45,48,94,43,34,76])).
% 97.93/98.03 cnf(5828,plain,
% 97.93/98.03 (P1(f78(a59,a59),a59)),
% 97.93/98.03 inference(scs_inference,[],[345,1210,1331,1339,5730,5648,5654,5802,5668,5474,5725,5390,5151,5340,5732,5361,5727,5384,278,1871,1866,12,6,5230,647,5809,951,14,636,50,29,51,32,39,69,70,52,27,71,99,102,37,23,38,28,15,20,30,31,36,22,17,21,41,79,78,49,47,45,48,94,43,34,76,46,44,81])).
% 97.93/98.03 cnf(5830,plain,
% 97.93/98.03 (P1(f77(a59,a59),a59)),
% 97.93/98.03 inference(scs_inference,[],[345,1210,1331,1339,5730,5648,5654,5802,5668,5474,5725,5390,5151,5340,5732,5361,5727,5384,278,1871,1866,12,6,5230,647,5809,951,14,636,50,29,51,32,39,69,70,52,27,71,99,102,37,23,38,28,15,20,30,31,36,22,17,21,41,79,78,49,47,45,48,94,43,34,76,46,44,81,80])).
% 97.93/98.03 cnf(5834,plain,
% 97.93/98.03 (P6(a69,a69,a4)),
% 97.93/98.03 inference(scs_inference,[],[345,1210,1331,1339,5730,5648,5654,5802,5668,5474,5725,5390,5151,5340,5732,5361,5727,5384,278,1871,1866,12,6,5230,13,647,5809,951,14,636,50,29,51,32,39,69,70,52,27,71,99,102,37,23,38,28,15,20,30,31,36,22,17,21,41,79,78,49,47,45,48,94,43,34,76,46,44,81,80,91,33])).
% 97.93/98.03 cnf(5836,plain,
% 97.93/98.03 (~P1(f22(a62,a65),a65)),
% 97.93/98.03 inference(scs_inference,[],[345,1210,1331,1339,5730,5648,5654,5802,5668,5474,5725,5390,5151,5340,5732,5361,5727,5384,278,5518,1871,1866,12,6,5230,13,647,5809,951,14,636,50,29,51,32,39,69,70,52,27,71,99,102,37,23,38,28,15,20,30,31,36,22,17,21,41,79,78,49,47,45,48,94,43,34,76,46,44,81,80,91,33,90])).
% 97.93/98.03 cnf(5844,plain,
% 97.93/98.03 (P1(f76(a69,a69),a69)),
% 97.93/98.03 inference(scs_inference,[],[1,345,1210,1331,1339,5730,5634,5648,5654,5802,5668,5474,5725,5390,5151,5340,5732,5361,5727,5384,5565,278,5518,1871,1866,12,6,5230,13,647,5809,951,14,636,50,29,51,32,39,69,70,52,27,71,99,102,37,23,38,28,15,20,30,31,36,22,17,21,41,79,78,49,47,45,48,94,43,34,76,46,44,81,80,91,33,90,74,1405,54])).
% 97.93/98.03 cnf(5860,plain,
% 97.93/98.03 (~P6(a56,x58601,a89)),
% 97.93/98.03 inference(scs_inference,[],[1347,5813,5820,636,50,51,29,39])).
% 97.93/98.03 cnf(5874,plain,
% 97.93/98.03 (~P6(a56,x58741,a83)),
% 97.93/98.03 inference(scs_inference,[],[355,1347,1356,5813,5820,636,50,51,29,39,69,32,70,71,52,99,37])).
% 97.93/98.03 cnf(5878,plain,
% 97.93/98.03 (~P6(a56,x58781,a85)),
% 97.93/98.03 inference(scs_inference,[],[355,1347,1356,5813,5820,636,50,51,29,39,69,32,70,71,52,99,37,102,38])).
% 97.93/98.03 cnf(5880,plain,
% 97.93/98.03 (P6(a56,x58801,a86)),
% 97.93/98.03 inference(scs_inference,[],[355,1347,1356,5813,5820,636,50,51,29,39,69,32,70,71,52,99,37,102,38,23])).
% 97.93/98.03 cnf(5894,plain,
% 97.93/98.03 (P6(x58941,a56,a80)),
% 97.93/98.03 inference(scs_inference,[],[355,1347,1356,5813,5392,5398,5820,14,636,50,51,29,39,69,32,70,71,52,99,37,102,38,23,28,15,20,30,31,36,22])).
% 97.93/98.03 cnf(5901,plain,
% 97.93/98.03 (P6(x59011,a69,a80)),
% 97.93/98.03 inference(rename_variables,[],[5789])).
% 97.93/98.03 cnf(5916,plain,
% 97.93/98.03 (~P1(x59161,f45(a5,a5))),
% 97.93/98.03 inference(rename_variables,[],[779])).
% 97.93/98.03 cnf(5919,plain,
% 97.93/98.03 (~P1(x59191,f45(a5,a5))),
% 97.93/98.03 inference(rename_variables,[],[779])).
% 97.93/98.03 cnf(5921,plain,
% 97.93/98.03 (~P2(a80,a84)),
% 97.93/98.03 inference(scs_inference,[],[1,355,1347,1356,5813,5455,5771,5773,5789,5901,5392,5110,5676,5398,5820,5340,10,5,5086,779,5916,14,636,50,51,29,39,69,32,70,71,52,99,37,102,38,23,28,15,20,30,31,36,22,17,21,79,49,78,41,47,45,48,43,94])).
% 97.93/98.03 cnf(5940,plain,
% 97.93/98.03 (~P6(a69,x59401,a89)),
% 97.93/98.03 inference(rename_variables,[],[5755])).
% 97.93/98.03 cnf(5942,plain,
% 97.93/98.03 (P6(a56,a56,a4)),
% 97.93/98.03 inference(scs_inference,[],[1,355,1347,1356,5813,5455,5755,5771,5773,5789,5901,5818,5834,5392,5110,5676,5844,5398,5820,583,5340,10,5,5086,779,5916,5919,14,636,50,51,29,39,69,32,70,71,52,99,37,102,38,23,28,15,20,30,31,36,22,17,21,79,49,78,41,47,45,48,43,94,34,46,76,44,81,80,91,33])).
% 97.93/98.03 cnf(5949,plain,
% 97.93/98.03 (P1(f76(a56,a56),a56)),
% 97.93/98.03 inference(scs_inference,[],[1,355,1347,1356,5813,5455,5755,5940,5771,5773,5789,5901,5818,5834,5392,5110,5676,5844,5398,5820,583,5340,10,5,5086,779,5916,5919,14,636,50,51,29,39,69,32,70,71,52,99,37,102,38,23,28,15,20,30,31,36,22,17,21,79,49,78,41,47,45,48,43,94,34,46,76,44,81,80,91,33,74,1405,54])).
% 97.93/98.03 cnf(5951,plain,
% 97.93/98.03 (~P1(f40(a2,a58),a2)),
% 97.93/98.03 inference(scs_inference,[],[1,355,1347,1356,5813,5455,5755,5940,5771,5773,5789,5901,5818,5834,5392,5110,5676,5844,5398,5820,583,5433,5340,10,5,5086,576,779,5916,5919,14,636,50,51,29,39,69,32,70,71,52,99,37,102,38,23,28,15,20,30,31,36,22,17,21,79,49,78,41,47,45,48,43,94,34,46,76,44,81,80,91,33,74,1405,54,101])).
% 97.93/98.03 cnf(5965,plain,
% 97.93/98.03 (~P6(a71,x59651,a89)),
% 97.93/98.03 inference(scs_inference,[],[1389,1391,5577,7,50,51,69,39])).
% 97.93/98.03 cnf(5975,plain,
% 97.93/98.03 (~P6(a71,x59751,a83)),
% 97.93/98.03 inference(scs_inference,[],[362,1389,1391,1655,1657,5577,7,50,51,69,39,70,52,99,71,37])).
% 97.93/98.03 cnf(5977,plain,
% 97.93/98.03 (~P6(a71,x59771,a85)),
% 97.93/98.03 inference(scs_inference,[],[362,1389,1391,1655,1657,5577,7,50,51,69,39,70,52,99,71,37,38])).
% 97.93/98.03 cnf(5981,plain,
% 97.93/98.03 (P6(a71,x59811,a86)),
% 97.93/98.03 inference(scs_inference,[],[362,1389,1391,1655,1657,5577,7,50,51,69,39,70,52,99,71,37,38,102,23])).
% 97.93/98.03 cnf(5991,plain,
% 97.93/98.03 (P6(x59911,a71,a80)),
% 97.93/98.03 inference(scs_inference,[],[362,1389,1391,1655,1657,5577,5162,5501,7,636,50,51,69,39,70,52,99,71,37,38,102,23,15,20,31,36,22])).
% 97.93/98.03 cnf(5993,plain,
% 97.93/98.03 (P1(f40(a2,a58),f74(a2))),
% 97.93/98.03 inference(scs_inference,[],[362,1389,1391,1655,1657,5577,5162,5501,5951,7,636,50,51,69,39,70,52,99,71,37,38,102,23,15,20,31,36,22,17])).
% 97.93/98.03 cnf(6004,plain,
% 97.93/98.03 (P6(x60041,a56,a80)),
% 97.93/98.03 inference(rename_variables,[],[5894])).
% 97.93/98.03 cnf(6008,plain,
% 97.93/98.03 (~P6(a69,a71,a90)),
% 97.93/98.03 inference(scs_inference,[],[1,362,1389,1391,1655,1657,5577,5874,5880,5894,5162,5501,5951,7,1602,12,6,636,11,50,51,69,39,70,52,99,71,37,38,102,23,15,20,31,36,22,17,21,78,41,79,49,47])).
% 97.93/98.03 cnf(6011,plain,
% 97.93/98.03 (P1(x60111,f48(a84,a84))),
% 97.93/98.03 inference(rename_variables,[],[647])).
% 97.93/98.03 cnf(6015,plain,
% 97.93/98.03 (~P2(a80,a85)),
% 97.93/98.03 inference(scs_inference,[],[1,362,1389,1391,1655,1657,5577,5652,5874,5880,5894,6004,5162,5501,5951,7,1602,12,6,5350,5287,647,636,11,50,51,69,39,70,52,99,71,37,38,102,23,15,20,31,36,22,17,21,78,41,79,49,47,45,48,94])).
% 97.93/98.03 cnf(6020,plain,
% 97.93/98.03 (P1(x60201,f48(a84,a84))),
% 97.93/98.03 inference(rename_variables,[],[647])).
% 97.93/98.03 cnf(6024,plain,
% 97.93/98.03 (~P6(f48(a84,a84),a2,a7)),
% 97.93/98.03 inference(scs_inference,[],[1,362,1389,1391,1655,1657,5577,5652,5874,5880,5894,6004,5162,5501,5951,7,1602,12,6,5350,5287,647,6011,6020,636,11,50,51,69,39,70,52,99,71,37,38,102,23,15,20,31,36,22,17,21,78,41,79,49,47,45,48,94,43,34,46])).
% 97.93/98.03 cnf(6025,plain,
% 97.93/98.03 (P1(x60251,f48(a84,a84))),
% 97.93/98.03 inference(rename_variables,[],[647])).
% 97.93/98.03 cnf(6036,plain,
% 97.93/98.03 (P6(a71,a71,a4)),
% 97.93/98.03 inference(scs_inference,[],[1,362,1389,1391,1655,1657,5577,5652,5874,5880,5894,6004,5942,5162,5949,5501,5951,7,1602,12,6,5350,5287,13,647,6011,6020,6025,636,11,50,51,69,39,70,52,99,71,37,38,102,23,15,20,31,36,22,17,21,78,41,79,49,47,45,48,94,43,34,46,44,81,80,91,33])).
% 97.93/98.03 cnf(6043,plain,
% 97.93/98.03 (P1(f76(a71,a71),a71)),
% 97.93/98.03 inference(scs_inference,[],[1,362,1389,1391,1655,1657,5577,5652,5860,5874,5880,5894,6004,5942,5162,5949,5501,5951,7,1602,12,6,5350,5287,13,647,6011,6020,6025,636,11,50,51,69,39,70,52,99,71,37,38,102,23,15,20,31,36,22,17,21,78,41,79,49,47,45,48,94,43,34,46,44,81,80,91,33,74,1405,54])).
% 97.93/98.03 cnf(6069,plain,
% 97.93/98.03 (~P6(f74(a2),x60691,a85)),
% 97.93/98.03 inference(scs_inference,[],[369,1674,1676,1705,1707,5921,5993,50,69,51,39,70,52,99,37,71,38])).
% 97.93/98.03 cnf(6073,plain,
% 97.93/98.03 (P6(f74(a2),x60731,a86)),
% 97.93/98.03 inference(scs_inference,[],[369,1674,1676,1705,1707,5921,5993,50,69,51,39,70,52,99,37,71,38,102,23])).
% 97.93/98.03 cnf(6083,plain,
% 97.93/98.03 (P1(f14(a2,a71),f74(a71))),
% 97.93/98.03 inference(scs_inference,[],[369,1674,1676,1705,1707,5921,5072,5993,5595,5247,50,69,51,39,70,52,99,37,71,38,102,23,15,20,36,22,17])).
% 97.93/98.03 cnf(6091,plain,
% 97.93/98.03 (P1(f52(a2,a71),a71)),
% 97.93/98.03 inference(scs_inference,[],[1,369,1674,1676,1705,1707,5921,5975,5981,5991,5072,5993,5595,5247,50,69,51,39,70,52,99,37,71,38,102,23,15,20,36,22,17,41,78,79])).
% 97.93/98.03 cnf(6092,plain,
% 97.93/98.03 (P6(x60921,a71,a80)),
% 97.93/98.03 inference(rename_variables,[],[5991])).
% 97.93/98.03 cnf(6094,plain,
% 97.93/98.03 (~P6(f74(a2),a2,a91)),
% 97.93/98.03 inference(scs_inference,[],[1,369,1674,1676,1705,1707,5921,5975,5981,5991,5072,5993,5595,5247,5951,50,69,51,39,70,52,99,37,71,38,102,23,15,20,36,22,17,41,78,79,49])).
% 97.93/98.03 cnf(6099,plain,
% 97.93/98.03 (~P1(x60991,f45(a5,a5))),
% 97.93/98.03 inference(rename_variables,[],[779])).
% 97.93/98.03 cnf(6101,plain,
% 97.93/98.03 (~P6(a71,a69,a75)),
% 97.93/98.03 inference(scs_inference,[],[1,369,1674,1676,1705,1707,5921,5975,5981,5991,5072,5793,5993,5595,5247,5951,12,6,779,50,69,51,39,70,52,99,37,71,38,102,23,15,20,36,22,17,41,78,79,49,47,48,45])).
% 97.93/98.03 cnf(6104,plain,
% 97.93/98.03 (~P1(x61041,f45(a5,a5))),
% 97.93/98.03 inference(rename_variables,[],[779])).
% 97.93/98.03 cnf(6106,plain,
% 97.93/98.03 (~P2(a80,a91)),
% 97.93/98.03 inference(scs_inference,[],[1,369,1674,1676,1705,1707,5804,5921,5975,5981,5991,6092,5072,5793,5993,5595,5247,5951,12,6,779,6099,50,69,51,39,70,52,99,37,71,38,102,23,15,20,36,22,17,41,78,79,49,47,48,45,43,94])).
% 97.93/98.03 cnf(6118,plain,
% 97.93/98.03 (P1(f77(a71,a71),a71)),
% 97.93/98.03 inference(scs_inference,[],[1,369,1674,1676,1705,1707,5804,5921,5975,5981,5991,6092,6036,5072,5793,6043,5993,5595,5247,5340,5951,5086,12,6,779,6099,6104,50,69,51,39,70,52,99,37,71,38,102,23,15,20,36,22,17,41,78,79,49,47,48,45,43,94,34,46,44,81,80])).
% 97.93/98.03 cnf(6122,plain,
% 97.93/98.03 (P6(f74(a2),f74(a2),a4)),
% 97.93/98.03 inference(scs_inference,[],[1,369,1674,1676,1705,1707,5804,5921,5975,5981,5991,6092,6036,5072,5793,6043,5993,5595,5247,5340,5951,5086,12,6,13,779,6099,6104,50,69,51,39,70,52,99,37,71,38,102,23,15,20,36,22,17,41,78,79,49,47,48,45,43,94,34,46,44,81,80,91,33])).
% 97.93/98.03 cnf(6124,plain,
% 97.93/98.03 (P1(f35(a71,a2),a71)),
% 97.93/98.03 inference(scs_inference,[],[1,369,1674,1676,1705,1707,5804,5921,5965,5975,5981,5991,6092,6036,5072,5793,6043,5993,5595,5247,5603,5340,5951,5086,12,6,13,779,6099,6104,50,69,51,39,70,52,99,37,71,38,102,23,15,20,36,22,17,41,78,79,49,47,48,45,43,94,34,46,44,81,80,91,33,74])).
% 97.93/98.03 cnf(6129,plain,
% 97.93/98.03 (P6(a59,a58,a6)),
% 97.93/98.03 inference(scs_inference,[],[1,369,1674,1676,1705,1707,5804,5921,5965,5975,5981,5991,6092,6036,5072,5672,5793,6043,5993,5595,5247,5603,5340,5951,5086,12,6,13,576,779,6099,6104,50,69,51,39,70,52,99,37,71,38,102,23,15,20,36,22,17,41,78,79,49,47,48,45,43,94,34,46,44,81,80,91,33,74,1405,40])).
% 97.93/98.03 cnf(6135,plain,
% 97.93/98.03 (~P5(a90,a90)),
% 97.93/98.03 inference(scs_inference,[],[1,369,1674,1676,1705,1707,5804,5921,5965,5975,5981,5991,6092,6036,5072,5672,5793,6043,5993,5595,5247,5603,240,5168,5340,5951,5086,12,6,13,576,779,6099,6104,14,50,69,51,39,70,52,99,37,71,38,102,23,15,20,36,22,17,41,78,79,49,47,48,45,43,94,34,46,44,81,80,91,33,74,1405,40,76,104])).
% 97.93/98.03 cnf(6137,plain,
% 97.93/98.03 (P1(f36(a69,a3),a69)),
% 97.93/98.03 inference(scs_inference,[],[1,369,1674,1676,1705,1707,5804,5921,5775,5965,5975,5981,5991,6092,6036,5072,5672,5793,6043,5993,5595,5247,5603,240,5168,5340,5951,5086,12,6,13,576,779,6099,6104,14,8,50,69,51,39,70,52,99,37,71,38,102,23,15,20,36,22,17,41,78,79,49,47,48,45,43,94,34,46,44,81,80,91,33,74,1405,40,76,104,93])).
% 97.93/98.03 cnf(6143,plain,
% 97.93/98.03 (P1(f38(a59,a58),a59)),
% 97.93/98.03 inference(scs_inference,[],[1,369,1674,1676,1705,1707,5804,5921,5775,5965,5975,5981,5991,6092,6008,6036,5072,5672,5793,6043,5993,5595,5247,5603,240,5168,5340,5951,5086,12,6,13,576,779,6099,6104,14,8,50,69,51,39,70,52,99,37,71,38,102,23,15,20,36,22,17,41,78,79,49,47,48,45,43,94,34,46,44,81,80,91,33,74,1405,40,76,104,93,88,65])).
% 97.93/98.03 cnf(6152,plain,
% 97.93/98.03 (~P6(f48(a84,a84),x61521,a89)),
% 97.93/98.03 inference(scs_inference,[],[1823,1825,5690,647,50,69,51,39])).
% 97.93/98.03 cnf(6160,plain,
% 97.93/98.03 (~P6(f48(a84,a84),x61601,a83)),
% 97.93/98.03 inference(scs_inference,[],[1823,1825,1832,1834,5690,647,50,69,51,39,70,52,99,37])).
% 97.93/98.03 cnf(6166,plain,
% 97.93/98.03 (~P6(f48(a84,a84),x61661,a85)),
% 97.93/98.03 inference(scs_inference,[],[376,1823,1825,1832,1834,5690,647,50,69,51,39,70,52,99,37,102,71,38])).
% 97.93/98.03 cnf(6168,plain,
% 97.93/98.03 (P6(f48(a84,a84),x61681,a86)),
% 97.93/98.03 inference(scs_inference,[],[376,1823,1825,1832,1834,5690,647,50,69,51,39,70,52,99,37,102,71,38,23])).
% 97.93/98.03 cnf(6172,plain,
% 97.93/98.03 (~P1(f77(a2,a2),f74(a2))),
% 97.93/98.03 inference(scs_inference,[],[376,1823,1825,1832,1834,5690,5164,5597,647,50,69,51,39,70,52,99,37,102,71,38,23,15,20])).
% 97.93/98.03 cnf(6188,plain,
% 97.93/98.03 (P1(x61881,f48(a84,a84))),
% 97.93/98.03 inference(rename_variables,[],[647])).
% 97.93/98.03 cnf(6190,plain,
% 97.93/98.03 (~P2(a73,a84)),
% 97.93/98.03 inference(scs_inference,[],[1,376,1823,1825,1832,1834,5546,5394,5690,5164,5597,5281,5836,1871,1602,5230,647,951,11,50,69,51,39,70,52,99,37,102,71,38,23,15,20,36,22,17,47,45,48,43,94])).
% 97.93/98.03 cnf(6200,plain,
% 97.93/98.03 (~P1(f23(a65,a3),a65)),
% 97.93/98.03 inference(scs_inference,[],[1,376,1823,1825,1832,1834,5546,5554,5394,5690,5164,6083,5597,5281,5836,1871,1602,5230,647,6188,951,8,11,50,69,51,39,70,52,99,37,102,71,38,23,15,20,36,22,17,47,45,48,43,94,34,46,44,98])).
% 97.93/98.03 cnf(6207,plain,
% 97.93/98.03 (P6(f74(a62),x62071,a86)),
% 97.93/98.03 inference(rename_variables,[],[5544])).
% 97.93/98.03 cnf(6209,plain,
% 97.93/98.03 (P3(a86,a82)),
% 97.93/98.03 inference(scs_inference,[],[1,376,1823,1825,1832,1834,5546,5554,5394,5690,5164,5584,5601,6083,5544,6207,5597,5281,5836,1871,1602,5230,13,647,6188,951,8,11,50,69,51,39,70,52,99,37,102,71,38,23,15,20,36,22,17,47,45,48,43,94,34,46,44,98,91,105,100])).
% 97.93/98.03 cnf(6242,plain,
% 97.93/98.03 (P1(f36(a62,a3),a65)),
% 97.93/98.03 inference(scs_inference,[],[383,1238,1246,6015,5613,576,50,69,51,39,99,70,52,37,38,102,71,23,15])).
% 97.93/98.03 cnf(6244,plain,
% 97.93/98.03 (~P1(a55,f74(a56))),
% 97.93/98.03 inference(scs_inference,[],[2,383,1238,1246,6015,5613,576,50,69,51,39,99,70,52,37,38,102,71,23,15,20])).
% 97.93/98.03 cnf(6248,plain,
% 97.93/98.03 (P6(x62481,f74(a58),a80)),
% 97.93/98.03 inference(scs_inference,[],[2,383,1238,1246,6015,5613,576,50,69,51,39,99,70,52,37,38,102,71,23,15,20,31,22])).
% 97.93/98.03 cnf(6252,plain,
% 97.93/98.03 (P1(f23(a65,a3),f74(a65))),
% 97.93/98.03 inference(scs_inference,[],[2,383,1238,1246,6015,6200,5613,576,50,69,51,39,99,70,52,37,38,102,71,23,15,20,31,22,36,17])).
% 97.93/98.03 cnf(6260,plain,
% 97.93/98.03 (~P1(x62601,f45(a5,a5))),
% 97.93/98.03 inference(rename_variables,[],[779])).
% 97.93/98.03 cnf(6265,plain,
% 97.93/98.03 (~P2(a73,a85)),
% 97.93/98.03 inference(scs_inference,[],[2,383,1238,1246,5599,6015,6172,6200,5613,1649,647,576,779,6260,50,69,51,39,99,70,52,37,38,102,71,23,15,20,31,22,36,17,49,45,48,43,94])).
% 97.93/98.03 cnf(6321,plain,
% 97.93/98.03 (~P6(a3,x63211,a85)),
% 97.93/98.03 inference(scs_inference,[],[1263,1255,6106,8,50,51,69,70,52,99,38])).
% 97.93/98.03 cnf(6331,plain,
% 97.93/98.03 (P1(f19(a62,a58),a65)),
% 97.93/98.03 inference(scs_inference,[],[395,1263,1255,6106,6242,5504,8,50,51,69,70,52,99,38,102,71,23,20,15])).
% 97.93/98.03 cnf(6333,plain,
% 97.93/98.03 (P6(x63331,a3,a80)),
% 97.93/98.03 inference(scs_inference,[],[395,1263,1255,6106,6242,5504,8,50,51,69,70,52,99,38,102,71,23,20,15,22])).
% 97.93/98.03 cnf(6335,plain,
% 97.93/98.03 (~P6(a3,x63351,a5)),
% 97.93/98.03 inference(scs_inference,[],[395,1263,1255,6106,6242,5504,8,50,51,69,70,52,99,38,102,71,23,20,15,22,36])).
% 97.93/98.03 cnf(6349,plain,
% 97.93/98.03 (~P2(a80,a75)),
% 97.93/98.03 inference(scs_inference,[],[2,395,1263,1255,6101,6106,6242,6244,5504,5125,5789,3,8,50,51,69,70,52,99,38,102,71,23,20,15,22,36,17,49,47,45,43,48,94])).
% 97.93/98.03 cnf(6388,plain,
% 97.93/98.03 (~P1(f19(a62,a58),f74(a65))),
% 97.93/98.03 inference(scs_inference,[],[406,1221,1229,6190,6331,50,51,69,52,99,70,102,71,20])).
% 97.93/98.03 cnf(6443,plain,
% 97.93/98.03 (~P1(f78(a59,a59),f74(a59))),
% 97.93/98.03 inference(scs_inference,[],[409,4197,4194,6265,5828,50,69,51,99,52,70,102,71,20])).
% 97.93/98.03 cnf(6458,plain,
% 97.93/98.03 (~P2(a80,a90)),
% 97.93/98.03 inference(scs_inference,[],[2,409,4197,4194,6265,5370,6388,5348,5828,5148,5504,1602,951,11,50,69,51,99,52,70,102,71,20,17,49,47,45,43,48,94])).
% 97.93/98.03 cnf(6462,plain,
% 97.93/98.03 (P1(x64621,f74(a58))),
% 97.93/98.03 inference(rename_variables,[],[576])).
% 97.93/98.03 cnf(6484,plain,
% 97.93/98.03 (P6(a56,a58,a6)),
% 97.93/98.03 inference(scs_inference,[],[2,409,4197,4194,6265,5370,6122,6388,5348,5828,5148,5504,5247,6083,1602,13,576,6462,951,11,50,69,51,99,52,70,102,71,20,17,49,47,45,43,48,94,34,46,44,91,33,32,29,27,28,30,31,40])).
% 97.93/98.03 cnf(6510,plain,
% 97.93/98.03 (~P1(f77(a59,a59),f74(a59))),
% 97.93/98.03 inference(scs_inference,[],[423,873,1043,6349,5830,50,69,51,99,52,70,102,71,20])).
% 97.93/98.03 cnf(6512,plain,
% 97.93/98.03 (P1(f38(a56,a58),a56)),
% 97.93/98.03 inference(scs_inference,[],[423,873,1043,6484,6349,5830,50,69,51,99,52,70,102,71,20,65])).
% 97.93/98.03 cnf(6514,plain,
% 97.93/98.03 (P1(f23(a71,a3),f74(a71))),
% 97.93/98.03 inference(scs_inference,[],[423,873,1043,6484,6349,5830,5715,50,69,51,99,52,70,102,71,20,65,17])).
% 97.93/98.03 cnf(6516,plain,
% 97.93/98.03 (P1(f29(a2,a56),a2)),
% 97.93/98.03 inference(scs_inference,[],[2,423,873,1043,6484,6349,5830,5715,5052,50,69,51,99,52,70,102,71,20,65,17,78])).
% 97.93/98.03 cnf(6519,plain,
% 97.93/98.03 (P1(f32(a62,a56),a62)),
% 97.93/98.03 inference(scs_inference,[],[2,423,873,1043,6484,6349,5830,5715,5052,5206,50,69,51,99,52,70,102,71,20,65,17,78,41])).
% 97.93/98.03 cnf(6530,plain,
% 97.93/98.03 (~P1(x65301,f45(a5,a5))),
% 97.93/98.03 inference(rename_variables,[],[779])).
% 97.93/98.03 cnf(6534,plain,
% 97.93/98.03 (P1(f72(a58,a56),a56)),
% 97.93/98.03 inference(scs_inference,[],[2,423,873,1043,6484,6349,6443,6252,5830,285,6124,5715,5052,5070,5206,6200,5828,6244,3,779,14,50,69,51,99,52,70,102,71,20,65,17,78,41,79,47,45,48,43,76])).
% 97.93/98.03 cnf(6537,plain,
% 97.93/98.03 (~P2(a6,a85)),
% 97.93/98.03 inference(scs_inference,[],[2,423,873,1043,6484,5878,6349,6443,6252,5830,285,6124,5715,5052,5070,5206,6200,5828,6244,3,779,14,50,69,51,99,52,70,102,71,20,65,17,78,41,79,47,45,48,43,76,94])).
% 97.93/98.03 cnf(6538,plain,
% 97.93/98.03 (~P6(a56,x65381,a85)),
% 97.93/98.03 inference(rename_variables,[],[5878])).
% 97.93/98.03 cnf(6541,plain,
% 97.93/98.03 (P1(x65411,a3)),
% 97.93/98.03 inference(rename_variables,[],[8])).
% 97.93/98.03 cnf(6549,plain,
% 97.93/98.03 (P1(x65491,a3)),
% 97.93/98.03 inference(rename_variables,[],[8])).
% 97.93/98.03 cnf(6550,plain,
% 97.93/98.03 (~P6(a56,x65501,a85)),
% 97.93/98.03 inference(rename_variables,[],[5878])).
% 97.93/98.03 cnf(6552,plain,
% 97.93/98.03 (~P5(a86,a6)),
% 97.93/98.03 inference(scs_inference,[],[2,423,873,1043,6484,5878,6538,6349,6443,6252,5830,285,6124,5715,5052,5070,5206,5880,6200,5828,6244,3,779,6530,14,8,6541,50,69,51,99,52,70,102,71,20,65,17,78,41,79,47,45,48,43,76,94,34,46,44,93,104])).
% 97.93/98.03 cnf(6558,plain,
% 97.93/98.03 (P6(a3,a56,a4)),
% 97.93/98.03 inference(scs_inference,[],[2,423,873,1043,6484,5878,6538,6550,6349,6443,6252,5830,285,6124,5715,5052,5070,5206,5880,6200,5828,6244,3,779,6530,14,8,6541,6549,50,69,51,99,52,70,102,71,20,65,17,78,41,79,47,45,48,43,76,94,34,46,44,93,104,91,33])).
% 97.93/98.03 cnf(6560,plain,
% 97.93/98.03 (P1(f32(a62,a56),a65)),
% 97.93/98.03 inference(scs_inference,[],[2,423,873,1043,6484,5878,6538,6550,6349,6443,6252,5830,285,6124,5715,5052,5070,5206,5880,6200,5828,6244,3,779,6530,14,8,6541,6549,50,69,51,99,52,70,102,71,20,65,17,78,41,79,47,45,48,43,76,94,34,46,44,93,104,91,33,15])).
% 97.93/98.03 cnf(6562,plain,
% 97.93/98.03 (P1(f76(a56,a3),a56)),
% 97.93/98.03 inference(scs_inference,[],[2,423,873,1043,6484,5878,6538,6550,6349,6443,6252,5830,285,6124,5715,5052,5070,5206,5880,6200,5828,6244,3,779,6530,14,8,6541,6549,50,69,51,99,52,70,102,71,20,65,17,78,41,79,47,45,48,43,76,94,34,46,44,93,104,91,33,15,54])).
% 97.93/98.03 cnf(6564,plain,
% 97.93/98.03 (P1(f77(a3,a56),a56)),
% 97.93/98.03 inference(scs_inference,[],[2,423,873,1043,6484,5878,6538,6550,6349,6443,6252,5830,285,6124,5715,5052,5070,5206,5880,6200,5828,6244,3,779,6530,14,8,6541,6549,50,69,51,99,52,70,102,71,20,65,17,78,41,79,47,45,48,43,76,94,34,46,44,93,104,91,33,15,54,80])).
% 97.93/98.03 cnf(6594,plain,
% 97.93/98.03 (~P2(a86,a7)),
% 97.93/98.03 inference(scs_inference,[],[433,876,1036,1455,6458,5123,6512,6510,1624,5336,5830,50,69,51,99,70,52,71,102,20,17,48,43,94])).
% 97.93/98.03 cnf(6597,plain,
% 97.93/98.03 (P6(a3,a56,a82)),
% 97.93/98.03 inference(scs_inference,[],[2,433,876,1036,1455,6458,5123,6512,6510,1624,5336,5830,8,50,69,51,99,70,52,71,102,20,17,48,43,94,34])).
% 97.93/98.03 cnf(6598,plain,
% 97.93/98.03 (P1(x65981,a3)),
% 97.93/98.03 inference(rename_variables,[],[8])).
% 97.93/98.03 cnf(6604,plain,
% 97.93/98.03 (P3(a90,a90)),
% 97.93/98.03 inference(scs_inference,[],[2,433,876,1036,1455,6458,6558,5123,6512,6510,1624,5336,5830,5168,13,8,50,69,51,99,70,52,71,102,20,17,48,43,94,34,46,91,100])).
% 97.93/98.03 cnf(6606,plain,
% 97.93/98.03 (P6(a56,a3,a4)),
% 97.93/98.03 inference(scs_inference,[],[2,433,876,1036,1455,6458,6558,5123,6512,6510,1624,5336,5830,5168,13,8,6598,50,69,51,99,70,52,71,102,20,17,48,43,94,34,46,91,100,33])).
% 97.93/98.03 cnf(6608,plain,
% 97.93/98.03 (P1(f76(a3,a56),a56)),
% 97.93/98.03 inference(scs_inference,[],[2,433,876,1036,1455,6458,6558,5123,6512,6510,1624,5336,5830,5168,13,8,6598,50,69,51,99,70,52,71,102,20,17,48,43,94,34,46,91,100,33,53])).
% 97.93/98.03 cnf(6612,plain,
% 97.93/98.03 (P1(f78(a56,a3),a56)),
% 97.93/98.03 inference(scs_inference,[],[2,307,433,876,1036,1455,6458,6558,5123,6512,6510,1624,5336,5830,5168,13,8,6598,50,69,51,99,70,52,71,102,20,17,48,43,94,34,46,91,100,33,53,108,81])).
% 97.93/98.03 cnf(6629,plain,
% 97.93/98.03 (P6(f49(a73,a87),f50(a73,a87),a73)),
% 97.93/98.03 inference(scs_inference,[],[437,1312,1317,1324,6594,50,69,51,99,52,70,71])).
% 97.93/98.03 cnf(6631,plain,
% 97.93/98.03 (~P6(f49(a73,a87),f50(a73,a87),a87)),
% 97.93/98.03 inference(scs_inference,[],[437,1312,1317,1324,6594,50,69,51,99,52,70,71,102])).
% 97.93/98.03 cnf(6635,plain,
% 97.93/98.03 (P1(f39(a58,a65),f74(a62))),
% 97.93/98.03 inference(scs_inference,[],[437,1312,1317,1324,6594,6608,1840,50,69,51,99,52,70,71,102,20,17])).
% 97.93/98.03 cnf(6637,plain,
% 97.93/98.03 (~P1(f14(a56,a2),a2)),
% 97.93/98.03 inference(scs_inference,[],[2,437,1312,1317,1324,6594,6608,1840,5425,50,69,51,99,52,70,71,102,20,17,77])).
% 97.93/98.03 cnf(6645,plain,
% 97.93/98.03 (~P2(a82,a85)),
% 97.93/98.03 inference(scs_inference,[],[2,437,1312,1317,1324,6594,6321,6597,6608,6514,6519,1840,5425,5715,779,50,69,51,99,52,70,71,102,20,17,77,48,43,94])).
% 97.93/98.03 cnf(6677,plain,
% 97.93/98.03 (P6(f49(a7,a75),f50(a7,a75),a7)),
% 97.93/98.03 inference(scs_inference,[],[450,4184,4181,6537,50,69,51,99,52,70,71])).
% 97.93/98.03 cnf(6679,plain,
% 97.93/98.03 (~P6(f49(a7,a75),f50(a7,a75),a75)),
% 97.93/98.03 inference(scs_inference,[],[450,4184,4181,6537,50,69,51,99,52,70,71,102])).
% 97.93/98.03 cnf(6683,plain,
% 97.93/98.03 (P1(f14(a56,a2),f74(a2))),
% 97.93/98.03 inference(scs_inference,[],[450,4184,4181,6537,6637,6612,50,69,51,99,52,70,71,102,20,17])).
% 97.93/98.03 cnf(6689,plain,
% 97.93/98.03 (~P2(a80,a7)),
% 97.93/98.03 inference(scs_inference,[],[450,4184,4181,6537,5704,6635,6637,5558,6612,5222,50,69,51,99,52,70,71,102,20,17,48,43,94])).
% 97.93/98.03 cnf(6724,plain,
% 97.93/98.03 (P6(f74(a2),a2,a6)),
% 97.93/98.03 inference(scs_inference,[],[456,4209,4206,6645,6683,6562,1922,50,69,99,51,52,70,71,102,20,17,40])).
% 97.93/98.03 cnf(6731,plain,
% 97.93/98.03 (~P2(a73,a87)),
% 97.93/98.03 inference(scs_inference,[],[456,4209,4206,6645,6631,6683,6629,6562,6143,1922,6637,951,50,69,99,51,52,70,71,102,20,17,40,48,43,94])).
% 97.93/98.03 cnf(6756,plain,
% 97.93/98.03 (~P6(f49(a5,a88),f50(a5,a88),a88)),
% 97.93/98.03 inference(scs_inference,[],[503,4511,4505,6689,50,69,99,51,70,52,102])).
% 97.93/98.03 cnf(6758,plain,
% 97.93/98.03 (P6(f49(a5,a88),f50(a5,a88),a5)),
% 97.93/98.03 inference(scs_inference,[],[503,4511,4505,6689,50,69,99,51,70,52,102,71])).
% 97.93/98.03 cnf(6764,plain,
% 97.93/98.03 (P1(f29(a62,a56),a62)),
% 97.93/98.03 inference(scs_inference,[],[2,503,4511,4505,6689,6564,1876,5208,50,69,99,51,70,52,102,71,20,17,78])).
% 97.93/98.03 cnf(6767,plain,
% 97.93/98.03 (P1(f32(a59,a56),a59)),
% 97.93/98.03 inference(scs_inference,[],[2,503,4511,4505,6689,6564,1876,5648,5208,50,69,99,51,70,52,102,71,20,17,78,41])).
% 97.93/98.03 cnf(6770,plain,
% 97.93/98.03 (P1(f52(a56,a62),a62)),
% 97.93/98.03 inference(scs_inference,[],[2,503,4511,4505,6689,6564,1876,5648,5208,5224,50,69,99,51,70,52,102,71,20,17,78,41,79])).
% 97.93/98.03 cnf(6773,plain,
% 97.93/98.03 (P1(f72(a58,a62),a62)),
% 97.93/98.03 inference(scs_inference,[],[2,503,4511,4505,6689,6564,1876,5648,5208,5224,563,14,50,69,99,51,70,52,102,71,20,17,78,41,79,76])).
% 97.93/98.03 cnf(6781,plain,
% 97.93/98.03 (~P2(a6,a75)),
% 97.93/98.03 inference(scs_inference,[],[2,503,4511,4505,6689,5250,6724,6564,1876,5648,5208,5224,563,1871,5230,14,636,50,69,99,51,70,52,102,71,20,17,78,41,79,76,48,43,94])).
% 97.93/98.03 cnf(6785,plain,
% 97.93/98.03 (P1(f36(a71,a3),a71)),
% 97.93/98.03 inference(scs_inference,[],[2,503,4511,4505,5977,6689,5250,6724,6564,1876,5648,5208,5224,563,1871,12,6,5230,14,636,8,50,69,99,51,70,52,102,71,20,17,78,41,79,76,48,43,94,46,93])).
% 97.93/98.03 cnf(6789,plain,
% 97.93/98.03 (~P5(a80,a6)),
% 97.93/98.03 inference(scs_inference,[],[2,503,4511,4505,5977,6689,5250,6724,6564,1876,5648,5208,5224,563,5070,1871,12,6,5230,14,636,8,50,69,99,51,70,52,102,71,20,17,78,41,79,76,48,43,94,46,93,104])).
% 97.93/98.03 cnf(6795,plain,
% 97.93/98.03 (P1(f29(a62,a56),a65)),
% 97.93/98.03 inference(scs_inference,[],[2,503,4511,4505,5977,6689,5250,6724,6073,6564,1876,5648,5208,5224,563,5070,1871,12,6,5230,14,636,8,50,69,99,51,70,52,102,71,20,17,78,41,79,76,48,43,94,46,93,104,105,15])).
% 97.93/98.03 cnf(6822,plain,
% 97.93/98.03 (P1(f52(a56,a62),a65)),
% 97.93/98.03 inference(scs_inference,[],[507,4286,4283,6731,6770,50,69,99,51,52,70,71,15])).
% 97.93/98.03 cnf(6826,plain,
% 97.93/98.03 (~P1(f72(a58,a62),f74(a62))),
% 97.93/98.03 inference(scs_inference,[],[507,4286,4283,6731,6773,6770,50,69,99,51,52,70,71,15,102,20])).
% 97.93/98.03 cnf(6839,plain,
% 97.93/98.03 (~P2(a5,a88)),
% 97.93/98.03 inference(scs_inference,[],[507,4286,4283,6731,6758,6773,6756,6770,5463,10,5,779,50,69,99,51,52,70,71,15,102,20,17,49,47,48,43,94])).
% 97.93/98.03 cnf(6875,plain,
% 97.93/98.03 (~P1(a55,f74(a59))),
% 97.93/98.03 inference(scs_inference,[],[3,514,4272,4269,6781,50,69,99,51,52,70,71,102,20])).
% 97.93/98.03 cnf(6883,plain,
% 97.93/98.03 (P6(f48(a84,a84),a59,a82)),
% 97.93/98.03 inference(scs_inference,[],[3,514,4272,4269,6781,6826,1815,5603,647,50,69,99,51,52,70,71,102,20,17,49,47,34])).
% 97.93/98.03 cnf(6884,plain,
% 97.93/98.03 (P1(x68841,f48(a84,a84))),
% 97.93/98.03 inference(rename_variables,[],[647])).
% 97.93/98.03 cnf(6888,plain,
% 97.93/98.03 (~P2(a86,a90)),
% 97.93/98.03 inference(scs_inference,[],[3,514,4272,4269,6781,5092,6826,1815,5544,5603,6244,647,50,69,99,51,52,70,71,102,20,17,49,47,34,48,94])).
% 97.93/98.03 cnf(6895,plain,
% 97.93/98.03 (P3(a80,a4)),
% 97.93/98.03 inference(scs_inference,[],[3,514,4272,4269,6781,5092,6826,6606,6333,1815,5544,5603,6244,647,50,69,99,51,52,70,71,102,20,17,49,47,34,48,94,43,46,100])).
% 97.93/98.03 cnf(6900,plain,
% 97.93/98.03 (~P1(f14(a59,a65),a65)),
% 97.93/98.03 inference(scs_inference,[],[3,514,4272,4269,6781,5092,6826,6606,6333,1815,5528,5544,5603,6244,647,6884,50,69,99,51,52,70,71,102,20,17,49,47,34,48,94,43,46,100,33,77])).
% 97.93/98.03 cnf(6942,plain,
% 97.93/98.03 (P1(f14(a59,a65),f74(a65))),
% 97.93/98.03 inference(scs_inference,[],[520,6604,6135,5129,5139,6839,6900,6822,69,50,99,52,51,70,102,71,20,17])).
% 97.93/98.03 cnf(6945,plain,
% 97.93/98.03 (P1(x69451,f48(a84,a84))),
% 97.93/98.03 inference(rename_variables,[],[647])).
% 97.93/98.03 cnf(6948,plain,
% 97.93/98.03 (~P1(x69481,f46(a88,a88))),
% 97.93/98.03 inference(rename_variables,[],[951])).
% 97.93/98.03 cnf(6951,plain,
% 97.93/98.03 (~P1(x69511,f46(a88,a88))),
% 97.93/98.03 inference(rename_variables,[],[951])).
% 97.93/98.03 cnf(6953,plain,
% 97.93/98.03 (~P2(a7,a75)),
% 97.93/98.03 inference(scs_inference,[],[3,520,6604,6135,5129,5139,6839,6679,6677,6900,6822,6767,6785,647,951,6948,69,50,99,52,51,70,102,71,20,17,34,48,43,94])).
% 97.93/98.03 cnf(6958,plain,
% 97.93/98.03 (P6(f48(a84,a84),a59,a4)),
% 97.93/98.03 inference(scs_inference,[],[3,520,6604,6135,5129,5139,6839,6679,6677,6900,6822,6767,6785,647,6945,951,6948,6951,69,50,99,52,51,70,102,71,20,17,34,48,43,94,46,33])).
% 97.93/98.03 cnf(6992,plain,
% 97.93/98.03 (P1(x69921,f74(a58))),
% 97.93/98.03 inference(rename_variables,[],[576])).
% 97.93/98.03 cnf(6997,plain,
% 97.93/98.03 (~P2(a86,a91)),
% 97.93/98.03 inference(scs_inference,[],[3,534,6552,5722,6888,5467,5445,6795,5511,6244,576,636,69,50,99,52,70,51,71,102,20,17,43,34,48,94])).
% 97.93/98.03 cnf(7000,plain,
% 97.93/98.03 (~P6(a59,a58,a7)),
% 97.93/98.03 inference(scs_inference,[],[3,534,6552,5722,6888,5467,5445,6795,5511,6244,576,14,636,69,50,99,52,70,51,71,102,20,17,43,34,48,94,46])).
% 97.93/98.03 cnf(7005,plain,
% 97.93/98.03 (P6(f74(a65),a65,a6)),
% 97.93/98.03 inference(scs_inference,[],[3,534,6552,5722,6888,5467,6942,5445,6795,5511,6244,576,6992,14,636,69,50,99,52,70,51,71,102,20,17,43,34,48,94,46,33,40])).
% 97.93/98.03 cnf(7027,plain,
% 97.93/98.03 (~P1(f29(a62,a56),f74(a62))),
% 97.93/98.03 inference(scs_inference,[],[543,5610,6209,6953,6764,69,99,50,52,70,51,71,102,20])).
% 97.93/98.03 cnf(7036,plain,
% 97.93/98.03 (P6(a59,f74(a58),a82)),
% 97.93/98.03 inference(scs_inference,[],[3,543,5610,6209,6953,6764,6091,5565,6875,2,576,779,69,99,50,52,70,51,71,102,20,17,45,43,34])).
% 97.93/98.03 cnf(7037,plain,
% 97.93/98.03 (P1(x70371,f74(a58))),
% 97.93/98.03 inference(rename_variables,[],[576])).
% 97.93/98.03 cnf(7039,plain,
% 97.93/98.03 (~P2(a82,a89)),
% 97.93/98.03 inference(scs_inference,[],[3,543,5610,6209,6953,6883,6152,6764,6091,5565,6875,2,576,779,69,99,50,52,70,51,71,102,20,17,45,43,34,94])).
% 97.93/98.03 cnf(7046,plain,
% 97.93/98.03 (P6(f74(a58),a59,a4)),
% 97.93/98.03 inference(scs_inference,[],[3,543,5610,6209,6953,6883,6152,6764,6091,5565,6875,2,576,7037,779,69,99,50,52,70,51,71,102,20,17,45,43,34,94,48,46,33])).
% 97.93/98.03 cnf(7050,plain,
% 97.93/98.03 (P1(f29(a59,a59),a59)),
% 97.93/98.03 inference(scs_inference,[],[3,543,5610,6209,6953,6883,6152,6764,6560,6091,5654,5680,6900,5565,6875,2,576,7037,779,69,99,50,52,70,51,71,102,20,17,45,43,34,94,48,46,33,88,78])).
% 97.93/98.03 cnf(7062,plain,
% 97.93/98.03 (~P5(a86,a82)),
% 97.93/98.03 inference(scs_inference,[],[3,543,5610,6209,6953,6883,6152,6168,6764,6560,6091,5771,5654,5668,5680,6900,5565,6875,571,2,576,7037,779,14,69,99,50,52,70,51,71,102,20,17,45,43,34,94,48,46,33,88,78,41,79,76,104])).
% 97.93/98.03 cnf(7070,plain,
% 97.93/98.03 (P6(f45(a80,a4),f46(a80,a4),a4)),
% 97.93/98.03 inference(scs_inference,[],[6895,69])).
% 97.93/98.03 cnf(7090,plain,
% 97.93/98.03 (P6(a3,a59,a82)),
% 97.93/98.03 inference(scs_inference,[],[3,551,6789,6895,6997,7050,5682,8,69,99,50,52,70,51,71,102,20,17,34])).
% 97.93/98.03 cnf(7091,plain,
% 97.93/98.03 (P1(x70911,a3)),
% 97.93/98.03 inference(rename_variables,[],[8])).
% 97.93/98.03 cnf(7093,plain,
% 97.93/98.03 (~P2(a6,a7)),
% 97.93/98.03 inference(scs_inference,[],[3,551,7000,6789,6895,6997,7050,6129,5682,8,69,99,50,52,70,51,71,102,20,17,34,94])).
% 97.93/98.03 cnf(7102,plain,
% 97.93/98.03 (P6(a59,a3,a4)),
% 97.93/98.03 inference(scs_inference,[],[3,551,7000,6789,6895,6997,7050,7046,6129,5682,12,6,13,636,8,7091,69,99,50,52,70,51,71,102,20,17,34,94,43,46,91,33])).
% 97.93/98.03 cnf(7104,plain,
% 97.93/98.03 (~P1(f10(a69,a71),a71)),
% 97.93/98.03 inference(scs_inference,[],[3,551,7000,6789,6895,6997,7050,7046,6129,5682,12,6,13,636,8,7091,69,99,50,52,70,51,71,102,20,17,34,94,43,46,91,33,42])).
% 97.93/98.03 cnf(7106,plain,
% 97.93/98.03 (P1(f10(a69,a71),a69)),
% 97.93/98.03 inference(scs_inference,[],[3,551,7000,6789,6895,6997,7050,7046,6129,5682,12,6,13,636,8,7091,69,99,50,52,70,51,71,102,20,17,34,94,43,46,91,33,42,26])).
% 97.93/98.03 cnf(7124,plain,
% 97.93/98.03 (P6(f45(a88,a88),f46(a88,a88),a88)),
% 97.93/98.03 inference(scs_inference,[],[7039,7062,295,614,69,99,50,52,70])).
% 97.93/98.03 cnf(7132,plain,
% 97.93/98.03 (~P1(f10(a69,a71),f74(a69))),
% 97.93/98.03 inference(scs_inference,[],[1046,7039,7062,7106,295,614,69,99,50,52,70,51,71,102,20])).
% 97.93/98.03 cnf(7134,plain,
% 97.93/98.03 (P1(f10(a69,a71),f74(a71))),
% 97.93/98.03 inference(scs_inference,[],[1046,7039,7062,7106,7104,295,614,69,99,50,52,70,51,71,102,20,17])).
% 97.93/98.03 cnf(7143,plain,
% 97.93/98.03 (~P1(x71431,f46(a88,a88))),
% 97.93/98.03 inference(rename_variables,[],[951])).
% 97.93/98.03 cnf(7146,plain,
% 97.93/98.03 (P1(x71461,a3)),
% 97.93/98.03 inference(rename_variables,[],[8])).
% 97.93/98.03 cnf(7149,plain,
% 97.93/98.03 (~P6(a3,x71491,a5)),
% 97.93/98.03 inference(rename_variables,[],[6335])).
% 97.93/98.03 cnf(7161,plain,
% 97.93/98.03 (P6(a3,a59,a4)),
% 97.93/98.03 inference(scs_inference,[],[3,1046,7039,7062,7090,7106,7104,6335,7149,6534,6516,295,614,951,7143,8,7146,69,99,50,52,70,51,71,102,20,17,47,49,45,43,34,94,48,44,46,91,33])).
% 97.93/98.03 cnf(7177,plain,
% 97.93/98.03 (P1(f76(a59,a3),a59)),
% 97.93/98.03 inference(scs_inference,[],[3,1046,7039,7062,7090,7106,7104,6335,7149,6534,6516,295,614,951,7143,8,7146,69,99,50,52,70,51,71,102,20,17,47,49,45,43,34,94,48,44,46,91,33,1409,27,29,32,30,28,31,54])).
% 97.93/98.03 cnf(7179,plain,
% 97.93/98.03 (~P1(f14(a59,a62),a62)),
% 97.93/98.03 inference(scs_inference,[],[3,1046,7039,7062,7090,7106,7104,6335,7149,6534,6516,295,614,1614,951,7143,8,7146,69,99,50,52,70,51,71,102,20,17,47,49,45,43,34,94,48,44,46,91,33,1409,27,29,32,30,28,31,54,77])).
% 97.93/98.03 cnf(7182,plain,
% 97.93/98.03 (P1(f77(a3,a59),a59)),
% 97.93/98.03 inference(scs_inference,[],[3,1046,7039,7062,7090,7106,7104,6335,7149,6534,6516,295,614,1614,951,7143,8,7146,69,99,50,52,70,51,71,102,20,17,47,49,45,43,34,94,48,44,46,91,33,1409,27,29,32,30,28,31,54,77,80])).
% 97.93/98.03 cnf(7187,plain,
% 97.93/98.03 (P3(a80,a82)),
% 97.93/98.03 inference(scs_inference,[],[3,1046,7039,7062,7090,5271,5216,7106,7104,7036,6248,6335,7149,6534,6516,295,614,1614,951,7143,8,7146,69,99,50,52,70,51,71,102,20,17,47,49,45,43,34,94,48,44,46,91,33,1409,27,29,32,30,28,31,54,77,80,75,100])).
% 97.93/98.03 cnf(7199,plain,
% 97.93/98.03 (~P6(f41(a6,a7),f47(a6,a7),a7)),
% 97.93/98.03 inference(scs_inference,[],[7093,99])).
% 97.93/98.03 cnf(7201,plain,
% 97.93/98.03 (P6(f41(a6,a7),f47(a6,a7),a6)),
% 97.93/98.03 inference(scs_inference,[],[7093,99,50])).
% 97.93/98.03 cnf(7207,plain,
% 97.93/98.03 (P6(f48(a84,a84),f51(a84,a84),a84)),
% 97.93/98.03 inference(scs_inference,[],[7093,7187,334,99,50,69,70,52])).
% 97.93/98.03 cnf(7215,plain,
% 97.93/98.03 (~P1(f76(a59,a3),f74(a59))),
% 97.93/98.03 inference(scs_inference,[],[1250,7093,7187,7177,304,334,99,50,69,70,52,51,71,102,20])).
% 97.93/98.03 cnf(7231,plain,
% 97.93/98.03 (~P2(a6,a91)),
% 97.93/98.03 inference(scs_inference,[],[1250,7093,7187,5573,7132,7134,7177,7179,7005,304,334,99,50,69,70,52,51,71,102,20,17,47,49,45,48,44,43,94])).
% 97.93/98.03 cnf(7239,plain,
% 97.93/98.03 (P6(f74(a71),a71,a6)),
% 97.93/98.03 inference(scs_inference,[],[1250,7093,7161,7187,5573,7132,7134,7177,7179,7005,6137,304,334,7104,6118,5804,13,99,50,69,70,52,51,71,102,20,17,47,49,45,48,44,43,94,46,91,95,40])).
% 97.93/98.03 cnf(7244,plain,
% 97.93/98.03 (~P6(f41(a6,a91),f47(a6,a91),a91)),
% 97.93/98.03 inference(scs_inference,[],[7231,99])).
% 97.93/98.03 cnf(7248,plain,
% 97.93/98.03 (P6(f41(a6,a91),f47(a6,a91),a6)),
% 97.93/98.03 inference(scs_inference,[],[7231,1339,99,69,50])).
% 97.93/98.03 cnf(7254,plain,
% 97.93/98.03 (P6(f49(a80,a4),f50(a80,a4),a80)),
% 97.93/98.03 inference(scs_inference,[],[1335,7231,491,1339,5129,99,69,50,52,51,71])).
% 97.93/98.03 cnf(7256,plain,
% 97.93/98.03 (~P6(f49(a80,a4),f50(a80,a4),a4)),
% 97.93/98.03 inference(scs_inference,[],[1335,7231,491,1339,5129,99,69,50,52,51,71,102])).
% 97.93/98.03 cnf(7264,plain,
% 97.93/98.03 (~P2(a4,a89)),
% 97.93/98.03 inference(scs_inference,[],[1335,7102,7231,7182,7027,491,1339,5129,5634,6764,5836,99,69,50,52,51,71,102,20,17,43,94])).
% 97.93/98.03 cnf(7272,plain,
% 97.93/98.03 (P1(f12(a59,a58),a59)),
% 97.93/98.03 inference(scs_inference,[],[3,1335,7102,7231,7215,7182,7027,491,1339,7000,5129,5634,6764,5836,6875,2,647,14,99,69,50,52,51,71,102,20,17,43,94,46,44,92])).
% 97.93/98.03 cnf(7281,plain,
% 97.93/98.03 (~P6(f41(a4,a89),f47(a4,a89),a89)),
% 97.93/98.03 inference(scs_inference,[],[7264,1324,69,99])).
% 97.93/98.03 cnf(7283,plain,
% 97.93/98.03 (P6(f41(a4,a89),f47(a4,a89),a4)),
% 97.93/98.03 inference(scs_inference,[],[7264,1324,69,99,50])).
% 97.93/98.03 cnf(7291,plain,
% 97.93/98.03 (~P1(f12(a59,a58),f74(a59))),
% 97.93/98.03 inference(scs_inference,[],[1351,1365,7264,7272,1455,1324,69,99,50,51,71,102,20])).
% 97.93/98.03 cnf(7297,plain,
% 97.93/98.03 (~P2(a6,a90)),
% 97.93/98.03 inference(scs_inference,[],[1351,1365,7264,5472,7272,7239,1455,1324,5727,7106,7132,69,99,50,51,71,102,20,17,43,94])).
% 97.93/98.03 cnf(7313,plain,
% 97.93/98.03 (~P1(x73131,a58)),
% 97.93/98.03 inference(rename_variables,[],[14])).
% 97.93/98.03 cnf(7315,plain,
% 97.93/98.03 (~P5(a86,a88)),
% 97.93/98.03 inference(scs_inference,[],[3,1351,1365,7264,5472,7124,7272,7070,7239,953,1455,5874,1324,5773,5894,560,5727,7106,7132,13,14,69,99,50,51,71,102,20,17,43,94,46,91,78,41,79,76,104])).
% 97.93/98.03 cnf(7316,plain,
% 97.93/98.03 (P6(x73161,f46(a88,a88),a86)),
% 97.93/98.03 inference(rename_variables,[],[953])).
% 97.93/98.03 cnf(7325,plain,
% 97.93/98.03 (P1(x73251,a59)+P1(f19(a59,a58),a59)),
% 97.93/98.03 inference(scs_inference,[],[3,338,1351,1365,7264,5472,7124,7272,7070,7239,953,7316,5730,1455,5874,1324,5773,5894,560,5727,7106,7132,13,14,7313,69,99,50,51,71,102,20,17,43,94,46,91,78,41,79,76,104,105,52,108,96])).
% 97.93/98.03 cnf(7328,plain,
% 97.93/98.03 (P1(f19(a59,a58),a59)),
% 97.93/98.03 inference(factoring_inference,[],[7325])).
% 97.93/98.03 cnf(7345,plain,
% 97.93/98.03 (~P2(a84,a83)),
% 97.93/98.03 inference(scs_inference,[],[1370,7297,7315,7207,7328,6160,5139,5222,69,99,50,51,71,102,20,17,94])).
% 97.93/98.03 cnf(7348,plain,
% 97.93/98.03 (~P6(a65,a62,a73)),
% 97.93/98.03 inference(scs_inference,[],[1370,7297,7315,7207,7328,6160,5139,5222,10,5,69,99,50,51,71,102,20,17,94,43])).
% 97.93/98.03 cnf(7355,plain,
% 97.93/98.03 (~P1(f10(a65,a62),a62)),
% 97.93/98.03 inference(scs_inference,[],[1370,7297,7315,7207,7328,7291,6160,7201,7199,5139,5222,10,5,576,69,99,50,51,71,102,20,17,94,43,46,91,42])).
% 97.93/98.03 cnf(7357,plain,
% 97.93/98.03 (P1(f10(a65,a62),a65)),
% 97.93/98.03 inference(scs_inference,[],[1370,7297,7315,7207,7328,7291,6160,7201,7199,5139,5222,10,5,576,69,99,50,51,71,102,20,17,94,43,46,91,42,26])).
% 97.93/98.03 cnf(7376,plain,
% 97.93/98.03 (~P1(f10(a65,a62),f74(a65))),
% 97.93/98.03 inference(scs_inference,[],[1380,7345,7357,50,99,71,102,20])).
% 97.93/98.03 cnf(7378,plain,
% 97.93/98.03 (P1(f10(a65,a62),f74(a62))),
% 97.93/98.03 inference(scs_inference,[],[1380,7345,7357,7355,50,99,71,102,20,17])).
% 97.93/98.03 cnf(7380,plain,
% 97.93/98.03 (~P1(f14(a59,a71),a71)),
% 97.93/98.03 inference(scs_inference,[],[3,1380,7345,7357,7355,5040,50,99,71,102,20,17,77])).
% 97.93/98.03 cnf(7383,plain,
% 97.93/98.03 (~P6(a59,a58,a73)),
% 97.93/98.03 inference(scs_inference,[],[3,1380,7345,7357,7355,5040,14,50,99,71,102,20,17,77,43])).
% 97.93/98.03 cnf(7386,plain,
% 97.93/98.03 (~P2(a80,a73)),
% 97.93/98.03 inference(scs_inference,[],[3,1380,7345,7348,7357,7355,5040,5224,14,50,99,71,102,20,17,77,43,94])).
% 97.93/98.03 cnf(7395,plain,
% 97.93/98.03 (P6(f41(a4,a89),f47(a4,a89),a73)),
% 97.93/98.03 inference(scs_inference,[],[3,1380,7345,7348,6094,6069,7283,7357,7355,6958,6168,5040,5224,13,14,50,99,71,102,20,17,77,43,94,75,100,91])).
% 97.93/98.03 cnf(7399,plain,
% 97.93/98.03 (P6(f45(a86,a4),f46(a86,a4),a4)),
% 97.93/98.03 inference(scs_inference,[],[3,1380,7345,7348,6094,6069,7283,7357,7355,6958,6168,5040,5224,13,14,50,99,71,102,20,17,77,43,94,75,100,91,70,69])).
% 97.93/98.03 cnf(7401,plain,
% 97.93/98.03 (P1(f10(a59,a58),a59)),
% 97.93/98.03 inference(scs_inference,[],[3,1380,7345,7348,6094,6069,7283,7357,7355,6958,6168,5040,5224,13,14,50,99,71,102,20,17,77,43,94,75,100,91,70,69,26])).
% 97.93/98.03 cnf(7415,plain,
% 97.93/98.03 (P6(f41(a80,a73),f47(a80,a73),a80)),
% 97.93/98.03 inference(scs_inference,[],[7386,50])).
% 97.93/98.03 cnf(7417,plain,
% 97.93/98.03 (~P6(f41(a80,a73),f47(a80,a73),a73)),
% 97.93/98.03 inference(scs_inference,[],[7386,50,99])).
% 97.93/98.03 cnf(7423,plain,
% 97.93/98.03 (~P1(a61,f74(a62))),
% 97.93/98.03 inference(scs_inference,[],[4,1384,7386,50,99,102,71,20])).
% 97.93/98.03 cnf(7437,plain,
% 97.93/98.03 (P1(x74371,f48(a84,a84))),
% 97.93/98.03 inference(rename_variables,[],[647])).
% 97.93/98.03 cnf(7445,plain,
% 97.93/98.03 (~P2(a80,a4)),
% 97.93/98.03 inference(scs_inference,[],[4,1384,7386,7376,7254,7256,7378,7380,647,576,50,99,102,71,20,17,40,49,47,45,34,48,44,43,94])).
% 97.93/98.03 cnf(7455,plain,
% 97.93/98.03 (P1(f38(a62,a58),a65)),
% 97.93/98.03 inference(scs_inference,[],[4,1384,7386,7376,7254,7256,7378,7248,7244,7380,647,7437,576,50,99,102,71,20,17,40,49,47,45,34,48,44,43,94,46,91,33,65,15])).
% 97.93/98.03 cnf(7467,plain,
% 97.93/98.03 (~P1(f38(a62,a58),f74(a65))),
% 97.93/98.03 inference(scs_inference,[],[1397,7445,7455,50,99,102,71,20])).
% 97.93/98.03 cnf(7472,plain,
% 97.93/98.03 (P1(x74721,f48(a84,a84))),
% 97.93/98.03 inference(rename_variables,[],[647])).
% 97.93/98.03 cnf(7475,plain,
% 97.93/98.03 (P1(x74751,f48(a84,a84))),
% 97.93/98.03 inference(rename_variables,[],[647])).
% 97.93/98.03 cnf(7478,plain,
% 97.93/98.03 (P1(x74781,f48(a84,a84))),
% 97.93/98.03 inference(rename_variables,[],[647])).
% 97.93/98.03 cnf(7482,plain,
% 97.93/98.03 (~P2(a6,a73)),
% 97.93/98.03 inference(scs_inference,[],[4,1397,7383,7445,7423,7455,6129,5405,6875,2,647,7472,7475,50,99,102,71,20,17,45,34,44,43,94])).
% 97.93/98.03 cnf(7485,plain,
% 97.93/98.03 (P1(x74851,f48(a84,a84))),
% 97.93/98.03 inference(rename_variables,[],[647])).
% 97.93/98.03 cnf(7489,plain,
% 97.93/98.03 (P6(f48(a84,a84),a62,a4)),
% 97.93/98.03 inference(scs_inference,[],[4,1397,7383,7445,7399,7423,7455,6129,5405,6875,13,2,647,7472,7475,7478,7485,50,99,102,71,20,17,45,34,44,43,94,46,91,33])).
% 97.93/98.03 cnf(7503,plain,
% 97.93/98.03 (~P1(f10(a59,a58),f74(a59))),
% 97.93/98.03 inference(scs_inference,[],[1406,7482,7401,50,99,102,71,20])).
% 97.93/98.03 cnf(7508,plain,
% 97.93/98.03 (P1(x75081,f74(a58))),
% 97.93/98.03 inference(rename_variables,[],[576])).
% 97.93/98.03 cnf(7513,plain,
% 97.93/98.03 (~P2(a73,a89)),
% 97.93/98.04 inference(scs_inference,[],[4,1406,7482,7467,7395,7281,7401,1871,647,576,50,99,102,71,20,17,34,43,94])).
% 97.93/98.04 cnf(7520,plain,
% 97.93/98.04 (P6(a62,f74(a58),a4)),
% 97.93/98.04 inference(scs_inference,[],[4,1406,7482,7467,7395,7417,7281,7415,7401,1871,647,576,7508,951,50,99,102,71,20,17,34,43,94,46,91,33])).
% 97.93/98.04 cnf(7522,plain,
% 97.93/98.04 (P1(f29(a71,a62),a71)),
% 97.93/98.04 inference(scs_inference,[],[4,1406,7482,7467,7395,7417,7281,7415,7401,5981,1871,647,576,7508,951,50,99,102,71,20,17,34,43,94,46,91,33,78])).
% 97.93/98.04 cnf(7525,plain,
% 97.93/98.04 (P1(f32(a71,a62),a71)),
% 97.93/98.04 inference(scs_inference,[],[4,1406,7482,7467,7395,7417,7281,7415,7401,5975,5981,1871,647,576,7508,951,50,99,102,71,20,17,34,43,94,46,91,33,78,41])).
% 97.93/98.04 cnf(7552,plain,
% 97.93/98.04 (~P1(f29(a71,a62),f74(a71))),
% 97.93/98.04 inference(scs_inference,[],[1449,7513,7522,99,50,102,71,20])).
% 97.93/98.04 cnf(7561,plain,
% 97.93/98.04 (P1(x75611,f74(a58))),
% 97.93/98.04 inference(rename_variables,[],[576])).
% 97.93/98.04 cnf(7569,plain,
% 97.93/98.04 (~P2(a86,a73)),
% 97.93/98.04 inference(scs_inference,[],[4,1449,7513,5113,7503,7522,5544,5226,647,576,951,99,50,102,71,20,17,49,47,34,44,43,94])).
% 97.93/98.04 cnf(7589,plain,
% 97.93/98.04 (~P1(f14(a62,a2),a2)),
% 97.93/98.04 inference(scs_inference,[],[4,1449,7513,5113,7503,7522,5425,5544,5226,647,576,7561,951,8,99,50,102,71,20,17,49,47,34,44,43,94,46,33,27,29,32,30,28,31,77])).
% 97.93/98.04 cnf(7595,plain,
% 97.93/98.04 (P3(a73,a4)),
% 97.93/98.04 inference(scs_inference,[],[4,1449,7513,5113,6024,7503,6166,7522,7520,600,5425,5544,5226,647,576,7561,951,8,99,50,102,71,20,17,49,47,34,44,43,94,46,33,27,29,32,30,28,31,77,75,100])).
% 97.93/98.04 cnf(7625,plain,
% 97.93/98.04 ($false),
% 97.93/98.04 inference(scs_inference,[],[4,1497,7569,7595,5592,5581,7489,7552,7525,7589,7522,13,14,8,70,69,50,99,102,71,20,17,34,43,94,46,91]),
% 97.93/98.04 ['proof']).
% 97.93/98.04 % SZS output end Proof
% 97.93/98.04 % Total time :97.260000s
%------------------------------------------------------------------------------