The dog is not green. The dog likes the rabbit. The dog does not visit the mouse. The mouse is blue. The mouse is green. The mouse does not like the dog. The mouse does not like the rabbit. The mouse needs the dog. The mouse visits the dog. The mouse visits the rabbit. The rabbit likes the dog. The rabbit likes the mouse. The rabbit needs the dog. The rabbit needs the mouse. The rabbit visits the dog. The rabbit does not visit the mouse. If the rabbit visits the mouse then the mouse is big. Big things are green. If something needs the dog and the dog likes the rabbit then it is big. If something needs the rabbit and it does not visit the mouse then the mouse likes the dog. If the rabbit is blue and the rabbit is not big then the rabbit does not like the dog. If the dog is blue and the dog visits the mouse then the mouse is not kind. If something visits the rabbit and it is not big then it is not blue. If something visits the rabbit and the rabbit does not like the dog then it does not need the mouse.
The dog is not green.
("dog" "is" "green" "-")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The dog does not visit the mouse.
("dog" "visits" "mouse" "-")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse does not like the dog.
("mouse" "likes" "dog" "-")
The mouse does not like the rabbit.
("mouse" "likes" "rabbit" "-")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
If the rabbit visits the mouse then the mouse is big.
((("rabbit" "visits" "mouse" "+")) -> ("mouse" "is" "big" "+"))
Big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If something needs the dog and the dog likes the rabbit then it is big.
((("something" "needs" "dog" "+") ("dog" "likes" "rabbit" "+")) -> ("something" "is" "big" "+"))
If something needs the rabbit and it does not visit the mouse then the mouse likes the dog.
((("something" "needs" "rabbit" "+") ("something" "visits" "mouse" "~")) -> ("mouse" "likes" "dog" "+"))
If the rabbit is blue and the rabbit is not big then the rabbit does not like the dog.
((("rabbit" "is" "blue" "+") ("rabbit" "is" "big" "~")) -> ("rabbit" "likes" "dog" "-"))
If the dog is blue and the dog visits the mouse then the mouse is not kind.
((("dog" "is" "blue" "+") ("dog" "visits" "mouse" "+")) -> ("mouse" "is" "kind" "-"))
If something visits the rabbit and it is not big then it is not blue.
((("something" "visits" "rabbit" "+") ("something" "is" "big" "~")) -> ("something" "is" "blue" "-"))
If something visits the rabbit and the rabbit does not like the dog then it does not need the mouse.
((("something" "visits" "rabbit" "+") ("rabbit" "likes" "dog" "~")) -> ("something" "needs" "mouse" "-"))
The mouse is green.
True
1
proof
[(triple5 OR ((((triple8 triple2) -> rule3)) -> rule2))]
("mouse" "is" "green" "+")
triple5
((((triple8 triple2) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The mouse does not need the dog.
False
1
inv-proof
[(triple8)]
("mouse" "needs" "dog" "-")
triple8
The rabbit is big.
True
3
proof
[(((triple13 triple2) -> rule3))]
("rabbit" "is" "big" "+")
((triple13 triple2) -> (rule3 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is not big.
False
3
inv-proof
[(((triple13 triple2) -> rule3))]
("rabbit" "is" "big" "-")
((triple13 triple2) -> (rule3 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is green.
True
4
proof
[(((((triple13 triple2) -> rule3)) -> rule2))]
("rabbit" "is" "green" "+")
((((triple13 triple2) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is not green.
False
4
inv-proof
[(((((triple13 triple2) -> rule3)) -> rule2))]
("rabbit" "is" "green" "-")
((((triple13 triple2) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The dog is not big.
Unknown
inv-rconc
[@1: The dog is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "big" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
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 round.
Unknown
inv-random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
@0: The dog does not visit the mouse.[(triple3)] The dog is not green.[(triple1)] The dog likes the rabbit.[(triple2)] The mouse does not like the dog.[(triple6)] The mouse does not like the rabbit.[(triple7)] The mouse is blue.[(triple4)] The mouse is green.[(triple5 OR ((((triple8 triple2) -> rule3)) -> rule2))] The mouse needs the dog.[(triple8)] The mouse visits the dog.[(triple9)] The mouse visits the rabbit.[(triple10)] The rabbit does not visit the mouse.[(triple16)] The rabbit likes the dog.[(triple11)] The rabbit likes the mouse.[(triple12)] The rabbit needs the dog.[(triple13)] The rabbit needs the mouse.[(triple14)] The rabbit visits the dog.[(triple15)] @1: The mouse is big.[(((triple8 triple2) -> rule3))] The rabbit is big.[(((triple13 triple2) -> rule3))] @2: The rabbit is green.[(((((triple13 triple2) -> rule3)) -> rule2))]
The dog does not visit the mouse.
("dog" "visits" "mouse" "-")
triple3
The dog is not green.
("dog" "is" "green" "-")
triple1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple2
The mouse does not like the dog.
("mouse" "likes" "dog" "-")
triple6
The mouse does not like the rabbit.
("mouse" "likes" "rabbit" "-")
triple7
The mouse is blue.
("mouse" "is" "blue" "+")
triple4
The mouse is green.
("mouse" "is" "green" "+")
triple5
((((triple8 triple2) -> (rule3 % int2))) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple8
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple9
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple10
The rabbit does not visit the mouse.
("rabbit" "visits" "mouse" "-")
triple16
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple11
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple12
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple13
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple14
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple15
The mouse is big.
("mouse" "is" "big" "+")
((triple8 triple2) -> (rule3 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
((triple13 triple2) -> (rule3 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
((((triple13 triple2) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2