The bald eagle visits the bear. The bear eats the bald eagle. The bear sees the dog. The bear visits the dog. The dog is blue. The tiger sees the bear. The tiger visits the bear. If the tiger sees the bear then the tiger eats the dog. If something visits the bald eagle then it eats the bald eagle. If something eats the tiger and it eats the bald eagle then the tiger is round. If something is kind then it visits the bald eagle. If something visits the tiger and the tiger does not see the dog then the dog is cold. If something sees the bear then it is kind.
The bald eagle visits the bear.
("bald eagle" "visits" "bear" "+")
The bear eats the bald eagle.
("bear" "eats" "bald eagle" "+")
The bear sees the dog.
("bear" "sees" "dog" "+")
The bear visits the dog.
("bear" "visits" "dog" "+")
The dog is blue.
("dog" "is" "blue" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
If the tiger sees the bear then the tiger eats the dog.
((("tiger" "sees" "bear" "+")) -> ("tiger" "eats" "dog" "+"))
If something visits the bald eagle then it eats the bald eagle.
((("something" "visits" "bald eagle" "+")) -> ("something" "eats" "bald eagle" "+"))
If something eats the tiger and it eats the bald eagle then the tiger is round.
((("something" "eats" "tiger" "+") ("something" "eats" "bald eagle" "+")) -> ("tiger" "is" "round" "+"))
If something is kind then it visits the bald eagle.
((("something" "is" "kind" "+")) -> ("something" "visits" "bald eagle" "+"))
If something visits the tiger and the tiger does not see the dog then the dog is cold.
((("something" "visits" "tiger" "+") ("tiger" "sees" "dog" "~")) -> ("dog" "is" "cold" "+"))
If something sees the bear then it is kind.
((("something" "sees" "bear" "+")) -> ("something" "is" "kind" "+"))
The tiger visits the bear.
True
1
proof
[(triple7)]
("tiger" "visits" "bear" "+")
triple7
The bear does not eat the bald eagle.
False
1
inv-proof
[(triple2)]
("bear" "eats" "bald eagle" "-")
triple2
The tiger is kind.
True
2
proof
[(((triple6) -> rule6))]
("tiger" "is" "kind" "+")
((triple6) -> (rule6 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger does not eat the dog.
False
2
inv-proof
[(((triple6) -> rule1))]
("tiger" "eats" "dog" "-")
((triple6) -> (rule1 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The tiger visits the bald eagle.
True
3
proof
[(((((triple6) -> rule6)) -> rule4))]
("tiger" "visits" "bald eagle" "+")
((((triple6) -> (rule6 % int2))) -> (rule4 % int1))
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger does not visit the bald eagle.
False
3
inv-proof
[(((((triple6) -> rule6)) -> rule4))]
("tiger" "visits" "bald eagle" "-")
((((triple6) -> (rule6 % int2))) -> (rule4 % int1))
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger eats the bald eagle.
True
4
proof
[(((((((triple6) -> rule6)) -> rule4)) -> rule2))]
("tiger" "eats" "bald eagle" "+")
((((((triple6) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The tiger eats the bald eagle.
("tiger" "eats" "bald eagle" "+")
int1
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The tiger does not eat the bald eagle.
False
4
inv-proof
[(((((((triple6) -> rule6)) -> rule4)) -> rule2))]
("tiger" "eats" "bald eagle" "-")
((((((triple6) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The tiger eats the bald eagle.
("tiger" "eats" "bald eagle" "+")
int1
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The bald eagle is not kind.
Unknown
inv-rconc
[@1: The bald eagle is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bald eagle" "is" "kind" "-")
The dog is cold.
Unknown
rconc
[@1: The dog is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "cold" "+")
The bear is not kind.
Unknown
inv-rconc
[@1: The bear is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "is" "kind" "-")
The bald eagle visits the bald eagle.
Unknown
rconc
[@2: The bald eagle visits the bald eagle.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("bald eagle" "visits" "bald eagle" "+")
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The tiger visits the dog.
Unknown
random
[@0: The tiger visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "dog" "+")
The dog does not see the bald eagle.
Unknown
inv-random
[@0: The dog sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "bald eagle" "-")
The bald eagle visits the tiger.
Unknown
random
[@0: The bald eagle visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "visits" "tiger" "+")
@0: The bald eagle visits the bear.[(triple1)] The bear eats the bald eagle.[(triple2)] The bear sees the dog.[(triple3)] The bear visits the dog.[(triple4)] The dog is blue.[(triple5)] The tiger sees the bear.[(triple6)] The tiger visits the bear.[(triple7)] @1: The tiger eats the dog.[(((triple6) -> rule1))] The tiger is kind.[(((triple6) -> rule6))] @2: The tiger visits the bald eagle.[(((((triple6) -> rule6)) -> rule4))] @3: The tiger eats the bald eagle.[(((((((triple6) -> rule6)) -> rule4)) -> rule2))]
The bald eagle visits the bear.
("bald eagle" "visits" "bear" "+")
triple1
The bear eats the bald eagle.
("bear" "eats" "bald eagle" "+")
triple2
The bear sees the dog.
("bear" "sees" "dog" "+")
triple3
The bear visits the dog.
("bear" "visits" "dog" "+")
triple4
The dog is blue.
("dog" "is" "blue" "+")
triple5
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple6
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple7
The tiger eats the dog.
("tiger" "eats" "dog" "+")
((triple6) -> (rule1 % int1))
The tiger eats the dog.
("tiger" "eats" "dog" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
((triple6) -> (rule6 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
((((triple6) -> (rule6 % int2))) -> (rule4 % int1))
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger eats the bald eagle.
("tiger" "eats" "bald eagle" "+")
((((((triple6) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The tiger eats the bald eagle.
("tiger" "eats" "bald eagle" "+")
int1
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3