The lion chases the rabbit. The lion is big. The lion is kind. The lion is nice. The lion is round. The lion is young. The lion needs the rabbit. The lion does not see the rabbit. The rabbit chases the lion. The rabbit is big. The rabbit is not kind. The rabbit is nice. The rabbit is round. The rabbit is not young. The rabbit needs the lion. The rabbit sees the lion. If the lion chases the rabbit then the lion needs the rabbit. If something chases the lion then it sees the lion. If something needs the rabbit and it chases the lion then the lion is big. If something is round then it chases the lion. If the rabbit needs the lion then the rabbit sees the lion. If something sees the lion and it needs the rabbit then it is kind.
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is round.
("lion" "is" "round" "+")
The lion is young.
("lion" "is" "young" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The lion does not see the rabbit.
("lion" "sees" "rabbit" "-")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is not kind.
("rabbit" "is" "kind" "-")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit is not young.
("rabbit" "is" "young" "-")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If the lion chases the rabbit then the lion needs the rabbit.
((("lion" "chases" "rabbit" "+")) -> ("lion" "needs" "rabbit" "+"))
If something chases the lion then it sees the lion.
((("something" "chases" "lion" "+")) -> ("something" "sees" "lion" "+"))
If something needs the rabbit and it chases the lion then the lion is big.
((("something" "needs" "rabbit" "+") ("something" "chases" "lion" "+")) -> ("lion" "is" "big" "+"))
If something is round then it chases the lion.
((("something" "is" "round" "+")) -> ("something" "chases" "lion" "+"))
If the rabbit needs the lion then the rabbit sees the lion.
((("rabbit" "needs" "lion" "+")) -> ("rabbit" "sees" "lion" "+"))
If something sees the lion and it needs the rabbit then it is kind.
((("something" "sees" "lion" "+") ("something" "needs" "rabbit" "+")) -> ("something" "is" "kind" "+"))
The lion does not see the rabbit.
True
1
proof
[(triple8)]
("lion" "sees" "rabbit" "-")
triple8
The lion does not need the rabbit.
False
1
inv-proof
[(triple7 OR ((triple1) -> rule1))]
("lion" "needs" "rabbit" "-")
triple7
((triple1) -> (rule1 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The lion chases the lion.
True
2
proof
[(((triple5) -> rule4))]
("lion" "chases" "lion" "+")
((triple5) -> (rule4 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion does not chase the lion.
False
2
inv-proof
[(((triple5) -> rule4))]
("lion" "chases" "lion" "-")
((triple5) -> (rule4 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion sees the lion.
True
3
proof
[(((((triple5) -> rule4)) -> rule2))]
("lion" "sees" "lion" "+")
((((triple5) -> (rule4 % int2))) -> (rule2 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion does not see the lion.
False
3
inv-proof
[(((((triple5) -> rule4)) -> rule2))]
("lion" "sees" "lion" "-")
((((triple5) -> (rule4 % int2))) -> (rule2 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
The rabbit does not chase the rabbit.
Unknown
inv-random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
@0: The lion chases the rabbit.[(triple1)] The lion does not see the rabbit.[(triple8)] The lion is big.[(triple2 OR ((triple7 ((triple5) -> rule4)) -> rule3) OR ((((triple1) -> rule1) ((triple5) -> rule4)) -> rule3))] The lion is kind.[(triple3 OR ((((((triple5) -> rule4)) -> rule2) triple7) -> rule6) OR ((((((triple5) -> rule4)) -> rule2) ((triple1) -> rule1)) -> rule6))] The lion is nice.[(triple4)] The lion is round.[(triple5)] The lion is young.[(triple6)] The lion needs the rabbit.[(triple7 OR ((triple1) -> rule1))] The rabbit chases the lion.[(triple9 OR ((triple13) -> rule4))] The rabbit is big.[(triple10)] The rabbit is nice.[(triple12)] The rabbit is not kind.[(triple11)] The rabbit is not young.[(triple14)] The rabbit is round.[(triple13)] The rabbit needs the lion.[(triple15)] The rabbit sees the lion.[(triple16 OR ((triple15) -> rule5) OR ((triple9) -> rule2) OR ((((triple13) -> rule4)) -> rule2))] @1: The lion chases the lion.[(((triple5) -> rule4))] @2: The lion sees the lion.[(((((triple5) -> rule4)) -> rule2))]
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple1
The lion does not see the rabbit.
("lion" "sees" "rabbit" "-")
triple8
The lion is big.
("lion" "is" "big" "+")
triple2
((triple7 ((triple5) -> (rule4 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
((((triple1) -> (rule1 % int3)) ((triple5) -> (rule4 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int3
The lion is kind.
("lion" "is" "kind" "+")
triple3
((((((triple5) -> (rule4 % int3))) -> (rule2 % int2)) triple7) -> (rule6 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
int2
The lion chases the lion.
("lion" "chases" "lion" "+")
int3
((((((triple5) -> (rule4 % int4))) -> (rule2 % int3)) ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int2
The lion sees the lion.
("lion" "sees" "lion" "+")
int3
The lion chases the lion.
("lion" "chases" "lion" "+")
int4
The lion is nice.
("lion" "is" "nice" "+")
triple4
The lion is round.
("lion" "is" "round" "+")
triple5
The lion is young.
("lion" "is" "young" "+")
triple6
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple7
((triple1) -> (rule1 % int1))
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
int1
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple9
((triple13) -> (rule4 % int1))
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
triple10
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple12
The rabbit is not kind.
("rabbit" "is" "kind" "-")
triple11
The rabbit is not young.
("rabbit" "is" "young" "-")
triple14
The rabbit is round.
("rabbit" "is" "round" "+")
triple13
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple15
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple16
((triple15) -> (rule5 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
((triple9) -> (rule2 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
((((triple13) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
int1
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
int2
The lion chases the lion.
("lion" "chases" "lion" "+")
((triple5) -> (rule4 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion sees the lion.
("lion" "sees" "lion" "+")
((((triple5) -> (rule4 % int2))) -> (rule2 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
int2