The bear eats the squirrel. The dog is cold. The rabbit is round. The squirrel is round. If the rabbit visits the squirrel then the rabbit is blue. If someone is blue then they visit the dog. If someone is cold then they visit the dog. If the squirrel visits the rabbit then the squirrel eats the rabbit. If someone visits the dog then they visit the bear. If someone is cold then they eat the rabbit.
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
The dog is cold.
("dog" "is" "cold" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
If the rabbit visits the squirrel then the rabbit is blue.
((("rabbit" "visits" "squirrel" "+")) -> ("rabbit" "is" "blue" "+"))
If someone is blue then they visit the dog.
((("someone" "is" "blue" "+")) -> ("someone" "visits" "dog" "+"))
If someone is cold then they visit the dog.
((("someone" "is" "cold" "+")) -> ("someone" "visits" "dog" "+"))
If the squirrel visits the rabbit then the squirrel eats the rabbit.
((("squirrel" "visits" "rabbit" "+")) -> ("squirrel" "eats" "rabbit" "+"))
If someone visits the dog then they visit the bear.
((("someone" "visits" "dog" "+")) -> ("someone" "visits" "bear" "+"))
If someone is cold then they eat the rabbit.
((("someone" "is" "cold" "+")) -> ("someone" "eats" "rabbit" "+"))
The rabbit is round.
True
1
proof
[(triple3)]
("rabbit" "is" "round" "+")
triple3
The bear does not eat the squirrel.
False
1
inv-proof
[(triple1)]
("bear" "eats" "squirrel" "-")
triple1
The dog visits the dog.
True
2
proof
[(((triple2) -> rule3))]
("dog" "visits" "dog" "+")
((triple2) -> (rule3 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog does not visit the dog.
False
2
inv-proof
[(((triple2) -> rule3))]
("dog" "visits" "dog" "-")
((triple2) -> (rule3 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog visits the bear.
True
3
proof
[(((((triple2) -> rule3)) -> rule5))]
("dog" "visits" "bear" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The dog visits the bear.
("dog" "visits" "bear" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog does not visit the bear.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule5))]
("dog" "visits" "bear" "-")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The dog visits the bear.
("dog" "visits" "bear" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The bear does not visit the bear.
Unknown
inv-rconc
[@2: The bear visits the bear.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("bear" "visits" "bear" "-")
The squirrel visits the dog.
Unknown
rconc
[@1: The squirrel visits the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "visits" "dog" "+")
The squirrel does not visit the bear.
Unknown
inv-rconc
[@2: The squirrel visits the bear.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("squirrel" "visits" "bear" "-")
The rabbit eats the dog.
Unknown
random
[@0: The rabbit eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "dog" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
@0: The bear eats the squirrel.[(triple1)] The dog is cold.[(triple2)] The rabbit is round.[(triple3)] The squirrel is round.[(triple4)] @1: The dog eats the rabbit.[(((triple2) -> rule6))] The dog visits the dog.[(((triple2) -> rule3))] @2: The dog visits the bear.[(((((triple2) -> rule3)) -> rule5))]
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
triple1
The dog is cold.
("dog" "is" "cold" "+")
triple2
The rabbit is round.
("rabbit" "is" "round" "+")
triple3
The squirrel is round.
("squirrel" "is" "round" "+")
triple4
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
((triple2) -> (rule6 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
((triple2) -> (rule3 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog visits the bear.
("dog" "visits" "bear" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The dog visits the bear.
("dog" "visits" "bear" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2