The cat eats the dog. The cow chases the cat. The dog chases the cow. If the cat eats the dog then the cat is rough. If someone needs the cow and they do not eat the cat then they do not need the dog. If the cat does not need the cow then the cow is blue.
The cat eats the dog.
("cat" "eats" "dog" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
If the cat eats the dog then the cat is rough.
((("cat" "eats" "dog" "+")) -> ("cat" "is" "rough" "+"))
If someone needs the cow and they do not eat the cat then they do not need the dog.
((("someone" "needs" "cow" "+") ("someone" "eats" "cat" "~")) -> ("someone" "needs" "dog" "-"))
If the cat does not need the cow then the cow is blue.
((("cat" "needs" "cow" "~")) -> ("cow" "is" "blue" "+"))
The cow chases the cat.
True
1
proof
[(triple2)]
("cow" "chases" "cat" "+")
triple2
The cat does not eat the dog.
False
1
inv-proof
[(triple1)]
("cat" "eats" "dog" "-")
triple1
The cat is rough.
True
2
proof
[(((triple1) -> rule1))]
("cat" "is" "rough" "+")
((triple1) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is not rough.
False
2
inv-proof
[(((triple1) -> rule1))]
("cat" "is" "rough" "-")
((triple1) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cow is not blue.
Unknown
inv-rconc
[@1: The cow is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "blue" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
The cat does not eat the cow.
Unknown
inv-random
[@0: The cat eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cow" "-")
The dog needs the cow.
Unknown
random
[@0: The dog needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "cow" "+")
@0: The cat eats the dog.[(triple1)] The cow chases the cat.[(triple2)] The dog chases the cow.[(triple3)] @1: The cat is rough.[(((triple1) -> rule1))]
The cat eats the dog.
("cat" "eats" "dog" "+")
triple1
The cow chases the cat.
("cow" "chases" "cat" "+")
triple2
The dog chases the cow.
("dog" "chases" "cow" "+")
triple3
The cat is rough.
("cat" "is" "rough" "+")
((triple1) -> (rule1 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1