The cat sees the cow. The cow needs the cat. If someone chases the cat and the cat chases the cow then the cat does not see the cow. If the cow is young then the cow needs the cat. If someone needs the cat and the cat sees the cow then they chase the cow. If someone chases the cow then the cow does not chase the cat. If someone sees the cat and the cat chases the cow then the cow does not see the cat. If someone is kind and they do not need the cat then they need the cow. If the cat needs the cow and the cat does not see the cow then the cat is not red. If someone sees the cow and they do not need the cow then they are not blue.
The cat sees the cow.
("cat" "sees" "cow" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
If someone chases the cat and the cat chases the cow then the cat does not see the cow.
((("someone" "chases" "cat" "+") ("cat" "chases" "cow" "+")) -> ("cat" "sees" "cow" "-"))
If the cow is young then the cow needs the cat.
((("cow" "is" "young" "+")) -> ("cow" "needs" "cat" "+"))
If someone needs the cat and the cat sees the cow then they chase the cow.
((("someone" "needs" "cat" "+") ("cat" "sees" "cow" "+")) -> ("someone" "chases" "cow" "+"))
If someone chases the cow then the cow does not chase the cat.
((("someone" "chases" "cow" "+")) -> ("cow" "chases" "cat" "-"))
If someone sees the cat and the cat chases the cow then the cow does not see the cat.
((("someone" "sees" "cat" "+") ("cat" "chases" "cow" "+")) -> ("cow" "sees" "cat" "-"))
If someone is kind and they do not need the cat then they need the cow.
((("someone" "is" "kind" "+") ("someone" "needs" "cat" "~")) -> ("someone" "needs" "cow" "+"))
If the cat needs the cow and the cat does not see the cow then the cat is not red.
((("cat" "needs" "cow" "+") ("cat" "sees" "cow" "~")) -> ("cat" "is" "red" "-"))
If someone sees the cow and they do not need the cow then they are not blue.
((("someone" "sees" "cow" "+") ("someone" "needs" "cow" "~")) -> ("someone" "is" "blue" "-"))
The cat sees the cow.
True
1
proof
[(triple1)]
("cat" "sees" "cow" "+")
triple1
The cow does not need the cat.
False
1
inv-proof
[(triple2)]
("cow" "needs" "cat" "-")
triple2
The cow chases the cow.
True
3
proof
[(((triple2 triple1) -> rule3))]
("cow" "chases" "cow" "+")
((triple2 triple1) -> (rule3 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow does not chase the cow.
False
3
inv-proof
[(((triple2 triple1) -> rule3))]
("cow" "chases" "cow" "-")
((triple2 triple1) -> (rule3 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow does not chase the cat.
True
4
proof
[(((((triple2 triple1) -> rule3)) -> rule4))]
("cow" "chases" "cat" "-")
((((triple2 triple1) -> (rule3 % int2))) -> (rule4 % int1))
The cow does not chase the cat.
("cow" "chases" "cat" "-")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow chases the cat.
False
4
inv-proof
[(((((triple2 triple1) -> rule3)) -> rule4))]
("cow" "chases" "cat" "+")
((((triple2 triple1) -> (rule3 % int2))) -> (rule4 % int1))
The cow does not chase the cat.
("cow" "chases" "cat" "-")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cat does not chase the cow.
Unknown
inv-rconc
[@1: The cat chases the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "chases" "cow" "-")
The cow needs the cow.
Unknown
rconc
[@1: The cow needs the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "needs" "cow" "+")
The cat does not need the cow.
Unknown
inv-rconc
[@1: The cat needs the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "needs" "cow" "-")
The cow sees the cat.
Unknown
random
[@0: The cow sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cat" "+")
The cat is not young.
Unknown
inv-random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
@0: The cat sees the cow.[(triple1)] The cow needs the cat.[(triple2)] @1: The cow chases the cow.[(((triple2 triple1) -> rule3))] @2: The cow does not chase the cat.[(((((triple2 triple1) -> rule3)) -> rule4))]
The cat sees the cow.
("cat" "sees" "cow" "+")
triple1
The cow needs the cat.
("cow" "needs" "cat" "+")
triple2
The cow chases the cow.
("cow" "chases" "cow" "+")
((triple2 triple1) -> (rule3 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow does not chase the cat.
("cow" "chases" "cat" "-")
((((triple2 triple1) -> (rule3 % int2))) -> (rule4 % int1))
The cow does not chase the cat.
("cow" "chases" "cat" "-")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2