%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : NUN054+1 : TPTP v8.2.0. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n011.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:33 EDT 2024
% Result : Theorem 60.40s 60.49s
% Output : CNFRefutation 60.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : NUN054+1 : TPTP v8.2.0. Bugfixed v7.3.0.
% 0.08/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.14/0.35 % Computer : n011.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Tue Jun 18 21:08:24 EDT 2024
% 0.14/0.35 % CPUTime :
% 0.21/0.58 start to proof:theBenchmark
% 60.40/60.47 %-------------------------------------------
% 60.40/60.47 % File :CSE---1.7
% 60.40/60.47 % Problem :theBenchmark
% 60.40/60.47 % Transform :cnf
% 60.40/60.47 % Format :tptp:raw
% 60.40/60.47 % Command :java -jar mcs_scs.jar %d %s
% 60.40/60.47
% 60.40/60.47 % Result :Theorem 59.840000s
% 60.40/60.47 % Output :CNFRefutation 59.840000s
% 60.40/60.47 %-------------------------------------------
% 60.40/60.48 %------------------------------------------------------------------------------
% 60.40/60.48 % File : NUN054+1 : TPTP v8.2.0. Bugfixed v7.3.0.
% 60.40/60.48 % Domain : Number Theory
% 60.40/60.48 % Problem : Robinson arithmetic: 0+1=1
% 60.40/60.48 % Version : Especial.
% 60.40/60.48 % English :
% 60.40/60.48
% 60.40/60.48 % Refs : [BBJ03] Boolos et al. (2003), Computability and Logic
% 60.40/60.48 % : [Smi07] Smith (2007), An Introduction to Goedel's Theorems
% 60.40/60.48 % : [Lam18] Lampert (2018), Email to Geoff Sutcliffe
% 60.40/60.48 % Source : [Lam18]
% 60.40/60.48 % Names : zeroplusoneidone [Lam18]
% 60.40/60.48
% 60.40/60.48 % Status : Theorem
% 60.40/60.48 % Rating : 0.19 v8.2.0, 0.27 v8.1.0, 0.29 v7.5.0, 0.43 v7.4.0, 0.19 v7.3.0
% 60.40/60.48 % Syntax : Number of formulae : 19 ( 1 unt; 0 def)
% 60.40/60.48 % Number of atoms : 82 ( 0 equ)
% 60.40/60.48 % Maximal formula atoms : 7 ( 4 avg)
% 60.40/60.48 % Number of connectives : 97 ( 34 ~; 26 |; 37 &)
% 60.40/60.48 % ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% 60.40/60.48 % Maximal formula depth : 13 ( 8 avg)
% 60.40/60.48 % Maximal term depth : 1 ( 1 avg)
% 60.40/60.48 % Number of predicates : 5 ( 5 usr; 0 prp; 1-3 aty)
% 60.40/60.48 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 60.40/60.48 % Number of variables : 73 ( 47 !; 26 ?)
% 60.40/60.48 % SPC : FOF_THM_RFO_NEQ
% 60.40/60.48
% 60.40/60.48 % Comments : Translated to FOL without equality.
% 60.40/60.48 % Bugfixes : v7.3.0 - Complete rewrite.
% 60.40/60.48 %------------------------------------------------------------------------------
% 60.40/60.48 include('Axioms/NUM009+0.ax').
% 60.40/60.48 %------------------------------------------------------------------------------
% 60.40/60.48 fof(zeroplusoneidone,conjecture,
% 60.40/60.48 ? [Y1] :
% 60.40/60.48 ( ? [Y2] :
% 60.40/60.48 ( ? [Y4] :
% 60.40/60.48 ( r1(Y4)
% 60.40/60.48 & r3(Y4,Y2,Y1) )
% 60.40/60.48 & ? [Y5] :
% 60.40/60.48 ( r1(Y5)
% 60.40/60.48 & r2(Y5,Y2) ) )
% 60.40/60.48 & ? [Y3] :
% 60.40/60.48 ( id(Y1,Y3)
% 60.40/60.48 & ? [Y6] :
% 60.40/60.48 ( r1(Y6)
% 60.40/60.48 & r2(Y6,Y3) ) ) ) ).
% 60.40/60.48
% 60.40/60.48 %------------------------------------------------------------------------------
% 60.40/60.48 %-------------------------------------------
% 60.40/60.48 % Proof found
% 60.40/60.49 % SZS status Theorem for theBenchmark
% 60.40/60.49 % SZS output start Proof
% 60.40/60.49 %ClaNum:43(EqnAxiom:0)
% 60.40/60.49 %VarNum:213(SingletonVarNum:104)
% 60.40/60.49 %MaxLitNum:7
% 60.40/60.49 %MaxfuncDepth:1
% 60.40/60.49 %SharedTerms:1
% 60.40/60.49 %goalClause: 39
% 60.40/60.49 [4]P2(x41,x41)
% 60.40/60.49 [1]P1(f1(x11))
% 60.40/60.49 [2]P1(f6(x21))
% 60.40/60.49 [3]P1(f8(x31))
% 60.40/60.49 [5]P2(f2(x51),x51)
% 60.40/60.49 [6]P2(f7(x61),f8(x61))
% 60.40/60.49 [12]P4(x121,f1(x121),f2(x121))
% 60.40/60.49 [13]P5(x131,f6(x131),f7(x131))
% 60.40/60.49 [7]P3(x71,f9(x72,x71))
% 60.40/60.49 [8]P3(x81,f3(x82,x81))
% 60.40/60.49 [9]P2(f10(x91,x92),f11(x91,x92))
% 60.40/60.49 [10]P2(f4(x101,x102),f19(x101,x102))
% 60.40/60.49 [11]P3(f20(x111,x112),f11(x111,x112))
% 60.40/60.49 [14]P4(x141,x142,f20(x141,x142))
% 60.40/60.49 [15]P5(x151,x152,f5(x151,x152))
% 60.40/60.49 [16]P4(x161,f9(x161,x162),f10(x161,x162))
% 60.40/60.49 [17]P5(x171,f3(x171,x172),f4(x171,x172))
% 60.40/60.49 [18]P4(f5(x181,x182),x181,f19(x181,x182))
% 60.40/60.49 [19]~P1(x191)+P2(x191,a12)
% 60.40/60.49 [20]P1(x201)+~P2(x201,a12)
% 60.40/60.49 [21]P2(x211,f15(x211))+P1(f13(x211))
% 60.40/60.49 [25]P3(f14(x251),f15(x251))+P1(f13(x251))
% 60.40/60.49 [26]P2(x261,f15(x261))+P2(x261,f13(x261))
% 60.40/60.49 [29]P3(f14(x291),f15(x291))+P2(x291,f13(x291))
% 60.40/60.49 [24]~P2(x242,x241)+P2(x241,x242)
% 60.40/60.49 [27]~P3(x272,x271)+P2(x271,f16(x272))
% 60.40/60.49 [28]P3(x281,x282)+~P2(x282,f16(x281))
% 60.40/60.49 [35]P4(x351,x352,x353)+~P2(x353,f17(x351,x352))
% 60.40/60.49 [36]P5(x361,x362,x363)+~P2(x363,f18(x361,x362))
% 60.40/60.49 [37]~P4(x372,x373,x371)+P2(x371,f17(x372,x373))
% 60.40/60.49 [38]~P5(x382,x383,x381)+P2(x381,f18(x382,x383))
% 60.40/60.49 [22]~P2(x222,x221)+P1(x221)+~P1(x222)
% 60.40/60.49 [23]~P2(x231,x232)+P1(x231)+~P1(x232)
% 60.40/60.49 [30]~P1(x301)+~P2(x301,x302)+~P3(x303,x302)
% 60.40/60.49 [31]~P2(x311,x313)+P2(x311,x312)+~P2(x313,x312)
% 60.40/60.49 [32]~P3(x322,x324)+~P3(x321,x323)+P2(x321,x322)+~P2(x323,x324)
% 60.40/60.49 [33]~P3(x334,x333)+P3(x331,x332)+~P2(x333,x332)+~P2(x334,x331)
% 60.40/60.49 [34]~P3(x344,x343)+P3(x341,x342)+~P2(x342,x343)+~P2(x341,x344)
% 60.40/60.49 [40]~P4(x406,x405,x404)+P4(x401,x402,x403)+~P2(x404,x403)+~P2(x405,x402)+~P2(x406,x401)
% 60.40/60.49 [41]~P4(x416,x415,x414)+P4(x411,x412,x413)+~P2(x413,x414)+~P2(x412,x415)+~P2(x411,x416)
% 60.40/60.49 [42]~P5(x426,x425,x424)+P5(x421,x422,x423)+~P2(x424,x423)+~P2(x425,x422)+~P2(x426,x421)
% 60.40/60.49 [43]~P5(x436,x435,x434)+P5(x431,x432,x433)+~P2(x433,x434)+~P2(x432,x435)+~P2(x431,x436)
% 60.40/60.49 [39]~P3(x391,x395)+~P4(x393,x396,x394)+~P1(x391)+~P1(x392)+~P2(x394,x395)+~P1(x393)+~P3(x392,x396)
% 60.40/60.49 %EqnAxiom
% 60.40/60.49
% 60.40/60.49 %-------------------------------------------
% 60.40/60.51 cnf(44,plain,
% 60.40/60.51 (P1(a12)),
% 60.40/60.51 inference(scs_inference,[],[4,20])).
% 60.40/60.51 cnf(45,plain,
% 60.40/60.51 (P2(x451,x451)),
% 60.40/60.51 inference(rename_variables,[],[4])).
% 60.40/60.51 cnf(47,plain,
% 60.40/60.51 (P3(x471,f16(x471))),
% 60.40/60.51 inference(scs_inference,[],[4,45,20,28])).
% 60.40/60.51 cnf(48,plain,
% 60.40/60.51 (P2(x481,x481)),
% 60.40/60.51 inference(rename_variables,[],[4])).
% 60.40/60.51 cnf(50,plain,
% 60.40/60.51 (P4(x501,x502,f17(x501,x502))),
% 60.40/60.51 inference(scs_inference,[],[4,45,48,20,28,35])).
% 60.40/60.51 cnf(51,plain,
% 60.40/60.51 (P2(x511,x511)),
% 60.40/60.51 inference(rename_variables,[],[4])).
% 60.40/60.51 cnf(53,plain,
% 60.40/60.51 (P5(x531,x532,f18(x531,x532))),
% 60.40/60.51 inference(scs_inference,[],[4,45,48,51,20,28,35,36])).
% 60.40/60.51 cnf(54,plain,
% 60.40/60.51 (P2(x541,x541)),
% 60.40/60.51 inference(rename_variables,[],[4])).
% 60.40/60.51 cnf(56,plain,
% 60.40/60.51 (~P3(x561,f1(x562))),
% 60.40/60.51 inference(scs_inference,[],[1,4,45,48,51,54,20,28,35,36,30])).
% 60.40/60.51 cnf(57,plain,
% 60.40/60.51 (P2(x571,x571)),
% 60.40/60.51 inference(rename_variables,[],[4])).
% 60.40/60.51 cnf(60,plain,
% 60.40/60.51 (P2(f2(x601),x601)),
% 60.40/60.51 inference(rename_variables,[],[5])).
% 60.40/60.51 cnf(61,plain,
% 60.40/60.51 (P2(x611,x611)),
% 60.40/60.51 inference(rename_variables,[],[4])).
% 60.40/60.51 cnf(64,plain,
% 60.40/60.51 (P2(f2(x641),x641)),
% 60.40/60.51 inference(rename_variables,[],[5])).
% 60.40/60.51 cnf(65,plain,
% 60.40/60.51 (P2(x651,x651)),
% 60.40/60.51 inference(rename_variables,[],[4])).
% 60.40/60.51 cnf(67,plain,
% 60.40/60.51 (P4(x671,x671,f2(f20(x671,x671)))),
% 60.40/60.51 inference(scs_inference,[],[1,7,4,45,48,51,54,57,61,65,14,5,60,64,20,28,35,36,30,33,34,41])).
% 60.40/60.51 cnf(68,plain,
% 60.40/60.51 (P2(f2(x681),x681)),
% 60.40/60.51 inference(rename_variables,[],[5])).
% 60.40/60.51 cnf(70,plain,
% 60.40/60.51 (P2(x701,x701)),
% 60.40/60.51 inference(rename_variables,[],[4])).
% 60.40/60.51 cnf(73,plain,
% 60.40/60.51 (P5(x731,x731,f2(f5(x731,x731)))),
% 60.40/60.51 inference(scs_inference,[],[1,7,4,45,48,51,54,57,61,65,70,14,5,60,64,68,15,20,28,35,36,30,33,34,41,43])).
% 60.40/60.51 cnf(76,plain,
% 60.40/60.51 (P2(x761,x761)),
% 60.40/60.51 inference(rename_variables,[],[4])).
% 60.40/60.51 cnf(79,plain,
% 60.40/60.51 (~P4(a12,f9(x791,a12),f9(x791,a12))),
% 60.40/60.51 inference(scs_inference,[],[1,7,4,45,48,51,54,57,61,65,70,76,14,5,60,64,68,15,20,28,35,36,30,33,34,41,43,39])).
% 60.40/60.51 cnf(88,plain,
% 60.40/60.51 (P2(f2(x881),x881)),
% 60.40/60.51 inference(rename_variables,[],[5])).
% 60.40/60.51 cnf(90,plain,
% 60.40/60.51 (P5(x901,x902,f2(f18(x901,x902)))),
% 60.40/60.51 inference(scs_inference,[],[5,88,28,36])).
% 60.40/60.51 cnf(91,plain,
% 60.40/60.51 (P2(f2(x911),x911)),
% 60.40/60.51 inference(rename_variables,[],[5])).
% 60.40/60.51 cnf(93,plain,
% 60.40/60.51 (P1(f2(a12))),
% 60.40/60.51 inference(scs_inference,[],[5,88,91,28,36,20])).
% 60.40/60.51 cnf(94,plain,
% 60.40/60.51 (P2(f2(x941),x941)),
% 60.40/60.51 inference(rename_variables,[],[5])).
% 60.40/60.51 cnf(100,plain,
% 60.40/60.51 (P2(x1001,x1001)),
% 60.40/60.51 inference(rename_variables,[],[4])).
% 60.40/60.51 cnf(103,plain,
% 60.40/60.51 (P2(x1031,x1031)),
% 60.40/60.51 inference(rename_variables,[],[4])).
% 60.40/60.51 cnf(104,plain,
% 60.40/60.51 (P3(x1041,f9(x1042,x1041))),
% 60.40/60.51 inference(rename_variables,[],[7])).
% 60.40/60.51 cnf(106,plain,
% 60.40/60.51 (P3(f8(x1061),f9(x1062,f7(x1061)))),
% 60.40/60.51 inference(scs_inference,[],[7,104,6,44,4,100,103,5,88,91,94,28,36,20,35,30,34,33])).
% 60.40/60.51 cnf(129,plain,
% 60.40/60.51 (~P3(x1291,f2(a12))),
% 60.40/60.51 inference(scs_inference,[],[93,4,30])).
% 60.51/60.51 cnf(130,plain,
% 60.51/60.51 (P2(x1301,x1301)),
% 60.51/60.51 inference(rename_variables,[],[4])).
% 60.51/60.51 cnf(133,plain,
% 60.51/60.51 (P2(x1331,x1331)),
% 60.51/60.51 inference(rename_variables,[],[4])).
% 60.51/60.51 cnf(134,plain,
% 60.51/60.51 (P3(x1341,f9(x1342,x1341))),
% 60.51/60.51 inference(rename_variables,[],[7])).
% 60.51/60.51 cnf(138,plain,
% 60.51/60.51 (P3(x1381,f9(x1382,x1381))),
% 60.51/60.51 inference(rename_variables,[],[7])).
% 60.51/60.51 cnf(141,plain,
% 60.51/60.51 (P2(f2(x1411),x1411)),
% 60.51/60.51 inference(rename_variables,[],[5])).
% 60.51/60.51 cnf(148,plain,
% 60.51/60.51 (~P3(f1(x1481),f11(f1(x1481),f1(x1481)))),
% 60.51/60.51 inference(scs_inference,[],[1,7,134,138,67,16,9,93,4,130,133,5,141,73,30,33,34,40,42,39])).
% 60.51/60.51 cnf(157,plain,
% 60.51/60.51 (~P3(x1571,f6(x1572))),
% 60.51/60.51 inference(scs_inference,[],[2,4,30])).
% 60.51/60.51 cnf(182,plain,
% 60.51/60.51 (~P3(x1821,f8(x1822))),
% 60.51/60.51 inference(scs_inference,[],[3,4,30])).
% 60.51/60.51 cnf(202,plain,
% 60.51/60.51 (P2(f2(x2021),x2021)),
% 60.51/60.51 inference(rename_variables,[],[5])).
% 60.51/60.51 cnf(205,plain,
% 60.51/60.51 (P2(x2051,x2051)),
% 60.51/60.51 inference(rename_variables,[],[4])).
% 60.51/60.51 cnf(206,plain,
% 60.51/60.51 (P3(x2061,f9(x2062,x2061))),
% 60.51/60.51 inference(rename_variables,[],[7])).
% 60.51/60.51 cnf(208,plain,
% 60.51/60.51 (P3(f2(x2081),f9(x2082,x2081))),
% 60.51/60.51 inference(scs_inference,[],[7,206,5,202,9,4,205,31,33,34])).
% 60.51/60.51 cnf(209,plain,
% 60.51/60.51 (P2(x2091,x2091)),
% 60.51/60.51 inference(rename_variables,[],[4])).
% 60.51/60.51 cnf(210,plain,
% 60.51/60.51 (P2(f2(x2101),x2101)),
% 60.52/60.51 inference(rename_variables,[],[5])).
% 60.52/60.51 cnf(213,plain,
% 60.52/60.51 (P2(x2131,x2131)),
% 60.52/60.51 inference(rename_variables,[],[4])).
% 60.52/60.51 cnf(221,plain,
% 60.52/60.51 (P2(f2(x2211),x2211)),
% 60.52/60.51 inference(rename_variables,[],[5])).
% 60.52/60.51 cnf(225,plain,
% 60.52/60.51 (~P5(x2251,x2251,x2251)+P5(f2(x2251),f2(x2251),f2(x2251))),
% 60.52/60.51 inference(scs_inference,[],[7,206,5,202,210,221,44,9,50,4,205,209,213,53,31,33,34,40,42,39,43])).
% 60.52/60.51 cnf(227,plain,
% 60.52/60.51 (~P4(x2271,x2271,x2271)+P4(f2(x2271),f2(x2271),f2(x2271))),
% 60.52/60.51 inference(scs_inference,[],[7,206,5,202,210,221,44,9,50,4,205,209,213,53,31,33,34,40,42,39,43,41])).
% 60.52/60.51 cnf(240,plain,
% 60.52/60.51 (P2(f2(f7(x2401)),f8(x2401))),
% 60.52/60.51 inference(scs_inference,[],[5,6,31])).
% 60.52/60.51 cnf(261,plain,
% 60.52/60.51 (~P4(f8(x2611),f8(x2611),f8(x2611))+P4(f7(x2611),f7(x2611),f7(x2611))),
% 60.52/60.51 inference(scs_inference,[],[5,240,40,41])).
% 60.52/60.51 cnf(287,plain,
% 60.52/60.51 (~P5(f8(x2871),f8(x2871),f8(x2871))+P5(f7(x2871),f7(x2871),f7(x2871))),
% 60.52/60.51 inference(scs_inference,[],[9,6,40,42,43])).
% 60.52/60.51 cnf(293,plain,
% 60.52/60.51 (P2(f6(x2931),a12)),
% 60.52/60.51 inference(scs_inference,[],[2,4,19,22])).
% 60.52/60.51 cnf(330,plain,
% 60.52/60.51 (P2(f2(f6(x3301)),a12)),
% 60.52/60.51 inference(scs_inference,[],[5,293,31])).
% 60.52/60.51 cnf(358,plain,
% 60.52/60.51 (~P3(a12,f11(a12,a12))),
% 60.52/60.51 inference(scs_inference,[],[7,9,5,44,16,90,42,39])).
% 60.52/60.51 cnf(423,plain,
% 60.52/60.51 (~P3(f8(x4231),f11(f8(x4231),f8(x4231)))),
% 60.52/60.51 inference(scs_inference,[],[9,7,3,16,39])).
% 60.52/60.51 cnf(614,plain,
% 60.52/60.51 (~P2(f1(x6141),f20(f1(x6141),f1(x6141)))),
% 60.52/60.51 inference(scs_inference,[],[148,4,11,34])).
% 60.52/60.51 cnf(624,plain,
% 60.52/60.51 (~P2(f8(x6241),f20(f8(x6241),f8(x6241)))),
% 60.52/60.51 inference(scs_inference,[],[423,4,614,11,24,34])).
% 60.52/60.51 cnf(631,plain,
% 60.52/60.51 (~P2(f20(f8(x6311),f8(x6311)),f8(x6311))),
% 60.52/60.51 inference(scs_inference,[],[624,24])).
% 60.52/60.51 cnf(640,plain,
% 60.52/60.51 (~P2(a12,f20(a12,a12))),
% 60.52/60.51 inference(scs_inference,[],[358,4,11,34])).
% 60.52/60.51 cnf(644,plain,
% 60.52/60.51 (~P2(f20(a12,a12),a12)),
% 60.52/60.51 inference(scs_inference,[],[358,4,11,34,24])).
% 60.52/60.51 cnf(648,plain,
% 60.52/60.51 (~P1(f20(a12,a12))),
% 60.52/60.51 inference(scs_inference,[],[358,10,4,631,11,34,24,32,19])).
% 60.52/60.51 cnf(678,plain,
% 60.52/60.51 (~P2(f20(a12,a12),f6(x6781))),
% 60.52/60.51 inference(scs_inference,[],[293,644,31])).
% 60.52/60.51 cnf(688,plain,
% 60.52/60.51 (~P2(f2(a12),f20(a12,a12))),
% 60.52/60.51 inference(scs_inference,[],[5,644,31,24])).
% 60.52/60.51 cnf(699,plain,
% 60.52/60.51 (~P2(f2(f6(x6991)),f20(a12,a12))),
% 60.52/60.51 inference(scs_inference,[],[148,9,4,330,644,31,33,24])).
% 60.52/60.51 cnf(718,plain,
% 60.52/60.51 (~P3(f6(x7181),f10(a12,a12))),
% 60.52/60.51 inference(scs_inference,[],[358,9,293,33])).
% 60.52/60.51 cnf(863,plain,
% 60.52/60.51 (P2(f10(x8631,x8632),f11(x8631,x8632))),
% 60.52/60.51 inference(rename_variables,[],[9])).
% 60.52/60.51 cnf(866,plain,
% 60.52/60.51 (~P3(a12,f11(a12,f7(x8661)))),
% 60.52/60.51 inference(scs_inference,[],[106,9,863,640,44,3,16,11,32,39])).
% 60.52/60.51 cnf(872,plain,
% 60.52/60.51 (P2(f10(x8721,x8722),f11(x8721,x8722))),
% 60.52/60.51 inference(rename_variables,[],[9])).
% 60.52/60.51 cnf(873,plain,
% 60.52/60.51 (P3(f20(x8731,x8732),f11(x8731,x8732))),
% 60.52/60.51 inference(rename_variables,[],[11])).
% 60.52/60.51 cnf(876,plain,
% 60.52/60.51 (P2(f10(x8761,x8762),f11(x8761,x8762))),
% 60.52/60.51 inference(rename_variables,[],[9])).
% 60.52/60.51 cnf(878,plain,
% 60.52/60.51 (~P2(a12,f20(a12,f7(x8781)))),
% 60.52/60.51 inference(scs_inference,[],[866,9,872,293,4,624,11,873,32,33,34])).
% 60.52/60.51 cnf(882,plain,
% 60.52/60.51 (~P3(f1(x8821),f11(f1(x8821),f7(x8822)))),
% 60.52/60.51 inference(scs_inference,[],[106,866,9,872,876,293,4,624,1,3,16,11,873,32,33,34,39])).
% 60.52/60.51 cnf(887,plain,
% 60.52/60.51 (~P2(f20(a12,f7(x8871)),a12)),
% 60.52/60.51 inference(scs_inference,[],[878,24])).
% 60.52/60.51 cnf(891,plain,
% 60.52/60.51 (~P3(f2(a12),f10(a12,a12))),
% 60.52/60.51 inference(scs_inference,[],[9,688,878,11,24,19,32])).
% 60.52/60.51 cnf(892,plain,
% 60.52/60.51 (P2(f10(x8921,x8922),f11(x8921,x8922))),
% 60.52/60.51 inference(rename_variables,[],[9])).
% 60.52/60.51 cnf(893,plain,
% 60.52/60.51 (P3(f20(x8931,x8932),f11(x8931,x8932))),
% 60.52/60.51 inference(rename_variables,[],[11])).
% 60.52/60.51 cnf(896,plain,
% 60.52/60.51 (P2(f10(x8961,x8962),f11(x8961,x8962))),
% 60.52/60.51 inference(rename_variables,[],[9])).
% 60.52/60.51 cnf(897,plain,
% 60.52/60.51 (P2(x8971,x8971)),
% 60.52/60.51 inference(rename_variables,[],[4])).
% 60.52/60.51 cnf(899,plain,
% 60.52/60.51 (~P2(f1(x8991),f20(f1(x8991),f7(x8992)))),
% 60.52/60.51 inference(scs_inference,[],[882,9,892,4,897,688,878,11,893,24,19,32,33,34])).
% 60.52/60.51 cnf(903,plain,
% 60.52/60.51 (~P3(f2(a12),f11(f2(a12),f7(x9031)))),
% 60.52/60.51 inference(scs_inference,[],[106,882,9,892,896,4,897,688,93,3,878,16,11,893,24,19,32,33,34,39])).
% 60.52/60.51 cnf(911,plain,
% 60.52/60.51 (P2(f10(x9111,x9112),f11(x9111,x9112))),
% 60.52/60.51 inference(rename_variables,[],[9])).
% 60.52/60.51 cnf(915,plain,
% 60.52/60.51 (P2(f10(x9151,x9152),f11(x9151,x9152))),
% 60.52/60.51 inference(rename_variables,[],[9])).
% 60.52/60.51 cnf(916,plain,
% 60.52/60.51 (P2(x9161,x9161)),
% 60.52/60.51 inference(rename_variables,[],[4])).
% 60.52/60.51 cnf(922,plain,
% 60.52/60.51 (~P3(f8(x9221),f11(f8(x9221),f7(x9221)))),
% 60.52/60.51 inference(scs_inference,[],[106,903,9,911,915,4,916,5,699,3,899,16,11,24,32,33,34,39])).
% 60.52/60.51 cnf(963,plain,
% 60.52/60.51 (~P3(a12,f11(x9631,x9632))+~P3(f20(a12,a12),f10(x9631,x9632))),
% 60.52/60.51 inference(scs_inference,[],[922,9,6,4,644,33,32])).
% 60.52/60.51 cnf(983,plain,
% 60.52/60.51 (~P3(f20(a12,a12),f10(x9831,x9832))+~P2(f11(x9831,x9832),f16(a12))),
% 60.52/60.51 inference(scs_inference,[],[963,28])).
% 60.52/60.51 cnf(987,plain,
% 60.52/60.51 (~P2(f11(a12,a12),f16(a12))),
% 60.52/60.51 inference(scs_inference,[],[9,4,11,983,34])).
% 60.52/60.51 cnf(1048,plain,
% 60.52/60.51 (~P3(f6(x10481),f11(a12,a12))),
% 60.52/60.51 inference(scs_inference,[],[358,293,4,33])).
% 60.52/60.51 cnf(1702,plain,
% 60.52/60.51 (~P3(f20(a12,a12),f9(x17021,a12))),
% 60.52/60.51 inference(scs_inference,[],[7,644,4,32])).
% 60.52/60.51 cnf(2950,plain,
% 60.52/60.51 (~P2(f20(a12,a12),f1(x29501))),
% 60.52/60.51 inference(scs_inference,[],[1,648,23])).
% 60.52/60.51 cnf(3064,plain,
% 60.52/60.51 (~P2(f20(a12,a12),f8(x30641))),
% 60.52/60.51 inference(scs_inference,[],[3,648,23])).
% 60.52/60.51 cnf(3066,plain,
% 60.52/60.51 (~P2(f8(x30661),f20(a12,a12))),
% 60.52/60.51 inference(scs_inference,[],[3,648,23,24])).
% 60.52/60.51 cnf(3344,plain,
% 60.52/60.51 (~P3(f8(x33441),f10(a12,a12))),
% 60.52/60.51 inference(scs_inference,[],[9,3066,11,32])).
% 60.52/60.51 cnf(3613,plain,
% 60.52/60.51 (P2(x36131,x36131)),
% 60.52/60.51 inference(rename_variables,[],[4])).
% 60.52/60.51 cnf(3614,plain,
% 60.52/60.51 (P3(x36141,f16(x36141))),
% 60.52/60.51 inference(rename_variables,[],[47])).
% 60.52/60.51 cnf(3616,plain,
% 60.52/60.51 (~P4(a12,f16(a12),f16(a12))),
% 60.52/60.51 inference(scs_inference,[],[47,3614,4,3613,987,44,32,39])).
% 60.52/60.51 cnf(3623,plain,
% 60.52/60.51 (P2(x36231,x36231)),
% 60.52/60.51 inference(rename_variables,[],[4])).
% 60.52/60.51 cnf(3626,plain,
% 60.52/60.51 (~P4(f2(a12),f16(a12),f16(a12))),
% 60.52/60.51 inference(scs_inference,[],[47,3616,4,3623,5,887,32,40])).
% 60.52/60.51 cnf(3933,plain,
% 60.52/60.51 (~P2(f20(a12,a12),f7(x39331))),
% 60.52/60.51 inference(scs_inference,[],[6,3064,31])).
% 60.52/60.51 cnf(3936,plain,
% 60.52/60.51 (~P2(f7(x39361),f20(a12,a12))),
% 60.52/60.51 inference(scs_inference,[],[6,3064,31,24])).
% 60.52/60.51 cnf(3946,plain,
% 60.52/60.51 (~P5(x39461,x39461,f2(x39462))+P5(x39461,x39461,x39462)),
% 60.52/60.51 inference(scs_inference,[],[4,5,42])).
% 60.52/60.51 cnf(3961,plain,
% 60.52/60.51 (~P4(f2(a12),f9(x39611,a12),f9(x39611,a12))),
% 60.52/60.51 inference(scs_inference,[],[4,79,5,40])).
% 60.52/60.51 cnf(3965,plain,
% 60.52/60.51 (P2(f20(x39651,x39652),f17(x39651,x39652))),
% 60.52/60.51 inference(scs_inference,[],[14,37])).
% 60.52/60.52 cnf(3967,plain,
% 60.52/60.52 (P2(f5(x39671,x39672),f18(x39671,x39672))),
% 60.52/60.52 inference(scs_inference,[],[14,15,37,38])).
% 60.52/60.52 cnf(3969,plain,
% 60.52/60.52 (~P2(f1(x39691),f16(x39692))),
% 60.52/60.52 inference(scs_inference,[],[56,14,15,37,38,28])).
% 60.52/60.52 cnf(3971,plain,
% 60.52/60.52 (P2(f1(x39711),a12)),
% 60.52/60.52 inference(scs_inference,[],[1,56,14,15,37,38,28,19])).
% 60.52/60.52 cnf(3973,plain,
% 60.52/60.52 (P2(f3(x39731,x39732),f16(x39732))),
% 60.52/60.52 inference(scs_inference,[],[1,56,14,15,8,37,38,28,19,27])).
% 60.52/60.52 cnf(3975,plain,
% 60.52/60.52 (P2(a12,f6(x39751))),
% 60.52/60.52 inference(scs_inference,[],[1,56,14,15,8,293,37,38,28,19,27,24])).
% 60.52/60.52 cnf(3979,plain,
% 60.52/60.52 (~P1(f10(x39791,x39792))),
% 60.52/60.52 inference(scs_inference,[],[1,56,3933,14,15,8,293,9,11,37,38,28,19,27,24,31,30])).
% 60.52/60.52 cnf(3982,plain,
% 60.52/60.52 (~P2(f1(x39821),f3(x39822,a12))),
% 60.52/60.52 inference(scs_inference,[],[1,56,3933,14,15,8,293,9,11,37,38,28,19,27,24,31,30,34])).
% 60.52/60.52 cnf(3983,plain,
% 60.52/60.52 (P3(x39831,f3(x39832,x39831))),
% 60.52/60.52 inference(rename_variables,[],[8])).
% 60.52/60.52 cnf(3984,plain,
% 60.52/60.52 (~P3(x39841,f1(x39842))),
% 60.52/60.52 inference(rename_variables,[],[56])).
% 60.52/60.52 cnf(3986,plain,
% 60.52/60.52 (~P2(f3(x39861,x39862),f1(x39863))),
% 60.52/60.52 inference(scs_inference,[],[1,56,3984,3933,14,15,8,3983,293,9,4,11,37,38,28,19,27,24,31,30,34,33])).
% 60.52/60.52 cnf(3987,plain,
% 60.52/60.52 (P2(x39871,x39871)),
% 60.52/60.52 inference(rename_variables,[],[4])).
% 60.52/60.52 cnf(3992,plain,
% 60.52/60.52 (P2(x39921,x39921)),
% 60.52/60.52 inference(rename_variables,[],[4])).
% 60.52/60.52 cnf(3996,plain,
% 60.52/60.52 (P2(x39961,x39961)),
% 60.52/60.52 inference(rename_variables,[],[4])).
% 60.52/60.52 cnf(4002,plain,
% 60.52/60.52 (P2(x40021,f2(x40021))),
% 60.52/60.52 inference(scs_inference,[],[1,56,3984,3933,14,15,8,3983,208,293,10,7,9,4,3987,3992,3996,11,37,38,28,19,27,24,31,30,34,33,40,42,20,23,32])).
% 60.52/60.52 cnf(4011,plain,
% 60.52/60.52 (P2(f8(x40111),a12)),
% 60.52/60.52 inference(scs_inference,[],[3,19])).
% 60.52/60.52 cnf(4013,plain,
% 60.52/60.52 (~P2(f6(x40131),f16(x40132))),
% 60.52/60.52 inference(scs_inference,[],[157,3,19,28])).
% 60.52/60.52 cnf(4015,plain,
% 60.52/60.52 (P2(f9(x40151,x40152),f16(x40152))),
% 60.52/60.52 inference(scs_inference,[],[157,3,7,19,28,27])).
% 60.52/60.52 cnf(4017,plain,
% 60.52/60.52 (P2(f17(x40171,x40172),f20(x40171,x40172))),
% 60.52/60.52 inference(scs_inference,[],[3965,157,3,7,19,28,27,24])).
% 60.52/60.52 cnf(4019,plain,
% 60.52/60.52 (~P2(f16(x40191),f1(x40192))),
% 60.52/60.52 inference(scs_inference,[],[3965,3973,157,3986,3,7,19,28,27,24,31])).
% 60.52/60.52 cnf(4020,plain,
% 60.52/60.52 (P2(f3(x40201,x40202),f16(x40202))),
% 60.52/60.52 inference(rename_variables,[],[3973])).
% 60.52/60.52 cnf(4025,plain,
% 60.52/60.52 (~P2(f6(x40251),f9(x40252,x40253))),
% 60.52/60.52 inference(scs_inference,[],[3965,4002,3973,4020,157,3986,208,47,3,7,19,28,27,24,31,30,34])).
% 60.52/60.52 cnf(4026,plain,
% 60.52/60.52 (P3(f2(x40261),f9(x40262,x40261))),
% 60.52/60.52 inference(rename_variables,[],[208])).
% 60.52/60.52 cnf(4027,plain,
% 60.52/60.52 (~P3(x40271,f6(x40272))),
% 60.52/60.52 inference(rename_variables,[],[157])).
% 60.52/60.52 cnf(4029,plain,
% 60.52/60.52 (~P2(f9(x40291,x40292),f6(x40293))),
% 60.52/60.52 inference(scs_inference,[],[3965,4002,3973,4020,157,4027,3986,208,4026,47,3,7,19,28,27,24,31,30,34,33])).
% 60.52/60.52 cnf(4033,plain,
% 60.52/60.52 (~P3(f7(x40331),f10(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[3965,4002,3973,4020,157,4027,3986,3936,208,4026,47,3,7,9,11,19,28,27,24,31,30,34,33,32])).
% 60.52/60.52 cnf(4058,plain,
% 60.52/60.52 (P2(f16(x40581),f9(x40582,x40581))),
% 60.52/60.52 inference(scs_inference,[],[4015,182,28,24])).
% 60.52/60.52 cnf(4061,plain,
% 60.52/60.52 (P2(f9(x40611,x40612),f16(x40612))),
% 60.52/60.52 inference(rename_variables,[],[4015])).
% 60.52/60.52 cnf(4066,plain,
% 60.52/60.52 (~P2(f10(a12,a12),f3(x40661,a12))),
% 60.52/60.52 inference(scs_inference,[],[4015,4061,182,3344,4029,4011,8,47,28,24,31,30,34])).
% 60.52/60.52 cnf(4068,plain,
% 60.52/60.52 (P3(x40681,f3(x40682,x40681))),
% 60.52/60.52 inference(rename_variables,[],[8])).
% 60.52/60.52 cnf(4080,plain,
% 60.52/60.52 (P5(f8(x40801),f8(x40801),f5(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4015,4061,182,3344,4029,718,3961,4011,3967,3975,4002,53,8,4068,47,16,4,28,24,31,30,34,33,40,43])).
% 60.52/60.52 cnf(4088,plain,
% 60.52/60.52 (P2(f16(x40881),f3(x40882,x40881))),
% 60.52/60.52 inference(scs_inference,[],[129,3973,28,24])).
% 60.52/60.52 cnf(4090,plain,
% 60.52/60.52 (~P2(a12,f16(x40901))),
% 60.52/60.52 inference(scs_inference,[],[3969,129,3973,3971,28,24,31])).
% 60.52/60.52 cnf(4097,plain,
% 60.52/60.52 (P3(x40971,f3(x40972,x40971))),
% 60.52/60.52 inference(rename_variables,[],[8])).
% 60.52/60.52 cnf(4098,plain,
% 60.52/60.52 (~P3(x40981,f2(a12))),
% 60.52/60.52 inference(rename_variables,[],[129])).
% 60.52/60.52 cnf(4100,plain,
% 60.52/60.52 (~P2(f3(x41001,a12),f2(a12))),
% 60.52/60.52 inference(scs_inference,[],[4058,3969,129,4098,3973,3971,3975,4011,8,4097,208,28,24,31,30,34,33])).
% 60.52/60.52 cnf(4106,plain,
% 60.52/60.52 (P2(f18(x41061,x41062),f5(x41061,x41062))),
% 60.52/60.52 inference(scs_inference,[],[3967,24])).
% 60.52/60.52 cnf(4108,plain,
% 60.52/60.52 (~P2(f9(x41081,x41082),f1(x41083))),
% 60.52/60.52 inference(scs_inference,[],[4019,4058,3967,24,31])).
% 60.52/60.52 cnf(4121,plain,
% 60.52/60.52 (~P2(f17(a12,a12),a12)),
% 60.52/60.52 inference(scs_inference,[],[4017,4019,18,4058,3967,648,5,10,4,24,31,41,22,23,20])).
% 60.52/60.52 cnf(4125,plain,
% 60.52/60.52 (P2(a12,f1(x41251))),
% 60.52/60.52 inference(scs_inference,[],[3971,24])).
% 60.52/60.52 cnf(4134,plain,
% 60.52/60.52 (P2(a12,f8(x41341))),
% 60.52/60.52 inference(scs_inference,[],[4011,24])).
% 60.52/60.52 cnf(4136,plain,
% 60.52/60.52 (~P2(a12,f3(x41361,a12))),
% 60.52/60.52 inference(scs_inference,[],[3982,4011,3971,24,31])).
% 60.52/60.52 cnf(4143,plain,
% 60.52/60.52 (P4(f8(x41431),f8(x41431),f20(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[3982,4017,1048,3975,4011,3971,50,8,24,31,33,40])).
% 60.52/60.52 cnf(4150,plain,
% 60.52/60.52 (P2(f19(x41501,x41502),f4(x41501,x41502))),
% 60.52/60.52 inference(scs_inference,[],[10,24])).
% 60.52/60.52 cnf(4160,plain,
% 60.52/60.52 (P4(f8(x41601),f8(x41601),f17(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4143,4100,4125,3973,3965,3967,15,10,4,24,31,42,40])).
% 60.52/60.52 cnf(4168,plain,
% 60.52/60.52 (P2(f11(x41681,x41682),f10(x41681,x41682))),
% 60.52/60.52 inference(scs_inference,[],[9,24])).
% 60.52/60.52 cnf(4186,plain,
% 60.52/60.52 (P2(f8(x41861),f7(x41861))),
% 60.52/60.52 inference(scs_inference,[],[6,24])).
% 60.52/60.52 cnf(4188,plain,
% 60.52/60.52 (~P3(x41881,f7(x41882))),
% 60.52/60.52 inference(scs_inference,[],[3,6,24,30])).
% 60.52/60.52 cnf(4202,plain,
% 60.52/60.52 (P4(f1(x42021),f1(x42021),f17(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4160,4136,4088,4134,4017,79,4011,14,3971,8,3,6,44,24,30,31,39,28,40,41])).
% 60.52/60.52 cnf(4213,plain,
% 60.52/60.52 (P3(x42131,f3(x42132,x42131))),
% 60.52/60.52 inference(rename_variables,[],[8])).
% 60.52/60.52 cnf(4214,plain,
% 60.52/60.52 (~P3(x42141,f7(x42142))),
% 60.52/60.52 inference(rename_variables,[],[4188])).
% 60.52/60.52 cnf(4216,plain,
% 60.52/60.52 (~P2(f3(x42161,a12),f7(x42162))),
% 60.52/60.52 inference(scs_inference,[],[4186,4188,4214,4066,4134,4011,8,4213,3,9,22,31,34,33])).
% 60.52/60.52 cnf(4224,plain,
% 60.52/60.52 (P2(f7(x42241),a12)),
% 60.52/60.52 inference(scs_inference,[],[4186,4188,4214,4066,4160,4134,4017,4011,8,4213,3,9,22,31,34,33,40,19])).
% 60.52/60.52 cnf(4226,plain,
% 60.52/60.52 (P2(a12,f7(x42261))),
% 60.52/60.52 inference(scs_inference,[],[4186,4188,4214,4066,4160,4134,4017,4011,8,4213,3,9,22,31,34,33,40,19,24])).
% 60.52/60.52 cnf(4228,plain,
% 60.52/60.52 (P5(f7(x42281),f7(x42281),f18(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4186,4188,4214,4066,4080,4160,4106,4134,4017,4011,8,4213,3,9,6,22,31,34,33,40,19,24,43])).
% 60.52/60.52 cnf(4248,plain,
% 60.52/60.52 (~P2(f10(a12,a12),f9(x42481,a12))),
% 60.52/60.52 inference(scs_inference,[],[4033,4216,4224,4168,3979,3973,7,22,31,34])).
% 60.52/60.52 cnf(4252,plain,
% 60.52/60.52 (~P2(f9(x42521,x42522),f7(x42523))),
% 60.52/60.52 inference(scs_inference,[],[4033,4216,4224,4168,3979,4188,3973,4002,208,7,22,31,34,33])).
% 60.52/60.52 cnf(4254,plain,
% 60.52/60.52 (P2(x42541,f2(x42541))),
% 60.52/60.52 inference(rename_variables,[],[4002])).
% 60.52/60.52 cnf(4260,plain,
% 60.52/60.52 (P4(f7(x42601),a12,a12)),
% 60.52/60.52 inference(scs_inference,[],[4033,4216,4224,4168,3979,4188,4143,12,4125,4186,3973,3965,4002,4254,208,7,22,31,34,33,40,41])).
% 60.52/60.52 cnf(4265,plain,
% 60.52/60.52 (P5(f7(x42651),a12,a12)),
% 60.52/60.52 inference(scs_inference,[],[4033,4216,13,4224,4226,4168,3979,4188,4143,12,4125,4186,3973,3965,3975,4002,4254,208,7,22,31,34,33,40,41,43])).
% 60.52/60.52 cnf(4277,plain,
% 60.52/60.52 (~P2(f9(x42771,x42772),f8(x42773))),
% 60.52/60.52 inference(scs_inference,[],[4248,182,4002,208,9,31,33])).
% 60.52/60.52 cnf(4281,plain,
% 60.52/60.52 (P4(a12,f7(x42811),f7(x42811))),
% 60.52/60.52 inference(scs_inference,[],[4248,4260,4226,182,4224,4002,208,9,31,33,41])).
% 60.52/60.52 cnf(4284,plain,
% 60.52/60.52 (P5(a12,f7(x42841),f7(x42841))),
% 60.52/60.52 inference(scs_inference,[],[4248,4260,4265,4226,182,4224,4002,208,9,31,33,41,43])).
% 60.52/60.52 cnf(4294,plain,
% 60.52/60.52 (~P2(f16(x42941),f7(x42942))),
% 60.52/60.52 inference(scs_inference,[],[4252,4015,31])).
% 60.52/60.52 cnf(4307,plain,
% 60.52/60.52 (P4(f2(a12),a12,a12)),
% 60.52/60.52 inference(scs_inference,[],[4294,4281,4088,4002,4224,31,40])).
% 60.52/60.52 cnf(4313,plain,
% 60.52/60.52 (~P2(f16(x43131),f8(x43132))),
% 60.52/60.52 inference(scs_inference,[],[4277,4015,31])).
% 60.52/60.52 cnf(4331,plain,
% 60.52/60.52 (P5(f8(x43311),f8(x43311),f18(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4013,4313,1702,4150,4106,4088,15,4011,4,11,31,34,32,43])).
% 60.52/60.52 cnf(4338,plain,
% 60.52/60.52 (P5(a12,f1(x43381),f1(x43381))),
% 60.52/60.52 inference(scs_inference,[],[4265,4226,3965,678,3971,31,43])).
% 60.52/60.52 cnf(4341,plain,
% 60.52/60.52 (P4(a12,f2(a12),f2(a12))),
% 60.52/60.52 inference(scs_inference,[],[4307,4265,4226,3965,678,3971,4002,5,31,43,40])).
% 60.52/60.52 cnf(4345,plain,
% 60.52/60.52 (~P4(f1(x43451),f9(x43452,a12),f16(a12))),
% 60.52/60.52 inference(scs_inference,[],[1,4307,4265,4058,4226,3965,678,3971,4002,93,208,5,31,43,40,39])).
% 60.52/60.52 cnf(4346,plain,
% 60.52/60.52 (P3(f2(x43461),f9(x43462,x43461))),
% 60.52/60.52 inference(rename_variables,[],[208])).
% 60.52/60.52 cnf(4353,plain,
% 60.52/60.52 (~P1(f18(x43531,x43532))+~P3(x43533,f5(x43531,x43532))),
% 60.52/60.52 inference(scs_inference,[],[1,4307,4265,891,4058,4226,4106,3965,678,3971,4002,93,208,4346,5,4,31,43,40,39,33,30])).
% 60.52/60.52 cnf(4355,plain,
% 60.52/60.52 (~P2(a12,f9(x43551,x43552))),
% 60.52/60.52 inference(scs_inference,[],[4025,293,31])).
% 60.52/60.52 cnf(4358,plain,
% 60.52/60.52 (P5(f8(x43581),f8(x43582),f8(x43582))),
% 60.52/60.52 inference(scs_inference,[],[4025,4284,4186,4011,293,31,43])).
% 60.52/60.52 cnf(4367,plain,
% 60.52/60.52 (P5(f1(x43671),a12,a12)),
% 60.52/60.52 inference(scs_inference,[],[4025,4345,4284,4338,4202,4125,4186,4011,3971,293,4,31,43,287,40,42])).
% 60.52/60.52 cnf(4375,plain,
% 60.52/60.52 (P4(f8(x43751),a12,a12)),
% 60.52/60.52 inference(scs_inference,[],[4355,4341,4226,4011,4002,31,41])).
% 60.52/60.52 cnf(4378,plain,
% 60.52/60.52 (P5(a12,a12,a12)),
% 60.52/60.52 inference(scs_inference,[],[4358,4355,4341,4226,4011,4002,31,41,42])).
% 60.52/60.52 cnf(4382,plain,
% 60.52/60.52 (P5(f2(a12),f2(a12),f2(a12))),
% 60.52/60.52 inference(scs_inference,[],[4358,4355,4341,4226,4011,4002,31,41,42,225])).
% 60.52/60.52 cnf(4384,plain,
% 60.52/60.52 (P2(a12,f18(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4358,4355,4341,4226,4011,4002,31,41,42,225,38])).
% 60.52/60.52 cnf(4386,plain,
% 60.52/60.52 (P2(f18(a12,a12),a12)),
% 60.52/60.52 inference(scs_inference,[],[4358,4355,4341,4226,4011,4002,31,41,42,225,38,24])).
% 60.52/60.52 cnf(4392,plain,
% 60.52/60.52 (P5(f2(a12),f2(a12),a12)),
% 60.52/60.52 inference(scs_inference,[],[4382,3946])).
% 60.52/60.52 cnf(4403,plain,
% 60.52/60.52 (P4(f18(a12,a12),f18(a12,a12),f20(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4378,4090,4382,4384,50,4017,3967,44,3946,22,23,31,42,40])).
% 60.52/60.52 cnf(4407,plain,
% 60.52/60.52 (~P3(x44071,f5(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4378,4090,4382,4384,50,4017,3967,44,3946,22,23,31,42,40,4353])).
% 60.52/60.52 cnf(4409,plain,
% 60.52/60.52 (P2(f5(a12,a12),a12)),
% 60.52/60.52 inference(scs_inference,[],[4378,4090,4382,4384,50,4017,3967,44,3946,22,23,31,42,40,4353,19])).
% 60.52/60.52 cnf(4413,plain,
% 60.52/60.52 (P2(a12,f5(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4378,4090,4382,4384,50,4017,3967,44,3946,22,23,31,42,40,4353,19,28,24])).
% 60.52/60.52 cnf(4415,plain,
% 60.52/60.52 (~P2(f3(x44151,a12),f5(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4378,4090,4382,4384,50,4017,3967,8,44,3946,22,23,31,42,40,4353,19,28,24,33])).
% 60.52/60.52 cnf(4418,plain,
% 60.52/60.52 (P4(f18(a12,a12),a12,a12)),
% 60.52/60.52 inference(scs_inference,[],[4378,4090,4382,4384,4386,4281,50,4017,4226,3967,8,44,3946,22,23,31,42,40,4353,19,28,24,33,41])).
% 60.52/60.52 cnf(4426,plain,
% 60.52/60.52 (~P3(x44261,f5(a12,a12))),
% 60.52/60.52 inference(rename_variables,[],[4407])).
% 60.52/60.52 cnf(4429,plain,
% 60.52/60.52 (~P2(f9(x44291,x44292),f5(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4407,4426,4415,4409,3973,4002,208,8,31,34,33])).
% 60.52/60.52 cnf(4433,plain,
% 60.52/60.52 (~P3(x44331,f18(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4407,4426,4415,4409,3973,4384,4002,208,8,44,31,34,33,30])).
% 60.52/60.52 cnf(4439,plain,
% 60.52/60.52 (P3(x44391,f3(x44392,x44391))),
% 60.52/60.52 inference(rename_variables,[],[8])).
% 60.52/60.52 cnf(4440,plain,
% 60.52/60.52 (~P3(x44401,f18(a12,a12))),
% 60.52/60.52 inference(rename_variables,[],[4433])).
% 60.52/60.52 cnf(4446,plain,
% 60.52/60.52 (P4(a12,f18(a12,a12),f18(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4433,4440,4418,4413,4386,4384,8,4439,34,33,41])).
% 60.52/60.52 cnf(4448,plain,
% 60.52/60.52 (P5(f5(a12,a12),f5(a12,a12),f5(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4433,4440,4418,4413,4386,4378,4409,4384,8,4439,34,33,41,43])).
% 60.52/60.52 cnf(4450,plain,
% 60.52/60.52 (P4(a12,f5(a12,a12),f5(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4433,4440,4418,4413,4386,4378,4409,4384,8,4439,34,33,41,43,40])).
% 60.52/60.52 cnf(4453,plain,
% 60.52/60.52 (P3(f2(x44531),f9(x44532,x44531))),
% 60.52/60.52 inference(rename_variables,[],[208])).
% 60.52/60.52 cnf(4464,plain,
% 60.52/60.52 (P5(f5(a12,a12),f16(x44641),f19(a12,x44641))),
% 60.52/60.52 inference(scs_inference,[],[17,4407,4433,4409,4150,4088,14,4017,4002,208,4453,34,33,41,43])).
% 60.52/60.52 cnf(4469,plain,
% 60.52/60.52 (~P2(f16(x44691),f5(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4429,17,4407,4433,4409,4150,4088,4015,14,4017,4002,208,4453,34,33,41,43,31])).
% 60.52/60.52 cnf(4481,plain,
% 60.52/60.52 (~P2(f11(x44811,x44812),f5(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4469,4407,4088,3965,11,31,33])).
% 60.52/60.52 cnf(4493,plain,
% 60.52/60.52 (P5(a12,f9(x44931,x44932),f4(a12,x44932))),
% 60.52/60.52 inference(scs_inference,[],[4469,4228,4464,4407,4168,4409,4058,4150,4125,12,4088,3965,4186,4384,4002,11,31,33,43,41,42])).
% 60.52/60.52 cnf(4503,plain,
% 60.52/60.52 (~P2(f18(a12,a12),f3(x45031,x45032))),
% 60.52/60.52 inference(scs_inference,[],[4481,4433,4168,8,5,31,34])).
% 60.52/60.52 cnf(4504,plain,
% 60.52/60.52 (P2(f2(x45041),x45041)),
% 60.52/60.52 inference(rename_variables,[],[5])).
% 60.52/60.52 cnf(4505,plain,
% 60.52/60.52 (~P3(x45051,f18(a12,a12))),
% 60.52/60.52 inference(rename_variables,[],[4433])).
% 60.52/60.52 cnf(4507,plain,
% 60.52/60.52 (~P2(f3(x45071,x45072),f18(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4481,4433,4505,4168,4002,8,5,31,34,33])).
% 60.52/60.52 cnf(4518,plain,
% 60.52/60.52 (P4(f5(a12,a12),f5(a12,a12),f20(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4481,4446,4433,4505,3626,4413,4378,4168,4125,50,4017,3965,4002,8,5,4504,31,34,33,30,42,41,40])).
% 60.52/60.52 cnf(4525,plain,
% 60.52/60.52 (~P2(a12,f3(x45251,x45252))),
% 60.52/60.52 inference(scs_inference,[],[4503,4386,31])).
% 60.52/60.52 cnf(4529,plain,
% 60.52/60.52 (P3(f2(x45291),f9(x45292,x45291))),
% 60.52/60.52 inference(rename_variables,[],[208])).
% 60.52/60.52 cnf(4531,plain,
% 60.52/60.52 (~P2(f9(x45311,x45312),f2(a12))),
% 60.52/60.52 inference(scs_inference,[],[4503,182,129,4386,4002,208,4529,31,34,33])).
% 60.52/60.52 cnf(4543,plain,
% 60.52/60.52 (~P2(f7(x45431),f11(x45432,x45433))),
% 60.52/60.52 inference(scs_inference,[],[4507,4188,3973,4017,11,31,34])).
% 60.52/60.52 cnf(4544,plain,
% 60.52/60.52 (P3(f20(x45441,x45442),f11(x45441,x45442))),
% 60.52/60.52 inference(rename_variables,[],[11])).
% 60.52/60.52 cnf(4545,plain,
% 60.52/60.52 (~P3(x45451,f7(x45452))),
% 60.52/60.52 inference(rename_variables,[],[4188])).
% 60.52/60.52 cnf(4547,plain,
% 60.52/60.52 (~P2(f11(x45471,x45472),f7(x45473))),
% 60.52/60.52 inference(scs_inference,[],[4507,4188,4545,3973,4017,3965,11,4544,31,34,33])).
% 60.52/60.52 cnf(4556,plain,
% 60.52/60.52 (P4(f18(a12,a12),f18(a12,a12),f17(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4518,4507,4188,4545,3973,4017,3967,3965,47,11,4544,44,31,34,33,39,40])).
% 60.52/60.52 cnf(4562,plain,
% 60.52/60.52 (P5(f5(a12,a12),a12,f5(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4448,4525,4413,4,31,43])).
% 60.52/60.52 cnf(4570,plain,
% 60.52/60.52 (~P2(a12,f11(x45701,x45702))),
% 60.52/60.52 inference(scs_inference,[],[4543,4224,31])).
% 60.52/60.52 cnf(4573,plain,
% 60.52/60.52 (P5(a12,f5(a12,a12),a12)),
% 60.52/60.52 inference(scs_inference,[],[4543,4562,4413,4409,4224,31,43])).
% 60.52/60.52 cnf(4582,plain,
% 60.52/60.52 (P4(f5(a12,a12),a12,a12)),
% 60.52/60.52 inference(scs_inference,[],[4543,4562,4375,4450,4134,4413,4409,4186,4224,10,31,43,40,30,42,41])).
% 60.52/60.52 cnf(4592,plain,
% 60.52/60.52 (P5(f18(a12,a12),f16(x45921),f19(a12,x45921))),
% 60.52/60.52 inference(scs_inference,[],[4547,4493,4168,4150,4386,4058,31,43])).
% 60.52/60.52 cnf(4597,plain,
% 60.52/60.52 (P4(f18(a12,a12),f5(a12,a12),f20(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4547,4493,4556,4106,4168,4150,4386,4058,4017,4,31,43,40])).
% 60.52/60.52 cnf(4607,plain,
% 60.52/60.52 (P2(f18(x46071,x46072),f5(x46071,x46072))),
% 60.52/60.52 inference(rename_variables,[],[4106])).
% 60.52/60.52 cnf(4611,plain,
% 60.52/60.52 (P2(f18(x46111,x46112),f5(x46111,x46112))),
% 60.52/60.52 inference(rename_variables,[],[4106])).
% 60.52/60.52 cnf(4614,plain,
% 60.52/60.52 (P5(f5(a12,a12),f3(x46141,x46142),f4(a12,x46142))),
% 60.52/60.52 inference(scs_inference,[],[4597,4592,4531,4088,4015,4106,4607,4611,4150,4409,4384,3965,4017,31,41,40,42])).
% 60.52/60.52 cnf(4649,plain,
% 60.52/60.52 (P5(f7(x46491),f18(a12,a12),f7(x46491))),
% 60.52/60.52 inference(scs_inference,[],[4573,4226,3967,42])).
% 60.52/60.52 cnf(4657,plain,
% 60.52/60.52 (P5(a12,f18(a12,a12),f18(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4367,4125,4386,43])).
% 60.52/60.52 cnf(4661,plain,
% 60.52/60.52 (P5(f8(x46611),f5(a12,a12),f5(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4657,4106,4134,42])).
% 60.52/60.52 cnf(4665,plain,
% 60.52/60.52 (P5(f7(x46651),f7(x46651),a12)),
% 60.52/60.52 inference(scs_inference,[],[4657,4331,4106,4134,4384,6,42,43])).
% 60.52/60.52 cnf(4682,plain,
% 60.52/60.52 (~P2(f1(x46821),f9(x46822,x46823))),
% 60.52/60.52 inference(scs_inference,[],[4108,4355,3973,4150,4125,8,47,44,39,32,31])).
% 60.52/60.52 cnf(4710,plain,
% 60.52/60.52 (~P2(f5(a12,a12),f11(x47101,x47102))),
% 60.52/60.52 inference(scs_inference,[],[4570,4413,31])).
% 60.52/60.52 cnf(4712,plain,
% 60.52/60.52 (P5(a12,f16(x47121),f19(a12,x47121))),
% 60.52/60.52 inference(scs_inference,[],[4614,4570,4088,4150,4413,31,43])).
% 60.52/60.52 cnf(4728,plain,
% 60.52/60.52 (P5(a12,a12,f1(x47281))),
% 60.52/60.52 inference(scs_inference,[],[4392,2950,3971,3965,4002,31,43])).
% 60.52/60.52 cnf(4732,plain,
% 60.52/60.52 (P2(f1(x47321),f18(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4392,2950,3971,3965,4002,31,43,38])).
% 60.52/60.52 cnf(4734,plain,
% 60.52/60.52 (P2(f18(a12,a12),f1(x47341))),
% 60.52/60.52 inference(scs_inference,[],[4392,2950,3971,3965,4002,31,43,38,24])).
% 60.52/60.52 cnf(4739,plain,
% 60.52/60.52 (P2(f1(x47391),f18(a12,a12))),
% 60.52/60.52 inference(rename_variables,[],[4732])).
% 60.52/60.52 cnf(4741,plain,
% 60.52/60.52 (P4(f1(x47411),f18(a12,a12),f17(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4682,4732,4739,4403,4017,4,31,41])).
% 60.52/60.52 cnf(4745,plain,
% 60.52/60.52 (P5(a12,f1(x47451),a12)),
% 60.52/60.52 inference(scs_inference,[],[4649,4682,4732,4739,4734,4403,4224,4017,4,31,41,42])).
% 60.52/60.52 cnf(4748,plain,
% 60.52/60.52 (P5(f5(a12,a12),f5(a12,a12),f18(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4649,4682,4732,4739,4734,4728,4403,4409,4224,4017,4,31,41,42,43])).
% 60.52/60.52 cnf(4752,plain,
% 60.52/60.52 (~P2(f18(a12,a12),f11(x47521,x47522))),
% 60.52/60.52 inference(scs_inference,[],[4710,3967,31])).
% 60.52/60.52 cnf(4759,plain,
% 60.52/60.52 (P5(f18(a12,a12),f18(a12,a12),f1(x47591))),
% 60.52/60.52 inference(scs_inference,[],[4748,4734,3967,42])).
% 60.52/60.52 cnf(4764,plain,
% 60.52/60.52 (P5(f7(x47641),f9(x47642,x47643),f4(a12,x47643))),
% 60.52/60.52 inference(scs_inference,[],[4712,4058,4226,4150,42])).
% 60.52/60.52 cnf(4770,plain,
% 60.52/60.52 (P4(f18(a12,a12),f18(a12,a12),f18(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4582,4386,4106,41])).
% 60.52/60.52 cnf(4773,plain,
% 60.52/60.52 (P5(f1(x47731),f18(a12,a12),f1(x47731))),
% 60.52/60.52 inference(scs_inference,[],[4745,4582,4734,4386,4106,3971,41,43])).
% 60.52/60.52 cnf(4786,plain,
% 60.52/60.52 (P4(f5(a12,a12),f5(a12,a12),f5(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4773,4752,4770,4665,4732,4734,4134,4106,4224,41,43,31,42,40])).
% 60.52/60.52 cnf(4789,plain,
% 60.52/60.52 (P2(f8(x47891),f18(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4773,4752,4770,4665,4732,4734,4134,4106,4224,41,43,31,42,40,38])).
% 60.52/60.52 cnf(4791,plain,
% 60.52/60.52 (P2(f18(a12,a12),f8(x47911))),
% 60.52/60.52 inference(scs_inference,[],[4773,4752,4770,4665,4732,4734,4134,4106,4224,41,43,31,42,40,38,24])).
% 60.52/60.52 cnf(4794,plain,
% 60.52/60.52 (P2(f8(x47941),f18(a12,a12))),
% 60.52/60.52 inference(rename_variables,[],[4789])).
% 60.52/60.52 cnf(4796,plain,
% 60.52/60.52 (P4(f18(a12,a12),f8(x47961),f20(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4789,4794,4741,4375,4734,3975,3965,40,41])).
% 60.52/60.52 cnf(4800,plain,
% 60.52/60.52 (P5(f8(x48001),f18(a12,a12),f18(a12,a12))),
% 60.52/60.52 inference(scs_inference,[],[4759,4789,4794,4741,4375,4734,3975,3965,4,40,41,43])).
% 60.52/60.52 cnf(4819,plain,
% 60.52/60.52 (P2(f18(a12,a12),f8(x48191))),
% 60.52/60.52 inference(rename_variables,[],[4791])).
% 60.52/60.52 cnf(4824,plain,
% 60.52/60.52 (P4(f8(x48241),f8(x48241),f8(x48241))),
% 60.52/60.52 inference(scs_inference,[],[4661,4800,4789,4770,4791,4819,4413,43,42,41])).
% 60.52/60.52 cnf(4843,plain,
% 60.52/60.52 ($false),
% 60.52/60.52 inference(scs_inference,[],[4824,4764,4121,4786,4796,4789,4791,4058,4409,4186,4150,4017,261,40,43,41,227,37,24]),
% 60.52/60.52 ['proof']).
% 60.52/60.52 % SZS output end Proof
% 60.52/60.52 % Total time :59.840000s
%------------------------------------------------------------------------------