%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : LAT301+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 : 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 07:48:12 AM UTC 2026
% Result : Theorem 16.14s 3.19s
% Output : CNFRefutation 16.14s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT301+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.11/0.36 % Computer : n016.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Fri Sep 25 20:42:30 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 16.14/3.19 % SZS status Theorem for theBenchmark.p
% 16.14/3.19 % SZS output start CNFRefutation for theBenchmark.p
% 16.14/3.19 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))))).
% 16.14/3.19 fof(dt_k15_filter_2, axiom, ! [X0] : ! [X1] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & ('l3$ulattices'(X0) & 'm2$ufilter$u2'(X1,X0)))) => 'm1$ufilter$u2'('k15$ufilter$u2'(X0,X1),'k1$ulattice2'(X0))))).
% 16.14/3.19 fof(dt_k1_lattice2, axiom, ! [X0] : (('l3$ulattices'(X0) => ('v3$ulattices'('k1$ulattice2'(X0)) & 'l3$ulattices'('k1$ulattice2'(X0)))))).
% 16.14/3.19 fof(dt_m2_filter_2, axiom, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & 'l3$ulattices'(X0))) => ! [X1] : (('m2$ufilter$u2'(X1,X0) => (~'v1$uxboole$u0'(X1) & 'm2$ulattice4'(X1,X0))))))).
% 16.14/3.19 fof(dt_m2_lattice4, axiom, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & 'l3$ulattices'(X0))) => ! [X1] : (('m2$ulattice4'(X1,X0) => 'm1$usubset$u1'(X1,'k1$uzfmisc$u1'('u1$ustruct$u0'(X0)))))))).
% 16.14/3.19 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))))))))))))).
% 16.14/3.19 fof(redefinition_k15_filter_2, axiom, ! [X0] : ! [X1] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & ('l3$ulattices'(X0) & 'm2$ufilter$u2'(X1,X0)))) => 'k15$ufilter$u2'(X0,X1) = 'k7$ufilter$u2'(X0,X1)))).
% 16.14/3.19 fof(redefinition_m1_filter_2, axiom, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & 'l3$ulattices'(X0))) => ! [X1] : (('m1$ufilter$u2'(X1,X0) <=> 'm1$ufilter$u0'(X1,X0)))))).
% 16.14/3.19 fof(t12_filter_0, axiom, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & 'l3$ulattices'(X0))) => ! [X1] : (('m1$ufilter$u0'(X1,X0) => ((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & ('v14$ulattices'(X0) & 'l3$ulattices'(X0)))) => 'r2$uhidden'('k6$ulattices'(X0),X1))))))).
% 16.14/3.19 fof(t63_lattice2, axiom, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & 'l3$ulattices'(X0))) => ('v13$ulattices'(X0) <=> 'v14$ulattices'('k1$ulattice2'(X0)))))).
% 16.14/3.19 fof(t78_lattice2, axiom, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & ('v13$ulattices'(X0) & 'l3$ulattices'(X0)))) => 'k5$ulattices'(X0) = 'k6$ulattices'('k1$ulattice2'(X0))))).
% 16.14/3.19 fof(t25_filter_2, conjecture, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & 'l3$ulattices'(X0))) => ! [X1] : (('m2$ufilter$u2'(X1,X0) => ('v13$ulattices'(X0) => 'r2$uhidden'('k5$ulattices'(X0),X1))))))).
% 16.14/3.19 fof(negated_conjecture, negated_conjecture, ~! [X0] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & 'l3$ulattices'(X0))) => ! [X1] : (('m2$ufilter$u2'(X1,X0) => ('v13$ulattices'(X0) => 'r2$uhidden'('k5$ulattices'(X0),X1)))))), inference(negate_conjecture, [status(cth)], [t25_filter_2])).
% 16.14/3.19 cnf(c23, plain, ~'v10$ulattices'(X0) | ~'m1$usubset$u1'(X1,'k1$uzfmisc$u1'('u1$ustruct$u0'(X0))) | 'v3$ustruct$u0'(X0) | 'k7$ufilter$u2'(X0,X1) = X1 | ~'l3$ulattices'(X0), inference(clausification, [status(esa)], [d6_filter_2])).
% 16.14/3.19 cnf(c26, plain, ~'v10$ulattices'(X0) | 'm1$ufilter$u2'('k15$ufilter$u2'(X0,X1),'k1$ulattice2'(X0)) | 'v3$ustruct$u0'(X0) | ~'m2$ufilter$u2'(X1,X0) | ~'l3$ulattices'(X0), inference(clausification, [status(esa)], [dt_k15_filter_2])).
% 16.14/3.19 cnf(c28, plain, ~'l3$ulattices'(X0) | 'l3$ulattices'('k1$ulattice2'(X0)), inference(clausification, [status(esa)], [dt_k1_lattice2])).
% 16.14/3.19 cnf(c41, plain, ~'m2$ufilter$u2'(X0,X1) | ~'l3$ulattices'(X1) | 'v3$ustruct$u0'(X1) | 'm2$ulattice4'(X0,X1) | ~'v10$ulattices'(X1), inference(clausification, [status(esa)], [dt_m2_filter_2])).
% 16.14/3.19 cnf(c42, plain, ~'v10$ulattices'(X0) | 'm1$usubset$u1'(X1,'k1$uzfmisc$u1'('u1$ustruct$u0'(X0))) | 'v3$ustruct$u0'(X0) | ~'l3$ulattices'(X0) | ~'m2$ulattice4'(X1,X0), inference(clausification, [status(esa)], [dt_m2_lattice4])).
% 16.14/3.19 cnf(c94, plain, 'v3$ustruct$u0'(X0) | ~'v10$ulattices'(X0) | ~'l3$ulattices'(X0) | X1(X0), inference(clausification, [status(esa)], [fc6_lattice2])).
% 16.14/3.19 cnf(c95, plain, ~X0(X1) | ~'v3$ustruct$u0'('k1$ulattice2'(X1)), inference(clausification, [status(esa)], [fc6_lattice2])).
% 16.14/3.19 cnf(c103, plain, ~X0(X1) | 'v10$ulattices'('k1$ulattice2'(X1)), inference(clausification, [status(esa)], [fc6_lattice2])).
% 16.14/3.19 cnf(c155, plain, ~'l3$ulattices'(X0) | 'k15$ufilter$u2'(X0,X1) = 'k7$ufilter$u2'(X0,X1) | ~'m2$ufilter$u2'(X1,X0) | ~'v10$ulattices'(X0) | 'v3$ustruct$u0'(X0), inference(clausification, [status(esa)], [redefinition_k15_filter_2])).
% 16.14/3.19 cnf(c156, plain, 'v3$ustruct$u0'(X0) | ~'l3$ulattices'(X0) | ~'m1$ufilter$u2'(X1,X0) | 'm1$ufilter$u0'(X1,X0) | ~'v10$ulattices'(X0), inference(clausification, [status(esa)], [redefinition_m1_filter_2])).
% 16.14/3.19 cnf(c161, plain, ~'l3$ulattices'(X0) | ~'v14$ulattices'(X0) | 'v3$ustruct$u0'(X0) | ~'v10$ulattices'(X0) | 'r2$uhidden'('k6$ulattices'(X0),X1) | ~'m1$ufilter$u0'(X1,X0), inference(clausification, [status(esa)], [t12_filter_0])).
% 16.14/3.19 cnf(c168, plain, ~'l3$ulattices'(X0) | 'v14$ulattices'('k1$ulattice2'(X0)) | ~'v10$ulattices'(X0) | 'v3$ustruct$u0'(X0) | ~'v13$ulattices'(X0), inference(clausification, [status(esa)], [t63_lattice2])).
% 16.14/3.19 cnf(c171, plain, ~'l3$ulattices'(X0) | ~'v13$ulattices'(X0) | 'v3$ustruct$u0'(X0) | 'k5$ulattices'(X0) = 'k6$ulattices'('k1$ulattice2'(X0)) | ~'v10$ulattices'(X0), inference(clausification, [status(esa)], [t78_lattice2])).
% 16.14/3.19 cnf(c174, plain, ~'v3$ustruct$u0'(sK136), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.14/3.19 cnf(c175, plain, 'v10$ulattices'(sK136), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.14/3.19 cnf(c176, plain, 'l3$ulattices'(sK136), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.14/3.19 cnf(c177, plain, 'm2$ufilter$u2'(sK137,sK136), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.14/3.19 cnf(c178, plain, 'v13$ulattices'(sK136), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.14/3.19 cnf(c179, plain, ~'r2$uhidden'('k5$ulattices'(sK136),sK137), inference(clausification, [status(esa)], [negated_conjecture])).
% 16.14/3.19 cnf(d0, plain, ~'l3$ulattices'(sK136) | ~'v10$ulattices'(sK136) | 'v3$ustruct$u0'(sK136) | 'm2$ulattice4'(sK137,sK136), inference(resolution, [status(thm)], [c41,c177])).
% 16.14/3.19 cnf(d1, plain, ~'l3$ulattices'(sK136) | ~'v10$ulattices'(sK136) | 'm2$ulattice4'(sK137,sK136), inference(resolution, [status(thm)], [c174,d0])).
% 16.14/3.19 cnf(d2, plain, ~'l3$ulattices'(sK136) | 'm2$ulattice4'(sK137,sK136), inference(resolution, [status(thm)], [c175,d1])).
% 16.14/3.19 cnf(d3, plain, 'm2$ulattice4'(sK137,sK136), inference(resolution, [status(thm)], [c176,d2])).
% 16.14/3.19 cnf(d4, plain, ~'l3$ulattices'(X0) | ~'v10$ulattices'(X0) | 'v3$ustruct$u0'(X0) | ~'m2$ulattice4'(X1,X0) | 'k7$ufilter$u2'(X0,X1) = X1 | ~'l3$ulattices'(X0) | ~'v10$ulattices'(X0) | 'v3$ustruct$u0'(X0), inference(resolution, [status(thm)], [c42,c23])).
% 16.14/3.19 cnf(d5, plain, 'k7$ufilter$u2'(sK136,sK137) = sK137 | ~'l3$ulattices'(sK136) | ~'v10$ulattices'(sK136) | 'v3$ustruct$u0'(sK136), inference(resolution, [status(thm)], [d4,d3])).
% 16.14/3.19 cnf(d6, plain, 'k7$ufilter$u2'(sK136,sK137) = sK137 | ~'l3$ulattices'(sK136) | ~'v10$ulattices'(sK136), inference(resolution, [status(thm)], [c174,d5])).
% 16.14/3.19 cnf(d7, plain, 'k7$ufilter$u2'(sK136,sK137) = sK137 | ~'l3$ulattices'(sK136), inference(resolution, [status(thm)], [c175,d6])).
% 16.14/3.19 cnf(d8, plain, 'k7$ufilter$u2'(sK136,sK137) = sK137, inference(resolution, [status(thm)], [c176,d7])).
% 16.14/3.19 cnf(d9, plain, 'k15$ufilter$u2'(sK136,sK137) = 'k7$ufilter$u2'(sK136,sK137) | ~'l3$ulattices'(sK136) | ~'v10$ulattices'(sK136) | 'v3$ustruct$u0'(sK136), inference(resolution, [status(thm)], [c155,c177])).
% 16.14/3.19 cnf(d10, plain, 'k15$ufilter$u2'(sK136,sK137) = 'k7$ufilter$u2'(sK136,sK137) | ~'l3$ulattices'(sK136) | ~'v10$ulattices'(sK136), inference(resolution, [status(thm)], [c174,d9])).
% 16.14/3.19 cnf(d11, plain, 'k15$ufilter$u2'(sK136,sK137) = 'k7$ufilter$u2'(sK136,sK137) | ~'l3$ulattices'(sK136), inference(resolution, [status(thm)], [c175,d10])).
% 16.14/3.19 cnf(d12, plain, 'k15$ufilter$u2'(sK136,sK137) = 'k7$ufilter$u2'(sK136,sK137), inference(resolution, [status(thm)], [c176,d11])).
% 16.14/3.19 cnf(d13, plain, 'm1$ufilter$u2'('k7$ufilter$u2'(sK136,sK137),'k1$ulattice2'(sK136)) | ~'l3$ulattices'(sK136) | ~'v10$ulattices'(sK136) | 'v3$ustruct$u0'(sK136) | ~'m2$ufilter$u2'(sK137,sK136), inference(superposition, [status(thm)], [d12,c26])).
% 16.14/3.19 cnf(d14, plain, ~'l3$ulattices'(sK136) | ~'v10$ulattices'(sK136) | ~'m2$ufilter$u2'(sK137,sK136) | 'm1$ufilter$u2'('k7$ufilter$u2'(sK136,sK137),'k1$ulattice2'(sK136)), inference(resolution, [status(thm)], [c174,d13])).
% 16.14/3.19 cnf(d15, plain, ~'l3$ulattices'(sK136) | ~'m2$ufilter$u2'(sK137,sK136) | 'm1$ufilter$u2'('k7$ufilter$u2'(sK136,sK137),'k1$ulattice2'(sK136)), inference(resolution, [status(thm)], [c175,d14])).
% 16.14/3.19 cnf(d16, plain, ~'m2$ufilter$u2'(sK137,sK136) | 'm1$ufilter$u2'('k7$ufilter$u2'(sK136,sK137),'k1$ulattice2'(sK136)), inference(resolution, [status(thm)], [c176,d15])).
% 16.14/3.19 cnf(d17, plain, 'm1$ufilter$u2'('k7$ufilter$u2'(sK136,sK137),'k1$ulattice2'(sK136)), inference(resolution, [status(thm)], [c177,d16])).
% 16.14/3.19 cnf(d18, plain, ~'l3$ulattices'('k1$ulattice2'(sK136)) | ~'v10$ulattices'('k1$ulattice2'(sK136)) | 'v3$ustruct$u0'('k1$ulattice2'(sK136)) | 'm1$ufilter$u0'('k7$ufilter$u2'(sK136,sK137),'k1$ulattice2'(sK136)), inference(resolution, [status(thm)], [d17,c156])).
% 16.14/3.19 cnf(d19, plain, 'k5$ulattices'(sK136) = 'k6$ulattices'('k1$ulattice2'(sK136)) | ~'l3$ulattices'(sK136) | ~'v10$ulattices'(sK136) | 'v3$ustruct$u0'(sK136), inference(resolution, [status(thm)], [c171,c178])).
% 16.14/3.19 cnf(d20, plain, 'k5$ulattices'(sK136) = 'k6$ulattices'('k1$ulattice2'(sK136)) | ~'l3$ulattices'(sK136) | ~'v10$ulattices'(sK136), inference(resolution, [status(thm)], [c174,d19])).
% 16.14/3.19 cnf(d21, plain, 'k5$ulattices'(sK136) = 'k6$ulattices'('k1$ulattice2'(sK136)) | ~'l3$ulattices'(sK136), inference(resolution, [status(thm)], [c175,d20])).
% 16.14/3.19 cnf(d22, plain, 'k5$ulattices'(sK136) = 'k6$ulattices'('k1$ulattice2'(sK136)), inference(resolution, [status(thm)], [c176,d21])).
% 16.14/3.19 cnf(d23, plain, 'r2$uhidden'('k5$ulattices'(sK136),X0) | ~'l3$ulattices'('k1$ulattice2'(sK136)) | ~'v10$ulattices'('k1$ulattice2'(sK136)) | 'v3$ustruct$u0'('k1$ulattice2'(sK136)) | ~'v14$ulattices'('k1$ulattice2'(sK136)) | ~'m1$ufilter$u0'(X0,'k1$ulattice2'(sK136)), inference(superposition, [status(thm)], [d22,c161])).
% 16.14/3.19 cnf(d24, plain, ~'l3$ulattices'('k1$ulattice2'(sK136)) | 'r2$uhidden'('k5$ulattices'(sK136),'k7$ufilter$u2'(sK136,sK137)) | ~'v10$ulattices'('k1$ulattice2'(sK136)) | 'v3$ustruct$u0'('k1$ulattice2'(sK136)) | ~'v14$ulattices'('k1$ulattice2'(sK136)) | ~'l3$ulattices'('k1$ulattice2'(sK136)) | ~'v10$ulattices'('k1$ulattice2'(sK136)) | 'v3$ustruct$u0'('k1$ulattice2'(sK136)), inference(resolution, [status(thm)], [d23,d18])).
% 16.14/3.19 cnf(d25, plain, ~'l3$ulattices'('k1$ulattice2'(sK136)) | 'r2$uhidden'('k5$ulattices'(sK136),sK137) | ~'v10$ulattices'('k1$ulattice2'(sK136)) | 'v3$ustruct$u0'('k1$ulattice2'(sK136)) | ~'v14$ulattices'('k1$ulattice2'(sK136)), inference(demodulation, [status(thm)], [d24,d8])).
% 16.14/3.19 cnf(d26, plain, ~'l3$ulattices'('k1$ulattice2'(sK136)) | ~'v10$ulattices'('k1$ulattice2'(sK136)) | 'v3$ustruct$u0'('k1$ulattice2'(sK136)) | ~'v14$ulattices'('k1$ulattice2'(sK136)), inference(resolution, [status(thm)], [c179,d25])).
% 16.14/3.19 cnf(d27, plain, ~'l3$ulattices'('k1$ulattice2'(sK136)) | ~'v10$ulattices'('k1$ulattice2'(sK136)) | 'v3$ustruct$u0'('k1$ulattice2'(sK136)) | ~'l3$ulattices'(sK136) | ~'v10$ulattices'(sK136) | 'v3$ustruct$u0'(sK136) | ~'v13$ulattices'(sK136), inference(resolution, [status(thm)], [d26,c168])).
% 16.14/3.19 cnf(d28, plain, ~'l3$ulattices'('k1$ulattice2'(sK136)) | ~'l3$ulattices'(sK136) | ~'v10$ulattices'('k1$ulattice2'(sK136)) | ~'v10$ulattices'(sK136) | 'v3$ustruct$u0'('k1$ulattice2'(sK136)) | ~'v13$ulattices'(sK136), inference(resolution, [status(thm)], [c174,d27])).
% 16.14/3.19 cnf(d29, plain, ~'l3$ulattices'('k1$ulattice2'(sK136)) | ~'l3$ulattices'(sK136) | ~'v10$ulattices'('k1$ulattice2'(sK136)) | 'v3$ustruct$u0'('k1$ulattice2'(sK136)) | ~'v13$ulattices'(sK136), inference(resolution, [status(thm)], [c175,d28])).
% 16.14/3.19 cnf(d30, plain, ~'l3$ulattices'('k1$ulattice2'(sK136)) | ~'v10$ulattices'('k1$ulattice2'(sK136)) | 'v3$ustruct$u0'('k1$ulattice2'(sK136)) | ~'v13$ulattices'(sK136), inference(resolution, [status(thm)], [c176,d29])).
% 16.14/3.19 cnf(d31, plain, ~'l3$ulattices'('k1$ulattice2'(sK136)) | ~'v10$ulattices'('k1$ulattice2'(sK136)) | 'v3$ustruct$u0'('k1$ulattice2'(sK136)), inference(resolution, [status(thm)], [c178,d30])).
% 16.14/3.19 cnf(d32, plain, ~'l3$ulattices'('k1$ulattice2'(sK136)) | 'v3$ustruct$u0'('k1$ulattice2'(sK136)) | ~'Ts80'(sK136), inference(resolution, [status(thm)], [d31,c103])).
% 16.14/3.19 cnf(d33, plain, ~'l3$ulattices'(sK136) | 'v3$ustruct$u0'(sK136) | 'Ts80'(sK136), inference(resolution, [status(thm)], [c94,c175])).
% 16.14/3.19 cnf(d34, plain, ~'l3$ulattices'(sK136) | 'Ts80'(sK136), inference(resolution, [status(thm)], [c174,d33])).
% 16.14/3.19 cnf(d35, plain, 'Ts80'(sK136), inference(resolution, [status(thm)], [c176,d34])).
% 16.14/3.19 cnf(d36, plain, ~'l3$ulattices'('k1$ulattice2'(sK136)) | 'v3$ustruct$u0'('k1$ulattice2'(sK136)), inference(resolution, [status(thm)], [d35,d32])).
% 16.14/3.19 cnf(d37, plain, 'v3$ustruct$u0'('k1$ulattice2'(sK136)) | ~'l3$ulattices'(sK136), inference(resolution, [status(thm)], [d36,c28])).
% 16.14/3.19 cnf(d38, plain, 'v3$ustruct$u0'('k1$ulattice2'(sK136)), inference(resolution, [status(thm)], [c176,d37])).
% 16.14/3.19 cnf(d39, plain, ~'Ts80'(sK136), inference(resolution, [status(thm)], [d38,c95])).
% 16.14/3.19 cnf(d40, plain, $false, inference(resolution, [status(thm)], [d35,d39])).
% 16.14/3.19 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------