The bear sees the lion. The lion is nice. The squirrel is kind. The tiger is nice. If something needs the squirrel then it visits the bear. If something needs the tiger and it visits the tiger then the tiger is round. If something sees the bear and it visits the tiger then the bear needs the tiger. If something is round then it needs the squirrel. If something sees the lion then the lion is round. If the tiger needs the lion then the tiger visits the squirrel.
The bear sees the lion.
("bear" "sees" "lion" "+")
The lion is nice.
("lion" "is" "nice" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
If something needs the squirrel then it visits the bear.
((("something" "needs" "squirrel" "+")) -> ("something" "visits" "bear" "+"))
If something needs the tiger and it visits the tiger then the tiger is round.
((("something" "needs" "tiger" "+") ("something" "visits" "tiger" "+")) -> ("tiger" "is" "round" "+"))
If something sees the bear and it visits the tiger then the bear needs the tiger.
((("something" "sees" "bear" "+") ("something" "visits" "tiger" "+")) -> ("bear" "needs" "tiger" "+"))
If something is round then it needs the squirrel.
((("something" "is" "round" "+")) -> ("something" "needs" "squirrel" "+"))
If something sees the lion then the lion is round.
((("something" "sees" "lion" "+")) -> ("lion" "is" "round" "+"))
If the tiger needs the lion then the tiger visits the squirrel.
((("tiger" "needs" "lion" "+")) -> ("tiger" "visits" "squirrel" "+"))
The squirrel is kind.
True
1
proof
[(triple3)]
("squirrel" "is" "kind" "+")
triple3
The bear does not see the lion.
False
1
inv-proof
[(triple1)]
("bear" "sees" "lion" "-")
triple1
The lion is round.
True
2
proof
[(((triple1) -> rule5))]
("lion" "is" "round" "+")
((triple1) -> (rule5 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is not round.
False
2
inv-proof
[(((triple1) -> rule5))]
("lion" "is" "round" "-")
((triple1) -> (rule5 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion needs the squirrel.
True
3
proof
[(((((triple1) -> rule5)) -> rule4))]
("lion" "needs" "squirrel" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion does not need the squirrel.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule4))]
("lion" "needs" "squirrel" "-")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion visits the bear.
True
4
proof
[(((((((triple1) -> rule5)) -> rule4)) -> rule1))]
("lion" "visits" "bear" "+")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int2
The lion is round.
("lion" "is" "round" "+")
int3
The lion does not visit the bear.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule4)) -> rule1))]
("lion" "visits" "bear" "-")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int2
The lion is round.
("lion" "is" "round" "+")
int3
The tiger is not round.
Unknown
inv-rconc
[@1: The tiger is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "round" "-")
The squirrel visits the bear.
Unknown
rconc
[@2: The squirrel visits the bear.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("squirrel" "visits" "bear" "+")
The squirrel does not need the squirrel.
Unknown
inv-rconc
[@1: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "needs" "squirrel" "-")
The tiger needs the squirrel.
Unknown
rconc
[@2: The tiger needs the squirrel.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("tiger" "needs" "squirrel" "+")
The bear does not see the squirrel.
Unknown
inv-random
[@0: The bear sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "squirrel" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
The tiger is not kind.
Unknown
inv-random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "-")
The squirrel is cold.
Unknown
random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "+")
@0: The bear sees the lion.[(triple1)] The lion is nice.[(triple2)] The squirrel is kind.[(triple3)] The tiger is nice.[(triple4)] @1: The lion is round.[(((triple1) -> rule5))] @2: The lion needs the squirrel.[(((((triple1) -> rule5)) -> rule4))] @3: The lion visits the bear.[(((((((triple1) -> rule5)) -> rule4)) -> rule1))]
The bear sees the lion.
("bear" "sees" "lion" "+")
triple1
The lion is nice.
("lion" "is" "nice" "+")
triple2
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple3
The tiger is nice.
("tiger" "is" "nice" "+")
triple4
The lion is round.
("lion" "is" "round" "+")
((triple1) -> (rule5 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion visits the bear.
("lion" "visits" "bear" "+")
((((((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The lion visits the bear.
("lion" "visits" "bear" "+")
int1
The lion needs the squirrel.
("lion" "needs" "squirrel" "+")
int2
The lion is round.
("lion" "is" "round" "+")
int3