The lion is round. The tiger is blue. If the tiger is red then the tiger eats the lion. If something eats the tiger then the tiger is blue. If something chases the lion then the lion is not red. If something is blue then it visits the tiger. If something visits the tiger then the tiger chases the lion. If the lion is blue and the lion visits the tiger then the tiger visits the lion. If something is cold and not blue then it chases the tiger. If something chases the tiger and it is not cold then it does not eat the lion.
The lion is round.
("lion" "is" "round" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
If the tiger is red then the tiger eats the lion.
((("tiger" "is" "red" "+")) -> ("tiger" "eats" "lion" "+"))
If something eats the tiger then the tiger is blue.
((("something" "eats" "tiger" "+")) -> ("tiger" "is" "blue" "+"))
If something chases the lion then the lion is not red.
((("something" "chases" "lion" "+")) -> ("lion" "is" "red" "-"))
If something is blue then it visits the tiger.
((("something" "is" "blue" "+")) -> ("something" "visits" "tiger" "+"))
If something visits the tiger then the tiger chases the lion.
((("something" "visits" "tiger" "+")) -> ("tiger" "chases" "lion" "+"))
If the lion is blue and the lion visits the tiger then the tiger visits the lion.
((("lion" "is" "blue" "+") ("lion" "visits" "tiger" "+")) -> ("tiger" "visits" "lion" "+"))
If something is cold and not blue then it chases the tiger.
((("something" "is" "cold" "+") ("something" "is" "blue" "~")) -> ("something" "chases" "tiger" "+"))
If something chases the tiger and it is not cold then it does not eat the lion.
((("something" "chases" "tiger" "+") ("something" "is" "cold" "~")) -> ("something" "eats" "lion" "-"))
The lion is round.
True
1
proof
[(triple1)]
("lion" "is" "round" "+")
triple1
The tiger is not blue.
False
1
inv-proof
[(triple2)]
("tiger" "is" "blue" "-")
triple2
The tiger visits the tiger.
True
2
proof
[(((triple2) -> rule4))]
("tiger" "visits" "tiger" "+")
((triple2) -> (rule4 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger does not visit the tiger.
False
2
inv-proof
[(((triple2) -> rule4))]
("tiger" "visits" "tiger" "-")
((triple2) -> (rule4 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger chases the lion.
True
3
proof
[(((((triple2) -> rule4)) -> rule5))]
("tiger" "chases" "lion" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The tiger does not chase the lion.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule5))]
("tiger" "chases" "lion" "-")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The lion is not red.
True
4
proof
[(((((((triple2) -> rule4)) -> rule5)) -> rule3))]
("lion" "is" "red" "-")
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The lion is not red.
("lion" "is" "red" "-")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int2
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int3
The lion is red.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule5)) -> rule3))]
("lion" "is" "red" "+")
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The lion is not red.
("lion" "is" "red" "-")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int2
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int3
The lion does not visit the tiger.
Unknown
inv-rconc
[@1: The lion visits the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "visits" "tiger" "-")
The tiger visits the lion.
Unknown
rconc
[@1: The tiger visits the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "visits" "lion" "+")
The lion does not chase the tiger.
Unknown
inv-rconc
[@1: The lion chases the tiger.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "chases" "tiger" "-")
The tiger chases the tiger.
Unknown
rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("tiger" "chases" "tiger" "+")
The lion does not eat the tiger.
Unknown
inv-random
[@0: The lion eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "tiger" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
The lion is kind.
Unknown
random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "+")
@0: The lion is round.[(triple1)] The tiger is blue.[(triple2)] @1: The tiger visits the tiger.[(((triple2) -> rule4))] @2: The tiger chases the lion.[(((((triple2) -> rule4)) -> rule5))] @3: The lion is not red.[(((((((triple2) -> rule4)) -> rule5)) -> rule3))]
The lion is round.
("lion" "is" "round" "+")
triple1
The tiger is blue.
("tiger" "is" "blue" "+")
triple2
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((triple2) -> (rule4 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int2
The lion is not red.
("lion" "is" "red" "-")
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The lion is not red.
("lion" "is" "red" "-")
int1
The tiger chases the lion.
("tiger" "chases" "lion" "+")
int2
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int3