The mouse visits the squirrel. The rabbit is green. The rabbit sees the tiger. The squirrel likes the rabbit. The squirrel does not like the tiger. The tiger is red. The tiger sees the mouse. The tiger sees the squirrel. The tiger visits the mouse. The tiger does not visit the rabbit. If something sees the squirrel and it sees the rabbit then it is green. If something visits the mouse then it likes the mouse. If something sees the squirrel and it likes the mouse then the squirrel visits the rabbit. If something visits the tiger then it does not see the squirrel. If something is green and it sees the tiger then it is not nice. If the rabbit is green then the rabbit is kind. If something visits the rabbit then it visits the squirrel. If something sees the tiger and the tiger likes the squirrel then the squirrel is rough.
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
The squirrel does not like the tiger.
("squirrel" "likes" "tiger" "-")
The tiger is red.
("tiger" "is" "red" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
The tiger does not visit the rabbit.
("tiger" "visits" "rabbit" "-")
If something sees the squirrel and it sees the rabbit then it is green.
((("something" "sees" "squirrel" "+") ("something" "sees" "rabbit" "+")) -> ("something" "is" "green" "+"))
If something visits the mouse then it likes the mouse.
((("something" "visits" "mouse" "+")) -> ("something" "likes" "mouse" "+"))
If something sees the squirrel and it likes the mouse then the squirrel visits the rabbit.
((("something" "sees" "squirrel" "+") ("something" "likes" "mouse" "+")) -> ("squirrel" "visits" "rabbit" "+"))
If something visits the tiger then it does not see the squirrel.
((("something" "visits" "tiger" "+")) -> ("something" "sees" "squirrel" "-"))
If something is green and it sees the tiger then it is not nice.
((("something" "is" "green" "+") ("something" "sees" "tiger" "+")) -> ("something" "is" "nice" "-"))
If the rabbit is green then the rabbit is kind.
((("rabbit" "is" "green" "+")) -> ("rabbit" "is" "kind" "+"))
If something visits the rabbit then it visits the squirrel.
((("something" "visits" "rabbit" "+")) -> ("something" "visits" "squirrel" "+"))
If something sees the tiger and the tiger likes the squirrel then the squirrel is rough.
((("something" "sees" "tiger" "+") ("tiger" "likes" "squirrel" "+")) -> ("squirrel" "is" "rough" "+"))
The rabbit sees the tiger.
True
1
proof
[(triple3)]
("rabbit" "sees" "tiger" "+")
triple3
The rabbit is not green.
False
1
inv-proof
[(triple2)]
("rabbit" "is" "green" "-")
triple2
The rabbit is not nice.
True
3
proof
[(((triple2 triple3) -> rule5))]
("rabbit" "is" "nice" "-")
((triple2 triple3) -> (rule5 % int1))
The rabbit is not nice.
("rabbit" "is" "nice" "-")
int1
The rabbit is nice.
False
3
inv-proof
[(((triple2 triple3) -> rule5))]
("rabbit" "is" "nice" "+")
((triple2 triple3) -> (rule5 % int1))
The rabbit is not nice.
("rabbit" "is" "nice" "-")
int1
The squirrel visits the rabbit.
True
4
proof
[(((triple8 ((triple9) -> rule2)) -> rule3))]
("squirrel" "visits" "rabbit" "+")
((triple8 ((triple9) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The squirrel does not visit the rabbit.
False
4
inv-proof
[(((triple8 ((triple9) -> rule2)) -> rule3))]
("squirrel" "visits" "rabbit" "-")
((triple8 ((triple9) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The squirrel visits the squirrel.
True
5
proof
[(((((triple8 ((triple9) -> rule2)) -> rule3)) -> rule7))]
("squirrel" "visits" "squirrel" "+")
((((triple8 ((triple9) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int2
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int3
The squirrel does not visit the squirrel.
False
5
inv-proof
[(((((triple8 ((triple9) -> rule2)) -> rule3)) -> rule7))]
("squirrel" "visits" "squirrel" "-")
((((triple8 ((triple9) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int2
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int3
The rabbit does not visit the squirrel.
Unknown
inv-rconc
[@1: The rabbit visits the squirrel.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "visits" "squirrel" "-")
The squirrel likes the mouse.
Unknown
rconc
[@1: The squirrel likes the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "likes" "mouse" "+")
The squirrel is not rough.
Unknown
inv-rconc
[@1: The squirrel is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "is" "rough" "-")
The mouse is green.
Unknown
rconc
[@1: The mouse is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "green" "+")
The mouse does not like the rabbit.
Unknown
inv-random
[@0: The mouse likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "rabbit" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
The squirrel does not see the rabbit.
Unknown
inv-random
[@0: The squirrel sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "rabbit" "-")
The mouse sees the tiger.
Unknown
random
[@0: The mouse sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "tiger" "+")
@0: The mouse visits the squirrel.[(triple1)] The rabbit is green.[(triple2)] The rabbit sees the tiger.[(triple3)] The squirrel does not like the tiger.[(triple5)] The squirrel likes the rabbit.[(triple4)] The tiger does not visit the rabbit.[(triple10)] The tiger is red.[(triple6)] The tiger sees the mouse.[(triple7)] The tiger sees the squirrel.[(triple8)] The tiger visits the mouse.[(triple9)] @1: The rabbit is kind.[(((triple2) -> rule6))] The rabbit is not nice.[(((triple2 triple3) -> rule5))] The tiger likes the mouse.[(((triple9) -> rule2))] @2: The squirrel visits the rabbit.[(((triple8 ((triple9) -> rule2)) -> rule3))] @3: The squirrel visits the squirrel.[(((((triple8 ((triple9) -> rule2)) -> rule3)) -> rule7))]
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple1
The rabbit is green.
("rabbit" "is" "green" "+")
triple2
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple3
The squirrel does not like the tiger.
("squirrel" "likes" "tiger" "-")
triple5
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
triple4
The tiger does not visit the rabbit.
("tiger" "visits" "rabbit" "-")
triple10
The tiger is red.
("tiger" "is" "red" "+")
triple6
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple7
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple8
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple9
The rabbit is kind.
("rabbit" "is" "kind" "+")
((triple2) -> (rule6 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is not nice.
("rabbit" "is" "nice" "-")
((triple2 triple3) -> (rule5 % int1))
The rabbit is not nice.
("rabbit" "is" "nice" "-")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
((triple9) -> (rule2 % int1))
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int1
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
((triple8 ((triple9) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int1
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int2
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((((triple8 ((triple9) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel visits the rabbit.
("squirrel" "visits" "rabbit" "+")
int2
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
int3