The bear does not like the squirrel. The dog is rough. The rabbit is red. The squirrel visits the dog. If the bear needs the rabbit then the rabbit is red. If something needs the rabbit and the rabbit is rough then the rabbit likes the bear. If something is rough then it is round. If something is red and not blue then it is rough. If the squirrel likes the bear and the bear does not need the squirrel then the squirrel needs the rabbit. If something is round and it visits the squirrel then the squirrel is rough. If something likes the rabbit and it does not need the rabbit then it needs the bear. If the rabbit does not like the dog and the dog is not rough then the dog needs the bear.
The bear does not like the squirrel.
("bear" "likes" "squirrel" "-")
The dog is rough.
("dog" "is" "rough" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
If the bear needs the rabbit then the rabbit is red.
((("bear" "needs" "rabbit" "+")) -> ("rabbit" "is" "red" "+"))
If something needs the rabbit and the rabbit is rough then the rabbit likes the bear.
((("something" "needs" "rabbit" "+") ("rabbit" "is" "rough" "+")) -> ("rabbit" "likes" "bear" "+"))
If something is rough then it is round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something is red and not blue then it is rough.
((("something" "is" "red" "+") ("something" "is" "blue" "~")) -> ("something" "is" "rough" "+"))
If the squirrel likes the bear and the bear does not need the squirrel then the squirrel needs the rabbit.
((("squirrel" "likes" "bear" "+") ("bear" "needs" "squirrel" "~")) -> ("squirrel" "needs" "rabbit" "+"))
If something is round and it visits the squirrel then the squirrel is rough.
((("something" "is" "round" "+") ("something" "visits" "squirrel" "+")) -> ("squirrel" "is" "rough" "+"))
If something likes the rabbit and it does not need the rabbit then it needs the bear.
((("something" "likes" "rabbit" "+") ("something" "needs" "rabbit" "~")) -> ("something" "needs" "bear" "+"))
If the rabbit does not like the dog and the dog is not rough then the dog needs the bear.
((("rabbit" "likes" "dog" "~") ("dog" "is" "rough" "~")) -> ("dog" "needs" "bear" "+"))
The dog is rough.
True
1
proof
[(triple2)]
("dog" "is" "rough" "+")
triple2
The squirrel does not visit the dog.
False
1
inv-proof
[(triple4)]
("squirrel" "visits" "dog" "-")
triple4
The dog is round.
True
2
proof
[(((triple2) -> rule3))]
("dog" "is" "round" "+")
((triple2) -> (rule3 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is not round.
False
2
inv-proof
[(((triple2) -> rule3))]
("dog" "is" "round" "-")
((triple2) -> (rule3 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The squirrel is not rough.
Unknown
inv-rconc
[@1: The squirrel is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "is" "rough" "-")
The rabbit needs the bear.
Unknown
rconc
[@1: The rabbit needs the bear.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "needs" "bear" "+")
The squirrel does not visit the rabbit.
Unknown
inv-random
[@0: The squirrel visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "rabbit" "-")
The rabbit is blue.
Unknown
random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "+")
@0: The bear does not like the squirrel.[(triple1)] The dog is rough.[(triple2)] The rabbit is red.[(triple3)] The squirrel visits the dog.[(triple4)] @1: The dog is round.[(((triple2) -> rule3))]
The bear does not like the squirrel.
("bear" "likes" "squirrel" "-")
triple1
The dog is rough.
("dog" "is" "rough" "+")
triple2
The rabbit is red.
("rabbit" "is" "red" "+")
triple3
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple4
The dog is round.
("dog" "is" "round" "+")
((triple2) -> (rule3 % int1))
The dog is round.
("dog" "is" "round" "+")
int1