%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : SEU371+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:48 AM UTC 2026
% Result : Theorem 9.70s 5.84s
% Output : CNFRefutation 9.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU371+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/0.36 % Computer : n016.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 09:26:00 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.70/5.84 % SZS status Theorem for theBenchmark.p
% 9.70/5.84 % SZS output start CNFRefutation for theBenchmark.p
% 9.70/5.84 fof(d11_yellow_0, axiom, ! [X0] : (('rel$ustr'(X0) => 'bottom$uof$urelstr'(X0) = 'join$uon$urelstr'(X0,'empty$uset')))).
% 9.70/5.84 fof(d2_yellow_1, axiom, ! [X0] : 'boole$uPOSet'(X0) = 'poset$uof$ulattice'('boole$ulattice'(X0))).
% 9.70/5.84 fof(dt_k1_lattice3, axiom, ! [X0] : (('strict$ulatt$ustr'('boole$ulattice'(X0)) & 'latt$ustr'('boole$ulattice'(X0))))).
% 9.70/5.84 fof(dt_k3_yellow_1, axiom, ! [X0] : (('strict$urel$ustr'('boole$uPOSet'(X0)) & 'rel$ustr'('boole$uPOSet'(X0))))).
% 9.70/5.84 fof(fc1_knaster, axiom, ! [X0] : ((~'empty$ucarrier'('boole$ulattice'(X0)) & ('strict$ulatt$ustr'('boole$ulattice'(X0)) & ('join$ucommutative'('boole$ulattice'(X0)) & ('join$uassociative'('boole$ulattice'(X0)) & ('meet$ucommutative'('boole$ulattice'(X0)) & ('meet$uassociative'('boole$ulattice'(X0)) & ('meet$uabsorbing'('boole$ulattice'(X0)) & ('join$uabsorbing'('boole$ulattice'(X0)) & (lattice('boole$ulattice'(X0)) & ('distributive$ulattstr'('boole$ulattice'(X0)) & ('modular$ulattstr'('boole$ulattice'(X0)) & ('lower$ubounded$usemilattstr'('boole$ulattice'(X0)) & ('upper$ubounded$usemilattstr'('boole$ulattice'(X0)) & ('bounded$ulattstr'('boole$ulattice'(X0)) & ('complemented$ulattstr'('boole$ulattice'(X0)) & ('boolean$ulattstr'('boole$ulattice'(X0)) & 'complete$ulatt$ustr'('boole$ulattice'(X0)))))))))))))))))))).
% 9.70/5.84 fof(t29_yellow_0, axiom, ! [X0] : (((~'empty$ucarrier'(X0) & (lattice(X0) & ('complete$ulatt$ustr'(X0) & 'latt$ustr'(X0)))) => ! [X1] : (('join$uof$ulatt$uset'(X0,X1) = 'join$uon$urelstr'('poset$uof$ulattice'(X0),X1) & 'meet$uof$ulatt$uset'(X0,X1) = 'meet$uon$urelstr'('poset$uof$ulattice'(X0),X1)))))).
% 9.70/5.84 fof(t3_lattice3, axiom, ! [X0] : (('lower$ubounded$usemilattstr'('boole$ulattice'(X0)) & 'bottom$uof$usemilattstr'('boole$ulattice'(X0)) = 'empty$uset'))).
% 9.70/5.84 fof(t50_lattice3, axiom, ! [X0] : (((~'empty$ucarrier'(X0) & (lattice(X0) & ('complete$ulatt$ustr'(X0) & 'latt$ustr'(X0)))) => (~'empty$ucarrier'(X0) & (lattice(X0) & ('lower$ubounded$usemilattstr'(X0) & ('latt$ustr'(X0) & 'bottom$uof$usemilattstr'(X0) = 'join$uof$ulatt$uset'(X0,'empty$uset')))))))).
% 9.70/5.84 fof(t18_yellow_1, conjecture, ! [X0] : 'bottom$uof$urelstr'('boole$uPOSet'(X0)) = 'empty$uset').
% 9.70/5.84 fof(negated_conjecture, negated_conjecture, ~! [X0] : 'bottom$uof$urelstr'('boole$uPOSet'(X0)) = 'empty$uset', inference(negate_conjecture, [status(cth)], [t18_yellow_1])).
% 9.70/5.84 cnf(c60, plain, ~'rel$ustr'(X0) | 'bottom$uof$urelstr'(X0) = 'join$uon$urelstr'(X0,'empty$uset'), inference(clausification, [status(esa)], [d11_yellow_0])).
% 9.70/5.84 cnf(c63, plain, 'boole$uPOSet'(X0) = 'poset$uof$ulattice'('boole$ulattice'(X0)), inference(clausification, [status(esa)], [d2_yellow_1])).
% 9.70/5.84 cnf(c71, plain, 'latt$ustr'('boole$ulattice'(X0)), inference(clausification, [status(esa)], [dt_k1_lattice3])).
% 9.70/5.84 cnf(c88, plain, 'rel$ustr'('boole$uPOSet'(X0)), inference(clausification, [status(esa)], [dt_k3_yellow_1])).
% 9.70/5.84 cnf(c112, plain, ~'empty$ucarrier'('boole$ulattice'(X0)), inference(clausification, [status(esa)], [fc1_knaster])).
% 9.70/5.84 cnf(c120, plain, lattice('boole$ulattice'(X0)), inference(clausification, [status(esa)], [fc1_knaster])).
% 9.70/5.84 cnf(c128, plain, 'complete$ulatt$ustr'('boole$ulattice'(X0)), inference(clausification, [status(esa)], [fc1_knaster])).
% 9.70/5.84 cnf(c368, plain, ~'complete$ulatt$ustr'(X0) | 'join$uof$ulatt$uset'(X0,X1) = 'join$uon$urelstr'('poset$uof$ulattice'(X0),X1) | ~lattice(X0) | ~'latt$ustr'(X0) | 'empty$ucarrier'(X0), inference(clausification, [status(esa)], [t29_yellow_0])).
% 9.70/5.84 cnf(c376, plain, 'bottom$uof$usemilattstr'('boole$ulattice'(X0)) = 'empty$uset', inference(clausification, [status(esa)], [t3_lattice3])).
% 9.70/5.84 cnf(c380, plain, ~lattice(X0) | X1(X0) | ~'complete$ulatt$ustr'(X0) | ~'latt$ustr'(X0) | 'empty$ucarrier'(X0), inference(clausification, [status(esa)], [t50_lattice3])).
% 9.70/5.84 cnf(c385, plain, ~X0(X1) | 'bottom$uof$usemilattstr'(X1) = 'join$uof$ulatt$uset'(X1,'empty$uset'), inference(clausification, [status(esa)], [t50_lattice3])).
% 9.70/5.84 cnf(c390, plain, 'bottom$uof$urelstr'('boole$uPOSet'(sK174)) != 'empty$uset', inference(clausification, [status(esa)], [negated_conjecture])).
% 9.70/5.84 cnf(d0, plain, ~'latt$ustr'('boole$ulattice'(X0)) | ~'complete$ulatt$ustr'('boole$ulattice'(X0)) | 'empty$ucarrier'('boole$ulattice'(X0)) | 'Ts164'('boole$ulattice'(X0)), inference(resolution, [status(thm)], [c380,c120])).
% 9.70/5.84 cnf(d1, plain, ~'complete$ulatt$ustr'('boole$ulattice'(X0)) | 'empty$ucarrier'('boole$ulattice'(X0)) | 'Ts164'('boole$ulattice'(X0)), inference(resolution, [status(thm)], [c71,d0])).
% 9.70/5.84 cnf(d2, plain, ~'complete$ulatt$ustr'('boole$ulattice'(X0)) | 'Ts164'('boole$ulattice'(X0)), inference(resolution, [status(thm)], [c112,d1])).
% 9.70/5.84 cnf(d3, plain, 'Ts164'('boole$ulattice'(X0)), inference(resolution, [status(thm)], [c128,d2])).
% 9.70/5.84 cnf(d4, plain, 'bottom$uof$usemilattstr'('boole$ulattice'(X0)) = 'join$uof$ulatt$uset'('boole$ulattice'(X0),'empty$uset'), inference(resolution, [status(thm)], [d3,c385])).
% 9.70/5.84 cnf(d5, plain, 'empty$uset' = 'join$uof$ulatt$uset'('boole$ulattice'(X0),'empty$uset'), inference(demodulation, [status(thm)], [d4,c376])).
% 9.70/5.84 cnf(d6, plain, 'join$uof$ulatt$uset'('boole$ulattice'(X0),X1) = 'join$uon$urelstr'('poset$uof$ulattice'('boole$ulattice'(X0)),X1) | ~'latt$ustr'('boole$ulattice'(X0)) | ~'complete$ulatt$ustr'('boole$ulattice'(X0)) | 'empty$ucarrier'('boole$ulattice'(X0)), inference(resolution, [status(thm)], [c368,c120])).
% 9.70/5.84 cnf(d7, plain, 'join$uof$ulatt$uset'('boole$ulattice'(X0),X1) = 'join$uon$urelstr'('boole$uPOSet'(X0),X1) | ~'latt$ustr'('boole$ulattice'(X0)) | ~'complete$ulatt$ustr'('boole$ulattice'(X0)) | 'empty$ucarrier'('boole$ulattice'(X0)), inference(demodulation, [status(thm)], [d6,c63])).
% 9.70/5.84 cnf(d8, plain, 'join$uof$ulatt$uset'('boole$ulattice'(X0),X1) = 'join$uon$urelstr'('boole$uPOSet'(X0),X1) | ~'complete$ulatt$ustr'('boole$ulattice'(X0)) | 'empty$ucarrier'('boole$ulattice'(X0)), inference(resolution, [status(thm)], [c71,d7])).
% 9.70/5.84 cnf(d9, plain, 'join$uof$ulatt$uset'('boole$ulattice'(X0),X1) = 'join$uon$urelstr'('boole$uPOSet'(X0),X1) | ~'complete$ulatt$ustr'('boole$ulattice'(X0)), inference(resolution, [status(thm)], [c112,d8])).
% 9.70/5.84 cnf(d10, plain, 'join$uof$ulatt$uset'('boole$ulattice'(X0),X1) = 'join$uon$urelstr'('boole$uPOSet'(X0),X1), inference(resolution, [status(thm)], [c128,d9])).
% 9.70/5.84 cnf(d11, plain, 'bottom$uof$urelstr'('boole$uPOSet'(X0)) = 'join$uon$urelstr'('boole$uPOSet'(X0),'empty$uset'), inference(resolution, [status(thm)], [c88,c60])).
% 9.70/5.84 cnf(d12, plain, 'bottom$uof$urelstr'('boole$uPOSet'(X0)) = 'join$uof$ulatt$uset'('boole$ulattice'(X0),'empty$uset'), inference(demodulation, [status(thm)], [d11,d10])).
% 9.70/5.84 cnf(d13, plain, 'bottom$uof$urelstr'('boole$uPOSet'(X0)) = 'empty$uset', inference(demodulation, [status(thm)], [d12,d5])).
% 9.70/5.84 cnf(d14, plain, $false, inference(resolution, [status(thm)], [d13,c390])).
% 9.70/5.84 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------