%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SEU261+1 : TPTP v9.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n016.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:53:25 PM UTC 2025
% Result : Theorem 3.48s 1.95s
% Output : CNFRefutation 3.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 3
% Syntax : Number of formulae : 56 ( 27 unt; 0 typ; 0 def)
% Number of atoms : 173 ( 0 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 220 ( 103 ~; 91 |; 11 &)
% ( 1 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 10 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 28 ( 28 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ relation_isomorphism > well_ordering > well_founded_relation > transitive > relation > reflexive > function > connected > antisymmetric > #nlpp > #skF_2 > #skF_3 > #skF_1 > #skF_4
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(well_ordering,type,
well_ordering: $i > $o ).
tff(antisymmetric,type,
antisymmetric: $i > $o ).
tff(relation,type,
relation: $i > $o ).
tff(connected,type,
connected: $i > $o ).
tff(function,type,
function: $i > $o ).
tff(well_founded_relation,type,
well_founded_relation: $i > $o ).
tff('#skF_2',type,
'#skF_2': $i ).
tff('#skF_3',type,
'#skF_3': $i ).
tff('#skF_1',type,
'#skF_1': $i ).
tff(relation_isomorphism,type,
relation_isomorphism: ( $i * $i * $i ) > $o ).
tff('#skF_4',type,
'#skF_4': $i ).
tff(transitive,type,
transitive: $i > $o ).
tff(reflexive,type,
reflexive: $i > $o ).
tff(f_93,negated_conjecture,
~ ! [A] :
( relation(A)
=> ! [B] :
( relation(B)
=> ! [C] :
( ( relation(C)
& function(C) )
=> ( ( well_ordering(A)
& relation_isomorphism(A,B,C) )
=> well_ordering(B) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t54_wellord1) ).
tff(f_40,axiom,
! [A] :
( relation(A)
=> ( well_ordering(A)
<=> ( reflexive(A)
& transitive(A)
& antisymmetric(A)
& connected(A)
& well_founded_relation(A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_wellord1) ).
tff(f_76,axiom,
! [A] :
( relation(A)
=> ! [B] :
( relation(B)
=> ! [C] :
( ( relation(C)
& function(C) )
=> ( relation_isomorphism(A,B,C)
=> ( ( reflexive(A)
=> reflexive(B) )
& ( transitive(A)
=> transitive(B) )
& ( connected(A)
=> connected(B) )
& ( antisymmetric(A)
=> antisymmetric(B) )
& ( well_founded_relation(A)
=> well_founded_relation(B) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t53_wellord1) ).
tff(c_38,plain,
relation('#skF_3'),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_76,plain,
! [A_18] :
( well_ordering(A_18)
| ~ well_founded_relation(A_18)
| ~ connected(A_18)
| ~ antisymmetric(A_18)
| ~ transitive(A_18)
| ~ reflexive(A_18)
| ~ relation(A_18) ),
inference(cnfTransformation,[status(thm)],[f_40]) ).
tff(c_28,plain,
~ well_ordering('#skF_3'),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_94,plain,
( ~ well_founded_relation('#skF_3')
| ~ connected('#skF_3')
| ~ antisymmetric('#skF_3')
| ~ transitive('#skF_3')
| ~ reflexive('#skF_3')
| ~ relation('#skF_3') ),
inference(resolution,[status(thm)],[c_76,c_28]) ).
tff(c_102,plain,
( ~ well_founded_relation('#skF_3')
| ~ connected('#skF_3')
| ~ antisymmetric('#skF_3')
| ~ transitive('#skF_3')
| ~ reflexive('#skF_3') ),
inference(demodulation,[status(thm),theory(equality)],[c_38,c_94]) ).
tff(c_103,plain,
~ reflexive('#skF_3'),
inference(splitLeft,[status(thm)],[c_102]) ).
tff(c_40,plain,
relation('#skF_2'),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_36,plain,
relation('#skF_4'),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_34,plain,
function('#skF_4'),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_32,plain,
well_ordering('#skF_2'),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_69,plain,
! [A_17] :
( reflexive(A_17)
| ~ well_ordering(A_17)
| ~ relation(A_17) ),
inference(cnfTransformation,[status(thm)],[f_40]) ).
tff(c_72,plain,
( reflexive('#skF_2')
| ~ relation('#skF_2') ),
inference(resolution,[status(thm)],[c_32,c_69]) ).
tff(c_75,plain,
reflexive('#skF_2'),
inference(demodulation,[status(thm),theory(equality)],[c_40,c_72]) ).
tff(c_30,plain,
relation_isomorphism('#skF_2','#skF_3','#skF_4'),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_125,plain,
! [B_28,A_29,C_30] :
( reflexive(B_28)
| ~ reflexive(A_29)
| ~ relation_isomorphism(A_29,B_28,C_30)
| ~ function(C_30)
| ~ relation(C_30)
| ~ relation(B_28)
| ~ relation(A_29) ),
inference(cnfTransformation,[status(thm)],[f_76]) ).
tff(c_128,plain,
( reflexive('#skF_3')
| ~ reflexive('#skF_2')
| ~ function('#skF_4')
| ~ relation('#skF_4')
| ~ relation('#skF_3')
| ~ relation('#skF_2') ),
inference(resolution,[status(thm)],[c_30,c_125]) ).
tff(c_131,plain,
reflexive('#skF_3'),
inference(demodulation,[status(thm),theory(equality)],[c_40,c_38,c_36,c_34,c_75,c_128]) ).
tff(c_133,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_103,c_131]) ).
tff(c_134,plain,
( ~ transitive('#skF_3')
| ~ antisymmetric('#skF_3')
| ~ connected('#skF_3')
| ~ well_founded_relation('#skF_3') ),
inference(splitRight,[status(thm)],[c_102]) ).
tff(c_136,plain,
~ well_founded_relation('#skF_3'),
inference(splitLeft,[status(thm)],[c_134]) ).
tff(c_41,plain,
! [A_13] :
( well_founded_relation(A_13)
| ~ well_ordering(A_13)
| ~ relation(A_13) ),
inference(cnfTransformation,[status(thm)],[f_40]) ).
tff(c_44,plain,
( well_founded_relation('#skF_2')
| ~ relation('#skF_2') ),
inference(resolution,[status(thm)],[c_32,c_41]) ).
tff(c_47,plain,
well_founded_relation('#skF_2'),
inference(demodulation,[status(thm),theory(equality)],[c_40,c_44]) ).
tff(c_151,plain,
! [B_37,A_38,C_39] :
( well_founded_relation(B_37)
| ~ well_founded_relation(A_38)
| ~ relation_isomorphism(A_38,B_37,C_39)
| ~ function(C_39)
| ~ relation(C_39)
| ~ relation(B_37)
| ~ relation(A_38) ),
inference(cnfTransformation,[status(thm)],[f_76]) ).
tff(c_154,plain,
( well_founded_relation('#skF_3')
| ~ well_founded_relation('#skF_2')
| ~ function('#skF_4')
| ~ relation('#skF_4')
| ~ relation('#skF_3')
| ~ relation('#skF_2') ),
inference(resolution,[status(thm)],[c_30,c_151]) ).
tff(c_157,plain,
well_founded_relation('#skF_3'),
inference(demodulation,[status(thm),theory(equality)],[c_40,c_38,c_36,c_34,c_47,c_154]) ).
tff(c_159,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_136,c_157]) ).
tff(c_160,plain,
( ~ connected('#skF_3')
| ~ antisymmetric('#skF_3')
| ~ transitive('#skF_3') ),
inference(splitRight,[status(thm)],[c_134]) ).
tff(c_162,plain,
~ transitive('#skF_3'),
inference(splitLeft,[status(thm)],[c_160]) ).
tff(c_48,plain,
! [A_14] :
( transitive(A_14)
| ~ well_ordering(A_14)
| ~ relation(A_14) ),
inference(cnfTransformation,[status(thm)],[f_40]) ).
tff(c_51,plain,
( transitive('#skF_2')
| ~ relation('#skF_2') ),
inference(resolution,[status(thm)],[c_32,c_48]) ).
tff(c_54,plain,
transitive('#skF_2'),
inference(demodulation,[status(thm),theory(equality)],[c_40,c_51]) ).
tff(c_184,plain,
! [B_49,A_50,C_51] :
( transitive(B_49)
| ~ transitive(A_50)
| ~ relation_isomorphism(A_50,B_49,C_51)
| ~ function(C_51)
| ~ relation(C_51)
| ~ relation(B_49)
| ~ relation(A_50) ),
inference(cnfTransformation,[status(thm)],[f_76]) ).
tff(c_187,plain,
( transitive('#skF_3')
| ~ transitive('#skF_2')
| ~ function('#skF_4')
| ~ relation('#skF_4')
| ~ relation('#skF_3')
| ~ relation('#skF_2') ),
inference(resolution,[status(thm)],[c_30,c_184]) ).
tff(c_190,plain,
transitive('#skF_3'),
inference(demodulation,[status(thm),theory(equality)],[c_40,c_38,c_36,c_34,c_54,c_187]) ).
tff(c_192,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_162,c_190]) ).
tff(c_193,plain,
( ~ antisymmetric('#skF_3')
| ~ connected('#skF_3') ),
inference(splitRight,[status(thm)],[c_160]) ).
tff(c_202,plain,
~ connected('#skF_3'),
inference(splitLeft,[status(thm)],[c_193]) ).
tff(c_62,plain,
! [A_16] :
( connected(A_16)
| ~ well_ordering(A_16)
| ~ relation(A_16) ),
inference(cnfTransformation,[status(thm)],[f_40]) ).
tff(c_65,plain,
( connected('#skF_2')
| ~ relation('#skF_2') ),
inference(resolution,[status(thm)],[c_32,c_62]) ).
tff(c_68,plain,
connected('#skF_2'),
inference(demodulation,[status(thm),theory(equality)],[c_40,c_65]) ).
tff(c_224,plain,
! [B_64,A_65,C_66] :
( connected(B_64)
| ~ connected(A_65)
| ~ relation_isomorphism(A_65,B_64,C_66)
| ~ function(C_66)
| ~ relation(C_66)
| ~ relation(B_64)
| ~ relation(A_65) ),
inference(cnfTransformation,[status(thm)],[f_76]) ).
tff(c_227,plain,
( connected('#skF_3')
| ~ connected('#skF_2')
| ~ function('#skF_4')
| ~ relation('#skF_4')
| ~ relation('#skF_3')
| ~ relation('#skF_2') ),
inference(resolution,[status(thm)],[c_30,c_224]) ).
tff(c_230,plain,
connected('#skF_3'),
inference(demodulation,[status(thm),theory(equality)],[c_40,c_38,c_36,c_34,c_68,c_227]) ).
tff(c_232,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_202,c_230]) ).
tff(c_233,plain,
~ antisymmetric('#skF_3'),
inference(splitRight,[status(thm)],[c_193]) ).
tff(c_55,plain,
! [A_15] :
( antisymmetric(A_15)
| ~ well_ordering(A_15)
| ~ relation(A_15) ),
inference(cnfTransformation,[status(thm)],[f_40]) ).
tff(c_58,plain,
( antisymmetric('#skF_2')
| ~ relation('#skF_2') ),
inference(resolution,[status(thm)],[c_32,c_55]) ).
tff(c_61,plain,
antisymmetric('#skF_2'),
inference(demodulation,[status(thm),theory(equality)],[c_40,c_58]) ).
tff(c_235,plain,
! [B_67,A_68,C_69] :
( antisymmetric(B_67)
| ~ antisymmetric(A_68)
| ~ relation_isomorphism(A_68,B_67,C_69)
| ~ function(C_69)
| ~ relation(C_69)
| ~ relation(B_67)
| ~ relation(A_68) ),
inference(cnfTransformation,[status(thm)],[f_76]) ).
tff(c_238,plain,
( antisymmetric('#skF_3')
| ~ antisymmetric('#skF_2')
| ~ function('#skF_4')
| ~ relation('#skF_4')
| ~ relation('#skF_3')
| ~ relation('#skF_2') ),
inference(resolution,[status(thm)],[c_30,c_235]) ).
tff(c_241,plain,
antisymmetric('#skF_3'),
inference(demodulation,[status(thm),theory(equality)],[c_40,c_38,c_36,c_34,c_61,c_238]) ).
tff(c_243,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_233,c_241]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SEU261+1 : TPTP v9.0.0. Released v3.3.0.
% 0.03/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.34 % Computer : n016.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.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Tue Apr 8 22:33:53 EDT 2025
% 0.13/0.35 % CPUTime :
% 3.48/1.95 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.48/1.96
% 3.48/1.96 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------