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