The lion chases the rabbit. The lion is not green. The lion is round. The rabbit does not chase the lion. The rabbit chases the tiger. The rabbit eats the lion. The rabbit eats the tiger. The rabbit is kind. The rabbit is nice. The rabbit is rough. The rabbit visits the lion. The tiger eats the rabbit. The tiger is green. The tiger is round. The tiger visits the rabbit. If someone is green and not rough then they eat the rabbit. If someone eats the lion then the lion chases the tiger. If someone is round and they do not eat the lion then the lion visits the tiger. If the rabbit is not rough then the rabbit does not chase the tiger. If someone visits the rabbit then they visit the lion. If someone chases the lion then the lion visits the rabbit. If someone chases the tiger then they visit the rabbit. If the rabbit is round and the rabbit is nice then the rabbit does not eat the tiger.
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion is not green.
("lion" "is" "green" "-")
The lion is round.
("lion" "is" "round" "+")
The rabbit does not chase the lion.
("rabbit" "chases" "lion" "-")
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If someone is green and not rough then they eat the rabbit.
((("someone" "is" "green" "+") ("someone" "is" "rough" "~")) -> ("someone" "eats" "rabbit" "+"))
If someone eats the lion then the lion chases the tiger.
((("someone" "eats" "lion" "+")) -> ("lion" "chases" "tiger" "+"))
If someone is round and they do not eat the lion then the lion visits the tiger.
((("someone" "is" "round" "+") ("someone" "eats" "lion" "~")) -> ("lion" "visits" "tiger" "+"))
If the rabbit is not rough then the rabbit does not chase the tiger.
((("rabbit" "is" "rough" "~")) -> ("rabbit" "chases" "tiger" "-"))
If someone visits the rabbit then they visit the lion.
((("someone" "visits" "rabbit" "+")) -> ("someone" "visits" "lion" "+"))
If someone chases the lion then the lion visits the rabbit.
((("someone" "chases" "lion" "+")) -> ("lion" "visits" "rabbit" "+"))
If someone chases the tiger then they visit the rabbit.
((("someone" "chases" "tiger" "+")) -> ("someone" "visits" "rabbit" "+"))
If the rabbit is round and the rabbit is nice then the rabbit does not eat the tiger.
((("rabbit" "is" "round" "+") ("rabbit" "is" "nice" "+")) -> ("rabbit" "eats" "tiger" "-"))
The rabbit is nice.
True
1
proof
[(triple9)]
("rabbit" "is" "nice" "+")
triple9
The lion is not round.
False
1
inv-proof
[(triple3)]
("lion" "is" "round" "-")
triple3
The lion chases the tiger.
True
2
proof
[(((triple6) -> rule2))]
("lion" "chases" "tiger" "+")
((triple6) -> (rule2 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The tiger does not visit the lion.
False
2
inv-proof
[(((triple15) -> rule5))]
("tiger" "visits" "lion" "-")
((triple15) -> (rule5 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
The lion visits the rabbit.
True
3
proof
[(((((triple6) -> rule2)) -> rule7))]
("lion" "visits" "rabbit" "+")
((((triple6) -> (rule2 % int2))) -> (rule7 % int1))
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int1
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int2
The lion does not visit the rabbit.
False
3
inv-proof
[(((((triple6) -> rule2)) -> rule7))]
("lion" "visits" "rabbit" "-")
((((triple6) -> (rule2 % int2))) -> (rule7 % int1))
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int1
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int2
The lion visits the lion.
True
4
proof
[(((((((triple6) -> rule2)) -> rule7)) -> rule5))]
("lion" "visits" "lion" "+")
((((((triple6) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int2
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int3
The lion does not visit the lion.
False
4
inv-proof
[(((((((triple6) -> rule2)) -> rule7)) -> rule5))]
("lion" "visits" "lion" "-")
((((((triple6) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int2
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int3
The lion does not eat the rabbit.
Unknown
inv-rconc
[@1: The lion eats the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "eats" "rabbit" "-")
The lion visits the tiger.
Unknown
rconc
[@1: The lion visits the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "visits" "tiger" "+")
The rabbit does not eat the rabbit.
Unknown
inv-rconc
[@1: The rabbit eats the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "eats" "rabbit" "-")
The tiger is nice.
Unknown
random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "+")
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 is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
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 is nice.
Unknown
random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "+")
@0: The lion chases the rabbit.[(triple1)] The lion is not green.[(triple2)] The lion is round.[(triple3)] The rabbit chases the tiger.[(triple5)] The rabbit does not chase the lion.[(triple4)] The rabbit eats the lion.[(triple6)] The rabbit eats the tiger.[(triple7)] The rabbit is kind.[(triple8)] The rabbit is nice.[(triple9)] The rabbit is rough.[(triple10)] The rabbit visits the lion.[(triple11 OR ((((triple5) -> rule7)) -> rule5))] The tiger eats the rabbit.[(triple12)] The tiger is green.[(triple13)] The tiger is round.[(triple14)] The tiger visits the rabbit.[(triple15)] @1: The lion chases the tiger.[(((triple6) -> rule2))] The rabbit visits the rabbit.[(((triple5) -> rule7))] The tiger visits the lion.[(((triple15) -> rule5))] @2: The lion visits the rabbit.[(((((triple6) -> rule2)) -> rule7))] @3: The lion visits the lion.[(((((((triple6) -> rule2)) -> rule7)) -> rule5))]
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple1
The lion is not green.
("lion" "is" "green" "-")
triple2
The lion is round.
("lion" "is" "round" "+")
triple3
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple5
The rabbit does not chase the lion.
("rabbit" "chases" "lion" "-")
triple4
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple6
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple7
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple8
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple9
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple10
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple11
((((triple5) -> (rule7 % int2))) -> (rule5 % int1))
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int2
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple12
The tiger is green.
("tiger" "is" "green" "+")
triple13
The tiger is round.
("tiger" "is" "round" "+")
triple14
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple15
The lion chases the tiger.
("lion" "chases" "tiger" "+")
((triple6) -> (rule2 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple5) -> (rule7 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The tiger visits the lion.
("tiger" "visits" "lion" "+")
((triple15) -> (rule5 % int1))
The tiger visits the lion.
("tiger" "visits" "lion" "+")
int1
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
((((triple6) -> (rule2 % int2))) -> (rule7 % int1))
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int1
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int2
The lion visits the lion.
("lion" "visits" "lion" "+")
((((((triple6) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
int2
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int3