%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : PHI010+1 : TPTP v8.1.2. Released v7.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n026.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:46:43 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.08/0.13 % Problem : PHI010+1 : TPTP v8.1.2. Released v7.2.0.
% 0.08/0.14 % Command : nanocop.sh %s %d
% 0.14/0.35 % Computer : n026.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 18 21:23:05 EDT 2023
% 0.14/0.35 % CPUTime :
% 0.34/1.39
% 0.34/1.39 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.34/1.39 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.34/1.39 %-----------------------------------------------------
% 0.34/1.39 ncf(matrix, plain, [(155 ^ _23136) ^ [] : [-(object(151 ^ []))], (157 ^ _23136) ^ [] : [-(property(152 ^ []))], (159 ^ _23136) ^ [] : [-(object(153 ^ []))], (161 ^ _23136) ^ [] : [-(is_the(151 ^ [], 152 ^ []))], (163 ^ _23136) ^ [] : [-(151 ^ [] = 153 ^ [])], (165 ^ _23136) ^ [] : [exemplifies_property(152 ^ [], 153 ^ [])], (68 ^ _23136) ^ [_25340] : [object(_25340), property(_25340)], (74 ^ _23136) ^ [_25541, _25543] : [exemplifies_property(_25541, _25543), 77 ^ _23136 : [(78 ^ _23136) ^ [] : [-(property(_25541))], (80 ^ _23136) ^ [] : [-(object(_25543))]]], (82 ^ _23136) ^ [_25822, _25824] : [is_the(_25824, _25822), 85 ^ _23136 : [(86 ^ _23136) ^ [] : [-(property(_25822))], (88 ^ _23136) ^ [] : [-(object(_25824))]]], (90 ^ _23136) ^ [_26097, _26099, _26101] : [property(_26101), object(_26099), object(_26097), 101 ^ _23136 : [(102 ^ _23136) ^ [] : [is_the(_26099, _26101), _26099 = _26097, 110 ^ _23136 : [(111 ^ _23136) ^ [] : [-(object(109 ^ [_26097, _26099, _26101]))], (113 ^ _23136) ^ [] : [-(exemplifies_property(_26101, 109 ^ [_26097, _26099, _26101]))], (125 ^ _23136) ^ [] : [-(109 ^ [_26097, _26099, _26101] = _26097)], (115 ^ _23136) ^ [_26911] : [object(_26911), exemplifies_property(_26101, _26911), -(_26911 = 109 ^ [_26097, _26099, _26101])]]], (127 ^ _23136) ^ [] : [147 ^ _23136 : [(148 ^ _23136) ^ [] : [-(is_the(_26099, _26101))], (150 ^ _23136) ^ [] : [-(_26099 = _26097)]], 128 ^ _23136 : [(129 ^ _23136) ^ [_27324] : [object(_27324), exemplifies_property(_26101, _27324), 139 ^ _23136 : [(140 ^ _23136) ^ [] : [-(object(138 ^ [_26097, _26099, _26101, _27324]))], (142 ^ _23136) ^ [] : [-(exemplifies_property(_26101, 138 ^ [_26097, _26099, _26101, _27324]))], (144 ^ _23136) ^ [] : [138 ^ [_26097, _26099, _26101, _27324] = _27324]], _27324 = _26097]]]]], (2 ^ _23136) ^ [_23260] : [-(_23260 = _23260)], (4 ^ _23136) ^ [_23367, _23369] : [_23369 = _23367, -(_23367 = _23369)], (10 ^ _23136) ^ [_23571, _23573, _23575] : [-(_23575 = _23571), _23575 = _23573, _23573 = _23571], (20 ^ _23136) ^ [_23884, _23886] : [-(property(_23884)), _23886 = _23884, property(_23886)], (30 ^ _23136) ^ [_24179, _24181] : [-(object(_24179)), _24181 = _24179, object(_24181)], (40 ^ _23136) ^ [_24502, _24504, _24506, _24508] : [-(is_the(_24506, _24502)), is_the(_24508, _24504), _24508 = _24506, _24504 = _24502], (54 ^ _23136) ^ [_24926, _24928, _24930, _24932] : [-(exemplifies_property(_24930, _24926)), exemplifies_property(_24932, _24928), _24932 = _24930, _24928 = _24926]], input).
% 0.34/1.39 ncf('1',plain,[exemplifies_property(152 ^ [], 153 ^ [])],start(165 ^ 0)).
% 0.34/1.39 ncf('1.1',plain,[-(exemplifies_property(152 ^ [], 153 ^ [])), exemplifies_property(152 ^ [], 109 ^ [153 ^ [], 151 ^ [], 152 ^ []]), 152 ^ [] = 152 ^ [], 109 ^ [153 ^ [], 151 ^ [], 152 ^ []] = 153 ^ []],extension(54 ^ 1,bind([[_24926, _24928, _24930, _24932], [153 ^ [], 109 ^ [153 ^ [], 151 ^ [], 152 ^ []], 152 ^ [], 152 ^ []]]))).
% 0.34/1.39 ncf('1.1.1',plain,[-(exemplifies_property(152 ^ [], 109 ^ [153 ^ [], 151 ^ [], 152 ^ []])), 102 : is_the(151 ^ [], 152 ^ []), 102 : 151 ^ [] = 153 ^ [], 102 : property(152 ^ []), 102 : object(151 ^ []), 102 : object(153 ^ [])],extension(90 ^ 2,bind([[_26097, _26099, _26101], [153 ^ [], 151 ^ [], 152 ^ []]]))).
% 0.34/1.39 ncf('1.1.1.1',plain,[-(is_the(151 ^ [], 152 ^ []))],extension(161 ^ 5)).
% 0.34/1.39 ncf('1.1.1.2',plain,[-(151 ^ [] = 153 ^ [])],extension(163 ^ 5)).
% 0.34/1.39 ncf('1.1.1.3',plain,[-(property(152 ^ []))],extension(157 ^ 3)).
% 0.34/1.39 ncf('1.1.1.4',plain,[-(object(151 ^ []))],extension(155 ^ 3)).
% 0.34/1.39 ncf('1.1.1.5',plain,[-(object(153 ^ []))],extension(159 ^ 3)).
% 0.34/1.39 ncf('1.1.2',plain,[-(152 ^ [] = 152 ^ [])],extension(2 ^ 2,bind([[_23260], [152 ^ []]]))).
% 0.34/1.39 ncf('1.1.3',plain,[-(109 ^ [153 ^ [], 151 ^ [], 152 ^ []] = 153 ^ []), 102 : is_the(151 ^ [], 152 ^ []), 102 : 151 ^ [] = 153 ^ [], 102 : property(152 ^ []), 102 : object(151 ^ []), 102 : object(153 ^ [])],extension(90 ^ 2,bind([[_26097, _26099, _26101], [153 ^ [], 151 ^ [], 152 ^ []]]))).
% 0.34/1.39 ncf('1.1.3.1',plain,[-(is_the(151 ^ [], 152 ^ []))],extension(161 ^ 5)).
% 0.34/1.39 ncf('1.1.3.2',plain,[-(151 ^ [] = 153 ^ [])],extension(163 ^ 5)).
% 0.34/1.39 ncf('1.1.3.3',plain,[-(property(152 ^ []))],extension(157 ^ 3)).
% 0.34/1.39 ncf('1.1.3.4',plain,[-(object(151 ^ []))],extension(155 ^ 3)).
% 0.34/1.39 ncf('1.1.3.5',plain,[-(object(153 ^ []))],extension(159 ^ 3)).
% 0.34/1.39 %-----------------------------------------------------
% 0.34/1.39 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------