The lion eats the tiger. The tiger needs the lion. The tiger visits the lion. If something needs the tiger and the tiger needs the lion then the tiger is round. Blue things are round. If something is kind then it needs the tiger. If the lion eats the tiger then the tiger needs the lion. If the tiger needs the lion and the tiger eats the lion then the tiger is blue. If something needs the lion then the lion is kind.
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If something needs the tiger and the tiger needs the lion then the tiger is round.
((("something" "needs" "tiger" "+") ("tiger" "needs" "lion" "+")) -> ("tiger" "is" "round" "+"))
Blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If something is kind then it needs the tiger.
((("something" "is" "kind" "+")) -> ("something" "needs" "tiger" "+"))
If the lion eats the tiger then the tiger needs the lion.
((("lion" "eats" "tiger" "+")) -> ("tiger" "needs" "lion" "+"))
If the tiger needs the lion and the tiger eats the lion then the tiger is blue.
((("tiger" "needs" "lion" "+") ("tiger" "eats" "lion" "+")) -> ("tiger" "is" "blue" "+"))
If something needs the lion then the lion is kind.
((("something" "needs" "lion" "+")) -> ("lion" "is" "kind" "+"))
The tiger visits the lion.
True
1
proof
[(triple3)]
("tiger" "visits" "lion" "+")
triple3
The tiger does not need the lion.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule4))]
("tiger" "needs" "lion" "-")
triple2
((triple1) -> (rule4 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The lion is kind.
True
2
proof
[(((triple2) -> rule6) OR ((((triple1) -> rule4)) -> rule6))]
("lion" "is" "kind" "+")
((triple2) -> (rule6 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int2
The lion is not kind.
False
2
inv-proof
[(((triple2) -> rule6) OR ((((triple1) -> rule4)) -> rule6))]
("lion" "is" "kind" "-")
((triple2) -> (rule6 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int2
The lion needs the tiger.
True
3
proof
[(((((triple2) -> rule6)) -> rule3) OR ((((((triple1) -> rule4)) -> rule6)) -> rule3))]
("lion" "needs" "tiger" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int3
The lion does not need the tiger.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule3) OR ((((((triple1) -> rule4)) -> rule6)) -> rule3))]
("lion" "needs" "tiger" "-")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int3
The tiger is not blue.
Unknown
inv-rconc
[@1: The tiger is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "is" "blue" "-")
The lion is round.
Unknown
rconc
[@1: The lion is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "round" "+")
The tiger does not need the tiger.
Unknown
inv-rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "needs" "tiger" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
The lion does not visit the lion.
Unknown
inv-random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
@0: The lion eats the tiger.[(triple1)] The tiger needs the lion.[(triple2 OR ((triple1) -> rule4))] The tiger visits the lion.[(triple3)] @1: The lion is kind.[(((triple2) -> rule6) OR ((((triple1) -> rule4)) -> rule6))] @2: The lion needs the tiger.[(((((triple2) -> rule6)) -> rule3) OR ((((((triple1) -> rule4)) -> rule6)) -> rule3))] @3: The tiger is round.[(((((((triple2) -> rule6)) -> rule3) triple2) -> rule1) OR ((((((triple2) -> rule6)) -> rule3) ((triple1) -> rule4)) -> rule1) OR ((((((((triple1) -> rule4)) -> rule6)) -> rule3) triple2) -> rule1) OR ((((((((triple1) -> rule4)) -> rule6)) -> rule3) ((triple1) -> rule4)) -> rule1))]
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple2
((triple1) -> (rule4 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple3
The lion is kind.
("lion" "is" "kind" "+")
((triple2) -> (rule6 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int2
The lion needs the tiger.
("lion" "needs" "tiger" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int3
The tiger is round.
("tiger" "is" "round" "+")
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2)) triple2) -> (rule1 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((((triple2) -> (rule6 % int4))) -> (rule3 % int3)) ((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int2
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int3
The lion is kind.
("lion" "is" "kind" "+")
int4
((((((((triple1) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule3 % int2)) triple2) -> (rule1 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int4
((((((((triple1) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule3 % int2)) ((triple1) -> (rule4 % int4))) -> (rule1 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The lion needs the tiger.
("lion" "needs" "tiger" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int4