The bald eagle is red. The bald eagle sees the cat. The cat is round. The cat is young. The cat needs the cow. The cat sees the bald eagle. The cat sees the cow. The cow is young. The cow needs the bald eagle. The cow visits the cat. If someone is red then they see the cat. If the bald eagle is young then the bald eagle needs the cat. If someone sees the cat then the cat sees the cow. If someone needs the bald eagle and the bald eagle sees the cat then the bald eagle needs the cow. If someone is blue then they see the cat. If someone needs the cat and the cat sees the cow then the cat needs the bald eagle. If the bald eagle sees the cat then the cat needs the cow. If someone needs the cow and they see the cat then the cat needs the cow.
The bald eagle is red.
("bald eagle" "is" "red" "+")
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
The cat is round.
("cat" "is" "round" "+")
The cat is young.
("cat" "is" "young" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
The cat sees the cow.
("cat" "sees" "cow" "+")
The cow is young.
("cow" "is" "young" "+")
The cow needs the bald eagle.
("cow" "needs" "bald eagle" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
If someone is red then they see the cat.
((("someone" "is" "red" "+")) -> ("someone" "sees" "cat" "+"))
If the bald eagle is young then the bald eagle needs the cat.
((("bald eagle" "is" "young" "+")) -> ("bald eagle" "needs" "cat" "+"))
If someone sees the cat then the cat sees the cow.
((("someone" "sees" "cat" "+")) -> ("cat" "sees" "cow" "+"))
If someone needs the bald eagle and the bald eagle sees the cat then the bald eagle needs the cow.
((("someone" "needs" "bald eagle" "+") ("bald eagle" "sees" "cat" "+")) -> ("bald eagle" "needs" "cow" "+"))
If someone is blue then they see the cat.
((("someone" "is" "blue" "+")) -> ("someone" "sees" "cat" "+"))
If someone needs the cat and the cat sees the cow then the cat needs the bald eagle.
((("someone" "needs" "cat" "+") ("cat" "sees" "cow" "+")) -> ("cat" "needs" "bald eagle" "+"))
If the bald eagle sees the cat then the cat needs the cow.
((("bald eagle" "sees" "cat" "+")) -> ("cat" "needs" "cow" "+"))
If someone needs the cow and they see the cat then the cat needs the cow.
((("someone" "needs" "cow" "+") ("someone" "sees" "cat" "+")) -> ("cat" "needs" "cow" "+"))
The bald eagle sees the cat.
True
1
proof
[(triple2 OR ((triple1) -> rule1))]
("bald eagle" "sees" "cat" "+")
triple2
((triple1) -> (rule1 % int1))
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int1
The cat is not young.
False
1
inv-proof
[(triple4)]
("cat" "is" "young" "-")
triple4
The bald eagle needs the cow.
True
3
proof
[(((triple9 triple2) -> rule4) OR ((triple9 ((triple1) -> rule1)) -> rule4))]
("bald eagle" "needs" "cow" "+")
((triple9 triple2) -> (rule4 % int1))
The bald eagle needs the cow.
("bald eagle" "needs" "cow" "+")
int1
((triple9 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The bald eagle needs the cow.
("bald eagle" "needs" "cow" "+")
int1
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int2
The bald eagle does not need the cow.
False
3
inv-proof
[(((triple9 triple2) -> rule4) OR ((triple9 ((triple1) -> rule1)) -> rule4))]
("bald eagle" "needs" "cow" "-")
((triple9 triple2) -> (rule4 % int1))
The bald eagle needs the cow.
("bald eagle" "needs" "cow" "+")
int1
((triple9 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The bald eagle needs the cow.
("bald eagle" "needs" "cow" "+")
int1
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int2
The bald eagle does not need the cat.
Unknown
inv-rconc
[@1: The bald eagle needs the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "needs" "cat" "-")
The cat needs the bald eagle.
Unknown
rconc
[@2: The cat needs the bald eagle.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("cat" "needs" "bald eagle" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
@0: The bald eagle is red.[(triple1)] The bald eagle sees the cat.[(triple2 OR ((triple1) -> rule1))] The cat is round.[(triple3)] The cat is young.[(triple4)] The cat needs the cow.[(triple5 OR ((triple2) -> rule7) OR ((((triple1) -> rule1)) -> rule7) OR ((((triple9 triple2) -> rule4) triple2) -> rule8) OR ((((triple9 triple2) -> rule4) ((triple1) -> rule1)) -> rule8) OR ((((triple9 ((triple1) -> rule1)) -> rule4) triple2) -> rule8) OR ((((triple9 ((triple1) -> rule1)) -> rule4) ((triple1) -> rule1)) -> rule8))] The cat sees the bald eagle.[(triple6)] The cat sees the cow.[(triple7 OR ((triple2) -> rule3) OR ((((triple1) -> rule1)) -> rule3))] The cow is young.[(triple8)] The cow needs the bald eagle.[(triple9)] The cow visits the cat.[(triple10)] @1: The bald eagle needs the cow.[(((triple9 triple2) -> rule4) OR ((triple9 ((triple1) -> rule1)) -> rule4))]
The bald eagle is red.
("bald eagle" "is" "red" "+")
triple1
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
triple2
((triple1) -> (rule1 % int1))
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
triple3
The cat is young.
("cat" "is" "young" "+")
triple4
The cat needs the cow.
("cat" "needs" "cow" "+")
triple5
((triple2) -> (rule7 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int2
((((triple9 triple2) -> (rule4 % int2)) triple2) -> (rule8 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The bald eagle needs the cow.
("bald eagle" "needs" "cow" "+")
int2
((((triple9 triple2) -> (rule4 % int3)) ((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int2
The bald eagle needs the cow.
("bald eagle" "needs" "cow" "+")
int3
((((triple9 ((triple1) -> (rule1 % int3))) -> (rule4 % int2)) triple2) -> (rule8 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The bald eagle needs the cow.
("bald eagle" "needs" "cow" "+")
int2
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int3
((((triple9 ((triple1) -> (rule1 % int3))) -> (rule4 % int2)) ((triple1) -> (rule1 % int3))) -> (rule8 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The bald eagle needs the cow.
("bald eagle" "needs" "cow" "+")
int2
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int3
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
triple6
The cat sees the cow.
("cat" "sees" "cow" "+")
triple7
((triple2) -> (rule3 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int2
The cow is young.
("cow" "is" "young" "+")
triple8
The cow needs the bald eagle.
("cow" "needs" "bald eagle" "+")
triple9
The cow visits the cat.
("cow" "visits" "cat" "+")
triple10
The bald eagle needs the cow.
("bald eagle" "needs" "cow" "+")
((triple9 triple2) -> (rule4 % int1))
The bald eagle needs the cow.
("bald eagle" "needs" "cow" "+")
int1
((triple9 ((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The bald eagle needs the cow.
("bald eagle" "needs" "cow" "+")
int1
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int2