The cat chases the cow. The cat chases the rabbit. The cat is blue. The cat is red. The cat sees the cow. The cat sees the rabbit. The cat visits the cow. The cow chases the cat. The cow is kind. The cow is round. The cow visits the cat. The rabbit chases the cat. The rabbit sees the cat. The rabbit visits the cat. The rabbit visits the cow. If someone sees the rabbit then the rabbit sees the cow. If someone is round and they visit the cow then the cow chases the cat.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is red.
("cat" "is" "red" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow is round.
("cow" "is" "round" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
If someone sees the rabbit then the rabbit sees the cow.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "sees" "cow" "+"))
If someone is round and they visit the cow then the cow chases the cat.
((("someone" "is" "round" "+") ("someone" "visits" "cow" "+")) -> ("cow" "chases" "cat" "+"))
The cat chases the cow.
True
1
proof
[(triple1)]
("cat" "chases" "cow" "+")
triple1
The cat does not chase the cow.
False
1
inv-proof
[(triple1)]
("cat" "chases" "cow" "-")
triple1
The rabbit sees the cow.
True
2
proof
[(((triple6) -> rule1))]
("rabbit" "sees" "cow" "+")
((triple6) -> (rule1 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The rabbit does not see the cow.
False
2
inv-proof
[(((triple6) -> rule1))]
("rabbit" "sees" "cow" "-")
((triple6) -> (rule1 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
The rabbit is not kind.
Unknown
inv-random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "-")
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 chases the rabbit.[(triple2)] The cat is blue.[(triple3)] The cat is red.[(triple4)] The cat sees the cow.[(triple5)] The cat sees the rabbit.[(triple6)] The cat visits the cow.[(triple7)] The cow chases the cat.[(triple8)] The cow is kind.[(triple9)] The cow is round.[(triple10)] The cow visits the cat.[(triple11)] The rabbit chases the cat.[(triple12)] The rabbit sees the cat.[(triple13)] The rabbit visits the cat.[(triple14)] The rabbit visits the cow.[(triple15)] @1: The rabbit sees the cow.[(((triple6) -> rule1))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple2
The cat is blue.
("cat" "is" "blue" "+")
triple3
The cat is red.
("cat" "is" "red" "+")
triple4
The cat sees the cow.
("cat" "sees" "cow" "+")
triple5
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple6
The cat visits the cow.
("cat" "visits" "cow" "+")
triple7
The cow chases the cat.
("cow" "chases" "cat" "+")
triple8
The cow is kind.
("cow" "is" "kind" "+")
triple9
The cow is round.
("cow" "is" "round" "+")
triple10
The cow visits the cat.
("cow" "visits" "cat" "+")
triple11
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple12
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple13
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple14
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple15
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
((triple6) -> (rule1 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1