The dog does not eat the mouse. The dog is rough. The dog likes the rabbit. The mouse eats the rabbit. The mouse is young. The mouse does not like the tiger. The rabbit chases the mouse. The rabbit does not chase the tiger. The tiger chases the mouse. The tiger likes the rabbit. If someone eats the mouse then they chase the dog. If someone likes the rabbit and the rabbit chases the dog then the rabbit is young. If someone eats the tiger then they like the dog. If someone likes the dog and the dog likes the tiger then they are young. If someone eats the rabbit then the rabbit eats the mouse. If someone is red and they eat the mouse then the mouse is red.
The dog does not eat the mouse.
("dog" "eats" "mouse" "-")
The dog is rough.
("dog" "is" "rough" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse does not like the tiger.
("mouse" "likes" "tiger" "-")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit does not chase the tiger.
("rabbit" "chases" "tiger" "-")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
If someone eats the mouse then they chase the dog.
((("someone" "eats" "mouse" "+")) -> ("someone" "chases" "dog" "+"))
If someone likes the rabbit and the rabbit chases the dog then the rabbit is young.
((("someone" "likes" "rabbit" "+") ("rabbit" "chases" "dog" "+")) -> ("rabbit" "is" "young" "+"))
If someone eats the tiger then they like the dog.
((("someone" "eats" "tiger" "+")) -> ("someone" "likes" "dog" "+"))
If someone likes the dog and the dog likes the tiger then they are young.
((("someone" "likes" "dog" "+") ("dog" "likes" "tiger" "+")) -> ("someone" "is" "young" "+"))
If someone eats the rabbit then the rabbit eats the mouse.
((("someone" "eats" "rabbit" "+")) -> ("rabbit" "eats" "mouse" "+"))
If someone is red and they eat the mouse then the mouse is red.
((("someone" "is" "red" "+") ("someone" "eats" "mouse" "+")) -> ("mouse" "is" "red" "+"))
The rabbit chases the mouse.
True
1
proof
[(triple7)]
("rabbit" "chases" "mouse" "+")
triple7
The rabbit does not chase the mouse.
False
1
inv-proof
[(triple7)]
("rabbit" "chases" "mouse" "-")
triple7
The rabbit eats the mouse.
True
2
proof
[(((triple4) -> rule5))]
("rabbit" "eats" "mouse" "+")
((triple4) -> (rule5 % int1))
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int1
The rabbit does not eat the mouse.
False
2
inv-proof
[(((triple4) -> rule5))]
("rabbit" "eats" "mouse" "-")
((triple4) -> (rule5 % int1))
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int1
The rabbit chases the dog.
True
3
proof
[(((((triple4) -> rule5)) -> rule1))]
("rabbit" "chases" "dog" "+")
((((triple4) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The rabbit does not chase the dog.
False
3
inv-proof
[(((((triple4) -> rule5)) -> rule1))]
("rabbit" "chases" "dog" "-")
((((triple4) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The rabbit is young.
True
5
proof
[(((triple10 ((((triple4) -> rule5)) -> rule1)) -> rule2) OR ((triple3 ((((triple4) -> rule5)) -> rule1)) -> rule2))]
("rabbit" "is" "young" "+")
((triple10 ((((triple4) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int3
((triple3 ((((triple4) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int3
The rabbit is not young.
False
5
inv-proof
[(((triple10 ((((triple4) -> rule5)) -> rule1)) -> rule2) OR ((triple3 ((((triple4) -> rule5)) -> rule1)) -> rule2))]
("rabbit" "is" "young" "-")
((triple10 ((((triple4) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int3
((triple3 ((((triple4) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int3
The tiger is not young.
Unknown
inv-rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "is" "young" "-")
The dog likes the dog.
Unknown
rconc
[@1: The dog likes the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "likes" "dog" "+")
The mouse does not like the dog.
Unknown
inv-rconc
[@1: The mouse likes the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "likes" "dog" "-")
The rabbit likes the dog.
Unknown
rconc
[@1: The rabbit likes the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "likes" "dog" "+")
The tiger does not eat the rabbit.
Unknown
inv-random
[@0: The tiger eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "rabbit" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
The rabbit does not like the mouse.
Unknown
inv-random
[@0: The rabbit likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "mouse" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
@0: The dog does not eat the mouse.[(triple1)] The dog is rough.[(triple2)] The dog likes the rabbit.[(triple3)] The mouse does not like the tiger.[(triple6)] The mouse eats the rabbit.[(triple4)] The mouse is young.[(triple5)] The rabbit chases the mouse.[(triple7)] The rabbit does not chase the tiger.[(triple8)] The tiger chases the mouse.[(triple9)] The tiger likes the rabbit.[(triple10)] @1: The rabbit eats the mouse.[(((triple4) -> rule5))] @2: The rabbit chases the dog.[(((((triple4) -> rule5)) -> rule1))] @3: The rabbit is young.[(((triple10 ((((triple4) -> rule5)) -> rule1)) -> rule2) OR ((triple3 ((((triple4) -> rule5)) -> rule1)) -> rule2))]
The dog does not eat the mouse.
("dog" "eats" "mouse" "-")
triple1
The dog is rough.
("dog" "is" "rough" "+")
triple2
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple3
The mouse does not like the tiger.
("mouse" "likes" "tiger" "-")
triple6
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple4
The mouse is young.
("mouse" "is" "young" "+")
triple5
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple7
The rabbit does not chase the tiger.
("rabbit" "chases" "tiger" "-")
triple8
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple9
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple10
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
((triple4) -> (rule5 % int1))
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
((((triple4) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
((triple10 ((((triple4) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int3
((triple3 ((((triple4) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int3