The lion likes the rabbit. The rabbit chases the lion. The rabbit chases the squirrel. The rabbit is big. The rabbit is red. The rabbit likes the lion. The rabbit likes the squirrel. The rabbit sees the lion. The rabbit sees the squirrel. The squirrel does not chase the rabbit. The squirrel is red. The squirrel sees the lion. If the rabbit likes the lion then the lion is not big. If something is red then it chases the squirrel. If something likes the squirrel then the squirrel is blue.
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel does not chase the rabbit.
("squirrel" "chases" "rabbit" "-")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
If the rabbit likes the lion then the lion is not big.
((("rabbit" "likes" "lion" "+")) -> ("lion" "is" "big" "-"))
If something is red then it chases the squirrel.
((("something" "is" "red" "+")) -> ("something" "chases" "squirrel" "+"))
If something likes the squirrel then the squirrel is blue.
((("something" "likes" "squirrel" "+")) -> ("squirrel" "is" "blue" "+"))
The rabbit chases the squirrel.
True
1
proof
[(triple3 OR ((triple5) -> rule2))]
("rabbit" "chases" "squirrel" "+")
triple3
((triple5) -> (rule2 % int1))
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int1
The squirrel chases the rabbit.
False
1
inv-proof
[(triple10)]
("squirrel" "chases" "rabbit" "+")
triple10
The lion is not big.
True
2
proof
[(((triple6) -> rule1))]
("lion" "is" "big" "-")
((triple6) -> (rule1 % int1))
The lion is not big.
("lion" "is" "big" "-")
int1
The squirrel is not blue.
False
2
inv-proof
[(((triple7) -> rule3))]
("squirrel" "is" "blue" "-")
((triple7) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The lion does not chase the squirrel.
Unknown
inv-rconc
[@1: The lion chases the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "chases" "squirrel" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
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 lion sees the squirrel.
Unknown
random
[@0: The lion sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "squirrel" "+")
@0: The lion likes the rabbit.[(triple1)] The rabbit chases the lion.[(triple2)] The rabbit chases the squirrel.[(triple3 OR ((triple5) -> rule2))] The rabbit is big.[(triple4)] The rabbit is red.[(triple5)] The rabbit likes the lion.[(triple6)] The rabbit likes the squirrel.[(triple7)] The rabbit sees the lion.[(triple8)] The rabbit sees the squirrel.[(triple9)] The squirrel does not chase the rabbit.[(triple10)] The squirrel is red.[(triple11)] The squirrel sees the lion.[(triple12)] @1: The lion is not big.[(((triple6) -> rule1))] The squirrel chases the squirrel.[(((triple11) -> rule2))] The squirrel is blue.[(((triple7) -> rule3))]
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple1
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple2
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
triple3
((triple5) -> (rule2 % int1))
The rabbit chases the squirrel.
("rabbit" "chases" "squirrel" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
triple4
The rabbit is red.
("rabbit" "is" "red" "+")
triple5
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple6
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
triple7
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple8
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple9
The squirrel does not chase the rabbit.
("squirrel" "chases" "rabbit" "-")
triple10
The squirrel is red.
("squirrel" "is" "red" "+")
triple11
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple12
The lion is not big.
("lion" "is" "big" "-")
((triple6) -> (rule1 % int1))
The lion is not big.
("lion" "is" "big" "-")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((triple11) -> (rule2 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
((triple7) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1