The dog is not rough. The mouse eats the dog. The mouse eats the rabbit. The mouse is big. The mouse needs the dog. The mouse needs the rabbit. The rabbit is rough. If someone eats the rabbit then the rabbit does not need the dog. If the dog visits the rabbit then the rabbit visits the mouse. If someone needs the mouse and they are not nice then the mouse visits the rabbit. If the rabbit needs the mouse and the mouse eats the rabbit then the rabbit is rough. If the rabbit visits the mouse and the rabbit is round then the mouse needs the dog. If the rabbit visits the dog then the dog is rough. If someone eats the dog then the dog visits the rabbit. If the mouse is round and the mouse does not eat the dog then the dog does not need the mouse.
The dog is not rough.
("dog" "is" "rough" "-")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
If someone eats the rabbit then the rabbit does not need the dog.
((("someone" "eats" "rabbit" "+")) -> ("rabbit" "needs" "dog" "-"))
If the dog visits the rabbit then the rabbit visits the mouse.
((("dog" "visits" "rabbit" "+")) -> ("rabbit" "visits" "mouse" "+"))
If someone needs the mouse and they are not nice then the mouse visits the rabbit.
((("someone" "needs" "mouse" "+") ("someone" "is" "nice" "~")) -> ("mouse" "visits" "rabbit" "+"))
If the rabbit needs the mouse and the mouse eats the rabbit then the rabbit is rough.
((("rabbit" "needs" "mouse" "+") ("mouse" "eats" "rabbit" "+")) -> ("rabbit" "is" "rough" "+"))
If the rabbit visits the mouse and the rabbit is round then the mouse needs the dog.
((("rabbit" "visits" "mouse" "+") ("rabbit" "is" "round" "+")) -> ("mouse" "needs" "dog" "+"))
If the rabbit visits the dog then the dog is rough.
((("rabbit" "visits" "dog" "+")) -> ("dog" "is" "rough" "+"))
If someone eats the dog then the dog visits the rabbit.
((("someone" "eats" "dog" "+")) -> ("dog" "visits" "rabbit" "+"))
If the mouse is round and the mouse does not eat the dog then the dog does not need the mouse.
((("mouse" "is" "round" "+") ("mouse" "eats" "dog" "~")) -> ("dog" "needs" "mouse" "-"))
The mouse is big.
True
1
proof
[(triple4)]
("mouse" "is" "big" "+")
triple4
The mouse does not eat the rabbit.
False
1
inv-proof
[(triple3)]
("mouse" "eats" "rabbit" "-")
triple3
The rabbit does not need the dog.
True
2
proof
[(((triple3) -> rule1))]
("rabbit" "needs" "dog" "-")
((triple3) -> (rule1 % int1))
The rabbit does not need the dog.
("rabbit" "needs" "dog" "-")
int1
The dog does not visit the rabbit.
False
2
inv-proof
[(((triple2) -> rule7))]
("dog" "visits" "rabbit" "-")
((triple2) -> (rule7 % int1))
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int1
The rabbit visits the mouse.
True
3
proof
[(((((triple2) -> rule7)) -> rule2))]
("rabbit" "visits" "mouse" "+")
((((triple2) -> (rule7 % int2))) -> (rule2 % int1))
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int1
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int2
The rabbit does not visit the mouse.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule2))]
("rabbit" "visits" "mouse" "-")
((((triple2) -> (rule7 % int2))) -> (rule2 % int1))
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int1
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int2
The mouse does not visit the rabbit.
Unknown
inv-rconc
[@1: The mouse visits the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "visits" "rabbit" "-")
The dog visits the mouse.
Unknown
random
[@0: The dog visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "mouse" "+")
The mouse does not visit the dog.
Unknown
inv-random
[@0: The mouse visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "dog" "-")
The dog needs the dog.
Unknown
random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The mouse is cold.
Unknown
random
[@0: The mouse is cold.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "cold" "+")
@0: The dog is not rough.[(triple1)] The mouse eats the dog.[(triple2)] The mouse eats the rabbit.[(triple3)] The mouse is big.[(triple4)] The mouse needs the dog.[(triple5)] The mouse needs the rabbit.[(triple6)] The rabbit is rough.[(triple7)] @1: The dog visits the rabbit.[(((triple2) -> rule7))] The rabbit does not need the dog.[(((triple3) -> rule1))] @2: The rabbit visits the mouse.[(((((triple2) -> rule7)) -> rule2))]
The dog is not rough.
("dog" "is" "rough" "-")
triple1
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple2
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple3
The mouse is big.
("mouse" "is" "big" "+")
triple4
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple5
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple6
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple7
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
((triple2) -> (rule7 % int1))
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int1
The rabbit does not need the dog.
("rabbit" "needs" "dog" "-")
((triple3) -> (rule1 % int1))
The rabbit does not need the dog.
("rabbit" "needs" "dog" "-")
int1
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
((((triple2) -> (rule7 % int2))) -> (rule2 % int1))
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int1
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int2