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