The cow chases the lion. The cow is blue. The cow is nice. The lion does not chase the cow. The lion eats the cow. The lion is blue. The lion is not green. The lion is nice. The lion is red. The lion sees the cow. If something eats the cow then it is blue. If something sees the cow and it chases the lion then it is not blue. If something eats the lion then the lion is rough. All rough things are green. If something is rough and not green then it sees the lion. If the cow is nice and the cow does not see the lion then the lion chases the cow.
The cow chases the lion.
("cow" "chases" "lion" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is nice.
("cow" "is" "nice" "+")
The lion does not chase the cow.
("lion" "chases" "cow" "-")
The lion eats the cow.
("lion" "eats" "cow" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is not green.
("lion" "is" "green" "-")
The lion is nice.
("lion" "is" "nice" "+")
The lion is red.
("lion" "is" "red" "+")
The lion sees the cow.
("lion" "sees" "cow" "+")
If something eats the cow then it is blue.
((("something" "eats" "cow" "+")) -> ("something" "is" "blue" "+"))
If something sees the cow and it chases the lion then it is not blue.
((("something" "sees" "cow" "+") ("something" "chases" "lion" "+")) -> ("something" "is" "blue" "-"))
If something eats the lion then the lion is rough.
((("something" "eats" "lion" "+")) -> ("lion" "is" "rough" "+"))
All rough things are green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
If something is rough and not green then it sees the lion.
((("something" "is" "rough" "+") ("something" "is" "green" "~")) -> ("something" "sees" "lion" "+"))
If the cow is nice and the cow does not see the lion then the lion chases the cow.
((("cow" "is" "nice" "+") ("cow" "sees" "lion" "~")) -> ("lion" "chases" "cow" "+"))
The lion does not chase the cow.
True
1
proof
[(triple4)]
("lion" "chases" "cow" "-")
triple4
The cow is not blue.
False
1
inv-proof
[(triple2)]
("cow" "is" "blue" "-")
triple2
The lion is not rough.
Unknown
inv-rconc
[@1: The lion is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "rough" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
@0: The cow chases the lion.[(triple1)] The cow is blue.[(triple2)] The cow is nice.[(triple3)] The lion does not chase the cow.[(triple4)] The lion eats the cow.[(triple5)] The lion is blue.[(triple6 OR ((triple5) -> rule1))] The lion is nice.[(triple8)] The lion is not green.[(triple7)] The lion is red.[(triple9)] The lion sees the cow.[(triple10)]
The cow chases the lion.
("cow" "chases" "lion" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The cow is nice.
("cow" "is" "nice" "+")
triple3
The lion does not chase the cow.
("lion" "chases" "cow" "-")
triple4
The lion eats the cow.
("lion" "eats" "cow" "+")
triple5
The lion is blue.
("lion" "is" "blue" "+")
triple6
((triple5) -> (rule1 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
triple8
The lion is not green.
("lion" "is" "green" "-")
triple7
The lion is red.
("lion" "is" "red" "+")
triple9
The lion sees the cow.
("lion" "sees" "cow" "+")
triple10