%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWX186+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n023.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:02 PM UTC 2026
% Result : Theorem 0.33s 1.38s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX186+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.13 % Command : nanocop.sh %s %d
% 0.16/0.34 % Computer : n023.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Tue May 5 09:37:38 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.33/1.38
% 0.33/1.38 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.33/1.38 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.33/1.38 %-----------------------------------------------------
% 0.33/1.38 ncf(matrix, plain, [(80 ^ _19403) ^ [_22481, _22483, _22485] : [drop(_22485, _22483) = drop(_22485, _22481), -(_22483 = _22481)], (64 ^ _19403) ^ [_21722, _21724] : [-(head(cons(_21724, _21722)) = _21724)], (66 ^ _19403) ^ [_21821, _21823] : [-(tail(cons(_21823, _21821)) = _21821)], (68 ^ _19403) ^ [_21919, _21921] : [nil = cons(_21921, _21919)], (70 ^ _19403) ^ [_22002] : [-(proj1S(s(_22002)) = _22002)], (72 ^ _19403) ^ [_22083] : [s(_22083) = z], (74 ^ _19403) ^ [_22163] : [-(drop(s(_22163), nil) = nil)], (76 ^ _19403) ^ [_22274, _22276, _22278] : [-(drop(s(_22278), cons(_22276, _22274)) = drop(_22278, _22274))], (78 ^ _19403) ^ [_22347] : [-(drop(z, _22347) = _22347)], (2 ^ _19403) ^ [_19527] : [-(_19527 = _19527)], (4 ^ _19403) ^ [_19634, _19636] : [_19636 = _19634, -(_19634 = _19636)], (10 ^ _19403) ^ [_19838, _19840, _19842] : [-(_19842 = _19838), _19842 = _19840, _19840 = _19838], (20 ^ _19403) ^ [_20151, _20153] : [_20153 = _20151, -(head(_20153) = head(_20151))], (26 ^ _19403) ^ [_20369, _20371] : [_20371 = _20369, -(tail(_20371) = tail(_20369))], (32 ^ _19403) ^ [_20587, _20589] : [_20589 = _20587, -(proj1S(_20589) = proj1S(_20587))], (38 ^ _19403) ^ [_20805, _20807] : [_20807 = _20805, -(s(_20807) = s(_20805))], (44 ^ _19403) ^ [_21051, _21053, _21055, _21057] : [-(cons(_21057, _21053) = cons(_21055, _21051)), _21057 = _21055, _21053 = _21051], (54 ^ _19403) ^ [_21390, _21392, _21394, _21396] : [-(drop(_21396, _21392) = drop(_21394, _21390)), _21396 = _21394, _21392 = _21390]], input).
% 0.33/1.38 ncf('1',plain,[nil = cons(_12817, drop(s(z), nil))],start(68 ^ 0,bind([[_21919, _21921], [drop(s(z), nil), _12817]]))).
% 0.33/1.38 ncf('1.1',plain,[-(nil = cons(_12817, drop(s(z), nil))), drop(s(z), nil) = drop(s(z), cons(_12817, drop(s(z), nil)))],extension(80 ^ 1,bind([[_22481, _22483, _22485], [cons(_12817, drop(s(z), nil)), nil, s(z)]]))).
% 0.33/1.38 ncf('1.1.1',plain,[-(drop(s(z), nil) = drop(s(z), cons(_12817, drop(s(z), nil)))), drop(s(z), cons(_12817, drop(s(z), nil))) = drop(s(z), nil)],extension(4 ^ 2,bind([[_19634, _19636], [drop(s(z), nil), drop(s(z), cons(_12817, drop(s(z), nil)))]]))).
% 0.33/1.38 ncf('1.1.1.1',plain,[-(drop(s(z), cons(_12817, drop(s(z), nil))) = drop(s(z), nil)), drop(s(z), cons(_12817, drop(s(z), nil))) = drop(z, drop(s(z), nil)), drop(z, drop(s(z), nil)) = drop(s(z), nil)],extension(10 ^ 3,bind([[_19838, _19840, _19842], [drop(s(z), nil), drop(z, drop(s(z), nil)), drop(s(z), cons(_12817, drop(s(z), nil)))]]))).
% 0.33/1.38 ncf('1.1.1.1.1',plain,[-(drop(s(z), cons(_12817, drop(s(z), nil))) = drop(z, drop(s(z), nil)))],extension(76 ^ 4,bind([[_22274, _22276, _22278], [drop(s(z), nil), _12817, z]]))).
% 0.33/1.38 ncf('1.1.1.1.2',plain,[-(drop(z, drop(s(z), nil)) = drop(s(z), nil))],extension(78 ^ 4,bind([[_22347], [drop(s(z), nil)]]))).
% 0.33/1.38 %-----------------------------------------------------
% 0.33/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------