%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SET680+3 : TPTP v9.0.0. Released v2.2.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 : n029.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:39:04 PM UTC 2025
% Result : Theorem 11.94s 3.83s
% Output : CNFRefutation 11.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 10
% Syntax : Number of formulae : 101 ( 44 unt; 0 typ; 0 def)
% Number of atoms : 231 ( 8 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 244 ( 114 ~; 88 |; 9 &)
% ( 4 <=>; 29 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 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 : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 8 con; 0-3 aty)
% Number of variables : 122 ( 120 !; 2 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ member > ilf_type > relation_like > empty > range > domain > unordered_pair > relation_type > ordered_pair > cross_product > #nlpp > subset_type > singleton > range_of > power_set > member_type > domain_of > set_type > binary_relation_type > #skF_4 > #skF_15 > #skF_16 > #skF_14 > #skF_5 > #skF_13 > #skF_10 > #skF_8 > #skF_3 > #skF_11 > #skF_2 > #skF_7 > #skF_1 > #skF_9 > #skF_6 > #skF_12
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(relation_type,type,
relation_type: ( $i * $i ) > $i ).
tff(power_set,type,
power_set: $i > $i ).
tff('#skF_4',type,
'#skF_4': $i > $i ).
tff(singleton,type,
singleton: $i > $i ).
tff('#skF_15',type,
'#skF_15': $i ).
tff(unordered_pair,type,
unordered_pair: ( $i * $i ) > $i ).
tff(ordered_pair,type,
ordered_pair: ( $i * $i ) > $i ).
tff('#skF_16',type,
'#skF_16': $i ).
tff(cross_product,type,
cross_product: ( $i * $i ) > $i ).
tff('#skF_14',type,
'#skF_14': $i ).
tff(set_type,type,
set_type: $i ).
tff('#skF_5',type,
'#skF_5': $i ).
tff(member,type,
member: ( $i * $i ) > $o ).
tff('#skF_13',type,
'#skF_13': $i ).
tff('#skF_10',type,
'#skF_10': ( $i * $i ) > $i ).
tff('#skF_8',type,
'#skF_8': ( $i * $i ) > $i ).
tff(empty,type,
empty: $i > $o ).
tff(range,type,
range: ( $i * $i * $i ) > $i ).
tff(ilf_type,type,
ilf_type: ( $i * $i ) > $o ).
tff(member_type,type,
member_type: $i > $i ).
tff(range_of,type,
range_of: $i > $i ).
tff(domain,type,
domain: ( $i * $i * $i ) > $i ).
tff('#skF_3',type,
'#skF_3': $i > $i ).
tff('#skF_11',type,
'#skF_11': $i > $i ).
tff(domain_of,type,
domain_of: $i > $i ).
tff(subset_type,type,
subset_type: $i > $i ).
tff('#skF_2',type,
'#skF_2': ( $i * $i ) > $i ).
tff(binary_relation_type,type,
binary_relation_type: $i ).
tff(relation_like,type,
relation_like: $i > $o ).
tff('#skF_7',type,
'#skF_7': ( $i * $i ) > $i ).
tff('#skF_1',type,
'#skF_1': ( $i * $i ) > $i ).
tff('#skF_9',type,
'#skF_9': ( $i * $i ) > $i ).
tff('#skF_6',type,
'#skF_6': $i > $i ).
tff('#skF_12',type,
'#skF_12': $i ).
tff(f_374,negated_conjecture,
~ ! [B] :
( ( ~ empty(B)
& ilf_type(B,set_type) )
=> ! [C] :
( ( ~ empty(C)
& ilf_type(C,set_type) )
=> ! [D] :
( ilf_type(D,relation_type(B,C))
=> ! [E] :
( ilf_type(E,member_type(B))
=> ( member(E,domain(B,C,D))
<=> ? [F] :
( ilf_type(F,member_type(C))
& member(ordered_pair(E,F),D) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_relset_1_47) ).
tff(f_348,axiom,
! [B] : ilf_type(B,set_type),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p31) ).
tff(f_312,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,relation_type(B,C))
=> ( domain(B,C,D) = domain_of(D) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p27) ).
tff(f_118,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ( ! [D] :
( ilf_type(D,subset_type(cross_product(B,C)))
=> ilf_type(D,relation_type(B,C)) )
& ! [E] :
( ilf_type(E,relation_type(B,C))
=> ilf_type(E,subset_type(cross_product(B,C))) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p6) ).
tff(f_301,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,subset_type(cross_product(B,C)))
=> relation_like(D) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p26) ).
tff(f_208,axiom,
! [B] :
( ilf_type(B,set_type)
=> ( ilf_type(B,binary_relation_type)
<=> ( relation_like(B)
& ilf_type(B,set_type) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p17) ).
tff(f_54,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,binary_relation_type)
=> ( member(ordered_pair(B,C),D)
=> ( member(B,domain_of(D))
& member(C,range_of(D)) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p2) ).
tff(f_39,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,binary_relation_type)
=> ( member(B,domain_of(C))
<=> ? [D] :
( ilf_type(D,set_type)
& member(ordered_pair(B,D),C) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p1) ).
tff(f_75,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ilf_type(C,set_type)
=> ! [D] :
( ilf_type(D,set_type)
=> ! [E] :
( ilf_type(E,set_type)
=> ! [F] :
( ilf_type(F,relation_type(B,C))
=> ( member(ordered_pair(D,E),F)
=> ( member(D,B)
& member(E,C) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p3) ).
tff(f_140,axiom,
! [B] :
( ilf_type(B,set_type)
=> ! [C] :
( ( ~ empty(C)
& ilf_type(C,set_type) )
=> ( ilf_type(B,member_type(C))
<=> member(B,C) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p8) ).
tff(c_120,plain,
ilf_type('#skF_14',relation_type('#skF_12','#skF_13')),
inference(cnfTransformation,[status(thm)],[f_374]) ).
tff(c_116,plain,
! [B_210] : ilf_type(B_210,set_type),
inference(cnfTransformation,[status(thm)],[f_348]) ).
tff(c_108,plain,
! [B_182,C_186,D_188] :
( ( domain(B_182,C_186,D_188) = domain_of(D_188) )
| ~ ilf_type(D_188,relation_type(B_182,C_186))
| ~ ilf_type(C_186,set_type)
| ~ ilf_type(B_182,set_type) ),
inference(cnfTransformation,[status(thm)],[f_312]) ).
tff(c_7325,plain,
! [B_981,C_982,D_983] :
( ( domain(B_981,C_982,D_983) = domain_of(D_983) )
| ~ ilf_type(D_983,relation_type(B_981,C_982)) ),
inference(demodulation,[status(thm),theory(equality)],[c_116,c_116,c_108]) ).
tff(c_7333,plain,
domain('#skF_12','#skF_13','#skF_14') = domain_of('#skF_14'),
inference(resolution,[status(thm)],[c_120,c_7325]) ).
tff(c_2320,plain,
! [B_536,C_537,D_538] :
( ( domain(B_536,C_537,D_538) = domain_of(D_538) )
| ~ ilf_type(D_538,relation_type(B_536,C_537)) ),
inference(demodulation,[status(thm),theory(equality)],[c_116,c_116,c_108]) ).
tff(c_2348,plain,
domain('#skF_12','#skF_13','#skF_14') = domain_of('#skF_14'),
inference(resolution,[status(thm)],[c_120,c_2320]) ).
tff(c_140,plain,
( member('#skF_15',domain('#skF_12','#skF_13','#skF_14'))
| ilf_type('#skF_16',member_type('#skF_13')) ),
inference(cnfTransformation,[status(thm)],[f_374]) ).
tff(c_304,plain,
ilf_type('#skF_16',member_type('#skF_13')),
inference(splitLeft,[status(thm)],[c_140]) ).
tff(c_136,plain,
( member('#skF_15',domain('#skF_12','#skF_13','#skF_14'))
| member(ordered_pair('#skF_15','#skF_16'),'#skF_14') ),
inference(cnfTransformation,[status(thm)],[f_374]) ).
tff(c_370,plain,
member(ordered_pair('#skF_15','#skF_16'),'#skF_14'),
inference(splitLeft,[status(thm)],[c_136]) ).
tff(c_713,plain,
! [B_328,C_329,D_330] :
( ( domain(B_328,C_329,D_330) = domain_of(D_330) )
| ~ ilf_type(D_330,relation_type(B_328,C_329)) ),
inference(demodulation,[status(thm),theory(equality)],[c_116,c_116,c_108]) ).
tff(c_721,plain,
domain('#skF_12','#skF_13','#skF_14') = domain_of('#skF_14'),
inference(resolution,[status(thm)],[c_120,c_713]) ).
tff(c_130,plain,
! [F_252] :
( ~ member(ordered_pair('#skF_15',F_252),'#skF_14')
| ~ ilf_type(F_252,member_type('#skF_13'))
| ~ member('#skF_15',domain('#skF_12','#skF_13','#skF_14')) ),
inference(cnfTransformation,[status(thm)],[f_374]) ).
tff(c_671,plain,
~ member('#skF_15',domain('#skF_12','#skF_13','#skF_14')),
inference(splitLeft,[status(thm)],[c_130]) ).
tff(c_722,plain,
~ member('#skF_15',domain_of('#skF_14')),
inference(demodulation,[status(thm),theory(equality)],[c_721,c_671]) ).
tff(c_22,plain,
! [E_93,B_83,C_89] :
( ilf_type(E_93,subset_type(cross_product(B_83,C_89)))
| ~ ilf_type(E_93,relation_type(B_83,C_89))
| ~ ilf_type(C_89,set_type)
| ~ ilf_type(B_83,set_type) ),
inference(cnfTransformation,[status(thm)],[f_118]) ).
tff(c_922,plain,
! [E_359,B_360,C_361] :
( ilf_type(E_359,subset_type(cross_product(B_360,C_361)))
| ~ ilf_type(E_359,relation_type(B_360,C_361)) ),
inference(demodulation,[status(thm),theory(equality)],[c_116,c_116,c_22]) ).
tff(c_106,plain,
! [D_181,B_175,C_179] :
( relation_like(D_181)
| ~ ilf_type(D_181,subset_type(cross_product(B_175,C_179)))
| ~ ilf_type(C_179,set_type)
| ~ ilf_type(B_175,set_type) ),
inference(cnfTransformation,[status(thm)],[f_301]) ).
tff(c_152,plain,
! [D_181,B_175,C_179] :
( relation_like(D_181)
| ~ ilf_type(D_181,subset_type(cross_product(B_175,C_179))) ),
inference(demodulation,[status(thm),theory(equality)],[c_116,c_116,c_106]) ).
tff(c_955,plain,
! [E_362,B_363,C_364] :
( relation_like(E_362)
| ~ ilf_type(E_362,relation_type(B_363,C_364)) ),
inference(resolution,[status(thm)],[c_922,c_152]) ).
tff(c_977,plain,
relation_like('#skF_14'),
inference(resolution,[status(thm)],[c_120,c_955]) ).
tff(c_52,plain,
! [B_121] :
( ilf_type(B_121,binary_relation_type)
| ~ relation_like(B_121)
| ~ ilf_type(B_121,set_type) ),
inference(cnfTransformation,[status(thm)],[f_208]) ).
tff(c_194,plain,
! [B_121] :
( ilf_type(B_121,binary_relation_type)
| ~ relation_like(B_121) ),
inference(demodulation,[status(thm),theory(equality)],[c_116,c_52]) ).
tff(c_8,plain,
! [C_15,D_17,B_11] :
( member(C_15,range_of(D_17))
| ~ member(ordered_pair(B_11,C_15),D_17)
| ~ ilf_type(D_17,binary_relation_type)
| ~ ilf_type(C_15,set_type)
| ~ ilf_type(B_11,set_type) ),
inference(cnfTransformation,[status(thm)],[f_54]) ).
tff(c_1496,plain,
! [C_423,D_424,B_425] :
( member(C_423,range_of(D_424))
| ~ member(ordered_pair(B_425,C_423),D_424)
| ~ ilf_type(D_424,binary_relation_type) ),
inference(demodulation,[status(thm),theory(equality)],[c_116,c_116,c_8]) ).
tff(c_1519,plain,
( member('#skF_16',range_of('#skF_14'))
| ~ ilf_type('#skF_14',binary_relation_type) ),
inference(resolution,[status(thm)],[c_370,c_1496]) ).
tff(c_1520,plain,
~ ilf_type('#skF_14',binary_relation_type),
inference(splitLeft,[status(thm)],[c_1519]) ).
tff(c_1523,plain,
~ relation_like('#skF_14'),
inference(resolution,[status(thm)],[c_194,c_1520]) ).
tff(c_1527,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_977,c_1523]) ).
tff(c_1529,plain,
ilf_type('#skF_14',binary_relation_type),
inference(splitRight,[status(thm)],[c_1519]) ).
tff(c_10,plain,
! [B_11,D_17,C_15] :
( member(B_11,domain_of(D_17))
| ~ member(ordered_pair(B_11,C_15),D_17)
| ~ ilf_type(D_17,binary_relation_type)
| ~ ilf_type(C_15,set_type)
| ~ ilf_type(B_11,set_type) ),
inference(cnfTransformation,[status(thm)],[f_54]) ).
tff(c_1712,plain,
! [B_447,D_448,C_449] :
( member(B_447,domain_of(D_448))
| ~ member(ordered_pair(B_447,C_449),D_448)
| ~ ilf_type(D_448,binary_relation_type) ),
inference(demodulation,[status(thm),theory(equality)],[c_116,c_116,c_10]) ).
tff(c_1730,plain,
( member('#skF_15',domain_of('#skF_14'))
| ~ ilf_type('#skF_14',binary_relation_type) ),
inference(resolution,[status(thm)],[c_370,c_1712]) ).
tff(c_1737,plain,
member('#skF_15',domain_of('#skF_14')),
inference(demodulation,[status(thm),theory(equality)],[c_1529,c_1730]) ).
tff(c_1739,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_722,c_1737]) ).
tff(c_1749,plain,
! [F_450] :
( ~ member(ordered_pair('#skF_15',F_450),'#skF_14')
| ~ ilf_type(F_450,member_type('#skF_13')) ),
inference(splitRight,[status(thm)],[c_130]) ).
tff(c_1752,plain,
~ ilf_type('#skF_16',member_type('#skF_13')),
inference(resolution,[status(thm)],[c_370,c_1749]) ).
tff(c_1756,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_304,c_1752]) ).
tff(c_1757,plain,
member('#skF_15',domain('#skF_12','#skF_13','#skF_14')),
inference(splitRight,[status(thm)],[c_136]) ).
tff(c_2352,plain,
member('#skF_15',domain_of('#skF_14')),
inference(demodulation,[status(thm),theory(equality)],[c_2348,c_1757]) ).
tff(c_2107,plain,
! [E_503,B_504,C_505] :
( ilf_type(E_503,subset_type(cross_product(B_504,C_505)))
| ~ ilf_type(E_503,relation_type(B_504,C_505)) ),
inference(demodulation,[status(thm),theory(equality)],[c_116,c_116,c_22]) ).
tff(c_2131,plain,
! [E_506,B_507,C_508] :
( relation_like(E_506)
| ~ ilf_type(E_506,relation_type(B_507,C_508)) ),
inference(resolution,[status(thm)],[c_2107,c_152]) ).
tff(c_2153,plain,
relation_like('#skF_14'),
inference(resolution,[status(thm)],[c_120,c_2131]) ).
tff(c_4,plain,
! [B_1,C_7] :
( member(ordered_pair(B_1,'#skF_1'(B_1,C_7)),C_7)
| ~ member(B_1,domain_of(C_7))
| ~ ilf_type(C_7,binary_relation_type)
| ~ ilf_type(B_1,set_type) ),
inference(cnfTransformation,[status(thm)],[f_39]) ).
tff(c_3985,plain,
! [B_724,C_725] :
( member(ordered_pair(B_724,'#skF_1'(B_724,C_725)),C_725)
| ~ member(B_724,domain_of(C_725))
| ~ ilf_type(C_725,binary_relation_type) ),
inference(demodulation,[status(thm),theory(equality)],[c_116,c_4]) ).
tff(c_1758,plain,
~ member(ordered_pair('#skF_15','#skF_16'),'#skF_14'),
inference(splitRight,[status(thm)],[c_136]) ).
tff(c_134,plain,
! [F_252] :
( ~ member(ordered_pair('#skF_15',F_252),'#skF_14')
| ~ ilf_type(F_252,member_type('#skF_13'))
| member(ordered_pair('#skF_15','#skF_16'),'#skF_14') ),
inference(cnfTransformation,[status(thm)],[f_374]) ).
tff(c_1805,plain,
! [F_252] :
( ~ member(ordered_pair('#skF_15',F_252),'#skF_14')
| ~ ilf_type(F_252,member_type('#skF_13')) ),
inference(negUnitSimplification,[status(thm)],[c_1758,c_134]) ).
tff(c_4017,plain,
( ~ ilf_type('#skF_1'('#skF_15','#skF_14'),member_type('#skF_13'))
| ~ member('#skF_15',domain_of('#skF_14'))
| ~ ilf_type('#skF_14',binary_relation_type) ),
inference(resolution,[status(thm)],[c_3985,c_1805]) ).
tff(c_4032,plain,
( ~ ilf_type('#skF_1'('#skF_15','#skF_14'),member_type('#skF_13'))
| ~ ilf_type('#skF_14',binary_relation_type) ),
inference(demodulation,[status(thm),theory(equality)],[c_2352,c_4017]) ).
tff(c_4097,plain,
~ ilf_type('#skF_14',binary_relation_type),
inference(splitLeft,[status(thm)],[c_4032]) ).
tff(c_4100,plain,
~ relation_like('#skF_14'),
inference(resolution,[status(thm)],[c_194,c_4097]) ).
tff(c_4104,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2153,c_4100]) ).
tff(c_4106,plain,
ilf_type('#skF_14',binary_relation_type),
inference(splitRight,[status(thm)],[c_4032]) ).
tff(c_12,plain,
! [C_34,E_46,F_48,D_42,B_18] :
( member(E_46,C_34)
| ~ member(ordered_pair(D_42,E_46),F_48)
| ~ ilf_type(F_48,relation_type(B_18,C_34))
| ~ ilf_type(E_46,set_type)
| ~ ilf_type(D_42,set_type)
| ~ ilf_type(C_34,set_type)
| ~ ilf_type(B_18,set_type) ),
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_232,plain,
! [C_34,E_46,F_48,D_42,B_18] :
( member(E_46,C_34)
| ~ member(ordered_pair(D_42,E_46),F_48)
| ~ ilf_type(F_48,relation_type(B_18,C_34)) ),
inference(demodulation,[status(thm),theory(equality)],[c_116,c_116,c_116,c_116,c_12]) ).
tff(c_6805,plain,
! [B_908,C_909,C_910,B_911] :
( member('#skF_1'(B_908,C_909),C_910)
| ~ ilf_type(C_909,relation_type(B_911,C_910))
| ~ member(B_908,domain_of(C_909))
| ~ ilf_type(C_909,binary_relation_type) ),
inference(resolution,[status(thm)],[c_3985,c_232]) ).
tff(c_6837,plain,
! [B_908] :
( member('#skF_1'(B_908,'#skF_14'),'#skF_13')
| ~ member(B_908,domain_of('#skF_14'))
| ~ ilf_type('#skF_14',binary_relation_type) ),
inference(resolution,[status(thm)],[c_120,c_6805]) ).
tff(c_6856,plain,
! [B_912] :
( member('#skF_1'(B_912,'#skF_14'),'#skF_13')
| ~ member(B_912,domain_of('#skF_14')) ),
inference(demodulation,[status(thm),theory(equality)],[c_4106,c_6837]) ).
tff(c_124,plain,
~ empty('#skF_13'),
inference(cnfTransformation,[status(thm)],[f_374]) ).
tff(c_28,plain,
! [B_100,C_102] :
( ilf_type(B_100,member_type(C_102))
| ~ member(B_100,C_102)
| ~ ilf_type(C_102,set_type)
| empty(C_102)
| ~ ilf_type(B_100,set_type) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_216,plain,
! [B_100,C_102] :
( ilf_type(B_100,member_type(C_102))
| ~ member(B_100,C_102)
| empty(C_102) ),
inference(demodulation,[status(thm),theory(equality)],[c_116,c_116,c_28]) ).
tff(c_4105,plain,
~ ilf_type('#skF_1'('#skF_15','#skF_14'),member_type('#skF_13')),
inference(splitRight,[status(thm)],[c_4032]) ).
tff(c_4114,plain,
( ~ member('#skF_1'('#skF_15','#skF_14'),'#skF_13')
| empty('#skF_13') ),
inference(resolution,[status(thm)],[c_216,c_4105]) ).
tff(c_4117,plain,
~ member('#skF_1'('#skF_15','#skF_14'),'#skF_13'),
inference(negUnitSimplification,[status(thm)],[c_124,c_4114]) ).
tff(c_6859,plain,
~ member('#skF_15',domain_of('#skF_14')),
inference(resolution,[status(thm)],[c_6856,c_4117]) ).
tff(c_6868,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2352,c_6859]) ).
tff(c_6869,plain,
member('#skF_15',domain('#skF_12','#skF_13','#skF_14')),
inference(splitRight,[status(thm)],[c_140]) ).
tff(c_7337,plain,
member('#skF_15',domain_of('#skF_14')),
inference(demodulation,[status(thm),theory(equality)],[c_7333,c_6869]) ).
tff(c_7197,plain,
! [E_964,B_965,C_966] :
( ilf_type(E_964,subset_type(cross_product(B_965,C_966)))
| ~ ilf_type(E_964,relation_type(B_965,C_966)) ),
inference(demodulation,[status(thm),theory(equality)],[c_116,c_116,c_22]) ).
tff(c_7212,plain,
! [E_967,B_968,C_969] :
( relation_like(E_967)
| ~ ilf_type(E_967,relation_type(B_968,C_969)) ),
inference(resolution,[status(thm)],[c_7197,c_152]) ).
tff(c_7220,plain,
relation_like('#skF_14'),
inference(resolution,[status(thm)],[c_120,c_7212]) ).
tff(c_8795,plain,
! [B_1180,C_1181] :
( member(ordered_pair(B_1180,'#skF_1'(B_1180,C_1181)),C_1181)
| ~ member(B_1180,domain_of(C_1181))
| ~ ilf_type(C_1181,binary_relation_type) ),
inference(demodulation,[status(thm),theory(equality)],[c_116,c_4]) ).
tff(c_6870,plain,
~ ilf_type('#skF_16',member_type('#skF_13')),
inference(splitRight,[status(thm)],[c_140]) ).
tff(c_138,plain,
! [F_252] :
( ~ member(ordered_pair('#skF_15',F_252),'#skF_14')
| ~ ilf_type(F_252,member_type('#skF_13'))
| ilf_type('#skF_16',member_type('#skF_13')) ),
inference(cnfTransformation,[status(thm)],[f_374]) ).
tff(c_6915,plain,
! [F_252] :
( ~ member(ordered_pair('#skF_15',F_252),'#skF_14')
| ~ ilf_type(F_252,member_type('#skF_13')) ),
inference(negUnitSimplification,[status(thm)],[c_6870,c_138]) ).
tff(c_8827,plain,
( ~ ilf_type('#skF_1'('#skF_15','#skF_14'),member_type('#skF_13'))
| ~ member('#skF_15',domain_of('#skF_14'))
| ~ ilf_type('#skF_14',binary_relation_type) ),
inference(resolution,[status(thm)],[c_8795,c_6915]) ).
tff(c_8842,plain,
( ~ ilf_type('#skF_1'('#skF_15','#skF_14'),member_type('#skF_13'))
| ~ ilf_type('#skF_14',binary_relation_type) ),
inference(demodulation,[status(thm),theory(equality)],[c_7337,c_8827]) ).
tff(c_8916,plain,
~ ilf_type('#skF_14',binary_relation_type),
inference(splitLeft,[status(thm)],[c_8842]) ).
tff(c_8919,plain,
~ relation_like('#skF_14'),
inference(resolution,[status(thm)],[c_194,c_8916]) ).
tff(c_8923,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_7220,c_8919]) ).
tff(c_8925,plain,
ilf_type('#skF_14',binary_relation_type),
inference(splitRight,[status(thm)],[c_8842]) ).
tff(c_11793,plain,
! [B_1362,C_1363,C_1364,B_1365] :
( member('#skF_1'(B_1362,C_1363),C_1364)
| ~ ilf_type(C_1363,relation_type(B_1365,C_1364))
| ~ member(B_1362,domain_of(C_1363))
| ~ ilf_type(C_1363,binary_relation_type) ),
inference(resolution,[status(thm)],[c_8795,c_232]) ).
tff(c_11829,plain,
! [B_1362] :
( member('#skF_1'(B_1362,'#skF_14'),'#skF_13')
| ~ member(B_1362,domain_of('#skF_14'))
| ~ ilf_type('#skF_14',binary_relation_type) ),
inference(resolution,[status(thm)],[c_120,c_11793]) ).
tff(c_11850,plain,
! [B_1366] :
( member('#skF_1'(B_1366,'#skF_14'),'#skF_13')
| ~ member(B_1366,domain_of('#skF_14')) ),
inference(demodulation,[status(thm),theory(equality)],[c_8925,c_11829]) ).
tff(c_8924,plain,
~ ilf_type('#skF_1'('#skF_15','#skF_14'),member_type('#skF_13')),
inference(splitRight,[status(thm)],[c_8842]) ).
tff(c_8939,plain,
( ~ member('#skF_1'('#skF_15','#skF_14'),'#skF_13')
| empty('#skF_13') ),
inference(resolution,[status(thm)],[c_216,c_8924]) ).
tff(c_8942,plain,
~ member('#skF_1'('#skF_15','#skF_14'),'#skF_13'),
inference(negUnitSimplification,[status(thm)],[c_124,c_8939]) ).
tff(c_11853,plain,
~ member('#skF_15',domain_of('#skF_14')),
inference(resolution,[status(thm)],[c_11850,c_8942]) ).
tff(c_11862,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_7337,c_11853]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SET680+3 : TPTP v9.0.0. Released v2.2.0.
% 0.07/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.12/0.34 % Computer : n029.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 21:24:19 EDT 2025
% 0.12/0.34 % CPUTime :
% 11.94/3.83 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.94/3.85
% 11.94/3.85 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------