The bear chases the rabbit. The dog is round. The rabbit chases the dog. The rabbit likes the tiger. The rabbit visits the bear. The tiger does not chase the dog. The tiger likes the dog. If the rabbit visits the dog and the dog does not chase the rabbit then the dog is big. If something visits the bear then the bear is not round.
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The dog is round.
("dog" "is" "round" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
The tiger does not chase the dog.
("tiger" "chases" "dog" "-")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
If the rabbit visits the dog and the dog does not chase the rabbit then the dog is big.
((("rabbit" "visits" "dog" "+") ("dog" "chases" "rabbit" "~")) -> ("dog" "is" "big" "+"))
If something visits the bear then the bear is not round.
((("something" "visits" "bear" "+")) -> ("bear" "is" "round" "-"))
The tiger likes the dog.
True
1
proof
[(triple7)]
("tiger" "likes" "dog" "+")
triple7
The tiger does not like the dog.
False
1
inv-proof
[(triple7)]
("tiger" "likes" "dog" "-")
triple7
The bear is not round.
True
2
proof
[(((triple5) -> rule2))]
("bear" "is" "round" "-")
((triple5) -> (rule2 % int1))
The bear is not round.
("bear" "is" "round" "-")
int1
The bear is round.
False
2
inv-proof
[(((triple5) -> rule2))]
("bear" "is" "round" "+")
((triple5) -> (rule2 % int1))
The bear is not round.
("bear" "is" "round" "-")
int1
The dog is not big.
Unknown
inv-rconc
[@1: The dog is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "big" "-")
The dog chases the tiger.
Unknown
random
[@0: The dog chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "tiger" "+")
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The rabbit likes the bear.
Unknown
random
[@0: The rabbit likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "bear" "+")
@0: The bear chases the rabbit.[(triple1)] The dog is round.[(triple2)] The rabbit chases the dog.[(triple3)] The rabbit likes the tiger.[(triple4)] The rabbit visits the bear.[(triple5)] The tiger does not chase the dog.[(triple6)] The tiger likes the dog.[(triple7)] @1: The bear is not round.[(((triple5) -> rule2))]
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple1
The dog is round.
("dog" "is" "round" "+")
triple2
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple3
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple4
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
triple5
The tiger does not chase the dog.
("tiger" "chases" "dog" "-")
triple6
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple7
The bear is not round.
("bear" "is" "round" "-")
((triple5) -> (rule2 % int1))
The bear is not round.
("bear" "is" "round" "-")
int1