The bear chases the cat. The bear chases the squirrel. The bear eats the squirrel. The bear is young. The bear sees the cow. The cat does not chase the squirrel. The cat is green. The cow chases the squirrel. The cow eats the squirrel. The cow sees the bear. The squirrel is kind. The squirrel is round. The squirrel is young. The squirrel does not see the cat. If someone chases the squirrel then they eat the cat. If someone eats the cow then the cow is blue. If someone is young then they eat the cow. If someone is blue then they eat the cow. If someone is green and they eat the cow then the cow does not see the bear. If someone sees the cow then they chase the cat. If someone chases the cow then the cow eats the squirrel. If someone eats the bear and they do not chase the squirrel then the squirrel eats the cow. If someone eats the cow and the cow eats the cat then they see the cow.
The bear chases the cat.
("bear" "chases" "cat" "+")
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
The bear is young.
("bear" "is" "young" "+")
The bear sees the cow.
("bear" "sees" "cow" "+")
The cat does not chase the squirrel.
("cat" "chases" "squirrel" "-")
The cat is green.
("cat" "is" "green" "+")
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel does not see the cat.
("squirrel" "sees" "cat" "-")
If someone chases the squirrel then they eat the cat.
((("someone" "chases" "squirrel" "+")) -> ("someone" "eats" "cat" "+"))
If someone eats the cow then the cow is blue.
((("someone" "eats" "cow" "+")) -> ("cow" "is" "blue" "+"))
If someone is young then they eat the cow.
((("someone" "is" "young" "+")) -> ("someone" "eats" "cow" "+"))
If someone is blue then they eat the cow.
((("someone" "is" "blue" "+")) -> ("someone" "eats" "cow" "+"))
If someone is green and they eat the cow then the cow does not see the bear.
((("someone" "is" "green" "+") ("someone" "eats" "cow" "+")) -> ("cow" "sees" "bear" "-"))
If someone sees the cow then they chase the cat.
((("someone" "sees" "cow" "+")) -> ("someone" "chases" "cat" "+"))
If someone chases the cow then the cow eats the squirrel.
((("someone" "chases" "cow" "+")) -> ("cow" "eats" "squirrel" "+"))
If someone eats the bear and they do not chase the squirrel then the squirrel eats the cow.
((("someone" "eats" "bear" "+") ("someone" "chases" "squirrel" "~")) -> ("squirrel" "eats" "cow" "+"))
If someone eats the cow and the cow eats the cat then they see the cow.
((("someone" "eats" "cow" "+") ("cow" "eats" "cat" "+")) -> ("someone" "sees" "cow" "+"))
The bear is young.
True
1
proof
[(triple4)]
("bear" "is" "young" "+")
triple4
The cow does not chase the squirrel.
False
1
inv-proof
[(triple8)]
("cow" "chases" "squirrel" "-")
triple8
The bear eats the cat.
True
2
proof
[(((triple2) -> rule1))]
("bear" "eats" "cat" "+")
((triple2) -> (rule1 % int1))
The bear eats the cat.
("bear" "eats" "cat" "+")
int1
The squirrel does not eat the cow.
False
2
inv-proof
[(((triple13) -> rule3))]
("squirrel" "eats" "cow" "-")
((triple13) -> (rule3 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The cow is blue.
True
3
proof
[(((((triple13) -> rule3)) -> rule2) OR ((((triple4) -> rule3)) -> rule2))]
("cow" "is" "blue" "+")
((((triple13) -> (rule3 % int2))) -> (rule2 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int2
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The bear eats the cow.
("bear" "eats" "cow" "+")
int2
The squirrel does not see the cow.
False
5
inv-proof
[(((((triple13) -> rule3) ((triple8) -> rule1)) -> rule9))]
("squirrel" "sees" "cow" "-")
((((triple13) -> (rule3 % int3)) ((triple8) -> (rule1 % int2))) -> (rule9 % int1))
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int1
The cow eats the cat.
("cow" "eats" "cat" "+")
int2
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int3
The cow eats the cow.
True
4
proof
[(((((((triple13) -> rule3)) -> rule2)) -> rule4) OR ((((((triple4) -> rule3)) -> rule2)) -> rule4))]
("cow" "eats" "cow" "+")
((((((triple13) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int3
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The bear eats the cow.
("bear" "eats" "cow" "+")
int3
The cow does not eat the cow.
False
4
inv-proof
[(((((((triple13) -> rule3)) -> rule2)) -> rule4) OR ((((((triple4) -> rule3)) -> rule2)) -> rule4))]
("cow" "eats" "cow" "-")
((((((triple13) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int3
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The bear eats the cow.
("bear" "eats" "cow" "+")
int3
The cow sees the cow.
True
7
proof
[(((((((((triple13) -> rule3)) -> rule2)) -> rule4) ((triple8) -> rule1)) -> rule9) OR ((((((((triple4) -> rule3)) -> rule2)) -> rule4) ((triple8) -> rule1)) -> rule9))]
("cow" "sees" "cow" "+")
((((((((triple13) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule4 % int3)) ((triple8) -> (rule1 % int2))) -> (rule9 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow eats the cat.
("cow" "eats" "cat" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
The cow is blue.
("cow" "is" "blue" "+")
int4
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int5
((((((((triple4) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule4 % int3)) ((triple8) -> (rule1 % int2))) -> (rule9 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow eats the cat.
("cow" "eats" "cat" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
The cow is blue.
("cow" "is" "blue" "+")
int4
The bear eats the cow.
("bear" "eats" "cow" "+")
int5
The cow does not see the cow.
False
7
inv-proof
[(((((((((triple13) -> rule3)) -> rule2)) -> rule4) ((triple8) -> rule1)) -> rule9) OR ((((((((triple4) -> rule3)) -> rule2)) -> rule4) ((triple8) -> rule1)) -> rule9))]
("cow" "sees" "cow" "-")
((((((((triple13) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule4 % int3)) ((triple8) -> (rule1 % int2))) -> (rule9 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow eats the cat.
("cow" "eats" "cat" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
The cow is blue.
("cow" "is" "blue" "+")
int4
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int5
((((((((triple4) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule4 % int3)) ((triple8) -> (rule1 % int2))) -> (rule9 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow eats the cat.
("cow" "eats" "cat" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
The cow is blue.
("cow" "is" "blue" "+")
int4
The bear eats the cow.
("bear" "eats" "cow" "+")
int5
The cow chases the cat.
True
8
proof
[(((((((((((triple13) -> rule3)) -> rule2)) -> rule4) ((triple8) -> rule1)) -> rule9)) -> rule6) OR ((((((((((triple4) -> rule3)) -> rule2)) -> rule4) ((triple8) -> rule1)) -> rule9)) -> rule6))]
("cow" "chases" "cat" "+")
((((((((((triple13) -> (rule3 % int6))) -> (rule2 % int5))) -> (rule4 % int4)) ((triple8) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The cow eats the cat.
("cow" "eats" "cat" "+")
int3
The cow eats the cow.
("cow" "eats" "cow" "+")
int4
The cow is blue.
("cow" "is" "blue" "+")
int5
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int6
((((((((((triple4) -> (rule3 % int6))) -> (rule2 % int5))) -> (rule4 % int4)) ((triple8) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The cow eats the cat.
("cow" "eats" "cat" "+")
int3
The cow eats the cow.
("cow" "eats" "cow" "+")
int4
The cow is blue.
("cow" "is" "blue" "+")
int5
The bear eats the cow.
("bear" "eats" "cow" "+")
int6
The cow does not chase the cat.
False
8
inv-proof
[(((((((((((triple13) -> rule3)) -> rule2)) -> rule4) ((triple8) -> rule1)) -> rule9)) -> rule6) OR ((((((((((triple4) -> rule3)) -> rule2)) -> rule4) ((triple8) -> rule1)) -> rule9)) -> rule6))]
("cow" "chases" "cat" "-")
((((((((((triple13) -> (rule3 % int6))) -> (rule2 % int5))) -> (rule4 % int4)) ((triple8) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The cow eats the cat.
("cow" "eats" "cat" "+")
int3
The cow eats the cow.
("cow" "eats" "cow" "+")
int4
The cow is blue.
("cow" "is" "blue" "+")
int5
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int6
((((((((((triple4) -> (rule3 % int6))) -> (rule2 % int5))) -> (rule4 % int4)) ((triple8) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The cow eats the cat.
("cow" "eats" "cat" "+")
int3
The cow eats the cow.
("cow" "eats" "cow" "+")
int4
The cow is blue.
("cow" "is" "blue" "+")
int5
The bear eats the cow.
("bear" "eats" "cow" "+")
int6
The squirrel does not eat the cat.
Unknown
inv-rconc
[@1: The squirrel eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "eats" "cat" "-")
The cat sees the cow.
Unknown
rconc
[@2: The cat sees the cow.[CWA. Example of deepest failure = (rule9 <- rule3 <- FAIL)]]
("cat" "sees" "cow" "+")
The cat does not eat the cow.
Unknown
inv-rconc
[@1: The cat eats the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "eats" "cow" "-")
The cat eats the cat.
Unknown
rconc
[@1: The cat eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "eats" "cat" "+")
The cat does not chase the cat.
Unknown
inv-rconc
[@3: The cat chases the cat.[CWA. Example of deepest failure = (rule6 <- rule9 <- rule3 <- FAIL)]]
("cat" "chases" "cat" "-")
The cow is round.
Unknown
random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "+")
The cat does not chase the bear.
Unknown
inv-random
[@0: The cat chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "bear" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
The cat does not eat the bear.
Unknown
inv-random
[@0: The cat eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "bear" "-")
The cow is kind.
Unknown
random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "+")
The cat is not kind.
Unknown
inv-random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "-")
The bear chases the bear.
Unknown
random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "+")
@0: The bear chases the cat.[(triple1 OR ((triple5) -> rule6) OR ((((((triple4) -> rule3) ((triple8) -> rule1)) -> rule9)) -> rule6))] The bear chases the squirrel.[(triple2)] The bear eats the squirrel.[(triple3)] The bear is young.[(triple4)] The bear sees the cow.[(triple5 OR ((((triple4) -> rule3) ((triple8) -> rule1)) -> rule9))] The cat does not chase the squirrel.[(triple6)] The cat is green.[(triple7)] The cow chases the squirrel.[(triple8)] The cow eats the squirrel.[(triple9)] The cow sees the bear.[(triple10)] The squirrel does not see the cat.[(triple14)] The squirrel is kind.[(triple11)] The squirrel is round.[(triple12)] The squirrel is young.[(triple13)] @1: The bear eats the cat.[(((triple2) -> rule1))] The bear eats the cow.[(((triple4) -> rule3))] The cow eats the cat.[(((triple8) -> rule1))] The squirrel eats the cow.[(((triple13) -> rule3))] @2: The cow is blue.[(((((triple13) -> rule3)) -> rule2) OR ((((triple4) -> rule3)) -> rule2))] The squirrel sees the cow.[(((((triple13) -> rule3) ((triple8) -> rule1)) -> rule9))] @3: The cow eats the cow.[(((((((triple13) -> rule3)) -> rule2)) -> rule4) OR ((((((triple4) -> rule3)) -> rule2)) -> rule4))] The squirrel chases the cat.[(((((((triple13) -> rule3) ((triple8) -> rule1)) -> rule9)) -> rule6))] @4: The cow sees the cow.[(((((((((triple13) -> rule3)) -> rule2)) -> rule4) ((triple8) -> rule1)) -> rule9) OR ((((((((triple4) -> rule3)) -> rule2)) -> rule4) ((triple8) -> rule1)) -> rule9))] @5: The cow chases the cat.[(((((((((((triple13) -> rule3)) -> rule2)) -> rule4) ((triple8) -> rule1)) -> rule9)) -> rule6) OR ((((((((((triple4) -> rule3)) -> rule2)) -> rule4) ((triple8) -> rule1)) -> rule9)) -> rule6))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
((triple5) -> (rule6 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
((((((triple4) -> (rule3 % int4)) ((triple8) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
The bear chases the cat.
("bear" "chases" "cat" "+")
int1
The bear sees the cow.
("bear" "sees" "cow" "+")
int2
The cow eats the cat.
("cow" "eats" "cat" "+")
int3
The bear eats the cow.
("bear" "eats" "cow" "+")
int4
The bear chases the squirrel.
("bear" "chases" "squirrel" "+")
triple2
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
triple3
The bear is young.
("bear" "is" "young" "+")
triple4
The bear sees the cow.
("bear" "sees" "cow" "+")
triple5
((((triple4) -> (rule3 % int3)) ((triple8) -> (rule1 % int2))) -> (rule9 % int1))
The bear sees the cow.
("bear" "sees" "cow" "+")
int1
The cow eats the cat.
("cow" "eats" "cat" "+")
int2
The bear eats the cow.
("bear" "eats" "cow" "+")
int3
The cat does not chase the squirrel.
("cat" "chases" "squirrel" "-")
triple6
The cat is green.
("cat" "is" "green" "+")
triple7
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
triple8
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
triple9
The cow sees the bear.
("cow" "sees" "bear" "+")
triple10
The squirrel does not see the cat.
("squirrel" "sees" "cat" "-")
triple14
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple11
The squirrel is round.
("squirrel" "is" "round" "+")
triple12
The squirrel is young.
("squirrel" "is" "young" "+")
triple13
The bear eats the cat.
("bear" "eats" "cat" "+")
((triple2) -> (rule1 % int1))
The bear eats the cat.
("bear" "eats" "cat" "+")
int1
The bear eats the cow.
("bear" "eats" "cow" "+")
((triple4) -> (rule3 % int1))
The bear eats the cow.
("bear" "eats" "cow" "+")
int1
The cow eats the cat.
("cow" "eats" "cat" "+")
((triple8) -> (rule1 % int1))
The cow eats the cat.
("cow" "eats" "cat" "+")
int1
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
((triple13) -> (rule3 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
((((triple13) -> (rule3 % int2))) -> (rule2 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int2
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The bear eats the cow.
("bear" "eats" "cow" "+")
int2
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
((((triple13) -> (rule3 % int3)) ((triple8) -> (rule1 % int2))) -> (rule9 % int1))
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int1
The cow eats the cat.
("cow" "eats" "cat" "+")
int2
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int3
The cow eats the cow.
("cow" "eats" "cow" "+")
((((((triple13) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int3
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow eats the cow.
("cow" "eats" "cow" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The bear eats the cow.
("bear" "eats" "cow" "+")
int3
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
((((((triple13) -> (rule3 % int4)) ((triple8) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
The squirrel sees the cow.
("squirrel" "sees" "cow" "+")
int2
The cow eats the cat.
("cow" "eats" "cat" "+")
int3
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int4
The cow sees the cow.
("cow" "sees" "cow" "+")
((((((((triple13) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule4 % int3)) ((triple8) -> (rule1 % int2))) -> (rule9 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow eats the cat.
("cow" "eats" "cat" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
The cow is blue.
("cow" "is" "blue" "+")
int4
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int5
((((((((triple4) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule4 % int3)) ((triple8) -> (rule1 % int2))) -> (rule9 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow eats the cat.
("cow" "eats" "cat" "+")
int2
The cow eats the cow.
("cow" "eats" "cow" "+")
int3
The cow is blue.
("cow" "is" "blue" "+")
int4
The bear eats the cow.
("bear" "eats" "cow" "+")
int5
The cow chases the cat.
("cow" "chases" "cat" "+")
((((((((((triple13) -> (rule3 % int6))) -> (rule2 % int5))) -> (rule4 % int4)) ((triple8) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The cow eats the cat.
("cow" "eats" "cat" "+")
int3
The cow eats the cow.
("cow" "eats" "cow" "+")
int4
The cow is blue.
("cow" "is" "blue" "+")
int5
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int6
((((((((((triple4) -> (rule3 % int6))) -> (rule2 % int5))) -> (rule4 % int4)) ((triple8) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule6 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The cow eats the cat.
("cow" "eats" "cat" "+")
int3
The cow eats the cow.
("cow" "eats" "cow" "+")
int4
The cow is blue.
("cow" "is" "blue" "+")
int5
The bear eats the cow.
("bear" "eats" "cow" "+")
int6