%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : NLP149+1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.sh %s %d
% Computer : n024.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:22 EDT 2022
% Result : Theorem 108.58s 105.68s
% Output : Proof 108.61s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : NLP149+1 : TPTP v8.1.0. Released v2.4.0.
% 0.11/0.12 % Command : leancop_casc.sh %s %d
% 0.11/0.33 % Computer : n024.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 600
% 0.11/0.33 % DateTime : Fri Jul 1 11:26:15 EDT 2022
% 0.11/0.33 % CPUTime :
% 108.58/105.68 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 108.59/105.69 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 108.59/105.70
% 108.59/105.70 %-----------------------------------------------------
% 108.59/105.70 fof(co1, conjecture, ~ ? [_138392] : (actual_world(_138392) & ? [_138407, _138410, _138413, _138416, _138419] : (of(_138392, _138407, _138410) & city(_138392, _138410) & hollywood_placename(_138392, _138407) & placename(_138392, _138407) & street(_138392, _138410) & lonely(_138392, _138410) & chevy(_138392, _138413) & white(_138392, _138413) & dirty(_138392, _138413) & old(_138392, _138413) & event(_138392, _138416) & agent(_138392, _138416, _138413) & present(_138392, _138416) & barrel(_138392, _138416) & down(_138392, _138416, _138410) & in(_138392, _138416, _138410) & ! [_138599] : (member(_138392, _138599, _138419) => ? [_138620, _138623] : (frontseat(_138392, _138623) & state(_138392, _138620) & be(_138392, _138620, _138599, _138623) & in(_138392, _138623, _138623))) & two(_138392, _138419) & group(_138392, _138419) & ! [_138700] : (member(_138392, _138700, _138419) => fellow(_138392, _138700) & young(_138392, _138700)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', co1)).
% 108.59/105.70 fof(ax1, axiom, ! [_139500, _139503] : (furniture(_139500, _139503) => instrumentality(_139500, _139503)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax1)).
% 108.59/105.70 fof(ax2, axiom, ! [_139646, _139649] : (seat(_139646, _139649) => furniture(_139646, _139649)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax2)).
% 108.59/105.70 fof(ax3, axiom, ! [_139792, _139795] : (frontseat(_139792, _139795) => seat(_139792, _139795)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax3)).
% 108.59/105.70 fof(ax18, axiom, ! [_139952, _139955] : (object(_139952, _139955) => nonliving(_139952, _139955)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax18)).
% 108.59/105.70 fof(ax20, axiom, ! [_140099, _140102] : (artifact(_140099, _140102) => object(_140099, _140102)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax20)).
% 108.59/105.70 fof(ax21, axiom, ! [_140245, _140248] : (instrumentality(_140245, _140248) => artifact(_140245, _140248)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax21)).
% 108.59/105.70 fof(ax38, axiom, ! [_140407, _140410] : (human_person(_140407, _140410) => animate(_140407, _140410)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax38)).
% 108.59/105.70 fof(ax48, axiom, ! [_140562, _140565] : (man(_140562, _140565) => human_person(_140562, _140565)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax48)).
% 108.59/105.70 fof(ax49, axiom, ! [_140708, _140711] : (fellow(_140708, _140711) => man(_140708, _140711)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax49)).
% 108.59/105.70 fof(ax50, axiom, ! [_140854, _140857] : (animate(_140854, _140857) => ~ nonliving(_140854, _140857)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax50)).
% 108.59/105.70 fof(ax59, axiom, ! [_141015, _141018, _141021, _141024] : (be(_141015, _141018, _141021, _141024) => _141021 = _141024), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax59)).
% 108.59/105.70 fof(ax60, axiom, ! [_141194, _141197] : (two(_141194, _141197) <=> ? [_141215] : (member(_141194, _141215, _141197) & ? [_141236] : (member(_141194, _141236, _141197) & (! _141236) = _141215 & ! [_141265] : (member(_141194, _141265, _141197) => _141265 = _141236 | _141265 = _141215)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', ax60)).
% 108.59/105.70
% 108.59/105.70 cnf(1, plain, [member(4 ^ [], _113138, 9 ^ []), -(frontseat(4 ^ [], 11 ^ [_113138]))], clausify(co1)).
% 108.59/105.70 cnf(2, plain, [member(4 ^ [], _113138, 9 ^ []), -(be(4 ^ [], 10 ^ [_113138], _113138, 11 ^ [_113138]))], clausify(co1)).
% 108.59/105.70 cnf(3, plain, [-(two(4 ^ [], 9 ^ []))], clausify(co1)).
% 108.59/105.70 cnf(4, plain, [member(4 ^ [], _113196, 9 ^ []), -(fellow(4 ^ [], _113196))], clausify(co1)).
% 108.59/105.70 cnf(5, plain, [furniture(_75256, _75301), -(instrumentality(_75256, _75301))], clausify(ax1)).
% 108.59/105.70 cnf(6, plain, [seat(_75566, _75611), -(furniture(_75566, _75611))], clausify(ax2)).
% 108.59/105.70 cnf(7, plain, [frontseat(_75876, _75921), -(seat(_75876, _75921))], clausify(ax3)).
% 108.59/105.70 cnf(8, plain, [object(_80526, _80571), -(nonliving(_80526, _80571))], clausify(ax18)).
% 108.59/105.70 cnf(9, plain, [artifact(_81146, _81191), -(object(_81146, _81191))], clausify(ax20)).
% 108.59/105.70 cnf(10, plain, [instrumentality(_81456, _81501), -(artifact(_81456, _81501))], clausify(ax21)).
% 108.59/105.70 cnf(11, plain, [human_person(_86726, _86771), -(animate(_86726, _86771))], clausify(ax38)).
% 108.59/105.70 cnf(12, plain, [man(_89826, _89871), -(human_person(_89826, _89871))], clausify(ax48)).
% 108.59/105.70 cnf(13, plain, [fellow(_90136, _90181), -(man(_90136, _90181))], clausify(ax49)).
% 108.59/105.70 cnf(14, plain, [animate(_90446, _90493), nonliving(_90446, _90493)], clausify(ax50)).
% 108.59/105.70 cnf(15, plain, [be(_94043, _94100, _94156, _94211), -(_94156 = _94211)], clausify(ax59)).
% 108.59/105.70 cnf(16, plain, [two(_94580, _94675), -(member(_94580, 1 ^ [_94675, _94580], _94675))], clausify(ax60)).
% 108.59/105.70 cnf(17, plain, [-(_34056 = _34056)], theory(equality)).
% 108.59/105.70 cnf(18, plain, [_34209 = _34254, -(_34254 = _34209)], theory(equality)).
% 108.59/105.70 cnf(19, plain, [-(furniture(_47640, _47771)), furniture(_47573, _47706), _47573 = _47640, _47706 = _47771], theory(equality)).
% 108.59/105.70
% 108.59/105.70 cnf('1',plain,[animate(4 ^ [], 1 ^ [9 ^ [], 4 ^ []]), nonliving(4 ^ [], 1 ^ [9 ^ [], 4 ^ []])],start(14,bind([[_90446, _90493], [4 ^ [], 1 ^ [9 ^ [], 4 ^ []]]]))).
% 108.59/105.70 cnf('1.1',plain,[-(animate(4 ^ [], 1 ^ [9 ^ [], 4 ^ []])), human_person(4 ^ [], 1 ^ [9 ^ [], 4 ^ []])],extension(11,bind([[_86726, _86771], [4 ^ [], 1 ^ [9 ^ [], 4 ^ []]]]))).
% 108.59/105.70 cnf('1.1.1',plain,[-(human_person(4 ^ [], 1 ^ [9 ^ [], 4 ^ []])), man(4 ^ [], 1 ^ [9 ^ [], 4 ^ []])],extension(12,bind([[_89826, _89871], [4 ^ [], 1 ^ [9 ^ [], 4 ^ []]]]))).
% 108.59/105.70 cnf('1.1.1.1',plain,[-(man(4 ^ [], 1 ^ [9 ^ [], 4 ^ []])), fellow(4 ^ [], 1 ^ [9 ^ [], 4 ^ []])],extension(13,bind([[_90136, _90181], [4 ^ [], 1 ^ [9 ^ [], 4 ^ []]]]))).
% 108.59/105.70 cnf('1.1.1.1.1',plain,[-(fellow(4 ^ [], 1 ^ [9 ^ [], 4 ^ []])), member(4 ^ [], 1 ^ [9 ^ [], 4 ^ []], 9 ^ [])],extension(4,bind([[_113196], [1 ^ [9 ^ [], 4 ^ []]]]))).
% 108.59/105.70 cnf('1.1.1.1.1.1',plain,[-(member(4 ^ [], 1 ^ [9 ^ [], 4 ^ []], 9 ^ [])), two(4 ^ [], 9 ^ [])],extension(16,bind([[_94580, _94675], [4 ^ [], 9 ^ []]]))).
% 108.59/105.70 cnf('1.1.1.1.1.1.1',plain,[-(two(4 ^ [], 9 ^ []))],extension(3)).
% 108.59/105.70 cnf('1.2',plain,[-(nonliving(4 ^ [], 1 ^ [9 ^ [], 4 ^ []])), object(4 ^ [], 1 ^ [9 ^ [], 4 ^ []])],extension(8,bind([[_80526, _80571], [4 ^ [], 1 ^ [9 ^ [], 4 ^ []]]]))).
% 108.59/105.70 cnf('1.2.1',plain,[-(object(4 ^ [], 1 ^ [9 ^ [], 4 ^ []])), artifact(4 ^ [], 1 ^ [9 ^ [], 4 ^ []])],extension(9,bind([[_81146, _81191], [4 ^ [], 1 ^ [9 ^ [], 4 ^ []]]]))).
% 108.59/105.70 cnf('1.2.1.1',plain,[-(artifact(4 ^ [], 1 ^ [9 ^ [], 4 ^ []])), instrumentality(4 ^ [], 1 ^ [9 ^ [], 4 ^ []])],extension(10,bind([[_81456, _81501], [4 ^ [], 1 ^ [9 ^ [], 4 ^ []]]]))).
% 108.59/105.70 cnf('1.2.1.1.1',plain,[-(instrumentality(4 ^ [], 1 ^ [9 ^ [], 4 ^ []])), furniture(4 ^ [], 1 ^ [9 ^ [], 4 ^ []])],extension(5,bind([[_75256, _75301], [4 ^ [], 1 ^ [9 ^ [], 4 ^ []]]]))).
% 108.59/105.70 cnf('1.2.1.1.1.1',plain,[-(furniture(4 ^ [], 1 ^ [9 ^ [], 4 ^ []])), furniture(4 ^ [], 11 ^ [1 ^ [9 ^ [], 4 ^ []]]), 4 ^ [] = 4 ^ [], 11 ^ [1 ^ [9 ^ [], 4 ^ []]] = 1 ^ [9 ^ [], 4 ^ []]],extension(19,bind([[_47573, _47640, _47706, _47771], [4 ^ [], 4 ^ [], 11 ^ [1 ^ [9 ^ [], 4 ^ []]], 1 ^ [9 ^ [], 4 ^ []]]]))).
% 108.59/105.70 cnf('1.2.1.1.1.1.1',plain,[-(furniture(4 ^ [], 11 ^ [1 ^ [9 ^ [], 4 ^ []]])), seat(4 ^ [], 11 ^ [1 ^ [9 ^ [], 4 ^ []]])],extension(6,bind([[_75566, _75611], [4 ^ [], 11 ^ [1 ^ [9 ^ [], 4 ^ []]]]]))).
% 108.59/105.70 cnf('1.2.1.1.1.1.1.1',plain,[-(seat(4 ^ [], 11 ^ [1 ^ [9 ^ [], 4 ^ []]])), frontseat(4 ^ [], 11 ^ [1 ^ [9 ^ [], 4 ^ []]])],extension(7,bind([[_75876, _75921], [4 ^ [], 11 ^ [1 ^ [9 ^ [], 4 ^ []]]]]))).
% 108.59/105.70 cnf('1.2.1.1.1.1.1.1.1',plain,[-(frontseat(4 ^ [], 11 ^ [1 ^ [9 ^ [], 4 ^ []]])), member(4 ^ [], 1 ^ [9 ^ [], 4 ^ []], 9 ^ [])],extension(1,bind([[_113138], [1 ^ [9 ^ [], 4 ^ []]]]))).
% 108.59/105.70 cnf('1.2.1.1.1.1.1.1.1.1',plain,[-(member(4 ^ [], 1 ^ [9 ^ [], 4 ^ []], 9 ^ [])), two(4 ^ [], 9 ^ [])],extension(16,bind([[_94580, _94675], [4 ^ [], 9 ^ []]]))).
% 108.59/105.70 cnf('1.2.1.1.1.1.1.1.1.1.1',plain,[-(two(4 ^ [], 9 ^ []))],extension(3)).
% 108.59/105.70 cnf('1.2.1.1.1.1.2',plain,[-(4 ^ [] = 4 ^ [])],extension(17,bind([[_34056], [4 ^ []]]))).
% 108.59/105.70 cnf('1.2.1.1.1.1.3',plain,[-(11 ^ [1 ^ [9 ^ [], 4 ^ []]] = 1 ^ [9 ^ [], 4 ^ []]), 1 ^ [9 ^ [], 4 ^ []] = 11 ^ [1 ^ [9 ^ [], 4 ^ []]]],extension(18,bind([[_34209, _34254], [1 ^ [9 ^ [], 4 ^ []], 11 ^ [1 ^ [9 ^ [], 4 ^ []]]]]))).
% 108.59/105.70 cnf('1.2.1.1.1.1.3.1',plain,[-(1 ^ [9 ^ [], 4 ^ []] = 11 ^ [1 ^ [9 ^ [], 4 ^ []]]), be(4 ^ [], 10 ^ [1 ^ [9 ^ [], 4 ^ []]], 1 ^ [9 ^ [], 4 ^ []], 11 ^ [1 ^ [9 ^ [], 4 ^ []]])],extension(15,bind([[_94043, _94100, _94156, _94211], [4 ^ [], 10 ^ [1 ^ [9 ^ [], 4 ^ []]], 1 ^ [9 ^ [], 4 ^ []], 11 ^ [1 ^ [9 ^ [], 4 ^ []]]]]))).
% 108.59/105.70 cnf('1.2.1.1.1.1.3.1.1',plain,[-(be(4 ^ [], 10 ^ [1 ^ [9 ^ [], 4 ^ []]], 1 ^ [9 ^ [], 4 ^ []], 11 ^ [1 ^ [9 ^ [], 4 ^ []]])), member(4 ^ [], 1 ^ [9 ^ [], 4 ^ []], 9 ^ [])],extension(2,bind([[_113138], [1 ^ [9 ^ [], 4 ^ []]]]))).
% 108.59/105.70 cnf('1.2.1.1.1.1.3.1.1.1',plain,[-(member(4 ^ [], 1 ^ [9 ^ [], 4 ^ []], 9 ^ [])), two(4 ^ [], 9 ^ [])],extension(16,bind([[_94580, _94675], [4 ^ [], 9 ^ []]]))).
% 108.59/105.70 cnf('1.2.1.1.1.1.3.1.1.1.1',plain,[-(two(4 ^ [], 9 ^ []))],extension(3)).
% 108.59/105.70 %-----------------------------------------------------
% 108.61/105.70
% 108.61/105.70 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------