The dog is cold. The dog is rough. The dog likes the rabbit. The mouse is big. The mouse likes the rabbit. The mouse visits the rabbit. The rabbit is big. The rabbit is blue. The rabbit is cold. The rabbit is young. The rabbit likes the dog. The rabbit sees the mouse. If someone is cold then they visit the mouse. If someone sees the rabbit and they visit the dog then they see the mouse.
The dog is cold.
("dog" "is" "cold" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If someone is cold then they visit the mouse.
((("someone" "is" "cold" "+")) -> ("someone" "visits" "mouse" "+"))
If someone sees the rabbit and they visit the dog then they see the mouse.
((("someone" "sees" "rabbit" "+") ("someone" "visits" "dog" "+")) -> ("someone" "sees" "mouse" "+"))
The rabbit sees the mouse.
True
1
proof
[(triple12)]
("rabbit" "sees" "mouse" "+")
triple12
The rabbit is not big.
False
1
inv-proof
[(triple7)]
("rabbit" "is" "big" "-")
triple7
The rabbit visits the mouse.
True
2
proof
[(((triple9) -> rule1))]
("rabbit" "visits" "mouse" "+")
((triple9) -> (rule1 % int1))
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int1
The dog does not visit the mouse.
False
2
inv-proof
[(((triple1) -> rule1))]
("dog" "visits" "mouse" "-")
((triple1) -> (rule1 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse visits the mouse.
Unknown
rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "visits" "mouse" "+")
The dog does not like the mouse.
Unknown
inv-random
[@0: The dog likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "mouse" "-")
The mouse visits the dog.
Unknown
random
[@0: The mouse visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "dog" "+")
@0: The dog is cold.[(triple1)] The dog is rough.[(triple2)] The dog likes the rabbit.[(triple3)] The mouse is big.[(triple4)] The mouse likes the rabbit.[(triple5)] The mouse visits the rabbit.[(triple6)] The rabbit is big.[(triple7)] The rabbit is blue.[(triple8)] The rabbit is cold.[(triple9)] The rabbit is young.[(triple10)] The rabbit likes the dog.[(triple11)] The rabbit sees the mouse.[(triple12)] @1: The dog visits the mouse.[(((triple1) -> rule1))] The rabbit visits the mouse.[(((triple9) -> rule1))]
The dog is cold.
("dog" "is" "cold" "+")
triple1
The dog is rough.
("dog" "is" "rough" "+")
triple2
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple3
The mouse is big.
("mouse" "is" "big" "+")
triple4
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple5
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple6
The rabbit is big.
("rabbit" "is" "big" "+")
triple7
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple8
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple9
The rabbit is young.
("rabbit" "is" "young" "+")
triple10
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple11
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple12
The dog visits the mouse.
("dog" "visits" "mouse" "+")
((triple1) -> (rule1 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
((triple9) -> (rule1 % int1))
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int1