;;;; -*- mode:Lisp; package:user -*- ;;;;
;;;; Created: 23 May 1992
;;;; Purpose: Test Reference File


Experiment #1---SQUIGS example:
The initial clauses are:
(1 (NOT (FEATHERS SQUIGS))
   V (BIRD SQUIGS)
(2 (FEATHERS SQUIGS)
(3 (NOT (BIRD SQUIGS))
There are 3 clauses on level 1.
I resolved 1 with 2 producing
(4 (BIRD SQUIGS)
I resolved 1 with 3 producing
(5 (NOT (FEATHERS SQUIGS))
There are 5 clauses on level 2.
I resolved 5 with 2 producing nil!
I proved the theorem!
There were 5 clauses on 2 levels at termination.

Experiment #2---ABOVE example:
The initial clauses are:
(1 (NOT (ON (? U-1) (? V-2)))
   V (ABOVE (? U-1) (? V-2))
(2 (NOT (ABOVE (? X-3) (? Y-4)))
   V (NOT (ABOVE (? Y-4) (? Z-5)))
   V (ABOVE (? X-3) (? Z-5))
(3 (ON B A)
(4 (ON A TABLE)
(5 (NOT (ABOVE B TABLE))
There are 5 clauses on level 1.
I resolved 1 with 2 producing
(6 (NOT (ON (? Y-9) (? Z-10)))
   V (NOT (ABOVE (? X-11) (? Y-9)))
   V (ABOVE (? X-11) (? Z-10))
I resolved 1 with 2 producing
(7 (NOT (ON (? X-6) (? Y-7)))
   V (NOT (ABOVE (? Y-7) (? Z-8)))
   V (ABOVE (? X-6) (? Z-8))
I resolved 1 with 3 producing
(8 (ABOVE B A)
I resolved 1 with 4 producing
(9 (ABOVE A TABLE)
I resolved 1 with 5 producing
(10 (NOT (ON B TABLE))
I resolved 2 with 5 producing
(11 (NOT (ABOVE B (? Y-12)))
   V (NOT (ABOVE (? Y-12) TABLE))
There are 11 clauses on level 2.
I resolved 11 with 9 producing
(12 (NOT (ABOVE B A))
I resolved 11 with 8 producing
(13 (NOT (ABOVE A TABLE))
I resolved 11 with 7 producing
(14 (NOT (ABOVE B (? Y-15)))
   V (NOT (ON (? Y-15) (? Y-16)))
   V (NOT (ABOVE (? Y-16) TABLE))
I resolved 11 with 7 producing
(15 (NOT (ABOVE (? Y-13) TABLE))
   V (NOT (ON B (? Y-14)))
   V (NOT (ABOVE (? Y-14) (? Y-13)))
I resolved 11 with 6 producing
(16 (NOT (ABOVE B (? Y-19)))
   V (NOT (ON (? Y-20) TABLE))
   V (NOT (ABOVE (? Y-19) (? Y-20)))
I resolved 11 with 6 producing
(17 (NOT (ABOVE (? Y-17) TABLE))
   V (NOT (ON (? Y-18) (? Y-17)))
   V (NOT (ABOVE B (? Y-18)))
I resolved 11 with 1 producing
(18 (NOT (ABOVE B (? Y-22)))
   V (NOT (ON (? Y-22) TABLE))
I resolved 11 with 1 producing
(19 (NOT (ABOVE (? Y-21) TABLE))
   V (NOT (ON B (? Y-21)))
I resolved 11 with 2 producing
(20 (NOT (ABOVE B (? Y-25)))
   V (NOT (ABOVE (? Y-25) (? Y-26)))
   V (NOT (ABOVE (? Y-26) TABLE))
I resolved 11 with 2 producing
(21 (NOT (ABOVE (? Y-23) TABLE))
   V (NOT (ABOVE B (? Y-24)))
   V (NOT (ABOVE (? Y-24) (? Y-23)))
I resolved 9 with 7 producing
(22 (NOT (ON (? X-27) A))
   V (ABOVE (? X-27) TABLE)
I resolved 9 with 6 producing
(23 (NOT (ON TABLE (? Z-28)))
   V (ABOVE A (? Z-28))
I resolved 9 with 2 producing
(24 (NOT (ABOVE (? X-30) A))
   V (ABOVE (? X-30) TABLE)
I resolved 9 with 2 producing
(25 (NOT (ABOVE TABLE (? Z-29)))
   V (ABOVE A (? Z-29))
I resolved 8 with 7 producing
(26 (NOT (ON (? X-31) B))
   V (ABOVE (? X-31) A)
I resolved 8 with 6 producing
(27 (NOT (ON A (? Z-32)))
   V (ABOVE B (? Z-32))
I resolved 8 with 2 producing
(28 (NOT (ABOVE (? X-34) B))
   V (ABOVE (? X-34) A)
I resolved 8 with 2 producing
(29 (NOT (ABOVE A (? Z-33)))
   V (ABOVE B (? Z-33))
I resolved 7 with 6 producing
(30 (NOT (ON (? X-39) (? Y-40)))
   V (NOT (ABOVE (? Y-40) (? Y-41)))
   V (NOT (ON (? Y-41) (? Z-42)))
   V (ABOVE (? X-39) (? Z-42))
I resolved 7 with 6 producing
(31 (NOT (ON (? X-35) (? Y-36)))
   V (ABOVE (? X-35) (? Z-37))
   V (NOT (ON (? Y-38) (? Z-37)))
   V (NOT (ABOVE (? Y-36) (? Y-38)))
I resolved 7 with 1 producing
(32 (NOT (ON (? X-43) (? Y-44)))
   V (ABOVE (? X-43) (? Z-45))
   V (NOT (ON (? Y-44) (? Z-45)))
I resolved 7 with 2 producing
(33 (NOT (ON (? Y-54) (? Y-55)))
   V (NOT (ABOVE (? Y-55) (? Z-56)))
   V (NOT (ABOVE (? X-57) (? Y-54)))
   V (ABOVE (? X-57) (? Z-56))
I resolved 7 with 2 producing
(34 (NOT (ON (? X-50) (? Y-51)))
   V (NOT (ABOVE (? Y-51) (? Y-52)))
   V (NOT (ABOVE (? Y-52) (? Z-53)))
   V (ABOVE (? X-50) (? Z-53))
I resolved 7 with 2 producing
(35 (NOT (ON (? X-46) (? Y-47)))
   V (ABOVE (? X-46) (? Z-48))
   V (NOT (ABOVE (? Y-47) (? Y-49)))
   V (NOT (ABOVE (? Y-49) (? Z-48)))
I resolved 7 with 3 producing
(36 (NOT (ABOVE A (? Z-58)))
   V (ABOVE B (? Z-58))
I resolved 7 with 4 producing
(37 (NOT (ABOVE TABLE (? Z-59)))
   V (ABOVE A (? Z-59))
I resolved 7 with 5 producing
(38 (NOT (ON B (? Y-60)))
   V (NOT (ABOVE (? Y-60) TABLE))
I resolved 6 with 1 producing
(39 (NOT (ON (? Y-61) (? Z-62)))
   V (ABOVE (? X-63) (? Z-62))
   V (NOT (ON (? X-63) (? Y-61)))
I resolved 6 with 2 producing
(40 (NOT (ON (? Y-72) (? Z-73)))
   V (NOT (ABOVE (? Y-74) (? Y-72)))
   V (NOT (ABOVE (? X-75) (? Y-74)))
   V (ABOVE (? X-75) (? Z-73))
I resolved 6 with 2 producing
(41 (NOT (ON (? Y-68) (? Y-69)))
   V (NOT (ABOVE (? X-70) (? Y-68)))
   V (NOT (ABOVE (? Y-69) (? Z-71)))
   V (ABOVE (? X-70) (? Z-71))
I resolved 6 with 2 producing
(42 (NOT (ON (? Y-64) (? Z-65)))
   V (ABOVE (? X-66) (? Z-65))
   V (NOT (ABOVE (? X-66) (? Y-67)))
   V (NOT (ABOVE (? Y-67) (? Y-64)))
I resolved 6 with 3 producing
(43 (NOT (ABOVE (? X-76) B))
   V (ABOVE (? X-76) A)
I resolved 6 with 4 producing
(44 (NOT (ABOVE (? X-77) A))
   V (ABOVE (? X-77) TABLE)
I resolved 6 with 5 producing
(45 (NOT (ON (? Y-78) TABLE))
   V (NOT (ABOVE B (? Y-78)))
I resolved 1 with 2 producing
(46 (NOT (ON (? Y-82) (? Z-83)))
   V (NOT (ABOVE (? X-84) (? Y-82)))
   V (ABOVE (? X-84) (? Z-83))
I resolved 1 with 2 producing
(47 (NOT (ON (? X-79) (? Y-80)))
   V (NOT (ABOVE (? Y-80) (? Z-81)))
   V (ABOVE (? X-79) (? Z-81))
I resolved 1 with 3 producing
(48 (ABOVE B A)
I resolved 1 with 4 producing
(49 (ABOVE A TABLE)
I resolved 1 with 5 producing
(50 (NOT (ON B TABLE))
I resolved 2 with 5 producing
(51 (NOT (ABOVE B (? Y-85)))
   V (NOT (ABOVE (? Y-85) TABLE))
There are 51 clauses on level 3.
I resolved 51 with 49 producing
(52 (NOT (ABOVE B A))
I resolved 51 with 48 producing
(53 (NOT (ABOVE A TABLE))
I resolved 51 with 47 producing
(54 (NOT (ABOVE B (? Y-88)))
   V (NOT (ON (? Y-88) (? Y-89)))
   V (NOT (ABOVE (? Y-89) TABLE))
I resolved 51 with 47 producing
(55 (NOT (ABOVE (? Y-86) TABLE))
   V (NOT (ON B (? Y-87)))
   V (NOT (ABOVE (? Y-87) (? Y-86)))
I resolved 51 with 46 producing
(56 (NOT (ABOVE B (? Y-92)))
   V (NOT (ON (? Y-93) TABLE))
   V (NOT (ABOVE (? Y-92) (? Y-93)))
I resolved 51 with 46 producing
(57 (NOT (ABOVE (? Y-90) TABLE))
   V (NOT (ON (? Y-91) (? Y-90)))
   V (NOT (ABOVE B (? Y-91)))
I resolved 51 with 44 producing
(58 (NOT (ABOVE B (? Y-94)))
   V (NOT (ABOVE (? Y-94) A))
I resolved 51 with 44 producing
(59 (NOT (ABOVE TABLE TABLE))
   V (NOT (ABOVE B A))
I resolved 51 with 43 producing
(60 (NOT (ABOVE A TABLE))
   V (NOT (ABOVE B B))
I resolved 51 with 42 producing
(61 (NOT (ABOVE B (? Y-98)))
   V (NOT (ON (? Y-99) TABLE))
   V (NOT (ABOVE (? Y-98) (? Y-100)))
   V (NOT (ABOVE (? Y-100) (? Y-99)))
I resolved 51 with 42 producing
(62 (NOT (ABOVE (? Y-95) TABLE))
   V (NOT (ON (? Y-96) (? Y-95)))
   V (NOT (ABOVE B (? Y-97)))
   V (NOT (ABOVE (? Y-97) (? Y-96)))
I resolved 51 with 41 producing
(63 (NOT (ABOVE B (? Y-104)))
   V (NOT (ON (? Y-105) (? Y-106)))
   V (NOT (ABOVE (? Y-104) (? Y-105)))
   V (NOT (ABOVE (? Y-106) TABLE))
I resolved 51 with 41 producing
(64 (NOT (ABOVE (? Y-101) TABLE))
   V (NOT (ON (? Y-102) (? Y-103)))
   V (NOT (ABOVE B (? Y-102)))
   V (NOT (ABOVE (? Y-103) (? Y-101)))
I resolved 51 with 40 producing
(65 (NOT (ABOVE B (? Y-110)))
   V (NOT (ON (? Y-111) TABLE))
   V (NOT (ABOVE (? Y-112) (? Y-111)))
   V (NOT (ABOVE (? Y-110) (? Y-112)))
I resolved 51 with 40 producing
(66 (NOT (ABOVE (? Y-107) TABLE))
   V (NOT (ON (? Y-108) (? Y-107)))
   V (NOT (ABOVE (? Y-109) (? Y-108)))
   V (NOT (ABOVE B (? Y-109)))
I resolved 51 with 39 producing
(67 (NOT (ABOVE B (? Y-115)))
   V (NOT (ON (? Y-116) TABLE))
   V (NOT (ON (? Y-115) (? Y-116)))
I resolved 51 with 39 producing
(68 (NOT (ABOVE (? Y-113) TABLE))
   V (NOT (ON (? Y-114) (? Y-113)))
   V (NOT (ON B (? Y-114)))
I resolved 51 with 37 producing
(69 (NOT (ABOVE B A))
   V (NOT (ABOVE TABLE TABLE))
I resolved 51 with 36 producing
(70 (NOT (ABOVE B B))
   V (NOT (ABOVE A TABLE))
I resolved 51 with 36 producing
(71 (NOT (ABOVE (? Y-117) TABLE))
   V (NOT (ABOVE A (? Y-117)))
I resolved 51 with 35 producing
(72 (NOT (ABOVE B (? Y-121)))
   V (NOT (ON (? Y-121) (? Y-122)))
   V (NOT (ABOVE (? Y-122) (? Y-123)))
   V (NOT (ABOVE (? Y-123) TABLE))
I resolved 51 with 35 producing
(73 (NOT (ABOVE (? Y-118) TABLE))
   V (NOT (ON B (? Y-119)))
   V (NOT (ABOVE (? Y-119) (? Y-120)))
   V (NOT (ABOVE (? Y-120) (? Y-118)))
I resolved 51 with 34 producing
(74 (NOT (ABOVE B (? Y-127)))
   V (NOT (ON (? Y-127) (? Y-128)))
   V (NOT (ABOVE (? Y-128) (? Y-129)))
   V (NOT (ABOVE (? Y-129) TABLE))
I resolved 51 with 34 producing
(75 (NOT (ABOVE (? Y-124) TABLE))
   V (NOT (ON B (? Y-125)))
   V (NOT (ABOVE (? Y-125) (? Y-126)))
   V (NOT (ABOVE (? Y-126) (? Y-124)))
I resolved 51 with 33 producing
(76 (NOT (ABOVE B (? Y-133)))
   V (NOT (ON (? Y-134) (? Y-135)))
   V (NOT (ABOVE (? Y-135) TABLE))
   V (NOT (ABOVE (? Y-133) (? Y-134)))
I resolved 51 with 33 producing
(77 (NOT (ABOVE (? Y-130) TABLE))
   V (NOT (ON (? Y-131) (? Y-132)))
   V (NOT (ABOVE (? Y-132) (? Y-130)))
   V (NOT (ABOVE B (? Y-131)))
I resolved 51 with 32 producing
(78 (NOT (ABOVE B (? Y-138)))
   V (NOT (ON (? Y-138) (? Y-139)))
   V (NOT (ON (? Y-139) TABLE))
I resolved 51 with 32 producing
(79 (NOT (ABOVE (? Y-136) TABLE))
   V (NOT (ON B (? Y-137)))
   V (NOT (ON (? Y-137) (? Y-136)))
I resolved 51 with 31 producing
(80 (NOT (ABOVE B (? Y-143)))
   V (NOT (ON (? Y-143) (? Y-144)))
   V (NOT (ON (? Y-145) TABLE))
   V (NOT (ABOVE (? Y-144) (? Y-145)))
I resolved 51 with 31 producing
(81 (NOT (ABOVE (? Y-140) TABLE))
   V (NOT (ON B (? Y-141)))
   V (NOT (ON (? Y-142) (? Y-140)))
   V (NOT (ABOVE (? Y-141) (? Y-142)))
I resolved 51 with 30 producing
(82 (NOT (ABOVE B (? Y-149)))
   V (NOT (ON (? Y-149) (? Y-150)))
   V (NOT (ABOVE (? Y-150) (? Y-151)))
   V (NOT (ON (? Y-151) TABLE))
I resolved 51 with 30 producing
(83 (NOT (ABOVE (? Y-146) TABLE))
   V (NOT (ON B (? Y-147)))
   V (NOT (ABOVE (? Y-147) (? Y-148)))
   V (NOT (ON (? Y-148) (? Y-146)))
I resolved 51 with 29 producing
(84 (NOT (ABOVE B B))
   V (NOT (ABOVE A TABLE))
I resolved 51 with 29 producing
(85 (NOT (ABOVE (? Y-152) TABLE))
   V (NOT (ABOVE A (? Y-152)))
I resolved 51 with 28 producing
(86 (NOT (ABOVE A TABLE))
   V (NOT (ABOVE B B))
I resolved 51 with 27 producing
(87 (NOT (ABOVE B B))
   V (NOT (ON A TABLE))
I resolved 51 with 27 producing
(88 (NOT (ABOVE (? Y-153) TABLE))
   V (NOT (ON A (? Y-153)))
I resolved 51 with 26 producing
(89 (NOT (ABOVE A TABLE))
   V (NOT (ON B B))
I resolved 51 with 25 producing
(90 (NOT (ABOVE B A))
   V (NOT (ABOVE TABLE TABLE))
I resolved 51 with 24 producing
(91 (NOT (ABOVE B (? Y-154)))
   V (NOT (ABOVE (? Y-154) A))
I resolved 51 with 24 producing
(92 (NOT (ABOVE TABLE TABLE))
   V (NOT (ABOVE B A))
I resolved 51 with 23 producing
(93 (NOT (ABOVE B A))
   V (NOT (ON TABLE TABLE))
I resolved 51 with 22 producing
(94 (NOT (ABOVE B (? Y-155)))
   V (NOT (ON (? Y-155) A))
I resolved 51 with 22 producing
(95 (NOT (ABOVE TABLE TABLE))
   V (NOT (ON B A))
I resolved 51 with 9 producing
(96 (NOT (ABOVE B A))
I resolved 51 with 8 producing
(97 (NOT (ABOVE A TABLE))
I resolved 51 with 7 producing
(98 (NOT (ABOVE B (? Y-158)))
   V (NOT (ON (? Y-158) (? Y-159)))
   V (NOT (ABOVE (? Y-159) TABLE))
I resolved 51 with 7 producing
(99 (NOT (ABOVE (? Y-156) TABLE))
   V (NOT (ON B (? Y-157)))
   V (NOT (ABOVE (? Y-157) (? Y-156)))
I resolved 51 with 6 producing
(100 (NOT (ABOVE B (? Y-162)))
   V (NOT (ON (? Y-163) TABLE))
   V (NOT (ABOVE (? Y-162) (? Y-163)))
I resolved 51 with 6 producing
(101 (NOT (ABOVE (? Y-160) TABLE))
   V (NOT (ON (? Y-161) (? Y-160)))
   V (NOT (ABOVE B (? Y-161)))
I resolved 51 with 1 producing
(102 (NOT (ABOVE B (? Y-165)))
   V (NOT (ON (? Y-165) TABLE))
I resolved 51 with 1 producing
(103 (NOT (ABOVE (? Y-164) TABLE))
   V (NOT (ON B (? Y-164)))
I resolved 51 with 2 producing
(104 (NOT (ABOVE B (? Y-168)))
   V (NOT (ABOVE (? Y-168) (? Y-169)))
   V (NOT (ABOVE (? Y-169) TABLE))
I resolved 51 with 2 producing
(105 (NOT (ABOVE (? Y-166) TABLE))
   V (NOT (ABOVE B (? Y-167)))
   V (NOT (ABOVE (? Y-167) (? Y-166)))
I resolved 49 with 47 producing
(106 (NOT (ON (? X-170) A))
   V (ABOVE (? X-170) TABLE)
I resolved 49 with 46 producing
(107 (NOT (ON TABLE (? Z-171)))
   V (ABOVE A (? Z-171))
I resolved 49 with 42 producing
(108 (NOT (ON TABLE (? Z-174)))
   V (ABOVE (? X-175) (? Z-174))
   V (NOT (ABOVE (? X-175) A))
I resolved 49 with 42 producing
(109 (NOT (ON (? Y-172) (? Z-173)))
   V (ABOVE A (? Z-173))
   V (NOT (ABOVE TABLE (? Y-172)))
I resolved 49 with 41 producing
(110 (NOT (ON (? Y-178) A))
   V (NOT (ABOVE (? X-179) (? Y-178)))
   V (ABOVE (? X-179) TABLE)
I resolved 49 with 41 producing
(111 (NOT (ON TABLE (? Y-176)))
   V (NOT (ABOVE (? Y-176) (? Z-177)))
   V (ABOVE A (? Z-177))
I resolved 49 with 40 producing
(112 (NOT (ON (? Y-182) (? Z-183)))
   V (NOT (ABOVE TABLE (? Y-182)))
   V (ABOVE A (? Z-183))
I resolved 49 with 40 producing
(113 (NOT (ON TABLE (? Z-180)))
   V (NOT (ABOVE (? X-181) A))
   V (ABOVE (? X-181) (? Z-180))
I resolved 49 with 38 producing
(114 (NOT (ON B A))
I resolved 49 with 36 producing
(115 (ABOVE B TABLE)
I resolved 49 with 35 producing
(116 (NOT (ON (? X-186) (? Y-187)))
   V (ABOVE (? X-186) TABLE)
   V (NOT (ABOVE (? Y-187) A))
I resolved 49 with 35 producing
(117 (NOT (ON (? X-184) A))
   V (ABOVE (? X-184) (? Z-185))
   V (NOT (ABOVE TABLE (? Z-185)))
I resolved 49 with 34 producing
(118 (NOT (ON (? X-190) (? Y-191)))
   V (NOT (ABOVE (? Y-191) A))
   V (ABOVE (? X-190) TABLE)
I resolved 49 with 34 producing
(119 (NOT (ON (? X-188) A))
   V (NOT (ABOVE TABLE (? Z-189)))
   V (ABOVE (? X-188) (? Z-189))
I resolved 49 with 33 producing
(120 (NOT (ON TABLE (? Y-194)))
   V (NOT (ABOVE (? Y-194) (? Z-195)))
   V (ABOVE A (? Z-195))
I resolved 49 with 33 producing
(121 (NOT (ON (? Y-192) A))
   V (NOT (ABOVE (? X-193) (? Y-192)))
   V (ABOVE (? X-193) TABLE)
I resolved 49 with 31 producing
(122 (NOT (ON (? X-196) A))
   V (ABOVE (? X-196) (? Z-197))
   V (NOT (ON TABLE (? Z-197)))
I resolved 49 with 30 producing
(123 (NOT (ON (? X-198) A))
   V (NOT (ON TABLE (? Z-199)))
   V (ABOVE (? X-198) (? Z-199))
I resolved 49 with 29 producing
(124 (ABOVE B TABLE)
I resolved 49 with 21 producing
(125 (NOT (ABOVE TABLE TABLE))
   V (NOT (ABOVE B A))
I resolved 49 with 21 producing
(126 (NOT (ABOVE B (? Y-200)))
   V (NOT (ABOVE (? Y-200) A))
I resolved 49 with 20 producing
(127 (NOT (ABOVE B (? Y-201)))
   V (NOT (ABOVE (? Y-201) A))
I resolved 49 with 20 producing
(128 (NOT (ABOVE B A))
   V (NOT (ABOVE TABLE TABLE))
I resolved 49 with 19 producing
(129 (NOT (ON B A))
I resolved 49 with 17 producing
(130 (NOT (ON (? Y-202) A))
   V (NOT (ABOVE B (? Y-202)))
I resolved 49 with 16 producing
(131 (NOT (ABOVE B A))
   V (NOT (ON TABLE TABLE))
I resolved 49 with 15 producing
(132 (NOT (ABOVE TABLE TABLE))
   V (NOT (ON B A))
I resolved 49 with 15 producing
(133 (NOT (ON B (? Y-203)))
   V (NOT (ABOVE (? Y-203) A))
I resolved 49 with 14 producing
(134 (NOT (ABOVE B (? Y-204)))
   V (NOT (ON (? Y-204) A))
I resolved 49 with 13 producing nil!
I proved the theorem!
There were 134 clauses on 3 levels at termination.