%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU344+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 : 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:22:23 PM UTC 2026
% Result : Theorem 0.28s 0.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU344+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.17/0.44 % Computer : n019.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Mon Sep 21 06:13:49 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.46 % Drodi V4.1.1
% 0.28/0.59 % Refutation found
% 0.28/0.59 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.28/0.59 % SZS output start CNFRefutation for theBenchmark
% 0.28/0.59 fof(f1,axiom,(
% 0.28/0.59 (! [A] :( latt_str(A)=> ( strict_latt_str(A)=> A = latt_str_of(the_carrier(A),the_L_join(A),the_L_meet(A)) ) ) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f2,axiom,(
% 0.28/0.59 (! [A,B] :( in(A,B)=> ~ in(B,A) ) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f5,axiom,(
% 0.28/0.59 (! [A,B] : set_union2(A,B) = set_union2(B,A) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f8,axiom,(
% 0.28/0.59 (! [A] :( ( ~ empty_carrier(A)& join_semilatt_str(A) )=> (! [B] :( element(B,the_carrier(A))=> (! [C] :( element(C,the_carrier(A))=> join(A,B,C) = apply_binary_as_element(the_carrier(A),the_carrier(A),the_carrier(A),the_L_join(A),B,C) ) )) )) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f9,axiom,(
% 0.28/0.59 (! [A] :( ( ~ empty_carrier(A)& meet_semilatt_str(A) )=> (! [B] :( element(B,the_carrier(A))=> (! [C] :( element(C,the_carrier(A))=> meet(A,B,C) = apply_binary_as_element(the_carrier(A),the_carrier(A),the_carrier(A),the_L_meet(A),B,C) ) )) )) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f10,axiom,(
% 0.28/0.59 (! [A] :( ( ~ empty_carrier(A)& join_semilatt_str(A) )=> (! [B] :( element(B,the_carrier(A))=> (! [C] :( element(C,the_carrier(A))=> ( below(A,B,C)<=> join(A,B,C) = C ) ) )) )) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f15,axiom,(
% 0.28/0.59 (! [A] :( strict_latt_str(boole_lattice(A))& latt_str(boole_lattice(A)) ) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f16,axiom,(
% 0.28/0.59 (! [A,B,C] :( ( ~ empty_carrier(A)& join_semilatt_str(A)& element(B,the_carrier(A))& element(C,the_carrier(A)) )=> element(join(A,B,C),the_carrier(A)) ) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f21,axiom,(
% 0.28/0.59 (! [A,B,C] :( ( ~ empty_carrier(A)& meet_semilatt_str(A)& element(B,the_carrier(A))& element(C,the_carrier(A)) )=> element(meet(A,B,C),the_carrier(A)) ) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f27,axiom,(
% 0.28/0.59 (! [A] :( meet_semilatt_str(A)=> one_sorted_str(A) ) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f30,axiom,(
% 0.28/0.59 (! [A] :( latt_str(A)=> ( meet_semilatt_str(A)& join_semilatt_str(A) ) ) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f42,axiom,(
% 0.28/0.59 (! [A] :(? [B] : element(B,A) ))),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f44,axiom,(
% 0.28/0.59 (! [A] :( ~ empty_carrier(boole_lattice(A))& strict_latt_str(boole_lattice(A)) ) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f46,axiom,(
% 0.28/0.59 (! [A] : ~ empty(powerset(A)) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f47,axiom,(
% 0.28/0.59 empty(empty_set) ),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f49,axiom,(
% 0.28/0.59 (! [A,B] :( ~ empty(A)=> ~ empty(set_union2(A,B)) ) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f57,axiom,(
% 0.28/0.59 (! [A] :( ~ empty(A)=> (? [B] :( element(B,powerset(A))& ~ empty(B) ) )) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f60,axiom,(
% 0.28/0.59 (? [A] : ~ empty(A) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f61,axiom,(
% 0.28/0.59 (? [A] :( latt_str(A)& strict_latt_str(A) ) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f62,axiom,(
% 0.28/0.59 (? [A] :( one_sorted_str(A)& ~ empty_carrier(A) ) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f63,axiom,(
% 0.28/0.59 (! [A] :( ( ~ empty_carrier(A)& one_sorted_str(A) )=> (? [B] :( element(B,powerset(the_carrier(A)))& ~ empty(B) ) )) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f64,axiom,(
% 0.28/0.59 (? [A] :( latt_str(A)& ~ empty_carrier(A)& strict_latt_str(A) ) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f67,axiom,(
% 0.28/0.59 (! [A,B] : subset(A,A) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f68,axiom,(
% 0.28/0.59 (! [A,B] :( subset(A,B)=> set_union2(A,B) = B ) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f69,axiom,(
% 0.28/0.59 (! [A] : set_union2(A,empty_set) = A )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f70,axiom,(
% 0.28/0.59 (! [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) ) ) )) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f73,conjecture,(
% 0.28/0.59 (! [A,B] :( element(B,the_carrier(boole_lattice(A)))=> (! [C] :( element(C,the_carrier(boole_lattice(A)))=> ( below(boole_lattice(A),B,C)<=> subset(B,C) ) ) )) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f74,negated_conjecture,(
% 0.28/0.59 ~((! [A,B] :( element(B,the_carrier(boole_lattice(A)))=> (! [C] :( element(C,the_carrier(boole_lattice(A)))=> ( below(boole_lattice(A),B,C)<=> subset(B,C) ) ) )) ))),
% 0.28/0.59 inference(negated_conjecture,[status(cth)],[f73])).
% 0.28/0.59 fof(f75,axiom,(
% 0.28/0.59 (! [A,B] :( element(A,B)=> ( empty(B)| in(A,B) ) ) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f76,axiom,(
% 0.28/0.59 (! [A,B] :( element(A,powerset(B))<=> subset(A,B) ) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f79,axiom,(
% 0.28/0.59 (! [A] :( empty(A)=> A = empty_set ) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f81,axiom,(
% 0.28/0.59 (! [A,B] : subset(A,set_union2(A,B)) )),
% 0.28/0.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.28/0.59 fof(f83,plain,(
% 0.28/0.59 ![A]: (~latt_str(A)|(~strict_latt_str(A)|A=latt_str_of(the_carrier(A),the_L_join(A),the_L_meet(A))))),
% 0.28/0.59 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.28/0.59 fof(f84,plain,(
% 0.28/0.59 ![X0]: (~latt_str(X0)|~strict_latt_str(X0)|X0=latt_str_of(the_carrier(X0),the_L_join(X0),the_L_meet(X0)))),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f83])).
% 0.28/0.59 fof(f85,plain,(
% 0.28/0.59 ![A,B]: (~in(A,B)|~in(B,A))),
% 0.28/0.59 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.28/0.59 fof(f86,plain,(
% 0.28/0.59 ![X0,X1]: (~in(X0,X1)|~in(X1,X0))),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f85])).
% 0.28/0.59 fof(f91,plain,(
% 0.28/0.59 ![X0,X1]: (set_union2(X0,X1)=set_union2(X1,X0))),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f5])).
% 0.28/0.59 fof(f95,plain,(
% 0.28/0.59 ![A]: ((empty_carrier(A)|~join_semilatt_str(A))|(![B]: (~element(B,the_carrier(A))|(![C]: (~element(C,the_carrier(A))|join(A,B,C)=apply_binary_as_element(the_carrier(A),the_carrier(A),the_carrier(A),the_L_join(A),B,C))))))),
% 0.28/0.59 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.28/0.59 fof(f96,plain,(
% 0.28/0.59 ![X0,X1,X2]: (empty_carrier(X0)|~join_semilatt_str(X0)|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|join(X0,X1,X2)=apply_binary_as_element(the_carrier(X0),the_carrier(X0),the_carrier(X0),the_L_join(X0),X1,X2))),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f95])).
% 0.28/0.59 fof(f97,plain,(
% 0.28/0.59 ![A]: ((empty_carrier(A)|~meet_semilatt_str(A))|(![B]: (~element(B,the_carrier(A))|(![C]: (~element(C,the_carrier(A))|meet(A,B,C)=apply_binary_as_element(the_carrier(A),the_carrier(A),the_carrier(A),the_L_meet(A),B,C))))))),
% 0.28/0.59 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.28/0.59 fof(f98,plain,(
% 0.28/0.59 ![X0,X1,X2]: (empty_carrier(X0)|~meet_semilatt_str(X0)|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|meet(X0,X1,X2)=apply_binary_as_element(the_carrier(X0),the_carrier(X0),the_carrier(X0),the_L_meet(X0),X1,X2))),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f97])).
% 0.28/0.59 fof(f99,plain,(
% 0.28/0.59 ![A]: ((empty_carrier(A)|~join_semilatt_str(A))|(![B]: (~element(B,the_carrier(A))|(![C]: (~element(C,the_carrier(A))|(below(A,B,C)<=>join(A,B,C)=C))))))),
% 0.28/0.59 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.28/0.59 fof(f100,plain,(
% 0.28/0.59 ![A]: ((empty_carrier(A)|~join_semilatt_str(A))|(![B]: (~element(B,the_carrier(A))|(![C]: (~element(C,the_carrier(A))|((~below(A,B,C)|join(A,B,C)=C)&(below(A,B,C)|~join(A,B,C)=C)))))))),
% 0.28/0.59 inference(NNF_transformation,[status(thm)],[f99])).
% 0.28/0.59 fof(f101,plain,(
% 0.28/0.59 ![X0,X1,X2]: (empty_carrier(X0)|~join_semilatt_str(X0)|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|~below(X0,X1,X2)|join(X0,X1,X2)=X2)),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f100])).
% 0.28/0.59 fof(f102,plain,(
% 0.28/0.59 ![X0,X1,X2]: (empty_carrier(X0)|~join_semilatt_str(X0)|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|below(X0,X1,X2)|~join(X0,X1,X2)=X2)),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f100])).
% 0.28/0.59 fof(f107,plain,(
% 0.28/0.59 (![A]: strict_latt_str(boole_lattice(A)))&(![A]: latt_str(boole_lattice(A)))),
% 0.28/0.59 inference(miniscoping,[status(thm)],[f15])).
% 0.28/0.59 fof(f109,plain,(
% 0.28/0.59 ![X0]: (latt_str(boole_lattice(X0)))),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f107])).
% 0.28/0.59 fof(f110,plain,(
% 0.28/0.59 ![A,B,C]: ((((empty_carrier(A)|~join_semilatt_str(A))|~element(B,the_carrier(A)))|~element(C,the_carrier(A)))|element(join(A,B,C),the_carrier(A)))),
% 0.28/0.59 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.28/0.59 fof(f111,plain,(
% 0.28/0.59 ![X0,X1,X2]: (empty_carrier(X0)|~join_semilatt_str(X0)|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|element(join(X0,X1,X2),the_carrier(X0)))),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f110])).
% 0.28/0.59 fof(f114,plain,(
% 0.28/0.59 ![A,B,C]: ((((empty_carrier(A)|~meet_semilatt_str(A))|~element(B,the_carrier(A)))|~element(C,the_carrier(A)))|element(meet(A,B,C),the_carrier(A)))),
% 0.28/0.59 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 0.28/0.59 fof(f115,plain,(
% 0.28/0.59 ![X0,X1,X2]: (empty_carrier(X0)|~meet_semilatt_str(X0)|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|element(meet(X0,X1,X2),the_carrier(X0)))),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f114])).
% 0.28/0.59 fof(f116,plain,(
% 0.28/0.59 ![A]: (~meet_semilatt_str(A)|one_sorted_str(A))),
% 0.28/0.59 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 0.28/0.59 fof(f117,plain,(
% 0.28/0.59 ![X0]: (~meet_semilatt_str(X0)|one_sorted_str(X0))),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f116])).
% 0.28/0.59 fof(f120,plain,(
% 0.28/0.59 ![A]: (~latt_str(A)|(meet_semilatt_str(A)&join_semilatt_str(A)))),
% 0.28/0.59 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 0.28/0.59 fof(f121,plain,(
% 0.28/0.59 ![X0]: (~latt_str(X0)|meet_semilatt_str(X0))),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f120])).
% 0.28/0.59 fof(f122,plain,(
% 0.28/0.59 ![X0]: (~latt_str(X0)|join_semilatt_str(X0))),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f120])).
% 0.28/0.59 fof(f143,plain,(
% 0.28/0.59 ![A]: element(sK5_skl(A),A)),
% 0.28/0.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl]),skolemize(B,sK5_skl(A))],[f42])).
% 0.28/0.59 fof(f144,plain,(
% 0.28/0.59 ![X0]: (element(sK5_skl(X0),X0))),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f143])).
% 0.28/0.59 fof(f147,plain,(
% 0.28/0.59 (![A]: ~empty_carrier(boole_lattice(A)))&(![A]: strict_latt_str(boole_lattice(A)))),
% 0.28/0.59 inference(miniscoping,[status(thm)],[f44])).
% 0.28/0.59 fof(f148,plain,(
% 0.28/0.59 ![X0]: (~empty_carrier(boole_lattice(X0)))),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f147])).
% 0.28/0.59 fof(f152,plain,(
% 0.28/0.59 ![X0]: (~empty(powerset(X0)))),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f46])).
% 0.28/0.59 fof(f153,plain,(
% 0.28/0.59 empty(empty_set)),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f47])).
% 0.28/0.59 fof(f155,plain,(
% 0.28/0.59 ![A,B]: (empty(A)|~empty(set_union2(A,B)))),
% 0.28/0.59 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 0.28/0.59 fof(f156,plain,(
% 0.28/0.59 ![A]: (empty(A)|(![B]: ~empty(set_union2(A,B))))),
% 0.28/0.59 inference(miniscoping,[status(thm)],[f155])).
% 0.28/0.59 fof(f157,plain,(
% 0.28/0.59 ![X0,X1]: (empty(X0)|~empty(set_union2(X0,X1)))),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f156])).
% 0.28/0.59 fof(f175,plain,(
% 0.28/0.59 ![A]: (empty(A)|(?[B]: (element(B,powerset(A))&~empty(B))))),
% 0.28/0.59 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 0.28/0.59 fof(f176,plain,(
% 0.28/0.59 ![A]: (empty(A)|(element(sK7_skl(A),powerset(A))&~empty(sK7_skl(A))))),
% 0.28/0.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(B,sK7_skl(A))],[f175])).
% 0.28/0.59 fof(f177,plain,(
% 0.28/0.59 ![X0]: (empty(X0)|element(sK7_skl(X0),powerset(X0)))),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f176])).
% 0.28/0.59 fof(f178,plain,(
% 0.28/0.59 ![X0]: (empty(X0)|~empty(sK7_skl(X0)))),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f176])).
% 0.28/0.59 fof(f184,plain,(
% 0.28/0.59 ~empty(sK10_skl)),
% 0.28/0.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(A,sK10_skl)],[f60])).
% 0.28/0.59 fof(f185,plain,(
% 0.28/0.59 ~empty(sK10_skl)),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f184])).
% 0.28/0.59 fof(f186,plain,(
% 0.28/0.59 (latt_str(sK11_skl)&strict_latt_str(sK11_skl))),
% 0.28/0.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(A,sK11_skl)],[f61])).
% 0.28/0.59 fof(f187,plain,(
% 0.28/0.59 latt_str(sK11_skl)),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f186])).
% 0.28/0.59 fof(f188,plain,(
% 0.28/0.59 strict_latt_str(sK11_skl)),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f186])).
% 0.28/0.59 fof(f189,plain,(
% 0.28/0.59 (one_sorted_str(sK12_skl)&~empty_carrier(sK12_skl))),
% 0.28/0.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(A,sK12_skl)],[f62])).
% 0.28/0.59 fof(f190,plain,(
% 0.28/0.59 one_sorted_str(sK12_skl)),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f189])).
% 0.28/0.59 fof(f191,plain,(
% 0.28/0.59 ~empty_carrier(sK12_skl)),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f189])).
% 0.28/0.59 fof(f192,plain,(
% 0.28/0.59 ![A]: ((empty_carrier(A)|~one_sorted_str(A))|(?[B]: (element(B,powerset(the_carrier(A)))&~empty(B))))),
% 0.28/0.59 inference(pre_NNF_transformation,[status(thm)],[f63])).
% 0.28/0.59 fof(f193,plain,(
% 0.28/0.59 ![A]: ((empty_carrier(A)|~one_sorted_str(A))|(element(sK13_skl(A),powerset(the_carrier(A)))&~empty(sK13_skl(A))))),
% 0.28/0.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(B,sK13_skl(A))],[f192])).
% 0.28/0.59 fof(f194,plain,(
% 0.28/0.59 ![X0]: (empty_carrier(X0)|~one_sorted_str(X0)|element(sK13_skl(X0),powerset(the_carrier(X0))))),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f193])).
% 0.28/0.59 fof(f196,plain,(
% 0.28/0.59 ((latt_str(sK14_skl)&~empty_carrier(sK14_skl))&strict_latt_str(sK14_skl))),
% 0.28/0.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(A,sK14_skl)],[f64])).
% 0.28/0.59 fof(f197,plain,(
% 0.28/0.59 latt_str(sK14_skl)),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f196])).
% 0.28/0.59 fof(f198,plain,(
% 0.28/0.59 ~empty_carrier(sK14_skl)),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f196])).
% 0.28/0.59 fof(f199,plain,(
% 0.28/0.59 strict_latt_str(sK14_skl)),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f196])).
% 0.28/0.59 fof(f206,plain,(
% 0.28/0.59 ![A]: subset(A,A)),
% 0.28/0.59 inference(miniscoping,[status(thm)],[f67])).
% 0.28/0.59 fof(f207,plain,(
% 0.28/0.59 ![X0]: (subset(X0,X0))),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f206])).
% 0.28/0.59 fof(f208,plain,(
% 0.28/0.59 ![A,B]: (~subset(A,B)|set_union2(A,B)=B)),
% 0.28/0.59 inference(pre_NNF_transformation,[status(thm)],[f68])).
% 0.28/0.59 fof(f209,plain,(
% 0.28/0.59 ![X0,X1]: (~subset(X0,X1)|set_union2(X0,X1)=X1)),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f208])).
% 0.28/0.59 fof(f210,plain,(
% 0.28/0.59 ![X0]: (set_union2(X0,empty_set)=X0)),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f69])).
% 0.28/0.59 fof(f211,plain,(
% 0.28/0.59 ![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)))))),
% 0.28/0.59 inference(pre_NNF_transformation,[status(thm)],[f70])).
% 0.28/0.59 fof(f212,plain,(
% 0.28/0.59 ![X0,X1,X2]: (~element(X0,the_carrier(boole_lattice(X1)))|~element(X2,the_carrier(boole_lattice(X1)))|join(boole_lattice(X1),X0,X2)=set_union2(X0,X2))),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f211])).
% 0.28/0.59 fof(f213,plain,(
% 0.28/0.59 ![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))),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f211])).
% 0.28/0.59 fof(f217,plain,(
% 0.28/0.59 (?[A,B]: (element(B,the_carrier(boole_lattice(A)))&(?[C]: (element(C,the_carrier(boole_lattice(A)))&(below(boole_lattice(A),B,C)<~>subset(B,C))))))),
% 0.28/0.59 inference(pre_NNF_transformation,[status(thm)],[f74])).
% 0.28/0.59 fof(f218,plain,(
% 0.28/0.59 ?[A,B]: (element(B,the_carrier(boole_lattice(A)))&(?[C]: (element(C,the_carrier(boole_lattice(A)))&((below(boole_lattice(A),B,C)|subset(B,C))&(~below(boole_lattice(A),B,C)|~subset(B,C))))))),
% 0.28/0.59 inference(NNF_transformation,[status(thm)],[f217])).
% 0.28/0.59 fof(f219,plain,(
% 0.28/0.59 (element(sK16_skl,the_carrier(boole_lattice(sK15_skl)))&(element(sK17_skl,the_carrier(boole_lattice(sK15_skl)))&((below(boole_lattice(sK15_skl),sK16_skl,sK17_skl)|subset(sK16_skl,sK17_skl))&(~below(boole_lattice(sK15_skl),sK16_skl,sK17_skl)|~subset(sK16_skl,sK17_skl)))))),
% 0.28/0.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl,sK17_skl]),skolemize(A,sK15_skl),skolemize(B,sK16_skl),skolemize(C,sK17_skl)],[f218])).
% 0.28/0.59 fof(f220,plain,(
% 0.28/0.59 element(sK16_skl,the_carrier(boole_lattice(sK15_skl)))),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f219])).
% 0.28/0.59 fof(f221,plain,(
% 0.28/0.59 element(sK17_skl,the_carrier(boole_lattice(sK15_skl)))),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f219])).
% 0.28/0.59 fof(f222,plain,(
% 0.28/0.59 below(boole_lattice(sK15_skl),sK16_skl,sK17_skl)|subset(sK16_skl,sK17_skl)),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f219])).
% 0.28/0.59 fof(f223,plain,(
% 0.28/0.59 ~below(boole_lattice(sK15_skl),sK16_skl,sK17_skl)|~subset(sK16_skl,sK17_skl)),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f219])).
% 0.28/0.59 fof(f224,plain,(
% 0.28/0.59 ![A,B]: (~element(A,B)|(empty(B)|in(A,B)))),
% 0.28/0.59 inference(pre_NNF_transformation,[status(thm)],[f75])).
% 0.28/0.59 fof(f225,plain,(
% 0.28/0.59 ![X0,X1]: (~element(X0,X1)|empty(X1)|in(X0,X1))),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f224])).
% 0.28/0.59 fof(f226,plain,(
% 0.28/0.59 ![A,B]: ((~element(A,powerset(B))|subset(A,B))&(element(A,powerset(B))|~subset(A,B)))),
% 0.28/0.59 inference(NNF_transformation,[status(thm)],[f76])).
% 0.28/0.59 fof(f227,plain,(
% 0.28/0.59 (![A,B]: (~element(A,powerset(B))|subset(A,B)))&(![A,B]: (element(A,powerset(B))|~subset(A,B)))),
% 0.28/0.59 inference(miniscoping,[status(thm)],[f226])).
% 0.28/0.59 fof(f228,plain,(
% 0.28/0.59 ![X0,X1]: (~element(X0,powerset(X1))|subset(X0,X1))),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f227])).
% 0.28/0.59 fof(f236,plain,(
% 0.28/0.59 ![A]: (~empty(A)|A=empty_set)),
% 0.28/0.59 inference(pre_NNF_transformation,[status(thm)],[f79])).
% 0.28/0.59 fof(f237,plain,(
% 0.28/0.59 ![X0]: (~empty(X0)|X0=empty_set)),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f236])).
% 0.28/0.59 fof(f241,plain,(
% 0.28/0.59 ![X0,X1]: (subset(X0,set_union2(X0,X1)))),
% 0.28/0.59 inference(cnf_transformation,[status(thm)],[f81])).
% 0.28/0.59 fof(f245,definition,(
% 0.28/0.59 sQ0_spl <=> (below(boole_lattice(sK15_skl),sK16_skl,sK17_skl))),
% 0.28/0.59 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.28/0.59 fof(f246,plain,(
% 0.28/0.59 below(boole_lattice(sK15_skl),sK16_skl,sK17_skl)|~sQ0_spl),
% 0.28/0.59 inference(component_clause,[status(thm)],[f245])).
% 0.28/0.59 fof(f247,plain,(
% 0.28/0.59 ~below(boole_lattice(sK15_skl),sK16_skl,sK17_skl)|sQ0_spl),
% 0.28/0.59 inference(component_clause,[status(thm)],[f245])).
% 0.28/0.59 fof(f248,definition,(
% 0.28/0.59 sQ1_spl <=> (subset(sK16_skl,sK17_skl))),
% 0.28/0.59 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.28/0.59 fof(f249,plain,(
% 0.28/0.59 subset(sK16_skl,sK17_skl)|~sQ1_spl),
% 0.28/0.59 inference(component_clause,[status(thm)],[f248])).
% 0.28/0.59 fof(f251,plain,(
% 0.28/0.59 sQ0_spl|sQ1_spl),
% 0.28/0.59 inference(split_clause,[status(thm)],[f222,f245,f248])).
% 0.28/0.59 fof(f252,plain,(
% 0.28/0.59 ~sQ0_spl|~sQ1_spl),
% 0.28/0.59 inference(split_clause,[status(thm)],[f223,f245,f248])).
% 0.28/0.59 fof(f253,plain,(
% 0.28/0.59 set_union2(sK16_skl,sK17_skl)=sK17_skl|~sQ1_spl),
% 0.28/0.59 inference(resolution,[status(thm)],[f209,f249])).
% 0.28/0.59 fof(f254,plain,(
% 0.28/0.59 ![X0,X1]: (set_union2(X0,set_union2(X0,X1))=set_union2(X0,X1))),
% 0.28/0.59 inference(resolution,[status(thm)],[f209,f241])).
% 0.28/0.59 fof(f255,plain,(
% 0.28/0.59 ![X0]: (set_union2(X0,X0)=X0)),
% 0.28/0.59 inference(resolution,[status(thm)],[f209,f207])).
% 0.28/0.59 fof(f271,plain,(
% 0.28/0.59 ~latt_str(sK11_skl)|sK11_skl=latt_str_of(the_carrier(sK11_skl),the_L_join(sK11_skl),the_L_meet(sK11_skl))),
% 0.28/0.59 inference(resolution,[status(thm)],[f84,f188])).
% 0.28/0.59 fof(f272,definition,(
% 0.28/0.59 sQ5_spl <=> (latt_str(sK11_skl))),
% 0.28/0.59 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.28/0.59 fof(f274,plain,(
% 0.28/0.59 ~latt_str(sK11_skl)|sQ5_spl),
% 0.28/0.59 inference(component_clause,[status(thm)],[f272])).
% 0.28/0.59 fof(f275,definition,(
% 0.28/0.59 sQ6_spl <=> (sK11_skl=latt_str_of(the_carrier(sK11_skl),the_L_join(sK11_skl),the_L_meet(sK11_skl)))),
% 0.28/0.59 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.28/0.59 fof(f278,plain,(
% 0.28/0.59 ~sQ5_spl|sQ6_spl),
% 0.28/0.59 inference(split_clause,[status(thm)],[f271,f272,f275])).
% 0.28/0.59 fof(f279,plain,(
% 0.28/0.59 $false|sQ5_spl),
% 0.28/0.59 inference(forward_subsumption_resolution,[status(thm)],[f274,f187])).
% 0.28/0.59 fof(f280,plain,(
% 0.28/0.59 sQ5_spl),
% 0.28/0.59 inference(contradiction_clause,[status(thm)],[f279])).
% 0.28/0.59 fof(f295,plain,(
% 0.28/0.59 ![X0,X1]: (set_union2(X0,set_union2(X1,X0))=set_union2(X0,X1))),
% 0.28/0.59 inference(paramodulation,[status(thm)],[f91,f254])).
% 0.28/0.59 fof(f296,plain,(
% 0.28/0.59 ![X0,X1]: (subset(X0,set_union2(X1,X0)))),
% 0.28/0.59 inference(paramodulation,[status(thm)],[f91,f241])).
% 0.28/0.59 fof(f299,plain,(
% 0.28/0.59 ~latt_str(sK14_skl)|sK14_skl=latt_str_of(the_carrier(sK14_skl),the_L_join(sK14_skl),the_L_meet(sK14_skl))),
% 0.28/0.59 inference(resolution,[status(thm)],[f199,f84])).
% 0.28/0.59 fof(f300,definition,(
% 0.28/0.59 sQ7_spl <=> (latt_str(sK14_skl))),
% 0.28/0.59 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.28/0.59 fof(f302,plain,(
% 0.28/0.59 ~latt_str(sK14_skl)|sQ7_spl),
% 0.28/0.59 inference(component_clause,[status(thm)],[f300])).
% 0.28/0.59 fof(f303,definition,(
% 0.28/0.59 sQ8_spl <=> (sK14_skl=latt_str_of(the_carrier(sK14_skl),the_L_join(sK14_skl),the_L_meet(sK14_skl)))),
% 0.28/0.59 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.28/0.59 fof(f306,plain,(
% 0.28/0.59 ~sQ7_spl|sQ8_spl),
% 0.28/0.59 inference(split_clause,[status(thm)],[f299,f300,f303])).
% 0.28/0.59 fof(f307,plain,(
% 0.28/0.59 $false|sQ7_spl),
% 0.28/0.59 inference(forward_subsumption_resolution,[status(thm)],[f302,f197])).
% 0.28/0.59 fof(f308,plain,(
% 0.28/0.59 sQ7_spl),
% 0.28/0.59 inference(contradiction_clause,[status(thm)],[f307])).
% 0.28/0.59 fof(f319,plain,(
% 0.28/0.59 ![X0,X1]: (set_union2(X0,set_union2(X1,X0))=set_union2(X1,X0))),
% 0.28/0.59 inference(resolution,[status(thm)],[f296,f209])).
% 0.28/0.59 fof(f325,plain,(
% 0.28/0.59 ![X0,X1]: (set_union2(set_union2(X0,X1),set_union2(X1,X0))=set_union2(set_union2(X0,X1),X1))),
% 0.28/0.59 inference(paramodulation,[status(thm)],[f295,f295])).
% 0.28/0.59 fof(f326,plain,(
% 0.28/0.59 ![X0,X1]: (set_union2(set_union2(X0,X1),set_union2(X0,X1))=set_union2(set_union2(X0,X1),X0))),
% 0.28/0.59 inference(paramodulation,[status(thm)],[f254,f295])).
% 0.28/0.59 fof(f334,plain,(
% 0.28/0.59 ![X0,X1]: (set_union2(X0,X1)=set_union2(set_union2(X0,X1),X0))),
% 0.28/0.59 inference(forward_demodulation,[status(thm)],[f255,f326])).
% 0.28/0.59 fof(f354,plain,(
% 0.28/0.59 ![X0,X1]: (set_union2(X0,set_union2(X0,X1))=set_union2(X1,X0))),
% 0.28/0.59 inference(paramodulation,[status(thm)],[f91,f319])).
% 0.28/0.59 fof(f361,plain,(
% 0.28/0.59 ![X0,X1]: (set_union2(set_union2(X0,X1),set_union2(X0,X1))=set_union2(set_union2(X0,X1),X1))),
% 0.28/0.59 inference(paramodulation,[status(thm)],[f319,f295])).
% 0.28/0.59 fof(f368,plain,(
% 0.28/0.59 ![X0,X1]: (set_union2(X0,X1)=set_union2(set_union2(X0,X1),X1))),
% 0.28/0.59 inference(forward_demodulation,[status(thm)],[f255,f361])).
% 0.28/0.59 fof(f375,plain,(
% 0.28/0.59 ![X0,X1]: (set_union2(X0,X1)=set_union2(set_union2(X1,X0),X0))),
% 0.28/0.59 inference(paramodulation,[status(thm)],[f91,f334])).
% 0.28/0.59 fof(f463,plain,(
% 0.28/0.59 ![X0,X1]: (set_union2(set_union2(X0,X1),set_union2(X1,X0))=set_union2(X0,X1))),
% 0.28/0.59 inference(forward_demodulation,[status(thm)],[f368,f325])).
% 0.28/0.59 fof(f524,plain,(
% 0.28/0.59 ![X0]: (~latt_str(X0)|one_sorted_str(X0))),
% 0.28/0.59 inference(resolution,[status(thm)],[f121,f117])).
% 0.28/0.59 fof(f527,plain,(
% 0.28/0.59 ![X0,X1,X2]: (~latt_str(X0)|empty_carrier(X0)|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|below(X0,X1,X2)|~join(X0,X1,X2)=X2)),
% 0.28/0.59 inference(resolution,[status(thm)],[f122,f102])).
% 0.28/0.59 fof(f528,plain,(
% 0.28/0.59 ![X0,X1,X2]: (~latt_str(X0)|empty_carrier(X0)|~element(X1,the_carrier(X0))|~element(X2,the_carrier(X0))|~below(X0,X1,X2)|join(X0,X1,X2)=X2)),
% 0.28/0.59 inference(resolution,[status(thm)],[f122,f101])).
% 0.28/0.59 fof(f530,plain,(
% 0.28/0.59 ![X0]: (subset(sK5_skl(powerset(X0)),X0))),
% 0.28/0.59 inference(resolution,[status(thm)],[f144,f228])).
% 0.28/0.59 fof(f548,plain,(
% 0.28/0.59 ![X0]: (set_union2(sK5_skl(powerset(X0)),X0)=X0)),
% 0.28/0.59 inference(resolution,[status(thm)],[f530,f209])).
% 0.28/0.59 fof(f590,plain,(
% 0.28/0.59 ~latt_str(boole_lattice(sK15_skl))|empty_carrier(boole_lattice(sK15_skl))|~element(sK16_skl,the_carrier(boole_lattice(sK15_skl)))|~element(sK17_skl,the_carrier(boole_lattice(sK15_skl)))|join(boole_lattice(sK15_skl),sK16_skl,sK17_skl)=sK17_skl|~sQ0_spl),
% 0.28/0.59 inference(resolution,[status(thm)],[f528,f246])).
% 0.28/0.59 fof(f592,definition,(
% 0.28/0.59 sQ12_spl <=> (latt_str(boole_lattice(sK15_skl)))),
% 0.28/0.59 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.28/0.59 fof(f594,plain,(
% 0.28/0.59 ~latt_str(boole_lattice(sK15_skl))|sQ12_spl),
% 0.28/0.59 inference(component_clause,[status(thm)],[f592])).
% 0.28/0.59 fof(f595,definition,(
% 0.28/0.59 sQ13_spl <=> (empty_carrier(boole_lattice(sK15_skl)))),
% 0.28/0.59 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.28/0.59 fof(f596,plain,(
% 0.28/0.59 empty_carrier(boole_lattice(sK15_skl))|~sQ13_spl),
% 0.28/0.59 inference(component_clause,[status(thm)],[f595])).
% 0.28/0.59 fof(f598,definition,(
% 0.28/0.59 sQ14_spl <=> (element(sK16_skl,the_carrier(boole_lattice(sK15_skl))))),
% 0.28/0.59 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.28/0.59 fof(f600,plain,(
% 0.28/0.59 ~element(sK16_skl,the_carrier(boole_lattice(sK15_skl)))|sQ14_spl),
% 0.28/0.59 inference(component_clause,[status(thm)],[f598])).
% 0.28/0.59 fof(f601,definition,(
% 0.28/0.59 sQ15_spl <=> (element(sK17_skl,the_carrier(boole_lattice(sK15_skl))))),
% 0.28/0.59 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.28/0.59 fof(f603,plain,(
% 0.28/0.59 ~element(sK17_skl,the_carrier(boole_lattice(sK15_skl)))|sQ15_spl),
% 0.28/0.59 inference(component_clause,[status(thm)],[f601])).
% 0.28/0.59 fof(f604,definition,(
% 0.28/0.59 sQ16_spl <=> (join(boole_lattice(sK15_skl),sK16_skl,sK17_skl)=sK17_skl)),
% 0.28/0.59 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.28/0.59 fof(f605,plain,(
% 0.28/0.59 join(boole_lattice(sK15_skl),sK16_skl,sK17_skl)=sK17_skl|~sQ16_spl),
% 0.28/0.59 inference(component_clause,[status(thm)],[f604])).
% 0.28/0.59 fof(f606,plain,(
% 0.28/0.59 ~join(boole_lattice(sK15_skl),sK16_skl,sK17_skl)=sK17_skl|sQ16_spl),
% 0.28/0.59 inference(component_clause,[status(thm)],[f604])).
% 0.28/0.59 fof(f607,plain,(
% 0.28/0.59 ~sQ12_spl|sQ13_spl|~sQ14_spl|~sQ15_spl|sQ16_spl|~sQ0_spl),
% 0.28/0.59 inference(split_clause,[status(thm)],[f590,f592,f595,f598,f601,f604,f245])).
% 0.28/0.59 fof(f611,plain,(
% 0.28/0.59 empty_set=sK5_skl(powerset(empty_set))),
% 0.28/0.59 inference(paramodulation,[status(thm)],[f548,f210])).
% 0.28/0.59 fof(f621,plain,(
% 0.28/0.59 ![X0]: (set_union2(X0,set_union2(empty_set,X0))=set_union2(X0,empty_set))),
% 0.28/0.59 inference(paramodulation,[status(thm)],[f210,f463])).
% 0.28/0.59 fof(f635,plain,(
% 0.28/0.59 ![X0]: (set_union2(empty_set,X0)=set_union2(X0,empty_set))),
% 0.28/0.59 inference(forward_demodulation,[status(thm)],[f319,f621])).
% 0.28/0.59 fof(f636,plain,(
% 0.28/0.59 ![X0]: (set_union2(empty_set,X0)=X0)),
% 0.28/0.59 inference(forward_demodulation,[status(thm)],[f210,f635])).
% 0.28/0.59 fof(f649,plain,(
% 0.28/0.59 one_sorted_str(sK14_skl)),
% 0.28/0.59 inference(resolution,[status(thm)],[f524,f197])).
% 0.28/0.59 fof(f653,definition,(
% 0.28/0.59 sQ17_spl <=> (join_semilatt_str(boole_lattice(sK15_skl)))),
% 0.28/0.59 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.28/0.59 fof(f654,plain,(
% 0.28/0.59 join_semilatt_str(boole_lattice(sK15_skl))|~sQ17_spl),
% 0.28/0.59 inference(component_clause,[status(thm)],[f653])).
% 0.28/0.59 fof(f655,plain,(
% 0.28/0.59 ~join_semilatt_str(boole_lattice(sK15_skl))|sQ17_spl),
% 0.28/0.59 inference(component_clause,[status(thm)],[f653])).
% 0.28/0.59 fof(f1008,plain,(
% 0.28/0.59 ![X0]: (empty(empty_set)|~empty(X0))),
% 0.28/0.59 inference(paramodulation,[status(thm)],[f636,f157])).
% 0.28/0.59 fof(f1018,plain,(
% 0.28/0.59 ![X0,X1]: (empty(X0)|~empty(set_union2(X1,X0)))),
% 0.28/0.59 inference(paramodulation,[status(thm)],[f354,f157])).
% 0.28/0.59 fof(f1025,definition,(
% 0.28/0.59 sQ22_spl <=> (empty(empty_set))),
% 0.28/0.59 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.28/0.59 fof(f1028,definition,(
% 0.28/0.59 ![X0]: (sQ23_spl <=> (~empty(X0)))),
% 0.28/0.59 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.28/0.59 fof(f1029,plain,(
% 0.28/0.59 ![X0]: (~empty(X0)|~sQ23_spl)),
% 0.28/0.59 inference(component_clause,[status(thm)],[f1028])).
% 0.28/0.59 fof(f1031,plain,(
% 0.28/0.59 sQ22_spl|sQ23_spl),
% 0.28/0.59 inference(split_clause,[status(thm)],[f1008,f1025,f1028])).
% 0.28/0.59 fof(f1033,plain,(
% 0.28/0.59 $false|~sQ23_spl),
% 0.28/0.59 inference(backward_subsumption_resolution,[status(thm)],[f153,f1029])).
% 0.28/0.59 fof(f1035,plain,(
% 0.28/0.59 ~sQ23_spl),
% 0.28/0.59 inference(contradiction_clause,[status(thm)],[f1033])).
% 0.28/0.59 fof(f1040,plain,(
% 0.28/0.59 ![X0,X1]: (empty(X0)|~empty(set_union2(X0,X1)))),
% 0.28/0.59 inference(paramodulation,[status(thm)],[f375,f1018])).
% 0.28/0.59 fof(f1105,plain,(
% 0.28/0.60 ![X0]: (empty(X0)|subset(sK7_skl(X0),X0))),
% 0.28/0.60 inference(resolution,[status(thm)],[f177,f228])).
% 0.28/0.60 fof(f1120,plain,(
% 0.28/0.60 ![X0]: (empty(X0)|set_union2(sK7_skl(X0),X0)=X0)),
% 0.28/0.60 inference(resolution,[status(thm)],[f1105,f209])).
% 0.28/0.60 fof(f1127,plain,(
% 0.28/0.60 set_union2(sK7_skl(sK10_skl),sK10_skl)=sK10_skl),
% 0.28/0.60 inference(resolution,[status(thm)],[f1120,f185])).
% 0.28/0.60 fof(f1132,plain,(
% 0.28/0.60 ![X0]: (set_union2(sK7_skl(X0),X0)=X0|X0=empty_set)),
% 0.28/0.60 inference(resolution,[status(thm)],[f1120,f237])).
% 0.28/0.60 fof(f1134,plain,(
% 0.28/0.60 set_union2(sK10_skl,sK7_skl(sK10_skl))=sK10_skl),
% 0.28/0.60 inference(paramodulation,[status(thm)],[f91,f1127])).
% 0.28/0.60 fof(f1137,plain,(
% 0.28/0.60 empty(sK7_skl(sK10_skl))|~empty(sK10_skl)),
% 0.28/0.60 inference(paramodulation,[status(thm)],[f1127,f1040])).
% 0.28/0.60 fof(f1157,definition,(
% 0.28/0.60 sQ24_spl <=> (empty(set_union2(sK10_skl,sK7_skl(sK10_skl))))),
% 0.28/0.60 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.28/0.60 fof(f1158,plain,(
% 0.28/0.60 empty(set_union2(sK10_skl,sK7_skl(sK10_skl)))|~sQ24_spl),
% 0.28/0.60 inference(component_clause,[status(thm)],[f1157])).
% 0.28/0.60 fof(f1160,definition,(
% 0.28/0.60 sQ25_spl <=> (empty(sK10_skl))),
% 0.28/0.60 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.28/0.60 fof(f1164,definition,(
% 0.28/0.60 sQ26_spl <=> (empty(sK7_skl(sK10_skl)))),
% 0.28/0.60 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.28/0.60 fof(f1165,plain,(
% 0.28/0.60 empty(sK7_skl(sK10_skl))|~sQ26_spl),
% 0.28/0.60 inference(component_clause,[status(thm)],[f1164])).
% 0.28/0.60 fof(f1167,plain,(
% 0.28/0.60 sQ26_spl|~sQ25_spl),
% 0.28/0.60 inference(split_clause,[status(thm)],[f1137,f1164,f1160])).
% 0.28/0.60 fof(f1179,plain,(
% 0.28/0.60 empty(sK10_skl)|~sQ26_spl),
% 0.28/0.60 inference(resolution,[status(thm)],[f1165,f178])).
% 0.28/0.60 fof(f1183,plain,(
% 0.28/0.60 $false|~sQ26_spl),
% 0.28/0.60 inference(forward_subsumption_resolution,[status(thm)],[f1179,f185])).
% 0.28/0.60 fof(f1184,plain,(
% 0.28/0.60 ~sQ26_spl),
% 0.28/0.60 inference(contradiction_clause,[status(thm)],[f1183])).
% 0.28/0.60 fof(f1187,plain,(
% 0.28/0.60 sK10_skl=sK10_skl|sK10_skl=empty_set),
% 0.28/0.60 inference(paramodulation,[status(thm)],[f1127,f1132])).
% 0.28/0.60 fof(f1214,definition,(
% 0.28/0.60 sQ27_spl <=> (sK10_skl=sK10_skl)),
% 0.28/0.60 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.28/0.60 fof(f1217,definition,(
% 0.28/0.60 sQ28_spl <=> (sK10_skl=empty_set)),
% 0.28/0.60 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.28/0.60 fof(f1218,plain,(
% 0.28/0.60 sK10_skl=empty_set|~sQ28_spl),
% 0.28/0.60 inference(component_clause,[status(thm)],[f1217])).
% 0.28/0.60 fof(f1220,plain,(
% 0.28/0.60 sQ27_spl|sQ28_spl),
% 0.28/0.60 inference(split_clause,[status(thm)],[f1187,f1214,f1217])).
% 0.28/0.60 fof(f1239,plain,(
% 0.28/0.60 ~empty(empty_set)|~sQ28_spl),
% 0.28/0.60 inference(backward_demodulation,[status(thm)],[f1218,f185])).
% 0.28/0.60 fof(f1244,plain,(
% 0.28/0.60 $false|~sQ28_spl),
% 0.28/0.60 inference(forward_subsumption_resolution,[status(thm)],[f1239,f153])).
% 0.28/0.60 fof(f1245,plain,(
% 0.28/0.60 ~sQ28_spl),
% 0.28/0.60 inference(contradiction_clause,[status(thm)],[f1244])).
% 0.28/0.60 fof(f1347,definition,(
% 0.28/0.60 sQ34_spl <=> (empty(set_union2(sK7_skl(sK10_skl),sK10_skl)))),
% 0.28/0.60 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.28/0.60 fof(f1348,plain,(
% 0.28/0.60 empty(set_union2(sK7_skl(sK10_skl),sK10_skl))|~sQ34_spl),
% 0.28/0.60 inference(component_clause,[status(thm)],[f1347])).
% 0.28/0.60 fof(f1375,plain,(
% 0.28/0.60 ![X0]: (empty_carrier(X0)|~one_sorted_str(X0)|subset(sK13_skl(X0),the_carrier(X0)))),
% 0.28/0.60 inference(resolution,[status(thm)],[f194,f228])).
% 0.28/0.60 fof(f1382,plain,(
% 0.28/0.60 ![X0]: (empty_carrier(X0)|~one_sorted_str(X0)|set_union2(sK13_skl(X0),the_carrier(X0))=the_carrier(X0))),
% 0.28/0.60 inference(resolution,[status(thm)],[f1375,f209])).
% 0.28/0.60 fof(f1383,plain,(
% 0.28/0.60 empty(sK10_skl)|~sQ24_spl),
% 0.28/0.60 inference(forward_demodulation,[status(thm)],[f1134,f1158])).
% 0.28/0.60 fof(f1384,plain,(
% 0.28/0.60 $false|~sQ24_spl),
% 0.28/0.60 inference(forward_subsumption_resolution,[status(thm)],[f1383,f185])).
% 0.28/0.60 fof(f1385,plain,(
% 0.28/0.60 ~sQ24_spl),
% 0.28/0.60 inference(contradiction_clause,[status(thm)],[f1384])).
% 0.28/0.60 fof(f1424,plain,(
% 0.28/0.60 ~one_sorted_str(sK14_skl)|set_union2(sK13_skl(sK14_skl),the_carrier(sK14_skl))=the_carrier(sK14_skl)),
% 0.28/0.60 inference(resolution,[status(thm)],[f1382,f198])).
% 0.28/0.60 fof(f1425,plain,(
% 0.28/0.60 ~one_sorted_str(sK12_skl)|set_union2(sK13_skl(sK12_skl),the_carrier(sK12_skl))=the_carrier(sK12_skl)),
% 0.28/0.60 inference(resolution,[status(thm)],[f1382,f191])).
% 0.28/0.60 fof(f1427,definition,(
% 0.28/0.60 sQ35_spl <=> (one_sorted_str(sK14_skl))),
% 0.28/0.60 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.28/0.60 fof(f1429,plain,(
% 0.28/0.60 ~one_sorted_str(sK14_skl)|sQ35_spl),
% 0.28/0.60 inference(component_clause,[status(thm)],[f1427])).
% 0.28/0.60 fof(f1430,definition,(
% 0.28/0.60 sQ36_spl <=> (set_union2(sK13_skl(sK14_skl),the_carrier(sK14_skl))=the_carrier(sK14_skl))),
% 0.28/0.60 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.28/0.60 fof(f1433,plain,(
% 0.28/0.60 ~sQ35_spl|sQ36_spl),
% 0.28/0.60 inference(split_clause,[status(thm)],[f1424,f1427,f1430])).
% 0.28/0.60 fof(f1434,definition,(
% 0.28/0.60 sQ37_spl <=> (one_sorted_str(sK12_skl))),
% 0.28/0.60 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.28/0.60 fof(f1436,plain,(
% 0.28/0.60 ~one_sorted_str(sK12_skl)|sQ37_spl),
% 0.28/0.60 inference(component_clause,[status(thm)],[f1434])).
% 0.28/0.60 fof(f1437,definition,(
% 0.28/0.60 sQ38_spl <=> (set_union2(sK13_skl(sK12_skl),the_carrier(sK12_skl))=the_carrier(sK12_skl))),
% 0.28/0.60 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.28/0.60 fof(f1440,plain,(
% 0.28/0.60 ~sQ37_spl|sQ38_spl),
% 0.28/0.60 inference(split_clause,[status(thm)],[f1425,f1434,f1437])).
% 0.28/0.60 fof(f1441,plain,(
% 0.28/0.60 $false|sQ37_spl),
% 0.28/0.60 inference(forward_subsumption_resolution,[status(thm)],[f1436,f190])).
% 0.28/0.60 fof(f1442,plain,(
% 0.28/0.60 sQ37_spl),
% 0.28/0.60 inference(contradiction_clause,[status(thm)],[f1441])).
% 0.28/0.60 fof(f1443,plain,(
% 0.28/0.60 $false|sQ35_spl),
% 0.28/0.60 inference(forward_subsumption_resolution,[status(thm)],[f1429,f649])).
% 0.28/0.60 fof(f1444,plain,(
% 0.28/0.60 sQ35_spl),
% 0.28/0.60 inference(contradiction_clause,[status(thm)],[f1443])).
% 0.28/0.60 fof(f1537,plain,(
% 0.28/0.60 ![X0]: (~element(X0,the_carrier(boole_lattice(sK15_skl)))|join(boole_lattice(sK15_skl),X0,sK17_skl)=set_union2(X0,sK17_skl))),
% 0.28/0.60 inference(resolution,[status(thm)],[f212,f221])).
% 0.28/0.60 fof(f1538,plain,(
% 0.28/0.60 ![X0]: (~element(X0,the_carrier(boole_lattice(sK15_skl)))|join(boole_lattice(sK15_skl),X0,sK16_skl)=set_union2(X0,sK16_skl))),
% 0.28/0.60 inference(resolution,[status(thm)],[f212,f220])).
% 0.28/0.60 fof(f1544,plain,(
% 0.28/0.60 ![X0]: (~element(X0,the_carrier(boole_lattice(sK15_skl)))|meet(boole_lattice(sK15_skl),X0,sK17_skl)=set_intersection2(X0,sK17_skl))),
% 0.28/0.60 inference(resolution,[status(thm)],[f213,f221])).
% 0.28/0.60 fof(f1545,plain,(
% 0.28/0.60 ![X0]: (~element(X0,the_carrier(boole_lattice(sK15_skl)))|meet(boole_lattice(sK15_skl),X0,sK16_skl)=set_intersection2(X0,sK16_skl))),
% 0.28/0.60 inference(resolution,[status(thm)],[f213,f220])).
% 0.28/0.60 fof(f1548,plain,(
% 0.28/0.60 ![X0,X1]: (join(boole_lattice(sK15_skl),meet(boole_lattice(sK15_skl),X0,X1),sK17_skl)=set_union2(meet(boole_lattice(sK15_skl),X0,X1),sK17_skl)|empty_carrier(boole_lattice(sK15_skl))|~meet_semilatt_str(boole_lattice(sK15_skl))|~element(X0,the_carrier(boole_lattice(sK15_skl)))|~element(X1,the_carrier(boole_lattice(sK15_skl))))),
% 0.28/0.60 inference(resolution,[status(thm)],[f1537,f115])).
% 0.28/0.60 fof(f1549,plain,(
% 0.28/0.60 ![X0,X1]: (join(boole_lattice(sK15_skl),join(boole_lattice(sK15_skl),X0,X1),sK17_skl)=set_union2(join(boole_lattice(sK15_skl),X0,X1),sK17_skl)|empty_carrier(boole_lattice(sK15_skl))|~join_semilatt_str(boole_lattice(sK15_skl))|~element(X0,the_carrier(boole_lattice(sK15_skl)))|~element(X1,the_carrier(boole_lattice(sK15_skl))))),
% 0.28/0.60 inference(resolution,[status(thm)],[f1537,f111])).
% 0.28/0.60 fof(f1552,plain,(
% 0.28/0.60 join(boole_lattice(sK15_skl),sK16_skl,sK17_skl)=set_union2(sK16_skl,sK17_skl)),
% 0.28/0.60 inference(resolution,[status(thm)],[f1537,f220])).
% 0.28/0.60 fof(f1553,definition,(
% 0.28/0.60 ![X0,X1]: (sQ39_spl <=> (join(boole_lattice(sK15_skl),meet(boole_lattice(sK15_skl),X0,X1),sK17_skl)=set_union2(meet(boole_lattice(sK15_skl),X0,X1),sK17_skl)|~element(X0,the_carrier(boole_lattice(sK15_skl)))|~element(X1,the_carrier(boole_lattice(sK15_skl)))))),
% 0.28/0.60 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.28/0.60 fof(f1556,definition,(
% 0.28/0.60 sQ40_spl <=> (meet_semilatt_str(boole_lattice(sK15_skl)))),
% 0.28/0.60 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.28/0.60 fof(f1557,plain,(
% 0.28/0.60 meet_semilatt_str(boole_lattice(sK15_skl))|~sQ40_spl),
% 0.28/0.60 inference(component_clause,[status(thm)],[f1556])).
% 0.28/0.60 fof(f1558,plain,(
% 0.28/0.60 ~meet_semilatt_str(boole_lattice(sK15_skl))|sQ40_spl),
% 0.28/0.60 inference(component_clause,[status(thm)],[f1556])).
% 0.28/0.60 fof(f1559,plain,(
% 0.28/0.60 sQ39_spl|sQ13_spl|~sQ40_spl),
% 0.28/0.60 inference(split_clause,[status(thm)],[f1548,f1553,f595,f1556])).
% 0.28/0.60 fof(f1560,definition,(
% 0.28/0.60 ![X0,X1]: (sQ41_spl <=> (join(boole_lattice(sK15_skl),join(boole_lattice(sK15_skl),X0,X1),sK17_skl)=set_union2(join(boole_lattice(sK15_skl),X0,X1),sK17_skl)|~element(X0,the_carrier(boole_lattice(sK15_skl)))|~element(X1,the_carrier(boole_lattice(sK15_skl)))))),
% 0.28/0.60 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.28/0.60 fof(f1563,plain,(
% 0.28/0.60 sQ41_spl|sQ13_spl|~sQ17_spl),
% 0.28/0.60 inference(split_clause,[status(thm)],[f1549,f1560,f595,f653])).
% 0.28/0.60 fof(f1565,plain,(
% 0.28/0.60 sK17_skl=set_union2(sK16_skl,sK17_skl)|~sQ16_spl),
% 0.28/0.60 inference(forward_demodulation,[status(thm)],[f605,f1552])).
% 0.28/0.60 fof(f1566,plain,(
% 0.28/0.60 $false|~sQ13_spl),
% 0.28/0.60 inference(forward_subsumption_resolution,[status(thm)],[f596,f148])).
% 0.28/0.60 fof(f1567,plain,(
% 0.28/0.60 ~sQ13_spl),
% 0.28/0.60 inference(contradiction_clause,[status(thm)],[f1566])).
% 0.28/0.60 fof(f1568,plain,(
% 0.28/0.60 empty(sK10_skl)|~sQ34_spl),
% 0.28/0.60 inference(forward_demodulation,[status(thm)],[f1127,f1348])).
% 0.28/0.60 fof(f1569,plain,(
% 0.28/0.60 $false|~sQ34_spl),
% 0.28/0.60 inference(forward_subsumption_resolution,[status(thm)],[f1568,f185])).
% 0.28/0.60 fof(f1570,plain,(
% 0.28/0.60 ~sQ34_spl),
% 0.28/0.60 inference(contradiction_clause,[status(thm)],[f1569])).
% 0.28/0.60 fof(f1572,plain,(
% 0.28/0.60 ~latt_str(boole_lattice(sK15_skl))|sQ17_spl),
% 0.28/0.60 inference(resolution,[status(thm)],[f655,f122])).
% 0.28/0.60 fof(f1573,plain,(
% 0.28/0.60 $false|sQ17_spl),
% 0.28/0.60 inference(forward_subsumption_resolution,[status(thm)],[f1572,f109])).
% 0.28/0.60 fof(f1574,plain,(
% 0.28/0.60 sQ17_spl),
% 0.28/0.60 inference(contradiction_clause,[status(thm)],[f1573])).
% 0.28/0.60 fof(f1575,plain,(
% 0.28/0.60 ~latt_str(boole_lattice(sK15_skl))|sQ40_spl),
% 0.28/0.60 inference(resolution,[status(thm)],[f1558,f121])).
% 0.28/0.60 fof(f1576,plain,(
% 0.28/0.60 $false|sQ40_spl),
% 0.28/0.60 inference(forward_subsumption_resolution,[status(thm)],[f1575,f109])).
% 0.28/0.60 fof(f1577,plain,(
% 0.28/0.60 sQ40_spl),
% 0.28/0.60 inference(contradiction_clause,[status(thm)],[f1576])).
% 0.28/0.60 fof(f1578,plain,(
% 0.28/0.60 ![X0,X1]: (join(boole_lattice(sK15_skl),meet(boole_lattice(sK15_skl),X0,X1),sK16_skl)=set_union2(meet(boole_lattice(sK15_skl),X0,X1),sK16_skl)|empty_carrier(boole_lattice(sK15_skl))|~meet_semilatt_str(boole_lattice(sK15_skl))|~element(X0,the_carrier(boole_lattice(sK15_skl)))|~element(X1,the_carrier(boole_lattice(sK15_skl))))),
% 0.28/0.60 inference(resolution,[status(thm)],[f1538,f115])).
% 0.28/0.60 fof(f1579,plain,(
% 0.28/0.60 ![X0,X1]: (join(boole_lattice(sK15_skl),join(boole_lattice(sK15_skl),X0,X1),sK16_skl)=set_union2(join(boole_lattice(sK15_skl),X0,X1),sK16_skl)|empty_carrier(boole_lattice(sK15_skl))|~join_semilatt_str(boole_lattice(sK15_skl))|~element(X0,the_carrier(boole_lattice(sK15_skl)))|~element(X1,the_carrier(boole_lattice(sK15_skl))))),
% 0.28/0.60 inference(resolution,[status(thm)],[f1538,f111])).
% 0.28/0.60 fof(f1583,definition,(
% 0.28/0.60 ![X0,X1]: (sQ42_spl <=> (join(boole_lattice(sK15_skl),meet(boole_lattice(sK15_skl),X0,X1),sK16_skl)=set_union2(meet(boole_lattice(sK15_skl),X0,X1),sK16_skl)|~element(X0,the_carrier(boole_lattice(sK15_skl)))|~element(X1,the_carrier(boole_lattice(sK15_skl)))))),
% 0.28/0.60 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.28/0.60 fof(f1586,plain,(
% 0.28/0.60 sQ42_spl|sQ13_spl|~sQ40_spl),
% 0.28/0.60 inference(split_clause,[status(thm)],[f1578,f1583,f595,f1556])).
% 0.28/0.60 fof(f1587,definition,(
% 0.28/0.60 ![X0,X1]: (sQ43_spl <=> (join(boole_lattice(sK15_skl),join(boole_lattice(sK15_skl),X0,X1),sK16_skl)=set_union2(join(boole_lattice(sK15_skl),X0,X1),sK16_skl)|~element(X0,the_carrier(boole_lattice(sK15_skl)))|~element(X1,the_carrier(boole_lattice(sK15_skl)))))),
% 0.28/0.60 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.28/0.60 fof(f1590,plain,(
% 0.28/0.60 sQ43_spl|sQ13_spl|~sQ17_spl),
% 0.28/0.60 inference(split_clause,[status(thm)],[f1579,f1587,f595,f653])).
% 0.28/0.60 fof(f1594,plain,(
% 0.28/0.60 ![X0,X1]: (empty_carrier(boole_lattice(sK15_skl))|~element(X0,the_carrier(boole_lattice(sK15_skl)))|~element(X1,the_carrier(boole_lattice(sK15_skl)))|join(boole_lattice(sK15_skl),X0,X1)=apply_binary_as_element(the_carrier(boole_lattice(sK15_skl)),the_carrier(boole_lattice(sK15_skl)),the_carrier(boole_lattice(sK15_skl)),the_L_join(boole_lattice(sK15_skl)),X0,X1)|~sQ17_spl)),
% 0.28/0.60 inference(resolution,[status(thm)],[f654,f96])).
% 0.28/0.60 fof(f1595,plain,(
% 0.28/0.60 ![X0,X1]: (empty_carrier(boole_lattice(sK15_skl))|~element(X0,the_carrier(boole_lattice(sK15_skl)))|~element(X1,the_carrier(boole_lattice(sK15_skl)))|below(boole_lattice(sK15_skl),X0,X1)|~join(boole_lattice(sK15_skl),X0,X1)=X1|~sQ17_spl)),
% 0.28/0.60 inference(resolution,[status(thm)],[f654,f102])).
% 0.28/0.60 fof(f1596,plain,(
% 0.28/0.60 ![X0,X1]: (empty_carrier(boole_lattice(sK15_skl))|~element(X0,the_carrier(boole_lattice(sK15_skl)))|~element(X1,the_carrier(boole_lattice(sK15_skl)))|~below(boole_lattice(sK15_skl),X0,X1)|join(boole_lattice(sK15_skl),X0,X1)=X1|~sQ17_spl)),
% 0.28/0.60 inference(resolution,[status(thm)],[f654,f101])).
% 0.28/0.60 fof(f1597,definition,(
% 0.28/0.60 ![X0,X1]: (sQ44_spl <=> (~element(X0,the_carrier(boole_lattice(sK15_skl)))|~element(X1,the_carrier(boole_lattice(sK15_skl)))|join(boole_lattice(sK15_skl),X0,X1)=apply_binary_as_element(the_carrier(boole_lattice(sK15_skl)),the_carrier(boole_lattice(sK15_skl)),the_carrier(boole_lattice(sK15_skl)),the_L_join(boole_lattice(sK15_skl)),X0,X1)))),
% 0.28/0.60 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.28/0.60 fof(f1600,plain,(
% 0.28/0.60 sQ13_spl|sQ44_spl|~sQ17_spl),
% 0.28/0.60 inference(split_clause,[status(thm)],[f1594,f595,f1597,f653])).
% 0.28/0.60 fof(f1601,definition,(
% 0.28/0.60 ![X0,X1]: (sQ45_spl <=> (~element(X0,the_carrier(boole_lattice(sK15_skl)))|~element(X1,the_carrier(boole_lattice(sK15_skl)))|below(boole_lattice(sK15_skl),X0,X1)|~join(boole_lattice(sK15_skl),X0,X1)=X1))),
% 0.28/0.60 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.28/0.60 fof(f1604,plain,(
% 0.28/0.60 sQ13_spl|sQ45_spl|~sQ17_spl),
% 0.28/0.60 inference(split_clause,[status(thm)],[f1595,f595,f1601,f653])).
% 0.28/0.60 fof(f1605,definition,(
% 0.28/0.60 ![X0,X1]: (sQ46_spl <=> (~element(X0,the_carrier(boole_lattice(sK15_skl)))|~element(X1,the_carrier(boole_lattice(sK15_skl)))|~below(boole_lattice(sK15_skl),X0,X1)|join(boole_lattice(sK15_skl),X0,X1)=X1))),
% 0.28/0.60 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.28/0.60 fof(f1608,plain,(
% 0.28/0.60 sQ13_spl|sQ46_spl|~sQ17_spl),
% 0.28/0.60 inference(split_clause,[status(thm)],[f1596,f595,f1605,f653])).
% 0.28/0.60 fof(f1610,plain,(
% 0.28/0.60 ![X0,X1]: (empty_carrier(boole_lattice(sK15_skl))|~element(X0,the_carrier(boole_lattice(sK15_skl)))|~element(X1,the_carrier(boole_lattice(sK15_skl)))|meet(boole_lattice(sK15_skl),X0,X1)=apply_binary_as_element(the_carrier(boole_lattice(sK15_skl)),the_carrier(boole_lattice(sK15_skl)),the_carrier(boole_lattice(sK15_skl)),the_L_meet(boole_lattice(sK15_skl)),X0,X1)|~sQ40_spl)),
% 0.28/0.60 inference(resolution,[status(thm)],[f1557,f98])).
% 0.28/0.60 fof(f1612,definition,(
% 0.28/0.60 ![X0,X1]: (sQ47_spl <=> (~element(X0,the_carrier(boole_lattice(sK15_skl)))|~element(X1,the_carrier(boole_lattice(sK15_skl)))|meet(boole_lattice(sK15_skl),X0,X1)=apply_binary_as_element(the_carrier(boole_lattice(sK15_skl)),the_carrier(boole_lattice(sK15_skl)),the_carrier(boole_lattice(sK15_skl)),the_L_meet(boole_lattice(sK15_skl)),X0,X1)))),
% 0.28/0.60 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.28/0.60 fof(f1615,plain,(
% 0.28/0.60 sQ13_spl|sQ47_spl|~sQ40_spl),
% 0.28/0.60 inference(split_clause,[status(thm)],[f1610,f595,f1612,f1556])).
% 0.28/0.60 fof(f1634,plain,(
% 0.28/0.60 subset(sK16_skl,sK17_skl)|~sQ16_spl),
% 0.28/0.60 inference(paramodulation,[status(thm)],[f1565,f241])).
% 0.28/0.60 fof(f1657,plain,(
% 0.28/0.60 sQ1_spl|~sQ16_spl),
% 0.28/0.60 inference(split_clause,[status(thm)],[f1634,f248,f604])).
% 0.28/0.60 fof(f1658,plain,(
% 0.28/0.60 $false|sQ15_spl),
% 0.28/0.60 inference(forward_subsumption_resolution,[status(thm)],[f603,f221])).
% 0.28/0.60 fof(f1659,plain,(
% 0.28/0.60 sQ15_spl),
% 0.28/0.60 inference(contradiction_clause,[status(thm)],[f1658])).
% 0.28/0.60 fof(f1660,plain,(
% 0.28/0.60 $false|sQ12_spl),
% 0.28/0.60 inference(forward_subsumption_resolution,[status(thm)],[f594,f109])).
% 0.28/0.60 fof(f1661,plain,(
% 0.28/0.60 sQ12_spl),
% 0.28/0.60 inference(contradiction_clause,[status(thm)],[f1660])).
% 0.28/0.60 fof(f1662,plain,(
% 0.28/0.60 $false|sQ14_spl),
% 0.28/0.60 inference(forward_subsumption_resolution,[status(thm)],[f600,f220])).
% 0.28/0.60 fof(f1663,plain,(
% 0.28/0.60 sQ14_spl),
% 0.28/0.60 inference(contradiction_clause,[status(thm)],[f1662])).
% 0.28/0.60 fof(f1681,plain,(
% 0.28/0.60 ~latt_str(boole_lattice(sK15_skl))|empty_carrier(boole_lattice(sK15_skl))|~element(sK16_skl,the_carrier(boole_lattice(sK15_skl)))|~element(sK17_skl,the_carrier(boole_lattice(sK15_skl)))|~join(boole_lattice(sK15_skl),sK16_skl,sK17_skl)=sK17_skl|sQ0_spl),
% 0.28/0.60 inference(resolution,[status(thm)],[f247,f527])).
% 0.28/0.60 fof(f1682,plain,(
% 0.28/0.60 ~sQ12_spl|sQ13_spl|~sQ14_spl|~sQ15_spl|~sQ16_spl|sQ0_spl),
% 0.28/0.60 inference(split_clause,[status(thm)],[f1681,f592,f595,f598,f601,f604,f245])).
% 0.28/0.60 fof(f1683,plain,(
% 0.28/0.60 ![X0,X1]: (meet(boole_lattice(sK15_skl),meet(boole_lattice(sK15_skl),X0,X1),sK17_skl)=set_intersection2(meet(boole_lattice(sK15_skl),X0,X1),sK17_skl)|empty_carrier(boole_lattice(sK15_skl))|~meet_semilatt_str(boole_lattice(sK15_skl))|~element(X0,the_carrier(boole_lattice(sK15_skl)))|~element(X1,the_carrier(boole_lattice(sK15_skl))))),
% 0.28/0.60 inference(resolution,[status(thm)],[f1544,f115])).
% 0.28/0.60 fof(f1684,plain,(
% 0.28/0.60 ![X0,X1]: (meet(boole_lattice(sK15_skl),join(boole_lattice(sK15_skl),X0,X1),sK17_skl)=set_intersection2(join(boole_lattice(sK15_skl),X0,X1),sK17_skl)|empty_carrier(boole_lattice(sK15_skl))|~join_semilatt_str(boole_lattice(sK15_skl))|~element(X0,the_carrier(boole_lattice(sK15_skl)))|~element(X1,the_carrier(boole_lattice(sK15_skl))))),
% 0.28/0.60 inference(resolution,[status(thm)],[f1544,f111])).
% 0.28/0.60 fof(f1688,definition,(
% 0.28/0.60 ![X0,X1]: (sQ53_spl <=> (meet(boole_lattice(sK15_skl),meet(boole_lattice(sK15_skl),X0,X1),sK17_skl)=set_intersection2(meet(boole_lattice(sK15_skl),X0,X1),sK17_skl)|~element(X0,the_carrier(boole_lattice(sK15_skl)))|~element(X1,the_carrier(boole_lattice(sK15_skl)))))),
% 0.28/0.60 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.28/0.60 fof(f1691,plain,(
% 0.28/0.60 sQ53_spl|sQ13_spl|~sQ40_spl),
% 0.28/0.60 inference(split_clause,[status(thm)],[f1683,f1688,f595,f1556])).
% 0.28/0.60 fof(f1692,definition,(
% 0.28/0.60 ![X0,X1]: (sQ54_spl <=> (meet(boole_lattice(sK15_skl),join(boole_lattice(sK15_skl),X0,X1),sK17_skl)=set_intersection2(join(boole_lattice(sK15_skl),X0,X1),sK17_skl)|~element(X0,the_carrier(boole_lattice(sK15_skl)))|~element(X1,the_carrier(boole_lattice(sK15_skl)))))),
% 0.28/0.60 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.28/0.60 fof(f1695,plain,(
% 0.28/0.60 sQ54_spl|sQ13_spl|~sQ17_spl),
% 0.28/0.60 inference(split_clause,[status(thm)],[f1684,f1692,f595,f653])).
% 0.28/0.60 fof(f1791,plain,(
% 0.28/0.60 ![X0]: (empty(X0)|in(sK5_skl(X0),X0))),
% 0.28/0.60 inference(resolution,[status(thm)],[f225,f144])).
% 0.28/0.60 fof(f1810,plain,(
% 0.28/0.60 ![X0,X1]: (meet(boole_lattice(sK15_skl),meet(boole_lattice(sK15_skl),X0,X1),sK16_skl)=set_intersection2(meet(boole_lattice(sK15_skl),X0,X1),sK16_skl)|empty_carrier(boole_lattice(sK15_skl))|~meet_semilatt_str(boole_lattice(sK15_skl))|~element(X0,the_carrier(boole_lattice(sK15_skl)))|~element(X1,the_carrier(boole_lattice(sK15_skl))))),
% 0.28/0.60 inference(resolution,[status(thm)],[f1545,f115])).
% 0.28/0.60 fof(f1811,plain,(
% 0.28/0.60 ![X0,X1]: (meet(boole_lattice(sK15_skl),join(boole_lattice(sK15_skl),X0,X1),sK16_skl)=set_intersection2(join(boole_lattice(sK15_skl),X0,X1),sK16_skl)|empty_carrier(boole_lattice(sK15_skl))|~join_semilatt_str(boole_lattice(sK15_skl))|~element(X0,the_carrier(boole_lattice(sK15_skl)))|~element(X1,the_carrier(boole_lattice(sK15_skl))))),
% 0.28/0.60 inference(resolution,[status(thm)],[f1545,f111])).
% 0.28/0.60 fof(f1815,definition,(
% 0.28/0.60 ![X0,X1]: (sQ61_spl <=> (meet(boole_lattice(sK15_skl),meet(boole_lattice(sK15_skl),X0,X1),sK16_skl)=set_intersection2(meet(boole_lattice(sK15_skl),X0,X1),sK16_skl)|~element(X0,the_carrier(boole_lattice(sK15_skl)))|~element(X1,the_carrier(boole_lattice(sK15_skl)))))),
% 0.28/0.60 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.28/0.60 fof(f1818,plain,(
% 0.28/0.60 sQ61_spl|sQ13_spl|~sQ40_spl),
% 0.28/0.60 inference(split_clause,[status(thm)],[f1810,f1815,f595,f1556])).
% 0.28/0.60 fof(f1819,definition,(
% 0.28/0.60 ![X0,X1]: (sQ62_spl <=> (meet(boole_lattice(sK15_skl),join(boole_lattice(sK15_skl),X0,X1),sK16_skl)=set_intersection2(join(boole_lattice(sK15_skl),X0,X1),sK16_skl)|~element(X0,the_carrier(boole_lattice(sK15_skl)))|~element(X1,the_carrier(boole_lattice(sK15_skl)))))),
% 0.28/0.60 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.28/0.60 fof(f1822,plain,(
% 0.28/0.60 sQ62_spl|sQ13_spl|~sQ17_spl),
% 0.28/0.60 inference(split_clause,[status(thm)],[f1811,f1819,f595,f653])).
% 0.28/0.60 fof(f1944,plain,(
% 0.28/0.60 ![X0]: (empty(X0)|~in(X0,sK5_skl(X0)))),
% 0.28/0.60 inference(resolution,[status(thm)],[f1791,f86])).
% 0.28/0.60 fof(f1945,plain,(
% 0.28/0.60 empty(powerset(empty_set))|in(empty_set,powerset(empty_set))),
% 0.28/0.60 inference(paramodulation,[status(thm)],[f611,f1791])).
% 0.28/0.60 fof(f1946,definition,(
% 0.28/0.60 sQ80_spl <=> (empty(powerset(empty_set)))),
% 0.28/0.60 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.28/0.60 fof(f1947,plain,(
% 0.28/0.60 empty(powerset(empty_set))|~sQ80_spl),
% 0.28/0.60 inference(component_clause,[status(thm)],[f1946])).
% 0.28/0.60 fof(f1949,definition,(
% 0.28/0.60 sQ81_spl <=> (in(empty_set,powerset(empty_set)))),
% 0.28/0.60 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.28/0.60 fof(f1952,plain,(
% 0.28/0.60 sQ80_spl|sQ81_spl),
% 0.28/0.60 inference(split_clause,[status(thm)],[f1945,f1946,f1949])).
% 0.28/0.60 fof(f1953,plain,(
% 0.28/0.60 $false|~sQ80_spl),
% 0.28/0.60 inference(forward_subsumption_resolution,[status(thm)],[f1947,f152])).
% 0.28/0.60 fof(f1954,plain,(
% 0.28/0.60 ~sQ80_spl),
% 0.28/0.60 inference(contradiction_clause,[status(thm)],[f1953])).
% 0.28/0.63 fof(f1955,plain,(
% 0.28/0.63 empty(powerset(empty_set))|~in(powerset(empty_set),empty_set)),
% 0.28/0.63 inference(paramodulation,[status(thm)],[f611,f1944])).
% 0.28/0.63 fof(f1956,definition,(
% 0.28/0.63 sQ82_spl <=> (in(powerset(empty_set),empty_set))),
% 0.28/0.63 introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition])).
% 0.28/0.63 fof(f1959,plain,(
% 0.28/0.63 sQ80_spl|~sQ82_spl),
% 0.28/0.63 inference(split_clause,[status(thm)],[f1955,f1946,f1956])).
% 0.28/0.63 fof(f2204,plain,(
% 0.28/0.63 join(boole_lattice(sK15_skl),sK16_skl,sK17_skl)=set_union2(sK16_skl,sK17_skl)),
% 0.28/0.63 inference(resolution,[status(thm)],[f1537,f220])).
% 0.28/0.63 fof(f2209,plain,(
% 0.28/0.63 join(boole_lattice(sK15_skl),sK16_skl,sK17_skl)=sK17_skl|~sQ1_spl),
% 0.28/0.63 inference(forward_demodulation,[status(thm)],[f253,f2204])).
% 0.28/0.63 fof(f2210,plain,(
% 0.28/0.63 $false|sQ16_spl|~sQ1_spl),
% 0.28/0.63 inference(forward_subsumption_resolution,[status(thm)],[f2209,f606])).
% 0.28/0.63 fof(f2211,plain,(
% 0.28/0.63 sQ16_spl|~sQ1_spl),
% 0.28/0.63 inference(contradiction_clause,[status(thm)],[f2210])).
% 0.28/0.63 fof(f2212,plain,(
% 0.28/0.63 $false),
% 0.28/0.63 inference(sat_refutation,[status(thm)],[f251,f252,f278,f280,f306,f308,f607,f1031,f1035,f1167,f1184,f1220,f1245,f1385,f1433,f1440,f1442,f1444,f1559,f1563,f1567,f1570,f1574,f1577,f1586,f1590,f1600,f1604,f1608,f1615,f1657,f1659,f1661,f1663,f1682,f1691,f1695,f1818,f1822,f1952,f1954,f1959,f2211])).
% 0.28/0.63 % SZS output end CNFRefutation for theBenchmark.p
% 0.28/0.63 % Elapsed time: 0.163616 seconds
% 0.28/0.63 % CPU time: 0.930474 seconds
% 0.28/0.63 % Total memory used: 119.025 MB
% 0.28/0.63 % Net memory used: 118.568 MB
%------------------------------------------------------------------------------