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