The bald eagle chases the tiger. The bald eagle likes the cow. The bear is green. The bear needs the cow. The cow chases the tiger. The cow is round. The cow needs the bear. The cow needs the tiger. The tiger chases the bear. The tiger is big. If something likes the bear then it likes the cow. If something is big then it likes the bear. If something likes the tiger then it is green. If the tiger likes the cow then the cow is big. If something likes the tiger and the tiger needs the bald eagle then the tiger chases the bald eagle.
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
The bear is green.
("bear" "is" "green" "+")
The bear needs the cow.
("bear" "needs" "cow" "+")
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow is round.
("cow" "is" "round" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
The tiger is big.
("tiger" "is" "big" "+")
If something likes the bear then it likes the cow.
((("something" "likes" "bear" "+")) -> ("something" "likes" "cow" "+"))
If something is big then it likes the bear.
((("something" "is" "big" "+")) -> ("something" "likes" "bear" "+"))
If something likes the tiger then it is green.
((("something" "likes" "tiger" "+")) -> ("something" "is" "green" "+"))
If the tiger likes the cow then the cow is big.
((("tiger" "likes" "cow" "+")) -> ("cow" "is" "big" "+"))
If something likes the tiger and the tiger needs the bald eagle then the tiger chases the bald eagle.
((("something" "likes" "tiger" "+") ("tiger" "needs" "bald eagle" "+")) -> ("tiger" "chases" "bald eagle" "+"))
The bald eagle chases the tiger.
True
1
proof
[(triple1)]
("bald eagle" "chases" "tiger" "+")
triple1
The cow does not need the tiger.
False
1
inv-proof
[(triple8)]
("cow" "needs" "tiger" "-")
triple8
The tiger likes the bear.
True
2
proof
[(((triple10) -> rule2))]
("tiger" "likes" "bear" "+")
((triple10) -> (rule2 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The tiger does not like the bear.
False
2
inv-proof
[(((triple10) -> rule2))]
("tiger" "likes" "bear" "-")
((triple10) -> (rule2 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The tiger likes the cow.
True
3
proof
[(((((triple10) -> rule2)) -> rule1))]
("tiger" "likes" "cow" "+")
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The tiger does not like the cow.
False
3
inv-proof
[(((((triple10) -> rule2)) -> rule1))]
("tiger" "likes" "cow" "-")
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The cow is big.
True
4
proof
[(((((((triple10) -> rule2)) -> rule1)) -> rule4))]
("cow" "is" "big" "+")
((((((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int2
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int3
The cow is not big.
False
4
inv-proof
[(((((((triple10) -> rule2)) -> rule1)) -> rule4))]
("cow" "is" "big" "-")
((((((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int2
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int3
The cow likes the bear.
True
5
proof
[(((((((((triple10) -> rule2)) -> rule1)) -> rule4)) -> rule2))]
("cow" "likes" "bear" "+")
((((((((triple10) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The cow likes the bear.
("cow" "likes" "bear" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int3
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int4
The cow does not like the bear.
False
5
inv-proof
[(((((((((triple10) -> rule2)) -> rule1)) -> rule4)) -> rule2))]
("cow" "likes" "bear" "-")
((((((((triple10) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The cow likes the bear.
("cow" "likes" "bear" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int3
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int4
The cow likes the cow.
True
6
proof
[(((((((((((triple10) -> rule2)) -> rule1)) -> rule4)) -> rule2)) -> rule1))]
("cow" "likes" "cow" "+")
((((((((((triple10) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow likes the bear.
("cow" "likes" "bear" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int4
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int5
The cow does not like the cow.
False
6
inv-proof
[(((((((((((triple10) -> rule2)) -> rule1)) -> rule4)) -> rule2)) -> rule1))]
("cow" "likes" "cow" "-")
((((((((((triple10) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow likes the bear.
("cow" "likes" "bear" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int4
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int5
The cow is not green.
Unknown
inv-rconc
[@1: The cow is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "green" "-")
The bald eagle likes the bear.
Unknown
rconc
[@1: The bald eagle likes the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "likes" "bear" "+")
The bear does not like the bear.
Unknown
inv-rconc
[@1: The bear likes the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "likes" "bear" "-")
The bald eagle is green.
Unknown
rconc
[@1: The bald eagle is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bald eagle" "is" "green" "+")
The tiger is not green.
Unknown
inv-rconc
[@1: The tiger is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "is" "green" "-")
The tiger chases the bald eagle.
Unknown
rconc
[@1: The tiger chases the bald eagle.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "chases" "bald eagle" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
The bald eagle likes the bald eagle.
Unknown
random
[@0: The bald eagle likes the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "likes" "bald eagle" "+")
The tiger does not chase the cow.
Unknown
inv-random
[@0: The tiger chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "cow" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
The bear is not kind.
Unknown
inv-random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "-")
The tiger needs the bald eagle.
Unknown
random
[@0: The tiger needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "bald eagle" "+")
@0: The bald eagle chases the tiger.[(triple1)] The bald eagle likes the cow.[(triple2)] The bear is green.[(triple3)] The bear needs the cow.[(triple4)] The cow chases the tiger.[(triple5)] The cow is round.[(triple6)] The cow needs the bear.[(triple7)] The cow needs the tiger.[(triple8)] The tiger chases the bear.[(triple9)] The tiger is big.[(triple10)] @1: The tiger likes the bear.[(((triple10) -> rule2))] @2: The tiger likes the cow.[(((((triple10) -> rule2)) -> rule1))] @3: The cow is big.[(((((((triple10) -> rule2)) -> rule1)) -> rule4))] @4: The cow likes the bear.[(((((((((triple10) -> rule2)) -> rule1)) -> rule4)) -> rule2))] @5: The cow likes the cow.[(((((((((((triple10) -> rule2)) -> rule1)) -> rule4)) -> rule2)) -> rule1))]
The bald eagle chases the tiger.
("bald eagle" "chases" "tiger" "+")
triple1
The bald eagle likes the cow.
("bald eagle" "likes" "cow" "+")
triple2
The bear is green.
("bear" "is" "green" "+")
triple3
The bear needs the cow.
("bear" "needs" "cow" "+")
triple4
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple5
The cow is round.
("cow" "is" "round" "+")
triple6
The cow needs the bear.
("cow" "needs" "bear" "+")
triple7
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple8
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple9
The tiger is big.
("tiger" "is" "big" "+")
triple10
The tiger likes the bear.
("tiger" "likes" "bear" "+")
((triple10) -> (rule2 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The cow is big.
("cow" "is" "big" "+")
((((((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int2
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int3
The cow likes the bear.
("cow" "likes" "bear" "+")
((((((((triple10) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The cow likes the bear.
("cow" "likes" "bear" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int3
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int4
The cow likes the cow.
("cow" "likes" "cow" "+")
((((((((((triple10) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow likes the bear.
("cow" "likes" "bear" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int4
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int5