%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : NUM925+6 : TPTP v7.0.0. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : n061.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.47s
% Output : CNFRefutation 0.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 8
% Syntax : Number of formulae : 34 ( 25 unt; 0 def)
% Number of atoms : 52 ( 7 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 : 16 ( 16 usr; 7 con; 0-4 aty)
% Number of variables : 18 ( 1 sgn 14 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(7,axiom,
equal(pls,zero_zero(int)),
file('/export/starexec/sandbox/tmp/tmpo41AVh/sel_theBenchmark.p_1',fact_73_Pls__def) ).
fof(16,axiom,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n)))),
file('/export/starexec/sandbox/tmp/tmpo41AVh/sel_theBenchmark.p_1',fact_0_n1pos) ).
fof(305,axiom,
linordered_semidom(int),
file('/export/starexec/sandbox/tmp/tmpo41AVh/sel_theBenchmark.p_1',arity_Int_Oint___Rings_Olinordered__semidom) ).
fof(314,axiom,
equal(one_one(int),number_number_of(int,hAPP(int,int,bit1,pls))),
file('/export/starexec/sandbox/tmp/tmpo41AVh/sel_theBenchmark.p_1',fact_37_one__is__num__one) ).
fof(329,axiom,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls)),
file('/export/starexec/sandbox/tmp/tmpo41AVh/sel_theBenchmark.p_1',fact_32_rel__simps_I2_J) ).
fof(346,axiom,
! [X9] : equal(number_number_of(int,X9),X9),
file('/export/starexec/sandbox/tmp/tmpo41AVh/sel_theBenchmark.p_1',fact_119_number__of__is__id) ).
fof(445,axiom,
! [X1] :
( linordered_semidom(X1)
=> ! [X16,X3] :
( hBOOL(hAPP(X1,bool,hAPP(X1,fun(X1,bool),ord_less(X1),zero_zero(X1)),X3))
=> hBOOL(hAPP(X1,bool,hAPP(X1,fun(X1,bool),ord_less(X1),zero_zero(X1)),hAPP(nat,X1,power_power(X1,X3),X16))) ) ),
file('/export/starexec/sandbox/tmp/tmpo41AVh/sel_theBenchmark.p_1',fact_178_zero__less__power) ).
fof(613,conjecture,
~ equal(hAPP(nat,int,power_power(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),zero_zero(int)),
file('/export/starexec/sandbox/tmp/tmpo41AVh/sel_theBenchmark.p_1',conj_0) ).
fof(661,negated_conjecture,
~ ~ equal(hAPP(nat,int,power_power(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),zero_zero(int)),
inference(assume_negation,[status(cth)],[613]) ).
fof(691,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls)),
inference(fof_simplification,[status(thm)],[329,theory(equality)]) ).
fof(711,negated_conjecture,
equal(hAPP(nat,int,power_power(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))),zero_zero(int)),
inference(fof_simplification,[status(thm)],[661,theory(equality)]) ).
cnf(738,plain,
pls = zero_zero(int),
inference(split_conjunct,[status(thm)],[7]) ).
cnf(762,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),zero_zero(int)),hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n)))),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(1739,plain,
linordered_semidom(int),
inference(split_conjunct,[status(thm)],[305]) ).
cnf(1768,plain,
one_one(int) = number_number_of(int,hAPP(int,int,bit1,pls)),
inference(split_conjunct,[status(thm)],[314]) ).
cnf(1820,plain,
~ hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls)),
inference(split_conjunct,[status(thm)],[691]) ).
fof(1874,plain,
! [X10] : equal(number_number_of(int,X10),X10),
inference(variable_rename,[status(thm)],[346]) ).
cnf(1875,plain,
number_number_of(int,X1) = X1,
inference(split_conjunct,[status(thm)],[1874]) ).
fof(2197,plain,
! [X1] :
( ~ linordered_semidom(X1)
| ! [X16,X3] :
( ~ hBOOL(hAPP(X1,bool,hAPP(X1,fun(X1,bool),ord_less(X1),zero_zero(X1)),X3))
| hBOOL(hAPP(X1,bool,hAPP(X1,fun(X1,bool),ord_less(X1),zero_zero(X1)),hAPP(nat,X1,power_power(X1,X3),X16))) ) ),
inference(fof_nnf,[status(thm)],[445]) ).
fof(2198,plain,
! [X17] :
( ~ linordered_semidom(X17)
| ! [X18,X19] :
( ~ hBOOL(hAPP(X17,bool,hAPP(X17,fun(X17,bool),ord_less(X17),zero_zero(X17)),X19))
| hBOOL(hAPP(X17,bool,hAPP(X17,fun(X17,bool),ord_less(X17),zero_zero(X17)),hAPP(nat,X17,power_power(X17,X19),X18))) ) ),
inference(variable_rename,[status(thm)],[2197]) ).
fof(2199,plain,
! [X17,X18,X19] :
( ~ hBOOL(hAPP(X17,bool,hAPP(X17,fun(X17,bool),ord_less(X17),zero_zero(X17)),X19))
| hBOOL(hAPP(X17,bool,hAPP(X17,fun(X17,bool),ord_less(X17),zero_zero(X17)),hAPP(nat,X17,power_power(X17,X19),X18)))
| ~ linordered_semidom(X17) ),
inference(shift_quantors,[status(thm)],[2198]) ).
cnf(2200,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)],[2199]) ).
cnf(2794,negated_conjecture,
hAPP(nat,int,power_power(int,hAPP(int,int,plus_plus(int,one_one(int)),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))) = zero_zero(int),
inference(split_conjunct,[status(thm)],[711]) ).
cnf(2950,plain,
hAPP(int,int,bit1,pls) = one_one(int),
inference(rw,[status(thm)],[1768,1875,theory(equality)]) ).
cnf(3961,negated_conjecture,
hAPP(nat,int,power_power(int,hAPP(int,int,plus_plus(int,hAPP(int,int,bit1,pls)),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))) = zero_zero(int),
inference(rw,[status(thm)],[2794,2950,theory(equality)]) ).
cnf(3962,negated_conjecture,
hAPP(nat,int,power_power(int,hAPP(int,int,plus_plus(int,hAPP(int,int,bit1,pls)),hAPP(nat,int,semiring_1_of_nat(int),n))),number_number_of(nat,hAPP(int,int,bit0,hAPP(int,int,bit1,pls)))) = pls,
inference(rw,[status(thm)],[3961,738,theory(equality)]) ).
cnf(5596,plain,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),hAPP(int,int,plus_plus(int,hAPP(int,int,bit1,pls)),hAPP(nat,int,semiring_1_of_nat(int),n)))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[762,738,theory(equality)]),2950,theory(equality)]) ).
cnf(18165,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)),hAPP(int,int,plus_plus(int,hAPP(int,int,bit1,pls)),hAPP(nat,int,semiring_1_of_nat(int),n)))) ),
inference(spm,[status(thm)],[2200,3962,theory(equality)]) ).
cnf(18200,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)),hAPP(int,int,plus_plus(int,hAPP(int,int,bit1,pls)),hAPP(nat,int,semiring_1_of_nat(int),n)))) ),
inference(rw,[status(thm)],[18165,738,theory(equality)]) ).
cnf(18201,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)),hAPP(int,int,plus_plus(int,hAPP(int,int,bit1,pls)),hAPP(nat,int,semiring_1_of_nat(int),n)))) ),
inference(rw,[status(thm)],[18200,1739,theory(equality)]) ).
cnf(18202,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)],[18201,738,theory(equality)]),5596,theory(equality)]) ).
cnf(18203,negated_conjecture,
hBOOL(hAPP(int,bool,hAPP(int,fun(int,bool),ord_less(int),pls),pls)),
inference(cn,[status(thm)],[18202,theory(equality)]) ).
cnf(18204,negated_conjecture,
$false,
inference(sr,[status(thm)],[18203,1820,theory(equality)]) ).
cnf(18205,negated_conjecture,
$false,
18204,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM925+6 : TPTP v7.0.0. Released v5.3.0.
% 0.00/0.04 % Command : Source/sine.py -e eprover -t %d %s
% 0.03/0.23 % Computer : n061.star.cs.uiowa.edu
% 0.03/0.23 % Model : x86_64 x86_64
% 0.03/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz
% 0.03/0.23 % Memory : 32218.625MB
% 0.03/0.23 % OS : Linux 3.10.0-693.2.2.el7.x86_64
% 0.03/0.23 % CPULimit : 300
% 0.03/0.23 % DateTime : Fri Jan 5 16:40:05 CST 2018
% 0.03/0.24 % CPUTime :
% 0.03/0.28 % SZS status Started for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.28 --creating new selector for []
% 0.47/0.83 -running prover on /export/starexec/sandbox/tmp/tmpo41AVh/sel_theBenchmark.p_1 with time limit 29
% 0.47/0.83 -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/tmpo41AVh/sel_theBenchmark.p_1']
% 0.47/0.83 -prover status Theorem
% 0.47/0.83 Problem theBenchmark.p solved in phase 0.
% 0.47/0.83 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.47/0.83 % SZS status Ended for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.47/0.83 Solved 1 out of 1.
% 0.47/0.83 # Problem is unsatisfiable (or provable), constructing proof object
% 0.47/0.83 # SZS status Theorem
% 0.47/0.83 # SZS output start CNFRefutation.
% See solution above
% 0.47/0.83 # SZS output end CNFRefutation
%------------------------------------------------------------------------------