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