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