The dog is not big. The dog likes the rabbit. The dog needs the rabbit. The dog sees the rabbit. The rabbit is not big. The rabbit is cold. The rabbit is round. The rabbit likes the dog. The rabbit needs the dog. The rabbit sees the dog. If something is big then it likes the rabbit. If something sees the rabbit and it likes the rabbit then the rabbit likes the dog. If something likes the dog and it is round then the dog is rough. If something is big and not round then it needs the dog. If something likes the dog and it likes the rabbit then the dog is young. If something is big and it does not like the dog then the dog needs the rabbit.
The dog is not big.
("dog" "is" "big" "-")
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 cold.
("rabbit" "is" "cold" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
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 something is big then it likes the rabbit.
((("something" "is" "big" "+")) -> ("something" "likes" "rabbit" "+"))
If something sees the rabbit and it likes the rabbit then the rabbit likes the dog.
((("something" "sees" "rabbit" "+") ("something" "likes" "rabbit" "+")) -> ("rabbit" "likes" "dog" "+"))
If something likes the dog and it is round then the dog is rough.
((("something" "likes" "dog" "+") ("something" "is" "round" "+")) -> ("dog" "is" "rough" "+"))
If something is big and not round then it needs the dog.
((("something" "is" "big" "+") ("something" "is" "round" "~")) -> ("something" "needs" "dog" "+"))
If something likes the dog and it likes the rabbit then the dog is young.
((("something" "likes" "dog" "+") ("something" "likes" "rabbit" "+")) -> ("dog" "is" "young" "+"))
If something is big and it does not like the dog then the dog needs the rabbit.
((("something" "is" "big" "+") ("something" "likes" "dog" "~")) -> ("dog" "needs" "rabbit" "+"))
The rabbit is cold.
True
1
proof
[(triple6)]
("rabbit" "is" "cold" "+")
triple6
The rabbit is not cold.
False
1
inv-proof
[(triple6)]
("rabbit" "is" "cold" "-")
triple6
The dog does not need the dog.
Unknown
inv-rconc
[@1: The dog needs the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "needs" "dog" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
@0: The dog is not big.[(triple1)] The dog likes the rabbit.[(triple2)] The dog needs the rabbit.[(triple3)] The dog sees the rabbit.[(triple4)] The rabbit is cold.[(triple6)] The rabbit is not big.[(triple5)] The rabbit is round.[(triple7)] The rabbit likes the dog.[(triple8 OR ((triple4 triple2) -> rule2))] The rabbit needs the dog.[(triple9)] The rabbit sees the dog.[(triple10)] @1: The dog is rough.[(((triple8 triple7) -> rule3) OR ((((triple4 triple2) -> rule2) triple7) -> rule3))]
The dog is not big.
("dog" "is" "big" "-")
triple1
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple2
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple3
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple4
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple6
The rabbit is not big.
("rabbit" "is" "big" "-")
triple5
The rabbit is round.
("rabbit" "is" "round" "+")
triple7
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple8
((triple4 triple2) -> (rule2 % int1))
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple9
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple10
The dog is rough.
("dog" "is" "rough" "+")
((triple8 triple7) -> (rule3 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
((((triple4 triple2) -> (rule2 % int2)) triple7) -> (rule3 % int1))
The dog is rough.
("dog" "is" "rough" "+")
int1
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int2