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