The lion is rough. The tiger is rough. If the tiger visits the lion then the tiger is blue. If the tiger sees the lion then the lion visits the tiger. If the tiger is rough then the tiger eats the lion. If something is rough and it does not see the lion then the lion is rough. If something sees the tiger then the tiger does not visit the lion. If the lion visits the tiger and the lion does not eat the tiger then the lion is nice. If something eats the lion then the lion is kind. If something is nice then it does not visit the lion.
The lion is rough.
("lion" "is" "rough" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
If the tiger visits the lion then the tiger is blue.
((("tiger" "visits" "lion" "+")) -> ("tiger" "is" "blue" "+"))
If the tiger sees the lion then the lion visits the tiger.
((("tiger" "sees" "lion" "+")) -> ("lion" "visits" "tiger" "+"))
If the tiger is rough then the tiger eats the lion.
((("tiger" "is" "rough" "+")) -> ("tiger" "eats" "lion" "+"))
If something is rough and it does not see the lion then the lion is rough.
((("something" "is" "rough" "+") ("something" "sees" "lion" "~")) -> ("lion" "is" "rough" "+"))
If something sees the tiger then the tiger does not visit the lion.
((("something" "sees" "tiger" "+")) -> ("tiger" "visits" "lion" "-"))
If the lion visits the tiger and the lion does not eat the tiger then the lion is nice.
((("lion" "visits" "tiger" "+") ("lion" "eats" "tiger" "~")) -> ("lion" "is" "nice" "+"))
If something eats the lion then the lion is kind.
((("something" "eats" "lion" "+")) -> ("lion" "is" "kind" "+"))
If something is nice then it does not visit the lion.
((("something" "is" "nice" "+")) -> ("something" "visits" "lion" "-"))
The tiger is rough.
True
1
proof
[(triple2)]
("tiger" "is" "rough" "+")
triple2
The lion is not rough.
False
1
inv-proof
[(triple1)]
("lion" "is" "rough" "-")
triple1
The tiger eats the lion.
True
2
proof
[(((triple2) -> rule3))]
("tiger" "eats" "lion" "+")
((triple2) -> (rule3 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1
The tiger does not eat the lion.
False
2
inv-proof
[(((triple2) -> rule3))]
("tiger" "eats" "lion" "-")
((triple2) -> (rule3 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1
The lion is kind.
True
3
proof
[(((((triple2) -> rule3)) -> rule7))]
("lion" "is" "kind" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The lion is not kind.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule7))]
("lion" "is" "kind" "-")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The tiger is not blue.
Unknown
inv-rconc
[@1: The tiger is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "blue" "-")
The lion visits the tiger.
Unknown
rconc
[@1: The lion visits the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "visits" "tiger" "+")
The lion is not nice.
Unknown
inv-rconc
[@1: The lion is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "is" "nice" "-")
The tiger is nice.
Unknown
random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The lion sees the tiger.
Unknown
random
[@0: The lion sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "tiger" "+")
@0: The lion is rough.[(triple1)] The tiger is rough.[(triple2)] @1: The tiger eats the lion.[(((triple2) -> rule3))] @2: The lion is kind.[(((((triple2) -> rule3)) -> rule7))]
The lion is rough.
("lion" "is" "rough" "+")
triple1
The tiger is rough.
("tiger" "is" "rough" "+")
triple2
The tiger eats the lion.
("tiger" "eats" "lion" "+")
((triple2) -> (rule3 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2