The dog is rough. The squirrel chases the dog. If something likes the dog then the dog is rough. If something needs the dog and it chases the dog then the dog chases the squirrel. If the dog chases the squirrel then the squirrel chases the dog. If the dog chases the squirrel then the dog likes the squirrel. If something is red and it needs the dog then the dog is rough. If something chases the dog then it likes the squirrel.
The dog is rough.
("dog" "is" "rough" "+")
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
If something likes the dog then the dog is rough.
((("something" "likes" "dog" "+")) -> ("dog" "is" "rough" "+"))
If something needs the dog and it chases the dog then the dog chases the squirrel.
((("something" "needs" "dog" "+") ("something" "chases" "dog" "+")) -> ("dog" "chases" "squirrel" "+"))
If the dog chases the squirrel then the squirrel chases the dog.
((("dog" "chases" "squirrel" "+")) -> ("squirrel" "chases" "dog" "+"))
If the dog chases the squirrel then the dog likes the squirrel.
((("dog" "chases" "squirrel" "+")) -> ("dog" "likes" "squirrel" "+"))
If something is red and it needs the dog then the dog is rough.
((("something" "is" "red" "+") ("something" "needs" "dog" "+")) -> ("dog" "is" "rough" "+"))
If something chases the dog then it likes the squirrel.
((("something" "chases" "dog" "+")) -> ("something" "likes" "squirrel" "+"))
The dog is rough.
True
1
proof
[(triple1)]
("dog" "is" "rough" "+")
triple1
The dog is not rough.
False
1
inv-proof
[(triple1)]
("dog" "is" "rough" "-")
triple1
The squirrel likes the squirrel.
True
2
proof
[(((triple2) -> rule6))]
("squirrel" "likes" "squirrel" "+")
((triple2) -> (rule6 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The squirrel does not like the squirrel.
False
2
inv-proof
[(((triple2) -> rule6))]
("squirrel" "likes" "squirrel" "-")
((triple2) -> (rule6 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1
The dog does not like the squirrel.
Unknown
inv-rconc
[@2: The dog likes the squirrel.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("dog" "likes" "squirrel" "-")
The dog chases the squirrel.
Unknown
rconc
[@1: The dog chases the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "chases" "squirrel" "+")
The squirrel is not rough.
Unknown
inv-random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "-")
The squirrel needs the dog.
Unknown
random
[@0: The squirrel needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "dog" "+")
@0: The dog is rough.[(triple1)] The squirrel chases the dog.[(triple2)] @1: The squirrel likes the squirrel.[(((triple2) -> rule6))]
The dog is rough.
("dog" "is" "rough" "+")
triple1
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
triple2
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
((triple2) -> (rule6 % int1))
The squirrel likes the squirrel.
("squirrel" "likes" "squirrel" "+")
int1