%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : SWX219+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %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 07:03:35 PM UTC 2026
% Result : Theorem 218.75s 211.77s
% Output : Proof 218.75s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SWX219+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : leancop_casc.sh %s %d
% 0.15/0.32 % Computer : n015.cluster.edu
% 0.15/0.32 % Model : x86_64 x86_64
% 0.15/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.32 % Memory : 8042.1875MB
% 0.15/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.32 % CPULimit : 300
% 0.15/0.32 % WCLimit : 300
% 0.15/0.32 % DateTime : Tue May 5 12:22:01 EDT 2026
% 0.15/0.33 % CPUTime :
% 218.75/211.77 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 218.75/211.77 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 218.75/211.78
% 218.75/211.78 %-----------------------------------------------------
% 218.75/211.78 fof(axiom_012, axiom, ! [_65210] : proj1Suc(suc(_65210)) = _65210, file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_012)).
% 218.75/211.78 fof(axiom_031, axiom, ! [_65348, _65351, _65354, _65357] : (index(_65348, _65354) = just(_65357) => (tc(_65348, var(_65354), _65351) <=> _65357 = _65351)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_031)).
% 218.75/211.78 fof(axiom_026, axiom, ! [_65578, _65581, _65584] : index(cons(_65578, _65581), suc(_65584)) = index(_65581, _65584), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_026)).
% 218.75/211.78 fof(goal_032, conjecture, ? [_65762] : tc(nil, _65762, arr(arr(b, c), arr(arr(a, b), arr(a, c)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', goal_032)).
% 218.75/211.78 fof(axiom_025, axiom, ! [_65956, _65959] : index(cons(_65956, _65959), zero) = just(_65956), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_025)).
% 218.75/211.78 fof(axiom_027, axiom, ! [_66124, _66127, _66130, _66133, _66136] : (tc(_66124, app(_66130, _66133, _66136), _66127) <=> tc(_66124, _66130, arr(_66136, _66127)) & tc(_66124, _66133, _66136)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_027)).
% 218.75/211.78 fof(axiom_029, axiom, ! [_66449, _66452, _66455, _66458] : (tc(_66449, lam(_66452), arr(_66455, _66458)) <=> tc(cons(_66455, _66449), _66452, _66458)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', axiom_029)).
% 218.75/211.78
% 218.75/211.78 cnf(1, plain, [-(proj1Suc(suc(_26394)) = _26394)], clausify(axiom_012)).
% 218.75/211.78 cnf(2, plain, [-(_14017 = _14128), _14017 = _14073, _14073 = _14128], theory(equality)).
% 218.75/211.78 cnf(3, plain, [index(_33742, _33879) = just(_33946), -(tc(_33742, var(_33879), _33811)), _33946 = _33811], clausify(axiom_031)).
% 218.75/211.78 cnf(4, plain, [-(index(cons(_30648, _30703), suc(_30757)) = index(_30703, _30757))], clausify(axiom_026)).
% 218.75/211.78 cnf(5, plain, [tc(nil, _34886, arr(arr(b, c), arr(arr(a, b), arr(a, c))))], clausify(goal_032)).
% 218.75/211.78 cnf(6, plain, [-(index(cons(_30318, _30365), zero) = just(_30318))], clausify(axiom_025)).
% 218.75/211.78 cnf(7, plain, [-(tc(_14568, _14735, _14898)), tc(_14483, _14652, _14817), _14483 = _14568, _14652 = _14735, _14817 = _14898], theory(equality)).
% 218.75/211.78 cnf(8, plain, [-(tc(_31091, app(_31242, _31316, _31389), _31167)), tc(_31091, _31242, arr(_31389, _31167)), tc(_31091, _31316, _31389)], clausify(axiom_027)).
% 218.75/211.78 cnf(9, plain, [_23016 = _23065, -(var(_23016) = var(_23065))], theory(equality)).
% 218.75/211.78 cnf(10, plain, [_13738 = _13783, -(_13783 = _13738)], theory(equality)).
% 218.75/211.78 cnf(11, plain, [-(_13585 = _13585)], theory(equality)).
% 218.75/211.78 cnf(12, plain, [-(tc(_32585, lam(_32650), arr(_32714, _32777))), tc(cons(_32714, _32585), _32650, _32777)], clausify(axiom_029)).
% 218.75/211.78 cnf(13, plain, [-(cons(_17172, _17305) = cons(_17239, _17370)), _17172 = _17239, _17305 = _17370], theory(equality)).
% 218.75/211.78
% 218.75/211.78 cnf('1',plain,[tc(nil, lam(lam(lam(app(var(suc(suc(zero))), app(var(suc(zero)), var(zero), a), b)))), arr(arr(b, c), arr(arr(a, b), arr(a, c))))],start(5,bind([[_34886], [lam(lam(lam(app(var(suc(suc(zero))), app(var(suc(zero)), var(zero), a), b))))]]))).
% 218.75/211.78 cnf('1.1',plain,[-(tc(nil, lam(lam(lam(app(var(suc(suc(zero))), app(var(suc(zero)), var(zero), a), b)))), arr(arr(b, c), arr(arr(a, b), arr(a, c))))), tc(cons(arr(b, c), nil), lam(lam(app(var(suc(suc(zero))), app(var(suc(zero)), var(zero), a), b))), arr(arr(a, b), arr(a, c)))],extension(12,bind([[_32714, _32585, _32650, _32777], [arr(b, c), nil, lam(lam(app(var(suc(suc(zero))), app(var(suc(zero)), var(zero), a), b))), arr(arr(a, b), arr(a, c))]]))).
% 218.75/211.78 cnf('1.1.1',plain,[-(tc(cons(arr(b, c), nil), lam(lam(app(var(suc(suc(zero))), app(var(suc(zero)), var(zero), a), b))), arr(arr(a, b), arr(a, c)))), tc(cons(arr(a, b), cons(arr(b, c), nil)), lam(app(var(suc(suc(zero))), app(var(suc(zero)), var(zero), a), b)), arr(a, c))],extension(12,bind([[_32714, _32585, _32650, _32777], [arr(a, b), cons(arr(b, c), nil), lam(app(var(suc(suc(zero))), app(var(suc(zero)), var(zero), a), b)), arr(a, c)]]))).
% 218.75/211.78 cnf('1.1.1.1',plain,[-(tc(cons(arr(a, b), cons(arr(b, c), nil)), lam(app(var(suc(suc(zero))), app(var(suc(zero)), var(zero), a), b)), arr(a, c))), tc(cons(a, cons(arr(a, b), cons(arr(b, c), nil))), app(var(suc(suc(zero))), app(var(suc(zero)), var(zero), a), b), c)],extension(12,bind([[_32714, _32585, _32650, _32777], [a, cons(arr(a, b), cons(arr(b, c), nil)), app(var(suc(suc(zero))), app(var(suc(zero)), var(zero), a), b), c]]))).
% 218.75/211.78 cnf('1.1.1.1.1',plain,[-(tc(cons(a, cons(arr(a, b), cons(arr(b, c), nil))), app(var(suc(suc(zero))), app(var(suc(zero)), var(zero), a), b), c)), tc(cons(a, cons(arr(a, b), cons(arr(b, c), nil))), var(suc(suc(zero))), arr(b, c)), tc(cons(a, cons(arr(a, b), cons(arr(b, c), nil))), app(var(suc(zero)), var(zero), a), b)],extension(8,bind([[_31242, _31167, _31091, _31316, _31389], [var(suc(suc(zero))), c, cons(a, cons(arr(a, b), cons(arr(b, c), nil))), app(var(suc(zero)), var(zero), a), b]]))).
% 218.75/211.78 cnf('1.1.1.1.1.1',plain,[-(tc(cons(a, cons(arr(a, b), cons(arr(b, c), nil))), var(suc(suc(zero))), arr(b, c))), index(cons(a, cons(arr(a, b), cons(arr(b, c), nil))), suc(suc(zero))) = just(arr(b, c)), arr(b, c) = arr(b, c)],extension(3,bind([[_33742, _33879, _33946, _33811], [cons(a, cons(arr(a, b), cons(arr(b, c), nil))), suc(suc(zero)), arr(b, c), arr(b, c)]]))).
% 218.75/211.78 cnf('1.1.1.1.1.1.1',plain,[-(index(cons(a, cons(arr(a, b), cons(arr(b, c), nil))), suc(suc(zero))) = just(arr(b, c))), index(cons(a, cons(arr(a, b), cons(arr(b, c), nil))), suc(suc(zero))) = index(cons(arr(b, c), nil), zero), index(cons(arr(b, c), nil), zero) = just(arr(b, c))],extension(2,bind([[_14017, _14073, _14128], [index(cons(a, cons(arr(a, b), cons(arr(b, c), nil))), suc(suc(zero))), index(cons(arr(b, c), nil), zero), just(arr(b, c))]]))).
% 218.75/211.78 cnf('1.1.1.1.1.1.1.1',plain,[-(index(cons(a, cons(arr(a, b), cons(arr(b, c), nil))), suc(suc(zero))) = index(cons(arr(b, c), nil), zero)), index(cons(a, cons(arr(a, b), cons(arr(b, c), nil))), suc(suc(zero))) = index(cons(arr(a, b), cons(arr(b, c), nil)), suc(zero)), index(cons(arr(a, b), cons(arr(b, c), nil)), suc(zero)) = index(cons(arr(b, c), nil), zero)],extension(2,bind([[_14017, _14073, _14128], [index(cons(a, cons(arr(a, b), cons(arr(b, c), nil))), suc(suc(zero))), index(cons(arr(a, b), cons(arr(b, c), nil)), suc(zero)), index(cons(arr(b, c), nil), zero)]]))).
% 218.75/211.78 cnf('1.1.1.1.1.1.1.1.1',plain,[-(index(cons(a, cons(arr(a, b), cons(arr(b, c), nil))), suc(suc(zero))) = index(cons(arr(a, b), cons(arr(b, c), nil)), suc(zero)))],extension(4,bind([[_30648, _30703, _30757], [a, cons(arr(a, b), cons(arr(b, c), nil)), suc(zero)]]))).
% 218.75/211.78 cnf('1.1.1.1.1.1.1.1.2',plain,[-(index(cons(arr(a, b), cons(arr(b, c), nil)), suc(zero)) = index(cons(arr(b, c), nil), zero))],extension(4,bind([[_30648, _30703, _30757], [arr(a, b), cons(arr(b, c), nil), zero]]))).
% 218.75/211.78 cnf('1.1.1.1.1.1.1.2',plain,[-(index(cons(arr(b, c), nil), zero) = just(arr(b, c)))],extension(6,bind([[_30365, _30318], [nil, arr(b, c)]]))).
% 218.75/211.78 cnf('1.1.1.1.1.1.2',plain,[-(arr(b, c) = arr(b, c)), arr(b, c) = proj1Suc(suc(arr(b, c))), proj1Suc(suc(arr(b, c))) = arr(b, c)],extension(2,bind([[_14017, _14073, _14128], [arr(b, c), proj1Suc(suc(arr(b, c))), arr(b, c)]]))).
% 218.75/211.78 cnf('1.1.1.1.1.1.2.1',plain,[-(arr(b, c) = proj1Suc(suc(arr(b, c)))), proj1Suc(suc(arr(b, c))) = arr(b, c)],extension(10,bind([[_13738, _13783], [proj1Suc(suc(arr(b, c))), arr(b, c)]]))).
% 218.75/211.78 cnf('1.1.1.1.1.1.2.1.1',plain,[-(proj1Suc(suc(arr(b, c))) = arr(b, c))],extension(1,bind([[_26394], [arr(b, c)]]))).
% 218.75/211.78 cnf('1.1.1.1.1.1.2.2',plain,[-(proj1Suc(suc(arr(b, c))) = arr(b, c))],extension(1,bind([[_26394], [arr(b, c)]]))).
% 218.75/211.78 cnf('1.1.1.1.1.2',plain,[-(tc(cons(a, cons(arr(a, b), cons(arr(b, c), nil))), app(var(suc(zero)), var(zero), a), b)), tc(cons(a, cons(arr(a, b), cons(arr(b, c), nil))), var(suc(zero)), arr(a, b)), tc(cons(a, cons(arr(a, b), cons(arr(b, c), nil))), var(zero), a)],extension(8,bind([[_31242, _31167, _31091, _31316, _31389], [var(suc(zero)), b, cons(a, cons(arr(a, b), cons(arr(b, c), nil))), var(zero), a]]))).
% 218.75/211.78 cnf('1.1.1.1.1.2.1',plain,[-(tc(cons(a, cons(arr(a, b), cons(arr(b, c), nil))), var(suc(zero)), arr(a, b))), index(cons(a, cons(arr(a, b), cons(arr(b, c), nil))), suc(zero)) = just(arr(a, b)), arr(a, b) = arr(a, b)],extension(3,bind([[_33742, _33879, _33946, _33811], [cons(a, cons(arr(a, b), cons(arr(b, c), nil))), suc(zero), arr(a, b), arr(a, b)]]))).
% 218.75/211.78 cnf('1.1.1.1.1.2.1.1',plain,[-(index(cons(a, cons(arr(a, b), cons(arr(b, c), nil))), suc(zero)) = just(arr(a, b))), index(cons(a, cons(arr(a, b), cons(arr(b, c), nil))), suc(zero)) = index(cons(arr(a, b), cons(arr(b, c), nil)), zero), index(cons(arr(a, b), cons(arr(b, c), nil)), zero) = just(arr(a, b))],extension(2,bind([[_14017, _14073, _14128], [index(cons(a, cons(arr(a, b), cons(arr(b, c), nil))), suc(zero)), index(cons(arr(a, b), cons(arr(b, c), nil)), zero), just(arr(a, b))]]))).
% 218.75/211.78 cnf('1.1.1.1.1.2.1.1.1',plain,[-(index(cons(a, cons(arr(a, b), cons(arr(b, c), nil))), suc(zero)) = index(cons(arr(a, b), cons(arr(b, c), nil)), zero))],extension(4,bind([[_30648, _30703, _30757], [a, cons(arr(a, b), cons(arr(b, c), nil)), zero]]))).
% 218.75/211.78 cnf('1.1.1.1.1.2.1.1.2',plain,[-(index(cons(arr(a, b), cons(arr(b, c), nil)), zero) = just(arr(a, b)))],extension(6,bind([[_30365, _30318], [cons(arr(b, c), nil), arr(a, b)]]))).
% 218.75/211.78 cnf('1.1.1.1.1.2.1.2',plain,[-(arr(a, b) = arr(a, b)), arr(a, b) = arr(a, b)],extension(10,bind([[_13738, _13783], [arr(a, b), arr(a, b)]]))).
% 218.75/211.78 cnf('1.1.1.1.1.2.1.2.1',plain,[-(arr(a, b) = arr(a, b))],extension(11,bind([[_13585], [arr(a, b)]]))).
% 218.75/211.78 cnf('1.1.1.1.1.2.2',plain,[-(tc(cons(a, cons(arr(a, b), cons(arr(b, c), nil))), var(zero), a)), tc(cons(proj1Suc(suc(a)), proj1Suc(suc(cons(arr(a, b), cons(arr(b, c), nil))))), var(zero), a), cons(proj1Suc(suc(a)), proj1Suc(suc(cons(arr(a, b), cons(arr(b, c), nil))))) = cons(a, cons(arr(a, b), cons(arr(b, c), nil))), var(zero) = var(zero), a = a],extension(7,bind([[_14483, _14568, _14652, _14735, _14817, _14898], [cons(proj1Suc(suc(a)), proj1Suc(suc(cons(arr(a, b), cons(arr(b, c), nil))))), cons(a, cons(arr(a, b), cons(arr(b, c), nil))), var(zero), var(zero), a, a]]))).
% 218.75/211.78 cnf('1.1.1.1.1.2.2.1',plain,[-(tc(cons(proj1Suc(suc(a)), proj1Suc(suc(cons(arr(a, b), cons(arr(b, c), nil))))), var(zero), a)), index(cons(proj1Suc(suc(a)), proj1Suc(suc(cons(arr(a, b), cons(arr(b, c), nil))))), zero) = just(proj1Suc(suc(a))), proj1Suc(suc(a)) = a],extension(3,bind([[_33742, _33879, _33946, _33811], [cons(proj1Suc(suc(a)), proj1Suc(suc(cons(arr(a, b), cons(arr(b, c), nil))))), zero, proj1Suc(suc(a)), a]]))).
% 218.75/211.78 cnf('1.1.1.1.1.2.2.1.1',plain,[-(index(cons(proj1Suc(suc(a)), proj1Suc(suc(cons(arr(a, b), cons(arr(b, c), nil))))), zero) = just(proj1Suc(suc(a))))],extension(6,bind([[_30365, _30318], [proj1Suc(suc(cons(arr(a, b), cons(arr(b, c), nil)))), proj1Suc(suc(a))]]))).
% 218.75/211.78 cnf('1.1.1.1.1.2.2.1.2',plain,[-(proj1Suc(suc(a)) = a)],extension(1,bind([[_26394], [a]]))).
% 218.75/211.78 cnf('1.1.1.1.1.2.2.2',plain,[-(cons(proj1Suc(suc(a)), proj1Suc(suc(cons(arr(a, b), cons(arr(b, c), nil))))) = cons(a, cons(arr(a, b), cons(arr(b, c), nil)))), proj1Suc(suc(a)) = a, proj1Suc(suc(cons(arr(a, b), cons(arr(b, c), nil)))) = cons(arr(a, b), cons(arr(b, c), nil))],extension(13,bind([[_17172, _17239, _17305, _17370], [proj1Suc(suc(a)), a, proj1Suc(suc(cons(arr(a, b), cons(arr(b, c), nil)))), cons(arr(a, b), cons(arr(b, c), nil))]]))).
% 218.75/211.78 cnf('1.1.1.1.1.2.2.2.1',plain,[-(proj1Suc(suc(a)) = a)],extension(1,bind([[_26394], [a]]))).
% 218.75/211.78 cnf('1.1.1.1.1.2.2.2.2',plain,[-(proj1Suc(suc(cons(arr(a, b), cons(arr(b, c), nil)))) = cons(arr(a, b), cons(arr(b, c), nil)))],extension(1,bind([[_26394], [cons(arr(a, b), cons(arr(b, c), nil))]]))).
% 218.75/211.78 cnf('1.1.1.1.1.2.2.3',plain,[-(var(zero) = var(zero)), zero = zero],extension(9,bind([[_23016, _23065], [zero, zero]]))).
% 218.75/211.78 cnf('1.1.1.1.1.2.2.3.1',plain,[-(zero = zero)],extension(11,bind([[_13585], [zero]]))).
% 218.75/211.78 cnf('1.1.1.1.1.2.2.4',plain,[-(a = a)],extension(11,bind([[_13585], [a]]))).
% 218.75/211.78 %-----------------------------------------------------
% 218.75/211.78
% 218.75/211.78 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------