The lion eats the tiger. The lion is big. The lion is blue. The lion is cold. The lion is green. The lion is young. The lion needs the tiger. The lion visits the tiger. The tiger eats the lion. The tiger is blue. The tiger is cold. The tiger is green. If someone visits the lion and the lion needs the tiger then the lion eats the tiger. If someone visits the lion and they visit the tiger then the tiger eats the lion. If the lion needs the tiger then the tiger visits the lion. If someone eats the tiger and they visit the tiger then they need the tiger. If someone eats the lion then the lion visits the tiger. If the lion visits the tiger then the tiger is green.
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is young.
("lion" "is" "young" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is green.
("tiger" "is" "green" "+")
If someone visits the lion and the lion needs the tiger then the lion eats the tiger.
((("someone" "visits" "lion" "+") ("lion" "needs" "tiger" "+")) -> ("lion" "eats" "tiger" "+"))
If someone visits the lion and they visit the tiger then the tiger eats the lion.
((("someone" "visits" "lion" "+") ("someone" "visits" "tiger" "+")) -> ("tiger" "eats" "lion" "+"))
If the lion needs the tiger then the tiger visits the lion.
((("lion" "needs" "tiger" "+")) -> ("tiger" "visits" "lion" "+"))
If someone eats the tiger and they visit the tiger then they need the tiger.
((("someone" "eats" "tiger" "+") ("someone" "visits" "tiger" "+")) -> ("someone" "needs" "tiger" "+"))
If someone eats the lion then the lion visits the tiger.
((("someone" "eats" "lion" "+")) -> ("lion" "visits" "tiger" "+"))
If the lion visits the tiger then the tiger is green.
((("lion" "visits" "tiger" "+")) -> ("tiger" "is" "green" "+"))
The lion needs the tiger.
True
1
proof
[(triple7 OR ((triple1 triple8) -> rule4) OR ((triple1 ((triple9) -> rule5)) -> rule4))]
("lion" "needs" "tiger" "+")
triple7
((triple1 triple8) -> (rule4 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
((triple1 ((triple9) -> (rule5 % int2))) -> (rule4 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int2
The lion does not eat the tiger.
False
1
inv-proof
[(triple1 OR ((((triple7) -> rule3) triple7) -> rule1))]
("lion" "eats" "tiger" "-")
triple1
((((triple7) -> (rule3 % int2)) triple7) -> (rule1 % int1))
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int2
The tiger visits the lion.
True
2
proof
[(((triple7) -> rule3) OR ((((triple1 triple8) -> rule4)) -> rule3) OR ((((triple1 ((triple9) -> rule5)) -> rule4)) -> rule3))]
("tiger" "visits" "lion" "+")
((triple7) -> (rule3 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
((((triple1 triple8) -> (rule4 % int2))) -> (rule3 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int2
((((triple1 ((triple9) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int2
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int3
The tiger does not visit the lion.
False
2
inv-proof
[(((triple7) -> rule3) OR ((((triple1 triple8) -> rule4)) -> rule3) OR ((((triple1 ((triple9) -> rule5)) -> rule4)) -> rule3))]
("tiger" "visits" "lion" "-")
((triple7) -> (rule3 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
((((triple1 triple8) -> (rule4 % int2))) -> (rule3 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int2
((((triple1 ((triple9) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int2
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int3
The tiger does not need the tiger.
Unknown
inv-rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "needs" "tiger" "-")
The tiger needs the lion.
Unknown
random
[@0: The tiger needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "lion" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
@0: The lion eats the tiger.[(triple1 OR ((((triple7) -> rule3) triple7) -> rule1))] The lion is big.[(triple2)] The lion is blue.[(triple3)] The lion is cold.[(triple4)] The lion is green.[(triple5)] The lion is young.[(triple6)] The lion needs the tiger.[(triple7 OR ((triple1 triple8) -> rule4) OR ((triple1 ((triple9) -> rule5)) -> rule4))] The lion visits the tiger.[(triple8 OR ((triple9) -> rule5))] The tiger eats the lion.[(triple9)] The tiger is blue.[(triple10)] The tiger is cold.[(triple11)] The tiger is green.[(triple12 OR ((triple8) -> rule6) OR ((((triple9) -> rule5)) -> rule6))] @1: The tiger visits the lion.[(((triple7) -> rule3) OR ((((triple1 triple8) -> rule4)) -> rule3) OR ((((triple1 ((triple9) -> rule5)) -> rule4)) -> rule3))]
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple1
((((triple7) -> (rule3 % int2)) triple7) -> (rule1 % int1))
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int2
The lion is big.
("lion" "is" "big" "+")
triple2
The lion is blue.
("lion" "is" "blue" "+")
triple3
The lion is cold.
("lion" "is" "cold" "+")
triple4
The lion is green.
("lion" "is" "green" "+")
triple5
The lion is young.
("lion" "is" "young" "+")
triple6
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple7
((triple1 triple8) -> (rule4 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
((triple1 ((triple9) -> (rule5 % int2))) -> (rule4 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int2
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple8
((triple9) -> (rule5 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple9
The tiger is blue.
("tiger" "is" "blue" "+")
triple10
The tiger is cold.
("tiger" "is" "cold" "+")
triple11
The tiger is green.
("tiger" "is" "green" "+")
triple12
((triple8) -> (rule6 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((((triple9) -> (rule5 % int2))) -> (rule6 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int2
The tiger visits the lion.
("tiger" "visits" "lion" "+")
((triple7) -> (rule3 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
((((triple1 triple8) -> (rule4 % int2))) -> (rule3 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int2
((((triple1 ((triple9) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int2
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int3