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