%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : GRP653+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 : n010.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:24:21 AM UTC 2026
% Result : Theorem 24.25s 3.75s
% Output : CNFRefutation 24.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP653+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.09/0.38 % Computer : n010.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Fri Sep 25 15:28:44 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 24.25/3.75 % SZS status Theorem for theBenchmark.p
% 24.25/3.75 % SZS output start CNFRefutation for theBenchmark.p
% 24.25/3.75 fof(dt_k11_group_4, axiom, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v3$ugroup$u1'(X0) & ('v4$ugroup$u1'(X0) & 'l1$ugroup$u1'(X0)))) => (~'v3$ustruct$u0'('k11$ugroup$u4'(X0)) & ('v3$ulattices'('k11$ugroup$u4'(X0)) & ('v10$ulattices'('k11$ugroup$u4'(X0)) & 'l3$ulattices'('k11$ugroup$u4'(X0)))))))).
% 24.25/3.75 fof(dt_k3_latsubgr, axiom, ! [X0] : ! [X1] : ! [X2] : (((~'v3$ustruct$u0'(X0) & ('v3$ugroup$u1'(X0) & ('v4$ugroup$u1'(X0) & ('l1$ugroup$u1'(X0) & (~'v3$ustruct$u0'(X1) & ('v3$ugroup$u1'(X1) & ('v4$ugroup$u1'(X1) & ('l1$ugroup$u1'(X1) & ('v1$ufunct$u1'(X2) & ('v1$ufunct$u2'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1)) & 'm1$urelset$u1'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1)))))))))))) => ('v1$ufunct$u1'('k3$ulatsubgr'(X0,X1,X2)) & ('v1$ufunct$u2'('k3$ulatsubgr'(X0,X1,X2),'u1$ustruct$u0'('k11$ugroup$u4'(X0)),'u1$ustruct$u0'('k11$ugroup$u4'(X1))) & 'm2$urelset$u1'('k3$ulatsubgr'(X0,X1,X2),'u1$ustruct$u0'('k11$ugroup$u4'(X0)),'u1$ustruct$u0'('k11$ugroup$u4'(X1)))))))).
% 24.25/3.75 fof(dt_m4_vectsp_8, axiom, ! [X0] : ! [X1] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & ('l3$ulattices'(X0) & (~'v3$ustruct$u0'(X1) & ('v10$ulattices'(X1) & 'l3$ulattices'(X1)))))) => ! [X2] : (('m4$uvectsp$u8'(X2,X0,X1) => ('v1$ufunct$u1'(X2) & ('v1$ufunct$u2'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1)) & 'm2$urelset$u1'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1))))))))).
% 24.25/3.75 fof(fc1_group_4, axiom, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v3$ugroup$u1'(X0) & ('v4$ugroup$u1'(X0) & 'l1$ugroup$u1'(X0)))) => (~'v3$ustruct$u0'('k11$ugroup$u4'(X0)) & ('v3$ulattices'('k11$ugroup$u4'(X0)) & ('v4$ulattices'('k11$ugroup$u4'(X0)) & ('v5$ulattices'('k11$ugroup$u4'(X0)) & ('v6$ulattices'('k11$ugroup$u4'(X0)) & ('v7$ulattices'('k11$ugroup$u4'(X0)) & ('v8$ulattices'('k11$ugroup$u4'(X0)) & ('v9$ulattices'('k11$ugroup$u4'(X0)) & ('v10$ulattices'('k11$ugroup$u4'(X0)) & ('v13$ulattices'('k11$ugroup$u4'(X0)) & ('v14$ulattices'('k11$ugroup$u4'(X0)) & 'v15$ulattices'('k11$ugroup$u4'(X0)))))))))))))))).
% 24.25/3.75 fof(redefinition_m2_relset_1, axiom, ! [X0] : ! [X1] : ! [X2] : (('m2$urelset$u1'(X2,X0,X1) <=> 'm1$urelset$u1'(X2,X0,X1)))).
% 24.25/3.75 fof(t11_vectsp_8, axiom, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v10$ulattices'(X0) & 'l3$ulattices'(X0))) => ! [X1] : (((~'v3$ustruct$u0'(X1) & ('v10$ulattices'(X1) & 'l3$ulattices'(X1))) => ! [X2] : ((('v1$ufunct$u1'(X2) & ('v1$ufunct$u2'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1)) & 'm2$urelset$u1'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1)))) => ('m1$ulattice4'(X2,X0,X1) <=> ('m4$uvectsp$u8'(X2,X0,X1) & 'm3$uvectsp$u8'(X2,X0,X1)))))))))).
% 24.25/3.75 fof(t36_latsubgr, axiom, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v3$ugroup$u1'(X0) & ('v4$ugroup$u1'(X0) & 'l1$ugroup$u1'(X0)))) => ! [X1] : (((~'v3$ustruct$u0'(X1) & ('v3$ugroup$u1'(X1) & ('v4$ugroup$u1'(X1) & 'l1$ugroup$u1'(X1)))) => ! [X2] : ((('v1$ufunct$u1'(X2) & ('v1$ufunct$u2'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1)) & ('v1$ugroup$u6'(X2,X0,X1) & 'm2$urelset$u1'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1))))) => ('v2$ufunct$u1'(X2) => 'm3$uvectsp$u8'('k3$ulatsubgr'(X0,X1,X2),'k11$ugroup$u4'(X0),'k11$ugroup$u4'(X1)))))))))).
% 24.25/3.75 fof(t37_latsubgr, axiom, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v3$ugroup$u1'(X0) & ('v4$ugroup$u1'(X0) & 'l1$ugroup$u1'(X0)))) => ! [X1] : (((~'v3$ustruct$u0'(X1) & ('v3$ugroup$u1'(X1) & ('v4$ugroup$u1'(X1) & 'l1$ugroup$u1'(X1)))) => ! [X2] : ((('v1$ufunct$u1'(X2) & ('v1$ufunct$u2'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1)) & ('v1$ugroup$u6'(X2,X0,X1) & 'm2$urelset$u1'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1))))) => 'm4$uvectsp$u8'('k3$ulatsubgr'(X0,X1,X2),'k11$ugroup$u4'(X0),'k11$ugroup$u4'(X1))))))))).
% 24.25/3.75 fof(t38_latsubgr, conjecture, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v3$ugroup$u1'(X0) & ('v4$ugroup$u1'(X0) & 'l1$ugroup$u1'(X0)))) => ! [X1] : (((~'v3$ustruct$u0'(X1) & ('v3$ugroup$u1'(X1) & ('v4$ugroup$u1'(X1) & 'l1$ugroup$u1'(X1)))) => ! [X2] : ((('v1$ufunct$u1'(X2) & ('v1$ufunct$u2'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1)) & ('v1$ugroup$u6'(X2,X0,X1) & 'm2$urelset$u1'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1))))) => ('v2$ufunct$u1'(X2) => 'm1$ulattice4'('k3$ulatsubgr'(X0,X1,X2),'k11$ugroup$u4'(X0),'k11$ugroup$u4'(X1)))))))))).
% 24.25/3.75 fof(negated_conjecture, negated_conjecture, ~! [X0] : (((~'v3$ustruct$u0'(X0) & ('v3$ugroup$u1'(X0) & ('v4$ugroup$u1'(X0) & 'l1$ugroup$u1'(X0)))) => ! [X1] : (((~'v3$ustruct$u0'(X1) & ('v3$ugroup$u1'(X1) & ('v4$ugroup$u1'(X1) & 'l1$ugroup$u1'(X1)))) => ! [X2] : ((('v1$ufunct$u1'(X2) & ('v1$ufunct$u2'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1)) & ('v1$ugroup$u6'(X2,X0,X1) & 'm2$urelset$u1'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1))))) => ('v2$ufunct$u1'(X2) => 'm1$ulattice4'('k3$ulatsubgr'(X0,X1,X2),'k11$ugroup$u4'(X0),'k11$ugroup$u4'(X1))))))))), inference(negate_conjecture, [status(cth)], [t38_latsubgr])).
% 24.25/3.75 cnf(c17, plain, 'l3$ulattices'('k11$ugroup$u4'(X0)) | ~'v3$ugroup$u1'(X0) | 'v3$ustruct$u0'(X0) | ~'v4$ugroup$u1'(X0) | ~'l1$ugroup$u1'(X0), inference(clausification, [status(esa)], [dt_k11_group_4])).
% 24.25/3.75 cnf(c18, plain, ~'v1$ufunct$u2'(X0,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2)) | ~'v4$ugroup$u1'(X1) | ~'m1$urelset$u1'(X0,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2)) | 'v3$ustruct$u0'(X1) | ~'l1$ugroup$u1'(X2) | ~'v3$ugroup$u1'(X2) | ~'v1$ufunct$u1'(X0) | 'v3$ustruct$u0'(X2) | ~'v4$ugroup$u1'(X2) | ~'v3$ugroup$u1'(X1) | ~'l1$ugroup$u1'(X1) | 'v1$ufunct$u1'('k3$ulatsubgr'(X1,X2,X0)), inference(clausification, [status(esa)], [dt_k3_latsubgr])).
% 24.25/3.75 cnf(c34, plain, ~'v10$ulattices'(X0) | 'v1$ufunct$u2'(X1,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X2)) | ~'v10$ulattices'(X2) | 'v3$ustruct$u0'(X2) | ~'l3$ulattices'(X0) | ~'m4$uvectsp$u8'(X1,X0,X2) | ~'l3$ulattices'(X2) | 'v3$ustruct$u0'(X0), inference(clausification, [status(esa)], [dt_m4_vectsp_8])).
% 24.25/3.75 cnf(c35, plain, ~'v10$ulattices'(X0) | ~'v10$ulattices'(X1) | 'v3$ustruct$u0'(X1) | 'm2$urelset$u1'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1)) | ~'l3$ulattices'(X0) | ~'m4$uvectsp$u8'(X2,X0,X1) | ~'l3$ulattices'(X1) | 'v3$ustruct$u0'(X0), inference(clausification, [status(esa)], [dt_m4_vectsp_8])).
% 24.25/3.75 cnf(c53, plain, X0(X1) | ~'l1$ugroup$u1'(X1) | ~'v3$ugroup$u1'(X1) | ~'v4$ugroup$u1'(X1) | 'v3$ustruct$u0'(X1), inference(clausification, [status(esa)], [fc1_group_4])).
% 24.25/3.75 cnf(c54, plain, ~X0(X1) | ~'v3$ustruct$u0'('k11$ugroup$u4'(X1)), inference(clausification, [status(esa)], [fc1_group_4])).
% 24.25/3.75 cnf(c62, plain, ~X0(X1) | 'v10$ulattices'('k11$ugroup$u4'(X1)), inference(clausification, [status(esa)], [fc1_group_4])).
% 24.25/3.75 cnf(c94, plain, ~'m2$urelset$u1'(X0,X1,X2) | 'm1$urelset$u1'(X0,X1,X2), inference(clausification, [status(esa)], [redefinition_m2_relset_1])).
% 24.25/3.75 cnf(c99, plain, ~'m2$urelset$u1'(X0,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2)) | 'v3$ustruct$u0'(X1) | ~'l3$ulattices'(X2) | 'v3$ustruct$u0'(X2) | ~'v10$ulattices'(X2) | ~'v1$ufunct$u2'(X0,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X2)) | ~'m4$uvectsp$u8'(X0,X1,X2) | ~'m3$uvectsp$u8'(X0,X1,X2) | ~'l3$ulattices'(X1) | ~'v1$ufunct$u1'(X0) | ~'v10$ulattices'(X1) | 'm1$ulattice4'(X0,X1,X2), inference(clausification, [status(esa)], [t11_vectsp_8])).
% 24.25/3.75 cnf(c102, plain, ~'v3$ugroup$u1'(X0) | ~'v1$ufunct$u1'(X1) | ~'v1$ugroup$u6'(X1,X0,X2) | 'm3$uvectsp$u8'('k3$ulatsubgr'(X0,X2,X1),'k11$ugroup$u4'(X0),'k11$ugroup$u4'(X2)) | ~'v2$ufunct$u1'(X1) | ~'l1$ugroup$u1'(X2) | ~'v4$ugroup$u1'(X2) | ~'v1$ufunct$u2'(X1,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X2)) | ~'m2$urelset$u1'(X1,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X2)) | ~'v3$ugroup$u1'(X2) | 'v3$ustruct$u0'(X0) | 'v3$ustruct$u0'(X2) | ~'v4$ugroup$u1'(X0) | ~'l1$ugroup$u1'(X0), inference(clausification, [status(esa)], [t36_latsubgr])).
% 24.25/3.75 cnf(c103, plain, 'v3$ustruct$u0'(X0) | ~'v1$ugroup$u6'(X1,X0,X2) | ~'v4$ugroup$u1'(X0) | ~'l1$ugroup$u1'(X2) | ~'v3$ugroup$u1'(X0) | ~'l1$ugroup$u1'(X0) | ~'v1$ufunct$u1'(X1) | ~'v1$ufunct$u2'(X1,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X2)) | ~'m2$urelset$u1'(X1,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X2)) | 'm4$uvectsp$u8'('k3$ulatsubgr'(X0,X2,X1),'k11$ugroup$u4'(X0),'k11$ugroup$u4'(X2)) | 'v3$ustruct$u0'(X2) | ~'v4$ugroup$u1'(X2) | ~'v3$ugroup$u1'(X2), inference(clausification, [status(esa)], [t37_latsubgr])).
% 24.25/3.75 cnf(c111, plain, ~'v3$ustruct$u0'(sK121), inference(clausification, [status(esa)], [negated_conjecture])).
% 24.25/3.75 cnf(c112, plain, 'v3$ugroup$u1'(sK121), inference(clausification, [status(esa)], [negated_conjecture])).
% 24.25/3.75 cnf(c113, plain, 'v4$ugroup$u1'(sK121), inference(clausification, [status(esa)], [negated_conjecture])).
% 24.25/3.75 cnf(c114, plain, 'l1$ugroup$u1'(sK121), inference(clausification, [status(esa)], [negated_conjecture])).
% 24.25/3.75 cnf(c115, plain, ~'v3$ustruct$u0'(sK122), inference(clausification, [status(esa)], [negated_conjecture])).
% 24.25/3.75 cnf(c116, plain, 'v3$ugroup$u1'(sK122), inference(clausification, [status(esa)], [negated_conjecture])).
% 24.25/3.75 cnf(c117, plain, 'v4$ugroup$u1'(sK122), inference(clausification, [status(esa)], [negated_conjecture])).
% 24.25/3.75 cnf(c118, plain, 'l1$ugroup$u1'(sK122), inference(clausification, [status(esa)], [negated_conjecture])).
% 24.25/3.75 cnf(c119, plain, 'v1$ufunct$u1'(sK123), inference(clausification, [status(esa)], [negated_conjecture])).
% 24.25/3.75 cnf(c120, plain, 'v1$ufunct$u2'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)), inference(clausification, [status(esa)], [negated_conjecture])).
% 24.25/3.75 cnf(c121, plain, 'v1$ugroup$u6'(sK123,sK121,sK122), inference(clausification, [status(esa)], [negated_conjecture])).
% 24.25/3.75 cnf(c122, plain, 'm2$urelset$u1'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)), inference(clausification, [status(esa)], [negated_conjecture])).
% 24.25/3.75 cnf(c123, plain, 'v2$ufunct$u1'(sK123), inference(clausification, [status(esa)], [negated_conjecture])).
% 24.25/3.75 cnf(c124, plain, ~'m1$ulattice4'('k3$ulatsubgr'(sK121,sK122,sK123),'k11$ugroup$u4'(sK121),'k11$ugroup$u4'(sK122)), inference(clausification, [status(esa)], [negated_conjecture])).
% 24.25/3.75 cnf(d0, plain, ~'l3$ulattices'(X0) | ~'l3$ulattices'(X1) | ~'v1$ufunct$u1'(X2) | ~'v1$ufunct$u2'(X2,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X0)) | 'v3$ustruct$u0'(X0) | 'v3$ustruct$u0'(X1) | ~'v10$ulattices'(X0) | ~'v10$ulattices'(X1) | 'm1$ulattice4'(X2,X1,X0) | ~'m3$uvectsp$u8'(X2,X1,X0) | ~'m4$uvectsp$u8'(X2,X1,X0) | ~'l3$ulattices'(X1) | ~'l3$ulattices'(X0) | 'v3$ustruct$u0'(X1) | 'v3$ustruct$u0'(X0) | ~'v10$ulattices'(X1) | ~'v10$ulattices'(X0) | ~'m4$uvectsp$u8'(X2,X1,X0), inference(resolution, [status(thm)], [c99,c35])).
% 24.25/3.75 cnf(d1, plain, ~'l3$ulattices'(X0) | ~'l3$ulattices'(X1) | ~'v1$ufunct$u1'(X2) | 'v3$ustruct$u0'(X0) | 'v3$ustruct$u0'(X1) | ~'v10$ulattices'(X0) | ~'v10$ulattices'(X1) | 'm1$ulattice4'(X2,X0,X1) | ~'m3$uvectsp$u8'(X2,X0,X1) | ~'m4$uvectsp$u8'(X2,X0,X1) | ~'l3$ulattices'(X0) | ~'l3$ulattices'(X1) | 'v3$ustruct$u0'(X0) | 'v3$ustruct$u0'(X1) | ~'v10$ulattices'(X0) | ~'v10$ulattices'(X1) | ~'m4$uvectsp$u8'(X2,X0,X1), inference(resolution, [status(thm)], [d0,c34])).
% 24.25/3.75 cnf(d2, plain, ~'l3$ulattices'('k11$ugroup$u4'(X0)) | ~'l3$ulattices'('k11$ugroup$u4'(X1)) | ~'v1$ufunct$u1'('k3$ulatsubgr'(X1,X0,X2)) | 'v3$ustruct$u0'('k11$ugroup$u4'(X0)) | 'v3$ustruct$u0'('k11$ugroup$u4'(X1)) | ~'v10$ulattices'('k11$ugroup$u4'(X0)) | ~'v10$ulattices'('k11$ugroup$u4'(X1)) | 'm1$ulattice4'('k3$ulatsubgr'(X1,X0,X2),'k11$ugroup$u4'(X1),'k11$ugroup$u4'(X0)) | ~'m3$uvectsp$u8'('k3$ulatsubgr'(X1,X0,X2),'k11$ugroup$u4'(X1),'k11$ugroup$u4'(X0)) | ~'v1$ufunct$u1'(X2) | ~'v1$ufunct$u2'(X2,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X0)) | 'v3$ustruct$u0'(X0) | 'v3$ustruct$u0'(X1) | ~'l1$ugroup$u1'(X0) | ~'l1$ugroup$u1'(X1) | ~'v3$ugroup$u1'(X0) | ~'v3$ugroup$u1'(X1) | ~'v4$ugroup$u1'(X0) | ~'v4$ugroup$u1'(X1) | ~'m2$urelset$u1'(X2,'u1$ustruct$u0'(X1),'u1$ustruct$u0'(X0)) | ~'v1$ugroup$u6'(X2,X1,X0), inference(resolution, [status(thm)], [d1,c103])).
% 24.25/3.75 cnf(d3, plain, ~'l3$ulattices'('k11$ugroup$u4'(X0)) | ~'l3$ulattices'('k11$ugroup$u4'(X1)) | ~'v1$ufunct$u1'(X2) | ~'v1$ufunct$u1'('k3$ulatsubgr'(X0,X1,X2)) | ~'v1$ufunct$u2'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1)) | 'v3$ustruct$u0'(X0) | 'v3$ustruct$u0'(X1) | 'v3$ustruct$u0'('k11$ugroup$u4'(X0)) | 'v3$ustruct$u0'('k11$ugroup$u4'(X1)) | ~'l1$ugroup$u1'(X0) | ~'l1$ugroup$u1'(X1) | ~'v3$ugroup$u1'(X0) | ~'v3$ugroup$u1'(X1) | ~'v4$ugroup$u1'(X0) | ~'v4$ugroup$u1'(X1) | ~'v10$ulattices'('k11$ugroup$u4'(X0)) | ~'v10$ulattices'('k11$ugroup$u4'(X1)) | ~'m2$urelset$u1'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1)) | 'm1$ulattice4'('k3$ulatsubgr'(X0,X1,X2),'k11$ugroup$u4'(X0),'k11$ugroup$u4'(X1)) | ~'v1$ugroup$u6'(X2,X0,X1) | ~'v1$ufunct$u1'(X2) | ~'v1$ufunct$u2'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1)) | 'v3$ustruct$u0'(X1) | 'v3$ustruct$u0'(X0) | ~'l1$ugroup$u1'(X1) | ~'l1$ugroup$u1'(X0) | ~'v3$ugroup$u1'(X1) | ~'v3$ugroup$u1'(X0) | ~'v4$ugroup$u1'(X1) | ~'v4$ugroup$u1'(X0) | ~'m2$urelset$u1'(X2,'u1$ustruct$u0'(X0),'u1$ustruct$u0'(X1)) | ~'v2$ufunct$u1'(X2) | ~'v1$ugroup$u6'(X2,X0,X1), inference(resolution, [status(thm)], [d2,c102])).
% 24.25/3.75 cnf(d4, plain, ~'l3$ulattices'('k11$ugroup$u4'(sK122)) | ~'l3$ulattices'('k11$ugroup$u4'(sK121)) | ~'v1$ufunct$u1'(sK123) | ~'v1$ufunct$u1'('k3$ulatsubgr'(sK121,sK122,sK123)) | ~'v1$ufunct$u2'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | 'v3$ustruct$u0'(sK122) | 'v3$ustruct$u0'(sK121) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | ~'l1$ugroup$u1'(sK122) | ~'l1$ugroup$u1'(sK121) | ~'v3$ugroup$u1'(sK122) | ~'v3$ugroup$u1'(sK121) | ~'v4$ugroup$u1'(sK122) | ~'v4$ugroup$u1'(sK121) | ~'v10$ulattices'('k11$ugroup$u4'(sK122)) | ~'v10$ulattices'('k11$ugroup$u4'(sK121)) | ~'m2$urelset$u1'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | ~'v2$ufunct$u1'(sK123) | ~'v1$ugroup$u6'(sK123,sK121,sK122), inference(resolution, [status(thm)], [d3,c124])).
% 24.25/3.75 cnf(d5, plain, ~'l3$ulattices'('k11$ugroup$u4'(sK121)) | ~'l3$ulattices'('k11$ugroup$u4'(sK122)) | ~'v1$ufunct$u1'('k3$ulatsubgr'(sK121,sK122,sK123)) | ~'v1$ufunct$u1'(sK123) | ~'v1$ufunct$u2'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)) | 'v3$ustruct$u0'(sK122) | ~'l1$ugroup$u1'(sK121) | ~'l1$ugroup$u1'(sK122) | ~'v3$ugroup$u1'(sK121) | ~'v3$ugroup$u1'(sK122) | ~'v4$ugroup$u1'(sK121) | ~'v4$ugroup$u1'(sK122) | ~'v10$ulattices'('k11$ugroup$u4'(sK121)) | ~'v10$ulattices'('k11$ugroup$u4'(sK122)) | ~'m2$urelset$u1'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | ~'v2$ufunct$u1'(sK123) | ~'v1$ugroup$u6'(sK123,sK121,sK122), inference(resolution, [status(thm)], [c111,d4])).
% 24.25/3.75 cnf(d6, plain, ~'l3$ulattices'('k11$ugroup$u4'(sK121)) | ~'l3$ulattices'('k11$ugroup$u4'(sK122)) | ~'v1$ufunct$u1'('k3$ulatsubgr'(sK121,sK122,sK123)) | ~'v1$ufunct$u1'(sK123) | ~'v1$ufunct$u2'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)) | 'v3$ustruct$u0'(sK122) | ~'l1$ugroup$u1'(sK121) | ~'l1$ugroup$u1'(sK122) | ~'v3$ugroup$u1'(sK122) | ~'v4$ugroup$u1'(sK121) | ~'v4$ugroup$u1'(sK122) | ~'v10$ulattices'('k11$ugroup$u4'(sK121)) | ~'v10$ulattices'('k11$ugroup$u4'(sK122)) | ~'m2$urelset$u1'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | ~'v2$ufunct$u1'(sK123) | ~'v1$ugroup$u6'(sK123,sK121,sK122), inference(resolution, [status(thm)], [c112,d5])).
% 24.25/3.75 cnf(d7, plain, ~'l3$ulattices'('k11$ugroup$u4'(sK121)) | ~'l3$ulattices'('k11$ugroup$u4'(sK122)) | ~'v1$ufunct$u1'('k3$ulatsubgr'(sK121,sK122,sK123)) | ~'v1$ufunct$u1'(sK123) | ~'v1$ufunct$u2'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)) | 'v3$ustruct$u0'(sK122) | ~'l1$ugroup$u1'(sK121) | ~'l1$ugroup$u1'(sK122) | ~'v3$ugroup$u1'(sK122) | ~'v4$ugroup$u1'(sK122) | ~'v10$ulattices'('k11$ugroup$u4'(sK121)) | ~'v10$ulattices'('k11$ugroup$u4'(sK122)) | ~'m2$urelset$u1'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | ~'v2$ufunct$u1'(sK123) | ~'v1$ugroup$u6'(sK123,sK121,sK122), inference(resolution, [status(thm)], [c113,d6])).
% 24.25/3.75 cnf(d8, plain, ~'l3$ulattices'('k11$ugroup$u4'(sK121)) | ~'l3$ulattices'('k11$ugroup$u4'(sK122)) | ~'v1$ufunct$u1'('k3$ulatsubgr'(sK121,sK122,sK123)) | ~'v1$ufunct$u1'(sK123) | ~'v1$ufunct$u2'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)) | 'v3$ustruct$u0'(sK122) | ~'l1$ugroup$u1'(sK122) | ~'v3$ugroup$u1'(sK122) | ~'v4$ugroup$u1'(sK122) | ~'v10$ulattices'('k11$ugroup$u4'(sK121)) | ~'v10$ulattices'('k11$ugroup$u4'(sK122)) | ~'m2$urelset$u1'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | ~'v2$ufunct$u1'(sK123) | ~'v1$ugroup$u6'(sK123,sK121,sK122), inference(resolution, [status(thm)], [c114,d7])).
% 24.25/3.75 cnf(d9, plain, ~'l3$ulattices'('k11$ugroup$u4'(sK121)) | ~'l3$ulattices'('k11$ugroup$u4'(sK122)) | ~'v1$ufunct$u1'('k3$ulatsubgr'(sK121,sK122,sK123)) | ~'v1$ufunct$u1'(sK123) | ~'v1$ufunct$u2'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)) | ~'l1$ugroup$u1'(sK122) | ~'v3$ugroup$u1'(sK122) | ~'v4$ugroup$u1'(sK122) | ~'v10$ulattices'('k11$ugroup$u4'(sK121)) | ~'v10$ulattices'('k11$ugroup$u4'(sK122)) | ~'m2$urelset$u1'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | ~'v2$ufunct$u1'(sK123) | ~'v1$ugroup$u6'(sK123,sK121,sK122), inference(resolution, [status(thm)], [c115,d8])).
% 24.25/3.75 cnf(d10, plain, ~'l3$ulattices'('k11$ugroup$u4'(sK121)) | ~'l3$ulattices'('k11$ugroup$u4'(sK122)) | ~'v1$ufunct$u1'('k3$ulatsubgr'(sK121,sK122,sK123)) | ~'v1$ufunct$u1'(sK123) | ~'v1$ufunct$u2'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)) | ~'l1$ugroup$u1'(sK122) | ~'v4$ugroup$u1'(sK122) | ~'v10$ulattices'('k11$ugroup$u4'(sK121)) | ~'v10$ulattices'('k11$ugroup$u4'(sK122)) | ~'m2$urelset$u1'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | ~'v2$ufunct$u1'(sK123) | ~'v1$ugroup$u6'(sK123,sK121,sK122), inference(resolution, [status(thm)], [c116,d9])).
% 24.25/3.75 cnf(d11, plain, ~'l3$ulattices'('k11$ugroup$u4'(sK121)) | ~'l3$ulattices'('k11$ugroup$u4'(sK122)) | ~'v1$ufunct$u1'('k3$ulatsubgr'(sK121,sK122,sK123)) | ~'v1$ufunct$u1'(sK123) | ~'v1$ufunct$u2'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)) | ~'l1$ugroup$u1'(sK122) | ~'v10$ulattices'('k11$ugroup$u4'(sK121)) | ~'v10$ulattices'('k11$ugroup$u4'(sK122)) | ~'m2$urelset$u1'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | ~'v2$ufunct$u1'(sK123) | ~'v1$ugroup$u6'(sK123,sK121,sK122), inference(resolution, [status(thm)], [c117,d10])).
% 24.25/3.75 cnf(d12, plain, ~'l3$ulattices'('k11$ugroup$u4'(sK121)) | ~'l3$ulattices'('k11$ugroup$u4'(sK122)) | ~'v1$ufunct$u1'('k3$ulatsubgr'(sK121,sK122,sK123)) | ~'v1$ufunct$u1'(sK123) | ~'v1$ufunct$u2'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)) | ~'v10$ulattices'('k11$ugroup$u4'(sK121)) | ~'v10$ulattices'('k11$ugroup$u4'(sK122)) | ~'m2$urelset$u1'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | ~'v2$ufunct$u1'(sK123) | ~'v1$ugroup$u6'(sK123,sK121,sK122), inference(resolution, [status(thm)], [c118,d11])).
% 24.25/3.75 cnf(d13, plain, ~'l3$ulattices'('k11$ugroup$u4'(sK121)) | ~'l3$ulattices'('k11$ugroup$u4'(sK122)) | ~'v1$ufunct$u1'('k3$ulatsubgr'(sK121,sK122,sK123)) | ~'v1$ufunct$u2'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)) | ~'v10$ulattices'('k11$ugroup$u4'(sK121)) | ~'v10$ulattices'('k11$ugroup$u4'(sK122)) | ~'m2$urelset$u1'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | ~'v2$ufunct$u1'(sK123) | ~'v1$ugroup$u6'(sK123,sK121,sK122), inference(resolution, [status(thm)], [c119,d12])).
% 24.25/3.75 cnf(d14, plain, ~'l3$ulattices'('k11$ugroup$u4'(sK121)) | ~'l3$ulattices'('k11$ugroup$u4'(sK122)) | ~'v1$ufunct$u1'('k3$ulatsubgr'(sK121,sK122,sK123)) | ~'v1$ufunct$u2'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)) | ~'v10$ulattices'('k11$ugroup$u4'(sK121)) | ~'v10$ulattices'('k11$ugroup$u4'(sK122)) | ~'m2$urelset$u1'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | ~'v1$ugroup$u6'(sK123,sK121,sK122), inference(resolution, [status(thm)], [c123,d13])).
% 24.25/3.75 cnf(d15, plain, ~'l3$ulattices'('k11$ugroup$u4'(sK121)) | ~'l3$ulattices'('k11$ugroup$u4'(sK122)) | ~'v1$ufunct$u1'('k3$ulatsubgr'(sK121,sK122,sK123)) | ~'v1$ufunct$u2'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)) | ~'v10$ulattices'('k11$ugroup$u4'(sK121)) | ~'v10$ulattices'('k11$ugroup$u4'(sK122)) | ~'m2$urelset$u1'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)), inference(resolution, [status(thm)], [c121,d14])).
% 24.25/3.75 cnf(d16, plain, ~'l3$ulattices'('k11$ugroup$u4'(sK121)) | ~'l3$ulattices'('k11$ugroup$u4'(sK122)) | ~'v1$ufunct$u1'('k3$ulatsubgr'(sK121,sK122,sK123)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)) | ~'v10$ulattices'('k11$ugroup$u4'(sK121)) | ~'v10$ulattices'('k11$ugroup$u4'(sK122)) | ~'m2$urelset$u1'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)), inference(resolution, [status(thm)], [c120,d15])).
% 24.25/3.75 cnf(d17, plain, ~'l3$ulattices'('k11$ugroup$u4'(sK121)) | ~'l3$ulattices'('k11$ugroup$u4'(sK122)) | ~'v1$ufunct$u1'('k3$ulatsubgr'(sK121,sK122,sK123)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)) | ~'v10$ulattices'('k11$ugroup$u4'(sK121)) | ~'v10$ulattices'('k11$ugroup$u4'(sK122)), inference(resolution, [status(thm)], [c122,d16])).
% 24.25/3.75 cnf(d18, plain, ~'v1$ufunct$u1'(sK123) | 'v1$ufunct$u1'('k3$ulatsubgr'(sK121,sK122,sK123)) | ~'m1$urelset$u1'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | 'v3$ustruct$u0'(sK121) | 'v3$ustruct$u0'(sK122) | ~'l1$ugroup$u1'(sK121) | ~'l1$ugroup$u1'(sK122) | ~'v3$ugroup$u1'(sK121) | ~'v3$ugroup$u1'(sK122) | ~'v4$ugroup$u1'(sK121) | ~'v4$ugroup$u1'(sK122), inference(resolution, [status(thm)], [c18,c120])).
% 24.25/3.75 cnf(d19, plain, 'v1$ufunct$u1'('k3$ulatsubgr'(sK121,sK122,sK123)) | ~'v1$ufunct$u1'(sK123) | ~'m1$urelset$u1'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | 'v3$ustruct$u0'(sK122) | ~'l1$ugroup$u1'(sK121) | ~'l1$ugroup$u1'(sK122) | ~'v3$ugroup$u1'(sK121) | ~'v3$ugroup$u1'(sK122) | ~'v4$ugroup$u1'(sK121) | ~'v4$ugroup$u1'(sK122), inference(resolution, [status(thm)], [c111,d18])).
% 24.25/3.75 cnf(d20, plain, 'v1$ufunct$u1'('k3$ulatsubgr'(sK121,sK122,sK123)) | ~'v1$ufunct$u1'(sK123) | ~'m1$urelset$u1'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | 'v3$ustruct$u0'(sK122) | ~'l1$ugroup$u1'(sK121) | ~'l1$ugroup$u1'(sK122) | ~'v3$ugroup$u1'(sK122) | ~'v4$ugroup$u1'(sK121) | ~'v4$ugroup$u1'(sK122), inference(resolution, [status(thm)], [c112,d19])).
% 24.25/3.75 cnf(d21, plain, 'v1$ufunct$u1'('k3$ulatsubgr'(sK121,sK122,sK123)) | ~'v1$ufunct$u1'(sK123) | ~'m1$urelset$u1'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | 'v3$ustruct$u0'(sK122) | ~'l1$ugroup$u1'(sK121) | ~'l1$ugroup$u1'(sK122) | ~'v3$ugroup$u1'(sK122) | ~'v4$ugroup$u1'(sK122), inference(resolution, [status(thm)], [c113,d20])).
% 24.25/3.75 cnf(d22, plain, 'v1$ufunct$u1'('k3$ulatsubgr'(sK121,sK122,sK123)) | ~'v1$ufunct$u1'(sK123) | ~'m1$urelset$u1'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | 'v3$ustruct$u0'(sK122) | ~'l1$ugroup$u1'(sK122) | ~'v3$ugroup$u1'(sK122) | ~'v4$ugroup$u1'(sK122), inference(resolution, [status(thm)], [c114,d21])).
% 24.25/3.75 cnf(d23, plain, 'v1$ufunct$u1'('k3$ulatsubgr'(sK121,sK122,sK123)) | ~'v1$ufunct$u1'(sK123) | ~'m1$urelset$u1'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | ~'l1$ugroup$u1'(sK122) | ~'v3$ugroup$u1'(sK122) | ~'v4$ugroup$u1'(sK122), inference(resolution, [status(thm)], [c115,d22])).
% 24.25/3.75 cnf(d24, plain, 'v1$ufunct$u1'('k3$ulatsubgr'(sK121,sK122,sK123)) | ~'v1$ufunct$u1'(sK123) | ~'m1$urelset$u1'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | ~'l1$ugroup$u1'(sK122) | ~'v4$ugroup$u1'(sK122), inference(resolution, [status(thm)], [c116,d23])).
% 24.25/3.75 cnf(d25, plain, 'v1$ufunct$u1'('k3$ulatsubgr'(sK121,sK122,sK123)) | ~'v1$ufunct$u1'(sK123) | ~'m1$urelset$u1'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)) | ~'l1$ugroup$u1'(sK122), inference(resolution, [status(thm)], [c117,d24])).
% 24.25/3.75 cnf(d26, plain, 'v1$ufunct$u1'('k3$ulatsubgr'(sK121,sK122,sK123)) | ~'v1$ufunct$u1'(sK123) | ~'m1$urelset$u1'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)), inference(resolution, [status(thm)], [c118,d25])).
% 24.25/3.75 cnf(d27, plain, 'v1$ufunct$u1'('k3$ulatsubgr'(sK121,sK122,sK123)) | ~'m1$urelset$u1'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)), inference(resolution, [status(thm)], [c119,d26])).
% 24.25/3.75 cnf(d28, plain, 'm1$urelset$u1'(sK123,'u1$ustruct$u0'(sK121),'u1$ustruct$u0'(sK122)), inference(resolution, [status(thm)], [c94,c122])).
% 24.25/3.75 cnf(d29, plain, 'v1$ufunct$u1'('k3$ulatsubgr'(sK121,sK122,sK123)), inference(resolution, [status(thm)], [d28,d27])).
% 24.25/3.75 cnf(d30, plain, ~'l3$ulattices'('k11$ugroup$u4'(sK121)) | ~'l3$ulattices'('k11$ugroup$u4'(sK122)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)) | ~'v10$ulattices'('k11$ugroup$u4'(sK121)) | ~'v10$ulattices'('k11$ugroup$u4'(sK122)), inference(resolution, [status(thm)], [d29,d17])).
% 24.25/3.75 cnf(d31, plain, ~'l3$ulattices'('k11$ugroup$u4'(sK121)) | ~'l3$ulattices'('k11$ugroup$u4'(sK122)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)) | ~'v10$ulattices'('k11$ugroup$u4'(sK121)) | ~'Ts62'(sK122), inference(resolution, [status(thm)], [d30,c62])).
% 24.25/3.75 cnf(d32, plain, 'v3$ustruct$u0'(sK122) | ~'l1$ugroup$u1'(sK122) | ~'v3$ugroup$u1'(sK122) | 'Ts62'(sK122), inference(resolution, [status(thm)], [c53,c117])).
% 24.25/3.75 cnf(d33, plain, ~'l1$ugroup$u1'(sK122) | ~'v3$ugroup$u1'(sK122) | 'Ts62'(sK122), inference(resolution, [status(thm)], [c115,d32])).
% 24.25/3.75 cnf(d34, plain, ~'l1$ugroup$u1'(sK122) | 'Ts62'(sK122), inference(resolution, [status(thm)], [c116,d33])).
% 24.25/3.75 cnf(d35, plain, 'Ts62'(sK122), inference(resolution, [status(thm)], [c118,d34])).
% 24.25/3.75 cnf(d36, plain, ~'l3$ulattices'('k11$ugroup$u4'(sK121)) | ~'l3$ulattices'('k11$ugroup$u4'(sK122)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)) | ~'v10$ulattices'('k11$ugroup$u4'(sK121)), inference(resolution, [status(thm)], [d35,d31])).
% 24.25/3.75 cnf(d37, plain, ~'l3$ulattices'('k11$ugroup$u4'(sK121)) | ~'l3$ulattices'('k11$ugroup$u4'(sK122)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)) | ~'Ts62'(sK121), inference(resolution, [status(thm)], [d36,c62])).
% 24.25/3.75 cnf(d38, plain, 'v3$ustruct$u0'(sK121) | ~'l1$ugroup$u1'(sK121) | ~'v3$ugroup$u1'(sK121) | 'Ts62'(sK121), inference(resolution, [status(thm)], [c53,c113])).
% 24.25/3.75 cnf(d39, plain, ~'l1$ugroup$u1'(sK121) | ~'v3$ugroup$u1'(sK121) | 'Ts62'(sK121), inference(resolution, [status(thm)], [c111,d38])).
% 24.25/3.75 cnf(d40, plain, ~'l1$ugroup$u1'(sK121) | 'Ts62'(sK121), inference(resolution, [status(thm)], [c112,d39])).
% 24.25/3.75 cnf(d41, plain, 'Ts62'(sK121), inference(resolution, [status(thm)], [c114,d40])).
% 24.25/3.75 cnf(d42, plain, ~'l3$ulattices'('k11$ugroup$u4'(sK121)) | ~'l3$ulattices'('k11$ugroup$u4'(sK122)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)), inference(resolution, [status(thm)], [d41,d37])).
% 24.25/3.75 cnf(d43, plain, ~'l3$ulattices'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)) | 'v3$ustruct$u0'(sK122) | ~'l1$ugroup$u1'(sK122) | ~'v3$ugroup$u1'(sK122) | ~'v4$ugroup$u1'(sK122), inference(resolution, [status(thm)], [d42,c17])).
% 24.25/3.75 cnf(d44, plain, ~'l3$ulattices'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)) | ~'l1$ugroup$u1'(sK122) | ~'v3$ugroup$u1'(sK122) | ~'v4$ugroup$u1'(sK122), inference(resolution, [status(thm)], [c115,d43])).
% 24.25/3.75 cnf(d45, plain, ~'l3$ulattices'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)) | ~'l1$ugroup$u1'(sK122) | ~'v4$ugroup$u1'(sK122), inference(resolution, [status(thm)], [c116,d44])).
% 24.25/3.75 cnf(d46, plain, ~'l3$ulattices'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)) | ~'l1$ugroup$u1'(sK122), inference(resolution, [status(thm)], [c117,d45])).
% 24.25/3.75 cnf(d47, plain, ~'l3$ulattices'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)), inference(resolution, [status(thm)], [c118,d46])).
% 24.25/3.75 cnf(d48, plain, 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)) | 'v3$ustruct$u0'(sK121) | ~'l1$ugroup$u1'(sK121) | ~'v3$ugroup$u1'(sK121) | ~'v4$ugroup$u1'(sK121), inference(resolution, [status(thm)], [d47,c17])).
% 24.25/3.75 cnf(d49, plain, 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)) | ~'l1$ugroup$u1'(sK121) | ~'v3$ugroup$u1'(sK121) | ~'v4$ugroup$u1'(sK121), inference(resolution, [status(thm)], [c111,d48])).
% 24.25/3.75 cnf(d50, plain, 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)) | ~'l1$ugroup$u1'(sK121) | ~'v4$ugroup$u1'(sK121), inference(resolution, [status(thm)], [c112,d49])).
% 24.25/3.75 cnf(d51, plain, 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)) | ~'l1$ugroup$u1'(sK121), inference(resolution, [status(thm)], [c113,d50])).
% 24.25/3.75 cnf(d52, plain, 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | 'v3$ustruct$u0'('k11$ugroup$u4'(sK122)), inference(resolution, [status(thm)], [c114,d51])).
% 24.25/3.75 cnf(d53, plain, 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)) | ~'Ts62'(sK122), inference(resolution, [status(thm)], [d52,c54])).
% 24.25/3.75 cnf(d54, plain, 'v3$ustruct$u0'('k11$ugroup$u4'(sK121)), inference(resolution, [status(thm)], [d35,d53])).
% 24.25/3.75 cnf(d55, plain, ~'Ts62'(sK121), inference(resolution, [status(thm)], [d54,c54])).
% 24.25/3.75 cnf(d56, plain, $false, inference(resolution, [status(thm)], [d41,d55])).
% 24.25/3.75 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------