%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SEV631+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n010.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:53:12 PM UTC 2026
% Result : Theorem 154.71s 151.78s
% Output : Proof 154.71s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEV631+1 : TPTP v9.3.0. Released v9.3.0.
% 0.13/0.13 % Command : leancop_casc.sh %s %d
% 0.17/0.35 % Computer : n010.cluster.edu
% 0.17/0.35 % Model : x86_64 x86_64
% 0.17/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.35 % Memory : 8042.1875MB
% 0.17/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.35 % CPULimit : 300
% 0.17/0.35 % WCLimit : 300
% 0.17/0.35 % DateTime : Tue May 5 06:26:36 EDT 2026
% 0.17/0.35 % CPUTime :
% 99.18/95.55 *** Overflow of the global/trail stack in spite of garbage collection!
% 99.18/95.55 You can use the "-g kBytes" (GLOBALSIZE) option to have a larger stack.
% 99.18/95.55 Peak sizes were: global stack 130976 kbytes, trail stack 4192 kbytes
% 127.45/123.01 *** Overflow of the global/trail stack in spite of garbage collection!
% 127.45/123.01 You can use the "-g kBytes" (GLOBALSIZE) option to have a larger stack.
% 127.45/123.01 Peak sizes were: global stack 130976 kbytes, trail stack 4192 kbytes
% 154.71/151.78 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 154.71/151.78 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 154.71/151.79
% 154.71/151.79 %-----------------------------------------------------
% 154.71/151.79 fof('$_inj_HList.hlist.Hcons', axiom, ! [_952475, _952478, _952481, _952484, _952487, _952490, _952493, _952496] : (cHList_2ehlist_2eHcons___24a4(_952475, _952481, _952487, _952493) = cHList_2ehlist_2eHcons___24a4(_952478, _952484, _952490, _952496) => _952493 = _952496 & _952487 = _952490 & _952481 = _952484 & _952475 = _952478), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', '$_inj_HList.hlist.Hcons')).
% 154.71/151.79 fof('_HAMMER_GOAL', conjecture, ! [_955289] : (ciT___24t(_955289) => ! [_955304] : (cCoq_2eInit_2eDatatypes_2elist___24t(ciT, _955304) => ! [_955322] : (cF___24t(_955289, _955322) => ! [_955340] : (cHList_2ehlist_2ehlist___24t(_955304, _955340) => ! [_955358] : (cF___24t(_955289, _955358) => ! [_955376] : (cHList_2ehlist_2ehlist___24t(_955304, _955376) => cHList_2ehlist_2eHcons___24a4(_955289, _955304, _955322, _955340) = cHList_2ehlist_2eHcons___24a4(_955289, _955304, _955358, _955376) => _955322 = _955358 & _955340 = _955376)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', '_HAMMER_GOAL')).
% 154.71/151.79
% 154.71/151.79 cnf(1, plain, [-(1498 ^ [_401143, _401142, _401141, _401140, _401139, _401138, _401137, _401136]), -(_401140 = _401141)], clausify('$_inj_HList.hlist.Hcons')).
% 154.71/151.79 cnf(2, plain, [-(1498 ^ [_401143, _401142, _401141, _401140, _401139, _401138, _401137, _401136]), -(_401142 = _401143)], clausify('$_inj_HList.hlist.Hcons')).
% 154.71/151.79 cnf(3, plain, [-(cHList_2ehlist_2eHcons___24a4(3919 ^ [], 3920 ^ [], 3921 ^ [], 3922 ^ []) = cHList_2ehlist_2eHcons___24a4(3919 ^ [], 3920 ^ [], 3923 ^ [], 3924 ^ []))], clausify('_HAMMER_GOAL')).
% 154.71/151.79 cnf(4, plain, [3921 ^ [] = 3923 ^ [], 3922 ^ [] = 3924 ^ []], clausify('_HAMMER_GOAL')).
% 154.71/151.79 cnf(5, plain, [cHList_2ehlist_2eHcons___24a4(_401136, _401138, _401140, _401142) = cHList_2ehlist_2eHcons___24a4(_401137, _401139, _401141, _401143), 1498 ^ [_401143, _401142, _401141, _401140, _401139, _401138, _401137, _401136]], clausify('$_inj_HList.hlist.Hcons')).
% 154.71/151.79
% 154.71/151.79 cnf('1',plain,[3921 ^ [] = 3923 ^ [], 3922 ^ [] = 3924 ^ []],start(4)).
% 154.71/151.79 cnf('1.1',plain,[-(3921 ^ [] = 3923 ^ []), -(1498 ^ [3924 ^ [], 3922 ^ [], 3923 ^ [], 3921 ^ [], 3920 ^ [], 3920 ^ [], 3919 ^ [], 3919 ^ []])],extension(1,bind([[_401143, _401142, _401141, _401140, _401139, _401138, _401137, _401136], [3924 ^ [], 3922 ^ [], 3923 ^ [], 3921 ^ [], 3920 ^ [], 3920 ^ [], 3919 ^ [], 3919 ^ []]]))).
% 154.71/151.79 cnf('1.1.1',plain,[1498 ^ [3924 ^ [], 3922 ^ [], 3923 ^ [], 3921 ^ [], 3920 ^ [], 3920 ^ [], 3919 ^ [], 3919 ^ []], cHList_2ehlist_2eHcons___24a4(3919 ^ [], 3920 ^ [], 3921 ^ [], 3922 ^ []) = cHList_2ehlist_2eHcons___24a4(3919 ^ [], 3920 ^ [], 3923 ^ [], 3924 ^ [])],extension(5,bind([[_401136, _401138, _401140, _401142, _401137, _401139, _401141, _401143], [3919 ^ [], 3920 ^ [], 3921 ^ [], 3922 ^ [], 3919 ^ [], 3920 ^ [], 3923 ^ [], 3924 ^ []]]))).
% 154.71/151.79 cnf('1.1.1.1',plain,[-(cHList_2ehlist_2eHcons___24a4(3919 ^ [], 3920 ^ [], 3921 ^ [], 3922 ^ []) = cHList_2ehlist_2eHcons___24a4(3919 ^ [], 3920 ^ [], 3923 ^ [], 3924 ^ []))],extension(3)).
% 154.71/151.79 cnf('1.2',plain,[-(3922 ^ [] = 3924 ^ []), -(1498 ^ [3924 ^ [], 3922 ^ [], 3923 ^ [], 3921 ^ [], 3920 ^ [], 3920 ^ [], 3919 ^ [], 3919 ^ []])],extension(2,bind([[_401143, _401142, _401141, _401140, _401139, _401138, _401137, _401136], [3924 ^ [], 3922 ^ [], 3923 ^ [], 3921 ^ [], 3920 ^ [], 3920 ^ [], 3919 ^ [], 3919 ^ []]]))).
% 154.71/151.79 cnf('1.2.1',plain,[1498 ^ [3924 ^ [], 3922 ^ [], 3923 ^ [], 3921 ^ [], 3920 ^ [], 3920 ^ [], 3919 ^ [], 3919 ^ []], cHList_2ehlist_2eHcons___24a4(3919 ^ [], 3920 ^ [], 3921 ^ [], 3922 ^ []) = cHList_2ehlist_2eHcons___24a4(3919 ^ [], 3920 ^ [], 3923 ^ [], 3924 ^ [])],extension(5,bind([[_401136, _401138, _401140, _401142, _401137, _401139, _401141, _401143], [3919 ^ [], 3920 ^ [], 3921 ^ [], 3922 ^ [], 3919 ^ [], 3920 ^ [], 3923 ^ [], 3924 ^ []]]))).
% 154.71/151.79 cnf('1.2.1.1',plain,[-(cHList_2ehlist_2eHcons___24a4(3919 ^ [], 3920 ^ [], 3921 ^ [], 3922 ^ []) = cHList_2ehlist_2eHcons___24a4(3919 ^ [], 3920 ^ [], 3923 ^ [], 3924 ^ []))],extension(3)).
% 154.71/151.79 %-----------------------------------------------------
% 154.71/151.79
% 154.71/151.79 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------