The dog is not big. The dog is blue. The dog is cold. The dog is round. The dog is young. The dog likes the rabbit. The dog needs the rabbit. The dog sees the rabbit. The rabbit is not big. The rabbit is not blue. The rabbit is cold. The rabbit is round. The rabbit is young. The rabbit likes the dog. The rabbit needs the dog. The rabbit sees the dog. If someone likes the dog and they need the rabbit then the dog needs the rabbit. If someone likes the rabbit then the rabbit needs the dog.
The dog is not big.
("dog" "is" "big" "-")
The dog is blue.
("dog" "is" "blue" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is round.
("dog" "is" "round" "+")
The dog is young.
("dog" "is" "young" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The rabbit is not big.
("rabbit" "is" "big" "-")
The rabbit is not blue.
("rabbit" "is" "blue" "-")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
If someone likes the dog and they need the rabbit then the dog needs the rabbit.
((("someone" "likes" "dog" "+") ("someone" "needs" "rabbit" "+")) -> ("dog" "needs" "rabbit" "+"))
If someone likes the rabbit then the rabbit needs the dog.
((("someone" "likes" "rabbit" "+")) -> ("rabbit" "needs" "dog" "+"))
The dog sees the rabbit.
True
1
proof
[(triple8)]
("dog" "sees" "rabbit" "+")
triple8
The dog is not blue.
False
1
inv-proof
[(triple2)]
("dog" "is" "blue" "-")
triple2
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
@0: The dog is blue.[(triple2)] The dog is cold.[(triple3)] The dog is not big.[(triple1)] The dog is round.[(triple4)] The dog is young.[(triple5)] The dog likes the rabbit.[(triple6)] The dog needs the rabbit.[(triple7)] The dog sees the rabbit.[(triple8)] The rabbit is cold.[(triple11)] The rabbit is not big.[(triple9)] The rabbit is not blue.[(triple10)] The rabbit is round.[(triple12)] The rabbit is young.[(triple13)] The rabbit likes the dog.[(triple14)] The rabbit needs the dog.[(triple15 OR ((triple6) -> rule2))] The rabbit sees the dog.[(triple16)]
The dog is blue.
("dog" "is" "blue" "+")
triple2
The dog is cold.
("dog" "is" "cold" "+")
triple3
The dog is not big.
("dog" "is" "big" "-")
triple1
The dog is round.
("dog" "is" "round" "+")
triple4
The dog is young.
("dog" "is" "young" "+")
triple5
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple6
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple7
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple8
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple11
The rabbit is not big.
("rabbit" "is" "big" "-")
triple9
The rabbit is not blue.
("rabbit" "is" "blue" "-")
triple10
The rabbit is round.
("rabbit" "is" "round" "+")
triple12
The rabbit is young.
("rabbit" "is" "young" "+")
triple13
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple14
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple15
((triple6) -> (rule2 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple16