%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL007+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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 : Thu Sep 24 02:03:32 PM UTC 2026
% Result : Theorem 28.98s 4.19s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : REL007+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.43 % Computer : n019.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Mon Sep 21 03:58:05 UTC 2026
% 0.18/0.43 % CPUTime :
% 0.18/0.44 % Drodi V4.1.1
% 28.98/4.19 % Refutation found
% 28.98/4.19 % SZS status Theorem for theBenchmark: Theorem is valid
% 28.98/4.19 % SZS output start CNFRefutation for theBenchmark
% 28.98/4.19 fof(f1,axiom,(
% 28.98/4.19 (! [X0,X1] : join(X0,X1) = join(X1,X0) )),
% 28.98/4.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.98/4.19 fof(f2,axiom,(
% 28.98/4.19 (! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2) )),
% 28.98/4.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.98/4.19 fof(f3,axiom,(
% 28.98/4.19 (! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) )),
% 28.98/4.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.98/4.19 fof(f4,axiom,(
% 28.98/4.19 (! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))) )),
% 28.98/4.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.98/4.19 fof(f5,axiom,(
% 28.98/4.19 (! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2) )),
% 28.98/4.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.98/4.19 fof(f6,axiom,(
% 28.98/4.19 (! [X0] : composition(X0,one) = X0 )),
% 28.98/4.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.98/4.19 fof(f8,axiom,(
% 28.98/4.19 (! [X0] : converse(converse(X0)) = X0 )),
% 28.98/4.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.98/4.19 fof(f9,axiom,(
% 28.98/4.19 (! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)) )),
% 28.98/4.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.98/4.19 fof(f10,axiom,(
% 28.98/4.19 (! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)) )),
% 28.98/4.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.98/4.19 fof(f11,axiom,(
% 28.98/4.19 (! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1) )),
% 28.98/4.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.98/4.19 fof(f12,axiom,(
% 28.98/4.19 (! [X0] : top = join(X0,complement(X0)) )),
% 28.98/4.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.98/4.19 fof(f13,axiom,(
% 28.98/4.19 (! [X0] : zero = meet(X0,complement(X0)) )),
% 28.98/4.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.98/4.19 fof(f14,conjecture,(
% 28.98/4.19 (! [X0,X1] :( meet(X0,converse(X1)) = zero=> meet(converse(X0),X1) = zero ) )),
% 28.98/4.19 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 28.98/4.19 fof(f15,negated_conjecture,(
% 28.98/4.19 ~((! [X0,X1] :( meet(X0,converse(X1)) = zero=> meet(converse(X0),X1) = zero ) ))),
% 28.98/4.19 inference(negated_conjecture,[status(cth)],[f14])).
% 28.98/4.19 fof(f16,plain,(
% 28.98/4.19 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 28.98/4.19 inference(cnf_transformation,[status(thm)],[f1])).
% 28.98/4.19 fof(f17,plain,(
% 28.98/4.19 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 28.98/4.19 inference(cnf_transformation,[status(thm)],[f2])).
% 28.98/4.19 fof(f18,plain,(
% 28.98/4.19 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 28.98/4.19 inference(cnf_transformation,[status(thm)],[f3])).
% 28.98/4.19 fof(f19,plain,(
% 28.98/4.19 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 28.98/4.19 inference(cnf_transformation,[status(thm)],[f4])).
% 28.98/4.19 fof(f20,plain,(
% 28.98/4.19 ![X0,X1,X2]: (composition(X0,composition(X1,X2))=composition(composition(X0,X1),X2))),
% 28.98/4.19 inference(cnf_transformation,[status(thm)],[f5])).
% 28.98/4.19 fof(f21,plain,(
% 28.98/4.19 ![X0]: (composition(X0,one)=X0)),
% 28.98/4.19 inference(cnf_transformation,[status(thm)],[f6])).
% 28.98/4.19 fof(f23,plain,(
% 28.98/4.19 ![X0]: (converse(converse(X0))=X0)),
% 28.98/4.19 inference(cnf_transformation,[status(thm)],[f8])).
% 28.98/4.19 fof(f24,plain,(
% 28.98/4.19 ![X0,X1]: (converse(join(X0,X1))=join(converse(X0),converse(X1)))),
% 28.98/4.19 inference(cnf_transformation,[status(thm)],[f9])).
% 28.98/4.19 fof(f25,plain,(
% 28.98/4.19 ![X0,X1]: (converse(composition(X0,X1))=composition(converse(X1),converse(X0)))),
% 28.98/4.19 inference(cnf_transformation,[status(thm)],[f10])).
% 28.98/4.19 fof(f26,plain,(
% 28.98/4.19 ![X0,X1]: (join(composition(converse(X0),complement(composition(X0,X1))),complement(X1))=complement(X1))),
% 28.98/4.19 inference(cnf_transformation,[status(thm)],[f11])).
% 28.98/4.19 fof(f27,plain,(
% 28.98/4.19 ![X0]: (top=join(X0,complement(X0)))),
% 28.98/4.19 inference(cnf_transformation,[status(thm)],[f12])).
% 28.98/4.19 fof(f28,plain,(
% 28.98/4.19 ![X0]: (zero=meet(X0,complement(X0)))),
% 28.98/4.19 inference(cnf_transformation,[status(thm)],[f13])).
% 28.98/4.19 fof(f29,plain,(
% 28.98/4.19 (?[X0,X1]: (meet(X0,converse(X1))=zero&~meet(converse(X0),X1)=zero))),
% 28.98/4.19 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 28.98/4.19 fof(f30,plain,(
% 28.98/4.19 (meet(sK0_skl,converse(sK1_skl))=zero&~meet(converse(sK0_skl),sK1_skl)=zero)),
% 28.98/4.19 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(X0,sK0_skl),skolemize(X1,sK1_skl)],[f29])).
% 28.98/4.19 fof(f31,plain,(
% 28.98/4.19 meet(sK0_skl,converse(sK1_skl))=zero),
% 28.98/4.19 inference(cnf_transformation,[status(thm)],[f30])).
% 28.98/4.19 fof(f32,plain,(
% 28.98/4.19 ~meet(converse(sK0_skl),sK1_skl)=zero),
% 28.98/4.19 inference(cnf_transformation,[status(thm)],[f30])).
% 28.98/4.19 fof(f33,definition,(
% 28.98/4.19 sF1_fnc=converse(sK0_skl)),
% 28.98/4.19 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 28.98/4.19 fof(f34,definition,(
% 28.98/4.19 sF0_fnc=meet(sF1_fnc,sK1_skl)),
% 28.98/4.19 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 28.98/4.19 fof(f35,plain,(
% 28.98/4.19 ~sF0_fnc=zero),
% 28.98/4.19 inference(definition_folding,[],[f32,f34,f33])).
% 28.98/4.19 fof(f36,plain,(
% 28.98/4.19 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),complement(join(complement(X0),complement(X1)))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f16,f18])).
% 28.98/4.19 fof(f37,plain,(
% 28.98/4.19 ![X0,X1]: (X0=join(complement(join(complement(X0),X1)),meet(X0,X1)))),
% 28.98/4.19 inference(backward_demodulation,[status(thm)],[f19,f36])).
% 28.98/4.19 fof(f38,plain,(
% 28.98/4.19 ![X0,X1]: (join(complement(X0),composition(converse(X1),complement(composition(X1,X0))))=complement(X0))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f16,f26])).
% 28.98/4.19 fof(f39,plain,(
% 28.98/4.19 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f16,f37])).
% 28.98/4.19 fof(f44,plain,(
% 28.98/4.19 ![X0,X1,X2]: (meet(X0,join(complement(X1),complement(X2)))=complement(join(complement(X0),meet(X1,X2))))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f19,f19])).
% 28.98/4.19 fof(f47,plain,(
% 28.98/4.19 ![X0,X1]: (converse(join(converse(X0),X1))=join(X0,converse(X1)))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f23,f24])).
% 28.98/4.19 fof(f84,plain,(
% 28.98/4.19 ![X0,X1]: (converse(composition(converse(X0),X1))=composition(converse(X1),X0))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f23,f25])).
% 28.98/4.19 fof(f203,plain,(
% 28.98/4.19 sK0_skl=join(zero,complement(join(complement(sK0_skl),converse(sK1_skl))))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f31,f39])).
% 28.98/4.19 fof(f205,plain,(
% 28.98/4.19 ![X0]: (X0=join(zero,complement(join(complement(X0),complement(X0)))))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f28,f39])).
% 28.98/4.19 fof(f206,plain,(
% 28.98/4.19 ![X0,X1]: (X0=join(meet(X0,complement(X1)),meet(X0,X1)))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f19,f39])).
% 28.98/4.19 fof(f209,plain,(
% 28.98/4.19 sK0_skl=join(zero,complement(join(converse(sK1_skl),complement(sK0_skl))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f16,f203])).
% 28.98/4.19 fof(f211,plain,(
% 28.98/4.19 ![X0]: (X0=join(zero,meet(X0,X0)))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f19,f205])).
% 28.98/4.19 fof(f212,plain,(
% 28.98/4.19 ![X0,X1]: (X0=join(meet(X0,X1),meet(X0,complement(X1))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f16,f206])).
% 28.98/4.19 fof(f217,plain,(
% 28.98/4.19 ![X0]: (converse(top)=join(X0,converse(complement(converse(X0)))))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f27,f47])).
% 28.98/4.19 fof(f218,plain,(
% 28.98/4.19 ![X0]: (meet(X0,complement(X0))=complement(top))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f27,f19])).
% 28.98/4.19 fof(f219,plain,(
% 28.98/4.19 ![X0]: (X0=join(meet(X0,complement(complement(X0))),complement(top)))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f27,f39])).
% 28.98/4.19 fof(f221,plain,(
% 28.98/4.19 zero=complement(top)),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f28,f218])).
% 28.98/4.19 fof(f222,plain,(
% 28.98/4.19 ![X0]: (X0=join(complement(top),meet(X0,complement(complement(X0)))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f16,f219])).
% 28.98/4.19 fof(f223,plain,(
% 28.98/4.19 ![X0]: (X0=join(zero,meet(X0,complement(complement(X0)))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f221,f222])).
% 28.98/4.19 fof(f229,plain,(
% 28.98/4.19 ![X0]: (meet(top,X0)=complement(join(zero,complement(X0))))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f221,f19])).
% 28.98/4.19 fof(f235,plain,(
% 28.98/4.19 ![X0,X1]: (converse(join(X0,X1))=join(converse(X1),converse(X0)))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f24,f16])).
% 28.98/4.19 fof(f243,plain,(
% 28.98/4.19 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f16,f19])).
% 28.98/4.19 fof(f266,plain,(
% 28.98/4.19 ![X0,X1]: (composition(X0,composition(one,X1))=composition(X0,X1))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f21,f20])).
% 28.98/4.19 fof(f282,plain,(
% 28.98/4.19 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f16,f17])).
% 28.98/4.19 fof(f290,plain,(
% 28.98/4.19 ![X0,X1,X2]: (join(meet(X0,X1),join(complement(join(complement(X0),X1)),X2))=join(X0,X2))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f39,f17])).
% 28.98/4.19 fof(f517,plain,(
% 28.98/4.19 ![X0,X1]: (meet(top,join(complement(X0),complement(X1)))=complement(join(zero,meet(X0,X1))))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f221,f44])).
% 28.98/4.19 fof(f683,plain,(
% 28.98/4.19 ![X0]: (X0=join(meet(X0,converse(complement(converse(complement(X0))))),complement(converse(top))))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f217,f39])).
% 28.98/4.19 fof(f729,plain,(
% 28.98/4.19 ![X0]: (X0=join(complement(converse(top)),meet(X0,converse(complement(converse(complement(X0)))))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f16,f683])).
% 28.98/4.19 fof(f785,plain,(
% 28.98/4.19 ![X0]: (join(zero,complement(X0))=join(zero,meet(join(zero,complement(X0)),complement(meet(top,X0)))))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f229,f223])).
% 28.98/4.19 fof(f935,plain,(
% 28.98/4.19 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f19,f243])).
% 28.98/4.19 fof(f955,plain,(
% 28.98/4.19 ![X0,X1]: (meet(top,join(complement(X0),complement(X1)))=complement(join(zero,meet(X1,X0))))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f243,f229])).
% 28.98/4.19 fof(f961,plain,(
% 28.98/4.19 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,meet(join(complement(X0),complement(X1)),complement(meet(X1,X0)))))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f243,f223])).
% 28.98/4.19 fof(f968,plain,(
% 28.98/4.19 sF0_fnc=meet(sK1_skl,sF1_fnc)),
% 28.98/4.19 inference(backward_demodulation,[status(thm)],[f935,f34])).
% 28.98/4.19 fof(f971,plain,(
% 28.98/4.19 ![X0]: (join(zero,complement(X0))=join(zero,meet(complement(meet(top,X0)),join(zero,complement(X0)))))),
% 28.98/4.19 inference(backward_demodulation,[status(thm)],[f935,f785])).
% 28.98/4.19 fof(f1002,plain,(
% 28.98/4.19 ![X0,X1]: (join(complement(X0),complement(X1))=join(zero,meet(complement(meet(X1,X0)),join(complement(X0),complement(X1)))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f935,f961])).
% 28.98/4.19 fof(f1159,plain,(
% 28.98/4.19 ![X0]: (converse(converse(X0))=composition(converse(one),X0))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f21,f84])).
% 28.98/4.19 fof(f1200,plain,(
% 28.98/4.19 ![X0]: (X0=composition(converse(one),X0))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f23,f1159])).
% 28.98/4.19 fof(f1261,plain,(
% 28.98/4.19 ![X0]: (composition(one,X0)=composition(converse(one),X0))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f266,f1200])).
% 28.98/4.19 fof(f1265,plain,(
% 28.98/4.19 ![X0]: (join(complement(X0),complement(composition(one,X0)))=complement(X0))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f1200,f38])).
% 28.98/4.19 fof(f1281,plain,(
% 28.98/4.19 ![X0]: (composition(one,X0)=X0)),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f1200,f1261])).
% 28.98/4.19 fof(f1285,plain,(
% 28.98/4.19 ![X0]: (join(complement(X0),complement(X0))=complement(X0))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f1281,f1265])).
% 28.98/4.19 fof(f1378,plain,(
% 28.98/4.19 ![X0]: (meet(X0,X0)=complement(complement(X0)))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f1285,f243])).
% 28.98/4.19 fof(f1380,plain,(
% 28.98/4.19 ![X0]: (X0=join(meet(X0,complement(X0)),complement(complement(X0))))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f1285,f39])).
% 28.98/4.19 fof(f1428,plain,(
% 28.98/4.19 ![X0]: (X0=join(complement(complement(X0)),meet(X0,complement(X0))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f16,f1380])).
% 28.98/4.19 fof(f1429,plain,(
% 28.98/4.19 ![X0]: (X0=join(complement(complement(X0)),zero))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f28,f1428])).
% 28.98/4.19 fof(f1430,plain,(
% 28.98/4.19 ![X0]: (X0=join(zero,complement(complement(X0))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f16,f1429])).
% 28.98/4.19 fof(f1468,plain,(
% 28.98/4.19 ![X0]: (meet(top,complement(X0))=complement(X0))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f1430,f229])).
% 28.98/4.19 fof(f1487,plain,(
% 28.98/4.19 ![X0,X1]: (meet(top,meet(X0,X1))=complement(join(complement(X1),complement(X0))))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f243,f1468])).
% 28.98/4.19 fof(f1497,plain,(
% 28.98/4.19 ![X0]: (top=join(complement(X0),complement(join(complement(top),complement(X0)))))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f1468,f39])).
% 28.98/4.19 fof(f1508,plain,(
% 28.98/4.19 ![X0,X1]: (meet(top,meet(X0,X1))=meet(X0,X1))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f243,f1487])).
% 28.98/4.19 fof(f1521,plain,(
% 28.98/4.19 ![X0]: (top=join(complement(X0),meet(X0,top)))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f243,f1497])).
% 28.98/4.19 fof(f1580,plain,(
% 28.98/4.19 ![X0]: (meet(X0,join(complement(X0),complement(top)))=complement(top))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f1521,f44])).
% 28.98/4.19 fof(f1582,plain,(
% 28.98/4.19 ![X0,X1]: (join(complement(X0),join(meet(X0,top),X1))=join(top,X1))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f1521,f17])).
% 28.98/4.19 fof(f1594,plain,(
% 28.98/4.19 ![X0]: (meet(X0,join(complement(X0),zero))=complement(top))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f221,f1580])).
% 28.98/4.19 fof(f1595,plain,(
% 28.98/4.19 ![X0]: (meet(X0,join(zero,complement(X0)))=complement(top))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f16,f1594])).
% 28.98/4.19 fof(f1596,plain,(
% 28.98/4.19 ![X0]: (meet(X0,join(zero,complement(X0)))=zero)),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f221,f1595])).
% 28.98/4.19 fof(f1617,plain,(
% 28.98/4.19 ![X0]: (join(meet(X0,X0),complement(complement(X0)))=complement(complement(X0)))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f1378,f1285])).
% 28.98/4.19 fof(f1630,plain,(
% 28.98/4.19 ![X0]: (zero=meet(complement(X0),meet(X0,X0)))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f1378,f28])).
% 28.98/4.19 fof(f1737,plain,(
% 28.98/4.19 ![X0,X1]: (zero=meet(meet(X0,X1),meet(join(complement(X0),complement(X1)),join(complement(X0),complement(X1)))))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f19,f1630])).
% 28.98/4.19 fof(f1760,plain,(
% 28.98/4.19 ![X0,X1]: (zero=meet(meet(X0,X1),complement(complement(join(complement(X0),complement(X1))))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f1378,f1737])).
% 28.98/4.19 fof(f1762,plain,(
% 28.98/4.19 ![X0,X1]: (zero=meet(meet(X0,X1),complement(meet(X1,X0))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f243,f1760])).
% 28.98/4.19 fof(f2158,plain,(
% 28.98/4.19 meet(top,join(converse(sK1_skl),complement(sK0_skl)))=complement(sK0_skl)),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f209,f229])).
% 28.98/4.19 fof(f2187,plain,(
% 28.98/4.19 ![X0]: (X0=join(zero,complement(join(complement(X0),join(zero,complement(X0))))))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f1596,f39])).
% 28.98/4.19 fof(f2224,plain,(
% 28.98/4.19 ![X0]: (X0=join(zero,complement(join(zero,join(complement(X0),complement(X0))))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f282,f2187])).
% 28.98/4.19 fof(f2225,plain,(
% 28.98/4.19 ![X0]: (X0=join(zero,complement(join(zero,complement(X0)))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f1285,f2224])).
% 28.98/4.19 fof(f2228,plain,(
% 28.98/4.19 ![X0]: (X0=join(zero,meet(top,X0)))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f229,f2225])).
% 28.98/4.19 fof(f2239,plain,(
% 28.98/4.19 ![X0,X1]: (meet(X0,X1)=join(zero,meet(X0,X1)))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f1508,f2228])).
% 28.98/4.19 fof(f2240,plain,(
% 28.98/4.19 ![X0]: (complement(X0)=join(zero,complement(X0)))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f1468,f2228])).
% 28.98/4.19 fof(f2245,plain,(
% 28.98/4.19 ![X0]: (X0=join(zero,meet(X0,top)))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f935,f2228])).
% 28.98/4.19 fof(f2254,plain,(
% 28.98/4.19 ![X0]: (X0=meet(top,X0))),
% 28.98/4.19 inference(backward_demodulation,[status(thm)],[f2239,f2228])).
% 28.98/4.19 fof(f2258,plain,(
% 28.98/4.19 ![X0]: (X0=meet(X0,X0))),
% 28.98/4.19 inference(backward_demodulation,[status(thm)],[f2239,f211])).
% 28.98/4.19 fof(f2259,plain,(
% 28.98/4.19 ![X0]: (join(zero,complement(X0))=meet(complement(meet(top,X0)),join(zero,complement(X0))))),
% 28.98/4.19 inference(backward_demodulation,[status(thm)],[f2239,f971])).
% 28.98/4.19 fof(f2262,plain,(
% 28.98/4.19 ![X0,X1]: (join(complement(X0),complement(X1))=meet(complement(meet(X1,X0)),join(complement(X0),complement(X1))))),
% 28.98/4.19 inference(backward_demodulation,[status(thm)],[f2239,f1002])).
% 28.98/4.19 fof(f2278,plain,(
% 28.98/4.19 ![X0,X1]: (meet(top,join(complement(X0),complement(X1)))=complement(meet(X1,X0)))),
% 28.98/4.19 inference(backward_demodulation,[status(thm)],[f2239,f955])).
% 28.98/4.19 fof(f2279,plain,(
% 28.98/4.19 ![X0,X1]: (meet(top,join(complement(X0),complement(X1)))=complement(meet(X0,X1)))),
% 28.98/4.19 inference(backward_demodulation,[status(thm)],[f2239,f517])).
% 28.98/4.19 fof(f2281,plain,(
% 28.98/4.19 ![X0]: (X0=complement(complement(X0)))),
% 28.98/4.19 inference(backward_demodulation,[status(thm)],[f2240,f1430])).
% 28.98/4.19 fof(f2319,plain,(
% 28.98/4.19 ![X0,X1]: (join(complement(X0),join(X0,X1))=join(top,X1))),
% 28.98/4.19 inference(backward_demodulation,[status(thm)],[f2324,f1582])).
% 28.98/4.19 fof(f2324,plain,(
% 28.98/4.19 ![X0]: (X0=meet(X0,top))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f2239,f2245])).
% 28.98/4.19 fof(f2334,plain,(
% 28.98/4.19 join(converse(sK1_skl),complement(sK0_skl))=complement(sK0_skl)),
% 28.98/4.19 inference(backward_demodulation,[status(thm)],[f2254,f2158])).
% 28.98/4.19 fof(f2369,plain,(
% 28.98/4.19 ![X0]: (join(X0,complement(complement(X0)))=complement(complement(X0)))),
% 28.98/4.19 inference(backward_demodulation,[status(thm)],[f2258,f1617])).
% 28.98/4.19 fof(f2372,plain,(
% 28.98/4.19 ![X0]: (complement(X0)=meet(complement(meet(top,X0)),join(zero,complement(X0))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f2240,f2259])).
% 28.98/4.19 fof(f2373,plain,(
% 28.98/4.19 ![X0]: (complement(X0)=meet(complement(X0),join(zero,complement(X0))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f2254,f2372])).
% 28.98/4.19 fof(f2374,plain,(
% 28.98/4.19 ![X0]: (complement(X0)=meet(complement(X0),complement(X0)))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f2240,f2373])).
% 28.98/4.19 fof(f2375,plain,(
% 28.98/4.19 ![X0]: (complement(X0)=complement(complement(complement(X0))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f1378,f2374])).
% 28.98/4.19 fof(f2403,plain,(
% 28.98/4.19 ![X0,X1]: (join(complement(X0),complement(X1))=meet(complement(meet(X1,X0)),complement(meet(X1,X0))))),
% 28.98/4.19 inference(backward_demodulation,[status(thm)],[f2468,f2262])).
% 28.98/4.19 fof(f2468,plain,(
% 28.98/4.19 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X1,X0)))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f2254,f2278])).
% 28.98/4.19 fof(f2469,plain,(
% 28.98/4.19 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X0,X1)))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f2254,f2279])).
% 28.98/4.19 fof(f2529,plain,(
% 28.98/4.19 ![X0,X1]: (join(X0,join(X1,complement(X0)))=join(top,X1))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f282,f2319])).
% 28.98/4.19 fof(f2571,plain,(
% 28.98/4.19 ![X0]: (join(X0,X0)=complement(complement(X0)))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f2281,f2369])).
% 28.98/4.19 fof(f2604,plain,(
% 28.98/4.19 ![X0]: (join(X0,X0)=X0)),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f2281,f2571])).
% 28.98/4.19 fof(f2619,plain,(
% 28.98/4.19 ![X0,X1]: (complement(meet(X0,X1))=meet(complement(meet(X1,X0)),complement(meet(X1,X0))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f2469,f2403])).
% 28.98/4.19 fof(f2620,plain,(
% 28.98/4.19 ![X0,X1]: (complement(meet(X0,X1))=complement(complement(complement(meet(X1,X0)))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f1378,f2619])).
% 28.98/4.19 fof(f2621,plain,(
% 28.98/4.19 ![X0,X1]: (complement(meet(X0,X1))=complement(meet(X1,X0)))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f2375,f2620])).
% 28.98/4.19 fof(f2694,plain,(
% 28.98/4.19 ![X0]: (X0=join(X0,meet(X0,complement(X0))))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f2258,f212])).
% 28.98/4.19 fof(f2701,plain,(
% 28.98/4.19 ![X0]: (X0=join(X0,zero))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f28,f2694])).
% 28.98/4.19 fof(f2716,plain,(
% 28.98/4.19 ![X0,X1]: (join(X0,join(X0,X1))=join(X0,X1))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f2604,f17])).
% 28.98/4.19 fof(f2760,plain,(
% 28.98/4.19 ![X0]: (X0=join(zero,X0))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f16,f2701])).
% 28.98/4.19 fof(f3046,plain,(
% 28.98/4.19 ![X0,X1]: (join(meet(X0,X1),X0)=join(meet(X0,X1),meet(X0,complement(X1))))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f212,f2716])).
% 28.98/4.19 fof(f3065,plain,(
% 28.98/4.19 ![X0]: (join(X0,top)=join(X0,complement(X0)))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f27,f2716])).
% 28.98/4.19 fof(f3090,plain,(
% 28.98/4.19 ![X0,X1]: (join(X0,meet(X0,X1))=join(meet(X0,X1),meet(X0,complement(X1))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f16,f3046])).
% 28.98/4.19 fof(f3098,plain,(
% 28.98/4.19 ![X0,X1]: (join(X0,meet(X0,X1))=X0)),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f212,f3090])).
% 28.98/4.19 fof(f3137,plain,(
% 28.98/4.19 ![X0]: (join(X0,top)=top)),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f27,f3065])).
% 28.98/4.19 fof(f3190,plain,(
% 28.98/4.19 ![X0]: (join(top,X0)=top)),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f16,f3137])).
% 28.98/4.19 fof(f3210,plain,(
% 28.98/4.19 ![X0,X1]: (join(X0,join(X1,complement(X0)))=top)),
% 28.98/4.19 inference(backward_demodulation,[status(thm)],[f3190,f2529])).
% 28.98/4.19 fof(f3251,plain,(
% 28.98/4.19 converse(top)=top),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f217,f3190])).
% 28.98/4.19 fof(f3272,plain,(
% 28.98/4.19 ![X0]: (X0=join(complement(top),meet(X0,converse(complement(converse(complement(X0)))))))),
% 28.98/4.19 inference(backward_demodulation,[status(thm)],[f3251,f729])).
% 28.98/4.19 fof(f3283,plain,(
% 28.98/4.19 ![X0]: (X0=join(zero,meet(X0,converse(complement(converse(complement(X0)))))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f221,f3272])).
% 28.98/4.19 fof(f3284,plain,(
% 28.98/4.19 ![X0]: (X0=meet(X0,converse(complement(converse(complement(X0))))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f2760,f3283])).
% 28.98/4.19 fof(f3348,plain,(
% 28.98/4.19 ![X0,X1]: (join(X0,meet(X1,X0))=X0)),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f935,f3098])).
% 28.98/4.19 fof(f3381,plain,(
% 28.98/4.19 ![X0,X1]: (converse(converse(X0))=join(X0,converse(meet(X1,converse(X0)))))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f3348,f47])).
% 28.98/4.19 fof(f3388,plain,(
% 28.98/4.19 ![X0,X1]: (X0=join(X0,converse(meet(X1,converse(X0)))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f23,f3381])).
% 28.98/4.19 fof(f3413,plain,(
% 28.98/4.19 ![X0,X1]: (X0=join(meet(X0,join(X1,complement(complement(X0)))),complement(top)))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f3210,f39])).
% 28.98/4.19 fof(f3429,plain,(
% 28.98/4.19 ![X0,X1]: (X0=join(complement(top),meet(X0,join(X1,complement(complement(X0))))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f16,f3413])).
% 28.98/4.19 fof(f3430,plain,(
% 28.98/4.19 ![X0,X1]: (X0=join(zero,meet(X0,join(X1,complement(complement(X0))))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f221,f3429])).
% 28.98/4.19 fof(f3431,plain,(
% 28.98/4.19 ![X0,X1]: (X0=meet(X0,join(X1,complement(complement(X0)))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f2760,f3430])).
% 28.98/4.19 fof(f3432,plain,(
% 28.98/4.19 ![X0,X1]: (X0=meet(X0,join(X1,X0)))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f2281,f3431])).
% 28.98/4.19 fof(f3460,plain,(
% 28.98/4.19 ![X0,X1]: (converse(X0)=meet(converse(X0),converse(join(X0,X1))))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f235,f3432])).
% 28.98/4.19 fof(f3462,plain,(
% 28.98/4.19 ![X0,X1]: (meet(X0,X1)=meet(meet(X0,X1),X1))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f3348,f3432])).
% 28.98/4.19 fof(f3497,plain,(
% 28.98/4.19 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X0,X1)))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f935,f3462])).
% 28.98/4.19 fof(f3926,plain,(
% 28.98/4.19 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X1,X0)))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f935,f3497])).
% 28.98/4.19 fof(f4882,plain,(
% 28.98/4.19 ![X0,X1]: (top=join(X0,complement(meet(X0,X1))))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f3210,f290])).
% 28.98/4.19 fof(f5238,plain,(
% 28.98/4.19 ![X0,X1]: (top=join(X0,complement(meet(X1,X0))))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f3926,f4882])).
% 28.98/4.19 fof(f5653,plain,(
% 28.98/4.19 ![X0]: (complement(converse(complement(X0)))=join(complement(converse(complement(X0))),converse(X0)))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f3284,f3388])).
% 28.98/4.19 fof(f5681,plain,(
% 28.98/4.19 ![X0]: (complement(converse(complement(X0)))=join(converse(X0),complement(converse(complement(X0)))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f16,f5653])).
% 28.98/4.19 fof(f11331,plain,(
% 28.98/4.19 ![X0,X1]: (top=complement(meet(meet(X0,complement(X1)),X1)))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f5238,f2468])).
% 28.98/4.19 fof(f11346,plain,(
% 28.98/4.19 ![X0,X1]: (join(complement(X0),X1)=complement(meet(complement(X1),X0)))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f2281,f2468])).
% 28.98/4.19 fof(f11380,plain,(
% 28.98/4.19 ![X0,X1]: (top=complement(meet(X0,meet(X1,complement(X0)))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f2621,f11331])).
% 28.98/4.19 fof(f11466,plain,(
% 28.98/4.19 ![X0,X1]: (zero=meet(meet(meet(X0,complement(X1)),X1),top))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f11380,f1762])).
% 28.98/4.19 fof(f11517,plain,(
% 28.98/4.19 ![X0,X1]: (zero=meet(meet(X0,complement(X1)),X1))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f2324,f11466])).
% 28.98/4.19 fof(f11521,plain,(
% 28.98/4.19 ![X0,X1]: (zero=meet(X0,meet(X1,complement(X0))))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f935,f11517])).
% 28.98/4.19 fof(f11624,plain,(
% 28.98/4.19 ![X0,X1]: (zero=meet(complement(X0),meet(X1,X0)))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f2281,f11521])).
% 28.98/4.19 fof(f21627,plain,(
% 28.98/4.19 converse(converse(sK1_skl))=meet(converse(converse(sK1_skl)),converse(complement(sK0_skl)))),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f2334,f3460])).
% 28.98/4.19 fof(f21827,plain,(
% 28.98/4.19 sK1_skl=meet(converse(converse(sK1_skl)),converse(complement(sK0_skl)))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f23,f21627])).
% 28.98/4.19 fof(f21828,plain,(
% 28.98/4.19 sK1_skl=meet(sK1_skl,converse(complement(sK0_skl)))),
% 28.98/4.19 inference(forward_demodulation,[status(thm)],[f23,f21827])).
% 28.98/4.19 fof(f22037,plain,(
% 28.98/4.19 zero=meet(complement(converse(complement(sK0_skl))),sK1_skl)),
% 28.98/4.19 inference(paramodulation,[status(thm)],[f21828,f11624])).
% 28.98/4.19 fof(f22071,plain,(
% 28.98/4.19 zero=meet(sK1_skl,complement(converse(complement(sK0_skl))))),
% 28.98/4.25 inference(forward_demodulation,[status(thm)],[f935,f22037])).
% 28.98/4.25 fof(f32972,plain,(
% 28.98/4.25 ![X0]: (join(complement(converse(complement(converse(complement(complement(X0)))))),X0)=complement(complement(X0)))),
% 28.98/4.25 inference(paramodulation,[status(thm)],[f3284,f11346])).
% 28.98/4.25 fof(f33065,plain,(
% 28.98/4.25 ![X0]: (join(X0,complement(converse(complement(converse(complement(complement(X0)))))))=complement(complement(X0)))),
% 28.98/4.25 inference(forward_demodulation,[status(thm)],[f16,f32972])).
% 28.98/4.25 fof(f33066,plain,(
% 28.98/4.25 ![X0]: (join(X0,complement(converse(complement(converse(X0)))))=complement(complement(X0)))),
% 28.98/4.25 inference(forward_demodulation,[status(thm)],[f2281,f33065])).
% 28.98/4.25 fof(f33067,plain,(
% 28.98/4.25 ![X0]: (join(X0,complement(converse(complement(converse(X0)))))=X0)),
% 28.98/4.25 inference(forward_demodulation,[status(thm)],[f2281,f33066])).
% 28.98/4.25 fof(f33278,plain,(
% 28.98/4.25 ![X0]: (join(converse(X0),complement(converse(complement(X0))))=converse(X0))),
% 28.98/4.25 inference(paramodulation,[status(thm)],[f23,f33067])).
% 28.98/4.25 fof(f33375,plain,(
% 28.98/4.25 ![X0]: (complement(converse(complement(X0)))=converse(X0))),
% 28.98/4.25 inference(backward_demodulation,[status(thm)],[f33278,f5681])).
% 28.98/4.25 fof(f33474,plain,(
% 28.98/4.25 zero=meet(sK1_skl,converse(sK0_skl))),
% 28.98/4.25 inference(backward_demodulation,[status(thm)],[f33375,f22071])).
% 28.98/4.25 fof(f33616,plain,(
% 28.98/4.25 sF0_fnc=zero),
% 28.98/4.25 inference(backward_demodulation,[status(thm)],[f33617,f968])).
% 28.98/4.25 fof(f33617,plain,(
% 28.98/4.25 zero=meet(sK1_skl,sF1_fnc)),
% 28.98/4.25 inference(forward_demodulation,[status(thm)],[f33,f33474])).
% 28.98/4.25 fof(f33672,plain,(
% 28.98/4.25 $false),
% 28.98/4.25 inference(forward_subsumption_resolution,[status(thm)],[f33616,f35])).
% 28.98/4.25 % SZS output end CNFRefutation for theBenchmark.p
% 23.01/4.30 % Elapsed time: 3.850440 seconds
% 23.01/4.30 % CPU time: 30.075951 seconds
% 23.01/4.30 % Total memory used: 227.392 MB
% 23.01/4.30 % Net memory used: 220.276 MB
%------------------------------------------------------------------------------