The bear needs the lion. The cat is cold. The lion eats the bear. The tiger needs the cat. If someone eats the lion then the lion is nice. If someone needs the lion and the lion is kind then the lion visits the bear. If someone needs the lion then they are kind. If the bear is kind then the bear eats the lion. If someone is kind and young then they eat the lion. If someone is kind then they eat the tiger. If someone visits the bear and they eat the lion then they are nice. If the cat visits the bear and the cat needs the tiger then the bear eats the tiger.
The bear needs the lion.
("bear" "needs" "lion" "+")
The cat is cold.
("cat" "is" "cold" "+")
The lion eats the bear.
("lion" "eats" "bear" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
If someone eats the lion then the lion is nice.
((("someone" "eats" "lion" "+")) -> ("lion" "is" "nice" "+"))
If someone needs the lion and the lion is kind then the lion visits the bear.
((("someone" "needs" "lion" "+") ("lion" "is" "kind" "+")) -> ("lion" "visits" "bear" "+"))
If someone needs the lion then they are kind.
((("someone" "needs" "lion" "+")) -> ("someone" "is" "kind" "+"))
If the bear is kind then the bear eats the lion.
((("bear" "is" "kind" "+")) -> ("bear" "eats" "lion" "+"))
If someone is kind and young then they eat the lion.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "eats" "lion" "+"))
If someone is kind then they eat the tiger.
((("someone" "is" "kind" "+")) -> ("someone" "eats" "tiger" "+"))
If someone visits the bear and they eat the lion then they are nice.
((("someone" "visits" "bear" "+") ("someone" "eats" "lion" "+")) -> ("someone" "is" "nice" "+"))
If the cat visits the bear and the cat needs the tiger then the bear eats the tiger.
((("cat" "visits" "bear" "+") ("cat" "needs" "tiger" "+")) -> ("bear" "eats" "tiger" "+"))
The bear needs the lion.
True
1
proof
[(triple1)]
("bear" "needs" "lion" "+")
triple1
The tiger does not need the cat.
False
1
inv-proof
[(triple4)]
("tiger" "needs" "cat" "-")
triple4
The bear is kind.
True
2
proof
[(((triple1) -> rule3))]
("bear" "is" "kind" "+")
((triple1) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is not kind.
False
2
inv-proof
[(((triple1) -> rule3))]
("bear" "is" "kind" "-")
((triple1) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear eats the lion.
True
3
proof
[(((((triple1) -> rule3)) -> rule4))]
("bear" "eats" "lion" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The bear eats the lion.
("bear" "eats" "lion" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
The bear does not eat the tiger.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule6))]
("bear" "eats" "tiger" "-")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
The lion is nice.
True
4
proof
[(((((((triple1) -> rule3)) -> rule4)) -> rule1))]
("lion" "is" "nice" "+")
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The bear eats the lion.
("bear" "eats" "lion" "+")
int2
The bear is kind.
("bear" "is" "kind" "+")
int3
The lion is not nice.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule4)) -> rule1))]
("lion" "is" "nice" "-")
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The bear eats the lion.
("bear" "eats" "lion" "+")
int2
The bear is kind.
("bear" "is" "kind" "+")
int3
The bear is not nice.
Unknown
inv-rconc
[@1: The bear is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "is" "nice" "-")
The cat is nice.
Unknown
rconc
[@1: The cat is nice.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "is" "nice" "+")
The cat does not eat the lion.
Unknown
inv-rconc
[@1: The cat eats the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "eats" "lion" "-")
The lion eats the tiger.
Unknown
rconc
[@2: The lion eats the tiger.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("lion" "eats" "tiger" "+")
The bear does not visit the bear.
Unknown
inv-random
[@0: The bear visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "bear" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The lion is not cold.
Unknown
inv-random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "-")
The tiger visits the cat.
Unknown
random
[@0: The tiger visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "cat" "+")
@0: The bear needs the lion.[(triple1)] The cat is cold.[(triple2)] The lion eats the bear.[(triple3)] The tiger needs the cat.[(triple4)] @1: The bear is kind.[(((triple1) -> rule3))] @2: The bear eats the lion.[(((((triple1) -> rule3)) -> rule4))] The bear eats the tiger.[(((((triple1) -> rule3)) -> rule6))] @3: The lion is nice.[(((((((triple1) -> rule3)) -> rule4)) -> rule1))]
The bear needs the lion.
("bear" "needs" "lion" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The lion eats the bear.
("lion" "eats" "bear" "+")
triple3
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple4
The bear is kind.
("bear" "is" "kind" "+")
((triple1) -> (rule3 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear eats the lion.
("bear" "eats" "lion" "+")
((((triple1) -> (rule3 % int2))) -> (rule4 % int1))
The bear eats the lion.
("bear" "eats" "lion" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
The bear eats the tiger.
("bear" "eats" "tiger" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The bear eats the tiger.
("bear" "eats" "tiger" "+")
int1
The bear is kind.
("bear" "is" "kind" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
((((((triple1) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The bear eats the lion.
("bear" "eats" "lion" "+")
int2
The bear is kind.
("bear" "is" "kind" "+")
int3