%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SEV655+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n015.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 05:15:54 PM UTC 2026
% Result : Theorem 46.00s 27.90s
% Output : CNFRefutation 46.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 10
% Syntax : Number of formulae : 50 ( 26 unt; 0 def)
% Number of atoms : 114 ( 70 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 100 ( 36 ~; 38 |; 11 &)
% ( 1 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 10 con; 0-2 aty)
% Number of variables : 46 ( 0 sgn 29 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof('_HAMMER_GOAL',conjecture,
! [X2451] :
( cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,X2451)
=> ! [X2452] :
( cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,X2452)
=> ( cIntMap_2eMap_2eMapCard___24a2(cCoq_2eInit_2eDatatypes_2eunit,cMaplists_2eMapLists_2eElems___24a1(X2451)) = cIntMap_2eMap_2eMapCard___24a2(cCoq_2eInit_2eDatatypes_2eunit,cMaplists_2eMapLists_2eElems___24a1(X2452))
=> ( cCoq_2eInit_2eDatatypes_2elength___24a2(cIntMap_2eMap_2ead,X2451) = cCoq_2eInit_2eDatatypes_2elength___24a2(cIntMap_2eMap_2ead,X2452)
=> cMaplists_2eMapLists_2ead__list__stutters___24a1(X2451) = cMaplists_2eMapLists_2ead__list__stutters___24a1(X2452) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','_HAMMER_GOAL') ).
fof('Maplists.MapLists.ad_list_not_stutters_card_conv',axiom,
! [X2451] :
( cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,X2451)
=> ( cCoq_2eInit_2eDatatypes_2elength___24a2(cIntMap_2eMap_2ead,X2451) = cIntMap_2eMap_2eMapCard___24a2(cCoq_2eInit_2eDatatypes_2eunit,cMaplists_2eMapLists_2eElems___24a1(X2451))
=> cMaplists_2eMapLists_2ead__list__stutters___24a1(X2451) = cCoq_2eInit_2eDatatypes_2efalse ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Maplists.MapLists.ad_list_not_stutters_card_conv') ).
fof('$adef_Maplists.MapLists.Elems_$a1',axiom,
! [X2456] : happ(cMaplists_2eMapLists_2eElems,X2456) = cMaplists_2eMapLists_2eElems___24a1(X2456),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','$adef_Maplists.MapLists.Elems_$a1') ).
fof('$adef_Maplists.MapLists.ad_list_stutters_$a1',axiom,
! [X2456] : happ(cMaplists_2eMapLists_2ead__list__stutters,X2456) = cMaplists_2eMapLists_2ead__list__stutters___24a1(X2456),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','$adef_Maplists.MapLists.ad_list_stutters_$a1') ).
fof('$adef_Coq.Init.Datatypes.length_$a2',axiom,
! [X2456,X2457] : happ(happ(cCoq_2eInit_2eDatatypes_2elength,X2456),X2457) = cCoq_2eInit_2eDatatypes_2elength___24a2(X2456,X2457),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','$adef_Coq.Init.Datatypes.length_$a2') ).
fof('$adef_IntMap.Map.MapCard_$a2',axiom,
! [X2456,X2457] : happ(happ(cIntMap_2eMap_2eMapCard,X2456),X2457) = cIntMap_2eMap_2eMapCard___24a2(X2456,X2457),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','$adef_IntMap.Map.MapCard_$a2') ).
fof('Maplists.MapLists.ad_list_not_stutters_card',axiom,
! [X2451] :
( cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,X2451)
=> ( cMaplists_2eMapLists_2ead__list__stutters___24a1(X2451) = cCoq_2eInit_2eDatatypes_2efalse
=> cCoq_2eInit_2eDatatypes_2elength___24a2(cIntMap_2eMap_2ead,X2451) = cIntMap_2eMap_2eMapCard___24a2(cCoq_2eInit_2eDatatypes_2eunit,cMaplists_2eMapLists_2eElems___24a1(X2451)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Maplists.MapLists.ad_list_not_stutters_card') ).
fof('$_type_785',axiom,
! [X2277] :
( c_24__type__785___24t(X2277)
<=> ! [X1] :
( cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,X1)
=> cCoq_2eInit_2eDatatypes_2ebool___24t(happ(X2277,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','$_type_785') ).
fof('$_case_Coq.Init.Datatypes.bool$54376',axiom,
! [X1,X2] :
( cCoq_2eInit_2eDatatypes_2ebool___24t(X1)
=> ( ( X1 = cCoq_2eInit_2eDatatypes_2etrue
& c_24__case__Coq_2eInit_2eDatatypes_2ebool_2454376___24a2(X1,X2) = X2 )
| ( X1 = cCoq_2eInit_2eDatatypes_2efalse
& c_24__case__Coq_2eInit_2eDatatypes_2ebool_2454376___24a2(X1,X2) = cCoq_2eInit_2eDatatypes_2efalse ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','$_case_Coq.Init.Datatypes.bool$54376') ).
fof('$_typeof_Maplists.MapLists.ad_list_stutters',axiom,
c_24__type__785___24t(cMaplists_2eMapLists_2ead__list__stutters),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','$_typeof_Maplists.MapLists.ad_list_stutters') ).
fof(c_0_10,negated_conjecture,
~ ! [X2451] :
( cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,X2451)
=> ! [X2452] :
( cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,X2452)
=> ( cIntMap_2eMap_2eMapCard___24a2(cCoq_2eInit_2eDatatypes_2eunit,cMaplists_2eMapLists_2eElems___24a1(X2451)) = cIntMap_2eMap_2eMapCard___24a2(cCoq_2eInit_2eDatatypes_2eunit,cMaplists_2eMapLists_2eElems___24a1(X2452))
=> ( cCoq_2eInit_2eDatatypes_2elength___24a2(cIntMap_2eMap_2ead,X2451) = cCoq_2eInit_2eDatatypes_2elength___24a2(cIntMap_2eMap_2ead,X2452)
=> cMaplists_2eMapLists_2ead__list__stutters___24a1(X2451) = cMaplists_2eMapLists_2ead__list__stutters___24a1(X2452) ) ) ) ),
inference(assume_negation,[status(cth)],['_HAMMER_GOAL']) ).
fof(c_0_11,plain,
! [X22956] :
( ~ cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,X22956)
| cCoq_2eInit_2eDatatypes_2elength___24a2(cIntMap_2eMap_2ead,X22956) != cIntMap_2eMap_2eMapCard___24a2(cCoq_2eInit_2eDatatypes_2eunit,cMaplists_2eMapLists_2eElems___24a1(X22956))
| cMaplists_2eMapLists_2ead__list__stutters___24a1(X22956) = cCoq_2eInit_2eDatatypes_2efalse ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['Maplists.MapLists.ad_list_not_stutters_card_conv'])]) ).
fof(c_0_12,plain,
! [X23467] : happ(cMaplists_2eMapLists_2eElems,X23467) = cMaplists_2eMapLists_2eElems___24a1(X23467),
inference(variable_rename,[status(thm)],['$adef_Maplists.MapLists.Elems_$a1']) ).
fof(c_0_13,plain,
! [X23125] : happ(cMaplists_2eMapLists_2ead__list__stutters,X23125) = cMaplists_2eMapLists_2ead__list__stutters___24a1(X23125),
inference(variable_rename,[status(thm)],['$adef_Maplists.MapLists.ad_list_stutters_$a1']) ).
fof(c_0_14,plain,
! [X25049,X25050] : happ(happ(cCoq_2eInit_2eDatatypes_2elength,X25049),X25050) = cCoq_2eInit_2eDatatypes_2elength___24a2(X25049,X25050),
inference(variable_rename,[status(thm)],['$adef_Coq.Init.Datatypes.length_$a2']) ).
fof(c_0_15,plain,
! [X24362,X24363] : happ(happ(cIntMap_2eMap_2eMapCard,X24362),X24363) = cIntMap_2eMap_2eMapCard___24a2(X24362,X24363),
inference(variable_rename,[status(thm)],['$adef_IntMap.Map.MapCard_$a2']) ).
fof(c_0_16,negated_conjecture,
( cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,esk1780_0)
& cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,esk1781_0)
& cIntMap_2eMap_2eMapCard___24a2(cCoq_2eInit_2eDatatypes_2eunit,cMaplists_2eMapLists_2eElems___24a1(esk1780_0)) = cIntMap_2eMap_2eMapCard___24a2(cCoq_2eInit_2eDatatypes_2eunit,cMaplists_2eMapLists_2eElems___24a1(esk1781_0))
& cCoq_2eInit_2eDatatypes_2elength___24a2(cIntMap_2eMap_2ead,esk1780_0) = cCoq_2eInit_2eDatatypes_2elength___24a2(cIntMap_2eMap_2ead,esk1781_0)
& cMaplists_2eMapLists_2ead__list__stutters___24a1(esk1780_0) != cMaplists_2eMapLists_2ead__list__stutters___24a1(esk1781_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_10])])]) ).
cnf(c_0_17,plain,
( cMaplists_2eMapLists_2ead__list__stutters___24a1(X1) = cCoq_2eInit_2eDatatypes_2efalse
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,X1)
| cCoq_2eInit_2eDatatypes_2elength___24a2(cIntMap_2eMap_2ead,X1) != cIntMap_2eMap_2eMapCard___24a2(cCoq_2eInit_2eDatatypes_2eunit,cMaplists_2eMapLists_2eElems___24a1(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_11]) ).
cnf(c_0_18,plain,
happ(cMaplists_2eMapLists_2eElems,X1) = cMaplists_2eMapLists_2eElems___24a1(X1),
inference(split_conjunct,[status(thm)],[c_0_12]) ).
cnf(c_0_19,plain,
happ(cMaplists_2eMapLists_2ead__list__stutters,X1) = cMaplists_2eMapLists_2ead__list__stutters___24a1(X1),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
cnf(c_0_20,plain,
happ(happ(cCoq_2eInit_2eDatatypes_2elength,X1),X2) = cCoq_2eInit_2eDatatypes_2elength___24a2(X1,X2),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
cnf(c_0_21,plain,
happ(happ(cIntMap_2eMap_2eMapCard,X1),X2) = cIntMap_2eMap_2eMapCard___24a2(X1,X2),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
cnf(c_0_22,negated_conjecture,
cIntMap_2eMap_2eMapCard___24a2(cCoq_2eInit_2eDatatypes_2eunit,cMaplists_2eMapLists_2eElems___24a1(esk1780_0)) = cIntMap_2eMap_2eMapCard___24a2(cCoq_2eInit_2eDatatypes_2eunit,cMaplists_2eMapLists_2eElems___24a1(esk1781_0)),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
cnf(c_0_23,negated_conjecture,
cCoq_2eInit_2eDatatypes_2elength___24a2(cIntMap_2eMap_2ead,esk1780_0) = cCoq_2eInit_2eDatatypes_2elength___24a2(cIntMap_2eMap_2ead,esk1781_0),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
fof(c_0_24,plain,
! [X22955] :
( ~ cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,X22955)
| cMaplists_2eMapLists_2ead__list__stutters___24a1(X22955) != cCoq_2eInit_2eDatatypes_2efalse
| cCoq_2eInit_2eDatatypes_2elength___24a2(cIntMap_2eMap_2ead,X22955) = cIntMap_2eMap_2eMapCard___24a2(cCoq_2eInit_2eDatatypes_2eunit,cMaplists_2eMapLists_2eElems___24a1(X22955)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['Maplists.MapLists.ad_list_not_stutters_card'])]) ).
cnf(c_0_25,plain,
( happ(cMaplists_2eMapLists_2ead__list__stutters,X1) = cCoq_2eInit_2eDatatypes_2efalse
| happ(happ(cCoq_2eInit_2eDatatypes_2elength,cIntMap_2eMap_2ead),X1) != happ(happ(cIntMap_2eMap_2eMapCard,cCoq_2eInit_2eDatatypes_2eunit),happ(cMaplists_2eMapLists_2eElems,X1))
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,X1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_17,c_0_18]),c_0_19]),c_0_20]),c_0_21]) ).
cnf(c_0_26,negated_conjecture,
happ(happ(cIntMap_2eMap_2eMapCard,cCoq_2eInit_2eDatatypes_2eunit),happ(cMaplists_2eMapLists_2eElems,esk1781_0)) = happ(happ(cIntMap_2eMap_2eMapCard,cCoq_2eInit_2eDatatypes_2eunit),happ(cMaplists_2eMapLists_2eElems,esk1780_0)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_22,c_0_18]),c_0_18]),c_0_21]),c_0_21]) ).
cnf(c_0_27,negated_conjecture,
happ(happ(cCoq_2eInit_2eDatatypes_2elength,cIntMap_2eMap_2ead),esk1781_0) = happ(happ(cCoq_2eInit_2eDatatypes_2elength,cIntMap_2eMap_2ead),esk1780_0),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_23,c_0_20]),c_0_20]) ).
cnf(c_0_28,negated_conjecture,
cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,esk1781_0),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
cnf(c_0_29,plain,
( cCoq_2eInit_2eDatatypes_2elength___24a2(cIntMap_2eMap_2ead,X1) = cIntMap_2eMap_2eMapCard___24a2(cCoq_2eInit_2eDatatypes_2eunit,cMaplists_2eMapLists_2eElems___24a1(X1))
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,X1)
| cMaplists_2eMapLists_2ead__list__stutters___24a1(X1) != cCoq_2eInit_2eDatatypes_2efalse ),
inference(split_conjunct,[status(thm)],[c_0_24]) ).
fof(c_0_30,plain,
! [X20916,X20917,X20918] :
( ( ~ c_24__type__785___24t(X20916)
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,X20917)
| cCoq_2eInit_2eDatatypes_2ebool___24t(happ(X20916,X20917)) )
& ( cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,esk1557_1(X20918))
| c_24__type__785___24t(X20918) )
& ( ~ cCoq_2eInit_2eDatatypes_2ebool___24t(happ(X20918,esk1557_1(X20918)))
| c_24__type__785___24t(X20918) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],['$_type_785'])])])])])]) ).
cnf(c_0_31,negated_conjecture,
cMaplists_2eMapLists_2ead__list__stutters___24a1(esk1780_0) != cMaplists_2eMapLists_2ead__list__stutters___24a1(esk1781_0),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
cnf(c_0_32,negated_conjecture,
( happ(cMaplists_2eMapLists_2ead__list__stutters,esk1781_0) = cCoq_2eInit_2eDatatypes_2efalse
| happ(happ(cIntMap_2eMap_2eMapCard,cCoq_2eInit_2eDatatypes_2eunit),happ(cMaplists_2eMapLists_2eElems,esk1780_0)) != happ(happ(cCoq_2eInit_2eDatatypes_2elength,cIntMap_2eMap_2ead),esk1780_0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_25,c_0_26]),c_0_27]),c_0_28])]) ).
cnf(c_0_33,plain,
( happ(happ(cCoq_2eInit_2eDatatypes_2elength,cIntMap_2eMap_2ead),X1) = happ(happ(cIntMap_2eMap_2eMapCard,cCoq_2eInit_2eDatatypes_2eunit),happ(cMaplists_2eMapLists_2eElems,X1))
| happ(cMaplists_2eMapLists_2ead__list__stutters,X1) != cCoq_2eInit_2eDatatypes_2efalse
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,X1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_29,c_0_18]),c_0_19]),c_0_20]),c_0_21]) ).
cnf(c_0_34,negated_conjecture,
cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,esk1780_0),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
fof(c_0_35,plain,
! [X13394,X13395] :
( ( X13394 = cCoq_2eInit_2eDatatypes_2efalse
| X13394 = cCoq_2eInit_2eDatatypes_2etrue
| ~ cCoq_2eInit_2eDatatypes_2ebool___24t(X13394) )
& ( c_24__case__Coq_2eInit_2eDatatypes_2ebool_2454376___24a2(X13394,X13395) = cCoq_2eInit_2eDatatypes_2efalse
| X13394 = cCoq_2eInit_2eDatatypes_2etrue
| ~ cCoq_2eInit_2eDatatypes_2ebool___24t(X13394) )
& ( X13394 = cCoq_2eInit_2eDatatypes_2efalse
| c_24__case__Coq_2eInit_2eDatatypes_2ebool_2454376___24a2(X13394,X13395) = X13395
| ~ cCoq_2eInit_2eDatatypes_2ebool___24t(X13394) )
& ( c_24__case__Coq_2eInit_2eDatatypes_2ebool_2454376___24a2(X13394,X13395) = cCoq_2eInit_2eDatatypes_2efalse
| c_24__case__Coq_2eInit_2eDatatypes_2ebool_2454376___24a2(X13394,X13395) = X13395
| ~ cCoq_2eInit_2eDatatypes_2ebool___24t(X13394) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['$_case_Coq.Init.Datatypes.bool$54376'])])]) ).
cnf(c_0_36,plain,
( cCoq_2eInit_2eDatatypes_2ebool___24t(happ(X1,X2))
| ~ c_24__type__785___24t(X1)
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,X2) ),
inference(split_conjunct,[status(thm)],[c_0_30]) ).
cnf(c_0_37,negated_conjecture,
happ(cMaplists_2eMapLists_2ead__list__stutters,esk1781_0) != happ(cMaplists_2eMapLists_2ead__list__stutters,esk1780_0),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_31,c_0_19]),c_0_19]) ).
cnf(c_0_38,negated_conjecture,
( happ(cMaplists_2eMapLists_2ead__list__stutters,esk1781_0) = cCoq_2eInit_2eDatatypes_2efalse
| happ(cMaplists_2eMapLists_2ead__list__stutters,esk1780_0) != cCoq_2eInit_2eDatatypes_2efalse ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32,c_0_33]),c_0_34])]) ).
cnf(c_0_39,plain,
( X1 = cCoq_2eInit_2eDatatypes_2efalse
| X1 = cCoq_2eInit_2eDatatypes_2etrue
| ~ cCoq_2eInit_2eDatatypes_2ebool___24t(X1) ),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
cnf(c_0_40,negated_conjecture,
( cCoq_2eInit_2eDatatypes_2ebool___24t(happ(X1,esk1781_0))
| ~ c_24__type__785___24t(X1) ),
inference(spm,[status(thm)],[c_0_36,c_0_28]) ).
cnf(c_0_41,negated_conjecture,
( happ(happ(cIntMap_2eMap_2eMapCard,cCoq_2eInit_2eDatatypes_2eunit),happ(cMaplists_2eMapLists_2eElems,esk1780_0)) = happ(happ(cCoq_2eInit_2eDatatypes_2elength,cIntMap_2eMap_2ead),esk1780_0)
| happ(cMaplists_2eMapLists_2ead__list__stutters,esk1781_0) != cCoq_2eInit_2eDatatypes_2efalse ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_26,c_0_33]),c_0_27]),c_0_28])]) ).
cnf(c_0_42,negated_conjecture,
happ(cMaplists_2eMapLists_2ead__list__stutters,esk1780_0) != cCoq_2eInit_2eDatatypes_2efalse,
inference(spm,[status(thm)],[c_0_37,c_0_38]) ).
cnf(c_0_43,negated_conjecture,
( happ(X1,esk1781_0) = cCoq_2eInit_2eDatatypes_2efalse
| happ(X1,esk1781_0) = cCoq_2eInit_2eDatatypes_2etrue
| ~ c_24__type__785___24t(X1) ),
inference(spm,[status(thm)],[c_0_39,c_0_40]) ).
cnf(c_0_44,plain,
c_24__type__785___24t(cMaplists_2eMapLists_2ead__list__stutters),
inference(split_conjunct,[status(thm)],['$_typeof_Maplists.MapLists.ad_list_stutters']) ).
cnf(c_0_45,negated_conjecture,
happ(cMaplists_2eMapLists_2ead__list__stutters,esk1781_0) != cCoq_2eInit_2eDatatypes_2efalse,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_25,c_0_41]),c_0_34])]),c_0_42]) ).
cnf(c_0_46,negated_conjecture,
( cCoq_2eInit_2eDatatypes_2ebool___24t(happ(X1,esk1780_0))
| ~ c_24__type__785___24t(X1) ),
inference(spm,[status(thm)],[c_0_36,c_0_34]) ).
cnf(c_0_47,negated_conjecture,
happ(cMaplists_2eMapLists_2ead__list__stutters,esk1780_0) != cCoq_2eInit_2eDatatypes_2etrue,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37,c_0_43]),c_0_44])]),c_0_45]) ).
cnf(c_0_48,negated_conjecture,
( happ(X1,esk1780_0) = cCoq_2eInit_2eDatatypes_2efalse
| happ(X1,esk1780_0) = cCoq_2eInit_2eDatatypes_2etrue
| ~ c_24__type__785___24t(X1) ),
inference(spm,[status(thm)],[c_0_39,c_0_46]) ).
cnf(c_0_49,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_47,c_0_48]),c_0_44])]),c_0_42]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SEV655+1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.13/0.31 % Computer : n015.cluster.edu
% 0.13/0.31 % Model : x86_64 x86_64
% 0.13/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.31 % Memory : 8042.1875MB
% 0.13/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.31 % CPULimit : 300
% 0.13/0.31 % WCLimit : 300
% 0.13/0.31 % DateTime : Tue May 5 04:04:32 EDT 2026
% 0.13/0.32 % CPUTime :
% 0.13/0.33 % start to proof: theBenchmark
% 46.00/27.90 % Version : CSE_E---1.7
% 46.00/27.90 % Problem : theBenchmark.p
% 46.00/27.90 % SZS status Theorem for theBenchmark.p
% 46.00/27.90 % SZS output start CNFRefutation
% See solution above
% 46.00/27.94 % Total time : 25.640s
%------------------------------------------------------------------------------