The cow needs the mouse. The mouse sees the squirrel. The squirrel does not see the mouse. If something visits the cow then the cow is rough. If the mouse does not visit the squirrel then the squirrel needs the mouse. If something is young then it does not see the cow. If something sees the squirrel and the squirrel is rough then the squirrel visits the mouse. If something sees the squirrel then it is round. If something sees the cow then it is not young.
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The squirrel does not see the mouse.
("squirrel" "sees" "mouse" "-")
If something visits the cow then the cow is rough.
((("something" "visits" "cow" "+")) -> ("cow" "is" "rough" "+"))
If the mouse does not visit the squirrel then the squirrel needs the mouse.
((("mouse" "visits" "squirrel" "~")) -> ("squirrel" "needs" "mouse" "+"))
If something is young then it does not see the cow.
((("something" "is" "young" "+")) -> ("something" "sees" "cow" "-"))
If something sees the squirrel and the squirrel is rough then the squirrel visits the mouse.
((("something" "sees" "squirrel" "+") ("squirrel" "is" "rough" "+")) -> ("squirrel" "visits" "mouse" "+"))
If something sees the squirrel then it is round.
((("something" "sees" "squirrel" "+")) -> ("something" "is" "round" "+"))
If something sees the cow then it is not young.
((("something" "sees" "cow" "+")) -> ("something" "is" "young" "-"))
The squirrel does not see the mouse.
True
1
proof
[(triple3)]
("squirrel" "sees" "mouse" "-")
triple3
The squirrel sees the mouse.
False
1
inv-proof
[(triple3)]
("squirrel" "sees" "mouse" "+")
triple3
The mouse is round.
True
2
proof
[(((triple2) -> rule5))]
("mouse" "is" "round" "+")
((triple2) -> (rule5 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The mouse is not round.
False
2
inv-proof
[(((triple2) -> rule5))]
("mouse" "is" "round" "-")
((triple2) -> (rule5 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The squirrel does not visit the mouse.
Unknown
inv-rconc
[@1: The squirrel visits the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "visits" "mouse" "-")
The squirrel needs the mouse.
Unknown
rconc
[@1: The squirrel needs the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "needs" "mouse" "+")
The cow is not young.
Unknown
inv-random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
@0: The cow needs the mouse.[(triple1)] The mouse sees the squirrel.[(triple2)] The squirrel does not see the mouse.[(triple3)] @1: The mouse is round.[(((triple2) -> rule5))]
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple2
The squirrel does not see the mouse.
("squirrel" "sees" "mouse" "-")
triple3
The mouse is round.
("mouse" "is" "round" "+")
((triple2) -> (rule5 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1