The dog is young. The rabbit is young. The tiger is not nice. If someone is young then they chase the dog. If someone eats the rabbit and they are green then the rabbit is round. If someone eats the tiger then the tiger is round. If someone eats the rabbit and they eat the tiger then the rabbit chases the tiger. If someone is green and they like the dog then they do not like the tiger. If someone chases the tiger and they are round then they like the tiger. If the rabbit does not eat the dog then the rabbit does not like the tiger. If someone chases the dog then the dog eats the tiger.
The dog is young.
("dog" "is" "young" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The tiger is not nice.
("tiger" "is" "nice" "-")
If someone is young then they chase the dog.
((("someone" "is" "young" "+")) -> ("someone" "chases" "dog" "+"))
If someone eats the rabbit and they are green then the rabbit is round.
((("someone" "eats" "rabbit" "+") ("someone" "is" "green" "+")) -> ("rabbit" "is" "round" "+"))
If someone eats the tiger then the tiger is round.
((("someone" "eats" "tiger" "+")) -> ("tiger" "is" "round" "+"))
If someone eats the rabbit and they eat the tiger then the rabbit chases the tiger.
((("someone" "eats" "rabbit" "+") ("someone" "eats" "tiger" "+")) -> ("rabbit" "chases" "tiger" "+"))
If someone is green and they like the dog then they do not like the tiger.
((("someone" "is" "green" "+") ("someone" "likes" "dog" "+")) -> ("someone" "likes" "tiger" "-"))
If someone chases the tiger and they are round then they like the tiger.
((("someone" "chases" "tiger" "+") ("someone" "is" "round" "+")) -> ("someone" "likes" "tiger" "+"))
If the rabbit does not eat the dog then the rabbit does not like the tiger.
((("rabbit" "eats" "dog" "~")) -> ("rabbit" "likes" "tiger" "-"))
If someone chases the dog then the dog eats the tiger.
((("someone" "chases" "dog" "+")) -> ("dog" "eats" "tiger" "+"))
The dog is young.
True
1
proof
[(triple1)]
("dog" "is" "young" "+")
triple1
The rabbit is not young.
False
1
inv-proof
[(triple2)]
("rabbit" "is" "young" "-")
triple2
The rabbit chases the dog.
True
2
proof
[(((triple2) -> rule1))]
("rabbit" "chases" "dog" "+")
((triple2) -> (rule1 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The rabbit does not chase the dog.
False
2
inv-proof
[(((triple2) -> rule1))]
("rabbit" "chases" "dog" "-")
((triple2) -> (rule1 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The dog eats the tiger.
True
3
proof
[(((((triple1) -> rule1)) -> rule8) OR ((((triple2) -> rule1)) -> rule8))]
("dog" "eats" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The dog does not eat the tiger.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule8) OR ((((triple2) -> rule1)) -> rule8))]
("dog" "eats" "tiger" "-")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The tiger is round.
True
4
proof
[(((((((triple1) -> rule1)) -> rule8)) -> rule3) OR ((((((triple2) -> rule1)) -> rule8)) -> rule3))]
("tiger" "is" "round" "+")
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int2
The dog chases the dog.
("dog" "chases" "dog" "+")
int3
((((((triple2) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int2
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int3
The tiger is not round.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule8)) -> rule3) OR ((((((triple2) -> rule1)) -> rule8)) -> rule3))]
("tiger" "is" "round" "-")
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int2
The dog chases the dog.
("dog" "chases" "dog" "+")
int3
((((((triple2) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int2
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int3
The tiger does not chase the dog.
Unknown
inv-rconc
[@1: The tiger chases the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "chases" "dog" "-")
The rabbit is round.
Unknown
rconc
[@1: The rabbit is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "round" "+")
The dog does not like the tiger.
Unknown
inv-rconc
[@1: The dog likes the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "likes" "tiger" "-")
The tiger likes the tiger.
Unknown
rconc
[@1: The tiger likes the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "likes" "tiger" "+")
The dog is not nice.
Unknown
inv-random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "-")
The rabbit eats the dog.
Unknown
random
[@0: The rabbit eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "dog" "+")
The tiger does not chase the rabbit.
Unknown
inv-random
[@0: The tiger chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "rabbit" "-")
The tiger likes the rabbit.
Unknown
random
[@0: The tiger likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "rabbit" "+")
@0: The dog is young.[(triple1)] The rabbit is young.[(triple2)] The tiger is not nice.[(triple3)] @1: The dog chases the dog.[(((triple1) -> rule1))] The rabbit chases the dog.[(((triple2) -> rule1))] @2: The dog eats the tiger.[(((((triple1) -> rule1)) -> rule8) OR ((((triple2) -> rule1)) -> rule8))] @3: The tiger is round.[(((((((triple1) -> rule1)) -> rule8)) -> rule3) OR ((((((triple2) -> rule1)) -> rule8)) -> rule3))]
The dog is young.
("dog" "is" "young" "+")
triple1
The rabbit is young.
("rabbit" "is" "young" "+")
triple2
The tiger is not nice.
("tiger" "is" "nice" "-")
triple3
The dog chases the dog.
("dog" "chases" "dog" "+")
((triple1) -> (rule1 % int1))
The dog chases the dog.
("dog" "chases" "dog" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
((triple2) -> (rule1 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int1
The dog chases the dog.
("dog" "chases" "dog" "+")
int2
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int2
The dog chases the dog.
("dog" "chases" "dog" "+")
int3
((((((triple2) -> (rule1 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int2
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int3