The lion is nice. The rabbit does not chase the lion. The rabbit chases the tiger. The rabbit does not eat the lion. The rabbit is young. The rabbit needs the tiger. The tiger is not nice. If the rabbit does not chase the lion then the lion is not kind. If something chases the lion then it is big. If something is young and it needs the tiger then the tiger needs the lion. If the tiger needs the lion then the tiger chases the lion. If something is nice then it chases the tiger. If something eats the lion and it does not chase the rabbit then the lion does not eat the tiger. If the lion is not kind then the lion eats the rabbit. If something eats the lion and it does not eat the tiger then it is rough.
The lion is nice.
("lion" "is" "nice" "+")
The rabbit does not chase the lion.
("rabbit" "chases" "lion" "-")
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit does not eat the lion.
("rabbit" "eats" "lion" "-")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The tiger is not nice.
("tiger" "is" "nice" "-")
If the rabbit does not chase the lion then the lion is not kind.
((("rabbit" "chases" "lion" "~")) -> ("lion" "is" "kind" "-"))
If something chases the lion then it is big.
((("something" "chases" "lion" "+")) -> ("something" "is" "big" "+"))
If something is young and it needs the tiger then the tiger needs the lion.
((("something" "is" "young" "+") ("something" "needs" "tiger" "+")) -> ("tiger" "needs" "lion" "+"))
If the tiger needs the lion then the tiger chases the lion.
((("tiger" "needs" "lion" "+")) -> ("tiger" "chases" "lion" "+"))
If something is nice then it chases the tiger.
((("something" "is" "nice" "+")) -> ("something" "chases" "tiger" "+"))
If something eats the lion and it does not chase the rabbit then the lion does not eat the tiger.
((("something" "eats" "lion" "+") ("something" "chases" "rabbit" "~")) -> ("lion" "eats" "tiger" "-"))
If the lion is not kind then the lion eats the rabbit.
((("lion" "is" "kind" "~")) -> ("lion" "eats" "rabbit" "+"))
If something eats the lion and it does not eat the tiger then it is rough.
((("something" "eats" "lion" "+") ("something" "eats" "tiger" "~")) -> ("something" "is" "rough" "+"))
The rabbit needs the tiger.
True
1
proof
[(triple6)]
("rabbit" "needs" "tiger" "+")
triple6
The rabbit is not young.
False
1
inv-proof
[(triple5)]
("rabbit" "is" "young" "-")
triple5
The lion chases the tiger.
True
2
proof
[(((triple1) -> rule5))]
("lion" "chases" "tiger" "+")
((triple1) -> (rule5 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The lion does not chase the tiger.
False
2
inv-proof
[(((triple1) -> rule5))]
("lion" "chases" "tiger" "-")
((triple1) -> (rule5 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The tiger chases the lion.
True
4
proof
[(((((triple5 triple6) -> rule3)) -> rule4))]
("tiger" "chases" "lion" "+")
((((triple5 triple6) -> (rule3 % int2))) -> (rule4 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int2
The tiger does not chase the lion.
False
4
inv-proof
[(((((triple5 triple6) -> rule3)) -> rule4))]
("tiger" "chases" "lion" "-")
((((triple5 triple6) -> (rule3 % int2))) -> (rule4 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int2
The tiger is big.
True
5
proof
[(((((((triple5 triple6) -> rule3)) -> rule4)) -> rule2))]
("tiger" "is" "big" "+")
((((((triple5 triple6) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int2
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int3
The tiger is not big.
False
5
inv-proof
[(((((((triple5 triple6) -> rule3)) -> rule4)) -> rule2))]
("tiger" "is" "big" "-")
((((((triple5 triple6) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int2
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int3
The lion is not rough.
Unknown
inv-rconc
[@1: The lion is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "is" "rough" "-")
The lion is big.
Unknown
rconc
[@1: The lion is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "big" "+")
The tiger is not rough.
Unknown
inv-rconc
[@1: The tiger is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "is" "rough" "-")
The tiger chases the tiger.
Unknown
rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "chases" "tiger" "+")
The tiger does not need the rabbit.
Unknown
inv-random
[@0: The tiger needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "rabbit" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
The rabbit does not eat the tiger.
Unknown
inv-random
[@0: The rabbit eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "tiger" "-")
The tiger eats the rabbit.
Unknown
random
[@0: The tiger eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "rabbit" "+")
@0: The lion is nice.[(triple1)] The rabbit chases the tiger.[(triple3)] The rabbit does not chase the lion.[(triple2)] The rabbit does not eat the lion.[(triple4)] The rabbit is young.[(triple5)] The rabbit needs the tiger.[(triple6)] The tiger is not nice.[(triple7)] @1: The lion chases the tiger.[(((triple1) -> rule5))] The lion is not kind.[(((triple2) -> rule1))] The tiger needs the lion.[(((triple5 triple6) -> rule3))] @2: The lion eats the rabbit.[(((((triple2) -> rule1)) -> rule7))] The tiger chases the lion.[(((((triple5 triple6) -> rule3)) -> rule4))] @3: The tiger is big.[(((((((triple5 triple6) -> rule3)) -> rule4)) -> rule2))]
The lion is nice.
("lion" "is" "nice" "+")
triple1
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple3
The rabbit does not chase the lion.
("rabbit" "chases" "lion" "-")
triple2
The rabbit does not eat the lion.
("rabbit" "eats" "lion" "-")
triple4
The rabbit is young.
("rabbit" "is" "young" "+")
triple5
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple6
The tiger is not nice.
("tiger" "is" "nice" "-")
triple7
The lion chases the tiger.
("lion" "chases" "tiger" "+")
((triple1) -> (rule5 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The lion is not kind.
("lion" "is" "kind" "-")
((triple2) -> (rule1 % int1))
The lion is not kind.
("lion" "is" "kind" "-")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
((triple5 triple6) -> (rule3 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
((((triple2) -> (rule1 % int2))) -> (rule7 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The lion is not kind.
("lion" "is" "kind" "-")
int2
The tiger chases the lion.
("tiger" "chases" "lion" "+")
((((triple5 triple6) -> (rule3 % int2))) -> (rule4 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
((((((triple5 triple6) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int2
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int3