The cat is red. The cat visits the cow. The cow is big. The cow needs the dog. The cow needs the squirrel. The dog does not need the cat. The dog visits the cow. The squirrel chases the cow. The squirrel is nice. The squirrel needs the dog. If someone needs the squirrel then they chase the cat. If someone chases the cat then the cat visits the cow. If someone chases the cat then they are nice. If someone chases the squirrel then the squirrel chases the cow. If someone chases the cow and they need the squirrel then the cow needs the squirrel. If someone is nice then they do not need the cat. If someone needs the dog and they are red then they chase the dog. If someone is nice and not green then they do not visit the cat.
The cat is red.
("cat" "is" "red" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow is big.
("cow" "is" "big" "+")
The cow needs the dog.
("cow" "needs" "dog" "+")
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The dog does not need the cat.
("dog" "needs" "cat" "-")
The dog visits the cow.
("dog" "visits" "cow" "+")
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
If someone needs the squirrel then they chase the cat.
((("someone" "needs" "squirrel" "+")) -> ("someone" "chases" "cat" "+"))
If someone chases the cat then the cat visits the cow.
((("someone" "chases" "cat" "+")) -> ("cat" "visits" "cow" "+"))
If someone chases the cat then they are nice.
((("someone" "chases" "cat" "+")) -> ("someone" "is" "nice" "+"))
If someone chases the squirrel then the squirrel chases the cow.
((("someone" "chases" "squirrel" "+")) -> ("squirrel" "chases" "cow" "+"))
If someone chases the cow and they need the squirrel then the cow needs the squirrel.
((("someone" "chases" "cow" "+") ("someone" "needs" "squirrel" "+")) -> ("cow" "needs" "squirrel" "+"))
If someone is nice then they do not need the cat.
((("someone" "is" "nice" "+")) -> ("someone" "needs" "cat" "-"))
If someone needs the dog and they are red then they chase the dog.
((("someone" "needs" "dog" "+") ("someone" "is" "red" "+")) -> ("someone" "chases" "dog" "+"))
If someone is nice and not green then they do not visit the cat.
((("someone" "is" "nice" "+") ("someone" "is" "green" "~")) -> ("someone" "visits" "cat" "-"))
The squirrel needs the dog.
True
1
proof
[(triple10)]
("squirrel" "needs" "dog" "+")
triple10
The cat does not visit the cow.
False
1
inv-proof
[(triple2 OR ((((triple5) -> rule1)) -> rule2))]
("cat" "visits" "cow" "-")
triple2
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The cow chases the cat.
("cow" "chases" "cat" "+")
int2
The squirrel does not need the cat.
True
2
proof
[(((triple9) -> rule6))]
("squirrel" "needs" "cat" "-")
((triple9) -> (rule6 % int1))
The squirrel does not need the cat.
("squirrel" "needs" "cat" "-")
int1
The squirrel needs the cat.
False
2
inv-proof
[(((triple9) -> rule6))]
("squirrel" "needs" "cat" "+")
((triple9) -> (rule6 % int1))
The squirrel does not need the cat.
("squirrel" "needs" "cat" "-")
int1
The cow is nice.
True
3
proof
[(((((triple5) -> rule1)) -> rule3))]
("cow" "is" "nice" "+")
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow chases the cat.
("cow" "chases" "cat" "+")
int2
The cow is not nice.
False
3
inv-proof
[(((((triple5) -> rule1)) -> rule3))]
("cow" "is" "nice" "-")
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow chases the cat.
("cow" "chases" "cat" "+")
int2
The cow does not need the cat.
True
4
proof
[(((((((triple5) -> rule1)) -> rule3)) -> rule6))]
("cow" "needs" "cat" "-")
((((((triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cow does not need the cat.
("cow" "needs" "cat" "-")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow chases the cat.
("cow" "chases" "cat" "+")
int3
The cow needs the cat.
False
4
inv-proof
[(((((((triple5) -> rule1)) -> rule3)) -> rule6))]
("cow" "needs" "cat" "+")
((((((triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cow does not need the cat.
("cow" "needs" "cat" "-")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow chases the cat.
("cow" "chases" "cat" "+")
int3
The dog does not chase the cat.
Unknown
inv-rconc
[@1: The dog chases the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "chases" "cat" "-")
The cow chases the dog.
Unknown
rconc
[@1: The cow chases the dog.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "chases" "dog" "+")
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 squirrel chases the dog.
Unknown
rconc
[@1: The squirrel chases the dog.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "chases" "dog" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
The squirrel does not visit the cow.
Unknown
inv-random
[@0: The squirrel visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "cow" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
@0: The cat is red.[(triple1)] The cat visits the cow.[(triple2 OR ((((triple5) -> rule1)) -> rule2))] The cow is big.[(triple3)] The cow needs the dog.[(triple4)] The cow needs the squirrel.[(triple5)] The dog does not need the cat.[(triple6)] The dog visits the cow.[(triple7)] The squirrel chases the cow.[(triple8)] The squirrel is nice.[(triple9)] The squirrel needs the dog.[(triple10)] @1: The cow chases the cat.[(((triple5) -> rule1))] The squirrel does not need the cat.[(((triple9) -> rule6))] @2: The cow is nice.[(((((triple5) -> rule1)) -> rule3))] @3: The cow does not need the cat.[(((((((triple5) -> rule1)) -> rule3)) -> rule6))]
The cat is red.
("cat" "is" "red" "+")
triple1
The cat visits the cow.
("cat" "visits" "cow" "+")
triple2
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The cow chases the cat.
("cow" "chases" "cat" "+")
int2
The cow is big.
("cow" "is" "big" "+")
triple3
The cow needs the dog.
("cow" "needs" "dog" "+")
triple4
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple5
The dog does not need the cat.
("dog" "needs" "cat" "-")
triple6
The dog visits the cow.
("dog" "visits" "cow" "+")
triple7
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
triple8
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple9
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
triple10
The cow chases the cat.
("cow" "chases" "cat" "+")
((triple5) -> (rule1 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The squirrel does not need the cat.
("squirrel" "needs" "cat" "-")
((triple9) -> (rule6 % int1))
The squirrel does not need the cat.
("squirrel" "needs" "cat" "-")
int1
The cow is nice.
("cow" "is" "nice" "+")
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow chases the cat.
("cow" "chases" "cat" "+")
int2
The cow does not need the cat.
("cow" "needs" "cat" "-")
((((((triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The cow does not need the cat.
("cow" "needs" "cat" "-")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow chases the cat.
("cow" "chases" "cat" "+")
int3