%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : CSR061+6 : TPTP v9.0.0. Bugfixed v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n023.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Jul 24 11:18:56 AM UTC 2025
% Result : Theorem 87.91s 42.00s
% Output : CNFRefutation 87.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 8
% Syntax : Number of formulae : 26 ( 6 unt; 0 def)
% Number of atoms : 46 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 36 ( 16 ~; 12 |; 1 &)
% ( 0 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 8 con; 0-1 aty)
% Number of variables : 22 ( 4 sgn 11 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(query311,plain,
( mtvisible(c_timehasnoendmt)
=> disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',query311) ).
fof(query311_negated,plain,
~ ( mtvisible(c_timehasnoendmt)
=> disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) ),
inference(negate_conjecture,[status(cth)],[query311]) ).
cnf(3341967,plain,
mtvisible(c_timehasnoendmt),
inference(cnf,[status(esa)],[query311_negated]) ).
cnf(l0,plain,
mtvisible(c_timehasnoendmt),
inference(instantiation,[status(thm)],[3341967]) ).
fof(ax5_624035,plain,
( mtvisible(c_timehasnoendmt)
=> argisa(c_intervalstartedby,n_1,f_samelengthtimeintervaltypefn(c_forever_quantity)) ),
file('Axioms/CSR002+5.ax',ax5_624035) ).
cnf(623930,plain,
( ~ mtvisible(c_timehasnoendmt)
| argisa(c_intervalstartedby,n_1,f_samelengthtimeintervaltypefn(c_forever_quantity)) ),
inference(cnf,[status(esa)],[ax5_624035]) ).
cnf(l1,plain,
( ~ mtvisible(c_timehasnoendmt)
| argisa(c_intervalstartedby,n_1,f_samelengthtimeintervaltypefn(c_forever_quantity)) ),
inference(instantiation,[status(thm)],[623930]) ).
fof(ax5_1597063,plain,
! [ARG1,ARG2,ARG3] :
( argisa(ARG1,ARG2,ARG3)
=> argelementof(ARG1,ARG2,ARG3) ),
file('Axioms/CSR002+5.ax',ax5_1597063) ).
cnf(1596812,plain,
( ~ argisa(X0,X1,X2)
| argelementof(X0,X1,X2) ),
inference(cnf,[status(esa)],[ax5_1597063]) ).
cnf(l14,plain,
( ~ argisa(c_intervalstartedby,n_1,f_samelengthtimeintervaltypefn(c_forever_quantity))
| argelementof(c_intervalstartedby,n_1,f_samelengthtimeintervaltypefn(c_forever_quantity)) ),
inference(instantiation,[status(thm)],[1596812]) ).
fof(ax5_2770413,plain,
! [ARG1,ARG2,ARG3] :
( argelementof(ARG1,ARG2,ARG3)
=> nonnegativeinteger(ARG2) ),
file('Axioms/CSR002+5.ax',ax5_2770413) ).
cnf(2769961,plain,
( ~ argelementof(X0,X1,X2)
| nonnegativeinteger(X1) ),
inference(cnf,[status(esa)],[ax5_2770413]) ).
cnf(l33,plain,
( ~ argelementof(c_intervalstartedby,n_1,f_samelengthtimeintervaltypefn(c_forever_quantity))
| nonnegativeinteger(n_1) ),
inference(instantiation,[status(thm)],[2769961]) ).
fof(ax5_446947,plain,
! [OBJ] :
~ ( nonnegativeinteger(OBJ)
& truthvalue(OBJ) ),
file('Axioms/CSR002+5.ax',ax5_446947) ).
cnf(446866,plain,
( ~ nonnegativeinteger(X0)
| ~ truthvalue(X0) ),
inference(cnf,[status(esa)],[ax5_446947]) ).
cnf(l53,plain,
( ~ nonnegativeinteger(n_1)
| ~ truthvalue(n_1) ),
inference(instantiation,[status(thm)],[446866]) ).
fof(ax5_3309992,plain,
! [X] :
( isa(X,c_truthvalue)
=> truthvalue(X) ),
file('Axioms/CSR002+5.ax',ax5_3309992) ).
cnf(3309510,plain,
( ~ isa(X0,c_truthvalue)
| truthvalue(X0) ),
inference(cnf,[status(esa)],[ax5_3309992]) ).
cnf(l85,plain,
( ~ isa(n_1,c_truthvalue)
| truthvalue(n_1) ),
inference(instantiation,[status(thm)],[3309510]) ).
fof(ax5_1761490,plain,
! [ARG1,ARG2,OBJ] :
( conceptuallyrelated(ARG1,ARG2)
=> isa(OBJ,ARG2) ),
file('Axioms/CSR002+5.ax',ax5_1761490) ).
cnf(1761207,plain,
( ~ conceptuallyrelated(X0,X1)
| isa(X2,X1) ),
inference(cnf,[status(esa)],[ax5_1761490]) ).
cnf(l87,plain,
( ~ conceptuallyrelated(c_cychltruthvalue,c_truthvalue)
| isa(n_1,c_truthvalue) ),
inference(instantiation,[status(thm)],[1761207]) ).
fof(ax5_1551952,plain,
conceptuallyrelated(c_cychltruthvalue,c_truthvalue),
file('Axioms/CSR002+5.ax',ax5_1551952) ).
cnf(1551712,plain,
conceptuallyrelated(c_cychltruthvalue,c_truthvalue),
inference(cnf,[status(esa)],[ax5_1551952]) ).
cnf(l155,plain,
conceptuallyrelated(c_cychltruthvalue,c_truthvalue),
inference(instantiation,[status(thm)],[1551712]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l14,l33,l53,l85,l87,l155]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : CSR061+6 : TPTP v9.0.0. Bugfixed v5.3.0.
% 0.11/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.33 % Computer : n023.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Sun Jul 20 07:08:04 EDT 2025
% 0.13/0.33 % CPUTime :
% 35.15/35.32 % launching worker at depth: 1
% 35.15/35.32 % launching worker at depth: 2
% 35.15/35.32 % launching worker at depth: 3
% 35.15/35.32 % launching worker at depth: 4
% 35.15/35.32 % launching worker at depth: 6
% 35.15/35.32 % launching worker at depth: 5
% 35.15/35.32 % launching worker at depth: 7
% 35.15/35.32 % launching worker at depth: 8
% 51.00/37.35 % launching worker at depth: 9
% 87.91/42.00 % SZS status Theorem for theBenchmark
% 87.91/42.00 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------