%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : NUM842+2 : TPTP v9.0.0. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n026.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 : Wed Apr 9 07:57:18 PM UTC 2025
% Result : Theorem 76.35s 61.05s
% Output : CNFRefutation 76.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 17
% Syntax : Number of formulae : 91 ( 39 unt; 0 typ; 0 def)
% Number of atoms : 161 ( 30 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 130 ( 60 ~; 55 |; 5 &)
% ( 2 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-2 aty)
% Number of variables : 101 ( 101 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ less > leq > greater > geq > vplus > #nlpp > vsucc > vskolem2 > vd356 > vd355 > vd354 > vd353 > v1 > #skF_3 > #skF_2 > #skF_1 > #skF_4
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(greater,type,
greater: ( $i * $i ) > $o ).
tff(vd354,type,
vd354: $i ).
tff(vplus,type,
vplus: ( $i * $i ) > $i ).
tff('#skF_3',type,
'#skF_3': ( $i * $i ) > $i ).
tff(less,type,
less: ( $i * $i ) > $o ).
tff(vskolem2,type,
vskolem2: $i > $i ).
tff(vd356,type,
vd356: $i ).
tff(vsucc,type,
vsucc: $i > $i ).
tff(vd353,type,
vd353: $i ).
tff(vd355,type,
vd355: $i ).
tff(v1,type,
v1: $i ).
tff(geq,type,
geq: ( $i * $i ) > $o ).
tff(leq,type,
leq: ( $i * $i ) > $o ).
tff('#skF_2',type,
'#skF_2': ( $i * $i ) > $i ).
tff('#skF_1',type,
'#skF_1': ( $i * $i ) > $i ).
tff('#skF_4',type,
'#skF_4': ( $i * $i ) > $i ).
tff(f_142,axiom,
! [Vd203,Vd204] :
( ( Vd203 != Vd204 )
| ~ greater(Vd203,Vd204) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ass(cond(goal(130),0),3)) ).
tff(f_110,axiom,
! [Vd244,Vd245] :
( geq(Vd245,Vd244)
<=> ( greater(Vd245,Vd244)
| ( Vd245 = Vd244 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def(cond(conseq(axiom(3)),16),1)) ).
tff(f_130,axiom,
! [Vd203,Vd204] :
( ( Vd203 != Vd204 )
| ~ less(Vd203,Vd204) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ass(cond(goal(130),0),1)) ).
tff(f_36,axiom,
( ( greater(vd355,vd356)
& geq(vd353,vd354) )
| ( geq(vd355,vd356)
& greater(vd353,vd354) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dis(antec(218))) ).
tff(f_66,axiom,
! [Vd301,Vd302,Vd303] :
( greater(Vd301,Vd302)
=> greater(vplus(Vd301,Vd303),vplus(Vd302,Vd303)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ass(cond(goal(193),0),2)) ).
tff(f_42,axiom,
! [Vd337,Vd338,Vd340,Vd341] :
( ( greater(Vd340,Vd341)
& greater(Vd337,Vd338) )
=> greater(vplus(Vd337,Vd340),vplus(Vd338,Vd341)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ass(cond(209,0),0)) ).
tff(f_29,negated_conjecture,
~ greater(vplus(vd353,vd355),vplus(vd354,vd356)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',holds(conseq(218),361,0)) ).
tff(f_194,axiom,
! [Vd78,Vd79] : ( vplus(Vd79,Vd78) = vplus(Vd78,Vd79) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ass(cond(61,0),0)) ).
tff(f_124,axiom,
! [Vd203,Vd204] :
( ( Vd203 = Vd204 )
| greater(Vd203,Vd204)
| less(Vd203,Vd204) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ass(cond(goal(130),0),0)) ).
tff(f_104,axiom,
! [Vd249,Vd250] :
( leq(Vd250,Vd249)
<=> ( less(Vd250,Vd249)
| ( Vd250 = Vd249 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def(cond(conseq(axiom(3)),17),1)) ).
tff(f_94,axiom,
! [Vd258,Vd259] :
( leq(Vd258,Vd259)
=> geq(Vd259,Vd258) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ass(cond(163,0),0)) ).
tff(f_118,axiom,
! [Vd208,Vd209] :
( greater(Vd208,Vd209)
=> less(Vd209,Vd208) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ass(cond(140,0),0)) ).
tff(f_98,axiom,
! [Vd254,Vd255] :
( geq(Vd254,Vd255)
=> leq(Vd255,Vd254) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ass(cond(158,0),0)) ).
tff(f_84,axiom,
! [Vd281,Vd282,Vd283] :
( ( ( less(Vd282,Vd283)
& leq(Vd281,Vd282) )
| ( leq(Vd282,Vd283)
& less(Vd281,Vd282) ) )
=> less(Vd281,Vd283) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ass(cond(goal(177),0),0)) ).
tff(f_46,axiom,
! [Vd328,Vd329,Vd330] :
( less(vplus(Vd328,Vd330),vplus(Vd329,Vd330))
=> less(Vd328,Vd329) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ass(cond(goal(202),0),0)) ).
tff(f_189,axiom,
! [Vd104,Vd105] :
( ( Vd104 != Vd105 )
=> ! [Vd107] : ( vplus(Vd107,Vd104) != vplus(Vd107,Vd105) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ass(cond(81,0),0)) ).
tff(f_136,axiom,
! [Vd203,Vd204] :
( ~ greater(Vd203,Vd204)
| ~ less(Vd203,Vd204) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ass(cond(goal(130),0),2)) ).
tff(c_63,plain,
! [Vd204_53] : ~ greater(Vd204_53,Vd204_53),
inference(cnfTransformation,[status(thm)],[f_142]) ).
tff(c_49,plain,
! [Vd245_41] : geq(Vd245_41,Vd245_41),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_59,plain,
! [Vd204_49] : ~ less(Vd204_49,Vd204_49),
inference(cnfTransformation,[status(thm)],[f_130]) ).
tff(c_4,plain,
( geq(vd353,vd354)
| greater(vd353,vd354) ),
inference(cnfTransformation,[status(thm)],[f_36]) ).
tff(c_200,plain,
greater(vd353,vd354),
inference(splitLeft,[status(thm)],[c_4]) ).
tff(c_25,plain,
! [Vd301_20,Vd303_22,Vd302_21] :
( greater(vplus(Vd301_20,Vd303_22),vplus(Vd302_21,Vd303_22))
| ~ greater(Vd301_20,Vd302_21) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_10,plain,
( greater(vd355,vd356)
| geq(vd355,vd356) ),
inference(cnfTransformation,[status(thm)],[f_36]) ).
tff(c_626,plain,
geq(vd355,vd356),
inference(splitLeft,[status(thm)],[c_10]) ).
tff(c_47,plain,
! [Vd245_41,Vd244_40] :
( ( Vd245_41 = Vd244_40 )
| greater(Vd245_41,Vd244_40)
| ~ geq(Vd245_41,Vd244_40) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_2891,plain,
! [Vd337_295,Vd340_296,Vd338_297,Vd341_298] :
( greater(vplus(Vd337_295,Vd340_296),vplus(Vd338_297,Vd341_298))
| ~ greater(Vd337_295,Vd338_297)
| ~ greater(Vd340_296,Vd341_298) ),
inference(cnfTransformation,[status(thm)],[f_42]) ).
tff(c_2,plain,
~ greater(vplus(vd353,vd355),vplus(vd354,vd356)),
inference(cnfTransformation,[status(thm)],[f_29]) ).
tff(c_2917,plain,
( ~ greater(vd353,vd354)
| ~ greater(vd355,vd356) ),
inference(resolution,[status(thm)],[c_2891,c_2]) ).
tff(c_2985,plain,
~ greater(vd355,vd356),
inference(demodulation,[status(thm),theory(equality)],[c_200,c_2917]) ).
tff(c_2989,plain,
( ( vd356 = vd355 )
| ~ geq(vd355,vd356) ),
inference(resolution,[status(thm)],[c_47,c_2985]) ).
tff(c_2992,plain,
vd356 = vd355,
inference(demodulation,[status(thm),theory(equality)],[c_626,c_2989]) ).
tff(c_2996,plain,
~ greater(vplus(vd353,vd355),vplus(vd354,vd355)),
inference(demodulation,[status(thm),theory(equality)],[c_2992,c_2]) ).
tff(c_3007,plain,
~ greater(vd353,vd354),
inference(resolution,[status(thm)],[c_25,c_2996]) ).
tff(c_3017,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_200,c_3007]) ).
tff(c_3019,plain,
~ geq(vd355,vd356),
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_3018,plain,
greater(vd355,vd356),
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_51,plain,
! [Vd245_41,Vd244_40] :
( ~ greater(Vd245_41,Vd244_40)
| geq(Vd245_41,Vd244_40) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_3023,plain,
geq(vd355,vd356),
inference(resolution,[status(thm)],[c_3018,c_51]) ).
tff(c_3024,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_3019,c_3023]) ).
tff(c_3026,plain,
~ greater(vd353,vd354),
inference(splitRight,[status(thm)],[c_4]) ).
tff(c_6,plain,
( greater(vd355,vd356)
| greater(vd353,vd354) ),
inference(cnfTransformation,[status(thm)],[f_36]) ).
tff(c_3247,plain,
greater(vd355,vd356),
inference(negUnitSimplification,[status(thm)],[c_3026,c_6]) ).
tff(c_85,plain,
! [Vd79_89,Vd78_88] : ( vplus(Vd79_89,Vd78_88) = vplus(Vd78_88,Vd79_89) ),
inference(cnfTransformation,[status(thm)],[f_194]) ).
tff(c_5598,plain,
! [Vd301_462,Vd303_463,Vd302_464] :
( greater(vplus(Vd301_462,Vd303_463),vplus(Vd302_464,Vd303_463))
| ~ greater(Vd301_462,Vd302_464) ),
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_5656,plain,
! [Vd301_462,Vd79_89,Vd78_88] :
( greater(vplus(Vd301_462,Vd79_89),vplus(Vd79_89,Vd78_88))
| ~ greater(Vd301_462,Vd78_88) ),
inference(superposition,[status(thm),theory(equality)],[c_85,c_5598]) ).
tff(c_4050,plain,
! [Vd203_387,Vd204_388] :
( less(Vd203_387,Vd204_388)
| greater(Vd203_387,Vd204_388)
| ( Vd204_388 = Vd203_387 ) ),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_45,plain,
! [Vd250_39,Vd249_38] :
( ~ less(Vd250_39,Vd249_38)
| leq(Vd250_39,Vd249_38) ),
inference(cnfTransformation,[status(thm)],[f_104]) ).
tff(c_16246,plain,
! [Vd203_762,Vd204_763] :
( leq(Vd203_762,Vd204_763)
| greater(Vd203_762,Vd204_763)
| ( Vd204_763 = Vd203_762 ) ),
inference(resolution,[status(thm)],[c_4050,c_45]) ).
tff(c_37,plain,
! [Vd259_35,Vd258_34] :
( geq(Vd259_35,Vd258_34)
| ~ leq(Vd258_34,Vd259_35) ),
inference(cnfTransformation,[status(thm)],[f_94]) ).
tff(c_37592,plain,
! [Vd204_1081,Vd203_1082] :
( geq(Vd204_1081,Vd203_1082)
| greater(Vd203_1082,Vd204_1081)
| ( Vd204_1081 = Vd203_1082 ) ),
inference(resolution,[status(thm)],[c_16246,c_37]) ).
tff(c_3025,plain,
geq(vd353,vd354),
inference(splitRight,[status(thm)],[c_4]) ).
tff(c_3925,plain,
! [Vd245_380,Vd244_381] :
( ( Vd245_380 = Vd244_381 )
| greater(Vd245_380,Vd244_381)
| ~ geq(Vd245_380,Vd244_381) ),
inference(cnfTransformation,[status(thm)],[f_110]) ).
tff(c_3963,plain,
( ( vd354 = vd353 )
| ~ geq(vd353,vd354) ),
inference(resolution,[status(thm)],[c_3925,c_3026]) ).
tff(c_3993,plain,
vd354 = vd353,
inference(demodulation,[status(thm),theory(equality)],[c_3025,c_3963]) ).
tff(c_4001,plain,
~ greater(vplus(vd353,vd355),vplus(vd353,vd356)),
inference(demodulation,[status(thm),theory(equality)],[c_3993,c_2]) ).
tff(c_37852,plain,
( geq(vplus(vd353,vd356),vplus(vd353,vd355))
| ( vplus(vd353,vd356) = vplus(vd353,vd355) ) ),
inference(resolution,[status(thm)],[c_37592,c_4001]) ).
tff(c_37877,plain,
vplus(vd353,vd356) = vplus(vd353,vd355),
inference(splitLeft,[status(thm)],[c_37852]) ).
tff(c_3994,plain,
( ( vplus(vd354,vd356) = vplus(vd353,vd355) )
| ~ geq(vplus(vd353,vd355),vplus(vd354,vd356)) ),
inference(resolution,[status(thm)],[c_3925,c_2]) ).
tff(c_4218,plain,
( ( vplus(vd353,vd356) = vplus(vd353,vd355) )
| ~ geq(vplus(vd353,vd355),vplus(vd353,vd356)) ),
inference(demodulation,[status(thm),theory(equality)],[c_3993,c_3993,c_3994]) ).
tff(c_4219,plain,
~ geq(vplus(vd353,vd355),vplus(vd353,vd356)),
inference(splitLeft,[status(thm)],[c_4218]) ).
tff(c_37878,plain,
~ geq(vplus(vd353,vd355),vplus(vd353,vd355)),
inference(demodulation,[status(thm),theory(equality)],[c_37877,c_4219]) ).
tff(c_37882,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_49,c_37878]) ).
tff(c_37883,plain,
geq(vplus(vd353,vd356),vplus(vd353,vd355)),
inference(splitRight,[status(thm)],[c_37852]) ).
tff(c_55,plain,
! [Vd209_45,Vd208_44] :
( less(Vd209_45,Vd208_44)
| ~ greater(Vd208_44,Vd209_45) ),
inference(cnfTransformation,[status(thm)],[f_118]) ).
tff(c_39,plain,
! [Vd255_37,Vd254_36] :
( leq(Vd255_37,Vd254_36)
| ~ geq(Vd254_36,Vd255_37) ),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_4896,plain,
! [Vd281_434,Vd282_435,Vd283_436] :
( ~ leq(Vd281_434,Vd282_435)
| ~ less(Vd282_435,Vd283_436)
| less(Vd281_434,Vd283_436) ),
inference(cnfTransformation,[status(thm)],[f_84]) ).
tff(c_21958,plain,
! [Vd254_876,Vd283_877,Vd255_878] :
( ~ less(Vd254_876,Vd283_877)
| less(Vd255_878,Vd283_877)
| ~ geq(Vd254_876,Vd255_878) ),
inference(resolution,[status(thm)],[c_39,c_4896]) ).
tff(c_236255,plain,
! [Vd255_2356,Vd208_2357,Vd209_2358] :
( less(Vd255_2356,Vd208_2357)
| ~ geq(Vd209_2358,Vd255_2356)
| ~ greater(Vd208_2357,Vd209_2358) ),
inference(resolution,[status(thm)],[c_55,c_21958]) ).
tff(c_236533,plain,
! [Vd208_2359] :
( less(vplus(vd353,vd355),Vd208_2359)
| ~ greater(Vd208_2359,vplus(vd353,vd356)) ),
inference(resolution,[status(thm)],[c_37883,c_236255]) ).
tff(c_5446,plain,
! [Vd328_456,Vd329_457,Vd330_458] :
( less(Vd328_456,Vd329_457)
| ~ less(vplus(Vd328_456,Vd330_458),vplus(Vd329_457,Vd330_458)) ),
inference(cnfTransformation,[status(thm)],[f_46]) ).
tff(c_5494,plain,
! [Vd328_456,Vd78_88,Vd79_89] :
( less(Vd328_456,Vd78_88)
| ~ less(vplus(Vd328_456,Vd79_89),vplus(Vd79_89,Vd78_88)) ),
inference(superposition,[status(thm),theory(equality)],[c_85,c_5446]) ).
tff(c_240345,plain,
! [Vd78_2376] :
( less(vd353,Vd78_2376)
| ~ greater(vplus(vd355,Vd78_2376),vplus(vd353,vd356)) ),
inference(resolution,[status(thm)],[c_236533,c_5494]) ).
tff(c_240477,plain,
( less(vd353,vd353)
| ~ greater(vd355,vd356) ),
inference(resolution,[status(thm)],[c_5656,c_240345]) ).
tff(c_240582,plain,
less(vd353,vd353),
inference(demodulation,[status(thm),theory(equality)],[c_3247,c_240477]) ).
tff(c_240584,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_59,c_240582]) ).
tff(c_240585,plain,
vplus(vd353,vd356) = vplus(vd353,vd355),
inference(splitRight,[status(thm)],[c_4218]) ).
tff(c_81,plain,
! [Vd107_85,Vd105_83,Vd104_82] :
( ( vplus(Vd107_85,Vd105_83) != vplus(Vd107_85,Vd104_82) )
| ( Vd105_83 = Vd104_82 ) ),
inference(cnfTransformation,[status(thm)],[f_189]) ).
tff(c_240615,plain,
! [Vd105_83] :
( ( vplus(vd353,vd355) != vplus(vd353,Vd105_83) )
| ( vd356 = Vd105_83 ) ),
inference(superposition,[status(thm),theory(equality)],[c_240585,c_81]) ).
tff(c_242352,plain,
vd356 = vd355,
inference(reflexivity,[status(thm),theory(equality)],[c_240615]) ).
tff(c_3408,plain,
! [Vd209_340,Vd208_341] :
( less(Vd209_340,Vd208_341)
| ~ greater(Vd208_341,Vd209_340) ),
inference(cnfTransformation,[status(thm)],[f_118]) ).
tff(c_61,plain,
! [Vd203_50,Vd204_51] :
( ~ less(Vd203_50,Vd204_51)
| ~ greater(Vd203_50,Vd204_51) ),
inference(cnfTransformation,[status(thm)],[f_136]) ).
tff(c_3453,plain,
! [Vd209_344,Vd208_345] :
( ~ greater(Vd209_344,Vd208_345)
| ~ greater(Vd208_345,Vd209_344) ),
inference(resolution,[status(thm)],[c_3408,c_61]) ).
tff(c_3467,plain,
~ greater(vd356,vd355),
inference(resolution,[status(thm)],[c_3247,c_3453]) ).
tff(c_3975,plain,
( ( vd356 = vd355 )
| ~ geq(vd356,vd355) ),
inference(resolution,[status(thm)],[c_3925,c_3467]) ).
tff(c_4071,plain,
~ geq(vd356,vd355),
inference(splitLeft,[status(thm)],[c_3975]) ).
tff(c_242399,plain,
~ geq(vd355,vd355),
inference(demodulation,[status(thm),theory(equality)],[c_242352,c_4071]) ).
tff(c_242413,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_49,c_242399]) ).
tff(c_242414,plain,
vd356 = vd355,
inference(splitRight,[status(thm)],[c_3975]) ).
tff(c_242418,plain,
greater(vd355,vd355),
inference(demodulation,[status(thm),theory(equality)],[c_242414,c_3247]) ).
tff(c_242421,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_63,c_242418]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUM842+2 : TPTP v9.0.0. Released v4.1.0.
% 0.03/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.33 % Computer : n026.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 Apr 8 15:34:38 EDT 2025
% 0.13/0.33 % CPUTime :
% 76.35/61.05 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 76.35/61.07
% 76.35/61.07 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------