The dog is rough. The dog is not round. The dog does not see the mouse. The dog does not visit the mouse. The dog visits the rabbit. The mouse is big. The mouse is not rough. The mouse needs the dog. The mouse needs the rabbit. The mouse sees the rabbit. The mouse visits the dog. The rabbit is big. The rabbit is rough. The rabbit does not see the dog. The rabbit visits the dog. If someone is red then they visit the dog. If the dog sees the rabbit and the dog sees the mouse then the rabbit is not round. If someone visits the mouse and they do not see the dog then the mouse visits the rabbit.
The dog is rough.
("dog" "is" "rough" "+")
The dog is not round.
("dog" "is" "round" "-")
The dog does not see the mouse.
("dog" "sees" "mouse" "-")
The dog does not visit the mouse.
("dog" "visits" "mouse" "-")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is not rough.
("mouse" "is" "rough" "-")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit does not see the dog.
("rabbit" "sees" "dog" "-")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
If someone is red then they visit the dog.
((("someone" "is" "red" "+")) -> ("someone" "visits" "dog" "+"))
If the dog sees the rabbit and the dog sees the mouse then the rabbit is not round.
((("dog" "sees" "rabbit" "+") ("dog" "sees" "mouse" "+")) -> ("rabbit" "is" "round" "-"))
If someone visits the mouse and they do not see the dog then the mouse visits the rabbit.
((("someone" "visits" "mouse" "+") ("someone" "sees" "dog" "~")) -> ("mouse" "visits" "rabbit" "+"))
The rabbit is rough.
True
1
proof
[(triple13)]
("rabbit" "is" "rough" "+")
triple13
The mouse is not big.
False
1
inv-proof
[(triple6)]
("mouse" "is" "big" "-")
triple6
The dog does not visit the dog.
Unknown
inv-rconc
[@1: The dog visits the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "visits" "dog" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
@0: The dog does not see the mouse.[(triple3)] The dog does not visit the mouse.[(triple4)] The dog is not round.[(triple2)] The dog is rough.[(triple1)] The dog visits the rabbit.[(triple5)] The mouse is big.[(triple6)] The mouse is not rough.[(triple7)] The mouse needs the dog.[(triple8)] The mouse needs the rabbit.[(triple9)] The mouse sees the rabbit.[(triple10)] The mouse visits the dog.[(triple11)] The rabbit does not see the dog.[(triple14)] The rabbit is big.[(triple12)] The rabbit is rough.[(triple13)] The rabbit visits the dog.[(triple15)]
The dog does not see the mouse.
("dog" "sees" "mouse" "-")
triple3
The dog does not visit the mouse.
("dog" "visits" "mouse" "-")
triple4
The dog is not round.
("dog" "is" "round" "-")
triple2
The dog is rough.
("dog" "is" "rough" "+")
triple1
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple5
The mouse is big.
("mouse" "is" "big" "+")
triple6
The mouse is not rough.
("mouse" "is" "rough" "-")
triple7
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple8
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple9
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple10
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple11
The rabbit does not see the dog.
("rabbit" "sees" "dog" "-")
triple14
The rabbit is big.
("rabbit" "is" "big" "+")
triple12
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple13
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple15