%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : NUN082+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 : n009.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:42 EDT 2024
% Result : Theorem 95.91s 95.99s
% Output : CNFRefutation 96.03s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : NUN082+1 : TPTP v8.2.0. Released v7.3.0.
% 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n009.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:03:54 EDT 2024
% 0.12/0.33 % CPUTime :
% 0.19/0.56 start to proof:theBenchmark
% 95.91/95.98 %-------------------------------------------
% 95.91/95.98 % File :CSE---1.7
% 95.91/95.98 % Problem :theBenchmark
% 95.91/95.98 % Transform :cnf
% 95.91/95.98 % Format :tptp:raw
% 95.91/95.98 % Command :java -jar mcs_scs.jar %d %s
% 95.91/95.98
% 95.91/95.98 % Result :Theorem 95.380000s
% 95.91/95.98 % Output :CNFRefutation 95.380000s
% 95.91/95.98 %-------------------------------------------
% 95.91/95.99 %------------------------------------------------------------------------------
% 95.91/95.99 % File : NUN082+1 : TPTP v8.2.0. Released v7.3.0.
% 95.91/95.99 % Domain : Number Theory
% 95.91/95.99 % Problem : Robinson arithmetic: There exists X * 1 = 0
% 95.91/95.99 % Version : Especial.
% 95.91/95.99 % English :
% 95.91/95.99
% 95.91/95.99 % Refs : [BBJ03] Boolos et al. (2003), Computability and Logic
% 95.91/95.99 % : [Smi07] Smith (2007), An Introduction to Goedel's Theorems
% 95.91/95.99 % : [Lam18] Lampert (2018), Email to Geoff Sutcliffe
% 95.91/95.99 % Source : [Lam18]
% 95.91/95.99 % Names : xtimesoneidzero [Lam18]
% 95.91/95.99
% 95.91/95.99 % Status : Theorem
% 95.91/95.99 % Rating : 0.44 v8.2.0, 0.47 v8.1.0, 0.50 v7.5.0, 0.62 v7.3.0
% 95.91/95.99 % Syntax : Number of formulae : 19 ( 1 unt; 0 def)
% 95.91/95.99 % Number of atoms : 80 ( 0 equ)
% 95.91/95.99 % Maximal formula atoms : 7 ( 4 avg)
% 95.91/95.99 % Number of connectives : 95 ( 34 ~; 26 |; 35 &)
% 95.91/95.99 % ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% 95.91/95.99 % Maximal formula depth : 13 ( 8 avg)
% 95.91/95.99 % Maximal term depth : 1 ( 1 avg)
% 95.91/95.99 % Number of predicates : 5 ( 5 usr; 0 prp; 1-3 aty)
% 95.91/95.99 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 95.91/95.99 % Number of variables : 72 ( 47 !; 25 ?)
% 95.91/95.99 % SPC : FOF_THM_RFO_NEQ
% 95.91/95.99
% 95.91/95.99 % Comments : Translated to FOL without equality.
% 95.91/95.99 %------------------------------------------------------------------------------
% 95.91/95.99 include('Axioms/NUM009+0.ax').
% 95.91/95.99 %------------------------------------------------------------------------------
% 95.91/95.99 fof(xtimesoneidzero,conjecture,
% 95.91/95.99 ? [Y1,Y2] :
% 95.91/95.99 ( ? [Y3] :
% 95.91/95.99 ( r4(Y1,Y3,Y2)
% 95.91/95.99 & ? [Y4] :
% 95.91/95.99 ( r1(Y4)
% 95.91/95.99 & r2(Y4,Y3) ) )
% 95.91/95.99 & ? [Y5] :
% 95.91/95.99 ( id(Y2,Y5)
% 95.91/95.99 & r1(Y5) ) ) ).
% 95.91/95.99
% 95.91/95.99 %------------------------------------------------------------------------------
% 95.91/95.99 %-------------------------------------------
% 95.91/95.99 % Proof found
% 95.91/95.99 % SZS status Theorem for theBenchmark
% 95.91/95.99 % SZS output start Proof
% 95.91/96.00 %ClaNum:43(EqnAxiom:0)
% 95.91/96.00 %VarNum:210(SingletonVarNum:103)
% 95.91/96.00 %MaxLitNum:5
% 95.91/96.00 %MaxfuncDepth:1
% 95.91/96.00 %SharedTerms:1
% 95.91/96.00 %goalClause: 39
% 95.91/96.00 [4]P2(x41,x41)
% 95.91/96.00 [1]P1(f1(x11))
% 95.91/96.00 [2]P1(f6(x21))
% 95.91/96.00 [3]P1(f8(x31))
% 95.91/96.00 [5]P2(f2(x51),x51)
% 95.91/96.00 [6]P2(f7(x61),f8(x61))
% 95.91/96.00 [12]P4(x121,f1(x121),f2(x121))
% 95.91/96.00 [13]P5(x131,f6(x131),f7(x131))
% 95.91/96.00 [7]P3(x71,f9(x72,x71))
% 95.91/96.00 [8]P3(x81,f3(x82,x81))
% 95.91/96.00 [9]P2(f10(x91,x92),f11(x91,x92))
% 95.91/96.00 [10]P2(f4(x101,x102),f19(x101,x102))
% 95.91/96.00 [11]P3(f20(x111,x112),f11(x111,x112))
% 95.91/96.00 [14]P4(x141,x142,f20(x141,x142))
% 95.91/96.00 [15]P5(x151,x152,f5(x151,x152))
% 95.91/96.00 [16]P4(x161,f9(x161,x162),f10(x161,x162))
% 95.91/96.00 [17]P5(x171,f3(x171,x172),f4(x171,x172))
% 95.91/96.00 [18]P4(f5(x181,x182),x181,f19(x181,x182))
% 95.91/96.00 [19]~P1(x191)+P2(x191,a12)
% 95.91/96.00 [20]P1(x201)+~P2(x201,a12)
% 95.91/96.00 [21]P2(x211,f15(x211))+P1(f13(x211))
% 95.91/96.00 [25]P3(f14(x251),f15(x251))+P1(f13(x251))
% 95.91/96.00 [26]P2(x261,f15(x261))+P2(x261,f13(x261))
% 95.91/96.00 [29]P3(f14(x291),f15(x291))+P2(x291,f13(x291))
% 95.91/96.00 [24]~P2(x242,x241)+P2(x241,x242)
% 95.91/96.00 [27]~P3(x272,x271)+P2(x271,f16(x272))
% 95.91/96.00 [28]P3(x281,x282)+~P2(x282,f16(x281))
% 95.91/96.00 [35]P4(x351,x352,x353)+~P2(x353,f17(x351,x352))
% 95.91/96.00 [36]P5(x361,x362,x363)+~P2(x363,f18(x361,x362))
% 95.91/96.00 [37]~P4(x372,x373,x371)+P2(x371,f17(x372,x373))
% 95.91/96.00 [38]~P5(x382,x383,x381)+P2(x381,f18(x382,x383))
% 95.91/96.00 [22]~P2(x222,x221)+P1(x221)+~P1(x222)
% 95.91/96.00 [23]~P2(x231,x232)+P1(x231)+~P1(x232)
% 95.91/96.00 [30]~P1(x301)+~P2(x301,x302)+~P3(x303,x302)
% 95.91/96.00 [31]~P2(x311,x313)+P2(x311,x312)+~P2(x313,x312)
% 95.91/96.00 [32]~P3(x322,x324)+~P3(x321,x323)+P2(x321,x322)+~P2(x323,x324)
% 95.91/96.00 [33]~P3(x334,x333)+P3(x331,x332)+~P2(x333,x332)+~P2(x334,x331)
% 95.91/96.00 [34]~P3(x344,x343)+P3(x341,x342)+~P2(x342,x343)+~P2(x341,x344)
% 95.91/96.00 [39]~P1(x391)+~P2(x393,x391)+~P5(x395,x394,x393)+~P1(x392)+~P3(x392,x394)
% 95.91/96.00 [40]~P4(x406,x405,x404)+P4(x401,x402,x403)+~P2(x404,x403)+~P2(x405,x402)+~P2(x406,x401)
% 95.91/96.00 [41]~P4(x416,x415,x414)+P4(x411,x412,x413)+~P2(x413,x414)+~P2(x412,x415)+~P2(x411,x416)
% 95.91/96.00 [42]~P5(x426,x425,x424)+P5(x421,x422,x423)+~P2(x424,x423)+~P2(x425,x422)+~P2(x426,x421)
% 95.91/96.00 [43]~P5(x436,x435,x434)+P5(x431,x432,x433)+~P2(x433,x434)+~P2(x432,x435)+~P2(x431,x436)
% 95.91/96.00 %EqnAxiom
% 95.91/96.00
% 95.91/96.00 %-------------------------------------------
% 96.03/96.02 cnf(44,plain,
% 96.03/96.02 (P1(a12)),
% 96.03/96.02 inference(scs_inference,[],[4,20])).
% 96.03/96.02 cnf(45,plain,
% 96.03/96.02 (P2(x451,x451)),
% 96.03/96.02 inference(rename_variables,[],[4])).
% 96.03/96.02 cnf(47,plain,
% 96.03/96.02 (P3(x471,f16(x471))),
% 96.03/96.02 inference(scs_inference,[],[4,45,20,28])).
% 96.03/96.02 cnf(48,plain,
% 96.03/96.02 (P2(x481,x481)),
% 96.03/96.02 inference(rename_variables,[],[4])).
% 96.03/96.02 cnf(50,plain,
% 96.03/96.02 (P4(x501,x502,f17(x501,x502))),
% 96.03/96.02 inference(scs_inference,[],[4,45,48,20,28,35])).
% 96.03/96.02 cnf(51,plain,
% 96.03/96.02 (P2(x511,x511)),
% 96.03/96.02 inference(rename_variables,[],[4])).
% 96.03/96.02 cnf(53,plain,
% 96.03/96.02 (P5(x531,x532,f18(x531,x532))),
% 96.03/96.02 inference(scs_inference,[],[4,45,48,51,20,28,35,36])).
% 96.03/96.02 cnf(54,plain,
% 96.03/96.02 (P2(x541,x541)),
% 96.03/96.02 inference(rename_variables,[],[4])).
% 96.03/96.02 cnf(56,plain,
% 96.03/96.02 (~P3(x561,f1(x562))),
% 96.03/96.02 inference(scs_inference,[],[1,4,45,48,51,54,20,28,35,36,30])).
% 96.03/96.02 cnf(86,plain,
% 96.03/96.02 (P1(f2(a12))),
% 96.03/96.02 inference(scs_inference,[],[5,20])).
% 96.03/96.02 cnf(87,plain,
% 96.03/96.02 (P2(f2(x871),x871)),
% 96.03/96.02 inference(rename_variables,[],[5])).
% 96.03/96.02 cnf(89,plain,
% 96.03/96.02 (P4(x891,x892,f2(f17(x891,x892)))),
% 96.03/96.02 inference(scs_inference,[],[5,87,20,35])).
% 96.03/96.02 cnf(90,plain,
% 96.03/96.02 (P2(f2(x901),x901)),
% 96.03/96.02 inference(rename_variables,[],[5])).
% 96.03/96.02 cnf(93,plain,
% 96.03/96.02 (P2(f2(x931),x931)),
% 96.03/96.02 inference(rename_variables,[],[5])).
% 96.03/96.02 cnf(95,plain,
% 96.03/96.02 (P5(x951,x952,f2(f18(x951,x952)))),
% 96.03/96.02 inference(scs_inference,[],[5,87,90,93,20,35,28,36])).
% 96.03/96.02 cnf(98,plain,
% 96.03/96.02 (~P3(x981,a12)),
% 96.03/96.02 inference(scs_inference,[],[44,4,5,87,90,93,20,35,28,36,30])).
% 96.03/96.02 cnf(99,plain,
% 96.03/96.02 (P2(x991,x991)),
% 96.03/96.02 inference(rename_variables,[],[4])).
% 96.03/96.02 cnf(101,plain,
% 96.03/96.02 (P3(f8(x1011),f16(f7(x1011)))),
% 96.03/96.02 inference(scs_inference,[],[47,6,44,4,99,5,87,90,93,20,35,28,36,30,33])).
% 96.03/96.02 cnf(129,plain,
% 96.03/96.02 (~P3(x1291,f2(a12))),
% 96.03/96.02 inference(scs_inference,[],[86,4,30])).
% 96.03/96.02 cnf(154,plain,
% 96.03/96.02 (~P3(x1541,f6(x1542))),
% 96.03/96.02 inference(scs_inference,[],[2,4,30])).
% 96.03/96.02 cnf(186,plain,
% 96.03/96.02 (~P3(x1861,f8(x1862))),
% 96.03/96.02 inference(scs_inference,[],[3,4,30])).
% 96.03/96.02 cnf(205,plain,
% 96.03/96.02 (P2(f2(x2051),x2051)),
% 96.03/96.02 inference(rename_variables,[],[5])).
% 96.03/96.02 cnf(208,plain,
% 96.03/96.02 (P2(x2081,x2081)),
% 96.03/96.02 inference(rename_variables,[],[4])).
% 96.03/96.02 cnf(211,plain,
% 96.03/96.02 (P4(x2111,x2111,f17(f2(x2111),f2(x2111)))),
% 96.03/96.02 inference(scs_inference,[],[5,205,9,47,4,208,50,31,33,40])).
% 96.03/96.02 cnf(215,plain,
% 96.03/96.02 (~P5(x2151,x2151,x2151)+P5(f2(x2151),f2(x2151),f2(x2151))),
% 96.03/96.02 inference(scs_inference,[],[5,205,9,47,4,208,50,31,33,40,43])).
% 96.03/96.02 cnf(217,plain,
% 96.03/96.02 (~P4(x2171,x2171,x2171)+P4(f2(x2171),f2(x2171),f2(x2171))),
% 96.03/96.02 inference(scs_inference,[],[5,205,9,47,4,208,50,31,33,40,43,41])).
% 96.03/96.02 cnf(280,plain,
% 96.03/96.02 (P2(f6(x2801),a12)),
% 96.03/96.02 inference(scs_inference,[],[2,4,19,22])).
% 96.03/96.02 cnf(281,plain,
% 96.03/96.02 (P2(f2(f6(x2811)),a12)),
% 96.03/96.02 inference(scs_inference,[],[5,280,31])).
% 96.03/96.02 cnf(284,plain,
% 96.03/96.02 (P1(f2(f6(x2841)))),
% 96.03/96.02 inference(scs_inference,[],[5,280,31,20])).
% 96.03/96.02 cnf(286,plain,
% 96.03/96.02 (~P5(f6(x2861),f6(x2861),f6(x2861))+P5(a12,a12,a12)),
% 96.03/96.02 inference(scs_inference,[],[5,280,31,20,42])).
% 96.03/96.02 cnf(288,plain,
% 96.03/96.02 (~P4(a12,a12,a12)+P4(f6(x2881),f6(x2881),f6(x2881))),
% 96.03/96.02 inference(scs_inference,[],[5,280,31,20,42,41])).
% 96.03/96.02 cnf(293,plain,
% 96.03/96.02 (P1(f10(x2931,x2932))+~P1(f11(x2931,x2932))),
% 96.03/96.02 inference(scs_inference,[],[9,24,22])).
% 96.03/96.02 cnf(295,plain,
% 96.03/96.02 (P2(x2951,x2951)),
% 96.03/96.02 inference(rename_variables,[],[4])).
% 96.03/96.02 cnf(301,plain,
% 96.03/96.02 (~P5(a12,a12,a12)+P5(f6(x3011),f6(x3011),f6(x3011))),
% 96.03/96.02 inference(scs_inference,[],[2,4,295,3,101,280,284,30,39,43])).
% 96.03/96.02 cnf(307,plain,
% 96.03/96.02 (~P4(f6(x3071),f6(x3071),f6(x3071))+P4(a12,a12,a12)),
% 96.03/96.02 inference(scs_inference,[],[280,40])).
% 96.03/96.02 cnf(350,plain,
% 96.03/96.02 (P1(f10(x3501,x3502))+~P2(f11(x3501,x3502),a12)),
% 96.03/96.02 inference(scs_inference,[],[293,20])).
% 96.03/96.02 cnf(366,plain,
% 96.03/96.02 (~P2(f11(x3661,x3662),a12)),
% 96.03/96.02 inference(scs_inference,[],[9,11,350,30])).
% 96.03/96.02 cnf(369,plain,
% 96.03/96.02 (~P2(a12,f11(x3691,x3692))),
% 96.03/96.02 inference(scs_inference,[],[366,19,24])).
% 96.03/96.02 cnf(421,plain,
% 96.03/96.02 (~P3(f11(x4211,x4212),f16(a12))),
% 96.03/96.02 inference(scs_inference,[],[4,47,366,32])).
% 96.03/96.02 cnf(443,plain,
% 96.03/96.02 (P5(f6(x4431),f6(x4431),f6(x4431))+~P2(a12,f18(a12,a12))),
% 96.03/96.02 inference(scs_inference,[],[301,36])).
% 96.03/96.02 cnf(448,plain,
% 96.03/96.02 (P4(f2(a12),f2(a12),f2(a12))+~P4(f6(x4481),f6(x4481),f6(x4481))),
% 96.03/96.02 inference(scs_inference,[],[307,217])).
% 96.03/96.02 cnf(553,plain,
% 96.03/96.02 (~P5(x5531,f16(a12),f6(x5532))),
% 96.03/96.02 inference(scs_inference,[],[44,280,47,39])).
% 96.03/96.02 cnf(565,plain,
% 96.03/96.02 (~P5(x5651,f9(x5652,a12),f6(x5653))),
% 96.03/96.02 inference(scs_inference,[],[44,280,7,39])).
% 96.03/96.02 cnf(569,plain,
% 96.03/96.02 (~P5(x5691,f3(x5692,a12),f6(x5693))),
% 96.03/96.02 inference(scs_inference,[],[44,280,8,39])).
% 96.03/96.02 cnf(678,plain,
% 96.03/96.02 (~P2(f6(x6781),f11(x6782,x6783))),
% 96.03/96.02 inference(scs_inference,[],[280,366,31,24])).
% 96.03/96.02 cnf(971,plain,
% 96.03/96.02 (P3(f6(x9711),f16(a12))),
% 96.03/96.02 inference(scs_inference,[],[280,4,47,34])).
% 96.03/96.02 cnf(972,plain,
% 96.03/96.02 (P2(x9721,x9721)),
% 96.03/96.02 inference(rename_variables,[],[4])).
% 96.03/96.02 cnf(976,plain,
% 96.03/96.02 (P2(x9761,x9761)),
% 96.03/96.02 inference(rename_variables,[],[4])).
% 96.03/96.02 cnf(977,plain,
% 96.03/96.02 (P5(x9771,x9772,f2(f18(x9771,x9772)))),
% 96.03/96.02 inference(rename_variables,[],[95])).
% 96.03/96.02 cnf(980,plain,
% 96.03/96.02 (P2(x9801,x9801)),
% 96.03/96.02 inference(rename_variables,[],[4])).
% 96.03/96.02 cnf(984,plain,
% 96.03/96.02 (P2(f2(x9841),x9841)),
% 96.03/96.02 inference(rename_variables,[],[5])).
% 96.03/96.02 cnf(991,plain,
% 96.03/96.02 (~P5(x9911,f16(a12),f1(x9912))),
% 96.03/96.02 inference(scs_inference,[],[280,1,4,972,976,980,5,984,47,2,95,977,211,89,34,43,41,40,42,39])).
% 96.03/96.02 cnf(1018,plain,
% 96.03/96.02 (P3(f2(f6(x10181)),f16(a12))),
% 96.03/96.02 inference(scs_inference,[],[281,4,47,34])).
% 96.03/96.02 cnf(1038,plain,
% 96.03/96.02 (~P2(a12,f10(x10381,x10382))),
% 96.03/96.02 inference(scs_inference,[],[369,9,31])).
% 96.03/96.02 cnf(1163,plain,
% 96.03/96.02 (~P3(f10(x11631,x11632),f16(a12))),
% 96.03/96.02 inference(scs_inference,[],[421,9,4,33])).
% 96.03/96.02 cnf(1246,plain,
% 96.03/96.02 (~P2(f6(x12461),f10(x12462,x12463))),
% 96.03/96.02 inference(scs_inference,[],[678,9,31])).
% 96.03/96.02 cnf(1749,plain,
% 96.03/96.02 (~P5(x17491,f16(a12),f7(x17492))),
% 96.03/96.02 inference(scs_inference,[],[3,6,284,1018,39])).
% 96.03/96.02 cnf(1882,plain,
% 96.03/96.02 (~P5(x18821,f16(a12),f2(a12))),
% 96.03/96.02 inference(scs_inference,[],[86,4,284,1018,39])).
% 96.03/96.02 cnf(2518,plain,
% 96.03/96.02 (~P5(f8(x25181),f16(a12),f8(x25181))),
% 96.03/96.02 inference(scs_inference,[],[1749,6,4,43])).
% 96.03/96.02 cnf(2566,plain,
% 96.03/96.02 (~P5(a12,f9(x25661,a12),a12)),
% 96.03/96.02 inference(scs_inference,[],[565,280,4,43])).
% 96.03/96.02 cnf(2572,plain,
% 96.03/96.02 (~P5(a12,f3(x25721,a12),a12)),
% 96.03/96.02 inference(scs_inference,[],[569,280,4,43])).
% 96.03/96.02 cnf(2683,plain,
% 96.03/96.02 (~P2(f3(x26831,a12),x26832)+~P5(f6(x26833),x26832,f6(x26833))),
% 96.03/96.02 inference(scs_inference,[],[569,4,43])).
% 96.03/96.02 cnf(2874,plain,
% 96.03/96.02 (~P2(f16(a12),x28741)+~P5(f7(x28742),x28741,f7(x28742))),
% 96.03/96.02 inference(scs_inference,[],[1749,4,43])).
% 96.03/96.02 cnf(2919,plain,
% 96.03/96.02 (~P2(f16(a12),x29191)+~P5(f2(a12),x29191,f2(a12))),
% 96.03/96.02 inference(scs_inference,[],[1882,4,43])).
% 96.03/96.02 cnf(3511,plain,
% 96.03/96.02 (~P4(x35111,x35111,f2(x35112))+P4(x35111,x35111,x35112)),
% 96.03/96.02 inference(scs_inference,[],[4,5,40])).
% 96.03/96.02 cnf(3527,plain,
% 96.03/96.02 (~P4(x35271,x35271,f2(x35272))+P2(x35272,f17(x35271,x35271))),
% 96.03/96.02 inference(scs_inference,[],[3511,37])).
% 96.03/96.02 cnf(3529,plain,
% 96.03/96.02 (P4(f2(x35291),f2(x35291),f20(x35291,x35291))),
% 96.03/96.02 inference(scs_inference,[],[5,4,14,41])).
% 96.03/96.02 cnf(3531,plain,
% 96.03/96.02 (P2(f2(x35311),x35311)),
% 96.03/96.02 inference(rename_variables,[],[5])).
% 96.03/96.02 cnf(3532,plain,
% 96.03/96.02 (P2(f2(x35321),x35321)),
% 96.03/96.02 inference(rename_variables,[],[5])).
% 96.03/96.02 cnf(3535,plain,
% 96.03/96.02 (~P4(f2(x35351),f2(x35351),f2(x35352))+P4(x35351,x35351,x35352)),
% 96.03/96.02 inference(scs_inference,[],[5,3532,3531,4,14,41,40])).
% 96.03/96.02 cnf(3548,plain,
% 96.03/96.02 (P2(f9(x35481,x35482),f16(x35482))),
% 96.03/96.02 inference(scs_inference,[],[7,27])).
% 96.03/96.02 cnf(3550,plain,
% 96.03/96.02 (P2(f20(x35501,x35502),f17(x35501,x35502))),
% 96.03/96.02 inference(scs_inference,[],[14,7,27,37])).
% 96.03/96.02 cnf(3552,plain,
% 96.03/96.02 (P2(f5(x35521,x35522),f18(x35521,x35522))),
% 96.03/96.02 inference(scs_inference,[],[15,14,7,27,37,38])).
% 96.03/96.02 cnf(3554,plain,
% 96.03/96.02 (P2(f1(x35541),a12)),
% 96.03/96.02 inference(scs_inference,[],[1,15,14,7,27,37,38,19])).
% 96.03/96.02 cnf(3558,plain,
% 96.03/96.02 (P2(x35581,f2(x35581))),
% 96.03/96.02 inference(scs_inference,[],[1,98,15,14,7,5,27,37,38,19,28,24])).
% 96.03/96.02 cnf(3561,plain,
% 96.03/96.02 (P2(x35611,x35611)),
% 96.03/96.02 inference(rename_variables,[],[4])).
% 96.03/96.02 cnf(3564,plain,
% 96.03/96.02 (P3(x35641,f9(x35642,x35641))),
% 96.03/96.02 inference(rename_variables,[],[7])).
% 96.03/96.02 cnf(3565,plain,
% 96.03/96.02 (~P3(x35651,a12)),
% 96.03/96.02 inference(rename_variables,[],[98])).
% 96.03/96.02 cnf(3571,plain,
% 96.03/96.02 (P2(a12,f6(x35711))),
% 96.03/96.02 inference(scs_inference,[],[1,98,3565,971,15,14,7,3564,5,280,4,27,37,38,19,28,24,30,34,33,32])).
% 96.03/96.02 cnf(3572,plain,
% 96.03/96.02 (P3(x35721,f9(x35722,x35721))),
% 96.03/96.02 inference(rename_variables,[],[7])).
% 96.03/96.02 cnf(3574,plain,
% 96.03/96.02 (P4(x35741,f2(x35741),f17(x35741,x35741))),
% 96.03/96.02 inference(scs_inference,[],[1,98,3565,3529,971,15,14,7,3564,5,280,4,3561,27,37,38,19,28,24,30,34,33,32,40])).
% 96.03/96.02 cnf(3576,plain,
% 96.03/96.02 (P2(f2(x35761),x35761)),
% 96.03/96.02 inference(rename_variables,[],[5])).
% 96.03/96.02 cnf(3579,plain,
% 96.03/96.02 (~P5(x35791,f9(x35792,a12),f2(a12))),
% 96.03/96.02 inference(scs_inference,[],[1,98,3565,3529,971,15,14,7,3564,3572,44,5,3576,280,4,3561,27,37,38,19,28,24,30,34,33,32,40,39])).
% 96.03/96.02 cnf(3589,plain,
% 96.03/96.02 (P2(f8(x35891),a12)),
% 96.03/96.02 inference(scs_inference,[],[3,19])).
% 96.03/96.02 cnf(3591,plain,
% 96.03/96.02 (P2(f3(x35911,x35912),f16(x35912))),
% 96.03/96.02 inference(scs_inference,[],[8,3,19,27])).
% 96.03/96.02 cnf(3595,plain,
% 96.03/96.02 (P2(f17(x35951,x35952),f20(x35951,x35952))),
% 96.03/96.02 inference(scs_inference,[],[3550,154,8,3,19,27,28,24])).
% 96.03/96.02 cnf(3600,plain,
% 96.03/96.02 (P2(f1(x36001),f2(a12))),
% 96.03/96.02 inference(scs_inference,[],[3550,3558,3548,154,3554,971,8,3,19,27,28,24,30,31])).
% 96.03/96.02 cnf(3601,plain,
% 96.03/96.02 (P2(x36011,f2(x36011))),
% 96.03/96.02 inference(rename_variables,[],[3558])).
% 96.03/96.02 cnf(3603,plain,
% 96.03/96.02 (~P2(f16(a12),f6(x36031))),
% 96.03/96.02 inference(scs_inference,[],[3550,3558,3601,3548,154,3554,971,8,3,19,27,28,24,30,31,33])).
% 96.03/96.02 cnf(3604,plain,
% 96.03/96.02 (P2(x36041,f2(x36041))),
% 96.03/96.02 inference(rename_variables,[],[3558])).
% 96.03/96.02 cnf(3607,plain,
% 96.03/96.02 (P4(f2(x36071),x36071,f17(x36071,x36071))),
% 96.03/96.02 inference(scs_inference,[],[3574,3550,3558,3601,3604,3548,154,3554,971,8,3,5,4,19,27,28,24,30,31,33,40])).
% 96.03/96.02 cnf(3616,plain,
% 96.03/96.02 (P5(f1(x36161),f1(x36161),f5(a12,a12))),
% 96.03/96.02 inference(scs_inference,[],[3574,3550,3552,3558,3601,3604,3548,154,3554,53,971,8,3,5,4,19,27,28,24,30,31,33,40,20,23,43])).
% 96.03/96.02 cnf(3620,plain,
% 96.03/96.02 (P4(f1(x36201),f1(x36201),f20(a12,a12))),
% 96.03/96.02 inference(scs_inference,[],[3574,3550,3552,3558,3601,3604,3548,154,3554,53,50,971,8,3,5,4,19,27,28,24,30,31,33,40,20,23,43,41])).
% 96.03/96.02 cnf(3628,plain,
% 96.03/96.02 (~P2(f8(x36281),f16(x36282))),
% 96.03/96.02 inference(scs_inference,[],[186,28])).
% 96.03/96.02 cnf(3630,plain,
% 96.03/96.02 (P2(f16(x36301),f3(x36302,x36301))),
% 96.03/96.02 inference(scs_inference,[],[3591,186,28,24])).
% 96.03/96.02 cnf(3635,plain,
% 96.03/96.02 (P2(f1(x36351),f6(x36352))),
% 96.03/96.02 inference(scs_inference,[],[3591,186,3571,3554,971,28,24,30,31])).
% 96.03/96.02 cnf(3637,plain,
% 96.03/96.02 (~P2(f3(x36371,a12),f8(x36372))),
% 96.03/96.02 inference(scs_inference,[],[3591,186,3571,3554,971,8,28,24,30,31,33])).
% 96.03/96.02 cnf(3641,plain,
% 96.03/96.02 (P5(f8(x36411),f8(x36411),f5(a12,a12))),
% 96.03/96.02 inference(scs_inference,[],[3591,186,3571,3589,3552,3554,53,971,8,28,24,30,31,33,43])).
% 96.03/96.02 cnf(3643,plain,
% 96.03/96.02 (P2(f5(x36431,x36432),f18(x36431,x36432))),
% 96.03/96.02 inference(rename_variables,[],[3552])).
% 96.03/96.02 cnf(3649,plain,
% 96.03/96.02 (~P5(f2(a12),f3(x36491,a12),f2(a12))),
% 96.03/96.02 inference(scs_inference,[],[3607,3591,186,3600,3571,3589,3552,3550,3554,53,971,8,28,24,30,31,33,43,41,2919])).
% 96.03/96.02 cnf(3653,plain,
% 96.03/96.02 (P5(f2(a12),f2(a12),f18(a12,a12))),
% 96.03/96.02 inference(scs_inference,[],[3607,3591,186,3616,3600,3571,3589,3552,3643,3550,3554,53,971,8,28,24,30,31,33,43,41,2919,20,42])).
% 96.03/96.02 cnf(3660,plain,
% 96.03/96.02 (P2(f6(x36601),f1(x36602))),
% 96.03/96.02 inference(scs_inference,[],[3635,129,28,24])).
% 96.03/96.02 cnf(3665,plain,
% 96.03/96.02 (~P2(f16(a12),f8(x36651))),
% 96.03/96.02 inference(scs_inference,[],[3630,3635,3637,129,3591,8,28,24,30,31])).
% 96.03/96.02 cnf(3668,plain,
% 96.03/96.02 (~P2(f16(a12),f2(a12))),
% 96.03/96.02 inference(scs_inference,[],[3630,3635,3637,129,3558,3591,971,8,28,24,30,31,33])).
% 96.03/96.02 cnf(3682,plain,
% 96.03/96.02 (P2(f16(x36821),f9(x36822,x36821))),
% 96.03/96.02 inference(scs_inference,[],[56,3548,28,24])).
% 96.03/96.02 cnf(3692,plain,
% 96.03/96.02 (~P3(x36921,f1(x36922))),
% 96.03/96.02 inference(rename_variables,[],[56])).
% 96.03/96.02 cnf(3694,plain,
% 96.03/96.02 (~P2(f9(x36941,x36942),f1(x36943))),
% 96.03/96.02 inference(scs_inference,[],[3595,3668,56,3692,3548,3630,3558,7,11,4,28,24,30,31,34,33])).
% 96.03/96.02 cnf(3702,plain,
% 96.03/96.02 (P4(f6(x37021),f6(x37021),f17(a12,a12))),
% 96.03/96.02 inference(scs_inference,[],[3595,3660,3668,3620,56,3692,3548,3630,3552,3558,7,11,4,28,24,30,31,34,33,20,22,41])).
% 96.03/96.02 cnf(3706,plain,
% 96.03/96.02 (P2(f2(a12),f1(x37061))),
% 96.03/96.02 inference(scs_inference,[],[3600,24])).
% 96.03/96.02 cnf(3708,plain,
% 96.03/96.02 (~P2(f16(x37081),f1(x37082))),
% 96.03/96.02 inference(scs_inference,[],[3694,3600,3548,24,31])).
% 96.03/96.02 cnf(3720,plain,
% 96.03/96.02 (P2(a12,f8(x37201))),
% 96.03/96.02 inference(scs_inference,[],[3589,24])).
% 96.03/96.02 cnf(3732,plain,
% 96.03/96.02 (P2(f20(x37321,x37322),x37323)+~P2(f11(x37321,x37322),f3(x37324,x37323))),
% 96.03/96.02 inference(scs_inference,[],[3708,1163,3630,3589,3591,11,8,47,24,30,31,20,34,32])).
% 96.03/96.02 cnf(3734,plain,
% 96.03/96.02 (P2(f18(x37341,x37342),f5(x37341,x37342))),
% 96.03/96.02 inference(scs_inference,[],[3552,24])).
% 96.03/96.02 cnf(3739,plain,
% 96.03/96.02 (P5(f2(x37391),f1(x37392),f8(x37391))),
% 96.03/96.02 inference(scs_inference,[],[3603,13,3682,3660,3558,3552,6,24,31,42])).
% 96.03/96.02 cnf(3741,plain,
% 96.03/96.02 (P5(x37411,f6(x37411),f7(x37411))),
% 96.03/96.03 inference(rename_variables,[],[13])).
% 96.03/96.03 cnf(3744,plain,
% 96.03/96.03 (~P1(f5(x37441,x37442))+~P3(x37443,f18(x37441,x37442))),
% 96.03/96.03 inference(scs_inference,[],[3603,13,3682,3660,3558,3552,6,24,31,42,30])).
% 96.03/96.03 cnf(3746,plain,
% 96.03/96.03 (~P2(f6(x37461),f9(x37462,a12))),
% 96.03/96.03 inference(scs_inference,[],[3603,13,3682,3660,154,3558,3552,3554,7,6,24,31,42,30,34])).
% 96.03/96.03 cnf(3750,plain,
% 96.03/96.03 (P5(f2(x37501),f1(x37502),f7(x37501))),
% 96.03/96.03 inference(scs_inference,[],[3603,13,3741,3682,3635,3660,154,3558,3552,3554,7,5,6,4,24,31,42,30,34,43])).
% 96.03/96.03 cnf(3755,plain,
% 96.03/96.03 (~P1(f5(x37551,x37552))+~P2(f18(x37551,x37552),f16(x37553))),
% 96.03/96.03 inference(scs_inference,[],[3603,13,3741,3682,3635,3660,154,3558,3552,3554,7,5,6,4,24,31,42,30,34,43,28])).
% 96.03/96.03 cnf(3758,plain,
% 96.03/96.03 (P2(a12,f1(x37581))),
% 96.03/96.03 inference(scs_inference,[],[3554,24])).
% 96.03/96.03 cnf(3763,plain,
% 96.03/96.03 (P5(f1(x37631),f2(a12),a12)),
% 96.03/96.03 inference(scs_inference,[],[3739,3665,3720,3706,3682,3600,3554,24,31,43])).
% 96.03/96.03 cnf(3765,plain,
% 96.03/96.03 (P2(a12,f8(x37651))),
% 96.03/96.03 inference(rename_variables,[],[3720])).
% 96.03/96.03 cnf(3767,plain,
% 96.03/96.03 (~P1(f18(x37671,x37672))+P1(f5(x37671,x37672))),
% 96.03/96.03 inference(scs_inference,[],[3734,3739,3665,3720,3706,3682,3600,3554,24,31,43,22])).
% 96.03/96.03 cnf(3769,plain,
% 96.03/96.03 (P4(f1(x37691),f1(x37691),f17(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[3734,3739,3665,3720,3706,3529,3682,3600,3550,3554,24,31,43,22,40])).
% 96.03/96.03 cnf(3773,plain,
% 96.03/96.03 (P5(f6(x37731),f1(x37732),f8(x37733))),
% 96.03/96.03 inference(scs_inference,[],[3734,3739,3665,3720,3765,3706,3529,3682,3635,3600,3550,3554,24,31,43,22,40,42])).
% 96.03/96.03 cnf(3778,plain,
% 96.03/96.03 (P2(f8(x37781),f7(x37781))),
% 96.03/96.03 inference(scs_inference,[],[6,24])).
% 96.03/96.03 cnf(3783,plain,
% 96.03/96.03 (~P2(f4(a12,a12),f8(x37831))),
% 96.03/96.03 inference(scs_inference,[],[3746,17,2518,3720,3660,3591,6,24,31,42])).
% 96.03/96.03 cnf(3788,plain,
% 96.03/96.03 (P5(a12,a12,f8(x37881))),
% 96.03/96.03 inference(scs_inference,[],[3746,17,3758,3763,2518,3720,3660,3558,3589,3591,6,24,31,42,43])).
% 96.03/96.03 cnf(3792,plain,
% 96.03/96.03 (P4(f6(x37921),f6(x37921),f20(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[3769,3746,17,3758,3763,2518,3720,3660,3558,3589,3591,3550,6,24,31,42,43,41])).
% 96.03/96.03 cnf(3796,plain,
% 96.03/96.03 (P2(f8(x37961),f18(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[3769,3746,17,3758,3763,2518,3720,3660,3558,3589,3591,3550,6,24,31,42,43,41,38])).
% 96.03/96.03 cnf(3801,plain,
% 96.03/96.03 (P2(f7(x38011),a12)),
% 96.03/96.03 inference(scs_inference,[],[3769,3746,17,3758,3763,2518,3720,3660,3558,3589,3591,3550,3,6,24,31,42,43,41,38,23,19])).
% 96.03/96.03 cnf(3803,plain,
% 96.03/96.03 (P4(f8(x38031),f8(x38031),f20(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[3769,3746,17,3758,3763,2518,3720,3660,3595,3558,3589,3591,3550,50,3,6,24,31,42,43,41,38,23,19,40])).
% 96.03/96.03 cnf(3807,plain,
% 96.03/96.03 (P2(f18(a12,a12),f8(x38071))),
% 96.03/96.03 inference(scs_inference,[],[3796,24])).
% 96.03/96.03 cnf(3809,plain,
% 96.03/96.03 (~P2(f7(x38091),f16(x38092))),
% 96.03/96.03 inference(scs_inference,[],[3778,3628,3796,24,31])).
% 96.03/96.03 cnf(3810,plain,
% 96.03/96.03 (P2(f8(x38101),f7(x38101))),
% 96.03/96.03 inference(rename_variables,[],[3778])).
% 96.03/96.03 cnf(3812,plain,
% 96.03/96.03 (P5(f7(x38121),f7(x38121),a12)),
% 96.03/96.03 inference(scs_inference,[],[3778,3628,3796,3801,3788,3720,24,31,43])).
% 96.03/96.03 cnf(3817,plain,
% 96.03/96.03 (P2(a12,f1(x38171))),
% 96.03/96.03 inference(rename_variables,[],[3758])).
% 96.03/96.03 cnf(3824,plain,
% 96.03/96.03 (~P2(f3(x38241,a12),f7(x38242))),
% 96.03/96.03 inference(scs_inference,[],[1,3778,3810,3628,3796,12,3801,3788,3758,3817,3720,3558,8,24,31,43,41,39,33])).
% 96.03/96.03 cnf(3829,plain,
% 96.03/96.03 (P2(f8(x38291),f7(x38291))),
% 96.03/96.03 inference(rename_variables,[],[3778])).
% 96.03/96.03 cnf(3831,plain,
% 96.03/96.03 (~P3(x38311,f7(x38312))),
% 96.03/96.03 inference(scs_inference,[],[1,3778,3810,3829,3628,3796,12,3801,3788,3641,3758,3817,565,3720,3558,8,3,24,31,43,41,39,33,42,30])).
% 96.03/96.03 cnf(3834,plain,
% 96.03/96.03 (P2(a12,f7(x38341))),
% 96.03/96.03 inference(scs_inference,[],[3801,24])).
% 96.03/96.03 cnf(3836,plain,
% 96.03/96.03 (P1(f18(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[3807,3801,3,24,23])).
% 96.03/96.03 cnf(3844,plain,
% 96.03/96.03 (P3(x38441,f9(x38442,x38441))),
% 96.03/96.03 inference(rename_variables,[],[7])).
% 96.03/96.03 cnf(3845,plain,
% 96.03/96.03 (~P3(x38451,f7(x38452))),
% 96.03/96.03 inference(rename_variables,[],[3831])).
% 96.03/96.03 cnf(3847,plain,
% 96.03/96.03 (P5(f8(x38471),f1(x38472),a12)),
% 96.03/96.03 inference(scs_inference,[],[3831,3807,3824,13,3801,3758,3660,3591,7,3,24,23,31,33,42])).
% 96.03/96.03 cnf(3850,plain,
% 96.03/96.03 (P2(f7(x38501),a12)),
% 96.03/96.03 inference(rename_variables,[],[3801])).
% 96.03/96.03 cnf(3852,plain,
% 96.03/96.03 (P5(f1(x38521),a12,f8(a12))),
% 96.03/96.03 inference(scs_inference,[],[3750,3831,3807,3824,3778,13,3801,3758,3600,3660,3591,7,3,24,23,31,33,42,43])).
% 96.03/96.03 cnf(3854,plain,
% 96.03/96.03 (P2(f8(x38541),f7(x38541))),
% 96.03/96.03 inference(rename_variables,[],[3778])).
% 96.03/96.03 cnf(3856,plain,
% 96.03/96.03 (P1(f5(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[3750,3831,3807,3824,3778,13,3801,3758,3600,3660,3591,7,3,24,23,31,33,42,43,3767])).
% 96.03/96.03 cnf(3858,plain,
% 96.03/96.03 (P2(f18(a12,a12),a12)),
% 96.03/96.03 inference(scs_inference,[],[3750,3831,3807,3824,3778,13,3801,3758,3600,3660,3591,7,3,24,23,31,33,42,43,3767,19])).
% 96.03/96.03 cnf(3860,plain,
% 96.03/96.03 (P4(f7(x38601),f7(x38601),f17(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[3750,3831,3807,3803,3824,3778,3854,13,3801,3758,3600,3660,3591,3550,7,3,24,23,31,33,42,43,3767,19,40])).
% 96.03/96.03 cnf(3864,plain,
% 96.03/96.03 (~P3(x38641,f18(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[3750,3831,3807,3803,3824,3778,3854,13,3801,3758,3600,3660,3591,3550,7,3,24,23,31,33,42,43,3767,19,40,3744])).
% 96.03/96.03 cnf(3866,plain,
% 96.03/96.03 (~P2(f18(a12,a12),f16(x38661))),
% 96.03/96.03 inference(scs_inference,[],[3750,3831,3807,3803,3824,3778,3854,13,3801,3758,3600,3660,3591,3550,7,3,24,23,31,33,42,43,3767,19,40,3744,3755])).
% 96.03/96.03 cnf(3868,plain,
% 96.03/96.03 (~P2(f7(x38681),f9(x38682,a12))),
% 96.03/96.03 inference(scs_inference,[],[3750,3831,3845,3807,3803,3824,3778,3854,13,3801,3850,3758,3600,3660,3591,3550,7,3844,3,24,23,31,33,42,43,3767,19,40,3744,3755,34])).
% 96.03/96.03 cnf(3872,plain,
% 96.03/96.03 (P4(f18(a12,a12),f18(a12,a12),f17(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[3750,3831,3845,3807,3803,3824,3778,3854,13,3801,3850,3758,3600,3595,3660,3591,3550,7,3844,3,24,23,31,33,42,43,3767,19,40,3744,3755,34,41])).
% 96.03/96.03 cnf(3876,plain,
% 96.03/96.03 (P2(f5(a12,a12),a12)),
% 96.03/96.03 inference(scs_inference,[],[3856,19])).
% 96.03/96.03 cnf(3878,plain,
% 96.03/96.03 (P2(a12,f18(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[3856,3858,19,24])).
% 96.03/96.03 cnf(3883,plain,
% 96.03/96.03 (~P2(f18(a12,a12),f11(x38831,x38832))),
% 96.03/96.03 inference(scs_inference,[],[3856,3866,3864,3858,3734,3595,11,19,24,31,34])).
% 96.03/96.03 cnf(3885,plain,
% 96.03/96.03 (~P3(x38851,f18(a12,a12))),
% 96.03/96.03 inference(rename_variables,[],[3864])).
% 96.03/96.03 cnf(3891,plain,
% 96.03/96.03 (P5(a12,a12,f7(x38911))),
% 96.03/96.03 inference(scs_inference,[],[3856,3866,3864,3885,3812,3834,3858,3734,3801,3595,3558,971,11,19,24,31,34,33,42])).
% 96.03/96.03 cnf(3894,plain,
% 96.03/96.03 (P5(f18(a12,a12),f18(a12,a12),f18(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[3856,3866,3864,3885,3812,3834,3858,3788,3734,3801,3807,3595,3558,971,11,19,24,31,34,33,42,43])).
% 96.03/96.03 cnf(3897,plain,
% 96.03/96.03 (P2(f7(x38971),f18(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[3856,3866,3864,3885,3812,3834,3858,3788,3734,3801,3807,3595,3558,971,11,19,24,31,34,33,42,43,38])).
% 96.03/96.03 cnf(3903,plain,
% 96.03/96.03 (P5(f6(x39031),f6(x39031),f6(x39031))),
% 96.03/96.03 inference(scs_inference,[],[3878,443])).
% 96.03/96.03 cnf(3910,plain,
% 96.03/96.03 (P5(a12,a12,a12)),
% 96.03/96.03 inference(scs_inference,[],[3903,2683,286])).
% 96.03/96.03 cnf(3912,plain,
% 96.03/96.03 (P2(f18(a12,a12),f7(x39121))),
% 96.03/96.03 inference(scs_inference,[],[3903,3897,2683,286,24])).
% 96.03/96.03 cnf(3917,plain,
% 96.03/96.03 (P5(f18(a12,a12),f18(a12,a12),a12)),
% 96.03/96.03 inference(scs_inference,[],[3903,3897,3868,3876,3796,3641,2683,286,24,31,42])).
% 96.03/96.03 cnf(3922,plain,
% 96.03/96.03 (P5(f2(a12),f2(a12),f2(a12))),
% 96.03/96.03 inference(scs_inference,[],[3903,3897,3894,3868,3876,3878,2566,3796,3641,2683,286,24,31,42,43,215])).
% 96.03/96.03 cnf(3945,plain,
% 96.03/96.03 (P2(a12,f5(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[3876,24])).
% 96.03/96.03 cnf(3948,plain,
% 96.03/96.03 (P2(f18(x39481,x39482),f5(x39481,x39482))),
% 96.03/96.03 inference(rename_variables,[],[3734])).
% 96.03/96.03 cnf(3950,plain,
% 96.03/96.03 (~P2(f7(x39501),f9(x39502,x39503))),
% 96.03/96.03 inference(scs_inference,[],[3883,3831,3876,3734,7,5,24,31,34])).
% 96.03/96.03 cnf(3957,plain,
% 96.03/96.03 (~P2(f18(a12,a12),f3(x39571,a12))),
% 96.03/96.03 inference(scs_inference,[],[3912,3883,3872,3917,3831,3876,569,3571,3734,3595,7,5,24,31,34,40,42])).
% 96.03/96.03 cnf(3962,plain,
% 96.03/96.03 (~P3(x39621,f5(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[3910,3912,3883,3872,3917,3836,3831,3876,569,3571,3734,3948,3595,7,5,24,31,34,40,42,43,30])).
% 96.03/96.03 cnf(3965,plain,
% 96.03/96.03 (P4(f18(a12,a12),f18(a12,a12),f20(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[3910,3912,3883,3872,3860,3917,3836,3831,3876,569,3571,3734,3948,3595,3550,7,5,24,31,34,40,42,43,30,41])).
% 96.03/96.03 cnf(3969,plain,
% 96.03/96.03 (P2(f11(x39691,x39692),f10(x39691,x39692))),
% 96.03/96.03 inference(scs_inference,[],[9,24])).
% 96.03/96.03 cnf(3971,plain,
% 96.03/96.03 (~P2(f18(a12,a12),f9(x39711,x39712))),
% 96.03/96.03 inference(scs_inference,[],[3950,3897,9,24,31])).
% 96.03/96.03 cnf(3974,plain,
% 96.03/96.03 (~P2(f11(x39741,x39742),f5(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[3950,3962,3897,3558,11,9,24,31,33])).
% 96.03/96.03 cnf(3983,plain,
% 96.03/96.03 (P4(f8(x39831),f8(x39831),f17(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[3950,3962,3965,3922,3945,3891,3796,3897,3600,3558,3595,11,9,24,31,33,42,43,41])).
% 96.03/96.03 cnf(3989,plain,
% 96.03/96.03 (P2(f19(x39891,x39892),f4(x39891,x39892))),
% 96.03/96.03 inference(scs_inference,[],[10,24])).
% 96.03/96.03 cnf(3992,plain,
% 96.03/96.03 (P2(f11(x39921,x39922),f10(x39921,x39922))),
% 96.03/96.03 inference(rename_variables,[],[3969])).
% 96.03/96.03 cnf(4001,plain,
% 96.03/96.03 (P5(f8(x40011),f8(x40011),f18(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[3969,3773,3974,3962,3812,3778,3858,3635,3660,971,10,24,31,33,42,43])).
% 96.03/96.03 cnf(4004,plain,
% 96.03/96.03 (P2(f20(x40041,x40042),x40043)+~P3(x40043,f10(x40041,x40042))),
% 96.03/96.03 inference(scs_inference,[],[3969,3992,3773,3974,3962,3812,3778,3858,3635,3660,971,11,10,24,31,33,42,43,32])).
% 96.03/96.03 cnf(4026,plain,
% 96.03/96.03 (P5(f7(x40261),f7(x40261),f18(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[3957,3945,3891,3962,3834,3912,3897,8,31,33,42])).
% 96.03/96.03 cnf(4033,plain,
% 96.03/96.03 (~P2(f5(a12,a12),f9(x40331,x40332))),
% 96.03/96.03 inference(scs_inference,[],[3971,3734,31])).
% 96.03/96.03 cnf(4036,plain,
% 96.03/96.03 (~P2(f4(a12,a12),f2(a12))),
% 96.03/96.03 inference(scs_inference,[],[3971,3649,17,3734,3558,4,31,42])).
% 96.03/96.03 cnf(4052,plain,
% 96.03/96.03 (~P2(a12,f9(x40521,x40522))),
% 96.03/96.03 inference(scs_inference,[],[4033,3876,31])).
% 96.03/96.03 cnf(4059,plain,
% 96.03/96.03 (P5(f18(a12,a12),f18(a12,a12),f8(x40591))),
% 96.03/96.03 inference(scs_inference,[],[4001,4033,3969,13,3876,3796,3807,3801,3660,31,42,43])).
% 96.03/96.03 cnf(4070,plain,
% 96.03/96.03 (~P2(f18(a12,a12),f3(x40701,x40702))),
% 96.03/96.03 inference(scs_inference,[],[3971,3864,3807,8,5,31,34])).
% 96.03/96.03 cnf(4078,plain,
% 96.03/96.03 (P5(f7(x40781),f6(x40782),f5(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[18,3847,3971,3864,3945,3989,3876,3778,3635,3807,8,5,31,34,40,42])).
% 96.03/96.03 cnf(4081,plain,
% 96.03/96.03 (P5(f8(x40811),f8(x40811),a12)),
% 96.03/96.03 inference(scs_inference,[],[18,4026,3847,3971,3864,3945,3989,3876,3878,3778,3635,3807,8,5,31,34,40,42,43])).
% 96.03/96.03 cnf(4084,plain,
% 96.03/96.03 (P4(f5(a12,a12),f5(a12,a12),f17(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[18,4026,3847,3971,3864,3945,3989,3876,3878,3778,3635,14,3807,3595,8,5,31,34,40,42,43,41])).
% 96.03/96.03 cnf(4088,plain,
% 96.03/96.03 (~P2(a12,f3(x40881,x40882))),
% 96.03/96.03 inference(scs_inference,[],[4070,3858,31])).
% 96.03/96.03 cnf(4090,plain,
% 96.03/96.03 (P5(f1(x40901),f1(x40901),a12)),
% 96.03/96.03 inference(scs_inference,[],[4070,3653,3858,3706,31,42])).
% 96.03/96.03 cnf(4092,plain,
% 96.03/96.03 (P4(f18(a12,a12),f16(x40921),f11(a12,x40921))),
% 96.03/96.03 inference(scs_inference,[],[4070,16,3653,3969,3682,3858,3706,31,42,41])).
% 96.03/96.03 cnf(4097,plain,
% 96.03/96.03 (~P2(f7(x40971),f3(x40972,x40973))),
% 96.03/96.03 inference(scs_inference,[],[4070,3912,31])).
% 96.03/96.03 cnf(4105,plain,
% 96.03/96.03 (~P2(f9(x41051,x41052),f7(x41053))),
% 96.03/96.03 inference(scs_inference,[],[4081,4070,2572,3831,3912,3589,3558,3550,7,4,31,42,30,33])).
% 96.03/96.03 cnf(4109,plain,
% 96.03/96.03 (P4(f7(x41091),f3(x41092,x41093),f10(a12,x41093))),
% 96.03/96.03 inference(scs_inference,[],[4092,4081,4070,2572,3831,3969,3630,3912,3589,3558,3550,7,4,31,42,30,33,40])).
% 96.03/96.03 cnf(4117,plain,
% 96.03/96.03 (~P2(f16(x41171),f7(x41172))),
% 96.03/96.03 inference(scs_inference,[],[4105,3548,31])).
% 96.03/96.03 cnf(4120,plain,
% 96.03/96.03 (P5(f18(a12,a12),f1(x41201),f18(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4105,4078,3548,3897,3552,3660,31,42])).
% 96.03/96.03 cnf(4125,plain,
% 96.03/96.03 (P4(a12,f16(x41251),f11(a12,x41251))),
% 96.03/96.03 inference(scs_inference,[],[4105,4109,4078,3834,3548,3969,3630,3897,3552,3660,31,42,41])).
% 96.03/96.03 cnf(4133,plain,
% 96.03/96.03 (P5(f5(a12,a12),a12,f5(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4117,4120,3630,3734,3554,31,42])).
% 96.03/96.03 cnf(4145,plain,
% 96.03/96.03 (~P2(f1(x41451),f9(x41452,x41453))),
% 96.03/96.03 inference(scs_inference,[],[4052,3758,31])).
% 96.03/96.03 cnf(4147,plain,
% 96.03/96.03 (P5(f6(x41471),f6(x41471),f1(x41472))),
% 96.03/96.03 inference(scs_inference,[],[4052,4090,3758,3635,31,42])).
% 96.03/96.03 cnf(4150,plain,
% 96.03/96.03 (P5(f2(a12),f2(a12),f7(x41501))),
% 96.03/96.03 inference(scs_inference,[],[4052,4090,3758,3801,3706,3635,31,42,43])).
% 96.03/96.03 cnf(4153,plain,
% 96.03/96.03 (P4(f5(a12,x41531),f1(x41532),f4(a12,x41531))),
% 96.03/96.03 inference(scs_inference,[],[4052,4090,18,3758,3801,3706,3635,3989,4,31,42,43,40])).
% 96.03/96.03 cnf(4161,plain,
% 96.03/96.03 (P5(a12,a12,f2(a12))),
% 96.03/96.03 inference(scs_inference,[],[4147,4145,3571,3706,3635,31,43])).
% 96.03/96.03 cnf(4165,plain,
% 96.03/96.03 (P2(f2(a12),f18(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4147,4145,3571,3706,3635,31,43,38])).
% 96.03/96.03 cnf(4167,plain,
% 96.03/96.03 (P2(f18(a12,a12),f2(a12))),
% 96.03/96.03 inference(scs_inference,[],[4147,4145,3571,3706,3635,31,43,38,24])).
% 96.03/96.03 cnf(4182,plain,
% 96.03/96.03 (P5(a12,f5(a12,a12),a12)),
% 96.03/96.03 inference(scs_inference,[],[4133,4088,3945,3876,31,42])).
% 96.03/96.03 cnf(4189,plain,
% 96.03/96.03 (P4(f2(a12),f2(a12),f17(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4165,4133,4088,3965,3763,3579,3945,3876,3758,3595,5,31,42,43,41])).
% 96.03/96.03 cnf(4192,plain,
% 96.03/96.03 (~P2(f19(a12,a12),f8(x41921))),
% 96.03/96.03 inference(scs_inference,[],[3783,10,31])).
% 96.03/96.03 cnf(4195,plain,
% 96.03/96.03 (~P2(f9(x41951,x41952),f8(x41953))),
% 96.03/96.03 inference(scs_inference,[],[3783,186,3558,7,10,31,33])).
% 96.03/96.03 cnf(4204,plain,
% 96.03/96.03 (P5(f8(x42041),f18(a12,a12),f8(x42041))),
% 96.03/96.03 inference(scs_inference,[],[3783,4125,4182,186,3682,3969,3720,3552,3558,7,10,31,33,40,42])).
% 96.03/96.03 cnf(4207,plain,
% 96.03/96.03 (P4(f18(a12,a12),f8(x42071),f20(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4167,3783,4125,4182,3607,186,3682,3969,3720,3589,3552,3550,3558,7,10,31,33,40,42,41])).
% 96.03/96.03 cnf(4221,plain,
% 96.03/96.03 (P4(f2(a12),f18(a12,a12),f17(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4195,4207,4165,3616,129,3548,3801,3876,3635,3807,3595,8,31,34,42,41])).
% 96.03/96.03 cnf(4236,plain,
% 96.03/96.03 (P5(f2(a12),f2(a12),a12)),
% 96.03/96.03 inference(scs_inference,[],[4059,4167,4070,4165,3720,31,43])).
% 96.03/96.03 cnf(4239,plain,
% 96.03/96.03 (~P2(f19(a12,a12),f2(a12))),
% 96.03/96.03 inference(scs_inference,[],[4036,10,31])).
% 96.03/96.03 cnf(4244,plain,
% 96.03/96.03 (P4(f18(a12,a12),a12,f20(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4189,3971,4167,3550,3558,31,41])).
% 96.03/96.03 cnf(4248,plain,
% 96.03/96.03 (P5(f1(x42481),f1(x42481),f18(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4189,4236,3971,4167,3878,3706,3550,3558,31,41,42])).
% 96.03/96.03 cnf(4250,plain,
% 96.03/96.03 (P4(f2(a12),f18(a12,a12),f20(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[3574,4165,3558,3595,40])).
% 96.03/96.03 cnf(4253,plain,
% 96.03/96.03 (P2(f17(x42531,x42532),f20(x42531,x42532))),
% 96.03/96.03 inference(rename_variables,[],[3595])).
% 96.03/96.03 cnf(4255,plain,
% 96.03/96.03 (P5(f18(a12,a12),f2(a12),f18(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4204,3574,4165,4167,3796,3558,3595,40,42])).
% 96.03/96.03 cnf(4258,plain,
% 96.03/96.03 (P4(f2(a12),f8(x42581),f17(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4244,4204,3574,4165,4167,3796,3589,3558,3595,4253,40,42,41])).
% 96.03/96.03 cnf(4264,plain,
% 96.03/96.03 (P4(f2(a12),f7(x42641),f17(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4244,1246,4167,3834,3660,3550,31,40])).
% 96.03/96.03 cnf(4265,plain,
% 96.03/96.03 (P2(f20(x42651,x42652),f17(x42651,x42652))),
% 96.03/96.03 inference(rename_variables,[],[3550])).
% 96.03/96.03 cnf(4267,plain,
% 96.03/96.03 (P4(f18(a12,a12),f2(a12),f20(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4221,4244,1246,4165,4167,3834,3660,3550,4265,31,40,41])).
% 96.03/96.03 cnf(4273,plain,
% 96.03/96.03 (P4(f6(x42731),a12,f17(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[3792,3571,3595,4,41])).
% 96.03/96.03 cnf(4282,plain,
% 96.03/96.03 (~P2(f18(a12,a12),f10(x42821,x42822))),
% 96.03/96.03 inference(scs_inference,[],[4221,1038,3878,3897,4167,3550,41,31])).
% 96.03/96.03 cnf(4288,plain,
% 96.03/96.03 (P4(f18(a12,a12),f9(x42881,x42882),f10(a12,x42882))),
% 96.03/96.03 inference(scs_inference,[],[4282,4092,3682,3969,3734,4,31,40])).
% 96.03/96.03 cnf(4294,plain,
% 96.03/96.03 (P4(a12,a12,f19(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4282,4153,4092,3682,3969,3945,3989,3734,3758,4,31,40,41])).
% 96.03/96.03 cnf(4299,plain,
% 96.03/96.03 (P2(f19(a12,a12),f17(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4294,37])).
% 96.03/96.03 cnf(4301,plain,
% 96.03/96.03 (P2(f17(a12,a12),f19(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4294,37,24])).
% 96.03/96.03 cnf(4305,plain,
% 96.03/96.03 (P4(f7(x43051),f7(x43051),f4(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4239,4294,3834,3989,37,24,31,40])).
% 96.03/96.03 cnf(4317,plain,
% 96.03/96.03 (P4(f18(a12,a12),f18(a12,a12),f19(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4084,4299,4301,4192,3552,31,40])).
% 96.03/96.03 cnf(4325,plain,
% 96.03/96.03 (P5(f1(x43251),f1(x43251),f8(x43252))),
% 96.03/96.03 inference(scs_inference,[],[3809,4084,4299,4301,4192,4150,3917,3778,3571,3912,3552,3600,31,40,42,32,43])).
% 96.03/96.03 cnf(4328,plain,
% 96.03/96.03 (P2(f20(a12,a12),f19(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4301,3550,31])).
% 96.03/96.03 cnf(4331,plain,
% 96.03/96.03 (P5(f18(a12,a12),a12,f18(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4301,4204,3878,3807,3550,31,43])).
% 96.03/96.03 cnf(4334,plain,
% 96.03/96.03 (P2(f19(a12,a12),f20(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4301,4204,3878,3807,3550,31,43,24])).
% 96.03/96.03 cnf(4342,plain,
% 96.03/96.03 (~P3(f2(a12),f10(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4305,4334,4239,3778,3989,31,41,4004])).
% 96.03/96.03 cnf(4347,plain,
% 96.03/96.03 (~P2(f20(a12,a12),f8(x43471))),
% 96.03/96.03 inference(scs_inference,[],[4192,4334,31])).
% 96.03/96.03 cnf(4353,plain,
% 96.03/96.03 (P4(f20(a12,a12),f2(a12),f19(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4328,4342,4192,12,4334,3706,3558,8,5,31,34,41])).
% 96.03/96.03 cnf(4368,plain,
% 96.03/96.03 (P4(f6(x43681),f6(x43681),f19(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[3769,4301,3635,40])).
% 96.03/96.03 cnf(4371,plain,
% 96.03/96.03 (P5(f18(a12,a12),f18(a12,a12),f7(x43711))),
% 96.03/96.03 inference(scs_inference,[],[3769,4236,4301,4165,3834,3635,40,42])).
% 96.03/96.03 cnf(4373,plain,
% 96.03/96.03 (P5(f2(a12),f18(a12,a12),f2(a12))),
% 96.03/96.03 inference(scs_inference,[],[4331,3769,4236,4301,4165,3834,3858,3635,40,42,43])).
% 96.03/96.03 cnf(4389,plain,
% 96.03/96.03 (~P2(f3(x43891,a12),f10(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4097,4342,3558,8,6,31,33])).
% 96.03/96.03 cnf(4393,plain,
% 96.03/96.03 (P5(f1(x43931),f7(x43932),f1(x43931))),
% 96.03/96.03 inference(scs_inference,[],[4373,4097,4342,3912,3706,3558,8,6,31,33,42])).
% 96.03/96.03 cnf(4403,plain,
% 96.03/96.03 (~P2(f16(a12),f10(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4389,3591,31])).
% 96.03/96.03 cnf(4407,plain,
% 96.03/96.03 (P4(a12,f18(a12,a12),f19(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4267,4389,4328,3591,3858,4165,31,40])).
% 96.03/96.03 cnf(4409,plain,
% 96.03/96.03 (~P3(f8(x44091),f10(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4267,4389,4347,4328,3591,3858,4165,31,40,4004])).
% 96.03/96.03 cnf(4420,plain,
% 96.03/96.03 (~P2(f8(x44201),f20(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4409,4403,3682,11,9,31,34])).
% 96.03/96.03 cnf(4426,plain,
% 96.03/96.03 (P5(f5(a12,a12),f5(a12,a12),f1(x44261))),
% 96.03/96.03 inference(scs_inference,[],[4409,4403,4161,4301,3682,3945,3706,11,9,31,34,22,42])).
% 96.03/96.03 cnf(4435,plain,
% 96.03/96.03 (~P2(f18(a12,a12),f20(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4420,3796,31])).
% 96.03/96.03 cnf(4438,plain,
% 96.03/96.03 (~P2(f1(x44381),f3(x44382,a12))),
% 96.03/96.03 inference(scs_inference,[],[4420,4325,2572,3796,3554,3589,31,42])).
% 96.03/96.03 cnf(4439,plain,
% 96.03/96.03 (P2(f1(x44391),a12)),
% 96.03/96.03 inference(rename_variables,[],[3554])).
% 96.03/96.03 cnf(4442,plain,
% 96.03/96.03 (P4(a12,f1(x44421),f19(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4420,4273,4325,2572,4299,3796,3554,4439,3589,3571,31,42,41])).
% 96.03/96.03 cnf(4447,plain,
% 96.03/96.03 (~P2(f3(x44471,x44472),f5(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4420,4273,4325,2572,3962,4334,4299,3796,3554,4439,3589,3571,3558,8,31,42,41,30,33])).
% 96.03/96.03 cnf(4451,plain,
% 96.03/96.03 (~P2(f7(x44511),f4(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4420,4273,4325,17,2572,1749,3962,4334,4299,3630,3796,3554,4439,3589,3571,3558,8,31,42,41,30,33,43])).
% 96.03/96.03 cnf(4459,plain,
% 96.03/96.03 (~P2(f16(x44591),f5(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4447,3591,31])).
% 96.03/96.03 cnf(4468,plain,
% 96.03/96.03 (~P2(a12,f4(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4451,3801,31])).
% 96.03/96.03 cnf(4471,plain,
% 96.03/96.03 (P4(f7(x44711),f7(x44711),f19(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4451,3983,4301,3801,3778,31,40])).
% 96.03/96.03 cnf(4474,plain,
% 96.03/96.03 (~P2(f18(a12,a12),f4(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4468,3878,31])).
% 96.03/96.03 cnf(4476,plain,
% 96.03/96.03 (P5(a12,f18(a12,a12),a12)),
% 96.03/96.03 inference(scs_inference,[],[4468,4393,3878,3912,3758,31,43])).
% 96.03/96.03 cnf(4482,plain,
% 96.03/96.03 (P4(f1(x44821),f18(a12,a12),f19(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4468,4393,4273,4334,4301,3878,3912,3758,3660,31,43,22,40])).
% 96.03/96.03 cnf(4508,plain,
% 96.03/96.03 (P5(f5(a12,a12),f5(a12,a12),a12)),
% 96.03/96.03 inference(scs_inference,[],[4459,4371,3682,3734,3801,31,42])).
% 96.03/96.03 cnf(4512,plain,
% 96.03/96.03 (P4(f19(a12,a12),f18(a12,a12),f17(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4459,4353,4371,4301,4334,3682,4167,3734,3801,31,42,41])).
% 96.03/96.03 cnf(4516,plain,
% 96.03/96.03 (~P2(f3(x45161,x45162),f18(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4459,4353,4371,4409,3864,4301,4334,3682,4167,3734,3801,3558,8,971,31,42,41,34,33])).
% 96.03/96.03 cnf(4520,plain,
% 96.03/96.03 (~P2(f16(x45201),f18(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4516,3591,31])).
% 96.03/96.03 cnf(4523,plain,
% 96.03/96.03 (P5(f18(a12,a12),f18(a12,a12),f5(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4516,4508,3591,3552,3945,31,42])).
% 96.03/96.03 cnf(4529,plain,
% 96.03/96.03 (~P2(a12,f20(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4435,3858,31])).
% 96.03/96.03 cnf(4531,plain,
% 96.03/96.03 (~P2(f6(x45311),f20(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4529,3571,31])).
% 96.03/96.03 cnf(4533,plain,
% 96.03/96.03 (~P3(a12,f10(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4529,3571,11,9,31,32])).
% 96.03/96.03 cnf(4544,plain,
% 96.03/96.03 (~P2(f9(x45441,x45442),f18(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4520,3682,31])).
% 96.03/96.03 cnf(4547,plain,
% 96.03/96.03 (~P2(f20(a12,a12),a12)),
% 96.03/96.03 inference(scs_inference,[],[4520,4533,3969,3682,11,31,33])).
% 96.03/96.03 cnf(4551,plain,
% 96.03/96.03 (P4(f8(x45511),a12,f17(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4520,4442,4533,4299,3969,3554,3682,3720,11,31,33,40])).
% 96.03/96.03 cnf(4558,plain,
% 96.03/96.03 (~P2(f1(x45581),f20(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4531,4547,3660,3732,31])).
% 96.03/96.03 cnf(4561,plain,
% 96.03/96.03 (P4(f17(a12,a12),f7(x45611),f19(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4531,4512,4547,4299,4301,3912,3660,3732,31,40])).
% 96.03/96.03 cnf(4563,plain,
% 96.03/96.03 (~P2(f2(a12),f4(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4474,4167,31])).
% 96.03/96.03 cnf(4575,plain,
% 96.03/96.03 (P4(f18(a12,a12),f5(a12,a12),f19(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4551,4248,4547,3876,4328,4299,3796,3807,3660,31,43,41])).
% 96.03/96.03 cnf(4591,plain,
% 96.03/96.03 (P5(a12,f1(x45911),a12)),
% 96.03/96.03 inference(scs_inference,[],[4558,3852,3554,3720,3600,3758,31,43])).
% 96.03/96.03 cnf(4595,plain,
% 96.03/96.03 (P4(f19(a12,a12),f8(x45951),f20(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4558,4561,3852,4328,3554,3778,4299,3720,3600,3758,31,43,41])).
% 96.03/96.03 cnf(4601,plain,
% 96.03/96.03 (P5(a12,a12,f6(x46011))),
% 96.03/96.03 inference(scs_inference,[],[4438,4426,3876,3635,31,42])).
% 96.03/96.03 cnf(4604,plain,
% 96.03/96.03 (P2(f6(x46041),f18(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4601,38])).
% 96.03/96.03 cnf(4606,plain,
% 96.03/96.03 (P2(f18(a12,a12),f6(x46061))),
% 96.03/96.03 inference(scs_inference,[],[4601,38,24])).
% 96.03/96.03 cnf(4615,plain,
% 96.03/96.03 (P5(f18(a12,a12),f18(a12,a12),f1(x46151))),
% 96.03/96.03 inference(scs_inference,[],[4563,4601,4092,3630,3969,3878,3858,3706,3660,38,24,31,40,42])).
% 96.03/96.03 cnf(4622,plain,
% 96.03/96.03 (P4(f4(a12,a12),a12,f19(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4595,4468,3589,3571,3989,4328,31,40])).
% 96.03/96.03 cnf(4626,plain,
% 96.03/96.03 (P4(a12,f6(x46261),f19(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4604,4595,4468,4250,3589,3571,3989,4334,4328,3558,31,40,41])).
% 96.03/96.03 cnf(4629,plain,
% 96.03/96.03 (P4(f6(x46291),f6(x46291),f4(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4606,4317,3989,40])).
% 96.03/96.03 cnf(4637,plain,
% 96.03/96.03 (P4(a12,f6(x46371),f17(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4482,4604,4301,3758,41])).
% 96.03/96.03 cnf(4640,plain,
% 96.03/96.03 (P4(f6(x46401),f18(a12,a12),f17(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4575,4604,3734,4301,41])).
% 96.03/96.03 cnf(4643,plain,
% 96.03/96.03 (P4(f18(a12,a12),f6(x46431),f19(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4640,4606,4604,4301,40])).
% 96.03/96.03 cnf(4647,plain,
% 96.03/96.03 (P4(f6(x46471),f18(a12,a12),f20(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4643,4606,4604,4334,40])).
% 96.03/96.03 cnf(4650,plain,
% 96.03/96.03 (~P2(f6(x46501),f3(x46502,x46503))),
% 96.03/96.03 inference(scs_inference,[],[4643,4606,4070,4604,4334,40,31])).
% 96.03/96.03 cnf(4658,plain,
% 96.03/96.03 (P5(f6(x46581),a12,f6(x46581))),
% 96.03/96.03 inference(scs_inference,[],[4544,4629,4643,4255,4606,4070,4604,3552,4334,3989,3635,5,40,31,41,32,42])).
% 96.03/96.03 cnf(4664,plain,
% 96.03/96.03 (P4(a12,f18(a12,a12),f17(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4650,4626,4604,4299,3660,4,31,40])).
% 96.03/96.03 cnf(4671,plain,
% 96.03/96.03 (P4(f5(a12,a12),f18(a12,a12),f19(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4637,4606,3876,4299,41])).
% 96.03/96.03 cnf(4674,plain,
% 96.03/96.03 (P4(f18(a12,a12),f6(x46741),f20(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4671,4604,3734,4328,41])).
% 96.03/96.03 cnf(4677,plain,
% 96.03/96.03 (P4(f6(x46771),f18(a12,a12),f19(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4674,4606,4604,4328,40])).
% 96.03/96.03 cnf(4680,plain,
% 96.03/96.03 (P4(f20(a12,a12),f18(a12,a12),f19(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4595,3796,4334,4328,40])).
% 96.03/96.03 cnf(4683,plain,
% 96.03/96.03 (P5(f18(a12,a12),f7(x46831),f18(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4658,4595,4606,3801,3796,4334,4328,40,43])).
% 96.03/96.03 cnf(4686,plain,
% 96.03/96.03 (P4(f18(a12,a12),f18(a12,a12),f4(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4368,4604,3989,40])).
% 96.03/96.03 cnf(4692,plain,
% 96.03/96.03 (P4(f5(a12,a12),f5(a12,a12),f19(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4686,3552,3989,41])).
% 96.03/96.03 cnf(4696,plain,
% 96.03/96.03 (P4(f18(a12,a12),f7(x46961),f19(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4647,4606,3897,4334,41])).
% 96.03/96.03 cnf(4700,plain,
% 96.03/96.03 (P4(f19(a12,a12),f6(x47001),f17(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4680,4606,4299,4328,40])).
% 96.03/96.03 cnf(4702,plain,
% 96.03/96.03 (P4(f18(a12,a12),f6(x47021),f17(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4680,4677,4604,4606,4301,4299,4328,40,41])).
% 96.03/96.03 cnf(4705,plain,
% 96.03/96.03 (P5(f6(x47051),f18(a12,a12),f6(x47051))),
% 96.03/96.03 inference(scs_inference,[],[4680,4677,4683,4604,4606,3897,4301,4299,4328,40,41,42])).
% 96.03/96.03 cnf(4709,plain,
% 96.03/96.03 (P4(f7(x47091),a12,f20(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4696,3912,3801,4334,40])).
% 96.03/96.03 cnf(4724,plain,
% 96.03/96.03 (P5(a12,f6(x47241),a12)),
% 96.03/96.03 inference(scs_inference,[],[4705,4604,3571,43])).
% 96.03/96.03 cnf(4727,plain,
% 96.03/96.03 (P4(f17(a12,a12),a12,f19(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4705,4700,4604,3571,4301,4299,43,41])).
% 96.03/96.03 cnf(4731,plain,
% 96.03/96.03 (P4(a12,a12,f4(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4692,3876,3989,40])).
% 96.03/96.03 cnf(4734,plain,
% 96.03/96.03 (P2(f4(a12,a12),f17(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4692,3876,3989,40,37])).
% 96.03/96.03 cnf(4736,plain,
% 96.03/96.03 (P2(f17(a12,a12),f4(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4692,3876,3989,40,37,24])).
% 96.03/96.03 cnf(4739,plain,
% 96.03/96.03 (P4(f1(x47391),f1(x47391),f4(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4734,3702,3635,41])).
% 96.03/96.03 cnf(4747,plain,
% 96.03/96.03 (P4(a12,f18(a12,a12),f4(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4702,4736,3858,4604,40])).
% 96.03/96.03 cnf(4759,plain,
% 96.03/96.03 (P4(f8(x47591),a12,f4(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4664,4476,4734,3878,3589,3807,42,41])).
% 96.03/96.03 cnf(4762,plain,
% 96.03/96.03 (P4(f8(x47621),f16(x47622),f11(a12,x47622))),
% 96.03/96.03 inference(scs_inference,[],[4288,3682,3796,3969,41])).
% 96.03/96.03 cnf(4770,plain,
% 96.03/96.03 (P2(x47701,x47701)),
% 96.03/96.03 inference(rename_variables,[],[4])).
% 96.03/96.03 cnf(4773,plain,
% 96.03/96.03 (P5(x47731,f3(x47731,x47732),f4(x47731,x47732))),
% 96.03/96.03 inference(rename_variables,[],[17])).
% 96.03/96.03 cnf(4774,plain,
% 96.03/96.03 (~P5(x47741,f16(a12),f2(a12))),
% 96.03/96.03 inference(rename_variables,[],[1882])).
% 96.03/96.03 cnf(4777,plain,
% 96.03/96.03 (~P2(f2(a12),f4(x47771,a12))),
% 96.03/96.03 inference(scs_inference,[],[4,4770,4686,1882,4774,17,4773,3591,3630,4167,40,42,43])).
% 96.03/96.03 cnf(4790,plain,
% 96.03/96.03 (~P4(f2(x47901),f2(x47901),f2(x47902))+P2(x47902,f17(x47901,x47901))),
% 96.03/96.03 inference(scs_inference,[],[3535,37])).
% 96.03/96.03 cnf(4791,plain,
% 96.03/96.03 (P4(f17(a12,a12),f7(x47911),f20(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4,4727,3834,4334,40])).
% 96.03/96.03 cnf(4798,plain,
% 96.03/96.03 (P4(f4(a12,a12),f7(x47981),f19(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4,4791,4736,4328,40])).
% 96.03/96.03 cnf(4807,plain,
% 96.03/96.03 (P2(x48071,x48071)),
% 96.03/96.03 inference(rename_variables,[],[4])).
% 96.03/96.03 cnf(4810,plain,
% 96.03/96.03 (P2(x48101,x48101)),
% 96.03/96.03 inference(rename_variables,[],[4])).
% 96.03/96.03 cnf(4812,plain,
% 96.03/96.03 (P4(f4(a12,a12),f18(a12,a12),f17(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4,4807,4810,4622,4523,3858,3897,4167,4301,43,42,41])).
% 96.03/96.03 cnf(4818,plain,
% 96.03/96.03 (P4(f4(a12,a12),a12,f17(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4,4798,3834,4301,41])).
% 96.03/96.03 cnf(4830,plain,
% 96.03/96.03 (P5(f2(a12),f2(a12),f1(x48301))),
% 96.03/96.03 inference(scs_inference,[],[4,4615,4165,43])).
% 96.03/96.03 cnf(4843,plain,
% 96.03/96.03 (P4(f7(x48431),f16(x48432),f10(a12,x48432))),
% 96.03/96.03 inference(scs_inference,[],[4,4762,3778,3969,40])).
% 96.03/96.03 cnf(4848,plain,
% 96.03/96.03 (P4(f7(x48481),f9(x48482,x48483),f11(a12,x48483))),
% 96.03/96.03 inference(scs_inference,[],[4,4843,3548,3969,41])).
% 96.03/96.03 cnf(4862,plain,
% 96.03/96.03 (P2(f2(x48621),x48621)),
% 96.03/96.03 inference(rename_variables,[],[5])).
% 96.03/96.03 cnf(4864,plain,
% 96.03/96.03 (~P2(f6(x48641),f4(x48642,a12))),
% 96.03/96.03 inference(scs_inference,[],[5,4862,4777,553,17,3630,31,43])).
% 96.03/96.03 cnf(4874,plain,
% 96.03/96.03 (~P2(f18(a12,a12),f4(x48741,a12))),
% 96.03/96.03 inference(scs_inference,[],[4864,4604,31])).
% 96.03/96.03 cnf(4885,plain,
% 96.03/96.03 (P4(f17(a12,a12),f8(x48851),f4(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[5,4874,4818,4830,4734,4736,3720,3554,3912,4,31,42,40])).
% 96.03/96.03 cnf(4897,plain,
% 96.03/96.03 (P4(f2(a12),f5(a12,a12),f17(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[5,4747,4736,3552,41])).
% 96.03/96.03 cnf(4913,plain,
% 96.03/96.03 (P2(f7(x49131),f8(x49131))),
% 96.03/96.03 inference(rename_variables,[],[6])).
% 96.03/96.03 cnf(4915,plain,
% 96.03/96.03 (P4(f8(x49151),f7(x49151),f17(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[6,4913,4471,4258,4734,4299,3558,4,41,40])).
% 96.03/96.03 cnf(4925,plain,
% 96.03/96.03 (P4(f4(a12,a12),f7(x49251),f17(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4885,4734,4736,3778,40])).
% 96.03/96.03 cnf(4929,plain,
% 96.03/96.03 (P4(f18(a12,a12),a12,f4(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4915,4736,3801,3796,40])).
% 96.03/96.03 cnf(4936,plain,
% 96.03/96.03 (P4(f17(a12,a12),a12,f4(a12,a12))),
% 96.03/96.03 inference(scs_inference,[],[4925,4734,3834,4736,41])).
% 96.03/96.03 cnf(4949,plain,
% 96.03/96.03 (P4(f18(a12,a12),f16(x49491),f10(a12,x49491))),
% 96.03/96.04 inference(scs_inference,[],[4848,3548,3897,3969,40])).
% 96.03/96.04 cnf(4960,plain,
% 96.03/96.04 (P4(f18(a12,a12),f9(x49601,x49602),f11(a12,x49602))),
% 96.03/96.04 inference(scs_inference,[],[4949,4407,3548,3734,3878,3989,3969,4,40,41])).
% 96.03/96.04 cnf(5028,plain,
% 96.03/96.04 (P2(a12,f6(x50281))),
% 96.03/96.04 inference(rename_variables,[],[3571])).
% 96.03/96.04 cnf(5030,plain,
% 96.03/96.04 (P4(f6(x50301),a12,f1(x50302))),
% 96.03/96.04 inference(scs_inference,[],[12,4724,3554,3571,5028,3706,43,40])).
% 96.03/96.04 cnf(5035,plain,
% 96.03/96.04 (P4(f18(a12,a12),f1(x50351),f17(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[4759,4734,3758,3796,40])).
% 96.03/96.04 cnf(5049,plain,
% 96.03/96.04 (P4(f3(x50491,x50492),a12,f16(x50492))),
% 96.03/96.04 inference(scs_inference,[],[12,3591,3758,3558,41])).
% 96.03/96.04 cnf(5060,plain,
% 96.03/96.04 (P5(f18(a12,a12),f6(x50601),f18(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[4591,3917,3635,3878,3801,3552,43,42])).
% 96.03/96.04 cnf(5063,plain,
% 96.03/96.04 (P4(f16(x50631),f6(x50632),f9(x50633,x50631))),
% 96.03/96.04 inference(scs_inference,[],[5049,3591,3682,3571,40])).
% 96.03/96.04 cnf(5067,plain,
% 96.03/96.04 (P4(f9(x50671,x50672),f18(a12,a12),f16(x50672))),
% 96.03/96.04 inference(scs_inference,[],[5063,3548,3682,4604,40])).
% 96.03/96.04 cnf(5072,plain,
% 96.03/96.04 (P4(f16(x50721),f18(a12,a12),f3(x50722,x50721))),
% 96.03/96.04 inference(scs_inference,[],[5067,3548,3630,4,40])).
% 96.03/96.04 cnf(5079,plain,
% 96.03/96.04 (P4(f3(x50791,x50792),f2(a12),f16(x50792))),
% 96.03/96.04 inference(scs_inference,[],[5072,3591,4165,3630,41])).
% 96.03/96.04 cnf(5086,plain,
% 96.03/96.04 (P5(f5(a12,a12),f5(a12,a12),f2(a12))),
% 96.03/96.04 inference(scs_inference,[],[5035,4615,3600,3734,3897,4734,3706,41,42])).
% 96.03/96.04 cnf(5090,plain,
% 96.03/96.04 (P4(f16(x50901),f18(a12,a12),f9(x50902,x50901))),
% 96.03/96.04 inference(scs_inference,[],[5079,3591,3682,4165,40])).
% 96.03/96.04 cnf(5108,plain,
% 96.03/96.04 (P4(f18(a12,a12),f5(a12,a12),f17(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[16,4709,3548,3876,3912,3595,3558,4,40,41])).
% 96.03/96.04 cnf(5113,plain,
% 96.03/96.04 (P4(f9(x51131,x51132),f2(a12),f16(x51132))),
% 96.03/96.04 inference(scs_inference,[],[5090,3548,4167,3682,40])).
% 96.03/96.04 cnf(5134,plain,
% 96.03/96.04 (P5(a12,a12,f1(x51341))),
% 96.03/96.04 inference(scs_inference,[],[5086,3706,3876,42])).
% 96.03/96.04 cnf(5136,plain,
% 96.03/96.04 (P2(f1(x51361),f18(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5086,3706,3876,42,38])).
% 96.03/96.04 cnf(5138,plain,
% 96.03/96.04 (P2(f18(a12,a12),f1(x51381))),
% 96.03/96.04 inference(scs_inference,[],[5086,3706,3876,42,38,24])).
% 96.03/96.04 cnf(5149,plain,
% 96.03/96.04 (P2(f1(x51491),f18(a12,a12))),
% 96.03/96.04 inference(rename_variables,[],[5136])).
% 96.03/96.04 cnf(5151,plain,
% 96.03/96.04 (P4(f16(x51511),f1(x51512),f3(x51513,x51511))),
% 96.03/96.04 inference(scs_inference,[],[4739,5136,5149,5067,3591,3682,4734,4,40,41])).
% 96.03/96.04 cnf(5162,plain,
% 96.03/96.04 (P4(f1(x51621),f18(a12,a12),f20(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5108,5060,5136,4606,3734,3550,43,41])).
% 96.03/96.04 cnf(5170,plain,
% 96.03/96.04 (P4(f16(x51701),f18(a12,a12),f16(x51701))),
% 96.03/96.04 inference(scs_inference,[],[5151,5138,3630,4,41])).
% 96.03/96.04 cnf(5175,plain,
% 96.03/96.04 (P4(f9(x51751,x51752),f1(x51753),f9(x51751,x51752))),
% 96.03/96.04 inference(scs_inference,[],[5170,5138,3682,40])).
% 96.03/96.04 cnf(5178,plain,
% 96.03/96.04 (P4(f1(x51781),f1(x51782),f19(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5162,5138,4328,4,40])).
% 96.03/96.04 cnf(5199,plain,
% 96.03/96.04 (~P2(f17(a12,a12),f1(x51991))),
% 96.03/96.04 inference(scs_inference,[],[17,4264,991,3720,3834,3600,4734,3591,42,41,31])).
% 96.03/96.04 cnf(5206,plain,
% 96.03/96.04 (P2(f18(a12,a12),f1(x52061))),
% 96.03/96.04 inference(rename_variables,[],[5138])).
% 96.03/96.04 cnf(5208,plain,
% 96.03/96.04 (P4(f1(x52081),f16(x52082),f10(a12,x52082))),
% 96.03/96.04 inference(scs_inference,[],[5175,5199,4960,5138,5206,3548,4301,3969,4,31,41,40])).
% 96.03/96.04 cnf(5230,plain,
% 96.03/96.04 (P4(f18(a12,a12),f1(x52301),f20(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[4640,5136,4606,3550,41])).
% 96.03/96.04 cnf(5243,plain,
% 96.03/96.04 (P5(x52431,f18(a12,a12),f7(x52431))),
% 96.03/96.04 inference(scs_inference,[],[3739,5136,3778,5,42])).
% 96.03/96.04 cnf(5261,plain,
% 96.03/96.04 (P5(x52611,f1(x52612),f18(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5243,5136,3912,3558,43])).
% 96.03/96.04 cnf(5274,plain,
% 96.03/96.04 (P4(f18(a12,a12),a12,f19(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[4897,4167,3945,4299,41])).
% 96.03/96.04 cnf(5280,plain,
% 96.03/96.04 (P4(f6(x52801),f1(x52802),f19(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[4647,5138,4328,4,40])).
% 96.03/96.04 cnf(5283,plain,
% 96.03/96.04 (P4(f4(a12,a12),f1(x52831),f20(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[4812,5136,3550,4,41])).
% 96.03/96.04 cnf(5284,plain,
% 96.03/96.04 (P2(x52841,x52841)),
% 96.03/96.04 inference(rename_variables,[],[4])).
% 96.03/96.04 cnf(5287,plain,
% 96.03/96.04 (P5(f18(a12,a12),f1(x52871),f1(x52872))),
% 96.03/96.04 inference(scs_inference,[],[5261,4812,5136,5138,3550,4,5284,41,42])).
% 96.03/96.04 cnf(5292,plain,
% 96.03/96.04 (P5(f1(x52921),f18(a12,a12),f18(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5287,5138,5136,43])).
% 96.03/96.04 cnf(5296,plain,
% 96.03/96.04 (P4(f17(a12,a12),f18(a12,a12),f19(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5283,5136,4328,4734,40])).
% 96.03/96.04 cnf(5299,plain,
% 96.03/96.04 (P4(f19(a12,a12),f1(x52991),f17(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5296,5136,4301,4299,41])).
% 96.03/96.04 cnf(5310,plain,
% 96.03/96.04 (P4(f20(a12,a12),f18(a12,a12),f20(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5299,5136,4334,3595,40])).
% 96.03/96.04 cnf(5314,plain,
% 96.03/96.04 (P5(x53141,f18(a12,a12),f1(x53142))),
% 96.03/96.04 inference(scs_inference,[],[5299,5261,5138,5136,4334,3595,3558,40,43])).
% 96.03/96.04 cnf(5321,plain,
% 96.03/96.04 (P5(f18(a12,a12),f6(x53211),f6(x53211))),
% 96.03/96.04 inference(scs_inference,[],[5292,5138,4604,4,42,43])).
% 96.03/96.04 cnf(5324,plain,
% 96.03/96.04 (P5(f1(x53241),a12,a12)),
% 96.03/96.04 inference(scs_inference,[],[5321,5138,280,42])).
% 96.03/96.04 cnf(5338,plain,
% 96.03/96.04 (P4(f8(x53381),f18(a12,a12),f19(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5230,3807,5136,4328,40])).
% 96.03/96.04 cnf(5362,plain,
% 96.03/96.04 (P4(f2(a12),a12,f19(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[4929,4165,3989,4,41])).
% 96.03/96.04 cnf(5368,plain,
% 96.03/96.04 (P4(a12,f18(a12,a12),f20(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5362,5274,3878,3796,3858,4334,4301,5,41,40])).
% 96.03/96.04 cnf(5371,plain,
% 96.03/96.04 (P4(f17(a12,a12),f6(x53711),f17(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5310,4606,3550,40])).
% 96.03/96.04 cnf(5378,plain,
% 96.03/96.04 (P5(f2(x53781),f8(x53782),f18(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5314,3807,5136,3558,42])).
% 96.03/96.04 cnf(5400,plain,
% 96.03/96.04 (P4(f1(x54001),f2(a12),f19(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5368,5324,3554,4165,3876,5138,4334,43,41])).
% 96.03/96.04 cnf(5407,plain,
% 96.03/96.04 (P4(f2(a12),a12,f4(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5208,5400,3600,3660,3989,3548,3969,5,41,40])).
% 96.03/96.04 cnf(5416,plain,
% 96.03/96.04 (P4(a12,f7(x54161),f17(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[4696,3878,4301,4,41])).
% 96.03/96.04 cnf(5419,plain,
% 96.03/96.04 (P4(f16(x54191),f1(x54192),f9(x54193,x54191))),
% 96.03/96.04 inference(scs_inference,[],[5113,3706,3682,3548,40])).
% 96.03/96.04 cnf(5426,plain,
% 96.03/96.04 (P4(a12,f5(a12,a12),f17(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5338,3552,3720,4301,41])).
% 96.03/96.04 cnf(5433,plain,
% 96.03/96.04 (P5(x54331,f18(a12,a12),f8(x54332))),
% 96.03/96.04 inference(scs_inference,[],[5378,3796,3807,5,42])).
% 96.03/96.04 cnf(5448,plain,
% 96.03/96.04 (P5(x54481,f7(x54482),a12)),
% 96.03/96.04 inference(scs_inference,[],[5433,3897,3720,3558,43])).
% 96.03/96.04 cnf(5463,plain,
% 96.03/96.04 (P4(f19(a12,a12),a12,f19(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5371,3571,4299,41])).
% 96.03/96.04 cnf(5466,plain,
% 96.03/96.04 (P4(a12,f1(x54661),f20(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5178,3554,4334,4,40])).
% 96.03/96.04 cnf(5479,plain,
% 96.03/96.04 (P4(f18(a12,a12),f2(a12),f4(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5280,5134,3600,3758,4604,3989,42,40])).
% 96.03/96.04 cnf(5505,plain,
% 96.03/96.04 (P4(f4(a12,a12),f7(x55051),f4(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5463,5448,3834,3554,3778,3989,43,40])).
% 96.03/96.04 cnf(5512,plain,
% 96.03/96.04 (P4(f3(x55121,x55122),f18(a12,a12),f16(x55122))),
% 96.03/96.04 inference(scs_inference,[],[5419,5136,3630,3548,40])).
% 96.03/96.04 cnf(5519,plain,
% 96.03/96.04 (P4(f16(x55191),f2(a12),f9(x55192,x55191))),
% 96.03/96.04 inference(scs_inference,[],[5512,4165,3630,3548,41])).
% 96.03/96.04 cnf(5563,plain,
% 96.03/96.04 (P4(f17(a12,a12),f18(a12,a12),f17(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5505,5519,3600,3897,3682,4734,3591,41,40])).
% 96.03/96.04 cnf(5573,plain,
% 96.03/96.04 (P4(f6(x55731),f5(a12,a12),f20(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[280,5426,3550,4,41])).
% 96.03/96.04 cnf(5586,plain,
% 96.03/96.04 (P4(f20(a12,a12),a12,f20(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5563,3858,3595,40])).
% 96.03/96.04 cnf(5613,plain,
% 96.03/96.04 (P5(x56131,a12,a12)),
% 96.03/96.04 inference(scs_inference,[],[5586,5433,3878,3554,3720,4334,3558,41,43])).
% 96.03/96.04 cnf(5616,plain,
% 96.03/96.04 (P2(a12,f18(x56161,a12))),
% 96.03/96.04 inference(scs_inference,[],[5586,5433,3878,3554,3720,4334,3558,41,43,38])).
% 96.03/96.04 cnf(5618,plain,
% 96.03/96.04 (P1(f18(x56181,a12))),
% 96.03/96.04 inference(scs_inference,[],[5586,5433,3878,3554,3720,44,4334,3558,41,43,38,22])).
% 96.03/96.04 cnf(5620,plain,
% 96.03/96.04 (~P3(x56201,f18(x56202,a12))),
% 96.03/96.04 inference(scs_inference,[],[5586,5433,3878,3554,3720,44,4334,3558,41,43,38,22,30])).
% 96.03/96.04 cnf(5622,plain,
% 96.03/96.04 (P1(f5(x56221,a12))),
% 96.03/96.04 inference(scs_inference,[],[5586,5433,3878,3554,3720,44,4334,3558,41,43,38,22,30,3767])).
% 96.03/96.04 cnf(5624,plain,
% 96.03/96.04 (~P2(f18(x56241,a12),f16(x56242))),
% 96.03/96.04 inference(scs_inference,[],[5586,5433,3878,3554,3720,44,4334,3558,41,43,38,22,30,3767,3755])).
% 96.03/96.04 cnf(5626,plain,
% 96.03/96.04 (P2(f18(x56261,a12),a12)),
% 96.03/96.04 inference(scs_inference,[],[5586,5433,3878,3554,3720,44,4334,3558,41,43,38,22,30,3767,3755,19])).
% 96.03/96.04 cnf(5630,plain,
% 96.03/96.04 (~P2(f16(a12),f18(x56301,a12))),
% 96.03/96.04 inference(scs_inference,[],[369,5586,5433,3878,3554,3720,44,4334,47,3558,41,43,38,22,30,3767,3755,19,31,33])).
% 96.03/96.04 cnf(5633,plain,
% 96.03/96.04 (P4(f18(x56331,a12),f18(x56331,a12),f17(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[369,5586,5433,4731,3878,3554,3720,44,4334,4734,47,3558,41,43,38,22,30,3767,3755,19,31,33,40])).
% 96.03/96.04 cnf(5635,plain,
% 96.03/96.04 (P2(f5(x56351,a12),a12)),
% 96.03/96.04 inference(scs_inference,[],[5622,19])).
% 96.03/96.04 cnf(5637,plain,
% 96.03/96.04 (P2(a12,f5(x56371,a12))),
% 96.03/96.04 inference(scs_inference,[],[5622,19,24])).
% 96.03/96.04 cnf(5644,plain,
% 96.03/96.04 (~P3(x56441,f18(x56442,a12))),
% 96.03/96.04 inference(rename_variables,[],[5620])).
% 96.03/96.04 cnf(5646,plain,
% 96.03/96.04 (~P2(f11(a12,a12),f18(x56461,a12))),
% 96.03/96.04 inference(scs_inference,[],[5620,5644,5622,5630,5626,4328,11,3630,8,19,24,31,34,33])).
% 96.03/96.04 cnf(5650,plain,
% 96.03/96.04 (P5(f18(x56501,a12),f18(x56501,a12),f18(x56501,a12))),
% 96.03/96.04 inference(scs_inference,[],[5613,5620,5644,5622,5630,5626,4328,11,3630,8,19,24,31,34,33,43])).
% 96.03/96.04 cnf(5651,plain,
% 96.03/96.04 (P5(x56511,a12,a12)),
% 96.03/96.04 inference(rename_variables,[],[5613])).
% 96.03/96.04 cnf(5659,plain,
% 96.03/96.04 (P5(f5(x56591,a12),f5(x56591,a12),f5(x56591,a12))),
% 96.03/96.04 inference(scs_inference,[],[5613,5651,5633,5620,5644,5407,5622,5630,5616,5626,4165,3552,4328,3550,11,3630,4734,8,19,24,31,34,33,43,40,41,42])).
% 96.03/96.04 cnf(5665,plain,
% 96.03/96.04 (P2(f5(x56651,a12),a12)),
% 96.03/96.04 inference(rename_variables,[],[5635])).
% 96.03/96.04 cnf(5672,plain,
% 96.03/96.04 (~P3(f18(x56721,a12),f5(x56722,a12))),
% 96.03/96.04 inference(scs_inference,[],[369,5650,5659,5618,4936,5635,5665,5637,5616,2566,4301,44,4734,31,42,43,40,39])).
% 96.03/96.04 cnf(5685,plain,
% 96.03/96.04 (~P2(f16(a12),f5(x56851,a12))),
% 96.03/96.04 inference(scs_inference,[],[5646,5672,5620,5635,4604,971,3969,7,31,34,33])).
% 96.03/96.04 cnf(5692,plain,
% 96.03/96.04 (~P3(x56921,f5(x56922,a12))),
% 96.03/96.04 inference(scs_inference,[],[5624,5637,3734,44,31,30])).
% 96.03/96.04 cnf(5694,plain,
% 96.03/96.04 (~P2(f11(x56941,x56942),f18(x56943,a12))),
% 96.03/96.04 inference(scs_inference,[],[5624,5620,5637,3734,44,3550,11,31,30,33])).
% 96.03/96.04 cnf(5701,plain,
% 96.03/96.04 (P4(f18(x57011,a12),f18(a12,a12),f19(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5694,5416,5626,3912,4299,3969,31,41])).
% 96.03/96.04 cnf(5712,plain,
% 96.03/96.04 (~P2(f11(a12,a12),f5(x57121,a12))),
% 96.03/96.04 inference(scs_inference,[],[5685,5692,4328,3682,11,31,33])).
% 96.03/96.04 cnf(5734,plain,
% 96.03/96.04 (P4(f5(x57341,a12),f18(a12,a12),f19(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5712,5466,5692,5637,5136,4328,3550,11,3969,31,33,40])).
% 96.03/96.04 cnf(5759,plain,
% 96.03/96.04 (P4(f1(x57591),a12,f17(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5573,5637,3635,3595,41])).
% 96.03/96.04 cnf(5873,plain,
% 96.03/96.04 (P4(f18(a12,a12),f5(x58731,a12),a12)),
% 96.03/96.04 inference(scs_inference,[],[5030,5637,3554,4604,40])).
% 96.03/96.04 cnf(5977,plain,
% 96.03/96.04 (P4(a12,f5(x59771,a12),f4(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5759,5635,3758,4734,41])).
% 96.03/96.04 cnf(6004,plain,
% 96.03/96.04 (P5(f5(x60041,a12),f5(x60041,a12),a12)),
% 96.03/96.04 inference(scs_inference,[],[5977,5134,5637,3554,4734,4,40,42])).
% 96.03/96.04 cnf(6010,plain,
% 96.03/96.04 (P2(f18(x60101,a12),f18(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[6004,5626,5637,43,38])).
% 96.03/96.04 cnf(6016,plain,
% 96.03/96.04 (P2(f18(a12,a12),f18(x60161,a12))),
% 96.03/96.04 inference(scs_inference,[],[6004,5368,5626,5637,3595,4,43,38,41,24])).
% 96.03/96.04 cnf(6020,plain,
% 96.03/96.04 (~P5(f7(x60201),f9(x60202,a12),f7(x60201))),
% 96.03/96.04 inference(scs_inference,[],[3682,2874])).
% 96.03/96.04 cnf(6075,plain,
% 96.03/96.04 (~P2(f7(x60751),f4(a12,x60752))+~P2(f9(x60753,a12),f3(a12,x60752))),
% 96.03/96.04 inference(scs_inference,[],[6020,17,3801,43])).
% 96.03/96.04 cnf(6085,plain,
% 96.03/96.04 (~P2(f4(a12,x60851),f7(x60852))+~P2(f9(x60853,a12),f3(a12,x60851))),
% 96.03/96.04 inference(scs_inference,[],[6075,24])).
% 96.03/96.04 cnf(6090,plain,
% 96.03/96.04 (~P2(f17(a12,a12),f7(x60901))+~P2(f9(x60902,a12),f3(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[4734,6085,31])).
% 96.03/96.04 cnf(6091,plain,
% 96.03/96.04 (P4(a12,f18(x60911,a12),f17(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5734,6010,5637,4301,41])).
% 96.03/96.04 cnf(6099,plain,
% 96.03/96.04 (~P2(f7(x60991),f17(a12,a12))+~P2(f9(x60992,a12),f3(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[6090,24])).
% 96.03/96.04 cnf(6105,plain,
% 96.03/96.04 (~P4(a12,a12,f7(x61051))+~P2(f9(x61052,a12),f3(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[6099,37])).
% 96.03/96.04 cnf(6113,plain,
% 96.03/96.04 (~P4(a12,a12,f7(x61131))),
% 96.03/96.04 inference(scs_inference,[],[3548,3630,6105,31])).
% 96.03/96.04 cnf(6124,plain,
% 96.03/96.04 (~P2(a12,f17(a12,a12))),
% 96.03/96.04 inference(scs_inference,[],[5479,5701,6113,5616,5626,3801,5,35,41,40,31])).
% 96.03/96.04 cnf(6142,plain,
% 96.03/96.04 (~P4(f2(a12),f2(a12),f2(a12))),
% 96.03/96.04 inference(scs_inference,[],[6091,6124,6016,5616,4736,3527,35,31,40,4790])).
% 96.03/96.04 cnf(6144,plain,
% 96.03/96.04 (~P4(f6(x61441),f6(x61441),f6(x61441))),
% 96.03/96.04 inference(scs_inference,[],[6142,448])).
% 96.03/96.04 cnf(6151,plain,
% 96.03/96.04 (~P4(a12,a12,a12)),
% 96.03/96.04 inference(scs_inference,[],[6144,288])).
% 96.03/96.04 cnf(6205,plain,
% 96.03/96.04 ($false),
% 96.03/96.04 inference(scs_inference,[],[5873,6142,6151,6124,4165,3571,5635,5626,5,4,31,41,40]),
% 96.03/96.04 ['proof']).
% 96.03/96.04 % SZS output end Proof
% 96.03/96.04 % Total time :95.380000s
%------------------------------------------------------------------------------