%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : KRS201+1 : TPTP v8.2.0. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Jun 24 10:08:52 EDT 2024
% Result : Theorem 58.85s 58.89s
% Output : CNFRefutation 58.87s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS201+1 : TPTP v8.2.0. Bugfixed v5.4.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n011.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed Jun 19 13:23:54 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.54/0.58 start to proof:theBenchmark
% 58.85/58.88 %-------------------------------------------
% 58.85/58.88 % File :CSE---1.7
% 58.85/58.88 % Problem :theBenchmark
% 58.85/58.88 % Transform :cnf
% 58.85/58.88 % Format :tptp:raw
% 58.85/58.88 % Command :java -jar mcs_scs.jar %d %s
% 58.85/58.88
% 58.85/58.88 % Result :Theorem 58.250000s
% 58.85/58.88 % Output :CNFRefutation 58.250000s
% 58.85/58.88 %-------------------------------------------
% 58.85/58.89 %------------------------------------------------------------------------------
% 58.85/58.89 % File : KRS201+1 : TPTP v8.2.0. Bugfixed v5.4.0.
% 58.85/58.89 % Domain : Knowledge Representation
% 58.85/58.89 % Problem : SAP nota THM
% 58.85/58.89 % Version : [Sut08] axioms.
% 58.85/58.89 % English :
% 58.85/58.89
% 58.85/58.89 % Refs : [Sut08] Sutcliffe (2008), The SZS Ontologies for Automated Rea
% 58.85/58.89 % Source : [TPTP]
% 58.85/58.89 % Names :
% 58.85/58.89
% 58.85/58.89 % Status : Theorem
% 58.85/58.89 % Rating : 0.19 v8.2.0, 0.27 v8.1.0, 0.14 v7.5.0, 0.24 v7.4.0, 0.12 v7.3.0, 0.29 v7.2.0, 0.17 v7.1.0, 0.25 v7.0.0, 0.14 v6.4.0, 0.07 v6.3.0, 0.08 v6.2.0, 0.27 v6.1.0, 0.24 v6.0.0, 0.50 v5.5.0, 0.38 v5.4.0
% 58.85/58.89 % Syntax : Number of formulae : 33 ( 3 unt; 0 def)
% 58.85/58.89 % Number of atoms : 107 ( 0 equ)
% 58.85/58.89 % Maximal formula atoms : 7 ( 3 avg)
% 58.85/58.89 % Number of connectives : 96 ( 22 ~; 1 |; 35 &)
% 58.85/58.89 % ( 28 <=>; 8 =>; 0 <=; 2 <~>)
% 58.85/58.89 % Maximal formula depth : 10 ( 6 avg)
% 58.85/58.89 % Maximal term depth : 2 ( 1 avg)
% 58.85/58.89 % Number of predicates : 7 ( 7 usr; 0 prp; 2-3 aty)
% 58.85/58.89 % Number of functors : 20 ( 20 usr; 19 con; 0-1 aty)
% 58.85/58.89 % Number of variables : 122 ( 72 !; 50 ?)
% 58.85/58.89 % SPC : FOF_THM_RFO_NEQ
% 58.85/58.89
% 58.85/58.89 % Comments :
% 58.85/58.89 % Bugfixes : v5.4.0 - Added missing axiom in KRS001+1.ax
% 58.85/58.89 %------------------------------------------------------------------------------
% 58.85/58.89 %----Include SZS success ontology nodes
% 58.85/58.89 include('Axioms/KRS001+0.ax').
% 58.85/58.89 %----Include SZS success ontology node relationships
% 58.85/58.89 include('Axioms/KRS001+1.ax').
% 58.85/58.89 %------------------------------------------------------------------------------
% 58.85/58.89 fof(nota_sap_thm,conjecture,
% 58.85/58.89 nota(sap,thm) ).
% 58.85/58.89
% 58.85/58.89 %------------------------------------------------------------------------------
% 58.85/58.89 %-------------------------------------------
% 58.85/58.89 % Proof found
% 58.85/58.89 % SZS status Theorem for theBenchmark
% 58.85/58.89 % SZS output start Proof
% 58.87/58.90 %ClaNum:109(EqnAxiom:0)
% 58.87/58.90 %VarNum:590(SingletonVarNum:249)
% 58.87/58.90 %MaxLitNum:6
% 58.87/58.90 %MaxfuncDepth:1
% 58.87/58.90 %SharedTerms:52
% 58.87/58.90 %goalClause: 13
% 58.87/58.90 %singleGoalClaCount:1
% 58.87/58.90 [1]P1(a1,a2)
% 58.87/58.90 [2]P1(a55,a56)
% 58.87/58.90 [3]P1(a55,a59)
% 58.87/58.90 [4]P1(a61,a62)
% 58.87/58.90 [5]P1(a66,a65)
% 58.87/58.90 [6]P1(a67,a69)
% 58.87/58.90 [7]P1(a70,a71)
% 58.87/58.90 [9]~P1(a57,a2)
% 58.87/58.90 [10]~P1(a66,a62)
% 58.87/58.90 [11]~P1(a68,a65)
% 58.87/58.90 [12]~P1(a67,a71)
% 58.87/58.90 [13]~P4(a73,a80)
% 58.87/58.90 [8]P1(x81,a3)
% 58.87/58.90 [14]~P1(x141,a58)
% 58.87/58.90 [18]~P1(a63,a56)+~P1(a64,a59)
% 58.87/58.90 [15]~P1(x151,a62)+P1(x151,a65)
% 58.87/58.90 [17]P1(x171,x172)+P1(x171,f74(x172))
% 58.87/58.90 [20]~P1(x201,x202)+~P1(x201,f74(x202))
% 58.87/58.90 [21]P6(x211,x212,a5)+P1(f4(x211),x211)
% 58.87/58.90 [24]P6(x241,x242,a86)+P1(f6(x241,x242),x242)
% 58.87/58.90 [25]P6(x251,x252,a73)+P1(f31(x251,x252),x251)
% 58.87/58.90 [26]P6(x261,x262,a80)+P1(f7(x261,x262),x261)
% 58.87/58.90 [42]P6(x421,x422,a80)+~P1(f7(x421,x422),x422)
% 58.87/58.90 [50]P2(x501,x502)+P6(f41(x501,x502),f47(x501,x502),x501)
% 58.87/58.90 [51]P5(x511,x512)+P6(f48(x511,x512),f51(x511,x512),x512)
% 58.87/58.90 [52]P5(x521,x522)+P6(f48(x521,x522),f51(x521,x522),x521)
% 58.87/58.90 [53]~P6(x531,x532,a82)+P1(f76(x531,x532),x532)
% 58.87/58.90 [54]~P6(x541,x542,a82)+P1(f76(x541,x542),x541)
% 58.87/58.90 [55]~P6(x551,x552,a10)+P1(f11(x551,x552),x551)
% 58.87/58.90 [56]~P6(x561,x562,a81)+P1(f13(x561,x562),x561)
% 58.87/58.90 [57]~P6(x571,x572,a90)+P1(f15(x571,x572),x571)
% 58.87/58.90 [58]~P6(x581,x582,a90)+P1(f17(x581,x582),x582)
% 58.87/58.90 [59]~P6(x591,x592,a75)+P1(f18(x591,x592),x591)
% 58.87/58.90 [60]~P6(x601,x602,a87)+P1(f20(x601,x602),x601)
% 58.87/58.90 [61]~P6(x611,x612,a91)+P1(f25(x611,x612),x611)
% 58.87/58.90 [62]~P6(x621,x622,a91)+P1(f28(x621,x622),x622)
% 58.87/58.90 [63]~P6(x631,x632,a83)+P1(f33(x631,x632),x632)
% 58.87/58.90 [64]~P6(x641,x642,a89)+P1(f34(x641,x642),x642)
% 58.87/58.90 [65]~P6(x651,x652,a9)+P1(f38(x651,x652),x651)
% 58.87/58.90 [66]~P6(x661,x662,a79)+P1(f42(x661,x662),x662)
% 58.87/58.90 [67]~P6(x671,x672,a79)+P1(f42(x671,x672),x671)
% 58.87/58.90 [68]~P6(x681,x682,a79)+P1(f44(x681,x682),x681)
% 58.87/58.90 [69]~P3(x691,x692)+P6(f45(x691,x692),f46(x691,x692),x692)
% 58.87/58.90 [70]~P3(x701,x702)+P6(f45(x701,x702),f46(x701,x702),x701)
% 58.87/58.90 [71]~P4(x711,x712)+P6(f49(x711,x712),f50(x711,x712),x711)
% 58.87/58.90 [72]~P6(x721,x722,a9)+P1(f38(x721,x722),f74(x722))
% 58.87/58.90 [73]~P6(x731,x732,a79)+P1(f44(x731,x732),f74(x732))
% 58.87/58.90 [82]~P6(x821,x822,a90)+~P1(f17(x821,x822),x821)
% 58.87/58.90 [83]~P6(x831,x832,a75)+~P1(f21(x831,x832),x831)
% 58.87/58.90 [84]~P6(x841,x842,a87)+~P1(f26(x841,x842),x841)
% 58.87/58.90 [85]~P6(x851,x852,a91)+~P1(f28(x851,x852),x851)
% 58.87/58.90 [86]~P6(x861,x862,a91)+~P1(f30(x861,x862),x862)
% 58.87/58.90 [87]~P6(x871,x872,a89)+~P1(f39(x871,x872),x872)
% 58.87/58.90 [99]P2(x991,x992)+~P6(f41(x991,x992),f47(x991,x992),x992)
% 58.87/58.90 [102]~P4(x1021,x1022)+~P6(f49(x1021,x1022),f50(x1021,x1022),x1022)
% 58.87/58.90 [22]~P1(x223,x222)+P6(x221,x222,a73)
% 58.87/58.90 [23]~P1(x233,x231)+P6(x231,x232,a86)
% 58.87/58.90 [27]P1(x271,x272)+~P6(x273,x272,a81)
% 58.87/58.90 [28]P1(x281,x282)+~P6(x283,x282,a84)
% 58.87/58.90 [29]P1(x291,x292)+~P6(x293,x292,a87)
% 58.87/58.90 [30]P1(x301,x302)+~P6(x303,x302,a85)
% 58.87/58.90 [31]P1(x311,x312)+~P6(x312,x313,a84)
% 58.87/58.90 [32]P1(x321,x322)+~P6(x322,x323,a88)
% 58.87/58.90 [36]~P1(x361,x362)+~P6(x362,x363,a5)
% 58.87/58.90 [37]~P1(x371,x372)+~P6(x372,x373,a83)
% 58.87/58.90 [38]~P1(x381,x382)+~P6(x382,x383,a85)
% 58.87/58.90 [39]~P1(x391,x392)+~P6(x392,x393,a89)
% 58.87/58.90 [35]~P6(x353,x352,a88)+P1(x351,f74(x352))
% 58.87/58.90 [76]P6(x761,x762,a8)+P1(f60(x761,x762),x761)+P1(f72(x761,x762),x762)
% 58.87/58.90 [93]P6(x931,x932,a85)+P1(f36(x931,x932),x931)+~P1(f37(x931,x932),x932)
% 58.87/58.90 [98]P6(x981,x982,a84)+~P1(f23(x981,x982),x981)+~P1(f24(x981,x982),x982)
% 58.87/58.90 [101]P6(x1011,x1012,a88)+~P1(f40(x1011,x1012),x1011)+~P1(f43(x1011,x1012),f74(x1012))
% 58.87/58.90 [108]P7(x1081,x1082)+P6(f53(x1081,x1082),f54(x1081,x1082),x1082)+~P6(f53(x1081,x1082),f54(x1081,x1082),x1081)
% 58.87/58.90 [109]P7(x1091,x1092)+P6(f53(x1091,x1092),f54(x1091,x1092),x1091)+~P6(f53(x1091,x1092),f54(x1091,x1092),x1092)
% 58.87/58.90 [34]~P1(x343,x341)+~P1(x343,x342)+P6(x341,x342,a82)
% 58.87/58.90 [43]P1(x431,x432)+~P1(x431,x433)+~P6(x433,x432,a80)
% 58.87/58.90 [44]P1(x441,x442)+~P1(x441,x443)+~P6(x442,x443,a10)
% 58.87/58.90 [45]P1(x451,x452)+~P1(x451,x453)+~P6(x452,x453,a75)
% 58.87/58.90 [46]P1(x461,x462)+~P1(x461,x463)+~P6(x463,x462,a10)
% 58.87/58.90 [47]P1(x471,x472)+~P1(x471,x473)+~P6(x473,x472,a90)
% 58.87/58.90 [48]P1(x481,x482)+~P1(x481,x483)+~P6(x483,x482,a75)
% 58.87/58.90 [49]P1(x491,x492)+~P1(x491,x493)+~P6(x493,x492,a91)
% 58.87/58.90 [40]~P1(x403,x401)+P6(x401,x402,a9)+~P1(x403,f74(x402))
% 58.87/58.90 [41]~P1(x413,x412)+P6(x411,x412,a83)+P1(f32(x411,x412),x411)
% 58.87/58.90 [77]~P1(x773,x771)+P6(x771,x772,a81)+~P1(f14(x771,x772),x772)
% 58.87/58.90 [78]~P1(x783,x782)+~P6(x781,x782,a86)+P1(f29(x781,x782),x781)
% 58.87/58.90 [79]~P1(x793,x791)+~P6(x791,x792,a73)+P1(f52(x791,x792),x792)
% 58.87/58.90 [80]~P1(x803,x801)+~P6(x801,x802,a8)+P1(f77(x801,x802),x802)
% 58.87/58.90 [81]~P1(x813,x812)+~P6(x811,x812,a8)+P1(f78(x811,x812),x811)
% 58.87/58.90 [33]~P1(x333,x332)+~P1(x334,x331)+P6(x331,x332,a8)
% 58.87/58.90 [75]~P7(x754,x753)+P6(x751,x752,x753)+P6(x751,x752,x754)
% 58.87/58.90 [91]~P6(x913,x914,x911)+P4(x911,x912)+P6(x913,x914,x912)
% 58.87/58.90 [94]~P6(x941,x942,x944)+P6(x941,x942,x943)+~P2(x944,x943)
% 58.87/58.90 [100]~P6(x1003,x1004,x1001)+P3(x1001,x1002)+~P6(x1003,x1004,x1002)
% 58.87/58.90 [104]~P6(x1043,x1044,x1041)+~P5(x1041,x1042)+~P6(x1043,x1044,x1042)
% 58.87/58.90 [105]~P6(x1053,x1054,x1051)+~P7(x1051,x1052)+~P6(x1053,x1054,x1052)
% 58.87/58.90 [92]~P1(x923,x921)+P6(x921,x922,a10)+P1(f12(x921,x922),x922)+P1(f12(x921,x922),x921)
% 58.87/58.90 [106]~P1(x1063,x1061)+P6(x1061,x1062,a10)+~P1(f12(x1061,x1062),x1062)+~P1(f12(x1061,x1062),x1061)
% 58.87/58.90 [74]P1(x741,x742)+~P1(x744,x742)+P6(x743,x742,a89)+P1(f35(x743,x742),x743)
% 58.87/58.90 [90]P1(x901,x902)+~P1(x904,x902)+P6(x902,x903,a87)+~P1(f22(x902,x903),x903)
% 58.87/58.90 [88]~P1(x881,x883)+P1(x881,x882)+~P1(x884,x882)+P6(x882,x883,a90)+P1(f16(x882,x883),x882)
% 58.87/58.90 [89]~P1(x894,x891)+~P1(x893,x891)+~P1(x894,x892)+P6(x891,x892,a79)+~P1(x893,f74(x892))
% 58.87/58.90 [96]P1(x961,x962)+~P1(x964,x962)+P6(x962,x963,a75)+P1(f19(x962,x963),x963)+P1(f19(x962,x963),x962)
% 58.87/58.90 [97]~P1(x971,x973)+P1(x971,x972)+~P1(x974,x972)+P6(x972,x973,a90)+~P1(f16(x972,x973),x973)
% 58.87/58.90 [107]P1(x1071,x1072)+~P1(x1074,x1072)+P6(x1072,x1073,a75)+~P1(f19(x1072,x1073),x1073)+~P1(f19(x1072,x1073),x1072)
% 58.87/58.90 [95]~P1(x953,x952)+P1(x951,x952)+P1(x953,x954)+~P1(x955,x954)+P6(x954,x952,a91)+P1(f27(x954,x952),x954)
% 58.87/58.90 [103]~P1(x1033,x1032)+P1(x1031,x1032)+P1(x1033,x1034)+~P1(x1035,x1034)+P6(x1034,x1032,a91)+~P1(f27(x1034,x1032),x1032)
% 58.87/58.90 %EqnAxiom
% 58.87/58.90
% 58.87/58.90 %-------------------------------------------
% 58.87/58.91 cnf(110,plain,
% 58.87/58.91 (P6(a58,x1101,a5)),
% 58.87/58.91 inference(scs_inference,[],[14,21])).
% 58.87/58.91 cnf(111,plain,
% 58.87/58.91 (~P1(x1111,a58)),
% 58.87/58.91 inference(rename_variables,[],[14])).
% 58.87/58.91 cnf(113,plain,
% 58.87/58.91 (P6(x1131,a58,a86)),
% 58.87/58.91 inference(scs_inference,[],[14,111,21,24])).
% 58.87/58.91 cnf(114,plain,
% 58.87/58.91 (~P1(x1141,a58)),
% 58.87/58.91 inference(rename_variables,[],[14])).
% 58.87/58.91 cnf(116,plain,
% 58.87/58.91 (P6(a58,x1161,a73)),
% 58.87/58.91 inference(scs_inference,[],[14,111,114,21,24,25])).
% 58.87/58.91 cnf(117,plain,
% 58.87/58.91 (~P1(x1171,a58)),
% 58.87/58.91 inference(rename_variables,[],[14])).
% 58.87/58.91 cnf(119,plain,
% 58.87/58.91 (P6(a58,x1191,a80)),
% 58.87/58.91 inference(scs_inference,[],[14,111,114,117,21,24,25,26])).
% 58.87/58.91 cnf(120,plain,
% 58.87/58.91 (~P1(x1201,a58)),
% 58.87/58.91 inference(rename_variables,[],[14])).
% 58.87/58.91 cnf(122,plain,
% 58.87/58.91 (P6(x1221,a3,a80)),
% 58.87/58.91 inference(scs_inference,[],[8,14,111,114,117,21,24,25,26,42])).
% 58.87/58.91 cnf(123,plain,
% 58.87/58.91 (P1(x1231,a3)),
% 58.87/58.91 inference(rename_variables,[],[8])).
% 58.87/58.91 cnf(125,plain,
% 58.87/58.91 (~P1(a68,a62)),
% 58.87/58.91 inference(scs_inference,[],[8,14,111,114,117,11,21,24,25,26,42,15])).
% 58.87/58.91 cnf(127,plain,
% 58.87/58.91 (~P6(x1271,a58,a82)),
% 58.87/58.91 inference(scs_inference,[],[8,14,111,114,117,120,11,21,24,25,26,42,15,53])).
% 58.87/58.91 cnf(128,plain,
% 58.87/58.91 (~P1(x1281,a58)),
% 58.87/58.91 inference(rename_variables,[],[14])).
% 58.87/58.91 cnf(130,plain,
% 58.87/58.91 (~P6(a58,x1301,a82)),
% 58.87/58.91 inference(scs_inference,[],[8,14,111,114,117,120,128,11,21,24,25,26,42,15,53,54])).
% 58.87/58.91 cnf(131,plain,
% 58.87/58.91 (~P1(x1311,a58)),
% 58.87/58.91 inference(rename_variables,[],[14])).
% 58.87/58.91 cnf(133,plain,
% 58.87/58.91 (~P6(a58,x1331,a10)),
% 58.87/58.91 inference(scs_inference,[],[8,14,111,114,117,120,128,131,11,21,24,25,26,42,15,53,54,55])).
% 58.87/58.91 cnf(134,plain,
% 58.87/58.91 (~P1(x1341,a58)),
% 58.87/58.91 inference(rename_variables,[],[14])).
% 58.87/58.91 cnf(136,plain,
% 58.87/58.91 (~P6(a58,x1361,a81)),
% 58.87/58.91 inference(scs_inference,[],[8,14,111,114,117,120,128,131,134,11,21,24,25,26,42,15,53,54,55,56])).
% 58.87/58.91 cnf(137,plain,
% 58.87/58.91 (~P1(x1371,a58)),
% 58.87/58.91 inference(rename_variables,[],[14])).
% 58.87/58.91 cnf(140,plain,
% 58.87/58.91 (~P1(x1401,a58)),
% 58.87/58.91 inference(rename_variables,[],[14])).
% 58.87/58.91 cnf(142,plain,
% 58.87/58.91 (~P6(x1421,a58,a90)),
% 58.87/58.91 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])).
% 58.87/58.91 cnf(143,plain,
% 58.87/58.91 (~P1(x1431,a58)),
% 58.87/58.91 inference(rename_variables,[],[14])).
% 58.87/58.91 cnf(146,plain,
% 58.87/58.91 (~P1(x1461,a58)),
% 58.87/58.91 inference(rename_variables,[],[14])).
% 58.87/58.91 cnf(149,plain,
% 58.87/58.91 (~P1(x1491,a58)),
% 58.87/58.91 inference(rename_variables,[],[14])).
% 58.87/58.91 cnf(152,plain,
% 58.87/58.91 (~P1(x1521,a58)),
% 58.87/58.91 inference(rename_variables,[],[14])).
% 58.87/58.91 cnf(155,plain,
% 58.87/58.91 (~P1(x1551,a58)),
% 58.87/58.91 inference(rename_variables,[],[14])).
% 58.87/58.91 cnf(158,plain,
% 58.87/58.91 (~P1(x1581,a58)),
% 58.87/58.91 inference(rename_variables,[],[14])).
% 58.87/58.91 cnf(161,plain,
% 58.87/58.91 (~P1(x1611,a58)),
% 58.87/58.91 inference(rename_variables,[],[14])).
% 58.87/58.91 cnf(164,plain,
% 58.87/58.91 (~P1(x1641,a58)),
% 58.87/58.91 inference(rename_variables,[],[14])).
% 58.87/58.91 cnf(167,plain,
% 58.87/58.91 (~P1(x1671,a58)),
% 58.87/58.91 inference(rename_variables,[],[14])).
% 58.87/58.91 cnf(170,plain,
% 58.87/58.91 (~P1(x1701,a58)),
% 58.87/58.91 inference(rename_variables,[],[14])).
% 58.87/58.91 cnf(173,plain,
% 58.87/58.91 (P1(x1731,a3)),
% 58.87/58.91 inference(rename_variables,[],[8])).
% 58.87/58.91 cnf(176,plain,
% 58.87/58.91 (P1(x1761,a3)),
% 58.87/58.91 inference(rename_variables,[],[8])).
% 58.87/58.91 cnf(179,plain,
% 58.87/58.91 (P1(x1791,a3)),
% 58.87/58.91 inference(rename_variables,[],[8])).
% 58.87/58.91 cnf(182,plain,
% 58.87/58.91 (P1(x1821,a3)),
% 58.87/58.91 inference(rename_variables,[],[8])).
% 58.87/58.91 cnf(185,plain,
% 58.87/58.91 (P1(x1851,a3)),
% 58.87/58.91 inference(rename_variables,[],[8])).
% 58.87/58.91 cnf(188,plain,
% 58.87/58.91 (P1(x1881,a3)),
% 58.87/58.91 inference(rename_variables,[],[8])).
% 58.87/58.91 cnf(190,plain,
% 58.87/58.91 (P4(a5,a82)),
% 58.87/58.91 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])).
% 58.87/58.91 cnf(194,plain,
% 58.87/58.91 (P6(a58,a3,a85)),
% 58.87/58.91 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])).
% 58.87/58.91 cnf(195,plain,
% 58.87/58.91 (~P1(x1951,a58)),
% 58.87/58.91 inference(rename_variables,[],[14])).
% 58.87/58.91 cnf(196,plain,
% 58.87/58.91 (P1(x1961,a3)),
% 58.87/58.91 inference(rename_variables,[],[8])).
% 58.87/58.91 cnf(198,plain,
% 58.87/58.91 (~P6(a3,a58,a8)),
% 58.87/58.91 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])).
% 58.87/58.91 cnf(199,plain,
% 58.87/58.91 (~P1(x1991,a58)),
% 58.87/58.91 inference(rename_variables,[],[14])).
% 58.87/58.91 cnf(201,plain,
% 58.87/58.91 (~P6(a58,a3,a8)),
% 58.87/58.91 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])).
% 58.87/58.91 cnf(211,plain,
% 58.87/58.91 (P1(x2111,a3)),
% 58.87/58.91 inference(rename_variables,[],[8])).
% 58.87/58.91 cnf(212,plain,
% 58.87/58.91 (P1(x2121,a3)),
% 58.87/58.91 inference(rename_variables,[],[8])).
% 58.87/58.91 cnf(214,plain,
% 58.87/58.91 (P6(a3,a3,a84)),
% 58.87/58.91 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])).
% 58.87/58.91 cnf(229,plain,
% 58.87/58.91 (P4(a5,a10)),
% 58.87/58.91 inference(scs_inference,[],[110,133,91])).
% 58.87/58.91 cnf(230,plain,
% 58.87/58.91 (~P6(a58,x2301,a10)),
% 58.87/58.91 inference(rename_variables,[],[133])).
% 58.87/58.91 cnf(237,plain,
% 58.87/58.91 (~P1(x2371,a58)),
% 58.87/58.91 inference(rename_variables,[],[14])).
% 58.87/58.91 cnf(239,plain,
% 58.87/58.91 (~P5(a5,a86)),
% 58.87/58.91 inference(scs_inference,[],[110,113,127,133,230,1,14,91,75,81,104])).
% 58.87/58.91 cnf(240,plain,
% 58.87/58.91 (P6(x2401,a58,a86)),
% 58.87/58.91 inference(rename_variables,[],[113])).
% 58.87/58.91 cnf(241,plain,
% 58.87/58.91 (P6(a58,x2411,a5)),
% 58.87/58.91 inference(rename_variables,[],[110])).
% 58.87/58.91 cnf(246,plain,
% 58.87/58.91 (P3(a5,a86)),
% 58.87/58.91 inference(scs_inference,[],[110,241,113,240,127,133,230,1,14,237,91,75,81,104,80,100])).
% 58.87/58.91 cnf(247,plain,
% 58.87/58.91 (P6(x2471,a58,a86)),
% 58.87/58.91 inference(rename_variables,[],[113])).
% 58.87/58.91 cnf(248,plain,
% 58.87/58.91 (P6(a58,x2481,a5)),
% 58.87/58.91 inference(rename_variables,[],[110])).
% 58.87/58.91 cnf(254,plain,
% 58.87/58.91 (P6(a3,x2541,a84)+~P1(f24(a3,x2541),x2541)),
% 58.87/58.91 inference(scs_inference,[],[110,241,248,113,240,247,127,133,230,1,8,14,237,91,75,81,104,80,100,105,98])).
% 58.87/58.91 cnf(278,plain,
% 58.87/58.91 (P4(a86,a8)),
% 58.87/58.91 inference(scs_inference,[],[113,198,91])).
% 58.87/58.91 cnf(285,plain,
% 58.87/58.91 (~P5(a85,a85)),
% 58.87/58.91 inference(scs_inference,[],[194,113,198,91,75,105,104])).
% 58.87/58.91 cnf(287,plain,
% 58.87/58.91 (P3(a85,a85)),
% 58.87/58.91 inference(scs_inference,[],[194,113,198,91,75,105,104,100])).
% 58.87/58.91 cnf(290,plain,
% 58.87/58.91 (P6(a58,x2901,a5)),
% 58.87/58.91 inference(rename_variables,[],[110])).
% 58.87/58.91 cnf(295,plain,
% 58.87/58.91 (~P5(a5,a73)),
% 58.87/58.91 inference(scs_inference,[],[110,290,116,201,130,91,75,104])).
% 58.87/58.91 cnf(296,plain,
% 58.87/58.91 (P6(a58,x2961,a73)),
% 58.87/58.91 inference(rename_variables,[],[116])).
% 58.87/58.91 cnf(298,plain,
% 58.87/58.91 (P3(a5,a73)),
% 58.87/58.91 inference(scs_inference,[],[110,290,116,296,201,130,91,75,104,100])).
% 58.87/58.91 cnf(305,plain,
% 58.87/58.91 (~P6(a58,x3051,a81)),
% 58.87/58.91 inference(rename_variables,[],[136])).
% 58.87/58.91 cnf(311,plain,
% 58.87/58.91 (P6(a58,x3111,a80)),
% 58.87/58.91 inference(rename_variables,[],[119])).
% 58.87/58.91 cnf(313,plain,
% 58.87/58.91 (P3(a5,a80)),
% 58.87/58.91 inference(scs_inference,[],[110,119,311,130,136,305,91,75,105,100])).
% 58.87/58.91 cnf(314,plain,
% 58.87/58.91 (P6(a58,x3141,a80)),
% 58.87/58.91 inference(rename_variables,[],[119])).
% 58.87/58.91 cnf(316,plain,
% 58.87/58.91 (~P5(a5,a80)),
% 58.87/58.91 inference(scs_inference,[],[110,119,311,314,130,136,305,91,75,105,100,104])).
% 58.87/58.91 cnf(320,plain,
% 58.87/58.91 (~P6(x3201,a58,a90)),
% 58.87/58.91 inference(rename_variables,[],[142])).
% 58.87/58.91 cnf(326,plain,
% 58.87/58.91 (~P5(a84,a84)),
% 58.87/58.91 inference(scs_inference,[],[110,214,198,142,320,91,75,104])).
% 58.87/58.91 cnf(449,plain,
% 58.87/58.91 (~P1(a61,f74(a65))),
% 58.87/58.91 inference(scs_inference,[],[4,20,15])).
% 58.87/58.91 cnf(452,plain,
% 58.87/58.91 (P1(a61,a65)),
% 58.87/58.91 inference(scs_inference,[],[449,35,17])).
% 58.87/58.91 cnf(454,plain,
% 58.87/58.91 (~P1(f43(a3,a65),f74(a65))),
% 58.87/58.91 inference(scs_inference,[],[8,449,35,17,101])).
% 58.87/58.91 cnf(478,plain,
% 58.87/58.91 (P6(a65,x4781,a86)),
% 58.87/58.91 inference(scs_inference,[],[454,23,17])).
% 58.87/58.91 cnf(479,plain,
% 58.87/58.91 (P1(f43(a3,a65),a65)),
% 58.87/58.91 inference(scs_inference,[],[454,17])).
% 58.87/58.91 cnf(521,plain,
% 58.87/58.91 (~P6(a56,a58,a8)),
% 58.87/58.91 inference(scs_inference,[],[2,14,80])).
% 58.87/58.91 cnf(522,plain,
% 58.87/58.91 (~P1(x5221,a58)),
% 58.87/58.91 inference(rename_variables,[],[14])).
% 58.87/58.91 cnf(524,plain,
% 58.87/58.91 (~P6(a58,a56,a8)),
% 58.87/58.91 inference(scs_inference,[],[2,14,522,80,81])).
% 58.87/58.91 cnf(546,plain,
% 58.87/58.91 (~P6(a59,a58,a8)),
% 58.87/58.91 inference(scs_inference,[],[3,14,80])).
% 58.87/58.91 cnf(565,plain,
% 58.87/58.91 (~P6(a62,a58,a8)),
% 58.87/58.91 inference(scs_inference,[],[4,14,80])).
% 58.87/58.91 cnf(566,plain,
% 58.87/58.91 (~P1(x5661,a58)),
% 58.87/58.91 inference(rename_variables,[],[14])).
% 58.87/58.91 cnf(568,plain,
% 58.87/58.91 (~P6(a58,a62,a8)),
% 58.87/58.91 inference(scs_inference,[],[4,14,566,80,81])).
% 58.87/58.91 cnf(580,plain,
% 58.87/58.91 (P6(a3,f74(a58),a84)),
% 58.87/58.91 inference(scs_inference,[],[14,254,17])).
% 58.87/58.91 cnf(581,plain,
% 58.87/58.91 (P1(x5811,f74(a58))),
% 58.87/58.91 inference(scs_inference,[],[580,28])).
% 58.87/58.91 cnf(594,plain,
% 58.87/58.91 (P1(x5941,f74(a58))),
% 58.87/58.91 inference(rename_variables,[],[581])).
% 58.87/58.91 cnf(597,plain,
% 58.87/58.91 (P1(x5971,f74(a58))),
% 58.87/58.91 inference(rename_variables,[],[581])).
% 58.87/58.91 cnf(600,plain,
% 58.87/58.91 (P1(x6001,f74(a58))),
% 58.87/58.91 inference(rename_variables,[],[581])).
% 58.87/58.91 cnf(603,plain,
% 58.87/58.91 (P1(x6031,f74(a58))),
% 58.87/58.91 inference(rename_variables,[],[581])).
% 58.87/58.91 cnf(606,plain,
% 58.87/58.91 (P1(x6061,f74(a58))),
% 58.87/58.91 inference(rename_variables,[],[581])).
% 58.87/58.91 cnf(609,plain,
% 58.87/58.91 (P1(x6091,f74(a58))),
% 58.87/58.91 inference(rename_variables,[],[581])).
% 58.87/58.91 cnf(612,plain,
% 58.87/58.91 (P1(x6121,a3)),
% 58.87/58.91 inference(rename_variables,[],[8])).
% 58.87/58.91 cnf(613,plain,
% 58.87/58.91 (P1(x6131,f74(a58))),
% 58.87/58.91 inference(rename_variables,[],[581])).
% 58.87/58.91 cnf(619,plain,
% 58.87/58.91 (P3(a88,a88)),
% 58.87/58.91 inference(scs_inference,[],[8,612,581,594,597,600,603,606,609,613,84,83,85,42,86,82,101,98,100])).
% 58.87/58.91 cnf(642,plain,
% 58.87/58.91 (P6(f48(a5,a5),f51(a5,a5),a5)),
% 58.87/58.91 inference(scs_inference,[],[110,51,104])).
% 58.87/58.91 cnf(643,plain,
% 58.87/58.91 (~P1(x6431,f48(a5,a5))),
% 58.87/58.91 inference(scs_inference,[],[642,36])).
% 58.87/58.91 cnf(652,plain,
% 58.87/58.91 (P1(x6521,f48(a84,a84))),
% 58.87/58.91 inference(scs_inference,[],[326,52,31])).
% 58.87/58.91 cnf(654,plain,
% 58.87/58.91 (~P1(x6541,f48(a5,a5))),
% 58.87/58.91 inference(rename_variables,[],[643])).
% 58.87/58.91 cnf(657,plain,
% 58.87/58.92 (~P1(x6571,f48(a5,a5))),
% 58.87/58.92 inference(rename_variables,[],[643])).
% 58.87/58.92 cnf(660,plain,
% 58.87/58.92 (~P1(x6601,f48(a5,a5))),
% 58.87/58.92 inference(rename_variables,[],[643])).
% 58.87/58.92 cnf(663,plain,
% 58.87/58.92 (P1(x6631,f48(a84,a84))),
% 58.87/58.92 inference(rename_variables,[],[652])).
% 58.87/58.92 cnf(666,plain,
% 58.87/58.92 (~P1(x6661,f48(a5,a5))),
% 58.87/58.92 inference(rename_variables,[],[643])).
% 58.87/58.92 cnf(669,plain,
% 58.87/58.92 (~P1(x6691,f48(a5,a5))),
% 58.87/58.92 inference(rename_variables,[],[643])).
% 58.87/58.92 cnf(672,plain,
% 58.87/58.92 (~P1(x6721,f48(a5,a5))),
% 58.87/58.92 inference(rename_variables,[],[643])).
% 58.87/58.92 cnf(675,plain,
% 58.87/58.92 (~P1(x6751,f48(a5,a5))),
% 58.87/58.92 inference(rename_variables,[],[643])).
% 58.87/58.92 cnf(677,plain,
% 58.87/58.92 (P6(f48(a5,a5),x6771,a80)),
% 58.87/58.92 inference(scs_inference,[],[643,654,657,660,666,669,672,675,652,57,59,21,84,58,53,62,24,26])).
% 58.87/58.92 cnf(678,plain,
% 58.87/58.92 (~P1(x6781,f48(a5,a5))),
% 58.87/58.92 inference(rename_variables,[],[643])).
% 58.87/58.92 cnf(681,plain,
% 58.87/58.92 (~P1(x6811,f48(a5,a5))),
% 58.87/58.92 inference(rename_variables,[],[643])).
% 58.87/58.92 cnf(684,plain,
% 58.87/58.92 (~P1(x6841,f48(a5,a5))),
% 58.87/58.92 inference(rename_variables,[],[643])).
% 58.87/58.92 cnf(687,plain,
% 58.87/58.92 (P1(x6871,f48(a84,a84))),
% 58.87/58.92 inference(rename_variables,[],[652])).
% 58.87/58.92 cnf(690,plain,
% 58.87/58.92 (P1(x6901,f48(a84,a84))),
% 58.87/58.92 inference(rename_variables,[],[652])).
% 58.87/58.92 cnf(693,plain,
% 58.87/58.92 (~P1(x6931,f48(a5,a5))),
% 58.87/58.92 inference(rename_variables,[],[643])).
% 58.87/58.92 cnf(696,plain,
% 58.87/58.92 (~P1(x6961,f48(a5,a5))),
% 58.87/58.92 inference(rename_variables,[],[643])).
% 58.87/58.92 cnf(699,plain,
% 58.87/58.92 (~P1(x6991,f48(a5,a5))),
% 58.87/58.92 inference(rename_variables,[],[643])).
% 58.87/58.92 cnf(702,plain,
% 58.87/58.92 (~P1(x7021,f48(a5,a5))),
% 58.87/58.92 inference(rename_variables,[],[643])).
% 58.87/58.92 cnf(705,plain,
% 58.87/58.92 (P1(x7051,f48(a84,a84))),
% 58.87/58.92 inference(rename_variables,[],[652])).
% 58.87/58.92 cnf(708,plain,
% 58.87/58.92 (~P1(x7081,f48(a5,a5))),
% 58.87/58.92 inference(rename_variables,[],[643])).
% 58.87/58.92 cnf(711,plain,
% 58.87/58.92 (~P1(x7111,f48(a5,a5))),
% 58.87/58.92 inference(rename_variables,[],[643])).
% 58.87/58.92 cnf(714,plain,
% 58.87/58.92 (~P1(x7141,f48(a5,a5))),
% 58.87/58.92 inference(rename_variables,[],[643])).
% 58.87/58.92 cnf(720,plain,
% 58.87/58.92 (P1(x7201,f48(a84,a84))),
% 58.87/58.92 inference(rename_variables,[],[652])).
% 58.87/58.92 cnf(722,plain,
% 58.87/58.92 (~P6(x7221,f48(a84,a84),a89)),
% 58.87/58.92 inference(scs_inference,[],[643,654,657,660,666,669,672,675,678,681,684,693,696,699,702,708,711,714,652,663,687,690,705,720,57,59,21,84,58,53,62,24,26,60,64,83,42,66,54,56,55,86,65,63,61,25,85,87])).
% 58.87/58.92 cnf(778,plain,
% 58.87/58.92 (P6(f45(a5,a5),f46(a5,a5),a5)),
% 58.87/58.92 inference(scs_inference,[],[110,69,100])).
% 58.87/58.92 cnf(779,plain,
% 58.87/58.92 (~P1(x7791,f45(a5,a5))),
% 58.87/58.92 inference(scs_inference,[],[778,36])).
% 58.87/58.92 cnf(933,plain,
% 58.87/58.92 (P1(x9331,f74(f46(a88,a88)))),
% 58.87/58.92 inference(scs_inference,[],[619,70,35])).
% 58.87/58.92 cnf(934,plain,
% 58.87/58.92 (~P1(x9341,f46(a88,a88))),
% 58.87/58.92 inference(scs_inference,[],[933,20])).
% 58.87/58.92 cnf(1344,plain,
% 58.87/58.92 (P6(a65,a3,a82)),
% 58.87/58.92 inference(scs_inference,[],[8,4,34,15])).
% 58.87/58.92 cnf(1363,plain,
% 58.87/58.92 (~P6(x13631,a58,a75)+P6(x13631,x13632,a5)),
% 58.87/58.92 inference(scs_inference,[],[14,48,21])).
% 58.87/58.92 cnf(1368,plain,
% 58.87/58.92 (P2(x13681,a5)+~P6(f41(x13681,a5),a58,a75)),
% 58.87/58.92 inference(scs_inference,[],[1363,99])).
% 58.87/58.92 cnf(1373,plain,
% 58.87/58.92 (~P2(a86,a75)+P2(x13731,a5)),
% 58.87/58.92 inference(scs_inference,[],[113,1368,94])).
% 58.87/58.92 cnf(1519,plain,
% 58.87/58.92 (P6(x15191,a65,a73)),
% 58.87/58.92 inference(scs_inference,[],[4,15,22])).
% 58.87/58.92 cnf(1548,plain,
% 58.87/58.92 (P1(a68,f74(a62))),
% 58.87/58.92 inference(scs_inference,[],[11,15,17])).
% 58.87/58.92 cnf(1553,plain,
% 58.87/58.92 (~P6(a65,x15531,a5)),
% 58.87/58.92 inference(scs_inference,[],[4,15,36])).
% 58.87/58.92 cnf(1562,plain,
% 58.87/58.92 (~P6(x15621,a62,a81)),
% 58.87/58.92 inference(scs_inference,[],[11,15,27])).
% 58.87/58.92 cnf(1567,plain,
% 58.87/58.92 (~P6(a65,x15671,a83)),
% 58.87/58.92 inference(scs_inference,[],[4,15,37])).
% 58.87/58.92 cnf(1572,plain,
% 58.87/58.92 (~P6(x15721,a62,a84)),
% 58.87/58.92 inference(scs_inference,[],[11,15,28])).
% 58.87/58.92 cnf(1573,plain,
% 58.87/58.92 (~P1(f24(a3,a62),a62)),
% 58.87/58.92 inference(scs_inference,[],[1572,254])).
% 58.87/58.92 cnf(1580,plain,
% 58.87/58.92 (~P6(a65,x15801,a85)),
% 58.87/58.92 inference(scs_inference,[],[4,15,38])).
% 58.87/58.92 cnf(1588,plain,
% 58.87/58.92 (~P6(x15881,a62,a87)),
% 58.87/58.92 inference(scs_inference,[],[11,15,29])).
% 58.87/58.92 cnf(1596,plain,
% 58.87/58.92 (~P6(a65,x15961,a89)),
% 58.87/58.92 inference(scs_inference,[],[4,15,39])).
% 58.87/58.92 cnf(1608,plain,
% 58.87/58.92 (P6(a65,a58,a9)),
% 58.87/58.92 inference(scs_inference,[],[4,581,15,40])).
% 58.87/58.92 cnf(1619,plain,
% 58.87/58.92 (~P6(a62,x16191,a84)),
% 58.87/58.92 inference(scs_inference,[],[11,15,31])).
% 58.87/58.92 cnf(1627,plain,
% 58.87/58.92 (P6(a58,a65,a83)),
% 58.87/58.92 inference(scs_inference,[],[4,14,15,41])).
% 58.87/58.92 cnf(1637,plain,
% 58.87/58.92 (~P6(a62,x16371,a88)),
% 58.87/58.92 inference(scs_inference,[],[11,15,32])).
% 58.87/58.92 cnf(1643,plain,
% 58.87/58.92 (~P6(a62,a3,a10)),
% 58.87/58.92 inference(scs_inference,[],[11,8,15,44])).
% 58.87/58.92 cnf(1652,plain,
% 58.87/58.92 (~P6(a62,a3,a75)),
% 58.87/58.92 inference(scs_inference,[],[11,8,15,45])).
% 58.87/58.92 cnf(1657,plain,
% 58.87/58.92 (P6(a65,a3,a81)),
% 58.87/58.92 inference(scs_inference,[],[4,8,15,77])).
% 58.87/58.92 cnf(1666,plain,
% 58.87/58.92 (P1(f60(a62,a58),a65)),
% 58.87/58.92 inference(scs_inference,[],[14,565,15,76])).
% 58.87/58.92 cnf(1671,plain,
% 58.87/58.92 (~P6(a58,a65,a86)),
% 58.87/58.92 inference(scs_inference,[],[4,14,15,78])).
% 58.87/58.92 cnf(1679,plain,
% 58.87/58.92 (~P6(a3,a62,a10)),
% 58.87/58.92 inference(scs_inference,[],[11,8,15,46])).
% 58.87/58.92 cnf(1759,plain,
% 58.87/58.92 (~P6(a65,a58,a73)),
% 58.87/58.92 inference(scs_inference,[],[4,14,15,79])).
% 58.87/58.92 cnf(1766,plain,
% 58.87/58.92 (P1(f72(a58,a62),a65)),
% 58.87/58.92 inference(scs_inference,[],[14,568,15,76])).
% 58.87/58.92 cnf(1771,plain,
% 58.87/58.92 (P6(a58,a65,a89)),
% 58.87/58.92 inference(scs_inference,[],[4,14,11,15,74])).
% 58.87/58.92 cnf(1782,plain,
% 58.87/58.92 (P6(a62,a3,a87)),
% 58.87/58.92 inference(scs_inference,[],[11,8,4,15,90])).
% 58.87/58.92 cnf(1809,plain,
% 58.87/58.92 (P6(a58,a62,a89)),
% 58.87/58.92 inference(scs_inference,[],[11,14,4,15,74])).
% 58.87/58.92 cnf(1813,plain,
% 58.87/58.92 (P6(a65,a3,a87)),
% 58.87/58.92 inference(scs_inference,[],[4,8,11,15,90])).
% 58.87/58.92 cnf(1826,plain,
% 58.87/58.92 (~P1(f19(a62,a3),a62)),
% 58.87/58.92 inference(scs_inference,[],[11,8,1652,4,15,107])).
% 58.87/58.92 cnf(1876,plain,
% 58.87/58.92 (~P6(a59,a3,a10)+~P1(a63,a56)),
% 58.87/58.92 inference(scs_inference,[],[8,18,44])).
% 58.87/58.92 cnf(1880,plain,
% 58.87/58.92 (~P2(a80,a10)+~P1(a63,a56)),
% 58.87/58.92 inference(scs_inference,[],[122,1876,94])).
% 58.87/58.92 cnf(1899,plain,
% 58.87/58.92 (~P6(a56,a3,a75)+~P1(a64,a59)),
% 58.87/58.92 inference(scs_inference,[],[8,18,45])).
% 58.87/58.92 cnf(1904,plain,
% 58.87/58.92 (~P2(a80,a75)+~P1(a64,a59)),
% 58.87/58.92 inference(scs_inference,[],[122,1899,94])).
% 58.87/58.92 cnf(4755,plain,
% 58.87/58.92 (~P2(a86,a75)),
% 58.87/58.92 inference(scs_inference,[],[1553,1519,1373,94])).
% 58.87/58.92 cnf(4765,plain,
% 58.87/58.92 (~P2(a80,a10)+~P6(a56,a3,a10)),
% 58.87/58.92 inference(scs_inference,[],[8,1880,44])).
% 58.87/58.92 cnf(4766,plain,
% 58.87/58.92 (~P2(a80,a10)),
% 58.87/58.92 inference(scs_inference,[],[122,4765,94])).
% 58.87/58.92 cnf(4767,plain,
% 58.87/58.92 (~P2(a80,a75)+~P6(a59,a3,a75)),
% 58.87/58.92 inference(scs_inference,[],[8,1904,45])).
% 58.87/58.92 cnf(4768,plain,
% 58.87/58.92 (~P2(a80,a75)),
% 58.87/58.92 inference(scs_inference,[],[122,4767,94])).
% 58.87/58.92 cnf(5392,plain,
% 58.87/58.92 (P6(f74(a58),f48(a84,a84),a84)),
% 58.87/58.92 inference(scs_inference,[],[652,581,98])).
% 58.87/58.92 cnf(5394,plain,
% 58.87/58.92 (P1(x53941,f48(a84,a84))),
% 58.87/58.92 inference(rename_variables,[],[652])).
% 58.87/58.92 cnf(5399,plain,
% 58.87/58.92 (P6(f48(a5,a5),f48(a84,a84),a85)),
% 58.87/58.92 inference(scs_inference,[],[652,5394,581,643,934,98,80,93])).
% 58.87/58.92 cnf(5671,plain,
% 58.87/58.92 (~P6(x56711,a71,a81)),
% 58.87/58.92 inference(scs_inference,[],[190,239,246,4766,12,50,51,52,69,70,71,99,102,27])).
% 58.87/58.92 cnf(5675,plain,
% 58.87/58.92 (~P6(x56751,a71,a87)),
% 58.87/58.92 inference(scs_inference,[],[190,239,246,4766,12,1548,50,51,52,69,70,71,99,102,27,37,29])).
% 58.87/58.92 cnf(5679,plain,
% 58.87/58.92 (~P6(a71,x56791,a88)),
% 58.87/58.92 inference(scs_inference,[],[190,239,246,4766,12,1548,50,51,52,69,70,71,99,102,27,37,29,39,32])).
% 58.87/58.92 cnf(5683,plain,
% 58.87/58.92 (~P6(a71,x56831,a84)),
% 58.87/58.92 inference(scs_inference,[],[190,239,246,4766,12,1548,50,51,52,69,70,71,99,102,27,37,29,39,32,38,31])).
% 58.87/58.92 cnf(5685,plain,
% 58.87/58.92 (~P1(f60(a62,a58),f74(a65))),
% 58.87/58.92 inference(scs_inference,[],[190,239,246,4766,12,1666,1548,50,51,52,69,70,71,99,102,27,37,29,39,32,38,31,20])).
% 58.87/58.92 cnf(5687,plain,
% 58.87/58.92 (~P6(x56871,a71,a85)),
% 58.87/58.92 inference(scs_inference,[],[190,239,246,4766,12,1666,1548,50,51,52,69,70,71,99,102,27,37,29,39,32,38,31,20,30])).
% 58.87/58.92 cnf(5691,plain,
% 58.87/58.92 (~P1(f26(a65,a3),a65)),
% 58.87/58.92 inference(scs_inference,[],[190,239,246,4766,12,1666,1548,1813,50,51,52,69,70,71,99,102,27,37,29,39,32,38,31,20,30,36,84])).
% 58.87/58.92 cnf(5693,plain,
% 58.87/58.92 (P6(f74(a62),x56931,a86)),
% 58.87/58.92 inference(scs_inference,[],[190,239,246,4766,12,1666,1548,1813,50,51,52,69,70,71,99,102,27,37,29,39,32,38,31,20,30,36,84,23])).
% 58.87/58.92 cnf(5697,plain,
% 58.87/58.92 (P6(x56971,f74(a62),a73)),
% 58.87/58.92 inference(scs_inference,[],[190,239,246,4766,12,1666,1548,1813,50,51,52,69,70,71,99,102,27,37,29,39,32,38,31,20,30,36,84,23,28,22])).
% 58.87/58.92 cnf(5705,plain,
% 58.87/58.92 (P1(f34(a58,a62),a62)),
% 58.87/58.92 inference(scs_inference,[],[190,239,246,4766,12,1666,1548,1671,1809,1813,1553,50,51,52,69,70,71,99,102,27,37,29,39,32,38,31,20,30,36,84,23,28,22,87,21,24,64])).
% 58.87/58.92 cnf(5711,plain,
% 58.87/58.92 (P1(a66,f74(a62))),
% 58.87/58.92 inference(scs_inference,[],[190,239,246,4766,10,12,1666,1548,1671,1809,1813,1657,1553,50,51,52,69,70,71,99,102,27,37,29,39,32,38,31,20,30,36,84,23,28,22,87,21,24,64,60,56,17])).
% 58.87/58.92 cnf(5750,plain,
% 58.87/58.92 (~P6(f74(a62),a62,a80)),
% 58.87/58.92 inference(scs_inference,[],[125,190,239,246,4766,10,12,479,5392,1666,1548,1562,1567,1759,1671,722,1809,1813,1657,1344,1608,1627,454,478,1519,1553,50,51,52,69,70,71,99,102,27,37,29,39,32,38,31,20,30,36,84,23,28,22,87,21,24,64,60,56,17,25,63,65,54,45,47,48,49,94,77,78,79,41,44,46,34,43])).
% 58.87/58.92 cnf(5752,plain,
% 58.87/58.92 (P1(f60(a56,a58),a56)),
% 58.87/58.92 inference(scs_inference,[],[125,190,239,246,4766,10,12,479,5392,1666,1548,1562,521,1567,1759,1671,722,1809,1813,1657,1344,1608,1627,454,478,1519,1553,14,50,51,52,69,70,71,99,102,27,37,29,39,32,38,31,20,30,36,84,23,28,22,87,21,24,64,60,56,17,25,63,65,54,45,47,48,49,94,77,78,79,41,44,46,34,43,76])).
% 58.87/58.92 cnf(5756,plain,
% 58.87/58.92 (P6(f48(a5,a5),x57561,a80)),
% 58.87/58.92 inference(rename_variables,[],[677])).
% 58.87/58.92 cnf(5759,plain,
% 58.87/58.92 (P1(x57591,a3)),
% 58.87/58.92 inference(rename_variables,[],[8])).
% 58.87/58.92 cnf(5767,plain,
% 58.87/58.92 (P6(f48(a5,a5),x57671,a80)),
% 58.87/58.92 inference(rename_variables,[],[677])).
% 58.87/58.92 cnf(5772,plain,
% 58.87/58.92 (P6(a65,a65,a8)),
% 58.87/58.92 inference(scs_inference,[],[125,190,239,246,4766,10,12,479,5392,5399,1666,1548,1562,521,677,5756,5767,1567,1637,1759,1671,722,1809,1813,1619,1657,1344,1608,1627,454,478,1519,1553,581,8,14,50,51,52,69,70,71,99,102,27,37,29,39,32,38,31,20,30,36,84,23,28,22,87,21,24,64,60,56,17,25,63,65,54,45,47,48,49,94,77,78,79,41,44,46,34,43,76,100,98,101,105,104,33])).
% 58.87/58.92 cnf(5775,plain,
% 58.87/58.92 (P1(x57751,a3)),
% 58.87/58.92 inference(rename_variables,[],[8])).
% 58.87/58.92 cnf(5779,plain,
% 58.87/58.92 (P1(x57791,a3)),
% 58.87/58.92 inference(rename_variables,[],[8])).
% 58.87/58.92 cnf(5780,plain,
% 58.87/58.92 (P1(x57801,a3)),
% 58.87/58.92 inference(rename_variables,[],[8])).
% 58.87/58.92 cnf(5796,plain,
% 58.87/58.92 (P6(a65,a3,a90)),
% 58.87/58.92 inference(scs_inference,[],[125,190,239,246,4766,10,12,479,5392,5399,1666,1548,1562,1588,521,677,5756,5767,1567,1596,1637,1759,1671,722,1809,1813,1679,1619,1657,1344,1608,1627,454,478,1580,1519,1553,581,8,5759,5775,5780,5779,11,14,50,51,52,69,70,71,99,102,27,37,29,39,32,38,31,20,30,36,84,23,28,22,87,21,24,64,60,56,17,25,63,65,54,45,47,48,49,94,77,78,79,41,44,46,34,43,76,100,98,101,105,104,33,93,106,74,90,1363,53,81,80,97])).
% 58.87/58.92 cnf(5828,plain,
% 58.87/58.92 (~P6(a65,x58281,a88)),
% 58.87/58.92 inference(scs_inference,[],[285,287,295,4768,5685,5691,5705,99,52,50,70,39,51,31,30,38,32])).
% 58.87/58.92 cnf(5830,plain,
% 58.87/58.92 (~P6(a62,x58301,a83)),
% 58.87/58.92 inference(scs_inference,[],[285,287,295,4768,5685,5691,5705,99,52,50,70,39,51,31,30,38,32,37])).
% 58.87/58.92 cnf(5844,plain,
% 58.87/58.92 (~P1(f72(a58,a62),f74(a65))),
% 58.87/58.92 inference(scs_inference,[],[229,285,287,295,298,4768,1766,5685,5691,5705,99,52,50,70,39,51,31,30,38,32,37,69,29,27,71,102,36,20])).
% 58.87/58.92 cnf(5846,plain,
% 58.87/58.92 (P6(x58461,a62,a73)),
% 58.87/58.92 inference(scs_inference,[],[229,285,287,295,298,4768,1766,5685,5691,5705,99,52,50,70,39,51,31,30,38,32,37,69,29,27,71,102,36,20,22])).
% 58.87/58.92 cnf(5848,plain,
% 58.87/58.92 (P6(a62,x58481,a86)),
% 58.87/58.92 inference(scs_inference,[],[229,285,287,295,298,4768,1766,5685,5691,5705,99,52,50,70,39,51,31,30,38,32,37,69,29,27,71,102,36,20,22,23])).
% 58.87/58.92 cnf(5860,plain,
% 58.87/58.92 (~P1(f17(a65,a3),a65)),
% 58.87/58.92 inference(scs_inference,[],[229,285,287,295,298,4768,5796,1766,5685,5691,5705,1782,1771,99,52,50,70,39,51,31,30,38,32,37,69,29,27,71,102,36,20,22,23,84,28,21,87,64,82])).
% 58.87/58.92 cnf(5866,plain,
% 58.87/58.92 (P1(f24(a3,a62),f74(a62))),
% 58.87/58.92 inference(scs_inference,[],[229,285,287,295,298,4768,5796,1573,1766,5685,5691,5705,1782,1771,99,52,50,70,39,51,31,30,38,32,37,69,29,27,71,102,36,20,22,23,84,28,21,87,64,82,60,57,17])).
% 58.87/58.92 cnf(5869,plain,
% 58.87/58.92 (~P6(x58691,a71,a81)),
% 58.87/58.92 inference(rename_variables,[],[5671])).
% 58.87/58.92 cnf(5880,plain,
% 58.87/58.92 (~P1(x58801,f45(a5,a5))),
% 58.87/58.92 inference(rename_variables,[],[779])).
% 58.87/58.92 cnf(5883,plain,
% 58.87/58.92 (~P1(x58831,f45(a5,a5))),
% 58.87/58.92 inference(rename_variables,[],[779])).
% 58.87/58.92 cnf(5894,plain,
% 58.87/58.92 (~P1(x58941,f45(a5,a5))),
% 58.87/58.92 inference(rename_variables,[],[779])).
% 58.87/58.92 cnf(5900,plain,
% 58.87/58.92 (~P1(x59001,f45(a5,a5))),
% 58.87/58.92 inference(rename_variables,[],[779])).
% 58.87/58.92 cnf(5909,plain,
% 58.87/58.92 (P6(a62,a62,a8)),
% 58.87/58.92 inference(scs_inference,[],[229,285,287,295,298,4768,5671,5869,5679,5796,1573,1766,5685,5693,5691,5705,5711,524,452,10,449,1782,5,1771,581,779,5880,5883,5894,5900,14,99,52,50,70,39,51,31,30,38,32,37,69,29,27,71,102,36,20,22,23,84,28,21,87,64,82,60,57,17,94,47,77,49,48,46,45,44,41,34,43,76,81,101,80,33])).
% 58.87/58.92 cnf(5923,plain,
% 58.87/58.92 (P1(f76(a62,a62),a62)),
% 58.87/58.92 inference(scs_inference,[],[13,229,285,287,295,298,4768,5671,5869,5675,5679,5796,1573,1766,5685,5693,5697,5691,5705,5711,1643,524,452,10,449,1782,5,1771,581,779,5880,5883,5894,5900,8,14,99,52,50,70,39,51,31,30,38,32,37,69,29,27,71,102,36,20,22,23,84,28,21,87,64,82,60,57,17,94,47,77,49,48,46,45,44,41,34,43,76,81,101,80,33,91,106,90,1363,15,53])).
% 58.87/58.92 cnf(5980,plain,
% 58.87/58.92 (~P6(a65,x59801,a88)),
% 58.87/58.92 inference(rename_variables,[],[5828])).
% 58.87/58.92 cnf(5983,plain,
% 58.87/58.92 (P6(x59831,a62,a73)),
% 58.87/58.92 inference(rename_variables,[],[5846])).
% 58.87/58.92 cnf(5988,plain,
% 58.87/58.92 (P1(x59881,f48(a84,a84))),
% 58.87/58.92 inference(rename_variables,[],[652])).
% 58.87/58.92 cnf(5995,plain,
% 58.87/58.92 (P1(x59951,f48(a84,a84))),
% 58.87/58.92 inference(rename_variables,[],[652])).
% 58.87/58.92 cnf(5998,plain,
% 58.87/58.92 (P1(x59981,f48(a84,a84))),
% 58.87/58.92 inference(rename_variables,[],[652])).
% 58.87/58.92 cnf(6028,plain,
% 58.87/58.92 ($false),
% 58.87/58.92 inference(scs_inference,[],[13,278,313,316,4755,5772,5683,5687,5828,5980,5830,5846,5983,5848,5909,1826,5923,5866,5844,5860,5752,5750,546,5671,9,12,1766,6,652,5988,5995,5998,581,14,99,50,52,39,31,70,69,32,71,51,36,29,27,30,38,37,15,20,102,23,22,28,21,17,78,94,79,47,46,49,48,45,44,41,77,34,43,76,101,80,81,75,33,91]),
% 58.87/58.92 ['proof']).
% 58.87/58.92 % SZS output end Proof
% 58.87/58.92 % Total time :58.250000s
%------------------------------------------------------------------------------