The mouse is nice. The tiger sees the mouse. If the tiger is green and the tiger sees the mouse then the mouse is green. If something sees the tiger then the tiger needs the mouse. If something sees the tiger then it needs the mouse. If something is round then it chases the tiger. If something is blue then it sees the tiger. If something sees the mouse then the mouse is green. If the tiger sees the mouse then the tiger is nice. If something chases the mouse then it is green.
The mouse is nice.
("mouse" "is" "nice" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If the tiger is green and the tiger sees the mouse then the mouse is green.
((("tiger" "is" "green" "+") ("tiger" "sees" "mouse" "+")) -> ("mouse" "is" "green" "+"))
If something sees the tiger then the tiger needs the mouse.
((("something" "sees" "tiger" "+")) -> ("tiger" "needs" "mouse" "+"))
If something sees the tiger then it needs the mouse.
((("something" "sees" "tiger" "+")) -> ("something" "needs" "mouse" "+"))
If something is round then it chases the tiger.
((("something" "is" "round" "+")) -> ("something" "chases" "tiger" "+"))
If something is blue then it sees the tiger.
((("something" "is" "blue" "+")) -> ("something" "sees" "tiger" "+"))
If something sees the mouse then the mouse is green.
((("something" "sees" "mouse" "+")) -> ("mouse" "is" "green" "+"))
If the tiger sees the mouse then the tiger is nice.
((("tiger" "sees" "mouse" "+")) -> ("tiger" "is" "nice" "+"))
If something chases the mouse then it is green.
((("something" "chases" "mouse" "+")) -> ("something" "is" "green" "+"))
The tiger sees the mouse.
True
1
proof
[(triple2)]
("tiger" "sees" "mouse" "+")
triple2
The mouse is not nice.
False
1
inv-proof
[(triple1)]
("mouse" "is" "nice" "-")
triple1
The mouse is green.
True
2
proof
[(((triple2) -> rule6))]
("mouse" "is" "green" "+")
((triple2) -> (rule6 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The tiger is not nice.
False
2
inv-proof
[(((triple2) -> rule7))]
("tiger" "is" "nice" "-")
((triple2) -> (rule7 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger does not chase the tiger.
Unknown
inv-rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "chases" "tiger" "-")
The tiger sees the tiger.
Unknown
rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "sees" "tiger" "+")
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 chases the mouse.
Unknown
random
[@0: The tiger chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "mouse" "+")
@0: The mouse is nice.[(triple1)] The tiger sees the mouse.[(triple2)] @1: The mouse is green.[(((triple2) -> rule6))] The tiger is nice.[(((triple2) -> rule7))]
The mouse is nice.
("mouse" "is" "nice" "+")
triple1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple2
The mouse is green.
("mouse" "is" "green" "+")
((triple2) -> (rule6 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
((triple2) -> (rule7 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1