%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : CSR056+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 : n031.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:53 AM UTC 2025
% Result : Theorem 35.67s 35.76s
% Output : CNFRefutation 35.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 6
% Syntax : Number of formulae : 20 ( 6 unt; 0 def)
% Number of atoms : 34 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 26 ( 12 ~; 8 |; 0 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-1 aty)
% Number of variables : 16 ( 2 sgn 7 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(query306,plain,
? [QUANTITY] :
( mtvisible(c_tptp_member3717_mt)
=> tptpofobject(c_tptpartsupplies,QUANTITY) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',query306) ).
fof(query306_negated,plain,
~ ? [QUANTITY] :
( mtvisible(c_tptp_member3717_mt)
=> tptpofobject(c_tptpartsupplies,QUANTITY) ),
inference(negate_conjecture,[status(cth)],[query306]) ).
cnf(3341967,plain,
mtvisible(c_tptp_member3717_mt),
inference(cnf,[status(esa)],[query306_negated]) ).
cnf(l0,plain,
mtvisible(c_tptp_member3717_mt),
inference(instantiation,[status(thm)],[3341967]) ).
fof(ax5_1067071,plain,
( mtvisible(c_tptp_member3717_mt)
=> relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_17(n_385)) ),
file('Axioms/CSR002+5.ax',ax5_1067071) ).
cnf(1066915,plain,
( ~ mtvisible(c_tptp_member3717_mt)
| relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_17(n_385)) ),
inference(cnf,[status(esa)],[ax5_1067071]) ).
cnf(l1,plain,
( ~ mtvisible(c_tptp_member3717_mt)
| relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_17(n_385)) ),
inference(instantiation,[status(thm)],[1066915]) ).
fof(ax5_517164,plain,
! [ARG1,ARG2,ARG3] :
( relationallinstance(ARG1,ARG2,ARG3)
=> collection(ARG2) ),
file('Axioms/CSR002+5.ax',ax5_517164) ).
cnf(517075,plain,
( ~ relationallinstance(X0,X1,X2)
| collection(X1) ),
inference(cnf,[status(esa)],[ax5_517164]) ).
cnf(l2,plain,
( ~ relationallinstance(c_tptpofobject,c_supplies,f_tptpquantityfn_17(n_385))
| collection(c_supplies) ),
inference(instantiation,[status(thm)],[517075]) ).
fof(ax5_3263384,plain,
! [X] :
( collection(X)
=> taxonomicsiblingcollections(X,X) ),
file('Axioms/CSR002+5.ax',ax5_3263384) ).
cnf(3262903,plain,
( ~ collection(X0)
| taxonomicsiblingcollections(X0,X0) ),
inference(cnf,[status(esa)],[ax5_3263384]) ).
cnf(l3,plain,
( ~ collection(c_supplies)
| taxonomicsiblingcollections(c_supplies,c_supplies) ),
inference(instantiation,[status(thm)],[3262903]) ).
fof(ax5_895896,plain,
! [ARG1,ARG2] :
( taxonomicsiblingcollections(ARG1,ARG2)
=> taxonomiccousincollections(ARG1,ARG2) ),
file('Axioms/CSR002+5.ax',ax5_895896) ).
cnf(895749,plain,
( ~ taxonomicsiblingcollections(X0,X1)
| taxonomiccousincollections(X0,X1) ),
inference(cnf,[status(esa)],[ax5_895896]) ).
cnf(l4,plain,
( ~ taxonomicsiblingcollections(c_supplies,c_supplies)
| taxonomiccousincollections(c_supplies,c_supplies) ),
inference(instantiation,[status(thm)],[895749]) ).
fof(ax5_3145099,plain,
! [X] : ~ taxonomiccousincollections(X,X),
file('Axioms/CSR002+5.ax',ax5_3145099) ).
cnf(3144619,plain,
~ taxonomiccousincollections(X0,X0),
inference(cnf,[status(esa)],[ax5_3145099]) ).
cnf(l5,plain,
~ taxonomiccousincollections(c_supplies,c_supplies),
inference(instantiation,[status(thm)],[3144619]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l2,l3,l4,l5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : CSR056+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.12/0.33 % Computer : n031.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Sun Jul 20 07:02:49 EDT 2025
% 0.12/0.33 % CPUTime :
% 35.44/35.69 % launching worker at depth: 1
% 35.44/35.69 % launching worker at depth: 2
% 35.44/35.69 % launching worker at depth: 3
% 35.44/35.69 % launching worker at depth: 4
% 35.44/35.69 % launching worker at depth: 5
% 35.44/35.69 % launching worker at depth: 6
% 35.44/35.69 % launching worker at depth: 7
% 35.44/35.69 % launching worker at depth: 8
% 35.67/35.76 % SZS status Theorem for theBenchmark
% 35.67/35.76 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------