The lion is nice. The tiger needs the lion. Blue people are young. If someone eats the lion then the lion eats the tiger. Green people are blue. If someone eats the tiger then they are green. If someone likes the lion and the lion needs the tiger then the tiger needs the lion. If someone eats the lion and they are nice then they are rough. If someone eats the tiger and the tiger is nice then the tiger needs the lion. If someone is nice then they eat the tiger.
The lion is nice.
("lion" "is" "nice" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
Blue people are young.
((("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
If someone eats the lion then the lion eats the tiger.
((("someone" "eats" "lion" "+")) -> ("lion" "eats" "tiger" "+"))
Green people are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If someone eats the tiger then they are green.
((("someone" "eats" "tiger" "+")) -> ("someone" "is" "green" "+"))
If someone likes the lion and the lion needs the tiger then the tiger needs the lion.
((("someone" "likes" "lion" "+") ("lion" "needs" "tiger" "+")) -> ("tiger" "needs" "lion" "+"))
If someone eats the lion and they are nice then they are rough.
((("someone" "eats" "lion" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone eats the tiger and the tiger is nice then the tiger needs the lion.
((("someone" "eats" "tiger" "+") ("tiger" "is" "nice" "+")) -> ("tiger" "needs" "lion" "+"))
If someone is nice then they eat the tiger.
((("someone" "is" "nice" "+")) -> ("someone" "eats" "tiger" "+"))
The tiger needs the lion.
True
1
proof
[(triple2)]
("tiger" "needs" "lion" "+")
triple2
The tiger does not need the lion.
False
1
inv-proof
[(triple2)]
("tiger" "needs" "lion" "-")
triple2
The lion eats the tiger.
True
2
proof
[(((triple1) -> rule8))]
("lion" "eats" "tiger" "+")
((triple1) -> (rule8 % int1))
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int1
The lion does not eat the tiger.
False
2
inv-proof
[(((triple1) -> rule8))]
("lion" "eats" "tiger" "-")
((triple1) -> (rule8 % int1))
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int1
The lion is green.
True
3
proof
[(((((triple1) -> rule8)) -> rule4))]
("lion" "is" "green" "+")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int2
The lion is not green.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule4))]
("lion" "is" "green" "-")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int2
The lion is blue.
True
4
proof
[(((((((triple1) -> rule8)) -> rule4)) -> rule3))]
("lion" "is" "blue" "+")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int3
The lion is not blue.
False
4
inv-proof
[(((((((triple1) -> rule8)) -> rule4)) -> rule3))]
("lion" "is" "blue" "-")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int3
The tiger is not young.
Unknown
inv-rconc
[@4: The tiger is young.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule4 <- rule8 <- FAIL)]]
("tiger" "is" "young" "-")
The tiger is green.
Unknown
rconc
[@2: The tiger is green.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("tiger" "is" "green" "+")
The tiger does not eat the tiger.
Unknown
inv-rconc
[@1: The tiger eats the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "eats" "tiger" "-")
The tiger is rough.
Unknown
rconc
[@1: The tiger is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "is" "rough" "+")
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 lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The lion likes the tiger.
Unknown
random
[@0: The lion likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "tiger" "+")
@0: The lion is nice.[(triple1)] The tiger needs the lion.[(triple2)] @1: The lion eats the tiger.[(((triple1) -> rule8))] @2: The lion is green.[(((((triple1) -> rule8)) -> rule4))] @3: The lion is blue.[(((((((triple1) -> rule8)) -> rule4)) -> rule3))] @4: The lion is young.[(((((((((triple1) -> rule8)) -> rule4)) -> rule3)) -> rule1))]
The lion is nice.
("lion" "is" "nice" "+")
triple1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple2
The lion eats the tiger.
("lion" "eats" "tiger" "+")
((triple1) -> (rule8 % int1))
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int1
The lion is green.
("lion" "is" "green" "+")
((((triple1) -> (rule8 % int2))) -> (rule4 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
((((((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int3
The lion is young.
("lion" "is" "young" "+")
((((((((triple1) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion is green.
("lion" "is" "green" "+")
int3
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int4