%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : NUN062+2 : 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 : n029.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:36 EDT 2024
% Result : Theorem 0.57s 0.69s
% Output : CNFRefutation 0.57s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : NUN062+2 : TPTP v8.2.0. Released v7.3.0.
% 0.08/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.13/0.34 % Computer : n029.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Tue Jun 18 20:35:54 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.54/0.62 start to proof:theBenchmark
% 0.57/0.69 %-------------------------------------------
% 0.57/0.69 % File :CSE---1.7
% 0.57/0.69 % Problem :theBenchmark
% 0.57/0.69 % Transform :cnf
% 0.57/0.69 % Format :tptp:raw
% 0.57/0.69 % Command :java -jar mcs_scs.jar %d %s
% 0.57/0.69
% 0.57/0.69 % Result :Theorem 0.010000s
% 0.57/0.69 % Output :CNFRefutation 0.010000s
% 0.57/0.69 %-------------------------------------------
% 0.57/0.69 %------------------------------------------------------------------------------
% 0.57/0.69 % File : NUN062+2 : TPTP v8.2.0. Released v7.3.0.
% 0.57/0.69 % Domain : Number Theory
% 0.57/0.69 % Problem : Robinson arithmetic: There exist infinite numbers
% 0.57/0.69 % Version : Especial.
% 0.57/0.69 % English :
% 0.57/0.69
% 0.57/0.69 % Refs : [BBJ03] Boolos et al. (2003), Computability and Logic
% 0.57/0.69 % : [Smi07] Smith (2007), An Introduction to Goedel's Theorems
% 0.57/0.69 % : [Lam18] Lampert (2018), Email to Geoff Sutcliffe
% 0.57/0.69 % Source : [Lam18]
% 0.57/0.69 % Names : infiniteNumbers [Lam18]
% 0.57/0.69
% 0.57/0.69 % Status : Theorem
% 0.57/0.69 % Rating : 0.17 v8.2.0, 0.19 v8.1.0, 0.22 v7.4.0, 0.07 v7.3.0
% 0.57/0.69 % Syntax : Number of formulae : 12 ( 0 unt; 0 def)
% 0.57/0.69 % Number of atoms : 48 ( 19 equ)
% 0.57/0.69 % Maximal formula atoms : 5 ( 4 avg)
% 0.57/0.69 % Number of connectives : 52 ( 16 ~; 11 |; 25 &)
% 0.57/0.69 % ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% 0.57/0.69 % Maximal formula depth : 9 ( 7 avg)
% 0.57/0.69 % Maximal term depth : 1 ( 1 avg)
% 0.57/0.69 % Number of predicates : 5 ( 4 usr; 0 prp; 1-3 aty)
% 0.57/0.69 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 0.57/0.69 % Number of variables : 48 ( 25 !; 23 ?)
% 0.57/0.69 % SPC : FOF_THM_RFO_SEQ
% 0.57/0.69
% 0.57/0.69 % Comments : Translated to FOL with equality.
% 0.57/0.69 %------------------------------------------------------------------------------
% 0.57/0.69 include('Axioms/NUM008+0.ax').
% 0.57/0.69 %------------------------------------------------------------------------------
% 0.57/0.69 fof(infiniteNumbers,conjecture,
% 0.57/0.69 ! [X1] :
% 0.57/0.69 ? [Y2,Y1] :
% 0.57/0.69 ( ! [Y4] :
% 0.57/0.69 ( ~ r1(Y4)
% 0.57/0.69 | Y1 != Y4 )
% 0.57/0.69 & ? [Y3] :
% 0.57/0.69 ( r3(X1,Y1,Y3)
% 0.57/0.69 & Y3 = Y2 ) ) ).
% 0.57/0.69
% 0.57/0.69 %------------------------------------------------------------------------------
% 0.57/0.69 %-------------------------------------------
% 0.57/0.69 % Proof found
% 0.57/0.69 % SZS status Theorem for theBenchmark
% 0.57/0.69 % SZS output start Proof
% 0.57/0.70 %ClaNum:66(EqnAxiom:37)
% 0.57/0.70 %VarNum:118(SingletonVarNum:56)
% 0.57/0.70 %MaxLitNum:4
% 0.57/0.70 %MaxfuncDepth:1
% 0.57/0.70 %SharedTerms:2
% 0.57/0.70 %goalClause: 65 66
% 0.57/0.70 [38]P1(f1(x381))
% 0.57/0.70 [39]P1(f4(x391))
% 0.57/0.70 [40]P1(f5(x401))
% 0.57/0.70 [43]P3(x431,f1(x431),x431)
% 0.57/0.70 [45]P4(x451,f5(x451),f4(x451))
% 0.57/0.70 [41]P2(x411,f6(x412,x411))
% 0.57/0.70 [42]P2(x421,f2(x422,x421))
% 0.57/0.70 [44]P2(f17(x441,x442),f7(x441,x442))
% 0.57/0.70 [46]P3(x461,x462,f17(x461,x462))
% 0.57/0.70 [47]P4(x471,x472,f3(x471,x472))
% 0.57/0.70 [48]P3(x481,f6(x481,x482),f7(x481,x482))
% 0.57/0.70 [49]P4(x491,f2(x491,x492),f18(x491,x492))
% 0.57/0.70 [50]P3(f3(x501,x502),x501,f18(x501,x502))
% 0.57/0.70 [51]P1(x511)+~E(x511,a8)
% 0.57/0.70 [52]~P1(x521)+E(x521,a8)
% 0.57/0.70 [53]E(f11(x531),x531)+E(f9(x531),x531)
% 0.57/0.70 [54]E(f11(x541),x541)+P1(f9(x541))
% 0.57/0.70 [57]P2(f10(x571),f11(x571))+E(f9(x571),x571)
% 0.57/0.70 [59]P2(f10(x591),f11(x591))+P1(f9(x591))
% 0.57/0.70 [55]P2(x551,x552)+~E(x552,f12(x551))
% 0.57/0.70 [56]~P2(x562,x561)+E(x561,f12(x562))
% 0.57/0.70 [61]P3(x611,x612,x613)+~E(x613,f15(x611,x612))
% 0.57/0.70 [62]P4(x621,x622,x623)+~E(x623,f16(x621,x622))
% 0.57/0.70 [63]~P3(x632,x633,x631)+E(x631,f15(x632,x633))
% 0.57/0.70 [64]~P4(x642,x643,x641)+E(x641,f16(x642,x643))
% 0.57/0.70 [58]~P1(x581)+~E(x581,x582)+~P2(x583,x582)
% 0.57/0.70 [65]~E(x651,x653)+~P3(a14,x652,x653)+E(f13(x651,x652),x652)
% 0.57/0.70 [66]~E(x661,x663)+~P3(a14,x662,x663)+P1(f13(x661,x662))
% 0.57/0.70 [60]~P2(x602,x604)+~P2(x601,x603)+E(x601,x602)+~E(x603,x604)
% 0.57/0.70 %EqnAxiom
% 0.57/0.70 [1]E(x11,x11)
% 0.57/0.70 [2]E(x22,x21)+~E(x21,x22)
% 0.57/0.70 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 0.57/0.70 [4]~E(x41,x42)+E(f1(x41),f1(x42))
% 0.57/0.70 [5]~E(x51,x52)+E(f4(x51),f4(x52))
% 0.57/0.70 [6]~E(x61,x62)+E(f5(x61),f5(x62))
% 0.57/0.70 [7]~E(x71,x72)+E(f6(x71,x73),f6(x72,x73))
% 0.57/0.70 [8]~E(x81,x82)+E(f6(x83,x81),f6(x83,x82))
% 0.57/0.70 [9]~E(x91,x92)+E(f2(x91,x93),f2(x92,x93))
% 0.57/0.70 [10]~E(x101,x102)+E(f2(x103,x101),f2(x103,x102))
% 0.57/0.70 [11]~E(x111,x112)+E(f13(x111,x113),f13(x112,x113))
% 0.57/0.70 [12]~E(x121,x122)+E(f13(x123,x121),f13(x123,x122))
% 0.57/0.70 [13]~E(x131,x132)+E(f17(x131,x133),f17(x132,x133))
% 0.57/0.70 [14]~E(x141,x142)+E(f17(x143,x141),f17(x143,x142))
% 0.57/0.70 [15]~E(x151,x152)+E(f7(x151,x153),f7(x152,x153))
% 0.57/0.70 [16]~E(x161,x162)+E(f7(x163,x161),f7(x163,x162))
% 0.57/0.70 [17]~E(x171,x172)+E(f16(x171,x173),f16(x172,x173))
% 0.57/0.70 [18]~E(x181,x182)+E(f16(x183,x181),f16(x183,x182))
% 0.57/0.70 [19]~E(x191,x192)+E(f15(x191,x193),f15(x192,x193))
% 0.57/0.70 [20]~E(x201,x202)+E(f15(x203,x201),f15(x203,x202))
% 0.57/0.70 [21]~E(x211,x212)+E(f11(x211),f11(x212))
% 0.57/0.70 [22]~E(x221,x222)+E(f3(x221,x223),f3(x222,x223))
% 0.57/0.70 [23]~E(x231,x232)+E(f3(x233,x231),f3(x233,x232))
% 0.57/0.70 [24]~E(x241,x242)+E(f10(x241),f10(x242))
% 0.57/0.70 [25]~E(x251,x252)+E(f9(x251),f9(x252))
% 0.57/0.70 [26]~E(x261,x262)+E(f12(x261),f12(x262))
% 0.57/0.70 [27]~E(x271,x272)+E(f18(x271,x273),f18(x272,x273))
% 0.57/0.70 [28]~E(x281,x282)+E(f18(x283,x281),f18(x283,x282))
% 0.57/0.70 [29]~P1(x291)+P1(x292)+~E(x291,x292)
% 0.57/0.70 [30]P3(x302,x303,x304)+~E(x301,x302)+~P3(x301,x303,x304)
% 0.57/0.70 [31]P3(x313,x312,x314)+~E(x311,x312)+~P3(x313,x311,x314)
% 0.57/0.70 [32]P3(x323,x324,x322)+~E(x321,x322)+~P3(x323,x324,x321)
% 0.57/0.70 [33]P2(x332,x333)+~E(x331,x332)+~P2(x331,x333)
% 0.57/0.70 [34]P2(x343,x342)+~E(x341,x342)+~P2(x343,x341)
% 0.57/0.70 [35]P4(x352,x353,x354)+~E(x351,x352)+~P4(x351,x353,x354)
% 0.57/0.70 [36]P4(x363,x362,x364)+~E(x361,x362)+~P4(x363,x361,x364)
% 0.57/0.70 [37]P4(x373,x374,x372)+~E(x371,x372)+~P4(x373,x374,x371)
% 0.57/0.70
% 0.57/0.70 %-------------------------------------------
% 0.57/0.70 cnf(69,plain,
% 0.57/0.70 (~P1(x691)+~P2(x692,x691)),
% 0.57/0.70 inference(equality_inference,[],[58])).
% 0.57/0.70 cnf(71,plain,
% 0.57/0.70 (P3(x711,x712,f15(x711,x712))),
% 0.57/0.70 inference(equality_inference,[],[61])).
% 0.57/0.70 cnf(73,plain,
% 0.57/0.70 (~P3(a14,x732,x731)+E(f13(x731,x732),x732)),
% 0.57/0.70 inference(equality_inference,[],[65])).
% 0.57/0.70 cnf(74,plain,
% 0.57/0.70 (~P3(a14,x742,x741)+P1(f13(x741,x742))),
% 0.57/0.70 inference(equality_inference,[],[66])).
% 0.57/0.70 cnf(75,plain,
% 0.57/0.70 (E(f13(f15(a14,x751),x751),x751)),
% 0.57/0.70 inference(scs_inference,[],[71,73])).
% 0.57/0.70 cnf(76,plain,
% 0.57/0.70 (P3(x761,x762,f15(x761,x762))),
% 0.57/0.70 inference(rename_variables,[],[71])).
% 0.57/0.70 cnf(78,plain,
% 0.57/0.70 (P1(f13(f15(a14,x781),x781))),
% 0.57/0.70 inference(scs_inference,[],[71,76,73,74])).
% 0.57/0.70 cnf(105,plain,
% 0.57/0.70 (P3(x1051,f6(x1051,x1052),f7(x1051,x1052))),
% 0.57/0.70 inference(rename_variables,[],[48])).
% 0.57/0.70 cnf(112,plain,
% 0.57/0.70 (E(f13(f15(a14,x1121),x1121),x1121)),
% 0.57/0.70 inference(rename_variables,[],[75])).
% 0.57/0.70 cnf(113,plain,
% 0.57/0.70 ($false),
% 0.57/0.70 inference(scs_inference,[],[78,75,112,48,105,41,69,73,74,2,29,58]),
% 0.57/0.70 ['proof']).
% 0.57/0.70 % SZS output end Proof
% 0.57/0.70 % Total time :0.010000s
%------------------------------------------------------------------------------