%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : SWB018+2 : TPTP v8.1.2. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n020.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:08:32 EDT 2023
% Result : Theorem 0.18s 1.32s
% Output : Proof 0.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.08 % Problem : SWB018+2 : TPTP v8.1.2. Released v5.2.0.
% 0.07/0.09 % Command : nanocop.sh %s %d
% 0.08/0.27 % Computer : n020.cluster.edu
% 0.08/0.27 % Model : x86_64 x86_64
% 0.08/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.27 % Memory : 8042.1875MB
% 0.08/0.27 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.27 % CPULimit : 300
% 0.08/0.27 % WCLimit : 300
% 0.08/0.27 % DateTime : Thu May 18 20:56:02 EDT 2023
% 0.08/0.27 % CPUTime :
% 0.18/1.32
% 0.18/1.32 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.18/1.32 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/1.32 %-----------------------------------------------------
% 0.18/1.32 ncf(matrix, plain, [(90 ^ _15421) ^ [] : [iext(uri_rdf_type, uri_ex_u, uri_ex_Person)], (52 ^ _15421) ^ [_17239, _17241] : [iext(uri_rdf_type, _17241, _17239), -(icext(_17239, _17241))], (58 ^ _15421) ^ [_17403, _17405] : [icext(_17403, _17405), -(iext(uri_rdf_type, _17405, _17403))], (64 ^ _15421) ^ [_17645, _17647, _17649, _17651] : [-(icext(_17649, _17647)), iext(uri_rdfs_domain, _17651, _17649), iext(_17651, _17647, _17645)], (86 ^ _15421) ^ [] : [-(iext(uri_rdfs_domain, uri_owl_sameAs, uri_ex_Person))], (88 ^ _15421) ^ [] : [-(iext(uri_owl_sameAs, uri_ex_w, uri_ex_u))], (74 ^ _15421) ^ [_17997, _17999] : [iext(uri_owl_sameAs, _17999, _17997), -(_17999 = _17997)], (80 ^ _15421) ^ [_18161, _18163] : [_18163 = _18161, -(iext(uri_owl_sameAs, _18163, _18161))], (2 ^ _15421) ^ [_15545] : [-(_15545 = _15545)], (4 ^ _15421) ^ [_15652, _15654] : [_15654 = _15652, -(_15652 = _15654)], (10 ^ _15421) ^ [_15856, _15858, _15860] : [-(_15860 = _15856), _15860 = _15858, _15858 = _15856], (20 ^ _15421) ^ [_16197, _16199, _16201, _16203] : [-(icext(_16201, _16197)), icext(_16203, _16199), _16203 = _16201, _16199 = _16197], (34 ^ _15421) ^ [_16649, _16651, _16653, _16655, _16657, _16659] : [-(iext(_16657, _16653, _16649)), iext(_16659, _16655, _16651), _16659 = _16657, _16655 = _16653, _16651 = _16649]], input).
% 0.18/1.32 ncf('1',plain,[iext(uri_rdf_type, uri_ex_u, uri_ex_Person)],start(90 ^ 0)).
% 0.18/1.32 ncf('1.1',plain,[-(iext(uri_rdf_type, uri_ex_u, uri_ex_Person)), icext(uri_ex_Person, uri_ex_u)],extension(58 ^ 1,bind([[_17403, _17405], [uri_ex_Person, uri_ex_u]]))).
% 0.18/1.32 ncf('1.1.1',plain,[-(icext(uri_ex_Person, uri_ex_u)), icext(uri_ex_Person, uri_ex_w), uri_ex_Person = uri_ex_Person, uri_ex_w = uri_ex_u],extension(20 ^ 2,bind([[_16197, _16199, _16201, _16203], [uri_ex_u, uri_ex_w, uri_ex_Person, uri_ex_Person]]))).
% 0.18/1.32 ncf('1.1.1.1',plain,[-(icext(uri_ex_Person, uri_ex_w)), iext(uri_rdfs_domain, uri_owl_sameAs, uri_ex_Person), iext(uri_owl_sameAs, uri_ex_w, uri_ex_u)],extension(64 ^ 3,bind([[_17645, _17647, _17649, _17651], [uri_ex_u, uri_ex_w, uri_ex_Person, uri_owl_sameAs]]))).
% 0.18/1.32 ncf('1.1.1.1.1',plain,[-(iext(uri_rdfs_domain, uri_owl_sameAs, uri_ex_Person))],extension(86 ^ 4)).
% 0.18/1.32 ncf('1.1.1.1.2',plain,[-(iext(uri_owl_sameAs, uri_ex_w, uri_ex_u))],extension(88 ^ 4)).
% 0.18/1.32 ncf('1.1.1.2',plain,[-(uri_ex_Person = uri_ex_Person)],extension(2 ^ 3,bind([[_15545], [uri_ex_Person]]))).
% 0.18/1.32 ncf('1.1.1.3',plain,[-(uri_ex_w = uri_ex_u), iext(uri_owl_sameAs, uri_ex_w, uri_ex_u)],extension(74 ^ 3,bind([[_17997, _17999], [uri_ex_u, uri_ex_w]]))).
% 0.18/1.32 ncf('1.1.1.3.1',plain,[-(iext(uri_owl_sameAs, uri_ex_w, uri_ex_u))],extension(88 ^ 4)).
% 0.18/1.32 %-----------------------------------------------------
% 0.18/1.32 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------