The dog chases the tiger. The dog is cold. The dog is round. The dog is young. The dog needs the rabbit. The dog does not visit the rabbit. The dog visits the tiger. The rabbit chases the tiger. The rabbit is cold. The rabbit is round. The rabbit is not young. The rabbit visits the dog. The rabbit visits the tiger. The tiger chases the dog. The tiger needs the rabbit. If something needs the tiger and it does not visit the dog then the tiger is red. If something needs the tiger and the tiger needs the dog then the tiger is red. If something chases the dog then the dog chases the rabbit.
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is round.
("dog" "is" "round" "+")
The dog is young.
("dog" "is" "young" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit is not young.
("rabbit" "is" "young" "-")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
If something needs the tiger and it does not visit the dog then the tiger is red.
((("something" "needs" "tiger" "+") ("something" "visits" "dog" "~")) -> ("tiger" "is" "red" "+"))
If something needs the tiger and the tiger needs the dog then the tiger is red.
((("something" "needs" "tiger" "+") ("tiger" "needs" "dog" "+")) -> ("tiger" "is" "red" "+"))
If something chases the dog then the dog chases the rabbit.
((("something" "chases" "dog" "+")) -> ("dog" "chases" "rabbit" "+"))
The rabbit is round.
True
1
proof
[(triple10)]
("rabbit" "is" "round" "+")
triple10
The rabbit is not round.
False
1
inv-proof
[(triple10)]
("rabbit" "is" "round" "-")
triple10
The tiger is not red.
Unknown
inv-rconc
[@1: The tiger is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "red" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The dog chases the tiger.[(triple1)] The dog does not visit the rabbit.[(triple6)] The dog is cold.[(triple2)] The dog is round.[(triple3)] The dog is young.[(triple4)] The dog needs the rabbit.[(triple5)] The dog visits the tiger.[(triple7)] The rabbit chases the tiger.[(triple8)] The rabbit is cold.[(triple9)] The rabbit is not young.[(triple11)] The rabbit is round.[(triple10)] The rabbit visits the dog.[(triple12)] The rabbit visits the tiger.[(triple13)] The tiger chases the dog.[(triple14)] The tiger needs the rabbit.[(triple15)] @1: The dog chases the rabbit.[(((triple14) -> rule3))]
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple1
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
triple6
The dog is cold.
("dog" "is" "cold" "+")
triple2
The dog is round.
("dog" "is" "round" "+")
triple3
The dog is young.
("dog" "is" "young" "+")
triple4
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple5
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple7
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple8
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple9
The rabbit is not young.
("rabbit" "is" "young" "-")
triple11
The rabbit is round.
("rabbit" "is" "round" "+")
triple10
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple12
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple13
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple14
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple15
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
((triple14) -> (rule3 % int1))
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int1