The dog likes the squirrel. The mouse likes the dog. The squirrel is red. The tiger is kind. If someone is red then they like the mouse. If someone likes the dog then they are red. If someone likes the squirrel then they eat the squirrel. If someone is kind and they eat the squirrel then they see the mouse. If someone eats the mouse then the mouse is cold. If someone is blue then they like the tiger.
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
If someone is red then they like the mouse.
((("someone" "is" "red" "+")) -> ("someone" "likes" "mouse" "+"))
If someone likes the dog then they are red.
((("someone" "likes" "dog" "+")) -> ("someone" "is" "red" "+"))
If someone likes the squirrel then they eat the squirrel.
((("someone" "likes" "squirrel" "+")) -> ("someone" "eats" "squirrel" "+"))
If someone is kind and they eat the squirrel then they see the mouse.
((("someone" "is" "kind" "+") ("someone" "eats" "squirrel" "+")) -> ("someone" "sees" "mouse" "+"))
If someone eats the mouse then the mouse is cold.
((("someone" "eats" "mouse" "+")) -> ("mouse" "is" "cold" "+"))
If someone is blue then they like the tiger.
((("someone" "is" "blue" "+")) -> ("someone" "likes" "tiger" "+"))
The squirrel is red.
True
1
proof
[(triple3)]
("squirrel" "is" "red" "+")
triple3
The mouse does not like the dog.
False
1
inv-proof
[(triple2)]
("mouse" "likes" "dog" "-")
triple2
The dog eats the squirrel.
True
2
proof
[(((triple1) -> rule3))]
("dog" "eats" "squirrel" "+")
((triple1) -> (rule3 % int1))
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int1
The squirrel does not like the mouse.
False
2
inv-proof
[(((triple3) -> rule1))]
("squirrel" "likes" "mouse" "-")
((triple3) -> (rule1 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The mouse likes the mouse.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("mouse" "likes" "mouse" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The mouse does not like the mouse.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("mouse" "likes" "mouse" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The squirrel does not like the tiger.
Unknown
inv-rconc
[@1: The squirrel likes the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "likes" "tiger" "-")
The squirrel sees the mouse.
Unknown
rconc
[@1: The squirrel sees the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "sees" "mouse" "+")
The dog does not like the mouse.
Unknown
inv-rconc
[@2: The dog likes the mouse.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("dog" "likes" "mouse" "-")
The tiger sees the squirrel.
Unknown
random
[@0: The tiger sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "squirrel" "+")
The dog is not blue.
Unknown
inv-random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
@0: The dog likes the squirrel.[(triple1)] The mouse likes the dog.[(triple2)] The squirrel is red.[(triple3)] The tiger is kind.[(triple4)] @1: The dog eats the squirrel.[(((triple1) -> rule3))] The mouse is red.[(((triple2) -> rule2))] The squirrel likes the mouse.[(((triple3) -> rule1))] @2: The mouse likes the mouse.[(((((triple2) -> rule2)) -> rule1))]
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
triple1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple2
The squirrel is red.
("squirrel" "is" "red" "+")
triple3
The tiger is kind.
("tiger" "is" "kind" "+")
triple4
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
((triple1) -> (rule3 % int1))
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
((triple2) -> (rule2 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
((triple3) -> (rule1 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2