%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : SEV679+1 : TPTP v9.3.0. Released v9.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 : Tue May 5 06:52:39 PM UTC 2026
% Result : Theorem 7.62s 1.58s
% Output : CNFRefutation 7.62s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.13 % Problem : SEV679+1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.14 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.36 % Computer : n023.cluster.edu
% 0.19/0.36 % Model : x86_64 x86_64
% 0.19/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.36 % Memory : 8042.1875MB
% 0.19/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.19/0.36 % CPULimit : 300
% 0.19/0.36 % WCLimit : 300
% 0.19/0.36 % DateTime : Tue May 5 08:27:53 EDT 2026
% 0.19/0.37 % CPUTime :
% 0.41/0.60 % launching worker at depth: 1
% 0.41/0.60 % launching worker at depth: 7
% 0.41/0.60 % launching worker at depth: 6
% 0.41/0.60 % launching worker at depth: 4
% 0.41/0.60 % launching worker at depth: 2
% 0.41/0.60 % launching worker at depth: 3
% 0.41/0.60 % launching worker at depth: 5
% 0.41/0.60 % launching worker at depth: 8
% 0.41/0.60 % launching worker at depth: 9
% 7.62/1.58 % SZS status Theorem for theBenchmark
% 7.62/1.58 % SZS output start CNFRefutation
% 7.62/1.58 fof('_HAMMER_GOAL', plain, ![V0__ST]:(cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V0__ST)=>![V1__t]:(cPLF_2eReferences_2eSTLCRef_2etm___24t(V1__t)=>![V2__t_27]:(cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27)=>![V3__T]:(cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T)=>![V4__st]:(cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)=>![V5__st_27]:(cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)=>(cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety),V0__ST,V1__t,V3__T)=>(cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST,V4__st)=>(cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,V1__t,V4__st),cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,V2__t_27,V5__st_27))=>?[V9__ST_27]:(cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27)&cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27,V0__ST)&cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety),V9__ST_27,V2__t_27,V3__T)&cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27,V5__st_27))))))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', '_HAMMER_GOAL')).
% 7.62/1.58 fof('_HAMMER_GOAL'_negated, plain, ~(![V0__ST]:(cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V0__ST)=>![V1__t]:(cPLF_2eReferences_2eSTLCRef_2etm___24t(V1__t)=>![V2__t_27]:(cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27)=>![V3__T]:(cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T)=>![V4__st]:(cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)=>![V5__st_27]:(cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)=>(cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety),V0__ST,V1__t,V3__T)=>(cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST,V4__st)=>(cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,V1__t,V4__st),cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,V2__t_27,V5__st_27))=>?[V9__ST_27]:(cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27)&cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27,V0__ST)&cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety),V9__ST_27,V2__t_27,V3__T)&cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27,V5__st_27)))))))))))), inference(negate_conjecture, [status(cth)], ['_HAMMER_GOAL'])).
% 7.62/1.58 cnf(9428, plain, ~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety),X0,sK2514,sK2515) | ~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(X0,sK2517) | ~cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(X0) | ~cPLF_2eReferences_2eSTLCRef_2eextends___24a2(X0,sK2512), inference(cnf, [status(esa)], ['_HAMMER_GOAL'_negated])).
% 7.62/1.58 cnf(l0, plain, ~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety),sK2507(sK2512,sK2513,sK2514,sK2515,sK2516,sK2517),sK2514,sK2515) | ~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(sK2507(sK2512,sK2513,sK2514,sK2515,sK2516,sK2517),sK2517) | ~cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(sK2507(sK2512,sK2513,sK2514,sK2515,sK2516,sK2517)) | ~cPLF_2eReferences_2eSTLCRef_2eextends___24a2(sK2507(sK2512,sK2513,sK2514,sK2515,sK2516,sK2517),sK2512), inference(instantiation, [status(thm)], [9428])).
% 7.62/1.58 fof('UseAuto.PreservationProgressReferences.preservation', plain, ![V0__ST]:(cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V0__ST)=>![V1__t]:(cPLF_2eReferences_2eSTLCRef_2etm___24t(V1__t)=>![V2__t_27]:(cPLF_2eReferences_2eSTLCRef_2etm___24t(V2__t_27)=>![V3__T]:(cPLF_2eReferences_2eSTLCRef_2ety___24t(V3__T)=>![V4__st]:(cPLF_2eReferences_2eSTLCRef_2estore___24t(V4__st)=>![V5__st_27]:(cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)=>(cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety),V0__ST,V1__t,V3__T)=>(cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST,V4__st)=>(cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,V1__t,V4__st),cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,V2__t_27,V5__st_27))=>?[V9__ST_27]:(cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(V9__ST_27)&cPLF_2eReferences_2eSTLCRef_2eextends___24a2(V9__ST_27,V0__ST)&cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety),V9__ST_27,V2__t_27,V3__T)&cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27,V5__st_27))))))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', 'UseAuto.PreservationProgressReferences.preservation')).
% 7.62/1.58 cnf(7536, plain, ~cPLF_2eReferences_2eSTLCRef_2estore___24t(X0) | ~cPLF_2eReferences_2eSTLCRef_2estore___24t(X1) | ~cPLF_2eReferences_2eSTLCRef_2etm___24t(X2) | ~cPLF_2eReferences_2eSTLCRef_2etm___24t(X3) | ~cPLF_2eReferences_2eSTLCRef_2ety___24t(X4) | ~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety),X5,X2,X4) | ~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(X5,X0) | ~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,X2,X0),cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,X3,X1)) | ~cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(X5) | cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(sK2507(X5,X2,X3,X4,X0,X1),X1), inference(cnf, [status(esa)], ['UseAuto.PreservationProgressReferences.preservation'])).
% 7.62/1.58 cnf(l39, plain, ~cPLF_2eReferences_2eSTLCRef_2estore___24t(sK2516) | ~cPLF_2eReferences_2eSTLCRef_2estore___24t(sK2517) | ~cPLF_2eReferences_2eSTLCRef_2etm___24t(sK2513) | ~cPLF_2eReferences_2eSTLCRef_2etm___24t(sK2514) | ~cPLF_2eReferences_2eSTLCRef_2ety___24t(sK2515) | ~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety),sK2512,sK2513,sK2515) | ~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(sK2512,sK2516) | ~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,sK2513,sK2516),cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,sK2514,sK2517)) | ~cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(sK2512) | cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(sK2507(sK2512,sK2513,sK2514,sK2515,sK2516,sK2517),sK2517), inference(instantiation, [status(thm)], [7536])).
% 7.62/1.58 cnf(7535, plain, ~cPLF_2eReferences_2eSTLCRef_2estore___24t(X0) | ~cPLF_2eReferences_2eSTLCRef_2estore___24t(X1) | ~cPLF_2eReferences_2eSTLCRef_2etm___24t(X2) | ~cPLF_2eReferences_2eSTLCRef_2etm___24t(X3) | ~cPLF_2eReferences_2eSTLCRef_2ety___24t(X4) | ~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety),X5,X2,X4) | ~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(X5,X0) | ~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,X2,X0),cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,X3,X1)) | ~cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(X5) | cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety),sK2507(X5,X2,X3,X4,X0,X1),X3,X4), inference(cnf, [status(esa)], ['UseAuto.PreservationProgressReferences.preservation'])).
% 7.62/1.58 cnf(l1, plain, ~cPLF_2eReferences_2eSTLCRef_2estore___24t(sK2516) | ~cPLF_2eReferences_2eSTLCRef_2estore___24t(sK2517) | ~cPLF_2eReferences_2eSTLCRef_2etm___24t(sK2513) | ~cPLF_2eReferences_2eSTLCRef_2etm___24t(sK2514) | ~cPLF_2eReferences_2eSTLCRef_2ety___24t(sK2515) | ~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety),sK2512,sK2513,sK2515) | ~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(sK2512,sK2516) | ~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,sK2513,sK2516),cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,sK2514,sK2517)) | ~cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(sK2512) | cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety),sK2507(sK2512,sK2513,sK2514,sK2515,sK2516,sK2517),sK2514,sK2515), inference(instantiation, [status(thm)], [7535])).
% 7.62/1.58 cnf(9421, plain, cPLF_2eReferences_2eSTLCRef_2etm___24t(sK2514), inference(cnf, [status(esa)], ['_HAMMER_GOAL'_negated])).
% 7.62/1.58 cnf(l8, plain, cPLF_2eReferences_2eSTLCRef_2etm___24t(sK2514), inference(instantiation, [status(thm)], [9421])).
% 7.62/1.58 cnf(9425, plain, cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety),sK2512,sK2513,sK2515), inference(cnf, [status(esa)], ['_HAMMER_GOAL'_negated])).
% 7.62/1.58 cnf(l45, plain, cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety),sK2512,sK2513,sK2515), inference(instantiation, [status(thm)], [9425])).
% 7.62/1.58 cnf(9427, plain, cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,sK2513,sK2516),cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,sK2514,sK2517)), inference(cnf, [status(esa)], ['_HAMMER_GOAL'_negated])).
% 7.62/1.58 cnf(l42, plain, cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,sK2513,sK2516),cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,sK2514,sK2517)), inference(instantiation, [status(thm)], [9427])).
% 7.62/1.58 cnf(9419, plain, cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(sK2512), inference(cnf, [status(esa)], ['_HAMMER_GOAL'_negated])).
% 7.62/1.58 cnf(l13, plain, cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(sK2512), inference(instantiation, [status(thm)], [9419])).
% 7.62/1.58 cnf(9420, plain, cPLF_2eReferences_2eSTLCRef_2etm___24t(sK2513), inference(cnf, [status(esa)], ['_HAMMER_GOAL'_negated])).
% 7.62/1.58 cnf(l2, plain, cPLF_2eReferences_2eSTLCRef_2etm___24t(sK2513), inference(instantiation, [status(thm)], [9420])).
% 7.62/1.58 cnf(9422, plain, cPLF_2eReferences_2eSTLCRef_2ety___24t(sK2515), inference(cnf, [status(esa)], ['_HAMMER_GOAL'_negated])).
% 7.62/1.58 cnf(l9, plain, cPLF_2eReferences_2eSTLCRef_2ety___24t(sK2515), inference(instantiation, [status(thm)], [9422])).
% 7.62/1.58 cnf(l3, plain, cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety),sK2512,sK2513,sK2515), inference(instantiation, [status(thm)], [9425])).
% 7.62/1.58 cnf(9424, plain, cPLF_2eReferences_2eSTLCRef_2estore___24t(sK2517), inference(cnf, [status(esa)], ['_HAMMER_GOAL'_negated])).
% 7.62/1.58 cnf(l4, plain, cPLF_2eReferences_2eSTLCRef_2estore___24t(sK2517), inference(instantiation, [status(thm)], [9424])).
% 7.62/1.58 cnf(9426, plain, cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(sK2512,sK2516), inference(cnf, [status(esa)], ['_HAMMER_GOAL'_negated])).
% 7.62/1.58 cnf(l40, plain, cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(sK2512,sK2516), inference(instantiation, [status(thm)], [9426])).
% 7.62/1.58 cnf(l51, plain, cPLF_2eReferences_2eSTLCRef_2etm___24t(sK2514), inference(instantiation, [status(thm)], [9421])).
% 7.62/1.58 cnf(7534, plain, ~cPLF_2eReferences_2eSTLCRef_2estore___24t(X0) | ~cPLF_2eReferences_2eSTLCRef_2estore___24t(X1) | ~cPLF_2eReferences_2eSTLCRef_2etm___24t(X2) | ~cPLF_2eReferences_2eSTLCRef_2etm___24t(X3) | ~cPLF_2eReferences_2eSTLCRef_2ety___24t(X4) | ~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety),X5,X2,X4) | ~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(X5,X0) | ~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,X2,X0),cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,X3,X1)) | ~cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(X5) | cPLF_2eReferences_2eSTLCRef_2eextends___24a2(sK2507(X5,X2,X3,X4,X0,X1),X5), inference(cnf, [status(esa)], ['UseAuto.PreservationProgressReferences.preservation'])).
% 7.62/1.58 cnf(l41, plain, ~cPLF_2eReferences_2eSTLCRef_2estore___24t(sK2516) | ~cPLF_2eReferences_2eSTLCRef_2estore___24t(sK2517) | ~cPLF_2eReferences_2eSTLCRef_2etm___24t(sK2513) | ~cPLF_2eReferences_2eSTLCRef_2etm___24t(sK2514) | ~cPLF_2eReferences_2eSTLCRef_2ety___24t(sK2515) | ~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety),sK2512,sK2513,sK2515) | ~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(sK2512,sK2516) | ~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,sK2513,sK2516),cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,sK2514,sK2517)) | ~cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(sK2512) | cPLF_2eReferences_2eSTLCRef_2eextends___24a2(sK2507(sK2512,sK2513,sK2514,sK2515,sK2516,sK2517),sK2512), inference(instantiation, [status(thm)], [7534])).
% 7.62/1.58 cnf(l63, plain, cPLF_2eReferences_2eSTLCRef_2estore___24t(sK2517), inference(instantiation, [status(thm)], [9424])).
% 7.62/1.58 cnf(l47, plain, cPLF_2eReferences_2eSTLCRef_2etm___24t(sK2513), inference(instantiation, [status(thm)], [9420])).
% 7.62/1.58 cnf(l66, plain, cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(sK2512), inference(instantiation, [status(thm)], [9419])).
% 7.62/1.58 cnf(l6, plain, cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,sK2513,sK2516),cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,sK2514,sK2517)), inference(instantiation, [status(thm)], [9427])).
% 7.62/1.58 cnf(l61, plain, cPLF_2eReferences_2eSTLCRef_2etm___24t(sK2514), inference(instantiation, [status(thm)], [9421])).
% 7.62/1.58 cnf(l64, plain, cPLF_2eReferences_2eSTLCRef_2ety___24t(sK2515), inference(instantiation, [status(thm)], [9422])).
% 7.62/1.58 cnf(9423, plain, cPLF_2eReferences_2eSTLCRef_2estore___24t(sK2516), inference(cnf, [status(esa)], ['_HAMMER_GOAL'_negated])).
% 7.62/1.58 cnf(l44, plain, cPLF_2eReferences_2eSTLCRef_2estore___24t(sK2516), inference(instantiation, [status(thm)], [9423])).
% 7.62/1.58 cnf(l53, plain, cPLF_2eReferences_2eSTLCRef_2estore___24t(sK2516), inference(instantiation, [status(thm)], [9423])).
% 7.62/1.58 cnf(7533, plain, ~cPLF_2eReferences_2eSTLCRef_2estore___24t(X0) | ~cPLF_2eReferences_2eSTLCRef_2estore___24t(X1) | ~cPLF_2eReferences_2eSTLCRef_2etm___24t(X2) | ~cPLF_2eReferences_2eSTLCRef_2etm___24t(X3) | ~cPLF_2eReferences_2eSTLCRef_2ety___24t(X4) | ~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety),X5,X2,X4) | ~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(X5,X0) | ~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,X2,X0),cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,X3,X1)) | ~cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(X5) | cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(sK2507(X5,X2,X3,X4,X0,X1)), inference(cnf, [status(esa)], ['UseAuto.PreservationProgressReferences.preservation'])).
% 7.62/1.58 cnf(l46, plain, ~cPLF_2eReferences_2eSTLCRef_2estore___24t(sK2516) | ~cPLF_2eReferences_2eSTLCRef_2estore___24t(sK2517) | ~cPLF_2eReferences_2eSTLCRef_2etm___24t(sK2513) | ~cPLF_2eReferences_2eSTLCRef_2etm___24t(sK2514) | ~cPLF_2eReferences_2eSTLCRef_2ety___24t(sK2515) | ~cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety),sK2512,sK2513,sK2515) | ~cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(sK2512,sK2516) | ~cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,sK2513,sK2516),cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,sK2514,sK2517)) | ~cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(sK2512) | cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(sK2507(sK2512,sK2513,sK2514,sK2515,sK2516,sK2517)), inference(instantiation, [status(thm)], [7533])).
% 7.62/1.58 cnf(l52, plain, cPLF_2eReferences_2eSTLCRef_2ety___24t(sK2515), inference(instantiation, [status(thm)], [9422])).
% 7.62/1.58 cnf(l70, plain, cPLF_2eReferences_2eSTLCRef_2etm___24t(sK2513), inference(instantiation, [status(thm)], [9420])).
% 7.62/1.58 cnf(l65, plain, cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,sK2513,sK2516),cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,sK2514,sK2517)), inference(instantiation, [status(thm)], [9427])).
% 7.62/1.58 cnf(l56, plain, cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(sK2512,sK2516), inference(instantiation, [status(thm)], [9426])).
% 7.62/1.58 cnf(l69, plain, cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(sK2512), inference(instantiation, [status(thm)], [9419])).
% 7.62/1.58 cnf(l60, plain, cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(sK2512,sK2516), inference(instantiation, [status(thm)], [9426])).
% 7.62/1.58 cnf(l49, plain, cPLF_2eReferences_2eSTLCRef_2estore__ty___24t(sK2512), inference(instantiation, [status(thm)], [9419])).
% 7.62/1.58 cnf(l54, plain, cPLF_2eReferences_2eSTLCRef_2estep___24a2(cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,sK2513,sK2516),cCoq_2eInit_2eDatatypes_2epair___24a4(cPLF_2eReferences_2eSTLCRef_2etm,cPLF_2eReferences_2eSTLCRef_2estore,sK2514,sK2517)), inference(instantiation, [status(thm)], [9427])).
% 7.62/1.58 cnf(l62, plain, cPLF_2eReferences_2eSTLCRef_2etm___24t(sK2513), inference(instantiation, [status(thm)], [9420])).
% 7.62/1.58 cnf(l57, plain, cPLF_2eReferences_2eSTLCRef_2etm___24t(sK2514), inference(instantiation, [status(thm)], [9421])).
% 7.62/1.58 cnf(l7, plain, cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(sK2512,sK2516), inference(instantiation, [status(thm)], [9426])).
% 7.62/1.58 cnf(l50, plain, cPLF_2eReferences_2eSTLCRef_2estore___24t(sK2516), inference(instantiation, [status(thm)], [9423])).
% 7.62/1.58 cnf(l55, plain, cPLF_2eReferences_2eSTLCRef_2estore___24t(sK2517), inference(instantiation, [status(thm)], [9424])).
% 7.62/1.58 cnf(l48, plain, cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety),sK2512,sK2513,sK2515), inference(instantiation, [status(thm)], [9425])).
% 7.62/1.58 cnf(l5, plain, cPLF_2eReferences_2eSTLCRef_2estore___24t(sK2516), inference(instantiation, [status(thm)], [9423])).
% 7.62/1.58 cnf(l68, plain, cPLF_2eReferences_2eSTLCRef_2ety___24t(sK2515), inference(instantiation, [status(thm)], [9422])).
% 7.62/1.58 cnf(l67, plain, cPLF_2eReferences_2eSTLCRef_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety),sK2512,sK2513,sK2515), inference(instantiation, [status(thm)], [9425])).
% 7.62/1.58 cnf(l43, plain, cPLF_2eReferences_2eSTLCRef_2estore___24t(sK2517), inference(instantiation, [status(thm)], [9424])).
% 7.62/1.58 cnf(final, plain, $false, inference(ground_refutation, [status(thm)], [l0, l39, l1, l8, l45, l42, l13, l2, l9, l3, l4, l40, l51, l41, l63, l47, l66, l6, l61, l64, l44, l53, l46, l52, l70, l65, l56, l69, l60, l49, l54, l62, l57, l7, l50, l55, l48, l5, l68, l67, l43])).
% 7.62/1.58 % SZS output end CNFRefutation
%------------------------------------------------------------------------------