%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : KRS217+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 : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 10:08:54 EDT 2024
% Result : Theorem 96.53s 97.25s
% Output : CNFRefutation 96.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS217+1 : TPTP v8.2.0. Bugfixed v5.4.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.11/0.34 % Computer : n009.cluster.edu
% 0.11/0.34 % Model : x86_64 x86_64
% 0.11/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.34 % Memory : 8042.1875MB
% 0.11/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.34 % CPULimit : 300
% 0.11/0.34 % WCLimit : 300
% 0.11/0.34 % DateTime : Wed Jun 19 13:20:53 EDT 2024
% 0.11/0.34 % CPUTime :
% 0.47/0.55 start to proof:theBenchmark
% 96.53/97.24 %-------------------------------------------
% 96.53/97.24 % File :CSE---1.7
% 96.53/97.24 % Problem :theBenchmark
% 96.53/97.24 % Transform :cnf
% 96.53/97.24 % Format :tptp:raw
% 96.53/97.24 % Command :java -jar mcs_scs.jar %d %s
% 96.53/97.24
% 96.53/97.24 % Result :Theorem 96.020000s
% 96.53/97.24 % Output :CNFRefutation 96.020000s
% 96.53/97.24 %-------------------------------------------
% 96.53/97.25 %------------------------------------------------------------------------------
% 96.53/97.25 % File : KRS217+1 : TPTP v8.2.0. Bugfixed v5.4.0.
% 96.53/97.25 % Domain : Knowledge Representation
% 96.53/97.25 % Problem : NOC nota THM
% 96.53/97.25 % Version : [Sut08] axioms.
% 96.53/97.25 % English :
% 96.53/97.25
% 96.53/97.25 % Refs : [Sut08] Sutcliffe (2008), The SZS Ontologies for Automated Rea
% 96.53/97.25 % Source : [TPTP]
% 96.53/97.25 % Names :
% 96.53/97.25
% 96.53/97.25 % Status : Theorem
% 96.53/97.25 % Rating : 0.19 v8.2.0, 0.27 v8.1.0, 0.14 v7.5.0, 0.33 v7.4.0, 0.19 v7.3.0, 0.43 v7.2.0, 0.33 v7.1.0, 0.25 v7.0.0, 0.14 v6.4.0, 0.07 v6.3.0, 0.15 v6.2.0, 0.27 v6.1.0, 0.40 v6.0.0, 0.50 v5.5.0, 0.54 v5.4.0
% 96.53/97.25 % Syntax : Number of formulae : 33 ( 3 unt; 0 def)
% 96.53/97.25 % Number of atoms : 107 ( 0 equ)
% 96.53/97.25 % Maximal formula atoms : 7 ( 3 avg)
% 96.53/97.25 % Number of connectives : 96 ( 22 ~; 1 |; 35 &)
% 96.53/97.25 % ( 28 <=>; 8 =>; 0 <=; 2 <~>)
% 96.53/97.25 % Maximal formula depth : 10 ( 6 avg)
% 96.53/97.25 % Maximal term depth : 2 ( 1 avg)
% 96.53/97.25 % Number of predicates : 7 ( 7 usr; 0 prp; 2-3 aty)
% 96.53/97.25 % Number of functors : 20 ( 20 usr; 19 con; 0-1 aty)
% 96.53/97.25 % Number of variables : 122 ( 72 !; 50 ?)
% 96.53/97.25 % SPC : FOF_THM_RFO_NEQ
% 96.53/97.25
% 96.53/97.25 % Comments :
% 96.53/97.25 % Bugfixes : v5.4.0 - Added missing axiom in KRS001+1.ax
% 96.53/97.25 %------------------------------------------------------------------------------
% 96.53/97.25 %----Include SZS success ontology nodes
% 96.53/97.25 include('Axioms/KRS001+0.ax').
% 96.53/97.25 %----Include SZS success ontology node relationships
% 96.53/97.25 include('Axioms/KRS001+1.ax').
% 96.53/97.25 %------------------------------------------------------------------------------
% 96.53/97.25 fof(nota_noc_thm,conjecture,
% 96.53/97.25 nota(noc,thm) ).
% 96.53/97.25
% 96.53/97.25 %------------------------------------------------------------------------------
% 96.53/97.25 %-------------------------------------------
% 96.53/97.25 % Proof found
% 96.53/97.25 % SZS status Theorem for theBenchmark
% 96.53/97.25 % SZS output start Proof
% 96.53/97.25 %ClaNum:109(EqnAxiom:0)
% 96.53/97.25 %VarNum:590(SingletonVarNum:249)
% 96.53/97.25 %MaxLitNum:6
% 96.53/97.25 %MaxfuncDepth:1
% 96.53/97.25 %SharedTerms:52
% 96.53/97.25 %goalClause: 13
% 96.53/97.25 %singleGoalClaCount:1
% 96.53/97.25 [1]P1(a1,a2)
% 96.53/97.25 [2]P1(a55,a56)
% 96.53/97.25 [3]P1(a55,a59)
% 96.53/97.25 [4]P1(a61,a62)
% 96.53/97.25 [5]P1(a66,a65)
% 96.53/97.25 [6]P1(a67,a69)
% 96.53/97.25 [7]P1(a70,a71)
% 96.53/97.25 [9]~P1(a57,a2)
% 96.53/97.25 [10]~P1(a66,a62)
% 96.53/97.25 [11]~P1(a68,a65)
% 96.53/97.25 [12]~P1(a67,a71)
% 96.53/97.25 [13]~P4(a73,a78)
% 96.53/97.25 [8]P1(x81,a3)
% 96.53/97.25 [14]~P1(x141,a58)
% 96.53/97.25 [18]~P1(a63,a56)+~P1(a64,a59)
% 96.53/97.25 [15]~P1(x151,a62)+P1(x151,a65)
% 96.53/97.25 [17]P1(x171,x172)+P1(x171,f79(x172))
% 96.53/97.25 [20]~P1(x201,x202)+~P1(x201,f79(x202))
% 96.53/97.25 [21]P6(x211,x212,a5)+P1(f4(x211),x211)
% 96.53/97.25 [24]P6(x241,x242,a86)+P1(f6(x241,x242),x242)
% 96.53/97.25 [25]P6(x251,x252,a80)+P1(f31(x251,x252),x251)
% 96.53/97.25 [26]P6(x261,x262,a78)+P1(f7(x261,x262),x261)
% 96.53/97.25 [42]P6(x421,x422,a78)+~P1(f7(x421,x422),x422)
% 96.53/97.25 [50]P2(x501,x502)+P6(f41(x501,x502),f47(x501,x502),x501)
% 96.53/97.25 [51]P5(x511,x512)+P6(f48(x511,x512),f51(x511,x512),x512)
% 96.53/97.25 [52]P5(x521,x522)+P6(f48(x521,x522),f51(x521,x522),x521)
% 96.53/97.25 [53]~P6(x531,x532,a82)+P1(f75(x531,x532),x532)
% 96.53/97.25 [54]~P6(x541,x542,a82)+P1(f75(x541,x542),x541)
% 96.53/97.25 [55]~P6(x551,x552,a10)+P1(f11(x551,x552),x551)
% 96.53/97.25 [56]~P6(x561,x562,a81)+P1(f13(x561,x562),x561)
% 96.53/97.25 [57]~P6(x571,x572,a90)+P1(f15(x571,x572),x571)
% 96.53/97.25 [58]~P6(x581,x582,a90)+P1(f17(x581,x582),x582)
% 96.53/97.26 [59]~P6(x591,x592,a74)+P1(f18(x591,x592),x591)
% 96.53/97.26 [60]~P6(x601,x602,a87)+P1(f20(x601,x602),x601)
% 96.53/97.26 [61]~P6(x611,x612,a91)+P1(f25(x611,x612),x611)
% 96.53/97.26 [62]~P6(x621,x622,a91)+P1(f28(x621,x622),x622)
% 96.53/97.26 [63]~P6(x631,x632,a83)+P1(f33(x631,x632),x632)
% 96.53/97.26 [64]~P6(x641,x642,a89)+P1(f34(x641,x642),x642)
% 96.53/97.26 [65]~P6(x651,x652,a9)+P1(f38(x651,x652),x651)
% 96.53/97.26 [66]~P6(x661,x662,a73)+P1(f42(x661,x662),x662)
% 96.53/97.26 [67]~P6(x671,x672,a73)+P1(f42(x671,x672),x671)
% 96.53/97.26 [68]~P6(x681,x682,a73)+P1(f44(x681,x682),x681)
% 96.53/97.26 [69]~P3(x691,x692)+P6(f45(x691,x692),f46(x691,x692),x692)
% 96.53/97.26 [70]~P3(x701,x702)+P6(f45(x701,x702),f46(x701,x702),x701)
% 96.53/97.26 [71]~P4(x711,x712)+P6(f49(x711,x712),f50(x711,x712),x711)
% 96.53/97.26 [72]~P6(x721,x722,a9)+P1(f38(x721,x722),f79(x722))
% 96.53/97.26 [73]~P6(x731,x732,a73)+P1(f44(x731,x732),f79(x732))
% 96.53/97.26 [82]~P6(x821,x822,a90)+~P1(f17(x821,x822),x821)
% 96.53/97.26 [83]~P6(x831,x832,a74)+~P1(f21(x831,x832),x831)
% 96.53/97.26 [84]~P6(x841,x842,a87)+~P1(f26(x841,x842),x841)
% 96.53/97.26 [85]~P6(x851,x852,a91)+~P1(f28(x851,x852),x851)
% 96.53/97.26 [86]~P6(x861,x862,a91)+~P1(f30(x861,x862),x862)
% 96.53/97.26 [87]~P6(x871,x872,a89)+~P1(f39(x871,x872),x872)
% 96.53/97.26 [99]P2(x991,x992)+~P6(f41(x991,x992),f47(x991,x992),x992)
% 96.53/97.26 [102]~P4(x1021,x1022)+~P6(f49(x1021,x1022),f50(x1021,x1022),x1022)
% 96.53/97.26 [22]~P1(x223,x222)+P6(x221,x222,a80)
% 96.53/97.26 [23]~P1(x233,x231)+P6(x231,x232,a86)
% 96.53/97.26 [27]P1(x271,x272)+~P6(x273,x272,a81)
% 96.53/97.26 [28]P1(x281,x282)+~P6(x283,x282,a84)
% 96.53/97.26 [29]P1(x291,x292)+~P6(x293,x292,a87)
% 96.53/97.26 [30]P1(x301,x302)+~P6(x303,x302,a85)
% 96.53/97.26 [31]P1(x311,x312)+~P6(x312,x313,a84)
% 96.53/97.26 [32]P1(x321,x322)+~P6(x322,x323,a88)
% 96.53/97.26 [36]~P1(x361,x362)+~P6(x362,x363,a5)
% 96.53/97.26 [37]~P1(x371,x372)+~P6(x372,x373,a83)
% 96.53/97.26 [38]~P1(x381,x382)+~P6(x382,x383,a85)
% 96.53/97.26 [39]~P1(x391,x392)+~P6(x392,x393,a89)
% 96.53/97.26 [35]~P6(x353,x352,a88)+P1(x351,f79(x352))
% 96.53/97.26 [76]P6(x761,x762,a8)+P1(f60(x761,x762),x761)+P1(f72(x761,x762),x762)
% 96.53/97.26 [93]P6(x931,x932,a85)+P1(f36(x931,x932),x931)+~P1(f37(x931,x932),x932)
% 96.53/97.26 [98]P6(x981,x982,a84)+~P1(f23(x981,x982),x981)+~P1(f24(x981,x982),x982)
% 96.53/97.26 [101]P6(x1011,x1012,a88)+~P1(f40(x1011,x1012),x1011)+~P1(f43(x1011,x1012),f79(x1012))
% 96.53/97.26 [108]P7(x1081,x1082)+P6(f53(x1081,x1082),f54(x1081,x1082),x1082)+~P6(f53(x1081,x1082),f54(x1081,x1082),x1081)
% 96.53/97.26 [109]P7(x1091,x1092)+P6(f53(x1091,x1092),f54(x1091,x1092),x1091)+~P6(f53(x1091,x1092),f54(x1091,x1092),x1092)
% 96.53/97.26 [34]~P1(x343,x341)+~P1(x343,x342)+P6(x341,x342,a82)
% 96.53/97.26 [43]P1(x431,x432)+~P1(x431,x433)+~P6(x433,x432,a78)
% 96.53/97.26 [44]P1(x441,x442)+~P1(x441,x443)+~P6(x442,x443,a10)
% 96.53/97.26 [45]P1(x451,x452)+~P1(x451,x453)+~P6(x452,x453,a74)
% 96.53/97.26 [46]P1(x461,x462)+~P1(x461,x463)+~P6(x463,x462,a10)
% 96.53/97.26 [47]P1(x471,x472)+~P1(x471,x473)+~P6(x473,x472,a90)
% 96.53/97.26 [48]P1(x481,x482)+~P1(x481,x483)+~P6(x483,x482,a74)
% 96.53/97.26 [49]P1(x491,x492)+~P1(x491,x493)+~P6(x493,x492,a91)
% 96.53/97.26 [40]~P1(x403,x401)+P6(x401,x402,a9)+~P1(x403,f79(x402))
% 96.53/97.26 [41]~P1(x413,x412)+P6(x411,x412,a83)+P1(f32(x411,x412),x411)
% 96.53/97.26 [77]~P1(x773,x771)+P6(x771,x772,a81)+~P1(f14(x771,x772),x772)
% 96.53/97.26 [78]~P1(x783,x782)+~P6(x781,x782,a86)+P1(f29(x781,x782),x781)
% 96.53/97.26 [79]~P1(x793,x791)+~P6(x791,x792,a80)+P1(f52(x791,x792),x792)
% 96.53/97.26 [80]~P1(x803,x801)+~P6(x801,x802,a8)+P1(f76(x801,x802),x802)
% 96.53/97.26 [81]~P1(x813,x812)+~P6(x811,x812,a8)+P1(f77(x811,x812),x811)
% 96.53/97.26 [33]~P1(x333,x332)+~P1(x334,x331)+P6(x331,x332,a8)
% 96.53/97.26 [75]~P7(x754,x753)+P6(x751,x752,x753)+P6(x751,x752,x754)
% 96.53/97.26 [91]~P6(x913,x914,x911)+P4(x911,x912)+P6(x913,x914,x912)
% 96.53/97.26 [94]~P6(x941,x942,x944)+P6(x941,x942,x943)+~P2(x944,x943)
% 96.53/97.26 [100]~P6(x1003,x1004,x1001)+P3(x1001,x1002)+~P6(x1003,x1004,x1002)
% 96.53/97.26 [104]~P6(x1043,x1044,x1041)+~P5(x1041,x1042)+~P6(x1043,x1044,x1042)
% 96.53/97.26 [105]~P6(x1053,x1054,x1051)+~P7(x1051,x1052)+~P6(x1053,x1054,x1052)
% 96.53/97.26 [92]~P1(x923,x921)+P6(x921,x922,a10)+P1(f12(x921,x922),x922)+P1(f12(x921,x922),x921)
% 96.53/97.26 [106]~P1(x1063,x1061)+P6(x1061,x1062,a10)+~P1(f12(x1061,x1062),x1062)+~P1(f12(x1061,x1062),x1061)
% 96.53/97.26 [74]P1(x741,x742)+~P1(x744,x742)+P6(x743,x742,a89)+P1(f35(x743,x742),x743)
% 96.53/97.26 [90]P1(x901,x902)+~P1(x904,x902)+P6(x902,x903,a87)+~P1(f22(x902,x903),x903)
% 96.53/97.26 [88]~P1(x881,x883)+P1(x881,x882)+~P1(x884,x882)+P6(x882,x883,a90)+P1(f16(x882,x883),x882)
% 96.53/97.26 [89]~P1(x894,x891)+~P1(x893,x891)+~P1(x894,x892)+P6(x891,x892,a73)+~P1(x893,f79(x892))
% 96.53/97.26 [96]P1(x961,x962)+~P1(x964,x962)+P6(x962,x963,a74)+P1(f19(x962,x963),x963)+P1(f19(x962,x963),x962)
% 96.53/97.26 [97]~P1(x971,x973)+P1(x971,x972)+~P1(x974,x972)+P6(x972,x973,a90)+~P1(f16(x972,x973),x973)
% 96.53/97.26 [107]P1(x1071,x1072)+~P1(x1074,x1072)+P6(x1072,x1073,a74)+~P1(f19(x1072,x1073),x1073)+~P1(f19(x1072,x1073),x1072)
% 96.53/97.26 [95]~P1(x953,x952)+P1(x951,x952)+P1(x953,x954)+~P1(x955,x954)+P6(x954,x952,a91)+P1(f27(x954,x952),x954)
% 96.53/97.26 [103]~P1(x1033,x1032)+P1(x1031,x1032)+P1(x1033,x1034)+~P1(x1035,x1034)+P6(x1034,x1032,a91)+~P1(f27(x1034,x1032),x1032)
% 96.53/97.26 %EqnAxiom
% 96.53/97.26
% 96.53/97.26 %-------------------------------------------
% 96.53/97.27 cnf(110,plain,
% 96.53/97.27 (P6(a58,x1101,a5)),
% 96.53/97.27 inference(scs_inference,[],[14,21])).
% 96.53/97.27 cnf(111,plain,
% 96.53/97.27 (~P1(x1111,a58)),
% 96.53/97.27 inference(rename_variables,[],[14])).
% 96.53/97.27 cnf(113,plain,
% 96.53/97.27 (P6(x1131,a58,a86)),
% 96.53/97.27 inference(scs_inference,[],[14,111,21,24])).
% 96.53/97.27 cnf(114,plain,
% 96.53/97.27 (~P1(x1141,a58)),
% 96.53/97.27 inference(rename_variables,[],[14])).
% 96.53/97.27 cnf(116,plain,
% 96.53/97.27 (P6(a58,x1161,a80)),
% 96.53/97.27 inference(scs_inference,[],[14,111,114,21,24,25])).
% 96.53/97.27 cnf(117,plain,
% 96.53/97.27 (~P1(x1171,a58)),
% 96.53/97.27 inference(rename_variables,[],[14])).
% 96.53/97.27 cnf(119,plain,
% 96.53/97.27 (P6(a58,x1191,a78)),
% 96.53/97.27 inference(scs_inference,[],[14,111,114,117,21,24,25,26])).
% 96.53/97.27 cnf(120,plain,
% 96.53/97.27 (~P1(x1201,a58)),
% 96.53/97.27 inference(rename_variables,[],[14])).
% 96.53/97.27 cnf(122,plain,
% 96.53/97.27 (P6(x1221,a3,a78)),
% 96.53/97.27 inference(scs_inference,[],[8,14,111,114,117,21,24,25,26,42])).
% 96.53/97.27 cnf(123,plain,
% 96.64/97.27 (P1(x1231,a3)),
% 96.64/97.27 inference(rename_variables,[],[8])).
% 96.64/97.27 cnf(125,plain,
% 96.64/97.27 (~P1(a68,a62)),
% 96.64/97.27 inference(scs_inference,[],[8,14,111,114,117,11,21,24,25,26,42,15])).
% 96.64/97.27 cnf(127,plain,
% 96.64/97.27 (~P6(x1271,a58,a82)),
% 96.64/97.27 inference(scs_inference,[],[8,14,111,114,117,120,11,21,24,25,26,42,15,53])).
% 96.64/97.27 cnf(128,plain,
% 96.64/97.27 (~P1(x1281,a58)),
% 96.64/97.27 inference(rename_variables,[],[14])).
% 96.64/97.27 cnf(130,plain,
% 96.64/97.27 (~P6(a58,x1301,a82)),
% 96.64/97.27 inference(scs_inference,[],[8,14,111,114,117,120,128,11,21,24,25,26,42,15,53,54])).
% 96.64/97.27 cnf(131,plain,
% 96.64/97.27 (~P1(x1311,a58)),
% 96.64/97.27 inference(rename_variables,[],[14])).
% 96.64/97.27 cnf(133,plain,
% 96.64/97.27 (~P6(a58,x1331,a10)),
% 96.64/97.27 inference(scs_inference,[],[8,14,111,114,117,120,128,131,11,21,24,25,26,42,15,53,54,55])).
% 96.64/97.27 cnf(134,plain,
% 96.64/97.27 (~P1(x1341,a58)),
% 96.64/97.27 inference(rename_variables,[],[14])).
% 96.64/97.27 cnf(136,plain,
% 96.64/97.27 (~P6(a58,x1361,a81)),
% 96.64/97.27 inference(scs_inference,[],[8,14,111,114,117,120,128,131,134,11,21,24,25,26,42,15,53,54,55,56])).
% 96.64/97.27 cnf(137,plain,
% 96.64/97.27 (~P1(x1371,a58)),
% 96.64/97.27 inference(rename_variables,[],[14])).
% 96.64/97.27 cnf(139,plain,
% 96.64/97.27 (~P6(a58,x1391,a90)),
% 96.64/97.27 inference(scs_inference,[],[8,14,111,114,117,120,128,131,134,137,11,21,24,25,26,42,15,53,54,55,56,57])).
% 96.64/97.27 cnf(140,plain,
% 96.64/97.27 (~P1(x1401,a58)),
% 96.64/97.27 inference(rename_variables,[],[14])).
% 96.64/97.27 cnf(142,plain,
% 96.64/97.27 (~P6(x1421,a58,a90)),
% 96.64/97.27 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])).
% 96.64/97.27 cnf(143,plain,
% 96.64/97.27 (~P1(x1431,a58)),
% 96.64/97.27 inference(rename_variables,[],[14])).
% 96.64/97.27 cnf(145,plain,
% 96.64/97.27 (~P6(a58,x1451,a74)),
% 96.64/97.27 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])).
% 96.64/97.27 cnf(146,plain,
% 96.64/97.27 (~P1(x1461,a58)),
% 96.64/97.27 inference(rename_variables,[],[14])).
% 96.64/97.27 cnf(148,plain,
% 96.64/97.27 (~P6(a58,x1481,a87)),
% 96.64/97.27 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])).
% 96.64/97.27 cnf(149,plain,
% 96.64/97.27 (~P1(x1491,a58)),
% 96.64/97.27 inference(rename_variables,[],[14])).
% 96.64/97.27 cnf(152,plain,
% 96.64/97.27 (~P1(x1521,a58)),
% 96.64/97.27 inference(rename_variables,[],[14])).
% 96.64/97.27 cnf(154,plain,
% 96.64/97.27 (~P6(x1541,a58,a91)),
% 96.64/97.27 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])).
% 96.64/97.27 cnf(155,plain,
% 96.64/97.27 (~P1(x1551,a58)),
% 96.64/97.27 inference(rename_variables,[],[14])).
% 96.64/97.27 cnf(157,plain,
% 96.64/97.27 (~P6(x1571,a58,a83)),
% 96.64/97.27 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])).
% 96.64/97.27 cnf(158,plain,
% 96.64/97.27 (~P1(x1581,a58)),
% 96.64/97.27 inference(rename_variables,[],[14])).
% 96.64/97.27 cnf(160,plain,
% 96.64/97.27 (~P6(x1601,a58,a89)),
% 96.64/97.27 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])).
% 96.64/97.27 cnf(161,plain,
% 96.64/97.27 (~P1(x1611,a58)),
% 96.64/97.27 inference(rename_variables,[],[14])).
% 96.64/97.27 cnf(163,plain,
% 96.64/97.27 (~P6(a58,x1631,a9)),
% 96.64/97.27 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])).
% 96.64/97.27 cnf(164,plain,
% 96.64/97.27 (~P1(x1641,a58)),
% 96.64/97.27 inference(rename_variables,[],[14])).
% 96.64/97.27 cnf(166,plain,
% 96.64/97.27 (~P6(x1661,a58,a73)),
% 96.64/97.27 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])).
% 96.64/97.27 cnf(167,plain,
% 96.64/97.27 (~P1(x1671,a58)),
% 96.64/97.27 inference(rename_variables,[],[14])).
% 96.64/97.27 cnf(169,plain,
% 96.64/97.27 (~P6(a58,x1691,a73)),
% 96.64/97.27 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])).
% 96.64/97.27 cnf(170,plain,
% 96.64/97.27 (~P1(x1701,a58)),
% 96.64/97.27 inference(rename_variables,[],[14])).
% 96.64/97.27 cnf(172,plain,
% 96.64/97.27 (~P6(a3,x1721,a90)),
% 96.64/97.27 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])).
% 96.64/97.27 cnf(173,plain,
% 96.64/97.27 (P1(x1731,a3)),
% 96.64/97.27 inference(rename_variables,[],[8])).
% 96.64/97.27 cnf(175,plain,
% 96.64/97.27 (~P6(a3,x1751,a74)),
% 96.64/97.27 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])).
% 96.64/97.27 cnf(176,plain,
% 96.64/97.27 (P1(x1761,a3)),
% 96.64/97.27 inference(rename_variables,[],[8])).
% 96.64/97.27 cnf(178,plain,
% 96.64/97.27 (~P6(a3,x1781,a87)),
% 96.64/97.27 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])).
% 96.64/97.27 cnf(179,plain,
% 96.64/97.27 (P1(x1791,a3)),
% 96.64/97.27 inference(rename_variables,[],[8])).
% 96.64/97.27 cnf(181,plain,
% 96.64/97.27 (~P6(a3,x1811,a91)),
% 96.64/97.27 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])).
% 96.64/97.27 cnf(182,plain,
% 96.64/97.27 (P1(x1821,a3)),
% 96.64/97.27 inference(rename_variables,[],[8])).
% 96.64/97.27 cnf(185,plain,
% 96.64/97.27 (P1(x1851,a3)),
% 96.64/97.27 inference(rename_variables,[],[8])).
% 96.64/97.27 cnf(188,plain,
% 96.64/97.27 (P1(x1881,a3)),
% 96.64/97.27 inference(rename_variables,[],[8])).
% 96.64/97.27 cnf(190,plain,
% 96.64/97.27 (P4(a5,a82)),
% 96.64/97.27 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])).
% 96.64/97.27 cnf(194,plain,
% 96.64/97.27 (P6(a58,a3,a85)),
% 96.64/97.27 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])).
% 96.64/97.27 cnf(195,plain,
% 96.64/97.27 (~P1(x1951,a58)),
% 96.64/97.27 inference(rename_variables,[],[14])).
% 96.64/97.27 cnf(196,plain,
% 96.64/97.27 (P1(x1961,a3)),
% 96.64/97.27 inference(rename_variables,[],[8])).
% 96.64/97.27 cnf(198,plain,
% 96.64/97.27 (~P6(a3,a58,a8)),
% 96.64/97.27 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])).
% 96.64/97.27 cnf(199,plain,
% 96.64/97.27 (~P1(x1991,a58)),
% 96.64/97.27 inference(rename_variables,[],[14])).
% 96.64/97.27 cnf(201,plain,
% 96.64/97.27 (~P6(a58,a3,a8)),
% 96.64/97.27 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])).
% 96.64/97.27 cnf(202,plain,
% 96.64/97.27 (~P1(x2021,a58)),
% 96.64/97.27 inference(rename_variables,[],[14])).
% 96.64/97.27 cnf(210,plain,
% 96.64/97.27 (P6(a3,a3,a10)),
% 96.64/97.27 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])).
% 96.64/97.27 cnf(211,plain,
% 96.64/97.27 (P1(x2111,a3)),
% 96.64/97.27 inference(rename_variables,[],[8])).
% 96.64/97.27 cnf(212,plain,
% 96.64/97.27 (P1(x2121,a3)),
% 96.64/97.27 inference(rename_variables,[],[8])).
% 96.64/97.27 cnf(214,plain,
% 96.64/97.27 (P6(a3,a3,a84)),
% 96.64/97.27 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])).
% 96.64/97.27 cnf(215,plain,
% 96.64/97.27 (P1(x2151,a3)),
% 96.64/97.27 inference(rename_variables,[],[8])).
% 96.64/97.27 cnf(218,plain,
% 96.64/97.27 (P6(a3,x2181,a88)+~P1(f43(a3,x2181),f79(x2181))),
% 96.64/97.27 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])).
% 96.64/97.27 cnf(222,plain,
% 96.64/97.27 (~P6(x2221,a58,a88)+P6(a3,a58,a88)),
% 96.64/97.27 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])).
% 96.64/97.27 cnf(229,plain,
% 96.64/97.27 (~P7(a10,a82)),
% 96.64/97.27 inference(scs_inference,[],[127,133,75])).
% 96.64/97.27 cnf(230,plain,
% 96.64/97.27 (~P6(a58,x2301,a10)),
% 96.64/97.27 inference(rename_variables,[],[133])).
% 96.64/97.27 cnf(233,plain,
% 96.64/97.27 (~P6(a2,a58,a8)),
% 96.64/97.27 inference(scs_inference,[],[127,133,1,14,75,80])).
% 96.64/97.27 cnf(234,plain,
% 96.64/97.27 (~P1(x2341,a58)),
% 96.64/97.27 inference(rename_variables,[],[14])).
% 96.64/97.27 cnf(236,plain,
% 96.64/97.27 (P4(a5,a10)),
% 96.64/97.27 inference(scs_inference,[],[110,127,133,230,1,14,75,80,91])).
% 96.64/97.27 cnf(239,plain,
% 96.64/97.27 (~P6(a58,a2,a8)),
% 96.64/97.27 inference(scs_inference,[],[110,127,133,230,1,14,234,75,80,91,81])).
% 96.64/97.28 cnf(242,plain,
% 96.64/97.28 (P3(a5,a86)),
% 96.64/97.28 inference(scs_inference,[],[110,113,127,133,230,1,14,234,75,80,91,81,100])).
% 96.64/97.28 cnf(243,plain,
% 96.64/97.28 (P6(x2431,a58,a86)),
% 96.64/97.28 inference(rename_variables,[],[113])).
% 96.64/97.28 cnf(244,plain,
% 96.64/97.28 (P6(a58,x2441,a5)),
% 96.64/97.28 inference(rename_variables,[],[110])).
% 96.64/97.28 cnf(247,plain,
% 96.64/97.28 (P6(x2471,a58,a86)),
% 96.64/97.28 inference(rename_variables,[],[113])).
% 96.64/97.28 cnf(248,plain,
% 96.64/97.28 (P6(a58,x2481,a5)),
% 96.64/97.28 inference(rename_variables,[],[110])).
% 96.64/97.28 cnf(250,plain,
% 96.64/97.28 (~P5(a5,a86)),
% 96.64/97.28 inference(scs_inference,[],[110,244,248,113,243,247,127,133,230,1,14,234,75,80,91,81,100,105,104])).
% 96.64/97.28 cnf(254,plain,
% 96.64/97.28 (P6(a3,x2541,a84)+~P1(f24(a3,x2541),x2541)),
% 96.64/97.28 inference(scs_inference,[],[110,244,248,113,243,247,127,133,230,1,8,14,234,75,80,91,81,100,105,104,98])).
% 96.64/97.28 cnf(280,plain,
% 96.64/97.28 (~P5(a85,a85)),
% 96.64/97.28 inference(scs_inference,[],[194,198,75,104])).
% 96.64/97.28 cnf(282,plain,
% 96.64/97.28 (P4(a86,a8)),
% 96.64/97.28 inference(scs_inference,[],[194,113,198,75,104,91])).
% 96.64/97.28 cnf(285,plain,
% 96.64/97.28 (P3(a85,a85)),
% 96.64/97.28 inference(scs_inference,[],[194,113,198,75,104,91,100])).
% 96.64/97.28 cnf(289,plain,
% 96.64/97.28 (~P5(a5,a80)),
% 96.64/97.28 inference(scs_inference,[],[110,116,104])).
% 96.64/97.28 cnf(290,plain,
% 96.64/97.28 (P6(a58,x2901,a80)),
% 96.64/97.28 inference(rename_variables,[],[116])).
% 96.64/97.28 cnf(292,plain,
% 96.64/97.28 (~P7(a82,a8)),
% 96.64/97.28 inference(scs_inference,[],[110,116,201,130,104,75])).
% 96.64/97.28 cnf(295,plain,
% 96.64/97.28 (P3(a5,a80)),
% 96.64/97.28 inference(scs_inference,[],[110,116,290,201,130,104,75,100])).
% 96.64/97.28 cnf(298,plain,
% 96.64/97.28 (P4(a5,a8)),
% 96.64/97.28 inference(scs_inference,[],[110,116,290,201,130,104,75,100,91])).
% 96.64/97.28 cnf(304,plain,
% 96.64/97.28 (~P7(a81,a82)),
% 96.64/97.28 inference(scs_inference,[],[130,136,75])).
% 96.64/97.28 cnf(305,plain,
% 96.64/97.28 (~P6(a58,x3051,a81)),
% 96.64/97.28 inference(rename_variables,[],[136])).
% 96.64/97.28 cnf(307,plain,
% 96.64/97.28 (~P5(a5,a78)),
% 96.64/97.28 inference(scs_inference,[],[110,119,130,136,75,104])).
% 96.64/97.28 cnf(308,plain,
% 96.64/97.28 (P6(a58,x3081,a78)),
% 96.64/97.28 inference(rename_variables,[],[119])).
% 96.64/97.28 cnf(310,plain,
% 96.64/97.28 (P4(a5,a81)),
% 96.64/97.28 inference(scs_inference,[],[110,119,130,136,305,75,104,91])).
% 96.64/97.28 cnf(313,plain,
% 96.64/97.28 (P3(a5,a78)),
% 96.64/97.28 inference(scs_inference,[],[110,119,308,130,136,305,75,104,91,100])).
% 96.64/97.28 cnf(319,plain,
% 96.64/97.28 (~P5(a84,a84)),
% 96.64/97.28 inference(scs_inference,[],[214,104])).
% 96.64/97.28 cnf(322,plain,
% 96.64/97.28 (~P6(x3221,a58,a90)),
% 96.64/97.28 inference(rename_variables,[],[142])).
% 96.64/97.28 cnf(324,plain,
% 96.64/97.28 (P3(a84,a84)),
% 96.64/97.28 inference(scs_inference,[],[214,198,142,104,75,100])).
% 96.64/97.28 cnf(326,plain,
% 96.64/97.28 (P4(a5,a90)),
% 96.64/97.28 inference(scs_inference,[],[110,214,198,142,322,104,75,100,91])).
% 96.64/97.28 cnf(332,plain,
% 96.64/97.28 (~P7(a87,a8)),
% 96.64/97.28 inference(scs_inference,[],[201,148,75])).
% 96.64/97.28 cnf(333,plain,
% 96.64/97.28 (~P6(a58,x3331,a87)),
% 96.64/97.28 inference(rename_variables,[],[148])).
% 96.64/97.28 cnf(335,plain,
% 96.64/97.28 (~P5(a10,a10)),
% 96.64/97.28 inference(scs_inference,[],[210,201,148,75,104])).
% 96.64/97.28 cnf(337,plain,
% 96.64/97.28 (P4(a5,a87)),
% 96.64/97.28 inference(scs_inference,[],[110,210,201,148,333,75,104,91])).
% 96.64/97.28 cnf(340,plain,
% 96.64/97.28 (P3(a10,a10)),
% 96.64/97.28 inference(scs_inference,[],[110,210,201,148,333,75,104,91,100])).
% 96.64/97.28 cnf(344,plain,
% 96.64/97.28 (~P7(a91,a82)),
% 96.64/97.28 inference(scs_inference,[],[130,154,75])).
% 96.64/97.28 cnf(345,plain,
% 96.64/97.28 (~P6(x3451,a58,a91)),
% 96.64/97.28 inference(rename_variables,[],[154])).
% 96.64/97.28 cnf(348,plain,
% 96.64/97.28 (P4(a5,a91)),
% 96.64/97.28 inference(scs_inference,[],[110,130,154,345,75,91])).
% 96.64/97.28 cnf(353,plain,
% 96.64/97.28 (~P6(x3531,a58,a83)),
% 96.64/97.28 inference(rename_variables,[],[157])).
% 96.64/97.28 cnf(355,plain,
% 96.64/97.28 (P4(a5,a83)),
% 96.64/97.28 inference(scs_inference,[],[110,198,157,353,75,91])).
% 96.64/97.28 cnf(360,plain,
% 96.64/97.28 (~P6(x3601,a58,a89)),
% 96.64/97.28 inference(rename_variables,[],[160])).
% 96.64/97.28 cnf(363,plain,
% 96.64/97.28 (P4(a5,a89)),
% 96.64/97.28 inference(scs_inference,[],[110,130,160,360,75,91])).
% 96.64/97.28 cnf(368,plain,
% 96.64/97.28 (~P6(a58,x3681,a9)),
% 96.64/97.28 inference(rename_variables,[],[163])).
% 96.64/97.28 cnf(370,plain,
% 96.64/97.28 (P4(a5,a9)),
% 96.64/97.28 inference(scs_inference,[],[110,201,163,368,75,91])).
% 96.64/97.28 cnf(373,plain,
% 96.64/97.28 (P4(a5,a73)),
% 96.64/97.28 inference(scs_inference,[],[110,166,91])).
% 96.64/97.28 cnf(383,plain,
% 96.64/97.28 (P4(a78,a90)),
% 96.64/97.28 inference(scs_inference,[],[122,198,172,181,75,91])).
% 96.64/97.28 cnf(387,plain,
% 96.64/97.28 (P4(a86,a87)),
% 96.64/97.28 inference(scs_inference,[],[113,178,91])).
% 96.64/97.28 cnf(397,plain,
% 96.64/97.28 (P4(a5,a74)),
% 96.64/97.28 inference(scs_inference,[],[110,130,169,145,75,91])).
% 96.64/97.28 cnf(400,plain,
% 96.64/97.28 (P4(a78,a74)),
% 96.64/97.28 inference(scs_inference,[],[122,175,91])).
% 96.64/97.28 cnf(411,plain,
% 96.64/97.28 (P4(a86,a90)),
% 96.64/97.28 inference(scs_inference,[],[113,130,139,172,75,91])).
% 96.64/97.28 cnf(415,plain,
% 96.64/97.28 (P4(a78,a87)),
% 96.64/97.28 inference(scs_inference,[],[122,178,91])).
% 96.64/97.28 cnf(425,plain,
% 96.64/97.28 (P4(a86,a91)),
% 96.64/97.28 inference(scs_inference,[],[113,130,148,181,75,91])).
% 96.64/97.28 cnf(429,plain,
% 96.64/97.28 (P4(a78,a91)),
% 96.64/97.28 inference(scs_inference,[],[122,181,91])).
% 96.64/97.28 cnf(442,plain,
% 96.64/97.28 (P4(a10,a74)),
% 96.64/97.28 inference(scs_inference,[],[210,175,91])).
% 96.64/97.28 cnf(445,plain,
% 96.64/97.28 (P4(a86,a74)),
% 96.64/97.28 inference(scs_inference,[],[113,175,91])).
% 96.64/97.28 cnf(449,plain,
% 96.64/97.28 (~P1(a61,f79(a65))),
% 96.64/97.28 inference(scs_inference,[],[4,20,15])).
% 96.64/97.28 cnf(450,plain,
% 96.64/97.28 (P1(a61,a65)),
% 96.64/97.28 inference(scs_inference,[],[449,17])).
% 96.64/97.28 cnf(452,plain,
% 96.64/97.28 (~P6(x4521,a65,a88)),
% 96.64/97.28 inference(scs_inference,[],[449,17,35])).
% 96.64/97.28 cnf(454,plain,
% 96.64/97.28 (~P1(f43(a3,a65),f79(a65))),
% 96.64/97.28 inference(scs_inference,[],[8,449,17,35,101])).
% 96.64/97.28 cnf(459,plain,
% 96.64/97.28 (~P6(a3,a65,x4591)+P4(x4591,a88)),
% 96.64/97.28 inference(scs_inference,[],[8,449,17,35,101,75,91])).
% 96.64/97.28 cnf(481,plain,
% 96.64/97.28 (P6(a65,x4811,a86)),
% 96.64/97.28 inference(scs_inference,[],[454,23,17])).
% 96.64/97.28 cnf(482,plain,
% 96.64/97.28 (P1(f43(a3,a65),a65)),
% 96.64/97.28 inference(scs_inference,[],[454,17])).
% 96.64/97.28 cnf(484,plain,
% 96.64/97.28 (~P5(a78,a86)),
% 96.64/97.28 inference(scs_inference,[],[122,481,454,17,104])).
% 96.64/97.28 cnf(485,plain,
% 96.64/97.28 (P6(a65,x4851,a86)),
% 96.64/97.28 inference(rename_variables,[],[481])).
% 96.64/97.28 cnf(486,plain,
% 96.64/97.28 (P6(x4861,a3,a78)),
% 96.64/97.28 inference(rename_variables,[],[122])).
% 96.64/97.28 cnf(488,plain,
% 96.64/97.28 (P3(a78,a86)),
% 96.64/97.28 inference(scs_inference,[],[122,486,481,485,454,17,104,100])).
% 96.64/97.28 cnf(489,plain,
% 96.64/97.28 (P6(a65,x4891,a86)),
% 96.64/97.28 inference(rename_variables,[],[481])).
% 96.64/97.28 cnf(490,plain,
% 96.64/97.28 (P6(x4901,a3,a78)),
% 96.64/97.28 inference(rename_variables,[],[122])).
% 96.64/97.28 cnf(497,plain,
% 96.64/97.28 (~P6(x4971,a65,a88)),
% 96.64/97.28 inference(rename_variables,[],[452])).
% 96.64/97.28 cnf(500,plain,
% 96.64/97.28 (P4(a5,a88)),
% 96.64/97.28 inference(scs_inference,[],[110,122,486,490,481,485,489,454,130,452,497,17,104,100,105,75,91])).
% 96.64/97.28 cnf(504,plain,
% 96.64/97.28 (P4(a10,a87)),
% 96.64/97.28 inference(scs_inference,[],[210,178,91])).
% 96.64/97.28 cnf(511,plain,
% 96.64/97.28 (P4(a10,a90)),
% 96.64/97.28 inference(scs_inference,[],[210,172,91])).
% 96.64/97.28 cnf(517,plain,
% 96.64/97.28 (P4(a10,a91)),
% 96.64/97.28 inference(scs_inference,[],[210,181,91])).
% 96.64/97.28 cnf(524,plain,
% 96.64/97.28 (~P6(a56,a58,a8)),
% 96.64/97.28 inference(scs_inference,[],[2,14,80])).
% 96.64/97.28 cnf(525,plain,
% 96.64/97.28 (~P1(x5251,a58)),
% 96.64/97.28 inference(rename_variables,[],[14])).
% 96.64/97.28 cnf(527,plain,
% 96.64/97.28 (~P6(a58,a56,a8)),
% 96.64/97.28 inference(scs_inference,[],[2,14,525,80,81])).
% 96.64/97.28 cnf(535,plain,
% 96.64/97.28 (~P6(f79(a65),x5351,a88)),
% 96.64/97.28 inference(scs_inference,[],[452,32,218])).
% 96.64/97.28 cnf(536,plain,
% 96.64/97.28 (P4(a78,a88)),
% 96.64/97.28 inference(scs_inference,[],[122,535,91])).
% 96.64/97.28 cnf(548,plain,
% 96.64/97.28 (~P6(a3,x5481,a83)),
% 96.64/97.28 inference(scs_inference,[],[214,37,28])).
% 96.64/97.28 cnf(549,plain,
% 96.64/97.28 (~P6(a59,a58,a8)),
% 96.64/97.28 inference(scs_inference,[],[3,14,80])).
% 96.64/97.28 cnf(550,plain,
% 96.64/97.28 (~P1(x5501,a58)),
% 96.64/97.28 inference(rename_variables,[],[14])).
% 96.64/97.28 cnf(552,plain,
% 96.64/97.28 (~P6(a58,a59,a8)),
% 96.64/97.28 inference(scs_inference,[],[3,14,550,80,81])).
% 96.64/97.28 cnf(555,plain,
% 96.64/97.28 (P4(a10,a83)),
% 96.64/97.28 inference(scs_inference,[],[3,210,14,550,548,80,81,91])).
% 96.64/97.28 cnf(558,plain,
% 96.64/97.28 (~P6(a3,x5581,a89)),
% 96.64/97.28 inference(scs_inference,[],[194,39,30])).
% 96.64/97.28 cnf(559,plain,
% 96.64/97.28 (P4(a10,a89)),
% 96.64/97.28 inference(scs_inference,[],[210,558,91])).
% 96.64/97.28 cnf(567,plain,
% 96.64/97.28 (~P6(f49(x5671,a88),f50(x5671,a88),a88)+~P6(a3,a65,x5671)),
% 96.64/97.28 inference(scs_inference,[],[459,102])).
% 96.64/97.28 cnf(568,plain,
% 96.64/97.28 (~P6(a58,a62,a8)),
% 96.64/97.28 inference(scs_inference,[],[4,14,81])).
% 96.64/97.28 cnf(569,plain,
% 96.64/97.28 (~P1(x5691,a58)),
% 96.64/97.28 inference(rename_variables,[],[14])).
% 96.64/97.28 cnf(571,plain,
% 96.64/97.28 (~P6(a62,a58,a8)),
% 96.64/97.28 inference(scs_inference,[],[4,14,569,81,80])).
% 96.64/97.28 cnf(574,plain,
% 96.64/97.28 (~P2(a88,a8)+~P6(x5741,a58,a88)),
% 96.64/97.28 inference(scs_inference,[],[198,222,94])).
% 96.64/97.28 cnf(575,plain,
% 96.64/97.28 (~P1(f43(a3,a58),f79(a58))+~P2(a88,a8)),
% 96.64/97.28 inference(scs_inference,[],[574,218])).
% 96.64/97.28 cnf(576,plain,
% 96.64/97.28 (~P6(a65,a58,a8)),
% 96.64/97.28 inference(scs_inference,[],[5,14,80])).
% 96.64/97.28 cnf(577,plain,
% 96.64/97.28 (~P1(x5771,a58)),
% 96.64/97.28 inference(rename_variables,[],[14])).
% 96.64/97.28 cnf(579,plain,
% 96.64/97.28 (~P6(a58,a65,a8)),
% 96.64/97.28 inference(scs_inference,[],[5,14,577,80,81])).
% 96.64/97.28 cnf(583,plain,
% 96.64/97.28 (P6(a3,f79(a58),a84)),
% 96.64/97.28 inference(scs_inference,[],[14,254,17])).
% 96.64/97.28 cnf(584,plain,
% 96.64/97.28 (P1(x5841,f79(a58))),
% 96.64/97.28 inference(scs_inference,[],[583,28])).
% 96.64/97.28 cnf(589,plain,
% 96.64/97.28 (~P1(x5891,a58)),
% 96.64/97.28 inference(rename_variables,[],[14])).
% 96.64/97.28 cnf(591,plain,
% 96.64/97.28 (~P6(a69,a58,a8)),
% 96.64/97.28 inference(scs_inference,[],[6,583,14,589,28,42,81,80])).
% 96.64/97.28 cnf(594,plain,
% 96.64/97.28 (~P2(a88,a8)),
% 96.64/97.28 inference(scs_inference,[],[584,575])).
% 96.64/97.28 cnf(597,plain,
% 96.64/97.28 (P1(x5971,f79(a58))),
% 96.64/97.28 inference(rename_variables,[],[584])).
% 96.64/97.28 cnf(600,plain,
% 96.64/97.28 (P1(x6001,f79(a58))),
% 96.64/97.28 inference(rename_variables,[],[584])).
% 96.64/97.28 cnf(602,plain,
% 96.64/97.28 (~P6(f79(a58),x6021,a74)),
% 96.64/97.28 inference(scs_inference,[],[584,597,600,84,85,83])).
% 96.64/97.28 cnf(603,plain,
% 96.64/97.28 (P1(x6031,f79(a58))),
% 96.64/97.28 inference(rename_variables,[],[584])).
% 96.64/97.28 cnf(606,plain,
% 96.64/97.28 (P1(x6061,f79(a58))),
% 96.64/97.28 inference(rename_variables,[],[584])).
% 96.64/97.28 cnf(609,plain,
% 96.64/97.28 (P1(x6091,f79(a58))),
% 96.64/97.28 inference(rename_variables,[],[584])).
% 96.64/97.28 cnf(612,plain,
% 96.64/97.28 (P1(x6121,f79(a58))),
% 96.64/97.28 inference(rename_variables,[],[584])).
% 96.64/97.28 cnf(614,plain,
% 96.64/97.28 (P6(a3,a58,a88)),
% 96.64/97.28 inference(scs_inference,[],[8,584,597,600,603,606,609,612,84,85,83,86,82,87,101])).
% 96.64/97.28 cnf(615,plain,
% 96.64/97.28 (P1(x6151,a3)),
% 96.64/97.28 inference(rename_variables,[],[8])).
% 96.64/97.28 cnf(616,plain,
% 96.64/97.28 (P1(x6161,f79(a58))),
% 96.64/97.28 inference(rename_variables,[],[584])).
% 96.64/97.28 cnf(622,plain,
% 96.64/97.28 (~P5(a88,a88)),
% 96.64/97.28 inference(scs_inference,[],[8,615,584,597,600,603,606,609,612,616,84,85,83,86,82,87,101,98,104])).
% 96.64/97.28 cnf(624,plain,
% 96.64/97.28 (P3(a88,a88)),
% 96.64/97.28 inference(scs_inference,[],[8,615,584,597,600,603,606,609,612,616,84,85,83,86,82,87,101,98,104,100])).
% 96.64/97.28 cnf(644,plain,
% 96.64/97.28 (P6(f48(a5,a5),f51(a5,a5),a5)),
% 96.64/97.28 inference(scs_inference,[],[110,51,104])).
% 96.64/97.28 cnf(645,plain,
% 96.64/97.28 (~P1(x6451,f48(a5,a5))),
% 96.64/97.28 inference(scs_inference,[],[644,36])).
% 96.64/97.28 cnf(654,plain,
% 96.64/97.28 (P1(x6541,f48(a84,a84))),
% 96.64/97.28 inference(scs_inference,[],[319,52,31])).
% 96.64/97.28 cnf(655,plain,
% 96.64/97.28 (P6(x6551,f48(a5,a5),a86)),
% 96.64/97.28 inference(scs_inference,[],[645,24])).
% 96.64/97.28 cnf(656,plain,
% 96.64/97.28 (~P1(x6561,f48(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[645])).
% 96.64/97.28 cnf(659,plain,
% 96.64/97.28 (~P1(x6591,f48(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[645])).
% 96.64/97.28 cnf(662,plain,
% 96.64/97.28 (~P1(x6621,f48(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[645])).
% 96.64/97.28 cnf(665,plain,
% 96.64/97.28 (~P1(x6651,f48(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[645])).
% 96.64/97.28 cnf(668,plain,
% 96.64/97.28 (P1(x6681,f48(a84,a84))),
% 96.64/97.28 inference(rename_variables,[],[654])).
% 96.64/97.28 cnf(670,plain,
% 96.64/97.28 (P6(f48(a5,a5),x6701,a78)),
% 96.64/97.28 inference(scs_inference,[],[645,656,659,662,665,654,24,63,64,53,85,26])).
% 96.64/97.28 cnf(671,plain,
% 96.64/97.28 (~P1(x6711,f48(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[645])).
% 96.64/97.28 cnf(674,plain,
% 96.64/97.28 (~P1(x6741,f48(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[645])).
% 96.64/97.28 cnf(677,plain,
% 96.64/97.28 (~P1(x6771,f48(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[645])).
% 96.64/97.28 cnf(680,plain,
% 96.64/97.28 (~P1(x6801,f48(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[645])).
% 96.64/97.28 cnf(683,plain,
% 96.64/97.28 (~P1(x6831,f48(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[645])).
% 96.64/97.28 cnf(686,plain,
% 96.64/97.28 (~P1(x6861,f48(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[645])).
% 96.64/97.28 cnf(689,plain,
% 96.64/97.28 (P1(x6891,f48(a84,a84))),
% 96.64/97.28 inference(rename_variables,[],[654])).
% 96.64/97.28 cnf(692,plain,
% 96.64/97.28 (~P1(x6921,f48(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[645])).
% 96.64/97.28 cnf(695,plain,
% 96.64/97.28 (~P1(x6951,f48(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[645])).
% 96.64/97.28 cnf(698,plain,
% 96.64/97.28 (~P1(x6981,f48(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[645])).
% 96.64/97.28 cnf(701,plain,
% 96.64/97.28 (P1(x7011,f48(a84,a84))),
% 96.64/97.28 inference(rename_variables,[],[654])).
% 96.64/97.28 cnf(704,plain,
% 96.64/97.28 (~P1(x7041,f48(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[645])).
% 96.64/97.28 cnf(707,plain,
% 96.64/97.28 (~P1(x7071,f48(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[645])).
% 96.64/97.28 cnf(710,plain,
% 96.64/97.28 (P1(x7101,f48(a84,a84))),
% 96.64/97.28 inference(rename_variables,[],[654])).
% 96.64/97.28 cnf(713,plain,
% 96.64/97.28 (~P1(x7131,f48(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[645])).
% 96.64/97.28 cnf(716,plain,
% 96.64/97.28 (~P1(x7161,f48(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[645])).
% 96.64/97.28 cnf(719,plain,
% 96.64/97.28 (~P1(x7191,f48(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[645])).
% 96.64/97.28 cnf(722,plain,
% 96.64/97.28 (P1(x7221,f48(a84,a84))),
% 96.64/97.28 inference(rename_variables,[],[654])).
% 96.64/97.28 cnf(725,plain,
% 96.64/97.28 (P1(x7251,f48(a84,a84))),
% 96.64/97.28 inference(rename_variables,[],[654])).
% 96.64/97.28 cnf(727,plain,
% 96.64/97.28 (~P6(x7271,f48(a84,a84),a89)),
% 96.64/97.28 inference(scs_inference,[],[645,656,659,662,665,671,674,677,680,683,686,692,695,698,704,707,713,716,654,668,689,701,710,722,725,24,63,64,53,85,26,55,58,66,61,21,84,56,57,60,86,62,25,42,59,65,54,83,82,87])).
% 96.64/97.28 cnf(728,plain,
% 96.64/97.28 (P1(x7281,f48(a84,a84))),
% 96.64/97.28 inference(rename_variables,[],[654])).
% 96.64/97.28 cnf(730,plain,
% 96.64/97.28 (P6(a58,f48(a5,a5),a8)),
% 96.64/97.28 inference(scs_inference,[],[14,645,656,659,662,665,671,674,677,680,683,686,692,695,698,704,707,713,716,719,654,668,689,701,710,722,725,24,63,64,53,85,26,55,58,66,61,21,84,56,57,60,86,62,25,42,59,65,54,83,82,87,76])).
% 96.64/97.28 cnf(732,plain,
% 96.64/97.28 (~P1(x7321,f48(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[645])).
% 96.64/97.28 cnf(735,plain,
% 96.64/97.28 (~P1(x7351,f48(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[645])).
% 96.64/97.28 cnf(736,plain,
% 96.64/97.28 (P1(x7361,a3)),
% 96.64/97.28 inference(rename_variables,[],[8])).
% 96.64/97.28 cnf(742,plain,
% 96.64/97.28 (P1(x7421,f48(a84,a84))),
% 96.64/97.28 inference(rename_variables,[],[654])).
% 96.64/97.28 cnf(745,plain,
% 96.64/97.28 (~P5(a78,a78)),
% 96.64/97.28 inference(scs_inference,[],[6,122,8,14,645,656,659,662,665,671,674,677,680,683,686,692,695,698,704,707,713,716,719,732,735,654,668,689,701,710,722,725,728,584,24,63,64,53,85,26,55,58,66,61,21,84,56,57,60,86,62,25,42,59,65,54,83,82,87,76,93,81,101,104])).
% 96.64/97.28 cnf(746,plain,
% 96.64/97.28 (P6(x7461,a3,a78)),
% 96.64/97.28 inference(rename_variables,[],[122])).
% 96.64/97.28 cnf(752,plain,
% 96.64/97.28 (P3(a78,a78)),
% 96.64/97.28 inference(scs_inference,[],[6,122,8,736,14,645,656,659,662,665,671,674,677,680,683,686,692,695,698,704,707,713,716,719,732,735,654,668,689,701,710,722,725,728,742,584,24,63,64,53,85,26,55,58,66,61,21,84,56,57,60,86,62,25,42,59,65,54,83,82,87,76,93,81,101,104,98,100])).
% 96.64/97.28 cnf(758,plain,
% 96.64/97.28 (P4(a78,a10)),
% 96.64/97.28 inference(scs_inference,[],[6,122,746,8,736,14,645,656,659,662,665,671,674,677,680,683,686,692,695,698,704,707,713,716,719,732,735,654,668,689,701,710,722,725,728,742,602,584,24,63,64,53,85,26,55,58,66,61,21,84,56,57,60,86,62,25,42,59,65,54,83,82,87,76,93,81,101,104,98,100,105,75,91])).
% 96.64/97.28 cnf(783,plain,
% 96.64/97.28 (P6(f45(a5,a5),f46(a5,a5),a5)),
% 96.64/97.28 inference(scs_inference,[],[110,69,100])).
% 96.64/97.28 cnf(784,plain,
% 96.64/97.28 (~P1(x7841,f45(a5,a5))),
% 96.64/97.28 inference(scs_inference,[],[783,36])).
% 96.64/97.28 cnf(796,plain,
% 96.64/97.28 (~P5(a8,a8)),
% 96.64/97.28 inference(scs_inference,[],[783,730,8,14,645,654,36,24,76,98,104])).
% 96.64/97.28 cnf(798,plain,
% 96.64/97.28 (P3(a8,a8)),
% 96.64/97.28 inference(scs_inference,[],[783,730,8,14,645,654,36,24,76,98,104,100])).
% 96.64/97.28 cnf(823,plain,
% 96.64/97.28 (~P1(x8231,f45(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[784])).
% 96.64/97.28 cnf(826,plain,
% 96.64/97.28 (~P1(x8261,f45(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[784])).
% 96.64/97.28 cnf(829,plain,
% 96.64/97.28 (~P1(x8291,f45(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[784])).
% 96.64/97.28 cnf(831,plain,
% 96.64/97.28 (~P6(f45(a5,a5),x8311,a10)),
% 96.64/97.28 inference(scs_inference,[],[784,823,826,829,68,63,53,55])).
% 96.64/97.28 cnf(832,plain,
% 96.64/97.28 (~P1(x8321,f45(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[784])).
% 96.64/97.28 cnf(835,plain,
% 96.64/97.28 (~P1(x8351,f45(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[784])).
% 96.64/97.28 cnf(838,plain,
% 96.64/97.28 (~P1(x8381,f45(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[784])).
% 96.64/97.28 cnf(841,plain,
% 96.64/97.28 (~P1(x8411,f45(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[784])).
% 96.64/97.28 cnf(844,plain,
% 96.64/97.28 (~P1(x8441,f45(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[784])).
% 96.64/97.28 cnf(847,plain,
% 96.64/97.28 (~P1(x8471,f45(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[784])).
% 96.64/97.28 cnf(850,plain,
% 96.64/97.28 (~P1(x8501,f45(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[784])).
% 96.64/97.28 cnf(853,plain,
% 96.64/97.28 (~P1(x8531,f45(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[784])).
% 96.64/97.28 cnf(856,plain,
% 96.64/97.28 (~P1(x8561,f45(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[784])).
% 96.64/97.28 cnf(859,plain,
% 96.64/97.28 (~P1(x8591,f45(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[784])).
% 96.64/97.28 cnf(862,plain,
% 96.64/97.28 (~P1(x8621,f45(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[784])).
% 96.64/97.28 cnf(865,plain,
% 96.64/97.28 (~P1(x8651,f45(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[784])).
% 96.64/97.28 cnf(868,plain,
% 96.64/97.28 (~P1(x8681,f45(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[784])).
% 96.64/97.28 cnf(870,plain,
% 96.64/97.28 (~P6(f45(a5,a5),x8701,a81)),
% 96.64/97.28 inference(scs_inference,[],[784,823,826,829,832,835,838,841,844,847,850,853,856,859,862,865,868,68,63,53,55,66,62,65,25,64,61,26,60,21,57,59,58,56])).
% 96.64/97.28 cnf(871,plain,
% 96.64/97.28 (~P1(x8711,f45(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[784])).
% 96.64/97.28 cnf(874,plain,
% 96.64/97.28 (~P1(x8741,f45(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[784])).
% 96.64/97.28 cnf(878,plain,
% 96.64/97.28 (~P1(x8781,f45(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[784])).
% 96.64/97.28 cnf(881,plain,
% 96.64/97.28 (~P1(x8811,f45(a5,a5))),
% 96.64/97.28 inference(rename_variables,[],[784])).
% 96.64/97.28 cnf(887,plain,
% 96.64/97.28 (~P5(a78,a80)),
% 96.64/97.28 inference(scs_inference,[],[6,122,8,14,784,823,826,829,832,835,838,841,844,847,850,853,856,859,862,865,868,871,874,878,881,68,63,53,55,66,62,65,25,64,61,26,60,21,57,59,58,56,54,76,93,81,104])).
% 96.64/97.28 cnf(892,plain,
% 96.64/97.28 (P3(a80,a80)),
% 96.64/97.28 inference(scs_inference,[],[6,122,8,14,784,823,826,829,832,835,838,841,844,847,850,853,856,859,862,865,868,871,874,878,881,68,63,53,55,66,62,65,25,64,61,26,60,21,57,59,58,56,54,76,93,81,104,105,100])).
% 96.64/97.28 cnf(917,plain,
% 96.64/97.28 (P1(x9171,f79(f46(a88,a88)))),
% 96.64/97.28 inference(scs_inference,[],[624,70,35])).
% 96.64/97.28 cnf(918,plain,
% 96.64/97.28 (~P1(x9181,f46(a88,a88))),
% 96.64/97.28 inference(scs_inference,[],[917,20])).
% 96.64/97.28 cnf(929,plain,
% 96.64/97.28 (~P1(x9291,f46(a88,a88))),
% 96.64/97.28 inference(rename_variables,[],[918])).
% 96.64/97.28 cnf(932,plain,
% 96.64/97.28 (~P1(x9321,f46(a88,a88))),
% 96.64/97.28 inference(rename_variables,[],[918])).
% 96.64/97.28 cnf(935,plain,
% 96.64/97.28 (~P1(x9351,f46(a88,a88))),
% 96.64/97.28 inference(rename_variables,[],[918])).
% 96.64/97.28 cnf(938,plain,
% 96.64/97.28 (~P1(x9381,f46(a88,a88))),
% 96.64/97.28 inference(rename_variables,[],[918])).
% 96.64/97.28 cnf(941,plain,
% 96.64/97.28 (~P1(x9411,f46(a88,a88))),
% 96.64/97.28 inference(rename_variables,[],[918])).
% 96.64/97.28 cnf(944,plain,
% 96.64/97.28 (~P1(x9441,f46(a88,a88))),
% 96.64/97.28 inference(rename_variables,[],[918])).
% 96.64/97.28 cnf(947,plain,
% 96.64/97.28 (~P1(x9471,f46(a88,a88))),
% 96.64/97.28 inference(rename_variables,[],[918])).
% 96.64/97.28 cnf(950,plain,
% 96.64/97.28 (~P1(x9501,f46(a88,a88))),
% 96.64/97.28 inference(rename_variables,[],[918])).
% 96.64/97.28 cnf(953,plain,
% 96.64/97.28 (~P1(x9531,f46(a88,a88))),
% 96.64/97.28 inference(rename_variables,[],[918])).
% 96.64/97.28 cnf(956,plain,
% 96.64/97.28 (~P1(x9561,f46(a88,a88))),
% 96.64/97.28 inference(rename_variables,[],[918])).
% 96.64/97.28 cnf(959,plain,
% 96.64/97.28 (~P1(x9591,f46(a88,a88))),
% 96.64/97.28 inference(rename_variables,[],[918])).
% 96.64/97.28 cnf(962,plain,
% 96.64/97.28 (~P1(x9621,f46(a88,a88))),
% 96.64/97.28 inference(rename_variables,[],[918])).
% 96.64/97.28 cnf(965,plain,
% 96.64/97.28 (~P1(x9651,f46(a88,a88))),
% 96.64/97.28 inference(rename_variables,[],[918])).
% 96.64/97.29 cnf(968,plain,
% 96.64/97.29 (~P1(x9681,f46(a88,a88))),
% 96.64/97.29 inference(rename_variables,[],[918])).
% 96.64/97.29 cnf(971,plain,
% 96.64/97.29 (~P1(x9711,f46(a88,a88))),
% 96.64/97.29 inference(rename_variables,[],[918])).
% 96.64/97.29 cnf(974,plain,
% 96.64/97.29 (~P1(x9741,f46(a88,a88))),
% 96.64/97.29 inference(rename_variables,[],[918])).
% 96.64/97.29 cnf(977,plain,
% 96.64/97.29 (~P1(x9771,f46(a88,a88))),
% 96.64/97.29 inference(rename_variables,[],[918])).
% 96.64/97.29 cnf(980,plain,
% 96.64/97.29 (~P1(x9801,f46(a88,a88))),
% 96.64/97.29 inference(rename_variables,[],[918])).
% 96.64/97.29 cnf(983,plain,
% 96.64/97.29 (~P1(x9831,f46(a88,a88))),
% 96.64/97.29 inference(rename_variables,[],[918])).
% 96.64/97.29 cnf(987,plain,
% 96.64/97.29 (~P1(x9871,f46(a88,a88))),
% 96.64/97.29 inference(rename_variables,[],[918])).
% 96.64/97.29 cnf(997,plain,
% 96.64/97.29 (~P5(a78,a5)),
% 96.64/97.29 inference(scs_inference,[],[6,122,8,14,584,918,929,932,935,938,941,944,947,950,953,956,959,962,965,968,971,974,977,980,983,987,917,63,24,55,65,64,53,60,66,56,62,61,26,59,54,25,57,21,58,93,80,101,76,104])).
% 96.64/97.29 cnf(998,plain,
% 96.64/97.29 (P6(x9981,a3,a78)),
% 96.64/97.29 inference(rename_variables,[],[122])).
% 96.64/97.29 cnf(1000,plain,
% 96.64/97.29 (P3(a78,a80)),
% 96.64/97.29 inference(scs_inference,[],[6,122,998,8,14,584,918,929,932,935,938,941,944,947,950,953,956,959,962,965,968,971,974,977,980,983,987,917,63,24,55,65,64,53,60,66,56,62,61,26,59,54,25,57,21,58,93,80,101,76,104,100])).
% 96.64/97.29 cnf(1102,plain,
% 96.64/97.29 (~P2(x11021,a88)+~P6(f49(x11022,a88),f50(x11022,a88),x11021)+~P6(a3,a65,x11022)),
% 96.64/97.29 inference(scs_inference,[],[567,94])).
% 96.64/97.29 cnf(1106,plain,
% 96.64/97.29 (~P5(a86,a86)),
% 96.64/97.29 inference(scs_inference,[],[113,104])).
% 96.64/97.29 cnf(1108,plain,
% 96.64/97.29 (P3(a86,a86)),
% 96.64/97.29 inference(scs_inference,[],[113,104,100])).
% 96.64/97.29 cnf(1117,plain,
% 96.64/97.29 (~P5(a86,a5)),
% 96.64/97.29 inference(scs_inference,[],[113,110,104])).
% 96.64/97.29 cnf(1118,plain,
% 96.64/97.29 (P6(a58,x11181,a5)),
% 96.64/97.29 inference(rename_variables,[],[110])).
% 96.64/97.29 cnf(1119,plain,
% 96.64/97.29 (P6(x11191,a58,a86)),
% 96.64/97.29 inference(rename_variables,[],[113])).
% 96.64/97.29 cnf(1121,plain,
% 96.64/97.29 (P3(a86,a5)),
% 96.64/97.29 inference(scs_inference,[],[113,1119,110,1118,104,100])).
% 96.64/97.29 cnf(1133,plain,
% 96.64/97.29 (P3(a86,a78)),
% 96.64/97.29 inference(scs_inference,[],[113,119,100])).
% 96.64/97.29 cnf(1134,plain,
% 96.64/97.29 (P6(a58,x11341,a78)),
% 96.64/97.29 inference(rename_variables,[],[119])).
% 96.64/97.29 cnf(1135,plain,
% 96.64/97.29 (P6(x11351,a58,a86)),
% 96.64/97.29 inference(rename_variables,[],[113])).
% 96.64/97.29 cnf(1137,plain,
% 96.64/97.29 (~P5(a86,a78)),
% 96.64/97.29 inference(scs_inference,[],[113,1135,119,1134,100,104])).
% 96.64/97.29 cnf(1149,plain,
% 96.64/97.29 (~P5(a86,a80)),
% 96.64/97.29 inference(scs_inference,[],[113,116,104])).
% 96.64/97.29 cnf(1150,plain,
% 96.64/97.29 (P6(a58,x11501,a80)),
% 96.64/97.29 inference(rename_variables,[],[116])).
% 96.64/97.29 cnf(1151,plain,
% 96.64/97.29 (P6(x11511,a58,a86)),
% 96.64/97.29 inference(rename_variables,[],[113])).
% 96.64/97.29 cnf(1153,plain,
% 96.64/97.29 (P3(a86,a80)),
% 96.64/97.29 inference(scs_inference,[],[113,1151,116,1150,104,100])).
% 96.64/97.29 cnf(1154,plain,
% 96.64/97.29 (P6(a58,x11541,a80)),
% 96.64/97.29 inference(rename_variables,[],[116])).
% 96.64/97.29 cnf(1155,plain,
% 96.64/97.29 (P6(x11551,a58,a86)),
% 96.64/97.29 inference(rename_variables,[],[113])).
% 96.64/97.29 cnf(1159,plain,
% 96.64/97.29 (P6(x11591,a58,a86)),
% 96.64/97.29 inference(rename_variables,[],[113])).
% 96.64/97.29 cnf(1161,plain,
% 96.64/97.29 (P4(a86,a10)),
% 96.64/97.29 inference(scs_inference,[],[113,1151,1155,1159,116,1150,1154,831,104,100,105,91])).
% 96.64/97.29 cnf(1198,plain,
% 96.64/97.29 (P3(a80,a5)),
% 96.64/97.29 inference(scs_inference,[],[116,110,100])).
% 96.64/97.29 cnf(1201,plain,
% 96.64/97.29 (~P5(a80,a80)),
% 96.64/97.29 inference(scs_inference,[],[116,110,100,104])).
% 96.64/97.29 cnf(1210,plain,
% 96.64/97.29 (~P5(a80,a5)),
% 96.64/97.29 inference(scs_inference,[],[116,110,104])).
% 96.64/97.29 cnf(1213,plain,
% 96.64/97.29 (P3(a80,a78)),
% 96.64/97.29 inference(scs_inference,[],[116,110,122,104,100])).
% 96.64/97.29 cnf(1214,plain,
% 96.64/97.29 (P6(x12141,a3,a78)),
% 96.64/97.29 inference(rename_variables,[],[122])).
% 96.64/97.29 cnf(1215,plain,
% 96.64/97.29 (P6(a58,x12151,a80)),
% 96.64/97.29 inference(rename_variables,[],[116])).
% 96.64/97.29 cnf(1219,plain,
% 96.64/97.29 (P6(a58,x12191,a80)),
% 96.64/97.29 inference(rename_variables,[],[116])).
% 96.64/97.29 cnf(1221,plain,
% 96.64/97.29 (P4(a80,a8)),
% 96.64/97.29 inference(scs_inference,[],[116,1215,1219,110,122,1214,201,104,100,105,91])).
% 96.64/97.29 cnf(1225,plain,
% 96.64/97.29 (P3(a80,a86)),
% 96.64/97.29 inference(scs_inference,[],[116,113,100])).
% 96.64/97.29 cnf(1226,plain,
% 96.64/97.29 (P6(x12261,a58,a86)),
% 96.64/97.29 inference(rename_variables,[],[113])).
% 96.64/97.29 cnf(1227,plain,
% 96.64/97.29 (P6(a58,x12271,a80)),
% 96.64/97.29 inference(rename_variables,[],[116])).
% 96.64/97.29 cnf(1229,plain,
% 96.64/97.29 (~P5(a80,a78)),
% 96.64/97.29 inference(scs_inference,[],[116,1227,122,113,100,104])).
% 96.64/97.29 cnf(1231,plain,
% 96.64/97.29 (P6(a58,x12311,a80)),
% 96.64/97.29 inference(rename_variables,[],[116])).
% 96.64/97.29 cnf(1235,plain,
% 96.64/97.29 (P6(a58,x12351,a80)),
% 96.64/97.29 inference(rename_variables,[],[116])).
% 96.64/97.29 cnf(1237,plain,
% 96.64/97.29 (P4(a80,a88)),
% 96.64/97.29 inference(scs_inference,[],[116,1227,1231,1235,122,113,1226,452,100,104,105,91])).
% 96.64/97.29 cnf(1242,plain,
% 96.64/97.29 (~P5(a80,a86)),
% 96.64/97.29 inference(scs_inference,[],[116,113,104])).
% 96.64/97.29 cnf(1251,plain,
% 96.64/97.29 (P4(a80,a89)),
% 96.64/97.29 inference(scs_inference,[],[116,727,91])).
% 96.64/97.29 cnf(1273,plain,
% 96.64/97.29 (P6(a65,a3,a82)),
% 96.64/97.29 inference(scs_inference,[],[8,4,34,15])).
% 96.64/97.29 cnf(1274,plain,
% 96.64/97.29 (P3(a82,a82)),
% 96.64/97.29 inference(scs_inference,[],[1273,100])).
% 96.64/97.29 cnf(1276,plain,
% 96.64/97.29 (~P5(a82,a82)),
% 96.64/97.29 inference(scs_inference,[],[1273,100,104])).
% 96.64/97.29 cnf(1292,plain,
% 96.64/97.29 (~P6(x12921,a58,a74)+P6(x12921,x12922,a5)),
% 96.64/97.29 inference(scs_inference,[],[14,48,21])).
% 96.64/97.29 cnf(1296,plain,
% 96.64/97.29 (P2(x12961,a5)+~P6(f41(x12961,a5),a58,a74)),
% 96.64/97.29 inference(scs_inference,[],[1292,99])).
% 96.64/97.29 cnf(1329,plain,
% 96.64/97.29 (~P2(a86,a74)+P2(x13291,a5)),
% 96.64/97.29 inference(scs_inference,[],[113,1296,94])).
% 96.64/97.29 cnf(1333,plain,
% 96.64/97.29 (P3(a78,a5)),
% 96.64/97.29 inference(scs_inference,[],[119,110,100])).
% 96.64/97.29 cnf(1360,plain,
% 96.64/97.29 (~P6(x13601,f45(a5,a5),a81)),
% 96.64/97.29 inference(scs_inference,[],[870,8,77,27])).
% 96.64/97.29 cnf(1370,plain,
% 96.64/97.29 (~P6(x13701,a58,a85)),
% 96.64/97.29 inference(scs_inference,[],[116,14,79,30])).
% 96.64/97.29 cnf(1432,plain,
% 96.64/97.29 (P6(x14321,a65,a80)),
% 96.64/97.29 inference(scs_inference,[],[4,15,22])).
% 96.64/97.29 cnf(1434,plain,
% 96.64/97.29 (P6(x14341,a65,a80)),
% 96.64/97.29 inference(rename_variables,[],[1432])).
% 96.64/97.29 cnf(1440,plain,
% 96.64/97.29 (~P6(f49(a80,a88),f50(a80,a88),x14401)+~P2(x14401,a88)),
% 96.64/97.29 inference(scs_inference,[],[133,1432,1434,1370,567,75,1102])).
% 96.64/97.29 cnf(1473,plain,
% 96.64/97.29 (~P2(a80,a88)),
% 96.64/97.29 inference(scs_inference,[],[1237,1440,71])).
% 96.64/97.29 cnf(1547,plain,
% 96.64/97.29 (P1(a68,f79(a62))),
% 96.64/97.29 inference(scs_inference,[],[11,15,17])).
% 96.64/97.29 cnf(1551,plain,
% 96.64/97.29 (~P6(a65,x15511,a5)),
% 96.64/97.29 inference(scs_inference,[],[4,15,36])).
% 96.64/97.29 cnf(1559,plain,
% 96.64/97.29 (~P6(x15591,a62,a81)),
% 96.64/97.29 inference(scs_inference,[],[11,15,27])).
% 96.64/97.29 cnf(1563,plain,
% 96.64/97.29 (~P6(a65,x15631,a83)),
% 96.64/97.29 inference(scs_inference,[],[4,15,37])).
% 96.64/97.29 cnf(1568,plain,
% 96.64/97.29 (~P6(x15681,a62,a84)),
% 96.64/97.29 inference(scs_inference,[],[11,15,28])).
% 96.64/97.29 cnf(1569,plain,
% 96.64/97.29 (~P1(f24(a3,a62),a62)),
% 96.64/97.29 inference(scs_inference,[],[1568,254])).
% 96.64/97.29 cnf(1576,plain,
% 96.64/97.29 (~P6(a65,x15761,a85)),
% 96.64/97.29 inference(scs_inference,[],[4,15,38])).
% 96.64/97.29 cnf(1585,plain,
% 96.64/97.29 (~P6(x15851,a62,a87)),
% 96.64/97.29 inference(scs_inference,[],[11,15,29])).
% 96.64/97.29 cnf(1586,plain,
% 96.64/97.29 (~P6(a65,x15861,a89)),
% 96.64/97.29 inference(scs_inference,[],[4,15,39])).
% 96.64/97.29 cnf(1595,plain,
% 96.64/97.29 (P6(a65,a58,a9)),
% 96.64/97.29 inference(scs_inference,[],[4,584,15,40])).
% 96.64/97.29 cnf(1596,plain,
% 96.64/97.29 (~P5(a9,a9)),
% 96.64/97.29 inference(scs_inference,[],[1595,104])).
% 96.64/97.29 cnf(1600,plain,
% 96.64/97.29 (P3(a9,a9)),
% 96.64/97.29 inference(scs_inference,[],[1595,104,105,100])).
% 96.64/97.29 cnf(1606,plain,
% 96.64/97.29 (~P6(a62,x16061,a84)),
% 96.64/97.29 inference(scs_inference,[],[11,15,31])).
% 96.64/97.29 cnf(1615,plain,
% 96.64/97.29 (P6(a58,a65,a83)),
% 96.64/97.29 inference(scs_inference,[],[4,14,15,41])).
% 96.64/97.29 cnf(1616,plain,
% 96.64/97.29 (~P5(a83,a83)),
% 96.64/97.29 inference(scs_inference,[],[1615,104])).
% 96.64/97.29 cnf(1618,plain,
% 96.64/97.29 (P3(a83,a83)),
% 96.64/97.29 inference(scs_inference,[],[1615,104,100])).
% 96.64/97.29 cnf(1626,plain,
% 96.64/97.29 (~P6(a62,x16261,a88)),
% 96.64/97.29 inference(scs_inference,[],[11,15,32])).
% 96.64/97.29 cnf(1636,plain,
% 96.64/97.29 (~P6(a62,a3,a10)),
% 96.64/97.29 inference(scs_inference,[],[11,8,15,44])).
% 96.64/97.29 cnf(1644,plain,
% 96.64/97.29 (~P6(a62,a3,a74)),
% 96.64/97.29 inference(scs_inference,[],[11,8,15,45])).
% 96.64/97.29 cnf(1648,plain,
% 96.64/97.29 (P6(a65,a3,a81)),
% 96.64/97.29 inference(scs_inference,[],[4,8,15,77])).
% 96.64/97.29 cnf(1649,plain,
% 96.64/97.29 (~P5(a81,a81)),
% 96.64/97.29 inference(scs_inference,[],[1648,104])).
% 96.64/97.29 cnf(1651,plain,
% 96.64/97.29 (P3(a81,a81)),
% 96.64/97.29 inference(scs_inference,[],[1648,104,100])).
% 96.64/97.29 cnf(1656,plain,
% 96.64/97.29 (P1(f60(a62,a58),a65)),
% 96.64/97.29 inference(scs_inference,[],[14,571,15,76])).
% 96.64/97.29 cnf(1661,plain,
% 96.64/97.29 (~P6(a58,a65,a86)),
% 96.64/97.29 inference(scs_inference,[],[4,14,15,78])).
% 96.64/97.29 cnf(1669,plain,
% 96.64/97.29 (~P6(a3,a62,a10)),
% 96.64/97.29 inference(scs_inference,[],[11,8,15,46])).
% 96.64/97.29 cnf(1717,plain,
% 96.64/97.29 (~P6(a65,a58,a80)),
% 96.64/97.29 inference(scs_inference,[],[4,14,15,79])).
% 96.64/97.29 cnf(1730,plain,
% 96.64/97.29 (P6(a58,a65,a89)),
% 96.64/97.29 inference(scs_inference,[],[4,14,11,15,74])).
% 96.64/97.29 cnf(1731,plain,
% 96.64/97.29 (~P5(a89,a89)),
% 96.64/97.29 inference(scs_inference,[],[1730,104])).
% 96.64/97.29 cnf(1735,plain,
% 96.64/97.29 (P3(a89,a89)),
% 96.64/97.29 inference(scs_inference,[],[1730,104,105,100])).
% 96.64/97.29 cnf(1741,plain,
% 96.64/97.29 (P6(a62,a3,a87)),
% 96.64/97.29 inference(scs_inference,[],[11,8,4,15,90])).
% 96.64/97.29 cnf(1742,plain,
% 96.64/97.29 (~P5(a87,a87)),
% 96.64/97.29 inference(scs_inference,[],[1741,104])).
% 96.64/97.29 cnf(1744,plain,
% 96.64/97.29 (P3(a87,a87)),
% 96.64/97.29 inference(scs_inference,[],[1741,104,100])).
% 96.64/97.29 cnf(1750,plain,
% 96.64/97.29 (~P1(f39(a58,a65),a62)),
% 96.64/97.29 inference(scs_inference,[],[1730,15,87])).
% 96.64/97.29 cnf(1768,plain,
% 96.64/97.29 (P6(a58,a62,a89)),
% 96.64/97.29 inference(scs_inference,[],[11,14,4,15,74])).
% 96.64/97.29 cnf(1773,plain,
% 96.64/97.29 (P6(a65,a3,a87)),
% 96.64/97.29 inference(scs_inference,[],[4,8,11,15,90])).
% 96.64/97.29 cnf(1778,plain,
% 96.64/97.29 (P1(f34(a58,a62),a65)),
% 96.64/97.29 inference(scs_inference,[],[1768,15,64])).
% 96.64/97.29 cnf(1782,plain,
% 96.64/97.29 (~P1(f26(a65,a3),a62)),
% 96.64/97.29 inference(scs_inference,[],[1773,15,84])).
% 96.64/97.29 cnf(1786,plain,
% 96.64/97.29 (~P1(f19(a62,a3),a62)),
% 96.64/97.29 inference(scs_inference,[],[11,8,1644,4,15,107])).
% 96.64/97.29 cnf(1831,plain,
% 96.64/97.29 (P6(a65,a3,a74)+~P1(f19(a65,a3),a62)),
% 96.64/97.29 inference(scs_inference,[],[8,11,15,107])).
% 96.64/97.29 cnf(1835,plain,
% 96.64/97.29 (~P1(f19(a65,a3),a62)),
% 96.64/97.29 inference(scs_inference,[],[11,8,1831,45])).
% 96.64/97.29 cnf(1842,plain,
% 96.64/97.29 (~P6(a59,a3,a10)+~P1(a63,a56)),
% 96.64/97.29 inference(scs_inference,[],[8,18,44])).
% 96.64/97.29 cnf(1847,plain,
% 96.64/97.29 (~P2(a78,a10)+~P1(a63,a56)),
% 96.64/97.29 inference(scs_inference,[],[122,1842,94])).
% 96.64/97.29 cnf(1861,plain,
% 96.64/97.29 (~P6(a56,a3,a74)+~P1(a64,a59)),
% 96.64/97.29 inference(scs_inference,[],[8,18,45])).
% 96.64/97.29 cnf(1866,plain,
% 96.64/97.29 (~P2(a78,a74)+~P1(a64,a59)),
% 96.64/97.29 inference(scs_inference,[],[122,1861,94])).
% 96.64/97.29 cnf(2849,plain,
% 96.64/97.29 (P3(a85,a5)),
% 96.64/97.29 inference(scs_inference,[],[194,110,100])).
% 96.64/97.29 cnf(2850,plain,
% 96.64/97.29 (P6(a58,x28501,a5)),
% 96.64/97.29 inference(rename_variables,[],[110])).
% 96.64/97.29 cnf(2852,plain,
% 96.64/97.29 (~P5(a85,a5)),
% 96.64/97.29 inference(scs_inference,[],[194,110,2850,100,104])).
% 96.64/97.29 cnf(2863,plain,
% 96.64/97.29 (P3(a85,a78)),
% 96.64/97.29 inference(scs_inference,[],[194,122,100])).
% 96.64/97.29 cnf(2864,plain,
% 96.64/97.29 (P6(x28641,a3,a78)),
% 96.64/97.29 inference(rename_variables,[],[122])).
% 96.64/97.29 cnf(2866,plain,
% 96.64/97.29 (~P5(a85,a78)),
% 96.64/97.29 inference(scs_inference,[],[194,122,2864,100,104])).
% 96.64/97.29 cnf(2875,plain,
% 96.64/97.29 (P3(a85,a80)),
% 96.64/97.29 inference(scs_inference,[],[194,116,100])).
% 96.64/97.29 cnf(2876,plain,
% 96.64/97.29 (P6(a58,x28761,a80)),
% 96.64/97.29 inference(rename_variables,[],[116])).
% 96.64/97.29 cnf(2878,plain,
% 96.64/97.29 (~P5(a85,a80)),
% 96.64/97.29 inference(scs_inference,[],[194,116,2876,100,104])).
% 96.64/97.29 cnf(2933,plain,
% 96.64/97.29 (P3(a10,a78)),
% 96.64/97.29 inference(scs_inference,[],[210,122,100])).
% 96.64/97.29 cnf(2934,plain,
% 96.64/97.29 (P6(x29341,a3,a78)),
% 96.64/97.29 inference(rename_variables,[],[122])).
% 96.64/97.29 cnf(2936,plain,
% 96.64/97.29 (~P5(a10,a78)),
% 96.64/97.29 inference(scs_inference,[],[210,122,2934,100,104])).
% 96.64/97.29 cnf(2944,plain,
% 96.64/97.29 (P3(a84,a78)),
% 96.64/97.29 inference(scs_inference,[],[214,122,100])).
% 96.64/97.29 cnf(2945,plain,
% 96.64/97.29 (P6(x29451,a3,a78)),
% 96.64/97.29 inference(rename_variables,[],[122])).
% 96.64/97.29 cnf(2947,plain,
% 96.64/97.29 (~P5(a84,a78)),
% 96.64/97.29 inference(scs_inference,[],[214,122,2945,100,104])).
% 96.64/97.29 cnf(3176,plain,
% 96.64/97.29 (~P2(a86,a74)),
% 96.64/97.29 inference(scs_inference,[],[1551,1432,1329,94])).
% 96.64/97.29 cnf(3190,plain,
% 96.64/97.29 (~P2(a78,a10)+~P6(a56,a3,a10)),
% 96.64/97.29 inference(scs_inference,[],[8,1847,44])).
% 96.64/97.29 cnf(3191,plain,
% 96.64/97.29 (~P2(a78,a10)),
% 96.64/97.29 inference(scs_inference,[],[122,3190,94])).
% 96.64/97.29 cnf(3220,plain,
% 96.64/97.29 (P3(a88,a86)),
% 96.64/97.29 inference(scs_inference,[],[614,113,100])).
% 96.64/97.29 cnf(3221,plain,
% 96.64/97.29 (P6(x32211,a58,a86)),
% 96.64/97.29 inference(rename_variables,[],[113])).
% 96.64/97.29 cnf(3223,plain,
% 96.64/97.29 (~P5(a88,a86)),
% 96.64/97.29 inference(scs_inference,[],[614,113,3221,100,104])).
% 96.64/97.29 cnf(3243,plain,
% 96.64/97.29 (~P2(a78,a74)+~P6(a59,a3,a74)),
% 96.64/97.29 inference(scs_inference,[],[8,1866,45])).
% 96.64/97.29 cnf(3247,plain,
% 96.64/97.29 (~P2(a78,a74)),
% 96.64/97.29 inference(scs_inference,[],[122,3243,94])).
% 96.64/97.29 cnf(3693,plain,
% 96.64/97.29 (P1(x36931,f48(a84,a84))),
% 96.64/97.29 inference(rename_variables,[],[654])).
% 96.64/97.29 cnf(3698,plain,
% 96.64/97.29 (P6(f48(a5,a5),f48(a84,a84),a85)),
% 96.64/97.29 inference(scs_inference,[],[654,3693,645,918,584,98,80,93])).
% 96.64/97.29 cnf(3764,plain,
% 96.64/97.29 (P3(a8,a5)),
% 96.64/97.29 inference(scs_inference,[],[730,110,100])).
% 96.64/97.29 cnf(3765,plain,
% 96.64/97.29 (P6(a58,x37651,a5)),
% 96.64/97.29 inference(rename_variables,[],[110])).
% 96.64/97.29 cnf(3768,plain,
% 96.64/97.29 (P6(a58,x37681,a5)),
% 96.64/97.29 inference(rename_variables,[],[110])).
% 96.64/97.29 cnf(3770,plain,
% 96.64/97.29 (~P5(a8,a5)),
% 96.64/97.29 inference(scs_inference,[],[730,110,3765,3768,100,105,104])).
% 96.64/97.29 cnf(3777,plain,
% 96.64/97.29 (P3(a8,a78)),
% 96.64/97.29 inference(scs_inference,[],[730,119,100])).
% 96.64/97.29 cnf(3778,plain,
% 96.64/97.29 (P6(a58,x37781,a78)),
% 96.64/97.29 inference(rename_variables,[],[119])).
% 96.64/97.29 cnf(3781,plain,
% 96.64/97.29 (P6(a58,x37811,a78)),
% 96.64/97.29 inference(rename_variables,[],[119])).
% 96.64/97.29 cnf(3783,plain,
% 96.64/97.29 (~P5(a8,a78)),
% 96.64/97.29 inference(scs_inference,[],[730,119,3778,3781,100,105,104])).
% 96.64/97.29 cnf(3790,plain,
% 96.64/97.29 (P3(a8,a80)),
% 96.64/97.29 inference(scs_inference,[],[730,116,100])).
% 96.64/97.29 cnf(3791,plain,
% 96.64/97.29 (P6(a58,x37911,a80)),
% 96.64/97.29 inference(rename_variables,[],[116])).
% 96.64/97.29 cnf(3794,plain,
% 96.64/97.29 (P6(a58,x37941,a80)),
% 96.64/97.29 inference(rename_variables,[],[116])).
% 96.64/97.29 cnf(3796,plain,
% 96.64/97.29 (~P5(a8,a80)),
% 96.64/97.29 inference(scs_inference,[],[730,116,3791,3794,100,105,104])).
% 96.64/97.29 cnf(3802,plain,
% 96.64/97.29 (P3(a8,a86)),
% 96.64/97.29 inference(scs_inference,[],[730,655,100])).
% 96.64/97.29 cnf(3803,plain,
% 96.64/97.29 (P6(x38031,f48(a5,a5),a86)),
% 96.64/97.29 inference(rename_variables,[],[655])).
% 96.64/97.29 cnf(3805,plain,
% 96.64/97.29 (~P5(a8,a86)),
% 96.64/97.29 inference(scs_inference,[],[730,655,3803,100,104])).
% 96.64/97.29 cnf(3852,plain,
% 96.64/97.29 (P6(f46(a88,a88),f45(a5,a5),a8)),
% 96.64/97.29 inference(scs_inference,[],[784,918,76])).
% 96.64/97.29 cnf(3999,plain,
% 96.64/97.29 (~P6(x39991,a71,a81)),
% 96.64/97.29 inference(scs_inference,[],[190,242,250,3191,12,50,51,52,69,70,99,102,27])).
% 96.64/97.29 cnf(4003,plain,
% 96.64/97.29 (~P6(x40031,a71,a87)),
% 96.64/97.29 inference(scs_inference,[],[190,242,250,3191,12,1547,50,51,52,69,70,99,102,27,37,29])).
% 96.64/97.29 cnf(4007,plain,
% 96.64/97.29 (~P6(a71,x40071,a88)),
% 96.64/97.29 inference(scs_inference,[],[190,242,250,3191,12,1547,50,51,52,69,70,99,102,27,37,29,39,32])).
% 96.64/97.29 cnf(4017,plain,
% 96.64/97.29 (~P1(f60(a62,a58),f79(a65))),
% 96.64/97.29 inference(scs_inference,[],[190,242,250,3191,12,1656,1547,1615,50,51,52,69,70,99,102,27,37,29,39,32,38,71,30,63,20])).
% 96.64/97.29 cnf(4019,plain,
% 96.64/97.29 (~P6(a71,x40191,a84)),
% 96.64/97.29 inference(scs_inference,[],[190,242,250,3191,12,1656,1547,1615,50,51,52,69,70,99,102,27,37,29,39,32,38,71,30,63,20,31])).
% 96.64/97.29 cnf(4023,plain,
% 96.64/97.29 (~P1(f26(a65,a3),a65)),
% 96.64/97.29 inference(scs_inference,[],[190,242,250,3191,12,1656,1547,1773,1615,50,51,52,69,70,99,102,27,37,29,39,32,38,71,30,63,20,31,23,84])).
% 96.64/97.29 cnf(4027,plain,
% 96.64/97.29 (P6(x40271,f79(a62),a80)),
% 96.64/97.29 inference(scs_inference,[],[190,242,250,3191,12,1656,1547,1661,1773,1615,50,51,52,69,70,99,102,27,37,29,39,32,38,71,30,63,20,31,23,84,24,22])).
% 96.64/97.29 cnf(4031,plain,
% 96.64/97.29 (~P6(x40311,a71,a84)),
% 96.64/97.29 inference(scs_inference,[],[190,242,250,3191,12,1656,1547,1661,1773,1615,50,51,52,69,70,99,102,27,37,29,39,32,38,71,30,63,20,31,23,84,24,22,36,28])).
% 96.64/97.29 cnf(4035,plain,
% 96.64/97.29 (P1(f34(a58,a62),a62)),
% 96.64/97.29 inference(scs_inference,[],[190,242,250,3191,12,1656,1547,1661,1768,1773,1648,1615,50,51,52,69,70,99,102,27,37,29,39,32,38,71,30,63,20,31,23,84,24,22,36,28,56,64])).
% 96.64/97.29 cnf(4037,plain,
% 96.64/97.29 (~P1(f39(a58,a62),a62)),
% 96.64/97.29 inference(scs_inference,[],[190,242,250,3191,12,1656,1547,1661,1768,1773,1648,1615,50,51,52,69,70,99,102,27,37,29,39,32,38,71,30,63,20,31,23,84,24,22,36,28,56,64,87])).
% 96.64/97.29 cnf(4045,plain,
% 96.64/97.29 (P1(a66,f79(a62))),
% 96.64/97.29 inference(scs_inference,[],[190,242,250,3191,10,12,1656,1547,1661,1768,1773,1273,1648,1595,1615,50,51,52,69,70,99,102,27,37,29,39,32,38,71,30,63,20,31,23,84,24,22,36,28,56,64,87,60,54,65,17])).
% 96.64/97.29 cnf(4053,plain,
% 96.64/97.29 (~P6(f79(a62),a62,a90)),
% 96.64/97.29 inference(scs_inference,[],[125,190,242,250,450,3191,10,12,1656,1547,1717,1661,1768,1773,1273,1648,449,1595,1615,1551,50,51,52,69,70,99,102,27,37,29,39,32,38,71,30,63,20,31,23,84,24,22,36,28,56,64,87,60,54,65,17,21,25,45,47])).
% 96.64/97.29 cnf(4059,plain,
% 96.64/97.29 (~P2(a8,a81)),
% 96.64/97.29 inference(scs_inference,[],[125,190,242,250,450,3191,10,12,1656,3852,1547,1360,1717,1661,1768,1773,1273,1648,449,1595,1615,1551,50,51,52,69,70,99,102,27,37,29,39,32,38,71,30,63,20,31,23,84,24,22,36,28,56,64,87,60,54,65,17,21,25,45,47,48,49,94])).
% 96.64/97.29 cnf(4062,plain,
% 96.64/97.29 (~P1(f14(a65,a62),a62)),
% 96.64/97.29 inference(scs_inference,[],[125,190,242,250,450,3191,10,12,1656,3852,1547,1559,1360,1717,1661,1768,1773,1273,1648,449,1595,1615,1551,50,51,52,69,70,99,102,27,37,29,39,32,38,71,30,63,20,31,23,84,24,22,36,28,56,64,87,60,54,65,17,21,25,45,47,48,49,94,77])).
% 96.64/97.29 cnf(4074,plain,
% 96.64/97.29 (P6(a65,a65,a8)),
% 96.64/97.29 inference(scs_inference,[],[125,190,242,250,450,3191,10,12,1656,3852,1547,1559,1360,1563,1717,1661,1768,1773,1273,1648,449,1595,1615,481,1432,1551,50,51,52,69,70,99,102,27,37,29,39,32,38,71,30,63,20,31,23,84,24,22,36,28,56,64,87,60,54,65,17,21,25,45,47,48,49,94,77,78,79,41,33])).
% 96.64/97.29 cnf(4082,plain,
% 96.64/97.29 (~P6(f79(a65),a65,a10)),
% 96.64/97.29 inference(scs_inference,[],[125,190,242,250,450,3191,10,12,1656,3852,1547,1559,1360,1563,1717,1661,1768,1773,1273,1648,449,1595,1615,481,1432,1551,50,51,52,69,70,99,102,27,37,29,39,32,38,71,30,63,20,31,23,84,24,22,36,28,56,64,87,60,54,65,17,21,25,45,47,48,49,94,77,78,79,41,33,34,43,46,44])).
% 96.64/97.29 cnf(4086,plain,
% 96.64/97.29 (P3(a78,a85)),
% 96.64/97.29 inference(scs_inference,[],[125,190,242,250,450,3191,10,12,1656,3852,1547,3698,1559,1360,670,1563,1717,1661,1768,1773,1273,1648,449,1595,1615,481,1432,1551,50,51,52,69,70,99,102,27,37,29,39,32,38,71,30,63,20,31,23,84,24,22,36,28,56,64,87,60,54,65,17,21,25,45,47,48,49,94,77,78,79,41,33,34,43,46,44,81,100])).
% 96.64/97.29 cnf(4087,plain,
% 96.64/97.29 (P6(f48(a5,a5),x40871,a78)),
% 96.64/97.29 inference(rename_variables,[],[670])).
% 96.64/97.29 cnf(4089,plain,
% 96.64/97.29 (~P1(f23(a62,a3),a62)),
% 96.64/97.29 inference(scs_inference,[],[125,190,242,250,450,3191,10,12,1656,3852,1547,3698,1559,1360,670,1563,1717,1661,1768,1773,1273,1648,449,1606,1595,1615,481,1432,1551,8,50,51,52,69,70,99,102,27,37,29,39,32,38,71,30,63,20,31,23,84,24,22,36,28,56,64,87,60,54,65,17,21,25,45,47,48,49,94,77,78,79,41,33,34,43,46,44,81,100,98])).
% 96.64/97.29 cnf(4090,plain,
% 96.64/97.29 (P1(x40901,a3)),
% 96.64/97.29 inference(rename_variables,[],[8])).
% 96.64/97.29 cnf(4093,plain,
% 96.64/97.29 (P1(f76(a65,a65),a65)),
% 96.64/97.29 inference(scs_inference,[],[125,190,242,250,450,3191,10,12,1656,3852,1547,3698,1559,1360,670,1563,1717,1661,1768,1773,1273,1648,449,1606,1595,1615,481,1432,1551,8,50,51,52,69,70,99,102,27,37,29,39,32,38,71,30,63,20,31,23,84,24,22,36,28,56,64,87,60,54,65,17,21,25,45,47,48,49,94,77,78,79,41,33,34,43,46,44,81,100,98,80])).
% 96.64/97.29 cnf(4095,plain,
% 96.64/97.29 (~P1(f40(a62,a58),a62)),
% 96.64/97.29 inference(scs_inference,[],[125,190,242,250,450,3191,10,12,1656,3852,1547,3698,1559,1360,670,1563,1626,1717,1661,1768,1773,1273,1648,449,1606,1595,1615,481,1432,1551,8,584,50,51,52,69,70,99,102,27,37,29,39,32,38,71,30,63,20,31,23,84,24,22,36,28,56,64,87,60,54,65,17,21,25,45,47,48,49,94,77,78,79,41,33,34,43,46,44,81,100,98,80,101])).
% 96.64/97.29 cnf(4099,plain,
% 96.64/97.29 (P1(f60(a56,a58),a56)),
% 96.64/97.29 inference(scs_inference,[],[125,190,242,250,450,3191,10,12,1656,3852,1547,3698,1559,1360,524,670,1563,1626,1717,1661,1768,1773,1273,1648,449,1606,1595,1615,481,1432,1551,14,8,584,50,51,52,69,70,99,102,27,37,29,39,32,38,71,30,63,20,31,23,84,24,22,36,28,56,64,87,60,54,65,17,21,25,45,47,48,49,94,77,78,79,41,33,34,43,46,44,81,100,98,80,101,76])).
% 96.64/97.29 cnf(4106,plain,
% 96.64/97.29 (P1(x41061,a3)),
% 96.64/97.29 inference(rename_variables,[],[8])).
% 96.64/97.29 cnf(4114,plain,
% 96.64/97.29 (~P1(f22(a65,a62),a62)),
% 96.64/97.29 inference(scs_inference,[],[13,125,190,242,250,450,3191,10,12,1656,3852,1547,3698,1559,1585,1360,524,670,4087,1563,1586,1626,1717,1661,1768,1773,1273,1648,449,1606,1595,1615,481,1576,1432,1551,14,11,8,4090,584,50,51,52,69,70,99,102,27,37,29,39,32,38,71,30,63,20,31,23,84,24,22,36,28,56,64,87,60,54,65,17,21,25,45,47,48,49,94,77,78,79,41,33,34,43,46,44,81,100,98,80,101,76,105,93,91,74,90])).
% 96.64/97.29 cnf(4117,plain,
% 96.64/97.29 (~P1(f12(a3,a62),a62)),
% 96.64/97.29 inference(scs_inference,[],[13,125,190,242,250,450,3191,10,12,1656,3852,1547,3698,1559,1585,1360,524,670,4087,1563,1586,1626,1717,1661,1768,1773,1669,1273,1648,449,1606,1595,1615,481,1576,1432,1551,14,11,8,4090,4106,584,50,51,52,69,70,99,102,27,37,29,39,32,38,71,30,63,20,31,23,84,24,22,36,28,56,64,87,60,54,65,17,21,25,45,47,48,49,94,77,78,79,41,33,34,43,46,44,81,100,98,80,101,76,105,93,91,74,90,106])).
% 96.64/97.29 cnf(4140,plain,
% 96.64/97.29 (~P6(a65,x41401,a88)),
% 96.64/97.29 inference(scs_inference,[],[4023,32])).
% 96.64/97.29 cnf(4148,plain,
% 96.64/97.29 (~P6(a62,x41481,a89)),
% 96.64/97.29 inference(scs_inference,[],[236,3247,4017,4023,4035,32,102,27,99,39])).
% 96.64/97.29 cnf(4150,plain,
% 96.64/97.29 (~P6(a62,x41501,a85)),
% 96.64/97.29 inference(scs_inference,[],[236,3247,4017,4023,4035,32,102,27,99,39,38])).
% 96.64/97.29 cnf(4158,plain,
% 96.64/97.29 (~P6(a62,x41581,a83)),
% 96.64/97.29 inference(scs_inference,[],[236,280,285,3247,4017,4023,4035,32,102,27,99,39,38,51,50,69,37])).
% 96.64/97.29 cnf(4168,plain,
% 96.64/97.29 (P6(a62,x41681,a86)),
% 96.64/97.29 inference(scs_inference,[],[236,280,285,289,295,3247,4017,4023,4035,32,102,27,99,39,38,51,50,69,37,52,70,29,71,23])).
% 96.64/97.29 cnf(4172,plain,
% 96.64/97.29 (P6(x41721,a62,a80)),
% 96.64/97.29 inference(scs_inference,[],[236,280,285,289,295,3247,4017,4023,4035,32,102,27,99,39,38,51,50,69,37,52,70,29,71,23,30,22])).
% 96.64/97.29 cnf(4176,plain,
% 96.64/97.29 (~P1(f34(a58,a62),f79(a62))),
% 96.64/97.29 inference(scs_inference,[],[236,280,285,289,295,3247,4017,4023,4035,32,102,27,99,39,38,51,50,69,37,52,70,29,71,23,30,22,31,20])).
% 96.64/97.29 cnf(4180,plain,
% 96.64/97.29 (~P1(f26(a62,a3),a62)),
% 96.64/97.29 inference(scs_inference,[],[236,280,285,289,295,3247,4017,4023,4035,1741,32,102,27,99,39,38,51,50,69,37,52,70,29,71,23,30,22,31,20,28,84])).
% 96.64/97.29 cnf(4184,plain,
% 96.64/97.29 (P1(f34(a58,a65),a65)),
% 96.64/97.29 inference(scs_inference,[],[236,280,285,289,295,3247,4017,4023,4035,1741,1730,32,102,27,99,39,38,51,50,69,37,52,70,29,71,23,30,22,31,20,28,84,36,64])).
% 96.64/97.29 cnf(4186,plain,
% 96.64/97.29 (P1(f20(a62,a3),a62)),
% 96.64/97.29 inference(scs_inference,[],[236,280,285,289,295,3247,4017,4023,4035,1741,1730,32,102,27,99,39,38,51,50,69,37,52,70,29,71,23,30,22,31,20,28,84,36,64,60])).
% 96.64/97.29 cnf(4188,plain,
% 96.64/97.29 (~P1(f39(a58,a65),a65)),
% 96.64/97.29 inference(scs_inference,[],[236,280,285,289,295,3247,4017,4023,4035,1741,1730,32,102,27,99,39,38,51,50,69,37,52,70,29,71,23,30,22,31,20,28,84,36,64,60,87])).
% 96.64/97.29 cnf(4190,plain,
% 96.64/97.29 (P1(f26(a65,a3),f79(a65))),
% 96.64/97.29 inference(scs_inference,[],[236,280,285,289,295,3247,4017,4023,4035,1741,1730,32,102,27,99,39,38,51,50,69,37,52,70,29,71,23,30,22,31,20,28,84,36,64,60,87,17])).
% 96.64/97.29 cnf(4192,plain,
% 96.64/97.29 (P1(f4(a62),a62)),
% 96.64/97.29 inference(scs_inference,[],[236,280,285,289,295,3247,4017,4023,4035,1741,1730,32,102,27,99,39,38,51,50,69,37,52,70,29,71,23,30,22,31,20,28,84,36,64,60,87,17,21])).
% 96.64/97.29 cnf(4198,plain,
% 96.64/97.29 (~P1(f14(a62,a71),a71)),
% 96.64/97.29 inference(scs_inference,[],[236,280,285,289,295,3247,3999,4017,4023,4035,4045,482,10,1741,1730,454,32,102,27,99,39,38,51,50,69,37,52,70,29,71,23,30,22,31,20,28,84,36,64,60,87,17,21,47,45,77])).
% 96.64/97.29 cnf(4201,plain,
% 96.64/97.29 (~P2(a8,a83)),
% 96.64/97.29 inference(scs_inference,[],[236,280,285,289,295,3247,3999,4074,4017,4023,4035,4045,482,10,1563,1741,1730,454,32,102,27,99,39,38,51,50,69,37,52,70,29,71,23,30,22,31,20,28,84,36,64,60,87,17,21,47,45,77,94])).
% 96.64/97.29 cnf(4204,plain,
% 96.64/97.29 (P6(a62,a62,a8)),
% 96.64/97.29 inference(scs_inference,[],[236,280,285,289,295,3247,3999,4074,4017,4023,4035,4045,482,10,1563,1741,1730,454,32,102,27,99,39,38,51,50,69,37,52,70,29,71,23,30,22,31,20,28,84,36,64,60,87,17,21,47,45,77,94,33])).
% 96.64/97.29 cnf(4211,plain,
% 96.64/97.29 (~P1(x42111,f46(a88,a88))),
% 96.64/97.29 inference(rename_variables,[],[918])).
% 96.64/97.29 cnf(4219,plain,
% 96.64/97.29 (~P6(a62,f79(a62),a10)),
% 96.64/97.29 inference(scs_inference,[],[236,280,285,289,295,3247,3999,4074,4017,4023,4035,4045,482,10,1563,5,1741,1730,454,654,918,4211,32,102,27,99,39,38,51,50,69,37,52,70,29,71,23,30,22,31,20,28,84,36,64,60,87,17,21,47,45,77,94,33,49,34,48,43,46,44])).
% 96.64/97.29 cnf(4221,plain,
% 96.64/97.29 (P1(f77(a62,a62),a62)),
% 96.64/97.29 inference(scs_inference,[],[236,280,285,289,295,3247,3999,4074,4017,4023,4035,4045,482,10,1563,5,1741,1730,454,654,918,4211,32,102,27,99,39,38,51,50,69,37,52,70,29,71,23,30,22,31,20,28,84,36,64,60,87,17,21,47,45,77,94,33,49,34,48,43,46,44,81])).
% 96.64/97.29 cnf(4223,plain,
% 96.64/97.29 (~P1(f40(a71,a58),a71)),
% 96.64/97.29 inference(scs_inference,[],[236,280,285,289,295,3247,3999,4007,4074,4017,4023,4035,4045,482,10,1563,5,1741,1730,454,654,918,4211,584,32,102,27,99,39,38,51,50,69,37,52,70,29,71,23,30,22,31,20,28,84,36,64,60,87,17,21,47,45,77,94,33,49,34,48,43,46,44,81,101])).
% 96.64/97.29 cnf(4227,plain,
% 96.64/97.29 (P1(f76(a62,a62),a62)),
% 96.64/97.29 inference(scs_inference,[],[236,280,285,289,295,3247,3999,4007,4074,4017,4023,4035,4045,482,10,1563,5,1741,1730,454,654,918,4211,584,32,102,27,99,39,38,51,50,69,37,52,70,29,71,23,30,22,31,20,28,84,36,64,60,87,17,21,47,45,77,94,33,49,34,48,43,46,44,81,101,80])).
% 96.64/97.29 cnf(4232,plain,
% 96.64/97.29 (~P1(f22(a62,a71),a71)),
% 96.64/97.29 inference(scs_inference,[],[236,280,285,289,295,3247,3999,4003,4007,4074,4017,4023,4035,4037,4045,482,527,10,1563,5,1741,1730,454,654,918,4211,14,584,32,102,27,99,39,38,51,50,69,37,52,70,29,71,23,30,22,31,20,28,84,36,64,60,87,17,21,47,45,77,94,33,49,34,48,43,46,44,81,101,80,76,90])).
% 96.64/97.29 cnf(4235,plain,
% 96.64/97.29 (~P1(f12(a62,a3),a62)),
% 96.64/97.29 inference(scs_inference,[],[236,280,285,289,295,3247,3999,4003,4007,4074,4017,4023,4035,4037,4045,482,1636,527,10,1563,5,1741,1730,454,654,918,4211,14,8,584,32,102,27,99,39,38,51,50,69,37,52,70,29,71,23,30,22,31,20,28,84,36,64,60,87,17,21,47,45,77,94,33,49,34,48,43,46,44,81,101,80,76,90,106])).
% 96.64/97.29 cnf(4238,plain,
% 96.64/97.29 (~P6(a62,a58,a74)),
% 96.64/97.29 inference(scs_inference,[],[236,280,285,289,295,3247,3999,4003,4007,4074,4017,4023,4035,4037,4045,482,1636,527,10,1563,5,1741,1730,454,654,918,4211,14,8,584,32,102,27,99,39,38,51,50,69,37,52,70,29,71,23,30,22,31,20,28,84,36,64,60,87,17,21,47,45,77,94,33,49,34,48,43,46,44,81,101,80,76,90,106,1292])).
% 96.64/97.29 cnf(4242,plain,
% 96.64/97.29 (P1(f75(a62,a62),a62)),
% 96.64/97.29 inference(scs_inference,[],[236,280,285,289,295,3247,3999,4003,4007,4074,4017,4023,4035,4037,4045,482,1636,527,10,1563,5,1741,1730,454,654,918,4211,14,8,584,32,102,27,99,39,38,51,50,69,37,52,70,29,71,23,30,22,31,20,28,84,36,64,60,87,17,21,47,45,77,94,33,49,34,48,43,46,44,81,101,80,76,90,106,1292,15,53])).
% 96.64/97.29 cnf(4252,plain,
% 96.64/97.29 (~P6(f49(a86,a8),f50(a86,a8),a8)),
% 96.64/97.29 inference(scs_inference,[],[282,102])).
% 96.64/97.29 cnf(4262,plain,
% 96.64/97.29 (P1(f75(a62,a62),a65)),
% 96.64/97.29 inference(scs_inference,[],[282,307,3176,4176,4242,4190,102,51,32,38,50,15])).
% 96.64/97.29 cnf(4274,plain,
% 96.64/97.29 (~P6(x42741,f79(a62),a87)),
% 96.64/97.29 inference(scs_inference,[],[282,307,313,3176,4176,4242,4190,102,51,32,38,50,15,70,99,27,52,39,29])).
% 96.64/97.29 cnf(4276,plain,
% 96.64/97.29 (~P1(f75(a62,a62),f79(a62))),
% 96.64/97.29 inference(scs_inference,[],[282,307,313,3176,4176,4242,4190,102,51,32,38,50,15,70,99,27,52,39,29,20])).
% 96.64/97.29 cnf(4286,plain,
% 96.64/97.29 (P6(f79(a65),x42861,a86)),
% 96.64/97.29 inference(scs_inference,[],[282,307,313,3176,4176,4242,4190,102,51,32,38,50,15,70,99,27,52,39,29,20,69,37,36,30,23])).
% 96.64/97.29 cnf(4288,plain,
% 96.64/97.29 (P6(f49(a86,a8),f50(a86,a8),a86)),
% 96.64/97.29 inference(scs_inference,[],[282,307,313,3176,4176,4242,4190,102,51,32,38,50,15,70,99,27,52,39,29,20,69,37,36,30,23,71])).
% 96.64/97.29 cnf(4292,plain,
% 96.64/97.29 (P6(x42921,f79(a65),a80)),
% 96.64/97.29 inference(scs_inference,[],[282,307,313,3176,4176,4242,4190,102,51,32,38,50,15,70,99,27,52,39,29,20,69,37,36,30,23,71,28,22])).
% 96.64/97.29 cnf(4296,plain,
% 96.64/97.29 (P1(f39(a58,a65),f79(a65))),
% 96.64/97.29 inference(scs_inference,[],[282,307,313,3176,4176,4242,4190,4188,102,51,32,38,50,15,70,99,27,52,39,29,20,69,37,36,30,23,71,28,22,31,17])).
% 96.64/97.29 cnf(4298,plain,
% 96.64/97.29 (P1(f52(a62,a62),a62)),
% 96.64/97.29 inference(scs_inference,[],[282,307,313,3176,4172,4176,4242,4190,4188,102,51,32,38,50,15,70,99,27,52,39,29,20,69,37,36,30,23,71,28,22,31,17,79])).
% 96.64/97.29 cnf(4299,plain,
% 96.64/97.29 (P6(x42991,a62,a80)),
% 96.64/97.29 inference(rename_variables,[],[4172])).
% 96.64/97.29 cnf(4301,plain,
% 96.64/97.29 (P1(f29(a62,a62),a62)),
% 96.64/97.29 inference(scs_inference,[],[282,307,313,3176,4168,4172,4176,4242,4190,4188,102,51,32,38,50,15,70,99,27,52,39,29,20,69,37,36,30,23,71,28,22,31,17,79,78])).
% 96.64/97.29 cnf(4306,plain,
% 96.64/97.29 (~P2(a80,a84)),
% 96.64/97.29 inference(scs_inference,[],[282,307,313,3176,4019,4168,4172,4299,4176,4242,4190,4188,1778,102,51,32,38,50,15,70,99,27,52,39,29,20,69,37,36,30,23,71,28,22,31,17,79,78,47,94])).
% 96.64/97.29 cnf(4310,plain,
% 96.64/97.29 (P1(f32(a62,a62),a62)),
% 96.64/97.29 inference(scs_inference,[],[282,307,313,3176,4019,4158,4168,4172,4299,4176,4242,4190,4188,1778,102,51,32,38,50,15,70,99,27,52,39,29,20,69,37,36,30,23,71,28,22,31,17,79,78,47,94,41])).
% 96.64/97.29 cnf(4313,plain,
% 96.64/97.29 (~P6(a65,f79(a62),a91)),
% 96.64/97.29 inference(scs_inference,[],[282,307,313,3176,4019,4158,4168,4172,4299,4176,4242,4190,4188,1778,102,51,32,38,50,15,70,99,27,52,39,29,20,69,37,36,30,23,71,28,22,31,17,79,78,47,94,41,49])).
% 96.64/97.29 cnf(4315,plain,
% 96.64/97.29 (~P1(f14(a62,a62),a62)),
% 96.64/97.29 inference(scs_inference,[],[282,307,313,3176,4019,4158,4168,4172,4299,4176,4242,4190,4188,1778,1559,102,51,32,38,50,15,70,99,27,52,39,29,20,69,37,36,30,23,71,28,22,31,17,79,78,47,94,41,49,77])).
% 96.64/97.29 cnf(4318,plain,
% 96.64/97.29 (P6(f79(a65),f79(a65),a8)),
% 96.64/97.29 inference(scs_inference,[],[282,307,313,3176,4019,4158,4168,4172,4299,4176,4242,4190,4188,1778,1559,102,51,32,38,50,15,70,99,27,52,39,29,20,69,37,36,30,23,71,28,22,31,17,79,78,47,94,41,49,77,33])).
% 96.64/97.29 cnf(4333,plain,
% 96.64/97.29 (~P1(f40(a65,a58),a65)),
% 96.64/97.29 inference(scs_inference,[],[282,307,313,3176,4019,4140,4158,4168,4172,4299,4176,4242,4190,4188,1778,1782,1559,918,584,102,51,32,38,50,15,70,99,27,52,39,29,20,69,37,36,30,23,71,28,22,31,17,79,78,47,94,41,49,77,33,34,45,48,44,46,43,101])).
% 96.64/97.29 cnf(4337,plain,
% 96.64/97.29 (P1(f60(a69,a58),a69)),
% 96.64/97.29 inference(scs_inference,[],[282,307,313,3176,4019,4140,4158,4168,4172,4299,4176,4242,4190,4188,1778,1782,591,1559,918,14,584,102,51,32,38,50,15,70,99,27,52,39,29,20,69,37,36,30,23,71,28,22,31,17,79,78,47,94,41,49,77,33,34,45,48,44,46,43,101,76])).
% 96.64/97.29 cnf(4340,plain,
% 96.64/97.29 (P1(f35(a62,a62),a62)),
% 96.64/97.29 inference(scs_inference,[],[282,307,313,3176,4019,4140,4148,4158,4168,4172,4299,4176,4242,4190,4188,4180,1778,1782,591,1559,918,14,584,102,51,32,38,50,15,70,99,27,52,39,29,20,69,37,36,30,23,71,28,22,31,17,79,78,47,94,41,49,77,33,34,45,48,44,46,43,101,76,74])).
% 96.64/97.29 cnf(4354,plain,
% 96.64/97.29 (~P6(a56,x43541,a85)),
% 96.64/97.29 inference(scs_inference,[],[4099,38])).
% 96.64/97.29 cnf(4362,plain,
% 96.64/97.29 (~P6(x43621,a65,a81)),
% 96.64/97.29 inference(scs_inference,[],[298,324,335,4099,4333,38,51,70,102,27])).
% 96.64/97.29 cnf(4364,plain,
% 96.64/97.29 (~P6(x43641,a65,a87)),
% 96.64/97.29 inference(scs_inference,[],[298,324,335,4099,4333,38,51,70,102,27,29])).
% 96.64/97.29 cnf(4374,plain,
% 96.64/97.29 (~P6(a56,x43741,a89)),
% 96.64/97.29 inference(scs_inference,[],[298,324,335,484,594,4221,4099,4333,9,38,51,70,102,27,29,50,32,52,15,39])).
% 96.64/97.29 cnf(4380,plain,
% 96.64/97.29 (~P6(a65,x43801,a84)),
% 96.64/97.29 inference(scs_inference,[],[298,324,335,340,484,594,4221,4099,4333,9,38,51,70,102,27,29,50,32,52,15,39,99,69,31])).
% 96.64/97.29 cnf(4382,plain,
% 96.64/97.29 (~P6(x43821,a65,a84)),
% 96.64/97.29 inference(scs_inference,[],[298,324,335,340,484,594,4221,4099,4333,9,38,51,70,102,27,29,50,32,52,15,39,99,69,31,28])).
% 96.64/97.29 cnf(4384,plain,
% 96.64/97.29 (~P1(f20(a62,a3),f79(a62))),
% 96.64/97.29 inference(scs_inference,[],[298,324,335,340,484,594,4186,4221,4099,4333,9,38,51,70,102,27,29,50,32,52,15,39,99,69,31,28,20])).
% 96.64/97.29 cnf(4386,plain,
% 96.64/97.29 (P6(a56,x43861,a86)),
% 96.64/97.29 inference(scs_inference,[],[298,324,335,340,484,594,4186,4221,4099,4333,9,38,51,70,102,27,29,50,32,52,15,39,99,69,31,28,20,23])).
% 96.64/97.29 cnf(4388,plain,
% 96.64/97.29 (P6(x43881,a56,a80)),
% 96.64/97.29 inference(scs_inference,[],[298,324,335,340,484,594,4186,4221,4099,4333,9,38,51,70,102,27,29,50,32,52,15,39,99,69,31,28,20,23,22])).
% 96.64/97.29 cnf(4390,plain,
% 96.64/97.29 (~P6(x43901,a65,a85)),
% 96.64/97.29 inference(scs_inference,[],[298,324,335,340,484,594,4186,4221,4099,4333,9,38,51,70,102,27,29,50,32,52,15,39,99,69,31,28,20,23,22,30])).
% 96.64/97.29 cnf(4392,plain,
% 96.64/97.29 (~P6(a56,x43921,a5)),
% 96.64/97.29 inference(scs_inference,[],[298,324,335,340,484,594,4186,4221,4099,4333,9,38,51,70,102,27,29,50,32,52,15,39,99,69,31,28,20,23,22,30,36])).
% 96.64/97.29 cnf(4394,plain,
% 96.64/97.29 (~P6(a56,x43941,a83)),
% 96.64/97.29 inference(scs_inference,[],[298,324,335,340,484,594,4186,4221,4099,4333,9,38,51,70,102,27,29,50,32,52,15,39,99,69,31,28,20,23,22,30,36,37])).
% 96.64/97.29 cnf(4398,plain,
% 96.64/97.29 (P1(f14(a62,a71),f79(a71))),
% 96.64/97.29 inference(scs_inference,[],[298,324,335,340,484,594,4186,4221,4198,4099,4333,9,38,51,70,102,27,29,50,32,52,15,39,99,69,31,28,20,23,22,30,36,37,71,17])).
% 96.64/97.29 cnf(4412,plain,
% 96.64/97.29 (~P2(a8,a85)),
% 96.64/97.29 inference(scs_inference,[],[298,324,335,340,484,4204,4150,594,4186,4221,4296,4198,4099,4333,1750,9,481,1432,38,51,70,102,27,29,50,32,52,15,39,99,69,31,28,20,23,22,30,36,37,71,17,21,79,47,78,49,94])).
% 96.64/97.29 cnf(4415,plain,
% 96.64/97.29 (P6(a56,a56,a8)),
% 96.64/97.29 inference(scs_inference,[],[298,324,335,340,484,4204,4150,594,4186,4221,4296,4198,4099,4333,1750,9,481,1432,38,51,70,102,27,29,50,32,52,15,39,99,69,31,28,20,23,22,30,36,37,71,17,21,79,47,78,49,94,33])).
% 96.64/97.29 cnf(4418,plain,
% 96.64/97.29 (~P1(x44181,f46(a88,a88))),
% 96.64/97.29 inference(rename_variables,[],[918])).
% 96.64/97.29 cnf(4420,plain,
% 96.64/97.29 (P6(a56,a56,a82)),
% 96.64/97.29 inference(scs_inference,[],[298,324,335,340,484,4204,4150,594,4186,4184,4221,4296,4198,4099,4333,1750,9,481,1432,918,38,51,70,102,27,29,50,32,52,15,39,99,69,31,28,20,23,22,30,36,37,71,17,21,79,47,78,49,94,33,48,34])).
% 96.64/97.29 cnf(4433,plain,
% 96.64/97.29 (P1(f76(a56,a56),a56)),
% 96.64/97.29 inference(scs_inference,[],[298,324,335,340,484,4204,4150,594,4186,4184,4221,4296,4276,4198,4262,4099,4333,1750,9,481,1432,918,4418,38,51,70,102,27,29,50,32,52,15,39,99,69,31,28,20,23,22,30,36,37,71,17,21,79,47,78,49,94,33,48,34,43,44,45,81,46,80])).
% 96.64/97.29 cnf(4435,plain,
% 96.64/97.29 (~P1(f40(a2,a58),a2)),
% 96.64/97.29 inference(scs_inference,[],[298,324,335,340,484,4204,4150,594,4186,4184,4221,4296,4276,4198,4262,4099,4333,1750,9,481,1432,918,4418,584,38,51,70,102,27,29,50,32,52,15,39,99,69,31,28,20,23,22,30,36,37,71,17,21,79,47,78,49,94,33,48,34,43,44,45,81,46,80,101])).
% 96.64/97.29 cnf(4439,plain,
% 96.64/97.29 (~P1(x44391,a58)),
% 96.64/97.29 inference(rename_variables,[],[14])).
% 96.64/97.29 cnf(4441,plain,
% 96.64/97.29 (~P6(a56,a58,a74)),
% 96.64/97.29 inference(scs_inference,[],[298,324,335,340,484,4204,4150,594,4186,4184,4221,4296,4276,4198,4262,4099,4333,1750,579,9,481,1432,918,4418,14,584,38,51,70,102,27,29,50,32,52,15,39,99,69,31,28,20,23,22,30,36,37,71,17,21,79,47,78,49,94,33,48,34,43,44,45,81,46,80,101,76,1292])).
% 96.64/97.29 cnf(4445,plain,
% 96.64/97.29 (P1(x44451,a56)+P1(f19(a56,a58),a56)),
% 96.64/97.29 inference(scs_inference,[],[298,324,335,340,484,4204,4150,594,4186,4184,4221,4296,4276,4198,4262,4099,4333,1750,579,9,481,1432,918,4418,14,4439,584,38,51,70,102,27,29,50,32,52,15,39,99,69,31,28,20,23,22,30,36,37,71,17,21,79,47,78,49,94,33,48,34,43,44,45,81,46,80,101,76,1292,54,96])).
% 96.64/97.29 cnf(4449,plain,
% 96.64/97.29 (P1(f19(a56,a58),a56)),
% 96.64/97.29 inference(factoring_inference,[],[4445])).
% 96.64/97.29 cnf(4454,plain,
% 96.64/97.29 (~P6(f79(a71),x44541,a85)),
% 96.64/97.29 inference(scs_inference,[],[310,622,4398,51,102,38])).
% 96.64/97.29 cnf(4464,plain,
% 96.64/97.29 (~P6(x44641,a2,a81)),
% 96.64/97.29 inference(scs_inference,[],[310,488,622,745,1473,4398,4435,51,102,38,50,70,99,52,27])).
% 96.64/97.29 cnf(4468,plain,
% 96.64/97.29 (~P6(f79(a71),x44681,a89)),
% 96.64/97.29 inference(scs_inference,[],[310,488,622,745,1473,4227,4398,4435,51,102,38,50,70,99,52,27,15,39])).
% 96.64/97.29 cnf(4470,plain,
% 96.64/97.29 (~P6(x44701,a2,a87)),
% 96.64/97.29 inference(scs_inference,[],[310,488,622,745,1473,4227,4398,4435,51,102,38,50,70,99,52,27,15,39,29])).
% 96.64/97.29 cnf(4474,plain,
% 96.64/97.29 (~P6(a2,x44741,a84)),
% 96.64/97.29 inference(scs_inference,[],[310,488,622,745,1473,4227,4398,4435,918,51,102,38,50,70,99,52,27,15,39,29,32,31])).
% 96.64/97.29 cnf(4486,plain,
% 96.64/97.29 (P6(f79(a71),x44861,a86)),
% 96.64/97.29 inference(scs_inference,[],[310,488,622,745,1473,4227,4398,4435,918,51,102,38,50,70,99,52,27,15,39,29,32,31,69,71,36,37,22,23])).
% 96.64/97.29 cnf(4488,plain,
% 96.64/97.29 (~P1(f19(a56,a58),f79(a56))),
% 96.64/97.29 inference(scs_inference,[],[310,488,622,745,1473,4449,4227,4398,4435,918,51,102,38,50,70,99,52,27,15,39,29,32,31,69,71,36,37,22,23,20])).
% 96.64/97.29 cnf(4490,plain,
% 96.64/97.29 (~P6(x44901,a2,a84)),
% 96.64/97.29 inference(scs_inference,[],[310,488,622,745,1473,4449,4227,4398,4435,918,51,102,38,50,70,99,52,27,15,39,29,32,31,69,71,36,37,22,23,20,28])).
% 96.64/97.29 cnf(4492,plain,
% 96.64/97.29 (~P6(x44921,a2,a85)),
% 96.64/97.29 inference(scs_inference,[],[310,488,622,745,1473,4449,4227,4398,4435,918,51,102,38,50,70,99,52,27,15,39,29,32,31,69,71,36,37,22,23,20,28,30])).
% 96.64/97.29 cnf(4494,plain,
% 96.64/97.29 (P1(f40(a71,a58),f79(a71))),
% 96.64/97.29 inference(scs_inference,[],[310,488,622,745,1473,4449,4227,4223,4398,4435,918,51,102,38,50,70,99,52,27,15,39,29,32,31,69,71,36,37,22,23,20,28,30,17])).
% 96.64/97.29 cnf(4501,plain,
% 96.64/97.29 (~P2(a86,a84)),
% 96.64/97.29 inference(scs_inference,[],[310,488,622,745,4031,4386,4388,1473,4449,4227,4223,4398,4435,4188,4296,918,51,102,38,50,70,99,52,27,15,39,29,32,31,69,71,36,37,22,23,20,28,30,17,79,47,94])).
% 96.64/97.29 cnf(4503,plain,
% 96.64/97.29 (P6(a56,x45031,a86)),
% 96.64/97.29 inference(rename_variables,[],[4386])).
% 96.64/97.29 cnf(4511,plain,
% 96.64/97.29 (~P6(f79(a65),a65,a91)),
% 96.64/97.29 inference(scs_inference,[],[310,488,622,745,4031,4386,4503,4388,4394,1473,4449,4227,4223,4398,4435,4188,4296,918,51,102,38,50,70,99,52,27,15,39,29,32,31,69,71,36,37,22,23,20,28,30,17,79,47,94,78,41,49])).
% 96.64/97.29 cnf(4513,plain,
% 96.64/97.29 (~P1(f14(a56,a65),a65)),
% 96.64/97.29 inference(scs_inference,[],[310,488,622,745,4031,4362,4386,4503,4388,4394,1473,4449,4227,4223,4398,4435,4188,4296,918,51,102,38,50,70,99,52,27,15,39,29,32,31,69,71,36,37,22,23,20,28,30,17,79,47,94,78,41,49,77])).
% 96.64/97.29 cnf(4518,plain,
% 96.64/97.29 (P6(f79(a71),f79(a71),a8)),
% 96.64/97.29 inference(scs_inference,[],[310,488,622,745,4031,4362,4386,4503,4388,4394,1473,4449,4227,4223,4398,4435,4188,4198,4296,918,51,102,38,50,70,99,52,27,15,39,29,32,31,69,71,36,37,22,23,20,28,30,17,79,47,94,78,41,49,77,48,33])).
% 96.64/97.29 cnf(4523,plain,
% 96.64/97.29 (~P1(x45231,f46(a88,a88))),
% 96.64/97.29 inference(rename_variables,[],[918])).
% 96.64/97.29 cnf(4525,plain,
% 96.64/97.29 (P6(f79(a71),f79(a71),a82)),
% 96.64/97.29 inference(scs_inference,[],[310,488,622,745,4031,4362,4386,4503,4388,4394,1473,4449,4227,4223,4398,4435,4188,4198,4296,918,51,102,38,50,70,99,52,27,15,39,29,32,31,69,71,36,37,22,23,20,28,30,17,79,47,94,78,41,49,77,48,33,44,46,34])).
% 96.64/97.29 cnf(4528,plain,
% 96.64/97.29 (P1(x45281,f48(a84,a84))),
% 96.64/97.29 inference(rename_variables,[],[654])).
% 96.64/97.29 cnf(4534,plain,
% 96.64/97.29 (~P1(x45341,f46(a88,a88))),
% 96.64/97.29 inference(rename_variables,[],[918])).
% 96.64/97.29 cnf(4539,plain,
% 96.64/97.29 (P1(f60(a59,a58),a59)),
% 96.64/97.29 inference(scs_inference,[],[310,488,622,745,4031,4362,4386,4503,4388,4394,1473,4449,4227,4223,4398,4337,4435,549,4188,4198,4296,4045,654,4528,918,4523,4534,14,51,102,38,50,70,99,52,27,15,39,29,32,31,69,71,36,37,22,23,20,28,30,17,79,47,94,78,41,49,77,48,33,44,46,34,45,43,81,80,76])).
% 96.64/97.29 cnf(4540,plain,
% 96.64/97.29 (~P1(x45401,a58)),
% 96.64/97.29 inference(rename_variables,[],[14])).
% 96.64/97.29 cnf(4542,plain,
% 96.64/97.29 (~P1(f22(a71,a65),a65)),
% 96.64/97.29 inference(scs_inference,[],[310,488,622,745,4031,4362,4364,4386,4503,4388,4394,1473,4449,4227,4223,4398,4337,4435,549,7,4188,4198,4296,4045,654,4528,918,4523,4534,14,51,102,38,50,70,99,52,27,15,39,29,32,31,69,71,36,37,22,23,20,28,30,17,79,47,94,78,41,49,77,48,33,44,46,34,45,43,81,80,76,90])).
% 96.64/97.29 cnf(4547,plain,
% 96.64/97.29 (P6(a56,a58,a9)),
% 96.64/97.29 inference(scs_inference,[],[310,488,622,745,4031,4362,4364,4386,4503,4388,4394,1473,4449,4227,4223,4398,4337,4435,549,7,4188,4198,4296,4045,654,4528,918,4523,4534,14,584,51,102,38,50,70,99,52,27,15,39,29,32,31,69,71,36,37,22,23,20,28,30,17,79,47,94,78,41,49,77,48,33,44,46,34,45,43,81,80,76,90,1292,40])).
% 96.64/97.29 cnf(4556,plain,
% 96.64/97.29 (P1(f19(a62,a58),a62)),
% 96.64/97.29 inference(scs_inference,[],[310,488,622,745,4238,4031,4354,4362,4364,4374,4386,4503,4388,4394,1473,4420,4449,4192,4227,4223,4398,4315,4337,4435,549,7,4188,4198,4296,4045,654,4528,918,4523,4534,14,4540,584,51,102,38,50,70,99,52,27,15,39,29,32,31,69,71,36,37,22,23,20,28,30,17,79,47,94,78,41,49,77,48,33,44,46,34,45,43,81,80,76,90,1292,40,91,74,96])).
% 96.64/97.29 cnf(4559,plain,
% 96.64/97.29 (P1(f38(a56,a58),a56)),
% 96.64/97.29 inference(scs_inference,[],[310,488,622,745,4238,4031,4354,4362,4364,4374,4386,4503,4388,4394,1473,4420,4449,4192,4227,4223,4398,4315,4337,4435,549,7,4188,4198,4296,4045,654,4528,918,4523,4534,14,4540,584,51,102,38,50,70,99,52,27,15,39,29,32,31,69,71,36,37,22,23,20,28,30,17,79,47,94,78,41,49,77,48,33,44,46,34,45,43,81,80,76,90,1292,40,91,74,96,65])).
% 96.64/97.29 cnf(4572,plain,
% 96.64/97.29 (~P6(a59,x45721,a85)),
% 96.64/97.29 inference(scs_inference,[],[326,796,1106,4059,4539,102,50,51,52,38])).
% 96.64/97.29 cnf(4574,plain,
% 96.64/97.29 (P1(f19(a62,a58),a65)),
% 96.64/97.29 inference(scs_inference,[],[326,796,1106,4059,4556,4539,102,50,51,52,38,15])).
% 96.64/97.29 cnf(4580,plain,
% 96.64/97.29 (~P6(a59,x45801,a89)),
% 96.64/97.29 inference(scs_inference,[],[326,752,796,1106,4059,4488,4556,4539,102,50,51,52,38,15,32,70,39])).
% 96.64/97.29 cnf(4592,plain,
% 96.64/97.29 (~P1(f38(a56,a58),f79(a56))),
% 96.64/97.29 inference(scs_inference,[],[326,752,796,798,1106,4059,4559,4488,4556,4539,102,50,51,52,38,15,32,70,39,29,99,27,69,31,20])).
% 96.64/97.29 cnf(4596,plain,
% 96.64/97.29 (P6(x45961,a59,a80)),
% 96.64/97.29 inference(scs_inference,[],[326,752,796,798,1106,4059,4559,4488,4556,4539,102,50,51,52,38,15,32,70,39,29,99,27,69,31,20,28,22])).
% 96.64/97.29 cnf(4602,plain,
% 96.64/97.29 (~P6(a59,x46021,a83)),
% 96.64/97.29 inference(scs_inference,[],[326,752,796,798,1106,4059,4559,4488,4556,4232,4539,102,50,51,52,38,15,32,70,39,29,99,27,69,31,20,28,22,17,30,37])).
% 96.64/97.29 cnf(4604,plain,
% 96.64/97.29 (~P6(a59,x46041,a5)),
% 96.64/97.29 inference(scs_inference,[],[326,752,796,798,1106,4059,4559,4488,4556,4232,4539,102,50,51,52,38,15,32,70,39,29,99,27,69,31,20,28,22,17,30,37,36])).
% 96.64/97.29 cnf(4608,plain,
% 96.64/97.29 (P6(a59,x46081,a86)),
% 96.64/97.29 inference(scs_inference,[],[326,752,796,798,1106,4059,4559,4488,4556,4232,4539,102,50,51,52,38,15,32,70,39,29,99,27,69,31,20,28,22,17,30,37,36,71,23])).
% 96.64/97.29 cnf(4610,plain,
% 96.64/97.29 (P1(f52(a56,a62),a62)),
% 96.64/97.29 inference(scs_inference,[],[326,752,796,798,1106,4059,4559,4488,4556,4232,4539,4172,102,50,51,52,38,15,32,70,39,29,99,27,69,31,20,28,22,17,30,37,36,71,23,79])).
% 96.64/97.29 cnf(4613,plain,
% 96.64/97.29 (~P2(a9,a74)),
% 96.64/97.29 inference(scs_inference,[],[326,752,796,798,1106,4547,4441,4059,4559,4488,4556,4232,4539,4172,102,50,51,52,38,15,32,70,39,29,99,27,69,31,20,28,22,17,30,37,36,71,23,79,94])).
% 96.64/97.29 cnf(4617,plain,
% 96.64/97.29 (P1(f29(a62,a56),a62)),
% 96.64/97.29 inference(scs_inference,[],[326,752,796,798,1106,4547,4441,4059,4559,4488,4494,4556,4232,4539,4168,4172,4223,102,50,51,52,38,15,32,70,39,29,99,27,69,31,20,28,22,17,30,37,36,71,23,79,94,47,78])).
% 96.64/97.29 cnf(4622,plain,
% 96.64/97.29 (P1(f32(a62,a56),a62)),
% 96.64/97.29 inference(scs_inference,[],[326,752,796,798,1106,4547,4441,4059,4559,4488,4494,4556,4232,4539,4158,4168,4172,4223,102,50,51,52,38,15,32,70,39,29,99,27,69,31,20,28,22,17,30,37,36,71,23,79,94,47,78,49,41])).
% 96.64/97.29 cnf(4626,plain,
% 96.64/97.29 (~P1(x46261,f46(a88,a88))),
% 96.64/97.29 inference(rename_variables,[],[918])).
% 96.64/97.29 cnf(4628,plain,
% 96.64/97.29 (~P1(f14(a56,a2),a2)),
% 96.64/97.29 inference(scs_inference,[],[326,752,796,798,1106,4547,4441,4464,4059,4559,4488,4494,4556,4232,4539,4158,4168,4172,4223,918,102,50,51,52,38,15,32,70,39,29,99,27,69,31,20,28,22,17,30,37,36,71,23,79,94,47,78,49,41,48,77])).
% 96.64/97.29 cnf(4633,plain,
% 96.64/97.29 (P6(a59,a59,a8)),
% 96.64/97.29 inference(scs_inference,[],[326,752,796,798,1106,4547,4441,4464,4059,4559,4488,4494,4556,4232,4539,4158,4168,4172,4223,4449,918,102,50,51,52,38,15,32,70,39,29,99,27,69,31,20,28,22,17,30,37,36,71,23,79,94,47,78,49,41,48,77,46,33])).
% 96.64/97.29 cnf(4644,plain,
% 96.64/97.29 (P1(f77(a59,a59),a59)),
% 96.64/97.29 inference(scs_inference,[],[326,752,796,798,1106,4547,4441,4464,4059,4559,4488,4494,4556,4232,4539,4158,4168,4172,4223,4449,918,4626,102,50,51,52,38,15,32,70,39,29,99,27,69,31,20,28,22,17,30,37,36,71,23,79,94,47,78,49,41,48,77,46,33,43,34,44,45,81])).
% 96.64/97.29 cnf(4646,plain,
% 96.64/97.29 (P3(a86,a8)),
% 96.64/97.29 inference(scs_inference,[],[326,752,796,798,1106,4547,4441,4464,4059,4559,4318,4488,4494,4286,4556,4232,4539,4158,4168,4172,4223,4449,918,4626,102,50,51,52,38,15,32,70,39,29,99,27,69,31,20,28,22,17,30,37,36,71,23,79,94,47,78,49,41,48,77,46,33,43,34,44,45,81,100])).
% 96.64/97.29 cnf(4647,plain,
% 96.64/97.29 (P6(f79(a65),x46471,a86)),
% 96.64/97.29 inference(rename_variables,[],[4286])).
% 96.64/97.29 cnf(4649,plain,
% 96.64/97.29 (P1(f76(a59,a59),a59)),
% 96.64/97.29 inference(scs_inference,[],[326,752,796,798,1106,4547,4441,4464,4059,4559,4318,4488,4494,4286,4556,4232,4539,4158,4168,4172,4223,4449,918,4626,102,50,51,52,38,15,32,70,39,29,99,27,69,31,20,28,22,17,30,37,36,71,23,79,94,47,78,49,41,48,77,46,33,43,34,44,45,81,100,80])).
% 96.64/97.29 cnf(4651,plain,
% 96.64/97.29 (P1(f72(a58,a59),a59)),
% 96.64/97.29 inference(scs_inference,[],[326,752,796,798,1106,4547,4441,4464,4059,4559,4318,4488,4494,4286,4556,4232,4539,552,4158,4168,4172,4223,4449,918,4626,14,102,50,51,52,38,15,32,70,39,29,99,27,69,31,20,28,22,17,30,37,36,71,23,79,94,47,78,49,41,48,77,46,33,43,34,44,45,81,100,80,76])).
% 96.64/97.29 cnf(4654,plain,
% 96.64/97.29 (~P6(a59,a58,a74)),
% 96.64/97.29 inference(scs_inference,[],[326,752,796,798,1106,4547,4441,4464,4059,4559,4318,4488,4494,4286,4556,4232,4539,552,4158,4168,4172,4223,4449,918,4626,14,102,50,51,52,38,15,32,70,39,29,99,27,69,31,20,28,22,17,30,37,36,71,23,79,94,47,78,49,41,48,77,46,33,43,34,44,45,81,100,80,76,1292])).
% 96.64/97.29 cnf(4656,plain,
% 96.64/97.29 (P1(f75(a59,a59),a59)),
% 96.64/97.29 inference(scs_inference,[],[326,752,796,798,1106,4547,4441,4464,4059,4559,4318,4488,4494,4286,4556,4232,4539,552,4158,4168,4172,4223,4449,918,4626,14,102,50,51,52,38,15,32,70,39,29,99,27,69,31,20,28,22,17,30,37,36,71,23,79,94,47,78,49,41,48,77,46,33,43,34,44,45,81,100,80,76,1292,54])).
% 96.64/97.29 cnf(4658,plain,
% 96.64/97.29 (P1(f4(a59),a59)),
% 96.64/97.29 inference(scs_inference,[],[326,752,796,798,1106,4547,4441,4464,4059,4559,4318,4488,4494,4286,4556,4232,4539,552,4158,4168,4172,4223,4449,918,4626,14,102,50,51,52,38,15,32,70,39,29,99,27,69,31,20,28,22,17,30,37,36,71,23,79,94,47,78,49,41,48,77,46,33,43,34,44,45,81,100,80,76,1292,54,21])).
% 96.64/97.29 cnf(4662,plain,
% 96.64/97.29 (~P1(f23(a65,a3),a65)),
% 96.64/97.29 inference(scs_inference,[],[229,326,752,796,798,1106,4547,4441,4380,4464,4059,4559,4318,4488,4494,4286,4556,4232,4539,552,4158,4168,4172,4223,4449,918,4626,14,8,102,50,51,52,38,15,32,70,39,29,99,27,69,31,20,28,22,17,30,37,36,71,23,79,94,47,78,49,41,48,77,46,33,43,34,44,45,81,100,80,76,1292,54,21,109,98])).
% 96.64/97.29 cnf(4667,plain,
% 96.64/97.29 (P6(f79(a65),x46671,a86)),
% 96.64/97.29 inference(rename_variables,[],[4286])).
% 96.64/97.29 cnf(4669,plain,
% 96.64/97.29 (~P5(a86,a8)),
% 96.64/97.29 inference(scs_inference,[],[229,326,752,796,798,1106,4547,4441,4380,4464,4059,4559,4318,4488,4494,4286,4647,4667,4556,4232,4539,552,4158,4168,4172,4223,4449,918,4626,14,8,102,50,51,52,38,15,32,70,39,29,99,27,69,31,20,28,22,17,30,37,36,71,23,79,94,47,78,49,41,48,77,46,33,43,34,44,45,81,100,80,76,1292,54,21,109,98,105,104])).
% 96.64/97.29 cnf(4705,plain,
% 96.64/97.29 (P1(f14(a56,a2),f79(a2))),
% 96.64/97.29 inference(scs_inference,[],[337,1108,1133,1137,4201,4610,4628,4337,918,784,50,102,51,52,38,32,15,28,29,39,70,99,27,71,69,17])).
% 96.64/97.29 cnf(4709,plain,
% 96.64/97.29 (~P1(f75(a59,a59),f79(a59))),
% 96.64/97.29 inference(scs_inference,[],[337,1108,1133,1137,4201,4656,4610,4628,4337,918,784,50,102,51,52,38,32,15,28,29,39,70,99,27,71,69,17,36,20])).
% 96.64/97.29 cnf(4711,plain,
% 96.64/97.29 (P6(a69,x47111,a86)),
% 96.64/97.29 inference(scs_inference,[],[337,1108,1133,1137,4201,4656,4610,4628,4337,918,784,50,102,51,52,38,32,15,28,29,39,70,99,27,71,69,17,36,20,23])).
% 96.64/97.29 cnf(4713,plain,
% 96.64/97.29 (P6(x47131,a69,a80)),
% 96.64/97.29 inference(scs_inference,[],[337,1108,1133,1137,4201,4656,4610,4628,4337,918,784,50,102,51,52,38,32,15,28,29,39,70,99,27,71,69,17,36,20,23,22])).
% 96.64/97.29 cnf(4717,plain,
% 96.64/97.29 (~P6(a69,x47171,a83)),
% 96.64/97.29 inference(scs_inference,[],[337,1108,1133,1137,4201,4656,4610,4628,4337,918,784,50,102,51,52,38,32,15,28,29,39,70,99,27,71,69,17,36,20,23,22,31,37])).
% 96.64/97.29 cnf(4725,plain,
% 96.64/97.29 (P1(f52(a59,a59),a59)),
% 96.64/97.29 inference(scs_inference,[],[337,1108,1133,1137,4596,4201,4656,4592,4610,4628,4337,4559,918,784,50,102,51,52,38,32,15,28,29,39,70,99,27,71,69,17,36,20,23,22,31,37,21,30,47,79])).
% 96.64/97.29 cnf(4733,plain,
% 96.64/97.29 (~P2(a86,a85)),
% 96.64/97.29 inference(scs_inference,[],[337,1108,1133,1137,4390,4596,4602,4608,4201,4656,4592,4610,4628,4337,4559,918,784,50,102,51,52,38,32,15,28,29,39,70,99,27,71,69,17,36,20,23,22,31,37,21,30,47,79,41,49,94])).
% 96.64/97.29 cnf(4734,plain,
% 96.64/97.29 (~P6(x47341,a65,a85)),
% 96.64/97.29 inference(rename_variables,[],[4390])).
% 96.64/97.29 cnf(4735,plain,
% 96.64/97.29 (P6(a59,x47351,a86)),
% 96.64/97.29 inference(rename_variables,[],[4608])).
% 96.64/97.29 cnf(4752,plain,
% 96.64/97.29 (P6(a69,a69,a8)),
% 96.64/97.29 inference(scs_inference,[],[337,1108,1133,1137,4382,4390,4734,4596,4602,4608,4735,4201,4656,4384,4592,4610,4628,4337,4186,4559,918,784,50,102,51,52,38,32,15,28,29,39,70,99,27,71,69,17,36,20,23,22,31,37,21,30,47,79,41,49,94,78,75,48,46,44,43,33])).
% 96.64/97.29 cnf(4758,plain,
% 96.64/97.29 (P1(f77(a69,a69),a69)),
% 96.73/97.29 inference(scs_inference,[],[337,1108,1133,1137,4382,4390,4734,4596,4602,4608,4735,4201,4656,4384,4592,4610,4628,4337,4186,4559,918,784,50,102,51,52,38,32,15,28,29,39,70,99,27,71,69,17,36,20,23,22,31,37,21,30,47,79,41,49,94,78,75,48,46,44,43,33,34,45,81])).
% 96.73/97.29 cnf(4764,plain,
% 96.73/97.29 (P1(f76(a69,a69),a69)),
% 96.73/97.29 inference(scs_inference,[],[337,1108,1133,1137,4382,4390,4734,4572,4596,4602,4608,4735,4201,4656,4384,4592,4610,4628,4337,4186,4559,918,784,8,50,102,51,52,38,32,15,28,29,39,70,99,27,71,69,17,36,20,23,22,31,37,21,30,47,79,41,49,94,78,75,48,46,44,43,33,34,45,81,93,80])).
% 96.73/97.29 cnf(4766,plain,
% 96.73/97.29 (P1(f60(a2,a58),a2)),
% 96.73/97.29 inference(scs_inference,[],[337,1108,1133,1137,4382,4390,4734,4572,4596,4602,4608,4735,4201,4656,4384,4592,4610,4628,233,4337,4186,4559,918,784,14,8,50,102,51,52,38,32,15,28,29,39,70,99,27,71,69,17,36,20,23,22,31,37,21,30,47,79,41,49,94,78,75,48,46,44,43,33,34,45,81,93,80,76])).
% 96.73/97.29 cnf(4772,plain,
% 96.73/97.29 (~P1(f22(a65,a2),a2)),
% 96.73/97.29 inference(scs_inference,[],[337,1108,1133,1137,4382,4390,4734,4470,4572,4580,4596,4602,4608,4735,4201,4656,4384,4592,4574,4610,4628,4662,233,4337,4186,4559,918,784,14,8,50,102,51,52,38,32,15,28,29,39,70,99,27,71,69,17,36,20,23,22,31,37,21,30,47,79,41,49,94,78,75,48,46,44,43,33,34,45,81,93,80,76,74,90])).
% 96.73/97.29 cnf(4777,plain,
% 96.73/97.29 (P1(f75(a69,a69),a69)),
% 96.73/97.29 inference(scs_inference,[],[337,1108,1133,1137,4382,4390,4734,4470,4572,4580,4596,4602,4608,4735,4201,4656,4384,4592,4574,4610,4628,4662,233,4337,4186,4559,918,784,14,8,50,102,51,52,38,32,15,28,29,39,70,99,27,71,69,17,36,20,23,22,31,37,21,30,47,79,41,49,94,78,75,48,46,44,43,33,34,45,81,93,80,76,74,90,1292,53])).
% 96.73/97.29 cnf(4796,plain,
% 96.73/97.29 (P1(f22(a65,a2),f79(a2))),
% 96.73/97.29 inference(scs_inference,[],[348,1229,4501,4709,4705,4772,4617,102,50,51,38,52,15,32,17])).
% 96.73/97.29 cnf(4806,plain,
% 96.73/97.29 (~P1(f77(a59,a59),f79(a59))),
% 96.73/97.29 inference(scs_inference,[],[348,1229,4501,4644,4709,4705,4772,4617,102,50,51,38,52,15,32,17,39,29,28,27,20])).
% 96.73/97.29 cnf(4824,plain,
% 96.73/97.29 (P6(f79(a2),x48241,a86)),
% 96.73/97.29 inference(scs_inference,[],[348,1213,1229,4501,4644,4709,4705,4772,4617,102,50,51,38,52,15,32,17,39,29,28,27,20,37,69,99,70,31,71,36,22,23])).
% 96.73/97.30 cnf(4841,plain,
% 96.73/97.30 (P1(f29(a69,a59),a69)),
% 96.73/97.30 inference(scs_inference,[],[348,1213,1229,4633,4501,4604,4711,4713,4717,4644,4709,4705,4772,4617,4628,102,50,51,38,52,15,32,17,39,29,28,27,20,37,69,99,70,31,71,36,22,23,30,79,94,47,49,41,78])).
% 96.73/97.30 cnf(4847,plain,
% 96.73/97.30 (~P1(f14(a59,a71),a71)),
% 96.73/97.30 inference(scs_inference,[],[348,1213,1229,4633,4501,4604,4711,4713,4717,4644,4709,4705,4772,4617,3999,4628,918,102,50,51,38,52,15,32,17,39,29,28,27,20,37,69,99,70,31,71,36,22,23,30,79,94,47,49,41,78,48,77])).
% 96.73/97.30 cnf(4894,plain,
% 96.73/97.30 (~P6(a2,x48941,a85)),
% 96.73/97.30 inference(scs_inference,[],[355,1242,4306,4766,50,102,51,38])).
% 96.73/97.30 cnf(4904,plain,
% 96.73/97.30 (~P6(a2,x49041,a83)),
% 96.73/97.30 inference(scs_inference,[],[355,1242,4306,4622,4766,784,14,50,102,51,38,52,32,15,29,37])).
% 96.73/97.30 cnf(4906,plain,
% 96.73/97.30 (~P6(a2,x49061,a89)),
% 96.73/97.30 inference(scs_inference,[],[355,1242,4306,4622,4766,784,14,50,102,51,38,52,32,15,29,37,39])).
% 96.73/97.30 cnf(4908,plain,
% 96.73/97.30 (P1(f14(a59,a71),f79(a71))),
% 96.73/97.30 inference(scs_inference,[],[355,1242,4306,4847,4622,4766,784,14,50,102,51,38,52,32,15,29,37,39,17])).
% 96.73/97.30 cnf(4914,plain,
% 96.73/97.30 (~P6(x49141,f48(a5,a5),a81)),
% 96.73/97.30 inference(scs_inference,[],[355,1242,4306,4847,4622,4766,784,14,645,50,102,51,38,52,32,15,29,37,39,17,99,28,27])).
% 96.73/97.30 cnf(4918,plain,
% 96.73/97.30 (~P1(f75(a69,a69),f79(a69))),
% 96.73/97.30 inference(scs_inference,[],[355,1225,1242,4306,4777,4847,4622,4766,784,14,645,50,102,51,38,52,32,15,29,37,39,17,99,28,27,70,20])).
% 96.73/97.30 cnf(4922,plain,
% 96.73/97.30 (P6(x49221,a2,a80)),
% 96.73/97.30 inference(scs_inference,[],[355,1225,1242,4306,4777,4847,4622,4766,784,14,645,50,102,51,38,52,32,15,29,37,39,17,99,28,27,70,20,36,22])).
% 96.73/97.30 cnf(4926,plain,
% 96.73/97.30 (~P6(f45(a5,a5),x49261,a84)),
% 96.73/97.30 inference(scs_inference,[],[355,1225,1242,4306,4777,4847,4622,4766,784,14,645,50,102,51,38,52,32,15,29,37,39,17,99,28,27,70,20,36,22,69,31])).
% 96.73/97.30 cnf(4930,plain,
% 96.73/97.30 (P6(a2,x49301,a86)),
% 96.73/97.30 inference(scs_inference,[],[355,1225,1242,4306,4777,4847,4622,4766,784,14,645,50,102,51,38,52,32,15,29,37,39,17,99,28,27,70,20,36,22,69,31,71,23])).
% 96.73/97.30 cnf(4934,plain,
% 96.73/97.30 (~P2(a86,a10)),
% 96.73/97.30 inference(scs_inference,[],[355,1225,1242,4306,4777,4082,4847,4622,4286,4766,784,14,645,50,102,51,38,52,32,15,29,37,39,17,99,28,27,70,20,36,22,69,31,71,23,30,94])).
% 96.73/97.30 cnf(4946,plain,
% 96.73/97.30 (P6(a2,a2,a8)),
% 96.73/97.30 inference(scs_inference,[],[355,1225,1242,4306,4777,4082,4806,4847,4622,4286,4766,4644,918,784,14,645,50,102,51,38,52,32,15,29,37,39,17,99,28,27,70,20,36,22,69,31,71,23,30,94,49,47,48,46,33])).
% 96.73/97.30 cnf(4954,plain,
% 96.73/97.30 (P1(f77(a2,a2),a2)),
% 96.73/97.30 inference(scs_inference,[],[355,1225,1242,4306,4777,4082,4806,4796,4847,4622,4286,4766,4772,4644,918,784,14,645,50,102,51,38,52,32,15,29,37,39,17,99,28,27,70,20,36,22,69,31,71,23,30,94,49,47,48,46,33,43,44,34,81])).
% 96.73/97.30 cnf(4958,plain,
% 96.73/97.30 (P1(f76(a2,a2),a2)),
% 96.73/97.30 inference(scs_inference,[],[355,1225,1242,4306,4777,4082,4806,4796,4847,4622,4286,4766,4772,4644,918,784,14,645,50,102,51,38,52,32,15,29,37,39,17,99,28,27,70,20,36,22,69,31,71,23,30,94,49,47,48,46,33,43,44,34,81,45,80])).
% 96.73/97.30 cnf(4963,plain,
% 96.73/97.30 (~P6(a2,a58,a74)),
% 96.73/97.30 inference(scs_inference,[],[355,1225,1242,4306,4777,4082,4806,4796,4847,4392,4415,4622,4286,4766,4772,4644,918,784,14,645,50,102,51,38,52,32,15,29,37,39,17,99,28,27,70,20,36,22,69,31,71,23,30,94,49,47,48,46,33,43,44,34,81,45,80,91,1292])).
% 96.73/97.30 cnf(4965,plain,
% 96.73/97.30 (P1(f75(a2,a2),a2)),
% 96.73/97.30 inference(scs_inference,[],[355,1225,1242,4306,4777,4082,4806,4796,4847,4392,4415,4622,4286,4766,4772,4644,918,784,14,645,50,102,51,38,52,32,15,29,37,39,17,99,28,27,70,20,36,22,69,31,71,23,30,94,49,47,48,46,33,43,44,34,81,45,80,91,1292,53])).
% 96.73/97.30 cnf(4967,plain,
% 96.73/97.30 (P1(f4(a2),a2)),
% 96.73/97.30 inference(scs_inference,[],[355,1225,1242,4306,4777,4082,4806,4796,4847,4392,4415,4622,4286,4766,4772,4644,918,784,14,645,50,102,51,38,52,32,15,29,37,39,17,99,28,27,70,20,36,22,69,31,71,23,30,94,49,47,48,46,33,43,44,34,81,45,80,91,1292,53,21])).
% 96.73/97.30 cnf(4969,plain,
% 96.73/97.30 (P6(a69,a58,a9)),
% 96.73/97.30 inference(scs_inference,[],[355,1225,1242,4306,4777,4082,4806,4796,4847,4392,4415,4622,4286,4766,4772,4644,918,784,14,645,584,50,102,51,38,52,32,15,29,37,39,17,99,28,27,70,20,36,22,69,31,71,23,30,94,49,47,48,46,33,43,44,34,81,45,80,91,1292,53,21,40])).
% 96.73/97.30 cnf(4986,plain,
% 96.73/97.30 (~P6(a71,x49861,a85)),
% 96.73/97.30 inference(scs_inference,[],[363,1276,4934,4969,7,102,50,51,65,38])).
% 96.73/97.30 cnf(4992,plain,
% 96.73/97.30 (~P6(a71,x49921,a89)),
% 96.73/97.30 inference(scs_inference,[],[363,1276,1596,4934,4969,4298,7,102,50,51,65,38,52,15,39])).
% 96.73/97.30 cnf(4996,plain,
% 96.73/97.30 (~P6(a71,x49961,a83)),
% 96.73/97.30 inference(scs_inference,[],[363,1276,1596,4934,4969,4918,4298,7,102,50,51,65,38,52,15,39,32,37])).
% 96.73/97.30 cnf(5018,plain,
% 96.73/97.30 (P6(x50181,a71,a80)),
% 96.73/97.30 inference(scs_inference,[],[363,1274,1276,1596,4934,4969,4649,4918,4542,4298,7,102,50,51,65,38,52,15,39,32,37,27,29,17,20,99,28,36,70,31,71,22])).
% 96.73/97.30 cnf(5022,plain,
% 96.73/97.30 (P6(a71,x50221,a86)),
% 96.73/97.30 inference(scs_inference,[],[363,1274,1276,1596,1600,4934,4969,4649,4918,4542,4298,7,102,50,51,65,38,52,15,39,32,37,27,29,17,20,99,28,36,70,31,71,22,69,23])).
% 96.73/97.30 cnf(5026,plain,
% 96.73/97.30 (P1(f52(a59,a2),a2)),
% 96.73/97.30 inference(scs_inference,[],[363,1274,1276,1596,1600,4934,4922,4969,4649,4918,4542,4298,7,102,50,51,65,38,52,15,39,32,37,27,29,17,20,99,28,36,70,31,71,22,69,23,30,79])).
% 96.73/97.30 cnf(5029,plain,
% 96.73/97.30 (~P2(a8,a84)),
% 96.73/97.30 inference(scs_inference,[],[363,1274,1276,1596,1600,4934,4474,4922,4946,4969,4649,4918,4542,4298,7,102,50,51,65,38,52,15,39,32,37,27,29,17,20,99,28,36,70,31,71,22,69,23,30,79,94])).
% 96.73/97.30 cnf(5043,plain,
% 96.73/97.30 (~P1(x50431,f46(a88,a88))),
% 96.73/97.30 inference(rename_variables,[],[918])).
% 96.73/97.30 cnf(5060,plain,
% 96.73/97.30 (P1(f76(a71,a71),a71)),
% 96.73/97.30 inference(scs_inference,[],[363,1274,1276,1596,1600,4934,4474,4904,4922,4930,4946,4969,4649,4758,4918,4542,4298,4384,7,4186,4777,918,5043,102,50,51,65,38,52,15,39,32,37,27,29,17,20,99,28,36,70,31,71,22,69,23,30,79,94,41,49,78,47,48,46,34,44,43,33,81,45,80])).
% 96.73/97.30 cnf(5066,plain,
% 96.73/97.30 (~P1(x50661,a58)),
% 96.73/97.30 inference(rename_variables,[],[14])).
% 96.73/97.30 cnf(5068,plain,
% 96.73/97.30 (~P6(a71,a58,a74)),
% 96.73/97.30 inference(scs_inference,[],[363,1274,1276,1596,1600,4934,4474,4904,4906,4922,4930,4946,4963,4969,4649,4758,4965,4918,4542,4298,4384,9,7,4186,4777,918,5043,14,102,50,51,65,38,52,15,39,32,37,27,29,17,20,99,28,36,70,31,71,22,69,23,30,79,94,41,49,78,47,48,46,34,44,43,33,81,45,80,74,96,1292])).
% 96.73/97.30 cnf(5072,plain,
% 96.73/97.30 (P1(f4(a71),a71)),
% 96.73/97.30 inference(scs_inference,[],[363,1274,1276,1596,1600,4934,4474,4904,4906,4922,4930,4946,4963,4969,4649,4758,4965,4918,4542,4298,4384,9,7,4186,4777,918,5043,14,102,50,51,65,38,52,15,39,32,37,27,29,17,20,99,28,36,70,31,71,22,69,23,30,79,94,41,49,78,47,48,46,34,44,43,33,81,45,80,74,96,1292,54,21])).
% 96.73/97.30 cnf(5074,plain,
% 96.73/97.30 (P1(f72(a58,a2),a2)),
% 96.73/97.30 inference(scs_inference,[],[363,1274,1276,1596,1600,4934,4474,4904,4906,4922,4930,4946,4963,4969,4649,4758,4965,4918,4542,4298,239,4384,9,7,4186,4777,918,5043,14,5066,102,50,51,65,38,52,15,39,32,37,27,29,17,20,99,28,36,70,31,71,22,69,23,30,79,94,41,49,78,47,48,46,34,44,43,33,81,45,80,74,96,1292,54,21,76])).
% 96.73/97.30 cnf(5103,plain,
% 96.73/97.30 (~P1(f76(a69,a69),f79(a69))),
% 96.73/97.30 inference(scs_inference,[],[370,1616,1649,4412,4764,4095,4301,654,645,102,50,51,38,52,32,39,29,37,15,17,20])).
% 96.73/97.30 cnf(5105,plain,
% 96.73/97.30 (~P6(f48(a84,a84),x51051,a5)),
% 96.73/97.30 inference(scs_inference,[],[370,1616,1649,4412,4764,4095,4301,654,645,102,50,51,38,52,32,39,29,37,15,17,20,36])).
% 96.73/97.30 cnf(5117,plain,
% 96.73/97.30 (~P6(a58,x51171,a84)),
% 96.73/97.30 inference(scs_inference,[],[370,1616,1618,1649,1651,4412,4764,4095,4301,654,14,645,102,50,51,38,52,32,39,29,37,15,17,20,36,99,28,70,71,69,31])).
% 96.73/97.30 cnf(5126,plain,
% 96.73/97.30 (P6(x51261,a71,a80)),
% 96.73/97.30 inference(rename_variables,[],[5018])).
% 96.73/97.30 cnf(5128,plain,
% 96.73/97.30 (~P6(a69,a71,a91)),
% 96.73/97.30 inference(scs_inference,[],[370,1616,1618,1649,1651,4412,5018,4764,4095,4301,12,6,654,14,645,102,50,51,38,52,32,39,29,37,15,17,20,36,99,28,70,71,69,31,22,30,23,79,49])).
% 96.73/97.30 cnf(5130,plain,
% 96.73/97.30 (~P2(a80,a85)),
% 96.73/97.30 inference(scs_inference,[],[370,1616,1618,1649,1651,4412,4894,5018,5126,4764,4095,4301,12,6,654,14,645,102,50,51,38,52,32,39,29,37,15,17,20,36,99,28,70,71,69,31,22,30,23,79,49,94])).
% 96.73/97.30 cnf(5134,plain,
% 96.73/97.30 (P1(f32(a71,a69),a71)),
% 96.73/97.30 inference(scs_inference,[],[370,1616,1618,1649,1651,4412,4894,4996,5018,5126,4764,4095,4301,12,6,654,14,645,102,50,51,38,52,32,39,29,37,15,17,20,36,99,28,70,71,69,31,22,30,23,79,49,94,41])).
% 96.73/97.30 cnf(5137,plain,
% 96.73/97.30 (P1(f29(a71,a69),a71)),
% 96.73/97.30 inference(scs_inference,[],[370,1616,1618,1649,1651,4412,4894,4996,5018,5126,5022,4764,4095,4301,12,6,654,14,645,102,50,51,38,52,32,39,29,37,15,17,20,36,99,28,70,71,69,31,22,30,23,79,49,94,41,78])).
% 96.73/97.30 cnf(5144,plain,
% 96.73/97.30 (P3(a80,a8)),
% 96.73/97.30 inference(scs_inference,[],[370,1616,1618,1649,1651,4752,4412,4894,4996,5018,5126,5022,4764,4095,4301,4713,1782,12,4190,6,654,14,645,102,50,51,38,52,32,39,29,37,15,17,20,36,99,28,70,71,69,31,22,30,23,79,49,94,41,78,47,48,100])).
% 96.73/97.30 cnf(5145,plain,
% 96.73/97.30 (P6(x51451,a69,a80)),
% 96.73/97.30 inference(rename_variables,[],[4713])).
% 96.73/97.30 cnf(5152,plain,
% 96.73/97.30 (~P1(x51521,f46(a88,a88))),
% 96.73/97.30 inference(rename_variables,[],[918])).
% 96.73/97.30 cnf(5156,plain,
% 96.73/97.30 (~P5(a80,a8)),
% 96.73/97.30 inference(scs_inference,[],[370,1616,1618,1649,1651,4752,4412,4894,4996,5018,5126,5022,4764,4967,4095,4301,4713,5145,1782,4045,12,5,10,4190,6,654,918,14,645,102,50,51,38,52,32,39,29,37,15,17,20,36,99,28,70,71,69,31,22,30,23,79,49,94,41,78,47,48,100,44,34,46,33,104])).
% 96.73/97.30 cnf(5157,plain,
% 96.73/97.30 (P6(x51571,a69,a80)),
% 96.73/97.30 inference(rename_variables,[],[4713])).
% 96.73/97.30 cnf(5163,plain,
% 96.73/97.30 (P1(x51631,f48(a84,a84))),
% 96.73/97.30 inference(rename_variables,[],[654])).
% 96.73/97.30 cnf(5171,plain,
% 96.73/97.30 (P1(f35(a71,a62),a71)),
% 96.73/97.30 inference(scs_inference,[],[370,1616,1618,1649,1651,4752,4412,4894,4992,4996,5018,5126,5022,4764,4967,4095,4301,4713,5145,5157,1782,4045,12,5,10,4190,6,654,5163,918,5152,14,645,102,50,51,38,52,32,39,29,37,15,17,20,36,99,28,70,71,69,31,22,30,23,79,49,94,41,78,47,48,100,44,34,46,33,104,105,43,81,45,74])).
% 96.73/97.30 cnf(5193,plain,
% 96.73/97.30 (~P1(f76(a2,a2),f79(a2))),
% 96.73/97.30 inference(scs_inference,[],[373,1731,1742,4733,4958,4310,4062,8,102,51,50,38,52,15,17,20])).
% 96.73/97.30 cnf(5199,plain,
% 96.73/97.30 (~P6(a3,x51991,a5)),
% 96.73/97.30 inference(scs_inference,[],[373,1731,1742,4733,4958,4310,4062,8,584,102,51,50,38,52,15,17,20,39,37,36])).
% 96.73/97.30 cnf(5209,plain,
% 96.73/97.30 (P6(x52091,a3,a80)),
% 96.73/97.30 inference(scs_inference,[],[373,1731,1735,1742,4733,4958,4310,4062,8,584,102,51,50,38,52,15,17,20,39,37,36,70,99,28,71,22])).
% 96.73/97.30 cnf(5215,plain,
% 96.73/97.30 (P6(a3,x52151,a86)),
% 96.73/97.30 inference(scs_inference,[],[373,1731,1735,1742,1744,4733,4958,4310,4062,645,8,584,102,51,50,38,52,15,17,20,39,37,36,70,99,28,71,22,69,31,23])).
% 96.73/97.30 cnf(5224,plain,
% 96.73/97.30 (~P2(a82,a85)),
% 96.73/97.30 inference(scs_inference,[],[373,1731,1735,1742,1744,4733,4525,4958,5103,4454,4310,4062,4388,4764,645,8,584,102,51,50,38,52,15,17,20,39,37,36,70,99,28,71,22,69,31,23,30,79,49,94])).
% 96.73/97.30 cnf(5278,plain,
% 96.73/97.30 (~P1(f76(a71,a71),f79(a71))),
% 96.73/97.30 inference(scs_inference,[],[383,1149,4613,5060,584,102,50,51,38,20])).
% 96.73/97.30 cnf(5280,plain,
% 96.73/97.30 (P1(f23(a62,a3),f79(a62))),
% 96.73/97.30 inference(scs_inference,[],[383,1149,4613,5060,4089,584,102,50,51,38,20,17])).
% 96.73/97.30 cnf(5284,plain,
% 96.73/97.30 (P1(f35(a62,a62),a65)),
% 96.73/97.30 inference(scs_inference,[],[383,1149,4613,5060,4340,4089,584,102,50,51,38,20,17,29,15])).
% 96.73/97.30 cnf(5294,plain,
% 96.73/97.30 (P6(x52941,f79(a58),a80)),
% 96.73/97.30 inference(scs_inference,[],[383,1149,1153,4613,5060,4340,4089,584,102,50,51,38,20,17,29,15,52,70,36,99,22])).
% 96.73/97.30 cnf(5308,plain,
% 96.73/97.30 (P6(a71,a58,a9)),
% 96.73/97.30 inference(scs_inference,[],[383,1149,1153,4613,5060,5193,4340,4089,584,102,50,51,38,20,17,29,15,52,70,36,99,22,28,71,31,23,69,30,40])).
% 96.73/97.30 cnf(5320,plain,
% 96.73/97.30 (P1(x53201,f48(a84,a84))),
% 96.73/97.30 inference(rename_variables,[],[654])).
% 96.73/97.30 cnf(5340,plain,
% 96.73/97.30 (P1(f38(a71,a58),a71)),
% 96.73/97.30 inference(scs_inference,[],[383,1149,1153,5068,5199,5209,4613,5060,5193,4340,4089,4232,5103,4764,4958,654,5320,918,14,584,102,50,51,38,20,17,29,15,52,70,36,99,22,28,71,31,23,69,30,40,49,94,48,34,44,46,47,33,43,45,96,1296,65])).
% 96.73/97.30 cnf(5346,plain,
% 96.73/97.30 (~P1(f14(a71,a65),a65)),
% 96.73/97.30 inference(scs_inference,[],[383,1149,1153,5068,5199,5209,4613,5060,5193,4340,4089,4362,4232,5103,4764,4958,654,5320,918,14,584,102,50,51,38,20,17,29,15,52,70,36,99,22,28,71,31,23,69,30,40,49,94,48,34,44,46,47,33,43,45,96,1296,65,27,32,77])).
% 96.73/97.30 cnf(5349,plain,
% 96.73/97.30 (P1(f29(a56,a71),a56)),
% 96.73/97.30 inference(scs_inference,[],[383,1149,1153,5068,5199,5209,4613,5060,5193,4340,4089,4362,4386,4232,5103,4764,4958,654,5320,918,14,584,102,50,51,38,20,17,29,15,52,70,36,99,22,28,71,31,23,69,30,40,49,94,48,34,44,46,47,33,43,45,96,1296,65,27,32,77,78])).
% 96.73/97.30 cnf(5364,plain,
% 96.73/97.30 (~P1(f38(a71,a58),f79(a71))),
% 96.73/97.30 inference(scs_inference,[],[387,1117,5130,5340,102,50,51,52,20])).
% 96.73/97.30 cnf(5366,plain,
% 96.73/97.30 (P1(f14(a71,a65),f79(a65))),
% 96.73/97.30 inference(scs_inference,[],[387,1117,5130,5340,5346,102,50,51,52,20,17])).
% 96.73/97.30 cnf(5380,plain,
% 96.73/97.30 (~P2(a9,a85)),
% 96.73/97.30 inference(scs_inference,[],[387,1117,1121,5130,4986,5308,5278,5340,5346,5060,102,50,51,52,20,17,70,99,71,31,69,49,94])).
% 96.73/97.30 cnf(5387,plain,
% 96.73/97.30 (P1(x53871,f48(a84,a84))),
% 96.73/97.30 inference(rename_variables,[],[654])).
% 96.73/97.30 cnf(5391,plain,
% 96.73/97.30 (~P6(a65,a62,a90)),
% 96.73/97.30 inference(scs_inference,[],[387,1117,1121,5130,4986,5308,5278,5280,5340,5346,5,10,5060,654,5387,784,102,50,51,52,20,17,70,99,71,31,69,49,94,48,34,33,47])).
% 96.73/97.30 cnf(5422,plain,
% 96.73/97.30 (P1(f22(a65,a62),f79(a62))),
% 96.73/97.30 inference(scs_inference,[],[397,887,5029,4114,50,102,51,52,17])).
% 96.73/97.30 cnf(5424,plain,
% 96.73/97.30 (~P1(f35(a62,a62),f79(a65))),
% 96.73/97.30 inference(scs_inference,[],[397,887,5029,5284,4114,50,102,51,52,17,20])).
% 96.73/97.30 cnf(5436,plain,
% 96.73/97.30 (~P2(a86,a91)),
% 96.73/97.30 inference(scs_inference,[],[397,887,1000,5029,5128,5284,4114,4711,1547,11,50,102,51,52,17,20,70,99,71,69,49,94])).
% 96.73/97.30 cnf(5439,plain,
% 96.73/97.30 (~P6(a69,a71,a74)),
% 96.73/97.30 inference(scs_inference,[],[397,887,1000,5029,5128,5284,4114,4711,12,1547,6,11,50,102,51,52,17,20,70,99,71,69,49,94,48])).
% 96.73/97.30 cnf(5442,plain,
% 96.73/97.30 (P1(x54421,f48(a84,a84))),
% 96.73/97.30 inference(rename_variables,[],[654])).
% 96.73/97.30 cnf(5458,plain,
% 96.73/97.30 (P6(f79(a65),a65,a9)),
% 96.73/97.30 inference(scs_inference,[],[397,887,1000,5029,5128,5364,5366,5284,4114,4711,4513,5340,12,1547,6,654,5442,918,11,50,102,51,52,17,20,70,99,71,69,49,94,48,34,33,46,47,44,43,45,40])).
% 96.73/97.30 cnf(5462,plain,
% 96.73/97.30 (P1(f60(a65,a58),a65)),
% 96.73/97.30 inference(scs_inference,[],[292,397,887,1000,5029,5128,5364,5366,5284,4114,4711,4513,576,5340,12,1547,6,654,5442,918,14,11,50,102,51,52,17,20,70,99,71,69,49,94,48,34,33,46,47,44,43,45,40,109,76])).
% 96.73/97.30 cnf(5477,plain,
% 96.73/97.30 (P1(f24(a3,a62),f79(a62))),
% 96.73/97.30 inference(scs_inference,[],[400,997,5224,5462,1569,50,102,51,52,20,17])).
% 96.73/97.30 cnf(5495,plain,
% 96.73/97.30 (~P2(a8,a89)),
% 96.73/97.30 inference(scs_inference,[],[400,892,997,1333,5224,4518,4468,5422,5424,5462,1569,4340,784,8,50,102,51,52,20,17,70,71,99,69,49,48,34,94])).
% 96.73/97.30 cnf(5534,plain,
% 96.73/97.30 (P1(f19(a65,a3),f79(a62))),
% 96.73/97.30 inference(scs_inference,[],[411,1201,2866,5380,5349,1835,50,51,102,52,20,17])).
% 96.73/97.30 cnf(5556,plain,
% 96.73/97.30 (~P2(a80,a90)),
% 96.73/97.30 inference(scs_inference,[],[411,1201,2863,2866,4490,5380,5391,5477,5105,5349,1835,4172,10,5,654,918,50,51,102,52,20,17,70,71,99,69,75,48,34,46,94])).
% 96.73/97.30 cnf(5582,plain,
% 96.73/97.30 (~P6(f49(a78,a87),f50(a78,a87),a87)),
% 96.73/97.30 inference(scs_inference,[],[415,5436,50,102])).
% 96.73/97.30 cnf(5588,plain,
% 96.73/97.30 (P1(f19(a62,a3),f79(a62))),
% 96.73/97.30 inference(scs_inference,[],[415,1210,5436,1786,50,102,51,52,17])).
% 96.73/97.30 cnf(5592,plain,
% 96.73/97.30 (~P1(f4(a59),f79(a59))),
% 96.73/97.30 inference(scs_inference,[],[415,1198,1210,5436,4658,1786,50,102,51,52,17,70,20])).
% 96.73/97.30 cnf(5594,plain,
% 96.73/97.30 (P6(f49(a78,a87),f50(a78,a87),a78)),
% 96.73/97.30 inference(scs_inference,[],[415,1198,1210,5436,4658,1786,50,102,51,52,17,70,20,71])).
% 96.73/97.30 cnf(5603,plain,
% 96.73/97.30 (P6(f79(a62),f79(a58),a82)),
% 96.73/97.30 inference(scs_inference,[],[415,1198,1210,5436,5534,4658,1786,784,584,50,102,51,52,17,70,20,71,99,69,48,34])).
% 96.73/97.30 cnf(5604,plain,
% 96.73/97.30 (P1(x56041,f79(a58))),
% 96.73/97.30 inference(rename_variables,[],[584])).
% 96.73/97.30 cnf(5608,plain,
% 96.73/97.30 (~P2(a86,a8)),
% 96.73/97.30 inference(scs_inference,[],[415,1198,1210,5436,5534,4288,4252,4658,1786,12,6,784,584,50,102,51,52,17,70,20,71,99,69,48,34,46,94])).
% 96.73/97.30 cnf(5610,plain,
% 96.73/97.30 (P6(f79(a58),f79(a62),a8)),
% 96.73/97.30 inference(scs_inference,[],[415,1198,1210,5436,5534,4288,4252,4658,1786,12,6,784,584,5604,50,102,51,52,17,70,20,71,99,69,48,34,46,94,33])).
% 96.73/97.30 cnf(5636,plain,
% 96.73/97.30 (P1(f14(a62,a62),f79(a62))),
% 96.73/97.30 inference(scs_inference,[],[425,3223,5495,4954,4315,50,102,51,20,52,17])).
% 96.73/97.30 cnf(5646,plain,
% 96.73/97.30 (P6(a3,f79(a62),a82)),
% 96.73/97.30 inference(scs_inference,[],[425,3220,3223,5495,5588,4954,4315,8,50,102,51,20,52,17,70,71,99,69,34])).
% 96.73/97.30 cnf(5647,plain,
% 96.73/97.30 (P1(x56471,a3)),
% 96.73/97.30 inference(rename_variables,[],[8])).
% 96.73/97.30 cnf(5652,plain,
% 96.73/97.30 (~P2(a80,a74)),
% 96.73/97.30 inference(scs_inference,[],[425,3220,3223,5439,5495,5588,4954,5018,4315,784,8,50,102,51,20,52,17,70,71,99,69,34,48,94])).
% 96.73/97.30 cnf(5656,plain,
% 96.73/97.30 (P1(x56561,f48(a84,a84))),
% 96.73/97.30 inference(rename_variables,[],[654])).
% 96.73/97.30 cnf(5665,plain,
% 96.73/97.30 (P3(a80,a82)),
% 96.73/97.30 inference(scs_inference,[],[425,3220,3223,5439,5495,5588,5592,5603,5294,4954,5018,5346,4315,5366,654,5656,784,8,5647,50,102,51,20,52,17,70,71,99,69,34,48,94,46,33,43,44,100])).
% 96.73/97.30 cnf(5666,plain,
% 96.73/97.30 (P6(x56661,f79(a58),a80)),
% 96.73/97.30 inference(rename_variables,[],[5294])).
% 96.73/97.30 cnf(5668,plain,
% 96.73/97.30 (~P5(a80,a82)),
% 96.73/97.30 inference(scs_inference,[],[425,3220,3223,5439,5495,5588,5592,5603,5294,5666,4954,5018,5346,4315,5366,654,5656,784,8,5647,50,102,51,20,52,17,70,71,99,69,34,48,94,46,33,43,44,100,104])).
% 96.73/97.30 cnf(5691,plain,
% 96.73/97.30 (~P6(f49(a78,a91),f50(a78,a91),a91)),
% 96.73/97.30 inference(scs_inference,[],[429,5556,50,102])).
% 96.73/97.30 cnf(5695,plain,
% 96.73/97.30 (~P1(f4(a71),f79(a71))),
% 96.73/97.30 inference(scs_inference,[],[429,3770,5556,5072,50,102,51,20])).
% 96.73/97.30 cnf(5697,plain,
% 96.73/97.30 (P1(f26(a62,a3),f79(a62))),
% 96.73/97.30 inference(scs_inference,[],[429,3770,5556,5072,4180,50,102,51,20,17])).
% 96.73/97.30 cnf(5703,plain,
% 96.73/97.30 (P6(f49(a78,a91),f50(a78,a91),a78)),
% 96.73/97.30 inference(scs_inference,[],[429,3764,3770,5556,5072,4180,50,102,51,20,17,52,70,71])).
% 96.73/97.30 cnf(5710,plain,
% 96.73/97.30 (~P1(x57101,f46(a88,a88))),
% 96.73/97.30 inference(rename_variables,[],[918])).
% 96.73/97.30 cnf(5713,plain,
% 96.73/97.30 (~P1(x57131,f46(a88,a88))),
% 96.73/97.30 inference(rename_variables,[],[918])).
% 96.73/97.30 cnf(5715,plain,
% 96.73/97.30 (~P2(a78,a87)),
% 96.73/97.30 inference(scs_inference,[],[429,3764,3770,5556,5594,5636,5582,5072,4180,918,5710,50,102,51,20,17,52,70,71,99,69,48,46,94])).
% 96.73/97.30 cnf(5720,plain,
% 96.73/97.30 (P6(f79(a62),a62,a9)),
% 96.73/97.30 inference(scs_inference,[],[429,3764,3770,5556,5594,5636,5582,5072,4180,918,5710,5713,50,102,51,20,17,52,70,71,99,69,48,46,94,43,40])).
% 96.73/97.30 cnf(5724,plain,
% 96.73/97.30 (P1(f72(a58,a62),a62)),
% 96.73/97.30 inference(scs_inference,[],[304,429,3764,3770,5556,5594,5636,5582,5072,568,4180,918,5710,5713,14,50,102,51,20,17,52,70,71,99,69,48,46,94,43,40,109,76])).
% 96.73/97.30 cnf(5731,plain,
% 96.73/97.30 (~P6(f49(a10,a74),f50(a10,a74),a74)),
% 96.73/97.30 inference(scs_inference,[],[442,5608,50,102])).
% 96.73/97.30 cnf(5739,plain,
% 96.73/97.30 (P1(f39(a58,a62),f79(a62))),
% 96.73/97.30 inference(scs_inference,[],[442,3783,5608,5724,4037,50,102,51,20,52,17])).
% 96.73/97.30 cnf(5743,plain,
% 96.73/97.30 (P6(f49(a10,a74),f50(a10,a74),a10)),
% 96.73/97.30 inference(scs_inference,[],[442,3777,3783,5608,5724,4037,50,102,51,20,52,17,70,71])).
% 96.73/97.30 cnf(5758,plain,
% 96.73/97.30 (~P2(a9,a90)),
% 96.73/97.30 inference(scs_inference,[],[442,3777,3783,5608,4053,5697,5695,5724,5720,4037,654,918,645,584,50,102,51,20,52,17,70,71,69,99,81,48,46,94])).
% 96.73/97.30 cnf(5776,plain,
% 96.73/97.30 (~P1(f32(a71,a69),f79(a71))),
% 96.73/97.30 inference(scs_inference,[],[445,3796,5652,5134,50,51,102,20])).
% 96.73/97.30 cnf(5795,plain,
% 96.73/97.30 (~P1(x57951,f45(a5,a5))),
% 96.73/97.30 inference(rename_variables,[],[784])).
% 96.73/97.30 cnf(5800,plain,
% 96.73/97.30 (~P2(a78,a91)),
% 96.73/97.30 inference(scs_inference,[],[445,3790,3796,4492,5117,5652,5739,5703,5691,5134,4433,4117,784,5795,50,51,102,20,17,52,70,71,69,99,75,48,46,94])).
% 96.73/97.30 cnf(5819,plain,
% 96.73/97.30 (~P1(f29(a71,a69),f79(a71))),
% 96.73/97.30 inference(scs_inference,[],[500,3805,5715,5137,50,102,51,20])).
% 96.73/97.30 cnf(5821,plain,
% 96.73/97.30 (P1(f12(a62,a3),f79(a62))),
% 96.73/97.30 inference(scs_inference,[],[500,3805,5715,5137,4235,50,102,51,20,17])).
% 96.73/97.30 cnf(5836,plain,
% 96.73/97.30 (~P2(a80,a10)),
% 96.73/97.30 inference(scs_inference,[],[500,3802,3805,5715,4219,5776,4027,5137,4235,8,50,102,51,20,17,70,52,71,69,99,46,94])).
% 96.73/97.30 cnf(5854,plain,
% 96.73/97.30 (~P1(f35(a71,a62),f79(a71))),
% 96.73/97.30 inference(scs_inference,[],[504,5758,5171,50,102,20])).
% 96.73/97.30 cnf(5858,plain,
% 96.73/97.30 (P1(f23(a65,a3),f79(a65))),
% 96.73/97.30 inference(scs_inference,[],[504,2852,5758,5171,4662,50,102,20,51,17])).
% 96.73/97.30 cnf(5870,plain,
% 96.73/97.30 (P3(a86,a82)),
% 96.73/97.30 inference(scs_inference,[],[504,2849,2852,5758,5646,5215,5171,4662,50,102,20,51,17,52,70,71,69,99,100])).
% 96.73/97.30 cnf(5871,plain,
% 96.73/97.30 (P6(a3,x58711,a86)),
% 96.73/97.30 inference(rename_variables,[],[5215])).
% 96.73/97.30 cnf(5873,plain,
% 96.73/97.30 (~P5(a86,a82)),
% 96.73/97.30 inference(scs_inference,[],[504,2849,2852,5758,5646,5215,5871,5171,4662,50,102,20,51,17,52,70,71,69,99,100,104])).
% 96.73/97.30 cnf(5874,plain,
% 96.73/97.30 (P6(a3,x58741,a86)),
% 96.73/97.30 inference(rename_variables,[],[5215])).
% 96.73/97.30 cnf(5880,plain,
% 96.73/97.30 (P1(x58801,f79(a58))),
% 96.73/97.30 inference(rename_variables,[],[584])).
% 96.73/97.30 cnf(5890,plain,
% 96.73/97.30 (~P2(a8,a87)),
% 96.73/97.30 inference(scs_inference,[],[504,2849,2852,5758,5610,5821,4274,5819,5646,5215,5871,5874,5171,4662,654,14,584,5880,50,102,20,51,17,52,70,71,69,99,100,104,105,34,33,44,46,94])).
% 96.73/97.30 cnf(5893,plain,
% 96.73/97.30 (~P6(f79(a2),a2,a78)),
% 96.73/97.30 inference(scs_inference,[],[504,2849,2852,5758,5610,5821,4274,5819,5646,5215,5871,5874,5171,4796,4662,4772,654,14,584,5880,50,102,20,51,17,52,70,71,69,99,100,104,105,34,33,44,46,94,43])).
% 96.73/97.30 cnf(5907,plain,
% 96.73/97.30 (~P1(f72(a58,a59),f79(a59))),
% 96.73/97.30 inference(scs_inference,[],[511,2878,5800,4651,4513,50,17,51,102,20])).
% 96.73/97.30 cnf(5919,plain,
% 96.73/97.30 (P6(f79(a71),a71,a9)),
% 96.73/97.30 inference(scs_inference,[],[511,2875,2878,5800,4908,4651,4513,50,17,51,102,20,70,52,71,69,99,40])).
% 96.73/97.30 cnf(5922,plain,
% 96.73/97.30 (P1(x59221,f48(a84,a84))),
% 96.73/97.30 inference(rename_variables,[],[654])).
% 96.73/97.30 cnf(5929,plain,
% 96.73/97.30 (P1(f60(a62,a58),a62)),
% 96.73/97.30 inference(scs_inference,[],[511,2875,2878,5800,5858,4908,4651,571,4513,654,5922,918,14,50,17,51,102,20,70,52,71,69,99,40,34,48,33,76])).
% 96.73/97.30 cnf(5930,plain,
% 96.73/97.30 (~P1(x59301,a58)),
% 96.73/97.30 inference(rename_variables,[],[14])).
% 96.73/97.30 cnf(5935,plain,
% 96.73/97.30 (~P2(a80,a91)),
% 96.73/97.30 inference(scs_inference,[],[511,2875,2878,5800,4313,5854,5858,4908,4651,4027,571,4513,654,5922,918,14,584,50,17,51,102,20,70,52,71,69,99,40,34,48,33,76,46,94])).
% 96.73/97.30 cnf(5940,plain,
% 96.73/97.30 (P1(x59401,a59)+P1(f19(a59,a58),a59)),
% 96.73/97.30 inference(scs_inference,[],[511,4654,2875,2878,5800,4313,5854,5858,4908,4651,4027,571,4513,1750,4296,654,5922,918,14,5930,584,50,17,51,102,20,70,52,71,69,99,40,34,48,33,76,46,94,43,96])).
% 96.73/97.30 cnf(5945,plain,
% 96.73/97.30 (P1(f19(a59,a58),a59)),
% 96.73/97.30 inference(factoring_inference,[],[5940])).
% 96.73/97.30 cnf(5948,plain,
% 96.73/97.30 (~P1(f19(a59,a58),f79(a59))),
% 96.73/97.30 inference(scs_inference,[],[5836,5945,50,20])).
% 96.73/97.30 cnf(5950,plain,
% 96.73/97.30 (P1(f26(a65,a3),f79(a62))),
% 96.73/97.30 inference(scs_inference,[],[5836,5945,1782,50,20,17])).
% 96.73/97.30 cnf(5966,plain,
% 96.73/97.30 (P1(f52(a59,a56),a56)),
% 96.73/97.30 inference(scs_inference,[],[517,2944,2947,5836,5945,4388,1782,50,20,17,102,51,70,52,71,69,99,79])).
% 96.73/97.30 cnf(5970,plain,
% 96.73/97.30 (P1(x59701,f48(a84,a84))),
% 96.73/97.30 inference(rename_variables,[],[654])).
% 96.73/97.30 cnf(5973,plain,
% 96.73/97.30 (~P1(x59731,f45(a5,a5))),
% 96.73/97.30 inference(rename_variables,[],[784])).
% 96.73/97.30 cnf(5976,plain,
% 96.73/97.30 (P1(x59761,f48(a84,a84))),
% 96.73/97.30 inference(rename_variables,[],[654])).
% 96.73/97.30 cnf(5981,plain,
% 96.73/97.30 (~P1(x59811,f45(a5,a5))),
% 96.73/97.30 inference(rename_variables,[],[784])).
% 96.73/97.30 cnf(5983,plain,
% 96.73/97.30 (~P2(a10,a74)),
% 96.73/97.30 inference(scs_inference,[],[517,2944,2947,5836,5945,5907,5743,5731,5074,4388,1782,654,5970,5976,784,5973,50,20,17,102,51,70,52,71,69,99,79,34,48,45,33,46,94])).
% 96.73/97.30 cnf(5988,plain,
% 96.73/97.30 (P1(f32(a56,a59),a56)),
% 96.73/97.30 inference(scs_inference,[],[517,2944,2947,5836,5945,5907,5743,5731,5074,4394,4388,1782,654,5970,5976,784,5973,5981,50,20,17,102,51,70,52,71,69,99,79,34,48,45,33,46,94,43,41])).
% 96.73/97.30 cnf(5991,plain,
% 96.73/97.30 (~P1(f14(a59,a2),a2)),
% 96.73/97.30 inference(scs_inference,[],[517,2944,2947,5836,5945,5907,5743,5731,5074,4394,4464,4388,1782,654,5970,5976,784,5973,5981,50,20,17,102,51,70,52,71,69,99,79,34,48,45,33,46,94,43,41,77])).
% 96.73/97.30 cnf(5994,plain,
% 96.73/97.30 (P1(f29(a71,a59),a71)),
% 96.73/97.30 inference(scs_inference,[],[517,2944,2947,5836,5945,5907,5743,5731,5074,4394,4464,5022,4388,1782,654,5970,5976,784,5973,5981,50,20,17,102,51,70,52,71,69,99,79,34,48,45,33,46,94,43,41,77,78])).
% 96.73/97.30 cnf(6010,plain,
% 96.73/97.30 (~P6(f49(a78,a88),f50(a78,a88),a88)),
% 96.73/97.30 inference(scs_inference,[],[536,5890,50,102])).
% 96.73/97.30 cnf(6012,plain,
% 96.73/97.30 (P1(f14(a59,a2),f79(a2))),
% 96.73/97.30 inference(scs_inference,[],[536,5890,5991,50,102,17])).
% 96.73/97.30 cnf(6014,plain,
% 96.73/97.30 (~P1(f52(a59,a56),f79(a56))),
% 96.73/97.30 inference(scs_inference,[],[536,5890,5966,5991,50,102,17,20])).
% 96.73/97.30 cnf(6022,plain,
% 96.73/97.30 (P6(f49(a78,a88),f50(a78,a88),a78)),
% 96.73/97.30 inference(scs_inference,[],[536,4646,4669,5890,5966,5991,50,102,17,20,51,70,52,71])).
% 96.73/97.30 cnf(6031,plain,
% 96.73/97.30 (~P2(a9,a91)),
% 96.73/97.30 inference(scs_inference,[],[536,4646,4669,5890,4511,5948,5966,5991,5458,8,50,102,17,20,51,70,52,71,99,69,46,94])).
% 96.73/97.30 cnf(6048,plain,
% 96.73/97.30 (~P6(f49(a10,a83),f50(a10,a83),a83)),
% 96.73/97.30 inference(scs_inference,[],[555,5935,50,102])).
% 96.73/97.30 cnf(6050,plain,
% 96.73/97.30 (P1(f39(a58,a65),f79(a62))),
% 96.73/97.30 inference(scs_inference,[],[555,5935,1750,50,102,17])).
% 96.73/97.30 cnf(6060,plain,
% 96.73/97.30 (P6(f49(a10,a83),f50(a10,a83),a10)),
% 96.73/97.30 inference(scs_inference,[],[555,2933,2936,5935,5994,1750,50,102,17,20,51,52,70,71])).
% 96.73/97.30 cnf(6067,plain,
% 96.73/97.30 (~P1(x60671,f46(a88,a88))),
% 96.73/97.30 inference(rename_variables,[],[918])).
% 96.73/97.30 cnf(6070,plain,
% 96.73/97.30 (P1(x60701,f48(a84,a84))),
% 96.73/97.30 inference(rename_variables,[],[654])).
% 96.73/97.30 cnf(6077,plain,
% 96.73/97.30 (~P2(a78,a88)),
% 96.73/97.30 inference(scs_inference,[],[555,2933,2936,5935,6012,6022,6010,5994,1750,654,6070,918,6067,50,102,17,20,51,52,70,71,69,99,48,34,33,46,94])).
% 96.73/97.30 cnf(6079,plain,
% 96.73/97.30 (~P6(f79(a62),a65,a78)),
% 96.73/97.30 inference(scs_inference,[],[555,2933,2936,5935,6012,6022,6010,5994,5950,4023,1750,654,6070,918,6067,50,102,17,20,51,52,70,71,69,99,48,34,33,46,94,43])).
% 96.73/97.30 cnf(6082,plain,
% 96.73/97.30 (~P6(f49(a10,a89),f50(a10,a89),a89)),
% 96.73/97.30 inference(scs_inference,[],[559,102])).
% 96.73/97.30 cnf(6086,plain,
% 96.73/97.30 (P1(f40(a65,a58),f79(a65))),
% 96.73/97.30 inference(scs_inference,[],[559,6077,4333,102,50,17])).
% 96.73/97.30 cnf(6096,plain,
% 96.73/97.30 (P6(f49(a10,a89),f50(a10,a89),a10)),
% 96.73/97.30 inference(scs_inference,[],[559,6077,4086,5156,5988,4333,102,50,17,20,51,70,52,71])).
% 96.73/97.30 cnf(6103,plain,
% 96.73/97.30 (~P1(x61031,f45(a5,a5))),
% 96.73/97.30 inference(rename_variables,[],[784])).
% 96.73/97.30 cnf(6108,plain,
% 96.73/97.30 (~P2(a86,a78)),
% 96.73/97.30 inference(scs_inference,[],[559,6077,4086,5156,5893,4824,5988,4841,4333,784,6103,102,50,17,20,51,70,52,71,69,99,48,46,94])).
% 96.73/97.30 cnf(6111,plain,
% 96.73/97.30 (~P6(f79(a2),a2,a73)),
% 96.73/97.30 inference(scs_inference,[],[13,559,6077,4086,5156,5893,4824,5988,4841,4333,784,6103,102,50,17,20,51,70,52,71,69,99,48,46,94,91])).
% 96.73/97.30 cnf(6113,plain,
% 96.73/97.30 (~P6(a62,f79(a65),a78)),
% 96.73/97.30 inference(scs_inference,[],[13,559,6077,4086,5156,5893,4824,5988,4841,5929,4017,4333,784,6103,102,50,17,20,51,70,52,71,69,99,48,46,94,91,43])).
% 96.73/97.30 cnf(6115,plain,
% 96.73/97.30 (P3(a86,a9)),
% 96.73/97.30 inference(scs_inference,[],[13,559,6077,4086,5156,5893,5919,4486,4824,5988,4841,5929,4017,4333,784,6103,102,50,17,20,51,70,52,71,69,99,48,46,94,91,43,100])).
% 96.73/97.30 cnf(6116,plain,
% 96.73/97.30 (P6(f79(a71),x61161,a86)),
% 96.73/97.30 inference(rename_variables,[],[4486])).
% 96.73/97.30 cnf(6118,plain,
% 96.73/97.30 (~P5(a86,a9)),
% 96.73/97.30 inference(scs_inference,[],[13,559,6077,4086,5156,5893,5919,4486,6116,4824,5988,4841,5929,4017,4333,784,6103,102,50,17,20,51,70,52,71,69,99,48,46,94,91,43,100,104])).
% 96.73/97.30 cnf(6119,plain,
% 96.73/97.30 (P6(f79(a71),x61191,a86)),
% 96.73/97.30 inference(rename_variables,[],[4486])).
% 96.73/97.30 cnf(6129,plain,
% 96.73/97.30 (P6(a59,a58,a9)),
% 96.73/97.30 inference(scs_inference,[],[13,332,559,6077,4086,5156,5893,6014,5919,4486,6116,6119,4824,5988,4725,4841,5929,4017,4333,654,784,6103,584,102,50,17,20,51,70,52,71,69,99,48,46,94,91,43,100,104,105,44,108,40])).
% 96.73/97.30 cnf(6134,plain,
% 96.73/97.30 (P1(f38(a59,a58),a59)),
% 96.73/97.30 inference(scs_inference,[],[6129,65])).
% 96.73/97.30 cnf(6140,plain,
% 96.73/97.30 (P1(a57,f79(a2))),
% 96.73/97.30 inference(scs_inference,[],[758,6129,5983,9,65,50,102,17])).
% 96.73/97.30 cnf(6142,plain,
% 96.73/97.30 (~P1(f76(a65,a65),f79(a65))),
% 96.73/97.30 inference(scs_inference,[],[758,6129,5983,4093,9,65,50,102,17,20])).
% 96.73/97.30 cnf(6157,plain,
% 96.73/97.30 (P1(x61571,a3)),
% 96.73/97.30 inference(rename_variables,[],[8])).
% 96.73/97.30 cnf(6167,plain,
% 96.73/97.30 (~P2(a10,a83)),
% 96.73/97.30 inference(scs_inference,[],[758,6129,5144,5668,5983,6086,6060,6048,4093,9,918,784,8,6157,65,50,102,17,20,51,70,52,71,69,99,34,48,33,46,94])).
% 96.73/97.30 cnf(6180,plain,
% 96.73/97.30 (P6(f41(a9,a91),f47(a9,a91),a9)),
% 96.73/97.30 inference(scs_inference,[],[1161,6031,102,50])).
% 96.73/97.30 cnf(6182,plain,
% 96.73/97.30 (P1(f40(a2,a58),f79(a2))),
% 96.73/97.30 inference(scs_inference,[],[1161,6031,4435,102,50,17])).
% 96.73/97.30 cnf(6196,plain,
% 96.73/97.30 (~P6(f41(a9,a91),f47(a9,a91),a91)),
% 96.73/97.30 inference(scs_inference,[],[1161,5665,5873,6031,6134,4435,102,50,17,20,51,70,52,69,71,99])).
% 96.73/97.30 cnf(6202,plain,
% 96.73/97.30 (P1(x62021,a3)),
% 96.73/97.30 inference(rename_variables,[],[8])).
% 96.73/97.30 cnf(6209,plain,
% 96.73/97.30 (P1(x62091,f48(a84,a84))),
% 96.73/97.30 inference(rename_variables,[],[654])).
% 96.73/97.30 cnf(6214,plain,
% 96.73/97.30 (~P6(f79(a62),a65,a73)),
% 96.73/97.30 inference(scs_inference,[],[13,1161,5665,5873,6031,6079,6134,6142,6113,4292,5018,4435,10,5,654,8,6202,102,50,17,20,51,70,52,69,71,99,79,34,48,33,46,94,91])).
% 96.73/97.30 cnf(6216,plain,
% 96.73/97.30 (~P6(a69,a71,a78)),
% 96.73/97.30 inference(scs_inference,[],[13,1161,5665,5873,6031,6079,6134,6142,6113,4292,5018,4435,10,5,12,6,654,8,6202,102,50,17,20,51,70,52,69,71,99,79,34,48,33,46,94,91,43])).
% 96.73/97.30 cnf(6218,plain,
% 96.73/97.30 (~P1(f7(a69,a71),a71)),
% 96.73/97.30 inference(scs_inference,[],[13,1161,5665,5873,6031,6079,6134,6142,6113,4292,5018,4435,10,5,12,6,654,8,6202,102,50,17,20,51,70,52,69,71,99,79,34,48,33,46,94,91,43,42])).
% 96.73/97.30 cnf(6220,plain,
% 96.73/97.30 (P1(f7(a69,a71),a69)),
% 96.73/97.30 inference(scs_inference,[],[13,1161,5665,5873,6031,6079,6134,6142,6113,4292,5018,4435,10,5,12,6,654,8,6202,102,50,17,20,51,70,52,69,71,99,79,34,48,33,46,94,91,43,42,26])).
% 96.73/97.30 cnf(6246,plain,
% 96.73/97.30 (~P1(f52(a59,a2),f79(a2))),
% 96.73/97.30 inference(scs_inference,[],[13,344,1161,5665,5873,6031,6079,6134,6142,6113,4914,4926,6140,6111,4292,5026,4996,4362,4168,5018,4435,10,5,12,6,654,6209,8,6202,102,50,17,20,51,70,52,69,71,99,79,34,48,33,46,94,91,43,42,26,53,77,109,41,75,78,44,15,81,89])).
% 96.73/97.30 cnf(6248,plain,
% 96.73/97.30 (~P6(f49(a80,a8),f50(a80,a8),a8)),
% 96.73/97.30 inference(scs_inference,[],[1221,102])).
% 96.73/97.30 cnf(6250,plain,
% 96.73/97.30 (P1(f7(a69,a71),f79(a71))),
% 96.73/97.30 inference(scs_inference,[],[1221,6218,102,17])).
% 96.73/97.30 cnf(6254,plain,
% 96.73/97.30 (~P1(f7(a69,a71),f79(a69))),
% 96.73/97.30 inference(scs_inference,[],[1221,6108,6220,6218,102,17,50,20])).
% 96.73/97.30 cnf(6264,plain,
% 96.73/97.30 (P6(f49(a80,a8),f50(a80,a8),a80)),
% 96.73/97.30 inference(scs_inference,[],[1221,6108,5870,6118,6220,6218,102,17,50,20,51,52,70,69,71])).
% 96.73/97.30 cnf(6269,plain,
% 96.73/97.30 (P1(x62691,a3)),
% 96.73/97.30 inference(rename_variables,[],[8])).
% 96.73/97.30 cnf(6277,plain,
% 96.73/97.30 (~P1(x62771,f45(a5,a5))),
% 96.73/97.30 inference(rename_variables,[],[784])).
% 96.73/97.30 cnf(6288,plain,
% 96.73/97.30 (~P1(f7(a65,a62),a62)),
% 96.73/97.30 inference(scs_inference,[],[1221,6108,5870,6118,6246,6182,6096,6196,6220,6082,6180,6218,10,5,654,784,6277,8,6269,102,17,50,20,51,52,70,69,71,99,34,44,33,48,46,94,91,43,42])).
% 96.73/97.30 cnf(6290,plain,
% 96.73/97.30 (P1(f7(a65,a62),a65)),
% 96.73/97.30 inference(scs_inference,[],[1221,6108,5870,6118,6246,6182,6096,6196,6220,6082,6180,6218,10,5,654,784,6277,8,6269,102,17,50,20,51,52,70,69,71,99,34,44,33,48,46,94,91,43,42,26])).
% 96.73/97.30 cnf(6330,plain,
% 96.73/97.30 (P1(x63301,f48(a84,a84))),
% 96.73/97.30 inference(rename_variables,[],[654])).
% 96.73/97.30 cnf(6348,plain,
% 96.73/97.30 ($false),
% 96.73/97.30 inference(scs_inference,[],[13,1251,6216,6115,6167,6264,6248,6250,6254,6290,6288,6050,289,319,6214,4296,654,6330,102,17,20,50,51,52,70,69,71,99,49,47,34,45,44,33,48,46,94,91,43,89]),
% 96.73/97.30 ['proof']).
% 96.73/97.30 % SZS output end Proof
% 96.73/97.30 % Total time :96.020000s
%------------------------------------------------------------------------------