The mouse needs the squirrel. The squirrel eats the mouse. The squirrel visits the mouse. If someone is big and they eat the mouse then they are young. If someone needs the squirrel then the squirrel visits the mouse. If someone visits the mouse and the mouse visits the squirrel then they visit the squirrel. If the squirrel is nice then the squirrel needs the mouse. If someone eats the mouse then the mouse visits the squirrel. If someone eats the squirrel then they are nice.
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
If someone is big and they eat the mouse then they are young.
((("someone" "is" "big" "+") ("someone" "eats" "mouse" "+")) -> ("someone" "is" "young" "+"))
If someone needs the squirrel then the squirrel visits the mouse.
((("someone" "needs" "squirrel" "+")) -> ("squirrel" "visits" "mouse" "+"))
If someone visits the mouse and the mouse visits the squirrel then they visit the squirrel.
((("someone" "visits" "mouse" "+") ("mouse" "visits" "squirrel" "+")) -> ("someone" "visits" "squirrel" "+"))
If the squirrel is nice then the squirrel needs the mouse.
((("squirrel" "is" "nice" "+")) -> ("squirrel" "needs" "mouse" "+"))
If someone eats the mouse then the mouse visits the squirrel.
((("someone" "eats" "mouse" "+")) -> ("mouse" "visits" "squirrel" "+"))
If someone eats the squirrel then they are nice.
((("someone" "eats" "squirrel" "+")) -> ("someone" "is" "nice" "+"))
The squirrel visits the mouse.
True
1
proof
[(triple3 OR ((triple1) -> rule2))]
("squirrel" "visits" "mouse" "+")
triple3
((triple1) -> (rule2 % int1))
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int1
The squirrel does not eat the mouse.
False
1
inv-proof
[(triple2)]
("squirrel" "eats" "mouse" "-")
triple2
The mouse visits the squirrel.
True
2
proof
[(((triple2) -> rule5))]
("mouse" "visits" "squirrel" "+")
((triple2) -> (rule5 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The mouse does not visit the squirrel.
False
2
inv-proof
[(((triple2) -> rule5))]
("mouse" "visits" "squirrel" "-")
((triple2) -> (rule5 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The squirrel visits the squirrel.
True
4
proof
[(((triple3 ((triple2) -> rule5)) -> rule3) OR ((((triple1) -> rule2) ((triple2) -> rule5)) -> rule3))]
("squirrel" "visits" "squirrel" "+")
((triple3 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
((((triple1) -> (rule2 % int3)) ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int3
The squirrel does not visit the squirrel.
False
4
inv-proof
[(((triple3 ((triple2) -> rule5)) -> rule3) OR ((((triple1) -> rule2) ((triple2) -> rule5)) -> rule3))]
("squirrel" "visits" "squirrel" "-")
((triple3 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
((((triple1) -> (rule2 % int3)) ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int3
The mouse is not nice.
Unknown
inv-rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "nice" "-")
The squirrel is young.
Unknown
rconc
[@1: The squirrel is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "young" "+")
The mouse is not young.
Unknown
inv-rconc
[@1: The mouse is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "young" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
The mouse is not kind.
Unknown
inv-random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "-")
The squirrel is big.
Unknown
random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "+")
@0: The mouse needs the squirrel.[(triple1)] The squirrel eats the mouse.[(triple2)] The squirrel visits the mouse.[(triple3 OR ((triple1) -> rule2))] @1: The mouse visits the squirrel.[(((triple2) -> rule5))] @2: The squirrel visits the squirrel.[(((triple3 ((triple2) -> rule5)) -> rule3) OR ((((triple1) -> rule2) ((triple2) -> rule5)) -> rule3))]
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple2
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple3
((triple1) -> (rule2 % int1))
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
((triple2) -> (rule5 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((triple3 ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
((((triple1) -> (rule2 % int3)) ((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int3