%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU386+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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:41:51 AM UTC 2026
% Result : Theorem 31.43s 9.48s
% Output : CNFRefutation 31.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU386+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/5.43 % Computer : n019.cluster.edu
% 0.16/5.43 % Model : x86_64 x86_64
% 0.16/5.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/5.43 % Memory : 8046.5625MB
% 0.16/5.43 % OS : Linux 6.8.0-71-generic
% 0.16/5.43 % CPULimit : 300
% 0.16/5.43 % WCLimit : 300
% 0.16/5.43 % DateTime : Sat Sep 26 09:24:11 UTC 2026
% 0.16/5.43 % CPUTime :
% 0.16/5.43 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 31.43/9.48 % SZS status Theorem for theBenchmark.p
% 31.43/9.48 % SZS output start CNFRefutation for theBenchmark.p
% 31.43/9.48 fof(d18_yellow_6, axiom, ! [X0] : (((~'empty$ucarrier'(X0) & ('topological$uspace'(X0) & 'top$ustr'(X0))) => ! [X1] : (((~'empty$ucarrier'(X1) & ('transitive$urelstr'(X1) & ('directed$urelstr'(X1) & 'net$ustr'(X1,X0)))) => ! [X2] : ((element(X2,powerset('the$ucarrier'(X0))) => (X2 = 'lim$upoints$uof$unet'(X0,X1) <=> ! [X3] : ((element(X3,'the$ucarrier'(X0)) => (in(X3,X2) <=> ! [X4] : (('point$uneighbourhood'(X4,X0,X3) => 'is$ueventually$uin'(X0,X1,X4)))))))))))))).
% 31.43/9.48 fof(d9_waybel_9, axiom, ! [X0] : (((~'empty$ucarrier'(X0) & ('topological$uspace'(X0) & 'top$ustr'(X0))) => ! [X1] : (((~'empty$ucarrier'(X1) & 'net$ustr'(X1,X0)) => ! [X2] : ((element(X2,'the$ucarrier'(X0)) => ('is$ua$ucluster$upoint$uof$unetstr'(X0,X1,X2) <=> ! [X3] : (('point$uneighbourhood'(X3,X0,X2) => 'is$uoften$uin'(X0,X1,X3))))))))))).
% 31.43/9.48 fof(dt_k11_yellow_6, axiom, ! [X0] : ! [X1] : (((~'empty$ucarrier'(X0) & ('topological$uspace'(X0) & ('top$ustr'(X0) & (~'empty$ucarrier'(X1) & ('transitive$urelstr'(X1) & ('directed$urelstr'(X1) & 'net$ustr'(X1,X0))))))) => element('lim$upoints$uof$unet'(X0,X1),powerset('the$ucarrier'(X0)))))).
% 31.43/9.48 fof(dt_l1_pre_topc, axiom, ! [X0] : (('top$ustr'(X0) => 'one$usorted$ustr'(X0)))).
% 31.43/9.48 fof(t28_yellow_6, axiom, ! [X0] : (((~'empty$ucarrier'(X0) & 'one$usorted$ustr'(X0)) => ! [X1] : (((~'empty$ucarrier'(X1) & ('transitive$urelstr'(X1) & ('directed$urelstr'(X1) & 'net$ustr'(X1,X0)))) => ! [X2] : (('is$ueventually$uin'(X0,X1,X2) => 'is$uoften$uin'(X0,X1,X2)))))))).
% 31.43/9.48 fof(t29_waybel_9, conjecture, ! [X0] : (((~'empty$ucarrier'(X0) & ('topological$uspace'(X0) & 'top$ustr'(X0))) => ! [X1] : (((~'empty$ucarrier'(X1) & ('transitive$urelstr'(X1) & ('directed$urelstr'(X1) & 'net$ustr'(X1,X0)))) => ! [X2] : ((element(X2,'the$ucarrier'(X0)) => (in(X2,'lim$upoints$uof$unet'(X0,X1)) => 'is$ua$ucluster$upoint$uof$unetstr'(X0,X1,X2))))))))).
% 31.43/9.48 fof(negated_conjecture, negated_conjecture, ~! [X0] : (((~'empty$ucarrier'(X0) & ('topological$uspace'(X0) & 'top$ustr'(X0))) => ! [X1] : (((~'empty$ucarrier'(X1) & ('transitive$urelstr'(X1) & ('directed$urelstr'(X1) & 'net$ustr'(X1,X0)))) => ! [X2] : ((element(X2,'the$ucarrier'(X0)) => (in(X2,'lim$upoints$uof$unet'(X0,X1)) => 'is$ua$ucluster$upoint$uof$unetstr'(X0,X1,X2)))))))), inference(negate_conjecture, [status(cth)], [t29_waybel_9])).
% 31.43/9.48 cnf(c7, plain, ~'directed$urelstr'(X0) | 'empty$ucarrier'(X1) | ~'transitive$urelstr'(X0) | 'empty$ucarrier'(X0) | X2(X1,X0,X3) | ~'top$ustr'(X1) | ~'net$ustr'(X0,X1) | X3 != 'lim$upoints$uof$unet'(X1,X0) | ~'topological$uspace'(X1) | ~element(X3,powerset('the$ucarrier'(X1))), inference(clausification, [status(esa)], [d18_yellow_6])).
% 31.43/9.48 cnf(c9, plain, ~X0(X1,X2,X3) | ~element(X4,'the$ucarrier'(X1)) | ~'point$uneighbourhood'(X5,X1,X4) | 'is$ueventually$uin'(X1,X2,X5) | ~in(X4,X3), inference(clausification, [status(esa)], [d18_yellow_6])).
% 31.43/9.48 cnf(c20, plain, 'empty$ucarrier'(X0) | 'point$uneighbourhood'(sK22(X0,X1,X2),X0,X2) | ~element(X2,'the$ucarrier'(X0)) | 'is$ua$ucluster$upoint$uof$unetstr'(X0,X1,X2) | ~'topological$uspace'(X0) | 'empty$ucarrier'(X1) | ~'net$ustr'(X1,X0) | ~'top$ustr'(X0), inference(clausification, [status(esa)], [d9_waybel_9])).
% 31.43/9.48 cnf(c21, plain, 'empty$ucarrier'(X0) | ~element(X1,'the$ucarrier'(X0)) | 'is$ua$ucluster$upoint$uof$unetstr'(X0,X2,X1) | ~'topological$uspace'(X0) | 'empty$ucarrier'(X2) | ~'net$ustr'(X2,X0) | ~'top$ustr'(X0) | ~'is$uoften$uin'(X0,X2,sK22(X0,X2,X1)), inference(clausification, [status(esa)], [d9_waybel_9])).
% 31.43/9.48 cnf(c22, plain, ~'topological$uspace'(X0) | ~'transitive$urelstr'(X1) | 'empty$ucarrier'(X1) | ~'top$ustr'(X0) | ~'net$ustr'(X1,X0) | 'empty$ucarrier'(X0) | element('lim$upoints$uof$unet'(X0,X1),powerset('the$ucarrier'(X0))) | ~'directed$urelstr'(X1), inference(clausification, [status(esa)], [dt_k11_yellow_6])).
% 31.43/9.48 cnf(c24, plain, ~'top$ustr'(X0) | 'one$usorted$ustr'(X0), inference(clausification, [status(esa)], [dt_l1_pre_topc])).
% 31.43/9.48 cnf(c55, plain, 'empty$ucarrier'(X0) | ~'is$ueventually$uin'(X1,X0,X2) | 'empty$ucarrier'(X1) | 'is$uoften$uin'(X1,X0,X2) | ~'transitive$urelstr'(X0) | ~'directed$urelstr'(X0) | ~'net$ustr'(X0,X1) | ~'one$usorted$ustr'(X1), inference(clausification, [status(esa)], [t28_yellow_6])).
% 31.43/9.48 cnf(c64, plain, ~'empty$ucarrier'(sK76), inference(clausification, [status(esa)], [negated_conjecture])).
% 31.43/9.48 cnf(c65, plain, 'topological$uspace'(sK76), inference(clausification, [status(esa)], [negated_conjecture])).
% 31.43/9.48 cnf(c66, plain, 'top$ustr'(sK76), inference(clausification, [status(esa)], [negated_conjecture])).
% 31.43/9.48 cnf(c67, plain, ~'empty$ucarrier'(sK77), inference(clausification, [status(esa)], [negated_conjecture])).
% 31.43/9.48 cnf(c68, plain, 'transitive$urelstr'(sK77), inference(clausification, [status(esa)], [negated_conjecture])).
% 31.43/9.48 cnf(c69, plain, 'directed$urelstr'(sK77), inference(clausification, [status(esa)], [negated_conjecture])).
% 31.43/9.48 cnf(c70, plain, 'net$ustr'(sK77,sK76), inference(clausification, [status(esa)], [negated_conjecture])).
% 31.43/9.48 cnf(c71, plain, element(sK78,'the$ucarrier'(sK76)), inference(clausification, [status(esa)], [negated_conjecture])).
% 31.43/9.48 cnf(c72, plain, in(sK78,'lim$upoints$uof$unet'(sK76,sK77)), inference(clausification, [status(esa)], [negated_conjecture])).
% 31.43/9.48 cnf(c73, plain, ~'is$ua$ucluster$upoint$uof$unetstr'(sK76,sK77,sK78), inference(clausification, [status(esa)], [negated_conjecture])).
% 31.43/9.48 cnf(d0, plain, ~element(X0,'the$ucarrier'(X1)) | ~'topological$uspace'(X1) | ~'net$ustr'(X2,X1) | ~'top$ustr'(X1) | 'empty$ucarrier'(X2) | 'empty$ucarrier'(X1) | 'is$ua$ucluster$upoint$uof$unetstr'(X1,X2,X0) | ~in(X0,X3) | ~element(X0,'the$ucarrier'(X1)) | ~'Ts8'(X1,X4,X3) | 'is$ueventually$uin'(X1,X4,sK22(X1,X2,X0)), inference(resolution, [status(thm)], [c20,c9])).
% 31.43/9.48 cnf(d1, plain, ~element('lim$upoints$uof$unet'(X0,X1),powerset('the$ucarrier'(X0))) | ~'directed$urelstr'(X1) | ~'topological$uspace'(X0) | ~'net$ustr'(X1,X0) | ~'transitive$urelstr'(X1) | ~'top$ustr'(X0) | 'Ts8'(X0,X1,'lim$upoints$uof$unet'(X0,X1)) | 'empty$ucarrier'(X0) | 'empty$ucarrier'(X1), inference(equality_resolution, [status(thm)], [c7])).
% 31.43/9.48 cnf(d2, plain, ~'directed$urelstr'(X0) | ~'topological$uspace'(X1) | ~'net$ustr'(X0,X1) | ~'transitive$urelstr'(X0) | ~'top$ustr'(X1) | 'Ts8'(X1,X0,'lim$upoints$uof$unet'(X1,X0)) | 'empty$ucarrier'(X0) | 'empty$ucarrier'(X1) | ~'directed$urelstr'(X0) | ~'topological$uspace'(X1) | ~'net$ustr'(X0,X1) | ~'transitive$urelstr'(X0) | ~'top$ustr'(X1) | 'empty$ucarrier'(X1) | 'empty$ucarrier'(X0), inference(resolution, [status(thm)], [d1,c22])).
% 31.43/9.48 cnf(d3, plain, ~'directed$urelstr'(X0) | ~'topological$uspace'(X1) | ~'net$ustr'(X0,X1) | ~'transitive$urelstr'(X0) | ~'top$ustr'(X1) | 'empty$ucarrier'(X1) | 'empty$ucarrier'(X0) | ~in(X2,'lim$upoints$uof$unet'(X1,X0)) | ~element(X2,'the$ucarrier'(X1)) | ~'topological$uspace'(X1) | ~'net$ustr'(X3,X1) | ~'top$ustr'(X1) | 'empty$ucarrier'(X3) | 'empty$ucarrier'(X1) | 'is$ueventually$uin'(X1,X0,sK22(X1,X3,X2)) | 'is$ua$ucluster$upoint$uof$unetstr'(X1,X3,X2), inference(resolution, [status(thm)], [d2,d0])).
% 31.43/9.48 cnf(d4, plain, ~in(X0,'lim$upoints$uof$unet'(X1,X2)) | ~element(X0,'the$ucarrier'(X1)) | ~'directed$urelstr'(X2) | ~'topological$uspace'(X1) | ~'net$ustr'(X3,X1) | ~'net$ustr'(X2,X1) | ~'transitive$urelstr'(X2) | ~'top$ustr'(X1) | 'empty$ucarrier'(X3) | 'empty$ucarrier'(X1) | 'empty$ucarrier'(X2) | 'is$ua$ucluster$upoint$uof$unetstr'(X1,X3,X0) | ~'directed$urelstr'(X2) | ~'net$ustr'(X2,X1) | ~'transitive$urelstr'(X2) | 'empty$ucarrier'(X1) | 'empty$ucarrier'(X2) | 'is$uoften$uin'(X1,X2,sK22(X1,X3,X0)) | ~'one$usorted$ustr'(X1), inference(resolution, [status(thm)], [d3,c55])).
% 31.43/9.48 cnf(d5, plain, ~in(X0,'lim$upoints$uof$unet'(X1,X2)) | ~element(X0,'the$ucarrier'(X1)) | ~'directed$urelstr'(X2) | ~'topological$uspace'(X1) | ~'net$ustr'(X2,X1) | ~'net$ustr'(X2,X1) | ~'transitive$urelstr'(X2) | ~'top$ustr'(X1) | 'empty$ucarrier'(X2) | 'empty$ucarrier'(X2) | 'empty$ucarrier'(X1) | 'is$ua$ucluster$upoint$uof$unetstr'(X1,X2,X0) | ~'one$usorted$ustr'(X1) | ~element(X0,'the$ucarrier'(X1)) | ~'topological$uspace'(X1) | ~'net$ustr'(X2,X1) | ~'top$ustr'(X1) | 'empty$ucarrier'(X2) | 'empty$ucarrier'(X1) | 'is$ua$ucluster$upoint$uof$unetstr'(X1,X2,X0), inference(resolution, [status(thm)], [d4,c21])).
% 31.43/9.48 cnf(d6, plain, ~element(sK78,'the$ucarrier'(sK76)) | ~'directed$urelstr'(sK77) | ~'topological$uspace'(sK76) | ~'net$ustr'(sK77,sK76) | ~'transitive$urelstr'(sK77) | ~'top$ustr'(sK76) | 'empty$ucarrier'(sK77) | 'empty$ucarrier'(sK76) | 'is$ua$ucluster$upoint$uof$unetstr'(sK76,sK77,sK78) | ~'one$usorted$ustr'(sK76), inference(resolution, [status(thm)], [d5,c72])).
% 31.43/9.48 cnf(d7, plain, ~element(sK78,'the$ucarrier'(sK76)) | ~'directed$urelstr'(sK77) | ~'topological$uspace'(sK76) | ~'net$ustr'(sK77,sK76) | ~'transitive$urelstr'(sK77) | ~'top$ustr'(sK76) | 'empty$ucarrier'(sK77) | 'is$ua$ucluster$upoint$uof$unetstr'(sK76,sK77,sK78) | ~'one$usorted$ustr'(sK76), inference(resolution, [status(thm)], [c64,d6])).
% 31.43/9.48 cnf(d8, plain, ~element(sK78,'the$ucarrier'(sK76)) | ~'directed$urelstr'(sK77) | ~'net$ustr'(sK77,sK76) | ~'transitive$urelstr'(sK77) | ~'top$ustr'(sK76) | 'empty$ucarrier'(sK77) | 'is$ua$ucluster$upoint$uof$unetstr'(sK76,sK77,sK78) | ~'one$usorted$ustr'(sK76), inference(resolution, [status(thm)], [c65,d7])).
% 31.43/9.48 cnf(d9, plain, ~element(sK78,'the$ucarrier'(sK76)) | ~'directed$urelstr'(sK77) | ~'net$ustr'(sK77,sK76) | ~'transitive$urelstr'(sK77) | 'empty$ucarrier'(sK77) | 'is$ua$ucluster$upoint$uof$unetstr'(sK76,sK77,sK78) | ~'one$usorted$ustr'(sK76), inference(resolution, [status(thm)], [c66,d8])).
% 31.43/9.48 cnf(d10, plain, ~element(sK78,'the$ucarrier'(sK76)) | ~'directed$urelstr'(sK77) | ~'net$ustr'(sK77,sK76) | ~'transitive$urelstr'(sK77) | 'is$ua$ucluster$upoint$uof$unetstr'(sK76,sK77,sK78) | ~'one$usorted$ustr'(sK76), inference(resolution, [status(thm)], [c67,d9])).
% 31.43/9.48 cnf(d11, plain, ~element(sK78,'the$ucarrier'(sK76)) | ~'directed$urelstr'(sK77) | ~'net$ustr'(sK77,sK76) | 'is$ua$ucluster$upoint$uof$unetstr'(sK76,sK77,sK78) | ~'one$usorted$ustr'(sK76), inference(resolution, [status(thm)], [c68,d10])).
% 31.43/9.48 cnf(d12, plain, ~element(sK78,'the$ucarrier'(sK76)) | ~'net$ustr'(sK77,sK76) | 'is$ua$ucluster$upoint$uof$unetstr'(sK76,sK77,sK78) | ~'one$usorted$ustr'(sK76), inference(resolution, [status(thm)], [c69,d11])).
% 31.43/9.48 cnf(d13, plain, ~element(sK78,'the$ucarrier'(sK76)) | 'is$ua$ucluster$upoint$uof$unetstr'(sK76,sK77,sK78) | ~'one$usorted$ustr'(sK76), inference(resolution, [status(thm)], [c70,d12])).
% 31.43/9.48 cnf(d14, plain, 'is$ua$ucluster$upoint$uof$unetstr'(sK76,sK77,sK78) | ~'one$usorted$ustr'(sK76), inference(resolution, [status(thm)], [c71,d13])).
% 31.43/9.48 cnf(d15, plain, ~'one$usorted$ustr'(sK76), inference(resolution, [status(thm)], [c73,d14])).
% 31.43/9.48 cnf(d16, plain, 'one$usorted$ustr'(sK76), inference(resolution, [status(thm)], [c24,c66])).
% 31.43/9.48 cnf(d17, plain, $false, inference(resolution, [status(thm)], [d16,d15])).
% 31.43/9.48 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------