The bald eagle eats the rabbit. The bear is rough. The dog sees the bald eagle. The rabbit sees the dog. If something sees the bald eagle and it sees the dog then it is round. If something is green then it sees the bald eagle. If the bald eagle is blue and the bald eagle chases the rabbit then the rabbit chases the bald eagle. If something sees the dog then it is green. All green things are blue. If something eats the bald eagle then the bald eagle is blue. If something sees the bald eagle then it chases the bald eagle. All blue things are green.
The bald eagle eats the rabbit.
("bald eagle" "eats" "rabbit" "+")
The bear is rough.
("bear" "is" "rough" "+")
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
If something sees the bald eagle and it sees the dog then it is round.
((("something" "sees" "bald eagle" "+") ("something" "sees" "dog" "+")) -> ("something" "is" "round" "+"))
If something is green then it sees the bald eagle.
((("something" "is" "green" "+")) -> ("something" "sees" "bald eagle" "+"))
If the bald eagle is blue and the bald eagle chases the rabbit then the rabbit chases the bald eagle.
((("bald eagle" "is" "blue" "+") ("bald eagle" "chases" "rabbit" "+")) -> ("rabbit" "chases" "bald eagle" "+"))
If something sees the dog then it is green.
((("something" "sees" "dog" "+")) -> ("something" "is" "green" "+"))
All green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If something eats the bald eagle then the bald eagle is blue.
((("something" "eats" "bald eagle" "+")) -> ("bald eagle" "is" "blue" "+"))
If something sees the bald eagle then it chases the bald eagle.
((("something" "sees" "bald eagle" "+")) -> ("something" "chases" "bald eagle" "+"))
All blue things are green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
The bear is rough.
True
1
proof
[(triple2)]
("bear" "is" "rough" "+")
triple2
The bear is not rough.
False
1
inv-proof
[(triple2)]
("bear" "is" "rough" "-")
triple2
The rabbit is green.
True
2
proof
[(((triple4) -> rule4))]
("rabbit" "is" "green" "+")
((triple4) -> (rule4 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The dog does not chase the bald eagle.
False
2
inv-proof
[(((triple3) -> rule7))]
("dog" "chases" "bald eagle" "-")
((triple3) -> (rule7 % int1))
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
int1
The rabbit is blue.
True
3
proof
[(((((triple4) -> rule4)) -> rule5))]
("rabbit" "is" "blue" "+")
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit is not blue.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule5))]
("rabbit" "is" "blue" "-")
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit is round.
True
5
proof
[(((((((triple4) -> rule4)) -> rule2) triple4) -> rule1))]
("rabbit" "is" "round" "+")
((((((triple4) -> (rule4 % int3))) -> (rule2 % int2)) triple4) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The rabbit does not chase the bald eagle.
False
4
inv-proof
[(((((((triple4) -> rule4)) -> rule2)) -> rule7))]
("rabbit" "chases" "bald eagle" "-")
((((((triple4) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
int1
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The bear is not green.
Unknown
inv-rconc
[@3: The bear is green.[CWA. Example of deepest failure = (rule8 <- rule5 <- rule4 <- FAIL)]]
("bear" "is" "green" "-")
The bear is round.
Unknown
rconc
[@1: The bear is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "round" "+")
The bald eagle is not round.
Unknown
inv-rconc
[@1: The bald eagle is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "is" "round" "-")
The dog is round.
Unknown
rconc
[@1: The dog is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "round" "+")
The bald eagle does not chase the bear.
Unknown
inv-random
[@0: The bald eagle chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "chases" "bear" "-")
The bald eagle is big.
Unknown
random
[@0: The bald eagle is big.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "big" "+")
The dog does not eat the bald eagle.
Unknown
inv-random
[@0: The dog eats the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "bald eagle" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
@0: The bald eagle eats the rabbit.[(triple1)] The bear is rough.[(triple2)] The dog sees the bald eagle.[(triple3)] The rabbit sees the dog.[(triple4)] @1: The dog chases the bald eagle.[(((triple3) -> rule7))] The rabbit is green.[(((triple4) -> rule4))] @2: The rabbit is blue.[(((((triple4) -> rule4)) -> rule5))] The rabbit sees the bald eagle.[(((((triple4) -> rule4)) -> rule2))] @3: The rabbit chases the bald eagle.[(((((((triple4) -> rule4)) -> rule2)) -> rule7))] The rabbit is round.[(((((((triple4) -> rule4)) -> rule2) triple4) -> rule1))]
The bald eagle eats the rabbit.
("bald eagle" "eats" "rabbit" "+")
triple1
The bear is rough.
("bear" "is" "rough" "+")
triple2
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
triple3
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple4
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
((triple3) -> (rule7 % int1))
The dog chases the bald eagle.
("dog" "chases" "bald eagle" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
((triple4) -> (rule4 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
((((((triple4) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
int1
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
The rabbit is round.
("rabbit" "is" "round" "+")
((((((triple4) -> (rule4 % int3))) -> (rule2 % int2)) triple4) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3