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