The bear eats the rabbit. The mouse eats the tiger. The mouse is cold. The mouse is kind. The mouse visits the bear. The mouse visits the rabbit. The mouse visits the tiger. The rabbit chases the tiger. The tiger chases the rabbit. The tiger eats the mouse. The tiger is kind. The tiger is red. If someone chases the bear and the bear eats the tiger then the tiger eats the rabbit. If someone chases the rabbit then they visit the bear. If someone visits the mouse and they eat the tiger then the tiger visits the mouse. If someone visits the bear then they are young. If the rabbit visits the tiger and the rabbit eats the mouse then the rabbit visits the mouse. If someone chases the rabbit and they are young then they visit the mouse. If the rabbit is kind and the rabbit chases the tiger then the tiger eats the bear. If someone is young and they visit the rabbit then they are kind.
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is red.
("tiger" "is" "red" "+")
If someone chases the bear and the bear eats the tiger then the tiger eats the rabbit.
((("someone" "chases" "bear" "+") ("bear" "eats" "tiger" "+")) -> ("tiger" "eats" "rabbit" "+"))
If someone chases the rabbit then they visit the bear.
((("someone" "chases" "rabbit" "+")) -> ("someone" "visits" "bear" "+"))
If someone visits the mouse and they eat the tiger then the tiger visits the mouse.
((("someone" "visits" "mouse" "+") ("someone" "eats" "tiger" "+")) -> ("tiger" "visits" "mouse" "+"))
If someone visits the bear then they are young.
((("someone" "visits" "bear" "+")) -> ("someone" "is" "young" "+"))
If the rabbit visits the tiger and the rabbit eats the mouse then the rabbit visits the mouse.
((("rabbit" "visits" "tiger" "+") ("rabbit" "eats" "mouse" "+")) -> ("rabbit" "visits" "mouse" "+"))
If someone chases the rabbit and they are young then they visit the mouse.
((("someone" "chases" "rabbit" "+") ("someone" "is" "young" "+")) -> ("someone" "visits" "mouse" "+"))
If the rabbit is kind and the rabbit chases the tiger then the tiger eats the bear.
((("rabbit" "is" "kind" "+") ("rabbit" "chases" "tiger" "+")) -> ("tiger" "eats" "bear" "+"))
If someone is young and they visit the rabbit then they are kind.
((("someone" "is" "young" "+") ("someone" "visits" "rabbit" "+")) -> ("someone" "is" "kind" "+"))
The tiger is red.
True
1
proof
[(triple12)]
("tiger" "is" "red" "+")
triple12
The tiger is not red.
False
1
inv-proof
[(triple12)]
("tiger" "is" "red" "-")
triple12
The tiger visits the bear.
True
2
proof
[(((triple9) -> rule2))]
("tiger" "visits" "bear" "+")
((triple9) -> (rule2 % int1))
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int1
The tiger does not visit the bear.
False
2
inv-proof
[(((triple9) -> rule2))]
("tiger" "visits" "bear" "-")
((triple9) -> (rule2 % int1))
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int1
The tiger is young.
True
3
proof
[(((((triple9) -> rule2)) -> rule4))]
("tiger" "is" "young" "+")
((((triple9) -> (rule2 % int2))) -> (rule4 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int2
The tiger is not young.
False
3
inv-proof
[(((((triple9) -> rule2)) -> rule4))]
("tiger" "is" "young" "-")
((((triple9) -> (rule2 % int2))) -> (rule4 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int2
The tiger visits the mouse.
True
5
proof
[(((triple9 ((((triple9) -> rule2)) -> rule4)) -> rule6))]
("tiger" "visits" "mouse" "+")
((triple9 ((((triple9) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int3
The tiger does not visit the mouse.
False
5
inv-proof
[(((triple9 ((((triple9) -> rule2)) -> rule4)) -> rule6))]
("tiger" "visits" "mouse" "-")
((triple9 ((((triple9) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int3
The tiger does not eat the bear.
Unknown
inv-rconc
[@2: The tiger eats the bear.[CWA. Example of deepest failure = (rule7 <- rule8 <- FAIL)]]
("tiger" "eats" "bear" "-")
The rabbit is kind.
Unknown
rconc
[@1: The rabbit is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "is" "kind" "+")
The bear is not young.
Unknown
inv-rconc
[@2: The bear is young.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("bear" "is" "young" "-")
The mouse visits the mouse.
Unknown
rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "visits" "mouse" "+")
The rabbit does not chase the bear.
Unknown
inv-random
[@0: The rabbit chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "bear" "-")
The rabbit eats the rabbit.
Unknown
random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "+")
The mouse is not red.
Unknown
inv-random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
@0: The bear eats the rabbit.[(triple1)] The mouse eats the tiger.[(triple2)] The mouse is cold.[(triple3)] The mouse is kind.[(triple4 OR ((((triple5) -> rule4) triple6) -> rule8))] The mouse visits the bear.[(triple5)] The mouse visits the rabbit.[(triple6)] The mouse visits the tiger.[(triple7)] The rabbit chases the tiger.[(triple8)] The tiger chases the rabbit.[(triple9)] The tiger eats the mouse.[(triple10)] The tiger is kind.[(triple11)] The tiger is red.[(triple12)] @1: The mouse is young.[(((triple5) -> rule4))] The tiger visits the bear.[(((triple9) -> rule2))] @2: The tiger is young.[(((((triple9) -> rule2)) -> rule4))] @3: The tiger visits the mouse.[(((triple9 ((((triple9) -> rule2)) -> rule4)) -> rule6))]
The bear eats the rabbit.
("bear" "eats" "rabbit" "+")
triple1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple2
The mouse is cold.
("mouse" "is" "cold" "+")
triple3
The mouse is kind.
("mouse" "is" "kind" "+")
triple4
((((triple5) -> (rule4 % int2)) triple6) -> (rule8 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple5
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple6
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple7
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple8
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple9
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple10
The tiger is kind.
("tiger" "is" "kind" "+")
triple11
The tiger is red.
("tiger" "is" "red" "+")
triple12
The mouse is young.
("mouse" "is" "young" "+")
((triple5) -> (rule4 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
((triple9) -> (rule2 % int1))
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
((((triple9) -> (rule2 % int2))) -> (rule4 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int2
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
((triple9 ((((triple9) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int3