The bear visits the mouse. The dog is green. The dog is rough. The mouse is rough. The mouse likes the bear. The mouse likes the dog. The mouse visits the dog. If something visits the mouse and it is big then it visits the dog. If something visits the dog and the dog visits the mouse then the mouse is big. If the dog visits the bear then the dog is big. If the mouse is nice and the mouse needs the dog then the mouse visits the bear. If something is rough and it likes the dog then it is green. If something visits the bear and it likes the mouse then it likes the dog.
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is rough.
("dog" "is" "rough" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
If something visits the mouse and it is big then it visits the dog.
((("something" "visits" "mouse" "+") ("something" "is" "big" "+")) -> ("something" "visits" "dog" "+"))
If something visits the dog and the dog visits the mouse then the mouse is big.
((("something" "visits" "dog" "+") ("dog" "visits" "mouse" "+")) -> ("mouse" "is" "big" "+"))
If the dog visits the bear then the dog is big.
((("dog" "visits" "bear" "+")) -> ("dog" "is" "big" "+"))
If the mouse is nice and the mouse needs the dog then the mouse visits the bear.
((("mouse" "is" "nice" "+") ("mouse" "needs" "dog" "+")) -> ("mouse" "visits" "bear" "+"))
If something is rough and it likes the dog then it is green.
((("something" "is" "rough" "+") ("something" "likes" "dog" "+")) -> ("something" "is" "green" "+"))
If something visits the bear and it likes the mouse then it likes the dog.
((("something" "visits" "bear" "+") ("something" "likes" "mouse" "+")) -> ("something" "likes" "dog" "+"))
The dog is green.
True
1
proof
[(triple2)]
("dog" "is" "green" "+")
triple2
The dog is not rough.
False
1
inv-proof
[(triple3)]
("dog" "is" "rough" "-")
triple3
The mouse is green.
True
3
proof
[(((triple4 triple6) -> rule5))]
("mouse" "is" "green" "+")
((triple4 triple6) -> (rule5 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is not green.
False
3
inv-proof
[(((triple4 triple6) -> rule5))]
("mouse" "is" "green" "-")
((triple4 triple6) -> (rule5 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse does not visit the bear.
Unknown
inv-rconc
[@1: The mouse visits the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "visits" "bear" "-")
The dog likes the dog.
Unknown
rconc
[@1: The dog likes the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "likes" "dog" "+")
The bear is not cold.
Unknown
inv-random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "-")
The dog is cold.
Unknown
random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "+")
@0: The bear visits the mouse.[(triple1)] The dog is green.[(triple2)] The dog is rough.[(triple3)] The mouse is rough.[(triple4)] The mouse likes the bear.[(triple5)] The mouse likes the dog.[(triple6)] The mouse visits the dog.[(triple7)] @1: The mouse is green.[(((triple4 triple6) -> rule5))]
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple1
The dog is green.
("dog" "is" "green" "+")
triple2
The dog is rough.
("dog" "is" "rough" "+")
triple3
The mouse is rough.
("mouse" "is" "rough" "+")
triple4
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple5
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple6
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple7
The mouse is green.
("mouse" "is" "green" "+")
((triple4 triple6) -> (rule5 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1