The lion does not see the mouse. The mouse chases the lion. The mouse chases the squirrel. The mouse does not chase the tiger. The mouse eats the tiger. The mouse is not round. The mouse is young. The mouse sees the squirrel. The squirrel eats the mouse. The squirrel is round. The squirrel sees the tiger. The tiger does not chase the mouse. The tiger does not chase the squirrel. The tiger sees the lion. The tiger sees the mouse. If something eats the mouse then it chases the tiger. If something sees the lion and the lion sees the mouse then the mouse eats the lion. If something chases the tiger and it is round then the tiger is nice.
The lion does not see the mouse.
("lion" "sees" "mouse" "-")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse does not chase the tiger.
("mouse" "chases" "tiger" "-")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is not round.
("mouse" "is" "round" "-")
The mouse is young.
("mouse" "is" "young" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger does not chase the mouse.
("tiger" "chases" "mouse" "-")
The tiger does not chase the squirrel.
("tiger" "chases" "squirrel" "-")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If something eats the mouse then it chases the tiger.
((("something" "eats" "mouse" "+")) -> ("something" "chases" "tiger" "+"))
If something sees the lion and the lion sees the mouse then the mouse eats the lion.
((("something" "sees" "lion" "+") ("lion" "sees" "mouse" "+")) -> ("mouse" "eats" "lion" "+"))
If something chases the tiger and it is round then the tiger is nice.
((("something" "chases" "tiger" "+") ("something" "is" "round" "+")) -> ("tiger" "is" "nice" "+"))
The tiger sees the mouse.
True
1
proof
[(triple15)]
("tiger" "sees" "mouse" "+")
triple15
The mouse is round.
False
1
inv-proof
[(triple6)]
("mouse" "is" "round" "+")
triple6
The squirrel chases the tiger.
True
2
proof
[(((triple9) -> rule1))]
("squirrel" "chases" "tiger" "+")
((triple9) -> (rule1 % int1))
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int1
The squirrel does not chase the tiger.
False
2
inv-proof
[(((triple9) -> rule1))]
("squirrel" "chases" "tiger" "-")
((triple9) -> (rule1 % int1))
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int1
The tiger is nice.
True
4
proof
[(((((triple9) -> rule1) triple10) -> rule3))]
("tiger" "is" "nice" "+")
((((triple9) -> (rule1 % int2)) triple10) -> (rule3 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int2
The tiger is not nice.
False
4
inv-proof
[(((((triple9) -> rule1) triple10) -> rule3))]
("tiger" "is" "nice" "-")
((((triple9) -> (rule1 % int2)) triple10) -> (rule3 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int2
The tiger does not chase the tiger.
Unknown
inv-rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "chases" "tiger" "-")
The lion chases the tiger.
Unknown
rconc
[@1: The lion chases the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "chases" "tiger" "+")
The mouse does not eat the lion.
Unknown
inv-rconc
[@1: The mouse eats the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "eats" "lion" "-")
The lion eats the squirrel.
Unknown
random
[@0: The lion eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "squirrel" "+")
The squirrel does not chase the mouse.
Unknown
inv-random
[@0: The squirrel chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "mouse" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
@0: The lion does not see the mouse.[(triple1)] The mouse chases the lion.[(triple2)] The mouse chases the squirrel.[(triple3)] The mouse does not chase the tiger.[(triple4)] The mouse eats the tiger.[(triple5)] The mouse is not round.[(triple6)] The mouse is young.[(triple7)] The mouse sees the squirrel.[(triple8)] The squirrel eats the mouse.[(triple9)] The squirrel is round.[(triple10)] The squirrel sees the tiger.[(triple11)] The tiger does not chase the mouse.[(triple12)] The tiger does not chase the squirrel.[(triple13)] The tiger sees the lion.[(triple14)] The tiger sees the mouse.[(triple15)] @1: The squirrel chases the tiger.[(((triple9) -> rule1))] @2: The tiger is nice.[(((((triple9) -> rule1) triple10) -> rule3))]
The lion does not see the mouse.
("lion" "sees" "mouse" "-")
triple1
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple2
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple3
The mouse does not chase the tiger.
("mouse" "chases" "tiger" "-")
triple4
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple5
The mouse is not round.
("mouse" "is" "round" "-")
triple6
The mouse is young.
("mouse" "is" "young" "+")
triple7
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple8
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple9
The squirrel is round.
("squirrel" "is" "round" "+")
triple10
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple11
The tiger does not chase the mouse.
("tiger" "chases" "mouse" "-")
triple12
The tiger does not chase the squirrel.
("tiger" "chases" "squirrel" "-")
triple13
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple14
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple15
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
((triple9) -> (rule1 % int1))
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
((((triple9) -> (rule1 % int2)) triple10) -> (rule3 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
int2