%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : NUN073+1 : TPTP v8.2.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n002.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:39 EDT 2024
% Result : Theorem 58.64s 58.68s
% Output : CNFRefutation 58.64s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : NUN073+1 : TPTP v8.2.0. Released v7.3.0.
% 0.06/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.33 % Computer : n002.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Tue Jun 18 21:05:54 EDT 2024
% 0.13/0.33 % CPUTime :
% 0.49/0.56 start to proof:theBenchmark
% 58.64/58.67 %-------------------------------------------
% 58.64/58.67 % File :CSE---1.7
% 58.64/58.67 % Problem :theBenchmark
% 58.64/58.67 % Transform :cnf
% 58.64/58.67 % Format :tptp:raw
% 58.64/58.67 % Command :java -jar mcs_scs.jar %d %s
% 58.64/58.67
% 58.64/58.67 % Result :Theorem 58.050000s
% 58.64/58.67 % Output :CNFRefutation 58.050000s
% 58.64/58.67 %-------------------------------------------
% 58.64/58.67 %------------------------------------------------------------------------------
% 58.64/58.67 % File : NUN073+1 : TPTP v8.2.0. Released v7.3.0.
% 58.64/58.67 % Domain : Number Theory
% 58.64/58.67 % Problem : Robinson arithmetic: 1 != 2
% 58.64/58.67 % Version : Especial.
% 58.64/58.67 % English :
% 58.64/58.67
% 58.64/58.67 % Refs : [BBJ03] Boolos et al. (2003), Computability and Logic
% 58.64/58.67 % : [Smi07] Smith (2007), An Introduction to Goedel's Theorems
% 58.64/58.67 % : [Lam18] Lampert (2018), Email to Geoff Sutcliffe
% 58.64/58.67 % Source : [Lam18]
% 58.64/58.67 % Names : oneunidtwo [Lam18]
% 58.64/58.68
% 58.64/58.68 % Status : Theorem
% 58.64/58.68 % Rating : 0.06 v8.2.0, 0.07 v7.5.0, 0.10 v7.4.0, 0.06 v7.3.0
% 58.64/58.68 % Syntax : Number of formulae : 19 ( 1 unt; 0 def)
% 58.64/58.68 % Number of atoms : 81 ( 0 equ)
% 58.64/58.68 % Maximal formula atoms : 7 ( 4 avg)
% 58.64/58.68 % Number of connectives : 102 ( 40 ~; 31 |; 31 &)
% 58.64/58.68 % ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% 58.64/58.68 % Maximal formula depth : 13 ( 8 avg)
% 58.64/58.68 % Maximal term depth : 1 ( 1 avg)
% 58.64/58.68 % Number of predicates : 5 ( 5 usr; 0 prp; 1-3 aty)
% 58.64/58.68 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 58.64/58.68 % Number of variables : 72 ( 52 !; 20 ?)
% 58.64/58.68 % SPC : FOF_THM_RFO_NEQ
% 58.64/58.68
% 58.64/58.68 % Comments : Translated to FOL without equality.
% 58.64/58.68 %------------------------------------------------------------------------------
% 58.64/58.68 include('Axioms/NUM009+0.ax').
% 58.64/58.68 %------------------------------------------------------------------------------
% 58.64/58.68 fof(oneunidtwo,conjecture,
% 58.64/58.68 ! [Y1] :
% 58.64/58.68 ( ! [Y2] :
% 58.64/58.68 ( ! [Y4] :
% 58.64/58.68 ( ~ r1(Y4)
% 58.64/58.68 | ~ r2(Y4,Y2) )
% 58.64/58.68 | ~ id(Y2,Y1) )
% 58.64/58.68 | ! [Y3] :
% 58.64/58.68 ( ! [Y5] :
% 58.64/58.68 ( ~ r1(Y5)
% 58.64/58.68 | ~ r2(Y5,Y3) )
% 58.64/58.68 | ~ r2(Y3,Y1) ) ) ).
% 58.64/58.68
% 58.64/58.68 %------------------------------------------------------------------------------
% 58.64/58.68 %-------------------------------------------
% 58.64/58.68 % Proof found
% 58.64/58.68 % SZS status Theorem for theBenchmark
% 58.64/58.68 % SZS output start Proof
% 58.64/58.68 %ClaNum:48(EqnAxiom:0)
% 58.64/58.68 %VarNum:201(SingletonVarNum:98)
% 58.64/58.68 %MaxLitNum:5
% 58.64/58.68 %MaxfuncDepth:1
% 58.64/58.68 %SharedTerms:12
% 58.64/58.68 %goalClause: 1 2 6 7 8 9
% 58.64/58.68 %singleGoalClaCount:6
% 58.64/58.68 [1]P1(a1)
% 58.64/58.68 [2]P1(a16)
% 58.64/58.68 [6]P2(a10,a11)
% 58.64/58.68 [7]P3(a1,a10)
% 58.64/58.68 [8]P3(a17,a11)
% 58.64/58.68 [9]P3(a16,a17)
% 58.64/58.68 [10]P2(x101,x101)
% 58.64/58.68 [3]P1(f2(x31))
% 58.64/58.68 [4]P1(f7(x41))
% 58.64/58.68 [5]P1(f9(x51))
% 58.64/58.68 [11]P2(f3(x111),x111)
% 58.64/58.68 [12]P2(f8(x121),f9(x121))
% 58.64/58.68 [18]P4(x181,f2(x181),f3(x181))
% 58.64/58.68 [19]P5(x191,f7(x191),f8(x191))
% 58.64/58.68 [13]P3(x131,f18(x132,x131))
% 58.64/58.68 [14]P3(x141,f4(x142,x141))
% 58.64/58.68 [15]P2(f19(x151,x152),f20(x151,x152))
% 58.64/58.68 [16]P2(f5(x161,x162),f24(x161,x162))
% 58.64/58.68 [17]P3(f25(x171,x172),f20(x171,x172))
% 58.64/58.68 [20]P4(x201,x202,f25(x201,x202))
% 58.64/58.68 [21]P5(x211,x212,f6(x211,x212))
% 58.64/58.68 [22]P4(x221,f18(x221,x222),f19(x221,x222))
% 58.64/58.68 [23]P5(x231,f4(x231,x232),f5(x231,x232))
% 58.64/58.68 [24]P4(f6(x241,x242),x241,f24(x241,x242))
% 58.64/58.68 [25]~P1(x251)+P2(x251,a12)
% 58.64/58.68 [26]P1(x261)+~P2(x261,a12)
% 58.64/58.68 [27]P2(x271,f15(x271))+P1(f13(x271))
% 58.64/58.68 [31]P3(f14(x311),f15(x311))+P1(f13(x311))
% 58.64/58.68 [32]P2(x321,f15(x321))+P2(x321,f13(x321))
% 58.64/58.68 [35]P3(f14(x351),f15(x351))+P2(x351,f13(x351))
% 58.64/58.68 [30]~P2(x302,x301)+P2(x301,x302)
% 58.64/58.68 [33]~P3(x332,x331)+P2(x331,f21(x332))
% 58.64/58.68 [34]P3(x341,x342)+~P2(x342,f21(x341))
% 58.64/58.68 [41]P4(x411,x412,x413)+~P2(x413,f22(x411,x412))
% 58.64/58.68 [42]P5(x421,x422,x423)+~P2(x423,f23(x421,x422))
% 58.64/58.68 [43]~P4(x432,x433,x431)+P2(x431,f22(x432,x433))
% 58.64/58.68 [44]~P5(x442,x443,x441)+P2(x441,f23(x442,x443))
% 58.64/58.68 [28]~P2(x282,x281)+P1(x281)+~P1(x282)
% 58.64/58.68 [29]~P2(x291,x292)+P1(x291)+~P1(x292)
% 58.64/58.68 [36]~P1(x361)+~P2(x361,x362)+~P3(x363,x362)
% 58.64/58.68 [37]~P2(x371,x373)+P2(x371,x372)+~P2(x373,x372)
% 58.64/58.68 [38]~P3(x382,x384)+~P3(x381,x383)+P2(x381,x382)+~P2(x383,x384)
% 58.64/58.68 [39]~P3(x394,x393)+P3(x391,x392)+~P2(x393,x392)+~P2(x394,x391)
% 58.64/58.68 [40]~P3(x404,x403)+P3(x401,x402)+~P2(x402,x403)+~P2(x401,x404)
% 58.64/58.68 [45]~P4(x456,x455,x454)+P4(x451,x452,x453)+~P2(x454,x453)+~P2(x455,x452)+~P2(x456,x451)
% 58.64/58.68 [46]~P4(x466,x465,x464)+P4(x461,x462,x463)+~P2(x463,x464)+~P2(x462,x465)+~P2(x461,x466)
% 58.64/58.68 [47]~P5(x476,x475,x474)+P5(x471,x472,x473)+~P2(x474,x473)+~P2(x475,x472)+~P2(x476,x471)
% 58.64/58.68 [48]~P5(x486,x485,x484)+P5(x481,x482,x483)+~P2(x483,x484)+~P2(x482,x485)+~P2(x481,x486)
% 58.64/58.68 %EqnAxiom
% 58.64/58.68
% 58.64/58.68 %-------------------------------------------
% 58.64/58.69 cnf(50,plain,
% 58.64/58.69 (P2(x501,x501)),
% 58.64/58.69 inference(rename_variables,[],[10])).
% 58.64/58.69 cnf(53,plain,
% 58.64/58.69 (P2(x531,x531)),
% 58.64/58.69 inference(rename_variables,[],[10])).
% 58.64/58.69 cnf(55,plain,
% 58.64/58.69 (P4(x551,x552,f22(x551,x552))),
% 58.64/58.69 inference(scs_inference,[],[10,50,53,26,34,41])).
% 58.64/58.69 cnf(56,plain,
% 58.64/58.69 (P2(x561,x561)),
% 58.64/58.69 inference(rename_variables,[],[10])).
% 58.64/58.69 cnf(58,plain,
% 58.64/58.69 (P5(x581,x582,f23(x581,x582))),
% 58.64/58.69 inference(scs_inference,[],[10,50,53,56,26,34,41,42])).
% 58.64/58.69 cnf(59,plain,
% 58.64/58.69 (P2(x591,x591)),
% 58.64/58.69 inference(rename_variables,[],[10])).
% 58.64/58.69 cnf(61,plain,
% 58.64/58.69 (~P3(x611,a1)),
% 58.64/58.69 inference(scs_inference,[],[1,10,50,53,56,59,26,34,41,42,36])).
% 58.64/58.69 cnf(62,plain,
% 58.64/58.69 (P2(x621,x621)),
% 58.64/58.69 inference(rename_variables,[],[10])).
% 58.64/58.69 cnf(65,plain,
% 58.64/58.69 (P2(x651,x651)),
% 58.64/58.69 inference(rename_variables,[],[10])).
% 58.64/58.69 cnf(66,plain,
% 58.64/58.69 (P3(x661,f18(x662,x661))),
% 58.64/58.69 inference(rename_variables,[],[13])).
% 58.64/58.69 cnf(68,plain,
% 58.64/58.69 (P3(a10,f18(x681,a11))),
% 58.64/58.69 inference(scs_inference,[],[1,6,10,50,53,56,59,62,65,13,66,26,34,41,42,36,39,40])).
% 58.64/58.69 cnf(69,plain,
% 58.64/58.69 (P2(x691,x691)),
% 58.64/58.69 inference(rename_variables,[],[10])).
% 58.64/58.69 cnf(73,plain,
% 58.64/58.69 (P2(x731,x731)),
% 58.64/58.69 inference(rename_variables,[],[10])).
% 58.64/58.69 cnf(74,plain,
% 58.64/58.69 (P4(x741,x742,f25(x741,x742))),
% 58.64/58.69 inference(rename_variables,[],[20])).
% 58.64/58.69 cnf(76,plain,
% 58.64/58.69 (P4(a10,a10,f25(a11,a11))),
% 58.64/58.69 inference(scs_inference,[],[1,6,10,50,53,56,59,62,65,69,73,20,74,13,66,26,34,41,42,36,39,40,45,46])).
% 58.64/58.69 cnf(77,plain,
% 58.64/58.69 (P2(x771,x771)),
% 58.64/58.69 inference(rename_variables,[],[10])).
% 58.64/58.69 cnf(81,plain,
% 58.64/58.69 (P2(x811,x811)),
% 58.64/58.69 inference(rename_variables,[],[10])).
% 58.64/58.69 cnf(82,plain,
% 58.64/58.69 (P5(x821,x822,f6(x821,x822))),
% 58.64/58.69 inference(rename_variables,[],[21])).
% 58.64/58.69 cnf(84,plain,
% 58.64/58.69 (P5(a10,a10,f6(a11,a11))),
% 58.64/58.69 inference(scs_inference,[],[1,6,10,50,53,56,59,62,65,69,73,77,81,20,74,21,82,13,66,26,34,41,42,36,39,40,45,46,47,48])).
% 58.64/58.69 cnf(89,plain,
% 58.64/58.69 (P2(f3(x891),x891)),
% 58.64/58.69 inference(rename_variables,[],[11])).
% 58.64/58.69 cnf(92,plain,
% 58.64/58.69 (P2(f3(x921),x921)),
% 58.64/58.69 inference(rename_variables,[],[11])).
% 58.64/58.69 cnf(95,plain,
% 58.64/58.69 (P2(f3(x951),x951)),
% 58.64/58.69 inference(rename_variables,[],[11])).
% 58.64/58.69 cnf(98,plain,
% 58.64/58.69 (P2(f3(x981),x981)),
% 58.64/58.69 inference(rename_variables,[],[11])).
% 58.64/58.69 cnf(100,plain,
% 58.64/58.69 (P2(f3(a10),a11)),
% 58.64/58.69 inference(scs_inference,[],[6,11,89,92,95,98,41,42,34,26,37])).
% 58.64/58.69 cnf(101,plain,
% 58.64/58.69 (P2(f3(x1011),x1011)),
% 58.64/58.69 inference(rename_variables,[],[11])).
% 58.64/58.69 cnf(106,plain,
% 58.64/58.69 (P3(a11,f21(a10))),
% 58.64/58.69 inference(scs_inference,[],[2,6,11,89,92,95,98,101,10,41,42,34,26,37,36,39])).
% 58.64/58.69 cnf(146,plain,
% 58.64/58.69 (~P3(x1461,f2(x1462))),
% 58.64/58.69 inference(scs_inference,[],[12,3,11,10,37,36])).
% 58.64/58.69 cnf(243,plain,
% 58.64/58.69 (P2(a1,a12)),
% 58.64/58.69 inference(scs_inference,[],[1,10,25,28])).
% 58.64/58.69 cnf(244,plain,
% 58.64/58.69 (P2(f3(a1),a12)),
% 58.64/58.69 inference(scs_inference,[],[243,11,37])).
% 58.64/58.69 cnf(317,plain,
% 58.64/58.69 (~P1(a11)),
% 58.64/58.69 inference(scs_inference,[],[6,7,30,36])).
% 58.64/58.69 cnf(318,plain,
% 58.64/58.69 (~P2(a16,a11)),
% 58.64/58.69 inference(scs_inference,[],[2,317,28])).
% 58.64/58.69 cnf(331,plain,
% 58.64/58.69 (~P2(a11,a1)),
% 58.64/58.69 inference(scs_inference,[],[1,317,29])).
% 58.64/58.69 cnf(405,plain,
% 58.64/58.69 (P2(x4051,x4051)),
% 58.64/58.69 inference(rename_variables,[],[10])).
% 58.64/58.69 cnf(407,plain,
% 58.64/58.69 (P3(a16,f3(a17))),
% 58.64/58.69 inference(scs_inference,[],[10,405,9,318,106,11,38,40])).
% 58.64/58.69 cnf(502,plain,
% 58.64/58.69 (~P3(a11,f3(a10))),
% 58.64/58.69 inference(scs_inference,[],[11,7,331,38])).
% 58.64/58.69 cnf(554,plain,
% 58.64/58.69 (P3(a10,f4(x5541,a11))),
% 58.64/58.69 inference(scs_inference,[],[14,6,10,40])).
% 58.64/58.69 cnf(773,plain,
% 58.64/58.69 (P4(a10,a10,f22(a11,a11))),
% 58.64/58.69 inference(scs_inference,[],[55,6,10,46])).
% 58.64/58.69 cnf(836,plain,
% 58.64/58.69 (P5(a10,a10,f23(a11,a11))),
% 58.64/58.69 inference(scs_inference,[],[58,6,10,48])).
% 58.64/58.69 cnf(1691,plain,
% 58.64/58.69 (~P2(a11,x16911)+~P3(x16911,f3(a10))),
% 58.64/58.69 inference(scs_inference,[],[502,6,10,11,39,40])).
% 58.64/58.69 cnf(1702,plain,
% 58.64/58.69 (~P3(f21(a17),f3(a10))),
% 58.64/58.69 inference(scs_inference,[],[8,1691,33])).
% 58.64/58.69 cnf(2208,plain,
% 58.64/58.69 (~P3(f21(a17),a11)),
% 58.64/58.69 inference(scs_inference,[],[1702,100,10,40])).
% 58.64/58.69 cnf(2493,plain,
% 58.64/58.69 (~P2(f21(a17),a17)),
% 58.64/58.69 inference(scs_inference,[],[2208,8,10,40])).
% 58.64/58.69 cnf(2615,plain,
% 58.64/58.69 (~P3(a17,f3(a17))),
% 58.64/58.69 inference(scs_inference,[],[2493,11,37,30,33])).
% 58.64/58.69 cnf(2737,plain,
% 58.64/58.69 (~P2(a16,a17)),
% 58.64/58.69 inference(scs_inference,[],[2615,407,10,40,30])).
% 58.64/58.69 cnf(2742,plain,
% 58.64/58.69 (~P3(a16,a10)),
% 58.64/58.69 inference(scs_inference,[],[6,8,2737,38])).
% 58.64/58.69 cnf(2752,plain,
% 58.64/58.69 (~P2(a16,a1)),
% 58.64/58.69 inference(scs_inference,[],[7,2742,10,40])).
% 58.64/58.69 cnf(2918,plain,
% 58.64/58.69 (~P2(f3(a1),a16)),
% 58.64/58.69 inference(scs_inference,[],[2752,11,37,30])).
% 58.64/58.69 cnf(3050,plain,
% 58.64/58.69 (P2(a16,a12)),
% 58.64/58.69 inference(scs_inference,[],[61,773,836,2,43,44,34,25])).
% 58.64/58.69 cnf(3056,plain,
% 58.64/58.69 (P1(f3(a16))),
% 58.64/58.69 inference(scs_inference,[],[61,773,836,554,2,12,11,43,44,34,25,33,30,29])).
% 58.64/58.69 cnf(3062,plain,
% 58.64/58.69 (~P2(a12,a16)),
% 58.64/58.69 inference(scs_inference,[],[61,773,836,17,554,2918,2,12,244,15,11,43,44,34,25,33,30,29,36,37])).
% 58.64/58.69 cnf(3102,plain,
% 58.64/58.69 ($false),
% 58.64/58.69 inference(scs_inference,[],[3050,3062,146,84,76,3056,68,43,44,34,25,33,30]),
% 58.64/58.69 ['proof']).
% 58.64/58.69 % SZS output end Proof
% 58.64/58.69 % Total time :58.050000s
%------------------------------------------------------------------------------