%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SEU216+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/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 : n010.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:14 PM UTC 2025
% Result : Theorem 19.31s 7.26s
% Output : CNFRefutation 19.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 13
% Syntax : Number of formulae : 217 ( 87 unt; 0 typ; 0 def)
% Number of atoms : 517 ( 207 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 508 ( 208 ~; 270 |; 12 &)
% ( 6 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 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 : 8 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 10 con; 0-2 aty)
% Number of variables : 123 ( 121 !; 2 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ in > element > relation_empty_yielding > relation > function > empty > unordered_pair > ordered_pair > apply > #nlpp > singleton > relation_rng > relation_dom > identity_relation > empty_set > #skF_5 > #skF_11 > #skF_7 > #skF_3 > #skF_10 > #skF_14 > #skF_6 > #skF_13 > #skF_9 > #skF_8 > #skF_2 > #skF_1 > #skF_12 > #skF_4
%Foreground sorts:
%Background operators:
%Foreground operators:
tff('#skF_5',type,
'#skF_5': $i > $i ).
tff(relation,type,
relation: $i > $o ).
tff(singleton,type,
singleton: $i > $i ).
tff('#skF_11',type,
'#skF_11': $i ).
tff(apply,type,
apply: ( $i * $i ) > $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(function,type,
function: $i > $o ).
tff('#skF_7',type,
'#skF_7': $i ).
tff(relation_empty_yielding,type,
relation_empty_yielding: $i > $o ).
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(identity_relation,type,
identity_relation: $i > $i ).
tff('#skF_6',type,
'#skF_6': $i ).
tff('#skF_13',type,
'#skF_13': $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('#skF_8',type,
'#skF_8': $i ).
tff('#skF_2',type,
'#skF_2': ( $i * $i ) > $i ).
tff(relation_rng,type,
relation_rng: $i > $i ).
tff('#skF_1',type,
'#skF_1': ( $i * $i ) > $i ).
tff('#skF_12',type,
'#skF_12': $i ).
tff('#skF_4',type,
'#skF_4': ( $i * $i ) > $i ).
tff(f_138,axiom,
? [A] : empty(A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_xboole_0) ).
tff(f_174,negated_conjecture,
~ ! [A,B] :
( ( relation(B)
& function(B) )
=> ( ( B = identity_relation(A) )
<=> ( ( relation_dom(B) = A )
& ! [C] :
( in(C,A)
=> ( apply(B,C) = C ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t34_funct_1) ).
tff(f_122,axiom,
! [A] :
( empty(A)
=> ( empty(relation_dom(A))
& relation(relation_dom(A)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc7_relat_1) ).
tff(f_160,axiom,
! [A,B] :
( element(A,B)
=> ( empty(B)
| in(A,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
tff(f_178,axiom,
! [A] :
( empty(A)
=> ( A = empty_set ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_boole) ).
tff(f_70,axiom,
! [A] :
( ( relation(A)
& function(A) )
=> ! [B,C] :
( ( in(B,relation_dom(A))
=> ( ( C = apply(A,B) )
<=> in(ordered_pair(B,C),A) ) )
& ( ~ in(B,relation_dom(A))
=> ( ( C = apply(A,B) )
<=> ( C = empty_set ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_funct_1) ).
tff(f_52,axiom,
! [A,B] :
( relation(B)
=> ( ( B = identity_relation(A) )
<=> ! [C,D] :
( in(ordered_pair(C,D),B)
<=> ( in(C,A)
& ( C = D ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d10_relat_1) ).
tff(f_205,axiom,
! [A,B,C] :
( ( relation(C)
& function(C) )
=> ( in(ordered_pair(A,B),C)
<=> ( in(A,relation_dom(C))
& ( B = apply(C,A) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_funct_1) ).
tff(f_154,axiom,
! [A,B] :
( in(A,B)
=> element(A,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
tff(f_136,axiom,
? [A] :
( empty(A)
& relation(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_relat_1) ).
tff(f_91,axiom,
! [A] :
( relation(identity_relation(A))
& function(identity_relation(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_funct_1) ).
tff(f_182,axiom,
! [A] :
( ( relation_dom(identity_relation(A)) = A )
& ( relation_rng(identity_relation(A)) = A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t71_relat_1) ).
tff(f_116,axiom,
! [A] :
( ( ~ empty(A)
& relation(A) )
=> ~ empty(relation_rng(A)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc6_relat_1) ).
tff(c_100,plain,
empty('#skF_8'),
inference(cnfTransformation,[status(thm)],[f_138]) ).
tff(c_132,plain,
( ( identity_relation('#skF_12') = '#skF_13' )
| ( relation_dom('#skF_13') = '#skF_12' ) ),
inference(cnfTransformation,[status(thm)],[f_174]) ).
tff(c_163,plain,
relation_dom('#skF_13') = '#skF_12',
inference(splitLeft,[status(thm)],[c_132]) ).
tff(c_241,plain,
! [A_66] :
( relation(relation_dom(A_66))
| ~ empty(A_66) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_247,plain,
( relation('#skF_12')
| ~ empty('#skF_13') ),
inference(superposition,[status(thm),theory(equality)],[c_163,c_241]) ).
tff(c_250,plain,
~ empty('#skF_13'),
inference(splitLeft,[status(thm)],[c_247]) ).
tff(c_114,plain,
! [A_37,B_38] :
( in(A_37,B_38)
| empty(B_38)
| ~ element(A_37,B_38) ),
inference(cnfTransformation,[status(thm)],[f_160]) ).
tff(c_118,plain,
relation('#skF_13'),
inference(cnfTransformation,[status(thm)],[f_174]) ).
tff(c_116,plain,
function('#skF_13'),
inference(cnfTransformation,[status(thm)],[f_174]) ).
tff(c_176,plain,
! [A_59] :
( ( empty_set = A_59 )
| ~ empty(A_59) ),
inference(cnfTransformation,[status(thm)],[f_178]) ).
tff(c_187,plain,
empty_set = '#skF_8',
inference(resolution,[status(thm)],[c_100,c_176]) ).
tff(c_34,plain,
! [A_15,B_18] :
( ( apply(A_15,B_18) = empty_set )
| in(B_18,relation_dom(A_15))
| ~ function(A_15)
| ~ relation(A_15) ),
inference(cnfTransformation,[status(thm)],[f_70]) ).
tff(c_1188,plain,
! [A_135,B_136] :
( ( apply(A_135,B_136) = '#skF_8' )
| in(B_136,relation_dom(A_135))
| ~ function(A_135)
| ~ relation(A_135) ),
inference(demodulation,[status(thm),theory(equality)],[c_187,c_34]) ).
tff(c_1214,plain,
! [B_136] :
( ( apply('#skF_13',B_136) = '#skF_8' )
| in(B_136,'#skF_12')
| ~ function('#skF_13')
| ~ relation('#skF_13') ),
inference(superposition,[status(thm),theory(equality)],[c_163,c_1188]) ).
tff(c_1282,plain,
! [B_142] :
( ( apply('#skF_13',B_142) = '#skF_8' )
| in(B_142,'#skF_12') ),
inference(demodulation,[status(thm),theory(equality)],[c_118,c_116,c_1214]) ).
tff(c_124,plain,
( in('#skF_14','#skF_12')
| ( relation_dom('#skF_13') != '#skF_12' )
| ( identity_relation('#skF_12') != '#skF_13' ) ),
inference(cnfTransformation,[status(thm)],[f_174]) ).
tff(c_167,plain,
identity_relation('#skF_12') != '#skF_13',
inference(splitLeft,[status(thm)],[c_124]) ).
tff(c_126,plain,
! [C_41] :
( ( identity_relation('#skF_12') = '#skF_13' )
| ( apply('#skF_13',C_41) = C_41 )
| ~ in(C_41,'#skF_12') ),
inference(cnfTransformation,[status(thm)],[f_174]) ).
tff(c_205,plain,
! [C_41] :
( ( apply('#skF_13',C_41) = C_41 )
| ~ in(C_41,'#skF_12') ),
inference(negUnitSimplification,[status(thm)],[c_167,c_126]) ).
tff(c_1301,plain,
! [B_142] :
( ( apply('#skF_13',B_142) = B_142 )
| ( apply('#skF_13',B_142) = '#skF_8' ) ),
inference(resolution,[status(thm)],[c_1282,c_205]) ).
tff(c_1382,plain,
! [B_142] :
( ( apply('#skF_13',B_142) = B_142 )
| ( B_142 != '#skF_8' ) ),
inference(factorization,[status(thm),theory(equality)],[c_1301]) ).
tff(c_1862,plain,
! [A_172,B_173] :
( in('#skF_1'(A_172,B_173),A_172)
| in(ordered_pair('#skF_3'(A_172,B_173),'#skF_4'(A_172,B_173)),B_173)
| ( identity_relation(A_172) = B_173 )
| ~ relation(B_173) ),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_152,plain,
! [A_48,C_50,B_49] :
( in(A_48,relation_dom(C_50))
| ~ in(ordered_pair(A_48,B_49),C_50)
| ~ function(C_50)
| ~ relation(C_50) ),
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_15573,plain,
! [A_389,B_390] :
( in('#skF_3'(A_389,B_390),relation_dom(B_390))
| ~ function(B_390)
| in('#skF_1'(A_389,B_390),A_389)
| ( identity_relation(A_389) = B_390 )
| ~ relation(B_390) ),
inference(resolution,[status(thm)],[c_1862,c_152]) ).
tff(c_15700,plain,
! [A_389] :
( in('#skF_3'(A_389,'#skF_13'),'#skF_12')
| ~ function('#skF_13')
| in('#skF_1'(A_389,'#skF_13'),A_389)
| ( identity_relation(A_389) = '#skF_13' )
| ~ relation('#skF_13') ),
inference(superposition,[status(thm),theory(equality)],[c_163,c_15573]) ).
tff(c_15763,plain,
! [A_395] :
( in('#skF_3'(A_395,'#skF_13'),'#skF_12')
| in('#skF_1'(A_395,'#skF_13'),A_395)
| ( identity_relation(A_395) = '#skF_13' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_118,c_116,c_15700]) ).
tff(c_14,plain,
! [A_7,B_8] :
( in('#skF_1'(A_7,B_8),A_7)
| ( '#skF_3'(A_7,B_8) != '#skF_4'(A_7,B_8) )
| ~ in('#skF_3'(A_7,B_8),A_7)
| ( identity_relation(A_7) = B_8 )
| ~ relation(B_8) ),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_15774,plain,
( ( '#skF_3'('#skF_12','#skF_13') != '#skF_4'('#skF_12','#skF_13') )
| ~ relation('#skF_13')
| in('#skF_1'('#skF_12','#skF_13'),'#skF_12')
| ( identity_relation('#skF_12') = '#skF_13' ) ),
inference(resolution,[status(thm)],[c_15763,c_14]) ).
tff(c_15827,plain,
( ( '#skF_3'('#skF_12','#skF_13') != '#skF_4'('#skF_12','#skF_13') )
| in('#skF_1'('#skF_12','#skF_13'),'#skF_12')
| ( identity_relation('#skF_12') = '#skF_13' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_118,c_15774]) ).
tff(c_15828,plain,
( ( '#skF_3'('#skF_12','#skF_13') != '#skF_4'('#skF_12','#skF_13') )
| in('#skF_1'('#skF_12','#skF_13'),'#skF_12') ),
inference(negUnitSimplification,[status(thm)],[c_167,c_15827]) ).
tff(c_16801,plain,
'#skF_3'('#skF_12','#skF_13') != '#skF_4'('#skF_12','#skF_13'),
inference(splitLeft,[status(thm)],[c_15828]) ).
tff(c_17747,plain,
! [A_431] :
( ( apply('#skF_13','#skF_3'(A_431,'#skF_13')) = '#skF_3'(A_431,'#skF_13') )
| in('#skF_1'(A_431,'#skF_13'),A_431)
| ( identity_relation(A_431) = '#skF_13' ) ),
inference(resolution,[status(thm)],[c_15763,c_205]) ).
tff(c_17781,plain,
( ( apply('#skF_13','#skF_1'('#skF_12','#skF_13')) = '#skF_1'('#skF_12','#skF_13') )
| ( apply('#skF_13','#skF_3'('#skF_12','#skF_13')) = '#skF_3'('#skF_12','#skF_13') )
| ( identity_relation('#skF_12') = '#skF_13' ) ),
inference(resolution,[status(thm)],[c_17747,c_205]) ).
tff(c_17794,plain,
( ( apply('#skF_13','#skF_1'('#skF_12','#skF_13')) = '#skF_1'('#skF_12','#skF_13') )
| ( apply('#skF_13','#skF_3'('#skF_12','#skF_13')) = '#skF_3'('#skF_12','#skF_13') ) ),
inference(negUnitSimplification,[status(thm)],[c_167,c_17781]) ).
tff(c_19120,plain,
apply('#skF_13','#skF_3'('#skF_12','#skF_13')) = '#skF_3'('#skF_12','#skF_13'),
inference(splitLeft,[status(thm)],[c_17794]) ).
tff(c_150,plain,
! [C_50,A_48,B_49] :
( ( apply(C_50,A_48) = B_49 )
| ~ in(ordered_pair(A_48,B_49),C_50)
| ~ function(C_50)
| ~ relation(C_50) ),
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_1909,plain,
! [B_173,A_172] :
( ( apply(B_173,'#skF_3'(A_172,B_173)) = '#skF_4'(A_172,B_173) )
| ~ function(B_173)
| in('#skF_1'(A_172,B_173),A_172)
| ( identity_relation(A_172) = B_173 )
| ~ relation(B_173) ),
inference(resolution,[status(thm)],[c_1862,c_150]) ).
tff(c_1708,plain,
! [A_168,C_169] :
( in(ordered_pair(A_168,apply(C_169,A_168)),C_169)
| ~ in(A_168,relation_dom(C_169))
| ~ function(C_169)
| ~ relation(C_169) ),
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_1762,plain,
! [B_142] :
( in(ordered_pair(B_142,B_142),'#skF_13')
| ~ in(B_142,relation_dom('#skF_13'))
| ~ function('#skF_13')
| ~ relation('#skF_13')
| ( B_142 != '#skF_8' ) ),
inference(superposition,[status(thm),theory(equality)],[c_1382,c_1708]) ).
tff(c_1810,plain,
! [B_142] :
( in(ordered_pair(B_142,B_142),'#skF_13')
| ~ in(B_142,'#skF_12')
| ( B_142 != '#skF_8' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_118,c_116,c_163,c_1762]) ).
tff(c_2152,plain,
! [A_179,B_180] :
( ( '#skF_2'(A_179,B_180) = '#skF_1'(A_179,B_180) )
| in(ordered_pair('#skF_3'(A_179,B_180),'#skF_4'(A_179,B_180)),B_180)
| ( identity_relation(A_179) = B_180 )
| ~ relation(B_180) ),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_21430,plain,
! [B_488,A_489] :
( ( apply(B_488,'#skF_3'(A_489,B_488)) = '#skF_4'(A_489,B_488) )
| ~ function(B_488)
| ( '#skF_2'(A_489,B_488) = '#skF_1'(A_489,B_488) )
| ( identity_relation(A_489) = B_488 )
| ~ relation(B_488) ),
inference(resolution,[status(thm)],[c_2152,c_150]) ).
tff(c_21455,plain,
( ( '#skF_3'('#skF_12','#skF_13') = '#skF_4'('#skF_12','#skF_13') )
| ~ function('#skF_13')
| ( '#skF_2'('#skF_12','#skF_13') = '#skF_1'('#skF_12','#skF_13') )
| ( identity_relation('#skF_12') = '#skF_13' )
| ~ relation('#skF_13') ),
inference(superposition,[status(thm),theory(equality)],[c_21430,c_19120]) ).
tff(c_21565,plain,
( ( '#skF_3'('#skF_12','#skF_13') = '#skF_4'('#skF_12','#skF_13') )
| ( '#skF_2'('#skF_12','#skF_13') = '#skF_1'('#skF_12','#skF_13') )
| ( identity_relation('#skF_12') = '#skF_13' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_118,c_116,c_21455]) ).
tff(c_21566,plain,
'#skF_2'('#skF_12','#skF_13') = '#skF_1'('#skF_12','#skF_13'),
inference(negUnitSimplification,[status(thm)],[c_167,c_16801,c_21565]) ).
tff(c_2523,plain,
! [A_219,B_220] :
( ~ in(ordered_pair('#skF_1'(A_219,B_220),'#skF_2'(A_219,B_220)),B_220)
| in(ordered_pair('#skF_3'(A_219,B_220),'#skF_4'(A_219,B_220)),B_220)
| ( identity_relation(A_219) = B_220 )
| ~ relation(B_220) ),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_22062,plain,
! [A_497,B_498] :
( in('#skF_3'(A_497,B_498),relation_dom(B_498))
| ~ function(B_498)
| ~ in(ordered_pair('#skF_1'(A_497,B_498),'#skF_2'(A_497,B_498)),B_498)
| ( identity_relation(A_497) = B_498 )
| ~ relation(B_498) ),
inference(resolution,[status(thm)],[c_2523,c_152]) ).
tff(c_22065,plain,
( in('#skF_3'('#skF_12','#skF_13'),relation_dom('#skF_13'))
| ~ function('#skF_13')
| ~ in(ordered_pair('#skF_1'('#skF_12','#skF_13'),'#skF_1'('#skF_12','#skF_13')),'#skF_13')
| ( identity_relation('#skF_12') = '#skF_13' )
| ~ relation('#skF_13') ),
inference(superposition,[status(thm),theory(equality)],[c_21566,c_22062]) ).
tff(c_22103,plain,
( in('#skF_3'('#skF_12','#skF_13'),'#skF_12')
| ~ in(ordered_pair('#skF_1'('#skF_12','#skF_13'),'#skF_1'('#skF_12','#skF_13')),'#skF_13')
| ( identity_relation('#skF_12') = '#skF_13' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_118,c_116,c_163,c_22065]) ).
tff(c_22104,plain,
( in('#skF_3'('#skF_12','#skF_13'),'#skF_12')
| ~ in(ordered_pair('#skF_1'('#skF_12','#skF_13'),'#skF_1'('#skF_12','#skF_13')),'#skF_13') ),
inference(negUnitSimplification,[status(thm)],[c_167,c_22103]) ).
tff(c_23834,plain,
~ in(ordered_pair('#skF_1'('#skF_12','#skF_13'),'#skF_1'('#skF_12','#skF_13')),'#skF_13'),
inference(splitLeft,[status(thm)],[c_22104]) ).
tff(c_23847,plain,
( ~ in('#skF_1'('#skF_12','#skF_13'),'#skF_12')
| ( '#skF_1'('#skF_12','#skF_13') != '#skF_8' ) ),
inference(resolution,[status(thm)],[c_1810,c_23834]) ).
tff(c_23866,plain,
'#skF_1'('#skF_12','#skF_13') != '#skF_8',
inference(splitLeft,[status(thm)],[c_23847]) ).
tff(c_19924,plain,
! [B_475,A_476] :
( ( apply(B_475,'#skF_3'(A_476,B_475)) = '#skF_4'(A_476,B_475) )
| ~ function(B_475)
| in('#skF_1'(A_476,B_475),A_476)
| ( identity_relation(A_476) = B_475 )
| ~ relation(B_475) ),
inference(resolution,[status(thm)],[c_1862,c_150]) ).
tff(c_21623,plain,
! [B_490] :
( ( apply('#skF_13','#skF_1'('#skF_12',B_490)) = '#skF_1'('#skF_12',B_490) )
| ( apply(B_490,'#skF_3'('#skF_12',B_490)) = '#skF_4'('#skF_12',B_490) )
| ~ function(B_490)
| ( identity_relation('#skF_12') = B_490 )
| ~ relation(B_490) ),
inference(resolution,[status(thm)],[c_19924,c_205]) ).
tff(c_21680,plain,
( ( '#skF_3'('#skF_12','#skF_13') = '#skF_4'('#skF_12','#skF_13') )
| ( apply('#skF_13','#skF_1'('#skF_12','#skF_13')) = '#skF_1'('#skF_12','#skF_13') )
| ~ function('#skF_13')
| ( identity_relation('#skF_12') = '#skF_13' )
| ~ relation('#skF_13') ),
inference(superposition,[status(thm),theory(equality)],[c_21623,c_19120]) ).
tff(c_21829,plain,
( ( '#skF_3'('#skF_12','#skF_13') = '#skF_4'('#skF_12','#skF_13') )
| ( apply('#skF_13','#skF_1'('#skF_12','#skF_13')) = '#skF_1'('#skF_12','#skF_13') )
| ( identity_relation('#skF_12') = '#skF_13' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_118,c_116,c_21680]) ).
tff(c_21830,plain,
apply('#skF_13','#skF_1'('#skF_12','#skF_13')) = '#skF_1'('#skF_12','#skF_13'),
inference(negUnitSimplification,[status(thm)],[c_167,c_16801,c_21829]) ).
tff(c_1765,plain,
! [B_142] :
( in(ordered_pair(B_142,B_142),'#skF_13')
| ~ in(B_142,relation_dom('#skF_13'))
| ~ function('#skF_13')
| ~ relation('#skF_13')
| ( apply('#skF_13',B_142) = '#skF_8' ) ),
inference(superposition,[status(thm),theory(equality)],[c_1301,c_1708]) ).
tff(c_1812,plain,
! [B_142] :
( in(ordered_pair(B_142,B_142),'#skF_13')
| ~ in(B_142,'#skF_12')
| ( apply('#skF_13',B_142) = '#skF_8' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_118,c_116,c_163,c_1765]) ).
tff(c_23843,plain,
( ~ in('#skF_1'('#skF_12','#skF_13'),'#skF_12')
| ( apply('#skF_13','#skF_1'('#skF_12','#skF_13')) = '#skF_8' ) ),
inference(resolution,[status(thm)],[c_1812,c_23834]) ).
tff(c_23853,plain,
( ~ in('#skF_1'('#skF_12','#skF_13'),'#skF_12')
| ( '#skF_1'('#skF_12','#skF_13') = '#skF_8' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_21830,c_23843]) ).
tff(c_23867,plain,
~ in('#skF_1'('#skF_12','#skF_13'),'#skF_12'),
inference(negUnitSimplification,[status(thm)],[c_23866,c_23853]) ).
tff(c_23873,plain,
( ( apply('#skF_13','#skF_3'('#skF_12','#skF_13')) = '#skF_4'('#skF_12','#skF_13') )
| ~ function('#skF_13')
| ( identity_relation('#skF_12') = '#skF_13' )
| ~ relation('#skF_13') ),
inference(resolution,[status(thm)],[c_1909,c_23867]) ).
tff(c_23897,plain,
( ( '#skF_3'('#skF_12','#skF_13') = '#skF_4'('#skF_12','#skF_13') )
| ( identity_relation('#skF_12') = '#skF_13' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_118,c_116,c_19120,c_23873]) ).
tff(c_23899,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_167,c_16801,c_23897]) ).
tff(c_23901,plain,
'#skF_1'('#skF_12','#skF_13') = '#skF_8',
inference(splitRight,[status(thm)],[c_23847]) ).
tff(c_24192,plain,
( ( apply('#skF_13','#skF_3'('#skF_12','#skF_13')) = '#skF_4'('#skF_12','#skF_13') )
| ~ function('#skF_13')
| in('#skF_8','#skF_12')
| ( identity_relation('#skF_12') = '#skF_13' )
| ~ relation('#skF_13') ),
inference(superposition,[status(thm),theory(equality)],[c_23901,c_1909]) ).
tff(c_24231,plain,
( ( '#skF_3'('#skF_12','#skF_13') = '#skF_4'('#skF_12','#skF_13') )
| in('#skF_8','#skF_12')
| ( identity_relation('#skF_12') = '#skF_13' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_118,c_116,c_19120,c_24192]) ).
tff(c_24232,plain,
in('#skF_8','#skF_12'),
inference(negUnitSimplification,[status(thm)],[c_167,c_16801,c_24231]) ).
tff(c_24172,plain,
~ in(ordered_pair('#skF_8','#skF_8'),'#skF_13'),
inference(demodulation,[status(thm),theory(equality)],[c_23901,c_23901,c_23834]) ).
tff(c_24321,plain,
~ in('#skF_8','#skF_12'),
inference(resolution,[status(thm)],[c_1810,c_24172]) ).
tff(c_24334,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_24232,c_24321]) ).
tff(c_24336,plain,
in(ordered_pair('#skF_1'('#skF_12','#skF_13'),'#skF_1'('#skF_12','#skF_13')),'#skF_13'),
inference(splitRight,[status(thm)],[c_22104]) ).
tff(c_24758,plain,
! [B_537,A_538] :
( ( apply(B_537,'#skF_3'(A_538,B_537)) = '#skF_4'(A_538,B_537) )
| ~ function(B_537)
| ~ in(ordered_pair('#skF_1'(A_538,B_537),'#skF_2'(A_538,B_537)),B_537)
| ( identity_relation(A_538) = B_537 )
| ~ relation(B_537) ),
inference(resolution,[status(thm)],[c_2523,c_150]) ).
tff(c_24761,plain,
( ( apply('#skF_13','#skF_3'('#skF_12','#skF_13')) = '#skF_4'('#skF_12','#skF_13') )
| ~ function('#skF_13')
| ~ in(ordered_pair('#skF_1'('#skF_12','#skF_13'),'#skF_1'('#skF_12','#skF_13')),'#skF_13')
| ( identity_relation('#skF_12') = '#skF_13' )
| ~ relation('#skF_13') ),
inference(superposition,[status(thm),theory(equality)],[c_21566,c_24758]) ).
tff(c_24799,plain,
( ( '#skF_3'('#skF_12','#skF_13') = '#skF_4'('#skF_12','#skF_13') )
| ( identity_relation('#skF_12') = '#skF_13' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_118,c_24336,c_116,c_19120,c_24761]) ).
tff(c_24801,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_167,c_16801,c_24799]) ).
tff(c_24803,plain,
apply('#skF_13','#skF_3'('#skF_12','#skF_13')) != '#skF_3'('#skF_12','#skF_13'),
inference(splitRight,[status(thm)],[c_17794]) ).
tff(c_24882,plain,
'#skF_3'('#skF_12','#skF_13') != '#skF_8',
inference(superposition,[status(thm),theory(equality)],[c_1382,c_24803]) ).
tff(c_24883,plain,
apply('#skF_13','#skF_3'('#skF_12','#skF_13')) = '#skF_8',
inference(superposition,[status(thm),theory(equality)],[c_1301,c_24803]) ).
tff(c_15833,plain,
! [A_395] :
( ( apply('#skF_13','#skF_3'(A_395,'#skF_13')) = '#skF_3'(A_395,'#skF_13') )
| in('#skF_1'(A_395,'#skF_13'),A_395)
| ( identity_relation(A_395) = '#skF_13' ) ),
inference(resolution,[status(thm)],[c_15763,c_205]) ).
tff(c_24802,plain,
apply('#skF_13','#skF_1'('#skF_12','#skF_13')) = '#skF_1'('#skF_12','#skF_13'),
inference(splitRight,[status(thm)],[c_17794]) ).
tff(c_17561,plain,
! [A_427,B_428] :
( in('#skF_3'(A_427,B_428),relation_dom(B_428))
| ~ function(B_428)
| ( '#skF_2'(A_427,B_428) = '#skF_1'(A_427,B_428) )
| ( identity_relation(A_427) = B_428 )
| ~ relation(B_428) ),
inference(resolution,[status(thm)],[c_2152,c_152]) ).
tff(c_17664,plain,
! [A_427] :
( in('#skF_3'(A_427,'#skF_13'),'#skF_12')
| ~ function('#skF_13')
| ( '#skF_2'(A_427,'#skF_13') = '#skF_1'(A_427,'#skF_13') )
| ( identity_relation(A_427) = '#skF_13' )
| ~ relation('#skF_13') ),
inference(superposition,[status(thm),theory(equality)],[c_163,c_17561]) ).
tff(c_25161,plain,
! [A_549] :
( in('#skF_3'(A_549,'#skF_13'),'#skF_12')
| ( '#skF_2'(A_549,'#skF_13') = '#skF_1'(A_549,'#skF_13') )
| ( identity_relation(A_549) = '#skF_13' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_118,c_116,c_17664]) ).
tff(c_26592,plain,
! [A_562] :
( ( apply('#skF_13','#skF_3'(A_562,'#skF_13')) = '#skF_3'(A_562,'#skF_13') )
| ( '#skF_2'(A_562,'#skF_13') = '#skF_1'(A_562,'#skF_13') )
| ( identity_relation(A_562) = '#skF_13' ) ),
inference(resolution,[status(thm)],[c_25161,c_205]) ).
tff(c_26599,plain,
( ( '#skF_3'('#skF_12','#skF_13') = '#skF_8' )
| ( '#skF_2'('#skF_12','#skF_13') = '#skF_1'('#skF_12','#skF_13') )
| ( identity_relation('#skF_12') = '#skF_13' ) ),
inference(superposition,[status(thm),theory(equality)],[c_26592,c_24883]) ).
tff(c_26652,plain,
'#skF_2'('#skF_12','#skF_13') = '#skF_1'('#skF_12','#skF_13'),
inference(negUnitSimplification,[status(thm)],[c_167,c_24882,c_26599]) ).
tff(c_27555,plain,
! [A_589,B_590] :
( in('#skF_3'(A_589,B_590),relation_dom(B_590))
| ~ function(B_590)
| ~ in(ordered_pair('#skF_1'(A_589,B_590),'#skF_2'(A_589,B_590)),B_590)
| ( identity_relation(A_589) = B_590 )
| ~ relation(B_590) ),
inference(resolution,[status(thm)],[c_2523,c_152]) ).
tff(c_27561,plain,
( in('#skF_3'('#skF_12','#skF_13'),relation_dom('#skF_13'))
| ~ function('#skF_13')
| ~ in(ordered_pair('#skF_1'('#skF_12','#skF_13'),'#skF_1'('#skF_12','#skF_13')),'#skF_13')
| ( identity_relation('#skF_12') = '#skF_13' )
| ~ relation('#skF_13') ),
inference(superposition,[status(thm),theory(equality)],[c_26652,c_27555]) ).
tff(c_27599,plain,
( in('#skF_3'('#skF_12','#skF_13'),'#skF_12')
| ~ in(ordered_pair('#skF_1'('#skF_12','#skF_13'),'#skF_1'('#skF_12','#skF_13')),'#skF_13')
| ( identity_relation('#skF_12') = '#skF_13' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_118,c_116,c_163,c_27561]) ).
tff(c_27600,plain,
( in('#skF_3'('#skF_12','#skF_13'),'#skF_12')
| ~ in(ordered_pair('#skF_1'('#skF_12','#skF_13'),'#skF_1'('#skF_12','#skF_13')),'#skF_13') ),
inference(negUnitSimplification,[status(thm)],[c_167,c_27599]) ).
tff(c_28041,plain,
~ in(ordered_pair('#skF_1'('#skF_12','#skF_13'),'#skF_1'('#skF_12','#skF_13')),'#skF_13'),
inference(splitLeft,[status(thm)],[c_27600]) ).
tff(c_28373,plain,
( ~ in('#skF_1'('#skF_12','#skF_13'),'#skF_12')
| ( apply('#skF_13','#skF_1'('#skF_12','#skF_13')) = '#skF_8' ) ),
inference(resolution,[status(thm)],[c_1812,c_28041]) ).
tff(c_28382,plain,
( ~ in('#skF_1'('#skF_12','#skF_13'),'#skF_12')
| ( '#skF_1'('#skF_12','#skF_13') = '#skF_8' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_24802,c_28373]) ).
tff(c_28391,plain,
~ in('#skF_1'('#skF_12','#skF_13'),'#skF_12'),
inference(splitLeft,[status(thm)],[c_28382]) ).
tff(c_28408,plain,
( ( apply('#skF_13','#skF_3'('#skF_12','#skF_13')) = '#skF_3'('#skF_12','#skF_13') )
| ( identity_relation('#skF_12') = '#skF_13' ) ),
inference(resolution,[status(thm)],[c_15833,c_28391]) ).
tff(c_28428,plain,
( ( '#skF_3'('#skF_12','#skF_13') = '#skF_8' )
| ( identity_relation('#skF_12') = '#skF_13' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_24883,c_28408]) ).
tff(c_28430,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_167,c_24882,c_28428]) ).
tff(c_28431,plain,
'#skF_1'('#skF_12','#skF_13') = '#skF_8',
inference(splitRight,[status(thm)],[c_28382]) ).
tff(c_28448,plain,
( ( apply('#skF_13','#skF_3'('#skF_12','#skF_13')) = '#skF_3'('#skF_12','#skF_13') )
| in('#skF_8','#skF_12')
| ( identity_relation('#skF_12') = '#skF_13' ) ),
inference(superposition,[status(thm),theory(equality)],[c_28431,c_15833]) ).
tff(c_28477,plain,
( ( '#skF_3'('#skF_12','#skF_13') = '#skF_8' )
| in('#skF_8','#skF_12')
| ( identity_relation('#skF_12') = '#skF_13' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_24883,c_28448]) ).
tff(c_28478,plain,
in('#skF_8','#skF_12'),
inference(negUnitSimplification,[status(thm)],[c_167,c_24882,c_28477]) ).
tff(c_1377,plain,
! [B_142] :
( ( apply('#skF_13',B_142) = '#skF_8' )
| ( B_142 != '#skF_8' ) ),
inference(factorization,[status(thm),theory(equality)],[c_1301]) ).
tff(c_1759,plain,
! [B_142] :
( in(ordered_pair(B_142,'#skF_8'),'#skF_13')
| ~ in(B_142,relation_dom('#skF_13'))
| ~ function('#skF_13')
| ~ relation('#skF_13')
| ( B_142 != '#skF_8' ) ),
inference(superposition,[status(thm),theory(equality)],[c_1377,c_1708]) ).
tff(c_29643,plain,
! [B_620] :
( in(ordered_pair(B_620,'#skF_8'),'#skF_13')
| ~ in(B_620,'#skF_12')
| ( B_620 != '#skF_8' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_118,c_116,c_163,c_1759]) ).
tff(c_28434,plain,
~ in(ordered_pair('#skF_8','#skF_8'),'#skF_13'),
inference(demodulation,[status(thm),theory(equality)],[c_28431,c_28431,c_28041]) ).
tff(c_29646,plain,
~ in('#skF_8','#skF_12'),
inference(resolution,[status(thm)],[c_29643,c_28434]) ).
tff(c_29670,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_28478,c_29646]) ).
tff(c_29671,plain,
in('#skF_3'('#skF_12','#skF_13'),'#skF_12'),
inference(splitRight,[status(thm)],[c_27600]) ).
tff(c_29695,plain,
apply('#skF_13','#skF_3'('#skF_12','#skF_13')) = '#skF_3'('#skF_12','#skF_13'),
inference(resolution,[status(thm)],[c_29671,c_205]) ).
tff(c_29711,plain,
'#skF_3'('#skF_12','#skF_13') = '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_24883,c_29695]) ).
tff(c_29713,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_24882,c_29711]) ).
tff(c_29714,plain,
in('#skF_1'('#skF_12','#skF_13'),'#skF_12'),
inference(splitRight,[status(thm)],[c_15828]) ).
tff(c_29739,plain,
apply('#skF_13','#skF_1'('#skF_12','#skF_13')) = '#skF_1'('#skF_12','#skF_13'),
inference(resolution,[status(thm)],[c_29714,c_205]) ).
tff(c_29715,plain,
'#skF_3'('#skF_12','#skF_13') = '#skF_4'('#skF_12','#skF_13'),
inference(splitRight,[status(thm)],[c_15828]) ).
tff(c_12,plain,
! [A_7,B_8] :
( ( '#skF_2'(A_7,B_8) = '#skF_1'(A_7,B_8) )
| ( '#skF_3'(A_7,B_8) != '#skF_4'(A_7,B_8) )
| ~ in('#skF_3'(A_7,B_8),A_7)
| ( identity_relation(A_7) = B_8 )
| ~ relation(B_8) ),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_29791,plain,
( ( '#skF_2'('#skF_12','#skF_13') = '#skF_1'('#skF_12','#skF_13') )
| ( '#skF_3'('#skF_12','#skF_13') != '#skF_4'('#skF_12','#skF_13') )
| ~ in('#skF_4'('#skF_12','#skF_13'),'#skF_12')
| ( identity_relation('#skF_12') = '#skF_13' )
| ~ relation('#skF_13') ),
inference(superposition,[status(thm),theory(equality)],[c_29715,c_12]) ).
tff(c_29824,plain,
( ( '#skF_2'('#skF_12','#skF_13') = '#skF_1'('#skF_12','#skF_13') )
| ~ in('#skF_4'('#skF_12','#skF_13'),'#skF_12')
| ( identity_relation('#skF_12') = '#skF_13' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_118,c_29715,c_29791]) ).
tff(c_29825,plain,
( ( '#skF_2'('#skF_12','#skF_13') = '#skF_1'('#skF_12','#skF_13') )
| ~ in('#skF_4'('#skF_12','#skF_13'),'#skF_12') ),
inference(negUnitSimplification,[status(thm)],[c_167,c_29824]) ).
tff(c_29893,plain,
~ in('#skF_4'('#skF_12','#skF_13'),'#skF_12'),
inference(splitLeft,[status(thm)],[c_29825]) ).
tff(c_148,plain,
! [A_48,C_50] :
( in(ordered_pair(A_48,apply(C_50,A_48)),C_50)
| ~ in(A_48,relation_dom(C_50))
| ~ function(C_50)
| ~ relation(C_50) ),
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_29848,plain,
( in(ordered_pair('#skF_1'('#skF_12','#skF_13'),'#skF_1'('#skF_12','#skF_13')),'#skF_13')
| ~ in('#skF_1'('#skF_12','#skF_13'),relation_dom('#skF_13'))
| ~ function('#skF_13')
| ~ relation('#skF_13') ),
inference(superposition,[status(thm),theory(equality)],[c_29739,c_148]) ).
tff(c_29882,plain,
in(ordered_pair('#skF_1'('#skF_12','#skF_13'),'#skF_1'('#skF_12','#skF_13')),'#skF_13'),
inference(demodulation,[status(thm),theory(equality)],[c_118,c_116,c_29714,c_163,c_29848]) ).
tff(c_29953,plain,
! [A_623,B_624] :
( in('#skF_3'(A_623,B_624),relation_dom(B_624))
| ~ function(B_624)
| ( '#skF_2'(A_623,B_624) = '#skF_1'(A_623,B_624) )
| ( identity_relation(A_623) = B_624 )
| ~ relation(B_624) ),
inference(resolution,[status(thm)],[c_2152,c_152]) ).
tff(c_29981,plain,
( in('#skF_4'('#skF_12','#skF_13'),relation_dom('#skF_13'))
| ~ function('#skF_13')
| ( '#skF_2'('#skF_12','#skF_13') = '#skF_1'('#skF_12','#skF_13') )
| ( identity_relation('#skF_12') = '#skF_13' )
| ~ relation('#skF_13') ),
inference(superposition,[status(thm),theory(equality)],[c_29715,c_29953]) ).
tff(c_30069,plain,
( in('#skF_4'('#skF_12','#skF_13'),'#skF_12')
| ( '#skF_2'('#skF_12','#skF_13') = '#skF_1'('#skF_12','#skF_13') )
| ( identity_relation('#skF_12') = '#skF_13' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_118,c_116,c_163,c_29981]) ).
tff(c_30070,plain,
'#skF_2'('#skF_12','#skF_13') = '#skF_1'('#skF_12','#skF_13'),
inference(negUnitSimplification,[status(thm)],[c_167,c_29893,c_30069]) ).
tff(c_16,plain,
! [A_7,B_8] :
( ~ in(ordered_pair('#skF_1'(A_7,B_8),'#skF_2'(A_7,B_8)),B_8)
| in(ordered_pair('#skF_3'(A_7,B_8),'#skF_4'(A_7,B_8)),B_8)
| ( identity_relation(A_7) = B_8 )
| ~ relation(B_8) ),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_29788,plain,
( ~ in(ordered_pair('#skF_1'('#skF_12','#skF_13'),'#skF_2'('#skF_12','#skF_13')),'#skF_13')
| in(ordered_pair('#skF_4'('#skF_12','#skF_13'),'#skF_4'('#skF_12','#skF_13')),'#skF_13')
| ( identity_relation('#skF_12') = '#skF_13' )
| ~ relation('#skF_13') ),
inference(superposition,[status(thm),theory(equality)],[c_29715,c_16]) ).
tff(c_29821,plain,
( ~ in(ordered_pair('#skF_1'('#skF_12','#skF_13'),'#skF_2'('#skF_12','#skF_13')),'#skF_13')
| in(ordered_pair('#skF_4'('#skF_12','#skF_13'),'#skF_4'('#skF_12','#skF_13')),'#skF_13')
| ( identity_relation('#skF_12') = '#skF_13' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_118,c_29788]) ).
tff(c_29822,plain,
( ~ in(ordered_pair('#skF_1'('#skF_12','#skF_13'),'#skF_2'('#skF_12','#skF_13')),'#skF_13')
| in(ordered_pair('#skF_4'('#skF_12','#skF_13'),'#skF_4'('#skF_12','#skF_13')),'#skF_13') ),
inference(negUnitSimplification,[status(thm)],[c_167,c_29821]) ).
tff(c_32637,plain,
in(ordered_pair('#skF_4'('#skF_12','#skF_13'),'#skF_4'('#skF_12','#skF_13')),'#skF_13'),
inference(demodulation,[status(thm),theory(equality)],[c_29882,c_30070,c_29822]) ).
tff(c_32643,plain,
( in('#skF_4'('#skF_12','#skF_13'),relation_dom('#skF_13'))
| ~ function('#skF_13')
| ~ relation('#skF_13') ),
inference(resolution,[status(thm)],[c_32637,c_152]) ).
tff(c_32662,plain,
in('#skF_4'('#skF_12','#skF_13'),'#skF_12'),
inference(demodulation,[status(thm),theory(equality)],[c_118,c_116,c_163,c_32643]) ).
tff(c_32664,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_29893,c_32662]) ).
tff(c_32666,plain,
in('#skF_4'('#skF_12','#skF_13'),'#skF_12'),
inference(splitRight,[status(thm)],[c_29825]) ).
tff(c_32665,plain,
'#skF_2'('#skF_12','#skF_13') = '#skF_1'('#skF_12','#skF_13'),
inference(splitRight,[status(thm)],[c_29825]) ).
tff(c_10,plain,
! [A_7,B_8] :
( ~ in(ordered_pair('#skF_1'(A_7,B_8),'#skF_2'(A_7,B_8)),B_8)
| ( '#skF_3'(A_7,B_8) != '#skF_4'(A_7,B_8) )
| ~ in('#skF_3'(A_7,B_8),A_7)
| ( identity_relation(A_7) = B_8 )
| ~ relation(B_8) ),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_32707,plain,
( ~ in(ordered_pair('#skF_1'('#skF_12','#skF_13'),'#skF_1'('#skF_12','#skF_13')),'#skF_13')
| ( '#skF_3'('#skF_12','#skF_13') != '#skF_4'('#skF_12','#skF_13') )
| ~ in('#skF_3'('#skF_12','#skF_13'),'#skF_12')
| ( identity_relation('#skF_12') = '#skF_13' )
| ~ relation('#skF_13') ),
inference(superposition,[status(thm),theory(equality)],[c_32665,c_10]) ).
tff(c_32711,plain,
( ~ in(ordered_pair('#skF_1'('#skF_12','#skF_13'),'#skF_1'('#skF_12','#skF_13')),'#skF_13')
| ( identity_relation('#skF_12') = '#skF_13' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_118,c_32666,c_29715,c_29715,c_32707]) ).
tff(c_32712,plain,
~ in(ordered_pair('#skF_1'('#skF_12','#skF_13'),'#skF_1'('#skF_12','#skF_13')),'#skF_13'),
inference(negUnitSimplification,[status(thm)],[c_167,c_32711]) ).
tff(c_32899,plain,
( ~ in('#skF_1'('#skF_12','#skF_13'),'#skF_12')
| ( apply('#skF_13','#skF_1'('#skF_12','#skF_13')) = '#skF_8' ) ),
inference(resolution,[status(thm)],[c_1812,c_32712]) ).
tff(c_32909,plain,
'#skF_1'('#skF_12','#skF_13') = '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_29739,c_29714,c_32899]) ).
tff(c_32913,plain,
~ in(ordered_pair('#skF_8','#skF_8'),'#skF_13'),
inference(demodulation,[status(thm),theory(equality)],[c_32909,c_32909,c_32712]) ).
tff(c_33029,plain,
( empty('#skF_13')
| ~ element(ordered_pair('#skF_8','#skF_8'),'#skF_13') ),
inference(resolution,[status(thm)],[c_114,c_32913]) ).
tff(c_33035,plain,
~ element(ordered_pair('#skF_8','#skF_8'),'#skF_13'),
inference(negUnitSimplification,[status(thm)],[c_250,c_33029]) ).
tff(c_112,plain,
! [A_35,B_36] :
( element(A_35,B_36)
| ~ in(A_35,B_36) ),
inference(cnfTransformation,[status(thm)],[f_154]) ).
tff(c_1802,plain,
! [A_168,C_169] :
( element(ordered_pair(A_168,apply(C_169,A_168)),C_169)
| ~ in(A_168,relation_dom(C_169))
| ~ function(C_169)
| ~ relation(C_169) ),
inference(resolution,[status(thm)],[c_1708,c_112]) ).
tff(c_29839,plain,
( element(ordered_pair('#skF_1'('#skF_12','#skF_13'),'#skF_1'('#skF_12','#skF_13')),'#skF_13')
| ~ in('#skF_1'('#skF_12','#skF_13'),relation_dom('#skF_13'))
| ~ function('#skF_13')
| ~ relation('#skF_13') ),
inference(superposition,[status(thm),theory(equality)],[c_29739,c_1802]) ).
tff(c_29875,plain,
element(ordered_pair('#skF_1'('#skF_12','#skF_13'),'#skF_1'('#skF_12','#skF_13')),'#skF_13'),
inference(demodulation,[status(thm),theory(equality)],[c_118,c_116,c_29714,c_163,c_29839]) ).
tff(c_33044,plain,
element(ordered_pair('#skF_8','#skF_8'),'#skF_13'),
inference(demodulation,[status(thm),theory(equality)],[c_32909,c_32909,c_29875]) ).
tff(c_33045,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_33035,c_33044]) ).
tff(c_33047,plain,
empty('#skF_13'),
inference(splitRight,[status(thm)],[c_247]) ).
tff(c_98,plain,
empty('#skF_7'),
inference(cnfTransformation,[status(thm)],[f_136]) ).
tff(c_186,plain,
empty_set = '#skF_7',
inference(resolution,[status(thm)],[c_98,c_176]) ).
tff(c_200,plain,
'#skF_7' = '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_187,c_186]) ).
tff(c_138,plain,
! [A_42] :
( ( empty_set = A_42 )
| ~ empty(A_42) ),
inference(cnfTransformation,[status(thm)],[f_178]) ).
tff(c_190,plain,
! [A_42] :
( ( A_42 = '#skF_7' )
| ~ empty(A_42) ),
inference(demodulation,[status(thm),theory(equality)],[c_186,c_138]) ).
tff(c_234,plain,
! [A_42] :
( ( A_42 = '#skF_8' )
| ~ empty(A_42) ),
inference(demodulation,[status(thm),theory(equality)],[c_200,c_190]) ).
tff(c_33051,plain,
'#skF_13' = '#skF_8',
inference(resolution,[status(thm)],[c_33047,c_234]) ).
tff(c_33055,plain,
relation_dom('#skF_8') = '#skF_12',
inference(demodulation,[status(thm),theory(equality)],[c_33051,c_163]) ).
tff(c_33118,plain,
! [A_687] :
( empty(relation_dom(A_687))
| ~ empty(A_687) ),
inference(cnfTransformation,[status(thm)],[f_122]) ).
tff(c_33124,plain,
( empty('#skF_12')
| ~ empty('#skF_8') ),
inference(superposition,[status(thm),theory(equality)],[c_33055,c_33118]) ).
tff(c_33130,plain,
empty('#skF_12'),
inference(demodulation,[status(thm),theory(equality)],[c_100,c_33124]) ).
tff(c_33134,plain,
'#skF_8' = '#skF_12',
inference(resolution,[status(thm)],[c_33130,c_234]) ).
tff(c_33054,plain,
identity_relation('#skF_12') != '#skF_8',
inference(demodulation,[status(thm),theory(equality)],[c_33051,c_167]) ).
tff(c_33138,plain,
identity_relation('#skF_12') != '#skF_12',
inference(demodulation,[status(thm),theory(equality)],[c_33134,c_33054]) ).
tff(c_68,plain,
! [A_27] : relation(identity_relation(A_27)),
inference(cnfTransformation,[status(thm)],[f_91]) ).
tff(c_142,plain,
! [A_43] : ( relation_rng(identity_relation(A_43)) = A_43 ),
inference(cnfTransformation,[status(thm)],[f_182]) ).
tff(c_33292,plain,
! [A_704] :
( ~ empty(relation_rng(A_704))
| ~ relation(A_704)
| empty(A_704) ),
inference(cnfTransformation,[status(thm)],[f_116]) ).
tff(c_33301,plain,
! [A_43] :
( ~ empty(A_43)
| ~ relation(identity_relation(A_43))
| empty(identity_relation(A_43)) ),
inference(superposition,[status(thm),theory(equality)],[c_142,c_33292]) ).
tff(c_33307,plain,
! [A_705] :
( ~ empty(A_705)
| empty(identity_relation(A_705)) ),
inference(demodulation,[status(thm),theory(equality)],[c_68,c_33301]) ).
tff(c_33142,plain,
! [A_42] :
( ( A_42 = '#skF_12' )
| ~ empty(A_42) ),
inference(demodulation,[status(thm),theory(equality)],[c_33134,c_234]) ).
tff(c_33333,plain,
! [A_706] :
( ( identity_relation(A_706) = '#skF_12' )
| ~ empty(A_706) ),
inference(resolution,[status(thm)],[c_33307,c_33142]) ).
tff(c_33339,plain,
identity_relation('#skF_12') = '#skF_12',
inference(resolution,[status(thm)],[c_33130,c_33333]) ).
tff(c_33350,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_33138,c_33339]) ).
tff(c_33352,plain,
identity_relation('#skF_12') = '#skF_13',
inference(splitRight,[status(thm)],[c_124]) ).
tff(c_122,plain,
( ( apply('#skF_13','#skF_14') != '#skF_14' )
| ( relation_dom('#skF_13') != '#skF_12' )
| ( identity_relation('#skF_12') != '#skF_13' ) ),
inference(cnfTransformation,[status(thm)],[f_174]) ).
tff(c_33358,plain,
( ( apply('#skF_13','#skF_14') != '#skF_14' )
| ( identity_relation('#skF_12') != '#skF_13' ) ),
inference(demodulation,[status(thm),theory(equality)],[c_163,c_122]) ).
tff(c_33359,plain,
identity_relation('#skF_12') != '#skF_13',
inference(splitLeft,[status(thm)],[c_33358]) ).
tff(c_33371,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_33352,c_33359]) ).
tff(c_33372,plain,
apply('#skF_13','#skF_14') != '#skF_14',
inference(splitRight,[status(thm)],[c_33358]) ).
tff(c_130,plain,
! [C_41] :
( in('#skF_14','#skF_12')
| ( relation_dom('#skF_13') != '#skF_12' )
| ( apply('#skF_13',C_41) = C_41 )
| ~ in(C_41,'#skF_12') ),
inference(cnfTransformation,[status(thm)],[f_174]) ).
tff(c_33457,plain,
! [C_41] :
( in('#skF_14','#skF_12')
| ( apply('#skF_13',C_41) = C_41 )
| ~ in(C_41,'#skF_12') ),
inference(demodulation,[status(thm),theory(equality)],[c_163,c_130]) ).
tff(c_33458,plain,
in('#skF_14','#skF_12'),
inference(splitLeft,[status(thm)],[c_33457]) ).
tff(c_22,plain,
! [D_14,A_7] :
( in(ordered_pair(D_14,D_14),identity_relation(A_7))
| ~ in(D_14,A_7)
| ~ relation(identity_relation(A_7)) ),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_34505,plain,
! [D_795,A_796] :
( in(ordered_pair(D_795,D_795),identity_relation(A_796))
| ~ in(D_795,A_796) ),
inference(demodulation,[status(thm),theory(equality)],[c_68,c_22]) ).
tff(c_34537,plain,
! [D_795] :
( in(ordered_pair(D_795,D_795),'#skF_13')
| ~ in(D_795,'#skF_12') ),
inference(superposition,[status(thm),theory(equality)],[c_33352,c_34505]) ).
tff(c_34690,plain,
! [C_808,A_809,B_810] :
( ( apply(C_808,A_809) = B_810 )
| ~ in(ordered_pair(A_809,B_810),C_808)
| ~ function(C_808)
| ~ relation(C_808) ),
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_34693,plain,
! [D_795] :
( ( apply('#skF_13',D_795) = D_795 )
| ~ function('#skF_13')
| ~ relation('#skF_13')
| ~ in(D_795,'#skF_12') ),
inference(resolution,[status(thm)],[c_34537,c_34690]) ).
tff(c_34718,plain,
! [D_811] :
( ( apply('#skF_13',D_811) = D_811 )
| ~ in(D_811,'#skF_12') ),
inference(demodulation,[status(thm),theory(equality)],[c_118,c_116,c_34693]) ).
tff(c_34728,plain,
apply('#skF_13','#skF_14') = '#skF_14',
inference(resolution,[status(thm)],[c_33458,c_34718]) ).
tff(c_34736,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_33372,c_34728]) ).
tff(c_34738,plain,
~ in('#skF_14','#skF_12'),
inference(splitRight,[status(thm)],[c_33457]) ).
tff(c_33351,plain,
( ( relation_dom('#skF_13') != '#skF_12' )
| in('#skF_14','#skF_12') ),
inference(splitRight,[status(thm)],[c_124]) ).
tff(c_34781,plain,
in('#skF_14','#skF_12'),
inference(demodulation,[status(thm),theory(equality)],[c_163,c_33351]) ).
tff(c_34782,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_34738,c_34781]) ).
tff(c_34784,plain,
relation_dom('#skF_13') != '#skF_12',
inference(splitRight,[status(thm)],[c_132]) ).
tff(c_34783,plain,
identity_relation('#skF_12') = '#skF_13',
inference(splitRight,[status(thm)],[c_132]) ).
tff(c_34801,plain,
! [A_822] : ( relation_dom(identity_relation(A_822)) = A_822 ),
inference(cnfTransformation,[status(thm)],[f_182]) ).
tff(c_34810,plain,
relation_dom('#skF_13') = '#skF_12',
inference(superposition,[status(thm),theory(equality)],[c_34783,c_34801]) ).
tff(c_34814,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_34784,c_34810]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.10 % Problem : SEU216+1 : TPTP v9.0.0. Released v3.3.0.
% 0.02/0.11 % 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.10/0.30 % Computer : n010.cluster.edu
% 0.10/0.30 % Model : x86_64 x86_64
% 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.30 % Memory : 8042.1875MB
% 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.30 % CPULimit : 300
% 0.10/0.30 % WCLimit : 300
% 0.10/0.30 % DateTime : Tue Apr 8 22:21:33 EDT 2025
% 0.10/0.31 % CPUTime :
% 19.31/7.26 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 19.47/7.28
% 19.47/7.28 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------