The dog is blue. The dog likes the squirrel. The dog visits the mouse. The dog does not visit the squirrel. The mouse chases the squirrel. The mouse is round. The squirrel visits the dog. If something likes the squirrel then the squirrel likes the dog. If something likes the squirrel then the squirrel does not visit the mouse.
The dog is blue.
("dog" "is" "blue" "+")
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The dog does not visit the squirrel.
("dog" "visits" "squirrel" "-")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse is round.
("mouse" "is" "round" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
If something likes the squirrel then the squirrel likes the dog.
((("something" "likes" "squirrel" "+")) -> ("squirrel" "likes" "dog" "+"))
If something likes the squirrel then the squirrel does not visit the mouse.
((("something" "likes" "squirrel" "+")) -> ("squirrel" "visits" "mouse" "-"))
The mouse chases the squirrel.
True
1
proof
[(triple5)]
("mouse" "chases" "squirrel" "+")
triple5
The dog is not blue.
False
1
inv-proof
[(triple1)]
("dog" "is" "blue" "-")
triple1
The squirrel does not visit the mouse.
True
2
proof
[(((triple2) -> rule2))]
("squirrel" "visits" "mouse" "-")
((triple2) -> (rule2 % int1))
The squirrel does not visit the mouse.
("squirrel" "visits" "mouse" "-")
int1
The squirrel visits the mouse.
False
2
inv-proof
[(((triple2) -> rule2))]
("squirrel" "visits" "mouse" "+")
((triple2) -> (rule2 % int1))
The squirrel does not visit the mouse.
("squirrel" "visits" "mouse" "-")
int1
The mouse does not chase the dog.
Unknown
inv-random
[@0: The mouse chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "dog" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
The squirrel is not blue.
Unknown
inv-random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "-")
The dog chases the mouse.
Unknown
random
[@0: The dog chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "mouse" "+")
@0: The dog does not visit the squirrel.[(triple4)] The dog is blue.[(triple1)] The dog likes the squirrel.[(triple2)] The dog visits the mouse.[(triple3)] The mouse chases the squirrel.[(triple5)] The mouse is round.[(triple6)] The squirrel visits the dog.[(triple7)] @1: The squirrel does not visit the mouse.[(((triple2) -> rule2))] The squirrel likes the dog.[(((triple2) -> rule1))]
The dog does not visit the squirrel.
("dog" "visits" "squirrel" "-")
triple4
The dog is blue.
("dog" "is" "blue" "+")
triple1
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
triple2
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple3
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple5
The mouse is round.
("mouse" "is" "round" "+")
triple6
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple7
The squirrel does not visit the mouse.
("squirrel" "visits" "mouse" "-")
((triple2) -> (rule2 % int1))
The squirrel does not visit the mouse.
("squirrel" "visits" "mouse" "-")
int1
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
((triple2) -> (rule1 % int1))
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
int1