The cow sees the lion. The lion is rough. If someone is cold and they need the cow then the cow sees the lion. If someone is red and kind then they need the lion. If someone sees the lion then they are kind. If someone needs the lion then the lion eats the cow. If someone eats the lion and they see the cow then the cow eats the lion. If someone needs the lion and the lion sees the cow then they see the cow. If someone needs the lion then they are big. If someone needs the lion then they are big.
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion is rough.
("lion" "is" "rough" "+")
If someone is cold and they need the cow then the cow sees the lion.
((("someone" "is" "cold" "+") ("someone" "needs" "cow" "+")) -> ("cow" "sees" "lion" "+"))
If someone is red and kind then they need the lion.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "needs" "lion" "+"))
If someone sees the lion then they are kind.
((("someone" "sees" "lion" "+")) -> ("someone" "is" "kind" "+"))
If someone needs the lion then the lion eats the cow.
((("someone" "needs" "lion" "+")) -> ("lion" "eats" "cow" "+"))
If someone eats the lion and they see the cow then the cow eats the lion.
((("someone" "eats" "lion" "+") ("someone" "sees" "cow" "+")) -> ("cow" "eats" "lion" "+"))
If someone needs the lion and the lion sees the cow then they see the cow.
((("someone" "needs" "lion" "+") ("lion" "sees" "cow" "+")) -> ("someone" "sees" "cow" "+"))
If someone needs the lion then they are big.
((("someone" "needs" "lion" "+")) -> ("someone" "is" "big" "+"))
If someone needs the lion then they are big.
((("someone" "needs" "lion" "+")) -> ("someone" "is" "big" "+"))
The lion is rough.
True
1
proof
[(triple2)]
("lion" "is" "rough" "+")
triple2
The lion is not rough.
False
1
inv-proof
[(triple2)]
("lion" "is" "rough" "-")
triple2
The cow is kind.
True
2
proof
[(((triple1) -> rule3))]
("cow" "is" "kind" "+")
((triple1) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow is not kind.
False
2
inv-proof
[(((triple1) -> rule3))]
("cow" "is" "kind" "-")
((triple1) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The lion is not big.
Unknown
inv-rconc
[@2: The lion is big.[CWA. Example of deepest failure = (rule7 <- rule2 <- FAIL)]]
("lion" "is" "big" "-")
The lion sees the cow.
Unknown
rconc
[@1: The lion sees the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "sees" "cow" "+")
The cow is not rough.
Unknown
inv-random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The cow sees the lion.[(triple1)] The lion is rough.[(triple2)] @1: The cow is kind.[(((triple1) -> rule3))]
The cow sees the lion.
("cow" "sees" "lion" "+")
triple1
The lion is rough.
("lion" "is" "rough" "+")
triple2
The cow is kind.
("cow" "is" "kind" "+")
((triple1) -> (rule3 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1