%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL026-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n005.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 02:34:52 PM UTC 2026
% Result : Unsatisfiable 78.76s 10.33s
% Output : CNFRefutation 78.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 132
% Number of leaves : 18
% Syntax : Number of clauses : 518 ( 518 unt; 0 nHn; 161 RR)
% Number of literals : 518 ( 517 equ; 6 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 8 con; 0-2 aty)
% Number of variables : 510 ( 66 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t6,axiom,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t66,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t6]) ).
cnf(t5,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t22,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t68,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t66,t22]) ).
cnf(t129539,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t68,t66]) ).
cnf(t85,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t129539]) ).
cnf(t14,axiom,
sFlat0 = composition(sk1,top),
introduced(definition) ).
cnf(t56,plain,
composition(sk1,top) = sFlat0,
inference(orient,[status(thm)],[t14]) ).
cnf(t15,axiom,
sFlat1 = meet(composition(sk1,top),sk2),
introduced(definition) ).
cnf(t129536,plain,
sFlat1 = meet(sFlat0,sk2),
inference(step,[status(thm)],[t15,t56]) ).
cnf(t75,plain,
meet(sFlat0,sk2) = sFlat1,
inference(orient,[status(thm)],[t129536]) ).
cnf(t16,axiom,
sFlat2 = composition(sk1,sk2),
introduced(definition) ).
cnf(t61,plain,
composition(sk1,sk2) = sFlat2,
inference(orient,[status(thm)],[t16]) ).
cnf(t11,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t30,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t7,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t49,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t7]) ).
cnf(t54,plain,
composition(join(X1,converse(X2)),converse(X3)) = join(composition(X1,converse(X3)),converse(composition(X3,X2))),
inference(cp,[status(thm)],[t30,t49]) ).
cnf(t14922,plain,
join(composition(X1,converse(X2)),converse(composition(X2,X3))) = composition(join(X1,converse(X3)),converse(X2)),
inference(orient,[status(thm)],[t54]) ).
cnf(t12,axiom,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t129535,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t12,t22]) ).
cnf(t33,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t129535]) ).
cnf(t1,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t21,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t34,plain,
complement(X1) = join(complement(X1),composition(X2,complement(composition(converse(X2),X1)))),
inference(cp,[status(thm)],[t33,t21]) ).
cnf(t2610,plain,
join(complement(X1),composition(X2,complement(composition(converse(X2),X1)))) = complement(X1),
inference(orient,[status(thm)],[t34]) ).
cnf(t3,axiom,
join(X1,complement(X1)) = top,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t27,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t3]) ).
cnf(t67,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t66,t27]) ).
cnf(t4,axiom,
meet(X1,complement(X1)) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t73,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t4]) ).
cnf(t129537,plain,
zero = complement(top),
inference(step,[status(thm)],[t67,t73]) ).
cnf(t76,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t129537]) ).
cnf(t2616,plain,
complement(top) = join(zero,composition(X1,complement(composition(converse(X1),top)))),
inference(cp,[status(thm)],[t2610,t76]) ).
cnf(t129723,plain,
zero = join(zero,composition(X1,complement(composition(converse(X1),top)))),
inference(step,[status(thm)],[t2616,t76]) ).
cnf(t10,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t24,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t51,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t49,t21]) ).
cnf(t170,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t51]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t20,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t171,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t170,t20]) ).
cnf(t129543,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t171,t21]) ).
cnf(t185,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t129543]) ).
cnf(t186,plain,
one = converse(one),
inference(cp,[status(thm)],[t185,t20]) ).
cnf(t192,plain,
converse(one) = one,
inference(orient,[status(thm)],[t186]) ).
cnf(t129544,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t185,t192]) ).
cnf(t202,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t129544]) ).
cnf(t203,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t202]) ).
cnf(t206,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t33,t203]) ).
cnf(t129547,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t206,t192]) ).
cnf(t129548,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t129547,t203]) ).
cnf(t235,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t129548]) ).
cnf(t239,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t235,t76]) ).
cnf(t129549,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t239,t76]) ).
cnf(t129550,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t129549,t76]) ).
cnf(t246,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t129550]) ).
cnf(t247,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t24,t246]) ).
cnf(t299,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t247]) ).
cnf(t13,axiom,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t17,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t13]) ).
cnf(t23,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t17]) ).
cnf(t129555,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t23,t22]) ).
cnf(t129556,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t129555,t66]) ).
cnf(t129557,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t129556,t22]) ).
cnf(t259,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t129557]) ).
cnf(t267,plain,
X1 = join(meet(X1,complement(X1)),complement(complement(X1))),
inference(cp,[status(thm)],[t259,t235]) ).
cnf(t129559,plain,
X1 = join(complement(complement(X1)),meet(X1,complement(X1))),
inference(step,[status(thm)],[t267,t22]) ).
cnf(t129560,plain,
X1 = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t129559,t73]) ).
cnf(t129561,plain,
X1 = join(zero,complement(complement(X1))),
inference(step,[status(thm)],[t129560,t22]) ).
cnf(t276,plain,
join(zero,complement(complement(X1))) = X1,
inference(orient,[status(thm)],[t129561]) ).
cnf(t301,plain,
join(zero,complement(complement(X1))) = join(zero,X1),
inference(cp,[status(thm)],[t299,t276]) ).
cnf(t129562,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t301,t276]) ).
cnf(t304,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t129562]) ).
cnf(t129724,plain,
zero = composition(X1,complement(composition(converse(X1),top))),
inference(step,[status(thm)],[t129723,t304]) ).
cnf(t2641,plain,
composition(X1,complement(composition(converse(X1),top))) = zero,
inference(orient,[status(thm)],[t129724]) ).
cnf(t2652,plain,
zero = composition(converse(X1),complement(composition(X1,top))),
inference(cp,[status(thm)],[t2641,t21]) ).
cnf(t2856,plain,
composition(converse(X1),complement(composition(X1,top))) = zero,
inference(orient,[status(thm)],[t2652]) ).
cnf(t129565,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t276,t304]) ).
cnf(t313,plain,
complement(complement(X1)) = X1,
inference(rw,[status(thm)],[t129565]) ).
cnf(t332,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t313]) ).
cnf(t335,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t235,t332]) ).
cnf(t129575,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t335,t332]) ).
cnf(t129576,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t129575,t332]) ).
cnf(t349,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t129576]) ).
cnf(t351,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t24,t349]) ).
cnf(t441,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t351]) ).
cnf(t445,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t441,t259]) ).
cnf(t129594,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t445,t259]) ).
cnf(t129595,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t129594,t22]) ).
cnf(t483,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t129595]) ).
cnf(t486,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t483,t85]) ).
cnf(t493,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t486]) ).
cnf(t497,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t24,t493]) ).
cnf(t5986,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t497]) ).
cnf(t333,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(cp,[status(thm)],[t332,t66]) ).
cnf(t851,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t333]) ).
cnf(t854,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(cp,[status(thm)],[t851,t332]) ).
cnf(t957,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(orient,[status(thm)],[t854]) ).
cnf(t963,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),X2)),
inference(cp,[status(thm)],[t332,t957]) ).
cnf(t1263,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t963]) ).
cnf(t129643,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t259,t1263]) ).
cnf(t1289,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(rw,[status(thm)],[t129643]) ).
cnf(t21395,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t1289]) ).
cnf(t21572,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(cp,[status(thm)],[t5986,t21395]) ).
cnf(t22044,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t21572]) ).
cnf(t22075,plain,
join(X1,X2) = join(X1,meet(complement(X1),X2)),
inference(cp,[status(thm)],[t22044,t85]) ).
cnf(t23355,plain,
join(X1,meet(complement(X1),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t22075]) ).
cnf(t23371,plain,
join(complement(X1),X2) = join(complement(X1),meet(X1,X2)),
inference(cp,[status(thm)],[t23355,t332]) ).
cnf(t26845,plain,
join(complement(X1),meet(X1,X2)) = join(complement(X1),X2),
inference(orient,[status(thm)],[t23371]) ).
cnf(t853,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(cp,[status(thm)],[t851,t332]) ).
cnf(t941,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t853]) ).
cnf(t948,plain,
meet(complement(X1),X2) = complement(join(X1,complement(X2))),
inference(cp,[status(thm)],[t332,t941]) ).
cnf(t973,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t948]) ).
cnf(t992,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(cp,[status(thm)],[t973,t332]) ).
cnf(t1290,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t992]) ).
cnf(t22061,plain,
join(X1,complement(X2)) = join(X1,complement(join(X2,X1))),
inference(cp,[status(thm)],[t22044,t1290]) ).
cnf(t24206,plain,
join(X1,complement(join(X2,X1))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t22061]) ).
cnf(t24453,plain,
meet(X1,complement(complement(join(X2,complement(X1))))) = complement(join(complement(X1),complement(X2))),
inference(cp,[status(thm)],[t1263,t24206]) ).
cnf(t130151,plain,
meet(X1,join(X2,complement(X1))) = complement(join(complement(X1),complement(X2))),
inference(step,[status(thm)],[t24453,t332]) ).
cnf(t130152,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(step,[status(thm)],[t130151,t66]) ).
cnf(t24570,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t130152]) ).
cnf(t24645,plain,
meet(X1,X2) = meet(X1,join(complement(X1),X2)),
inference(cp,[status(thm)],[t24570,t22]) ).
cnf(t24669,plain,
meet(X1,join(complement(X1),X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t24645]) ).
cnf(t8,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t37,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t39,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t37,t21]) ).
cnf(t139,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t39]) ).
cnf(t140,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t139,t27]) ).
cnf(t444,plain,
join(X1,complement(X1)) = join(X1,top),
inference(cp,[status(thm)],[t441,t27]) ).
cnf(t129586,plain,
top = join(X1,top),
inference(step,[status(thm)],[t444,t27]) ).
cnf(t451,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t129586]) ).
cnf(t455,plain,
join(X1,converse(top)) = converse(top),
inference(cp,[status(thm)],[t139,t451]) ).
cnf(t470,plain,
join(X1,converse(top)) = converse(top),
inference(orient,[status(thm)],[t455]) ).
cnf(t452,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t451,t22]) ).
cnf(t457,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t452]) ).
cnf(t471,plain,
converse(top) = top,
inference(cp,[status(thm)],[t470,t457]) ).
cnf(t475,plain,
converse(top) = top,
inference(orient,[status(thm)],[t471]) ).
cnf(t129644,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(step,[status(thm)],[t140,t475]) ).
cnf(t1304,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(orient,[status(thm)],[t129644]) ).
cnf(t24716,plain,
meet(X1,converse(complement(converse(complement(X1))))) = meet(X1,top),
inference(cp,[status(thm)],[t24669,t1304]) ).
cnf(t79,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t66,t76]) ).
cnf(t103,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t79]) ).
cnf(t280,plain,
meet(top,complement(X1)) = complement(X1),
inference(cp,[status(thm)],[t103,t276]) ).
cnf(t281,plain,
meet(top,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t280]) ).
cnf(t334,plain,
complement(complement(X1)) = meet(top,X1),
inference(cp,[status(thm)],[t281,t332]) ).
cnf(t129574,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t334,t332]) ).
cnf(t347,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t129574]) ).
cnf(t348,plain,
X1 = meet(X1,top),
inference(cp,[status(thm)],[t347,t85]) ).
cnf(t352,plain,
meet(X1,top) = X1,
inference(orient,[status(thm)],[t348]) ).
cnf(t130154,plain,
meet(X1,converse(complement(converse(complement(X1))))) = X1,
inference(step,[status(thm)],[t24716,t352]) ).
cnf(t24767,plain,
meet(X1,converse(complement(converse(complement(X1))))) = X1,
inference(orient,[status(thm)],[t130154]) ).
cnf(t24829,plain,
join(X1,complement(converse(complement(converse(complement(complement(X1))))))) = complement(complement(X1)),
inference(cp,[status(thm)],[t941,t24767]) ).
cnf(t130155,plain,
join(X1,complement(converse(complement(converse(X1))))) = complement(complement(X1)),
inference(step,[status(thm)],[t24829,t332]) ).
cnf(t130156,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(step,[status(thm)],[t130155,t332]) ).
cnf(t24838,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(orient,[status(thm)],[t130156]) ).
cnf(t24947,plain,
join(X1,converse(complement(converse(complement(converse(converse(X1))))))) = converse(converse(X1)),
inference(cp,[status(thm)],[t139,t24838]) ).
cnf(t130170,plain,
join(X1,converse(complement(converse(complement(X1))))) = converse(converse(X1)),
inference(step,[status(thm)],[t24947,t21]) ).
cnf(t130171,plain,
join(X1,converse(complement(converse(complement(X1))))) = X1,
inference(step,[status(thm)],[t130170,t21]) ).
cnf(t25191,plain,
join(X1,converse(complement(converse(complement(X1))))) = X1,
inference(orient,[status(thm)],[t130171]) ).
cnf(t25255,plain,
meet(X1,converse(complement(converse(complement(complement(X1)))))) = meet(X1,complement(X1)),
inference(cp,[status(thm)],[t24669,t25191]) ).
cnf(t130172,plain,
meet(X1,converse(complement(converse(X1)))) = meet(X1,complement(X1)),
inference(step,[status(thm)],[t25255,t332]) ).
cnf(t130173,plain,
meet(X1,converse(complement(converse(X1)))) = zero,
inference(step,[status(thm)],[t130172,t73]) ).
cnf(t25300,plain,
meet(X1,converse(complement(converse(X1)))) = zero,
inference(orient,[status(thm)],[t130173]) ).
cnf(t25311,plain,
zero = meet(converse(X1),converse(complement(X1))),
inference(cp,[status(thm)],[t25300,t21]) ).
cnf(t25332,plain,
meet(converse(X1),converse(complement(X1))) = zero,
inference(orient,[status(thm)],[t25311]) ).
cnf(t26921,plain,
join(complement(converse(X1)),converse(complement(X1))) = join(complement(converse(X1)),zero),
inference(cp,[status(thm)],[t26845,t25332]) ).
cnf(t130311,plain,
join(converse(complement(X1)),complement(converse(X1))) = join(complement(converse(X1)),zero),
inference(step,[status(thm)],[t26921,t22]) ).
cnf(t306,plain,
X1 = join(X1,zero),
inference(cp,[status(thm)],[t304,t22]) ).
cnf(t325,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t306]) ).
cnf(t130312,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(step,[status(thm)],[t130311,t325]) ).
cnf(t32091,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(orient,[status(thm)],[t130312]) ).
cnf(t32096,plain,
complement(converse(complement(X1))) = join(converse(X1),complement(converse(complement(X1)))),
inference(cp,[status(thm)],[t32091,t332]) ).
cnf(t24849,plain,
converse(X1) = join(converse(X1),complement(converse(complement(X1)))),
inference(cp,[status(thm)],[t24838,t21]) ).
cnf(t28688,plain,
join(converse(X1),complement(converse(complement(X1)))) = converse(X1),
inference(orient,[status(thm)],[t24849]) ).
cnf(t130313,plain,
complement(converse(complement(X1))) = converse(X1),
inference(step,[status(thm)],[t32096,t28688]) ).
cnf(t32131,plain,
complement(converse(complement(X1))) = converse(X1),
inference(orient,[status(thm)],[t130313]) ).
cnf(t32136,plain,
converse(complement(X1)) = complement(converse(X1)),
inference(cp,[status(thm)],[t32131,t332]) ).
cnf(t32189,plain,
complement(converse(X1)) = converse(complement(X1)),
inference(orient,[status(thm)],[t32136]) ).
cnf(t479,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(cp,[status(thm)],[t49,t475]) ).
cnf(t520,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(orient,[status(thm)],[t479]) ).
cnf(t32194,plain,
converse(complement(composition(top,X1))) = complement(composition(converse(X1),top)),
inference(cp,[status(thm)],[t32189,t520]) ).
cnf(t32407,plain,
complement(composition(converse(X1),top)) = converse(complement(composition(top,X1))),
inference(orient,[status(thm)],[t32194]) ).
cnf(t32447,plain,
zero = composition(converse(converse(X1)),converse(complement(composition(top,X1)))),
inference(cp,[status(thm)],[t2856,t32407]) ).
cnf(t130373,plain,
zero = converse(composition(complement(composition(top,X1)),converse(X1))),
inference(step,[status(thm)],[t32447,t49]) ).
cnf(t50,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t49,t21]) ).
cnf(t158,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t50]) ).
cnf(t130374,plain,
zero = composition(X1,converse(complement(composition(top,X1)))),
inference(step,[status(thm)],[t130373,t158]) ).
cnf(t32953,plain,
composition(X1,converse(complement(composition(top,X1)))) = zero,
inference(orient,[status(thm)],[t130374]) ).
cnf(t478,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(cp,[status(thm)],[t49,t475]) ).
cnf(t502,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(orient,[status(thm)],[t478]) ).
cnf(t9,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t44,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t504,plain,
composition(top,converse(composition(X1,X2))) = converse(composition(X1,composition(X2,top))),
inference(cp,[status(thm)],[t502,t44]) ).
cnf(t65293,plain,
converse(composition(X1,composition(X2,top))) = composition(top,converse(composition(X1,X2))),
inference(orient,[status(thm)],[t504]) ).
cnf(t57,plain,
composition(sk1,composition(top,X1)) = composition(sFlat0,X1),
inference(cp,[status(thm)],[t44,t56]) ).
cnf(t95,plain,
composition(sk1,composition(top,X1)) = composition(sFlat0,X1),
inference(orient,[status(thm)],[t57]) ).
cnf(t96,plain,
composition(join(sk1,X1),composition(top,X2)) = join(composition(sFlat0,X2),composition(X1,composition(top,X2))),
inference(cp,[status(thm)],[t30,t95]) ).
cnf(t47,plain,
composition(join(X1,composition(X2,X3)),Y3) = join(composition(X1,Y3),composition(X2,composition(X3,Y3))),
inference(cp,[status(thm)],[t30,t44]) ).
cnf(t5845,plain,
join(composition(X1,X2),composition(X3,composition(Y3,X2))) = composition(join(X1,composition(X3,Y3)),X2),
inference(orient,[status(thm)],[t47]) ).
cnf(t130124,plain,
composition(join(sk1,X1),composition(top,X2)) = composition(join(sFlat0,composition(X1,top)),X2),
inference(step,[status(thm)],[t96,t5845]) ).
cnf(t22585,plain,
composition(join(sFlat0,composition(X1,top)),X2) = composition(join(sk1,X1),composition(top,X2)),
inference(orient,[status(thm)],[t130124]) ).
cnf(t2645,plain,
zero = composition(top,complement(composition(top,top))),
inference(cp,[status(thm)],[t2641,t475]) ).
cnf(t2684,plain,
composition(top,complement(composition(top,top))) = zero,
inference(orient,[status(thm)],[t2645]) ).
cnf(t2688,plain,
composition(join(top,X1),complement(composition(top,top))) = join(zero,composition(X1,complement(composition(top,top)))),
inference(cp,[status(thm)],[t30,t2684]) ).
cnf(t129729,plain,
composition(top,complement(composition(top,top))) = join(zero,composition(X1,complement(composition(top,top)))),
inference(step,[status(thm)],[t2688,t457]) ).
cnf(t129730,plain,
zero = join(zero,composition(X1,complement(composition(top,top)))),
inference(step,[status(thm)],[t129729,t2684]) ).
cnf(t129731,plain,
zero = composition(X1,complement(composition(top,top))),
inference(step,[status(thm)],[t129730,t304]) ).
cnf(t2695,plain,
composition(X1,complement(composition(top,top))) = zero,
inference(orient,[status(thm)],[t129731]) ).
cnf(t2696,plain,
zero = complement(composition(top,top)),
inference(cp,[status(thm)],[t2695,t203]) ).
cnf(t2719,plain,
complement(composition(top,top)) = zero,
inference(orient,[status(thm)],[t2696]) ).
cnf(t2724,plain,
composition(top,top) = complement(zero),
inference(cp,[status(thm)],[t332,t2719]) ).
cnf(t305,plain,
complement(zero) = top,
inference(cp,[status(thm)],[t304,t27]) ).
cnf(t315,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t305]) ).
cnf(t129745,plain,
composition(top,top) = top,
inference(step,[status(thm)],[t2724,t315]) ).
cnf(t2734,plain,
composition(top,top) = top,
inference(orient,[status(thm)],[t129745]) ).
cnf(t2737,plain,
composition(sFlat0,top) = composition(sk1,top),
inference(cp,[status(thm)],[t95,t2734]) ).
cnf(t129748,plain,
composition(sFlat0,top) = sFlat0,
inference(step,[status(thm)],[t2737,t56]) ).
cnf(t2739,plain,
composition(sFlat0,top) = sFlat0,
inference(orient,[status(thm)],[t129748]) ).
cnf(t2742,plain,
composition(join(sFlat0,X1),top) = join(sFlat0,composition(X1,top)),
inference(cp,[status(thm)],[t30,t2739]) ).
cnf(t2778,plain,
composition(join(sFlat0,X1),top) = join(sFlat0,composition(X1,top)),
inference(orient,[status(thm)],[t2742]) ).
cnf(t485,plain,
sFlat0 = join(sFlat0,sFlat1),
inference(cp,[status(thm)],[t483,t75]) ).
cnf(t491,plain,
join(sFlat0,sFlat1) = sFlat0,
inference(orient,[status(thm)],[t485]) ).
cnf(t2788,plain,
join(sFlat0,composition(sFlat1,top)) = composition(sFlat0,top),
inference(cp,[status(thm)],[t2778,t491]) ).
cnf(t129752,plain,
join(sFlat0,composition(sFlat1,top)) = sFlat0,
inference(step,[status(thm)],[t2788,t2739]) ).
cnf(t2813,plain,
join(sFlat0,composition(sFlat1,top)) = sFlat0,
inference(orient,[status(thm)],[t129752]) ).
cnf(t22596,plain,
composition(join(sk1,sFlat1),composition(top,X1)) = composition(sFlat0,X1),
inference(cp,[status(thm)],[t22585,t2813]) ).
cnf(t130272,plain,
composition(join(sFlat1,sk1),composition(top,X1)) = composition(sFlat0,X1),
inference(step,[status(thm)],[t22596,t22]) ).
cnf(t31017,plain,
composition(join(sFlat1,sk1),composition(top,X1)) = composition(sFlat0,X1),
inference(orient,[status(thm)],[t130272]) ).
cnf(t65294,plain,
composition(top,converse(composition(join(sFlat1,sk1),top))) = converse(composition(sFlat0,top)),
inference(cp,[status(thm)],[t65293,t31017]) ).
cnf(t130971,plain,
composition(top,composition(top,converse(join(sFlat1,sk1)))) = converse(composition(sFlat0,top)),
inference(step,[status(thm)],[t65294,t502]) ).
cnf(t2738,plain,
composition(top,composition(top,X1)) = composition(top,X1),
inference(cp,[status(thm)],[t44,t2734]) ).
cnf(t2763,plain,
composition(top,composition(top,X1)) = composition(top,X1),
inference(orient,[status(thm)],[t2738]) ).
cnf(t130972,plain,
composition(top,converse(join(sFlat1,sk1))) = converse(composition(sFlat0,top)),
inference(step,[status(thm)],[t130971,t2763]) ).
cnf(t130973,plain,
composition(top,converse(join(sFlat1,sk1))) = composition(top,converse(sFlat0)),
inference(step,[status(thm)],[t130972,t502]) ).
cnf(t2740,plain,
composition(top,converse(sFlat0)) = converse(sFlat0),
inference(cp,[status(thm)],[t502,t2739]) ).
cnf(t2746,plain,
composition(top,converse(sFlat0)) = converse(sFlat0),
inference(orient,[status(thm)],[t2740]) ).
cnf(t130974,plain,
composition(top,converse(join(sFlat1,sk1))) = converse(sFlat0),
inference(step,[status(thm)],[t130973,t2746]) ).
cnf(t65367,plain,
composition(top,converse(join(sFlat1,sk1))) = converse(sFlat0),
inference(orient,[status(thm)],[t130974]) ).
cnf(t65384,plain,
zero = composition(converse(join(sFlat1,sk1)),converse(complement(converse(sFlat0)))),
inference(cp,[status(thm)],[t32953,t65367]) ).
cnf(t130982,plain,
zero = converse(composition(complement(converse(sFlat0)),join(sFlat1,sk1))),
inference(step,[status(thm)],[t65384,t49]) ).
cnf(t130983,plain,
zero = converse(composition(converse(complement(sFlat0)),join(sFlat1,sk1))),
inference(step,[status(thm)],[t130982,t32189]) ).
cnf(t130984,plain,
zero = composition(converse(join(sFlat1,sk1)),complement(sFlat0)),
inference(step,[status(thm)],[t130983,t170]) ).
cnf(t65434,plain,
composition(converse(join(sFlat1,sk1)),complement(sFlat0)) = zero,
inference(orient,[status(thm)],[t130984]) ).
cnf(t2868,plain,
zero = composition(converse(sk1),complement(sFlat0)),
inference(cp,[status(thm)],[t2856,t56]) ).
cnf(t2876,plain,
composition(converse(sk1),complement(sFlat0)) = zero,
inference(orient,[status(thm)],[t2868]) ).
cnf(t2882,plain,
composition(converse(complement(sFlat0)),sk1) = converse(zero),
inference(cp,[status(thm)],[t170,t2876]) ).
cnf(t40,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t37,t21]) ).
cnf(t148,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t40]) ).
cnf(t310,plain,
join(converse(zero),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t148,t304]) ).
cnf(t129578,plain,
join(converse(zero),X1) = X1,
inference(step,[status(thm)],[t310,t21]) ).
cnf(t356,plain,
join(converse(zero),X1) = X1,
inference(orient,[status(thm)],[t129578]) ).
cnf(t358,plain,
zero = converse(zero),
inference(cp,[status(thm)],[t356,t325]) ).
cnf(t361,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t358]) ).
cnf(t129758,plain,
composition(converse(complement(sFlat0)),sk1) = zero,
inference(step,[status(thm)],[t2882,t361]) ).
cnf(t2883,plain,
composition(converse(complement(sFlat0)),sk1) = zero,
inference(orient,[status(thm)],[t129758]) ).
cnf(t2885,plain,
composition(join(converse(complement(sFlat0)),X1),sk1) = join(zero,composition(X1,sk1)),
inference(cp,[status(thm)],[t30,t2883]) ).
cnf(t129902,plain,
composition(join(converse(complement(sFlat0)),X1),sk1) = composition(X1,sk1),
inference(step,[status(thm)],[t2885,t304]) ).
cnf(t8825,plain,
composition(join(converse(complement(sFlat0)),X1),sk1) = composition(X1,sk1),
inference(orient,[status(thm)],[t129902]) ).
cnf(t24953,plain,
composition(complement(converse(complement(converse(converse(complement(sFlat0)))))),sk1) = composition(converse(complement(sFlat0)),sk1),
inference(cp,[status(thm)],[t8825,t24838]) ).
cnf(t130163,plain,
composition(complement(converse(complement(complement(sFlat0)))),sk1) = composition(converse(complement(sFlat0)),sk1),
inference(step,[status(thm)],[t24953,t21]) ).
cnf(t130164,plain,
composition(complement(converse(sFlat0)),sk1) = composition(converse(complement(sFlat0)),sk1),
inference(step,[status(thm)],[t130163,t332]) ).
cnf(t130165,plain,
composition(complement(converse(sFlat0)),sk1) = zero,
inference(step,[status(thm)],[t130164,t2883]) ).
cnf(t24991,plain,
composition(complement(converse(sFlat0)),sk1) = zero,
inference(orient,[status(thm)],[t130165]) ).
cnf(t24993,plain,
composition(join(complement(converse(sFlat0)),X1),sk1) = join(zero,composition(X1,sk1)),
inference(cp,[status(thm)],[t30,t24991]) ).
cnf(t130298,plain,
composition(join(complement(converse(sFlat0)),X1),sk1) = composition(X1,sk1),
inference(step,[status(thm)],[t24993,t304]) ).
cnf(t31797,plain,
composition(join(complement(converse(sFlat0)),X1),sk1) = composition(X1,sk1),
inference(orient,[status(thm)],[t130298]) ).
cnf(t31800,plain,
composition(meet(converse(sFlat0),X1),sk1) = composition(join(complement(converse(sFlat0)),X1),sk1),
inference(cp,[status(thm)],[t31797,t26845]) ).
cnf(t130300,plain,
composition(meet(converse(sFlat0),X1),sk1) = composition(X1,sk1),
inference(step,[status(thm)],[t31800,t31797]) ).
cnf(t31870,plain,
composition(meet(converse(sFlat0),X1),sk1) = composition(X1,sk1),
inference(orient,[status(thm)],[t130300]) ).
cnf(t32199,plain,
converse(complement(join(converse(X1),X2))) = complement(join(X1,converse(X2))),
inference(cp,[status(thm)],[t32189,t139]) ).
cnf(t33215,plain,
converse(complement(join(converse(X1),X2))) = complement(join(X1,converse(X2))),
inference(orient,[status(thm)],[t32199]) ).
cnf(t32210,plain,
complement(meet(converse(X1),X2)) = join(converse(complement(X1)),complement(X2)),
inference(cp,[status(thm)],[t851,t32189]) ).
cnf(t33462,plain,
join(converse(complement(X1)),complement(X2)) = complement(meet(converse(X1),X2)),
inference(orient,[status(thm)],[t32210]) ).
cnf(t33506,plain,
complement(join(complement(X1),converse(complement(X2)))) = converse(complement(complement(meet(converse(X1),X2)))),
inference(cp,[status(thm)],[t33215,t33462]) ).
cnf(t130380,plain,
meet(X1,complement(converse(complement(X2)))) = converse(complement(complement(meet(converse(X1),X2)))),
inference(step,[status(thm)],[t33506,t1263]) ).
cnf(t130381,plain,
meet(X1,converse(X2)) = converse(complement(complement(meet(converse(X1),X2)))),
inference(step,[status(thm)],[t130380,t32131]) ).
cnf(t130382,plain,
meet(X1,converse(X2)) = converse(meet(converse(X1),X2)),
inference(step,[status(thm)],[t130381,t332]) ).
cnf(t33521,plain,
converse(meet(converse(X1),X2)) = meet(X1,converse(X2)),
inference(orient,[status(thm)],[t130382]) ).
cnf(t33549,plain,
meet(converse(X1),converse(X2)) = converse(meet(X1,X2)),
inference(cp,[status(thm)],[t33521,t21]) ).
cnf(t33696,plain,
meet(converse(X1),converse(X2)) = converse(meet(X1,X2)),
inference(orient,[status(thm)],[t33549]) ).
cnf(t33753,plain,
composition(converse(X1),sk1) = composition(converse(meet(sFlat0,X1)),sk1),
inference(cp,[status(thm)],[t31870,t33696]) ).
cnf(t33856,plain,
composition(converse(meet(sFlat0,X1)),sk1) = composition(converse(X1),sk1),
inference(orient,[status(thm)],[t33753]) ).
cnf(t24454,plain,
meet(complement(X1),join(X2,X1)) = complement(join(X1,complement(X2))),
inference(cp,[status(thm)],[t973,t24206]) ).
cnf(t130214,plain,
meet(complement(X1),join(X2,X1)) = meet(complement(X1),X2),
inference(step,[status(thm)],[t24454,t973]) ).
cnf(t27437,plain,
meet(complement(X1),join(X2,X1)) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t130214]) ).
cnf(t23364,plain,
join(X1,complement(X2)) = join(X1,complement(join(X1,X2))),
inference(cp,[status(thm)],[t23355,t1290]) ).
cnf(t26329,plain,
join(X1,complement(join(X1,X2))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t23364]) ).
cnf(t204,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(cp,[status(thm)],[t30,t203]) ).
cnf(t68269,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t204]) ).
cnf(t68372,plain,
join(X1,composition(complement(one),X1)) = composition(top,X1),
inference(cp,[status(thm)],[t68269,t27]) ).
cnf(t76884,plain,
join(X1,composition(complement(one),X1)) = composition(top,X1),
inference(orient,[status(thm)],[t68372]) ).
cnf(t77110,plain,
join(X1,converse(composition(complement(one),converse(X1)))) = converse(composition(top,converse(X1))),
inference(cp,[status(thm)],[t139,t76884]) ).
cnf(t25,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t24,t22]) ).
cnf(t561,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t25]) ).
cnf(t574,plain,
join(complement(X1),join(X2,X1)) = join(X2,top),
inference(cp,[status(thm)],[t561,t27]) ).
cnf(t129604,plain,
join(X1,join(complement(X1),X2)) = join(X2,top),
inference(step,[status(thm)],[t574,t561]) ).
cnf(t129605,plain,
join(X1,join(complement(X1),X2)) = top,
inference(step,[status(thm)],[t129604,t451]) ).
cnf(t683,plain,
join(X1,join(complement(X1),X2)) = top,
inference(orient,[status(thm)],[t129605]) ).
cnf(t695,plain,
X1 = join(meet(X1,join(complement(complement(X1)),X2)),complement(top)),
inference(cp,[status(thm)],[t259,t683]) ).
cnf(t129606,plain,
X1 = join(complement(top),meet(X1,join(complement(complement(X1)),X2))),
inference(step,[status(thm)],[t695,t22]) ).
cnf(t129607,plain,
X1 = join(zero,meet(X1,join(complement(complement(X1)),X2))),
inference(step,[status(thm)],[t129606,t76]) ).
cnf(t129608,plain,
X1 = meet(X1,join(complement(complement(X1)),X2)),
inference(step,[status(thm)],[t129607,t304]) ).
cnf(t129609,plain,
X1 = meet(X1,join(X1,X2)),
inference(step,[status(thm)],[t129608,t332]) ).
cnf(t708,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t129609]) ).
cnf(t719,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t708,t22]) ).
cnf(t746,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t719]) ).
cnf(t687,plain,
top = join(X1,join(X2,complement(X1))),
inference(cp,[status(thm)],[t683,t22]) ).
cnf(t810,plain,
join(X1,join(X2,complement(X1))) = top,
inference(orient,[status(thm)],[t687]) ).
cnf(t863,plain,
top = join(X1,complement(meet(X2,X1))),
inference(cp,[status(thm)],[t810,t851]) ).
cnf(t894,plain,
join(X1,complement(meet(X2,X1))) = top,
inference(orient,[status(thm)],[t863]) ).
cnf(t975,plain,
meet(complement(X1),meet(X2,X1)) = complement(top),
inference(cp,[status(thm)],[t973,t894]) ).
cnf(t129628,plain,
meet(complement(X1),meet(X2,X1)) = zero,
inference(step,[status(thm)],[t975,t76]) ).
cnf(t1015,plain,
meet(complement(X1),meet(X2,X1)) = zero,
inference(orient,[status(thm)],[t129628]) ).
cnf(t1025,plain,
zero = meet(complement(join(X1,X2)),X2),
inference(cp,[status(thm)],[t1015,t746]) ).
cnf(t129638,plain,
zero = meet(X2,complement(join(X1,X2))),
inference(step,[status(thm)],[t1025,t85]) ).
cnf(t1202,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(orient,[status(thm)],[t129638]) ).
cnf(t35,plain,
complement(one) = join(complement(one),composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t33,t20]) ).
cnf(t3094,plain,
join(complement(one),composition(converse(X1),complement(X1))) = complement(one),
inference(orient,[status(thm)],[t35]) ).
cnf(t3112,plain,
zero = meet(composition(converse(X1),complement(X1)),complement(complement(one))),
inference(cp,[status(thm)],[t1202,t3094]) ).
cnf(t129803,plain,
zero = meet(complement(complement(one)),composition(converse(X1),complement(X1))),
inference(step,[status(thm)],[t3112,t85]) ).
cnf(t129804,plain,
zero = meet(one,composition(converse(X1),complement(X1))),
inference(step,[status(thm)],[t129803,t332]) ).
cnf(t3223,plain,
meet(one,composition(converse(X1),complement(X1))) = zero,
inference(orient,[status(thm)],[t129804]) ).
cnf(t3236,plain,
zero = meet(one,composition(converse(complement(X1)),X1)),
inference(cp,[status(thm)],[t3223,t332]) ).
cnf(t3246,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(orient,[status(thm)],[t3236]) ).
cnf(t3248,plain,
zero = meet(one,converse(complement(one))),
inference(cp,[status(thm)],[t3246,t20]) ).
cnf(t3253,plain,
meet(one,converse(complement(one))) = zero,
inference(orient,[status(thm)],[t3248]) ).
cnf(t21490,plain,
one = join(zero,meet(one,complement(converse(complement(one))))),
inference(cp,[status(thm)],[t21395,t3253]) ).
cnf(t130085,plain,
one = meet(one,complement(converse(complement(one)))),
inference(step,[status(thm)],[t21490,t304]) ).
cnf(t21585,plain,
meet(one,complement(converse(complement(one)))) = one,
inference(orient,[status(thm)],[t130085]) ).
cnf(t21603,plain,
join(complement(one),converse(complement(one))) = complement(one),
inference(cp,[status(thm)],[t957,t21585]) ).
cnf(t21752,plain,
join(complement(one),converse(complement(one))) = complement(one),
inference(orient,[status(thm)],[t21603]) ).
cnf(t21760,plain,
converse(complement(one)) = meet(converse(complement(one)),complement(one)),
inference(cp,[status(thm)],[t746,t21752]) ).
cnf(t130134,plain,
converse(complement(one)) = meet(complement(one),converse(complement(one))),
inference(step,[status(thm)],[t21760,t85]) ).
cnf(t762,plain,
converse(X1) = meet(converse(X1),converse(join(X2,X1))),
inference(cp,[status(thm)],[t746,t37]) ).
cnf(t4395,plain,
meet(converse(X1),converse(join(X2,X1))) = converse(X1),
inference(orient,[status(thm)],[t762]) ).
cnf(t21764,plain,
converse(converse(complement(one))) = meet(converse(converse(complement(one))),converse(complement(one))),
inference(cp,[status(thm)],[t4395,t21752]) ).
cnf(t130090,plain,
complement(one) = meet(converse(converse(complement(one))),converse(complement(one))),
inference(step,[status(thm)],[t21764,t21]) ).
cnf(t130091,plain,
complement(one) = meet(converse(complement(one)),converse(converse(complement(one)))),
inference(step,[status(thm)],[t130090,t85]) ).
cnf(t130092,plain,
complement(one) = meet(converse(complement(one)),complement(one)),
inference(step,[status(thm)],[t130091,t21]) ).
cnf(t130093,plain,
complement(one) = meet(complement(one),converse(complement(one))),
inference(step,[status(thm)],[t130092,t85]) ).
cnf(t21773,plain,
meet(complement(one),converse(complement(one))) = complement(one),
inference(orient,[status(thm)],[t130093]) ).
cnf(t130135,plain,
converse(complement(one)) = complement(one),
inference(step,[status(thm)],[t130134,t21773]) ).
cnf(t22918,plain,
converse(complement(one)) = complement(one),
inference(orient,[status(thm)],[t130135]) ).
cnf(t22920,plain,
converse(composition(complement(one),X1)) = composition(converse(X1),complement(one)),
inference(cp,[status(thm)],[t49,t22918]) ).
cnf(t22988,plain,
converse(composition(complement(one),X1)) = composition(converse(X1),complement(one)),
inference(orient,[status(thm)],[t22920]) ).
cnf(t131261,plain,
join(X1,composition(converse(converse(X1)),complement(one))) = converse(composition(top,converse(X1))),
inference(step,[status(thm)],[t77110,t22988]) ).
cnf(t131262,plain,
join(X1,composition(X1,complement(one))) = converse(composition(top,converse(X1))),
inference(step,[status(thm)],[t131261,t21]) ).
cnf(t131263,plain,
join(X1,composition(X1,complement(one))) = composition(converse(converse(X1)),top),
inference(step,[status(thm)],[t131262,t520]) ).
cnf(t131264,plain,
join(X1,composition(X1,complement(one))) = composition(X1,top),
inference(step,[status(thm)],[t131263,t21]) ).
cnf(t77396,plain,
join(X1,composition(X1,complement(one))) = composition(X1,top),
inference(orient,[status(thm)],[t131264]) ).
cnf(t195,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(cp,[status(thm)],[t37,t192]) ).
cnf(t207,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t195]) ).
cnf(t196,plain,
converse(join(X1,one)) = join(converse(X1),one),
inference(cp,[status(thm)],[t37,t192]) ).
cnf(t129545,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(step,[status(thm)],[t196,t22]) ).
cnf(t217,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t129545]) ).
cnf(t2,axiom,
join(sk1,one) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t42,plain,
join(sk1,one) = one,
inference(orient,[status(thm)],[t2]) ).
cnf(t219,plain,
join(one,converse(sk1)) = converse(one),
inference(cp,[status(thm)],[t217,t42]) ).
cnf(t129546,plain,
join(one,converse(sk1)) = one,
inference(step,[status(thm)],[t219,t192]) ).
cnf(t231,plain,
join(one,converse(sk1)) = one,
inference(orient,[status(thm)],[t129546]) ).
cnf(t233,plain,
join(one,join(converse(sk1),X1)) = join(one,X1),
inference(cp,[status(thm)],[t24,t231]) ).
cnf(t1648,plain,
join(one,join(converse(sk1),X1)) = join(one,X1),
inference(orient,[status(thm)],[t233]) ).
cnf(t489,plain,
join(X1,converse(meet(converse(X1),X2))) = converse(converse(X1)),
inference(cp,[status(thm)],[t139,t483]) ).
cnf(t129669,plain,
join(X1,converse(meet(converse(X1),X2))) = X1,
inference(step,[status(thm)],[t489,t21]) ).
cnf(t1725,plain,
join(X1,converse(meet(converse(X1),X2))) = X1,
inference(orient,[status(thm)],[t129669]) ).
cnf(t1744,plain,
join(one,converse(meet(converse(converse(sk1)),X1))) = join(one,converse(sk1)),
inference(cp,[status(thm)],[t1648,t1725]) ).
cnf(t129670,plain,
join(one,converse(meet(sk1,X1))) = join(one,converse(sk1)),
inference(step,[status(thm)],[t1744,t21]) ).
cnf(t129671,plain,
join(one,converse(meet(sk1,X1))) = one,
inference(step,[status(thm)],[t129670,t231]) ).
cnf(t1750,plain,
join(one,converse(meet(sk1,X1))) = one,
inference(orient,[status(thm)],[t129671]) ).
cnf(t1754,plain,
join(one,converse(converse(meet(sk1,X1)))) = converse(one),
inference(cp,[status(thm)],[t207,t1750]) ).
cnf(t129672,plain,
join(one,meet(sk1,X1)) = converse(one),
inference(step,[status(thm)],[t1754,t21]) ).
cnf(t129673,plain,
join(one,meet(sk1,X1)) = one,
inference(step,[status(thm)],[t129672,t192]) ).
cnf(t1761,plain,
join(one,meet(sk1,X1)) = one,
inference(orient,[status(thm)],[t129673]) ).
cnf(t748,plain,
meet(X1,X2) = meet(meet(X1,X2),X2),
inference(cp,[status(thm)],[t746,t493]) ).
cnf(t129614,plain,
meet(X1,X2) = meet(X2,meet(X1,X2)),
inference(step,[status(thm)],[t748,t85]) ).
cnf(t784,plain,
meet(X1,meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t129614]) ).
cnf(t1766,plain,
one = join(one,meet(X1,sk1)),
inference(cp,[status(thm)],[t1761,t784]) ).
cnf(t1777,plain,
join(one,meet(X1,sk1)) = one,
inference(orient,[status(thm)],[t1766]) ).
cnf(t1782,plain,
join(one,join(meet(X1,sk1),X2)) = join(one,X2),
inference(cp,[status(thm)],[t24,t1777]) ).
cnf(t7613,plain,
join(one,join(meet(X1,sk1),X2)) = join(one,X2),
inference(orient,[status(thm)],[t1782]) ).
cnf(t21565,plain,
join(one,meet(X1,complement(sk1))) = join(one,X1),
inference(cp,[status(thm)],[t7613,t21395]) ).
cnf(t21968,plain,
join(one,meet(X1,complement(sk1))) = join(one,X1),
inference(orient,[status(thm)],[t21565]) ).
cnf(t21972,plain,
join(one,X1) = join(one,meet(complement(sk1),X1)),
inference(cp,[status(thm)],[t21968,t85]) ).
cnf(t23280,plain,
join(one,meet(complement(sk1),X1)) = join(one,X1),
inference(orient,[status(thm)],[t21972]) ).
cnf(t23282,plain,
join(one,complement(X1)) = join(one,complement(join(sk1,X1))),
inference(cp,[status(thm)],[t23280,t1290]) ).
cnf(t26184,plain,
join(one,complement(join(sk1,X1))) = join(one,complement(X1)),
inference(orient,[status(thm)],[t23282]) ).
cnf(t26230,plain,
meet(complement(one),join(sk1,X1)) = complement(join(one,complement(X1))),
inference(cp,[status(thm)],[t973,t26184]) ).
cnf(t130219,plain,
meet(complement(one),join(sk1,X1)) = meet(complement(one),X1),
inference(step,[status(thm)],[t26230,t973]) ).
cnf(t28274,plain,
meet(complement(one),join(sk1,X1)) = meet(complement(one),X1),
inference(orient,[status(thm)],[t130219]) ).
cnf(t77417,plain,
meet(complement(one),composition(sk1,complement(one))) = meet(complement(one),composition(sk1,top)),
inference(cp,[status(thm)],[t28274,t77396]) ).
cnf(t68343,plain,
join(X1,composition(converse(sk1),X1)) = composition(one,X1),
inference(cp,[status(thm)],[t68269,t231]) ).
cnf(t131153,plain,
join(X1,composition(converse(sk1),X1)) = X1,
inference(step,[status(thm)],[t68343,t203]) ).
cnf(t70952,plain,
join(X1,composition(converse(sk1),X1)) = X1,
inference(orient,[status(thm)],[t131153]) ).
cnf(t71128,plain,
join(X1,converse(composition(converse(sk1),converse(X1)))) = converse(converse(X1)),
inference(cp,[status(thm)],[t139,t70952]) ).
cnf(t131154,plain,
join(X1,composition(converse(converse(X1)),sk1)) = converse(converse(X1)),
inference(step,[status(thm)],[t71128,t170]) ).
cnf(t131155,plain,
join(X1,composition(X1,sk1)) = converse(converse(X1)),
inference(step,[status(thm)],[t131154,t21]) ).
cnf(t131156,plain,
join(X1,composition(X1,sk1)) = X1,
inference(step,[status(thm)],[t131155,t21]) ).
cnf(t71147,plain,
join(X1,composition(X1,sk1)) = X1,
inference(orient,[status(thm)],[t131156]) ).
cnf(t71329,plain,
join(X1,composition(composition(one,sk1),X1)) = composition(one,X1),
inference(cp,[status(thm)],[t68269,t71147]) ).
cnf(t131162,plain,
join(X1,composition(one,composition(sk1,X1))) = composition(one,X1),
inference(step,[status(thm)],[t71329,t44]) ).
cnf(t131163,plain,
join(X1,composition(sk1,X1)) = composition(one,X1),
inference(step,[status(thm)],[t131162,t203]) ).
cnf(t131164,plain,
join(X1,composition(sk1,X1)) = X1,
inference(step,[status(thm)],[t131163,t203]) ).
cnf(t71485,plain,
join(X1,composition(sk1,X1)) = X1,
inference(orient,[status(thm)],[t131164]) ).
cnf(t71555,plain,
composition(sk1,X1) = meet(composition(sk1,X1),X1),
inference(cp,[status(thm)],[t746,t71485]) ).
cnf(t131174,plain,
composition(sk1,X1) = meet(X1,composition(sk1,X1)),
inference(step,[status(thm)],[t71555,t85]) ).
cnf(t72498,plain,
meet(X1,composition(sk1,X1)) = composition(sk1,X1),
inference(orient,[status(thm)],[t131174]) ).
cnf(t131265,plain,
composition(sk1,complement(one)) = meet(complement(one),composition(sk1,top)),
inference(step,[status(thm)],[t77417,t72498]) ).
cnf(t131266,plain,
composition(sk1,complement(one)) = meet(complement(one),sFlat0),
inference(step,[status(thm)],[t131265,t56]) ).
cnf(t131267,plain,
composition(sk1,complement(one)) = meet(sFlat0,complement(one)),
inference(step,[status(thm)],[t131266,t85]) ).
cnf(t77626,plain,
composition(sk1,complement(one)) = meet(sFlat0,complement(one)),
inference(orient,[status(thm)],[t131267]) ).
cnf(t77632,plain,
composition(sk1,top) = join(sk1,meet(sFlat0,complement(one))),
inference(cp,[status(thm)],[t77396,t77626]) ).
cnf(t131269,plain,
sFlat0 = join(sk1,meet(sFlat0,complement(one))),
inference(step,[status(thm)],[t77632,t56]) ).
cnf(t77726,plain,
join(sk1,meet(sFlat0,complement(one))) = sFlat0,
inference(orient,[status(thm)],[t131269]) ).
cnf(t77754,plain,
join(sk1,complement(meet(sFlat0,complement(one)))) = join(sk1,complement(sFlat0)),
inference(cp,[status(thm)],[t26329,t77726]) ).
cnf(t131270,plain,
join(sk1,join(complement(sFlat0),one)) = join(sk1,complement(sFlat0)),
inference(step,[status(thm)],[t77754,t957]) ).
cnf(t131271,plain,
join(sk1,join(one,complement(sFlat0))) = join(sk1,complement(sFlat0)),
inference(step,[status(thm)],[t131270,t22]) ).
cnf(t43,plain,
join(sk1,join(one,X1)) = join(one,X1),
inference(cp,[status(thm)],[t24,t42]) ).
cnf(t88,plain,
join(sk1,join(one,X1)) = join(one,X1),
inference(orient,[status(thm)],[t43]) ).
cnf(t131272,plain,
join(one,complement(sFlat0)) = join(sk1,complement(sFlat0)),
inference(step,[status(thm)],[t131271,t88]) ).
cnf(t77764,plain,
join(one,complement(sFlat0)) = join(sk1,complement(sFlat0)),
inference(orient,[status(thm)],[t131272]) ).
cnf(t77769,plain,
meet(complement(complement(sFlat0)),one) = meet(complement(complement(sFlat0)),join(sk1,complement(sFlat0))),
inference(cp,[status(thm)],[t27437,t77764]) ).
cnf(t131273,plain,
meet(one,complement(complement(sFlat0))) = meet(complement(complement(sFlat0)),join(sk1,complement(sFlat0))),
inference(step,[status(thm)],[t77769,t85]) ).
cnf(t131274,plain,
meet(one,sFlat0) = meet(complement(complement(sFlat0)),join(sk1,complement(sFlat0))),
inference(step,[status(thm)],[t131273,t332]) ).
cnf(t131275,plain,
meet(sFlat0,one) = meet(complement(complement(sFlat0)),join(sk1,complement(sFlat0))),
inference(step,[status(thm)],[t131274,t85]) ).
cnf(t131276,plain,
meet(sFlat0,one) = meet(complement(complement(sFlat0)),sk1),
inference(step,[status(thm)],[t131275,t27437]) ).
cnf(t131277,plain,
meet(sFlat0,one) = meet(sk1,complement(complement(sFlat0))),
inference(step,[status(thm)],[t131276,t85]) ).
cnf(t131278,plain,
meet(sFlat0,one) = meet(sk1,sFlat0),
inference(step,[status(thm)],[t131277,t332]) ).
cnf(t131279,plain,
meet(sFlat0,one) = meet(sFlat0,sk1),
inference(step,[status(thm)],[t131278,t85]) ).
cnf(t503,plain,
composition(top,converse(sk1)) = converse(sFlat0),
inference(cp,[status(thm)],[t502,t56]) ).
cnf(t514,plain,
composition(top,converse(sk1)) = converse(sFlat0),
inference(orient,[status(thm)],[t503]) ).
cnf(t517,plain,
composition(join(top,X1),converse(sk1)) = join(converse(sFlat0),composition(X1,converse(sk1))),
inference(cp,[status(thm)],[t30,t514]) ).
cnf(t129810,plain,
composition(top,converse(sk1)) = join(converse(sFlat0),composition(X1,converse(sk1))),
inference(step,[status(thm)],[t517,t457]) ).
cnf(t129811,plain,
converse(sFlat0) = join(converse(sFlat0),composition(X1,converse(sk1))),
inference(step,[status(thm)],[t129810,t514]) ).
cnf(t3305,plain,
join(converse(sFlat0),composition(X1,converse(sk1))) = converse(sFlat0),
inference(orient,[status(thm)],[t129811]) ).
cnf(t3307,plain,
converse(sFlat0) = join(converse(sFlat0),converse(sk1)),
inference(cp,[status(thm)],[t3305,t203]) ).
cnf(t129812,plain,
converse(sFlat0) = converse(join(sFlat0,sk1)),
inference(step,[status(thm)],[t3307,t37]) ).
cnf(t3318,plain,
converse(join(sFlat0,sk1)) = converse(sFlat0),
inference(orient,[status(thm)],[t129812]) ).
cnf(t3319,plain,
join(sFlat0,sk1) = converse(converse(sFlat0)),
inference(cp,[status(thm)],[t21,t3318]) ).
cnf(t129813,plain,
join(sFlat0,sk1) = sFlat0,
inference(step,[status(thm)],[t3319,t21]) ).
cnf(t3337,plain,
join(sFlat0,sk1) = sFlat0,
inference(orient,[status(thm)],[t129813]) ).
cnf(t3340,plain,
sk1 = meet(sk1,sFlat0),
inference(cp,[status(thm)],[t746,t3337]) ).
cnf(t129814,plain,
sk1 = meet(sFlat0,sk1),
inference(step,[status(thm)],[t3340,t85]) ).
cnf(t3347,plain,
meet(sFlat0,sk1) = sk1,
inference(orient,[status(thm)],[t129814]) ).
cnf(t131280,plain,
meet(sFlat0,one) = sk1,
inference(step,[status(thm)],[t131279,t3347]) ).
cnf(t77810,plain,
meet(sFlat0,one) = sk1,
inference(orient,[status(thm)],[t131280]) ).
cnf(t77847,plain,
composition(converse(one),sk1) = composition(converse(sk1),sk1),
inference(cp,[status(thm)],[t33856,t77810]) ).
cnf(t131315,plain,
composition(one,sk1) = composition(converse(sk1),sk1),
inference(step,[status(thm)],[t77847,t192]) ).
cnf(t131316,plain,
sk1 = composition(converse(sk1),sk1),
inference(step,[status(thm)],[t131315,t203]) ).
cnf(t77947,plain,
composition(converse(sk1),sk1) = sk1,
inference(orient,[status(thm)],[t131316]) ).
cnf(t77965,plain,
composition(converse(sk1),sk1) = converse(sk1),
inference(cp,[status(thm)],[t170,t77947]) ).
cnf(t131318,plain,
sk1 = converse(sk1),
inference(step,[status(thm)],[t77965,t77947]) ).
cnf(t77976,plain,
converse(sk1) = sk1,
inference(orient,[status(thm)],[t131318]) ).
cnf(t77983,plain,
converse(join(X1,sk1)) = join(converse(X1),sk1),
inference(cp,[status(thm)],[t37,t77976]) ).
cnf(t131427,plain,
converse(join(X1,sk1)) = join(sk1,converse(X1)),
inference(step,[status(thm)],[t77983,t22]) ).
cnf(t79360,plain,
converse(join(X1,sk1)) = join(sk1,converse(X1)),
inference(orient,[status(thm)],[t131427]) ).
cnf(t131429,plain,
composition(join(sk1,converse(sFlat1)),complement(sFlat0)) = zero,
inference(step,[status(thm)],[t65434,t79360]) ).
cnf(t79439,plain,
composition(join(sk1,converse(sFlat1)),complement(sFlat0)) = zero,
inference(rw,[status(thm)],[t131429]) ).
cnf(t96051,plain,
composition(join(sk1,converse(sFlat1)),complement(sFlat0)) = zero,
inference(orient,[status(thm)],[t79439]) ).
cnf(t3314,plain,
join(sFlat0,converse(composition(X1,converse(sk1)))) = converse(converse(sFlat0)),
inference(cp,[status(thm)],[t139,t3305]) ).
cnf(t129819,plain,
join(sFlat0,composition(sk1,converse(X1))) = converse(converse(sFlat0)),
inference(step,[status(thm)],[t3314,t158]) ).
cnf(t129820,plain,
join(sFlat0,composition(sk1,converse(X1))) = sFlat0,
inference(step,[status(thm)],[t129819,t21]) ).
cnf(t3508,plain,
join(sFlat0,composition(sk1,converse(X1))) = sFlat0,
inference(orient,[status(thm)],[t129820]) ).
cnf(t3514,plain,
sFlat0 = join(sFlat0,composition(sk1,X1)),
inference(cp,[status(thm)],[t3508,t21]) ).
cnf(t3527,plain,
join(sFlat0,composition(sk1,X1)) = sFlat0,
inference(orient,[status(thm)],[t3514]) ).
cnf(t3537,plain,
zero = meet(composition(sk1,X1),complement(sFlat0)),
inference(cp,[status(thm)],[t1202,t3527]) ).
cnf(t129839,plain,
zero = meet(complement(sFlat0),composition(sk1,X1)),
inference(step,[status(thm)],[t3537,t85]) ).
cnf(t3904,plain,
meet(complement(sFlat0),composition(sk1,X1)) = zero,
inference(orient,[status(thm)],[t129839]) ).
cnf(t72503,plain,
composition(sk1,complement(sFlat0)) = zero,
inference(cp,[status(thm)],[t72498,t3904]) ).
cnf(t72875,plain,
composition(sk1,complement(sFlat0)) = zero,
inference(orient,[status(thm)],[t72503]) ).
cnf(t72877,plain,
composition(join(sk1,X1),complement(sFlat0)) = join(zero,composition(X1,complement(sFlat0))),
inference(cp,[status(thm)],[t30,t72875]) ).
cnf(t131746,plain,
composition(join(sk1,X1),complement(sFlat0)) = composition(X1,complement(sFlat0)),
inference(step,[status(thm)],[t72877,t304]) ).
cnf(t102887,plain,
composition(join(sk1,X1),complement(sFlat0)) = composition(X1,complement(sFlat0)),
inference(orient,[status(thm)],[t131746]) ).
cnf(t131747,plain,
composition(converse(sFlat1),complement(sFlat0)) = zero,
inference(step,[status(thm)],[t96051,t102887]) ).
cnf(t102965,plain,
composition(converse(sFlat1),complement(sFlat0)) = zero,
inference(rw,[status(thm)],[t131747]) ).
cnf(t102966,plain,
composition(converse(sFlat1),complement(sFlat0)) = zero,
inference(orient,[status(thm)],[t102965]) ).
cnf(t102970,plain,
composition(join(X1,converse(complement(sFlat0))),converse(converse(sFlat1))) = join(composition(X1,converse(converse(sFlat1))),converse(zero)),
inference(cp,[status(thm)],[t14922,t102966]) ).
cnf(t132011,plain,
composition(join(X1,converse(complement(sFlat0))),sFlat1) = join(composition(X1,converse(converse(sFlat1))),converse(zero)),
inference(step,[status(thm)],[t102970,t21]) ).
cnf(t132012,plain,
composition(join(X1,converse(complement(sFlat0))),sFlat1) = join(converse(zero),composition(X1,converse(converse(sFlat1)))),
inference(step,[status(thm)],[t132011,t22]) ).
cnf(t132013,plain,
composition(join(X1,converse(complement(sFlat0))),sFlat1) = composition(X1,converse(converse(sFlat1))),
inference(step,[status(thm)],[t132012,t356]) ).
cnf(t132014,plain,
composition(join(X1,converse(complement(sFlat0))),sFlat1) = composition(X1,sFlat1),
inference(step,[status(thm)],[t132013,t21]) ).
cnf(t129287,plain,
composition(join(X1,converse(complement(sFlat0))),sFlat1) = composition(X1,sFlat1),
inference(orient,[status(thm)],[t132014]) ).
cnf(t77780,plain,
join(one,converse(complement(sFlat0))) = converse(join(sk1,complement(sFlat0))),
inference(cp,[status(thm)],[t207,t77764]) ).
cnf(t77982,plain,
converse(join(sk1,X1)) = join(sk1,converse(X1)),
inference(cp,[status(thm)],[t37,t77976]) ).
cnf(t79250,plain,
converse(join(sk1,X1)) = join(sk1,converse(X1)),
inference(orient,[status(thm)],[t77982]) ).
cnf(t131487,plain,
join(one,converse(complement(sFlat0))) = join(sk1,converse(complement(sFlat0))),
inference(step,[status(thm)],[t77780,t79250]) ).
cnf(t81165,plain,
join(one,converse(complement(sFlat0))) = join(sk1,converse(complement(sFlat0))),
inference(orient,[status(thm)],[t131487]) ).
cnf(t129292,plain,
composition(one,sFlat1) = composition(join(sk1,converse(complement(sFlat0))),sFlat1),
inference(cp,[status(thm)],[t129287,t81165]) ).
cnf(t132015,plain,
sFlat1 = composition(join(sk1,converse(complement(sFlat0))),sFlat1),
inference(step,[status(thm)],[t129292,t203]) ).
cnf(t33859,plain,
composition(converse(sk2),sk1) = composition(converse(sFlat1),sk1),
inference(cp,[status(thm)],[t33856,t75]) ).
cnf(t33889,plain,
composition(converse(sk2),sk1) = composition(converse(sFlat1),sk1),
inference(orient,[status(thm)],[t33859]) ).
cnf(t33903,plain,
composition(converse(sk1),sk2) = converse(composition(converse(sFlat1),sk1)),
inference(cp,[status(thm)],[t170,t33889]) ).
cnf(t130386,plain,
composition(converse(sk1),sk2) = composition(converse(sk1),sFlat1),
inference(step,[status(thm)],[t33903,t170]) ).
cnf(t33931,plain,
composition(converse(sk1),sk2) = composition(converse(sk1),sFlat1),
inference(orient,[status(thm)],[t130386]) ).
cnf(t131335,plain,
composition(sk1,sk2) = composition(converse(sk1),sFlat1),
inference(step,[status(thm)],[t33931,t77976]) ).
cnf(t131336,plain,
sFlat2 = composition(converse(sk1),sFlat1),
inference(step,[status(thm)],[t131335,t61]) ).
cnf(t131337,plain,
sFlat2 = composition(sk1,sFlat1),
inference(step,[status(thm)],[t131336,t77976]) ).
cnf(t78052,plain,
sFlat2 = composition(sk1,sFlat1),
inference(rw,[status(thm)],[t131337]) ).
cnf(t78174,plain,
composition(sk1,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t78052]) ).
cnf(t78180,plain,
composition(join(sk1,X1),sFlat1) = join(sFlat2,composition(X1,sFlat1)),
inference(cp,[status(thm)],[t30,t78174]) ).
cnf(t82604,plain,
composition(join(sk1,X1),sFlat1) = join(sFlat2,composition(X1,sFlat1)),
inference(orient,[status(thm)],[t78180]) ).
cnf(t132016,plain,
sFlat1 = join(sFlat2,composition(converse(complement(sFlat0)),sFlat1)),
inference(step,[status(thm)],[t132015,t82604]) ).
cnf(t102979,plain,
composition(converse(complement(sFlat0)),sFlat1) = converse(zero),
inference(cp,[status(thm)],[t170,t102966]) ).
cnf(t131748,plain,
composition(converse(complement(sFlat0)),sFlat1) = zero,
inference(step,[status(thm)],[t102979,t361]) ).
cnf(t102989,plain,
composition(converse(complement(sFlat0)),sFlat1) = zero,
inference(orient,[status(thm)],[t131748]) ).
cnf(t132017,plain,
sFlat1 = join(sFlat2,zero),
inference(step,[status(thm)],[t132016,t102989]) ).
cnf(t132018,plain,
sFlat1 = sFlat2,
inference(step,[status(thm)],[t132017,t325]) ).
cnf(t129319,plain,
sFlat2 = sFlat1,
inference(orient,[status(thm)],[t132018]) ).
cnf(t132019,plain,
composition(sk1,sk2) = sFlat1,
inference(step,[status(thm)],[t61,t129319]) ).
cnf(t129320,plain,
composition(sk1,sk2) = sFlat1,
inference(orient,[status(thm)],[t132019]) ).
cnf(goal_0,negated_conjecture,
meet(composition(sk1,top),sk2) != composition(sk1,sk2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
meet(sk2,composition(sk1,top)) != composition(sk1,sk2),
inference(rw,[status(thm)],[goal_0,t85]) ).
cnf(g0_1,plain,
meet(sk2,sFlat0) != composition(sk1,sk2),
inference(rw,[status(thm)],[g0_0,t56]) ).
cnf(g0_2,plain,
meet(sFlat0,sk2) != composition(sk1,sk2),
inference(rw,[status(thm)],[g0_1,t85]) ).
cnf(g0_3,plain,
sFlat1 != composition(sk1,sk2),
inference(rw,[status(thm)],[g0_2,t75]) ).
cnf(g0_4,plain,
sFlat1 != sFlat1,
inference(rw,[status(thm)],[g0_3,t129320]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL026-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n005.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Thu Sep 24 07:20:50 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 78.76/10.33 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 78.76/10.33 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------