The lion eats the rabbit. The lion is kind. The lion likes the rabbit. The lion likes the squirrel. The lion sees the rabbit. The rabbit eats the lion. The rabbit eats the squirrel. The rabbit is kind. The rabbit is nice. The rabbit is red. The rabbit is round. The rabbit sees the lion. The rabbit sees the squirrel. The squirrel eats the lion. The squirrel is blue. The squirrel is round. If something eats the rabbit then the rabbit is blue. Round things are red. If something eats the rabbit and it is round then it sees the lion. If something sees the rabbit then it is kind. If the squirrel eats the rabbit then the rabbit is nice. If the rabbit is red then the rabbit sees the lion. If something sees the rabbit then the rabbit likes the lion. If something likes the lion then it sees the rabbit.
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
If something eats the rabbit then the rabbit is blue.
((("something" "eats" "rabbit" "+")) -> ("rabbit" "is" "blue" "+"))
Round things are red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If something eats the rabbit and it is round then it sees the lion.
((("something" "eats" "rabbit" "+") ("something" "is" "round" "+")) -> ("something" "sees" "lion" "+"))
If something sees the rabbit then it is kind.
((("something" "sees" "rabbit" "+")) -> ("something" "is" "kind" "+"))
If the squirrel eats the rabbit then the rabbit is nice.
((("squirrel" "eats" "rabbit" "+")) -> ("rabbit" "is" "nice" "+"))
If the rabbit is red then the rabbit sees the lion.
((("rabbit" "is" "red" "+")) -> ("rabbit" "sees" "lion" "+"))
If something sees the rabbit then the rabbit likes the lion.
((("something" "sees" "rabbit" "+")) -> ("rabbit" "likes" "lion" "+"))
If something likes the lion then it sees the rabbit.
((("something" "likes" "lion" "+")) -> ("something" "sees" "rabbit" "+"))
The lion sees the rabbit.
True
1
proof
[(triple5)]
("lion" "sees" "rabbit" "+")
triple5
The rabbit is not red.
False
1
inv-proof
[(triple10 OR ((triple11) -> rule2))]
("rabbit" "is" "red" "-")
triple10
((triple11) -> (rule2 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The squirrel is red.
True
2
proof
[(((triple16) -> rule2))]
("squirrel" "is" "red" "+")
((triple16) -> (rule2 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is not red.
False
2
inv-proof
[(((triple16) -> rule2))]
("squirrel" "is" "red" "-")
((triple16) -> (rule2 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The rabbit sees the rabbit.
True
3
proof
[(((((triple5) -> rule7)) -> rule8))]
("rabbit" "sees" "rabbit" "+")
((((triple5) -> (rule7 % int2))) -> (rule8 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int2
The rabbit does not see the rabbit.
False
3
inv-proof
[(((((triple5) -> rule7)) -> rule8))]
("rabbit" "sees" "rabbit" "-")
((((triple5) -> (rule7 % int2))) -> (rule8 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int2
The squirrel is not kind.
Unknown
inv-rconc
[@2: The squirrel is kind.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("squirrel" "is" "kind" "-")
The lion sees the lion.
Unknown
rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "sees" "lion" "+")
The squirrel does not see the rabbit.
Unknown
inv-rconc
[@1: The squirrel sees the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "sees" "rabbit" "-")
The rabbit likes the squirrel.
Unknown
random
[@0: The rabbit likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "squirrel" "+")
The rabbit does not eat the rabbit.
Unknown
inv-random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "-")
The lion is blue.
Unknown
random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "+")
@0: The lion eats the rabbit.[(triple1)] The lion is kind.[(triple2 OR ((triple5) -> rule4))] The lion likes the rabbit.[(triple3)] The lion likes the squirrel.[(triple4)] The lion sees the rabbit.[(triple5)] The rabbit eats the lion.[(triple6)] The rabbit eats the squirrel.[(triple7)] The rabbit is kind.[(triple8 OR ((((((triple5) -> rule7)) -> rule8)) -> rule4))] The rabbit is nice.[(triple9)] The rabbit is red.[(triple10 OR ((triple11) -> rule2))] The rabbit is round.[(triple11)] The rabbit sees the lion.[(triple12 OR ((triple10) -> rule6) OR ((((triple11) -> rule2)) -> rule6))] The rabbit sees the squirrel.[(triple13)] The squirrel eats the lion.[(triple14)] The squirrel is blue.[(triple15)] The squirrel is round.[(triple16)] @1: The rabbit is blue.[(((triple1) -> rule1))] The rabbit likes the lion.[(((triple5) -> rule7))] The squirrel is red.[(((triple16) -> rule2))] @2: The rabbit sees the rabbit.[(((((triple5) -> rule7)) -> rule8))]
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple1
The lion is kind.
("lion" "is" "kind" "+")
triple2
((triple5) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple3
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple4
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple5
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple6
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
triple7
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple8
((((((triple5) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int3
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple9
The rabbit is red.
("rabbit" "is" "red" "+")
triple10
((triple11) -> (rule2 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
triple11
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple12
((triple10) -> (rule6 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
((((triple11) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple13
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple14
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple15
The squirrel is round.
("squirrel" "is" "round" "+")
triple16
The rabbit is blue.
("rabbit" "is" "blue" "+")
((triple1) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
((triple5) -> (rule7 % int1))
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
((triple16) -> (rule2 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((((triple5) -> (rule7 % int2))) -> (rule8 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
int2