The cow needs the lion. The lion sees the cow. If someone sees the cow then the cow sees the lion. If someone chases the lion then the lion sees the cow. If the lion chases the cow and the cow does not see the lion then the cow does not need the lion. If someone is cold and they do not see the lion then they need the cow. If someone needs the cow and they need the lion then the lion does not chase the cow. If someone chases the lion then the lion does not chase the cow.
The cow needs the lion.
("cow" "needs" "lion" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
If someone sees the cow then the cow sees the lion.
((("someone" "sees" "cow" "+")) -> ("cow" "sees" "lion" "+"))
If someone chases the lion then the lion sees the cow.
((("someone" "chases" "lion" "+")) -> ("lion" "sees" "cow" "+"))
If the lion chases the cow and the cow does not see the lion then the cow does not need the lion.
((("lion" "chases" "cow" "+") ("cow" "sees" "lion" "~")) -> ("cow" "needs" "lion" "-"))
If someone is cold and they do not see the lion then they need the cow.
((("someone" "is" "cold" "+") ("someone" "sees" "lion" "~")) -> ("someone" "needs" "cow" "+"))
If someone needs the cow and they need the lion then the lion does not chase the cow.
((("someone" "needs" "cow" "+") ("someone" "needs" "lion" "+")) -> ("lion" "chases" "cow" "-"))
If someone chases the lion then the lion does not chase the cow.
((("someone" "chases" "lion" "+")) -> ("lion" "chases" "cow" "-"))
The lion sees the cow.
True
1
proof
[(triple2)]
("lion" "sees" "cow" "+")
triple2
The lion does not see the cow.
False
1
inv-proof
[(triple2)]
("lion" "sees" "cow" "-")
triple2
The cow sees the lion.
True
2
proof
[(((triple2) -> rule1))]
("cow" "sees" "lion" "+")
((triple2) -> (rule1 % int1))
The cow sees the lion.
("cow" "sees" "lion" "+")
int1
The cow does not see the lion.
False
2
inv-proof
[(((triple2) -> rule1))]
("cow" "sees" "lion" "-")
((triple2) -> (rule1 % int1))
The cow sees the lion.
("cow" "sees" "lion" "+")
int1
The lion does not need the cow.
Unknown
inv-rconc
[@1: The lion needs the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "needs" "cow" "-")
The cow needs the cow.
Unknown
rconc
[@1: The cow needs the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "needs" "cow" "+")
The cow is not red.
Unknown
inv-random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "-")
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 needs the lion.[(triple1)] The lion sees the cow.[(triple2)] @1: The cow sees the lion.[(((triple2) -> rule1))]
The cow needs the lion.
("cow" "needs" "lion" "+")
triple1
The lion sees the cow.
("lion" "sees" "cow" "+")
triple2
The cow sees the lion.
("cow" "sees" "lion" "+")
((triple2) -> (rule1 % int1))
The cow sees the lion.
("cow" "sees" "lion" "+")
int1