%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SEU303+1 : TPTP v8.1.2. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n016.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:03:04 EDT 2023
% Result : Theorem 0.34s 1.39s
% Output : Proof 0.34s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SEU303+1 : TPTP v8.1.2. Released v3.3.0.
% 0.06/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n016.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 18 12:55:11 EDT 2023
% 0.12/0.34 % CPUTime :
% 0.34/1.39
% 0.34/1.39 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.34/1.39 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.34/1.39 %-----------------------------------------------------
% 0.34/1.39 ncf(matrix, plain, [(130 ^ _18565) ^ [] : [-(relation(128 ^ []))], (132 ^ _18565) ^ [] : [-(function(128 ^ []))], (134 ^ _18565) ^ [] : [-(finite(relation_dom(128 ^ [])))], (136 ^ _18565) ^ [] : [finite(relation_rng(128 ^ []))], (72 ^ _18565) ^ [] : [true___, -(true___)], (78 ^ _18565) ^ [] : [true___, -(true___)], (84 ^ _18565) ^ [] : [true___, -(true___)], (90 ^ _18565) ^ [_21350, _21352] : [-(finite(relation_image(_21352, _21350))), relation(_21352), function(_21352), finite(_21350)], (105 ^ _18565) ^ [] : [-(relation(103 ^ []))], (107 ^ _18565) ^ [] : [-(function(103 ^ []))], (109 ^ _18565) ^ [_21871] : [relation(_21871), -(relation_image(_21871, relation_dom(_21871)) = relation_rng(_21871))], (115 ^ _18565) ^ [_22067, _22069] : [relation(_22067), function(_22067), finite(_22069), -(finite(relation_image(_22067, _22069)))], (50 ^ _18565) ^ [_20236, _20238, _20240, _20242] : [-(relation_image(_20242, _20238) = relation_image(_20240, _20236)), _20242 = _20240, _20238 = _20236], (60 ^ _18565) ^ [_20567, _20569] : [_20569 = _20567, -(relation_dom(_20569) = relation_dom(_20567))], (66 ^ _18565) ^ [_20765, _20767] : [_20767 = _20765, -(relation_rng(_20767) = relation_rng(_20765))], (2 ^ _18565) ^ [_18709] : [-(_18709 = _18709)], (4 ^ _18565) ^ [_18816, _18818] : [_18818 = _18816, -(_18816 = _18818)], (10 ^ _18565) ^ [_19020, _19022, _19024] : [-(_19024 = _19020), _19024 = _19022, _19022 = _19020], (20 ^ _18565) ^ [_19333, _19335] : [-(relation(_19333)), _19335 = _19333, relation(_19335)], (30 ^ _18565) ^ [_19628, _19630] : [-(function(_19628)), _19630 = _19628, function(_19630)], (40 ^ _18565) ^ [_19903, _19905] : [-(finite(_19903)), _19905 = _19903, finite(_19905)]], input).
% 0.34/1.39 ncf('1',plain,[finite(relation_rng(128 ^ []))],start(136 ^ 0)).
% 0.34/1.39 ncf('1.1',plain,[-(finite(relation_rng(128 ^ []))), relation_image(128 ^ [], relation_dom(128 ^ [])) = relation_rng(128 ^ []), finite(relation_image(128 ^ [], relation_dom(128 ^ [])))],extension(40 ^ 1,bind([[_19903, _19905], [relation_rng(128 ^ []), relation_image(128 ^ [], relation_dom(128 ^ []))]]))).
% 0.34/1.39 ncf('1.1.1',plain,[-(relation_image(128 ^ [], relation_dom(128 ^ [])) = relation_rng(128 ^ [])), relation(128 ^ [])],extension(109 ^ 2,bind([[_21871], [128 ^ []]]))).
% 0.34/1.39 ncf('1.1.1.1',plain,[-(relation(128 ^ []))],extension(130 ^ 3)).
% 0.34/1.39 ncf('1.1.2',plain,[-(finite(relation_image(128 ^ [], relation_dom(128 ^ [])))), relation(128 ^ []), function(128 ^ []), finite(relation_dom(128 ^ []))],extension(90 ^ 2,bind([[_21350, _21352], [relation_dom(128 ^ []), 128 ^ []]]))).
% 0.34/1.39 ncf('1.1.2.1',plain,[-(relation(128 ^ []))],extension(130 ^ 3)).
% 0.34/1.39 ncf('1.1.2.2',plain,[-(function(128 ^ []))],extension(132 ^ 3)).
% 0.34/1.39 ncf('1.1.2.3',plain,[-(finite(relation_dom(128 ^ [])))],extension(134 ^ 3)).
% 0.34/1.39 %-----------------------------------------------------
% 0.34/1.39 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------