The cat chases the lion. The cat does not chase the mouse. The cat needs the lion. The cat needs the mouse. The cat visits the mouse. The lion chases the cat. The lion is green. The lion is not kind. The lion is nice. The lion needs the cat. The lion does not visit the cat. The lion visits the mouse. The mouse is kind. The mouse is nice. The mouse needs the lion. The mouse does not visit the cat. If someone visits the mouse then the mouse is young. If someone chases the mouse then the mouse is not young. If someone is kind then they need the cat. If someone is kind then they need the cat. If someone is young then they visit the lion. If the mouse needs the lion then the mouse does not chase the lion. If someone is green and they need the lion then the lion visits the cat. If the lion visits the cat and the cat needs the mouse then the lion chases the cat.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat does not chase the mouse.
("cat" "chases" "mouse" "-")
The cat needs the lion.
("cat" "needs" "lion" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is not kind.
("lion" "is" "kind" "-")
The lion is nice.
("lion" "is" "nice" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion does not visit the cat.
("lion" "visits" "cat" "-")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The mouse does not visit the cat.
("mouse" "visits" "cat" "-")
If someone visits the mouse then the mouse is young.
((("someone" "visits" "mouse" "+")) -> ("mouse" "is" "young" "+"))
If someone chases the mouse then the mouse is not young.
((("someone" "chases" "mouse" "+")) -> ("mouse" "is" "young" "-"))
If someone is kind then they need the cat.
((("someone" "is" "kind" "+")) -> ("someone" "needs" "cat" "+"))
If someone is kind then they need the cat.
((("someone" "is" "kind" "+")) -> ("someone" "needs" "cat" "+"))
If someone is young then they visit the lion.
((("someone" "is" "young" "+")) -> ("someone" "visits" "lion" "+"))
If the mouse needs the lion then the mouse does not chase the lion.
((("mouse" "needs" "lion" "+")) -> ("mouse" "chases" "lion" "-"))
If someone is green and they need the lion then the lion visits the cat.
((("someone" "is" "green" "+") ("someone" "needs" "lion" "+")) -> ("lion" "visits" "cat" "+"))
If the lion visits the cat and the cat needs the mouse then the lion chases the cat.
((("lion" "visits" "cat" "+") ("cat" "needs" "mouse" "+")) -> ("lion" "chases" "cat" "+"))
The lion is not kind.
True
1
proof
[(triple8)]
("lion" "is" "kind" "-")
triple8
The lion is not green.
False
1
inv-proof
[(triple7)]
("lion" "is" "green" "-")
triple7
The mouse needs the cat.
True
2
proof
[(((triple13) -> rule3) OR ((triple13) -> rule4))]
("mouse" "needs" "cat" "+")
((triple13) -> (rule3 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1
((triple13) -> (rule4 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1
The mouse does not need the cat.
False
2
inv-proof
[(((triple13) -> rule3) OR ((triple13) -> rule4))]
("mouse" "needs" "cat" "-")
((triple13) -> (rule3 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1
((triple13) -> (rule4 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1
The mouse visits the lion.
True
3
proof
[(((((triple12) -> rule1)) -> rule5) OR ((((triple5) -> rule1)) -> rule5))]
("mouse" "visits" "lion" "+")
((((triple12) -> (rule1 % int2))) -> (rule5 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
((((triple5) -> (rule1 % int2))) -> (rule5 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The mouse does not visit the lion.
False
3
inv-proof
[(((((triple12) -> rule1)) -> rule5) OR ((((triple5) -> rule1)) -> rule5))]
("mouse" "visits" "lion" "-")
((((triple12) -> (rule1 % int2))) -> (rule5 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
((((triple5) -> (rule1 % int2))) -> (rule5 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
The cat does not need the cat.
Unknown
inv-rconc
[@1: The cat needs the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "needs" "cat" "-")
The lion visits the lion.
Unknown
rconc
[@1: The lion visits the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "visits" "lion" "+")
The cat does not visit the lion.
Unknown
inv-rconc
[@1: The cat visits the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "visits" "lion" "-")
The cat is green.
Unknown
random
[@0: The cat is green.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "green" "+")
The cat is not rough.
Unknown
inv-random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "-")
The lion chases the mouse.
Unknown
random
[@0: The lion chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "mouse" "+")
@0: The cat chases the lion.[(triple1)] The cat does not chase the mouse.[(triple2)] The cat needs the lion.[(triple3)] The cat needs the mouse.[(triple4)] The cat visits the mouse.[(triple5)] The lion chases the cat.[(triple6)] The lion does not visit the cat.[(triple11)] The lion is green.[(triple7)] The lion is nice.[(triple9)] The lion is not kind.[(triple8)] The lion needs the cat.[(triple10)] The lion visits the mouse.[(triple12)] The mouse does not visit the cat.[(triple16)] The mouse is kind.[(triple13)] The mouse is nice.[(triple14)] The mouse needs the lion.[(triple15)] @1: The mouse does not chase the lion.[(((triple15) -> rule6))] The mouse is young.[(((triple12) -> rule1) OR ((triple5) -> rule1))] The mouse needs the cat.[(((triple13) -> rule3) OR ((triple13) -> rule4))] @2: The mouse visits the lion.[(((((triple12) -> rule1)) -> rule5) OR ((((triple5) -> rule1)) -> rule5))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The cat does not chase the mouse.
("cat" "chases" "mouse" "-")
triple2
The cat needs the lion.
("cat" "needs" "lion" "+")
triple3
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple4
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple5
The lion chases the cat.
("lion" "chases" "cat" "+")
triple6
The lion does not visit the cat.
("lion" "visits" "cat" "-")
triple11
The lion is green.
("lion" "is" "green" "+")
triple7
The lion is nice.
("lion" "is" "nice" "+")
triple9
The lion is not kind.
("lion" "is" "kind" "-")
triple8
The lion needs the cat.
("lion" "needs" "cat" "+")
triple10
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple12
The mouse does not visit the cat.
("mouse" "visits" "cat" "-")
triple16
The mouse is kind.
("mouse" "is" "kind" "+")
triple13
The mouse is nice.
("mouse" "is" "nice" "+")
triple14
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple15
The mouse does not chase the lion.
("mouse" "chases" "lion" "-")
((triple15) -> (rule6 % int1))
The mouse does not chase the lion.
("mouse" "chases" "lion" "-")
int1
The mouse is young.
("mouse" "is" "young" "+")
((triple12) -> (rule1 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
((triple5) -> (rule1 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse needs the cat.
("mouse" "needs" "cat" "+")
((triple13) -> (rule3 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1
((triple13) -> (rule4 % int1))
The mouse needs the cat.
("mouse" "needs" "cat" "+")
int1
The mouse visits the lion.
("mouse" "visits" "lion" "+")
((((triple12) -> (rule1 % int2))) -> (rule5 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2
((((triple5) -> (rule1 % int2))) -> (rule5 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
int2