The cat is kind. The cow is red. The dog does not eat the lion. The lion does not chase the cow. If something is round and it chases the lion then the lion is not red. If something chases the lion then it is blue. If something is red and it visits the cow then it does not chase the cow. If something chases the dog then the dog visits the lion. If something chases the cat then the cat does not visit the lion. If the cow chases the dog and the cow chases the lion then the cow is nice. If the cat does not visit the dog then the dog chases the cat. If something is red then it is not nice.
The cat is kind.
("cat" "is" "kind" "+")
The cow is red.
("cow" "is" "red" "+")
The dog does not eat the lion.
("dog" "eats" "lion" "-")
The lion does not chase the cow.
("lion" "chases" "cow" "-")
If something is round and it chases the lion then the lion is not red.
((("something" "is" "round" "+") ("something" "chases" "lion" "+")) -> ("lion" "is" "red" "-"))
If something chases the lion then it is blue.
((("something" "chases" "lion" "+")) -> ("something" "is" "blue" "+"))
If something is red and it visits the cow then it does not chase the cow.
((("something" "is" "red" "+") ("something" "visits" "cow" "+")) -> ("something" "chases" "cow" "-"))
If something chases the dog then the dog visits the lion.
((("something" "chases" "dog" "+")) -> ("dog" "visits" "lion" "+"))
If something chases the cat then the cat does not visit the lion.
((("something" "chases" "cat" "+")) -> ("cat" "visits" "lion" "-"))
If the cow chases the dog and the cow chases the lion then the cow is nice.
((("cow" "chases" "dog" "+") ("cow" "chases" "lion" "+")) -> ("cow" "is" "nice" "+"))
If the cat does not visit the dog then the dog chases the cat.
((("cat" "visits" "dog" "~")) -> ("dog" "chases" "cat" "+"))
If something is red then it is not nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "-"))
The cow is red.
True
1
proof
[(triple2)]
("cow" "is" "red" "+")
triple2
The cow is not red.
False
1
inv-proof
[(triple2)]
("cow" "is" "red" "-")
triple2
The cow is not nice.
True
2
proof
[(((triple2) -> rule8))]
("cow" "is" "nice" "-")
((triple2) -> (rule8 % int1))
The cow is not nice.
("cow" "is" "nice" "-")
int1
The cow is nice.
False
2
inv-proof
[(((triple2) -> rule8))]
("cow" "is" "nice" "+")
((triple2) -> (rule8 % int1))
The cow is not nice.
("cow" "is" "nice" "-")
int1
The cat is not blue.
Unknown
inv-rconc
[@1: The cat is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "blue" "-")
The cow is blue.
Unknown
rconc
[@1: The cow is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "blue" "+")
The cow does not visit the cat.
Unknown
inv-random
[@0: The cow visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cat" "-")
The cow eats the cat.
Unknown
random
[@0: The cow eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cat" "+")
@0: The cat is kind.[(triple1)] The cow is red.[(triple2)] The dog does not eat the lion.[(triple3)] The lion does not chase the cow.[(triple4)] @1: The cow is not nice.[(((triple2) -> rule8))]
The cat is kind.
("cat" "is" "kind" "+")
triple1
The cow is red.
("cow" "is" "red" "+")
triple2
The dog does not eat the lion.
("dog" "eats" "lion" "-")
triple3
The lion does not chase the cow.
("lion" "chases" "cow" "-")
triple4
The cow is not nice.
("cow" "is" "nice" "-")
((triple2) -> (rule8 % int1))
The cow is not nice.
("cow" "is" "nice" "-")
int1