%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU243+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 : n013.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 13.37s 2.62s
% Output : CNFRefutation 13.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU243+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n013.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 08:57:21 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.37/2.62 % SZS status Theorem for theBenchmark.p
% 13.37/2.62 % SZS output start CNFRefutation for theBenchmark.p
% 13.37/2.62 fof(d2_wellord1, axiom, ! [X0] : ((relation(X0) => ('well$ufounded$urelation'(X0) <=> ! [X1] : ~((subset(X1,'relation$ufield'(X0)) & (X1 != 'empty$uset' & ! [X2] : ~((in(X2,X1) & disjoint(fiber(X0,X2),X1)))))))))).
% 13.37/2.62 fof(d3_wellord1, axiom, ! [X0] : ((relation(X0) => ! [X1] : (('is$uwell$ufounded$uin'(X0,X1) <=> ! [X2] : ~((subset(X2,X1) & (X2 != 'empty$uset' & ! [X3] : ~((in(X3,X2) & disjoint(fiber(X0,X3),X2))))))))))).
% 13.37/2.62 fof(t5_wellord1, conjecture, ! [X0] : ((relation(X0) => ('well$ufounded$urelation'(X0) <=> 'is$uwell$ufounded$uin'(X0,'relation$ufield'(X0)))))).
% 13.37/2.62 fof(negated_conjecture, negated_conjecture, ~! [X0] : ((relation(X0) => ('well$ufounded$urelation'(X0) <=> 'is$uwell$ufounded$uin'(X0,'relation$ufield'(X0))))), inference(negate_conjecture, [status(cth)], [t5_wellord1])).
% 13.37/2.62 cnf(c6, plain, ~relation(X0) | ~'well$ufounded$urelation'(X0) | X1(X0), inference(clausification, [status(esa)], [d2_wellord1])).
% 13.37/2.62 cnf(c7, plain, ~relation(X0) | 'well$ufounded$urelation'(X0) | ~X1(X0), inference(clausification, [status(esa)], [d2_wellord1])).
% 13.37/2.62 cnf(c8, plain, ~X0(X1) | ~subset(X2,'relation$ufield'(X1)) | X2 = 'empty$uset' | in(sK9(X1,X2),X2), inference(clausification, [status(esa)], [d2_wellord1])).
% 13.37/2.62 cnf(c9, plain, ~X0(X1) | ~subset(X2,'relation$ufield'(X1)) | X2 = 'empty$uset' | disjoint(fiber(X1,sK9(X1,X2)),X2), inference(clausification, [status(esa)], [d2_wellord1])).
% 13.37/2.62 cnf(c10, plain, X0(X1) | subset(sK10(X1),'relation$ufield'(X1)), inference(clausification, [status(esa)], [d2_wellord1])).
% 13.37/2.62 cnf(c11, plain, X0(X1) | sK10(X1) != 'empty$uset', inference(clausification, [status(esa)], [d2_wellord1])).
% 13.37/2.62 cnf(c12, plain, X0(X1) | ~in(X2,sK10(X1)) | ~disjoint(fiber(X1,X2),sK10(X1)), inference(clausification, [status(esa)], [d2_wellord1])).
% 13.37/2.62 cnf(c13, plain, ~relation(X0) | ~'is$uwell$ufounded$uin'(X0,X1) | X2(X0,X1), inference(clausification, [status(esa)], [d3_wellord1])).
% 13.37/2.62 cnf(c14, plain, ~relation(X0) | 'is$uwell$ufounded$uin'(X0,X1) | ~X2(X0,X1), inference(clausification, [status(esa)], [d3_wellord1])).
% 13.37/2.62 cnf(c15, plain, ~X0(X1,X2) | ~subset(X3,X2) | X3 = 'empty$uset' | in(sK16(X1,X3),X3), inference(clausification, [status(esa)], [d3_wellord1])).
% 13.37/2.62 cnf(c16, plain, ~X0(X1,X2) | ~subset(X3,X2) | X3 = 'empty$uset' | disjoint(fiber(X1,sK16(X1,X3)),X3), inference(clausification, [status(esa)], [d3_wellord1])).
% 13.37/2.62 cnf(c17, plain, X0(X1,X2) | subset(sK17(X1,X2),X2), inference(clausification, [status(esa)], [d3_wellord1])).
% 13.37/2.62 cnf(c18, plain, X0(X1,X2) | sK17(X1,X2) != 'empty$uset', inference(clausification, [status(esa)], [d3_wellord1])).
% 13.37/2.62 cnf(c19, plain, X0(X1,X2) | ~in(X3,sK17(X1,X2)) | ~disjoint(fiber(X1,X3),sK17(X1,X2)), inference(clausification, [status(esa)], [d3_wellord1])).
% 13.37/2.62 cnf(c48, plain, relation(sK55), inference(clausification, [status(esa)], [negated_conjecture])).
% 13.37/2.62 cnf(c50, plain, 'well$ufounded$urelation'(sK55) | 'is$uwell$ufounded$uin'(sK55,'relation$ufield'(sK55)), inference(clausification, [status(esa)], [negated_conjecture])).
% 13.37/2.62 cnf(c51, plain, ~'is$uwell$ufounded$uin'(sK55,'relation$ufield'(sK55)) | ~'well$ufounded$urelation'(sK55), inference(clausification, [status(esa)], [negated_conjecture])).
% 13.37/2.62 cnf(d0, plain, ~in(sK9(X0,sK17(X0,X1)),sK17(X0,X1)) | 'Ts12'(X0,X1) | sK17(X0,X1) = 'empty$uset' | ~'Ts6'(X0) | ~subset(sK17(X0,X1),'relation$ufield'(X0)), inference(resolution, [status(thm)], [c19,c9])).
% 13.37/2.62 cnf(d1, plain, sK17(X0,X1) = 'empty$uset' | ~'Ts6'(X0) | ~subset(sK17(X0,X1),'relation$ufield'(X0)) | 'Ts12'(X0,X1) | sK17(X0,X1) = 'empty$uset' | ~'Ts6'(X0) | ~subset(sK17(X0,X1),'relation$ufield'(X0)), inference(resolution, [status(thm)], [d0,c8])).
% 13.37/2.62 cnf(d2, plain, sK17(X0,'relation$ufield'(X0)) = 'empty$uset' | ~'Ts6'(X0) | 'Ts12'(X0,'relation$ufield'(X0)) | 'Ts12'(X0,'relation$ufield'(X0)), inference(resolution, [status(thm)], [d1,c17])).
% 13.37/2.62 cnf(d3, plain, sK17(X0,'relation$ufield'(X0)) = 'empty$uset' | ~'Ts6'(X0) | ~relation(X0) | 'is$uwell$ufounded$uin'(X0,'relation$ufield'(X0)), inference(resolution, [status(thm)], [d2,c14])).
% 13.37/2.62 cnf(d4, plain, sK17(sK55,'relation$ufield'(sK55)) = 'empty$uset' | ~relation(sK55) | ~'Ts6'(sK55) | ~'well$ufounded$urelation'(sK55), inference(resolution, [status(thm)], [d3,c51])).
% 13.37/2.62 cnf(d5, plain, sK17(sK55,'relation$ufield'(sK55)) = 'empty$uset' | ~'well$ufounded$urelation'(sK55) | ~'Ts6'(sK55), inference(resolution, [status(thm)], [c48,d4])).
% 13.37/2.62 cnf(d6, plain, ~relation(sK55) | 'Ts12'(sK55,'relation$ufield'(sK55)) | 'well$ufounded$urelation'(sK55), inference(resolution, [status(thm)], [c13,c50])).
% 13.37/2.62 cnf(d7, plain, 'well$ufounded$urelation'(sK55) | 'Ts12'(sK55,'relation$ufield'(sK55)), inference(resolution, [status(thm)], [c48,d6])).
% 13.37/2.62 cnf(d8, plain, X0 = 'empty$uset' | in(sK16(sK55,X0),X0) | ~subset(X0,'relation$ufield'(sK55)) | 'well$ufounded$urelation'(sK55), inference(resolution, [status(thm)], [c15,d7])).
% 13.37/2.62 cnf(d9, plain, X0 = 'empty$uset' | ~subset(X0,'relation$ufield'(sK55)) | disjoint(fiber(sK55,sK16(sK55,X0)),X0) | 'well$ufounded$urelation'(sK55), inference(resolution, [status(thm)], [c16,d7])).
% 13.37/2.62 cnf(d10, plain, sK10(sK55) = 'empty$uset' | 'well$ufounded$urelation'(sK55) | ~subset(sK10(sK55),'relation$ufield'(sK55)) | ~in(sK16(sK55,sK10(sK55)),sK10(sK55)) | 'Ts6'(sK55), inference(resolution, [status(thm)], [d9,c12])).
% 13.37/2.62 cnf(d11, plain, sK10(sK55) = 'empty$uset' | 'well$ufounded$urelation'(sK55) | 'Ts6'(sK55) | ~subset(sK10(sK55),'relation$ufield'(sK55)) | sK10(sK55) = 'empty$uset' | 'well$ufounded$urelation'(sK55) | ~subset(sK10(sK55),'relation$ufield'(sK55)), inference(resolution, [status(thm)], [d10,d8])).
% 13.37/2.62 cnf(d12, plain, sK10(sK55) = 'empty$uset' | 'well$ufounded$urelation'(sK55) | 'Ts6'(sK55) | 'Ts6'(sK55), inference(resolution, [status(thm)], [d11,c10])).
% 13.37/2.62 cnf(d13, plain, sK10(sK55) = 'empty$uset' | 'Ts6'(sK55) | ~relation(sK55) | 'Ts6'(sK55), inference(resolution, [status(thm)], [d12,c6])).
% 13.37/2.62 cnf(d14, plain, sK10(sK55) = 'empty$uset' | 'Ts6'(sK55), inference(resolution, [status(thm)], [c48,d13])).
% 13.37/2.62 cnf(d15, plain, sK10(sK55) = 'empty$uset' | ~relation(sK55) | 'well$ufounded$urelation'(sK55), inference(resolution, [status(thm)], [d14,c7])).
% 13.37/2.62 cnf(d16, plain, sK10(sK55) = 'empty$uset' | 'well$ufounded$urelation'(sK55), inference(resolution, [status(thm)], [c48,d15])).
% 13.37/2.62 cnf(d17, plain, sK17(sK55,'relation$ufield'(sK55)) = 'empty$uset' | ~'well$ufounded$urelation'(sK55) | sK10(sK55) = 'empty$uset', inference(resolution, [status(thm)], [d5,d14])).
% 13.37/2.62 cnf(d18, plain, sK10(sK55) = 'empty$uset' | sK17(sK55,'relation$ufield'(sK55)) = 'empty$uset' | sK10(sK55) = 'empty$uset', inference(resolution, [status(thm)], [d17,d16])).
% 13.37/2.62 cnf(d19, plain, 'empty$uset' != 'empty$uset' | 'Ts12'(sK55,'relation$ufield'(sK55)) | sK10(sK55) = 'empty$uset', inference(superposition, [status(thm)], [d18,c18])).
% 13.37/2.62 cnf(d20, plain, sK10(sK55) = 'empty$uset' | 'Ts12'(sK55,'relation$ufield'(sK55)), inference(equality_resolution, [status(thm)], [d19])).
% 13.37/2.62 cnf(d21, plain, sK10(sK55) = 'empty$uset' | ~relation(sK55) | 'is$uwell$ufounded$uin'(sK55,'relation$ufield'(sK55)), inference(resolution, [status(thm)], [d20,c14])).
% 13.37/2.62 cnf(d22, plain, sK10(sK55) = 'empty$uset' | 'is$uwell$ufounded$uin'(sK55,'relation$ufield'(sK55)), inference(resolution, [status(thm)], [c48,d21])).
% 13.37/2.62 cnf(d23, plain, sK10(sK55) = 'empty$uset' | ~'well$ufounded$urelation'(sK55), inference(resolution, [status(thm)], [d22,c51])).
% 13.37/2.62 cnf(d24, plain, sK10(sK55) = 'empty$uset' | sK10(sK55) = 'empty$uset', inference(resolution, [status(thm)], [d23,d16])).
% 13.37/2.62 cnf(d25, plain, 'empty$uset' != 'empty$uset' | 'Ts6'(sK55), inference(superposition, [status(thm)], [d24,c11])).
% 13.37/2.62 cnf(d26, plain, 'Ts6'(sK55), inference(equality_resolution, [status(thm)], [d25])).
% 13.37/2.62 cnf(d27, plain, sK17(sK55,'relation$ufield'(sK55)) = 'empty$uset' | ~'well$ufounded$urelation'(sK55), inference(resolution, [status(thm)], [d26,d5])).
% 13.37/2.62 cnf(d28, plain, ~relation(sK55) | 'well$ufounded$urelation'(sK55), inference(resolution, [status(thm)], [d26,c7])).
% 13.37/2.62 cnf(d29, plain, 'well$ufounded$urelation'(sK55), inference(resolution, [status(thm)], [c48,d28])).
% 13.37/2.62 cnf(d30, plain, sK17(sK55,'relation$ufield'(sK55)) = 'empty$uset', inference(resolution, [status(thm)], [d29,d27])).
% 13.37/2.62 cnf(d31, plain, 'empty$uset' != 'empty$uset' | 'Ts12'(sK55,'relation$ufield'(sK55)), inference(superposition, [status(thm)], [d30,c18])).
% 13.37/2.62 cnf(d32, plain, 'Ts12'(sK55,'relation$ufield'(sK55)), inference(equality_resolution, [status(thm)], [d31])).
% 13.37/2.62 cnf(d33, plain, ~relation(sK55) | 'is$uwell$ufounded$uin'(sK55,'relation$ufield'(sK55)), inference(resolution, [status(thm)], [d32,c14])).
% 13.37/2.62 cnf(d34, plain, 'is$uwell$ufounded$uin'(sK55,'relation$ufield'(sK55)), inference(resolution, [status(thm)], [c48,d33])).
% 13.37/2.62 cnf(d35, plain, ~'is$uwell$ufounded$uin'(sK55,'relation$ufield'(sK55)), inference(resolution, [status(thm)], [d29,c51])).
% 13.37/2.62 cnf(d36, plain, $false, inference(resolution, [status(thm)], [d35,d34])).
% 13.37/2.62 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------