The cat chases the squirrel. The cat sees the mouse. The cat sees the squirrel. The lion visits the cat. The mouse does not chase the cat. The mouse chases the lion. The mouse chases the squirrel. The mouse is blue. The mouse sees the lion. The squirrel is blue. The squirrel sees the cat. The squirrel sees the mouse. If something visits the squirrel then the squirrel is green. If the squirrel chases the cat and the squirrel is not blue then the squirrel chases the mouse. If something is blue and it sees the lion then it visits the squirrel. If the cat chases the mouse then the cat chases the lion. If the mouse does not chase the squirrel then the mouse sees the lion. If the squirrel does not see the mouse and the mouse does not visit the squirrel then the mouse is green.
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
The mouse does not chase the cat.
("mouse" "chases" "cat" "-")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse sees the lion.
("mouse" "sees" "lion" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
If something visits the squirrel then the squirrel is green.
((("something" "visits" "squirrel" "+")) -> ("squirrel" "is" "green" "+"))
If the squirrel chases the cat and the squirrel is not blue then the squirrel chases the mouse.
((("squirrel" "chases" "cat" "+") ("squirrel" "is" "blue" "~")) -> ("squirrel" "chases" "mouse" "+"))
If something is blue and it sees the lion then it visits the squirrel.
((("something" "is" "blue" "+") ("something" "sees" "lion" "+")) -> ("something" "visits" "squirrel" "+"))
If the cat chases the mouse then the cat chases the lion.
((("cat" "chases" "mouse" "+")) -> ("cat" "chases" "lion" "+"))
If the mouse does not chase the squirrel then the mouse sees the lion.
((("mouse" "chases" "squirrel" "~")) -> ("mouse" "sees" "lion" "+"))
If the squirrel does not see the mouse and the mouse does not visit the squirrel then the mouse is green.
((("squirrel" "sees" "mouse" "~") ("mouse" "visits" "squirrel" "~")) -> ("mouse" "is" "green" "+"))
The squirrel sees the mouse.
True
1
proof
[(triple12)]
("squirrel" "sees" "mouse" "+")
triple12
The mouse chases the cat.
False
1
inv-proof
[(triple5)]
("mouse" "chases" "cat" "+")
triple5
The mouse visits the squirrel.
True
3
proof
[(((triple8 triple9) -> rule3))]
("mouse" "visits" "squirrel" "+")
((triple8 triple9) -> (rule3 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The mouse does not visit the squirrel.
False
3
inv-proof
[(((triple8 triple9) -> rule3))]
("mouse" "visits" "squirrel" "-")
((triple8 triple9) -> (rule3 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The squirrel is green.
True
4
proof
[(((((triple8 triple9) -> rule3)) -> rule1))]
("squirrel" "is" "green" "+")
((((triple8 triple9) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The squirrel is not green.
False
4
inv-proof
[(((((triple8 triple9) -> rule3)) -> rule1))]
("squirrel" "is" "green" "-")
((((triple8 triple9) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The lion does not visit the squirrel.
Unknown
inv-rconc
[@1: The lion visits the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "visits" "squirrel" "-")
The cat chases the lion.
Unknown
rconc
[@1: The cat chases the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "chases" "lion" "+")
The cat does not visit the squirrel.
Unknown
inv-rconc
[@1: The cat visits the squirrel.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "visits" "squirrel" "-")
The squirrel sees the lion.
Unknown
random
[@0: The squirrel sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "lion" "+")
The mouse is not young.
Unknown
inv-random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "-")
The squirrel visits the lion.
Unknown
random
[@0: The squirrel visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "lion" "+")
@0: The cat chases the squirrel.[(triple1)] The cat sees the mouse.[(triple2)] The cat sees the squirrel.[(triple3)] The lion visits the cat.[(triple4)] The mouse chases the lion.[(triple6)] The mouse chases the squirrel.[(triple7)] The mouse does not chase the cat.[(triple5)] The mouse is blue.[(triple8)] The mouse sees the lion.[(triple9)] The squirrel is blue.[(triple10)] The squirrel sees the cat.[(triple11)] The squirrel sees the mouse.[(triple12)] @1: The mouse visits the squirrel.[(((triple8 triple9) -> rule3))] @2: The squirrel is green.[(((((triple8 triple9) -> rule3)) -> rule1))]
The cat chases the squirrel.
("cat" "chases" "squirrel" "+")
triple1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple2
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
triple3
The lion visits the cat.
("lion" "visits" "cat" "+")
triple4
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple6
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple7
The mouse does not chase the cat.
("mouse" "chases" "cat" "-")
triple5
The mouse is blue.
("mouse" "is" "blue" "+")
triple8
The mouse sees the lion.
("mouse" "sees" "lion" "+")
triple9
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple10
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple11
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple12
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
((triple8 triple9) -> (rule3 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
((((triple8 triple9) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2