The dog is young. The dog likes the tiger. The dog sees the mouse. The mouse chases the squirrel. The mouse is green. The mouse likes the dog. The mouse likes the squirrel. The mouse likes the tiger. The mouse sees the tiger. The squirrel is blue. The squirrel sees the dog. The tiger is blue. The tiger likes the dog. The tiger sees the dog. The tiger sees the mouse. If the tiger is nice and the tiger likes the dog then the dog likes the tiger. If something chases the mouse and it likes the tiger then the tiger is nice. If something is blue and nice then it likes the dog. Blue things are young. If the tiger is young and the tiger sees the mouse then the mouse sees the squirrel. If the tiger is kind then the tiger likes the mouse. If the dog likes the squirrel and the squirrel is blue then the squirrel chases the mouse. If something chases the mouse and the mouse chases the tiger then the tiger likes the squirrel.
The dog is young.
("dog" "is" "young" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger sees the dog.
("tiger" "sees" "dog" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If the tiger is nice and the tiger likes the dog then the dog likes the tiger.
((("tiger" "is" "nice" "+") ("tiger" "likes" "dog" "+")) -> ("dog" "likes" "tiger" "+"))
If something chases the mouse and it likes the tiger then the tiger is nice.
((("something" "chases" "mouse" "+") ("something" "likes" "tiger" "+")) -> ("tiger" "is" "nice" "+"))
If something is blue and nice then it likes the dog.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "likes" "dog" "+"))
Blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If the tiger is young and the tiger sees the mouse then the mouse sees the squirrel.
((("tiger" "is" "young" "+") ("tiger" "sees" "mouse" "+")) -> ("mouse" "sees" "squirrel" "+"))
If the tiger is kind then the tiger likes the mouse.
((("tiger" "is" "kind" "+")) -> ("tiger" "likes" "mouse" "+"))
If the dog likes the squirrel and the squirrel is blue then the squirrel chases the mouse.
((("dog" "likes" "squirrel" "+") ("squirrel" "is" "blue" "+")) -> ("squirrel" "chases" "mouse" "+"))
If something chases the mouse and the mouse chases the tiger then the tiger likes the squirrel.
((("something" "chases" "mouse" "+") ("mouse" "chases" "tiger" "+")) -> ("tiger" "likes" "squirrel" "+"))
The squirrel sees the dog.
True
1
proof
[(triple11)]
("squirrel" "sees" "dog" "+")
triple11
The mouse does not see the tiger.
False
1
inv-proof
[(triple9)]
("mouse" "sees" "tiger" "-")
triple9
The squirrel is young.
True
2
proof
[(((triple10) -> rule4))]
("squirrel" "is" "young" "+")
((triple10) -> (rule4 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is not young.
False
2
inv-proof
[(((triple10) -> rule4))]
("squirrel" "is" "young" "-")
((triple10) -> (rule4 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The mouse sees the squirrel.
True
4
proof
[(((((triple12) -> rule4) triple15) -> rule5))]
("mouse" "sees" "squirrel" "+")
((((triple12) -> (rule4 % int2)) triple15) -> (rule5 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The mouse does not see the squirrel.
False
4
inv-proof
[(((((triple12) -> rule4) triple15) -> rule5))]
("mouse" "sees" "squirrel" "-")
((((triple12) -> (rule4 % int2)) triple15) -> (rule5 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger does not like the mouse.
Unknown
inv-rconc
[@1: The tiger likes the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "likes" "mouse" "-")
The mouse is young.
Unknown
rconc
[@1: The mouse is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "young" "+")
The tiger is not nice.
Unknown
inv-rconc
[@1: The tiger is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "nice" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
The dog is not nice.
Unknown
inv-random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The dog is young.[(triple1)] The dog likes the tiger.[(triple2)] The dog sees the mouse.[(triple3)] The mouse chases the squirrel.[(triple4)] The mouse is green.[(triple5)] The mouse likes the dog.[(triple6)] The mouse likes the squirrel.[(triple7)] The mouse likes the tiger.[(triple8)] The mouse sees the tiger.[(triple9)] The squirrel is blue.[(triple10)] The squirrel sees the dog.[(triple11)] The tiger is blue.[(triple12)] The tiger likes the dog.[(triple13)] The tiger sees the dog.[(triple14)] The tiger sees the mouse.[(triple15)] @1: The squirrel is young.[(((triple10) -> rule4))] The tiger is young.[(((triple12) -> rule4))] @2: The mouse sees the squirrel.[(((((triple12) -> rule4) triple15) -> rule5))]
The dog is young.
("dog" "is" "young" "+")
triple1
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple2
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple3
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple4
The mouse is green.
("mouse" "is" "green" "+")
triple5
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple6
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple7
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple8
The mouse sees the tiger.
("mouse" "sees" "tiger" "+")
triple9
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple10
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
triple11
The tiger is blue.
("tiger" "is" "blue" "+")
triple12
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple13
The tiger sees the dog.
("tiger" "sees" "dog" "+")
triple14
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple15
The squirrel is young.
("squirrel" "is" "young" "+")
((triple10) -> (rule4 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
((triple12) -> (rule4 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
((((triple12) -> (rule4 % int2)) triple15) -> (rule5 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2