The cat is round. The cat likes the lion. The lion is big. The lion is young. The rabbit is big. The rabbit needs the cat. The squirrel chases the cat. If something chases the lion and the lion chases the squirrel then the squirrel likes the rabbit. If something needs the cat then the cat needs the rabbit. If something needs the rabbit then the rabbit is young.
The cat is round.
("cat" "is" "round" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is young.
("lion" "is" "young" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
If something chases the lion and the lion chases the squirrel then the squirrel likes the rabbit.
((("something" "chases" "lion" "+") ("lion" "chases" "squirrel" "+")) -> ("squirrel" "likes" "rabbit" "+"))
If something needs the cat then the cat needs the rabbit.
((("something" "needs" "cat" "+")) -> ("cat" "needs" "rabbit" "+"))
If something needs the rabbit then the rabbit is young.
((("something" "needs" "rabbit" "+")) -> ("rabbit" "is" "young" "+"))
The lion is big.
True
1
proof
[(triple3)]
("lion" "is" "big" "+")
triple3
The rabbit does not need the cat.
False
1
inv-proof
[(triple6)]
("rabbit" "needs" "cat" "-")
triple6
The cat needs the rabbit.
True
2
proof
[(((triple6) -> rule2))]
("cat" "needs" "rabbit" "+")
((triple6) -> (rule2 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The cat does not need the rabbit.
False
2
inv-proof
[(((triple6) -> rule2))]
("cat" "needs" "rabbit" "-")
((triple6) -> (rule2 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The rabbit is young.
True
3
proof
[(((((triple6) -> rule2)) -> rule3))]
("rabbit" "is" "young" "+")
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int2
The rabbit is not young.
False
3
inv-proof
[(((((triple6) -> rule2)) -> rule3))]
("rabbit" "is" "young" "-")
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int2
The squirrel does not like the rabbit.
Unknown
inv-rconc
[@1: The squirrel likes the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "likes" "rabbit" "-")
The cat is cold.
Unknown
random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "+")
The lion does not like the squirrel.
Unknown
inv-random
[@0: The lion likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "squirrel" "-")
The squirrel needs the rabbit.
Unknown
random
[@0: The squirrel needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "rabbit" "+")
The cat does not chase the squirrel.
Unknown
inv-random
[@0: The cat chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "squirrel" "-")
The lion chases the rabbit.
Unknown
random
[@0: The lion chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "rabbit" "+")
@0: The cat is round.[(triple1)] The cat likes the lion.[(triple2)] The lion is big.[(triple3)] The lion is young.[(triple4)] The rabbit is big.[(triple5)] The rabbit needs the cat.[(triple6)] The squirrel chases the cat.[(triple7)] @1: The cat needs the rabbit.[(((triple6) -> rule2))] @2: The rabbit is young.[(((((triple6) -> rule2)) -> rule3))]
The cat is round.
("cat" "is" "round" "+")
triple1
The cat likes the lion.
("cat" "likes" "lion" "+")
triple2
The lion is big.
("lion" "is" "big" "+")
triple3
The lion is young.
("lion" "is" "young" "+")
triple4
The rabbit is big.
("rabbit" "is" "big" "+")
triple5
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple6
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
triple7
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
((triple6) -> (rule2 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
((((triple6) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int2