The cow sees the lion. The lion sees the cow. If someone sees the lion and the lion sees the cow then they are not green. If someone sees the lion and the lion is cold then the lion does not visit the cow. If someone visits the lion then they do not visit the cow. If someone is nice and they see the cow then the cow does not see the lion. If someone sees the lion and the lion does not see the cow then they need the cow. If someone needs the lion then the lion is not cold. If someone needs the cow then they visit the lion. If someone needs the lion then they see the lion.
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
If someone sees the lion and the lion sees the cow then they are not green.
((("someone" "sees" "lion" "+") ("lion" "sees" "cow" "+")) -> ("someone" "is" "green" "-"))
If someone sees the lion and the lion is cold then the lion does not visit the cow.
((("someone" "sees" "lion" "+") ("lion" "is" "cold" "+")) -> ("lion" "visits" "cow" "-"))
If someone visits the lion then they do not visit the cow.
((("someone" "visits" "lion" "+")) -> ("someone" "visits" "cow" "-"))
If someone is nice and they see the cow then the cow does not see the lion.
((("someone" "is" "nice" "+") ("someone" "sees" "cow" "+")) -> ("cow" "sees" "lion" "-"))
If someone sees the lion and the lion does not see the cow then they need the cow.
((("someone" "sees" "lion" "+") ("lion" "sees" "cow" "~")) -> ("someone" "needs" "cow" "+"))
If someone needs the lion then the lion is not cold.
((("someone" "needs" "lion" "+")) -> ("lion" "is" "cold" "-"))
If someone needs the cow then they visit the lion.
((("someone" "needs" "cow" "+")) -> ("someone" "visits" "lion" "+"))
If someone needs the lion then they see the lion.
((("someone" "needs" "lion" "+")) -> ("someone" "sees" "lion" "+"))
The cow sees the lion.
True
1
proof
[(triple1)]
("cow" "sees" "lion" "+")
triple1
The lion does not see the cow.
False
1
inv-proof
[(triple2)]
("lion" "sees" "cow" "-")
triple2
The cow is not green.
True
3
proof
[(((triple1 triple2) -> rule1))]
("cow" "is" "green" "-")
((triple1 triple2) -> (rule1 % int1))
The cow is not green.
("cow" "is" "green" "-")
int1
The cow is green.
False
3
inv-proof
[(((triple1 triple2) -> rule1))]
("cow" "is" "green" "+")
((triple1 triple2) -> (rule1 % int1))
The cow is not green.
("cow" "is" "green" "-")
int1
The cow does not visit the lion.
Unknown
inv-rconc
[@2: The cow visits the lion.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("cow" "visits" "lion" "-")
The cow needs the cow.
Unknown
rconc
[@1: The cow needs the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "needs" "cow" "+")
The cow is not nice.
Unknown
inv-random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "-")
The cow is blue.
Unknown
random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "+")
@0: The cow sees the lion.[(triple1)] The lion sees the cow.[(triple2)] @1: The cow is not green.[(((triple1 triple2) -> rule1))]
The cow sees the lion.
("cow" "sees" "lion" "+")
triple1
The lion sees the cow.
("lion" "sees" "cow" "+")
triple2
The cow is not green.
("cow" "is" "green" "-")
((triple1 triple2) -> (rule1 % int1))
The cow is not green.
("cow" "is" "green" "-")
int1