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