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