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