The dog is not blue. The dog likes the rabbit. The dog sees the rabbit. The dog visits the rabbit. The rabbit is big. The rabbit is kind. The rabbit is round. The rabbit likes the squirrel. The rabbit sees the dog. The rabbit sees the squirrel. The squirrel is not big. The squirrel is not round. The squirrel does not like the dog. The squirrel sees the dog. The squirrel sees the rabbit. The squirrel does not visit the rabbit. If someone sees the rabbit and they visit the rabbit then the rabbit sees the squirrel. If someone likes the squirrel and they are rough then the squirrel does not see the rabbit. If the dog likes the squirrel and the dog is not blue then the squirrel is not kind. If the squirrel visits the rabbit and the squirrel visits the dog then the rabbit sees the dog. If someone sees the squirrel and they are kind then the squirrel does not like the dog. If someone likes the rabbit and the rabbit is round then the rabbit visits the dog.
The dog is not blue.
("dog" "is" "blue" "-")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
The squirrel is not big.
("squirrel" "is" "big" "-")
The squirrel is not round.
("squirrel" "is" "round" "-")
The squirrel does not like the dog.
("squirrel" "likes" "dog" "-")
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
The squirrel does not visit the rabbit.
("squirrel" "visits" "rabbit" "-")
If someone sees the rabbit and they visit the rabbit then the rabbit sees the squirrel.
((("someone" "sees" "rabbit" "+") ("someone" "visits" "rabbit" "+")) -> ("rabbit" "sees" "squirrel" "+"))
If someone likes the squirrel and they are rough then the squirrel does not see the rabbit.
((("someone" "likes" "squirrel" "+") ("someone" "is" "rough" "+")) -> ("squirrel" "sees" "rabbit" "-"))
If the dog likes the squirrel and the dog is not blue then the squirrel is not kind.
((("dog" "likes" "squirrel" "+") ("dog" "is" "blue" "~")) -> ("squirrel" "is" "kind" "-"))
If the squirrel visits the rabbit and the squirrel visits the dog then the rabbit sees the dog.
((("squirrel" "visits" "rabbit" "+") ("squirrel" "visits" "dog" "+")) -> ("rabbit" "sees" "dog" "+"))
If someone sees the squirrel and they are kind then the squirrel does not like the dog.
((("someone" "sees" "squirrel" "+") ("someone" "is" "kind" "+")) -> ("squirrel" "likes" "dog" "-"))
If someone likes the rabbit and the rabbit is round then the rabbit visits the dog.
((("someone" "likes" "rabbit" "+") ("rabbit" "is" "round" "+")) -> ("rabbit" "visits" "dog" "+"))
The dog sees the rabbit.
True
1
proof
[(triple3)]
("dog" "sees" "rabbit" "+")
triple3
The squirrel is round.
False
1
inv-proof
[(triple12)]
("squirrel" "is" "round" "+")
triple12
The rabbit visits the dog.
True
3
proof
[(((triple2 triple7) -> rule6))]
("rabbit" "visits" "dog" "+")
((triple2 triple7) -> (rule6 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The rabbit does not visit the dog.
False
3
inv-proof
[(((triple2 triple7) -> rule6))]
("rabbit" "visits" "dog" "-")
((triple2 triple7) -> (rule6 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1
The rabbit does not like the dog.
Unknown
inv-random
[@0: The rabbit likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "dog" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
The rabbit does not visit the squirrel.
Unknown
inv-random
[@0: The rabbit visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "squirrel" "-")
The dog is big.
Unknown
random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "+")
@0: The dog is not blue.[(triple1)] The dog likes the rabbit.[(triple2)] The dog sees the rabbit.[(triple3)] The dog visits the rabbit.[(triple4)] The rabbit is big.[(triple5)] The rabbit is kind.[(triple6)] The rabbit is round.[(triple7)] The rabbit likes the squirrel.[(triple8)] The rabbit sees the dog.[(triple9)] The rabbit sees the squirrel.[(triple10 OR ((triple3 triple4) -> rule1))] The squirrel does not like the dog.[(triple13 OR ((triple10 triple6) -> rule5) OR ((((triple3 triple4) -> rule1) triple6) -> rule5))] The squirrel does not visit the rabbit.[(triple16)] The squirrel is not big.[(triple11)] The squirrel is not round.[(triple12)] The squirrel sees the dog.[(triple14)] The squirrel sees the rabbit.[(triple15)] @1: The rabbit visits the dog.[(((triple2 triple7) -> rule6))]
The dog is not blue.
("dog" "is" "blue" "-")
triple1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple2
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple3
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple4
The rabbit is big.
("rabbit" "is" "big" "+")
triple5
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple6
The rabbit is round.
("rabbit" "is" "round" "+")
triple7
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
triple8
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple9
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
triple10
((triple3 triple4) -> (rule1 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The squirrel does not like the dog.
("squirrel" "likes" "dog" "-")
triple13
((triple10 triple6) -> (rule5 % int1))
The squirrel does not like the dog.
("squirrel" "likes" "dog" "-")
int1
((((triple3 triple4) -> (rule1 % int2)) triple6) -> (rule5 % int1))
The squirrel does not like the dog.
("squirrel" "likes" "dog" "-")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
The squirrel does not visit the rabbit.
("squirrel" "visits" "rabbit" "-")
triple16
The squirrel is not big.
("squirrel" "is" "big" "-")
triple11
The squirrel is not round.
("squirrel" "is" "round" "-")
triple12
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
triple14
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple15
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
((triple2 triple7) -> (rule6 % int1))
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
int1