The bear eats the lion. The bear is round. The bear visits the mouse. The bear visits the rabbit. The lion needs the bear. The mouse needs the bear. The mouse needs the lion. The mouse visits the bear. The mouse visits the lion. The rabbit eats the bear. If someone needs the mouse then they visit the rabbit. If someone needs the bear then the bear needs the rabbit. If someone eats the lion then the lion eats the bear. If someone is rough and they visit the bear then they are kind. If someone needs the lion then the lion needs the mouse. If someone eats the bear and they visit the rabbit then they visit the mouse.
The bear eats the lion.
("bear" "eats" "lion" "+")
The bear is round.
("bear" "is" "round" "+")
The bear visits the mouse.
("bear" "visits" "mouse" "+")
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The mouse needs the bear.
("mouse" "needs" "bear" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
If someone needs the mouse then they visit the rabbit.
((("someone" "needs" "mouse" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone needs the bear then the bear needs the rabbit.
((("someone" "needs" "bear" "+")) -> ("bear" "needs" "rabbit" "+"))
If someone eats the lion then the lion eats the bear.
((("someone" "eats" "lion" "+")) -> ("lion" "eats" "bear" "+"))
If someone is rough and they visit the bear then they are kind.
((("someone" "is" "rough" "+") ("someone" "visits" "bear" "+")) -> ("someone" "is" "kind" "+"))
If someone needs the lion then the lion needs the mouse.
((("someone" "needs" "lion" "+")) -> ("lion" "needs" "mouse" "+"))
If someone eats the bear and they visit the rabbit then they visit the mouse.
((("someone" "eats" "bear" "+") ("someone" "visits" "rabbit" "+")) -> ("someone" "visits" "mouse" "+"))
The bear is round.
True
1
proof
[(triple2)]
("bear" "is" "round" "+")
triple2
The mouse does not visit the bear.
False
1
inv-proof
[(triple8)]
("mouse" "visits" "bear" "-")
triple8
The lion needs the mouse.
True
2
proof
[(((triple7) -> rule5))]
("lion" "needs" "mouse" "+")
((triple7) -> (rule5 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The bear does not need the rabbit.
False
2
inv-proof
[(((triple5) -> rule2) OR ((triple6) -> rule2))]
("bear" "needs" "rabbit" "-")
((triple5) -> (rule2 % int1))
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int1
((triple6) -> (rule2 % int1))
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int1
The lion visits the rabbit.
True
3
proof
[(((((triple7) -> rule5)) -> rule1))]
("lion" "visits" "rabbit" "+")
((((triple7) -> (rule5 % int2))) -> (rule1 % int1))
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int2
The lion does not visit the rabbit.
False
3
inv-proof
[(((((triple7) -> rule5)) -> rule1))]
("lion" "visits" "rabbit" "-")
((((triple7) -> (rule5 % int2))) -> (rule1 % int1))
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int2
The rabbit does not visit the rabbit.
Unknown
inv-rconc
[@1: The rabbit visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "visits" "rabbit" "-")
The mouse visits the rabbit.
Unknown
rconc
[@1: The mouse visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "visits" "rabbit" "+")
The rabbit is not kind.
Unknown
inv-rconc
[@1: The rabbit is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "is" "kind" "-")
The bear is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
The mouse does not eat the bear.
Unknown
inv-random
[@0: The mouse eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "bear" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
@0: The bear eats the lion.[(triple1)] The bear is round.[(triple2)] The bear visits the mouse.[(triple3)] The bear visits the rabbit.[(triple4)] The lion needs the bear.[(triple5)] The mouse needs the bear.[(triple6)] The mouse needs the lion.[(triple7)] The mouse visits the bear.[(triple8)] The mouse visits the lion.[(triple9)] The rabbit eats the bear.[(triple10)] @1: The bear needs the rabbit.[(((triple5) -> rule2) OR ((triple6) -> rule2))] The lion eats the bear.[(((triple1) -> rule3))] The lion needs the mouse.[(((triple7) -> rule5))] @2: The lion visits the rabbit.[(((((triple7) -> rule5)) -> rule1))] @3: The lion visits the mouse.[(((((triple1) -> rule3) ((((triple7) -> rule5)) -> rule1)) -> rule6))]
The bear eats the lion.
("bear" "eats" "lion" "+")
triple1
The bear is round.
("bear" "is" "round" "+")
triple2
The bear visits the mouse.
("bear" "visits" "mouse" "+")
triple3
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple4
The lion needs the bear.
("lion" "needs" "bear" "+")
triple5
The mouse needs the bear.
("mouse" "needs" "bear" "+")
triple6
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple7
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple8
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple9
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
triple10
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
((triple5) -> (rule2 % int1))
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int1
((triple6) -> (rule2 % int1))
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
int1
The lion eats the bear.
("lion" "eats" "bear" "+")
((triple1) -> (rule3 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
((triple7) -> (rule5 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
((((triple7) -> (rule5 % int2))) -> (rule1 % int1))
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int1
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int2
The lion visits the mouse.
("lion" "visits" "mouse" "+")
((((triple1) -> (rule3 % int4)) ((((triple7) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int2
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int3
The lion eats the bear.
("lion" "eats" "bear" "+")
int4