%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWX224+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n018.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:05:06 PM UTC 2026
% Result : Theorem 192.01s 185.60s
% Output : Proof 192.01s
% 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 : nanocop.sh %s %d
% 0.17/0.33 % Computer : n018.cluster.edu
% 0.17/0.33 % Model : x86_64 x86_64
% 0.17/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.33 % Memory : 8042.1875MB
% 0.17/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.33 % CPULimit : 300
% 0.17/0.33 % WCLimit : 300
% 0.17/0.33 % DateTime : Tue May 5 12:40:16 EDT 2026
% 0.17/0.33 % CPUTime :
% 192.01/185.60
% 192.01/185.60 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 192.01/185.60 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 192.01/185.60 %-----------------------------------------------------
% 192.01/185.60 ncf(matrix, plain, [(282 ^ _80589) ^ [_80618] : [tc(nil, _80618, arr(arr(a, arr(a, b)), arr(a, b)))], !, (184 ^ _69633) ^ [_76431, _76433] : [arr(_76433, _76431) = b], (260 ^ _69633) ^ [_79758, _79760, _79762] : [index(_79762, _79758) = nothing, tc(_79762, var(_79758), _79760)], (4 ^ _69633) ^ [_69864, _69866] : [_69866 = _69864, -(_69864 = _69866)], (214 ^ _69633) ^ [_77772, _77774, _77776, _77778] : [app(_77778, _77776, _77774) = var(_77772)], (150 ^ _69633) ^ [_75040, _75042] : [_75042 = _75040, -(just(_75042) = just(_75040))], (118 ^ _69633) ^ [_73886, _73888] : [_73888 = _73886, -(proj2Arr(_73888) = proj2Arr(_73886))], (212 ^ _69633) ^ [_77641, _77643, _77645, _77647] : [app(_77647, _77645, _77643) = lam(_77641)], (74 ^ _69633) ^ [_72280, _72282] : [_72282 = _72280, -(proj3App(_72282) = proj3App(_72280))], (266 ^ _69633) ^ [_79995, _79997, _79999, _80001] : [index(_80001, _79997) = just(_79995), 269 ^ _69633 : [(276 ^ _69633) ^ [] : [_79995 = _79999, -(tc(_80001, var(_79997), _79999))], (270 ^ _69633) ^ [] : [tc(_80001, var(_79997), _79999), -(_79995 = _79999)]]], (194 ^ _69633) ^ [_76766] : [-(proj1Suc(suc(_76766)) = _76766)], (178 ^ _69633) ^ [_76138, _76140] : [-(proj1Arr(arr(_76140, _76138)) = _76140)], (98 ^ _69633) ^ [_73208, _73210, _73212, _73214, _73216, _73218] : [-(app(_73218, _73214, _73210) = app(_73216, _73212, _73208)), _73218 = _73216, _73214 = _73212, _73210 = _73208], (232 ^ _69633) ^ [_78644, _78646, _78648, _78650, _78652] : [-(tc(_78652, app(_78648, _78646, _78644), _78650)), tc(_78652, _78648, arr(_78644, _78650)), tc(_78652, _78646, _78644)], (218 ^ _69633) ^ [_77959] : [-(index(nil, _77959) = nothing)], (206 ^ _69633) ^ [_77348, _77350, _77352] : [-(proj3App(app(_77352, _77350, _77348)) = _77348)], (196 ^ _69633) ^ [_76847] : [zero = suc(_76847)], (210 ^ _69633) ^ [_77518] : [-(proj1Var(var(_77518)) = _77518)], (188 ^ _69633) ^ [] : [a = b], (172 ^ _69633) ^ [_75844, _75846] : [-(head(cons(_75846, _75844)) = _75846)], (92 ^ _69633) ^ [_72934, _72936] : [_72936 = _72934, -(suc(_72936) = suc(_72934))], (140 ^ _69633) ^ [_74709, _74711, _74713, _74715] : [-(index(_74715, _74711) = index(_74713, _74709)), _74715 = _74713, _74711 = _74709], (222 ^ _69633) ^ [_78170, _78172, _78174] : [-(index(cons(_78174, _78172), suc(_78170)) = index(_78172, _78170))], (220 ^ _69633) ^ [_78054, _78056] : [-(index(cons(_78056, _78054), zero) = just(_78056))], (62 ^ _69633) ^ [_71844, _71846] : [_71846 = _71844, -(proj1App(_71846) = proj1App(_71844))], (182 ^ _69633) ^ [_76335, _76337] : [arr(_76337, _76335) = a], (190 ^ _69633) ^ [] : [a = c], (254 ^ _69633) ^ [_79500, _79502, _79504, _79506] : [tc(cons(_79502, _79506), _79504, _79500), -(tc(_79506, lam(_79504), arr(_79502, _79500)))], (186 ^ _69633) ^ [_76527, _76529] : [arr(_76529, _76527) = c], (208 ^ _69633) ^ [_77436] : [-(proj1Lam(lam(_77436)) = _77436)], (44 ^ _69633) ^ [_71190, _71192] : [_71192 = _71190, -(tail(_71192) = tail(_71190))], (180 ^ _69633) ^ [_76237, _76239] : [-(proj2Arr(arr(_76239, _76237)) = _76237)], (242 ^ _69633) ^ [_79009, _79011, _79013] : [-(_79011 = arr(proj1Arr(_79011), proj2Arr(_79011))), tc(_79013, lam(_79009), _79011)], (20 ^ _69633) ^ [_70417, _70419, _70421, _70423, _70425, _70427] : [-(tc(_70425, _70421, _70417)), tc(_70427, _70423, _70419), _70427 = _70425, _70423 = _70421, _70419 = _70417], (38 ^ _69633) ^ [_70972, _70974] : [_70974 = _70972, -(head(_70974) = head(_70972))], (156 ^ _69633) ^ [_75258, _75260] : [_75260 = _75258, -(var(_75260) = var(_75258))], (86 ^ _69633) ^ [_72716, _72718] : [_72718 = _72716, -(proj1Var(_72718) = proj1Var(_72716))], (162 ^ _69633) ^ [_75484, _75486, _75488, _75490] : [-(arr(_75490, _75486) = arr(_75488, _75484)), _75490 = _75488, _75486 = _75484], (50 ^ _69633) ^ [_71408, _71410] : [_71410 = _71408, -(proj1Suc(_71410) = proj1Suc(_71408))], (174 ^ _69633) ^ [_75943, _75945] : [-(tail(cons(_75945, _75943)) = _75943)], (216 ^ _69633) ^ [_77875, _77877] : [lam(_77877) = var(_77875)], (112 ^ _69633) ^ [_73668, _73670] : [_73670 = _73668, -(proj1Arr(_73670) = proj1Arr(_73668))], (224 ^ _69633) ^ [_78363, _78365, _78367, _78369, _78371] : [tc(_78371, app(_78367, _78365, _78363), _78369), 227 ^ _69633 : [(230 ^ _69633) ^ [] : [-(tc(_78371, _78365, _78363))], (228 ^ _69633) ^ [] : [-(tc(_78371, _78367, arr(_78363, _78369)))]]], (2 ^ _69633) ^ [_69757] : [-(_69757 = _69757)], (202 ^ _69633) ^ [_77116, _77118, _77120] : [-(proj1App(app(_77120, _77118, _77116)) = _77120)], (80 ^ _69633) ^ [_72498, _72500] : [_72500 = _72498, -(proj1Lam(_72500) = proj1Lam(_72498))], (56 ^ _69633) ^ [_71626, _71628] : [_71628 = _71626, -(proj1Just(_71628) = proj1Just(_71626))], (68 ^ _69633) ^ [_72062, _72064] : [_72064 = _72062, -(proj2App(_72064) = proj2App(_72062))], (200 ^ _69633) ^ [_77008] : [nothing = just(_77008)], (124 ^ _69633) ^ [_74104, _74106] : [_74106 = _74104, -(lam(_74106) = lam(_74104))], (248 ^ _69633) ^ [_79306, _79308, _79310, _79312] : [tc(_79312, lam(_79310), arr(_79308, _79306)), -(tc(cons(_79308, _79312), _79310, _79306))], (10 ^ _69633) ^ [_70068, _70070, _70072] : [-(_70072 = _70068), _70072 = _70070, _70070 = _70068], (130 ^ _69633) ^ [_74350, _74352, _74354, _74356] : [-(cons(_74356, _74352) = cons(_74354, _74350)), _74356 = _74354, _74352 = _74350], (176 ^ _69633) ^ [_76041, _76043] : [nil = cons(_76043, _76041)], (204 ^ _69633) ^ [_77232, _77234, _77236] : [-(proj2App(app(_77236, _77234, _77232)) = _77234)], (198 ^ _69633) ^ [_76927] : [-(proj1Just(just(_76927)) = _76927)], (192 ^ _69633) ^ [] : [b = c]], input).
% 192.01/185.60 ncf('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(282 ^ 0,bind([[_80618], [lam(lam(app(app(var(suc(zero)), var(zero), a), var(zero), a)))]]))).
% 192.01/185.60 ncf('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(254 ^ 1,bind([[_79500, _79502, _79504, _79506], [arr(a, b), arr(a, arr(a, b)), lam(app(app(var(suc(zero)), var(zero), a), var(zero), a)), nil]]))).
% 192.01/185.60 ncf('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(254 ^ 2,bind([[_79500, _79502, _79504, _79506], [b, a, app(app(var(suc(zero)), var(zero), a), var(zero), a), cons(arr(a, arr(a, b)), nil)]]))).
% 192.01/185.60 ncf('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(232 ^ 3,bind([[_78644, _78646, _78648, _78650, _78652], [a, var(zero), app(var(suc(zero)), var(zero), a), b, cons(a, cons(arr(a, arr(a, b)), nil))]]))).
% 192.01/185.60 ncf('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(232 ^ 4,bind([[_78644, _78646, _78648, _78650, _78652], [a, var(zero), var(suc(zero)), arr(a, b), cons(a, cons(arr(a, arr(a, b)), nil))]]))).
% 192.01/185.60 ncf('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)))), 276 : arr(a, arr(a, b)) = arr(a, arr(a, b)), 276 : index(cons(a, cons(arr(a, arr(a, b)), nil)), suc(zero)) = just(arr(a, arr(a, b)))],extension(266 ^ 5,bind([[_79995, _79997, _79999, _80001], [arr(a, arr(a, b)), suc(zero), arr(a, arr(a, b)), cons(a, cons(arr(a, arr(a, b)), nil))]]))).
% 192.01/185.60 ncf('1.1.1.1.1.1.1',plain,[-(arr(a, arr(a, b)) = arr(a, arr(a, b))), arr(a, arr(a, b)) = arr(a, arr(a, b))],extension(4 ^ 8,bind([[_69864, _69866], [arr(a, arr(a, b)), arr(a, arr(a, b))]]))).
% 192.01/185.60 ncf('1.1.1.1.1.1.1.1',plain,[-(arr(a, arr(a, b)) = arr(a, arr(a, b)))],extension(2 ^ 9,bind([[_69757], [arr(a, arr(a, b))]]))).
% 192.01/185.60 ncf('1.1.1.1.1.1.2',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(10 ^ 6,bind([[_70068, _70070, _70072], [just(arr(a, arr(a, b))), index(cons(arr(a, arr(a, b)), nil), zero), index(cons(a, cons(arr(a, arr(a, b)), nil)), suc(zero))]]))).
% 192.01/185.60 ncf('1.1.1.1.1.1.2.1',plain,[-(index(cons(a, cons(arr(a, arr(a, b)), nil)), suc(zero)) = index(cons(arr(a, arr(a, b)), nil), zero))],extension(222 ^ 7,bind([[_78170, _78172, _78174], [zero, cons(arr(a, arr(a, b)), nil), a]]))).
% 192.01/185.60 ncf('1.1.1.1.1.1.2.2',plain,[-(index(cons(arr(a, arr(a, b)), nil), zero) = just(arr(a, arr(a, b))))],extension(220 ^ 7,bind([[_78054, _78056], [nil, arr(a, arr(a, b))]]))).
% 192.01/185.60 ncf('1.1.1.1.1.2',plain,[-(tc(cons(a, cons(arr(a, arr(a, b)), nil)), var(zero), a)), 276 : a = a, 276 : index(cons(a, cons(arr(a, arr(a, b)), nil)), zero) = just(a)],extension(266 ^ 5,bind([[_79995, _79997, _79999, _80001], [a, zero, a, cons(a, cons(arr(a, arr(a, b)), nil))]]))).
% 192.01/185.60 ncf('1.1.1.1.1.2.1',plain,[-(a = a), a = a],extension(4 ^ 8,bind([[_69864, _69866], [a, a]]))).
% 192.01/185.60 ncf('1.1.1.1.1.2.1.1',plain,[-(a = a)],extension(2 ^ 9,bind([[_69757], [a]]))).
% 192.01/185.60 ncf('1.1.1.1.1.2.2',plain,[-(index(cons(a, cons(arr(a, arr(a, b)), nil)), zero) = just(a))],extension(220 ^ 6,bind([[_78054, _78056], [cons(arr(a, arr(a, b)), nil), a]]))).
% 192.01/185.60 ncf('1.1.1.1.2',plain,[-(tc(cons(a, cons(arr(a, arr(a, b)), nil)), var(zero), a)), 276 : a = a, 276 : index(cons(a, cons(arr(a, arr(a, b)), nil)), zero) = just(a)],extension(266 ^ 4,bind([[_79995, _79997, _79999, _80001], [a, zero, a, cons(a, cons(arr(a, arr(a, b)), nil))]]))).
% 192.01/185.60 ncf('1.1.1.1.2.1',plain,[-(a = a), a = a],extension(4 ^ 7,bind([[_69864, _69866], [a, a]]))).
% 192.01/185.60 ncf('1.1.1.1.2.1.1',plain,[-(a = a)],extension(2 ^ 8,bind([[_69757], [a]]))).
% 192.01/185.60 ncf('1.1.1.1.2.2',plain,[-(index(cons(a, cons(arr(a, arr(a, b)), nil)), zero) = just(a))],extension(220 ^ 5,bind([[_78054, _78056], [cons(arr(a, arr(a, b)), nil), a]]))).
% 192.01/185.60 %-----------------------------------------------------
% 192.01/185.60 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------