%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU053+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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 115.15s 18.37s
% Output : CNFRefutation 115.15s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU053+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.07 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.43 % Computer : n018.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Sat Sep 26 08:35:21 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.44 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 115.15/18.37 % SZS status Theorem for theBenchmark.p
% 115.15/18.37 % SZS output start CNFRefutation for theBenchmark.p
% 115.15/18.37 fof(commutativity_k3_xboole_0, axiom, ! [X0] : ! [X1] : 'set$uintersection2'(X0,X1) = 'set$uintersection2'(X1,X0)).
% 115.15/18.37 fof(d7_xboole_0, axiom, ! [X0] : ! [X1] : ((disjoint(X0,X1) <=> 'set$uintersection2'(X0,X1) = 'empty$uset'))).
% 115.15/18.37 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)))))).
% 115.15/18.37 fof(fc12_relat_1, axiom, (empty('empty$uset') & (relation('empty$uset') & 'relation$uempty$uyielding'('empty$uset')))).
% 115.15/18.37 fof(fc2_subset_1, axiom, ! [X0] : ~empty(singleton(X0))).
% 115.15/18.37 fof(idempotence_k3_xboole_0, axiom, ! [X0] : ! [X1] : 'set$uintersection2'(X0,X0) = X0).
% 115.15/18.37 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)))))).
% 115.15/18.37 fof(t149_relat_1, axiom, ! [X0] : ((relation(X0) => 'relation$uimage'(X0,'empty$uset') = 'empty$uset'))).
% 115.15/18.37 fof(t17_zfmisc_1, axiom, ! [X0] : ! [X1] : ((X0 != X1 => disjoint(singleton(X0),singleton(X1))))).
% 115.15/18.37 fof(t122_funct_1, conjecture, ! [X0] : (((relation(X0) & function(X0)) => (! [X1] : ! [X2] : 'relation$uimage'(X0,'set$uintersection2'(X1,X2)) = 'set$uintersection2'('relation$uimage'(X0,X1),'relation$uimage'(X0,X2)) => 'one$uto$uone'(X0))))).
% 115.15/18.37 fof(negated_conjecture, negated_conjecture, ~! [X0] : (((relation(X0) & function(X0)) => (! [X1] : ! [X2] : 'relation$uimage'(X0,'set$uintersection2'(X1,X2)) = 'set$uintersection2'('relation$uimage'(X0,X1),'relation$uimage'(X0,X2)) => 'one$uto$uone'(X0)))), inference(negate_conjecture, [status(cth)], [t122_funct_1])).
% 115.15/18.37 cnf(c6, plain, 'set$uintersection2'(X0,X1) = 'set$uintersection2'(X1,X0), inference(clausification, [status(esa)], [commutativity_k3_xboole_0])).
% 115.15/18.37 cnf(c13, plain, ~disjoint(X0,X1) | 'set$uintersection2'(X0,X1) = 'empty$uset', inference(clausification, [status(esa)], [d7_xboole_0])).
% 115.15/18.37 cnf(c14, plain, disjoint(X0,X1) | 'set$uintersection2'(X0,X1) != 'empty$uset', inference(clausification, [status(esa)], [d7_xboole_0])).
% 115.15/18.37 cnf(c15, plain, ~function(X0) | ~relation(X0) | X1(X0), inference(clausification, [status(esa)], [d8_funct_1])).
% 115.15/18.37 cnf(c17, plain, ~X0(X1) | 'one$uto$uone'(X1) | in(sK18(X1),'relation$udom'(X1)), inference(clausification, [status(esa)], [d8_funct_1])).
% 115.15/18.37 cnf(c18, plain, ~X0(X1) | 'one$uto$uone'(X1) | apply(X1,sK18(X1)) = apply(X1,sK17(X1)), inference(clausification, [status(esa)], [d8_funct_1])).
% 115.15/18.37 cnf(c19, plain, ~X0(X1) | 'one$uto$uone'(X1) | in(sK17(X1),'relation$udom'(X1)), inference(clausification, [status(esa)], [d8_funct_1])).
% 115.15/18.37 cnf(c20, plain, ~X0(X1) | 'one$uto$uone'(X1) | sK18(X1) != sK17(X1), inference(clausification, [status(esa)], [d8_funct_1])).
% 115.15/18.37 cnf(c22, plain, empty('empty$uset'), inference(clausification, [status(esa)], [fc12_relat_1])).
% 115.15/18.37 cnf(c28, plain, ~empty(singleton(X0)), inference(clausification, [status(esa)], [fc2_subset_1])).
% 115.15/18.37 cnf(c34, plain, 'set$uintersection2'(X0,X0) = X0, inference(clausification, [status(esa)], [idempotence_k3_xboole_0])).
% 115.15/18.37 cnf(c61, plain, ~function(X0) | ~relation(X0) | singleton(apply(X0,X1)) = 'relation$uimage'(X0,singleton(X1)) | ~in(X1,'relation$udom'(X0)), inference(clausification, [status(esa)], [t117_funct_1])).
% 115.15/18.37 cnf(c62, plain, ~relation(X0) | 'relation$uimage'(X0,'empty$uset') = 'empty$uset', inference(clausification, [status(esa)], [t149_relat_1])).
% 115.15/18.37 cnf(c63, plain, X0 = X1 | disjoint(singleton(X1),singleton(X0)), inference(clausification, [status(esa)], [t17_zfmisc_1])).
% 115.15/18.37 cnf(c74, plain, function(sK74), inference(clausification, [status(esa)], [negated_conjecture])).
% 115.15/18.37 cnf(c75, plain, relation(sK74), inference(clausification, [status(esa)], [negated_conjecture])).
% 115.15/18.37 cnf(c76, plain, ~'one$uto$uone'(sK74), inference(clausification, [status(esa)], [negated_conjecture])).
% 115.15/18.37 cnf(c77, plain, 'set$uintersection2'('relation$uimage'(sK74,X0),'relation$uimage'(sK74,X1)) = 'relation$uimage'(sK74,'set$uintersection2'(X0,X1)), inference(clausification, [status(esa)], [negated_conjecture])).
% 115.15/18.37 cnf(d0, plain, ~function(sK74) | 'Ts13'(sK74), inference(resolution, [status(thm)], [c15,c75])).
% 115.15/18.37 cnf(d1, plain, 'Ts13'(sK74), inference(resolution, [status(thm)], [c74,d0])).
% 115.15/18.37 cnf(d2, plain, apply(sK74,sK18(sK74)) = apply(sK74,sK17(sK74)) | 'one$uto$uone'(sK74), inference(resolution, [status(thm)], [c18,d1])).
% 115.15/18.37 cnf(d3, plain, apply(sK74,sK18(sK74)) = apply(sK74,sK17(sK74)), inference(resolution, [status(thm)], [c76,d2])).
% 115.15/18.37 cnf(d4, plain, singleton(apply(X0,sK17(X0))) = 'relation$uimage'(X0,singleton(sK17(X0))) | ~function(X0) | ~relation(X0) | 'one$uto$uone'(X0) | ~'Ts13'(X0), inference(resolution, [status(thm)], [c61,c19])).
% 115.15/18.37 cnf(d5, plain, singleton(apply(sK74,sK17(sK74))) = 'relation$uimage'(sK74,singleton(sK17(sK74))) | ~function(sK74) | ~relation(sK74) | 'one$uto$uone'(sK74), inference(resolution, [status(thm)], [d4,d1])).
% 115.15/18.37 cnf(d6, plain, singleton(apply(sK74,sK18(sK74))) = 'relation$uimage'(sK74,singleton(sK17(sK74))) | ~function(sK74) | ~relation(sK74) | 'one$uto$uone'(sK74), inference(demodulation, [status(thm)], [d5,d3])).
% 115.15/18.37 cnf(d7, plain, singleton(apply(sK74,sK18(sK74))) = 'relation$uimage'(sK74,singleton(sK17(sK74))) | ~relation(sK74) | 'one$uto$uone'(sK74), inference(resolution, [status(thm)], [c74,d6])).
% 115.15/18.37 cnf(d8, plain, singleton(apply(sK74,sK18(sK74))) = 'relation$uimage'(sK74,singleton(sK17(sK74))) | 'one$uto$uone'(sK74), inference(resolution, [status(thm)], [c75,d7])).
% 115.15/18.37 cnf(d9, plain, singleton(apply(sK74,sK18(sK74))) = 'relation$uimage'(sK74,singleton(sK17(sK74))), inference(resolution, [status(thm)], [c76,d8])).
% 115.15/18.37 cnf(d10, plain, 'relation$uimage'(sK74,'set$uintersection2'(X0,X1)) = 'set$uintersection2'('relation$uimage'(sK74,X1),'relation$uimage'(sK74,X0)), inference(superposition, [status(thm)], [c77,c6])).
% 115.15/18.37 cnf(d11, plain, 'relation$uimage'(sK74,'set$uintersection2'(singleton(sK17(sK74)),X0)) = 'set$uintersection2'('relation$uimage'(sK74,X0),singleton(apply(sK74,sK18(sK74)))), inference(superposition, [status(thm)], [d9,d10])).
% 115.15/18.37 cnf(d12, plain, 'relation$uimage'(sK74,'set$uintersection2'(X1,X0)) != 'empty$uset' | disjoint('relation$uimage'(sK74,X0),'relation$uimage'(sK74,X1)), inference(superposition, [status(thm)], [d10,c14])).
% 115.15/18.37 cnf(d13, plain, 'relation$uimage'(sK74,'empty$uset') = 'empty$uset', inference(resolution, [status(thm)], [c62,c75])).
% 115.15/18.37 cnf(d14, plain, 'set$uintersection2'('relation$uimage'(sK74,X1),'relation$uimage'(sK74,X0)) = 'relation$uimage'(sK74,'set$uintersection2'(X0,X1)), inference(superposition, [status(thm)], [c6,c77])).
% 115.15/18.37 cnf(d15, plain, 'relation$uimage'(sK74,'set$uintersection2'(X1,X0)) = 'relation$uimage'(sK74,'set$uintersection2'(X0,X1)), inference(superposition, [status(thm)], [d14,c77])).
% 115.15/18.37 cnf(d16, plain, X0 = X1 | 'set$uintersection2'(singleton(X1),singleton(X0)) = 'empty$uset', inference(resolution, [status(thm)], [c63,c13])).
% 115.15/18.37 cnf(d17, plain, 'relation$uimage'(sK74,'empty$uset') = 'relation$uimage'(sK74,'set$uintersection2'(singleton(X1),singleton(X0))) | X1 = X0, inference(superposition, [status(thm)], [d16,d15])).
% 115.15/18.37 cnf(d18, plain, X0 = X1 | 'empty$uset' = 'relation$uimage'(sK74,'set$uintersection2'(singleton(X0),singleton(X1))), inference(demodulation, [status(thm)], [d17,d13])).
% 115.15/18.37 cnf(d19, plain, 'empty$uset' != 'empty$uset' | disjoint('relation$uimage'(sK74,singleton(X1)),'relation$uimage'(sK74,singleton(X0))) | X0 = X1, inference(superposition, [status(thm)], [d18,d12])).
% 115.15/18.37 cnf(d20, plain, 'relation$uimage'(sK74,'set$uintersection2'(X0,X1)) != 'empty$uset' | disjoint('relation$uimage'(sK74,X0),'relation$uimage'(sK74,X1)), inference(superposition, [status(thm)], [c77,c14])).
% 115.15/18.37 cnf(d21, plain, 'relation$uimage'(sK74,X0) != 'empty$uset' | disjoint('relation$uimage'(sK74,X0),'relation$uimage'(sK74,X0)), inference(superposition, [status(thm)], [c34,d20])).
% 115.15/18.37 cnf(d22, plain, 'empty$uset' != 'empty$uset' | disjoint('relation$uimage'(sK74,'empty$uset'),'relation$uimage'(sK74,'empty$uset')), inference(superposition, [status(thm)], [d13,d21])).
% 115.15/18.37 cnf(d23, plain, 'empty$uset' != 'empty$uset' | disjoint('empty$uset','relation$uimage'(sK74,'empty$uset')), inference(demodulation, [status(thm)], [d22,d13])).
% 115.15/18.37 cnf(d24, plain, 'empty$uset' != 'empty$uset' | disjoint('empty$uset','empty$uset'), inference(demodulation, [status(thm)], [d23,d13])).
% 115.15/18.37 cnf(d25, plain, disjoint('empty$uset','empty$uset'), inference(equality_resolution, [status(thm)], [d24])).
% 115.15/18.37 cnf(d26, plain, 'set$uintersection2'('empty$uset','empty$uset') = 'empty$uset', inference(resolution, [status(thm)], [d25,c13])).
% 115.15/18.37 cnf(d27, plain, 'empty$uset' = 'empty$uset', inference(demodulation, [status(thm)], [d26,c34])).
% 115.15/18.37 cnf(d28, plain, X0 = X1 | disjoint('relation$uimage'(sK74,singleton(X1)),'relation$uimage'(sK74,singleton(X0))), inference(resolution, [status(thm)], [d27,d19])).
% 115.15/18.37 cnf(d29, plain, singleton(apply(X0,sK18(X0))) = 'relation$uimage'(X0,singleton(sK18(X0))) | ~function(X0) | ~relation(X0) | 'one$uto$uone'(X0) | ~'Ts13'(X0), inference(resolution, [status(thm)], [c61,c17])).
% 115.15/18.37 cnf(d30, plain, singleton(apply(sK74,sK18(sK74))) = 'relation$uimage'(sK74,singleton(sK18(sK74))) | ~function(sK74) | ~relation(sK74) | 'one$uto$uone'(sK74), inference(resolution, [status(thm)], [d29,d1])).
% 115.15/18.37 cnf(d31, plain, singleton(apply(sK74,sK18(sK74))) = 'relation$uimage'(sK74,singleton(sK18(sK74))) | ~relation(sK74) | 'one$uto$uone'(sK74), inference(resolution, [status(thm)], [c74,d30])).
% 115.15/18.37 cnf(d32, plain, singleton(apply(sK74,sK18(sK74))) = 'relation$uimage'(sK74,singleton(sK18(sK74))) | 'one$uto$uone'(sK74), inference(resolution, [status(thm)], [c75,d31])).
% 115.15/18.37 cnf(d33, plain, singleton(apply(sK74,sK18(sK74))) = 'relation$uimage'(sK74,singleton(sK18(sK74))), inference(resolution, [status(thm)], [c76,d32])).
% 115.15/18.37 cnf(d34, plain, disjoint(singleton(apply(sK74,sK18(sK74))),'relation$uimage'(sK74,singleton(X0))) | X0 = sK18(sK74), inference(superposition, [status(thm)], [d33,d28])).
% 115.15/18.37 cnf(d35, plain, X0 = sK18(sK74) | 'set$uintersection2'(singleton(apply(sK74,sK18(sK74))),'relation$uimage'(sK74,singleton(X0))) = 'empty$uset', inference(resolution, [status(thm)], [d34,c13])).
% 115.15/18.37 cnf(d36, plain, 'empty$uset' = 'set$uintersection2'('relation$uimage'(sK74,singleton(X0)),singleton(apply(sK74,sK18(sK74)))) | X0 = sK18(sK74), inference(superposition, [status(thm)], [d35,c6])).
% 115.15/18.37 cnf(d37, plain, X0 = sK18(sK74) | 'empty$uset' = 'relation$uimage'(sK74,'set$uintersection2'(singleton(sK17(sK74)),singleton(X0))), inference(demodulation, [status(thm)], [d36,d11])).
% 115.15/18.37 cnf(d38, plain, 'empty$uset' = 'relation$uimage'(sK74,singleton(sK17(sK74))) | sK17(sK74) = sK18(sK74), inference(superposition, [status(thm)], [c34,d37])).
% 115.15/18.37 cnf(d39, plain, 'empty$uset' = singleton(apply(sK74,sK18(sK74))) | sK17(sK74) = sK18(sK74), inference(demodulation, [status(thm)], [d38,d9])).
% 115.15/18.37 cnf(d40, plain, ~empty('empty$uset') | sK17(sK74) = sK18(sK74), inference(superposition, [status(thm)], [d39,c28])).
% 115.15/18.37 cnf(d41, plain, sK17(sK74) = sK18(sK74), inference(resolution, [status(thm)], [c22,d40])).
% 115.15/18.37 cnf(d42, plain, sK18(sK74) != sK18(sK74) | 'one$uto$uone'(sK74) | ~'Ts13'(sK74), inference(superposition, [status(thm)], [d41,c20])).
% 115.15/18.37 cnf(d43, plain, sK18(sK74) != sK18(sK74) | ~'Ts13'(sK74), inference(resolution, [status(thm)], [c76,d42])).
% 115.15/18.37 cnf(d44, plain, sK18(sK74) != sK18(sK74), inference(resolution, [status(thm)], [d1,d43])).
% 115.15/18.37 cnf(d45, plain, $false, inference(equality_resolution, [status(thm)], [d44])).
% 115.15/18.37 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------