The cat chases the squirrel. The cow chases the cat. The squirrel eats the cow. If someone likes the cat then the cat likes the squirrel. If someone is red and they chase the squirrel then they do not like the squirrel. If someone eats the cow then the cow is big. If someone chases the cat then the cat chases the cow. If the squirrel chases the cat and the squirrel is not nice then the squirrel does not chase the cow. If someone is nice and red then they like the cow. If someone chases the cow then they do not eat the cat. If someone chases the cow and they do not eat the cat then the cow is blue.
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
If someone likes the cat then the cat likes the squirrel.
((("someone" "likes" "cat" "+")) -> ("cat" "likes" "squirrel" "+"))
If someone is red and they chase the squirrel then they do not like the squirrel.
((("someone" "is" "red" "+") ("someone" "chases" "squirrel" "+")) -> ("someone" "likes" "squirrel" "-"))
If someone eats the cow then the cow is big.
((("someone" "eats" "cow" "+")) -> ("cow" "is" "big" "+"))
If someone chases the cat then the cat chases the cow.
((("someone" "chases" "cat" "+")) -> ("cat" "chases" "cow" "+"))
If the squirrel chases the cat and the squirrel is not nice then the squirrel does not chase the cow.
((("squirrel" "chases" "cat" "+") ("squirrel" "is" "nice" "~")) -> ("squirrel" "chases" "cow" "-"))
If someone is nice and red then they like the cow.
((("someone" "is" "nice" "+") ("someone" "is" "red" "+")) -> ("someone" "likes" "cow" "+"))
If someone chases the cow then they do not eat the cat.
((("someone" "chases" "cow" "+")) -> ("someone" "eats" "cat" "-"))
If someone chases the cow and they do not eat the cat then the cow is blue.
((("someone" "chases" "cow" "+") ("someone" "eats" "cat" "~")) -> ("cow" "is" "blue" "+"))
The cow chases the cat.
True
1
proof
[(triple2)]
("cow" "chases" "cat" "+")
triple2
The cow does not chase the cat.
False
1
inv-proof
[(triple2)]
("cow" "chases" "cat" "-")
triple2
The cow is big.
True
2
proof
[(((triple3) -> rule3))]
("cow" "is" "big" "+")
((triple3) -> (rule3 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cat does not chase the cow.
False
2
inv-proof
[(((triple2) -> rule4))]
("cat" "chases" "cow" "-")
((triple2) -> (rule4 % int1))
The cat chases the cow.
("cat" "chases" "cow" "+")
int1
The cat does not eat the cat.
True
3
proof
[(((((triple2) -> rule4)) -> rule7))]
("cat" "eats" "cat" "-")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
The cat does not eat the cat.
("cat" "eats" "cat" "-")
int1
The cat chases the cow.
("cat" "chases" "cow" "+")
int2
The cat eats the cat.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule7))]
("cat" "eats" "cat" "+")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
The cat does not eat the cat.
("cat" "eats" "cat" "-")
int1
The cat chases the cow.
("cat" "chases" "cow" "+")
int2
The cow is blue.
True
6
proof
[(((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule7)) -> rule8))]
("cow" "is" "blue" "+")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cat does not eat the cat.
("cat" "eats" "cat" "-")
int2
The cat chases the cow.
("cat" "chases" "cow" "+")
int3
The cow is not blue.
False
6
inv-proof
[(((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule7)) -> rule8))]
("cow" "is" "blue" "-")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cat does not eat the cat.
("cat" "eats" "cat" "-")
int2
The cat chases the cow.
("cat" "chases" "cow" "+")
int3
The squirrel does not like the cow.
Unknown
inv-rconc
[@1: The squirrel likes the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "likes" "cow" "-")
The cow likes the cow.
Unknown
rconc
[@1: The cow likes the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "likes" "cow" "+")
The cat does not like the cow.
Unknown
inv-rconc
[@1: The cat likes the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "likes" "cow" "-")
The cat likes the squirrel.
Unknown
rconc
[@1: The cat likes the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "squirrel" "+")
The cat is not blue.
Unknown
inv-random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
The squirrel does not eat the cat.
Unknown
inv-random
[@0: The squirrel eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "cat" "-")
The squirrel is nice.
Unknown
random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "+")
@0: The cat chases the squirrel.[(triple1)] The cow chases the cat.[(triple2)] The squirrel eats the cow.[(triple3)] @1: The cat chases the cow.[(((triple2) -> rule4))] The cow is big.[(((triple3) -> rule3))] @2: The cat does not eat the cat.[(((((triple2) -> rule4)) -> rule7))] @3: The cow is blue.[(((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule7)) -> rule8))]
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
triple1
The cow chases the cat.
("cow" "chases" "cat" "+")
triple2
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
triple3
The cat chases the cow.
("cat" "chases" "cow" "+")
((triple2) -> (rule4 % int1))
The cat chases the cow.
("cat" "chases" "cow" "+")
int1
The cow is big.
("cow" "is" "big" "+")
((triple3) -> (rule3 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cat does not eat the cat.
("cat" "eats" "cat" "-")
((((triple2) -> (rule4 % int2))) -> (rule7 % int1))
The cat does not eat the cat.
("cat" "eats" "cat" "-")
int1
The cat chases the cow.
("cat" "chases" "cow" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cat does not eat the cat.
("cat" "eats" "cat" "-")
int2
The cat chases the cow.
("cat" "chases" "cow" "+")
int3