%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU345+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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:22:23 PM UTC 2026
% Result : Theorem 55.57s 7.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU345+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n006.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 06:13:57 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.46 % Drodi V4.1.1
% 55.57/7.56 % Refutation found
% 55.57/7.56 % SZS status Theorem for theBenchmark: Theorem is valid
% 55.57/7.56 % SZS output start CNFRefutation for theBenchmark
% 55.57/7.56 fof(f8,axiom,(
% 55.57/7.56 (! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) )),
% 55.57/7.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 55.57/7.56 fof(f12,axiom,(
% 55.57/7.56 (! [A] :( ( ~ empty_carrier(A)& meet_semilatt_str(A) )=> ( lower_bounded_semilattstr(A)<=> (? [B] :( element(B,the_carrier(A))& (! [C] :( element(C,the_carrier(A))=> ( meet(A,B,C) = B& meet(A,C,B) = B ) ) )) )) ) )),
% 55.57/7.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 55.57/7.56 fof(f13,axiom,(
% 55.57/7.56 (! [A] :( ( ~ empty_carrier(A)& meet_semilatt_str(A) )=> ( lower_bounded_semilattstr(A)=> (! [B] :( element(B,the_carrier(A))=> ( B = bottom_of_semilattstr(A)<=> (! [C] :( element(C,the_carrier(A))=> ( meet(A,B,C) = B& meet(A,C,B) = B ) ) )) ) )) ) )),
% 55.57/7.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 55.57/7.56 fof(f15,axiom,(
% 55.57/7.56 (! [A,B] :( ( strict_latt_str(B)& latt_str(B) )=> ( B = boole_lattice(A)<=> ( the_carrier(B) = powerset(A)& (! [C] :( element(C,powerset(A))=> (! [D] :( element(D,powerset(A))=> ( apply_binary(the_L_join(B),C,D) = subset_union2(A,C,D)& apply_binary(the_L_meet(B),C,D) = subset_intersection2(A,C,D) ) ) )) )) ) ) )),
% 55.57/7.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 55.57/7.56 fof(f22,axiom,(
% 55.57/7.56 (! [A] :( strict_latt_str(boole_lattice(A))& latt_str(boole_lattice(A)) ) )),
% 55.57/7.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 55.57/7.56 fof(f36,axiom,(
% 55.57/7.56 (! [A] :( ( ~ empty_carrier(A)& meet_semilatt_str(A) )=> element(bottom_of_semilattstr(A),the_carrier(A)) ) )),
% 55.57/7.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 55.57/7.56 fof(f41,axiom,(
% 55.57/7.56 (! [A] :( latt_str(A)=> ( meet_semilatt_str(A)& join_semilatt_str(A) ) ) )),
% 55.57/7.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 55.57/7.56 fof(f55,axiom,(
% 55.57/7.56 (! [A] :( ~ empty_carrier(boole_lattice(A))& strict_latt_str(boole_lattice(A)) ) )),
% 55.57/7.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 55.57/7.56 fof(f76,axiom,(
% 55.57/7.56 (? [A] : empty(A) )),
% 55.57/7.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 55.57/7.56 fof(f77,axiom,(
% 55.57/7.56 (! [A] :(? [B] :( element(B,powerset(A))& empty(B) ) ))),
% 55.57/7.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 55.57/7.56 fof(f91,axiom,(
% 55.57/7.56 (! [A,B] :( element(B,the_carrier(boole_lattice(A)))=> (! [C] :( element(C,the_carrier(boole_lattice(A)))=> ( join(boole_lattice(A),B,C) = set_union2(B,C)& meet(boole_lattice(A),B,C) = set_intersection2(B,C) ) ) )) )),
% 55.57/7.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 55.57/7.56 fof(f93,axiom,(
% 55.57/7.56 (! [A] : set_intersection2(A,empty_set) = empty_set )),
% 55.57/7.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 55.57/7.56 fof(f96,conjecture,(
% 55.57/7.56 (! [A] :( lower_bounded_semilattstr(boole_lattice(A))& bottom_of_semilattstr(boole_lattice(A)) = empty_set ) )),
% 55.57/7.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 55.57/7.56 fof(f97,negated_conjecture,(
% 55.57/7.56 ~((! [A] :( lower_bounded_semilattstr(boole_lattice(A))& bottom_of_semilattstr(boole_lattice(A)) = empty_set ) ))),
% 55.57/7.56 inference(negated_conjecture,[status(cth)],[f96])).
% 55.57/7.56 fof(f101,axiom,(
% 55.57/7.56 (! [A] :( empty(A)=> A = empty_set ) )),
% 55.57/7.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 55.57/7.56 fof(f124,plain,(
% 55.57/7.56 ![X0,X1]: (set_intersection2(X0,X1)=set_intersection2(X1,X0))),
% 55.57/7.56 inference(cnf_transformation,[status(thm)],[f8])).
% 55.57/7.56 fof(f131,plain,(
% 55.57/7.56 ![A]: ((empty_carrier(A)|~meet_semilatt_str(A))|(lower_bounded_semilattstr(A)<=>(?[B]: (element(B,the_carrier(A))&(![C]: (~element(C,the_carrier(A))|(meet(A,B,C)=B&meet(A,C,B)=B)))))))),
% 55.57/7.56 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 55.57/7.56 fof(f132,plain,(
% 55.57/7.56 ![A]: ((empty_carrier(A)|~meet_semilatt_str(A))|((~lower_bounded_semilattstr(A)|(?[B]: (element(B,the_carrier(A))&(![C]: (~element(C,the_carrier(A))|(meet(A,B,C)=B&meet(A,C,B)=B))))))&(lower_bounded_semilattstr(A)|(![B]: (~element(B,the_carrier(A))|(?[C]: (element(C,the_carrier(A))&(~meet(A,B,C)=B|~meet(A,C,B)=B))))))))),
% 55.57/7.56 inference(NNF_transformation,[status(thm)],[f131])).
% 55.57/7.56 fof(f133,plain,(
% 55.57/7.56 ![A]: ((empty_carrier(A)|~meet_semilatt_str(A))|((~lower_bounded_semilattstr(A)|(element(sK0_skl(A),the_carrier(A))&(![C]: (~element(C,the_carrier(A))|(meet(A,sK0_skl(A),C)=sK0_skl(A)&meet(A,C,sK0_skl(A))=sK0_skl(A))))))&(lower_bounded_semilattstr(A)|(![B]: (~element(B,the_carrier(A))|(element(sK1_skl(B,A),the_carrier(A))&(~meet(A,B,sK1_skl(B,A))=B|~meet(A,sK1_skl(B,A),B)=B)))))))),
% 55.57/7.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(B,sK0_skl(A)),skolemize(C,sK1_skl(B,A))],[f132])).
% 55.57/7.56 fof(f137,plain,(
% 55.57/7.56 ![X0,X1]: (empty_carrier(X0)|~meet_semilatt_str(X0)|lower_bounded_semilattstr(X0)|~element(X1,the_carrier(X0))|element(sK1_skl(X1,X0),the_carrier(X0)))),
% 55.57/7.56 inference(cnf_transformation,[status(thm)],[f133])).
% 55.57/7.56 fof(f138,plain,(
% 55.57/7.56 ![X0,X1]: (empty_carrier(X0)|~meet_semilatt_str(X0)|lower_bounded_semilattstr(X0)|~element(X1,the_carrier(X0))|~meet(X0,X1,sK1_skl(X1,X0))=X1|~meet(X0,sK1_skl(X1,X0),X1)=X1)),
% 55.57/7.56 inference(cnf_transformation,[status(thm)],[f133])).
% 55.57/7.56 fof(f139,plain,(
% 55.57/7.56 ![A]: ((empty_carrier(A)|~meet_semilatt_str(A))|(~lower_bounded_semilattstr(A)|(![B]: (~element(B,the_carrier(A))|(B=bottom_of_semilattstr(A)<=>(![C]: (~element(C,the_carrier(A))|(meet(A,B,C)=B&meet(A,C,B)=B))))))))),
% 55.57/7.56 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 55.57/7.56 fof(f140,plain,(
% 55.57/7.56 ![A]: ((empty_carrier(A)|~meet_semilatt_str(A))|(~lower_bounded_semilattstr(A)|(![B]: (~element(B,the_carrier(A))|((~B=bottom_of_semilattstr(A)|(![C]: (~element(C,the_carrier(A))|(meet(A,B,C)=B&meet(A,C,B)=B))))&(B=bottom_of_semilattstr(A)|(?[C]: (element(C,the_carrier(A))&(~meet(A,B,C)=B|~meet(A,C,B)=B)))))))))),
% 55.57/7.56 inference(NNF_transformation,[status(thm)],[f139])).
% 55.57/7.56 fof(f141,plain,(
% 55.57/7.56 ![A]: ((empty_carrier(A)|~meet_semilatt_str(A))|(~lower_bounded_semilattstr(A)|(![B]: (~element(B,the_carrier(A))|((~B=bottom_of_semilattstr(A)|(![C]: (~element(C,the_carrier(A))|(meet(A,B,C)=B&meet(A,C,B)=B))))&(B=bottom_of_semilattstr(A)|(element(sK2_skl(B,A),the_carrier(A))&(~meet(A,B,sK2_skl(B,A))=B|~meet(A,sK2_skl(B,A),B)=B))))))))),
% 55.57/7.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(C,sK2_skl(B,A))],[f140])).
% 55.57/7.56 fof(f143,plain,(
% 55.57/7.56 ![X0,X1,X2]: (empty_carrier(X0)|~meet_semilatt_str(X0)|~lower_bounded_semilattstr(X0)|~element(X1,the_carrier(X0))|~X1=bottom_of_semilattstr(X0)|~element(X2,the_carrier(X0))|meet(X0,X2,X1)=X1)),
% 55.57/7.56 inference(cnf_transformation,[status(thm)],[f141])).
% 55.57/7.56 fof(f148,plain,(
% 55.57/7.56 ![A,B]: ((~strict_latt_str(B)|~latt_str(B))|(B=boole_lattice(A)<=>(the_carrier(B)=powerset(A)&(![C]: (~element(C,powerset(A))|(![D]: (~element(D,powerset(A))|(apply_binary(the_L_join(B),C,D)=subset_union2(A,C,D)&apply_binary(the_L_meet(B),C,D)=subset_intersection2(A,C,D)))))))))),
% 55.57/7.56 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 55.57/7.56 fof(f149,plain,(
% 55.57/7.56 ![A,B]: ((~strict_latt_str(B)|~latt_str(B))|((~B=boole_lattice(A)|(the_carrier(B)=powerset(A)&(![C]: (~element(C,powerset(A))|(![D]: (~element(D,powerset(A))|(apply_binary(the_L_join(B),C,D)=subset_union2(A,C,D)&apply_binary(the_L_meet(B),C,D)=subset_intersection2(A,C,D))))))))&(B=boole_lattice(A)|(~the_carrier(B)=powerset(A)|(?[C]: (element(C,powerset(A))&(?[D]: (element(D,powerset(A))&(~apply_binary(the_L_join(B),C,D)=subset_union2(A,C,D)|~apply_binary(the_L_meet(B),C,D)=subset_intersection2(A,C,D))))))))))),
% 55.57/7.56 inference(NNF_transformation,[status(thm)],[f148])).
% 55.57/7.56 fof(f150,plain,(
% 55.57/7.56 ![B]: ((~strict_latt_str(B)|~latt_str(B))|((![A]: (~B=boole_lattice(A)|(the_carrier(B)=powerset(A)&(![C]: (~element(C,powerset(A))|(![D]: (~element(D,powerset(A))|(apply_binary(the_L_join(B),C,D)=subset_union2(A,C,D)&apply_binary(the_L_meet(B),C,D)=subset_intersection2(A,C,D)))))))))&(![A]: (B=boole_lattice(A)|(~the_carrier(B)=powerset(A)|(?[C]: (element(C,powerset(A))&(?[D]: (element(D,powerset(A))&(~apply_binary(the_L_join(B),C,D)=subset_union2(A,C,D)|~apply_binary(the_L_meet(B),C,D)=subset_intersection2(A,C,D)))))))))))),
% 55.57/7.56 inference(miniscoping,[status(thm)],[f149])).
% 55.57/7.56 fof(f151,plain,(
% 55.57/7.56 ![B]: ((~strict_latt_str(B)|~latt_str(B))|((![A]: (~B=boole_lattice(A)|(the_carrier(B)=powerset(A)&(![C]: (~element(C,powerset(A))|(![D]: (~element(D,powerset(A))|(apply_binary(the_L_join(B),C,D)=subset_union2(A,C,D)&apply_binary(the_L_meet(B),C,D)=subset_intersection2(A,C,D)))))))))&(![A]: (B=boole_lattice(A)|(~the_carrier(B)=powerset(A)|(element(sK3_skl(A,B),powerset(A))&(element(sK4_skl(A,B),powerset(A))&(~apply_binary(the_L_join(B),sK3_skl(A,B),sK4_skl(A,B))=subset_union2(A,sK3_skl(A,B),sK4_skl(A,B))|~apply_binary(the_L_meet(B),sK3_skl(A,B),sK4_skl(A,B))=subset_intersection2(A,sK3_skl(A,B),sK4_skl(A,B))))))))))),
% 55.57/7.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl,sK4_skl]),skolemize(C,sK3_skl(A,B)),skolemize(D,sK4_skl(A,B))],[f150])).
% 55.57/7.56 fof(f152,plain,(
% 55.57/7.56 ![X0,X1]: (~strict_latt_str(X0)|~latt_str(X0)|~X0=boole_lattice(X1)|the_carrier(X0)=powerset(X1))),
% 55.57/7.56 inference(cnf_transformation,[status(thm)],[f151])).
% 55.57/7.56 fof(f166,plain,(
% 55.57/7.56 (![A]: strict_latt_str(boole_lattice(A)))&(![A]: latt_str(boole_lattice(A)))),
% 55.57/7.56 inference(miniscoping,[status(thm)],[f22])).
% 55.57/7.56 fof(f167,plain,(
% 55.57/7.56 ![X0]: (strict_latt_str(boole_lattice(X0)))),
% 55.57/7.56 inference(cnf_transformation,[status(thm)],[f166])).
% 55.57/7.56 fof(f168,plain,(
% 55.57/7.56 ![X0]: (latt_str(boole_lattice(X0)))),
% 55.57/7.56 inference(cnf_transformation,[status(thm)],[f166])).
% 55.57/7.56 fof(f179,plain,(
% 55.57/7.56 ![A]: ((empty_carrier(A)|~meet_semilatt_str(A))|element(bottom_of_semilattstr(A),the_carrier(A)))),
% 55.57/7.56 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 55.57/7.56 fof(f180,plain,(
% 55.57/7.56 ![X0]: (empty_carrier(X0)|~meet_semilatt_str(X0)|element(bottom_of_semilattstr(X0),the_carrier(X0)))),
% 55.57/7.56 inference(cnf_transformation,[status(thm)],[f179])).
% 55.57/7.56 fof(f187,plain,(
% 55.57/7.56 ![A]: (~latt_str(A)|(meet_semilatt_str(A)&join_semilatt_str(A)))),
% 55.57/7.56 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 55.57/7.56 fof(f188,plain,(
% 55.57/7.56 ![X0]: (~latt_str(X0)|meet_semilatt_str(X0))),
% 55.57/7.56 inference(cnf_transformation,[status(thm)],[f187])).
% 55.57/7.56 fof(f214,plain,(
% 55.57/7.56 (![A]: ~empty_carrier(boole_lattice(A)))&(![A]: strict_latt_str(boole_lattice(A)))),
% 55.57/7.56 inference(miniscoping,[status(thm)],[f55])).
% 55.57/7.56 fof(f215,plain,(
% 55.57/7.56 ![X0]: (~empty_carrier(boole_lattice(X0)))),
% 55.57/7.56 inference(cnf_transformation,[status(thm)],[f214])).
% 55.57/7.56 fof(f286,plain,(
% 55.57/7.56 empty(sK13_skl)),
% 55.57/7.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(A,sK13_skl)],[f76])).
% 55.57/7.56 fof(f287,plain,(
% 55.57/7.56 empty(sK13_skl)),
% 55.57/7.56 inference(cnf_transformation,[status(thm)],[f286])).
% 55.57/7.56 fof(f288,plain,(
% 55.57/7.56 ![A]: (element(sK14_skl(A),powerset(A))&empty(sK14_skl(A)))),
% 55.57/7.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(B,sK14_skl(A))],[f77])).
% 55.57/7.56 fof(f289,plain,(
% 55.57/7.56 ![X0]: (element(sK14_skl(X0),powerset(X0)))),
% 55.57/7.56 inference(cnf_transformation,[status(thm)],[f288])).
% 55.57/7.56 fof(f290,plain,(
% 55.57/7.56 ![X0]: (empty(sK14_skl(X0)))),
% 55.57/7.56 inference(cnf_transformation,[status(thm)],[f288])).
% 55.57/7.56 fof(f333,plain,(
% 55.57/7.56 ![A,B]: (~element(B,the_carrier(boole_lattice(A)))|(![C]: (~element(C,the_carrier(boole_lattice(A)))|(join(boole_lattice(A),B,C)=set_union2(B,C)&meet(boole_lattice(A),B,C)=set_intersection2(B,C)))))),
% 55.57/7.56 inference(pre_NNF_transformation,[status(thm)],[f91])).
% 55.57/7.56 fof(f335,plain,(
% 55.57/7.56 ![X0,X1,X2]: (~element(X0,the_carrier(boole_lattice(X1)))|~element(X2,the_carrier(boole_lattice(X1)))|meet(boole_lattice(X1),X0,X2)=set_intersection2(X0,X2))),
% 55.57/7.56 inference(cnf_transformation,[status(thm)],[f333])).
% 55.57/7.56 fof(f338,plain,(
% 55.57/7.56 ![X0]: (set_intersection2(X0,empty_set)=empty_set)),
% 55.57/7.56 inference(cnf_transformation,[status(thm)],[f93])).
% 55.57/7.56 fof(f342,plain,(
% 55.57/7.56 (?[A]: (~lower_bounded_semilattstr(boole_lattice(A))|~bottom_of_semilattstr(boole_lattice(A))=empty_set))),
% 55.57/7.56 inference(pre_NNF_transformation,[status(thm)],[f97])).
% 55.57/7.56 fof(f343,plain,(
% 55.57/7.56 (?[A]: ~lower_bounded_semilattstr(boole_lattice(A)))|(?[A]: ~bottom_of_semilattstr(boole_lattice(A))=empty_set)),
% 55.57/7.56 inference(miniscoping,[status(thm)],[f342])).
% 55.57/7.56 fof(f344,plain,(
% 55.57/7.56 ~lower_bounded_semilattstr(boole_lattice(sK21_skl))|~bottom_of_semilattstr(boole_lattice(sK22_skl))=empty_set),
% 55.57/7.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl,sK22_skl]),skolemize(A,sK21_skl),skolemize(A,sK22_skl)],[f343])).
% 55.57/7.56 fof(f345,plain,(
% 55.57/7.56 ~lower_bounded_semilattstr(boole_lattice(sK21_skl))|~bottom_of_semilattstr(boole_lattice(sK22_skl))=empty_set),
% 55.57/7.56 inference(cnf_transformation,[status(thm)],[f344])).
% 55.57/7.56 fof(f356,plain,(
% 55.57/7.56 ![A]: (~empty(A)|A=empty_set)),
% 55.57/7.56 inference(pre_NNF_transformation,[status(thm)],[f101])).
% 55.57/7.56 fof(f357,plain,(
% 55.57/7.56 ![X0]: (~empty(X0)|X0=empty_set)),
% 55.57/7.56 inference(cnf_transformation,[status(thm)],[f356])).
% 55.57/7.56 fof(f364,definition,(
% 55.57/7.56 sQ0_spl <=> (lower_bounded_semilattstr(boole_lattice(sK21_skl)))),
% 55.57/7.56 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 55.57/7.56 fof(f366,plain,(
% 55.57/7.56 ~lower_bounded_semilattstr(boole_lattice(sK21_skl))|sQ0_spl),
% 55.57/7.56 inference(component_clause,[status(thm)],[f364])).
% 55.57/7.56 fof(f367,definition,(
% 55.57/7.56 sQ1_spl <=> (bottom_of_semilattstr(boole_lattice(sK22_skl))=empty_set)),
% 55.57/7.56 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 55.57/7.56 fof(f369,plain,(
% 55.57/7.56 ~bottom_of_semilattstr(boole_lattice(sK22_skl))=empty_set|sQ1_spl),
% 55.57/7.56 inference(component_clause,[status(thm)],[f367])).
% 55.57/7.56 fof(f370,plain,(
% 55.57/7.56 ~sQ0_spl|~sQ1_spl),
% 55.57/7.56 inference(split_clause,[status(thm)],[f345,f364,f367])).
% 55.57/7.56 fof(f372,plain,(
% 55.57/7.56 ![X0,X1]: (empty_carrier(X0)|~meet_semilatt_str(X0)|~lower_bounded_semilattstr(X0)|~element(bottom_of_semilattstr(X0),the_carrier(X0))|~element(X1,the_carrier(X0))|meet(X0,X1,bottom_of_semilattstr(X0))=bottom_of_semilattstr(X0))),
% 55.57/7.56 inference(destructive_equality_resolution,[status(thm)],[f143])).
% 55.57/7.56 fof(f373,plain,(
% 55.57/7.56 ![X0]: (~strict_latt_str(boole_lattice(X0))|~latt_str(boole_lattice(X0))|the_carrier(boole_lattice(X0))=powerset(X0))),
% 55.57/7.56 inference(destructive_equality_resolution,[status(thm)],[f152])).
% 55.57/7.56 fof(f378,plain,(
% 55.57/7.56 ![X0]: (~latt_str(boole_lattice(X0))|the_carrier(boole_lattice(X0))=powerset(X0))),
% 55.57/7.56 inference(backward_subsumption_resolution,[status(thm)],[f373,f167])).
% 55.57/7.56 fof(f379,plain,(
% 55.57/7.56 ![X0,X1]: (empty_carrier(X0)|~meet_semilatt_str(X0)|~lower_bounded_semilattstr(X0)|~element(X1,the_carrier(X0))|meet(X0,X1,bottom_of_semilattstr(X0))=bottom_of_semilattstr(X0))),
% 55.57/7.56 inference(backward_subsumption_resolution,[status(thm)],[f372,f180])).
% 55.57/7.56 fof(f383,plain,(
% 55.57/7.56 ![X0,X1,X2]: (~element(X0,the_carrier(boole_lattice(X1)))|~element(X2,powerset(X1))|meet(boole_lattice(X1),X0,X2)=set_intersection2(X0,X2))),
% 55.57/7.56 inference(backward_demodulation,[status(thm)],[f385,f335])).
% 55.57/7.56 fof(f385,plain,(
% 55.57/7.56 ![X0]: (the_carrier(boole_lattice(X0))=powerset(X0))),
% 55.57/7.56 inference(forward_subsumption_resolution,[status(thm)],[f378,f168])).
% 55.57/7.56 fof(f386,plain,(
% 55.57/7.56 ![X0,X1,X2]: (~element(X0,powerset(X1))|~element(X2,powerset(X1))|meet(boole_lattice(X1),X0,X2)=set_intersection2(X0,X2))),
% 55.57/7.56 inference(forward_demodulation,[status(thm)],[f385,f383])).
% 55.57/7.56 fof(f397,plain,(
% 55.57/7.56 sK13_skl=empty_set),
% 55.57/7.56 inference(resolution,[status(thm)],[f287,f357])).
% 55.57/7.56 fof(f398,plain,(
% 55.57/7.56 ![X0]: (~empty(X0)|X0=sK13_skl)),
% 55.57/7.56 inference(backward_demodulation,[status(thm)],[f397,f357])).
% 55.57/7.56 fof(f402,plain,(
% 55.57/7.56 ![X0]: (set_intersection2(X0,empty_set)=sK13_skl)),
% 55.57/7.56 inference(backward_demodulation,[status(thm)],[f397,f338])).
% 55.57/7.56 fof(f403,plain,(
% 55.57/7.56 ![X0]: (set_intersection2(X0,sK13_skl)=sK13_skl)),
% 55.57/7.56 inference(forward_demodulation,[status(thm)],[f397,f402])).
% 55.57/7.56 fof(f433,plain,(
% 55.57/7.56 ![X0]: (sK13_skl=set_intersection2(sK13_skl,X0))),
% 55.57/7.56 inference(paramodulation,[status(thm)],[f403,f124])).
% 55.57/7.56 fof(f588,plain,(
% 55.57/7.56 ![X0]: (meet_semilatt_str(boole_lattice(X0)))),
% 55.57/7.56 inference(resolution,[status(thm)],[f188,f168])).
% 55.57/7.56 fof(f1576,plain,(
% 55.57/7.56 ![X0]: (sK14_skl(X0)=sK13_skl)),
% 55.57/7.56 inference(resolution,[status(thm)],[f290,f398])).
% 55.57/7.56 fof(f1578,plain,(
% 55.57/7.56 ![X0]: (element(sK13_skl,powerset(X0)))),
% 55.57/7.56 inference(backward_demodulation,[status(thm)],[f1576,f289])).
% 55.57/7.56 fof(f1703,plain,(
% 55.57/7.56 ![X0]: (empty_carrier(boole_lattice(X0))|element(bottom_of_semilattstr(boole_lattice(X0)),the_carrier(boole_lattice(X0))))),
% 55.57/7.56 inference(resolution,[status(thm)],[f588,f180])).
% 55.57/7.56 fof(f1710,plain,(
% 55.57/7.56 ![X0]: (empty_carrier(boole_lattice(X0))|element(bottom_of_semilattstr(boole_lattice(X0)),powerset(X0)))),
% 55.57/7.56 inference(forward_demodulation,[status(thm)],[f385,f1703])).
% 55.57/7.56 fof(f1711,plain,(
% 55.57/7.56 ![X0]: (element(bottom_of_semilattstr(boole_lattice(X0)),powerset(X0)))),
% 55.57/7.56 inference(forward_subsumption_resolution,[status(thm)],[f1710,f215])).
% 55.57/7.56 fof(f3729,plain,(
% 55.57/7.56 ![X0,X1]: (empty_carrier(boole_lattice(X0))|~meet_semilatt_str(boole_lattice(X0))|lower_bounded_semilattstr(boole_lattice(X0))|~element(X1,powerset(X0))|~meet(boole_lattice(X0),X1,sK1_skl(X1,boole_lattice(X0)))=X1|~meet(boole_lattice(X0),sK1_skl(X1,boole_lattice(X0)),X1)=X1)),
% 55.57/7.56 inference(paramodulation,[status(thm)],[f385,f138])).
% 55.57/7.56 fof(f3730,plain,(
% 55.57/7.56 ![X0,X1]: (empty_carrier(boole_lattice(X0))|~meet_semilatt_str(boole_lattice(X0))|lower_bounded_semilattstr(boole_lattice(X0))|~element(X1,powerset(X0))|element(sK1_skl(X1,boole_lattice(X0)),the_carrier(boole_lattice(X0))))),
% 55.57/7.56 inference(paramodulation,[status(thm)],[f385,f137])).
% 55.57/7.56 fof(f3736,plain,(
% 55.57/7.56 ![X0,X1]: (empty_carrier(boole_lattice(X0))|~meet_semilatt_str(boole_lattice(X0))|~lower_bounded_semilattstr(boole_lattice(X0))|~element(X1,powerset(X0))|meet(boole_lattice(X0),X1,bottom_of_semilattstr(boole_lattice(X0)))=bottom_of_semilattstr(boole_lattice(X0)))),
% 55.57/7.56 inference(paramodulation,[status(thm)],[f385,f379])).
% 55.57/7.56 fof(f3776,plain,(
% 55.57/7.56 ![X0,X1]: (~meet_semilatt_str(boole_lattice(X0))|lower_bounded_semilattstr(boole_lattice(X0))|~element(X1,powerset(X0))|~meet(boole_lattice(X0),X1,sK1_skl(X1,boole_lattice(X0)))=X1|~meet(boole_lattice(X0),sK1_skl(X1,boole_lattice(X0)),X1)=X1)),
% 55.57/7.56 inference(forward_subsumption_resolution,[status(thm)],[f3729,f215])).
% 55.57/7.56 fof(f3777,plain,(
% 55.57/7.56 ![X0,X1]: (empty_carrier(boole_lattice(X0))|~meet_semilatt_str(boole_lattice(X0))|lower_bounded_semilattstr(boole_lattice(X0))|~element(X1,powerset(X0))|element(sK1_skl(X1,boole_lattice(X0)),powerset(X0)))),
% 55.57/7.56 inference(forward_demodulation,[status(thm)],[f385,f3730])).
% 55.57/7.56 fof(f3778,plain,(
% 55.57/7.56 ![X0,X1]: (~meet_semilatt_str(boole_lattice(X0))|lower_bounded_semilattstr(boole_lattice(X0))|~element(X1,powerset(X0))|element(sK1_skl(X1,boole_lattice(X0)),powerset(X0)))),
% 55.57/7.56 inference(forward_subsumption_resolution,[status(thm)],[f3777,f215])).
% 55.57/7.56 fof(f3785,plain,(
% 55.57/7.56 ![X0,X1]: (~meet_semilatt_str(boole_lattice(X0))|~lower_bounded_semilattstr(boole_lattice(X0))|~element(X1,powerset(X0))|meet(boole_lattice(X0),X1,bottom_of_semilattstr(boole_lattice(X0)))=bottom_of_semilattstr(boole_lattice(X0)))),
% 55.57/7.56 inference(forward_subsumption_resolution,[status(thm)],[f3736,f215])).
% 55.57/7.56 fof(f3789,plain,(
% 55.57/7.56 ![X0,X1]: (~element(X0,powerset(X1))|meet(boole_lattice(X1),sK13_skl,X0)=set_intersection2(sK13_skl,X0))),
% 55.57/7.56 inference(resolution,[status(thm)],[f386,f1578])).
% 55.57/7.56 fof(f3793,plain,(
% 55.57/7.56 ![X0,X1]: (~element(X0,powerset(X1))|meet(boole_lattice(X1),X0,sK13_skl)=set_intersection2(X0,sK13_skl))),
% 55.57/7.56 inference(resolution,[status(thm)],[f386,f1578])).
% 55.57/7.56 fof(f3797,plain,(
% 55.57/7.56 ![X0,X1]: (~element(X0,powerset(X1))|meet(boole_lattice(X1),sK13_skl,X0)=sK13_skl)),
% 55.57/7.56 inference(forward_demodulation,[status(thm)],[f433,f3789])).
% 55.57/7.56 fof(f3799,plain,(
% 55.57/7.56 ![X0,X1]: (~element(X0,powerset(X1))|meet(boole_lattice(X1),X0,sK13_skl)=sK13_skl)),
% 55.57/7.56 inference(forward_demodulation,[status(thm)],[f403,f3793])).
% 55.57/7.56 fof(f4129,plain,(
% 55.57/7.56 ![X0]: (~meet_semilatt_str(boole_lattice(X0))|lower_bounded_semilattstr(boole_lattice(X0))|~meet(boole_lattice(X0),sK13_skl,sK1_skl(sK13_skl,boole_lattice(X0)))=sK13_skl|~meet(boole_lattice(X0),sK1_skl(sK13_skl,boole_lattice(X0)),sK13_skl)=sK13_skl)),
% 55.57/7.56 inference(resolution,[status(thm)],[f3776,f1578])).
% 55.57/7.56 fof(f4133,plain,(
% 55.57/7.56 ![X0]: (lower_bounded_semilattstr(boole_lattice(X0))|~meet(boole_lattice(X0),sK13_skl,sK1_skl(sK13_skl,boole_lattice(X0)))=sK13_skl|~meet(boole_lattice(X0),sK1_skl(sK13_skl,boole_lattice(X0)),sK13_skl)=sK13_skl)),
% 55.57/7.56 inference(forward_subsumption_resolution,[status(thm)],[f4129,f588])).
% 55.57/7.56 fof(f4351,plain,(
% 55.57/7.56 ![X0]: (~meet_semilatt_str(boole_lattice(X0))|lower_bounded_semilattstr(boole_lattice(X0))|element(sK1_skl(sK13_skl,boole_lattice(X0)),powerset(X0)))),
% 55.57/7.56 inference(resolution,[status(thm)],[f3778,f1578])).
% 55.57/7.56 fof(f4356,plain,(
% 55.57/7.56 ![X0]: (lower_bounded_semilattstr(boole_lattice(X0))|element(sK1_skl(sK13_skl,boole_lattice(X0)),powerset(X0)))),
% 55.57/7.56 inference(forward_subsumption_resolution,[status(thm)],[f4351,f588])).
% 55.57/7.56 fof(f4650,plain,(
% 55.57/7.56 ![X0]: (~meet_semilatt_str(boole_lattice(X0))|~lower_bounded_semilattstr(boole_lattice(X0))|meet(boole_lattice(X0),sK13_skl,bottom_of_semilattstr(boole_lattice(X0)))=bottom_of_semilattstr(boole_lattice(X0)))),
% 32.15/7.65 inference(resolution,[status(thm)],[f3785,f1578])).
% 32.15/7.65 fof(f4655,plain,(
% 32.15/7.65 ![X0]: (~lower_bounded_semilattstr(boole_lattice(X0))|meet(boole_lattice(X0),sK13_skl,bottom_of_semilattstr(boole_lattice(X0)))=bottom_of_semilattstr(boole_lattice(X0)))),
% 32.15/7.65 inference(forward_subsumption_resolution,[status(thm)],[f4650,f588])).
% 32.15/7.65 fof(f4693,plain,(
% 32.15/7.65 ![X0]: (meet(boole_lattice(X0),sK13_skl,bottom_of_semilattstr(boole_lattice(X0)))=sK13_skl)),
% 32.15/7.65 inference(resolution,[status(thm)],[f3797,f1711])).
% 32.15/7.65 fof(f4697,plain,(
% 32.15/7.65 ![X0]: (~lower_bounded_semilattstr(boole_lattice(X0))|sK13_skl=bottom_of_semilattstr(boole_lattice(X0)))),
% 32.15/7.65 inference(backward_demodulation,[status(thm)],[f4693,f4655])).
% 32.15/7.65 fof(f8610,plain,(
% 32.15/7.65 ~bottom_of_semilattstr(boole_lattice(sK22_skl))=sK13_skl|sQ1_spl),
% 32.15/7.65 inference(forward_demodulation,[status(thm)],[f397,f369])).
% 32.15/7.65 fof(f14047,plain,(
% 32.15/7.65 ![X0]: (lower_bounded_semilattstr(boole_lattice(X0))|meet(boole_lattice(X0),sK1_skl(sK13_skl,boole_lattice(X0)),sK13_skl)=sK13_skl)),
% 32.15/7.65 inference(resolution,[status(thm)],[f4356,f3799])).
% 32.15/7.65 fof(f14048,plain,(
% 32.15/7.65 ![X0]: (lower_bounded_semilattstr(boole_lattice(X0))|meet(boole_lattice(X0),sK13_skl,sK1_skl(sK13_skl,boole_lattice(X0)))=sK13_skl)),
% 32.15/7.65 inference(resolution,[status(thm)],[f4356,f3797])).
% 32.15/7.65 fof(f14177,plain,(
% 32.15/7.65 ![X0]: (lower_bounded_semilattstr(boole_lattice(X0))|~meet(boole_lattice(X0),sK13_skl,sK1_skl(sK13_skl,boole_lattice(X0)))=sK13_skl)),
% 32.15/7.65 inference(backward_subsumption_resolution,[status(thm)],[f4133,f14047])).
% 32.15/7.65 fof(f14243,plain,(
% 32.15/7.65 $false|sQ0_spl),
% 32.15/7.65 inference(backward_subsumption_resolution,[status(thm)],[f366,f14279])).
% 32.15/7.65 fof(f14248,plain,(
% 32.15/7.65 ![X0]: (sK13_skl=bottom_of_semilattstr(boole_lattice(X0)))),
% 32.15/7.65 inference(backward_subsumption_resolution,[status(thm)],[f4697,f14279])).
% 32.15/7.65 fof(f14279,plain,(
% 32.15/7.65 ![X0]: (lower_bounded_semilattstr(boole_lattice(X0)))),
% 32.15/7.65 inference(forward_subsumption_resolution,[status(thm)],[f14177,f14048])).
% 32.15/7.65 fof(f14290,plain,(
% 32.15/7.65 sQ0_spl),
% 32.15/7.65 inference(contradiction_clause,[status(thm)],[f14243])).
% 32.15/7.65 fof(f14291,plain,(
% 32.15/7.65 ~sK13_skl=sK13_skl|sQ1_spl),
% 32.15/7.65 inference(backward_demodulation,[status(thm)],[f14248,f8610])).
% 32.15/7.65 fof(f14934,plain,(
% 32.15/7.65 $false|sQ1_spl),
% 32.15/7.65 inference(trivial_equality_resolution,[status(thm)],[f14291])).
% 32.15/7.65 fof(f14935,plain,(
% 32.15/7.65 sQ1_spl),
% 32.15/7.65 inference(contradiction_clause,[status(thm)],[f14934])).
% 32.15/7.65 fof(f14936,plain,(
% 32.15/7.65 $false),
% 32.15/7.65 inference(sat_refutation,[status(thm)],[f370,f14290,f14935])).
% 32.15/7.65 % SZS output end CNFRefutation for theBenchmark.p
% 32.15/7.67 % Elapsed time: 7.214708 seconds
% 32.15/7.67 % CPU time: 56.429486 seconds
% 32.15/7.67 % Total memory used: 462.925 MB
% 32.15/7.67 % Net memory used: 446.625 MB
%------------------------------------------------------------------------------