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