The bear is big. The bear is blue. The bear needs the lion. The bear visits the lion. The bear visits the squirrel. The lion eats the bear. The lion eats the squirrel. The lion is big. The lion is rough. The lion needs the squirrel. The lion visits the squirrel. The squirrel eats the bear. The squirrel is blue. The squirrel is rough. The squirrel needs the lion. If the lion visits the bear then the bear is green. If something needs the squirrel and the squirrel is green then it eats the bear. If something visits the bear and the bear is big then it is red. If something eats the squirrel and the squirrel needs the lion then the lion visits the bear. If something is blue then it visits the lion. If the lion needs the squirrel and the lion eats the bear then the bear needs the squirrel. If something visits the lion then the lion needs the bear. If something is rough then it visits the lion.
The bear is big.
("bear" "is" "big" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear needs the lion.
("bear" "needs" "lion" "+")
The bear visits the lion.
("bear" "visits" "lion" "+")
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
The lion eats the bear.
("lion" "eats" "bear" "+")
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
If the lion visits the bear then the bear is green.
((("lion" "visits" "bear" "+")) -> ("bear" "is" "green" "+"))
If something needs the squirrel and the squirrel is green then it eats the bear.
((("something" "needs" "squirrel" "+") ("squirrel" "is" "green" "+")) -> ("something" "eats" "bear" "+"))
If something visits the bear and the bear is big then it is red.
((("something" "visits" "bear" "+") ("bear" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something eats the squirrel and the squirrel needs the lion then the lion visits the bear.
((("something" "eats" "squirrel" "+") ("squirrel" "needs" "lion" "+")) -> ("lion" "visits" "bear" "+"))
If something is blue then it visits the lion.
((("something" "is" "blue" "+")) -> ("something" "visits" "lion" "+"))
If the lion needs the squirrel and the lion eats the bear then the bear needs the squirrel.
((("lion" "needs" "squirrel" "+") ("lion" "eats" "bear" "+")) -> ("bear" "needs" "squirrel" "+"))
If something visits the lion then the lion needs the bear.
((("something" "visits" "lion" "+")) -> ("lion" "needs" "bear" "+"))
If something is rough then it visits the lion.
((("something" "is" "rough" "+")) -> ("something" "visits" "lion" "+"))
The squirrel needs the lion.
True
1
proof
[(triple15)]
("squirrel" "needs" "lion" "+")
triple15
The bear is not big.
False
1
inv-proof
[(triple1)]
("bear" "is" "big" "-")
triple1
The bear does not eat the bear.
Unknown
inv-rconc
[@1: The bear eats the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "eats" "bear" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
@0: The bear is big.[(triple1)] The bear is blue.[(triple2)] The bear needs the lion.[(triple3)] The bear visits the lion.[(triple4 OR ((triple2) -> rule5))] The bear visits the squirrel.[(triple5)] The lion eats the bear.[(triple6)] The lion eats the squirrel.[(triple7)] The lion is big.[(triple8)] The lion is rough.[(triple9)] The lion needs the squirrel.[(triple10)] The lion visits the squirrel.[(triple11)] The squirrel eats the bear.[(triple12)] The squirrel is blue.[(triple13)] The squirrel is rough.[(triple14)] The squirrel needs the lion.[(triple15)] @1: The bear needs the squirrel.[(((triple10 triple6) -> rule6))] The lion needs the bear.[(((triple4) -> rule7) OR ((((triple13) -> rule5)) -> rule7) OR ((((triple14) -> rule8)) -> rule7) OR ((((triple2) -> rule5)) -> rule7) OR ((((triple9) -> rule8)) -> rule7))] The lion visits the bear.[(((triple7 triple15) -> rule4))] The lion visits the lion.[(((triple9) -> rule8))] The squirrel visits the lion.[(((triple13) -> rule5) OR ((triple14) -> rule8))] @2: The bear is green.[(((((triple7 triple15) -> rule4)) -> rule1))] The lion is red.[(((((triple7 triple15) -> rule4) triple1) -> rule3))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear is blue.
("bear" "is" "blue" "+")
triple2
The bear needs the lion.
("bear" "needs" "lion" "+")
triple3
The bear visits the lion.
("bear" "visits" "lion" "+")
triple4
((triple2) -> (rule5 % int1))
The bear visits the lion.
("bear" "visits" "lion" "+")
int1
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
triple5
The lion eats the bear.
("lion" "eats" "bear" "+")
triple6
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple7
The lion is big.
("lion" "is" "big" "+")
triple8
The lion is rough.
("lion" "is" "rough" "+")
triple9
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
triple10
The lion visits the squirrel.
("lion" "visits" "squirrel" "+")
triple11
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
triple12
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple13
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple14
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple15
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
((triple10 triple6) -> (rule6 % int1))
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
int1
The lion needs the bear.
("lion" "needs" "bear" "+")
((triple4) -> (rule7 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
((((triple13) -> (rule5 % int2))) -> (rule7 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int2
((((triple14) -> (rule8 % int2))) -> (rule7 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int2
((((triple2) -> (rule5 % int2))) -> (rule7 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The bear visits the lion.
("bear" "visits" "lion" "+")
int2
((((triple9) -> (rule8 % int2))) -> (rule7 % int1))
The lion needs the bear.
("lion" "needs" "bear" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
int2
The lion visits the bear.
("lion" "visits" "bear" "+")
((triple7 triple15) -> (rule4 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
((triple9) -> (rule8 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
((triple13) -> (rule5 % int1))
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int1
((triple14) -> (rule8 % int1))
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int1
The bear is green.
("bear" "is" "green" "+")
((((triple7 triple15) -> (rule4 % int2))) -> (rule1 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The lion visits the bear.
("lion" "visits" "bear" "+")
int2
The lion is red.
("lion" "is" "red" "+")
((((triple7 triple15) -> (rule4 % int2)) triple1) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion visits the bear.
("lion" "visits" "bear" "+")
int2