The mouse is nice. The mouse needs the tiger. The rabbit is round. The rabbit sees the mouse. The squirrel does not eat the tiger. The tiger eats the squirrel. The tiger is nice. The tiger is not rough. The tiger sees the mouse. The tiger sees the rabbit. If someone needs the squirrel and the squirrel sees the rabbit then the squirrel is round. If someone sees the rabbit then they are round. If the squirrel eats the tiger then the tiger is red. If someone sees the rabbit and they are round then the rabbit eats the mouse. If someone needs the rabbit then they are green. If someone needs the tiger and the tiger needs the rabbit then they see the tiger. If someone eats the mouse then they are nice. If someone eats the tiger then the tiger eats the squirrel.
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
The squirrel does not eat the tiger.
("squirrel" "eats" "tiger" "-")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is not rough.
("tiger" "is" "rough" "-")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If someone needs the squirrel and the squirrel sees the rabbit then the squirrel is round.
((("someone" "needs" "squirrel" "+") ("squirrel" "sees" "rabbit" "+")) -> ("squirrel" "is" "round" "+"))
If someone sees the rabbit then they are round.
((("someone" "sees" "rabbit" "+")) -> ("someone" "is" "round" "+"))
If the squirrel eats the tiger then the tiger is red.
((("squirrel" "eats" "tiger" "+")) -> ("tiger" "is" "red" "+"))
If someone sees the rabbit and they are round then the rabbit eats the mouse.
((("someone" "sees" "rabbit" "+") ("someone" "is" "round" "+")) -> ("rabbit" "eats" "mouse" "+"))
If someone needs the rabbit then they are green.
((("someone" "needs" "rabbit" "+")) -> ("someone" "is" "green" "+"))
If someone needs the tiger and the tiger needs the rabbit then they see the tiger.
((("someone" "needs" "tiger" "+") ("tiger" "needs" "rabbit" "+")) -> ("someone" "sees" "tiger" "+"))
If someone eats the mouse then they are nice.
((("someone" "eats" "mouse" "+")) -> ("someone" "is" "nice" "+"))
If someone eats the tiger then the tiger eats the squirrel.
((("someone" "eats" "tiger" "+")) -> ("tiger" "eats" "squirrel" "+"))
The rabbit sees the mouse.
True
1
proof
[(triple4)]
("rabbit" "sees" "mouse" "+")
triple4
The tiger is not nice.
False
1
inv-proof
[(triple7)]
("tiger" "is" "nice" "-")
triple7
The tiger is round.
True
2
proof
[(((triple10) -> rule2))]
("tiger" "is" "round" "+")
((triple10) -> (rule2 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is not round.
False
2
inv-proof
[(((triple10) -> rule2))]
("tiger" "is" "round" "-")
((triple10) -> (rule2 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The rabbit eats the mouse.
True
4
proof
[(((triple10 ((triple10) -> rule2)) -> rule4))]
("rabbit" "eats" "mouse" "+")
((triple10 ((triple10) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The rabbit does not eat the mouse.
False
4
inv-proof
[(((triple10 ((triple10) -> rule2)) -> rule4))]
("rabbit" "eats" "mouse" "-")
((triple10 ((triple10) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The rabbit is nice.
True
5
proof
[(((((triple10 ((triple10) -> rule2)) -> rule4)) -> rule7))]
("rabbit" "is" "nice" "+")
((((triple10 ((triple10) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
The rabbit is not nice.
False
5
inv-proof
[(((((triple10 ((triple10) -> rule2)) -> rule4)) -> rule7))]
("rabbit" "is" "nice" "-")
((((triple10 ((triple10) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3
The rabbit does not see the tiger.
Unknown
inv-rconc
[@1: The rabbit sees the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "sees" "tiger" "-")
The rabbit is green.
Unknown
rconc
[@1: The rabbit is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "green" "+")
The mouse is not green.
Unknown
inv-rconc
[@1: The mouse is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "green" "-")
The squirrel is round.
Unknown
rconc
[@1: The squirrel is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "round" "+")
The squirrel does not need the tiger.
Unknown
inv-random
[@0: The squirrel needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "tiger" "-")
The squirrel is rough.
Unknown
random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The rabbit needs the mouse.
Unknown
random
[@0: The rabbit needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "mouse" "+")
@0: The mouse is nice.[(triple1)] The mouse needs the tiger.[(triple2)] The rabbit is round.[(triple3)] The rabbit sees the mouse.[(triple4)] The squirrel does not eat the tiger.[(triple5)] The tiger eats the squirrel.[(triple6)] The tiger is nice.[(triple7)] The tiger is not rough.[(triple8)] The tiger sees the mouse.[(triple9)] The tiger sees the rabbit.[(triple10)] @1: The tiger is round.[(((triple10) -> rule2))] @2: The rabbit eats the mouse.[(((triple10 ((triple10) -> rule2)) -> rule4))] @3: The rabbit is nice.[(((((triple10 ((triple10) -> rule2)) -> rule4)) -> rule7))]
The mouse is nice.
("mouse" "is" "nice" "+")
triple1
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple2
The rabbit is round.
("rabbit" "is" "round" "+")
triple3
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple4
The squirrel does not eat the tiger.
("squirrel" "eats" "tiger" "-")
triple5
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple6
The tiger is nice.
("tiger" "is" "nice" "+")
triple7
The tiger is not rough.
("tiger" "is" "rough" "-")
triple8
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple9
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple10
The tiger is round.
("tiger" "is" "round" "+")
((triple10) -> (rule2 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
((triple10 ((triple10) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The rabbit is nice.
("rabbit" "is" "nice" "+")
((((triple10 ((triple10) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
int3