The bear chases the tiger. The tiger likes the bear. If something likes the bear then it is green. If something chases the tiger then the tiger likes the bear. If something chases the tiger and the tiger likes the bear then it sees the bear. If something is green then it chases the bear. If something sees the tiger and it is young then it chases the tiger. If the tiger chases the bear and the tiger is blue then the bear chases the tiger. If something chases the tiger then it is young. If something likes the tiger and the tiger chases the bear then it sees the tiger.
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The tiger likes the bear.
("tiger" "likes" "bear" "+")
If something likes the bear then it is green.
((("something" "likes" "bear" "+")) -> ("something" "is" "green" "+"))
If something chases the tiger then the tiger likes the bear.
((("something" "chases" "tiger" "+")) -> ("tiger" "likes" "bear" "+"))
If something chases the tiger and the tiger likes the bear then it sees the bear.
((("something" "chases" "tiger" "+") ("tiger" "likes" "bear" "+")) -> ("something" "sees" "bear" "+"))
If something is green then it chases the bear.
((("something" "is" "green" "+")) -> ("something" "chases" "bear" "+"))
If something sees the tiger and it is young then it chases the tiger.
((("something" "sees" "tiger" "+") ("something" "is" "young" "+")) -> ("something" "chases" "tiger" "+"))
If the tiger chases the bear and the tiger is blue then the bear chases the tiger.
((("tiger" "chases" "bear" "+") ("tiger" "is" "blue" "+")) -> ("bear" "chases" "tiger" "+"))
If something chases the tiger then it is young.
((("something" "chases" "tiger" "+")) -> ("something" "is" "young" "+"))
If something likes the tiger and the tiger chases the bear then it sees the tiger.
((("something" "likes" "tiger" "+") ("tiger" "chases" "bear" "+")) -> ("something" "sees" "tiger" "+"))
The bear chases the tiger.
True
1
proof
[(triple1)]
("bear" "chases" "tiger" "+")
triple1
The tiger does not like the bear.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule2))]
("tiger" "likes" "bear" "-")
triple2
((triple1) -> (rule2 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The bear sees the bear.
True
3
proof
[(((triple1 triple2) -> rule3) OR ((triple1 ((triple1) -> rule2)) -> rule3))]
("bear" "sees" "bear" "+")
((triple1 triple2) -> (rule3 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The tiger is not green.
False
2
inv-proof
[(((triple2) -> rule1) OR ((((triple1) -> rule2)) -> rule1))]
("tiger" "is" "green" "-")
((triple2) -> (rule1 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The tiger chases the bear.
True
3
proof
[(((((triple2) -> rule1)) -> rule4) OR ((((((triple1) -> rule2)) -> rule1)) -> rule4))]
("tiger" "chases" "bear" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int3
The tiger does not chase the bear.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule4) OR ((((((triple1) -> rule2)) -> rule1)) -> rule4))]
("tiger" "chases" "bear" "-")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int3
The tiger does not chase the tiger.
Unknown
inv-rconc
[@2: The tiger chases the tiger.[CWA. Example of deepest failure = (rule5 <- rule8 <- FAIL)]]
("tiger" "chases" "tiger" "-")
The tiger sees the tiger.
Unknown
rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("tiger" "sees" "tiger" "+")
The bear does not chase the bear.
Unknown
inv-rconc
[@2: The bear chases the bear.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("bear" "chases" "bear" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
The bear is not kind.
Unknown
inv-random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "-")
The tiger is blue.
Unknown
random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "+")
@0: The bear chases the tiger.[(triple1)] The tiger likes the bear.[(triple2 OR ((triple1) -> rule2))] @1: The bear is young.[(((triple1) -> rule7))] The bear sees the bear.[(((triple1 triple2) -> rule3) OR ((triple1 ((triple1) -> rule2)) -> rule3))] The tiger is green.[(((triple2) -> rule1) OR ((((triple1) -> rule2)) -> rule1))] @2: The tiger chases the bear.[(((((triple2) -> rule1)) -> rule4) OR ((((((triple1) -> rule2)) -> rule1)) -> rule4))]
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
triple2
((triple1) -> (rule2 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The bear is young.
("bear" "is" "young" "+")
((triple1) -> (rule7 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear sees the bear.
("bear" "sees" "bear" "+")
((triple1 triple2) -> (rule3 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The bear sees the bear.
("bear" "sees" "bear" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
((triple2) -> (rule1 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The tiger chases the bear.
("tiger" "chases" "bear" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int3