The mouse chases the tiger. The squirrel chases the mouse. The tiger sees the mouse. If something is big then it chases the tiger. If something chases the mouse then it sees the tiger. If the squirrel sees the mouse then the squirrel is round. If something is green then it needs the squirrel. If something chases the tiger then the tiger is blue. If the tiger is big and the tiger chases the mouse then the tiger needs the squirrel.
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If something is big then it chases the tiger.
((("something" "is" "big" "+")) -> ("something" "chases" "tiger" "+"))
If something chases the mouse then it sees the tiger.
((("something" "chases" "mouse" "+")) -> ("something" "sees" "tiger" "+"))
If the squirrel sees the mouse then the squirrel is round.
((("squirrel" "sees" "mouse" "+")) -> ("squirrel" "is" "round" "+"))
If something is green then it needs the squirrel.
((("something" "is" "green" "+")) -> ("something" "needs" "squirrel" "+"))
If something chases the tiger then the tiger is blue.
((("something" "chases" "tiger" "+")) -> ("tiger" "is" "blue" "+"))
If the tiger is big and the tiger chases the mouse then the tiger needs the squirrel.
((("tiger" "is" "big" "+") ("tiger" "chases" "mouse" "+")) -> ("tiger" "needs" "squirrel" "+"))
The mouse chases the tiger.
True
1
proof
[(triple1)]
("mouse" "chases" "tiger" "+")
triple1
The squirrel does not chase the mouse.
False
1
inv-proof
[(triple2)]
("squirrel" "chases" "mouse" "-")
triple2
The squirrel sees the tiger.
True
2
proof
[(((triple2) -> rule2))]
("squirrel" "sees" "tiger" "+")
((triple2) -> (rule2 % int1))
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int1
The squirrel does not see the tiger.
False
2
inv-proof
[(((triple2) -> rule2))]
("squirrel" "sees" "tiger" "-")
((triple2) -> (rule2 % int1))
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int1
The mouse does not need the squirrel.
Unknown
inv-rconc
[@1: The mouse needs the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "needs" "squirrel" "-")
The squirrel is round.
Unknown
rconc
[@1: The squirrel is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "round" "+")
The mouse is not blue.
Unknown
inv-random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
@0: The mouse chases the tiger.[(triple1)] The squirrel chases the mouse.[(triple2)] The tiger sees the mouse.[(triple3)] @1: The squirrel sees the tiger.[(((triple2) -> rule2))] The tiger is blue.[(((triple1) -> rule5))]
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
triple2
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple3
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
((triple2) -> (rule2 % int1))
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
((triple1) -> (rule5 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1