The cat does not eat the tiger. The cat likes the tiger. The dog does not need the squirrel. The squirrel eats the tiger. The squirrel does not need the cat. The tiger eats the cat. The tiger likes the dog. If someone likes the squirrel then they do not eat the cat. If someone needs the dog then the dog eats the tiger. If someone eats the cat then they need the dog. If someone needs the dog then they are nice. If someone eats the dog and the dog does not like the cat then they are not big. If someone likes the dog and the dog eats the tiger then the dog eats the cat.
The cat does not eat the tiger.
("cat" "eats" "tiger" "-")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The dog does not need the squirrel.
("dog" "needs" "squirrel" "-")
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The squirrel does not need the cat.
("squirrel" "needs" "cat" "-")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
If someone likes the squirrel then they do not eat the cat.
((("someone" "likes" "squirrel" "+")) -> ("someone" "eats" "cat" "-"))
If someone needs the dog then the dog eats the tiger.
((("someone" "needs" "dog" "+")) -> ("dog" "eats" "tiger" "+"))
If someone eats the cat then they need the dog.
((("someone" "eats" "cat" "+")) -> ("someone" "needs" "dog" "+"))
If someone needs the dog then they are nice.
((("someone" "needs" "dog" "+")) -> ("someone" "is" "nice" "+"))
If someone eats the dog and the dog does not like the cat then they are not big.
((("someone" "eats" "dog" "+") ("dog" "likes" "cat" "~")) -> ("someone" "is" "big" "-"))
If someone likes the dog and the dog eats the tiger then the dog eats the cat.
((("someone" "likes" "dog" "+") ("dog" "eats" "tiger" "+")) -> ("dog" "eats" "cat" "+"))
The squirrel eats the tiger.
True
1
proof
[(triple4)]
("squirrel" "eats" "tiger" "+")
triple4
The dog needs the squirrel.
False
1
inv-proof
[(triple3)]
("dog" "needs" "squirrel" "+")
triple3
The tiger needs the dog.
True
2
proof
[(((triple6) -> rule3))]
("tiger" "needs" "dog" "+")
((triple6) -> (rule3 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The tiger does not need the dog.
False
2
inv-proof
[(((triple6) -> rule3))]
("tiger" "needs" "dog" "-")
((triple6) -> (rule3 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The tiger is nice.
True
3
proof
[(((((triple6) -> rule3)) -> rule4))]
("tiger" "is" "nice" "+")
((((triple6) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int2
The tiger is not nice.
False
3
inv-proof
[(((((triple6) -> rule3)) -> rule4))]
("tiger" "is" "nice" "-")
((((triple6) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int2
The dog eats the cat.
True
5
proof
[(((triple7 ((((triple6) -> rule3)) -> rule2)) -> rule6))]
("dog" "eats" "cat" "+")
((triple7 ((((triple6) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int2
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int3
The dog does not eat the cat.
False
5
inv-proof
[(((triple7 ((((triple6) -> rule3)) -> rule2)) -> rule6))]
("dog" "eats" "cat" "-")
((triple7 ((((triple6) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int2
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int3
The dog needs the dog.
True
6
proof
[(((((triple7 ((((triple6) -> rule3)) -> rule2)) -> rule6)) -> rule3))]
("dog" "needs" "dog" "+")
((((triple7 ((((triple6) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog eats the cat.
("dog" "eats" "cat" "+")
int2
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int3
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int4
The dog does not need the dog.
False
6
inv-proof
[(((((triple7 ((((triple6) -> rule3)) -> rule2)) -> rule6)) -> rule3))]
("dog" "needs" "dog" "-")
((((triple7 ((((triple6) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog eats the cat.
("dog" "eats" "cat" "+")
int2
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int3
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int4
The dog is nice.
True
7
proof
[(((((((triple7 ((((triple6) -> rule3)) -> rule2)) -> rule6)) -> rule3)) -> rule4))]
("dog" "is" "nice" "+")
((((((triple7 ((((triple6) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog eats the cat.
("dog" "eats" "cat" "+")
int3
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int4
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int5
The dog is not nice.
False
7
inv-proof
[(((((((triple7 ((((triple6) -> rule3)) -> rule2)) -> rule6)) -> rule3)) -> rule4))]
("dog" "is" "nice" "-")
((((((triple7 ((((triple6) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog eats the cat.
("dog" "eats" "cat" "+")
int3
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int4
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int5
The squirrel is not nice.
Unknown
inv-rconc
[@2: The squirrel is nice.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("squirrel" "is" "nice" "-")
The cat is nice.
Unknown
rconc
[@2: The cat is nice.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("cat" "is" "nice" "+")
The cat does not need the dog.
Unknown
inv-rconc
[@1: The cat needs the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "needs" "dog" "-")
The squirrel needs the dog.
Unknown
rconc
[@1: The squirrel needs the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "needs" "dog" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The dog likes the tiger.
Unknown
random
[@0: The dog likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "tiger" "+")
The squirrel is not rough.
Unknown
inv-random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "-")
The cat eats the dog.
Unknown
random
[@0: The cat eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "dog" "+")
The dog does not eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The squirrel eats the dog.
Unknown
random
[@0: The squirrel eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "dog" "+")
The dog does not eat the squirrel.
Unknown
inv-random
[@0: The dog eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "squirrel" "-")
The dog is rough.
Unknown
random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "+")
@0: The cat does not eat the tiger.[(triple1)] The cat likes the tiger.[(triple2)] The dog does not need the squirrel.[(triple3)] The squirrel does not need the cat.[(triple5)] The squirrel eats the tiger.[(triple4)] The tiger eats the cat.[(triple6)] The tiger likes the dog.[(triple7)] @1: The tiger needs the dog.[(((triple6) -> rule3))] @2: The dog eats the tiger.[(((((triple6) -> rule3)) -> rule2))] The tiger is nice.[(((((triple6) -> rule3)) -> rule4))] @3: The dog eats the cat.[(((triple7 ((((triple6) -> rule3)) -> rule2)) -> rule6))] @4: The dog needs the dog.[(((((triple7 ((((triple6) -> rule3)) -> rule2)) -> rule6)) -> rule3))] @5: The dog is nice.[(((((((triple7 ((((triple6) -> rule3)) -> rule2)) -> rule6)) -> rule3)) -> rule4))]
The cat does not eat the tiger.
("cat" "eats" "tiger" "-")
triple1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple2
The dog does not need the squirrel.
("dog" "needs" "squirrel" "-")
triple3
The squirrel does not need the cat.
("squirrel" "needs" "cat" "-")
triple5
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple4
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple6
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple7
The tiger needs the dog.
("tiger" "needs" "dog" "+")
((triple6) -> (rule3 % int1))
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
((((triple6) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int2
The dog eats the cat.
("dog" "eats" "cat" "+")
((triple7 ((((triple6) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int2
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int3
The dog needs the dog.
("dog" "needs" "dog" "+")
((((triple7 ((((triple6) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog eats the cat.
("dog" "eats" "cat" "+")
int2
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int3
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int4
The dog is nice.
("dog" "is" "nice" "+")
((((((triple7 ((((triple6) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog eats the cat.
("dog" "eats" "cat" "+")
int3
The dog eats the tiger.
("dog" "eats" "tiger" "+")
int4
The tiger needs the dog.
("tiger" "needs" "dog" "+")
int5