The bald eagle chases the rabbit. The cat needs the bald eagle. The rabbit is red. The rabbit needs the cat. The rabbit visits the tiger. The tiger chases the cat. The tiger chases the rabbit. If someone visits the rabbit and the rabbit is nice then the rabbit is young. If someone is red then they visit the bald eagle. If the cat chases the rabbit and the rabbit visits the tiger then the rabbit is young. If someone needs the cat and the cat chases the rabbit then they chase the rabbit. If someone chases the cat then the cat chases the rabbit. If someone needs the tiger then they need the cat.
The bald eagle chases the rabbit.
("bald eagle" "chases" "rabbit" "+")
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
If someone visits the rabbit and the rabbit is nice then the rabbit is young.
((("someone" "visits" "rabbit" "+") ("rabbit" "is" "nice" "+")) -> ("rabbit" "is" "young" "+"))
If someone is red then they visit the bald eagle.
((("someone" "is" "red" "+")) -> ("someone" "visits" "bald eagle" "+"))
If the cat chases the rabbit and the rabbit visits the tiger then the rabbit is young.
((("cat" "chases" "rabbit" "+") ("rabbit" "visits" "tiger" "+")) -> ("rabbit" "is" "young" "+"))
If someone needs the cat and the cat chases the rabbit then they chase the rabbit.
((("someone" "needs" "cat" "+") ("cat" "chases" "rabbit" "+")) -> ("someone" "chases" "rabbit" "+"))
If someone chases the cat then the cat chases the rabbit.
((("someone" "chases" "cat" "+")) -> ("cat" "chases" "rabbit" "+"))
If someone needs the tiger then they need the cat.
((("someone" "needs" "tiger" "+")) -> ("someone" "needs" "cat" "+"))
The cat needs the bald eagle.
True
1
proof
[(triple2)]
("cat" "needs" "bald eagle" "+")
triple2
The rabbit does not visit the tiger.
False
1
inv-proof
[(triple5)]
("rabbit" "visits" "tiger" "-")
triple5
The cat chases the rabbit.
True
2
proof
[(((triple6) -> rule5))]
("cat" "chases" "rabbit" "+")
((triple6) -> (rule5 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The rabbit does not visit the bald eagle.
False
2
inv-proof
[(((triple3) -> rule2))]
("rabbit" "visits" "bald eagle" "-")
((triple3) -> (rule2 % int1))
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
int1
The rabbit chases the rabbit.
True
4
proof
[(((triple4 ((triple6) -> rule5)) -> rule4))]
("rabbit" "chases" "rabbit" "+")
((triple4 ((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The rabbit is not young.
False
4
inv-proof
[(((((triple6) -> rule5) triple5) -> rule3))]
("rabbit" "is" "young" "-")
((((triple6) -> (rule5 % int2)) triple5) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The tiger does not visit the bald eagle.
Unknown
inv-rconc
[@1: The tiger visits the bald eagle.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "visits" "bald eagle" "-")
The cat visits the bald eagle.
Unknown
rconc
[@1: The cat visits the bald eagle.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "visits" "bald eagle" "+")
The bald eagle does not need the cat.
Unknown
inv-rconc
[@1: The bald eagle needs the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bald eagle" "needs" "cat" "-")
The tiger chases the bald eagle.
Unknown
random
[@0: The tiger chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "bald eagle" "+")
The cat does not visit the rabbit.
Unknown
inv-random
[@0: The cat visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "rabbit" "-")
The rabbit chases the cat.
Unknown
random
[@0: The rabbit chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "cat" "+")
@0: The bald eagle chases the rabbit.[(triple1)] The cat needs the bald eagle.[(triple2)] The rabbit is red.[(triple3)] The rabbit needs the cat.[(triple4)] The rabbit visits the tiger.[(triple5)] The tiger chases the cat.[(triple6)] The tiger chases the rabbit.[(triple7)] @1: The cat chases the rabbit.[(((triple6) -> rule5))] The rabbit visits the bald eagle.[(((triple3) -> rule2))] @2: The rabbit chases the rabbit.[(((triple4 ((triple6) -> rule5)) -> rule4))] The rabbit is young.[(((((triple6) -> rule5) triple5) -> rule3))]
The bald eagle chases the rabbit.
("bald eagle" "chases" "rabbit" "+")
triple1
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
triple2
The rabbit is red.
("rabbit" "is" "red" "+")
triple3
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple4
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple5
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple6
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple7
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
((triple6) -> (rule5 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
((triple3) -> (rule2 % int1))
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((triple4 ((triple6) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
((((triple6) -> (rule5 % int2)) triple5) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2