%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU244+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:25 AM UTC 2026
% Result : Theorem 15.90s 2.45s
% Output : CNFRefutation 15.90s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU244+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n019.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sat Sep 26 08:58:19 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.90/2.45 % SZS status Theorem for theBenchmark.p
% 15.90/2.45 % SZS output start CNFRefutation for theBenchmark.p
% 15.90/2.45 fof(d12_relat_2, axiom, ! [X0] : ((relation(X0) => (antisymmetric(X0) <=> 'is$uantisymmetric$uin'(X0,'relation$ufield'(X0)))))).
% 15.90/2.45 fof(d14_relat_2, axiom, ! [X0] : ((relation(X0) => (connected(X0) <=> 'is$uconnected$uin'(X0,'relation$ufield'(X0)))))).
% 15.90/2.45 fof(d16_relat_2, axiom, ! [X0] : ((relation(X0) => (transitive(X0) <=> 'is$utransitive$uin'(X0,'relation$ufield'(X0)))))).
% 15.90/2.45 fof(d4_wellord1, axiom, ! [X0] : ((relation(X0) => ('well$uordering'(X0) <=> (reflexive(X0) & (transitive(X0) & (antisymmetric(X0) & (connected(X0) & 'well$ufounded$urelation'(X0))))))))).
% 15.90/2.45 fof(d5_wellord1, axiom, ! [X0] : ((relation(X0) => ! [X1] : (('well$uorders'(X0,X1) <=> ('is$ureflexive$uin'(X0,X1) & ('is$utransitive$uin'(X0,X1) & ('is$uantisymmetric$uin'(X0,X1) & ('is$uconnected$uin'(X0,X1) & 'is$uwell$ufounded$uin'(X0,X1)))))))))).
% 15.90/2.45 fof(d9_relat_2, axiom, ! [X0] : ((relation(X0) => (reflexive(X0) <=> 'is$ureflexive$uin'(X0,'relation$ufield'(X0)))))).
% 15.90/2.45 fof(t5_wellord1, axiom, ! [X0] : ((relation(X0) => ('well$ufounded$urelation'(X0) <=> 'is$uwell$ufounded$uin'(X0,'relation$ufield'(X0)))))).
% 15.90/2.45 fof(t8_wellord1, conjecture, ! [X0] : ((relation(X0) => ('well$uorders'(X0,'relation$ufield'(X0)) <=> 'well$uordering'(X0))))).
% 15.90/2.45 fof(negated_conjecture, negated_conjecture, ~! [X0] : ((relation(X0) => ('well$uorders'(X0,'relation$ufield'(X0)) <=> 'well$uordering'(X0)))), inference(negate_conjecture, [status(cth)], [t8_wellord1])).
% 15.90/2.45 cnf(c1, plain, ~relation(X0) | ~antisymmetric(X0) | 'is$uantisymmetric$uin'(X0,'relation$ufield'(X0)), inference(clausification, [status(esa)], [d12_relat_2])).
% 15.90/2.45 cnf(c2, plain, ~relation(X0) | antisymmetric(X0) | ~'is$uantisymmetric$uin'(X0,'relation$ufield'(X0)), inference(clausification, [status(esa)], [d12_relat_2])).
% 15.90/2.45 cnf(c3, plain, ~relation(X0) | ~connected(X0) | 'is$uconnected$uin'(X0,'relation$ufield'(X0)), inference(clausification, [status(esa)], [d14_relat_2])).
% 15.90/2.45 cnf(c4, plain, ~relation(X0) | connected(X0) | ~'is$uconnected$uin'(X0,'relation$ufield'(X0)), inference(clausification, [status(esa)], [d14_relat_2])).
% 15.90/2.45 cnf(c5, plain, ~relation(X0) | ~transitive(X0) | 'is$utransitive$uin'(X0,'relation$ufield'(X0)), inference(clausification, [status(esa)], [d16_relat_2])).
% 15.90/2.45 cnf(c6, plain, ~relation(X0) | transitive(X0) | ~'is$utransitive$uin'(X0,'relation$ufield'(X0)), inference(clausification, [status(esa)], [d16_relat_2])).
% 15.90/2.45 cnf(c7, plain, ~relation(X0) | ~'well$uordering'(X0) | X1(X0), inference(clausification, [status(esa)], [d4_wellord1])).
% 15.90/2.45 cnf(c8, plain, ~relation(X0) | 'well$uordering'(X0) | ~X1(X0), inference(clausification, [status(esa)], [d4_wellord1])).
% 15.90/2.45 cnf(c9, plain, ~X0(X1) | reflexive(X1), inference(clausification, [status(esa)], [d4_wellord1])).
% 15.90/2.45 cnf(c10, plain, ~X0(X1) | transitive(X1), inference(clausification, [status(esa)], [d4_wellord1])).
% 15.90/2.45 cnf(c11, plain, ~X0(X1) | antisymmetric(X1), inference(clausification, [status(esa)], [d4_wellord1])).
% 15.90/2.45 cnf(c12, plain, ~X0(X1) | connected(X1), inference(clausification, [status(esa)], [d4_wellord1])).
% 15.90/2.45 cnf(c13, plain, ~X0(X1) | 'well$ufounded$urelation'(X1), inference(clausification, [status(esa)], [d4_wellord1])).
% 15.90/2.45 cnf(c14, plain, ~'well$ufounded$urelation'(X0) | X1(X0) | ~connected(X0) | ~antisymmetric(X0) | ~transitive(X0) | ~reflexive(X0), inference(clausification, [status(esa)], [d4_wellord1])).
% 15.90/2.45 cnf(c15, plain, ~relation(X0) | ~'well$uorders'(X0,X1) | X2(X0,X1), inference(clausification, [status(esa)], [d5_wellord1])).
% 15.90/2.45 cnf(c16, plain, ~relation(X0) | 'well$uorders'(X0,X1) | ~X2(X0,X1), inference(clausification, [status(esa)], [d5_wellord1])).
% 15.90/2.45 cnf(c17, plain, ~X0(X1,X2) | 'is$ureflexive$uin'(X1,X2), inference(clausification, [status(esa)], [d5_wellord1])).
% 15.90/2.45 cnf(c18, plain, ~X0(X1,X2) | 'is$utransitive$uin'(X1,X2), inference(clausification, [status(esa)], [d5_wellord1])).
% 15.90/2.45 cnf(c19, plain, ~X0(X1,X2) | 'is$uantisymmetric$uin'(X1,X2), inference(clausification, [status(esa)], [d5_wellord1])).
% 15.90/2.45 cnf(c20, plain, ~X0(X1,X2) | 'is$uconnected$uin'(X1,X2), inference(clausification, [status(esa)], [d5_wellord1])).
% 15.90/2.45 cnf(c21, plain, ~X0(X1,X2) | 'is$uwell$ufounded$uin'(X1,X2), inference(clausification, [status(esa)], [d5_wellord1])).
% 15.90/2.45 cnf(c22, plain, ~'is$uconnected$uin'(X0,X1) | X2(X0,X1) | ~'is$uwell$ufounded$uin'(X0,X1) | ~'is$ureflexive$uin'(X0,X1) | ~'is$uantisymmetric$uin'(X0,X1) | ~'is$utransitive$uin'(X0,X1), inference(clausification, [status(esa)], [d5_wellord1])).
% 15.90/2.45 cnf(c24, plain, ~relation(X0) | ~reflexive(X0) | 'is$ureflexive$uin'(X0,'relation$ufield'(X0)), inference(clausification, [status(esa)], [d9_relat_2])).
% 15.90/2.45 cnf(c25, plain, ~relation(X0) | reflexive(X0) | ~'is$ureflexive$uin'(X0,'relation$ufield'(X0)), inference(clausification, [status(esa)], [d9_relat_2])).
% 15.90/2.45 cnf(c27, plain, ~relation(X0) | ~'well$ufounded$urelation'(X0) | 'is$uwell$ufounded$uin'(X0,'relation$ufield'(X0)), inference(clausification, [status(esa)], [t5_wellord1])).
% 15.90/2.45 cnf(c28, plain, ~relation(X0) | 'well$ufounded$urelation'(X0) | ~'is$uwell$ufounded$uin'(X0,'relation$ufield'(X0)), inference(clausification, [status(esa)], [t5_wellord1])).
% 15.90/2.45 cnf(c29, plain, relation(sK15), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.90/2.45 cnf(c31, plain, 'well$uorders'(sK15,'relation$ufield'(sK15)) | 'well$uordering'(sK15), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.90/2.45 cnf(c32, plain, ~'well$uordering'(sK15) | ~'well$uorders'(sK15,'relation$ufield'(sK15)), inference(clausification, [status(esa)], [negated_conjecture])).
% 15.90/2.45 cnf(d0, plain, ~relation(sK15) | 'Ts7'(sK15,'relation$ufield'(sK15)) | 'well$uordering'(sK15), inference(resolution, [status(thm)], [c15,c31])).
% 15.90/2.45 cnf(d1, plain, 'well$uordering'(sK15) | 'Ts7'(sK15,'relation$ufield'(sK15)), inference(resolution, [status(thm)], [c29,d0])).
% 15.90/2.45 cnf(d2, plain, 'is$uantisymmetric$uin'(sK15,'relation$ufield'(sK15)) | 'well$uordering'(sK15), inference(resolution, [status(thm)], [c19,d1])).
% 15.90/2.45 cnf(d3, plain, 'well$uordering'(sK15) | ~relation(sK15) | antisymmetric(sK15), inference(resolution, [status(thm)], [d2,c2])).
% 15.90/2.45 cnf(d4, plain, antisymmetric(sK15) | 'well$uordering'(sK15), inference(resolution, [status(thm)], [c29,d3])).
% 15.90/2.45 cnf(d5, plain, 'is$uconnected$uin'(sK15,'relation$ufield'(sK15)) | 'well$uordering'(sK15), inference(resolution, [status(thm)], [c20,d1])).
% 15.90/2.45 cnf(d6, plain, 'well$uordering'(sK15) | ~relation(sK15) | connected(sK15), inference(resolution, [status(thm)], [d5,c4])).
% 15.90/2.45 cnf(d7, plain, connected(sK15) | 'well$uordering'(sK15), inference(resolution, [status(thm)], [c29,d6])).
% 15.90/2.45 cnf(d8, plain, 'is$utransitive$uin'(sK15,'relation$ufield'(sK15)) | 'well$uordering'(sK15), inference(resolution, [status(thm)], [c18,d1])).
% 15.90/2.45 cnf(d9, plain, 'well$uordering'(sK15) | ~relation(sK15) | transitive(sK15), inference(resolution, [status(thm)], [d8,c6])).
% 15.90/2.45 cnf(d10, plain, transitive(sK15) | 'well$uordering'(sK15), inference(resolution, [status(thm)], [c29,d9])).
% 15.90/2.45 cnf(d11, plain, 'is$ureflexive$uin'(sK15,'relation$ufield'(sK15)) | 'well$uordering'(sK15), inference(resolution, [status(thm)], [c17,d1])).
% 15.90/2.45 cnf(d12, plain, ~relation(sK15) | reflexive(sK15) | 'well$uordering'(sK15), inference(resolution, [status(thm)], [c25,d11])).
% 15.90/2.45 cnf(d13, plain, 'well$uordering'(sK15) | reflexive(sK15), inference(resolution, [status(thm)], [c29,d12])).
% 15.90/2.45 cnf(d14, plain, 'is$uwell$ufounded$uin'(sK15,'relation$ufield'(sK15)) | 'well$uordering'(sK15), inference(resolution, [status(thm)], [c21,d1])).
% 15.90/2.45 cnf(d15, plain, ~relation(sK15) | 'well$ufounded$urelation'(sK15) | 'well$uordering'(sK15), inference(resolution, [status(thm)], [c28,d14])).
% 15.90/2.45 cnf(d16, plain, 'well$uordering'(sK15) | 'well$ufounded$urelation'(sK15), inference(resolution, [status(thm)], [c29,d15])).
% 15.90/2.45 cnf(d17, plain, 'well$uordering'(sK15) | ~antisymmetric(sK15) | ~connected(sK15) | ~transitive(sK15) | 'Ts5'(sK15) | ~reflexive(sK15), inference(resolution, [status(thm)], [d16,c14])).
% 15.90/2.45 cnf(d18, plain, ~antisymmetric(sK15) | ~connected(sK15) | ~transitive(sK15) | 'well$uordering'(sK15) | 'Ts5'(sK15) | 'well$uordering'(sK15), inference(resolution, [status(thm)], [d17,d13])).
% 15.90/2.45 cnf(d19, plain, ~antisymmetric(sK15) | ~connected(sK15) | 'well$uordering'(sK15) | 'Ts5'(sK15) | 'well$uordering'(sK15), inference(resolution, [status(thm)], [d18,d10])).
% 15.90/2.45 cnf(d20, plain, ~antisymmetric(sK15) | 'well$uordering'(sK15) | 'Ts5'(sK15) | 'well$uordering'(sK15), inference(resolution, [status(thm)], [d19,d7])).
% 15.90/2.45 cnf(d21, plain, 'well$uordering'(sK15) | 'Ts5'(sK15) | 'well$uordering'(sK15), inference(resolution, [status(thm)], [d20,d4])).
% 15.90/2.45 cnf(d22, plain, 'Ts5'(sK15) | ~relation(sK15) | 'Ts5'(sK15), inference(resolution, [status(thm)], [d21,c7])).
% 15.90/2.45 cnf(d23, plain, 'Ts5'(sK15), inference(resolution, [status(thm)], [c29,d22])).
% 15.90/2.45 cnf(d24, plain, ~relation(sK15) | 'well$uordering'(sK15), inference(resolution, [status(thm)], [d23,c8])).
% 15.90/2.45 cnf(d25, plain, 'well$uordering'(sK15), inference(resolution, [status(thm)], [c29,d24])).
% 15.90/2.45 cnf(d26, plain, ~'well$uorders'(sK15,'relation$ufield'(sK15)), inference(resolution, [status(thm)], [d25,c32])).
% 15.90/2.45 cnf(d27, plain, ~relation(X0) | ~'well$ufounded$urelation'(X0) | ~'is$uantisymmetric$uin'(X0,'relation$ufield'(X0)) | ~'is$uconnected$uin'(X0,'relation$ufield'(X0)) | ~'is$utransitive$uin'(X0,'relation$ufield'(X0)) | 'Ts7'(X0,'relation$ufield'(X0)) | ~'is$ureflexive$uin'(X0,'relation$ufield'(X0)), inference(resolution, [status(thm)], [c27,c22])).
% 15.90/2.45 cnf(d28, plain, ~relation(X0) | ~'is$uantisymmetric$uin'(X0,'relation$ufield'(X0)) | ~'is$uconnected$uin'(X0,'relation$ufield'(X0)) | ~'is$utransitive$uin'(X0,'relation$ufield'(X0)) | ~'well$ufounded$urelation'(X0) | 'Ts7'(X0,'relation$ufield'(X0)) | ~relation(X0) | ~reflexive(X0), inference(resolution, [status(thm)], [d27,c24])).
% 15.90/2.45 cnf(d29, plain, ~relation(X0) | ~'is$uantisymmetric$uin'(X0,'relation$ufield'(X0)) | ~'is$uconnected$uin'(X0,'relation$ufield'(X0)) | ~reflexive(X0) | ~'well$ufounded$urelation'(X0) | 'Ts7'(X0,'relation$ufield'(X0)) | ~relation(X0) | ~transitive(X0), inference(resolution, [status(thm)], [d28,c5])).
% 15.90/2.45 cnf(d30, plain, ~relation(X0) | ~'is$uantisymmetric$uin'(X0,'relation$ufield'(X0)) | ~transitive(X0) | ~reflexive(X0) | ~'well$ufounded$urelation'(X0) | 'Ts7'(X0,'relation$ufield'(X0)) | ~relation(X0) | ~connected(X0), inference(resolution, [status(thm)], [d29,c3])).
% 15.90/2.45 cnf(d31, plain, ~relation(X0) | ~connected(X0) | ~transitive(X0) | ~reflexive(X0) | ~'well$ufounded$urelation'(X0) | 'Ts7'(X0,'relation$ufield'(X0)) | ~relation(X0) | ~antisymmetric(X0), inference(resolution, [status(thm)], [d30,c1])).
% 15.90/2.45 cnf(d32, plain, ~relation(X0) | ~antisymmetric(X0) | ~connected(X0) | ~transitive(X0) | ~reflexive(X0) | ~'well$ufounded$urelation'(X0) | ~relation(X0) | 'well$uorders'(X0,'relation$ufield'(X0)), inference(resolution, [status(thm)], [d31,c16])).
% 15.90/2.45 cnf(d33, plain, ~relation(sK15) | ~antisymmetric(sK15) | ~connected(sK15) | ~transitive(sK15) | ~reflexive(sK15) | ~'well$ufounded$urelation'(sK15), inference(resolution, [status(thm)], [d32,d26])).
% 15.90/2.45 cnf(d34, plain, ~antisymmetric(sK15) | ~connected(sK15) | ~transitive(sK15) | ~reflexive(sK15) | ~'well$ufounded$urelation'(sK15), inference(resolution, [status(thm)], [c29,d33])).
% 15.90/2.45 cnf(d35, plain, 'well$ufounded$urelation'(sK15), inference(resolution, [status(thm)], [d23,c13])).
% 15.90/2.45 cnf(d36, plain, ~antisymmetric(sK15) | ~connected(sK15) | ~transitive(sK15) | ~reflexive(sK15), inference(resolution, [status(thm)], [d35,d34])).
% 15.90/2.45 cnf(d37, plain, transitive(sK15), inference(resolution, [status(thm)], [d23,c10])).
% 15.90/2.45 cnf(d38, plain, ~antisymmetric(sK15) | ~connected(sK15) | ~reflexive(sK15), inference(resolution, [status(thm)], [d37,d36])).
% 15.90/2.45 cnf(d39, plain, antisymmetric(sK15), inference(resolution, [status(thm)], [d23,c11])).
% 15.90/2.45 cnf(d40, plain, ~connected(sK15) | ~reflexive(sK15), inference(resolution, [status(thm)], [d39,d38])).
% 15.90/2.45 cnf(d41, plain, connected(sK15), inference(resolution, [status(thm)], [d23,c12])).
% 15.90/2.45 cnf(d42, plain, ~reflexive(sK15), inference(resolution, [status(thm)], [d41,d40])).
% 15.90/2.45 cnf(d43, plain, reflexive(sK15), inference(resolution, [status(thm)], [d23,c9])).
% 15.90/2.45 cnf(d44, plain, $false, inference(resolution, [status(thm)], [d43,d42])).
% 15.90/2.45 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------