The lion chases the tiger. The tiger eats the lion. If the lion chases the tiger then the lion visits the tiger. If something eats the tiger then the tiger is cold.
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
If the lion chases the tiger then the lion visits the tiger.
((("lion" "chases" "tiger" "+")) -> ("lion" "visits" "tiger" "+"))
If something eats the tiger then the tiger is cold.
((("something" "eats" "tiger" "+")) -> ("tiger" "is" "cold" "+"))
The lion chases the tiger.
True
1
proof
[(triple1)]
("lion" "chases" "tiger" "+")
triple1
The tiger does not eat the lion.
False
1
inv-proof
[(triple2)]
("tiger" "eats" "lion" "-")
triple2
The lion visits the tiger.
True
2
proof
[(((triple1) -> rule1))]
("lion" "visits" "tiger" "+")
((triple1) -> (rule1 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The lion does not visit the tiger.
False
2
inv-proof
[(((triple1) -> rule1))]
("lion" "visits" "tiger" "-")
((triple1) -> (rule1 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The tiger is not cold.
Unknown
inv-rconc
[@1: The tiger is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "cold" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
The tiger does not visit the lion.
Unknown
inv-random
[@0: The tiger visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "lion" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
@0: The lion chases the tiger.[(triple1)] The tiger eats the lion.[(triple2)] @1: The lion visits the tiger.[(((triple1) -> rule1))]
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple2
The lion visits the tiger.
("lion" "visits" "tiger" "+")
((triple1) -> (rule1 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1