The cat chases the cow. The cat eats the cow. The cat is big. The cat is blue. The cat is red. The cat is rough. The cat is not round. The cat sees the cow. The cow chases the cat. The cow does not eat the cat. The cow is big. The cow is blue. The cow is red. The cow is round. The cow sees the cat. If the cat is round and the cat does not see the cow then the cow is round. If something is blue and red then it chases the cat. If the cat is not blue and the cat is not round then the cat is not rough. If the cow is rough and the cow sees the cat then the cat does not chase the cow. If something is rough then it eats the cow. If something is round and not big then it is rough. If the cow is rough and the cow sees the cat then the cow chases the cat. If something sees the cow and it does not chase the cat then it chases the cow.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat is not round.
("cat" "is" "round" "-")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The cow does not eat the cat.
("cow" "eats" "cat" "-")
The cow is big.
("cow" "is" "big" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is red.
("cow" "is" "red" "+")
The cow is round.
("cow" "is" "round" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
If the cat is round and the cat does not see the cow then the cow is round.
((("cat" "is" "round" "+") ("cat" "sees" "cow" "~")) -> ("cow" "is" "round" "+"))
If something is blue and red then it chases the cat.
((("something" "is" "blue" "+") ("something" "is" "red" "+")) -> ("something" "chases" "cat" "+"))
If the cat is not blue and the cat is not round then the cat is not rough.
((("cat" "is" "blue" "~") ("cat" "is" "round" "~")) -> ("cat" "is" "rough" "-"))
If the cow is rough and the cow sees the cat then the cat does not chase the cow.
((("cow" "is" "rough" "+") ("cow" "sees" "cat" "+")) -> ("cat" "chases" "cow" "-"))
If something is rough then it eats the cow.
((("something" "is" "rough" "+")) -> ("something" "eats" "cow" "+"))
If something is round and not big then it is rough.
((("something" "is" "round" "+") ("something" "is" "big" "~")) -> ("something" "is" "rough" "+"))
If the cow is rough and the cow sees the cat then the cow chases the cat.
((("cow" "is" "rough" "+") ("cow" "sees" "cat" "+")) -> ("cow" "chases" "cat" "+"))
If something sees the cow and it does not chase the cat then it chases the cow.
((("something" "sees" "cow" "+") ("something" "chases" "cat" "~")) -> ("something" "chases" "cow" "+"))
The cat is big.
True
1
proof
[(triple3)]
("cat" "is" "big" "+")
triple3
The cat does not see the cow.
False
1
inv-proof
[(triple8)]
("cat" "sees" "cow" "-")
triple8
The cow does not chase the cow.
Unknown
inv-rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "chases" "cow" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
@0: The cat chases the cow.[(triple1)] The cat eats the cow.[(triple2 OR ((triple6) -> rule5))] The cat is big.[(triple3)] The cat is blue.[(triple4)] The cat is not round.[(triple7)] The cat is red.[(triple5)] The cat is rough.[(triple6)] The cat sees the cow.[(triple8)] The cow chases the cat.[(triple9 OR ((triple12 triple13) -> rule2))] The cow does not eat the cat.[(triple10)] The cow is big.[(triple11)] The cow is blue.[(triple12)] The cow is red.[(triple13)] The cow is round.[(triple14)] The cow sees the cat.[(triple15)] @1: The cat chases the cat.[(((triple4 triple5) -> rule2))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
The cat eats the cow.
("cat" "eats" "cow" "+")
triple2
((triple6) -> (rule5 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The cat is big.
("cat" "is" "big" "+")
triple3
The cat is blue.
("cat" "is" "blue" "+")
triple4
The cat is not round.
("cat" "is" "round" "-")
triple7
The cat is red.
("cat" "is" "red" "+")
triple5
The cat is rough.
("cat" "is" "rough" "+")
triple6
The cat sees the cow.
("cat" "sees" "cow" "+")
triple8
The cow chases the cat.
("cow" "chases" "cat" "+")
triple9
((triple12 triple13) -> (rule2 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow does not eat the cat.
("cow" "eats" "cat" "-")
triple10
The cow is big.
("cow" "is" "big" "+")
triple11
The cow is blue.
("cow" "is" "blue" "+")
triple12
The cow is red.
("cow" "is" "red" "+")
triple13
The cow is round.
("cow" "is" "round" "+")
triple14
The cow sees the cat.
("cow" "sees" "cat" "+")
triple15
The cat chases the cat.
("cat" "chases" "cat" "+")
((triple4 triple5) -> (rule2 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1