The dog is not big. The dog is green. The dog sees the mouse. The dog does not visit the rabbit. The mouse needs the rabbit. The mouse sees the rabbit. The mouse visits the dog. The rabbit sees the dog. The rabbit sees the mouse. The rabbit visits the dog. If someone needs the dog and the dog is rough then they are green. If someone sees the rabbit then the rabbit visits the mouse. If someone is kind then they are not big. If the dog is rough then the dog needs the rabbit. If the dog is rough and the dog needs the mouse then the dog visits the mouse. If the mouse sees the dog and the mouse needs the dog then the mouse does not need the rabbit.
The dog is not big.
("dog" "is" "big" "-")
The dog is green.
("dog" "is" "green" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
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 sees the dog.
("rabbit" "sees" "dog" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
If someone needs the dog and the dog is rough then they are green.
((("someone" "needs" "dog" "+") ("dog" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
If someone sees the rabbit then the rabbit visits the mouse.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "visits" "mouse" "+"))
If someone is kind then they are not big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "-"))
If the dog is rough then the dog needs the rabbit.
((("dog" "is" "rough" "+")) -> ("dog" "needs" "rabbit" "+"))
If the dog is rough and the dog needs the mouse then the dog visits the mouse.
((("dog" "is" "rough" "+") ("dog" "needs" "mouse" "+")) -> ("dog" "visits" "mouse" "+"))
If the mouse sees the dog and the mouse needs the dog then the mouse does not need the rabbit.
((("mouse" "sees" "dog" "+") ("mouse" "needs" "dog" "+")) -> ("mouse" "needs" "rabbit" "-"))
The mouse visits the dog.
True
1
proof
[(triple7)]
("mouse" "visits" "dog" "+")
triple7
The dog does not see the mouse.
False
1
inv-proof
[(triple3)]
("dog" "sees" "mouse" "-")
triple3
The rabbit visits the mouse.
True
2
proof
[(((triple6) -> rule2))]
("rabbit" "visits" "mouse" "+")
((triple6) -> (rule2 % int1))
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int1
The rabbit does not visit the mouse.
False
2
inv-proof
[(((triple6) -> rule2))]
("rabbit" "visits" "mouse" "-")
((triple6) -> (rule2 % int1))
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int1
The dog does not need the rabbit.
Unknown
inv-rconc
[@1: The dog needs the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "needs" "rabbit" "-")
The rabbit is green.
Unknown
rconc
[@1: The rabbit is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "is" "green" "+")
The dog is not round.
Unknown
inv-random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
@0: The dog does not visit the rabbit.[(triple4)] The dog is green.[(triple2)] The dog is not big.[(triple1)] The dog sees the mouse.[(triple3)] The mouse needs the rabbit.[(triple5)] The mouse sees the rabbit.[(triple6)] The mouse visits the dog.[(triple7)] The rabbit sees the dog.[(triple8)] The rabbit sees the mouse.[(triple9)] The rabbit visits the dog.[(triple10)] @1: The rabbit visits the mouse.[(((triple6) -> rule2))]
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
triple4
The dog is green.
("dog" "is" "green" "+")
triple2
The dog is not big.
("dog" "is" "big" "-")
triple1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple3
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple5
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple6
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple7
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple8
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple9
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple10
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
((triple6) -> (rule2 % int1))
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int1