%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : SEU101+1 : TPTP v5.0.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art05.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 04:36:02 EST 2010
% Result : Theorem 0.26s
% Output : CNFRefutation 0.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 4
% Syntax : Number of formulae : 66 ( 8 unt; 0 def)
% Number of atoms : 283 ( 0 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 347 ( 130 ~; 145 |; 63 &)
% ( 5 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-2 aty)
% Number of variables : 89 ( 0 sgn 56 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(2,axiom,
! [X1] :
( cup_closed(X1)
<=> ! [X2,X3] :
( ( in(X2,X1)
& in(X3,X1) )
=> in(set_union2(X2,X3),X1) ) ),
file('/tmp/tmpHisXVQ/sel_SEU101+1.p_1',d1_finsub_1) ).
fof(12,axiom,
! [X1] :
( preboolean(X1)
<=> ( cup_closed(X1)
& diff_closed(X1) ) ),
file('/tmp/tmpHisXVQ/sel_SEU101+1.p_1',d4_finsub_1) ).
fof(32,axiom,
! [X1] :
( diff_closed(X1)
<=> ! [X2,X3] :
( ( in(X2,X1)
& in(X3,X1) )
=> in(set_difference(X2,X3),X1) ) ),
file('/tmp/tmpHisXVQ/sel_SEU101+1.p_1',d3_finsub_1) ).
fof(36,conjecture,
! [X1] :
( preboolean(X1)
<=> ! [X2,X3] :
( ( in(X2,X1)
& in(X3,X1) )
=> ( in(set_union2(X2,X3),X1)
& in(set_difference(X2,X3),X1) ) ) ),
file('/tmp/tmpHisXVQ/sel_SEU101+1.p_1',t10_finsub_1) ).
fof(40,negated_conjecture,
~ ! [X1] :
( preboolean(X1)
<=> ! [X2,X3] :
( ( in(X2,X1)
& in(X3,X1) )
=> ( in(set_union2(X2,X3),X1)
& in(set_difference(X2,X3),X1) ) ) ),
inference(assume_negation,[status(cth)],[36]) ).
fof(54,plain,
! [X1] :
( ( ~ cup_closed(X1)
| ! [X2,X3] :
( ~ in(X2,X1)
| ~ in(X3,X1)
| in(set_union2(X2,X3),X1) ) )
& ( ? [X2,X3] :
( in(X2,X1)
& in(X3,X1)
& ~ in(set_union2(X2,X3),X1) )
| cup_closed(X1) ) ),
inference(fof_nnf,[status(thm)],[2]) ).
fof(55,plain,
! [X4] :
( ( ~ cup_closed(X4)
| ! [X5,X6] :
( ~ in(X5,X4)
| ~ in(X6,X4)
| in(set_union2(X5,X6),X4) ) )
& ( ? [X7,X8] :
( in(X7,X4)
& in(X8,X4)
& ~ in(set_union2(X7,X8),X4) )
| cup_closed(X4) ) ),
inference(variable_rename,[status(thm)],[54]) ).
fof(56,plain,
! [X4] :
( ( ~ cup_closed(X4)
| ! [X5,X6] :
( ~ in(X5,X4)
| ~ in(X6,X4)
| in(set_union2(X5,X6),X4) ) )
& ( ( in(esk1_1(X4),X4)
& in(esk2_1(X4),X4)
& ~ in(set_union2(esk1_1(X4),esk2_1(X4)),X4) )
| cup_closed(X4) ) ),
inference(skolemize,[status(esa)],[55]) ).
fof(57,plain,
! [X4,X5,X6] :
( ( ~ in(X5,X4)
| ~ in(X6,X4)
| in(set_union2(X5,X6),X4)
| ~ cup_closed(X4) )
& ( ( in(esk1_1(X4),X4)
& in(esk2_1(X4),X4)
& ~ in(set_union2(esk1_1(X4),esk2_1(X4)),X4) )
| cup_closed(X4) ) ),
inference(shift_quantors,[status(thm)],[56]) ).
fof(58,plain,
! [X4,X5,X6] :
( ( ~ in(X5,X4)
| ~ in(X6,X4)
| in(set_union2(X5,X6),X4)
| ~ cup_closed(X4) )
& ( in(esk1_1(X4),X4)
| cup_closed(X4) )
& ( in(esk2_1(X4),X4)
| cup_closed(X4) )
& ( ~ in(set_union2(esk1_1(X4),esk2_1(X4)),X4)
| cup_closed(X4) ) ),
inference(distribute,[status(thm)],[57]) ).
cnf(59,plain,
( cup_closed(X1)
| ~ in(set_union2(esk1_1(X1),esk2_1(X1)),X1) ),
inference(split_conjunct,[status(thm)],[58]) ).
cnf(60,plain,
( cup_closed(X1)
| in(esk2_1(X1),X1) ),
inference(split_conjunct,[status(thm)],[58]) ).
cnf(61,plain,
( cup_closed(X1)
| in(esk1_1(X1),X1) ),
inference(split_conjunct,[status(thm)],[58]) ).
cnf(62,plain,
( in(set_union2(X2,X3),X1)
| ~ cup_closed(X1)
| ~ in(X3,X1)
| ~ in(X2,X1) ),
inference(split_conjunct,[status(thm)],[58]) ).
fof(109,plain,
! [X1] :
( ( ~ preboolean(X1)
| ( cup_closed(X1)
& diff_closed(X1) ) )
& ( ~ cup_closed(X1)
| ~ diff_closed(X1)
| preboolean(X1) ) ),
inference(fof_nnf,[status(thm)],[12]) ).
fof(110,plain,
! [X2] :
( ( ~ preboolean(X2)
| ( cup_closed(X2)
& diff_closed(X2) ) )
& ( ~ cup_closed(X2)
| ~ diff_closed(X2)
| preboolean(X2) ) ),
inference(variable_rename,[status(thm)],[109]) ).
fof(111,plain,
! [X2] :
( ( cup_closed(X2)
| ~ preboolean(X2) )
& ( diff_closed(X2)
| ~ preboolean(X2) )
& ( ~ cup_closed(X2)
| ~ diff_closed(X2)
| preboolean(X2) ) ),
inference(distribute,[status(thm)],[110]) ).
cnf(112,plain,
( preboolean(X1)
| ~ diff_closed(X1)
| ~ cup_closed(X1) ),
inference(split_conjunct,[status(thm)],[111]) ).
cnf(113,plain,
( diff_closed(X1)
| ~ preboolean(X1) ),
inference(split_conjunct,[status(thm)],[111]) ).
cnf(114,plain,
( cup_closed(X1)
| ~ preboolean(X1) ),
inference(split_conjunct,[status(thm)],[111]) ).
fof(169,plain,
! [X1] :
( ( ~ diff_closed(X1)
| ! [X2,X3] :
( ~ in(X2,X1)
| ~ in(X3,X1)
| in(set_difference(X2,X3),X1) ) )
& ( ? [X2,X3] :
( in(X2,X1)
& in(X3,X1)
& ~ in(set_difference(X2,X3),X1) )
| diff_closed(X1) ) ),
inference(fof_nnf,[status(thm)],[32]) ).
fof(170,plain,
! [X4] :
( ( ~ diff_closed(X4)
| ! [X5,X6] :
( ~ in(X5,X4)
| ~ in(X6,X4)
| in(set_difference(X5,X6),X4) ) )
& ( ? [X7,X8] :
( in(X7,X4)
& in(X8,X4)
& ~ in(set_difference(X7,X8),X4) )
| diff_closed(X4) ) ),
inference(variable_rename,[status(thm)],[169]) ).
fof(171,plain,
! [X4] :
( ( ~ diff_closed(X4)
| ! [X5,X6] :
( ~ in(X5,X4)
| ~ in(X6,X4)
| in(set_difference(X5,X6),X4) ) )
& ( ( in(esk9_1(X4),X4)
& in(esk10_1(X4),X4)
& ~ in(set_difference(esk9_1(X4),esk10_1(X4)),X4) )
| diff_closed(X4) ) ),
inference(skolemize,[status(esa)],[170]) ).
fof(172,plain,
! [X4,X5,X6] :
( ( ~ in(X5,X4)
| ~ in(X6,X4)
| in(set_difference(X5,X6),X4)
| ~ diff_closed(X4) )
& ( ( in(esk9_1(X4),X4)
& in(esk10_1(X4),X4)
& ~ in(set_difference(esk9_1(X4),esk10_1(X4)),X4) )
| diff_closed(X4) ) ),
inference(shift_quantors,[status(thm)],[171]) ).
fof(173,plain,
! [X4,X5,X6] :
( ( ~ in(X5,X4)
| ~ in(X6,X4)
| in(set_difference(X5,X6),X4)
| ~ diff_closed(X4) )
& ( in(esk9_1(X4),X4)
| diff_closed(X4) )
& ( in(esk10_1(X4),X4)
| diff_closed(X4) )
& ( ~ in(set_difference(esk9_1(X4),esk10_1(X4)),X4)
| diff_closed(X4) ) ),
inference(distribute,[status(thm)],[172]) ).
cnf(174,plain,
( diff_closed(X1)
| ~ in(set_difference(esk9_1(X1),esk10_1(X1)),X1) ),
inference(split_conjunct,[status(thm)],[173]) ).
cnf(175,plain,
( diff_closed(X1)
| in(esk10_1(X1),X1) ),
inference(split_conjunct,[status(thm)],[173]) ).
cnf(176,plain,
( diff_closed(X1)
| in(esk9_1(X1),X1) ),
inference(split_conjunct,[status(thm)],[173]) ).
cnf(177,plain,
( in(set_difference(X2,X3),X1)
| ~ diff_closed(X1)
| ~ in(X3,X1)
| ~ in(X2,X1) ),
inference(split_conjunct,[status(thm)],[173]) ).
fof(191,negated_conjecture,
? [X1] :
( ( ~ preboolean(X1)
| ? [X2,X3] :
( in(X2,X1)
& in(X3,X1)
& ( ~ in(set_union2(X2,X3),X1)
| ~ in(set_difference(X2,X3),X1) ) ) )
& ( preboolean(X1)
| ! [X2,X3] :
( ~ in(X2,X1)
| ~ in(X3,X1)
| ( in(set_union2(X2,X3),X1)
& in(set_difference(X2,X3),X1) ) ) ) ),
inference(fof_nnf,[status(thm)],[40]) ).
fof(192,negated_conjecture,
? [X4] :
( ( ~ preboolean(X4)
| ? [X5,X6] :
( in(X5,X4)
& in(X6,X4)
& ( ~ in(set_union2(X5,X6),X4)
| ~ in(set_difference(X5,X6),X4) ) ) )
& ( preboolean(X4)
| ! [X7,X8] :
( ~ in(X7,X4)
| ~ in(X8,X4)
| ( in(set_union2(X7,X8),X4)
& in(set_difference(X7,X8),X4) ) ) ) ),
inference(variable_rename,[status(thm)],[191]) ).
fof(193,negated_conjecture,
( ( ~ preboolean(esk13_0)
| ( in(esk14_0,esk13_0)
& in(esk15_0,esk13_0)
& ( ~ in(set_union2(esk14_0,esk15_0),esk13_0)
| ~ in(set_difference(esk14_0,esk15_0),esk13_0) ) ) )
& ( preboolean(esk13_0)
| ! [X7,X8] :
( ~ in(X7,esk13_0)
| ~ in(X8,esk13_0)
| ( in(set_union2(X7,X8),esk13_0)
& in(set_difference(X7,X8),esk13_0) ) ) ) ),
inference(skolemize,[status(esa)],[192]) ).
fof(194,negated_conjecture,
! [X7,X8] :
( ( ~ in(X7,esk13_0)
| ~ in(X8,esk13_0)
| ( in(set_union2(X7,X8),esk13_0)
& in(set_difference(X7,X8),esk13_0) )
| preboolean(esk13_0) )
& ( ~ preboolean(esk13_0)
| ( in(esk14_0,esk13_0)
& in(esk15_0,esk13_0)
& ( ~ in(set_union2(esk14_0,esk15_0),esk13_0)
| ~ in(set_difference(esk14_0,esk15_0),esk13_0) ) ) ) ),
inference(shift_quantors,[status(thm)],[193]) ).
fof(195,negated_conjecture,
! [X7,X8] :
( ( in(set_union2(X7,X8),esk13_0)
| ~ in(X7,esk13_0)
| ~ in(X8,esk13_0)
| preboolean(esk13_0) )
& ( in(set_difference(X7,X8),esk13_0)
| ~ in(X7,esk13_0)
| ~ in(X8,esk13_0)
| preboolean(esk13_0) )
& ( in(esk14_0,esk13_0)
| ~ preboolean(esk13_0) )
& ( in(esk15_0,esk13_0)
| ~ preboolean(esk13_0) )
& ( ~ in(set_union2(esk14_0,esk15_0),esk13_0)
| ~ in(set_difference(esk14_0,esk15_0),esk13_0)
| ~ preboolean(esk13_0) ) ),
inference(distribute,[status(thm)],[194]) ).
cnf(196,negated_conjecture,
( ~ preboolean(esk13_0)
| ~ in(set_difference(esk14_0,esk15_0),esk13_0)
| ~ in(set_union2(esk14_0,esk15_0),esk13_0) ),
inference(split_conjunct,[status(thm)],[195]) ).
cnf(197,negated_conjecture,
( in(esk15_0,esk13_0)
| ~ preboolean(esk13_0) ),
inference(split_conjunct,[status(thm)],[195]) ).
cnf(198,negated_conjecture,
( in(esk14_0,esk13_0)
| ~ preboolean(esk13_0) ),
inference(split_conjunct,[status(thm)],[195]) ).
cnf(199,negated_conjecture,
( preboolean(esk13_0)
| in(set_difference(X2,X1),esk13_0)
| ~ in(X1,esk13_0)
| ~ in(X2,esk13_0) ),
inference(split_conjunct,[status(thm)],[195]) ).
cnf(200,negated_conjecture,
( preboolean(esk13_0)
| in(set_union2(X2,X1),esk13_0)
| ~ in(X1,esk13_0)
| ~ in(X2,esk13_0) ),
inference(split_conjunct,[status(thm)],[195]) ).
cnf(277,negated_conjecture,
( cup_closed(esk13_0)
| preboolean(esk13_0)
| ~ in(esk1_1(esk13_0),esk13_0)
| ~ in(esk2_1(esk13_0),esk13_0) ),
inference(spm,[status(thm)],[59,200,theory(equality)]) ).
cnf(278,negated_conjecture,
( diff_closed(esk13_0)
| preboolean(esk13_0)
| ~ in(esk9_1(esk13_0),esk13_0)
| ~ in(esk10_1(esk13_0),esk13_0) ),
inference(spm,[status(thm)],[174,199,theory(equality)]) ).
cnf(444,negated_conjecture,
( preboolean(esk13_0)
| cup_closed(esk13_0)
| ~ in(esk1_1(esk13_0),esk13_0) ),
inference(csr,[status(thm)],[277,60]) ).
cnf(445,negated_conjecture,
( preboolean(esk13_0)
| cup_closed(esk13_0) ),
inference(csr,[status(thm)],[444,61]) ).
cnf(446,negated_conjecture,
cup_closed(esk13_0),
inference(csr,[status(thm)],[445,114]) ).
cnf(447,negated_conjecture,
( preboolean(esk13_0)
| diff_closed(esk13_0)
| ~ in(esk9_1(esk13_0),esk13_0) ),
inference(csr,[status(thm)],[278,175]) ).
cnf(448,negated_conjecture,
( preboolean(esk13_0)
| diff_closed(esk13_0) ),
inference(csr,[status(thm)],[447,176]) ).
cnf(449,negated_conjecture,
diff_closed(esk13_0),
inference(csr,[status(thm)],[448,113]) ).
cnf(450,negated_conjecture,
( preboolean(esk13_0)
| ~ cup_closed(esk13_0) ),
inference(spm,[status(thm)],[112,449,theory(equality)]) ).
cnf(451,negated_conjecture,
( preboolean(esk13_0)
| $false ),
inference(rw,[status(thm)],[450,446,theory(equality)]) ).
cnf(452,negated_conjecture,
preboolean(esk13_0),
inference(cn,[status(thm)],[451,theory(equality)]) ).
cnf(455,negated_conjecture,
( $false
| ~ in(set_union2(esk14_0,esk15_0),esk13_0)
| ~ in(set_difference(esk14_0,esk15_0),esk13_0) ),
inference(rw,[status(thm)],[196,452,theory(equality)]) ).
cnf(456,negated_conjecture,
( ~ in(set_union2(esk14_0,esk15_0),esk13_0)
| ~ in(set_difference(esk14_0,esk15_0),esk13_0) ),
inference(cn,[status(thm)],[455,theory(equality)]) ).
cnf(459,negated_conjecture,
( in(esk15_0,esk13_0)
| $false ),
inference(rw,[status(thm)],[197,452,theory(equality)]) ).
cnf(460,negated_conjecture,
in(esk15_0,esk13_0),
inference(cn,[status(thm)],[459,theory(equality)]) ).
cnf(461,negated_conjecture,
( in(esk14_0,esk13_0)
| $false ),
inference(rw,[status(thm)],[198,452,theory(equality)]) ).
cnf(462,negated_conjecture,
in(esk14_0,esk13_0),
inference(cn,[status(thm)],[461,theory(equality)]) ).
cnf(465,negated_conjecture,
( ~ in(set_union2(esk14_0,esk15_0),esk13_0)
| ~ diff_closed(esk13_0)
| ~ in(esk15_0,esk13_0)
| ~ in(esk14_0,esk13_0) ),
inference(spm,[status(thm)],[456,177,theory(equality)]) ).
cnf(466,negated_conjecture,
( ~ in(set_union2(esk14_0,esk15_0),esk13_0)
| $false
| ~ in(esk15_0,esk13_0)
| ~ in(esk14_0,esk13_0) ),
inference(rw,[status(thm)],[465,449,theory(equality)]) ).
cnf(467,negated_conjecture,
( ~ in(set_union2(esk14_0,esk15_0),esk13_0)
| $false
| $false
| ~ in(esk14_0,esk13_0) ),
inference(rw,[status(thm)],[466,460,theory(equality)]) ).
cnf(468,negated_conjecture,
( ~ in(set_union2(esk14_0,esk15_0),esk13_0)
| ~ in(esk14_0,esk13_0) ),
inference(cn,[status(thm)],[467,theory(equality)]) ).
cnf(469,negated_conjecture,
( ~ in(esk14_0,esk13_0)
| ~ in(esk15_0,esk13_0)
| ~ cup_closed(esk13_0) ),
inference(spm,[status(thm)],[468,62,theory(equality)]) ).
cnf(470,negated_conjecture,
( ~ in(esk14_0,esk13_0)
| $false
| ~ cup_closed(esk13_0) ),
inference(rw,[status(thm)],[469,460,theory(equality)]) ).
cnf(471,negated_conjecture,
( ~ in(esk14_0,esk13_0)
| $false
| $false ),
inference(rw,[status(thm)],[470,446,theory(equality)]) ).
cnf(472,negated_conjecture,
~ in(esk14_0,esk13_0),
inference(cn,[status(thm)],[471,theory(equality)]) ).
cnf(473,negated_conjecture,
$false,
inference(sr,[status(thm)],[462,472,theory(equality)]) ).
cnf(474,negated_conjecture,
$false,
473,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/SEU/SEU101+1.p
% --creating new selector for []
% -running prover on /tmp/tmpHisXVQ/sel_SEU101+1.p_1 with time limit 29
% -prover status Theorem
% Problem SEU101+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/SEU/SEU101+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/SEU/SEU101+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
%
%------------------------------------------------------------------------------