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