The dog is young. The mouse is kind. The tiger is rough. If the dog is young then the dog chases the tiger. If someone eats the dog then the dog chases the tiger. If someone eats the mouse then the mouse is young. If someone is rough then they eat the tiger. If someone is rough and they chase the mouse then they eat the dog. If someone likes the mouse and they are young then they are kind. If someone eats the tiger then the tiger is cold. If the dog likes the tiger then the tiger is young.
The dog is young.
("dog" "is" "young" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
If the dog is young then the dog chases the tiger.
((("dog" "is" "young" "+")) -> ("dog" "chases" "tiger" "+"))
If someone eats the dog then the dog chases the tiger.
((("someone" "eats" "dog" "+")) -> ("dog" "chases" "tiger" "+"))
If someone eats the mouse then the mouse is young.
((("someone" "eats" "mouse" "+")) -> ("mouse" "is" "young" "+"))
If someone is rough then they eat the tiger.
((("someone" "is" "rough" "+")) -> ("someone" "eats" "tiger" "+"))
If someone is rough and they chase the mouse then they eat the dog.
((("someone" "is" "rough" "+") ("someone" "chases" "mouse" "+")) -> ("someone" "eats" "dog" "+"))
If someone likes the mouse and they are young then they are kind.
((("someone" "likes" "mouse" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
If someone eats the tiger then the tiger is cold.
((("someone" "eats" "tiger" "+")) -> ("tiger" "is" "cold" "+"))
If the dog likes the tiger then the tiger is young.
((("dog" "likes" "tiger" "+")) -> ("tiger" "is" "young" "+"))
The dog is young.
True
1
proof
[(triple1)]
("dog" "is" "young" "+")
triple1
The mouse is not kind.
False
1
inv-proof
[(triple2)]
("mouse" "is" "kind" "-")
triple2
The tiger eats the tiger.
True
2
proof
[(((triple3) -> rule4))]
("tiger" "eats" "tiger" "+")
((triple3) -> (rule4 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger does not eat the tiger.
False
2
inv-proof
[(((triple3) -> rule4))]
("tiger" "eats" "tiger" "-")
((triple3) -> (rule4 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is cold.
True
3
proof
[(((((triple3) -> rule4)) -> rule7))]
("tiger" "is" "cold" "+")
((((triple3) -> (rule4 % int2))) -> (rule7 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger is not cold.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule7))]
("tiger" "is" "cold" "-")
((((triple3) -> (rule4 % int2))) -> (rule7 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The dog does not eat the tiger.
Unknown
inv-rconc
[@1: The dog eats the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "eats" "tiger" "-")
The mouse is young.
Unknown
rconc
[@1: The mouse is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "young" "+")
The tiger does not eat the dog.
Unknown
inv-rconc
[@1: The tiger eats the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "eats" "dog" "-")
The mouse likes the tiger.
Unknown
random
[@0: The mouse likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "tiger" "+")
The mouse is not rough.
Unknown
inv-random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "-")
The mouse chases the dog.
Unknown
random
[@0: The mouse chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "dog" "+")
@0: The dog is young.[(triple1)] The mouse is kind.[(triple2)] The tiger is rough.[(triple3)] @1: The dog chases the tiger.[(((triple1) -> rule1))] The tiger eats the tiger.[(((triple3) -> rule4))] @2: The tiger is cold.[(((((triple3) -> rule4)) -> rule7))]
The dog is young.
("dog" "is" "young" "+")
triple1
The mouse is kind.
("mouse" "is" "kind" "+")
triple2
The tiger is rough.
("tiger" "is" "rough" "+")
triple3
The dog chases the tiger.
("dog" "chases" "tiger" "+")
((triple1) -> (rule1 % int1))
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((triple3) -> (rule4 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
((((triple3) -> (rule4 % int2))) -> (rule7 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2