%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL019+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 : n003.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:46 PM UTC 2026
% Result : Theorem 41.16s 5.69s
% Output : Proof 41.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 82
% Number of leaves : 13
% Syntax : Number of formulae : 292 ( 288 unt; 0 def)
% Number of atoms : 300 ( 299 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 16 ( 8 ~; 0 |; 6 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 6 ( 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 : 454 ( 66 sgn 70 !; 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(t7,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t62,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t7]) ).
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(t6,plain,
join(X1,X2) = join(X2,X1),
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t20,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t64,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t62,t20]) ).
cnf(t76494,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t64,t62]) ).
cnf(t80,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t76494]) ).
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(t13,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t76491,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t13,t20]) ).
cnf(t31,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t76491]) ).
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(t8,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t45,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t8]) ).
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(t3,plain,
converse(converse(X1)) = X1,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t19,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t47,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t45,t19]) ).
cnf(t147,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t47]) ).
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(t18,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t148,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t147,t18]) ).
cnf(t76496,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t148,t19]) ).
cnf(t162,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t76496]) ).
cnf(t163,plain,
one = converse(one),
inference(cp,[status(thm)],[t162,t18]) ).
cnf(t169,plain,
converse(one) = one,
inference(orient,[status(thm)],[t163]) ).
cnf(t76497,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t162,t169]) ).
cnf(t179,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t76497]) ).
cnf(t180,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t179]) ).
cnf(t183,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t31,t180]) ).
cnf(t76499,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t183,t169]) ).
cnf(t76500,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t76499,t180]) ).
cnf(t207,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t76500]) ).
cnf(t217,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t62,t207]) ).
cnf(t224,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t217]) ).
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(t14,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t15,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t14]) ).
cnf(t21,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t15]) ).
cnf(t76508,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t21,t20]) ).
cnf(t76509,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t76508,t62]) ).
cnf(t76510,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t76509,t20]) ).
cnf(t288,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t76510]) ).
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(t5,plain,
meet(X1,complement(X1)) = zero,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t69,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t5]) ).
cnf(t289,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t288,t69]) ).
cnf(t76511,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t289,t62]) ).
cnf(t307,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t76511]) ).
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(t11,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t22,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
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(t4,plain,
join(X1,complement(X1)) = top,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t25,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t4]) ).
cnf(t63,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t62,t25]) ).
cnf(t76492,plain,
zero = complement(top),
inference(step,[status(thm)],[t63,t69]) ).
cnf(t71,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t76492]) ).
cnf(t211,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t207,t71]) ).
cnf(t76501,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t211,t71]) ).
cnf(t76502,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t76501,t71]) ).
cnf(t218,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t76502]) ).
cnf(t219,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t22,t218]) ).
cnf(t234,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t219]) ).
cnf(t309,plain,
join(zero,meet(X1,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t234,t307]) ).
cnf(t76512,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t309,t307]) ).
cnf(t311,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t76512]) ).
cnf(t76513,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t307,t311]) ).
cnf(t318,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t76513]) ).
cnf(t340,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t318]) ).
cnf(t76520,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t224,t340]) ).
cnf(t342,plain,
X1 = complement(complement(X1)),
inference(rw,[status(thm)],[t76520]) ).
cnf(t347,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t342]) ).
cnf(t348,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(cp,[status(thm)],[t347,t62]) ).
cnf(t571,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t348]) ).
cnf(t574,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(cp,[status(thm)],[t571,t347]) ).
cnf(t589,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(orient,[status(thm)],[t574]) ).
cnf(t595,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),X2)),
inference(cp,[status(thm)],[t347,t589]) ).
cnf(t620,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t595]) ).
cnf(t349,plain,
complement(complement(X1)) = join(X1,complement(complement(X1))),
inference(cp,[status(thm)],[t207,t347]) ).
cnf(t76525,plain,
X1 = join(X1,complement(complement(X1))),
inference(step,[status(thm)],[t349,t347]) ).
cnf(t76526,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t76525,t347]) ).
cnf(t357,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t76526]) ).
cnf(t359,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t22,t357]) ).
cnf(t453,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t359]) ).
cnf(t457,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t453,t288]) ).
cnf(t76543,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t457,t288]) ).
cnf(t76544,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t76543,t20]) ).
cnf(t494,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t76544]) ).
cnf(t496,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t494,t80]) ).
cnf(t503,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t496]) ).
cnf(t508,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t22,t503]) ).
cnf(t1949,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t508]) ).
cnf(t76547,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t288,t620]) ).
cnf(t641,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(rw,[status(thm)],[t76547]) ).
cnf(t3986,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t641]) ).
cnf(t4049,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(cp,[status(thm)],[t1949,t3986]) ).
cnf(t4058,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t4049]) ).
cnf(t573,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(cp,[status(thm)],[t571,t347]) ).
cnf(t579,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t573]) ).
cnf(t583,plain,
meet(complement(X1),X2) = complement(join(X1,complement(X2))),
inference(cp,[status(thm)],[t347,t579]) ).
cnf(t602,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t583]) ).
cnf(t609,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(cp,[status(thm)],[t602,t347]) ).
cnf(t933,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t609]) ).
cnf(t4065,plain,
join(X1,complement(X2)) = join(X1,complement(join(X2,X1))),
inference(cp,[status(thm)],[t4058,t933]) ).
cnf(t4595,plain,
join(X1,complement(join(X2,X1))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t4065]) ).
cnf(t4665,plain,
meet(X1,complement(complement(join(X2,complement(X1))))) = complement(join(complement(X1),complement(X2))),
inference(cp,[status(thm)],[t620,t4595]) ).
cnf(t76655,plain,
meet(X1,join(X2,complement(X1))) = complement(join(complement(X1),complement(X2))),
inference(step,[status(thm)],[t4665,t347]) ).
cnf(t76656,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(step,[status(thm)],[t76655,t62]) ).
cnf(t4671,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t76656]) ).
cnf(t4691,plain,
meet(X1,X2) = meet(X1,join(complement(X1),X2)),
inference(cp,[status(thm)],[t4671,t20]) ).
cnf(t4707,plain,
meet(X1,join(complement(X1),X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t4691]) ).
cnf(t4090,plain,
join(X1,meet(X2,complement(meet(X3,X1)))) = join(X1,join(meet(X3,X1),X2)),
inference(cp,[status(thm)],[t1949,t4058]) ).
cnf(t77288,plain,
join(X1,meet(X2,complement(meet(X3,X1)))) = join(X1,X2),
inference(step,[status(thm)],[t4090,t1949]) ).
cnf(t24459,plain,
join(X1,meet(X2,complement(meet(X3,X1)))) = join(X1,X2),
inference(orient,[status(thm)],[t77288]) ).
cnf(t24469,plain,
join(X1,X2) = join(X1,meet(X2,join(X3,complement(X1)))),
inference(cp,[status(thm)],[t24459,t579]) ).
cnf(t26227,plain,
join(X1,meet(X2,join(X3,complement(X1)))) = join(X1,X2),
inference(orient,[status(thm)],[t24469]) ).
cnf(t26286,plain,
meet(X1,meet(X2,join(X3,complement(complement(X1))))) = meet(X1,join(complement(X1),X2)),
inference(cp,[status(thm)],[t4707,t26227]) ).
cnf(t77325,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,join(complement(X1),X2)),
inference(step,[status(thm)],[t26286,t347]) ).
cnf(t77326,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,X2),
inference(step,[status(thm)],[t77325,t4707]) ).
cnf(t26315,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t77326]) ).
cnf(t26427,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X1,X3))),
inference(cp,[status(thm)],[t26315,t20]) ).
cnf(t26700,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t26427]) ).
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(t9,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t35,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t9]) ).
cnf(t37,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t35,t19]) ).
cnf(t116,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t37]) ).
fof(f6,axiom,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',composition_distributivity) ).
fof(f6_nnf,plain,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
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(t28,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t12]) ).
cnf(t181,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(cp,[status(thm)],[t28,t180]) ).
cnf(t68872,plain,
composition(join(one,X1),X2) = join(X2,composition(X1,X2)),
inference(orient,[status(thm)],[t181]) ).
cnf(t455,plain,
join(X1,complement(X1)) = join(X1,top),
inference(cp,[status(thm)],[t453,t25]) ).
cnf(t76534,plain,
top = join(X1,top),
inference(step,[status(thm)],[t455,t25]) ).
cnf(t463,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t76534]) ).
cnf(t68929,plain,
join(X1,composition(top,X1)) = composition(top,X1),
inference(cp,[status(thm)],[t68872,t463]) ).
cnf(t69475,plain,
join(X1,composition(top,X1)) = composition(top,X1),
inference(orient,[status(thm)],[t68929]) ).
cnf(t69524,plain,
join(X1,converse(composition(top,converse(X1)))) = converse(composition(top,converse(X1))),
inference(cp,[status(thm)],[t116,t69475]) ).
cnf(t464,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t463,t20]) ).
cnf(t471,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t464]) ).
cnf(t117,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t116,t25]) ).
cnf(t250,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t117]) ).
cnf(t472,plain,
top = converse(top),
inference(cp,[status(thm)],[t471,t250]) ).
cnf(t477,plain,
converse(top) = top,
inference(orient,[status(thm)],[t472]) ).
cnf(t483,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(cp,[status(thm)],[t45,t477]) ).
cnf(t538,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(orient,[status(thm)],[t483]) ).
cnf(t78372,plain,
join(X1,composition(converse(converse(X1)),top)) = converse(composition(top,converse(X1))),
inference(step,[status(thm)],[t69524,t538]) ).
cnf(t78373,plain,
join(X1,composition(X1,top)) = converse(composition(top,converse(X1))),
inference(step,[status(thm)],[t78372,t19]) ).
cnf(t78374,plain,
join(X1,composition(X1,top)) = composition(converse(converse(X1)),top),
inference(step,[status(thm)],[t78373,t538]) ).
cnf(t78375,plain,
join(X1,composition(X1,top)) = composition(X1,top),
inference(step,[status(thm)],[t78374,t19]) ).
cnf(t69765,plain,
join(X1,composition(X1,top)) = composition(X1,top),
inference(orient,[status(thm)],[t78375]) ).
cnf(t69795,plain,
meet(X1,X2) = meet(X1,meet(X2,composition(X1,top))),
inference(cp,[status(thm)],[t26700,t69765]) ).
cnf(t74854,plain,
meet(X1,meet(X2,composition(X1,top))) = meet(X1,X2),
inference(orient,[status(thm)],[t69795]) ).
cnf(t622,plain,
meet(X1,complement(meet(complement(X1),X2))) = complement(complement(X1)),
inference(cp,[status(thm)],[t620,t494]) ).
cnf(t76548,plain,
meet(X1,join(X1,complement(X2))) = complement(complement(X1)),
inference(step,[status(thm)],[t622,t579]) ).
cnf(t76549,plain,
meet(X1,join(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t76548,t347]) ).
cnf(t642,plain,
meet(X1,join(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t76549]) ).
cnf(t650,plain,
X1 = meet(X1,join(X1,X2)),
inference(cp,[status(thm)],[t642,t347]) ).
cnf(t651,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t650]) ).
cnf(t658,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t651,t20]) ).
cnf(t663,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t658]) ).
cnf(t482,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(cp,[status(thm)],[t45,t477]) ).
cnf(t511,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(orient,[status(thm)],[t482]) ).
fof(f13,conjecture,
! [X0,X1] :
( ( composition(X1,top) = X1
& composition(X0,top) = X0 )
=> composition(meet(X0,X1),top) = meet(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f13_neg,negated_conjecture,
~ ! [X0,X1] :
( ( composition(X1,top) = X1
& composition(X0,top) = X0 )
=> composition(meet(X0,X1),top) = meet(X0,X1) ),
inference(negated_conjecture,[status(cth)],[f13]) ).
fof(f13_nnf,plain,
? [X0,X1] :
( composition(meet(X0,X1),top) != meet(X0,X1)
& composition(X1,top) = X1
& composition(X0,top) = X0 ),
inference(nnf_transformation,[status(thm)],[f13_neg]) ).
fof(f13_sk,plain,
( composition(meet(sk0,sk1),top) != meet(sk0,sk1)
& composition(sk1,top) = sk1
& composition(sk0,top) = sk0 ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1])],[f13_nnf]) ).
cnf(c13,plain,
composition(sk0,top) = sk0,
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(t1,plain,
composition(sk0,top) = sk0,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t52,plain,
composition(sk0,top) = sk0,
inference(orient,[status(thm)],[t1]) ).
cnf(t516,plain,
composition(top,converse(sk0)) = converse(sk0),
inference(cp,[status(thm)],[t511,t52]) ).
cnf(t533,plain,
composition(top,converse(sk0)) = converse(sk0),
inference(orient,[status(thm)],[t516]) ).
cnf(t535,plain,
composition(join(top,X1),converse(sk0)) = join(converse(sk0),composition(X1,converse(sk0))),
inference(cp,[status(thm)],[t28,t533]) ).
cnf(t76602,plain,
composition(top,converse(sk0)) = join(converse(sk0),composition(X1,converse(sk0))),
inference(step,[status(thm)],[t535,t471]) ).
cnf(t76603,plain,
converse(sk0) = join(converse(sk0),composition(X1,converse(sk0))),
inference(step,[status(thm)],[t76602,t533]) ).
cnf(t1379,plain,
join(converse(sk0),composition(X1,converse(sk0))) = converse(sk0),
inference(orient,[status(thm)],[t76603]) ).
cnf(t1386,plain,
join(sk0,converse(composition(X1,converse(sk0)))) = converse(converse(sk0)),
inference(cp,[status(thm)],[t116,t1379]) ).
cnf(t46,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t45,t19]) ).
cnf(t135,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t46]) ).
cnf(t76604,plain,
join(sk0,composition(sk0,converse(X1))) = converse(converse(sk0)),
inference(step,[status(thm)],[t1386,t135]) ).
cnf(t76605,plain,
join(sk0,composition(sk0,converse(X1))) = sk0,
inference(step,[status(thm)],[t76604,t19]) ).
cnf(t1390,plain,
join(sk0,composition(sk0,converse(X1))) = sk0,
inference(orient,[status(thm)],[t76605]) ).
cnf(t1398,plain,
sk0 = join(sk0,composition(sk0,X1)),
inference(cp,[status(thm)],[t1390,t19]) ).
cnf(t1419,plain,
join(sk0,composition(sk0,X1)) = sk0,
inference(orient,[status(thm)],[t1398]) ).
cnf(t1421,plain,
join(sk0,join(composition(sk0,X1),X2)) = join(sk0,X2),
inference(cp,[status(thm)],[t22,t1419]) ).
cnf(t2608,plain,
join(sk0,join(composition(sk0,X1),X2)) = join(sk0,X2),
inference(orient,[status(thm)],[t1421]) ).
cnf(t2613,plain,
join(sk0,composition(X1,X2)) = join(sk0,composition(join(sk0,X1),X2)),
inference(cp,[status(thm)],[t2608,t28]) ).
cnf(t18876,plain,
join(sk0,composition(join(sk0,X1),X2)) = join(sk0,composition(X1,X2)),
inference(orient,[status(thm)],[t2613]) ).
cnf(t18920,plain,
join(sk0,composition(meet(X1,sk0),X2)) = join(sk0,composition(sk0,X2)),
inference(cp,[status(thm)],[t18876,t503]) ).
cnf(t77104,plain,
join(sk0,composition(meet(X1,sk0),X2)) = sk0,
inference(step,[status(thm)],[t18920,t1419]) ).
cnf(t19007,plain,
join(sk0,composition(meet(X1,sk0),X2)) = sk0,
inference(orient,[status(thm)],[t77104]) ).
cnf(t19017,plain,
composition(meet(X1,sk0),X2) = meet(composition(meet(X1,sk0),X2),sk0),
inference(cp,[status(thm)],[t663,t19007]) ).
cnf(t77274,plain,
composition(meet(X1,sk0),X2) = meet(sk0,composition(meet(X1,sk0),X2)),
inference(step,[status(thm)],[t19017,t80]) ).
cnf(t24028,plain,
meet(sk0,composition(meet(X1,sk0),X2)) = composition(meet(X1,sk0),X2),
inference(orient,[status(thm)],[t77274]) ).
cnf(t74892,plain,
meet(meet(X1,sk0),sk0) = meet(meet(X1,sk0),composition(meet(X1,sk0),top)),
inference(cp,[status(thm)],[t74854,t24028]) ).
cnf(t26356,plain,
meet(meet(X1,X2),X3) = meet(meet(X1,X2),meet(X3,X1)),
inference(cp,[status(thm)],[t26315,t494]) ).
cnf(t26982,plain,
meet(meet(X1,X2),meet(X3,X1)) = meet(meet(X1,X2),X3),
inference(orient,[status(thm)],[t26356]) ).
cnf(t26993,plain,
meet(meet(X1,X2),X3) = meet(meet(X3,X1),meet(X1,X2)),
inference(cp,[status(thm)],[t26982,t80]) ).
cnf(t26337,plain,
meet(X1,X2) = meet(X1,meet(join(X3,X1),X2)),
inference(cp,[status(thm)],[t26315,t80]) ).
cnf(t26502,plain,
meet(X1,meet(join(X2,X1),X3)) = meet(X1,X3),
inference(orient,[status(thm)],[t26337]) ).
cnf(t26557,plain,
meet(meet(X1,X2),X3) = meet(meet(X1,X2),meet(X2,X3)),
inference(cp,[status(thm)],[t26502,t503]) ).
cnf(t27907,plain,
meet(meet(X1,X2),meet(X2,X3)) = meet(meet(X1,X2),X3),
inference(orient,[status(thm)],[t26557]) ).
cnf(t77328,plain,
meet(meet(X1,X2),X3) = meet(meet(X3,X1),X2),
inference(step,[status(thm)],[t26993,t27907]) ).
cnf(t28313,plain,
meet(meet(X1,X2),X3) = meet(meet(X3,X1),X2),
inference(orient,[status(thm)],[t77328]) ).
cnf(t28328,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(cp,[status(thm)],[t28313,t80]) ).
cnf(t29003,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t28328]) ).
cnf(t78440,plain,
meet(X1,meet(sk0,sk0)) = meet(meet(X1,sk0),composition(meet(X1,sk0),top)),
inference(step,[status(thm)],[t74892,t29003]) ).
cnf(t78441,plain,
meet(X1,sk0) = meet(meet(X1,sk0),composition(meet(X1,sk0),top)),
inference(step,[status(thm)],[t78440,t340]) ).
cnf(t78442,plain,
meet(X1,sk0) = meet(X1,meet(sk0,composition(meet(X1,sk0),top))),
inference(step,[status(thm)],[t78441,t29003]) ).
cnf(t54,plain,
composition(join(sk0,X1),top) = join(sk0,composition(X1,top)),
inference(cp,[status(thm)],[t28,t52]) ).
cnf(t267,plain,
composition(join(sk0,X1),top) = join(sk0,composition(X1,top)),
inference(orient,[status(thm)],[t54]) ).
cnf(t506,plain,
join(sk0,composition(meet(X1,sk0),top)) = composition(sk0,top),
inference(cp,[status(thm)],[t267,t503]) ).
cnf(t76579,plain,
join(sk0,composition(meet(X1,sk0),top)) = sk0,
inference(step,[status(thm)],[t506,t52]) ).
cnf(t1032,plain,
join(sk0,composition(meet(X1,sk0),top)) = sk0,
inference(orient,[status(thm)],[t76579]) ).
cnf(t1033,plain,
composition(meet(X1,sk0),top) = meet(composition(meet(X1,sk0),top),sk0),
inference(cp,[status(thm)],[t663,t1032]) ).
cnf(t77087,plain,
composition(meet(X1,sk0),top) = meet(sk0,composition(meet(X1,sk0),top)),
inference(step,[status(thm)],[t1033,t80]) ).
cnf(t17711,plain,
meet(sk0,composition(meet(X1,sk0),top)) = composition(meet(X1,sk0),top),
inference(orient,[status(thm)],[t77087]) ).
cnf(t78443,plain,
meet(X1,sk0) = meet(X1,composition(meet(X1,sk0),top)),
inference(step,[status(thm)],[t78442,t17711]) ).
cnf(t76366,plain,
meet(X1,composition(meet(X1,sk0),top)) = meet(X1,sk0),
inference(orient,[status(thm)],[t78443]) ).
cnf(c14,plain,
composition(sk1,top) = sk1,
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(t2,plain,
composition(sk1,top) = sk1,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t57,plain,
composition(sk1,top) = sk1,
inference(orient,[status(thm)],[t2]) ).
cnf(t515,plain,
composition(top,converse(sk1)) = converse(sk1),
inference(cp,[status(thm)],[t511,t57]) ).
cnf(t528,plain,
composition(top,converse(sk1)) = converse(sk1),
inference(orient,[status(thm)],[t515]) ).
cnf(t530,plain,
composition(join(top,X1),converse(sk1)) = join(converse(sk1),composition(X1,converse(sk1))),
inference(cp,[status(thm)],[t28,t528]) ).
cnf(t76596,plain,
composition(top,converse(sk1)) = join(converse(sk1),composition(X1,converse(sk1))),
inference(step,[status(thm)],[t530,t471]) ).
cnf(t76597,plain,
converse(sk1) = join(converse(sk1),composition(X1,converse(sk1))),
inference(step,[status(thm)],[t76596,t528]) ).
cnf(t1316,plain,
join(converse(sk1),composition(X1,converse(sk1))) = converse(sk1),
inference(orient,[status(thm)],[t76597]) ).
cnf(t1323,plain,
join(sk1,converse(composition(X1,converse(sk1)))) = converse(converse(sk1)),
inference(cp,[status(thm)],[t116,t1316]) ).
cnf(t76598,plain,
join(sk1,composition(sk1,converse(X1))) = converse(converse(sk1)),
inference(step,[status(thm)],[t1323,t135]) ).
cnf(t76599,plain,
join(sk1,composition(sk1,converse(X1))) = sk1,
inference(step,[status(thm)],[t76598,t19]) ).
cnf(t1327,plain,
join(sk1,composition(sk1,converse(X1))) = sk1,
inference(orient,[status(thm)],[t76599]) ).
cnf(t1335,plain,
sk1 = join(sk1,composition(sk1,X1)),
inference(cp,[status(thm)],[t1327,t19]) ).
cnf(t1356,plain,
join(sk1,composition(sk1,X1)) = sk1,
inference(orient,[status(thm)],[t1335]) ).
cnf(t1358,plain,
join(sk1,join(composition(sk1,X1),X2)) = join(sk1,X2),
inference(cp,[status(thm)],[t22,t1356]) ).
cnf(t2525,plain,
join(sk1,join(composition(sk1,X1),X2)) = join(sk1,X2),
inference(orient,[status(thm)],[t1358]) ).
cnf(t2530,plain,
join(sk1,composition(X1,X2)) = join(sk1,composition(join(sk1,X1),X2)),
inference(cp,[status(thm)],[t2525,t28]) ).
cnf(t18568,plain,
join(sk1,composition(join(sk1,X1),X2)) = join(sk1,composition(X1,X2)),
inference(orient,[status(thm)],[t2530]) ).
cnf(t18611,plain,
join(sk1,composition(meet(sk1,X1),X2)) = join(sk1,composition(sk1,X2)),
inference(cp,[status(thm)],[t18568,t494]) ).
cnf(t77096,plain,
join(sk1,composition(meet(sk1,X1),X2)) = sk1,
inference(step,[status(thm)],[t18611,t1356]) ).
cnf(t18658,plain,
join(sk1,composition(meet(sk1,X1),X2)) = sk1,
inference(orient,[status(thm)],[t77096]) ).
cnf(t18677,plain,
composition(meet(sk1,X1),X2) = meet(composition(meet(sk1,X1),X2),sk1),
inference(cp,[status(thm)],[t663,t18658]) ).
cnf(t77271,plain,
composition(meet(sk1,X1),X2) = meet(sk1,composition(meet(sk1,X1),X2)),
inference(step,[status(thm)],[t18677,t80]) ).
cnf(t23868,plain,
meet(sk1,composition(meet(sk1,X1),X2)) = composition(meet(sk1,X1),X2),
inference(orient,[status(thm)],[t77271]) ).
cnf(t76369,plain,
meet(sk1,sk0) = composition(meet(sk1,sk0),top),
inference(cp,[status(thm)],[t76366,t23868]) ).
cnf(t76451,plain,
composition(meet(sk1,sk0),top) = meet(sk1,sk0),
inference(orient,[status(thm)],[t76369]) ).
cnf(c15,plain,
composition(meet(sk0,sk1),top) != meet(sk0,sk1),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(goal_0,negated_conjecture,
composition(meet(sk0,sk1),top) != meet(sk0,sk1),
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(g0_0,plain,
composition(meet(sk1,sk0),top) != meet(sk0,sk1),
inference(rw,[status(thm)],[goal_0,t80]) ).
cnf(g0_1,plain,
meet(sk1,sk0) != meet(sk0,sk1),
inference(rw,[status(thm)],[g0_0,t76451]) ).
cnf(g0_2,plain,
meet(sk1,sk0) != meet(sk1,sk0),
inference(rw,[status(thm)],[g0_1,t80]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL019+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n003.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.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 07:17:50 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 41.16/5.69 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 41.16/5.69 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------