%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : KLE004+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n014.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 : Fri May 19 11:25:15 EDT 2023
% Result : Theorem 0.31s 1.38s
% Output : Proof 0.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KLE004+1 : TPTP v8.1.2. Released v4.0.0.
% 0.03/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n014.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri May 19 02:56:12 EDT 2023
% 0.12/0.33 % CPUTime :
% 0.31/1.38
% 0.31/1.38 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.31/1.38 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.31/1.38 %-----------------------------------------------------
% 0.31/1.38 ncf(matrix, plain, [(177 ^ _32504) ^ [] : [c(zero) = one], (84 ^ _32504) ^ [_35376, _35378] : [-(addition(_35378, _35376) = addition(_35376, _35378))], (86 ^ _32504) ^ [_35490, _35492, _35494] : [-(addition(_35490, addition(_35492, _35494)) = addition(addition(_35490, _35492), _35494))], (88 ^ _32504) ^ [_35584] : [-(addition(_35584, zero) = _35584)], (90 ^ _32504) ^ [_35665] : [-(addition(_35665, _35665) = _35665)], (92 ^ _32504) ^ [_35774, _35776, _35778] : [-(multiplication(_35778, multiplication(_35776, _35774)) = multiplication(multiplication(_35778, _35776), _35774))], (94 ^ _32504) ^ [_35868] : [-(multiplication(_35868, one) = _35868)], (96 ^ _32504) ^ [_35949] : [-(multiplication(one, _35949) = _35949)], (98 ^ _32504) ^ [_36058, _36060, _36062] : [-(multiplication(_36062, addition(_36060, _36058)) = addition(multiplication(_36062, _36060), multiplication(_36062, _36058)))], (100 ^ _32504) ^ [_36183, _36185, _36187] : [-(multiplication(addition(_36187, _36185), _36183) = addition(multiplication(_36187, _36183), multiplication(_36185, _36183)))], (102 ^ _32504) ^ [_36280] : [-(multiplication(_36280, zero) = zero)], (104 ^ _32504) ^ [_36361] : [-(multiplication(zero, _36361) = zero)], (106 ^ _32504) ^ [_36480, _36482] : [leq(_36482, _36480), -(addition(_36482, _36480) = _36480)], (112 ^ _32504) ^ [_36648, _36650] : [addition(_36650, _36648) = _36648, -(leq(_36650, _36648))], (118 ^ _32504) ^ [_36903] : [test(_36903), -(complement(121 ^ [_36903], _36903))], (125 ^ _32504) ^ [_37108] : [126 ^ _32504 : [(127 ^ _32504) ^ [_37175] : [complement(_37175, _37108)]], -(test(_37108))], (131 ^ _32504) ^ [_37363, _37365] : [complement(_37363, _37365), 134 ^ _32504 : [(135 ^ _32504) ^ [] : [-(multiplication(_37365, _37363) = zero)], (137 ^ _32504) ^ [] : [-(multiplication(_37363, _37365) = zero)], (139 ^ _32504) ^ [] : [-(addition(_37365, _37363) = one)]]], (141 ^ _32504) ^ [_37692, _37694] : [-(complement(_37692, _37694)), multiplication(_37694, _37692) = zero, multiplication(_37692, _37694) = zero, addition(_37694, _37692) = one], (171 ^ _32504) ^ [_38530] : [-(test(_38530)), -(c(_38530) = zero)], (155 ^ _32504) ^ [_38100, _38102] : [test(_38102), 158 ^ _32504 : [(159 ^ _32504) ^ [] : [c(_38102) = _38100, -(complement(_38102, _38100))], (165 ^ _32504) ^ [] : [complement(_38102, _38100), -(c(_38102) = _38100)]]], (58 ^ _32504) ^ [_34473, _34475, _34477, _34479] : [-(multiplication(_34479, _34475) = multiplication(_34477, _34473)), _34479 = _34477, _34475 = _34473], (78 ^ _32504) ^ [_35143, _35145] : [_35145 = _35143, -(c(_35145) = c(_35143))], (68 ^ _32504) ^ [_34832, _34834, _34836, _34838] : [-(addition(_34838, _34834) = addition(_34836, _34832)), _34838 = _34836, _34834 = _34832], (2 ^ _32504) ^ [_32648] : [-(_32648 = _32648)], (4 ^ _32504) ^ [_32755, _32757] : [_32757 = _32755, -(_32755 = _32757)], (10 ^ _32504) ^ [_32959, _32961, _32963] : [-(_32963 = _32959), _32963 = _32961, _32961 = _32959], (20 ^ _32504) ^ [_33300, _33302, _33304, _33306] : [-(leq(_33304, _33300)), leq(_33306, _33302), _33306 = _33304, _33302 = _33300], (48 ^ _32504) ^ [_34140, _34142] : [-(test(_34140)), _34142 = _34140, test(_34142)], (34 ^ _32504) ^ [_33744, _33746, _33748, _33750] : [-(complement(_33748, _33744)), complement(_33750, _33746), _33750 = _33748, _33746 = _33744]], input).
% 0.31/1.38 ncf('1',plain,[c(zero) = one],start(177 ^ 0)).
% 0.31/1.38 ncf('1.1',plain,[-(c(zero) = one), 165 : complement(zero, one), 165 : test(zero)],extension(155 ^ 1,bind([[_38100, _38102], [one, zero]]))).
% 0.31/1.38 ncf('1.1.1',plain,[-(complement(zero, one)), multiplication(one, zero) = zero, multiplication(zero, one) = zero, addition(one, zero) = one],extension(141 ^ 4,bind([[_37692, _37694], [zero, one]]))).
% 0.31/1.38 ncf('1.1.1.1',plain,[-(multiplication(one, zero) = zero)],extension(96 ^ 5,bind([[_35949], [zero]]))).
% 0.31/1.38 ncf('1.1.1.2',plain,[-(multiplication(zero, one) = zero)],extension(94 ^ 5,bind([[_35868], [zero]]))).
% 0.31/1.38 ncf('1.1.1.3',plain,[-(addition(one, zero) = one)],extension(88 ^ 5,bind([[_35584], [one]]))).
% 0.31/1.38 ncf('1.1.2',plain,[-(test(zero)), 127 : complement(one, zero)],extension(125 ^ 2,bind([[_37108, _37175], [zero, one]]))).
% 0.31/1.38 ncf('1.1.2.1',plain,[-(complement(one, zero)), multiplication(zero, one) = zero, multiplication(one, zero) = zero, addition(zero, one) = one],extension(141 ^ 5,bind([[_37692, _37694], [one, zero]]))).
% 0.31/1.38 ncf('1.1.2.1.1',plain,[-(multiplication(zero, one) = zero)],extension(94 ^ 6,bind([[_35868], [zero]]))).
% 0.31/1.38 ncf('1.1.2.1.2',plain,[-(multiplication(one, zero) = zero)],extension(96 ^ 6,bind([[_35949], [zero]]))).
% 0.31/1.38 ncf('1.1.2.1.3',plain,[-(addition(zero, one) = one), addition(zero, one) = addition(one, zero), addition(one, zero) = one],extension(10 ^ 6,bind([[_32959, _32961, _32963], [one, addition(one, zero), addition(zero, one)]]))).
% 0.31/1.38 ncf('1.1.2.1.3.1',plain,[-(addition(zero, one) = addition(one, zero))],extension(84 ^ 7,bind([[_35376, _35378], [one, zero]]))).
% 0.31/1.38 ncf('1.1.2.1.3.2',plain,[-(addition(one, zero) = one)],extension(88 ^ 7,bind([[_35584], [one]]))).
% 0.31/1.38 %-----------------------------------------------------
% 0.31/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------