The cow eats the lion. The lion likes the cow. If something chases the lion then the lion likes the cow. If the cow chases the lion then the cow likes the lion. If something eats the cow then it is nice. If something eats the lion and the lion likes the cow then the lion eats the cow. If the cow is nice then the cow is kind. If something likes the cow and the cow is kind then the cow is cold.
The cow eats the lion.
("cow" "eats" "lion" "+")
The lion likes the cow.
("lion" "likes" "cow" "+")
If something chases the lion then the lion likes the cow.
((("something" "chases" "lion" "+")) -> ("lion" "likes" "cow" "+"))
If the cow chases the lion then the cow likes the lion.
((("cow" "chases" "lion" "+")) -> ("cow" "likes" "lion" "+"))
If something eats the cow then it is nice.
((("something" "eats" "cow" "+")) -> ("something" "is" "nice" "+"))
If something eats the lion and the lion likes the cow then the lion eats the cow.
((("something" "eats" "lion" "+") ("lion" "likes" "cow" "+")) -> ("lion" "eats" "cow" "+"))
If the cow is nice then the cow is kind.
((("cow" "is" "nice" "+")) -> ("cow" "is" "kind" "+"))
If something likes the cow and the cow is kind then the cow is cold.
((("something" "likes" "cow" "+") ("cow" "is" "kind" "+")) -> ("cow" "is" "cold" "+"))
The lion likes the cow.
True
1
proof
[(triple2)]
("lion" "likes" "cow" "+")
triple2
The cow does not eat the lion.
False
1
inv-proof
[(triple1)]
("cow" "eats" "lion" "-")
triple1
The lion eats the cow.
True
3
proof
[(((triple1 triple2) -> rule4))]
("lion" "eats" "cow" "+")
((triple1 triple2) -> (rule4 % int1))
The lion eats the cow.
("lion" "eats" "cow" "+")
int1
The lion does not eat the cow.
False
3
inv-proof
[(((triple1 triple2) -> rule4))]
("lion" "eats" "cow" "-")
((triple1 triple2) -> (rule4 % int1))
The lion eats the cow.
("lion" "eats" "cow" "+")
int1
The lion is nice.
True
4
proof
[(((((triple1 triple2) -> rule4)) -> rule3))]
("lion" "is" "nice" "+")
((((triple1 triple2) -> (rule4 % int2))) -> (rule3 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
int2
The lion is not nice.
False
4
inv-proof
[(((((triple1 triple2) -> rule4)) -> rule3))]
("lion" "is" "nice" "-")
((((triple1 triple2) -> (rule4 % int2))) -> (rule3 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
int2
The cow does not like the lion.
Unknown
inv-rconc
[@1: The cow likes the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "likes" "lion" "-")
The cow is nice.
Unknown
rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "nice" "+")
The cow is not cold.
Unknown
inv-rconc
[@3: The cow is cold.[CWA. Example of deepest failure = (rule6 <- rule5 <- rule3 <- FAIL)]]
("cow" "is" "cold" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
The cow does not like the cow.
Unknown
inv-random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
@0: The cow eats the lion.[(triple1)] The lion likes the cow.[(triple2)] @1: The lion eats the cow.[(((triple1 triple2) -> rule4))] @2: The lion is nice.[(((((triple1 triple2) -> rule4)) -> rule3))]
The cow eats the lion.
("cow" "eats" "lion" "+")
triple1
The lion likes the cow.
("lion" "likes" "cow" "+")
triple2
The lion eats the cow.
("lion" "eats" "cow" "+")
((triple1 triple2) -> (rule4 % int1))
The lion eats the cow.
("lion" "eats" "cow" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
((((triple1 triple2) -> (rule4 % int2))) -> (rule3 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion eats the cow.
("lion" "eats" "cow" "+")
int2