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