The lion chases the rabbit. The lion does not eat the rabbit. The lion is not big. The lion is nice. The lion is red. The lion is rough. The lion needs the rabbit. The rabbit chases the lion. The rabbit does not eat the lion. The rabbit is big. The rabbit is nice. The rabbit is red. The rabbit is rough. The rabbit is young. The rabbit needs the lion. If someone eats the rabbit then they need the rabbit. If someone eats the rabbit then they need the rabbit. If someone needs the lion then they eat the rabbit. If someone is big then they do not chase the rabbit. If someone eats the lion and they eat the rabbit then they need the lion. If someone needs the rabbit and they do not chase the lion then they need the lion.
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion does not eat the rabbit.
("lion" "eats" "rabbit" "-")
The lion is not big.
("lion" "is" "big" "-")
The lion is nice.
("lion" "is" "nice" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit does not eat the lion.
("rabbit" "eats" "lion" "-")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
If someone eats the rabbit then they need the rabbit.
((("someone" "eats" "rabbit" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone eats the rabbit then they need the rabbit.
((("someone" "eats" "rabbit" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone needs the lion then they eat the rabbit.
((("someone" "needs" "lion" "+")) -> ("someone" "eats" "rabbit" "+"))
If someone is big then they do not chase the rabbit.
((("someone" "is" "big" "+")) -> ("someone" "chases" "rabbit" "-"))
If someone eats the lion and they eat the rabbit then they need the lion.
((("someone" "eats" "lion" "+") ("someone" "eats" "rabbit" "+")) -> ("someone" "needs" "lion" "+"))
If someone needs the rabbit and they do not chase the lion then they need the lion.
((("someone" "needs" "rabbit" "+") ("someone" "chases" "lion" "~")) -> ("someone" "needs" "lion" "+"))
The rabbit needs the lion.
True
1
proof
[(triple15)]
("rabbit" "needs" "lion" "+")
triple15
The lion is not red.
False
1
inv-proof
[(triple5)]
("lion" "is" "red" "-")
triple5
The rabbit eats the rabbit.
True
2
proof
[(((triple15) -> rule3))]
("rabbit" "eats" "rabbit" "+")
((triple15) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit does not eat the rabbit.
False
2
inv-proof
[(((triple15) -> rule3))]
("rabbit" "eats" "rabbit" "-")
((triple15) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the rabbit.
True
3
proof
[(((((triple15) -> rule3)) -> rule1) OR ((((triple15) -> rule3)) -> rule2))]
("rabbit" "needs" "rabbit" "+")
((((triple15) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
((((triple15) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit does not need the rabbit.
False
3
inv-proof
[(((((triple15) -> rule3)) -> rule1) OR ((((triple15) -> rule3)) -> rule2))]
("rabbit" "needs" "rabbit" "-")
((((triple15) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
((((triple15) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The lion does not need the lion.
Unknown
inv-rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "needs" "lion" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The lion is young.
Unknown
random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "+")
@0: The lion chases the rabbit.[(triple1)] The lion does not eat the rabbit.[(triple2)] The lion is nice.[(triple4)] The lion is not big.[(triple3)] The lion is red.[(triple5)] The lion is rough.[(triple6)] The lion needs the rabbit.[(triple7)] The rabbit chases the lion.[(triple8)] The rabbit does not eat the lion.[(triple9)] The rabbit is big.[(triple10)] The rabbit is nice.[(triple11)] The rabbit is red.[(triple12)] The rabbit is rough.[(triple13)] The rabbit is young.[(triple14)] The rabbit needs the lion.[(triple15)] @1: The rabbit does not chase the rabbit.[(((triple10) -> rule4))] The rabbit eats the rabbit.[(((triple15) -> rule3))] @2: The rabbit needs the rabbit.[(((((triple15) -> rule3)) -> rule1) OR ((((triple15) -> rule3)) -> rule2))]
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple1
The lion does not eat the rabbit.
("lion" "eats" "rabbit" "-")
triple2
The lion is nice.
("lion" "is" "nice" "+")
triple4
The lion is not big.
("lion" "is" "big" "-")
triple3
The lion is red.
("lion" "is" "red" "+")
triple5
The lion is rough.
("lion" "is" "rough" "+")
triple6
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple7
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple8
The rabbit does not eat the lion.
("rabbit" "eats" "lion" "-")
triple9
The rabbit is big.
("rabbit" "is" "big" "+")
triple10
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple11
The rabbit is red.
("rabbit" "is" "red" "+")
triple12
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple13
The rabbit is young.
("rabbit" "is" "young" "+")
triple14
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple15
The rabbit does not chase the rabbit.
("rabbit" "chases" "rabbit" "-")
((triple10) -> (rule4 % int1))
The rabbit does not chase the rabbit.
("rabbit" "chases" "rabbit" "-")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((triple15) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((((triple15) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
((((triple15) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2