The dog eats the mouse. The mouse chases the squirrel. The rabbit eats the mouse. The squirrel is cold. If someone is red then they chase the mouse. If someone visits the rabbit then they eat the mouse. If someone is young then they eat the dog. If someone is cold and they visit the rabbit then they chase the mouse. If someone chases the mouse and they are red then they eat the dog. If someone chases the squirrel then they eat the mouse. If someone eats the mouse then they chase the mouse. If the rabbit visits the mouse and the rabbit is red then the rabbit is round.
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
If someone is red then they chase the mouse.
((("someone" "is" "red" "+")) -> ("someone" "chases" "mouse" "+"))
If someone visits the rabbit then they eat the mouse.
((("someone" "visits" "rabbit" "+")) -> ("someone" "eats" "mouse" "+"))
If someone is young then they eat the dog.
((("someone" "is" "young" "+")) -> ("someone" "eats" "dog" "+"))
If someone is cold and they visit the rabbit then they chase the mouse.
((("someone" "is" "cold" "+") ("someone" "visits" "rabbit" "+")) -> ("someone" "chases" "mouse" "+"))
If someone chases the mouse and they are red then they eat the dog.
((("someone" "chases" "mouse" "+") ("someone" "is" "red" "+")) -> ("someone" "eats" "dog" "+"))
If someone chases the squirrel then they eat the mouse.
((("someone" "chases" "squirrel" "+")) -> ("someone" "eats" "mouse" "+"))
If someone eats the mouse then they chase the mouse.
((("someone" "eats" "mouse" "+")) -> ("someone" "chases" "mouse" "+"))
If the rabbit visits the mouse and the rabbit is red then the rabbit is round.
((("rabbit" "visits" "mouse" "+") ("rabbit" "is" "red" "+")) -> ("rabbit" "is" "round" "+"))
The dog eats the mouse.
True
1
proof
[(triple1)]
("dog" "eats" "mouse" "+")
triple1
The dog does not eat the mouse.
False
1
inv-proof
[(triple1)]
("dog" "eats" "mouse" "-")
triple1
The rabbit chases the mouse.
True
2
proof
[(((triple3) -> rule7))]
("rabbit" "chases" "mouse" "+")
((triple3) -> (rule7 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The mouse does not eat the mouse.
False
2
inv-proof
[(((triple2) -> rule6))]
("mouse" "eats" "mouse" "-")
((triple2) -> (rule6 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The rabbit does not eat the dog.
Unknown
inv-rconc
[@1: The rabbit eats the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "eats" "dog" "-")
The squirrel eats the mouse.
Unknown
rconc
[@1: The squirrel eats the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "eats" "mouse" "+")
The dog is not red.
Unknown
inv-random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
@0: The dog eats the mouse.[(triple1)] The mouse chases the squirrel.[(triple2)] The rabbit eats the mouse.[(triple3)] The squirrel is cold.[(triple4)] @1: The dog chases the mouse.[(((triple1) -> rule7))] The mouse eats the mouse.[(((triple2) -> rule6))] The rabbit chases the mouse.[(((triple3) -> rule7))] @2: The mouse chases the mouse.[(((((triple2) -> rule6)) -> rule7))]
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple1
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple2
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
triple3
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple4
The dog chases the mouse.
("dog" "chases" "mouse" "+")
((triple1) -> (rule7 % int1))
The dog chases the mouse.
("dog" "chases" "mouse" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((triple2) -> (rule6 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
((triple3) -> (rule7 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((((triple2) -> (rule6 % int2))) -> (rule7 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int2