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