%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : SEU371+1 : TPTP v5.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art04.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 : Sun Dec 26 07:54:43 EST 2010
% Result : Theorem 0.43s
% Output : CNFRefutation 0.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 9
% Syntax : Number of formulae : 61 ( 19 unt; 0 def)
% Number of atoms : 311 ( 45 equ)
% Maximal formula atoms : 25 ( 5 avg)
% Number of connectives : 355 ( 105 ~; 129 |; 114 &)
% ( 0 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 25 ( 23 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 2 con; 0-2 aty)
% Number of variables : 57 ( 6 sgn 36 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(4,conjecture,
! [X1] : bottom_of_relstr(boole_POSet(X1)) = empty_set,
file('/tmp/tmpbYWV39/sel_SEU371+1.p_1',t18_yellow_1) ).
fof(5,axiom,
! [X1] :
( ~ empty_carrier(boole_lattice(X1))
& strict_latt_str(boole_lattice(X1))
& join_commutative(boole_lattice(X1))
& join_associative(boole_lattice(X1))
& meet_commutative(boole_lattice(X1))
& meet_associative(boole_lattice(X1))
& meet_absorbing(boole_lattice(X1))
& join_absorbing(boole_lattice(X1))
& lattice(boole_lattice(X1))
& distributive_lattstr(boole_lattice(X1))
& modular_lattstr(boole_lattice(X1))
& lower_bounded_semilattstr(boole_lattice(X1))
& upper_bounded_semilattstr(boole_lattice(X1))
& bounded_lattstr(boole_lattice(X1))
& complemented_lattstr(boole_lattice(X1))
& boolean_lattstr(boole_lattice(X1))
& complete_latt_str(boole_lattice(X1)) ),
file('/tmp/tmpbYWV39/sel_SEU371+1.p_1',fc1_knaster) ).
fof(11,axiom,
! [X1] :
( rel_str(X1)
=> bottom_of_relstr(X1) = join_on_relstr(X1,empty_set) ),
file('/tmp/tmpbYWV39/sel_SEU371+1.p_1',d11_yellow_0) ).
fof(40,axiom,
! [X1] :
( ( ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) )
=> ( strict_rel_str(poset_of_lattice(X1))
& reflexive_relstr(poset_of_lattice(X1))
& transitive_relstr(poset_of_lattice(X1))
& antisymmetric_relstr(poset_of_lattice(X1))
& rel_str(poset_of_lattice(X1)) ) ),
file('/tmp/tmpbYWV39/sel_SEU371+1.p_1',dt_k3_lattice3) ).
fof(58,axiom,
! [X1] :
( ( ~ empty_carrier(X1)
& lattice(X1)
& complete_latt_str(X1)
& latt_str(X1) )
=> ! [X2] :
( join_of_latt_set(X1,X2) = join_on_relstr(poset_of_lattice(X1),X2)
& meet_of_latt_set(X1,X2) = meet_on_relstr(poset_of_lattice(X1),X2) ) ),
file('/tmp/tmpbYWV39/sel_SEU371+1.p_1',t29_yellow_0) ).
fof(63,axiom,
! [X1] :
( ( ~ empty_carrier(X1)
& lattice(X1)
& complete_latt_str(X1)
& latt_str(X1) )
=> ( ~ empty_carrier(X1)
& lattice(X1)
& lower_bounded_semilattstr(X1)
& latt_str(X1)
& bottom_of_semilattstr(X1) = join_of_latt_set(X1,empty_set) ) ),
file('/tmp/tmpbYWV39/sel_SEU371+1.p_1',t50_lattice3) ).
fof(82,axiom,
! [X1] :
( strict_latt_str(boole_lattice(X1))
& latt_str(boole_lattice(X1)) ),
file('/tmp/tmpbYWV39/sel_SEU371+1.p_1',dt_k1_lattice3) ).
fof(84,axiom,
! [X1] :
( lower_bounded_semilattstr(boole_lattice(X1))
& bottom_of_semilattstr(boole_lattice(X1)) = empty_set ),
file('/tmp/tmpbYWV39/sel_SEU371+1.p_1',t3_lattice3) ).
fof(103,axiom,
! [X1] : boole_POSet(X1) = poset_of_lattice(boole_lattice(X1)),
file('/tmp/tmpbYWV39/sel_SEU371+1.p_1',d2_yellow_1) ).
fof(116,negated_conjecture,
~ ! [X1] : bottom_of_relstr(boole_POSet(X1)) = empty_set,
inference(assume_negation,[status(cth)],[4]) ).
fof(118,plain,
! [X1] :
( ~ empty_carrier(boole_lattice(X1))
& strict_latt_str(boole_lattice(X1))
& join_commutative(boole_lattice(X1))
& join_associative(boole_lattice(X1))
& meet_commutative(boole_lattice(X1))
& meet_associative(boole_lattice(X1))
& meet_absorbing(boole_lattice(X1))
& join_absorbing(boole_lattice(X1))
& lattice(boole_lattice(X1))
& distributive_lattstr(boole_lattice(X1))
& modular_lattstr(boole_lattice(X1))
& lower_bounded_semilattstr(boole_lattice(X1))
& upper_bounded_semilattstr(boole_lattice(X1))
& bounded_lattstr(boole_lattice(X1))
& complemented_lattstr(boole_lattice(X1))
& boolean_lattstr(boole_lattice(X1))
& complete_latt_str(boole_lattice(X1)) ),
inference(fof_simplification,[status(thm)],[5,theory(equality)]) ).
fof(131,plain,
! [X1] :
( ( ~ empty_carrier(X1)
& lattice(X1)
& latt_str(X1) )
=> ( strict_rel_str(poset_of_lattice(X1))
& reflexive_relstr(poset_of_lattice(X1))
& transitive_relstr(poset_of_lattice(X1))
& antisymmetric_relstr(poset_of_lattice(X1))
& rel_str(poset_of_lattice(X1)) ) ),
inference(fof_simplification,[status(thm)],[40,theory(equality)]) ).
fof(141,plain,
! [X1] :
( ( ~ empty_carrier(X1)
& lattice(X1)
& complete_latt_str(X1)
& latt_str(X1) )
=> ! [X2] :
( join_of_latt_set(X1,X2) = join_on_relstr(poset_of_lattice(X1),X2)
& meet_of_latt_set(X1,X2) = meet_on_relstr(poset_of_lattice(X1),X2) ) ),
inference(fof_simplification,[status(thm)],[58,theory(equality)]) ).
fof(143,plain,
! [X1] :
( ( ~ empty_carrier(X1)
& lattice(X1)
& complete_latt_str(X1)
& latt_str(X1) )
=> ( ~ empty_carrier(X1)
& lattice(X1)
& lower_bounded_semilattstr(X1)
& latt_str(X1)
& bottom_of_semilattstr(X1) = join_of_latt_set(X1,empty_set) ) ),
inference(fof_simplification,[status(thm)],[63,theory(equality)]) ).
fof(191,negated_conjecture,
? [X1] : bottom_of_relstr(boole_POSet(X1)) != empty_set,
inference(fof_nnf,[status(thm)],[116]) ).
fof(192,negated_conjecture,
? [X2] : bottom_of_relstr(boole_POSet(X2)) != empty_set,
inference(variable_rename,[status(thm)],[191]) ).
fof(193,negated_conjecture,
bottom_of_relstr(boole_POSet(esk3_0)) != empty_set,
inference(skolemize,[status(esa)],[192]) ).
cnf(194,negated_conjecture,
bottom_of_relstr(boole_POSet(esk3_0)) != empty_set,
inference(split_conjunct,[status(thm)],[193]) ).
fof(195,plain,
! [X2] :
( ~ empty_carrier(boole_lattice(X2))
& strict_latt_str(boole_lattice(X2))
& join_commutative(boole_lattice(X2))
& join_associative(boole_lattice(X2))
& meet_commutative(boole_lattice(X2))
& meet_associative(boole_lattice(X2))
& meet_absorbing(boole_lattice(X2))
& join_absorbing(boole_lattice(X2))
& lattice(boole_lattice(X2))
& distributive_lattstr(boole_lattice(X2))
& modular_lattstr(boole_lattice(X2))
& lower_bounded_semilattstr(boole_lattice(X2))
& upper_bounded_semilattstr(boole_lattice(X2))
& bounded_lattstr(boole_lattice(X2))
& complemented_lattstr(boole_lattice(X2))
& boolean_lattstr(boole_lattice(X2))
& complete_latt_str(boole_lattice(X2)) ),
inference(variable_rename,[status(thm)],[118]) ).
cnf(196,plain,
complete_latt_str(boole_lattice(X1)),
inference(split_conjunct,[status(thm)],[195]) ).
cnf(204,plain,
lattice(boole_lattice(X1)),
inference(split_conjunct,[status(thm)],[195]) ).
cnf(212,plain,
~ empty_carrier(boole_lattice(X1)),
inference(split_conjunct,[status(thm)],[195]) ).
fof(230,plain,
! [X1] :
( ~ rel_str(X1)
| bottom_of_relstr(X1) = join_on_relstr(X1,empty_set) ),
inference(fof_nnf,[status(thm)],[11]) ).
fof(231,plain,
! [X2] :
( ~ rel_str(X2)
| bottom_of_relstr(X2) = join_on_relstr(X2,empty_set) ),
inference(variable_rename,[status(thm)],[230]) ).
cnf(232,plain,
( bottom_of_relstr(X1) = join_on_relstr(X1,empty_set)
| ~ rel_str(X1) ),
inference(split_conjunct,[status(thm)],[231]) ).
fof(367,plain,
! [X1] :
( empty_carrier(X1)
| ~ lattice(X1)
| ~ latt_str(X1)
| ( strict_rel_str(poset_of_lattice(X1))
& reflexive_relstr(poset_of_lattice(X1))
& transitive_relstr(poset_of_lattice(X1))
& antisymmetric_relstr(poset_of_lattice(X1))
& rel_str(poset_of_lattice(X1)) ) ),
inference(fof_nnf,[status(thm)],[131]) ).
fof(368,plain,
! [X2] :
( empty_carrier(X2)
| ~ lattice(X2)
| ~ latt_str(X2)
| ( strict_rel_str(poset_of_lattice(X2))
& reflexive_relstr(poset_of_lattice(X2))
& transitive_relstr(poset_of_lattice(X2))
& antisymmetric_relstr(poset_of_lattice(X2))
& rel_str(poset_of_lattice(X2)) ) ),
inference(variable_rename,[status(thm)],[367]) ).
fof(369,plain,
! [X2] :
( ( strict_rel_str(poset_of_lattice(X2))
| empty_carrier(X2)
| ~ lattice(X2)
| ~ latt_str(X2) )
& ( reflexive_relstr(poset_of_lattice(X2))
| empty_carrier(X2)
| ~ lattice(X2)
| ~ latt_str(X2) )
& ( transitive_relstr(poset_of_lattice(X2))
| empty_carrier(X2)
| ~ lattice(X2)
| ~ latt_str(X2) )
& ( antisymmetric_relstr(poset_of_lattice(X2))
| empty_carrier(X2)
| ~ lattice(X2)
| ~ latt_str(X2) )
& ( rel_str(poset_of_lattice(X2))
| empty_carrier(X2)
| ~ lattice(X2)
| ~ latt_str(X2) ) ),
inference(distribute,[status(thm)],[368]) ).
cnf(370,plain,
( empty_carrier(X1)
| rel_str(poset_of_lattice(X1))
| ~ latt_str(X1)
| ~ lattice(X1) ),
inference(split_conjunct,[status(thm)],[369]) ).
fof(483,plain,
! [X1] :
( empty_carrier(X1)
| ~ lattice(X1)
| ~ complete_latt_str(X1)
| ~ latt_str(X1)
| ! [X2] :
( join_of_latt_set(X1,X2) = join_on_relstr(poset_of_lattice(X1),X2)
& meet_of_latt_set(X1,X2) = meet_on_relstr(poset_of_lattice(X1),X2) ) ),
inference(fof_nnf,[status(thm)],[141]) ).
fof(484,plain,
! [X3] :
( empty_carrier(X3)
| ~ lattice(X3)
| ~ complete_latt_str(X3)
| ~ latt_str(X3)
| ! [X4] :
( join_of_latt_set(X3,X4) = join_on_relstr(poset_of_lattice(X3),X4)
& meet_of_latt_set(X3,X4) = meet_on_relstr(poset_of_lattice(X3),X4) ) ),
inference(variable_rename,[status(thm)],[483]) ).
fof(485,plain,
! [X3,X4] :
( ( join_of_latt_set(X3,X4) = join_on_relstr(poset_of_lattice(X3),X4)
& meet_of_latt_set(X3,X4) = meet_on_relstr(poset_of_lattice(X3),X4) )
| empty_carrier(X3)
| ~ lattice(X3)
| ~ complete_latt_str(X3)
| ~ latt_str(X3) ),
inference(shift_quantors,[status(thm)],[484]) ).
fof(486,plain,
! [X3,X4] :
( ( join_of_latt_set(X3,X4) = join_on_relstr(poset_of_lattice(X3),X4)
| empty_carrier(X3)
| ~ lattice(X3)
| ~ complete_latt_str(X3)
| ~ latt_str(X3) )
& ( meet_of_latt_set(X3,X4) = meet_on_relstr(poset_of_lattice(X3),X4)
| empty_carrier(X3)
| ~ lattice(X3)
| ~ complete_latt_str(X3)
| ~ latt_str(X3) ) ),
inference(distribute,[status(thm)],[485]) ).
cnf(488,plain,
( empty_carrier(X1)
| join_of_latt_set(X1,X2) = join_on_relstr(poset_of_lattice(X1),X2)
| ~ latt_str(X1)
| ~ complete_latt_str(X1)
| ~ lattice(X1) ),
inference(split_conjunct,[status(thm)],[486]) ).
fof(508,plain,
! [X1] :
( empty_carrier(X1)
| ~ lattice(X1)
| ~ complete_latt_str(X1)
| ~ latt_str(X1)
| ( ~ empty_carrier(X1)
& lattice(X1)
& lower_bounded_semilattstr(X1)
& latt_str(X1)
& bottom_of_semilattstr(X1) = join_of_latt_set(X1,empty_set) ) ),
inference(fof_nnf,[status(thm)],[143]) ).
fof(509,plain,
! [X2] :
( empty_carrier(X2)
| ~ lattice(X2)
| ~ complete_latt_str(X2)
| ~ latt_str(X2)
| ( ~ empty_carrier(X2)
& lattice(X2)
& lower_bounded_semilattstr(X2)
& latt_str(X2)
& bottom_of_semilattstr(X2) = join_of_latt_set(X2,empty_set) ) ),
inference(variable_rename,[status(thm)],[508]) ).
fof(510,plain,
! [X2] :
( ( ~ empty_carrier(X2)
| empty_carrier(X2)
| ~ lattice(X2)
| ~ complete_latt_str(X2)
| ~ latt_str(X2) )
& ( lattice(X2)
| empty_carrier(X2)
| ~ lattice(X2)
| ~ complete_latt_str(X2)
| ~ latt_str(X2) )
& ( lower_bounded_semilattstr(X2)
| empty_carrier(X2)
| ~ lattice(X2)
| ~ complete_latt_str(X2)
| ~ latt_str(X2) )
& ( latt_str(X2)
| empty_carrier(X2)
| ~ lattice(X2)
| ~ complete_latt_str(X2)
| ~ latt_str(X2) )
& ( bottom_of_semilattstr(X2) = join_of_latt_set(X2,empty_set)
| empty_carrier(X2)
| ~ lattice(X2)
| ~ complete_latt_str(X2)
| ~ latt_str(X2) ) ),
inference(distribute,[status(thm)],[509]) ).
cnf(511,plain,
( empty_carrier(X1)
| bottom_of_semilattstr(X1) = join_of_latt_set(X1,empty_set)
| ~ latt_str(X1)
| ~ complete_latt_str(X1)
| ~ lattice(X1) ),
inference(split_conjunct,[status(thm)],[510]) ).
fof(615,plain,
! [X2] :
( strict_latt_str(boole_lattice(X2))
& latt_str(boole_lattice(X2)) ),
inference(variable_rename,[status(thm)],[82]) ).
cnf(616,plain,
latt_str(boole_lattice(X1)),
inference(split_conjunct,[status(thm)],[615]) ).
fof(634,plain,
! [X2] :
( lower_bounded_semilattstr(boole_lattice(X2))
& bottom_of_semilattstr(boole_lattice(X2)) = empty_set ),
inference(variable_rename,[status(thm)],[84]) ).
cnf(635,plain,
bottom_of_semilattstr(boole_lattice(X1)) = empty_set,
inference(split_conjunct,[status(thm)],[634]) ).
fof(742,plain,
! [X2] : boole_POSet(X2) = poset_of_lattice(boole_lattice(X2)),
inference(variable_rename,[status(thm)],[103]) ).
cnf(743,plain,
boole_POSet(X1) = poset_of_lattice(boole_lattice(X1)),
inference(split_conjunct,[status(thm)],[742]) ).
cnf(820,negated_conjecture,
bottom_of_relstr(poset_of_lattice(boole_lattice(esk3_0))) != empty_set,
inference(rw,[status(thm)],[194,743,theory(equality)]),
[unfolding] ).
cnf(1111,plain,
( join_of_latt_set(boole_lattice(X1),empty_set) = empty_set
| empty_carrier(boole_lattice(X1))
| ~ latt_str(boole_lattice(X1))
| ~ complete_latt_str(boole_lattice(X1))
| ~ lattice(boole_lattice(X1)) ),
inference(spm,[status(thm)],[635,511,theory(equality)]) ).
cnf(1113,plain,
( join_of_latt_set(boole_lattice(X1),empty_set) = empty_set
| empty_carrier(boole_lattice(X1))
| $false
| ~ complete_latt_str(boole_lattice(X1))
| ~ lattice(boole_lattice(X1)) ),
inference(rw,[status(thm)],[1111,616,theory(equality)]) ).
cnf(1114,plain,
( join_of_latt_set(boole_lattice(X1),empty_set) = empty_set
| empty_carrier(boole_lattice(X1))
| $false
| $false
| ~ lattice(boole_lattice(X1)) ),
inference(rw,[status(thm)],[1113,196,theory(equality)]) ).
cnf(1115,plain,
( join_of_latt_set(boole_lattice(X1),empty_set) = empty_set
| empty_carrier(boole_lattice(X1))
| $false
| $false
| $false ),
inference(rw,[status(thm)],[1114,204,theory(equality)]) ).
cnf(1116,plain,
( join_of_latt_set(boole_lattice(X1),empty_set) = empty_set
| empty_carrier(boole_lattice(X1)) ),
inference(cn,[status(thm)],[1115,theory(equality)]) ).
cnf(1117,plain,
join_of_latt_set(boole_lattice(X1),empty_set) = empty_set,
inference(sr,[status(thm)],[1116,212,theory(equality)]) ).
cnf(1175,plain,
( join_of_latt_set(X1,empty_set) = bottom_of_relstr(poset_of_lattice(X1))
| empty_carrier(X1)
| ~ rel_str(poset_of_lattice(X1))
| ~ latt_str(X1)
| ~ complete_latt_str(X1)
| ~ lattice(X1) ),
inference(spm,[status(thm)],[232,488,theory(equality)]) ).
cnf(2756,plain,
( bottom_of_relstr(poset_of_lattice(X1)) = join_of_latt_set(X1,empty_set)
| empty_carrier(X1)
| ~ latt_str(X1)
| ~ complete_latt_str(X1)
| ~ lattice(X1) ),
inference(csr,[status(thm)],[1175,370]) ).
cnf(2757,negated_conjecture,
( empty_carrier(boole_lattice(esk3_0))
| join_of_latt_set(boole_lattice(esk3_0),empty_set) != empty_set
| ~ latt_str(boole_lattice(esk3_0))
| ~ complete_latt_str(boole_lattice(esk3_0))
| ~ lattice(boole_lattice(esk3_0)) ),
inference(spm,[status(thm)],[820,2756,theory(equality)]) ).
cnf(2759,negated_conjecture,
( empty_carrier(boole_lattice(esk3_0))
| $false
| ~ latt_str(boole_lattice(esk3_0))
| ~ complete_latt_str(boole_lattice(esk3_0))
| ~ lattice(boole_lattice(esk3_0)) ),
inference(rw,[status(thm)],[2757,1117,theory(equality)]) ).
cnf(2760,negated_conjecture,
( empty_carrier(boole_lattice(esk3_0))
| $false
| $false
| ~ complete_latt_str(boole_lattice(esk3_0))
| ~ lattice(boole_lattice(esk3_0)) ),
inference(rw,[status(thm)],[2759,616,theory(equality)]) ).
cnf(2761,negated_conjecture,
( empty_carrier(boole_lattice(esk3_0))
| $false
| $false
| $false
| ~ lattice(boole_lattice(esk3_0)) ),
inference(rw,[status(thm)],[2760,196,theory(equality)]) ).
cnf(2762,negated_conjecture,
( empty_carrier(boole_lattice(esk3_0))
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[2761,204,theory(equality)]) ).
cnf(2763,negated_conjecture,
empty_carrier(boole_lattice(esk3_0)),
inference(cn,[status(thm)],[2762,theory(equality)]) ).
cnf(2764,negated_conjecture,
$false,
inference(sr,[status(thm)],[2763,212,theory(equality)]) ).
cnf(2765,negated_conjecture,
$false,
2764,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/SEU/SEU371+1.p
% --creating new selector for []
% -running prover on /tmp/tmpbYWV39/sel_SEU371+1.p_1 with time limit 29
% -prover status Theorem
% Problem SEU371+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/SEU/SEU371+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/SEU/SEU371+1.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% See solution above
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------