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