The cow likes the squirrel. The cow needs the tiger. The dog visits the cow. The squirrel does not like the cow. The squirrel likes the tiger. The tiger is big. The tiger is nice. The tiger likes the cow. The tiger needs the dog. The tiger visits the squirrel. If someone likes the tiger then they visit the dog. If the cow visits the squirrel then the cow is round. If someone is nice then they like the tiger. If someone needs the tiger and the tiger visits the dog then they like the dog. If someone is round and they like the dog then the dog visits the tiger. If the dog is round then the dog does not like the tiger. If the squirrel does not visit the tiger then the squirrel needs the dog. If someone visits the dog then the dog is young.
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
The squirrel does not like the cow.
("squirrel" "likes" "cow" "-")
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If someone likes the tiger then they visit the dog.
((("someone" "likes" "tiger" "+")) -> ("someone" "visits" "dog" "+"))
If the cow visits the squirrel then the cow is round.
((("cow" "visits" "squirrel" "+")) -> ("cow" "is" "round" "+"))
If someone is nice then they like the tiger.
((("someone" "is" "nice" "+")) -> ("someone" "likes" "tiger" "+"))
If someone needs the tiger and the tiger visits the dog then they like the dog.
((("someone" "needs" "tiger" "+") ("tiger" "visits" "dog" "+")) -> ("someone" "likes" "dog" "+"))
If someone is round and they like the dog then the dog visits the tiger.
((("someone" "is" "round" "+") ("someone" "likes" "dog" "+")) -> ("dog" "visits" "tiger" "+"))
If the dog is round then the dog does not like the tiger.
((("dog" "is" "round" "+")) -> ("dog" "likes" "tiger" "-"))
If the squirrel does not visit the tiger then the squirrel needs the dog.
((("squirrel" "visits" "tiger" "~")) -> ("squirrel" "needs" "dog" "+"))
If someone visits the dog then the dog is young.
((("someone" "visits" "dog" "+")) -> ("dog" "is" "young" "+"))
The cow needs the tiger.
True
1
proof
[(triple2)]
("cow" "needs" "tiger" "+")
triple2
The dog does not visit the cow.
False
1
inv-proof
[(triple3)]
("dog" "visits" "cow" "-")
triple3
The tiger likes the tiger.
True
2
proof
[(((triple7) -> rule3))]
("tiger" "likes" "tiger" "+")
((triple7) -> (rule3 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The squirrel does not visit the dog.
False
2
inv-proof
[(((triple5) -> rule1))]
("squirrel" "visits" "dog" "-")
((triple5) -> (rule1 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1
The tiger visits the dog.
True
3
proof
[(((((triple7) -> rule3)) -> rule1))]
("tiger" "visits" "dog" "+")
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The tiger does not visit the dog.
False
3
inv-proof
[(((((triple7) -> rule3)) -> rule1))]
("tiger" "visits" "dog" "-")
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The cow likes the dog.
True
5
proof
[(((triple2 ((((triple7) -> rule3)) -> rule1)) -> rule4))]
("cow" "likes" "dog" "+")
((triple2 ((((triple7) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cow likes the dog.
("cow" "likes" "dog" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The cow does not like the dog.
False
5
inv-proof
[(((triple2 ((((triple7) -> rule3)) -> rule1)) -> rule4))]
("cow" "likes" "dog" "-")
((triple2 ((((triple7) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cow likes the dog.
("cow" "likes" "dog" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The cow does not like the tiger.
Unknown
inv-rconc
[@1: The cow likes the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "likes" "tiger" "-")
The cow is round.
Unknown
rconc
[@1: The cow is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "round" "+")
The cow does not visit the dog.
Unknown
inv-rconc
[@2: The cow visits the dog.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("cow" "visits" "dog" "-")
The squirrel likes the dog.
Unknown
rconc
[@1: The squirrel likes the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "likes" "dog" "+")
The tiger does not need the squirrel.
Unknown
inv-random
[@0: The tiger needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "squirrel" "-")
The squirrel is round.
Unknown
random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "+")
The cow does not visit the tiger.
Unknown
inv-random
[@0: The cow visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "tiger" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
@0: The cow likes the squirrel.[(triple1)] The cow needs the tiger.[(triple2)] The dog visits the cow.[(triple3)] The squirrel does not like the cow.[(triple4)] The squirrel likes the tiger.[(triple5)] The tiger is big.[(triple6)] The tiger is nice.[(triple7)] The tiger likes the cow.[(triple8)] The tiger needs the dog.[(triple9)] The tiger visits the squirrel.[(triple10)] @1: The squirrel visits the dog.[(((triple5) -> rule1))] The tiger likes the tiger.[(((triple7) -> rule3))] @2: The dog is young.[(((((triple5) -> rule1)) -> rule8) OR ((((((triple7) -> rule3)) -> rule1)) -> rule8))] The tiger visits the dog.[(((((triple7) -> rule3)) -> rule1))] @3: The cow likes the dog.[(((triple2 ((((triple7) -> rule3)) -> rule1)) -> rule4))]
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
triple1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple2
The dog visits the cow.
("dog" "visits" "cow" "+")
triple3
The squirrel does not like the cow.
("squirrel" "likes" "cow" "-")
triple4
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
triple5
The tiger is big.
("tiger" "is" "big" "+")
triple6
The tiger is nice.
("tiger" "is" "nice" "+")
triple7
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple8
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple9
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple10
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
((triple5) -> (rule1 % int1))
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple7) -> (rule3 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The dog is young.
("dog" "is" "young" "+")
((((triple5) -> (rule1 % int2))) -> (rule8 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
int2
((((((triple7) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3
The tiger visits the dog.
("tiger" "visits" "dog" "+")
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int2
The cow likes the dog.
("cow" "likes" "dog" "+")
((triple2 ((((triple7) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The cow likes the dog.
("cow" "likes" "dog" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int3