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