%------------------------------------------------------------------------------
% File : nanoCoP---2.0
% Problem : PUZ031+2 : TPTP v8.1.2. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : nanocop.sh %s %d
% Computer : n006.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:47:53 EDT 2023
% Result : Theorem 0.51s 1.37s
% Output : Proof 0.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : PUZ031+2 : TPTP v8.1.2. Released v4.1.0.
% 0.12/0.12 % Command : nanocop.sh %s %d
% 0.13/0.33 % Computer : n006.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Thu May 18 19:53:06 EDT 2023
% 0.13/0.33 % CPUTime :
% 0.51/1.37
% 0.51/1.37 /export/starexec/sandbox/benchmark/theBenchmark.p is a Theorem
% 0.51/1.37 Start of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.51/1.37 %-----------------------------------------------------
% 0.51/1.37 ncf(matrix, plain, [(184 ^ _30183) ^ [_35862, _35864] : [animal(_35864), animal(_35862), 191 ^ _30183 : [(192 ^ _30183) ^ [_36085] : [grain(_36085), eats(_35862, _36085), eats(_35864, _35862)]]], (3 ^ _30183) ^ [] : [-(wolf(1 ^ []))], (6 ^ _30183) ^ [] : [-(fox(4 ^ []))], (9 ^ _30183) ^ [] : [-(bird(7 ^ []))], (12 ^ _30183) ^ [] : [-(caterpillar(10 ^ []))], (15 ^ _30183) ^ [] : [-(snail(13 ^ []))], (17 ^ _30183) ^ [_30727] : [wolf(_30727), -(animal(_30727))], (23 ^ _30183) ^ [_30913] : [fox(_30913), -(animal(_30913))], (29 ^ _30183) ^ [_31099] : [bird(_31099), -(animal(_31099))], (35 ^ _30183) ^ [_31285] : [caterpillar(_31285), -(animal(_31285))], (41 ^ _30183) ^ [_31471] : [snail(_31471), -(animal(_31471))], (48 ^ _30183) ^ [] : [-(grain(46 ^ []))], (50 ^ _30183) ^ [_31746] : [grain(_31746), -(plant(_31746))], (56 ^ _30183) ^ [_31932] : [animal(_31932), 61 ^ _30183 : [(62 ^ _30183) ^ [_32132] : [plant(_32132), -(eats(_31932, _32132))]], 67 ^ _30183 : [(68 ^ _30183) ^ [_32308] : [-(eats(_31932, _32308)), animal(_32308), much_smaller(_32308, _31932), 77 ^ _30183 : [(78 ^ _30183) ^ [_32569] : [plant(_32569), eats(_32308, _32569)]]]]], (86 ^ _30183) ^ [_32855, _32857] : [-(much_smaller(_32855, _32857)), bird(_32857), snail(_32855)], (96 ^ _30183) ^ [_33150, _33152] : [-(much_smaller(_33150, _33152)), bird(_33152), caterpillar(_33150)], (106 ^ _30183) ^ [_33445, _33447] : [-(much_smaller(_33447, _33445)), bird(_33447), fox(_33445)], (116 ^ _30183) ^ [_33740, _33742] : [-(much_smaller(_33742, _33740)), fox(_33742), wolf(_33740)], (126 ^ _30183) ^ [_34035, _34037] : [eats(_34037, _34035), wolf(_34037), fox(_34035)], (136 ^ _30183) ^ [_34331, _34333] : [eats(_34333, _34331), wolf(_34333), grain(_34331)], (146 ^ _30183) ^ [_34627, _34629] : [-(eats(_34629, _34627)), bird(_34629), caterpillar(_34627)], (156 ^ _30183) ^ [_34922, _34924] : [eats(_34924, _34922), bird(_34924), snail(_34922)], (166 ^ _30183) ^ [_35204] : [caterpillar(_35204), 170 ^ _30183 : [(171 ^ _30183) ^ [] : [-(plant(169 ^ [_35204]))], (173 ^ _30183) ^ [] : [-(eats(_35204, 169 ^ [_35204]))]]], (175 ^ _30183) ^ [_35504] : [snail(_35504), 179 ^ _30183 : [(180 ^ _30183) ^ [] : [-(plant(178 ^ [_35504]))], (182 ^ _30183) ^ [] : [-(eats(_35504, 178 ^ [_35504]))]]]], input).
% 0.51/1.37 ncf('1',plain,[animal(4 ^ []), animal(7 ^ []), 192 : grain(46 ^ []), 192 : eats(7 ^ [], 46 ^ []), 192 : eats(4 ^ [], 7 ^ [])],start(184 ^ 0,bind([[_35862, _35864, _36085], [7 ^ [], 4 ^ [], 46 ^ []]]))).
% 0.51/1.37 ncf('1.1',plain,[-(animal(4 ^ [])), fox(4 ^ [])],extension(23 ^ 1,bind([[_30913], [4 ^ []]]))).
% 0.51/1.37 ncf('1.1.1',plain,[-(fox(4 ^ []))],extension(6 ^ 2)).
% 0.51/1.37 ncf('1.2',plain,[-(animal(7 ^ [])), bird(7 ^ [])],extension(29 ^ 1,bind([[_31099], [7 ^ []]]))).
% 0.51/1.37 ncf('1.2.1',plain,[-(bird(7 ^ []))],extension(9 ^ 2)).
% 0.51/1.37 ncf('1.3',plain,[-(grain(46 ^ []))],extension(48 ^ 3)).
% 0.51/1.37 ncf('1.4',plain,[-(eats(7 ^ [], 46 ^ [])), 62 : plant(46 ^ []), 62 : animal(7 ^ []), 68 : -(eats(7 ^ [], 13 ^ [])), 68 : animal(13 ^ []), 68 : much_smaller(13 ^ [], 7 ^ []), 78 : plant(178 ^ [13 ^ []]), 78 : eats(13 ^ [], 178 ^ [13 ^ []])],extension(56 ^ 3,bind([[_31932, _32132, _32308, _32569], [7 ^ [], 46 ^ [], 13 ^ [], 178 ^ [13 ^ []]]]))).
% 0.51/1.37 ncf('1.4.1',plain,[-(plant(46 ^ [])), grain(46 ^ [])],extension(50 ^ 6,bind([[_31746], [46 ^ []]]))).
% 0.51/1.37 ncf('1.4.1.1',plain,[-(grain(46 ^ []))],lemmata('x')).
% 0.51/1.37 ncf('1.4.2',plain,[-(animal(7 ^ []))],lemmata('x')).
% 0.51/1.37 ncf('1.4.3',plain,[eats(7 ^ [], 13 ^ []), bird(7 ^ []), snail(13 ^ [])],extension(156 ^ 6,bind([[_34922, _34924], [13 ^ [], 7 ^ []]]))).
% 0.51/1.37 ncf('1.4.3.1',plain,[-(bird(7 ^ []))],extension(9 ^ 7)).
% 0.51/1.37 ncf('1.4.3.2',plain,[-(snail(13 ^ []))],extension(15 ^ 7)).
% 0.51/1.37 ncf('1.4.4',plain,[-(animal(13 ^ [])), snail(13 ^ [])],extension(41 ^ 6,bind([[_31471], [13 ^ []]]))).
% 0.51/1.37 ncf('1.4.4.1',plain,[-(snail(13 ^ []))],extension(15 ^ 7)).
% 0.51/1.37 ncf('1.4.5',plain,[-(much_smaller(13 ^ [], 7 ^ [])), bird(7 ^ []), snail(13 ^ [])],extension(86 ^ 6,bind([[_32855, _32857], [13 ^ [], 7 ^ []]]))).
% 0.51/1.37 ncf('1.4.5.1',plain,[-(bird(7 ^ []))],extension(9 ^ 7)).
% 0.51/1.37 ncf('1.4.5.2',plain,[-(snail(13 ^ []))],extension(15 ^ 7)).
% 0.51/1.37 ncf('1.4.6',plain,[-(plant(178 ^ [13 ^ []])), snail(13 ^ [])],extension(175 ^ 8,bind([[_35504], [13 ^ []]]))).
% 0.51/1.37 ncf('1.4.6.1',plain,[-(snail(13 ^ []))],extension(15 ^ 9)).
% 0.51/1.37 ncf('1.4.7',plain,[-(eats(13 ^ [], 178 ^ [13 ^ []])), snail(13 ^ [])],extension(175 ^ 8,bind([[_35504], [13 ^ []]]))).
% 0.51/1.37 ncf('1.4.7.1',plain,[-(snail(13 ^ []))],extension(15 ^ 9)).
% 0.51/1.37 ncf('1.5',plain,[-(eats(4 ^ [], 7 ^ [])), 68 : animal(7 ^ []), 68 : much_smaller(7 ^ [], 4 ^ []), 78 : plant(46 ^ []), 78 : eats(7 ^ [], 46 ^ []), 68 : animal(4 ^ []), 62 : plant(46 ^ []), 62 : -(eats(4 ^ [], 46 ^ []))],extension(56 ^ 3,bind([[_31932, _32308, _32569, _32132], [4 ^ [], 7 ^ [], 46 ^ [], 46 ^ []]]))).
% 0.51/1.37 ncf('1.5.1',plain,[-(animal(7 ^ []))],lemmata('x')).
% 0.51/1.37 ncf('1.5.2',plain,[-(much_smaller(7 ^ [], 4 ^ [])), bird(7 ^ []), fox(4 ^ [])],extension(106 ^ 6,bind([[_33445, _33447], [4 ^ [], 7 ^ []]]))).
% 0.51/1.37 ncf('1.5.2.1',plain,[-(bird(7 ^ []))],extension(9 ^ 7)).
% 0.51/1.37 ncf('1.5.2.2',plain,[-(fox(4 ^ []))],extension(6 ^ 7)).
% 0.51/1.37 ncf('1.5.3',plain,[-(plant(46 ^ [])), grain(46 ^ [])],extension(50 ^ 8,bind([[_31746], [46 ^ []]]))).
% 0.51/1.37 ncf('1.5.3.1',plain,[-(grain(46 ^ []))],extension(48 ^ 9)).
% 0.51/1.37 ncf('1.5.4',plain,[-(eats(7 ^ [], 46 ^ []))],lemmata('x')).
% 0.51/1.37 ncf('1.5.5',plain,[-(animal(4 ^ []))],lemmata('x')).
% 0.51/1.37 ncf('1.5.6',plain,[-(plant(46 ^ [])), grain(46 ^ [])],extension(50 ^ 6,bind([[_31746], [46 ^ []]]))).
% 0.51/1.37 ncf('1.5.6.1',plain,[-(grain(46 ^ []))],extension(48 ^ 7)).
% 0.51/1.37 ncf('1.5.7',plain,[eats(4 ^ [], 46 ^ []), 78 : plant(46 ^ []), 78 : -(eats(1 ^ [], 4 ^ [])), 78 : animal(4 ^ []), 78 : much_smaller(4 ^ [], 1 ^ []), 68 : animal(1 ^ []), 62 : plant(46 ^ []), 62 : -(eats(1 ^ [], 46 ^ []))],extension(56 ^ 6,bind([[_31932, _32308, _32569, _32132], [1 ^ [], 4 ^ [], 46 ^ [], 46 ^ []]]))).
% 0.51/1.37 ncf('1.5.7.1',plain,[-(plant(46 ^ []))],lemmata('[1].x')).
% 0.51/1.37 ncf('1.5.7.2',plain,[eats(1 ^ [], 4 ^ []), wolf(1 ^ []), fox(4 ^ [])],extension(126 ^ 9,bind([[_34035, _34037], [4 ^ [], 1 ^ []]]))).
% 0.51/1.37 ncf('1.5.7.2.1',plain,[-(wolf(1 ^ []))],extension(3 ^ 10)).
% 0.51/1.37 ncf('1.5.7.2.2',plain,[-(fox(4 ^ []))],extension(6 ^ 10)).
% 0.51/1.37 ncf('1.5.7.3',plain,[-(animal(4 ^ []))],lemmata('[1].x')).
% 0.51/1.37 ncf('1.5.7.4',plain,[-(much_smaller(4 ^ [], 1 ^ [])), fox(4 ^ []), wolf(1 ^ [])],extension(116 ^ 9,bind([[_33740, _33742], [1 ^ [], 4 ^ []]]))).
% 0.51/1.37 ncf('1.5.7.4.1',plain,[-(fox(4 ^ []))],extension(6 ^ 10)).
% 0.51/1.37 ncf('1.5.7.4.2',plain,[-(wolf(1 ^ []))],extension(3 ^ 10)).
% 0.51/1.37 ncf('1.5.7.5',plain,[-(animal(1 ^ [])), wolf(1 ^ [])],extension(17 ^ 7,bind([[_30727], [1 ^ []]]))).
% 0.51/1.37 ncf('1.5.7.5.1',plain,[-(wolf(1 ^ []))],extension(3 ^ 8)).
% 0.51/1.37 ncf('1.5.7.6',plain,[-(plant(46 ^ [])), grain(46 ^ [])],extension(50 ^ 9,bind([[_31746], [46 ^ []]]))).
% 0.51/1.37 ncf('1.5.7.6.1',plain,[-(grain(46 ^ []))],extension(48 ^ 10)).
% 0.51/1.37 ncf('1.5.7.7',plain,[eats(1 ^ [], 46 ^ []), wolf(1 ^ []), grain(46 ^ [])],extension(136 ^ 9,bind([[_34331, _34333], [46 ^ [], 1 ^ []]]))).
% 0.51/1.37 ncf('1.5.7.7.1',plain,[-(wolf(1 ^ []))],extension(3 ^ 10)).
% 0.51/1.37 ncf('1.5.7.7.2',plain,[-(grain(46 ^ []))],lemmata('x')).
% 0.51/1.37 %-----------------------------------------------------
% 0.51/1.37 End of proof for /export/starexec/sandbox/benchmark/theBenchmark.p
%------------------------------------------------------------------------------