The dog is young. The rabbit needs the dog. The tiger eats the dog. If something is big then it eats the tiger. If something chases the tiger and the tiger chases the rabbit then the tiger is big. If something is rough and it chases the tiger then it is nice. If something chases the rabbit then it eats the tiger. If the dog eats the rabbit and the rabbit chases the tiger then the tiger chases the rabbit. If something eats the dog then the dog is big. Rough things are young. If something is young then it eats the tiger.
The dog is young.
("dog" "is" "young" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The tiger eats the dog.
("tiger" "eats" "dog" "+")
If something is big then it eats the tiger.
((("something" "is" "big" "+")) -> ("something" "eats" "tiger" "+"))
If something chases the tiger and the tiger chases the rabbit then the tiger is big.
((("something" "chases" "tiger" "+") ("tiger" "chases" "rabbit" "+")) -> ("tiger" "is" "big" "+"))
If something is rough and it chases the tiger then it is nice.
((("something" "is" "rough" "+") ("something" "chases" "tiger" "+")) -> ("something" "is" "nice" "+"))
If something chases the rabbit then it eats the tiger.
((("something" "chases" "rabbit" "+")) -> ("something" "eats" "tiger" "+"))
If the dog eats the rabbit and the rabbit chases the tiger then the tiger chases the rabbit.
((("dog" "eats" "rabbit" "+") ("rabbit" "chases" "tiger" "+")) -> ("tiger" "chases" "rabbit" "+"))
If something eats the dog then the dog is big.
((("something" "eats" "dog" "+")) -> ("dog" "is" "big" "+"))
Rough things are young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something is young then it eats the tiger.
((("something" "is" "young" "+")) -> ("something" "eats" "tiger" "+"))
The dog is young.
True
1
proof
[(triple1)]
("dog" "is" "young" "+")
triple1
The tiger does not eat the dog.
False
1
inv-proof
[(triple3)]
("tiger" "eats" "dog" "-")
triple3
The rabbit is not nice.
Unknown
inv-rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "nice" "-")
The rabbit chases the tiger.
Unknown
random
[@0: The rabbit chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "tiger" "+")
@0: The dog is young.[(triple1)] The rabbit needs the dog.[(triple2)] The tiger eats the dog.[(triple3)] @1: The dog eats the tiger.[(((triple1) -> rule8) OR ((((triple3) -> rule6)) -> rule1))] The dog is big.[(((triple3) -> rule6))]
The dog is young.
("dog" "is" "young" "+")
triple1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple2
The tiger eats the dog.
("tiger" "eats" "dog" "+")
triple3
The dog eats the tiger.
("dog" "eats" "tiger" "+")
((triple1) -> (rule8 % int1))
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int1
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog is big.
("dog" "is" "big" "+")
((triple3) -> (rule6 % int1))
The dog is big.
("dog" "is" "big" "+")
int1