%------------------------------------------------------------------------------
% File : Enigma---0.5.1
% Problem : SEV655+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : enigmatic-eprover.py %s %d 1
% Computer : n002.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:51:38 PM UTC 2026
% Result : Theorem 207.02s 34.41s
% Output : CNFRefutation 207.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 11
% Syntax : Number of formulae : 54 ( 29 unt; 0 def)
% Number of atoms : 118 ( 77 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 103 ( 39 ~; 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 : 44 ( 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('$_discrim_Coq.Init.Datatypes.true$Coq.Init.Datatypes.false',axiom,
cCoq_2eInit_2eDatatypes_2etrue != cCoq_2eInit_2eDatatypes_2efalse,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','$_discrim_Coq.Init.Datatypes.true$Coq.Init.Datatypes.false') ).
fof(c_0_11,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_12,plain,
! [X12049] :
( ~ cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,X12049)
| cCoq_2eInit_2eDatatypes_2elength___24a2(cIntMap_2eMap_2ead,X12049) != cIntMap_2eMap_2eMapCard___24a2(cCoq_2eInit_2eDatatypes_2eunit,cMaplists_2eMapLists_2eElems___24a1(X12049))
| cMaplists_2eMapLists_2ead__list__stutters___24a1(X12049) = 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_13,plain,
! [X12560] : happ(cMaplists_2eMapLists_2eElems,X12560) = cMaplists_2eMapLists_2eElems___24a1(X12560),
inference(variable_rename,[status(thm)],['$adef_Maplists.MapLists.Elems_$a1']) ).
fof(c_0_14,plain,
! [X12218] : happ(cMaplists_2eMapLists_2ead__list__stutters,X12218) = cMaplists_2eMapLists_2ead__list__stutters___24a1(X12218),
inference(variable_rename,[status(thm)],['$adef_Maplists.MapLists.ad_list_stutters_$a1']) ).
fof(c_0_15,plain,
! [X14142,X14143] : happ(happ(cCoq_2eInit_2eDatatypes_2elength,X14142),X14143) = cCoq_2eInit_2eDatatypes_2elength___24a2(X14142,X14143),
inference(variable_rename,[status(thm)],['$adef_Coq.Init.Datatypes.length_$a2']) ).
fof(c_0_16,plain,
! [X13455,X13456] : happ(happ(cIntMap_2eMap_2eMapCard,X13455),X13456) = cIntMap_2eMap_2eMapCard___24a2(X13455,X13456),
inference(variable_rename,[status(thm)],['$adef_IntMap.Map.MapCard_$a2']) ).
fof(c_0_17,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_11])])]) ).
fof(c_0_18,plain,
! [X12048] :
( ~ cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,X12048)
| cMaplists_2eMapLists_2ead__list__stutters___24a1(X12048) != cCoq_2eInit_2eDatatypes_2efalse
| cCoq_2eInit_2eDatatypes_2elength___24a2(cIntMap_2eMap_2ead,X12048) = cIntMap_2eMap_2eMapCard___24a2(cCoq_2eInit_2eDatatypes_2eunit,cMaplists_2eMapLists_2eElems___24a1(X12048)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['Maplists.MapLists.ad_list_not_stutters_card'])]) ).
cnf(c_0_19,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_12]) ).
cnf(c_0_20,plain,
happ(cMaplists_2eMapLists_2eElems,X1) = cMaplists_2eMapLists_2eElems___24a1(X1),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
cnf(c_0_21,plain,
happ(cMaplists_2eMapLists_2ead__list__stutters,X1) = cMaplists_2eMapLists_2ead__list__stutters___24a1(X1),
inference(split_conjunct,[status(thm)],[c_0_14]) ).
cnf(c_0_22,plain,
happ(happ(cCoq_2eInit_2eDatatypes_2elength,X1),X2) = cCoq_2eInit_2eDatatypes_2elength___24a2(X1,X2),
inference(split_conjunct,[status(thm)],[c_0_15]) ).
cnf(c_0_23,plain,
happ(happ(cIntMap_2eMap_2eMapCard,X1),X2) = cIntMap_2eMap_2eMapCard___24a2(X1,X2),
inference(split_conjunct,[status(thm)],[c_0_16]) ).
cnf(c_0_24,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_17]) ).
cnf(c_0_25,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_17]) ).
cnf(c_0_26,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_18]) ).
fof(c_0_27,plain,
! [X10009,X10010,X10011] :
( ( ~ c_24__type__785___24t(X10009)
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,X10010)
| cCoq_2eInit_2eDatatypes_2ebool___24t(happ(X10009,X10010)) )
& ( cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,esk1557_1(X10011))
| c_24__type__785___24t(X10011) )
& ( ~ cCoq_2eInit_2eDatatypes_2ebool___24t(happ(X10011,esk1557_1(X10011)))
| c_24__type__785___24t(X10011) ) ),
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_28,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_19,c_0_20]),c_0_21]),c_0_22]),c_0_23]) ).
cnf(c_0_29,negated_conjecture,
cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,esk1781_0),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_30,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_24,c_0_20]),c_0_20]),c_0_23]),c_0_23]) ).
cnf(c_0_31,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_25,c_0_22]),c_0_22]) ).
cnf(c_0_32,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_26,c_0_20]),c_0_21]),c_0_22]),c_0_23]) ).
cnf(c_0_33,negated_conjecture,
cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,esk1780_0),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
fof(c_0_34,plain,
! [X2487,X2488] :
( ( X2487 = cCoq_2eInit_2eDatatypes_2efalse
| X2487 = cCoq_2eInit_2eDatatypes_2etrue
| ~ cCoq_2eInit_2eDatatypes_2ebool___24t(X2487) )
& ( c_24__case__Coq_2eInit_2eDatatypes_2ebool_2454376___24a2(X2487,X2488) = cCoq_2eInit_2eDatatypes_2efalse
| X2487 = cCoq_2eInit_2eDatatypes_2etrue
| ~ cCoq_2eInit_2eDatatypes_2ebool___24t(X2487) )
& ( X2487 = cCoq_2eInit_2eDatatypes_2efalse
| c_24__case__Coq_2eInit_2eDatatypes_2ebool_2454376___24a2(X2487,X2488) = X2488
| ~ cCoq_2eInit_2eDatatypes_2ebool___24t(X2487) )
& ( c_24__case__Coq_2eInit_2eDatatypes_2ebool_2454376___24a2(X2487,X2488) = cCoq_2eInit_2eDatatypes_2efalse
| c_24__case__Coq_2eInit_2eDatatypes_2ebool_2454376___24a2(X2487,X2488) = X2488
| ~ cCoq_2eInit_2eDatatypes_2ebool___24t(X2487) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],['$_case_Coq.Init.Datatypes.bool$54376'])])]) ).
cnf(c_0_35,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_27]) ).
cnf(c_0_36,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_37,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_17]) ).
cnf(c_0_38,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(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28,c_0_29]),c_0_30]),c_0_31]) ).
cnf(c_0_39,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,esk1780_0) != cCoq_2eInit_2eDatatypes_2efalse ),
inference(spm,[status(thm)],[c_0_32,c_0_33]) ).
cnf(c_0_40,plain,
( X1 = cCoq_2eInit_2eDatatypes_2efalse
| X1 = cCoq_2eInit_2eDatatypes_2etrue
| ~ cCoq_2eInit_2eDatatypes_2ebool___24t(X1) ),
inference(split_conjunct,[status(thm)],[c_0_34]) ).
cnf(c_0_41,plain,
( cCoq_2eInit_2eDatatypes_2ebool___24t(happ(cMaplists_2eMapLists_2ead__list__stutters,X1))
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,X1) ),
inference(spm,[status(thm)],[c_0_35,c_0_36]) ).
cnf(c_0_42,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_37,c_0_21]),c_0_21]) ).
cnf(c_0_43,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(spm,[status(thm)],[c_0_38,c_0_39]) ).
cnf(c_0_44,negated_conjecture,
( happ(cMaplists_2eMapLists_2ead__list__stutters,esk1780_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(spm,[status(thm)],[c_0_28,c_0_33]) ).
cnf(c_0_45,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(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32,c_0_29]),c_0_30]),c_0_31]) ).
cnf(c_0_46,plain,
( happ(cMaplists_2eMapLists_2ead__list__stutters,X1) = cCoq_2eInit_2eDatatypes_2efalse
| happ(cMaplists_2eMapLists_2ead__list__stutters,X1) = cCoq_2eInit_2eDatatypes_2etrue
| ~ cCoq_2eInit_2eDatatypes_2elist___24t(cIntMap_2eMap_2ead,X1) ),
inference(spm,[status(thm)],[c_0_40,c_0_41]) ).
cnf(c_0_47,negated_conjecture,
happ(cMaplists_2eMapLists_2ead__list__stutters,esk1780_0) != cCoq_2eInit_2eDatatypes_2efalse,
inference(spm,[status(thm)],[c_0_42,c_0_43]) ).
cnf(c_0_48,negated_conjecture,
( happ(cMaplists_2eMapLists_2ead__list__stutters,esk1780_0) = cCoq_2eInit_2eDatatypes_2efalse
| happ(cMaplists_2eMapLists_2ead__list__stutters,esk1781_0) != cCoq_2eInit_2eDatatypes_2efalse ),
inference(spm,[status(thm)],[c_0_44,c_0_45]) ).
cnf(c_0_49,negated_conjecture,
happ(cMaplists_2eMapLists_2ead__list__stutters,esk1780_0) = cCoq_2eInit_2eDatatypes_2etrue,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_46,c_0_33]),c_0_47]) ).
cnf(c_0_50,plain,
cCoq_2eInit_2eDatatypes_2etrue != cCoq_2eInit_2eDatatypes_2efalse,
inference(split_conjunct,[status(thm)],['$_discrim_Coq.Init.Datatypes.true$Coq.Init.Datatypes.false']) ).
cnf(c_0_51,negated_conjecture,
happ(cMaplists_2eMapLists_2ead__list__stutters,esk1781_0) != cCoq_2eInit_2eDatatypes_2efalse,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_48,c_0_49]),c_0_50]) ).
cnf(c_0_52,negated_conjecture,
happ(cMaplists_2eMapLists_2ead__list__stutters,esk1781_0) != cCoq_2eInit_2eDatatypes_2etrue,
inference(rw,[status(thm)],[c_0_42,c_0_49]) ).
cnf(c_0_53,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_46,c_0_29]),c_0_51]),c_0_52]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SEV655+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : enigmatic-eprover.py %s %d 1
% 0.16/0.33 % Computer : n002.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 07:30:48 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.29/0.47 # ENIGMATIC: Selected SinE mode:
% 0.46/0.63 # Parsing /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.46/0.63 # Filter: axfilter_auto 0 goes into file theBenchmark_axfilter_auto 0.p
% 0.46/0.63 # Filter: axfilter_auto 1 goes into file theBenchmark_axfilter_auto 1.p
% 0.46/0.63 # Filter: axfilter_auto 2 goes into file theBenchmark_axfilter_auto 2.p
% 207.02/34.41 # ENIGMATIC: Solved by autoschedule:
% 207.02/34.41 # No SInE strategy applied
% 207.02/34.41 # Trying AutoSched0 for 146 seconds
% 207.02/34.41 # AutoSched0-Mode selected heuristic SAT001_MinMin_x000000_rr
% 207.02/34.41 # and selection function SelectMaxLComplexAvoidPosPred.
% 207.02/34.41 #
% 207.02/34.41 # Preprocessing time : 10.486 s
% 207.02/34.41 # Presaturation interreduction done
% 207.02/34.41
% 207.02/34.41 # Proof found!
% 207.02/34.41 # SZS status Theorem
% 207.02/34.41 # SZS output start CNFRefutation
% See solution above
% 207.02/34.41 # Training examples: 0 positive, 0 negative
% 207.02/34.41
% 207.02/34.41 # -------------------------------------------------
% 207.02/34.41 # User time : 23.673 s
% 207.02/34.41 # System time : 0.131 s
% 207.02/34.41 # Total time : 23.805 s
% 207.02/34.41 # Maximum resident set size: 9968 pages
% 207.02/34.41
%------------------------------------------------------------------------------