%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SWX224+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n005.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 07:03:35 PM UTC 2026
% Result : Theorem 218.26s 210.83s
% Output : Proof 218.26s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX224+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : leancop_casc.sh %s %d
% 0.15/0.33 % Computer : n005.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 12:39:45 EDT 2026
% 0.15/0.34 % CPUTime :
% 218.26/210.83 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 218.26/210.84 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 218.26/210.85
% 218.26/210.85 %-----------------------------------------------------
% 218.26/210.85 fof(axiom_012, axiom, ! [_62690] : proj1Suc(suc(_62690)) = _62690, file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_012)).
% 218.26/210.85 fof(axiom_031, axiom, ! [_62828, _62831, _62834, _62837] : (index(_62828, _62834) = just(_62837) => (tc(_62828, var(_62834), _62831) <=> _62837 = _62831)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_031)).
% 218.26/210.85 fof(axiom_026, axiom, ! [_63058, _63061, _63064] : index(cons(_63058, _63061), suc(_63064)) = index(_63061, _63064), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_026)).
% 218.26/210.85 fof(goal_032, conjecture, ? [_63242] : tc(nil, _63242, arr(arr(a, arr(a, b)), arr(a, b))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', goal_032)).
% 218.26/210.85 fof(axiom_025, axiom, ! [_63420, _63423] : index(cons(_63420, _63423), zero) = just(_63420), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_025)).
% 218.26/210.85 fof(axiom_027, axiom, ! [_63588, _63591, _63594, _63597, _63600] : (tc(_63588, app(_63594, _63597, _63600), _63591) <=> tc(_63588, _63594, arr(_63600, _63591)) & tc(_63588, _63597, _63600)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_027)).
% 218.26/210.85 fof(axiom_029, axiom, ! [_63913, _63916, _63919, _63922] : (tc(_63913, lam(_63916), arr(_63919, _63922)) <=> tc(cons(_63919, _63913), _63916, _63922)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', axiom_029)).
% 218.26/210.85
% 218.26/210.85 cnf(1, plain, [-(proj1Suc(suc(_26328)) = _26328)], clausify(axiom_012)).
% 218.26/210.85 cnf(2, plain, [-(_13951 = _14062), _13951 = _14007, _14007 = _14062], theory(equality)).
% 218.26/210.85 cnf(3, plain, [index(_33676, _33813) = just(_33880), -(tc(_33676, var(_33813), _33745)), _33880 = _33745], clausify(axiom_031)).
% 218.26/210.85 cnf(4, plain, [-(index(cons(_30582, _30637), suc(_30691)) = index(_30637, _30691))], clausify(axiom_026)).
% 218.26/210.85 cnf(5, plain, [tc(nil, _34820, arr(arr(a, arr(a, b)), arr(a, b)))], clausify(goal_032)).
% 218.26/210.85 cnf(6, plain, [-(index(cons(_30252, _30299), zero) = just(_30252))], clausify(axiom_025)).
% 218.26/210.85 cnf(7, plain, [-(tc(_14502, _14669, _14832)), tc(_14417, _14586, _14751), _14417 = _14502, _14586 = _14669, _14751 = _14832], theory(equality)).
% 218.26/210.85 cnf(8, plain, [-(tc(_31025, app(_31176, _31250, _31323), _31101)), tc(_31025, _31176, arr(_31323, _31101)), tc(_31025, _31250, _31323)], clausify(axiom_027)).
% 218.26/210.85 cnf(9, plain, [_22950 = _22999, -(var(_22950) = var(_22999))], theory(equality)).
% 218.26/210.85 cnf(10, plain, [_13672 = _13717, -(_13717 = _13672)], theory(equality)).
% 218.26/210.85 cnf(11, plain, [-(_13519 = _13519)], theory(equality)).
% 218.26/210.85 cnf(12, plain, [-(tc(_32519, lam(_32584), arr(_32648, _32711))), tc(cons(_32648, _32519), _32584, _32711)], clausify(axiom_029)).
% 218.26/210.85 cnf(13, plain, [-(cons(_17106, _17239) = cons(_17173, _17304)), _17106 = _17173, _17239 = _17304], theory(equality)).
% 218.26/210.85
% 218.26/210.85 cnf('1',plain,[tc(nil, lam(lam(app(app(var(suc(zero)), var(zero), a), var(zero), a))), arr(arr(a, arr(a, b)), arr(a, b)))],start(5,bind([[_34820], [lam(lam(app(app(var(suc(zero)), var(zero), a), var(zero), a)))]]))).
% 218.26/210.85 cnf('1.1',plain,[-(tc(nil, lam(lam(app(app(var(suc(zero)), var(zero), a), var(zero), a))), arr(arr(a, arr(a, b)), arr(a, b)))), tc(cons(arr(a, arr(a, b)), nil), lam(app(app(var(suc(zero)), var(zero), a), var(zero), a)), arr(a, b))],extension(12,bind([[_32648, _32519, _32584, _32711], [arr(a, arr(a, b)), nil, lam(app(app(var(suc(zero)), var(zero), a), var(zero), a)), arr(a, b)]]))).
% 218.26/210.85 cnf('1.1.1',plain,[-(tc(cons(arr(a, arr(a, b)), nil), lam(app(app(var(suc(zero)), var(zero), a), var(zero), a)), arr(a, b))), tc(cons(a, cons(arr(a, arr(a, b)), nil)), app(app(var(suc(zero)), var(zero), a), var(zero), a), b)],extension(12,bind([[_32648, _32519, _32584, _32711], [a, cons(arr(a, arr(a, b)), nil), app(app(var(suc(zero)), var(zero), a), var(zero), a), b]]))).
% 218.26/210.85 cnf('1.1.1.1',plain,[-(tc(cons(a, cons(arr(a, arr(a, b)), nil)), app(app(var(suc(zero)), var(zero), a), var(zero), a), b)), tc(cons(a, cons(arr(a, arr(a, b)), nil)), app(var(suc(zero)), var(zero), a), arr(a, b)), tc(cons(a, cons(arr(a, arr(a, b)), nil)), var(zero), a)],extension(8,bind([[_31176, _31101, _31025, _31250, _31323], [app(var(suc(zero)), var(zero), a), b, cons(a, cons(arr(a, arr(a, b)), nil)), var(zero), a]]))).
% 218.26/210.85 cnf('1.1.1.1.1',plain,[-(tc(cons(a, cons(arr(a, arr(a, b)), nil)), app(var(suc(zero)), var(zero), a), arr(a, b))), tc(cons(a, cons(arr(a, arr(a, b)), nil)), var(suc(zero)), arr(a, arr(a, b))), tc(cons(a, cons(arr(a, arr(a, b)), nil)), var(zero), a)],extension(8,bind([[_31176, _31101, _31025, _31250, _31323], [var(suc(zero)), arr(a, b), cons(a, cons(arr(a, arr(a, b)), nil)), var(zero), a]]))).
% 218.26/210.85 cnf('1.1.1.1.1.1',plain,[-(tc(cons(a, cons(arr(a, arr(a, b)), nil)), var(suc(zero)), arr(a, arr(a, b)))), index(cons(a, cons(arr(a, arr(a, b)), nil)), suc(zero)) = just(arr(a, arr(a, b))), arr(a, arr(a, b)) = arr(a, arr(a, b))],extension(3,bind([[_33676, _33813, _33880, _33745], [cons(a, cons(arr(a, arr(a, b)), nil)), suc(zero), arr(a, arr(a, b)), arr(a, arr(a, b))]]))).
% 218.26/210.85 cnf('1.1.1.1.1.1.1',plain,[-(index(cons(a, cons(arr(a, arr(a, b)), nil)), suc(zero)) = just(arr(a, arr(a, b)))), index(cons(a, cons(arr(a, arr(a, b)), nil)), suc(zero)) = index(cons(arr(a, arr(a, b)), nil), zero), index(cons(arr(a, arr(a, b)), nil), zero) = just(arr(a, arr(a, b)))],extension(2,bind([[_13951, _14007, _14062], [index(cons(a, cons(arr(a, arr(a, b)), nil)), suc(zero)), index(cons(arr(a, arr(a, b)), nil), zero), just(arr(a, arr(a, b)))]]))).
% 218.26/210.85 cnf('1.1.1.1.1.1.1.1',plain,[-(index(cons(a, cons(arr(a, arr(a, b)), nil)), suc(zero)) = index(cons(arr(a, arr(a, b)), nil), zero))],extension(4,bind([[_30582, _30637, _30691], [a, cons(arr(a, arr(a, b)), nil), zero]]))).
% 218.26/210.85 cnf('1.1.1.1.1.1.1.2',plain,[-(index(cons(arr(a, arr(a, b)), nil), zero) = just(arr(a, arr(a, b))))],extension(6,bind([[_30299, _30252], [nil, arr(a, arr(a, b))]]))).
% 218.26/210.85 cnf('1.1.1.1.1.1.2',plain,[-(arr(a, arr(a, b)) = arr(a, arr(a, b))), arr(a, arr(a, b)) = arr(a, arr(a, b))],extension(10,bind([[_13672, _13717], [arr(a, arr(a, b)), arr(a, arr(a, b))]]))).
% 218.26/210.85 cnf('1.1.1.1.1.1.2.1',plain,[-(arr(a, arr(a, b)) = arr(a, arr(a, b)))],extension(11,bind([[_13519], [arr(a, arr(a, b))]]))).
% 218.26/210.85 cnf('1.1.1.1.1.2',plain,[-(tc(cons(a, cons(arr(a, arr(a, b)), nil)), var(zero), a)), tc(cons(proj1Suc(suc(a)), proj1Suc(suc(cons(arr(a, arr(a, b)), nil)))), var(zero), a), cons(proj1Suc(suc(a)), proj1Suc(suc(cons(arr(a, arr(a, b)), nil)))) = cons(a, cons(arr(a, arr(a, b)), nil)), var(zero) = var(zero), a = a],extension(7,bind([[_14417, _14502, _14586, _14669, _14751, _14832], [cons(proj1Suc(suc(a)), proj1Suc(suc(cons(arr(a, arr(a, b)), nil)))), cons(a, cons(arr(a, arr(a, b)), nil)), var(zero), var(zero), a, a]]))).
% 218.26/210.85 cnf('1.1.1.1.1.2.1',plain,[-(tc(cons(proj1Suc(suc(a)), proj1Suc(suc(cons(arr(a, arr(a, b)), nil)))), var(zero), a)), index(cons(proj1Suc(suc(a)), proj1Suc(suc(cons(arr(a, arr(a, b)), nil)))), zero) = just(proj1Suc(suc(a))), proj1Suc(suc(a)) = a],extension(3,bind([[_33676, _33813, _33880, _33745], [cons(proj1Suc(suc(a)), proj1Suc(suc(cons(arr(a, arr(a, b)), nil)))), zero, proj1Suc(suc(a)), a]]))).
% 218.26/210.85 cnf('1.1.1.1.1.2.1.1',plain,[-(index(cons(proj1Suc(suc(a)), proj1Suc(suc(cons(arr(a, arr(a, b)), nil)))), zero) = just(proj1Suc(suc(a))))],extension(6,bind([[_30299, _30252], [proj1Suc(suc(cons(arr(a, arr(a, b)), nil))), proj1Suc(suc(a))]]))).
% 218.26/210.85 cnf('1.1.1.1.1.2.1.2',plain,[-(proj1Suc(suc(a)) = a)],extension(1,bind([[_26328], [a]]))).
% 218.26/210.85 cnf('1.1.1.1.1.2.2',plain,[-(cons(proj1Suc(suc(a)), proj1Suc(suc(cons(arr(a, arr(a, b)), nil)))) = cons(a, cons(arr(a, arr(a, b)), nil))), proj1Suc(suc(a)) = a, proj1Suc(suc(cons(arr(a, arr(a, b)), nil))) = cons(arr(a, arr(a, b)), nil)],extension(13,bind([[_17106, _17173, _17239, _17304], [proj1Suc(suc(a)), a, proj1Suc(suc(cons(arr(a, arr(a, b)), nil))), cons(arr(a, arr(a, b)), nil)]]))).
% 218.26/210.85 cnf('1.1.1.1.1.2.2.1',plain,[-(proj1Suc(suc(a)) = a)],extension(1,bind([[_26328], [a]]))).
% 218.26/210.85 cnf('1.1.1.1.1.2.2.2',plain,[-(proj1Suc(suc(cons(arr(a, arr(a, b)), nil))) = cons(arr(a, arr(a, b)), nil))],extension(1,bind([[_26328], [cons(arr(a, arr(a, b)), nil)]]))).
% 218.26/210.85 cnf('1.1.1.1.1.2.3',plain,[-(var(zero) = var(zero)), zero = zero],extension(9,bind([[_22950, _22999], [zero, zero]]))).
% 218.26/210.85 cnf('1.1.1.1.1.2.3.1',plain,[-(zero = zero)],extension(11,bind([[_13519], [zero]]))).
% 218.26/210.85 cnf('1.1.1.1.1.2.4',plain,[-(a = a)],extension(11,bind([[_13519], [a]]))).
% 218.26/210.85 cnf('1.1.1.1.2',plain,[-(tc(cons(a, cons(arr(a, arr(a, b)), nil)), var(zero), a)), index(cons(a, cons(arr(a, arr(a, b)), nil)), zero) = just(a), a = a],extension(3,bind([[_33676, _33813, _33880, _33745], [cons(a, cons(arr(a, arr(a, b)), nil)), zero, a, a]]))).
% 218.26/210.85 cnf('1.1.1.1.2.1',plain,[-(index(cons(a, cons(arr(a, arr(a, b)), nil)), zero) = just(a))],extension(6,bind([[_30299, _30252], [cons(arr(a, arr(a, b)), nil), a]]))).
% 218.26/210.85 cnf('1.1.1.1.2.2',plain,[-(a = a), a = proj1Suc(suc(a)), proj1Suc(suc(a)) = a],extension(2,bind([[_13951, _14007, _14062], [a, proj1Suc(suc(a)), a]]))).
% 218.26/210.85 cnf('1.1.1.1.2.2.1',plain,[-(a = proj1Suc(suc(a))), proj1Suc(suc(a)) = a],extension(10,bind([[_13672, _13717], [proj1Suc(suc(a)), a]]))).
% 218.26/210.85 cnf('1.1.1.1.2.2.1.1',plain,[-(proj1Suc(suc(a)) = a)],extension(1,bind([[_26328], [a]]))).
% 218.26/210.85 cnf('1.1.1.1.2.2.2',plain,[-(proj1Suc(suc(a)) = a)],extension(1,bind([[_26328], [a]]))).
% 218.26/210.85 %-----------------------------------------------------
% 218.26/210.85
% 218.26/210.85 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------