%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL025-2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:34:51 PM UTC 2026
% Result : Unsatisfiable 57.21s 7.65s
% Output : Proof 57.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 100
% Number of leaves : 16
% Syntax : Number of formulae : 505 ( 501 unt; 0 def)
% Number of atoms : 509 ( 508 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 14 ( 10 ~; 4 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 6 con; 0-4 aty)
% Number of variables : 669 ( 40 sgn 50 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f14,negated_conjecture,
( join(converse(sk1),sk1) != sk1
| join(sk1,converse(sk1)) != converse(sk1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_17) ).
fof(f14_nnf,plain,
( join(converse(sk1),sk1) != sk1
| join(sk1,converse(sk1)) != converse(sk1) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
( join(converse(sk1),sk1) != sk1
| join(sk1,converse(sk1)) != converse(sk1) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( join(converse(sk1),sk1) != sk1
| join(sk1,converse(sk1)) != converse(sk1) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(t15,plain,
ifeq(join(sk1,converse(sk1)),converse(sk1),ifeq(join(converse(sk1),sk1),sk1,false,true),true) = true,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(f0,axiom,
join(A,B) = join(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux1_join_commutativity_1) ).
fof(f0_nnf,plain,
! [A,B] : join(A,B) = join(B,A),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B] : join(A,B) = join(B,A),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t6,plain,
join(X1,X2) = join(X2,X1),
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t22,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t33208,plain,
ifeq(join(sk1,converse(sk1)),converse(sk1),ifeq(join(sk1,converse(sk1)),sk1,false,true),true) = true,
inference(step,[status(thm)],[t15,t22]) ).
cnf(t61,plain,
ifeq(join(sk1,converse(sk1)),converse(sk1),ifeq(join(sk1,converse(sk1)),sk1,false,true),true) = true,
inference(orient,[status(thm)],[t33208]) ).
cnf(f3,axiom,
meet(A,B) = complement(join(complement(A),complement(B))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux4_definiton_of_meet_4) ).
fof(f3_nnf,plain,
! [A,B] : meet(A,B) = complement(join(complement(A),complement(B))),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A,B] : meet(A,B) = complement(join(complement(A),complement(B))),
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(t7,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t42,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t7]) ).
cnf(f2,axiom,
A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux3_a_kind_of_de_Morgan_3) ).
fof(f2_nnf,plain,
! [A,B] : A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A,B] : A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))),
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(t14,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t16,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t14]) ).
cnf(t17,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(complement(join(complement(X1),complement(X2))),join(complement(X1),X2)))),
inference(cp,[status(thm)],[t16,t16]) ).
cnf(f1,axiom,
join(A,join(B,C)) = join(join(A,B),C),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux2_join_associativity_2) ).
fof(f1_nnf,plain,
! [A,B,C] : join(A,join(B,C)) = join(join(A,B),C),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A,B,C] : join(A,join(B,C)) = join(join(A,B),C),
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(t11,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t24,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
cnf(t26,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t24,t22]) ).
cnf(t33218,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t26,t24]) ).
cnf(t151,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t33218]) ).
cnf(t33233,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(complement(X1),join(complement(join(complement(X1),complement(X2))),X2)))),
inference(step,[status(thm)],[t17,t151]) ).
cnf(t33234,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(complement(X1),join(X2,complement(join(complement(X1),complement(X2))))))),
inference(step,[status(thm)],[t33233,t22]) ).
cnf(t33235,plain,
join(complement(X1),complement(X2)) = join(complement(X1),complement(join(complement(X1),join(X2,meet(X1,X2))))),
inference(step,[status(thm)],[t33234,t42]) ).
cnf(t251,plain,
join(complement(X1),complement(join(complement(X1),join(X2,meet(X1,X2))))) = join(complement(X1),complement(X2)),
inference(orient,[status(thm)],[t33235]) ).
cnf(t267,plain,
meet(X1,join(complement(X1),join(X2,meet(X1,X2)))) = complement(join(complement(X1),complement(X2))),
inference(cp,[status(thm)],[t42,t251]) ).
cnf(t46,plain,
meet(join(complement(X1),complement(X2)),X3) = complement(join(meet(X1,X2),complement(X3))),
inference(cp,[status(thm)],[t42,t42]) ).
cnf(t597,plain,
complement(join(meet(X1,X2),complement(X3))) = meet(join(complement(X1),complement(X2)),X3),
inference(orient,[status(thm)],[t46]) ).
cnf(t599,plain,
meet(join(complement(X1),complement(X2)),X3) = complement(join(complement(X3),meet(X1,X2))),
inference(cp,[status(thm)],[t597,t22]) ).
cnf(t47,plain,
meet(X1,join(complement(X2),complement(X3))) = complement(join(complement(X1),meet(X2,X3))),
inference(cp,[status(thm)],[t42,t42]) ).
cnf(t623,plain,
complement(join(complement(X1),meet(X2,X3))) = meet(X1,join(complement(X2),complement(X3))),
inference(orient,[status(thm)],[t47]) ).
cnf(t23,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t16]) ).
cnf(t33357,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t23,t22]) ).
cnf(t33358,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t33357,t42]) ).
cnf(t33359,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t33358,t22]) ).
cnf(t1537,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t33359]) ).
cnf(f11,axiom,
top = join(A,complement(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_top_12) ).
fof(f11_nnf,plain,
! [A] : top = join(A,complement(A)),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [A] : top = join(A,complement(A)),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
top = join(X0,complement(X0)),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t3,plain,
join(X1,complement(X1)) = top,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t27,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t3]) ).
cnf(t1572,plain,
X1 = join(meet(X1,complement(complement(X1))),complement(top)),
inference(cp,[status(thm)],[t1537,t27]) ).
cnf(t33362,plain,
X1 = join(complement(top),meet(X1,complement(complement(X1)))),
inference(step,[status(thm)],[t1572,t22]) ).
cnf(t43,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t42,t27]) ).
cnf(f12,axiom,
zero = meet(A,complement(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_zero_13) ).
fof(f12_nnf,plain,
! [A] : zero = meet(A,complement(A)),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [A] : zero = meet(A,complement(A)),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
zero = meet(X0,complement(X0)),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(t4,plain,
meet(X1,complement(X1)) = zero,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t62,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t4]) ).
cnf(t33210,plain,
zero = complement(top),
inference(step,[status(thm)],[t43,t62]) ).
cnf(t65,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t33210]) ).
cnf(t33363,plain,
X1 = join(zero,meet(X1,complement(complement(X1)))),
inference(step,[status(thm)],[t33362,t65]) ).
cnf(t29,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t24,t27]) ).
cnf(t217,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t29]) ).
cnf(t256,plain,
join(complement(X1),complement(complement(complement(X1)))) = join(complement(X1),complement(join(top,meet(X1,complement(complement(X1)))))),
inference(cp,[status(thm)],[t251,t217]) ).
cnf(f10,axiom,
join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_cancellativity_11) ).
fof(f10_nnf,plain,
! [A,B] : join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [A,B] : join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B),
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(t13,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t33207,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t13,t22]) ).
cnf(t36,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t33207]) ).
cnf(f9,axiom,
converse(composition(A,B)) = composition(converse(B),converse(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_multiplicativity_10) ).
fof(f9_nnf,plain,
! [A,B] : converse(composition(A,B)) = composition(converse(B),converse(A)),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [A,B] : converse(composition(A,B)) = composition(converse(B),converse(A)),
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(t8,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t49,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t8]) ).
cnf(f7,axiom,
converse(converse(A)) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_idempotence_8) ).
fof(f7_nnf,plain,
! [A] : converse(converse(A)) = A,
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [A] : converse(converse(A)) = A,
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(t19,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t51,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t49,t19]) ).
cnf(t111,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t51]) ).
cnf(f5,axiom,
composition(A,one) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_identity_6) ).
fof(f5_nnf,plain,
! [A] : composition(A,one) = A,
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [A] : composition(A,one) = A,
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(t20,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t112,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t111,t20]) ).
cnf(t33215,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t112,t19]) ).
cnf(t126,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t33215]) ).
cnf(f4,axiom,
composition(A,composition(B,C)) = composition(composition(A,B),C),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_associativity_5) ).
fof(f4_nnf,plain,
! [A,B,C] : composition(A,composition(B,C)) = composition(composition(A,B),C),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A,B,C] : composition(A,composition(B,C)) = composition(composition(A,B),C),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t10,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t55,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t56,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(cp,[status(thm)],[t55,t20]) ).
cnf(t74,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(orient,[status(thm)],[t56]) ).
cnf(t128,plain,
composition(one,X1) = composition(converse(one),X1),
inference(cp,[status(thm)],[t126,t74]) ).
cnf(t33217,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t128,t126]) ).
cnf(t144,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t33217]) ).
cnf(t147,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t36,t144]) ).
cnf(t127,plain,
one = converse(one),
inference(cp,[status(thm)],[t126,t20]) ).
cnf(t133,plain,
converse(one) = one,
inference(orient,[status(thm)],[t127]) ).
cnf(t33221,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t147,t133]) ).
cnf(t33222,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t33221,t144]) ).
cnf(t195,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t33222]) ).
cnf(t221,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t217,t195]) ).
cnf(t33226,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t221,t27]) ).
cnf(t234,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t33226]) ).
cnf(t235,plain,
top = join(top,meet(X1,X2)),
inference(cp,[status(thm)],[t234,t42]) ).
cnf(t248,plain,
join(top,meet(X1,X2)) = top,
inference(orient,[status(thm)],[t235]) ).
cnf(t33268,plain,
join(complement(X1),complement(complement(complement(X1)))) = join(complement(X1),complement(top)),
inference(step,[status(thm)],[t256,t248]) ).
cnf(t33269,plain,
join(complement(X1),complement(complement(complement(X1)))) = join(complement(X1),zero),
inference(step,[status(thm)],[t33268,t65]) ).
cnf(t33270,plain,
join(complement(X1),complement(complement(complement(X1)))) = join(zero,complement(X1)),
inference(step,[status(thm)],[t33269,t22]) ).
cnf(t520,plain,
join(complement(X1),complement(complement(complement(X1)))) = join(zero,complement(X1)),
inference(orient,[status(thm)],[t33270]) ).
cnf(t530,plain,
meet(X1,complement(complement(X1))) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t42,t520]) ).
cnf(t68,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t42,t65]) ).
cnf(t178,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t68]) ).
cnf(t33276,plain,
meet(X1,complement(complement(X1))) = meet(top,X1),
inference(step,[status(thm)],[t530,t178]) ).
cnf(t534,plain,
meet(X1,complement(complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t33276]) ).
cnf(t33364,plain,
X1 = join(zero,meet(top,X1)),
inference(step,[status(thm)],[t33363,t534]) ).
cnf(t1611,plain,
join(zero,meet(top,X1)) = X1,
inference(orient,[status(thm)],[t33364]) ).
cnf(t603,plain,
meet(join(complement(X1),complement(X2)),top) = complement(join(meet(X1,X2),zero)),
inference(cp,[status(thm)],[t597,t65]) ).
cnf(t44,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t42,t22]) ).
cnf(t33209,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t44,t42]) ).
cnf(t64,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t33209]) ).
cnf(t33347,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(meet(X1,X2),zero)),
inference(step,[status(thm)],[t603,t64]) ).
cnf(t33348,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(step,[status(thm)],[t33347,t22]) ).
cnf(t1269,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(orient,[status(thm)],[t33348]) ).
cnf(t1270,plain,
complement(join(zero,meet(X1,X1))) = meet(top,complement(X1)),
inference(cp,[status(thm)],[t1269,t195]) ).
cnf(t1287,plain,
complement(join(zero,meet(X1,X1))) = meet(top,complement(X1)),
inference(orient,[status(thm)],[t1270]) ).
cnf(t1539,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t1537,t62]) ).
cnf(t33360,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t1539,t42]) ).
cnf(t1596,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t33360]) ).
cnf(t33361,plain,
complement(X1) = meet(top,complement(X1)),
inference(step,[status(thm)],[t1287,t1596]) ).
cnf(t1600,plain,
complement(X1) = meet(top,complement(X1)),
inference(rw,[status(thm)],[t33361]) ).
cnf(t1601,plain,
meet(top,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t1600]) ).
cnf(t1612,plain,
complement(X1) = join(zero,complement(X1)),
inference(cp,[status(thm)],[t1611,t1601]) ).
cnf(t1642,plain,
join(zero,complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t1612]) ).
cnf(t204,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t42,t195]) ).
cnf(t208,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t204]) ).
cnf(t1650,plain,
complement(complement(X1)) = join(zero,meet(X1,X1)),
inference(cp,[status(thm)],[t1642,t208]) ).
cnf(t33383,plain,
complement(complement(X1)) = meet(top,X1),
inference(step,[status(thm)],[t178,t1642]) ).
cnf(t1654,plain,
complement(complement(X1)) = meet(top,X1),
inference(rw,[status(thm)],[t33383]) ).
cnf(t1655,plain,
complement(complement(X1)) = meet(top,X1),
inference(orient,[status(thm)],[t1654]) ).
cnf(t33387,plain,
meet(top,X1) = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t1650,t1655]) ).
cnf(t33388,plain,
meet(top,X1) = X1,
inference(step,[status(thm)],[t33387,t1596]) ).
cnf(t1693,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t33388]) ).
cnf(t1703,plain,
meet(X1,join(complement(top),complement(X2))) = complement(join(complement(X1),X2)),
inference(cp,[status(thm)],[t623,t1693]) ).
cnf(t33411,plain,
meet(X1,join(zero,complement(X2))) = complement(join(complement(X1),X2)),
inference(step,[status(thm)],[t1703,t65]) ).
cnf(t33412,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),X2)),
inference(step,[status(thm)],[t33411,t1642]) ).
cnf(t1771,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t33412]) ).
cnf(t33440,plain,
meet(join(complement(X1),complement(X2)),X3) = meet(X3,complement(meet(X1,X2))),
inference(step,[status(thm)],[t599,t1771]) ).
cnf(t2433,plain,
meet(join(complement(X1),complement(X2)),X3) = meet(X3,complement(meet(X1,X2))),
inference(orient,[status(thm)],[t33440]) ).
cnf(t1700,plain,
X1 = meet(X1,top),
inference(cp,[status(thm)],[t1693,t64]) ).
cnf(t1711,plain,
meet(X1,top) = X1,
inference(orient,[status(thm)],[t1700]) ).
cnf(t2435,plain,
meet(top,complement(meet(X1,X2))) = join(complement(X1),complement(X2)),
inference(cp,[status(thm)],[t2433,t1711]) ).
cnf(t33441,plain,
complement(meet(X1,X2)) = join(complement(X1),complement(X2)),
inference(step,[status(thm)],[t2435,t1601]) ).
cnf(t2450,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t33441]) ).
cnf(t2455,plain,
complement(meet(X1,join(complement(X2),X3))) = join(complement(X1),meet(X2,complement(X3))),
inference(cp,[status(thm)],[t2450,t1771]) ).
cnf(t11691,plain,
complement(meet(X1,join(complement(X2),X3))) = join(complement(X1),meet(X2,complement(X3))),
inference(orient,[status(thm)],[t2455]) ).
cnf(t1549,plain,
X1 = join(meet(X1,complement(X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t1537,t42]) ).
cnf(t33424,plain,
X1 = join(meet(X1,X2),meet(X1,complement(X2))),
inference(step,[status(thm)],[t1549,t22]) ).
cnf(t1874,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t33424]) ).
cnf(t223,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t217,t22]) ).
cnf(t280,plain,
join(X1,join(X2,complement(X1))) = join(top,X2),
inference(orient,[status(thm)],[t223]) ).
cnf(t2459,plain,
join(top,complement(X1)) = join(X2,complement(meet(X1,X2))),
inference(cp,[status(thm)],[t280,t2450]) ).
cnf(t33443,plain,
top = join(X2,complement(meet(X1,X2))),
inference(step,[status(thm)],[t2459,t234]) ).
cnf(t2463,plain,
join(X1,complement(meet(X2,X1))) = top,
inference(orient,[status(thm)],[t33443]) ).
cnf(t2468,plain,
meet(X1,complement(complement(meet(X2,complement(X1))))) = complement(top),
inference(cp,[status(thm)],[t1771,t2463]) ).
cnf(t33393,plain,
complement(complement(X1)) = X1,
inference(step,[status(thm)],[t1655,t1693]) ).
cnf(t1698,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t33393]) ).
cnf(t33446,plain,
meet(X1,meet(X2,complement(X1))) = complement(top),
inference(step,[status(thm)],[t2468,t1698]) ).
cnf(t33447,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(step,[status(thm)],[t33446,t65]) ).
cnf(t2504,plain,
meet(X1,meet(X2,complement(X1))) = zero,
inference(orient,[status(thm)],[t33447]) ).
cnf(t2511,plain,
X1 = join(zero,meet(X1,complement(meet(X2,complement(X1))))),
inference(cp,[status(thm)],[t1874,t2504]) ).
cnf(t33395,plain,
join(zero,X1) = X1,
inference(step,[status(thm)],[t1611,t1693]) ).
cnf(t1707,plain,
join(zero,X1) = X1,
inference(rw,[status(thm)],[t33395]) ).
cnf(t1737,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t1707]) ).
cnf(t33451,plain,
X1 = meet(X1,complement(meet(X2,complement(X1)))),
inference(step,[status(thm)],[t2511,t1737]) ).
cnf(t1799,plain,
join(complement(X1),X2) = complement(meet(X1,complement(X2))),
inference(cp,[status(thm)],[t1698,t1771]) ).
cnf(t1931,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(orient,[status(thm)],[t1799]) ).
cnf(t33452,plain,
X1 = meet(X1,join(complement(X2),X1)),
inference(step,[status(thm)],[t33451,t1931]) ).
cnf(t2574,plain,
meet(X1,join(complement(X2),X1)) = X1,
inference(orient,[status(thm)],[t33452]) ).
cnf(t2596,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t2574,t1698]) ).
cnf(t2600,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t2596]) ).
cnf(t11693,plain,
join(complement(X1),meet(X2,complement(X1))) = complement(X1),
inference(cp,[status(thm)],[t11691,t2600]) ).
cnf(t11842,plain,
join(complement(X1),meet(X2,complement(X1))) = complement(X1),
inference(orient,[status(thm)],[t11693]) ).
cnf(t11849,plain,
complement(complement(X1)) = join(X1,meet(X2,complement(complement(X1)))),
inference(cp,[status(thm)],[t11842,t1698]) ).
cnf(t33813,plain,
X1 = join(X1,meet(X2,complement(complement(X1)))),
inference(step,[status(thm)],[t11849,t1698]) ).
cnf(t33814,plain,
X1 = join(X1,meet(X2,X1)),
inference(step,[status(thm)],[t33813,t1698]) ).
cnf(t11875,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t33814]) ).
cnf(t34132,plain,
meet(X1,join(complement(X1),X2)) = complement(join(complement(X1),complement(X2))),
inference(step,[status(thm)],[t267,t11875]) ).
cnf(t34133,plain,
meet(X1,join(complement(X1),X2)) = meet(X1,X2),
inference(step,[status(thm)],[t34132,t42]) ).
cnf(t28277,plain,
meet(X1,join(complement(X1),X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t34133]) ).
cnf(t28346,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,join(complement(X1),X3))),
inference(cp,[status(thm)],[t28277,t151]) ).
cnf(t29966,plain,
meet(X1,join(X2,join(complement(X1),X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t28346]) ).
cnf(f6,axiom,
composition(join(A,B),C) = join(composition(A,C),composition(B,C)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_distributivity_7) ).
fof(f6_nnf,plain,
! [A,B,C] : composition(join(A,B),C) = join(composition(A,C),composition(B,C)),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [A,B,C] : composition(join(A,B),C) = join(composition(A,C),composition(B,C)),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t12,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t34,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t12]) ).
cnf(t146,plain,
composition(join(X1,one),X2) = join(composition(X1,X2),X2),
inference(cp,[status(thm)],[t34,t144]) ).
cnf(t33236,plain,
composition(join(X1,one),X2) = join(X2,composition(X1,X2)),
inference(step,[status(thm)],[t146,t22]) ).
cnf(t310,plain,
composition(join(X1,one),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t33236]) ).
cnf(f13,negated_conjecture,
join(sk1,one) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals_14) ).
fof(f13_nnf,plain,
join(sk1,one) = one,
inference(nnf_transformation,[status(thm)],[f13]) ).
cnf(c13,plain,
join(sk1,one) = one,
inference(cnf_transformation,[status(esa)],[f13_nnf]) ).
cnf(t2,plain,
join(sk1,one) = one,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t40,plain,
join(sk1,one) = one,
inference(orient,[status(thm)],[t2]) ).
cnf(t312,plain,
join(X1,composition(sk1,X1)) = composition(one,X1),
inference(cp,[status(thm)],[t310,t40]) ).
cnf(t33237,plain,
join(X1,composition(sk1,X1)) = X1,
inference(step,[status(thm)],[t312,t144]) ).
cnf(t323,plain,
join(X1,composition(sk1,X1)) = X1,
inference(orient,[status(thm)],[t33237]) ).
cnf(t30051,plain,
meet(X1,join(X2,composition(sk1,complement(X1)))) = meet(X1,join(X2,complement(X1))),
inference(cp,[status(thm)],[t29966,t323]) ).
cnf(t28334,plain,
meet(X1,X2) = meet(X1,join(X2,complement(X1))),
inference(cp,[status(thm)],[t28277,t22]) ).
cnf(t28393,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t28334]) ).
cnf(t34227,plain,
meet(X1,join(X2,composition(sk1,complement(X1)))) = meet(X1,X2),
inference(step,[status(thm)],[t30051,t28393]) ).
cnf(t32933,plain,
meet(X1,join(X2,composition(sk1,complement(X1)))) = meet(X1,X2),
inference(orient,[status(thm)],[t34227]) ).
cnf(f8,axiom,
converse(join(A,B)) = join(converse(A),converse(B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_additivity_9) ).
fof(f8_nnf,plain,
! [A,B] : converse(join(A,B)) = join(converse(A),converse(B)),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [A,B] : converse(join(A,B)) = join(converse(A),converse(B)),
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(t9,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t30,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t9]) ).
cnf(t31,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t30,t19]) ).
cnf(t81,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t31]) ).
cnf(t145,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(cp,[status(thm)],[t34,t144]) ).
cnf(t289,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t145]) ).
cnf(t309,plain,
join(X1,converse(composition(X2,converse(X1)))) = converse(composition(join(one,X2),converse(X1))),
inference(cp,[status(thm)],[t81,t289]) ).
cnf(t50,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t49,t19]) ).
cnf(t99,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t50]) ).
cnf(t33334,plain,
join(X1,composition(X1,converse(X2))) = converse(composition(join(one,X2),converse(X1))),
inference(step,[status(thm)],[t309,t99]) ).
cnf(t33335,plain,
join(X1,composition(X1,converse(X2))) = composition(X1,converse(join(one,X2))),
inference(step,[status(thm)],[t33334,t99]) ).
cnf(t136,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(cp,[status(thm)],[t30,t133]) ).
cnf(t153,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t136]) ).
cnf(t33336,plain,
join(X1,composition(X1,converse(X2))) = composition(X1,join(one,converse(X2))),
inference(step,[status(thm)],[t33335,t153]) ).
cnf(t1046,plain,
join(X1,composition(X1,converse(X2))) = composition(X1,join(one,converse(X2))),
inference(orient,[status(thm)],[t33336]) ).
cnf(t1065,plain,
composition(X1,join(one,converse(converse(X2)))) = join(X1,composition(X1,X2)),
inference(cp,[status(thm)],[t1046,t19]) ).
cnf(t33341,plain,
composition(X1,join(one,X2)) = join(X1,composition(X1,X2)),
inference(step,[status(thm)],[t1065,t19]) ).
cnf(t1122,plain,
composition(X1,join(one,X2)) = join(X1,composition(X1,X2)),
inference(orient,[status(thm)],[t33341]) ).
cnf(t296,plain,
join(X1,composition(complement(one),X1)) = composition(top,X1),
inference(cp,[status(thm)],[t289,t27]) ).
cnf(t379,plain,
join(X1,composition(complement(one),X1)) = composition(top,X1),
inference(orient,[status(thm)],[t296]) ).
cnf(t1131,plain,
join(X1,composition(X1,composition(complement(one),one))) = composition(X1,composition(top,one)),
inference(cp,[status(thm)],[t1122,t379]) ).
cnf(t33471,plain,
join(X1,composition(X1,complement(one))) = composition(X1,composition(top,one)),
inference(step,[status(thm)],[t1131,t20]) ).
cnf(t33472,plain,
join(X1,composition(X1,complement(one))) = composition(X1,top),
inference(step,[status(thm)],[t33471,t20]) ).
cnf(t2748,plain,
join(X1,composition(X1,complement(one))) = composition(X1,top),
inference(orient,[status(thm)],[t33472]) ).
cnf(t32936,plain,
meet(one,sk1) = meet(one,composition(sk1,top)),
inference(cp,[status(thm)],[t32933,t2748]) ).
cnf(t34228,plain,
meet(sk1,one) = meet(one,composition(sk1,top)),
inference(step,[status(thm)],[t32936,t64]) ).
cnf(t1704,plain,
meet(join(complement(top),complement(X1)),X2) = complement(join(X1,complement(X2))),
inference(cp,[status(thm)],[t597,t1693]) ).
cnf(t33427,plain,
meet(join(zero,complement(X1)),X2) = complement(join(X1,complement(X2))),
inference(step,[status(thm)],[t1704,t65]) ).
cnf(t33428,plain,
meet(complement(X1),X2) = complement(join(X1,complement(X2))),
inference(step,[status(thm)],[t33427,t1642]) ).
cnf(t1893,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t33428]) ).
cnf(t41,plain,
join(sk1,join(one,X1)) = join(one,X1),
inference(cp,[status(thm)],[t24,t40]) ).
cnf(t76,plain,
join(sk1,join(one,X1)) = join(one,X1),
inference(orient,[status(thm)],[t41]) ).
cnf(t78,plain,
join(one,X1) = join(sk1,join(X1,one)),
inference(cp,[status(thm)],[t76,t22]) ).
cnf(t194,plain,
join(sk1,join(X1,one)) = join(one,X1),
inference(orient,[status(thm)],[t78]) ).
cnf(t218,plain,
join(top,one) = join(one,complement(sk1)),
inference(cp,[status(thm)],[t217,t194]) ).
cnf(t242,plain,
join(one,complement(sk1)) = join(top,one),
inference(orient,[status(thm)],[t218]) ).
cnf(t244,plain,
join(one,complement(sk1)) = join(sk1,join(top,one)),
inference(cp,[status(thm)],[t76,t242]) ).
cnf(t33228,plain,
join(top,one) = join(sk1,join(top,one)),
inference(step,[status(thm)],[t244,t242]) ).
cnf(t33229,plain,
join(top,one) = join(one,top),
inference(step,[status(thm)],[t33228,t194]) ).
cnf(t222,plain,
join(top,complement(complement(X1))) = join(X1,top),
inference(cp,[status(thm)],[t217,t27]) ).
cnf(t33227,plain,
top = join(X1,top),
inference(step,[status(thm)],[t222,t234]) ).
cnf(t238,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t33227]) ).
cnf(t33230,plain,
join(top,one) = top,
inference(step,[status(thm)],[t33229,t238]) ).
cnf(t245,plain,
join(top,one) = top,
inference(orient,[status(thm)],[t33230]) ).
cnf(t33231,plain,
join(one,complement(sk1)) = top,
inference(step,[status(thm)],[t242,t245]) ).
cnf(t246,plain,
join(one,complement(sk1)) = top,
inference(orient,[status(thm)],[t33231]) ).
cnf(t1894,plain,
meet(complement(one),sk1) = complement(top),
inference(cp,[status(thm)],[t1893,t246]) ).
cnf(t33430,plain,
meet(sk1,complement(one)) = complement(top),
inference(step,[status(thm)],[t1894,t64]) ).
cnf(t33431,plain,
meet(sk1,complement(one)) = zero,
inference(step,[status(thm)],[t33430,t65]) ).
cnf(t1918,plain,
meet(sk1,complement(one)) = zero,
inference(orient,[status(thm)],[t33431]) ).
cnf(t1919,plain,
sk1 = join(zero,meet(sk1,complement(complement(one)))),
inference(cp,[status(thm)],[t1874,t1918]) ).
cnf(t33432,plain,
sk1 = meet(sk1,complement(complement(one))),
inference(step,[status(thm)],[t1919,t1737]) ).
cnf(t33433,plain,
sk1 = meet(sk1,one),
inference(step,[status(thm)],[t33432,t1698]) ).
cnf(t1921,plain,
meet(sk1,one) = sk1,
inference(orient,[status(thm)],[t33433]) ).
cnf(t34229,plain,
sk1 = meet(one,composition(sk1,top)),
inference(step,[status(thm)],[t34228,t1921]) ).
cnf(t2456,plain,
complement(meet(X1,join(X2,complement(X3)))) = join(complement(X1),meet(complement(X2),X3)),
inference(cp,[status(thm)],[t2450,t1893]) ).
cnf(t3244,plain,
complement(meet(X1,join(X2,complement(X3)))) = join(complement(X1),meet(complement(X2),X3)),
inference(orient,[status(thm)],[t2456]) ).
cnf(t45,plain,
top = join(join(complement(X1),complement(X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t27,t42]) ).
cnf(t33350,plain,
top = join(complement(X1),join(complement(X2),meet(X1,X2))),
inference(step,[status(thm)],[t45,t24]) ).
cnf(t1335,plain,
join(complement(X1),join(complement(X2),meet(X1,X2))) = top,
inference(orient,[status(thm)],[t33350]) ).
cnf(t1551,plain,
X1 = join(meet(X1,join(complement(X2),meet(X1,X2))),complement(top)),
inference(cp,[status(thm)],[t1537,t1335]) ).
cnf(t33737,plain,
X1 = join(complement(top),meet(X1,join(complement(X2),meet(X1,X2)))),
inference(step,[status(thm)],[t1551,t22]) ).
cnf(t33738,plain,
X1 = join(zero,meet(X1,join(complement(X2),meet(X1,X2)))),
inference(step,[status(thm)],[t33737,t65]) ).
cnf(t33739,plain,
X1 = meet(X1,join(complement(X2),meet(X1,X2))),
inference(step,[status(thm)],[t33738,t1737]) ).
cnf(t8744,plain,
meet(X1,join(complement(X2),meet(X1,X2))) = X1,
inference(orient,[status(thm)],[t33739]) ).
cnf(t1797,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(cp,[status(thm)],[t1771,t1698]) ).
cnf(t1923,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t1797]) ).
cnf(t8755,plain,
complement(X1) = meet(complement(X1),join(complement(complement(X2)),complement(join(X1,X2)))),
inference(cp,[status(thm)],[t8744,t1923]) ).
cnf(t33742,plain,
complement(X1) = meet(complement(X1),complement(meet(complement(X2),join(X1,X2)))),
inference(step,[status(thm)],[t8755,t2450]) ).
cnf(t1899,plain,
join(X1,complement(X2)) = complement(meet(complement(X1),X2)),
inference(cp,[status(thm)],[t1698,t1893]) ).
cnf(t3153,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t1899]) ).
cnf(t33743,plain,
complement(X1) = meet(complement(X1),join(X2,complement(join(X1,X2)))),
inference(step,[status(thm)],[t33742,t3153]) ).
cnf(t8797,plain,
meet(complement(X1),join(X2,complement(join(X1,X2)))) = complement(X1),
inference(orient,[status(thm)],[t33743]) ).
cnf(t8897,plain,
join(complement(complement(X1)),meet(complement(X2),join(X1,X2))) = complement(complement(X1)),
inference(cp,[status(thm)],[t3244,t8797]) ).
cnf(t33757,plain,
join(X1,meet(complement(X2),join(X1,X2))) = complement(complement(X1)),
inference(step,[status(thm)],[t8897,t1698]) ).
cnf(t33758,plain,
join(X1,meet(complement(X2),join(X1,X2))) = X1,
inference(step,[status(thm)],[t33757,t1698]) ).
cnf(t9002,plain,
join(X1,meet(complement(X2),join(X1,X2))) = X1,
inference(orient,[status(thm)],[t33758]) ).
cnf(t82,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t81,t27]) ).
cnf(t268,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t82]) ).
cnf(t25,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t24,t22]) ).
cnf(t148,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t25]) ).
cnf(t77,plain,
join(one,complement(one)) = join(sk1,top),
inference(cp,[status(thm)],[t76,t27]) ).
cnf(t33213,plain,
top = join(sk1,top),
inference(step,[status(thm)],[t77,t27]) ).
cnf(t33214,plain,
top = join(top,sk1),
inference(step,[status(thm)],[t33213,t22]) ).
cnf(t79,plain,
join(top,sk1) = top,
inference(orient,[status(thm)],[t33214]) ).
cnf(t80,plain,
join(top,join(sk1,X1)) = join(top,X1),
inference(cp,[status(thm)],[t24,t79]) ).
cnf(t250,plain,
join(top,join(sk1,X1)) = join(top,X1),
inference(orient,[status(thm)],[t80]) ).
cnf(t277,plain,
join(top,converse(complement(converse(sk1)))) = join(top,converse(top)),
inference(cp,[status(thm)],[t250,t268]) ).
cnf(t240,plain,
join(X1,converse(top)) = converse(top),
inference(cp,[status(thm)],[t81,t238]) ).
cnf(t241,plain,
join(X1,converse(top)) = converse(top),
inference(orient,[status(thm)],[t240]) ).
cnf(t33250,plain,
join(top,converse(complement(converse(sk1)))) = converse(top),
inference(step,[status(thm)],[t277,t241]) ).
cnf(t429,plain,
join(top,converse(complement(converse(sk1)))) = converse(top),
inference(orient,[status(thm)],[t33250]) ).
cnf(t432,plain,
join(converse(complement(converse(sk1))),join(X1,top)) = join(X1,converse(top)),
inference(cp,[status(thm)],[t148,t429]) ).
cnf(t33251,plain,
join(converse(complement(converse(sk1))),top) = join(X1,converse(top)),
inference(step,[status(thm)],[t432,t238]) ).
cnf(t33252,plain,
top = join(X1,converse(top)),
inference(step,[status(thm)],[t33251,t238]) ).
cnf(t33253,plain,
top = converse(top),
inference(step,[status(thm)],[t33252,t241]) ).
cnf(t433,plain,
converse(top) = top,
inference(orient,[status(thm)],[t33253]) ).
cnf(t33254,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(step,[status(thm)],[t268,t433]) ).
cnf(t434,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(orient,[status(thm)],[t33254]) ).
cnf(t9039,plain,
X1 = join(X1,meet(complement(converse(complement(converse(X1)))),top)),
inference(cp,[status(thm)],[t9002,t434]) ).
cnf(t33764,plain,
X1 = join(X1,complement(converse(complement(converse(X1))))),
inference(step,[status(thm)],[t9039,t1711]) ).
cnf(t9255,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(orient,[status(thm)],[t33764]) ).
cnf(t9283,plain,
complement(converse(complement(converse(X1)))) = meet(complement(converse(complement(converse(X1)))),X1),
inference(cp,[status(thm)],[t2600,t9255]) ).
cnf(t34062,plain,
complement(converse(complement(converse(X1)))) = meet(X1,complement(converse(complement(converse(X1))))),
inference(step,[status(thm)],[t9283,t64]) ).
cnf(t9302,plain,
join(X1,converse(complement(converse(complement(converse(converse(X1))))))) = converse(converse(X1)),
inference(cp,[status(thm)],[t81,t9255]) ).
cnf(t33772,plain,
join(X1,converse(complement(converse(complement(X1))))) = converse(converse(X1)),
inference(step,[status(thm)],[t9302,t19]) ).
cnf(t33773,plain,
join(X1,converse(complement(converse(complement(X1))))) = X1,
inference(step,[status(thm)],[t33772,t19]) ).
cnf(t9449,plain,
join(X1,converse(complement(converse(complement(X1))))) = X1,
inference(orient,[status(thm)],[t33773]) ).
cnf(t9479,plain,
meet(X1,complement(converse(complement(converse(complement(complement(X1))))))) = complement(complement(X1)),
inference(cp,[status(thm)],[t1771,t9449]) ).
cnf(t33785,plain,
meet(X1,complement(converse(complement(converse(X1))))) = complement(complement(X1)),
inference(step,[status(thm)],[t9479,t1698]) ).
cnf(t33786,plain,
meet(X1,complement(converse(complement(converse(X1))))) = X1,
inference(step,[status(thm)],[t33785,t1698]) ).
cnf(t9859,plain,
meet(X1,complement(converse(complement(converse(X1))))) = X1,
inference(orient,[status(thm)],[t33786]) ).
cnf(t34063,plain,
complement(converse(complement(converse(X1)))) = X1,
inference(step,[status(thm)],[t34062,t9859]) ).
cnf(t21641,plain,
complement(converse(complement(converse(X1)))) = X1,
inference(orient,[status(thm)],[t34063]) ).
cnf(t21672,plain,
converse(X1) = complement(converse(complement(X1))),
inference(cp,[status(thm)],[t21641,t19]) ).
cnf(t21749,plain,
complement(converse(complement(X1))) = converse(X1),
inference(orient,[status(thm)],[t21672]) ).
cnf(t21793,plain,
join(complement(X1),converse(complement(X2))) = complement(meet(X1,converse(X2))),
inference(cp,[status(thm)],[t1931,t21749]) ).
cnf(t22173,plain,
join(complement(X1),converse(complement(X2))) = complement(meet(X1,converse(X2))),
inference(orient,[status(thm)],[t21793]) ).
cnf(t21756,plain,
converse(complement(X1)) = complement(converse(X1)),
inference(cp,[status(thm)],[t21749,t1698]) ).
cnf(t21838,plain,
complement(converse(X1)) = converse(complement(X1)),
inference(orient,[status(thm)],[t21756]) ).
cnf(t22176,plain,
complement(meet(converse(X1),converse(X2))) = join(converse(complement(X1)),converse(complement(X2))),
inference(cp,[status(thm)],[t22173,t21838]) ).
cnf(t34097,plain,
complement(meet(converse(X1),converse(X2))) = converse(join(complement(X1),complement(X2))),
inference(step,[status(thm)],[t22176,t30]) ).
cnf(t34098,plain,
complement(meet(converse(X1),converse(X2))) = converse(complement(meet(X1,X2))),
inference(step,[status(thm)],[t34097,t2450]) ).
cnf(t23148,plain,
complement(meet(converse(X1),converse(X2))) = converse(complement(meet(X1,X2))),
inference(orient,[status(thm)],[t34098]) ).
cnf(t23231,plain,
meet(converse(X1),converse(X2)) = complement(converse(complement(meet(X1,X2)))),
inference(cp,[status(thm)],[t1698,t23148]) ).
cnf(t34099,plain,
meet(converse(X1),converse(X2)) = converse(meet(X1,X2)),
inference(step,[status(thm)],[t23231,t21749]) ).
cnf(t23313,plain,
meet(converse(X1),converse(X2)) = converse(meet(X1,X2)),
inference(orient,[status(thm)],[t34099]) ).
cnf(t23383,plain,
converse(meet(X1,composition(X2,converse(X3)))) = meet(converse(X1),composition(X3,converse(X2))),
inference(cp,[status(thm)],[t23313,t99]) ).
cnf(t26879,plain,
converse(meet(X1,composition(X2,converse(X3)))) = meet(converse(X1),composition(X3,converse(X2))),
inference(orient,[status(thm)],[t23383]) ).
cnf(t442,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(cp,[status(thm)],[t49,t433]) ).
cnf(t455,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(orient,[status(thm)],[t442]) ).
cnf(t52,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t34,t49]) ).
cnf(t7085,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t52]) ).
cnf(t7116,plain,
composition(join(converse(X1),converse(X2)),converse(X3)) = join(converse(composition(X3,X1)),converse(composition(X3,X2))),
inference(cp,[status(thm)],[t7085,t49]) ).
cnf(t33692,plain,
composition(converse(join(X1,X2)),converse(X3)) = join(converse(composition(X3,X1)),converse(composition(X3,X2))),
inference(step,[status(thm)],[t7116,t30]) ).
cnf(t33693,plain,
converse(composition(X3,join(X1,X2))) = join(converse(composition(X3,X1)),converse(composition(X3,X2))),
inference(step,[status(thm)],[t33692,t49]) ).
cnf(t33694,plain,
converse(composition(X3,join(X1,X2))) = converse(join(composition(X3,X1),composition(X3,X2))),
inference(step,[status(thm)],[t33693,t30]) ).
cnf(t7157,plain,
converse(join(composition(X1,X2),composition(X1,X3))) = converse(composition(X1,join(X2,X3))),
inference(orient,[status(thm)],[t33694]) ).
cnf(t7213,plain,
join(composition(X1,X2),composition(X1,X3)) = converse(converse(composition(X1,join(X2,X3)))),
inference(cp,[status(thm)],[t19,t7157]) ).
cnf(t33695,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(step,[status(thm)],[t7213,t19]) ).
cnf(t7278,plain,
join(composition(X1,X2),composition(X1,X3)) = composition(X1,join(X2,X3)),
inference(orient,[status(thm)],[t33695]) ).
cnf(t37,plain,
complement(X1) = join(complement(X1),composition(X2,complement(composition(converse(X2),X1)))),
inference(cp,[status(thm)],[t36,t19]) ).
cnf(t3308,plain,
join(complement(X1),composition(X2,complement(composition(converse(X2),X1)))) = complement(X1),
inference(orient,[status(thm)],[t37]) ).
cnf(t3318,plain,
complement(top) = join(zero,composition(X1,complement(composition(converse(X1),top)))),
inference(cp,[status(thm)],[t3308,t65]) ).
cnf(t33514,plain,
zero = join(zero,composition(X1,complement(composition(converse(X1),top)))),
inference(step,[status(thm)],[t3318,t65]) ).
cnf(t33515,plain,
zero = composition(X1,complement(composition(converse(X1),top))),
inference(step,[status(thm)],[t33514,t1737]) ).
cnf(t3353,plain,
composition(X1,complement(composition(converse(X1),top))) = zero,
inference(orient,[status(thm)],[t33515]) ).
cnf(t7295,plain,
composition(X1,join(complement(composition(converse(X1),top)),X2)) = join(zero,composition(X1,X2)),
inference(cp,[status(thm)],[t7278,t3353]) ).
cnf(t33853,plain,
composition(X1,join(complement(composition(converse(X1),top)),X2)) = composition(X1,X2),
inference(step,[status(thm)],[t7295,t1737]) ).
cnf(t12824,plain,
composition(X1,join(complement(composition(converse(X1),top)),X2)) = composition(X1,X2),
inference(orient,[status(thm)],[t33853]) ).
cnf(t1059,plain,
composition(X1,join(one,converse(top))) = join(X1,composition(X1,top)),
inference(cp,[status(thm)],[t1046,t433]) ).
cnf(t33337,plain,
composition(X1,converse(top)) = join(X1,composition(X1,top)),
inference(step,[status(thm)],[t1059,t241]) ).
cnf(t33338,plain,
composition(X1,top) = join(X1,composition(X1,top)),
inference(step,[status(thm)],[t33337,t433]) ).
cnf(t1106,plain,
join(X1,composition(X1,top)) = composition(X1,top),
inference(orient,[status(thm)],[t33338]) ).
cnf(t1110,plain,
join(top,composition(complement(X1),top)) = join(X1,composition(complement(X1),top)),
inference(cp,[status(thm)],[t217,t1106]) ).
cnf(t444,plain,
converse(join(top,X1)) = join(top,converse(X1)),
inference(cp,[status(thm)],[t30,t433]) ).
cnf(t485,plain,
converse(join(top,X1)) = join(top,converse(X1)),
inference(orient,[status(thm)],[t444]) ).
cnf(t494,plain,
join(top,converse(X1)) = converse(join(X1,top)),
inference(cp,[status(thm)],[t485,t22]) ).
cnf(t33263,plain,
join(top,converse(X1)) = converse(top),
inference(step,[status(thm)],[t494,t238]) ).
cnf(t33264,plain,
join(top,converse(X1)) = top,
inference(step,[status(thm)],[t33263,t433]) ).
cnf(t509,plain,
join(top,converse(X1)) = top,
inference(orient,[status(thm)],[t33264]) ).
cnf(t33265,plain,
converse(join(top,X1)) = top,
inference(step,[status(thm)],[t485,t509]) ).
cnf(t510,plain,
converse(join(top,X1)) = top,
inference(orient,[status(thm)],[t33265]) ).
cnf(t292,plain,
join(X1,composition(complement(sk1),X1)) = composition(top,X1),
inference(cp,[status(thm)],[t289,t246]) ).
cnf(t702,plain,
join(X1,composition(complement(sk1),X1)) = composition(top,X1),
inference(orient,[status(thm)],[t292]) ).
cnf(t704,plain,
top = converse(composition(top,top)),
inference(cp,[status(thm)],[t510,t702]) ).
cnf(t443,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(cp,[status(thm)],[t49,t433]) ).
cnf(t473,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(orient,[status(thm)],[t443]) ).
cnf(t33284,plain,
top = composition(converse(top),top),
inference(step,[status(thm)],[t704,t473]) ).
cnf(t33285,plain,
top = composition(top,top),
inference(step,[status(thm)],[t33284,t433]) ).
cnf(t711,plain,
composition(top,top) = top,
inference(orient,[status(thm)],[t33285]) ).
cnf(t713,plain,
composition(join(top,X1),top) = join(top,composition(X1,top)),
inference(cp,[status(thm)],[t34,t711]) ).
cnf(t1017,plain,
composition(join(top,X1),top) = join(top,composition(X1,top)),
inference(orient,[status(thm)],[t713]) ).
cnf(t1033,plain,
join(top,composition(X1,top)) = composition(join(X1,top),top),
inference(cp,[status(thm)],[t1017,t22]) ).
cnf(t33328,plain,
join(top,composition(X1,top)) = composition(top,top),
inference(step,[status(thm)],[t1033,t238]) ).
cnf(t33329,plain,
join(top,composition(X1,top)) = top,
inference(step,[status(thm)],[t33328,t711]) ).
cnf(t1041,plain,
join(top,composition(X1,top)) = top,
inference(orient,[status(thm)],[t33329]) ).
cnf(t33344,plain,
top = join(X1,composition(complement(X1),top)),
inference(step,[status(thm)],[t1110,t1041]) ).
cnf(t1210,plain,
join(X1,composition(complement(X1),top)) = top,
inference(orient,[status(thm)],[t33344]) ).
cnf(t1776,plain,
meet(X1,complement(composition(complement(complement(X1)),top))) = complement(top),
inference(cp,[status(thm)],[t1771,t1210]) ).
cnf(t33484,plain,
meet(X1,complement(composition(X1,top))) = complement(top),
inference(step,[status(thm)],[t1776,t1698]) ).
cnf(t33485,plain,
meet(X1,complement(composition(X1,top))) = zero,
inference(step,[status(thm)],[t33484,t65]) ).
cnf(t2832,plain,
meet(X1,complement(composition(X1,top))) = zero,
inference(orient,[status(thm)],[t33485]) ).
cnf(t2835,plain,
join(complement(X1),composition(X1,top)) = complement(zero),
inference(cp,[status(thm)],[t1931,t2832]) ).
cnf(t1615,plain,
complement(complement(top)) = join(zero,meet(top,top)),
inference(cp,[status(thm)],[t1611,t534]) ).
cnf(t33366,plain,
meet(top,top) = join(zero,meet(top,top)),
inference(step,[status(thm)],[t1615,t208]) ).
cnf(t180,plain,
meet(top,top) = complement(join(zero,zero)),
inference(cp,[status(thm)],[t178,t65]) ).
cnf(t187,plain,
complement(join(zero,zero)) = meet(top,top),
inference(orient,[status(thm)],[t180]) ).
cnf(t199,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t195,t65]) ).
cnf(t33223,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t199,t65]) ).
cnf(t33224,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t33223,t65]) ).
cnf(t205,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t33224]) ).
cnf(t33225,plain,
complement(zero) = meet(top,top),
inference(step,[status(thm)],[t187,t205]) ).
cnf(t206,plain,
complement(zero) = meet(top,top),
inference(rw,[status(thm)],[t33225]) ).
cnf(t207,plain,
meet(top,top) = complement(zero),
inference(orient,[status(thm)],[t206]) ).
cnf(t33367,plain,
complement(zero) = join(zero,meet(top,top)),
inference(step,[status(thm)],[t33366,t207]) ).
cnf(t33368,plain,
complement(zero) = top,
inference(step,[status(thm)],[t33367,t1611]) ).
cnf(t1619,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t33368]) ).
cnf(t33539,plain,
join(complement(X1),composition(X1,top)) = top,
inference(step,[status(thm)],[t2835,t1619]) ).
cnf(t3823,plain,
join(complement(X1),composition(X1,top)) = top,
inference(orient,[status(thm)],[t33539]) ).
cnf(t12832,plain,
composition(X1,composition(composition(converse(X1),top),top)) = composition(X1,top),
inference(cp,[status(thm)],[t12824,t3823]) ).
cnf(t33854,plain,
composition(X1,composition(converse(X1),composition(top,top))) = composition(X1,top),
inference(step,[status(thm)],[t12832,t55]) ).
cnf(t33855,plain,
composition(X1,composition(converse(X1),top)) = composition(X1,top),
inference(step,[status(thm)],[t33854,t711]) ).
cnf(t12992,plain,
composition(X1,composition(converse(X1),top)) = composition(X1,top),
inference(orient,[status(thm)],[t33855]) ).
cnf(t13027,plain,
composition(converse(sk1),top) = join(composition(converse(sk1),top),composition(sk1,top)),
inference(cp,[status(thm)],[t323,t12992]) ).
cnf(t33872,plain,
composition(converse(sk1),top) = composition(join(converse(sk1),sk1),top),
inference(step,[status(thm)],[t13027,t34]) ).
cnf(t33873,plain,
composition(converse(sk1),top) = composition(join(sk1,converse(sk1)),top),
inference(step,[status(thm)],[t33872,t22]) ).
cnf(t137,plain,
converse(join(X1,one)) = join(converse(X1),one),
inference(cp,[status(thm)],[t30,t133]) ).
cnf(t33219,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(step,[status(thm)],[t137,t22]) ).
cnf(t166,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t33219]) ).
cnf(t167,plain,
join(one,converse(sk1)) = converse(one),
inference(cp,[status(thm)],[t166,t40]) ).
cnf(t33220,plain,
join(one,converse(sk1)) = one,
inference(step,[status(thm)],[t167,t133]) ).
cnf(t177,plain,
join(one,converse(sk1)) = one,
inference(orient,[status(thm)],[t33220]) ).
cnf(t290,plain,
join(X1,composition(converse(sk1),X1)) = composition(one,X1),
inference(cp,[status(thm)],[t289,t177]) ).
cnf(t33244,plain,
join(X1,composition(converse(sk1),X1)) = X1,
inference(step,[status(thm)],[t290,t144]) ).
cnf(t365,plain,
join(X1,composition(converse(sk1),X1)) = X1,
inference(orient,[status(thm)],[t33244]) ).
cnf(t13060,plain,
composition(converse(converse(sk1)),top) = join(composition(converse(converse(sk1)),top),composition(converse(sk1),top)),
inference(cp,[status(thm)],[t365,t12992]) ).
cnf(t33864,plain,
composition(sk1,top) = join(composition(converse(converse(sk1)),top),composition(converse(sk1),top)),
inference(step,[status(thm)],[t13060,t19]) ).
cnf(t33865,plain,
composition(sk1,top) = composition(join(converse(converse(sk1)),converse(sk1)),top),
inference(step,[status(thm)],[t33864,t34]) ).
cnf(t33866,plain,
composition(sk1,top) = composition(converse(join(converse(sk1),sk1)),top),
inference(step,[status(thm)],[t33865,t30]) ).
cnf(t33867,plain,
composition(sk1,top) = composition(join(sk1,converse(sk1)),top),
inference(step,[status(thm)],[t33866,t81]) ).
cnf(t13289,plain,
composition(join(sk1,converse(sk1)),top) = composition(sk1,top),
inference(orient,[status(thm)],[t33867]) ).
cnf(t33874,plain,
composition(converse(sk1),top) = composition(sk1,top),
inference(step,[status(thm)],[t33873,t13289]) ).
cnf(t13392,plain,
composition(converse(sk1),top) = composition(sk1,top),
inference(orient,[status(thm)],[t33874]) ).
cnf(t13401,plain,
composition(top,converse(converse(sk1))) = converse(composition(sk1,top)),
inference(cp,[status(thm)],[t455,t13392]) ).
cnf(t33875,plain,
composition(top,sk1) = converse(composition(sk1,top)),
inference(step,[status(thm)],[t13401,t19]) ).
cnf(t33876,plain,
composition(top,sk1) = composition(top,converse(sk1)),
inference(step,[status(thm)],[t33875,t455]) ).
cnf(t13439,plain,
composition(top,converse(sk1)) = composition(top,sk1),
inference(orient,[status(thm)],[t33876]) ).
cnf(t26889,plain,
meet(converse(X1),composition(sk1,converse(top))) = converse(meet(X1,composition(top,sk1))),
inference(cp,[status(thm)],[t26879,t13439]) ).
cnf(t34119,plain,
meet(converse(X1),composition(sk1,top)) = converse(meet(X1,composition(top,sk1))),
inference(step,[status(thm)],[t26889,t433]) ).
cnf(t27042,plain,
converse(meet(X1,composition(top,sk1))) = meet(converse(X1),composition(sk1,top)),
inference(orient,[status(thm)],[t34119]) ).
cnf(t370,plain,
join(X1,converse(composition(converse(sk1),converse(X1)))) = converse(converse(X1)),
inference(cp,[status(thm)],[t81,t365]) ).
cnf(t33245,plain,
join(X1,composition(converse(converse(X1)),sk1)) = converse(converse(X1)),
inference(step,[status(thm)],[t370,t111]) ).
cnf(t33246,plain,
join(X1,composition(X1,sk1)) = converse(converse(X1)),
inference(step,[status(thm)],[t33245,t19]) ).
cnf(t33247,plain,
join(X1,composition(X1,sk1)) = X1,
inference(step,[status(thm)],[t33246,t19]) ).
cnf(t372,plain,
join(X1,composition(X1,sk1)) = X1,
inference(orient,[status(thm)],[t33247]) ).
cnf(t30046,plain,
meet(X1,join(X2,composition(complement(X1),sk1))) = meet(X1,join(X2,complement(X1))),
inference(cp,[status(thm)],[t29966,t372]) ).
cnf(t34222,plain,
meet(X1,join(X2,composition(complement(X1),sk1))) = meet(X1,X2),
inference(step,[status(thm)],[t30046,t28393]) ).
cnf(t32777,plain,
meet(X1,join(X2,composition(complement(X1),sk1))) = meet(X1,X2),
inference(orient,[status(thm)],[t34222]) ).
cnf(t32780,plain,
meet(one,sk1) = meet(one,composition(top,sk1)),
inference(cp,[status(thm)],[t32777,t379]) ).
cnf(t34223,plain,
meet(sk1,one) = meet(one,composition(top,sk1)),
inference(step,[status(thm)],[t32780,t64]) ).
cnf(t34224,plain,
sk1 = meet(one,composition(top,sk1)),
inference(step,[status(thm)],[t34223,t1921]) ).
cnf(t32843,plain,
meet(one,composition(top,sk1)) = sk1,
inference(orient,[status(thm)],[t34224]) ).
cnf(t32856,plain,
meet(converse(one),composition(sk1,top)) = converse(sk1),
inference(cp,[status(thm)],[t27042,t32843]) ).
cnf(t34225,plain,
meet(one,composition(sk1,top)) = converse(sk1),
inference(step,[status(thm)],[t32856,t133]) ).
cnf(t32861,plain,
meet(one,composition(sk1,top)) = converse(sk1),
inference(orient,[status(thm)],[t34225]) ).
cnf(t34230,plain,
sk1 = converse(sk1),
inference(step,[status(thm)],[t34229,t32861]) ).
cnf(t32999,plain,
converse(sk1) = sk1,
inference(orient,[status(thm)],[t34230]) ).
cnf(t34246,plain,
ifeq(join(sk1,sk1),converse(sk1),ifeq(join(sk1,converse(sk1)),sk1,false,true),true) = true,
inference(step,[status(thm)],[t61,t32999]) ).
cnf(t196,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t195,t42]) ).
cnf(t33332,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t196,t42]) ).
cnf(t33333,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t33332,t42]) ).
cnf(t1045,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t33333]) ).
cnf(t1701,plain,
meet(top,X1) = join(X1,meet(top,X1)),
inference(cp,[status(thm)],[t1045,t1693]) ).
cnf(t33401,plain,
X1 = join(X1,meet(top,X1)),
inference(step,[status(thm)],[t1701,t1693]) ).
cnf(t33402,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t33401,t1693]) ).
cnf(t1719,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t33402]) ).
cnf(t34247,plain,
ifeq(sk1,converse(sk1),ifeq(join(sk1,converse(sk1)),sk1,false,true),true) = true,
inference(step,[status(thm)],[t34246,t1719]) ).
cnf(t34248,plain,
ifeq(sk1,sk1,ifeq(join(sk1,converse(sk1)),sk1,false,true),true) = true,
inference(step,[status(thm)],[t34247,t32999]) ).
cnf(t5,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t21,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t5]) ).
cnf(t34249,plain,
ifeq(join(sk1,converse(sk1)),sk1,false,true) = true,
inference(step,[status(thm)],[t34248,t21]) ).
cnf(t34250,plain,
ifeq(join(sk1,sk1),sk1,false,true) = true,
inference(step,[status(thm)],[t34249,t32999]) ).
cnf(t34251,plain,
ifeq(sk1,sk1,false,true) = true,
inference(step,[status(thm)],[t34250,t1719]) ).
cnf(t34252,plain,
false = true,
inference(step,[status(thm)],[t34251,t21]) ).
cnf(t33085,plain,
false = true,
inference(rw,[status(thm)],[t34252]) ).
cnf(t33206,plain,
false = true,
inference(orient,[status(thm)],[t33085]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t33206]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL025-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n010.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 07:20:20 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 57.21/7.65 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 57.21/7.65 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------