%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : NUM925+7 : 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 2.19s
% Output : CNFRefutation 2.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 11
% Syntax : Number of formulae : 49 ( 40 unt; 0 def)
% Number of atoms : 67 ( 17 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 37 ( 19 ~; 16 |; 0 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 6 con; 0-4 aty)
% Number of variables : 24 ( 1 sgn 18 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(10,axiom,
equal(pls,zero_zero(int)),
file('/export/starexec/sandbox2/tmp/tmp3Ko1Bt/sel_theBenchmark.p_1',fact_73_Pls__def) ).
fof(38,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n)))),
file('/export/starexec/sandbox2/tmp/tmp3Ko1Bt/sel_theBenchmark.p_1',fact_0_n1pos) ).
fof(376,axiom,
equal(bit0(pls),pls),
file('/export/starexec/sandbox2/tmp/tmp3Ko1Bt/sel_theBenchmark.p_1',fact_72_Bit0__Pls) ).
fof(559,axiom,
! [X28] : equal(bit0(X28),plus_plus(int,X28,X28)),
file('/export/starexec/sandbox2/tmp/tmp3Ko1Bt/sel_theBenchmark.p_1',fact_78_Bit0__def) ).
fof(607,axiom,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls)),
file('/export/starexec/sandbox2/tmp/tmp3Ko1Bt/sel_theBenchmark.p_1',fact_32_rel__simps_I2_J) ).
fof(750,conjecture,
~ equal(hAPP(nat,int,power_power(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,bit0(bit1(pls)))),zero_zero(int)),
file('/export/starexec/sandbox2/tmp/tmp3Ko1Bt/sel_theBenchmark.p_1',conj_0) ).
fof(874,axiom,
linordered_semidom(int),
file('/export/starexec/sandbox2/tmp/tmp3Ko1Bt/sel_theBenchmark.p_1',arity_Int_Oint___Rings_Olinordered__semidom) ).
fof(913,axiom,
! [X28] : equal(minus_minus(int,X28,min),succ(X28)),
file('/export/starexec/sandbox2/tmp/tmp3Ko1Bt/sel_theBenchmark.p_1',fact_777_diff__bin__simps_I2_J) ).
fof(925,axiom,
! [X2] :
( linordered_semidom(X2)
=> ! [X8,X4] :
( hBOOL(hAPP(X2,bool,hAPP(X2,fun(X2,bool),ord_less(X2),zero_zero(X2)),X4))
=> hBOOL(hAPP(X2,bool,hAPP(X2,fun(X2,bool),ord_less(X2),zero_zero(X2)),hAPP(nat,X2,power_power(X2,X4),X8))) ) ),
file('/export/starexec/sandbox2/tmp/tmp3Ko1Bt/sel_theBenchmark.p_1',fact_179_zero__less__power) ).
fof(1187,axiom,
! [X28] : equal(succ(bit0(X28)),bit1(X28)),
file('/export/starexec/sandbox2/tmp/tmp3Ko1Bt/sel_theBenchmark.p_1',fact_514_succ__Bit0) ).
fof(1234,axiom,
equal(plus_plus(nat,one_one(nat),one_one(nat)),number_number_of(nat,bit0(bit1(pls)))),
file('/export/starexec/sandbox2/tmp/tmp3Ko1Bt/sel_theBenchmark.p_1',fact_29_nat__1__add__1) ).
fof(1252,negated_conjecture,
~ ~ equal(hAPP(nat,int,power_power(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,bit0(bit1(pls)))),zero_zero(int)),
inference(assume_negation,[status(cth)],[750]) ).
fof(1297,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls)),
inference(fof_simplification,[status(thm)],[607,theory(equality)]) ).
fof(1305,negated_conjecture,
equal(hAPP(nat,int,power_power(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,bit0(bit1(pls)))),zero_zero(int)),
inference(fof_simplification,[status(thm)],[1252,theory(equality)]) ).
cnf(1366,plain,
pls = zero_zero(int),
inference(split_conjunct,[status(thm)],[10]) ).
cnf(1453,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n)))),
inference(split_conjunct,[status(thm)],[38]) ).
cnf(2541,plain,
bit0(pls) = pls,
inference(split_conjunct,[status(thm)],[376]) ).
fof(3171,plain,
! [X29] : equal(bit0(X29),plus_plus(int,X29,X29)),
inference(variable_rename,[status(thm)],[559]) ).
cnf(3172,plain,
bit0(X1) = plus_plus(int,X1,X1),
inference(split_conjunct,[status(thm)],[3171]) ).
cnf(3348,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls)),
inference(split_conjunct,[status(thm)],[1297]) ).
cnf(3829,negated_conjecture,
hAPP(nat,int,power_power(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,bit0(bit1(pls)))) = zero_zero(int),
inference(split_conjunct,[status(thm)],[1305]) ).
cnf(4256,plain,
linordered_semidom(int),
inference(split_conjunct,[status(thm)],[874]) ).
fof(4382,plain,
! [X29] : equal(minus_minus(int,X29,min),succ(X29)),
inference(variable_rename,[status(thm)],[913]) ).
cnf(4383,plain,
minus_minus(int,X1,min) = succ(X1),
inference(split_conjunct,[status(thm)],[4382]) ).
fof(4413,plain,
! [X2] :
( ~ linordered_semidom(X2)
| ! [X8,X4] :
( ~ hBOOL(hAPP(X2,bool,hAPP(X2,fun(X2,bool),ord_less(X2),zero_zero(X2)),X4))
| hBOOL(hAPP(X2,bool,hAPP(X2,fun(X2,bool),ord_less(X2),zero_zero(X2)),hAPP(nat,X2,power_power(X2,X4),X8))) ) ),
inference(fof_nnf,[status(thm)],[925]) ).
fof(4414,plain,
! [X9] :
( ~ linordered_semidom(X9)
| ! [X10,X11] :
( ~ hBOOL(hAPP(X9,bool,hAPP(X9,fun(X9,bool),ord_less(X9),zero_zero(X9)),X11))
| hBOOL(hAPP(X9,bool,hAPP(X9,fun(X9,bool),ord_less(X9),zero_zero(X9)),hAPP(nat,X9,power_power(X9,X11),X10))) ) ),
inference(variable_rename,[status(thm)],[4413]) ).
fof(4415,plain,
! [X9,X10,X11] :
( ~ hBOOL(hAPP(X9,bool,hAPP(X9,fun(X9,bool),ord_less(X9),zero_zero(X9)),X11))
| hBOOL(hAPP(X9,bool,hAPP(X9,fun(X9,bool),ord_less(X9),zero_zero(X9)),hAPP(nat,X9,power_power(X9,X11),X10)))
| ~ linordered_semidom(X9) ),
inference(shift_quantors,[status(thm)],[4414]) ).
cnf(4416,plain,
( hBOOL(hAPP(X1,bool,hAPP(X1,fun(X1,bool),ord_less(X1),zero_zero(X1)),hAPP(nat,X1,power_power(X1,X2),X3)))
| ~ linordered_semidom(X1)
| ~ hBOOL(hAPP(X1,bool,hAPP(X1,fun(X1,bool),ord_less(X1),zero_zero(X1)),X2)) ),
inference(split_conjunct,[status(thm)],[4415]) ).
fof(5302,plain,
! [X29] : equal(succ(bit0(X29)),bit1(X29)),
inference(variable_rename,[status(thm)],[1187]) ).
cnf(5303,plain,
succ(bit0(X1)) = bit1(X1),
inference(split_conjunct,[status(thm)],[5302]) ).
cnf(5459,plain,
plus_plus(nat,one_one(nat),one_one(nat)) = number_number_of(nat,bit0(bit1(pls))),
inference(split_conjunct,[status(thm)],[1234]) ).
cnf(5540,plain,
plus_plus(nat,one_one(nat),one_one(nat)) = number_number_of(nat,bit0(succ(bit0(pls)))),
inference(rw,[status(thm)],[5459,5303,theory(equality)]),
[unfolding] ).
cnf(5552,negated_conjecture,
hAPP(nat,int,power_power(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,bit0(succ(bit0(pls))))) = zero_zero(int),
inference(rw,[status(thm)],[3829,5303,theory(equality)]),
[unfolding] ).
cnf(5728,plain,
plus_plus(int,pls,pls) = pls,
inference(rw,[status(thm)],[2541,3172,theory(equality)]),
[unfolding] ).
cnf(5756,plain,
plus_plus(nat,one_one(nat),one_one(nat)) = number_number_of(nat,plus_plus(int,succ(plus_plus(int,pls,pls)),succ(plus_plus(int,pls,pls)))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[5540,3172,theory(equality)]),3172,theory(equality)]),
[unfolding] ).
cnf(5768,negated_conjecture,
hAPP(nat,int,power_power(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,plus_plus(int,succ(plus_plus(int,pls,pls)),succ(plus_plus(int,pls,pls))))) = zero_zero(int),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[5552,3172,theory(equality)]),3172,theory(equality)]),
[unfolding] ).
cnf(6006,plain,
plus_plus(nat,one_one(nat),one_one(nat)) = number_number_of(nat,plus_plus(int,minus_minus(int,plus_plus(int,pls,pls),min),minus_minus(int,plus_plus(int,pls,pls),min))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[5756,4383,theory(equality)]),4383,theory(equality)]),
[unfolding] ).
cnf(6018,negated_conjecture,
hAPP(nat,int,power_power(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,plus_plus(int,minus_minus(int,plus_plus(int,pls,pls),min),minus_minus(int,plus_plus(int,pls,pls),min)))) = zero_zero(int),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[5768,4383,theory(equality)]),4383,theory(equality)]),
[unfolding] ).
cnf(6212,plain,
number_number_of(nat,plus_plus(int,minus_minus(int,pls,min),minus_minus(int,pls,min))) = plus_plus(nat,one_one(nat),one_one(nat)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[6006,5728,theory(equality)]),5728,theory(equality)]) ).
cnf(6217,negated_conjecture,
hAPP(nat,int,power_power(int,plus_plus(int,one_one(int),hAPP(nat,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)],[6018,5728,theory(equality)]),5728,theory(equality)]),6212,theory(equality)]) ).
cnf(6218,negated_conjecture,
hAPP(nat,int,power_power(int,plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n))),plus_plus(nat,one_one(nat),one_one(nat))) = pls,
inference(rw,[status(thm)],[6217,1366,theory(equality)]) ).
cnf(7886,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n)))),
inference(rw,[status(thm)],[1453,1366,theory(equality)]) ).
cnf(92564,negated_conjecture,
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),pls))
| ~ linordered_semidom(int)
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n)))) ),
inference(spm,[status(thm)],[4416,6218,theory(equality)]) ).
cnf(92606,negated_conjecture,
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls))
| ~ linordered_semidom(int)
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n)))) ),
inference(rw,[status(thm)],[92564,1366,theory(equality)]) ).
cnf(92607,negated_conjecture,
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls))
| $false
| ~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),plus_plus(int,one_one(int),hAPP(nat,int,semiring_1_of_nat(int),n)))) ),
inference(rw,[status(thm)],[92606,4256,theory(equality)]) ).
cnf(92608,negated_conjecture,
( hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls))
| $false
| $false ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[92607,1366,theory(equality)]),7886,theory(equality)]) ).
cnf(92609,negated_conjecture,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls)),
inference(cn,[status(thm)],[92608,theory(equality)]) ).
cnf(92610,negated_conjecture,
$false,
inference(sr,[status(thm)],[92609,3348,theory(equality)]) ).
cnf(92611,negated_conjecture,
$false,
92610,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM925+7 : TPTP v7.0.0. Released v5.3.0.
% 0.00/0.04 % Command : Source/sine.py -e eprover -t %d %s
% 0.02/0.24 % Computer : n058.star.cs.uiowa.edu
% 0.02/0.24 % Model : x86_64 x86_64
% 0.02/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.02/0.24 % Memory : 32218.625MB
% 0.02/0.24 % OS : Linux 3.10.0-693.2.2.el7.x86_64
% 0.02/0.24 % CPULimit : 300
% 0.02/0.24 % DateTime : Fri Jan 5 16:13:34 CST 2018
% 0.02/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 []
% 2.19/2.48 -running prover on /export/starexec/sandbox2/tmp/tmp3Ko1Bt/sel_theBenchmark.p_1 with time limit 29
% 2.19/2.48 -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/tmp3Ko1Bt/sel_theBenchmark.p_1']
% 2.19/2.48 -prover status Theorem
% 2.19/2.48 Problem theBenchmark.p solved in phase 0.
% 2.19/2.48 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.19/2.48 % SZS status Ended for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.19/2.48 Solved 1 out of 1.
% 2.19/2.48 # Problem is unsatisfiable (or provable), constructing proof object
% 2.19/2.48 # SZS status Theorem
% 2.19/2.48 # SZS output start CNFRefutation.
% See solution above
% 2.19/2.48 # SZS output end CNFRefutation
%------------------------------------------------------------------------------