The cow chases the squirrel. The cow is blue. The cow sees the lion. The lion chases the cow. The lion chases the squirrel. The squirrel is not blue. The squirrel likes the cow. If someone sees the lion and the lion is kind then they are red. If someone chases the lion and they are not blue then they see the squirrel. If someone chases the squirrel then the squirrel sees the lion. If someone is red then they see the cow. If someone sees the cow then they do not like the cow. If the lion sees the squirrel then the lion likes the cow. If someone chases the cow then the cow is red. If the squirrel chases the cow and the squirrel does not like the cow then the cow is young.
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The squirrel is not blue.
("squirrel" "is" "blue" "-")
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
If someone sees the lion and the lion is kind then they are red.
((("someone" "sees" "lion" "+") ("lion" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
If someone chases the lion and they are not blue then they see the squirrel.
((("someone" "chases" "lion" "+") ("someone" "is" "blue" "~")) -> ("someone" "sees" "squirrel" "+"))
If someone chases the squirrel then the squirrel sees the lion.
((("someone" "chases" "squirrel" "+")) -> ("squirrel" "sees" "lion" "+"))
If someone is red then they see the cow.
((("someone" "is" "red" "+")) -> ("someone" "sees" "cow" "+"))
If someone sees the cow then they do not like the cow.
((("someone" "sees" "cow" "+")) -> ("someone" "likes" "cow" "-"))
If the lion sees the squirrel then the lion likes the cow.
((("lion" "sees" "squirrel" "+")) -> ("lion" "likes" "cow" "+"))
If someone chases the cow then the cow is red.
((("someone" "chases" "cow" "+")) -> ("cow" "is" "red" "+"))
If the squirrel chases the cow and the squirrel does not like the cow then the cow is young.
((("squirrel" "chases" "cow" "+") ("squirrel" "likes" "cow" "~")) -> ("cow" "is" "young" "+"))
The cow chases the squirrel.
True
1
proof
[(triple1)]
("cow" "chases" "squirrel" "+")
triple1
The cow does not chase the squirrel.
False
1
inv-proof
[(triple1)]
("cow" "chases" "squirrel" "-")
triple1
The squirrel sees the lion.
True
2
proof
[(((triple1) -> rule3) OR ((triple5) -> rule3))]
("squirrel" "sees" "lion" "+")
((triple1) -> (rule3 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
((triple5) -> (rule3 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The squirrel does not see the lion.
False
2
inv-proof
[(((triple1) -> rule3) OR ((triple5) -> rule3))]
("squirrel" "sees" "lion" "-")
((triple1) -> (rule3 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
((triple5) -> (rule3 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The cow sees the cow.
True
3
proof
[(((((triple4) -> rule7)) -> rule4))]
("cow" "sees" "cow" "+")
((((triple4) -> (rule7 % int2))) -> (rule4 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow does not see the cow.
False
3
inv-proof
[(((((triple4) -> rule7)) -> rule4))]
("cow" "sees" "cow" "-")
((((triple4) -> (rule7 % int2))) -> (rule4 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow does not like the cow.
True
4
proof
[(((((((triple4) -> rule7)) -> rule4)) -> rule5))]
("cow" "likes" "cow" "-")
((((((triple4) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow does not like the cow.
("cow" "likes" "cow" "-")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow likes the cow.
False
4
inv-proof
[(((((((triple4) -> rule7)) -> rule4)) -> rule5))]
("cow" "likes" "cow" "+")
((((((triple4) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow does not like the cow.
("cow" "likes" "cow" "-")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow is not young.
Unknown
inv-rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "is" "young" "-")
The lion sees the squirrel.
Unknown
rconc
[@1: The lion sees the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "sees" "squirrel" "+")
The squirrel does not see the squirrel.
Unknown
inv-rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "sees" "squirrel" "-")
The lion is red.
Unknown
rconc
[@1: The lion is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "red" "+")
The squirrel does not chase the lion.
Unknown
inv-random
[@0: The squirrel chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "lion" "-")
The squirrel is round.
Unknown
random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "+")
The squirrel does not chase the squirrel.
Unknown
inv-random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The cow chases the squirrel.[(triple1)] The cow is blue.[(triple2)] The cow sees the lion.[(triple3)] The lion chases the cow.[(triple4)] The lion chases the squirrel.[(triple5)] The squirrel is not blue.[(triple6)] The squirrel likes the cow.[(triple7)] @1: The cow is red.[(((triple4) -> rule7))] The squirrel sees the lion.[(((triple1) -> rule3) OR ((triple5) -> rule3))] @2: The cow sees the cow.[(((((triple4) -> rule7)) -> rule4))] @3: The cow does not like the cow.[(((((((triple4) -> rule7)) -> rule4)) -> rule5))]
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The cow sees the lion.
("cow" "sees" "lion" "+")
triple3
The lion chases the cow.
("lion" "chases" "cow" "+")
triple4
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple5
The squirrel is not blue.
("squirrel" "is" "blue" "-")
triple6
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
triple7
The cow is red.
("cow" "is" "red" "+")
((triple4) -> (rule7 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
((triple1) -> (rule3 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
((triple5) -> (rule3 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
((((triple4) -> (rule7 % int2))) -> (rule4 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow does not like the cow.
("cow" "likes" "cow" "-")
((((((triple4) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cow does not like the cow.
("cow" "likes" "cow" "-")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3