The dog is blue. The dog is cold. The dog is green. The dog is rough. The dog is young. The dog likes the rabbit. The dog does not need the rabbit. The dog sees the rabbit. The rabbit is not blue. The rabbit is cold. The rabbit is rough. The rabbit is not young. The rabbit likes the dog. The rabbit needs the dog. The rabbit does not see the dog. If something needs the dog then it is rough. If the dog needs the rabbit then the rabbit sees the dog. If something is young and it does not see the rabbit then it does not see the dog. If something likes the dog then it needs the rabbit. If something is green and it likes the dog then it does not need the rabbit. If the dog needs the rabbit then the dog likes the rabbit. If the dog is blue then the dog likes the rabbit. If something is cold and it does not see the dog then the dog likes the rabbit.
The dog is blue.
("dog" "is" "blue" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog is young.
("dog" "is" "young" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The dog does not need the rabbit.
("dog" "needs" "rabbit" "-")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The rabbit is not blue.
("rabbit" "is" "blue" "-")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is not young.
("rabbit" "is" "young" "-")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit does not see the dog.
("rabbit" "sees" "dog" "-")
If something needs the dog then it is rough.
((("something" "needs" "dog" "+")) -> ("something" "is" "rough" "+"))
If the dog needs the rabbit then the rabbit sees the dog.
((("dog" "needs" "rabbit" "+")) -> ("rabbit" "sees" "dog" "+"))
If something is young and it does not see the rabbit then it does not see the dog.
((("something" "is" "young" "+") ("something" "sees" "rabbit" "~")) -> ("something" "sees" "dog" "-"))
If something likes the dog then it needs the rabbit.
((("something" "likes" "dog" "+")) -> ("something" "needs" "rabbit" "+"))
If something is green and it likes the dog then it does not need the rabbit.
((("something" "is" "green" "+") ("something" "likes" "dog" "+")) -> ("something" "needs" "rabbit" "-"))
If the dog needs the rabbit then the dog likes the rabbit.
((("dog" "needs" "rabbit" "+")) -> ("dog" "likes" "rabbit" "+"))
If the dog is blue then the dog likes the rabbit.
((("dog" "is" "blue" "+")) -> ("dog" "likes" "rabbit" "+"))
If something is cold and it does not see the dog then the dog likes the rabbit.
((("something" "is" "cold" "+") ("something" "sees" "dog" "~")) -> ("dog" "likes" "rabbit" "+"))
The rabbit is not young.
True
1
proof
[(triple12)]
("rabbit" "is" "young" "-")
triple12
The dog is not cold.
False
1
inv-proof
[(triple2)]
("dog" "is" "cold" "-")
triple2
The rabbit needs the rabbit.
True
2
proof
[(((triple13) -> rule4))]
("rabbit" "needs" "rabbit" "+")
((triple13) -> (rule4 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit does not need the rabbit.
False
2
inv-proof
[(((triple13) -> rule4))]
("rabbit" "needs" "rabbit" "-")
((triple13) -> (rule4 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
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 like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
The rabbit is green.
Unknown
random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "+")
@0: The dog does not need the rabbit.[(triple7)] The dog is blue.[(triple1)] The dog is cold.[(triple2)] The dog is green.[(triple3)] The dog is rough.[(triple4)] The dog is young.[(triple5)] The dog likes the rabbit.[(triple6 OR ((triple1) -> rule7) OR ((triple10 triple15) -> rule8))] The dog sees the rabbit.[(triple8)] The rabbit does not see the dog.[(triple15)] The rabbit is cold.[(triple10)] The rabbit is not blue.[(triple9)] The rabbit is not young.[(triple12)] The rabbit is rough.[(triple11 OR ((triple14) -> rule1))] The rabbit likes the dog.[(triple13)] The rabbit needs the dog.[(triple14)] @1: The rabbit needs the rabbit.[(((triple13) -> rule4))]
The dog does not need the rabbit.
("dog" "needs" "rabbit" "-")
triple7
The dog is blue.
("dog" "is" "blue" "+")
triple1
The dog is cold.
("dog" "is" "cold" "+")
triple2
The dog is green.
("dog" "is" "green" "+")
triple3
The dog is rough.
("dog" "is" "rough" "+")
triple4
The dog is young.
("dog" "is" "young" "+")
triple5
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple6
((triple1) -> (rule7 % int1))
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int1
((triple10 triple15) -> (rule8 % int1))
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple8
The rabbit does not see the dog.
("rabbit" "sees" "dog" "-")
triple15
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple10
The rabbit is not blue.
("rabbit" "is" "blue" "-")
triple9
The rabbit is not young.
("rabbit" "is" "young" "-")
triple12
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple11
((triple14) -> (rule1 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple13
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple14
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple13) -> (rule4 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1