%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : NUM388+1 : TPTP v7.0.0. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : n091.star.cs.uiowa.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz
% Memory : 32218.625MB
% OS : Linux 3.10.0-693.2.2.el7.x86_64
% CPULimit : 300s
% DateTime : Mon Jan 8 15:21:14 EST 2018
% Result : Theorem 0.07s
% Output : CNFRefutation 0.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 7
% Syntax : Number of formulae : 49 ( 10 unt; 0 def)
% Number of atoms : 152 ( 0 equ)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 160 ( 57 ~; 54 |; 35 &)
% ( 2 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 8 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-1 aty)
% Number of variables : 76 ( 1 sgn 49 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(2,axiom,
! [X1] :
( ordinal(X1)
=> ( epsilon_transitive(X1)
& epsilon_connected(X1) ) ),
file('/export/starexec/sandbox/tmp/tmppf8G1Q/sel_theBenchmark.p_1',cc1_ordinal1) ).
fof(5,conjecture,
! [X1] :
( ordinal(X1)
=> ! [X2] :
( ordinal(X2)
=> ! [X3] :
( epsilon_transitive(X3)
=> ( ( in(X3,X1)
& in(X1,X2) )
=> in(X3,X2) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmppf8G1Q/sel_theBenchmark.p_1',t19_ordinal1) ).
fof(10,axiom,
! [X1,X2,X3] :
( ( in(X1,X2)
& element(X2,powerset(X3)) )
=> element(X1,X3) ),
file('/export/starexec/sandbox/tmp/tmppf8G1Q/sel_theBenchmark.p_1',t4_subset) ).
fof(12,axiom,
! [X1,X2] :
~ ( in(X1,X2)
& empty(X2) ),
file('/export/starexec/sandbox/tmp/tmppf8G1Q/sel_theBenchmark.p_1',t7_boole) ).
fof(14,axiom,
! [X1] :
( epsilon_transitive(X1)
<=> ! [X2] :
( in(X2,X1)
=> subset(X2,X1) ) ),
file('/export/starexec/sandbox/tmp/tmppf8G1Q/sel_theBenchmark.p_1',d2_ordinal1) ).
fof(20,axiom,
! [X1,X2] :
( element(X1,X2)
=> ( empty(X2)
| in(X1,X2) ) ),
file('/export/starexec/sandbox/tmp/tmppf8G1Q/sel_theBenchmark.p_1',t2_subset) ).
fof(21,axiom,
! [X1,X2] :
( element(X1,powerset(X2))
<=> subset(X1,X2) ),
file('/export/starexec/sandbox/tmp/tmppf8G1Q/sel_theBenchmark.p_1',t3_subset) ).
fof(33,negated_conjecture,
~ ! [X1] :
( ordinal(X1)
=> ! [X2] :
( ordinal(X2)
=> ! [X3] :
( epsilon_transitive(X3)
=> ( ( in(X3,X1)
& in(X1,X2) )
=> in(X3,X2) ) ) ) ),
inference(assume_negation,[status(cth)],[5]) ).
fof(42,plain,
! [X1] :
( ~ ordinal(X1)
| ( epsilon_transitive(X1)
& epsilon_connected(X1) ) ),
inference(fof_nnf,[status(thm)],[2]) ).
fof(43,plain,
! [X2] :
( ~ ordinal(X2)
| ( epsilon_transitive(X2)
& epsilon_connected(X2) ) ),
inference(variable_rename,[status(thm)],[42]) ).
fof(44,plain,
! [X2] :
( ( epsilon_transitive(X2)
| ~ ordinal(X2) )
& ( epsilon_connected(X2)
| ~ ordinal(X2) ) ),
inference(distribute,[status(thm)],[43]) ).
cnf(46,plain,
( epsilon_transitive(X1)
| ~ ordinal(X1) ),
inference(split_conjunct,[status(thm)],[44]) ).
fof(53,negated_conjecture,
? [X1] :
( ordinal(X1)
& ? [X2] :
( ordinal(X2)
& ? [X3] :
( epsilon_transitive(X3)
& in(X3,X1)
& in(X1,X2)
& ~ in(X3,X2) ) ) ),
inference(fof_nnf,[status(thm)],[33]) ).
fof(54,negated_conjecture,
? [X4] :
( ordinal(X4)
& ? [X5] :
( ordinal(X5)
& ? [X6] :
( epsilon_transitive(X6)
& in(X6,X4)
& in(X4,X5)
& ~ in(X6,X5) ) ) ),
inference(variable_rename,[status(thm)],[53]) ).
fof(55,negated_conjecture,
( ordinal(esk3_0)
& ordinal(esk4_0)
& epsilon_transitive(esk5_0)
& in(esk5_0,esk3_0)
& in(esk3_0,esk4_0)
& ~ in(esk5_0,esk4_0) ),
inference(skolemize,[status(esa)],[54]) ).
cnf(56,negated_conjecture,
~ in(esk5_0,esk4_0),
inference(split_conjunct,[status(thm)],[55]) ).
cnf(57,negated_conjecture,
in(esk3_0,esk4_0),
inference(split_conjunct,[status(thm)],[55]) ).
cnf(58,negated_conjecture,
in(esk5_0,esk3_0),
inference(split_conjunct,[status(thm)],[55]) ).
cnf(60,negated_conjecture,
ordinal(esk4_0),
inference(split_conjunct,[status(thm)],[55]) ).
fof(76,plain,
! [X1,X2,X3] :
( ~ in(X1,X2)
| ~ element(X2,powerset(X3))
| element(X1,X3) ),
inference(fof_nnf,[status(thm)],[10]) ).
fof(77,plain,
! [X4,X5,X6] :
( ~ in(X4,X5)
| ~ element(X5,powerset(X6))
| element(X4,X6) ),
inference(variable_rename,[status(thm)],[76]) ).
cnf(78,plain,
( element(X1,X2)
| ~ element(X3,powerset(X2))
| ~ in(X1,X3) ),
inference(split_conjunct,[status(thm)],[77]) ).
fof(84,plain,
! [X1,X2] :
( ~ in(X1,X2)
| ~ empty(X2) ),
inference(fof_nnf,[status(thm)],[12]) ).
fof(85,plain,
! [X3,X4] :
( ~ in(X3,X4)
| ~ empty(X4) ),
inference(variable_rename,[status(thm)],[84]) ).
cnf(86,plain,
( ~ empty(X1)
| ~ in(X2,X1) ),
inference(split_conjunct,[status(thm)],[85]) ).
fof(90,plain,
! [X1] :
( ( ~ epsilon_transitive(X1)
| ! [X2] :
( ~ in(X2,X1)
| subset(X2,X1) ) )
& ( ? [X2] :
( in(X2,X1)
& ~ subset(X2,X1) )
| epsilon_transitive(X1) ) ),
inference(fof_nnf,[status(thm)],[14]) ).
fof(91,plain,
! [X3] :
( ( ~ epsilon_transitive(X3)
| ! [X4] :
( ~ in(X4,X3)
| subset(X4,X3) ) )
& ( ? [X5] :
( in(X5,X3)
& ~ subset(X5,X3) )
| epsilon_transitive(X3) ) ),
inference(variable_rename,[status(thm)],[90]) ).
fof(92,plain,
! [X3] :
( ( ~ epsilon_transitive(X3)
| ! [X4] :
( ~ in(X4,X3)
| subset(X4,X3) ) )
& ( ( in(esk9_1(X3),X3)
& ~ subset(esk9_1(X3),X3) )
| epsilon_transitive(X3) ) ),
inference(skolemize,[status(esa)],[91]) ).
fof(93,plain,
! [X3,X4] :
( ( ~ in(X4,X3)
| subset(X4,X3)
| ~ epsilon_transitive(X3) )
& ( ( in(esk9_1(X3),X3)
& ~ subset(esk9_1(X3),X3) )
| epsilon_transitive(X3) ) ),
inference(shift_quantors,[status(thm)],[92]) ).
fof(94,plain,
! [X3,X4] :
( ( ~ in(X4,X3)
| subset(X4,X3)
| ~ epsilon_transitive(X3) )
& ( in(esk9_1(X3),X3)
| epsilon_transitive(X3) )
& ( ~ subset(esk9_1(X3),X3)
| epsilon_transitive(X3) ) ),
inference(distribute,[status(thm)],[93]) ).
cnf(97,plain,
( subset(X2,X1)
| ~ epsilon_transitive(X1)
| ~ in(X2,X1) ),
inference(split_conjunct,[status(thm)],[94]) ).
fof(118,plain,
! [X1,X2] :
( ~ element(X1,X2)
| empty(X2)
| in(X1,X2) ),
inference(fof_nnf,[status(thm)],[20]) ).
fof(119,plain,
! [X3,X4] :
( ~ element(X3,X4)
| empty(X4)
| in(X3,X4) ),
inference(variable_rename,[status(thm)],[118]) ).
cnf(120,plain,
( in(X1,X2)
| empty(X2)
| ~ element(X1,X2) ),
inference(split_conjunct,[status(thm)],[119]) ).
fof(121,plain,
! [X1,X2] :
( ( ~ element(X1,powerset(X2))
| subset(X1,X2) )
& ( ~ subset(X1,X2)
| element(X1,powerset(X2)) ) ),
inference(fof_nnf,[status(thm)],[21]) ).
fof(122,plain,
! [X3,X4] :
( ( ~ element(X3,powerset(X4))
| subset(X3,X4) )
& ( ~ subset(X3,X4)
| element(X3,powerset(X4)) ) ),
inference(variable_rename,[status(thm)],[121]) ).
cnf(123,plain,
( element(X1,powerset(X2))
| ~ subset(X1,X2) ),
inference(split_conjunct,[status(thm)],[122]) ).
cnf(161,negated_conjecture,
epsilon_transitive(esk4_0),
inference(spm,[status(thm)],[46,60,theory(equality)]) ).
cnf(178,negated_conjecture,
~ empty(esk4_0),
inference(spm,[status(thm)],[86,57,theory(equality)]) ).
cnf(199,plain,
( element(X1,X2)
| ~ in(X1,X3)
| ~ subset(X3,X2) ),
inference(spm,[status(thm)],[78,123,theory(equality)]) ).
cnf(286,plain,
( element(X1,X2)
| ~ in(X1,X3)
| ~ in(X3,X2)
| ~ epsilon_transitive(X2) ),
inference(spm,[status(thm)],[199,97,theory(equality)]) ).
cnf(312,negated_conjecture,
( element(esk5_0,X1)
| ~ in(esk3_0,X1)
| ~ epsilon_transitive(X1) ),
inference(spm,[status(thm)],[286,58,theory(equality)]) ).
cnf(336,negated_conjecture,
( element(esk5_0,esk4_0)
| ~ in(esk3_0,esk4_0) ),
inference(spm,[status(thm)],[312,161,theory(equality)]) ).
cnf(342,negated_conjecture,
( element(esk5_0,esk4_0)
| $false ),
inference(rw,[status(thm)],[336,57,theory(equality)]) ).
cnf(343,negated_conjecture,
element(esk5_0,esk4_0),
inference(cn,[status(thm)],[342,theory(equality)]) ).
cnf(344,negated_conjecture,
( empty(esk4_0)
| in(esk5_0,esk4_0) ),
inference(spm,[status(thm)],[120,343,theory(equality)]) ).
cnf(345,negated_conjecture,
in(esk5_0,esk4_0),
inference(sr,[status(thm)],[344,178,theory(equality)]) ).
cnf(346,negated_conjecture,
$false,
inference(sr,[status(thm)],[345,56,theory(equality)]) ).
cnf(347,negated_conjecture,
$false,
346,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.01/0.03 % Problem : NUM388+1 : TPTP v7.0.0. Released v3.2.0.
% 0.01/0.03 % Command : Source/sine.py -e eprover -t %d %s
% 0.02/0.23 % Computer : n091.star.cs.uiowa.edu
% 0.02/0.23 % Model : x86_64 x86_64
% 0.02/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.02/0.23 % Memory : 32218.625MB
% 0.02/0.23 % OS : Linux 3.10.0-693.2.2.el7.x86_64
% 0.02/0.23 % CPULimit : 300
% 0.02/0.23 % DateTime : Fri Jan 5 02:36:45 CST 2018
% 0.02/0.23 % CPUTime :
% 0.07/0.28 % SZS status Started for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.28 --creating new selector for []
% 0.07/0.36 -running prover on /export/starexec/sandbox/tmp/tmppf8G1Q/sel_theBenchmark.p_1 with time limit 29
% 0.07/0.36 -running prover with command ['/export/starexec/sandbox/solver/bin/Source/./Source/PROVER/eproof.working', '-s', '-tLPO4', '-xAuto', '-tAuto', '--memory-limit=768', '--tptp3-format', '--cpu-limit=29', '/export/starexec/sandbox/tmp/tmppf8G1Q/sel_theBenchmark.p_1']
% 0.07/0.36 -prover status Theorem
% 0.07/0.36 Problem theBenchmark.p solved in phase 0.
% 0.07/0.36 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.36 % SZS status Ended for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.36 Solved 1 out of 1.
% 0.07/0.36 # Problem is unsatisfiable (or provable), constructing proof object
% 0.07/0.36 # SZS status Theorem
% 0.07/0.36 # SZS output start CNFRefutation.
% See solution above
% 0.07/0.36 # SZS output end CNFRefutation
%------------------------------------------------------------------------------