The mouse is green. The mouse is red. The mouse is rough. The mouse sees the squirrel. The squirrel is green. The squirrel is nice. The squirrel sees the mouse. The tiger chases the mouse. The tiger eats the squirrel. The tiger is green. The tiger is red. The tiger sees the mouse. If something eats the squirrel then it eats the tiger.
The mouse is green.
("mouse" "is" "green" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If something eats the squirrel then it eats the tiger.
((("something" "eats" "squirrel" "+")) -> ("something" "eats" "tiger" "+"))
The tiger eats the squirrel.
True
1
proof
[(triple9)]
("tiger" "eats" "squirrel" "+")
triple9
The mouse is not green.
False
1
inv-proof
[(triple1)]
("mouse" "is" "green" "-")
triple1
The squirrel does not eat the tiger.
Unknown
inv-rconc
[@1: The squirrel eats the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "eats" "tiger" "-")
The mouse sees the tiger.
Unknown
random
[@0: The mouse sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "tiger" "+")
@0: The mouse is green.[(triple1)] The mouse is red.[(triple2)] The mouse is rough.[(triple3)] The mouse sees the squirrel.[(triple4)] The squirrel is green.[(triple5)] The squirrel is nice.[(triple6)] The squirrel sees the mouse.[(triple7)] The tiger chases the mouse.[(triple8)] The tiger eats the squirrel.[(triple9)] The tiger is green.[(triple10)] The tiger is red.[(triple11)] The tiger sees the mouse.[(triple12)] @1: The tiger eats the tiger.[(((triple9) -> rule1))]
The mouse is green.
("mouse" "is" "green" "+")
triple1
The mouse is red.
("mouse" "is" "red" "+")
triple2
The mouse is rough.
("mouse" "is" "rough" "+")
triple3
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple4
The squirrel is green.
("squirrel" "is" "green" "+")
triple5
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple6
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple7
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple8
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple9
The tiger is green.
("tiger" "is" "green" "+")
triple10
The tiger is red.
("tiger" "is" "red" "+")
triple11
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple12
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((triple9) -> (rule1 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1