The cat likes the lion. The cat likes the tiger. The cat needs the tiger. The cow likes the tiger. The cow needs the cat. The lion chases the cat. The lion chases the tiger. The lion is kind. The lion does not need the cow. The tiger does not chase the cow. If someone needs the cat then the cat needs the tiger. If someone needs the tiger and they are not kind then they need the cow. If someone needs the tiger then the tiger is not red. If someone needs the cow then they need the lion. If someone is big then they do not chase the lion. If someone chases the tiger and the tiger is not red then the tiger is big.
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion does not need the cow.
("lion" "needs" "cow" "-")
The tiger does not chase the cow.
("tiger" "chases" "cow" "-")
If someone needs the cat then the cat needs the tiger.
((("someone" "needs" "cat" "+")) -> ("cat" "needs" "tiger" "+"))
If someone needs the tiger and they are not kind then they need the cow.
((("someone" "needs" "tiger" "+") ("someone" "is" "kind" "~")) -> ("someone" "needs" "cow" "+"))
If someone needs the tiger then the tiger is not red.
((("someone" "needs" "tiger" "+")) -> ("tiger" "is" "red" "-"))
If someone needs the cow then they need the lion.
((("someone" "needs" "cow" "+")) -> ("someone" "needs" "lion" "+"))
If someone is big then they do not chase the lion.
((("someone" "is" "big" "+")) -> ("someone" "chases" "lion" "-"))
If someone chases the tiger and the tiger is not red then the tiger is big.
((("someone" "chases" "tiger" "+") ("tiger" "is" "red" "~")) -> ("tiger" "is" "big" "+"))
The lion chases the cat.
True
1
proof
[(triple6)]
("lion" "chases" "cat" "+")
triple6
The cat does not like the lion.
False
1
inv-proof
[(triple1)]
("cat" "likes" "lion" "-")
triple1
The tiger is not red.
True
2
proof
[(((triple3) -> rule3) OR ((((triple5) -> rule1)) -> rule3))]
("tiger" "is" "red" "-")
((triple3) -> (rule3 % int1))
The tiger is not red.
("tiger" "is" "red" "-")
int1
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
The tiger is not red.
("tiger" "is" "red" "-")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
The tiger is red.
False
2
inv-proof
[(((triple3) -> rule3) OR ((((triple5) -> rule1)) -> rule3))]
("tiger" "is" "red" "+")
((triple3) -> (rule3 % int1))
The tiger is not red.
("tiger" "is" "red" "-")
int1
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
The tiger is not red.
("tiger" "is" "red" "-")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
The tiger is big.
True
4
proof
[(((triple7 ((triple3) -> rule3)) -> rule6) OR ((triple7 ((((triple5) -> rule1)) -> rule3)) -> rule6))]
("tiger" "is" "big" "+")
((triple7 ((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is not red.
("tiger" "is" "red" "-")
int2
((triple7 ((((triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is not red.
("tiger" "is" "red" "-")
int2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int3
The tiger is not big.
False
4
inv-proof
[(((triple7 ((triple3) -> rule3)) -> rule6) OR ((triple7 ((((triple5) -> rule1)) -> rule3)) -> rule6))]
("tiger" "is" "big" "-")
((triple7 ((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is not red.
("tiger" "is" "red" "-")
int2
((triple7 ((((triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is not red.
("tiger" "is" "red" "-")
int2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int3
The tiger does not chase the lion.
True
5
proof
[(((((triple7 ((triple3) -> rule3)) -> rule6)) -> rule5) OR ((((triple7 ((((triple5) -> rule1)) -> rule3)) -> rule6)) -> rule5))]
("tiger" "chases" "lion" "-")
((((triple7 ((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The tiger does not chase the lion.
("tiger" "chases" "lion" "-")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is not red.
("tiger" "is" "red" "-")
int3
((((triple7 ((((triple5) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The tiger does not chase the lion.
("tiger" "chases" "lion" "-")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is not red.
("tiger" "is" "red" "-")
int3
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int4
The tiger chases the lion.
False
5
inv-proof
[(((((triple7 ((triple3) -> rule3)) -> rule6)) -> rule5) OR ((((triple7 ((((triple5) -> rule1)) -> rule3)) -> rule6)) -> rule5))]
("tiger" "chases" "lion" "+")
((((triple7 ((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The tiger does not chase the lion.
("tiger" "chases" "lion" "-")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is not red.
("tiger" "is" "red" "-")
int3
((((triple7 ((((triple5) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The tiger does not chase the lion.
("tiger" "chases" "lion" "-")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is not red.
("tiger" "is" "red" "-")
int3
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int4
The cat does not need the cow.
Unknown
inv-rconc
[@1: The cat needs the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "needs" "cow" "-")
The lion needs the lion.
Unknown
rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "needs" "lion" "+")
The tiger does not need the lion.
Unknown
inv-rconc
[@2: The tiger needs the lion.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("tiger" "needs" "lion" "-")
The tiger needs the cow.
Unknown
rconc
[@1: The tiger needs the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "needs" "cow" "+")
The tiger does not chase the cat.
Unknown
inv-random
[@0: The tiger chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "cat" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The cat is big.
Unknown
random
[@0: The cat is big.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "big" "+")
@0: The cat likes the lion.[(triple1)] The cat likes the tiger.[(triple2)] The cat needs the tiger.[(triple3 OR ((triple5) -> rule1))] The cow likes the tiger.[(triple4)] The cow needs the cat.[(triple5)] The lion chases the cat.[(triple6)] The lion chases the tiger.[(triple7)] The lion does not need the cow.[(triple9)] The lion is kind.[(triple8)] The tiger does not chase the cow.[(triple10)] @1: The tiger is not red.[(((triple3) -> rule3) OR ((((triple5) -> rule1)) -> rule3))] @2: The tiger is big.[(((triple7 ((triple3) -> rule3)) -> rule6) OR ((triple7 ((((triple5) -> rule1)) -> rule3)) -> rule6))] @3: The tiger does not chase the lion.[(((((triple7 ((triple3) -> rule3)) -> rule6)) -> rule5) OR ((((triple7 ((((triple5) -> rule1)) -> rule3)) -> rule6)) -> rule5))]
The cat likes the lion.
("cat" "likes" "lion" "+")
triple1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple3
((triple5) -> (rule1 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple4
The cow needs the cat.
("cow" "needs" "cat" "+")
triple5
The lion chases the cat.
("lion" "chases" "cat" "+")
triple6
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple7
The lion does not need the cow.
("lion" "needs" "cow" "-")
triple9
The lion is kind.
("lion" "is" "kind" "+")
triple8
The tiger does not chase the cow.
("tiger" "chases" "cow" "-")
triple10
The tiger is not red.
("tiger" "is" "red" "-")
((triple3) -> (rule3 % int1))
The tiger is not red.
("tiger" "is" "red" "-")
int1
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
The tiger is not red.
("tiger" "is" "red" "-")
int1
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
((triple7 ((triple3) -> (rule3 % int2))) -> (rule6 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is not red.
("tiger" "is" "red" "-")
int2
((triple7 ((((triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is not red.
("tiger" "is" "red" "-")
int2
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int3
The tiger does not chase the lion.
("tiger" "chases" "lion" "-")
((((triple7 ((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The tiger does not chase the lion.
("tiger" "chases" "lion" "-")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is not red.
("tiger" "is" "red" "-")
int3
((((triple7 ((((triple5) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The tiger does not chase the lion.
("tiger" "chases" "lion" "-")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is not red.
("tiger" "is" "red" "-")
int3
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int4