%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : NUN054+2 : TPTP v8.2.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n029.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:34 EDT 2024
% Result : Theorem 58.69s 58.73s
% Output : CNFRefutation 58.69s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : NUN054+2 : TPTP v8.2.0. Released v7.3.0.
% 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n029.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 : Tue Jun 18 21:07:39 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.19/0.55 start to proof:theBenchmark
% 58.69/58.72 %-------------------------------------------
% 58.69/58.72 % File :CSE---1.7
% 58.69/58.72 % Problem :theBenchmark
% 58.69/58.72 % Transform :cnf
% 58.69/58.72 % Format :tptp:raw
% 58.69/58.72 % Command :java -jar mcs_scs.jar %d %s
% 58.69/58.72
% 58.69/58.72 % Result :Theorem 58.130000s
% 58.69/58.72 % Output :CNFRefutation 58.130000s
% 58.69/58.72 %-------------------------------------------
% 58.69/58.73 %------------------------------------------------------------------------------
% 58.69/58.73 % File : NUN054+2 : TPTP v8.2.0. Released v7.3.0.
% 58.69/58.73 % Domain : Number Theory
% 58.69/58.73 % Problem : Robinson arithmetic: 0+1=1
% 58.69/58.73 % Version : Especial.
% 58.69/58.73 % English :
% 58.69/58.73
% 58.69/58.73 % Refs : [BBJ03] Boolos et al. (2003), Computability and Logic
% 58.69/58.73 % : [Smi07] Smith (2007), An Introduction to Goedel's Theorems
% 58.69/58.73 % : [Lam18] Lampert (2018), Email to Geoff Sutcliffe
% 58.69/58.73 % Source : [Lam18]
% 58.69/58.73 % Names : zeroplusoneeqone [Lam18]
% 58.69/58.73
% 58.69/58.73 % Status : Theorem
% 58.69/58.73 % Rating : 0.31 v8.2.0, 0.28 v7.5.0, 0.31 v7.4.0, 0.23 v7.3.0
% 58.69/58.73 % Syntax : Number of formulae : 12 ( 0 unt; 0 def)
% 58.69/58.73 % Number of atoms : 51 ( 18 equ)
% 58.69/58.73 % Maximal formula atoms : 7 ( 4 avg)
% 58.69/58.73 % Number of connectives : 53 ( 14 ~; 10 |; 29 &)
% 58.69/58.73 % ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% 58.69/58.73 % Maximal formula depth : 9 ( 7 avg)
% 58.69/58.73 % Maximal term depth : 1 ( 1 avg)
% 58.69/58.73 % Number of predicates : 5 ( 4 usr; 0 prp; 1-3 aty)
% 58.69/58.73 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 58.69/58.73 % Number of variables : 49 ( 23 !; 26 ?)
% 58.69/58.73 % SPC : FOF_THM_RFO_SEQ
% 58.69/58.73
% 58.69/58.73 % Comments : Translated to FOL with equality.
% 58.69/58.73 %------------------------------------------------------------------------------
% 58.69/58.73 include('Axioms/NUM008+0.ax').
% 58.69/58.73 %------------------------------------------------------------------------------
% 58.69/58.73 fof(zeroplusoneeqone,conjecture,
% 58.69/58.73 ? [Y1] :
% 58.69/58.73 ( ? [Y2] :
% 58.69/58.73 ( ? [Y4] :
% 58.69/58.73 ( r1(Y4)
% 58.69/58.73 & r3(Y4,Y2,Y1) )
% 58.69/58.73 & ? [Y5] :
% 58.69/58.73 ( r1(Y5)
% 58.69/58.73 & r2(Y5,Y2) ) )
% 58.69/58.73 & ? [Y3] :
% 58.69/58.73 ( Y1 = Y3
% 58.69/58.73 & ? [Y6] :
% 58.69/58.73 ( r1(Y6)
% 58.69/58.73 & r2(Y6,Y3) ) ) ) ).
% 58.69/58.73
% 58.69/58.73 %------------------------------------------------------------------------------
% 58.69/58.73 %-------------------------------------------
% 58.69/58.73 % Proof found
% 58.69/58.73 % SZS status Theorem for theBenchmark
% 58.69/58.73 % SZS output start Proof
% 58.69/58.74 %ClaNum:63(EqnAxiom:35)
% 58.69/58.74 %VarNum:117(SingletonVarNum:56)
% 58.69/58.74 %MaxLitNum:7
% 58.69/58.74 %MaxfuncDepth:1
% 58.69/58.74 %SharedTerms:1
% 58.69/58.74 %goalClause: 63
% 58.69/58.74 [36]P1(f1(x361))
% 58.69/58.74 [37]P1(f4(x371))
% 58.69/58.74 [38]P1(f5(x381))
% 58.69/58.74 [41]P3(x411,f1(x411),x411)
% 58.69/58.74 [43]P4(x431,f5(x431),f4(x431))
% 58.69/58.74 [39]P2(x391,f6(x392,x391))
% 58.69/58.74 [40]P2(x401,f2(x402,x401))
% 58.69/58.74 [42]P2(f15(x421,x422),f7(x421,x422))
% 58.69/58.74 [44]P3(x441,x442,f15(x441,x442))
% 58.69/58.74 [45]P4(x451,x452,f3(x451,x452))
% 58.69/58.74 [46]P3(x461,f6(x461,x462),f7(x461,x462))
% 58.69/58.74 [47]P4(x471,f2(x471,x472),f16(x471,x472))
% 58.69/58.74 [48]P3(f3(x481,x482),x481,f16(x481,x482))
% 58.69/58.74 [49]P1(x491)+~E(x491,a8)
% 58.69/58.74 [50]~P1(x501)+E(x501,a8)
% 58.69/58.74 [51]E(f11(x511),x511)+E(f9(x511),x511)
% 58.69/58.74 [52]E(f11(x521),x521)+P1(f9(x521))
% 58.69/58.74 [55]P2(f10(x551),f11(x551))+E(f9(x551),x551)
% 58.69/58.74 [57]P2(f10(x571),f11(x571))+P1(f9(x571))
% 58.69/58.74 [53]P2(x531,x532)+~E(x532,f12(x531))
% 58.69/58.74 [54]~P2(x542,x541)+E(x541,f12(x542))
% 58.69/58.74 [59]P3(x591,x592,x593)+~E(x593,f13(x591,x592))
% 58.69/58.74 [60]P4(x601,x602,x603)+~E(x603,f14(x601,x602))
% 58.69/58.74 [61]~P3(x612,x613,x611)+E(x611,f13(x612,x613))
% 58.69/58.74 [62]~P4(x622,x623,x621)+E(x621,f14(x622,x623))
% 58.69/58.74 [56]~P1(x561)+~E(x561,x562)+~P2(x563,x562)
% 58.69/58.74 [58]~P2(x582,x584)+~P2(x581,x583)+E(x581,x582)+~E(x583,x584)
% 58.69/58.74 [63]~P2(x633,x632)+~P3(x635,x636,x631)+~E(x631,x632)+~P1(x633)+~P2(x634,x636)+~P1(x634)+~P1(x635)
% 58.69/58.74 %EqnAxiom
% 58.69/58.74 [1]E(x11,x11)
% 58.69/58.74 [2]E(x22,x21)+~E(x21,x22)
% 58.69/58.74 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 58.69/58.74 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 58.69/58.74 [5]~E(x51,x52)+E(f4(x51),f4(x52))
% 58.69/58.74 [6]~E(x61,x62)+E(f5(x61),f5(x62))
% 58.69/58.74 [7]~E(x71,x72)+E(f6(x71,x73),f6(x72,x73))
% 58.69/58.74 [8]~E(x81,x82)+E(f6(x83,x81),f6(x83,x82))
% 58.69/58.74 [9]~E(x91,x92)+E(f2(x91,x93),f2(x92,x93))
% 58.69/58.74 [10]~E(x101,x102)+E(f2(x103,x101),f2(x103,x102))
% 58.69/58.74 [11]~E(x111,x112)+E(f14(x111,x113),f14(x112,x113))
% 58.69/58.74 [12]~E(x121,x122)+E(f14(x123,x121),f14(x123,x122))
% 58.69/58.74 [13]~E(x131,x132)+E(f15(x131,x133),f15(x132,x133))
% 58.69/58.74 [14]~E(x141,x142)+E(f15(x143,x141),f15(x143,x142))
% 58.69/58.74 [15]~E(x151,x152)+E(f7(x151,x153),f7(x152,x153))
% 58.69/58.74 [16]~E(x161,x162)+E(f7(x163,x161),f7(x163,x162))
% 58.69/58.74 [17]~E(x171,x172)+E(f10(x171),f10(x172))
% 58.69/58.74 [18]~E(x181,x182)+E(f13(x181,x183),f13(x182,x183))
% 58.69/58.74 [19]~E(x191,x192)+E(f13(x193,x191),f13(x193,x192))
% 58.69/58.74 [20]~E(x201,x202)+E(f9(x201),f9(x202))
% 58.69/58.74 [21]~E(x211,x212)+E(f3(x211,x213),f3(x212,x213))
% 58.69/58.74 [22]~E(x221,x222)+E(f3(x223,x221),f3(x223,x222))
% 58.69/58.74 [23]~E(x231,x232)+E(f12(x231),f12(x232))
% 58.69/58.74 [24]~E(x241,x242)+E(f11(x241),f11(x242))
% 58.69/58.74 [25]~E(x251,x252)+E(f16(x251,x253),f16(x252,x253))
% 58.69/58.74 [26]~E(x261,x262)+E(f16(x263,x261),f16(x263,x262))
% 58.69/58.74 [27]~P1(x271)+P1(x272)+~E(x271,x272)
% 58.69/58.74 [28]P3(x282,x283,x284)+~E(x281,x282)+~P3(x281,x283,x284)
% 58.69/58.74 [29]P3(x293,x292,x294)+~E(x291,x292)+~P3(x293,x291,x294)
% 58.69/58.74 [30]P3(x303,x304,x302)+~E(x301,x302)+~P3(x303,x304,x301)
% 58.69/58.74 [31]P2(x312,x313)+~E(x311,x312)+~P2(x311,x313)
% 58.69/58.74 [32]P2(x323,x322)+~E(x321,x322)+~P2(x323,x321)
% 58.69/58.74 [33]P4(x332,x333,x334)+~E(x331,x332)+~P4(x331,x333,x334)
% 58.69/58.74 [34]P4(x343,x342,x344)+~E(x341,x342)+~P4(x343,x341,x344)
% 58.69/58.74 [35]P4(x353,x354,x352)+~E(x351,x352)+~P4(x353,x354,x351)
% 58.69/58.74
% 58.69/58.74 %-------------------------------------------
% 58.69/58.75 cnf(64,plain,
% 58.69/58.75 (P1(a8)),
% 58.69/58.75 inference(equality_inference,[],[49])).
% 58.69/58.75 cnf(65,plain,
% 58.69/58.75 (P2(x651,f12(x651))),
% 58.69/58.75 inference(equality_inference,[],[53])).
% 58.69/58.75 cnf(66,plain,
% 58.69/58.75 (~P1(x661)+~P2(x662,x661)),
% 58.69/58.75 inference(equality_inference,[],[56])).
% 58.69/58.75 cnf(67,plain,
% 58.69/58.75 (E(x671,x672)+~P2(x672,x673)+~P2(x671,x673)),
% 58.69/58.75 inference(equality_inference,[],[58])).
% 58.69/58.75 cnf(68,plain,
% 58.69/58.75 (P3(x681,x682,f13(x681,x682))),
% 58.69/58.75 inference(equality_inference,[],[59])).
% 58.69/58.75 cnf(69,plain,
% 58.69/58.75 (P4(x691,x692,f14(x691,x692))),
% 58.69/58.75 inference(equality_inference,[],[60])).
% 58.69/58.75 cnf(70,plain,
% 58.69/58.75 (~P1(x702)+~P1(x703)+~P1(x704)+~P2(x702,x701)+~P3(x704,x705,x701)+~P2(x703,x705)),
% 58.69/58.75 inference(equality_inference,[],[63])).
% 58.69/58.75 cnf(71,plain,
% 58.69/58.75 (~P2(x711,f1(x712))),
% 58.69/58.75 inference(scs_inference,[],[36,66])).
% 58.69/58.75 cnf(74,plain,
% 58.69/58.75 (P2(x741,f6(x742,x741))),
% 58.69/58.75 inference(rename_variables,[],[39])).
% 58.69/58.75 cnf(77,plain,
% 58.69/58.75 (P3(x771,x772,f13(x773,x772))+~E(x773,x771)),
% 58.69/58.75 inference(scs_inference,[],[36,39,74,68,66,32,56,28])).
% 58.69/58.75 cnf(78,plain,
% 58.69/58.75 (P3(x781,x782,f13(x781,x783))+~E(x783,x782)),
% 58.69/58.75 inference(scs_inference,[],[36,39,74,68,66,32,56,28,29])).
% 58.69/58.75 cnf(80,plain,
% 58.69/58.75 (P2(x801,f6(x802,x803))+~E(x803,x801)),
% 58.69/58.75 inference(scs_inference,[],[36,39,74,68,66,32,56,28,29,30,31])).
% 58.69/58.75 cnf(81,plain,
% 58.69/58.75 (P4(x811,x812,f14(x813,x812))+~E(x813,x811)),
% 58.69/58.75 inference(scs_inference,[],[36,39,74,68,69,66,32,56,28,29,30,31,33])).
% 58.69/58.75 cnf(82,plain,
% 58.69/58.75 (P4(x821,x822,f14(x821,x823))+~E(x823,x822)),
% 58.69/58.75 inference(scs_inference,[],[36,39,74,68,69,66,32,56,28,29,30,31,33,34])).
% 58.69/58.75 cnf(89,plain,
% 58.69/58.75 (~P2(x891,a8)),
% 58.69/58.75 inference(scs_inference,[],[64,66])).
% 58.69/58.75 cnf(91,plain,
% 58.69/58.75 (~E(a8,f6(x911,x912))),
% 58.69/58.75 inference(scs_inference,[],[39,64,66,56])).
% 58.69/58.75 cnf(94,plain,
% 58.69/58.75 (P2(x941,f12(x941))),
% 58.69/58.75 inference(rename_variables,[],[65])).
% 58.69/58.75 cnf(99,plain,
% 58.69/58.75 (~P2(f6(x991,a8),f6(x991,a8))),
% 58.69/58.75 inference(scs_inference,[],[39,65,94,64,71,66,56,32,58,54])).
% 58.69/58.75 cnf(101,plain,
% 58.69/58.75 (P4(x1011,f5(x1011),x1012)+~E(f4(x1011),x1012)),
% 58.69/58.75 inference(scs_inference,[],[39,65,94,64,71,43,66,56,32,58,54,35])).
% 58.69/58.75 cnf(102,plain,
% 58.69/58.75 (P4(x1021,x1022,f4(x1021))+~E(f5(x1021),x1022)),
% 58.69/58.75 inference(scs_inference,[],[39,65,94,64,71,43,66,56,32,58,54,35,34])).
% 58.69/58.75 cnf(103,plain,
% 58.69/58.75 (P4(x1031,f5(x1032),f4(x1032))+~E(x1032,x1031)),
% 58.69/58.75 inference(scs_inference,[],[39,65,94,64,71,43,66,56,32,58,54,35,34,33])).
% 58.69/58.75 cnf(104,plain,
% 58.69/58.75 (P3(x1041,f1(x1041),x1042)+~E(x1041,x1042)),
% 58.69/58.75 inference(scs_inference,[],[39,65,94,41,64,71,43,66,56,32,58,54,35,34,33,30])).
% 58.69/58.75 cnf(105,plain,
% 58.69/58.75 (P3(x1051,x1052,x1051)+~E(f1(x1051),x1052)),
% 58.69/58.75 inference(scs_inference,[],[39,65,94,41,64,71,43,66,56,32,58,54,35,34,33,30,29])).
% 58.69/58.75 cnf(106,plain,
% 58.69/58.75 (P3(x1061,f1(x1062),x1062)+~E(x1062,x1061)),
% 58.69/58.75 inference(scs_inference,[],[39,65,94,41,64,71,43,66,56,32,58,54,35,34,33,30,29,28])).
% 58.69/58.75 cnf(113,plain,
% 58.69/58.75 (~P2(x1131,f4(x1132))),
% 58.69/58.75 inference(scs_inference,[],[37,66])).
% 58.69/58.75 cnf(118,plain,
% 58.69/58.75 (P2(x1181,f6(x1182,x1181))),
% 58.69/58.75 inference(rename_variables,[],[39])).
% 58.69/58.75 cnf(123,plain,
% 58.69/58.75 (~E(f6(x1231,a8),a8)),
% 58.69/58.75 inference(scs_inference,[],[39,118,99,40,91,37,66,56,32,58,8])).
% 58.69/58.75 cnf(127,plain,
% 58.69/58.75 (P2(x1271,f7(x1272,x1273))+~E(f15(x1272,x1273),x1271)),
% 58.69/58.75 inference(scs_inference,[],[39,118,99,42,40,47,91,37,66,56,32,58,8,35,50,31])).
% 58.69/58.75 cnf(129,plain,
% 58.69/58.75 (P4(x1291,f2(x1292,x1293),f16(x1292,x1293))+~E(x1292,x1291)),
% 58.69/58.75 inference(scs_inference,[],[39,118,99,46,42,40,47,91,37,66,56,32,58,8,35,50,31,30,33])).
% 58.69/58.75 cnf(131,plain,
% 58.69/58.75 (P3(x1311,f6(x1312,x1313),f7(x1312,x1313))+~E(x1312,x1311)),
% 58.69/58.75 inference(scs_inference,[],[39,118,99,46,42,40,47,91,37,66,56,32,58,8,35,50,31,30,33,34,28])).
% 58.69/58.75 cnf(143,plain,
% 58.69/58.75 (P2(x1431,f12(x1431))),
% 58.69/58.75 inference(rename_variables,[],[65])).
% 58.69/58.75 cnf(146,plain,
% 58.69/58.75 (P2(x1461,f12(x1461))),
% 58.69/58.75 inference(rename_variables,[],[65])).
% 58.69/58.75 cnf(150,plain,
% 58.69/58.75 (P2(x1501,f12(x1502))+~E(x1502,x1501)),
% 58.69/58.75 inference(scs_inference,[],[39,48,65,143,146,99,45,123,38,66,56,32,58,35,30,31])).
% 58.69/58.75 cnf(151,plain,
% 58.69/58.75 (P3(f3(x1511,x1512),x1513,f16(x1511,x1512))+~E(x1511,x1513)),
% 58.69/58.75 inference(scs_inference,[],[39,48,65,143,146,99,45,123,38,66,56,32,58,35,30,31,29])).
% 58.69/58.75 cnf(153,plain,
% 58.69/58.75 (P4(x1531,x1532,f3(x1531,x1533))+~E(x1533,x1532)),
% 58.69/58.75 inference(scs_inference,[],[39,48,65,143,146,99,45,123,38,66,56,32,58,35,30,31,29,28,34])).
% 58.69/58.75 cnf(164,plain,
% 58.69/58.75 (P2(x1641,f2(x1642,x1641))),
% 58.69/58.75 inference(rename_variables,[],[40])).
% 58.69/58.75 cnf(168,plain,
% 58.69/58.75 (P4(x1681,x1682,f3(x1683,x1682))+~E(x1683,x1681)),
% 58.69/58.75 inference(scs_inference,[],[39,44,42,40,123,113,69,45,32,58,35,30,33])).
% 58.69/58.75 cnf(169,plain,
% 58.69/58.75 (P3(x1691,x1692,f15(x1693,x1692))+~E(x1693,x1691)),
% 58.69/58.75 inference(scs_inference,[],[39,44,42,40,123,113,69,45,32,58,35,30,33,28])).
% 58.69/58.75 cnf(170,plain,
% 58.69/58.75 (P3(x1701,x1702,f15(x1701,x1703))+~E(x1703,x1702)),
% 58.69/58.75 inference(scs_inference,[],[39,44,42,40,123,113,69,45,32,58,35,30,33,28,29])).
% 58.69/58.75 cnf(171,plain,
% 58.69/58.75 (P2(x1711,f2(x1712,x1713))+~E(x1713,x1711)),
% 58.69/58.75 inference(scs_inference,[],[39,44,42,40,164,123,113,69,45,32,58,35,30,33,28,29,31])).
% 58.69/58.75 cnf(190,plain,
% 58.69/58.75 (~E(f7(x1901,x1902),a8)),
% 58.69/58.75 inference(scs_inference,[],[42,89,32])).
% 58.69/58.75 cnf(224,plain,
% 58.69/58.75 (~P3(a8,f6(x2241,a8),f6(x2241,a8))),
% 58.69/58.75 inference(scs_inference,[],[39,64,70])).
% 58.69/58.75 cnf(238,plain,
% 58.69/58.75 (~P3(a8,f6(x2381,a8),f2(x2382,a8))),
% 58.69/58.75 inference(scs_inference,[],[39,224,44,40,64,30,70])).
% 58.69/58.75 cnf(246,plain,
% 58.69/58.75 (~P3(a8,f6(x2461,a8),f12(a8))),
% 58.69/58.75 inference(scs_inference,[],[39,238,68,65,64,30,70])).
% 58.69/58.75 cnf(252,plain,
% 58.69/58.75 (~E(f7(a8,a8),f12(a8))),
% 58.69/58.75 inference(scs_inference,[],[246,46,30])).
% 58.69/58.75 cnf(257,plain,
% 58.69/58.75 (~E(f15(a8,a8),a8)),
% 58.69/58.75 inference(scs_inference,[],[246,46,42,30,54,31])).
% 58.69/58.75 cnf(258,plain,
% 58.69/58.75 (P2(f15(x2581,x2582),f7(x2581,x2582))),
% 58.69/58.75 inference(rename_variables,[],[42])).
% 58.69/58.75 cnf(261,plain,
% 58.69/58.75 (P2(f15(x2611,x2612),f7(x2611,x2612))),
% 58.69/58.75 inference(rename_variables,[],[42])).
% 58.69/58.75 cnf(265,plain,
% 58.69/58.75 (~P1(f15(a8,a8))),
% 58.69/58.75 inference(scs_inference,[],[39,246,46,42,258,261,64,30,54,31,58,70,50])).
% 58.69/58.75 cnf(274,plain,
% 58.69/58.75 (~P1(f11(x2741))+P1(f9(x2741))),
% 58.69/58.75 inference(scs_inference,[],[57,66])).
% 58.69/58.75 cnf(279,plain,
% 58.69/58.75 (~P1(f11(x2791))+E(f9(x2791),a8)),
% 58.69/58.75 inference(scs_inference,[],[274,50])).
% 58.69/58.75 cnf(294,plain,
% 58.69/58.75 (~E(a8,f2(x2941,x2942))),
% 58.69/58.75 inference(scs_inference,[],[40,64,56])).
% 58.69/58.75 cnf(297,plain,
% 58.69/58.75 (P2(x2971,f2(x2972,x2971))),
% 58.69/58.75 inference(rename_variables,[],[40])).
% 58.69/58.75 cnf(300,plain,
% 58.69/58.75 (~P3(a8,f2(x3001,a8),f2(x3001,a8))),
% 58.69/58.75 inference(scs_inference,[],[40,297,39,64,190,56,58,70])).
% 58.69/58.75 cnf(310,plain,
% 58.69/58.75 (P2(x3101,f2(x3102,x3101))),
% 58.69/58.75 inference(rename_variables,[],[40])).
% 58.69/58.75 cnf(311,plain,
% 58.69/58.75 (P2(x3111,f6(x3112,x3111))),
% 58.69/58.75 inference(rename_variables,[],[39])).
% 58.69/58.75 cnf(313,plain,
% 58.69/58.75 (~P3(a8,f2(x3131,a8),f6(x3132,a8))),
% 58.69/58.75 inference(scs_inference,[],[40,310,39,311,300,68,64,257,36,56,30,58,70])).
% 58.69/58.75 cnf(323,plain,
% 58.69/58.75 (P2(x3231,f2(x3232,x3231))),
% 58.69/58.75 inference(rename_variables,[],[40])).
% 58.69/58.75 cnf(326,plain,
% 58.69/58.75 (~P3(a8,f2(x3261,a8),f12(a8))),
% 58.69/58.75 inference(scs_inference,[],[40,323,39,313,44,65,64,37,123,56,30,58,70])).
% 58.69/58.75 cnf(339,plain,
% 58.69/58.75 (~P2(a8,f13(a8,f2(x3391,a8)))),
% 58.69/58.75 inference(scs_inference,[],[40,39,326,68,38,91,56,30,58,54])).
% 58.69/58.75 cnf(344,plain,
% 58.69/58.75 (P2(x3441,f2(x3442,x3441))),
% 58.69/58.75 inference(rename_variables,[],[40])).
% 58.69/58.75 cnf(351,plain,
% 58.69/58.75 (~P3(a8,f2(x3511,a8),f2(x3512,a8))),
% 58.69/58.75 inference(scs_inference,[],[40,344,39,300,44,339,294,32,30,58,61])).
% 58.69/58.75 cnf(719,plain,
% 58.69/58.75 (~P3(x7191,f6(x7192,a8),f6(x7192,a8))+~E(x7191,a8)),
% 58.69/58.75 inference(scs_inference,[],[39,64,49,70])).
% 58.69/58.75 cnf(734,plain,
% 58.69/58.75 (P4(x7341,f5(x7341),a8)),
% 58.69/58.75 inference(scs_inference,[],[37,50,101])).
% 58.69/58.75 cnf(739,plain,
% 58.69/58.75 (P4(x7391,x7392,a8)+~E(f5(x7391),x7392)),
% 58.69/58.75 inference(scs_inference,[],[252,65,734,67,35,34])).
% 58.69/58.75 cnf(740,plain,
% 58.69/58.75 (P4(x7401,f5(x7402),a8)+~E(x7402,x7401)),
% 58.69/58.75 inference(scs_inference,[],[252,65,734,67,35,34,33])).
% 58.69/58.75 cnf(744,plain,
% 58.69/58.75 (P4(x7441,a8,f4(x7441))),
% 58.69/58.76 inference(scs_inference,[],[38,50,102])).
% 58.69/58.76 cnf(747,plain,
% 58.69/58.76 (P4(x7471,a8,f4(x7472))+~E(x7472,x7471)),
% 58.69/58.76 inference(scs_inference,[],[744,34,35,33])).
% 58.69/58.76 cnf(751,plain,
% 58.69/58.76 (P3(x7511,a8,x7511)),
% 58.69/58.76 inference(scs_inference,[],[36,50,105])).
% 58.69/58.76 cnf(752,plain,
% 58.69/58.76 (P3(x7521,a8,x7522)+~E(x7522,x7521)),
% 58.69/58.76 inference(scs_inference,[],[751,28])).
% 58.69/58.76 cnf(754,plain,
% 58.69/58.76 (P3(x7541,a8,x7542)+~E(x7541,x7542)),
% 58.69/58.76 inference(scs_inference,[],[751,28,29,30])).
% 58.69/58.76 cnf(758,plain,
% 58.69/58.76 (P4(x7581,a8,a8)),
% 58.69/58.76 inference(scs_inference,[],[38,50,739])).
% 58.69/58.76 cnf(759,plain,
% 58.69/58.76 (P4(x7591,x7592,a8)+~E(a8,x7592)),
% 58.69/58.76 inference(scs_inference,[],[758,34])).
% 58.69/58.76 cnf(762,plain,
% 58.69/58.76 (P4(x7621,a8,x7622)+~E(a8,x7622)),
% 58.69/58.76 inference(scs_inference,[],[758,35])).
% 58.69/58.76 cnf(773,plain,
% 58.69/58.76 (~P2(f15(a8,a8),f12(a8))),
% 58.69/58.76 inference(scs_inference,[],[257,65,67])).
% 58.69/58.76 cnf(1190,plain,
% 58.69/58.76 (P1(f11(a8))+P1(f9(a8))),
% 58.69/58.76 inference(scs_inference,[],[52,49])).
% 58.69/58.76 cnf(1211,plain,
% 58.69/58.76 (P1(f11(a8))+E(f9(a8),a8)),
% 58.69/58.76 inference(scs_inference,[],[1190,50])).
% 58.69/58.76 cnf(1220,plain,
% 58.69/58.76 (P1(f9(a8))),
% 58.69/58.76 inference(scs_inference,[],[1190,274])).
% 58.69/58.76 cnf(1581,plain,
% 58.69/58.76 (E(f12(x15811),f6(x15812,x15811))),
% 58.69/58.76 inference(scs_inference,[],[39,54,2])).
% 58.69/58.76 cnf(1585,plain,
% 58.69/58.76 (P3(f12(x15851),f1(f12(x15851)),f6(x15852,x15851))),
% 58.69/58.76 inference(scs_inference,[],[1581,77,78,80,104])).
% 58.69/58.76 cnf(1588,plain,
% 58.69/58.76 (P3(f6(x15881,x15882),x15883,f15(f12(x15882),x15883))),
% 58.69/58.76 inference(scs_inference,[],[1581,77,78,80,104,106,150,169])).
% 58.69/58.76 cnf(1591,plain,
% 58.69/58.76 (P4(f6(x15911,x15912),x15913,f14(f12(x15912),x15913))),
% 58.69/58.76 inference(scs_inference,[],[1581,77,78,80,104,106,150,169,170,171,81])).
% 58.69/58.76 cnf(1593,plain,
% 58.69/58.76 (P4(x15931,f6(x15932,x15933),f3(x15931,f12(x15933)))),
% 58.69/58.76 inference(scs_inference,[],[1581,77,78,80,104,106,150,169,170,171,81,82,153])).
% 58.69/58.76 cnf(1594,plain,
% 58.69/58.76 (P4(f6(x15941,x15942),x15943,f3(f12(x15942),x15943))),
% 58.69/58.76 inference(scs_inference,[],[1581,77,78,80,104,106,150,169,170,171,81,82,153,168])).
% 58.69/58.76 cnf(1595,plain,
% 58.69/58.76 (E(f6(x15951,x15952),f12(x15952))),
% 58.69/58.76 inference(scs_inference,[],[1581,77,78,80,104,106,150,169,170,171,81,82,153,168,2])).
% 58.69/58.76 cnf(1599,plain,
% 58.69/58.76 (P3(f6(x15991,x15992),a8,f12(x15992))),
% 58.69/58.76 inference(scs_inference,[],[751,1581,734,77,78,80,104,106,150,169,170,171,81,82,153,168,2,34,33,28])).
% 58.69/58.76 cnf(1600,plain,
% 58.69/58.76 (P3(x16001,a8,x16001)),
% 58.69/58.76 inference(rename_variables,[],[751])).
% 58.69/58.76 cnf(1601,plain,
% 58.69/58.76 (P3(x16011,f12(x16012),f7(x16011,x16012))),
% 58.69/58.76 inference(scs_inference,[],[751,46,1581,734,77,78,80,104,106,150,169,170,171,81,82,153,168,2,34,33,28,29])).
% 58.69/58.76 cnf(1603,plain,
% 58.69/58.76 (P3(f12(x16031),a8,f6(x16032,x16031))),
% 58.69/58.76 inference(scs_inference,[],[751,1600,46,1581,734,77,78,80,104,106,150,169,170,171,81,82,153,168,2,34,33,28,29,30])).
% 58.69/58.76 cnf(1617,plain,
% 58.69/58.76 (P4(x16171,f12(x16172),f14(x16171,f6(x16173,x16172)))),
% 58.69/58.76 inference(scs_inference,[],[1595,80,82])).
% 58.69/58.76 cnf(1621,plain,
% 58.69/58.76 (P3(f6(x16211,x16212),f1(f6(x16211,x16212)),f12(x16212))),
% 58.69/58.76 inference(scs_inference,[],[1595,80,82,150,171,81,104])).
% 58.69/58.76 cnf(1622,plain,
% 58.69/58.76 (P4(x16221,f12(x16222),f3(x16221,f6(x16223,x16222)))),
% 58.69/58.76 inference(scs_inference,[],[1595,80,82,150,171,81,104,153])).
% 58.69/58.76 cnf(1626,plain,
% 58.69/58.76 (P3(f12(x16261),f1(f6(x16262,x16261)),f6(x16262,x16261))),
% 58.69/58.76 inference(scs_inference,[],[1595,80,82,150,171,81,104,153,77,169,170,106])).
% 58.69/58.76 cnf(1637,plain,
% 58.69/58.76 (P3(f6(x16371,x16372),a8,f6(x16373,x16372))),
% 58.69/58.76 inference(scs_inference,[],[1585,1601,1595,1599,1581,744,1591,80,82,150,171,81,104,153,77,169,170,106,78,168,34,33,28,29,30])).
% 58.69/58.76 cnf(1649,plain,
% 58.69/58.76 (P3(f12(x16491),f1(f6(x16492,x16491)),f12(x16491))),
% 58.69/58.76 inference(scs_inference,[],[1595,1621,734,1594,34,33,28])).
% 58.69/58.76 cnf(1666,plain,
% 58.69/58.76 (P3(f12(x16661),f1(f6(x16662,x16661)),f6(x16663,x16661))),
% 58.69/58.76 inference(scs_inference,[],[1595,1581,1626,1649,1588,1593,1617,34,33,28,29,30])).
% 58.69/58.76 cnf(1684,plain,
% 58.69/58.76 (P4(x16841,f12(x16842),f3(x16841,f6(x16843,x16842)))),
% 58.69/58.76 inference(rename_variables,[],[1622])).
% 58.69/58.76 cnf(1687,plain,
% 58.69/58.76 (P4(f12(x16871),f12(x16872),f3(f6(x16873,x16871),f6(x16874,x16872)))),
% 58.69/58.76 inference(scs_inference,[],[1595,1581,1666,1622,1684,34,28,33])).
% 58.69/58.76 cnf(1865,plain,
% 58.69/58.76 (P3(f12(x18651),x18652,f6(x18653,x18651))+~E(a8,x18652)),
% 58.69/58.76 inference(scs_inference,[],[1603,1687,35,29])).
% 58.69/58.76 cnf(1898,plain,
% 58.69/58.76 (P3(f6(x18981,x18982),x18983,f6(x18984,x18982))+~E(a8,x18983)),
% 58.69/58.76 inference(scs_inference,[],[1637,29])).
% 58.69/58.76 cnf(1899,plain,
% 58.69/58.76 (P3(f6(x18991,x18992),x18993,f12(x18992))+~E(a8,x18993)),
% 58.69/58.76 inference(scs_inference,[],[1595,1637,29,30])).
% 58.69/58.76 cnf(2029,plain,
% 58.69/58.76 (E(f6(x20291,x20292),f6(x20293,x20292))),
% 58.69/58.76 inference(scs_inference,[],[39,1581,54,3])).
% 58.69/58.76 cnf(2143,plain,
% 58.69/58.76 (E(f9(a8),a8)),
% 58.69/58.76 inference(scs_inference,[],[279,1211])).
% 58.69/58.76 cnf(2148,plain,
% 58.69/58.76 (E(a8,f9(a8))),
% 58.69/58.76 inference(scs_inference,[],[2143,719,2])).
% 58.69/58.76 cnf(2176,plain,
% 58.69/58.76 (P4(x21761,a8,f9(a8))),
% 58.69/58.76 inference(scs_inference,[],[313,751,1595,2143,734,744,719,2,104,150,106,169,153,170,81,82,171,78,77,80,168,28,34,33,35,29,30,131,151,1865,1898,1899,103,129,759,762])).
% 58.69/58.76 cnf(2187,plain,
% 58.69/58.76 (P3(x21871,f9(a8),f15(x21871,a8))),
% 58.69/58.76 inference(scs_inference,[],[2148,104,106,170])).
% 58.69/58.76 cnf(2188,plain,
% 58.69/58.76 (P2(f9(a8),f12(a8))),
% 58.69/58.76 inference(scs_inference,[],[2148,104,106,170,150])).
% 58.69/58.76 cnf(2190,plain,
% 58.69/58.76 (P4(x21901,f9(a8),f3(x21901,a8))),
% 58.69/58.76 inference(scs_inference,[],[2148,104,106,170,150,78,153])).
% 58.69/58.76 cnf(2191,plain,
% 58.69/58.76 (P3(f9(a8),x21911,f15(a8,x21911))),
% 58.69/58.76 inference(scs_inference,[],[2148,104,106,170,150,78,153,169])).
% 58.69/58.76 cnf(2193,plain,
% 58.69/58.76 (P4(f9(a8),x21931,f14(a8,x21931))),
% 58.69/58.76 inference(scs_inference,[],[2148,104,106,170,150,78,153,169,171,81])).
% 58.69/58.76 cnf(2194,plain,
% 58.69/58.76 (P2(f9(a8),f6(x21941,a8))),
% 58.69/58.76 inference(scs_inference,[],[2148,104,106,170,150,78,153,169,171,81,80])).
% 58.69/58.76 cnf(2198,plain,
% 58.69/58.76 (~E(f9(a8),f15(a8,a8))),
% 58.69/58.76 inference(scs_inference,[],[2148,773,104,106,170,150,78,153,169,171,81,80,82,77,168,31])).
% 58.69/58.76 cnf(2224,plain,
% 58.69/58.76 (~P2(f9(a8),f7(a8,a8))),
% 58.69/58.76 inference(scs_inference,[],[42,1595,2198,2187,2191,2190,2193,28,34,33,29,67])).
% 58.69/58.76 cnf(2628,plain,
% 58.69/58.76 (P3(a8,a8,f9(a8))),
% 58.69/58.76 inference(scs_inference,[],[2143,751,744,33,28])).
% 58.69/58.76 cnf(2931,plain,
% 58.69/58.76 (~P3(f4(x29311),f6(x29312,a8),f6(x29312,a8))),
% 58.69/58.76 inference(scs_inference,[],[37,2194,1220,70])).
% 58.69/58.76 cnf(2934,plain,
% 58.69/58.76 (~P3(f4(x29341),f12(a8),f12(a8))),
% 58.69/58.76 inference(scs_inference,[],[37,2188,1220,70])).
% 58.69/58.76 cnf(2940,plain,
% 58.69/58.76 (E(f9(a8),f13(a8,a8))),
% 58.69/58.76 inference(scs_inference,[],[2224,2176,2628,62,127,61])).
% 58.69/58.76 cnf(2944,plain,
% 58.69/58.76 (E(f2(x29441,x29442),f12(x29442))),
% 58.69/58.76 inference(scs_inference,[],[37,2224,2176,2628,40,62,127,61,50,54])).
% 58.69/58.76 cnf(2957,plain,
% 58.69/58.76 (~E(f14(x29571,a8),f12(x29572))),
% 58.69/58.76 inference(scs_inference,[],[37,2224,2931,2934,2176,351,2628,265,2029,1220,2143,40,1595,62,127,61,50,54,27,56,28,29,30,752,754,53])).
% 58.69/58.76 cnf(2972,plain,
% 58.69/58.76 (E(x29721,f13(x29721,a8))),
% 58.69/58.76 inference(scs_inference,[],[2944,758,751,62,752,754,61])).
% 58.69/58.76 cnf(2975,plain,
% 58.69/58.76 (E(f5(x29751),a8)),
% 58.69/58.76 inference(scs_inference,[],[2944,2957,758,751,38,62,752,754,61,2,50])).
% 58.69/58.76 cnf(2977,plain,
% 58.69/58.76 (~E(f13(a8,a8),f15(a8,a8))),
% 58.69/58.76 inference(scs_inference,[],[2944,2957,2940,2198,758,751,38,62,752,754,61,2,50,3])).
% 58.69/58.76 cnf(2997,plain,
% 58.69/58.76 ($false),
% 58.69/58.76 inference(scs_inference,[],[2977,2972,2975,45,44,740,747,62,752,754,61,2]),
% 58.69/58.76 ['proof']).
% 58.69/58.76 % SZS output end Proof
% 58.69/58.76 % Total time :58.130000s
%------------------------------------------------------------------------------