The bear eats the cow. The bear eats the tiger. The bear needs the dog. The cow is big. The cow is young. The cow likes the bear. The cow needs the tiger. The dog eats the cow. The tiger eats the bear. The tiger is big. If someone eats the bear and they like the tiger then the bear needs the cow. If someone eats the bear then they need the cow. If someone needs the cow then they need the tiger. If someone needs the cow and the cow is cold then the cow needs the dog. If someone needs the tiger and they are big then they like the tiger.
The bear eats the cow.
("bear" "eats" "cow" "+")
The bear eats the tiger.
("bear" "eats" "tiger" "+")
The bear needs the dog.
("bear" "needs" "dog" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is young.
("cow" "is" "young" "+")
The cow likes the bear.
("cow" "likes" "bear" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The dog eats the cow.
("dog" "eats" "cow" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger is big.
("tiger" "is" "big" "+")
If someone eats the bear and they like the tiger then the bear needs the cow.
((("someone" "eats" "bear" "+") ("someone" "likes" "tiger" "+")) -> ("bear" "needs" "cow" "+"))
If someone eats the bear then they need the cow.
((("someone" "eats" "bear" "+")) -> ("someone" "needs" "cow" "+"))
If someone needs the cow then they need the tiger.
((("someone" "needs" "cow" "+")) -> ("someone" "needs" "tiger" "+"))
If someone needs the cow and the cow is cold then the cow needs the dog.
((("someone" "needs" "cow" "+") ("cow" "is" "cold" "+")) -> ("cow" "needs" "dog" "+"))
If someone needs the tiger and they are big then they like the tiger.
((("someone" "needs" "tiger" "+") ("someone" "is" "big" "+")) -> ("someone" "likes" "tiger" "+"))
The tiger is big.
True
1
proof
[(triple10)]
("tiger" "is" "big" "+")
triple10
The bear does not need the dog.
False
1
inv-proof
[(triple3)]
("bear" "needs" "dog" "-")
triple3
The tiger needs the cow.
True
2
proof
[(((triple9) -> rule2))]
("tiger" "needs" "cow" "+")
((triple9) -> (rule2 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The cow does not like the tiger.
False
3
inv-proof
[(((triple7 triple4) -> rule5))]
("cow" "likes" "tiger" "-")
((triple7 triple4) -> (rule5 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The tiger needs the tiger.
True
3
proof
[(((((triple9) -> rule2)) -> rule3))]
("tiger" "needs" "tiger" "+")
((((triple9) -> (rule2 % int2))) -> (rule3 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The tiger does not need the tiger.
False
3
inv-proof
[(((((triple9) -> rule2)) -> rule3))]
("tiger" "needs" "tiger" "-")
((((triple9) -> (rule2 % int2))) -> (rule3 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The tiger likes the tiger.
True
5
proof
[(((((((triple9) -> rule2)) -> rule3) triple10) -> rule5))]
("tiger" "likes" "tiger" "+")
((((((triple9) -> (rule2 % int3))) -> (rule3 % int2)) triple10) -> (rule5 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int3
The tiger does not like the tiger.
False
5
inv-proof
[(((((((triple9) -> rule2)) -> rule3) triple10) -> rule5))]
("tiger" "likes" "tiger" "-")
((((((triple9) -> (rule2 % int3))) -> (rule3 % int2)) triple10) -> (rule5 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int3
The bear needs the cow.
True
7
proof
[(((triple9 ((((((triple9) -> rule2)) -> rule3) triple10) -> rule5)) -> rule1))]
("bear" "needs" "cow" "+")
((triple9 ((((((triple9) -> (rule2 % int4))) -> (rule3 % int3)) triple10) -> (rule5 % int2))) -> (rule1 % int1))
The bear needs the cow.
("bear" "needs" "cow" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int3
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int4
The bear does not need the cow.
False
7
inv-proof
[(((triple9 ((((((triple9) -> rule2)) -> rule3) triple10) -> rule5)) -> rule1))]
("bear" "needs" "cow" "-")
((triple9 ((((((triple9) -> (rule2 % int4))) -> (rule3 % int3)) triple10) -> (rule5 % int2))) -> (rule1 % int1))
The bear needs the cow.
("bear" "needs" "cow" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int3
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int4
The bear needs the tiger.
True
8
proof
[(((((triple9 ((((((triple9) -> rule2)) -> rule3) triple10) -> rule5)) -> rule1)) -> rule3))]
("bear" "needs" "tiger" "+")
((((triple9 ((((((triple9) -> (rule2 % int5))) -> (rule3 % int4)) triple10) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The bear needs the cow.
("bear" "needs" "cow" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int4
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int5
The bear does not need the tiger.
False
8
inv-proof
[(((((triple9 ((((((triple9) -> rule2)) -> rule3) triple10) -> rule5)) -> rule1)) -> rule3))]
("bear" "needs" "tiger" "-")
((((triple9 ((((((triple9) -> (rule2 % int5))) -> (rule3 % int4)) triple10) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The bear needs the cow.
("bear" "needs" "cow" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int4
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int5
The dog does not need the cow.
Unknown
inv-rconc
[@1: The dog needs the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "needs" "cow" "-")
The bear likes the tiger.
Unknown
rconc
[@1: The bear likes the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "likes" "tiger" "+")
The dog does not like the tiger.
Unknown
inv-rconc
[@1: The dog likes the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "likes" "tiger" "-")
The cow needs the cow.
Unknown
rconc
[@1: The cow needs the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "needs" "cow" "+")
The dog does not need the tiger.
Unknown
inv-rconc
[@2: The dog needs the tiger.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("dog" "needs" "tiger" "-")
The cow needs the dog.
Unknown
rconc
[@1: The cow needs the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "needs" "dog" "+")
The dog does not like the bear.
Unknown
inv-random
[@0: The dog likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "bear" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
The dog is not big.
Unknown
inv-random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
The dog does not need the bear.
Unknown
inv-random
[@0: The dog needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "bear" "-")
The cow eats the bear.
Unknown
random
[@0: The cow eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "bear" "+")
@0: The bear eats the cow.[(triple1)] The bear eats the tiger.[(triple2)] The bear needs the dog.[(triple3)] The cow is big.[(triple4)] The cow is young.[(triple5)] The cow likes the bear.[(triple6)] The cow needs the tiger.[(triple7)] The dog eats the cow.[(triple8)] The tiger eats the bear.[(triple9)] The tiger is big.[(triple10)] @1: The cow likes the tiger.[(((triple7 triple4) -> rule5))] The tiger needs the cow.[(((triple9) -> rule2))] @2: The tiger needs the tiger.[(((((triple9) -> rule2)) -> rule3))] @3: The tiger likes the tiger.[(((((((triple9) -> rule2)) -> rule3) triple10) -> rule5))] @4: The bear needs the cow.[(((triple9 ((((((triple9) -> rule2)) -> rule3) triple10) -> rule5)) -> rule1))] @5: The bear needs the tiger.[(((((triple9 ((((((triple9) -> rule2)) -> rule3) triple10) -> rule5)) -> rule1)) -> rule3))]
The bear eats the cow.
("bear" "eats" "cow" "+")
triple1
The bear eats the tiger.
("bear" "eats" "tiger" "+")
triple2
The bear needs the dog.
("bear" "needs" "dog" "+")
triple3
The cow is big.
("cow" "is" "big" "+")
triple4
The cow is young.
("cow" "is" "young" "+")
triple5
The cow likes the bear.
("cow" "likes" "bear" "+")
triple6
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple7
The dog eats the cow.
("dog" "eats" "cow" "+")
triple8
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple9
The tiger is big.
("tiger" "is" "big" "+")
triple10
The cow likes the tiger.
("cow" "likes" "tiger" "+")
((triple7 triple4) -> (rule5 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
((triple9) -> (rule2 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((((triple9) -> (rule2 % int2))) -> (rule3 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((((((triple9) -> (rule2 % int3))) -> (rule3 % int2)) triple10) -> (rule5 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int3
The bear needs the cow.
("bear" "needs" "cow" "+")
((triple9 ((((((triple9) -> (rule2 % int4))) -> (rule3 % int3)) triple10) -> (rule5 % int2))) -> (rule1 % int1))
The bear needs the cow.
("bear" "needs" "cow" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int3
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int4
The bear needs the tiger.
("bear" "needs" "tiger" "+")
((((triple9 ((((((triple9) -> (rule2 % int5))) -> (rule3 % int4)) triple10) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The bear needs the cow.
("bear" "needs" "cow" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int4
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int5