The cat chases the cow. The cat is green. The cat needs the cow. The cow chases the cat. The cow is green. The cow needs the cat. The cow visits the cat. If something is blue then it chases the cat. If the cat chases the cow then the cow visits the cat. If the cow visits the cat and the cow chases the cat then the cat visits the cow.
The cat chases the cow.
("cat" "chases" "cow" "+")
The cat is green.
("cat" "is" "green" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The cow is green.
("cow" "is" "green" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
If something is blue then it chases the cat.
((("something" "is" "blue" "+")) -> ("something" "chases" "cat" "+"))
If the cat chases the cow then the cow visits the cat.
((("cat" "chases" "cow" "+")) -> ("cow" "visits" "cat" "+"))
If the cow visits the cat and the cow chases the cat then the cat visits the cow.
((("cow" "visits" "cat" "+") ("cow" "chases" "cat" "+")) -> ("cat" "visits" "cow" "+"))
The cow is green.
True
1
proof
[(triple5)]
("cow" "is" "green" "+")
triple5
The cow is not green.
False
1
inv-proof
[(triple5)]
("cow" "is" "green" "-")
triple5
The cat visits the cow.
True
3
proof
[(((triple7 triple4) -> rule3) OR ((((triple1) -> rule2) triple4) -> rule3))]
("cat" "visits" "cow" "+")
((triple7 triple4) -> (rule3 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
((((triple1) -> (rule2 % int2)) triple4) -> (rule3 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The cow visits the cat.
("cow" "visits" "cat" "+")
int2
The cat does not visit the cow.
False
3
inv-proof
[(((triple7 triple4) -> rule3) OR ((((triple1) -> rule2) triple4) -> rule3))]
("cat" "visits" "cow" "-")
((triple7 triple4) -> (rule3 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
((((triple1) -> (rule2 % int2)) triple4) -> (rule3 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The cow visits the cat.
("cow" "visits" "cat" "+")
int2
The cat does not chase the cat.
Unknown
inv-rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "chases" "cat" "-")
The cat is rough.
Unknown
random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "+")
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
@0: The cat chases the cow.[(triple1)] The cat is green.[(triple2)] The cat needs the cow.[(triple3)] The cow chases the cat.[(triple4)] The cow is green.[(triple5)] The cow needs the cat.[(triple6)] The cow visits the cat.[(triple7 OR ((triple1) -> rule2))] @1: The cat visits the cow.[(((triple7 triple4) -> rule3) OR ((((triple1) -> rule2) triple4) -> rule3))]
The cat chases the cow.
("cat" "chases" "cow" "+")
triple1
The cat is green.
("cat" "is" "green" "+")
triple2
The cat needs the cow.
("cat" "needs" "cow" "+")
triple3
The cow chases the cat.
("cow" "chases" "cat" "+")
triple4
The cow is green.
("cow" "is" "green" "+")
triple5
The cow needs the cat.
("cow" "needs" "cat" "+")
triple6
The cow visits the cat.
("cow" "visits" "cat" "+")
triple7
((triple1) -> (rule2 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
The cat visits the cow.
("cat" "visits" "cow" "+")
((triple7 triple4) -> (rule3 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
((((triple1) -> (rule2 % int2)) triple4) -> (rule3 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The cow visits the cat.
("cow" "visits" "cat" "+")
int2