The mouse is young. The squirrel is blue. The squirrel visits the mouse. If something visits the mouse and it is young then the mouse visits the squirrel. If something visits the squirrel and it chases the mouse then it sees the squirrel. If something visits the mouse and the mouse chases the squirrel then it is young. If something is blue and it chases the mouse then the mouse is round. If something chases the mouse and the mouse is rough then it is nice. If something is blue then it chases the mouse. If the mouse is round then the mouse sees the squirrel. If the squirrel chases the mouse then the squirrel sees the mouse.
The mouse is young.
("mouse" "is" "young" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
If something visits the mouse and it is young then the mouse visits the squirrel.
((("something" "visits" "mouse" "+") ("something" "is" "young" "+")) -> ("mouse" "visits" "squirrel" "+"))
If something visits the squirrel and it chases the mouse then it sees the squirrel.
((("something" "visits" "squirrel" "+") ("something" "chases" "mouse" "+")) -> ("something" "sees" "squirrel" "+"))
If something visits the mouse and the mouse chases the squirrel then it is young.
((("something" "visits" "mouse" "+") ("mouse" "chases" "squirrel" "+")) -> ("something" "is" "young" "+"))
If something is blue and it chases the mouse then the mouse is round.
((("something" "is" "blue" "+") ("something" "chases" "mouse" "+")) -> ("mouse" "is" "round" "+"))
If something chases the mouse and the mouse is rough then it is nice.
((("something" "chases" "mouse" "+") ("mouse" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something is blue then it chases the mouse.
((("something" "is" "blue" "+")) -> ("something" "chases" "mouse" "+"))
If the mouse is round then the mouse sees the squirrel.
((("mouse" "is" "round" "+")) -> ("mouse" "sees" "squirrel" "+"))
If the squirrel chases the mouse then the squirrel sees the mouse.
((("squirrel" "chases" "mouse" "+")) -> ("squirrel" "sees" "mouse" "+"))
The squirrel is blue.
True
1
proof
[(triple2)]
("squirrel" "is" "blue" "+")
triple2
The squirrel does not visit the mouse.
False
1
inv-proof
[(triple3)]
("squirrel" "visits" "mouse" "-")
triple3
The squirrel chases the mouse.
True
2
proof
[(((triple2) -> rule6))]
("squirrel" "chases" "mouse" "+")
((triple2) -> (rule6 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The squirrel does not chase the mouse.
False
2
inv-proof
[(((triple2) -> rule6))]
("squirrel" "chases" "mouse" "-")
((triple2) -> (rule6 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The mouse is round.
True
4
proof
[(((triple2 ((triple2) -> rule6)) -> rule4))]
("mouse" "is" "round" "+")
((triple2 ((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int2
The mouse is not round.
False
4
inv-proof
[(((triple2 ((triple2) -> rule6)) -> rule4))]
("mouse" "is" "round" "-")
((triple2 ((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int2
The mouse sees the squirrel.
True
5
proof
[(((((triple2 ((triple2) -> rule6)) -> rule4)) -> rule7))]
("mouse" "sees" "squirrel" "+")
((((triple2 ((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int3
The mouse does not see the squirrel.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule6)) -> rule4)) -> rule7))]
("mouse" "sees" "squirrel" "-")
((((triple2 ((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int3
The squirrel is not young.
Unknown
inv-rconc
[@1: The squirrel is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "young" "-")
The mouse visits the squirrel.
Unknown
rconc
[@2: The mouse visits the squirrel.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("mouse" "visits" "squirrel" "+")
The mouse is not nice.
Unknown
inv-rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "nice" "-")
The squirrel is nice.
Unknown
rconc
[@1: The squirrel is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "is" "nice" "+")
The squirrel is not rough.
Unknown
inv-random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "-")
The mouse is rough.
Unknown
random
[@0: The mouse is rough.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "rough" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The mouse is young.[(triple1)] The squirrel is blue.[(triple2)] The squirrel visits the mouse.[(triple3)] @1: The squirrel chases the mouse.[(((triple2) -> rule6))] @2: The mouse is round.[(((triple2 ((triple2) -> rule6)) -> rule4))] The squirrel sees the mouse.[(((((triple2) -> rule6)) -> rule8))] @3: The mouse sees the squirrel.[(((((triple2 ((triple2) -> rule6)) -> rule4)) -> rule7))]
The mouse is young.
("mouse" "is" "young" "+")
triple1
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple2
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple3
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
((triple2) -> (rule6 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
((triple2 ((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int2
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
((((triple2) -> (rule6 % int2))) -> (rule8 % int1))
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int2
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
((((triple2 ((triple2) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The mouse is round.
("mouse" "is" "round" "+")
int2
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int3