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