The bear chases the dog. The bear is young. The bear needs the dog. The dog is young. The dog needs the tiger. The rabbit chases the bear. The rabbit is nice. The tiger chases the dog. The tiger is young. The tiger visits the bear. The tiger visits the dog. The tiger visits the rabbit. If someone is young then they are nice. If someone needs the bear then the bear chases the rabbit. If someone needs the dog and the dog is round then the dog chases the rabbit.
The bear chases the dog.
("bear" "chases" "dog" "+")
The bear is young.
("bear" "is" "young" "+")
The bear needs the dog.
("bear" "needs" "dog" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If someone is young then they are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
If someone needs the bear then the bear chases the rabbit.
((("someone" "needs" "bear" "+")) -> ("bear" "chases" "rabbit" "+"))
If someone needs the dog and the dog is round then the dog chases the rabbit.
((("someone" "needs" "dog" "+") ("dog" "is" "round" "+")) -> ("dog" "chases" "rabbit" "+"))
The tiger is young.
True
1
proof
[(triple9)]
("tiger" "is" "young" "+")
triple9
The bear does not need the dog.
False
1
inv-proof
[(triple3)]
("bear" "needs" "dog" "-")
triple3
The bear is nice.
True
2
proof
[(((triple2) -> rule1))]
("bear" "is" "nice" "+")
((triple2) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The dog is not nice.
False
2
inv-proof
[(((triple4) -> rule1))]
("dog" "is" "nice" "-")
((triple4) -> (rule1 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog does not chase the rabbit.
Unknown
inv-rconc
[@1: The dog chases the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "chases" "rabbit" "-")
The bear chases the rabbit.
Unknown
rconc
[@1: The bear chases the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "chases" "rabbit" "+")
The rabbit is not young.
Unknown
inv-random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "young" "-")
The rabbit needs the tiger.
Unknown
random
[@0: The rabbit needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "tiger" "+")
@0: The bear chases the dog.[(triple1)] The bear is young.[(triple2)] The bear needs the dog.[(triple3)] The dog is young.[(triple4)] The dog needs the tiger.[(triple5)] The rabbit chases the bear.[(triple6)] The rabbit is nice.[(triple7)] The tiger chases the dog.[(triple8)] The tiger is young.[(triple9)] The tiger visits the bear.[(triple10)] The tiger visits the dog.[(triple11)] The tiger visits the rabbit.[(triple12)] @1: The bear is nice.[(((triple2) -> rule1))] The dog is nice.[(((triple4) -> rule1))] The tiger is nice.[(((triple9) -> rule1))]
The bear chases the dog.
("bear" "chases" "dog" "+")
triple1
The bear is young.
("bear" "is" "young" "+")
triple2
The bear needs the dog.
("bear" "needs" "dog" "+")
triple3
The dog is young.
("dog" "is" "young" "+")
triple4
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple5
The rabbit chases the bear.
("rabbit" "chases" "bear" "+")
triple6
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple7
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple8
The tiger is young.
("tiger" "is" "young" "+")
triple9
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple10
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple11
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple12
The bear is nice.
("bear" "is" "nice" "+")
((triple2) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
((triple4) -> (rule1 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
((triple9) -> (rule1 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1