%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : NLP208+1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n011.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 : 600s
% DateTime : Mon Jul 18 02:59:54 EDT 2022
% Result : Theorem 7.53s 7.64s
% Output : Proof 7.53s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NLP208+1 : TPTP v8.1.0. Released v2.4.0.
% 0.07/0.13 % Command : leancop_casc.sh %s %d
% 0.12/0.34 % Computer : n011.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 : 600
% 0.12/0.34 % DateTime : Fri Jul 1 06:29:33 EDT 2022
% 0.12/0.34 % CPUTime :
% 7.53/7.64 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.53/7.65 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.53/7.66
% 7.53/7.66 %-----------------------------------------------------
% 7.53/7.66 fof(co1, conjecture, ~ ? [_172257] : (actual_world(_172257) & ? [_172272, _172275, _172278, _172281, _172284, _172287, _172290, _172293, _172296, _172299] : (of(_172257, _172275, _172272) & man(_172257, _172272) & jules_forename(_172257, _172275) & forename(_172257, _172275) & frontseat(_172257, _172284) & chevy(_172257, _172278) & white(_172257, _172278) & dirty(_172257, _172278) & old(_172257, _172278) & of(_172257, _172281, _172284) & city(_172257, _172284) & hollywood_placename(_172257, _172281) & placename(_172257, _172281) & street(_172257, _172284) & lonely(_172257, _172284) & event(_172257, _172287) & agent(_172257, _172287, _172278) & present(_172257, _172287) & barrel(_172257, _172287) & down(_172257, _172287, _172284) & in(_172257, _172287, _172284) & ! [_172532] : (member(_172257, _172532, _172290) => ? [_172553, _172556] : (state(_172257, _172553) & be(_172257, _172553, _172532, _172556) & in(_172257, _172556, _172284))) & two(_172257, _172290) & group(_172257, _172290) & ! [_172623] : (member(_172257, _172623, _172290) => fellow(_172257, _172623) & young(_172257, _172623)) & ! [_172664] : (member(_172257, _172664, _172293) => ! [_172685] : (member(_172257, _172685, _172290) => ? [_172706] : (event(_172257, _172706) & agent(_172257, _172706, _172685) & patient(_172257, _172706, _172664) & present(_172257, _172706) & nonreflexive(_172257, _172706) & wear(_172257, _172706)))) & group(_172257, _172293) & ! [_172790] : (member(_172257, _172790, _172293) => coat(_172257, _172790) & black(_172257, _172790) & cheap(_172257, _172790)) & wheel(_172257, _172299) & state(_172257, _172296) & be(_172257, _172296, _172272, _172299) & behind(_172257, _172299, _172299))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', co1)).
% 7.53/7.66 fof(ax25, axiom, ! [_174228, _174231] : (human_person(_174228, _174231) => animate(_174228, _174231)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax25)).
% 7.53/7.66 fof(ax31, axiom, ! [_174379, _174382] : (man(_174379, _174382) => human_person(_174379, _174382)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax31)).
% 7.53/7.66 fof(ax40, axiom, ! [_174533, _174536] : (object(_174533, _174536) => nonliving(_174533, _174536)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax40)).
% 7.53/7.66 fof(ax45, axiom, ! [_174683, _174686] : (artifact(_174683, _174686) => object(_174683, _174686)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax45)).
% 7.53/7.66 fof(ax46, axiom, ! [_174829, _174832] : (instrumentality(_174829, _174832) => artifact(_174829, _174832)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax46)).
% 7.53/7.66 fof(ax47, axiom, ! [_174975, _174978] : (device(_174975, _174978) => instrumentality(_174975, _174978)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax47)).
% 7.53/7.66 fof(ax48, axiom, ! [_175121, _175124] : (wheel(_175121, _175124) => device(_175121, _175124)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax48)).
% 7.53/7.66 fof(ax57, axiom, ! [_175275, _175278] : (animate(_175275, _175278) => ~ nonliving(_175275, _175278)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax57)).
% 7.53/7.66 fof(ax71, axiom, ! [_175439, _175442, _175445, _175448] : (be(_175439, _175442, _175445, _175448) => _175445 = _175448), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax71)).
% 7.53/7.66
% 7.53/7.66 cnf(1, plain, [-(man(4 ^ [], 5 ^ []))], clausify(co1)).
% 7.53/7.66 cnf(2, plain, [-(wheel(4 ^ [], 14 ^ []))], clausify(co1)).
% 7.53/7.66 cnf(3, plain, [-(be(4 ^ [], 13 ^ [], 5 ^ [], 14 ^ []))], clausify(co1)).
% 7.53/7.66 cnf(4, plain, [human_person(_101178, _101223), -(animate(_101178, _101223))], clausify(ax25)).
% 7.53/7.66 cnf(5, plain, [man(_103038, _103083), -(human_person(_103038, _103083))], clausify(ax31)).
% 7.53/7.66 cnf(6, plain, [object(_105828, _105873), -(nonliving(_105828, _105873))], clausify(ax40)).
% 7.53/7.66 cnf(7, plain, [artifact(_107378, _107423), -(object(_107378, _107423))], clausify(ax45)).
% 7.53/7.66 cnf(8, plain, [instrumentality(_107688, _107733), -(artifact(_107688, _107733))], clausify(ax46)).
% 7.53/7.66 cnf(9, plain, [device(_107998, _108043), -(instrumentality(_107998, _108043))], clausify(ax47)).
% 7.53/7.66 cnf(10, plain, [wheel(_108308, _108353), -(device(_108308, _108353))], clausify(ax48)).
% 7.53/7.66 cnf(11, plain, [animate(_111098, _111145), nonliving(_111098, _111145)], clausify(ax57)).
% 7.53/7.66 cnf(12, plain, [be(_118182, _118239, _118295, _118350), -(_118295 = _118350)], clausify(ax71)).
% 7.53/7.66 cnf(13, plain, [-(_44068 = _44068)], theory(equality)).
% 7.53/7.66 cnf(14, plain, [_44221 = _44266, -(_44266 = _44221)], theory(equality)).
% 7.53/7.66 cnf(15, plain, [-(instrumentality(_67814, _67945)), instrumentality(_67747, _67880), _67747 = _67814, _67880 = _67945], theory(equality)).
% 7.53/7.66
% 7.53/7.66 cnf('1',plain,[animate(4 ^ [], 5 ^ []), nonliving(4 ^ [], 5 ^ [])],start(11,bind([[_111098, _111145], [4 ^ [], 5 ^ []]]))).
% 7.53/7.66 cnf('1.1',plain,[-(animate(4 ^ [], 5 ^ [])), human_person(4 ^ [], 5 ^ [])],extension(4,bind([[_101178, _101223], [4 ^ [], 5 ^ []]]))).
% 7.53/7.66 cnf('1.1.1',plain,[-(human_person(4 ^ [], 5 ^ [])), man(4 ^ [], 5 ^ [])],extension(5,bind([[_103038, _103083], [4 ^ [], 5 ^ []]]))).
% 7.53/7.66 cnf('1.1.1.1',plain,[-(man(4 ^ [], 5 ^ []))],extension(1)).
% 7.53/7.66 cnf('1.2',plain,[-(nonliving(4 ^ [], 5 ^ [])), object(4 ^ [], 5 ^ [])],extension(6,bind([[_105828, _105873], [4 ^ [], 5 ^ []]]))).
% 7.53/7.66 cnf('1.2.1',plain,[-(object(4 ^ [], 5 ^ [])), artifact(4 ^ [], 5 ^ [])],extension(7,bind([[_107378, _107423], [4 ^ [], 5 ^ []]]))).
% 7.53/7.66 cnf('1.2.1.1',plain,[-(artifact(4 ^ [], 5 ^ [])), instrumentality(4 ^ [], 5 ^ [])],extension(8,bind([[_107688, _107733], [4 ^ [], 5 ^ []]]))).
% 7.53/7.66 cnf('1.2.1.1.1',plain,[-(instrumentality(4 ^ [], 5 ^ [])), instrumentality(4 ^ [], 14 ^ []), 4 ^ [] = 4 ^ [], 14 ^ [] = 5 ^ []],extension(15,bind([[_67747, _67814, _67880, _67945], [4 ^ [], 4 ^ [], 14 ^ [], 5 ^ []]]))).
% 7.53/7.66 cnf('1.2.1.1.1.1',plain,[-(instrumentality(4 ^ [], 14 ^ [])), device(4 ^ [], 14 ^ [])],extension(9,bind([[_107998, _108043], [4 ^ [], 14 ^ []]]))).
% 7.53/7.66 cnf('1.2.1.1.1.1.1',plain,[-(device(4 ^ [], 14 ^ [])), wheel(4 ^ [], 14 ^ [])],extension(10,bind([[_108308, _108353], [4 ^ [], 14 ^ []]]))).
% 7.53/7.66 cnf('1.2.1.1.1.1.1.1',plain,[-(wheel(4 ^ [], 14 ^ []))],extension(2)).
% 7.53/7.66 cnf('1.2.1.1.1.2',plain,[-(4 ^ [] = 4 ^ [])],extension(13,bind([[_44068], [4 ^ []]]))).
% 7.53/7.66 cnf('1.2.1.1.1.3',plain,[-(14 ^ [] = 5 ^ []), 5 ^ [] = 14 ^ []],extension(14,bind([[_44221, _44266], [5 ^ [], 14 ^ []]]))).
% 7.53/7.66 cnf('1.2.1.1.1.3.1',plain,[-(5 ^ [] = 14 ^ []), be(4 ^ [], 13 ^ [], 5 ^ [], 14 ^ [])],extension(12,bind([[_118182, _118239, _118295, _118350], [4 ^ [], 13 ^ [], 5 ^ [], 14 ^ []]]))).
% 7.53/7.66 cnf('1.2.1.1.1.3.1.1',plain,[-(be(4 ^ [], 13 ^ [], 5 ^ [], 14 ^ []))],extension(3)).
% 7.53/7.66 %-----------------------------------------------------
% 7.53/7.66
% 7.53/7.67 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------