%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SYN550+1 : TPTP v8.1.2. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n015.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:34:16 EDT 2023
% 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.06/0.12 % Problem : SYN550+1 : TPTP v8.1.2. Released v2.2.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n015.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Thu May 18 20:03:22 EDT 2023
% 0.13/0.33 % 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, [(2 ^ _18300) ^ [_18384] : [-(reachable(_18384, _18384))], (4 ^ _18300) ^ [_18485, _18487, _18489] : [-(reachable(_18489, _18485)), reachable(_18489, _18487), reachable(_18487, _18485)], (14 ^ _18300) ^ [] : [16 ^ _18300 : [(17 ^ _18300) ^ [] : [-(reachable(initial_world, 15 ^ []))], (19 ^ _18300) ^ [_18927] : [reachable(15 ^ [], _18927), -(p(_18927))], (25 ^ _18300) ^ [_19097] : [reachable(initial_world, _19097), 29 ^ _18300 : [(30 ^ _18300) ^ [] : [-(reachable(_19097, 28 ^ [_19097]))], (32 ^ _18300) ^ [_19388] : [reachable(28 ^ [_19097], _19388), 36 ^ _18300 : [(37 ^ _18300) ^ [] : [-(reachable(_19388, 35 ^ [_19097, _19388]))], (39 ^ _18300) ^ [] : [p(35 ^ [_19097, _19388])]]]]]], 41 ^ _18300 : [(57 ^ _18300) ^ [_20340] : [reachable(initial_world, _20340), 61 ^ _18300 : [(62 ^ _18300) ^ [] : [-(reachable(_20340, 60 ^ [_20340]))], (64 ^ _18300) ^ [] : [p(60 ^ [_20340])]]], (42 ^ _18300) ^ [] : [-(reachable(initial_world, 40 ^ []))], (44 ^ _18300) ^ [_19876] : [reachable(40 ^ [], _19876), 48 ^ _18300 : [(49 ^ _18300) ^ [] : [-(reachable(_19876, 47 ^ [_19876]))], (51 ^ _18300) ^ [_20145] : [reachable(47 ^ [_19876], _20145), -(p(_20145))]]]]]], input).
% 0.33/1.38 ncf('1',plain,[25 : reachable(initial_world, 15 ^ []), 32 : reachable(28 ^ [15 ^ []], 28 ^ [15 ^ []]), 39 : p(35 ^ [15 ^ [], 28 ^ [15 ^ []]]), 57 : reachable(initial_world, 47 ^ [60 ^ [40 ^ []]]), 64 : p(60 ^ [47 ^ [60 ^ [40 ^ []]]])],start(14 ^ 0,bind([[_19097, _19388, _20340], [15 ^ [], 28 ^ [15 ^ []], 47 ^ [60 ^ [40 ^ []]]]]))).
% 0.33/1.38 ncf('1.1',plain,[-(reachable(initial_world, 15 ^ [])), reachable(initial_world, 15 ^ []), reachable(15 ^ [], 15 ^ [])],extension(4 ^ 3,bind([[_18485, _18487, _18489], [15 ^ [], 15 ^ [], initial_world]]))).
% 0.33/1.38 ncf('1.1.1',plain,[-(reachable(initial_world, 15 ^ [])), reachable(initial_world, 15 ^ []), reachable(15 ^ [], 15 ^ [])],extension(4 ^ 4,bind([[_18485, _18487, _18489], [15 ^ [], 15 ^ [], initial_world]]))).
% 0.33/1.38 ncf('1.1.1.1',plain,[-(reachable(initial_world, 15 ^ []))],extension(17 ^ 5)).
% 0.33/1.38 ncf('1.1.1.2',plain,[-(reachable(15 ^ [], 15 ^ []))],extension(2 ^ 5,bind([[_18384], [15 ^ []]]))).
% 0.33/1.38 ncf('1.1.2',plain,[-(reachable(15 ^ [], 15 ^ []))],extension(2 ^ 4,bind([[_18384], [15 ^ []]]))).
% 0.33/1.38 ncf('1.2',plain,[-(reachable(28 ^ [15 ^ []], 28 ^ [15 ^ []]))],extension(2 ^ 5,bind([[_18384], [28 ^ [15 ^ []]]]))).
% 0.33/1.38 ncf('1.3',plain,[-(p(35 ^ [15 ^ [], 28 ^ [15 ^ []]])), reachable(15 ^ [], 35 ^ [15 ^ [], 28 ^ [15 ^ []]])],extension(19 ^ 7,bind([[_18927], [35 ^ [15 ^ [], 28 ^ [15 ^ []]]]]))).
% 0.33/1.38 ncf('1.3.1',plain,[-(reachable(15 ^ [], 35 ^ [15 ^ [], 28 ^ [15 ^ []]])), reachable(15 ^ [], 28 ^ [15 ^ []]), reachable(28 ^ [15 ^ []], 35 ^ [15 ^ [], 28 ^ [15 ^ []]])],extension(4 ^ 8,bind([[_18485, _18487, _18489], [35 ^ [15 ^ [], 28 ^ [15 ^ []]], 28 ^ [15 ^ []], 15 ^ []]]))).
% 0.33/1.38 ncf('1.3.1.1',plain,[-(reachable(15 ^ [], 28 ^ [15 ^ []]))],extension(30 ^ 9)).
% 0.33/1.38 ncf('1.3.1.2',plain,[-(reachable(28 ^ [15 ^ []], 35 ^ [15 ^ [], 28 ^ [15 ^ []]]))],extension(37 ^ 9)).
% 0.33/1.38 ncf('1.4',plain,[-(reachable(initial_world, 47 ^ [60 ^ [40 ^ []]])), reachable(initial_world, 40 ^ []), reachable(40 ^ [], 47 ^ [60 ^ [40 ^ []]])],extension(4 ^ 3,bind([[_18485, _18487, _18489], [47 ^ [60 ^ [40 ^ []]], 40 ^ [], initial_world]]))).
% 0.33/1.38 ncf('1.4.1',plain,[-(reachable(initial_world, 40 ^ [])), reachable(initial_world, 40 ^ []), reachable(40 ^ [], 40 ^ [])],extension(4 ^ 4,bind([[_18485, _18487, _18489], [40 ^ [], 40 ^ [], initial_world]]))).
% 0.33/1.38 ncf('1.4.1.1',plain,[-(reachable(initial_world, 40 ^ []))],extension(42 ^ 5)).
% 0.33/1.38 ncf('1.4.1.2',plain,[-(reachable(40 ^ [], 40 ^ []))],extension(2 ^ 5,bind([[_18384], [40 ^ []]]))).
% 0.33/1.38 ncf('1.4.2',plain,[-(reachable(40 ^ [], 47 ^ [60 ^ [40 ^ []]])), reachable(40 ^ [], 60 ^ [40 ^ []]), reachable(60 ^ [40 ^ []], 47 ^ [60 ^ [40 ^ []]])],extension(4 ^ 4,bind([[_18485, _18487, _18489], [47 ^ [60 ^ [40 ^ []]], 60 ^ [40 ^ []], 40 ^ []]]))).
% 0.33/1.38 ncf('1.4.2.1',plain,[-(reachable(40 ^ [], 60 ^ [40 ^ []])), reachable(initial_world, 40 ^ [])],extension(57 ^ 5,bind([[_20340], [40 ^ []]]))).
% 0.33/1.38 ncf('1.4.2.1.1',plain,[-(reachable(initial_world, 40 ^ []))],lemmata('[1].x')).
% 0.33/1.38 ncf('1.4.2.2',plain,[-(reachable(60 ^ [40 ^ []], 47 ^ [60 ^ [40 ^ []]])), reachable(40 ^ [], 60 ^ [40 ^ []])],extension(44 ^ 5,bind([[_19876], [60 ^ [40 ^ []]]]))).
% 0.33/1.38 ncf('1.4.2.2.1',plain,[-(reachable(40 ^ [], 60 ^ [40 ^ []]))],lemmata('[4, 1].x')).
% 0.33/1.38 ncf('1.5',plain,[-(p(60 ^ [47 ^ [60 ^ [40 ^ []]]])), 51 : reachable(47 ^ [60 ^ [40 ^ []]], 60 ^ [47 ^ [60 ^ [40 ^ []]]]), 51 : reachable(40 ^ [], 60 ^ [40 ^ []])],extension(44 ^ 5,bind([[_19876, _20145], [60 ^ [40 ^ []], 60 ^ [47 ^ [60 ^ [40 ^ []]]]]]))).
% 0.33/1.38 ncf('1.5.1',plain,[-(reachable(47 ^ [60 ^ [40 ^ []]], 60 ^ [47 ^ [60 ^ [40 ^ []]]])), reachable(47 ^ [60 ^ [40 ^ []]], 60 ^ [47 ^ [60 ^ [40 ^ []]]]), reachable(60 ^ [47 ^ [60 ^ [40 ^ []]]], 60 ^ [47 ^ [60 ^ [40 ^ []]]])],extension(4 ^ 8,bind([[_18485, _18487, _18489], [60 ^ [47 ^ [60 ^ [40 ^ []]]], 60 ^ [47 ^ [60 ^ [40 ^ []]]], 47 ^ [60 ^ [40 ^ []]]]]))).
% 0.33/1.38 ncf('1.5.1.1',plain,[-(reachable(47 ^ [60 ^ [40 ^ []]], 60 ^ [47 ^ [60 ^ [40 ^ []]]]))],extension(62 ^ 9)).
% 0.33/1.38 ncf('1.5.1.2',plain,[-(reachable(60 ^ [47 ^ [60 ^ [40 ^ []]]], 60 ^ [47 ^ [60 ^ [40 ^ []]]]))],extension(2 ^ 9,bind([[_18384], [60 ^ [47 ^ [60 ^ [40 ^ []]]]]]))).
% 0.33/1.38 ncf('1.5.2',plain,[-(reachable(40 ^ [], 60 ^ [40 ^ []])), reachable(40 ^ [], 60 ^ [40 ^ []]), reachable(60 ^ [40 ^ []], 60 ^ [40 ^ []])],extension(4 ^ 6,bind([[_18485, _18487, _18489], [60 ^ [40 ^ []], 60 ^ [40 ^ []], 40 ^ []]]))).
% 0.33/1.38 ncf('1.5.2.1',plain,[-(reachable(40 ^ [], 60 ^ [40 ^ []])), reachable(initial_world, 40 ^ [])],extension(57 ^ 7,bind([[_20340], [40 ^ []]]))).
% 0.33/1.38 ncf('1.5.2.1.1',plain,[-(reachable(initial_world, 40 ^ []))],extension(42 ^ 8)).
% 0.33/1.38 ncf('1.5.2.2',plain,[-(reachable(60 ^ [40 ^ []], 60 ^ [40 ^ []]))],extension(2 ^ 7,bind([[_18384], [60 ^ [40 ^ []]]]))).
% 0.33/1.38 %-----------------------------------------------------
% 0.33/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------