The bald eagle is blue. The bald eagle visits the cat. The cat is cold. The cat is green. The cat needs the rabbit. The cat sees the rabbit. The cat visits the bald eagle. The rabbit is green. The rabbit is round. The rabbit needs the bald eagle. The rabbit needs the cat. The rabbit sees the bald eagle. The rabbit sees the cat. The rabbit visits the bald eagle. The rabbit visits the cat. If the rabbit sees the cat and the rabbit sees the bald eagle then the rabbit needs the bald eagle. If something visits the bald eagle then the bald eagle visits the cat. If something visits the cat and the cat is green then the cat is young. If the rabbit sees the cat and the cat is blue then the cat visits the rabbit. If something visits the cat then it sees the rabbit. If something visits the cat then it needs the bald eagle.
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is green.
("cat" "is" "green" "+")
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit needs the bald eagle.
("rabbit" "needs" "bald eagle" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
If the rabbit sees the cat and the rabbit sees the bald eagle then the rabbit needs the bald eagle.
((("rabbit" "sees" "cat" "+") ("rabbit" "sees" "bald eagle" "+")) -> ("rabbit" "needs" "bald eagle" "+"))
If something visits the bald eagle then the bald eagle visits the cat.
((("something" "visits" "bald eagle" "+")) -> ("bald eagle" "visits" "cat" "+"))
If something visits the cat and the cat is green then the cat is young.
((("something" "visits" "cat" "+") ("cat" "is" "green" "+")) -> ("cat" "is" "young" "+"))
If the rabbit sees the cat and the cat is blue then the cat visits the rabbit.
((("rabbit" "sees" "cat" "+") ("cat" "is" "blue" "+")) -> ("cat" "visits" "rabbit" "+"))
If something visits the cat then it sees the rabbit.
((("something" "visits" "cat" "+")) -> ("something" "sees" "rabbit" "+"))
If something visits the cat then it needs the bald eagle.
((("something" "visits" "cat" "+")) -> ("something" "needs" "bald eagle" "+"))
The rabbit sees the bald eagle.
True
1
proof
[(triple12)]
("rabbit" "sees" "bald eagle" "+")
triple12
The cat does not need the rabbit.
False
1
inv-proof
[(triple5)]
("cat" "needs" "rabbit" "-")
triple5
The cat does not visit the rabbit.
Unknown
inv-rconc
[@1: The cat visits the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "visits" "rabbit" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
@0: The bald eagle is blue.[(triple1)] The bald eagle visits the cat.[(triple2 OR ((triple14) -> rule2) OR ((triple7) -> rule2))] The cat is cold.[(triple3)] The cat is green.[(triple4)] The cat needs the rabbit.[(triple5)] The cat sees the rabbit.[(triple6)] The cat visits the bald eagle.[(triple7)] The rabbit is green.[(triple8)] The rabbit is round.[(triple9)] The rabbit needs the bald eagle.[(triple10 OR ((triple15) -> rule6) OR ((triple13 triple12) -> rule1))] The rabbit needs the cat.[(triple11)] The rabbit sees the bald eagle.[(triple12)] The rabbit sees the cat.[(triple13)] The rabbit visits the bald eagle.[(triple14)] The rabbit visits the cat.[(triple15)] @1: The bald eagle needs the bald eagle.[(((triple2) -> rule6) OR ((((triple14) -> rule2)) -> rule6) OR ((((triple7) -> rule2)) -> rule6))] The bald eagle sees the rabbit.[(((triple2) -> rule5) OR ((((triple14) -> rule2)) -> rule5) OR ((((triple7) -> rule2)) -> rule5))] The cat is young.[(((triple15 triple4) -> rule3) OR ((triple2 triple4) -> rule3) OR ((((triple14) -> rule2) triple4) -> rule3) OR ((((triple7) -> rule2) triple4) -> rule3))] The rabbit sees the rabbit.[(((triple15) -> rule5))]
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
triple1
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
triple2
((triple14) -> (rule2 % int1))
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int1
((triple7) -> (rule2 % int1))
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
triple3
The cat is green.
("cat" "is" "green" "+")
triple4
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
triple5
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple6
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
triple7
The rabbit is green.
("rabbit" "is" "green" "+")
triple8
The rabbit is round.
("rabbit" "is" "round" "+")
triple9
The rabbit needs the bald eagle.
("rabbit" "needs" "bald eagle" "+")
triple10
((triple15) -> (rule6 % int1))
The rabbit needs the bald eagle.
("rabbit" "needs" "bald eagle" "+")
int1
((triple13 triple12) -> (rule1 % int1))
The rabbit needs the bald eagle.
("rabbit" "needs" "bald eagle" "+")
int1
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple11
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
triple12
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple13
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
triple14
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple15
The bald eagle needs the bald eagle.
("bald eagle" "needs" "bald eagle" "+")
((triple2) -> (rule6 % int1))
The bald eagle needs the bald eagle.
("bald eagle" "needs" "bald eagle" "+")
int1
((((triple14) -> (rule2 % int2))) -> (rule6 % int1))
The bald eagle needs the bald eagle.
("bald eagle" "needs" "bald eagle" "+")
int1
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int2
((((triple7) -> (rule2 % int2))) -> (rule6 % int1))
The bald eagle needs the bald eagle.
("bald eagle" "needs" "bald eagle" "+")
int1
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int2
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
((triple2) -> (rule5 % int1))
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int1
((((triple14) -> (rule2 % int2))) -> (rule5 % int1))
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int1
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int2
((((triple7) -> (rule2 % int2))) -> (rule5 % int1))
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int1
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int2
The cat is young.
("cat" "is" "young" "+")
((triple15 triple4) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((triple2 triple4) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
((((triple14) -> (rule2 % int2)) triple4) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int2
((((triple7) -> (rule2 % int2)) triple4) -> (rule3 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
int2
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((triple15) -> (rule5 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1