%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : LAT351+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 : n020.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:26 AM UTC 2026
% Result : Theorem 112.05s 22.96s
% Output : CNFRefutation 112.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT351+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/5.58 % Computer : n020.cluster.edu
% 0.10/5.58 % Model : x86_64 x86_64
% 0.10/5.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.58 % Memory : 8046.5625MB
% 0.10/5.58 % OS : Linux 6.8.0-71-generic
% 0.10/5.58 % CPULimit : 300
% 0.10/5.58 % WCLimit : 300
% 0.10/5.58 % DateTime : Fri Sep 25 21:12:54 UTC 2026
% 0.10/5.59 % CPUTime :
% 0.10/5.59 Running casc-portfolio.sh -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 112.05/22.96 % SZS status Theorem for theBenchmark.p
% 112.05/22.96 % SZS output start CNFRefutation for theBenchmark.p
% 112.05/22.96 fof(dt_k2_yellow_1, axiom, ! [X0] : (('v1$uorders$u2'('k2$uyellow$u1'(X0)) & 'l1$uorders$u2'('k2$uyellow$u1'(X0))))).
% 112.05/22.96 fof(dt_k3_yellow_1, axiom, ! [X0] : (('v1$uorders$u2'('k3$uyellow$u1'(X0)) & 'l1$uorders$u2'('k3$uyellow$u1'(X0))))).
% 112.05/22.96 fof(fc14_waybel_8, axiom, ! [X0] : ((~'v3$ustruct$u0'('k3$uyellow$u1'(X0)) & ('v1$uorders$u2'('k3$uyellow$u1'(X0)) & ('v2$uorders$u2'('k3$uyellow$u1'(X0)) & ('v3$uorders$u2'('k3$uyellow$u1'(X0)) & ('v4$uorders$u2'('k3$uyellow$u1'(X0)) & ('v1$ulattice3'('k3$uyellow$u1'(X0)) & ('v2$ulattice3'('k3$uyellow$u1'(X0)) & ('v3$ulattice3'('k3$uyellow$u1'(X0)) & ('v1$uyellow$u0'('k3$uyellow$u1'(X0)) & ('v2$uyellow$u0'('k3$uyellow$u1'(X0)) & ('v3$uyellow$u0'('k3$uyellow$u1'(X0)) & ('v24$uwaybel$u0'('k3$uyellow$u1'(X0)) & ('v25$uwaybel$u0'('k3$uyellow$u1'(X0)) & ('v2$uwaybel$u1'('k3$uyellow$u1'(X0)) & ('v9$uwaybel$u1'('k3$uyellow$u1'(X0)) & ('v10$uwaybel$u1'('k3$uyellow$u1'(X0)) & ('v11$uwaybel$u1'('k3$uyellow$u1'(X0)) & ('v2$uwaybel$u3'('k3$uyellow$u1'(X0)) & ('v3$uwaybel$u3'('k3$uyellow$u1'(X0)) & ('v1$uwaybel$u8'('k3$uyellow$u1'(X0)) & 'v2$uwaybel$u8'('k3$uyellow$u1'(X0)))))))))))))))))))))))).
% 112.05/22.96 fof(fc1_waybel22, axiom, ! [X0] : (((~'v3$ustruct$u0'(X0) & ('v2$uorders$u2'(X0) & ('v3$uorders$u2'(X0) & ('v4$uorders$u2'(X0) & ('v2$uyellow$u0'(X0) & ('v2$ulattice3'(X0) & 'l1$uorders$u2'(X0))))))) => (~'v3$ustruct$u0'('k2$uyellow$u1'('k9$uwaybel$u0'(X0))) & ('v1$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'(X0))) & ('v2$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'(X0))) & ('v3$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'(X0))) & ('v4$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'(X0))) & ('v1$uyellow$u0'('k2$uyellow$u1'('k9$uwaybel$u0'(X0))) & ('v2$uyellow$u0'('k2$uyellow$u1'('k9$uwaybel$u0'(X0))) & ('v3$uyellow$u0'('k2$uyellow$u1'('k9$uwaybel$u0'(X0))) & ('v24$uwaybel$u0'('k2$uyellow$u1'('k9$uwaybel$u0'(X0))) & ('v25$uwaybel$u0'('k2$uyellow$u1'('k9$uwaybel$u0'(X0))) & ('v1$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'(X0))) & ('v2$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'(X0))) & ('v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'(X0))) & 'v3$uwaybel$u3'('k2$uyellow$u1'('k9$uwaybel$u0'(X0))))))))))))))))))).
% 112.05/22.96 fof(fc2_waybel16, axiom, ! [X0] : ((('v2$uorders$u2'(X0) & ('v3$uorders$u2'(X0) & ('v4$uorders$u2'(X0) & ('v2$ulattice3'(X0) & ('v2$uyellow$u0'(X0) & 'l1$uorders$u2'(X0)))))) => (~'v3$ustruct$u0'('k2$uyellow$u1'('k9$uwaybel$u0'(X0))) & ('v1$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'(X0))) & ('v2$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'(X0))) & ('v3$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'(X0))) & ('v4$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'(X0))) & ('v2$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'(X0))) & ('v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'(X0))) & ('v1$uyellow$u0'('k2$uyellow$u1'('k9$uwaybel$u0'(X0))) & ('v24$uwaybel$u0'('k2$uyellow$u1'('k9$uwaybel$u0'(X0))) & 'v25$uwaybel$u0'('k2$uyellow$u1'('k9$uwaybel$u0'(X0))))))))))))))).
% 112.05/22.96 fof(t10_waybel22, axiom, ! [X0] : 'k1$ucard$u1'('k1$uwaybel22'(X0)) = 'k1$ucard$u1'(X0)).
% 112.05/22.96 fof(t16_waybel22, axiom, ! [X0] : 'r1$uwaybel22'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(X0))),'k1$uwaybel22'(X0))).
% 112.05/22.96 fof(t17_waybel22, axiom, ! [X0] : ((('v2$uorders$u2'(X0) & ('v3$uorders$u2'(X0) & ('v4$uorders$u2'(X0) & ('v1$ulattice3'(X0) & ('v2$ulattice3'(X0) & ('v3$ulattice3'(X0) & ('v3$uwaybel$u3'(X0) & 'l1$uorders$u2'(X0)))))))) => ! [X1] : ((('v2$uorders$u2'(X1) & ('v3$uorders$u2'(X1) & ('v4$uorders$u2'(X1) & ('v1$ulattice3'(X1) & ('v2$ulattice3'(X1) & ('v3$ulattice3'(X1) & ('v3$uwaybel$u3'(X1) & 'l1$uorders$u2'(X1)))))))) => ! [X2] : ! [X3] : ((('r1$uwaybel22'(X0,X2) & ('r1$uwaybel22'(X1,X3) & 'k1$ucard$u1'(X2) = 'k1$ucard$u1'(X3))) => 'r5$uwaybel$u1'(X0,X1)))))))).
% 112.05/22.96 fof(t18_waybel22, conjecture, ! [X0] : ! [X1] : ((('v2$uorders$u2'(X1) & ('v3$uorders$u2'(X1) & ('v4$uorders$u2'(X1) & ('v1$ulattice3'(X1) & ('v2$ulattice3'(X1) & ('v3$ulattice3'(X1) & ('v3$uwaybel$u3'(X1) & 'l1$uorders$u2'(X1)))))))) => ! [X2] : ((('r1$uwaybel22'(X1,X2) & 'k1$ucard$u1'(X2) = 'k1$ucard$u1'(X0)) => 'r5$uwaybel$u1'(X1,'k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(X0))))))))).
% 112.05/22.96 fof(negated_conjecture, negated_conjecture, ~! [X0] : ! [X1] : ((('v2$uorders$u2'(X1) & ('v3$uorders$u2'(X1) & ('v4$uorders$u2'(X1) & ('v1$ulattice3'(X1) & ('v2$ulattice3'(X1) & ('v3$ulattice3'(X1) & ('v3$uwaybel$u3'(X1) & 'l1$uorders$u2'(X1)))))))) => ! [X2] : ((('r1$uwaybel22'(X1,X2) & 'k1$ucard$u1'(X2) = 'k1$ucard$u1'(X0)) => 'r5$uwaybel$u1'(X1,'k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(X0)))))))), inference(negate_conjecture, [status(cth)], [t18_waybel22])).
% 112.05/22.96 cnf(c148, plain, 'l1$uorders$u2'('k2$uyellow$u1'(X0)), inference(clausification, [status(esa)], [dt_k2_yellow_1])).
% 112.05/22.96 cnf(c150, plain, 'l1$uorders$u2'('k3$uyellow$u1'(X0)), inference(clausification, [status(esa)], [dt_k3_yellow_1])).
% 112.05/22.96 cnf(c192, plain, ~'v3$ustruct$u0'('k3$uyellow$u1'(X0)), inference(clausification, [status(esa)], [fc14_waybel_8])).
% 112.05/22.96 cnf(c194, plain, 'v2$uorders$u2'('k3$uyellow$u1'(X0)), inference(clausification, [status(esa)], [fc14_waybel_8])).
% 112.05/22.96 cnf(c195, plain, 'v3$uorders$u2'('k3$uyellow$u1'(X0)), inference(clausification, [status(esa)], [fc14_waybel_8])).
% 112.05/22.96 cnf(c196, plain, 'v4$uorders$u2'('k3$uyellow$u1'(X0)), inference(clausification, [status(esa)], [fc14_waybel_8])).
% 112.05/22.96 cnf(c198, plain, 'v2$ulattice3'('k3$uyellow$u1'(X0)), inference(clausification, [status(esa)], [fc14_waybel_8])).
% 112.05/22.96 cnf(c201, plain, 'v2$uyellow$u0'('k3$uyellow$u1'(X0)), inference(clausification, [status(esa)], [fc14_waybel_8])).
% 112.05/22.96 cnf(c218, plain, ~'v2$uorders$u2'(X0) | X1(X0) | ~'l1$uorders$u2'(X0) | ~'v4$uorders$u2'(X0) | 'v3$ustruct$u0'(X0) | ~'v2$uyellow$u0'(X0) | ~'v3$uorders$u2'(X0) | ~'v2$ulattice3'(X0), inference(clausification, [status(esa)], [fc1_waybel22])).
% 112.05/22.96 cnf(c221, plain, ~X0(X1) | 'v2$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'(X1))), inference(clausification, [status(esa)], [fc1_waybel22])).
% 112.05/22.96 cnf(c222, plain, ~X0(X1) | 'v3$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'(X1))), inference(clausification, [status(esa)], [fc1_waybel22])).
% 112.05/22.96 cnf(c223, plain, ~X0(X1) | 'v4$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'(X1))), inference(clausification, [status(esa)], [fc1_waybel22])).
% 112.05/22.96 cnf(c229, plain, ~X0(X1) | 'v1$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'(X1))), inference(clausification, [status(esa)], [fc1_waybel22])).
% 112.05/22.96 cnf(c232, plain, ~X0(X1) | 'v3$uwaybel$u3'('k2$uyellow$u1'('k9$uwaybel$u0'(X1))), inference(clausification, [status(esa)], [fc1_waybel22])).
% 112.05/22.96 cnf(c240, plain, ~'v4$uorders$u2'(X0) | ~'l1$uorders$u2'(X0) | ~'v2$ulattice3'(X0) | ~'v3$uorders$u2'(X0) | ~'v2$uorders$u2'(X0) | X1(X0) | ~'v2$uyellow$u0'(X0), inference(clausification, [status(esa)], [fc2_waybel16])).
% 112.05/22.96 cnf(c246, plain, ~X0(X1) | 'v2$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'(X1))), inference(clausification, [status(esa)], [fc2_waybel16])).
% 112.05/22.96 cnf(c247, plain, ~X0(X1) | 'v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'(X1))), inference(clausification, [status(esa)], [fc2_waybel16])).
% 112.05/22.96 cnf(c398, plain, 'k1$ucard$u1'('k1$uwaybel22'(X0)) = 'k1$ucard$u1'(X0), inference(clausification, [status(esa)], [t10_waybel22])).
% 112.05/22.96 cnf(c399, plain, 'r1$uwaybel22'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(X0))),'k1$uwaybel22'(X0)), inference(clausification, [status(esa)], [t16_waybel22])).
% 112.05/22.96 cnf(c400, plain, ~'l1$uorders$u2'(X0) | ~'v4$uorders$u2'(X1) | ~'v2$uorders$u2'(X0) | ~'v4$uorders$u2'(X0) | 'r5$uwaybel$u1'(X0,X1) | ~'v3$uorders$u2'(X1) | ~'r1$uwaybel22'(X1,X2) | ~'v2$uorders$u2'(X1) | ~'v3$ulattice3'(X1) | ~'v3$uwaybel$u3'(X1) | ~'v1$ulattice3'(X0) | ~'v2$ulattice3'(X1) | ~'r1$uwaybel22'(X0,X3) | ~'v1$ulattice3'(X1) | ~'v3$uorders$u2'(X0) | 'k1$ucard$u1'(X3) != 'k1$ucard$u1'(X2) | ~'v3$uwaybel$u3'(X0) | ~'v3$ulattice3'(X0) | ~'v2$ulattice3'(X0) | ~'l1$uorders$u2'(X1), inference(clausification, [status(esa)], [t17_waybel22])).
% 112.05/22.96 cnf(c414, plain, 'v2$uorders$u2'(sK185), inference(clausification, [status(esa)], [negated_conjecture])).
% 112.05/22.96 cnf(c415, plain, 'v3$uorders$u2'(sK185), inference(clausification, [status(esa)], [negated_conjecture])).
% 112.05/22.96 cnf(c416, plain, 'v4$uorders$u2'(sK185), inference(clausification, [status(esa)], [negated_conjecture])).
% 112.05/22.96 cnf(c417, plain, 'v1$ulattice3'(sK185), inference(clausification, [status(esa)], [negated_conjecture])).
% 112.05/22.96 cnf(c418, plain, 'v2$ulattice3'(sK185), inference(clausification, [status(esa)], [negated_conjecture])).
% 112.05/22.96 cnf(c419, plain, 'v3$ulattice3'(sK185), inference(clausification, [status(esa)], [negated_conjecture])).
% 112.05/22.96 cnf(c420, plain, 'v3$uwaybel$u3'(sK185), inference(clausification, [status(esa)], [negated_conjecture])).
% 112.05/22.96 cnf(c421, plain, 'l1$uorders$u2'(sK185), inference(clausification, [status(esa)], [negated_conjecture])).
% 112.05/22.96 cnf(c422, plain, 'r1$uwaybel22'(sK185,sK186), inference(clausification, [status(esa)], [negated_conjecture])).
% 112.05/22.96 cnf(c423, plain, 'k1$ucard$u1'(sK186) = 'k1$ucard$u1'(sK184), inference(clausification, [status(esa)], [negated_conjecture])).
% 112.05/22.96 cnf(c424, plain, ~'r5$uwaybel$u1'(sK185,'k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))), inference(clausification, [status(esa)], [negated_conjecture])).
% 112.05/22.96 cnf(d0, plain, 'k1$ucard$u1'(X1) != 'k1$ucard$u1'(X0) | ~'l1$uorders$u2'(X2) | ~'l1$uorders$u2'(X3) | ~'v3$ulattice3'(X2) | ~'v3$ulattice3'(X3) | ~'v2$uorders$u2'(X2) | ~'v2$uorders$u2'(X3) | ~'v3$uorders$u2'(X2) | ~'v3$uorders$u2'(X3) | ~'v4$uorders$u2'(X2) | ~'v4$uorders$u2'(X3) | ~'v1$ulattice3'(X2) | ~'v1$ulattice3'(X3) | ~'v2$ulattice3'(X2) | ~'v2$ulattice3'(X3) | ~'v3$uwaybel$u3'(X2) | ~'v3$uwaybel$u3'(X3) | 'r5$uwaybel$u1'(X2,X3) | ~'r1$uwaybel22'(X2,X1) | ~'r1$uwaybel22'(X3,'k1$uwaybel22'(X0)), inference(superposition, [status(thm)], [c398,c400])).
% 112.05/22.96 cnf(d1, plain, 'k1$ucard$u1'(X0) != 'k1$ucard$u1'(sK186) | ~'l1$uorders$u2'(X1) | ~'l1$uorders$u2'(X2) | ~'v3$ulattice3'(X1) | ~'v3$ulattice3'(X2) | ~'v2$uorders$u2'(X1) | ~'v2$uorders$u2'(X2) | ~'v3$uorders$u2'(X1) | ~'v3$uorders$u2'(X2) | ~'v4$uorders$u2'(X1) | ~'v4$uorders$u2'(X2) | ~'v1$ulattice3'(X1) | ~'v1$ulattice3'(X2) | ~'v2$ulattice3'(X1) | ~'v2$ulattice3'(X2) | ~'v3$uwaybel$u3'(X1) | ~'v3$uwaybel$u3'(X2) | 'r5$uwaybel$u1'(X2,X1) | ~'r1$uwaybel22'(X1,'k1$uwaybel22'(sK184)) | ~'r1$uwaybel22'(X2,X0), inference(superposition, [status(thm)], [c423,d0])).
% 112.05/22.96 cnf(d2, plain, ~'l1$uorders$u2'(X0) | ~'l1$uorders$u2'(X1) | ~'v3$ulattice3'(X0) | ~'v3$ulattice3'(X1) | ~'v2$uorders$u2'(X0) | ~'v2$uorders$u2'(X1) | ~'v3$uorders$u2'(X0) | ~'v3$uorders$u2'(X1) | ~'v4$uorders$u2'(X0) | ~'v4$uorders$u2'(X1) | ~'v1$ulattice3'(X0) | ~'v1$ulattice3'(X1) | ~'v2$ulattice3'(X0) | ~'v2$ulattice3'(X1) | ~'v3$uwaybel$u3'(X0) | ~'v3$uwaybel$u3'(X1) | 'r5$uwaybel$u1'(X0,X1) | ~'r1$uwaybel22'(X0,sK186) | ~'r1$uwaybel22'(X1,'k1$uwaybel22'(sK184)), inference(equality_resolution, [status(thm)], [d1])).
% 112.05/22.96 cnf(d3, plain, ~'l1$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'l1$uorders$u2'(X0) | ~'v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$ulattice3'(X0) | ~'v2$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$uorders$u2'(X0) | ~'v3$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uorders$u2'(X0) | ~'v4$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v4$uorders$u2'(X0) | ~'v1$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v1$ulattice3'(X0) | ~'v2$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$ulattice3'(X0) | ~'v3$uwaybel$u3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uwaybel$u3'(X0) | 'r5$uwaybel$u1'(X0,'k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'r1$uwaybel22'(X0,sK186), inference(resolution, [status(thm)], [d2,c399])).
% 112.05/22.96 cnf(d4, plain, ~'l1$uorders$u2'(X0) | ~'v3$ulattice3'(X0) | ~'v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$uorders$u2'(X0) | ~'v2$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uorders$u2'(X0) | ~'v3$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v4$uorders$u2'(X0) | ~'v4$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v1$ulattice3'(X0) | ~'v1$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$ulattice3'(X0) | ~'v2$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uwaybel$u3'(X0) | ~'v3$uwaybel$u3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | 'r5$uwaybel$u1'(X0,'k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'r1$uwaybel22'(X0,sK186), inference(resolution, [status(thm)], [c148,d3])).
% 112.05/22.96 cnf(d5, plain, ~'l1$uorders$u2'(sK185) | ~'v3$ulattice3'(sK185) | ~'v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$uorders$u2'(sK185) | ~'v2$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uorders$u2'(sK185) | ~'v3$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v4$uorders$u2'(sK185) | ~'v4$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v1$ulattice3'(sK185) | ~'v1$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$ulattice3'(sK185) | ~'v2$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uwaybel$u3'(sK185) | ~'v3$uwaybel$u3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'r1$uwaybel22'(sK185,sK186), inference(resolution, [status(thm)], [d4,c424])).
% 112.05/22.96 cnf(d6, plain, ~'l1$uorders$u2'(sK185) | ~'v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$ulattice3'(sK185) | ~'v2$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uorders$u2'(sK185) | ~'v4$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v4$uorders$u2'(sK185) | ~'v1$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v1$ulattice3'(sK185) | ~'v2$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$ulattice3'(sK185) | ~'v3$uwaybel$u3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uwaybel$u3'(sK185) | ~'r1$uwaybel22'(sK185,sK186), inference(resolution, [status(thm)], [c414,d5])).
% 112.05/22.96 cnf(d7, plain, ~'l1$uorders$u2'(sK185) | ~'v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$ulattice3'(sK185) | ~'v2$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v4$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v4$uorders$u2'(sK185) | ~'v1$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v1$ulattice3'(sK185) | ~'v2$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$ulattice3'(sK185) | ~'v3$uwaybel$u3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uwaybel$u3'(sK185) | ~'r1$uwaybel22'(sK185,sK186), inference(resolution, [status(thm)], [c415,d6])).
% 112.05/22.96 cnf(d8, plain, ~'l1$uorders$u2'(sK185) | ~'v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$ulattice3'(sK185) | ~'v2$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v4$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v1$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v1$ulattice3'(sK185) | ~'v2$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$ulattice3'(sK185) | ~'v3$uwaybel$u3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uwaybel$u3'(sK185) | ~'r1$uwaybel22'(sK185,sK186), inference(resolution, [status(thm)], [c416,d7])).
% 112.05/22.96 cnf(d9, plain, ~'l1$uorders$u2'(sK185) | ~'v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$ulattice3'(sK185) | ~'v2$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v4$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v1$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$ulattice3'(sK185) | ~'v3$uwaybel$u3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uwaybel$u3'(sK185) | ~'r1$uwaybel22'(sK185,sK186), inference(resolution, [status(thm)], [c417,d8])).
% 112.05/22.96 cnf(d10, plain, ~'l1$uorders$u2'(sK185) | ~'v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$ulattice3'(sK185) | ~'v2$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v4$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v1$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uwaybel$u3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uwaybel$u3'(sK185) | ~'r1$uwaybel22'(sK185,sK186), inference(resolution, [status(thm)], [c418,d9])).
% 112.05/22.96 cnf(d11, plain, ~'l1$uorders$u2'(sK185) | ~'v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v4$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v1$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uwaybel$u3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uwaybel$u3'(sK185) | ~'r1$uwaybel22'(sK185,sK186), inference(resolution, [status(thm)], [c419,d10])).
% 112.05/22.96 cnf(d12, plain, ~'l1$uorders$u2'(sK185) | ~'v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v4$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v1$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uwaybel$u3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'r1$uwaybel22'(sK185,sK186), inference(resolution, [status(thm)], [c420,d11])).
% 112.05/22.96 cnf(d13, plain, ~'v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v4$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v1$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uwaybel$u3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'r1$uwaybel22'(sK185,sK186), inference(resolution, [status(thm)], [c421,d12])).
% 112.05/22.96 cnf(d14, plain, ~'v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v4$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v1$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uwaybel$u3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))), inference(resolution, [status(thm)], [c422,d13])).
% 112.05/22.96 cnf(d15, plain, ~'v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v4$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v1$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'Ts92'('k3$uyellow$u1'(sK184)), inference(resolution, [status(thm)], [d14,c232])).
% 112.05/22.96 cnf(d16, plain, ~'l1$uorders$u2'('k3$uyellow$u1'(X0)) | 'v3$ustruct$u0'('k3$uyellow$u1'(X0)) | ~'v2$uorders$u2'('k3$uyellow$u1'(X0)) | ~'v3$uorders$u2'('k3$uyellow$u1'(X0)) | ~'v4$uorders$u2'('k3$uyellow$u1'(X0)) | ~'v2$ulattice3'('k3$uyellow$u1'(X0)) | 'Ts92'('k3$uyellow$u1'(X0)), inference(resolution, [status(thm)], [c218,c201])).
% 112.05/22.96 cnf(d17, plain, 'v3$ustruct$u0'('k3$uyellow$u1'(X0)) | ~'v2$uorders$u2'('k3$uyellow$u1'(X0)) | ~'v3$uorders$u2'('k3$uyellow$u1'(X0)) | ~'v4$uorders$u2'('k3$uyellow$u1'(X0)) | ~'v2$ulattice3'('k3$uyellow$u1'(X0)) | 'Ts92'('k3$uyellow$u1'(X0)), inference(resolution, [status(thm)], [c150,d16])).
% 112.05/22.96 cnf(d18, plain, ~'v2$uorders$u2'('k3$uyellow$u1'(X0)) | ~'v3$uorders$u2'('k3$uyellow$u1'(X0)) | ~'v4$uorders$u2'('k3$uyellow$u1'(X0)) | ~'v2$ulattice3'('k3$uyellow$u1'(X0)) | 'Ts92'('k3$uyellow$u1'(X0)), inference(resolution, [status(thm)], [c192,d17])).
% 112.05/22.96 cnf(d19, plain, ~'v3$uorders$u2'('k3$uyellow$u1'(X0)) | ~'v4$uorders$u2'('k3$uyellow$u1'(X0)) | ~'v2$ulattice3'('k3$uyellow$u1'(X0)) | 'Ts92'('k3$uyellow$u1'(X0)), inference(resolution, [status(thm)], [c194,d18])).
% 112.05/22.96 cnf(d20, plain, ~'v4$uorders$u2'('k3$uyellow$u1'(X0)) | ~'v2$ulattice3'('k3$uyellow$u1'(X0)) | 'Ts92'('k3$uyellow$u1'(X0)), inference(resolution, [status(thm)], [c195,d19])).
% 112.05/22.96 cnf(d21, plain, ~'v2$ulattice3'('k3$uyellow$u1'(X0)) | 'Ts92'('k3$uyellow$u1'(X0)), inference(resolution, [status(thm)], [c196,d20])).
% 112.05/22.96 cnf(d22, plain, 'Ts92'('k3$uyellow$u1'(X0)), inference(resolution, [status(thm)], [c198,d21])).
% 112.05/22.96 cnf(d23, plain, ~'v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v4$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v1$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))), inference(resolution, [status(thm)], [d22,d15])).
% 112.05/22.96 cnf(d24, plain, ~'v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v4$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v1$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'Ts98'('k3$uyellow$u1'(sK184)), inference(resolution, [status(thm)], [d23,c246])).
% 112.05/22.96 cnf(d25, plain, ~'l1$uorders$u2'('k3$uyellow$u1'(X0)) | ~'v2$uorders$u2'('k3$uyellow$u1'(X0)) | ~'v3$uorders$u2'('k3$uyellow$u1'(X0)) | ~'v4$uorders$u2'('k3$uyellow$u1'(X0)) | ~'v2$ulattice3'('k3$uyellow$u1'(X0)) | 'Ts98'('k3$uyellow$u1'(X0)), inference(resolution, [status(thm)], [c240,c201])).
% 112.05/22.96 cnf(d26, plain, ~'v2$uorders$u2'('k3$uyellow$u1'(X0)) | ~'v3$uorders$u2'('k3$uyellow$u1'(X0)) | ~'v4$uorders$u2'('k3$uyellow$u1'(X0)) | ~'v2$ulattice3'('k3$uyellow$u1'(X0)) | 'Ts98'('k3$uyellow$u1'(X0)), inference(resolution, [status(thm)], [c150,d25])).
% 112.05/22.96 cnf(d27, plain, ~'v3$uorders$u2'('k3$uyellow$u1'(X0)) | ~'v4$uorders$u2'('k3$uyellow$u1'(X0)) | ~'v2$ulattice3'('k3$uyellow$u1'(X0)) | 'Ts98'('k3$uyellow$u1'(X0)), inference(resolution, [status(thm)], [c194,d26])).
% 112.05/22.96 cnf(d28, plain, ~'v4$uorders$u2'('k3$uyellow$u1'(X0)) | ~'v2$ulattice3'('k3$uyellow$u1'(X0)) | 'Ts98'('k3$uyellow$u1'(X0)), inference(resolution, [status(thm)], [c195,d27])).
% 112.05/22.96 cnf(d29, plain, ~'v2$ulattice3'('k3$uyellow$u1'(X0)) | 'Ts98'('k3$uyellow$u1'(X0)), inference(resolution, [status(thm)], [c196,d28])).
% 112.05/22.96 cnf(d30, plain, 'Ts98'('k3$uyellow$u1'(X0)), inference(resolution, [status(thm)], [c198,d29])).
% 112.05/22.96 cnf(d31, plain, ~'v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v4$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v1$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))), inference(resolution, [status(thm)], [d30,d24])).
% 112.05/22.96 cnf(d32, plain, ~'v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v4$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'Ts92'('k3$uyellow$u1'(sK184)), inference(resolution, [status(thm)], [d31,c229])).
% 112.05/22.96 cnf(d33, plain, ~'v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v4$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))), inference(resolution, [status(thm)], [d22,d32])).
% 112.05/22.96 cnf(d34, plain, ~'v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'Ts92'('k3$uyellow$u1'(sK184)), inference(resolution, [status(thm)], [d33,c223])).
% 112.05/22.96 cnf(d35, plain, ~'v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v3$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))), inference(resolution, [status(thm)], [d22,d34])).
% 112.05/22.96 cnf(d36, plain, ~'v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'Ts92'('k3$uyellow$u1'(sK184)), inference(resolution, [status(thm)], [d35,c222])).
% 112.05/22.96 cnf(d37, plain, ~'v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'v2$uorders$u2'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))), inference(resolution, [status(thm)], [d22,d36])).
% 112.05/22.96 cnf(d38, plain, ~'v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))) | ~'Ts92'('k3$uyellow$u1'(sK184)), inference(resolution, [status(thm)], [d37,c221])).
% 112.05/22.96 cnf(d39, plain, ~'v3$ulattice3'('k2$uyellow$u1'('k9$uwaybel$u0'('k3$uyellow$u1'(sK184)))), inference(resolution, [status(thm)], [d22,d38])).
% 112.05/22.96 cnf(d40, plain, ~'Ts98'('k3$uyellow$u1'(sK184)), inference(resolution, [status(thm)], [d39,c247])).
% 112.05/22.96 cnf(d41, plain, $false, inference(resolution, [status(thm)], [d30,d40])).
% 112.05/22.96 % SZS output end CNFRefutation for theBenchmark.p
%------------------------------------------------------------------------------