%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : NUM925+5 : TPTP v7.0.0. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : n058.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:42 EST 2018
% Result : Theorem 0.06s
% Output : CNFRefutation 0.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 13
% Syntax : Number of formulae : 62 ( 44 unt; 0 def)
% Number of atoms : 102 ( 34 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 76 ( 36 ~; 33 |; 4 &)
% ( 1 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 4 con; 0-3 aty)
% Number of variables : 39 ( 0 sgn 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(6,axiom,
equal(pls,zero_zero(int)),
file('/export/starexec/sandbox2/tmp/tmpYdWFRS/sel_theBenchmark.p_1',fact_73_Pls__def) ).
fof(17,axiom,
ord_less(int,zero_zero(int),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),
file('/export/starexec/sandbox2/tmp/tmpYdWFRS/sel_theBenchmark.p_1',fact_0_n1pos) ).
fof(33,axiom,
! [X1] :
( number_ring(X1)
=> ! [X22] : equal(plus_plus(X1,X22,number_number_of(X1,pls)),ti(X1,X22)) ),
file('/export/starexec/sandbox2/tmp/tmpYdWFRS/sel_theBenchmark.p_1',fact_85_add__numeral__0__right) ).
fof(42,axiom,
! [X1] :
( ring_11004092258visors(X1)
=> ! [X23] :
( equal(power_power(X1,X23,number_number_of(nat,bit0(bit1(pls)))),zero_zero(X1))
<=> equal(ti(X1,X23),zero_zero(X1)) ) ),
file('/export/starexec/sandbox2/tmp/tmpYdWFRS/sel_theBenchmark.p_1',fact_5_zero__eq__power2) ).
fof(58,axiom,
equal(zero_zero(int),number_number_of(int,pls)),
file('/export/starexec/sandbox2/tmp/tmpYdWFRS/sel_theBenchmark.p_1',fact_19_zero__is__num__zero) ).
fof(91,axiom,
ring_11004092258visors(int),
file('/export/starexec/sandbox2/tmp/tmpYdWFRS/sel_theBenchmark.p_1',arity_Int_Oint___Rings_Oring__1__no__zero__divisors) ).
fof(114,conjecture,
~ equal(power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(bit1(pls)))),zero_zero(int)),
file('/export/starexec/sandbox2/tmp/tmpYdWFRS/sel_theBenchmark.p_1',conj_0) ).
fof(121,axiom,
! [X4] : equal(plus_plus(int,X4,pls),X4),
file('/export/starexec/sandbox2/tmp/tmpYdWFRS/sel_theBenchmark.p_1',fact_75_add__Pls__right) ).
fof(122,axiom,
! [X4] : equal(bit0(X4),plus_plus(int,X4,X4)),
file('/export/starexec/sandbox2/tmp/tmpYdWFRS/sel_theBenchmark.p_1',fact_78_Bit0__def) ).
fof(124,axiom,
! [X4] : equal(bit1(X4),plus_plus(int,plus_plus(int,one_one(int),X4),X4)),
file('/export/starexec/sandbox2/tmp/tmpYdWFRS/sel_theBenchmark.p_1',fact_92_Bit1__def) ).
fof(146,axiom,
~ ord_less(int,pls,pls),
file('/export/starexec/sandbox2/tmp/tmpYdWFRS/sel_theBenchmark.p_1',fact_32_rel__simps_I2_J) ).
fof(147,axiom,
equal(plus_plus(nat,one_one(nat),one_one(nat)),number_number_of(nat,bit0(bit1(pls)))),
file('/export/starexec/sandbox2/tmp/tmpYdWFRS/sel_theBenchmark.p_1',fact_29_nat__1__add__1) ).
fof(153,axiom,
number_ring(int),
file('/export/starexec/sandbox2/tmp/tmpYdWFRS/sel_theBenchmark.p_1',arity_Int_Oint___Int_Onumber__ring) ).
fof(154,negated_conjecture,
~ ~ equal(power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(bit1(pls)))),zero_zero(int)),
inference(assume_negation,[status(cth)],[114]) ).
fof(159,negated_conjecture,
equal(power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(bit1(pls)))),zero_zero(int)),
inference(fof_simplification,[status(thm)],[154,theory(equality)]) ).
fof(160,plain,
~ ord_less(int,pls,pls),
inference(fof_simplification,[status(thm)],[146,theory(equality)]) ).
cnf(175,plain,
pls = zero_zero(int),
inference(split_conjunct,[status(thm)],[6]) ).
cnf(201,plain,
ord_less(int,zero_zero(int),plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),
inference(split_conjunct,[status(thm)],[17]) ).
fof(247,plain,
! [X1] :
( ~ number_ring(X1)
| ! [X22] : equal(plus_plus(X1,X22,number_number_of(X1,pls)),ti(X1,X22)) ),
inference(fof_nnf,[status(thm)],[33]) ).
fof(248,plain,
! [X23] :
( ~ number_ring(X23)
| ! [X24] : equal(plus_plus(X23,X24,number_number_of(X23,pls)),ti(X23,X24)) ),
inference(variable_rename,[status(thm)],[247]) ).
fof(249,plain,
! [X23,X24] :
( equal(plus_plus(X23,X24,number_number_of(X23,pls)),ti(X23,X24))
| ~ number_ring(X23) ),
inference(shift_quantors,[status(thm)],[248]) ).
cnf(250,plain,
( plus_plus(X1,X2,number_number_of(X1,pls)) = ti(X1,X2)
| ~ number_ring(X1) ),
inference(split_conjunct,[status(thm)],[249]) ).
fof(273,plain,
! [X1] :
( ~ ring_11004092258visors(X1)
| ! [X23] :
( ( ~ equal(power_power(X1,X23,number_number_of(nat,bit0(bit1(pls)))),zero_zero(X1))
| equal(ti(X1,X23),zero_zero(X1)) )
& ( ~ equal(ti(X1,X23),zero_zero(X1))
| equal(power_power(X1,X23,number_number_of(nat,bit0(bit1(pls)))),zero_zero(X1)) ) ) ),
inference(fof_nnf,[status(thm)],[42]) ).
fof(274,plain,
! [X24] :
( ~ ring_11004092258visors(X24)
| ! [X25] :
( ( ~ equal(power_power(X24,X25,number_number_of(nat,bit0(bit1(pls)))),zero_zero(X24))
| equal(ti(X24,X25),zero_zero(X24)) )
& ( ~ equal(ti(X24,X25),zero_zero(X24))
| equal(power_power(X24,X25,number_number_of(nat,bit0(bit1(pls)))),zero_zero(X24)) ) ) ),
inference(variable_rename,[status(thm)],[273]) ).
fof(275,plain,
! [X24,X25] :
( ( ( ~ equal(power_power(X24,X25,number_number_of(nat,bit0(bit1(pls)))),zero_zero(X24))
| equal(ti(X24,X25),zero_zero(X24)) )
& ( ~ equal(ti(X24,X25),zero_zero(X24))
| equal(power_power(X24,X25,number_number_of(nat,bit0(bit1(pls)))),zero_zero(X24)) ) )
| ~ ring_11004092258visors(X24) ),
inference(shift_quantors,[status(thm)],[274]) ).
fof(276,plain,
! [X24,X25] :
( ( ~ equal(power_power(X24,X25,number_number_of(nat,bit0(bit1(pls)))),zero_zero(X24))
| equal(ti(X24,X25),zero_zero(X24))
| ~ ring_11004092258visors(X24) )
& ( ~ equal(ti(X24,X25),zero_zero(X24))
| equal(power_power(X24,X25,number_number_of(nat,bit0(bit1(pls)))),zero_zero(X24))
| ~ ring_11004092258visors(X24) ) ),
inference(distribute,[status(thm)],[275]) ).
cnf(278,plain,
( ti(X1,X2) = zero_zero(X1)
| ~ ring_11004092258visors(X1)
| power_power(X1,X2,number_number_of(nat,bit0(bit1(pls)))) != zero_zero(X1) ),
inference(split_conjunct,[status(thm)],[276]) ).
cnf(314,plain,
zero_zero(int) = number_number_of(int,pls),
inference(split_conjunct,[status(thm)],[58]) ).
cnf(411,plain,
ring_11004092258visors(int),
inference(split_conjunct,[status(thm)],[91]) ).
cnf(472,negated_conjecture,
power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,bit0(bit1(pls)))) = zero_zero(int),
inference(split_conjunct,[status(thm)],[159]) ).
fof(498,plain,
! [X5] : equal(plus_plus(int,X5,pls),X5),
inference(variable_rename,[status(thm)],[121]) ).
cnf(499,plain,
plus_plus(int,X1,pls) = X1,
inference(split_conjunct,[status(thm)],[498]) ).
fof(500,plain,
! [X5] : equal(bit0(X5),plus_plus(int,X5,X5)),
inference(variable_rename,[status(thm)],[122]) ).
cnf(501,plain,
bit0(X1) = plus_plus(int,X1,X1),
inference(split_conjunct,[status(thm)],[500]) ).
fof(504,plain,
! [X5] : equal(bit1(X5),plus_plus(int,plus_plus(int,one_one(int),X5),X5)),
inference(variable_rename,[status(thm)],[124]) ).
cnf(505,plain,
bit1(X1) = plus_plus(int,plus_plus(int,one_one(int),X1),X1),
inference(split_conjunct,[status(thm)],[504]) ).
cnf(575,plain,
~ ord_less(int,pls,pls),
inference(split_conjunct,[status(thm)],[160]) ).
cnf(576,plain,
plus_plus(nat,one_one(nat),one_one(nat)) = number_number_of(nat,bit0(bit1(pls))),
inference(split_conjunct,[status(thm)],[147]) ).
cnf(590,plain,
number_ring(int),
inference(split_conjunct,[status(thm)],[153]) ).
cnf(597,plain,
plus_plus(nat,one_one(nat),one_one(nat)) = number_number_of(nat,plus_plus(int,bit1(pls),bit1(pls))),
inference(rw,[status(thm)],[576,501,theory(equality)]),
[unfolding] ).
cnf(598,negated_conjecture,
power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,plus_plus(int,bit1(pls),bit1(pls)))) = zero_zero(int),
inference(rw,[status(thm)],[472,501,theory(equality)]),
[unfolding] ).
cnf(626,plain,
( ti(X1,X2) = zero_zero(X1)
| power_power(X1,X2,number_number_of(nat,plus_plus(int,bit1(pls),bit1(pls)))) != zero_zero(X1)
| ~ ring_11004092258visors(X1) ),
inference(rw,[status(thm)],[278,501,theory(equality)]),
[unfolding] ).
cnf(643,plain,
plus_plus(nat,one_one(nat),one_one(nat)) = number_number_of(nat,plus_plus(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[597,505,theory(equality)]),505,theory(equality)]),
[unfolding] ).
cnf(644,negated_conjecture,
power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),number_number_of(nat,plus_plus(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls)))) = zero_zero(int),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[598,505,theory(equality)]),505,theory(equality)]),
[unfolding] ).
cnf(670,plain,
( ti(X1,X2) = zero_zero(X1)
| power_power(X1,X2,number_number_of(nat,plus_plus(int,plus_plus(int,plus_plus(int,one_one(int),pls),pls),plus_plus(int,plus_plus(int,one_one(int),pls),pls)))) != zero_zero(X1)
| ~ ring_11004092258visors(X1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[626,505,theory(equality)]),505,theory(equality)]),
[unfolding] ).
cnf(687,plain,
number_number_of(int,pls) = pls,
inference(rw,[status(thm)],[314,175,theory(equality)]) ).
cnf(716,plain,
number_number_of(nat,plus_plus(int,one_one(int),one_one(int))) = plus_plus(nat,one_one(nat),one_one(nat)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[643,499,theory(equality)]),499,theory(equality)]),499,theory(equality)]),499,theory(equality)]) ).
cnf(717,plain,
ord_less(int,pls,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))),
inference(rw,[status(thm)],[201,175,theory(equality)]) ).
cnf(728,negated_conjecture,
power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),plus_plus(nat,one_one(nat),one_one(nat))) = zero_zero(int),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[644,499,theory(equality)]),499,theory(equality)]),499,theory(equality)]),499,theory(equality)]),716,theory(equality)]) ).
cnf(729,negated_conjecture,
power_power(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n)),plus_plus(nat,one_one(nat),one_one(nat))) = pls,
inference(rw,[status(thm)],[728,175,theory(equality)]) ).
cnf(1478,plain,
plus_plus(int,X1,number_number_of(int,pls)) = ti(int,X1),
inference(spm,[status(thm)],[250,590,theory(equality)]) ).
cnf(1479,plain,
X1 = ti(int,X1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[1478,687,theory(equality)]),499,theory(equality)]) ).
cnf(1900,plain,
( ti(X1,X2) = zero_zero(X1)
| power_power(X1,X2,plus_plus(nat,one_one(nat),one_one(nat))) != zero_zero(X1)
| ~ ring_11004092258visors(X1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[670,499,theory(equality)]),499,theory(equality)]),499,theory(equality)]),499,theory(equality)]),716,theory(equality)]) ).
cnf(1901,negated_conjecture,
( ti(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))) = zero_zero(int)
| pls != zero_zero(int)
| ~ ring_11004092258visors(int) ),
inference(spm,[status(thm)],[1900,729,theory(equality)]) ).
cnf(1904,negated_conjecture,
( ti(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))) = pls
| pls != zero_zero(int)
| ~ ring_11004092258visors(int) ),
inference(rw,[status(thm)],[1901,175,theory(equality)]) ).
cnf(1905,negated_conjecture,
( ti(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))) = pls
| $false
| ~ ring_11004092258visors(int) ),
inference(rw,[status(thm)],[1904,175,theory(equality)]) ).
cnf(1906,negated_conjecture,
( ti(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))) = pls
| $false
| $false ),
inference(rw,[status(thm)],[1905,411,theory(equality)]) ).
cnf(1907,negated_conjecture,
ti(int,plus_plus(int,one_one(int),semiring_1_of_nat(int,n))) = pls,
inference(cn,[status(thm)],[1906,theory(equality)]) ).
cnf(4808,negated_conjecture,
plus_plus(int,one_one(int),semiring_1_of_nat(int,n)) = pls,
inference(rw,[status(thm)],[1907,1479,theory(equality)]) ).
cnf(4853,plain,
ord_less(int,pls,pls),
inference(rw,[status(thm)],[717,4808,theory(equality)]) ).
cnf(4854,plain,
$false,
inference(sr,[status(thm)],[4853,575,theory(equality)]) ).
cnf(4855,plain,
$false,
4854,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM925+5 : TPTP v7.0.0. Released v5.3.0.
% 0.00/0.04 % Command : Source/sine.py -e eprover -t %d %s
% 0.03/0.24 % Computer : n058.star.cs.uiowa.edu
% 0.03/0.24 % Model : x86_64 x86_64
% 0.03/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.03/0.24 % Memory : 32218.625MB
% 0.03/0.24 % OS : Linux 3.10.0-693.2.2.el7.x86_64
% 0.03/0.24 % CPULimit : 300
% 0.03/0.24 % DateTime : Fri Jan 5 16:17:34 CST 2018
% 0.06/0.24 % CPUTime :
% 0.06/0.29 % SZS status Started for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.06/0.29 --creating new selector for []
% 0.06/0.47 -running prover on /export/starexec/sandbox2/tmp/tmpYdWFRS/sel_theBenchmark.p_1 with time limit 29
% 0.06/0.47 -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/tmpYdWFRS/sel_theBenchmark.p_1']
% 0.06/0.47 -prover status Theorem
% 0.06/0.47 Problem theBenchmark.p solved in phase 0.
% 0.06/0.47 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.06/0.47 % SZS status Ended for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.06/0.47 Solved 1 out of 1.
% 0.06/0.47 # Problem is unsatisfiable (or provable), constructing proof object
% 0.06/0.47 # SZS status Theorem
% 0.06/0.47 # SZS output start CNFRefutation.
% See solution above
% 0.06/0.47 # SZS output end CNFRefutation
%------------------------------------------------------------------------------