The dog is green. The dog is kind. The dog is nice. The dog needs the rabbit. The dog needs the squirrel. The rabbit is rough. The rabbit needs the dog. The rabbit sees the dog. The rabbit sees the squirrel. The squirrel is rough. The squirrel is round. The squirrel likes the dog. The squirrel likes the rabbit. The squirrel needs the rabbit. The squirrel sees the dog. If the dog does not like the rabbit then the dog needs the rabbit. If someone sees the dog and they are round then they see the squirrel. If someone sees the dog then the dog likes the squirrel. If someone is kind then they see the dog. If someone is rough and they like the rabbit then they see the dog. If someone needs the rabbit and the rabbit is kind then the rabbit sees the dog. If someone sees the squirrel then they need the squirrel. If someone needs the dog then the dog needs the squirrel.
The dog is green.
("dog" "is" "green" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
If the dog does not like the rabbit then the dog needs the rabbit.
((("dog" "likes" "rabbit" "~")) -> ("dog" "needs" "rabbit" "+"))
If someone sees the dog and they are round then they see the squirrel.
((("someone" "sees" "dog" "+") ("someone" "is" "round" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone sees the dog then the dog likes the squirrel.
((("someone" "sees" "dog" "+")) -> ("dog" "likes" "squirrel" "+"))
If someone is kind then they see the dog.
((("someone" "is" "kind" "+")) -> ("someone" "sees" "dog" "+"))
If someone is rough and they like the rabbit then they see the dog.
((("someone" "is" "rough" "+") ("someone" "likes" "rabbit" "+")) -> ("someone" "sees" "dog" "+"))
If someone needs the rabbit and the rabbit is kind then the rabbit sees the dog.
((("someone" "needs" "rabbit" "+") ("rabbit" "is" "kind" "+")) -> ("rabbit" "sees" "dog" "+"))
If someone sees the squirrel then they need the squirrel.
((("someone" "sees" "squirrel" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone needs the dog then the dog needs the squirrel.
((("someone" "needs" "dog" "+")) -> ("dog" "needs" "squirrel" "+"))
The squirrel likes the dog.
True
1
proof
[(triple12)]
("squirrel" "likes" "dog" "+")
triple12
The squirrel does not like the dog.
False
1
inv-proof
[(triple12)]
("squirrel" "likes" "dog" "-")
triple12
The squirrel sees the squirrel.
True
3
proof
[(((triple15 triple11) -> rule2) OR ((((triple10 triple13) -> rule5) triple11) -> rule2))]
("squirrel" "sees" "squirrel" "+")
((triple15 triple11) -> (rule2 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
((((triple10 triple13) -> (rule5 % int2)) triple11) -> (rule2 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int2
The squirrel does not see the squirrel.
False
3
inv-proof
[(((triple15 triple11) -> rule2) OR ((((triple10 triple13) -> rule5) triple11) -> rule2))]
("squirrel" "sees" "squirrel" "-")
((triple15 triple11) -> (rule2 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
((((triple10 triple13) -> (rule5 % int2)) triple11) -> (rule2 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int2
The squirrel needs the squirrel.
True
4
proof
[(((((triple15 triple11) -> rule2)) -> rule7) OR ((((((triple10 triple13) -> rule5) triple11) -> rule2)) -> rule7))]
("squirrel" "needs" "squirrel" "+")
((((triple15 triple11) -> (rule2 % int2))) -> (rule7 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
((((((triple10 triple13) -> (rule5 % int3)) triple11) -> (rule2 % int2))) -> (rule7 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int3
The squirrel does not need the squirrel.
False
4
inv-proof
[(((((triple15 triple11) -> rule2)) -> rule7) OR ((((((triple10 triple13) -> rule5) triple11) -> rule2)) -> rule7))]
("squirrel" "needs" "squirrel" "-")
((((triple15 triple11) -> (rule2 % int2))) -> (rule7 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
((((((triple10 triple13) -> (rule5 % int3)) triple11) -> (rule2 % int2))) -> (rule7 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int3
The dog does not see the squirrel.
Unknown
inv-rconc
[@1: The dog sees the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "sees" "squirrel" "-")
The rabbit likes the dog.
Unknown
random
[@0: The rabbit likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "dog" "+")
The rabbit does not like the squirrel.
Unknown
inv-random
[@0: The rabbit likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "squirrel" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
The squirrel does not need the dog.
Unknown
inv-random
[@0: The squirrel needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "dog" "-")
The dog is round.
Unknown
random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "+")
@0: The dog is green.[(triple1)] The dog is kind.[(triple2)] The dog is nice.[(triple3)] The dog needs the rabbit.[(triple4)] The dog needs the squirrel.[(triple5 OR ((triple7) -> rule8))] The rabbit is rough.[(triple6)] The rabbit needs the dog.[(triple7)] The rabbit sees the dog.[(triple8)] The rabbit sees the squirrel.[(triple9)] The squirrel is rough.[(triple10)] The squirrel is round.[(triple11)] The squirrel likes the dog.[(triple12)] The squirrel likes the rabbit.[(triple13)] The squirrel needs the rabbit.[(triple14)] The squirrel sees the dog.[(triple15 OR ((triple10 triple13) -> rule5))] @1: The dog likes the squirrel.[(((triple15) -> rule3) OR ((triple8) -> rule3) OR ((((triple2) -> rule4)) -> rule3) OR ((((triple10 triple13) -> rule5)) -> rule3))] The dog sees the dog.[(((triple2) -> rule4))] The rabbit needs the squirrel.[(((triple9) -> rule7))] The squirrel sees the squirrel.[(((triple15 triple11) -> rule2) OR ((((triple10 triple13) -> rule5) triple11) -> rule2))] @2: The squirrel needs the squirrel.[(((((triple15 triple11) -> rule2)) -> rule7) OR ((((((triple10 triple13) -> rule5) triple11) -> rule2)) -> rule7))]
The dog is green.
("dog" "is" "green" "+")
triple1
The dog is kind.
("dog" "is" "kind" "+")
triple2
The dog is nice.
("dog" "is" "nice" "+")
triple3
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple4
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
triple5
((triple7) -> (rule8 % int1))
The dog needs the squirrel.
("dog" "needs" "squirrel" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple6
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple7
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple8
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple9
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple10
The squirrel is round.
("squirrel" "is" "round" "+")
triple11
The squirrel likes the dog.
("squirrel" "likes" "dog" "+")
triple12
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
triple13
The squirrel needs the rabbit.
("squirrel" "needs" "rabbit" "+")
triple14
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
triple15
((triple10 triple13) -> (rule5 % int1))
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int1
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
((triple15) -> (rule3 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
((triple8) -> (rule3 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule3 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
int2
((((triple10 triple13) -> (rule5 % int2))) -> (rule3 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int2
The dog sees the dog.
("dog" "sees" "dog" "+")
((triple2) -> (rule4 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
((triple9) -> (rule7 % int1))
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((triple15 triple11) -> (rule2 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
((((triple10 triple13) -> (rule5 % int2)) triple11) -> (rule2 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int2
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((((triple15 triple11) -> (rule2 % int2))) -> (rule7 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
((((((triple10 triple13) -> (rule5 % int3)) triple11) -> (rule2 % int2))) -> (rule7 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int2
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int3