%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : NUM925+2 : TPTP v7.0.0. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : n104.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:22:41 EST 2018
% Result : Theorem 0.07s
% Output : CNFRefutation 0.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 9
% Syntax : Number of formulae : 42 ( 34 unt; 0 def)
% Number of atoms : 50 ( 12 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 21 ( 13 ~; 7 |; 0 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 6 con; 0-2 aty)
% Number of variables : 25 ( 3 sgn 14 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(13,axiom,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n)))),
file('/export/starexec/sandbox2/tmp/tmpbZFVUw/sel_theBenchmark.p_1',fact_0_n1pos) ).
fof(153,axiom,
! [X1] : equal(succ(X1),hAPP_int_int(plus_plus_int(X1),one_one_int)),
file('/export/starexec/sandbox2/tmp/tmpbZFVUw/sel_theBenchmark.p_1',fact_573_succ__def) ).
fof(172,axiom,
! [X98] : equal(hAPP_int_int(plus_plus_int(zero_zero_int),X98),X98),
file('/export/starexec/sandbox2/tmp/tmpbZFVUw/sel_theBenchmark.p_1',fact_365_add__0) ).
fof(265,axiom,
! [X1] : equal(bit0(X1),hAPP_int_int(plus_plus_int(X1),X1)),
file('/export/starexec/sandbox2/tmp/tmpbZFVUw/sel_theBenchmark.p_1',fact_103_Bit0__def) ).
fof(297,axiom,
! [X1] : equal(succ(bit0(X1)),bit1(X1)),
file('/export/starexec/sandbox2/tmp/tmpbZFVUw/sel_theBenchmark.p_1',fact_568_succ__Bit0) ).
fof(324,axiom,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),zero_zero_int)),
file('/export/starexec/sandbox2/tmp/tmpbZFVUw/sel_theBenchmark.p_1',fact_79_bin__less__0__simps_I1_J) ).
fof(418,axiom,
! [X240,X241] :
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),X241))
=> hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),hAPP_nat_int(power_power_int(X241),X240))) ),
file('/export/starexec/sandbox2/tmp/tmpbZFVUw/sel_theBenchmark.p_1',fact_267_zero__less__power) ).
fof(477,axiom,
equal(pls,zero_zero_int),
file('/export/starexec/sandbox2/tmp/tmpbZFVUw/sel_theBenchmark.p_1',fact_98_Pls__def) ).
fof(669,conjecture,
~ equal(hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))),zero_zero_int),
file('/export/starexec/sandbox2/tmp/tmpbZFVUw/sel_theBenchmark.p_1',conj_0) ).
fof(709,negated_conjecture,
~ ~ equal(hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))),zero_zero_int),
inference(assume_negation,[status(cth)],[669]) ).
fof(731,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),zero_zero_int)),
inference(fof_simplification,[status(thm)],[324,theory(equality)]) ).
fof(747,negated_conjecture,
equal(hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))),zero_zero_int),
inference(fof_simplification,[status(thm)],[709,theory(equality)]) ).
cnf(788,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n)))),
inference(split_conjunct,[status(thm)],[13]) ).
fof(1229,plain,
! [X2] : equal(succ(X2),hAPP_int_int(plus_plus_int(X2),one_one_int)),
inference(variable_rename,[status(thm)],[153]) ).
cnf(1230,plain,
succ(X1) = hAPP_int_int(plus_plus_int(X1),one_one_int),
inference(split_conjunct,[status(thm)],[1229]) ).
fof(1290,plain,
! [X99] : equal(hAPP_int_int(plus_plus_int(zero_zero_int),X99),X99),
inference(variable_rename,[status(thm)],[172]) ).
cnf(1291,plain,
hAPP_int_int(plus_plus_int(zero_zero_int),X1) = X1,
inference(split_conjunct,[status(thm)],[1290]) ).
fof(1568,plain,
! [X2] : equal(bit0(X2),hAPP_int_int(plus_plus_int(X2),X2)),
inference(variable_rename,[status(thm)],[265]) ).
cnf(1569,plain,
bit0(X1) = hAPP_int_int(plus_plus_int(X1),X1),
inference(split_conjunct,[status(thm)],[1568]) ).
fof(1658,plain,
! [X2] : equal(succ(bit0(X2)),bit1(X2)),
inference(variable_rename,[status(thm)],[297]) ).
cnf(1659,plain,
succ(bit0(X1)) = bit1(X1),
inference(split_conjunct,[status(thm)],[1658]) ).
cnf(1725,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),zero_zero_int)),
inference(split_conjunct,[status(thm)],[731]) ).
fof(2004,plain,
! [X240,X241] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),X241))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),hAPP_nat_int(power_power_int(X241),X240))) ),
inference(fof_nnf,[status(thm)],[418]) ).
fof(2005,plain,
! [X242,X243] :
( ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),X243))
| hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),hAPP_nat_int(power_power_int(X243),X242))) ),
inference(variable_rename,[status(thm)],[2004]) ).
cnf(2006,plain,
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),hAPP_nat_int(power_power_int(X1),X2)))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),X1)) ),
inference(split_conjunct,[status(thm)],[2005]) ).
cnf(2193,plain,
pls = zero_zero_int,
inference(split_conjunct,[status(thm)],[477]) ).
cnf(2792,negated_conjecture,
hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(bit1(pls)))) = zero_zero_int,
inference(split_conjunct,[status(thm)],[747]) ).
cnf(3012,negated_conjecture,
hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(bit0(succ(bit0(pls))))) = zero_zero_int,
inference(rw,[status(thm)],[2792,1659,theory(equality)]),
[unfolding] ).
cnf(3167,negated_conjecture,
hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(hAPP_int_int(plus_plus_int(succ(hAPP_int_int(plus_plus_int(pls),pls))),succ(hAPP_int_int(plus_plus_int(pls),pls))))) = zero_zero_int,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[3012,1569,theory(equality)]),1569,theory(equality)]),
[unfolding] ).
cnf(3344,negated_conjecture,
hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(pls),pls)),one_one_int)),hAPP_int_int(plus_plus_int(hAPP_int_int(plus_plus_int(pls),pls)),one_one_int)))) = zero_zero_int,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[3167,1230,theory(equality)]),1230,theory(equality)]),
[unfolding] ).
cnf(3477,plain,
hAPP_int_int(plus_plus_int(pls),X1) = X1,
inference(rw,[status(thm)],[1291,2193,theory(equality)]) ).
cnf(4020,plain,
~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),pls)),
inference(rw,[status(thm)],[1725,2193,theory(equality)]) ).
cnf(4308,plain,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n)))),
inference(rw,[status(thm)],[788,2193,theory(equality)]) ).
cnf(4388,negated_conjecture,
hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(hAPP_int_int(plus_plus_int(one_one_int),one_one_int))) = zero_zero_int,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[3344,3477,theory(equality)]),3477,theory(equality)]),3477,theory(equality)]),3477,theory(equality)]) ).
cnf(4389,negated_conjecture,
hAPP_nat_int(power_power_int(hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n))),number_number_of_nat(hAPP_int_int(plus_plus_int(one_one_int),one_one_int))) = pls,
inference(rw,[status(thm)],[4388,2193,theory(equality)]) ).
cnf(6390,plain,
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_nat_int(power_power_int(X1),X2)))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,zero_zero_int),X1)) ),
inference(rw,[status(thm)],[2006,2193,theory(equality)]) ).
cnf(6391,plain,
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_nat_int(power_power_int(X1),X2)))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),X1)) ),
inference(rw,[status(thm)],[6390,2193,theory(equality)]) ).
cnf(6397,negated_conjecture,
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),pls))
| ~ hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),hAPP_int_int(plus_plus_int(one_one_int),hAPP_nat_int(semiri1621563631at_int,n)))) ),
inference(spm,[status(thm)],[6391,4389,theory(equality)]) ).
cnf(6409,negated_conjecture,
( hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),pls))
| $false ),
inference(rw,[status(thm)],[6397,4308,theory(equality)]) ).
cnf(6410,negated_conjecture,
hBOOL(hAPP_int_bool(hAPP_i1948725293t_bool(ord_less_int,pls),pls)),
inference(cn,[status(thm)],[6409,theory(equality)]) ).
cnf(6411,negated_conjecture,
$false,
inference(sr,[status(thm)],[6410,4020,theory(equality)]) ).
cnf(6412,negated_conjecture,
$false,
6411,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM925+2 : TPTP v7.0.0. Released v5.3.0.
% 0.00/0.04 % Command : Source/sine.py -e eprover -t %d %s
% 0.02/0.23 % Computer : n104.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 16:35:34 CST 2018
% 0.02/0.23 % CPUTime :
% 0.02/0.27 % SZS status Started for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.02/0.28 --creating new selector for []
% 0.07/0.56 -running prover on /export/starexec/sandbox2/tmp/tmpbZFVUw/sel_theBenchmark.p_1 with time limit 29
% 0.07/0.56 -running prover with command ['/export/starexec/sandbox2/solver/bin/Source/./Source/PROVER/eproof.working', '-s', '-tLPO4', '-xAuto', '-tAuto', '--memory-limit=768', '--tptp3-format', '--cpu-limit=29', '/export/starexec/sandbox2/tmp/tmpbZFVUw/sel_theBenchmark.p_1']
% 0.07/0.56 -prover status Theorem
% 0.07/0.56 Problem theBenchmark.p solved in phase 0.
% 0.07/0.56 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.56 % SZS status Ended for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.56 Solved 1 out of 1.
% 0.07/0.56 # Problem is unsatisfiable (or provable), constructing proof object
% 0.07/0.56 # SZS status Theorem
% 0.07/0.56 # SZS output start CNFRefutation.
% See solution above
% 0.07/0.56 # SZS output end CNFRefutation
%------------------------------------------------------------------------------