The dog sees the mouse. The mouse is cold. The mouse sees the dog. If something visits the dog then it is big. If something eats the dog then the dog sees the mouse. If the dog is green and the dog eats the mouse then the dog sees the mouse.
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
If something visits the dog then it is big.
((("something" "visits" "dog" "+")) -> ("something" "is" "big" "+"))
If something eats the dog then the dog sees the mouse.
((("something" "eats" "dog" "+")) -> ("dog" "sees" "mouse" "+"))
If the dog is green and the dog eats the mouse then the dog sees the mouse.
((("dog" "is" "green" "+") ("dog" "eats" "mouse" "+")) -> ("dog" "sees" "mouse" "+"))
The mouse sees the dog.
True
1
proof
[(triple3)]
("mouse" "sees" "dog" "+")
triple3
The mouse does not see the dog.
False
1
inv-proof
[(triple3)]
("mouse" "sees" "dog" "-")
triple3
The mouse is not big.
Unknown
inv-rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "big" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
@0: The dog sees the mouse.[(triple1)] The mouse is cold.[(triple2)] The mouse sees the dog.[(triple3)]
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple1
The mouse is cold.
("mouse" "is" "cold" "+")
triple2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple3