The lion is red. The tiger sees the lion. If the lion is red then the lion sees the tiger. If something sees the tiger then the tiger needs the lion. If something needs the lion and the lion sees the tiger then the lion visits the tiger.
The lion is red.
("lion" "is" "red" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If the lion is red then the lion sees the tiger.
((("lion" "is" "red" "+")) -> ("lion" "sees" "tiger" "+"))
If something sees the tiger then the tiger needs the lion.
((("something" "sees" "tiger" "+")) -> ("tiger" "needs" "lion" "+"))
If something needs the lion and the lion sees the tiger then the lion visits the tiger.
((("something" "needs" "lion" "+") ("lion" "sees" "tiger" "+")) -> ("lion" "visits" "tiger" "+"))
The tiger sees the lion.
True
1
proof
[(triple2)]
("tiger" "sees" "lion" "+")
triple2
The tiger does not see the lion.
False
1
inv-proof
[(triple2)]
("tiger" "sees" "lion" "-")
triple2
The lion sees the tiger.
True
2
proof
[(((triple1) -> rule1))]
("lion" "sees" "tiger" "+")
((triple1) -> (rule1 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The lion does not see the tiger.
False
2
inv-proof
[(((triple1) -> rule1))]
("lion" "sees" "tiger" "-")
((triple1) -> (rule1 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The tiger needs the lion.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("tiger" "needs" "lion" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The tiger does not need the lion.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("tiger" "needs" "lion" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The lion visits the tiger.
True
6
proof
[(((((((triple1) -> rule1)) -> rule2) ((triple1) -> rule1)) -> rule3))]
("lion" "visits" "tiger" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2)) ((triple1) -> (rule1 % int3))) -> (rule3 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3
The lion does not visit the tiger.
False
6
inv-proof
[(((((((triple1) -> rule1)) -> rule2) ((triple1) -> rule1)) -> rule3))]
("lion" "visits" "tiger" "-")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2)) ((triple1) -> (rule1 % int3))) -> (rule3 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3
The tiger is not cold.
Unknown
inv-random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
The tiger is not big.
Unknown
inv-random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "-")
The lion is green.
Unknown
random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "+")
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 needs the tiger.
Unknown
random
[@0: The lion needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "tiger" "+")
@0: The lion is red.[(triple1)] The tiger sees the lion.[(triple2)] @1: The lion sees the tiger.[(((triple1) -> rule1))] @2: The tiger needs the lion.[(((((triple1) -> rule1)) -> rule2))] @3: The lion visits the tiger.[(((((((triple1) -> rule1)) -> rule2) ((triple1) -> rule1)) -> rule3))]
The lion is red.
("lion" "is" "red" "+")
triple1
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
((triple1) -> (rule1 % int1))
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int2
The lion visits the tiger.
("lion" "visits" "tiger" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2)) ((triple1) -> (rule1 % int3))) -> (rule3 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int2
The lion sees the tiger.
("lion" "sees" "tiger" "+")
int3