%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : SEU224+2 : TPTP v5.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art06.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 05:52:09 EST 2010
% Result : Theorem 0.86s
% Output : CNFRefutation 0.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 2
% Syntax : Number of formulae : 33 ( 6 unt; 0 def)
% Number of atoms : 121 ( 0 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 140 ( 52 ~; 55 |; 27 &)
% ( 3 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 33 ( 1 sgn 18 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(92,conjecture,
! [X1,X2,X3] :
( ( relation(X3)
& function(X3) )
=> ( in(X2,relation_dom(relation_dom_restriction(X3,X1)))
<=> ( in(X2,relation_dom(X3))
& in(X2,X1) ) ) ),
file('/tmp/tmpzZcb6H/sel_SEU224+2.p_1',l82_funct_1) ).
fof(178,axiom,
! [X1,X2,X3] :
( relation(X3)
=> ( in(X1,relation_dom(relation_dom_restriction(X3,X2)))
<=> ( in(X1,X2)
& in(X1,relation_dom(X3)) ) ) ),
file('/tmp/tmpzZcb6H/sel_SEU224+2.p_1',t86_relat_1) ).
fof(240,negated_conjecture,
~ ! [X1,X2,X3] :
( ( relation(X3)
& function(X3) )
=> ( in(X2,relation_dom(relation_dom_restriction(X3,X1)))
<=> ( in(X2,relation_dom(X3))
& in(X2,X1) ) ) ),
inference(assume_negation,[status(cth)],[92]) ).
fof(641,negated_conjecture,
? [X1,X2,X3] :
( relation(X3)
& function(X3)
& ( ~ in(X2,relation_dom(relation_dom_restriction(X3,X1)))
| ~ in(X2,relation_dom(X3))
| ~ in(X2,X1) )
& ( in(X2,relation_dom(relation_dom_restriction(X3,X1)))
| ( in(X2,relation_dom(X3))
& in(X2,X1) ) ) ),
inference(fof_nnf,[status(thm)],[240]) ).
fof(642,negated_conjecture,
? [X4,X5,X6] :
( relation(X6)
& function(X6)
& ( ~ in(X5,relation_dom(relation_dom_restriction(X6,X4)))
| ~ in(X5,relation_dom(X6))
| ~ in(X5,X4) )
& ( in(X5,relation_dom(relation_dom_restriction(X6,X4)))
| ( in(X5,relation_dom(X6))
& in(X5,X4) ) ) ),
inference(variable_rename,[status(thm)],[641]) ).
fof(643,negated_conjecture,
( relation(esk33_0)
& function(esk33_0)
& ( ~ in(esk32_0,relation_dom(relation_dom_restriction(esk33_0,esk31_0)))
| ~ in(esk32_0,relation_dom(esk33_0))
| ~ in(esk32_0,esk31_0) )
& ( in(esk32_0,relation_dom(relation_dom_restriction(esk33_0,esk31_0)))
| ( in(esk32_0,relation_dom(esk33_0))
& in(esk32_0,esk31_0) ) ) ),
inference(skolemize,[status(esa)],[642]) ).
fof(644,negated_conjecture,
( relation(esk33_0)
& function(esk33_0)
& ( ~ in(esk32_0,relation_dom(relation_dom_restriction(esk33_0,esk31_0)))
| ~ in(esk32_0,relation_dom(esk33_0))
| ~ in(esk32_0,esk31_0) )
& ( in(esk32_0,relation_dom(esk33_0))
| in(esk32_0,relation_dom(relation_dom_restriction(esk33_0,esk31_0))) )
& ( in(esk32_0,esk31_0)
| in(esk32_0,relation_dom(relation_dom_restriction(esk33_0,esk31_0))) ) ),
inference(distribute,[status(thm)],[643]) ).
cnf(645,negated_conjecture,
( in(esk32_0,relation_dom(relation_dom_restriction(esk33_0,esk31_0)))
| in(esk32_0,esk31_0) ),
inference(split_conjunct,[status(thm)],[644]) ).
cnf(646,negated_conjecture,
( in(esk32_0,relation_dom(relation_dom_restriction(esk33_0,esk31_0)))
| in(esk32_0,relation_dom(esk33_0)) ),
inference(split_conjunct,[status(thm)],[644]) ).
cnf(647,negated_conjecture,
( ~ in(esk32_0,esk31_0)
| ~ in(esk32_0,relation_dom(esk33_0))
| ~ in(esk32_0,relation_dom(relation_dom_restriction(esk33_0,esk31_0))) ),
inference(split_conjunct,[status(thm)],[644]) ).
cnf(649,negated_conjecture,
relation(esk33_0),
inference(split_conjunct,[status(thm)],[644]) ).
fof(988,plain,
! [X1,X2,X3] :
( ~ relation(X3)
| ( ( ~ in(X1,relation_dom(relation_dom_restriction(X3,X2)))
| ( in(X1,X2)
& in(X1,relation_dom(X3)) ) )
& ( ~ in(X1,X2)
| ~ in(X1,relation_dom(X3))
| in(X1,relation_dom(relation_dom_restriction(X3,X2))) ) ) ),
inference(fof_nnf,[status(thm)],[178]) ).
fof(989,plain,
! [X4,X5,X6] :
( ~ relation(X6)
| ( ( ~ in(X4,relation_dom(relation_dom_restriction(X6,X5)))
| ( in(X4,X5)
& in(X4,relation_dom(X6)) ) )
& ( ~ in(X4,X5)
| ~ in(X4,relation_dom(X6))
| in(X4,relation_dom(relation_dom_restriction(X6,X5))) ) ) ),
inference(variable_rename,[status(thm)],[988]) ).
fof(990,plain,
! [X4,X5,X6] :
( ( in(X4,X5)
| ~ in(X4,relation_dom(relation_dom_restriction(X6,X5)))
| ~ relation(X6) )
& ( in(X4,relation_dom(X6))
| ~ in(X4,relation_dom(relation_dom_restriction(X6,X5)))
| ~ relation(X6) )
& ( ~ in(X4,X5)
| ~ in(X4,relation_dom(X6))
| in(X4,relation_dom(relation_dom_restriction(X6,X5)))
| ~ relation(X6) ) ),
inference(distribute,[status(thm)],[989]) ).
cnf(991,plain,
( in(X2,relation_dom(relation_dom_restriction(X1,X3)))
| ~ relation(X1)
| ~ in(X2,relation_dom(X1))
| ~ in(X2,X3) ),
inference(split_conjunct,[status(thm)],[990]) ).
cnf(992,plain,
( in(X2,relation_dom(X1))
| ~ relation(X1)
| ~ in(X2,relation_dom(relation_dom_restriction(X1,X3))) ),
inference(split_conjunct,[status(thm)],[990]) ).
cnf(993,plain,
( in(X2,X3)
| ~ relation(X1)
| ~ in(X2,relation_dom(relation_dom_restriction(X1,X3))) ),
inference(split_conjunct,[status(thm)],[990]) ).
cnf(1527,negated_conjecture,
( in(esk32_0,esk31_0)
| ~ relation(esk33_0) ),
inference(spm,[status(thm)],[993,645,theory(equality)]) ).
cnf(1531,negated_conjecture,
( in(esk32_0,esk31_0)
| $false ),
inference(rw,[status(thm)],[1527,649,theory(equality)]) ).
cnf(1532,negated_conjecture,
in(esk32_0,esk31_0),
inference(cn,[status(thm)],[1531,theory(equality)]) ).
cnf(1607,negated_conjecture,
( in(esk32_0,relation_dom(esk33_0))
| ~ relation(esk33_0) ),
inference(spm,[status(thm)],[992,646,theory(equality)]) ).
cnf(1612,negated_conjecture,
( in(esk32_0,relation_dom(esk33_0))
| $false ),
inference(rw,[status(thm)],[1607,649,theory(equality)]) ).
cnf(1613,negated_conjecture,
in(esk32_0,relation_dom(esk33_0)),
inference(cn,[status(thm)],[1612,theory(equality)]) ).
cnf(7297,negated_conjecture,
( ~ in(esk32_0,relation_dom(relation_dom_restriction(esk33_0,esk31_0)))
| ~ in(esk32_0,relation_dom(esk33_0))
| $false ),
inference(rw,[status(thm)],[647,1532,theory(equality)]) ).
cnf(7298,negated_conjecture,
( ~ in(esk32_0,relation_dom(relation_dom_restriction(esk33_0,esk31_0)))
| ~ in(esk32_0,relation_dom(esk33_0)) ),
inference(cn,[status(thm)],[7297,theory(equality)]) ).
cnf(7343,negated_conjecture,
( ~ in(esk32_0,relation_dom(relation_dom_restriction(esk33_0,esk31_0)))
| $false ),
inference(rw,[status(thm)],[7298,1613,theory(equality)]) ).
cnf(7344,negated_conjecture,
~ in(esk32_0,relation_dom(relation_dom_restriction(esk33_0,esk31_0))),
inference(cn,[status(thm)],[7343,theory(equality)]) ).
cnf(7354,plain,
( ~ in(esk32_0,relation_dom(esk33_0))
| ~ in(esk32_0,esk31_0)
| ~ relation(esk33_0) ),
inference(spm,[status(thm)],[7344,991,theory(equality)]) ).
cnf(7358,plain,
( $false
| ~ in(esk32_0,esk31_0)
| ~ relation(esk33_0) ),
inference(rw,[status(thm)],[7354,1613,theory(equality)]) ).
cnf(7359,plain,
( $false
| $false
| ~ relation(esk33_0) ),
inference(rw,[status(thm)],[7358,1532,theory(equality)]) ).
cnf(7360,plain,
( $false
| $false
| $false ),
inference(rw,[status(thm)],[7359,649,theory(equality)]) ).
cnf(7361,plain,
$false,
inference(cn,[status(thm)],[7360,theory(equality)]) ).
cnf(7362,plain,
$false,
7361,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/SEU/SEU224+2.p
% --creating new selector for []
% -running prover on /tmp/tmpzZcb6H/sel_SEU224+2.p_1 with time limit 29
% -prover status Theorem
% Problem SEU224+2.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/SEU/SEU224+2.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/SEU/SEU224+2.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
%
%------------------------------------------------------------------------------