%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU395+1 : TPTP v9.3.1. Released v3.3.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:41:52 AM UTC 2026
% Result : Theorem 50.71s 11.60s
% Output : CNFRefutation 50.80s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU395+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n017.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 09:20:48 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 50.71/11.60 % SZS status Theorem for theBenchmark.p
% 50.71/11.60 % SZS output start CNFRefutation for theBenchmark.p
% 50.71/11.60 fof(d3_yellow19, axiom, ! [X0] : (((~'empty$ucarrier'(X0) & 'one$usorted$ustr'(X0)) => ! [X1] : (((~'empty$ucarrier'(X1) & 'net$ustr'(X1,X0)) => 'filter$uof$unet$ustr'(X0,X1) = 'a$u2$u1$uyellow19'(X0,X1)))))).
% 50.71/11.60 fof(dt_k2_pre_topc, axiom, ! [X0] : (('one$usorted$ustr'(X0) => element('cast$uas$ucarrier$usubset'(X0),powerset('the$ucarrier'(X0)))))).
% 50.71/11.60 fof(dt_k3_yellow19, axiom, ! [X0] : ! [X1] : ! [X2] : (((~'empty$ucarrier'(X0) & ('one$usorted$ustr'(X0) & (~empty(X1) & (element(X1,powerset('the$ucarrier'(X0))) & (~empty(X2) & ('filtered$usubset'(X2,'boole$uPOSet'(X1)) & ('upper$urelstr$usubset'(X2,'boole$uPOSet'(X1)) & element(X2,powerset('the$ucarrier'('boole$uPOSet'(X1))))))))))) => (~'empty$ucarrier'('net$uof$ubool$ufilter'(X0,X1,X2)) & ('strict$unet$ustr'('net$uof$ubool$ufilter'(X0,X1,X2),X0) & 'net$ustr'('net$uof$ubool$ufilter'(X0,X1,X2),X0)))))).
% 50.71/11.60 fof(dt_l1_pre_topc, axiom, ! [X0] : (('top$ustr'(X0) => 'one$usorted$ustr'(X0)))).
% 50.80/11.60 fof(fc2_pre_topc, axiom, ! [X0] : (((~'empty$ucarrier'(X0) & 'one$usorted$ustr'(X0)) => ~empty('cast$uas$ucarrier$usubset'(X0))))).
% 50.80/11.60 fof(fc4_yellow19, axiom, ! [X0] : ! [X1] : ! [X2] : (((~'empty$ucarrier'(X0) & ('one$usorted$ustr'(X0) & (~empty(X1) & (element(X1,powerset('the$ucarrier'(X0))) & (~empty(X2) & ('filtered$usubset'(X2,'boole$uPOSet'(X1)) & ('upper$urelstr$usubset'(X2,'boole$uPOSet'(X1)) & element(X2,powerset('the$ucarrier'('boole$uPOSet'(X1))))))))))) => (~'empty$ucarrier'('net$uof$ubool$ufilter'(X0,X1,X2)) & ('reflexive$urelstr'('net$uof$ubool$ufilter'(X0,X1,X2)) & ('transitive$urelstr'('net$uof$ubool$ufilter'(X0,X1,X2)) & 'strict$unet$ustr'('net$uof$ubool$ufilter'(X0,X1,X2),X0))))))).
% 50.80/11.60 fof(fc5_yellow19, axiom, ! [X0] : ! [X1] : ! [X2] : (((~'empty$ucarrier'(X0) & ('one$usorted$ustr'(X0) & (~empty(X1) & (element(X1,powerset('the$ucarrier'(X0))) & (~empty(X2) & ('filtered$usubset'(X2,'boole$uPOSet'(X1)) & ('upper$urelstr$usubset'(X2,'boole$uPOSet'(X1)) & ('proper$uelement'(X2,powerset('the$ucarrier'('boole$uPOSet'(X1)))) & element(X2,powerset('the$ucarrier'('boole$uPOSet'(X1)))))))))))) => (~'empty$ucarrier'('net$uof$ubool$ufilter'(X0,X1,X2)) & ('reflexive$urelstr'('net$uof$ubool$ufilter'(X0,X1,X2)) & ('transitive$urelstr'('net$uof$ubool$ufilter'(X0,X1,X2)) & ('strict$unet$ustr'('net$uof$ubool$ufilter'(X0,X1,X2),X0) & 'directed$urelstr'('net$uof$ubool$ufilter'(X0,X1,X2))))))))).
% 50.80/11.60 fof(t13_yellow19, 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,'the$ucarrier'(X0)) => (in(X2,'lim$upoints$uof$unet'(X0,X1)) <=> 'is$ua$uconvergence$upoint$uof$uset'(X0,'filter$uof$unet$ustr'(X0,X1),X2))))))))).
% 50.80/11.60 fof(t15_yellow19, axiom, ! [X0] : (((~'empty$ucarrier'(X0) & 'one$usorted$ustr'(X0)) => ! [X1] : (((~empty(X1) & ('filtered$usubset'(X1,'boole$uPOSet'('cast$uas$ucarrier$usubset'(X0))) & ('upper$urelstr$usubset'(X1,'boole$uPOSet'('cast$uas$ucarrier$usubset'(X0))) & ('proper$uelement'(X1,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(X0))))) & element(X1,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(X0))))))))) => X1 = 'filter$uof$unet$ustr'(X0,'net$uof$ubool$ufilter'(X0,'cast$uas$ucarrier$usubset'(X0),X1))))))).
% 50.80/11.60 fof(t18_yellow19, conjecture, ! [X0] : (((~'empty$ucarrier'(X0) & ('topological$uspace'(X0) & 'top$ustr'(X0))) => ! [X1] : (((~empty(X1) & ('filtered$usubset'(X1,'boole$uPOSet'('cast$uas$ucarrier$usubset'(X0))) & ('upper$urelstr$usubset'(X1,'boole$uPOSet'('cast$uas$ucarrier$usubset'(X0))) & ('proper$uelement'(X1,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(X0))))) & element(X1,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(X0))))))))) => ! [X2] : ((element(X2,'the$ucarrier'(X0)) => (in(X2,'lim$upoints$uof$unet'(X0,'net$uof$ubool$ufilter'(X0,'cast$uas$ucarrier$usubset'(X0),X1))) <=> 'is$ua$uconvergence$upoint$uof$uset'(X0,X1,X2))))))))).
% 50.80/11.60 fof(negated_conjecture, negated_conjecture, ~! [X0] : (((~'empty$ucarrier'(X0) & ('topological$uspace'(X0) & 'top$ustr'(X0))) => ! [X1] : (((~empty(X1) & ('filtered$usubset'(X1,'boole$uPOSet'('cast$uas$ucarrier$usubset'(X0))) & ('upper$urelstr$usubset'(X1,'boole$uPOSet'('cast$uas$ucarrier$usubset'(X0))) & ('proper$uelement'(X1,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(X0))))) & element(X1,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(X0))))))))) => ! [X2] : ((element(X2,'the$ucarrier'(X0)) => (in(X2,'lim$upoints$uof$unet'(X0,'net$uof$ubool$ufilter'(X0,'cast$uas$ucarrier$usubset'(X0),X1))) <=> 'is$ua$uconvergence$upoint$uof$uset'(X0,X1,X2)))))))), inference(negate_conjecture, [status(cth)], [t18_yellow19])).
% 50.80/11.60 cnf(c76, plain, ~'net$ustr'(X0,X1) | 'empty$ucarrier'(X1) | 'a$u2$u1$uyellow19'(X1,X0) = 'filter$uof$unet$ustr'(X1,X0) | 'empty$ucarrier'(X0) | ~'one$usorted$ustr'(X1), inference(clausification, [status(esa)], [d3_yellow19])).
% 50.80/11.60 cnf(c82, plain, ~'one$usorted$ustr'(X0) | element('cast$uas$ucarrier$usubset'(X0),powerset('the$ucarrier'(X0))), inference(clausification, [status(esa)], [dt_k2_pre_topc])).
% 50.80/11.60 cnf(c84, plain, 'empty$ucarrier'(X0) | empty(X1) | ~'one$usorted$ustr'(X0) | ~'upper$urelstr$usubset'(X1,'boole$uPOSet'(X2)) | ~element(X1,powerset('the$ucarrier'('boole$uPOSet'(X2)))) | ~'empty$ucarrier'('net$uof$ubool$ufilter'(X0,X2,X1)) | ~'filtered$usubset'(X1,'boole$uPOSet'(X2)) | ~element(X2,powerset('the$ucarrier'(X0))) | empty(X2), inference(clausification, [status(esa)], [dt_k3_yellow19])).
% 50.80/11.60 cnf(c85, plain, 'empty$ucarrier'(X0) | empty(X1) | ~'one$usorted$ustr'(X0) | ~'upper$urelstr$usubset'(X1,'boole$uPOSet'(X2)) | ~element(X1,powerset('the$ucarrier'('boole$uPOSet'(X2)))) | 'net$ustr'('net$uof$ubool$ufilter'(X0,X2,X1),X0) | ~'filtered$usubset'(X1,'boole$uPOSet'(X2)) | ~element(X2,powerset('the$ucarrier'(X0))) | empty(X2), inference(clausification, [status(esa)], [dt_k3_yellow19])).
% 50.80/11.60 cnf(c90, plain, ~'top$ustr'(X0) | 'one$usorted$ustr'(X0), inference(clausification, [status(esa)], [dt_l1_pre_topc])).
% 50.80/11.60 cnf(c135, plain, ~'one$usorted$ustr'(X0) | 'empty$ucarrier'(X0) | ~empty('cast$uas$ucarrier$usubset'(X0)), inference(clausification, [status(esa)], [fc2_pre_topc])).
% 50.80/11.60 cnf(c173, plain, ~'upper$urelstr$usubset'(X0,'boole$uPOSet'(X1)) | ~'one$usorted$ustr'(X2) | empty(X1) | ~element(X1,powerset('the$ucarrier'(X2))) | ~'filtered$usubset'(X0,'boole$uPOSet'(X1)) | 'transitive$urelstr'('net$uof$ubool$ufilter'(X2,X1,X0)) | empty(X0) | 'empty$ucarrier'(X2) | ~element(X0,powerset('the$ucarrier'('boole$uPOSet'(X1)))), inference(clausification, [status(esa)], [fc4_yellow19])).
% 50.80/11.60 cnf(c179, plain, ~element(X0,powerset('the$ucarrier'(X1))) | ~'one$usorted$ustr'(X1) | ~'filtered$usubset'(X2,'boole$uPOSet'(X0)) | empty(X0) | ~element(X2,powerset('the$ucarrier'('boole$uPOSet'(X0)))) | ~'proper$uelement'(X2,powerset('the$ucarrier'('boole$uPOSet'(X0)))) | empty(X2) | X3(X1,X0,X2) | ~'upper$urelstr$usubset'(X2,'boole$uPOSet'(X0)) | 'empty$ucarrier'(X1), inference(clausification, [status(esa)], [fc5_yellow19])).
% 50.80/11.60 cnf(c182, plain, ~X0(X1,X2,X3) | 'directed$urelstr'('net$uof$ubool$ufilter'(X1,X2,X3)), inference(clausification, [status(esa)], [fc5_yellow19])).
% 50.80/11.60 cnf(c423, plain, ~'top$ustr'(X0) | ~'topological$uspace'(X0) | 'empty$ucarrier'(X1) | ~'transitive$urelstr'(X1) | ~in(X2,'lim$upoints$uof$unet'(X0,X1)) | 'is$ua$uconvergence$upoint$uof$uset'(X0,'filter$uof$unet$ustr'(X0,X1),X2) | 'empty$ucarrier'(X0) | ~element(X2,'the$ucarrier'(X0)) | ~'directed$urelstr'(X1) | ~'net$ustr'(X1,X0), inference(clausification, [status(esa)], [t13_yellow19])).
% 50.80/11.60 cnf(c424, plain, ~'top$ustr'(X0) | ~'topological$uspace'(X0) | 'empty$ucarrier'(X1) | ~'transitive$urelstr'(X1) | ~'is$ua$uconvergence$upoint$uof$uset'(X0,'filter$uof$unet$ustr'(X0,X1),X2) | 'empty$ucarrier'(X0) | in(X2,'lim$upoints$uof$unet'(X0,X1)) | ~element(X2,'the$ucarrier'(X0)) | ~'directed$urelstr'(X1) | ~'net$ustr'(X1,X0), inference(clausification, [status(esa)], [t13_yellow19])).
% 50.80/11.60 cnf(c425, plain, ~'upper$urelstr$usubset'(X0,'boole$uPOSet'('cast$uas$ucarrier$usubset'(X1))) | ~'proper$uelement'(X0,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(X1))))) | 'empty$ucarrier'(X1) | ~'filtered$usubset'(X0,'boole$uPOSet'('cast$uas$ucarrier$usubset'(X1))) | ~'one$usorted$ustr'(X1) | 'filter$uof$unet$ustr'(X1,'net$uof$ubool$ufilter'(X1,'cast$uas$ucarrier$usubset'(X1),X0)) = X0 | empty(X0) | ~element(X0,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(X1))))), inference(clausification, [status(esa)], [t15_yellow19])).
% 50.80/11.60 cnf(c439, plain, 'topological$uspace'(sK235), inference(clausification, [status(esa)], [negated_conjecture])).
% 50.80/11.60 cnf(c440, plain, 'top$ustr'(sK235), inference(clausification, [status(esa)], [negated_conjecture])).
% 50.80/11.60 cnf(c441, plain, ~'empty$ucarrier'(sK235), inference(clausification, [status(esa)], [negated_conjecture])).
% 50.80/11.60 cnf(c442, plain, 'filtered$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))), inference(clausification, [status(esa)], [negated_conjecture])).
% 50.80/11.60 cnf(c443, plain, 'proper$uelement'(sK236,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))))), inference(clausification, [status(esa)], [negated_conjecture])).
% 50.80/11.60 cnf(c444, plain, element(sK236,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))))), inference(clausification, [status(esa)], [negated_conjecture])).
% 50.80/11.60 cnf(c445, plain, 'upper$urelstr$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))), inference(clausification, [status(esa)], [negated_conjecture])).
% 50.80/11.60 cnf(c446, plain, ~empty(sK236), inference(clausification, [status(esa)], [negated_conjecture])).
% 50.80/11.60 cnf(c447, plain, element(sK237,'the$ucarrier'(sK235)), inference(clausification, [status(esa)], [negated_conjecture])).
% 50.80/11.60 cnf(c449, plain, in(sK237,'lim$upoints$uof$unet'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236))) | 'is$ua$uconvergence$upoint$uof$uset'(sK235,sK236,sK237), inference(clausification, [status(esa)], [negated_conjecture])).
% 50.80/11.60 cnf(c450, plain, ~'is$ua$uconvergence$upoint$uof$uset'(sK235,sK236,sK237) | ~in(sK237,'lim$upoints$uof$unet'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236))), inference(clausification, [status(esa)], [negated_conjecture])).
% 50.80/11.60 cnf(d0, plain, ~'one$usorted$ustr'(X0) | 'net$ustr'('net$uof$ubool$ufilter'(X0,'cast$uas$ucarrier$usubset'(sK235),sK236),X0) | 'empty$ucarrier'(X0) | empty('cast$uas$ucarrier$usubset'(sK235)) | empty(sK236) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(X0))) | ~'upper$urelstr$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))) | ~'filtered$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))), inference(resolution, [status(thm)], [c85,c444])).
% 50.80/11.60 cnf(d1, plain, ~'one$usorted$ustr'(X0) | 'net$ustr'('net$uof$ubool$ufilter'(X0,'cast$uas$ucarrier$usubset'(sK235),sK236),X0) | 'empty$ucarrier'(X0) | empty('cast$uas$ucarrier$usubset'(sK235)) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(X0))) | ~'upper$urelstr$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))) | ~'filtered$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))), inference(resolution, [status(thm)], [c446,d0])).
% 50.80/11.60 cnf(d2, plain, ~'one$usorted$ustr'(X0) | 'net$ustr'('net$uof$ubool$ufilter'(X0,'cast$uas$ucarrier$usubset'(sK235),sK236),X0) | 'empty$ucarrier'(X0) | empty('cast$uas$ucarrier$usubset'(sK235)) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(X0))) | ~'upper$urelstr$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))), inference(resolution, [status(thm)], [c442,d1])).
% 50.80/11.60 cnf(d3, plain, ~'one$usorted$ustr'(X0) | 'net$ustr'('net$uof$ubool$ufilter'(X0,'cast$uas$ucarrier$usubset'(sK235),sK236),X0) | 'empty$ucarrier'(X0) | empty('cast$uas$ucarrier$usubset'(sK235)) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(X0))), inference(resolution, [status(thm)], [c445,d2])).
% 50.80/11.60 cnf(d4, plain, ~'one$usorted$ustr'(X0) | 'empty$ucarrier'(X0) | empty('cast$uas$ucarrier$usubset'(sK235)) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(X0))) | 'a$u2$u1$uyellow19'(X0,'net$uof$ubool$ufilter'(X0,'cast$uas$ucarrier$usubset'(sK235),sK236)) = 'filter$uof$unet$ustr'(X0,'net$uof$ubool$ufilter'(X0,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'one$usorted$ustr'(X0) | 'empty$ucarrier'(X0) | 'empty$ucarrier'('net$uof$ubool$ufilter'(X0,'cast$uas$ucarrier$usubset'(sK235),sK236)), inference(resolution, [status(thm)], [d3,c76])).
% 50.80/11.60 cnf(d5, plain, ~'one$usorted$ustr'(X0) | 'empty$ucarrier'(X0) | ~'empty$ucarrier'('net$uof$ubool$ufilter'(X0,'cast$uas$ucarrier$usubset'(sK235),sK236)) | empty('cast$uas$ucarrier$usubset'(sK235)) | empty(sK236) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(X0))) | ~'upper$urelstr$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))) | ~'filtered$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))), inference(resolution, [status(thm)], [c84,c444])).
% 50.80/11.60 cnf(d6, plain, ~'one$usorted$ustr'(X0) | 'empty$ucarrier'(X0) | ~'empty$ucarrier'('net$uof$ubool$ufilter'(X0,'cast$uas$ucarrier$usubset'(sK235),sK236)) | empty('cast$uas$ucarrier$usubset'(sK235)) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(X0))) | ~'upper$urelstr$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))) | ~'filtered$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))), inference(resolution, [status(thm)], [c446,d5])).
% 50.80/11.60 cnf(d7, plain, ~'one$usorted$ustr'(X0) | 'empty$ucarrier'(X0) | ~'empty$ucarrier'('net$uof$ubool$ufilter'(X0,'cast$uas$ucarrier$usubset'(sK235),sK236)) | empty('cast$uas$ucarrier$usubset'(sK235)) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(X0))) | ~'upper$urelstr$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))), inference(resolution, [status(thm)], [c442,d6])).
% 50.80/11.60 cnf(d8, plain, ~'one$usorted$ustr'(X0) | 'empty$ucarrier'(X0) | ~'empty$ucarrier'('net$uof$ubool$ufilter'(X0,'cast$uas$ucarrier$usubset'(sK235),sK236)) | empty('cast$uas$ucarrier$usubset'(sK235)) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(X0))), inference(resolution, [status(thm)], [c445,d7])).
% 50.80/11.60 cnf(d9, plain, ~'one$usorted$ustr'(X0) | 'empty$ucarrier'(X0) | empty('cast$uas$ucarrier$usubset'(sK235)) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(X0))) | 'a$u2$u1$uyellow19'(X0,'net$uof$ubool$ufilter'(X0,'cast$uas$ucarrier$usubset'(sK235),sK236)) = 'filter$uof$unet$ustr'(X0,'net$uof$ubool$ufilter'(X0,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'one$usorted$ustr'(X0) | 'empty$ucarrier'(X0) | empty('cast$uas$ucarrier$usubset'(sK235)) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(X0))), inference(resolution, [status(thm)], [d8,d4])).
% 50.80/11.60 cnf(d10, plain, 'a$u2$u1$uyellow19'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) = 'filter$uof$unet$ustr'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'one$usorted$ustr'(sK235) | 'empty$ucarrier'(sK235) | empty('cast$uas$ucarrier$usubset'(sK235)) | ~'one$usorted$ustr'(sK235), inference(resolution, [status(thm)], [d9,c82])).
% 50.80/11.60 cnf(d11, plain, 'a$u2$u1$uyellow19'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) = 'filter$uof$unet$ustr'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'one$usorted$ustr'(sK235) | empty('cast$uas$ucarrier$usubset'(sK235)), inference(resolution, [status(thm)], [c441,d10])).
% 50.80/11.60 cnf(d12, plain, 'one$usorted$ustr'(sK235), inference(resolution, [status(thm)], [c90,c440])).
% 50.80/11.60 cnf(d13, plain, 'a$u2$u1$uyellow19'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) = 'filter$uof$unet$ustr'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | empty('cast$uas$ucarrier$usubset'(sK235)), inference(resolution, [status(thm)], [d12,d11])).
% 50.80/11.60 cnf(d14, plain, 'a$u2$u1$uyellow19'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) = 'filter$uof$unet$ustr'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'one$usorted$ustr'(sK235) | 'empty$ucarrier'(sK235), inference(resolution, [status(thm)], [d13,c135])).
% 50.80/11.60 cnf(d15, plain, 'a$u2$u1$uyellow19'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) = 'filter$uof$unet$ustr'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'one$usorted$ustr'(sK235), inference(resolution, [status(thm)], [c441,d14])).
% 50.80/11.60 cnf(d16, plain, 'a$u2$u1$uyellow19'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) = 'filter$uof$unet$ustr'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)), inference(resolution, [status(thm)], [d12,d15])).
% 50.80/11.60 cnf(d17, plain, 'filter$uof$unet$ustr'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) = sK236 | ~'one$usorted$ustr'(sK235) | 'empty$ucarrier'(sK235) | empty(sK236) | ~element(sK236,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))))) | ~'upper$urelstr$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))) | ~'filtered$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))), inference(resolution, [status(thm)], [c425,c443])).
% 50.80/11.60 cnf(d18, plain, 'a$u2$u1$uyellow19'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) = sK236 | ~'one$usorted$ustr'(sK235) | 'empty$ucarrier'(sK235) | empty(sK236) | ~element(sK236,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))))) | ~'upper$urelstr$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))) | ~'filtered$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))), inference(demodulation, [status(thm)], [d17,d16])).
% 50.80/11.60 cnf(d19, plain, 'a$u2$u1$uyellow19'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) = sK236 | ~'one$usorted$ustr'(sK235) | empty(sK236) | ~element(sK236,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))))) | ~'upper$urelstr$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))) | ~'filtered$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))), inference(resolution, [status(thm)], [c441,d18])).
% 50.80/11.60 cnf(d20, plain, 'a$u2$u1$uyellow19'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) = sK236 | ~'one$usorted$ustr'(sK235) | ~element(sK236,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))))) | ~'upper$urelstr$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))) | ~'filtered$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))), inference(resolution, [status(thm)], [c446,d19])).
% 50.80/11.60 cnf(d21, plain, 'a$u2$u1$uyellow19'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) = sK236 | ~'one$usorted$ustr'(sK235) | ~element(sK236,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))))) | ~'upper$urelstr$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))), inference(resolution, [status(thm)], [c442,d20])).
% 50.80/11.60 cnf(d22, plain, 'a$u2$u1$uyellow19'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) = sK236 | ~'one$usorted$ustr'(sK235) | ~element(sK236,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))))), inference(resolution, [status(thm)], [c445,d21])).
% 50.80/11.60 cnf(d23, plain, 'a$u2$u1$uyellow19'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) = sK236 | ~'one$usorted$ustr'(sK235), inference(resolution, [status(thm)], [c444,d22])).
% 50.80/11.60 cnf(d24, plain, 'a$u2$u1$uyellow19'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) = sK236, inference(resolution, [status(thm)], [d12,d23])).
% 50.80/11.60 cnf(d25, plain, ~'is$ua$uconvergence$upoint$uof$uset'(sK235,'a$u2$u1$uyellow19'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)),X0) | ~'net$ustr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236),sK235) | in(X0,'lim$upoints$uof$unet'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236))) | 'empty$ucarrier'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | 'empty$ucarrier'(sK235) | ~'transitive$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~element(X0,'the$ucarrier'(sK235)) | ~'top$ustr'(sK235) | ~'topological$uspace'(sK235) | ~'directed$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)), inference(superposition, [status(thm)], [d16,c424])).
% 50.80/11.60 cnf(d26, plain, ~'net$ustr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236),sK235) | in(X0,'lim$upoints$uof$unet'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236))) | 'empty$ucarrier'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | 'empty$ucarrier'(sK235) | ~'transitive$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~element(X0,'the$ucarrier'(sK235)) | ~'top$ustr'(sK235) | ~'topological$uspace'(sK235) | ~'directed$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'is$ua$uconvergence$upoint$uof$uset'(sK235,sK236,X0), inference(demodulation, [status(thm)], [d25,d24])).
% 50.80/11.60 cnf(d27, plain, ~'net$ustr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236),sK235) | in(X0,'lim$upoints$uof$unet'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236))) | 'empty$ucarrier'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | 'empty$ucarrier'(sK235) | ~'transitive$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~element(X0,'the$ucarrier'(sK235)) | ~'top$ustr'(sK235) | ~'directed$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'is$ua$uconvergence$upoint$uof$uset'(sK235,sK236,X0), inference(resolution, [status(thm)], [c439,d26])).
% 50.80/11.60 cnf(d28, plain, ~'net$ustr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236),sK235) | in(X0,'lim$upoints$uof$unet'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236))) | 'empty$ucarrier'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | 'empty$ucarrier'(sK235) | ~'transitive$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~element(X0,'the$ucarrier'(sK235)) | ~'directed$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'is$ua$uconvergence$upoint$uof$uset'(sK235,sK236,X0), inference(resolution, [status(thm)], [c440,d27])).
% 50.80/11.60 cnf(d29, plain, ~'net$ustr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236),sK235) | in(X0,'lim$upoints$uof$unet'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236))) | 'empty$ucarrier'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'transitive$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~element(X0,'the$ucarrier'(sK235)) | ~'directed$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'is$ua$uconvergence$upoint$uof$uset'(sK235,sK236,X0), inference(resolution, [status(thm)], [c441,d28])).
% 50.80/11.60 cnf(d30, plain, ~'net$ustr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236),sK235) | 'empty$ucarrier'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'transitive$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~element(sK237,'the$ucarrier'(sK235)) | ~'directed$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'is$ua$uconvergence$upoint$uof$uset'(sK235,sK236,sK237) | ~'is$ua$uconvergence$upoint$uof$uset'(sK235,sK236,sK237), inference(resolution, [status(thm)], [d29,c450])).
% 50.80/11.60 cnf(d31, plain, ~'net$ustr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236),sK235) | 'empty$ucarrier'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'transitive$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'directed$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'is$ua$uconvergence$upoint$uof$uset'(sK235,sK236,sK237), inference(resolution, [status(thm)], [c447,d30])).
% 50.80/11.60 cnf(d32, plain, 'is$ua$uconvergence$upoint$uof$uset'(sK235,'a$u2$u1$uyellow19'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)),X0) | ~'net$ustr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236),sK235) | ~in(X0,'lim$upoints$uof$unet'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236))) | 'empty$ucarrier'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | 'empty$ucarrier'(sK235) | ~'transitive$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~element(X0,'the$ucarrier'(sK235)) | ~'top$ustr'(sK235) | ~'topological$uspace'(sK235) | ~'directed$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)), inference(superposition, [status(thm)], [d16,c423])).
% 50.80/11.60 cnf(d33, plain, ~'net$ustr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236),sK235) | ~in(X0,'lim$upoints$uof$unet'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236))) | 'empty$ucarrier'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | 'empty$ucarrier'(sK235) | ~'transitive$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~element(X0,'the$ucarrier'(sK235)) | ~'top$ustr'(sK235) | ~'topological$uspace'(sK235) | ~'directed$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | 'is$ua$uconvergence$upoint$uof$uset'(sK235,sK236,X0), inference(demodulation, [status(thm)], [d32,d24])).
% 50.80/11.60 cnf(d34, plain, ~'net$ustr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236),sK235) | ~in(X0,'lim$upoints$uof$unet'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236))) | 'empty$ucarrier'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | 'empty$ucarrier'(sK235) | ~'transitive$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~element(X0,'the$ucarrier'(sK235)) | ~'top$ustr'(sK235) | ~'directed$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | 'is$ua$uconvergence$upoint$uof$uset'(sK235,sK236,X0), inference(resolution, [status(thm)], [c439,d33])).
% 50.80/11.60 cnf(d35, plain, ~'net$ustr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236),sK235) | ~in(X0,'lim$upoints$uof$unet'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236))) | 'empty$ucarrier'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | 'empty$ucarrier'(sK235) | ~'transitive$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~element(X0,'the$ucarrier'(sK235)) | ~'directed$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | 'is$ua$uconvergence$upoint$uof$uset'(sK235,sK236,X0), inference(resolution, [status(thm)], [c440,d34])).
% 50.80/11.60 cnf(d36, plain, ~'net$ustr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236),sK235) | ~in(X0,'lim$upoints$uof$unet'(sK235,'net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236))) | 'empty$ucarrier'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'transitive$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~element(X0,'the$ucarrier'(sK235)) | ~'directed$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | 'is$ua$uconvergence$upoint$uof$uset'(sK235,sK236,X0), inference(resolution, [status(thm)], [c441,d35])).
% 50.80/11.60 cnf(d37, plain, ~'net$ustr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236),sK235) | 'empty$ucarrier'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'transitive$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~element(sK237,'the$ucarrier'(sK235)) | ~'directed$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | 'is$ua$uconvergence$upoint$uof$uset'(sK235,sK236,sK237) | 'is$ua$uconvergence$upoint$uof$uset'(sK235,sK236,sK237), inference(resolution, [status(thm)], [d36,c449])).
% 50.80/11.60 cnf(d38, plain, ~'net$ustr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236),sK235) | 'empty$ucarrier'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'transitive$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'directed$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | 'is$ua$uconvergence$upoint$uof$uset'(sK235,sK236,sK237), inference(resolution, [status(thm)], [c447,d37])).
% 50.80/11.60 cnf(d39, plain, ~'net$ustr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236),sK235) | 'empty$ucarrier'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'transitive$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'directed$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'net$ustr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236),sK235) | 'empty$ucarrier'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'transitive$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'directed$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)), inference(resolution, [status(thm)], [d38,d31])).
% 50.80/11.60 cnf(d40, plain, 'empty$ucarrier'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'transitive$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'directed$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'one$usorted$ustr'(sK235) | 'empty$ucarrier'(sK235) | empty('cast$uas$ucarrier$usubset'(sK235)) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(sK235))), inference(resolution, [status(thm)], [d39,d3])).
% 50.80/11.60 cnf(d41, plain, ~'one$usorted$ustr'(sK235) | 'empty$ucarrier'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'transitive$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | empty('cast$uas$ucarrier$usubset'(sK235)) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(sK235))) | ~'directed$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)), inference(resolution, [status(thm)], [c441,d40])).
% 50.80/11.60 cnf(d42, plain, 'empty$ucarrier'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | ~'transitive$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | empty('cast$uas$ucarrier$usubset'(sK235)) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(sK235))) | ~'directed$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)), inference(resolution, [status(thm)], [d12,d41])).
% 50.80/11.60 cnf(d43, plain, ~'one$usorted$ustr'(sK235) | 'empty$ucarrier'(sK235) | ~'empty$ucarrier'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | empty('cast$uas$ucarrier$usubset'(sK235)) | ~'one$usorted$ustr'(sK235), inference(resolution, [status(thm)], [d8,c82])).
% 50.80/11.60 cnf(d44, plain, ~'one$usorted$ustr'(sK235) | ~'empty$ucarrier'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | empty('cast$uas$ucarrier$usubset'(sK235)), inference(resolution, [status(thm)], [c441,d43])).
% 50.80/11.60 cnf(d45, plain, ~'empty$ucarrier'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | empty('cast$uas$ucarrier$usubset'(sK235)), inference(resolution, [status(thm)], [d12,d44])).
% 50.80/11.60 cnf(d46, plain, empty('cast$uas$ucarrier$usubset'(sK235)) | ~'transitive$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | empty('cast$uas$ucarrier$usubset'(sK235)) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(sK235))) | ~'directed$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)), inference(resolution, [status(thm)], [d45,d42])).
% 50.80/11.60 cnf(d47, plain, ~'one$usorted$ustr'(X0) | 'empty$ucarrier'(X0) | 'transitive$urelstr'('net$uof$ubool$ufilter'(X0,'cast$uas$ucarrier$usubset'(sK235),sK236)) | empty('cast$uas$ucarrier$usubset'(sK235)) | empty(sK236) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(X0))) | ~'upper$urelstr$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))) | ~'filtered$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))), inference(resolution, [status(thm)], [c173,c444])).
% 50.80/11.60 cnf(d48, plain, ~'one$usorted$ustr'(X0) | 'empty$ucarrier'(X0) | 'transitive$urelstr'('net$uof$ubool$ufilter'(X0,'cast$uas$ucarrier$usubset'(sK235),sK236)) | empty('cast$uas$ucarrier$usubset'(sK235)) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(X0))) | ~'upper$urelstr$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))) | ~'filtered$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))), inference(resolution, [status(thm)], [c446,d47])).
% 50.80/11.60 cnf(d49, plain, ~'one$usorted$ustr'(X0) | 'empty$ucarrier'(X0) | 'transitive$urelstr'('net$uof$ubool$ufilter'(X0,'cast$uas$ucarrier$usubset'(sK235),sK236)) | empty('cast$uas$ucarrier$usubset'(sK235)) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(X0))) | ~'upper$urelstr$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))), inference(resolution, [status(thm)], [c442,d48])).
% 50.80/11.60 cnf(d50, plain, ~'one$usorted$ustr'(X0) | 'empty$ucarrier'(X0) | 'transitive$urelstr'('net$uof$ubool$ufilter'(X0,'cast$uas$ucarrier$usubset'(sK235),sK236)) | empty('cast$uas$ucarrier$usubset'(sK235)) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(X0))), inference(resolution, [status(thm)], [c445,d49])).
% 50.80/11.60 cnf(d51, plain, ~'one$usorted$ustr'(sK235) | 'empty$ucarrier'(sK235) | 'transitive$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | empty('cast$uas$ucarrier$usubset'(sK235)) | ~'one$usorted$ustr'(sK235), inference(resolution, [status(thm)], [d50,c82])).
% 50.80/11.60 cnf(d52, plain, ~'one$usorted$ustr'(sK235) | 'transitive$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | empty('cast$uas$ucarrier$usubset'(sK235)), inference(resolution, [status(thm)], [c441,d51])).
% 50.80/11.60 cnf(d53, plain, 'transitive$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)) | empty('cast$uas$ucarrier$usubset'(sK235)), inference(resolution, [status(thm)], [d12,d52])).
% 50.80/11.60 cnf(d54, plain, empty('cast$uas$ucarrier$usubset'(sK235)) | empty('cast$uas$ucarrier$usubset'(sK235)) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(sK235))) | ~'directed$urelstr'('net$uof$ubool$ufilter'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236)), inference(resolution, [status(thm)], [d53,d46])).
% 50.80/11.60 cnf(d55, plain, empty('cast$uas$ucarrier$usubset'(sK235)) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(sK235))) | ~'Ts108'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236), inference(resolution, [status(thm)], [d54,c182])).
% 50.80/11.60 cnf(d56, plain, ~'one$usorted$ustr'(X0) | 'empty$ucarrier'(X0) | empty('cast$uas$ucarrier$usubset'(sK235)) | empty(sK236) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(X0))) | ~element(sK236,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))))) | ~'upper$urelstr$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))) | ~'filtered$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))) | 'Ts108'(X0,'cast$uas$ucarrier$usubset'(sK235),sK236), inference(resolution, [status(thm)], [c179,c443])).
% 50.80/11.60 cnf(d57, plain, ~'one$usorted$ustr'(X0) | 'empty$ucarrier'(X0) | empty('cast$uas$ucarrier$usubset'(sK235)) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(X0))) | ~element(sK236,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))))) | ~'upper$urelstr$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))) | ~'filtered$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))) | 'Ts108'(X0,'cast$uas$ucarrier$usubset'(sK235),sK236), inference(resolution, [status(thm)], [c446,d56])).
% 50.80/11.60 cnf(d58, plain, ~'one$usorted$ustr'(X0) | 'empty$ucarrier'(X0) | empty('cast$uas$ucarrier$usubset'(sK235)) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(X0))) | ~element(sK236,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))))) | ~'upper$urelstr$usubset'(sK236,'boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))) | 'Ts108'(X0,'cast$uas$ucarrier$usubset'(sK235),sK236), inference(resolution, [status(thm)], [c442,d57])).
% 50.80/11.60 cnf(d59, plain, ~'one$usorted$ustr'(X0) | 'empty$ucarrier'(X0) | empty('cast$uas$ucarrier$usubset'(sK235)) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(X0))) | ~element(sK236,powerset('the$ucarrier'('boole$uPOSet'('cast$uas$ucarrier$usubset'(sK235))))) | 'Ts108'(X0,'cast$uas$ucarrier$usubset'(sK235),sK236), inference(resolution, [status(thm)], [c445,d58])).
% 50.80/11.60 cnf(d60, plain, ~'one$usorted$ustr'(X0) | 'empty$ucarrier'(X0) | empty('cast$uas$ucarrier$usubset'(sK235)) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(X0))) | 'Ts108'(X0,'cast$uas$ucarrier$usubset'(sK235),sK236), inference(resolution, [status(thm)], [c444,d59])).
% 50.80/11.60 cnf(d61, plain, ~'one$usorted$ustr'(sK235) | 'empty$ucarrier'(sK235) | empty('cast$uas$ucarrier$usubset'(sK235)) | 'Ts108'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236) | ~'one$usorted$ustr'(sK235), inference(resolution, [status(thm)], [d60,c82])).
% 50.80/11.60 cnf(d62, plain, ~'one$usorted$ustr'(sK235) | empty('cast$uas$ucarrier$usubset'(sK235)) | 'Ts108'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236), inference(resolution, [status(thm)], [c441,d61])).
% 50.80/11.60 cnf(d63, plain, empty('cast$uas$ucarrier$usubset'(sK235)) | 'Ts108'(sK235,'cast$uas$ucarrier$usubset'(sK235),sK236), inference(resolution, [status(thm)], [d12,d62])).
% 50.80/11.60 cnf(d64, plain, empty('cast$uas$ucarrier$usubset'(sK235)) | empty('cast$uas$ucarrier$usubset'(sK235)) | ~element('cast$uas$ucarrier$usubset'(sK235),powerset('the$ucarrier'(sK235))), inference(resolution, [status(thm)], [d63,d55])).
% 50.80/11.60 cnf(d65, plain, empty('cast$uas$ucarrier$usubset'(sK235)) | ~'one$usorted$ustr'(sK235), inference(resolution, [status(thm)], [d64,c82])).
% 50.80/11.60 cnf(d66, plain, empty('cast$uas$ucarrier$usubset'(sK235)), inference(resolution, [status(thm)], [d12,d65])).
% 50.80/11.60 cnf(d67, plain, ~'one$usorted$ustr'(sK235) | 'empty$ucarrier'(sK235), inference(resolution, [status(thm)], [d66,c135])).
% 50.80/11.60 cnf(d68, plain, ~'one$usorted$ustr'(sK235), inference(resolution, [status(thm)], [c441,d67])).
% 50.80/11.60 cnf(d69, plain, $false, inference(resolution, [status(thm)], [d12,d68])).
% 50.80/11.60 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------