%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : KRS268+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 : n002.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:09:03 EDT 2024
% Result : Theorem 1.20s 1.31s
% Output : CNFRefutation 1.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS268+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.12/0.34 % Computer : n002.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Jun 19 12:27:24 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.52/0.57 start to proof:theBenchmark
% 1.20/1.31 %-------------------------------------------
% 1.20/1.31 % File :CSE---1.7
% 1.20/1.31 % Problem :theBenchmark
% 1.20/1.31 % Transform :cnf
% 1.20/1.31 % Format :tptp:raw
% 1.20/1.31 % Command :java -jar mcs_scs.jar %d %s
% 1.20/1.31
% 1.20/1.31 % Result :Theorem 0.680000s
% 1.20/1.31 % Output :CNFRefutation 0.680000s
% 1.20/1.31 %-------------------------------------------
% 1.20/1.31 %------------------------------------------------------------------------------
% 1.20/1.31 % File : KRS268+1 : TPTP v8.2.0. Bugfixed v5.4.0.
% 1.20/1.31 % Domain : Knowledge Representation
% 1.20/1.31 % Problem : WCA mighta THM
% 1.20/1.31 % Version : [Sut08] axioms.
% 1.20/1.31 % English :
% 1.20/1.31
% 1.20/1.31 % Refs : [Sut08] Sutcliffe (2008), The SZS Ontologies for Automated Rea
% 1.20/1.31 % Source : [TPTP]
% 1.20/1.31 % Names :
% 1.20/1.31
% 1.20/1.31 % Status : Theorem
% 1.20/1.31 % Rating : 0.19 v8.2.0, 0.13 v8.1.0, 0.14 v7.5.0, 0.19 v7.3.0, 0.29 v7.2.0, 0.17 v7.1.0, 0.25 v7.0.0, 0.07 v6.4.0, 0.14 v6.3.0, 0.23 v6.2.0, 0.36 v6.0.0, 0.50 v5.5.0, 0.54 v5.4.0
% 1.20/1.31 % Syntax : Number of formulae : 33 ( 3 unt; 0 def)
% 1.20/1.31 % Number of atoms : 107 ( 0 equ)
% 1.20/1.31 % Maximal formula atoms : 7 ( 3 avg)
% 1.20/1.31 % Number of connectives : 96 ( 22 ~; 1 |; 35 &)
% 1.20/1.31 % ( 28 <=>; 8 =>; 0 <=; 2 <~>)
% 1.20/1.31 % Maximal formula depth : 10 ( 6 avg)
% 1.20/1.31 % Maximal term depth : 2 ( 1 avg)
% 1.20/1.31 % Number of predicates : 7 ( 7 usr; 0 prp; 2-3 aty)
% 1.20/1.31 % Number of functors : 20 ( 20 usr; 19 con; 0-1 aty)
% 1.20/1.31 % Number of variables : 122 ( 72 !; 50 ?)
% 1.20/1.31 % SPC : FOF_THM_RFO_NEQ
% 1.20/1.31
% 1.20/1.31 % Comments :
% 1.20/1.31 % Bugfixes : v5.4.0 - Added missing axiom in KRS001+1.ax
% 1.20/1.31 %------------------------------------------------------------------------------
% 1.20/1.31 %----Include SZS success ontology nodes
% 1.20/1.31 include('Axioms/KRS001+0.ax').
% 1.20/1.31 %----Include SZS success ontology node relationships
% 1.20/1.31 include('Axioms/KRS001+1.ax').
% 1.20/1.31 %------------------------------------------------------------------------------
% 1.20/1.31 fof(mighta_wca_thm,conjecture,
% 1.20/1.31 mighta(wca,thm) ).
% 1.20/1.31
% 1.20/1.31 %------------------------------------------------------------------------------
% 1.20/1.31 %-------------------------------------------
% 1.20/1.31 % Proof found
% 1.20/1.31 % SZS status Theorem for theBenchmark
% 1.20/1.31 % SZS output start Proof
% 1.20/1.31 %ClaNum:109(EqnAxiom:0)
% 1.20/1.31 %VarNum:590(SingletonVarNum:249)
% 1.20/1.31 %MaxLitNum:6
% 1.20/1.31 %MaxfuncDepth:1
% 1.20/1.31 %SharedTerms:52
% 1.20/1.31 %goalClause: 13
% 1.20/1.31 %singleGoalClaCount:1
% 1.20/1.31 [1]P1(a1,a2)
% 1.20/1.31 [2]P1(a55,a56)
% 1.20/1.31 [3]P1(a55,a59)
% 1.20/1.31 [4]P1(a61,a62)
% 1.20/1.31 [5]P1(a66,a65)
% 1.20/1.31 [6]P1(a67,a69)
% 1.20/1.31 [7]P1(a70,a71)
% 1.20/1.31 [9]~P1(a57,a2)
% 1.20/1.31 [10]~P1(a66,a62)
% 1.20/1.31 [11]~P1(a68,a65)
% 1.20/1.31 [12]~P1(a67,a71)
% 1.20/1.31 [13]~P2(a73,a74)
% 1.20/1.31 [8]P1(x81,a3)
% 1.20/1.31 [14]~P1(x141,a58)
% 1.20/1.31 [18]~P1(a63,a56)+~P1(a64,a59)
% 1.20/1.31 [15]~P1(x151,a62)+P1(x151,a65)
% 1.20/1.31 [17]P1(x171,x172)+P1(x171,f75(x172))
% 1.20/1.31 [20]~P1(x201,x202)+~P1(x201,f75(x202))
% 1.20/1.31 [21]P4(x211,x212,a5)+P1(f4(x211),x211)
% 1.20/1.31 [24]P4(x241,x242,a87)+P1(f6(x241,x242),x242)
% 1.20/1.31 [25]P4(x251,x252,a81)+P1(f31(x251,x252),x251)
% 1.20/1.31 [26]P4(x261,x262,a74)+P1(f7(x261,x262),x261)
% 1.20/1.31 [42]P4(x421,x422,a74)+~P1(f7(x421,x422),x422)
% 1.20/1.31 [50]P3(x501,x502)+P4(f41(x501,x502),f47(x501,x502),x501)
% 1.20/1.31 [51]P5(x511,x512)+P4(f48(x511,x512),f51(x511,x512),x512)
% 1.20/1.31 [52]P5(x521,x522)+P4(f48(x521,x522),f51(x521,x522),x521)
% 1.20/1.31 [53]~P4(x531,x532,a83)+P1(f77(x531,x532),x532)
% 1.20/1.31 [54]~P4(x541,x542,a83)+P1(f77(x541,x542),x541)
% 1.20/1.31 [55]~P4(x551,x552,a10)+P1(f11(x551,x552),x551)
% 1.20/1.31 [56]~P4(x561,x562,a82)+P1(f13(x561,x562),x561)
% 1.20/1.31 [57]~P4(x571,x572,a90)+P1(f15(x571,x572),x571)
% 1.20/1.31 [58]~P4(x581,x582,a90)+P1(f17(x581,x582),x582)
% 1.20/1.31 [59]~P4(x591,x592,a76)+P1(f18(x591,x592),x591)
% 1.20/1.31 [60]~P4(x601,x602,a89)+P1(f20(x601,x602),x601)
% 1.20/1.31 [61]~P4(x611,x612,a91)+P1(f25(x611,x612),x611)
% 1.20/1.31 [62]~P4(x621,x622,a91)+P1(f28(x621,x622),x622)
% 1.20/1.31 [63]~P4(x631,x632,a84)+P1(f33(x631,x632),x632)
% 1.20/1.31 [64]~P4(x641,x642,a73)+P1(f34(x641,x642),x642)
% 1.20/1.31 [65]~P4(x651,x652,a9)+P1(f38(x651,x652),x651)
% 1.20/1.31 [66]~P4(x661,x662,a80)+P1(f42(x661,x662),x662)
% 1.20/1.31 [67]~P4(x671,x672,a80)+P1(f42(x671,x672),x671)
% 1.20/1.31 [68]~P4(x681,x682,a80)+P1(f44(x681,x682),x681)
% 1.20/1.31 [69]~P2(x691,x692)+P4(f45(x691,x692),f46(x691,x692),x692)
% 1.20/1.31 [70]~P2(x701,x702)+P4(f45(x701,x702),f46(x701,x702),x701)
% 1.20/1.31 [71]~P6(x711,x712)+P4(f49(x711,x712),f50(x711,x712),x711)
% 1.20/1.31 [72]~P4(x721,x722,a9)+P1(f38(x721,x722),f75(x722))
% 1.20/1.31 [73]~P4(x731,x732,a80)+P1(f44(x731,x732),f75(x732))
% 1.20/1.31 [82]~P4(x821,x822,a90)+~P1(f17(x821,x822),x821)
% 1.20/1.31 [83]~P4(x831,x832,a76)+~P1(f21(x831,x832),x831)
% 1.20/1.31 [84]~P4(x841,x842,a89)+~P1(f26(x841,x842),x841)
% 1.20/1.31 [85]~P4(x851,x852,a91)+~P1(f28(x851,x852),x851)
% 1.20/1.31 [86]~P4(x861,x862,a91)+~P1(f30(x861,x862),x862)
% 1.20/1.32 [87]~P4(x871,x872,a73)+~P1(f39(x871,x872),x872)
% 1.20/1.32 [99]P3(x991,x992)+~P4(f41(x991,x992),f47(x991,x992),x992)
% 1.20/1.32 [102]~P6(x1021,x1022)+~P4(f49(x1021,x1022),f50(x1021,x1022),x1022)
% 1.20/1.32 [22]~P1(x223,x222)+P4(x221,x222,a81)
% 1.20/1.32 [23]~P1(x233,x231)+P4(x231,x232,a87)
% 1.20/1.32 [27]P1(x271,x272)+~P4(x273,x272,a82)
% 1.20/1.32 [28]P1(x281,x282)+~P4(x283,x282,a85)
% 1.20/1.32 [29]P1(x291,x292)+~P4(x293,x292,a89)
% 1.20/1.32 [30]P1(x301,x302)+~P4(x303,x302,a86)
% 1.20/1.32 [31]P1(x311,x312)+~P4(x312,x313,a85)
% 1.20/1.32 [32]P1(x321,x322)+~P4(x322,x323,a88)
% 1.20/1.32 [36]~P1(x361,x362)+~P4(x362,x363,a5)
% 1.20/1.32 [37]~P1(x371,x372)+~P4(x372,x373,a84)
% 1.20/1.32 [38]~P1(x381,x382)+~P4(x382,x383,a86)
% 1.20/1.32 [39]~P1(x391,x392)+~P4(x392,x393,a73)
% 1.20/1.32 [35]~P4(x353,x352,a88)+P1(x351,f75(x352))
% 1.20/1.32 [76]P4(x761,x762,a8)+P1(f60(x761,x762),x761)+P1(f72(x761,x762),x762)
% 1.20/1.32 [93]P4(x931,x932,a86)+P1(f36(x931,x932),x931)+~P1(f37(x931,x932),x932)
% 1.20/1.32 [98]P4(x981,x982,a85)+~P1(f23(x981,x982),x981)+~P1(f24(x981,x982),x982)
% 1.20/1.32 [101]P4(x1011,x1012,a88)+~P1(f40(x1011,x1012),x1011)+~P1(f43(x1011,x1012),f75(x1012))
% 1.20/1.32 [108]P7(x1081,x1082)+P4(f53(x1081,x1082),f54(x1081,x1082),x1082)+~P4(f53(x1081,x1082),f54(x1081,x1082),x1081)
% 1.20/1.32 [109]P7(x1091,x1092)+P4(f53(x1091,x1092),f54(x1091,x1092),x1091)+~P4(f53(x1091,x1092),f54(x1091,x1092),x1092)
% 1.20/1.32 [34]~P1(x343,x341)+~P1(x343,x342)+P4(x341,x342,a83)
% 1.20/1.32 [43]P1(x431,x432)+~P1(x431,x433)+~P4(x433,x432,a74)
% 1.20/1.32 [44]P1(x441,x442)+~P1(x441,x443)+~P4(x442,x443,a10)
% 1.20/1.32 [45]P1(x451,x452)+~P1(x451,x453)+~P4(x452,x453,a76)
% 1.20/1.32 [46]P1(x461,x462)+~P1(x461,x463)+~P4(x463,x462,a10)
% 1.20/1.32 [47]P1(x471,x472)+~P1(x471,x473)+~P4(x473,x472,a90)
% 1.20/1.32 [48]P1(x481,x482)+~P1(x481,x483)+~P4(x483,x482,a76)
% 1.20/1.32 [49]P1(x491,x492)+~P1(x491,x493)+~P4(x493,x492,a91)
% 1.20/1.32 [40]~P1(x403,x401)+P4(x401,x402,a9)+~P1(x403,f75(x402))
% 1.20/1.32 [41]~P1(x413,x412)+P4(x411,x412,a84)+P1(f32(x411,x412),x411)
% 1.20/1.32 [77]~P1(x773,x771)+P4(x771,x772,a82)+~P1(f14(x771,x772),x772)
% 1.20/1.32 [78]~P1(x783,x782)+~P4(x781,x782,a87)+P1(f29(x781,x782),x781)
% 1.20/1.32 [79]~P1(x793,x791)+~P4(x791,x792,a81)+P1(f52(x791,x792),x792)
% 1.20/1.32 [80]~P1(x803,x801)+~P4(x801,x802,a8)+P1(f78(x801,x802),x802)
% 1.20/1.32 [81]~P1(x813,x812)+~P4(x811,x812,a8)+P1(f79(x811,x812),x811)
% 1.20/1.32 [33]~P1(x333,x332)+~P1(x334,x331)+P4(x331,x332,a8)
% 1.20/1.32 [75]~P7(x754,x753)+P4(x751,x752,x753)+P4(x751,x752,x754)
% 1.20/1.32 [91]~P4(x913,x914,x911)+P6(x911,x912)+P4(x913,x914,x912)
% 1.20/1.32 [94]~P4(x941,x942,x944)+P4(x941,x942,x943)+~P3(x944,x943)
% 1.20/1.32 [100]~P4(x1003,x1004,x1001)+P2(x1001,x1002)+~P4(x1003,x1004,x1002)
% 1.20/1.32 [104]~P4(x1043,x1044,x1041)+~P5(x1041,x1042)+~P4(x1043,x1044,x1042)
% 1.20/1.32 [105]~P4(x1053,x1054,x1051)+~P7(x1051,x1052)+~P4(x1053,x1054,x1052)
% 1.20/1.32 [92]~P1(x923,x921)+P4(x921,x922,a10)+P1(f12(x921,x922),x922)+P1(f12(x921,x922),x921)
% 1.20/1.32 [106]~P1(x1063,x1061)+P4(x1061,x1062,a10)+~P1(f12(x1061,x1062),x1062)+~P1(f12(x1061,x1062),x1061)
% 1.20/1.32 [74]P1(x741,x742)+~P1(x744,x742)+P4(x743,x742,a73)+P1(f35(x743,x742),x743)
% 1.20/1.32 [90]P1(x901,x902)+~P1(x904,x902)+P4(x902,x903,a89)+~P1(f22(x902,x903),x903)
% 1.29/1.32 [88]~P1(x881,x883)+P1(x881,x882)+~P1(x884,x882)+P4(x882,x883,a90)+P1(f16(x882,x883),x882)
% 1.29/1.32 [89]~P1(x894,x891)+~P1(x893,x891)+~P1(x894,x892)+P4(x891,x892,a80)+~P1(x893,f75(x892))
% 1.29/1.32 [96]P1(x961,x962)+~P1(x964,x962)+P4(x962,x963,a76)+P1(f19(x962,x963),x963)+P1(f19(x962,x963),x962)
% 1.29/1.32 [97]~P1(x971,x973)+P1(x971,x972)+~P1(x974,x972)+P4(x972,x973,a90)+~P1(f16(x972,x973),x973)
% 1.29/1.32 [107]P1(x1071,x1072)+~P1(x1074,x1072)+P4(x1072,x1073,a76)+~P1(f19(x1072,x1073),x1073)+~P1(f19(x1072,x1073),x1072)
% 1.29/1.32 [95]~P1(x953,x952)+P1(x951,x952)+P1(x953,x954)+~P1(x955,x954)+P4(x954,x952,a91)+P1(f27(x954,x952),x954)
% 1.29/1.32 [103]~P1(x1033,x1032)+P1(x1031,x1032)+P1(x1033,x1034)+~P1(x1035,x1034)+P4(x1034,x1032,a91)+~P1(f27(x1034,x1032),x1032)
% 1.29/1.32 %EqnAxiom
% 1.29/1.32
% 1.29/1.32 %-------------------------------------------
% 1.29/1.32 cnf(110,plain,
% 1.29/1.32 (P4(a58,x1101,a5)),
% 1.29/1.32 inference(scs_inference,[],[14,21])).
% 1.29/1.32 cnf(111,plain,
% 1.29/1.32 (~P1(x1111,a58)),
% 1.29/1.32 inference(rename_variables,[],[14])).
% 1.29/1.32 cnf(113,plain,
% 1.29/1.32 (P4(x1131,a58,a87)),
% 1.29/1.32 inference(scs_inference,[],[14,111,21,24])).
% 1.29/1.32 cnf(114,plain,
% 1.29/1.32 (~P1(x1141,a58)),
% 1.29/1.32 inference(rename_variables,[],[14])).
% 1.29/1.32 cnf(117,plain,
% 1.29/1.32 (~P1(x1171,a58)),
% 1.29/1.32 inference(rename_variables,[],[14])).
% 1.29/1.32 cnf(120,plain,
% 1.29/1.32 (~P1(x1201,a58)),
% 1.29/1.32 inference(rename_variables,[],[14])).
% 1.29/1.32 cnf(123,plain,
% 1.29/1.32 (P1(x1231,a3)),
% 1.29/1.32 inference(rename_variables,[],[8])).
% 1.29/1.32 cnf(127,plain,
% 1.29/1.32 (~P4(x1271,a58,a83)),
% 1.29/1.32 inference(scs_inference,[],[8,14,111,114,117,120,11,21,24,25,26,42,15,53])).
% 1.29/1.32 cnf(128,plain,
% 1.29/1.32 (~P1(x1281,a58)),
% 1.29/1.32 inference(rename_variables,[],[14])).
% 1.29/1.32 cnf(131,plain,
% 1.29/1.32 (~P1(x1311,a58)),
% 1.29/1.32 inference(rename_variables,[],[14])).
% 1.29/1.32 cnf(133,plain,
% 1.29/1.32 (~P4(a58,x1331,a10)),
% 1.29/1.32 inference(scs_inference,[],[8,14,111,114,117,120,128,131,11,21,24,25,26,42,15,53,54,55])).
% 1.29/1.32 cnf(134,plain,
% 1.29/1.32 (~P1(x1341,a58)),
% 1.29/1.32 inference(rename_variables,[],[14])).
% 1.29/1.32 cnf(137,plain,
% 1.29/1.32 (~P1(x1371,a58)),
% 1.29/1.32 inference(rename_variables,[],[14])).
% 1.29/1.32 cnf(140,plain,
% 1.29/1.32 (~P1(x1401,a58)),
% 1.29/1.32 inference(rename_variables,[],[14])).
% 1.29/1.32 cnf(143,plain,
% 1.29/1.32 (~P1(x1431,a58)),
% 1.29/1.32 inference(rename_variables,[],[14])).
% 1.29/1.32 cnf(146,plain,
% 1.29/1.32 (~P1(x1461,a58)),
% 1.29/1.32 inference(rename_variables,[],[14])).
% 1.29/1.32 cnf(149,plain,
% 1.29/1.32 (~P1(x1491,a58)),
% 1.29/1.32 inference(rename_variables,[],[14])).
% 1.29/1.32 cnf(152,plain,
% 1.29/1.32 (~P1(x1521,a58)),
% 1.29/1.32 inference(rename_variables,[],[14])).
% 1.29/1.32 cnf(155,plain,
% 1.29/1.32 (~P1(x1551,a58)),
% 1.29/1.32 inference(rename_variables,[],[14])).
% 1.29/1.32 cnf(158,plain,
% 1.29/1.32 (~P1(x1581,a58)),
% 1.29/1.32 inference(rename_variables,[],[14])).
% 1.29/1.32 cnf(161,plain,
% 1.29/1.32 (~P1(x1611,a58)),
% 1.29/1.32 inference(rename_variables,[],[14])).
% 1.29/1.32 cnf(164,plain,
% 1.29/1.32 (~P1(x1641,a58)),
% 1.29/1.32 inference(rename_variables,[],[14])).
% 1.29/1.32 cnf(167,plain,
% 1.29/1.32 (~P1(x1671,a58)),
% 1.29/1.32 inference(rename_variables,[],[14])).
% 1.29/1.32 cnf(170,plain,
% 1.29/1.32 (~P1(x1701,a58)),
% 1.29/1.32 inference(rename_variables,[],[14])).
% 1.29/1.32 cnf(173,plain,
% 1.29/1.32 (P1(x1731,a3)),
% 1.29/1.32 inference(rename_variables,[],[8])).
% 1.29/1.32 cnf(176,plain,
% 1.29/1.32 (P1(x1761,a3)),
% 1.29/1.32 inference(rename_variables,[],[8])).
% 1.29/1.32 cnf(179,plain,
% 1.29/1.32 (P1(x1791,a3)),
% 1.29/1.32 inference(rename_variables,[],[8])).
% 1.29/1.32 cnf(182,plain,
% 1.29/1.32 (P1(x1821,a3)),
% 1.29/1.32 inference(rename_variables,[],[8])).
% 1.29/1.32 cnf(185,plain,
% 1.29/1.32 (P1(x1851,a3)),
% 1.29/1.32 inference(rename_variables,[],[8])).
% 1.29/1.32 cnf(188,plain,
% 1.29/1.32 (P1(x1881,a3)),
% 1.29/1.32 inference(rename_variables,[],[8])).
% 1.29/1.32 cnf(197,plain,
% 1.29/1.32 (~P1(x1971,a58)),
% 1.29/1.32 inference(rename_variables,[],[14])).
% 1.29/1.32 cnf(198,plain,
% 1.29/1.32 (P1(x1981,a3)),
% 1.29/1.32 inference(rename_variables,[],[8])).
% 1.29/1.32 cnf(200,plain,
% 1.29/1.32 (~P4(a3,a58,a8)),
% 1.29/1.32 inference(scs_inference,[],[8,123,173,176,179,182,185,188,198,14,111,114,117,120,128,131,134,137,140,143,146,149,152,155,158,161,164,167,170,197,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,100,75,91,93,80])).
% 1.29/1.32 cnf(201,plain,
% 1.29/1.32 (~P1(x2011,a58)),
% 1.29/1.32 inference(rename_variables,[],[14])).
% 1.29/1.32 cnf(211,plain,
% 1.29/1.32 (P1(x2111,a3)),
% 1.29/1.32 inference(rename_variables,[],[8])).
% 1.29/1.32 cnf(212,plain,
% 1.29/1.32 (P1(x2121,a3)),
% 1.29/1.32 inference(rename_variables,[],[8])).
% 1.29/1.32 cnf(214,plain,
% 1.29/1.32 (P4(a3,a3,a85)),
% 1.29/1.32 inference(scs_inference,[],[8,123,173,176,179,182,185,188,198,212,211,14,111,114,117,120,128,131,134,137,140,143,146,149,152,155,158,161,164,167,170,197,201,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,100,75,91,93,80,81,104,105,106,98])).
% 1.29/1.32 cnf(215,plain,
% 1.29/1.32 (P1(x2151,a3)),
% 1.29/1.32 inference(rename_variables,[],[8])).
% 1.29/1.32 cnf(218,plain,
% 1.29/1.32 (P4(a3,x2181,a88)+~P1(f43(a3,x2181),f75(x2181))),
% 1.29/1.32 inference(scs_inference,[],[8,123,173,176,179,182,185,188,198,212,215,211,14,111,114,117,120,128,131,134,137,140,143,146,149,152,155,158,161,164,167,170,197,201,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,100,75,91,93,80,81,104,105,106,98,101])).
% 1.29/1.32 cnf(230,plain,
% 1.29/1.32 (~P4(a58,x2301,a10)),
% 1.29/1.32 inference(rename_variables,[],[133])).
% 1.29/1.32 cnf(234,plain,
% 1.29/1.32 (~P1(x2341,a58)),
% 1.29/1.32 inference(rename_variables,[],[14])).
% 1.29/1.32 cnf(243,plain,
% 1.29/1.32 (P4(x2431,a58,a87)),
% 1.29/1.32 inference(rename_variables,[],[113])).
% 1.29/1.32 cnf(244,plain,
% 1.29/1.32 (P4(a58,x2441,a5)),
% 1.29/1.32 inference(rename_variables,[],[110])).
% 1.29/1.32 cnf(247,plain,
% 1.29/1.32 (P4(x2471,a58,a87)),
% 1.29/1.32 inference(rename_variables,[],[113])).
% 1.29/1.32 cnf(248,plain,
% 1.29/1.32 (P4(a58,x2481,a5)),
% 1.29/1.32 inference(rename_variables,[],[110])).
% 1.29/1.32 cnf(254,plain,
% 1.29/1.32 (P4(a3,x2541,a85)+~P1(f24(a3,x2541),x2541)),
% 1.29/1.32 inference(scs_inference,[],[110,244,248,113,243,247,127,133,230,1,8,14,234,75,80,81,91,105,100,104,98])).
% 1.29/1.32 cnf(449,plain,
% 1.29/1.32 (~P1(a61,f75(a65))),
% 1.29/1.32 inference(scs_inference,[],[4,20,15])).
% 1.29/1.32 cnf(452,plain,
% 1.29/1.32 (~P4(x4521,a65,a88)),
% 1.29/1.32 inference(scs_inference,[],[449,17,35])).
% 1.29/1.32 cnf(461,plain,
% 1.29/1.32 (~P1(f43(a3,a65),f75(a65))),
% 1.29/1.32 inference(scs_inference,[],[452,218])).
% 1.29/1.32 cnf(470,plain,
% 1.29/1.32 (P4(a3,x4701,a87)),
% 1.29/1.32 inference(scs_inference,[],[214,23,28])).
% 1.29/1.32 cnf(515,plain,
% 1.29/1.32 (~P4(a3,x5151,a73)),
% 1.29/1.32 inference(scs_inference,[],[214,39,31])).
% 1.29/1.32 cnf(573,plain,
% 1.29/1.32 (P4(a3,f75(a58),a85)),
% 1.29/1.32 inference(scs_inference,[],[14,254,17])).
% 1.29/1.32 cnf(574,plain,
% 1.29/1.32 (P1(x5741,f75(a58))),
% 1.29/1.32 inference(scs_inference,[],[573,28])).
% 1.29/1.32 cnf(576,plain,
% 1.29/1.32 (P4(a3,a58,a88)),
% 1.29/1.32 inference(scs_inference,[],[573,8,28,101])).
% 1.29/1.32 cnf(595,plain,
% 1.29/1.32 (P1(x5951,f75(a58))),
% 1.29/1.32 inference(rename_variables,[],[574])).
% 1.29/1.32 cnf(598,plain,
% 1.29/1.32 (P1(x5981,f75(a58))),
% 1.29/1.32 inference(rename_variables,[],[574])).
% 1.29/1.32 cnf(601,plain,
% 1.29/1.32 (P1(x6011,f75(a58))),
% 1.29/1.32 inference(rename_variables,[],[574])).
% 1.29/1.32 cnf(604,plain,
% 1.29/1.32 (P1(x6041,f75(a58))),
% 1.29/1.32 inference(rename_variables,[],[574])).
% 1.29/1.32 cnf(607,plain,
% 1.29/1.32 (P1(x6071,f75(a58))),
% 1.29/1.32 inference(rename_variables,[],[574])).
% 1.29/1.32 cnf(610,plain,
% 1.29/1.32 (P1(x6101,f75(a58))),
% 1.29/1.32 inference(rename_variables,[],[574])).
% 1.29/1.32 cnf(613,plain,
% 1.29/1.32 (P1(x6131,f75(a58))),
% 1.29/1.32 inference(rename_variables,[],[574])).
% 1.29/1.32 cnf(616,plain,
% 1.29/1.32 (P1(x6161,f75(a58))),
% 1.29/1.32 inference(rename_variables,[],[574])).
% 1.29/1.32 cnf(617,plain,
% 1.29/1.32 (P1(x6171,a3)),
% 1.29/1.32 inference(rename_variables,[],[8])).
% 1.29/1.32 cnf(623,plain,
% 1.29/1.32 (P1(x6231,f75(a58))),
% 1.29/1.32 inference(rename_variables,[],[574])).
% 1.29/1.32 cnf(631,plain,
% 1.29/1.32 (~P5(a88,a88)),
% 1.29/1.32 inference(scs_inference,[],[576,470,8,574,595,598,601,604,607,610,613,616,127,452,86,84,82,42,83,87,85,98,75,101,100,105,104])).
% 1.29/1.32 cnf(635,plain,
% 1.29/1.32 (P4(a3,f75(a58),a10)),
% 1.29/1.32 inference(scs_inference,[],[576,470,8,617,200,574,595,598,601,604,607,610,613,616,623,127,452,86,84,82,42,83,87,85,98,75,101,100,105,104,91,106])).
% 1.29/1.32 cnf(651,plain,
% 1.29/1.32 (P4(f48(a5,a5),f51(a5,a5),a5)),
% 1.29/1.32 inference(scs_inference,[],[110,51,104])).
% 1.29/1.32 cnf(652,plain,
% 1.29/1.32 (~P1(x6521,f48(a5,a5))),
% 1.29/1.32 inference(scs_inference,[],[651,36])).
% 1.29/1.32 cnf(661,plain,
% 1.29/1.32 (P1(x6611,f75(f51(a88,a88)))),
% 1.29/1.32 inference(scs_inference,[],[631,52,35])).
% 1.29/1.32 cnf(662,plain,
% 1.29/1.32 (~P1(x6621,f51(a88,a88))),
% 1.29/1.32 inference(scs_inference,[],[661,20])).
% 1.29/1.32 cnf(664,plain,
% 1.29/1.32 (P4(f48(a5,a5),x6641,a5)),
% 1.29/1.32 inference(scs_inference,[],[661,652,20,21])).
% 1.29/1.32 cnf(665,plain,
% 1.29/1.32 (~P1(x6651,f48(a5,a5))),
% 1.29/1.32 inference(rename_variables,[],[652])).
% 1.29/1.32 cnf(667,plain,
% 1.29/1.32 (~P4(f48(a5,a5),x6671,a89)),
% 1.29/1.32 inference(scs_inference,[],[661,652,665,20,21,60])).
% 1.29/1.33 cnf(668,plain,
% 1.29/1.33 (~P1(x6681,f48(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[652])).
% 1.29/1.33 cnf(671,plain,
% 1.29/1.33 (~P1(x6711,f48(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[652])).
% 1.29/1.33 cnf(674,plain,
% 1.29/1.33 (~P1(x6741,f48(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[652])).
% 1.29/1.33 cnf(679,plain,
% 1.29/1.33 (~P1(x6791,f48(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[652])).
% 1.29/1.33 cnf(682,plain,
% 1.29/1.33 (~P1(x6821,f48(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[652])).
% 1.29/1.33 cnf(685,plain,
% 1.29/1.33 (~P1(x6851,f48(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[652])).
% 1.29/1.33 cnf(688,plain,
% 1.29/1.33 (~P1(x6881,f48(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[652])).
% 1.29/1.33 cnf(691,plain,
% 1.29/1.33 (~P1(x6911,f48(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[652])).
% 1.29/1.33 cnf(694,plain,
% 1.29/1.33 (~P1(x6941,f48(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[652])).
% 1.29/1.33 cnf(697,plain,
% 1.29/1.33 (~P1(x6971,f48(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[652])).
% 1.29/1.33 cnf(699,plain,
% 1.29/1.33 (P4(f48(a5,a5),x6991,a74)),
% 1.29/1.33 inference(scs_inference,[],[661,652,665,668,671,674,679,682,685,688,691,694,697,20,21,60,66,65,67,58,54,57,55,61,62,25,26])).
% 1.29/1.33 cnf(752,plain,
% 1.29/1.33 (P4(f45(a5,a5),f46(a5,a5),a5)),
% 1.29/1.33 inference(scs_inference,[],[664,69,100])).
% 1.29/1.33 cnf(753,plain,
% 1.29/1.33 (~P1(x7531,f45(a5,a5))),
% 1.29/1.33 inference(scs_inference,[],[752,36])).
% 1.29/1.33 cnf(758,plain,
% 1.29/1.33 (~P1(x7581,f51(a88,a88))),
% 1.29/1.33 inference(rename_variables,[],[662])).
% 1.29/1.33 cnf(761,plain,
% 1.29/1.33 (~P1(x7611,f51(a88,a88))),
% 1.29/1.33 inference(rename_variables,[],[662])).
% 1.29/1.33 cnf(764,plain,
% 1.29/1.33 (~P1(x7641,f51(a88,a88))),
% 1.29/1.33 inference(rename_variables,[],[662])).
% 1.29/1.33 cnf(767,plain,
% 1.29/1.33 (~P1(x7671,f51(a88,a88))),
% 1.29/1.33 inference(rename_variables,[],[662])).
% 1.29/1.33 cnf(770,plain,
% 1.29/1.33 (~P1(x7701,f51(a88,a88))),
% 1.29/1.33 inference(rename_variables,[],[662])).
% 1.29/1.33 cnf(772,plain,
% 1.29/1.33 (P4(f51(a88,a88),x7721,a74)),
% 1.29/1.33 inference(scs_inference,[],[752,662,758,761,764,767,770,36,67,54,57,60,62,66,26])).
% 1.29/1.33 cnf(773,plain,
% 1.29/1.33 (~P1(x7731,f51(a88,a88))),
% 1.29/1.33 inference(rename_variables,[],[662])).
% 1.29/1.33 cnf(776,plain,
% 1.29/1.33 (~P1(x7761,f51(a88,a88))),
% 1.29/1.33 inference(rename_variables,[],[662])).
% 1.29/1.33 cnf(779,plain,
% 1.29/1.33 (~P1(x7791,f51(a88,a88))),
% 1.29/1.33 inference(rename_variables,[],[662])).
% 1.29/1.33 cnf(782,plain,
% 1.29/1.33 (~P1(x7821,f51(a88,a88))),
% 1.29/1.33 inference(rename_variables,[],[662])).
% 1.29/1.33 cnf(785,plain,
% 1.29/1.33 (~P1(x7851,f51(a88,a88))),
% 1.29/1.33 inference(rename_variables,[],[662])).
% 1.29/1.33 cnf(788,plain,
% 1.29/1.33 (~P1(x7881,f51(a88,a88))),
% 1.29/1.33 inference(rename_variables,[],[662])).
% 1.29/1.33 cnf(791,plain,
% 1.29/1.33 (~P1(x7911,f51(a88,a88))),
% 1.29/1.33 inference(rename_variables,[],[662])).
% 1.29/1.33 cnf(794,plain,
% 1.29/1.33 (~P1(x7941,f51(a88,a88))),
% 1.29/1.33 inference(rename_variables,[],[662])).
% 1.29/1.33 cnf(797,plain,
% 1.29/1.33 (~P1(x7971,f51(a88,a88))),
% 1.29/1.33 inference(rename_variables,[],[662])).
% 1.29/1.33 cnf(800,plain,
% 1.29/1.33 (~P1(x8001,f51(a88,a88))),
% 1.29/1.33 inference(rename_variables,[],[662])).
% 1.29/1.33 cnf(803,plain,
% 1.29/1.33 (~P1(x8031,f51(a88,a88))),
% 1.29/1.33 inference(rename_variables,[],[662])).
% 1.29/1.33 cnf(805,plain,
% 1.29/1.33 (P4(x8051,f51(a88,a88),a87)),
% 1.29/1.33 inference(scs_inference,[],[752,662,758,761,764,767,770,773,776,779,782,785,788,791,794,797,800,803,36,67,54,57,60,62,66,26,61,21,65,58,63,56,64,59,55,25,24])).
% 1.29/1.33 cnf(806,plain,
% 1.29/1.33 (~P1(x8061,f51(a88,a88))),
% 1.29/1.33 inference(rename_variables,[],[662])).
% 1.29/1.33 cnf(809,plain,
% 1.29/1.33 (~P1(x8091,f51(a88,a88))),
% 1.29/1.33 inference(rename_variables,[],[662])).
% 1.29/1.33 cnf(813,plain,
% 1.29/1.33 (~P1(x8131,f51(a88,a88))),
% 1.29/1.33 inference(rename_variables,[],[662])).
% 1.29/1.33 cnf(816,plain,
% 1.29/1.33 (~P1(x8161,f51(a88,a88))),
% 1.29/1.33 inference(rename_variables,[],[662])).
% 1.29/1.33 cnf(828,plain,
% 1.29/1.33 (~P4(f48(a5,a5),x8281,a73)),
% 1.29/1.33 inference(scs_inference,[],[1,13,699,752,8,14,574,662,758,761,764,767,770,773,776,779,782,785,788,791,794,797,800,803,806,809,813,816,667,661,36,67,54,57,60,62,66,26,61,21,65,58,63,56,64,59,55,25,24,53,76,93,81,75,101,100])).
% 1.29/1.33 cnf(848,plain,
% 1.29/1.33 (~P1(x8481,f45(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[753])).
% 1.29/1.33 cnf(851,plain,
% 1.29/1.33 (~P1(x8511,f45(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[753])).
% 1.29/1.33 cnf(854,plain,
% 1.29/1.33 (~P1(x8541,f45(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[753])).
% 1.29/1.33 cnf(857,plain,
% 1.29/1.33 (~P1(x8571,f45(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[753])).
% 1.29/1.33 cnf(860,plain,
% 1.29/1.33 (~P1(x8601,f45(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[753])).
% 1.29/1.33 cnf(863,plain,
% 1.29/1.33 (~P1(x8631,f45(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[753])).
% 1.29/1.33 cnf(866,plain,
% 1.29/1.33 (~P1(x8661,f45(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[753])).
% 1.29/1.33 cnf(869,plain,
% 1.29/1.33 (~P1(x8691,f45(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[753])).
% 1.29/1.33 cnf(872,plain,
% 1.29/1.33 (~P1(x8721,f45(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[753])).
% 1.29/1.33 cnf(875,plain,
% 1.29/1.33 (~P1(x8751,f45(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[753])).
% 1.29/1.33 cnf(878,plain,
% 1.29/1.33 (~P1(x8781,f45(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[753])).
% 1.29/1.33 cnf(881,plain,
% 1.29/1.33 (~P1(x8811,f45(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[753])).
% 1.29/1.33 cnf(884,plain,
% 1.29/1.33 (~P1(x8841,f45(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[753])).
% 1.29/1.33 cnf(887,plain,
% 1.29/1.33 (~P1(x8871,f45(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[753])).
% 1.29/1.33 cnf(890,plain,
% 1.29/1.33 (~P1(x8901,f45(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[753])).
% 1.29/1.33 cnf(893,plain,
% 1.29/1.33 (~P1(x8931,f45(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[753])).
% 1.29/1.33 cnf(896,plain,
% 1.29/1.33 (~P1(x8961,f45(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[753])).
% 1.29/1.33 cnf(899,plain,
% 1.29/1.33 (~P1(x8991,f45(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[753])).
% 1.29/1.33 cnf(902,plain,
% 1.29/1.33 (~P1(x9021,f48(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[652])).
% 1.29/1.33 cnf(906,plain,
% 1.29/1.33 (~P1(x9061,f45(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[753])).
% 1.29/1.33 cnf(909,plain,
% 1.29/1.33 (~P1(x9091,f45(a5,a5))),
% 1.29/1.33 inference(rename_variables,[],[753])).
% 1.29/1.33 cnf(920,plain,
% 1.29/1.33 (P4(x9201,f51(a88,a88),a87)),
% 1.29/1.33 inference(rename_variables,[],[805])).
% 1.29/1.33 cnf(928,plain,
% 1.29/1.33 (~P1(x9281,f75(a65))),
% 1.29/1.33 inference(scs_inference,[],[1,828,13,461,635,772,805,920,8,14,652,902,753,848,851,854,857,860,863,866,869,872,875,878,881,884,887,890,893,896,899,906,909,515,62,26,61,56,65,54,58,57,60,66,64,24,59,21,53,63,25,55,76,80,93,81,75,100,105,104,91,74])).
% 1.29/1.33 cnf(945,plain,
% 1.29/1.33 (~P1(x9451,f75(a65))),
% 1.29/1.33 inference(rename_variables,[],[928])).
% 1.29/1.33 cnf(948,plain,
% 1.29/1.33 (~P1(x9481,f75(a65))),
% 1.29/1.33 inference(rename_variables,[],[928])).
% 1.29/1.33 cnf(951,plain,
% 1.29/1.33 (~P1(x9511,f75(a65))),
% 1.29/1.33 inference(rename_variables,[],[928])).
% 1.29/1.33 cnf(954,plain,
% 1.29/1.33 (~P1(x9541,f75(a65))),
% 1.29/1.33 inference(rename_variables,[],[928])).
% 1.29/1.33 cnf(957,plain,
% 1.29/1.33 (~P1(x9571,f75(a65))),
% 1.29/1.33 inference(rename_variables,[],[928])).
% 1.29/1.33 cnf(960,plain,
% 1.29/1.33 (~P1(x9601,f75(a65))),
% 1.29/1.33 inference(rename_variables,[],[928])).
% 1.29/1.33 cnf(963,plain,
% 1.29/1.33 (~P1(x9631,f75(a65))),
% 1.29/1.33 inference(rename_variables,[],[928])).
% 1.29/1.33 cnf(966,plain,
% 1.29/1.33 (~P1(x9661,f75(a65))),
% 1.29/1.33 inference(rename_variables,[],[928])).
% 1.29/1.33 cnf(968,plain,
% 1.29/1.33 ($false),
% 1.29/1.33 inference(scs_inference,[],[928,945,948,951,954,957,960,963,966,11,73,68,62,56,26,57,60,54,17]),
% 1.29/1.33 ['proof']).
% 1.29/1.33 % SZS output end Proof
% 1.29/1.33 % Total time :0.680000s
%------------------------------------------------------------------------------