%------------------------------------------------------------------------------
% File : leanCoP---2.2
% Problem : NLP009+1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : leancop_casc.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 : 600s
% DateTime : Mon Jul 18 02:58:00 EDT 2022
% Result : Theorem 0.38s 1.39s
% Output : Proof 0.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : NLP009+1 : TPTP v8.1.0. Released v2.4.0.
% 0.11/0.12 % Command : leancop_casc.sh %s %d
% 0.11/0.33 % Computer : n015.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 00:50:42 EDT 2022
% 0.11/0.33 % CPUTime :
% 0.38/1.39 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.38/1.40 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.38/1.41
% 0.38/1.41 %-----------------------------------------------------
% 0.38/1.41 fof(co1, conjecture, (? [_70223, _70226, _70229, _70232, _70235, _70238, _70241, _70244, _70247] : (hollywood(_70223) & city(_70223) & event(_70226) & street(_70229) & way(_70229) & lonely(_70229) & chevy(_70232) & car(_70232) & white(_70232) & dirty(_70232) & old(_70232) & barrel(_70226, _70232) & down(_70226, _70229) & in(_70226, _70223) & seat(_70241) & furniture(_70241) & front(_70241) & (! _70235) = _70238 & fellow(_70235) & man(_70235) & young(_70235) & fellow(_70238) & man(_70238) & young(_70238) & _70235 = _70244 & in(_70244, _70241) & _70238 = _70247 & in(_70247, _70241)) => ? [_70465, _70468, _70471, _70474, _70477, _70480, _70483, _70486, _70489] : (hollywood(_70465) & city(_70465) & event(_70468) & chevy(_70471) & car(_70471) & white(_70471) & dirty(_70471) & old(_70471) & street(_70474) & way(_70474) & lonely(_70474) & barrel(_70468, _70471) & down(_70468, _70474) & in(_70468, _70465) & seat(_70483) & furniture(_70483) & front(_70483) & (! _70477) = _70480 & fellow(_70477) & man(_70477) & young(_70477) & fellow(_70480) & man(_70480) & young(_70480) & _70477 = _70486 & in(_70486, _70483) & _70480 = _70489 & in(_70489, _70483))) & (? [_70707, _70710, _70713, _70716, _70719, _70722, _70725, _70728, _70731] : (hollywood(_70707) & city(_70707) & event(_70710) & chevy(_70713) & car(_70713) & white(_70713) & dirty(_70713) & old(_70713) & street(_70716) & way(_70716) & lonely(_70716) & barrel(_70710, _70713) & down(_70710, _70716) & in(_70710, _70707) & seat(_70725) & furniture(_70725) & front(_70725) & (! _70719) = _70722 & fellow(_70719) & man(_70719) & young(_70719) & fellow(_70722) & man(_70722) & young(_70722) & _70719 = _70728 & in(_70728, _70725) & _70722 = _70731 & in(_70731, _70725)) => ? [_70949, _70952, _70955, _70958, _70961, _70964, _70967, _70970, _70973] : (hollywood(_70949) & city(_70949) & event(_70952) & street(_70955) & way(_70955) & lonely(_70955) & chevy(_70958) & car(_70958) & white(_70958) & dirty(_70958) & old(_70958) & barrel(_70952, _70958) & down(_70952, _70955) & in(_70952, _70949) & seat(_70967) & furniture(_70967) & front(_70967) & (! _70961) = _70964 & fellow(_70961) & man(_70961) & young(_70961) & fellow(_70964) & man(_70964) & young(_70964) & _70961 = _70970 & in(_70970, _70967) & _70964 = _70973 & in(_70973, _70967))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', co1)).
% 0.38/1.41
% 0.38/1.41 cnf(1, plain, [-(20 ^ []), hollywood(_34542), city(_34542), event(_34761), street(_34979), way(_34979), lonely(_34979), chevy(_35196), car(_35196), white(_35196), dirty(_35196), old(_35196), barrel(_34761, _35196), down(_34761, _34979), in(_34761, _34542), seat(_35841), furniture(_35841), front(_35841), -(_35412 = _35627), fellow(_35412), man(_35412), young(_35412), fellow(_35627), man(_35627), young(_35627), _35412 = _36054, in(_36054, _35841), _35627 = _36266, in(_36266, _35841)], clausify(co1)).
% 0.38/1.41 cnf(2, plain, [-(20 ^ []), -(in(19 ^ [], 17 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(3, plain, [-(20 ^ []), -(16 ^ [] = 19 ^ [])], clausify(co1)).
% 0.38/1.41 cnf(4, plain, [-(20 ^ []), -(in(18 ^ [], 17 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(5, plain, [-(20 ^ []), -(15 ^ [] = 18 ^ [])], clausify(co1)).
% 0.38/1.41 cnf(6, plain, [-(20 ^ []), -(young(16 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(7, plain, [-(20 ^ []), -(man(16 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(8, plain, [-(20 ^ []), -(fellow(16 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(9, plain, [-(20 ^ []), -(young(15 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(10, plain, [-(20 ^ []), -(man(15 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(11, plain, [-(20 ^ []), -(fellow(15 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(12, plain, [-(20 ^ []), 15 ^ [] = 16 ^ []], clausify(co1)).
% 0.38/1.41 cnf(13, plain, [-(20 ^ []), -(front(17 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(14, plain, [-(20 ^ []), -(furniture(17 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(15, plain, [-(20 ^ []), -(seat(17 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(16, plain, [-(20 ^ []), -(in(12 ^ [], 11 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(17, plain, [-(20 ^ []), -(down(12 ^ [], 14 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(18, plain, [-(20 ^ []), -(barrel(12 ^ [], 13 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(19, plain, [-(20 ^ []), -(lonely(14 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(20, plain, [-(20 ^ []), -(way(14 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(21, plain, [-(20 ^ []), -(street(14 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(22, plain, [-(20 ^ []), -(old(13 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(23, plain, [-(20 ^ []), -(dirty(13 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(24, plain, [-(20 ^ []), -(white(13 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(25, plain, [-(20 ^ []), -(car(13 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(26, plain, [-(20 ^ []), -(chevy(13 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(27, plain, [-(20 ^ []), -(event(12 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(28, plain, [-(20 ^ []), -(city(11 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(29, plain, [-(20 ^ []), -(hollywood(11 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(30, plain, [-(10 ^ []), hollywood(_27235), city(_27235), event(_27454), chevy(_27672), car(_27672), white(_27672), dirty(_27672), old(_27672), street(_27889), way(_27889), lonely(_27889), barrel(_27454, _27672), down(_27454, _27889), in(_27454, _27235), seat(_28534), furniture(_28534), front(_28534), -(_28105 = _28320), fellow(_28105), man(_28105), young(_28105), fellow(_28320), man(_28320), young(_28320), _28105 = _28747, in(_28747, _28534), _28320 = _28959, in(_28959, _28534)], clausify(co1)).
% 0.38/1.41 cnf(31, plain, [-(10 ^ []), -(in(9 ^ [], 7 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(32, plain, [-(10 ^ []), -(6 ^ [] = 9 ^ [])], clausify(co1)).
% 0.38/1.41 cnf(33, plain, [-(10 ^ []), -(in(8 ^ [], 7 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(34, plain, [-(10 ^ []), -(5 ^ [] = 8 ^ [])], clausify(co1)).
% 0.38/1.41 cnf(35, plain, [-(10 ^ []), -(young(6 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(36, plain, [-(10 ^ []), -(man(6 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(37, plain, [-(10 ^ []), -(fellow(6 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(38, plain, [-(10 ^ []), -(young(5 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(39, plain, [-(10 ^ []), -(man(5 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(40, plain, [-(10 ^ []), -(fellow(5 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(41, plain, [-(10 ^ []), 5 ^ [] = 6 ^ []], clausify(co1)).
% 0.38/1.41 cnf(42, plain, [-(10 ^ []), -(front(7 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(43, plain, [-(10 ^ []), -(furniture(7 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(44, plain, [-(10 ^ []), -(seat(7 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(45, plain, [-(10 ^ []), -(in(2 ^ [], 1 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(46, plain, [-(10 ^ []), -(down(2 ^ [], 3 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(47, plain, [-(10 ^ []), -(barrel(2 ^ [], 4 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(48, plain, [-(10 ^ []), -(old(4 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(49, plain, [-(10 ^ []), -(dirty(4 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(50, plain, [-(10 ^ []), -(white(4 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(51, plain, [-(10 ^ []), -(car(4 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(52, plain, [-(10 ^ []), -(chevy(4 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(53, plain, [-(10 ^ []), -(lonely(3 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(54, plain, [-(10 ^ []), -(way(3 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(55, plain, [-(10 ^ []), -(street(3 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(56, plain, [-(10 ^ []), -(event(2 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(57, plain, [-(10 ^ []), -(city(1 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(58, plain, [-(10 ^ []), -(hollywood(1 ^ []))], clausify(co1)).
% 0.38/1.41 cnf(59, plain, [10 ^ [], 20 ^ []], clausify(co1)).
% 0.38/1.41
% 0.38/1.41 cnf('1',plain,[10 ^ [], 20 ^ []],start(59)).
% 0.38/1.41 cnf('1.1',plain,[-(10 ^ []), hollywood(1 ^ []), city(1 ^ []), event(2 ^ []), chevy(4 ^ []), car(4 ^ []), white(4 ^ []), dirty(4 ^ []), old(4 ^ []), street(3 ^ []), way(3 ^ []), lonely(3 ^ []), barrel(2 ^ [], 4 ^ []), down(2 ^ [], 3 ^ []), in(2 ^ [], 1 ^ []), seat(7 ^ []), furniture(7 ^ []), front(7 ^ []), -(5 ^ [] = 6 ^ []), fellow(5 ^ []), man(5 ^ []), young(5 ^ []), fellow(6 ^ []), man(6 ^ []), young(6 ^ []), 5 ^ [] = 8 ^ [], in(8 ^ [], 7 ^ []), 6 ^ [] = 9 ^ [], in(9 ^ [], 7 ^ [])],extension(30,bind([[_27672, _27889, _27454, _27235, _28105, _28747, _28320, _28959, _28534], [4 ^ [], 3 ^ [], 2 ^ [], 1 ^ [], 5 ^ [], 8 ^ [], 6 ^ [], 9 ^ [], 7 ^ []]]))).
% 0.38/1.41 cnf('1.1.1',plain,[-(hollywood(1 ^ [])), -(10 ^ [])],extension(58)).
% 0.38/1.41 cnf('1.1.1.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.2',plain,[-(city(1 ^ [])), -(10 ^ [])],extension(57)).
% 0.38/1.41 cnf('1.1.2.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.3',plain,[-(event(2 ^ [])), -(10 ^ [])],extension(56)).
% 0.38/1.41 cnf('1.1.3.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.4',plain,[-(chevy(4 ^ [])), -(10 ^ [])],extension(52)).
% 0.38/1.41 cnf('1.1.4.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.5',plain,[-(car(4 ^ [])), -(10 ^ [])],extension(51)).
% 0.38/1.41 cnf('1.1.5.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.6',plain,[-(white(4 ^ [])), -(10 ^ [])],extension(50)).
% 0.38/1.41 cnf('1.1.6.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.7',plain,[-(dirty(4 ^ [])), -(10 ^ [])],extension(49)).
% 0.38/1.41 cnf('1.1.7.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.8',plain,[-(old(4 ^ [])), -(10 ^ [])],extension(48)).
% 0.38/1.41 cnf('1.1.8.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.9',plain,[-(street(3 ^ [])), -(10 ^ [])],extension(55)).
% 0.38/1.41 cnf('1.1.9.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.10',plain,[-(way(3 ^ [])), -(10 ^ [])],extension(54)).
% 0.38/1.41 cnf('1.1.10.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.11',plain,[-(lonely(3 ^ [])), -(10 ^ [])],extension(53)).
% 0.38/1.41 cnf('1.1.11.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.12',plain,[-(barrel(2 ^ [], 4 ^ [])), -(10 ^ [])],extension(47)).
% 0.38/1.41 cnf('1.1.12.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.13',plain,[-(down(2 ^ [], 3 ^ [])), -(10 ^ [])],extension(46)).
% 0.38/1.41 cnf('1.1.13.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.14',plain,[-(in(2 ^ [], 1 ^ [])), -(10 ^ [])],extension(45)).
% 0.38/1.41 cnf('1.1.14.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.15',plain,[-(seat(7 ^ [])), -(10 ^ [])],extension(44)).
% 0.38/1.41 cnf('1.1.15.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.16',plain,[-(furniture(7 ^ [])), -(10 ^ [])],extension(43)).
% 0.38/1.41 cnf('1.1.16.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.17',plain,[-(front(7 ^ [])), -(10 ^ [])],extension(42)).
% 0.38/1.41 cnf('1.1.17.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.18',plain,[5 ^ [] = 6 ^ [], -(10 ^ [])],extension(41)).
% 0.38/1.41 cnf('1.1.18.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.19',plain,[-(fellow(5 ^ [])), -(10 ^ [])],extension(40)).
% 0.38/1.41 cnf('1.1.19.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.20',plain,[-(man(5 ^ [])), -(10 ^ [])],extension(39)).
% 0.38/1.41 cnf('1.1.20.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.21',plain,[-(young(5 ^ [])), -(10 ^ [])],extension(38)).
% 0.38/1.41 cnf('1.1.21.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.22',plain,[-(fellow(6 ^ [])), -(10 ^ [])],extension(37)).
% 0.38/1.41 cnf('1.1.22.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.23',plain,[-(man(6 ^ [])), -(10 ^ [])],extension(36)).
% 0.38/1.41 cnf('1.1.23.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.24',plain,[-(young(6 ^ [])), -(10 ^ [])],extension(35)).
% 0.38/1.41 cnf('1.1.24.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.25',plain,[-(5 ^ [] = 8 ^ []), -(10 ^ [])],extension(34)).
% 0.38/1.41 cnf('1.1.25.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.26',plain,[-(in(8 ^ [], 7 ^ [])), -(10 ^ [])],extension(33)).
% 0.38/1.41 cnf('1.1.26.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.27',plain,[-(6 ^ [] = 9 ^ []), -(10 ^ [])],extension(32)).
% 0.38/1.41 cnf('1.1.27.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.1.28',plain,[-(in(9 ^ [], 7 ^ [])), -(10 ^ [])],extension(31)).
% 0.38/1.41 cnf('1.1.28.1',plain,[10 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2',plain,[-(20 ^ []), hollywood(11 ^ []), city(11 ^ []), event(12 ^ []), street(14 ^ []), way(14 ^ []), lonely(14 ^ []), chevy(13 ^ []), car(13 ^ []), white(13 ^ []), dirty(13 ^ []), old(13 ^ []), barrel(12 ^ [], 13 ^ []), down(12 ^ [], 14 ^ []), in(12 ^ [], 11 ^ []), seat(17 ^ []), furniture(17 ^ []), front(17 ^ []), -(15 ^ [] = 16 ^ []), fellow(15 ^ []), man(15 ^ []), young(15 ^ []), fellow(16 ^ []), man(16 ^ []), young(16 ^ []), 15 ^ [] = 18 ^ [], in(18 ^ [], 17 ^ []), 16 ^ [] = 19 ^ [], in(19 ^ [], 17 ^ [])],extension(1,bind([[_35196, _34979, _34761, _34542, _35412, _36054, _35627, _36266, _35841], [13 ^ [], 14 ^ [], 12 ^ [], 11 ^ [], 15 ^ [], 18 ^ [], 16 ^ [], 19 ^ [], 17 ^ []]]))).
% 0.38/1.41 cnf('1.2.1',plain,[-(hollywood(11 ^ [])), -(20 ^ [])],extension(29)).
% 0.38/1.41 cnf('1.2.1.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.2',plain,[-(city(11 ^ [])), -(20 ^ [])],extension(28)).
% 0.38/1.41 cnf('1.2.2.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.3',plain,[-(event(12 ^ [])), -(20 ^ [])],extension(27)).
% 0.38/1.41 cnf('1.2.3.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.4',plain,[-(street(14 ^ [])), -(20 ^ [])],extension(21)).
% 0.38/1.41 cnf('1.2.4.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.5',plain,[-(way(14 ^ [])), -(20 ^ [])],extension(20)).
% 0.38/1.41 cnf('1.2.5.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.6',plain,[-(lonely(14 ^ [])), -(20 ^ [])],extension(19)).
% 0.38/1.41 cnf('1.2.6.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.7',plain,[-(chevy(13 ^ [])), -(20 ^ [])],extension(26)).
% 0.38/1.41 cnf('1.2.7.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.8',plain,[-(car(13 ^ [])), -(20 ^ [])],extension(25)).
% 0.38/1.41 cnf('1.2.8.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.9',plain,[-(white(13 ^ [])), -(20 ^ [])],extension(24)).
% 0.38/1.41 cnf('1.2.9.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.10',plain,[-(dirty(13 ^ [])), -(20 ^ [])],extension(23)).
% 0.38/1.41 cnf('1.2.10.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.11',plain,[-(old(13 ^ [])), -(20 ^ [])],extension(22)).
% 0.38/1.41 cnf('1.2.11.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.12',plain,[-(barrel(12 ^ [], 13 ^ [])), -(20 ^ [])],extension(18)).
% 0.38/1.41 cnf('1.2.12.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.13',plain,[-(down(12 ^ [], 14 ^ [])), -(20 ^ [])],extension(17)).
% 0.38/1.41 cnf('1.2.13.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.14',plain,[-(in(12 ^ [], 11 ^ [])), -(20 ^ [])],extension(16)).
% 0.38/1.41 cnf('1.2.14.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.15',plain,[-(seat(17 ^ [])), -(20 ^ [])],extension(15)).
% 0.38/1.41 cnf('1.2.15.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.16',plain,[-(furniture(17 ^ [])), -(20 ^ [])],extension(14)).
% 0.38/1.41 cnf('1.2.16.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.17',plain,[-(front(17 ^ [])), -(20 ^ [])],extension(13)).
% 0.38/1.41 cnf('1.2.17.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.18',plain,[15 ^ [] = 16 ^ [], -(20 ^ [])],extension(12)).
% 0.38/1.41 cnf('1.2.18.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.19',plain,[-(fellow(15 ^ [])), -(20 ^ [])],extension(11)).
% 0.38/1.41 cnf('1.2.19.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.20',plain,[-(man(15 ^ [])), -(20 ^ [])],extension(10)).
% 0.38/1.41 cnf('1.2.20.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.21',plain,[-(young(15 ^ [])), -(20 ^ [])],extension(9)).
% 0.38/1.41 cnf('1.2.21.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.22',plain,[-(fellow(16 ^ [])), -(20 ^ [])],extension(8)).
% 0.38/1.41 cnf('1.2.22.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.23',plain,[-(man(16 ^ [])), -(20 ^ [])],extension(7)).
% 0.38/1.41 cnf('1.2.23.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.24',plain,[-(young(16 ^ [])), -(20 ^ [])],extension(6)).
% 0.38/1.41 cnf('1.2.24.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.25',plain,[-(15 ^ [] = 18 ^ []), -(20 ^ [])],extension(5)).
% 0.38/1.41 cnf('1.2.25.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.26',plain,[-(in(18 ^ [], 17 ^ [])), -(20 ^ [])],extension(4)).
% 0.38/1.41 cnf('1.2.26.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.27',plain,[-(16 ^ [] = 19 ^ []), -(20 ^ [])],extension(3)).
% 0.38/1.41 cnf('1.2.27.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 cnf('1.2.28',plain,[-(in(19 ^ [], 17 ^ [])), -(20 ^ [])],extension(2)).
% 0.38/1.41 cnf('1.2.28.1',plain,[20 ^ []],reduction('1')).
% 0.38/1.41 %-----------------------------------------------------
% 0.38/1.41
% 0.38/1.41 % SZS output end Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------