problem-set/puzzles/carroll/lizard.ver1.out created : 07/19/88 revised : 07/19/88 OTTER version 0.91, 14 June 1988. set(hyper_res). set(UR_res). set(binary_res). list(sos). 12 -CUNNING(x) | -SAVAGE(x) | DESTRUCTIVE(x). 13 -FAT(x) | -LAZY(x) | -CLIMB_TREES(x). 14 -POISONOUS(x) | -HAS_CLAWS(x) | WRIGGLES(x). 15 -CLIMB_TREES(x) | -LIZARD(x) | DESTRUCTIVE(x). 16 CLIMB_TREES(x) | -LIZARD(x) | -DESTRUCTIVE(x). 17 -HAS_CLAWS(x) | HAS_SCALES(x) | FAT(x). 18 -GRINNING(x) | -DREADED(x) | HAS_CLAWS(x). 19 -ACTIVE(x) | -DESTRUCTIVE(x) | -FAT(x). 20 -HAS_SCALES(x) | -DREADED(x) | POISONOUS(x). 21 -GRINNING(x) | -HAS_CLAWS(x) | CUNNING(x). 22 -SAVAGE(x) | -LIZARD(x) | DREADED(x). end_of_list. new given clause: 12 -CUNNING(x) | -SAVAGE(x) | DESTRUCTIVE(x). ** KEPT: 23 (12,10) -SAVAGE(x) | DESTRUCTIVE(x) | -GRINNING(x) | -HAS_CLAWS(x). ** KEPT: 24 (12,8) -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x) | -FAT(x). ** KEPT: 25 (12,5) -CUNNING(x) | -SAVAGE(x) | CLIMB_TREES(x) | -LIZARD(x). new given clause: 13 -FAT(x) | -LAZY(x) | -CLIMB_TREES(x). ** KEPT: 26 (13,6) -LAZY(x) | -CLIMB_TREES(x) | -HAS_CLAWS(x) | HAS_SCALES(x). ** KEPT: 27 (13,5) -FAT(x) | -LAZY(x) | -LIZARD(x) | -DESTRUCTIVE(x). new given clause: 14 -POISONOUS(x) | -HAS_CLAWS(x) | WRIGGLES(x). ** KEPT: 28 (14,9) -HAS_CLAWS(x) | WRIGGLES(x) | -HAS_SCALES(x) | -DREADED(x). ** KEPT: 29 (14,7) -POISONOUS(x) | WRIGGLES(x) | -GRINNING(x) | -DREADED(x). new given clause: 15 -CLIMB_TREES(x) | -LIZARD(x) | DESTRUCTIVE(x). ** KEPT: 30 (15,8) -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x) | -FAT(x). new given clause: 16 CLIMB_TREES(x) | -LIZARD(x) | -DESTRUCTIVE(x). new given clause: 17 -HAS_CLAWS(x) | HAS_SCALES(x) | FAT(x). ** KEPT: 31 (17,7) HAS_SCALES(x) | FAT(x) | -GRINNING(x) | -DREADED(x). ** KEPT: 32 (17,9) -HAS_CLAWS(x) | FAT(x) | -DREADED(x) | POISONOUS(x). ** KEPT: 33 (17,8) -HAS_CLAWS(x) | HAS_SCALES(x) | -ACTIVE(x) | -DESTRUCTIVE(x). new given clause: 18 -GRINNING(x) | -DREADED(x) | HAS_CLAWS(x). ** KEPT: 34 (18,11) -GRINNING(x) | HAS_CLAWS(x) | -SAVAGE(x) | -LIZARD(x). ** KEPT: 35 (18,10) -GRINNING(x) | -DREADED(x) | CUNNING(x). new given clause: 19 -ACTIVE(x) | -DESTRUCTIVE(x) | -FAT(x). new given clause: 20 -HAS_SCALES(x) | -DREADED(x) | POISONOUS(x). ** KEPT: 36 (20,11) -HAS_SCALES(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x). new given clause: 21 -GRINNING(x) | -HAS_CLAWS(x) | CUNNING(x). new given clause: 22 -SAVAGE(x) | -LIZARD(x) | DREADED(x). new given clause: 35 (18,10) -GRINNING(x) | -DREADED(x) | CUNNING(x). ** KEPT: 37 (35,22) -GRINNING(x) | CUNNING(x) | -SAVAGE(x) | -LIZARD(x). ** KEPT: 38 (35,12) -GRINNING(x) | -DREADED(x) | -SAVAGE(x) | DESTRUCTIVE(x). new given clause: 23 (12,10) -SAVAGE(x) | DESTRUCTIVE(x) | -GRINNING(x) | -HAS_CLAWS(x). ** KEPT: 39 (23,19) -SAVAGE(x) | -GRINNING(x) | -HAS_CLAWS(x) | -ACTIVE(x) | -FAT(x). ** KEPT: 40 (23,16) -SAVAGE(x) | -GRINNING(x) | -HAS_CLAWS(x) | CLIMB_TREES(x) | -LIZARD(x). new given clause: 24 (12,8) -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x) | -FAT(x). ** KEPT: 41 (24,35) -SAVAGE(x) | -ACTIVE(x) | -FAT(x) | -GRINNING(x) | -DREADED(x). ** KEPT: 42 (24,17) -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x) | -HAS_CLAWS(x) | HAS_SCALES(x). new given clause: 25 (12,5) -CUNNING(x) | -SAVAGE(x) | CLIMB_TREES(x) | -LIZARD(x). ** KEPT: 43 (25,35) -SAVAGE(x) | CLIMB_TREES(x) | -LIZARD(x) | -GRINNING(x) | -DREADED(x). ** KEPT: 44 (25,13) -CUNNING(x) | -SAVAGE(x) | -LIZARD(x) | -FAT(x) | -LAZY(x). new given clause: 26 (13,6) -LAZY(x) | -CLIMB_TREES(x) | -HAS_CLAWS(x) | HAS_SCALES(x). ** KEPT: 45 (26,25) -LAZY(x) | -HAS_CLAWS(x) | HAS_SCALES(x) | -CUNNING(x) | -SAVAGE(x) | -LIZARD(x). ** KEPT: 46 (26,16) -LAZY(x) | -HAS_CLAWS(x) | HAS_SCALES(x) | -LIZARD(x) | -DESTRUCTIVE(x). ** KEPT: 47 (26,18) -LAZY(x) | -CLIMB_TREES(x) | HAS_SCALES(x) | -GRINNING(x) | -DREADED(x). ** KEPT: 48 (26,20) -LAZY(x) | -CLIMB_TREES(x) | -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x). new given clause: 27 (13,5) -FAT(x) | -LAZY(x) | -LIZARD(x) | -DESTRUCTIVE(x). ** KEPT: 49 (27,23) -FAT(x) | -LAZY(x) | -LIZARD(x) | -SAVAGE(x) | -GRINNING(x) | -HAS_CLAWS(x). new given clause: 28 (14,9) -HAS_CLAWS(x) | WRIGGLES(x) | -HAS_SCALES(x) | -DREADED(x). ** KEPT: 50 (28,18) WRIGGLES(x) | -HAS_SCALES(x) | -DREADED(x) | -GRINNING(x). ** KEPT: 51 (28,26) -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x) | -LAZY(x) | -CLIMB_TREES(x). ** KEPT: 52 (28,17) -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x) | FAT(x). ** KEPT: 53 (28,22) -HAS_CLAWS(x) | WRIGGLES(x) | -HAS_SCALES(x) | -SAVAGE(x) | -LIZARD(x). new given clause: 29 (14,7) -POISONOUS(x) | WRIGGLES(x) | -GRINNING(x) | -DREADED(x). ** KEPT: 54 (29,22) -POISONOUS(x) | WRIGGLES(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x). new given clause: 30 (15,8) -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x) | -FAT(x). ** KEPT: 55 (30,17) -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x) | -HAS_CLAWS(x) | HAS_SCALES(x). new given clause: 31 (17,7) HAS_SCALES(x) | FAT(x) | -GRINNING(x) | -DREADED(x). ** KEPT: 56 (31,20) FAT(x) | -GRINNING(x) | -DREADED(x) | POISONOUS(x). ** KEPT: 57 (31,30) HAS_SCALES(x) | -GRINNING(x) | -DREADED(x) | -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x). ** KEPT: 58 (31,27) HAS_SCALES(x) | -GRINNING(x) | -DREADED(x) | -LAZY(x) | -LIZARD(x) | -DESTRUCTIVE(x). ** KEPT: 59 (31,24) HAS_SCALES(x) | -GRINNING(x) | -DREADED(x) | -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x). ** KEPT: 60 (31,19) HAS_SCALES(x) | -GRINNING(x) | -DREADED(x) | -ACTIVE(x) | -DESTRUCTIVE(x). ** KEPT: 61 (31,22) HAS_SCALES(x) | FAT(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x). new given clause: 32 (17,9) -HAS_CLAWS(x) | FAT(x) | -DREADED(x) | POISONOUS(x). ** KEPT: 62 (32,30) -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x) | -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x). ** KEPT: 63 (32,27) -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x) | -LAZY(x) | -LIZARD(x) | -DESTRUCTIVE(x). ** KEPT: 64 (32,24) -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x) | -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x). ** KEPT: 65 (32,19) -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x) | -ACTIVE(x) | -DESTRUCTIVE(x). ** KEPT: 66 (32,22) -HAS_CLAWS(x) | FAT(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x). new given clause: 33 (17,8) -HAS_CLAWS(x) | HAS_SCALES(x) | -ACTIVE(x) | -DESTRUCTIVE(x). ** KEPT: 67 (33,28) -HAS_CLAWS(x) | -ACTIVE(x) | -DESTRUCTIVE(x) | WRIGGLES(x) | -DREADED(x). ** KEPT: 68 (33,23) -HAS_CLAWS(x) | HAS_SCALES(x) | -ACTIVE(x) | -SAVAGE(x) | -GRINNING(x). new given clause: 34 (18,11) -GRINNING(x) | HAS_CLAWS(x) | -SAVAGE(x) | -LIZARD(x). ** KEPT: 69 (34,33) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | HAS_SCALES(x) | -ACTIVE(x) | -DESTRUCTIVE(x). ** KEPT: 70 (34,26) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -CLIMB_TREES(x) | HAS_SCALES(x). ** KEPT: 71 (34,23) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | DESTRUCTIVE(x). new given clause: 36 (20,11) -HAS_SCALES(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x). ** KEPT: 72 (36,33) POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -HAS_CLAWS(x) | -ACTIVE(x) | -DESTRUCTIVE(x). ** KEPT: 73 (36,26) POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -CLIMB_TREES(x) | -HAS_CLAWS(x). new given clause: 37 (35,22) -GRINNING(x) | CUNNING(x) | -SAVAGE(x) | -LIZARD(x). ** KEPT: 74 (37,25) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | CLIMB_TREES(x). ** KEPT: 75 (37,24) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -ACTIVE(x) | -FAT(x). 74 back subsumes: 43 (25,35) -SAVAGE(x) | CLIMB_TREES(x) | -LIZARD(x) | -GRINNING(x) | -DREADED(x). 74 back subsumes: 40 (23,16) -SAVAGE(x) | -GRINNING(x) | -HAS_CLAWS(x) | CLIMB_TREES(x) | -LIZARD(x). new given clause: 38 (35,12) -GRINNING(x) | -DREADED(x) | -SAVAGE(x) | DESTRUCTIVE(x). ** KEPT: 76 (38,27) -GRINNING(x) | -DREADED(x) | -SAVAGE(x) | -FAT(x) | -LAZY(x) | -LIZARD(x). new given clause: 50 (28,18) WRIGGLES(x) | -HAS_SCALES(x) | -DREADED(x) | -GRINNING(x). ** KEPT: 77 (50,31) WRIGGLES(x) | -DREADED(x) | -GRINNING(x) | FAT(x). ** KEPT: 78 (50,22) WRIGGLES(x) | -HAS_SCALES(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x). new given clause: 52 (28,17) -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x) | FAT(x). ** KEPT: 79 (52,22) -HAS_CLAWS(x) | WRIGGLES(x) | FAT(x) | -SAVAGE(x) | -LIZARD(x). ** KEPT: 80 (52,30) -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x) | -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x). ** KEPT: 81 (52,27) -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x) | -LAZY(x) | -LIZARD(x) | -DESTRUCTIVE(x). ** KEPT: 82 (52,24) -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x) | -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x). new given clause: 56 (31,20) FAT(x) | -GRINNING(x) | -DREADED(x) | POISONOUS(x). ** KEPT: 83 (56,30) -GRINNING(x) | -DREADED(x) | POISONOUS(x) | -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x). ** KEPT: 84 (56,27) -GRINNING(x) | -DREADED(x) | POISONOUS(x) | -LAZY(x) | -LIZARD(x) | -DESTRUCTIVE(x). ** KEPT: 85 (56,24) -GRINNING(x) | -DREADED(x) | POISONOUS(x) | -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x). ** KEPT: 86 (56,19) -GRINNING(x) | -DREADED(x) | POISONOUS(x) | -ACTIVE(x) | -DESTRUCTIVE(x). ** KEPT: 87 (56,13) -GRINNING(x) | -DREADED(x) | POISONOUS(x) | -LAZY(x) | -CLIMB_TREES(x). ** KEPT: 88 (56,22) FAT(x) | -GRINNING(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x). new given clause: 71 (34,23) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | DESTRUCTIVE(x). ** KEPT: 89 (71,27) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -FAT(x) | -LAZY(x). 89 back subsumes: 76 (38,27) -GRINNING(x) | -DREADED(x) | -SAVAGE(x) | -FAT(x) | -LAZY(x) | -LIZARD(x). 89 back subsumes: 49 (27,23) -FAT(x) | -LAZY(x) | -LIZARD(x) | -SAVAGE(x) | -GRINNING(x) | -HAS_CLAWS(x). new given clause: 74 (37,25) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | CLIMB_TREES(x). ** KEPT: 90 (74,26) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -HAS_CLAWS(x) | HAS_SCALES(x). new given clause: 77 (50,31) WRIGGLES(x) | -DREADED(x) | -GRINNING(x) | FAT(x). ** KEPT: 91 (77,22) WRIGGLES(x) | -GRINNING(x) | FAT(x) | -SAVAGE(x) | -LIZARD(x). ** KEPT: 92 (77,30) WRIGGLES(x) | -DREADED(x) | -GRINNING(x) | -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x). ** KEPT: 93 (77,27) WRIGGLES(x) | -DREADED(x) | -GRINNING(x) | -LAZY(x) | -LIZARD(x) | -DESTRUCTIVE(x). ** KEPT: 94 (77,24) WRIGGLES(x) | -DREADED(x) | -GRINNING(x) | -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x). ** KEPT: 95 (77,19) WRIGGLES(x) | -DREADED(x) | -GRINNING(x) | -ACTIVE(x) | -DESTRUCTIVE(x). ** KEPT: 96 (77,13) WRIGGLES(x) | -DREADED(x) | -GRINNING(x) | -LAZY(x) | -CLIMB_TREES(x). new given clause: 39 (23,19) -SAVAGE(x) | -GRINNING(x) | -HAS_CLAWS(x) | -ACTIVE(x) | -FAT(x). ** KEPT: 97 (39,77) -SAVAGE(x) | -GRINNING(x) | -HAS_CLAWS(x) | -ACTIVE(x) | WRIGGLES(x) | -DREADED(x). ** KEPT: 98 (39,56) -SAVAGE(x) | -GRINNING(x) | -HAS_CLAWS(x) | -ACTIVE(x) | -DREADED(x) | POISONOUS(x). new given clause: 41 (24,35) -SAVAGE(x) | -ACTIVE(x) | -FAT(x) | -GRINNING(x) | -DREADED(x). ** KEPT: 99 (41,77) -SAVAGE(x) | -ACTIVE(x) | -GRINNING(x) | -DREADED(x) | WRIGGLES(x). ** KEPT: 100 (41,56) -SAVAGE(x) | -ACTIVE(x) | -GRINNING(x) | -DREADED(x) | POISONOUS(x). ** KEPT: 101 (41,31) -SAVAGE(x) | -ACTIVE(x) | -GRINNING(x) | -DREADED(x) | HAS_SCALES(x). 99 back subsumes: 97 (39,77) -SAVAGE(x) | -GRINNING(x) | -HAS_CLAWS(x) | -ACTIVE(x) | WRIGGLES(x) | -DREADED(x). 99 back subsumes: 94 (77,24) WRIGGLES(x) | -DREADED(x) | -GRINNING(x) | -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x). 100 back subsumes: 98 (39,56) -SAVAGE(x) | -GRINNING(x) | -HAS_CLAWS(x) | -ACTIVE(x) | -DREADED(x) | POISONOUS(x). 100 back subsumes: 85 (56,24) -GRINNING(x) | -DREADED(x) | POISONOUS(x) | -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x). 101 back subsumes: 59 (31,24) HAS_SCALES(x) | -GRINNING(x) | -DREADED(x) | -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x). new given clause: 42 (24,17) -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x) | -HAS_CLAWS(x) | HAS_SCALES(x). ** KEPT: 102 (42,34) -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x) | HAS_SCALES(x) | -GRINNING(x) | -LIZARD(x). ** KEPT: 103 (42,36) -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x) | -HAS_CLAWS(x) | POISONOUS(x) | -LIZARD(x). new given clause: 44 (25,13) -CUNNING(x) | -SAVAGE(x) | -LIZARD(x) | -FAT(x) | -LAZY(x). ** KEPT: 104 (44,77) -CUNNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | WRIGGLES(x) | -DREADED(x) | -GRINNING(x). ** KEPT: 105 (44,56) -CUNNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -GRINNING(x) | -DREADED(x) | POISONOUS(x). ** KEPT: 106 (44,52) -CUNNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x). ** KEPT: 107 (44,32) -CUNNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x). ** KEPT: 108 (44,31) -CUNNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | HAS_SCALES(x) | -GRINNING(x) | -DREADED(x). new given clause: 46 (26,16) -LAZY(x) | -HAS_CLAWS(x) | HAS_SCALES(x) | -LIZARD(x) | -DESTRUCTIVE(x). ** KEPT: 109 (46,34) -LAZY(x) | HAS_SCALES(x) | -LIZARD(x) | -DESTRUCTIVE(x) | -GRINNING(x) | -SAVAGE(x). ** KEPT: 110 (46,36) -LAZY(x) | -HAS_CLAWS(x) | -LIZARD(x) | -DESTRUCTIVE(x) | POISONOUS(x) | -SAVAGE(x). new given clause: 47 (26,18) -LAZY(x) | -CLIMB_TREES(x) | HAS_SCALES(x) | -GRINNING(x) | -DREADED(x). ** KEPT: 111 (47,74) -LAZY(x) | HAS_SCALES(x) | -GRINNING(x) | -DREADED(x) | -SAVAGE(x) | -LIZARD(x). 111 back subsumes: 108 (44,31) -CUNNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | HAS_SCALES(x) | -GRINNING(x) | -DREADED(x). new given clause: 48 (26,20) -LAZY(x) | -CLIMB_TREES(x) | -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x). ** KEPT: 112 (48,74) -LAZY(x) | -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x). new given clause: 51 (28,26) -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x) | -LAZY(x) | -CLIMB_TREES(x). ** KEPT: 113 (51,22) -HAS_CLAWS(x) | WRIGGLES(x) | -LAZY(x) | -CLIMB_TREES(x) | -SAVAGE(x) | -LIZARD(x). ** KEPT: 114 (51,74) -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x) | -LAZY(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x). new given clause: 53 (28,22) -HAS_CLAWS(x) | WRIGGLES(x) | -HAS_SCALES(x) | -SAVAGE(x) | -LIZARD(x). ** KEPT: 115 (53,46) -HAS_CLAWS(x) | WRIGGLES(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -DESTRUCTIVE(x). ** KEPT: 116 (53,42) -HAS_CLAWS(x) | WRIGGLES(x) | -SAVAGE(x) | -LIZARD(x) | -CUNNING(x) | -ACTIVE(x). ** KEPT: 117 (53,33) -HAS_CLAWS(x) | WRIGGLES(x) | -SAVAGE(x) | -LIZARD(x) | -ACTIVE(x) | -DESTRUCTIVE(x). new given clause: 54 (29,22) -POISONOUS(x) | WRIGGLES(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x). new given clause: 55 (30,17) -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x) | -HAS_CLAWS(x) | HAS_SCALES(x). ** KEPT: 118 (55,34) -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x) | HAS_SCALES(x) | -GRINNING(x) | -SAVAGE(x). ** KEPT: 119 (55,53) -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x) | -HAS_CLAWS(x) | WRIGGLES(x) | -SAVAGE(x). ** KEPT: 120 (55,36) -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x) | -HAS_CLAWS(x) | POISONOUS(x) | -SAVAGE(x). new given clause: 60 (31,19) HAS_SCALES(x) | -GRINNING(x) | -DREADED(x) | -ACTIVE(x) | -DESTRUCTIVE(x). new given clause: 61 (31,22) HAS_SCALES(x) | FAT(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x). ** KEPT: 121 (61,44) HAS_SCALES(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -CUNNING(x) | -LAZY(x). new given clause: 65 (32,19) -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x) | -ACTIVE(x) | -DESTRUCTIVE(x). new given clause: 66 (32,22) -HAS_CLAWS(x) | FAT(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x). ** KEPT: 122 (66,44) -HAS_CLAWS(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -CUNNING(x) | -LAZY(x). ** KEPT: 123 (66,39) -HAS_CLAWS(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -GRINNING(x) | -ACTIVE(x). 122 back subsumes: 107 (44,32) -CUNNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x). new given clause: 67 (33,28) -HAS_CLAWS(x) | -ACTIVE(x) | -DESTRUCTIVE(x) | WRIGGLES(x) | -DREADED(x). new given clause: 68 (33,23) -HAS_CLAWS(x) | HAS_SCALES(x) | -ACTIVE(x) | -SAVAGE(x) | -GRINNING(x). ** KEPT: 124 (68,34) HAS_SCALES(x) | -ACTIVE(x) | -SAVAGE(x) | -GRINNING(x) | -LIZARD(x). ** KEPT: 125 (68,53) -HAS_CLAWS(x) | -ACTIVE(x) | -SAVAGE(x) | -GRINNING(x) | WRIGGLES(x) | -LIZARD(x). 124 back subsumes: 118 (55,34) -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x) | HAS_SCALES(x) | -GRINNING(x) | -SAVAGE(x). 124 back subsumes: 102 (42,34) -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x) | HAS_SCALES(x) | -GRINNING(x) | -LIZARD(x). 124 back subsumes: 69 (34,33) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | HAS_SCALES(x) | -ACTIVE(x) | -DESTRUCTIVE(x). new given clause: 75 (37,24) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -ACTIVE(x) | -FAT(x). new given clause: 78 (50,22) WRIGGLES(x) | -HAS_SCALES(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x). new given clause: 79 (52,22) -HAS_CLAWS(x) | WRIGGLES(x) | FAT(x) | -SAVAGE(x) | -LIZARD(x). ** KEPT: 126 (79,44) -HAS_CLAWS(x) | WRIGGLES(x) | -SAVAGE(x) | -LIZARD(x) | -CUNNING(x) | -LAZY(x). 126 back subsumes: 106 (44,52) -CUNNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x). new given clause: 86 (56,19) -GRINNING(x) | -DREADED(x) | POISONOUS(x) | -ACTIVE(x) | -DESTRUCTIVE(x). ** KEPT: 127 (86,22) -GRINNING(x) | POISONOUS(x) | -ACTIVE(x) | -DESTRUCTIVE(x) | -SAVAGE(x) | -LIZARD(x). new given clause: 87 (56,13) -GRINNING(x) | -DREADED(x) | POISONOUS(x) | -LAZY(x) | -CLIMB_TREES(x). ** KEPT: 128 (87,22) -GRINNING(x) | POISONOUS(x) | -LAZY(x) | -CLIMB_TREES(x) | -SAVAGE(x) | -LIZARD(x). ** KEPT: 129 (87,74) -GRINNING(x) | -DREADED(x) | POISONOUS(x) | -LAZY(x) | -SAVAGE(x) | -LIZARD(x). 129 back subsumes: 112 (48,74) -LAZY(x) | -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x). 129 back subsumes: 105 (44,56) -CUNNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -GRINNING(x) | -DREADED(x) | POISONOUS(x). new given clause: 88 (56,22) FAT(x) | -GRINNING(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x). ** KEPT: 130 (88,75) -GRINNING(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -ACTIVE(x). ** KEPT: 131 (88,44) -GRINNING(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -CUNNING(x) | -LAZY(x). ** KEPT: 132 (88,27) -GRINNING(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -DESTRUCTIVE(x). 130 back subsumes: 127 (86,22) -GRINNING(x) | POISONOUS(x) | -ACTIVE(x) | -DESTRUCTIVE(x) | -SAVAGE(x) | -LIZARD(x). 130 back subsumes: 123 (66,39) -HAS_CLAWS(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -GRINNING(x) | -ACTIVE(x). new given clause: 89 (71,27) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -FAT(x) | -LAZY(x). ** KEPT: 133 (89,88) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | POISONOUS(x). ** KEPT: 134 (89,79) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -HAS_CLAWS(x) | WRIGGLES(x). ** KEPT: 135 (89,77) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | WRIGGLES(x) | -DREADED(x). ** KEPT: 136 (89,61) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | HAS_SCALES(x). 133 back subsumes: 132 (88,27) -GRINNING(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -DESTRUCTIVE(x). 133 back subsumes: 131 (88,44) -GRINNING(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -CUNNING(x) | -LAZY(x). 133 back subsumes: 129 (87,74) -GRINNING(x) | -DREADED(x) | POISONOUS(x) | -LAZY(x) | -SAVAGE(x) | -LIZARD(x). 133 back subsumes: 128 (87,22) -GRINNING(x) | POISONOUS(x) | -LAZY(x) | -CLIMB_TREES(x) | -SAVAGE(x) | -LIZARD(x). 134 back subsumes: 114 (51,74) -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x) | -LAZY(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x). 135 back subsumes: 104 (44,77) -CUNNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | WRIGGLES(x) | -DREADED(x) | -GRINNING(x). 136 back subsumes: 121 (61,44) HAS_SCALES(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -CUNNING(x) | -LAZY(x). 136 back subsumes: 111 (47,74) -LAZY(x) | HAS_SCALES(x) | -GRINNING(x) | -DREADED(x) | -SAVAGE(x) | -LIZARD(x). 136 back subsumes: 109 (46,34) -LAZY(x) | HAS_SCALES(x) | -LIZARD(x) | -DESTRUCTIVE(x) | -GRINNING(x) | -SAVAGE(x). 136 back subsumes: 90 (74,26) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -HAS_CLAWS(x) | HAS_SCALES(x). 136 back subsumes: 70 (34,26) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -CLIMB_TREES(x) | HAS_SCALES(x). new given clause: 91 (77,22) WRIGGLES(x) | -GRINNING(x) | FAT(x) | -SAVAGE(x) | -LIZARD(x). ** KEPT: 137 (91,89) WRIGGLES(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x). ** KEPT: 138 (91,75) WRIGGLES(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -ACTIVE(x). 137 back subsumes: 135 (89,77) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | WRIGGLES(x) | -DREADED(x). 137 back subsumes: 134 (89,79) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -HAS_CLAWS(x) | WRIGGLES(x). 138 back subsumes: 125 (68,53) -HAS_CLAWS(x) | -ACTIVE(x) | -SAVAGE(x) | -GRINNING(x) | WRIGGLES(x) | -LIZARD(x). new given clause: 95 (77,19) WRIGGLES(x) | -DREADED(x) | -GRINNING(x) | -ACTIVE(x) | -DESTRUCTIVE(x). new given clause: 96 (77,13) WRIGGLES(x) | -DREADED(x) | -GRINNING(x) | -LAZY(x) | -CLIMB_TREES(x). new given clause: 99 (41,77) -SAVAGE(x) | -ACTIVE(x) | -GRINNING(x) | -DREADED(x) | WRIGGLES(x). new given clause: 100 (41,56) -SAVAGE(x) | -ACTIVE(x) | -GRINNING(x) | -DREADED(x) | POISONOUS(x). new given clause: 101 (41,31) -SAVAGE(x) | -ACTIVE(x) | -GRINNING(x) | -DREADED(x) | HAS_SCALES(x). new given clause: 124 (68,34) HAS_SCALES(x) | -ACTIVE(x) | -SAVAGE(x) | -GRINNING(x) | -LIZARD(x). new given clause: 130 (88,75) -GRINNING(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -ACTIVE(x). new given clause: 133 (89,88) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | POISONOUS(x). new given clause: 136 (89,61) -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | HAS_SCALES(x). new given clause: 137 (91,89) WRIGGLES(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x). new given clause: 138 (91,75) WRIGGLES(x) | -GRINNING(x) | -SAVAGE(x) | -LIZARD(x) | -ACTIVE(x). new given clause: 45 (26,25) -LAZY(x) | -HAS_CLAWS(x) | HAS_SCALES(x) | -CUNNING(x) | -SAVAGE(x) | -LIZARD(x). new given clause: 57 (31,30) HAS_SCALES(x) | -GRINNING(x) | -DREADED(x) | -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x). new given clause: 58 (31,27) HAS_SCALES(x) | -GRINNING(x) | -DREADED(x) | -LAZY(x) | -LIZARD(x) | -DESTRUCTIVE(x). new given clause: 62 (32,30) -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x) | -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x). new given clause: 63 (32,27) -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x) | -LAZY(x) | -LIZARD(x) | -DESTRUCTIVE(x). new given clause: 64 (32,24) -HAS_CLAWS(x) | -DREADED(x) | POISONOUS(x) | -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x). new given clause: 72 (36,33) POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -HAS_CLAWS(x) | -ACTIVE(x) | -DESTRUCTIVE(x). new given clause: 73 (36,26) POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -CLIMB_TREES(x) | -HAS_CLAWS(x). new given clause: 80 (52,30) -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x) | -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x). new given clause: 81 (52,27) -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x) | -LAZY(x) | -LIZARD(x) | -DESTRUCTIVE(x). new given clause: 82 (52,24) -HAS_CLAWS(x) | WRIGGLES(x) | -DREADED(x) | -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x). new given clause: 83 (56,30) -GRINNING(x) | -DREADED(x) | POISONOUS(x) | -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x). new given clause: 84 (56,27) -GRINNING(x) | -DREADED(x) | POISONOUS(x) | -LAZY(x) | -LIZARD(x) | -DESTRUCTIVE(x). new given clause: 92 (77,30) WRIGGLES(x) | -DREADED(x) | -GRINNING(x) | -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x). new given clause: 93 (77,27) WRIGGLES(x) | -DREADED(x) | -GRINNING(x) | -LAZY(x) | -LIZARD(x) | -DESTRUCTIVE(x). new given clause: 103 (42,36) -CUNNING(x) | -SAVAGE(x) | -ACTIVE(x) | -HAS_CLAWS(x) | POISONOUS(x) | -LIZARD(x). new given clause: 110 (46,36) -LAZY(x) | -HAS_CLAWS(x) | -LIZARD(x) | -DESTRUCTIVE(x) | POISONOUS(x) | -SAVAGE(x). new given clause: 113 (51,22) -HAS_CLAWS(x) | WRIGGLES(x) | -LAZY(x) | -CLIMB_TREES(x) | -SAVAGE(x) | -LIZARD(x). new given clause: 115 (53,46) -HAS_CLAWS(x) | WRIGGLES(x) | -SAVAGE(x) | -LIZARD(x) | -LAZY(x) | -DESTRUCTIVE(x). new given clause: 116 (53,42) -HAS_CLAWS(x) | WRIGGLES(x) | -SAVAGE(x) | -LIZARD(x) | -CUNNING(x) | -ACTIVE(x). new given clause: 117 (53,33) -HAS_CLAWS(x) | WRIGGLES(x) | -SAVAGE(x) | -LIZARD(x) | -ACTIVE(x) | -DESTRUCTIVE(x). new given clause: 119 (55,53) -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x) | -HAS_CLAWS(x) | WRIGGLES(x) | -SAVAGE(x). new given clause: 120 (55,36) -CLIMB_TREES(x) | -LIZARD(x) | -ACTIVE(x) | -HAS_CLAWS(x) | POISONOUS(x) | -SAVAGE(x). new given clause: 122 (66,44) -HAS_CLAWS(x) | POISONOUS(x) | -SAVAGE(x) | -LIZARD(x) | -CUNNING(x) | -LAZY(x). new given clause: 126 (79,44) -HAS_CLAWS(x) | WRIGGLES(x) | -SAVAGE(x) | -LIZARD(x) | -CUNNING(x) | -LAZY(x). ------------ END OF SEARCH ------------ sos empty. --------------- options --------------- set(binary_res). set(hyper_res). set(UR_res). set(demod_hist). set(for_sub). set(print_kept). set(back_sub). set(print_back_sub). set(print_given). set(check_arity). clear(para_from). clear(para_into). clear(demod_inf). clear(para_from_left). clear(para_from_right). clear(para_into_vars). clear(para_from_vars). clear(para_all). clear(para_ones_rule). clear(no_para_into_left). clear(no_para_into_right). clear(demod_linear). clear(print_gen). clear(sort_literals). clear(Unit_deletion). clear(factor). clear(print_weight). clear(sos_fifo). clear(bird_print). clear(atom_wt_max_args). clear(print_lists_at_end). clear(free_all_mem). clear(for_sub_fpa). clear(no_fapl). clear(no_fanl). clear(order_eq). assign(report, 0). assign(max_seconds, 0). assign(max_given, 0). assign(max_kept, 0). assign(max_gen, 0). assign(max_mem, 0). assign(max_weight, 0). assign(max_literals, 0). assign(fpa_literals, 3). assign(fpa_terms, 3). assign(demod_limit, 100). assign(max_proofs, 1). assign(neg_weight, 0). -------------- statistics ------------- clauses input 22 clauses given 94 clauses generated 846 demodulation rewrites 0 clauses wt or lit delete 0 tautologies deleted 6 clauses forward subsumed 724 (clauses subsumed by sos) 515 unit deletions 0 clauses kept 116 empty clauses 0 factors generated 0 clauses back subsumed 33 clauses not processed 0 ----------- times (seconds) ----------- run time 13.53 input time 0.24 binary_res time 1.05 hyper_res time 0.07 UR_res time 0.23 para_into time 0.00 para_from time 0.00 pre_process time 9.73 demod time 0.00 weigh time 0.04 for_sub time 7.80 unit_del time 0.00 post_process time 1.37 back_sub time 1.07 conflict time 0.01 factor time 0.00 FPA build time 0.33 IS build time 0.14 print_cl time 0.98 cl integrate time 0.08 window time 0.00