The bear chases the rabbit. The bear is big. The bear is blue. The bear is cold. The bear is green. The bear is kind. The bear needs the rabbit. The bear sees the rabbit. The rabbit chases the bear. The rabbit is big. The rabbit is blue. The rabbit is green. The rabbit is kind. The rabbit needs the bear. The rabbit sees the bear. If someone needs the bear and they see the bear then they need the rabbit. If someone sees the bear and they are kind then they chase the rabbit. If someone needs the bear and they see the rabbit then the bear chases the rabbit. If someone chases the bear then they are cold. If someone is cold and kind then they are big. If someone chases the bear and the bear chases the rabbit then the rabbit is kind. If someone chases the bear then the bear chases the rabbit. If someone is blue then they see the rabbit.
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The bear is big.
("bear" "is" "big" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is green.
("bear" "is" "green" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
If someone needs the bear and they see the bear then they need the rabbit.
((("someone" "needs" "bear" "+") ("someone" "sees" "bear" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone sees the bear and they are kind then they chase the rabbit.
((("someone" "sees" "bear" "+") ("someone" "is" "kind" "+")) -> ("someone" "chases" "rabbit" "+"))
If someone needs the bear and they see the rabbit then the bear chases the rabbit.
((("someone" "needs" "bear" "+") ("someone" "sees" "rabbit" "+")) -> ("bear" "chases" "rabbit" "+"))
If someone chases the bear then they are cold.
((("someone" "chases" "bear" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold and kind then they are big.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If someone chases the bear and the bear chases the rabbit then the rabbit is kind.
((("someone" "chases" "bear" "+") ("bear" "chases" "rabbit" "+")) -> ("rabbit" "is" "kind" "+"))
If someone chases the bear then the bear chases the rabbit.
((("someone" "chases" "bear" "+")) -> ("bear" "chases" "rabbit" "+"))
If someone is blue then they see the rabbit.
((("someone" "is" "blue" "+")) -> ("someone" "sees" "rabbit" "+"))
The rabbit is blue.
True
1
proof
[(triple11)]
("rabbit" "is" "blue" "+")
triple11
The bear is not blue.
False
1
inv-proof
[(triple3)]
("bear" "is" "blue" "-")
triple3
The rabbit needs the rabbit.
True
3
proof
[(((triple14 triple15) -> rule1))]
("rabbit" "needs" "rabbit" "+")
((triple14 triple15) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit does not chase the rabbit.
False
3
inv-proof
[(((triple15 triple13) -> rule2) OR ((triple15 ((triple9 triple1) -> rule6)) -> rule2) OR ((triple15 ((triple9 ((triple9) -> rule7)) -> rule6)) -> rule2) OR ((triple15 ((triple9 ((triple14 ((triple11) -> rule8)) -> rule3)) -> rule6)) -> rule2))]
("rabbit" "chases" "rabbit" "-")
((triple15 triple13) -> (rule2 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
((triple15 ((triple9 triple1) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
((triple15 ((triple9 ((triple9) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int3
((triple15 ((triple9 ((triple14 ((triple11) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int3
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int4
The bear does not chase the bear.
Unknown
inv-random
[@0: The bear chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "bear" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
@0: The bear chases the rabbit.[(triple1 OR ((triple9) -> rule7) OR ((triple14 ((triple11) -> rule8)) -> rule3))] The bear is big.[(triple2 OR ((triple4 triple6) -> rule5))] The bear is blue.[(triple3)] The bear is cold.[(triple4)] The bear is green.[(triple5)] The bear is kind.[(triple6)] The bear needs the rabbit.[(triple7)] The bear sees the rabbit.[(triple8 OR ((triple3) -> rule8))] The rabbit chases the bear.[(triple9)] The rabbit is big.[(triple10 OR ((((triple9) -> rule4) triple13) -> rule5) OR ((((triple9) -> rule4) ((triple9 triple1) -> rule6)) -> rule5) OR ((((triple9) -> rule4) ((triple9 ((triple9) -> rule7)) -> rule6)) -> rule5) OR ((((triple9) -> rule4) ((triple9 ((triple14 ((triple11) -> rule8)) -> rule3)) -> rule6)) -> rule5))] The rabbit is blue.[(triple11)] The rabbit is green.[(triple12)] The rabbit is kind.[(triple13 OR ((triple9 triple1) -> rule6) OR ((triple9 ((triple9) -> rule7)) -> rule6) OR ((triple9 ((triple14 ((triple11) -> rule8)) -> rule3)) -> rule6))] The rabbit needs the bear.[(triple14)] The rabbit sees the bear.[(triple15)] @1: The rabbit chases the rabbit.[(((triple15 triple13) -> rule2) OR ((triple15 ((triple9 triple1) -> rule6)) -> rule2) OR ((triple15 ((triple9 ((triple9) -> rule7)) -> rule6)) -> rule2) OR ((triple15 ((triple9 ((triple14 ((triple11) -> rule8)) -> rule3)) -> rule6)) -> rule2))] The rabbit is cold.[(((triple9) -> rule4))] The rabbit needs the rabbit.[(((triple14 triple15) -> rule1))] The rabbit sees the rabbit.[(((triple11) -> rule8))]
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple1
((triple9) -> (rule7 % int1))
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int1
((triple14 ((triple11) -> (rule8 % int2))) -> (rule3 % int1))
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int2
The bear is big.
("bear" "is" "big" "+")
triple2
((triple4 triple6) -> (rule5 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The bear is blue.
("bear" "is" "blue" "+")
triple3
The bear is cold.
("bear" "is" "cold" "+")
triple4
The bear is green.
("bear" "is" "green" "+")
triple5
The bear is kind.
("bear" "is" "kind" "+")
triple6
The bear needs the rabbit.
("bear" "needs" "rabbit" "+")
triple7
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple8
((triple3) -> (rule8 % int1))
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
int1
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple9
The rabbit is big.
("rabbit" "is" "big" "+")
triple10
((((triple9) -> (rule4 % int2)) triple13) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
((((triple9) -> (rule4 % int3)) ((triple9 triple1) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3
((((triple9) -> (rule4 % int4)) ((triple9 ((triple9) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int3
The rabbit is cold.
("rabbit" "is" "cold" "+")
int4
((((triple9) -> (rule4 % int5)) ((triple9 ((triple14 ((triple11) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int3
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int4
The rabbit is cold.
("rabbit" "is" "cold" "+")
int5
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple11
The rabbit is green.
("rabbit" "is" "green" "+")
triple12
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple13
((triple9 triple1) -> (rule6 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
((triple9 ((triple9) -> (rule7 % int2))) -> (rule6 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int2
((triple9 ((triple14 ((triple11) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int2
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int3
The rabbit needs the bear.
("rabbit" "needs" "bear" "+")
triple14
The rabbit sees the bear.
("rabbit" "sees" "bear" "+")
triple15
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((triple15 triple13) -> (rule2 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
((triple15 ((triple9 triple1) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
((triple15 ((triple9 ((triple9) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int3
((triple15 ((triple9 ((triple14 ((triple11) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
int3
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int4
The rabbit is cold.
("rabbit" "is" "cold" "+")
((triple9) -> (rule4 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple14 triple15) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((triple11) -> (rule8 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1