%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : NUN086+2 : TPTP v8.2.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n018.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:44 EDT 2024
% Result : Theorem 67.09s 67.24s
% Output : CNFRefutation 67.29s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUN086+2 : TPTP v8.2.0. Released v7.3.0.
% 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n018.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:00:24 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.55/0.59 start to proof:theBenchmark
% 67.09/67.22 %-------------------------------------------
% 67.09/67.22 % File :CSE---1.7
% 67.09/67.22 % Problem :theBenchmark
% 67.09/67.22 % Transform :cnf
% 67.09/67.22 % Format :tptp:raw
% 67.09/67.22 % Command :java -jar mcs_scs.jar %d %s
% 67.09/67.22
% 67.09/67.22 % Result :Theorem 66.550000s
% 67.09/67.22 % Output :CNFRefutation 66.550000s
% 67.09/67.22 %-------------------------------------------
% 67.09/67.23 %------------------------------------------------------------------------------
% 67.09/67.23 % File : NUN086+2 : TPTP v8.2.0. Released v7.3.0.
% 67.09/67.23 % Domain : Number Theory
% 67.09/67.23 % Problem : Robinson arithmetic: 0 * 1 = 0
% 67.09/67.23 % Version : Especial.
% 67.09/67.24 % English :
% 67.09/67.24
% 67.09/67.24 % Refs : [BBJ03] Boolos et al. (2003), Computability and Logic
% 67.09/67.24 % : [Smi07] Smith (2007), An Introduction to Goedel's Theorems
% 67.09/67.24 % : [Lam18] Lampert (2018), Email to Geoff Sutcliffe
% 67.09/67.24 % Source : [Lam18]
% 67.09/67.24 % Names : zerotimesoneeqzero [Lam18]
% 67.09/67.24
% 67.09/67.24 % Status : Theorem
% 67.09/67.24 % Rating : 0.31 v8.2.0, 0.28 v7.5.0, 0.31 v7.4.0, 0.20 v7.3.0
% 67.09/67.24 % Syntax : Number of formulae : 12 ( 0 unt; 0 def)
% 67.09/67.24 % Number of atoms : 50 ( 18 equ)
% 67.09/67.24 % Maximal formula atoms : 6 ( 4 avg)
% 67.09/67.24 % Number of connectives : 52 ( 14 ~; 10 |; 28 &)
% 67.09/67.24 % ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% 67.09/67.24 % Maximal formula depth : 9 ( 7 avg)
% 67.09/67.24 % Maximal term depth : 1 ( 1 avg)
% 67.09/67.24 % Number of predicates : 5 ( 4 usr; 0 prp; 1-3 aty)
% 67.09/67.24 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 67.09/67.24 % Number of variables : 48 ( 23 !; 25 ?)
% 67.09/67.24 % SPC : FOF_THM_RFO_SEQ
% 67.09/67.24
% 67.09/67.24 % Comments : Translated to FOL with equality.
% 67.09/67.24 %------------------------------------------------------------------------------
% 67.09/67.24 include('Axioms/NUM008+0.ax').
% 67.09/67.24 %------------------------------------------------------------------------------
% 67.09/67.24 fof(zerotimesoneeqzero,conjecture,
% 67.09/67.24 ? [Y1] :
% 67.09/67.24 ( ? [Y2] :
% 67.09/67.24 ( ? [Y3] :
% 67.09/67.24 ( r1(Y3)
% 67.09/67.24 & r2(Y3,Y2) )
% 67.09/67.24 & ? [Y4] :
% 67.09/67.24 ( r1(Y4)
% 67.09/67.24 & r4(Y4,Y2,Y1) ) )
% 67.09/67.24 & ? [Y5] :
% 67.09/67.24 ( r1(Y5)
% 67.09/67.24 & Y1 = Y5 ) ) ).
% 67.09/67.24
% 67.09/67.24 %------------------------------------------------------------------------------
% 67.09/67.24 %-------------------------------------------
% 67.09/67.24 % Proof found
% 67.09/67.24 % SZS status Theorem for theBenchmark
% 67.09/67.24 % SZS output start Proof
% 67.20/67.25 %ClaNum:63(EqnAxiom:35)
% 67.20/67.25 %VarNum:115(SingletonVarNum:55)
% 67.20/67.25 %MaxLitNum:6
% 67.20/67.25 %MaxfuncDepth:1
% 67.20/67.25 %SharedTerms:1
% 67.20/67.25 %goalClause: 63
% 67.20/67.25 [36]P1(f1(x361))
% 67.20/67.25 [37]P1(f4(x371))
% 67.20/67.25 [38]P1(f5(x381))
% 67.20/67.25 [41]P3(x411,f1(x411),x411)
% 67.20/67.25 [43]P4(x431,f5(x431),f4(x431))
% 67.20/67.25 [39]P2(x391,f6(x392,x391))
% 67.20/67.25 [40]P2(x401,f2(x402,x401))
% 67.20/67.25 [42]P2(f15(x421,x422),f7(x421,x422))
% 67.20/67.25 [44]P3(x441,x442,f15(x441,x442))
% 67.20/67.25 [45]P4(x451,x452,f3(x451,x452))
% 67.20/67.25 [46]P3(x461,f6(x461,x462),f7(x461,x462))
% 67.20/67.25 [47]P4(x471,f2(x471,x472),f16(x471,x472))
% 67.20/67.25 [48]P3(f3(x481,x482),x481,f16(x481,x482))
% 67.20/67.25 [49]P1(x491)+~E(x491,a8)
% 67.20/67.25 [50]~P1(x501)+E(x501,a8)
% 67.20/67.25 [51]E(f11(x511),x511)+E(f9(x511),x511)
% 67.20/67.25 [52]E(f11(x521),x521)+P1(f9(x521))
% 67.20/67.25 [55]P2(f10(x551),f11(x551))+E(f9(x551),x551)
% 67.20/67.25 [57]P2(f10(x571),f11(x571))+P1(f9(x571))
% 67.20/67.25 [53]P2(x531,x532)+~E(x532,f12(x531))
% 67.20/67.25 [54]~P2(x542,x541)+E(x541,f12(x542))
% 67.20/67.25 [59]P3(x591,x592,x593)+~E(x593,f13(x591,x592))
% 67.20/67.25 [60]P4(x601,x602,x603)+~E(x603,f14(x601,x602))
% 67.20/67.25 [61]~P3(x612,x613,x611)+E(x611,f13(x612,x613))
% 67.20/67.25 [62]~P4(x622,x623,x621)+E(x621,f14(x622,x623))
% 67.20/67.25 [56]~P1(x561)+~E(x561,x562)+~P2(x563,x562)
% 67.20/67.25 [58]~P2(x582,x584)+~P2(x581,x583)+E(x581,x582)+~E(x583,x584)
% 67.20/67.25 [63]~P1(x632)+~P4(x633,x635,x631)+~E(x631,x632)+~P2(x634,x635)+~P1(x633)+~P1(x634)
% 67.20/67.25 %EqnAxiom
% 67.20/67.25 [1]E(x11,x11)
% 67.20/67.25 [2]E(x22,x21)+~E(x21,x22)
% 67.20/67.25 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 67.20/67.25 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 67.20/67.25 [5]~E(x51,x52)+E(f4(x51),f4(x52))
% 67.20/67.25 [6]~E(x61,x62)+E(f5(x61),f5(x62))
% 67.20/67.25 [7]~E(x71,x72)+E(f6(x71,x73),f6(x72,x73))
% 67.20/67.25 [8]~E(x81,x82)+E(f6(x83,x81),f6(x83,x82))
% 67.20/67.25 [9]~E(x91,x92)+E(f2(x91,x93),f2(x92,x93))
% 67.20/67.25 [10]~E(x101,x102)+E(f2(x103,x101),f2(x103,x102))
% 67.20/67.25 [11]~E(x111,x112)+E(f14(x111,x113),f14(x112,x113))
% 67.20/67.25 [12]~E(x121,x122)+E(f14(x123,x121),f14(x123,x122))
% 67.20/67.25 [13]~E(x131,x132)+E(f15(x131,x133),f15(x132,x133))
% 67.20/67.25 [14]~E(x141,x142)+E(f15(x143,x141),f15(x143,x142))
% 67.20/67.25 [15]~E(x151,x152)+E(f7(x151,x153),f7(x152,x153))
% 67.20/67.25 [16]~E(x161,x162)+E(f7(x163,x161),f7(x163,x162))
% 67.20/67.25 [17]~E(x171,x172)+E(f10(x171),f10(x172))
% 67.20/67.25 [18]~E(x181,x182)+E(f13(x181,x183),f13(x182,x183))
% 67.20/67.25 [19]~E(x191,x192)+E(f13(x193,x191),f13(x193,x192))
% 67.20/67.25 [20]~E(x201,x202)+E(f9(x201),f9(x202))
% 67.20/67.25 [21]~E(x211,x212)+E(f3(x211,x213),f3(x212,x213))
% 67.20/67.25 [22]~E(x221,x222)+E(f3(x223,x221),f3(x223,x222))
% 67.20/67.25 [23]~E(x231,x232)+E(f12(x231),f12(x232))
% 67.20/67.25 [24]~E(x241,x242)+E(f11(x241),f11(x242))
% 67.20/67.25 [25]~E(x251,x252)+E(f16(x251,x253),f16(x252,x253))
% 67.20/67.25 [26]~E(x261,x262)+E(f16(x263,x261),f16(x263,x262))
% 67.20/67.25 [27]~P1(x271)+P1(x272)+~E(x271,x272)
% 67.20/67.25 [28]P4(x282,x283,x284)+~E(x281,x282)+~P4(x281,x283,x284)
% 67.20/67.25 [29]P4(x293,x292,x294)+~E(x291,x292)+~P4(x293,x291,x294)
% 67.20/67.25 [30]P4(x303,x304,x302)+~E(x301,x302)+~P4(x303,x304,x301)
% 67.20/67.25 [31]P2(x312,x313)+~E(x311,x312)+~P2(x311,x313)
% 67.20/67.25 [32]P2(x323,x322)+~E(x321,x322)+~P2(x323,x321)
% 67.20/67.25 [33]P3(x332,x333,x334)+~E(x331,x332)+~P3(x331,x333,x334)
% 67.20/67.25 [34]P3(x343,x342,x344)+~E(x341,x342)+~P3(x343,x341,x344)
% 67.20/67.25 [35]P3(x353,x354,x352)+~E(x351,x352)+~P3(x353,x354,x351)
% 67.20/67.25
% 67.20/67.25 %-------------------------------------------
% 67.20/67.28 cnf(64,plain,
% 67.20/67.28 (P1(a8)),
% 67.20/67.28 inference(equality_inference,[],[49])).
% 67.20/67.28 cnf(65,plain,
% 67.20/67.28 (P2(x651,f12(x651))),
% 67.20/67.28 inference(equality_inference,[],[53])).
% 67.20/67.28 cnf(66,plain,
% 67.20/67.28 (~P1(x661)+~P2(x662,x661)),
% 67.20/67.28 inference(equality_inference,[],[56])).
% 67.20/67.28 cnf(67,plain,
% 67.20/67.28 (E(x671,x672)+~P2(x672,x673)+~P2(x671,x673)),
% 67.20/67.28 inference(equality_inference,[],[58])).
% 67.20/67.28 cnf(68,plain,
% 67.20/67.28 (P3(x681,x682,f13(x681,x682))),
% 67.20/67.28 inference(equality_inference,[],[59])).
% 67.20/67.28 cnf(69,plain,
% 67.20/67.28 (P4(x691,x692,f14(x691,x692))),
% 67.20/67.28 inference(equality_inference,[],[60])).
% 67.20/67.28 cnf(70,plain,
% 67.20/67.28 (~P1(x702)+~P1(x703)+~P1(x701)+~P4(x702,x704,x701)+~P2(x703,x704)),
% 67.20/67.28 inference(equality_inference,[],[63])).
% 67.20/67.28 cnf(71,plain,
% 67.20/67.28 (~P2(x711,f1(x712))),
% 67.20/67.28 inference(scs_inference,[],[36,66])).
% 67.20/67.28 cnf(76,plain,
% 67.20/67.28 (P2(x761,f12(x761))),
% 67.20/67.28 inference(rename_variables,[],[65])).
% 67.20/67.28 cnf(78,plain,
% 67.20/67.28 (P2(x781,f12(x781))),
% 67.20/67.28 inference(rename_variables,[],[65])).
% 67.20/67.28 cnf(80,plain,
% 67.20/67.28 (P4(x801,x802,f14(x803,x802))+~E(x803,x801)),
% 67.20/67.28 inference(scs_inference,[],[36,65,76,69,66,56,32,70,28])).
% 67.20/67.28 cnf(81,plain,
% 67.20/67.28 (P4(x811,x812,f14(x811,x813))+~E(x813,x812)),
% 67.20/67.28 inference(scs_inference,[],[36,65,76,69,66,56,32,70,28,29])).
% 67.20/67.28 cnf(82,plain,
% 67.20/67.28 (P4(x821,f5(x821),x822)+~E(f4(x821),x822)),
% 67.20/67.28 inference(scs_inference,[],[36,65,76,69,43,66,56,32,70,28,29,30])).
% 67.20/67.28 cnf(83,plain,
% 67.20/67.28 (P2(x831,f12(x832))+~E(x832,x831)),
% 67.20/67.28 inference(scs_inference,[],[36,65,76,78,69,43,66,56,32,70,28,29,30,31])).
% 67.20/67.28 cnf(84,plain,
% 67.20/67.28 (P3(x841,x842,f13(x843,x842))+~E(x843,x841)),
% 67.20/67.28 inference(scs_inference,[],[36,65,76,78,69,43,68,66,56,32,70,28,29,30,31,33])).
% 67.20/67.28 cnf(85,plain,
% 67.20/67.28 (P3(x851,x852,f13(x851,x853))+~E(x853,x852)),
% 67.20/67.28 inference(scs_inference,[],[36,65,76,78,69,43,68,66,56,32,70,28,29,30,31,33,34])).
% 67.20/67.28 cnf(92,plain,
% 67.20/67.28 (~P2(x921,a8)),
% 67.20/67.28 inference(scs_inference,[],[64,66])).
% 67.20/67.28 cnf(94,plain,
% 67.20/67.28 (~E(a8,f12(x941))),
% 67.20/67.28 inference(scs_inference,[],[64,65,66,56])).
% 67.20/67.28 cnf(100,plain,
% 67.20/67.28 (P2(x1001,f12(x1001))),
% 67.20/67.28 inference(rename_variables,[],[65])).
% 67.20/67.28 cnf(102,plain,
% 67.20/67.28 (~P4(a8,f12(a8),a8)),
% 67.20/67.28 inference(scs_inference,[],[64,65,100,71,42,39,66,56,32,58,70])).
% 67.20/67.28 cnf(105,plain,
% 67.20/67.28 (P3(x1051,f1(x1051),x1052)+~E(x1051,x1052)),
% 67.20/67.28 inference(scs_inference,[],[64,65,100,71,41,42,39,66,56,32,58,70,35])).
% 67.20/67.28 cnf(106,plain,
% 67.20/67.28 (P4(x1061,f2(x1062,x1063),f16(x1062,x1063))+~E(x1062,x1061)),
% 67.20/67.28 inference(scs_inference,[],[47,64,65,100,71,41,42,39,66,56,32,58,70,35,28])).
% 67.20/67.28 cnf(107,plain,
% 67.20/67.28 (P3(x1071,f1(x1072),x1072)+~E(x1072,x1071)),
% 67.20/67.28 inference(scs_inference,[],[47,64,65,100,71,41,42,39,66,56,32,58,70,35,28,33])).
% 67.20/67.28 cnf(108,plain,
% 67.20/67.28 (P3(x1081,x1082,x1081)+~E(f1(x1081),x1082)),
% 67.20/67.28 inference(scs_inference,[],[47,64,65,100,71,41,42,39,66,56,32,58,70,35,28,33,34])).
% 67.20/67.28 cnf(109,plain,
% 67.20/67.28 (P2(x1091,f7(x1092,x1093))+~E(f15(x1092,x1093),x1091)),
% 67.20/67.28 inference(scs_inference,[],[47,64,65,100,71,41,42,39,66,56,32,58,70,35,28,33,34,31])).
% 67.20/67.28 cnf(110,plain,
% 67.20/67.28 (P4(x1101,x1102,f16(x1101,x1103))+~E(f2(x1101,x1103),x1102)),
% 67.20/67.28 inference(scs_inference,[],[47,64,65,100,71,41,42,39,66,56,32,58,70,35,28,33,34,31,29])).
% 67.20/67.28 cnf(121,plain,
% 67.20/67.28 (~E(f12(x1211),a8)),
% 67.20/67.28 inference(scs_inference,[],[37,65,92,66,56,32])).
% 67.20/67.28 cnf(122,plain,
% 67.20/67.28 (P2(x1221,f12(x1221))),
% 67.20/67.28 inference(rename_variables,[],[65])).
% 67.20/67.28 cnf(124,plain,
% 67.20/67.28 (P2(x1241,f12(x1241))),
% 67.20/67.28 inference(rename_variables,[],[65])).
% 67.20/67.28 cnf(132,plain,
% 67.20/67.28 (~P2(f12(x1321),f2(x1322,a8))),
% 67.20/67.28 inference(scs_inference,[],[37,65,122,124,92,40,94,66,56,32,58,70,50,54])).
% 67.20/67.28 cnf(136,plain,
% 67.20/67.28 (P3(x1361,x1362,f7(x1361,x1363))+~E(f6(x1361,x1363),x1362)),
% 67.20/67.28 inference(scs_inference,[],[37,47,65,122,124,46,92,40,94,66,56,32,58,70,50,54,35,30,34])).
% 67.20/67.28 cnf(137,plain,
% 67.20/67.28 (P3(x1371,f6(x1372,x1373),f7(x1372,x1373))+~E(x1372,x1371)),
% 67.20/67.28 inference(scs_inference,[],[37,47,65,122,124,46,92,40,94,66,56,32,58,70,50,54,35,30,34,33])).
% 67.20/67.28 cnf(138,plain,
% 67.20/67.28 (P4(x1381,x1382,f3(x1383,x1382))+~E(x1383,x1381)),
% 67.20/67.28 inference(scs_inference,[],[45,37,47,65,122,124,46,92,40,94,66,56,32,58,70,50,54,35,30,34,33,28])).
% 67.20/67.28 cnf(139,plain,
% 67.20/67.28 (P2(x1391,f6(x1392,x1393))+~E(x1393,x1391)),
% 67.20/67.28 inference(scs_inference,[],[45,37,47,65,122,124,46,92,40,94,39,66,56,32,58,70,50,54,35,30,34,33,28,31])).
% 67.20/67.28 cnf(146,plain,
% 67.20/67.28 (~P2(x1461,f5(x1462))),
% 67.20/67.28 inference(scs_inference,[],[38,66])).
% 67.20/67.28 cnf(148,plain,
% 67.20/67.28 (~E(f5(x1481),f12(x1482))),
% 67.20/67.28 inference(scs_inference,[],[38,65,66,56])).
% 67.20/67.28 cnf(151,plain,
% 67.20/67.28 (P2(x1511,f12(x1511))),
% 67.20/67.28 inference(rename_variables,[],[65])).
% 67.20/67.28 cnf(153,plain,
% 67.20/67.28 (P2(x1531,f12(x1531))),
% 67.20/67.28 inference(rename_variables,[],[65])).
% 67.20/67.28 cnf(159,plain,
% 67.20/67.28 (~P2(a8,f2(x1591,f12(x1592)))),
% 67.20/67.28 inference(scs_inference,[],[132,38,65,151,153,121,40,66,56,32,58,70,54])).
% 67.20/67.28 cnf(161,plain,
% 67.20/67.28 (P3(f3(x1611,x1612),x1613,f16(x1611,x1612))+~E(x1611,x1613)),
% 67.20/67.28 inference(scs_inference,[],[132,38,65,151,153,48,121,40,66,56,32,58,70,54,34])).
% 67.20/67.28 cnf(162,plain,
% 67.20/67.28 (P4(x1621,x1622,f4(x1621))+~E(f5(x1621),x1622)),
% 67.20/67.28 inference(scs_inference,[],[43,132,38,65,151,153,48,121,40,66,56,32,58,70,54,34,29])).
% 67.20/67.28 cnf(165,plain,
% 67.20/67.28 (P4(x1651,f5(x1652),f4(x1652))+~E(x1652,x1651)),
% 67.20/67.28 inference(scs_inference,[],[43,132,38,65,151,153,48,121,40,66,56,32,58,70,54,34,29,35,33,28])).
% 67.20/67.28 cnf(172,plain,
% 67.20/67.28 (P2(x1721,f12(x1721))),
% 67.20/67.28 inference(rename_variables,[],[65])).
% 67.20/67.28 cnf(177,plain,
% 67.20/67.28 (~P2(a8,f6(x1771,f12(x1772)))),
% 67.20/67.28 inference(scs_inference,[],[159,65,172,121,39,32,58,54])).
% 67.20/67.28 cnf(179,plain,
% 67.20/67.28 (P3(x1791,x1792,x1793)+~E(f15(x1791,x1792),x1793)),
% 67.20/67.28 inference(scs_inference,[],[159,65,172,121,39,44,32,58,54,35])).
% 67.20/67.28 cnf(180,plain,
% 67.20/67.28 (P4(x1801,x1802,f3(x1801,x1803))+~E(x1803,x1802)),
% 67.20/67.28 inference(scs_inference,[],[159,45,65,172,121,39,44,32,58,54,35,29])).
% 67.20/67.28 cnf(181,plain,
% 67.20/67.28 (P3(x1811,x1812,f15(x1813,x1812))+~E(x1813,x1811)),
% 67.20/67.28 inference(scs_inference,[],[159,45,65,172,121,39,44,32,58,54,35,29,33])).
% 67.20/67.28 cnf(182,plain,
% 67.20/67.28 (P3(x1821,x1822,f15(x1821,x1823))+~E(x1823,x1822)),
% 67.20/67.28 inference(scs_inference,[],[159,45,65,172,121,39,44,32,58,54,35,29,33,34])).
% 67.20/67.28 cnf(183,plain,
% 67.20/67.28 (P4(x1831,x1832,f3(x1833,x1834))+~E(x1834,x1832)+~E(x1833,x1831)),
% 67.20/67.28 inference(scs_inference,[],[159,45,65,172,121,39,44,32,58,54,29,28])).
% 67.20/67.28 cnf(190,plain,
% 67.20/67.28 (P3(x1901,x1902,x1903)+~E(f13(x1901,x1902),x1903)),
% 67.20/67.28 inference(scs_inference,[],[177,65,68,32,35])).
% 67.20/67.28 cnf(200,plain,
% 67.20/67.28 (P2(x2001,f6(x2002,x2001))),
% 67.20/67.28 inference(rename_variables,[],[39])).
% 67.20/67.28 cnf(205,plain,
% 67.20/67.28 (~P2(f12(x2051),f6(x2052,a8))),
% 67.20/67.28 inference(scs_inference,[],[65,159,94,39,200,32,58,54])).
% 67.20/67.28 cnf(219,plain,
% 67.20/67.28 (E(f13(x2191,f1(x2191)),x2191)),
% 67.20/67.28 inference(scs_inference,[],[41,2,61])).
% 67.20/67.28 cnf(220,plain,
% 67.20/67.28 (P1(f13(a8,f1(a8)))),
% 67.20/67.28 inference(scs_inference,[],[219,49])).
% 67.20/67.28 cnf(221,plain,
% 67.20/67.28 (E(f13(x2211,f1(x2211)),x2211)),
% 67.20/67.28 inference(rename_variables,[],[219])).
% 67.20/67.28 cnf(223,plain,
% 67.20/67.28 (E(x2231,f13(x2231,f1(x2231)))),
% 67.20/67.28 inference(scs_inference,[],[219,221,49,2])).
% 67.20/67.28 cnf(224,plain,
% 67.20/67.28 (~P2(x2241,f13(a8,f1(a8)))),
% 67.20/67.28 inference(scs_inference,[],[219,221,49,2,66])).
% 67.20/67.28 cnf(233,plain,
% 67.20/67.28 (~P3(a8,f1(a8),f12(x2331))),
% 67.20/67.28 inference(scs_inference,[],[36,65,219,221,177,121,40,49,2,66,3,32,63,61])).
% 67.20/67.28 cnf(240,plain,
% 67.20/67.28 (P2(f13(a8,f1(a8)),f6(x2401,a8))),
% 67.20/67.28 inference(scs_inference,[],[36,65,219,221,177,121,40,49,2,66,3,32,63,61,80,81,83,106,138,139])).
% 67.20/67.28 cnf(252,plain,
% 67.20/67.28 (~E(f15(a8,f1(a8)),f12(x2521))),
% 67.20/67.28 inference(scs_inference,[],[36,65,219,221,177,205,44,121,40,49,2,66,3,32,63,61,80,81,83,106,138,139,165,180,84,85,107,137,161,181,182,30,31,35])).
% 67.20/67.28 cnf(264,plain,
% 67.20/67.28 (P2(f13(x2641,f1(x2641)),f6(x2642,x2641))),
% 67.20/67.28 inference(scs_inference,[],[223,85,165,81,139])).
% 67.20/67.28 cnf(266,plain,
% 67.20/67.28 (P2(f13(x2661,f1(x2661)),f12(x2661))),
% 67.20/67.28 inference(scs_inference,[],[223,85,165,81,139,182,83])).
% 67.20/67.28 cnf(276,plain,
% 67.20/67.28 (~P2(x2761,f15(a8,f1(a8)))),
% 67.20/67.28 inference(scs_inference,[],[223,252,85,165,81,139,182,83,107,161,106,137,180,181,84,80,138,54])).
% 67.20/67.28 cnf(278,plain,
% 67.20/67.28 (~E(f6(x2781,a8),f13(a8,f1(a8)))),
% 67.20/67.28 inference(scs_inference,[],[223,240,224,252,85,165,81,139,182,83,107,161,106,137,180,181,84,80,138,54,32])).
% 67.20/67.28 cnf(284,plain,
% 67.20/67.28 (P3(f13(x2841,f1(x2841)),x2842,x2841)+~E(f1(x2841),x2842)),
% 67.20/67.28 inference(scs_inference,[],[223,240,224,252,85,165,81,139,182,83,107,161,106,137,180,181,84,80,138,54,32,30,29,33,35,34])).
% 67.20/67.28 cnf(294,plain,
% 67.20/67.28 (~P3(a8,f1(a8),f6(x2941,a8))),
% 67.20/67.28 inference(scs_inference,[],[278,61])).
% 67.20/67.28 cnf(302,plain,
% 67.20/67.28 (~E(f2(x3021,x3022),f15(a8,f1(a8)))),
% 67.20/67.28 inference(scs_inference,[],[276,40,32])).
% 67.20/67.28 cnf(325,plain,
% 67.20/67.29 (~P4(a8,f6(x3251,a8),a8)),
% 67.20/67.29 inference(scs_inference,[],[39,64,70])).
% 67.20/67.29 cnf(338,plain,
% 67.20/67.29 (~P4(f1(x3381),f2(x3382,f1(x3381)),f1(x3381))),
% 67.20/67.29 inference(scs_inference,[],[40,36,70])).
% 67.20/67.29 cnf(339,plain,
% 67.20/67.29 (P2(x3391,f2(x3392,x3391))),
% 67.20/67.29 inference(rename_variables,[],[40])).
% 67.20/67.29 cnf(341,plain,
% 67.20/67.29 (~P4(f1(x3411),f2(x3412,f1(x3411)),a8)),
% 67.20/67.29 inference(scs_inference,[],[40,339,36,223,220,70,63])).
% 67.20/67.29 cnf(345,plain,
% 67.20/67.29 (~E(f16(f1(x3451),f1(x3451)),f1(x3451))),
% 67.20/67.29 inference(scs_inference,[],[40,339,36,47,223,220,70,63,30])).
% 67.20/67.29 cnf(348,plain,
% 67.20/67.29 (~P4(a8,f2(x3481,a8),a8)),
% 67.20/67.29 inference(scs_inference,[],[40,64,70])).
% 67.20/67.29 cnf(352,plain,
% 67.20/67.29 (~P4(f5(x3521),f2(x3522,f5(x3521)),f5(x3521))),
% 67.20/67.29 inference(scs_inference,[],[40,38,70])).
% 67.20/67.29 cnf(356,plain,
% 67.20/67.29 (~P4(f4(x3561),f2(x3562,f4(x3561)),f4(x3561))),
% 67.20/67.29 inference(scs_inference,[],[40,37,70])).
% 67.20/67.29 cnf(389,plain,
% 67.20/67.29 (~P2(f2(x3891,x3892),f7(a8,f1(a8)))),
% 67.20/67.29 inference(scs_inference,[],[42,302,67])).
% 67.20/67.29 cnf(476,plain,
% 67.20/67.29 (~E(f14(a8,f12(a8)),a8)),
% 67.20/67.29 inference(scs_inference,[],[102,69,30])).
% 67.20/67.29 cnf(480,plain,
% 67.20/67.29 (~E(f3(a8,f12(a8)),a8)),
% 67.20/67.29 inference(scs_inference,[],[102,45,30])).
% 67.20/67.29 cnf(511,plain,
% 67.20/67.29 (E(a8,f1(x5111))),
% 67.20/67.29 inference(scs_inference,[],[36,50,2])).
% 67.20/67.29 cnf(512,plain,
% 67.20/67.29 (P3(a8,f1(a8),f1(x5121))),
% 67.20/67.29 inference(scs_inference,[],[511,105])).
% 67.20/67.29 cnf(513,plain,
% 67.20/67.29 (P3(x5131,f1(x5132),f13(x5131,a8))),
% 67.20/67.29 inference(scs_inference,[],[511,105,85])).
% 67.20/67.29 cnf(514,plain,
% 67.20/67.29 (E(f1(x5141),a8)),
% 67.20/67.29 inference(scs_inference,[],[511,105,85,2])).
% 67.20/67.29 cnf(515,plain,
% 67.20/67.29 (P3(x5151,f1(x5152),f15(x5151,a8))),
% 67.20/67.29 inference(scs_inference,[],[511,105,85,2,182])).
% 67.20/67.29 cnf(516,plain,
% 67.20/67.29 (P4(x5161,f1(x5162),f14(x5161,a8))),
% 67.20/67.29 inference(scs_inference,[],[511,105,85,2,182,81])).
% 67.20/67.29 cnf(517,plain,
% 67.20/67.29 (P4(f1(x5171),f2(a8,x5172),f16(a8,x5172))),
% 67.20/67.29 inference(scs_inference,[],[511,105,85,2,182,81,106])).
% 67.20/67.29 cnf(518,plain,
% 67.20/67.29 (P4(f1(x5181),x5182,f14(a8,x5182))),
% 67.20/67.29 inference(scs_inference,[],[511,105,85,2,182,81,106,80])).
% 67.20/67.29 cnf(520,plain,
% 67.20/67.29 (P4(f1(x5201),f5(a8),f4(a8))),
% 67.20/67.29 inference(scs_inference,[],[511,105,85,2,182,81,106,80,84,165])).
% 67.20/67.29 cnf(521,plain,
% 67.20/67.29 (P3(f1(x5211),f6(a8,x5212),f7(a8,x5212))),
% 67.20/67.29 inference(scs_inference,[],[511,105,85,2,182,81,106,80,84,165,137])).
% 67.20/67.29 cnf(522,plain,
% 67.20/67.29 (P2(f1(x5221),f6(x5222,a8))),
% 67.20/67.29 inference(scs_inference,[],[511,105,85,2,182,81,106,80,84,165,137,139])).
% 67.20/67.29 cnf(523,plain,
% 67.20/67.29 (P3(f3(a8,x5231),f1(x5232),f16(a8,x5231))),
% 67.20/67.29 inference(scs_inference,[],[511,105,85,2,182,81,106,80,84,165,137,139,161])).
% 67.20/67.29 cnf(524,plain,
% 67.20/67.29 (P4(x5241,f1(x5242),f3(x5241,a8))),
% 67.20/67.29 inference(scs_inference,[],[511,105,85,2,182,81,106,80,84,165,137,139,161,180])).
% 67.20/67.29 cnf(525,plain,
% 67.20/67.29 (P2(f1(x5251),f12(a8))),
% 67.20/67.29 inference(scs_inference,[],[511,105,85,2,182,81,106,80,84,165,137,139,161,180,83])).
% 67.20/67.29 cnf(527,plain,
% 67.20/67.29 (P3(f1(x5271),x5272,f15(a8,x5272))),
% 67.20/67.29 inference(scs_inference,[],[511,105,85,2,182,81,106,80,84,165,137,139,161,180,83,107,181])).
% 67.20/67.29 cnf(528,plain,
% 67.20/67.29 (P4(f1(x5281),x5282,f3(a8,x5282))),
% 67.20/67.29 inference(scs_inference,[],[511,105,85,2,182,81,106,80,84,165,137,139,161,180,83,107,181,138])).
% 67.20/67.29 cnf(530,plain,
% 67.20/67.29 (~E(f16(f1(x5301),f1(x5301)),a8)),
% 67.20/67.29 inference(scs_inference,[],[345,511,105,85,2,182,81,106,80,84,165,137,139,161,180,83,107,181,138,183,3])).
% 67.20/67.29 cnf(533,plain,
% 67.20/67.29 (~E(f16(a8,f1(x5331)),f1(x5331))),
% 67.20/67.29 inference(scs_inference,[],[338,223,345,511,105,85,2,182,81,106,80,84,165,137,139,161,180,83,107,181,138,183,3,29,30])).
% 67.20/67.29 cnf(537,plain,
% 67.20/67.29 (E(x5371,f13(x5371,f1(x5371)))),
% 67.20/67.29 inference(rename_variables,[],[223])).
% 67.20/67.29 cnf(548,plain,
% 67.20/67.29 (~P2(x5481,f13(a8,a8))),
% 67.20/67.29 inference(scs_inference,[],[36,338,223,537,65,64,345,233,511,105,85,2,182,81,106,80,84,165,137,139,161,180,83,107,181,138,183,3,29,30,28,33,34,35,67,63,108,284,54])).
% 67.20/67.29 cnf(553,plain,
% 67.20/67.29 (P3(x5531,a8,x5531)),
% 67.20/67.29 inference(scs_inference,[],[514,108])).
% 67.20/67.29 cnf(556,plain,
% 67.20/67.29 (P3(x5561,a8,f13(x5561,f1(x5562)))),
% 67.20/67.29 inference(scs_inference,[],[514,108,284,105,85])).
% 67.20/67.29 cnf(557,plain,
% 67.20/67.29 (P3(x5571,a8,f15(x5571,f1(x5572)))),
% 67.20/67.29 inference(scs_inference,[],[514,108,284,105,85,182])).
% 67.20/67.29 cnf(558,plain,
% 67.20/67.29 (P2(a8,f6(x5581,f1(x5582)))),
% 67.20/67.29 inference(scs_inference,[],[514,108,284,105,85,182,139])).
% 67.20/67.29 cnf(559,plain,
% 67.20/67.29 (P4(x5591,a8,f14(x5591,f1(x5592)))),
% 67.20/67.29 inference(scs_inference,[],[514,108,284,105,85,182,139,81])).
% 67.20/67.29 cnf(561,plain,
% 67.20/67.29 (P3(a8,x5611,f13(f1(x5612),x5611))),
% 67.20/67.29 inference(scs_inference,[],[514,108,284,105,85,182,139,81,180,84])).
% 67.20/67.29 cnf(563,plain,
% 67.20/67.29 (P4(a8,x5631,f3(f1(x5632),x5631))),
% 67.20/67.29 inference(scs_inference,[],[514,108,284,105,85,182,139,81,180,84,80,138])).
% 67.20/67.29 cnf(568,plain,
% 67.20/67.29 (P3(a8,x5681,f15(f1(x5682),x5681))),
% 67.20/67.29 inference(scs_inference,[],[514,530,108,284,105,85,182,139,81,180,84,80,138,83,107,50,181])).
% 67.20/67.29 cnf(592,plain,
% 67.20/67.29 (~P3(a8,a8,f12(x5921))),
% 67.20/67.29 inference(scs_inference,[],[36,352,223,47,65,64,266,548,524,528,533,522,514,294,476,68,513,527,530,108,284,105,85,182,139,81,180,84,80,138,83,107,50,181,183,3,29,30,28,33,35,34,67,32,63,61])).
% 67.20/67.29 cnf(594,plain,
% 67.20/67.29 (E(f1(f1(x5941)),f1(a8))),
% 67.20/67.29 inference(scs_inference,[],[36,50,4])).
% 67.20/67.29 cnf(596,plain,
% 67.20/67.29 (E(f1(a8),f1(f1(x5961)))),
% 67.20/67.29 inference(scs_inference,[],[594,108,2])).
% 67.20/67.29 cnf(612,plain,
% 67.20/67.29 (~P2(x6121,f15(a8,a8))),
% 67.20/67.29 inference(scs_inference,[],[146,356,223,47,65,525,594,592,480,533,514,44,515,553,108,2,3,30,33,35,34,67,32,54])).
% 67.20/67.29 cnf(614,plain,
% 67.20/67.29 (E(f4(f1(x6141)),f4(a8))),
% 67.20/67.29 inference(scs_inference,[],[36,50,5])).
% 67.20/67.29 cnf(617,plain,
% 67.20/67.29 (E(f4(a8),f4(f1(x6171)))),
% 67.20/67.29 inference(scs_inference,[],[614,596,82,108,2])).
% 67.20/67.29 cnf(618,plain,
% 67.20/67.29 (~E(f16(a8,f1(x6181)),a8)),
% 67.20/67.29 inference(scs_inference,[],[341,517,614,596,82,108,2,30])).
% 67.20/67.29 cnf(630,plain,
% 67.20/67.29 (~P2(x6301,f13(a8,f1(x6302)))),
% 67.20/67.29 inference(scs_inference,[],[146,341,264,517,614,596,522,592,345,556,82,108,2,30,35,67,32,50,54])).
% 67.20/67.29 cnf(635,plain,
% 67.20/67.29 (~E(f16(a8,a8),a8)),
% 67.20/67.29 inference(scs_inference,[],[348,47,617,618,514,82,3,30])).
% 67.20/67.29 cnf(642,plain,
% 67.20/67.29 (~P1(f16(a8,a8))),
% 67.20/67.29 inference(scs_inference,[],[146,348,47,617,618,592,514,40,557,82,3,30,35,32,50])).
% 67.20/67.29 cnf(644,plain,
% 67.20/67.29 (~P2(x6441,f15(a8,f1(x6442)))),
% 67.20/67.29 inference(scs_inference,[],[146,348,47,617,618,592,514,40,557,82,3,30,35,32,50,54])).
% 67.20/67.29 cnf(652,plain,
% 67.20/67.29 (~P2(x6521,f13(f1(x6522),f1(a8)))),
% 67.20/67.29 inference(scs_inference,[],[558,635,233,514,561,3,67,35,54])).
% 67.20/67.29 cnf(654,plain,
% 67.20/67.29 (E(f5(f1(x6541)),f5(a8))),
% 67.20/67.29 inference(scs_inference,[],[36,50,6])).
% 67.20/67.29 cnf(656,plain,
% 67.20/67.29 (E(f5(a8),f5(f1(x6561)))),
% 67.20/67.29 inference(scs_inference,[],[654,162,2])).
% 67.20/67.29 cnf(657,plain,
% 67.20/67.29 (~P2(f16(f1(x6571),f1(x6571)),f12(a8))),
% 67.20/67.29 inference(scs_inference,[],[654,525,345,162,2,67])).
% 67.20/67.29 cnf(666,plain,
% 67.20/67.29 (E(f6(f1(x6661),x6662),f6(a8,x6662))),
% 67.20/67.29 inference(scs_inference,[],[36,50,7])).
% 67.20/67.29 cnf(673,plain,
% 67.20/67.29 (~P2(x6731,f15(f1(x6732),f1(a8)))),
% 67.20/67.29 inference(scs_inference,[],[666,656,525,233,657,568,136,162,2,31,35,54])).
% 67.20/67.29 cnf(675,plain,
% 67.20/67.29 (E(f6(x6751,f1(x6752)),f6(x6751,a8))),
% 67.20/67.29 inference(scs_inference,[],[36,50,8])).
% 67.20/67.29 cnf(677,plain,
% 67.20/67.29 (E(f6(x6771,a8),f6(x6771,f1(x6772)))),
% 67.20/67.29 inference(scs_inference,[],[675,136,2])).
% 67.20/67.29 cnf(679,plain,
% 67.20/67.29 (E(f2(f1(x6791),x6792),f2(a8,x6792))),
% 67.20/67.29 inference(scs_inference,[],[36,50,9])).
% 67.20/67.29 cnf(680,plain,
% 67.20/67.29 (P4(f1(x6801),f2(a8,x6802),f16(f1(x6801),x6802))),
% 67.20/67.29 inference(scs_inference,[],[679,110])).
% 67.20/67.29 cnf(683,plain,
% 67.20/67.29 (E(f2(x6831,f1(x6832)),f2(x6831,a8))),
% 67.20/67.29 inference(scs_inference,[],[36,50,10])).
% 67.20/67.29 cnf(685,plain,
% 67.20/67.29 (P3(x6851,f6(x6851,f1(x6852)),f7(x6851,a8))),
% 67.20/67.29 inference(scs_inference,[],[677,683,110,136])).
% 67.20/67.29 cnf(686,plain,
% 67.20/67.29 (E(f2(x6861,a8),f2(x6861,f1(x6862)))),
% 67.20/67.29 inference(scs_inference,[],[677,683,110,136,2])).
% 67.20/67.29 cnf(696,plain,
% 67.20/67.29 (E(f14(x6961,f1(x6962)),f14(x6961,a8))),
% 67.20/67.29 inference(scs_inference,[],[36,50,12])).
% 67.20/67.29 cnf(697,plain,
% 67.20/67.29 (P4(x6971,f2(x6971,f1(x6972)),f16(x6971,a8))),
% 67.20/67.29 inference(scs_inference,[],[686,110])).
% 67.20/67.29 cnf(699,plain,
% 67.20/67.29 (~E(f16(f1(x6991),a8),f1(x6991))),
% 67.20/67.29 inference(scs_inference,[],[338,686,696,110,2,30])).
% 67.20/67.29 cnf(712,plain,
% 67.20/67.29 (~P2(f14(a8,f12(a8)),f12(a8))),
% 67.20/67.29 inference(scs_inference,[],[65,511,476,699,3,67])).
% 67.20/67.29 cnf(740,plain,
% 67.20/67.29 (~P3(a8,f1(a8),f16(a8,a8))),
% 67.20/67.29 inference(scs_inference,[],[65,219,635,3,67,61])).
% 67.20/67.29 cnf(742,plain,
% 67.20/67.29 (~E(f3(a8,a8),a8)),
% 67.20/67.29 inference(scs_inference,[],[65,219,635,523,3,67,61,33])).
% 67.20/67.29 cnf(744,plain,
% 67.20/67.29 (~P1(f3(a8,a8))),
% 67.20/67.29 inference(scs_inference,[],[65,219,635,523,3,67,61,33,50])).
% 67.20/67.29 cnf(757,plain,
% 67.20/67.29 (~P4(a8,f12(a8),f1(x7571))),
% 67.20/67.29 inference(scs_inference,[],[525,480,740,44,39,712,31,67,35,62])).
% 67.20/67.29 cnf(761,plain,
% 67.20/67.29 (~E(f13(a8,a8),f16(a8,a8))),
% 67.20/67.29 inference(scs_inference,[],[740,513,35])).
% 67.20/67.29 cnf(765,plain,
% 67.20/67.29 (P2(x7651,f12(x7651))),
% 67.20/67.29 inference(rename_variables,[],[65])).
% 67.20/67.29 cnf(767,plain,
% 67.20/67.29 (~E(f12(x7671),f15(a8,a8))),
% 67.20/67.29 inference(scs_inference,[],[148,65,765,612,67,32])).
% 67.20/67.29 cnf(775,plain,
% 67.20/67.29 (~P3(f1(x7751),f1(a8),f12(x7752))),
% 67.20/67.29 inference(scs_inference,[],[65,652,42,767,67,32,61])).
% 67.20/67.29 cnf(783,plain,
% 67.20/67.29 (~E(f12(x7831),f15(f1(x7832),f1(a8)))),
% 67.20/67.29 inference(scs_inference,[],[148,65,673,775,39,515,67,35,32])).
% 67.20/67.29 cnf(785,plain,
% 67.20/67.29 (~P2(x7851,f15(f1(x7852),a8))),
% 67.20/67.29 inference(scs_inference,[],[148,65,673,775,39,515,67,35,32,54])).
% 67.29/67.29 cnf(795,plain,
% 67.29/67.29 (~P3(a8,f1(x7951),f12(x7952))),
% 67.29/67.29 inference(scs_inference,[],[65,630,775,42,513,783,67,35,32,61])).
% 67.29/67.29 cnf(797,plain,
% 67.29/67.29 (~P2(x7971,f13(f1(x7972),a8))),
% 67.29/67.29 inference(scs_inference,[],[65,630,775,42,513,783,67,35,32,61,54])).
% 67.29/67.29 cnf(805,plain,
% 67.29/67.29 (~E(f12(x8051),f15(a8,f1(x8052)))),
% 67.29/67.29 inference(scs_inference,[],[65,266,644,795,278,561,67,35,32])).
% 67.29/67.29 cnf(807,plain,
% 67.29/67.29 (~P2(x8071,f13(f1(x8072),f1(x8073)))),
% 67.29/67.29 inference(scs_inference,[],[65,266,644,795,278,561,67,35,32,54])).
% 67.29/67.29 cnf(819,plain,
% 67.29/67.29 (~P2(x8191,f15(f1(x8192),f1(x8193)))),
% 67.29/67.29 inference(scs_inference,[],[65,264,807,795,278,568,67,35,32,61,54])).
% 67.29/67.29 cnf(825,plain,
% 67.29/67.29 (~E(f12(x8251),f15(f1(x8252),f1(x8253)))),
% 67.29/67.29 inference(scs_inference,[],[65,819,42,805,67,32])).
% 67.29/67.29 cnf(831,plain,
% 67.29/67.29 (~E(f12(x8311),f15(f1(x8312),a8))),
% 67.29/67.29 inference(scs_inference,[],[65,785,42,825,67,32])).
% 67.29/67.29 cnf(839,plain,
% 67.29/67.29 (~P3(f1(x8391),a8,f12(x8392))),
% 67.29/67.29 inference(scs_inference,[],[65,797,42,831,67,32,61])).
% 67.29/67.29 cnf(850,plain,
% 67.29/67.29 (~E(f6(x8501,a8),f15(f1(x8502),f1(x8503)))),
% 67.29/67.29 inference(scs_inference,[],[522,819,32])).
% 67.29/67.29 cnf(857,plain,
% 67.29/67.29 (~P3(a8,a8,f6(x8571,a8))),
% 67.29/67.29 inference(scs_inference,[],[522,548,42,850,67,32,61])).
% 67.29/67.29 cnf(862,plain,
% 67.29/67.29 (~E(f6(x8621,x8622),f15(a8,a8))),
% 67.29/67.29 inference(scs_inference,[],[264,857,612,561,35,32])).
% 67.29/67.29 cnf(864,plain,
% 67.29/67.29 (~P2(f6(x8641,x8642),f7(a8,a8))),
% 67.29/67.29 inference(scs_inference,[],[42,862,67])).
% 67.29/67.29 cnf(871,plain,
% 67.29/67.29 (~P3(a8,f1(x8711),f6(x8712,a8))),
% 67.29/67.29 inference(scs_inference,[],[522,630,857,42,568,862,67,35,32,61])).
% 67.29/67.29 cnf(876,plain,
% 67.29/67.29 (~E(f6(x8761,x8762),f15(a8,f1(x8763)))),
% 67.29/67.29 inference(scs_inference,[],[264,871,644,561,35,32])).
% 67.29/67.29 cnf(883,plain,
% 67.29/67.29 (~E(f6(x8831,a8),f15(f1(x8832),a8))),
% 67.29/67.29 inference(scs_inference,[],[522,785,871,42,568,876,67,35,32])).
% 67.29/67.29 cnf(885,plain,
% 67.29/67.29 (E(f15(f1(x8851),x8852),f15(a8,x8852))),
% 67.29/67.29 inference(scs_inference,[],[36,50,13])).
% 67.29/67.29 cnf(886,plain,
% 67.29/67.29 (P2(f15(a8,x8861),f7(f1(x8862),x8861))),
% 67.29/67.29 inference(scs_inference,[],[885,109])).
% 67.29/67.29 cnf(887,plain,
% 67.29/67.29 (E(f15(a8,x8871),f15(f1(x8872),x8871))),
% 67.29/67.29 inference(scs_inference,[],[885,109,2])).
% 67.29/67.29 cnf(888,plain,
% 67.29/67.29 (~E(f6(x8881,x8882),f15(f1(x8883),a8))),
% 67.29/67.29 inference(scs_inference,[],[885,862,109,2,3])).
% 67.29/67.29 cnf(893,plain,
% 67.29/67.29 (~E(f6(x8931,x8932),f13(f1(x8933),a8))),
% 67.29/67.29 inference(scs_inference,[],[264,885,797,42,883,862,109,2,3,67,32])).
% 67.29/67.29 cnf(911,plain,
% 67.29/67.29 (P2(f15(f1(x9111),x9112),f7(a8,x9112))),
% 67.29/67.29 inference(scs_inference,[],[887,109])).
% 67.29/67.29 cnf(918,plain,
% 67.29/67.29 (~E(f6(x9181,x9182),f13(f1(x9183),f1(x9184)))),
% 67.29/67.29 inference(scs_inference,[],[264,887,807,42,389,888,893,109,61,31,67,32])).
% 67.29/67.29 cnf(935,plain,
% 67.29/67.29 (~E(f6(x9351,x9352),f15(f1(x9353),f1(x9354)))),
% 67.29/67.29 inference(scs_inference,[],[264,911,819,918,864,61,31,32])).
% 67.29/67.29 cnf(955,plain,
% 67.29/67.29 (~P3(a8,a8,f6(x9551,x9552))),
% 67.29/67.29 inference(scs_inference,[],[264,548,42,935,67,32,61])).
% 67.29/67.29 cnf(962,plain,
% 67.29/67.29 (~E(f7(f1(x9621),x9622),f15(a8,a8))),
% 67.29/67.29 inference(scs_inference,[],[886,955,612,561,35,32])).
% 67.29/67.29 cnf(967,plain,
% 67.29/67.29 (~E(f6(x9671,x9672),f13(a8,f1(x9673)))),
% 67.29/67.29 inference(scs_inference,[],[264,630,42,962,67,32])).
% 67.29/67.29 cnf(969,plain,
% 67.29/67.29 (~P3(a8,f1(x9691),f6(x9692,x9693))),
% 67.29/67.29 inference(scs_inference,[],[967,61])).
% 67.29/67.29 cnf(971,plain,
% 67.29/67.29 (~E(f7(a8,x9711),f15(a8,f1(x9712)))),
% 67.29/67.29 inference(scs_inference,[],[911,644,967,61,32])).
% 67.29/67.29 cnf(973,plain,
% 67.29/67.29 (~E(f7(a8,x9731),f15(f1(x9732),f1(x9733)))),
% 67.29/67.29 inference(scs_inference,[],[885,971,3])).
% 67.29/67.29 cnf(980,plain,
% 67.29/67.29 (~E(f7(a8,x9801),f15(f1(x9802),a8))),
% 67.29/67.29 inference(scs_inference,[],[885,886,911,969,785,512,971,3,67,35,32])).
% 67.29/67.29 cnf(983,plain,
% 67.29/67.29 (P2(f15(f1(x9831),x9832),f7(a8,x9832))),
% 67.29/67.29 inference(rename_variables,[],[911])).
% 67.29/67.29 cnf(987,plain,
% 67.29/67.29 (~E(f7(a8,x9871),f13(f1(x9872),a8))),
% 67.29/67.29 inference(scs_inference,[],[911,983,969,797,561,973,67,35,32])).
% 67.29/67.29 cnf(991,plain,
% 67.29/67.29 (~E(f7(a8,x9911),f15(a8,a8))),
% 67.29/67.29 inference(scs_inference,[],[887,980,987,61,3])).
% 67.29/67.29 cnf(994,plain,
% 67.29/67.29 (P2(f15(f1(x9941),x9942),f7(a8,x9942))),
% 67.29/67.29 inference(rename_variables,[],[911])).
% 67.29/67.29 cnf(996,plain,
% 67.29/67.29 (~E(f7(a8,x9961),f13(f1(x9962),f1(x9963)))),
% 67.29/67.29 inference(scs_inference,[],[887,911,994,807,980,987,61,3,67,32])).
% 67.29/67.29 cnf(1003,plain,
% 67.29/67.29 (~E(f7(x10031,x10032),f15(f1(x10033),f1(x10034)))),
% 67.29/67.29 inference(scs_inference,[],[886,819,42,991,996,61,67,32])).
% 67.29/67.29 cnf(1005,plain,
% 67.29/67.29 (~E(f7(x10051,x10052),f15(a8,f1(x10053)))),
% 67.29/67.29 inference(scs_inference,[],[887,1003,3])).
% 67.29/67.29 cnf(1017,plain,
% 67.29/67.29 (~E(f7(x10171,x10172),f15(a8,a8))),
% 67.29/67.29 inference(scs_inference,[],[886,612,42,1005,67,32])).
% 67.29/67.29 cnf(1019,plain,
% 67.29/67.29 (~E(f7(x10191,x10192),f15(f1(x10193),a8))),
% 67.29/67.29 inference(scs_inference,[],[885,1017,3])).
% 67.29/67.29 cnf(1024,plain,
% 67.29/67.29 (~E(f7(a8,x10241),f13(a8,f1(x10242)))),
% 67.29/67.29 inference(scs_inference,[],[885,886,911,630,1017,3,67,32])).
% 67.29/67.29 cnf(1029,plain,
% 67.29/67.29 (~P2(f7(x10291,x10292),f7(a8,a8))),
% 67.29/67.29 inference(scs_inference,[],[911,1019,1024,61,67])).
% 67.29/67.29 cnf(1135,plain,
% 67.29/67.29 (~P4(f5(x11351),f6(x11352,a8),f5(x11351))),
% 67.29/67.29 inference(scs_inference,[],[264,38,220,70])).
% 67.29/67.29 cnf(1163,plain,
% 67.29/67.29 (~E(f2(x11631,x11632),f15(f1(x11633),f1(a8)))),
% 67.29/67.29 inference(scs_inference,[],[302,885,3])).
% 67.29/67.29 cnf(1263,plain,
% 67.29/67.29 (E(f15(x12631,f1(x12632)),f15(x12631,a8))),
% 67.29/67.29 inference(scs_inference,[],[36,50,14])).
% 67.29/67.30 cnf(1266,plain,
% 67.29/67.30 (~E(f2(x12661,x12662),f15(f1(x12663),a8))),
% 67.29/67.30 inference(scs_inference,[],[1263,1163,109,2,3])).
% 67.29/67.30 cnf(1505,plain,
% 67.29/67.30 (P3(x15051,f1(x15052),x15051)),
% 67.29/67.30 inference(scs_inference,[],[511,697,559,553,29,28,34])).
% 67.29/67.30 cnf(1515,plain,
% 67.29/67.30 (P3(a8,a8,f1(x15151))),
% 67.29/67.30 inference(scs_inference,[],[514,680,518,512,29,28,34])).
% 67.29/67.30 cnf(1523,plain,
% 67.29/67.30 (P4(a8,a8,f14(f1(x15231),f1(x15232)))),
% 67.29/67.30 inference(scs_inference,[],[514,559,528,29,28])).
% 67.29/67.30 cnf(1536,plain,
% 67.29/67.30 (P3(a8,a8,f13(f1(x15361),f1(x15362)))),
% 67.29/67.30 inference(scs_inference,[],[514,516,563,527,556,28,29,34,33])).
% 67.29/67.30 cnf(1578,plain,
% 67.29/67.30 (~P4(f1(x15781),f6(x15782,a8),a8)),
% 67.29/67.30 inference(scs_inference,[],[522,36,223,220,63])).
% 67.29/67.30 cnf(1741,plain,
% 67.29/67.30 (~P3(a8,a8,f7(x17411,x17412))),
% 67.29/67.30 inference(scs_inference,[],[548,42,32,61])).
% 67.29/67.30 cnf(1746,plain,
% 67.29/67.30 (~P3(a8,a8,f2(x17461,x17462))),
% 67.29/67.30 inference(scs_inference,[],[548,1741,40,1536,35,32,61])).
% 67.29/67.30 cnf(2138,plain,
% 67.29/67.30 (~P2(f3(a8,a8),f6(x21381,a8))),
% 67.29/67.30 inference(scs_inference,[],[677,558,742,58])).
% 67.29/67.30 cnf(2400,plain,
% 67.29/67.30 (~P2(f2(x24001,x24002),f7(a8,a8))),
% 67.29/67.30 inference(scs_inference,[],[911,1266,67])).
% 67.29/67.30 cnf(2460,plain,
% 67.29/67.30 (P4(f1(x24601),f1(x24602),f3(a8,a8))),
% 67.29/67.30 inference(scs_inference,[],[511,1523,528,685,28,33,29])).
% 67.29/67.30 cnf(2541,plain,
% 67.29/67.30 (P4(f1(x25411),f5(a8),x25412)+~E(f4(a8),x25412)),
% 67.29/67.30 inference(scs_inference,[],[38,522,520,56,30])).
% 67.29/67.30 cnf(2542,plain,
% 67.29/67.30 (P4(f1(x25421),x25422,f16(a8,x25423))+~E(f2(a8,x25423),x25422)),
% 67.29/67.30 inference(scs_inference,[],[38,522,517,520,56,30,29])).
% 67.29/67.30 cnf(2547,plain,
% 67.29/67.30 (P4(f1(x25471),x25472,f4(a8))+~E(f5(a8),x25472)),
% 67.29/67.30 inference(scs_inference,[],[520,29])).
% 67.29/67.30 cnf(2555,plain,
% 67.29/67.30 (E(f3(x25551,x25552),f14(x25551,x25552))),
% 67.29/67.30 inference(scs_inference,[],[955,45,190,179,62])).
% 67.29/67.30 cnf(2559,plain,
% 67.29/67.30 (E(f6(x25591,x25592),f12(x25592))),
% 67.29/67.30 inference(scs_inference,[],[2138,2400,955,45,39,190,179,62,109,139,54])).
% 67.29/67.30 cnf(2561,plain,
% 67.29/67.30 (E(f4(x25611),a8)),
% 67.29/67.30 inference(scs_inference,[],[37,2138,2400,955,45,39,190,179,62,109,139,54,50])).
% 67.29/67.30 cnf(2563,plain,
% 67.29/67.30 (E(f1(x25631),f13(a8,a8))),
% 67.29/67.30 inference(scs_inference,[],[37,2138,2400,1515,955,45,39,190,179,62,109,139,54,50,61])).
% 67.29/67.30 cnf(2566,plain,
% 67.29/67.30 (~E(f1(x25661),f3(a8,a8))),
% 67.29/67.30 inference(scs_inference,[],[37,2138,2400,1515,955,761,45,522,39,190,179,62,109,139,54,50,61,2,31])).
% 67.29/67.30 cnf(2568,plain,
% 67.29/67.30 (~E(f4(x25681),f3(a8,a8))),
% 67.29/67.30 inference(scs_inference,[],[37,744,2138,2400,1515,955,761,45,522,39,190,179,62,109,139,54,50,61,2,31,27])).
% 67.29/67.30 cnf(2571,plain,
% 67.29/67.30 (~P4(a8,f6(x25711,a8),f1(x25712))),
% 67.29/67.30 inference(scs_inference,[],[37,744,2138,757,2400,1515,955,325,761,45,742,522,514,39,190,179,62,109,139,54,50,61,2,31,27,3,28,30])).
% 67.29/67.30 cnf(2572,plain,
% 67.29/67.30 (~P3(a8,a8,f16(a8,a8))),
% 67.29/67.30 inference(scs_inference,[],[37,744,2138,757,2400,1515,955,740,325,761,45,742,522,514,39,511,190,179,62,109,139,54,50,61,2,31,27,3,28,30,34])).
% 67.29/67.30 cnf(2574,plain,
% 67.29/67.30 (P4(f1(x25741),f13(a8,a8),f3(a8,a8))),
% 67.29/67.30 inference(scs_inference,[],[37,744,2138,757,2460,2400,1515,955,740,325,761,45,742,522,514,39,511,190,179,62,109,139,54,50,61,2,31,27,3,28,30,34,29])).
% 67.29/67.30 cnf(2591,plain,
% 67.29/67.30 (~E(f15(a8,a8),f16(a8,a8))),
% 67.29/67.30 inference(scs_inference,[],[2572,1746,190,179])).
% 67.29/67.30 cnf(2593,plain,
% 67.29/67.30 (E(f2(x25931,x25932),f12(x25932))),
% 67.29/67.30 inference(scs_inference,[],[2572,1029,1746,40,190,179,109,54])).
% 67.29/67.30 cnf(2595,plain,
% 67.29/67.30 (E(f5(x25951),a8)),
% 67.29/67.30 inference(scs_inference,[],[2572,1029,1746,38,40,190,179,109,54,50])).
% 67.29/67.30 cnf(2597,plain,
% 67.29/67.30 (E(x25971,f13(x25971,a8))),
% 67.29/67.30 inference(scs_inference,[],[2572,1029,1746,553,38,40,190,179,109,54,50,61])).
% 67.29/67.30 cnf(2599,plain,
% 67.29/67.30 (~E(f3(a8,a8),f1(x25991))),
% 67.29/67.30 inference(scs_inference,[],[2566,2572,1029,1746,553,38,40,190,179,109,54,50,61,2])).
% 67.29/67.30 cnf(2601,plain,
% 67.29/67.30 (~E(f13(a8,a8),f3(a8,a8))),
% 67.29/67.30 inference(scs_inference,[],[37,2563,2566,2572,642,1029,1746,553,38,40,190,179,109,54,50,61,2,27,3])).
% 67.29/67.30 cnf(2605,plain,
% 67.29/67.30 (E(f3(x26051,x26052),f14(x26051,x26052))),
% 67.29/67.30 inference(rename_variables,[],[2555])).
% 67.29/67.30 cnf(2609,plain,
% 67.29/67.30 (P3(x26091,f1(x26092),x26091)),
% 67.29/67.30 inference(rename_variables,[],[1505])).
% 67.29/67.30 cnf(2610,plain,
% 67.29/67.30 (P3(f3(x26101,x26102),f1(x26103),f14(x26101,x26102))),
% 67.29/67.30 inference(scs_inference,[],[37,2555,2605,2559,2563,2566,2574,2571,2561,2572,642,1505,2609,1029,521,1746,553,38,40,190,179,109,54,50,61,2,27,3,28,30,34,33,35])).
% 67.29/67.30 cnf(2624,plain,
% 67.29/67.30 (~E(f3(a8,a8),f4(x26241))),
% 67.29/67.30 inference(scs_inference,[],[2568,1741,44,190,61,2])).
% 67.29/67.30 cnf(2627,plain,
% 67.29/67.30 (~E(f14(a8,a8),f1(x26271))),
% 67.29/67.30 inference(scs_inference,[],[37,2568,2599,2555,1741,44,39,190,61,2,56,3])).
% 67.29/67.30 cnf(2631,plain,
% 67.29/67.30 (~P3(f1(x26311),f5(x26312),f12(x26313))),
% 67.29/67.30 inference(scs_inference,[],[37,2568,2599,839,1578,2595,2555,2571,1741,44,39,190,61,2,56,3,28,30,34])).
% 67.29/67.30 cnf(2662,plain,
% 67.29/67.30 (P4(f13(x26621,a8),f13(x26621,a8),f3(x26621,x26621))),
% 67.29/67.30 inference(scs_inference,[],[2601,2597,2595,2547,2,183])).
% 67.29/67.30 cnf(2680,plain,
% 67.29/67.30 (E(f2(x26801,x26802),f12(x26802))),
% 67.29/67.30 inference(rename_variables,[],[2593])).
% 67.29/67.30 cnf(2692,plain,
% 67.29/67.30 (~P2(f14(a8,a8),f6(x26921,a8))),
% 67.29/67.30 inference(scs_inference,[],[2610,2627,1135,2662,2631,757,2559,2593,2680,1505,2563,2555,2595,2561,522,2541,2542,2,28,30,34,33,35,29,67])).
% 67.29/67.30 cnf(2698,plain,
% 67.29/67.30 (~E(f13(a8,a8),f14(a8,a8))),
% 67.29/67.30 inference(scs_inference,[],[2692,2591,2597,139,2,3])).
% 67.29/67.30 cnf(2714,plain,
% 67.29/67.30 (~E(f14(a8,a8),f4(x27141))),
% 67.29/67.30 inference(scs_inference,[],[2624,2698,2555,2,3])).
% 67.29/67.30 cnf(2749,plain,
% 67.29/67.30 (~E(f4(x27491),f14(a8,a8))),
% 67.29/67.30 inference(scs_inference,[],[2714,2])).
% 67.29/67.30 cnf(3083,plain,
% 67.29/67.30 ($false),
% 67.29/67.30 inference(scs_inference,[],[43,2749,2597,2595,28,29,62]),
% 67.29/67.30 ['proof']).
% 67.29/67.30 % SZS output end Proof
% 67.29/67.30 % Total time :66.550000s
%------------------------------------------------------------------------------