The bear chases the lion. The bear is big. The bear is cold. The bear is green. The bear is nice. The bear needs the lion. The bear visits the lion. The lion chases the bear. The lion is big. The lion is cold. The lion is green. The lion is nice. The lion is round. The lion needs the bear. The lion visits the bear. If something is nice and it needs the lion then the lion is nice. If something visits the lion and the lion is big then it chases the lion. If something needs the bear then it needs the lion. If something visits the bear then it is big. If something needs the bear and it chases the lion then the lion needs the bear. If something needs the bear and it is round then it chases the lion. If something chases the bear then the bear needs the lion. If something is cold then it needs the lion.
The bear chases the lion.
("bear" "chases" "lion" "+")
The bear is big.
("bear" "is" "big" "+")
The bear is cold.
("bear" "is" "cold" "+")
The bear is green.
("bear" "is" "green" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear needs the lion.
("bear" "needs" "lion" "+")
The bear visits the lion.
("bear" "visits" "lion" "+")
The lion chases the bear.
("lion" "chases" "bear" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is round.
("lion" "is" "round" "+")
The lion needs the bear.
("lion" "needs" "bear" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
If something is nice and it needs the lion then the lion is nice.
((("something" "is" "nice" "+") ("something" "needs" "lion" "+")) -> ("lion" "is" "nice" "+"))
If something visits the lion and the lion is big then it chases the lion.
((("something" "visits" "lion" "+") ("lion" "is" "big" "+")) -> ("something" "chases" "lion" "+"))
If something needs the bear then it needs the lion.
((("something" "needs" "bear" "+")) -> ("something" "needs" "lion" "+"))
If something visits the bear then it is big.
((("something" "visits" "bear" "+")) -> ("something" "is" "big" "+"))
If something needs the bear and it chases the lion then the lion needs the bear.
((("something" "needs" "bear" "+") ("something" "chases" "lion" "+")) -> ("lion" "needs" "bear" "+"))
If something needs the bear and it is round then it chases the lion.
((("something" "needs" "bear" "+") ("something" "is" "round" "+")) -> ("something" "chases" "lion" "+"))
If something chases the bear then the bear needs the lion.
((("something" "chases" "bear" "+")) -> ("bear" "needs" "lion" "+"))
If something is cold then it needs the lion.
((("something" "is" "cold" "+")) -> ("something" "needs" "lion" "+"))
The lion is nice.
True
1
proof
[(triple12 OR ((triple5 triple6) -> rule1) OR ((triple5 ((triple3) -> rule8)) -> rule1) OR ((triple5 ((triple8) -> rule7)) -> rule1))]
("lion" "is" "nice" "+")
triple12
((triple5 triple6) -> (rule1 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
((triple5 ((triple3) -> (rule8 % int2))) -> (rule1 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
((triple5 ((triple8) -> (rule7 % int2))) -> (rule1 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The lion is not big.
False
1
inv-proof
[(triple9 OR ((triple15) -> rule4))]
("lion" "is" "big" "-")
triple9
((triple15) -> (rule4 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion needs the lion.
True
2
proof
[(((triple10) -> rule8) OR ((triple14) -> rule3))]
("lion" "needs" "lion" "+")
((triple10) -> (rule8 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
((triple14) -> (rule3 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion does not need the lion.
False
2
inv-proof
[(((triple10) -> rule8) OR ((triple14) -> rule3))]
("lion" "needs" "lion" "-")
((triple10) -> (rule8 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
((triple14) -> (rule3 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
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 visits the bear.
Unknown
random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "+")
The bear is not round.
Unknown
inv-random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "-")
The bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
@0: The bear chases the lion.[(triple1 OR ((triple7 triple9) -> rule2) OR ((triple7 ((triple15) -> rule4)) -> rule2))] The bear is big.[(triple2)] The bear is cold.[(triple3)] The bear is green.[(triple4)] The bear is nice.[(triple5)] The bear needs the lion.[(triple6 OR ((triple3) -> rule8) OR ((triple8) -> rule7))] The bear visits the lion.[(triple7)] The lion chases the bear.[(triple8)] The lion is big.[(triple9 OR ((triple15) -> rule4))] The lion is cold.[(triple10)] The lion is green.[(triple11)] The lion is nice.[(triple12 OR ((triple5 triple6) -> rule1) OR ((triple5 ((triple3) -> rule8)) -> rule1) OR ((triple5 ((triple8) -> rule7)) -> rule1))] The lion is round.[(triple13)] The lion needs the bear.[(triple14)] The lion visits the bear.[(triple15)] @1: The lion chases the lion.[(((triple14 triple13) -> rule6))] The lion needs the lion.[(((triple10) -> rule8) OR ((triple14) -> rule3))]
The bear chases the lion.
("bear" "chases" "lion" "+")
triple1
((triple7 triple9) -> (rule2 % int1))
The bear chases the lion.
("bear" "chases" "lion" "+")
int1
((triple7 ((triple15) -> (rule4 % int2))) -> (rule2 % int1))
The bear chases the lion.
("bear" "chases" "lion" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The bear is big.
("bear" "is" "big" "+")
triple2
The bear is cold.
("bear" "is" "cold" "+")
triple3
The bear is green.
("bear" "is" "green" "+")
triple4
The bear is nice.
("bear" "is" "nice" "+")
triple5
The bear needs the lion.
("bear" "needs" "lion" "+")
triple6
((triple3) -> (rule8 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
((triple8) -> (rule7 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The bear visits the lion.
("bear" "visits" "lion" "+")
triple7
The lion chases the bear.
("lion" "chases" "bear" "+")
triple8
The lion is big.
("lion" "is" "big" "+")
triple9
((triple15) -> (rule4 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
triple10
The lion is green.
("lion" "is" "green" "+")
triple11
The lion is nice.
("lion" "is" "nice" "+")
triple12
((triple5 triple6) -> (rule1 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
((triple5 ((triple3) -> (rule8 % int2))) -> (rule1 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
((triple5 ((triple8) -> (rule7 % int2))) -> (rule1 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The lion is round.
("lion" "is" "round" "+")
triple13
The lion needs the bear.
("lion" "needs" "bear" "+")
triple14
The lion visits the bear.
("lion" "visits" "bear" "+")
triple15
The lion chases the lion.
("lion" "chases" "lion" "+")
((triple14 triple13) -> (rule6 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple10) -> (rule8 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
((triple14) -> (rule3 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1