%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU219+1 : TPTP v8.1.2. Released v3.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 : Fri May 19 12:02:43 EDT 2023
% Result : Theorem 0.30s 1.39s
% Output : Proof 0.30s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SEU219+1 : TPTP v8.1.2. Released v3.3.0.
% 0.11/0.13 % Command : nanocop.sh %s %d
% 0.13/0.34 % Computer : n023.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 18 13:27:59 EDT 2023
% 0.13/0.35 % CPUTime :
% 0.30/1.39
% 0.30/1.39 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.30/1.39 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.30/1.39 %-----------------------------------------------------
% 0.30/1.39 ncf(matrix, plain, [(161 ^ _24960) ^ [] : [-(relation(159 ^ []))], (163 ^ _24960) ^ [] : [-(function(159 ^ []))], (165 ^ _24960) ^ [] : [-(one_to_one(159 ^ []))], (167 ^ _24960) ^ [] : [relation_rng(159 ^ []) = relation_dom(function_inverse(159 ^ [])), relation_dom(159 ^ []) = relation_rng(function_inverse(159 ^ []))], (74 ^ _24960) ^ [_27455] : [relation(_27455), function(_27455), one_to_one(_27455), -(function_inverse(_27455) = relation_inverse(_27455))], (88 ^ _24960) ^ [] : [true___, -(true___)], (94 ^ _24960) ^ [_27938] : [101 ^ _24960 : [(102 ^ _24960) ^ [] : [-(relation(function_inverse(_27938)))], (104 ^ _24960) ^ [] : [-(function(function_inverse(_27938)))]], relation(_27938), function(_27938)], (106 ^ _24960) ^ [] : [true___, -(true___)], (112 ^ _24960) ^ [_28405] : [relation(_28405), -(relation(relation_inverse(_28405)))], (118 ^ _24960) ^ [_28595] : [129 ^ _24960 : [(130 ^ _24960) ^ [] : [-(relation(relation_inverse(_28595)))], (132 ^ _24960) ^ [] : [-(function(relation_inverse(_28595)))]], relation(_28595), function(_28595), one_to_one(_28595)], (134 ^ _24960) ^ [_29026] : [relation(_29026), -(relation_inverse(relation_inverse(_29026)) = _29026)], (141 ^ _24960) ^ [] : [-(relation(139 ^ []))], (143 ^ _24960) ^ [] : [-(function(139 ^ []))], (146 ^ _24960) ^ [] : [-(relation(144 ^ []))], (148 ^ _24960) ^ [] : [-(function(144 ^ []))], (150 ^ _24960) ^ [] : [-(one_to_one(144 ^ []))], (152 ^ _24960) ^ [_29560] : [relation(_29560), 155 ^ _24960 : [(156 ^ _24960) ^ [] : [-(relation_rng(_29560) = relation_dom(relation_inverse(_29560)))], (158 ^ _24960) ^ [] : [-(relation_dom(_29560) = relation_rng(relation_inverse(_29560)))]]], (50 ^ _24960) ^ [_26603, _26605] : [_26605 = _26603, -(relation_inverse(_26605) = relation_inverse(_26603))], (56 ^ _24960) ^ [_26821, _26823] : [_26823 = _26821, -(relation_dom(_26823) = relation_dom(_26821))], (62 ^ _24960) ^ [_27039, _27041] : [_27041 = _27039, -(relation_rng(_27041) = relation_rng(_27039))], (68 ^ _24960) ^ [_27237, _27239] : [_27239 = _27237, -(function_inverse(_27239) = function_inverse(_27237))], (2 ^ _24960) ^ [_25104] : [-(_25104 = _25104)], (4 ^ _24960) ^ [_25211, _25213] : [_25213 = _25211, -(_25211 = _25213)], (10 ^ _24960) ^ [_25415, _25417, _25419] : [-(_25419 = _25415), _25419 = _25417, _25417 = _25415], (20 ^ _24960) ^ [_25728, _25730] : [-(relation(_25728)), _25730 = _25728, relation(_25730)], (30 ^ _24960) ^ [_26023, _26025] : [-(function(_26023)), _26025 = _26023, function(_26025)], (40 ^ _24960) ^ [_26298, _26300] : [-(one_to_one(_26298)), _26300 = _26298, one_to_one(_26300)]], input).
% 0.30/1.39 ncf('1',plain,[relation_rng(159 ^ []) = relation_dom(function_inverse(159 ^ [])), relation_dom(159 ^ []) = relation_rng(function_inverse(159 ^ []))],start(167 ^ 0)).
% 0.30/1.39 ncf('1.1',plain,[-(relation_rng(159 ^ []) = relation_dom(function_inverse(159 ^ []))), relation_rng(159 ^ []) = relation_dom(relation_inverse(159 ^ [])), relation_dom(relation_inverse(159 ^ [])) = relation_dom(function_inverse(159 ^ []))],extension(10 ^ 1,bind([[_25415, _25417, _25419], [relation_dom(function_inverse(159 ^ [])), relation_dom(relation_inverse(159 ^ [])), relation_rng(159 ^ [])]]))).
% 0.30/1.39 ncf('1.1.1',plain,[-(relation_rng(159 ^ []) = relation_dom(relation_inverse(159 ^ []))), relation(159 ^ [])],extension(152 ^ 2,bind([[_29560], [159 ^ []]]))).
% 0.30/1.39 ncf('1.1.1.1',plain,[-(relation(159 ^ []))],extension(161 ^ 3)).
% 0.30/1.39 ncf('1.1.2',plain,[-(relation_dom(relation_inverse(159 ^ [])) = relation_dom(function_inverse(159 ^ []))), relation_inverse(159 ^ []) = function_inverse(159 ^ [])],extension(56 ^ 2,bind([[_26821, _26823], [function_inverse(159 ^ []), relation_inverse(159 ^ [])]]))).
% 0.30/1.39 ncf('1.1.2.1',plain,[-(relation_inverse(159 ^ []) = function_inverse(159 ^ [])), function_inverse(159 ^ []) = relation_inverse(159 ^ [])],extension(4 ^ 3,bind([[_25211, _25213], [relation_inverse(159 ^ []), function_inverse(159 ^ [])]]))).
% 0.30/1.39 ncf('1.1.2.1.1',plain,[-(function_inverse(159 ^ []) = relation_inverse(159 ^ [])), relation(159 ^ []), function(159 ^ []), one_to_one(159 ^ [])],extension(74 ^ 4,bind([[_27455], [159 ^ []]]))).
% 0.30/1.39 ncf('1.1.2.1.1.1',plain,[-(relation(159 ^ []))],extension(161 ^ 5)).
% 0.30/1.39 ncf('1.1.2.1.1.2',plain,[-(function(159 ^ []))],extension(163 ^ 5)).
% 0.30/1.39 ncf('1.1.2.1.1.3',plain,[-(one_to_one(159 ^ []))],extension(165 ^ 5)).
% 0.30/1.39 ncf('1.2',plain,[-(relation_dom(159 ^ []) = relation_rng(function_inverse(159 ^ []))), relation_dom(159 ^ []) = relation_rng(relation_inverse(159 ^ [])), relation_rng(relation_inverse(159 ^ [])) = relation_rng(function_inverse(159 ^ []))],extension(10 ^ 1,bind([[_25415, _25417, _25419], [relation_rng(function_inverse(159 ^ [])), relation_rng(relation_inverse(159 ^ [])), relation_dom(159 ^ [])]]))).
% 0.30/1.39 ncf('1.2.1',plain,[-(relation_dom(159 ^ []) = relation_rng(relation_inverse(159 ^ []))), relation(159 ^ [])],extension(152 ^ 2,bind([[_29560], [159 ^ []]]))).
% 0.30/1.39 ncf('1.2.1.1',plain,[-(relation(159 ^ []))],extension(161 ^ 3)).
% 0.30/1.39 ncf('1.2.2',plain,[-(relation_rng(relation_inverse(159 ^ [])) = relation_rng(function_inverse(159 ^ []))), relation_inverse(159 ^ []) = function_inverse(159 ^ [])],extension(62 ^ 2,bind([[_27039, _27041], [function_inverse(159 ^ []), relation_inverse(159 ^ [])]]))).
% 0.30/1.39 ncf('1.2.2.1',plain,[-(relation_inverse(159 ^ []) = function_inverse(159 ^ [])), function_inverse(159 ^ []) = relation_inverse(159 ^ [])],extension(4 ^ 3,bind([[_25211, _25213], [relation_inverse(159 ^ []), function_inverse(159 ^ [])]]))).
% 0.30/1.39 ncf('1.2.2.1.1',plain,[-(function_inverse(159 ^ []) = relation_inverse(159 ^ [])), relation(159 ^ []), function(159 ^ []), one_to_one(159 ^ [])],extension(74 ^ 4,bind([[_27455], [159 ^ []]]))).
% 0.30/1.39 ncf('1.2.2.1.1.1',plain,[-(relation(159 ^ []))],extension(161 ^ 5)).
% 0.30/1.39 ncf('1.2.2.1.1.2',plain,[-(function(159 ^ []))],extension(163 ^ 5)).
% 0.30/1.39 ncf('1.2.2.1.1.3',plain,[-(one_to_one(159 ^ []))],extension(165 ^ 5)).
% 0.30/1.39 %-----------------------------------------------------
% 0.30/1.39 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------