The bear sees the dog. The dog is cold. The squirrel likes the dog. If the bear likes the dog and the dog visits the squirrel then the dog is young. If someone likes the squirrel then they see the dog. If the dog sees the bear and the bear is rough then the bear is cold. If someone likes the dog then they visit the dog. If someone sees the squirrel then they are not blue. If someone visits the bear then they like the squirrel.
The bear sees the dog.
("bear" "sees" "dog" "+")
The dog is cold.
("dog" "is" "cold" "+")
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
If the bear likes the dog and the dog visits the squirrel then the dog is young.
((("bear" "likes" "dog" "+") ("dog" "visits" "squirrel" "+")) -> ("dog" "is" "young" "+"))
If someone likes the squirrel then they see the dog.
((("someone" "likes" "squirrel" "+")) -> ("someone" "sees" "dog" "+"))
If the dog sees the bear and the bear is rough then the bear is cold.
((("dog" "sees" "bear" "+") ("bear" "is" "rough" "+")) -> ("bear" "is" "cold" "+"))
If someone likes the dog then they visit the dog.
((("someone" "likes" "dog" "+")) -> ("someone" "visits" "dog" "+"))
If someone sees the squirrel then they are not blue.
((("someone" "sees" "squirrel" "+")) -> ("someone" "is" "blue" "-"))
If someone visits the bear then they like the squirrel.
((("someone" "visits" "bear" "+")) -> ("someone" "likes" "squirrel" "+"))
The dog is cold.
True
1
proof
[(triple2)]
("dog" "is" "cold" "+")
triple2
The squirrel does not like the dog.
False
1
inv-proof
[(triple3)]
("squirrel" "likes" "dog" "-")
triple3
The squirrel visits the dog.
True
2
proof
[(((triple3) -> rule4))]
("squirrel" "visits" "dog" "+")
((triple3) -> (rule4 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1
The squirrel does not visit the dog.
False
2
inv-proof
[(((triple3) -> rule4))]
("squirrel" "visits" "dog" "-")
((triple3) -> (rule4 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1
The dog does not visit the dog.
Unknown
inv-rconc
[@1: The dog visits the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "visits" "dog" "-")
The bear visits the dog.
Unknown
rconc
[@1: The bear visits the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "visits" "dog" "+")
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
@0: The bear sees the dog.[(triple1)] The dog is cold.[(triple2)] The squirrel likes the dog.[(triple3)] @1: The squirrel visits the dog.[(((triple3) -> rule4))]
The bear sees the dog.
("bear" "sees" "dog" "+")
triple1
The dog is cold.
("dog" "is" "cold" "+")
triple2
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
triple3
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
((triple3) -> (rule4 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1