The cat sees the dog. The dog is cold. The dog sees the mouse. The dog visits the cat. The dog visits the mouse. The mouse sees the dog. The mouse visits the dog. If someone visits the dog then they visit the mouse.
The cat sees the dog.
("cat" "sees" "dog" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
If someone visits the dog then they visit the mouse.
((("someone" "visits" "dog" "+")) -> ("someone" "visits" "mouse" "+"))
The dog visits the cat.
True
1
proof
[(triple4)]
("dog" "visits" "cat" "+")
triple4
The mouse does not see the dog.
False
1
inv-proof
[(triple6)]
("mouse" "sees" "dog" "-")
triple6
The cat does not visit the mouse.
Unknown
inv-rconc
[@1: The cat visits the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "visits" "mouse" "-")
The dog sees the cat.
Unknown
random
[@0: The dog sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "cat" "+")
@0: The cat sees the dog.[(triple1)] The dog is cold.[(triple2)] The dog sees the mouse.[(triple3)] The dog visits the cat.[(triple4)] The dog visits the mouse.[(triple5)] The mouse sees the dog.[(triple6)] The mouse visits the dog.[(triple7)] @1: The mouse visits the mouse.[(((triple7) -> rule1))]
The cat sees the dog.
("cat" "sees" "dog" "+")
triple1
The dog is cold.
("dog" "is" "cold" "+")
triple2
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple3
The dog visits the cat.
("dog" "visits" "cat" "+")
triple4
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple5
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple6
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple7
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((triple7) -> (rule1 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1