%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : NUN059+2 : TPTP v8.2.0. Bugfixed v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n005.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 13:29:35 EDT 2024
% Result : Theorem 58.70s 58.73s
% Output : CNFRefutation 58.73s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : NUN059+2 : TPTP v8.2.0. Bugfixed v7.4.0.
% 0.03/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n005.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Tue Jun 18 21:09:54 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.45/0.62 start to proof:theBenchmark
% 58.65/58.71 %-------------------------------------------
% 58.65/58.71 % File :CSE---1.7
% 58.65/58.71 % Problem :theBenchmark
% 58.65/58.71 % Transform :cnf
% 58.65/58.71 % Format :tptp:raw
% 58.65/58.71 % Command :java -jar mcs_scs.jar %d %s
% 58.65/58.71
% 58.65/58.71 % Result :Theorem 58.030000s
% 58.65/58.71 % Output :CNFRefutation 58.030000s
% 58.65/58.72 %-------------------------------------------
% 58.70/58.73 %------------------------------------------------------------------------------
% 58.70/58.73 % File : NUN059+2 : TPTP v8.2.0. Bugfixed v7.4.0.
% 58.70/58.73 % Domain : Number Theory
% 58.70/58.73 % Problem : Robinson arithmetic: There exists X^2 + Y^2 = Z^2
% 58.70/58.73 % Version : Especial.
% 58.70/58.73 % English :
% 58.70/58.73
% 58.70/58.73 % Refs : [BBJ03] Boolos et al. (2003), Computability and Logic
% 58.70/58.73 % : [Smi07] Smith (2007), An Introduction to Goedel's Theorems
% 58.70/58.73 % : [Lam18] Lampert (2018), Email to Geoff Sutcliffe
% 58.70/58.73 % Source : [Lam18]
% 58.70/58.73 % Names : fermattothepoweroftwo [Lam18]
% 58.70/58.73
% 58.70/58.73 % Status : Theorem
% 58.70/58.73 % Rating : 0.22 v8.2.0, 0.19 v8.1.0, 0.53 v7.5.0, 0.81 v7.4.0
% 58.70/58.73 % Syntax : Number of formulae : 12 ( 0 unt; 0 def)
% 58.70/58.73 % Number of atoms : 49 ( 18 equ)
% 58.70/58.73 % Maximal formula atoms : 5 ( 4 avg)
% 58.70/58.73 % Number of connectives : 51 ( 14 ~; 10 |; 27 &)
% 58.70/58.73 % ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% 58.70/58.73 % Maximal formula depth : 10 ( 8 avg)
% 58.70/58.73 % Maximal term depth : 1 ( 1 avg)
% 58.70/58.73 % Number of predicates : 5 ( 4 usr; 0 prp; 1-3 aty)
% 58.70/58.73 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 58.70/58.73 % Number of variables : 50 ( 23 !; 27 ?)
% 58.70/58.73 % SPC : FOF_THM_RFO_SEQ
% 58.70/58.73
% 58.70/58.73 % Comments : Translated to FOL with equality.
% 58.70/58.73 % Bugfixes : v7.4.0 - Bugfixes in formulae's use if the r1/3 predicate.
% 58.70/58.73 %------------------------------------------------------------------------------
% 58.70/58.73 include('Axioms/NUM008+0.ax').
% 58.70/58.73 %------------------------------------------------------------------------------
% 58.70/58.73 fof(fermattothepoweroftwo,conjecture,
% 58.70/58.73 ? [Y1,Y3,Y2,Y4] :
% 58.70/58.73 ( ? [Y5] :
% 58.70/58.73 ( r4(Y2,Y2,Y5)
% 58.70/58.73 & Y4 = Y5 )
% 58.70/58.73 & ? [Y6] :
% 58.70/58.73 ( r4(Y3,Y3,Y6)
% 58.70/58.73 & ? [Y7] :
% 58.70/58.73 ( r4(Y1,Y1,Y7)
% 58.70/58.73 & r3(Y7,Y6,Y4) ) ) ) ).
% 58.70/58.73
% 58.70/58.73 %------------------------------------------------------------------------------
% 58.70/58.73 %-------------------------------------------
% 58.70/58.73 % Proof found
% 58.70/58.73 % SZS status Theorem for theBenchmark
% 58.70/58.73 % SZS output start Proof
% 58.70/58.74 %ClaNum:63(EqnAxiom:35)
% 58.70/58.74 %VarNum:119(SingletonVarNum:57)
% 58.70/58.74 %MaxLitNum:5
% 58.70/58.74 %MaxfuncDepth:1
% 58.70/58.74 %SharedTerms:1
% 58.70/58.74 %goalClause: 63
% 58.70/58.74 [36]P1(f1(x361))
% 58.70/58.74 [37]P1(f4(x371))
% 58.70/58.74 [38]P1(f5(x381))
% 58.70/58.74 [41]P3(x411,f1(x411),x411)
% 58.70/58.74 [43]P4(x431,f5(x431),f4(x431))
% 58.70/58.74 [39]P2(x391,f6(x392,x391))
% 58.70/58.74 [40]P2(x401,f2(x402,x401))
% 58.70/58.74 [42]P2(f15(x421,x422),f7(x421,x422))
% 58.70/58.74 [44]P3(x441,x442,f15(x441,x442))
% 58.70/58.74 [45]P4(x451,x452,f3(x451,x452))
% 58.70/58.74 [46]P3(x461,f6(x461,x462),f7(x461,x462))
% 58.70/58.74 [47]P4(x471,f2(x471,x472),f16(x471,x472))
% 58.70/58.74 [48]P3(f3(x481,x482),x481,f16(x481,x482))
% 58.70/58.74 [49]P1(x491)+~E(x491,a8)
% 58.70/58.74 [50]~P1(x501)+E(x501,a8)
% 58.70/58.74 [51]E(f11(x511),x511)+E(f9(x511),x511)
% 58.70/58.74 [52]E(f11(x521),x521)+P1(f9(x521))
% 58.70/58.74 [55]P2(f10(x551),f11(x551))+E(f9(x551),x551)
% 58.70/58.74 [57]P2(f10(x571),f11(x571))+P1(f9(x571))
% 58.70/58.74 [53]P2(x531,x532)+~E(x532,f12(x531))
% 58.70/58.74 [54]~P2(x542,x541)+E(x541,f12(x542))
% 58.70/58.74 [59]P3(x591,x592,x593)+~E(x593,f13(x591,x592))
% 58.70/58.74 [60]P4(x601,x602,x603)+~E(x603,f14(x601,x602))
% 58.70/58.74 [61]~P3(x612,x613,x611)+E(x611,f13(x612,x613))
% 58.70/58.74 [62]~P4(x622,x623,x621)+E(x621,f14(x622,x623))
% 58.70/58.74 [56]~P1(x561)+~E(x561,x562)+~P2(x563,x562)
% 58.70/58.74 [58]~P2(x582,x584)+~P2(x581,x583)+E(x581,x582)+~E(x583,x584)
% 58.70/58.74 [63]~E(x631,x632)+~P3(x633,x634,x632)+~P4(x635,x635,x633)+~P4(x636,x636,x634)+~P4(x637,x637,x631)
% 58.70/58.74 %EqnAxiom
% 58.70/58.74 [1]E(x11,x11)
% 58.70/58.74 [2]E(x22,x21)+~E(x21,x22)
% 58.70/58.74 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.70/58.74 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 58.70/58.74 [5]~E(x51,x52)+E(f4(x51),f4(x52))
% 58.70/58.74 [6]~E(x61,x62)+E(f5(x61),f5(x62))
% 58.70/58.74 [7]~E(x71,x72)+E(f6(x71,x73),f6(x72,x73))
% 58.70/58.74 [8]~E(x81,x82)+E(f6(x83,x81),f6(x83,x82))
% 58.70/58.74 [9]~E(x91,x92)+E(f2(x91,x93),f2(x92,x93))
% 58.73/58.74 [10]~E(x101,x102)+E(f2(x103,x101),f2(x103,x102))
% 58.73/58.74 [11]~E(x111,x112)+E(f14(x111,x113),f14(x112,x113))
% 58.73/58.74 [12]~E(x121,x122)+E(f14(x123,x121),f14(x123,x122))
% 58.73/58.74 [13]~E(x131,x132)+E(f15(x131,x133),f15(x132,x133))
% 58.73/58.74 [14]~E(x141,x142)+E(f15(x143,x141),f15(x143,x142))
% 58.73/58.74 [15]~E(x151,x152)+E(f7(x151,x153),f7(x152,x153))
% 58.73/58.74 [16]~E(x161,x162)+E(f7(x163,x161),f7(x163,x162))
% 58.73/58.74 [17]~E(x171,x172)+E(f10(x171),f10(x172))
% 58.73/58.74 [18]~E(x181,x182)+E(f13(x181,x183),f13(x182,x183))
% 58.73/58.74 [19]~E(x191,x192)+E(f13(x193,x191),f13(x193,x192))
% 58.73/58.74 [20]~E(x201,x202)+E(f9(x201),f9(x202))
% 58.73/58.74 [21]~E(x211,x212)+E(f3(x211,x213),f3(x212,x213))
% 58.73/58.74 [22]~E(x221,x222)+E(f3(x223,x221),f3(x223,x222))
% 58.73/58.74 [23]~E(x231,x232)+E(f12(x231),f12(x232))
% 58.73/58.74 [24]~E(x241,x242)+E(f11(x241),f11(x242))
% 58.73/58.74 [25]~E(x251,x252)+E(f16(x251,x253),f16(x252,x253))
% 58.73/58.74 [26]~E(x261,x262)+E(f16(x263,x261),f16(x263,x262))
% 58.73/58.74 [27]~P1(x271)+P1(x272)+~E(x271,x272)
% 58.73/58.74 [28]P4(x282,x283,x284)+~E(x281,x282)+~P4(x281,x283,x284)
% 58.73/58.74 [29]P4(x293,x292,x294)+~E(x291,x292)+~P4(x293,x291,x294)
% 58.73/58.74 [30]P4(x303,x304,x302)+~E(x301,x302)+~P4(x303,x304,x301)
% 58.73/58.74 [31]P3(x312,x313,x314)+~E(x311,x312)+~P3(x311,x313,x314)
% 58.73/58.74 [32]P3(x323,x322,x324)+~E(x321,x322)+~P3(x323,x321,x324)
% 58.73/58.74 [33]P3(x333,x334,x332)+~E(x331,x332)+~P3(x333,x334,x331)
% 58.73/58.74 [34]P2(x342,x343)+~E(x341,x342)+~P2(x341,x343)
% 58.73/58.74 [35]P2(x353,x352)+~E(x351,x352)+~P2(x353,x351)
% 58.73/58.74
% 58.73/58.74 %-------------------------------------------
% 58.73/58.76 cnf(64,plain,
% 58.73/58.76 (P1(a8)),
% 58.73/58.76 inference(equality_inference,[],[49])).
% 58.73/58.76 cnf(65,plain,
% 58.73/58.76 (P2(x651,f12(x651))),
% 58.73/58.76 inference(equality_inference,[],[53])).
% 58.73/58.76 cnf(66,plain,
% 58.73/58.76 (~P1(x661)+~P2(x662,x661)),
% 58.73/58.76 inference(equality_inference,[],[56])).
% 58.73/58.76 cnf(67,plain,
% 58.73/58.76 (E(x671,x672)+~P2(x672,x673)+~P2(x671,x673)),
% 58.73/58.76 inference(equality_inference,[],[58])).
% 58.73/58.76 cnf(68,plain,
% 58.73/58.76 (P3(x681,x682,f13(x681,x682))),
% 58.73/58.76 inference(equality_inference,[],[59])).
% 58.73/58.76 cnf(69,plain,
% 58.73/58.76 (P4(x691,x692,f14(x691,x692))),
% 58.73/58.76 inference(equality_inference,[],[60])).
% 58.73/58.76 cnf(70,plain,
% 58.73/58.76 (~P3(x702,x703,x701)+~P4(x704,x704,x702)+~P4(x705,x705,x703)+~P4(x706,x706,x701)),
% 58.73/58.76 inference(equality_inference,[],[63])).
% 58.73/58.76 cnf(71,plain,
% 58.73/58.76 (~P2(x711,f1(x712))),
% 58.73/58.76 inference(scs_inference,[],[36,66])).
% 58.73/58.76 cnf(75,plain,
% 58.73/58.76 (~E(f12(x751),f1(x752))),
% 58.73/58.76 inference(scs_inference,[],[36,65,66,56,35])).
% 58.73/58.76 cnf(76,plain,
% 58.73/58.76 (P2(x761,f12(x761))),
% 58.73/58.76 inference(rename_variables,[],[65])).
% 58.73/58.76 cnf(77,plain,
% 58.73/58.76 (~P4(x771,x771,f13(f14(x772,x772),f14(x772,x772)))),
% 58.73/58.76 inference(scs_inference,[],[36,68,69,65,66,56,35,70])).
% 58.73/58.76 cnf(78,plain,
% 58.73/58.76 (P3(x781,x782,f13(x781,x782))),
% 58.73/58.76 inference(rename_variables,[],[68])).
% 58.73/58.76 cnf(80,plain,
% 58.73/58.76 (P4(x801,x802,f14(x801,x802))),
% 58.73/58.76 inference(rename_variables,[],[69])).
% 58.73/58.76 cnf(82,plain,
% 58.73/58.76 (P4(x821,x822,f14(x823,x822))+~E(x823,x821)),
% 58.73/58.76 inference(scs_inference,[],[36,68,69,80,65,66,56,35,70,28])).
% 58.73/58.76 cnf(84,plain,
% 58.73/58.76 (P4(x841,x842,f14(x841,x842))),
% 58.73/58.76 inference(rename_variables,[],[69])).
% 58.73/58.76 cnf(85,plain,
% 58.73/58.76 (~P3(f14(x851,x851),f14(x851,x851),f14(x852,x852))),
% 58.73/58.76 inference(scs_inference,[],[36,68,69,80,65,66,56,35,70,28,30,61])).
% 58.73/58.76 cnf(87,plain,
% 58.73/58.76 (P4(x871,x872,f14(x871,x873))+~E(x873,x872)),
% 58.73/58.76 inference(scs_inference,[],[36,68,69,80,84,65,66,56,35,70,28,30,61,29])).
% 58.73/58.76 cnf(88,plain,
% 58.73/58.76 (P3(x881,x882,f13(x883,x882))+~E(x883,x881)),
% 58.73/58.76 inference(scs_inference,[],[36,68,78,69,80,84,65,66,56,35,70,28,30,61,29,31])).
% 58.73/58.76 cnf(89,plain,
% 58.73/58.76 (P3(x891,x892,f13(x891,x893))+~E(x893,x892)),
% 58.73/58.76 inference(scs_inference,[],[36,68,78,69,80,84,65,66,56,35,70,28,30,61,29,31,32])).
% 58.73/58.76 cnf(92,plain,
% 58.73/58.76 (P2(x921,f12(x922))+~E(x922,x921)),
% 58.73/58.76 inference(scs_inference,[],[36,68,78,69,80,84,65,76,66,56,35,70,28,30,61,29,31,32,33,34])).
% 58.73/58.76 cnf(98,plain,
% 58.73/58.76 (~P2(x981,a8)),
% 58.73/58.76 inference(scs_inference,[],[64,66])).
% 58.73/58.76 cnf(103,plain,
% 58.73/58.76 (P3(x1031,f1(x1031),x1031)),
% 58.73/58.76 inference(rename_variables,[],[41])).
% 58.73/58.76 cnf(104,plain,
% 58.73/58.76 (~P3(f14(x1041,x1041),f14(x1041,x1041),f14(x1042,x1042))),
% 58.73/58.76 inference(rename_variables,[],[85])).
% 58.73/58.76 cnf(111,plain,
% 58.73/58.76 (~P4(x1111,x1111,f1(f14(x1112,x1112)))),
% 58.73/58.76 inference(scs_inference,[],[36,77,85,104,69,71,41,103,44,45,42,64,66,56,32,30,33,35,70])).
% 58.73/58.76 cnf(112,plain,
% 58.73/58.76 (P3(x1121,f1(x1121),x1121)),
% 58.73/58.76 inference(rename_variables,[],[41])).
% 58.73/58.76 cnf(118,plain,
% 58.73/58.76 (~P3(f14(x1181,x1181),f14(x1181,x1181),f3(x1182,x1182))),
% 58.73/58.76 inference(scs_inference,[],[36,77,85,104,69,71,41,103,44,45,42,64,66,56,32,30,33,35,70,62,61])).
% 58.73/58.76 cnf(120,plain,
% 58.73/58.76 (P4(x1201,f5(x1202),f4(x1202))+~E(x1202,x1201)),
% 58.73/58.76 inference(scs_inference,[],[36,77,85,104,69,71,41,103,43,44,45,42,64,66,56,32,30,33,35,70,62,61,28])).
% 58.73/58.76 cnf(121,plain,
% 58.73/58.76 (P3(x1211,f1(x1212),x1212)+~E(x1212,x1211)),
% 58.73/58.76 inference(scs_inference,[],[36,77,85,104,69,71,41,103,112,43,44,45,42,64,66,56,32,30,33,35,70,62,61,28,31])).
% 58.73/58.76 cnf(123,plain,
% 58.73/58.76 (P4(x1231,x1232,f4(x1231))+~E(f5(x1231),x1232)),
% 58.73/58.76 inference(scs_inference,[],[36,77,85,104,69,71,41,103,112,43,44,45,42,64,66,56,32,30,33,35,70,62,61,28,31,34,29])).
% 58.73/58.76 cnf(128,plain,
% 58.73/58.76 (~P2(x1281,f4(x1282))),
% 58.73/58.76 inference(scs_inference,[],[37,66])).
% 58.73/58.76 cnf(134,plain,
% 58.73/58.76 (~E(f14(x1341,x1341),f1(f14(x1342,x1342)))),
% 58.73/58.76 inference(scs_inference,[],[36,111,68,118,69,39,37,66,56,33,30])).
% 58.73/58.76 cnf(135,plain,
% 58.73/58.76 (P4(x1351,x1352,f14(x1351,x1352))),
% 58.73/58.76 inference(rename_variables,[],[69])).
% 58.73/58.76 cnf(136,plain,
% 58.73/58.76 (~E(f6(x1361,x1362),a8)),
% 58.73/58.76 inference(scs_inference,[],[36,111,68,118,69,98,39,37,66,56,33,30,35])).
% 58.73/58.76 cnf(137,plain,
% 58.73/58.76 (P2(x1371,f6(x1372,x1371))),
% 58.73/58.76 inference(rename_variables,[],[39])).
% 58.73/58.76 cnf(139,plain,
% 58.73/58.76 (P2(x1391,f6(x1392,x1391))),
% 58.73/58.76 inference(rename_variables,[],[39])).
% 58.73/58.76 cnf(142,plain,
% 58.73/58.76 (~P4(x1421,x1421,f16(f14(x1422,x1422),f14(x1422,x1422)))),
% 58.73/58.76 inference(scs_inference,[],[36,111,68,118,69,135,48,98,39,137,40,37,45,66,56,33,30,35,58,70])).
% 58.73/58.76 cnf(151,plain,
% 58.73/58.76 (P2(x1511,f6(x1512,x1513))+~E(x1513,x1511)),
% 58.73/58.76 inference(scs_inference,[],[36,111,68,118,69,135,47,48,98,39,137,139,40,37,45,66,56,33,30,35,58,70,50,28,34])).
% 58.73/58.76 cnf(156,plain,
% 58.73/58.76 (~P2(x1561,f5(x1562))),
% 58.73/58.76 inference(scs_inference,[],[38,66])).
% 58.73/58.76 cnf(161,plain,
% 58.73/58.76 (P2(x1611,f2(x1612,x1611))),
% 58.73/58.76 inference(rename_variables,[],[40])).
% 58.73/58.76 cnf(168,plain,
% 58.73/58.76 (P2(x1681,f2(x1682,x1681))),
% 58.73/58.76 inference(rename_variables,[],[40])).
% 58.73/58.76 cnf(173,plain,
% 58.73/58.76 (P4(x1731,x1732,f3(x1733,x1732))+~E(x1733,x1731)),
% 58.73/58.76 inference(scs_inference,[],[36,142,69,128,136,38,47,40,161,65,45,66,56,35,30,29,58,62,28])).
% 58.73/58.76 cnf(174,plain,
% 58.73/58.76 (P2(x1741,f2(x1742,x1743))+~E(x1743,x1741)),
% 58.73/58.76 inference(scs_inference,[],[36,142,69,128,136,38,47,40,161,168,65,45,66,56,35,30,29,58,62,28,34])).
% 58.73/58.76 cnf(175,plain,
% 58.73/58.76 (P3(x1751,f6(x1752,x1753),f7(x1752,x1753))+~E(x1752,x1751)),
% 58.73/58.76 inference(scs_inference,[],[36,142,69,128,46,136,38,47,40,161,168,65,45,66,56,35,30,29,58,62,28,34,31])).
% 58.73/58.76 cnf(176,plain,
% 58.73/58.76 (P3(x1761,f1(x1761),x1762)+~E(x1761,x1762)),
% 58.73/58.76 inference(scs_inference,[],[36,142,69,41,128,46,136,38,47,40,161,168,65,45,66,56,35,30,29,58,62,28,34,31,33])).
% 58.73/58.76 cnf(187,plain,
% 58.73/58.76 (~E(a8,f6(x1871,x1872))),
% 58.73/58.76 inference(scs_inference,[],[64,39,56])).
% 58.73/58.76 cnf(190,plain,
% 58.73/58.76 (P2(x1901,f6(x1902,x1901))),
% 58.73/58.76 inference(rename_variables,[],[39])).
% 58.73/58.76 cnf(195,plain,
% 58.73/58.76 (P3(x1951,x1952,f15(x1953,x1952))+~E(x1953,x1951)),
% 58.73/58.76 inference(scs_inference,[],[44,136,156,64,39,190,65,56,35,58,31])).
% 58.73/58.76 cnf(208,plain,
% 58.73/58.76 (~E(f2(x2081,x2082),f1(x2083))),
% 58.73/58.76 inference(scs_inference,[],[118,44,37,42,40,71,56,33,35])).
% 58.73/58.76 cnf(209,plain,
% 58.73/58.76 (P2(x2091,f2(x2092,x2091))),
% 58.73/58.76 inference(rename_variables,[],[40])).
% 58.73/58.76 cnf(214,plain,
% 58.73/58.76 (P4(x2141,x2142,f3(x2141,x2143))+~E(x2143,x2142)),
% 58.73/58.76 inference(scs_inference,[],[118,44,45,37,42,40,209,187,71,65,56,33,35,58,29])).
% 58.73/58.76 cnf(216,plain,
% 58.73/58.76 (~P3(f14(x2161,x2161),f14(x2161,x2161),f3(x2162,x2163))+~E(x2163,x2162)),
% 58.73/58.76 inference(scs_inference,[],[77,118,44,45,37,42,40,209,187,71,65,56,33,35,58,29,30,61])).
% 58.73/58.76 cnf(225,plain,
% 58.73/58.76 (~E(f3(x2251,x2251),f1(f14(x2252,x2252)))),
% 58.73/58.76 inference(scs_inference,[],[111,45,38,42,56,30])).
% 58.73/58.76 cnf(249,plain,
% 58.73/58.76 (~P2(a8,f6(x2491,f6(x2492,x2493)))),
% 58.73/58.76 inference(scs_inference,[],[136,64,42,65,39,156,56,35,58,54])).
% 58.73/58.76 cnf(258,plain,
% 58.73/58.76 (~E(f7(x2581,x2582),a8)),
% 58.73/58.76 inference(scs_inference,[],[42,98,35])).
% 58.73/58.76 cnf(275,plain,
% 58.73/58.76 (P2(x2751,f6(x2752,x2751))),
% 58.73/58.76 inference(rename_variables,[],[39])).
% 58.73/58.76 cnf(280,plain,
% 58.73/58.76 (P3(f3(x2801,x2802),x2803,f16(x2801,x2802))+~E(x2801,x2803)),
% 58.73/58.76 inference(scs_inference,[],[249,48,136,40,39,275,35,58,32])).
% 58.73/58.76 cnf(289,plain,
% 58.73/58.76 (P2(x2891,f12(x2891))),
% 58.73/58.76 inference(rename_variables,[],[65])).
% 58.73/58.76 cnf(294,plain,
% 58.73/58.76 (~P2(a8,f2(x2941,f6(x2942,x2943)))),
% 58.73/58.76 inference(scs_inference,[],[249,136,65,289,40,35,58,54])).
% 58.73/58.76 cnf(296,plain,
% 58.73/58.76 (P4(x2961,f5(x2961),x2962)+~E(f4(x2961),x2962)),
% 58.73/58.76 inference(scs_inference,[],[249,43,136,65,289,40,35,58,54,30])).
% 58.73/58.76 cnf(303,plain,
% 58.73/58.76 (P2(x3031,f2(x3032,x3031))),
% 58.73/58.76 inference(rename_variables,[],[40])).
% 58.73/58.76 cnf(308,plain,
% 58.73/58.76 (~P2(a8,f2(x3081,f7(x3082,x3083)))),
% 58.73/58.76 inference(scs_inference,[],[142,294,45,258,65,40,303,30,35,58,54])).
% 58.73/58.76 cnf(310,plain,
% 58.73/58.76 (P3(x3101,x3102,f15(x3101,x3103))+~E(x3103,x3102)),
% 58.73/58.76 inference(scs_inference,[],[142,294,45,44,258,65,40,303,30,35,58,54,32])).
% 58.73/58.76 cnf(344,plain,
% 58.73/58.76 (E(f4(f5(x3441)),f4(a8))),
% 58.73/58.76 inference(scs_inference,[],[38,5,50])).
% 58.73/58.76 cnf(346,plain,
% 58.73/58.76 (E(f4(a8),f4(f5(x3461)))),
% 58.73/58.76 inference(scs_inference,[],[344,296,2])).
% 58.73/58.76 cnf(350,plain,
% 58.73/58.76 (~P3(f14(x3501,x3501),f14(x3501,x3501),f4(a8))+~E(f5(f5(x3502)),f5(x3502))),
% 58.73/58.76 inference(scs_inference,[],[77,344,296,2,29,30,61])).
% 58.73/58.76 cnf(359,plain,
% 58.73/58.76 (P4(a8,f5(a8),f4(f5(x3591)))),
% 58.73/58.76 inference(scs_inference,[],[346,296])).
% 58.73/58.76 cnf(376,plain,
% 58.73/58.76 (P4(x3761,f5(a8),f4(f5(x3762)))+~E(a8,x3761)),
% 58.73/58.76 inference(scs_inference,[],[308,39,359,35,28])).
% 58.73/58.76 cnf(1415,plain,
% 58.73/58.76 (~E(f5(x14151),x14151)+~P3(f14(x14152,x14152),f14(x14152,x14152),f4(a8))),
% 58.73/58.76 inference(scs_inference,[],[350,6])).
% 58.73/58.76 cnf(1446,plain,
% 58.73/58.76 (~P3(f14(x14461,x14461),f14(x14461,x14461),f4(a8))),
% 58.73/58.76 inference(scs_inference,[],[38,1415,50])).
% 58.73/58.76 cnf(2028,plain,
% 58.73/58.76 (~P4(x20281,x20281,f13(f3(x20282,x20282),f3(x20282,x20282)))),
% 58.73/58.76 inference(scs_inference,[],[45,68,70])).
% 58.73/58.76 cnf(2036,plain,
% 58.73/58.76 (P4(x20361,x20362,f3(x20361,x20362))),
% 58.73/58.76 inference(rename_variables,[],[45])).
% 58.73/58.76 cnf(2037,plain,
% 58.73/58.76 (~P4(x20371,x20371,f1(f3(x20372,x20372)))),
% 58.73/58.76 inference(scs_inference,[],[45,2036,2028,41,30,70])).
% 58.73/58.76 cnf(2042,plain,
% 58.73/58.76 (~P3(f3(x20421,x20421),f3(x20421,x20421),f3(x20422,x20422))),
% 58.73/58.76 inference(scs_inference,[],[45,2036,2028,41,30,70,61])).
% 58.73/58.76 cnf(2049,plain,
% 58.73/58.76 (~E(f3(x20491,x20491),f1(f3(x20492,x20492)))),
% 58.73/58.76 inference(scs_inference,[],[45,2037,2042,41,32,30])).
% 58.73/58.76 cnf(2075,plain,
% 58.73/58.76 (~P3(f3(x20751,x20751),f3(x20751,x20751),f14(x20752,x20752))),
% 58.73/58.76 inference(scs_inference,[],[2028,69,30,61])).
% 58.73/58.76 cnf(2089,plain,
% 58.73/58.76 (~E(f14(x20891,x20891),f1(f3(x20892,x20892)))),
% 58.73/58.76 inference(scs_inference,[],[2037,69,2075,44,33,30])).
% 58.73/58.76 cnf(2824,plain,
% 58.73/58.76 (E(a8,f1(x28241))),
% 58.73/58.76 inference(scs_inference,[],[36,50,2])).
% 58.73/58.76 cnf(2829,plain,
% 58.73/58.76 (P4(f1(x28291),f5(a8),f4(a8))),
% 58.73/58.76 inference(scs_inference,[],[2824,82,87,88,89,120])).
% 58.73/58.76 cnf(2841,plain,
% 58.73/58.76 (P2(f1(x28411),f12(a8))),
% 58.73/58.76 inference(scs_inference,[],[2824,82,87,88,89,120,121,173,175,176,195,214,216,280,310,376,92])).
% 58.73/58.76 cnf(2842,plain,
% 58.73/58.76 (P2(f1(x28421),f6(x28422,a8))),
% 58.73/58.76 inference(scs_inference,[],[2824,82,87,88,89,120,121,173,175,176,195,214,216,280,310,376,92,151])).
% 58.73/58.76 cnf(2843,plain,
% 58.73/58.76 (P2(f1(x28431),f2(x28432,a8))),
% 58.73/58.76 inference(scs_inference,[],[2824,82,87,88,89,120,121,173,175,176,195,214,216,280,310,376,92,151,174])).
% 58.73/58.76 cnf(2844,plain,
% 58.73/58.76 (E(f1(x28441),a8)),
% 58.73/58.76 inference(scs_inference,[],[2824,82,87,88,89,120,121,173,175,176,195,214,216,280,310,376,92,151,174,2])).
% 58.73/58.76 cnf(2872,plain,
% 58.73/58.76 (P2(a8,f12(f1(x28721)))),
% 58.73/58.76 inference(scs_inference,[],[2844,216,151,173,87,310,82,176,92])).
% 58.73/58.76 cnf(2900,plain,
% 58.73/58.76 (E(a8,f1(x29001))),
% 58.73/58.76 inference(rename_variables,[],[2824])).
% 58.73/58.76 cnf(2901,plain,
% 58.73/58.76 (P2(f1(x29011),f12(f1(x29012)))),
% 58.73/58.76 inference(scs_inference,[],[2824,2900,208,2843,2872,67,3,34])).
% 58.73/58.76 cnf(2936,plain,
% 58.73/58.76 (~P2(f12(x29361),f6(x29362,a8))),
% 58.73/58.76 inference(scs_inference,[],[75,2842,67])).
% 58.73/58.76 cnf(2974,plain,
% 58.73/58.76 (~P2(f2(x29741,x29742),f12(a8))),
% 58.73/58.76 inference(scs_inference,[],[208,2841,67])).
% 58.73/58.76 cnf(3634,plain,
% 58.73/58.76 (~P2(f14(x36341,x36341),f12(a8))),
% 58.73/58.76 inference(scs_inference,[],[2824,134,2841,3,67])).
% 58.73/58.76 cnf(3649,plain,
% 58.73/58.76 (~P1(f3(x36491,x36491))),
% 58.73/58.76 inference(scs_inference,[],[2824,225,2842,2841,3634,34,67,3,62,50])).
% 58.73/58.76 cnf(3665,plain,
% 58.73/58.76 (~P2(f3(x36651,x36651),f12(f1(x36652)))),
% 58.73/58.76 inference(scs_inference,[],[2049,2901,67])).
% 58.73/58.76 cnf(3672,plain,
% 58.73/58.76 (~P2(f14(x36721,x36721),f12(f1(x36722)))),
% 58.73/58.76 inference(scs_inference,[],[2089,2901,2872,3665,34,67])).
% 58.73/58.76 cnf(3682,plain,
% 58.73/58.76 (~P4(x36821,x36821,a8)),
% 58.73/58.76 inference(scs_inference,[],[134,2843,2872,3672,34,67,62])).
% 58.73/58.76 cnf(5137,plain,
% 58.73/58.76 (P4(f1(x51371),f2(a8,x51372),f16(a8,x51372))),
% 58.73/58.76 inference(scs_inference,[],[2824,47,65,37,56,28])).
% 58.73/58.76 cnf(5155,plain,
% 58.73/58.76 (~E(f1(x51551),f5(a8))+~E(f4(a8),a8)),
% 58.73/58.76 inference(scs_inference,[],[2829,3682,5137,29,30,28])).
% 58.73/58.76 cnf(5196,plain,
% 58.73/58.76 (~E(f1(x51961),f5(a8))),
% 58.73/58.76 inference(scs_inference,[],[37,5155,50])).
% 58.73/58.76 cnf(5209,plain,
% 58.73/58.76 (E(f1(x52091),a8)),
% 58.73/58.76 inference(rename_variables,[],[2844])).
% 58.73/58.76 cnf(5211,plain,
% 58.73/58.76 (~P3(f14(x52111,x52111),f14(x52111,x52111),f4(a8))),
% 58.73/58.76 inference(rename_variables,[],[1446])).
% 58.73/58.76 cnf(5216,plain,
% 58.73/58.76 (~P4(x52161,x52161,a8)),
% 58.73/58.76 inference(rename_variables,[],[3682])).
% 58.73/58.76 cnf(5221,plain,
% 58.73/58.76 (~P4(x52211,x52211,a8)),
% 58.73/58.76 inference(rename_variables,[],[3682])).
% 58.73/58.76 cnf(5226,plain,
% 58.73/58.76 (~E(f5(x52261),x52261)),
% 58.73/58.76 inference(scs_inference,[],[3649,2936,2974,5196,3682,5216,5221,1446,5211,37,2843,44,2842,2841,45,39,2844,5209,50,61,62,2,54,34,3,31,32,35,29,67,28,27,30,58,123])).
% 58.73/58.76 cnf(5231,plain,
% 58.73/58.76 ($false),
% 58.73/58.77 inference(scs_inference,[],[5226,38,50]),
% 58.73/58.77 ['proof']).
% 58.73/58.77 % SZS output end Proof
% 58.73/58.77 % Total time :58.030000s
%------------------------------------------------------------------------------