The mouse does not like the squirrel. The squirrel is green. The squirrel is young. The squirrel likes the mouse. The squirrel sees the tiger. The tiger is not green. The tiger likes the mouse. If someone sees the mouse then they chase the mouse. If someone sees the tiger and the tiger likes the mouse then they see the mouse. If someone likes the tiger then the tiger chases the squirrel. If someone is young then they chase the squirrel. If someone chases the mouse and they like the mouse then they are not red. If the tiger does not like the squirrel then the squirrel does not like the tiger. If someone chases the squirrel and the squirrel is not cold then the squirrel chases the tiger. If someone sees the mouse and the mouse does not chase the tiger then the tiger likes the mouse.
The mouse does not like the squirrel.
("mouse" "likes" "squirrel" "-")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger is not green.
("tiger" "is" "green" "-")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
If someone sees the mouse then they chase the mouse.
((("someone" "sees" "mouse" "+")) -> ("someone" "chases" "mouse" "+"))
If someone sees the tiger and the tiger likes the mouse then they see the mouse.
((("someone" "sees" "tiger" "+") ("tiger" "likes" "mouse" "+")) -> ("someone" "sees" "mouse" "+"))
If someone likes the tiger then the tiger chases the squirrel.
((("someone" "likes" "tiger" "+")) -> ("tiger" "chases" "squirrel" "+"))
If someone is young then they chase the squirrel.
((("someone" "is" "young" "+")) -> ("someone" "chases" "squirrel" "+"))
If someone chases the mouse and they like the mouse then they are not red.
((("someone" "chases" "mouse" "+") ("someone" "likes" "mouse" "+")) -> ("someone" "is" "red" "-"))
If the tiger does not like the squirrel then the squirrel does not like the tiger.
((("tiger" "likes" "squirrel" "~")) -> ("squirrel" "likes" "tiger" "-"))
If someone chases the squirrel and the squirrel is not cold then the squirrel chases the tiger.
((("someone" "chases" "squirrel" "+") ("squirrel" "is" "cold" "~")) -> ("squirrel" "chases" "tiger" "+"))
If someone sees the mouse and the mouse does not chase the tiger then the tiger likes the mouse.
((("someone" "sees" "mouse" "+") ("mouse" "chases" "tiger" "~")) -> ("tiger" "likes" "mouse" "+"))
The squirrel is young.
True
1
proof
[(triple3)]
("squirrel" "is" "young" "+")
triple3
The squirrel does not see the tiger.
False
1
inv-proof
[(triple5)]
("squirrel" "sees" "tiger" "-")
triple5
The squirrel chases the squirrel.
True
2
proof
[(((triple3) -> rule4))]
("squirrel" "chases" "squirrel" "+")
((triple3) -> (rule4 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel does not see the mouse.
False
3
inv-proof
[(((triple5 triple7) -> rule2))]
("squirrel" "sees" "mouse" "-")
((triple5 triple7) -> (rule2 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The squirrel chases the mouse.
True
4
proof
[(((((triple5 triple7) -> rule2)) -> rule1))]
("squirrel" "chases" "mouse" "+")
((((triple5 triple7) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int2
The squirrel does not chase the mouse.
False
4
inv-proof
[(((((triple5 triple7) -> rule2)) -> rule1))]
("squirrel" "chases" "mouse" "-")
((((triple5 triple7) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int2
The squirrel is not red.
True
6
proof
[(((((((triple5 triple7) -> rule2)) -> rule1) triple4) -> rule5))]
("squirrel" "is" "red" "-")
((((((triple5 triple7) -> (rule2 % int3))) -> (rule1 % int2)) triple4) -> (rule5 % int1))
The squirrel is not red.
("squirrel" "is" "red" "-")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int2
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int3
The squirrel is red.
False
6
inv-proof
[(((((((triple5 triple7) -> rule2)) -> rule1) triple4) -> rule5))]
("squirrel" "is" "red" "+")
((((((triple5 triple7) -> (rule2 % int3))) -> (rule1 % int2)) triple4) -> (rule5 % int1))
The squirrel is not red.
("squirrel" "is" "red" "-")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int2
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int3
The tiger does not chase the mouse.
Unknown
inv-rconc
[@2: The tiger chases the mouse.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("tiger" "chases" "mouse" "-")
The mouse sees the mouse.
Unknown
rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "sees" "mouse" "+")
The mouse does not chase the mouse.
Unknown
inv-rconc
[@2: The mouse chases the mouse.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("mouse" "chases" "mouse" "-")
The tiger sees the mouse.
Unknown
rconc
[@1: The tiger sees the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "sees" "mouse" "+")
The squirrel does not like the tiger.
Unknown
inv-random
[@0: The squirrel likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "tiger" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
The mouse is not green.
Unknown
inv-random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
@0: The mouse does not like the squirrel.[(triple1)] The squirrel is green.[(triple2)] The squirrel is young.[(triple3)] The squirrel likes the mouse.[(triple4)] The squirrel sees the tiger.[(triple5)] The tiger is not green.[(triple6)] The tiger likes the mouse.[(triple7)] @1: The squirrel chases the squirrel.[(((triple3) -> rule4))] The squirrel sees the mouse.[(((triple5 triple7) -> rule2))] @2: The squirrel chases the mouse.[(((((triple5 triple7) -> rule2)) -> rule1))] @3: The squirrel is not red.[(((((((triple5 triple7) -> rule2)) -> rule1) triple4) -> rule5))]
The mouse does not like the squirrel.
("mouse" "likes" "squirrel" "-")
triple1
The squirrel is green.
("squirrel" "is" "green" "+")
triple2
The squirrel is young.
("squirrel" "is" "young" "+")
triple3
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
triple4
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple5
The tiger is not green.
("tiger" "is" "green" "-")
triple6
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple7
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((triple3) -> (rule4 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
((triple5 triple7) -> (rule2 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
((((triple5 triple7) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int2
The squirrel is not red.
("squirrel" "is" "red" "-")
((((((triple5 triple7) -> (rule2 % int3))) -> (rule1 % int2)) triple4) -> (rule5 % int1))
The squirrel is not red.
("squirrel" "is" "red" "-")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int2
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int3