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