The lion eats the tiger. The lion sees the mouse. The lion does not see the squirrel. The lion sees the tiger. The mouse is young. The mouse sees the squirrel. The mouse visits the tiger. The squirrel eats the mouse. The squirrel is big. The squirrel is cold. The squirrel is young. The squirrel sees the lion. The squirrel does not visit the mouse. The tiger eats the lion. The tiger does not eat the mouse. The tiger sees the mouse. All cold people are young. If someone sees the mouse then the mouse eats the squirrel.
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion sees the mouse.
("lion" "sees" "mouse" "+")
The lion does not see the squirrel.
("lion" "sees" "squirrel" "-")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
The squirrel does not visit the mouse.
("squirrel" "visits" "mouse" "-")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
The tiger does not eat the mouse.
("tiger" "eats" "mouse" "-")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
All cold people are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
If someone sees the mouse then the mouse eats the squirrel.
((("someone" "sees" "mouse" "+")) -> ("mouse" "eats" "squirrel" "+"))
The squirrel does not visit the mouse.
True
1
proof
[(triple13)]
("squirrel" "visits" "mouse" "-")
triple13
The mouse does not visit the tiger.
False
1
inv-proof
[(triple7)]
("mouse" "visits" "tiger" "-")
triple7
The mouse eats the squirrel.
True
2
proof
[(((triple16) -> rule2) OR ((triple2) -> rule2))]
("mouse" "eats" "squirrel" "+")
((triple16) -> (rule2 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
((triple2) -> (rule2 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The mouse does not eat the squirrel.
False
2
inv-proof
[(((triple16) -> rule2) OR ((triple2) -> rule2))]
("mouse" "eats" "squirrel" "-")
((triple16) -> (rule2 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
((triple2) -> (rule2 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The lion is not young.
Unknown
inv-rconc
[@1: The lion is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "young" "-")
The tiger is young.
Unknown
rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "young" "+")
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 tiger visits the squirrel.
Unknown
random
[@0: The tiger visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "squirrel" "+")
@0: The lion does not see the squirrel.[(triple3)] The lion eats the tiger.[(triple1)] The lion sees the mouse.[(triple2)] The lion sees the tiger.[(triple4)] The mouse is young.[(triple5)] The mouse sees the squirrel.[(triple6)] The mouse visits the tiger.[(triple7)] The squirrel does not visit the mouse.[(triple13)] The squirrel eats the mouse.[(triple8)] The squirrel is big.[(triple9)] The squirrel is cold.[(triple10)] The squirrel is young.[(triple11 OR ((triple10) -> rule1))] The squirrel sees the lion.[(triple12)] The tiger does not eat the mouse.[(triple15)] The tiger eats the lion.[(triple14)] The tiger sees the mouse.[(triple16)] @1: The mouse eats the squirrel.[(((triple16) -> rule2) OR ((triple2) -> rule2))]
The lion does not see the squirrel.
("lion" "sees" "squirrel" "-")
triple3
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple1
The lion sees the mouse.
("lion" "sees" "mouse" "+")
triple2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple4
The mouse is young.
("mouse" "is" "young" "+")
triple5
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple6
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple7
The squirrel does not visit the mouse.
("squirrel" "visits" "mouse" "-")
triple13
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple8
The squirrel is big.
("squirrel" "is" "big" "+")
triple9
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple10
The squirrel is young.
("squirrel" "is" "young" "+")
triple11
((triple10) -> (rule1 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel sees the lion.
("squirrel" "sees" "lion" "+")
triple12
The tiger does not eat the mouse.
("tiger" "eats" "mouse" "-")
triple15
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple14
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple16
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
((triple16) -> (rule2 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
((triple2) -> (rule2 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1