The bear visits the lion. The cow sees the lion. The lion visits the cow. If someone is red and they visit the bear then the bear is rough. If someone sees the lion then they eat the lion. If someone eats the lion then they are round. If someone is red and they eat the lion then the lion visits the cow. If someone eats the lion and they are red then the lion is rough. If someone is red and they see the bear then the bear is blue. If someone visits the bear then the bear visits the lion. If someone visits the cow and the cow eats the lion then the cow visits the bear.
The bear visits the lion.
("bear" "visits" "lion" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
If someone is red and they visit the bear then the bear is rough.
((("someone" "is" "red" "+") ("someone" "visits" "bear" "+")) -> ("bear" "is" "rough" "+"))
If someone sees the lion then they eat the lion.
((("someone" "sees" "lion" "+")) -> ("someone" "eats" "lion" "+"))
If someone eats the lion then they are round.
((("someone" "eats" "lion" "+")) -> ("someone" "is" "round" "+"))
If someone is red and they eat the lion then the lion visits the cow.
((("someone" "is" "red" "+") ("someone" "eats" "lion" "+")) -> ("lion" "visits" "cow" "+"))
If someone eats the lion and they are red then the lion is rough.
((("someone" "eats" "lion" "+") ("someone" "is" "red" "+")) -> ("lion" "is" "rough" "+"))
If someone is red and they see the bear then the bear is blue.
((("someone" "is" "red" "+") ("someone" "sees" "bear" "+")) -> ("bear" "is" "blue" "+"))
If someone visits the bear then the bear visits the lion.
((("someone" "visits" "bear" "+")) -> ("bear" "visits" "lion" "+"))
If someone visits the cow and the cow eats the lion then the cow visits the bear.
((("someone" "visits" "cow" "+") ("cow" "eats" "lion" "+")) -> ("cow" "visits" "bear" "+"))
The bear visits the lion.
True
1
proof
[(triple1 OR ((((triple3 ((triple2) -> rule2)) -> rule8)) -> rule7))]
("bear" "visits" "lion" "+")
triple1
((((triple3 ((triple2) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The cow visits the bear.
("cow" "visits" "bear" "+")
int2
The cow eats the lion.
("cow" "eats" "lion" "+")
int3
The lion does not visit the cow.
False
1
inv-proof
[(triple3)]
("lion" "visits" "cow" "-")
triple3
The cow eats the lion.
True
2
proof
[(((triple2) -> rule2))]
("cow" "eats" "lion" "+")
((triple2) -> (rule2 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The cow does not eat the lion.
False
2
inv-proof
[(((triple2) -> rule2))]
("cow" "eats" "lion" "-")
((triple2) -> (rule2 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The cow visits the bear.
True
4
proof
[(((triple3 ((triple2) -> rule2)) -> rule8))]
("cow" "visits" "bear" "+")
((triple3 ((triple2) -> (rule2 % int2))) -> (rule8 % int1))
The cow visits the bear.
("cow" "visits" "bear" "+")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
int2
The cow is not round.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule3))]
("cow" "is" "round" "-")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
int2
The bear does not eat the lion.
Unknown
inv-rconc
[@1: The bear eats the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "eats" "lion" "-")
The lion is round.
Unknown
rconc
[@2: The lion is round.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("lion" "is" "round" "+")
The lion is not rough.
Unknown
inv-rconc
[@1: The lion is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "is" "rough" "-")
The lion is kind.
Unknown
random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The cow sees the bear.
Unknown
random
[@0: The cow sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "bear" "+")
@0: The bear visits the lion.[(triple1 OR ((((triple3 ((triple2) -> rule2)) -> rule8)) -> rule7))] The cow sees the lion.[(triple2)] The lion visits the cow.[(triple3)] @1: The cow eats the lion.[(((triple2) -> rule2))] @2: The cow is round.[(((((triple2) -> rule2)) -> rule3))] The cow visits the bear.[(((triple3 ((triple2) -> rule2)) -> rule8))]
The bear visits the lion.
("bear" "visits" "lion" "+")
triple1
((((triple3 ((triple2) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The cow visits the bear.
("cow" "visits" "bear" "+")
int2
The cow eats the lion.
("cow" "eats" "lion" "+")
int3
The cow sees the lion.
("cow" "sees" "lion" "+")
triple2
The lion visits the cow.
("lion" "visits" "cow" "+")
triple3
The cow eats the lion.
("cow" "eats" "lion" "+")
((triple2) -> (rule2 % int1))
The cow eats the lion.
("cow" "eats" "lion" "+")
int1
The cow is round.
("cow" "is" "round" "+")
((((triple2) -> (rule2 % int2))) -> (rule3 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
int2
The cow visits the bear.
("cow" "visits" "bear" "+")
((triple3 ((triple2) -> (rule2 % int2))) -> (rule8 % int1))
The cow visits the bear.
("cow" "visits" "bear" "+")
int1
The cow eats the lion.
("cow" "eats" "lion" "+")
int2