The bear likes the rabbit. The bear visits the rabbit. The lion likes the rabbit. The lion needs the rabbit. The rabbit is rough. The rabbit likes the bear. The rabbit needs the lion. If something needs the rabbit and the rabbit needs the bear then it likes the lion. If something needs the rabbit and it likes the rabbit then it is round. If something likes the lion then it visits the bear. If something visits the lion then the lion visits the bear. If something visits the bear then the bear visits the lion. If something visits the lion and it visits the bear then the lion needs the bear. If something likes the bear and it visits the bear then it is big. If something likes the rabbit then it visits the bear.
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
If something needs the rabbit and the rabbit needs the bear then it likes the lion.
((("something" "needs" "rabbit" "+") ("rabbit" "needs" "bear" "+")) -> ("something" "likes" "lion" "+"))
If something needs the rabbit and it likes the rabbit then it is round.
((("something" "needs" "rabbit" "+") ("something" "likes" "rabbit" "+")) -> ("something" "is" "round" "+"))
If something likes the lion then it visits the bear.
((("something" "likes" "lion" "+")) -> ("something" "visits" "bear" "+"))
If something visits the lion then the lion visits the bear.
((("something" "visits" "lion" "+")) -> ("lion" "visits" "bear" "+"))
If something visits the bear then the bear visits the lion.
((("something" "visits" "bear" "+")) -> ("bear" "visits" "lion" "+"))
If something visits the lion and it visits the bear then the lion needs the bear.
((("something" "visits" "lion" "+") ("something" "visits" "bear" "+")) -> ("lion" "needs" "bear" "+"))
If something likes the bear and it visits the bear then it is big.
((("something" "likes" "bear" "+") ("something" "visits" "bear" "+")) -> ("something" "is" "big" "+"))
If something likes the rabbit then it visits the bear.
((("something" "likes" "rabbit" "+")) -> ("something" "visits" "bear" "+"))
The rabbit needs the lion.
True
1
proof
[(triple7)]
("rabbit" "needs" "lion" "+")
triple7
The bear does not like the rabbit.
False
1
inv-proof
[(triple1)]
("bear" "likes" "rabbit" "-")
triple1
The lion is round.
True
3
proof
[(((triple4 triple3) -> rule2))]
("lion" "is" "round" "+")
((triple4 triple3) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is not round.
False
3
inv-proof
[(((triple4 triple3) -> rule2))]
("lion" "is" "round" "-")
((triple4 triple3) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The bear visits the lion.
True
3
proof
[(((((triple1) -> rule8)) -> rule5) OR ((((triple3) -> rule8)) -> rule5))]
("bear" "visits" "lion" "+")
((((triple1) -> (rule8 % int2))) -> (rule5 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
((((triple3) -> (rule8 % int2))) -> (rule5 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The lion visits the bear.
("lion" "visits" "bear" "+")
int2
The bear does not visit the lion.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule5) OR ((((triple3) -> rule8)) -> rule5))]
("bear" "visits" "lion" "-")
((((triple1) -> (rule8 % int2))) -> (rule5 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
((((triple3) -> (rule8 % int2))) -> (rule5 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The lion visits the bear.
("lion" "visits" "bear" "+")
int2
The lion needs the bear.
True
6
proof
[(((((((triple1) -> rule8)) -> rule5) ((triple1) -> rule8)) -> rule6) OR ((((((triple3) -> rule8)) -> rule5) ((triple1) -> rule8)) -> rule6))]
("lion" "needs" "bear" "+")
((((((triple1) -> (rule8 % int3))) -> (rule5 % int2)) ((triple1) -> (rule8 % int3))) -> (rule6 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The bear visits the lion.
("bear" "visits" "lion" "+")
int2
The bear visits the bear.
("bear" "visits" "bear" "+")
int3
((((((triple3) -> (rule8 % int4))) -> (rule5 % int3)) ((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The bear visits the lion.
("bear" "visits" "lion" "+")
int3
The lion visits the bear.
("lion" "visits" "bear" "+")
int4
The lion does not need the bear.
False
6
inv-proof
[(((((((triple1) -> rule8)) -> rule5) ((triple1) -> rule8)) -> rule6) OR ((((((triple3) -> rule8)) -> rule5) ((triple1) -> rule8)) -> rule6))]
("lion" "needs" "bear" "-")
((((((triple1) -> (rule8 % int3))) -> (rule5 % int2)) ((triple1) -> (rule8 % int3))) -> (rule6 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The bear visits the lion.
("bear" "visits" "lion" "+")
int2
The bear visits the bear.
("bear" "visits" "bear" "+")
int3
((((((triple3) -> (rule8 % int4))) -> (rule5 % int3)) ((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The bear visits the lion.
("bear" "visits" "lion" "+")
int3
The lion visits the bear.
("lion" "visits" "bear" "+")
int4
The rabbit is not round.
Unknown
inv-rconc
[@1: The rabbit is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "round" "-")
The bear likes the lion.
Unknown
rconc
[@1: The bear likes the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "likes" "lion" "+")
The rabbit does not visit the bear.
Unknown
inv-rconc
[@2: The rabbit visits the bear.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("rabbit" "visits" "bear" "-")
The bear is round.
Unknown
rconc
[@1: The bear is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "is" "round" "+")
The rabbit does not visit the lion.
Unknown
inv-random
[@0: The rabbit visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "lion" "-")
The rabbit is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
The bear does not like the bear.
Unknown
inv-random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "-")
The lion likes the bear.
Unknown
random
[@0: The lion likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "bear" "+")
@0: The bear likes the rabbit.[(triple1)] The bear visits the rabbit.[(triple2)] The lion likes the rabbit.[(triple3)] The lion needs the rabbit.[(triple4)] The rabbit is rough.[(triple5)] The rabbit likes the bear.[(triple6)] The rabbit needs the lion.[(triple7)] @1: The bear visits the bear.[(((triple1) -> rule8))] The lion is round.[(((triple4 triple3) -> rule2))] The lion visits the bear.[(((triple3) -> rule8) OR ((((((triple1) -> rule8)) -> rule5)) -> rule4))] @2: The bear visits the lion.[(((((triple1) -> rule8)) -> rule5) OR ((((triple3) -> rule8)) -> rule5))] @3: The lion needs the bear.[(((((((triple1) -> rule8)) -> rule5) ((triple1) -> rule8)) -> rule6) OR ((((((triple3) -> rule8)) -> rule5) ((triple1) -> rule8)) -> rule6))]
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
triple1
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple2
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple3
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple4
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple5
The rabbit likes the bear.
("rabbit" "likes" "bear" "+")
triple6
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple7
The bear visits the bear.
("bear" "visits" "bear" "+")
((triple1) -> (rule8 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The lion is round.
("lion" "is" "round" "+")
((triple4 triple3) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion visits the bear.
("lion" "visits" "bear" "+")
((triple3) -> (rule8 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
((((((triple1) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The bear visits the lion.
("bear" "visits" "lion" "+")
int2
The bear visits the bear.
("bear" "visits" "bear" "+")
int3
The bear visits the lion.
("bear" "visits" "lion" "+")
((((triple1) -> (rule8 % int2))) -> (rule5 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
((((triple3) -> (rule8 % int2))) -> (rule5 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The lion visits the bear.
("lion" "visits" "bear" "+")
int2
The lion needs the bear.
("lion" "needs" "bear" "+")
((((((triple1) -> (rule8 % int3))) -> (rule5 % int2)) ((triple1) -> (rule8 % int3))) -> (rule6 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The bear visits the lion.
("bear" "visits" "lion" "+")
int2
The bear visits the bear.
("bear" "visits" "bear" "+")
int3
((((((triple3) -> (rule8 % int4))) -> (rule5 % int3)) ((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The bear visits the lion.
("bear" "visits" "lion" "+")
int3
The lion visits the bear.
("lion" "visits" "bear" "+")
int4