The bald eagle is big. The bald eagle is nice. The bald eagle needs the cat. The bald eagle sees the cat. The bald eagle visits the cat. The cat is blue. The cat is cold. The cat is green. The cat is nice. The cat needs the bald eagle. The cat sees the bald eagle. The cat visits the bald eagle. If someone visits the bald eagle and the bald eagle needs the cat then the cat sees the bald eagle. If someone is cold then they visit the bald eagle. If someone visits the cat then they visit the bald eagle. If someone needs the cat and the cat is blue then the cat visits the bald eagle. If someone is nice then they need the bald eagle. Blue people are green.
The bald eagle is big.
("bald eagle" "is" "big" "+")
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
If someone visits the bald eagle and the bald eagle needs the cat then the cat sees the bald eagle.
((("someone" "visits" "bald eagle" "+") ("bald eagle" "needs" "cat" "+")) -> ("cat" "sees" "bald eagle" "+"))
If someone is cold then they visit the bald eagle.
((("someone" "is" "cold" "+")) -> ("someone" "visits" "bald eagle" "+"))
If someone visits the cat then they visit the bald eagle.
((("someone" "visits" "cat" "+")) -> ("someone" "visits" "bald eagle" "+"))
If someone needs the cat and the cat is blue then the cat visits the bald eagle.
((("someone" "needs" "cat" "+") ("cat" "is" "blue" "+")) -> ("cat" "visits" "bald eagle" "+"))
If someone is nice then they need the bald eagle.
((("someone" "is" "nice" "+")) -> ("someone" "needs" "bald eagle" "+"))
Blue people are green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
The bald eagle is nice.
True
1
proof
[(triple2)]
("bald eagle" "is" "nice" "+")
triple2
The cat does not visit the bald eagle.
False
1
inv-proof
[(triple12 OR ((triple7) -> rule2) OR ((triple3 triple6) -> rule4))]
("cat" "visits" "bald eagle" "-")
triple12
((triple7) -> (rule2 % int1))
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int1
((triple3 triple6) -> (rule4 % int1))
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int1
The bald eagle is not green.
Unknown
inv-rconc
[@1: The bald eagle is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bald eagle" "is" "green" "-")
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 big.[(triple1)] The bald eagle is nice.[(triple2)] The bald eagle needs the cat.[(triple3)] The bald eagle sees the cat.[(triple4)] The bald eagle visits the cat.[(triple5)] The cat is blue.[(triple6)] The cat is cold.[(triple7)] The cat is green.[(triple8 OR ((triple6) -> rule6))] The cat is nice.[(triple9)] The cat needs the bald eagle.[(triple10 OR ((triple9) -> rule5))] The cat sees the bald eagle.[(triple11 OR ((triple12 triple3) -> rule1) OR ((((triple5) -> rule3) triple3) -> rule1) OR ((((triple7) -> rule2) triple3) -> rule1) OR ((((triple3 triple6) -> rule4) triple3) -> rule1))] The cat visits the bald eagle.[(triple12 OR ((triple7) -> rule2) OR ((triple3 triple6) -> rule4))] @1: The bald eagle needs the bald eagle.[(((triple2) -> rule5))] The bald eagle visits the bald eagle.[(((triple5) -> rule3))]
The bald eagle is big.
("bald eagle" "is" "big" "+")
triple1
The bald eagle is nice.
("bald eagle" "is" "nice" "+")
triple2
The bald eagle needs the cat.
("bald eagle" "needs" "cat" "+")
triple3
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
triple4
The bald eagle visits the cat.
("bald eagle" "visits" "cat" "+")
triple5
The cat is blue.
("cat" "is" "blue" "+")
triple6
The cat is cold.
("cat" "is" "cold" "+")
triple7
The cat is green.
("cat" "is" "green" "+")
triple8
((triple6) -> (rule6 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
triple9
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
triple10
((triple9) -> (rule5 % int1))
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
int1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
triple11
((triple12 triple3) -> (rule1 % int1))
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int1
((((triple5) -> (rule3 % int2)) triple3) -> (rule1 % int1))
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int1
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int2
((((triple7) -> (rule2 % int2)) triple3) -> (rule1 % int1))
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int1
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int2
((((triple3 triple6) -> (rule4 % int2)) triple3) -> (rule1 % int1))
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int1
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int2
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
triple12
((triple7) -> (rule2 % int1))
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int1
((triple3 triple6) -> (rule4 % int1))
The cat visits the bald eagle.
("cat" "visits" "bald eagle" "+")
int1
The bald eagle needs the bald eagle.
("bald eagle" "needs" "bald eagle" "+")
((triple2) -> (rule5 % int1))
The bald eagle needs the bald eagle.
("bald eagle" "needs" "bald eagle" "+")
int1
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
((triple5) -> (rule3 % int1))
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int1