%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : PHI011+1 : TPTP v8.1.2. Released v7.2.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:46:43 EDT 2023
% Result : Theorem 0.36s 1.39s
% Output : Proof 0.36s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : PHI011+1 : TPTP v8.1.2. Released v7.2.0.
% 0.07/0.12 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n014.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 21:03:27 EDT 2023
% 0.12/0.34 % CPUTime :
% 0.36/1.39
% 0.36/1.39 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.36/1.39 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/1.39 %-----------------------------------------------------
% 0.36/1.39 ncf(matrix, plain, [(113 ^ _18175) ^ [] : [-(property(111 ^ []))], (116 ^ _18175) ^ [] : [-(object(114 ^ []))], (118 ^ _18175) ^ [] : [-(is_the(114 ^ [], 111 ^ []))], (121 ^ _18175) ^ [] : [-(object(119 ^ []))], (123 ^ _18175) ^ [] : [-(is_the(119 ^ [], 111 ^ []))], (125 ^ _18175) ^ [] : [exemplifies_property(111 ^ [], 119 ^ [])], (68 ^ _18175) ^ [_20379] : [object(_20379), property(_20379)], (74 ^ _18175) ^ [_20580, _20582] : [exemplifies_property(_20580, _20582), 77 ^ _18175 : [(78 ^ _18175) ^ [] : [-(property(_20580))], (80 ^ _18175) ^ [] : [-(object(_20582))]]], (82 ^ _18175) ^ [_20861, _20863] : [is_the(_20863, _20861), 85 ^ _18175 : [(86 ^ _18175) ^ [] : [-(property(_20861))], (88 ^ _18175) ^ [] : [-(object(_20863))]]], (90 ^ _18175) ^ [_21136, _21138, _21140] : [object(_21140), property(_21138), object(_21136), -(exemplifies_property(_21138, _21136)), is_the(_21140, _21138), _21140 = _21136], (2 ^ _18175) ^ [_18299] : [-(_18299 = _18299)], (4 ^ _18175) ^ [_18406, _18408] : [_18408 = _18406, -(_18406 = _18408)], (10 ^ _18175) ^ [_18610, _18612, _18614] : [-(_18614 = _18610), _18614 = _18612, _18612 = _18610], (20 ^ _18175) ^ [_18923, _18925] : [-(property(_18923)), _18925 = _18923, property(_18925)], (30 ^ _18175) ^ [_19218, _19220] : [-(object(_19218)), _19220 = _19218, object(_19220)], (40 ^ _18175) ^ [_19541, _19543, _19545, _19547] : [-(is_the(_19545, _19541)), is_the(_19547, _19543), _19547 = _19545, _19543 = _19541], (54 ^ _18175) ^ [_19965, _19967, _19969, _19971] : [-(exemplifies_property(_19969, _19965)), exemplifies_property(_19971, _19967), _19971 = _19969, _19967 = _19965]], input).
% 0.36/1.39 ncf('1',plain,[exemplifies_property(111 ^ [], 119 ^ [])],start(125 ^ 0)).
% 0.36/1.39 ncf('1.1',plain,[-(exemplifies_property(111 ^ [], 119 ^ [])), object(119 ^ []), property(111 ^ []), object(119 ^ []), is_the(119 ^ [], 111 ^ []), 119 ^ [] = 119 ^ []],extension(90 ^ 1,bind([[_21136, _21138, _21140], [119 ^ [], 111 ^ [], 119 ^ []]]))).
% 0.36/1.39 ncf('1.1.1',plain,[-(object(119 ^ []))],extension(121 ^ 2)).
% 0.36/1.39 ncf('1.1.2',plain,[-(property(111 ^ []))],extension(113 ^ 2)).
% 0.36/1.39 ncf('1.1.3',plain,[-(object(119 ^ []))],lemmata('[1].x')).
% 0.36/1.39 ncf('1.1.4',plain,[-(is_the(119 ^ [], 111 ^ []))],extension(123 ^ 2)).
% 0.36/1.39 ncf('1.1.5',plain,[-(119 ^ [] = 119 ^ [])],extension(2 ^ 2,bind([[_18299], [119 ^ []]]))).
% 0.36/1.39 %-----------------------------------------------------
% 0.36/1.39 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------