%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NLP079+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n027.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.37s 1.39s
% Output : Proof 0.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : NLP079+1 : TPTP v8.1.2. Released v2.4.0.
% 0.11/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n027.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 15:28:05 EDT 2023
% 0.18/0.34 % CPUTime :
% 0.37/1.39
% 0.37/1.39 /export/starexec/sandbox2/benchmark/theBenchmark.p is a Theorem
% 0.37/1.39 Start of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/1.39 %-----------------------------------------------------
% 0.37/1.39 ncf(matrix, plain, [(2 ^ _280566) ^ [] : [4 ^ _280566 : [(5 ^ _280566) ^ [] : [-(actual_world(3 ^ []))], (14 ^ _280566) ^ [] : [-(male(3 ^ [], 6 ^ []))], (16 ^ _280566) ^ [] : [-(male(3 ^ [], 7 ^ []))], (18 ^ _280566) ^ [] : [-(man(3 ^ [], 7 ^ []))], (20 ^ _280566) ^ [] : [-(of(3 ^ [], 8 ^ [], 7 ^ []))], (22 ^ _280566) ^ [] : [-(cannon(3 ^ [], 8 ^ []))], (24 ^ _280566) ^ [_282743] : [member(3 ^ [], _282743, 9 ^ []), 28 ^ _280566 : [(29 ^ _280566) ^ [] : [-(event(3 ^ [], 27 ^ [_282743]))], (31 ^ _280566) ^ [] : [-(agent(3 ^ [], 27 ^ [_282743], 7 ^ []))], (33 ^ _280566) ^ [] : [-(patient(3 ^ [], 27 ^ [_282743], _282743))], (35 ^ _280566) ^ [] : [-(present(3 ^ [], 27 ^ [_282743]))], (37 ^ _280566) ^ [] : [-(nonreflexive(3 ^ [], 27 ^ [_282743]))], (39 ^ _280566) ^ [] : [-(fire(3 ^ [], 27 ^ [_282743]))], (41 ^ _280566) ^ [] : [-(from_loc(3 ^ [], 27 ^ [_282743], 8 ^ []))]]], (43 ^ _280566) ^ [] : [-(six(3 ^ [], 9 ^ []))], (45 ^ _280566) ^ [] : [-(group(3 ^ [], 9 ^ []))], (53 ^ _280566) ^ [] : [-(revenge(3 ^ [], 10 ^ []))], (55 ^ _280566) ^ [] : [-(cry(3 ^ [], 11 ^ []))], (57 ^ _280566) ^ [] : [-(event(3 ^ [], 12 ^ []))], (59 ^ _280566) ^ [] : [-(agent(3 ^ [], 12 ^ [], 6 ^ []))], (61 ^ _280566) ^ [] : [-(patient(3 ^ [], 12 ^ [], 11 ^ []))], (63 ^ _280566) ^ [] : [-(present(3 ^ [], 12 ^ []))], (65 ^ _280566) ^ [] : [-(nonreflexive(3 ^ [], 12 ^ []))], (67 ^ _280566) ^ [] : [-(scream(3 ^ [], 12 ^ []))], (69 ^ _280566) ^ [] : [-(of(3 ^ [], 12 ^ [], 10 ^ []))], (47 ^ _280566) ^ [_283600] : [member(3 ^ [], _283600, 9 ^ []), -(shot(3 ^ [], _283600))], (71 ^ _280566) ^ [_284281] : [actual_world(_284281), 74 ^ _280566 : [(75 ^ _280566) ^ [_284694, _284696, _284698, _284700, _284702, _284704, _284706] : [male(_284281, _284706), male(_284281, _284704), man(_284281, _284704), of(_284281, _284702, _284704), cannon(_284281, _284702), 97 ^ _280566 : [(98 ^ _280566) ^ [] : [-(member(_284281, 96 ^ [_284281, _284694, _284696, _284698, _284700, _284702, _284704, _284706], _284700))], (100 ^ _280566) ^ [_285691] : [event(_284281, _285691), agent(_284281, _285691, _284704), patient(_284281, _285691, 96 ^ [_284281, _284694, _284696, _284698, _284700, _284702, _284704, _284706]), present(_284281, _285691), nonreflexive(_284281, _285691), fire(_284281, _285691), from_loc(_284281, _285691, _284702)]], six(_284281, _284700), group(_284281, _284700), 136 ^ _280566 : [(137 ^ _280566) ^ [] : [-(member(_284281, 135 ^ [_284281, _284694, _284696, _284698, _284700, _284702, _284704, _284706], _284700))], (139 ^ _280566) ^ [] : [shot(_284281, 135 ^ [_284281, _284694, _284696, _284698, _284700, _284702, _284704, _284706])]], cry(_284281, _284698), revenge(_284281, _284696), event(_284281, _284694), agent(_284281, _284694, _284706), patient(_284281, _284694, _284698), present(_284281, _284694), nonreflexive(_284281, _284694), scream(_284281, _284694), of(_284281, _284694, _284696)]]]], 175 ^ _280566 : [(176 ^ _280566) ^ [] : [-(actual_world(174 ^ []))], (185 ^ _280566) ^ [] : [-(male(174 ^ [], 177 ^ []))], (187 ^ _280566) ^ [] : [-(male(174 ^ [], 178 ^ []))], (189 ^ _280566) ^ [] : [-(man(174 ^ [], 178 ^ []))], (191 ^ _280566) ^ [] : [-(of(174 ^ [], 179 ^ [], 178 ^ []))], (193 ^ _280566) ^ [] : [-(cannon(174 ^ [], 179 ^ []))], (195 ^ _280566) ^ [_290144] : [member(174 ^ [], _290144, 180 ^ []), 199 ^ _280566 : [(200 ^ _280566) ^ [] : [-(event(174 ^ [], 198 ^ [_290144]))], (202 ^ _280566) ^ [] : [-(agent(174 ^ [], 198 ^ [_290144], 178 ^ []))], (204 ^ _280566) ^ [] : [-(patient(174 ^ [], 198 ^ [_290144], _290144))], (206 ^ _280566) ^ [] : [-(present(174 ^ [], 198 ^ [_290144]))], (208 ^ _280566) ^ [] : [-(nonreflexive(174 ^ [], 198 ^ [_290144]))], (210 ^ _280566) ^ [] : [-(fire(174 ^ [], 198 ^ [_290144]))], (212 ^ _280566) ^ [] : [-(from_loc(174 ^ [], 198 ^ [_290144], 179 ^ []))]]], (214 ^ _280566) ^ [] : [-(six(174 ^ [], 180 ^ []))], (216 ^ _280566) ^ [] : [-(group(174 ^ [], 180 ^ []))], (224 ^ _280566) ^ [] : [-(cry(174 ^ [], 181 ^ []))], (226 ^ _280566) ^ [] : [-(revenge(174 ^ [], 182 ^ []))], (228 ^ _280566) ^ [] : [-(event(174 ^ [], 183 ^ []))], (230 ^ _280566) ^ [] : [-(agent(174 ^ [], 183 ^ [], 177 ^ []))], (232 ^ _280566) ^ [] : [-(patient(174 ^ [], 183 ^ [], 181 ^ []))], (234 ^ _280566) ^ [] : [-(present(174 ^ [], 183 ^ []))], (236 ^ _280566) ^ [] : [-(nonreflexive(174 ^ [], 183 ^ []))], (238 ^ _280566) ^ [] : [-(scream(174 ^ [], 183 ^ []))], (240 ^ _280566) ^ [] : [-(of(174 ^ [], 183 ^ [], 182 ^ []))], (218 ^ _280566) ^ [_291001] : [member(174 ^ [], _291001, 180 ^ []), -(shot(174 ^ [], _291001))], (242 ^ _280566) ^ [_291682] : [actual_world(_291682), 245 ^ _280566 : [(246 ^ _280566) ^ [_292095, _292097, _292099, _292101, _292103, _292105, _292107] : [male(_291682, _292107), male(_291682, _292105), man(_291682, _292105), of(_291682, _292103, _292105), cannon(_291682, _292103), 268 ^ _280566 : [(269 ^ _280566) ^ [] : [-(member(_291682, 267 ^ [_291682, _292095, _292097, _292099, _292101, _292103, _292105, _292107], _292101))], (271 ^ _280566) ^ [_293092] : [event(_291682, _293092), agent(_291682, _293092, _292105), patient(_291682, _293092, 267 ^ [_291682, _292095, _292097, _292099, _292101, _292103, _292105, _292107]), present(_291682, _293092), nonreflexive(_291682, _293092), fire(_291682, _293092), from_loc(_291682, _293092, _292103)]], six(_291682, _292101), group(_291682, _292101), 307 ^ _280566 : [(308 ^ _280566) ^ [] : [-(member(_291682, 306 ^ [_291682, _292095, _292097, _292099, _292101, _292103, _292105, _292107], _292101))], (310 ^ _280566) ^ [] : [shot(_291682, 306 ^ [_291682, _292095, _292097, _292099, _292101, _292103, _292105, _292107])]], revenge(_291682, _292099), cry(_291682, _292097), event(_291682, _292095), agent(_291682, _292095, _292107), patient(_291682, _292095, _292097), present(_291682, _292095), nonreflexive(_291682, _292095), scream(_291682, _292095), of(_291682, _292095, _292099)]]]]]], input).
% 0.37/1.39 ncf('1',plain,[71 : actual_world(3 ^ []), 75 : male(3 ^ [], 6 ^ []), 75 : male(3 ^ [], 7 ^ []), 75 : man(3 ^ [], 7 ^ []), 75 : of(3 ^ [], 8 ^ [], 7 ^ []), 75 : cannon(3 ^ [], 8 ^ []), 100 : event(3 ^ [], 27 ^ [96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]]), 100 : agent(3 ^ [], 27 ^ [96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]], 7 ^ []), 100 : patient(3 ^ [], 27 ^ [96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]], 96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]), 100 : present(3 ^ [], 27 ^ [96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]]), 100 : nonreflexive(3 ^ [], 27 ^ [96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]]), 100 : fire(3 ^ [], 27 ^ [96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]]), 100 : from_loc(3 ^ [], 27 ^ [96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]], 8 ^ []), 100 : six(3 ^ [], 9 ^ []), 100 : group(3 ^ [], 9 ^ []), 139 : shot(3 ^ [], 135 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]), 139 : cry(3 ^ [], 11 ^ []), 139 : revenge(3 ^ [], 10 ^ []), 139 : event(3 ^ [], 12 ^ []), 139 : agent(3 ^ [], 12 ^ [], 6 ^ []), 139 : patient(3 ^ [], 12 ^ [], 11 ^ []), 139 : present(3 ^ [], 12 ^ []), 139 : nonreflexive(3 ^ [], 12 ^ []), 139 : scream(3 ^ [], 12 ^ []), 139 : of(3 ^ [], 12 ^ [], 10 ^ []), 242 : actual_world(174 ^ []), 246 : male(174 ^ [], 177 ^ []), 246 : male(174 ^ [], 178 ^ []), 246 : man(174 ^ [], 178 ^ []), 246 : of(174 ^ [], 179 ^ [], 178 ^ []), 246 : cannon(174 ^ [], 179 ^ []), 271 : event(174 ^ [], 198 ^ [267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []]]), 271 : agent(174 ^ [], 198 ^ [267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []]], 178 ^ []), 271 : patient(174 ^ [], 198 ^ [267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []]], 267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []]), 271 : present(174 ^ [], 198 ^ [267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []]]), 271 : nonreflexive(174 ^ [], 198 ^ [267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []]]), 271 : fire(174 ^ [], 198 ^ [267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []]]), 271 : from_loc(174 ^ [], 198 ^ [267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []]], 179 ^ []), 271 : six(174 ^ [], 180 ^ []), 271 : group(174 ^ [], 180 ^ []), 310 : shot(174 ^ [], 306 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []]), 310 : revenge(174 ^ [], 182 ^ []), 310 : cry(174 ^ [], 181 ^ []), 310 : event(174 ^ [], 183 ^ []), 310 : agent(174 ^ [], 183 ^ [], 177 ^ []), 310 : patient(174 ^ [], 183 ^ [], 181 ^ []), 310 : present(174 ^ [], 183 ^ []), 310 : nonreflexive(174 ^ [], 183 ^ []), 310 : scream(174 ^ [], 183 ^ []), 310 : of(174 ^ [], 183 ^ [], 182 ^ [])],start(2 ^ 0,bind([[_284281, _284694, _284696, _284698, _284700, _284702, _284704, _284706, _285691, _291682, _292095, _292097, _292099, _292101, _292103, _292105, _292107, _293092], [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ [], 27 ^ [96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]], 174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ [], 198 ^ [267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []]]]]))).
% 0.37/1.39 ncf('1.1',plain,[-(actual_world(3 ^ []))],extension(5 ^ 3)).
% 0.37/1.39 ncf('1.2',plain,[-(male(3 ^ [], 6 ^ []))],extension(14 ^ 5)).
% 0.37/1.39 ncf('1.3',plain,[-(male(3 ^ [], 7 ^ []))],extension(16 ^ 5)).
% 0.37/1.39 ncf('1.4',plain,[-(man(3 ^ [], 7 ^ []))],extension(18 ^ 5)).
% 0.37/1.39 ncf('1.5',plain,[-(of(3 ^ [], 8 ^ [], 7 ^ []))],extension(20 ^ 5)).
% 0.37/1.39 ncf('1.6',plain,[-(cannon(3 ^ [], 8 ^ []))],extension(22 ^ 5)).
% 0.37/1.39 ncf('1.7',plain,[-(event(3 ^ [], 27 ^ [96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]])), member(3 ^ [], 96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 9 ^ [])],extension(24 ^ 7,bind([[_282743], [96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]]]))).
% 0.37/1.39 ncf('1.7.1',plain,[-(member(3 ^ [], 96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 9 ^ []))],extension(98 ^ 8)).
% 0.37/1.39 ncf('1.8',plain,[-(agent(3 ^ [], 27 ^ [96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]], 7 ^ [])), member(3 ^ [], 96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 9 ^ [])],extension(24 ^ 7,bind([[_282743], [96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]]]))).
% 0.37/1.39 ncf('1.8.1',plain,[-(member(3 ^ [], 96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 9 ^ []))],extension(98 ^ 8)).
% 0.37/1.39 ncf('1.9',plain,[-(patient(3 ^ [], 27 ^ [96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]], 96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []])), member(3 ^ [], 96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 9 ^ [])],extension(24 ^ 7,bind([[_282743], [96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]]]))).
% 0.37/1.39 ncf('1.9.1',plain,[-(member(3 ^ [], 96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 9 ^ []))],extension(98 ^ 8)).
% 0.37/1.39 ncf('1.10',plain,[-(present(3 ^ [], 27 ^ [96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]])), member(3 ^ [], 96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 9 ^ [])],extension(24 ^ 7,bind([[_282743], [96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]]]))).
% 0.37/1.39 ncf('1.10.1',plain,[-(member(3 ^ [], 96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 9 ^ []))],extension(98 ^ 8)).
% 0.37/1.39 ncf('1.11',plain,[-(nonreflexive(3 ^ [], 27 ^ [96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]])), member(3 ^ [], 96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 9 ^ [])],extension(24 ^ 7,bind([[_282743], [96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]]]))).
% 0.37/1.39 ncf('1.11.1',plain,[-(member(3 ^ [], 96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 9 ^ []))],extension(98 ^ 8)).
% 0.37/1.39 ncf('1.12',plain,[-(fire(3 ^ [], 27 ^ [96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]])), member(3 ^ [], 96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 9 ^ [])],extension(24 ^ 7,bind([[_282743], [96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]]]))).
% 0.37/1.39 ncf('1.12.1',plain,[-(member(3 ^ [], 96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 9 ^ []))],extension(98 ^ 8)).
% 0.37/1.39 ncf('1.13',plain,[-(from_loc(3 ^ [], 27 ^ [96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]], 8 ^ [])), member(3 ^ [], 96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 9 ^ [])],extension(24 ^ 7,bind([[_282743], [96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]]]))).
% 0.37/1.39 ncf('1.13.1',plain,[-(member(3 ^ [], 96 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 9 ^ []))],extension(98 ^ 8)).
% 0.37/1.39 ncf('1.14',plain,[-(six(3 ^ [], 9 ^ []))],extension(43 ^ 5)).
% 0.37/1.39 ncf('1.15',plain,[-(group(3 ^ [], 9 ^ []))],extension(45 ^ 5)).
% 0.37/1.39 ncf('1.16',plain,[-(shot(3 ^ [], 135 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []])), member(3 ^ [], 135 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 9 ^ [])],extension(47 ^ 7,bind([[_283600], [135 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []]]]))).
% 0.37/1.39 ncf('1.16.1',plain,[-(member(3 ^ [], 135 ^ [3 ^ [], 12 ^ [], 10 ^ [], 11 ^ [], 9 ^ [], 8 ^ [], 7 ^ [], 6 ^ []], 9 ^ []))],extension(137 ^ 8)).
% 0.37/1.39 ncf('1.17',plain,[-(cry(3 ^ [], 11 ^ []))],extension(55 ^ 5)).
% 0.37/1.39 ncf('1.18',plain,[-(revenge(3 ^ [], 10 ^ []))],extension(53 ^ 5)).
% 0.37/1.39 ncf('1.19',plain,[-(event(3 ^ [], 12 ^ []))],extension(57 ^ 5)).
% 0.37/1.39 ncf('1.20',plain,[-(agent(3 ^ [], 12 ^ [], 6 ^ []))],extension(59 ^ 5)).
% 0.37/1.39 ncf('1.21',plain,[-(patient(3 ^ [], 12 ^ [], 11 ^ []))],extension(61 ^ 5)).
% 0.37/1.39 ncf('1.22',plain,[-(present(3 ^ [], 12 ^ []))],extension(63 ^ 5)).
% 0.37/1.39 ncf('1.23',plain,[-(nonreflexive(3 ^ [], 12 ^ []))],extension(65 ^ 5)).
% 0.37/1.39 ncf('1.24',plain,[-(scream(3 ^ [], 12 ^ []))],extension(67 ^ 5)).
% 0.37/1.39 ncf('1.25',plain,[-(of(3 ^ [], 12 ^ [], 10 ^ []))],extension(69 ^ 5)).
% 0.37/1.39 ncf('1.26',plain,[-(actual_world(174 ^ []))],extension(176 ^ 3)).
% 0.37/1.39 ncf('1.27',plain,[-(male(174 ^ [], 177 ^ []))],extension(185 ^ 5)).
% 0.37/1.39 ncf('1.28',plain,[-(male(174 ^ [], 178 ^ []))],extension(187 ^ 5)).
% 0.37/1.39 ncf('1.29',plain,[-(man(174 ^ [], 178 ^ []))],extension(189 ^ 5)).
% 0.37/1.39 ncf('1.30',plain,[-(of(174 ^ [], 179 ^ [], 178 ^ []))],extension(191 ^ 5)).
% 0.37/1.39 ncf('1.31',plain,[-(cannon(174 ^ [], 179 ^ []))],extension(193 ^ 5)).
% 0.37/1.39 ncf('1.32',plain,[-(event(174 ^ [], 198 ^ [267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []]])), member(174 ^ [], 267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []], 180 ^ [])],extension(195 ^ 7,bind([[_290144], [267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []]]]))).
% 0.37/1.39 ncf('1.32.1',plain,[-(member(174 ^ [], 267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []], 180 ^ []))],extension(269 ^ 8)).
% 0.37/1.39 ncf('1.33',plain,[-(agent(174 ^ [], 198 ^ [267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []]], 178 ^ [])), member(174 ^ [], 267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []], 180 ^ [])],extension(195 ^ 7,bind([[_290144], [267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []]]]))).
% 0.37/1.39 ncf('1.33.1',plain,[-(member(174 ^ [], 267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []], 180 ^ []))],extension(269 ^ 8)).
% 0.37/1.39 ncf('1.34',plain,[-(patient(174 ^ [], 198 ^ [267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []]], 267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []])), member(174 ^ [], 267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []], 180 ^ [])],extension(195 ^ 7,bind([[_290144], [267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []]]]))).
% 0.37/1.39 ncf('1.34.1',plain,[-(member(174 ^ [], 267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []], 180 ^ []))],extension(269 ^ 8)).
% 0.37/1.39 ncf('1.35',plain,[-(present(174 ^ [], 198 ^ [267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []]])), member(174 ^ [], 267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []], 180 ^ [])],extension(195 ^ 7,bind([[_290144], [267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []]]]))).
% 0.37/1.39 ncf('1.35.1',plain,[-(member(174 ^ [], 267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []], 180 ^ []))],extension(269 ^ 8)).
% 0.37/1.39 ncf('1.36',plain,[-(nonreflexive(174 ^ [], 198 ^ [267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []]])), member(174 ^ [], 267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []], 180 ^ [])],extension(195 ^ 7,bind([[_290144], [267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []]]]))).
% 0.37/1.39 ncf('1.36.1',plain,[-(member(174 ^ [], 267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []], 180 ^ []))],extension(269 ^ 8)).
% 0.37/1.39 ncf('1.37',plain,[-(fire(174 ^ [], 198 ^ [267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []]])), member(174 ^ [], 267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []], 180 ^ [])],extension(195 ^ 7,bind([[_290144], [267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []]]]))).
% 0.37/1.39 ncf('1.37.1',plain,[-(member(174 ^ [], 267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []], 180 ^ []))],extension(269 ^ 8)).
% 0.37/1.39 ncf('1.38',plain,[-(from_loc(174 ^ [], 198 ^ [267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []]], 179 ^ [])), member(174 ^ [], 267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []], 180 ^ [])],extension(195 ^ 7,bind([[_290144], [267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []]]]))).
% 0.37/1.39 ncf('1.38.1',plain,[-(member(174 ^ [], 267 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []], 180 ^ []))],extension(269 ^ 8)).
% 0.37/1.39 ncf('1.39',plain,[-(six(174 ^ [], 180 ^ []))],extension(214 ^ 5)).
% 0.37/1.39 ncf('1.40',plain,[-(group(174 ^ [], 180 ^ []))],extension(216 ^ 5)).
% 0.37/1.39 ncf('1.41',plain,[-(shot(174 ^ [], 306 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []])), member(174 ^ [], 306 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []], 180 ^ [])],extension(218 ^ 7,bind([[_291001], [306 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []]]]))).
% 0.37/1.39 ncf('1.41.1',plain,[-(member(174 ^ [], 306 ^ [174 ^ [], 183 ^ [], 181 ^ [], 182 ^ [], 180 ^ [], 179 ^ [], 178 ^ [], 177 ^ []], 180 ^ []))],extension(308 ^ 8)).
% 0.37/1.39 ncf('1.42',plain,[-(revenge(174 ^ [], 182 ^ []))],extension(226 ^ 5)).
% 0.37/1.39 ncf('1.43',plain,[-(cry(174 ^ [], 181 ^ []))],extension(224 ^ 5)).
% 0.37/1.39 ncf('1.44',plain,[-(event(174 ^ [], 183 ^ []))],extension(228 ^ 5)).
% 0.37/1.39 ncf('1.45',plain,[-(agent(174 ^ [], 183 ^ [], 177 ^ []))],extension(230 ^ 5)).
% 0.37/1.39 ncf('1.46',plain,[-(patient(174 ^ [], 183 ^ [], 181 ^ []))],extension(232 ^ 5)).
% 0.37/1.39 ncf('1.47',plain,[-(present(174 ^ [], 183 ^ []))],extension(234 ^ 5)).
% 0.37/1.39 ncf('1.48',plain,[-(nonreflexive(174 ^ [], 183 ^ []))],extension(236 ^ 5)).
% 0.37/1.39 ncf('1.49',plain,[-(scream(174 ^ [], 183 ^ []))],extension(238 ^ 5)).
% 0.37/1.39 ncf('1.50',plain,[-(of(174 ^ [], 183 ^ [], 182 ^ []))],extension(240 ^ 5)).
% 0.37/1.39 %-----------------------------------------------------
% 0.37/1.39 End of proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------