%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SEU265+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:26 PM UTC 2025
% Result : Theorem 127.18s 97.33s
% Output : CNFRefutation 127.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 15
% Syntax : Number of formulae : 141 ( 46 unt; 0 typ; 0 def)
% Number of atoms : 317 ( 62 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 311 ( 135 ~; 155 |; 6 &)
% ( 4 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 25 ( 25 usr; 7 con; 0-3 aty)
% Number of variables : 176 ( 173 !; 3 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ relation_of2_as_subset > relation_of2 > subset > in > element > relation > empty > relation_dom_as_subset > unordered_pair > ordered_pair > cartesian_product2 > #nlpp > singleton > relation_rng > relation_dom > powerset > empty_set > #skF_11 > #skF_4 > #skF_3 > #skF_10 > #skF_14 > #skF_9 > #skF_8 > #skF_13 > #skF_2 > #skF_7 > #skF_1 > #skF_16 > #skF_5 > #skF_15 > #skF_6 > #skF_12
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(relation,type,
relation: $i > $o ).
tff(singleton,type,
singleton: $i > $i ).
tff('#skF_11',type,
'#skF_11': $i ).
tff(unordered_pair,type,
unordered_pair: ( $i * $i ) > $i ).
tff(element,type,
element: ( $i * $i ) > $o ).
tff(ordered_pair,type,
ordered_pair: ( $i * $i ) > $i ).
tff('#skF_4',type,
'#skF_4': ( $i * $i * $i ) > $i ).
tff('#skF_3',type,
'#skF_3': ( $i * $i ) > $i ).
tff('#skF_10',type,
'#skF_10': $i ).
tff(in,type,
in: ( $i * $i ) > $o ).
tff('#skF_14',type,
'#skF_14': $i ).
tff(subset,type,
subset: ( $i * $i ) > $o ).
tff(relation_dom_as_subset,type,
relation_dom_as_subset: ( $i * $i * $i ) > $i ).
tff(empty,type,
empty: $i > $o ).
tff('#skF_9',type,
'#skF_9': $i ).
tff(empty_set,type,
empty_set: $i ).
tff(relation_dom,type,
relation_dom: $i > $i ).
tff(relation_of2,type,
relation_of2: ( $i * $i * $i ) > $o ).
tff('#skF_8',type,
'#skF_8': $i ).
tff('#skF_13',type,
'#skF_13': $i > $i ).
tff('#skF_2',type,
'#skF_2': ( $i * $i ) > $i ).
tff(powerset,type,
powerset: $i > $i ).
tff(relation_rng,type,
relation_rng: $i > $i ).
tff('#skF_7',type,
'#skF_7': ( $i * $i ) > $i ).
tff(cartesian_product2,type,
cartesian_product2: ( $i * $i ) > $i ).
tff('#skF_1',type,
'#skF_1': ( $i * $i ) > $i ).
tff('#skF_16',type,
'#skF_16': ( $i * $i ) > $i ).
tff(relation_of2_as_subset,type,
relation_of2_as_subset: ( $i * $i * $i ) > $o ).
tff('#skF_5',type,
'#skF_5': ( $i * $i ) > $i ).
tff('#skF_15',type,
'#skF_15': ( $i * $i ) > $i ).
tff('#skF_6',type,
'#skF_6': $i > $i ).
tff('#skF_12',type,
'#skF_12': $i ).
tff(f_112,negated_conjecture,
~ ! [A,B,C] :
( relation_of2_as_subset(C,B,A)
=> ( ! [D] :
~ ( in(D,B)
& ! [E] : ~ in(ordered_pair(D,E),C) )
<=> ( relation_dom_as_subset(B,A,C) = B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t22_relset_1) ).
tff(f_59,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
=> element(C,powerset(cartesian_product2(A,B))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_relset_1) ).
tff(f_35,axiom,
! [A,B,C] :
( element(C,powerset(cartesian_product2(A,B)))
=> relation(C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_relset_1) ).
tff(f_85,axiom,
! [A,B,C] :
( relation_of2_as_subset(C,A,B)
<=> relation_of2(C,A,B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
tff(f_81,axiom,
! [A,B,C] :
( relation_of2(C,A,B)
=> ( relation_dom_as_subset(A,B,C) = relation_dom(C) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k4_relset_1) ).
tff(f_55,axiom,
! [A,B,C] :
( relation_of2(C,A,B)
=> element(relation_dom_as_subset(A,B,C),powerset(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_relset_1) ).
tff(f_142,axiom,
! [A,B,C] :
~ ( in(A,B)
& element(B,powerset(C))
& empty(C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_subset) ).
tff(f_48,axiom,
! [A] :
( relation(A)
=> ! [B] :
( ( B = relation_dom(A) )
<=> ! [C] :
( in(C,B)
<=> ? [D] : in(ordered_pair(C,D),A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_relat_1) ).
tff(f_99,axiom,
! [A,B,C] :
( relation(C)
=> ( in(ordered_pair(A,B),C)
=> ( in(A,relation_dom(C))
& in(B,relation_rng(C)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t20_relat_1) ).
tff(f_135,axiom,
! [A,B,C] :
( ( in(A,B)
& element(B,powerset(C)) )
=> element(A,C) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_subset) ).
tff(f_151,axiom,
! [A,B] :
~ ( in(A,B)
& empty(B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
tff(f_118,axiom,
! [A,B] :
( element(A,B)
=> ( empty(B)
| in(A,B) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_subset) ).
tff(f_74,axiom,
? [A] : empty(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_xboole_0) ).
tff(f_146,axiom,
! [A] :
( empty(A)
=> ( A = empty_set ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_boole) ).
tff(f_65,axiom,
! [A] :
? [B] : element(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_m1_subset_1) ).
tff(c_74,plain,
relation_of2_as_subset('#skF_12','#skF_11','#skF_10'),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_927869,plain,
! [C_487920,A_487921,B_487922] :
( element(C_487920,powerset(cartesian_product2(A_487921,B_487922)))
| ~ relation_of2_as_subset(C_487920,A_487921,B_487922) ),
inference(cnfTransformation,[status(thm)],[f_59]) ).
tff(c_4,plain,
! [C_5,A_3,B_4] :
( relation(C_5)
| ~ element(C_5,powerset(cartesian_product2(A_3,B_4))) ),
inference(cnfTransformation,[status(thm)],[f_35]) ).
tff(c_927881,plain,
! [C_487923,A_487924,B_487925] :
( relation(C_487923)
| ~ relation_of2_as_subset(C_487923,A_487924,B_487925) ),
inference(resolution,[status(thm)],[c_927869,c_4]) ).
tff(c_927893,plain,
relation('#skF_12'),
inference(resolution,[status(thm)],[c_74,c_927881]) ).
tff(c_205,plain,
! [C_137,A_138,B_139] :
( relation_of2(C_137,A_138,B_139)
| ~ relation_of2_as_subset(C_137,A_138,B_139) ),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_217,plain,
relation_of2('#skF_12','#skF_11','#skF_10'),
inference(resolution,[status(thm)],[c_74,c_205]) ).
tff(c_451839,plain,
! [A_238024,B_238025,C_238026] :
( ( relation_dom_as_subset(A_238024,B_238025,C_238026) = relation_dom(C_238026) )
| ~ relation_of2(C_238026,A_238024,B_238025) ),
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_451850,plain,
relation_dom_as_subset('#skF_11','#skF_10','#skF_12') = relation_dom('#skF_12'),
inference(resolution,[status(thm)],[c_217,c_451839]) ).
tff(c_451913,plain,
! [A_238036,B_238037,C_238038] :
( element(relation_dom_as_subset(A_238036,B_238037,C_238038),powerset(A_238036))
| ~ relation_of2(C_238038,A_238036,B_238037) ),
inference(cnfTransformation,[status(thm)],[f_55]) ).
tff(c_451927,plain,
( element(relation_dom('#skF_12'),powerset('#skF_11'))
| ~ relation_of2('#skF_12','#skF_11','#skF_10') ),
inference(superposition,[status(thm),theory(equality)],[c_451850,c_451913]) ).
tff(c_451933,plain,
element(relation_dom('#skF_12'),powerset('#skF_11')),
inference(demodulation,[status(thm),theory(equality)],[c_217,c_451927]) ).
tff(c_104,plain,
! [C_101,B_100,A_99] :
( ~ empty(C_101)
| ~ element(B_100,powerset(C_101))
| ~ in(A_99,B_100) ),
inference(cnfTransformation,[status(thm)],[f_142]) ).
tff(c_451943,plain,
! [A_99] :
( ~ empty('#skF_11')
| ~ in(A_99,relation_dom('#skF_12')) ),
inference(resolution,[status(thm)],[c_451933,c_104]) ).
tff(c_451967,plain,
~ empty('#skF_11'),
inference(splitLeft,[status(thm)],[c_451943]) ).
tff(c_80,plain,
( ( relation_dom_as_subset('#skF_11','#skF_10','#skF_12') != '#skF_11' )
| in('#skF_14','#skF_11') ),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_131,plain,
relation_dom_as_subset('#skF_11','#skF_10','#skF_12') != '#skF_11',
inference(splitLeft,[status(thm)],[c_80]) ).
tff(c_451852,plain,
relation_dom('#skF_12') != '#skF_11',
inference(demodulation,[status(thm),theory(equality)],[c_451850,c_131]) ).
tff(c_451885,plain,
! [C_238030,A_238031,B_238032] :
( element(C_238030,powerset(cartesian_product2(A_238031,B_238032)))
| ~ relation_of2_as_subset(C_238030,A_238031,B_238032) ),
inference(cnfTransformation,[status(thm)],[f_59]) ).
tff(c_451900,plain,
! [C_238033,A_238034,B_238035] :
( relation(C_238033)
| ~ relation_of2_as_subset(C_238033,A_238034,B_238035) ),
inference(resolution,[status(thm)],[c_451885,c_4]) ).
tff(c_451912,plain,
relation('#skF_12'),
inference(resolution,[status(thm)],[c_74,c_451900]) ).
tff(c_453297,plain,
! [A_238163,B_238164] :
( in(ordered_pair('#skF_1'(A_238163,B_238164),'#skF_2'(A_238163,B_238164)),A_238163)
| in('#skF_3'(A_238163,B_238164),B_238164)
| ( relation_dom(A_238163) = B_238164 )
| ~ relation(A_238163) ),
inference(cnfTransformation,[status(thm)],[f_48]) ).
tff(c_72,plain,
! [A_76,C_78,B_77] :
( in(A_76,relation_dom(C_78))
| ~ in(ordered_pair(A_76,B_77),C_78)
| ~ relation(C_78) ),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_461179,plain,
! [A_238537,B_238538] :
( in('#skF_1'(A_238537,B_238538),relation_dom(A_238537))
| in('#skF_3'(A_238537,B_238538),B_238538)
| ( relation_dom(A_238537) = B_238538 )
| ~ relation(A_238537) ),
inference(resolution,[status(thm)],[c_453297,c_72]) ).
tff(c_102,plain,
! [A_96,C_98,B_97] :
( element(A_96,C_98)
| ~ element(B_97,powerset(C_98))
| ~ in(A_96,B_97) ),
inference(cnfTransformation,[status(thm)],[f_135]) ).
tff(c_451942,plain,
! [A_96] :
( element(A_96,'#skF_11')
| ~ in(A_96,relation_dom('#skF_12')) ),
inference(resolution,[status(thm)],[c_451933,c_102]) ).
tff(c_461216,plain,
! [B_238538] :
( element('#skF_1'('#skF_12',B_238538),'#skF_11')
| in('#skF_3'('#skF_12',B_238538),B_238538)
| ( relation_dom('#skF_12') = B_238538 )
| ~ relation('#skF_12') ),
inference(resolution,[status(thm)],[c_461179,c_451942]) ).
tff(c_461366,plain,
! [B_238538] :
( element('#skF_1'('#skF_12',B_238538),'#skF_11')
| in('#skF_3'('#skF_12',B_238538),B_238538)
| ( relation_dom('#skF_12') = B_238538 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_451912,c_461216]) ).
tff(c_82,plain,
! [D_85] :
( in(ordered_pair(D_85,'#skF_13'(D_85)),'#skF_12')
| ~ in(D_85,'#skF_11')
| in('#skF_14','#skF_11') ),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_230,plain,
in('#skF_14','#skF_11'),
inference(splitLeft,[status(thm)],[c_82]) ).
tff(c_108,plain,
! [B_104,A_103] :
( ~ empty(B_104)
| ~ in(A_103,B_104) ),
inference(cnfTransformation,[status(thm)],[f_151]) ).
tff(c_241,plain,
~ empty('#skF_11'),
inference(resolution,[status(thm)],[c_230,c_108]) ).
tff(c_448,plain,
! [A_171,B_172,C_173] :
( ( relation_dom_as_subset(A_171,B_172,C_173) = relation_dom(C_173) )
| ~ relation_of2(C_173,A_171,B_172) ),
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_459,plain,
relation_dom_as_subset('#skF_11','#skF_10','#skF_12') = relation_dom('#skF_12'),
inference(resolution,[status(thm)],[c_217,c_448]) ).
tff(c_461,plain,
relation_dom('#skF_12') != '#skF_11',
inference(demodulation,[status(thm),theory(equality)],[c_459,c_131]) ).
tff(c_528,plain,
! [C_178,A_179,B_180] :
( element(C_178,powerset(cartesian_product2(A_179,B_180)))
| ~ relation_of2_as_subset(C_178,A_179,B_180) ),
inference(cnfTransformation,[status(thm)],[f_59]) ).
tff(c_540,plain,
! [C_181,A_182,B_183] :
( relation(C_181)
| ~ relation_of2_as_subset(C_181,A_182,B_183) ),
inference(resolution,[status(thm)],[c_528,c_4]) ).
tff(c_552,plain,
relation('#skF_12'),
inference(resolution,[status(thm)],[c_74,c_540]) ).
tff(c_1952,plain,
! [A_326,B_327] :
( in(ordered_pair('#skF_1'(A_326,B_327),'#skF_2'(A_326,B_327)),A_326)
| in('#skF_3'(A_326,B_327),B_327)
| ( relation_dom(A_326) = B_327 )
| ~ relation(A_326) ),
inference(cnfTransformation,[status(thm)],[f_48]) ).
tff(c_9238,plain,
! [A_675,B_676] :
( in('#skF_1'(A_675,B_676),relation_dom(A_675))
| in('#skF_3'(A_675,B_676),B_676)
| ( relation_dom(A_675) = B_676 )
| ~ relation(A_675) ),
inference(resolution,[status(thm)],[c_1952,c_72]) ).
tff(c_777,plain,
! [A_227,B_228,C_229] :
( element(relation_dom_as_subset(A_227,B_228,C_229),powerset(A_227))
| ~ relation_of2(C_229,A_227,B_228) ),
inference(cnfTransformation,[status(thm)],[f_55]) ).
tff(c_791,plain,
( element(relation_dom('#skF_12'),powerset('#skF_11'))
| ~ relation_of2('#skF_12','#skF_11','#skF_10') ),
inference(superposition,[status(thm),theory(equality)],[c_459,c_777]) ).
tff(c_797,plain,
element(relation_dom('#skF_12'),powerset('#skF_11')),
inference(demodulation,[status(thm),theory(equality)],[c_217,c_791]) ).
tff(c_805,plain,
! [A_96] :
( element(A_96,'#skF_11')
| ~ in(A_96,relation_dom('#skF_12')) ),
inference(resolution,[status(thm)],[c_797,c_102]) ).
tff(c_9275,plain,
! [B_676] :
( element('#skF_1'('#skF_12',B_676),'#skF_11')
| in('#skF_3'('#skF_12',B_676),B_676)
| ( relation_dom('#skF_12') = B_676 )
| ~ relation('#skF_12') ),
inference(resolution,[status(thm)],[c_9238,c_805]) ).
tff(c_9425,plain,
! [B_676] :
( element('#skF_1'('#skF_12',B_676),'#skF_11')
| in('#skF_3'('#skF_12',B_676),B_676)
| ( relation_dom('#skF_12') = B_676 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_552,c_9275]) ).
tff(c_86,plain,
! [D_85] :
( in(ordered_pair(D_85,'#skF_13'(D_85)),'#skF_12')
| ~ in(D_85,'#skF_11')
| ( relation_dom_as_subset('#skF_11','#skF_10','#skF_12') = '#skF_11' ) ),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_268,plain,
! [D_85] :
( in(ordered_pair(D_85,'#skF_13'(D_85)),'#skF_12')
| ~ in(D_85,'#skF_11') ),
inference(negUnitSimplification,[status(thm)],[c_131,c_86]) ).
tff(c_697,plain,
! [A_218,C_219,B_220] :
( in(A_218,relation_dom(C_219))
| ~ in(ordered_pair(A_218,B_220),C_219)
| ~ relation(C_219) ),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_700,plain,
! [D_85] :
( in(D_85,relation_dom('#skF_12'))
| ~ relation('#skF_12')
| ~ in(D_85,'#skF_11') ),
inference(resolution,[status(thm)],[c_268,c_697]) ).
tff(c_707,plain,
! [D_85] :
( in(D_85,relation_dom('#skF_12'))
| ~ in(D_85,'#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_552,c_700]) ).
tff(c_8,plain,
! [C_44,A_8] :
( in(ordered_pair(C_44,'#skF_4'(A_8,relation_dom(A_8),C_44)),A_8)
| ~ in(C_44,relation_dom(A_8))
| ~ relation(A_8) ),
inference(cnfTransformation,[status(thm)],[f_48]) ).
tff(c_2112,plain,
! [A_343,B_344,D_345] :
( in(ordered_pair('#skF_1'(A_343,B_344),'#skF_2'(A_343,B_344)),A_343)
| ~ in(ordered_pair('#skF_3'(A_343,B_344),D_345),A_343)
| ( relation_dom(A_343) = B_344 )
| ~ relation(A_343) ),
inference(cnfTransformation,[status(thm)],[f_48]) ).
tff(c_11700,plain,
! [A_751,B_752] :
( in(ordered_pair('#skF_1'(A_751,B_752),'#skF_2'(A_751,B_752)),A_751)
| ( relation_dom(A_751) = B_752 )
| ~ in('#skF_3'(A_751,B_752),relation_dom(A_751))
| ~ relation(A_751) ),
inference(resolution,[status(thm)],[c_8,c_2112]) ).
tff(c_306367,plain,
! [A_178397,B_178398] :
( in('#skF_1'(A_178397,B_178398),relation_dom(A_178397))
| ( relation_dom(A_178397) = B_178398 )
| ~ in('#skF_3'(A_178397,B_178398),relation_dom(A_178397))
| ~ relation(A_178397) ),
inference(resolution,[status(thm)],[c_11700,c_72]) ).
tff(c_306757,plain,
! [B_178398] :
( in('#skF_1'('#skF_12',B_178398),relation_dom('#skF_12'))
| ( relation_dom('#skF_12') = B_178398 )
| ~ relation('#skF_12')
| ~ in('#skF_3'('#skF_12',B_178398),'#skF_11') ),
inference(resolution,[status(thm)],[c_707,c_306367]) ).
tff(c_449759,plain,
! [B_236647] :
( in('#skF_1'('#skF_12',B_236647),relation_dom('#skF_12'))
| ( relation_dom('#skF_12') = B_236647 )
| ~ in('#skF_3'('#skF_12',B_236647),'#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_552,c_306757]) ).
tff(c_450448,plain,
! [B_236904] :
( element('#skF_1'('#skF_12',B_236904),'#skF_11')
| ( relation_dom('#skF_12') = B_236904 )
| ~ in('#skF_3'('#skF_12',B_236904),'#skF_11') ),
inference(resolution,[status(thm)],[c_449759,c_805]) ).
tff(c_450452,plain,
( element('#skF_1'('#skF_12','#skF_11'),'#skF_11')
| ( relation_dom('#skF_12') = '#skF_11' ) ),
inference(resolution,[status(thm)],[c_9425,c_450448]) ).
tff(c_450806,plain,
element('#skF_1'('#skF_12','#skF_11'),'#skF_11'),
inference(negUnitSimplification,[status(thm)],[c_461,c_461,c_450452]) ).
tff(c_88,plain,
! [A_89,B_90] :
( in(A_89,B_90)
| empty(B_90)
| ~ element(A_89,B_90) ),
inference(cnfTransformation,[status(thm)],[f_118]) ).
tff(c_16,plain,
! [A_8,B_30] :
( ~ in('#skF_1'(A_8,B_30),B_30)
| in('#skF_3'(A_8,B_30),B_30)
| ( relation_dom(A_8) = B_30 )
| ~ relation(A_8) ),
inference(cnfTransformation,[status(thm)],[f_48]) ).
tff(c_1765,plain,
! [A_308,B_309,D_310] :
( ~ in('#skF_1'(A_308,B_309),B_309)
| ~ in(ordered_pair('#skF_3'(A_308,B_309),D_310),A_308)
| ( relation_dom(A_308) = B_309 )
| ~ relation(A_308) ),
inference(cnfTransformation,[status(thm)],[f_48]) ).
tff(c_10889,plain,
! [A_723,B_724,D_725] :
( ~ in(ordered_pair('#skF_3'(A_723,B_724),D_725),A_723)
| ( relation_dom(A_723) = B_724 )
| ~ relation(A_723)
| empty(B_724)
| ~ element('#skF_1'(A_723,B_724),B_724) ),
inference(resolution,[status(thm)],[c_88,c_1765]) ).
tff(c_10901,plain,
! [B_724] :
( ( relation_dom('#skF_12') = B_724 )
| ~ relation('#skF_12')
| empty(B_724)
| ~ element('#skF_1'('#skF_12',B_724),B_724)
| ~ in('#skF_3'('#skF_12',B_724),'#skF_11') ),
inference(resolution,[status(thm)],[c_268,c_10889]) ).
tff(c_10910,plain,
! [B_724] :
( ( relation_dom('#skF_12') = B_724 )
| empty(B_724)
| ~ element('#skF_1'('#skF_12',B_724),B_724)
| ~ in('#skF_3'('#skF_12',B_724),'#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_552,c_10901]) ).
tff(c_450828,plain,
( ( relation_dom('#skF_12') = '#skF_11' )
| empty('#skF_11')
| ~ in('#skF_3'('#skF_12','#skF_11'),'#skF_11') ),
inference(resolution,[status(thm)],[c_450806,c_10910]) ).
tff(c_451084,plain,
~ in('#skF_3'('#skF_12','#skF_11'),'#skF_11'),
inference(negUnitSimplification,[status(thm)],[c_241,c_461,c_450828]) ).
tff(c_451111,plain,
( ~ in('#skF_1'('#skF_12','#skF_11'),'#skF_11')
| ( relation_dom('#skF_12') = '#skF_11' )
| ~ relation('#skF_12') ),
inference(resolution,[status(thm)],[c_16,c_451084]) ).
tff(c_451128,plain,
( ~ in('#skF_1'('#skF_12','#skF_11'),'#skF_11')
| ( relation_dom('#skF_12') = '#skF_11' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_552,c_451111]) ).
tff(c_451129,plain,
~ in('#skF_1'('#skF_12','#skF_11'),'#skF_11'),
inference(negUnitSimplification,[status(thm)],[c_461,c_451128]) ).
tff(c_451143,plain,
( empty('#skF_11')
| ~ element('#skF_1'('#skF_12','#skF_11'),'#skF_11') ),
inference(resolution,[status(thm)],[c_88,c_451129]) ).
tff(c_451146,plain,
empty('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_450806,c_451143]) ).
tff(c_451148,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_241,c_451146]) ).
tff(c_451149,plain,
! [D_85] :
( in(ordered_pair(D_85,'#skF_13'(D_85)),'#skF_12')
| ~ in(D_85,'#skF_11') ),
inference(splitRight,[status(thm)],[c_82]) ).
tff(c_451974,plain,
! [A_238049,C_238050,B_238051] :
( in(A_238049,relation_dom(C_238050))
| ~ in(ordered_pair(A_238049,B_238051),C_238050)
| ~ relation(C_238050) ),
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_451977,plain,
! [D_85] :
( in(D_85,relation_dom('#skF_12'))
| ~ relation('#skF_12')
| ~ in(D_85,'#skF_11') ),
inference(resolution,[status(thm)],[c_451149,c_451974]) ).
tff(c_451984,plain,
! [D_85] :
( in(D_85,relation_dom('#skF_12'))
| ~ in(D_85,'#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_451912,c_451977]) ).
tff(c_453527,plain,
! [A_238184,B_238185,D_238186] :
( in(ordered_pair('#skF_1'(A_238184,B_238185),'#skF_2'(A_238184,B_238185)),A_238184)
| ~ in(ordered_pair('#skF_3'(A_238184,B_238185),D_238186),A_238184)
| ( relation_dom(A_238184) = B_238185 )
| ~ relation(A_238184) ),
inference(cnfTransformation,[status(thm)],[f_48]) ).
tff(c_463215,plain,
! [A_238594,B_238595] :
( in(ordered_pair('#skF_1'(A_238594,B_238595),'#skF_2'(A_238594,B_238595)),A_238594)
| ( relation_dom(A_238594) = B_238595 )
| ~ in('#skF_3'(A_238594,B_238595),relation_dom(A_238594))
| ~ relation(A_238594) ),
inference(resolution,[status(thm)],[c_8,c_453527]) ).
tff(c_738913,plain,
! [A_412027,B_412028] :
( in('#skF_1'(A_412027,B_412028),relation_dom(A_412027))
| ( relation_dom(A_412027) = B_412028 )
| ~ in('#skF_3'(A_412027,B_412028),relation_dom(A_412027))
| ~ relation(A_412027) ),
inference(resolution,[status(thm)],[c_463215,c_72]) ).
tff(c_739307,plain,
! [B_412028] :
( in('#skF_1'('#skF_12',B_412028),relation_dom('#skF_12'))
| ( relation_dom('#skF_12') = B_412028 )
| ~ relation('#skF_12')
| ~ in('#skF_3'('#skF_12',B_412028),'#skF_11') ),
inference(resolution,[status(thm)],[c_451984,c_738913]) ).
tff(c_926011,plain,
! [B_486569] :
( in('#skF_1'('#skF_12',B_486569),relation_dom('#skF_12'))
| ( relation_dom('#skF_12') = B_486569 )
| ~ in('#skF_3'('#skF_12',B_486569),'#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_451912,c_739307]) ).
tff(c_926707,plain,
! [B_486826] :
( element('#skF_1'('#skF_12',B_486826),'#skF_11')
| ( relation_dom('#skF_12') = B_486826 )
| ~ in('#skF_3'('#skF_12',B_486826),'#skF_11') ),
inference(resolution,[status(thm)],[c_926011,c_451942]) ).
tff(c_926711,plain,
( element('#skF_1'('#skF_12','#skF_11'),'#skF_11')
| ( relation_dom('#skF_12') = '#skF_11' ) ),
inference(resolution,[status(thm)],[c_461366,c_926707]) ).
tff(c_927065,plain,
element('#skF_1'('#skF_12','#skF_11'),'#skF_11'),
inference(negUnitSimplification,[status(thm)],[c_451852,c_451852,c_926711]) ).
tff(c_453250,plain,
! [A_238154,B_238155,D_238156] :
( ~ in('#skF_1'(A_238154,B_238155),B_238155)
| ~ in(ordered_pair('#skF_3'(A_238154,B_238155),D_238156),A_238154)
| ( relation_dom(A_238154) = B_238155 )
| ~ relation(A_238154) ),
inference(cnfTransformation,[status(thm)],[f_48]) ).
tff(c_462612,plain,
! [A_238575,B_238576,D_238577] :
( ~ in(ordered_pair('#skF_3'(A_238575,B_238576),D_238577),A_238575)
| ( relation_dom(A_238575) = B_238576 )
| ~ relation(A_238575)
| empty(B_238576)
| ~ element('#skF_1'(A_238575,B_238576),B_238576) ),
inference(resolution,[status(thm)],[c_88,c_453250]) ).
tff(c_462624,plain,
! [B_238576] :
( ( relation_dom('#skF_12') = B_238576 )
| ~ relation('#skF_12')
| empty(B_238576)
| ~ element('#skF_1'('#skF_12',B_238576),B_238576)
| ~ in('#skF_3'('#skF_12',B_238576),'#skF_11') ),
inference(resolution,[status(thm)],[c_451149,c_462612]) ).
tff(c_462633,plain,
! [B_238576] :
( ( relation_dom('#skF_12') = B_238576 )
| empty(B_238576)
| ~ element('#skF_1'('#skF_12',B_238576),B_238576)
| ~ in('#skF_3'('#skF_12',B_238576),'#skF_11') ),
inference(demodulation,[status(thm),theory(equality)],[c_451912,c_462624]) ).
tff(c_927086,plain,
( ( relation_dom('#skF_12') = '#skF_11' )
| empty('#skF_11')
| ~ in('#skF_3'('#skF_12','#skF_11'),'#skF_11') ),
inference(resolution,[status(thm)],[c_927065,c_462633]) ).
tff(c_927342,plain,
~ in('#skF_3'('#skF_12','#skF_11'),'#skF_11'),
inference(negUnitSimplification,[status(thm)],[c_451967,c_451852,c_927086]) ).
tff(c_927369,plain,
( ~ in('#skF_1'('#skF_12','#skF_11'),'#skF_11')
| ( relation_dom('#skF_12') = '#skF_11' )
| ~ relation('#skF_12') ),
inference(resolution,[status(thm)],[c_16,c_927342]) ).
tff(c_927386,plain,
( ~ in('#skF_1'('#skF_12','#skF_11'),'#skF_11')
| ( relation_dom('#skF_12') = '#skF_11' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_451912,c_927369]) ).
tff(c_927387,plain,
~ in('#skF_1'('#skF_12','#skF_11'),'#skF_11'),
inference(negUnitSimplification,[status(thm)],[c_451852,c_927386]) ).
tff(c_927401,plain,
( empty('#skF_11')
| ~ element('#skF_1'('#skF_12','#skF_11'),'#skF_11') ),
inference(resolution,[status(thm)],[c_88,c_927387]) ).
tff(c_927404,plain,
empty('#skF_11'),
inference(demodulation,[status(thm),theory(equality)],[c_927065,c_927401]) ).
tff(c_927406,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_451967,c_927404]) ).
tff(c_927408,plain,
empty('#skF_11'),
inference(splitRight,[status(thm)],[c_451943]) ).
tff(c_56,plain,
empty('#skF_8'),
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_112,plain,
! [A_108] :
( ( empty_set = A_108 )
| ~ empty(A_108) ),
inference(cnfTransformation,[status(thm)],[f_146]) ).
tff(c_121,plain,
empty_set = '#skF_8',
inference(resolution,[status(thm)],[c_56,c_112]) ).
tff(c_106,plain,
! [A_102] :
( ( empty_set = A_102 )
| ~ empty(A_102) ),
inference(cnfTransformation,[status(thm)],[f_146]) ).
tff(c_122,plain,
! [A_102] :
( ( A_102 = '#skF_8' )
| ~ empty(A_102) ),
inference(demodulation,[status(thm),theory(equality)],[c_121,c_106]) ).
tff(c_927415,plain,
'#skF_11' = '#skF_8',
inference(resolution,[status(thm)],[c_927408,c_122]) ).
tff(c_927422,plain,
relation_dom('#skF_12') != '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_927415,c_451852]) ).
tff(c_48,plain,
! [A_59] : element('#skF_6'(A_59),A_59),
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_927447,plain,
! [A_487854] : ~ in(A_487854,relation_dom('#skF_12')),
inference(splitRight,[status(thm)],[c_451943]) ).
tff(c_927452,plain,
! [A_89] :
( empty(relation_dom('#skF_12'))
| ~ element(A_89,relation_dom('#skF_12')) ),
inference(resolution,[status(thm)],[c_88,c_927447]) ).
tff(c_927553,plain,
! [A_487860] : ~ element(A_487860,relation_dom('#skF_12')),
inference(splitLeft,[status(thm)],[c_927452]) ).
tff(c_927558,plain,
$false,
inference(resolution,[status(thm)],[c_48,c_927553]) ).
tff(c_927559,plain,
empty(relation_dom('#skF_12')),
inference(splitRight,[status(thm)],[c_927452]) ).
tff(c_927564,plain,
relation_dom('#skF_12') = '#skF_8',
inference(resolution,[status(thm)],[c_927559,c_122]) ).
tff(c_927569,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_927422,c_927564]) ).
tff(c_927570,plain,
in('#skF_14','#skF_11'),
inference(splitRight,[status(thm)],[c_80]) ).
tff(c_927571,plain,
relation_dom_as_subset('#skF_11','#skF_10','#skF_12') = '#skF_11',
inference(splitRight,[status(thm)],[c_80]) ).
tff(c_927652,plain,
! [C_487885,A_487886,B_487887] :
( relation_of2(C_487885,A_487886,B_487887)
| ~ relation_of2_as_subset(C_487885,A_487886,B_487887) ),
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_927664,plain,
relation_of2('#skF_12','#skF_11','#skF_10'),
inference(resolution,[status(thm)],[c_74,c_927652]) ).
tff(c_927895,plain,
! [A_487928,B_487929,C_487930] :
( ( relation_dom_as_subset(A_487928,B_487929,C_487930) = relation_dom(C_487930) )
| ~ relation_of2(C_487930,A_487928,B_487929) ),
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_927901,plain,
relation_dom_as_subset('#skF_11','#skF_10','#skF_12') = relation_dom('#skF_12'),
inference(resolution,[status(thm)],[c_927664,c_927895]) ).
tff(c_927907,plain,
relation_dom('#skF_12') = '#skF_11',
inference(demodulation,[status(thm),theory(equality)],[c_927571,c_927901]) ).
tff(c_929083,plain,
! [C_488041,A_488042] :
( in(ordered_pair(C_488041,'#skF_4'(A_488042,relation_dom(A_488042),C_488041)),A_488042)
| ~ in(C_488041,relation_dom(A_488042))
| ~ relation(A_488042) ),
inference(cnfTransformation,[status(thm)],[f_48]) ).
tff(c_76,plain,
! [E_88] :
( ( relation_dom_as_subset('#skF_11','#skF_10','#skF_12') != '#skF_11' )
| ~ in(ordered_pair('#skF_14',E_88),'#skF_12') ),
inference(cnfTransformation,[status(thm)],[f_112]) ).
tff(c_927592,plain,
! [E_88] : ~ in(ordered_pair('#skF_14',E_88),'#skF_12'),
inference(demodulation,[status(thm),theory(equality)],[c_927571,c_76]) ).
tff(c_929125,plain,
( ~ in('#skF_14',relation_dom('#skF_12'))
| ~ relation('#skF_12') ),
inference(resolution,[status(thm)],[c_929083,c_927592]) ).
tff(c_929152,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_927893,c_927570,c_927907,c_929125]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SEU265+1 : TPTP v9.0.0. Released v3.3.0.
% 0.12/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.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Tue Apr 8 22:34:53 EDT 2025
% 0.19/0.35 % CPUTime :
% 127.18/97.33 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 127.18/97.35
% 127.18/97.35 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------