The mouse needs the squirrel. The squirrel needs the mouse. The squirrel visits the mouse. If something is young and it likes the mouse then it is red. If something is young and it visits the mouse then the mouse likes the squirrel. If something is blue and it visits the squirrel then the squirrel needs the mouse. If something needs the squirrel and the squirrel visits the mouse then the mouse visits the squirrel. If something is red then it visits the squirrel. If something visits the squirrel and the squirrel needs the mouse then the mouse likes the squirrel.
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
If something is young and it likes the mouse then it is red.
((("something" "is" "young" "+") ("something" "likes" "mouse" "+")) -> ("something" "is" "red" "+"))
If something is young and it visits the mouse then the mouse likes the squirrel.
((("something" "is" "young" "+") ("something" "visits" "mouse" "+")) -> ("mouse" "likes" "squirrel" "+"))
If something is blue and it visits the squirrel then the squirrel needs the mouse.
((("something" "is" "blue" "+") ("something" "visits" "squirrel" "+")) -> ("squirrel" "needs" "mouse" "+"))
If something needs the squirrel and the squirrel visits the mouse then the mouse visits the squirrel.
((("something" "needs" "squirrel" "+") ("squirrel" "visits" "mouse" "+")) -> ("mouse" "visits" "squirrel" "+"))
If something is red then it visits the squirrel.
((("something" "is" "red" "+")) -> ("something" "visits" "squirrel" "+"))
If something visits the squirrel and the squirrel needs the mouse then the mouse likes the squirrel.
((("something" "visits" "squirrel" "+") ("squirrel" "needs" "mouse" "+")) -> ("mouse" "likes" "squirrel" "+"))
The mouse needs the squirrel.
True
1
proof
[(triple1)]
("mouse" "needs" "squirrel" "+")
triple1
The squirrel does not visit the mouse.
False
1
inv-proof
[(triple3)]
("squirrel" "visits" "mouse" "-")
triple3
The mouse visits the squirrel.
True
3
proof
[(((triple1 triple3) -> rule4))]
("mouse" "visits" "squirrel" "+")
((triple1 triple3) -> (rule4 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The mouse does not visit the squirrel.
False
3
inv-proof
[(((triple1 triple3) -> rule4))]
("mouse" "visits" "squirrel" "-")
((triple1 triple3) -> (rule4 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The mouse likes the squirrel.
True
5
proof
[(((((triple1 triple3) -> rule4) triple2) -> rule6))]
("mouse" "likes" "squirrel" "+")
((((triple1 triple3) -> (rule4 % int2)) triple2) -> (rule6 % int1))
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The mouse does not like the squirrel.
False
5
inv-proof
[(((((triple1 triple3) -> rule4) triple2) -> rule6))]
("mouse" "likes" "squirrel" "-")
((((triple1 triple3) -> (rule4 % int2)) triple2) -> (rule6 % int1))
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The mouse is not red.
Unknown
inv-rconc
[@1: The mouse is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "red" "-")
The squirrel visits the squirrel.
Unknown
rconc
[@2: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("squirrel" "visits" "squirrel" "+")
The squirrel is not red.
Unknown
inv-rconc
[@1: The squirrel is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "red" "-")
The squirrel is rough.
Unknown
random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "+")
The squirrel is not blue.
Unknown
inv-random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "-")
The squirrel is young.
Unknown
random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "+")
@0: The mouse needs the squirrel.[(triple1)] The squirrel needs the mouse.[(triple2)] The squirrel visits the mouse.[(triple3)] @1: The mouse visits the squirrel.[(((triple1 triple3) -> rule4))] @2: The mouse likes the squirrel.[(((((triple1 triple3) -> rule4) triple2) -> rule6))]
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple1
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple2
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple3
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
((triple1 triple3) -> (rule4 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
((((triple1 triple3) -> (rule4 % int2)) triple2) -> (rule6 % int1))
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2