The bald eagle is kind. The bald eagle likes the rabbit. The bald eagle needs the rabbit. The cat is rough. The cat likes the rabbit. The rabbit likes the tiger. The rabbit needs the bald eagle. The rabbit needs the tiger. The rabbit sees the bald eagle. The rabbit sees the tiger. The tiger is nice. The tiger is rough. The tiger needs the cat. The tiger sees the rabbit. If the cat sees the tiger then the cat is nice. If something is rough and it likes the rabbit then it needs the tiger. If something is nice then it needs the cat. If the rabbit needs the cat then the cat sees the tiger. If something sees the tiger then it is nice. If the cat is kind then the cat is red. If something is rough and it sees the cat then the cat is red.
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
The bald eagle likes the rabbit.
("bald eagle" "likes" "rabbit" "+")
The bald eagle needs the rabbit.
("bald eagle" "needs" "rabbit" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The rabbit needs the bald eagle.
("rabbit" "needs" "bald eagle" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If the cat sees the tiger then the cat is nice.
((("cat" "sees" "tiger" "+")) -> ("cat" "is" "nice" "+"))
If something is rough and it likes the rabbit then it needs the tiger.
((("something" "is" "rough" "+") ("something" "likes" "rabbit" "+")) -> ("something" "needs" "tiger" "+"))
If something is nice then it needs the cat.
((("something" "is" "nice" "+")) -> ("something" "needs" "cat" "+"))
If the rabbit needs the cat then the cat sees the tiger.
((("rabbit" "needs" "cat" "+")) -> ("cat" "sees" "tiger" "+"))
If something sees the tiger then it is nice.
((("something" "sees" "tiger" "+")) -> ("something" "is" "nice" "+"))
If the cat is kind then the cat is red.
((("cat" "is" "kind" "+")) -> ("cat" "is" "red" "+"))
If something is rough and it sees the cat then the cat is red.
((("something" "is" "rough" "+") ("something" "sees" "cat" "+")) -> ("cat" "is" "red" "+"))
The rabbit sees the bald eagle.
True
1
proof
[(triple9)]
("rabbit" "sees" "bald eagle" "+")
triple9
The cat is not rough.
False
1
inv-proof
[(triple4)]
("cat" "is" "rough" "-")
triple4
The cat needs the tiger.
True
3
proof
[(((triple4 triple5) -> rule2))]
("cat" "needs" "tiger" "+")
((triple4 triple5) -> (rule2 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The cat does not need the tiger.
False
3
inv-proof
[(((triple4 triple5) -> rule2))]
("cat" "needs" "tiger" "-")
((triple4 triple5) -> (rule2 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The rabbit needs the cat.
True
3
proof
[(((((triple10) -> rule5)) -> rule3))]
("rabbit" "needs" "cat" "+")
((((triple10) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit does not need the cat.
False
3
inv-proof
[(((((triple10) -> rule5)) -> rule3))]
("rabbit" "needs" "cat" "-")
((((triple10) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The cat sees the tiger.
True
4
proof
[(((((((triple10) -> rule5)) -> rule3)) -> rule4))]
("cat" "sees" "tiger" "+")
((((((triple10) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int2
The rabbit is nice.
("rabbit" "is" "nice" "+")
int3
The cat does not see the tiger.
False
4
inv-proof
[(((((((triple10) -> rule5)) -> rule3)) -> rule4))]
("cat" "sees" "tiger" "-")
((((((triple10) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int2
The rabbit is nice.
("rabbit" "is" "nice" "+")
int3
The cat is nice.
True
5
proof
[(((((((((triple10) -> rule5)) -> rule3)) -> rule4)) -> rule1) OR ((((((((triple10) -> rule5)) -> rule3)) -> rule4)) -> rule5))]
("cat" "is" "nice" "+")
((((((((triple10) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int3
The rabbit is nice.
("rabbit" "is" "nice" "+")
int4
((((((((triple10) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int3
The rabbit is nice.
("rabbit" "is" "nice" "+")
int4
The cat is not nice.
False
5
inv-proof
[(((((((((triple10) -> rule5)) -> rule3)) -> rule4)) -> rule1) OR ((((((((triple10) -> rule5)) -> rule3)) -> rule4)) -> rule5))]
("cat" "is" "nice" "-")
((((((((triple10) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int3
The rabbit is nice.
("rabbit" "is" "nice" "+")
int4
((((((((triple10) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int3
The rabbit is nice.
("rabbit" "is" "nice" "+")
int4
The cat needs the cat.
True
6
proof
[(((((((((((triple10) -> rule5)) -> rule3)) -> rule4)) -> rule1)) -> rule3) OR ((((((((((triple10) -> rule5)) -> rule3)) -> rule4)) -> rule5)) -> rule3))]
("cat" "needs" "cat" "+")
((((((((((triple10) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int4
The rabbit is nice.
("rabbit" "is" "nice" "+")
int5
((((((((((triple10) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int4
The rabbit is nice.
("rabbit" "is" "nice" "+")
int5
The cat does not need the cat.
False
6
inv-proof
[(((((((((((triple10) -> rule5)) -> rule3)) -> rule4)) -> rule1)) -> rule3) OR ((((((((((triple10) -> rule5)) -> rule3)) -> rule4)) -> rule5)) -> rule3))]
("cat" "needs" "cat" "-")
((((((((((triple10) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int4
The rabbit is nice.
("rabbit" "is" "nice" "+")
int5
((((((((((triple10) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int4
The rabbit is nice.
("rabbit" "is" "nice" "+")
int5
The bald eagle does not need the cat.
Unknown
inv-rconc
[@2: The bald eagle needs the cat.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("bald eagle" "needs" "cat" "-")
The tiger needs the tiger.
Unknown
rconc
[@1: The tiger needs the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "needs" "tiger" "+")
The bald eagle does not need the tiger.
Unknown
inv-rconc
[@1: The bald eagle needs the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "needs" "tiger" "-")
The bald eagle is nice.
Unknown
rconc
[@1: The bald eagle is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bald eagle" "is" "nice" "+")
The cat is not red.
Unknown
inv-rconc
[@1: The cat is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "is" "red" "-")
The rabbit sees the cat.
Unknown
random
[@0: The rabbit sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "cat" "+")
The bald eagle is not red.
Unknown
inv-random
[@0: The bald eagle is red.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "red" "-")
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 like the bald eagle.
Unknown
inv-random
[@0: The rabbit likes the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "bald eagle" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
The tiger does not like the rabbit.
Unknown
inv-random
[@0: The tiger likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "rabbit" "-")
The bald eagle is blue.
Unknown
random
[@0: The bald eagle is blue.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "blue" "+")
@0: The bald eagle is kind.[(triple1)] The bald eagle likes the rabbit.[(triple2)] The bald eagle needs the rabbit.[(triple3)] The cat is rough.[(triple4)] The cat likes the rabbit.[(triple5)] The rabbit likes the tiger.[(triple6)] The rabbit needs the bald eagle.[(triple7)] The rabbit needs the tiger.[(triple8)] The rabbit sees the bald eagle.[(triple9)] The rabbit sees the tiger.[(triple10)] The tiger is nice.[(triple11)] The tiger is rough.[(triple12)] The tiger needs the cat.[(triple13 OR ((triple11) -> rule3))] The tiger sees the rabbit.[(triple14)] @1: The cat needs the tiger.[(((triple4 triple5) -> rule2))] The rabbit is nice.[(((triple10) -> rule5))] @2: The rabbit needs the cat.[(((((triple10) -> rule5)) -> rule3))] @3: The cat sees the tiger.[(((((((triple10) -> rule5)) -> rule3)) -> rule4))] @4: The cat is nice.[(((((((((triple10) -> rule5)) -> rule3)) -> rule4)) -> rule1) OR ((((((((triple10) -> rule5)) -> rule3)) -> rule4)) -> rule5))] @5: The cat needs the cat.[(((((((((((triple10) -> rule5)) -> rule3)) -> rule4)) -> rule1)) -> rule3) OR ((((((((((triple10) -> rule5)) -> rule3)) -> rule4)) -> rule5)) -> rule3))]
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
triple1
The bald eagle likes the rabbit.
("bald eagle" "likes" "rabbit" "+")
triple2
The bald eagle needs the rabbit.
("bald eagle" "needs" "rabbit" "+")
triple3
The cat is rough.
("cat" "is" "rough" "+")
triple4
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple5
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple6
The rabbit needs the bald eagle.
("rabbit" "needs" "bald eagle" "+")
triple7
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple8
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
triple9
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple10
The tiger is nice.
("tiger" "is" "nice" "+")
triple11
The tiger is rough.
("tiger" "is" "rough" "+")
triple12
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple13
((triple11) -> (rule3 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple14
The cat needs the tiger.
("cat" "needs" "tiger" "+")
((triple4 triple5) -> (rule2 % int1))
The cat needs the tiger.
("cat" "needs" "tiger" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
((triple10) -> (rule5 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
((((triple10) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
((((((triple10) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int2
The rabbit is nice.
("rabbit" "is" "nice" "+")
int3
The cat is nice.
("cat" "is" "nice" "+")
((((((((triple10) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int3
The rabbit is nice.
("rabbit" "is" "nice" "+")
int4
((((((((triple10) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int3
The rabbit is nice.
("rabbit" "is" "nice" "+")
int4
The cat needs the cat.
("cat" "needs" "cat" "+")
((((((((((triple10) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int4
The rabbit is nice.
("rabbit" "is" "nice" "+")
int5
((((((((((triple10) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
int4
The rabbit is nice.
("rabbit" "is" "nice" "+")
int5