%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT223-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n015.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 : Fri Sep 25 01:56:21 PM UTC 2026
% Result : Unsatisfiable 175.78s 30.75s
% Output : CNFRefutation 175.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 17
% Syntax : Number of clauses : 175 ( 175 unt; 0 nHn; 68 RR)
% Number of literals : 175 ( 174 equ; 5 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 7 con; 0-4 aty)
% Number of variables : 184 ( 44 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t14,axiom,
sFlat0 = complement(b),
introduced(definition) ).
cnf(t95,plain,
complement(b) = sFlat0,
inference(orient,[status(thm)],[t14]) ).
cnf(t15,axiom,
sFlat1 = complement(a),
introduced(definition) ).
cnf(t90,plain,
complement(a) = sFlat1,
inference(orient,[status(thm)],[t15]) ).
cnf(t16,axiom,
sFlat2 = join(complement(b),complement(a)),
introduced(definition) ).
cnf(t85,plain,
join(complement(b),complement(a)) = sFlat2,
inference(orient,[status(thm)],[t16]) ).
cnf(t389647,plain,
join(complement(b),sFlat1) = sFlat2,
inference(step,[status(thm)],[t85,t90]) ).
cnf(t94,plain,
join(complement(b),sFlat1) = sFlat2,
inference(rw,[status(thm)],[t389647]) ).
cnf(t6,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t65,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t389658,plain,
join(sFlat1,complement(b)) = sFlat2,
inference(step,[status(thm)],[t94,t65]) ).
cnf(t389659,plain,
join(sFlat1,sFlat0) = sFlat2,
inference(step,[status(thm)],[t389658,t95]) ).
cnf(t389660,plain,
join(sFlat0,sFlat1) = sFlat2,
inference(step,[status(thm)],[t389659,t65]) ).
cnf(t166,plain,
join(sFlat0,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t389660]) ).
cnf(t7,axiom,
join(X1,meet(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t20,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t8,axiom,
meet(X1,X2) = meet(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t27,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t8]) ).
cnf(t28,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t20,t27]) ).
cnf(t175,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t28]) ).
cnf(t11,axiom,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t30,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
cnf(t9,axiom,
meet(X1,join(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t18,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t9]) ).
cnf(t10,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t69,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t168,plain,
join(sFlat0,join(sFlat1,X1)) = join(sFlat2,X1),
inference(cp,[status(thm)],[t69,t166]) ).
cnf(t311,plain,
join(sFlat0,join(sFlat1,X1)) = join(sFlat2,X1),
inference(orient,[status(thm)],[t168]) ).
cnf(t325,plain,
sFlat0 = meet(sFlat0,join(sFlat2,X1)),
inference(cp,[status(thm)],[t18,t311]) ).
cnf(t374,plain,
meet(sFlat0,join(sFlat2,X1)) = sFlat0,
inference(orient,[status(thm)],[t325]) ).
cnf(t377,plain,
meet(sFlat0,meet(join(sFlat2,X1),X2)) = meet(sFlat0,X2),
inference(cp,[status(thm)],[t30,t374]) ).
cnf(t2485,plain,
meet(sFlat0,meet(join(sFlat2,X1),X2)) = meet(sFlat0,X2),
inference(orient,[status(thm)],[t377]) ).
cnf(t66,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t18,t65]) ).
cnf(t188,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t66]) ).
cnf(t190,plain,
meet(X1,X2) = meet(meet(X1,X2),X1),
inference(cp,[status(thm)],[t188,t20]) ).
cnf(t389707,plain,
meet(X1,X2) = meet(X1,meet(X2,X1)),
inference(step,[status(thm)],[t190,t30]) ).
cnf(t538,plain,
meet(X1,meet(X2,X1)) = meet(X1,X2),
inference(orient,[status(thm)],[t389707]) ).
cnf(t2489,plain,
meet(sFlat0,meet(X1,join(sFlat2,X2))) = meet(sFlat0,meet(join(sFlat2,X2),X1)),
inference(cp,[status(thm)],[t2485,t538]) ).
cnf(t389861,plain,
meet(sFlat0,meet(X1,join(sFlat2,X2))) = meet(sFlat0,X1),
inference(step,[status(thm)],[t2489,t2485]) ).
cnf(t4034,plain,
meet(sFlat0,meet(X1,join(sFlat2,X2))) = meet(sFlat0,X1),
inference(orient,[status(thm)],[t389861]) ).
cnf(t4041,plain,
meet(X1,join(sFlat2,X2)) = join(meet(X1,join(sFlat2,X2)),meet(sFlat0,X1)),
inference(cp,[status(thm)],[t175,t4034]) ).
cnf(t391283,plain,
meet(X1,join(sFlat2,X2)) = join(meet(sFlat0,X1),meet(X1,join(sFlat2,X2))),
inference(step,[status(thm)],[t4041,t65]) ).
cnf(t376308,plain,
join(meet(sFlat0,X1),meet(X1,join(sFlat2,X2))) = meet(X1,join(sFlat2,X2)),
inference(orient,[status(thm)],[t391283]) ).
cnf(t1,axiom,
meet(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t17,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t34,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(cp,[status(thm)],[t30,t17]) ).
cnf(t208,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t34]) ).
cnf(t12,axiom,
ifeq(join(X1,X2),one,ifeq(meet(X1,X2),zero,complement(X1),X2),X2) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t22,plain,
ifeq(join(X1,X2),one,ifeq(meet(X1,X2),zero,complement(X1),X2),X2) = X2,
inference(orient,[status(thm)],[t12]) ).
cnf(t177,plain,
join(X1,X2) = join(join(X1,X2),X1),
inference(cp,[status(thm)],[t175,t18]) ).
cnf(t389686,plain,
join(X1,X2) = join(X1,join(X2,X1)),
inference(step,[status(thm)],[t177,t69]) ).
cnf(t398,plain,
join(X1,join(X2,X1)) = join(X1,X2),
inference(orient,[status(thm)],[t389686]) ).
cnf(t3,axiom,
join(X1,complement(X1)) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t80,plain,
join(X1,complement(X1)) = one,
inference(orient,[status(thm)],[t3]) ).
cnf(t83,plain,
join(X1,join(complement(X1),X2)) = join(one,X2),
inference(cp,[status(thm)],[t69,t80]) ).
cnf(t82,plain,
X1 = meet(X1,one),
inference(cp,[status(thm)],[t18,t80]) ).
cnf(t108,plain,
meet(X1,one) = X1,
inference(orient,[status(thm)],[t82]) ).
cnf(t109,plain,
X1 = meet(one,X1),
inference(cp,[status(thm)],[t108,t27]) ).
cnf(t142,plain,
meet(one,X1) = X1,
inference(orient,[status(thm)],[t109]) ).
cnf(t144,plain,
join(one,X1) = one,
inference(cp,[status(thm)],[t142,t18]) ).
cnf(t157,plain,
join(one,X1) = one,
inference(orient,[status(thm)],[t144]) ).
cnf(t389780,plain,
join(X1,join(complement(X1),X2)) = one,
inference(step,[status(thm)],[t83,t157]) ).
cnf(t1199,plain,
join(X1,join(complement(X1),X2)) = one,
inference(orient,[status(thm)],[t389780]) ).
cnf(t1202,plain,
join(join(complement(X1),X2),X1) = join(join(complement(X1),X2),one),
inference(cp,[status(thm)],[t398,t1199]) ).
cnf(t389782,plain,
join(complement(X1),join(X2,X1)) = join(join(complement(X1),X2),one),
inference(step,[status(thm)],[t1202,t69]) ).
cnf(t389783,plain,
join(complement(X1),join(X2,X1)) = join(complement(X1),join(X2,one)),
inference(step,[status(thm)],[t389782,t69]) ).
cnf(t158,plain,
one = join(X1,one),
inference(cp,[status(thm)],[t157,t65]) ).
cnf(t164,plain,
join(X1,one) = one,
inference(orient,[status(thm)],[t158]) ).
cnf(t389784,plain,
join(complement(X1),join(X2,X1)) = join(complement(X1),one),
inference(step,[status(thm)],[t389783,t164]) ).
cnf(t389785,plain,
join(complement(X1),join(X2,X1)) = one,
inference(step,[status(thm)],[t389784,t164]) ).
cnf(t1271,plain,
join(complement(X1),join(X2,X1)) = one,
inference(orient,[status(thm)],[t389785]) ).
cnf(t1277,plain,
one = join(complement(meet(X1,X2)),X2),
inference(cp,[status(thm)],[t1271,t175]) ).
cnf(t389787,plain,
one = join(X2,complement(meet(X1,X2))),
inference(step,[status(thm)],[t1277,t65]) ).
cnf(t1323,plain,
join(X1,complement(meet(X2,X1))) = one,
inference(orient,[status(thm)],[t389787]) ).
cnf(t13,axiom,
meet(X1,join(X2,meet(X1,join(meet(X1,X2),meet(X3,join(X1,X2)))))) = meet(X1,join(X2,meet(X1,X3))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t39,plain,
meet(X1,join(X2,meet(X1,join(meet(X1,X2),meet(X3,join(X1,X2)))))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t13]) ).
cnf(t2,axiom,
meet(b,a) = a,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t60,plain,
meet(b,a) = a,
inference(orient,[status(thm)],[t2]) ).
cnf(t62,plain,
b = join(b,a),
inference(cp,[status(thm)],[t20,t60]) ).
cnf(t104,plain,
join(b,a) = b,
inference(orient,[status(thm)],[t62]) ).
cnf(t105,plain,
join(b,join(a,X1)) = join(b,X1),
inference(cp,[status(thm)],[t69,t104]) ).
cnf(t236,plain,
join(b,join(a,X1)) = join(b,X1),
inference(orient,[status(thm)],[t105]) ).
cnf(t237,plain,
join(b,complement(a)) = join(b,one),
inference(cp,[status(thm)],[t236,t80]) ).
cnf(t389669,plain,
join(b,sFlat1) = join(b,one),
inference(step,[status(thm)],[t237,t90]) ).
cnf(t389670,plain,
join(sFlat1,b) = join(b,one),
inference(step,[status(thm)],[t389669,t65]) ).
cnf(t389671,plain,
join(sFlat1,b) = one,
inference(step,[status(thm)],[t389670,t164]) ).
cnf(t242,plain,
join(sFlat1,b) = one,
inference(orient,[status(thm)],[t389671]) ).
cnf(t245,plain,
meet(sFlat1,join(b,meet(sFlat1,X1))) = meet(sFlat1,join(b,meet(sFlat1,join(meet(sFlat1,b),meet(X1,one))))),
inference(cp,[status(thm)],[t39,t242]) ).
cnf(t391289,plain,
meet(sFlat1,join(b,meet(sFlat1,X1))) = meet(sFlat1,join(b,meet(sFlat1,join(meet(sFlat1,b),X1)))),
inference(step,[status(thm)],[t245,t108]) ).
cnf(t387843,plain,
meet(sFlat1,join(b,meet(sFlat1,join(meet(sFlat1,b),X1)))) = meet(sFlat1,join(b,meet(sFlat1,X1))),
inference(orient,[status(thm)],[t391289]) ).
cnf(t1325,plain,
one = join(meet(X1,X2),complement(meet(X2,X1))),
inference(cp,[status(thm)],[t1323,t538]) ).
cnf(t6608,plain,
join(meet(X1,X2),complement(meet(X2,X1))) = one,
inference(orient,[status(thm)],[t1325]) ).
cnf(t387860,plain,
meet(sFlat1,join(b,meet(sFlat1,complement(meet(b,sFlat1))))) = meet(sFlat1,join(b,meet(sFlat1,one))),
inference(cp,[status(thm)],[t387843,t6608]) ).
cnf(t391290,plain,
meet(sFlat1,join(b,meet(sFlat1,complement(meet(sFlat1,b))))) = meet(sFlat1,join(b,meet(sFlat1,one))),
inference(step,[status(thm)],[t387860,t27]) ).
cnf(t391291,plain,
meet(sFlat1,join(b,meet(sFlat1,complement(meet(sFlat1,b))))) = meet(sFlat1,join(b,sFlat1)),
inference(step,[status(thm)],[t391290,t108]) ).
cnf(t391292,plain,
meet(sFlat1,join(b,meet(sFlat1,complement(meet(sFlat1,b))))) = meet(sFlat1,join(sFlat1,b)),
inference(step,[status(thm)],[t391291,t65]) ).
cnf(t391293,plain,
meet(sFlat1,join(b,meet(sFlat1,complement(meet(sFlat1,b))))) = meet(sFlat1,one),
inference(step,[status(thm)],[t391292,t242]) ).
cnf(t391294,plain,
meet(sFlat1,join(b,meet(sFlat1,complement(meet(sFlat1,b))))) = sFlat1,
inference(step,[status(thm)],[t391293,t108]) ).
cnf(t388166,plain,
meet(sFlat1,join(b,meet(sFlat1,complement(meet(sFlat1,b))))) = sFlat1,
inference(orient,[status(thm)],[t391294]) ).
cnf(t388305,plain,
one = join(join(b,meet(sFlat1,complement(meet(sFlat1,b)))),complement(sFlat1)),
inference(cp,[status(thm)],[t1323,t388166]) ).
cnf(t391295,plain,
one = join(b,join(meet(sFlat1,complement(meet(sFlat1,b))),complement(sFlat1))),
inference(step,[status(thm)],[t388305,t69]) ).
cnf(t391296,plain,
one = join(b,join(complement(sFlat1),meet(sFlat1,complement(meet(sFlat1,b))))),
inference(step,[status(thm)],[t391295,t65]) ).
cnf(t4,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t54,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t4]) ).
cnf(t92,plain,
zero = meet(a,sFlat1),
inference(cp,[status(thm)],[t54,t90]) ).
cnf(t389649,plain,
zero = meet(sFlat1,a),
inference(step,[status(thm)],[t92,t27]) ).
cnf(t117,plain,
meet(sFlat1,a) = zero,
inference(orient,[status(thm)],[t389649]) ).
cnf(t119,plain,
a = ifeq(join(sFlat1,a),one,ifeq(zero,zero,complement(sFlat1),a),a),
inference(cp,[status(thm)],[t22,t117]) ).
cnf(t91,plain,
one = join(a,sFlat1),
inference(cp,[status(thm)],[t80,t90]) ).
cnf(t389648,plain,
one = join(sFlat1,a),
inference(step,[status(thm)],[t91,t65]) ).
cnf(t113,plain,
join(sFlat1,a) = one,
inference(orient,[status(thm)],[t389648]) ).
cnf(t389650,plain,
a = ifeq(one,one,ifeq(zero,zero,complement(sFlat1),a),a),
inference(step,[status(thm)],[t119,t113]) ).
cnf(t5,axiom,
ifeq(X1,X1,X2,X3) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t21,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t5]) ).
cnf(t389651,plain,
a = ifeq(zero,zero,complement(sFlat1),a),
inference(step,[status(thm)],[t389650,t21]) ).
cnf(t389652,plain,
a = complement(sFlat1),
inference(step,[status(thm)],[t389651,t21]) ).
cnf(t121,plain,
complement(sFlat1) = a,
inference(orient,[status(thm)],[t389652]) ).
cnf(t391297,plain,
one = join(b,join(a,meet(sFlat1,complement(meet(sFlat1,b))))),
inference(step,[status(thm)],[t391296,t121]) ).
cnf(t391298,plain,
one = join(b,meet(sFlat1,complement(meet(sFlat1,b)))),
inference(step,[status(thm)],[t391297,t236]) ).
cnf(t388400,plain,
join(b,meet(sFlat1,complement(meet(sFlat1,b)))) = one,
inference(orient,[status(thm)],[t391298]) ).
cnf(t388405,plain,
meet(sFlat1,complement(meet(sFlat1,b))) = ifeq(one,one,ifeq(meet(b,meet(sFlat1,complement(meet(sFlat1,b)))),zero,complement(b),meet(sFlat1,complement(meet(sFlat1,b)))),meet(sFlat1,complement(meet(sFlat1,b)))),
inference(cp,[status(thm)],[t22,t388400]) ).
cnf(t391299,plain,
meet(sFlat1,complement(meet(sFlat1,b))) = ifeq(meet(b,meet(sFlat1,complement(meet(sFlat1,b)))),zero,complement(b),meet(sFlat1,complement(meet(sFlat1,b)))),
inference(step,[status(thm)],[t388405,t21]) ).
cnf(t56,plain,
meet(X1,meet(complement(X1),X2)) = meet(zero,X2),
inference(cp,[status(thm)],[t30,t54]) ).
cnf(t57,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t20,t54]) ).
cnf(t99,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t57]) ).
cnf(t100,plain,
X1 = join(zero,X1),
inference(cp,[status(thm)],[t99,t65]) ).
cnf(t133,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t100]) ).
cnf(t135,plain,
meet(zero,X1) = zero,
inference(cp,[status(thm)],[t133,t20]) ).
cnf(t153,plain,
meet(zero,X1) = zero,
inference(orient,[status(thm)],[t135]) ).
cnf(t389767,plain,
meet(X1,meet(complement(X1),X2)) = zero,
inference(step,[status(thm)],[t56,t153]) ).
cnf(t1050,plain,
meet(X1,meet(complement(X1),X2)) = zero,
inference(orient,[status(thm)],[t389767]) ).
cnf(t1054,plain,
meet(meet(complement(X1),X2),X1) = meet(meet(complement(X1),X2),zero),
inference(cp,[status(thm)],[t538,t1050]) ).
cnf(t389768,plain,
meet(complement(X1),meet(X2,X1)) = meet(meet(complement(X1),X2),zero),
inference(step,[status(thm)],[t1054,t30]) ).
cnf(t389769,plain,
meet(complement(X1),meet(X2,X1)) = meet(complement(X1),meet(X2,zero)),
inference(step,[status(thm)],[t389768,t30]) ).
cnf(t154,plain,
zero = meet(X1,zero),
inference(cp,[status(thm)],[t153,t27]) ).
cnf(t161,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t154]) ).
cnf(t389770,plain,
meet(complement(X1),meet(X2,X1)) = meet(complement(X1),zero),
inference(step,[status(thm)],[t389769,t161]) ).
cnf(t389771,plain,
meet(complement(X1),meet(X2,X1)) = zero,
inference(step,[status(thm)],[t389770,t161]) ).
cnf(t1065,plain,
meet(complement(X1),meet(X2,X1)) = zero,
inference(orient,[status(thm)],[t389771]) ).
cnf(t1072,plain,
zero = meet(complement(join(X1,X2)),X2),
inference(cp,[status(thm)],[t1065,t188]) ).
cnf(t389773,plain,
zero = meet(X2,complement(join(X1,X2))),
inference(step,[status(thm)],[t1072,t27]) ).
cnf(t1114,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(orient,[status(thm)],[t389773]) ).
cnf(t557,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X2,X1)),
inference(cp,[status(thm)],[t175,t538]) ).
cnf(t2689,plain,
join(meet(X1,X2),meet(X2,X1)) = meet(X1,X2),
inference(orient,[status(thm)],[t557]) ).
cnf(t2767,plain,
zero = meet(meet(X1,X2),complement(meet(X2,X1))),
inference(cp,[status(thm)],[t1114,t2689]) ).
cnf(t389952,plain,
zero = meet(X1,meet(X2,complement(meet(X2,X1)))),
inference(step,[status(thm)],[t2767,t30]) ).
cnf(t8250,plain,
meet(X1,meet(X2,complement(meet(X2,X1)))) = zero,
inference(orient,[status(thm)],[t389952]) ).
cnf(t391300,plain,
meet(sFlat1,complement(meet(sFlat1,b))) = ifeq(zero,zero,complement(b),meet(sFlat1,complement(meet(sFlat1,b)))),
inference(step,[status(thm)],[t391299,t8250]) ).
cnf(t391301,plain,
meet(sFlat1,complement(meet(sFlat1,b))) = complement(b),
inference(step,[status(thm)],[t391300,t21]) ).
cnf(t391302,plain,
meet(sFlat1,complement(meet(sFlat1,b))) = sFlat0,
inference(step,[status(thm)],[t391301,t95]) ).
cnf(t388519,plain,
meet(sFlat1,complement(meet(sFlat1,b))) = sFlat0,
inference(orient,[status(thm)],[t391302]) ).
cnf(t388527,plain,
meet(sFlat1,complement(meet(sFlat1,b))) = meet(sFlat1,sFlat0),
inference(cp,[status(thm)],[t208,t388519]) ).
cnf(t391304,plain,
sFlat0 = meet(sFlat1,sFlat0),
inference(step,[status(thm)],[t388527,t388519]) ).
cnf(t391305,plain,
sFlat0 = meet(sFlat0,sFlat1),
inference(step,[status(thm)],[t391304,t27]) ).
cnf(t388809,plain,
meet(sFlat0,sFlat1) = sFlat0,
inference(orient,[status(thm)],[t391305]) ).
cnf(t388824,plain,
meet(sFlat1,join(sFlat2,X1)) = join(sFlat0,meet(sFlat1,join(sFlat2,X1))),
inference(cp,[status(thm)],[t376308,t388809]) ).
cnf(t191,plain,
sFlat1 = meet(sFlat1,sFlat2),
inference(cp,[status(thm)],[t188,t166]) ).
cnf(t197,plain,
meet(sFlat1,sFlat2) = sFlat1,
inference(orient,[status(thm)],[t191]) ).
cnf(t199,plain,
meet(sFlat1,meet(sFlat2,X1)) = meet(sFlat1,X1),
inference(cp,[status(thm)],[t30,t197]) ).
cnf(t620,plain,
meet(sFlat1,meet(sFlat2,X1)) = meet(sFlat1,X1),
inference(orient,[status(thm)],[t199]) ).
cnf(t623,plain,
meet(sFlat1,join(sFlat2,X1)) = meet(sFlat1,sFlat2),
inference(cp,[status(thm)],[t620,t18]) ).
cnf(t389721,plain,
meet(sFlat1,join(sFlat2,X1)) = sFlat1,
inference(step,[status(thm)],[t623,t197]) ).
cnf(t635,plain,
meet(sFlat1,join(sFlat2,X1)) = sFlat1,
inference(orient,[status(thm)],[t389721]) ).
cnf(t391310,plain,
sFlat1 = join(sFlat0,meet(sFlat1,join(sFlat2,X1))),
inference(step,[status(thm)],[t388824,t635]) ).
cnf(t391311,plain,
sFlat1 = join(sFlat0,sFlat1),
inference(step,[status(thm)],[t391310,t635]) ).
cnf(t391312,plain,
sFlat1 = sFlat2,
inference(step,[status(thm)],[t391311,t166]) ).
cnf(t389076,plain,
sFlat2 = sFlat1,
inference(orient,[status(thm)],[t391312]) ).
cnf(t391313,plain,
join(sFlat0,sFlat1) = sFlat1,
inference(step,[status(thm)],[t166,t389076]) ).
cnf(t389077,plain,
join(sFlat0,sFlat1) = sFlat1,
inference(orient,[status(thm)],[t391313]) ).
cnf(goal_0,negated_conjecture,
join(complement(b),complement(a)) != complement(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
join(sFlat0,complement(a)) != complement(a),
inference(rw,[status(thm)],[goal_0,t95]) ).
cnf(g0_1,plain,
join(sFlat0,sFlat1) != complement(a),
inference(rw,[status(thm)],[g0_0,t90]) ).
cnf(g0_2,plain,
sFlat1 != complement(a),
inference(rw,[status(thm)],[g0_1,t389077]) ).
cnf(g0_3,plain,
sFlat1 != sFlat1,
inference(rw,[status(thm)],[g0_2,t90]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT223-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/5.36 % Computer : n015.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Wed Sep 23 20:39:45 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 175.78/30.75 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 175.78/30.75 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------