%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : NUN086+1 : 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 : 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:43 EDT 2024
% Result : Theorem 66.54s 66.57s
% Output : CNFRefutation 66.57s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : NUN086+1 : TPTP v8.2.0. Released v7.3.0.
% 0.06/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n005.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:15:09 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.42/0.58 start to proof:theBenchmark
% 66.54/66.56 %-------------------------------------------
% 66.54/66.56 % File :CSE---1.7
% 66.54/66.56 % Problem :theBenchmark
% 66.54/66.56 % Transform :cnf
% 66.54/66.56 % Format :tptp:raw
% 66.54/66.56 % Command :java -jar mcs_scs.jar %d %s
% 66.54/66.56
% 66.54/66.56 % Result :Theorem 65.940000s
% 66.54/66.56 % Output :CNFRefutation 65.940000s
% 66.54/66.56 %-------------------------------------------
% 66.54/66.57 %------------------------------------------------------------------------------
% 66.54/66.57 % File : NUN086+1 : TPTP v8.2.0. Released v7.3.0.
% 66.54/66.57 % Domain : Number Theory
% 66.54/66.57 % Problem : Robinson arithmetic: 0 * 1 = 0
% 66.54/66.57 % Version : Especial.
% 66.54/66.57 % English :
% 66.54/66.57
% 66.54/66.57 % Refs : [BBJ03] Boolos et al. (2003), Computability and Logic
% 66.54/66.57 % : [Smi07] Smith (2007), An Introduction to Goedel's Theorems
% 66.54/66.57 % : [Lam18] Lampert (2018), Email to Geoff Sutcliffe
% 66.54/66.57 % Source : [Lam18]
% 66.54/66.57 % Names : zerotimesoneidzero [Lam18]
% 66.54/66.57
% 66.54/66.57 % Status : Theorem
% 66.54/66.57 % Rating : 0.38 v8.2.0, 0.40 v8.1.0, 0.50 v7.5.0, 0.57 v7.4.0, 0.56 v7.3.0
% 66.54/66.57 % Syntax : Number of formulae : 19 ( 1 unt; 0 def)
% 66.54/66.57 % Number of atoms : 81 ( 0 equ)
% 66.54/66.57 % Maximal formula atoms : 7 ( 4 avg)
% 66.54/66.57 % Number of connectives : 96 ( 34 ~; 26 |; 36 &)
% 66.54/66.57 % ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% 66.54/66.57 % Maximal formula depth : 13 ( 8 avg)
% 66.54/66.57 % Maximal term depth : 1 ( 1 avg)
% 66.54/66.57 % Number of predicates : 5 ( 5 usr; 0 prp; 1-3 aty)
% 66.54/66.57 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 66.54/66.57 % Number of variables : 72 ( 47 !; 25 ?)
% 66.54/66.57 % SPC : FOF_THM_RFO_NEQ
% 66.54/66.57
% 66.54/66.57 % Comments : Translated to FOL without equality.
% 66.54/66.57 %------------------------------------------------------------------------------
% 66.54/66.57 include('Axioms/NUM009+0.ax').
% 66.54/66.57 %------------------------------------------------------------------------------
% 66.54/66.57 fof(zerotimesoneidzero,conjecture,
% 66.54/66.57 ? [Y1] :
% 66.54/66.57 ( ? [Y2] :
% 66.54/66.57 ( ? [Y3] :
% 66.54/66.57 ( r1(Y3)
% 66.54/66.57 & r2(Y3,Y2) )
% 66.54/66.57 & ? [Y4] :
% 66.54/66.57 ( r1(Y4)
% 66.54/66.57 & r4(Y4,Y2,Y1) ) )
% 66.54/66.57 & ? [Y5] :
% 66.54/66.57 ( id(Y1,Y5)
% 66.54/66.57 & r1(Y5) ) ) ).
% 66.54/66.57
% 66.54/66.57 %------------------------------------------------------------------------------
% 66.54/66.57 %-------------------------------------------
% 66.54/66.57 % Proof found
% 66.54/66.57 % SZS status Theorem for theBenchmark
% 66.54/66.57 % SZS output start Proof
% 66.57/66.58 %ClaNum:43(EqnAxiom:0)
% 66.57/66.58 %VarNum:211(SingletonVarNum:103)
% 66.57/66.58 %MaxLitNum:6
% 66.57/66.58 %MaxfuncDepth:1
% 66.57/66.58 %SharedTerms:1
% 66.57/66.58 %goalClause: 39
% 66.57/66.58 [4]P2(x41,x41)
% 66.57/66.58 [1]P1(f1(x11))
% 66.57/66.58 [2]P1(f6(x21))
% 66.57/66.58 [3]P1(f8(x31))
% 66.57/66.58 [5]P2(f2(x51),x51)
% 66.57/66.58 [6]P2(f7(x61),f8(x61))
% 66.57/66.58 [12]P4(x121,f1(x121),f2(x121))
% 66.57/66.58 [13]P5(x131,f6(x131),f7(x131))
% 66.57/66.58 [7]P3(x71,f9(x72,x71))
% 66.57/66.58 [8]P3(x81,f3(x82,x81))
% 66.57/66.58 [9]P2(f10(x91,x92),f11(x91,x92))
% 66.57/66.58 [10]P2(f4(x101,x102),f19(x101,x102))
% 66.57/66.58 [11]P3(f20(x111,x112),f11(x111,x112))
% 66.57/66.58 [14]P4(x141,x142,f20(x141,x142))
% 66.57/66.58 [15]P5(x151,x152,f5(x151,x152))
% 66.57/66.58 [16]P4(x161,f9(x161,x162),f10(x161,x162))
% 66.57/66.58 [17]P5(x171,f3(x171,x172),f4(x171,x172))
% 66.57/66.58 [18]P4(f5(x181,x182),x181,f19(x181,x182))
% 66.57/66.58 [19]~P1(x191)+P2(x191,a12)
% 66.57/66.58 [20]P1(x201)+~P2(x201,a12)
% 66.57/66.58 [21]P2(x211,f15(x211))+P1(f13(x211))
% 66.57/66.58 [25]P3(f14(x251),f15(x251))+P1(f13(x251))
% 66.57/66.58 [26]P2(x261,f15(x261))+P2(x261,f13(x261))
% 66.57/66.58 [29]P3(f14(x291),f15(x291))+P2(x291,f13(x291))
% 66.57/66.58 [24]~P2(x242,x241)+P2(x241,x242)
% 66.57/66.58 [27]~P3(x272,x271)+P2(x271,f16(x272))
% 66.57/66.58 [28]P3(x281,x282)+~P2(x282,f16(x281))
% 66.57/66.58 [35]P4(x351,x352,x353)+~P2(x353,f17(x351,x352))
% 66.57/66.58 [36]P5(x361,x362,x363)+~P2(x363,f18(x361,x362))
% 66.57/66.58 [37]~P4(x372,x373,x371)+P2(x371,f17(x372,x373))
% 66.57/66.58 [38]~P5(x382,x383,x381)+P2(x381,f18(x382,x383))
% 66.57/66.58 [22]~P2(x222,x221)+P1(x221)+~P1(x222)
% 66.57/66.58 [23]~P2(x231,x232)+P1(x231)+~P1(x232)
% 66.57/66.58 [30]~P1(x301)+~P2(x301,x302)+~P3(x303,x302)
% 66.57/66.58 [31]~P2(x311,x313)+P2(x311,x312)+~P2(x313,x312)
% 66.57/66.58 [32]~P3(x322,x324)+~P3(x321,x323)+P2(x321,x322)+~P2(x323,x324)
% 66.57/66.58 [33]~P3(x334,x333)+P3(x331,x332)+~P2(x333,x332)+~P2(x334,x331)
% 66.57/66.58 [34]~P3(x344,x343)+P3(x341,x342)+~P2(x342,x343)+~P2(x341,x344)
% 66.57/66.58 [40]~P4(x406,x405,x404)+P4(x401,x402,x403)+~P2(x404,x403)+~P2(x405,x402)+~P2(x406,x401)
% 66.57/66.58 [41]~P4(x416,x415,x414)+P4(x411,x412,x413)+~P2(x413,x414)+~P2(x412,x415)+~P2(x411,x416)
% 66.57/66.58 [42]~P5(x426,x425,x424)+P5(x421,x422,x423)+~P2(x424,x423)+~P2(x425,x422)+~P2(x426,x421)
% 66.57/66.58 [43]~P5(x436,x435,x434)+P5(x431,x432,x433)+~P2(x433,x434)+~P2(x432,x435)+~P2(x431,x436)
% 66.57/66.58 [39]~P5(x392,x395,x394)+~P1(x391)+~P1(x392)+~P2(x394,x391)+~P3(x393,x395)+~P1(x393)
% 66.57/66.58 %EqnAxiom
% 66.57/66.58
% 66.57/66.58 %-------------------------------------------
% 66.57/66.59 cnf(44,plain,
% 66.57/66.59 (P1(a12)),
% 66.57/66.59 inference(scs_inference,[],[4,20])).
% 66.57/66.59 cnf(45,plain,
% 66.57/66.59 (P2(x451,x451)),
% 66.57/66.59 inference(rename_variables,[],[4])).
% 66.57/66.59 cnf(47,plain,
% 66.57/66.59 (P5(x471,x472,f18(x471,x472))),
% 66.57/66.59 inference(scs_inference,[],[4,45,20,36])).
% 66.57/66.59 cnf(48,plain,
% 66.57/66.59 (P2(x481,x481)),
% 66.57/66.59 inference(rename_variables,[],[4])).
% 66.57/66.59 cnf(50,plain,
% 66.57/66.59 (P3(x501,f16(x501))),
% 66.57/66.59 inference(scs_inference,[],[4,45,48,20,36,28])).
% 66.57/66.59 cnf(51,plain,
% 66.57/66.59 (P2(x511,x511)),
% 66.57/66.59 inference(rename_variables,[],[4])).
% 66.57/66.59 cnf(53,plain,
% 66.57/66.59 (P4(x531,x532,f17(x531,x532))),
% 66.57/66.59 inference(scs_inference,[],[4,45,48,51,20,36,28,35])).
% 66.57/66.59 cnf(54,plain,
% 66.57/66.59 (P2(x541,x541)),
% 66.57/66.59 inference(rename_variables,[],[4])).
% 66.57/66.59 cnf(56,plain,
% 66.57/66.59 (~P3(x561,f1(x562))),
% 66.57/66.59 inference(scs_inference,[],[1,4,45,48,51,54,20,36,28,35,30])).
% 66.57/66.59 cnf(57,plain,
% 66.57/66.59 (P2(x571,x571)),
% 66.57/66.59 inference(rename_variables,[],[4])).
% 66.57/66.59 cnf(60,plain,
% 66.57/66.59 (P2(f2(x601),x601)),
% 66.57/66.59 inference(rename_variables,[],[5])).
% 66.57/66.59 cnf(61,plain,
% 66.57/66.59 (P2(x611,x611)),
% 66.57/66.59 inference(rename_variables,[],[4])).
% 66.57/66.59 cnf(64,plain,
% 66.57/66.59 (P2(f2(x641),x641)),
% 66.57/66.59 inference(rename_variables,[],[5])).
% 66.57/66.59 cnf(65,plain,
% 66.57/66.59 (P2(x651,x651)),
% 66.57/66.59 inference(rename_variables,[],[4])).
% 66.57/66.59 cnf(67,plain,
% 66.57/66.59 (P5(x671,x671,f2(f5(x671,x671)))),
% 66.57/66.59 inference(scs_inference,[],[1,4,45,48,51,54,57,61,65,15,5,60,64,11,20,36,28,35,30,33,34,43])).
% 66.57/66.59 cnf(68,plain,
% 66.57/66.59 (P2(f2(x681),x681)),
% 66.57/66.59 inference(rename_variables,[],[5])).
% 66.57/66.59 cnf(70,plain,
% 66.57/66.59 (P2(x701,x701)),
% 66.57/66.59 inference(rename_variables,[],[4])).
% 66.57/66.59 cnf(73,plain,
% 66.57/66.59 (P4(x731,x731,f2(f20(x731,x731)))),
% 66.57/66.59 inference(scs_inference,[],[1,4,45,48,51,54,57,61,65,70,15,5,60,64,68,14,11,20,36,28,35,30,33,34,43,41])).
% 66.57/66.59 cnf(85,plain,
% 66.57/66.59 (P2(f2(x851),x851)),
% 66.57/66.59 inference(rename_variables,[],[5])).
% 66.57/66.59 cnf(87,plain,
% 66.57/66.59 (P1(f2(a12))),
% 66.57/66.59 inference(scs_inference,[],[5,85,28,20])).
% 66.57/66.59 cnf(88,plain,
% 66.57/66.59 (P2(f2(x881),x881)),
% 66.57/66.59 inference(rename_variables,[],[5])).
% 66.57/66.59 cnf(90,plain,
% 66.57/66.59 (P5(x901,x902,f2(f18(x901,x902)))),
% 66.57/66.59 inference(scs_inference,[],[5,85,88,28,20,36])).
% 66.57/66.59 cnf(91,plain,
% 66.57/66.59 (P2(f2(x911),x911)),
% 66.57/66.59 inference(rename_variables,[],[5])).
% 66.57/66.59 cnf(93,plain,
% 66.57/66.59 (P4(x931,x932,f2(f17(x931,x932)))),
% 66.57/66.59 inference(scs_inference,[],[5,85,88,91,28,20,36,35])).
% 66.57/66.59 cnf(96,plain,
% 66.57/66.59 (~P3(x961,a12)),
% 66.57/66.59 inference(scs_inference,[],[44,4,5,85,88,91,28,20,36,35,30])).
% 66.57/66.59 cnf(128,plain,
% 66.57/66.60 (~P3(x1281,f2(a12))),
% 66.57/66.60 inference(scs_inference,[],[87,4,30])).
% 66.57/66.60 cnf(152,plain,
% 66.57/66.60 (~P3(x1521,f6(x1522))),
% 66.57/66.60 inference(scs_inference,[],[2,4,30])).
% 66.57/66.60 cnf(153,plain,
% 66.57/66.60 (P2(x1531,x1531)),
% 66.57/66.60 inference(rename_variables,[],[4])).
% 66.57/66.60 cnf(156,plain,
% 66.57/66.60 (P2(x1561,x1561)),
% 66.57/66.60 inference(rename_variables,[],[4])).
% 66.57/66.60 cnf(157,plain,
% 66.57/66.60 (P3(x1571,f16(x1571))),
% 66.57/66.60 inference(rename_variables,[],[50])).
% 66.57/66.60 cnf(164,plain,
% 66.57/66.60 (P2(f2(x1641),x1641)),
% 66.57/66.60 inference(rename_variables,[],[5])).
% 66.57/66.60 cnf(171,plain,
% 66.57/66.60 (~P1(f19(f1(x1711),f1(x1711)))),
% 66.57/66.60 inference(scs_inference,[],[1,90,17,10,2,50,157,4,153,156,5,164,93,8,30,33,34,40,42,39])).
% 66.57/66.60 cnf(188,plain,
% 66.57/66.60 (~P2(f19(f1(x1881),f1(x1881)),f1(x1882))),
% 66.57/66.60 inference(scs_inference,[],[1,171,22,23])).
% 66.57/66.60 cnf(190,plain,
% 66.57/66.60 (~P3(x1901,f8(x1902))),
% 66.57/66.60 inference(scs_inference,[],[1,171,3,4,22,23,30])).
% 66.57/66.60 cnf(239,plain,
% 66.57/66.60 (P2(f2(x2391),x2391)),
% 66.57/66.60 inference(rename_variables,[],[5])).
% 66.57/66.60 cnf(247,plain,
% 66.57/66.60 (~P5(x2471,x2471,x2471)+P5(f2(x2471),f2(x2471),f2(x2471))),
% 66.57/66.60 inference(scs_inference,[],[5,239,4,50,6,31,33,40,43])).
% 66.57/66.60 cnf(250,plain,
% 66.57/66.60 (P2(f2(x2501),x2501)),
% 66.57/66.60 inference(rename_variables,[],[5])).
% 66.57/66.60 cnf(258,plain,
% 66.57/66.60 (P2(f4(x2581,x2582),f19(x2581,x2582))),
% 66.57/66.60 inference(rename_variables,[],[10])).
% 66.57/66.60 cnf(268,plain,
% 66.57/66.60 (~P5(f8(x2681),f8(x2681),f8(x2681))+P5(f7(x2681),f7(x2681),f7(x2681))),
% 66.57/66.60 inference(scs_inference,[],[1,10,258,5,250,2,188,6,17,67,73,8,40,42,39,22,23,32,43])).
% 66.57/66.60 cnf(282,plain,
% 66.57/66.60 (P2(f6(x2821),a12)),
% 66.57/66.60 inference(scs_inference,[],[2,4,19,22])).
% 66.57/66.60 cnf(443,plain,
% 66.57/66.60 (P3(x4431,f2(f9(x4432,x4431)))),
% 66.57/66.60 inference(scs_inference,[],[7,4,5,34])).
% 66.57/66.60 cnf(506,plain,
% 66.57/66.60 (~P1(f19(f8(x5061),f8(x5061)))),
% 66.57/66.60 inference(scs_inference,[],[10,5,3,443,17,8,33,39])).
% 66.57/66.60 cnf(523,plain,
% 66.57/66.60 (~P1(f19(f2(a12),f2(a12)))),
% 66.57/66.60 inference(scs_inference,[],[10,506,3,87,17,8,23,39])).
% 66.57/66.60 cnf(538,plain,
% 66.57/66.60 (~P1(f19(a12,a12))),
% 66.57/66.60 inference(scs_inference,[],[10,523,3,44,17,8,23,39])).
% 66.57/66.60 cnf(539,plain,
% 66.57/66.60 (P2(f4(x5391,x5392),f19(x5391,x5392))),
% 66.57/66.60 inference(rename_variables,[],[10])).
% 66.57/66.60 cnf(545,plain,
% 66.57/66.60 (~P1(f4(a12,a12))),
% 66.57/66.60 inference(scs_inference,[],[10,539,523,3,44,17,8,23,39,24,22])).
% 66.57/66.60 cnf(783,plain,
% 66.57/66.60 (~P2(f19(a12,a12),a12)),
% 66.57/66.60 inference(scs_inference,[],[44,538,23])).
% 66.57/66.60 cnf(862,plain,
% 66.57/66.60 (~P2(f4(a12,a12),a12)),
% 66.57/66.60 inference(scs_inference,[],[44,545,23])).
% 66.57/66.60 cnf(1759,plain,
% 66.57/66.60 (P3(f6(x17591),f16(a12))),
% 66.57/66.60 inference(scs_inference,[],[282,4,50,34])).
% 66.57/66.60 cnf(2291,plain,
% 66.57/66.60 (~P2(f4(a12,a12),f6(x22911))),
% 66.57/66.60 inference(scs_inference,[],[862,282,31])).
% 66.57/66.60 cnf(2762,plain,
% 66.57/66.60 (~P3(f19(a12,a12),f16(a12))),
% 66.57/66.60 inference(scs_inference,[],[4,783,50,32])).
% 66.57/66.60 cnf(3622,plain,
% 66.57/66.60 (~P3(f4(a12,a12),f16(a12))),
% 66.57/66.60 inference(scs_inference,[],[862,4,50,32])).
% 66.57/66.60 cnf(4198,plain,
% 66.57/66.60 (~P4(x41981,x41981,f2(x41982))+P4(x41981,x41981,x41982)),
% 66.57/66.60 inference(scs_inference,[],[4,5,40])).
% 66.57/66.60 cnf(4209,plain,
% 66.57/66.60 (~P4(x42091,x42091,f2(x42092))+P2(x42092,f17(x42091,x42091))),
% 66.57/66.60 inference(scs_inference,[],[4198,37])).
% 66.57/66.60 cnf(4210,plain,
% 66.57/66.60 (~P5(x42101,x42101,f2(x42102))+P5(x42101,x42101,x42102)),
% 66.57/66.60 inference(scs_inference,[],[4,5,42])).
% 66.57/66.60 cnf(4226,plain,
% 66.57/66.60 (P2(f9(x42261,x42262),f16(x42262))),
% 66.57/66.60 inference(scs_inference,[],[7,27])).
% 66.57/66.60 cnf(4228,plain,
% 66.57/66.60 (P2(f20(x42281,x42282),f17(x42281,x42282))),
% 66.57/66.60 inference(scs_inference,[],[14,7,27,37])).
% 66.57/66.60 cnf(4230,plain,
% 66.57/66.60 (P2(f5(x42301,x42302),f18(x42301,x42302))),
% 66.57/66.60 inference(scs_inference,[],[14,15,7,27,37,38])).
% 66.57/66.60 cnf(4232,plain,
% 66.57/66.60 (~P2(f1(x42321),f16(x42322))),
% 66.57/66.60 inference(scs_inference,[],[56,14,15,7,27,37,38,28])).
% 66.57/66.60 cnf(4234,plain,
% 66.57/66.60 (P2(f1(x42341),a12)),
% 66.57/66.60 inference(scs_inference,[],[1,56,14,15,7,27,37,38,28,19])).
% 66.57/66.60 cnf(4236,plain,
% 66.57/66.60 (P2(x42361,f2(x42361))),
% 66.57/66.60 inference(scs_inference,[],[1,56,14,15,7,5,27,37,38,28,19,24])).
% 66.57/66.60 cnf(4239,plain,
% 66.57/66.60 (P2(x42391,x42391)),
% 66.57/66.60 inference(rename_variables,[],[4])).
% 66.57/66.60 cnf(4241,plain,
% 66.57/66.60 (~P2(f1(x42411),f9(x42412,a12))),
% 66.57/66.60 inference(scs_inference,[],[1,56,1759,14,15,7,5,282,4,27,37,38,28,19,24,30,34])).
% 66.57/66.60 cnf(4243,plain,
% 66.57/66.60 (~P3(x42431,f1(x42432))),
% 66.57/66.60 inference(rename_variables,[],[56])).
% 66.57/66.60 cnf(4245,plain,
% 66.57/66.60 (~P2(f16(a12),f1(x42451))),
% 66.57/66.60 inference(scs_inference,[],[1,56,4243,1759,14,15,7,5,282,4,27,37,38,28,19,24,30,34,33])).
% 66.57/66.60 cnf(4249,plain,
% 66.57/66.60 (P2(a12,f6(x42491))),
% 66.57/66.60 inference(scs_inference,[],[1,56,4243,1759,14,15,7,5,50,282,4,4239,27,37,38,28,19,24,30,34,33,32])).
% 66.57/66.60 cnf(4251,plain,
% 66.57/66.60 (P2(x42511,x42511)),
% 66.57/66.60 inference(rename_variables,[],[4])).
% 66.57/66.60 cnf(4253,plain,
% 66.57/66.60 (P4(f6(x42531),f6(x42531),f20(a12,a12))),
% 66.57/66.60 inference(scs_inference,[],[1,56,4243,1759,14,15,7,5,50,282,4,4239,4251,27,37,38,28,19,24,30,34,33,32,40])).
% 66.57/66.60 cnf(4254,plain,
% 66.57/66.60 (P4(x42541,x42542,f20(x42541,x42542))),
% 66.57/66.60 inference(rename_variables,[],[14])).
% 66.57/66.60 cnf(4255,plain,
% 66.57/66.60 (P2(x42551,x42551)),
% 66.57/66.60 inference(rename_variables,[],[4])).
% 66.57/66.60 cnf(4258,plain,
% 66.57/66.60 (P2(f2(x42581),x42581)),
% 66.57/66.60 inference(rename_variables,[],[5])).
% 66.57/66.60 cnf(4259,plain,
% 66.57/66.60 (P2(f2(x42591),x42591)),
% 66.57/66.60 inference(rename_variables,[],[5])).
% 66.57/66.60 cnf(4261,plain,
% 66.57/66.60 (P2(x42611,x42611)),
% 66.57/66.60 inference(rename_variables,[],[4])).
% 66.57/66.60 cnf(4266,plain,
% 66.57/66.60 (P2(x42661,x42661)),
% 66.57/66.60 inference(rename_variables,[],[4])).
% 66.57/66.60 cnf(4274,plain,
% 66.57/66.60 (P1(f7(x42741))),
% 66.57/66.60 inference(scs_inference,[],[1,56,4243,1759,14,4254,15,7,5,4259,4258,6,50,282,3,4,4239,4251,4255,4261,4266,27,37,38,28,19,24,30,34,33,32,40,41,43,42,20,23])).
% 66.57/66.60 cnf(4277,plain,
% 66.57/66.60 (~P1(f10(x42771,x42772))+P1(f11(x42771,x42772))),
% 66.57/66.60 inference(scs_inference,[],[1,56,4243,1759,14,4254,15,7,5,4259,4258,6,50,282,3,4,4239,4251,4255,4261,4266,9,27,37,38,28,19,24,30,34,33,32,40,41,43,42,20,23,22])).
% 66.57/66.60 cnf(4280,plain,
% 66.57/66.60 (~P1(f10(x42801,x42802))),
% 66.57/66.60 inference(scs_inference,[],[11,4,4277,30])).
% 66.57/66.60 cnf(4281,plain,
% 66.57/66.60 (P2(f3(x42811,x42812),f16(x42812))),
% 66.57/66.60 inference(scs_inference,[],[8,27])).
% 66.57/66.60 cnf(4283,plain,
% 66.57/66.60 (P2(f7(x42831),a12)),
% 66.57/66.60 inference(scs_inference,[],[4274,8,27,19])).
% 66.57/66.60 cnf(4289,plain,
% 66.57/66.60 (P2(f17(x42891,x42892),f20(x42891,x42892))),
% 66.57/66.60 inference(scs_inference,[],[4228,152,4274,4280,8,27,19,28,20,24])).
% 66.57/66.60 cnf(4291,plain,
% 66.57/66.60 (~P2(a12,f16(x42911))),
% 66.57/66.60 inference(scs_inference,[],[4228,152,4232,4274,4280,4234,8,27,19,28,20,24,31])).
% 66.57/66.60 cnf(4294,plain,
% 66.57/66.60 (~P1(f9(x42941,a12))),
% 66.57/66.60 inference(scs_inference,[],[4228,4226,152,4232,4274,4280,4234,1759,8,27,19,28,20,24,31,30])).
% 66.57/66.60 cnf(4299,plain,
% 66.57/66.60 (~P3(x42991,f6(x42992))),
% 66.57/66.60 inference(rename_variables,[],[152])).
% 66.57/66.60 cnf(4301,plain,
% 66.57/66.60 (~P2(f11(x43011,x43012),f6(x43013))),
% 66.57/66.60 inference(scs_inference,[],[4228,4226,152,4299,4232,4274,4280,4234,11,1759,5,8,27,19,28,20,24,31,30,34,33])).
% 66.57/66.60 cnf(4325,plain,
% 66.57/66.60 (P2(f8(x43251),a12)),
% 66.57/66.60 inference(scs_inference,[],[3,19])).
% 66.57/66.60 cnf(4331,plain,
% 66.57/66.60 (P2(f16(x43311),f3(x43312,x43311))),
% 66.57/66.60 inference(scs_inference,[],[4281,190,4294,3,19,28,20,24])).
% 66.57/66.60 cnf(4334,plain,
% 66.57/66.60 (P2(x43341,f2(x43341))),
% 66.57/66.60 inference(rename_variables,[],[4236])).
% 66.57/66.60 cnf(4336,plain,
% 66.57/66.60 (~P1(f3(x43361,a12))),
% 66.57/66.60 inference(scs_inference,[],[4236,4281,190,4294,4291,1759,3,19,28,20,24,31,30])).
% 66.57/66.60 cnf(4339,plain,
% 66.57/66.60 (~P2(f8(x43391),f11(x43392,x43393))),
% 66.57/66.60 inference(scs_inference,[],[4236,4289,4281,190,4294,4291,11,1759,3,19,28,20,24,31,30,34])).
% 66.57/66.60 cnf(4340,plain,
% 66.57/66.60 (P2(f17(x43401,x43402),f20(x43401,x43402))),
% 66.57/66.60 inference(rename_variables,[],[4289])).
% 66.57/66.60 cnf(4341,plain,
% 66.57/66.60 (~P3(x43411,f8(x43412))),
% 66.57/66.60 inference(rename_variables,[],[190])).
% 66.57/66.60 cnf(4343,plain,
% 66.57/66.60 (~P2(f11(x43431,x43432),f8(x43433))),
% 66.57/66.60 inference(scs_inference,[],[4236,4334,4289,4281,190,4341,4294,4291,11,1759,3,19,28,20,24,31,30,34,33])).
% 66.57/66.60 cnf(4345,plain,
% 66.57/66.60 (P2(x43451,f2(x43451))),
% 66.57/66.60 inference(rename_variables,[],[4236])).
% 66.57/66.60 cnf(4347,plain,
% 66.57/66.60 (P4(f2(x43471),a12,x43471)),
% 66.57/66.60 inference(scs_inference,[],[4236,4334,4345,4289,4281,190,4341,4294,12,4291,4234,11,1759,5,3,19,28,20,24,31,30,34,33,40])).
% 66.57/66.60 cnf(4349,plain,
% 66.57/66.60 (P2(x43491,f2(x43491))),
% 66.57/66.60 inference(rename_variables,[],[4236])).
% 66.57/66.60 cnf(4352,plain,
% 66.57/66.60 (P2(f20(x43521,x43522),x43523)+~P2(f11(x43521,x43522),f9(x43524,x43523))),
% 66.57/66.60 inference(scs_inference,[],[4236,4334,4345,4289,4281,190,4341,4294,12,4291,4234,11,1759,7,5,3,19,28,20,24,31,30,34,33,40,32])).
% 66.57/66.60 cnf(4354,plain,
% 66.57/66.60 (P4(f20(x43541,x43542),f7(x43543),f17(x43541,x43542))),
% 66.57/66.60 inference(scs_inference,[],[4236,4334,4345,4349,4289,4340,4281,190,4341,4294,12,4283,4291,4234,11,1759,7,5,3,19,28,20,24,31,30,34,33,40,32,41])).
% 66.57/66.60 cnf(4361,plain,
% 66.57/66.60 (P2(a12,f8(x43611))),
% 66.57/66.60 inference(scs_inference,[],[4325,24])).
% 66.57/66.60 cnf(4368,plain,
% 66.57/66.60 (~P1(f9(x43681,x43682))),
% 66.57/66.60 inference(scs_inference,[],[4331,4245,4336,4325,4226,50,24,20,31,30])).
% 66.57/66.60 cnf(4371,plain,
% 66.57/66.60 (~P2(f16(a12),f2(a12))),
% 66.57/66.60 inference(scs_inference,[],[4331,128,4245,4336,4325,4236,4226,1759,50,24,20,31,30,33])).
% 66.57/66.60 cnf(4377,plain,
% 66.57/66.60 (P4(f8(x43771),f8(x43771),f20(a12,a12))),
% 66.57/66.60 inference(scs_inference,[],[4331,2762,128,4245,4336,4325,4236,4226,4228,53,1759,11,50,24,20,31,30,33,34,41])).
% 66.57/66.60 cnf(4383,plain,
% 66.57/66.60 (P2(a12,f7(x43831))),
% 66.57/66.60 inference(scs_inference,[],[4283,24])).
% 66.57/66.60 cnf(4388,plain,
% 66.57/66.60 (P2(f16(x43881),f3(x43882,x43881))),
% 66.57/66.60 inference(rename_variables,[],[4331])).
% 66.57/66.60 cnf(4390,plain,
% 66.57/66.60 (~P1(f16(x43901))),
% 66.57/66.60 inference(scs_inference,[],[4368,4371,4331,4388,4283,8,24,20,31,30])).
% 66.57/66.60 cnf(4402,plain,
% 66.57/66.60 (P2(f18(x44021,x44022),f5(x44021,x44022))),
% 66.57/66.60 inference(scs_inference,[],[4230,24])).
% 66.57/66.60 cnf(4404,plain,
% 66.57/66.60 (~P2(f16(x44041),a12)),
% 66.57/66.60 inference(scs_inference,[],[4390,4230,24,20])).
% 66.57/66.60 cnf(4410,plain,
% 66.57/66.60 (~P3(x44101,f2(a12))),
% 66.57/66.60 inference(rename_variables,[],[128])).
% 66.57/66.60 cnf(4412,plain,
% 66.57/66.60 (~P2(f11(x44121,x44122),f2(a12))),
% 66.57/66.60 inference(scs_inference,[],[4390,4383,4291,128,4410,4230,4236,4234,11,7,24,20,31,34,33])).
% 66.57/66.60 cnf(4421,plain,
% 66.57/66.60 (P2(f16(x44211),f9(x44212,x44211))),
% 66.57/66.60 inference(scs_inference,[],[4226,24])).
% 66.57/66.60 cnf(4423,plain,
% 66.57/66.60 (~P2(a12,f11(x44231,x44232))),
% 66.57/66.60 inference(scs_inference,[],[4339,4226,4325,24,31])).
% 66.57/66.60 cnf(4436,plain,
% 66.57/66.60 (P2(a12,f1(x44361))),
% 66.57/66.60 inference(scs_inference,[],[4234,24])).
% 66.57/66.60 cnf(4444,plain,
% 66.57/66.60 (~P2(f16(a12),f6(x44441))),
% 66.57/66.60 inference(scs_inference,[],[4404,4281,4331,152,4236,4234,1759,50,24,30,31,33])).
% 66.57/66.60 cnf(4448,plain,
% 66.57/66.60 (P5(f7(x44481),f7(x44481),f5(a12,a12))),
% 66.57/66.60 inference(scs_inference,[],[4404,4281,4331,152,4236,4234,4283,4230,47,1759,50,24,30,31,33,43])).
% 66.57/66.60 cnf(4460,plain,
% 66.57/66.60 (P2(f8(x44601),f7(x44601))),
% 66.57/66.60 inference(scs_inference,[],[6,24])).
% 66.57/66.60 cnf(4462,plain,
% 66.57/66.60 (~P3(x44621,f7(x44622))),
% 66.57/66.60 inference(scs_inference,[],[4383,6,44,24,30])).
% 66.57/66.60 cnf(4467,plain,
% 66.57/66.60 (P5(f8(x44671),f8(x44671),f5(a12,a12))),
% 66.57/66.60 inference(scs_inference,[],[4421,4444,4383,4325,4230,47,6,44,24,30,31,43])).
% 66.57/66.60 cnf(4471,plain,
% 66.57/66.60 (~P5(a12,f9(x44711,a12),f8(x44712))),
% 66.57/66.60 inference(scs_inference,[],[4421,4444,4383,4325,4230,47,7,6,44,24,30,31,43,39])).
% 66.57/66.60 cnf(4474,plain,
% 66.57/66.60 (~P1(f18(x44741,x44742))+P1(f5(x44741,x44742))),
% 66.57/66.60 inference(scs_inference,[],[4421,4444,4402,4383,4325,4230,47,7,6,44,24,30,31,43,39,22])).
% 66.57/66.60 cnf(4485,plain,
% 66.57/66.60 (P2(f19(x44851,x44852),f4(x44851,x44852))),
% 66.57/66.60 inference(scs_inference,[],[10,24])).
% 66.57/66.60 cnf(4491,plain,
% 66.57/66.60 (~P3(x44911,f7(x44912))),
% 66.57/66.60 inference(rename_variables,[],[4462])).
% 66.57/66.60 cnf(4497,plain,
% 66.57/66.60 (P4(f1(x44971),f1(x44971),f20(a12,a12))),
% 66.57/66.60 inference(scs_inference,[],[4462,4491,4423,4436,4289,53,4236,1759,11,10,24,31,34,33,40])).
% 66.57/66.60 cnf(4512,plain,
% 66.57/66.60 (P2(f11(x45121,x45122),f10(x45121,x45122))),
% 66.57/66.60 inference(scs_inference,[],[9,24])).
% 66.57/66.60 cnf(4517,plain,
% 66.57/66.60 (~P2(f7(x45171),f9(x45172,x45173))),
% 66.57/66.60 inference(scs_inference,[],[4241,4462,4234,7,5,9,24,31,34])).
% 66.57/66.60 cnf(4534,plain,
% 66.57/66.60 (~P2(f10(x45341,x45342),f6(x45343))),
% 66.57/66.60 inference(scs_inference,[],[4512,4301,31])).
% 66.57/66.60 cnf(4539,plain,
% 66.57/66.60 (P3(f20(x45391,x45392),f11(x45391,x45392))),
% 66.57/66.60 inference(rename_variables,[],[11])).
% 66.57/66.60 cnf(4541,plain,
% 66.57/66.60 (~P2(f11(x45411,x45412),f7(x45413))),
% 66.57/66.60 inference(scs_inference,[],[4512,4301,4462,128,4236,4289,11,4539,31,34,33])).
% 66.57/66.60 cnf(4558,plain,
% 66.57/66.60 (~P1(f5(x45581,x45582))+P1(f18(x45581,x45582))),
% 66.57/66.60 inference(scs_inference,[],[4343,4512,4280,4402,31,22,23])).
% 66.57/66.60 cnf(4572,plain,
% 66.57/66.60 (~P2(a12,f9(x45721,x45722))),
% 66.57/66.60 inference(scs_inference,[],[4517,4283,31])).
% 66.57/66.60 cnf(4577,plain,
% 66.57/66.60 (P2(f20(x45771,x45772),f17(x45771,x45772))),
% 66.57/66.60 inference(rename_variables,[],[4228])).
% 66.57/66.60 cnf(4584,plain,
% 66.57/66.60 (P2(f8(x45841),f7(x45841))),
% 66.57/66.60 inference(rename_variables,[],[4460])).
% 66.57/66.60 cnf(4587,plain,
% 66.57/66.60 (~P1(f18(x45871,x45872))+~P3(x45873,f5(x45871,x45872))),
% 66.57/66.60 inference(scs_inference,[],[1,4517,4448,4377,4460,4274,4402,4283,4228,4230,1759,2,4,31,40,42,39,30])).
% 66.57/66.60 cnf(4589,plain,
% 66.57/66.60 (P4(f17(x45891,x45892),f8(x45893),f20(x45891,x45892))),
% 66.57/66.60 inference(scs_inference,[],[1,4517,4448,4377,4354,4460,4584,4274,4402,4283,4228,4577,4230,4289,1759,2,4,31,40,42,39,30,41])).
% 66.57/66.60 cnf(4593,plain,
% 66.57/66.60 (~P1(f18(x45931,x45932))+~P2(f5(x45931,x45932),f16(x45933))),
% 66.57/66.60 inference(scs_inference,[],[1,4517,4448,4377,4354,4460,4584,4274,4402,4283,4228,4577,4230,4289,1759,2,4,31,40,42,39,30,41,28])).
% 66.57/66.60 cnf(4598,plain,
% 66.57/66.60 (P4(f1(x45981),f1(x45981),f17(a12,a12))),
% 66.57/66.60 inference(scs_inference,[],[4572,4436,14,4234,4289,31,41])).
% 66.57/66.60 cnf(4614,plain,
% 66.57/66.60 (P1(f17(x46141,x46142))+~P2(f20(x46141,x46142),a12)),
% 66.57/66.60 inference(scs_inference,[],[4541,4512,4228,31,22,23,20])).
% 66.57/66.60 cnf(4627,plain,
% 66.57/66.60 (~P1(f5(x46271,x46272))+~P3(x46273,f18(x46271,x46272))),
% 66.57/66.60 inference(scs_inference,[],[4412,4512,4230,31,30])).
% 66.57/66.60 cnf(4632,plain,
% 66.57/66.60 (P4(f20(x46321,x46322),a12,f17(x46321,x46322))),
% 66.57/66.60 inference(scs_inference,[],[4589,4371,4421,4361,4228,4289,31,41])).
% 66.57/66.60 cnf(4645,plain,
% 66.57/66.60 (P4(f17(x46451,x46452),f7(x46453),f20(x46451,x46452))),
% 66.57/66.60 inference(scs_inference,[],[4632,4245,4467,4471,4421,4283,4325,4228,4289,31,42,41])).
% 66.57/66.60 cnf(4652,plain,
% 66.57/66.60 (P4(f2(x46521),f16(x46522),f11(x46521,x46522))),
% 66.57/66.60 inference(scs_inference,[],[16,4444,4421,4331,4512,5,31,41])).
% 66.57/66.60 cnf(4666,plain,
% 66.57/66.60 (P4(x46661,f9(x46662,x46663),f10(x46661,x46663))),
% 66.57/66.60 inference(scs_inference,[],[4652,4421,4512,5,40])).
% 66.57/66.60 cnf(4675,plain,
% 66.57/66.60 (P4(f20(x46751,x46752),f8(x46753),f17(x46751,x46752))),
% 66.57/66.60 inference(scs_inference,[],[4645,4460,4289,4228,41])).
% 66.57/66.60 cnf(4680,plain,
% 66.57/66.60 (P4(f9(x46801,x46802),a12,f16(x46802))),
% 66.57/66.60 inference(scs_inference,[],[12,4226,4436,4236,41])).
% 66.57/66.60 cnf(4688,plain,
% 66.57/66.60 (P4(f16(x46881),f6(x46882),f9(x46883,x46881))),
% 66.57/66.60 inference(scs_inference,[],[4680,4572,4249,4226,4421,31,40])).
% 66.57/66.60 cnf(4733,plain,
% 66.57/66.60 (P4(f8(x47331),f16(x47332),f11(a12,x47332))),
% 66.57/66.60 inference(scs_inference,[],[4666,4421,4325,4512,41])).
% 66.57/66.60 cnf(4734,plain,
% 66.57/66.60 (P4(x47341,f9(x47342,x47343),f10(x47341,x47343))),
% 66.57/66.60 inference(rename_variables,[],[4666])).
% 66.57/66.60 cnf(4738,plain,
% 66.57/66.60 (P4(f2(x47381),f16(x47382),f10(x47381,x47382))),
% 66.57/66.60 inference(scs_inference,[],[4666,4734,4226,4421,4325,4236,4512,4,41,40])).
% 66.57/66.60 cnf(4744,plain,
% 66.57/66.60 (P4(f16(x47441),f8(x47442),f3(x47443,x47441))),
% 66.57/66.60 inference(scs_inference,[],[4680,4361,4331,4226,40])).
% 66.57/66.60 cnf(4746,plain,
% 66.57/66.60 (P2(f9(x47461,x47462),f16(x47462))),
% 66.57/66.60 inference(rename_variables,[],[4226])).
% 66.57/66.60 cnf(4748,plain,
% 66.57/66.60 (P5(f2(x47481),f8(x47482),f18(x47481,a12))),
% 66.57/66.60 inference(scs_inference,[],[4680,4361,4331,4226,15,4236,4230,40,42])).
% 66.57/66.60 cnf(4749,plain,
% 66.57/66.60 (P2(x47491,f2(x47491))),
% 66.57/66.60 inference(rename_variables,[],[4236])).
% 66.57/66.60 cnf(4753,plain,
% 66.57/66.60 (P4(x47531,f3(x47532,x47533),f11(x47531,x47533))),
% 66.57/66.60 inference(scs_inference,[],[4738,4680,4361,4331,4281,4226,15,4236,4749,4512,4230,40,42,41])).
% 66.57/66.60 cnf(4767,plain,
% 66.57/66.60 (~P2(f16(a12),f8(x47671))),
% 66.57/66.60 inference(scs_inference,[],[2,4738,4680,190,4274,4361,4331,4281,4226,4746,4460,15,4236,4749,4512,4230,1759,7,40,42,41,39,33,31])).
% 66.57/66.60 cnf(4773,plain,
% 66.57/66.60 (P5(x47731,f7(x47732),f5(x47731,a12))),
% 66.57/66.60 inference(scs_inference,[],[4748,4767,4331,4236,4230,6,31,43])).
% 66.57/66.60 cnf(4779,plain,
% 66.57/66.60 (P4(f7(x47791),f3(x47792,x47793),f10(a12,x47793))),
% 66.57/66.60 inference(scs_inference,[],[4753,4383,4512,4,40])).
% 66.57/66.60 cnf(4785,plain,
% 66.57/66.60 (P4(a12,f1(x47851),f20(a12,a12))),
% 66.57/66.60 inference(scs_inference,[],[4598,4436,4228,4,41])).
% 66.57/66.60 cnf(4790,plain,
% 66.57/66.60 (P5(f2(x47901),a12,f18(x47901,a12))),
% 66.57/66.60 inference(scs_inference,[],[4773,4383,4402,5,43])).
% 66.57/66.60 cnf(4792,plain,
% 66.57/66.60 (P2(a12,f7(x47921))),
% 66.57/66.60 inference(rename_variables,[],[4383])).
% 66.57/66.60 cnf(4798,plain,
% 66.57/66.60 (P4(f18(a12,x47981),f7(x47982),f4(a12,x47981))),
% 66.57/66.60 inference(scs_inference,[],[4534,4773,18,4383,4792,4485,4402,4230,5,43,32,40])).
% 66.57/66.60 cnf(4803,plain,
% 66.57/66.60 (P4(f9(x48031,x48032),f7(x48033),f16(x48032))),
% 66.57/66.60 inference(scs_inference,[],[4744,4281,4421,4460,40])).
% 66.57/66.60 cnf(4805,plain,
% 66.57/66.60 (P2(f16(x48051),f9(x48052,x48051))),
% 66.57/66.60 inference(rename_variables,[],[4421])).
% 66.57/66.60 cnf(4813,plain,
% 66.57/66.60 (P4(f3(x48131,x48132),a12,f16(x48132))),
% 66.57/66.60 inference(scs_inference,[],[4688,4744,4790,4249,4281,4421,4805,4460,4402,4236,5,40,42,41])).
% 66.57/66.60 cnf(4818,plain,
% 66.57/66.60 (P4(f16(x48181),a12,f9(x48182,x48181))),
% 66.57/66.60 inference(scs_inference,[],[4803,4383,4226,4421,41])).
% 66.57/66.60 cnf(4829,plain,
% 66.57/66.60 (~P2(f17(x48291,x48292),f4(a12,a12))+~P2(f11(x48291,x48292),f16(a12))),
% 66.57/66.60 inference(scs_inference,[],[4803,4790,3622,4383,4226,4421,4325,4236,4230,4228,11,41,43,33,31])).
% 66.57/66.60 cnf(4850,plain,
% 66.57/66.60 (P4(f6(x48501),f6(x48501),f17(a12,a12))),
% 66.57/66.60 inference(scs_inference,[],[14,4436,4289,7,1,282,44,39,41])).
% 66.57/66.60 cnf(4860,plain,
% 66.57/66.60 (P2(a12,f8(x48601))),
% 66.57/66.60 inference(rename_variables,[],[4361])).
% 66.57/66.60 cnf(4863,plain,
% 66.57/66.60 (P4(f3(x48631,x48632),f8(x48633),f16(x48632))),
% 66.57/66.60 inference(scs_inference,[],[3,4818,4331,4361,4860,4226,1759,2,39,40])).
% 66.57/66.60 cnf(4867,plain,
% 66.57/66.60 (P4(f16(x48671),f7(x48672),f3(x48673,x48671))),
% 66.57/66.60 inference(scs_inference,[],[4863,4331,4281,4460,40])).
% 66.57/66.60 cnf(4876,plain,
% 66.57/66.60 (P4(a12,f16(x48761),f11(a12,x48761))),
% 66.57/66.60 inference(scs_inference,[],[4779,4383,4331,4512,41])).
% 66.57/66.60 cnf(4880,plain,
% 66.57/66.60 (P2(f11(x48801,x48802),f10(x48801,x48802))),
% 66.57/66.60 inference(rename_variables,[],[4512])).
% 66.57/66.60 cnf(4885,plain,
% 66.57/66.60 (P1(f17(x48851,x48852))+~P3(a12,f10(x48851,x48852))),
% 66.57/66.60 inference(scs_inference,[],[4779,4383,4331,4512,4880,11,41,32,4614])).
% 66.57/66.60 cnf(4912,plain,
% 66.57/66.60 (P5(x49121,f1(x49122),f5(x49121,a12))),
% 66.57/66.60 inference(scs_inference,[],[4785,4790,4436,4283,4234,4230,4236,4289,41,43])).
% 66.57/66.60 cnf(4923,plain,
% 66.57/66.60 (~P2(f10(x49231,x49232),f1(x49233))),
% 66.57/66.60 inference(scs_inference,[],[56,4512,4236,11,33,31])).
% 66.57/66.60 cnf(4925,plain,
% 66.57/66.60 (P4(a12,f6(x49251),f20(a12,a12))),
% 66.57/66.60 inference(scs_inference,[],[4850,4249,4228,4,41])).
% 66.57/66.60 cnf(4927,plain,
% 66.57/66.60 (P2(a12,f6(x49271))),
% 66.57/66.60 inference(rename_variables,[],[4249])).
% 66.57/66.60 cnf(4930,plain,
% 66.57/66.60 (P4(f6(x49301),f9(x49302,x49303),f10(a12,x49303))),
% 66.57/66.60 inference(scs_inference,[],[4850,4876,4249,4927,4421,4512,4228,4,41,40])).
% 66.57/66.60 cnf(4940,plain,
% 66.57/66.60 (P4(f8(x49401),a12,f17(a12,a12))),
% 66.57/66.60 inference(scs_inference,[],[4925,4249,4325,4289,41])).
% 66.57/66.60 cnf(4944,plain,
% 66.57/66.60 (P4(f3(x49441,x49442),f7(x49443),f16(x49442))),
% 66.57/66.60 inference(scs_inference,[],[4,4867,4281,4331,41])).
% 66.57/66.60 cnf(4946,plain,
% 66.57/66.60 (P2(x49461,x49461)),
% 66.57/66.60 inference(rename_variables,[],[4])).
% 66.57/66.60 cnf(4951,plain,
% 66.57/66.60 (P2(x49511,x49511)),
% 66.57/66.60 inference(rename_variables,[],[4])).
% 66.57/66.60 cnf(4952,plain,
% 66.57/66.60 (P2(f18(x49521,x49522),f5(x49521,x49522))),
% 66.57/66.60 inference(rename_variables,[],[4402])).
% 66.57/66.60 cnf(4954,plain,
% 66.57/66.60 (P5(f2(x49541),f1(x49542),f18(x49541,a12))),
% 66.57/66.60 inference(scs_inference,[],[4,4946,4951,4867,4912,4790,4361,4281,4331,4402,4952,5,41,42,43])).
% 66.57/66.60 cnf(4966,plain,
% 66.57/66.60 (P2(x49661,x49661)),
% 66.57/66.60 inference(rename_variables,[],[4])).
% 66.57/66.60 cnf(4968,plain,
% 66.57/66.60 (P5(f2(x49681),a12,f5(x49681,a12))),
% 66.57/66.60 inference(scs_inference,[],[4,4966,4954,4274,4436,4230,1759,2,39,43])).
% 66.57/66.61 cnf(4987,plain,
% 66.57/66.61 (P4(f7(x49871),f16(x49872),f10(a12,x49872))),
% 66.57/66.61 inference(scs_inference,[],[4,4733,4460,4512,40])).
% 66.57/66.61 cnf(4996,plain,
% 66.57/66.61 (P2(x49961,x49961)),
% 66.57/66.61 inference(rename_variables,[],[4])).
% 66.57/66.61 cnf(4999,plain,
% 66.57/66.61 (P4(a12,f9(x49991,x49992),f11(a12,x49992))),
% 66.57/66.61 inference(scs_inference,[],[4,4996,4944,4930,4249,4421,4281,4512,40,41])).
% 66.57/66.61 cnf(5006,plain,
% 66.57/66.61 (P4(f5(a12,x50061),f7(x50062),f19(a12,x50061))),
% 66.57/66.61 inference(scs_inference,[],[4,4798,4485,4230,41])).
% 66.57/66.61 cnf(5019,plain,
% 66.57/66.61 (~P3(x50191,f5(x50192,x50193))+~P1(f5(x50192,x50193))),
% 66.57/66.61 inference(scs_inference,[],[4587,4558])).
% 66.57/66.61 cnf(5049,plain,
% 66.57/66.61 (~P1(f5(x50491,x50492))+~P2(f18(x50491,x50492),f16(x50493))),
% 66.57/66.61 inference(scs_inference,[],[4627,28])).
% 66.57/66.61 cnf(5061,plain,
% 66.57/66.61 (P4(f7(x50611),f8(x50612),f20(a12,a12))),
% 66.57/66.61 inference(scs_inference,[],[4940,4361,4460,4289,40])).
% 66.57/66.61 cnf(5072,plain,
% 66.57/66.61 (P4(f18(a12,x50721),a12,f4(a12,x50721))),
% 66.57/66.61 inference(scs_inference,[],[5006,4283,4485,4230,40])).
% 66.57/66.61 cnf(5131,plain,
% 66.57/66.61 (P4(a12,f7(x51311),f17(a12,a12))),
% 66.57/66.61 inference(scs_inference,[],[6,5061,4999,4436,4383,4226,4512,4289,40,41])).
% 66.57/66.61 cnf(5135,plain,
% 66.57/66.61 (~P1(f5(x51351,x51352))+~P2(f5(x51351,x51352),f16(x51353))),
% 66.57/66.61 inference(scs_inference,[],[5019,28])).
% 66.57/66.61 cnf(5136,plain,
% 66.57/66.61 (~P2(f9(x51361,x51362),f7(x51363))),
% 66.57/66.61 inference(scs_inference,[],[7,4462,4236,33])).
% 66.57/66.61 cnf(5141,plain,
% 66.57/66.61 (~P2(f16(x51411),f7(x51412))),
% 66.57/66.61 inference(scs_inference,[],[5136,4226,31])).
% 66.57/66.61 cnf(5148,plain,
% 66.57/66.61 (P4(f1(x51481),f7(x51482),f20(a12,a12))),
% 66.57/66.61 inference(scs_inference,[],[7,5136,5131,128,4436,4226,4289,5,4,31,34,40])).
% 66.57/66.61 cnf(5149,plain,
% 66.57/66.61 (P2(x51491,x51491)),
% 66.57/66.61 inference(rename_variables,[],[4])).
% 66.57/66.61 cnf(5150,plain,
% 66.57/66.61 (P2(f17(x51501,x51502),f20(x51501,x51502))),
% 66.57/66.61 inference(rename_variables,[],[4289])).
% 66.57/66.61 cnf(5152,plain,
% 66.57/66.61 (P4(f1(x51521),a12,f17(a12,a12))),
% 66.57/66.61 inference(scs_inference,[],[7,5136,5131,4497,128,4436,4226,4289,5150,5,4,5149,31,34,40,41])).
% 66.57/66.61 cnf(5161,plain,
% 66.57/66.61 (P5(x51611,f8(x51612),f18(x51611,a12))),
% 66.57/66.61 inference(scs_inference,[],[5141,4968,4331,4325,4402,4236,31,43])).
% 66.57/66.61 cnf(5171,plain,
% 66.57/66.61 (P4(f20(x51711,x51712),f7(x51713),f20(x51711,x51712))),
% 66.57/66.61 inference(scs_inference,[],[4675,5141,4987,4968,4281,4331,4460,4325,4402,4512,4289,4236,4,31,43,41,40])).
% 66.57/66.61 cnf(5175,plain,
% 66.57/66.61 (P2(f17(x51751,x51751),x51752)+~P4(x51751,x51751,f2(x51752))),
% 66.57/66.61 inference(scs_inference,[],[4209,24])).
% 66.57/66.61 cnf(5176,plain,
% 66.57/66.61 (P4(f17(x51761,x51762),a12,f17(x51761,x51762))),
% 66.57/66.61 inference(scs_inference,[],[5171,4283,4228,40])).
% 66.57/66.61 cnf(5184,plain,
% 66.57/66.61 (~P1(f18(x51841,x51842))+~P2(f16(x51843),f5(x51841,x51842))),
% 66.57/66.61 inference(scs_inference,[],[4593,24])).
% 66.57/66.61 cnf(5191,plain,
% 66.57/66.61 (~P2(a12,f3(x51911,a12))),
% 66.57/66.61 inference(scs_inference,[],[8,96,4234,34])).
% 66.57/66.61 cnf(5223,plain,
% 66.57/66.61 (~P2(f3(x52231,x52232),f1(x52233))),
% 66.57/66.61 inference(scs_inference,[],[8,5191,5161,56,4249,4325,4402,4236,31,42,33])).
% 66.57/66.61 cnf(5227,plain,
% 66.57/66.61 (P4(a12,f6(x52271),f17(a12,a12))),
% 66.57/66.61 inference(scs_inference,[],[8,5191,5161,4253,56,4249,4325,4402,4289,4236,4,31,42,33,41])).
% 66.57/66.61 cnf(5234,plain,
% 66.57/66.61 (~P2(f8(x52341),f3(x52342,a12))),
% 66.57/66.61 inference(scs_inference,[],[5191,4361,31])).
% 66.57/66.61 cnf(5236,plain,
% 66.57/66.61 (~P2(f6(x52361),f3(x52362,x52363))),
% 66.57/66.61 inference(scs_inference,[],[8,5191,152,4361,5,31,34])).
% 66.57/66.61 cnf(5240,plain,
% 66.57/66.61 (P4(f20(x52401,x52402),f8(x52403),f20(x52401,x52402))),
% 66.57/66.61 inference(scs_inference,[],[8,5176,5191,152,4361,4289,5,31,34,40])).
% 66.57/66.61 cnf(5241,plain,
% 66.57/66.61 (P2(f17(x52411,x52412),f20(x52411,x52412))),
% 66.57/66.61 inference(rename_variables,[],[4289])).
% 66.57/66.61 cnf(5243,plain,
% 66.57/66.61 (P4(a12,f8(x52431),f17(a12,a12))),
% 66.57/66.61 inference(scs_inference,[],[8,5148,5176,5191,152,4361,4436,4460,4289,5241,5,31,34,40,41])).
% 66.57/66.61 cnf(5257,plain,
% 66.57/66.61 (~P2(f16(x52571),f1(x52572))),
% 66.57/66.61 inference(scs_inference,[],[5223,4281,31])).
% 66.57/66.61 cnf(5260,plain,
% 66.57/66.61 (P5(f16(x52601),a12,a12)),
% 66.57/66.61 inference(scs_inference,[],[5223,13,4331,4281,4383,4249,31,43])).
% 66.57/66.61 cnf(5278,plain,
% 66.57/66.61 (P2(f16(x52781),f9(x52782,x52781))),
% 66.57/66.61 inference(rename_variables,[],[4421])).
% 66.57/66.61 cnf(5280,plain,
% 66.57/66.61 (P5(f9(x52801,x52802),f1(x52803),f1(x52803))),
% 66.57/66.61 inference(scs_inference,[],[5257,5260,4421,5278,4436,31,42])).
% 66.57/66.61 cnf(5297,plain,
% 66.57/66.61 (P5(f16(x52971),f1(x52972),f1(x52972))),
% 66.57/66.61 inference(scs_inference,[],[5280,5234,4421,4460,4,31,43])).
% 66.57/66.61 cnf(5301,plain,
% 66.57/66.61 (~P2(f3(x53011,x53012),f8(x53013))),
% 66.57/66.61 inference(scs_inference,[],[8,5280,5234,190,4421,4460,4236,4,31,43,33])).
% 66.57/66.61 cnf(5309,plain,
% 66.57/66.61 (~P2(a12,f3(x53091,x53092))),
% 66.57/66.61 inference(scs_inference,[],[5236,282,31])).
% 66.57/66.61 cnf(5312,plain,
% 66.57/66.61 (~P2(f2(a12),f3(x53121,a12))),
% 66.57/66.61 inference(scs_inference,[],[8,5236,128,4283,282,31,34])).
% 66.57/66.61 cnf(5316,plain,
% 66.57/66.61 (P5(f9(x53161,x53162),a12,a12)),
% 66.57/66.61 inference(scs_inference,[],[8,5297,5236,128,4283,4436,4226,282,31,34,43])).
% 66.57/66.61 cnf(5325,plain,
% 66.57/66.61 (~P2(f16(x53251),f8(x53252))),
% 66.57/66.61 inference(scs_inference,[],[5301,4281,31])).
% 66.57/66.61 cnf(5344,plain,
% 66.57/66.61 (P2(f16(x53441),f9(x53442,x53441))),
% 66.57/66.61 inference(rename_variables,[],[4421])).
% 66.57/66.61 cnf(5349,plain,
% 66.57/66.61 (P4(a12,f8(x53491),f20(a12,a12))),
% 66.57/66.61 inference(scs_inference,[],[5325,5152,5316,4421,5344,4283,4325,4436,4228,31,43,41])).
% 66.57/66.61 cnf(5353,plain,
% 66.57/66.61 (P4(f20(x53531,x53532),a12,f20(x53531,x53532))),
% 66.57/66.61 inference(scs_inference,[],[5240,5325,5152,5316,4421,5344,4283,4325,4436,4228,4,31,43,41,40])).
% 66.57/66.61 cnf(5362,plain,
% 66.57/66.61 (P4(f6(x53621),f7(x53622),f20(a12,a12))),
% 66.57/66.61 inference(scs_inference,[],[5353,5243,4234,4249,4460,4289,41,40])).
% 66.57/66.61 cnf(5388,plain,
% 66.57/66.61 (P4(f5(a12,x53881),f1(x53882),f19(a12,x53881))),
% 66.57/66.61 inference(scs_inference,[],[5072,5309,4234,4485,4436,4230,31,41])).
% 66.57/66.61 cnf(5394,plain,
% 66.57/66.61 (P4(f8(x53941),a12,f20(a12,a12))),
% 66.57/66.61 inference(scs_inference,[],[5227,4325,4249,4228,41])).
% 66.57/66.61 cnf(5409,plain,
% 66.57/66.61 (~P2(f18(x54091,x54092),f16(x54093))+~P1(f18(x54091,x54092))),
% 66.57/66.61 inference(scs_inference,[],[5049,4474])).
% 66.57/66.61 cnf(5424,plain,
% 66.57/66.61 (P2(f20(x54241,x54242),x54243)+~P2(f11(x54241,x54242),f3(x54244,x54243))),
% 66.57/66.61 inference(scs_inference,[],[11,5362,4383,4289,8,4,41,32])).
% 66.57/66.61 cnf(5440,plain,
% 66.57/66.61 (P4(a12,f1(x54401),f17(a12,a12))),
% 66.57/66.61 inference(scs_inference,[],[4923,5394,4234,4361,4485,4289,32,41])).
% 66.57/66.61 cnf(5450,plain,
% 66.57/66.61 (P2(f20(x54501,x54502),f17(x54501,x54502))),
% 66.57/66.61 inference(rename_variables,[],[4228])).
% 66.57/66.61 cnf(5458,plain,
% 66.57/66.61 (P2(f20(x54581,x54582),x54583)+~P2(f9(x54584,x54583),f11(x54581,x54582))),
% 66.57/66.61 inference(scs_inference,[],[11,5349,5440,4383,4234,4436,7,4228,5450,4,41,40,32,24])).
% 66.57/66.61 cnf(5531,plain,
% 66.57/66.61 (~P2(f16(x55311),f5(x55312,x55313))+~P1(f5(x55312,x55313))),
% 66.57/66.61 inference(scs_inference,[],[5184,4558])).
% 66.57/66.61 cnf(5535,plain,
% 66.57/66.61 (~P2(f18(x55351,x55352),f16(x55353))+~P2(f18(x55351,x55352),a12)),
% 66.57/66.61 inference(scs_inference,[],[5409,20])).
% 66.57/66.61 cnf(5536,plain,
% 66.57/66.61 (P5(f2(x55361),a12,a12)),
% 66.57/66.61 inference(scs_inference,[],[13,4283,4236,282,42])).
% 66.57/66.61 cnf(5546,plain,
% 66.57/66.61 (~P2(f9(x55461,x55462),f5(x55463,x55464))+~P1(f5(x55463,x55464))),
% 66.57/66.61 inference(scs_inference,[],[4421,5531,31])).
% 66.57/66.61 cnf(5550,plain,
% 66.57/66.61 (P5(x55501,f8(x55502),f8(x55502))),
% 66.57/66.61 inference(scs_inference,[],[5536,4325,4234,1759,4274,4236,2,44,39,43])).
% 66.57/66.61 cnf(5554,plain,
% 66.57/66.61 (P5(f7(x55541),f7(x55541),f7(x55541))),
% 66.57/66.61 inference(scs_inference,[],[5550,268])).
% 66.57/66.61 cnf(5567,plain,
% 66.57/66.61 (P4(f5(a12,x55671),f8(x55672),f19(a12,x55671))),
% 66.57/66.61 inference(scs_inference,[],[5072,4325,4485,4230,41])).
% 66.57/66.61 cnf(5583,plain,
% 66.57/66.61 (P5(a12,a12,a12)),
% 66.57/66.61 inference(scs_inference,[],[5312,5554,4813,4281,4331,4436,4383,4402,40,32,43])).
% 66.57/66.61 cnf(5590,plain,
% 66.57/66.61 (P2(a12,f18(a12,a12))),
% 66.57/66.61 inference(scs_inference,[],[5583,247,38])).
% 66.57/66.61 cnf(5592,plain,
% 66.57/66.61 (P2(f18(a12,a12),a12)),
% 66.57/66.61 inference(scs_inference,[],[5583,247,38,24])).
% 66.57/66.61 cnf(5594,plain,
% 66.57/66.61 (~P2(f18(a12,a12),f11(x55941,x55942))),
% 66.57/66.61 inference(scs_inference,[],[5583,4423,247,38,24,31])).
% 66.57/66.61 cnf(5596,plain,
% 66.57/66.61 (P5(f18(a12,a12),f18(a12,a12),f18(a12,a12))),
% 66.57/66.61 inference(scs_inference,[],[5583,4423,247,38,24,31,42])).
% 66.57/66.61 cnf(5610,plain,
% 66.57/66.61 (P1(f5(a12,a12))),
% 66.57/66.61 inference(scs_inference,[],[5583,4423,53,4234,4402,4228,44,247,38,24,31,42,41,43,4210,5535,23,22])).
% 66.57/66.61 cnf(5611,plain,
% 66.57/66.61 (P2(f18(x56111,x56112),f5(x56111,x56112))),
% 66.57/66.61 inference(rename_variables,[],[4402])).
% 66.57/66.61 cnf(5613,plain,
% 66.57/66.61 (~P3(x56131,f5(a12,a12))),
% 66.57/66.61 inference(scs_inference,[],[5583,4423,53,4234,4402,5611,4228,44,247,38,24,31,42,41,43,4210,5535,23,22,30])).
% 66.57/66.61 cnf(5620,plain,
% 66.57/66.61 (P2(f5(a12,a12),a12)),
% 66.57/66.61 inference(scs_inference,[],[5583,4423,53,4234,4402,5611,4228,44,247,38,24,31,42,41,43,4210,5535,23,22,30,5135,5184,19])).
% 66.57/66.61 cnf(5622,plain,
% 66.57/66.61 (~P3(x56221,f18(a12,a12))),
% 66.57/66.61 inference(scs_inference,[],[5610,4627])).
% 66.57/66.61 cnf(5626,plain,
% 66.57/66.61 (P2(a12,f5(a12,a12))),
% 66.57/66.61 inference(scs_inference,[],[5610,5620,4627,5546,24])).
% 66.57/66.61 cnf(5632,plain,
% 66.57/66.61 (~P3(x56321,f5(a12,a12))),
% 66.57/66.61 inference(rename_variables,[],[5613])).
% 66.57/66.61 cnf(5634,plain,
% 66.57/66.61 (~P2(f11(x56341,x56342),f5(a12,a12))),
% 66.57/66.61 inference(scs_inference,[],[5613,5632,5610,5592,5620,5590,5309,7,4236,11,4627,5546,24,31,34,33])).
% 66.57/66.61 cnf(5638,plain,
% 66.57/66.61 (P5(f5(a12,a12),f5(a12,a12),f5(a12,a12))),
% 66.57/66.61 inference(scs_inference,[],[5596,5613,5632,5610,5592,5620,5590,5309,4402,7,4236,11,4627,5546,24,31,34,33,42])).
% 66.57/66.61 cnf(5668,plain,
% 66.57/66.61 (P4(f5(a12,a12),f5(a12,a12),f17(a12,a12))),
% 66.57/66.61 inference(scs_inference,[],[14,5634,5622,5620,5626,5610,1759,4512,7,4289,2,31,39,34,41])).
% 66.57/66.61 cnf(5696,plain,
% 66.57/66.61 (P4(a12,f7(x56961),f4(a12,a12))),
% 66.57/66.61 inference(scs_inference,[],[5594,5567,5638,5626,5620,4460,4485,4402,4,31,43,40])).
% 66.57/66.61 cnf(5739,plain,
% 66.57/66.61 (P4(f5(a12,a12),f5(a12,a12),f20(a12,a12))),
% 66.57/66.61 inference(scs_inference,[],[5309,5626,53,4289,31,40])).
% 66.57/66.61 cnf(5758,plain,
% 66.57/66.61 (P2(f19(x57581,x57582),f4(x57581,x57582))),
% 66.57/66.61 inference(rename_variables,[],[4485])).
% 66.57/66.61 cnf(5766,plain,
% 66.57/66.61 (P2(f17(a12,a12),f4(a12,a12))),
% 66.57/66.61 inference(scs_inference,[],[5696,5388,5592,5620,4383,4234,4485,5758,41,40,37,24])).
% 66.57/66.61 cnf(5768,plain,
% 66.57/66.61 (~P1(f17(a12,a12))),
% 66.57/66.61 inference(scs_inference,[],[5696,5388,545,5592,5620,4383,4234,4485,5758,41,40,37,24,22])).
% 66.57/66.61 cnf(5775,plain,
% 66.57/66.61 (~P2(f20(a12,a12),a12)),
% 66.57/66.61 inference(scs_inference,[],[5696,5388,2291,545,5592,5620,4383,4234,4485,5758,4289,41,40,37,24,22,23,31,4614])).
% 66.57/66.61 cnf(5777,plain,
% 66.57/66.61 (~P2(f17(a12,a12),a12)),
% 66.57/66.61 inference(scs_inference,[],[5696,5388,2291,545,5592,5620,4383,4234,4485,5758,4289,41,40,37,24,22,23,31,4614,20])).
% 66.57/66.61 cnf(5782,plain,
% 66.57/66.61 (~P3(a12,f10(a12,a12))),
% 66.57/66.61 inference(scs_inference,[],[5768,4885])).
% 66.57/66.61 cnf(5784,plain,
% 66.57/66.61 (~P4(a12,a12,f2(a12))),
% 66.57/66.61 inference(scs_inference,[],[5768,5777,4885,5175])).
% 66.57/66.61 cnf(5800,plain,
% 66.57/66.61 (~P2(f11(a12,a12),f9(x58001,a12))),
% 66.57/66.61 inference(scs_inference,[],[5668,5766,5768,5775,5777,4572,5626,5620,4885,5175,5424,4829,28,35,31,40,5458,4352])).
% 66.57/66.61 cnf(5812,plain,
% 66.57/66.61 (~P2(a12,f20(a12,a12))),
% 66.57/66.61 inference(scs_inference,[],[5739,5784,5782,5800,5620,1759,4512,11,282,9,31,33,40,34])).
% 66.57/66.61 cnf(5836,plain,
% 66.57/66.61 ($false),
% 66.57/66.61 inference(scs_inference,[],[5784,4347,5812,5626,4236,5,4,31,40]),
% 66.57/66.61 ['proof']).
% 66.57/66.61 % SZS output end Proof
% 66.57/66.61 % Total time :65.940000s
%------------------------------------------------------------------------------