The bear does not chase the cat. The cat eats the bear. The cat eats the cow. The cat is blue. The cow does not eat the cat. The cow is not blue. The cow needs the bear. The rabbit chases the cat. The rabbit chases the cow. The rabbit eats the bear. The rabbit is red. The rabbit is young. If the rabbit is young then the rabbit needs the cow. If the bear chases the rabbit and the bear is young then the bear does not eat the rabbit. If someone needs the cow and the cow needs the bear then they chase the cow. If someone needs the cow then they chase the bear. If someone needs the cat then they eat the rabbit. If someone is nice then they need the cat. If someone chases the bear and they are red then they are nice. If someone is young then they are red. If someone needs the bear and they do not chase the bear then the bear eats the cow.
The bear does not chase the cat.
("bear" "chases" "cat" "-")
The cat eats the bear.
("cat" "eats" "bear" "+")
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cow does not eat the cat.
("cow" "eats" "cat" "-")
The cow is not blue.
("cow" "is" "blue" "-")
The cow needs the bear.
("cow" "needs" "bear" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
If the rabbit is young then the rabbit needs the cow.
((("rabbit" "is" "young" "+")) -> ("rabbit" "needs" "cow" "+"))
If the bear chases the rabbit and the bear is young then the bear does not eat the rabbit.
((("bear" "chases" "rabbit" "+") ("bear" "is" "young" "+")) -> ("bear" "eats" "rabbit" "-"))
If someone needs the cow and the cow needs the bear then they chase the cow.
((("someone" "needs" "cow" "+") ("cow" "needs" "bear" "+")) -> ("someone" "chases" "cow" "+"))
If someone needs the cow then they chase the bear.
((("someone" "needs" "cow" "+")) -> ("someone" "chases" "bear" "+"))
If someone needs the cat then they eat the rabbit.
((("someone" "needs" "cat" "+")) -> ("someone" "eats" "rabbit" "+"))
If someone is nice then they need the cat.
((("someone" "is" "nice" "+")) -> ("someone" "needs" "cat" "+"))
If someone chases the bear and they are red then they are nice.
((("someone" "chases" "bear" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If someone is young then they are red.
((("someone" "is" "young" "+")) -> ("someone" "is" "red" "+"))
If someone needs the bear and they do not chase the bear then the bear eats the cow.
((("someone" "needs" "bear" "+") ("someone" "chases" "bear" "~")) -> ("bear" "eats" "cow" "+"))
The cow is not blue.
True
1
proof
[(triple6)]
("cow" "is" "blue" "-")
triple6
The cat does not eat the cow.
False
1
inv-proof
[(triple3)]
("cat" "eats" "cow" "-")
triple3
The rabbit needs the cow.
True
2
proof
[(((triple12) -> rule1))]
("rabbit" "needs" "cow" "+")
((triple12) -> (rule1 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The rabbit does not need the cow.
False
2
inv-proof
[(((triple12) -> rule1))]
("rabbit" "needs" "cow" "-")
((triple12) -> (rule1 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The rabbit chases the bear.
True
3
proof
[(((((triple12) -> rule1)) -> rule4))]
("rabbit" "chases" "bear" "+")
((((triple12) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The rabbit does not chase the bear.
False
3
inv-proof
[(((((triple12) -> rule1)) -> rule4))]
("rabbit" "chases" "bear" "-")
((((triple12) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The rabbit is nice.
True
5
proof
[(((((((triple12) -> rule1)) -> rule4) triple11) -> rule7) OR ((((((triple12) -> rule1)) -> rule4) ((triple12) -> rule8)) -> rule7))]
("rabbit" "is" "nice" "+")
((((((triple12) -> (rule1 % int3))) -> (rule4 % int2)) triple11) -> (rule7 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int3
((((((triple12) -> (rule1 % int4))) -> (rule4 % int3)) ((triple12) -> (rule8 % int2))) -> (rule7 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int3
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int4
The rabbit is not nice.
False
5
inv-proof
[(((((((triple12) -> rule1)) -> rule4) triple11) -> rule7) OR ((((((triple12) -> rule1)) -> rule4) ((triple12) -> rule8)) -> rule7))]
("rabbit" "is" "nice" "-")
((((((triple12) -> (rule1 % int3))) -> (rule4 % int2)) triple11) -> (rule7 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int3
((((((triple12) -> (rule1 % int4))) -> (rule4 % int3)) ((triple12) -> (rule8 % int2))) -> (rule7 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int3
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int4
The rabbit needs the cat.
True
6
proof
[(((((((((triple12) -> rule1)) -> rule4) triple11) -> rule7)) -> rule6) OR ((((((((triple12) -> rule1)) -> rule4) ((triple12) -> rule8)) -> rule7)) -> rule6))]
("rabbit" "needs" "cat" "+")
((((((((triple12) -> (rule1 % int4))) -> (rule4 % int3)) triple11) -> (rule7 % int2))) -> (rule6 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int3
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int4
((((((((triple12) -> (rule1 % int5))) -> (rule4 % int4)) ((triple12) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int4
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int5
The rabbit does not need the cat.
False
6
inv-proof
[(((((((((triple12) -> rule1)) -> rule4) triple11) -> rule7)) -> rule6) OR ((((((((triple12) -> rule1)) -> rule4) ((triple12) -> rule8)) -> rule7)) -> rule6))]
("rabbit" "needs" "cat" "-")
((((((((triple12) -> (rule1 % int4))) -> (rule4 % int3)) triple11) -> (rule7 % int2))) -> (rule6 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int3
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int4
((((((((triple12) -> (rule1 % int5))) -> (rule4 % int4)) ((triple12) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int4
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int5
The rabbit eats the rabbit.
True
7
proof
[(((((((((((triple12) -> rule1)) -> rule4) triple11) -> rule7)) -> rule6)) -> rule5) OR ((((((((((triple12) -> rule1)) -> rule4) ((triple12) -> rule8)) -> rule7)) -> rule6)) -> rule5))]
("rabbit" "eats" "rabbit" "+")
((((((((((triple12) -> (rule1 % int5))) -> (rule4 % int4)) triple11) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int2
The rabbit is nice.
("rabbit" "is" "nice" "+")
int3
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int4
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int5
((((((((((triple12) -> (rule1 % int6))) -> (rule4 % int5)) ((triple12) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int2
The rabbit is nice.
("rabbit" "is" "nice" "+")
int3
The rabbit is red.
("rabbit" "is" "red" "+")
int4
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int5
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int6
The rabbit does not eat the rabbit.
False
7
inv-proof
[(((((((((((triple12) -> rule1)) -> rule4) triple11) -> rule7)) -> rule6)) -> rule5) OR ((((((((((triple12) -> rule1)) -> rule4) ((triple12) -> rule8)) -> rule7)) -> rule6)) -> rule5))]
("rabbit" "eats" "rabbit" "-")
((((((((((triple12) -> (rule1 % int5))) -> (rule4 % int4)) triple11) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int2
The rabbit is nice.
("rabbit" "is" "nice" "+")
int3
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int4
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int5
((((((((((triple12) -> (rule1 % int6))) -> (rule4 % int5)) ((triple12) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int2
The rabbit is nice.
("rabbit" "is" "nice" "+")
int3
The rabbit is red.
("rabbit" "is" "red" "+")
int4
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int5
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int6
The bear does not chase the cow.
Unknown
inv-rconc
[@1: The bear chases the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "chases" "cow" "-")
The cow needs the cat.
Unknown
rconc
[@3: The cow needs the cat.[CWA. Example of deepest failure = (rule6 <- rule7 <- rule4 <- FAIL)]]
("cow" "needs" "cat" "+")
The bear is not red.
Unknown
inv-rconc
[@1: The bear is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "is" "red" "-")
The cow is red.
Unknown
rconc
[@1: The cow is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "is" "red" "+")
The cow does not eat the rabbit.
Unknown
inv-rconc
[@4: The cow eats the rabbit.[CWA. Example of deepest failure = (rule5 <- rule6 <- rule7 <- rule4 <- FAIL)]]
("cow" "eats" "rabbit" "-")
The bear is nice.
Unknown
rconc
[@2: The bear is nice.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("bear" "is" "nice" "+")
The cat does not need the cow.
Unknown
inv-random
[@0: The cat needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cow" "-")
The bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
The rabbit does not eat the cat.
Unknown
inv-random
[@0: The rabbit eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "cat" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
The cow does not chase the rabbit.
Unknown
inv-random
[@0: The cow chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "rabbit" "-")
The bear is blue.
Unknown
random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "+")
@0: The bear does not chase the cat.[(triple1)] The cat eats the bear.[(triple2)] The cat eats the cow.[(triple3)] The cat is blue.[(triple4)] The cow does not eat the cat.[(triple5)] The cow is not blue.[(triple6)] The cow needs the bear.[(triple7)] The rabbit chases the cat.[(triple8)] The rabbit chases the cow.[(triple9 OR ((((triple12) -> rule1) triple7) -> rule3))] The rabbit eats the bear.[(triple10)] The rabbit is red.[(triple11 OR ((triple12) -> rule8))] The rabbit is young.[(triple12)] @1: The rabbit needs the cow.[(((triple12) -> rule1))] @2: The rabbit chases the bear.[(((((triple12) -> rule1)) -> rule4))] @3: The rabbit is nice.[(((((((triple12) -> rule1)) -> rule4) triple11) -> rule7) OR ((((((triple12) -> rule1)) -> rule4) ((triple12) -> rule8)) -> rule7))] @4: The rabbit needs the cat.[(((((((((triple12) -> rule1)) -> rule4) triple11) -> rule7)) -> rule6) OR ((((((((triple12) -> rule1)) -> rule4) ((triple12) -> rule8)) -> rule7)) -> rule6))] @5: The rabbit eats the rabbit.[(((((((((((triple12) -> rule1)) -> rule4) triple11) -> rule7)) -> rule6)) -> rule5) OR ((((((((((triple12) -> rule1)) -> rule4) ((triple12) -> rule8)) -> rule7)) -> rule6)) -> rule5))]
The bear does not chase the cat.
("bear" "chases" "cat" "-")
triple1
The cat eats the bear.
("cat" "eats" "bear" "+")
triple2
The cat eats the cow.
("cat" "eats" "cow" "+")
triple3
The cat is blue.
("cat" "is" "blue" "+")
triple4
The cow does not eat the cat.
("cow" "eats" "cat" "-")
triple5
The cow is not blue.
("cow" "is" "blue" "-")
triple6
The cow needs the bear.
("cow" "needs" "bear" "+")
triple7
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple8
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
triple9
((((triple12) -> (rule1 % int2)) triple7) -> (rule3 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
triple10
The rabbit is red.
("rabbit" "is" "red" "+")
triple11
((triple12) -> (rule8 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
triple12
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
((triple12) -> (rule1 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
((((triple12) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The rabbit is nice.
("rabbit" "is" "nice" "+")
((((((triple12) -> (rule1 % int3))) -> (rule4 % int2)) triple11) -> (rule7 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int2
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int3
((((((triple12) -> (rule1 % int4))) -> (rule4 % int3)) ((triple12) -> (rule8 % int2))) -> (rule7 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int3
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int4
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
((((((((triple12) -> (rule1 % int4))) -> (rule4 % int3)) triple11) -> (rule7 % int2))) -> (rule6 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int3
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int4
((((((((triple12) -> (rule1 % int5))) -> (rule4 % int4)) ((triple12) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int4
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int5
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((((((((((triple12) -> (rule1 % int5))) -> (rule4 % int4)) triple11) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int2
The rabbit is nice.
("rabbit" "is" "nice" "+")
int3
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int4
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int5
((((((((((triple12) -> (rule1 % int6))) -> (rule4 % int5)) ((triple12) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int2
The rabbit is nice.
("rabbit" "is" "nice" "+")
int3
The rabbit is red.
("rabbit" "is" "red" "+")
int4
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
int5
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int6