The dog eats the mouse. The dog is red. The dog does not see the rabbit. The mouse is red. The mouse is rough. The rabbit chases the mouse. The rabbit is round. If the mouse sees the rabbit then the rabbit is cold. If someone is rough then they eat the dog. If someone sees the dog then they eat the dog. If someone is round then they see the dog. If someone eats the mouse and the mouse is rough then the mouse sees the dog. If someone is round and not cold then they eat the rabbit. If the rabbit chases the dog and the dog is round then the rabbit eats the dog. If someone eats the rabbit and the rabbit is young then the rabbit eats the dog.
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The dog is red.
("dog" "is" "red" "+")
The dog does not see the rabbit.
("dog" "sees" "rabbit" "-")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
If the mouse sees the rabbit then the rabbit is cold.
((("mouse" "sees" "rabbit" "+")) -> ("rabbit" "is" "cold" "+"))
If someone is rough then they eat the dog.
((("someone" "is" "rough" "+")) -> ("someone" "eats" "dog" "+"))
If someone sees the dog then they eat the dog.
((("someone" "sees" "dog" "+")) -> ("someone" "eats" "dog" "+"))
If someone is round then they see the dog.
((("someone" "is" "round" "+")) -> ("someone" "sees" "dog" "+"))
If someone eats the mouse and the mouse is rough then the mouse sees the dog.
((("someone" "eats" "mouse" "+") ("mouse" "is" "rough" "+")) -> ("mouse" "sees" "dog" "+"))
If someone is round and not cold then they eat the rabbit.
((("someone" "is" "round" "+") ("someone" "is" "cold" "~")) -> ("someone" "eats" "rabbit" "+"))
If the rabbit chases the dog and the dog is round then the rabbit eats the dog.
((("rabbit" "chases" "dog" "+") ("dog" "is" "round" "+")) -> ("rabbit" "eats" "dog" "+"))
If someone eats the rabbit and the rabbit is young then the rabbit eats the dog.
((("someone" "eats" "rabbit" "+") ("rabbit" "is" "young" "+")) -> ("rabbit" "eats" "dog" "+"))
The rabbit is round.
True
1
proof
[(triple7)]
("rabbit" "is" "round" "+")
triple7
The dog sees the rabbit.
False
1
inv-proof
[(triple3)]
("dog" "sees" "rabbit" "+")
triple3
The mouse eats the dog.
True
2
proof
[(((triple5) -> rule2) OR ((((triple1 triple5) -> rule5)) -> rule3))]
("mouse" "eats" "dog" "+")
((triple5) -> (rule2 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
((((triple1 triple5) -> (rule5 % int2))) -> (rule3 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
The rabbit does not see the dog.
False
2
inv-proof
[(((triple7) -> rule4))]
("rabbit" "sees" "dog" "-")
((triple7) -> (rule4 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit eats the dog.
True
3
proof
[(((((triple7) -> rule4)) -> rule3))]
("rabbit" "eats" "dog" "+")
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int2
The rabbit does not eat the dog.
False
3
inv-proof
[(((((triple7) -> rule4)) -> rule3))]
("rabbit" "eats" "dog" "-")
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int2
The dog does not eat the rabbit.
Unknown
inv-rconc
[@1: The dog eats the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "eats" "rabbit" "-")
The rabbit is cold.
Unknown
rconc
[@1: The rabbit is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "cold" "+")
The dog does not see the dog.
Unknown
inv-rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "sees" "dog" "-")
The rabbit is young.
Unknown
random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "+")
The dog is not round.
Unknown
inv-random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "-")
The dog sees the mouse.
Unknown
random
[@0: The dog sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "mouse" "+")
@0: The dog does not see the rabbit.[(triple3)] The dog eats the mouse.[(triple1)] The dog is red.[(triple2)] The mouse is red.[(triple4)] The mouse is rough.[(triple5)] The rabbit chases the mouse.[(triple6)] The rabbit is round.[(triple7)] @1: The mouse eats the dog.[(((triple5) -> rule2) OR ((((triple1 triple5) -> rule5)) -> rule3))] The mouse sees the dog.[(((triple1 triple5) -> rule5))] The rabbit sees the dog.[(((triple7) -> rule4))] @2: The rabbit eats the dog.[(((((triple7) -> rule4)) -> rule3))]
The dog does not see the rabbit.
("dog" "sees" "rabbit" "-")
triple3
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple1
The dog is red.
("dog" "is" "red" "+")
triple2
The mouse is red.
("mouse" "is" "red" "+")
triple4
The mouse is rough.
("mouse" "is" "rough" "+")
triple5
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple6
The rabbit is round.
("rabbit" "is" "round" "+")
triple7
The mouse eats the dog.
("mouse" "eats" "dog" "+")
((triple5) -> (rule2 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
((((triple1 triple5) -> (rule5 % int2))) -> (rule3 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
((triple1 triple5) -> (rule5 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
((triple7) -> (rule4 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
((((triple7) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int2