The lion chases the tiger. The tiger is not big. If something chases the tiger then it sees the lion. If something chases the tiger then it visits the tiger. If something is round and not rough then it does not visit the tiger. If something chases the tiger and it is young then it is big. If something sees the lion and the lion does not see the tiger then the tiger sees the lion. If the lion sees the tiger and the lion is not big then the lion visits the tiger. If something chases the tiger then the tiger chases the lion. If something visits the lion and it visits the tiger then the tiger chases the lion.
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The tiger is not big.
("tiger" "is" "big" "-")
If something chases the tiger then it sees the lion.
((("something" "chases" "tiger" "+")) -> ("something" "sees" "lion" "+"))
If something chases the tiger then it visits the tiger.
((("something" "chases" "tiger" "+")) -> ("something" "visits" "tiger" "+"))
If something is round and not rough then it does not visit the tiger.
((("something" "is" "round" "+") ("something" "is" "rough" "~")) -> ("something" "visits" "tiger" "-"))
If something chases the tiger and it is young then it is big.
((("something" "chases" "tiger" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
If something sees the lion and the lion does not see the tiger then the tiger sees the lion.
((("something" "sees" "lion" "+") ("lion" "sees" "tiger" "~")) -> ("tiger" "sees" "lion" "+"))
If the lion sees the tiger and the lion is not big then the lion visits the tiger.
((("lion" "sees" "tiger" "+") ("lion" "is" "big" "~")) -> ("lion" "visits" "tiger" "+"))
If something chases the tiger then the tiger chases the lion.
((("something" "chases" "tiger" "+")) -> ("tiger" "chases" "lion" "+"))
If something visits the lion and it visits the tiger then the tiger chases the lion.
((("something" "visits" "lion" "+") ("something" "visits" "tiger" "+")) -> ("tiger" "chases" "lion" "+"))
The tiger is not big.
True
1
proof
[(triple2)]
("tiger" "is" "big" "-")
triple2
The lion does not chase the tiger.
False
1
inv-proof
[(triple1)]
("lion" "chases" "tiger" "-")
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 tiger does not chase the lion.
False
2
inv-proof
[(((triple1) -> rule7))]
("tiger" "chases" "lion" "-")
((triple1) -> (rule7 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
The lion is not big.
Unknown
inv-rconc
[@1: The lion is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "big" "-")
The tiger sees the lion.
Unknown
rconc
[@1: The tiger sees the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "sees" "lion" "+")
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
@0: The lion chases the tiger.[(triple1)] The tiger is not big.[(triple2)] @1: The lion sees the lion.[(((triple1) -> rule1))] The lion visits the tiger.[(((triple1) -> rule2))] The tiger chases the lion.[(((triple1) -> rule7))]
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple1
The tiger is not big.
("tiger" "is" "big" "-")
triple2
The lion sees the lion.
("lion" "sees" "lion" "+")
((triple1) -> (rule1 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion visits the tiger.
("lion" "visits" "tiger" "+")
((triple1) -> (rule2 % int1))
The lion visits the tiger.
("lion" "visits" "tiger" "+")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
((triple1) -> (rule7 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1