%------------------------------------------------------------------------------
% File : CSE---1.7
% Problem : NUM836+1 : TPTP v8.2.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% Computer : n032.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 12:26:39 EDT 2024
% Result : Theorem 1.49s 1.59s
% Output : CNFRefutation 1.49s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : NUM836+1 : TPTP v8.2.0. Released v4.1.0.
% 0.00/0.09 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s
% 0.09/0.28 % Computer : n032.cluster.edu
% 0.09/0.28 % Model : x86_64 x86_64
% 0.09/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.28 % Memory : 8042.1875MB
% 0.09/0.28 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.28 % CPULimit : 300
% 0.09/0.28 % WCLimit : 300
% 0.09/0.28 % DateTime : Sat Jun 22 19:45:53 EDT 2024
% 0.09/0.28 % CPUTime :
% 0.13/0.44 start to proof:theBenchmark
% 1.44/1.58 %-------------------------------------------
% 1.44/1.58 % File :CSE---1.7
% 1.44/1.58 % Problem :theBenchmark
% 1.44/1.58 % Transform :cnf
% 1.44/1.58 % Format :tptp:raw
% 1.44/1.58 % Command :java -jar mcs_scs.jar %d %s
% 1.44/1.58
% 1.44/1.58 % Result :Theorem 1.100000s
% 1.44/1.58 % Output :CNFRefutation 1.100000s
% 1.44/1.58 %-------------------------------------------
% 1.44/1.58 %------------------------------------------------------------------------------
% 1.44/1.58 % File : NUM836+1 : TPTP v8.2.0. Released v4.1.0.
% 1.44/1.58 % Domain : Number Theory
% 1.44/1.58 % Problem : dis(ex(cond(conseq(131),0),1))
% 1.44/1.58 % Version : Especial.
% 1.44/1.58 % English :
% 1.44/1.58
% 1.44/1.58 % Refs : [Lan30] Landau (1930), Grundlagen der Analysis
% 1.44/1.58 % : [Kue09] Kuehlwein (2009), Email to Geoff Sutcliffe
% 1.44/1.58 % : [KC+10] Kuehlwein et al. (2010), Premise Selection in the Napr
% 1.44/1.58 % Source : [Kue09]
% 1.44/1.58 % Names :
% 1.44/1.58
% 1.44/1.58 % Status : Theorem
% 1.44/1.58 % Rating : 0.14 v8.2.0, 0.17 v8.1.0, 0.19 v7.4.0, 0.13 v7.3.0, 0.17 v7.2.0, 0.14 v7.1.0, 0.22 v7.0.0, 0.20 v6.4.0, 0.27 v6.3.0, 0.33 v6.2.0, 0.32 v6.1.0, 0.30 v5.4.0, 0.32 v5.3.0, 0.41 v5.2.0, 0.25 v5.1.0, 0.29 v5.0.0, 0.25 v4.1.0
% 1.44/1.58 % Syntax : Number of formulae : 20 ( 7 unt; 0 def)
% 1.44/1.58 % Number of atoms : 34 ( 29 equ)
% 1.44/1.58 % Maximal formula atoms : 3 ( 1 avg)
% 1.44/1.58 % Number of connectives : 32 ( 18 ~; 7 |; 1 &)
% 1.44/1.58 % ( 2 <=>; 4 =>; 0 <=; 0 <~>)
% 1.44/1.58 % Maximal formula depth : 6 ( 4 avg)
% 1.44/1.58 % Maximal term depth : 3 ( 1 avg)
% 1.44/1.58 % Number of predicates : 3 ( 2 usr; 0 prp; 2-2 aty)
% 1.44/1.58 % Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% 1.44/1.58 % Number of variables : 42 ( 34 !; 8 ?)
% 1.44/1.58 % SPC : FOF_THM_RFO_SEQ
% 1.44/1.58
% 1.44/1.58 % Comments : From the Landau in Naproche 0.45 collection.
% 1.44/1.58 %------------------------------------------------------------------------------
% 1.44/1.58 fof('dis(ex(cond(conseq(131), 0), 1))',conjecture,
% 1.44/1.58 ( ~ greater(vd203,vd204)
% 1.44/1.58 | ~ less(vd203,vd204) ) ).
% 1.44/1.58
% 1.44/1.58 fof('dis(ex(cond(conseq(131), 0), 0))',axiom,
% 1.44/1.58 ( vd203 != vd204
% 1.44/1.58 | ~ greater(vd203,vd204) ) ).
% 1.44/1.58
% 1.44/1.58 fof('def(cond(conseq(axiom(3)), 12), 1)',axiom,
% 1.44/1.58 ! [Vd198,Vd199] :
% 1.44/1.58 ( less(Vd199,Vd198)
% 1.44/1.58 <=> ? [Vd201] : Vd198 = vplus(Vd199,Vd201) ) ).
% 1.44/1.58
% 1.44/1.58 fof('def(cond(conseq(axiom(3)), 11), 1)',axiom,
% 1.44/1.58 ! [Vd193,Vd194] :
% 1.44/1.58 ( greater(Vd194,Vd193)
% 1.44/1.58 <=> ? [Vd196] : Vd194 = vplus(Vd193,Vd196) ) ).
% 1.44/1.58
% 1.44/1.58 fof('ass(cond(goal(88), 0), 0)',axiom,
% 1.44/1.58 ! [Vd120,Vd121] :
% 1.44/1.58 ( Vd120 = Vd121
% 1.44/1.58 | ? [Vd123] : Vd120 = vplus(Vd121,Vd123)
% 1.44/1.58 | ? [Vd125] : Vd121 = vplus(Vd120,Vd125) ) ).
% 1.49/1.58
% 1.49/1.58 fof('ass(cond(goal(88), 0), 1)',axiom,
% 1.49/1.58 ! [Vd120,Vd121] :
% 1.49/1.58 ( Vd120 != Vd121
% 1.49/1.58 | ~ ? [Vd125] : Vd121 = vplus(Vd120,Vd125) ) ).
% 1.49/1.58
% 1.49/1.58 fof('ass(cond(goal(88), 0), 2)',axiom,
% 1.49/1.58 ! [Vd120,Vd121] :
% 1.49/1.58 ( ~ ? [Vd123] : Vd120 = vplus(Vd121,Vd123)
% 1.49/1.58 | ~ ? [Vd125] : Vd121 = vplus(Vd120,Vd125) ) ).
% 1.49/1.58
% 1.49/1.58 fof('ass(cond(goal(88), 0), 3)',axiom,
% 1.49/1.58 ! [Vd120,Vd121] :
% 1.49/1.58 ( Vd120 != Vd121
% 1.49/1.58 | ~ ? [Vd123] : Vd120 = vplus(Vd121,Vd123) ) ).
% 1.49/1.58
% 1.49/1.58 fof('ass(cond(81, 0), 0)',axiom,
% 1.49/1.58 ! [Vd104,Vd105] :
% 1.49/1.58 ( Vd104 != Vd105
% 1.49/1.58 => ! [Vd107] : vplus(Vd107,Vd104) != vplus(Vd107,Vd105) ) ).
% 1.49/1.58
% 1.49/1.58 fof('ass(cond(73, 0), 0)',axiom,
% 1.49/1.58 ! [Vd92,Vd93] : Vd93 != vplus(Vd92,Vd93) ).
% 1.49/1.58
% 1.49/1.58 fof('ass(cond(61, 0), 0)',axiom,
% 1.49/1.58 ! [Vd78,Vd79] : vplus(Vd79,Vd78) = vplus(Vd78,Vd79) ).
% 1.49/1.58
% 1.49/1.58 fof('ass(cond(52, 0), 0)',axiom,
% 1.49/1.58 ! [Vd68,Vd69] : vplus(vsucc(Vd68),Vd69) = vsucc(vplus(Vd68,Vd69)) ).
% 1.49/1.58
% 1.49/1.58 fof('ass(cond(43, 0), 0)',axiom,
% 1.49/1.58 ! [Vd59] : vplus(v1,Vd59) = vsucc(Vd59) ).
% 1.49/1.58
% 1.49/1.58 fof('ass(cond(33, 0), 0)',axiom,
% 1.49/1.58 ! [Vd46,Vd47,Vd48] : vplus(vplus(Vd46,Vd47),Vd48) = vplus(Vd46,vplus(Vd47,Vd48)) ).
% 1.49/1.58
% 1.49/1.58 fof('qu(cond(conseq(axiom(3)), 3), and(holds(definiens(29), 45, 0), holds(definiens(29), 44, 0)))',axiom,
% 1.49/1.58 ! [Vd42,Vd43] :
% 1.49/1.58 ( vplus(Vd42,vsucc(Vd43)) = vsucc(vplus(Vd42,Vd43))
% 1.49/1.58 & vplus(Vd42,v1) = vsucc(Vd42) ) ).
% 1.49/1.58
% 1.49/1.58 fof('ass(cond(20, 0), 0)',axiom,
% 1.49/1.58 ! [Vd24] :
% 1.49/1.58 ( Vd24 != v1
% 1.49/1.58 => Vd24 = vsucc(vskolem2(Vd24)) ) ).
% 1.49/1.58
% 1.49/1.58 fof('ass(cond(12, 0), 0)',axiom,
% 1.49/1.58 ! [Vd16] : vsucc(Vd16) != Vd16 ).
% 1.49/1.58
% 1.49/1.58 fof('ass(cond(6, 0), 0)',axiom,
% 1.49/1.58 ! [Vd7,Vd8] :
% 1.49/1.58 ( Vd7 != Vd8
% 1.49/1.58 => vsucc(Vd7) != vsucc(Vd8) ) ).
% 1.49/1.58
% 1.49/1.58 fof('qu(antec(axiom(3)), imp(antec(axiom(3))))',axiom,
% 1.49/1.58 ! [Vd3,Vd4] :
% 1.49/1.58 ( vsucc(Vd3) = vsucc(Vd4)
% 1.49/1.58 => Vd3 = Vd4 ) ).
% 1.49/1.58
% 1.49/1.58 fof('qu(restrictor(axiom(1)), holds(scope(axiom(1)), 2, 0))',axiom,
% 1.49/1.59 ! [Vd1] : vsucc(Vd1) != v1 ).
% 1.49/1.59
% 1.49/1.59 %------------------------------------------------------------------------------
% 1.49/1.59 %-------------------------------------------
% 1.49/1.59 % Proof found
% 1.49/1.59 % SZS status Theorem for theBenchmark
% 1.49/1.59 % SZS output start Proof
% 1.49/1.59 %ClaNum:41(EqnAxiom:18)
% 1.49/1.59 %VarNum:80(SingletonVarNum:38)
% 1.49/1.59 %MaxLitNum:3
% 1.49/1.59 %MaxfuncDepth:2
% 1.49/1.59 %SharedTerms:7
% 1.49/1.59 %goalClause: 19 20
% 1.49/1.59 %singleGoalClaCount:2
% 1.49/1.59 [19]P1(a1,a7)
% 1.49/1.59 [20]P2(a1,a7)
% 1.49/1.59 [27]~E(f8(x271,a2),x271)
% 1.49/1.59 [22]E(f8(x221,x222),f8(x222,x221))
% 1.49/1.59 [28]~E(f8(x281,x282),x282)
% 1.49/1.59 [24]E(f8(f8(x241,a2),x242),f8(f8(x241,x242),a2))
% 1.49/1.59 [25]E(f8(f8(x251,x252),x253),f8(x251,f8(x252,x253)))
% 1.49/1.59 [29]~E(a7,a1)+~P1(a1,a7)
% 1.49/1.59 [30]E(x301,a2)+E(f8(f9(x301),a2),x301)
% 1.49/1.59 [36]E(x361,x362)+~E(f8(x361,a2),f8(x362,a2))
% 1.49/1.59 [39]~P2(x391,x392)+E(f8(x391,f3(x392,x391)),x392)
% 1.49/1.59 [40]~P1(x402,x401)+E(f8(x401,f4(x401,x402)),x402)
% 1.49/1.59 [31]~E(x311,x312)+~E(x312,f8(x311,x313))
% 1.49/1.59 [32]~E(x321,x322)+~E(x321,f8(x322,x323))
% 1.49/1.59 [33]P1(x331,x332)+~E(x331,f8(x332,x333))
% 1.49/1.59 [34]P2(x341,x342)+~E(x342,f8(x341,x343))
% 1.49/1.59 [37]E(x371,x372)+~E(f8(x373,x371),f8(x373,x372))
% 1.49/1.59 [38]~E(x381,f8(x382,x383))+~E(x382,f8(x381,x384))
% 1.49/1.59 [41]E(x411,x412)+E(f8(x411,f5(x411,x412)),x412)+E(f8(x412,f6(x411,x412)),x411)
% 1.49/1.59 %EqnAxiom
% 1.49/1.59 [1]E(x11,x11)
% 1.49/1.59 [2]E(x22,x21)+~E(x21,x22)
% 1.49/1.59 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33)
% 1.49/1.59 [4]~E(x41,x42)+E(f8(x41,x43),f8(x42,x43))
% 1.49/1.59 [5]~E(x51,x52)+E(f8(x53,x51),f8(x53,x52))
% 1.49/1.59 [6]~E(x61,x62)+E(f6(x61,x63),f6(x62,x63))
% 1.49/1.59 [7]~E(x71,x72)+E(f6(x73,x71),f6(x73,x72))
% 1.49/1.59 [8]~E(x81,x82)+E(f5(x81,x83),f5(x82,x83))
% 1.49/1.59 [9]~E(x91,x92)+E(f5(x93,x91),f5(x93,x92))
% 1.49/1.59 [10]~E(x101,x102)+E(f4(x101,x103),f4(x102,x103))
% 1.49/1.59 [11]~E(x111,x112)+E(f4(x113,x111),f4(x113,x112))
% 1.49/1.59 [12]~E(x121,x122)+E(f3(x121,x123),f3(x122,x123))
% 1.49/1.59 [13]~E(x131,x132)+E(f3(x133,x131),f3(x133,x132))
% 1.49/1.59 [14]~E(x141,x142)+E(f9(x141),f9(x142))
% 1.49/1.59 [15]P1(x152,x153)+~E(x151,x152)+~P1(x151,x153)
% 1.49/1.59 [16]P1(x163,x162)+~E(x161,x162)+~P1(x163,x161)
% 1.49/1.59 [17]P2(x172,x173)+~E(x171,x172)+~P2(x171,x173)
% 1.49/1.59 [18]P2(x183,x182)+~E(x181,x182)+~P2(x183,x181)
% 1.49/1.59
% 1.49/1.59 %-------------------------------------------
% 1.49/1.59 cnf(42,plain,
% 1.49/1.59 (P1(f8(x421,x422),x421)),
% 1.49/1.59 inference(equality_inference,[],[33])).
% 1.49/1.59 cnf(46,plain,
% 1.49/1.59 (~E(x461,f8(x462,x461))),
% 1.49/1.59 inference(scs_inference,[],[22,31])).
% 1.49/1.59 cnf(48,plain,
% 1.49/1.59 (~E(f8(f8(x481,x482),x483),x481)),
% 1.49/1.59 inference(scs_inference,[],[22,25,31,32])).
% 1.49/1.59 cnf(50,plain,
% 1.49/1.59 (P1(f8(x501,x502),x502)),
% 1.49/1.59 inference(scs_inference,[],[22,25,31,32,33])).
% 1.49/1.59 cnf(56,plain,
% 1.49/1.59 (E(f8(x561,f8(x562,x563)),f8(f8(x561,x562),x563))),
% 1.49/1.59 inference(scs_inference,[],[22,25,31,32,33,34,38,2])).
% 1.49/1.59 cnf(58,plain,
% 1.49/1.59 (E(f8(x581,f6(f8(x581,x581),x581)),f8(x581,x581))),
% 1.49/1.59 inference(scs_inference,[],[22,28,25,31,32,33,34,38,2,4,41])).
% 1.49/1.59 cnf(59,plain,
% 1.49/1.59 (~E(f8(x591,x592),x592)),
% 1.49/1.59 inference(rename_variables,[],[28])).
% 1.49/1.59 cnf(61,plain,
% 1.49/1.59 (E(f6(f8(x611,x611),x611),x611)),
% 1.49/1.59 inference(scs_inference,[],[22,28,25,31,32,33,34,38,2,4,41,37])).
% 1.49/1.59 cnf(63,plain,
% 1.49/1.59 (P1(x631,a7)+~E(a1,x631)),
% 1.49/1.59 inference(scs_inference,[],[19,22,28,25,31,32,33,34,38,2,4,41,37,15])).
% 1.49/1.59 cnf(66,plain,
% 1.49/1.59 (P2(x661,a7)+~E(a1,x661)),
% 1.49/1.59 inference(scs_inference,[],[19,20,22,28,59,25,31,32,33,34,38,2,4,41,37,15,3,16,17])).
% 1.49/1.59 cnf(74,plain,
% 1.49/1.59 (~E(f8(f8(x741,x742),x743),x741)),
% 1.49/1.59 inference(rename_variables,[],[48])).
% 1.49/1.59 cnf(76,plain,
% 1.49/1.59 (~P1(x761,f8(x761,x762))),
% 1.49/1.59 inference(scs_inference,[],[48,74,39,40])).
% 1.49/1.59 cnf(82,plain,
% 1.49/1.59 (E(f6(f8(x821,x821),x821),x821)),
% 1.49/1.59 inference(rename_variables,[],[61])).
% 1.49/1.59 cnf(90,plain,
% 1.49/1.59 (E(f6(f8(x901,x901),x901),x901)),
% 1.49/1.59 inference(rename_variables,[],[61])).
% 1.49/1.59 cnf(93,plain,
% 1.49/1.59 (~E(f8(x931,f8(x932,x933)),x932)),
% 1.49/1.59 inference(scs_inference,[],[58,50,61,82,56,48,74,39,40,38,33,31,32,2,34,4,15])).
% 1.49/1.59 cnf(99,plain,
% 1.49/1.59 (E(x991,f6(f8(x991,x991),x991))),
% 1.49/1.59 inference(scs_inference,[],[19,20,58,46,50,61,82,90,56,48,74,39,40,38,33,31,32,2,34,4,15,17,16,3,37])).
% 1.49/1.59 cnf(103,plain,
% 1.49/1.59 (P1(f6(f8(a1,a1),a1),a7)),
% 1.49/1.59 inference(scs_inference,[],[99,63])).
% 1.49/1.59 cnf(104,plain,
% 1.49/1.59 (E(x1041,f6(f8(x1041,x1041),x1041))),
% 1.49/1.59 inference(rename_variables,[],[99])).
% 1.49/1.59 cnf(105,plain,
% 1.49/1.59 (P2(f6(f8(a1,a1),a1),a7)),
% 1.49/1.59 inference(scs_inference,[],[99,104,63,66])).
% 1.49/1.59 cnf(107,plain,
% 1.49/1.59 (~E(f8(f8(x1071,x1072),x1073),x1072)),
% 1.49/1.59 inference(scs_inference,[],[93,99,104,63,66,5])).
% 1.49/1.59 cnf(113,plain,
% 1.49/1.59 (~E(f8(x1131,x1132),f8(f8(x1131,a2),x1132))),
% 1.49/1.59 inference(scs_inference,[],[93,99,104,24,63,66,5,39,38,31])).
% 1.49/1.59 cnf(121,plain,
% 1.49/1.59 (E(f8(f8(x1211,x1212),a2),f8(f8(x1211,a2),x1212))),
% 1.49/1.59 inference(scs_inference,[],[93,99,104,24,63,66,5,39,38,31,32,33,34,2])).
% 1.49/1.59 cnf(147,plain,
% 1.49/1.59 (~E(a7,f8(f6(f8(a1,a1),a1),x1471))),
% 1.49/1.59 inference(scs_inference,[],[103,76,107,113,121,40,38,31,32,34,33,4,16])).
% 1.49/1.59 cnf(414,plain,
% 1.49/1.59 (~P1(a7,f6(f8(a1,a1),a1))),
% 1.49/1.59 inference(scs_inference,[],[147,2,40])).
% 1.49/1.59 cnf(417,plain,
% 1.49/1.59 ($false),
% 1.49/1.59 inference(scs_inference,[],[414,105,42,15,39]),
% 1.49/1.59 ['proof']).
% 1.49/1.59 % SZS output end Proof
% 1.49/1.59 % Total time :1.100000s
%------------------------------------------------------------------------------