%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SEU345+1 : TPTP v5.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art03.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Thu Dec 30 03:50:27 EST 2010
% Result : Theorem 1.43s
% Output : Solution 1.43s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP6397/SEU345+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP6397/SEU345+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP6397/SEU345+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 6493
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.026 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:(empty(X1)=>X1=empty_set),file('/tmp/SRASS.s.p', t6_boole)).
% fof(3, axiom,![X1]:set_intersection2(X1,empty_set)=empty_set,file('/tmp/SRASS.s.p', t2_boole)).
% fof(6, axiom,![X1]:((~(empty_carrier(X1))&meet_semilatt_str(X1))=>element(bottom_of_semilattstr(X1),the_carrier(X1))),file('/tmp/SRASS.s.p', dt_k5_lattices)).
% fof(18, axiom,![X1]:![X2]:set_intersection2(X1,X2)=set_intersection2(X2,X1),file('/tmp/SRASS.s.p', commutativity_k3_xboole_0)).
% fof(20, axiom,![X1]:((~(empty_carrier(X1))&meet_semilatt_str(X1))=>(lower_bounded_semilattstr(X1)=>![X2]:(element(X2,the_carrier(X1))=>(X2=bottom_of_semilattstr(X1)<=>![X3]:(element(X3,the_carrier(X1))=>(meet(X1,X2,X3)=X2&meet(X1,X3,X2)=X2)))))),file('/tmp/SRASS.s.p', d16_lattices)).
% fof(22, axiom,![X1]:(~(empty_carrier(boole_lattice(X1)))&strict_latt_str(boole_lattice(X1))),file('/tmp/SRASS.s.p', fc1_lattice3)).
% fof(24, axiom,![X1]:(strict_latt_str(boole_lattice(X1))&latt_str(boole_lattice(X1))),file('/tmp/SRASS.s.p', dt_k1_lattice3)).
% fof(35, axiom,![X1]:((~(empty_carrier(X1))&meet_semilatt_str(X1))=>(lower_bounded_semilattstr(X1)<=>?[X2]:(element(X2,the_carrier(X1))&![X3]:(element(X3,the_carrier(X1))=>(meet(X1,X2,X3)=X2&meet(X1,X3,X2)=X2))))),file('/tmp/SRASS.s.p', d13_lattices)).
% fof(47, axiom,![X1]:?[X2]:(element(X2,powerset(X1))&empty(X2)),file('/tmp/SRASS.s.p', rc2_subset_1)).
% fof(51, axiom,![X1]:![X2]:(element(X2,the_carrier(boole_lattice(X1)))=>![X3]:(element(X3,the_carrier(boole_lattice(X1)))=>(join(boole_lattice(X1),X2,X3)=set_union2(X2,X3)&meet(boole_lattice(X1),X2,X3)=set_intersection2(X2,X3)))),file('/tmp/SRASS.s.p', t1_lattice3)).
% fof(68, axiom,![X1]:(latt_str(X1)=>(meet_semilatt_str(X1)&join_semilatt_str(X1))),file('/tmp/SRASS.s.p', dt_l3_lattices)).
% fof(77, axiom,![X1]:![X2]:((strict_latt_str(X2)&latt_str(X2))=>(X2=boole_lattice(X1)<=>(the_carrier(X2)=powerset(X1)&![X3]:(element(X3,powerset(X1))=>![X4]:(element(X4,powerset(X1))=>(apply_binary(the_L_join(X2),X3,X4)=subset_union2(X1,X3,X4)&apply_binary(the_L_meet(X2),X3,X4)=subset_intersection2(X1,X3,X4))))))),file('/tmp/SRASS.s.p', d1_lattice3)).
% fof(102, conjecture,![X1]:(lower_bounded_semilattstr(boole_lattice(X1))&bottom_of_semilattstr(boole_lattice(X1))=empty_set),file('/tmp/SRASS.s.p', t3_lattice3)).
% fof(103, negated_conjecture,~(![X1]:(lower_bounded_semilattstr(boole_lattice(X1))&bottom_of_semilattstr(boole_lattice(X1))=empty_set)),inference(assume_negation,[status(cth)],[102])).
% fof(105, plain,![X1]:((~(empty_carrier(X1))&meet_semilatt_str(X1))=>element(bottom_of_semilattstr(X1),the_carrier(X1))),inference(fof_simplification,[status(thm)],[6,theory(equality)])).
% fof(107, plain,![X1]:((~(empty_carrier(X1))&meet_semilatt_str(X1))=>(lower_bounded_semilattstr(X1)=>![X2]:(element(X2,the_carrier(X1))=>(X2=bottom_of_semilattstr(X1)<=>![X3]:(element(X3,the_carrier(X1))=>(meet(X1,X2,X3)=X2&meet(X1,X3,X2)=X2)))))),inference(fof_simplification,[status(thm)],[20,theory(equality)])).
% fof(109, plain,![X1]:(~(empty_carrier(boole_lattice(X1)))&strict_latt_str(boole_lattice(X1))),inference(fof_simplification,[status(thm)],[22,theory(equality)])).
% fof(117, plain,![X1]:((~(empty_carrier(X1))&meet_semilatt_str(X1))=>(lower_bounded_semilattstr(X1)<=>?[X2]:(element(X2,the_carrier(X1))&![X3]:(element(X3,the_carrier(X1))=>(meet(X1,X2,X3)=X2&meet(X1,X3,X2)=X2))))),inference(fof_simplification,[status(thm)],[35,theory(equality)])).
% fof(139, plain,![X1]:(~(empty(X1))|X1=empty_set),inference(fof_nnf,[status(thm)],[1])).
% fof(140, plain,![X2]:(~(empty(X2))|X2=empty_set),inference(variable_rename,[status(thm)],[139])).
% cnf(141,plain,(X1=empty_set|~empty(X1)),inference(split_conjunct,[status(thm)],[140])).
% fof(144, plain,![X2]:set_intersection2(X2,empty_set)=empty_set,inference(variable_rename,[status(thm)],[3])).
% cnf(145,plain,(set_intersection2(X1,empty_set)=empty_set),inference(split_conjunct,[status(thm)],[144])).
% fof(150, plain,![X1]:((empty_carrier(X1)|~(meet_semilatt_str(X1)))|element(bottom_of_semilattstr(X1),the_carrier(X1))),inference(fof_nnf,[status(thm)],[105])).
% fof(151, plain,![X2]:((empty_carrier(X2)|~(meet_semilatt_str(X2)))|element(bottom_of_semilattstr(X2),the_carrier(X2))),inference(variable_rename,[status(thm)],[150])).
% cnf(152,plain,(element(bottom_of_semilattstr(X1),the_carrier(X1))|empty_carrier(X1)|~meet_semilatt_str(X1)),inference(split_conjunct,[status(thm)],[151])).
% fof(181, plain,![X3]:![X4]:set_intersection2(X3,X4)=set_intersection2(X4,X3),inference(variable_rename,[status(thm)],[18])).
% cnf(182,plain,(set_intersection2(X1,X2)=set_intersection2(X2,X1)),inference(split_conjunct,[status(thm)],[181])).
% fof(185, plain,![X1]:((empty_carrier(X1)|~(meet_semilatt_str(X1)))|(~(lower_bounded_semilattstr(X1))|![X2]:(~(element(X2,the_carrier(X1)))|((~(X2=bottom_of_semilattstr(X1))|![X3]:(~(element(X3,the_carrier(X1)))|(meet(X1,X2,X3)=X2&meet(X1,X3,X2)=X2)))&(?[X3]:(element(X3,the_carrier(X1))&(~(meet(X1,X2,X3)=X2)|~(meet(X1,X3,X2)=X2)))|X2=bottom_of_semilattstr(X1)))))),inference(fof_nnf,[status(thm)],[107])).
% fof(186, plain,![X4]:((empty_carrier(X4)|~(meet_semilatt_str(X4)))|(~(lower_bounded_semilattstr(X4))|![X5]:(~(element(X5,the_carrier(X4)))|((~(X5=bottom_of_semilattstr(X4))|![X6]:(~(element(X6,the_carrier(X4)))|(meet(X4,X5,X6)=X5&meet(X4,X6,X5)=X5)))&(?[X7]:(element(X7,the_carrier(X4))&(~(meet(X4,X5,X7)=X5)|~(meet(X4,X7,X5)=X5)))|X5=bottom_of_semilattstr(X4)))))),inference(variable_rename,[status(thm)],[185])).
% fof(187, plain,![X4]:((empty_carrier(X4)|~(meet_semilatt_str(X4)))|(~(lower_bounded_semilattstr(X4))|![X5]:(~(element(X5,the_carrier(X4)))|((~(X5=bottom_of_semilattstr(X4))|![X6]:(~(element(X6,the_carrier(X4)))|(meet(X4,X5,X6)=X5&meet(X4,X6,X5)=X5)))&((element(esk6_2(X4,X5),the_carrier(X4))&(~(meet(X4,X5,esk6_2(X4,X5))=X5)|~(meet(X4,esk6_2(X4,X5),X5)=X5)))|X5=bottom_of_semilattstr(X4)))))),inference(skolemize,[status(esa)],[186])).
% fof(188, plain,![X4]:![X5]:![X6]:((((((~(element(X6,the_carrier(X4)))|(meet(X4,X5,X6)=X5&meet(X4,X6,X5)=X5))|~(X5=bottom_of_semilattstr(X4)))&((element(esk6_2(X4,X5),the_carrier(X4))&(~(meet(X4,X5,esk6_2(X4,X5))=X5)|~(meet(X4,esk6_2(X4,X5),X5)=X5)))|X5=bottom_of_semilattstr(X4)))|~(element(X5,the_carrier(X4))))|~(lower_bounded_semilattstr(X4)))|(empty_carrier(X4)|~(meet_semilatt_str(X4)))),inference(shift_quantors,[status(thm)],[187])).
% fof(189, plain,![X4]:![X5]:![X6]:(((((((meet(X4,X5,X6)=X5|~(element(X6,the_carrier(X4))))|~(X5=bottom_of_semilattstr(X4)))|~(element(X5,the_carrier(X4))))|~(lower_bounded_semilattstr(X4)))|(empty_carrier(X4)|~(meet_semilatt_str(X4))))&(((((meet(X4,X6,X5)=X5|~(element(X6,the_carrier(X4))))|~(X5=bottom_of_semilattstr(X4)))|~(element(X5,the_carrier(X4))))|~(lower_bounded_semilattstr(X4)))|(empty_carrier(X4)|~(meet_semilatt_str(X4)))))&(((((element(esk6_2(X4,X5),the_carrier(X4))|X5=bottom_of_semilattstr(X4))|~(element(X5,the_carrier(X4))))|~(lower_bounded_semilattstr(X4)))|(empty_carrier(X4)|~(meet_semilatt_str(X4))))&(((((~(meet(X4,X5,esk6_2(X4,X5))=X5)|~(meet(X4,esk6_2(X4,X5),X5)=X5))|X5=bottom_of_semilattstr(X4))|~(element(X5,the_carrier(X4))))|~(lower_bounded_semilattstr(X4)))|(empty_carrier(X4)|~(meet_semilatt_str(X4)))))),inference(distribute,[status(thm)],[188])).
% cnf(192,plain,(empty_carrier(X1)|meet(X1,X3,X2)=X2|~meet_semilatt_str(X1)|~lower_bounded_semilattstr(X1)|~element(X2,the_carrier(X1))|X2!=bottom_of_semilattstr(X1)|~element(X3,the_carrier(X1))),inference(split_conjunct,[status(thm)],[189])).
% fof(198, plain,![X2]:(~(empty_carrier(boole_lattice(X2)))&strict_latt_str(boole_lattice(X2))),inference(variable_rename,[status(thm)],[109])).
% cnf(199,plain,(strict_latt_str(boole_lattice(X1))),inference(split_conjunct,[status(thm)],[198])).
% cnf(200,plain,(~empty_carrier(boole_lattice(X1))),inference(split_conjunct,[status(thm)],[198])).
% fof(204, plain,![X2]:(strict_latt_str(boole_lattice(X2))&latt_str(boole_lattice(X2))),inference(variable_rename,[status(thm)],[24])).
% cnf(205,plain,(latt_str(boole_lattice(X1))),inference(split_conjunct,[status(thm)],[204])).
% fof(248, plain,![X1]:((empty_carrier(X1)|~(meet_semilatt_str(X1)))|((~(lower_bounded_semilattstr(X1))|?[X2]:(element(X2,the_carrier(X1))&![X3]:(~(element(X3,the_carrier(X1)))|(meet(X1,X2,X3)=X2&meet(X1,X3,X2)=X2))))&(![X2]:(~(element(X2,the_carrier(X1)))|?[X3]:(element(X3,the_carrier(X1))&(~(meet(X1,X2,X3)=X2)|~(meet(X1,X3,X2)=X2))))|lower_bounded_semilattstr(X1)))),inference(fof_nnf,[status(thm)],[117])).
% fof(249, plain,![X4]:((empty_carrier(X4)|~(meet_semilatt_str(X4)))|((~(lower_bounded_semilattstr(X4))|?[X5]:(element(X5,the_carrier(X4))&![X6]:(~(element(X6,the_carrier(X4)))|(meet(X4,X5,X6)=X5&meet(X4,X6,X5)=X5))))&(![X7]:(~(element(X7,the_carrier(X4)))|?[X8]:(element(X8,the_carrier(X4))&(~(meet(X4,X7,X8)=X7)|~(meet(X4,X8,X7)=X7))))|lower_bounded_semilattstr(X4)))),inference(variable_rename,[status(thm)],[248])).
% fof(250, plain,![X4]:((empty_carrier(X4)|~(meet_semilatt_str(X4)))|((~(lower_bounded_semilattstr(X4))|(element(esk11_1(X4),the_carrier(X4))&![X6]:(~(element(X6,the_carrier(X4)))|(meet(X4,esk11_1(X4),X6)=esk11_1(X4)&meet(X4,X6,esk11_1(X4))=esk11_1(X4)))))&(![X7]:(~(element(X7,the_carrier(X4)))|(element(esk12_2(X4,X7),the_carrier(X4))&(~(meet(X4,X7,esk12_2(X4,X7))=X7)|~(meet(X4,esk12_2(X4,X7),X7)=X7))))|lower_bounded_semilattstr(X4)))),inference(skolemize,[status(esa)],[249])).
% fof(251, plain,![X4]:![X6]:![X7]:((((~(element(X7,the_carrier(X4)))|(element(esk12_2(X4,X7),the_carrier(X4))&(~(meet(X4,X7,esk12_2(X4,X7))=X7)|~(meet(X4,esk12_2(X4,X7),X7)=X7))))|lower_bounded_semilattstr(X4))&(((~(element(X6,the_carrier(X4)))|(meet(X4,esk11_1(X4),X6)=esk11_1(X4)&meet(X4,X6,esk11_1(X4))=esk11_1(X4)))&element(esk11_1(X4),the_carrier(X4)))|~(lower_bounded_semilattstr(X4))))|(empty_carrier(X4)|~(meet_semilatt_str(X4)))),inference(shift_quantors,[status(thm)],[250])).
% fof(252, plain,![X4]:![X6]:![X7]:(((((element(esk12_2(X4,X7),the_carrier(X4))|~(element(X7,the_carrier(X4))))|lower_bounded_semilattstr(X4))|(empty_carrier(X4)|~(meet_semilatt_str(X4))))&((((~(meet(X4,X7,esk12_2(X4,X7))=X7)|~(meet(X4,esk12_2(X4,X7),X7)=X7))|~(element(X7,the_carrier(X4))))|lower_bounded_semilattstr(X4))|(empty_carrier(X4)|~(meet_semilatt_str(X4)))))&(((((meet(X4,esk11_1(X4),X6)=esk11_1(X4)|~(element(X6,the_carrier(X4))))|~(lower_bounded_semilattstr(X4)))|(empty_carrier(X4)|~(meet_semilatt_str(X4))))&(((meet(X4,X6,esk11_1(X4))=esk11_1(X4)|~(element(X6,the_carrier(X4))))|~(lower_bounded_semilattstr(X4)))|(empty_carrier(X4)|~(meet_semilatt_str(X4)))))&((element(esk11_1(X4),the_carrier(X4))|~(lower_bounded_semilattstr(X4)))|(empty_carrier(X4)|~(meet_semilatt_str(X4)))))),inference(distribute,[status(thm)],[251])).
% cnf(256,plain,(empty_carrier(X1)|lower_bounded_semilattstr(X1)|~meet_semilatt_str(X1)|~element(X2,the_carrier(X1))|meet(X1,esk12_2(X1,X2),X2)!=X2|meet(X1,X2,esk12_2(X1,X2))!=X2),inference(split_conjunct,[status(thm)],[252])).
% cnf(257,plain,(empty_carrier(X1)|lower_bounded_semilattstr(X1)|element(esk12_2(X1,X2),the_carrier(X1))|~meet_semilatt_str(X1)|~element(X2,the_carrier(X1))),inference(split_conjunct,[status(thm)],[252])).
% fof(303, plain,![X3]:?[X4]:(element(X4,powerset(X3))&empty(X4)),inference(variable_rename,[status(thm)],[47])).
% fof(304, plain,![X3]:(element(esk17_1(X3),powerset(X3))&empty(esk17_1(X3))),inference(skolemize,[status(esa)],[303])).
% cnf(305,plain,(empty(esk17_1(X1))),inference(split_conjunct,[status(thm)],[304])).
% cnf(306,plain,(element(esk17_1(X1),powerset(X1))),inference(split_conjunct,[status(thm)],[304])).
% fof(318, plain,![X1]:![X2]:(~(element(X2,the_carrier(boole_lattice(X1))))|![X3]:(~(element(X3,the_carrier(boole_lattice(X1))))|(join(boole_lattice(X1),X2,X3)=set_union2(X2,X3)&meet(boole_lattice(X1),X2,X3)=set_intersection2(X2,X3)))),inference(fof_nnf,[status(thm)],[51])).
% fof(319, plain,![X4]:![X5]:(~(element(X5,the_carrier(boole_lattice(X4))))|![X6]:(~(element(X6,the_carrier(boole_lattice(X4))))|(join(boole_lattice(X4),X5,X6)=set_union2(X5,X6)&meet(boole_lattice(X4),X5,X6)=set_intersection2(X5,X6)))),inference(variable_rename,[status(thm)],[318])).
% fof(320, plain,![X4]:![X5]:![X6]:((~(element(X6,the_carrier(boole_lattice(X4))))|(join(boole_lattice(X4),X5,X6)=set_union2(X5,X6)&meet(boole_lattice(X4),X5,X6)=set_intersection2(X5,X6)))|~(element(X5,the_carrier(boole_lattice(X4))))),inference(shift_quantors,[status(thm)],[319])).
% fof(321, plain,![X4]:![X5]:![X6]:(((join(boole_lattice(X4),X5,X6)=set_union2(X5,X6)|~(element(X6,the_carrier(boole_lattice(X4)))))|~(element(X5,the_carrier(boole_lattice(X4)))))&((meet(boole_lattice(X4),X5,X6)=set_intersection2(X5,X6)|~(element(X6,the_carrier(boole_lattice(X4)))))|~(element(X5,the_carrier(boole_lattice(X4)))))),inference(distribute,[status(thm)],[320])).
% cnf(322,plain,(meet(boole_lattice(X2),X1,X3)=set_intersection2(X1,X3)|~element(X1,the_carrier(boole_lattice(X2)))|~element(X3,the_carrier(boole_lattice(X2)))),inference(split_conjunct,[status(thm)],[321])).
% fof(373, plain,![X1]:(~(latt_str(X1))|(meet_semilatt_str(X1)&join_semilatt_str(X1))),inference(fof_nnf,[status(thm)],[68])).
% fof(374, plain,![X2]:(~(latt_str(X2))|(meet_semilatt_str(X2)&join_semilatt_str(X2))),inference(variable_rename,[status(thm)],[373])).
% fof(375, plain,![X2]:((meet_semilatt_str(X2)|~(latt_str(X2)))&(join_semilatt_str(X2)|~(latt_str(X2)))),inference(distribute,[status(thm)],[374])).
% cnf(377,plain,(meet_semilatt_str(X1)|~latt_str(X1)),inference(split_conjunct,[status(thm)],[375])).
% fof(417, plain,![X1]:![X2]:((~(strict_latt_str(X2))|~(latt_str(X2)))|((~(X2=boole_lattice(X1))|(the_carrier(X2)=powerset(X1)&![X3]:(~(element(X3,powerset(X1)))|![X4]:(~(element(X4,powerset(X1)))|(apply_binary(the_L_join(X2),X3,X4)=subset_union2(X1,X3,X4)&apply_binary(the_L_meet(X2),X3,X4)=subset_intersection2(X1,X3,X4))))))&((~(the_carrier(X2)=powerset(X1))|?[X3]:(element(X3,powerset(X1))&?[X4]:(element(X4,powerset(X1))&(~(apply_binary(the_L_join(X2),X3,X4)=subset_union2(X1,X3,X4))|~(apply_binary(the_L_meet(X2),X3,X4)=subset_intersection2(X1,X3,X4))))))|X2=boole_lattice(X1)))),inference(fof_nnf,[status(thm)],[77])).
% fof(418, plain,![X5]:![X6]:((~(strict_latt_str(X6))|~(latt_str(X6)))|((~(X6=boole_lattice(X5))|(the_carrier(X6)=powerset(X5)&![X7]:(~(element(X7,powerset(X5)))|![X8]:(~(element(X8,powerset(X5)))|(apply_binary(the_L_join(X6),X7,X8)=subset_union2(X5,X7,X8)&apply_binary(the_L_meet(X6),X7,X8)=subset_intersection2(X5,X7,X8))))))&((~(the_carrier(X6)=powerset(X5))|?[X9]:(element(X9,powerset(X5))&?[X10]:(element(X10,powerset(X5))&(~(apply_binary(the_L_join(X6),X9,X10)=subset_union2(X5,X9,X10))|~(apply_binary(the_L_meet(X6),X9,X10)=subset_intersection2(X5,X9,X10))))))|X6=boole_lattice(X5)))),inference(variable_rename,[status(thm)],[417])).
% fof(419, plain,![X5]:![X6]:((~(strict_latt_str(X6))|~(latt_str(X6)))|((~(X6=boole_lattice(X5))|(the_carrier(X6)=powerset(X5)&![X7]:(~(element(X7,powerset(X5)))|![X8]:(~(element(X8,powerset(X5)))|(apply_binary(the_L_join(X6),X7,X8)=subset_union2(X5,X7,X8)&apply_binary(the_L_meet(X6),X7,X8)=subset_intersection2(X5,X7,X8))))))&((~(the_carrier(X6)=powerset(X5))|(element(esk20_2(X5,X6),powerset(X5))&(element(esk21_2(X5,X6),powerset(X5))&(~(apply_binary(the_L_join(X6),esk20_2(X5,X6),esk21_2(X5,X6))=subset_union2(X5,esk20_2(X5,X6),esk21_2(X5,X6)))|~(apply_binary(the_L_meet(X6),esk20_2(X5,X6),esk21_2(X5,X6))=subset_intersection2(X5,esk20_2(X5,X6),esk21_2(X5,X6)))))))|X6=boole_lattice(X5)))),inference(skolemize,[status(esa)],[418])).
% fof(420, plain,![X5]:![X6]:![X7]:![X8]:((((((~(element(X8,powerset(X5)))|(apply_binary(the_L_join(X6),X7,X8)=subset_union2(X5,X7,X8)&apply_binary(the_L_meet(X6),X7,X8)=subset_intersection2(X5,X7,X8)))|~(element(X7,powerset(X5))))&the_carrier(X6)=powerset(X5))|~(X6=boole_lattice(X5)))&((~(the_carrier(X6)=powerset(X5))|(element(esk20_2(X5,X6),powerset(X5))&(element(esk21_2(X5,X6),powerset(X5))&(~(apply_binary(the_L_join(X6),esk20_2(X5,X6),esk21_2(X5,X6))=subset_union2(X5,esk20_2(X5,X6),esk21_2(X5,X6)))|~(apply_binary(the_L_meet(X6),esk20_2(X5,X6),esk21_2(X5,X6))=subset_intersection2(X5,esk20_2(X5,X6),esk21_2(X5,X6)))))))|X6=boole_lattice(X5)))|(~(strict_latt_str(X6))|~(latt_str(X6)))),inference(shift_quantors,[status(thm)],[419])).
% fof(421, plain,![X5]:![X6]:![X7]:![X8]:(((((((apply_binary(the_L_join(X6),X7,X8)=subset_union2(X5,X7,X8)|~(element(X8,powerset(X5))))|~(element(X7,powerset(X5))))|~(X6=boole_lattice(X5)))|(~(strict_latt_str(X6))|~(latt_str(X6))))&((((apply_binary(the_L_meet(X6),X7,X8)=subset_intersection2(X5,X7,X8)|~(element(X8,powerset(X5))))|~(element(X7,powerset(X5))))|~(X6=boole_lattice(X5)))|(~(strict_latt_str(X6))|~(latt_str(X6)))))&((the_carrier(X6)=powerset(X5)|~(X6=boole_lattice(X5)))|(~(strict_latt_str(X6))|~(latt_str(X6)))))&((((element(esk20_2(X5,X6),powerset(X5))|~(the_carrier(X6)=powerset(X5)))|X6=boole_lattice(X5))|(~(strict_latt_str(X6))|~(latt_str(X6))))&((((element(esk21_2(X5,X6),powerset(X5))|~(the_carrier(X6)=powerset(X5)))|X6=boole_lattice(X5))|(~(strict_latt_str(X6))|~(latt_str(X6))))&((((~(apply_binary(the_L_join(X6),esk20_2(X5,X6),esk21_2(X5,X6))=subset_union2(X5,esk20_2(X5,X6),esk21_2(X5,X6)))|~(apply_binary(the_L_meet(X6),esk20_2(X5,X6),esk21_2(X5,X6))=subset_intersection2(X5,esk20_2(X5,X6),esk21_2(X5,X6))))|~(the_carrier(X6)=powerset(X5)))|X6=boole_lattice(X5))|(~(strict_latt_str(X6))|~(latt_str(X6))))))),inference(distribute,[status(thm)],[420])).
% cnf(425,plain,(the_carrier(X1)=powerset(X2)|~latt_str(X1)|~strict_latt_str(X1)|X1!=boole_lattice(X2)),inference(split_conjunct,[status(thm)],[421])).
% fof(500, negated_conjecture,?[X1]:(~(lower_bounded_semilattstr(boole_lattice(X1)))|~(bottom_of_semilattstr(boole_lattice(X1))=empty_set)),inference(fof_nnf,[status(thm)],[103])).
% fof(501, negated_conjecture,?[X2]:(~(lower_bounded_semilattstr(boole_lattice(X2)))|~(bottom_of_semilattstr(boole_lattice(X2))=empty_set)),inference(variable_rename,[status(thm)],[500])).
% fof(502, negated_conjecture,(~(lower_bounded_semilattstr(boole_lattice(esk22_0)))|~(bottom_of_semilattstr(boole_lattice(esk22_0))=empty_set)),inference(skolemize,[status(esa)],[501])).
% cnf(503,negated_conjecture,(bottom_of_semilattstr(boole_lattice(esk22_0))!=empty_set|~lower_bounded_semilattstr(boole_lattice(esk22_0))),inference(split_conjunct,[status(thm)],[502])).
% cnf(512,plain,(meet_semilatt_str(boole_lattice(X1))),inference(spm,[status(thm)],[377,205,theory(equality)])).
% cnf(520,plain,(set_intersection2(empty_set,X1)=empty_set),inference(spm,[status(thm)],[145,182,theory(equality)])).
% cnf(536,plain,(empty_set=esk17_1(X1)),inference(spm,[status(thm)],[141,305,theory(equality)])).
% cnf(551,plain,(powerset(X1)=the_carrier(boole_lattice(X1))|~strict_latt_str(boole_lattice(X1))|~latt_str(boole_lattice(X1))),inference(er,[status(thm)],[425,theory(equality)])).
% cnf(552,plain,(powerset(X1)=the_carrier(boole_lattice(X1))|$false|~latt_str(boole_lattice(X1))),inference(rw,[status(thm)],[551,199,theory(equality)])).
% cnf(553,plain,(powerset(X1)=the_carrier(boole_lattice(X1))|$false|$false),inference(rw,[status(thm)],[552,205,theory(equality)])).
% cnf(554,plain,(powerset(X1)=the_carrier(boole_lattice(X1))),inference(cn,[status(thm)],[553,theory(equality)])).
% cnf(652,plain,(meet(X1,X2,bottom_of_semilattstr(X1))=bottom_of_semilattstr(X1)|empty_carrier(X1)|~lower_bounded_semilattstr(X1)|~element(X2,the_carrier(X1))|~element(bottom_of_semilattstr(X1),the_carrier(X1))|~meet_semilatt_str(X1)),inference(er,[status(thm)],[192,theory(equality)])).
% cnf(714,plain,(element(empty_set,powerset(X1))),inference(rw,[status(thm)],[306,536,theory(equality)])).
% cnf(716,plain,(element(bottom_of_semilattstr(boole_lattice(X1)),powerset(X1))|empty_carrier(boole_lattice(X1))|~meet_semilatt_str(boole_lattice(X1))),inference(spm,[status(thm)],[152,554,theory(equality)])).
% cnf(724,plain,(lower_bounded_semilattstr(boole_lattice(X1))|element(esk12_2(boole_lattice(X1),X2),powerset(X1))|empty_carrier(boole_lattice(X1))|~element(X2,powerset(X1))|~meet_semilatt_str(boole_lattice(X1))),inference(spm,[status(thm)],[257,554,theory(equality)])).
% cnf(741,plain,(meet(boole_lattice(X1),X2,X3)=set_intersection2(X2,X3)|~element(X3,powerset(X1))|~element(X2,the_carrier(boole_lattice(X1)))),inference(rw,[status(thm)],[322,554,theory(equality)])).
% cnf(742,plain,(meet(boole_lattice(X1),X2,X3)=set_intersection2(X2,X3)|~element(X3,powerset(X1))|~element(X2,powerset(X1))),inference(rw,[status(thm)],[741,554,theory(equality)])).
% cnf(743,plain,(element(bottom_of_semilattstr(boole_lattice(X1)),powerset(X1))|empty_carrier(boole_lattice(X1))|$false),inference(rw,[status(thm)],[716,512,theory(equality)])).
% cnf(744,plain,(element(bottom_of_semilattstr(boole_lattice(X1)),powerset(X1))|empty_carrier(boole_lattice(X1))),inference(cn,[status(thm)],[743,theory(equality)])).
% cnf(745,plain,(element(bottom_of_semilattstr(boole_lattice(X1)),powerset(X1))),inference(sr,[status(thm)],[744,200,theory(equality)])).
% cnf(767,plain,(lower_bounded_semilattstr(boole_lattice(X1))|element(esk12_2(boole_lattice(X1),X2),powerset(X1))|empty_carrier(boole_lattice(X1))|~element(X2,powerset(X1))|$false),inference(rw,[status(thm)],[724,512,theory(equality)])).
% cnf(768,plain,(lower_bounded_semilattstr(boole_lattice(X1))|element(esk12_2(boole_lattice(X1),X2),powerset(X1))|empty_carrier(boole_lattice(X1))|~element(X2,powerset(X1))),inference(cn,[status(thm)],[767,theory(equality)])).
% cnf(769,plain,(lower_bounded_semilattstr(boole_lattice(X1))|element(esk12_2(boole_lattice(X1),X2),powerset(X1))|~element(X2,powerset(X1))),inference(sr,[status(thm)],[768,200,theory(equality)])).
% cnf(836,plain,(lower_bounded_semilattstr(boole_lattice(X1))|empty_carrier(boole_lattice(X1))|meet(boole_lattice(X1),X2,esk12_2(boole_lattice(X1),X2))!=X2|set_intersection2(esk12_2(boole_lattice(X1),X2),X2)!=X2|~element(X2,the_carrier(boole_lattice(X1)))|~meet_semilatt_str(boole_lattice(X1))|~element(X2,powerset(X1))|~element(esk12_2(boole_lattice(X1),X2),powerset(X1))),inference(spm,[status(thm)],[256,742,theory(equality)])).
% cnf(841,plain,(lower_bounded_semilattstr(boole_lattice(X1))|empty_carrier(boole_lattice(X1))|meet(boole_lattice(X1),X2,esk12_2(boole_lattice(X1),X2))!=X2|set_intersection2(esk12_2(boole_lattice(X1),X2),X2)!=X2|~element(X2,powerset(X1))|~meet_semilatt_str(boole_lattice(X1))|~element(X2,powerset(X1))|~element(esk12_2(boole_lattice(X1),X2),powerset(X1))),inference(rw,[status(thm)],[836,554,theory(equality)])).
% cnf(842,plain,(lower_bounded_semilattstr(boole_lattice(X1))|empty_carrier(boole_lattice(X1))|meet(boole_lattice(X1),X2,esk12_2(boole_lattice(X1),X2))!=X2|set_intersection2(esk12_2(boole_lattice(X1),X2),X2)!=X2|~element(X2,powerset(X1))|$false|~element(X2,powerset(X1))|~element(esk12_2(boole_lattice(X1),X2),powerset(X1))),inference(rw,[status(thm)],[841,512,theory(equality)])).
% cnf(843,plain,(lower_bounded_semilattstr(boole_lattice(X1))|empty_carrier(boole_lattice(X1))|meet(boole_lattice(X1),X2,esk12_2(boole_lattice(X1),X2))!=X2|set_intersection2(esk12_2(boole_lattice(X1),X2),X2)!=X2|~element(X2,powerset(X1))|~element(esk12_2(boole_lattice(X1),X2),powerset(X1))),inference(cn,[status(thm)],[842,theory(equality)])).
% cnf(844,plain,(lower_bounded_semilattstr(boole_lattice(X1))|meet(boole_lattice(X1),X2,esk12_2(boole_lattice(X1),X2))!=X2|set_intersection2(esk12_2(boole_lattice(X1),X2),X2)!=X2|~element(X2,powerset(X1))|~element(esk12_2(boole_lattice(X1),X2),powerset(X1))),inference(sr,[status(thm)],[843,200,theory(equality)])).
% cnf(1492,plain,(meet(X1,X2,bottom_of_semilattstr(X1))=bottom_of_semilattstr(X1)|empty_carrier(X1)|~lower_bounded_semilattstr(X1)|~element(X2,the_carrier(X1))|~meet_semilatt_str(X1)),inference(csr,[status(thm)],[652,152])).
% cnf(1493,plain,(bottom_of_semilattstr(boole_lattice(X1))=set_intersection2(X2,bottom_of_semilattstr(boole_lattice(X1)))|empty_carrier(boole_lattice(X1))|~element(bottom_of_semilattstr(boole_lattice(X1)),powerset(X1))|~element(X2,powerset(X1))|~lower_bounded_semilattstr(boole_lattice(X1))|~element(X2,the_carrier(boole_lattice(X1)))|~meet_semilatt_str(boole_lattice(X1))),inference(spm,[status(thm)],[742,1492,theory(equality)])).
% cnf(1501,plain,(bottom_of_semilattstr(boole_lattice(X1))=set_intersection2(X2,bottom_of_semilattstr(boole_lattice(X1)))|empty_carrier(boole_lattice(X1))|$false|~element(X2,powerset(X1))|~lower_bounded_semilattstr(boole_lattice(X1))|~element(X2,the_carrier(boole_lattice(X1)))|~meet_semilatt_str(boole_lattice(X1))),inference(rw,[status(thm)],[1493,745,theory(equality)])).
% cnf(1502,plain,(bottom_of_semilattstr(boole_lattice(X1))=set_intersection2(X2,bottom_of_semilattstr(boole_lattice(X1)))|empty_carrier(boole_lattice(X1))|$false|~element(X2,powerset(X1))|~lower_bounded_semilattstr(boole_lattice(X1))|~element(X2,powerset(X1))|~meet_semilatt_str(boole_lattice(X1))),inference(rw,[status(thm)],[1501,554,theory(equality)])).
% cnf(1503,plain,(bottom_of_semilattstr(boole_lattice(X1))=set_intersection2(X2,bottom_of_semilattstr(boole_lattice(X1)))|empty_carrier(boole_lattice(X1))|$false|~element(X2,powerset(X1))|~lower_bounded_semilattstr(boole_lattice(X1))|~element(X2,powerset(X1))|$false),inference(rw,[status(thm)],[1502,512,theory(equality)])).
% cnf(1504,plain,(bottom_of_semilattstr(boole_lattice(X1))=set_intersection2(X2,bottom_of_semilattstr(boole_lattice(X1)))|empty_carrier(boole_lattice(X1))|~element(X2,powerset(X1))|~lower_bounded_semilattstr(boole_lattice(X1))),inference(cn,[status(thm)],[1503,theory(equality)])).
% cnf(1505,plain,(set_intersection2(X2,bottom_of_semilattstr(boole_lattice(X1)))=bottom_of_semilattstr(boole_lattice(X1))|~element(X2,powerset(X1))|~lower_bounded_semilattstr(boole_lattice(X1))),inference(sr,[status(thm)],[1504,200,theory(equality)])).
% cnf(1522,plain,(bottom_of_semilattstr(boole_lattice(X1))=empty_set|~lower_bounded_semilattstr(boole_lattice(X1))|~element(empty_set,powerset(X1))),inference(spm,[status(thm)],[520,1505,theory(equality)])).
% cnf(1532,plain,(bottom_of_semilattstr(boole_lattice(X1))=empty_set|~lower_bounded_semilattstr(boole_lattice(X1))|$false),inference(rw,[status(thm)],[1522,714,theory(equality)])).
% cnf(1533,plain,(bottom_of_semilattstr(boole_lattice(X1))=empty_set|~lower_bounded_semilattstr(boole_lattice(X1))),inference(cn,[status(thm)],[1532,theory(equality)])).
% cnf(1539,negated_conjecture,(~lower_bounded_semilattstr(boole_lattice(esk22_0))),inference(spm,[status(thm)],[503,1533,theory(equality)])).
% cnf(2791,plain,(lower_bounded_semilattstr(boole_lattice(X1))|meet(boole_lattice(X1),X2,esk12_2(boole_lattice(X1),X2))!=X2|set_intersection2(X2,esk12_2(boole_lattice(X1),X2))!=X2|~element(X2,powerset(X1))|~element(esk12_2(boole_lattice(X1),X2),powerset(X1))),inference(rw,[status(thm)],[844,182,theory(equality)])).
% cnf(2792,plain,(lower_bounded_semilattstr(boole_lattice(X1))|meet(boole_lattice(X1),X2,esk12_2(boole_lattice(X1),X2))!=X2|set_intersection2(X2,esk12_2(boole_lattice(X1),X2))!=X2|~element(X2,powerset(X1))),inference(csr,[status(thm)],[2791,769])).
% cnf(2796,plain,(lower_bounded_semilattstr(boole_lattice(X1))|set_intersection2(X2,esk12_2(boole_lattice(X1),X2))!=X2|~element(X2,powerset(X1))|~element(esk12_2(boole_lattice(X1),X2),powerset(X1))),inference(spm,[status(thm)],[2792,742,theory(equality)])).
% cnf(3766,plain,(lower_bounded_semilattstr(boole_lattice(X1))|set_intersection2(X2,esk12_2(boole_lattice(X1),X2))!=X2|~element(X2,powerset(X1))),inference(csr,[status(thm)],[2796,769])).
% cnf(3770,plain,(lower_bounded_semilattstr(boole_lattice(X1))|~element(empty_set,powerset(X1))),inference(spm,[status(thm)],[3766,520,theory(equality)])).
% cnf(3773,plain,(lower_bounded_semilattstr(boole_lattice(X1))|$false),inference(rw,[status(thm)],[3770,714,theory(equality)])).
% cnf(3774,plain,(lower_bounded_semilattstr(boole_lattice(X1))),inference(cn,[status(thm)],[3773,theory(equality)])).
% cnf(3890,negated_conjecture,($false),inference(rw,[status(thm)],[1539,3774,theory(equality)])).
% cnf(3891,negated_conjecture,($false),inference(cn,[status(thm)],[3890,theory(equality)])).
% cnf(3892,negated_conjecture,($false),3891,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 850
% # ...of these trivial : 8
% # ...subsumed : 452
% # ...remaining for further processing: 390
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 18
% # Backward-rewritten : 68
% # Generated clauses : 1651
% # ...of the previous two non-trivial : 1519
% # Contextual simplify-reflections : 433
% # Paramodulations : 1641
% # Factorizations : 0
% # Equation resolutions : 7
% # Current number of processed clauses: 303
% # Positive orientable unit clauses: 69
% # Positive unorientable unit clauses: 3
% # Negative unit clauses : 15
% # Non-unit-clauses : 216
% # Current number of unprocessed clauses: 325
% # ...number of literals in the above : 1464
% # Clause-clause subsumption calls (NU) : 10474
% # Rec. Clause-clause subsumption calls : 6365
% # Unit Clause-clause subsumption calls : 340
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 36
% # Indexed BW rewrite successes : 22
% # Backwards rewriting index: 332 leaves, 1.49+/-1.455 terms/leaf
% # Paramod-from index: 156 leaves, 1.17+/-0.618 terms/leaf
% # Paramod-into index: 293 leaves, 1.26+/-0.772 terms/leaf
% # -------------------------------------------------
% # User time : 0.161 s
% # System time : 0.008 s
% # Total time : 0.169 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.31 CPU 0.40 WC
% FINAL PrfWatch: 0.31 CPU 0.40 WC
% SZS output end Solution for /tmp/SystemOnTPTP6397/SEU345+1.tptp
%
%------------------------------------------------------------------------------