%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : REL048+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 : n017.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:45 PM UTC 2026
% Result : Theorem 0.27s 0.85s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : REL048+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.16/0.44 % Computer : n017.cluster.edu
% 0.16/0.44 % Model : x86_64 x86_64
% 0.16/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.44 % Memory : 8046.5625MB
% 0.16/0.44 % OS : Linux 6.8.0-71-generic
% 0.16/0.44 % CPULimit : 300
% 0.16/0.44 % WCLimit : 300
% 0.16/0.44 % DateTime : Mon Sep 21 04:03:58 UTC 2026
% 0.16/0.45 % CPUTime :
% 0.16/0.47 % Drodi V4.1.1
% 0.27/0.85 % Refutation found
% 0.27/0.85 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.27/0.85 % SZS output start CNFRefutation for theBenchmark
% 0.27/0.85 fof(f1,axiom,(
% 0.27/0.85 (! [X0,X1] : join(X0,X1) = join(X1,X0) )),
% 0.27/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.27/0.85 fof(f2,axiom,(
% 0.27/0.85 (! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2) )),
% 0.27/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.27/0.85 fof(f3,axiom,(
% 0.27/0.85 (! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))) )),
% 0.27/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.27/0.85 fof(f4,axiom,(
% 0.27/0.85 (! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))) )),
% 0.27/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.27/0.85 fof(f12,axiom,(
% 0.27/0.85 (! [X0] : top = join(X0,complement(X0)) )),
% 0.27/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.27/0.85 fof(f13,axiom,(
% 0.27/0.85 (! [X0] : zero = meet(X0,complement(X0)) )),
% 0.27/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.27/0.85 fof(f14,conjecture,(
% 0.27/0.85 (! [X0,X1,X2] :( join(join(X0,X1),X2) = X2=> ( join(X0,X2) = X2& join(X1,X2) = X2 ) ) )),
% 0.27/0.85 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.27/0.85 fof(f15,negated_conjecture,(
% 0.27/0.85 ~((! [X0,X1,X2] :( join(join(X0,X1),X2) = X2=> ( join(X0,X2) = X2& join(X1,X2) = X2 ) ) ))),
% 0.27/0.85 inference(negated_conjecture,[status(cth)],[f14])).
% 0.27/0.85 fof(f16,plain,(
% 0.27/0.85 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 0.27/0.85 inference(cnf_transformation,[status(thm)],[f1])).
% 0.27/0.85 fof(f17,plain,(
% 0.27/0.85 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),X2))),
% 0.27/0.85 inference(cnf_transformation,[status(thm)],[f2])).
% 0.27/0.85 fof(f18,plain,(
% 0.27/0.85 ![X0,X1]: (X0=join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))))),
% 0.27/0.85 inference(cnf_transformation,[status(thm)],[f3])).
% 0.27/0.85 fof(f19,plain,(
% 0.27/0.85 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X0),complement(X1))))),
% 0.27/0.85 inference(cnf_transformation,[status(thm)],[f4])).
% 0.27/0.85 fof(f27,plain,(
% 0.27/0.85 ![X0]: (top=join(X0,complement(X0)))),
% 0.27/0.85 inference(cnf_transformation,[status(thm)],[f12])).
% 0.27/0.85 fof(f28,plain,(
% 0.27/0.85 ![X0]: (zero=meet(X0,complement(X0)))),
% 0.27/0.85 inference(cnf_transformation,[status(thm)],[f13])).
% 0.27/0.85 fof(f29,plain,(
% 0.27/0.85 (?[X0,X1,X2]: (join(join(X0,X1),X2)=X2&(~join(X0,X2)=X2|~join(X1,X2)=X2)))),
% 0.27/0.85 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.27/0.85 fof(f30,plain,(
% 0.27/0.85 (join(join(sK0_skl,sK1_skl),sK2_skl)=sK2_skl&(~join(sK0_skl,sK2_skl)=sK2_skl|~join(sK1_skl,sK2_skl)=sK2_skl))),
% 0.27/0.85 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl]),skolemize(X0,sK0_skl),skolemize(X1,sK1_skl),skolemize(X2,sK2_skl)],[f29])).
% 0.27/0.85 fof(f31,plain,(
% 0.27/0.85 join(join(sK0_skl,sK1_skl),sK2_skl)=sK2_skl),
% 0.27/0.85 inference(cnf_transformation,[status(thm)],[f30])).
% 0.27/0.85 fof(f32,plain,(
% 0.27/0.85 ~join(sK0_skl,sK2_skl)=sK2_skl|~join(sK1_skl,sK2_skl)=sK2_skl),
% 0.27/0.85 inference(cnf_transformation,[status(thm)],[f30])).
% 0.27/0.85 fof(f33,definition,(
% 0.27/0.85 sQ0_spl <=> (join(sK0_skl,sK2_skl)=sK2_skl)),
% 0.27/0.85 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.27/0.85 fof(f35,plain,(
% 0.27/0.85 ~join(sK0_skl,sK2_skl)=sK2_skl|sQ0_spl),
% 0.27/0.85 inference(component_clause,[status(thm)],[f33])).
% 0.27/0.85 fof(f36,definition,(
% 0.27/0.85 sQ1_spl <=> (join(sK1_skl,sK2_skl)=sK2_skl)),
% 0.27/0.85 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.27/0.85 fof(f38,plain,(
% 0.27/0.85 ~join(sK1_skl,sK2_skl)=sK2_skl|sQ1_spl),
% 0.27/0.85 inference(component_clause,[status(thm)],[f36])).
% 0.27/0.85 fof(f39,plain,(
% 0.27/0.85 ~sQ0_spl|~sQ1_spl),
% 0.27/0.85 inference(split_clause,[status(thm)],[f32,f33,f36])).
% 0.27/0.85 fof(f40,plain,(
% 0.27/0.85 ![X0,X1]: (X0=join(meet(X0,X1),complement(join(complement(X0),X1))))),
% 0.27/0.85 inference(backward_demodulation,[status(thm)],[f19,f18])).
% 0.27/0.85 fof(f41,plain,(
% 0.27/0.85 join(sK0_skl,join(sK1_skl,sK2_skl))=sK2_skl),
% 0.27/0.85 inference(forward_demodulation,[status(thm)],[f17,f31])).
% 0.27/0.85 fof(f47,plain,(
% 0.27/0.85 ![X0,X1]: (join(X0,join(X1,complement(join(X0,X1))))=top)),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f27,f17])).
% 0.27/0.85 fof(f48,plain,(
% 0.27/0.85 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,X1)))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f16,f17])).
% 0.27/0.85 fof(f51,plain,(
% 0.27/0.85 ![X0,X1]: (join(X0,join(complement(X0),X1))=join(top,X1))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f27,f17])).
% 0.27/0.85 fof(f83,plain,(
% 0.27/0.85 ![X0]: (meet(X0,complement(X0))=complement(top))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f27,f19])).
% 0.27/0.85 fof(f84,plain,(
% 0.27/0.85 ![X0,X1]: (meet(X0,X1)=complement(join(complement(X1),complement(X0))))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f16,f19])).
% 0.27/0.85 fof(f89,plain,(
% 0.27/0.85 ![X0,X1]: (top=join(join(complement(X0),complement(X1)),meet(X0,X1)))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f19,f27])).
% 0.27/0.85 fof(f90,plain,(
% 0.27/0.85 zero=complement(top)),
% 0.27/0.85 inference(forward_demodulation,[status(thm)],[f28,f83])).
% 0.27/0.85 fof(f91,plain,(
% 0.27/0.85 ![X0,X1]: (top=join(complement(X0),join(complement(X1),meet(X0,X1))))),
% 0.27/0.85 inference(forward_demodulation,[status(thm)],[f17,f89])).
% 0.27/0.85 fof(f92,plain,(
% 0.27/0.85 ![X0]: (meet(X0,top)=complement(join(complement(X0),zero)))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f90,f19])).
% 0.27/0.85 fof(f93,plain,(
% 0.27/0.85 ![X0]: (meet(top,X0)=complement(join(zero,complement(X0))))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f90,f19])).
% 0.27/0.85 fof(f100,plain,(
% 0.27/0.85 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X1,join(X2,X0)))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f16,f48])).
% 0.27/0.85 fof(f109,plain,(
% 0.27/0.85 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X1,join(X0,X2)))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f16,f48])).
% 0.27/0.85 fof(f123,plain,(
% 0.27/0.85 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X1,X0)))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f16,f48])).
% 0.27/0.85 fof(f392,plain,(
% 0.27/0.85 ![X0,X1]: (join(top,X0)=join(complement(X1),join(X0,X1)))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f27,f100])).
% 0.27/0.85 fof(f393,plain,(
% 0.27/0.85 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X0,join(X2,X1)))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f16,f100])).
% 0.27/0.85 fof(f635,plain,(
% 0.27/0.85 ![X0,X1]: (join(X0,top)=join(complement(X1),join(X1,X0)))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f27,f123])).
% 0.27/0.85 fof(f1625,plain,(
% 0.27/0.85 ![X0,X1]: (top=join(complement(X0),join(complement(X1),meet(X1,X0))))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f109,f91])).
% 0.27/0.85 fof(f1627,plain,(
% 0.27/0.85 ![X0,X1]: (top=join(complement(X0),join(meet(X1,X0),complement(X1))))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f48,f91])).
% 0.27/0.85 fof(f1778,plain,(
% 0.27/0.85 ![X0]: (X0=join(zero,complement(join(complement(X0),complement(X0)))))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f28,f40])).
% 0.27/0.85 fof(f1809,plain,(
% 0.27/0.85 ![X0]: (X0=join(zero,meet(X0,X0)))),
% 0.27/0.85 inference(forward_demodulation,[status(thm)],[f19,f1778])).
% 0.27/0.85 fof(f1818,plain,(
% 0.27/0.85 ![X0,X1]: (join(X0,X1)=join(zero,join(X1,meet(X0,X0))))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f1809,f393])).
% 0.27/0.85 fof(f1825,plain,(
% 0.27/0.85 ![X0,X1]: (join(zero,join(meet(X0,X0),X1))=join(X1,X0))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f1809,f48])).
% 0.27/0.85 fof(f1827,plain,(
% 0.27/0.85 ![X0,X1]: (join(zero,join(meet(X0,X0),X1))=join(X0,X1))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f1809,f17])).
% 0.27/0.85 fof(f2149,plain,(
% 0.27/0.85 ![X0]: (join(complement(join(zero,meet(X0,X0))),X0)=top)),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f1825,f47])).
% 0.27/0.85 fof(f2222,plain,(
% 0.27/0.85 ![X0]: (join(complement(X0),X0)=top)),
% 0.27/0.85 inference(forward_demodulation,[status(thm)],[f1809,f2149])).
% 0.27/0.85 fof(f2320,plain,(
% 0.27/0.85 ![X0]: (X0=join(meet(X0,X0),complement(top)))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f2222,f40])).
% 0.27/0.85 fof(f2362,plain,(
% 0.27/0.85 ![X0]: (X0=join(meet(X0,X0),zero))),
% 0.27/0.85 inference(forward_demodulation,[status(thm)],[f90,f2320])).
% 0.27/0.85 fof(f2478,plain,(
% 0.27/0.85 ![X0,X1]: (join(X0,meet(X1,X1))=join(X1,meet(X0,X0)))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f1818,f1827])).
% 0.27/0.85 fof(f2604,plain,(
% 0.27/0.85 ![X0,X1]: (X0=join(meet(X0,join(complement(complement(X0)),X1)),complement(join(top,X1))))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f51,f40])).
% 0.27/0.85 fof(f2685,plain,(
% 0.27/0.85 ![X0]: (X0=join(X0,meet(zero,zero)))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f1809,f2478])).
% 0.27/0.85 fof(f2790,plain,(
% 0.27/0.85 complement(meet(zero,zero))=top),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f2222,f2685])).
% 0.27/0.85 fof(f2798,plain,(
% 0.27/0.85 ![X0]: (X0=join(meet(zero,zero),X0))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f16,f2685])).
% 0.27/0.85 fof(f2803,plain,(
% 0.27/0.85 top=join(complement(zero),complement(zero))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f2685,f1625])).
% 0.27/0.85 fof(f2807,plain,(
% 0.27/0.85 ![X0]: (X0=join(meet(X0,meet(zero,zero)),complement(complement(X0))))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f2685,f40])).
% 0.27/0.85 fof(f2859,plain,(
% 0.27/0.85 meet(zero,zero)=complement(top)),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f2803,f19])).
% 0.27/0.85 fof(f2875,plain,(
% 0.27/0.85 ![X0]: (X0=join(X0,zero))),
% 0.27/0.85 inference(backward_demodulation,[status(thm)],[f2881,f2685])).
% 0.27/0.85 fof(f2878,plain,(
% 0.27/0.85 ![X0]: (X0=join(meet(X0,zero),complement(complement(X0))))),
% 0.27/0.85 inference(backward_demodulation,[status(thm)],[f2881,f2807])).
% 0.27/0.85 fof(f2879,plain,(
% 0.27/0.85 ![X0]: (X0=join(zero,X0))),
% 0.27/0.85 inference(backward_demodulation,[status(thm)],[f2881,f2798])).
% 0.27/0.85 fof(f2880,plain,(
% 0.27/0.85 complement(zero)=top),
% 0.27/0.85 inference(backward_demodulation,[status(thm)],[f2881,f2790])).
% 0.27/0.85 fof(f2881,plain,(
% 0.27/0.85 meet(zero,zero)=zero),
% 0.27/0.85 inference(forward_demodulation,[status(thm)],[f90,f2859])).
% 0.27/0.85 fof(f2889,plain,(
% 0.27/0.85 ![X0]: (X0=meet(X0,X0))),
% 0.27/0.85 inference(backward_demodulation,[status(thm)],[f2875,f2362])).
% 0.27/0.85 fof(f2899,plain,(
% 0.27/0.85 ![X0]: (meet(X0,top)=complement(complement(X0)))),
% 0.27/0.85 inference(backward_demodulation,[status(thm)],[f2875,f92])).
% 0.27/0.85 fof(f2934,plain,(
% 0.27/0.85 ![X0]: (meet(top,X0)=complement(complement(X0)))),
% 0.27/0.85 inference(backward_demodulation,[status(thm)],[f2879,f93])).
% 0.27/0.85 fof(f2980,plain,(
% 0.27/0.85 ![X0]: (X0=join(meet(X0,zero),meet(X0,top)))),
% 0.27/0.85 inference(backward_demodulation,[status(thm)],[f2899,f2878])).
% 0.27/0.85 fof(f2981,plain,(
% 0.27/0.85 ![X0,X1]: (X0=join(meet(X0,join(meet(X0,top),X1)),complement(join(top,X1))))),
% 0.27/0.85 inference(backward_demodulation,[status(thm)],[f2899,f2604])).
% 0.27/0.85 fof(f3028,plain,(
% 0.27/0.85 ![X0]: (top=join(complement(X0),join(X0,complement(X0))))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f2889,f1627])).
% 0.27/0.85 fof(f3029,plain,(
% 0.27/0.85 ![X0]: (top=join(complement(X0),join(complement(X0),X0)))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f2889,f1625])).
% 0.27/0.85 fof(f3033,plain,(
% 0.27/0.85 ![X0]: (top=join(complement(X0),top))),
% 0.27/0.85 inference(forward_demodulation,[status(thm)],[f635,f3028])).
% 0.27/0.85 fof(f3034,plain,(
% 0.27/0.85 ![X0]: (top=join(top,complement(X0)))),
% 0.27/0.85 inference(forward_demodulation,[status(thm)],[f392,f3029])).
% 0.27/0.85 fof(f3046,plain,(
% 0.27/0.85 ![X0]: (X0=join(meet(X0,zero),complement(complement(X0))))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f2875,f40])).
% 0.27/0.85 fof(f3077,plain,(
% 0.27/0.85 ![X0]: (X0=join(meet(X0,zero),meet(top,X0)))),
% 0.27/0.85 inference(forward_demodulation,[status(thm)],[f2934,f3046])).
% 0.27/0.85 fof(f3235,plain,(
% 0.27/0.85 ![X0]: (zero=join(meet(zero,X0),complement(join(top,X0))))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f2880,f40])).
% 0.27/0.85 fof(f3243,plain,(
% 0.27/0.85 ![X0]: (meet(X0,zero)=complement(join(complement(X0),top)))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f2880,f19])).
% 0.27/0.85 fof(f3244,plain,(
% 0.27/0.85 ![X0]: (meet(zero,X0)=complement(join(top,complement(X0))))),
% 0.27/0.85 inference(paramodulation,[status(thm)],[f2880,f19])).
% 0.27/0.85 fof(f3251,plain,(
% 0.27/0.85 ![X0]: (meet(X0,zero)=complement(top))),
% 0.27/0.85 inference(forward_demodulation,[status(thm)],[f3033,f3243])).
% 0.27/0.85 fof(f3254,plain,(
% 0.27/0.85 ![X0]: (X0=join(zero,meet(top,X0)))),
% 0.27/0.85 inference(backward_demodulation,[status(thm)],[f3256,f3077])).
% 0.27/0.85 fof(f3255,plain,(
% 0.27/0.85 ![X0]: (X0=join(zero,meet(X0,top)))),
% 0.27/0.85 inference(backward_demodulation,[status(thm)],[f3256,f2980])).
% 0.27/0.85 fof(f3256,plain,(
% 0.27/0.85 ![X0]: (meet(X0,zero)=zero)),
% 0.27/0.85 inference(forward_demodulation,[status(thm)],[f90,f3251])).
% 0.27/0.85 fof(f3257,plain,(
% 0.27/0.85 ![X0]: (meet(zero,X0)=complement(top))),
% 0.27/0.85 inference(forward_demodulation,[status(thm)],[f3034,f3244])).
% 0.27/0.85 fof(f3260,plain,(
% 0.27/0.85 ![X0]: (zero=join(zero,complement(join(top,X0))))),
% 0.27/0.85 inference(backward_demodulation,[status(thm)],[f3261,f3235])).
% 0.27/0.85 fof(f3261,plain,(
% 0.27/0.85 ![X0]: (meet(zero,X0)=zero)),
% 0.27/0.85 inference(forward_demodulation,[status(thm)],[f90,f3257])).
% 0.27/0.85 fof(f3264,plain,(
% 0.27/0.85 ![X0]: (X0=complement(complement(X0)))),
% 0.27/0.85 inference(backward_demodulation,[status(thm)],[f3266,f2934])).
% 0.27/0.85 fof(f3266,plain,(
% 0.27/0.85 ![X0]: (X0=meet(top,X0))),
% 0.27/0.85 inference(forward_demodulation,[status(thm)],[f2879,f3254])).
% 0.27/0.85 fof(f3269,plain,(
% 0.27/0.85 ![X0,X1]: (X0=join(meet(X0,join(X0,X1)),complement(join(top,X1))))),
% 0.27/0.85 inference(backward_demodulation,[status(thm)],[f3274,f2981])).
% 0.27/0.85 fof(f3274,plain,(
% 0.27/0.85 ![X0]: (X0=meet(X0,top))),
% 0.27/0.85 inference(forward_demodulation,[status(thm)],[f2879,f3255])).
% 0.27/0.85 fof(f3277,plain,(
% 0.27/0.85 ![X0]: (zero=complement(join(top,X0)))),
% 0.27/0.85 inference(forward_demodulation,[status(thm)],[f2879,f3260])).
% 0.27/0.85 fof(f3278,plain,(
% 0.27/0.86 ![X0,X1]: (X0=join(meet(X0,join(X0,X1)),zero))),
% 0.27/0.86 inference(forward_demodulation,[status(thm)],[f3277,f3269])).
% 0.27/0.86 fof(f3279,plain,(
% 0.27/0.86 ![X0,X1]: (X0=meet(X0,join(X0,X1)))),
% 0.27/0.86 inference(forward_demodulation,[status(thm)],[f2875,f3278])).
% 0.27/0.86 fof(f3312,plain,(
% 0.27/0.86 ![X0,X1]: (join(complement(X0),complement(X1))=complement(meet(X0,X1)))),
% 0.27/0.86 inference(paramodulation,[status(thm)],[f19,f3264])).
% 0.27/0.86 fof(f3323,plain,(
% 0.27/0.86 ![X0,X1]: (meet(X0,complement(X1))=complement(join(complement(X0),X1)))),
% 0.27/0.86 inference(paramodulation,[status(thm)],[f3264,f19])).
% 0.27/0.86 fof(f3343,plain,(
% 0.27/0.86 ![X0,X1]: (meet(X0,X1)=complement(complement(meet(X1,X0))))),
% 0.27/0.86 inference(backward_demodulation,[status(thm)],[f3312,f84])).
% 0.27/0.86 fof(f3345,plain,(
% 0.27/0.86 ![X0,X1]: (X0=join(meet(X0,X1),meet(X0,complement(X1))))),
% 0.27/0.86 inference(backward_demodulation,[status(thm)],[f3323,f40])).
% 0.27/0.86 fof(f3361,plain,(
% 0.27/0.86 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 0.27/0.86 inference(forward_demodulation,[status(thm)],[f3264,f3343])).
% 0.27/0.86 fof(f3516,plain,(
% 0.27/0.86 ![X0,X1]: (meet(X0,X1)=meet(meet(X0,X1),X0))),
% 0.27/0.86 inference(paramodulation,[status(thm)],[f3345,f3279])).
% 0.27/0.86 fof(f3548,plain,(
% 0.27/0.86 ![X0,X1]: (X0=meet(X0,join(X1,X0)))),
% 0.27/0.86 inference(paramodulation,[status(thm)],[f16,f3279])).
% 0.27/0.86 fof(f4065,plain,(
% 0.27/0.86 join(sK1_skl,sK2_skl)=meet(join(sK1_skl,sK2_skl),sK2_skl)),
% 0.27/0.86 inference(paramodulation,[status(thm)],[f41,f3548])).
% 0.27/0.86 fof(f4104,plain,(
% 0.27/0.86 ![X0,X1]: (meet(X0,X1)=meet(meet(X1,X0),X0))),
% 0.27/0.86 inference(paramodulation,[status(thm)],[f3361,f3516])).
% 0.27/0.86 fof(f4910,plain,(
% 0.27/0.86 ![X0,X1]: (meet(join(X0,X1),X1)=meet(X1,join(X0,X1)))),
% 0.27/0.86 inference(paramodulation,[status(thm)],[f3548,f4104])).
% 0.27/0.86 fof(f4935,plain,(
% 0.27/0.86 join(sK1_skl,sK2_skl)=sK2_skl),
% 0.27/0.86 inference(backward_demodulation,[status(thm)],[f4937,f4065])).
% 0.27/0.86 fof(f4937,plain,(
% 0.27/0.86 ![X0,X1]: (meet(join(X0,X1),X1)=X1)),
% 0.27/0.86 inference(forward_demodulation,[status(thm)],[f3548,f4910])).
% 0.27/0.86 fof(f4944,plain,(
% 0.27/0.86 join(sK0_skl,sK2_skl)=sK2_skl),
% 0.27/0.86 inference(backward_demodulation,[status(thm)],[f4935,f41])).
% 0.27/0.86 fof(f4957,plain,(
% 0.27/0.86 $false|sQ0_spl),
% 0.27/0.86 inference(forward_subsumption_resolution,[status(thm)],[f4944,f35])).
% 0.27/0.86 fof(f4958,plain,(
% 0.27/0.86 sQ0_spl),
% 0.27/0.86 inference(contradiction_clause,[status(thm)],[f4957])).
% 0.27/0.86 fof(f4965,plain,(
% 0.27/0.86 ~sK2_skl=sK2_skl|sQ1_spl),
% 0.27/0.86 inference(forward_demodulation,[status(thm)],[f4935,f38])).
% 0.27/0.86 fof(f4966,plain,(
% 0.27/0.86 $false|sQ1_spl),
% 0.27/0.86 inference(trivial_equality_resolution,[status(thm)],[f4965])).
% 0.27/0.86 fof(f4967,plain,(
% 0.27/0.86 sQ1_spl),
% 0.27/0.86 inference(contradiction_clause,[status(thm)],[f4966])).
% 0.27/0.86 fof(f4968,plain,(
% 0.27/0.86 $false),
% 0.27/0.86 inference(sat_refutation,[status(thm)],[f39,f4958,f4967])).
% 0.27/0.86 % SZS output end CNFRefutation for theBenchmark.p
% 0.27/0.90 % Elapsed time: 0.434652 seconds
% 0.27/0.90 % CPU time: 3.030660 seconds
% 0.27/0.90 % Total memory used: 84.769 MB
% 0.27/0.90 % Net memory used: 84.192 MB
%------------------------------------------------------------------------------