%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU240+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 : n016.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:24 AM UTC 2026
% Result : Theorem 12.04s 28.45s
% Output : CNFRefutation 12.04s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU240+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.09/5.38 % Computer : n016.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/25.43 % CPULimit : 300
% 0.10/25.43 % WCLimit : 300
% 0.10/25.43 % DateTime : Sat Sep 26 08:58:16 UTC 2026
% 0.10/25.44 % CPUTime :
% 0.10/25.44 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.04/28.45 % SZS status Theorem for theBenchmark.p
% 12.04/28.45 % SZS output start CNFRefutation for theBenchmark.p
% 12.04/28.45 fof(d16_relat_2, axiom, ! [X0] : ((relation(X0) => (transitive(X0) <=> 'is$utransitive$uin'(X0,'relation$ufield'(X0)))))).
% 12.04/28.45 fof(d8_relat_2, axiom, ! [X0] : ((relation(X0) => ! [X1] : (('is$utransitive$uin'(X0,X1) <=> ! [X2] : ! [X3] : ! [X4] : (((in(X2,X1) & (in(X3,X1) & (in(X4,X1) & (in('ordered$upair'(X2,X3),X0) & in('ordered$upair'(X3,X4),X0))))) => in('ordered$upair'(X2,X4),X0)))))))).
% 12.04/28.45 fof(t30_relat_1, axiom, ! [X0] : ! [X1] : ! [X2] : ((relation(X2) => (in('ordered$upair'(X0,X1),X2) => (in(X0,'relation$ufield'(X2)) & in(X1,'relation$ufield'(X2))))))).
% 12.04/28.45 fof(l2_wellord1, conjecture, ! [X0] : ((relation(X0) => (transitive(X0) <=> ! [X1] : ! [X2] : ! [X3] : (((in('ordered$upair'(X1,X2),X0) & in('ordered$upair'(X2,X3),X0)) => in('ordered$upair'(X1,X3),X0))))))).
% 12.04/28.45 fof(negated_conjecture, negated_conjecture, ~! [X0] : ((relation(X0) => (transitive(X0) <=> ! [X1] : ! [X2] : ! [X3] : (((in('ordered$upair'(X1,X2),X0) & in('ordered$upair'(X2,X3),X0)) => in('ordered$upair'(X1,X3),X0)))))), inference(negate_conjecture, [status(cth)], [l2_wellord1])).
% 12.04/28.45 cnf(c7, plain, ~relation(X0) | ~transitive(X0) | 'is$utransitive$uin'(X0,'relation$ufield'(X0)), inference(clausification, [status(esa)], [d16_relat_2])).
% 12.04/28.45 cnf(c8, plain, ~relation(X0) | transitive(X0) | ~'is$utransitive$uin'(X0,'relation$ufield'(X0)), inference(clausification, [status(esa)], [d16_relat_2])).
% 12.04/28.45 cnf(c11, plain, ~relation(X0) | ~'is$utransitive$uin'(X0,X1) | X2(X0,X1), inference(clausification, [status(esa)], [d8_relat_2])).
% 12.04/28.45 cnf(c12, plain, ~relation(X0) | 'is$utransitive$uin'(X0,X1) | ~X2(X0,X1), inference(clausification, [status(esa)], [d8_relat_2])).
% 12.04/28.45 cnf(c13, plain, ~in('ordered$upair'(X0,X1),X2) | in('ordered$upair'(X0,X3),X2) | ~in(X3,X4) | ~in('ordered$upair'(X1,X3),X2) | ~in(X0,X4) | ~in(X1,X4) | ~X5(X2,X4), inference(clausification, [status(esa)], [d8_relat_2])).
% 12.04/28.45 cnf(c17, plain, X0(X1,X2) | in('ordered$upair'(sK18(X1,X2),sK19(X1,X2)),X1), inference(clausification, [status(esa)], [d8_relat_2])).
% 12.04/28.45 cnf(c18, plain, X0(X1,X2) | in('ordered$upair'(sK19(X1,X2),sK20(X1,X2)),X1), inference(clausification, [status(esa)], [d8_relat_2])).
% 12.04/28.45 cnf(c19, plain, X0(X1,X2) | ~in('ordered$upair'(sK18(X1,X2),sK20(X1,X2)),X1), inference(clausification, [status(esa)], [d8_relat_2])).
% 12.04/28.45 cnf(c39, plain, ~relation(X0) | ~in('ordered$upair'(X1,X2),X0) | in(X1,'relation$ufield'(X0)), inference(clausification, [status(esa)], [t30_relat_1])).
% 12.04/28.45 cnf(c40, plain, ~relation(X0) | ~in('ordered$upair'(X1,X2),X0) | in(X2,'relation$ufield'(X0)), inference(clausification, [status(esa)], [t30_relat_1])).
% 12.04/28.45 cnf(c44, plain, relation(sK49), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.04/28.45 cnf(c46, plain, transitive(sK49) | ~in('ordered$upair'(X0,X1),sK49) | ~in('ordered$upair'(X1,X2),sK49) | in('ordered$upair'(X0,X2),sK49), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.04/28.45 cnf(c47, plain, in('ordered$upair'(sK50,sK51),sK49) | ~transitive(sK49), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.04/28.45 cnf(c49, plain, in('ordered$upair'(sK51,sK52),sK49) | ~transitive(sK49), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.04/28.45 cnf(c51, plain, ~in('ordered$upair'(sK50,sK52),sK49) | ~transitive(sK49), inference(clausification, [status(esa)], [negated_conjecture])).
% 12.04/28.45 cnf(d0, plain, ~relation(X0) | 'Ts12'(X0,'relation$ufield'(X0)) | ~relation(X0) | ~transitive(X0), inference(resolution, [status(thm)], [c11,c7])).
% 12.04/28.45 cnf(d1, plain, 'Ts12'(sK49,X0) | ~in('ordered$upair'(sK19(sK49,X0),X1),sK49) | in('ordered$upair'(sK18(sK49,X0),X1),sK49) | transitive(sK49), inference(resolution, [status(thm)], [c17,c46])).
% 12.04/28.45 cnf(d2, plain, 'Ts12'(sK49,X0) | in('ordered$upair'(sK18(sK49,X0),sK20(sK49,X0)),sK49) | transitive(sK49) | 'Ts12'(sK49,X0), inference(resolution, [status(thm)], [c18,d1])).
% 12.04/28.45 cnf(d3, plain, 'Ts12'(sK49,X0) | transitive(sK49) | 'Ts12'(sK49,X0), inference(resolution, [status(thm)], [c19,d2])).
% 12.04/28.45 cnf(d4, plain, transitive(sK49) | ~relation(sK49) | 'is$utransitive$uin'(sK49,X0), inference(resolution, [status(thm)], [d3,c12])).
% 12.04/28.45 cnf(d5, plain, transitive(sK49) | 'is$utransitive$uin'(sK49,X0), inference(resolution, [status(thm)], [c44,d4])).
% 12.04/28.45 cnf(d6, plain, transitive(sK49) | ~relation(sK49) | transitive(sK49), inference(resolution, [status(thm)], [d5,c8])).
% 12.04/28.45 cnf(d7, plain, transitive(sK49), inference(resolution, [status(thm)], [c44,d6])).
% 12.04/28.45 cnf(d8, plain, in('ordered$upair'(sK51,sK52),sK49), inference(resolution, [status(thm)], [d7,c49])).
% 12.04/28.45 cnf(d9, plain, ~in(X0,X1) | ~in(sK51,X1) | ~in(sK50,X1) | ~in('ordered$upair'(sK51,X0),sK49) | in('ordered$upair'(sK50,X0),sK49) | ~'Ts12'(sK49,X1) | ~transitive(sK49), inference(resolution, [status(thm)], [c13,c47])).
% 12.04/28.45 cnf(d10, plain, ~in(X0,X1) | in('ordered$upair'(sK50,X0),sK49) | ~in('ordered$upair'(sK51,X0),sK49) | ~in(sK50,X1) | ~in(sK51,X1) | ~'Ts12'(sK49,X1), inference(resolution, [status(thm)], [d7,d9])).
% 12.04/28.45 cnf(d11, plain, ~in(sK52,X0) | in('ordered$upair'(sK50,sK52),sK49) | ~in(sK50,X0) | ~in(sK51,X0) | ~'Ts12'(sK49,X0), inference(resolution, [status(thm)], [d10,d8])).
% 12.04/28.45 cnf(d12, plain, ~in('ordered$upair'(sK50,sK52),sK49), inference(resolution, [status(thm)], [d7,c51])).
% 12.04/28.45 cnf(d13, plain, ~in(sK50,X0) | ~in(sK51,X0) | ~in(sK52,X0) | ~'Ts12'(sK49,X0), inference(resolution, [status(thm)], [d12,d11])).
% 12.04/28.45 cnf(d14, plain, ~in(sK50,'relation$ufield'(sK49)) | ~in(sK51,'relation$ufield'(sK49)) | ~in(sK52,'relation$ufield'(sK49)) | ~relation(sK49) | ~transitive(sK49), inference(resolution, [status(thm)], [d13,d0])).
% 12.04/28.45 cnf(d15, plain, ~in(sK50,'relation$ufield'(sK49)) | ~in(sK51,'relation$ufield'(sK49)) | ~in(sK52,'relation$ufield'(sK49)) | ~transitive(sK49), inference(resolution, [status(thm)], [c44,d14])).
% 12.04/28.45 cnf(d16, plain, ~in(sK50,'relation$ufield'(sK49)) | ~in(sK51,'relation$ufield'(sK49)) | ~in(sK52,'relation$ufield'(sK49)), inference(resolution, [status(thm)], [d7,d15])).
% 12.04/28.45 cnf(d17, plain, in(sK51,'relation$ufield'(sK49)) | ~relation(sK49), inference(resolution, [status(thm)], [c39,d8])).
% 12.04/28.45 cnf(d18, plain, in(sK51,'relation$ufield'(sK49)), inference(resolution, [status(thm)], [c44,d17])).
% 12.04/28.45 cnf(d19, plain, ~in(sK50,'relation$ufield'(sK49)) | ~in(sK52,'relation$ufield'(sK49)), inference(resolution, [status(thm)], [d18,d16])).
% 12.04/28.45 cnf(d20, plain, in('ordered$upair'(sK50,sK51),sK49), inference(resolution, [status(thm)], [d7,c47])).
% 12.04/28.45 cnf(d21, plain, in(sK50,'relation$ufield'(sK49)) | ~relation(sK49), inference(resolution, [status(thm)], [c39,d20])).
% 12.04/28.45 cnf(d22, plain, in(sK50,'relation$ufield'(sK49)), inference(resolution, [status(thm)], [c44,d21])).
% 12.04/28.45 cnf(d23, plain, ~in(sK52,'relation$ufield'(sK49)), inference(resolution, [status(thm)], [d22,d19])).
% 12.04/28.45 cnf(d24, plain, in(sK52,'relation$ufield'(sK49)) | ~relation(sK49), inference(resolution, [status(thm)], [c40,d8])).
% 12.04/28.45 cnf(d25, plain, in(sK52,'relation$ufield'(sK49)), inference(resolution, [status(thm)], [c44,d24])).
% 12.04/28.45 cnf(d26, plain, $false, inference(resolution, [status(thm)], [d25,d23])).
% 12.04/28.45 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------