%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : NUN089+1 : TPTP v8.2.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% Computer : n015.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:45 EDT 2024
% Result : Theorem 0.58s 0.62s
% Output : CNFRefutation 0.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NUN089+1 : TPTP v8.2.0. Released v7.3.0.
% 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s
% 0.12/0.34 % Computer : n015.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Tue Jun 18 20:33:54 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.21/0.57 start to proof:theBenchmark
% 0.57/0.62 %-------------------------------------------
% 0.57/0.62 % File :CSE---1.7
% 0.57/0.62 % Problem :theBenchmark
% 0.57/0.62 % Transform :cnf
% 0.57/0.62 % Format :tptp:raw
% 0.57/0.62 % Command :java -jar mcs_scs.jar %d %s
% 0.57/0.62
% 0.57/0.62 % Result :Theorem 0.010000s
% 0.57/0.62 % Output :CNFRefutation 0.010000s
% 0.57/0.62 %-------------------------------------------
% 0.58/0.62 %------------------------------------------------------------------------------
% 0.58/0.62 % File : NUN089+1 : TPTP v8.2.0. Released v7.3.0.
% 0.58/0.62 % Domain : Number Theory
% 0.58/0.62 % Problem : Robinson arithmetic: 0 != 2
% 0.58/0.62 % Version : Especial.
% 0.58/0.62 % English :
% 0.58/0.62
% 0.58/0.62 % Refs : [BBJ03] Boolos et al. (2003), Computability and Logic
% 0.58/0.62 % : [Smi07] Smith (2007), An Introduction to Goedel's Theorems
% 0.58/0.62 % : [Lam18] Lampert (2018), Email to Geoff Sutcliffe
% 0.58/0.62 % Source : [Lam18]
% 0.58/0.62 % Names : zerounidtwo [Lam18]
% 0.58/0.62
% 0.58/0.62 % Status : Theorem
% 0.58/0.62 % Rating : 0.00 v7.3.0
% 0.58/0.62 % Syntax : Number of formulae : 19 ( 1 unt; 0 def)
% 0.58/0.62 % Number of atoms : 80 ( 0 equ)
% 0.58/0.62 % Maximal formula atoms : 7 ( 4 avg)
% 0.58/0.62 % Number of connectives : 100 ( 39 ~; 30 |; 31 &)
% 0.58/0.62 % ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% 0.58/0.62 % Maximal formula depth : 13 ( 8 avg)
% 0.58/0.62 % Maximal term depth : 1 ( 1 avg)
% 0.58/0.62 % Number of predicates : 5 ( 5 usr; 0 prp; 1-3 aty)
% 0.58/0.62 % Number of functors : 0 ( 0 usr; 0 con; --- aty)
% 0.58/0.62 % Number of variables : 71 ( 51 !; 20 ?)
% 0.58/0.62 % SPC : FOF_THM_RFO_NEQ
% 0.58/0.62
% 0.58/0.62 % Comments : Translated to FOL without equality.
% 0.58/0.62 %------------------------------------------------------------------------------
% 0.58/0.62 include('Axioms/NUM009+0.ax').
% 0.58/0.62 %------------------------------------------------------------------------------
% 0.58/0.62 fof(zerounidtwo,conjecture,
% 0.58/0.62 ! [Y1] :
% 0.58/0.62 ( ! [Y2] :
% 0.58/0.62 ( ! [Y3] :
% 0.58/0.62 ( ~ r1(Y3)
% 0.58/0.62 | ~ r2(Y3,Y2) )
% 0.58/0.62 | ~ r2(Y2,Y1) )
% 0.58/0.62 | ! [Y4] :
% 0.58/0.62 ( ~ id(Y4,Y1)
% 0.58/0.62 | ~ r1(Y4) ) ) ).
% 0.58/0.62
% 0.58/0.62 %------------------------------------------------------------------------------
% 0.58/0.62 %-------------------------------------------
% 0.58/0.62 % Proof found
% 0.58/0.62 % SZS status Theorem for theBenchmark
% 0.58/0.62 % SZS output start Proof
% 0.58/0.63 %ClaNum:47(EqnAxiom:0)
% 0.58/0.63 %VarNum:201(SingletonVarNum:98)
% 0.58/0.63 %MaxLitNum:5
% 0.58/0.63 %MaxfuncDepth:1
% 0.58/0.63 %SharedTerms:10
% 0.58/0.63 %goalClause: 1 2 6 7 8
% 0.58/0.63 %singleGoalClaCount:5
% 0.58/0.63 [1]P1(a1)
% 0.58/0.63 [2]P1(a16)
% 0.58/0.63 [6]P2(a16,a10)
% 0.58/0.63 [7]P3(a15,a10)
% 0.58/0.63 [8]P3(a1,a15)
% 0.58/0.63 [9]P2(x91,x91)
% 0.58/0.63 [3]P1(f2(x31))
% 0.58/0.63 [4]P1(f7(x41))
% 0.58/0.63 [5]P1(f9(x51))
% 0.58/0.63 [10]P2(f3(x101),x101)
% 0.58/0.63 [11]P2(f8(x111),f9(x111))
% 0.58/0.63 [17]P4(x171,f2(x171),f3(x171))
% 0.58/0.63 [18]P5(x181,f7(x181),f8(x181))
% 0.58/0.63 [12]P3(x121,f17(x122,x121))
% 0.58/0.63 [13]P3(x131,f4(x132,x131))
% 0.58/0.63 [14]P2(f18(x141,x142),f19(x141,x142))
% 0.58/0.63 [15]P2(f5(x151,x152),f23(x151,x152))
% 0.58/0.63 [16]P3(f24(x161,x162),f19(x161,x162))
% 0.58/0.63 [19]P4(x191,x192,f24(x191,x192))
% 0.58/0.63 [20]P5(x201,x202,f6(x201,x202))
% 0.58/0.63 [21]P4(x211,f17(x211,x212),f18(x211,x212))
% 0.58/0.63 [22]P5(x221,f4(x221,x222),f5(x221,x222))
% 0.58/0.63 [23]P4(f6(x231,x232),x231,f23(x231,x232))
% 0.58/0.63 [24]~P1(x241)+P2(x241,a11)
% 0.58/0.63 [25]P1(x251)+~P2(x251,a11)
% 0.58/0.63 [26]P2(x261,f14(x261))+P1(f12(x261))
% 0.58/0.63 [30]P3(f13(x301),f14(x301))+P1(f12(x301))
% 0.58/0.63 [31]P2(x311,f14(x311))+P2(x311,f12(x311))
% 0.58/0.63 [34]P3(f13(x341),f14(x341))+P2(x341,f12(x341))
% 0.58/0.63 [29]~P2(x292,x291)+P2(x291,x292)
% 0.58/0.63 [32]~P3(x322,x321)+P2(x321,f20(x322))
% 0.58/0.63 [33]P3(x331,x332)+~P2(x332,f20(x331))
% 0.58/0.63 [40]P4(x401,x402,x403)+~P2(x403,f21(x401,x402))
% 0.58/0.63 [41]P5(x411,x412,x413)+~P2(x413,f22(x411,x412))
% 0.58/0.63 [42]~P4(x422,x423,x421)+P2(x421,f21(x422,x423))
% 0.58/0.63 [43]~P5(x432,x433,x431)+P2(x431,f22(x432,x433))
% 0.58/0.63 [27]~P2(x272,x271)+P1(x271)+~P1(x272)
% 0.58/0.63 [28]~P2(x281,x282)+P1(x281)+~P1(x282)
% 0.58/0.63 [35]~P1(x351)+~P2(x351,x352)+~P3(x353,x352)
% 0.58/0.63 [36]~P2(x361,x363)+P2(x361,x362)+~P2(x363,x362)
% 0.58/0.63 [37]~P3(x372,x374)+~P3(x371,x373)+P2(x371,x372)+~P2(x373,x374)
% 0.58/0.63 [38]~P3(x384,x383)+P3(x381,x382)+~P2(x383,x382)+~P2(x384,x381)
% 0.58/0.63 [39]~P3(x394,x393)+P3(x391,x392)+~P2(x392,x393)+~P2(x391,x394)
% 0.58/0.63 [44]~P4(x446,x445,x444)+P4(x441,x442,x443)+~P2(x444,x443)+~P2(x445,x442)+~P2(x446,x441)
% 0.58/0.63 [45]~P4(x456,x455,x454)+P4(x451,x452,x453)+~P2(x453,x454)+~P2(x452,x455)+~P2(x451,x456)
% 0.58/0.63 [46]~P5(x466,x465,x464)+P5(x461,x462,x463)+~P2(x464,x463)+~P2(x465,x462)+~P2(x466,x461)
% 0.58/0.63 [47]~P5(x476,x475,x474)+P5(x471,x472,x473)+~P2(x473,x474)+~P2(x472,x475)+~P2(x471,x476)
% 0.58/0.63 %EqnAxiom
% 0.58/0.63
% 0.58/0.63 %-------------------------------------------
% 0.58/0.63 cnf(88,plain,
% 0.58/0.63 (P2(f3(x881),x881)),
% 0.58/0.63 inference(rename_variables,[],[10])).
% 0.58/0.63 cnf(91,plain,
% 0.58/0.63 (P2(f3(x911),x911)),
% 0.58/0.63 inference(rename_variables,[],[10])).
% 0.58/0.63 cnf(94,plain,
% 0.58/0.63 (P2(f3(x941),x941)),
% 0.58/0.63 inference(rename_variables,[],[10])).
% 0.58/0.63 cnf(97,plain,
% 0.58/0.63 (P2(f3(x971),x971)),
% 0.58/0.63 inference(rename_variables,[],[10])).
% 0.58/0.63 cnf(102,plain,
% 0.58/0.63 ($false),
% 0.58/0.63 inference(scs_inference,[],[2,7,6,10,88,91,94,97,41,33,40,25,36,35]),
% 0.58/0.63 ['proof']).
% 0.58/0.63 % SZS output end Proof
% 0.58/0.63 % Total time :0.010000s
%------------------------------------------------------------------------------