The bear likes the squirrel. The rabbit likes the bear. The squirrel eats the rabbit. If something likes the rabbit then it is not blue. If something eats the bear and the bear likes the squirrel then the bear is round. If something likes the bear then it likes the rabbit. If something is cold and nice then it chases the squirrel. If something likes the rabbit then it does not like the squirrel. If something likes the rabbit and the rabbit chases the squirrel then the squirrel eats the rabbit.
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
If something likes the rabbit then it is not blue.
((("something" "likes" "rabbit" "+")) -> ("something" "is" "blue" "-"))
If something eats the bear and the bear likes the squirrel then the bear is round.
((("something" "eats" "bear" "+") ("bear" "likes" "squirrel" "+")) -> ("bear" "is" "round" "+"))
If something likes the bear then it likes the rabbit.
((("something" "likes" "bear" "+")) -> ("something" "likes" "rabbit" "+"))
If something is cold and nice then it chases the squirrel.
((("something" "is" "cold" "+") ("something" "is" "nice" "+")) -> ("something" "chases" "squirrel" "+"))
If something likes the rabbit then it does not like the squirrel.
((("something" "likes" "rabbit" "+")) -> ("something" "likes" "squirrel" "-"))
If something likes the rabbit and the rabbit chases the squirrel then the squirrel eats the rabbit.
((("something" "likes" "rabbit" "+") ("rabbit" "chases" "squirrel" "+")) -> ("squirrel" "eats" "rabbit" "+"))
The squirrel eats the rabbit.
True
1
proof
[(triple3)]
("squirrel" "eats" "rabbit" "+")
triple3
The bear does not like the squirrel.
False
1
inv-proof
[(triple1)]
("bear" "likes" "squirrel" "-")
triple1
The rabbit likes the rabbit.
True
2
proof
[(((triple2) -> rule3))]
("rabbit" "likes" "rabbit" "+")
((triple2) -> (rule3 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit does not like the rabbit.
False
2
inv-proof
[(((triple2) -> rule3))]
("rabbit" "likes" "rabbit" "-")
((triple2) -> (rule3 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit is not blue.
True
3
proof
[(((((triple2) -> rule3)) -> rule1))]
("rabbit" "is" "blue" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit is not blue.
("rabbit" "is" "blue" "-")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The rabbit is blue.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1))]
("rabbit" "is" "blue" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit is not blue.
("rabbit" "is" "blue" "-")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The bear does not chase the squirrel.
Unknown
inv-rconc
[@1: The bear chases the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "chases" "squirrel" "-")
The bear likes the rabbit.
Unknown
rconc
[@1: The bear likes the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "likes" "rabbit" "+")
The squirrel does not chase the squirrel.
Unknown
inv-rconc
[@1: The squirrel chases the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "chases" "squirrel" "-")
The squirrel chases the bear.
Unknown
random
[@0: The squirrel chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "bear" "+")
The bear is not cold.
Unknown
inv-random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "-")
The bear chases the bear.
Unknown
random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "+")
@0: The bear likes the squirrel.[(triple1)] The rabbit likes the bear.[(triple2)] The squirrel eats the rabbit.[(triple3)] @1: The rabbit likes the rabbit.[(((triple2) -> rule3))] @2: The rabbit does not like the squirrel.[(((((triple2) -> rule3)) -> rule5))] The rabbit is not blue.[(((((triple2) -> rule3)) -> rule1))]
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
triple1
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple2
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
triple3
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((triple2) -> (rule3 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit does not like the squirrel.
("rabbit" "likes" "squirrel" "-")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit does not like the squirrel.
("rabbit" "likes" "squirrel" "-")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The rabbit is not blue.
("rabbit" "is" "blue" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit is not blue.
("rabbit" "is" "blue" "-")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2