The cat is kind. The cat needs the lion. The cat needs the mouse. The lion is round. The mouse is kind. The mouse needs the cat. The mouse visits the cat. If someone needs the mouse then the mouse likes the lion. Nice people are green. If someone needs the cat and they visit the lion then the lion visits the cat. If someone is round and they like the cat then the cat visits the mouse. If someone likes the lion then the lion is green. If someone needs the cat then they need the mouse. If someone visits the cat then the cat visits the lion. If someone is rough and they need the mouse then they like the cat.
The cat is kind.
("cat" "is" "kind" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The lion is round.
("lion" "is" "round" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse needs the cat.
("mouse" "needs" "cat" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
If someone needs the mouse then the mouse likes the lion.
((("someone" "needs" "mouse" "+")) -> ("mouse" "likes" "lion" "+"))
Nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If someone needs the cat and they visit the lion then the lion visits the cat.
((("someone" "needs" "cat" "+") ("someone" "visits" "lion" "+")) -> ("lion" "visits" "cat" "+"))
If someone is round and they like the cat then the cat visits the mouse.
((("someone" "is" "round" "+") ("someone" "likes" "cat" "+")) -> ("cat" "visits" "mouse" "+"))
If someone likes the lion then the lion is green.
((("someone" "likes" "lion" "+")) -> ("lion" "is" "green" "+"))
If someone needs the cat then they need the mouse.
((("someone" "needs" "cat" "+")) -> ("someone" "needs" "mouse" "+"))
If someone visits the cat then the cat visits the lion.
((("someone" "visits" "cat" "+")) -> ("cat" "visits" "lion" "+"))
If someone is rough and they need the mouse then they like the cat.
((("someone" "is" "rough" "+") ("someone" "needs" "mouse" "+")) -> ("someone" "likes" "cat" "+"))
The mouse visits the cat.
True
1
proof
[(triple7)]
("mouse" "visits" "cat" "+")
triple7
The cat is not kind.
False
1
inv-proof
[(triple1)]
("cat" "is" "kind" "-")
triple1
The mouse likes the lion.
True
2
proof
[(((triple3) -> rule1) OR ((((triple6) -> rule6)) -> rule1))]
("mouse" "likes" "lion" "+")
((triple3) -> (rule1 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse does not like the lion.
False
2
inv-proof
[(((triple3) -> rule1) OR ((((triple6) -> rule6)) -> rule1))]
("mouse" "likes" "lion" "-")
((triple3) -> (rule1 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The lion is green.
True
3
proof
[(((((triple3) -> rule1)) -> rule5) OR ((((((triple6) -> rule6)) -> rule1)) -> rule5))]
("lion" "is" "green" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int2
((((((triple6) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int2
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int3
The lion is not green.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule5) OR ((((((triple6) -> rule6)) -> rule1)) -> rule5))]
("lion" "is" "green" "-")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int2
((((((triple6) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int2
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int3
The lion does not visit the cat.
Unknown
inv-rconc
[@1: The lion visits the cat.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "visits" "cat" "-")
The cat is green.
Unknown
rconc
[@1: The cat is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "green" "+")
The lion does not need the mouse.
Unknown
inv-rconc
[@1: The lion needs the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "needs" "mouse" "-")
The mouse is round.
Unknown
random
[@0: The mouse is round.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "round" "+")
The lion is not rough.
Unknown
inv-random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
@0: The cat is kind.[(triple1)] The cat needs the lion.[(triple2)] The cat needs the mouse.[(triple3)] The lion is round.[(triple4)] The mouse is kind.[(triple5)] The mouse needs the cat.[(triple6)] The mouse visits the cat.[(triple7)] @1: The cat visits the lion.[(((triple7) -> rule7))] The mouse likes the lion.[(((triple3) -> rule1) OR ((((triple6) -> rule6)) -> rule1))] The mouse needs the mouse.[(((triple6) -> rule6))] @2: The lion is green.[(((((triple3) -> rule1)) -> rule5) OR ((((((triple6) -> rule6)) -> rule1)) -> rule5))]
The cat is kind.
("cat" "is" "kind" "+")
triple1
The cat needs the lion.
("cat" "needs" "lion" "+")
triple2
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple3
The lion is round.
("lion" "is" "round" "+")
triple4
The mouse is kind.
("mouse" "is" "kind" "+")
triple5
The mouse needs the cat.
("mouse" "needs" "cat" "+")
triple6
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple7
The cat visits the lion.
("cat" "visits" "lion" "+")
((triple7) -> (rule7 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
((triple3) -> (rule1 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int1
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int2
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
((triple6) -> (rule6 % int1))
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int1
The lion is green.
("lion" "is" "green" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int2
((((((triple6) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The mouse likes the lion.
("mouse" "likes" "lion" "+")
int2
The mouse needs the mouse.
("mouse" "needs" "mouse" "+")
int3