%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWX200+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n011.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:04 PM UTC 2026
% Result : Theorem 0.34s 1.37s
% Output : Proof 0.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SWX200+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : nanocop.sh %s %d
% 0.15/0.33 % Computer : n011.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 11:14:47 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.34/1.37
% 0.34/1.37 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.34/1.37 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.34/1.37 %-----------------------------------------------------
% 0.34/1.37 ncf(matrix, plain, [(152 ^ _30929) ^ [_36588, _36590] : [ord(_36590), -(ord(_36588)), -(ord(merge(_36590, _36588)))], (88 ^ _30929) ^ [_33999, _34001] : [-(head(cons(_34001, _33999)) = _34001)], (90 ^ _30929) ^ [_34098, _34100] : [-(tail(cons(_34100, _34098)) = _34098)], (92 ^ _30929) ^ [_34196, _34198] : [nil = cons(_34198, _34196)], (94 ^ _30929) ^ [_34279] : [-(proj1S(s(_34279)) = _34279)], (96 ^ _30929) ^ [_34360] : [z = s(_34360)], (98 ^ _30929) ^ [_34440] : [-(leqNat(z, _34440))], (100 ^ _30929) ^ [_34517] : [leqNat(s(_34517), z)], (102 ^ _30929) ^ [_34655, _34657] : [leqNat(s(_34657), s(_34655)), -(leqNat(_34657, _34655))], (108 ^ _30929) ^ [_34825, _34827] : [leqNat(_34827, _34825), -(leqNat(s(_34827), s(_34825)))], (114 ^ _30929) ^ [_35016] : [-(merge(nil, _35016) = _35016)], (116 ^ _30929) ^ [_35111, _35113] : [-(merge(cons(_35113, _35111), nil) = cons(_35113, _35111))], (118 ^ _30929) ^ [_35257, _35259, _35261, _35263] : [leqNat(_35263, _35259), -(merge(cons(_35263, _35261), cons(_35259, _35257)) = cons(_35263, merge(_35261, cons(_35259, _35257))))], (124 ^ _30929) ^ [_35543, _35545, _35547, _35549] : [-(leqNat(_35549, _35545)), -(merge(cons(_35549, _35547), cons(_35545, _35543)) = cons(_35545, merge(cons(_35549, _35547), _35543)))], (130 ^ _30929) ^ [] : [-(ord(nil))], (132 ^ _30929) ^ [_35828] : [-(ord(cons(_35828, nil)))], (134 ^ _30929) ^ [_35960, _35962, _35964] : [ord(cons(_35964, cons(_35962, _35960))), 137 ^ _30929 : [(138 ^ _30929) ^ [] : [-(leqNat(_35964, _35962))], (140 ^ _30929) ^ [] : [-(ord(cons(_35962, _35960)))]]], (142 ^ _30929) ^ [_36219, _36221, _36223] : [-(ord(cons(_36223, cons(_36221, _36219)))), leqNat(_36223, _36221), ord(cons(_36221, _36219))], (2 ^ _30929) ^ [_31073] : [-(_31073 = _31073)], (4 ^ _30929) ^ [_31180, _31182] : [_31182 = _31180, -(_31180 = _31182)], (10 ^ _30929) ^ [_31384, _31386, _31388] : [-(_31388 = _31384), _31388 = _31386, _31386 = _31384], (34 ^ _30929) ^ [_32121, _32123] : [-(ord(_32121)), _32123 = _32121, ord(_32123)], (20 ^ _30929) ^ [_31725, _31727, _31729, _31731] : [-(leqNat(_31729, _31725)), leqNat(_31731, _31727), _31731 = _31729, _31727 = _31725], (44 ^ _30929) ^ [_32424, _32426] : [_32426 = _32424, -(head(_32426) = head(_32424))], (50 ^ _30929) ^ [_32642, _32644] : [_32644 = _32642, -(tail(_32644) = tail(_32642))], (56 ^ _30929) ^ [_32860, _32862] : [_32862 = _32860, -(proj1S(_32862) = proj1S(_32860))], (62 ^ _30929) ^ [_33078, _33080] : [_33080 = _33078, -(s(_33080) = s(_33078))], (68 ^ _30929) ^ [_33324, _33326, _33328, _33330] : [-(cons(_33330, _33326) = cons(_33328, _33324)), _33330 = _33328, _33326 = _33324], (78 ^ _30929) ^ [_33663, _33665, _33667, _33669] : [-(merge(_33669, _33665) = merge(_33667, _33663)), _33669 = _33667, _33665 = _33663]], input).
% 0.34/1.37 ncf('1',plain,[leqNat(s(_19415), z)],start(100 ^ 0,bind([[_34517], [_19415]]))).
% 0.34/1.37 ncf('1.1',plain,[-(leqNat(s(_19415), z)), ord(cons(s(_19415), cons(z, _21754)))],extension(134 ^ 1,bind([[_35960, _35962, _35964], [_21754, z, s(_19415)]]))).
% 0.34/1.37 ncf('1.1.1',plain,[-(ord(cons(s(_19415), cons(z, _21754)))), ord(nil), -(ord(merge(nil, cons(s(_19415), cons(z, _21754)))))],extension(152 ^ 2,bind([[_36588, _36590], [cons(s(_19415), cons(z, _21754)), nil]]))).
% 0.34/1.37 ncf('1.1.1.1',plain,[-(ord(nil))],extension(130 ^ 3)).
% 0.34/1.37 ncf('1.1.1.2',plain,[ord(merge(nil, cons(s(_19415), cons(z, _21754)))), -(ord(cons(s(_19415), cons(z, _21754)))), merge(nil, cons(s(_19415), cons(z, _21754))) = cons(s(_19415), cons(z, _21754))],extension(34 ^ 3,bind([[_32121, _32123], [cons(s(_19415), cons(z, _21754)), merge(nil, cons(s(_19415), cons(z, _21754)))]]))).
% 0.34/1.37 ncf('1.1.1.2.1',plain,[ord(cons(s(_19415), cons(z, _21754)))],reduction('1.1')).
% 0.34/1.37 ncf('1.1.1.2.2',plain,[-(merge(nil, cons(s(_19415), cons(z, _21754))) = cons(s(_19415), cons(z, _21754)))],extension(114 ^ 4,bind([[_35016], [cons(s(_19415), cons(z, _21754))]]))).
% 0.34/1.37 %-----------------------------------------------------
% 0.34/1.37 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------