%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : CSR070+1 : TPTP v9.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n027.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:19:02 AM UTC 2025
% Result : Theorem 0.12s 0.34s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : CSR070+1 : TPTP v9.0.0. Released v3.4.0.
% 0.07/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.34 % Computer : n027.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Sun Jul 20 07:15:19 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 3
% 0.12/0.34 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 9
% 0.12/0.34 % SZS status Theorem for theBenchmark
% 0.12/0.34 % SZS output start CNFRefutation
% 0.12/0.34 fof(query70, plain, (mtvisible(c_tptp_spindlecollectormt)=>tptptypes_5_802(f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible),c_tptpcol_16_8886)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', query70)).
% 0.12/0.34 % launching worker at depth: fof(query70_negated, plain, ~((mtvisible(c_tptp_spindlecollectormt)=>tptptypes_5_802(f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible),c_tptpcol_16_8886))), inference(negate_conjecture, [status(cth)], [query70])).
% 0.12/0.34 10
% 0.12/0.34 cnf(79, plain, mtvisible(c_tptp_spindlecollectormt), inference(cnf, [status(esa)], [query70_negated])).
% 0.12/0.34 cnf(l0, plain, mtvisible(c_tptp_spindlecollectormt), inference(instantiation, [status(thm)], [79])).
% 0.12/0.34 fof(just57, plain, ![SPECMT,GENLMT]:((mtvisible(SPECMT)&genlmt(SPECMT,GENLMT))=>mtvisible(GENLMT)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just57)).
% 0.12/0.34 cnf(56, plain, ~genlmt(X0,X1) | ~mtvisible(X0) | mtvisible(X1), inference(cnf, [status(esa)], [just57])).
% 0.12/0.34 cnf(l1, plain, ~genlmt(c_tptp_spindlecollectormt,c_tptp_member2668_mt) | ~mtvisible(c_tptp_spindlecollectormt) | mtvisible(c_tptp_member2668_mt), inference(instantiation, [status(thm)], [56])).
% 0.12/0.34 fof(just16, plain, genlmt(c_tptp_spindlecollectormt,c_tptp_member2668_mt), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just16)).
% 0.12/0.34 cnf(15, plain, genlmt(c_tptp_spindlecollectormt,c_tptp_member2668_mt), inference(cnf, [status(esa)], [just16])).
% 0.12/0.34 cnf(l2, plain, genlmt(c_tptp_spindlecollectormt,c_tptp_member2668_mt), inference(instantiation, [status(thm)], [15])).
% 0.12/0.34 fof(just19, plain, (mtvisible(c_tptp_member2668_mt)=>tptptypes_9_824(f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible),c_tptpcol_16_8886)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just19)).
% 0.12/0.34 cnf(18, plain, ~mtvisible(c_tptp_member2668_mt) | tptptypes_9_824(f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible),c_tptpcol_16_8886), inference(cnf, [status(esa)], [just19])).
% 0.12/0.34 cnf(l3, plain, ~mtvisible(c_tptp_member2668_mt) | tptptypes_9_824(f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible),c_tptpcol_16_8886), inference(instantiation, [status(thm)], [18])).
% 0.12/0.34 fof(just14, plain, ![ARG1,ARG2]:(tptptypes_9_824(ARG1,ARG2)=>tptptypes_8_823(ARG1,ARG2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just14)).
% 0.12/0.34 cnf(13, plain, ~tptptypes_9_824(X0,X1) | tptptypes_8_823(X0,X1), inference(cnf, [status(esa)], [just14])).
% 0.12/0.34 cnf(l4, plain, ~tptptypes_9_824(f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible),c_tptpcol_16_8886) | tptptypes_8_823(f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible),c_tptpcol_16_8886), inference(instantiation, [status(thm)], [13])).
% 0.12/0.34 fof(just12, plain, ![ARG1,ARG2]:(tptptypes_8_823(ARG1,ARG2)=>tptptypes_7_819(ARG1,ARG2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just12)).
% 0.12/0.34 cnf(11, plain, ~tptptypes_8_823(X0,X1) | tptptypes_7_819(X0,X1), inference(cnf, [status(esa)], [just12])).
% 0.12/0.34 cnf(l5, plain, ~tptptypes_8_823(f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible),c_tptpcol_16_8886) | tptptypes_7_819(f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible),c_tptpcol_16_8886), inference(instantiation, [status(thm)], [11])).
% 0.12/0.34 fof(just10, plain, ![ARG1,ARG2]:(tptptypes_7_819(ARG1,ARG2)=>tptptypes_6_818(ARG1,ARG2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just10)).
% 0.12/0.34 cnf(9, plain, ~tptptypes_7_819(X0,X1) | tptptypes_6_818(X0,X1), inference(cnf, [status(esa)], [just10])).
% 0.12/0.34 cnf(l6, plain, ~tptptypes_7_819(f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible),c_tptpcol_16_8886) | tptptypes_6_818(f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible),c_tptpcol_16_8886), inference(instantiation, [status(thm)], [9])).
% 0.12/0.34 fof(just8, plain, ![ARG1,ARG2]:(tptptypes_6_818(ARG1,ARG2)=>tptptypes_5_802(ARG1,ARG2)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', just8)).
% 0.12/0.34 cnf(7, plain, ~tptptypes_6_818(X0,X1) | tptptypes_5_802(X0,X1), inference(cnf, [status(esa)], [just8])).
% 0.12/0.34 cnf(l7, plain, ~tptptypes_6_818(f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible),c_tptpcol_16_8886) | tptptypes_5_802(f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible),c_tptpcol_16_8886), inference(instantiation, [status(thm)], [7])).
% 0.12/0.34 cnf(80, plain, ~tptptypes_5_802(f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible),c_tptpcol_16_8886), inference(cnf, [status(esa)], [query70_negated])).
% 0.12/0.34 cnf(l8, plain, ~tptptypes_5_802(f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible),c_tptpcol_16_8886), inference(instantiation, [status(thm)], [80])).
% 0.12/0.34 cnf(final, plain, $false, inference(ground_refutation, [status(thm)], [l0, l1, l2, l3, l4, l5, l6, l7, l8])).
% 0.12/0.34 % SZS output end CNFRefutation
%------------------------------------------------------------------------------