The bald eagle visits the tiger. The bear sees the tiger. The cow visits the bald eagle. The tiger sees the bear. If something sees the bear then it chases the bear. If something visits the bald eagle and the bald eagle visits the tiger then the tiger visits the bald eagle. If something sees the tiger then it chases the cow. If something chases the bear then it is big. If something chases the bear and it is nice then the bear is cold. If something visits the tiger and it visits the bald eagle then it is young.
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
If something sees the bear then it chases the bear.
((("something" "sees" "bear" "+")) -> ("something" "chases" "bear" "+"))
If something visits the bald eagle and the bald eagle visits the tiger then the tiger visits the bald eagle.
((("something" "visits" "bald eagle" "+") ("bald eagle" "visits" "tiger" "+")) -> ("tiger" "visits" "bald eagle" "+"))
If something sees the tiger then it chases the cow.
((("something" "sees" "tiger" "+")) -> ("something" "chases" "cow" "+"))
If something chases the bear then it is big.
((("something" "chases" "bear" "+")) -> ("something" "is" "big" "+"))
If something chases the bear and it is nice then the bear is cold.
((("something" "chases" "bear" "+") ("something" "is" "nice" "+")) -> ("bear" "is" "cold" "+"))
If something visits the tiger and it visits the bald eagle then it is young.
((("something" "visits" "tiger" "+") ("something" "visits" "bald eagle" "+")) -> ("something" "is" "young" "+"))
The bald eagle visits the tiger.
True
1
proof
[(triple1)]
("bald eagle" "visits" "tiger" "+")
triple1
The cow does not visit the bald eagle.
False
1
inv-proof
[(triple3)]
("cow" "visits" "bald eagle" "-")
triple3
The tiger chases the bear.
True
2
proof
[(((triple4) -> rule1))]
("tiger" "chases" "bear" "+")
((triple4) -> (rule1 % int1))
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int1
The tiger does not chase the bear.
False
2
inv-proof
[(((triple4) -> rule1))]
("tiger" "chases" "bear" "-")
((triple4) -> (rule1 % int1))
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int1
The tiger is big.
True
3
proof
[(((((triple4) -> rule1)) -> rule4))]
("tiger" "is" "big" "+")
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int2
The tiger is not big.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule4))]
("tiger" "is" "big" "-")
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int2
The bear is not young.
Unknown
inv-rconc
[@1: The bear is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "is" "young" "-")
The cow is big.
Unknown
rconc
[@2: The cow is big.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("cow" "is" "big" "+")
The tiger is not young.
Unknown
inv-rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "is" "young" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
The bear does not chase the tiger.
Unknown
inv-random
[@0: The bear chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "tiger" "-")
The tiger chases the bald eagle.
Unknown
random
[@0: The tiger chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "bald eagle" "+")
@0: The bald eagle visits the tiger.[(triple1)] The bear sees the tiger.[(triple2)] The cow visits the bald eagle.[(triple3)] The tiger sees the bear.[(triple4)] @1: The bear chases the cow.[(((triple2) -> rule3))] The tiger chases the bear.[(((triple4) -> rule1))] The tiger visits the bald eagle.[(((triple3 triple1) -> rule2))] @2: The tiger is big.[(((((triple4) -> rule1)) -> rule4))]
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
triple1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple2
The cow visits the bald eagle.
("cow" "visits" "bald eagle" "+")
triple3
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple4
The bear chases the cow.
("bear" "chases" "cow" "+")
((triple2) -> (rule3 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The tiger chases the bear.
("tiger" "chases" "bear" "+")
((triple4) -> (rule1 % int1))
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int1
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
((triple3 triple1) -> (rule2 % int1))
The tiger visits the bald eagle.
("tiger" "visits" "bald eagle" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int2