The bear is big. The bear likes the dog. The bear likes the squirrel. The bear needs the squirrel. The dog eats the squirrel. The dog likes the bear. The dog likes the squirrel. The dog needs the bear. The squirrel is big. The squirrel is green. The squirrel is rough. The squirrel needs the bear. If someone needs the bear and the bear needs the squirrel then they eat the bear. If someone likes the dog then the dog eats the squirrel. If the bear likes the dog and the bear likes the squirrel then the bear is kind. If someone is nice and kind then they like the bear. If someone needs the bear then they eat the bear. If someone likes the bear then the bear likes the squirrel. If someone eats the bear then they eat the squirrel. If the squirrel likes the bear and the bear eats the squirrel then the squirrel is big.
The bear is big.
("bear" "is" "big" "+")
The bear likes the dog.
("bear" "likes" "dog" "+")
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
The dog likes the bear.
("dog" "likes" "bear" "+")
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
The dog needs the bear.
("dog" "needs" "bear" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
If someone needs the bear and the bear needs the squirrel then they eat the bear.
((("someone" "needs" "bear" "+") ("bear" "needs" "squirrel" "+")) -> ("someone" "eats" "bear" "+"))
If someone likes the dog then the dog eats the squirrel.
((("someone" "likes" "dog" "+")) -> ("dog" "eats" "squirrel" "+"))
If the bear likes the dog and the bear likes the squirrel then the bear is kind.
((("bear" "likes" "dog" "+") ("bear" "likes" "squirrel" "+")) -> ("bear" "is" "kind" "+"))
If someone is nice and kind then they like the bear.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "likes" "bear" "+"))
If someone needs the bear then they eat the bear.
((("someone" "needs" "bear" "+")) -> ("someone" "eats" "bear" "+"))
If someone likes the bear then the bear likes the squirrel.
((("someone" "likes" "bear" "+")) -> ("bear" "likes" "squirrel" "+"))
If someone eats the bear then they eat the squirrel.
((("someone" "eats" "bear" "+")) -> ("someone" "eats" "squirrel" "+"))
If the squirrel likes the bear and the bear eats the squirrel then the squirrel is big.
((("squirrel" "likes" "bear" "+") ("bear" "eats" "squirrel" "+")) -> ("squirrel" "is" "big" "+"))
The dog eats the squirrel.
True
1
proof
[(triple5 OR ((triple2) -> rule2) OR ((((triple8) -> rule5)) -> rule7) OR ((((triple8 triple4) -> rule1)) -> rule7))]
("dog" "eats" "squirrel" "+")
triple5
((triple2) -> (rule2 % int1))
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int1
((((triple8) -> (rule5 % int2))) -> (rule7 % int1))
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int1
The dog eats the bear.
("dog" "eats" "bear" "+")
int2
((((triple8 triple4) -> (rule1 % int2))) -> (rule7 % int1))
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int1
The dog eats the bear.
("dog" "eats" "bear" "+")
int2
The squirrel is not big.
False
1
inv-proof
[(triple9)]
("squirrel" "is" "big" "-")
triple9
The bear is kind.
True
3
proof
[(((triple2 triple3) -> rule3) OR ((triple2 ((triple6) -> rule6)) -> rule3))]
("bear" "is" "kind" "+")
((triple2 triple3) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
((triple2 ((triple6) -> (rule6 % int2))) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2
The bear is not kind.
False
3
inv-proof
[(((triple2 triple3) -> rule3) OR ((triple2 ((triple6) -> rule6)) -> rule3))]
("bear" "is" "kind" "-")
((triple2 triple3) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
((triple2 ((triple6) -> (rule6 % int2))) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2
The squirrel eats the squirrel.
True
3
proof
[(((((triple12) -> rule5)) -> rule7) OR ((((triple12 triple4) -> rule1)) -> rule7))]
("squirrel" "eats" "squirrel" "+")
((((triple12) -> (rule5 % int2))) -> (rule7 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int2
((((triple12 triple4) -> (rule1 % int2))) -> (rule7 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int2
The squirrel does not eat the squirrel.
False
3
inv-proof
[(((((triple12) -> rule5)) -> rule7) OR ((((triple12 triple4) -> rule1)) -> rule7))]
("squirrel" "eats" "squirrel" "-")
((((triple12) -> (rule5 % int2))) -> (rule7 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int2
((((triple12 triple4) -> (rule1 % int2))) -> (rule7 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int2
The squirrel does not like the bear.
Unknown
inv-rconc
[@1: The squirrel likes the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "likes" "bear" "-")
The bear likes the bear.
Unknown
rconc
[@1: The bear likes the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "likes" "bear" "+")
The bear does not eat the squirrel.
Unknown
inv-rconc
[@2: The bear eats the squirrel.[CWA. Example of deepest failure = (rule7 <- rule1 <- FAIL)]]
("bear" "eats" "squirrel" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
The dog is not rough.
Unknown
inv-random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "-")
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 is big.[(triple1)] The bear likes the dog.[(triple2)] The bear likes the squirrel.[(triple3 OR ((triple6) -> rule6))] The bear needs the squirrel.[(triple4)] The dog eats the squirrel.[(triple5 OR ((triple2) -> rule2) OR ((((triple8) -> rule5)) -> rule7) OR ((((triple8 triple4) -> rule1)) -> rule7))] The dog likes the bear.[(triple6)] The dog likes the squirrel.[(triple7)] The dog needs the bear.[(triple8)] The squirrel is big.[(triple9)] The squirrel is green.[(triple10)] The squirrel is rough.[(triple11)] The squirrel needs the bear.[(triple12)] @1: The bear is kind.[(((triple2 triple3) -> rule3) OR ((triple2 ((triple6) -> rule6)) -> rule3))] The dog eats the bear.[(((triple8) -> rule5) OR ((triple8 triple4) -> rule1))] The squirrel eats the bear.[(((triple12) -> rule5) OR ((triple12 triple4) -> rule1))] @2: The squirrel eats the squirrel.[(((((triple12) -> rule5)) -> rule7) OR ((((triple12 triple4) -> rule1)) -> rule7))]
The bear is big.
("bear" "is" "big" "+")
triple1
The bear likes the dog.
("bear" "likes" "dog" "+")
triple2
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
triple3
((triple6) -> (rule6 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The bear needs the squirrel.
("bear" "needs" "squirrel" "+")
triple4
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
triple5
((triple2) -> (rule2 % int1))
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int1
((((triple8) -> (rule5 % int2))) -> (rule7 % int1))
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int1
The dog eats the bear.
("dog" "eats" "bear" "+")
int2
((((triple8 triple4) -> (rule1 % int2))) -> (rule7 % int1))
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int1
The dog eats the bear.
("dog" "eats" "bear" "+")
int2
The dog likes the bear.
("dog" "likes" "bear" "+")
triple6
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
triple7
The dog needs the bear.
("dog" "needs" "bear" "+")
triple8
The squirrel is big.
("squirrel" "is" "big" "+")
triple9
The squirrel is green.
("squirrel" "is" "green" "+")
triple10
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple11
The squirrel needs the bear.
("squirrel" "needs" "bear" "+")
triple12
The bear is kind.
("bear" "is" "kind" "+")
((triple2 triple3) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
((triple2 ((triple6) -> (rule6 % int2))) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int2
The dog eats the bear.
("dog" "eats" "bear" "+")
((triple8) -> (rule5 % int1))
The dog eats the bear.
("dog" "eats" "bear" "+")
int1
((triple8 triple4) -> (rule1 % int1))
The dog eats the bear.
("dog" "eats" "bear" "+")
int1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
((triple12) -> (rule5 % int1))
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int1
((triple12 triple4) -> (rule1 % int1))
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((((triple12) -> (rule5 % int2))) -> (rule7 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int2
((((triple12 triple4) -> (rule1 % int2))) -> (rule7 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int2