The mouse likes the rabbit. The mouse likes the tiger. The rabbit chases the mouse. The rabbit likes the squirrel. The squirrel chases the tiger. The squirrel sees the rabbit. The tiger chases the mouse. The tiger is green. The tiger is rough. The tiger is round. The tiger sees the rabbit. The tiger sees the squirrel. If someone is rough then they like the tiger. If someone sees the squirrel and they see the mouse then the squirrel likes the rabbit. If someone is rough and they like the squirrel then the squirrel chases the mouse. If someone likes the tiger then they like the rabbit. If someone likes the mouse and the mouse is cold then the mouse likes the tiger. If someone is green and they like the rabbit then the rabbit is green.
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
If someone is rough then they like the tiger.
((("someone" "is" "rough" "+")) -> ("someone" "likes" "tiger" "+"))
If someone sees the squirrel and they see the mouse then the squirrel likes the rabbit.
((("someone" "sees" "squirrel" "+") ("someone" "sees" "mouse" "+")) -> ("squirrel" "likes" "rabbit" "+"))
If someone is rough and they like the squirrel then the squirrel chases the mouse.
((("someone" "is" "rough" "+") ("someone" "likes" "squirrel" "+")) -> ("squirrel" "chases" "mouse" "+"))
If someone likes the tiger then they like the rabbit.
((("someone" "likes" "tiger" "+")) -> ("someone" "likes" "rabbit" "+"))
If someone likes the mouse and the mouse is cold then the mouse likes the tiger.
((("someone" "likes" "mouse" "+") ("mouse" "is" "cold" "+")) -> ("mouse" "likes" "tiger" "+"))
If someone is green and they like the rabbit then the rabbit is green.
((("someone" "is" "green" "+") ("someone" "likes" "rabbit" "+")) -> ("rabbit" "is" "green" "+"))
The tiger is green.
True
1
proof
[(triple8)]
("tiger" "is" "green" "+")
triple8
The tiger is not rough.
False
1
inv-proof
[(triple9)]
("tiger" "is" "rough" "-")
triple9
The tiger likes the tiger.
True
2
proof
[(((triple9) -> rule1))]
("tiger" "likes" "tiger" "+")
((triple9) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger does not like the tiger.
False
2
inv-proof
[(((triple9) -> rule1))]
("tiger" "likes" "tiger" "-")
((triple9) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger likes the rabbit.
True
3
proof
[(((((triple9) -> rule1)) -> rule4))]
("tiger" "likes" "rabbit" "+")
((((triple9) -> (rule1 % int2))) -> (rule4 % int1))
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger does not like the rabbit.
False
3
inv-proof
[(((((triple9) -> rule1)) -> rule4))]
("tiger" "likes" "rabbit" "-")
((((triple9) -> (rule1 % int2))) -> (rule4 % int1))
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The rabbit is green.
True
5
proof
[(((triple8 ((((triple9) -> rule1)) -> rule4)) -> rule6))]
("rabbit" "is" "green" "+")
((triple8 ((((triple9) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The rabbit is not green.
False
5
inv-proof
[(((triple8 ((((triple9) -> rule1)) -> rule4)) -> rule6))]
("rabbit" "is" "green" "-")
((triple8 ((((triple9) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The rabbit does not like the tiger.
Unknown
inv-rconc
[@1: The rabbit likes the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "likes" "tiger" "-")
The squirrel chases the mouse.
Unknown
rconc
[@1: The squirrel chases the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "chases" "mouse" "+")
The rabbit does not like the rabbit.
Unknown
inv-rconc
[@2: The rabbit likes the rabbit.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("rabbit" "likes" "rabbit" "-")
The squirrel likes the rabbit.
Unknown
rconc
[@2: The squirrel likes the rabbit.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("squirrel" "likes" "rabbit" "+")
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
The tiger does not chase the squirrel.
Unknown
inv-random
[@0: The tiger chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "squirrel" "-")
The tiger sees the mouse.
Unknown
random
[@0: The tiger sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "mouse" "+")
@0: The mouse likes the rabbit.[(triple1 OR ((triple2) -> rule4))] The mouse likes the tiger.[(triple2)] The rabbit chases the mouse.[(triple3)] The rabbit likes the squirrel.[(triple4)] The squirrel chases the tiger.[(triple5)] The squirrel sees the rabbit.[(triple6)] The tiger chases the mouse.[(triple7)] The tiger is green.[(triple8)] The tiger is rough.[(triple9)] The tiger is round.[(triple10)] The tiger sees the rabbit.[(triple11)] The tiger sees the squirrel.[(triple12)] @1: The tiger likes the tiger.[(((triple9) -> rule1))] @2: The tiger likes the rabbit.[(((((triple9) -> rule1)) -> rule4))] @3: The rabbit is green.[(((triple8 ((((triple9) -> rule1)) -> rule4)) -> rule6))]
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple1
((triple2) -> (rule4 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple2
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple3
The rabbit likes the squirrel.
("rabbit" "likes" "squirrel" "+")
triple4
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple5
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple6
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple7
The tiger is green.
("tiger" "is" "green" "+")
triple8
The tiger is rough.
("tiger" "is" "rough" "+")
triple9
The tiger is round.
("tiger" "is" "round" "+")
triple10
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple11
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple12
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple9) -> (rule1 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
((((triple9) -> (rule1 % int2))) -> (rule4 % int1))
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
((triple8 ((((triple9) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3