The cat does not chase the cow. The cat chases the tiger. The cat is kind. The cat is red. The cat sees the cow. The cat visits the cow. The cow is not blue. The cow sees the tiger. The tiger does not chase the cow. The tiger is red. If someone visits the cat and the cat is red then they see the cow. If the cow does not see the tiger then the tiger sees the cat. If someone is blue and red then they chase the cat. If someone chases the tiger and the tiger is blue then the tiger is nice. If the cat visits the cow then the cow chases the tiger. If someone is young and they do not see the cow then they do not visit the cow.
The cat does not chase the cow.
("cat" "chases" "cow" "-")
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is red.
("cat" "is" "red" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow is not blue.
("cow" "is" "blue" "-")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The tiger does not chase the cow.
("tiger" "chases" "cow" "-")
The tiger is red.
("tiger" "is" "red" "+")
If someone visits the cat and the cat is red then they see the cow.
((("someone" "visits" "cat" "+") ("cat" "is" "red" "+")) -> ("someone" "sees" "cow" "+"))
If the cow does not see the tiger then the tiger sees the cat.
((("cow" "sees" "tiger" "~")) -> ("tiger" "sees" "cat" "+"))
If someone is blue and red then they chase the cat.
((("someone" "is" "blue" "+") ("someone" "is" "red" "+")) -> ("someone" "chases" "cat" "+"))
If someone chases the tiger and the tiger is blue then the tiger is nice.
((("someone" "chases" "tiger" "+") ("tiger" "is" "blue" "+")) -> ("tiger" "is" "nice" "+"))
If the cat visits the cow then the cow chases the tiger.
((("cat" "visits" "cow" "+")) -> ("cow" "chases" "tiger" "+"))
If someone is young and they do not see the cow then they do not visit the cow.
((("someone" "is" "young" "+") ("someone" "sees" "cow" "~")) -> ("someone" "visits" "cow" "-"))
The cat sees the cow.
True
1
proof
[(triple5)]
("cat" "sees" "cow" "+")
triple5
The cat is not red.
False
1
inv-proof
[(triple4)]
("cat" "is" "red" "-")
triple4
The cow chases the tiger.
True
2
proof
[(((triple6) -> rule5))]
("cow" "chases" "tiger" "+")
((triple6) -> (rule5 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The cow does not chase the tiger.
False
2
inv-proof
[(((triple6) -> rule5))]
("cow" "chases" "tiger" "-")
((triple6) -> (rule5 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The tiger does not see the cow.
Unknown
inv-rconc
[@1: The tiger sees the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "sees" "cow" "-")
The cow sees the cow.
Unknown
rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "sees" "cow" "+")
The cow does not visit the tiger.
Unknown
inv-random
[@0: The cow visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "tiger" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
@0: The cat chases the tiger.[(triple2)] The cat does not chase the cow.[(triple1)] The cat is kind.[(triple3)] The cat is red.[(triple4)] The cat sees the cow.[(triple5)] The cat visits the cow.[(triple6)] The cow is not blue.[(triple7)] The cow sees the tiger.[(triple8)] The tiger does not chase the cow.[(triple9)] The tiger is red.[(triple10)] @1: The cow chases the tiger.[(((triple6) -> rule5))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple2
The cat does not chase the cow.
("cat" "chases" "cow" "-")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple3
The cat is red.
("cat" "is" "red" "+")
triple4
The cat sees the cow.
("cat" "sees" "cow" "+")
triple5
The cat visits the cow.
("cat" "visits" "cow" "+")
triple6
The cow is not blue.
("cow" "is" "blue" "-")
triple7
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple8
The tiger does not chase the cow.
("tiger" "chases" "cow" "-")
triple9
The tiger is red.
("tiger" "is" "red" "+")
triple10
The cow chases the tiger.
("cow" "chases" "tiger" "+")
((triple6) -> (rule5 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1