The lion is big. The tiger chases the lion. The tiger visits the lion. If something is nice then it chases the tiger. If something visits the lion then it is nice. If the lion visits the tiger and the tiger needs the lion then the lion is nice.
The lion is big.
("lion" "is" "big" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If something is nice then it chases the tiger.
((("something" "is" "nice" "+")) -> ("something" "chases" "tiger" "+"))
If something visits the lion then it is nice.
((("something" "visits" "lion" "+")) -> ("something" "is" "nice" "+"))
If the lion visits the tiger and the tiger needs the lion then the lion is nice.
((("lion" "visits" "tiger" "+") ("tiger" "needs" "lion" "+")) -> ("lion" "is" "nice" "+"))
The tiger chases the lion.
True
1
proof
[(triple2)]
("tiger" "chases" "lion" "+")
triple2
The tiger does not chase the lion.
False
1
inv-proof
[(triple2)]
("tiger" "chases" "lion" "-")
triple2
The tiger is nice.
True
2
proof
[(((triple3) -> rule2))]
("tiger" "is" "nice" "+")
((triple3) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is not nice.
False
2
inv-proof
[(((triple3) -> rule2))]
("tiger" "is" "nice" "-")
((triple3) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger chases the tiger.
True
3
proof
[(((((triple3) -> rule2)) -> rule1))]
("tiger" "chases" "tiger" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger does not chase the tiger.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule1))]
("tiger" "chases" "tiger" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The lion is not nice.
Unknown
inv-rconc
[@1: The lion is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "nice" "-")
The lion chases the tiger.
Unknown
rconc
[@2: The lion chases the tiger.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("lion" "chases" "tiger" "+")
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The lion does not need the tiger.
Unknown
inv-random
[@0: The lion needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "tiger" "-")
The lion is blue.
Unknown
random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "+")
@0: The lion is big.[(triple1)] The tiger chases the lion.[(triple2)] The tiger visits the lion.[(triple3)] @1: The tiger is nice.[(((triple3) -> rule2))] @2: The tiger chases the tiger.[(((((triple3) -> rule2)) -> rule1))]
The lion is big.
("lion" "is" "big" "+")
triple1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple2
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple3
The tiger is nice.
("tiger" "is" "nice" "+")
((triple3) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2