%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : NLP204+1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n031.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:37:15 EDT 2023
% Result : Theorem 2.43s 3.44s
% Output : Proof 2.43s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NLP204+1 : TPTP v8.1.2. Released v2.4.0.
% 0.07/0.13 % Command : nanocop.sh %s %d
% 0.12/0.34 % Computer : n031.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:30:25 EDT 2023
% 0.12/0.34 % CPUTime :
% 2.43/3.44
% 2.43/3.44 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 2.43/3.44 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.43/3.44 %-----------------------------------------------------
% 2.43/3.44 ncf(matrix, plain, [(1548 ^ _258015) ^ [] : [-(actual_world(1546 ^ []))], (1561 ^ _258015) ^ [] : [-(of(1546 ^ [], 1550 ^ [], 1549 ^ []))], (1563 ^ _258015) ^ [] : [-(man(1546 ^ [], 1549 ^ []))], (1565 ^ _258015) ^ [] : [-(jules_forename(1546 ^ [], 1550 ^ []))], (1567 ^ _258015) ^ [] : [-(forename(1546 ^ [], 1550 ^ []))], (1569 ^ _258015) ^ [] : [-(frontseat(1546 ^ [], 1551 ^ []))], (1571 ^ _258015) ^ [] : [-(chevy(1546 ^ [], 1552 ^ []))], (1573 ^ _258015) ^ [] : [-(white(1546 ^ [], 1552 ^ []))], (1575 ^ _258015) ^ [] : [-(dirty(1546 ^ [], 1552 ^ []))], (1577 ^ _258015) ^ [] : [-(old(1546 ^ [], 1552 ^ []))], (1579 ^ _258015) ^ [] : [-(of(1546 ^ [], 1553 ^ [], 1554 ^ []))], (1581 ^ _258015) ^ [] : [-(city(1546 ^ [], 1554 ^ []))], (1583 ^ _258015) ^ [] : [-(hollywood_placename(1546 ^ [], 1553 ^ []))], (1585 ^ _258015) ^ [] : [-(placename(1546 ^ [], 1553 ^ []))], (1587 ^ _258015) ^ [] : [-(street(1546 ^ [], 1554 ^ []))], (1589 ^ _258015) ^ [] : [-(lonely(1546 ^ [], 1554 ^ []))], (1591 ^ _258015) ^ [] : [-(event(1546 ^ [], 1555 ^ []))], (1593 ^ _258015) ^ [] : [-(agent(1546 ^ [], 1555 ^ [], 1552 ^ []))], (1595 ^ _258015) ^ [] : [-(present(1546 ^ [], 1555 ^ []))], (1597 ^ _258015) ^ [] : [-(barrel(1546 ^ [], 1555 ^ []))], (1599 ^ _258015) ^ [] : [-(down(1546 ^ [], 1555 ^ [], 1554 ^ []))], (1601 ^ _258015) ^ [] : [-(in(1546 ^ [], 1555 ^ [], 1554 ^ []))], (1603 ^ _258015) ^ [_315796] : [member(1546 ^ [], _315796, 1556 ^ []), 1608 ^ _258015 : [(1609 ^ _258015) ^ [] : [-(state(1546 ^ [], 1606 ^ [_315796]))], (1611 ^ _258015) ^ [] : [-(be(1546 ^ [], 1606 ^ [_315796], _315796, 1607 ^ [_315796]))], (1613 ^ _258015) ^ [] : [-(in(1546 ^ [], 1607 ^ [_315796], 1551 ^ []))]]], (1615 ^ _258015) ^ [] : [-(two(1546 ^ [], 1556 ^ []))], (1617 ^ _258015) ^ [] : [-(group(1546 ^ [], 1556 ^ []))], (1619 ^ _258015) ^ [_316402] : [member(1546 ^ [], _316402, 1556 ^ []), 1622 ^ _258015 : [(1623 ^ _258015) ^ [] : [-(fellow(1546 ^ [], _316402))], (1625 ^ _258015) ^ [] : [-(young(1546 ^ [], _316402))]]], (1648 ^ _258015) ^ [] : [-(group(1546 ^ [], 1557 ^ []))], (1660 ^ _258015) ^ [] : [-(wheel(1546 ^ [], 1559 ^ []))], (1662 ^ _258015) ^ [] : [-(state(1546 ^ [], 1558 ^ []))], (1664 ^ _258015) ^ [] : [-(be(1546 ^ [], 1558 ^ [], 1549 ^ [], 1559 ^ []))], (1666 ^ _258015) ^ [] : [-(behind(1546 ^ [], 1559 ^ [], 1559 ^ []))], (1650 ^ _258015) ^ [_317597] : [member(1546 ^ [], _317597, 1557 ^ []), 1653 ^ _258015 : [(1654 ^ _258015) ^ [] : [-(coat(1546 ^ [], _317597))], (1656 ^ _258015) ^ [] : [-(black(1546 ^ [], _317597))], (1658 ^ _258015) ^ [] : [-(cheap(1546 ^ [], _317597))]]], (1627 ^ _258015) ^ [_316667] : [member(1546 ^ [], _316667, 1557 ^ []), 1630 ^ _258015 : [(1631 ^ _258015) ^ [_316840] : [member(1546 ^ [], _316840, 1556 ^ []), 1635 ^ _258015 : [(1636 ^ _258015) ^ [] : [-(event(1546 ^ [], 1634 ^ [_316667, _316840]))], (1638 ^ _258015) ^ [] : [-(agent(1546 ^ [], 1634 ^ [_316667, _316840], _316840))], (1640 ^ _258015) ^ [] : [-(patient(1546 ^ [], 1634 ^ [_316667, _316840], _316667))], (1642 ^ _258015) ^ [] : [-(present(1546 ^ [], 1634 ^ [_316667, _316840]))], (1644 ^ _258015) ^ [] : [-(nonreflexive(1546 ^ [], 1634 ^ [_316667, _316840]))], (1646 ^ _258015) ^ [] : [-(wear(1546 ^ [], 1634 ^ [_316667, _316840]))]]]]], (1046 ^ _258015) ^ [_292077, _292079] : [jules_forename(_292079, _292077), -(forename(_292079, _292077))], (1052 ^ _258015) ^ [_292287, _292289] : [forename(_292289, _292287), -(relname(_292289, _292287))], (1058 ^ _258015) ^ [_292497, _292499] : [furniture(_292499, _292497), -(instrumentality(_292499, _292497))], (1064 ^ _258015) ^ [_292707, _292709] : [seat(_292709, _292707), -(furniture(_292709, _292707))], (1070 ^ _258015) ^ [_292917, _292919] : [frontseat(_292919, _292917), -(seat(_292919, _292917))], (1076 ^ _258015) ^ [_293127, _293129] : [location(_293129, _293127), -(object(_293129, _293127))], (1082 ^ _258015) ^ [_293337, _293339] : [city(_293339, _293337), -(location(_293339, _293337))], (1088 ^ _258015) ^ [_293547, _293549] : [hollywood_placename(_293549, _293547), -(placename(_293549, _293547))], (1094 ^ _258015) ^ [_293757, _293759] : [abstraction(_293759, _293757), -(unisex(_293759, _293757))], (1100 ^ _258015) ^ [_293967, _293969] : [abstraction(_293969, _293967), -(general(_293969, _293967))], (1106 ^ _258015) ^ [_294177, _294179] : [abstraction(_294179, _294177), -(nonhuman(_294179, _294177))], (1112 ^ _258015) ^ [_294387, _294389] : [abstraction(_294389, _294387), -(thing(_294389, _294387))], (1118 ^ _258015) ^ [_294597, _294599] : [relation(_294599, _294597), -(abstraction(_294599, _294597))], (1124 ^ _258015) ^ [_294807, _294809] : [relname(_294809, _294807), -(relation(_294809, _294807))], (1130 ^ _258015) ^ [_295017, _295019] : [placename(_295019, _295017), -(relname(_295019, _295017))], (1136 ^ _258015) ^ [_295227, _295229] : [transport(_295229, _295227), -(instrumentality(_295229, _295227))], (1142 ^ _258015) ^ [_295437, _295439] : [vehicle(_295439, _295437), -(transport(_295439, _295437))], (1148 ^ _258015) ^ [_295647, _295649] : [car(_295649, _295647), -(vehicle(_295649, _295647))], (1154 ^ _258015) ^ [_295857, _295859] : [chevy(_295859, _295857), -(car(_295859, _295857))], (1160 ^ _258015) ^ [_296067, _296069] : [way(_296069, _296067), -(artifact(_296069, _296067))], (1166 ^ _258015) ^ [_296277, _296279] : [street(_296279, _296277), -(way(_296279, _296277))], (1172 ^ _258015) ^ [_296487, _296489] : [barrel(_296489, _296487), -(event(_296489, _296487))], (1178 ^ _258015) ^ [_296697, _296699] : [two(_296699, _296697), -(group(_296699, _296697))], (1184 ^ _258015) ^ [_296907, _296909] : [man(_296909, _296907), -(male(_296909, _296907))], (1190 ^ _258015) ^ [_297117, _297119] : [human_person(_297119, _297117), -(animate(_297119, _297117))], (1196 ^ _258015) ^ [_297327, _297329] : [human_person(_297329, _297327), -(human(_297329, _297327))], (1202 ^ _258015) ^ [_297537, _297539] : [organism(_297539, _297537), -(living(_297539, _297537))], (1208 ^ _258015) ^ [_297747, _297749] : [organism(_297749, _297747), -(impartial(_297749, _297747))], (1214 ^ _258015) ^ [_297957, _297959] : [organism(_297959, _297957), -(entity(_297959, _297957))], (1220 ^ _258015) ^ [_298167, _298169] : [human_person(_298169, _298167), -(organism(_298169, _298167))], (1226 ^ _258015) ^ [_298377, _298379] : [man(_298379, _298377), -(human_person(_298379, _298377))], (1232 ^ _258015) ^ [_298587, _298589] : [fellow(_298589, _298587), -(man(_298589, _298587))], (1238 ^ _258015) ^ [_298797, _298799] : [wear(_298799, _298797), -(event(_298799, _298797))], (1244 ^ _258015) ^ [_299007, _299009] : [set(_299009, _299007), -(multiple(_299009, _299007))], (1250 ^ _258015) ^ [_299217, _299219] : [group(_299219, _299217), -(set(_299219, _299217))], (1256 ^ _258015) ^ [_299427, _299429] : [clothes(_299429, _299427), -(artifact(_299429, _299427))], (1262 ^ _258015) ^ [_299637, _299639] : [coat(_299639, _299637), -(clothes(_299639, _299637))], (1268 ^ _258015) ^ [_299847, _299849] : [object(_299849, _299847), -(unisex(_299849, _299847))], (1274 ^ _258015) ^ [_300057, _300059] : [object(_300059, _300057), -(impartial(_300059, _300057))], (1280 ^ _258015) ^ [_300267, _300269] : [object(_300269, _300267), -(nonliving(_300269, _300267))], (1286 ^ _258015) ^ [_300477, _300479] : [entity(_300479, _300477), -(existent(_300479, _300477))], (1292 ^ _258015) ^ [_300687, _300689] : [entity(_300689, _300687), -(specific(_300689, _300687))], (1298 ^ _258015) ^ [_300897, _300899] : [entity(_300899, _300897), -(thing(_300899, _300897))], (1304 ^ _258015) ^ [_301107, _301109] : [object(_301109, _301107), -(entity(_301109, _301107))], (1310 ^ _258015) ^ [_301317, _301319] : [artifact(_301319, _301317), -(object(_301319, _301317))], (1316 ^ _258015) ^ [_301527, _301529] : [instrumentality(_301529, _301527), -(artifact(_301529, _301527))], (1322 ^ _258015) ^ [_301737, _301739] : [device(_301739, _301737), -(instrumentality(_301739, _301737))], (1328 ^ _258015) ^ [_301947, _301949] : [wheel(_301949, _301947), -(device(_301949, _301947))], (1334 ^ _258015) ^ [_302157, _302159] : [event(_302159, _302157), -(eventuality(_302159, _302157))], (1340 ^ _258015) ^ [_302367, _302369] : [state(_302369, _302367), -(event(_302369, _302367))], (1346 ^ _258015) ^ [_302577, _302579] : [eventuality(_302579, _302577), -(unisex(_302579, _302577))], (1352 ^ _258015) ^ [_302787, _302789] : [eventuality(_302789, _302787), -(nonexistent(_302789, _302787))], (1358 ^ _258015) ^ [_302997, _302999] : [eventuality(_302999, _302997), -(specific(_302999, _302997))], (1364 ^ _258015) ^ [_303207, _303209] : [thing(_303209, _303207), -(singleton(_303209, _303207))], (1370 ^ _258015) ^ [_303417, _303419] : [eventuality(_303419, _303417), -(thing(_303419, _303417))], (1376 ^ _258015) ^ [_303627, _303629] : [state(_303629, _303627), -(eventuality(_303629, _303627))], (1382 ^ _258015) ^ [_303837, _303839] : [animate(_303839, _303837), nonliving(_303839, _303837)], (1388 ^ _258015) ^ [_304048, _304050] : [existent(_304050, _304048), nonexistent(_304050, _304048)], (1394 ^ _258015) ^ [_304259, _304261] : [nonhuman(_304261, _304259), human(_304261, _304259)], (1400 ^ _258015) ^ [_304470, _304472] : [nonliving(_304472, _304470), living(_304472, _304470)], (1406 ^ _258015) ^ [_304681, _304683] : [singleton(_304683, _304681), multiple(_304683, _304681)], (1412 ^ _258015) ^ [_304892, _304894] : [specific(_304894, _304892), general(_304894, _304892)], (1418 ^ _258015) ^ [_305103, _305105] : [unisex(_305105, _305103), male(_305105, _305103)], (1424 ^ _258015) ^ [_305314, _305316] : [white(_305316, _305314), black(_305316, _305314)], (1430 ^ _258015) ^ [_305525, _305527] : [young(_305527, _305525), old(_305527, _305525)], (1436 ^ _258015) ^ [_305750, _305752, _305754] : [entity(_305754, _305752), forename(_305754, _305750), of(_305754, _305750, _305752), 1447 ^ _258015 : [(1448 ^ _258015) ^ [_306090] : [forename(_305754, _306090), -(_306090 = _305750), of(_305754, _306090, _305752)]]], (1458 ^ _258015) ^ [_306442, _306444, _306446] : [entity(_306446, _306444), placename(_306446, _306442), of(_306446, _306442, _306444), 1469 ^ _258015 : [(1470 ^ _258015) ^ [_306782] : [placename(_306446, _306782), -(_306782 = _306442), of(_306446, _306782, _306444)]]], (1539 ^ _258015) ^ [_309428, _309430] : [member(_309430, _309428, _309428)], (1541 ^ _258015) ^ [_309546, _309548, _309550, _309552] : [be(_309552, _309550, _309548, _309546), -(_309548 = _309546)], (1525 ^ _258015) ^ [_309023, _309025, _309027, _309029] : [_309025 = _309023, nonreflexive(_309029, _309027), agent(_309029, _309027, _309025), patient(_309029, _309027, _309023)], (1480 ^ _258015) ^ [_307149, _307151] : [two(_307151, _307149), 1484 ^ _258015 : [(1485 ^ _258015) ^ [] : [-(member(_307151, 1483 ^ [_307149, _307151], _307149))], (1488 ^ _258015) ^ [] : [-(member(_307151, 1486 ^ [_307149, _307151], _307149))], (1490 ^ _258015) ^ [] : [1486 ^ [_307149, _307151] = 1483 ^ [_307149, _307151]], (1492 ^ _258015) ^ [_307734] : [member(_307151, _307734, _307149), -(_307734 = 1486 ^ [_307149, _307151]), -(_307734 = 1483 ^ [_307149, _307151])]]], (1502 ^ _258015) ^ [_308041, _308043] : [-(two(_308043, _308041)), 1503 ^ _258015 : [(1504 ^ _258015) ^ [_308172] : [member(_308043, _308172, _308041), 1507 ^ _258015 : [(1508 ^ _258015) ^ [_308346] : [member(_308043, _308346, _308041), -(_308346 = _308172), 1516 ^ _258015 : [(1517 ^ _258015) ^ [] : [-(member(_308043, 1515 ^ [_308041, _308043, _308172, _308346], _308041))], (1519 ^ _258015) ^ [] : [1515 ^ [_308041, _308043, _308172, _308346] = _308346], (1521 ^ _258015) ^ [] : [1515 ^ [_308041, _308043, _308172, _308346] = _308172]]]]]]], (2 ^ _258015) ^ [_258139] : [-(_258139 = _258139)], (4 ^ _258015) ^ [_258246, _258248] : [_258248 = _258246, -(_258246 = _258248)], (10 ^ _258015) ^ [_258450, _258452, _258454] : [-(_258454 = _258450), _258454 = _258452, _258452 = _258450], (20 ^ _258015) ^ [_258791, _258793, _258795, _258797] : [-(furniture(_258795, _258791)), furniture(_258797, _258793), _258797 = _258795, _258793 = _258791], (34 ^ _258015) ^ [_259235, _259237, _259239, _259241] : [-(seat(_259239, _259235)), seat(_259241, _259237), _259241 = _259239, _259237 = _259235], (48 ^ _258015) ^ [_259679, _259681, _259683, _259685] : [-(location(_259683, _259679)), location(_259685, _259681), _259685 = _259683, _259681 = _259679], (62 ^ _258015) ^ [_260123, _260125, _260127, _260129] : [-(abstraction(_260127, _260123)), abstraction(_260129, _260125), _260129 = _260127, _260125 = _260123], (76 ^ _258015) ^ [_260567, _260569, _260571, _260573] : [-(relation(_260571, _260567)), relation(_260573, _260569), _260573 = _260571, _260569 = _260567], (90 ^ _258015) ^ [_261011, _261013, _261015, _261017] : [-(relname(_261015, _261011)), relname(_261017, _261013), _261017 = _261015, _261013 = _261011], (104 ^ _258015) ^ [_261455, _261457, _261459, _261461] : [-(transport(_261459, _261455)), transport(_261461, _261457), _261461 = _261459, _261457 = _261455], (118 ^ _258015) ^ [_261899, _261901, _261903, _261905] : [-(vehicle(_261903, _261899)), vehicle(_261905, _261901), _261905 = _261903, _261901 = _261899], (132 ^ _258015) ^ [_262343, _262345, _262347, _262349] : [-(car(_262347, _262343)), car(_262349, _262345), _262349 = _262347, _262345 = _262343], (146 ^ _258015) ^ [_262787, _262789, _262791, _262793] : [-(way(_262791, _262787)), way(_262793, _262789), _262793 = _262791, _262789 = _262787], (160 ^ _258015) ^ [_263231, _263233, _263235, _263237] : [-(organism(_263235, _263231)), organism(_263237, _263233), _263237 = _263235, _263233 = _263231], (174 ^ _258015) ^ [_263675, _263677, _263679, _263681] : [-(human_person(_263679, _263675)), human_person(_263681, _263677), _263681 = _263679, _263677 = _263675], (188 ^ _258015) ^ [_264119, _264121, _264123, _264125] : [-(set(_264123, _264119)), set(_264125, _264121), _264125 = _264123, _264121 = _264119], (202 ^ _258015) ^ [_264563, _264565, _264567, _264569] : [-(clothes(_264567, _264563)), clothes(_264569, _264565), _264569 = _264567, _264565 = _264563], (216 ^ _258015) ^ [_265007, _265009, _265011, _265013] : [-(impartial(_265011, _265007)), impartial(_265013, _265009), _265013 = _265011, _265009 = _265007], (230 ^ _258015) ^ [_265451, _265453, _265455, _265457] : [-(object(_265455, _265451)), object(_265457, _265453), _265457 = _265455, _265453 = _265451], (244 ^ _258015) ^ [_265895, _265897, _265899, _265901] : [-(artifact(_265899, _265895)), artifact(_265901, _265897), _265901 = _265899, _265897 = _265895], (258 ^ _258015) ^ [_266339, _266341, _266343, _266345] : [-(instrumentality(_266343, _266339)), instrumentality(_266345, _266341), _266345 = _266343, _266341 = _266339], (272 ^ _258015) ^ [_266783, _266785, _266787, _266789] : [-(device(_266787, _266783)), device(_266789, _266785), _266789 = _266787, _266785 = _266783], (286 ^ _258015) ^ [_267227, _267229, _267231, _267233] : [-(thing(_267231, _267227)), thing(_267233, _267229), _267233 = _267231, _267229 = _267227], (300 ^ _258015) ^ [_267671, _267673, _267675, _267677] : [-(eventuality(_267675, _267671)), eventuality(_267677, _267673), _267677 = _267675, _267673 = _267671], (314 ^ _258015) ^ [_268115, _268117, _268119, _268121] : [-(animate(_268119, _268115)), animate(_268121, _268117), _268121 = _268119, _268117 = _268115], (328 ^ _258015) ^ [_268559, _268561, _268563, _268565] : [-(existent(_268563, _268559)), existent(_268565, _268561), _268565 = _268563, _268561 = _268559], (342 ^ _258015) ^ [_269003, _269005, _269007, _269009] : [-(nonexistent(_269007, _269003)), nonexistent(_269009, _269005), _269009 = _269007, _269005 = _269003], (356 ^ _258015) ^ [_269447, _269449, _269451, _269453] : [-(nonhuman(_269451, _269447)), nonhuman(_269453, _269449), _269453 = _269451, _269449 = _269447], (370 ^ _258015) ^ [_269891, _269893, _269895, _269897] : [-(human(_269895, _269891)), human(_269897, _269893), _269897 = _269895, _269893 = _269891], (384 ^ _258015) ^ [_270335, _270337, _270339, _270341] : [-(nonliving(_270339, _270335)), nonliving(_270341, _270337), _270341 = _270339, _270337 = _270335], (398 ^ _258015) ^ [_270779, _270781, _270783, _270785] : [-(living(_270783, _270779)), living(_270785, _270781), _270785 = _270783, _270781 = _270779], (412 ^ _258015) ^ [_271223, _271225, _271227, _271229] : [-(singleton(_271227, _271223)), singleton(_271229, _271225), _271229 = _271227, _271225 = _271223], (426 ^ _258015) ^ [_271667, _271669, _271671, _271673] : [-(multiple(_271671, _271667)), multiple(_271673, _271669), _271673 = _271671, _271669 = _271667], (440 ^ _258015) ^ [_272111, _272113, _272115, _272117] : [-(specific(_272115, _272111)), specific(_272117, _272113), _272117 = _272115, _272113 = _272111], (454 ^ _258015) ^ [_272555, _272557, _272559, _272561] : [-(general(_272559, _272555)), general(_272561, _272557), _272561 = _272559, _272557 = _272555], (468 ^ _258015) ^ [_272999, _273001, _273003, _273005] : [-(unisex(_273003, _272999)), unisex(_273005, _273001), _273005 = _273003, _273001 = _272999], (482 ^ _258015) ^ [_273443, _273445, _273447, _273449] : [-(male(_273447, _273443)), male(_273449, _273445), _273449 = _273447, _273445 = _273443], (496 ^ _258015) ^ [_273887, _273889, _273891, _273893] : [-(entity(_273891, _273887)), entity(_273893, _273889), _273893 = _273891, _273889 = _273887], (510 ^ _258015) ^ [_274303, _274305] : [-(actual_world(_274303)), _274305 = _274303, actual_world(_274305)], (520 ^ _258015) ^ [_274626, _274628, _274630, _274632] : [-(man(_274630, _274626)), man(_274632, _274628), _274632 = _274630, _274628 = _274626], (534 ^ _258015) ^ [_275070, _275072, _275074, _275076] : [-(jules_forename(_275074, _275070)), jules_forename(_275076, _275072), _275076 = _275074, _275072 = _275070], (548 ^ _258015) ^ [_275514, _275516, _275518, _275520] : [-(forename(_275518, _275514)), forename(_275520, _275516), _275520 = _275518, _275516 = _275514], (562 ^ _258015) ^ [_275958, _275960, _275962, _275964] : [-(frontseat(_275962, _275958)), frontseat(_275964, _275960), _275964 = _275962, _275960 = _275958], (576 ^ _258015) ^ [_276402, _276404, _276406, _276408] : [-(chevy(_276406, _276402)), chevy(_276408, _276404), _276408 = _276406, _276404 = _276402], (590 ^ _258015) ^ [_276846, _276848, _276850, _276852] : [-(white(_276850, _276846)), white(_276852, _276848), _276852 = _276850, _276848 = _276846], (604 ^ _258015) ^ [_277290, _277292, _277294, _277296] : [-(dirty(_277294, _277290)), dirty(_277296, _277292), _277296 = _277294, _277292 = _277290], (618 ^ _258015) ^ [_277734, _277736, _277738, _277740] : [-(old(_277738, _277734)), old(_277740, _277736), _277740 = _277738, _277736 = _277734], (632 ^ _258015) ^ [_278206, _278208, _278210, _278212, _278214, _278216] : [-(of(_278214, _278210, _278206)), of(_278216, _278212, _278208), _278216 = _278214, _278212 = _278210, _278208 = _278206], (650 ^ _258015) ^ [_278787, _278789, _278791, _278793] : [-(city(_278791, _278787)), city(_278793, _278789), _278793 = _278791, _278789 = _278787], (664 ^ _258015) ^ [_279231, _279233, _279235, _279237] : [-(hollywood_placename(_279235, _279231)), hollywood_placename(_279237, _279233), _279237 = _279235, _279233 = _279231], (678 ^ _258015) ^ [_279675, _279677, _279679, _279681] : [-(placename(_279679, _279675)), placename(_279681, _279677), _279681 = _279679, _279677 = _279675], (692 ^ _258015) ^ [_280119, _280121, _280123, _280125] : [-(street(_280123, _280119)), street(_280125, _280121), _280125 = _280123, _280121 = _280119], (706 ^ _258015) ^ [_280563, _280565, _280567, _280569] : [-(lonely(_280567, _280563)), lonely(_280569, _280565), _280569 = _280567, _280565 = _280563], (720 ^ _258015) ^ [_281007, _281009, _281011, _281013] : [-(barrel(_281011, _281007)), barrel(_281013, _281009), _281013 = _281011, _281009 = _281007], (734 ^ _258015) ^ [_281479, _281481, _281483, _281485, _281487, _281489] : [-(down(_281487, _281483, _281479)), down(_281489, _281485, _281481), _281489 = _281487, _281485 = _281483, _281481 = _281479], (752 ^ _258015) ^ [_282088, _282090, _282092, _282094, _282096, _282098] : [-(in(_282096, _282092, _282088)), in(_282098, _282094, _282090), _282098 = _282096, _282094 = _282092, _282090 = _282088], (770 ^ _258015) ^ [_282669, _282671, _282673, _282675] : [-(two(_282673, _282669)), two(_282675, _282671), _282675 = _282673, _282671 = _282669], (784 ^ _258015) ^ [_283113, _283115, _283117, _283119] : [-(fellow(_283117, _283113)), fellow(_283119, _283115), _283119 = _283117, _283115 = _283113], (798 ^ _258015) ^ [_283557, _283559, _283561, _283563] : [-(young(_283561, _283557)), young(_283563, _283559), _283563 = _283561, _283559 = _283557], (812 ^ _258015) ^ [_284001, _284003, _284005, _284007] : [-(event(_284005, _284001)), event(_284007, _284003), _284007 = _284005, _284003 = _284001], (826 ^ _258015) ^ [_284473, _284475, _284477, _284479, _284481, _284483] : [-(agent(_284481, _284477, _284473)), agent(_284483, _284479, _284475), _284483 = _284481, _284479 = _284477, _284475 = _284473], (844 ^ _258015) ^ [_285082, _285084, _285086, _285088, _285090, _285092] : [-(patient(_285090, _285086, _285082)), patient(_285092, _285088, _285084), _285092 = _285090, _285088 = _285086, _285084 = _285082], (862 ^ _258015) ^ [_285663, _285665, _285667, _285669] : [-(present(_285667, _285663)), present(_285669, _285665), _285669 = _285667, _285665 = _285663], (876 ^ _258015) ^ [_286107, _286109, _286111, _286113] : [-(nonreflexive(_286111, _286107)), nonreflexive(_286113, _286109), _286113 = _286111, _286109 = _286107], (890 ^ _258015) ^ [_286551, _286553, _286555, _286557] : [-(wear(_286555, _286551)), wear(_286557, _286553), _286557 = _286555, _286553 = _286551], (904 ^ _258015) ^ [_286995, _286997, _286999, _287001] : [-(group(_286999, _286995)), group(_287001, _286997), _287001 = _286999, _286997 = _286995], (918 ^ _258015) ^ [_287467, _287469, _287471, _287473, _287475, _287477] : [-(member(_287475, _287471, _287467)), member(_287477, _287473, _287469), _287477 = _287475, _287473 = _287471, _287469 = _287467], (936 ^ _258015) ^ [_288048, _288050, _288052, _288054] : [-(coat(_288052, _288048)), coat(_288054, _288050), _288054 = _288052, _288050 = _288048], (950 ^ _258015) ^ [_288492, _288494, _288496, _288498] : [-(black(_288496, _288492)), black(_288498, _288494), _288498 = _288496, _288494 = _288492], (964 ^ _258015) ^ [_288936, _288938, _288940, _288942] : [-(cheap(_288940, _288936)), cheap(_288942, _288938), _288942 = _288940, _288938 = _288936], (978 ^ _258015) ^ [_289380, _289382, _289384, _289386] : [-(wheel(_289384, _289380)), wheel(_289386, _289382), _289386 = _289384, _289382 = _289380], (992 ^ _258015) ^ [_289824, _289826, _289828, _289830] : [-(state(_289828, _289824)), state(_289830, _289826), _289830 = _289828, _289826 = _289824], (1028 ^ _258015) ^ [_291066, _291068, _291070, _291072, _291074, _291076] : [-(behind(_291074, _291070, _291066)), behind(_291076, _291072, _291068), _291076 = _291074, _291072 = _291070, _291068 = _291066], (1006 ^ _258015) ^ [_290324, _290326, _290328, _290330, _290332, _290334, _290336, _290338] : [-(be(_290336, _290332, _290328, _290324)), be(_290338, _290334, _290330, _290326), _290338 = _290336, _290334 = _290332, _290330 = _290328, _290326 = _290324]], input).
% 2.43/3.44 ncf('1',plain,[animate(1546 ^ [], 1549 ^ []), nonliving(1546 ^ [], 1549 ^ [])],start(1382 ^ 0,bind([[_303837, _303839], [1549 ^ [], 1546 ^ []]]))).
% 2.43/3.44 ncf('1.1',plain,[-(animate(1546 ^ [], 1549 ^ [])), human_person(1546 ^ [], 1549 ^ [])],extension(1190 ^ 1,bind([[_297117, _297119], [1549 ^ [], 1546 ^ []]]))).
% 2.43/3.44 ncf('1.1.1',plain,[-(human_person(1546 ^ [], 1549 ^ [])), man(1546 ^ [], 1549 ^ [])],extension(1226 ^ 2,bind([[_298377, _298379], [1549 ^ [], 1546 ^ []]]))).
% 2.43/3.44 ncf('1.1.1.1',plain,[-(man(1546 ^ [], 1549 ^ []))],extension(1563 ^ 3)).
% 2.43/3.44 ncf('1.2',plain,[-(nonliving(1546 ^ [], 1549 ^ [])), object(1546 ^ [], 1549 ^ [])],extension(1280 ^ 1,bind([[_300267, _300269], [1549 ^ [], 1546 ^ []]]))).
% 2.43/3.44 ncf('1.2.1',plain,[-(object(1546 ^ [], 1549 ^ [])), artifact(1546 ^ [], 1549 ^ [])],extension(1310 ^ 2,bind([[_301317, _301319], [1549 ^ [], 1546 ^ []]]))).
% 2.43/3.44 ncf('1.2.1.1',plain,[-(artifact(1546 ^ [], 1549 ^ [])), instrumentality(1546 ^ [], 1549 ^ [])],extension(1316 ^ 3,bind([[_301527, _301529], [1549 ^ [], 1546 ^ []]]))).
% 2.43/3.44 ncf('1.2.1.1.1',plain,[-(instrumentality(1546 ^ [], 1549 ^ [])), instrumentality(1546 ^ [], 1559 ^ []), 1546 ^ [] = 1546 ^ [], 1559 ^ [] = 1549 ^ []],extension(258 ^ 4,bind([[_266339, _266341, _266343, _266345], [1549 ^ [], 1559 ^ [], 1546 ^ [], 1546 ^ []]]))).
% 2.43/3.44 ncf('1.2.1.1.1.1',plain,[-(instrumentality(1546 ^ [], 1559 ^ [])), device(1546 ^ [], 1559 ^ [])],extension(1322 ^ 5,bind([[_301737, _301739], [1559 ^ [], 1546 ^ []]]))).
% 2.43/3.44 ncf('1.2.1.1.1.1.1',plain,[-(device(1546 ^ [], 1559 ^ [])), wheel(1546 ^ [], 1559 ^ [])],extension(1328 ^ 6,bind([[_301947, _301949], [1559 ^ [], 1546 ^ []]]))).
% 2.43/3.44 ncf('1.2.1.1.1.1.1.1',plain,[-(wheel(1546 ^ [], 1559 ^ []))],extension(1660 ^ 7)).
% 2.43/3.44 ncf('1.2.1.1.1.2',plain,[-(1546 ^ [] = 1546 ^ [])],extension(2 ^ 5,bind([[_258139], [1546 ^ []]]))).
% 2.43/3.44 ncf('1.2.1.1.1.3',plain,[-(1559 ^ [] = 1549 ^ []), 1549 ^ [] = 1559 ^ []],extension(4 ^ 5,bind([[_258246, _258248], [1559 ^ [], 1549 ^ []]]))).
% 2.43/3.44 ncf('1.2.1.1.1.3.1',plain,[-(1549 ^ [] = 1559 ^ []), be(1546 ^ [], 1558 ^ [], 1549 ^ [], 1559 ^ [])],extension(1541 ^ 6,bind([[_309546, _309548, _309550, _309552], [1559 ^ [], 1549 ^ [], 1558 ^ [], 1546 ^ []]]))).
% 2.43/3.44 ncf('1.2.1.1.1.3.1.1',plain,[-(be(1546 ^ [], 1558 ^ [], 1549 ^ [], 1559 ^ []))],extension(1664 ^ 7)).
% 2.43/3.44 %-----------------------------------------------------
% 2.43/3.44 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------