%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL006+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 : n007.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:39 PM UTC 2026
% Result : Theorem 6.94s 1.51s
% Output : Proof 6.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 79
% Number of leaves : 12
% Syntax : Number of formulae : 248 ( 244 unt; 0 def)
% Number of atoms : 252 ( 251 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 10 ( 6 ~; 0 |; 2 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 331 ( 51 sgn 61 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',maddux4_definiton_of_meet) ).
fof(f3_nnf,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t6,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t39,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t6]) ).
fof(f1,axiom,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',maddux2_join_associativity) ).
fof(f1_nnf,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t10,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t21,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
fof(f10,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',converse_cancellativity) ).
fof(f10_nnf,plain,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t12,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(equality_encoding,[status(esa)],[c10]) ).
fof(f0,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',maddux1_join_commutativity) ).
fof(f0_nnf,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t5,plain,
join(X1,X2) = join(X2,X1),
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t19,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t2233,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t12,t19]) ).
cnf(t30,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t2233]) ).
fof(f9,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',converse_multiplicativity) ).
fof(f9_nnf,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t7,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t51,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t7]) ).
fof(f7,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',converse_idempotence) ).
fof(f7_nnf,plain,
! [X0] : converse(converse(X0)) = X0,
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X0] : converse(converse(X0)) = X0,
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
converse(converse(X0)) = X0,
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t1,plain,
converse(converse(X1)) = X1,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t18,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t53,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t51,t18]) ).
cnf(t131,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t53]) ).
fof(f5,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',composition_identity) ).
fof(f5_nnf,plain,
! [X0] : composition(X0,one) = X0,
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X0] : composition(X0,one) = X0,
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
composition(X0,one) = X0,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t0,plain,
composition(X1,one) = X1,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t17,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t132,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t131,t17]) ).
cnf(t2239,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t132,t18]) ).
cnf(t146,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t2239]) ).
cnf(t147,plain,
one = converse(one),
inference(cp,[status(thm)],[t146,t17]) ).
cnf(t153,plain,
converse(one) = one,
inference(orient,[status(thm)],[t147]) ).
cnf(t2240,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t146,t153]) ).
cnf(t163,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t2240]) ).
cnf(t164,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t163]) ).
cnf(t167,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t30,t164]) ).
cnf(t2242,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t167,t153]) ).
cnf(t2243,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t2242,t164]) ).
cnf(t191,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t2243]) ).
cnf(t201,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t39,t191]) ).
cnf(t208,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t201]) ).
fof(f2,axiom,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',maddux3_a_kind_of_de_Morgan) ).
fof(f2_nnf,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t13,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t14,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t13]) ).
cnf(t20,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t14]) ).
cnf(t2255,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t20,t19]) ).
cnf(t2256,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t2255,t39]) ).
cnf(t2257,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t2256,t19]) ).
cnf(t288,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t2257]) ).
fof(f12,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_zero) ).
fof(f12_nnf,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
zero = meet(X0,complement(X0)),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(t3,plain,
meet(X1,complement(X1)) = zero,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t58,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t3]) ).
cnf(t289,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t288,t58]) ).
cnf(t2264,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t289,t39]) ).
cnf(t325,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t2264]) ).
fof(f11,axiom,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',def_top) ).
fof(f11_nnf,plain,
! [X0] : top = join(X0,complement(X0)),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X0] : top = join(X0,complement(X0)),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
top = join(X0,complement(X0)),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t2,plain,
join(X1,complement(X1)) = top,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t24,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t2]) ).
cnf(t40,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t39,t24]) ).
cnf(t2234,plain,
zero = complement(top),
inference(step,[status(thm)],[t40,t58]) ).
cnf(t61,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t2234]) ).
cnf(t195,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t191,t61]) ).
cnf(t2244,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t195,t61]) ).
cnf(t2245,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t2244,t61]) ).
cnf(t202,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t2245]) ).
cnf(t203,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t21,t202]) ).
cnf(t218,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t203]) ).
cnf(t327,plain,
join(zero,meet(X1,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t218,t325]) ).
cnf(t2265,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t327,t325]) ).
cnf(t329,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t2265]) ).
cnf(t2266,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t325,t329]) ).
cnf(t336,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t2266]) ).
cnf(t351,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t336]) ).
cnf(t2272,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t208,t351]) ).
cnf(t353,plain,
X1 = complement(complement(X1)),
inference(rw,[status(thm)],[t2272]) ).
cnf(t360,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t353]) ).
cnf(t362,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t191,t360]) ).
cnf(t2279,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t362,t360]) ).
cnf(t2280,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t2279,t360]) ).
cnf(t371,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t2280]) ).
cnf(t373,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t21,t371]) ).
cnf(t445,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t373]) ).
cnf(t449,plain,
join(X1,X2) = join(X1,join(X2,X1)),
inference(cp,[status(thm)],[t445,t19]) ).
cnf(t464,plain,
join(X1,join(X2,X1)) = join(X1,X2),
inference(orient,[status(thm)],[t449]) ).
cnf(t26,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t21,t24]) ).
cnf(t251,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t26]) ).
cnf(t213,plain,
top = join(complement(X1),meet(X1,X1)),
inference(cp,[status(thm)],[t24,t208]) ).
cnf(t229,plain,
join(complement(X1),meet(X1,X1)) = top,
inference(orient,[status(thm)],[t213]) ).
cnf(t255,plain,
join(top,meet(X1,X1)) = join(X1,top),
inference(cp,[status(thm)],[t251,t229]) ).
cnf(t257,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t251,t191]) ).
cnf(t2250,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t257,t24]) ).
cnf(t268,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t2250]) ).
cnf(t269,plain,
top = join(top,meet(X1,X2)),
inference(cp,[status(thm)],[t268,t39]) ).
cnf(t276,plain,
join(top,meet(X1,X2)) = top,
inference(orient,[status(thm)],[t269]) ).
cnf(t2252,plain,
top = join(X1,top),
inference(step,[status(thm)],[t255,t276]) ).
cnf(t282,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t2252]) ).
cnf(t283,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t282,t19]) ).
cnf(t309,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t283]) ).
cnf(t2258,plain,
join(X1,join(complement(X1),X2)) = top,
inference(step,[status(thm)],[t251,t309]) ).
cnf(t310,plain,
join(X1,join(complement(X1),X2)) = top,
inference(orient,[status(thm)],[t2258]) ).
cnf(t466,plain,
join(join(complement(X1),X2),X1) = join(join(complement(X1),X2),top),
inference(cp,[status(thm)],[t464,t310]) ).
cnf(t2293,plain,
join(complement(X1),join(X2,X1)) = join(join(complement(X1),X2),top),
inference(step,[status(thm)],[t466,t21]) ).
cnf(t2294,plain,
join(complement(X1),join(X2,X1)) = join(complement(X1),join(X2,top)),
inference(step,[status(thm)],[t2293,t21]) ).
cnf(t2295,plain,
join(complement(X1),join(X2,X1)) = join(complement(X1),top),
inference(step,[status(thm)],[t2294,t282]) ).
cnf(t2296,plain,
join(complement(X1),join(X2,X1)) = top,
inference(step,[status(thm)],[t2295,t282]) ).
cnf(t522,plain,
join(complement(X1),join(X2,X1)) = top,
inference(orient,[status(thm)],[t2296]) ).
cnf(t447,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t445,t288]) ).
cnf(t2284,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t447,t288]) ).
cnf(t2285,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t2284,t19]) ).
cnf(t451,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t2285]) ).
cnf(t41,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t39,t19]) ).
cnf(t2236,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t41,t39]) ).
cnf(t70,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t2236]) ).
cnf(t453,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t451,t70]) ).
cnf(t458,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t453]) ).
cnf(t529,plain,
top = join(complement(meet(X1,X2)),X2),
inference(cp,[status(thm)],[t522,t458]) ).
cnf(t2302,plain,
top = join(X2,complement(meet(X1,X2))),
inference(step,[status(thm)],[t529,t19]) ).
cnf(t557,plain,
join(X1,complement(meet(X2,X1))) = top,
inference(orient,[status(thm)],[t2302]) ).
cnf(t562,plain,
meet(X1,meet(X2,complement(X1))) = complement(top),
inference(cp,[status(thm)],[t39,t557]) ).
cnf(t2304,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(step,[status(thm)],[t562,t61]) ).
cnf(t571,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(orient,[status(thm)],[t2304]) ).
cnf(t572,plain,
zero = meet(complement(X1),meet(X2,X1)),
inference(cp,[status(thm)],[t571,t360]) ).
cnf(t582,plain,
meet(complement(X1),meet(X2,X1)) = zero,
inference(orient,[status(thm)],[t572]) ).
cnf(t368,plain,
top = join(complement(X1),join(X1,X2)),
inference(cp,[status(thm)],[t310,t360]) ).
cnf(t474,plain,
join(complement(X1),join(X1,X2)) = top,
inference(orient,[status(thm)],[t368]) ).
cnf(t487,plain,
X1 = join(meet(X1,join(X1,X2)),complement(top)),
inference(cp,[status(thm)],[t288,t474]) ).
cnf(t2286,plain,
X1 = join(complement(top),meet(X1,join(X1,X2))),
inference(step,[status(thm)],[t487,t19]) ).
cnf(t2287,plain,
X1 = join(zero,meet(X1,join(X1,X2))),
inference(step,[status(thm)],[t2286,t61]) ).
cnf(t2288,plain,
X1 = meet(X1,join(X1,X2)),
inference(step,[status(thm)],[t2287,t329]) ).
cnf(t488,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t2288]) ).
cnf(t588,plain,
zero = meet(complement(join(X1,X2)),X1),
inference(cp,[status(thm)],[t582,t488]) ).
cnf(t2305,plain,
zero = meet(X1,complement(join(X1,X2))),
inference(step,[status(thm)],[t588,t70]) ).
cnf(t591,plain,
meet(X1,complement(join(X1,X2))) = zero,
inference(orient,[status(thm)],[t2305]) ).
fof(f8,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',converse_additivity) ).
fof(f8_nnf,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t8,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t34,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t36,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t34,t18]) ).
cnf(t100,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t36]) ).
cnf(t462,plain,
join(X1,converse(meet(X2,converse(X1)))) = converse(converse(X1)),
inference(cp,[status(thm)],[t100,t458]) ).
cnf(t2309,plain,
join(X1,converse(meet(X2,converse(X1)))) = X1,
inference(step,[status(thm)],[t462,t18]) ).
cnf(t744,plain,
join(X1,converse(meet(X2,converse(X1)))) = X1,
inference(orient,[status(thm)],[t2309]) ).
cnf(t361,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(cp,[status(thm)],[t360,t39]) ).
cnf(t608,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t361]) ).
cnf(t611,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(cp,[status(thm)],[t608,t360]) ).
cnf(t638,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(orient,[status(thm)],[t611]) ).
cnf(t648,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),X2)),
inference(cp,[status(thm)],[t360,t638]) ).
cnf(t685,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t648]) ).
cnf(t2307,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t288,t685]) ).
cnf(t711,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(rw,[status(thm)],[t2307]) ).
cnf(t1908,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t711]) ).
cnf(t493,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t488,t19]) ).
cnf(t494,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t493]) ).
cnf(t589,plain,
zero = meet(complement(join(X1,X2)),X2),
inference(cp,[status(thm)],[t582,t494]) ).
cnf(t2306,plain,
zero = meet(X2,complement(join(X1,X2))),
inference(step,[status(thm)],[t589,t70]) ).
cnf(t597,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(orient,[status(thm)],[t2306]) ).
cnf(t598,plain,
zero = meet(join(X1,X2),complement(join(X2,X1))),
inference(cp,[status(thm)],[t597,t464]) ).
cnf(t1785,plain,
meet(join(X1,X2),complement(join(X2,X1))) = zero,
inference(orient,[status(thm)],[t598]) ).
cnf(t563,plain,
join(X1,converse(complement(meet(X2,converse(X1))))) = converse(top),
inference(cp,[status(thm)],[t100,t557]) ).
cnf(t101,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t100,t24]) ).
cnf(t234,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t101]) ).
cnf(t312,plain,
top = converse(top),
inference(cp,[status(thm)],[t309,t234]) ).
cnf(t315,plain,
converse(top) = top,
inference(orient,[status(thm)],[t312]) ).
cnf(t2332,plain,
join(X1,converse(complement(meet(X2,converse(X1))))) = top,
inference(step,[status(thm)],[t563,t315]) ).
cnf(t1746,plain,
join(X1,converse(complement(meet(X2,converse(X1))))) = top,
inference(orient,[status(thm)],[t2332]) ).
cnf(t490,plain,
converse(X1) = meet(converse(X1),converse(join(X1,X2))),
inference(cp,[status(thm)],[t488,t34]) ).
cnf(t959,plain,
meet(converse(X1),converse(join(X1,X2))) = converse(X1),
inference(orient,[status(thm)],[t490]) ).
fof(f13,conjecture,
! [X0,X1] :
( meet(converse(X0),X1) = zero
=> meet(X0,converse(X1)) = zero ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f13_neg,negated_conjecture,
~ ! [X0,X1] :
( meet(converse(X0),X1) = zero
=> meet(X0,converse(X1)) = zero ),
inference(negated_conjecture,[status(cth)],[f13]) ).
fof(f13_nnf,plain,
? [X0,X1] :
( meet(X0,converse(X1)) != zero
& meet(converse(X0),X1) = zero ),
inference(nnf_transformation,[status(thm)],[f13_neg]) ).
fof(f13_sk,plain,
( meet(sk0,converse(sk1)) != zero
& meet(converse(sk0),sk1) = zero ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1])],[f13_nnf]) ).
cnf(c13,plain,
meet(converse(sk0),sk1) = zero,
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(t4,plain,
meet(converse(sk0),sk1) = zero,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t60,plain,
meet(converse(sk0),sk1) = zero,
inference(orient,[status(thm)],[t4]) ).
cnf(t72,plain,
meet(converse(sk0),sk1) = zero,
inference(rw,[status(thm)],[t60]) ).
cnf(t2238,plain,
meet(sk1,converse(sk0)) = zero,
inference(step,[status(thm)],[t72,t70]) ).
cnf(t74,plain,
meet(sk1,converse(sk0)) = zero,
inference(orient,[status(thm)],[t2238]) ).
cnf(t1919,plain,
sk1 = join(zero,meet(sk1,complement(converse(sk0)))),
inference(cp,[status(thm)],[t1908,t74]) ).
cnf(t2334,plain,
sk1 = meet(sk1,complement(converse(sk0))),
inference(step,[status(thm)],[t1919,t329]) ).
cnf(t1959,plain,
meet(sk1,complement(converse(sk0))) = sk1,
inference(orient,[status(thm)],[t2334]) ).
cnf(t1974,plain,
join(complement(sk1),converse(sk0)) = complement(sk1),
inference(cp,[status(thm)],[t638,t1959]) ).
cnf(t2335,plain,
join(converse(sk0),complement(sk1)) = complement(sk1),
inference(step,[status(thm)],[t1974,t19]) ).
cnf(t1978,plain,
join(converse(sk0),complement(sk1)) = complement(sk1),
inference(orient,[status(thm)],[t2335]) ).
cnf(t1991,plain,
converse(converse(sk0)) = meet(converse(converse(sk0)),converse(complement(sk1))),
inference(cp,[status(thm)],[t959,t1978]) ).
cnf(t2336,plain,
sk0 = meet(converse(converse(sk0)),converse(complement(sk1))),
inference(step,[status(thm)],[t1991,t18]) ).
cnf(t2337,plain,
sk0 = meet(sk0,converse(complement(sk1))),
inference(step,[status(thm)],[t2336,t18]) ).
cnf(t2000,plain,
meet(sk0,converse(complement(sk1))) = sk0,
inference(orient,[status(thm)],[t2337]) ).
cnf(t2018,plain,
top = join(complement(sk1),converse(complement(sk0))),
inference(cp,[status(thm)],[t1746,t2000]) ).
cnf(t2179,plain,
join(complement(sk1),converse(complement(sk0))) = top,
inference(orient,[status(thm)],[t2018]) ).
cnf(t2183,plain,
zero = meet(top,complement(join(converse(complement(sk0)),complement(sk1)))),
inference(cp,[status(thm)],[t1785,t2179]) ).
cnf(t64,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t39,t61]) ).
cnf(t77,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t64]) ).
cnf(t2269,plain,
complement(complement(X1)) = meet(top,X1),
inference(step,[status(thm)],[t77,t329]) ).
cnf(t338,plain,
complement(complement(X1)) = meet(top,X1),
inference(rw,[status(thm)],[t2269]) ).
cnf(t2281,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t338,t360]) ).
cnf(t374,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t2281]) ).
cnf(t2342,plain,
zero = complement(join(converse(complement(sk0)),complement(sk1))),
inference(step,[status(thm)],[t2183,t374]) ).
cnf(t610,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(cp,[status(thm)],[t608,t360]) ).
cnf(t617,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t610]) ).
cnf(t628,plain,
meet(complement(X1),X2) = complement(join(X1,complement(X2))),
inference(cp,[status(thm)],[t360,t617]) ).
cnf(t659,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t628]) ).
cnf(t2343,plain,
zero = meet(complement(converse(complement(sk0))),sk1),
inference(step,[status(thm)],[t2342,t659]) ).
cnf(t2344,plain,
zero = meet(sk1,complement(converse(complement(sk0)))),
inference(step,[status(thm)],[t2343,t70]) ).
cnf(t2189,plain,
meet(sk1,complement(converse(complement(sk0)))) = zero,
inference(orient,[status(thm)],[t2344]) ).
cnf(t2190,plain,
sk1 = join(zero,meet(sk1,complement(complement(converse(complement(sk0)))))),
inference(cp,[status(thm)],[t1908,t2189]) ).
cnf(t2345,plain,
sk1 = meet(sk1,complement(complement(converse(complement(sk0))))),
inference(step,[status(thm)],[t2190,t329]) ).
cnf(t2346,plain,
sk1 = meet(sk1,converse(complement(sk0))),
inference(step,[status(thm)],[t2345,t360]) ).
cnf(t2192,plain,
meet(sk1,converse(complement(sk0))) = sk1,
inference(orient,[status(thm)],[t2346]) ).
cnf(t2209,plain,
complement(sk0) = join(complement(sk0),converse(sk1)),
inference(cp,[status(thm)],[t744,t2192]) ).
cnf(t2347,plain,
complement(sk0) = join(converse(sk1),complement(sk0)),
inference(step,[status(thm)],[t2209,t19]) ).
cnf(t2210,plain,
join(converse(sk1),complement(sk0)) = complement(sk0),
inference(orient,[status(thm)],[t2347]) ).
cnf(t2225,plain,
zero = meet(converse(sk1),complement(complement(sk0))),
inference(cp,[status(thm)],[t591,t2210]) ).
cnf(t2348,plain,
zero = meet(converse(sk1),sk0),
inference(step,[status(thm)],[t2225,t360]) ).
cnf(t2349,plain,
zero = meet(sk0,converse(sk1)),
inference(step,[status(thm)],[t2348,t70]) ).
cnf(t2231,plain,
meet(sk0,converse(sk1)) = zero,
inference(orient,[status(thm)],[t2349]) ).
cnf(c14,plain,
meet(sk0,converse(sk1)) != zero,
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(goal_0,negated_conjecture,
meet(sk0,converse(sk1)) != zero,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(g0_0,plain,
zero != zero,
inference(rw,[status(thm)],[goal_0,t2231]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL006+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.07/0.41 % Computer : n007.cluster.edu
% 0.07/0.41 % Model : x86_64 x86_64
% 0.07/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.41 % Memory : 8046.5625MB
% 0.07/0.41 % OS : Linux 6.8.0-71-generic
% 0.07/0.41 % CPULimit : 300
% 0.07/0.41 % WCLimit : 300
% 0.07/0.41 % DateTime : Thu Sep 24 07:08:38 UTC 2026
% 0.07/0.41 % CPUTime :
% 0.07/0.41 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 6.94/1.51 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.94/1.51 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------