The lion eats the rabbit. The lion is cold. The lion is nice. The lion visits the mouse. The lion visits the rabbit. The mouse eats the rabbit. The mouse sees the squirrel. The mouse visits the lion. The rabbit is blue. The rabbit is cold. The rabbit is nice. The rabbit sees the mouse. The squirrel is blue. The squirrel is cold. The squirrel sees the mouse. The squirrel visits the mouse. If someone eats the squirrel then they see the lion. If someone sees the squirrel then the squirrel eats the mouse. If someone visits the squirrel then they visit the rabbit. If someone visits the squirrel then they are kind. If someone visits the mouse then the mouse sees the rabbit. If someone eats the mouse and they visit the mouse then they eat the squirrel. If someone sees the rabbit then they see the lion. If someone eats the rabbit then the rabbit is nice. If the squirrel sees the lion then the lion eats the mouse.
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
If someone eats the squirrel then they see the lion.
((("someone" "eats" "squirrel" "+")) -> ("someone" "sees" "lion" "+"))
If someone sees the squirrel then the squirrel eats the mouse.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "eats" "mouse" "+"))
If someone visits the squirrel then they visit the rabbit.
((("someone" "visits" "squirrel" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone visits the squirrel then they are kind.
((("someone" "visits" "squirrel" "+")) -> ("someone" "is" "kind" "+"))
If someone visits the mouse then the mouse sees the rabbit.
((("someone" "visits" "mouse" "+")) -> ("mouse" "sees" "rabbit" "+"))
If someone eats the mouse and they visit the mouse then they eat the squirrel.
((("someone" "eats" "mouse" "+") ("someone" "visits" "mouse" "+")) -> ("someone" "eats" "squirrel" "+"))
If someone sees the rabbit then they see the lion.
((("someone" "sees" "rabbit" "+")) -> ("someone" "sees" "lion" "+"))
If someone eats the rabbit then the rabbit is nice.
((("someone" "eats" "rabbit" "+")) -> ("rabbit" "is" "nice" "+"))
If the squirrel sees the lion then the lion eats the mouse.
((("squirrel" "sees" "lion" "+")) -> ("lion" "eats" "mouse" "+"))
The lion visits the rabbit.
True
1
proof
[(triple5)]
("lion" "visits" "rabbit" "+")
triple5
The lion is not cold.
False
1
inv-proof
[(triple2)]
("lion" "is" "cold" "-")
triple2
The mouse sees the rabbit.
True
2
proof
[(((triple16) -> rule5) OR ((triple4) -> rule5))]
("mouse" "sees" "rabbit" "+")
((triple16) -> (rule5 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
((triple4) -> (rule5 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
The mouse does not see the rabbit.
False
2
inv-proof
[(((triple16) -> rule5) OR ((triple4) -> rule5))]
("mouse" "sees" "rabbit" "-")
((triple16) -> (rule5 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
((triple4) -> (rule5 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
The squirrel eats the squirrel.
True
4
proof
[(((((triple7) -> rule2) triple16) -> rule6))]
("squirrel" "eats" "squirrel" "+")
((((triple7) -> (rule2 % int2)) triple16) -> (rule6 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int2
The squirrel does not eat the squirrel.
False
4
inv-proof
[(((((triple7) -> rule2) triple16) -> rule6))]
("squirrel" "eats" "squirrel" "-")
((((triple7) -> (rule2 % int2)) triple16) -> (rule6 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int2
The squirrel sees the lion.
True
5
proof
[(((((((triple7) -> rule2) triple16) -> rule6)) -> rule1))]
("squirrel" "sees" "lion" "+")
((((((triple7) -> (rule2 % int3)) triple16) -> (rule6 % int2))) -> (rule1 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int3
The squirrel does not see the lion.
False
5
inv-proof
[(((((((triple7) -> rule2) triple16) -> rule6)) -> rule1))]
("squirrel" "sees" "lion" "-")
((((((triple7) -> (rule2 % int3)) triple16) -> (rule6 % int2))) -> (rule1 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int3
The lion eats the mouse.
True
6
proof
[(((((((((triple7) -> rule2) triple16) -> rule6)) -> rule1)) -> rule9))]
("lion" "eats" "mouse" "+")
((((((((triple7) -> (rule2 % int4)) triple16) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int3
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int4
The lion does not eat the mouse.
False
6
inv-proof
[(((((((((triple7) -> rule2) triple16) -> rule6)) -> rule1)) -> rule9))]
("lion" "eats" "mouse" "-")
((((((((triple7) -> (rule2 % int4)) triple16) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int3
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int4
The lion eats the squirrel.
True
8
proof
[(((((((((((triple7) -> rule2) triple16) -> rule6)) -> rule1)) -> rule9) triple4) -> rule6))]
("lion" "eats" "squirrel" "+")
((((((((((triple7) -> (rule2 % int5)) triple16) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule9 % int2)) triple4) -> (rule6 % int1))
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int2
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int3
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int4
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int5
The lion does not eat the squirrel.
False
8
inv-proof
[(((((((((((triple7) -> rule2) triple16) -> rule6)) -> rule1)) -> rule9) triple4) -> rule6))]
("lion" "eats" "squirrel" "-")
((((((((((triple7) -> (rule2 % int5)) triple16) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule9 % int2)) triple4) -> (rule6 % int1))
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int2
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int3
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int4
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int5
The mouse does not eat the squirrel.
Unknown
inv-rconc
[@1: The mouse eats the squirrel.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "eats" "squirrel" "-")
The mouse is kind.
Unknown
rconc
[@1: The mouse is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "kind" "+")
The mouse does not visit the rabbit.
Unknown
inv-rconc
[@1: The mouse visits the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "visits" "rabbit" "-")
The squirrel visits the rabbit.
Unknown
rconc
[@1: The squirrel visits the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "visits" "rabbit" "+")
The rabbit does not visit the rabbit.
Unknown
inv-rconc
[@1: The rabbit visits the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "visits" "rabbit" "-")
The rabbit sees the lion.
Unknown
rconc
[@2: The rabbit sees the lion.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("rabbit" "sees" "lion" "+")
The rabbit does not see the squirrel.
Unknown
inv-random
[@0: The rabbit sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "squirrel" "-")
The squirrel is rough.
Unknown
random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
The mouse is not rough.
Unknown
inv-random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
@0: The lion eats the rabbit.[(triple1)] The lion is cold.[(triple2)] The lion is nice.[(triple3)] The lion visits the mouse.[(triple4)] The lion visits the rabbit.[(triple5)] The mouse eats the rabbit.[(triple6)] The mouse sees the squirrel.[(triple7)] The mouse visits the lion.[(triple8)] The rabbit is blue.[(triple9)] The rabbit is cold.[(triple10)] The rabbit is nice.[(triple11 OR ((triple1) -> rule8) OR ((triple6) -> rule8))] The rabbit sees the mouse.[(triple12)] The squirrel is blue.[(triple13)] The squirrel is cold.[(triple14)] The squirrel sees the mouse.[(triple15)] The squirrel visits the mouse.[(triple16)] @1: The mouse sees the rabbit.[(((triple16) -> rule5) OR ((triple4) -> rule5))] The squirrel eats the mouse.[(((triple7) -> rule2))] @2: The mouse sees the lion.[(((((triple16) -> rule5)) -> rule7) OR ((((triple4) -> rule5)) -> rule7))] The squirrel eats the squirrel.[(((((triple7) -> rule2) triple16) -> rule6))] @3: The squirrel sees the lion.[(((((((triple7) -> rule2) triple16) -> rule6)) -> rule1))] @4: The lion eats the mouse.[(((((((((triple7) -> rule2) triple16) -> rule6)) -> rule1)) -> rule9))] @5: The lion eats the squirrel.[(((((((((((triple7) -> rule2) triple16) -> rule6)) -> rule1)) -> rule9) triple4) -> rule6))] @6: The lion sees the lion.[(((((((((((((triple7) -> rule2) triple16) -> rule6)) -> rule1)) -> rule9) triple4) -> rule6)) -> rule1))]
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
The lion is nice.
("lion" "is" "nice" "+")
triple3
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple4
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
triple5
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple6
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple7
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple8
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple9
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple10
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple11
((triple1) -> (rule8 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
((triple6) -> (rule8 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple12
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple13
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple14
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple15
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple16
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
((triple16) -> (rule5 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
((triple4) -> (rule5 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
((triple7) -> (rule2 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The mouse sees the lion.
("mouse" "sees" "lion" "+")
((((triple16) -> (rule5 % int2))) -> (rule7 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int2
((((triple4) -> (rule5 % int2))) -> (rule7 % int1))
The mouse sees the lion.
("mouse" "sees" "lion" "+")
int1
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((((triple7) -> (rule2 % int2)) triple16) -> (rule6 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int2
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
((((((triple7) -> (rule2 % int3)) triple16) -> (rule6 % int2))) -> (rule1 % int1))
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int2
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int3
The lion eats the mouse.
("lion" "eats" "mouse" "+")
((((((((triple7) -> (rule2 % int4)) triple16) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int2
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int3
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int4
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
((((((((((triple7) -> (rule2 % int5)) triple16) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule9 % int2)) triple4) -> (rule6 % int1))
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int1
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int2
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int3
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int4
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int5
The lion sees the lion.
("lion" "sees" "lion" "+")
((((((((((((triple7) -> (rule2 % int6)) triple16) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule9 % int3)) triple4) -> (rule6 % int2))) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int2
The lion eats the mouse.
("lion" "eats" "mouse" "+")
int3
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
int4
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int5
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int6