The mouse is green. The mouse is kind. The mouse is nice. The mouse needs the tiger. The mouse does not see the tiger. The tiger eats the mouse. The tiger is big. The tiger is green. The tiger is kind. The tiger is not nice. The tiger needs the mouse. The tiger sees the mouse. If something needs the mouse and it is not big then the mouse is nice. If something sees the tiger and the tiger eats the mouse then the mouse is not nice. If the tiger sees the mouse then the mouse eats the tiger. If something is blue then it needs the mouse. If something sees the mouse and the mouse needs the tiger then it is kind. If something needs the mouse and the mouse does not eat the tiger then it is not green. If something is big and green then it needs the tiger. If something needs the tiger then the tiger is kind.
The mouse is green.
("mouse" "is" "green" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The mouse does not see the tiger.
("mouse" "sees" "tiger" "-")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is not nice.
("tiger" "is" "nice" "-")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If something needs the mouse and it is not big then the mouse is nice.
((("something" "needs" "mouse" "+") ("something" "is" "big" "~")) -> ("mouse" "is" "nice" "+"))
If something sees the tiger and the tiger eats the mouse then the mouse is not nice.
((("something" "sees" "tiger" "+") ("tiger" "eats" "mouse" "+")) -> ("mouse" "is" "nice" "-"))
If the tiger sees the mouse then the mouse eats the tiger.
((("tiger" "sees" "mouse" "+")) -> ("mouse" "eats" "tiger" "+"))
If something is blue then it needs the mouse.
((("something" "is" "blue" "+")) -> ("something" "needs" "mouse" "+"))
If something sees the mouse and the mouse needs the tiger then it is kind.
((("something" "sees" "mouse" "+") ("mouse" "needs" "tiger" "+")) -> ("something" "is" "kind" "+"))
If something needs the mouse and the mouse does not eat the tiger then it is not green.
((("something" "needs" "mouse" "+") ("mouse" "eats" "tiger" "~")) -> ("something" "is" "green" "-"))
If something is big and green then it needs the tiger.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "needs" "tiger" "+"))
If something needs the tiger then the tiger is kind.
((("something" "needs" "tiger" "+")) -> ("tiger" "is" "kind" "+"))
The mouse is green.
True
1
proof
[(triple1)]
("mouse" "is" "green" "+")
triple1
The tiger does not eat the mouse.
False
1
inv-proof
[(triple6)]
("tiger" "eats" "mouse" "-")
triple6
The tiger needs the tiger.
True
3
proof
[(((triple7 triple8) -> rule7))]
("tiger" "needs" "tiger" "+")
((triple7 triple8) -> (rule7 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger does not need the tiger.
False
3
inv-proof
[(((triple7 triple8) -> rule7))]
("tiger" "needs" "tiger" "-")
((triple7 triple8) -> (rule7 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The mouse does not need the mouse.
Unknown
inv-rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "needs" "mouse" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The mouse does not see the tiger.[(triple5)] The mouse is green.[(triple1)] The mouse is kind.[(triple2)] The mouse is nice.[(triple3)] The mouse needs the tiger.[(triple4)] The tiger eats the mouse.[(triple6)] The tiger is big.[(triple7)] The tiger is green.[(triple8)] The tiger is kind.[(triple9 OR ((triple4) -> rule8) OR ((triple12 triple4) -> rule5) OR ((((triple7 triple8) -> rule7)) -> rule8))] The tiger is not nice.[(triple10)] The tiger needs the mouse.[(triple11)] The tiger sees the mouse.[(triple12)] @1: The mouse eats the tiger.[(((triple12) -> rule3))] The tiger needs the tiger.[(((triple7 triple8) -> rule7))]
The mouse does not see the tiger.
("mouse" "sees" "tiger" "-")
triple5
The mouse is green.
("mouse" "is" "green" "+")
triple1
The mouse is kind.
("mouse" "is" "kind" "+")
triple2
The mouse is nice.
("mouse" "is" "nice" "+")
triple3
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple4
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple6
The tiger is big.
("tiger" "is" "big" "+")
triple7
The tiger is green.
("tiger" "is" "green" "+")
triple8
The tiger is kind.
("tiger" "is" "kind" "+")
triple9
((triple4) -> (rule8 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
((triple12 triple4) -> (rule5 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
((((triple7 triple8) -> (rule7 % int2))) -> (rule8 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger is not nice.
("tiger" "is" "nice" "-")
triple10
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple11
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple12
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
((triple12) -> (rule3 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((triple7 triple8) -> (rule7 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1