%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NLP081+1 : TPTP v8.1.2. Released v2.4.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 11:36:57 EDT 2023
% Result : Theorem 0.35s 1.38s
% Output : Proof 0.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : NLP081+1 : TPTP v8.1.2. Released v2.4.0.
% 0.06/0.12 % Command : nanocop.sh %s %d
% 0.12/0.33 % Computer : n015.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 18 15:15:52 EDT 2023
% 0.12/0.34 % CPUTime :
% 0.35/1.38
% 0.35/1.38 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.35/1.38 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.35/1.38 %-----------------------------------------------------
% 0.35/1.38 ncf(matrix, plain, [(2 ^ _261614) ^ [] : [4 ^ _261614 : [(5 ^ _261614) ^ [] : [-(actual_world(3 ^ []))], (13 ^ _261614) ^ [] : [-(male(3 ^ [], 6 ^ []))], (15 ^ _261614) ^ [] : [-(man(3 ^ [], 6 ^ []))], (17 ^ _261614) ^ [] : [-(of(3 ^ [], 7 ^ [], 6 ^ []))], (19 ^ _261614) ^ [] : [-(cannon(3 ^ [], 7 ^ []))], (21 ^ _261614) ^ [_263468] : [member(3 ^ [], _263468, 8 ^ []), 25 ^ _261614 : [(26 ^ _261614) ^ [] : [-(event(3 ^ [], 24 ^ [_263468]))], (28 ^ _261614) ^ [] : [-(agent(3 ^ [], 24 ^ [_263468], 6 ^ []))], (30 ^ _261614) ^ [] : [-(patient(3 ^ [], 24 ^ [_263468], _263468))], (32 ^ _261614) ^ [] : [-(present(3 ^ [], 24 ^ [_263468]))], (34 ^ _261614) ^ [] : [-(nonreflexive(3 ^ [], 24 ^ [_263468]))], (36 ^ _261614) ^ [] : [-(fire(3 ^ [], 24 ^ [_263468]))], (38 ^ _261614) ^ [] : [-(from_loc(3 ^ [], 24 ^ [_263468], 7 ^ []))]]], (40 ^ _261614) ^ [] : [-(six(3 ^ [], 8 ^ []))], (42 ^ _261614) ^ [] : [-(group(3 ^ [], 8 ^ []))], (50 ^ _261614) ^ [] : [-(revenge(3 ^ [], 9 ^ []))], (52 ^ _261614) ^ [] : [-(cry(3 ^ [], 10 ^ []))], (54 ^ _261614) ^ [] : [-(event(3 ^ [], 11 ^ []))], (56 ^ _261614) ^ [] : [-(agent(3 ^ [], 11 ^ [], 6 ^ []))], (58 ^ _261614) ^ [] : [-(patient(3 ^ [], 11 ^ [], 10 ^ []))], (60 ^ _261614) ^ [] : [-(present(3 ^ [], 11 ^ []))], (62 ^ _261614) ^ [] : [-(nonreflexive(3 ^ [], 11 ^ []))], (64 ^ _261614) ^ [] : [-(scream(3 ^ [], 11 ^ []))], (66 ^ _261614) ^ [] : [-(of(3 ^ [], 11 ^ [], 9 ^ []))], (44 ^ _261614) ^ [_264325] : [member(3 ^ [], _264325, 8 ^ []), -(shot(3 ^ [], _264325))], (68 ^ _261614) ^ [_265004] : [actual_world(_265004), 71 ^ _261614 : [(72 ^ _261614) ^ [_265392, _265394, _265396, _265398, _265400, _265402] : [male(_265004, _265402), man(_265004, _265402), of(_265004, _265400, _265402), cannon(_265004, _265400), 90 ^ _261614 : [(91 ^ _261614) ^ [] : [-(member(_265004, 89 ^ [_265004, _265392, _265394, _265396, _265398, _265400, _265402], _265398))], (93 ^ _261614) ^ [_266254] : [event(_265004, _266254), agent(_265004, _266254, _265402), patient(_265004, _266254, 89 ^ [_265004, _265392, _265394, _265396, _265398, _265400, _265402]), present(_265004, _266254), nonreflexive(_265004, _266254), fire(_265004, _266254), from_loc(_265004, _266254, _265400)]], six(_265004, _265398), group(_265004, _265398), 129 ^ _261614 : [(130 ^ _261614) ^ [] : [-(member(_265004, 128 ^ [_265004, _265392, _265394, _265396, _265398, _265400, _265402], _265398))], (132 ^ _261614) ^ [] : [shot(_265004, 128 ^ [_265004, _265392, _265394, _265396, _265398, _265400, _265402])]], cry(_265004, _265396), revenge(_265004, _265394), event(_265004, _265392), agent(_265004, _265392, _265402), patient(_265004, _265392, _265396), present(_265004, _265392), nonreflexive(_265004, _265392), scream(_265004, _265392), of(_265004, _265392, _265394)]]]], 168 ^ _261614 : [(169 ^ _261614) ^ [] : [-(actual_world(167 ^ []))], (177 ^ _261614) ^ [] : [-(male(167 ^ [], 170 ^ []))], (179 ^ _261614) ^ [] : [-(man(167 ^ [], 170 ^ []))], (181 ^ _261614) ^ [] : [-(of(167 ^ [], 171 ^ [], 170 ^ []))], (183 ^ _261614) ^ [] : [-(cannon(167 ^ [], 171 ^ []))], (185 ^ _261614) ^ [_270290] : [member(167 ^ [], _270290, 172 ^ []), 189 ^ _261614 : [(190 ^ _261614) ^ [] : [-(event(167 ^ [], 188 ^ [_270290]))], (192 ^ _261614) ^ [] : [-(agent(167 ^ [], 188 ^ [_270290], 170 ^ []))], (194 ^ _261614) ^ [] : [-(patient(167 ^ [], 188 ^ [_270290], _270290))], (196 ^ _261614) ^ [] : [-(present(167 ^ [], 188 ^ [_270290]))], (198 ^ _261614) ^ [] : [-(nonreflexive(167 ^ [], 188 ^ [_270290]))], (200 ^ _261614) ^ [] : [-(fire(167 ^ [], 188 ^ [_270290]))], (202 ^ _261614) ^ [] : [-(from_loc(167 ^ [], 188 ^ [_270290], 171 ^ []))]]], (204 ^ _261614) ^ [] : [-(six(167 ^ [], 172 ^ []))], (206 ^ _261614) ^ [] : [-(group(167 ^ [], 172 ^ []))], (214 ^ _261614) ^ [] : [-(cry(167 ^ [], 173 ^ []))], (216 ^ _261614) ^ [] : [-(revenge(167 ^ [], 174 ^ []))], (218 ^ _261614) ^ [] : [-(event(167 ^ [], 175 ^ []))], (220 ^ _261614) ^ [] : [-(agent(167 ^ [], 175 ^ [], 170 ^ []))], (222 ^ _261614) ^ [] : [-(patient(167 ^ [], 175 ^ [], 173 ^ []))], (224 ^ _261614) ^ [] : [-(present(167 ^ [], 175 ^ []))], (226 ^ _261614) ^ [] : [-(nonreflexive(167 ^ [], 175 ^ []))], (228 ^ _261614) ^ [] : [-(scream(167 ^ [], 175 ^ []))], (230 ^ _261614) ^ [] : [-(of(167 ^ [], 175 ^ [], 174 ^ []))], (208 ^ _261614) ^ [_271147] : [member(167 ^ [], _271147, 172 ^ []), -(shot(167 ^ [], _271147))], (232 ^ _261614) ^ [_271826] : [actual_world(_271826), 235 ^ _261614 : [(236 ^ _261614) ^ [_272214, _272216, _272218, _272220, _272222, _272224] : [male(_271826, _272224), man(_271826, _272224), of(_271826, _272222, _272224), cannon(_271826, _272222), 254 ^ _261614 : [(255 ^ _261614) ^ [] : [-(member(_271826, 253 ^ [_271826, _272214, _272216, _272218, _272220, _272222, _272224], _272220))], (257 ^ _261614) ^ [_273076] : [event(_271826, _273076), agent(_271826, _273076, _272224), patient(_271826, _273076, 253 ^ [_271826, _272214, _272216, _272218, _272220, _272222, _272224]), present(_271826, _273076), nonreflexive(_271826, _273076), fire(_271826, _273076), from_loc(_271826, _273076, _272222)]], six(_271826, _272220), group(_271826, _272220), 293 ^ _261614 : [(294 ^ _261614) ^ [] : [-(member(_271826, 292 ^ [_271826, _272214, _272216, _272218, _272220, _272222, _272224], _272220))], (296 ^ _261614) ^ [] : [shot(_271826, 292 ^ [_271826, _272214, _272216, _272218, _272220, _272222, _272224])]], revenge(_271826, _272218), cry(_271826, _272216), event(_271826, _272214), agent(_271826, _272214, _272224), patient(_271826, _272214, _272216), present(_271826, _272214), nonreflexive(_271826, _272214), scream(_271826, _272214), of(_271826, _272214, _272218)]]]]]], input).
% 0.35/1.38 ncf('1',plain,[68 : actual_world(3 ^ []), 72 : male(3 ^ [], 6 ^ []), 72 : man(3 ^ [], 6 ^ []), 72 : of(3 ^ [], 7 ^ [], 6 ^ []), 72 : cannon(3 ^ [], 7 ^ []), 93 : event(3 ^ [], 24 ^ [89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]]), 93 : agent(3 ^ [], 24 ^ [89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]], 6 ^ []), 93 : patient(3 ^ [], 24 ^ [89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]], 89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]), 93 : present(3 ^ [], 24 ^ [89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]]), 93 : nonreflexive(3 ^ [], 24 ^ [89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]]), 93 : fire(3 ^ [], 24 ^ [89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]]), 93 : from_loc(3 ^ [], 24 ^ [89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]], 7 ^ []), 93 : six(3 ^ [], 8 ^ []), 93 : group(3 ^ [], 8 ^ []), 132 : shot(3 ^ [], 128 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]), 132 : cry(3 ^ [], 10 ^ []), 132 : revenge(3 ^ [], 9 ^ []), 132 : event(3 ^ [], 11 ^ []), 132 : agent(3 ^ [], 11 ^ [], 6 ^ []), 132 : patient(3 ^ [], 11 ^ [], 10 ^ []), 132 : present(3 ^ [], 11 ^ []), 132 : nonreflexive(3 ^ [], 11 ^ []), 132 : scream(3 ^ [], 11 ^ []), 132 : of(3 ^ [], 11 ^ [], 9 ^ []), 232 : actual_world(167 ^ []), 236 : male(167 ^ [], 170 ^ []), 236 : man(167 ^ [], 170 ^ []), 236 : of(167 ^ [], 171 ^ [], 170 ^ []), 236 : cannon(167 ^ [], 171 ^ []), 257 : event(167 ^ [], 188 ^ [253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []]]), 257 : agent(167 ^ [], 188 ^ [253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []]], 170 ^ []), 257 : patient(167 ^ [], 188 ^ [253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []]], 253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []]), 257 : present(167 ^ [], 188 ^ [253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []]]), 257 : nonreflexive(167 ^ [], 188 ^ [253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []]]), 257 : fire(167 ^ [], 188 ^ [253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []]]), 257 : from_loc(167 ^ [], 188 ^ [253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []]], 171 ^ []), 257 : six(167 ^ [], 172 ^ []), 257 : group(167 ^ [], 172 ^ []), 296 : shot(167 ^ [], 292 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []]), 296 : revenge(167 ^ [], 174 ^ []), 296 : cry(167 ^ [], 173 ^ []), 296 : event(167 ^ [], 175 ^ []), 296 : agent(167 ^ [], 175 ^ [], 170 ^ []), 296 : patient(167 ^ [], 175 ^ [], 173 ^ []), 296 : present(167 ^ [], 175 ^ []), 296 : nonreflexive(167 ^ [], 175 ^ []), 296 : scream(167 ^ [], 175 ^ []), 296 : of(167 ^ [], 175 ^ [], 174 ^ [])],start(2 ^ 0,bind([[_265004, _265392, _265394, _265396, _265398, _265400, _265402, _266254, _271826, _272214, _272216, _272218, _272220, _272222, _272224, _273076], [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ [], 24 ^ [89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]], 167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ [], 188 ^ [253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []]]]]))).
% 0.35/1.38 ncf('1.1',plain,[-(actual_world(3 ^ []))],extension(5 ^ 3)).
% 0.35/1.38 ncf('1.2',plain,[-(male(3 ^ [], 6 ^ []))],extension(13 ^ 5)).
% 0.35/1.38 ncf('1.3',plain,[-(man(3 ^ [], 6 ^ []))],extension(15 ^ 5)).
% 0.35/1.38 ncf('1.4',plain,[-(of(3 ^ [], 7 ^ [], 6 ^ []))],extension(17 ^ 5)).
% 0.35/1.38 ncf('1.5',plain,[-(cannon(3 ^ [], 7 ^ []))],extension(19 ^ 5)).
% 0.35/1.38 ncf('1.6',plain,[-(event(3 ^ [], 24 ^ [89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]])), member(3 ^ [], 89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 8 ^ [])],extension(21 ^ 7,bind([[_263468], [89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]]]))).
% 0.35/1.38 ncf('1.6.1',plain,[-(member(3 ^ [], 89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 8 ^ []))],extension(91 ^ 8)).
% 0.35/1.38 ncf('1.7',plain,[-(agent(3 ^ [], 24 ^ [89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]], 6 ^ [])), member(3 ^ [], 89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 8 ^ [])],extension(21 ^ 7,bind([[_263468], [89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]]]))).
% 0.35/1.38 ncf('1.7.1',plain,[-(member(3 ^ [], 89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 8 ^ []))],extension(91 ^ 8)).
% 0.35/1.38 ncf('1.8',plain,[-(patient(3 ^ [], 24 ^ [89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]], 89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []])), member(3 ^ [], 89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 8 ^ [])],extension(21 ^ 7,bind([[_263468], [89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]]]))).
% 0.35/1.38 ncf('1.8.1',plain,[-(member(3 ^ [], 89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 8 ^ []))],extension(91 ^ 8)).
% 0.35/1.38 ncf('1.9',plain,[-(present(3 ^ [], 24 ^ [89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]])), member(3 ^ [], 89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 8 ^ [])],extension(21 ^ 7,bind([[_263468], [89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]]]))).
% 0.35/1.38 ncf('1.9.1',plain,[-(member(3 ^ [], 89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 8 ^ []))],extension(91 ^ 8)).
% 0.35/1.38 ncf('1.10',plain,[-(nonreflexive(3 ^ [], 24 ^ [89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]])), member(3 ^ [], 89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 8 ^ [])],extension(21 ^ 7,bind([[_263468], [89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]]]))).
% 0.35/1.38 ncf('1.10.1',plain,[-(member(3 ^ [], 89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 8 ^ []))],extension(91 ^ 8)).
% 0.35/1.38 ncf('1.11',plain,[-(fire(3 ^ [], 24 ^ [89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]])), member(3 ^ [], 89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 8 ^ [])],extension(21 ^ 7,bind([[_263468], [89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]]]))).
% 0.35/1.38 ncf('1.11.1',plain,[-(member(3 ^ [], 89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 8 ^ []))],extension(91 ^ 8)).
% 0.35/1.38 ncf('1.12',plain,[-(from_loc(3 ^ [], 24 ^ [89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]], 7 ^ [])), member(3 ^ [], 89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 8 ^ [])],extension(21 ^ 7,bind([[_263468], [89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]]]))).
% 0.35/1.38 ncf('1.12.1',plain,[-(member(3 ^ [], 89 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 8 ^ []))],extension(91 ^ 8)).
% 0.35/1.38 ncf('1.13',plain,[-(six(3 ^ [], 8 ^ []))],extension(40 ^ 5)).
% 0.35/1.38 ncf('1.14',plain,[-(group(3 ^ [], 8 ^ []))],extension(42 ^ 5)).
% 0.35/1.38 ncf('1.15',plain,[-(shot(3 ^ [], 128 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []])), member(3 ^ [], 128 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 8 ^ [])],extension(44 ^ 7,bind([[_264325], [128 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]]]))).
% 0.35/1.38 ncf('1.15.1',plain,[-(member(3 ^ [], 128 ^ [3 ^ [], 11 ^ [], 9 ^ [], 10 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 8 ^ []))],extension(130 ^ 8)).
% 0.35/1.38 ncf('1.16',plain,[-(cry(3 ^ [], 10 ^ []))],extension(52 ^ 5)).
% 0.35/1.38 ncf('1.17',plain,[-(revenge(3 ^ [], 9 ^ []))],extension(50 ^ 5)).
% 0.35/1.38 ncf('1.18',plain,[-(event(3 ^ [], 11 ^ []))],extension(54 ^ 5)).
% 0.35/1.38 ncf('1.19',plain,[-(agent(3 ^ [], 11 ^ [], 6 ^ []))],extension(56 ^ 5)).
% 0.35/1.38 ncf('1.20',plain,[-(patient(3 ^ [], 11 ^ [], 10 ^ []))],extension(58 ^ 5)).
% 0.35/1.38 ncf('1.21',plain,[-(present(3 ^ [], 11 ^ []))],extension(60 ^ 5)).
% 0.35/1.38 ncf('1.22',plain,[-(nonreflexive(3 ^ [], 11 ^ []))],extension(62 ^ 5)).
% 0.35/1.38 ncf('1.23',plain,[-(scream(3 ^ [], 11 ^ []))],extension(64 ^ 5)).
% 0.35/1.38 ncf('1.24',plain,[-(of(3 ^ [], 11 ^ [], 9 ^ []))],extension(66 ^ 5)).
% 0.35/1.38 ncf('1.25',plain,[-(actual_world(167 ^ []))],extension(169 ^ 3)).
% 0.35/1.38 ncf('1.26',plain,[-(male(167 ^ [], 170 ^ []))],extension(177 ^ 5)).
% 0.35/1.38 ncf('1.27',plain,[-(man(167 ^ [], 170 ^ []))],extension(179 ^ 5)).
% 0.35/1.38 ncf('1.28',plain,[-(of(167 ^ [], 171 ^ [], 170 ^ []))],extension(181 ^ 5)).
% 0.35/1.38 ncf('1.29',plain,[-(cannon(167 ^ [], 171 ^ []))],extension(183 ^ 5)).
% 0.35/1.38 ncf('1.30',plain,[-(event(167 ^ [], 188 ^ [253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []]])), member(167 ^ [], 253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []], 172 ^ [])],extension(185 ^ 7,bind([[_270290], [253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []]]]))).
% 0.35/1.38 ncf('1.30.1',plain,[-(member(167 ^ [], 253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []], 172 ^ []))],extension(255 ^ 8)).
% 0.35/1.38 ncf('1.31',plain,[-(agent(167 ^ [], 188 ^ [253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []]], 170 ^ [])), member(167 ^ [], 253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []], 172 ^ [])],extension(185 ^ 7,bind([[_270290], [253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []]]]))).
% 0.35/1.38 ncf('1.31.1',plain,[-(member(167 ^ [], 253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []], 172 ^ []))],extension(255 ^ 8)).
% 0.35/1.38 ncf('1.32',plain,[-(patient(167 ^ [], 188 ^ [253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []]], 253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []])), member(167 ^ [], 253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []], 172 ^ [])],extension(185 ^ 7,bind([[_270290], [253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []]]]))).
% 0.35/1.38 ncf('1.32.1',plain,[-(member(167 ^ [], 253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []], 172 ^ []))],extension(255 ^ 8)).
% 0.35/1.38 ncf('1.33',plain,[-(present(167 ^ [], 188 ^ [253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []]])), member(167 ^ [], 253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []], 172 ^ [])],extension(185 ^ 7,bind([[_270290], [253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []]]]))).
% 0.35/1.38 ncf('1.33.1',plain,[-(member(167 ^ [], 253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []], 172 ^ []))],extension(255 ^ 8)).
% 0.35/1.38 ncf('1.34',plain,[-(nonreflexive(167 ^ [], 188 ^ [253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []]])), member(167 ^ [], 253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []], 172 ^ [])],extension(185 ^ 7,bind([[_270290], [253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []]]]))).
% 0.35/1.38 ncf('1.34.1',plain,[-(member(167 ^ [], 253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []], 172 ^ []))],extension(255 ^ 8)).
% 0.35/1.38 ncf('1.35',plain,[-(fire(167 ^ [], 188 ^ [253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []]])), member(167 ^ [], 253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []], 172 ^ [])],extension(185 ^ 7,bind([[_270290], [253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []]]]))).
% 0.35/1.38 ncf('1.35.1',plain,[-(member(167 ^ [], 253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []], 172 ^ []))],extension(255 ^ 8)).
% 0.35/1.38 ncf('1.36',plain,[-(from_loc(167 ^ [], 188 ^ [253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []]], 171 ^ [])), member(167 ^ [], 253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []], 172 ^ [])],extension(185 ^ 7,bind([[_270290], [253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []]]]))).
% 0.35/1.38 ncf('1.36.1',plain,[-(member(167 ^ [], 253 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []], 172 ^ []))],extension(255 ^ 8)).
% 0.35/1.38 ncf('1.37',plain,[-(six(167 ^ [], 172 ^ []))],extension(204 ^ 5)).
% 0.35/1.38 ncf('1.38',plain,[-(group(167 ^ [], 172 ^ []))],extension(206 ^ 5)).
% 0.35/1.38 ncf('1.39',plain,[-(shot(167 ^ [], 292 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []])), member(167 ^ [], 292 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []], 172 ^ [])],extension(208 ^ 7,bind([[_271147], [292 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []]]]))).
% 0.35/1.38 ncf('1.39.1',plain,[-(member(167 ^ [], 292 ^ [167 ^ [], 175 ^ [], 173 ^ [], 174 ^ [], 172 ^ [], 171 ^ [], 170 ^ []], 172 ^ []))],extension(294 ^ 8)).
% 0.35/1.38 ncf('1.40',plain,[-(revenge(167 ^ [], 174 ^ []))],extension(216 ^ 5)).
% 0.35/1.38 ncf('1.41',plain,[-(cry(167 ^ [], 173 ^ []))],extension(214 ^ 5)).
% 0.35/1.38 ncf('1.42',plain,[-(event(167 ^ [], 175 ^ []))],extension(218 ^ 5)).
% 0.35/1.38 ncf('1.43',plain,[-(agent(167 ^ [], 175 ^ [], 170 ^ []))],extension(220 ^ 5)).
% 0.35/1.38 ncf('1.44',plain,[-(patient(167 ^ [], 175 ^ [], 173 ^ []))],extension(222 ^ 5)).
% 0.35/1.38 ncf('1.45',plain,[-(present(167 ^ [], 175 ^ []))],extension(224 ^ 5)).
% 0.35/1.38 ncf('1.46',plain,[-(nonreflexive(167 ^ [], 175 ^ []))],extension(226 ^ 5)).
% 0.35/1.38 ncf('1.47',plain,[-(scream(167 ^ [], 175 ^ []))],extension(228 ^ 5)).
% 0.35/1.38 ncf('1.48',plain,[-(of(167 ^ [], 175 ^ [], 174 ^ []))],extension(230 ^ 5)).
% 0.35/1.38 %-----------------------------------------------------
% 0.35/1.38 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------