The bear sees the tiger. The cow eats the bear. The cow sees the dog. The dog chases the bear. The dog chases the tiger. The tiger chases the bear. The tiger is big. If something is kind and it eats the dog then the dog chases the bear. If something chases the cow then the cow is big. If something chases the bear and the bear chases the tiger then the tiger eats the dog. If something is kind and it eats the tiger then the tiger is big. If something is big then it eats the tiger. If something eats the tiger then it chases the cow.
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The cow eats the bear.
("cow" "eats" "bear" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog chases the bear.
("dog" "chases" "bear" "+")
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
The tiger is big.
("tiger" "is" "big" "+")
If something is kind and it eats the dog then the dog chases the bear.
((("something" "is" "kind" "+") ("something" "eats" "dog" "+")) -> ("dog" "chases" "bear" "+"))
If something chases the cow then the cow is big.
((("something" "chases" "cow" "+")) -> ("cow" "is" "big" "+"))
If something chases the bear and the bear chases the tiger then the tiger eats the dog.
((("something" "chases" "bear" "+") ("bear" "chases" "tiger" "+")) -> ("tiger" "eats" "dog" "+"))
If something is kind and it eats the tiger then the tiger is big.
((("something" "is" "kind" "+") ("something" "eats" "tiger" "+")) -> ("tiger" "is" "big" "+"))
If something is big then it eats the tiger.
((("something" "is" "big" "+")) -> ("something" "eats" "tiger" "+"))
If something eats the tiger then it chases the cow.
((("something" "eats" "tiger" "+")) -> ("something" "chases" "cow" "+"))
The dog chases the tiger.
True
1
proof
[(triple5)]
("dog" "chases" "tiger" "+")
triple5
The dog does not chase the tiger.
False
1
inv-proof
[(triple5)]
("dog" "chases" "tiger" "-")
triple5
The tiger eats the tiger.
True
2
proof
[(((triple7) -> rule5))]
("tiger" "eats" "tiger" "+")
((triple7) -> (rule5 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger does not eat the tiger.
False
2
inv-proof
[(((triple7) -> rule5))]
("tiger" "eats" "tiger" "-")
((triple7) -> (rule5 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger chases the cow.
True
3
proof
[(((((triple7) -> rule5)) -> rule6))]
("tiger" "chases" "cow" "+")
((((triple7) -> (rule5 % int2))) -> (rule6 % int1))
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger does not chase the cow.
False
3
inv-proof
[(((((triple7) -> rule5)) -> rule6))]
("tiger" "chases" "cow" "-")
((((triple7) -> (rule5 % int2))) -> (rule6 % int1))
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The cow is big.
True
4
proof
[(((((((triple7) -> rule5)) -> rule6)) -> rule2))]
("cow" "is" "big" "+")
((((((triple7) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int3
The cow is not big.
False
4
inv-proof
[(((((((triple7) -> rule5)) -> rule6)) -> rule2))]
("cow" "is" "big" "-")
((((((triple7) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int3
The cow eats the tiger.
True
5
proof
[(((((((((triple7) -> rule5)) -> rule6)) -> rule2)) -> rule5))]
("cow" "eats" "tiger" "+")
((((((((triple7) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int3
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int4
The cow does not eat the tiger.
False
5
inv-proof
[(((((((((triple7) -> rule5)) -> rule6)) -> rule2)) -> rule5))]
("cow" "eats" "tiger" "-")
((((((((triple7) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int3
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int4
The cow chases the cow.
True
6
proof
[(((((((((((triple7) -> rule5)) -> rule6)) -> rule2)) -> rule5)) -> rule6))]
("cow" "chases" "cow" "+")
((((((((((triple7) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int4
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int5
The cow does not chase the cow.
False
6
inv-proof
[(((((((((((triple7) -> rule5)) -> rule6)) -> rule2)) -> rule5)) -> rule6))]
("cow" "chases" "cow" "-")
((((((((((triple7) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int4
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int5
The dog does not chase the cow.
Unknown
inv-rconc
[@2: The dog chases the cow.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("dog" "chases" "cow" "-")
The dog eats the tiger.
Unknown
rconc
[@1: The dog eats the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "eats" "tiger" "+")
The bear does not chase the cow.
Unknown
inv-rconc
[@2: The bear chases the cow.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("bear" "chases" "cow" "-")
The bear eats the tiger.
Unknown
rconc
[@1: The bear eats the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "eats" "tiger" "+")
The tiger does not eat the dog.
Unknown
inv-rconc
[@1: The tiger eats the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "eats" "dog" "-")
The tiger sees the dog.
Unknown
random
[@0: The tiger sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "dog" "+")
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
The bear chases the dog.
Unknown
random
[@0: The bear chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "dog" "+")
The bear is not round.
Unknown
inv-random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "-")
The tiger eats the cow.
Unknown
random
[@0: The tiger eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "cow" "+")
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 dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
@0: The bear sees the tiger.[(triple1)] The cow eats the bear.[(triple2)] The cow sees the dog.[(triple3)] The dog chases the bear.[(triple4)] The dog chases the tiger.[(triple5)] The tiger chases the bear.[(triple6)] The tiger is big.[(triple7)] @1: The tiger eats the tiger.[(((triple7) -> rule5))] @2: The tiger chases the cow.[(((((triple7) -> rule5)) -> rule6))] @3: The cow is big.[(((((((triple7) -> rule5)) -> rule6)) -> rule2))] @4: The cow eats the tiger.[(((((((((triple7) -> rule5)) -> rule6)) -> rule2)) -> rule5))] @5: The cow chases the cow.[(((((((((((triple7) -> rule5)) -> rule6)) -> rule2)) -> rule5)) -> rule6))]
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple1
The cow eats the bear.
("cow" "eats" "bear" "+")
triple2
The cow sees the dog.
("cow" "sees" "dog" "+")
triple3
The dog chases the bear.
("dog" "chases" "bear" "+")
triple4
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple5
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple6
The tiger is big.
("tiger" "is" "big" "+")
triple7
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((triple7) -> (rule5 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger chases the cow.
("tiger" "chases" "cow" "+")
((((triple7) -> (rule5 % int2))) -> (rule6 % int1))
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The cow is big.
("cow" "is" "big" "+")
((((((triple7) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int2
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int3
The cow eats the tiger.
("cow" "eats" "tiger" "+")
((((((((triple7) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int1
The cow is big.
("cow" "is" "big" "+")
int2
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int3
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int4
The cow chases the cow.
("cow" "chases" "cow" "+")
((((((((((triple7) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow eats the tiger.
("cow" "eats" "tiger" "+")
int2
The cow is big.
("cow" "is" "big" "+")
int3
The tiger chases the cow.
("tiger" "chases" "cow" "+")
int4
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int5