The mouse eats the squirrel. The mouse is young. The mouse needs the squirrel. The mouse visits the squirrel. The squirrel eats the mouse. The squirrel is big. The squirrel is blue. The squirrel is kind. The squirrel is rough. The squirrel is young. The squirrel needs the mouse. The squirrel visits the mouse. If the mouse is young then the mouse eats the squirrel. If something is rough then it needs the mouse. If something is blue and it visits the mouse then it visits the squirrel. If something visits the squirrel and it needs the mouse then the squirrel needs the mouse. If something is rough then it eats the mouse. If something needs the squirrel and it is kind then the squirrel visits the mouse. If something visits the mouse and the mouse eats the squirrel then the squirrel needs the mouse. If something visits the squirrel and it is rough then it eats the squirrel.
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
If the mouse is young then the mouse eats the squirrel.
((("mouse" "is" "young" "+")) -> ("mouse" "eats" "squirrel" "+"))
If something is rough then it needs the mouse.
((("something" "is" "rough" "+")) -> ("something" "needs" "mouse" "+"))
If something is blue and it visits the mouse then it visits the squirrel.
((("something" "is" "blue" "+") ("something" "visits" "mouse" "+")) -> ("something" "visits" "squirrel" "+"))
If something visits the squirrel and it needs the mouse then the squirrel needs the mouse.
((("something" "visits" "squirrel" "+") ("something" "needs" "mouse" "+")) -> ("squirrel" "needs" "mouse" "+"))
If something is rough then it eats the mouse.
((("something" "is" "rough" "+")) -> ("something" "eats" "mouse" "+"))
If something needs the squirrel and it is kind then the squirrel visits the mouse.
((("something" "needs" "squirrel" "+") ("something" "is" "kind" "+")) -> ("squirrel" "visits" "mouse" "+"))
If something visits the mouse and the mouse eats the squirrel then the squirrel needs the mouse.
((("something" "visits" "mouse" "+") ("mouse" "eats" "squirrel" "+")) -> ("squirrel" "needs" "mouse" "+"))
If something visits the squirrel and it is rough then it eats the squirrel.
((("something" "visits" "squirrel" "+") ("something" "is" "rough" "+")) -> ("something" "eats" "squirrel" "+"))
The squirrel is rough.
True
1
proof
[(triple9)]
("squirrel" "is" "rough" "+")
triple9
The squirrel is not big.
False
1
inv-proof
[(triple6)]
("squirrel" "is" "big" "-")
triple6
The squirrel visits the squirrel.
True
3
proof
[(((triple7 triple12) -> rule3))]
("squirrel" "visits" "squirrel" "+")
((triple7 triple12) -> (rule3 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel does not visit the squirrel.
False
3
inv-proof
[(((triple7 triple12) -> rule3))]
("squirrel" "visits" "squirrel" "-")
((triple7 triple12) -> (rule3 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel eats the squirrel.
True
5
proof
[(((((triple7 triple12) -> rule3) triple9) -> rule8))]
("squirrel" "eats" "squirrel" "+")
((((triple7 triple12) -> (rule3 % int2)) triple9) -> (rule8 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The squirrel does not eat the squirrel.
False
5
inv-proof
[(((((triple7 triple12) -> rule3) triple9) -> rule8))]
("squirrel" "eats" "squirrel" "-")
((((triple7 triple12) -> (rule3 % int2)) triple9) -> (rule8 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The mouse does not eat the mouse.
Unknown
inv-rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "eats" "mouse" "-")
The mouse needs the mouse.
Unknown
rconc
[@1: The mouse needs the mouse.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "needs" "mouse" "+")
The mouse does not visit the mouse.
Unknown
inv-random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "-")
The mouse is big.
Unknown
random
[@0: The mouse is big.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "big" "+")
The squirrel does not need the squirrel.
Unknown
inv-random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
@0: The mouse eats the squirrel.[(triple1 OR ((triple2) -> rule1))] The mouse is young.[(triple2)] The mouse needs the squirrel.[(triple3)] The mouse visits the squirrel.[(triple4)] The squirrel eats the mouse.[(triple5 OR ((triple9) -> rule5))] The squirrel is big.[(triple6)] The squirrel is blue.[(triple7)] The squirrel is kind.[(triple8)] The squirrel is rough.[(triple9)] The squirrel is young.[(triple10)] The squirrel needs the mouse.[(triple11 OR ((triple9) -> rule2) OR ((triple12 triple1) -> rule7) OR ((triple12 ((triple2) -> rule1)) -> rule7))] The squirrel visits the mouse.[(triple12)] @1: The squirrel visits the squirrel.[(((triple7 triple12) -> rule3))] @2: The squirrel eats the squirrel.[(((((triple7 triple12) -> rule3) triple9) -> rule8))]
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple1
((triple2) -> (rule1 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
triple2
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple3
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple4
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple5
((triple9) -> (rule5 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
triple6
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple7
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple8
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple9
The squirrel is young.
("squirrel" "is" "young" "+")
triple10
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple11
((triple9) -> (rule2 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
((triple12 triple1) -> (rule7 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
((triple12 ((triple2) -> (rule1 % int2))) -> (rule7 % int1))
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple12
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((triple7 triple12) -> (rule3 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((((triple7 triple12) -> (rule3 % int2)) triple9) -> (rule8 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2