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