The dog chases the mouse. The dog is not big. The dog is not kind. The dog likes the squirrel. The mouse is blue. The mouse is cold. The mouse likes the squirrel. The mouse needs the squirrel. The squirrel does not chase the mouse. The squirrel is blue. The squirrel needs the dog. The squirrel needs the mouse. If something is big then it likes the dog. If something is blue and it likes the squirrel then it needs the dog.
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog is not big.
("dog" "is" "big" "-")
The dog is not kind.
("dog" "is" "kind" "-")
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The squirrel does not chase the mouse.
("squirrel" "chases" "mouse" "-")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
If something is big then it likes the dog.
((("something" "is" "big" "+")) -> ("something" "likes" "dog" "+"))
If something is blue and it likes the squirrel then it needs the dog.
((("something" "is" "blue" "+") ("something" "likes" "squirrel" "+")) -> ("something" "needs" "dog" "+"))
The dog is not kind.
True
1
proof
[(triple3)]
("dog" "is" "kind" "-")
triple3
The squirrel is not blue.
False
1
inv-proof
[(triple10)]
("squirrel" "is" "blue" "-")
triple10
The mouse needs the dog.
True
3
proof
[(((triple5 triple7) -> rule2))]
("mouse" "needs" "dog" "+")
((triple5 triple7) -> (rule2 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse does not need the dog.
False
3
inv-proof
[(((triple5 triple7) -> rule2))]
("mouse" "needs" "dog" "-")
((triple5 triple7) -> (rule2 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The dog does not need the dog.
Unknown
inv-rconc
[@1: The dog needs the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "needs" "dog" "-")
The dog likes the dog.
Unknown
rconc
[@1: The dog likes the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "likes" "dog" "+")
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 squirrel likes the mouse.
Unknown
random
[@0: The squirrel likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "mouse" "+")
@0: The dog chases the mouse.[(triple1)] The dog is not big.[(triple2)] The dog is not kind.[(triple3)] The dog likes the squirrel.[(triple4)] The mouse is blue.[(triple5)] The mouse is cold.[(triple6)] The mouse likes the squirrel.[(triple7)] The mouse needs the squirrel.[(triple8)] The squirrel does not chase the mouse.[(triple9)] The squirrel is blue.[(triple10)] The squirrel needs the dog.[(triple11)] The squirrel needs the mouse.[(triple12)] @1: The mouse needs the dog.[(((triple5 triple7) -> rule2))]
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple1
The dog is not big.
("dog" "is" "big" "-")
triple2
The dog is not kind.
("dog" "is" "kind" "-")
triple3
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
triple4
The mouse is blue.
("mouse" "is" "blue" "+")
triple5
The mouse is cold.
("mouse" "is" "cold" "+")
triple6
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple7
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple8
The squirrel does not chase the mouse.
("squirrel" "chases" "mouse" "-")
triple9
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple10
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
triple11
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple12
The mouse needs the dog.
("mouse" "needs" "dog" "+")
((triple5 triple7) -> (rule2 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1