%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : NUN059+1 : TPTP v8.2.0. Bugfixed v7.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n028.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:35 EDT 2024
% Result : Theorem 58.73s 58.82s
% Output : CNFRefutation 58.76s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : NUN059+1 : TPTP v8.2.0. Bugfixed v7.4.0.
% 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.12/0.33 % Computer : n028.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:08:54 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.56/0.60 start to proof:theBenchmark
% 58.73/58.81 %-------------------------------------------
% 58.73/58.81 % File :CSE---1.7
% 58.73/58.81 % Problem :theBenchmark
% 58.73/58.81 % Transform :cnf
% 58.73/58.81 % Format :tptp:raw
% 58.73/58.81 % Command :java -jar mcs_scs.jar %d %s
% 58.73/58.81
% 58.73/58.81 % Result :Theorem 58.110000s
% 58.73/58.81 % Output :CNFRefutation 58.110000s
% 58.73/58.81 %-------------------------------------------
% 58.73/58.82 %------------------------------------------------------------------------------
% 58.73/58.82 % File : NUN059+1 : TPTP v8.2.0. Bugfixed v7.4.0.
% 58.73/58.82 % Domain : Number Theory
% 58.73/58.82 % Problem : Robinson arithmetic: There exists X^2 + Y^2 = Z^2
% 58.73/58.82 % Version : Especial.
% 58.73/58.82 % English :
% 58.73/58.82
% 58.73/58.82 % Refs : [BBJ03] Boolos et al. (2003), Computability and Logic
% 58.73/58.82 % : [Smi07] Smith (2007), An Introduction to Goedel's Theorems
% 58.73/58.82 % : [Lam18] Lampert (2018), Email to Geoff Sutcliffe
% 58.73/58.82 % Source : [Lam18]
% 58.73/58.82 % Names : fermattothepoweroftwoid [Lam18]
% 58.73/58.82
% 58.73/58.82 % Status : Theorem
% 58.73/58.82 % Rating : 0.12 v8.2.0, 0.20 v8.1.0, 0.50 v7.5.0, 0.86 v7.4.0
% 58.73/58.82 % Syntax : Number of formulae : 19 ( 1 unt; 0 def)
% 58.73/58.82 % Number of atoms : 80 ( 0 equ)
% 58.73/58.82 % Maximal formula atoms : 7 ( 4 avg)
% 58.73/58.82 % Number of connectives : 95 ( 34 ~; 26 |; 35 &)
% 58.73/58.82 % ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% 58.73/58.82 % Maximal formula depth : 13 ( 8 avg)
% 58.73/58.82 % Maximal term depth : 1 ( 1 avg)
% 58.73/58.82 % Number of predicates : 5 ( 5 usr; 0 prp; 1-3 aty)
% 58.73/58.82 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 58.73/58.82 % Number of variables : 74 ( 47 !; 27 ?)
% 58.73/58.82 % SPC : FOF_THM_RFO_NEQ
% 58.73/58.82
% 58.73/58.82 % Comments : Translated to FOL without equality.
% 58.73/58.82 % Bugfixes : v7.4.0 - Bugfixes in formulae's use if the r1/3 predicate.
% 58.73/58.82 %------------------------------------------------------------------------------
% 58.73/58.82 include('Axioms/NUM009+0.ax').
% 58.73/58.82 %------------------------------------------------------------------------------
% 58.73/58.82 fof(fermattothepoweroftwoid,conjecture,
% 58.73/58.82 ? [Y1,Y3,Y2,Y4] :
% 58.73/58.82 ( ? [Y5] :
% 58.73/58.82 ( id(Y4,Y5)
% 58.73/58.82 & r4(Y2,Y2,Y5) )
% 58.73/58.82 & ? [Y6] :
% 58.73/58.82 ( r4(Y3,Y3,Y6)
% 58.73/58.82 & ? [Y7] :
% 58.73/58.82 ( r4(Y1,Y1,Y7)
% 58.73/58.82 & r3(Y7,Y6,Y4) ) ) ) ).
% 58.73/58.82
% 58.73/58.82 %------------------------------------------------------------------------------
% 58.73/58.82 %-------------------------------------------
% 58.73/58.82 % Proof found
% 58.73/58.82 % SZS status Theorem for theBenchmark
% 58.73/58.82 % SZS output start Proof
% 58.76/58.83 %ClaNum:43(EqnAxiom:0)
% 58.76/58.83 %VarNum:215(SingletonVarNum:105)
% 58.76/58.83 %MaxLitNum:5
% 58.76/58.83 %MaxfuncDepth:1
% 58.76/58.83 %SharedTerms:1
% 58.76/58.83 %goalClause: 43
% 58.76/58.83 [4]P2(x41,x41)
% 58.76/58.83 [1]P1(f1(x11))
% 58.76/58.83 [2]P1(f6(x21))
% 58.76/58.83 [3]P1(f8(x31))
% 58.76/58.83 [5]P2(f2(x51),x51)
% 58.76/58.83 [6]P2(f7(x61),f8(x61))
% 58.76/58.83 [12]P4(x121,f1(x121),f2(x121))
% 58.76/58.83 [13]P5(x131,f6(x131),f7(x131))
% 58.76/58.83 [7]P3(x71,f9(x72,x71))
% 58.76/58.83 [8]P3(x81,f3(x82,x81))
% 58.76/58.83 [9]P2(f10(x91,x92),f11(x91,x92))
% 58.76/58.83 [10]P2(f4(x101,x102),f19(x101,x102))
% 58.76/58.83 [11]P3(f20(x111,x112),f11(x111,x112))
% 58.76/58.83 [14]P4(x141,x142,f20(x141,x142))
% 58.76/58.83 [15]P5(x151,x152,f5(x151,x152))
% 58.76/58.83 [16]P4(x161,f9(x161,x162),f10(x161,x162))
% 58.76/58.83 [17]P5(x171,f3(x171,x172),f4(x171,x172))
% 58.76/58.83 [18]P4(f5(x181,x182),x181,f19(x181,x182))
% 58.76/58.83 [19]~P1(x191)+P2(x191,a12)
% 58.76/58.83 [20]P1(x201)+~P2(x201,a12)
% 58.76/58.83 [21]P2(x211,f15(x211))+P1(f13(x211))
% 58.76/58.83 [25]P3(f14(x251),f15(x251))+P1(f13(x251))
% 58.76/58.83 [26]P2(x261,f15(x261))+P2(x261,f13(x261))
% 58.76/58.83 [29]P3(f14(x291),f15(x291))+P2(x291,f13(x291))
% 58.76/58.83 [24]~P2(x242,x241)+P2(x241,x242)
% 58.76/58.83 [27]~P3(x272,x271)+P2(x271,f16(x272))
% 58.76/58.83 [28]P3(x281,x282)+~P2(x282,f16(x281))
% 58.76/58.83 [35]P4(x351,x352,x353)+~P2(x353,f17(x351,x352))
% 58.76/58.83 [36]P5(x361,x362,x363)+~P2(x363,f18(x361,x362))
% 58.76/58.83 [37]~P4(x372,x373,x371)+P2(x371,f17(x372,x373))
% 58.76/58.83 [38]~P5(x382,x383,x381)+P2(x381,f18(x382,x383))
% 58.76/58.83 [22]~P2(x222,x221)+P1(x221)+~P1(x222)
% 58.76/58.83 [23]~P2(x231,x232)+P1(x231)+~P1(x232)
% 58.76/58.83 [30]~P1(x301)+~P2(x301,x302)+~P3(x303,x302)
% 58.76/58.83 [31]~P2(x311,x313)+P2(x311,x312)+~P2(x313,x312)
% 58.76/58.83 [32]~P3(x322,x324)+~P3(x321,x323)+P2(x321,x322)+~P2(x323,x324)
% 58.76/58.83 [33]~P3(x334,x333)+P3(x331,x332)+~P2(x333,x332)+~P2(x334,x331)
% 58.76/58.83 [34]~P3(x344,x343)+P3(x341,x342)+~P2(x342,x343)+~P2(x341,x344)
% 58.76/58.83 [39]~P4(x396,x395,x394)+P4(x391,x392,x393)+~P2(x394,x393)+~P2(x395,x392)+~P2(x396,x391)
% 58.76/58.83 [40]~P4(x406,x405,x404)+P4(x401,x402,x403)+~P2(x403,x404)+~P2(x402,x405)+~P2(x401,x406)
% 58.76/58.83 [41]~P5(x416,x415,x414)+P5(x411,x412,x413)+~P2(x414,x413)+~P2(x415,x412)+~P2(x416,x411)
% 58.76/58.83 [42]~P5(x426,x425,x424)+P5(x421,x422,x423)+~P2(x423,x424)+~P2(x422,x425)+~P2(x421,x426)
% 58.76/58.83 [43]~P2(x431,x432)+~P4(x433,x434,x431)+~P5(x435,x435,x433)+~P5(x436,x436,x434)+~P5(x437,x437,x432)
% 58.76/58.83 %EqnAxiom
% 58.76/58.83
% 58.76/58.83 %-------------------------------------------
% 58.76/58.85 cnf(44,plain,
% 58.76/58.85 (P1(a12)),
% 58.76/58.85 inference(scs_inference,[],[4,20])).
% 58.76/58.85 cnf(45,plain,
% 58.76/58.85 (P2(x451,x451)),
% 58.76/58.85 inference(rename_variables,[],[4])).
% 58.76/58.85 cnf(47,plain,
% 58.76/58.85 (P3(x471,f16(x471))),
% 58.76/58.85 inference(scs_inference,[],[4,45,20,28])).
% 58.76/58.85 cnf(48,plain,
% 58.76/58.85 (P2(x481,x481)),
% 58.76/58.85 inference(rename_variables,[],[4])).
% 58.76/58.85 cnf(51,plain,
% 58.76/58.85 (P2(x511,x511)),
% 58.76/58.85 inference(rename_variables,[],[4])).
% 58.76/58.85 cnf(53,plain,
% 58.76/58.85 (P5(x531,x532,f18(x531,x532))),
% 58.76/58.85 inference(scs_inference,[],[4,45,48,51,20,28,35,36])).
% 58.76/58.85 cnf(54,plain,
% 58.76/58.85 (P2(x541,x541)),
% 58.76/58.85 inference(rename_variables,[],[4])).
% 58.76/58.85 cnf(56,plain,
% 58.76/58.85 (~P3(x561,f1(x562))),
% 58.76/58.85 inference(scs_inference,[],[1,4,45,48,51,54,20,28,35,36,30])).
% 58.76/58.85 cnf(88,plain,
% 58.76/58.85 (P1(f2(a12))),
% 58.76/58.85 inference(scs_inference,[],[5,20])).
% 58.76/58.85 cnf(89,plain,
% 58.76/58.85 (P2(f2(x891),x891)),
% 58.76/58.85 inference(rename_variables,[],[5])).
% 58.76/58.85 cnf(92,plain,
% 58.76/58.85 (P2(f2(x921),x921)),
% 58.76/58.85 inference(rename_variables,[],[5])).
% 58.76/58.85 cnf(94,plain,
% 58.76/58.85 (P3(x941,f2(f16(x941)))),
% 58.76/58.85 inference(scs_inference,[],[5,89,92,20,35,28])).
% 58.76/58.85 cnf(95,plain,
% 58.76/58.85 (P2(f2(x951),x951)),
% 58.76/58.85 inference(rename_variables,[],[5])).
% 58.76/58.85 cnf(97,plain,
% 58.76/58.85 (P5(x971,x972,f2(f18(x971,x972)))),
% 58.76/58.85 inference(scs_inference,[],[5,89,92,95,20,35,28,36])).
% 58.76/58.85 cnf(100,plain,
% 58.76/58.85 (~P3(x1001,a12)),
% 58.76/58.85 inference(scs_inference,[],[4,5,89,92,95,44,20,35,28,36,30])).
% 58.76/58.85 cnf(125,plain,
% 58.76/58.85 (~P3(x1251,f2(a12))),
% 58.76/58.85 inference(scs_inference,[],[4,88,30])).
% 58.76/58.85 cnf(142,plain,
% 58.76/58.85 (~P3(x1421,f6(x1422))),
% 58.76/58.85 inference(scs_inference,[],[4,2,30])).
% 58.76/58.85 cnf(165,plain,
% 58.76/58.85 (~P3(x1651,f8(x1652))),
% 58.76/58.85 inference(scs_inference,[],[4,3,30])).
% 58.76/58.85 cnf(253,plain,
% 58.76/58.85 (P2(f6(x2531),a12)),
% 58.76/58.85 inference(scs_inference,[],[2,4,19,22])).
% 58.76/58.85 cnf(254,plain,
% 58.76/58.85 (~P5(a12,a12,a12)+P5(f6(x2541),f6(x2541),f6(x2541))),
% 58.76/58.85 inference(scs_inference,[],[253,42])).
% 58.76/58.85 cnf(263,plain,
% 58.76/58.85 (P2(a12,f6(x2631))),
% 58.76/58.85 inference(scs_inference,[],[2,24,19])).
% 58.76/58.85 cnf(264,plain,
% 58.76/58.85 (~P5(f6(x2641),f6(x2641),f6(x2641))+P5(a12,a12,a12)),
% 58.76/58.85 inference(scs_inference,[],[263,42])).
% 58.76/58.85 cnf(310,plain,
% 58.76/58.85 (P2(f2(f4(x3101,x3102)),f19(x3101,x3102))),
% 58.76/58.85 inference(scs_inference,[],[5,10,31])).
% 58.76/58.85 cnf(311,plain,
% 58.76/58.85 (P2(f2(x3111),x3111)),
% 58.76/58.85 inference(rename_variables,[],[5])).
% 58.76/58.85 cnf(313,plain,
% 58.76/58.85 (P3(f2(x3131),f16(x3131))),
% 58.76/58.85 inference(scs_inference,[],[5,311,4,10,47,31,34])).
% 58.76/58.85 cnf(314,plain,
% 58.76/58.85 (P2(x3141,x3141)),
% 58.76/58.85 inference(rename_variables,[],[4])).
% 58.76/58.85 cnf(315,plain,
% 58.76/58.85 (P2(f2(x3151),x3151)),
% 58.76/58.85 inference(rename_variables,[],[5])).
% 58.76/58.85 cnf(317,plain,
% 58.76/58.85 (P3(x3171,f16(f2(x3171)))),
% 58.76/58.85 inference(scs_inference,[],[5,311,315,4,314,10,47,31,34,33])).
% 58.76/58.85 cnf(318,plain,
% 58.76/58.85 (P2(x3181,x3181)),
% 58.76/58.85 inference(rename_variables,[],[4])).
% 58.76/58.85 cnf(321,plain,
% 58.76/58.85 (P5(f2(x3211),f2(x3211),f2(f18(x3211,x3211)))),
% 58.76/58.85 inference(scs_inference,[],[5,311,315,4,314,318,10,97,47,31,34,33,42])).
% 58.76/58.85 cnf(345,plain,
% 58.76/58.85 (P2(f2(x3451),x3451)),
% 58.76/58.85 inference(rename_variables,[],[5])).
% 58.76/58.85 cnf(349,plain,
% 58.76/58.85 (P2(f2(x3491),x3491)),
% 58.76/58.85 inference(rename_variables,[],[5])).
% 58.76/58.85 cnf(353,plain,
% 58.76/58.85 (~P5(f6(x3531),f6(x3531),f6(x3531))+P5(f2(a12),f2(a12),f2(a12))),
% 58.76/58.85 inference(scs_inference,[],[5,345,349,4,9,253,313,31,34,42,41])).
% 58.76/58.85 cnf(367,plain,
% 58.76/58.85 (P2(f2(f6(x3671)),a12)),
% 58.76/58.85 inference(scs_inference,[],[5,253,31])).
% 58.76/58.85 cnf(368,plain,
% 58.76/58.85 (P2(f2(x3681),x3681)),
% 58.76/58.85 inference(rename_variables,[],[5])).
% 58.76/58.85 cnf(372,plain,
% 58.76/58.85 (~P4(x3721,x3721,x3721)+P4(f2(x3721),f2(x3721),f2(x3721))),
% 58.76/58.85 inference(scs_inference,[],[5,368,253,31,20,40])).
% 58.76/58.85 cnf(388,plain,
% 58.76/58.85 (P2(f2(a12),f6(x3881))),
% 58.76/58.85 inference(scs_inference,[],[5,263,31])).
% 58.76/58.85 cnf(405,plain,
% 58.76/58.85 (P2(f2(f2(a12)),f6(x4051))),
% 58.76/58.85 inference(scs_inference,[],[5,388,31])).
% 58.76/58.85 cnf(410,plain,
% 58.76/58.85 (~P5(f6(x4101),f6(x4101),f6(x4101))+P5(f6(x4102),f6(x4102),f6(x4102))),
% 58.76/58.85 inference(scs_inference,[],[5,388,31,41,353])).
% 58.76/58.85 cnf(888,plain,
% 58.76/58.85 (P3(x8881,f2(f9(x8882,x8881)))),
% 58.76/58.85 inference(scs_inference,[],[7,4,5,34])).
% 58.76/58.85 cnf(889,plain,
% 58.76/58.85 (P2(f2(x8891),x8891)),
% 58.76/58.85 inference(rename_variables,[],[5])).
% 58.76/58.85 cnf(890,plain,
% 58.76/58.85 (P2(x8901,x8901)),
% 58.76/58.85 inference(rename_variables,[],[4])).
% 58.76/58.85 cnf(892,plain,
% 58.76/58.85 (P5(f2(x8921),f2(x8921),f18(x8921,x8921))),
% 58.76/58.85 inference(scs_inference,[],[7,4,890,5,889,321,34,41])).
% 58.76/58.85 cnf(908,plain,
% 58.76/58.85 (P5(f6(x9081),f6(x9081),f6(x9081))+~P2(a12,f18(a12,a12))),
% 58.76/58.85 inference(scs_inference,[],[254,36])).
% 58.76/58.85 cnf(941,plain,
% 58.76/58.85 (P3(x9411,f2(f3(x9412,x9411)))),
% 58.76/58.85 inference(scs_inference,[],[8,4,5,34])).
% 58.76/58.85 cnf(964,plain,
% 58.76/58.85 (~P4(f18(x9641,x9641),f18(x9641,x9641),f18(x9641,x9641))),
% 58.76/58.85 inference(scs_inference,[],[4,321,372,43])).
% 58.76/58.85 cnf(1092,plain,
% 58.76/58.85 (P5(f6(x10921),f6(x10921),f6(x10921))+~P2(f6(x10922),f18(f6(x10922),f6(x10922)))),
% 58.76/58.85 inference(scs_inference,[],[410,36])).
% 58.76/58.85 cnf(1113,plain,
% 58.76/58.85 (P2(f6(x11131),f6(x11132))),
% 58.76/58.85 inference(scs_inference,[],[253,263,31])).
% 58.76/58.85 cnf(1175,plain,
% 58.76/58.85 (P3(f2(x11751),f2(f16(x11751)))),
% 58.76/58.85 inference(scs_inference,[],[313,4,5,34])).
% 58.76/58.85 cnf(1221,plain,
% 58.76/58.85 (P2(f2(f2(a12)),a12)),
% 58.76/58.85 inference(scs_inference,[],[405,253,31])).
% 58.76/58.85 cnf(1245,plain,
% 58.76/58.85 (~P5(x12451,x12451,f1(f18(x12452,x12452)))),
% 58.76/58.85 inference(scs_inference,[],[892,5,12,43])).
% 58.76/58.85 cnf(1388,plain,
% 58.76/58.85 (P3(f6(x13881),f9(x13882,a12))),
% 58.76/58.85 inference(scs_inference,[],[263,5,888,33])).
% 58.76/58.85 cnf(1393,plain,
% 58.76/58.85 (P3(f6(x13931),f3(x13932,a12))),
% 58.76/58.85 inference(scs_inference,[],[263,5,941,33])).
% 58.76/58.85 cnf(1408,plain,
% 58.76/58.85 (P3(f2(a12),f9(x14081,a12))),
% 58.76/58.85 inference(scs_inference,[],[388,4,1388,34])).
% 58.76/58.85 cnf(1412,plain,
% 58.76/58.85 (P3(f2(a12),f3(x14121,a12))),
% 58.76/58.85 inference(scs_inference,[],[388,4,1393,34])).
% 58.76/58.85 cnf(1424,plain,
% 58.76/58.85 (P2(a12,f1(x14241))),
% 58.76/58.85 inference(scs_inference,[],[1,19,24])).
% 58.76/58.85 cnf(1426,plain,
% 58.76/58.85 (P2(a12,f1(x14261))),
% 58.76/58.85 inference(rename_variables,[],[1424])).
% 58.76/58.85 cnf(1429,plain,
% 58.76/58.85 (~P5(f6(x14291),f6(x14291),f6(x14291))),
% 58.76/58.85 inference(scs_inference,[],[1245,1424,41,264])).
% 58.76/58.85 cnf(1436,plain,
% 58.76/58.85 (~P2(f18(f6(x14361),f6(x14361)),f6(x14361))),
% 58.76/58.85 inference(scs_inference,[],[1245,1424,1426,41,264,1092,42,40,24])).
% 58.76/58.85 cnf(1439,plain,
% 58.76/58.85 (~P5(f2(a12),f2(a12),f2(a12))),
% 58.76/58.85 inference(scs_inference,[],[388,1429,41])).
% 58.76/58.85 cnf(1485,plain,
% 58.76/58.85 (P2(f2(f2(a12)),f1(x14851))),
% 58.76/58.85 inference(scs_inference,[],[1221,1424,31])).
% 58.76/58.85 cnf(1520,plain,
% 58.76/58.85 (~P2(f18(a12,a12),a12)),
% 58.76/58.85 inference(scs_inference,[],[1429,24,908])).
% 58.76/58.85 cnf(1521,plain,
% 58.76/58.85 (~P1(f18(a12,a12))),
% 58.76/58.85 inference(scs_inference,[],[1520,19])).
% 58.76/58.85 cnf(1523,plain,
% 58.76/58.85 (~P2(a12,f18(a12,a12))),
% 58.76/58.85 inference(scs_inference,[],[1520,19,24])).
% 58.76/58.85 cnf(1534,plain,
% 58.76/58.85 (P2(f16(f2(a12)),f9(x15341,a12))),
% 58.76/58.85 inference(scs_inference,[],[1408,24,27])).
% 58.76/58.85 cnf(1551,plain,
% 58.76/58.85 (P2(f16(f2(a12)),f3(x15511,a12))),
% 58.76/58.85 inference(scs_inference,[],[1412,24,27])).
% 58.76/58.85 cnf(1583,plain,
% 58.76/58.85 (P3(f1(x15831),f16(a12))),
% 58.76/58.85 inference(scs_inference,[],[1424,5,94,33])).
% 58.76/58.85 cnf(1593,plain,
% 58.76/58.85 (P3(f1(x15931),f3(x15932,a12))),
% 58.76/58.85 inference(scs_inference,[],[1424,5,941,33])).
% 58.76/58.85 cnf(1623,plain,
% 58.76/58.85 (P3(f1(x16231),f16(f2(a12)))),
% 58.76/58.85 inference(scs_inference,[],[1485,5,1175,33])).
% 58.76/58.85 cnf(1654,plain,
% 58.76/58.85 (~P1(f9(x16541,a12))),
% 58.76/58.85 inference(scs_inference,[],[1534,1623,24,30])).
% 58.76/58.85 cnf(1655,plain,
% 58.76/58.85 (~P1(f16(f2(a12)))),
% 58.76/58.85 inference(scs_inference,[],[1534,1654,22])).
% 58.76/58.85 cnf(1658,plain,
% 58.76/58.85 (~P3(f18(a12,a12),f9(x16581,a12))),
% 58.76/58.85 inference(scs_inference,[],[1534,1523,1654,317,22,32])).
% 58.76/58.85 cnf(1685,plain,
% 58.76/58.85 (~P1(f3(x16851,a12))),
% 58.76/58.85 inference(scs_inference,[],[1551,1655,24,22])).
% 58.76/58.85 cnf(1780,plain,
% 58.76/58.85 (P2(f2(x17801),x17801)),
% 58.76/58.85 inference(rename_variables,[],[5])).
% 58.76/58.85 cnf(1782,plain,
% 58.76/58.85 (P2(f2(a12),f1(x17821))),
% 58.76/58.85 inference(scs_inference,[],[5,1780,1424,1521,22,31])).
% 58.76/58.85 cnf(1988,plain,
% 58.76/58.85 (P2(f6(x19881),f1(x19882))),
% 58.76/58.85 inference(scs_inference,[],[253,1424,31])).
% 58.76/58.85 cnf(2041,plain,
% 58.76/58.85 (~P2(f18(a12,a12),f6(x20411))),
% 58.76/58.85 inference(scs_inference,[],[253,1520,31])).
% 58.76/58.85 cnf(2047,plain,
% 58.76/58.85 (~P5(a12,a12,f6(x20471))),
% 58.76/58.85 inference(scs_inference,[],[310,253,1520,31,24,32,38])).
% 58.76/58.85 cnf(2053,plain,
% 58.76/58.85 (~P2(f6(x20531),f18(f6(x20532),f6(x20532)))),
% 58.76/58.85 inference(scs_inference,[],[1113,1436,31,24])).
% 58.76/58.85 cnf(2065,plain,
% 58.76/58.85 (~P5(a12,a12,f2(a12))),
% 58.76/58.85 inference(scs_inference,[],[310,5,1520,2053,31,24,32,38])).
% 58.76/58.85 cnf(2067,plain,
% 58.76/58.85 (~P2(f18(a12,a12),f2(f6(x20671)))),
% 58.76/58.85 inference(scs_inference,[],[1520,367,31])).
% 58.76/58.85 cnf(2082,plain,
% 58.76/58.85 (~P5(a12,a12,f2(f2(a12)))),
% 58.76/58.85 inference(scs_inference,[],[310,1520,1221,2067,31,24,32,38])).
% 58.76/58.85 cnf(2208,plain,
% 58.76/58.85 (~P5(f1(x22081),f1(x22081),f6(x22082))),
% 58.76/58.85 inference(scs_inference,[],[1424,388,2065,42])).
% 58.76/58.85 cnf(2211,plain,
% 58.76/58.85 (~P5(f1(x22111),f1(x22111),a12)),
% 58.76/58.85 inference(scs_inference,[],[1424,253,2047,42])).
% 58.76/58.85 cnf(2215,plain,
% 58.76/58.85 (~P5(f1(x22151),f1(x22151),f2(a12))),
% 58.76/58.85 inference(scs_inference,[],[1424,5,2082,42])).
% 58.76/58.85 cnf(2386,plain,
% 58.76/58.85 (~P2(f1(x23861),x23862)+~P2(f1(x23861),x23863)+~P5(x23862,x23863,f6(x23864))),
% 58.76/58.85 inference(scs_inference,[],[2208,4,42])).
% 58.76/58.85 cnf(2387,plain,
% 58.76/58.85 (~P5(a12,f1(x23871),f6(x23872))),
% 58.76/58.85 inference(scs_inference,[],[4,1,2386,19])).
% 58.76/58.85 cnf(2616,plain,
% 58.76/58.85 (~P2(f1(x26161),x26162)+~P2(f1(x26161),x26163)+~P5(x26162,x26163,a12)),
% 58.76/58.85 inference(scs_inference,[],[2211,4,42])).
% 58.76/58.85 cnf(2651,plain,
% 58.76/58.85 (~P5(a12,f1(x26511),a12)),
% 58.76/58.85 inference(scs_inference,[],[4,1,2616,19])).
% 58.76/58.85 cnf(2846,plain,
% 58.76/58.85 (~P2(f1(x28461),x28462)+~P2(f1(x28461),x28463)+~P5(x28462,x28463,f2(a12))),
% 58.76/58.85 inference(scs_inference,[],[2215,4,42])).
% 58.76/58.85 cnf(2928,plain,
% 58.76/58.85 (~P5(a12,f1(x29281),f2(a12))),
% 58.76/58.85 inference(scs_inference,[],[4,1,2846,19])).
% 58.76/58.85 cnf(3105,plain,
% 58.76/58.85 (~P5(f1(x31051),f1(x31052),a12)),
% 58.76/58.85 inference(scs_inference,[],[2387,4,253,1424,42])).
% 58.76/58.85 cnf(3116,plain,
% 58.76/58.85 (~P2(f1(x31161),x31162)+~P5(a12,x31162,a12)),
% 58.76/58.85 inference(scs_inference,[],[2651,4,42])).
% 58.76/58.85 cnf(3143,plain,
% 58.76/58.85 (~P5(f1(x31431),f1(x31432),f1(x31433))),
% 58.76/58.85 inference(scs_inference,[],[2928,4,1782,1424,42])).
% 58.76/58.85 cnf(3377,plain,
% 58.76/58.85 (~P2(f1(x33771),x33772)+~P2(f1(x33773),x33774)+~P5(x33772,x33774,a12)),
% 58.76/58.85 inference(scs_inference,[],[3105,4,42])).
% 58.76/58.85 cnf(4264,plain,
% 58.76/58.85 (~P5(f2(a12),a12,f2(a12))),
% 58.76/58.85 inference(scs_inference,[],[5,4,1439,42])).
% 58.76/58.85 cnf(4290,plain,
% 58.76/58.85 (P2(f9(x42901,x42902),f16(x42902))),
% 58.76/58.85 inference(scs_inference,[],[7,27])).
% 58.76/58.85 cnf(4292,plain,
% 58.76/58.85 (P2(f1(x42921),a12)),
% 58.76/58.85 inference(scs_inference,[],[1,7,27,19])).
% 58.76/58.85 cnf(4294,plain,
% 58.76/58.85 (P2(f20(x42941,x42942),f17(x42941,x42942))),
% 58.76/58.85 inference(scs_inference,[],[1,14,7,27,19,37])).
% 58.76/58.85 cnf(4296,plain,
% 58.76/58.85 (P2(f5(x42961,x42962),f18(x42961,x42962))),
% 58.76/58.85 inference(scs_inference,[],[1,14,7,15,27,19,37,38])).
% 58.76/58.85 cnf(4300,plain,
% 58.76/58.85 (~P2(f3(x43001,a12),a12)),
% 58.76/58.85 inference(scs_inference,[],[1,1685,14,100,7,15,27,19,37,38,28,20])).
% 58.76/58.85 cnf(4302,plain,
% 58.76/58.85 (P2(f1(x43021),f2(a12))),
% 58.76/58.85 inference(scs_inference,[],[1,1685,14,100,1782,7,15,27,19,37,38,28,20,24])).
% 58.76/58.85 cnf(4305,plain,
% 58.76/58.85 (P2(x43051,x43051)),
% 58.76/58.85 inference(rename_variables,[],[4])).
% 58.76/58.85 cnf(4308,plain,
% 58.76/58.85 (P2(x43081,x43081)),
% 58.76/58.85 inference(rename_variables,[],[4])).
% 58.76/58.85 cnf(4316,plain,
% 58.76/58.86 (P5(x43161,f6(x43161),f7(x43161))),
% 58.76/58.86 inference(rename_variables,[],[13])).
% 58.76/58.86 cnf(4327,plain,
% 58.76/58.86 (~P2(f8(a12),f1(x43271))),
% 58.76/58.86 inference(scs_inference,[],[1,3143,4264,13,4316,1685,14,100,1782,1988,7,1424,15,5,263,6,4,4305,4308,27,19,37,38,28,20,24,2846,3377,39,42,41,3116,31])).
% 58.76/58.86 cnf(4336,plain,
% 58.76/58.86 (~P1(f10(x43361,x43362))),
% 58.76/58.86 inference(scs_inference,[],[1,3143,4264,13,4316,1658,1685,14,100,56,1583,11,1782,1988,7,1424,15,5,9,263,6,4,4305,4308,27,19,37,38,28,20,24,2846,3377,39,42,41,3116,31,34,33,30])).
% 58.76/58.86 cnf(4337,plain,
% 58.76/58.86 (P2(f10(x43371,x43372),f11(x43371,x43372))),
% 58.76/58.86 inference(rename_variables,[],[9])).
% 58.76/58.86 cnf(4339,plain,
% 58.76/58.86 (~P1(f11(x43391,x43392))),
% 58.76/58.86 inference(scs_inference,[],[1,3143,4264,13,4316,1658,1685,14,100,56,1583,11,1782,1988,7,1424,15,5,9,4337,263,6,4,4305,4308,27,19,37,38,28,20,24,2846,3377,39,42,41,3116,31,34,33,30,23])).
% 58.76/58.86 cnf(4344,plain,
% 58.76/58.86 (P2(f3(x43441,x43442),f16(x43442))),
% 58.76/58.86 inference(scs_inference,[],[8,27])).
% 58.76/58.86 cnf(4346,plain,
% 58.76/58.86 (P2(f8(x43461),a12)),
% 58.76/58.86 inference(scs_inference,[],[3,8,27,19])).
% 58.76/58.86 cnf(4352,plain,
% 58.76/58.86 (P2(f17(x43521,x43522),f20(x43521,x43522))),
% 58.76/58.86 inference(scs_inference,[],[4294,4336,142,3,8,27,19,28,20,24])).
% 58.76/58.86 cnf(4356,plain,
% 58.76/58.86 (~P1(f9(x43561,x43562))),
% 58.76/58.86 inference(scs_inference,[],[4294,4290,4336,4302,142,3,313,8,27,19,28,20,24,2386,30])).
% 58.76/58.86 cnf(4386,plain,
% 58.76/58.86 (P2(f18(x43861,x43862),f5(x43861,x43862))),
% 58.76/58.86 inference(scs_inference,[],[4296,4339,165,28,20,24])).
% 58.76/58.86 cnf(4389,plain,
% 58.76/58.86 (P2(f1(x43891),f2(a12))),
% 58.76/58.86 inference(rename_variables,[],[4302])).
% 58.76/58.86 cnf(4400,plain,
% 58.76/58.86 (P2(f17(x44001,x44002),f20(x44001,x44002))),
% 58.76/58.86 inference(rename_variables,[],[4352])).
% 58.76/58.86 cnf(4401,plain,
% 58.76/58.86 (~P3(x44011,f8(x44012))),
% 58.76/58.86 inference(rename_variables,[],[165])).
% 58.76/58.86 cnf(4414,plain,
% 58.76/58.86 (P2(f5(x44141,x44142),f18(x44141,x44142))),
% 58.76/58.86 inference(rename_variables,[],[4296])).
% 58.76/58.86 cnf(4416,plain,
% 58.76/58.86 (P5(f8(x44161),f8(x44161),f5(a12,a12))),
% 58.76/58.86 inference(scs_inference,[],[4296,4414,4352,4400,4344,4339,18,4346,4300,4292,165,4401,1583,14,11,4302,4389,964,53,4,28,20,24,2846,3377,30,31,34,33,40,39,42])).
% 58.76/58.86 cnf(4424,plain,
% 58.76/58.86 (P2(f16(x44241),f3(x44242,x44241))),
% 58.76/58.86 inference(scs_inference,[],[4356,4344,125,28,20,24])).
% 58.76/58.86 cnf(4429,plain,
% 58.76/58.86 (~P1(f3(x44291,x44292))),
% 58.76/58.86 inference(scs_inference,[],[4356,4344,125,4292,313,4,28,20,24,2846,30])).
% 58.76/58.86 cnf(4460,plain,
% 58.76/58.86 (P2(f18(x44601,x44602),f5(x44601,x44602))),
% 58.76/58.86 inference(rename_variables,[],[4386])).
% 58.76/58.86 cnf(4472,plain,
% 58.76/58.86 (P2(f18(x44721,x44722),f5(x44721,x44722))),
% 58.76/58.86 inference(rename_variables,[],[4386])).
% 58.76/58.86 cnf(4477,plain,
% 58.76/58.86 (~P1(f16(x44771))),
% 58.76/58.86 inference(scs_inference,[],[4386,4460,4472,4424,4429,4416,4296,4290,100,56,1593,1521,2041,1988,8,6,4,28,20,24,31,34,41,42,23,30])).
% 58.76/58.86 cnf(4488,plain,
% 58.76/58.86 ($false),
% 58.76/58.86 inference(scs_inference,[],[4477,4327,4346,1424,20,24,31]),
% 58.76/58.86 ['proof']).
% 58.76/58.86 % SZS output end Proof
% 58.76/58.86 % Total time :58.110000s
%------------------------------------------------------------------------------