The cat chases the cow. The cat is big. The cat is nice. The cat is young. The cat likes the cow. The cow chases the cat. The cow is big. The cow is nice. The cow is red. The cow is rough. The cow likes the cat. The cow visits the cat. If someone is red and they like the cow then they like the cat. If someone visits the cow then they chase the cat. If someone chases the cat then they visit the cow. If someone is big and they visit the cat then the cat likes the cow. If someone likes the cat then they chase the cat. If someone visits the cow and the cow visits the cat then they like the cat.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat is young.
("cat" "is" "young" "+")
The cat likes the cow.
("cat" "likes" "cow" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
If someone is red and they like the cow then they like the cat.
((("someone" "is" "red" "+") ("someone" "likes" "cow" "+")) -> ("someone" "likes" "cat" "+"))
If someone visits the cow then they chase the cat.
((("someone" "visits" "cow" "+")) -> ("someone" "chases" "cat" "+"))
If someone chases the cat then they visit the cow.
((("someone" "chases" "cat" "+")) -> ("someone" "visits" "cow" "+"))
If someone is big and they visit the cat then the cat likes the cow.
((("someone" "is" "big" "+") ("someone" "visits" "cat" "+")) -> ("cat" "likes" "cow" "+"))
If someone likes the cat then they chase the cat.
((("someone" "likes" "cat" "+")) -> ("someone" "chases" "cat" "+"))
If someone visits the cow and the cow visits the cat then they like the cat.
((("someone" "visits" "cow" "+") ("cow" "visits" "cat" "+")) -> ("someone" "likes" "cat" "+"))
The cat chases the cow.
True
1
proof
[(triple1)]
("cat" "chases" "cow" "+")
triple1
The cow does not chase the cat.
False
1
inv-proof
[(triple6 OR ((triple11) -> rule5))]
("cow" "chases" "cat" "-")
triple6
((triple11) -> (rule5 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow visits the cow.
True
2
proof
[(((triple6) -> rule3) OR ((((triple11) -> rule5)) -> rule3))]
("cow" "visits" "cow" "+")
((triple6) -> (rule3 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
((((triple11) -> (rule5 % int2))) -> (rule3 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow chases the cat.
("cow" "chases" "cat" "+")
int2
The cow does not visit the cow.
False
2
inv-proof
[(((triple6) -> rule3) OR ((((triple11) -> rule5)) -> rule3))]
("cow" "visits" "cow" "-")
((triple6) -> (rule3 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
((((triple11) -> (rule5 % int2))) -> (rule3 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow chases the cat.
("cow" "chases" "cat" "+")
int2
The cat does not chase the cat.
Unknown
inv-rconc
[@4: The cat chases the cat.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule5 <- rule1 <- FAIL)]]
("cat" "chases" "cat" "-")
The cat visits the cow.
Unknown
rconc
[@3: The cat visits the cow.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule1 <- FAIL)]]
("cat" "visits" "cow" "+")
The cow is not young.
Unknown
inv-random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
@0: The cat chases the cow.[(triple1)] The cat is big.[(triple2)] The cat is nice.[(triple3)] The cat is young.[(triple4)] The cat likes the cow.[(triple5 OR ((triple7 triple12) -> rule4))] The cow chases the cat.[(triple6 OR ((triple11) -> rule5))] The cow is big.[(triple7)] The cow is nice.[(triple8)] The cow is red.[(triple9)] The cow is rough.[(triple10)] The cow likes the cat.[(triple11 OR ((((triple6) -> rule3) triple12) -> rule6))] The cow visits the cat.[(triple12)] @1: The cow visits the cow.[(((triple6) -> rule3) OR ((((triple11) -> rule5)) -> rule3))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat is nice.
("cat" "is" "nice" "+")
triple3
The cat is young.
("cat" "is" "young" "+")
triple4
The cat likes the cow.
("cat" "likes" "cow" "+")
triple5
((triple7 triple12) -> (rule4 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cow chases the cat.
("cow" "chases" "cat" "+")
triple6
((triple11) -> (rule5 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow is big.
("cow" "is" "big" "+")
triple7
The cow is nice.
("cow" "is" "nice" "+")
triple8
The cow is red.
("cow" "is" "red" "+")
triple9
The cow is rough.
("cow" "is" "rough" "+")
triple10
The cow likes the cat.
("cow" "likes" "cat" "+")
triple11
((((triple6) -> (rule3 % int2)) triple12) -> (rule6 % int1))
The cow likes the cat.
("cow" "likes" "cat" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow visits the cat.
("cow" "visits" "cat" "+")
triple12
The cow visits the cow.
("cow" "visits" "cow" "+")
((triple6) -> (rule3 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
((((triple11) -> (rule5 % int2))) -> (rule3 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow chases the cat.
("cow" "chases" "cat" "+")
int2