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