%------------------------------------------------------------------------------
% File : Metis---2.4
% Problem : SEV679+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : metis --show proof --show saturation %s
% Computer : n013.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:54:15 PM UTC 2026
% Result : Theorem 84.52s 84.77s
% Output : CNFRefutation 84.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 4
% Syntax : Number of formulae : 12 ( 3 unt; 0 def)
% Number of atoms : 122 ( 0 equ)
% Maximal formula atoms : 14 ( 10 avg)
% Number of connectives : 129 ( 19 ~; 15 |; 45 &)
% ( 2 <=>; 48 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 15 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 10 ( 9 usr; 1 prp; 0-4 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-4 aty)
% Number of variables : 63 ( 0 sgn 44 !; 19 ?)
% Comments :
%------------------------------------------------------------------------------
fof('$_def_PLF.References.STLCRef.preservation_theorem',axiom,
( p(cPLF_2eReferences_2eSTLCRef_2epreservation__theorem)
<=> ! [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) ) ) ) ) ) ) ) ) ) ) ) ).
fof('PLF.References.STLCRef.preservation',axiom,
! [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) ) ) ) ) ) ) ) ) ) ) ).
fof('UseAuto.PreservationProgressReferences.preservation',axiom,
! [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) ) ) ) ) ) ) ) ) ) ) ).
fof('_HAMMER_GOAL',conjecture,
! [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) ) ) ) ) ) ) ) ) ) ) ).
fof(subgoal_0,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(strip,[],['_HAMMER_GOAL']) ).
fof(negate_0_0,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,[],[subgoal_0]) ).
fof(normalize_0_0,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_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety),V0__ST,V1__t,V3__T)
& 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))
& cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)
& cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST,V4__st)
& ! [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__ty___24t(V9__ST_27)
| ~ cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27,V5__st_27) ) ) ) ) ) ) ),
inference(canonicalize,[],[negate_0_0]) ).
fof(normalize_0_1,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_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety),V0__ST,V1__t,V3__T)
| ~ 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))
| ~ cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)
| ~ cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST,V4__st)
| ? [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__ty___24t(V9__ST_27)
& cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27,V5__st_27) ) ) ) ) ) ) ),
inference(canonicalize,[],['UseAuto.PreservationProgressReferences.preservation']) ).
fof(normalize_0_2,plain,
( ~ p(cPLF_2eReferences_2eSTLCRef_2epreservation__theorem)
<=> ? [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_2ehas__type___24a4(cPLF_2eMaps_2eempty___24a1(cPLF_2eReferences_2eSTLCRef_2ety),V0__ST,V1__t,V3__T)
& 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))
& cPLF_2eReferences_2eSTLCRef_2estore___24t(V5__st_27)
& cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V0__ST,V4__st)
& ! [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__ty___24t(V9__ST_27)
| ~ cPLF_2eReferences_2eSTLCRef_2estore__well__typed___24a2(V9__ST_27,V5__st_27) ) ) ) ) ) ) ) ),
inference(canonicalize,[],['$_def_PLF.References.STLCRef.preservation_theorem']) ).
fof(normalize_0_3,plain,
p(cPLF_2eReferences_2eSTLCRef_2epreservation__theorem),
inference(simplify,[],[normalize_0_1,normalize_0_2]) ).
fof(normalize_0_4,plain,
$false,
inference(simplify,[],[normalize_0_0,normalize_0_3,normalize_0_2]) ).
cnf(refute_0_0,plain,
$false,
inference(canonicalize,[],[normalize_0_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEV679+1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : metis --show proof --show saturation %s
% 0.16/0.33 % Computer : n013.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 08:26:10 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 84.52/84.77 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 84.52/84.77
% 84.52/84.77 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 84.52/84.78
%------------------------------------------------------------------------------