%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU055+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:40:49 AM UTC 2026
% Result : Theorem 8.87s 4.12s
% Output : CNFRefutation 8.87s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SEU055+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n017.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Sat Sep 26 08:28:18 UTC 2026
% 0.17/0.42 % CPUTime :
% 0.17/0.42 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.87/4.12 % SZS status Theorem for theBenchmark.p
% 8.87/4.12 % SZS output start CNFRefutation for theBenchmark.p
% 8.87/4.12 fof(d8_funct_1, axiom, ! [X0] : (((relation(X0) & function(X0)) => ('one$uto$uone'(X0) <=> ! [X1] : ! [X2] : (((in(X1,'relation$udom'(X0)) & (in(X2,'relation$udom'(X0)) & apply(X0,X1) = apply(X0,X2))) => X1 = X2)))))).
% 8.87/4.12 fof(fc12_relat_1, axiom, (empty('empty$uset') & (relation('empty$uset') & 'relation$uempty$uyielding'('empty$uset')))).
% 8.87/4.12 fof(fc2_subset_1, axiom, ! [X0] : ~empty(singleton(X0))).
% 8.87/4.12 fof(reflexivity_r1_tarski, axiom, ! [X0] : ! [X1] : subset(X0,X0)).
% 8.87/4.12 fof(t117_funct_1, axiom, ! [X0] : ! [X1] : (((relation(X1) & function(X1)) => (in(X0,'relation$udom'(X1)) => 'relation$uimage'(X1,singleton(X0)) = singleton(apply(X1,X0)))))).
% 8.87/4.12 fof(t20_zfmisc_1, axiom, ! [X0] : ! [X1] : (('set$udifference'(singleton(X0),singleton(X1)) = singleton(X0) <=> X0 != X1))).
% 8.87/4.12 fof(t37_xboole_1, axiom, ! [X0] : ! [X1] : (('set$udifference'(X0,X1) = 'empty$uset' <=> subset(X0,X1)))).
% 8.87/4.12 fof(t124_funct_1, conjecture, ! [X0] : (((relation(X0) & function(X0)) => (! [X1] : ! [X2] : 'relation$uimage'(X0,'set$udifference'(X1,X2)) = 'set$udifference'('relation$uimage'(X0,X1),'relation$uimage'(X0,X2)) => 'one$uto$uone'(X0))))).
% 8.87/4.12 fof(negated_conjecture, negated_conjecture, ~! [X0] : (((relation(X0) & function(X0)) => (! [X1] : ! [X2] : 'relation$uimage'(X0,'set$udifference'(X1,X2)) = 'set$udifference'('relation$uimage'(X0,X1),'relation$uimage'(X0,X2)) => 'one$uto$uone'(X0)))), inference(negate_conjecture, [status(cth)], [t124_funct_1])).
% 8.87/4.12 cnf(c13, plain, ~relation(X0) | ~function(X0) | 'one$uto$uone'(X0) | ~X1(X0), inference(clausification, [status(esa)], [d8_funct_1])).
% 8.87/4.12 cnf(c15, plain, X0(X1) | in(sK13(X1),'relation$udom'(X1)), inference(clausification, [status(esa)], [d8_funct_1])).
% 8.87/4.12 cnf(c16, plain, X0(X1) | in(sK14(X1),'relation$udom'(X1)), inference(clausification, [status(esa)], [d8_funct_1])).
% 8.87/4.12 cnf(c17, plain, X0(X1) | apply(X1,sK13(X1)) = apply(X1,sK14(X1)), inference(clausification, [status(esa)], [d8_funct_1])).
% 8.87/4.12 cnf(c18, plain, X0(X1) | sK13(X1) != sK14(X1), inference(clausification, [status(esa)], [d8_funct_1])).
% 8.87/4.12 cnf(c20, plain, empty('empty$uset'), inference(clausification, [status(esa)], [fc12_relat_1])).
% 8.87/4.12 cnf(c25, plain, ~empty(singleton(X0)), inference(clausification, [status(esa)], [fc2_subset_1])).
% 8.87/4.12 cnf(c52, plain, subset(X0,X0), inference(clausification, [status(esa)], [reflexivity_r1_tarski])).
% 8.87/4.12 cnf(c53, plain, ~relation(X0) | ~function(X0) | ~in(X1,'relation$udom'(X0)) | 'relation$uimage'(X0,singleton(X1)) = singleton(apply(X0,X1)), inference(clausification, [status(esa)], [t117_funct_1])).
% 8.87/4.12 cnf(c56, plain, 'set$udifference'(singleton(X0),singleton(X1)) = singleton(X0) | X0 = X1, inference(clausification, [status(esa)], [t20_zfmisc_1])).
% 8.87/4.12 cnf(c59, plain, 'set$udifference'(X0,X1) = 'empty$uset' | ~subset(X0,X1), inference(clausification, [status(esa)], [t37_xboole_1])).
% 8.87/4.12 cnf(c69, plain, relation(sK62), inference(clausification, [status(esa)], [negated_conjecture])).
% 8.87/4.12 cnf(c70, plain, function(sK62), inference(clausification, [status(esa)], [negated_conjecture])).
% 8.87/4.12 cnf(c71, plain, 'relation$uimage'(sK62,'set$udifference'(X0,X1)) = 'set$udifference'('relation$uimage'(sK62,X0),'relation$uimage'(sK62,X1)), inference(clausification, [status(esa)], [negated_conjecture])).
% 8.87/4.12 cnf(c72, plain, ~'one$uto$uone'(sK62), inference(clausification, [status(esa)], [negated_conjecture])).
% 8.87/4.12 cnf(d0, plain, 'relation$uimage'(X0,singleton(sK13(X0))) = singleton(apply(X0,sK13(X0))) | ~function(X0) | ~relation(X0) | 'Ts9'(X0), inference(resolution, [status(thm)], [c53,c15])).
% 8.87/4.12 cnf(d1, plain, 'relation$uimage'(sK62,singleton(sK13(sK62))) = singleton(apply(sK62,sK13(sK62))) | ~function(sK62) | 'Ts9'(sK62), inference(resolution, [status(thm)], [d0,c69])).
% 8.87/4.12 cnf(d2, plain, 'relation$uimage'(sK62,singleton(sK13(sK62))) = singleton(apply(sK62,sK13(sK62))) | 'Ts9'(sK62), inference(resolution, [status(thm)], [c70,d1])).
% 8.87/4.12 cnf(d3, plain, 'relation$uimage'(sK62,singleton(sK13(sK62))) = singleton(apply(sK62,sK13(sK62))) | ~function(sK62) | ~relation(sK62) | 'one$uto$uone'(sK62), inference(resolution, [status(thm)], [d2,c13])).
% 8.87/4.12 cnf(d4, plain, 'relation$uimage'(sK62,singleton(sK13(sK62))) = singleton(apply(sK62,sK13(sK62))) | ~function(sK62) | 'one$uto$uone'(sK62), inference(resolution, [status(thm)], [c69,d3])).
% 8.87/4.12 cnf(d5, plain, 'relation$uimage'(sK62,singleton(sK13(sK62))) = singleton(apply(sK62,sK13(sK62))) | 'one$uto$uone'(sK62), inference(resolution, [status(thm)], [c70,d4])).
% 8.87/4.12 cnf(d6, plain, 'relation$uimage'(sK62,singleton(sK13(sK62))) = singleton(apply(sK62,sK13(sK62))), inference(resolution, [status(thm)], [c72,d5])).
% 8.87/4.12 cnf(d7, plain, 'set$udifference'(X0,X0) = 'empty$uset', inference(resolution, [status(thm)], [c59,c52])).
% 8.87/4.12 cnf(d8, plain, 'relation$uimage'(sK62,'set$udifference'(X0,X0)) = 'empty$uset', inference(superposition, [status(thm)], [d7,c71])).
% 8.87/4.12 cnf(d9, plain, 'relation$uimage'(sK62,'empty$uset') = 'empty$uset', inference(demodulation, [status(thm)], [d8,d7])).
% 8.87/4.12 cnf(d10, plain, 'relation$uimage'(sK62,'set$udifference'(singleton(sK13(sK62)),X0)) = 'set$udifference'(singleton(apply(sK62,sK13(sK62))),'relation$uimage'(sK62,X0)), inference(superposition, [status(thm)], [d6,c71])).
% 8.87/4.12 cnf(d11, plain, apply(X0,sK13(X0)) = apply(X0,sK14(X0)) | ~function(X0) | ~relation(X0) | 'one$uto$uone'(X0), inference(resolution, [status(thm)], [c17,c13])).
% 8.87/4.12 cnf(d12, plain, apply(sK62,sK13(sK62)) = apply(sK62,sK14(sK62)) | ~function(sK62) | 'one$uto$uone'(sK62), inference(resolution, [status(thm)], [d11,c69])).
% 8.87/4.12 cnf(d13, plain, apply(sK62,sK13(sK62)) = apply(sK62,sK14(sK62)) | 'one$uto$uone'(sK62), inference(resolution, [status(thm)], [c70,d12])).
% 8.87/4.12 cnf(d14, plain, apply(sK62,sK13(sK62)) = apply(sK62,sK14(sK62)), inference(resolution, [status(thm)], [c72,d13])).
% 8.87/4.12 cnf(d15, plain, 'relation$uimage'(X0,singleton(sK14(X0))) = singleton(apply(X0,sK14(X0))) | ~function(X0) | ~relation(X0) | 'Ts9'(X0), inference(resolution, [status(thm)], [c53,c16])).
% 8.87/4.12 cnf(d16, plain, 'relation$uimage'(sK62,singleton(sK14(sK62))) = singleton(apply(sK62,sK14(sK62))) | ~function(sK62) | 'Ts9'(sK62), inference(resolution, [status(thm)], [d15,c69])).
% 8.87/4.12 cnf(d17, plain, 'relation$uimage'(sK62,singleton(sK14(sK62))) = singleton(apply(sK62,sK13(sK62))) | ~function(sK62) | 'Ts9'(sK62), inference(demodulation, [status(thm)], [d16,d14])).
% 8.87/4.12 cnf(d18, plain, 'relation$uimage'(sK62,singleton(sK14(sK62))) = singleton(apply(sK62,sK13(sK62))) | 'Ts9'(sK62), inference(resolution, [status(thm)], [c70,d17])).
% 8.87/4.12 cnf(d19, plain, 'relation$uimage'(sK62,singleton(sK14(sK62))) = singleton(apply(sK62,sK13(sK62))) | ~function(sK62) | ~relation(sK62) | 'one$uto$uone'(sK62), inference(resolution, [status(thm)], [d18,c13])).
% 8.87/4.12 cnf(d20, plain, 'relation$uimage'(sK62,singleton(sK14(sK62))) = singleton(apply(sK62,sK13(sK62))) | ~function(sK62) | 'one$uto$uone'(sK62), inference(resolution, [status(thm)], [c69,d19])).
% 8.87/4.12 cnf(d21, plain, 'relation$uimage'(sK62,singleton(sK14(sK62))) = singleton(apply(sK62,sK13(sK62))) | 'one$uto$uone'(sK62), inference(resolution, [status(thm)], [c70,d20])).
% 8.87/4.12 cnf(d22, plain, 'relation$uimage'(sK62,singleton(sK14(sK62))) = singleton(apply(sK62,sK13(sK62))), inference(resolution, [status(thm)], [c72,d21])).
% 8.87/4.12 cnf(d23, plain, 'relation$uimage'(sK62,'set$udifference'(singleton(sK14(sK62)),X0)) = 'set$udifference'(singleton(apply(sK62,sK13(sK62))),'relation$uimage'(sK62,X0)), inference(superposition, [status(thm)], [d22,c71])).
% 8.87/4.12 cnf(d24, plain, 'relation$uimage'(sK62,'set$udifference'(singleton(sK14(sK62)),X0)) = 'relation$uimage'(sK62,'set$udifference'(singleton(sK13(sK62)),X0)), inference(demodulation, [status(thm)], [d23,d10])).
% 8.87/4.12 cnf(d25, plain, 'relation$uimage'(sK62,'empty$uset') = 'relation$uimage'(sK62,'set$udifference'(singleton(sK13(sK62)),singleton(sK14(sK62)))), inference(superposition, [status(thm)], [d7,d24])).
% 8.87/4.12 cnf(d26, plain, 'empty$uset' = 'relation$uimage'(sK62,'set$udifference'(singleton(sK13(sK62)),singleton(sK14(sK62)))), inference(demodulation, [status(thm)], [d25,d9])).
% 8.87/4.12 cnf(d27, plain, 'empty$uset' = 'relation$uimage'(sK62,singleton(sK13(sK62))) | sK13(sK62) = sK14(sK62), inference(superposition, [status(thm)], [c56,d26])).
% 8.87/4.12 cnf(d28, plain, sK13(sK62) = sK14(sK62) | 'empty$uset' = singleton(apply(sK62,sK13(sK62))), inference(demodulation, [status(thm)], [d27,d6])).
% 8.87/4.12 cnf(d29, plain, ~empty('empty$uset') | sK13(sK62) = sK14(sK62), inference(superposition, [status(thm)], [d28,c25])).
% 8.87/4.12 cnf(d30, plain, sK13(sK62) = sK14(sK62), inference(resolution, [status(thm)], [c20,d29])).
% 8.87/4.12 cnf(d31, plain, sK13(sK62) != sK13(sK62) | 'Ts9'(sK62), inference(superposition, [status(thm)], [d30,c18])).
% 8.87/4.12 cnf(d32, plain, 'Ts9'(sK62), inference(equality_resolution, [status(thm)], [d31])).
% 8.87/4.12 cnf(d33, plain, ~function(sK62) | ~relation(sK62) | 'one$uto$uone'(sK62), inference(resolution, [status(thm)], [d32,c13])).
% 8.87/4.12 cnf(d34, plain, ~function(sK62) | 'one$uto$uone'(sK62), inference(resolution, [status(thm)], [c69,d33])).
% 8.87/4.12 cnf(d35, plain, 'one$uto$uone'(sK62), inference(resolution, [status(thm)], [c70,d34])).
% 8.87/4.12 cnf(d36, plain, $false, inference(resolution, [status(thm)], [c72,d35])).
% 8.87/4.12 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------