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