The lion is young. The tiger chases the lion. If someone is young then they see the lion. If someone sees the lion then they do not chase the tiger.
The lion is young.
("lion" "is" "young" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
If someone is young then they see the lion.
((("someone" "is" "young" "+")) -> ("someone" "sees" "lion" "+"))
If someone sees the lion then they do not chase the tiger.
((("someone" "sees" "lion" "+")) -> ("someone" "chases" "tiger" "-"))
The tiger chases the lion.
True
1
proof
[(triple2)]
("tiger" "chases" "lion" "+")
triple2
The lion is not young.
False
1
inv-proof
[(triple1)]
("lion" "is" "young" "-")
triple1
The lion sees the lion.
True
2
proof
[(((triple1) -> rule1))]
("lion" "sees" "lion" "+")
((triple1) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion does not see the lion.
False
2
inv-proof
[(((triple1) -> rule1))]
("lion" "sees" "lion" "-")
((triple1) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion does not chase the tiger.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("lion" "chases" "tiger" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The lion does not chase the tiger.
("lion" "chases" "tiger" "-")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2
The lion chases the tiger.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("lion" "chases" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The lion does not chase the tiger.
("lion" "chases" "tiger" "-")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2
The tiger does not see the lion.
Unknown
inv-rconc
[@1: The tiger sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "sees" "lion" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
The lion is not cold.
Unknown
inv-random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "-")
The lion eats the tiger.
Unknown
random
[@0: The lion eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "tiger" "+")
@0: The lion is young.[(triple1)] The tiger chases the lion.[(triple2)] @1: The lion sees the lion.[(((triple1) -> rule1))] @2: The lion does not chase the tiger.[(((((triple1) -> rule1)) -> rule2))]
The lion is young.
("lion" "is" "young" "+")
triple1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple2
The lion sees the lion.
("lion" "sees" "lion" "+")
((triple1) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion does not chase the tiger.
("lion" "chases" "tiger" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The lion does not chase the tiger.
("lion" "chases" "tiger" "-")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2