%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU376+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 : n015.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:49 AM UTC 2026
% Result : Theorem 44.04s 10.85s
% Output : CNFRefutation 44.04s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU376+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.39 % Computer : n015.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sat Sep 26 09:25:14 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 44.04/10.85 % SZS status Theorem for theBenchmark.p
% 44.04/10.85 % SZS output start CNFRefutation for theBenchmark.p
% 44.04/10.85 fof(d11_waybel_0, axiom, ! [X0] : (((~'empty$ucarrier'(X0) & 'one$usorted$ustr'(X0)) => ! [X1] : (((~'empty$ucarrier'(X1) & 'net$ustr'(X1,X0)) => ! [X2] : (('is$ueventually$uin'(X0,X1,X2) <=> ? [X3] : ((element(X3,'the$ucarrier'(X1)) & ! [X4] : ((element(X4,'the$ucarrier'(X1)) => (related(X1,X3,X4) => in('apply$unetmap'(X0,X1,X4),X2))))))))))))).
% 44.04/10.85 fof(d12_waybel_0, axiom, ! [X0] : (((~'empty$ucarrier'(X0) & 'one$usorted$ustr'(X0)) => ! [X1] : (((~'empty$ucarrier'(X1) & 'net$ustr'(X1,X0)) => ! [X2] : (('is$uoften$uin'(X0,X1,X2) <=> ! [X3] : ((element(X3,'the$ucarrier'(X1)) => ? [X4] : ((element(X4,'the$ucarrier'(X1)) & (related(X1,X3,X4) & in('apply$unetmap'(X0,X1,X4),X2))))))))))))).
% 44.04/10.85 fof(d5_yellow_6, axiom, ! [X0] : (((~'empty$ucarrier'(X0) & 'rel$ustr'(X0)) => ('directed$urelstr'(X0) <=> ! [X1] : ((element(X1,'the$ucarrier'(X0)) => ! [X2] : ((element(X2,'the$ucarrier'(X0)) => ? [X3] : ((element(X3,'the$ucarrier'(X0)) & (related(X0,X1,X3) & related(X0,X2,X3)))))))))))).
% 44.04/10.85 fof(dt_l1_waybel_0, axiom, ! [X0] : (('one$usorted$ustr'(X0) => ! [X1] : (('net$ustr'(X1,X0) => 'rel$ustr'(X1)))))).
% 44.04/10.85 fof(t28_yellow_6, conjecture, ! [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)))))))).
% 44.04/10.85 fof(negated_conjecture, negated_conjecture, ~! [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))))))), inference(negate_conjecture, [status(cth)], [t28_yellow_6])).
% 44.04/10.85 cnf(c9, plain, X0(X1,X2,X3) | ~'is$ueventually$uin'(X1,X2,X3) | 'empty$ucarrier'(X1) | ~'net$ustr'(X2,X1) | 'empty$ucarrier'(X2) | ~'one$usorted$ustr'(X1), inference(clausification, [status(esa)], [d11_waybel_0])).
% 44.04/10.85 cnf(c11, plain, ~X0(X1,X2,X3) | element(sK14(X1,X2,X3),'the$ucarrier'(X2)), inference(clausification, [status(esa)], [d11_waybel_0])).
% 44.04/10.85 cnf(c12, plain, ~X0(X1,X2,X3) | ~element(X4,'the$ucarrier'(X2)) | ~related(X2,sK14(X1,X2,X3),X4) | in('apply$unetmap'(X1,X2,X4),X3), inference(clausification, [status(esa)], [d11_waybel_0])).
% 44.04/10.85 cnf(c17, plain, 'is$uoften$uin'(X0,X1,X2) | ~'net$ustr'(X1,X0) | 'empty$ucarrier'(X0) | ~'one$usorted$ustr'(X0) | ~X3(X0,X1,X2) | 'empty$ucarrier'(X1), inference(clausification, [status(esa)], [d12_waybel_0])).
% 44.04/10.85 cnf(c21, plain, X0(X1,X2,X3) | element(sK24(X1,X2,X3),'the$ucarrier'(X2)), inference(clausification, [status(esa)], [d12_waybel_0])).
% 44.04/10.85 cnf(c22, plain, X0(X1,X2,X3) | ~element(X4,'the$ucarrier'(X2)) | ~related(X2,sK24(X1,X2,X3),X4) | ~in('apply$unetmap'(X1,X2,X4),X3), inference(clausification, [status(esa)], [d12_waybel_0])).
% 44.04/10.85 cnf(c23, plain, 'empty$ucarrier'(X0) | ~'rel$ustr'(X0) | ~'directed$urelstr'(X0) | X1(X0), inference(clausification, [status(esa)], [d5_yellow_6])).
% 44.04/10.85 cnf(c25, plain, ~X0(X1) | ~element(X2,'the$ucarrier'(X1)) | ~element(X3,'the$ucarrier'(X1)) | element(sK30(X1,X2,X3),'the$ucarrier'(X1)), inference(clausification, [status(esa)], [d5_yellow_6])).
% 44.04/10.85 cnf(c26, plain, ~X0(X1) | ~element(X2,'the$ucarrier'(X1)) | ~element(X3,'the$ucarrier'(X1)) | related(X1,X2,sK30(X1,X2,X3)), inference(clausification, [status(esa)], [d5_yellow_6])).
% 44.04/10.85 cnf(c27, plain, ~X0(X1) | ~element(X2,'the$ucarrier'(X1)) | ~element(X3,'the$ucarrier'(X1)) | related(X1,X3,sK30(X1,X2,X3)), inference(clausification, [status(esa)], [d5_yellow_6])).
% 44.04/10.85 cnf(c35, plain, ~'one$usorted$ustr'(X0) | ~'net$ustr'(X1,X0) | 'rel$ustr'(X1), inference(clausification, [status(esa)], [dt_l1_waybel_0])).
% 44.04/10.85 cnf(c99, plain, ~'empty$ucarrier'(sK111), inference(clausification, [status(esa)], [negated_conjecture])).
% 44.04/10.85 cnf(c100, plain, 'one$usorted$ustr'(sK111), inference(clausification, [status(esa)], [negated_conjecture])).
% 44.04/10.85 cnf(c101, plain, ~'empty$ucarrier'(sK112), inference(clausification, [status(esa)], [negated_conjecture])).
% 44.04/10.85 cnf(c103, plain, 'directed$urelstr'(sK112), inference(clausification, [status(esa)], [negated_conjecture])).
% 44.04/10.85 cnf(c104, plain, 'net$ustr'(sK112,sK111), inference(clausification, [status(esa)], [negated_conjecture])).
% 44.04/10.85 cnf(c105, plain, 'is$ueventually$uin'(sK111,sK112,sK113), inference(clausification, [status(esa)], [negated_conjecture])).
% 44.04/10.85 cnf(c106, plain, ~'is$uoften$uin'(sK111,sK112,sK113), inference(clausification, [status(esa)], [negated_conjecture])).
% 44.04/10.85 cnf(d0, plain, 'empty$ucarrier'(sK111) | 'empty$ucarrier'(sK112) | ~'net$ustr'(sK112,sK111) | ~'one$usorted$ustr'(sK111) | 'Ts10'(sK111,sK112,sK113), inference(resolution, [status(thm)], [c9,c105])).
% 44.04/10.85 cnf(d1, plain, 'empty$ucarrier'(sK112) | ~'net$ustr'(sK112,sK111) | ~'one$usorted$ustr'(sK111) | 'Ts10'(sK111,sK112,sK113), inference(resolution, [status(thm)], [c99,d0])).
% 44.04/10.85 cnf(d2, plain, 'empty$ucarrier'(sK112) | ~'net$ustr'(sK112,sK111) | 'Ts10'(sK111,sK112,sK113), inference(resolution, [status(thm)], [c100,d1])).
% 44.04/10.85 cnf(d3, plain, ~'net$ustr'(sK112,sK111) | 'Ts10'(sK111,sK112,sK113), inference(resolution, [status(thm)], [c101,d2])).
% 44.04/10.85 cnf(d4, plain, 'Ts10'(sK111,sK112,sK113), inference(resolution, [status(thm)], [c104,d3])).
% 44.04/10.85 cnf(d5, plain, ~element(sK14(X0,X1,X2),'the$ucarrier'(X1)) | ~element(X3,'the$ucarrier'(X1)) | ~'Ts26'(X1) | in('apply$unetmap'(X0,X1,sK30(X1,sK14(X0,X1,X2),X3)),X2) | ~element(sK30(X1,sK14(X0,X1,X2),X3),'the$ucarrier'(X1)) | ~'Ts10'(X0,X1,X2), inference(resolution, [status(thm)], [c26,c12])).
% 44.04/10.85 cnf(d6, plain, ~'Ts10'(X0,X1,X2) | in('apply$unetmap'(X0,X1,sK30(X1,sK14(X0,X1,X2),X3)),X2) | ~element(X3,'the$ucarrier'(X1)) | ~element(sK30(X1,sK14(X0,X1,X2),X3),'the$ucarrier'(X1)) | ~'Ts10'(X0,X1,X2) | ~'Ts26'(X1), inference(resolution, [status(thm)], [c11,d5])).
% 44.04/10.85 cnf(d7, plain, ~element(X0,'the$ucarrier'(X1)) | ~element(sK24(X2,X1,X3),'the$ucarrier'(X1)) | ~'Ts26'(X1) | ~in('apply$unetmap'(X2,X1,sK30(X1,X0,sK24(X2,X1,X3))),X3) | ~element(sK30(X1,X0,sK24(X2,X1,X3)),'the$ucarrier'(X1)) | 'Ts18'(X2,X1,X3), inference(resolution, [status(thm)], [c27,c22])).
% 44.04/10.85 cnf(d8, plain, 'Ts18'(X0,X1,X2) | ~in('apply$unetmap'(X0,X1,sK30(X1,X3,sK24(X0,X1,X2))),X2) | ~element(X3,'the$ucarrier'(X1)) | ~element(sK30(X1,X3,sK24(X0,X1,X2)),'the$ucarrier'(X1)) | 'Ts18'(X0,X1,X2) | ~'Ts26'(X1), inference(resolution, [status(thm)], [c21,d7])).
% 44.04/10.85 cnf(d9, plain, ~element(sK14(X0,X1,X2),'the$ucarrier'(X1)) | ~element(sK30(X1,sK14(X0,X1,X2),sK24(X0,X1,X2)),'the$ucarrier'(X1)) | 'Ts18'(X0,X1,X2) | ~'Ts26'(X1) | ~element(sK24(X0,X1,X2),'the$ucarrier'(X1)) | ~element(sK30(X1,sK14(X0,X1,X2),sK24(X0,X1,X2)),'the$ucarrier'(X1)) | ~'Ts10'(X0,X1,X2) | ~'Ts26'(X1), inference(resolution, [status(thm)], [d8,d6])).
% 44.04/10.85 cnf(d10, plain, ~'Ts10'(X0,X1,X2) | ~element(sK24(X0,X1,X2),'the$ucarrier'(X1)) | ~element(sK30(X1,sK14(X0,X1,X2),sK24(X0,X1,X2)),'the$ucarrier'(X1)) | ~'Ts10'(X0,X1,X2) | 'Ts18'(X0,X1,X2) | ~'Ts26'(X1), inference(resolution, [status(thm)], [c11,d9])).
% 44.04/10.85 cnf(d11, plain, 'Ts18'(X0,X1,X2) | ~element(sK30(X1,sK14(X0,X1,X2),sK24(X0,X1,X2)),'the$ucarrier'(X1)) | ~'Ts10'(X0,X1,X2) | 'Ts18'(X0,X1,X2) | ~'Ts26'(X1), inference(resolution, [status(thm)], [c21,d10])).
% 44.04/10.85 cnf(d12, plain, ~'Ts10'(X0,X1,X2) | 'Ts18'(X0,X1,X2) | ~'Ts26'(X1) | ~element(sK14(X0,X1,X2),'the$ucarrier'(X1)) | ~element(sK24(X0,X1,X2),'the$ucarrier'(X1)) | ~'Ts26'(X1), inference(resolution, [status(thm)], [d11,c25])).
% 44.04/10.85 cnf(d13, plain, ~'Ts10'(X0,X1,X2) | ~element(sK24(X0,X1,X2),'the$ucarrier'(X1)) | ~'Ts10'(X0,X1,X2) | 'Ts18'(X0,X1,X2) | ~'Ts26'(X1), inference(resolution, [status(thm)], [c11,d12])).
% 44.04/10.85 cnf(d14, plain, 'Ts18'(X0,X1,X2) | ~'Ts10'(X0,X1,X2) | 'Ts18'(X0,X1,X2) | ~'Ts26'(X1), inference(resolution, [status(thm)], [c21,d13])).
% 44.04/10.85 cnf(d15, plain, 'Ts18'(sK111,sK112,sK113) | ~'Ts26'(sK112), inference(resolution, [status(thm)], [d14,d4])).
% 44.04/10.85 cnf(d16, plain, 'empty$ucarrier'(sK112) | ~'rel$ustr'(sK112) | 'Ts26'(sK112), inference(resolution, [status(thm)], [c23,c103])).
% 44.04/10.85 cnf(d17, plain, ~'rel$ustr'(sK112) | 'Ts26'(sK112), inference(resolution, [status(thm)], [c101,d16])).
% 44.04/10.85 cnf(d18, plain, 'rel$ustr'(sK112) | ~'one$usorted$ustr'(sK111), inference(resolution, [status(thm)], [c35,c104])).
% 44.04/10.85 cnf(d19, plain, 'rel$ustr'(sK112), inference(resolution, [status(thm)], [c100,d18])).
% 44.04/10.85 cnf(d20, plain, 'Ts26'(sK112), inference(resolution, [status(thm)], [d19,d17])).
% 44.04/10.85 cnf(d21, plain, 'Ts18'(sK111,sK112,sK113), inference(resolution, [status(thm)], [d20,d15])).
% 44.04/10.85 cnf(d22, plain, 'empty$ucarrier'(sK112) | 'empty$ucarrier'(sK111) | ~'net$ustr'(sK112,sK111) | ~'one$usorted$ustr'(sK111) | 'is$uoften$uin'(sK111,sK112,sK113), inference(resolution, [status(thm)], [d21,c17])).
% 44.04/10.85 cnf(d23, plain, 'empty$ucarrier'(sK112) | ~'net$ustr'(sK112,sK111) | ~'one$usorted$ustr'(sK111) | 'is$uoften$uin'(sK111,sK112,sK113), inference(resolution, [status(thm)], [c99,d22])).
% 44.04/10.85 cnf(d24, plain, 'empty$ucarrier'(sK112) | ~'net$ustr'(sK112,sK111) | 'is$uoften$uin'(sK111,sK112,sK113), inference(resolution, [status(thm)], [c100,d23])).
% 44.04/10.85 cnf(d25, plain, ~'net$ustr'(sK112,sK111) | 'is$uoften$uin'(sK111,sK112,sK113), inference(resolution, [status(thm)], [c101,d24])).
% 44.04/10.85 cnf(d26, plain, 'is$uoften$uin'(sK111,sK112,sK113), inference(resolution, [status(thm)], [c104,d25])).
% 44.04/10.85 cnf(d27, plain, $false, inference(resolution, [status(thm)], [c106,d26])).
% 44.04/10.85 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------