The bear is red. The bear needs the lion. The bear sees the lion. The bear sees the rabbit. The lion is blue. The lion is cold. The lion is nice. The lion likes the bear. The lion sees the rabbit. The rabbit is nice. The rabbit is red. The rabbit likes the bear. The rabbit needs the bear. The rabbit sees the bear. The rabbit sees the lion. If something is blue and cold then it needs the lion. If the bear is red then the bear likes the lion. If something likes the rabbit then it needs the rabbit. If the lion needs the rabbit and the rabbit likes the bear then the bear likes the rabbit. If something likes the lion and the lion is kind then the lion needs the rabbit. If the bear is nice then the bear is cold. If something likes the rabbit and the rabbit likes the bear then the bear is nice. If something likes the bear and it sees the rabbit then it likes the rabbit.
The bear is red.
("bear" "is" "red" "+")
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 is blue.
("lion" "is" "blue" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If something is blue and cold then it needs the lion.
((("something" "is" "blue" "+") ("something" "is" "cold" "+")) -> ("something" "needs" "lion" "+"))
If the bear is red then the bear likes the lion.
((("bear" "is" "red" "+")) -> ("bear" "likes" "lion" "+"))
If something likes the rabbit then it needs the rabbit.
((("something" "likes" "rabbit" "+")) -> ("something" "needs" "rabbit" "+"))
If the lion needs the rabbit and the rabbit likes the bear then the bear likes the rabbit.
((("lion" "needs" "rabbit" "+") ("rabbit" "likes" "bear" "+")) -> ("bear" "likes" "rabbit" "+"))
If something likes the lion and the lion is kind then the lion needs the rabbit.
((("something" "likes" "lion" "+") ("lion" "is" "kind" "+")) -> ("lion" "needs" "rabbit" "+"))
If the bear is nice then the bear is cold.
((("bear" "is" "nice" "+")) -> ("bear" "is" "cold" "+"))
If something likes the rabbit and the rabbit likes the bear then the bear is nice.
((("something" "likes" "rabbit" "+") ("rabbit" "likes" "bear" "+")) -> ("bear" "is" "nice" "+"))
If something likes the bear and it sees the rabbit then it likes the rabbit.
((("something" "likes" "bear" "+") ("something" "sees" "rabbit" "+")) -> ("something" "likes" "rabbit" "+"))
The lion is blue.
True
1
proof
[(triple5)]
("lion" "is" "blue" "+")
triple5
The rabbit does not see the bear.
False
1
inv-proof
[(triple14)]
("rabbit" "sees" "bear" "-")
triple14
The lion likes the rabbit.
True
3
proof
[(((triple8 triple9) -> rule8))]
("lion" "likes" "rabbit" "+")
((triple8 triple9) -> (rule8 % int1))
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int1
The lion does not like the rabbit.
False
3
inv-proof
[(((triple8 triple9) -> rule8))]
("lion" "likes" "rabbit" "-")
((triple8 triple9) -> (rule8 % int1))
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int1
The bear is nice.
True
5
proof
[(((((triple8 triple9) -> rule8) triple12) -> rule7) OR ((((((((triple8 triple9) -> rule8)) -> rule3) triple12) -> rule4) triple12) -> rule7))]
("bear" "is" "nice" "+")
((((triple8 triple9) -> (rule8 % int2)) triple12) -> (rule7 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int2
((((((((triple8 triple9) -> (rule8 % int4))) -> (rule3 % int3)) triple12) -> (rule4 % int2)) triple12) -> (rule7 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int2
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int3
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int4
The bear is not nice.
False
5
inv-proof
[(((((triple8 triple9) -> rule8) triple12) -> rule7) OR ((((((((triple8 triple9) -> rule8)) -> rule3) triple12) -> rule4) triple12) -> rule7))]
("bear" "is" "nice" "-")
((((triple8 triple9) -> (rule8 % int2)) triple12) -> (rule7 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int2
((((((((triple8 triple9) -> (rule8 % int4))) -> (rule3 % int3)) triple12) -> (rule4 % int2)) triple12) -> (rule7 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int2
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int3
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int4
The rabbit does not need the lion.
Unknown
inv-rconc
[@1: The rabbit needs the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "needs" "lion" "-")
The rabbit likes the rabbit.
Unknown
rconc
[@1: The rabbit likes the rabbit.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "likes" "rabbit" "+")
The rabbit does not need the rabbit.
Unknown
inv-rconc
[@2: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule3 <- rule8 <- FAIL)]]
("rabbit" "needs" "rabbit" "-")
The lion needs the bear.
Unknown
random
[@0: The lion needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "bear" "+")
The lion is not red.
Unknown
inv-random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "-")
The bear is blue.
Unknown
random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "+")
@0: The bear is red.[(triple1)] The bear needs the lion.[(triple2)] The bear sees the lion.[(triple3)] The bear sees the rabbit.[(triple4)] The lion is blue.[(triple5)] The lion is cold.[(triple6)] The lion is nice.[(triple7)] The lion likes the bear.[(triple8)] The lion sees the rabbit.[(triple9)] The rabbit is nice.[(triple10)] The rabbit is red.[(triple11)] The rabbit likes the bear.[(triple12)] The rabbit needs the bear.[(triple13)] The rabbit sees the bear.[(triple14)] The rabbit sees the lion.[(triple15)] @1: The bear likes the lion.[(((triple1) -> rule2))] The lion likes the rabbit.[(((triple8 triple9) -> rule8))] The lion needs the lion.[(((triple5 triple6) -> rule1))] @2: The bear is nice.[(((((triple8 triple9) -> rule8) triple12) -> rule7) OR ((((((((triple8 triple9) -> rule8)) -> rule3) triple12) -> rule4) triple12) -> rule7))] The lion needs the rabbit.[(((((triple8 triple9) -> rule8)) -> rule3))] @3: The bear is cold.[(((((((triple8 triple9) -> rule8) triple12) -> rule7)) -> rule6) OR ((((((((((triple8 triple9) -> rule8)) -> rule3) triple12) -> rule4) triple12) -> rule7)) -> rule6))] The bear likes the rabbit.[(((((((triple8 triple9) -> rule8)) -> rule3) triple12) -> rule4))] @4: The bear needs the rabbit.[(((((((((triple8 triple9) -> rule8)) -> rule3) triple12) -> rule4)) -> rule3))]
The bear is red.
("bear" "is" "red" "+")
triple1
The bear needs the lion.
("bear" "needs" "lion" "+")
triple2
The bear sees the lion.
("bear" "sees" "lion" "+")
triple3
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple4
The lion is blue.
("lion" "is" "blue" "+")
triple5
The lion is cold.
("lion" "is" "cold" "+")
triple6
The lion is nice.
("lion" "is" "nice" "+")
triple7
The lion likes the bear.
("lion" "likes" "bear" "+")
triple8
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple9
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple10
The rabbit is red.
("rabbit" "is" "red" "+")
triple11
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple12
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple13
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
triple14
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple15
The bear likes the lion.
("bear" "likes" "lion" "+")
((triple1) -> (rule2 % int1))
The bear likes the lion.
("bear" "likes" "lion" "+")
int1
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
((triple8 triple9) -> (rule8 % int1))
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple5 triple6) -> (rule1 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
((((triple8 triple9) -> (rule8 % int2)) triple12) -> (rule7 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int2
((((((((triple8 triple9) -> (rule8 % int4))) -> (rule3 % int3)) triple12) -> (rule4 % int2)) triple12) -> (rule7 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int2
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int3
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int4
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
((((triple8 triple9) -> (rule8 % int2))) -> (rule3 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int2
The bear is cold.
("bear" "is" "cold" "+")
((((((triple8 triple9) -> (rule8 % int3)) triple12) -> (rule7 % int2))) -> (rule6 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int3
((((((((((triple8 triple9) -> (rule8 % int5))) -> (rule3 % int4)) triple12) -> (rule4 % int3)) triple12) -> (rule7 % int2))) -> (rule6 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int3
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int4
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int5
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
((((((triple8 triple9) -> (rule8 % int3))) -> (rule3 % int2)) triple12) -> (rule4 % int1))
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int1
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int2
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int3
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
((((((((triple8 triple9) -> (rule8 % int4))) -> (rule3 % int3)) triple12) -> (rule4 % int2))) -> (rule3 % int1))
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int1
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int2
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int3
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
int4