%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : LAT346+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 : n017.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:25 AM UTC 2026
% Result : Theorem 58.50s 10.36s
% Output : CNFRefutation 58.50s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT346+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.10/0.37 % Computer : n017.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 : Fri Sep 25 21:03:03 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 58.50/10.36 % SZS status Theorem for theBenchmark.p
% 58.50/10.36 % SZS output start CNFRefutation for theBenchmark.p
% 58.50/10.36 fof(d5_lattice4, axiom, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & 'l3$ulattices'(X0))) => ! [X1] : (((~'v3$ustruct$u0'(X1) & ('v10$ulattices'(X1) & 'l3$ulattices'(X1))) => ('r1$ufilter$u1'(X0,X1) <=> ? [X2] : (('m1$ulattice4'(X2,X0,X1) & 'v3$ulattice4'(X2,X0,X1))))))))).
% 58.50/10.36 fof(d7_conlat_2, axiom, ! [X0] : (((~'v3$uconlat$u1'(X0) & 'l2$uconlat$u1'(X0)) => 'k7$uconlat$u2'(X0) = 'g2$uconlat$u1'('u2$uconlat$u1'(X0),'u1$uconlat$u1'(X0),'k6$urelset$u1'('u1$uconlat$u1'(X0),'u2$uconlat$u1'(X0),'u3$uconlat$u1'(X0)))))).
% 58.50/10.36 fof(dt_g2_conlat_1, axiom, ! [X0] : ! [X1] : ! [X2] : (('m1$urelset$u1'(X2,X0,X1) => ('v4$uconlat$u1'('g2$uconlat$u1'(X0,X1,X2)) & 'l2$uconlat$u1'('g2$uconlat$u1'(X0,X1,X2)))))).
% 58.50/10.36 fof(dt_k10_conlat_2, axiom, ! [X0] : (((~'v3$uconlat$u1'(X0) & 'l2$uconlat$u1'(X0)) => 'm1$ulattice4'('k10$uconlat$u2'(X0),'k1$ulattice2'('k11$uconlat$u1'(X0)),'k11$uconlat$u1'('k7$uconlat$u2'(X0)))))).
% 58.50/10.36 fof(dt_k11_conlat_1, axiom, ! [X0] : (((~'v3$uconlat$u1'(X0) & 'l2$uconlat$u1'(X0)) => (~'v3$ustruct$u0'('k11$uconlat$u1'(X0)) & ('v3$ulattices'('k11$uconlat$u1'(X0)) & 'l3$ulattices'('k11$uconlat$u1'(X0))))))).
% 58.50/10.36 fof(dt_k1_lattice2, axiom, ! [X0] : (('l3$ulattices'(X0) => ('v3$ulattices'('k1$ulattice2'(X0)) & 'l3$ulattices'('k1$ulattice2'(X0)))))).
% 58.50/10.36 fof(dt_k6_relset_1, axiom, ! [X0] : ! [X1] : ! [X2] : (('m1$urelset$u1'(X2,X0,X1) => 'm2$urelset$u1'('k6$urelset$u1'(X0,X1,X2),X1,X0)))).
% 58.50/10.36 fof(dt_k7_conlat_2, axiom, ! [X0] : (((~'v3$uconlat$u1'(X0) & 'l2$uconlat$u1'(X0)) => (~'v3$uconlat$u1'('k7$uconlat$u2'(X0)) & ('v4$uconlat$u1'('k7$uconlat$u2'(X0)) & 'l2$uconlat$u1'('k7$uconlat$u2'(X0))))))).
% 58.50/10.36 fof(dt_u3_conlat_1, axiom, ! [X0] : (('l2$uconlat$u1'(X0) => 'm2$urelset$u1'('u3$uconlat$u1'(X0),'u1$uconlat$u1'(X0),'u2$uconlat$u1'(X0))))).
% 58.50/10.36 fof(fc1_conlat_2, axiom, ! [X0] : (((~'v3$uconlat$u1'(X0) & 'l2$uconlat$u1'(X0)) => (~'v3$ustruct$u0'('k11$uconlat$u1'(X0)) & ('v3$ulattices'('k11$uconlat$u1'(X0)) & ('v4$ulattices'('k11$uconlat$u1'(X0)) & ('v5$ulattices'('k11$uconlat$u1'(X0)) & ('v6$ulattices'('k11$uconlat$u1'(X0)) & ('v7$ulattices'('k11$uconlat$u1'(X0)) & ('v8$ulattices'('k11$uconlat$u1'(X0)) & ('v9$ulattices'('k11$uconlat$u1'(X0)) & ('v10$ulattices'('k11$uconlat$u1'(X0)) & ('v13$ulattices'('k11$uconlat$u1'(X0)) & ('v14$ulattices'('k11$uconlat$u1'(X0)) & ('v15$ulattices'('k11$uconlat$u1'(X0)) & 'v4$ulattice3'('k11$uconlat$u1'(X0))))))))))))))))).
% 58.50/10.36 fof(fc2_conlat_2, axiom, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & ('v4$ulattice3'(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)) & 'v4$ulattice3'('k1$ulattice2'(X0)))))))))))))).
% 58.50/10.36 fof(fc4_conlat_1, axiom, ! [X0] : (((~'v3$uconlat$u1'(X0) & 'l2$uconlat$u1'(X0)) => (~'v3$ustruct$u0'('k11$uconlat$u1'(X0)) & ('v3$ulattices'('k11$uconlat$u1'(X0)) & ('v4$ulattices'('k11$uconlat$u1'(X0)) & ('v5$ulattices'('k11$uconlat$u1'(X0)) & ('v6$ulattices'('k11$uconlat$u1'(X0)) & ('v7$ulattices'('k11$uconlat$u1'(X0)) & ('v8$ulattices'('k11$uconlat$u1'(X0)) & ('v9$ulattices'('k11$uconlat$u1'(X0)) & 'v10$ulattices'('k11$uconlat$u1'(X0))))))))))))).
% 58.50/10.36 fof(redefinition_m2_relset_1, axiom, ! [X0] : ! [X1] : ! [X2] : (('m2$urelset$u1'(X2,X0,X1) <=> 'm1$urelset$u1'(X2,X0,X1)))).
% 58.50/10.36 fof(symmetry_r1_filter_1, axiom, ! [X0] : ! [X1] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & ('l3$ulattices'(X0) & (~'v3$ustruct$u0'(X1) & ('v10$ulattices'(X1) & 'l3$ulattices'(X1)))))) => ('r1$ufilter$u1'(X0,X1) => 'r1$ufilter$u1'(X1,X0))))).
% 58.50/10.36 fof(t21_conlat_2, axiom, ! [X0] : (((~'v3$uconlat$u1'(X0) & 'l2$uconlat$u1'(X0)) => 'v3$ulattice4'('k10$uconlat$u2'(X0),'k1$ulattice2'('k11$uconlat$u1'(X0)),'k11$uconlat$u1'('k7$uconlat$u2'(X0)))))).
% 58.50/10.36 fof(t22_conlat_2, conjecture, ! [X0] : (((~'v3$uconlat$u1'(X0) & 'l2$uconlat$u1'(X0)) => 'r1$ufilter$u1'('k11$uconlat$u1'('k7$uconlat$u2'(X0)),'k1$ulattice2'('k11$uconlat$u1'(X0)))))).
% 58.50/10.36 fof(negated_conjecture, negated_conjecture, ~! [X0] : (((~'v3$uconlat$u1'(X0) & 'l2$uconlat$u1'(X0)) => 'r1$ufilter$u1'('k11$uconlat$u1'('k7$uconlat$u2'(X0)),'k1$ulattice2'('k11$uconlat$u1'(X0))))), inference(negate_conjecture, [status(cth)], [t22_conlat_2])).
% 58.50/10.36 cnf(c30, plain, ~'m1$ulattice4'(X0,X1,X2) | 'v3$ustruct$u0'(X1) | ~'v10$ulattices'(X1) | ~'l3$ulattices'(X2) | ~'v3$ulattice4'(X0,X1,X2) | ~'l3$ulattices'(X1) | ~'v10$ulattices'(X2) | 'v3$ustruct$u0'(X2) | 'r1$ufilter$u1'(X1,X2), inference(clausification, [status(esa)], [d5_lattice4])).
% 58.50/10.36 cnf(c31, plain, ~'l2$uconlat$u1'(X0) | 'v3$uconlat$u1'(X0) | 'g2$uconlat$u1'('u2$uconlat$u1'(X0),'u1$uconlat$u1'(X0),'k6$urelset$u1'('u1$uconlat$u1'(X0),'u2$uconlat$u1'(X0),'u3$uconlat$u1'(X0))) = 'k7$uconlat$u2'(X0), inference(clausification, [status(esa)], [d7_conlat_2])).
% 58.50/10.36 cnf(c33, plain, ~'m1$urelset$u1'(X0,X1,X2) | 'l2$uconlat$u1'('g2$uconlat$u1'(X1,X2,X0)), inference(clausification, [status(esa)], [dt_g2_conlat_1])).
% 58.50/10.36 cnf(c36, plain, ~'l2$uconlat$u1'(X0) | 'v3$uconlat$u1'(X0) | 'm1$ulattice4'('k10$uconlat$u2'(X0),'k1$ulattice2'('k11$uconlat$u1'(X0)),'k11$uconlat$u1'('k7$uconlat$u2'(X0))), inference(clausification, [status(esa)], [dt_k10_conlat_2])).
% 58.50/10.36 cnf(c38, plain, ~'l2$uconlat$u1'(X0) | 'v3$uconlat$u1'(X0) | 'l3$ulattices'('k11$uconlat$u1'(X0)), inference(clausification, [status(esa)], [dt_k11_conlat_1])).
% 58.50/10.36 cnf(c41, plain, ~'l3$ulattices'(X0) | 'l3$ulattices'('k1$ulattice2'(X0)), inference(clausification, [status(esa)], [dt_k1_lattice2])).
% 58.50/10.36 cnf(c43, plain, ~'m1$urelset$u1'(X0,X1,X2) | 'm2$urelset$u1'('k6$urelset$u1'(X1,X2,X0),X2,X1), inference(clausification, [status(esa)], [dt_k6_relset_1])).
% 58.50/10.36 cnf(c44, plain, ~'l2$uconlat$u1'(X0) | 'v3$uconlat$u1'(X0) | ~'v3$uconlat$u1'('k7$uconlat$u2'(X0)), inference(clausification, [status(esa)], [dt_k7_conlat_2])).
% 58.50/10.36 cnf(c62, plain, ~'l2$uconlat$u1'(X0) | 'm2$urelset$u1'('u3$uconlat$u1'(X0),'u1$uconlat$u1'(X0),'u2$uconlat$u1'(X0)), inference(clausification, [status(esa)], [dt_u3_conlat_1])).
% 58.50/10.36 cnf(c74, plain, ~'l2$uconlat$u1'(X0) | 'v3$uconlat$u1'(X0) | X1(X0), inference(clausification, [status(esa)], [fc1_conlat_2])).
% 58.50/10.36 cnf(c75, plain, ~X0(X1) | ~'v3$ustruct$u0'('k11$uconlat$u1'(X1)), inference(clausification, [status(esa)], [fc1_conlat_2])).
% 58.50/10.36 cnf(c79, plain, ~X0(X1) | 'v10$ulattices'('k11$uconlat$u1'(X1)), inference(clausification, [status(esa)], [fc1_conlat_2])).
% 58.50/10.36 cnf(c81, plain, ~X0(X1) | 'v4$ulattice3'('k11$uconlat$u1'(X1)), inference(clausification, [status(esa)], [fc1_conlat_2])).
% 58.50/10.36 cnf(c94, plain, ~'v10$ulattices'(X0) | X1(X0) | ~'l3$ulattices'(X0) | 'v3$ustruct$u0'(X0) | ~'v4$ulattice3'(X0), inference(clausification, [status(esa)], [fc2_conlat_2])).
% 58.50/10.36 cnf(c95, plain, ~X0(X1) | ~'v3$ustruct$u0'('k1$ulattice2'(X1)), inference(clausification, [status(esa)], [fc2_conlat_2])).
% 58.50/10.36 cnf(c99, plain, ~X0(X1) | 'v10$ulattices'('k1$ulattice2'(X1)), inference(clausification, [status(esa)], [fc2_conlat_2])).
% 58.50/10.36 cnf(c119, plain, ~'l2$uconlat$u1'(X0) | 'v3$uconlat$u1'(X0) | X1(X0), inference(clausification, [status(esa)], [fc4_conlat_1])).
% 58.50/10.36 cnf(c120, plain, ~X0(X1) | ~'v3$ustruct$u0'('k11$uconlat$u1'(X1)), inference(clausification, [status(esa)], [fc4_conlat_1])).
% 58.50/10.36 cnf(c124, plain, ~X0(X1) | 'v10$ulattices'('k11$uconlat$u1'(X1)), inference(clausification, [status(esa)], [fc4_conlat_1])).
% 58.50/10.36 cnf(c226, plain, ~'m2$urelset$u1'(X0,X1,X2) | 'm1$urelset$u1'(X0,X1,X2), inference(clausification, [status(esa)], [redefinition_m2_relset_1])).
% 58.50/10.36 cnf(c230, plain, ~'v10$ulattices'(X0) | 'r1$ufilter$u1'(X0,X1) | ~'r1$ufilter$u1'(X1,X0) | 'v3$ustruct$u0'(X1) | ~'l3$ulattices'(X1) | ~'v10$ulattices'(X1) | 'v3$ustruct$u0'(X0) | ~'l3$ulattices'(X0), inference(clausification, [status(esa)], [symmetry_r1_filter_1])).
% 58.50/10.36 cnf(c232, plain, ~'l2$uconlat$u1'(X0) | 'v3$uconlat$u1'(X0) | 'v3$ulattice4'('k10$uconlat$u2'(X0),'k1$ulattice2'('k11$uconlat$u1'(X0)),'k11$uconlat$u1'('k7$uconlat$u2'(X0))), inference(clausification, [status(esa)], [t21_conlat_2])).
% 58.50/10.36 cnf(c241, plain, 'l2$uconlat$u1'(sK169), inference(clausification, [status(esa)], [negated_conjecture])).
% 58.50/10.36 cnf(c242, plain, ~'v3$uconlat$u1'(sK169), inference(clausification, [status(esa)], [negated_conjecture])).
% 58.50/10.36 cnf(c243, plain, ~'r1$ufilter$u1'('k11$uconlat$u1'('k7$uconlat$u2'(sK169)),'k1$ulattice2'('k11$uconlat$u1'(sK169))), inference(clausification, [status(esa)], [negated_conjecture])).
% 58.50/10.36 cnf(d0, plain, ~'l3$ulattices'('k11$uconlat$u1'(X0)) | ~'v10$ulattices'('k11$uconlat$u1'(X0)) | 'v3$ustruct$u0'('k11$uconlat$u1'(X0)) | 'Ts77'('k11$uconlat$u1'(X0)) | ~'Ts71'(X0), inference(resolution, [status(thm)], [c94,c81])).
% 58.50/10.36 cnf(d1, plain, ~'Ts71'(X0) | ~'l3$ulattices'('k11$uconlat$u1'(X0)) | ~'v10$ulattices'('k11$uconlat$u1'(X0)) | ~'Ts71'(X0) | 'Ts77'('k11$uconlat$u1'(X0)), inference(resolution, [status(thm)], [c75,d0])).
% 58.50/10.36 cnf(d2, plain, ~'Ts71'(X0) | ~'l3$ulattices'('k11$uconlat$u1'(X0)) | ~'Ts71'(X0) | 'Ts77'('k11$uconlat$u1'(X0)), inference(resolution, [status(thm)], [c79,d1])).
% 58.50/10.36 cnf(d3, plain, ~'Ts71'(X0) | 'Ts77'('k11$uconlat$u1'(X0)) | ~'l2$uconlat$u1'(X0) | 'v3$uconlat$u1'(X0), inference(resolution, [status(thm)], [d2,c38])).
% 58.50/10.36 cnf(d4, plain, ~'l2$uconlat$u1'(X0) | 'v3$uconlat$u1'(X0) | ~'l2$uconlat$u1'(X0) | 'v3$uconlat$u1'(X0) | 'Ts77'('k11$uconlat$u1'(X0)), inference(resolution, [status(thm)], [c74,d3])).
% 58.50/10.36 cnf(d5, plain, ~'l2$uconlat$u1'(X0) | 'v3$uconlat$u1'(X0) | ~'l3$ulattices'('k1$ulattice2'('k11$uconlat$u1'(X0))) | ~'l3$ulattices'('k11$uconlat$u1'('k7$uconlat$u2'(X0))) | ~'v10$ulattices'('k1$ulattice2'('k11$uconlat$u1'(X0))) | ~'v10$ulattices'('k11$uconlat$u1'('k7$uconlat$u2'(X0))) | 'v3$ustruct$u0'('k1$ulattice2'('k11$uconlat$u1'(X0))) | 'v3$ustruct$u0'('k11$uconlat$u1'('k7$uconlat$u2'(X0))) | 'r1$ufilter$u1'('k1$ulattice2'('k11$uconlat$u1'(X0)),'k11$uconlat$u1'('k7$uconlat$u2'(X0))) | ~'m1$ulattice4'('k10$uconlat$u2'(X0),'k1$ulattice2'('k11$uconlat$u1'(X0)),'k11$uconlat$u1'('k7$uconlat$u2'(X0))), inference(resolution, [status(thm)], [c232,c30])).
% 58.50/10.36 cnf(d6, plain, ~'l2$uconlat$u1'(X0) | 'v3$uconlat$u1'(X0) | ~'l3$ulattices'('k1$ulattice2'('k11$uconlat$u1'(X0))) | ~'l3$ulattices'('k11$uconlat$u1'('k7$uconlat$u2'(X0))) | ~'l2$uconlat$u1'(X0) | ~'v10$ulattices'('k1$ulattice2'('k11$uconlat$u1'(X0))) | ~'v10$ulattices'('k11$uconlat$u1'('k7$uconlat$u2'(X0))) | 'v3$ustruct$u0'('k1$ulattice2'('k11$uconlat$u1'(X0))) | 'v3$ustruct$u0'('k11$uconlat$u1'('k7$uconlat$u2'(X0))) | 'r1$ufilter$u1'('k1$ulattice2'('k11$uconlat$u1'(X0)),'k11$uconlat$u1'('k7$uconlat$u2'(X0))) | 'v3$uconlat$u1'(X0), inference(resolution, [status(thm)], [c36,d5])).
% 58.50/10.36 cnf(d7, plain, ~'l3$ulattices'('k1$ulattice2'('k11$uconlat$u1'(X0))) | ~'l3$ulattices'('k11$uconlat$u1'('k7$uconlat$u2'(X0))) | ~'l2$uconlat$u1'(X0) | ~'v10$ulattices'('k1$ulattice2'('k11$uconlat$u1'(X0))) | ~'v10$ulattices'('k11$uconlat$u1'('k7$uconlat$u2'(X0))) | 'v3$ustruct$u0'('k1$ulattice2'('k11$uconlat$u1'(X0))) | 'v3$ustruct$u0'('k11$uconlat$u1'('k7$uconlat$u2'(X0))) | 'v3$uconlat$u1'(X0) | ~'l3$ulattices'('k11$uconlat$u1'('k7$uconlat$u2'(X0))) | ~'l3$ulattices'('k1$ulattice2'('k11$uconlat$u1'(X0))) | ~'v10$ulattices'('k11$uconlat$u1'('k7$uconlat$u2'(X0))) | ~'v10$ulattices'('k1$ulattice2'('k11$uconlat$u1'(X0))) | 'v3$ustruct$u0'('k11$uconlat$u1'('k7$uconlat$u2'(X0))) | 'v3$ustruct$u0'('k1$ulattice2'('k11$uconlat$u1'(X0))) | 'r1$ufilter$u1'('k11$uconlat$u1'('k7$uconlat$u2'(X0)),'k1$ulattice2'('k11$uconlat$u1'(X0))), inference(resolution, [status(thm)], [d6,c230])).
% 58.50/10.36 cnf(d8, plain, ~'l3$ulattices'('k1$ulattice2'('k11$uconlat$u1'(sK169))) | ~'l3$ulattices'('k11$uconlat$u1'('k7$uconlat$u2'(sK169))) | ~'l2$uconlat$u1'(sK169) | ~'v10$ulattices'('k1$ulattice2'('k11$uconlat$u1'(sK169))) | ~'v10$ulattices'('k11$uconlat$u1'('k7$uconlat$u2'(sK169))) | 'v3$ustruct$u0'('k1$ulattice2'('k11$uconlat$u1'(sK169))) | 'v3$ustruct$u0'('k11$uconlat$u1'('k7$uconlat$u2'(sK169))) | 'v3$uconlat$u1'(sK169), inference(resolution, [status(thm)], [d7,c243])).
% 58.50/10.36 cnf(d9, plain, ~'l3$ulattices'('k1$ulattice2'('k11$uconlat$u1'(sK169))) | ~'l3$ulattices'('k11$uconlat$u1'('k7$uconlat$u2'(sK169))) | ~'v10$ulattices'('k1$ulattice2'('k11$uconlat$u1'(sK169))) | ~'v10$ulattices'('k11$uconlat$u1'('k7$uconlat$u2'(sK169))) | 'v3$ustruct$u0'('k1$ulattice2'('k11$uconlat$u1'(sK169))) | 'v3$ustruct$u0'('k11$uconlat$u1'('k7$uconlat$u2'(sK169))) | 'v3$uconlat$u1'(sK169), inference(resolution, [status(thm)], [c241,d8])).
% 58.50/10.36 cnf(d10, plain, ~'l3$ulattices'('k1$ulattice2'('k11$uconlat$u1'(sK169))) | ~'l3$ulattices'('k11$uconlat$u1'('k7$uconlat$u2'(sK169))) | ~'v10$ulattices'('k1$ulattice2'('k11$uconlat$u1'(sK169))) | ~'v10$ulattices'('k11$uconlat$u1'('k7$uconlat$u2'(sK169))) | 'v3$ustruct$u0'('k1$ulattice2'('k11$uconlat$u1'(sK169))) | 'v3$ustruct$u0'('k11$uconlat$u1'('k7$uconlat$u2'(sK169))), inference(resolution, [status(thm)], [c242,d9])).
% 58.50/10.36 cnf(d11, plain, ~'l3$ulattices'('k1$ulattice2'('k11$uconlat$u1'(sK169))) | ~'l3$ulattices'('k11$uconlat$u1'('k7$uconlat$u2'(sK169))) | ~'v10$ulattices'('k1$ulattice2'('k11$uconlat$u1'(sK169))) | 'v3$ustruct$u0'('k1$ulattice2'('k11$uconlat$u1'(sK169))) | 'v3$ustruct$u0'('k11$uconlat$u1'('k7$uconlat$u2'(sK169))) | ~'Ts86'('k7$uconlat$u2'(sK169)), inference(resolution, [status(thm)], [d10,c124])).
% 58.50/10.36 cnf(d12, plain, ~'Ts86'('k7$uconlat$u2'(sK169)) | ~'l3$ulattices'('k1$ulattice2'('k11$uconlat$u1'(sK169))) | ~'l3$ulattices'('k11$uconlat$u1'('k7$uconlat$u2'(sK169))) | ~'v10$ulattices'('k1$ulattice2'('k11$uconlat$u1'(sK169))) | 'v3$ustruct$u0'('k1$ulattice2'('k11$uconlat$u1'(sK169))) | ~'Ts86'('k7$uconlat$u2'(sK169)), inference(resolution, [status(thm)], [c120,d11])).
% 58.50/10.36 cnf(d13, plain, ~'l3$ulattices'('k1$ulattice2'('k11$uconlat$u1'(sK169))) | ~'l3$ulattices'('k11$uconlat$u1'('k7$uconlat$u2'(sK169))) | 'v3$ustruct$u0'('k1$ulattice2'('k11$uconlat$u1'(sK169))) | ~'Ts86'('k7$uconlat$u2'(sK169)) | ~'Ts77'('k11$uconlat$u1'(sK169)), inference(resolution, [status(thm)], [d12,c99])).
% 58.50/10.36 cnf(d14, plain, ~'Ts77'('k11$uconlat$u1'(sK169)) | ~'l3$ulattices'('k1$ulattice2'('k11$uconlat$u1'(sK169))) | ~'l3$ulattices'('k11$uconlat$u1'('k7$uconlat$u2'(sK169))) | ~'Ts77'('k11$uconlat$u1'(sK169)) | ~'Ts86'('k7$uconlat$u2'(sK169)), inference(resolution, [status(thm)], [c95,d13])).
% 58.50/10.36 cnf(d15, plain, ~'l3$ulattices'('k1$ulattice2'('k11$uconlat$u1'(sK169))) | ~'Ts77'('k11$uconlat$u1'(sK169)) | ~'Ts86'('k7$uconlat$u2'(sK169)) | ~'l2$uconlat$u1'('k7$uconlat$u2'(sK169)) | 'v3$uconlat$u1'('k7$uconlat$u2'(sK169)), inference(resolution, [status(thm)], [d14,c38])).
% 58.50/10.36 cnf(d16, plain, 'g2$uconlat$u1'('u2$uconlat$u1'(sK169),'u1$uconlat$u1'(sK169),'k6$urelset$u1'('u1$uconlat$u1'(sK169),'u2$uconlat$u1'(sK169),'u3$uconlat$u1'(sK169))) = 'k7$uconlat$u2'(sK169) | 'v3$uconlat$u1'(sK169), inference(resolution, [status(thm)], [c31,c241])).
% 58.50/10.36 cnf(d17, plain, 'g2$uconlat$u1'('u2$uconlat$u1'(sK169),'u1$uconlat$u1'(sK169),'k6$urelset$u1'('u1$uconlat$u1'(sK169),'u2$uconlat$u1'(sK169),'u3$uconlat$u1'(sK169))) = 'k7$uconlat$u2'(sK169), inference(resolution, [status(thm)], [c242,d16])).
% 58.50/10.36 cnf(d18, plain, 'l2$uconlat$u1'('k7$uconlat$u2'(sK169)) | ~'m1$urelset$u1'('k6$urelset$u1'('u1$uconlat$u1'(sK169),'u2$uconlat$u1'(sK169),'u3$uconlat$u1'(sK169)),'u2$uconlat$u1'(sK169),'u1$uconlat$u1'(sK169)), inference(superposition, [status(thm)], [d17,c33])).
% 58.50/10.36 cnf(d19, plain, 'm1$urelset$u1'('k6$urelset$u1'(X0,X1,X2),X1,X0) | ~'m1$urelset$u1'(X2,X0,X1), inference(resolution, [status(thm)], [c226,c43])).
% 58.50/10.36 cnf(d20, plain, ~'m1$urelset$u1'('u3$uconlat$u1'(sK169),'u1$uconlat$u1'(sK169),'u2$uconlat$u1'(sK169)) | 'l2$uconlat$u1'('k7$uconlat$u2'(sK169)), inference(resolution, [status(thm)], [d19,d18])).
% 58.50/10.36 cnf(d21, plain, 'm1$urelset$u1'('u3$uconlat$u1'(X0),'u1$uconlat$u1'(X0),'u2$uconlat$u1'(X0)) | ~'l2$uconlat$u1'(X0), inference(resolution, [status(thm)], [c226,c62])).
% 58.50/10.36 cnf(d22, plain, ~'l2$uconlat$u1'(sK169) | 'l2$uconlat$u1'('k7$uconlat$u2'(sK169)), inference(resolution, [status(thm)], [d21,d20])).
% 58.50/10.36 cnf(d23, plain, 'l2$uconlat$u1'('k7$uconlat$u2'(sK169)), inference(resolution, [status(thm)], [c241,d22])).
% 58.50/10.36 cnf(d24, plain, ~'l3$ulattices'('k1$ulattice2'('k11$uconlat$u1'(sK169))) | 'v3$uconlat$u1'('k7$uconlat$u2'(sK169)) | ~'Ts77'('k11$uconlat$u1'(sK169)) | ~'Ts86'('k7$uconlat$u2'(sK169)), inference(resolution, [status(thm)], [d23,d15])).
% 58.50/10.36 cnf(d25, plain, 'v3$uconlat$u1'('k7$uconlat$u2'(sK169)) | 'Ts86'('k7$uconlat$u2'(sK169)), inference(resolution, [status(thm)], [d23,c119])).
% 58.50/10.36 cnf(d26, plain, 'v3$uconlat$u1'('k7$uconlat$u2'(sK169)) | ~'l3$ulattices'('k1$ulattice2'('k11$uconlat$u1'(sK169))) | 'v3$uconlat$u1'('k7$uconlat$u2'(sK169)) | ~'Ts77'('k11$uconlat$u1'(sK169)), inference(resolution, [status(thm)], [d25,d24])).
% 58.50/10.36 cnf(d27, plain, 'v3$uconlat$u1'('k7$uconlat$u2'(sK169)) | ~'Ts77'('k11$uconlat$u1'(sK169)) | ~'l3$ulattices'('k11$uconlat$u1'(sK169)), inference(resolution, [status(thm)], [d26,c41])).
% 58.50/10.36 cnf(d28, plain, ~'l3$ulattices'('k11$uconlat$u1'(sK169)) | 'v3$uconlat$u1'('k7$uconlat$u2'(sK169)) | ~'l2$uconlat$u1'(sK169) | 'v3$uconlat$u1'(sK169), inference(resolution, [status(thm)], [d27,d4])).
% 58.50/10.36 cnf(d29, plain, ~'l3$ulattices'('k11$uconlat$u1'(sK169)) | 'v3$uconlat$u1'('k7$uconlat$u2'(sK169)) | 'v3$uconlat$u1'(sK169), inference(resolution, [status(thm)], [c241,d28])).
% 58.50/10.36 cnf(d30, plain, ~'l3$ulattices'('k11$uconlat$u1'(sK169)) | 'v3$uconlat$u1'('k7$uconlat$u2'(sK169)), inference(resolution, [status(thm)], [c242,d29])).
% 58.50/10.36 cnf(d31, plain, 'v3$uconlat$u1'('k7$uconlat$u2'(sK169)) | ~'l2$uconlat$u1'(sK169) | 'v3$uconlat$u1'(sK169), inference(resolution, [status(thm)], [d30,c38])).
% 58.50/10.36 cnf(d32, plain, 'v3$uconlat$u1'('k7$uconlat$u2'(sK169)) | 'v3$uconlat$u1'(sK169), inference(resolution, [status(thm)], [c241,d31])).
% 58.50/10.36 cnf(d33, plain, 'v3$uconlat$u1'('k7$uconlat$u2'(sK169)), inference(resolution, [status(thm)], [c242,d32])).
% 58.50/10.36 cnf(d34, plain, ~'l2$uconlat$u1'(sK169) | 'v3$uconlat$u1'(sK169), inference(resolution, [status(thm)], [d33,c44])).
% 58.50/10.36 cnf(d35, plain, 'v3$uconlat$u1'(sK169), inference(resolution, [status(thm)], [c241,d34])).
% 58.50/10.36 cnf(d36, plain, $false, inference(resolution, [status(thm)], [c242,d35])).
% 58.50/10.36 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------