%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : PRO010+1 : TPTP v9.0.0. Released v4.0.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 : n019.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 08:24:11 PM UTC 2025
% Result : Theorem 5.41s 2.25s
% Output : CNFRefutation 5.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 8
% Syntax : Number of formulae : 57 ( 21 unt; 0 typ; 0 def)
% Number of atoms : 122 ( 16 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 118 ( 53 ~; 40 |; 16 &)
% ( 2 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 19 ( 17 usr; 1 prp; 0-3 aty)
% Number of functors : 26 ( 26 usr; 6 con; 0-4 aty)
% Number of variables : 64 ( 53 !; 11 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ next_subocc > min_precedes > subactivity_occurrence > subactivity > root_occ > root > precedes > occurrence_of > leaf_occ > leaf > earlier > atocc > legal > atomic > arboreal > activity_occurrence > activity > #nlpp > tptp4 > tptp3 > tptp2 > tptp1 > tptp0 > #skF_11 > #skF_16 > #skF_6 > #skF_18 > #skF_13 > #skF_1 > #skF_20 > #skF_19 > #skF_14 > #skF_12 > #skF_5 > #skF_2 > #skF_17 > #skF_3 > #skF_8 > #skF_7 > #skF_21 > #skF_9 > #skF_15 > #skF_4 > #skF_10
%Foreground sorts:
%Background operators:
%Foreground operators:
tff('#skF_11',type,
'#skF_11': ( $i * $i ) > $i ).
tff(arboreal,type,
arboreal: $i > $o ).
tff('#skF_16',type,
'#skF_16': $i > $i ).
tff(tptp1,type,
tptp1: $i ).
tff('#skF_6',type,
'#skF_6': ( $i * $i ) > $i ).
tff('#skF_18',type,
'#skF_18': $i > $i ).
tff('#skF_13',type,
'#skF_13': ( $i * $i * $i * $i ) > $i ).
tff(subactivity,type,
subactivity: ( $i * $i ) > $o ).
tff(root,type,
root: ( $i * $i ) > $o ).
tff('#skF_1',type,
'#skF_1': $i > $i ).
tff('#skF_20',type,
'#skF_20': ( $i * $i ) > $i ).
tff(tptp2,type,
tptp2: $i ).
tff(leaf,type,
leaf: ( $i * $i ) > $o ).
tff(tptp0,type,
tptp0: $i ).
tff('#skF_19',type,
'#skF_19': $i ).
tff(root_occ,type,
root_occ: ( $i * $i ) > $o ).
tff(tptp3,type,
tptp3: $i ).
tff(occurrence_of,type,
occurrence_of: ( $i * $i ) > $o ).
tff(atomic,type,
atomic: $i > $o ).
tff('#skF_14',type,
'#skF_14': ( $i * $i ) > $i ).
tff(tptp4,type,
tptp4: $i ).
tff('#skF_12',type,
'#skF_12': ( $i * $i ) > $i ).
tff(legal,type,
legal: $i > $o ).
tff(earlier,type,
earlier: ( $i * $i ) > $o ).
tff(activity_occurrence,type,
activity_occurrence: $i > $o ).
tff('#skF_5',type,
'#skF_5': ( $i * $i * $i ) > $i ).
tff('#skF_2',type,
'#skF_2': ( $i * $i * $i ) > $i ).
tff(leaf_occ,type,
leaf_occ: ( $i * $i ) > $o ).
tff('#skF_17',type,
'#skF_17': $i > $i ).
tff(activity,type,
activity: $i > $o ).
tff(min_precedes,type,
min_precedes: ( $i * $i * $i ) > $o ).
tff(precedes,type,
precedes: ( $i * $i ) > $o ).
tff('#skF_3',type,
'#skF_3': ( $i * $i * $i ) > $i ).
tff(subactivity_occurrence,type,
subactivity_occurrence: ( $i * $i ) > $o ).
tff(next_subocc,type,
next_subocc: ( $i * $i * $i ) > $o ).
tff('#skF_8',type,
'#skF_8': ( $i * $i * $i ) > $i ).
tff('#skF_7',type,
'#skF_7': ( $i * $i ) > $i ).
tff(atocc,type,
atocc: ( $i * $i ) > $o ).
tff('#skF_21',type,
'#skF_21': ( $i * $i ) > $i ).
tff('#skF_9',type,
'#skF_9': ( $i * $i ) > $i ).
tff('#skF_15',type,
'#skF_15': ( $i * $i ) > $i ).
tff('#skF_4',type,
'#skF_4': ( $i * $i ) > $i ).
tff('#skF_10',type,
'#skF_10': ( $i * $i * $i ) > $i ).
tff(f_354,negated_conjecture,
~ ! [X109] :
( occurrence_of(X109,tptp0)
=> ? [X110,X111] :
( leaf_occ(X111,X109)
& ( occurrence_of(X111,tptp1)
=> ~ ? [X112] :
( occurrence_of(X112,tptp2)
& min_precedes(X110,X112,tptp0) ) )
& ( occurrence_of(X111,tptp2)
=> ~ ? [X113] :
( occurrence_of(X113,tptp1)
& min_precedes(X110,X113,tptp0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
tff(f_313,axiom,
! [X105] :
( occurrence_of(X105,tptp0)
=> ? [X106,X107,X108] :
( occurrence_of(X106,tptp3)
& root_occ(X106,X105)
& occurrence_of(X107,tptp4)
& next_subocc(X106,X107,tptp0)
& ( occurrence_of(X108,tptp1)
| occurrence_of(X108,tptp2) )
& next_subocc(X107,X108,tptp0)
& leaf_occ(X108,X105) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_35) ).
tff(f_332,axiom,
tptp1 != tptp2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_47) ).
tff(f_166,axiom,
! [X56,X57] :
( leaf(X56,X57)
<=> ( ( root(X56,X57)
| ? [X58] : min_precedes(X58,X56,X57) )
& ~ ? [X59] : min_precedes(X56,X59,X57) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_21) ).
tff(f_294,axiom,
! [X102,X103] :
( leaf_occ(X102,X103)
<=> ? [X104] :
( occurrence_of(X103,X104)
& subactivity_occurrence(X102,X103)
& leaf(X102,X104) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_34) ).
tff(f_43,axiom,
! [X4,X5,X6] :
( ( occurrence_of(X4,X5)
& occurrence_of(X4,X6) )
=> ( X5 = X6 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_02) ).
tff(f_191,axiom,
! [X67,X68] :
( subactivity_occurrence(X67,X68)
=> ( activity_occurrence(X67)
& activity_occurrence(X68) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_24) ).
tff(f_37,axiom,
! [X2] :
( activity_occurrence(X2)
=> ? [X3] :
( activity(X3)
& occurrence_of(X2,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos_01) ).
tff(c_172,plain,
occurrence_of('#skF_19',tptp0),
inference(cnfTransformation,[status(thm)],[f_354]) ).
tff(c_134,plain,
! [X105_118] :
( leaf_occ('#skF_18'(X105_118),X105_118)
| ~ occurrence_of(X105_118,tptp0) ),
inference(cnfTransformation,[status(thm)],[f_313]) ).
tff(c_170,plain,
tptp2 != tptp1,
inference(cnfTransformation,[status(thm)],[f_332]) ).
tff(c_338,plain,
! [X111_190,X110_191] :
( occurrence_of(X111_190,tptp1)
| min_precedes(X110_191,'#skF_21'(X110_191,X111_190),tptp0)
| ~ leaf_occ(X111_190,'#skF_19') ),
inference(cnfTransformation,[status(thm)],[f_354]) ).
tff(c_64,plain,
! [X56_57,X59_64,X57_58] :
( ~ min_precedes(X56_57,X59_64,X57_58)
| ~ leaf(X56_57,X57_58) ),
inference(cnfTransformation,[status(thm)],[f_166]) ).
tff(c_353,plain,
! [X110_191,X111_190] :
( ~ leaf(X110_191,tptp0)
| occurrence_of(X111_190,tptp1)
| ~ leaf_occ(X111_190,'#skF_19') ),
inference(resolution,[status(thm)],[c_338,c_64]) ).
tff(c_953,plain,
! [X110_191] : ~ leaf(X110_191,tptp0),
inference(splitLeft,[status(thm)],[c_353]) ).
tff(c_132,plain,
! [X103_114,X102_113] :
( occurrence_of(X103_114,'#skF_15'(X102_113,X103_114))
| ~ leaf_occ(X102_113,X103_114) ),
inference(cnfTransformation,[status(thm)],[f_294]) ).
tff(c_579,plain,
! [X6_244,X5_245,X4_246] :
( ( X6_244 = X5_245 )
| ~ occurrence_of(X4_246,X6_244)
| ~ occurrence_of(X4_246,X5_245) ),
inference(cnfTransformation,[status(thm)],[f_43]) ).
tff(c_613,plain,
! [X5_247] :
( ( tptp0 = X5_247 )
| ~ occurrence_of('#skF_19',X5_247) ),
inference(resolution,[status(thm)],[c_172,c_579]) ).
tff(c_725,plain,
! [X102_255] :
( ( '#skF_15'(X102_255,'#skF_19') = tptp0 )
| ~ leaf_occ(X102_255,'#skF_19') ),
inference(resolution,[status(thm)],[c_132,c_613]) ).
tff(c_729,plain,
( ( '#skF_15'('#skF_18'('#skF_19'),'#skF_19') = tptp0 )
| ~ occurrence_of('#skF_19',tptp0) ),
inference(resolution,[status(thm)],[c_134,c_725]) ).
tff(c_732,plain,
'#skF_15'('#skF_18'('#skF_19'),'#skF_19') = tptp0,
inference(demodulation,[status(thm),theory(equality)],[c_172,c_729]) ).
tff(c_128,plain,
! [X102_113,X103_114] :
( leaf(X102_113,'#skF_15'(X102_113,X103_114))
| ~ leaf_occ(X102_113,X103_114) ),
inference(cnfTransformation,[status(thm)],[f_294]) ).
tff(c_736,plain,
( leaf('#skF_18'('#skF_19'),tptp0)
| ~ leaf_occ('#skF_18'('#skF_19'),'#skF_19') ),
inference(superposition,[status(thm),theory(equality)],[c_732,c_128]) ).
tff(c_1081,plain,
~ leaf_occ('#skF_18'('#skF_19'),'#skF_19'),
inference(negUnitSimplification,[status(thm)],[c_953,c_736]) ).
tff(c_1084,plain,
~ occurrence_of('#skF_19',tptp0),
inference(resolution,[status(thm)],[c_134,c_1081]) ).
tff(c_1088,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_172,c_1084]) ).
tff(c_1089,plain,
! [X111_190] :
( occurrence_of(X111_190,tptp1)
| ~ leaf_occ(X111_190,'#skF_19') ),
inference(splitRight,[status(thm)],[c_353]) ).
tff(c_263,plain,
! [X105_175] :
( leaf_occ('#skF_18'(X105_175),X105_175)
| ~ occurrence_of(X105_175,tptp0) ),
inference(cnfTransformation,[status(thm)],[f_313]) ).
tff(c_230,plain,
! [X102_157,X103_158] :
( subactivity_occurrence(X102_157,X103_158)
| ~ leaf_occ(X102_157,X103_158) ),
inference(cnfTransformation,[status(thm)],[f_294]) ).
tff(c_90,plain,
! [X67_76,X68_77] :
( activity_occurrence(X67_76)
| ~ subactivity_occurrence(X67_76,X68_77) ),
inference(cnfTransformation,[status(thm)],[f_191]) ).
tff(c_237,plain,
! [X102_157,X103_158] :
( activity_occurrence(X102_157)
| ~ leaf_occ(X102_157,X103_158) ),
inference(resolution,[status(thm)],[c_230,c_90]) ).
tff(c_271,plain,
! [X105_175] :
( activity_occurrence('#skF_18'(X105_175))
| ~ occurrence_of(X105_175,tptp0) ),
inference(resolution,[status(thm)],[c_263,c_237]) ).
tff(c_416,plain,
! [X110_199,X111_200] :
( min_precedes(X110_199,'#skF_20'(X110_199,X111_200),tptp0)
| occurrence_of(X111_200,tptp2)
| ~ leaf_occ(X111_200,'#skF_19') ),
inference(cnfTransformation,[status(thm)],[f_354]) ).
tff(c_431,plain,
! [X110_199,X111_200] :
( ~ leaf(X110_199,tptp0)
| occurrence_of(X111_200,tptp2)
| ~ leaf_occ(X111_200,'#skF_19') ),
inference(resolution,[status(thm)],[c_416,c_64]) ).
tff(c_862,plain,
! [X110_199] : ~ leaf(X110_199,tptp0),
inference(splitLeft,[status(thm)],[c_431]) ).
tff(c_864,plain,
~ leaf_occ('#skF_18'('#skF_19'),'#skF_19'),
inference(negUnitSimplification,[status(thm)],[c_862,c_736]) ).
tff(c_867,plain,
~ occurrence_of('#skF_19',tptp0),
inference(resolution,[status(thm)],[c_134,c_864]) ).
tff(c_871,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_172,c_867]) ).
tff(c_873,plain,
! [X111_267] :
( occurrence_of(X111_267,tptp2)
| ~ leaf_occ(X111_267,'#skF_19') ),
inference(splitRight,[status(thm)],[c_431]) ).
tff(c_6,plain,
! [X2_3] :
( occurrence_of(X2_3,'#skF_1'(X2_3))
| ~ activity_occurrence(X2_3) ),
inference(cnfTransformation,[status(thm)],[f_37]) ).
tff(c_609,plain,
! [X5_245,X2_3] :
( ( X5_245 = '#skF_1'(X2_3) )
| ~ occurrence_of(X2_3,X5_245)
| ~ activity_occurrence(X2_3) ),
inference(resolution,[status(thm)],[c_6,c_579]) ).
tff(c_906,plain,
! [X111_268] :
( ( '#skF_1'(X111_268) = tptp2 )
| ~ activity_occurrence(X111_268)
| ~ leaf_occ(X111_268,'#skF_19') ),
inference(resolution,[status(thm)],[c_873,c_609]) ).
tff(c_910,plain,
( ( '#skF_1'('#skF_18'('#skF_19')) = tptp2 )
| ~ activity_occurrence('#skF_18'('#skF_19'))
| ~ occurrence_of('#skF_19',tptp0) ),
inference(resolution,[status(thm)],[c_134,c_906]) ).
tff(c_913,plain,
( ( '#skF_1'('#skF_18'('#skF_19')) = tptp2 )
| ~ activity_occurrence('#skF_18'('#skF_19')) ),
inference(demodulation,[status(thm),theory(equality)],[c_172,c_910]) ).
tff(c_914,plain,
~ activity_occurrence('#skF_18'('#skF_19')),
inference(splitLeft,[status(thm)],[c_913]) ).
tff(c_922,plain,
~ occurrence_of('#skF_19',tptp0),
inference(resolution,[status(thm)],[c_271,c_914]) ).
tff(c_926,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_172,c_922]) ).
tff(c_928,plain,
activity_occurrence('#skF_18'('#skF_19')),
inference(splitRight,[status(thm)],[c_913]) ).
tff(c_927,plain,
'#skF_1'('#skF_18'('#skF_19')) = tptp2,
inference(splitRight,[status(thm)],[c_913]) ).
tff(c_938,plain,
( occurrence_of('#skF_18'('#skF_19'),tptp2)
| ~ activity_occurrence('#skF_18'('#skF_19')) ),
inference(superposition,[status(thm),theory(equality)],[c_927,c_6]) ).
tff(c_949,plain,
occurrence_of('#skF_18'('#skF_19'),tptp2),
inference(demodulation,[status(thm),theory(equality)],[c_928,c_938]) ).
tff(c_10,plain,
! [X6_7,X5_6,X4_5] :
( ( X6_7 = X5_6 )
| ~ occurrence_of(X4_5,X6_7)
| ~ occurrence_of(X4_5,X5_6) ),
inference(cnfTransformation,[status(thm)],[f_43]) ).
tff(c_1155,plain,
! [X5_278] :
( ( tptp2 = X5_278 )
| ~ occurrence_of('#skF_18'('#skF_19'),X5_278) ),
inference(resolution,[status(thm)],[c_949,c_10]) ).
tff(c_1159,plain,
( ( tptp2 = tptp1 )
| ~ leaf_occ('#skF_18'('#skF_19'),'#skF_19') ),
inference(resolution,[status(thm)],[c_1089,c_1155]) ).
tff(c_1185,plain,
~ leaf_occ('#skF_18'('#skF_19'),'#skF_19'),
inference(negUnitSimplification,[status(thm)],[c_170,c_1159]) ).
tff(c_1198,plain,
~ occurrence_of('#skF_19',tptp0),
inference(resolution,[status(thm)],[c_134,c_1185]) ).
tff(c_1202,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_172,c_1198]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : PRO010+1 : TPTP v9.0.0. Released v4.0.0.
% 0.11/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.12/0.34 % Computer : n019.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 Apr 8 16:58:17 EDT 2025
% 0.12/0.34 % CPUTime :
% 5.41/2.25 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.41/2.26
% 5.41/2.26 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------