The bear eats the rabbit. The bear is rough. The bear likes the lion. The bear likes the rabbit. The lion eats the rabbit. The lion is cold. The lion is rough. The lion is round. The lion is young. The lion sees the bear. The rabbit eats the lion. The rabbit is cold. The rabbit is green. The rabbit is young. The rabbit sees the bear. The rabbit sees the lion. If someone likes the bear and the bear is green then they see the lion. If someone eats the rabbit and the rabbit likes the bear then they see the bear. If someone likes the bear and they are cold then the bear is cold. If someone likes the lion and they are young then the lion likes the bear. If someone sees the bear then they eat the rabbit. If someone likes the rabbit and they are cold then they eat the bear. If someone is cold then they like the bear. If someone sees the rabbit then they eat the bear.
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear likes the lion.
("bear" "likes" "lion" "+")
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is round.
("lion" "is" "round" "+")
The lion is young.
("lion" "is" "young" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If someone likes the bear and the bear is green then they see the lion.
((("someone" "likes" "bear" "+") ("bear" "is" "green" "+")) -> ("someone" "sees" "lion" "+"))
If someone eats the rabbit and the rabbit likes the bear then they see the bear.
((("someone" "eats" "rabbit" "+") ("rabbit" "likes" "bear" "+")) -> ("someone" "sees" "bear" "+"))
If someone likes the bear and they are cold then the bear is cold.
((("someone" "likes" "bear" "+") ("someone" "is" "cold" "+")) -> ("bear" "is" "cold" "+"))
If someone likes the lion and they are young then the lion likes the bear.
((("someone" "likes" "lion" "+") ("someone" "is" "young" "+")) -> ("lion" "likes" "bear" "+"))
If someone sees the bear then they eat the rabbit.
((("someone" "sees" "bear" "+")) -> ("someone" "eats" "rabbit" "+"))
If someone likes the rabbit and they are cold then they eat the bear.
((("someone" "likes" "rabbit" "+") ("someone" "is" "cold" "+")) -> ("someone" "eats" "bear" "+"))
If someone is cold then they like the bear.
((("someone" "is" "cold" "+")) -> ("someone" "likes" "bear" "+"))
If someone sees the rabbit then they eat the bear.
((("someone" "sees" "rabbit" "+")) -> ("someone" "eats" "bear" "+"))
The rabbit eats the lion.
True
1
proof
[(triple11)]
("rabbit" "eats" "lion" "+")
triple11
The rabbit does not see the lion.
False
1
inv-proof
[(triple16)]
("rabbit" "sees" "lion" "-")
triple16
The rabbit likes the bear.
True
2
proof
[(((triple12) -> rule7))]
("rabbit" "likes" "bear" "+")
((triple12) -> (rule7 % int1))
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int1
The lion does not like the bear.
False
2
inv-proof
[(((triple6) -> rule7))]
("lion" "likes" "bear" "-")
((triple6) -> (rule7 % int1))
The lion likes the bear.
("lion" "likes" "bear" "+")
int1
The bear sees the bear.
True
4
proof
[(((triple1 ((triple12) -> rule7)) -> rule2))]
("bear" "sees" "bear" "+")
((triple1 ((triple12) -> (rule7 % int2))) -> (rule2 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int2
The bear is not cold.
False
4
inv-proof
[(((((triple12) -> rule7) triple12) -> rule3) OR ((((triple6) -> rule7) triple6) -> rule3))]
("bear" "is" "cold" "-")
((((triple12) -> (rule7 % int2)) triple12) -> (rule3 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int2
((((triple6) -> (rule7 % int2)) triple6) -> (rule3 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
The bear likes the bear.
True
5
proof
[(((((((triple12) -> rule7) triple12) -> rule3)) -> rule7) OR ((((((triple6) -> rule7) triple6) -> rule3)) -> rule7))]
("bear" "likes" "bear" "+")
((((((triple12) -> (rule7 % int3)) triple12) -> (rule3 % int2))) -> (rule7 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int3
((((((triple6) -> (rule7 % int3)) triple6) -> (rule3 % int2))) -> (rule7 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The lion likes the bear.
("lion" "likes" "bear" "+")
int3
The bear does not like the bear.
False
5
inv-proof
[(((((((triple12) -> rule7) triple12) -> rule3)) -> rule7) OR ((((((triple6) -> rule7) triple6) -> rule3)) -> rule7))]
("bear" "likes" "bear" "-")
((((((triple12) -> (rule7 % int3)) triple12) -> (rule3 % int2))) -> (rule7 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int3
((((((triple6) -> (rule7 % int3)) triple6) -> (rule3 % int2))) -> (rule7 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The lion likes the bear.
("lion" "likes" "bear" "+")
int3
The lion does not eat the bear.
Unknown
inv-rconc
[@1: The lion eats the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "eats" "bear" "-")
The bear sees the lion.
Unknown
rconc
[@1: The bear sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "sees" "lion" "+")
The lion does not see the lion.
Unknown
inv-rconc
[@1: The lion sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "sees" "lion" "-")
The rabbit eats the bear.
Unknown
rconc
[@1: The rabbit eats the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "eats" "bear" "+")
The lion does not like the rabbit.
Unknown
inv-random
[@0: The lion likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "rabbit" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
The bear does not eat the lion.
Unknown
inv-random
[@0: The bear eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "lion" "-")
The lion sees the rabbit.
Unknown
random
[@0: The lion sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "rabbit" "+")
@0: The bear eats the rabbit.[(triple1)] The bear is rough.[(triple2)] The bear likes the lion.[(triple3)] The bear likes the rabbit.[(triple4)] The lion eats the rabbit.[(triple5 OR ((triple10) -> rule5))] The lion is cold.[(triple6)] The lion is rough.[(triple7)] The lion is round.[(triple8)] The lion is young.[(triple9)] The lion sees the bear.[(triple10 OR ((triple5 ((triple12) -> rule7)) -> rule2))] The rabbit eats the lion.[(triple11)] The rabbit is cold.[(triple12)] The rabbit is green.[(triple13)] The rabbit is young.[(triple14)] The rabbit sees the bear.[(triple15)] The rabbit sees the lion.[(triple16)] @1: The lion likes the bear.[(((triple6) -> rule7))] The rabbit eats the rabbit.[(((triple15) -> rule5))] The rabbit likes the bear.[(((triple12) -> rule7))] @2: The bear is cold.[(((((triple12) -> rule7) triple12) -> rule3) OR ((((triple6) -> rule7) triple6) -> rule3))] The bear sees the bear.[(((triple1 ((triple12) -> rule7)) -> rule2))] @3: The bear eats the bear.[(((triple4 ((((triple12) -> rule7) triple12) -> rule3)) -> rule6) OR ((triple4 ((((triple6) -> rule7) triple6) -> rule3)) -> rule6))] The bear likes the bear.[(((((((triple12) -> rule7) triple12) -> rule3)) -> rule7) OR ((((((triple6) -> rule7) triple6) -> rule3)) -> rule7))]
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
triple1
The bear is rough.
("bear" "is" "rough" "+")
triple2
The bear likes the lion.
("bear" "likes" "lion" "+")
triple3
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple4
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple5
((triple10) -> (rule5 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
triple6
The lion is rough.
("lion" "is" "rough" "+")
triple7
The lion is round.
("lion" "is" "round" "+")
triple8
The lion is young.
("lion" "is" "young" "+")
triple9
The lion sees the bear.
("lion" "sees" "bear" "+")
triple10
((triple5 ((triple12) -> (rule7 % int2))) -> (rule2 % int1))
The lion sees the bear.
("lion" "sees" "bear" "+")
int1
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int2
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple11
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple12
The rabbit is green.
("rabbit" "is" "green" "+")
triple13
The rabbit is young.
("rabbit" "is" "young" "+")
triple14
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
triple15
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple16
The lion likes the bear.
("lion" "likes" "bear" "+")
((triple6) -> (rule7 % int1))
The lion likes the bear.
("lion" "likes" "bear" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((triple15) -> (rule5 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
((triple12) -> (rule7 % int1))
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
((((triple12) -> (rule7 % int2)) triple12) -> (rule3 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int2
((((triple6) -> (rule7 % int2)) triple6) -> (rule3 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The lion likes the bear.
("lion" "likes" "bear" "+")
int2
The bear sees the bear.
("bear" "sees" "bear" "+")
((triple1 ((triple12) -> (rule7 % int2))) -> (rule2 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int2
The bear eats the bear.
("bear" "eats" "bear" "+")
((triple4 ((((triple12) -> (rule7 % int3)) triple12) -> (rule3 % int2))) -> (rule6 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int3
((triple4 ((((triple6) -> (rule7 % int3)) triple6) -> (rule3 % int2))) -> (rule6 % int1))
The bear eats the bear.
("bear" "eats" "bear" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The lion likes the bear.
("lion" "likes" "bear" "+")
int3
The bear likes the bear.
("bear" "likes" "bear" "+")
((((((triple12) -> (rule7 % int3)) triple12) -> (rule3 % int2))) -> (rule7 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
int3
((((((triple6) -> (rule7 % int3)) triple6) -> (rule3 % int2))) -> (rule7 % int1))
The bear likes the bear.
("bear" "likes" "bear" "+")
int1
The bear is cold.
("bear" "is" "cold" "+")
int2
The lion likes the bear.
("lion" "likes" "bear" "+")
int3