%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SEV664+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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 : Tue May 5 06:52:38 PM UTC 2026
% Result : Theorem 38.97s 5.47s
% Output : CNFRefutation 38.97s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEV664+1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.33 % Computer : n011.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 300
% 0.14/0.34 % DateTime : Tue May 5 07:54:47 EDT 2026
% 0.14/0.34 % CPUTime :
% 0.29/0.51 % launching worker at depth: 1
% 0.29/0.51 % launching worker at depth: 4
% 0.29/0.51 % launching worker at depth: 3
% 0.29/0.51 % launching worker at depth: 2
% 0.29/0.51 % launching worker at depth: 5
% 0.29/0.51 % launching worker at depth: 6
% 0.29/0.51 % launching worker at depth: 8
% 0.29/0.51 % launching worker at depth: 7
% 2.53/0.83 % launching worker at depth: 9
% 38.97/5.47 % SZS status Theorem for theBenchmark
% 38.97/5.47 % SZS output start CNFRefutation
% 38.97/5.47 fof('_HAMMER_GOAL', plain, ![V0__P]:(cProp___24t(V0__P)=>![V1__Q]:(cProp___24t(V1__Q)=>(V0__P=V1__Q=>(p(V0__P)=>p(V1__Q))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', '_HAMMER_GOAL')).
% 38.97/5.47 fof('_HAMMER_GOAL'_negated, plain, ~(![V0__P]:(cProp___24t(V0__P)=>![V1__Q]:(cProp___24t(V1__Q)=>(V0__P=V1__Q=>(p(V0__P)=>p(V1__Q)))))), inference(negate_conjecture, [status(cth)], ['_HAMMER_GOAL'])).
% 38.97/5.47 cnf(5707, plain, cProp___24t(sK1198), inference(cnf, [status(esa)], ['_HAMMER_GOAL'_negated])).
% 38.97/5.47 cnf(l0, plain, cProp___24t(sK1198), inference(instantiation, [status(thm)], [5707])).
% 38.97/5.47 fof('$_inversion_Coq.Init.Specif.sumbool', plain, ![Vvar__0__A__407,Vvar__1__B__408,VX409]:(cProp___24t(Vvar__0__A__407)=>(cProp___24t(Vvar__1__B__408)=>(cCoq_2eInit_2eSpecif_2esumbool___24t(Vvar__0__A__407,Vvar__1__B__408,VX409)=>((p(Vvar__0__A__407)&VX409=cCoq_2eInit_2eSpecif_2eleft___24a2(Vvar__0__A__407,Vvar__1__B__408))|(p(Vvar__1__B__408)&VX409=cCoq_2eInit_2eSpecif_2eright___24a2(Vvar__0__A__407,Vvar__1__B__408)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', '$_inversion_Coq.Init.Specif.sumbool')).
% 38.97/5.47 cnf(1676, plain, ~cProp___24t(X0) | ~cProp___24t(X1) | ~cCoq_2eInit_2eSpecif_2esumbool___24t(X0,X1,X2) | p(X0) | sP259(X1,X0,X2), inference(cnf, [status(esa)], ['$_inversion_Coq.Init.Specif.sumbool'])).
% 38.97/5.47 cnf(l1, plain, ~cProp___24t(sK1198) | ~cProp___24t(sK1199) | ~cCoq_2eInit_2eSpecif_2esumbool___24t(sK1198,sK1199,happ(happ(cCoq_2eInit_2eSpecif_2eleft,sK1198),sK1199)) | p(sK1198) | sP259(sK1199,sK1198,happ(happ(cCoq_2eInit_2eSpecif_2eleft,sK1198),sK1199)), inference(instantiation, [status(thm)], [1676])).
% 38.97/5.47 cnf(5711, plain, ~p(sK1199), inference(cnf, [status(esa)], ['_HAMMER_GOAL'_negated])).
% 38.97/5.47 cnf(l5, plain, ~p(sK1199), inference(instantiation, [status(thm)], [5711])).
% 38.97/5.47 cnf(5709, plain, sK1198 = sK1199, inference(cnf, [status(esa)], ['_HAMMER_GOAL'_negated])).
% 38.97/5.47 cnf(l22, plain, sK1198 = sK1199, inference(instantiation, [status(thm)], [5709])).
% 38.97/5.47 fof('$_type_8904', plain, ![Vvar__8905]:(c_24__type__8904___24t(Vvar__8905)<=>![Vv__CANONICAL__0]:(cProp___24t(Vv__CANONICAL__0)=>![Vv__CANONICAL__1]:(cProp___24t(Vv__CANONICAL__1)=>(p(Vv__CANONICAL__0)=>cCoq_2eInit_2eSpecif_2esumbool___24t(Vv__CANONICAL__0,Vv__CANONICAL__1,happ(happ(Vvar__8905,Vv__CANONICAL__0),Vv__CANONICAL__1)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', '$_type_8904')).
% 38.97/5.47 cnf(3383, plain, ~p(X0) | ~cProp___24t(X0) | ~cProp___24t(X1) | ~c_24__type__8904___24t(X2) | cCoq_2eInit_2eSpecif_2esumbool___24t(X0,X1,happ(happ(X2,X0),X1)), inference(cnf, [status(esa)], ['$_type_8904'])).
% 38.97/5.47 cnf(l7, plain, ~p(sK1198) | ~cProp___24t(sK1198) | ~cProp___24t(sK1199) | ~c_24__type__8904___24t(cCoq_2eInit_2eSpecif_2eleft) | cCoq_2eInit_2eSpecif_2esumbool___24t(sK1198,sK1199,happ(happ(cCoq_2eInit_2eSpecif_2eleft,sK1198),sK1199)), inference(instantiation, [status(thm)], [3383])).
% 38.97/5.47 fof('$_typeof_Coq.Init.Specif.left', plain, c_24__type__8904___24t(cCoq_2eInit_2eSpecif_2eleft), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', '$_typeof_Coq.Init.Specif.left')).
% 38.97/5.47 cnf(3781, plain, c_24__type__8904___24t(cCoq_2eInit_2eSpecif_2eleft), inference(cnf, [status(esa)], ['$_typeof_Coq.Init.Specif.left'])).
% 38.97/5.47 cnf(l41, plain, c_24__type__8904___24t(cCoq_2eInit_2eSpecif_2eleft), inference(instantiation, [status(thm)], [3781])).
% 38.97/5.47 cnf(5710, plain, p(sK1198), inference(cnf, [status(esa)], ['_HAMMER_GOAL'_negated])).
% 38.97/5.47 cnf(l8, plain, p(sK1198), inference(instantiation, [status(thm)], [5710])).
% 38.97/5.47 cnf(1679, plain, p(X0) | ~sP259(X0,X1,X2), inference(cnf, [status(esa)], ['$_inversion_Coq.Init.Specif.sumbool'])).
% 38.97/5.47 cnf(l44, plain, p(sK1199) | ~sP259(sK1199,sK1198,happ(happ(cCoq_2eInit_2eSpecif_2eleft,sK1198),sK1199)), inference(instantiation, [status(thm)], [1679])).
% 38.97/5.47 cnf(5708, plain, cProp___24t(sK1199), inference(cnf, [status(esa)], ['_HAMMER_GOAL'_negated])).
% 38.97/5.47 cnf(l43, plain, cProp___24t(sK1199), inference(instantiation, [status(thm)], [5708])).
% 38.97/5.47 cnf(l45, plain, ~p(sK1199), inference(instantiation, [status(thm)], [5711])).
% 38.97/5.47 cnf(l55, plain, sK1198 = sK1199, inference(instantiation, [status(thm)], [5709])).
% 38.97/5.47 cnf(final, plain, $false, inference(ground_refutation, [status(thm)], [l0, l1, l5, l22, l7, l41, l8, l44, l43, l45, l55])).
% 38.97/5.47 % SZS output end CNFRefutation
%------------------------------------------------------------------------------