The lion chases the tiger. The rabbit visits the lion. The tiger is blue. If someone chases the tiger then the tiger visits the rabbit. If the tiger visits the rabbit then the tiger eats the lion. If someone eats the tiger then the tiger eats the lion. If the tiger eats the lion then the lion eats the rabbit. If someone eats the lion then the lion eats the rabbit. If someone chases the rabbit and they eat the tiger then the rabbit visits the tiger. If the lion eats the tiger and the lion is kind then the lion is not big. If the tiger is not rough then the tiger visits the lion.
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
If someone chases the tiger then the tiger visits the rabbit.
((("someone" "chases" "tiger" "+")) -> ("tiger" "visits" "rabbit" "+"))
If the tiger visits the rabbit then the tiger eats the lion.
((("tiger" "visits" "rabbit" "+")) -> ("tiger" "eats" "lion" "+"))
If someone eats the tiger then the tiger eats the lion.
((("someone" "eats" "tiger" "+")) -> ("tiger" "eats" "lion" "+"))
If the tiger eats the lion then the lion eats the rabbit.
((("tiger" "eats" "lion" "+")) -> ("lion" "eats" "rabbit" "+"))
If someone eats the lion then the lion eats the rabbit.
((("someone" "eats" "lion" "+")) -> ("lion" "eats" "rabbit" "+"))
If someone chases the rabbit and they eat the tiger then the rabbit visits the tiger.
((("someone" "chases" "rabbit" "+") ("someone" "eats" "tiger" "+")) -> ("rabbit" "visits" "tiger" "+"))
If the lion eats the tiger and the lion is kind then the lion is not big.
((("lion" "eats" "tiger" "+") ("lion" "is" "kind" "+")) -> ("lion" "is" "big" "-"))
If the tiger is not rough then the tiger visits the lion.
((("tiger" "is" "rough" "~")) -> ("tiger" "visits" "lion" "+"))
The lion chases the tiger.
True
1
proof
[(triple1)]
("lion" "chases" "tiger" "+")
triple1
The tiger is not blue.
False
1
inv-proof
[(triple3)]
("tiger" "is" "blue" "-")
triple3
The tiger visits the rabbit.
True
2
proof
[(((triple1) -> rule1))]
("tiger" "visits" "rabbit" "+")
((triple1) -> (rule1 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The tiger does not visit the rabbit.
False
2
inv-proof
[(((triple1) -> rule1))]
("tiger" "visits" "rabbit" "-")
((triple1) -> (rule1 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The tiger eats the lion.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("tiger" "eats" "lion" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2
The tiger does not eat the lion.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("tiger" "eats" "lion" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2
The lion eats the rabbit.
True
4
proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule4) OR ((((((triple1) -> rule1)) -> rule2)) -> rule5))]
("lion" "eats" "rabbit" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int3
The lion does not eat the rabbit.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule2)) -> rule4) OR ((((((triple1) -> rule1)) -> rule2)) -> rule5))]
("lion" "eats" "rabbit" "-")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int3
The rabbit does not visit the tiger.
Unknown
inv-rconc
[@1: The rabbit visits the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "visits" "tiger" "-")
The tiger visits the lion.
Unknown
rconc
[@1: The tiger visits the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "visits" "lion" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The tiger is nice.
Unknown
random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "+")
The rabbit does not eat the lion.
Unknown
inv-random
[@0: The rabbit eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "lion" "-")
The lion chases the rabbit.
Unknown
random
[@0: The lion chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "rabbit" "+")
The tiger is not rough.
Unknown
inv-random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
@0: The lion chases the tiger.[(triple1)] The rabbit visits the lion.[(triple2)] The tiger is blue.[(triple3)] @1: The tiger visits the rabbit.[(((triple1) -> rule1))] @2: The tiger eats the lion.[(((((triple1) -> rule1)) -> rule2))] @3: The lion eats the rabbit.[(((((((triple1) -> rule1)) -> rule2)) -> rule4) OR ((((((triple1) -> rule1)) -> rule2)) -> rule5))]
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple1
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple2
The tiger is blue.
("tiger" "is" "blue" "+")
triple3
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
((triple1) -> (rule1 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int2
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
int1
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int2
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int3