The cow eats the lion. The lion is red. The mouse is green. If someone likes the cow and they do not eat the cow then they do not visit the lion. If someone eats the mouse then the mouse is big. If someone is big then they like the cow. If someone eats the cow then they visit the cow. If someone is red then they eat the mouse. If someone is young and they eat the cow then they like the mouse. If someone eats the cow and the cow visits the mouse then the mouse visits the lion. If someone visits the cow and they are not big then they do not visit the mouse.
The cow eats the lion.
("cow" "eats" "lion" "+")
The lion is red.
("lion" "is" "red" "+")
The mouse is green.
("mouse" "is" "green" "+")
If someone likes the cow and they do not eat the cow then they do not visit the lion.
((("someone" "likes" "cow" "+") ("someone" "eats" "cow" "~")) -> ("someone" "visits" "lion" "-"))
If someone eats the mouse then the mouse is big.
((("someone" "eats" "mouse" "+")) -> ("mouse" "is" "big" "+"))
If someone is big then they like the cow.
((("someone" "is" "big" "+")) -> ("someone" "likes" "cow" "+"))
If someone eats the cow then they visit the cow.
((("someone" "eats" "cow" "+")) -> ("someone" "visits" "cow" "+"))
If someone is red then they eat the mouse.
((("someone" "is" "red" "+")) -> ("someone" "eats" "mouse" "+"))
If someone is young and they eat the cow then they like the mouse.
((("someone" "is" "young" "+") ("someone" "eats" "cow" "+")) -> ("someone" "likes" "mouse" "+"))
If someone eats the cow and the cow visits the mouse then the mouse visits the lion.
((("someone" "eats" "cow" "+") ("cow" "visits" "mouse" "+")) -> ("mouse" "visits" "lion" "+"))
If someone visits the cow and they are not big then they do not visit the mouse.
((("someone" "visits" "cow" "+") ("someone" "is" "big" "~")) -> ("someone" "visits" "mouse" "-"))
The cow eats the lion.
True
1
proof
[(triple1)]
("cow" "eats" "lion" "+")
triple1
The mouse is not green.
False
1
inv-proof
[(triple3)]
("mouse" "is" "green" "-")
triple3
The lion eats the mouse.
True
2
proof
[(((triple2) -> rule5))]
("lion" "eats" "mouse" "+")
((triple2) -> (rule5 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The lion does not eat the mouse.
False
2
inv-proof
[(((triple2) -> rule5))]
("lion" "eats" "mouse" "-")
((triple2) -> (rule5 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The mouse is big.
True
3
proof
[(((((triple2) -> rule5)) -> rule2))]
("mouse" "is" "big" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int2
The mouse is not big.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule2))]
("mouse" "is" "big" "-")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int2
The mouse likes the cow.
True
4
proof
[(((((((triple2) -> rule5)) -> rule2)) -> rule3))]
("mouse" "likes" "cow" "+")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int3
The mouse does not like the cow.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule2)) -> rule3))]
("mouse" "likes" "cow" "-")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int3
The cow does not eat the mouse.
Unknown
inv-rconc
[@1: The cow eats the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "eats" "mouse" "-")
The mouse visits the cow.
Unknown
rconc
[@1: The mouse visits the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "visits" "cow" "+")
The lion does not like the mouse.
Unknown
inv-rconc
[@1: The lion likes the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "likes" "mouse" "-")
The cow likes the mouse.
Unknown
rconc
[@1: The cow likes the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "likes" "mouse" "+")
The lion is not green.
Unknown
inv-random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "-")
The lion is big.
Unknown
random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "+")
The cow is not young.
Unknown
inv-random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
@0: The cow eats the lion.[(triple1)] The lion is red.[(triple2)] The mouse is green.[(triple3)] @1: The lion eats the mouse.[(((triple2) -> rule5))] @2: The mouse is big.[(((((triple2) -> rule5)) -> rule2))] @3: The mouse likes the cow.[(((((((triple2) -> rule5)) -> rule2)) -> rule3))]
The cow eats the lion.
("cow" "eats" "lion" "+")
triple1
The lion is red.
("lion" "is" "red" "+")
triple2
The mouse is green.
("mouse" "is" "green" "+")
triple3
The lion eats the mouse.
("lion" "eats" "mouse" "+")
((triple2) -> (rule5 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int2
The mouse likes the cow.
("mouse" "likes" "cow" "+")
((((((triple2) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int3