The cat chases the cow. The cow chases the cat. The cow is kind. If something chases the cow and the cow chases the cat then the cat likes the cow. Round things are not cold. If something likes the cow then it sees the cat. If something sees the cow then it chases the cow. If something sees the cat and the cat is round then the cat does not chase the cow. If something sees the cat then the cat is not blue.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The cow is kind.
("cow" "is" "kind" "+")
If something chases the cow and the cow chases the cat then the cat likes the cow.
((("something" "chases" "cow" "+") ("cow" "chases" "cat" "+")) -> ("cat" "likes" "cow" "+"))
Round things are not cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "-"))
If something likes the cow then it sees the cat.
((("something" "likes" "cow" "+")) -> ("something" "sees" "cat" "+"))
If something sees the cow then it chases the cow.
((("something" "sees" "cow" "+")) -> ("something" "chases" "cow" "+"))
If something sees the cat and the cat is round then the cat does not chase the cow.
((("something" "sees" "cat" "+") ("cat" "is" "round" "+")) -> ("cat" "chases" "cow" "-"))
If something sees the cat then the cat is not blue.
((("something" "sees" "cat" "+")) -> ("cat" "is" "blue" "-"))
The cow chases the cat.
True
1
proof
[(triple2)]
("cow" "chases" "cat" "+")
triple2
The cow is not kind.
False
1
inv-proof
[(triple3)]
("cow" "is" "kind" "-")
triple3
The cat likes the cow.
True
3
proof
[(((triple1 triple2) -> rule1))]
("cat" "likes" "cow" "+")
((triple1 triple2) -> (rule1 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cat does not like the cow.
False
3
inv-proof
[(((triple1 triple2) -> rule1))]
("cat" "likes" "cow" "-")
((triple1 triple2) -> (rule1 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cat sees the cat.
True
4
proof
[(((((triple1 triple2) -> rule1)) -> rule3))]
("cat" "sees" "cat" "+")
((((triple1 triple2) -> (rule1 % int2))) -> (rule3 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The cat does not see the cat.
False
4
inv-proof
[(((((triple1 triple2) -> rule1)) -> rule3))]
("cat" "sees" "cat" "-")
((((triple1 triple2) -> (rule1 % int2))) -> (rule3 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The cat is not blue.
True
5
proof
[(((((((triple1 triple2) -> rule1)) -> rule3)) -> rule6))]
("cat" "is" "blue" "-")
((((((triple1 triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cat is not blue.
("cat" "is" "blue" "-")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat likes the cow.
("cat" "likes" "cow" "+")
int3
The cat is blue.
False
5
inv-proof
[(((((((triple1 triple2) -> rule1)) -> rule3)) -> rule6))]
("cat" "is" "blue" "+")
((((((triple1 triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cat is not blue.
("cat" "is" "blue" "-")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat likes the cow.
("cat" "likes" "cow" "+")
int3
The cow does not see the cat.
Unknown
inv-rconc
[@1: The cow sees the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "sees" "cat" "-")
The cow chases the cow.
Unknown
rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "chases" "cow" "+")
The cow is not big.
Unknown
inv-random
[@0: The cow is big.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "big" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The cat is cold.
Unknown
random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "+")
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The cat sees the cow.
Unknown
random
[@0: The cat sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cow" "+")
@0: The cat chases the cow.[(triple1)] The cow chases the cat.[(triple2)] The cow is kind.[(triple3)] @1: The cat likes the cow.[(((triple1 triple2) -> rule1))] @2: The cat sees the cat.[(((((triple1 triple2) -> rule1)) -> rule3))] @3: The cat is not blue.[(((((((triple1 triple2) -> rule1)) -> rule3)) -> rule6))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
The cow chases the cat.
("cow" "chases" "cat" "+")
triple2
The cow is kind.
("cow" "is" "kind" "+")
triple3
The cat likes the cow.
("cat" "likes" "cow" "+")
((triple1 triple2) -> (rule1 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
((((triple1 triple2) -> (rule1 % int2))) -> (rule3 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The cat is not blue.
("cat" "is" "blue" "-")
((((((triple1 triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cat is not blue.
("cat" "is" "blue" "-")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat likes the cow.
("cat" "likes" "cow" "+")
int3