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