%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : LAT311+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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 07:48:15 AM UTC 2026
% Result : Theorem 19.16s 4.58s
% Output : CNFRefutation 19.16s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT311+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n026.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Fri Sep 25 20:46:40 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 19.16/4.58 % SZS status Theorem for theBenchmark.p
% 19.16/4.58 % SZS output start CNFRefutation for theBenchmark.p
% 19.16/4.58 fof(d3_filter_0, axiom, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & 'l3$ulattices'(X0))) => ! [X1] : (('m1$usubset$u1'(X1,'u1$ustruct$u0'(X0)) => 'k2$ufilter$u0'(X0,X1) = 'a$u2$u0$ufilter$u0'(X0,X1)))))).
% 19.16/4.58 fof(d4_filter_2, axiom, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & 'l3$ulattices'(X0))) => ! [X1] : (('m1$usubset$u1'(X1,'u1$ustruct$u0'(X0)) => 'k5$ufilter$u2'(X0,X1) = X1))))).
% 19.16/4.58 fof(d6_filter_2, axiom, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & 'l3$ulattices'(X0))) => ! [X1] : (('m1$usubset$u1'(X1,'k1$uzfmisc$u1'('u1$ustruct$u0'(X0))) => 'k7$ufilter$u2'(X0,X1) = X1))))).
% 19.16/4.58 fof(dt_k1_lattice2, axiom, ! [X0] : (('l3$ulattices'(X0) => ('v3$ulattices'('k1$ulattice2'(X0)) & 'l3$ulattices'('k1$ulattice2'(X0)))))).
% 19.16/4.58 fof(dt_k5_filter_2, axiom, ! [X0] : ! [X1] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & ('l3$ulattices'(X0) & 'm1$usubset$u1'(X1,'u1$ustruct$u0'(X0))))) => 'm1$usubset$u1'('k5$ufilter$u2'(X0,X1),'u1$ustruct$u0'('k1$ulattice2'(X0)))))).
% 19.16/4.58 fof(dt_k7_filter_2, axiom, ! [X0] : ! [X1] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & ('l3$ulattices'(X0) & 'm1$usubset$u1'(X1,'k1$uzfmisc$u1'('u1$ustruct$u0'(X0)))))) => 'm1$usubset$u1'('k7$ufilter$u2'(X0,X1),'k1$uzfmisc$u1'('u1$ustruct$u0'('k1$ulattice2'(X0))))))).
% 19.16/4.58 fof(fc6_lattice2, axiom, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & 'l3$ulattices'(X0))) => (~'v3$ustruct$u0'('k1$ulattice2'(X0)) & ('v3$ulattices'('k1$ulattice2'(X0)) & ('v4$ulattices'('k1$ulattice2'(X0)) & ('v5$ulattices'('k1$ulattice2'(X0)) & ('v6$ulattices'('k1$ulattice2'(X0)) & ('v7$ulattices'('k1$ulattice2'(X0)) & ('v8$ulattices'('k1$ulattice2'(X0)) & ('v9$ulattices'('k1$ulattice2'(X0)) & 'v10$ulattices'('k1$ulattice2'(X0))))))))))))).
% 19.16/4.58 fof(redefinition_k2_filter_2, axiom, ! [X0] : ! [X1] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & ('l3$ulattices'(X0) & 'm1$usubset$u1'(X1,'u1$ustruct$u0'(X0))))) => 'k2$ufilter$u2'(X0,X1) = 'k2$ufilter$u0'(X0,X1)))).
% 19.16/4.58 fof(redefinition_k3_filter_2, axiom, ! [X0] : ! [X1] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & ('l3$ulattices'(X0) & (~'v1$uxboole$u0'(X1) & 'm1$usubset$u1'(X1,'k1$uzfmisc$u1'('u1$ustruct$u0'(X0))))))) => 'k3$ufilter$u2'(X0,X1) = 'k3$ufilter$u0'(X0,X1)))).
% 19.16/4.58 fof(t29_filter_0, axiom, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & 'l3$ulattices'(X0))) => ! [X1] : (('m1$usubset$u1'(X1,'u1$ustruct$u0'(X0)) => ! [X2] : (((~'v1$uxboole$u0'(X2) & 'm1$usubset$u1'(X2,'k1$uzfmisc$u1'('u1$ustruct$u0'(X0)))) => ('r2$uhidden'(X1,X2) => 'r1$utarski'('k2$ufilter$u0'(X0,X1),'k3$ufilter$u0'(X0,X2)))))))))).
% 19.16/4.58 fof(t30_filter_2, axiom, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & 'l3$ulattices'(X0))) => ! [X1] : (('m1$usubset$u1'(X1,'u1$ustruct$u0'(X0)) => ('k18$ufilter$u2'(X0,X1) = 'k2$ufilter$u2'('k1$ulattice2'(X0),'k5$ufilter$u2'(X0,X1)) & 'k18$ufilter$u2'('k1$ulattice2'(X0),'k5$ufilter$u2'(X0,X1)) = 'k2$ufilter$u2'(X0,X1))))))).
% 19.16/4.58 fof(t37_filter_2, axiom, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & 'l3$ulattices'(X0))) => ! [X1] : (((~'v1$uxboole$u0'(X1) & 'm1$usubset$u1'(X1,'k1$uzfmisc$u1'('u1$ustruct$u0'(X0)))) => ! [X2] : (((~'v1$uxboole$u0'(X2) & 'm1$usubset$u1'(X2,'k1$uzfmisc$u1'('u1$ustruct$u0'('k1$ulattice2'(X0))))) => ('k3$ufilter$u2'('k1$ulattice2'(X0),'k7$ufilter$u2'(X0,X1)) = 'k19$ufilter$u2'(X0,X1) & ('k3$ufilter$u2'(X0,X1) = 'k19$ufilter$u2'('k1$ulattice2'(X0),'k7$ufilter$u2'(X0,X1)) & ('k3$ufilter$u2'(X0,'k8$ufilter$u2'(X0,X2)) = 'k19$ufilter$u2'('k1$ulattice2'(X0),X2) & 'k3$ufilter$u2'('k1$ulattice2'(X0),X2) = 'k19$ufilter$u2'(X0,'k8$ufilter$u2'(X0,X2)))))))))))).
% 19.16/4.58 fof(t40_filter_2, conjecture, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & 'l3$ulattices'(X0))) => ! [X1] : (('m1$usubset$u1'(X1,'u1$ustruct$u0'(X0)) => ! [X2] : (((~'v1$uxboole$u0'(X2) & 'm1$usubset$u1'(X2,'k1$uzfmisc$u1'('u1$ustruct$u0'(X0)))) => ('r2$uhidden'(X1,X2) => 'r1$utarski'('k18$ufilter$u2'(X0,X1),'k19$ufilter$u2'(X0,X2)))))))))).
% 19.16/4.58 fof(negated_conjecture, negated_conjecture, ~! [X0] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & 'l3$ulattices'(X0))) => ! [X1] : (('m1$usubset$u1'(X1,'u1$ustruct$u0'(X0)) => ! [X2] : (((~'v1$uxboole$u0'(X2) & 'm1$usubset$u1'(X2,'k1$uzfmisc$u1'('u1$ustruct$u0'(X0)))) => ('r2$uhidden'(X1,X2) => 'r1$utarski'('k18$ufilter$u2'(X0,X1),'k19$ufilter$u2'(X0,X2))))))))), inference(negate_conjecture, [status(cth)], [t40_filter_2])).
% 19.16/4.58 cnf(c18, plain, 'k2$ufilter$u0'(X0,X1) = 'a$u2$u0$ufilter$u0'(X0,X1) | ~'m1$usubset$u1'(X1,'u1$ustruct$u0'(X0)) | 'v3$ustruct$u0'(X0) | ~'v10$ulattices'(X0) | ~'l3$ulattices'(X0), inference(clausification, [status(esa)], [d3_filter_0])).
% 19.16/4.58 cnf(c19, plain, ~'v10$ulattices'(X0) | 'k5$ufilter$u2'(X0,X1) = X1 | ~'m1$usubset$u1'(X1,'u1$ustruct$u0'(X0)) | ~'l3$ulattices'(X0) | 'v3$ustruct$u0'(X0), inference(clausification, [status(esa)], [d4_filter_2])).
% 19.16/4.58 cnf(c20, plain, 'k7$ufilter$u2'(X0,X1) = X1 | ~'m1$usubset$u1'(X1,'k1$uzfmisc$u1'('u1$ustruct$u0'(X0))) | ~'v10$ulattices'(X0) | 'v3$ustruct$u0'(X0) | ~'l3$ulattices'(X0), inference(clausification, [status(esa)], [d6_filter_2])).
% 19.16/4.58 cnf(c28, plain, ~'l3$ulattices'(X0) | 'l3$ulattices'('k1$ulattice2'(X0)), inference(clausification, [status(esa)], [dt_k1_lattice2])).
% 19.16/4.58 cnf(c33, plain, ~'l3$ulattices'(X0) | ~'v10$ulattices'(X0) | ~'m1$usubset$u1'(X1,'u1$ustruct$u0'(X0)) | 'v3$ustruct$u0'(X0) | 'm1$usubset$u1'('k5$ufilter$u2'(X0,X1),'u1$ustruct$u0'('k1$ulattice2'(X0))), inference(clausification, [status(esa)], [dt_k5_filter_2])).
% 19.16/4.58 cnf(c34, plain, 'v3$ustruct$u0'(X0) | ~'l3$ulattices'(X0) | ~'m1$usubset$u1'(X1,'k1$uzfmisc$u1'('u1$ustruct$u0'(X0))) | 'm1$usubset$u1'('k7$ufilter$u2'(X0,X1),'k1$uzfmisc$u1'('u1$ustruct$u0'('k1$ulattice2'(X0)))) | ~'v10$ulattices'(X0), inference(clausification, [status(esa)], [dt_k7_filter_2])).
% 19.16/4.58 cnf(c99, plain, 'v3$ustruct$u0'(X0) | ~'v10$ulattices'(X0) | ~'l3$ulattices'(X0) | X1(X0), inference(clausification, [status(esa)], [fc6_lattice2])).
% 19.16/4.58 cnf(c100, plain, ~X0(X1) | ~'v3$ustruct$u0'('k1$ulattice2'(X1)), inference(clausification, [status(esa)], [fc6_lattice2])).
% 19.16/4.58 cnf(c108, plain, ~X0(X1) | 'v10$ulattices'('k1$ulattice2'(X1)), inference(clausification, [status(esa)], [fc6_lattice2])).
% 19.16/4.58 cnf(c155, plain, ~'m1$usubset$u1'(X0,'u1$ustruct$u0'(X1)) | 'k2$ufilter$u2'(X1,X0) = 'k2$ufilter$u0'(X1,X0) | 'v3$ustruct$u0'(X1) | ~'l3$ulattices'(X1) | ~'v10$ulattices'(X1), inference(clausification, [status(esa)], [redefinition_k2_filter_2])).
% 19.16/4.58 cnf(c156, plain, ~'l3$ulattices'(X0) | 'k3$ufilter$u2'(X0,X1) = 'k3$ufilter$u0'(X0,X1) | 'v1$uxboole$u0'(X1) | ~'v10$ulattices'(X0) | 'v3$ustruct$u0'(X0) | ~'m1$usubset$u1'(X1,'k1$uzfmisc$u1'('u1$ustruct$u0'(X0))), inference(clausification, [status(esa)], [redefinition_k3_filter_2])).
% 19.16/4.58 cnf(c166, plain, ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(X1))) | ~'r2$uhidden'(X2,X0) | 'v3$ustruct$u0'(X1) | 'r1$utarski'('k2$ufilter$u0'(X1,X2),'k3$ufilter$u0'(X1,X0)) | ~'v10$ulattices'(X1) | ~'l3$ulattices'(X1) | 'v1$uxboole$u0'(X0) | ~'m1$usubset$u1'(X2,'u1$ustruct$u0'(X1)), inference(clausification, [status(esa)], [t29_filter_0])).
% 19.16/4.58 cnf(c172, plain, ~'m1$usubset$u1'(X0,'u1$ustruct$u0'(X1)) | 'k18$ufilter$u2'(X1,X0) = 'k2$ufilter$u2'('k1$ulattice2'(X1),'k5$ufilter$u2'(X1,X0)) | ~'v10$ulattices'(X1) | 'v3$ustruct$u0'(X1) | ~'l3$ulattices'(X1), inference(clausification, [status(esa)], [t30_filter_2])).
% 19.16/4.58 cnf(c174, plain, 'v1$uxboole$u0'(X0) | ~'m1$usubset$u1'(X1,'k1$uzfmisc$u1'('u1$ustruct$u0'('k1$ulattice2'(X2)))) | 'v3$ustruct$u0'(X2) | ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(X2))) | ~'l3$ulattices'(X2) | 'v1$uxboole$u0'(X1) | ~'v10$ulattices'(X2) | 'k3$ufilter$u2'('k1$ulattice2'(X2),'k7$ufilter$u2'(X2,X0)) = 'k19$ufilter$u2'(X2,X0), inference(clausification, [status(esa)], [t37_filter_2])).
% 19.16/4.58 cnf(c185, plain, ~'v3$ustruct$u0'(sK180), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.16/4.58 cnf(c186, plain, 'v10$ulattices'(sK180), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.16/4.58 cnf(c187, plain, 'l3$ulattices'(sK180), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.16/4.58 cnf(c188, plain, 'm1$usubset$u1'(sK181,'u1$ustruct$u0'(sK180)), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.16/4.58 cnf(c189, plain, ~'v1$uxboole$u0'(sK182), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.16/4.58 cnf(c190, plain, 'm1$usubset$u1'(sK182,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK180))), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.16/4.58 cnf(c191, plain, 'r2$uhidden'(sK181,sK182), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.16/4.58 cnf(c192, plain, ~'r1$utarski'('k18$ufilter$u2'(sK180,sK181),'k19$ufilter$u2'(sK180,sK182)), inference(clausification, [status(esa)], [negated_conjecture])).
% 19.16/4.58 cnf(d0, plain, 'k7$ufilter$u2'(sK180,sK182) = sK182 | ~'l3$ulattices'(sK180) | ~'v10$ulattices'(sK180) | 'v3$ustruct$u0'(sK180), inference(resolution, [status(thm)], [c20,c190])).
% 19.16/4.58 cnf(d1, plain, 'k7$ufilter$u2'(sK180,sK182) = sK182 | ~'l3$ulattices'(sK180) | ~'v10$ulattices'(sK180), inference(resolution, [status(thm)], [c185,d0])).
% 19.16/4.58 cnf(d2, plain, 'k7$ufilter$u2'(sK180,sK182) = sK182 | ~'l3$ulattices'(sK180), inference(resolution, [status(thm)], [c186,d1])).
% 19.16/4.58 cnf(d3, plain, 'k7$ufilter$u2'(sK180,sK182) = sK182, inference(resolution, [status(thm)], [c187,d2])).
% 19.16/4.58 cnf(d4, plain, 'm1$usubset$u1'(sK182,'k1$uzfmisc$u1'('u1$ustruct$u0'('k1$ulattice2'(sK180)))) | ~'l3$ulattices'(sK180) | ~'v10$ulattices'(sK180) | 'v3$ustruct$u0'(sK180) | ~'m1$usubset$u1'(sK182,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK180))), inference(superposition, [status(thm)], [d3,c34])).
% 19.16/4.58 cnf(d5, plain, ~'l3$ulattices'(sK180) | ~'v10$ulattices'(sK180) | 'm1$usubset$u1'(sK182,'k1$uzfmisc$u1'('u1$ustruct$u0'('k1$ulattice2'(sK180)))) | ~'m1$usubset$u1'(sK182,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK180))), inference(resolution, [status(thm)], [c185,d4])).
% 19.16/4.58 cnf(d6, plain, ~'l3$ulattices'(sK180) | 'm1$usubset$u1'(sK182,'k1$uzfmisc$u1'('u1$ustruct$u0'('k1$ulattice2'(sK180)))) | ~'m1$usubset$u1'(sK182,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK180))), inference(resolution, [status(thm)], [c186,d5])).
% 19.16/4.58 cnf(d7, plain, 'm1$usubset$u1'(sK182,'k1$uzfmisc$u1'('u1$ustruct$u0'('k1$ulattice2'(sK180)))) | ~'m1$usubset$u1'(sK182,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK180))), inference(resolution, [status(thm)], [c187,d6])).
% 19.16/4.58 cnf(d8, plain, 'm1$usubset$u1'(sK182,'k1$uzfmisc$u1'('u1$ustruct$u0'('k1$ulattice2'(sK180)))), inference(resolution, [status(thm)], [c190,d7])).
% 19.16/4.58 cnf(d9, plain, 'k3$ufilter$u2'('k1$ulattice2'(sK180),'k7$ufilter$u2'(sK180,X0)) = 'k19$ufilter$u2'(sK180,X0) | ~'l3$ulattices'(sK180) | 'v1$uxboole$u0'(X0) | 'v1$uxboole$u0'(sK182) | ~'v10$ulattices'(sK180) | 'v3$ustruct$u0'(sK180) | ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK180))), inference(resolution, [status(thm)], [c174,d8])).
% 19.16/4.58 cnf(d10, plain, 'k3$ufilter$u2'('k1$ulattice2'(sK180),'k7$ufilter$u2'(sK180,X0)) = 'k19$ufilter$u2'(sK180,X0) | ~'l3$ulattices'(sK180) | 'v1$uxboole$u0'(X0) | 'v1$uxboole$u0'(sK182) | ~'v10$ulattices'(sK180) | ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK180))), inference(resolution, [status(thm)], [c185,d9])).
% 19.16/4.58 cnf(d11, plain, 'k3$ufilter$u2'('k1$ulattice2'(sK180),'k7$ufilter$u2'(sK180,X0)) = 'k19$ufilter$u2'(sK180,X0) | ~'l3$ulattices'(sK180) | 'v1$uxboole$u0'(X0) | 'v1$uxboole$u0'(sK182) | ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK180))), inference(resolution, [status(thm)], [c186,d10])).
% 19.16/4.58 cnf(d12, plain, 'k3$ufilter$u2'('k1$ulattice2'(sK180),'k7$ufilter$u2'(sK180,X0)) = 'k19$ufilter$u2'(sK180,X0) | 'v1$uxboole$u0'(X0) | 'v1$uxboole$u0'(sK182) | ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK180))), inference(resolution, [status(thm)], [c187,d11])).
% 19.16/4.58 cnf(d13, plain, 'k3$ufilter$u2'('k1$ulattice2'(sK180),'k7$ufilter$u2'(sK180,X0)) = 'k19$ufilter$u2'(sK180,X0) | 'v1$uxboole$u0'(X0) | ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'(sK180))), inference(resolution, [status(thm)], [c189,d12])).
% 19.16/4.58 cnf(d14, plain, 'k3$ufilter$u2'('k1$ulattice2'(sK180),'k7$ufilter$u2'(sK180,sK182)) = 'k19$ufilter$u2'(sK180,sK182) | 'v1$uxboole$u0'(sK182), inference(resolution, [status(thm)], [d13,c190])).
% 19.16/4.58 cnf(d15, plain, 'k3$ufilter$u2'('k1$ulattice2'(sK180),sK182) = 'k19$ufilter$u2'(sK180,sK182) | 'v1$uxboole$u0'(sK182), inference(demodulation, [status(thm)], [d14,d3])).
% 19.16/4.58 cnf(d16, plain, 'k3$ufilter$u2'('k1$ulattice2'(sK180),sK182) = 'k19$ufilter$u2'(sK180,sK182), inference(resolution, [status(thm)], [c189,d15])).
% 19.16/4.58 cnf(d17, plain, 'k5$ufilter$u2'(sK180,sK181) = sK181 | ~'l3$ulattices'(sK180) | ~'v10$ulattices'(sK180) | 'v3$ustruct$u0'(sK180), inference(resolution, [status(thm)], [c19,c188])).
% 19.16/4.58 cnf(d18, plain, 'k5$ufilter$u2'(sK180,sK181) = sK181 | ~'l3$ulattices'(sK180) | ~'v10$ulattices'(sK180), inference(resolution, [status(thm)], [c185,d17])).
% 19.16/4.58 cnf(d19, plain, 'k5$ufilter$u2'(sK180,sK181) = sK181 | ~'l3$ulattices'(sK180), inference(resolution, [status(thm)], [c186,d18])).
% 19.16/4.58 cnf(d20, plain, 'k5$ufilter$u2'(sK180,sK181) = sK181, inference(resolution, [status(thm)], [c187,d19])).
% 19.16/4.58 cnf(d21, plain, 'm1$usubset$u1'(sK181,'u1$ustruct$u0'('k1$ulattice2'(sK180))) | ~'l3$ulattices'(sK180) | ~'v10$ulattices'(sK180) | 'v3$ustruct$u0'(sK180) | ~'m1$usubset$u1'(sK181,'u1$ustruct$u0'(sK180)), inference(superposition, [status(thm)], [d20,c33])).
% 19.16/4.58 cnf(d22, plain, ~'l3$ulattices'(sK180) | ~'v10$ulattices'(sK180) | 'm1$usubset$u1'(sK181,'u1$ustruct$u0'('k1$ulattice2'(sK180))) | ~'m1$usubset$u1'(sK181,'u1$ustruct$u0'(sK180)), inference(resolution, [status(thm)], [c185,d21])).
% 19.16/4.58 cnf(d23, plain, ~'l3$ulattices'(sK180) | 'm1$usubset$u1'(sK181,'u1$ustruct$u0'('k1$ulattice2'(sK180))) | ~'m1$usubset$u1'(sK181,'u1$ustruct$u0'(sK180)), inference(resolution, [status(thm)], [c186,d22])).
% 19.16/4.58 cnf(d24, plain, 'm1$usubset$u1'(sK181,'u1$ustruct$u0'('k1$ulattice2'(sK180))) | ~'m1$usubset$u1'(sK181,'u1$ustruct$u0'(sK180)), inference(resolution, [status(thm)], [c187,d23])).
% 19.16/4.58 cnf(d25, plain, 'm1$usubset$u1'(sK181,'u1$ustruct$u0'('k1$ulattice2'(sK180))), inference(resolution, [status(thm)], [c188,d24])).
% 19.16/4.58 cnf(d26, plain, 'k2$ufilter$u0'('k1$ulattice2'(sK180),sK181) = 'a$u2$u0$ufilter$u0'('k1$ulattice2'(sK180),sK181) | ~'l3$ulattices'('k1$ulattice2'(sK180)) | ~'v10$ulattices'('k1$ulattice2'(sK180)) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)), inference(resolution, [status(thm)], [d25,c18])).
% 19.16/4.58 cnf(d27, plain, ~'Ts100'(sK180) | 'k2$ufilter$u0'('k1$ulattice2'(sK180),sK181) = 'a$u2$u0$ufilter$u0'('k1$ulattice2'(sK180),sK181) | ~'l3$ulattices'('k1$ulattice2'(sK180)) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)), inference(resolution, [status(thm)], [c108,d26])).
% 19.16/4.58 cnf(d28, plain, ~'l3$ulattices'(sK180) | 'v3$ustruct$u0'(sK180) | 'Ts100'(sK180), inference(resolution, [status(thm)], [c99,c186])).
% 19.16/4.58 cnf(d29, plain, ~'l3$ulattices'(sK180) | 'Ts100'(sK180), inference(resolution, [status(thm)], [c185,d28])).
% 19.16/4.58 cnf(d30, plain, 'Ts100'(sK180), inference(resolution, [status(thm)], [c187,d29])).
% 19.16/4.58 cnf(d31, plain, 'k2$ufilter$u0'('k1$ulattice2'(sK180),sK181) = 'a$u2$u0$ufilter$u0'('k1$ulattice2'(sK180),sK181) | ~'l3$ulattices'('k1$ulattice2'(sK180)) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)), inference(resolution, [status(thm)], [d30,d27])).
% 19.16/4.58 cnf(d32, plain, 'k2$ufilter$u0'('k1$ulattice2'(sK180),sK181) = 'a$u2$u0$ufilter$u0'('k1$ulattice2'(sK180),sK181) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)) | ~'l3$ulattices'(sK180), inference(resolution, [status(thm)], [d31,c28])).
% 19.16/4.58 cnf(d33, plain, 'k2$ufilter$u0'('k1$ulattice2'(sK180),sK181) = 'a$u2$u0$ufilter$u0'('k1$ulattice2'(sK180),sK181) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)), inference(resolution, [status(thm)], [c187,d32])).
% 19.16/4.58 cnf(d34, plain, 'k2$ufilter$u0'('k1$ulattice2'(sK180),sK181) = 'a$u2$u0$ufilter$u0'('k1$ulattice2'(sK180),sK181) | ~'Ts100'(sK180), inference(resolution, [status(thm)], [d33,c100])).
% 19.16/4.58 cnf(d35, plain, 'k2$ufilter$u0'('k1$ulattice2'(sK180),sK181) = 'a$u2$u0$ufilter$u0'('k1$ulattice2'(sK180),sK181), inference(resolution, [status(thm)], [d30,d34])).
% 19.16/4.58 cnf(d36, plain, 'k18$ufilter$u2'(sK180,sK181) = 'k2$ufilter$u2'('k1$ulattice2'(sK180),'k5$ufilter$u2'(sK180,sK181)) | ~'l3$ulattices'(sK180) | ~'v10$ulattices'(sK180) | 'v3$ustruct$u0'(sK180), inference(resolution, [status(thm)], [c172,c188])).
% 19.16/4.58 cnf(d37, plain, 'k18$ufilter$u2'(sK180,sK181) = 'k2$ufilter$u2'('k1$ulattice2'(sK180),sK181) | ~'l3$ulattices'(sK180) | ~'v10$ulattices'(sK180) | 'v3$ustruct$u0'(sK180), inference(demodulation, [status(thm)], [d36,d20])).
% 19.16/4.58 cnf(d38, plain, 'k18$ufilter$u2'(sK180,sK181) = 'k2$ufilter$u2'('k1$ulattice2'(sK180),sK181) | ~'l3$ulattices'(sK180) | ~'v10$ulattices'(sK180), inference(resolution, [status(thm)], [c185,d37])).
% 19.16/4.58 cnf(d39, plain, 'k18$ufilter$u2'(sK180,sK181) = 'k2$ufilter$u2'('k1$ulattice2'(sK180),sK181) | ~'l3$ulattices'(sK180), inference(resolution, [status(thm)], [c186,d38])).
% 19.16/4.58 cnf(d40, plain, 'k18$ufilter$u2'(sK180,sK181) = 'k2$ufilter$u2'('k1$ulattice2'(sK180),sK181), inference(resolution, [status(thm)], [c187,d39])).
% 19.16/4.58 cnf(d41, plain, 'k2$ufilter$u2'('k1$ulattice2'(sK180),sK181) = 'k2$ufilter$u0'('k1$ulattice2'(sK180),sK181) | ~'l3$ulattices'('k1$ulattice2'(sK180)) | ~'v10$ulattices'('k1$ulattice2'(sK180)) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)), inference(resolution, [status(thm)], [c155,d25])).
% 19.16/4.58 cnf(d42, plain, 'k18$ufilter$u2'(sK180,sK181) = 'k2$ufilter$u0'('k1$ulattice2'(sK180),sK181) | ~'l3$ulattices'('k1$ulattice2'(sK180)) | ~'v10$ulattices'('k1$ulattice2'(sK180)) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)), inference(demodulation, [status(thm)], [d41,d40])).
% 19.16/4.58 cnf(d43, plain, 'k18$ufilter$u2'(sK180,sK181) = 'a$u2$u0$ufilter$u0'('k1$ulattice2'(sK180),sK181) | ~'l3$ulattices'('k1$ulattice2'(sK180)) | ~'v10$ulattices'('k1$ulattice2'(sK180)) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)), inference(demodulation, [status(thm)], [d42,d35])).
% 19.16/4.58 cnf(d44, plain, 'k18$ufilter$u2'(sK180,sK181) = 'a$u2$u0$ufilter$u0'('k1$ulattice2'(sK180),sK181) | ~'l3$ulattices'('k1$ulattice2'(sK180)) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)) | ~'Ts100'(sK180), inference(resolution, [status(thm)], [d43,c108])).
% 19.16/4.58 cnf(d45, plain, 'k18$ufilter$u2'(sK180,sK181) = 'a$u2$u0$ufilter$u0'('k1$ulattice2'(sK180),sK181) | ~'l3$ulattices'('k1$ulattice2'(sK180)) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)), inference(resolution, [status(thm)], [d30,d44])).
% 19.16/4.58 cnf(d46, plain, 'k18$ufilter$u2'(sK180,sK181) = 'a$u2$u0$ufilter$u0'('k1$ulattice2'(sK180),sK181) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)) | ~'l3$ulattices'(sK180), inference(resolution, [status(thm)], [d45,c28])).
% 19.16/4.58 cnf(d47, plain, 'k18$ufilter$u2'(sK180,sK181) = 'a$u2$u0$ufilter$u0'('k1$ulattice2'(sK180),sK181) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)), inference(resolution, [status(thm)], [c187,d46])).
% 19.16/4.58 cnf(d48, plain, 'k18$ufilter$u2'(sK180,sK181) = 'a$u2$u0$ufilter$u0'('k1$ulattice2'(sK180),sK181) | ~'Ts100'(sK180), inference(resolution, [status(thm)], [d47,c100])).
% 19.16/4.58 cnf(d49, plain, 'k18$ufilter$u2'(sK180,sK181) = 'a$u2$u0$ufilter$u0'('k1$ulattice2'(sK180),sK181), inference(resolution, [status(thm)], [d30,d48])).
% 19.16/4.58 cnf(d50, plain, 'r1$utarski'('a$u2$u0$ufilter$u0'('k1$ulattice2'(sK180),sK181),'k3$ufilter$u0'('k1$ulattice2'(sK180),X0)) | ~'l3$ulattices'('k1$ulattice2'(sK180)) | ~'r2$uhidden'(sK181,X0) | 'v1$uxboole$u0'(X0) | ~'v10$ulattices'('k1$ulattice2'(sK180)) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)) | ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'('k1$ulattice2'(sK180)))) | ~'m1$usubset$u1'(sK181,'u1$ustruct$u0'('k1$ulattice2'(sK180))), inference(superposition, [status(thm)], [d35,c166])).
% 19.16/4.58 cnf(d51, plain, ~'l3$ulattices'('k1$ulattice2'(sK180)) | ~'r2$uhidden'(sK181,X0) | 'v1$uxboole$u0'(X0) | ~'v10$ulattices'('k1$ulattice2'(sK180)) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)) | ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'('k1$ulattice2'(sK180)))) | ~'m1$usubset$u1'(sK181,'u1$ustruct$u0'('k1$ulattice2'(sK180))) | 'r1$utarski'('k18$ufilter$u2'(sK180,sK181),'k3$ufilter$u0'('k1$ulattice2'(sK180),X0)), inference(demodulation, [status(thm)], [d50,d49])).
% 19.16/4.58 cnf(d52, plain, ~'l3$ulattices'('k1$ulattice2'(sK180)) | ~'r2$uhidden'(sK181,X0) | 'v1$uxboole$u0'(X0) | ~'v10$ulattices'('k1$ulattice2'(sK180)) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)) | ~'m1$usubset$u1'(X0,'k1$uzfmisc$u1'('u1$ustruct$u0'('k1$ulattice2'(sK180)))) | 'r1$utarski'('k18$ufilter$u2'(sK180,sK181),'k3$ufilter$u0'('k1$ulattice2'(sK180),X0)), inference(resolution, [status(thm)], [d25,d51])).
% 19.16/4.58 cnf(d53, plain, 'k3$ufilter$u2'('k1$ulattice2'(sK180),sK182) = 'k3$ufilter$u0'('k1$ulattice2'(sK180),sK182) | ~'l3$ulattices'('k1$ulattice2'(sK180)) | 'v1$uxboole$u0'(sK182) | ~'v10$ulattices'('k1$ulattice2'(sK180)) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)), inference(resolution, [status(thm)], [c156,d8])).
% 19.16/4.58 cnf(d54, plain, 'k3$ufilter$u2'('k1$ulattice2'(sK180),sK182) = 'k3$ufilter$u0'('k1$ulattice2'(sK180),sK182) | ~'l3$ulattices'('k1$ulattice2'(sK180)) | ~'v10$ulattices'('k1$ulattice2'(sK180)) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)), inference(resolution, [status(thm)], [c189,d53])).
% 19.16/4.58 cnf(d55, plain, 'k3$ufilter$u2'('k1$ulattice2'(sK180),sK182) = 'k3$ufilter$u0'('k1$ulattice2'(sK180),sK182) | ~'l3$ulattices'('k1$ulattice2'(sK180)) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)) | ~'Ts100'(sK180), inference(resolution, [status(thm)], [d54,c108])).
% 19.16/4.58 cnf(d56, plain, 'k3$ufilter$u2'('k1$ulattice2'(sK180),sK182) = 'k3$ufilter$u0'('k1$ulattice2'(sK180),sK182) | ~'l3$ulattices'('k1$ulattice2'(sK180)) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)), inference(resolution, [status(thm)], [d30,d55])).
% 19.16/4.58 cnf(d57, plain, 'k3$ufilter$u2'('k1$ulattice2'(sK180),sK182) = 'k3$ufilter$u0'('k1$ulattice2'(sK180),sK182) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)) | ~'l3$ulattices'(sK180), inference(resolution, [status(thm)], [d56,c28])).
% 19.16/4.58 cnf(d58, plain, 'k3$ufilter$u2'('k1$ulattice2'(sK180),sK182) = 'k3$ufilter$u0'('k1$ulattice2'(sK180),sK182) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)), inference(resolution, [status(thm)], [c187,d57])).
% 19.16/4.58 cnf(d59, plain, 'k3$ufilter$u2'('k1$ulattice2'(sK180),sK182) = 'k3$ufilter$u0'('k1$ulattice2'(sK180),sK182) | ~'Ts100'(sK180), inference(resolution, [status(thm)], [d58,c100])).
% 19.16/4.58 cnf(d60, plain, 'k3$ufilter$u2'('k1$ulattice2'(sK180),sK182) = 'k3$ufilter$u0'('k1$ulattice2'(sK180),sK182), inference(resolution, [status(thm)], [d30,d59])).
% 19.16/4.58 cnf(d61, plain, 'r1$utarski'('k18$ufilter$u2'(sK180,sK181),'k3$ufilter$u2'('k1$ulattice2'(sK180),sK182)) | ~'l3$ulattices'('k1$ulattice2'(sK180)) | ~'r2$uhidden'(sK181,sK182) | 'v1$uxboole$u0'(sK182) | ~'v10$ulattices'('k1$ulattice2'(sK180)) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)) | ~'m1$usubset$u1'(sK182,'k1$uzfmisc$u1'('u1$ustruct$u0'('k1$ulattice2'(sK180)))), inference(superposition, [status(thm)], [d60,d52])).
% 19.16/4.58 cnf(d62, plain, ~'l3$ulattices'('k1$ulattice2'(sK180)) | ~'r2$uhidden'(sK181,sK182) | 'v1$uxboole$u0'(sK182) | ~'v10$ulattices'('k1$ulattice2'(sK180)) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)) | ~'m1$usubset$u1'(sK182,'k1$uzfmisc$u1'('u1$ustruct$u0'('k1$ulattice2'(sK180)))) | 'r1$utarski'('k18$ufilter$u2'(sK180,sK181),'k19$ufilter$u2'(sK180,sK182)), inference(demodulation, [status(thm)], [d61,d16])).
% 19.16/4.58 cnf(d63, plain, ~'l3$ulattices'('k1$ulattice2'(sK180)) | ~'r2$uhidden'(sK181,sK182) | ~'v10$ulattices'('k1$ulattice2'(sK180)) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)) | ~'m1$usubset$u1'(sK182,'k1$uzfmisc$u1'('u1$ustruct$u0'('k1$ulattice2'(sK180)))) | 'r1$utarski'('k18$ufilter$u2'(sK180,sK181),'k19$ufilter$u2'(sK180,sK182)), inference(resolution, [status(thm)], [c189,d62])).
% 19.16/4.58 cnf(d64, plain, ~'l3$ulattices'('k1$ulattice2'(sK180)) | ~'v10$ulattices'('k1$ulattice2'(sK180)) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)) | ~'m1$usubset$u1'(sK182,'k1$uzfmisc$u1'('u1$ustruct$u0'('k1$ulattice2'(sK180)))) | 'r1$utarski'('k18$ufilter$u2'(sK180,sK181),'k19$ufilter$u2'(sK180,sK182)), inference(resolution, [status(thm)], [c191,d63])).
% 19.16/4.58 cnf(d65, plain, ~'l3$ulattices'('k1$ulattice2'(sK180)) | ~'v10$ulattices'('k1$ulattice2'(sK180)) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)) | ~'m1$usubset$u1'(sK182,'k1$uzfmisc$u1'('u1$ustruct$u0'('k1$ulattice2'(sK180)))), inference(resolution, [status(thm)], [c192,d64])).
% 19.16/4.58 cnf(d66, plain, ~'l3$ulattices'('k1$ulattice2'(sK180)) | ~'v10$ulattices'('k1$ulattice2'(sK180)) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)), inference(resolution, [status(thm)], [d8,d65])).
% 19.16/4.58 cnf(d67, plain, ~'l3$ulattices'('k1$ulattice2'(sK180)) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)) | ~'Ts100'(sK180), inference(resolution, [status(thm)], [d66,c108])).
% 19.16/4.58 cnf(d68, plain, ~'l3$ulattices'('k1$ulattice2'(sK180)) | 'v3$ustruct$u0'('k1$ulattice2'(sK180)), inference(resolution, [status(thm)], [d30,d67])).
% 19.16/4.58 cnf(d69, plain, 'v3$ustruct$u0'('k1$ulattice2'(sK180)) | ~'l3$ulattices'(sK180), inference(resolution, [status(thm)], [d68,c28])).
% 19.16/4.58 cnf(d70, plain, 'v3$ustruct$u0'('k1$ulattice2'(sK180)), inference(resolution, [status(thm)], [c187,d69])).
% 19.16/4.58 cnf(d71, plain, ~'Ts100'(sK180), inference(resolution, [status(thm)], [d70,c100])).
% 19.16/4.58 cnf(d72, plain, $false, inference(resolution, [status(thm)], [d30,d71])).
% 19.16/4.58 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------